Skip to content

Fix imt skipping #350

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: compatible
Choose a base branch
from
Open

Fix imt skipping #350

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
541701f
Fix not checking the right case
MartinOndejka Sep 4, 2025
36039b9
Optimize the checks
MartinOndejka Sep 4, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
18 changes: 12 additions & 6 deletions src/app/zeko/circuits/indexed_merkle_tree.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -88,12 +88,18 @@ struct
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 )
(* if is_right, then hash_other != empty_hash, else hash_other == empty_hash
<=> (!(empty_hash == hash_other) && is_right) || (empty_hash == hash_other && !is_right) .\ A := empty_hash == hash_other, B := is_right
<=> (!A && B) || (A && !B)
<=> !(A == B)
<=> not (empty_hash == hash_other && is_right)*)
let* checks =
Checked.List.map (List.zip_exn path_y empty_path)
~f:(fun (PathStep.{ hash_other; is_right }, empty_hash) ->
Field.Checked.equal empty_hash hash_other
>>= Boolean.( &&& ) is_right >>| Boolean.not )
in
Boolean.all checks
Copy link
Collaborator

@L-as L-as Sep 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

There should probably be a comment explaining the logic.
Whenever we replace an empty account with a non-empty account, it must be that all accounts before it must be non-empty.
We can define this inductively.
For the depth 0 ledger of one account, the condition always holds.
For the depth 1 ledger of two accounts, we can only fill the right account if the left account isn't the empty account.
For the depth 2 ledger of four accounts, we can only fill, if the account is in the left subtree, then the same condition as above, otherwise it's the same condition as above but also the left subtree must not have any empty accounts.

Consider then your above code.

If only index (left, left) is non-empty,
and we then insert into (right, left) instead of (left, right),
I think the checks would all succeed, because it's not empty hash for the first level,
and it's left for the second level.

Also you could reformulate it as empty_hash != hash_other || is_left to make it simpler.

You probably need another field in the outer account to keep track of the right-most account,
such that if you make a new account, then the index must be last + 1, and then update it appropriately.

The above code checks that the trees on right are all empty,
but it doesn't correctly check that there are no empty subtrees on the left.

in
let* () =
if_ check ~typ:Boolean.typ ~then_:is_y_most_left ~else_:Boolean.true_
Expand Down