1. 引言

前序博客有：

Mina技术白皮书

所谓wrap snark，是将Tick snark（Mina代码中称为step proof）包裹为Tock snark（Mina代码中称为wrap proof）。
wrap snark的目的是：将一个Tick snark 包裹为一个Tock snark，以便用另一个Tick snark就能证明它。

Tick snark对应的场景为：

public 输入：x,πtickx, \pi_{\text{tick}}x,πtick
witness：www
待证明relation：Verifytick((x,πtick);w)=true\text{Verify}_{\text{tick}}((x,\pi_{\text{tick}});w) = \text{true}Verifytick((x,πtick);w)=true

经Wrap snark包裹为Tock snark对应的场景为：

public 输入：x,πtockx,\pi_{\text{tock}}x,πtock
witness：w,πtickw, \pi_{\text{tick}}w,πtick
待证明relation：Verifytick((x,πtock);(w,πtick))=true\text{Verify}_{\text{tick}}((x,\pi_{\text{tock}});(w, \pi_{\text{tick}})) = \text{true}Verifytick((x,πtock);(w,πtick))=true

1.1 关键约束电路

1）Boolean.Assert.any对应的约束为：

     let%snarkydef_ any (bs : var list) =assert_non_zero (Cvar.sum (bs :> Cvar.t list))let%snarkydef_ assert_non_zero (v : Cvar.t) =let open Let_syntax inlet%map _ = inv v in()(* We get a better stack trace by failing at the call to is_satisfied, so weput a bogus value for the inverse to make the constraint system unsat ifx is zero. *)let inv ?(label = "Checked.inv") (x : Cvar.t) =match x with| Constant x ->return (Cvar.constant (Field.inv x))| _ ->with_label label(let open Let_syntax inlet%bind x_inv =exists Typ.field~compute:As_prover.(map (read_var x) ~f:(fun x ->if Field.(equal zero x) then Field.zeroelse Backend.Field.inv x))inlet%map () =assert_r1cs ~label:"field_inverse" x x_inv(Cvar.constant Field.one)inx_inv)let assert_r1cs ?label a b c = assert_ (Constraint.r1cs ?label a b c)let r1cs ?label a b c = [ create_basic ?label (R1CS (a, b, c)) ]let create_basic ?label basic = { basic; annotation = label }let assert_ ?label c = (* 返回的为Add_constraint 枚举类型 *)add_constraint (List.map c ~f:(fun c -> Constraint.override_label c label))let add_constraint c = Add_constraint (c, return ())

1.2 wrap_main.main函数内关键代码

wrap_main.main函数内incrementally_verify_proof时prev_statement的结构为：

{ proof_state = { unfinalized_proofs; me_only }; pass_through }(* 其中unfinalized_proofs结构为：Step.Proof_state.Per_proof.In_circuit.t *){ deferred_values ={ xi; bulletproof_challenges; b; combined_inner_product; plonk ={ alpha; beta; gamma; zeta; zeta_to_srs_length; zeta_to_domain_size; poseidon_selector; vbmul; complete_add; endomul; endomul_scalar; perm; generic}}; should_finalize; sponge_digest_before_evaluations}(* 相应的Step.Proof_state.Per_proof.In_circuit.t spec为： *)let spec bp_log2 = (* bp_log2取Backend.Tock.Rounds.n，值为15 *)let open Spec inStruct[ Vector (B Field, Nat.N19.n); Vector (B Digest, Nat.N1.n); Vector (B Challenge, Nat.N2.n); Vector (Scalar Challenge, Nat.N3.n); Vector (B Bulletproof_challenge, bp_log2); Vector (B Bool, Nat.N1.n)]

2. 关键代码

调用o1-labs/proof-systems的接口（如caml_pasta_fq_plonk_proof_create），生成的proof为Kimchi_types.prover_proof结构：【其中commitments.w_comm有15个poly_comm。】

type t = (Curve.Affine.Backend.t, Scalar_field.t) Kimchi_types.prover_prooftype nonrec ('caml_g, 'caml_f) prover_proof ={ commitments : 'caml_g prover_commitments; proof : ('caml_g, 'caml_f) opening_proof; evals : 'caml_f proof_evaluations * 'caml_f proof_evaluations; ft_eval1 : 'caml_f; public : 'caml_f array; prev_challenges : ('caml_f array * 'caml_g poly_comm) array}type nonrec 'caml_g prover_commitments ={ w_comm :'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm* 'caml_g poly_comm; z_comm : 'caml_g poly_comm; t_comm : 'caml_g poly_comm}type nonrec 'caml_g poly_comm ={ unshifted : 'caml_g array; shifted : 'caml_g option }type nonrec ('g, 'f) opening_proof ={ lr : ('g * 'g) array; delta : 'g; z1 : 'f; z2 : 'f; sg : 'g }type nonrec 'caml_f proof_evaluations ={ w :'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array; z : 'caml_f array; s :'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array* 'caml_f array; generic_selector : 'caml_f array; poseidon_selector : 'caml_f array}

基础类型：uint、field、snarkless、as_prover、sgn、Inner_curve/Snarky_curve 等 typ的基本定义为：

 let unit () : (unit, unit, 'field) t =Typ{ var_to_fields = (fun () -> ([||], ())); var_of_fields = (fun _ -> ()); value_to_fields = (fun () -> ([||], ())); value_of_fields = (fun _ -> ()); size_in_field_elements = 0; constraint_system_auxiliary = (fun () -> ()); check = (fun () -> Checked.return ())}let field () : ('field Cvar.t, 'field, 'field) t =Typ{ var_to_fields = (fun f -> ([| f |], ())); var_of_fields = (fun (fields, _) -> fields.(0)); value_to_fields = (fun f -> ([| f |], ())); value_of_fields = (fun (fields, _) -> fields.(0)); size_in_field_elements = 1; constraint_system_auxiliary = (fun () -> ()); check = (fun _ -> Checked.return ())}let snarkless value : _ t =Typ{ var_to_fields = (fun _ -> ([||], ())); var_of_fields = (fun _ -> value); value_to_fields =(fun value' ->assert (phys_equal value value') ;([||], ())); value_of_fields = (fun _ -> value); size_in_field_elements = 0; constraint_system_auxiliary = (fun () -> ()); check = (fun _ -> Checked.return ())}(* as_prover.typ定义： *)let typ : ('a t, 'a, _) Types.Typ.t =Typ{ var_to_fields = (fun x -> ([||], !x)); var_of_fields = (fun (_, x) -> ref x); value_to_fields = (fun x -> ([||], Some x)); value_of_fields = (fun (_, x) -> Option.value_exn x); size_in_field_elements = 0; constraint_system_auxiliary = (fun () -> None); check = (fun _ -> Checked.return ())}(* sgn.typ定义： *)let typ : (var, t) Typ.t =let open Typ inTyp{ check = (fun x -> assert_r1cs x x (Field.Var.constant Field.one)); var_to_fields = (fun t -> ([| t |], ())); var_of_fields = (fun (ts, ()) -> ts.(0)); value_to_fields = (fun t -> ([| to_field t |], ())); value_of_fields = (fun (ts, ()) -> of_field_exn ts.(0)); size_in_field_elements = 1; constraint_system_auxiliary = (fun () -> ())}(* Inner_curve.typ定义为：*)let typ : (t, Constant.t) Typ.t =let (Typ typ_unchecked) = typ_unchecked inTyp{ typ_unchecked withcheck = (fun t -> make_checked (fun () -> assert_on_curve t))}

构建约束系统关键是其中的check函数，如：

1）Boolean typ有：

let typ : (var, value) Typ.t =let (Typ typ) =Typ.field|> Typ.transport~there:(function true -> Field.one | false -> Field.zero)~back:(fun x -> if Field.equal x Field.zero then false else true)|> Typ.transport_var~there:(fun (b : var) -> (b :> Cvar.t))~back:createinTyp{ typ withcheck =(fun v ->Checked.assert_(Constraint.boolean ~label:"boolean-alloc" (v :> Cvar.t)))}

2）Checked_runner中的let rec run函数内会再次定义check函数check = (fun var -> run (check var))：

| Exists( Typ{ var_to_fields; var_of_fields; value_to_fields; value_of_fields; size_in_field_elements; constraint_system_auxiliary; check}, p, k ) ->let typ =Types.Typ.Typ{ var_to_fields; var_of_fields; value_to_fields; value_of_fields; size_in_field_elements; constraint_system_auxiliary; check = (fun var -> run (check var))}inlet s, y = handle_error s (fun () -> exists typ p s) inlet k = handle_error s (fun () -> k y) inrun k s

3）snarky_curve.ml中Make_checked的typ为：

let typ : (t, Constant.t) Typ.t =
let (Typ typ_unchecked) = typ_unchecked in
Typ{ typ_unchecked withcheck = (fun t -> make_checked (fun () -> assert_on_curve t))}

4）one_hot_vector.ml中Make的typ为：

let typ (n : 'n Nat.t) : ('n t, Constant.t) Typ.t =
let (Typ typ) = Vector.typ Boolean.typ n in
let typ : _ Typ.t =Typ{ typ withcheck =(fun x ->Snarky_backendless.Checked.bind (typ.check x) ~f:(fun () ->make_checked (fun () ->Boolean.Assert.exactly_one (Vector.to_list x) ) ) )}
in
Typ.transport typ~there:(fun i -> Vector.init n ~f:(( = ) i))~back:(fun v ->let i, _ =List.findi (Vector.to_list v) ~f:(fun _ b -> b) |> Option.value_exnini )

5）impls.ml中Step的check为：

let check t =let open Internal_Basic inlet open Let_syntax inlet equal (x1, b1) (x2, b2) =let%bind x_eq = Field.Checked.equal x1 (Field.Var.constant x2) inlet b_eq = match b2 with true -> b1 | false -> Boolean.not b1 inBoolean.( && ) x_eq b_eqinlet (Typ typ_unchecked) = typ_unchecked inlet%bind () = typ_unchecked.check t inChecked.List.map forbidden_shifted_values ~f:(equal t)>>= Boolean.any >>| Boolean.not >>= Boolean.Assert.is_true

6）impls.ml中Wrap的check为：

let check t =let open Internal_Basic inlet open Let_syntax inlet equal x1 x2 = Field.Checked.equal x1 (Field.Var.constant x2) inlet%bind () = t0.check t inChecked.List.map forbidden_shifted_values ~f:(equal t)>>= Boolean.any >>| Boolean.not >>= Boolean.Assert.is_true

7）mina_numbers/nat.ml中Make_checked的typ为：

let typ : (var, N.t) Typ.t =
let (Typ field_typ) = Field.typ in
Typ.transport(Typ { field_typ with check = range_check })~there:to_field ~back:of_field

8）Inner_curve.typ的check为：

let typ : (t, Constant.t) Typ.t =let (Typ typ_unchecked) = typ_unchecked inTyp{ typ_unchecked withcheck = (fun t -> make_checked (fun () -> assert_on_curve t))}

assert_、assert_r1cs、assert_square、assert_all、assert_equal对应的均为 let add_constraint c = Add_constraint (c, return ())类型。

调用exists也会构建约束系统：【会运行run->Runner.run函数，%map会调用checked.ml中的let rec map函数，%bind会调用checked.ml中的let rec bind函数。】

 let exists ?request ?compute typ =let request = Option.map request ~f:As_prover.run_prover inlet compute = Option.map compute ~f:As_prover.run_prover inrun (exists ?request ?compute typ)let exists ?request ?compute typ =let%map h = exists_handle ?request ?compute typ inHandle.var hlet exists_handle ?request ?compute typ =let provider =let request =Option.value request ~default:(As_prover.return Request.Fail)inmatch compute with| None ->Types.Provider.Request request| Some c ->Types.Provider.Both (request, c)inexists typ provider           let exists typ p = Exists (typ, p, return)let run (checked : _ Checked.t) =match checked with| Pure x ->x| _ ->if not (is_active_functor_id this_functor_id) thenfailwithf"Could not run this function.\n\n\Hint: The module used to create this function had internal ID \%i, but the module used to run it had internal ID %i. The same \instance of Snarky.Snark.Run.Make must be used for both."this_functor_id (active_functor_id ()) ()else if not !state.is_running thenfailwith"This function can't be run outside of a checked computation." ;let () = Printf.printf "BEFORE ZYD run_checked Runner.run, state.next_auxiliary:%d\n" !(!state.next_auxiliary) inlet state', x = Runner.run checked !state inlet () = Printf.printf "AFTER ZYD run_checked Runner.run, state.next_auxiliary:%d\n" !(!state.next_auxiliary) instate := state' ;x

即wrap_main.main等函数内调用exists会构建Exists (typ, p, return)，而在 Runner.run时，会对Exists类型调用checked_runner.ml中Make_checked的exists函数：【若只是构建约束系统，走ELSE分支；若生成证明，即has_witness为true，走IF分支。】

 let exists(Types.Typ.Typ{ Types.Typ.var_of_fields; value_to_fields; size_in_field_elements; check; constraint_system_auxiliary; _}) p s =if s.has_witness then (let () = Printf.printf "IF ZYD exists s.has_witness: %b\n" s.has_witness inlet old = !(s.as_prover) ins.as_prover := true ;let value = As_prover.Provider.run p s.stack (get_value s) s.handler ins.as_prover := old ;let var =let store_value =if !(s.as_prover) then(* If we're nested in a prover block, create constants instead ofstoring.*)Cvar.constantelse store_field_elt sinlet fields, aux = value_to_fields value inlet field_vars = Array.map ~f:store_value fields invar_of_fields (field_vars, aux)in(* TODO: Push a label onto the stack here *)let s, () = check var s in(s, { Handle.var; value = Some value }) )elselet () = Printf.printf "ELSE ZYD exists s.has_witness: %b, size_in_field_elements:%d\n" s.has_witness size_in_field_elements inlet var =var_of_fields( Array.init size_in_field_elements ~f:(fun _ -> alloc_var s ()), constraint_system_auxiliary () )in(* TODO: Push a label onto the stack here *)let s, () = check var s in(s, { Handle.var; value = None })

Field.equal函数会调用：【对于非常量equal，会调用exists->run，Typ.(field * field)对应的size_in_field_elements为2。】

let equal (x : Cvar.t) (y : Cvar.t) : Cvar.t Boolean.t t =match (x, y) with| Constant x, Constant y ->let () = Printf.printf "ZYD checked equal Constant\n" inChecked.return(Boolean.Unsafe.create(Cvar.constant(if Field.equal x y then Field.one else Field.zero)))| _ ->let () = Printf.printf "ZYD checked equal non constant\n" inlet z = Cvar.(x - y) inlet%bind r, inv =exists Typ.(field * field) ~compute:(equal_vars z)inlet%map () = equal_constraints z inv r inBoolean.Unsafe.create r

2.0 Impls.Step.input()函数以及Impls.Wrap.input()函数

1）Impls.Step.input()函数内，对应的to_data为Step.Statement内的to_data()函数：

let to_data { proof_state = { unfinalized_proofs; me_only }; pass_through }=let () = Printf.printf "ZYD Step.Statement to_data\n"  inlet open Hlist.HlistId in[ Vector.map unfinalized_proofs~f:Proof_state.Per_proof.In_circuit.to_data; me_only; pass_through](* Step.Proof_state.Per_proof.In_circuit.to_data()函数对应为： *)let to_data({ deferred_values ={ xi; bulletproof_challenges; b; combined_inner_product; plonk ={ alpha; beta; gamma; zeta; zeta_to_srs_length; zeta_to_domain_size; poseidon_selector; vbmul; complete_add; endomul; endomul_scalar; perm; generic}}; should_finalize; sponge_digest_before_evaluations} :_ t ) =let open Vector inlet fq =combined_inner_product :: b :: zeta_to_srs_length:: zeta_to_domain_size :: poseidon_selector :: vbmul :: complete_add:: endomul :: endomul_scalar :: perm :: genericinlet challenge = [ beta; gamma ] inlet scalar_challenge = [ alpha; zeta; xi ] inlet digest = [ sponge_digest_before_evaluations ] inlet bool = [ should_finalize ] inlet open Hlist.HlistId in[ fq; digest; challenge; scalar_challenge; bulletproof_challenges; bool]

2）Impls.Wrap.input()函数内，对应的to_data为Wrap.Statement.In_circuit内的to_data()函数

(** Convert a statement (as structured data) into the flat data-based representation. *)let to_data({ proof_state ={ deferred_values ={ xi; combined_inner_product; b; branch_data; bulletproof_challenges; plonk ={ alpha; beta; gamma; zeta; zeta_to_srs_length; zeta_to_domain_size; poseidon_selector; vbmul; complete_add; endomul; endomul_scalar; perm; generic}}; sponge_digest_before_evaluations; me_only(* me_only is represented as a digest (and then unhashed) inside the circuit *)}; pass_through(* pass_through is represented as a digest inside the circuit *)} :_ t ) =let open Vector inlet fp =combined_inner_product :: b :: zeta_to_srs_length:: zeta_to_domain_size :: poseidon_selector :: vbmul :: complete_add:: endomul :: endomul_scalar :: perm :: genericinlet challenge = [ beta; gamma ] inlet scalar_challenge = [ alpha; zeta; xi ] inlet digest =[ sponge_digest_before_evaluations; me_only; pass_through ]inlet index = [ branch_data ] inHlist.HlistId.[ fp; challenge; scalar_challenge; digest; bulletproof_challenges; index]

2.1 pickles_base.domain模块

domain结构定义为：

type t = Pow_2_roots_of_unity of int

let tag, cache_handle, p, Pickles.Provers.[ step ] =Pickles.compile ~cache:Cache_dir.cache(module Statement_var)(module Statement)~typ~branches:(module Nat.N1)~max_proofs_verified:(module Nat.N2)~name:"blockchain-snark"~constraint_constants:(Genesis_constants.Constraint_constants.to_snark_keys_headerconstraint_constants )~choices:(fun ~self ->[ rule ~proof_level ~constraint_constants T.tag self ] )

根据调用Pickles.compile时的max_proofs_verified参数，相应的wrap_domain取值为：

let wrap_domains ~proofs_verified =let h =match proofs_verified with 0 -> 13 | 1 -> 14 | 2 -> 15 | _ -> assert falsein{ Domains.h = Pow_2_roots_of_unity h }

如compile时参数为~max_proofs_verified:(module Nat.N2)，对应的wrap_domains为：

ZYD wrap_domains:{"h":["Pow_2_roots_of_unity",15]}

如compile时参数为~branches:(module Nat.N1)，对应的prev_varss_n和proofs_verified为：【prev_varss_n和proofs_verified数组长度与 branches参数以及choices参数中rule数组的个数一致。】

ZYD prev_varss_n:1
ZYD proofs_verifieds:1

2.2 pickles.wrap_main_inputs模块

pickles.wrap_main_inputs模块主要针对的是Tock曲线。其中的Other模块针对的为Tick曲线。
其中主要包含了：

Sponge模块
Input_domain模块
Inner_curve模块：对应为Tick曲线
Generators模块

2.3 pickles.wrap_verifier模块

pickles.wrap_verifier模块实现了challenge_polynomial函数：

(* given [chals], compute\prod_i (1 + chals.(i) * x^{2^{k - 1 - i}}) *)
let challenge_polynomial ~one ~add ~mul chals = ......

pickles.wrap_verifier模块中的Make模块内定义了：

print_g等打印函数
product、absorb、scalar_to_field、squeeze_challenge、squeeze_scalar等函数
assert_n_bits、lowest_128_bits、equal_g、mask、assert_eq_marlin、shift1、shift2等函数
bullet_reduce、lagrange、lagrange_with_correction、h_precomp、group_map、map_challenges等函数
choose_key、scale_fast、check_bulletproof、iter2、pow2pow、map_plonk_to_field等函数
incrementally_verify_proof、mask_evals、combined_evaluation、compute_challenges、actual_evaluation等函数

finalize_other_proof函数：

(* This finalizes the "deferred values" coming from a previous proof over the same field.It1. Checks that [xi] and [r] where sampled correctly. I.e., by absorbing all theevaluation openings and then squeezing.2. Checks that the "combined inner product" value used in the elliptic curve part ofthe opening proof was computed correctly, in terms of the evaluation openings and theevaluation points.3. Check that the "b" value was computed correctly.4. Perform the arithmetic checks from marlin. *)
let finalize_other_proof (type b)(module Proofs_verified : Nat.Add.Intf with type n = b)?actual_proofs_verified ~domain ~max_quot_size ~sponge~(old_bulletproof_challenges : (_, b) Vector.t)({ xi; combined_inner_product; bulletproof_challenges; b; plonk } :( _, _, _ Shifted_value.Type2.t, _ )Types.Step.Proof_state.Deferred_values.In_circuit.t ){ Plonk_types.All_evals.ft_eval1; evals =( { evals = evals1; public_input = x_hat1 }, { evals = evals2; public_input = x_hat2 } )} = .......

Other_field模块
Challenge模块
Digest模块
Scalar_challenge模块
Ops模块
One_hot_vector模块
Split_commitments模块
Opt模块
Pseudo模块
Plonk模块
Split_evaluations模块
Plonk_checks模块

定义index为Plonk_verification_key_evals类型：

type 'comm t ={ sigma_comm : 'comm Plonk_types.Permuts_vec.Stable.V1.t; coefficients_comm : 'comm Plonk_types.Columns_vec.Stable.V1.t; generic_comm : 'comm; psm_comm : 'comm; complete_add_comm : 'comm; mul_comm : 'comm; emul_comm : 'comm; endomul_scalar_comm : 'comm}

2.4 pickles.wrap_main模块

pickles.wrap_main模块中包含：

1）pad_domains函数：当前假设所有的wrap domains是相同的，当切换到dlog-dlog system时，该函数将有用。

2）Old_bulletproof_chals模块：

module Old_bulletproof_chals = structtype t =| T :'max_local_max_proofs_verified Nat.t* 'max_local_max_proofs_verified Challenges_vector.t-> t
end

3）pack_statement、shifts、domain_generator、split_field_typ、split_field等函数函数：

4）wrap_main函数：为The SNARK function for wrapping any proof coming from the given set of keys。

let wrap_main(type max_proofs_verified branches prev_varss prev_valuess envmax_local_max_proofs_verifieds )(full_signature :( max_proofs_verified, branches, max_local_max_proofs_verifieds )Full_signature.t ) (pi_branches : (prev_varss, branches) Hlist.Length.t)(step_keys :(Wrap_main_inputs.Inner_curve.Constant.t index, branches) Vector.t Lazy.t) (step_widths : (int, branches) Vector.t)(step_domains : (Domains.t, branches) Vector.t)(prev_wrap_domains :(prev_varss, prev_valuess, _, _) H4.T(H4.T(E04(Domains))).t )(module Max_proofs_verified : Nat.Add.Intf with type n = max_proofs_verified):(max_proofs_verified, max_local_max_proofs_verifieds) Requests.Wrap.t* (   ( _, _, _ Shifted_value.Type1.t, _, _, _, _, _, _ )Types.Wrap.Statement.In_circuit.t-> unit ) =

wrap_main的调用方式，返回的分别为wrap_requests（为 (max_proofs_verified, max_local_max_proofs_verifieds) Requests.Wrap.t类型）和wrap_main（输入为Types.Wrap.Statement.In_circuit.t，输出为unit的函数）：

let wrap_requests, wrap_main_main = Wrap_main.wrap_main full_signature prev_varss_length step_vksproofs_verifieds step_domains prev_wrap_domains(module Max_proofs_verified)

其中:

full_signature对应结构为：

(full_signature :( max_proofs_verified, branches, max_local_max_proofs_verifieds )Full_signature.t )

prev_varss_length对应结构为：

(pi_branches : (prev_varss, branches) Hlist.Length.t)

step_vks对应结构为：

(step_keys :(Wrap_main_inputs.Inner_curve.Constant.t index, branches) Vector.t Lazy.t)

proofs_verifieds对应结构为：

(step_widths : (int, branches) Vector.t)

step_domains对应结构为：【step_domains数组的长度与 compile时choices中rule数组的长度一致】
```
(step_domains : (Domains.t, branches) Vector.t)
```

prev_wrap_domains对应结构为：

(prev_wrap_domains :(prev_varss, prev_valuess, _, _) H4.T(H4.T(E04(Domains))).t )

Max_proofs_verified对应结构为：

(module Max_proofs_verified : Nat.Add.Intf with type n = max_proofs_verified)

返回的wrap_requests对应结构为：

(max_proofs_verified, max_local_max_proofs_verifieds) Requests.Wrap.t`

返回的wrap_main_main为函数：

(   ( _, _, _ Shifted_value.Type1.t, _, _, _, _, _, _ )Types.Wrap.Statement.In_circuit.t-> unit )(* Shifted_value.Type1.t结构为： *)type 'f t = Shifted_value of 'f(* Types.Wrap.Statement.In_circuit.t结构为： *)type ( 'challenge, 'scalar_challenge, 'fp, 'fq, 'me_only, 'digest, 'pass_through, 'bp_chals, 'index )t =( ( 'challenge, 'scalar_challenge, 'fp )Proof_state.Deferred_values.Plonk.In_circuit.t, 'scalar_challenge, 'fp, 'fq, 'me_only, 'digest, 'pass_through, 'bp_chals, 'index )Stable.Latest.t
(*  Stable.Latest.t结构为： *)type ( 'plonk, 'scalar_challenge, 'fp, 'fq, 'me_only, 'digest, 'pass_through, 'bp_chals, 'index )t ={ proof_state :( 'plonk, 'scalar_challenge, 'fp, 'fq, 'me_only, 'digest, 'bp_chals, 'index )Proof_state.Stable.V1.t; pass_through : 'pass_through}
(* Proof_state.Deferred_values.Plonk.In_circuit.t结构为： *)(** All scalar values deferred by a verifier circuit.The values in [poseidon_selector], [vbmul], [complete_add], [endomul], [endomul_scalar], [perm], and [generic]are all scalars which will have been used to scale selector polynomials during thecomputation of the linearized polynomial commitment.Then, we expose them so the next guy (who can do scalar arithmetic) can check that theywere computed correctly from the evaluations in the proof and the challenges.*)type ('challenge, 'scalar_challenge, 'fp) t ={ alpha : 'scalar_challenge; beta : 'challenge; gamma : 'challenge; zeta : 'scalar_challenge(* TODO: zeta_to_srs_length is kind of unnecessary.Try to get rid of it when you can.*); zeta_to_srs_length : 'fp; zeta_to_domain_size : 'fp; poseidon_selector : 'fp(** scalar used on the poseidon selector *); vbmul : 'fp  (** scalar used on the vbmul selector *); complete_add : 'fp(** scalar used on the complete_add selector *); endomul : 'fp  (** scalar used on the endomul selector *); endomul_scalar : 'fp(** scalar used on the endomul_scalar selector *); perm : 'fp(** scalar used on one of the permutation polynomial commitments. *); generic : 'fp Generic_coeffs_vec.t(** scalars used on the coefficient column commitments. *)}

2.5 pickles.impls.wrap模块

pickles.impls.wrap模块中包含：

1）Impl模块，为：module Wrap_impl = Snarky_backendless.Snark.Run.Make (Tock)。即wrap模块的实现是基于Tock曲线的。
2）基于Tock曲线的Challenge和Digest模块。
3）模块Wrap_field=Tock.Field，Step_field=Tick.Field。
4）模块Verification_key=Tock.Verification_key，Proving_key=Tock.Proving_key。
5）模块Keypair，提供了generate函数，可根据constraint system生成相应的proving key和verification key。
```
type t = { pk : Proving_key.t; vk : Verification_key.t }
```
6）模块Other_field：
```
type t = Field.t (* 为Tock.Field.t结构 *)
```
- 6.1）模块Constant=Tick.Field
- 6.2）typ_unchecked定义了Tock->Tick与Tick->Tock之间的转换。
- 6.3）check定义了Field域内两个变量是否相等的约束。
- 6.4）typ定义了Typ { typ_unchecked with check }。
- 6.5）to_bits函数将Field值以bits表示。

7）input函数：

let input () =let fp : ('a, Other_field.Constant.t) Typ.t = Other_field.typ_unchecked inlet open Types.Wrap.Statement inlet (T (typ, f, f_inv)) =Spec.packed_typ (* 对应为：let packed_typ impl field t = etyp (packed_typ_basic impl field) t *)(module Impl)(T( Shifted_value.Type1.typ fp, (fun (Shifted_value x as t) ->Impl.run_checked (Other_field.check x) ;t ), Fn.id ) )In_circuit.specinlet typ =Typ.transport typ ~there:In_circuit.to_data ~back:In_circuit.of_datainSpec.ETyp.T( typ, (fun x -> In_circuit.of_data (f x)), fun x -> f_inv (In_circuit.to_data x) )

其中：

(* In_circuit.spec结构为： *)
(** A layout of the raw data in a statement, which is needed forrepresenting it inside the circuit. *)let spec =let open Spec inStruct[ Vector (B Field, Nat.N19.n); Vector (B Challenge, Nat.N2.n); Vector (Scalar Challenge, Nat.N3.n); Vector (B Digest, Nat.N3.n); Vector (B Bulletproof_challenge, Backend.Tick.Rounds.n); Vector (B Branch_data, Nat.N1.n)]

该spec的结构本质是与Wrap.Statement.In_circuit.to_data的输出相对应的，spec中的各个Vector分别对应下面的fp、challenge、scalar_challenge、digest、bulletproof_challenges、index：

### ZYD to_data.total_len:44, fp.length:19, challenge.length:2, scalar_challenge.length:3,
### digest.length:3, bulletproof_challenges.length:16, index.length:1 ###let fp =combined_inner_product :: b :: zeta_to_srs_length:: zeta_to_domain_size :: poseidon_selector :: vbmul :: complete_add:: endomul :: endomul_scalar :: perm :: genericinlet challenge = [ beta; gamma ] inlet scalar_challenge = [ alpha; zeta; xi ] inlet digest =[ sponge_digest_before_evaluations; me_only; pass_through ]inlet index = [ branch_data ] let bulletproof_challenges = [bulletproof_challenges]

(* Etyp结构为： *)
type ('var, 'value, 'f) t =
| T :('inner, 'value, 'f) Snarky_backendless.Typ.t* ('inner -> 'var)* ('var -> 'inner)-> ('var, 'value, 'f) t

其中Env中后缀为1的表示的变量值，后缀为2的表示的变量。

(* (packed_typ_basic impl field) 定义为： *)
let packed_typ_basic (type field other_field other_field_var)(module Impl : Snarky_backendless.Snark_intf.Run with type field = field)(field : (other_field_var, other_field, field) ETyp.t) =let open Impl inlet module Digest = D.Make (Impl) inlet module Challenge = Limb_vector.Challenge.Make (Impl) inlet module Env = structtype ('other_field, 'other_field_var, 'a) t = (* `Env`中后缀为1的表示的变量值，后缀为2的表示的变量。 *)< field1 : 'other_field; field2 : 'other_field_var; bool1 : bool; bool2 : Boolean.var; digest1 : Digest.Constant.t; digest2 : Field.t; challenge1 : Challenge.Constant.t; challenge2 : (* Challenge.t *) Field.t; bulletproof_challenge1 :Challenge.Constant.t Sc.t Bulletproof_challenge.t; bulletproof_challenge2 : Field.t Sc.t Bulletproof_challenge.t; branch_data1 : Branch_data.t; branch_data2 : Field.t; .. >as'aend inlet etyp :type a b.(a, b, ((other_field, other_field_var, 'e) Env.t as 'e)) Basic.t-> (b, a, field) ETyp.t = function| Field ->field| Bool ->T (Boolean.typ, Fn.id, Fn.id)| Digest ->T (Digest.typ, Fn.id, Fn.id)| Challenge ->T (Challenge.typ, Fn.id, Fn.id)| Branch_data ->T (Branch_data.packed_typ (module Impl), Fn.id, Fn.id)| Bulletproof_challenge ->let typ =let there { Bulletproof_challenge.prechallenge = { Sc.inner = pre } }=preinlet back pre ={ Bulletproof_challenge.prechallenge = { Sc.inner = pre } }inTyp.transport Challenge.typ ~there ~back|> Typ.transport_var ~there ~backinT (typ, Fn.id, Fn.id)in{ etyp }

type ('f, 'env) etyp ={ etyp :'var 'value. ('value, 'var, 'env) Basic.t -> ('var, 'value, 'f) ETyp.t}let rec etyp :type f var value env.(f, env) etyp -> (value, var, env) T.t -> (var, value, f) ETyp.t =let open Snarky_backendless.Typ infun e spec ->match spec with| B spec ->e.etyp spec| Scalar chal ->let (T (typ, f, f_inv)) = e.etyp chal inT (Sc.typ typ, Sc.map ~f, Sc.map ~f:f_inv)| Vector (spec, n) ->let (T (typ, f, f_inv)) = etyp e spec inT (Vector.typ typ n, Vector.map ~f, Vector.map ~f:f_inv)| Array (spec, n) ->let (T (typ, f, f_inv)) = etyp e spec inT (array ~length:n typ, Array.map ~f, Array.map ~f:f_inv)| Struct [] ->let open Hlist.HlistId inlet there [] = () inlet back () = [] inT( transport (unit ()) ~there ~back |> transport_var ~there ~back, Fn.id, Fn.id )| Struct (spec :: specs) ->let open Hlist.HlistId inlet (T (t1, f1, f1_inv)) = etyp e spec inlet (T (t2, f2, f2_inv)) = etyp e (Struct specs) inT( tuple2 t1 t2|> transport~there:(fun (x :: xs) -> (x, xs))~back:(fun (x, xs) -> x :: xs), (fun (x, xs) -> f1 x :: f2 xs), fun (x :: xs) -> (f1_inv x, f2_inv xs) )

2.6 snarky.src.base.types.Typ模块

snarky.src.base.types.Typ模块定义为：【typ.Typ会将('var, 'value, 'aux, 'field, 'checked) typ'转换为 ('var, 'value, 'field, 'checked) typ，也就是说，此时已界定了电路的public input和auxiliary input。】

module Typ = structmodule T = struct(** The type [('var, 'value, 'field, 'checked) t] describes a mapping fromOCaml types to the variables and constraints they represent:- ['value] is the OCaml type- ['field] is the type of the field elements- ['var] is some other type that contains some R1CS variables- ['checked] is the type of checked computation that verifies the storedcontents as R1CS variables.For convenience and readability, it is usually best to have the ['var]type mirror the ['value] type in structure, for example:
{[type t = {b1 : bool; b2 : bool} (* 'value *)let or (x : t) = x.b1 || x.b2module Checked = structtype t = {b1 : Snark.Boolean.var; b2 : Snark.Boolean.var} (* 'var *)let or (x : t) = Snark.Boolean.(x.b1 || x.b2)end
]}*)type ('var, 'value, 'aux, 'field, 'checked) typ' ={ var_to_fields : 'var -> 'field Cvar.t array * 'aux; var_of_fields : 'field Cvar.t array * 'aux -> 'var; value_to_fields : 'value -> 'field array * 'aux; value_of_fields : 'field array * 'aux -> 'value; size_in_field_elements : int; constraint_system_auxiliary : unit -> 'aux; check : 'var -> 'checked}type ('var, 'value, 'field, 'checked) typ =| Typ :('var, 'value, 'aux, 'field, 'checked) typ'-> ('var, 'value, 'field, 'checked) typendinclude Ttype ('var, 'value, 'field, 'checked) t = ('var, 'value, 'field, 'checked) typ
end

2.7 pickles.composition_types.composition_types模块

pickles.composition_types.composition_types模块中包含：

1）Step.Proof_state.Per_proof.In_circuit模块：有spec函数：

 (** A layout of the raw data in this value, which is needed forrepresenting it inside the circuit. *)let spec bp_log2 = (* bp_log2为Tock.Rounds.n，值为15 *)let open Spec inStruct[ Vector (B Field, Nat.N19.n); Vector (B Digest, Nat.N1.n); Vector (B Challenge, Nat.N2.n); Vector (Scalar Challenge, Nat.N3.n); Vector (B Bulletproof_challenge, bp_log2); Vector (B Bool, Nat.N1.n)]

其中Vector (B Field, Nat.N19.n)括号内的第一个元素B或Scalar等的含义为：

module rec T : sigtype (_, _, _) t =| B : ('a, 'b, 'env) Basic.t -> ('a, 'b, 'env) t| Scalar :('a, 'b, (< challenge1 : 'a ; challenge2 : 'b ; .. > as 'env)) Basic.t-> ('a Sc.t, 'b Sc.t, 'env) t| Vector :('t1, 't2, 'env) t * 'n Nat.t-> (('t1, 'n) Vector.t, ('t2, 'n) Vector.t, 'env) t| Array : ('t1, 't2, 'env) t * int -> ('t1 array, 't2 array, 'env) t| Struct :('xs1, 'xs2, 'env) H2_1.T(T).t-> ('xs1 Hlist.HlistId.t, 'xs2 Hlist.HlistId.t, 'env) t

Vector (B Field, Nat.N19.n)括号内的第二个元素Field等的含义为：

type ('a, 'b, 'c) basic = ('a, 'b, 'c) Basic.t =| Field: ('field1, 'field2, < field1 : 'field1 ; field2 : 'field2 ; .. >) basic| Bool : ('bool1, 'bool2, < bool1 : 'bool1 ; bool2 : 'bool2 ; .. >) basic| Digest: ( 'digest1, 'digest2, < digest1 : 'digest1 ; digest2 : 'digest2 ; .. > )basic| Challenge: ( 'challenge1, 'challenge2, < challenge1 : 'challenge1 ; challenge2 : 'challenge2 ; .. > )basic| Bulletproof_challenge: ( 'bp_chal1, 'bp_chal2, < bulletproof_challenge1 : 'bp_chal1; bulletproof_challenge2 : 'bp_chal2; .. > )basic| Branch_data: ( 'branch_data1, 'branch_data2, < branch_data1 : 'branch_data1 ; branch_data2 : 'branch_data2 ; .. >)basic

2）Step.Other_field.typ_unchecked函数为：【typ_unchecked的输出为(t, Constant.t) Typ.t类型，第一个t表示变量，第二个Constant.t表示变量Value值。】【there、back为将Tock.Field与bits表达之间的相互转换。】

let typ_unchecked : (t, Constant.t) Typ.t =Typ.transport(Typ.tuple2 Field.typ Boolean.typ)~there:(fun x ->match Tock.Field.to_bits x with| [] ->assert false| low :: high ->(Field.Constant.project high, low) )~back:(fun (high, low) ->let high = Field.Constant.unpack high inTock.Field.of_bits (low :: high) )(** Convert a list of bits into a field element. *)val project : bool list -> t(* tuple2对应为：【即将2组变量值(var1,value1)和(var2,vlue2)转换为((var1,var2), (value1,value2))】 *)val tuple2 :('var1, 'value1) t-> ('var2, 'value2) t-> ('var1 * 'var2, 'value1 * 'value2) tlet tuple2 typ1 typ2 =let open H_list inhlist [ typ1; typ2 ]|> transport~there:(fun (a, b) -> [ a; b ])~back:(fun ([ a; b ] : (unit, _ -> _ -> unit) H_list.t) -> (a, b))|> transport_var~there:(fun (a, b) -> [ a; b ])~back:(fun ([ a; b ] : (unit, _ -> _ -> unit) H_list.t) -> (a, b))

Step.Other_field结构定义为：【第一个Field.t为变量；第二个Boolean.var为变量——表示Field值的正负?】

type t = (* Low bits, high bit *)Field.t * Boolean.var
(* Field.t结构为： *)
type t = field Cvar.t
(** The finite field over which the R1CS operates. *)
type field
(* Cvar.t结构为： *)
type 'f t =| Constant of 'f| Var of int| Add of 'f t * 'f t| Scale of 'f * 'f t

Boolean.typ对应为src/lib/snarky/src/base/snark0.ml中的Make_basic.Checked.Boolean模块内的：【为Boolean结构，在true/false与Field.one/Field.zero之间转换。约束为Boolean constraint。】

let typ : (var, value) Typ.t =let (Typ typ) =Typ.field|> Typ.transport~there:(function true -> Field.one | false -> Field.zero)~back:(fun x -> if Field.equal x Field.zero then false else true)|> Typ.transport_var~there:(fun (b : var) -> (b :> Cvar.t))~back:createinTyp{ typ withcheck =(fun v ->Checked.assert_(Constraint.boolean ~label:"boolean-alloc" (v :> Cvar.t)))}
(* Constraint.boolean函数对应在src/lib/snarky/src/base/constraint.ml中： *)
let boolean ?label x = [ create_basic ?label (Boolean x) ]
let create_basic ?label basic = { basic; annotation = label }
(* Checked.assert_函数对应为src/lib/snarky/src/base/checked.ml中的Make模块内的assert_函数： *)
let assert_ ?label c =add_constraint (List.map c ~f:(fun c -> Constraint.override_label c label))
let add_constraint c = Add_constraint (c, return ())
(* 对应为src/lib/snarky/sr/base/types.ml中的type为： *)
Add_constraint : ('f Cvar.t, 'f) Constraint.t * ('a, 'f) t -> ('a, 'f) tlet typ_unchecked : (var, value) Typ.t =let (Typ typ) = typ inTyp { typ with check = (fun _ -> Checked.return ()) }(* Typ.t结构为： *)
type ('var, 'value) t = ('var, 'value, Field.t) T.t
(* T.t结构为： *)
type ('var, 'value, 'field) t =('var, 'value, 'field, (unit, 'field) Checked.t) Types.Typ.t

Field.typ对应为src/lib/snarky/snarky_curve/snarky_curve.ml中的Make_checked模块内的：【为Tick.Field.t或Tock.Field.t结构，即为(x,y) point，相应的约束为(x,y)(x,y)(x,y)在曲线上，即assert_on_curve。there back为to_affine_exn与of_affine之间的转换。】

let typ_unchecked : (t, Constant.t) Typ.t =Typ.transportTyp.(tuple2 F.typ F.typ)~there:Constant.to_affine_exn ~back:Constant.of_affinelet typ : (t, Constant.t) Typ.t =let (Typ typ_unchecked) = typ_unchecked inTyp{ typ_unchecked withcheck = (fun t -> make_checked (fun () -> assert_on_curve t))}
(* src/lib/pickles/wrap_main_inputs.ml中有： *)
module Wrap_impl = Snarky_backendless.Snark.Run.Make (Tock)
module T = Snarky_curve.For_native_base_field (Inputs)
include Make_checked (Inputs)

Types.Typ.t结构为：

type ('var, 'value, 'aux, 'field, 'checked) typ' ={ var_to_fields : 'var -> 'field Cvar.t array * 'aux; var_of_fields : 'field Cvar.t array * 'aux -> 'var; value_to_fields : 'value -> 'field array * 'aux; value_of_fields : 'field array * 'aux -> 'value; size_in_field_elements : int; constraint_system_auxiliary : unit -> 'aux; check : 'var -> 'checked}type ('var, 'value, 'field, 'checked) typ =| Typ :('var, 'value, 'aux, 'field, 'checked) typ'-> ('var, 'value, 'field, 'checked) typ

Typ.transport与Typ.transport_var函数的定义为：【其中Typ.transport定义了value_to_fields和value_of_fields，Typ.transport_var定义了var_to_fields和var_of_fields】

val transport :('var, 'value1) t-> there:('value2 -> 'value1)-> back:('value1 -> 'value2)-> ('var, 'value2) t(* 对应定义了： *); value_to_fields = (fun x -> value_to_fields (there x)); value_of_fields = (fun x -> back (value_of_fields x))val transport_var :('var1, 'value) t-> there:('var2 -> 'var1)-> back:('var1 -> 'var2)-> ('var2, 'value) tvar_to_fields = (fun x -> var_to_fields (there x)); var_of_fields = (fun x -> back (var_of_fields x))

3）src/lib/pickles/composition_types/spec.ml中的packed_typ定义为：

let packed_typ impl field t = etyp (packed_typ_basic impl field) t

调用见：

let (T (typ, f, f_inv)) =Spec.packed_typ(module Impl)(T( Shifted_value.Type2.typ Other_field.typ_unchecked, (fun (Shifted_value.Type2.Shifted_value x as t) ->Impl.run_checked (Other_field.check x) ;t ), Fn.id ) ) (* 对应packed_typ函数定义中的参数field *)spec (* 对应packed_typ函数定义中的参数t *)
(* Step模块的Impl定义为： *)
module Impl = Snarky_backendless.Snark.Run.Make (Tick)

2.8 pickles.wrap模块

pickles.wrap模块中包含：

1）Plonk_checks模块：其中Type1针对Tick曲线，Type2针对Tock曲线。
2）vector_of_list函数：将list输入转换为vector输出。
3）challenge_polynomial函数：为Tick域的challenge_polynomial函数，作用为： given [chals], compute \prod_i (1 + chals.(i) * x^{2{k - 1 - i}}) 。
4）tick_rounds：即Tick.Rounds.n。（为16）
5）combined_inner_product函数：
6）Step_acc模块：即为Tick affine坐标系。

7）wrap函数：

(* The prover for wrapping a proof *)
let wrap(type actual_proofs_verified max_proofs_verifiedmax_local_max_proofs_verifieds )~(max_proofs_verified : max_proofs_verified Nat.t)(module Max_local_max_proof_verifieds : Hlist.Maxes.Swith type ns = max_local_max_proofs_verifiedsand type length = max_proofs_verified )(( moduleReq ) :(max_proofs_verified, max_local_max_proofs_verifieds) Requests.Wrap.t )~dlog_plonk_index wrap_main to_field_elements ~step_vk ~wrap_domains~step_plonk_indices pk({ statement = prev_statement; prev_evals; proof; index = which_index } :( _, _, (_, actual_proofs_verified) Vector.t, (_, actual_proofs_verified) Vector.t, max_local_max_proofs_verifieds H1.T(P.Base.Me_only.Wrap).t, ( (Tock.Field.t, Tock.Field.t array) Plonk_types.All_evals.t, max_proofs_verified )Vector.t )P.Base.Step.t ) =

调用wrap函数为：

     let%map.Promise wrap_proof =Wrap.wrap ~max_proofs_verified:Max_proofs_verified.nfull_signature.maxes wrap_requests~dlog_plonk_index:wrap_vk.commitments wrap_main_mainA_value.to_field_elements ~step_vk~step_plonk_indices:(Lazy.force step_vks) ~wrap_domains(Impls.Wrap.Keypair.pk (fst (Lazy.force wrap_pk)))step_proof

其中：

dlog_plonk_index参数为：wrap_vk.commitments，包含：

type 'comm t ={ sigma_comm : 'comm Plonk_types.Permuts_vec.Stable.V1.t; coefficients_comm : 'comm Plonk_types.Columns_vec.Stable.V1.t; generic_comm : 'comm; psm_comm : 'comm; complete_add_comm : 'comm; mul_comm : 'comm; emul_comm : 'comm; endomul_scalar_comm : 'comm}

Mina代码中，Tick.Field.t表示的是Tick曲线的scalar域（Fp）；Tock.Filed.t表示的是Tock曲线的scalar域（Fq）。由于为Tick和Tock为2-cycle curves，Tick曲线的base域为Fq，Tock曲线的base域为Fp。令ζq∈\zeta_q\inζq∈Fq 为order为3的element，ζp∈\zeta_p\inζp∈Fp 为order为3的element，根据endomorphism属性，对于Tick曲线上的某point P，有[ζp]P=(ζqx,y)[\zeta_p]P=(\zeta_qx,y)[ζp]P=(ζqx,y)；对于Tock曲线上的某point P，有[ζq]P=(ζpx,y)[\zeta_q]P=(\zeta_px,y)[ζq]P=(ζpx,y)。
to_field_elements参数为：A_value.to_field_elements。

Oracles结构为：

type nonrec 'f oracles ={ o : 'f random_oracles; p_eval : 'f * 'f; opening_prechallenges : 'f array; digest_before_evaluations : 'f}pub struct RandomOracles<F: Field> {pub joint_combiner: (ScalarChallenge<F>, F),pub beta: F,pub gamma: F,pub alpha_chal: ScalarChallenge<F>,pub alpha: F,pub zeta: F,pub v: F,pub u: F,pub zeta_chal: ScalarChallenge<F>,pub v_chal: ScalarChallenge<F>,pub u_chal: ScalarChallenge<F>,
}

基本流程为：

1）取step_proof.statement=prev_statement，step_proof.index=which_index, step_proof.prev_evals=prev_evals, step_proof.proof=proof。
调用P.Base.Me_only.Wrap.prepare 构造prev_me_only（为Me_only.t结构）：
- 令prev_me_only.challenge_polynomial_commitment=prev_statement.passthrough.challenge_polynomial_commitment；
- 令prev_me_only.old_bulletproof_challenegs="以prev_statement.passthrough.old_bulletproof_challenges中的每个challenge为r⃗\vec{r}r，按照Halo论文算法2计算映射为[aζq+b][a\zeta_q+b][aζq+b]（对应为Tock曲线的scalar域）“，借助2-cycle curve的endomorphism属性，提升scalar multiplication计算效率，进而提升验证step_proof的效率。详细见博客基于endomorphism优化scalar multiplication及其用途中第2节。
2）取me_only_a=prev_statement.proof_state.me_only，调用P.Base.Me_only.Step.prepare，替换其中的dlog_plonk_index为wrap_vk.commitments；替换其中的old_bulletproof_challenges中的每个challenge为相应的[aζp+b][a\zeta_p+b][aζp+b]（对于为Tick曲线的scalar域）。
调用Common.hash_step_me_only将me_only_a 经Tick_field_sponge获得哈希结果表示为step_me_only_hash。
取proof_state=prev_statement.proof_state，将其中的me_only替换为step_me_only_hash。
3）对prev_me_only.old_bulletproof_challenges调用pad_challenges填充为长度为2的vector，调用Wrap_hack.hash_dlog_me_only经Tock_field_sponge获得哈希结果表示为pass_through。
将proof_state和pass_through组装为prev_statement_with_hashes。
4）构建handler，支持Evals、Step_accs、Old_bulletproof_challenges、Messages、Openings_proof、Proof_state、Which_branch等request操作。
5）基于prev_statement_with_hashes调用tick_public_input_of_statement获得public_input。
6）调用compute_challenges，将prev_statement.proof_state.me_only.old_bulletproof_challenges中的每个challenge映射为相应的[aζp+b][a\zeta_p+b][aζp+b]（对于为Tick曲线的scalar域），将映射后的结果表示为prev_challenges。
7）取actual_proofs_verified = Vector.length prev_challenges，令 lte = Nat.lte_exn actual_proofs_verified (Length.to_nat Max_local_max_proof_verifieds.length)。
8）取prev_me_only.challenge_polynomial_commitment为sgs，取Tick.Oracles为O，基于step_vk、sgs、lte、prev_challenges、public_input、proof调用O.create创建oracle o。
9）取x_hat=(fst o.p_eval, snd o.p_eval)，取o.digest_before_evaluations为digest_before_evaluations。
构建plonk0，使其alpha=o.o.alpha_chal，beta=o.o.beta，gamma=o.o.gamma, zeta=o.o.zeta_chal。
取r=o.o.u_chal，xi=o.o.v_chal。

10）构建tick_plonk_minimal、tick_combined_evals、tick_domain、tick_env、combined_inner_product、me_only，然后生成new_bulletproof_challenges、plonk、shift_value、branch_data，最终生成next_statement：

let next_statement : _ Types.Wrap.Statement.In_circuit.t =
{ proof_state ={ deferred_values ={ xi; b = shift_value b; bulletproof_challenges =Vector.of_array_and_length_exn new_bulletproof_challengesTick.Rounds.n; combined_inner_product = shift_value combined_inner_product; branch_data; plonk ={ plonk withzeta = plonk0.zeta; alpha = plonk0.alpha; beta = chal plonk0.beta; gamma = chal plonk0.gamma}}; sponge_digest_before_evaluations =Digest.Constant.of_tick_field sponge_digest_before_evaluations; me_only}
; pass_through = prev_statement.proof_state.me_only
}

11）调用P.Base.Me_only.Wrap.prepare 构造me_only_prepared（为Me_only.t结构）：
- 令me_only_prepared.challenge_polynomial_commitment=next_statement.proof_state.me_only.challenge_polynomial_commitment；
- 令me_only_prepared.old_bulletproof_challenegs="以next_statement.proof_state.me_only.old_bulletproof_challenges中的每个challenge为r⃗\vec{r}r，按照Halo论文算法2计算映射为[aζq+b][a\zeta_q+b][aζq+b]（对应为Tock曲线的scalar域）“。

12）调用Impls.Wrap.generate_witness_conv，获得的Tock proof为：

let%map.Promise next_proof =let (T (input, conv, _conv_inv)) = Impls.Wrap.input () inCommon.time "wrap proof" (fun () ->Impls.Wrap.generate_witness_conv~f:(fun { Impls.Wrap.Proof_inputs.auxiliary_inputs; public_inputs } () ->Backend.Tock.Proof.create_async ~primary:public_inputs~auxiliary:auxiliary_inputs pk~message:( Vector.map2(Vector.extend_exnprev_statement.proof_state.me_only.challenge_polynomial_commitments max_proofs_verified(Lazy.force Dummy.Ipa.Wrap.sg) )me_only_prepared.old_bulletproof_challenges~f:(fun sg chals ->{ Tock.Proof.Challenge_polynomial.commitment = sg; challenges = Vector.to_array chals} )|> Wrap_hack.pad_accumulator ) )[ input ]~return_typ:(Snarky_backendless.Typ.unit ())(fun x () : unit ->Impls.Wrap.handle (fun () : unit -> wrap_main (conv x)) handler ){ pass_through = prev_statement_with_hashes.proof_state.me_only; proof_state ={ next_statement.proof_state withme_only =Wrap_hack.hash_dlog_me_only max_proofs_verifiedme_only_prepared}} )

其中：

let (T (input, conv, _conv_inv)) = Impls.Wrap.input ()中的input对应为变量：

let fp : ('a, Other_field.Constant.t) Typ.t = Other_field.typ_unchecked
Shifted_value.Type1.typ fp
let typ =Typ.transport typ ~there:In_circuit.to_data ~back:In_circuit.of_data

let (T (input, conv, _conv_inv)) = Impls.Wrap.input ()中的conv对应为取变量值的函数：(fun x -> In_circuit.of_data (f x))。In_circuit.of_data和In_circuit.to_data函数为：

(* In_circuit.of_data函数为： *)(** Construct a statement (as structured data) from the flat data-based representation. *)let of_dataHlist.HlistId.[ fp; challenge; scalar_challenge; digest; bulletproof_challenges; index] : _ t =let open Vector inlet (combined_inner_product:: b:: zeta_to_srs_length:: zeta_to_domain_size:: poseidon_selector:: vbmul:: complete_add:: endomul :: endomul_scalar :: perm :: generic )=fpinlet [ beta; gamma ] = challenge inlet [ alpha; zeta; xi ] = scalar_challenge inlet [ sponge_digest_before_evaluations; me_only; pass_through ] =digestinlet [ branch_data ] = index in{ proof_state ={ deferred_values ={ xi; combined_inner_product; b; branch_data; bulletproof_challenges; plonk ={ alpha; beta; gamma; zeta; zeta_to_srs_length; zeta_to_domain_size; poseidon_selector; vbmul; complete_add; endomul; endomul_scalar; perm; generic}}; sponge_digest_before_evaluations; me_only}; pass_through}
(*In_circuit.to_data函数为：*)
(** Convert a statement (as structured data) into the flat data-based representation. *)let to_data({ proof_state ={ deferred_values ={ xi; combined_inner_product; b; branch_data; bulletproof_challenges; plonk ={ alpha; beta; gamma; zeta; zeta_to_srs_length; zeta_to_domain_size; poseidon_selector; vbmul; complete_add; endomul; endomul_scalar; perm; generic}}; sponge_digest_before_evaluations; me_only(* me_only is represented as a digest (and then unhashed) inside the circuit *)}; pass_through(* pass_through is represented as a digest inside the circuit *)} :_ t ) =let open Vector inlet fp =combined_inner_product :: b :: zeta_to_srs_length:: zeta_to_domain_size :: poseidon_selector :: vbmul :: complete_add:: endomul :: endomul_scalar :: perm :: genericinlet challenge = [ beta; gamma ] inlet scalar_challenge = [ alpha; zeta; xi ] inlet digest =[ sponge_digest_before_evaluations; me_only; pass_through ]inlet index = [ branch_data ] inHlist.HlistId.[ fp; challenge; scalar_challenge; digest; bulletproof_challenges; index]

let (T (input, conv, _conv_inv)) = Impls.Wrap.input ()中的_conv_inv对应为函数：fun x -> f_inv (In_circuit.to_data x)。

13）将Tock proof封装为P.Base.Wrap.t结构：

{ proof = next_proof
; statement = Types.Wrap.Statement.to_minimal next_statement
; prev_evals ={ Plonk_types.All_evals.evals =Double.map2 x_hat proof.openings.evals ~f:(fun p e ->{ Plonk_types.All_evals.With_public_input.public_input = p; evals = e} ); ft_eval1 = proof.openings.ft_eval1}
}
: _ P.Base.Wrap.t

3. 生成Tock proof的关键函数generate_witness_conv

生成Tock proof的关键函数generate_witness_conv定义为：

val generate_witness_conv :f:(Proof_inputs.t -> 'r_value -> 'out)-> (unit -> 'r_var, 'out, 'k_var, 'k_value) Data_spec.t-> return_typ:('r_var, 'r_value) Typ.t-> 'k_var-> 'k_value

let generate_witness_conv ~f spec ~return_typ x =。。。。。
其中：

f对应为函数：

(fun { Impls.Wrap.Proof_inputs.auxiliary_inputs; public_inputs } () ->Backend.Tock.Proof.create_async ~primary:public_inputs~auxiliary:auxiliary_inputs pk~message:( Vector.map2(Vector.extend_exnprev_statement.proof_state.me_only.challenge_polynomial_commitments max_proofs_verified(Lazy.force Dummy.Ipa.Wrap.sg) )me_only_prepared.old_bulletproof_challenges~f:(fun sg chals ->{ Tock.Proof.Challenge_polynomial.commitment = sg; challenges = Vector.to_array chals} )|> Wrap_hack.pad_accumulator ) )

spec对应为Impls.Wrap.input ()输出的[input]。

return_typ对应为：

(Snarky_backendless.Typ.unit ())(* Typ.unit()结构为： *)
let unit () : (unit, unit, 'field) t =Typ{ var_to_fields = (fun () -> ([||], ())); var_of_fields = (fun _ -> ()); value_to_fields = (fun () -> ([||], ())); value_of_fields = (fun _ -> ()); size_in_field_elements = 0; constraint_system_auxiliary = (fun () -> ()); check = (fun () -> Checked.return ())}

x对应为函数：

(fun x () : unit ->Impls.Wrap.handle (fun () : unit -> wrap_main (conv x)) handler )

Impls.Wrap.handle函数定义为：

val handle : (unit -> 'a) -> Handler.t -> 'alet handle x h =let h = Request.Handler.create_single h inlet { handler; _ } = !state instate := { !state with handler = Request.Handler.push handler h } ;let a = x () in (* 运行完wrap_main (conv x) 之后，再将state的handler还原 *)state := { !state with handler } ;a

其中的state为run_state结构：

(** The internal state used to run a checked computation. *)
type 'field t ={ system : 'field Constraint_system.t option; input : 'field Vector.t; aux : 'field Vector.t; eval_constraints : bool; num_inputs : int; next_auxiliary : int ref; has_witness : bool; stack : string list; handler : Request.Handler.t; is_running : bool; as_prover : bool ref; log_constraint :(   ?at_label_boundary:[ `Start | `End ] * string-> ('field Cvar.t, 'field) Constraint.t-> unit)option}

Run.generate_witness_conv函数对应为k_value值：

{ pass_through = prev_statement_with_hashes.proof_state.me_only; proof_state ={ next_statement.proof_state withme_only =Wrap_hack.hash_dlog_me_only max_proofs_verifiedme_only_prepared}}

let generate_witness_conv ~f spec ~return_typ x =let x = inject_wrapper spec x ~f:(fun x () -> mark_active ~f:x) inPerform.generate_witness_conv ~run:as_stateful ~f spec ~return_typ x

其中的run对应为as_stateful函数：

 let as_stateful x state' =state := state' ;let a = x () in(!state, a)

inject_wrapper为递归函数，将spec展开获得新的x函数：

let rec inject_wrapper :type r_var r_value k_var k_value.(r_var, r_value, k_var, k_value) Data_spec.t-> f:(r_var -> r_var)-> k_var-> k_var =fun spec ~f ->match spec with| [] ->fun x -> f x| _ :: spec ->fun x a -> inject_wrapper spec ~f (x a)

Perform.generate_witness_conv函数为：【其中t为spec，k为x函数】

let generate_witness_conv ~run ~f t ~return_typ k =Run.generate_witness_conv ~run ~f t ~return_typ k

Run.generate_witness_conv函数为：【其中?handlers:Handler.t list为上面的k函数->x函数】

let generate_witness_conv :run:('a, 'checked) Runner.run-> f:(Proof_inputs.t -> _ -> 'out)-> ('checked, 'out, 'k_var, 'k_value, _, _) Typ.Data_spec.data_spec-> return_typ:_ Typ.t-> ?handlers:Handler.t list-> 'k_var-> 'k_value =fun ~run ~f t ~return_typ ?handlers k -> (* 其中的k为：wrap.wrap函数内的结构值：{ pass_through = prev_statement_with_hashes.proof_state.me_only; proof_state ={ next_statement.proof_state withme_only =Wrap_hack.hash_dlog_me_only max_proofs_verifiedme_only_prepared}} *)conv(fun num_inputs output c primary ->let auxiliary =auxiliary_input ~run ?handlers ~return_typ ~output ~num_inputs cprimaryinlet output =let (Typ return_typ) = return_typ inlet fields, aux = return_typ.var_to_fields output inlet read_cvar =let get_one i =if i <= num_inputs then Field.Vector.get primary (i - 1)else Field.Vector.get auxiliary (i - num_inputs - 1)inCvar.eval (`Return_values_will_be_mutated get_one)inlet fields = Array.map ~f:read_cvar fields inreturn_typ.value_of_fields (fields, aux)inf{ Proof_inputs.public_inputs = primary; auxiliary_inputs = auxiliary}output)t return_typ(fun () -> k)

其中conv函数定义为：【其中t0为t->spec，k0为fun()->k】

let conv :type r_var r_value.(int -> _ -> r_var -> Field.Vector.t -> r_value)-> (r_var, r_value, 'k_var, 'k_value, _, _) Typ.Data_spec.data_spec-> _ Typ.t-> (unit -> 'k_var)-> 'k_value =fun cont0 t0 (Typ return_typ) k0 ->let primary_input = Field.Vector.create () inlet next_input = ref 1 inlet store_field_elt x =let v = !next_input inincr next_input ;Field.Vector.emplace_back primary_input x ;Cvar.Unsafe.of_index vinlet rec go :type k_var k_value.(r_var, r_value, k_var, k_value, _, _) Typ.Data_spec.data_spec-> (unit -> k_var)-> k_value =fun t k ->match t with| [] ->let retval =return_typ.var_of_fields( Core_kernel.Array.init return_typ.size_in_field_elements~f:(fun _ -> alloc_var next_input ()), return_typ.constraint_system_auxiliary () )incont0 !next_input retval (k ()) primary_input| Typ { var_of_fields; value_to_fields; _ } :: t' ->fun value ->let fields, aux = value_to_fields value inlet fields = Array.map ~f:store_field_elt fields inlet var = var_of_fields (fields, aux) ingo t' (fun () -> k () var)ingo t0 k0

其中cont0对应为函数：

     (fun num_inputs output c primary ->let auxiliary = (* 其中run为上面的as_stateful函数，return_typ为 *)auxiliary_input ~run ?handlers ~return_typ ~output ~num_inputs cprimaryinlet output =let (Typ return_typ) = return_typ in (* 此处的return_typ对应为(Snarky_backendless.Typ.unit ()) *)let fields, aux = return_typ.var_to_fields output in (* 此处的output对应为上面的retval *)let read_cvar = (* index i为num_inputs之前的为primary(public) input，num_inputs之后的为auxiliary input。 *)let get_one i =if i <= num_inputs then Field.Vector.get primary (i - 1)else Field.Vector.get auxiliary (i - num_inputs - 1)inCvar.eval (`Return_values_will_be_mutated get_one)inlet fields = Array.map ~f:read_cvar fields inreturn_typ.value_of_fields (fields, aux)inf (* 本质是调用wrap.wrap()函数内的next_proof中的~f函数 *){ Proof_inputs.public_inputs = primary; auxiliary_inputs = auxiliary}output)

 let auxiliary_input ?system ~run ~num_inputs?(handlers = ([] : Handler.t list)) t0 (input : Field.Vector.t)~return_typ:(Types.Typ.Typ return_typ) ~output : Field.Vector.t =

其中auxiliary_input函数的参数为：

1）run：对应为上面的as_stateful函数。
2）return_typ：对应为(Snarky_backendless.Typ.unit ())
3）output：对应为上面的retval

4）c（t0）：对应为上面的(k())，其中k对应为函数：

let x = inject_wrapper spec x ~f:(fun x () -> mark_active ~f:x)

其中x对应为wrap.wrap()函数内的x函数：

(fun x () : unit ->Impls.Wrap.handle (fun () : unit -> wrap_main (conv x)) handler )

5）primary（input）：对应为上面的primary_input
6）num_inputs：对一个为上面的num_inputs

7）handlers：对应为wrap.wrap()函数内的x函数：

(fun x () : unit ->Impls.Wrap.handle (fun () : unit -> wrap_main (conv x)) handler )

let auxiliary_input ?system ~run ~num_inputs?(handlers = ([] : Handler.t list)) t0 (input : Field.Vector.t)~return_typ:(Types.Typ.Typ return_typ) ~output : Field.Vector.t =let next_auxiliary = ref (1 + num_inputs) inlet aux = Field.Vector.create () inlet handler =List.fold ~init:Request.Handler.fail handlers ~f:(fun handler h ->Request.Handler.(push handler (create_single h)) )inlet state =Runner.State.make ?system ~num_inputs ~input:(pack_field_vec input)~next_auxiliary ~aux:(pack_field_vec aux) ~handler ~with_witness:true ()inlet state, res = run t0 state inlet res, _ = return_typ.var_to_fields res inlet output, _ = return_typ.var_to_fields output inlet _state =Array.fold2_exn ~init:state res output ~f:(fun state res output ->Field.Vector.emplace_back input (Runner.get_value state res) ;fst @@ Checked.run (Checked.assert_equal res output) state )inOption.iter system ~f:(fun system ->let auxiliary_input_size = !next_auxiliary - (1 + num_inputs) inR1CS_constraint_system.set_auxiliary_input_size systemauxiliary_input_size ;R1CS_constraint_system.finalize system ) ;aux

其中：

1）Runner.State.make返回的state为：

{ system (* 为none *); input (* 为primary（input）：对应为上面的primary_input *); aux (* 为上面的aux数组 *); eval_constraints (* 为true *); num_inputs; next_auxiliary (* 为 1+num_inputs *); has_witness = with_witness (* 为true *); stack = []; handler = Option.value handler ~default:Request.Handler.fail (* 对应为wrap.wrap()函数内的x函数 *); is_running = true; as_prover = ref false; log_constraint = !constraint_logger (* 为None或Some *)}

2）let state, res = run t0 state ，其本质为调用as_stateful函数-》其中的t0（x）对应为wrap.wrap的x函数，执行完wrap.wrap的x函数的结果a存入res中：

let as_stateful x state' =state := state' ;let a = x () in(!state, a)(fun x () : unit ->Impls.Wrap.handle (fun () : unit -> wrap_main (conv x)) handler )

其中Impls.Wrap.handle函数对应为：

let handle x h =let h = Request.Handler.create_single h inlet { handler; _ } = !state instate := { !state with handler = Request.Handler.push handler h } ;let a = x () instate := { !state with handler } ;a

conv x，本质为调用(fun x -> In_circuit.of_data (f x))，返回的为Wrap.Statement.In_circuit结构类型：

{ proof_state ={ deferred_values ={ xi; combined_inner_product; b; branch_data; bulletproof_challenges; plonk ={ alpha; beta; gamma; zeta; zeta_to_srs_length; zeta_to_domain_size; poseidon_selector; vbmul; complete_add; endomul; endomul_scalar; perm; generic}}; sponge_digest_before_evaluations; me_only}; pass_through}

然后将以上(conv x)的输出作为输入，调用wrap_main.main函数：

let main({ proof_state ={ deferred_values ={ plonk; xi; combined_inner_product; b; branch_data; bulletproof_challenges}; sponge_digest_before_evaluations; me_only = me_only_digest}; pass_through} :( _, _, _ Shifted_value.Type1.t, _, _, _, _, _, Field.t )Types.Wrap.Statement.In_circuit.t ) = ......

let x = inject_wrapper spec x ~f:(fun x () -> mark_active ~f:x) inlet rec inject_wrapper :type r_var r_value k_var k_value.(r_var, r_value, k_var, k_value) Data_spec.t-> f:(r_var -> r_var)-> k_var-> k_var =fun spec ~f ->match spec with| [] ->let () = Printf.printf "ZYD inject_wrapper []\n" infun x -> f x| _ :: spec ->let () = Printf.printf "ZYD inject_wrapper Some\n" infun x a -> inject_wrapper spec ~f (x a)

inject_wrapper为Some
返回的x为函数: fun x a -> inject_wrapper spec ~f (x a)
其中的f为: (fun x () -> mark_active ~f:x)

let mark_active ~f =let counters = !active_counters inactive_counters := this_functor_id :: counters ;trylet ret = f () in (* 此处的f函数为wrap.wrap的x函数 *)active_counters := counters ;retwith exn ->active_counters := counters ;raise exn

基本的调试信息为：

ZYD generate_witness_conv 444
ZYD inject_wrapper Some
ZYD after inject_wrapper ###
ZYD generate_witness_conv 222
ZYD generate_witness_conv 111
ZYD conv Some
ZYD conv []
ZYD inject_wrapper []
ZYD proving 11111
ZYD runner.state.make
ZYD in x before Impls.Wrap.handle
ZYD proving 22222
ZYD proving 33333
ZYD in f before tock.proof.create_async
ZYD provers 4444

参考资料

[1] Mina背后的理想乡：递归零知识证明
[2] Recusive ZK-SNARKS

附录1. Mina系列博客

Mina系列博客有：

Mina概览
Mina的支付流程
Mina的zkApp
Mina中的Pasta（Pallas和Vesta）曲线
Mina中的Schnorr signature
Mina中的Pickles SNARK
Mina中的Kimchi SNARK
Mina Kimchi SNARK 代码解析
Mina Berkeley QANet测试网zkApp初体验
Mina中的Poseidon hash
Mina中的多项式承诺方案
Recursive SNARKs总览
Mina技术白皮书
Mina代码解析
Mina中的Snark Worker
Mina中的Scan State
Mina中的VRF
Mina中的delta_transition_chain_proof/delta_block_chain_proof
Mina中的stake delegation
Mina如何实现22KB？
Mina中的stake_proof
Mina中的genesis_proof
Mina中的交易及经济白皮书
Mina中的ledger proof
Mina中的基于DLG的Plonk polynomial commitment scheme代码解析
Mina中的约束系统代码解析
Mina中的scan state代码解析
Mina中的区块证明

Mina中的wrap snark相关推荐

Mina中的Kimchi SNARK
1. 引言 Mina系列博客有: Mina概览 Mina的支付流程 Mina的zkApp Mina中的Pasta(Pallas和Vesta)曲线 Mina中的Schnorr signature Min ...
Mina中的Pickles SNARK
1. 引言 Mina系列博客有: Mina概览 Mina的支付流程 Mina的zkApp Mina中的Pasta(Pallas和Vesta)曲线 Mina中的Schnorr signature 视频可 ...
Mina中的zkApp交易snark
1. 引言前序博客有: Mina中的支付交易snark(针对Payment交易) Mina的zkApp Mina中的树结构 --账号树 Mina中的user_command交易目前有: 1)Sign ...
Mina中的支付交易snark
1. 引言前序博客有: Mina的支付流程 Mina中目前的交易类型主要有: Coinbase交易:给产块者激励和手续费的交易,为内部交易. Fee_transfer交易:给snark worker ...
Mina中的Snark Worker
1. 引言 Mina系列博客有: Mina概览 Mina的支付流程 Mina的zkApp Mina中的Pasta(Pallas和Vesta)曲线 Mina中的Schnorr signature Min ...
Mina中的区块证明
1. 引言 Mina的Pickles支持2种类型的tag: Side_loaded Compiled type ('var, 'value, 'n1, 'n2) t ={ kind : kind; i ...
Mina中的stake delegation
1. 引言为支持将某人的质押委托给另一人,增加受托人赢的几率. 质押委托的设计目标为: 从网络安全的角度来看,希望质押或委托的金额越多越好. 应不会too expensive inside the ...
mina 中的IoBufer(一)
为什么80%的码农都做不了架构师?>>> IoBuffer 是 MINA 中的独有接口,主要继承实现的是 java NIO 中的 ByteBuffer ,所以从使用方法上来看二 ...
从Jetty、Tomcat和Mina中提炼NIO构架网络服务器的经典模式（三）
2019独角兽企业重金招聘Python工程师标准>>> 从Jetty.Tomcat和Mina中提炼NIO构架网络服务器的经典模式(三) 博客分类: java 最后我们再看看NIO方面 ...

Mina中的wrap snark