Skip to main content

🌌 Alpha_services.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Alpha_context.
Require TezosOfOCaml.Proto_alpha.Constants_services.
Require TezosOfOCaml.Proto_alpha.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Contract_services.
Require TezosOfOCaml.Proto_alpha.Delegate_services.
Require TezosOfOCaml.Proto_alpha.Nonce_hash.
Require TezosOfOCaml.Proto_alpha.Sapling_services.
Require TezosOfOCaml.Proto_alpha.Script_cache.
Require TezosOfOCaml.Proto_alpha.Services_registration.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_services.
Require TezosOfOCaml.Proto_alpha.Voting_services.

Definition custom_root {A : Set} : RPC_path.context A := RPC_path.open_root.

Module Seed_computation.
  Module S.
    Definition seed_computation_status_encoding
      : Data_encoding.encoding Alpha_context.Seed.seed_computation_status :=
      Data_encoding.union None
        [
          Data_encoding.case_value "Nonce revelation stage" None
            (Data_encoding.Tag 0)
            (Data_encoding.obj1
              (Data_encoding.req None None "nonce_revelation_stage"
                Data_encoding.unit_value))
            (fun (function_parameter :
              Alpha_context.Seed.seed_computation_status) ⇒
              match function_parameter with
              | Alpha_context.Seed.Nonce_revelation_stageSome tt
              | _None
              end)
            (fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              Alpha_context.Seed.Nonce_revelation_stage);
          Data_encoding.case_value "VDF revelation stage" None
            (Data_encoding.Tag 1)
            (Data_encoding.obj2
              (Data_encoding.req None None "seed_discriminant"
                Alpha_context.Seed.seed_encoding)
              (Data_encoding.req None None "seed_challenge"
                Alpha_context.Seed.seed_encoding))
            (fun (function_parameter :
              Alpha_context.Seed.seed_computation_status) ⇒
              match function_parameter with
              |
                Alpha_context.Seed.Vdf_revelation_stage {|
                  Alpha_context.Seed.seed_computation_status.Vdf_revelation_stage.seed_discriminant
                    := seed_discriminant;
                    Alpha_context.Seed.seed_computation_status.Vdf_revelation_stage.seed_challenge
                      :=
                      seed_challenge
                    |} ⇒
                Some (seed_discriminant, seed_challenge)
              | _None
              end)
            (fun (function_parameter :
              Alpha_context.Seed.seed × Alpha_context.Seed.seed) ⇒
              let '(seed_discriminant, seed_challenge) :=
                function_parameter in
              Alpha_context.Seed.Vdf_revelation_stage
                {|
                  Alpha_context.Seed.seed_computation_status.Vdf_revelation_stage.seed_discriminant
                    := seed_discriminant;
                  Alpha_context.Seed.seed_computation_status.Vdf_revelation_stage.seed_challenge
                    := seed_challenge; |});
          Data_encoding.case_value "Computation finished" None
            (Data_encoding.Tag 2)
            (Data_encoding.obj1
              (Data_encoding.req None None "computation_finished"
                Data_encoding.unit_value))
            (fun (function_parameter :
              Alpha_context.Seed.seed_computation_status) ⇒
              match function_parameter with
              | Alpha_context.Seed.Computation_finishedSome tt
              | _None
              end)
            (fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              Alpha_context.Seed.Computation_finished)
        ].

    Definition seed_computation
      : RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
        Alpha_context.Seed.seed_computation_status :=
      RPC_service.get_service (Some "Seed computation status") RPC_query.empty
        seed_computation_status_encoding
        (RPC_path.op_div (RPC_path.op_div custom_root "context")
          "seed_computation").
  End S.

Init function; without side-effects in Coq
  Definition init_module : unit :=
    Services_registration.register0 false S.seed_computation
      (fun (ctxt : Alpha_context.t) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Alpha_context.Seed.get_seed_computation_status ctxt).

  Definition get {A : Set} (ctxt : RPC_context.simple A) (block : A)
    : Error_monad.shell_tzresult Alpha_context.Seed.seed_computation_status :=
    RPC_context.make_call0 S.seed_computation ctxt block tt tt.
End Seed_computation.

Module Seed.
  Module S.
    Definition seed_value
      : RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
        Alpha_context.Seed.seed :=
      RPC_service.post_service
        (Some "Seed of the cycle to which the block belongs.") RPC_query.empty
        Data_encoding.empty Alpha_context.Seed.seed_encoding
        (RPC_path.op_div (RPC_path.op_div custom_root "context") "seed").
  End S.

Init function; without side-effects in Coq
  Definition init_module : unit :=
    Services_registration.register0 false S.seed_value
      (fun (ctxt : Alpha_context.t) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            let l_value := Alpha_context.Level.current ctxt in
            Alpha_context.Seed.for_cycle ctxt
              l_value.(Alpha_context.Level.t.cycle)).

  Definition get {A : Set} (ctxt : RPC_context.simple A) (block : A)
    : Error_monad.shell_tzresult Alpha_context.Seed.seed :=
    RPC_context.make_call0 S.seed_value ctxt block tt tt.
End Seed.

Module Nonce.
  Inductive info : Set :=
  | Revealed : Alpha_context.Nonce.t info
  | Missing : Nonce_hash.t info
  | Forgotten : info.

  Definition info_encoding : Data_encoding.encoding info :=
    Data_encoding.union None
      [
        Data_encoding.case_value "Revealed" None (Data_encoding.Tag 0)
          (Data_encoding.obj1
            (Data_encoding.req None None "nonce"
              Alpha_context.Nonce.encoding))
          (fun (function_parameter : info) ⇒
            match function_parameter with
            | Revealed nonce_valueSome nonce_value
            | _None
            end)
          (fun (nonce_value : Alpha_context.Nonce.nonce) ⇒
            Revealed nonce_value);
        Data_encoding.case_value "Missing" None (Data_encoding.Tag 1)
          (Data_encoding.obj1
            (Data_encoding.req None None "hash" Nonce_hash.encoding))
          (fun (function_parameter : info) ⇒
            match function_parameter with
            | Missing nonce_valueSome nonce_value
            | _None
            end)
          (fun (nonce_value : Nonce_hash.t) ⇒ Missing nonce_value);
        Data_encoding.case_value "Forgotten" None (Data_encoding.Tag 2)
          Data_encoding.empty
          (fun (function_parameter : info) ⇒
            match function_parameter with
            | ForgottenSome tt
            | _None
            end)
          (fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Forgotten)
      ].

  Module S.
    Definition get
      : RPC_service.service Updater.rpc_context
        (Updater.rpc_context × Alpha_context.Raw_level.raw_level) unit unit info :=
      RPC_service.get_service (Some "Info about the nonce of a previous block.")
        RPC_query.empty info_encoding
        (RPC_path.op_divcolon
          (RPC_path.op_div (RPC_path.op_div custom_root "context") "nonces")
          Alpha_context.Raw_level.rpc_arg).
  End S.

  Definition register (function_parameter : unit) : unit :=
    let '_ := function_parameter in
    Services_registration.register1 false S.get
      (fun (ctxt : Alpha_context.t) ⇒
        fun (raw_level : Alpha_context.Raw_level.raw_level) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? level := Alpha_context.Level.from_raw ctxt raw_level in
              let function_parameter := Alpha_context.Nonce.get ctxt level in
              match function_parameter with
              | Pervasives.Ok (Storage.Cycle.Revealed nonce_value) ⇒
                return? (Revealed nonce_value)
              |
                Pervasives.Ok
                  (Storage.Cycle.Unrevealed {|
                    Storage.Cycle.unrevealed_nonce.nonce_hash := nonce_hash
                      |}) ⇒ return? (Missing nonce_hash)
              | Pervasives.Error _return? Forgotten
              end).

  Definition get {A : Set}
    (ctxt : RPC_context.simple A) (block : A)
    (level : Alpha_context.Raw_level.raw_level)
    : Error_monad.shell_tzresult info :=
    RPC_context.make_call1 S.get ctxt block level tt tt.
End Nonce.

Module No_available_snapshots.
  Record record : Set := Build {
    min_cycle : int32;
  }.
  Definition with_min_cycle min_cycle (r : record) :=
    Build min_cycle.
End No_available_snapshots.
Definition No_available_snapshots := No_available_snapshots.record.

Init function; without side-effects in Coq
Definition init_module : unit :=
  Error_monad.register_error_kind Error_monad.Permanent "no_available_snapshots"
    "No available snapshots" "No available snapshots"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (min_cycle : int32) ⇒
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "No available snapshots until cycle "
                (CamlinternalFormatBasics.Int32 CamlinternalFormatBasics.Int_d
                  CamlinternalFormatBasics.No_padding
                  CamlinternalFormatBasics.No_precision
                  CamlinternalFormatBasics.End_of_format))
              "No available snapshots until cycle %ld") min_cycle))
    (Data_encoding.obj1
      (Data_encoding.req None None "min_cycle" Data_encoding.int32_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "No_available_snapshots" then
          let '{| No_available_snapshots.min_cycle := min_cycle |} :=
            cast No_available_snapshots payload in
          Some min_cycle
        else None
      end)
    (fun (min_cycle : int32) ⇒
      Build_extensible "No_available_snapshots" No_available_snapshots
        {| No_available_snapshots.min_cycle := min_cycle; |}).

Module Snapshot_index.
  Module S.
    Definition cycle_query : RPC_query.t (option Alpha_context.Cycle.t) :=
      RPC_query.seal
        (RPC_query.op_pipeplus
          (RPC_query.query_value
            (fun (x_value : option Alpha_context.Cycle.t) ⇒ x_value))
          (RPC_query.opt_field None "cycle" Alpha_context.Cycle.rpc_arg
            (fun (cycle : option Alpha_context.Cycle.t) ⇒ cycle))).

    Definition selected_snapshot
      : RPC_service.service Updater.rpc_context Updater.rpc_context
        (option Alpha_context.Cycle.t) unit int :=
      RPC_service.get_service
        (Some
          "Returns the index of the selected snapshot for the current cycle or for the specific `cycle` passed as argument, if any.")
        cycle_query Data_encoding.int31
        (RPC_path.op_div (RPC_path.op_div custom_root "context")
          "selected_snapshot").
  End S.

  Definition register (function_parameter : unit) : unit :=
    let '_ := function_parameter in
    Services_registration.register0 false S.selected_snapshot
      (fun (ctxt : Alpha_context.t) ⇒
        fun (cycle : option Alpha_context.Cycle.t) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            let blocks_per_stake_snapshot :=
              Alpha_context.Constants.blocks_per_stake_snapshot ctxt in
            let blocks_per_cycle :=
              Alpha_context.Constants.blocks_per_cycle ctxt in
            let preserved_cycles :=
              Int32.of_int (Alpha_context.Constants.preserved_cycles ctxt) in
            let cycle :=
              match cycle with
              | None
                (Alpha_context.Level.current ctxt).(Alpha_context.Level.t.cycle)
              | Some cyclecycle
              end in
            if
              (Alpha_context.Cycle.to_int32 cycle) i32
              (Int32.succ preserved_cycles)
            then
              Error_monad.tzfail
                (Build_extensible "No_available_snapshots"
                  No_available_snapshots
                  {|
                    No_available_snapshots.min_cycle := preserved_cycles +i32 2;
                    |})
            else
              let max_snapshot_index :=
                Int32.to_int (blocks_per_cycle /i32 blocks_per_stake_snapshot)
                in
              Alpha_context.Stake_distribution.compute_snapshot_index ctxt cycle
                max_snapshot_index).

  Definition get {A : Set}
    (ctxt : RPC_context.simple A) (block : A)
    (cycle : option Alpha_context.Cycle.t) (function_parameter : unit)
    : Error_monad.shell_tzresult int :=
    let '_ := function_parameter in
    RPC_context.make_call0 S.selected_snapshot ctxt block cycle tt.
End Snapshot_index.

Module Contract := Contract_services.

Module Constants := Constants_services.

Module Delegate := Delegate_services.

Module Voting := Voting_services.

Module Sapling := Sapling_services.

Module Tx_rollup := Tx_rollup_services.

Module Liquidity_baking.
  Module S.
    Definition get_cpmm_address
      : RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
        Contract_hash.t :=
      RPC_service.get_service (Some "Liquidity baking CPMM address")
        RPC_query.empty Alpha_context.Contract.originated_encoding
        (RPC_path.op_div
          (RPC_path.op_div (RPC_path.op_div custom_root "context")
            "liquidity_baking") "cpmm_address").
  End S.

  Definition register (function_parameter : unit) : unit :=
    let '_ := function_parameter in
    Services_registration.register0 false S.get_cpmm_address
      (fun (ctxt : Alpha_context.t) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            Alpha_context.Liquidity_baking.get_cpmm_address ctxt).

  Definition get_cpmm_address {A : Set}
    (ctxt : RPC_context.simple A) (block : A)
    : Error_monad.shell_tzresult Contract_hash.t :=
    RPC_context.make_call0 S.get_cpmm_address ctxt block tt tt.
End Liquidity_baking.

Module Cache.
  Module S.
    Definition cached_contracts
      : RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
        (list (Contract_hash.t × int)) :=
      RPC_service.get_service (Some "Return the list of cached contracts")
        RPC_query.empty
        (Data_encoding.list_value None
          (Data_encoding.tup2 Contract_hash.encoding Data_encoding.int31))
        (RPC_path.op_div
          (RPC_path.op_div
            (RPC_path.op_div (RPC_path.op_div custom_root "context") "cache")
            "contracts") "all").

    Definition contract_cache_size
      : RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
        int :=
      RPC_service.get_service (Some "Return the size of the contract cache")
        RPC_query.empty Data_encoding.int31
        (RPC_path.op_div
          (RPC_path.op_div
            (RPC_path.op_div (RPC_path.op_div custom_root "context") "cache")
            "contracts") "size").

    Definition contract_cache_size_limit
      : RPC_service.service Updater.rpc_context Updater.rpc_context unit unit
        int :=
      RPC_service.get_service
        (Some "Return the size limit of the contract cache") RPC_query.empty
        Data_encoding.int31
        (RPC_path.op_div
          (RPC_path.op_div
            (RPC_path.op_div (RPC_path.op_div custom_root "context") "cache")
            "contracts") "size_limit").

    Definition contract_rank
      : RPC_service.service Updater.rpc_context Updater.rpc_context unit
        Contract_hash.t (option int) :=
      RPC_service.post_service
        (Some
          "Return the number of cached contracts older than the provided contract")
        RPC_query.empty Alpha_context.Contract.originated_encoding
        (Data_encoding.option_value Data_encoding.int31)
        (RPC_path.op_div
          (RPC_path.op_div
            (RPC_path.op_div (RPC_path.op_div custom_root "context") "cache")
            "contracts") "rank").
  End S.

  Definition register (function_parameter : unit) : unit :=
    let '_ := function_parameter in
    let '_ :=
      Services_registration.register0 true S.cached_contracts
        (fun (ctxt : Alpha_context.t) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              Script_cache.entries ctxt) in
    let '_ :=
      Services_registration.register0 false S.contract_cache_size
        (fun (ctxt : Alpha_context.t) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              return? (Script_cache.size_value ctxt)) in
    let '_ :=
      Services_registration.register0 false S.contract_cache_size_limit
        (fun (ctxt : Alpha_context.t) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              return? (Script_cache.size_limit ctxt)) in
    Services_registration.register0 false S.contract_rank
      (fun (ctxt : Alpha_context.t) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          fun (contract : Contract_hash.t) ⇒
            return? (Script_cache.contract_rank ctxt contract)).

  Definition cached_contracts {A : Set}
    (ctxt : RPC_context.simple A) (block : A)
    : Error_monad.shell_tzresult (list (Contract_hash.t × int)) :=
    RPC_context.make_call0 S.cached_contracts ctxt block tt tt.

  Definition contract_cache_size {A : Set}
    (ctxt : RPC_context.simple A) (block : A)
    : Error_monad.shell_tzresult int :=
    RPC_context.make_call0 S.contract_cache_size ctxt block tt tt.

  Definition contract_cache_size_limit {A : Set}
    (ctxt : RPC_context.simple A) (block : A)
    : Error_monad.shell_tzresult int :=
    RPC_context.make_call0 S.contract_cache_size_limit ctxt block tt tt.

  Definition contract_rank {A : Set}
    (ctxt : RPC_context.simple A) (block : A) (contract : Contract_hash.t)
    : Error_monad.shell_tzresult (option int) :=
    RPC_context.make_call0 S.contract_rank ctxt block tt contract.
End Cache.

Definition register (function_parameter : unit) : unit :=
  let '_ := function_parameter in
  let '_ := Contract.register tt in
  let '_ := Constants.register tt in
  let '_ := Delegate.register tt in
  let '_ := Nonce.register tt in
  let '_ := Snapshot_index.register tt in
  let '_ := Voting.register tt in
  let '_ := Sapling.register tt in
  let '_ := Liquidity_baking.register tt in
  let '_ := Cache.register tt in
  Tx_rollup.register tt.