Forbid skipping of indices in account set

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)
 

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

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 () ->