Skip to main content

🐆 Tx_rollup_state_storage.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.V7.
Require TezosOfOCaml.Proto_alpha.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_state_repr.

Definition init_value (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  : M? Raw_context.t :=
  let? '(ctxt, already_exists) :=
    Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
      ctxt tx_rollup in
  let? '_ :=
    Error_monad.fail_when already_exists
      (Build_extensible "Tx_rollup_already_exists" Tx_rollup_repr.t tx_rollup)
    in
  let pre_allocated_storage :=
    Z.of_int (Constants_storage.tx_rollup_origination_size ctxt) in
  Error_monad.op_gtpipeeqquestion
    (Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.init_value)
      ctxt tx_rollup (Tx_rollup_state_repr.initial_state pre_allocated_storage))
    Pervasives.fst.

Definition find
  : Raw_context.t Tx_rollup_repr.t
  M? (Raw_context.t × option Tx_rollup_state_repr.t) :=
  Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find).

Definition get (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  : M? (Raw_context.t × Tx_rollup_state_repr.t) :=
  let? '(ctxt, state_value) := find ctxt tx_rollup in
  match state_value with
  | Some state_valuereturn? (ctxt, state_value)
  | None
    Error_monad.fail
      (Build_extensible "Tx_rollup_does_not_exist" Tx_rollup_repr.t tx_rollup)
  end.

Definition assert_exist (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  : M? Raw_context.t :=
  let? '(ctxt, tx_rollup_exists) :=
    Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.mem)
      ctxt tx_rollup in
  let? '_ :=
    Error_monad.fail_unless tx_rollup_exists
      (Build_extensible "Tx_rollup_does_not_exist" Tx_rollup_repr.t tx_rollup)
    in
  return? ctxt.

Definition update
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (t_value : Tx_rollup_state_repr.t) : M? Raw_context.t :=
  let? '(ctxt, _) :=
    Storage.Tx_rollup.State.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
      ctxt tx_rollup t_value in
  return? ctxt.