🐆 Tx_rollup_reveal_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.V8.
Require TezosOfOCaml.Proto_alpha.Bitset.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_level_repr.
Require TezosOfOCaml.Proto_alpha.Tx_rollup_repr.

Definition record
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (level : Tx_rollup_level_repr.t) (message_position : int)
  : M? Raw_context.t :=
  let? '(ctxt, revealed_withdrawals_opt) :=
    Storage.Tx_rollup.Revealed_withdrawals.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, tx_rollup) level in
  let? revealed_withdrawals :=
    Bitset.add (Option.value_value revealed_withdrawals_opt Bitset.empty)
      message_position in
  let? '(ctxt, _new_size, _is_new) :=
    Storage.Tx_rollup.Revealed_withdrawals.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
      (ctxt, tx_rollup) level revealed_withdrawals in
  return? ctxt.

Definition mem
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (level : Tx_rollup_level_repr.t) (message_position : int)
  : M? (Raw_context.t × bool) :=
  let? '(ctxt, revealed_withdrawals_opt) :=
    Storage.Tx_rollup.Revealed_withdrawals.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, tx_rollup) level in
  match revealed_withdrawals_opt with
  | Some field_value ⇒
    let? res := Bitset.mem field_value message_position in
    return? (ctxt, res)
  | None ⇒ return? (ctxt, false)
  end.

Definition remove
  (ctxt : Raw_context.t) (tx_rollup : Tx_rollup_repr.t)
  (level : Tx_rollup_level_repr.t) : M? Raw_context.t :=
  let? '(ctxt, _freed_size, _existed) :=
    Storage.Tx_rollup.Revealed_withdrawals.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.remove)
      (ctxt, tx_rollup) level in
  return? ctxt.