🐆 Tx_rollup_services.v
Translated 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.
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.