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 non-empty Tezos level greater than the level of the Last Cemented Commitment (LCC).
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 sparse 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.
The protocol maintains the hashes of the head of H, and the root hash of 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
  let '_ :=
    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) in
  Error_monad.register_error_kind Error_monad.Permanent
    "sc_rollup_inbox.empty_upper_level"
    "Internal error: No payload found in a [Level_crossing] proof"
    "Failed to find any message in the [upper_level] of a [Level_crossing] proof"
    None
    (Data_encoding.obj1
      (Data_encoding.req None None "upper_level" Raw_level_repr.encoding))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Empty_upper_level" then
          let upper_level := cast Raw_level_repr.t payload in
          Some upper_level
        else None
      end)
    (fun (upper_level : Raw_level_repr.raw_level) ⇒
      Build_extensible "Empty_upper_level" Raw_level_repr.raw_level upper_level).

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.

Definition hash_skip_list_cell
  (cell_value : Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t) : Hash.t :=
  let current_level_hash := 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 (Hash.to_bytes current_level_hash)
      (List.map Hash.to_bytes back_pointers_hashes)).

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

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

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

  Definition pp_history_proof
    (fmt : Format.formatter)
    (history_value : Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t) : unit :=
    let history_hash := hash_skip_list_cell history_value in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Formatting_gen
          (CamlinternalFormatBasics.Open_box
            (CamlinternalFormatBasics.Format
              CamlinternalFormatBasics.End_of_format ""))
          (CamlinternalFormatBasics.String_literal "hash : "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.Formatting_lit
                (CamlinternalFormatBasics.Break "@;" 1 0)
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.Formatting_lit
                    CamlinternalFormatBasics.Close_box
                    CamlinternalFormatBasics.End_of_format))))))
        "@[hash : %a@;%a@]") Hash.pp history_hash
      (Skip_list.(Skip_list_repr.S.pp) Hash.pp Hash.pp) history_value.

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 {
      rollup : Sc_rollup_repr.t;
      level : Raw_level_repr.t;
      nb_messages_in_commitment_period : int64;
      starting_level_of_current_commitment_period : Raw_level_repr.t;
      message_counter : Z.t;
      current_level_hash : unit Hash.t;
      old_levels_messages : history_proof;
    }.
    Definition with_rollup rollup (r : record) :=
      Build rollup r.(level) r.(nb_messages_in_commitment_period)
        r.(starting_level_of_current_commitment_period) r.(message_counter)
        r.(current_level_hash) r.(old_levels_messages).
    Definition with_level level (r : record) :=
      Build r.(rollup) level r.(nb_messages_in_commitment_period)
        r.(starting_level_of_current_commitment_period) r.(message_counter)
        r.(current_level_hash) r.(old_levels_messages).
    Definition with_nb_messages_in_commitment_period
      nb_messages_in_commitment_period (r : record) :=
      Build r.(rollup) r.(level) nb_messages_in_commitment_period
        r.(starting_level_of_current_commitment_period) r.(message_counter)
        r.(current_level_hash) r.(old_levels_messages).
    Definition with_starting_level_of_current_commitment_period
      starting_level_of_current_commitment_period (r : record) :=
      Build r.(rollup) r.(level) r.(nb_messages_in_commitment_period)
        starting_level_of_current_commitment_period r.(message_counter)
        r.(current_level_hash) r.(old_levels_messages).
    Definition with_message_counter message_counter (r : record) :=
      Build r.(rollup) r.(level) r.(nb_messages_in_commitment_period)
        r.(starting_level_of_current_commitment_period) message_counter
        r.(current_level_hash) r.(old_levels_messages).
    Definition with_current_level_hash current_level_hash (r : record) :=
      Build r.(rollup) r.(level) r.(nb_messages_in_commitment_period)
        r.(starting_level_of_current_commitment_period) r.(message_counter)
        current_level_hash r.(old_levels_messages).
    Definition with_old_levels_messages old_levels_messages (r : record) :=
      Build r.(rollup) r.(level) r.(nb_messages_in_commitment_period)
        r.(starting_level_of_current_commitment_period) r.(message_counter)
        r.(current_level_hash) old_levels_messages.
  End t.
  Definition t := t.record.

  Definition equal (inbox1 : t) (inbox2 : t) : bool :=
    let '{|
      t.rollup := rollup;
        t.level := level;
        t.nb_messages_in_commitment_period := nb_messages_in_commitment_period;
        t.starting_level_of_current_commitment_period :=
          starting_level_of_current_commitment_period;
        t.message_counter := message_counter;
        t.current_level_hash := current_level_hash;
        t.old_levels_messages := old_levels_messages
        |} := inbox1 in
    (Sc_rollup_repr.Address.equal rollup inbox2.(t.rollup)) &&
    ((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)) &&
    ((Raw_level_repr.equal starting_level_of_current_commitment_period
      inbox2.(t.starting_level_of_current_commitment_period)) &&
    ((Z.equal message_counter inbox2.(t.message_counter)) &&
    ((Hash.equal (current_level_hash tt) (inbox2.(t.current_level_hash) tt)) &&
    (equal_history_proof old_levels_messages inbox2.(t.old_levels_messages))))))).

  Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
    let '{|
      t.rollup := rollup;
        t.level := level;
        t.nb_messages_in_commitment_period := nb_messages_in_commitment_period;
        t.starting_level_of_current_commitment_period :=
          starting_level_of_current_commitment_period;
        t.message_counter := message_counter;
        t.current_level_hash := current_level_hash;
        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 "{ rollup = "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.Formatting_lit
                (CamlinternalFormatBasics.Break "@;" 1 0)
                (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
                                    "starting_level_of_current_commitment_period = "
                                    (CamlinternalFormatBasics.Alpha
                                      (CamlinternalFormatBasics.Formatting_lit
                                        (CamlinternalFormatBasics.Break "@;" 1 0)
                                        (CamlinternalFormatBasics.String_literal
                                          "message_counter = "
                                          (CamlinternalFormatBasics.Alpha
                                            (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>{ rollup = %a@;level = %a@;current messages hash = %a@;nb_messages_in_commitment_period = %s@;starting_level_of_current_commitment_period = %a@;message_counter = %a@;old_levels_messages = %a@;}@]")
      Sc_rollup_repr.Address.pp rollup Raw_level_repr.pp level Hash.pp
      (current_level_hash tt) (Int64.to_string nb_messages_in_commitment_period)
      Raw_level_repr.pp starting_level_of_current_commitment_period Z.pp_print
      message_counter 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_hash (inbox_value : t) : Hash.t :=
    inbox_value.(t.current_level_hash) tt.

  Definition old_levels_messages_encoding
    : Data_encoding.t (Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t) :=
    Skip_list.(Skip_list_repr.S.encoding) Hash.encoding Hash.encoding.

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{|
          t.rollup := rollup;
            t.level := level;
            t.nb_messages_in_commitment_period :=
              nb_messages_in_commitment_period;
            t.starting_level_of_current_commitment_period :=
              starting_level_of_current_commitment_period;
            t.message_counter := message_counter;
            t.current_level_hash := current_level_hash;
            t.old_levels_messages := old_levels_messages
            |} := function_parameter in
        (rollup, message_counter, nb_messages_in_commitment_period,
          starting_level_of_current_commitment_period, level,
          (current_level_hash tt), old_levels_messages))
      (fun (function_parameter :
        Sc_rollup_repr.t × Z.t × int64 × Raw_level_repr.t × Raw_level_repr.t ×
          Hash.t × history_proof) ⇒
        let
          '(rollup, message_counter, nb_messages_in_commitment_period,
            starting_level_of_current_commitment_period, level,
            current_level_hash, old_levels_messages) := function_parameter in
        {| t.rollup := rollup; t.level := level;
          t.nb_messages_in_commitment_period :=
            nb_messages_in_commitment_period;
          t.starting_level_of_current_commitment_period :=
            starting_level_of_current_commitment_period;
          t.message_counter := message_counter;
          t.current_level_hash :=
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              current_level_hash; t.old_levels_messages := old_levels_messages;
          |}) None
      (Data_encoding.obj7
        (Data_encoding.req None None "rollup" Sc_rollup_repr.encoding)
        (Data_encoding.req None None "message_counter" Data_encoding.n_value)
        (Data_encoding.req None None "nb_messages_in_commitment_period"
          Data_encoding.int64_value)
        (Data_encoding.req None None
          "starting_level_of_current_commitment_period" Raw_level_repr.encoding)
        (Data_encoding.req None None "level" Raw_level_repr.encoding)
        (Data_encoding.req None None "current_level_hash" Hash.encoding)
        (Data_encoding.req None None "old_levels_messages"
          old_levels_messages_encoding)).

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

  Definition start_new_commitment_period
    (inbox_value : t) (level : Raw_level_repr.t) : t :=
    t.with_starting_level_of_current_commitment_period level
      (t.with_nb_messages_in_commitment_period 0 inbox_value).

  Definition starting_level_of_current_commitment_period (inbox_value : t)
    : Raw_level_repr.t :=
    inbox_value.(t.starting_level_of_current_commitment_period).

  Definition refresh_commitment_period
    (commitment_period : int32) (level : Raw_level_repr.raw_level)
    (inbox_value : t) : M? t :=
    let start := starting_level_of_current_commitment_period inbox_value in
    let freshness := Raw_level_repr.diff_value level start in
    if freshness i32 commitment_period then
      let nb_periods :=
        Int32.to_int
          (Int32.mul (freshness /i32 commitment_period) commitment_period) in
      let? new_starting_level := Raw_level_repr.add start nb_periods in
      if
        (Raw_level_repr.op_lteq new_starting_level level) &&
        ((Int32.rem (Raw_level_repr.diff_value new_starting_level start)
          commitment_period) =i32 0)
      then
        return? (start_new_commitment_period inbox_value new_starting_level)
      else
        Error_monad.error_value (Build_extensible "Asserted" unit tt)
    else
      return? inbox_value.
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 key_of_message (ix : Z.t) : list string :=
  [ "message"; Data_encoding.Binary.to_string_exn None Data_encoding.n_value ix ].

Definition level_key : list string := [ "level" ].

Definition number_of_messages_key : list string := [ "number_of_messages" ].

Definition serialized_proof : Set := bytes.

Definition serialized_proof_encoding : Data_encoding.encoding Bytes.t :=
  Data_encoding.bytes_value.

Module Merkelized_operations.
  Record signature {inbox_context tree inclusion_proof proof : Set} : Set := {
    inbox_context := inbox_context;
    tree := tree;
    hash_level_tree : tree Hash.t;
    new_level_tree : inbox_context Raw_level_repr.t tree;
    add_messages :
      inbox_context V1.History.(Bounded_history_repr.S.t) t
      Raw_level_repr.t list Sc_rollup_inbox_message_repr.serialized
      option tree M? (tree × V1.History.(Bounded_history_repr.S.t) × t);
    add_messages_no_history :
      inbox_context t Raw_level_repr.t
      list Sc_rollup_inbox_message_repr.serialized option tree
      M? (tree × t);
    get_message_payload :
      tree Z.t option Sc_rollup_inbox_message_repr.serialized;
    form_history_proof :
      inbox_context V1.History.(Bounded_history_repr.S.t) t
      option tree M? (V1.History.(Bounded_history_repr.S.t) × history_proof);
    take_snapshot : t history_proof;
    inclusion_proof := inclusion_proof;
    inclusion_proof_encoding : Data_encoding.t inclusion_proof;
    pp_inclusion_proof : Format.formatter inclusion_proof unit;
    number_of_proof_steps : inclusion_proof int;
    verify_inclusion_proof :
      inclusion_proof history_proof history_proof bool;
    proof := proof;
    pp_proof : Format.formatter proof unit;
    to_serialized_proof : proof serialized_proof;
    of_serialized_proof : serialized_proof option proof;
    verify_proof :
      Raw_level_repr.t × Z.t history_proof proof
      M? (option Sc_rollup_PVM_sig.inbox_message);
    produce_proof :
      inbox_context V1.History.(Bounded_history_repr.S.t) history_proof
      Raw_level_repr.t × Z.t
      M? (proof × option Sc_rollup_PVM_sig.inbox_message);
    empty : inbox_context Sc_rollup_repr.t Raw_level_repr.t t;
  }.
End Merkelized_operations.
Definition Merkelized_operations := @Merkelized_operations.signature.
Arguments Merkelized_operations {_ _ _ _}.

Module P.
  Record signature {Tree_t Tree_tree proof : Set} : Set := {
    Tree :
      Context.TREE (t := Tree_t) (tree := Tree_tree) (key := list string)
        (value := bytes);
    t := Tree.(Context.TREE.t);
    tree := Tree.(Context.TREE.tree);
    commit_tree :
      Tree.(Context.TREE.t) list string Tree.(Context.TREE.tree) unit;
    lookup_tree : Tree.(Context.TREE.t) Hash.t option tree;
    proof := proof;
    proof_encoding : Data_encoding.t proof;
    proof_before : proof Hash.t;
    verify_proof :
       {a : Set}, proof (tree tree × a) option (tree × a);
    produce_proof :
       {a : Set},
      Tree.(Context.TREE.t) tree (tree tree × a) option (proof × a);
  }.
End P.
Definition P := @P.signature.
Arguments P {_ _ _}.

Module Make_hashing_scheme.
  Class FArgs {P_Tree_t P_Tree_tree P_proof : Set} := {
    P : P (Tree_t := P_Tree_t) (Tree_tree := P_Tree_tree) (proof := P_proof);
  }.
  Arguments Build_FArgs {_ _ _}.

  Definition Tree `{FArgs} := P.(P.Tree).

  Definition inbox_context `{FArgs} : Set := P.(P.Tree).(Context.TREE.t).

  Definition tree `{FArgs} : Set := P.(P.Tree).(Context.TREE.tree).

  Definition hash_level_tree `{FArgs}
    (level_tree : P.(P.Tree).(Context.TREE.tree)) : Hash.t :=
    Hash.of_context_hash (Tree.(Context.TREE.hash_value) level_tree).

  Definition set_level `{FArgs}
    (tree_value : P.(P.Tree).(Context.TREE.tree))
    (level : Raw_level_repr.raw_level) : P.(P.Tree).(Context.TREE.tree) :=
    let level_bytes :=
      Data_encoding.Binary.to_bytes_exn None Raw_level_repr.encoding level in
    Tree.(Context.TREE.add) tree_value level_key level_bytes.

  Definition find_level `{FArgs} (tree_value : P.(P.Tree).(Context.TREE.tree))
    : option Raw_level_repr.raw_level :=
    let level_bytes := Tree.(Context.TREE.find) tree_value level_key in
    Option.bind level_bytes
      (Data_encoding.Binary.of_bytes_opt Raw_level_repr.encoding).

  Definition set_number_of_messages `{FArgs}
    (tree_value : tree) (number_of_messages : Z.t)
    : P.(P.Tree).(Context.TREE.tree) :=
    let number_of_messages_bytes :=
      Data_encoding.Binary.to_bytes_exn None Data_encoding.n_value
        number_of_messages in
    Tree.(Context.TREE.add) tree_value number_of_messages_key
      number_of_messages_bytes.

Initialise the merkle tree for a new level in the inbox. We have to include the [level] in this structure so that it cannot be forged by a malicious rollup node.
  Definition new_level_tree `{FArgs}
    (ctxt : P.(P.Tree).(Context.TREE.t)) (level : Raw_level_repr.raw_level)
    : P.(P.Tree).(Context.TREE.tree) :=
    let tree_value := Tree.(Context.TREE.empty) ctxt in
    let tree_value := set_number_of_messages tree_value Z.zero in
    set_level tree_value level.

  Definition add_message `{FArgs} {A : Set}
    (inbox_value : t) (payload : Sc_rollup_inbox_message_repr.serialized)
    (level_tree : P.(P.Tree).(Context.TREE.tree))
    : Pervasives.result (P.(P.Tree).(Context.TREE.tree) × t) A :=
    let message_index := inbox_value.(V1.t.message_counter) in
    let message_counter := Z.succ message_index in
    let level_tree :=
      Tree.(Context.TREE.add) level_tree (key_of_message message_index)
        (Bytes.of_string payload) in
    let level_tree := set_number_of_messages level_tree message_counter in
    let nb_messages_in_commitment_period :=
      Int64.succ inbox_value.(V1.t.nb_messages_in_commitment_period) in
    let inbox_value :=
      {| V1.t.rollup := inbox_value.(V1.t.rollup);
        V1.t.level := inbox_value.(V1.t.level);
        V1.t.nb_messages_in_commitment_period :=
          nb_messages_in_commitment_period;
        V1.t.starting_level_of_current_commitment_period :=
          inbox_value.(V1.t.starting_level_of_current_commitment_period);
        V1.t.message_counter := message_counter;
        V1.t.current_level_hash := inbox_value.(V1.t.current_level_hash);
        V1.t.old_levels_messages := inbox_value.(V1.t.old_levels_messages); |}
      in
    return? (level_tree, inbox_value).

  Definition get_message_payload `{FArgs}
    (level_tree : P.(P.Tree).(Context.TREE.tree)) (message_index : Z.t)
    : option Sc_rollup_inbox_message_repr.serialized :=
    let key_value := key_of_message message_index in
    let bytes_value := Tree.(Context.TREE.find) level_tree key_value in
    Option.map
      (fun (bs : bytes) ⇒
        Sc_rollup_inbox_message_repr.unsafe_of_string (Bytes.to_string bs))
      bytes_value.

[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.
  Definition no_history `{FArgs} : V1.History.(Bounded_history_repr.S.t) :=
    History.(Bounded_history_repr.S.empty) 0.

  Definition take_snapshot `{FArgs} (inbox_value : t)
    : Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t :=
    let prev_cell := inbox_value.(V1.t.old_levels_messages) in
    let prev_cell_ptr := hash_skip_list_cell prev_cell in
    Skip_list.(Skip_list_repr.S.next) prev_cell prev_cell_ptr
      (current_level_hash inbox_value).

  Definition key_of_level `{FArgs} (level : Raw_level_repr.raw_level)
    : string :=
    let level_bytes :=
      Data_encoding.Binary.to_bytes_exn None Raw_level_repr.encoding level in
    Bytes.to_string level_bytes.

  Definition commit_tree `{FArgs}
    (ctxt : P.(P.Tree).(Context.TREE.t))
    (tree_value : P.(P.Tree).(Context.TREE.tree))
    (inbox_level : Raw_level_repr.raw_level) : unit :=
    let key_value := [ key_of_level inbox_level ] in
    P.(P.commit_tree) ctxt key_value tree_value.

  Definition form_history_proof `{FArgs}
    (ctxt : P.(P.Tree).(Context.TREE.t))
    (history_value : V1.History.(Bounded_history_repr.S.t)) (inbox_value : t)
    (level_tree : option P.(P.Tree).(Context.TREE.tree))
    : M?
      (V1.History.(Bounded_history_repr.S.t) ×
        Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t) :=
    let '_ :=
      let tree_value :=
        match level_tree with
        | Some tree_valuetree_value
        | Nonenew_level_tree ctxt inbox_value.(V1.t.level)
        end in
      commit_tree ctxt tree_value inbox_value.(V1.t.level) in
    let prev_cell := inbox_value.(V1.t.old_levels_messages) in
    let prev_cell_ptr := hash_skip_list_cell prev_cell in
    let? history_value :=
      History.(Bounded_history_repr.S.remember) prev_cell_ptr prev_cell
        history_value in
    let cell_value :=
      Skip_list.(Skip_list_repr.S.next) prev_cell prev_cell_ptr
        (current_level_hash inbox_value) in
    return? (history_value, cell_value).

[archive_if_needed ctxt 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 with the right [level] key.
This function and {!form_history_proof} are the only places we begin new level trees.
  Definition archive_if_needed `{FArgs}
    (ctxt : P.(P.Tree).(Context.TREE.t))
    (history_value : V1.History.(Bounded_history_repr.S.t)) (inbox_value : t)
    (new_level : Raw_level_repr.raw_level)
    (level_tree : option P.(P.Tree).(Context.TREE.tree))
    : M?
      (V1.History.(Bounded_history_repr.S.t) × t ×
        P.(P.Tree).(Context.TREE.tree)) :=
    if Raw_level_repr.op_eq inbox_value.(V1.t.level) new_level then
      match level_tree with
      | Some tree_valuereturn? (history_value, inbox_value, tree_value)
      | None
        let tree_value := new_level_tree ctxt new_level in
        return? (history_value, inbox_value, tree_value)
      end
    else
      let? '(history_value, old_levels_messages) :=
        form_history_proof ctxt history_value inbox_value level_tree in
      let tree_value := new_level_tree ctxt new_level in
      let inbox_value :=
        {| V1.t.rollup := inbox_value.(V1.t.rollup); V1.t.level := new_level;
          V1.t.nb_messages_in_commitment_period :=
            inbox_value.(V1.t.nb_messages_in_commitment_period);
          V1.t.starting_level_of_current_commitment_period :=
            inbox_value.(V1.t.starting_level_of_current_commitment_period);
          V1.t.message_counter := Z.zero;
          V1.t.current_level_hash := inbox_value.(V1.t.current_level_hash);
          V1.t.old_levels_messages := old_levels_messages; |} in
      return? (history_value, inbox_value, tree_value).

  Definition add_messages `{FArgs}
    (ctxt : P.(P.Tree).(Context.TREE.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 P.(P.Tree).(Context.TREE.tree))
    : M?
      (P.(P.Tree).(Context.TREE.tree) × V1.History.(Bounded_history_repr.S.t) ×
        t) :=
    let? '_ :=
      Error_monad.fail_when
        match payloads with
        | []true
        | _false
        end (Build_extensible "Tried_to_add_zero_messages" unit tt) in
    let? '_ :=
      Error_monad.fail_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) :=
      archive_if_needed ctxt history_value inbox_value level level_tree in
    let? '(level_tree, inbox_value) :=
      List.fold_left_es
        (fun (function_parameter : P.(P.Tree).(Context.TREE.tree) × t) ⇒
          let '(level_tree, inbox_value) := function_parameter in
          fun (payload : Sc_rollup_inbox_message_repr.serialized) ⇒
            add_message inbox_value payload level_tree)
        (level_tree, inbox_value) payloads in
    let current_level_hash (function_parameter : unit) : Hash.t :=
      let '_ := function_parameter in
      hash_level_tree level_tree in
    return?
      (level_tree, history_value,
        (V1.t.with_current_level_hash current_level_hash inbox_value)).

  Definition add_messages_no_history `{FArgs}
    (ctxt : P.(P.Tree).(Context.TREE.t)) (inbox_value : t)
    (level : Raw_level_repr.raw_level)
    (payloads : list Sc_rollup_inbox_message_repr.serialized)
    (level_tree : option P.(P.Tree).(Context.TREE.tree))
    : M? (P.(P.Tree).(Context.TREE.tree) × t) :=
    Error_monad.Lwt_tzresult_syntax.op_letplus
      (add_messages ctxt 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 `{FArgs} : Set := list history_proof.

  Definition inclusion_proof_encoding `{FArgs}
    : Data_encoding.encoding (list history_proof) :=
    Data_encoding.list_value None history_proof_encoding.

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

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

  Definition lift_ptr_path `{FArgs} {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.

  Definition verify_inclusion_proof `{FArgs}
    (proof_value : list (Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t))
    (a_value : Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t)
    (b_value : Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t) : bool :=
    let assoc :=
      List.map
        (fun (c_value : Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t) ⇒
          ((hash_skip_list_cell c_value), c_value)) proof_value in
    let path := Pervasives.fst (List.split assoc) in
    let deref :=
      let map := Hash.H.(HASH.Map).(S.INDEXES_MAP.of_seq) (List.to_seq assoc) in
      fun (ptr : Hash.H.(S.HASH.t)) ⇒
        Hash.H.(HASH.Map).(S.INDEXES_MAP.find_opt) ptr map in
    let cell_ptr := hash_skip_list_cell b_value in
    let target_ptr := hash_skip_list_cell a_value in
    Skip_list.(Skip_list_repr.S.valid_back_path) Hash.equal deref cell_ptr
      target_ptr path.

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

      Module Level_crossing.
        Record record {lower upper inc lower_message_proof upper_message_proof
          upper_level : Set} : Set := Build {
          lower : lower;
          upper : upper;
          inc : inc;
          lower_message_proof : lower_message_proof;
          upper_message_proof : upper_message_proof;
          upper_level : upper_level;
        }.
        Arguments record : clear implicits.
        Definition with_lower
          {t_lower t_upper t_inc t_lower_message_proof t_upper_message_proof
            t_upper_level} lower
          (r :
            record t_lower t_upper t_inc t_lower_message_proof
              t_upper_message_proof t_upper_level) :=
          Build t_lower t_upper t_inc t_lower_message_proof
            t_upper_message_proof t_upper_level lower r.(upper) r.(inc)
            r.(lower_message_proof) r.(upper_message_proof) r.(upper_level).
        Definition with_upper
          {t_lower t_upper t_inc t_lower_message_proof t_upper_message_proof
            t_upper_level} upper
          (r :
            record t_lower t_upper t_inc t_lower_message_proof
              t_upper_message_proof t_upper_level) :=
          Build t_lower t_upper t_inc t_lower_message_proof
            t_upper_message_proof t_upper_level r.(lower) upper r.(inc)
            r.(lower_message_proof) r.(upper_message_proof) r.(upper_level).
        Definition with_inc
          {t_lower t_upper t_inc t_lower_message_proof t_upper_message_proof
            t_upper_level} inc
          (r :
            record t_lower t_upper t_inc t_lower_message_proof
              t_upper_message_proof t_upper_level) :=
          Build t_lower t_upper t_inc t_lower_message_proof
            t_upper_message_proof t_upper_level r.(lower) r.(upper) inc
            r.(lower_message_proof) r.(upper_message_proof) r.(upper_level).
        Definition with_lower_message_proof
          {t_lower t_upper t_inc t_lower_message_proof t_upper_message_proof
            t_upper_level} lower_message_proof
          (r :
            record t_lower t_upper t_inc t_lower_message_proof
              t_upper_message_proof t_upper_level) :=
          Build t_lower t_upper t_inc t_lower_message_proof
            t_upper_message_proof t_upper_level r.(lower) r.(upper) r.(inc)
            lower_message_proof r.(upper_message_proof) r.(upper_level).
        Definition with_upper_message_proof
          {t_lower t_upper t_inc t_lower_message_proof t_upper_message_proof
            t_upper_level} upper_message_proof
          (r :
            record t_lower t_upper t_inc t_lower_message_proof
              t_upper_message_proof t_upper_level) :=
          Build t_lower t_upper t_inc t_lower_message_proof
            t_upper_message_proof t_upper_level r.(lower) r.(upper) r.(inc)
            r.(lower_message_proof) upper_message_proof r.(upper_level).
        Definition with_upper_level
          {t_lower t_upper t_inc t_lower_message_proof t_upper_message_proof
            t_upper_level} upper_level
          (r :
            record t_lower t_upper t_inc t_lower_message_proof
              t_upper_message_proof t_upper_level) :=
          Build t_lower t_upper t_inc t_lower_message_proof
            t_upper_message_proof t_upper_level r.(lower) r.(upper) r.(inc)
            r.(lower_message_proof) r.(upper_message_proof) upper_level.
      End Level_crossing.
      Definition Level_crossing_skeleton := Level_crossing.record.
    End proof.
  End ConstructorRecords_proof.
  Import ConstructorRecords_proof.

  Reserved Notation "'proof.Single_level".
  Reserved Notation "'proof.Level_crossing".

  Inductive proof `{FArgs} : Set :=
  | Single_level : 'proof.Single_level proof
  | Level_crossing : 'proof.Level_crossing proof
  
  where "'proof.Single_level" :=
    (proof.Single_level_skeleton history_proof inclusion_proof P.(P.proof))
  and "'proof.Level_crossing" :=
    (proof.Level_crossing_skeleton history_proof history_proof inclusion_proof
      P.(P.proof) P.(P.proof) Raw_level_repr.t).

  Module proof.
    Include ConstructorRecords_proof.proof.
    Definition Single_level `{FArgs} := 'proof.Single_level.
    Definition Level_crossing `{FArgs} := 'proof.Level_crossing.
  End proof.

  Definition pp_proof `{FArgs} (fmt : Format.formatter) (proof_value : proof)
    : unit :=
    match proof_value with
    | Single_level {| proof.Single_level.level := level |} ⇒
      let hash_value := Skip_list.(Skip_list_repr.S.content) level in
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "Single_level inbox proof at "
            (CamlinternalFormatBasics.Alpha
              CamlinternalFormatBasics.End_of_format))
          "Single_level inbox proof at %a") Hash.pp hash_value
    |
      Level_crossing {|
        proof.Level_crossing.lower := lower;
          proof.Level_crossing.upper := upper;
          proof.Level_crossing.upper_level := upper_level
          |} ⇒
      let lower_hash := Skip_list.(Skip_list_repr.S.content) lower in
      let upper_hash := Skip_list.(Skip_list_repr.S.content) upper in
      Format.fprintf fmt
        (CamlinternalFormatBasics.Format
          (CamlinternalFormatBasics.String_literal
            "Level_crossing inbox proof between "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal " and "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal " (upper_level "
                    (CamlinternalFormatBasics.Alpha
                      (CamlinternalFormatBasics.Char_literal ")" % char
                        CamlinternalFormatBasics.End_of_format)))))))
          "Level_crossing inbox proof between %a and %a (upper_level %a)")
        Hash.pp lower_hash Hash.pp upper_hash Raw_level_repr.pp upper_level
    end.

  Definition proof_encoding `{FArgs} : 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.obj3
            (Data_encoding.req None None "level" history_proof_encoding)
            (Data_encoding.req None None "inclusion_proof"
              inclusion_proof_encoding)
            (Data_encoding.req None None "message_proof"
              P.(P.proof_encoding)))
          (fun (function_parameter : proof) ⇒
            match function_parameter with
            |
              Single_level {|
                proof.Single_level.level := level;
                  proof.Single_level.inc := inc;
                  proof.Single_level.message_proof :=
                    message_proof
                  |} ⇒ Some (level, inc, message_proof)
            | _None
            end)
          (fun (function_parameter :
            history_proof × inclusion_proof × P.(P.proof)) ⇒
            let '(level, inc, message_proof) := function_parameter in
            Single_level
              {| proof.Single_level.level := level;
                proof.Single_level.inc := inc;
                proof.Single_level.message_proof :=
                  message_proof; |});
        Data_encoding.case_value "Level_crossing" None (Data_encoding.Tag 1)
          (Data_encoding.obj6
            (Data_encoding.req None None "lower" history_proof_encoding)
            (Data_encoding.req None None "upper" history_proof_encoding)
            (Data_encoding.req None None "inclusion_proof"
              inclusion_proof_encoding)
            (Data_encoding.req None None "lower_message_proof"
              P.(P.proof_encoding))
            (Data_encoding.req None None "upper_message_proof"
              P.(P.proof_encoding))
            (Data_encoding.req None None "upper_level"
              Raw_level_repr.encoding))
          (fun (function_parameter : proof) ⇒
            match function_parameter with
            |
              Level_crossing {|
                proof.Level_crossing.lower := lower;
                  proof.Level_crossing.upper := upper;
                  proof.Level_crossing.inc := inc;
                  proof.Level_crossing.lower_message_proof
                    :=
                    lower_message_proof;
                  proof.Level_crossing.upper_message_proof
                    :=
                    upper_message_proof;
                  proof.Level_crossing.upper_level :=
                    upper_level
                  |} ⇒
              Some
                (lower, upper, inc, lower_message_proof,
                  upper_message_proof, upper_level)
            | _None
            end)
          (fun (function_parameter :
            history_proof × history_proof × inclusion_proof ×
              P.(P.proof) × P.(P.proof) × Raw_level_repr.raw_level)
            ⇒
            let
              '(lower, upper, inc, lower_message_proof,
                upper_message_proof, upper_level) :=
              function_parameter in
            Level_crossing
              {| proof.Level_crossing.lower := lower;
                proof.Level_crossing.upper := upper;
                proof.Level_crossing.inc := inc;
                proof.Level_crossing.lower_message_proof :=
                  lower_message_proof;
                proof.Level_crossing.upper_message_proof :=
                  upper_message_proof;
                proof.Level_crossing.upper_level := upper_level;
                |})
      ].

  Definition of_serialized_proof `{FArgs} : bytes option proof :=
    Data_encoding.Binary.of_bytes_opt proof_encoding.

  Definition to_serialized_proof `{FArgs} : proof bytes :=
    Data_encoding.Binary.to_bytes_exn None proof_encoding.

  Definition proof_error `{FArgs} {A : Set} (reason_value : string) : M? A :=
    Error_monad.Lwt_tzresult_syntax.fail
      (Build_extensible "Inbox_proof_error" string reason_value).

  Definition check `{FArgs} (p_value : bool) (reason_value : string)
    : M? unit :=
    Error_monad.unless p_value
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        proof_error reason_value).

Utility function that checks the inclusion proof [inc] for any inbox proof.
In the case of a [Single_level] proof this is just an inclusion proof between [level] and the inbox snapshot targeted the proof.
In the case of a [Level_crossing] proof [inc] must be an inclusion proof between [upper] and the inbox snapshot. In this case we must additionally check that [lower] is the immediate predecessor of [upper] in the inbox skip list. NB: there may be many 'inbox levels' apart, but if the intervening levels are empty they will be immediate neighbours in the skip list because it misses empty levels out.
  Definition check_inclusions `{FArgs}
    (proof_value : proof)
    (snapshot_value : Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t)
    : M? unit :=
    check
      match proof_value with
      |
        Single_level {|
          proof.Single_level.level := level;
            proof.Single_level.inc := inc
            |} ⇒ verify_inclusion_proof inc level snapshot_value
      |
        Level_crossing {|
          proof.Level_crossing.lower := lower;
            proof.Level_crossing.upper := upper;
            proof.Level_crossing.inc := inc
            |} ⇒
        let prev_cell := Skip_list.(Skip_list_repr.S.back_pointer) upper 0 in
        match prev_cell with
        | Nonefalse
        | Some p_value
          (verify_inclusion_proof inc upper snapshot_value) &&
          (Hash.equal p_value (hash_skip_list_cell lower))
        end
      end "invalid inclusions".

To construct or verify a tree proof we need a function of type
[tree -> (tree, result) Lwt.t]
where [result] is some data extracted from the tree that we care about proving. [payload_and_level n] is such a function, used for checking both the inbox level specified inside the tree and the message at a particular index, [n].
For this function, the [result] is
[(payload, level) : string option * Raw_level_repr.t option]
where [payload] is [None] if there was no message at the index. The [level] part of the result will only be [None] if the [tree] is not in the correct format for an inbox level. This should not happen if the [tree] was correctly initialised with [new_level_tree].
  Definition payload_and_level `{FArgs}
    (n_value : Z.t) (tree_value : P.(P.Tree).(Context.TREE.tree))
    : P.(P.Tree).(Context.TREE.tree) ×
      (option Sc_rollup_inbox_message_repr.serialized ×
        option Raw_level_repr.raw_level) :=
    let payload := get_message_payload tree_value n_value in
    let level := find_level tree_value in
    (tree_value, (payload, level)).

Utility function that handles all the verification needed for a particular message proof at a particular level. It calls [P.verify_proof], but also checks the proof has the correct [P.proof_before] hash and the [level] stored inside the tree is the expected one.
  Definition check_message_proof `{FArgs}
    (message_proof : P.(P.proof)) (level_hash : Hash.t)
    (function_parameter : Raw_level_repr.raw_level × Z.t)
    : string M? (option Sc_rollup_inbox_message_repr.serialized) :=
    let '(l_value, n_value) := function_parameter in
    fun (label : string) ⇒
      let? '_ :=
        check (Hash.equal level_hash (P.(P.proof_before) message_proof))
          (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 result_value :=
        P.(P.verify_proof) message_proof (payload_and_level n_value) in
      match result_value with
      | None
        proof_error
          (Format.sprintf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "message_proof is invalid ("
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.Char_literal ")" % char
                    CamlinternalFormatBasics.End_of_format)))
              "message_proof is invalid (%s)") label)
      | Some (_, (_, None))
        proof_error
          (Format.sprintf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal
                "badly encoded level in message_proof ("
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.Char_literal ")" % char
                    CamlinternalFormatBasics.End_of_format)))
              "badly encoded level in message_proof (%s)") label)
      | Some (_, (payload_opt, Some proof_level))
        let? '_ :=
          check (Raw_level_repr.equal proof_level l_value)
            (Format.sprintf
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "incorrect level in message_proof ("
                  (CamlinternalFormatBasics.String
                    CamlinternalFormatBasics.No_padding
                    (CamlinternalFormatBasics.Char_literal ")" % char
                      CamlinternalFormatBasics.End_of_format)))
                "incorrect level in message_proof (%s)") label) in
        return? payload_opt
      end.

  Definition verify_proof `{FArgs}
    (function_parameter : Raw_level_repr.raw_level × Z.t)
    : Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t proof
    M? (option Sc_rollup_PVM_sig.inbox_message) :=
    let '(l_value, n_value) := function_parameter in
    fun (snapshot_value : Skip_list.(Skip_list_repr.S.cell) Hash.t Hash.t) ⇒
      fun (proof_value : proof) ⇒
        let? '_ := check_inclusions proof_value snapshot_value in
        match proof_value with
        | Single_level p_value
          let level_hash :=
            Skip_list.(Skip_list_repr.S.content)
              p_value.(proof.Single_level.level) in
          let? payload_opt :=
            check_message_proof p_value.(proof.Single_level.message_proof)
              level_hash (l_value, n_value) "single level" in
          match payload_opt with
          | None
            if
              equal_history_proof snapshot_value
                p_value.(proof.Single_level.level)
            then
              return? None
            else
              proof_error "payload is None but proof.level not top level"
          | Some payload
            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
        | Level_crossing p_value
          let lower_level_hash :=
            Skip_list.(Skip_list_repr.S.content)
              p_value.(proof.Level_crossing.lower) in
          let? should_be_none :=
            check_message_proof
              p_value.(proof.Level_crossing.lower_message_proof)
              lower_level_hash (l_value, n_value) "lower" in
          let? '_ :=
            match should_be_none with
            | Nonereturn? tt
            | Some _proof_error "more messages to read in lower level"
            end in
          let upper_level_hash :=
            Skip_list.(Skip_list_repr.S.content)
              p_value.(proof.Level_crossing.upper) in
          let? payload_opt :=
            check_message_proof
              p_value.(proof.Level_crossing.upper_message_proof)
              upper_level_hash
              (p_value.(proof.Level_crossing.upper_level), Z.zero) "upper" in
          match payload_opt with
          | None
            Error_monad.Lwt_tzresult_syntax.fail
              (Build_extensible "Empty_upper_level" Raw_level_repr.t
                p_value.(proof.Level_crossing.upper_level))
          | Some payload
            return?
              (Some
                {|
                  Sc_rollup_PVM_sig.inbox_message.inbox_level :=
                    p_value.(proof.Level_crossing.upper_level);
                  Sc_rollup_PVM_sig.inbox_message.message_counter := Z.zero;
                  Sc_rollup_PVM_sig.inbox_message.payload := payload; |})
          end
        end.

Utility function; we convert all our calls to be consistent with [Lwt_tzresult_syntax].
  Definition option_to_result `{FArgs} {A : Set}
    (e_value : string) (lwt_opt : option A) : M? A :=
    let opt := lwt_opt in
    match opt with
    | Noneproof_error e_value
    | Some x_valuereturn? x_value
    end.

  Definition produce_proof `{FArgs}
    (ctxt : P.(P.Tree).(Context.TREE.t))
    (history_value : V1.History.(Bounded_history_repr.S.t))
    (inbox_value : V1.history_proof)
    (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 (hash_value : Hash.t) : int :=
      let tree_value := P.(P.lookup_tree) ctxt hash_value in
      match tree_value with
      | None ⇒ (-1)
      | Some tree_value
        let level := find_level tree_value in
        match level with
        | None ⇒ (-1)
        | Some levelRaw_level_repr.compare level l_value
        end
      end in
    let result_value :=
      Skip_list.(Skip_list_repr.S.search) deref compare inbox_value in
    let? '(inc, level) :=
      match result_value with
      | {|
        Skip_list_repr.search_result.rev_path := rev_path;
          Skip_list_repr.search_result.last_cell := Skip_list_repr.Found level
          |} ⇒ return? ((List.rev rev_path), level)
      |
        ({|
        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
          |}) ⇒
        proof_error
          (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_tree :=
      option_to_result "could not find level_tree in the inbox_context"
        (P.(P.lookup_tree) ctxt (Skip_list.(Skip_list_repr.S.content) level)) in
    let? '(message_proof, (payload_opt, _)) :=
      option_to_result "failed to produce message proof for level_tree"
        (P.(P.produce_proof) ctxt level_tree (payload_and_level n_value)) in
    match payload_opt with
    | Some payload
      return?
        ((Single_level
          {| proof.Single_level.level := 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_value level then
        return?
          ((Single_level
            {| proof.Single_level.level := level; proof.Single_level.inc := inc;
              proof.Single_level.message_proof := message_proof; |}), None)
      else
        let target_index :=
          (Skip_list.(Skip_list_repr.S.index_value) level) +i 1 in
        let cell_ptr := hash_skip_list_cell inbox_value in
        let? history_value :=
          History.(Bounded_history_repr.S.remember) cell_ptr inbox_value
            history_value in
        let deref (ptr : Hash.H.(S.HASH.t)) : option V1.history_proof :=
          History.(Bounded_history_repr.S.find) ptr history_value in
        let? inc :=
          option_to_result "failed to find path to upper level"
            (Option.join
              (Option.map (lift_ptr_path deref)
                (Skip_list.(Skip_list_repr.S.back_path) deref cell_ptr
                  target_index))) in
        let? upper :=
          option_to_result "back_path returned empty list" (List.last_opt inc)
          in
        let? upper_level_tree :=
          option_to_result
            "could not find upper_level_tree in the inbox_context"
            (P.(P.lookup_tree) ctxt (Skip_list.(Skip_list_repr.S.content) upper))
          in
        let? '(upper_message_proof, (payload_opt, upper_level_opt)) :=
          option_to_result
            "failed to produce message proof for upper_level_tree"
            (P.(P.produce_proof) ctxt upper_level_tree
              (payload_and_level Z.zero)) in
        let? upper_level :=
          option_to_result
            "upper_level_tree was misformed---could not find level"
            upper_level_opt in
        match payload_opt with
        | None
          proof_error "if upper_level_tree exists, the payload must exist"
        | Some payload
          let input_given :=
            Some
              {| Sc_rollup_PVM_sig.inbox_message.inbox_level := upper_level;
                Sc_rollup_PVM_sig.inbox_message.message_counter := Z.zero;
                Sc_rollup_PVM_sig.inbox_message.payload := payload; |} in
          return?
            ((Level_crossing
              {| proof.Level_crossing.lower := level;
                proof.Level_crossing.upper := upper;
                proof.Level_crossing.inc := inc;
                proof.Level_crossing.lower_message_proof := message_proof;
                proof.Level_crossing.upper_message_proof := upper_message_proof;
                proof.Level_crossing.upper_level := upper_level; |}),
              input_given)
        end
    end.

  Definition empty `{FArgs}
    (context_value : P.(P.Tree).(Context.TREE.t)) (rollup : Sc_rollup_repr.t)
    (level : Raw_level_repr.raw_level) : t :=
    let '_ :=
      (* ❌ Assert instruction is not handled. *)
      assert unit (Raw_level_repr.op_ltgt level Raw_level_repr.root_value) in
    let pre_genesis_level := Raw_level_repr.root_value in
    let initial_level := new_level_tree context_value pre_genesis_level in
    let '_ := commit_tree context_value initial_level pre_genesis_level in
    let initial_hash := hash_level_tree initial_level in
    {| V1.t.rollup := rollup; V1.t.level := level;
      V1.t.nb_messages_in_commitment_period := 0;
      V1.t.starting_level_of_current_commitment_period := level;
      V1.t.message_counter := Z.zero;
      V1.t.current_level_hash :=
        fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          initial_hash;
      V1.t.old_levels_messages :=
        Skip_list.(Skip_list_repr.S.genesis) initial_hash; |}.

  (* Make_hashing_scheme *)
  Definition functor `{FArgs} :=
    {|
      Merkelized_operations.hash_level_tree := hash_level_tree;
      Merkelized_operations.new_level_tree := new_level_tree;
      Merkelized_operations.add_messages := add_messages;
      Merkelized_operations.add_messages_no_history := add_messages_no_history;
      Merkelized_operations.get_message_payload := get_message_payload;
      Merkelized_operations.form_history_proof := form_history_proof;
      Merkelized_operations.take_snapshot := take_snapshot;
      Merkelized_operations.inclusion_proof_encoding := inclusion_proof_encoding;
      Merkelized_operations.pp_inclusion_proof := pp_inclusion_proof;
      Merkelized_operations.number_of_proof_steps := number_of_proof_steps;
      Merkelized_operations.verify_inclusion_proof := verify_inclusion_proof;
      Merkelized_operations.pp_proof := pp_proof;
      Merkelized_operations.to_serialized_proof := to_serialized_proof;
      Merkelized_operations.of_serialized_proof := of_serialized_proof;
      Merkelized_operations.verify_proof := verify_proof;
      Merkelized_operations.produce_proof := produce_proof;
      Merkelized_operations.empty := empty
    |}.
End Make_hashing_scheme.
Definition Make_hashing_scheme {P_Tree_t P_Tree_tree P_proof : Set}
  (P : P (Tree_t := P_Tree_t) (Tree_tree := P_Tree_tree) (proof := P_proof))
  : Merkelized_operations (inbox_context := P.(P.Tree).(Context.TREE.t))
    (tree := P.(P.Tree).(Context.TREE.tree)) (inclusion_proof := _) (proof := _)
  :=
  let '_ := Make_hashing_scheme.Build_FArgs P in
  Make_hashing_scheme.functor.

Definition Make_hashing_scheme_include :
  Merkelized_operations (inbox_context := Context.t) (tree := Context.tree)
    (inclusion_proof := _) (proof := _) :=
  Make_hashing_scheme
    (let Tree :=
      let mem := Context.Tree.(Context.TREE.mem) in
      let mem_tree := Context.Tree.(Context.TREE.mem_tree) in
      let find := Context.Tree.(Context.TREE.find) in
      let find_tree := Context.Tree.(Context.TREE.find_tree) in
      let list_value := Context.Tree.(Context.TREE.list_value) in
      let length := Context.Tree.(Context.TREE.length) in
      let add := Context.Tree.(Context.TREE.add) in
      let add_tree := Context.Tree.(Context.TREE.add_tree) in
      let remove := Context.Tree.(Context.TREE.remove) in
      let fold {a : Set} := Context.Tree.(Context.TREE.fold) in
      let config_value := Context.Tree.(Context.TREE.config_value) in
      let empty := Context.Tree.(Context.TREE.empty) in
      let is_empty := Context.Tree.(Context.TREE.is_empty) in
      let kind_value := Context.Tree.(Context.TREE.kind_value) in
      let to_value := Context.Tree.(Context.TREE.to_value) in
      let of_value := Context.Tree.(Context.TREE.of_value) in
      let hash_value := Context.Tree.(Context.TREE.hash_value) in
      let equal := Context.Tree.(Context.TREE.equal) in
      let clear := Context.Tree.(Context.TREE.clear) in
      let t : Set := Context.t in
      let tree : Set := Context.tree in
      let value : Set := bytes in
      let key : Set := list string in
      {|
        Context.TREE.mem := mem;
        Context.TREE.mem_tree := mem_tree;
        Context.TREE.find := find;
        Context.TREE.find_tree := find_tree;
        Context.TREE.list_value := list_value;
        Context.TREE.length := length;
        Context.TREE.add := add;
        Context.TREE.add_tree := add_tree;
        Context.TREE.remove := remove;
        Context.TREE.fold _ := fold;
        Context.TREE.config_value := config_value;
        Context.TREE.empty := empty;
        Context.TREE.is_empty := is_empty;
        Context.TREE.kind_value := kind_value;
        Context.TREE.to_value := to_value;
        Context.TREE.of_value := of_value;
        Context.TREE.hash_value := hash_value;
        Context.TREE.equal := equal;
        Context.TREE.clear := clear
      |} in
    let t : Set := Context.t in
    let tree : Set := Context.tree in
    let commit_tree {A B C : Set} (_ctxt : A) (_key : B) (_tree : C) : unit :=
      tt in
    let lookup_tree {A B C : Set} (_ctxt : A) (_hash : B) : option C :=
      None in
    let proof : Set := Context.Proof.t Context.Proof.tree in
    let proof_encoding :=
      Context.Proof_encoding.V1.Tree32.(Context.PROOF_ENCODING.tree_proof_encoding)
      in
    let proof_before {A : Set} (proof_value : Context.Proof.t A) : Hash.t :=
      match proof_value.(Context.Proof.t.before) with
      | (Context.Proof.KValue hash_value | Context.Proof.KNode hash_value) ⇒
        Hash.of_context_hash hash_value
      end in
    let verify_proof {A : Set}
      (p_value : Context.Proof.t Context.Proof.tree)
      (f_value : Context.tree Context.tree × A)
      : option (Context.tree × A) :=
      id Result.to_option (Context.verify_tree_proof p_value f_value) in
    let produce_proof {A B C D : Set} (function_parameter : A)
      : B C option D :=
      let '_ := function_parameter in
      fun (function_parameter : B) ⇒
        let '_ := function_parameter in
        fun (function_parameter : C) ⇒
          let '_ := function_parameter in
          None in
    {|
      P.Tree := Tree;
      P.commit_tree := commit_tree;
      P.lookup_tree := lookup_tree;
      P.proof_encoding := proof_encoding;
      P.proof_before := proof_before;
      P.verify_proof _ := verify_proof;
      P.produce_proof _ := produce_proof
    |}).

Inclusion of the module [Make_hashing_scheme_include]
Definition inbox_context :=
  Make_hashing_scheme_include.(Merkelized_operations.inbox_context).

Definition tree := Make_hashing_scheme_include.(Merkelized_operations.tree).

Definition hash_level_tree :=
  Make_hashing_scheme_include.(Merkelized_operations.hash_level_tree).

Definition new_level_tree :=
  Make_hashing_scheme_include.(Merkelized_operations.new_level_tree).

Definition add_messages_no_history :=
  Make_hashing_scheme_include.(Merkelized_operations.add_messages_no_history).

Definition get_message_payload :=
  Make_hashing_scheme_include.(Merkelized_operations.get_message_payload).

Definition form_history_proof :=
  Make_hashing_scheme_include.(Merkelized_operations.form_history_proof).

Definition take_snapshot :=
  Make_hashing_scheme_include.(Merkelized_operations.take_snapshot).

Definition inclusion_proof :=
  Make_hashing_scheme_include.(Merkelized_operations.inclusion_proof).

Definition inclusion_proof_encoding :=
  Make_hashing_scheme_include.(Merkelized_operations.inclusion_proof_encoding).

Definition pp_inclusion_proof :=
  Make_hashing_scheme_include.(Merkelized_operations.pp_inclusion_proof).

Definition number_of_proof_steps :=
  Make_hashing_scheme_include.(Merkelized_operations.number_of_proof_steps).

Definition verify_inclusion_proof :=
  Make_hashing_scheme_include.(Merkelized_operations.verify_inclusion_proof).

Definition proof := Make_hashing_scheme_include.(Merkelized_operations.proof).

Definition pp_proof :=
  Make_hashing_scheme_include.(Merkelized_operations.pp_proof).

Definition to_serialized_proof :=
  Make_hashing_scheme_include.(Merkelized_operations.to_serialized_proof).

Definition of_serialized_proof :=
  Make_hashing_scheme_include.(Merkelized_operations.of_serialized_proof).

Definition verify_proof :=
  Make_hashing_scheme_include.(Merkelized_operations.verify_proof).

Definition produce_proof :=
  Make_hashing_scheme_include.(Merkelized_operations.produce_proof).

Definition empty := Make_hashing_scheme_include.(Merkelized_operations.empty).

Definition inbox : Set := t.