Skip to main content

🦏 Sc_rollup_inbox_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
A Merkelized inbox represents a list of messages. This list is decomposed into sublists of messages, one for each Tezos level greater than the level where SCORU is activated.
This module is designed to:
1. provide a space-efficient representation for proofs of inbox inclusions (only for inboxes obtained at the end of block validation) ;
2. offer an efficient function to add a new batch of messages in the inbox at the current level.
To solve (1), we use a proof tree H which is implemented by a merkelized skip list allowing for compact inclusion proofs (See {!skip_list_repr.ml}).
To solve (2), we maintain a separate proof tree C witnessing the contents of messages of the current level also implemented by a merkelized skip list for the same reason.
The protocol maintains the hashes of the head of H and C.
The rollup node needs to maintain a full representation for C and a partial representation for H back to the level of the LCC.
Init function; without side-effects in Coq
Definition init_module_repr : unit :=
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "sc_rollup_inbox.invalid_level_add_messages"
      "Internal error: Trying to add a message to an inbox from the past"
      "An inbox can only accept messages for its current level or for the next levels."
      None
      (Data_encoding.obj1
        (Data_encoding.req None None "level" Raw_level_repr.encoding))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Invalid_level_add_messages" then
            let level := cast Raw_level_repr.t payload in
            Some level
          else None
        end)
      (fun (level : Raw_level_repr.raw_level) ⇒
        Build_extensible "Invalid_level_add_messages" Raw_level_repr.raw_level
          level) in
  let '_ :=
    Error_monad.register_error_kind Error_monad.Permanent
      "sc_rollup_inbox.inbox_proof_error"
      "Internal error: error occurred during proof production or validation"
      "An inbox proof error."
      (Some
        (fun (ppf : Format.formatter) ⇒
          fun (e_value : string) ⇒
            Format.fprintf ppf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal "Inbox proof error: "
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    CamlinternalFormatBasics.End_of_format))
                "Inbox proof error: %s") e_value))
      (Data_encoding.obj1
        (Data_encoding.req None None "error" Data_encoding.string_value))
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Inbox_proof_error" then
            let e_value := cast string payload in
            Some e_value
          else None
        end)
      (fun (e_value : string) ⇒
        Build_extensible "Inbox_proof_error" string e_value) in
  Error_monad.register_error_kind Error_monad.Permanent
    "sc_rollup_inbox.add_zero_messages"
    "Internal error: trying to add zero messages"
    "Message adding functions must be called with a positive number of messages"
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Tried to add zero messages"
                CamlinternalFormatBasics.End_of_format)
              "Tried to add zero messages"))) Data_encoding.empty
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Tried_to_add_zero_messages" then
          Some tt
        else None
      end)
    (fun (function_parameter : unit) ⇒
      let '_ := function_parameter in
      Build_extensible "Tried_to_add_zero_messages" unit tt).

Definition Int64_map :=
  Map.Make
    {|
      Compare.COMPARABLE.compare := Int64.compare
    |}.

Definition hash_prefix : string :=
  String.String "003"
    (String.String "250"
      (String.String "174" (String.String "238" (String.String "208" "")))).

Module Hash.
  Definition prefix : string := "scib1".

  Definition encoded_size : int := 55.

  Definition H :=
    Blake2B.Make
      {|
        Blake2B.Register.register_encoding _ := Base58.register_encoding
      |}
      (let name := "inbox_hash" in
      let title := "The hash of an inbox of a smart contract rollup" in
      let b58check_prefix := hash_prefix in
      let size_value {A : Set} : option A :=
        None in
      {|
        Blake2B.PrefixedName.name := name;
        Blake2B.PrefixedName.title := title;
        Blake2B.PrefixedName.size_value := size_value;
        Blake2B.PrefixedName.b58check_prefix := b58check_prefix
      |}).

Inclusion of the module [H]
  Definition t := H.(S.HASH.t).

  Definition name := H.(S.HASH.name).

  Definition title := H.(S.HASH.title).

  Definition pp := H.(S.HASH.pp).

  Definition pp_short := H.(S.HASH.pp_short).

  Definition op_eq := H.(S.HASH.op_eq).

  Definition op_ltgt := H.(S.HASH.op_ltgt).

  Definition op_lt := H.(S.HASH.op_lt).

  Definition op_lteq := H.(S.HASH.op_lteq).

  Definition op_gteq := H.(S.HASH.op_gteq).

  Definition op_gt := H.(S.HASH.op_gt).

  Definition compare := H.(S.HASH.compare).

  Definition equal := H.(S.HASH.equal).

  Definition max := H.(S.HASH.max).

  Definition min := H.(S.HASH.min).

  Definition hash_bytes := H.(S.HASH.hash_bytes).

  Definition hash_string := H.(S.HASH.hash_string).

  Definition zero := H.(S.HASH.zero).

  Definition size_value := H.(S.HASH.size_value).

  Definition to_bytes := H.(S.HASH.to_bytes).

  Definition of_bytes_opt := H.(S.HASH.of_bytes_opt).

  Definition of_bytes_exn := H.(S.HASH.of_bytes_exn).

  Definition to_b58check := H.(S.HASH.to_b58check).

  Definition to_short_b58check := H.(S.HASH.to_short_b58check).

  Definition of_b58check_exn := H.(S.HASH.of_b58check_exn).

  Definition of_b58check_opt := H.(S.HASH.of_b58check_opt).

  Definition b58check_encoding := H.(S.HASH.b58check_encoding).

  Definition encoding := H.(S.HASH.encoding).

  Definition rpc_arg := H.(S.HASH.rpc_arg).

Init function; without side-effects in Coq
Inclusion of the module [Path_encoding_Make_hex_include]
  Definition to_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.to_path).

  Definition of_path :=
    Path_encoding_Make_hex_include.(Path_encoding.S.of_path).

  Definition path_length :=
    Path_encoding_Make_hex_include.(Path_encoding.S.path_length).
End Hash.

Module Skip_list_parameters.
  Definition basis : int := 2.

  (* Skip_list_parameters *)
  Definition module :=
    {|
      Skip_list_repr.S_Parameters.basis := basis
    |}.
End Skip_list_parameters.
Definition Skip_list_parameters := Skip_list_parameters.module.

Definition Skip_list : Skip_list_repr.S (cell := _) :=
  Skip_list_repr.Make Skip_list_parameters.

Module V1.
  Module level_proof.
    Record record : Set := Build {
      hash : Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t;
      level : Raw_level_repr.t;
    }.
    Definition with_hash hash (r : record) :=
      Build hash r.(level).
    Definition with_level level (r : record) :=
      Build r.(hash) level.
  End level_proof.
  Definition level_proof := level_proof.record.

  Definition level_proof_encoding : Data_encoding.encoding level_proof :=
    Data_encoding.conv
      (fun (function_parameter : level_proof) ⇒
        let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
          function_parameter in
        (hash_value, level))
      (fun (function_parameter :
        Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t × Raw_level_repr.t)
        ⇒
        let '(hash_value, level) := function_parameter in
        {| level_proof.hash := hash_value; level_proof.level := level; |}) None
      (Data_encoding.obj2
        (Data_encoding.req None None "hash"
          Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.encoding)
        (Data_encoding.req None None "level" Raw_level_repr.encoding)).

  Definition equal_level_proof (function_parameter : level_proof)
    : level_proof bool :=
    let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
      function_parameter in
    fun (level_proof_2 : level_proof) ⇒
      (Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.equal hash_value
        level_proof_2.(level_proof.hash)) &&
      (Raw_level_repr.equal level level_proof_2.(level_proof.level)).

  Definition history_proof : Set :=
    Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t.

  Definition hash_history_proof
    (cell_value : Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t)
    : Hash.t :=
    let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
      Skip_list.(Skip_list_repr.S.content) cell_value in
    let back_pointers_hashes :=
      Skip_list.(Skip_list_repr.S.back_pointers) cell_value in
    Hash.hash_bytes None
      (cons
        (Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.to_bytes hash_value)
        (cons
          (Bytes.of_string (Int32.to_string (Raw_level_repr.to_int32 level)))
          (List.map Hash.to_bytes back_pointers_hashes))).

  Definition equal_history_proof
    : Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t
    Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t bool :=
    Skip_list.(Skip_list_repr.S.equal) Hash.equal equal_level_proof.

  Definition history_proof_encoding : Data_encoding.t history_proof :=
    Skip_list.(Skip_list_repr.S.encoding) Hash.encoding level_proof_encoding.

  Definition pp_level_proof
    (fmt : Format.formatter) (function_parameter : level_proof) : unit :=
    let '{| level_proof.hash := hash_value; level_proof.level := level |} :=
      function_parameter in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "hash: "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.Formatting_lit
              (CamlinternalFormatBasics.Break "@," 0 0)
              (CamlinternalFormatBasics.String_literal "level: "
                (CamlinternalFormatBasics.Alpha
                  CamlinternalFormatBasics.End_of_format)))))
        "hash: %a@,level: %a")
      Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.pp hash_value
      Raw_level_repr.pp level.

  Definition pp_history_proof
    (fmt : Format.formatter)
    (history_proof : Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t)
    : unit :=
    Skip_list.(Skip_list_repr.S.pp) Hash.pp pp_level_proof fmt history_proof.

Construct an inbox [history] with a given [capacity]. If you are running a rollup node, [capacity] needs to be large enough to remember any levels for which you may need to produce proofs.
  Definition History :
    Bounded_history_repr.S (t := _) (key := Hash.t) (value := history_proof) :=
    Bounded_history_repr.Make
      (let name := "inbox_history" in
      let _sig_NAME := tt in
      {|
        Bounded_history_repr.NAME.name := name;
        Bounded_history_repr.NAME._sig_NAME := _sig_NAME
      |})
      (let t : Set := Hash.t in
      let compare := Hash.compare in
      let pp := Hash.pp in
      let encoding := Hash.encoding in
      let _sig_KEY := tt in
      {|
        Bounded_history_repr.KEY.compare := compare;
        Bounded_history_repr.KEY.pp := pp;
        Bounded_history_repr.KEY.encoding := encoding;
        Bounded_history_repr.KEY._sig_KEY := _sig_KEY
      |})
      (let t : Set := history_proof in
      let pp := pp_history_proof in
      let equal := equal_history_proof in
      let encoding := history_proof_encoding in
      {|
        Bounded_history_repr.VALUE.equal := equal;
        Bounded_history_repr.VALUE.pp := pp;
        Bounded_history_repr.VALUE.encoding := encoding
      |}).

  Module t.
    Record record : Set := Build {
      level : Raw_level_repr.t;
      nb_messages_in_commitment_period : int64;
      current_level_proof : unit level_proof;
      old_levels_messages : history_proof;
    }.
    Definition with_level level (r : record) :=
      Build level r.(nb_messages_in_commitment_period) r.(current_level_proof)
        r.(old_levels_messages).
    Definition with_nb_messages_in_commitment_period
      nb_messages_in_commitment_period (r : record) :=
      Build r.(level) nb_messages_in_commitment_period r.(current_level_proof)
        r.(old_levels_messages).
    Definition with_current_level_proof current_level_proof (r : record) :=
      Build r.(level) r.(nb_messages_in_commitment_period) current_level_proof
        r.(old_levels_messages).
    Definition with_old_levels_messages old_levels_messages (r : record) :=
      Build r.(level) r.(nb_messages_in_commitment_period)
        r.(current_level_proof) old_levels_messages.
  End t.
  Definition t := t.record.

  Definition equal (inbox1 : t) (inbox2 : t) : bool :=
    let '{|
      t.level := level;
        t.nb_messages_in_commitment_period := nb_messages_in_commitment_period;
        t.current_level_proof := current_level_proof;
        t.old_levels_messages := old_levels_messages
        |} := inbox1 in
    (Raw_level_repr.equal level inbox2.(t.level)) &&
    ((Compare.Int64.(Compare.S.equal) nb_messages_in_commitment_period
      inbox2.(t.nb_messages_in_commitment_period)) &&
    ((equal_level_proof (current_level_proof tt)
      (inbox2.(t.current_level_proof) tt)) &&
    (equal_history_proof old_levels_messages inbox2.(t.old_levels_messages)))).

  Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
    let '{|
      t.level := level;
        t.nb_messages_in_commitment_period := nb_messages_in_commitment_period;
        t.current_level_proof := current_level_proof;
        t.old_levels_messages := old_levels_messages
        |} := function_parameter in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "<hov 2>"
                CamlinternalFormatBasics.End_of_format) "<hov 2>"))
          (CamlinternalFormatBasics.String_literal "{ level = "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.Formatting_lit
                (CamlinternalFormatBasics.Break "@;" 1 0)
                (CamlinternalFormatBasics.String_literal
                  "current messages hash = "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Formatting_lit
                      (CamlinternalFormatBasics.Break "@;" 1 0)
                      (CamlinternalFormatBasics.String_literal
                        "nb_messages_in_commitment_period = "
                        (CamlinternalFormatBasics.String
                          CamlinternalFormatBasics.No_padding
                          (CamlinternalFormatBasics.Formatting_lit
                            (CamlinternalFormatBasics.Break "@;" 1 0)
                            (CamlinternalFormatBasics.String_literal
                              "old_levels_messages = "
                              (CamlinternalFormatBasics.Alpha
                                (CamlinternalFormatBasics.Formatting_lit
                                  (CamlinternalFormatBasics.Break "@;" 1 0)
                                  (CamlinternalFormatBasics.Char_literal
                                    "}" % char
                                    (CamlinternalFormatBasics.Formatting_lit
                                      CamlinternalFormatBasics.Close_box
                                      CamlinternalFormatBasics.End_of_format)))))))))))))))
        "@[<hov 2>{ level = %a@;current messages hash = %a@;nb_messages_in_commitment_period = %s@;old_levels_messages = %a@;}@]")
      Raw_level_repr.pp level pp_level_proof (current_level_proof tt)
      (Int64.to_string nb_messages_in_commitment_period) pp_history_proof
      old_levels_messages.

  Definition inbox_level (inbox_value : t) : Raw_level_repr.t :=
    inbox_value.(t.level).

  Definition old_levels_messages (inbox_value : t) : history_proof :=
    inbox_value.(t.old_levels_messages).

  Definition current_level_proof (inbox_value : t) : level_proof :=
    inbox_value.(t.current_level_proof) tt.

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{|
          t.level := level;
            t.nb_messages_in_commitment_period :=
              nb_messages_in_commitment_period;
            t.current_level_proof := current_level_proof;
            t.old_levels_messages := old_levels_messages
            |} := function_parameter in
        (nb_messages_in_commitment_period, level, (current_level_proof tt),
          old_levels_messages))
      (fun (function_parameter :
        int64 × Raw_level_repr.t × level_proof × history_proof) ⇒
        let
          '(nb_messages_in_commitment_period, level, current_level_proof,
            old_levels_messages) := function_parameter in
        {| t.level := level;
          t.nb_messages_in_commitment_period :=
            nb_messages_in_commitment_period;
          t.current_level_proof :=
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              current_level_proof; t.old_levels_messages := old_levels_messages;
          |}) None
      (Data_encoding.obj4
        (Data_encoding.req None None "nb_messages_in_commitment_period"
          Data_encoding.int64_value)
        (Data_encoding.req None None "level" Raw_level_repr.encoding)
        (Data_encoding.req None None "current_level_proof" level_proof_encoding)
        (Data_encoding.req None None "old_levels_messages"
          history_proof_encoding)).

  Definition number_of_messages_during_commitment_period (inbox_value : t)
    : int64 := inbox_value.(t.nb_messages_in_commitment_period).
End V1.

Inductive versioned : Set :=
| V1 : V1.t versioned.

Definition versioned_encoding : Data_encoding.encoding versioned :=
  Data_encoding.union None
    [
      Data_encoding.case_value "V1" None (Data_encoding.Tag 0) V1.encoding
        (fun (function_parameter : versioned) ⇒
          let 'V1 inbox_value := function_parameter in
          Some inbox_value) (fun (inbox_value : V1.t) ⇒ V1 inbox_value)
    ].

Include V1.

Definition of_versioned (function_parameter : versioned) : V1.t :=
  let 'V1 inbox_value := function_parameter in
  inbox_value.

Definition to_versioned (inbox_value : V1.t) : versioned := V1 inbox_value.

Definition serialized_proof : Set := string.

Definition serialized_proof_encoding : Data_encoding.encoding string :=
  Data_encoding.string' None Data_encoding.Hex.

Module level_tree_proof.
  Record record : Set := Build {
    proof : Sc_rollup_inbox_merkelized_payload_hashes_repr.proof;
    payload : option Sc_rollup_inbox_message_repr.serialized;
  }.
  Definition with_proof proof (r : record) :=
    Build proof r.(payload).
  Definition with_payload payload (r : record) :=
    Build r.(proof) payload.
End level_tree_proof.
Definition level_tree_proof := level_tree_proof.record.

Definition level_tree_proof_encoding
  : Data_encoding.encoding level_tree_proof :=
  Data_encoding.conv
    (fun (function_parameter : level_tree_proof) ⇒
      let '{|
        level_tree_proof.proof := proof_value;
          level_tree_proof.payload := payload
          |} := function_parameter in
      (proof_value, payload))
    (fun (function_parameter :
      Sc_rollup_inbox_merkelized_payload_hashes_repr.proof × option string) ⇒
      let '(proof_value, payload) := function_parameter in
      {| level_tree_proof.proof := proof_value;
        level_tree_proof.payload :=
          Option.map Sc_rollup_inbox_message_repr.unsafe_of_string payload; |})
    None
    (Data_encoding.obj2
      (Data_encoding.req None None "proof"
        Sc_rollup_inbox_merkelized_payload_hashes_repr.proof_encoding)
      (Data_encoding.opt None None "payload" Data_encoding.string_value)).

Definition add_message
  (inbox_value : t) (payload : Sc_rollup_inbox_message_repr.serialized)
  (level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
  (level_tree : Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
  : M?
    (Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
      Sc_rollup_inbox_merkelized_payload_hashes_repr.t × t) :=
  let? '(level_tree_history, level_tree) :=
    Sc_rollup_inbox_merkelized_payload_hashes_repr.add_payload
      level_tree_history level_tree payload in
  let nb_messages_in_commitment_period :=
    Int64.succ inbox_value.(V1.t.nb_messages_in_commitment_period) in
  let inbox_value :=
    V1.t.with_nb_messages_in_commitment_period nb_messages_in_commitment_period
      inbox_value in
  return? (level_tree_history, level_tree, inbox_value).

[initialize_level_tree_when_needed level_tree_history inbox level_tree payloads] creates a new [level_tree] with the first element of [payloads] if [level_tree] is None.
[no_history] creates an empty history with [capacity] set to zero---this makes the [remember] function a no-op. We want this behaviour in the protocol because we don't want to store previous levels of the inbox.
[archive_if_needed level_tree_history history inbox new_level level_tree] is responsible for ensuring that the {!add_messages} function below has a correctly set-up [level_tree] to which to add the messages. If [new_level] is a higher level than the current inbox, we create a new inbox level tree at that level in which to start adding messages, and archive the earlier levels depending on the [history] parameter's [capacity]. If [level_tree] is [None] (this happens when the inbox is first created) we similarly create a new empty level tree.
This function is the only place we begin new level trees.
Definition archive_if_needed
  (level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
  (history_value : V1.History.(Bounded_history_repr.S.t)) (inbox_value : t)
  (new_level : Raw_level_repr.raw_level)
  (level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
  (payloads : list Sc_rollup_inbox_message_repr.serialized)
  : M?
    (V1.History.(Bounded_history_repr.S.t) × t ×
      Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
      Sc_rollup_inbox_merkelized_payload_hashes_repr.t ×
      list Sc_rollup_inbox_message_repr.serialized) :=
  if Raw_level_repr.op_eq inbox_value.(V1.t.level) new_level then
    match level_tree with
    | Some tree_value
      return?
        (history_value, inbox_value, level_tree_history, tree_value, payloads)
    | None
      let? '(inbox_value, level_tree_history, tree_value, payloads) :=
        initialize_level_tree_when_needed level_tree_history inbox_value
          level_tree payloads in
      return?
        (history_value, inbox_value, level_tree_history, tree_value, payloads)
    end
  else
    let? '(history_value, old_levels_messages) :=
      form_history_proof history_value inbox_value in
    let? '(inbox_value, level_tree_history, tree_value, payloads) :=
      initialize_level_tree_when_needed level_tree_history inbox_value
        level_tree payloads in
    let inbox_value :=
      {| V1.t.level := new_level;
        V1.t.nb_messages_in_commitment_period :=
          inbox_value.(V1.t.nb_messages_in_commitment_period);
        V1.t.current_level_proof := inbox_value.(V1.t.current_level_proof);
        V1.t.old_levels_messages := old_levels_messages; |} in
    return?
      (history_value, inbox_value, level_tree_history, tree_value, payloads).

Definition add_messages
  (level_tree_history : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
  (history_value : V1.History.(Bounded_history_repr.S.t)) (inbox_value : t)
  (level : Raw_level_repr.raw_level)
  (payloads : list Sc_rollup_inbox_message_repr.serialized)
  (level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
  : M?
    (Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
      Sc_rollup_inbox_merkelized_payload_hashes_repr.t ×
      V1.History.(Bounded_history_repr.S.t) × t) :=
  let? '_ :=
    Error_monad.error_when
      match payloads with
      | []true
      | _false
      end (Build_extensible "Tried_to_add_zero_messages" unit tt) in
  let? '_ :=
    Error_monad.error_when (Raw_level_repr.op_lt level inbox_value.(V1.t.level))
      (Build_extensible "Invalid_level_add_messages" Raw_level_repr.raw_level
        level) in
  let?
    '(history_value, inbox_value, level_tree_history, level_tree, payloads) :=
    archive_if_needed level_tree_history history_value inbox_value level
      level_tree payloads in
  let? '(level_tree_history, level_tree, inbox_value) :=
    List.fold_left_e
      (fun (function_parameter :
        Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t ×
          Sc_rollup_inbox_merkelized_payload_hashes_repr.t × t) ⇒
        let '(level_tree_history, level_tree, inbox_value) := function_parameter
          in
        fun (payload : Sc_rollup_inbox_message_repr.serialized) ⇒
          add_message inbox_value payload level_tree_history level_tree)
      (level_tree_history, level_tree, inbox_value) payloads in
  let current_level_proof (function_parameter : unit) : level_proof :=
    let '_ := function_parameter in
    let hash_value :=
      Sc_rollup_inbox_merkelized_payload_hashes_repr.hash_value level_tree in
    {| V1.level_proof.hash := hash_value; V1.level_proof.level := level; |} in
  return?
    (level_tree_history, level_tree, history_value,
      (V1.t.with_current_level_proof current_level_proof inbox_value)).

Definition add_messages_no_history
  (inbox_value : t) (level : Raw_level_repr.raw_level)
  (payloads : list Sc_rollup_inbox_message_repr.serialized)
  (level_tree : option Sc_rollup_inbox_merkelized_payload_hashes_repr.t)
  : M? (Sc_rollup_inbox_merkelized_payload_hashes_repr.t × t) :=
  Error_monad.Result_syntax.op_letplus
    (add_messages
      Sc_rollup_inbox_merkelized_payload_hashes_repr.History.no_history
      no_history inbox_value level payloads level_tree)
    (fun function_parameter
      let '(_, level_tree, _, inbox_value) := function_parameter in
      (level_tree, inbox_value)).

Definition inclusion_proof : Set := list history_proof.

Definition inclusion_proof_encoding
  : Data_encoding.encoding (list history_proof) :=
  Data_encoding.list_value None history_proof_encoding.

Definition pp_inclusion_proof
  (fmt : Format.formatter)
  (proof_value : list (Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t))
  : unit := Format.pp_print_list None pp_history_proof fmt proof_value.

Definition number_of_proof_steps {A : Set} (proof_value : list A) : int :=
  List.length proof_value.

Definition lift_ptr_path {A B : Set} (deref : A option B) (ptr_path : list A)
  : option (list B) :=
  let fix aux (accu_value : list B) (function_parameter : list A)
    : option (list B) :=
    match function_parameter with
    | []Some (List.rev accu_value)
    | cons x_value xs
      Option.bind (deref x_value)
        (fun (c_value : B) ⇒ aux (cons c_value accu_value) xs)
    end in
  aux nil ptr_path.

Records for the constructor parameters
Module ConstructorRecords_proof.
  Module proof.
    Module Single_level.
      Record record {inc message_proof : Set} : Set := Build {
        inc : inc;
        message_proof : message_proof;
      }.
      Arguments record : clear implicits.
      Definition with_inc {t_inc t_message_proof} inc
        (r : record t_inc t_message_proof) :=
        Build t_inc t_message_proof inc r.(message_proof).
      Definition with_message_proof {t_inc t_message_proof} message_proof
        (r : record t_inc t_message_proof) :=
        Build t_inc t_message_proof r.(inc) message_proof.
    End Single_level.
    Definition Single_level_skeleton := Single_level.record.

    Module Next_level.
      Record record {lower_message_proof inc : Set} : Set := Build {
        lower_message_proof : lower_message_proof;
        inc : inc;
      }.
      Arguments record : clear implicits.
      Definition with_lower_message_proof {t_lower_message_proof t_inc}
        lower_message_proof (r : record t_lower_message_proof t_inc) :=
        Build t_lower_message_proof t_inc lower_message_proof r.(inc).
      Definition with_inc {t_lower_message_proof t_inc} inc
        (r : record t_lower_message_proof t_inc) :=
        Build t_lower_message_proof t_inc r.(lower_message_proof) inc.
    End Next_level.
    Definition Next_level_skeleton := Next_level.record.
  End proof.
End ConstructorRecords_proof.
Import ConstructorRecords_proof.

Reserved Notation "'proof.Single_level".
Reserved Notation "'proof.Next_level".

Inductive proof : Set :=
| Single_level : 'proof.Single_level proof
| Next_level : 'proof.Next_level proof

where "'proof.Single_level" :=
  (proof.Single_level_skeleton inclusion_proof level_tree_proof)
and "'proof.Next_level" :=
  (proof.Next_level_skeleton level_tree_proof inclusion_proof).

Module proof.
  Include ConstructorRecords_proof.proof.
  Definition Single_level := 'proof.Single_level.
  Definition Next_level := 'proof.Next_level.
End proof.

Definition pp_proof (fmt : Format.formatter) (proof_value : proof) : unit :=
  match proof_value with
  | Single_level _
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Single_level inbox proof"
          CamlinternalFormatBasics.End_of_format) "Single_level inbox proof")
  | Next_level _
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "Next_level inbox proof"
          CamlinternalFormatBasics.End_of_format) "Next_level inbox proof")
  end.

Definition proof_encoding : Data_encoding.encoding proof :=
  Data_encoding.union (Some (Variant.Build "Uint8" unit tt))
    [
      Data_encoding.case_value "Single_level" None (Data_encoding.Tag 0)
        (Data_encoding.obj2
          (Data_encoding.req None None "inclusion_proof"
            inclusion_proof_encoding)
          (Data_encoding.req None None "message_proof"
            level_tree_proof_encoding))
        (fun (function_parameter : proof) ⇒
          match function_parameter with
          |
            Single_level {|
              proof.Single_level.inc := inc;
                proof.Single_level.message_proof := message_proof
                |} ⇒ Some (inc, message_proof)
          | _None
          end)
        (fun (function_parameter : inclusion_proof × level_tree_proof) ⇒
          let '(inc, message_proof) := function_parameter in
          Single_level
            {| proof.Single_level.inc := inc;
              proof.Single_level.message_proof := message_proof; |});
      Data_encoding.case_value "Next_level" None (Data_encoding.Tag 1)
        (Data_encoding.obj2
          (Data_encoding.req None None "lower_message_proof"
            level_tree_proof_encoding)
          (Data_encoding.req None None "inclusion_proof"
            inclusion_proof_encoding))
        (fun (function_parameter : proof) ⇒
          match function_parameter with
          |
            Next_level {|
              proof.Next_level.lower_message_proof := lower_message_proof;
                proof.Next_level.inc := inc
                |} ⇒ Some (lower_message_proof, inc)
          | _None
          end)
        (fun (function_parameter : level_tree_proof × inclusion_proof) ⇒
          let '(lower_message_proof, inc) := function_parameter in
          Next_level
            {|
              proof.Next_level.lower_message_proof :=
                lower_message_proof; proof.Next_level.inc := inc; |})
    ].

Definition of_serialized_proof : string option proof :=
  Data_encoding.Binary.of_string_opt proof_encoding.

Definition to_serialized_proof : proof string :=
  Data_encoding.Binary.to_string_exn None proof_encoding.

[verify_level_tree_proof {proof; payload} head_cell_hash n label] handles all the verification needed for a particular message proof at a particular level.
First it checks that [proof] is a valid inclusion of [payload_cell] in [head_cell] and that [head_cell] hash is [head_cell_hash].
Then there is two cases, - either [n] is superior to the index of [head_cell] then the provided [payload] must be empty (and [payload_cell = head_cell]); - or [0 < n < max_index head_cell] then the provided payload must exist and the payload hash must equal the content of the [payload_cell].
Definition verify_level_tree_proof (function_parameter : level_tree_proof)
  : Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t Z.t string
  M? (option Sc_rollup_inbox_message_repr.serialized) :=
  let '{|
    level_tree_proof.proof := proof_value;
      level_tree_proof.payload := payload
      |} := function_parameter in
  fun (head_cell_hash : Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.t)
    ⇒
    fun (n_value : Z.t) ⇒
      fun (label : string) ⇒
        let? '(payload_cell, head_cell) :=
          Sc_rollup_inbox_merkelized_payload_hashes_repr.verify_proof
            proof_value in
        let? '_ :=
          Error_monad.error_unless
            (Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.equal
              head_cell_hash
              (Sc_rollup_inbox_merkelized_payload_hashes_repr.hash_value
                head_cell))
            (Build_extensible "Inbox_proof_error" string
              (Format.sprintf
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal "message_proof ("
                    (CamlinternalFormatBasics.String
                      CamlinternalFormatBasics.No_padding
                      (CamlinternalFormatBasics.String_literal
                        ") does not match history"
                        CamlinternalFormatBasics.End_of_format)))
                  "message_proof (%s) does not match history") label)) in
        let max_index :=
          Sc_rollup_inbox_merkelized_payload_hashes_repr.get_index head_cell in
        if (Z.to_int n_value) >i max_index then
          let? '_ :=
            Error_monad.error_unless (Option.is_none payload)
              (Build_extensible "Inbox_proof_error" string
                "Payload provided but none expected") in
          let? '_ :=
            Error_monad.error_unless
              (Sc_rollup_inbox_merkelized_payload_hashes_repr.equal payload_cell
                head_cell)
              (Build_extensible "Inbox_proof_error" string
                "Provided proof is about a unexpected payload") in
          Error_monad.Result_syntax.return_none
        else
          let? payload :=
            match payload with
            | Some payloadreturn? payload
            | None
              Error_monad.Result_syntax.tzfail
                (Build_extensible "Inbox_proof_error" string
                  "Expected a payload but none provided in the proof")
            end in
          let payload_hash :=
            Sc_rollup_inbox_message_repr.hash_serialized_message payload in
          let proven_payload_hash :=
            Sc_rollup_inbox_merkelized_payload_hashes_repr.get_payload_hash
              payload_cell in
          let? '_ :=
            Error_monad.error_unless
              (Sc_rollup_inbox_message_repr.Hash.equal payload_hash
                proven_payload_hash)
              (Build_extensible "Inbox_proof_error" string
                "the payload provided does not match the payload's hash found in the message proof")
            in
          let payload_index :=
            Sc_rollup_inbox_merkelized_payload_hashes_repr.get_index
              payload_cell in
          let? '_ :=
            Error_monad.error_unless
              (Compare.Int.equal (Z.to_int n_value) payload_index)
              (Build_extensible "Inbox_proof_error" string
                (Format.sprintf
                  (CamlinternalFormatBasics.Format
                    (CamlinternalFormatBasics.String_literal
                      "found index in message_proof ("
                      (CamlinternalFormatBasics.String
                        CamlinternalFormatBasics.No_padding
                        (CamlinternalFormatBasics.String_literal
                          ") is incorrect"
                          CamlinternalFormatBasics.End_of_format)))
                    "found index in message_proof (%s) is incorrect") label)) in
          Error_monad.Result_syntax.return_some payload.

[produce_level_tree_proof get_level_tree_history head_cell_hash ~index]
[get_level_tree_history cell_hash] is a function that returns an {!Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t}. The returned history must contains the cell with hash [cell_hash], all its ancestor cell and their associated payload.
[head_cell] the latest cell of the [level_tree] we want to produce a proof on with hash [head_cell_hash].
This function produce either: - if [index <= head_cell_max_index], a proof that [payload_cell] with [index] is an ancestor to [head_cell] where [head_cell] is the cell with hash [head_cell_hash]. It returns the proof and the payload associated to [payload_cell]; - else a proof that [index] is out of bound for [head_cell]. It returns the proof and no payload.
Definition produce_level_tree_proof
  (get_level_tree_history :
    Sc_rollup_inbox_merkelized_payload_hashes_repr.History.key
    Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
  (head_cell_hash : Sc_rollup_inbox_merkelized_payload_hashes_repr.History.key)
  (index_value : int) : M? level_tree_proof :=
  let level_tree_history := get_level_tree_history head_cell_hash in
  let? head_cell :=
    match
      Sc_rollup_inbox_merkelized_payload_hashes_repr.History.find head_cell_hash
        level_tree_history with
    |
      Some {|
        Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.merkelized
          := head_cell;
          Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.payload
            := _
          |} ⇒ return? head_cell
    | None
      Error_monad.error_value
        (Build_extensible "Inbox_proof_error" string
          "could not find head_cell in the level_tree_history")
    end in
  let head_cell_max_index :=
    Sc_rollup_inbox_merkelized_payload_hashes_repr.get_index head_cell in
  let target_index := Compare.Int.min index_value head_cell_max_index in
  let proof_value :=
    Sc_rollup_inbox_merkelized_payload_hashes_repr.produce_proof
      level_tree_history target_index head_cell in
  match proof_value with
  |
    Some
      ({|
        Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.merkelized
          := _;
          Sc_rollup_inbox_merkelized_payload_hashes_repr.merkelized_and_payload.payload
            := payload
          |}, proof_value)
    if target_index =i index_value then
      return?
        {| level_tree_proof.proof := proof_value;
          level_tree_proof.payload := Some payload; |}
    else
      return?
        {| level_tree_proof.proof := proof_value;
          level_tree_proof.payload := None; |}
  | None
    Error_monad.Lwt_result_syntax.tzfail
      (Build_extensible "Inbox_proof_error" string
        "could not produce a valid proof.")
  end.

Axiom verify_inclusion_proof :
  inclusion_proof history_proof M? history_proof.

Definition verify_proof (function_parameter : Raw_level_repr.t × Z.t)
  : history_proof proof M? (option Sc_rollup_PVM_sig.inbox_message) :=
  let '(l_value, n_value) := function_parameter in
  fun (inbox_snapshot : history_proof) ⇒
    fun (proof_value : proof) ⇒
      let '_ :=
        (* ❌ Assert instruction is not handled. *)
        assert unit (Z.geq n_value Z.zero) in
      match proof_value with
      |
        Single_level {|
          proof.Single_level.inc := inc;
            proof.Single_level.message_proof := message_proof
            |} ⇒
        let? history_proof := verify_inclusion_proof inc inbox_snapshot in
        let level_proof := Skip_list.(Skip_list_repr.S.content) history_proof in
        let? payload_opt :=
          verify_level_tree_proof message_proof
            level_proof.(V1.level_proof.hash) n_value "single level" in
        match payload_opt with
        | None
          if equal_history_proof inbox_snapshot history_proof then
            Error_monad.Result_syntax.return_none
          else
            Error_monad.Result_syntax.tzfail
              (Build_extensible "Inbox_proof_error" string
                "payload is None but proof.level not top level")
        | Some payload
          Error_monad.Result_syntax.return_some
            {| Sc_rollup_PVM_sig.inbox_message.inbox_level := l_value;
              Sc_rollup_PVM_sig.inbox_message.message_counter := n_value;
              Sc_rollup_PVM_sig.inbox_message.payload := payload; |}
        end
      |
        Next_level {|
          proof.Next_level.lower_message_proof := lower_message_proof;
            proof.Next_level.inc := inc
            |} ⇒
        let? lower_history_proof := verify_inclusion_proof inc inbox_snapshot in
        let lower_level_proof :=
          Skip_list.(Skip_list_repr.S.content) lower_history_proof in
        let? should_be_none :=
          verify_level_tree_proof lower_message_proof
            lower_level_proof.(V1.level_proof.hash) n_value "lower" in
        match should_be_none with
        | None
          let? payload :=
            Sc_rollup_inbox_message_repr.serialize
              (Sc_rollup_inbox_message_repr.Internal
                Sc_rollup_inbox_message_repr.Start_of_level) in
          let inbox_level := Raw_level_repr.succ l_value in
          let message_counter := Z.zero in
          Error_monad.Result_syntax.return_some
            {| Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
              Sc_rollup_PVM_sig.inbox_message.message_counter :=
                message_counter;
              Sc_rollup_PVM_sig.inbox_message.payload := payload; |}
        | Some _
          Error_monad.Result_syntax.tzfail
            (Build_extensible "Inbox_proof_error" string
              "more messages to read in current level")
        end
      end.

Definition produce_proof
  (get_level_tree_history :
    Sc_rollup_inbox_merkelized_payload_hashes_repr.History.key
    Sc_rollup_inbox_merkelized_payload_hashes_repr.History.t)
  (history_value : V1.History.(Bounded_history_repr.S.t))
  (inbox_snapshot : Skip_list.(Skip_list_repr.S.cell) level_proof Hash.t)
  (function_parameter : Raw_level_repr.raw_level × Z.t)
  : M? (proof × option Sc_rollup_PVM_sig.inbox_message) :=
  let '(l_value, n_value) := function_parameter in
  let deref (ptr : Hash.H.(S.HASH.t)) : option V1.history_proof :=
    History.(Bounded_history_repr.S.find) ptr history_value in
  let compare (function_parameter : level_proof) : int :=
    let '{| V1.level_proof.hash := _; V1.level_proof.level := level |} :=
      function_parameter in
    Raw_level_repr.compare level l_value in
  let result_value :=
    Skip_list.(Skip_list_repr.S.search) deref compare inbox_snapshot in
  let? '(inc, history_proof) :=
    match result_value with
    | {|
      Skip_list_repr.search_result.rev_path := rev_path;
        Skip_list_repr.search_result.last_cell :=
          Skip_list_repr.Found history_proof
        |} ⇒ return? ((List.rev rev_path), history_proof)
    |
      ({| Skip_list_repr.search_result.last_cell := Skip_list_repr.Nearest _ |}
      | {|
      Skip_list_repr.search_result.last_cell := Skip_list_repr.No_exact_or_lower_ptr
        |} | {|
      Skip_list_repr.search_result.last_cell := Skip_list_repr.Deref_returned_none
        |}) ⇒
      Error_monad.Lwt_result_syntax.tzfail
        (Build_extensible "Inbox_proof_error" string
          (Format.asprintf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "Skip_list.search failed to find a valid path: "
                (CamlinternalFormatBasics.Alpha
                  CamlinternalFormatBasics.End_of_format))
              "Skip_list.search failed to find a valid path: %a")
            (Skip_list.(Skip_list_repr.S.pp_search_result) pp_history_proof)
            result_value))
    end in
  let level_proof := Skip_list.(Skip_list_repr.S.content) history_proof in
  let?
    '{| level_tree_proof.proof := _; level_tree_proof.payload := payload |} as
      message_proof :=
    produce_level_tree_proof get_level_tree_history
      level_proof.(V1.level_proof.hash) (Z.to_int n_value) in
  match payload with
  | Some payload
    return?
      ((Single_level
        {| proof.Single_level.inc := inc;
          proof.Single_level.message_proof := message_proof; |}),
        (Some
          {| Sc_rollup_PVM_sig.inbox_message.inbox_level := l_value;
            Sc_rollup_PVM_sig.inbox_message.message_counter := n_value;
            Sc_rollup_PVM_sig.inbox_message.payload := payload; |}))
  | None
    if equal_history_proof inbox_snapshot history_proof then
      return?
        ((Single_level
          {| proof.Single_level.inc := inc;
            proof.Single_level.message_proof := message_proof; |}), None)
    else
      let lower_message_proof := message_proof in
      let? input_given :=
        let inbox_level := Raw_level_repr.succ l_value in
        let message_counter := Z.zero in
        let? payload :=
          Sc_rollup_inbox_message_repr.serialize
            (Sc_rollup_inbox_message_repr.Internal
              Sc_rollup_inbox_message_repr.Start_of_level) in
        Error_monad.Lwt_result_syntax.return_some
          {| Sc_rollup_PVM_sig.inbox_message.inbox_level := inbox_level;
            Sc_rollup_PVM_sig.inbox_message.message_counter := message_counter;
            Sc_rollup_PVM_sig.inbox_message.payload := payload; |} in
      return?
        ((Next_level
          {| proof.Next_level.lower_message_proof := lower_message_proof;
            proof.Next_level.inc := inc; |}), input_given)
  end.

Definition empty (level : Raw_level_repr.t) : t :=
  let pre_genesis_level := Raw_level_repr.root_value in
  let initial_level_proof :=
    let hash_value := Sc_rollup_inbox_merkelized_payload_hashes_repr.Hash.zero
      in
    {| V1.level_proof.hash := hash_value;
      V1.level_proof.level := pre_genesis_level; |} in
  {| V1.t.level := level; V1.t.nb_messages_in_commitment_period := 0;
    V1.t.current_level_proof :=
      fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        initial_level_proof;
    V1.t.old_levels_messages :=
      Skip_list.(Skip_list_repr.S.genesis) initial_level_proof; |}.

Definition inbox : Set := t.