🦏 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.V8.
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.Sc_rollup_costs.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_inbox_merkelized_payload_hashes_repr.
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 get_inbox (ctxt : Raw_context.t)
  : M? (Sc_rollup_inbox_repr.V1.t × Raw_context.t) :=
  let? inbox_value := Store.Inbox.(Storage_sigs.Single_data_storage.get) ctxt in
  return? (inbox_value, ctxt).

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_aux
  (ctxt : Raw_context.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? '(inbox_value, ctxt) := get_inbox ctxt 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 cost_add_serialized_messages :=
    Sc_rollup_costs.cost_add_serialized_messages num_messages
      total_messages_size 0 in
  let? ctxt := Raw_context.consume_gas ctxt cost_add_serialized_messages in
  let current_messages :=
    Raw_context.Sc_rollup_in_memory_inbox.current_messages ctxt in
  let? '(current_messages, inbox_value) :=
    Sc_rollup_inbox_repr.add_messages_no_history inbox_value level messages
      current_messages in
  let ctxt :=
    Raw_context.Sc_rollup_in_memory_inbox.set_current_messages ctxt
      current_messages in
  let? ctxt :=
    Store.Inbox.(Storage_sigs.Single_data_storage.update) ctxt inbox_value in
  return? (inbox_value, Z.zero, 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)
  (internal_message : Sc_rollup_inbox_message_repr.internal_inbox_message)
  : M? (Sc_rollup_inbox_message_repr.serialized × Raw_context.t) :=
  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) (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_aux ctxt messages.

Definition add_internal_message
  (ctxt : Raw_context.t)
  (internal_message : Sc_rollup_inbox_message_repr.internal_inbox_message)
  : M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
  let? '(message, ctxt) := serialize_internal_message ctxt internal_message in
  add_messages_aux ctxt [ message ].

Definition add_deposit
  (ctxt : Raw_context.t) (payload : Script_repr.expr) (sender : Contract_hash.t)
  (source : Signature.public_key_hash) (destination : Sc_rollup_repr.Address.t)
  : M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
  let internal_message :=
    Sc_rollup_inbox_message_repr.Transfer
      {|
        Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.payload :=
          payload;
        Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.sender :=
          sender;
        Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.source :=
          source;
        Sc_rollup_inbox_message_repr.internal_inbox_message.Transfer.destination
          := destination; |} in
  add_internal_message ctxt internal_message.

Definition add_start_of_level (ctxt : Raw_context.t)
  : M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
  add_internal_message ctxt Sc_rollup_inbox_message_repr.Start_of_level.

Definition add_end_of_level (ctxt : Raw_context.t)
  : M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
  add_internal_message ctxt Sc_rollup_inbox_message_repr.End_of_level.

Definition add_info_per_level
  (ctxt : Raw_context.t) (timestamp : Time.t) (predecessor : Block_hash.t)
  : M? (Sc_rollup_inbox_repr.t × Z.t × Raw_context.t) :=
  add_internal_message ctxt
    (Sc_rollup_inbox_message_repr.Info_per_level
      {|
        Sc_rollup_inbox_message_repr.internal_inbox_message.Info_per_level.timestamp
          := timestamp;
        Sc_rollup_inbox_message_repr.internal_inbox_message.Info_per_level.predecessor
          := predecessor; |}).

Definition init_value
  (timestamp : Time.t) (predecessor : Block_hash.t) (ctxt : Raw_context.t)
  : M? Raw_context.t :=
  let '{| Level_repr.t.level := level |} := Raw_context.current_level ctxt in
  let inbox_value := Sc_rollup_inbox_repr.empty level in
  let? ctxt :=
    Store.Inbox.(Storage_sigs.Single_data_storage.init_value) ctxt inbox_value
    in
  let? '(_inbox, _diff, ctxt) := add_start_of_level ctxt in
  let? '(_inbox, _diff, ctxt) := add_info_per_level ctxt timestamp predecessor
    in
  let? '(_inbox, _diff, ctxt) := add_end_of_level ctxt in
  return? ctxt.