🔗 Merkle_list.v
Translated OCaml
File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Definition max_depth (count_limit : int) : int :=
let log2 (n_value : int) : int :=
Z.numbits (Z.of_int n_value) in
log2 count_limit.
Require Import CoqOfOCaml.Settings.
Require Import TezosOfOCaml.Environment.V8.
Definition max_depth (count_limit : int) : int :=
let log2 (n_value : int) : int :=
Z.numbits (Z.of_int n_value) in
log2 count_limit.
Init function; without side-effects in Coq
Definition init_module : unit :=
Error_monad.register_error_kind Error_monad.Temporary
"Merkle_list_invalid_position" "Merkle_list_invalid_position"
"Merkle_list_invalid_position"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
"Merkle_list_invalid_position")) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Merkle_list_invalid_position" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Merkle_list_invalid_position" unit tt).
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
| Empty ⇒ empty
| Leaf h_value ⇒ h_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_value ⇒ aux (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_value ⇒ aux (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
| Top ⇒ t_value
| Left z_value r_value ⇒ rebuild_tree z_value (node_of t_value r_value)
| Right l_value z_value ⇒ rebuild_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
| Empty ⇒ List.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
| None ⇒ path_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
| pl ⇒ aux 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.
Error_monad.register_error_kind Error_monad.Temporary
"Merkle_list_invalid_position" "Merkle_list_invalid_position"
"Merkle_list_invalid_position"
(Some
(fun (ppf : Format.formatter) ⇒
fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Format.fprintf ppf
(CamlinternalFormatBasics.Format
(CamlinternalFormatBasics.String
CamlinternalFormatBasics.No_padding
CamlinternalFormatBasics.End_of_format) "%s")
"Merkle_list_invalid_position")) Data_encoding.empty
(fun (function_parameter : Error_monad._error) ⇒
match function_parameter with
| Build_extensible tag _ payload ⇒
if String.eqb tag "Merkle_list_invalid_position" then
Some tt
else None
end)
(fun (function_parameter : unit) ⇒
let '_ := function_parameter in
Build_extensible "Merkle_list_invalid_position" unit tt).
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
| Empty ⇒ empty
| Leaf h_value ⇒ h_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_value ⇒ aux (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_value ⇒ aux (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
| Top ⇒ t_value
| Left z_value r_value ⇒ rebuild_tree z_value (node_of t_value r_value)
| Right l_value z_value ⇒ rebuild_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
| Empty ⇒ List.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
| None ⇒ path_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
| pl ⇒ aux 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.