Skip to main content

🦏 Sc_rollup_inbox_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.Contract_hash.
Require TezosOfOCaml.Proto_alpha.Gas_limit_repr.
Require TezosOfOCaml.Proto_alpha.Level_repr.
Require TezosOfOCaml.Proto_alpha.Raw_context.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_commitment_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_costs.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_message_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Script_repr.
Require TezosOfOCaml.Proto_alpha.Storage.
Require TezosOfOCaml.Proto_alpha.Storage_sigs.

Module Store := Storage.Sc_rollup.

Definition update_num_and_size_of_messages
  (num_messages : int) (total_messages_size : int)
  (message : Sc_rollup_inbox_message_repr.serialized) : int × int :=
  ((num_messages +i 1), (total_messages_size +i (String.length message))).

Definition inbox_value
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  : M? (Sc_rollup_inbox_repr.V1.t × Raw_context.t) :=
  let? '(ctxt, res) :=
    Store.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.find)
      ctxt rollup in
  match res with
  | None
    Error_monad.Lwt_tzresult_syntax.fail
      (Build_extensible "Sc_rollup_does_not_exist" Sc_rollup_repr.Address.t
        rollup)
  | Some inbox_valuereturn? (inbox_value, ctxt)
  end.

Definition assert_inbox_nb_messages_in_commitment_period
  (ctxt : Raw_context.t) (inbox_value : Sc_rollup_inbox_repr.t)
  (extra_messages : int) : M? unit :=
  let nb_messages_in_commitment_period :=
    (Sc_rollup_inbox_repr.number_of_messages_during_commitment_period
      inbox_value) +i64 (Int64.of_int extra_messages) in
  let limit :=
    Int64.of_int
      (Constants_storage.sc_rollup_max_number_of_messages_per_commitment_period
        ctxt) in
  Error_monad.fail_when (nb_messages_in_commitment_period >i64 limit)
    (Build_extensible
      "Sc_rollup_max_number_of_messages_reached_for_commitment_period" unit tt).

Definition add_messages
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (messages : list Sc_rollup_inbox_message_repr.serialized)
  : M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
  let '{| Level_repr.t.level := level |} := Raw_context.current_level ctxt in
  let commitment_period :=
    Int32.of_int (Constants_storage.sc_rollup_commitment_period_in_blocks ctxt)
    in
  let? '(inbox_value, ctxt) := inbox_value ctxt rollup in
  let? '(num_messages, total_messages_size, ctxt) :=
    List.fold_left_es
      (fun (function_parameter : int × int × Raw_context.t) ⇒
        let '(num_messages, total_messages_size, ctxt) := function_parameter in
        fun (message : Sc_rollup_inbox_message_repr.serialized) ⇒
          let? ctxt :=
            Raw_context.consume_gas ctxt
              Sc_rollup_costs.Constants.cost_update_num_and_size_of_messages in
          let '(num_messages, total_messages_size) :=
            update_num_and_size_of_messages num_messages total_messages_size
              message in
          return? (num_messages, total_messages_size, ctxt)) (0, 0, ctxt)
      messages in
  let? inbox_value :=
    Sc_rollup_inbox_repr.refresh_commitment_period commitment_period level
      inbox_value in
  let? '_ :=
    assert_inbox_nb_messages_in_commitment_period ctxt inbox_value num_messages
    in
  let inbox_level := Sc_rollup_inbox_repr.inbox_level inbox_value in
  let? '(ctxt, genesis_info) :=
    Storage.Sc_rollup.Genesis_info.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.get)
      ctxt rollup in
  let origination_level :=
    genesis_info.(Sc_rollup_commitment_repr.genesis_info.level) in
  let levels :=
    (Raw_level_repr.to_int32 inbox_level) -i32
    (Raw_level_repr.to_int32 origination_level) in
  let? '(current_messages, ctxt) :=
    Raw_context.Sc_rollup_in_memory_inbox.current_messages ctxt rollup in
  let cost_add_serialized_messages :=
    Sc_rollup_costs.cost_add_serialized_messages num_messages
      total_messages_size levels in
  let? ctxt := Raw_context.consume_gas ctxt cost_add_serialized_messages in
  let? '(current_messages, inbox_value) :=
    Sc_rollup_inbox_repr.add_messages_no_history (Raw_context.recover ctxt)
      inbox_value level messages current_messages in
  let? ctxt :=
    Raw_context.Sc_rollup_in_memory_inbox.set_current_messages ctxt rollup
      current_messages in
  let? '(ctxt, size_value) :=
    Store.Inbox.(Storage_sigs.Non_iterable_indexed_carbonated_data_storage.update)
      ctxt rollup inbox_value in
  return? (inbox_value, (Z.of_int size_value), ctxt).

Definition serialize_external_messages
  (ctxt : Raw_context.t) (external_messages : list string)
  : M? (Raw_context.t × list Sc_rollup_inbox_message_repr.serialized) :=
  List.fold_left_map_e
    (fun (ctxt : Raw_context.t) ⇒
      fun (message : string) ⇒
        let? ctxt :=
          let bytes_len := String.length message in
          Raw_context.consume_gas ctxt
            (Sc_rollup_costs.cost_serialize_external_inbox_message bytes_len) in
        let? serialized_message :=
          Sc_rollup_inbox_message_repr.serialize
            (Sc_rollup_inbox_message_repr.External message) in
        return? (ctxt, serialized_message)) ctxt external_messages.

Definition serialize_internal_message
  (ctxt : Raw_context.t) (payload : Script_repr.expr) (sender : Contract_hash.t)
  (source : Signature.public_key_hash)
  : M? (Sc_rollup_inbox_message_repr.serialized × Raw_context.t) :=
  let internal_message :=
    {| Sc_rollup_inbox_message_repr.internal_inbox_message.payload := payload;
      Sc_rollup_inbox_message_repr.internal_inbox_message.sender := sender;
      Sc_rollup_inbox_message_repr.internal_inbox_message.source := source; |}
    in
  let? ctxt :=
    Raw_context.consume_gas ctxt
      (Sc_rollup_costs.cost_serialize_internal_inbox_message internal_message)
    in
  let? message :=
    Sc_rollup_inbox_message_repr.serialize
      (Sc_rollup_inbox_message_repr.Internal internal_message) in
  return? (message, ctxt).

Definition add_external_messages
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (external_messages : list string)
  : M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
  let? '(ctxt, messages) := serialize_external_messages ctxt external_messages
    in
  add_messages ctxt rollup messages.

Definition add_internal_message
  (ctxt : Raw_context.t) (rollup : Sc_rollup_repr.Address.t)
  (payload : Script_repr.expr) (sender : Contract_hash.t)
  (source : Signature.public_key_hash)
  : M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
  let? '(message, ctxt) := serialize_internal_message ctxt payload sender source
    in
  add_messages ctxt rollup [ message ].