Mina中的wrap snark

前序博客有：

• 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 , π tick x, \pi_{\text{tick}} x,πtick​
• witness： w w w
• 待证明relation： Verify tick ( ( 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 , π tock x,\pi_{\text{tock}} x,πtock​
• witness： w , π tick w, \pi_{\text{tick}} w,πtick​
• 待证明relation： Verify tick ( ( 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）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 in
      let%map _ = inv v in
      ()

	(* We get a better stack trace by failing at the call to is_satisfied, so we
       put a bogus value for the inverse to make the constraint system unsat if
       x 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 in
            let%bind x_inv =
              exists Typ.field
                ~compute:
                  As_prover.(
                    map (read_var x) ~f:(fun x ->
                        if Field.(equal zero x) then Field.zero
                        else Backend.Field.inv x))
            in
            let%map () =
              assert_r1cs ~label:"field_inverse" x x_inv
                (Cvar.constant Field.one)
            in
            x_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 ())

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 in
          Struct
            [ 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)
            ]

调用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_proof

type 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 in
	  Typ
	    { 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 in
    Typ
      { typ_unchecked with
        check = (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:create
      in
      Typ
        { typ with
          check =
            (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))
          }
      in
      let s, y = handle_error s (fun () -> exists typ p s) in
      let k = handle_error s (fun () -> k y) in
      run 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 with
      check = (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 with
        check =
          (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_exn
      in
      i )
  

• 5）impls.ml中Step的check为：

  let check t =
    let open Internal_Basic in
    let open Let_syntax in
    let equal (x1, b1) (x2, b2) =
      let%bind x_eq = Field.Checked.equal x1 (Field.Var.constant x2) in
      let b_eq = match b2 with true -> b1 | false -> Boolean.not b1 in
      Boolean.( && ) x_eq b_eq
    in
    let (Typ typ_unchecked) = typ_unchecked in
    let%bind () = typ_unchecked.check t in
    Checked.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 in
      let open Let_syntax in
      let equal x1 x2 = Field.Checked.equal x1 (Field.Var.constant x2) in
      let%bind () = t0.check t in
      Checked.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 in
      Typ
        { typ_unchecked with
          check = (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 in
      let compute = Option.map compute ~f:As_prover.run_prover in
      run (exists ?request ?compute typ)

      	  let exists ?request ?compute typ =
            let%map h = exists_handle ?request ?compute typ in
            Handle.var h

            	let exists_handle ?request ?compute typ =
                  let provider =
                    let request =
                      Option.value request ~default:(As_prover.return Request.Fail)
                    in
                    match compute with
                    | None ->
                        Types.Provider.Request request
                    | Some c ->
                        Types.Provider.Both (request, c)
                  in
                  exists 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) then
                              failwithf
                                "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 then
                              failwith
                                "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) in
                            let state', x = Runner.run checked !state in
                            let () = Printf.printf "AFTER ZYD run_checked Runner.run, state.next_auxiliary:%d\n" !(!state.next_auxiliary) in
                            state := 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 in
      let old = !(s.as_prover) in
      s.as_prover := true ;
      let value = As_prover.Provider.run p s.stack (get_value s) s.handler in
      s.as_prover := old ;
      let var =
        let store_value =
          if !(s.as_prover) then
            (* If we're nested in a prover block, create constants instead of
               storing.
            *)
            Cvar.constant
          else store_field_elt s
        in
        let fields, aux = value_to_fields value in
        let field_vars = Array.map ~f:store_value fields in
        var_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 }) )
    else
      let () = Printf.printf "ELSE ZYD exists s.has_witness: %b, size_in_field_elements:%d\n" s.has_witness size_in_field_elements in
      let 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" in
          Checked.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" in
          let z = Cvar.(x - y) in
          let%bind r, inv =
            exists Typ.(field * field) ~compute:(equal_vars z)
          in
          let%map () = equal_constraints z inv r in
          Boolean.Unsafe.create r

• 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"  in
    let 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 in
        let fq =
          combined_inner_product :: b :: zeta_to_srs_length
          :: zeta_to_domain_size :: poseidon_selector :: vbmul :: complete_add
          :: endomul :: endomul_scalar :: perm :: generic
        in
        let challenge = [ beta; gamma ] in
        let scalar_challenge = [ alpha; zeta; xi ] in
        let digest = [ sponge_digest_before_evaluations ] in
        let bool = [ should_finalize ] in
        let 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 in
      let fp =
        combined_inner_product :: b :: zeta_to_srs_length
        :: zeta_to_domain_size :: poseidon_selector :: vbmul :: complete_add
        :: endomul :: endomul_scalar :: perm :: generic
      in
      let challenge = [ beta; gamma ] in
      let scalar_challenge = [ alpha; zeta; xi ] in
      let digest =
        [ sponge_digest_before_evaluations; me_only; pass_through ]
      in
      let index = [ branch_data ] in
      Hlist.HlistId.
        [ fp
        ; challenge
        ; scalar_challenge
        ; digest
        ; bulletproof_challenges
        ; index
        ]
  

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_header
           constraint_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 false
  in
  { 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

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

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

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.
   It
   1. Checks that [xi] and [r] where sampled correctly. I.e., by absorbing all the
   evaluation openings and then squeezing.
   2. Checks that the "combined inner product" value used in the elliptic curve part of
   the opening proof was computed correctly, in terms of the evaluation openings and the
   evaluation 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
    }
  

pickles.wrap_main模块中包含：

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

  module Old_bulletproof_chals = struct
    type 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 env
      max_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_vks
        proofs_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 the
            computation of the linearized polynomial commitment.
  
            Then, we expose them so the next guy (who can do scalar arithmetic) can check that they
            were 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. *)
          }
  

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 in
      let open Types.Wrap.Statement in
      let (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.spec
      in
      let typ =
        Typ.transport typ ~there:In_circuit.to_data ~back:In_circuit.of_data
      in
      Spec.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 for
        representing it inside the circuit. *)
    let spec =
      let open Spec in
      Struct
        [ 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 :: generic
      in
      let challenge = [ beta; gamma ] in
      let scalar_challenge = [ alpha; zeta; xi ] in
      let digest =
        [ sponge_digest_before_evaluations; me_only; pass_through ]
      in
      let 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 in
    let module Digest = D.Make (Impl) in
    let module Challenge = Limb_vector.Challenge.Make (Impl) in
    let module Env = struct
      type ('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
        'a
    end in
    let 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 } }
                =
              pre
            in
            let back pre =
              { Bulletproof_challenge.prechallenge = { Sc.inner = pre } }
            in
            Typ.transport Challenge.typ ~there ~back
            |> Typ.transport_var ~there ~back
          in
          T (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 in
    fun e spec ->
      match spec with
      | B spec ->
          e.etyp spec
      | Scalar chal ->
          let (T (typ, f, f_inv)) = e.etyp chal in
          T (Sc.typ typ, Sc.map ~f, Sc.map ~f:f_inv)
      | Vector (spec, n) ->
          let (T (typ, f, f_inv)) = etyp e spec in
          T (Vector.typ typ n, Vector.map ~f, Vector.map ~f:f_inv)
      | Array (spec, n) ->
          let (T (typ, f, f_inv)) = etyp e spec in
          T (array ~length:n typ, Array.map ~f, Array.map ~f:f_inv)
      | Struct [] ->
          let open Hlist.HlistId in
          let there [] = () in
          let back () = [] in
          T
            ( transport (unit ()) ~there ~back |> transport_var ~there ~back
            , Fn.id
            , Fn.id )
      | Struct (spec :: specs) ->
          let open Hlist.HlistId in
          let (T (t1, f1, f1_inv)) = etyp e spec in
          let (T (t2, f2, f2_inv)) = etyp e (Struct specs) in
          T
            ( 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) )
  

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

module Typ = struct
  module T = struct
    (** The type [('var, 'value, 'field, 'checked) t] describes a mapping from
      OCaml 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 stored
        contents 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.b2

  module Checked = struct
    type 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) typ
  end

  include T

  type ('var, 'value, 'field, 'checked) t = ('var, 'value, 'field, 'checked) typ
end

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 for
        representing it inside the circuit. *)
      let spec bp_log2 = (* bp_log2为Tock.Rounds.n，值为15 *)
        let open Spec in
        Struct
          [ 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 : sig
    type (_, _, _) 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 in
        Tock.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) t
    
    let tuple2 typ1 typ2 =
        let open H_list in
        hlist [ 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:create
      in
      Typ
        { typ with
          check =
            (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) t
  
  let typ_unchecked : (var, value) Typ.t =
      let (Typ typ) = typ in
      Typ { 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.transport
        Typ.(tuple2 F.typ F.typ)
        ~there:Constant.to_affine_exn ~back:Constant.of_affine
  
  let typ : (t, Constant.t) Typ.t =
      let (Typ typ_unchecked) = typ_unchecked in
      Typ
        { typ_unchecked with
          check = (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) t
   	
   	 var_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)
  

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_verified
      max_local_max_proofs_verifieds )
      ~(max_proofs_verified : max_proofs_verified Nat.t)
      (module Max_local_max_proof_verifieds : Hlist.Maxes.S
        with type ns = max_local_max_proofs_verifieds
         and type length = max_proofs_verified )
      (( module
        Req ) :
        (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.n
              full_signature.maxes wrap_requests
              ~dlog_plonk_index:wrap_vk.commitments wrap_main_main
              A_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 = ( ζ q x , y ) [\zeta_p]P=(\zeta_qx,y) [ζp​]P=(ζq​x,y)；对于Tock曲线上的某point P，有 [ ζ q ] P = ( ζ p x , y ) [\zeta_q]P=(\zeta_px,y) [ζq​]P=(ζp​x,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 {
      pub joint_combiner: (ScalarChallenge, F),
      pub beta: F,
      pub gamma: F,
      pub alpha_chal: ScalarChallenge,
      pub alpha: F,
      pub zeta: F,
      pub v: F,
      pub u: F,
      pub zeta_chal: ScalarChallenge,
      pub v_chal: ScalarChallenge,
      pub u_chal: ScalarChallenge,
  }
  

基本流程为：

• 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_challenges
                Tick.Rounds.n
          ; combined_inner_product = shift_value combined_inner_product
          ; branch_data
          ; plonk =
              { plonk with
                zeta = 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 () in
      Common.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_exn
                         prev_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 with
                  me_only =
                    Wrap_hack.hash_dlog_me_only max_proofs_verified
                      me_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_data
          Hlist.HlistId.
            [ fp
            ; challenge
            ; scalar_challenge
            ; digest
            ; bulletproof_challenges
            ; index
            ] : _ t =
        let open Vector in
        let (combined_inner_product
            :: b
               :: zeta_to_srs_length
                  :: zeta_to_domain_size
                     :: poseidon_selector
                        :: vbmul
                           :: complete_add
                              :: endomul :: endomul_scalar :: perm :: generic )
            =
          fp
        in
        let [ beta; gamma ] = challenge in
        let [ alpha; zeta; xi ] = scalar_challenge in
        let [ sponge_digest_before_evaluations; me_only; pass_through ] =
          digest
        in
        let [ 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 in
        let fp =
          combined_inner_product :: b :: zeta_to_srs_length
          :: zeta_to_domain_size :: poseidon_selector :: vbmul :: complete_add
          :: endomul :: endomul_scalar :: perm :: generic
        in
        let challenge = [ beta; gamma ] in
        let scalar_challenge = [ alpha; zeta; xi ] in
        let digest =
          [ sponge_digest_before_evaluations; me_only; pass_through ]
        in
        let index = [ branch_data ] in
        Hlist.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
  

生成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_exn
                     prev_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 -> 'a
  
  let handle x h =
    let h = Request.Handler.create_single h in
    let { handler; _ } = !state in
    state := { !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 with
              me_only =
                Wrap_hack.hash_dlog_me_only max_proofs_verified
                  me_only_prepared
            }
        }
  

let generate_witness_conv ~f spec ~return_typ x =
      let x = inject_wrapper spec x ~f:(fun x () -> mark_active ~f:x) in
      Perform.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 with
                me_only =
                  Wrap_hack.hash_dlog_me_only max_proofs_verified
                    me_only_prepared
              }
          } 
      *)
      conv
        (fun num_inputs output c primary ->
          let auxiliary =
            auxiliary_input ~run ?handlers ~return_typ ~output ~num_inputs c
              primary
          in
          let output =
            let (Typ return_typ) = return_typ in
            let fields, aux = return_typ.var_to_fields output in
            let read_cvar =
              let get_one i =
                if i  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 () in
      let next_input = ref 1 in
      let store_field_elt x =
        let v = !next_input in
        incr next_input ;
        Field.Vector.emplace_back primary_input x ;
        Cvar.Unsafe.of_index v
      in
      let 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 () )
            in
            cont0 !next_input retval (k ()) primary_input
        | Typ { var_of_fields; value_to_fields; _ } :: t' ->
            fun value ->
              let fields, aux = value_to_fields value in
              let fields = Array.map ~f:store_field_elt fields in
              let var = var_of_fields (fields, aux) in
              go t' (fun () -> k () var)
      in
      go 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 c
              primary
          in
          let 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  mark_active ~f:x)

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

(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) in
    let aux = Field.Vector.create () in
    let handler =
      List.fold ~init:Request.Handler.fail handlers ~f:(fun handler h ->
          Request.Handler.(push handler (create_single h)) )
    in
    let state =
      Runner.State.make ?system ~num_inputs ~input:(pack_field_vec input)
        ~next_auxiliary ~aux:(pack_field_vec aux) ~handler ~with_witness:true ()
    in
    let state, res = run t0 state in
    let res, _ = return_typ.var_to_fields res in
    let output, _ = return_typ.var_to_fields output in
    let _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 )
    in
    Option.iter system ~f:(fun system ->
        let auxiliary_input_size = !next_auxiliary - (1 + num_inputs) in
        R1CS_constraint_system.set_auxiliary_input_size system
          auxiliary_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 in
    let { handler; _ } = !state in
    state := { !state with handler = Request.Handler.push handler h } ;
    let a = x () in
    state := { !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) in

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
      | [] ->
          let () = Printf.printf "ZYD inject_wrapper []\n" in
          fun x -> f x
      | _ :: spec ->
          let () = Printf.printf "ZYD inject_wrapper Some\n" in
          fun 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 in
  active_counters := this_functor_id :: counters ;
  try
    let ret = f () in (* 此处的f函数为wrap.wrap的x函数 *)
    active_counters := counters ;
    ret
  with 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

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中的区块证明