Skip to main content

🔗 Merkle_list.v

Translated OCaml

Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.

Definition max_depth (count_limit : int) : int :=
  let log2 (n_value : int) : int :=
    Z.numbits (Z.of_int n_value) in
  log2 count_limit.

Module T.
  Record signature {t h elt path : Set} : Set := {
    t := t;
    h := h;
    elt := elt;
    path := path;
    dummy_path : path;
    pp_path : Format.formatter path unit;
    nil : t;
    empty : h;
    root_value : t h;
    snoc : t elt t;
    snoc_tr : t elt t;
    compute : list elt h;
    path_encoding : Data_encoding.t path;
    bounded_path_encoding : option int unit Data_encoding.t path;
    compute_path : t int M? path;
    check_path : path int elt h M? bool;
    path_depth : path int;
    elt_bytes : elt Bytes.t;
  }.
End T.
Definition T := @T.signature.
Arguments T {_ _ _ _}.

Module S_El.
  Record signature {t : Set} : Set := {
    t := t;
    to_bytes : t bytes;
  }.
End S_El.
Definition S_El := @S_El.signature.
Arguments S_El {_}.

Module Make.
  Class FArgs {El_t H_t H_Set_t : Set} {H_Map_t : Set Set} := {
    El : S_El (t := El_t);
    H : S.HASH (t := H_t) (Set_t := H_Set_t) (Map_t := H_Map_t);
  }.
  Arguments Build_FArgs {_ _ _ _}.

  Definition h `{FArgs} : Set := H.(S.HASH.t).

  Definition elt `{FArgs} : Set := El.(S_El.t).

  Definition elt_bytes `{FArgs} : El.(S_El.t) bytes := El.(S_El.to_bytes).

  Inductive tree `{FArgs} : Set :=
  | Empty : tree
  | Leaf : h tree
  | Node : h × tree × tree tree.

  Module t.
    Record record `{FArgs} : Set := Build {
      tree : tree;
      depth : int;
      next_pos : int;
    }.
    Definition with_tree `{FArgs} tree (r : record) :=
      Build _ _ _ _ _ tree r.(depth) r.(next_pos).
    Definition with_depth `{FArgs} depth (r : record) :=
      Build _ _ _ _ _ r.(tree) depth r.(next_pos).
    Definition with_next_pos `{FArgs} next_pos (r : record) :=
      Build _ _ _ _ _ r.(tree) r.(depth) next_pos.
  End t.
  Definition t `{FArgs} := t.record.

  Definition path `{FArgs} : Set := list h.

  Definition dummy_path `{FArgs} {A : Set} : list A := nil.

  Definition pp_path `{FArgs} (ppf : Format.formatter)
    : list H.(S.HASH.t) unit :=
    Format.fprintf ppf
      (CamlinternalFormatBasics.Format
        (CamlinternalFormatBasics.Alpha CamlinternalFormatBasics.End_of_format)
        "%a")
      (Format.pp_print_list
        (Some
          (fun (fmt : Format.formatter) ⇒
            fun (function_parameter : unit) ⇒
              let '_ := function_parameter in
              Format.fprintf fmt
                (CamlinternalFormatBasics.Format
                  (CamlinternalFormatBasics.Char_literal ";" % char
                    (CamlinternalFormatBasics.Formatting_lit
                      (CamlinternalFormatBasics.Break "@ " 1 0)
                      CamlinternalFormatBasics.End_of_format)) ";@ ")))
        H.(S.HASH.pp)).

  Definition empty `{FArgs} : H.(S.HASH.t) := H.(S.HASH.zero).

  Definition root_aux `{FArgs} (function_parameter : tree) : h :=
    match function_parameter with
    | Emptyempty
    | Leaf h_valueh_value
    | Node (h_value, _, _)h_value
    end.

  Definition nil `{FArgs} : t :=
    {| t.tree := Empty; t.depth := 0; t.next_pos := 0; |}.

  Definition hash_elt `{FArgs} (el : El.(S_El.t)) : H.(S.HASH.t) :=
    H.(S.HASH.hash_bytes) None [ elt_bytes el ].

  Definition leaf_of `{FArgs} (el : El.(S_El.t)) : tree := Leaf (hash_elt el).

  Definition hash2 `{FArgs} (h1 : H.(S.HASH.t)) (h2 : H.(S.HASH.t))
    : H.(S.HASH.t) :=
    H.(S.HASH.hash_bytes) None
      [ H.(S.HASH.to_bytes) h1; H.(S.HASH.to_bytes) h2 ].

  Definition node_of `{FArgs} (t1 : tree) (t2 : tree) : tree :=
    Node ((hash2 (root_aux t1) (root_aux t2)), t1, t2).

  #[bypass_check(guard)]
  Definition to_bin `{FArgs} (pos : int) (depth : int) : list bool :=
    let fix aux (acc_value : list bool) (pos : int) (depth : int) {struct depth}
      : list bool :=
      let '(pos', dir) := ((pos /i 2), (Pervasives._mod pos 2)) in
      match depth with
      | 0 ⇒ acc_value
      | d_valueaux (cons (dir =i 1) acc_value) pos' (d_value -i 1)
      end in
    aux List.nil pos depth.

  #[bypass_check(guard)]
  Definition make_spine_with `{FArgs} (el : El.(S_El.t)) : int tree :=
    let fix aux (_left : tree) (function_parameter : int)
      {struct function_parameter} : tree :=
      match function_parameter with
      | 0 ⇒ _left
      | d_valueaux (node_of _left Empty) (d_value -i 1)
      end in
    aux (leaf_of el).

  #[bypass_check(guard)]
  Definition snoc `{FArgs} (t_value : t) (el : elt) : t :=
    let fix traverse (tree_value : tree) (depth : int) (key_value : list bool)
      {struct depth} : tree :=
      match (tree_value, key_value) with
      | (Node (_, t_left, Empty), cons true _key)
        let t_right := make_spine_with el (depth -i 1) in
        node_of t_left t_right
      | (Node (_, t_left, Empty), cons false key_value)
        let t_left := traverse t_left (depth -i 1) key_value in
        node_of t_left Empty
      | (Node (_, t_left, t_right), cons true key_value)
        let t_right := traverse t_right (depth -i 1) key_value in
        node_of t_left t_right
      | (_, _)
        (* ❌ Assert instruction is not handled. *)
        assert tree false
      end in
    let '(tree', depth') :=
      match (t_value.(t.tree), t_value.(t.depth), t_value.(t.next_pos)) with
      | (Empty, 0, 0)((node_of (leaf_of el) Empty), 1)
      | (tree_value, depth, pos)
        if Int32.equal (Int32.shift_left 1 depth) (Int32.of_int pos) then
          let t_right := make_spine_with el depth in
          ((node_of tree_value t_right), (depth +i 1))
        else
          let key_value := to_bin pos depth in
          ((traverse tree_value depth key_value), depth)
      end in
    {| t.tree := tree'; t.depth := depth';
      t.next_pos := t_value.(t.next_pos) +i 1; |}.

  Inductive zipper `{FArgs} : Set :=
  | Left : zipper tree zipper
  | Right : tree zipper zipper
  | Top : zipper.

  Fixpoint rebuild_tree `{FArgs} (z_value : zipper) (t_value : tree) : tree :=
    match z_value with
    | Topt_value
    | Left z_value r_valuerebuild_tree z_value (node_of t_value r_value)
    | Right l_value z_valuerebuild_tree z_value (node_of l_value t_value)
    end.

  Definition snoc_tr `{FArgs} (t_value : t) (el : elt) : t :=
    let fix traverse
      (z_value : zipper) (tree_value : tree) (depth : int)
      (key_value : list bool) : tree :=
      match (tree_value, key_value) with
      | (Node (_, t_left, Empty), cons true _key)
        let t_right := make_spine_with el (depth -i 1) in
        rebuild_tree z_value (node_of t_left t_right)
      | (Node (_, t_left, Empty), cons false key_value)
        let z_value := Left z_value Empty in
        traverse z_value t_left (depth -i 1) key_value
      | (Node (_, t_left, t_right), cons true key_value)
        let z_value := Right t_left z_value in
        traverse z_value t_right (depth -i 1) key_value
      | (_, _)
        (* ❌ Assert instruction is not handled. *)
        assert tree false
      end in
    let '(tree', depth') :=
      match (t_value.(t.tree), t_value.(t.depth), t_value.(t.next_pos)) with
      | (Empty, 0, 0)((node_of (leaf_of el) Empty), 1)
      | (tree_value, depth, pos)
        if Int32.equal (Int32.shift_left 1 depth) (Int32.of_int pos) then
          let t_right := make_spine_with el depth in
          ((node_of tree_value t_right), (depth +i 1))
        else
          let key_value := to_bin pos depth in
          ((traverse Top tree_value depth key_value), depth)
      end in
    {| t.tree := tree'; t.depth := depth';
      t.next_pos := t_value.(t.next_pos) +i 1; |}.

  Fixpoint tree_to_list `{FArgs} (function_parameter : tree) : list h :=
    match function_parameter with
    | EmptyList.nil
    | Leaf h_value[ h_value ]
    | Node (_, t_left, t_right)
      Pervasives.op_at (tree_to_list t_left) (tree_to_list t_right)
    end.

  Definition path_encoding `{FArgs}
    : Data_encoding.encoding (list H.(S.HASH.t)) :=
    Data_encoding.list_value None H.(S.HASH.encoding).

  Definition bounded_path_encoding `{FArgs}
    (max_length : option int) (function_parameter : unit)
    : Data_encoding.encoding (list H.(S.HASH.t)) :=
    let '_ := function_parameter in
    match max_length with
    | Nonepath_encoding
    | Some max_length
      Data_encoding.list_value (Some max_length) H.(S.HASH.encoding)
    end.

  Definition compute_path `{FArgs} (function_parameter : t)
    : int M? (list h) :=
    let '{| t.tree := tree_value; t.depth := depth; t.next_pos := next_pos |} :=
      function_parameter in
    fun (pos : int) ⇒
      if (pos <i 0) || (pos i next_pos) then
        Error_monad.error_value
          (Build_extensible "Merkle_list_invalid_position" unit tt)
      else
        let key_value := to_bin pos depth in
        let fix aux
          (acc_value : list h) (tree_value : tree) (key_value : list bool)
          : M? (list h) :=
          match (tree_value, key_value) with
          | (Leaf _, [])return? acc_value
          | (Node (_, l_value, r_value), cons b_value key_value)
            if b_value then
              aux (cons (root_aux l_value) acc_value) r_value key_value
            else
              aux (cons (root_aux r_value) acc_value) l_value key_value
          | _
            Error_monad.error_value
              (Build_extensible "Merkle_list_invalid_position" unit tt)
          end in
        aux List.nil tree_value key_value.

  Definition check_path `{FArgs}
    (path : list H.(S.HASH.t)) (pos : int) (el : El.(S_El.t))
    (expected_root : H.(S.HASH.t)) : M? bool :=
    let depth := List.length path in
    if (pos i 0) && ((Z.of_int pos) <Z (Z.shift_left Z.one depth)) then
      let key_value := List.rev (to_bin pos depth) in
      let computed_root :=
        List.fold_left
          (fun (acc_value : H.(S.HASH.t)) ⇒
            fun (function_parameter : H.(S.HASH.t) × bool) ⇒
              let '(sibling, b_value) := function_parameter in
              if b_value then
                hash2 sibling acc_value
              else
                hash2 acc_value sibling) (hash_elt el)
          (List.combine_drop path key_value) in
      return? (H.(S.HASH.equal) computed_root expected_root)
    else
      Error_monad.error_value
        (Build_extensible "Merkle_list_invalid_position" unit tt).

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

  #[bypass_check(guard)]
  Definition compute `{FArgs} (l_value : list El.(S_El.t)) : H.(S.HASH.t) :=
    let fix aux (l_value : list H.(S.HASH.t)) {struct l_value} : H.(S.HASH.t) :=
      let fix pairs
        (acc_value : list H.(S.HASH.t)) (function_parameter : list H.(S.HASH.t))
        : list H.(S.HASH.t) :=
        match function_parameter with
        | []List.rev acc_value
        | cons x_value []List.rev (cons (hash2 x_value empty) acc_value)
        | cons x_value (cons y_value xs) ⇒
          pairs (cons (hash2 x_value y_value) acc_value) xs
        end in
      match pairs List.nil l_value with
      | []empty
      | cons h_value []h_value
      | plaux pl
      end in
    aux (List.map hash_elt l_value).

  Definition root_value `{FArgs} (t_value : t) : h := root_aux t_value.(t.tree).

  (* Make *)
  Definition functor `{FArgs} :=
    {|
      T.dummy_path := dummy_path;
      T.pp_path := pp_path;
      T.nil := nil;
      T.empty := empty;
      T.root_value := root_value;
      T.snoc := snoc;
      T.snoc_tr := snoc_tr;
      T.compute := compute;
      T.path_encoding := path_encoding;
      T.bounded_path_encoding := bounded_path_encoding;
      T.compute_path := compute_path;
      T.check_path := check_path;
      T.path_depth := path_depth;
      T.elt_bytes := elt_bytes
    |}.
End Make.
Definition Make {El_t H_t H_Set_t : Set} {H_Map_t : Set Set}
  (El : S_El (t := El_t))
  (H : S.HASH (t := H_t) (Set_t := H_Set_t) (Map_t := H_Map_t))
  : T (t := _) (h := H.(S.HASH.t)) (elt := El.(S_El.t)) (path := list Make.H.(HASH.t)) :=
  let '_ := Make.Build_FArgs El H in
  Make.functor.