diff --git a/src/app/zeko/circuits/indexed_merkle_tree.ml b/src/app/zeko/circuits/indexed_merkle_tree.ml index 213dd31912..2d9a263d62 100644 --- a/src/app/zeko/circuits/indexed_merkle_tree.ml +++ b/src/app/zeko/circuits/indexed_merkle_tree.ml @@ -1,5 +1,7 @@ +open Core_kernel open Snark_params.Tick open Zeko_util +open Checked.Let_syntax module Make (Inputs : sig module Key : SnarkType @@ -36,6 +38,19 @@ struct let hash_entry = var_to_hash ~init:Zeko_constants.indexed_merkle_tree_salt Entry.typ + let empty_path = + List.init height ~f:Fn.id + |> List.fold_map ~init:Field.zero ~f:(fun acc _ -> + let next = + Random_oracle.hash + ~init: + (Hash_prefix_create.salt + Zeko_constants.indexed_merkle_tree_merge_salt ) + [| acc; acc |] + in + (next, constant Field.typ acc) ) + |> snd + (* TODO: consider different salt per level. *) (* NB: The first element in the list is the neighbor of init, and the next element is a level up, and so on. This is the same as what the Mina code base does. *) @@ -46,13 +61,15 @@ struct ~typ:Typ.(F.typ * F.typ) ~then_:(hash_other, acc) ~else_:(acc, hash_other) in - var_to_hash ~init:"indexed merkle tree" Typ.(F.typ * F.typ) (left, right) ) + var_to_hash ~init:Zeko_constants.indexed_merkle_tree_merge_salt + Typ.(F.typ * F.typ) + (left, right) ) let implied_root (entry : Entry.var) (path : Path.var) : F.var Checked.t = let* init = hash_entry entry in implied_root_raw init path - let add_key_var ?check ~x ~path_x ~y ~path_y ~z () = + let add_key_var ~check ~x ~path_x ~y ~path_y ~z () = let* () = with_label __LOC__ (fun () -> assert_x_less_than_y_less_than_z ~x ~y ~z) in @@ -62,23 +79,25 @@ struct implied_root_raw Field.(constant typ zero) path_y in let* root_intermediate = - match check with - | Some check -> - if_ check ~typ:F.typ ~then_:root_intermediate - ~else_:root_intermediate' - | None -> - Checked.return root_intermediate + if_ check ~typ:F.typ ~then_:root_intermediate ~else_:root_intermediate' in let* () = assert_equal ~label:__LOC__ F.typ root_intermediate root_intermediate' in let* root_new = implied_root { key = y; next_key = z } path_y in - let* root = - match check with - | Some check -> - if_ check ~typ:F.typ ~then_:root ~else_:root_new - | None -> - Checked.return root + let* root = if_ check ~typ:F.typ ~then_:root ~else_:root_new in + (* Check that no empty indices have been skipped. *) + let* is_y_most_left = + foldl (List.zip_exn path_y empty_path) ~init:Boolean.true_ + ~f:(fun acc (PathStep.{ hash_other; is_right }, empty_hash) -> + let* is_valid_left = + Field.Checked.equal empty_hash hash_other >>= Boolean.( &&& ) acc + in + if_ is_right ~typ:Boolean.typ ~then_:acc ~else_:is_valid_left ) + in + let* () = + if_ check ~typ:Boolean.typ ~then_:is_y_most_left ~else_:Boolean.true_ + >>= Boolean.Assert.is_true in Checked.return (`Before_adding_y root, `After_adding_y root_new) diff --git a/src/app/zeko/circuits/indexed_merkle_tree.mli b/src/app/zeko/circuits/indexed_merkle_tree.mli index 05c174ce21..20a07b95c6 100644 --- a/src/app/zeko/circuits/indexed_merkle_tree.mli +++ b/src/app/zeko/circuits/indexed_merkle_tree.mli @@ -48,7 +48,7 @@ end) : sig end val add_key_var : - ?check:Boolean.var + check:Boolean.var -> x:Key.var -> path_x:Path.var -> y:Key.var diff --git a/src/app/zeko/circuits/rule_commit.ml b/src/app/zeko/circuits/rule_commit.ml index e3097023bb..af6d6f35ad 100644 --- a/src/app/zeko/circuits/rule_commit.ml +++ b/src/app/zeko/circuits/rule_commit.ml @@ -166,9 +166,7 @@ struct in let input = let open Random_oracle.Input.Chunked in - append - (Ledger_hash.var_to_field target_ledger |> field) - (Account_set.to_input_var target_acc_set) + Ledger_hash.var_to_field target_ledger |> field in let* payload = make_checked (fun () ->