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.V7.
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.

Module Header.
  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 Header.

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 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;
    header : Header.t;
  }.
  Definition with_id id (r : record) :=
    Build id r.(header).
  Definition with_header header (r : record) :=
    Build r.(id) header.
End t.
Definition t := t.record.

Definition slot : Set := t.

Definition slot_index : Set := Index.t.

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 slot_equal (function_parameter : t) : t bool :=
  let '{| t.id := id; t.header := header |} := function_parameter in
  fun (s2 : t) ⇒
    (slot_id_equal id s2.(t.id)) && (Header.equal header s2.(t.header)).

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.header := Header.zero; |}.

Module Slot_index := Index.

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

  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_index : Slot_index.t;
      page_index : Index.t;
    }.
    Definition with_slot_index slot_index (r : record) :=
      Build slot_index r.(page_index).
    Definition with_page_index page_index (r : record) :=
      Build r.(slot_index) page_index.
  End t.
  Definition t := t.record.

  Definition encoding : Data_encoding.encoding t :=
    Data_encoding.conv
      (fun (function_parameter : t) ⇒
        let '{| t.slot_index := slot_index; t.page_index := page_index |} :=
          function_parameter in
        (slot_index, page_index))
      (fun (function_parameter : Slot_index.t × Index.t) ⇒
        let '(slot_index, page_index) := function_parameter in
        {| t.slot_index := slot_index; t.page_index := page_index; |}) None
      (Data_encoding.obj2
        (Data_encoding.req None None "slot_index" Slot_index.encoding)
        (Data_encoding.req None None "page_index" Index.encoding)).

  Definition equal (page : t) (page' : t) : bool :=
    (Slot_index.equal page.(t.slot_index) page'.(t.slot_index)) &&
    (Index.equal page.(t.page_index) page'.(t.page_index)).

  Definition pp (fmt : Format.formatter) (function_parameter : t) : unit :=
    let '{| t.slot_index := slot_index; t.page_index := page_index |} :=
      function_parameter in
    Format.fprintf fmt
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.String_literal "(slot_index: "
          (CamlinternalFormatBasics.Alpha
            (CamlinternalFormatBasics.String_literal ", page_index: "
              (CamlinternalFormatBasics.Alpha
                (CamlinternalFormatBasics.Char_literal ")" % char
                  CamlinternalFormatBasics.End_of_format)))))
        "(slot_index: %a, page_index: %a)") Slot_index.pp slot_index Index.pp
      page_index.
End Page.

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

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

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

  Module t.
    Record record : Set := Build {
      length : int;
      slots : Slot_index_map.(Map.S.t) slot;
    }.
    Definition with_length length (r : record) :=
      Build length r.(slots).
    Definition with_slots slots (r : record) :=
      Build r.(length) slots.
  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 slots {A : Set} : Slot_index_map.(Map.S.t) A :=
      Slot_index_map.(Map.S.empty) in
    {| t.length := length; t.slots := slots; |}.

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

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

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

Module Slots_history.
  Module Leaf.
    Definition t : Set := slot.

    Definition to_bytes : t bytes :=
      Data_encoding.Binary.to_bytes_exn None slot_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.

  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 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 compare : id id int := compare_slot_id.

    Definition compare_lwt (a_value : id) (b_value : id) : int :=
      compare a_value b_value.

Init function; without side-effects in Coq
    Definition init_module_repr : 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).

    Definition next {A : Set}
      (prev_cell : cell t A) (prev_cell_ptr : A) (elt_value : t)
      : M? (Skip_list.(Skip_list_repr.S.cell) t A) :=
      let? '_ :=
        Error_monad.error_when
          ((compare elt_value.(t.id) (content prev_cell).(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) id A))
      (cell_value : Skip_list.(Skip_list_repr.S.cell) id A) (id_target : id)
      : Skip_list.(Skip_list_repr.S.search_result) id A :=
      Skip_list.(Skip_list_repr.S.search) deref (compare_lwt id_target)
        cell_value.


  End Skip_list.

  Module V1.
    Definition content : Set := slot.

    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 slot_encoding.

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

    Definition encoding : Data_encoding.t history := history_encoding.

    Definition equal : t t bool := equal_history.

    Definition genesis : t := Skip_list.genesis 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 slot_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 pp_slot) 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
      (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 : 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 in
        return? (new_cell, cache).

    Definition add_confirmed_slots
      (t_value : t) (cache : History_cache.(Bounded_history_repr.S.t))
      (slots : list content)
      : M? (history × History_cache.(Bounded_history_repr.S.t)) :=
      List.fold_left_e add_confirmed_slot (t_value, cache) slots.

    Definition add_confirmed_slots_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 (t_value, no_cache) slots)
            Pervasives.fst.
  End V1.

  Include V1.
End Slots_history.

Definition encoding : Data_encoding.encoding t := slot_encoding.

Definition pp : Format.formatter t unit := pp_slot.

Definition equal : t t bool := slot_equal.