🐆 Tx_rollup_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.Services_registration.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Definition custom_root : RPC_path.context RPC_context.t :=
  RPC_path.op_div (RPC_path.op_div RPC_path.open_root "context") "tx_rollup".

Module S.
  Definition state_value
    : RPC_service.service RPC_context.t
      (RPC_context.t × Alpha_context.Tx_rollup.t) unit unit
      Alpha_context.Tx_rollup_state.t :=
    RPC_service.get_service (Some "Access the state of a rollup.")
      RPC_query.empty Alpha_context.Tx_rollup_state.encoding
      (RPC_path.op_div
        (RPC_path.op_divcolon custom_root Alpha_context.Tx_rollup.rpc_arg)
        "state").

  Definition inbox_value
    : RPC_service.service RPC_context.t
      ((RPC_context.t × Alpha_context.Tx_rollup.t) ×
        Alpha_context.Tx_rollup_level.level) unit unit
      (option Alpha_context.Tx_rollup_inbox.t) :=
    RPC_service.get_service (Some "Get the inbox of a transaction rollup")
      RPC_query.empty
      (Data_encoding.option_value Alpha_context.Tx_rollup_inbox.encoding)
      (RPC_path.op_divcolon
        (RPC_path.op_div
          (RPC_path.op_divcolon custom_root Alpha_context.Tx_rollup.rpc_arg)
          "inbox") Alpha_context.Tx_rollup_level.rpc_arg).

  Definition commitment
    : RPC_service.service RPC_context.t
      ((RPC_context.t × Alpha_context.Tx_rollup.t) ×
        Alpha_context.Tx_rollup_level.level) unit unit
      (option
        Alpha_context.Tx_rollup_commitment.Submitted_commitment.(Storage_sigs.VALUE.t)) :=
    RPC_service.get_service (Some "Return the commitment for a level, if any")
      RPC_query.empty
      (Data_encoding.option_value
        Alpha_context.Tx_rollup_commitment.Submitted_commitment.(Storage_sigs.VALUE.encoding))
      (RPC_path.op_divcolon
        (RPC_path.op_div
          (RPC_path.op_divcolon custom_root Alpha_context.Tx_rollup.rpc_arg)
          "commitment") Alpha_context.Tx_rollup_level.rpc_arg).

  Definition pending_bonded_commitments
    : RPC_service.service RPC_context.t
      ((RPC_context.t × Alpha_context.Tx_rollup.t) × Signature.public_key_hash)
      unit unit int32 :=
    RPC_service.get_service
      (Some "Get the number of pending bonded commitments for a pkh on a rollup")
      RPC_query.empty Data_encoding.int32_value
      (RPC_path.op_divcolon
        (RPC_path.op_div
          (RPC_path.op_divcolon custom_root Alpha_context.Tx_rollup.rpc_arg)
          "pending_bonded_commitments")
        Signature.Public_key_hash.(S.SIGNATURE_PUBLIC_KEY_HASH.rpc_arg)).
End S.

Definition register (function_parameter : unit) : unit :=
  let '_ := function_parameter in
  let '_ :=
    Services_registration.opt_register1 false S.state_value
      (fun (ctxt : Alpha_context.t) ⇒
        fun (tx_rollup : Alpha_context.Tx_rollup.t) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              Error_monad.op_gtpipeeqquestion
                (Alpha_context.Tx_rollup_state.find ctxt tx_rollup)
                Pervasives.snd) in
  let '_ :=
    Services_registration.register2 false S.inbox_value
      (fun (ctxt : Alpha_context.t) ⇒
        fun (tx_rollup : Alpha_context.Tx_rollup.t) ⇒
          fun (level : Alpha_context.Tx_rollup_level.level) ⇒
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                Error_monad.op_gtpipeeqquestion
                  (Alpha_context.Tx_rollup_inbox.find ctxt level tx_rollup)
                  Pervasives.snd) in
  let '_ :=
    Services_registration.register2 false S.commitment
      (fun (ctxt : Alpha_context.t) ⇒
        fun (tx_rollup : Alpha_context.Tx_rollup.t) ⇒
          fun (level : Alpha_context.Tx_rollup_level.level) ⇒
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              fun (function_parameter : unit) ⇒
                let '_ := function_parameter in
                let? '(ctxt, state_value) :=
                  Alpha_context.Tx_rollup_state.get ctxt tx_rollup in
                let? '(_, commitment) :=
                  Alpha_context.Tx_rollup_commitment.find ctxt tx_rollup
                    state_value level in
                return? commitment) in
  Services_registration.register2 false S.pending_bonded_commitments
    (fun (ctxt : Alpha_context.t) ⇒
      fun (tx_rollup : Alpha_context.Tx_rollup.t) ⇒
        fun (pkh : Signature.public_key_hash) ⇒
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              let? '(_, count) :=
                Alpha_context.Tx_rollup_commitment.pending_bonded_commitments
                  ctxt tx_rollup pkh in
              return? (Int32.of_int count)).

Definition state_value {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (tx_rollup : Alpha_context.Tx_rollup.t)
  : Error_monad.shell_tzresult Alpha_context.Tx_rollup_state.t :=
  RPC_context.make_call1 S.state_value ctxt block tx_rollup tt tt.

Definition inbox_value {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (tx_rollup : Alpha_context.Tx_rollup.t)
  (level : Alpha_context.Tx_rollup_level.level)
  : Error_monad.shell_tzresult (option Alpha_context.Tx_rollup_inbox.t) :=
  RPC_context.make_call2 S.inbox_value ctxt block tx_rollup level tt tt.

Definition commitment {A : Set}
  (ctxt : RPC_context.simple A) (block : A)
  (tx_rollup : Alpha_context.Tx_rollup.t)
  (level : Alpha_context.Tx_rollup_level.level)
  : Error_monad.shell_tzresult
    (option
      Alpha_context.Tx_rollup_commitment.Submitted_commitment.(Storage_sigs.VALUE.t)) :=
  RPC_context.make_call2 S.commitment ctxt block tx_rollup level tt tt.