Skip to main content

🦏 Sc_rollup_inbox_repr.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Sc_rollup_repr.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.

A Merkelized inbox represents a list of available messages. This list is decomposed into sublist of messages, one for each Tezos level greater than the level of the Last Cemented Commitment (LCC).
This module is designed to:
1. give a constant-time access to the number of available messages ;
2. provide a space-efficient representation for proofs of inbox inclusions (only for inboxes obtained at the end of block validation) ;
3. offer an efficient function to add a new batch of messages in the inbox at the current level.
To solve (1), we simply maintain the number of available messages in a field.
To solve (2), 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 (3), we maintain a separate proof tree C witnessing the contents of messages of the current level.
The protocol maintains the number of available messages, 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 an 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
  Error_monad.register_error_kind Error_monad.Permanent
    "sc_rollup_inbox.consume_n_messages"
    "Internal error: Trying to consume a negative number of messages"
    "Sc_rollup_inbox.consume_n_messages must be called with a non negative integer."
    None
    (Data_encoding.obj1
      (Data_encoding.req None None "n" Data_encoding.int64_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Invalid_number_of_messages_to_consume" then
          let n_value := cast int64 payload in
          Some n_value
        else None
      end)
    (fun (n_value : int64) ⇒
      Build_extensible "Invalid_number_of_messages_to_consume" int64 n_value).

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.Make Skip_list_parameters.

Definition proof_hash : Set := Context.Proof.hash.

Definition history_proof_hash : Set := Context.Proof.hash.

Definition history_proof : Set :=
  Skip_list.(Skip_list_repr.S.cell) proof_hash history_proof_hash.

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

Definition history_proof_encoding
  : Data_encoding.t
    (Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t) :=
  Skip_list.(Skip_list_repr.S.encoding) Context_hash.encoding
    Context_hash.encoding.

Definition pp_history_proof
  (fmt : Format.formatter)
  (cell_value : Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)
  : unit :=
  Format.fprintf fmt
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.String_literal "\n content = "
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.String_literal "\n index = "
            (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
              CamlinternalFormatBasics.No_padding
              CamlinternalFormatBasics.No_precision
              (CamlinternalFormatBasics.String_literal
                "\n back_pointers = "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal "\n "
                    CamlinternalFormatBasics.End_of_format)))))))
      "\n content = %a\n index = %d\n back_pointers = %a\n ")
    Context_hash.pp (Skip_list.(Skip_list_repr.S.content) cell_value)
    (Skip_list.(Skip_list_repr.S.index_value) cell_value)
    (Format.pp_print_list None Context_hash.pp)
    (Skip_list.(Skip_list_repr.S.back_pointers) cell_value).

Module t.
  Record record : Set := Build {
    rollup : Sc_rollup_repr.t;
    level : Raw_level_repr.t;
    nb_available_messages : int64;
    message_counter : Z.t;
    current_messages_hash : unit Context.Proof.hash;
    old_levels_messages : history_proof;
  }.
  Definition with_rollup rollup (r : record) :=
    Build rollup r.(level) r.(nb_available_messages) r.(message_counter)
      r.(current_messages_hash) r.(old_levels_messages).
  Definition with_level level (r : record) :=
    Build r.(rollup) level r.(nb_available_messages) r.(message_counter)
      r.(current_messages_hash) r.(old_levels_messages).
  Definition with_nb_available_messages nb_available_messages (r : record) :=
    Build r.(rollup) r.(level) nb_available_messages r.(message_counter)
      r.(current_messages_hash) r.(old_levels_messages).
  Definition with_message_counter message_counter (r : record) :=
    Build r.(rollup) r.(level) r.(nb_available_messages) message_counter
      r.(current_messages_hash) r.(old_levels_messages).
  Definition with_current_messages_hash current_messages_hash (r : record) :=
    Build r.(rollup) r.(level) r.(nb_available_messages) r.(message_counter)
      current_messages_hash r.(old_levels_messages).
  Definition with_old_levels_messages old_levels_messages (r : record) :=
    Build r.(rollup) r.(level) r.(nb_available_messages) r.(message_counter)
      r.(current_messages_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_available_messages := nb_available_messages;
      t.message_counter := message_counter;
      t.current_messages_hash := current_messages_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_available_messages
    inbox2.(t.nb_available_messages)) &&
  ((Z.equal message_counter inbox2.(t.message_counter)) &&
  ((Context_hash.equal (current_messages_hash tt)
    (inbox2.(t.current_messages_hash) tt)) &&
  (equal_history_proof old_levels_messages inbox2.(t.old_levels_messages)))))).

Definition pp (fmt : Format.formatter) (inbox : t) : unit :=
  Format.fprintf fmt
    (CamlinternalFormatBasics.Format
      (CamlinternalFormatBasics.String_literal "\n rollup = "
        (CamlinternalFormatBasics.Alpha
          (CamlinternalFormatBasics.String_literal "\n level = "
            (CamlinternalFormatBasics.Alpha
              (CamlinternalFormatBasics.String_literal
                "\n current messages hash = "
                (CamlinternalFormatBasics.Alpha
                  (CamlinternalFormatBasics.String_literal
                    "\n nb_available_messages = "
                    (CamlinternalFormatBasics.String
                      CamlinternalFormatBasics.No_padding
                      (CamlinternalFormatBasics.String_literal
                        "\n message_counter = "
                        (CamlinternalFormatBasics.Alpha
                          (CamlinternalFormatBasics.String_literal
                            "\n old_levels_messages = "
                            (CamlinternalFormatBasics.Alpha
                              (CamlinternalFormatBasics.String_literal "\n "
                                CamlinternalFormatBasics.End_of_format)))))))))))))
      "\n rollup = %a\n level = %a\n current messages hash = %a\n nb_available_messages = %s\n message_counter = %a\n old_levels_messages = %a\n ")
    Sc_rollup_repr.Address.pp inbox.(t.rollup) Raw_level_repr.pp inbox.(t.level)
    Context_hash.pp (inbox.(t.current_messages_hash) tt)
    (Int64.to_string inbox.(t.nb_available_messages)) Z.pp_print
    inbox.(t.message_counter) pp_history_proof inbox.(t.old_levels_messages).

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

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

Definition encoding : Data_encoding.encoding t :=
  Data_encoding.conv
    (fun (function_parameter : t) ⇒
      let '{|
        t.rollup := rollup;
          t.level := level;
          t.nb_available_messages := nb_available_messages;
          t.message_counter := message_counter;
          t.current_messages_hash := current_messages_hash;
          t.old_levels_messages := old_levels_messages
          |} := function_parameter in
      (rollup, message_counter, nb_available_messages, level,
        (current_messages_hash tt), old_levels_messages))
    (fun (function_parameter :
      Sc_rollup_repr.t × Z.t × int64 × Raw_level_repr.t × Context.Proof.hash ×
        history_proof) ⇒
      let
        '(rollup, message_counter, nb_available_messages, level,
          current_messages_hash, old_levels_messages) := function_parameter in
      {| t.rollup := rollup; t.level := level;
        t.nb_available_messages := nb_available_messages;
        t.message_counter := message_counter;
        t.current_messages_hash :=
          fun (function_parameter : unit) ⇒
            let '_ := function_parameter in
            current_messages_hash; t.old_levels_messages := old_levels_messages;
        |}) None
    (Data_encoding.obj6
      (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_available_messages"
        Data_encoding.int64_value)
      (Data_encoding.req None None "level" Raw_level_repr.encoding)
      (Data_encoding.req None None "current_messages_hash" Context_hash.encoding)
      (Data_encoding.req None None "old_levels_messages"
        old_levels_messages_encoding)).

Definition number_of_available_messages (inbox : t) : Z.t :=
  Z.of_int64 inbox.(t.nb_available_messages).

Definition no_messages_hash : Context_hash.t :=
  Context_hash.hash_bytes None [ Bytes.empty ].

Definition empty (rollup : Sc_rollup_repr.t) (level : Raw_level_repr.t) : t :=
  {| t.rollup := rollup; t.level := level; t.nb_available_messages := 0;
    t.message_counter := Z.zero;
    t.current_messages_hash :=
      fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        no_messages_hash;
    t.old_levels_messages :=
      Skip_list.(Skip_list_repr.S.genesis) no_messages_hash; |}.

Definition consume_n_messages (n_value : int) (function_parameter : t)
  : M? (option t) :=
  let '{| t.nb_available_messages := nb_available_messages |} as inbox :=
    function_parameter in
  if n_value <i 0 then
    Error_monad.error_value
      (Build_extensible "Invalid_number_of_messages_to_consume" int64
        (Int64.of_int n_value))
  else
    if (Int64.of_int n_value) >i64 nb_available_messages then
      return? None
    else
      let nb_available_messages :=
        nb_available_messages -i64 (Int64.of_int n_value) in
      return? (Some (t.with_nb_available_messages nb_available_messages inbox)).

Definition key_of_message : Z.t string :=
  Data_encoding.Binary.to_string_exn None Data_encoding.z_value.

Module MerkelizedOperations.
  Record signature {tree history inclusion_proof : Set} : Set := {
    tree := tree;
    messages := tree;
    message := tree;
    history := history;
    history_encoding : Data_encoding.t history;
    pp_history : Format.formatter history unit;
    history_at_genesis : int64 history;
    add_messages :
      history t Raw_level_repr.t list string messages
      M? (messages × history × t);
    add_messages_no_history :
      t Raw_level_repr.t list string messages M? (messages × t);
    get_message : messages Z.t option message;
    get_message_payload : messages Z.t option string;
    inclusion_proof := inclusion_proof;
    pp_inclusion_proof : Format.formatter inclusion_proof unit;
    number_of_proof_steps : inclusion_proof int;
    produce_inclusion_proof : history t t option inclusion_proof;
    verify_inclusion_proof : inclusion_proof t t bool;
  }.
End MerkelizedOperations.
Definition MerkelizedOperations := @MerkelizedOperations.signature.
Arguments MerkelizedOperations {_ _ _}.

Module TREE.
  Record signature {t tree : Set} : Set := {
    t := t;
    tree := tree;
    key := list string;
    value := bytes;
    find : tree key option value;
    find_tree : tree key option tree;
    add : tree key value tree;
    is_empty : tree bool;
    hash_value : tree Context_hash.t;
    __infer_t : t unit;
  }.
End TREE.
Definition TREE := @TREE.signature.
Arguments TREE {_ _}.

Module MakeHashingScheme.
  Class FArgs {P_t P_tree : Set} := {
    P : TREE (t := P_t) (tree := P_tree);
  }.
  Arguments Build_FArgs {_ _}.

  Definition Tree `{FArgs} := P.

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

  Definition messages `{FArgs} : Set := tree.

  Definition message `{FArgs} : Set := tree.

  Definition add_message `{FArgs}
    (inbox : t) (payload : string) (messages : P.(TREE.tree))
    : P.(TREE.tree) × t :=
    let message_index := inbox.(t.message_counter) in
    let message_counter := Z.succ inbox.(t.message_counter) in
    let key_value := key_of_message message_index in
    let nb_available_messages := Int64.succ inbox.(t.nb_available_messages) in
    let messages :=
      Tree.(TREE.add) messages [ key_value; "payload" ]
        (Bytes.of_string payload) in
    let inbox :=
      t.with_message_counter message_counter
        (t.with_nb_available_messages nb_available_messages inbox) in
    (messages, inbox).

  Definition get_message `{FArgs}
    (messages : P.(TREE.tree)) (message_index : Z.t) : option P.(TREE.tree) :=
    let key_value := key_of_message message_index in
    Tree.(TREE.find_tree) messages [ key_value ].

  Definition get_message_payload `{FArgs}
    (messages : P.(TREE.tree)) (message_index : Z.t) : option string :=
    let key_value := key_of_message message_index in
    Error_monad.op_gtpipeeq (Tree.(TREE.find) messages [ key_value; "payload" ])
      (Option.map Bytes.to_string).

  Definition hash_old_levels_messages `{FArgs}
    (cell_value :
      Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)
    : Context_hash.t :=
    let current_messages_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
    (let arg := Context_hash.hash_bytes in
    fun (eta : list bytes) ⇒ arg None eta)
      (List.map Context_hash.to_bytes
        (cons current_messages_hash back_pointers_hashes)).

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

  Module history.
    Record record `{FArgs} : Set := Build {
      events : Context_hash.Map.(S.INDEXES_MAP.t) history_proof;
      sequence : Int64_map.(Map.S.t) Context_hash.t;
      bound : int64;
      counter : int64;
    }.
    Definition with_events `{FArgs} events (r : record) :=
      Build _ _ _ events r.(sequence) r.(bound) r.(counter).
    Definition with_sequence `{FArgs} sequence (r : record) :=
      Build _ _ _ r.(events) sequence r.(bound) r.(counter).
    Definition with_bound `{FArgs} bound (r : record) :=
      Build _ _ _ r.(events) r.(sequence) bound r.(counter).
    Definition with_counter `{FArgs} counter (r : record) :=
      Build _ _ _ r.(events) r.(sequence) r.(bound) counter.
  End history.
  Definition history `{FArgs} := history.record.

  Definition history_encoding `{FArgs} : Data_encoding.encoding history :=
    let events_encoding :=
      Context_hash.Map.(S.INDEXES_MAP.encoding) history_proof_encoding in
    let sequence_encoding :=
      Data_encoding.conv
        (fun (m_value : Int64_map.(Map.S.t) Context_hash.t) ⇒
          Int64_map.(Map.S.bindings) m_value)
        (List.fold_left
          (fun (m_value : Int64_map.(Map.S.t) Context_hash.t) ⇒
            fun (function_parameter : Int64.t × Context_hash.t) ⇒
              let '(k_value, v_value) := function_parameter in
              Int64_map.(Map.S.add) k_value v_value m_value)
          Int64_map.(Map.S.empty)) None
        (Data_encoding.list_value None
          (Data_encoding.tup2 Data_encoding.int64_value Context_hash.encoding))
      in
    Data_encoding.conv
      (fun (function_parameter : history) ⇒
        let '{|
          history.events := events;
            history.sequence := sequence_value;
            history.bound := bound;
            history.counter := counter
            |} := function_parameter in
        (events, sequence_value, bound, counter))
      (fun (function_parameter :
        Context_hash.Map.(S.INDEXES_MAP.t) history_proof ×
          Int64_map.(Map.S.t) Context_hash.t × int64 × int64) ⇒
        let '(events, sequence_value, bound, counter) := function_parameter in
        {| history.events := events; history.sequence := sequence_value;
          history.bound := bound; history.counter := counter; |}) None
      (Data_encoding.obj4 (Data_encoding.req None None "events" events_encoding)
        (Data_encoding.req None None "sequence" sequence_encoding)
        (Data_encoding.req None None "bound" Data_encoding.int64_value)
        (Data_encoding.req None None "counter" Data_encoding.int64_value)).

  Definition pp_history `{FArgs}
    (fmt : Format.formatter) (history_value : history) : unit :=
    (fun (bindings :
      list
        (Context_hash.t ×
          Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)) ⇒
      let pp_binding
        (fmt : Format.formatter)
        (function_parameter :
          Context_hash.t ×
            Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t)
        : unit :=
        let '(hash_value, history_proof) := function_parameter in
        Format.fprintf fmt
          (CamlinternalFormatBasics.Format
            (CamlinternalFormatBasics.Formatting_gen
              (CamlinternalFormatBasics.Open_box
                (CamlinternalFormatBasics.Format
                  CamlinternalFormatBasics.End_of_format ""))
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.String_literal " -> "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Formatting_lit
                      CamlinternalFormatBasics.Close_box
                      CamlinternalFormatBasics.End_of_format))))) "@[%a -> %a@]")
          Context_hash.pp hash_value pp_history_proof history_proof in
      Format.pp_print_list None pp_binding fmt bindings)
      (Context_hash.Map.(S.INDEXES_MAP.bindings) history_value.(history.events)).

  Definition history_at_genesis `{FArgs} (bound : int64) : history :=
    {| history.events := Context_hash.Map.(S.INDEXES_MAP.empty);
      history.sequence := Int64_map.(Map.S.empty); history.bound := bound;
      history.counter := 0; |}.

[remember ptr cell history] extends [history] with a new mapping from [ptr] to [cell]. If [history] is full, the oldest mapping is removed. If the history bound is less or equal to zero, then this function returns [history] untouched.
  Definition remember `{FArgs}
    (ptr : Context_hash.t) (cell_value : history_proof)
    (history_value : history) : history :=
    if history_value.(history.bound) i64 0 then
      history_value
    else
      let events :=
        Context_hash.Map.(S.INDEXES_MAP.add) ptr cell_value
          history_value.(history.events) in
      let counter := Int64.succ history_value.(history.counter) in
      let history_value :=
        {| history.events := events;
          history.sequence :=
            Int64_map.(Map.S.add) history_value.(history.counter) ptr
              history_value.(history.sequence);
          history.bound := history_value.(history.bound);
          history.counter := counter; |} in
      if
        Int64.equal history_value.(history.counter)
          history_value.(history.bound)
      then
        match Int64_map.(Map.S.min_binding) history_value.(history.sequence)
          with
        | Nonehistory_value
        | Some (l_value, h_value)
          let sequence_value :=
            Int64_map.(Map.S.remove) l_value history_value.(history.sequence) in
          let events := Context_hash.Map.(S.INDEXES_MAP.remove) h_value events
            in
          {| history.events := events; history.sequence := sequence_value;
            history.bound := history_value.(history.bound);
            history.counter := Int64.pred history_value.(history.counter); |}
        end
      else
        history_value.

  #[bypass_check(guard)]
  Definition archive_if_needed `{FArgs}
    (history_value : history) (inbox : t)
    (target_level : Raw_level_repr.raw_level) : history × t :=
    let archive_level (history_value : history) (inbox : t) : history × t :=
      let prev_cell := inbox.(t.old_levels_messages) in
      let prev_cell_ptr := hash_old_levels_messages prev_cell in
      let history_value := remember prev_cell_ptr prev_cell history_value in
      let old_levels_messages :=
        Skip_list.(Skip_list_repr.S.next) prev_cell prev_cell_ptr
          (inbox.(t.current_messages_hash) tt) in
      let level := Raw_level_repr.succ inbox.(t.level) in
      let current_messages_hash (function_parameter : unit) : Context_hash.t :=
        let '_ := function_parameter in
        no_messages_hash in
      let inbox :=
        {| t.rollup := inbox.(t.rollup); t.level := level;
          t.nb_available_messages := inbox.(t.nb_available_messages);
          t.message_counter := Z.zero;
          t.current_messages_hash := current_messages_hash;
          t.old_levels_messages := old_levels_messages; |} in
      (history_value, inbox) in
    let fix aux (function_parameter : history × t) {struct function_parameter}
      : history × t :=
      let '(history_value, inbox) := function_parameter in
      if Raw_level_repr.op_eq inbox.(t.level) target_level then
        (history_value, inbox)
      else
        aux (archive_level history_value inbox) in
    aux (history_value, inbox).

  Definition add_messages `{FArgs}
    (history_value : history) (inbox : t) (level : Raw_level_repr.raw_level)
    (payloads : list string) (messages : P.(TREE.tree))
    : M? (P.(TREE.tree) × history × t) :=
    if Raw_level_repr.op_lt level inbox.(t.level) then
      Error_monad.fail
        (Build_extensible "Invalid_level_add_messages" Raw_level_repr.raw_level
          level)
    else
      let '(history_value, inbox) := archive_if_needed history_value inbox level
        in
      let? '(messages, inbox) :=
        List.fold_left_es
          (fun (function_parameter : P.(TREE.tree) × t) ⇒
            let '(messages, inbox) := function_parameter in
            fun (payload : string) ⇒
              Error_monad.op_gtgteq (add_message inbox payload messages)
                Error_monad._return) (messages, inbox) payloads in
      let current_messages_hash (function_parameter : unit) : Context_hash.t :=
        let '_ := function_parameter in
        if Tree.(TREE.is_empty) messages then
          no_messages_hash
        else
          Tree.(TREE.hash_value) messages in
      return?
        (messages, history_value,
          (t.with_current_messages_hash current_messages_hash inbox)).

  Definition add_messages_no_history `{FArgs}
    (inbox : t) (level : Raw_level_repr.raw_level) (payloads : list string)
    (messages : P.(TREE.tree)) : M? (P.(TREE.tree) × t) :=
    let history_value := history_at_genesis 0 in
    let? '(messages, _, inbox) :=
      add_messages history_value inbox level payloads messages in
    return? (messages, inbox).

  Definition inclusion_proof `{FArgs} : Set := list history_proof.

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

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

  Definition lift_ptr_path `{FArgs} {A B : Set}
    (history_value : 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 (history_value x_value)
          (fun (c_value : B) ⇒ aux (cons c_value accu_value) xs)
      end in
    aux nil ptr_path.

  Definition produce_inclusion_proof `{FArgs}
    (history_value : history) (inbox1 : t) (inbox2 : t)
    : option (list history_proof) :=
    let cell_ptr := hash_old_levels_messages inbox2.(t.old_levels_messages) in
    let target_index :=
      Skip_list.(Skip_list_repr.S.index_value) inbox1.(t.old_levels_messages) in
    let history_value :=
      remember cell_ptr inbox2.(t.old_levels_messages) history_value in
    let deref (ptr : Context_hash.t) : option history_proof :=
      Context_hash.Map.(S.INDEXES_MAP.find_opt) ptr
        history_value.(history.events) in
    Option.join
      (Option.map (lift_ptr_path deref)
        (Skip_list.(Skip_list_repr.S.back_path) deref cell_ptr target_index)).

  Definition verify_inclusion_proof `{FArgs}
    (proof :
      list (Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t))
    (inbox1 : t) (inbox2 : t) : bool :=
    let assoc :=
      List.map
        (fun (c_value :
          Skip_list.(Skip_list_repr.S.cell) Context_hash.t Context_hash.t) ⇒
          ((hash_old_levels_messages c_value), c_value)) proof in
    let path := Pervasives.fst (List.split assoc) in
    let deref :=
      let map := Context_hash.Map.(S.INDEXES_MAP.of_seq) (List.to_seq assoc) in
      fun (ptr : Context_hash.t) ⇒
        Context_hash.Map.(S.INDEXES_MAP.find_opt) ptr map in
    let cell_ptr := hash_old_levels_messages inbox2.(t.old_levels_messages) in
    let target_ptr := hash_old_levels_messages inbox1.(t.old_levels_messages) in
    Skip_list.(Skip_list_repr.S.valid_back_path) Context_hash.equal deref
      cell_ptr target_ptr path.

  (* MakeHashingScheme *)
  Definition functor `{FArgs} :=
    {|
      MerkelizedOperations.history_encoding := history_encoding;
      MerkelizedOperations.pp_history := pp_history;
      MerkelizedOperations.history_at_genesis := history_at_genesis;
      MerkelizedOperations.add_messages := add_messages;
      MerkelizedOperations.add_messages_no_history := add_messages_no_history;
      MerkelizedOperations.get_message := get_message;
      MerkelizedOperations.get_message_payload := get_message_payload;
      MerkelizedOperations.pp_inclusion_proof := pp_inclusion_proof;
      MerkelizedOperations.number_of_proof_steps := number_of_proof_steps;
      MerkelizedOperations.produce_inclusion_proof := produce_inclusion_proof;
      MerkelizedOperations.verify_inclusion_proof := verify_inclusion_proof
    |}.
End MakeHashingScheme.
Definition MakeHashingScheme {P_t P_tree : Set}
  (P : TREE (t := P_t) (tree := P_tree))
  : MerkelizedOperations (tree := P.(TREE.tree)) (history := _)
    (inclusion_proof := _) :=
  let '_ := MakeHashingScheme.Build_FArgs P in
  MakeHashingScheme.functor.

Definition MakeHashingScheme_include :
  MerkelizedOperations (tree := Context.tree) (history := _)
    (inclusion_proof := _) :=
  MakeHashingScheme
    (let find := Context.Tree.(Context.TREE.find) in
    let find_tree := Context.Tree.(Context.TREE.find_tree) in
    let add := Context.Tree.(Context.TREE.add) in
    let is_empty := Context.Tree.(Context.TREE.is_empty) in
    let hash_value := Context.Tree.(Context.TREE.hash_value) in
    let t : Set := Context.t in
    let tree : Set := Context.tree in
    let value : Set := bytes in
    let key : Set := list string in
    let __infer_t (function_parameter : t) : unit :=
      let '_ := function_parameter in
      tt in
    {|
      TREE.find := find;
      TREE.find_tree := find_tree;
      TREE.add := add;
      TREE.is_empty := is_empty;
      TREE.hash_value := hash_value;
      TREE.__infer_t := __infer_t
    |}).

Inclusion of the module [MakeHashingScheme_include]
Definition tree := MakeHashingScheme_include.(MerkelizedOperations.tree).

Definition messages :=
  MakeHashingScheme_include.(MerkelizedOperations.messages).

Definition message := MakeHashingScheme_include.(MerkelizedOperations.message).

Definition history := MakeHashingScheme_include.(MerkelizedOperations.history).

Definition history_encoding :=
  MakeHashingScheme_include.(MerkelizedOperations.history_encoding).

Definition pp_history :=
  MakeHashingScheme_include.(MerkelizedOperations.pp_history).

Definition history_at_genesis :=
  MakeHashingScheme_include.(MerkelizedOperations.history_at_genesis).

Definition add_messages :=
  MakeHashingScheme_include.(MerkelizedOperations.add_messages).

Definition add_messages_no_history :=
  MakeHashingScheme_include.(MerkelizedOperations.add_messages_no_history).

Definition get_message :=
  MakeHashingScheme_include.(MerkelizedOperations.get_message).

Definition get_message_payload :=
  MakeHashingScheme_include.(MerkelizedOperations.get_message_payload).

Definition inclusion_proof :=
  MakeHashingScheme_include.(MerkelizedOperations.inclusion_proof).

Definition pp_inclusion_proof :=
  MakeHashingScheme_include.(MerkelizedOperations.pp_inclusion_proof).

Definition number_of_proof_steps :=
  MakeHashingScheme_include.(MerkelizedOperations.number_of_proof_steps).

Definition produce_inclusion_proof :=
  MakeHashingScheme_include.(MerkelizedOperations.produce_inclusion_proof).

Definition verify_inclusion_proof :=
  MakeHashingScheme_include.(MerkelizedOperations.verify_inclusion_proof).