🦏 Sc_rollup_outbox_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.Constants_storage.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Definition level_index (ctxt : Raw_context.t) (level : Raw_level_repr.raw_level)
  : int32 :=
  let max_active_levels :=
    Constants_storage.sc_rollup_max_active_outbox_levels ctxt in
  Int32.rem (Raw_level_repr.to_int32 level) max_active_levels.

Definition record_applied_message
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.t)
  (level : Raw_level_repr.raw_level) (message_index : int)
  : M? (Z.t × Raw_context.t) :=
  let? '_ :=
    let max_outbox_messages_per_level :=
      Constants_storage.sc_rollup_max_outbox_messages_per_level ctxt in
    Error_monad.error_unless
      ((0 ≤i message_index) && (message_index <i max_outbox_messages_per_level))
      (Build_extensible "Sc_rollup_invalid_outbox_message_index" unit tt) in
  let level_index := level_index ctxt level in
  let? '(ctxt, level_and_bitset_opt) :=
    Storage.Sc_rollup.Applied_outbox_messages.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      (ctxt, rollup) level_index in
  let? '(bitset, ctxt) :=
    let? '(bitset, ctxt) :=
      match
        (level_and_bitset_opt,
          match level_and_bitset_opt with
          | Some (existing_level, bitset) ⇒
            Raw_level_repr.op_eq existing_level level
          | _ ⇒ false
          end,
          match level_and_bitset_opt with
          | Some (existing_level, _bitset) ⇒
            Raw_level_repr.op_lt level existing_level
          | _ ⇒ false
          end) with
      | (Some (existing_level, bitset), true, _) ⇒
        let? already_applied := Bitset.mem bitset message_index in
        let? '_ :=
          Error_monad.error_when already_applied
            (Build_extensible "Sc_rollup_outbox_message_already_applied" unit tt)
          in
        return? (bitset, ctxt)
      | (Some (existing_level, _bitset), _, true) ⇒
        Error_monad.Result_syntax.tzfail
          (Build_extensible "Sc_rollup_outbox_level_expired" unit tt)
      | ((Some _ | None), _, _) ⇒ return? (Bitset.empty, ctxt)
      end in
    let? bitset := Bitset.add bitset message_index in
    return? (bitset, ctxt) in
  Error_monad.Lwt_result_syntax.op_letplus
    (Storage.Sc_rollup.Applied_outbox_messages.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.add)
      (ctxt, rollup) level_index (level, bitset))
    (fun function_parameter ⇒
      let '(ctxt, size_diff, _is_new) := function_parameter in
      ((Z.of_int size_diff), ctxt)).