From 215332c06cb624d9ac6a30043d42eb3dd032443f Mon Sep 17 00:00:00 2001 From: Martin Ondejka Date: Wed, 20 Aug 2025 21:57:41 +0200 Subject: [PATCH 1/5] Forbid skipping indices in account set --- src/app/zeko/circuits/indexed_merkle_tree.ml | 28 +++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/src/app/zeko/circuits/indexed_merkle_tree.ml b/src/app/zeko/circuits/indexed_merkle_tree.ml index 213dd31912..3af9fbc413 100644 --- a/src/app/zeko/circuits/indexed_merkle_tree.ml +++ b/src/app/zeko/circuits/indexed_merkle_tree.ml @@ -1,5 +1,6 @@ open Snark_params.Tick open Zeko_util +open Checked.Let_syntax module Make (Inputs : sig module Key : SnarkType @@ -37,6 +38,9 @@ struct var_to_hash ~init:Zeko_constants.indexed_merkle_tree_salt Entry.typ (* TODO: consider different salt per level. *) + let merge_hashes left right = + var_to_hash ~init:"indexed merkle tree" Typ.(F.typ * F.typ) (left, right) + (* 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. *) let implied_root_raw (init : F.var) (path : Path.var) : F.var Checked.t = @@ -46,7 +50,7 @@ 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) ) + merge_hashes left right ) let implied_root (entry : Entry.var) (path : Path.var) : F.var Checked.t = let* init = hash_entry entry in @@ -80,6 +84,28 @@ struct | None -> Checked.return root in + let* is_y_most_left, _empty_root = + foldl path_y + ~init:(Boolean.true_, Field.(constant typ zero)) + ~f:(fun (acc, prev_empty_hash) PathStep.{ hash_other; is_right } -> + let* is_valid_left = + Field.Checked.equal prev_empty_hash hash_other + >>= Boolean.( &&& ) acc + in + let* acc = + if_ is_right ~typ:Boolean.typ ~then_:acc ~else_:is_valid_left + in + let*| empty_hash = merge_hashes prev_empty_hash prev_empty_hash in + (acc, empty_hash) ) + in + let* () = + match check with + | Some check -> + if_ check ~typ:Boolean.typ ~then_:is_y_most_left ~else_:Boolean.true_ + >>= Boolean.Assert.is_true + | None -> + Checked.return () + in Checked.return (`Before_adding_y root, `After_adding_y root_new) let to_input_var = Random_oracle.Input.Chunked.field From 12bed7d380aea79009e9d7b3326cb7f0be42b5bf Mon Sep 17 00:00:00 2001 From: Martin Ondejka Date: Wed, 20 Aug 2025 21:58:04 +0200 Subject: [PATCH 2/5] Don't require acc set signature in commit rule --- src/app/zeko/circuits/rule_commit.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) 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 () -> From f23a4bf68aaf6eda2546f4b4c6c344ee773e49c0 Mon Sep 17 00:00:00 2001 From: Martin Ondejka Date: Wed, 20 Aug 2025 22:35:16 +0200 Subject: [PATCH 3/5] Make the empty path constant --- src/app/zeko/circuits/indexed_merkle_tree.ml | 37 ++++++++++++-------- 1 file changed, 22 insertions(+), 15 deletions(-) diff --git a/src/app/zeko/circuits/indexed_merkle_tree.ml b/src/app/zeko/circuits/indexed_merkle_tree.ml index 3af9fbc413..a5f90cad53 100644 --- a/src/app/zeko/circuits/indexed_merkle_tree.ml +++ b/src/app/zeko/circuits/indexed_merkle_tree.ml @@ -1,3 +1,4 @@ +open Core_kernel open Snark_params.Tick open Zeko_util open Checked.Let_syntax @@ -37,10 +38,20 @@ struct let hash_entry = var_to_hash ~init:Zeko_constants.indexed_merkle_tree_salt Entry.typ - (* TODO: consider different salt per level. *) - let merge_hashes left right = - var_to_hash ~init:"indexed merkle tree" Typ.(F.typ * F.typ) (left, right) + 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. *) let implied_root_raw (init : F.var) (path : Path.var) : F.var Checked.t = @@ -50,7 +61,9 @@ struct ~typ:Typ.(F.typ * F.typ) ~then_:(hash_other, acc) ~else_:(acc, hash_other) in - merge_hashes 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 @@ -84,19 +97,13 @@ struct | None -> Checked.return root in - let* is_y_most_left, _empty_root = - foldl path_y - ~init:(Boolean.true_, Field.(constant typ zero)) - ~f:(fun (acc, prev_empty_hash) PathStep.{ hash_other; is_right } -> + 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 prev_empty_hash hash_other - >>= Boolean.( &&& ) acc - in - let* acc = - if_ is_right ~typ:Boolean.typ ~then_:acc ~else_:is_valid_left + Field.Checked.equal empty_hash hash_other >>= Boolean.( &&& ) acc in - let*| empty_hash = merge_hashes prev_empty_hash prev_empty_hash in - (acc, empty_hash) ) + if_ is_right ~typ:Boolean.typ ~then_:acc ~else_:is_valid_left ) in let* () = match check with From e7174eec819adf16842411fcf08313ff38eb049f Mon Sep 17 00:00:00 2001 From: Martin Ondejka Date: Wed, 20 Aug 2025 22:40:04 +0200 Subject: [PATCH 4/5] Add comment --- src/app/zeko/circuits/indexed_merkle_tree.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/app/zeko/circuits/indexed_merkle_tree.ml b/src/app/zeko/circuits/indexed_merkle_tree.ml index a5f90cad53..21a5a896c3 100644 --- a/src/app/zeko/circuits/indexed_merkle_tree.ml +++ b/src/app/zeko/circuits/indexed_merkle_tree.ml @@ -97,6 +97,7 @@ struct | None -> Checked.return root 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) -> From 8fc1cddf4f1404698a3be6164e6cdde16e82377d Mon Sep 17 00:00:00 2001 From: Martin Ondejka Date: Wed, 20 Aug 2025 22:46:37 +0200 Subject: [PATCH 5/5] Remove redundant optionality in check --- src/app/zeko/circuits/indexed_merkle_tree.ml | 25 ++++--------------- src/app/zeko/circuits/indexed_merkle_tree.mli | 2 +- 2 files changed, 6 insertions(+), 21 deletions(-) diff --git a/src/app/zeko/circuits/indexed_merkle_tree.ml b/src/app/zeko/circuits/indexed_merkle_tree.ml index 21a5a896c3..2d9a263d62 100644 --- a/src/app/zeko/circuits/indexed_merkle_tree.ml +++ b/src/app/zeko/circuits/indexed_merkle_tree.ml @@ -69,7 +69,7 @@ struct 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 @@ -79,24 +79,13 @@ 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 - in + 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_ @@ -107,12 +96,8 @@ struct if_ is_right ~typ:Boolean.typ ~then_:acc ~else_:is_valid_left ) in let* () = - match check with - | Some check -> - if_ check ~typ:Boolean.typ ~then_:is_y_most_left ~else_:Boolean.true_ - >>= Boolean.Assert.is_true - | None -> - Checked.return () + 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