Skip to main content

🍲 Dal_slot_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.Environment.V8.
Require TezosOfOCaml.Proto_alpha.Bounded_history_repr.
Require TezosOfOCaml.Proto_alpha.Merkle_list.
Require TezosOfOCaml.Proto_alpha.Raw_level_repr.
Require TezosOfOCaml.Proto_alpha.Skip_list_repr.

Definition parameters : Set := Dal.parameters.

Definition parameters_encoding : Data_encoding.t Dal.parameters :=
  Dal.parameters_encoding.

Module Commitment.
  Definition t : Set := Dal.commitment.

  Definition equal : Dal.commitment Dal.commitment bool :=
    Dal.Commitment.equal.

  Definition encoding : Data_encoding.t Dal.commitment :=
    Dal.Commitment.encoding.

  Definition pp (ppf : Format.formatter) (commitment : Dal.commitment) : unit :=
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String CamlinternalFormatBasics.No_padding
          CamlinternalFormatBasics.End_of_format) "%s")
      (Dal.Commitment.to_b58check commitment).

  Definition zero : Dal.commitment := Dal.Commitment.zero.
End Commitment.

Module Index.
  Definition t : Set := int.

  Definition max_value : int := 255.

  Definition encoding : Data_encoding.encoding int := Data_encoding.uint8.

  Definition pp : Format.formatter int unit := Format.pp_print_int.

  Definition zero : int := 0.

  Definition of_int (slot_index : int) : option int :=
    if (slot_index i max_value) && (slot_index i zero) then
      Some slot_index
    else
      None.

  Definition to_int {A : Set} (slot_index : A) : A := slot_index.

  Definition compare : int int int := Compare.Int.compare.

  Definition equal : int int bool := Compare.Int.equal.
End Index.

Module Header.
  Module id.
    Record record : Set := Build {
      published_level : Raw_level_repr.t;
      index : Index.t;
    }.
    Definition with_published_level published_level (r : record) :=
      Build published_level r.(index).
    Definition with_index index (r : record) :=
      Build r.(published_level) index.
  End id.
  Definition id := id.record.

  Module t.
    Record record : Set := Build {
      id : id;
      commitment : Commitment.t;
    }.
    Definition with_id id (r : record) :=
      Build id r.(commitment).
    Definition with_commitment commitment (r : record) :=
      Build r.(id) commitment.
  End t.
  Definition t := t.record.

  Definition slot_id_equal (function_parameter : id) : id bool :=
    let '{| id.published_level := published_level; id.index := index_value |} :=
      function_parameter in
    fun (s2 : id) ⇒
      (Raw_level_repr.equal published_level s2.(id.published_level)) &&
      (Index.equal index_value s2.(id.index)).

  Definition equal (function_parameter : t) : t bool :=
    let '{| t.id := id; t.commitment := commitment |} := function_parameter in
    fun (s2 : t) ⇒
      (slot_id_equal id s2.(t.id)) &&
      (Commitment.equal commitment s2.(t.commitment)).

  Definition compare_slot_id (function_parameter : id) : id int :=
    let '{| id.published_level := published_level; id.index := index_value |} :=
      function_parameter in
    fun (s2 : id) ⇒
      let c_value :=
        Raw_level_repr.compare published_level s2.(id.published_level) in
      if c_value i 0 then
        c_value
      else
        Index.compare index_value s2.(id.index).

  Definition zero_id : id :=
    {| id.published_level := Raw_level_repr.root_value; id.index := Index.zero;
      |}.

  Definition zero : t :=
    {| t.id := zero_id; t.commitment := Commitment.zero; |}.

  Definition id_encoding : Data_encoding.encoding id :=
    Data_encoding.conv
      (fun (function_parameter : id) ⇒
        let '{|
          id.published_level := published_level; id.index := index_value |} :=
          function_parameter in
        (published_level, index_value))
      (fun (function_parameter : Raw_level_repr.t × Index.t) ⇒
        let '(published_level, index_value) := function_parameter in
        {| id.published_level := published_level; id.index := index_value; |})
      None
      (Data_encoding.obj2
        (Data_encoding.req None None "level" Raw_level_repr.encoding)
        (Data_encoding.req None None "index" Data_encoding.uint8)).

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{| t.id := id; t.commitment := commitment |} := function_parameter
          in
        (id, commitment))
      (fun (function_parameter : id × Commitment.t) ⇒
        let '(id, commitment) := function_parameter in
        {| t.id := id; t.commitment := commitment; |}) None
      (Data_encoding.merge_objs id_encoding
        (Data_encoding.obj1
          (Data_encoding.req None None "commitment" Commitment.encoding))).

  Definition pp_id (fmt : Format.formatter) (function_parameter : id) : unit :=
    let '{| id.published_level := published_level; id.index := index_value |} :=
      function_parameter in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "published_level: "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.String_literal ", index: "
              (CamlinternalFormatBasics.Alpha
                CamlinternalFormatBasics.End_of_format))))
        "published_level: %a, index: %a") Raw_level_repr.pp published_level
      Format.pp_print_int index_value.

  Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
    let '{| t.id := id; t.commitment := c_value |} := function_parameter in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "id:("
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.String_literal "), commitment: "
              (CamlinternalFormatBasics.Alpha
                CamlinternalFormatBasics.End_of_format))))
        "id:(%a), commitment: %a") pp_id id Commitment.pp c_value.
End Header.

Module Dal_slot_repr_Index := Index.

Module Page.
  Definition content : Set := Bytes.t.

  Definition slot_index : Set := Index.t.

  Definition pages_per_slot : Dal.parameters int := Dal.pages_per_slot.

  Module Index.
    Definition t : Set := int.

    Definition zero : int := 0.

    Definition encoding : Data_encoding.encoding int := Data_encoding.int16.

    Definition pp : Format.formatter int unit := Format.pp_print_int.

    Definition compare : int int int := Compare.Int.compare.

    Definition equal : int int bool := Compare.Int.equal.
  End Index.

  Module t.
    Record record : Set := Build {
      slot_id : Header.id;
      page_index : Index.t;
    }.
    Definition with_slot_id slot_id (r : record) :=
      Build slot_id r.(page_index).
    Definition with_page_index page_index (r : record) :=
      Build r.(slot_id) page_index.
  End t.
  Definition t := t.record.

  Definition proof : Set := Dal.page_proof.

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{|
          t.slot_id := {|
            Header.id.published_level := published_level;
              Header.id.index := index_value
              |};
            t.page_index := page_index
            |} := function_parameter in
        (published_level, index_value, page_index))
      (fun (function_parameter : Raw_level_repr.t × Index.t × Index.t) ⇒
        let '(published_level, index_value, page_index) := function_parameter in
        {|
          t.slot_id :=
            {| Header.id.published_level := published_level;
              Header.id.index := index_value; |}; t.page_index := page_index; |})
      None
      (Data_encoding.obj3
        (Data_encoding.req None None "published_level" Raw_level_repr.encoding)
        (Data_encoding.req None None "slot_index" Dal_slot_repr_Index.encoding)
        (Data_encoding.req None None "page_index" Index.encoding)).

  Definition equal (function_parameter : t) : t bool :=
    let '{| t.slot_id := slot_id; t.page_index := page_index |} :=
      function_parameter in
    fun (p_value : t) ⇒
      (Header.slot_id_equal slot_id p_value.(t.slot_id)) &&
      (Index.equal page_index p_value.(t.page_index)).

  Definition proof_encoding : Data_encoding.t Dal.page_proof :=
    Dal.page_proof_encoding.

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

  Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
    let '{|
      t.slot_id := {|
        Header.id.published_level := published_level;
          Header.id.index := index_value
          |};
        t.page_index := page_index
        |} := function_parameter in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "(published_level: "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.String_literal ", slot_index: "
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.String_literal ", page_index: "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.Char_literal ")" % char
                      CamlinternalFormatBasics.End_of_format)))))))
        "(published_level: %a, slot_index: %a, page_index: %a)")
      Raw_level_repr.pp published_level Dal_slot_repr_Index.pp index_value
      Index.pp page_index.

  Definition pp_proof (fmt : Format.formatter) (proof_value : Dal.page_proof)
    : unit :=
    Data_encoding.Json.pp fmt
      (Data_encoding.Json.construct None proof_encoding proof_value).
End Page.

Module Slot_market.
  Definition Slot_index_map :=
    Map.Make
      {|
        Compare.COMPARABLE.compare := Index.compare
      |}.

  Module t.
    Record record : Set := Build {
      length : int;
      slot_headers : Slot_index_map.(Map.S.t) Header.t;
    }.
    Definition with_length length (r : record) :=
      Build length r.(slot_headers).
    Definition with_slot_headers slot_headers (r : record) :=
      Build r.(length) slot_headers.
  End t.
  Definition t := t.record.

  Definition init_value (length : int) : t :=
    let '_ :=
      if length <i 0 then
        Pervasives.invalid_arg
          "Dal_slot_repr.Slot_market.init: length cannot be negative"
      else
        tt in
    let slot_headers {A : Set} : Slot_index_map.(Map.S.t) A :=
      Slot_index_map.(Map.S.empty) in
    {| t.length := length; t.slot_headers := slot_headers; |}.

  Definition length (function_parameter : t) : int :=
    let '{| t.length := length |} := function_parameter in
    length.

  Definition register (t_value : t) (new_slot_header : Header.t)
    : option (t × bool) :=
    if
      Pervasives.not
        ((0 i new_slot_header.(Header.t.id).(Header.id.index)) &&
        (new_slot_header.(Header.t.id).(Header.id.index) <i t_value.(t.length)))
    then
      None
    else
      let has_changed := Pervasives.ref_value false in
      let update (function_parameter : option Header.t) : option Header.t :=
        match function_parameter with
        | None
          let '_ := Pervasives.op_coloneq has_changed true in
          Some new_slot_header
        | Some x_valueSome x_value
        end in
      let slot_headers :=
        Slot_index_map.(Map.S.update)
          new_slot_header.(Header.t.id).(Header.id.index) update
          t_value.(t.slot_headers) in
      let t_value := t.with_slot_headers slot_headers t_value in
      Some (t_value, (Pervasives.op_exclamation has_changed)).

  Definition candidates (t_value : t) : list Header.t :=
    List.of_seq
      (Seq.map Pervasives.snd
        (Slot_index_map.(Map.S.to_seq) t_value.(t.slot_headers))).
End Slot_market.

Module History.
  Module Leaf.
    Definition t : Set := Header.t.

    Definition to_bytes : Header.t bytes :=
      Data_encoding.Binary.to_bytes_exn None Header.encoding.

    (* Leaf *)
    Definition module :=
      {|
        Merkle_list.S_El.to_bytes := to_bytes
      |}.
  End Leaf.
  Definition Leaf := Leaf.module.

  Module Content_prefix.
    Definition _prefix : string := "dash1".

    Definition b58check_prefix : string :=
      String.String "002" (String.String "224" ("H^" ++ String.String "219" "")).

    Definition size_value : option int := Some 32.

    Definition name : string := "dal_skip_list_content".

    Definition title : string :=
      "A hash to represent the content of a cell in the skip list".
  End Content_prefix.

  Definition Content_hash :=
    Blake2B.Make
      {|
        Blake2B.Register.register_encoding _ := Base58.register_encoding
      |}
      {|
        Blake2B.PrefixedName.name := Content_prefix.name;
        Blake2B.PrefixedName.title := Content_prefix.title;
        Blake2B.PrefixedName.size_value := Content_prefix.size_value;
        Blake2B.PrefixedName.b58check_prefix := Content_prefix.b58check_prefix
      |}.

  Definition Merkle_list := Merkle_list.Make Leaf Content_hash.

  Module Pointer_prefix.
    Definition _prefix : string := "dask1".

    Definition b58check_prefix : string :=
      String.String "002" (String.String "224" "Hs").

    Definition size_value : option int := Some 32.

    Definition name : string := "dal_skip_list_pointer".

    Definition title : string :=
      "A hash that represents the skip list pointers".
  End Pointer_prefix.

  Module Pointer_hash.
    Definition Blake2B_Make_include :=
      Blake2B.Make
        {|
          Blake2B.Register.register_encoding _ := Base58.register_encoding
        |}
        {|
          Blake2B.PrefixedName.name := Pointer_prefix.name;
          Blake2B.PrefixedName.title := Pointer_prefix.title;
          Blake2B.PrefixedName.size_value := Pointer_prefix.size_value;
          Blake2B.PrefixedName.b58check_prefix := Pointer_prefix.b58check_prefix
        |}.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

    Definition _sig_KEY : unit := tt.
  End Pointer_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.

Init function; without side-effects in Coq
  Definition init_module1 : unit :=
    Error_monad.register_error_kind Error_monad.Temporary
      "Dal_slot_repr.add_element_in_slots_skip_list_violates_ordering"
      "Add an element in slots skip list that violates ordering"
      "Attempting to add an element on top of the Dal confirmed slots skip list that violates the ordering."
      None Data_encoding.unit_value
      (fun (function_parameter : Error_monad._error) ⇒
        match function_parameter with
        | Build_extensible tag _ payload
          if String.eqb tag "Add_element_in_slots_skip_list_violates_ordering"
            then
            Some tt
          else None
        end)
      (fun (function_parameter : unit) ⇒
        let '_ := function_parameter in
        Build_extensible "Add_element_in_slots_skip_list_violates_ordering" unit
          tt).

  Module Skip_list.
    Definition Skip_list := Skip_list_repr.Make Skip_list_parameters.

Inclusion of the module [Skip_list]
    Definition cell := Skip_list.(Skip_list_repr.S.cell).

    Definition pp {ptr content : Set} :=
      Skip_list.(Skip_list_repr.S.pp) (ptr := ptr) (content := content).

    Definition equal {ptr content : Set} :=
      Skip_list.(Skip_list_repr.S.equal) (ptr := ptr) (content := content).

    Definition encoding {ptr content : Set} :=
      Skip_list.(Skip_list_repr.S.encoding) (ptr := ptr) (content := content).

    Definition index_value {content ptr : Set} :=
      Skip_list.(Skip_list_repr.S.index_value) (content := content) (ptr := ptr).

    Definition content {content ptr : Set} :=
      Skip_list.(Skip_list_repr.S.content) (content := content) (ptr := ptr).

    Definition back_pointer {content ptr : Set} :=
      Skip_list.(Skip_list_repr.S.back_pointer) (content := content)
        (ptr := ptr).

    Definition back_pointers {content ptr : Set} :=
      Skip_list.(Skip_list_repr.S.back_pointers) (content := content)
        (ptr := ptr).

    Definition genesis {content ptr : Set} :=
      Skip_list.(Skip_list_repr.S.genesis) (content := content) (ptr := ptr).

    Definition find {ptr content : Set} :=
      Skip_list.(Skip_list_repr.S.find) (ptr := ptr) (content := content).

    Definition back_path {ptr content : Set} :=
      Skip_list.(Skip_list_repr.S.back_path) (ptr := ptr) (content := content).

    Definition valid_back_path {ptr content : Set} :=
      Skip_list.(Skip_list_repr.S.valid_back_path) (ptr := ptr)
        (content := content).

    Definition search_cell_result :=
      Skip_list.(Skip_list_repr.S.search_cell_result).

    Definition search_result := Skip_list.(Skip_list_repr.S.search_result).

    Definition pp_search_result {ptr content : Set} :=
      Skip_list.(Skip_list_repr.S.pp_search_result) (ptr := ptr)
        (content := content).

    Definition next {A : Set}
      (prev_cell : cell Header.t A) (prev_cell_ptr : A) (elt_value : Header.t)
      : M? (Skip_list.(Skip_list_repr.S.cell) Header.t A) :=
      let? '_ :=
        Error_monad.error_when
          ((Header.compare_slot_id elt_value.(Header.t.id)
            (content prev_cell).(Header.t.id)) i 0)
          (Build_extensible "Add_element_in_slots_skip_list_violates_ordering"
            unit tt) in
      return?
        (Skip_list.(Skip_list_repr.S.next) prev_cell prev_cell_ptr elt_value).

    Definition search {A : Set}
      (deref : A option (Skip_list.(Skip_list_repr.S.cell) Header.t A))
      (cell_value : Skip_list.(Skip_list_repr.S.cell) Header.t A)
      (target_id : Header.id)
      : Skip_list.(Skip_list_repr.S.search_result) Header.t A :=
      Skip_list.(Skip_list_repr.S.search) deref
        (fun (slot : Header.t) ⇒
          Header.compare_slot_id slot.(Header.t.id) target_id) cell_value.
  End Skip_list.

  Module V1.
    Definition content : Set := Header.t.

    Definition ptr : Set := Pointer_hash.t.

    Definition history : Set := Skip_list.cell content ptr.

    Definition t : Set := history.

    Definition history_encoding : Data_encoding.t history :=
      Skip_list.encoding Pointer_hash.encoding Header.encoding.

    Definition equal_history : history history bool :=
      Skip_list.equal Pointer_hash.equal Header.equal.

    Definition encoding : Data_encoding.t history := history_encoding.

    Definition equal : t t bool := equal_history.

    Definition genesis : t := Skip_list.genesis Header.zero.

    Definition hash_skip_list_cell (cell_value : history) : Pointer_hash.t :=
      let current_slot := Skip_list.content cell_value in
      let back_pointers_hashes := Skip_list.back_pointers cell_value in
      Pointer_hash.hash_bytes None
        (cons
          (Data_encoding.Binary.to_bytes_exn None Header.encoding current_slot)
          (List.map Pointer_hash.to_bytes back_pointers_hashes)).

    Definition pp_history (fmt : Format.formatter) (history_value : history)
      : 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@]") Pointer_hash.pp history_hash
        (Skip_list.pp Pointer_hash.pp Header.pp) history_value.

    Definition History_cache :=
      Bounded_history_repr.Make
        (let name := "dal_slots_cache" in
        let _sig_NAME := tt in
        {|
          Bounded_history_repr.NAME.name := name;
          Bounded_history_repr.NAME._sig_NAME := _sig_NAME
        |})
        {|
          Bounded_history_repr.KEY.compare := Pointer_hash.compare;
          Bounded_history_repr.KEY.pp := Pointer_hash.pp;
          Bounded_history_repr.KEY.encoding := Pointer_hash.encoding;
          Bounded_history_repr.KEY._sig_KEY := Pointer_hash._sig_KEY
        |}
        (let t : Set := history in
        let encoding := history_encoding in
        let pp := pp_history in
        let equal := equal_history in
        {|
          Bounded_history_repr.VALUE.equal := equal;
          Bounded_history_repr.VALUE.pp := pp;
          Bounded_history_repr.VALUE.encoding := encoding
        |}).

    Definition add_confirmed_slot_header
      (function_parameter : history × History_cache.(Bounded_history_repr.S.t))
      : content
      M?
        (Skip_list.Skip_list.(Skip_list_repr.S.cell) content ptr ×
          History_cache.(Bounded_history_repr.S.t)) :=
      let '(t_value, cache) := function_parameter in
      fun (slot_header : content) ⇒
        let prev_cell_ptr := hash_skip_list_cell t_value in
        let? cache :=
          History_cache.(Bounded_history_repr.S.remember) prev_cell_ptr t_value
            cache in
        let? new_cell := Skip_list.next t_value prev_cell_ptr slot_header in
        return? (new_cell, cache).

    Definition add_confirmed_slot_headers
      (t_value : t) (cache : History_cache.(Bounded_history_repr.S.t))
      (slot_headers : list content)
      : M? (history × History_cache.(Bounded_history_repr.S.t)) :=
      List.fold_left_e add_confirmed_slot_header (t_value, cache) slot_headers.

    Definition add_confirmed_slot_headers_no_cache
      : history list content M? history :=
      let no_cache := History_cache.(Bounded_history_repr.S.empty) 0 in
      fun (t_value : history) ⇒
        fun (slots : list content) ⇒
          Error_monad.op_gtpipequestion
            (List.fold_left_e add_confirmed_slot_header (t_value, no_cache)
              slots) Pervasives.fst.

An inclusion proof, for a page ID, is a list of the slots' history skip list's cells that encodes a minimal path: from a starting cell, which serves as a reference. It is usually called 'snapshot' below, to a final cell, that is either the exact target cell in case the slot of the page is confirmed, or a cell whose slot ID is the smallest that directly follows the page's slot id, in case the target slot is not confirmed.
Using the starting cell as a trustable starting point (i.e. maintained and provided by L1), and combined with the extra information stored in the {!proof} type below, one can verify if a slot (and then a page of that slot) is confirmed on L1 or not.
    Definition inclusion_proof : Set := list history.

(See the documentation in the mli file to understand what we want to prove in game refutation involving Dal and why.)
A Dal proof is an algebraic datatype with two cases, where we basically prove that a Dal page is confirmed on L1 or not. Being 'not confirmed' here includes the case where the slot's header is not published and the case where the slot's header is published, but the endorsers didn't confirm the availability of its data.
To produce a proof representation for a page (see function {!produce_proof_repr} below), we assume given: - [page_id], identifies the page; - [slots_history], a current/recent cell of the slots history skip list. Typically, it should be the skip list cell snapshotted when starting the refutation game; - [history_cache], a sufficiently large slots history cache, to navigate back through the successive cells of the skip list. Typically, the cache should at least contain the cell whose slot ID is [page_id.slot_id] in case the page is confirmed, or the cell whose slot ID is immediately after [page_id.slot_id] in case of an unconfirmed page. Indeed, inclusion proofs encode paths through skip lists' cells where the head is the reference/snapshot cell and the last element is the target slot in or the nearest upper slot (w.r.t [page_id]'s slot id and to skip list elements ordering) ; - [page_info], that provides the page's information (the content and the slot membership proof) for page_id. In case the page is supposed to be confirmed, this argument should contain the page's content and the proof that the page is part of the (confirmed) slot whose ID is given in [page_id]. In case we want to show that the page is not confirmed, the value [page_info] should be [None].
[dal_parameters] is used when verifying that/if the page is part of the candidate slot (if any). Records for the constructor parameters
    Module ConstructorRecords_proof_repr.
      Module proof_repr.
        Module Page_confirmed.
          Record record {target_cell inc_proof page_data page_proof : Set} : Set := Build {
            target_cell : target_cell;
            inc_proof : inc_proof;
            page_data : page_data;
            page_proof : page_proof;
          }.
          Arguments record : clear implicits.
          Definition with_target_cell
            {t_target_cell t_inc_proof t_page_data t_page_proof} target_cell
            (r : record t_target_cell t_inc_proof t_page_data t_page_proof) :=
            Build t_target_cell t_inc_proof t_page_data t_page_proof target_cell
              r.(inc_proof) r.(page_data) r.(page_proof).
          Definition with_inc_proof
            {t_target_cell t_inc_proof t_page_data t_page_proof} inc_proof
            (r : record t_target_cell t_inc_proof t_page_data t_page_proof) :=
            Build t_target_cell t_inc_proof t_page_data t_page_proof
              r.(target_cell) inc_proof r.(page_data) r.(page_proof).
          Definition with_page_data
            {t_target_cell t_inc_proof t_page_data t_page_proof} page_data
            (r : record t_target_cell t_inc_proof t_page_data t_page_proof) :=
            Build t_target_cell t_inc_proof t_page_data t_page_proof
              r.(target_cell) r.(inc_proof) page_data r.(page_proof).
          Definition with_page_proof
            {t_target_cell t_inc_proof t_page_data t_page_proof} page_proof
            (r : record t_target_cell t_inc_proof t_page_data t_page_proof) :=
            Build t_target_cell t_inc_proof t_page_data t_page_proof
              r.(target_cell) r.(inc_proof) r.(page_data) page_proof.
        End Page_confirmed.
        Definition Page_confirmed_skeleton := Page_confirmed.record.

        Module Page_unconfirmed.
          Record record {prev_cell next_cell_opt next_inc_proof : Set} : Set := Build {
            prev_cell : prev_cell;
            next_cell_opt : next_cell_opt;
            next_inc_proof : next_inc_proof;
          }.
          Arguments record : clear implicits.
          Definition with_prev_cell
            {t_prev_cell t_next_cell_opt t_next_inc_proof} prev_cell
            (r : record t_prev_cell t_next_cell_opt t_next_inc_proof) :=
            Build t_prev_cell t_next_cell_opt t_next_inc_proof prev_cell
              r.(next_cell_opt) r.(next_inc_proof).
          Definition with_next_cell_opt
            {t_prev_cell t_next_cell_opt t_next_inc_proof} next_cell_opt
            (r : record t_prev_cell t_next_cell_opt t_next_inc_proof) :=
            Build t_prev_cell t_next_cell_opt t_next_inc_proof r.(prev_cell)
              next_cell_opt r.(next_inc_proof).
          Definition with_next_inc_proof
            {t_prev_cell t_next_cell_opt t_next_inc_proof} next_inc_proof
            (r : record t_prev_cell t_next_cell_opt t_next_inc_proof) :=
            Build t_prev_cell t_next_cell_opt t_next_inc_proof r.(prev_cell)
              r.(next_cell_opt) next_inc_proof.
        End Page_unconfirmed.
        Definition Page_unconfirmed_skeleton := Page_unconfirmed.record.
      End proof_repr.
    End ConstructorRecords_proof_repr.
    Import ConstructorRecords_proof_repr.

    Reserved Notation "'proof_repr.Page_confirmed".
    Reserved Notation "'proof_repr.Page_unconfirmed".

    Inductive proof_repr : Set :=
    | Page_confirmed : 'proof_repr.Page_confirmed proof_repr
    | Page_unconfirmed : 'proof_repr.Page_unconfirmed proof_repr
    
    where "'proof_repr.Page_confirmed" :=
      (proof_repr.Page_confirmed_skeleton history inclusion_proof Page.content
        Page.proof)
    and "'proof_repr.Page_unconfirmed" :=
      (proof_repr.Page_unconfirmed_skeleton history (option history)
        inclusion_proof).

    Module proof_repr.
      Include ConstructorRecords_proof_repr.proof_repr.
      Definition Page_confirmed := 'proof_repr.Page_confirmed.
      Definition Page_unconfirmed := 'proof_repr.Page_unconfirmed.
    End proof_repr.

    Definition proof_repr_encoding : Data_encoding.encoding proof_repr :=
      let case_page_confirmed : Data_encoding.case proof_repr :=
        Data_encoding.case_value "confirmed dal page proof representation" None
          (Data_encoding.Tag 0)
          (Data_encoding.obj5
            (Data_encoding.req None None "kind"
              (Data_encoding.constant "confirmed"))
            (Data_encoding.req None None "target_cell" history_encoding)
            (Data_encoding.req None None "inc_proof"
              (Data_encoding.list_value None history_encoding))
            (Data_encoding.req None None "page_data" Data_encoding.bytes_value)
            (Data_encoding.req None None "page_proof" Page.proof_encoding))
          (fun (function_parameter : proof_repr) ⇒
            match function_parameter with
            |
              Page_confirmed {|
                proof_repr.Page_confirmed.target_cell := target_cell;
                  proof_repr.Page_confirmed.inc_proof := inc_proof;
                  proof_repr.Page_confirmed.page_data := page_data;
                  proof_repr.Page_confirmed.page_proof := page_proof
                  |} ⇒ Some (tt, target_cell, inc_proof, page_data, page_proof)
            | _None
            end)
          (fun (function_parameter :
            unit × history × inclusion_proof × Bytes.t × Dal.page_proof) ⇒
            let '(_, target_cell, inc_proof, page_data, page_proof) :=
              function_parameter in
            Page_confirmed
              {| proof_repr.Page_confirmed.target_cell := target_cell;
                proof_repr.Page_confirmed.inc_proof := inc_proof;
                proof_repr.Page_confirmed.page_data := page_data;
                proof_repr.Page_confirmed.page_proof := page_proof; |})
      in let case_page_unconfirmed : Data_encoding.case proof_repr :=
        Data_encoding.case_value "unconfirmed dal page proof representation"
          None (Data_encoding.Tag 1)
          (Data_encoding.obj4
            (Data_encoding.req None None "kind"
              (Data_encoding.constant "unconfirmed"))
            (Data_encoding.req None None "prev_cell" history_encoding)
            (Data_encoding.req None None "next_cell_opt"
              (Data_encoding.option_value history_encoding))
            (Data_encoding.req None None "next_inc_proof"
              (Data_encoding.list_value None history_encoding)))
          (fun (function_parameter : proof_repr) ⇒
            match function_parameter with
            |
              Page_unconfirmed {|
                proof_repr.Page_unconfirmed.prev_cell := prev_cell;
                  proof_repr.Page_unconfirmed.next_cell_opt := next_cell_opt;
                  proof_repr.Page_unconfirmed.next_inc_proof := next_inc_proof
                  |} ⇒ Some (tt, prev_cell, next_cell_opt, next_inc_proof)
            | _None
            end)
          (fun (function_parameter :
            unit × history × option history × inclusion_proof) ⇒
            let '(_, prev_cell, next_cell_opt, next_inc_proof) :=
              function_parameter in
            Page_unconfirmed
              {| proof_repr.Page_unconfirmed.prev_cell := prev_cell;
                proof_repr.Page_unconfirmed.next_cell_opt := next_cell_opt;
                proof_repr.Page_unconfirmed.next_inc_proof := next_inc_proof; |})
        in
      Data_encoding.union None [ case_page_confirmed; case_page_unconfirmed ].

    Definition proof : Set := bytes.

DAL/FIXME: https://gitlab.com/tezos/tezos/-/issues/4084 DAL proof's encoding should be bounded
Init function; without side-effects in Coq
    Definition init_module2 : unit :=
      Error_monad.register_error_kind Error_monad.Permanent
        "Dal_slot_repr.invalid_proof_serialization"
        "Dal invalid proof serialization"
        "Error occured during dal proof serialization" None
        Data_encoding.unit_value
        (fun (function_parameter : Error_monad._error) ⇒
          match function_parameter with
          | Build_extensible tag _ payload
            if String.eqb tag "Dal_invalid_proof_serialization" then
              Some tt
            else None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Build_extensible "Dal_invalid_proof_serialization" unit tt).

    Definition serialize_proof (proof_value : proof_repr) : M? bytes :=
      match
        Data_encoding.Binary.to_bytes_opt None proof_repr_encoding proof_value
        with
      | None
        Error_monad.error_value
          (Build_extensible "Dal_invalid_proof_serialization" unit tt)
      | Some serialized_proofreturn? serialized_proof
      end.

Init function; without side-effects in Coq
    Definition init_module3 : unit :=
      Error_monad.register_error_kind Error_monad.Permanent
        "Dal_slot_repr.invalid_proof_deserialization"
        "Dal invalid proof deserialization"
        "Error occured during dal proof deserialization" None
        Data_encoding.unit_value
        (fun (function_parameter : Error_monad._error) ⇒
          match function_parameter with
          | Build_extensible tag _ payload
            if String.eqb tag "Dal_invalid_proof_deserialization" then
              Some tt
            else None
          end)
        (fun (function_parameter : unit) ⇒
          let '_ := function_parameter in
          Build_extensible "Dal_invalid_proof_deserialization" unit tt).

    Definition deserialize_proof (proof_value : bytes) : M? proof_repr :=
      match Data_encoding.Binary.of_bytes_opt proof_repr_encoding proof_value
        with
      | None
        Error_monad.error_value
          (Build_extensible "Dal_invalid_proof_deserialization" unit tt)
      | Some deserialized_proofreturn? deserialized_proof
      end.

    Definition pp_inclusion_proof : Format.formatter list history unit :=
      Format.pp_print_list None pp_history.

    Definition pp_history_opt : Format.formatter option history unit :=
      Format.pp_print_option None pp_history.

    Definition pp_proof
      (serialized : bool) (fmt : Format.formatter) (p_value : bytes) : unit :=
      if serialized then
        Format.pp_print_string fmt (Bytes.to_string p_value)
      else
        match deserialize_proof p_value with
        | Pervasives.Error msgError_monad.pp_trace fmt msg
        | Pervasives.Ok proof_value
          match proof_value with
          |
            Page_confirmed {|
              proof_repr.Page_confirmed.target_cell := target_cell;
                proof_repr.Page_confirmed.inc_proof := inc_proof;
                proof_repr.Page_confirmed.page_data := page_data;
                proof_repr.Page_confirmed.page_proof := page_proof
                |} ⇒
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Page_confirmed (target_cell="
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal ", data="
                      (CamlinternalFormatBasics.String
                        CamlinternalFormatBasics.No_padding
                        (CamlinternalFormatBasics.Char_literal "," % char
                          (CamlinternalFormatBasics.Formatting_lit
                            (CamlinternalFormatBasics.Break "@ " 1 0)
                            (CamlinternalFormatBasics.String_literal
                              "inc_proof:[size="
                              (CamlinternalFormatBasics.Int
                                CamlinternalFormatBasics.Int_d
                                CamlinternalFormatBasics.No_padding
                                CamlinternalFormatBasics.No_precision
                                (CamlinternalFormatBasics.String_literal " |"
                                  (CamlinternalFormatBasics.Formatting_lit
                                    (CamlinternalFormatBasics.Break "@ " 1 0)
                                    (CamlinternalFormatBasics.String_literal
                                      "path="
                                      (CamlinternalFormatBasics.Alpha
                                        (CamlinternalFormatBasics.Char_literal
                                          "]" % char
                                          (CamlinternalFormatBasics.Formatting_lit
                                            (CamlinternalFormatBasics.Break "@ "
                                              1 0)
                                            (CamlinternalFormatBasics.String_literal
                                              "page_proof:"
                                              (CamlinternalFormatBasics.Alpha
                                                (CamlinternalFormatBasics.Char_literal
                                                  ")" % char
                                                  CamlinternalFormatBasics.End_of_format)))))))))))))))))
                "Page_confirmed (target_cell=%a, data=%s,@ inc_proof:[size=%d |@ path=%a]@ page_proof:%a)")
              pp_history target_cell (Bytes.to_string page_data)
              (List.length inc_proof) pp_inclusion_proof inc_proof Page.pp_proof
              page_proof
          |
            Page_unconfirmed {|
              proof_repr.Page_unconfirmed.prev_cell := prev_cell;
                proof_repr.Page_unconfirmed.next_cell_opt := next_cell_opt;
                proof_repr.Page_unconfirmed.next_inc_proof := next_inc_proof
                |} ⇒
            Format.fprintf fmt
              (CamlinternalFormatBasics.Format
                (CamlinternalFormatBasics.String_literal
                  "Page_unconfirmed (prev_cell = "
                  (CamlinternalFormatBasics.Alpha
                    (CamlinternalFormatBasics.String_literal " | next_cell = "
                      (CamlinternalFormatBasics.Alpha
                        (CamlinternalFormatBasics.String_literal
                          " | prev_inc_proof:[size="
                          (CamlinternalFormatBasics.Int
                            CamlinternalFormatBasics.Int_d
                            CamlinternalFormatBasics.No_padding
                            CamlinternalFormatBasics.No_precision
                            (CamlinternalFormatBasics.Formatting_lit
                              (CamlinternalFormatBasics.Break "@ " 1 0)
                              (CamlinternalFormatBasics.String_literal "| path="
                                (CamlinternalFormatBasics.Alpha
                                  (CamlinternalFormatBasics.String_literal "])"
                                    CamlinternalFormatBasics.End_of_format))))))))))
                "Page_unconfirmed (prev_cell = %a | next_cell = %a | prev_inc_proof:[size=%d@ | path=%a])")
              pp_history prev_cell pp_history_opt next_cell_opt
              (List.length next_inc_proof) pp_inclusion_proof next_inc_proof
          end
        end.

    Module Unexpected_page_size.
      Record record : Set := Build {
        expected_size : int;
        page_size : int;
      }.
      Definition with_expected_size expected_size (r : record) :=
        Build expected_size r.(page_size).
      Definition with_page_size page_size (r : record) :=
        Build r.(expected_size) page_size.
    End Unexpected_page_size.
    Definition Unexpected_page_size := Unexpected_page_size.record.

Init function; without side-effects in Coq
    Definition init_module4 : unit :=
      Error_monad.register_error_kind Error_monad.Permanent
        "dal_slot_repr.slots_history.dal_proof_error" "Dal proof error"
        "Error occurred during Dal proof production or validation"
        (Some
          (fun (ppf : Format.formatter) ⇒
            fun (e_value : string) ⇒
              Format.fprintf ppf
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal "Dal proof error: "
                    (CamlinternalFormatBasics.String
                      CamlinternalFormatBasics.No_padding
                      CamlinternalFormatBasics.End_of_format))
                  "Dal 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 "Dal_proof_error" then
              let e_value := cast string payload in
              Some e_value
            else None
          end)
        (fun (e_value : string) ⇒
          Build_extensible "Dal_proof_error" string e_value).

Init function; without side-effects in Coq
    Definition init_module5 : unit :=
      Error_monad.register_error_kind Error_monad.Permanent
        "dal_slot_repr.slots_history.unexpected_page_size"
        "Unexpected page size"
        "The size of the given page content doesn't match the expected one."
        (Some
          (fun (ppf : Format.formatter) ⇒
            fun (function_parameter : int × int) ⇒
              let '(expected, size_value) := function_parameter in
              Format.fprintf ppf
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.String_literal
                    "The size of a Dal page is expected to be "
                    (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                      CamlinternalFormatBasics.No_padding
                      CamlinternalFormatBasics.No_precision
                      (CamlinternalFormatBasics.String_literal
                        " bytes. The given one has "
                        (CamlinternalFormatBasics.Int
                          CamlinternalFormatBasics.Int_d
                          CamlinternalFormatBasics.No_padding
                          CamlinternalFormatBasics.No_precision
                          CamlinternalFormatBasics.End_of_format))))
                  "The size of a Dal page is expected to be %d bytes. The given one has %d")
                expected size_value))
        (Data_encoding.obj2
          (Data_encoding.req None None "expected_size" Data_encoding.int16)
          (Data_encoding.req None None "page_size" Data_encoding.int16))
        (fun (function_parameter : Error_monad._error) ⇒
          match function_parameter with
          | Build_extensible tag _ payload
            if String.eqb tag "Unexpected_page_size" then
              let '{|
                Unexpected_page_size.expected_size := expected_size;
                  Unexpected_page_size.page_size := page_size
                  |} := cast Unexpected_page_size payload in
              Some (expected_size, page_size)
            else None
          end)
        (fun (function_parameter : int × int) ⇒
          let '(expected_size, page_size) := function_parameter in
          Build_extensible "Unexpected_page_size" Unexpected_page_size
            {| Unexpected_page_size.expected_size := expected_size;
              Unexpected_page_size.page_size := page_size; |}).

    Definition dal_proof_error (reason_value : string) : Error_monad._error :=
      Build_extensible "Dal_proof_error" string reason_value.

    Definition proof_error {A : Set} (reason_value : string) : M? A :=
      Error_monad.error_value (dal_proof_error reason_value).

    Axiom check_page_proof :
      Dal.parameters Dal.page_proof Dal.page Page.t
      Dal.commitment M? unit.

    Definition produce_proof_repr
      (dal_params : Dal.parameters) (page_id : Page.t)
      (page_info : option (Dal.page × Dal.page_proof))
      (slots_hist :
        Skip_list.Skip_list.(Skip_list_repr.S.cell) content
          History_cache.(Bounded_history_repr.S.key))
      (hist_cache : History_cache.(Bounded_history_repr.S.t))
      : M? (proof_repr × option Dal.page) :=
      let '{| Page.t.slot_id := slot_id; Page.t.page_index := _ |} := page_id in
      let deref (ptr : History_cache.(Bounded_history_repr.S.key))
        : option history :=
        History_cache.(Bounded_history_repr.S.find) ptr hist_cache in
      let search_result := Skip_list.search deref slots_hist slot_id in
      match (page_info, search_result.(Skip_list_repr.search_result.last_cell))
        with
      | (_, Skip_list_repr.Deref_returned_none)
        proof_error
          "Skip_list.search returned 'Deref_returned_none': Slots history cache is ill-formed or has too few entries."
      | (_, Skip_list_repr.No_exact_or_lower_ptr)
        proof_error
          "Skip_list.search returned 'No_exact_or_lower_ptr', while it is initialized with a min elt (slot zero)."
      | (Some (page_data, page_proof), Skip_list_repr.Found target_cell)
        let '{| Header.t.id := id; Header.t.commitment := commitment |} :=
          Skip_list.content target_cell in
        let? '_ :=
          Error_monad.error_when
            ((Header.compare_slot_id id Header.zero.(Header.t.id)) =i 0)
            (dal_proof_error
              "Skip_list.search returned 'Found <zero_slot>': No existence proof should be constructed with the slot zero.")
          in
        let? '_ :=
          check_page_proof dal_params page_proof page_data page_id commitment in
        let inc_proof :=
          List.rev search_result.(Skip_list_repr.search_result.rev_path) in
        let? '_ :=
          Error_monad.error_when (List.is_empty inc_proof)
            (dal_proof_error "The inclusion proof cannot be empty") in
        return?
          ((Page_confirmed
            {| proof_repr.Page_confirmed.target_cell := target_cell;
              proof_repr.Page_confirmed.inc_proof := inc_proof;
              proof_repr.Page_confirmed.page_data := page_data;
              proof_repr.Page_confirmed.page_proof := page_proof; |}),
            (Some page_data))
      |
        (None,
          Skip_list_repr.Nearest {|
            Skip_list_repr.search_cell_result.Nearest.lower := prev_cell;
              Skip_list_repr.search_cell_result.Nearest.upper := next_cell_opt
              |})
        let? next_inc_proof :=
          match search_result.(Skip_list_repr.search_result.rev_path) with
          | []
            (* ❌ Assert instruction is not handled. *)
            assert (M? inclusion_proof) false
          | cons prev rev_next_inc_proof
            let? '_ :=
              Error_monad.error_unless (equal_history prev prev_cell)
                (dal_proof_error
                  "Internal error: search's Nearest result is inconsistent.") in
            return? (List.rev rev_next_inc_proof)
          end in
        return?
          ((Page_unconfirmed
            {| proof_repr.Page_unconfirmed.prev_cell := prev_cell;
              proof_repr.Page_unconfirmed.next_cell_opt := next_cell_opt;
              proof_repr.Page_unconfirmed.next_inc_proof := next_inc_proof; |}),
            None)
      | (None, Skip_list_repr.Found _)
        proof_error
          "The page ID's slot is confirmed, but no page content and proof are provided."
      | (Some _, Skip_list_repr.Nearest _)
        proof_error
          "The page ID's slot is not confirmed, but page content and proof are provided."
      end.

    Definition produce_proof
      (dal_params : Dal.parameters) (page_id : Page.t)
      (page_info : option (Dal.page × Dal.page_proof))
      (slots_hist :
        Skip_list.Skip_list.(Skip_list_repr.S.cell) content
          History_cache.(Bounded_history_repr.S.key))
      (hist_cache : History_cache.(Bounded_history_repr.S.t))
      : M? (bytes × option Dal.page) :=
      let? '(proof_repr, page_data) :=
        produce_proof_repr dal_params page_id page_info slots_hist hist_cache in
      let? serialized_proof := serialize_proof proof_repr in
      return? (serialized_proof, page_data).

    Axiom verify_inclusion_proof :
      list history history history M? unit.

    Definition verify_proof_repr
      (dal_params : Dal.parameters) (page_id : Page.t)
      (snapshot_value : history) (proof_value : proof_repr)
      : M? (option Page.content) :=
      let '{| Page.t.slot_id := slot_id; Page.t.page_index := _ |} := page_id in
      match proof_value with
      |
        Page_confirmed {|
          proof_repr.Page_confirmed.target_cell := target_cell;
            proof_repr.Page_confirmed.inc_proof := inc_proof;
            proof_repr.Page_confirmed.page_data := page_data;
            proof_repr.Page_confirmed.page_proof := page_proof
            |} ⇒
        let '{| Header.t.id := id; Header.t.commitment := commitment |} :=
          Skip_list.content target_cell in
        let? '_ :=
          Error_monad.error_when
            ((Header.compare_slot_id id Header.zero.(Header.t.id)) =i 0)
            (dal_proof_error
              "verify_proof_repr: cannot construct a confirmation page proof with 'zero' as target slot.")
          in
        let? '_ := verify_inclusion_proof inc_proof snapshot_value target_cell
          in
        let? '_ :=
          check_page_proof dal_params page_proof page_data page_id commitment in
        Error_monad.Result_syntax.return_some page_data
      |
        Page_unconfirmed {|
          proof_repr.Page_unconfirmed.prev_cell := prev_cell;
            proof_repr.Page_unconfirmed.next_cell_opt := next_cell_opt;
            proof_repr.Page_unconfirmed.next_inc_proof := next_inc_proof
            |} ⇒
        let op_lt (a_value : Header.id) (b_value : Header.id) : bool :=
          (Header.compare_slot_id a_value b_value) <i 0 in
        let? '_ :=
          match next_cell_opt with
          | None
            let? '_ :=
              Error_monad.error_unless (List.is_empty next_inc_proof)
                (dal_proof_error "verify_proof_repr: invalid next_inc_proof") in
            Error_monad.error_unless
              ((op_lt (Skip_list.content prev_cell).(Header.t.id) slot_id) &&
              (equal_history snapshot_value prev_cell))
              (dal_proof_error "verify_proof_repr: invalid next_inc_proof")
          | Some next_cell
            let? '_ :=
              Error_monad.error_unless
                ((op_lt (Skip_list.content prev_cell).(Header.t.id) slot_id) &&
                ((op_lt slot_id (Skip_list.content next_cell).(Header.t.id)) &&
                (let prev_cell_pointer := Skip_list.back_pointer next_cell 0 in
                match prev_cell_pointer with
                | Nonefalse
                | Some prev_ptr
                  Pointer_hash.equal prev_ptr (hash_skip_list_cell prev_cell)
                end)))
                (dal_proof_error "verify_proof_repr: invalid next_inc_proof") in
            verify_inclusion_proof next_inc_proof snapshot_value next_cell
          end in
        Error_monad.Result_syntax.return_none
      end.

    Definition verify_proof
      (dal_params : Dal.parameters) (page_id : Page.t)
      (snapshot_value : history) (serialized_proof : bytes)
      : M? (option Page.content) :=
      let? proof_repr := deserialize_proof serialized_proof in
      verify_proof_repr dal_params page_id snapshot_value proof_repr.
  End V1.

  Include V1.
End History.