New design integration into the sequencer

src/app/zeko/circuits/ase.ml

@@ -6,7 +6,8 @@ open Zeko_util
 
 module M_with_length = struct
   module Stmt = struct
-    type t = { action_state : F.t; length : Checked32.t } [@@deriving snarky]
+    type t = { action_state : F.t; length : Checked32.t }
+    [@@deriving snarky, yojson]
   end
 
   module Elem = F
@@ -32,7 +33,7 @@ module M_with_length = struct
 
   let extend_option_iterations = Int.pow 2 9
 
-  let override_wrap_domain = None
+  let override_wrap_domain = Some `N1
 end
 
 module M_without_length = struct
@@ -57,7 +58,7 @@ module M_without_length = struct
 
   let extend_option_iterations = Int.pow 2 10
 
-  let override_wrap_domain = None
+  let override_wrap_domain = Some `N1
 end
 
 module Made_without_length = Folder.Make (M_without_length) ()
@@ -109,6 +110,14 @@ module With_length = struct
           ~length:target.length
       in
       (({ source; target } : Stmt.var), verifier)
+
+    let fold (source : Init.t) actions =
+      Made_2.fold ~source ~init_arg:source ~elems:actions
+        ~step_state:(fun acc action ->
+          { action_state =
+              Mina_base.Zkapp_account.Actions.push_hash acc.action_state action
+          ; length = Checked32.succ acc.length
+          } )
   end
 end
 
@@ -146,5 +155,10 @@ module Without_length = struct
       let source = Action_state.unsafe_var_of_field source in
       let target = Action_state.unsafe_var_of_field target in
       (({ source; target } : Stmt.var), verifier)
+
+    let fold (source : Init.t) actions =
+      Made_2.fold ~source ~init_arg:source ~elems:actions
+        ~step_state:(fun acc action ->
+          Mina_base.Zkapp_account.Actions.push_hash acc action )
   end
 end

src/app/zeko/circuits/ase.mli

@@ -5,9 +5,12 @@ open Zeko_util
 
 module With_length : sig
   module Stmt : sig
-    type t = { action_state : F.t; length : Checked32.t } [@@deriving snarky]
+    type t = { action_state : F.t; length : Checked32.t }
+    [@@deriving snarky, yojson]
   end
 
+  module Init = Stmt
+
   type trans = { source : Stmt.t; target : Stmt.t }
 
   val leaf : field list * Stmt.t -> (trans * Proof.t) Promise.t
@@ -69,11 +72,14 @@ module With_length : sig
          ?check:Zeko_util.Boolean.var
       -> var
       -> (Stmt.var * tag_var Compile_simple.prev) Checked.t
+
+    val fold : Init.t -> field list -> t Promise.t
   end
 end
 
 module Without_length : sig
   module Stmt = F
+  module Init = Stmt
 
   type trans = { source : field; target : field }
 
@@ -132,5 +138,7 @@ module Without_length : sig
          ?check:Zeko_util.Boolean.var
       -> var
       -> (Stmt.var * tag_var Compile_simple.prev) Checked.t
+
+    val fold : Init.t -> field list -> t Promise.t
   end
 end

src/app/zeko/circuits/bridge_rules.ml

@@ -64,6 +64,10 @@ struct
             ; Rule_bridge_enable.rule
             ]
           () )
+
+  (* FIXME: remove for lazy compilation *)
+  let () =
+    Promise.block_on_async_exn (fun () -> Compile_simple.force_tag System.tag)
 end
 
 module Make_custom (Inputs : sig
@@ -132,4 +136,8 @@ struct
             ; Rule_bridge_enable.rule
             ]
           () )
+
+  (* FIXME: remove for lazy compilation *)
+  let () =
+    Promise.block_on_async_exn (fun () -> Compile_simple.force_tag System.tag)
 end

src/app/zeko/circuits/compile_simple.ml

@@ -7,6 +7,8 @@ type self_width = Pickles_types.Nat.N2.n
 module Proof = struct
   include Pickles.Side_loaded.Proof
 
+  let to_pickles x = x
+
   let of_pickles x = x
 end
 
@@ -20,6 +22,8 @@ module Verification_key = struct
 
   let of_pickles x = x
 
+  let to_pickles x = x
+
   let var_of_pickles x = x
 
   let of_tag (Tag tag) = of_compiled_promise tag
@@ -621,7 +625,7 @@ let compile (type out_t out_var first_input branches n_available_branches)
        with type out_t = out_t
         and type out_var = out_var
         and type branches = (first_input, branches) cons_branch ) =
-  printf "(compile_simple) called for circuit %s\n" name ;
+  printf "(compile_simple) called for circuit %s\n%!" name ;
   assert (Run.in_checked_computation () |> not) ;
   assert (Run.in_prover () |> not) ;
   let (Count_branches_result tag_branches) = count_branches branches in

src/app/zeko/circuits/compile_simple.mli

@@ -1,6 +1,8 @@
 module Proof : sig
   type t [@@deriving yojson]
 
+  val to_pickles : t -> Pickles.Side_loaded.Proof.t
+
   val of_pickles : Pickles.Side_loaded.Proof.t -> t
 end
 
@@ -17,6 +19,8 @@ module Verification_key : sig
 
   val of_pickles : Pickles.Side_loaded.Verification_key.t -> t
 
+  val to_pickles : t -> Pickles.Side_loaded.Verification_key.t
+
   val var_of_pickles : Pickles.Side_loaded.Verification_key.Checked.t -> var
 
   val of_tag : 'tag_var tag -> t Promise.t

src/app/zeko/circuits/dune

@@ -7,6 +7,7 @@
   core_kernel
   transaction_snark
   staged_ledger_diff
+  zeko_constants
   )
  (inline_tests)
  (instrumentation

src/app/zeko/circuits/folder.ml

@@ -239,6 +239,10 @@ struct
             ]
           ~out_typ:Trans.typ () )
 
+  (* FIXME: remove for lazy compilation *)
+  let () =
+    Promise.block_on_async_exn (fun () -> Compile_simple.force_tag System.tag)
+
   type tag_var = System.tag_var
 
   type tag_t = System.tag_t
@@ -298,5 +302,53 @@ struct
           { source = proof_source; target = proof_target }
       in
       ({ init_arg; t; excess } : t)
+
+    let fold ~source ~init_arg ~elems ~step_state =
+      let elems_to_prove, excess =
+        let i = ref 0 in
+        let l = List.length elems in
+        List.split_while elems ~f:(fun _ ->
+            let r = !i < l - get_iterations in
+            i := !i + 1 ;
+            r )
+      in
+      match elems_to_prove with
+      | [] ->
+          (* No need for folding, everything goes to excess *)
+          let proof_target = List.fold excess ~init:source ~f:step_state in
+          Promise.return
+            (make ?proof:None ~proof_source:source ~proof_target init_arg excess)
+      | elems_to_prove ->
+          (* Need to fold *)
+          let leaf_prover, (leaf_elems, rest) =
+            match List.length elems_to_prove with
+            | full_leaf when full_leaf > leaf_iterations ->
+                (leaf, List.split_n elems_to_prove leaf_iterations)
+            | _incomplete_leaf ->
+                (leaf_option, List.split_n elems_to_prove leaf_option_iterations)
+          in
+          let%bind.Promise leaf = leaf_prover (leaf_elems, source) in
+          let rec extend_rest elems_to_prove acc =
+            match elems_to_prove with
+            | [] ->
+                Promise.return acc
+            | elems_to_prove ->
+                let extend_prover, (extend_elems, rest) =
+                  match List.length elems_to_prove with
+                  | full_extend when full_extend > extend_iterations ->
+                      (extend, List.split_n elems_to_prove extend_iterations)
+                  | _incomplete_extend ->
+                      ( extend_option
+                      , List.split_n elems_to_prove extend_option_iterations )
+                in
+                let%bind.Promise acc = extend_prover (extend_elems, acc) in
+                extend_rest rest acc
+          in
+          let%bind.Promise trans, proof = extend_rest rest leaf in
+          let proof_target =
+            List.fold excess ~init:trans.target ~f:step_state
+          in
+          Promise.return
+            (make ~proof ~proof_source:source ~proof_target init_arg excess)
   end
 end

src/app/zeko/circuits/folder.mli

@@ -116,5 +116,12 @@ end)
       -> t
 
     val get_iterations : int
+
+    val fold :
+         source:Stmt.t
+      -> init_arg:Init.t
+      -> elems:Elem.t list
+      -> step_state:(Stmt.t -> Elem.t -> Stmt.t)
+      -> t Promise.t
   end
 end

src/app/zeko/circuits/indexed_merkle_tree.ml

@@ -16,7 +16,7 @@ struct
     type t = { key : Key.t; next_key : Key.t } [@@deriving snarky]
   end
 
-  type t = F.t
+  type t = F.t [@@deriving yojson, sexp]
 
   type var = F.var
 
@@ -33,7 +33,8 @@ struct
         let length = height
       end)
 
-  let hash_entry = var_to_hash ~init:"indexed merkle tree entry hash" Entry.typ
+  let hash_entry =
+    var_to_hash ~init:Zeko_constants.indexed_merkle_tree_salt Entry.typ
 
   let implied_root_raw (init : F.var) (path : Path.var) : F.var Checked.t =
     Checked.List.fold path ~init ~f:(fun acc { hash; is_left } ->

src/app/zeko/circuits/indexed_merkle_tree.mli

@@ -27,7 +27,7 @@ module Make (Inputs : sig
 end) : sig
   open Inputs
 
-  type t
+  type t = F.t [@@deriving yojson, sexp]
 
   type var
 

src/app/zeko/circuits/inner_rules.ml

@@ -3,3 +3,6 @@ include
           ~out_typ:Snark_params.Tick.Typ.(Mina_base.Zkapp_statement.typ * V.typ)
           ~name:"Inner_rules" ~override_wrap_domain:`N0
           ~branches:[ Rule_inner_sync.rule; Rule_inner_action_witness.rule ] )
+
+(* FIXME: remove for lazy compilation *)
+let () = Promise.block_on_async_exn (fun () -> Compile_simple.force_tag tag)

src/app/zeko/circuits/outer_rules.ml

@@ -20,3 +20,6 @@ include
           ~branches:
             [ Rule_commit_inst.rule; Rule_action_witness.rule; Rule_pause.rule ]
           ~name:"Outer_rules" )
+
+(* FIXME: remove for lazy compilation *)
+let () = Promise.block_on_async_exn (fun () -> Compile_simple.force_tag tag)

src/app/zeko/circuits/rollup_state.ml

@@ -141,6 +141,8 @@ module Inner_state = struct
         Outer_action_state.With_length.unsafe_value_of_fields ~state ~length
     }
 
+  let value_to_init_state t = Zeko_util.value_to_init_state typ t
+
   type fine = { outer_action_state : Outer_action_state.With_length.fine }
 
   (* NB! This will warn you if add a field to `t` without fixing it here.
@@ -234,6 +236,8 @@ module Outer_state = struct
     ; Whole (Even_PC.typ, da_key)
     ; Whole (Zeko_transaction_snark.Account_set.typ, acc_set)
     ]
+
+  let value_to_app_state t = Zeko_util.value_to_app_state typ t
 end
 
 module Outer_action = struct

src/app/zeko/circuits/rule_bridge_finalize_cancelled_deposit.ml

@@ -92,6 +92,9 @@ struct
                 Typ.(
                   Ase_outer_inst.Stmt.typ * Ase_outer_with_length_inst.Stmt.typ)
               () )
+
+    (* FIXME: remove for lazy compilation *)
+    let () = Promise.block_on_async_exn (fun () -> Compile_simple.force_tag tag)
   end
 
   module Check_accepted_params = struct
@@ -133,6 +136,9 @@ struct
                   Check_accepted.Definition.Stmt.typ
                   * Ase_outer_with_length_inst.Stmt.typ)
               () )
+
+    (* FIXME: remove for lazy compilation *)
+    let () = Promise.block_on_async_exn (fun () -> Compile_simple.force_tag tag)
   end
 
   module Witness = struct

src/app/zeko/circuits/rule_commit.ml

@@ -10,14 +10,14 @@ open Checked.Let_syntax
 module Ase_outer_inst = Ase.Without_length.Make (struct
   module Action_state = Outer_action_state
 
-  let get_iterations = Int.pow 2 14
+  let get_iterations = Int.pow 2 10
 end)
 
 (** Used to prove the length of the inner action state as stored on the outer account. *)
 module Ase_inner_inst = Ase.With_length.Make (struct
   module Action_state = Inner_action_state
 
-  let get_iterations = Int.pow 2 14
+  let get_iterations = Int.pow 2 10
 end)
 
 (** Proves both Ase_outer_inst and Ase_inner_inst, to circumvent limitation of two recursive proof verifications per proof. *)
@@ -38,9 +38,13 @@ module Verify_both_ases = struct
     }
 
   include
-    ( val Compile_simple.compile ~name:"Verify_both_ases" ~branches:[ rule ]
+    ( val Compile_simple.compile ~override_wrap_domain:`N1
+            ~name:"Verify_both_ases" ~branches:[ rule ]
             ~out_typ:Typ.(Ase_outer_inst.Stmt.typ * Ase_inner_inst.Stmt.typ)
             () )
+
+  (* FIXME: remove for lazy compilation *)
+  let () = Promise.block_on_async_exn (fun () -> Compile_simple.force_tag tag)
 end
 
 module Make (Inputs : sig

src/app/zeko/circuits/zeko_transaction_snark.ml

@@ -359,7 +359,7 @@ module Local_state = struct
     ; excess : Currency.Amount.Signed.t
     ; account_update_index : Account_update_index.t
     }
-  [@@deriving snarky]
+  [@@deriving snarky, yojson]
 
   let to_mina_var ~supply_increase
       { ledger
@@ -410,11 +410,21 @@ module Zeko_stmt = struct
     ; source_local_state : Local_state.t
     ; target_local_state : Local_state.t
     }
-  [@@deriving snarky]
+  [@@deriving snarky, yojson]
 end
 
 module T = struct
   type t = { stmt : Zeko_stmt.t; proof : Proof_V.t } [@@deriving snarky]
+
+  let to_yojson ({ stmt; proof } : t) =
+    `Assoc
+      [ ("stmt", Zeko_stmt.to_yojson stmt); ("proof", Proof.to_yojson proof) ]
+
+  let of_yojson json =
+    let open Ppx_deriving_yojson_runtime in
+    let stmt = Zeko_stmt.of_yojson json in
+    let proof = Proof.of_yojson json in
+    stmt >>= fun stmt -> proof >>= fun proof -> Ok ({ stmt; proof } : t)
 end
 
 type update_acc_set_witness =
@@ -972,3 +982,6 @@ include
             ; { branch_name = "merge"; tags = Two_tags_own; main = rule_merge }
             ]
           () )
+
+(* FIXME: remove for lazy compilation *)
+let () = Promise.block_on_async_exn (fun () -> Compile_simple.force_tag tag)