Mina中的约束系统代码解析
Posted mutourend
tags:
篇首语：本文由小常识网(cha138.com)小编为大家整理，主要介绍了Mina中的约束系统代码解析相关的知识，希望对你有一定的参考价值。
1. 引言
以Backend.Tick.R1CS_constraint_system为例，其中Tick对应Vesta（Step）曲线，用于生成Mina中的区块和交易证明。
R1CS_constraint_system统一调用plonk_constraint_system.ml中的Make来构建：
module R1CS_constraint_system =
Plonk_constraint_system.Make (Field) (Kimchi.Protocol.Gates.Vector.Fp)
(struct
let params =
Sponge.Params.(
map pasta_p_3 ~f:(fun x ->
Field.of_bigint (Bigint256.of_decimal_string x)))
end)
module Make
(Fp : Field.S)
(* We create a type for gate vector, instead of using `Gate.t list`. If we did, we would have to convert it to a `Gate.t array` to pass it across the FFI boundary, where then it gets converted to a `Vec<Gate>`; it's more efficient to just create the `Vec<Gate>` directly. *)
(Gates : Gate_vector_intf with type field := Fp.t)
(Params : sig
val params : Fp.t Params.t
end) = 。。。。。
2. 约束系统定义
约束系统结构体定义为：
type ('a, 'f) t =
(* map of cells that share the same value (enforced by to the permutation) *)
equivalence_classes : Row.t Position.t list V.Table.t
; (* How to compute each internal variable (as a linear combination of other variables) *)
internal_vars : (('f * V.t) list * 'f option) Internal_var.Table.t
; (* The variables that hold each witness value for each row, in reverse order *)
mutable rows_rev : V.t option array list
; (* a circuit is described by a series of gates. A gate is finalized if TKTK *)
mutable gates :
[ `Finalized | `Unfinalized_rev of (unit, 'f) Gate_spec.t list ]
; (* an instruction pointer *)
mutable next_row : int
; (* hash of the circuit, for distinguishing different circuits *)
mutable hash : Hash_state.t
; (* the size of the public input (which fills the first rows of our constraint system *)
public_input_size : int Core_kernel.Set_once.t
; (* whatever is not public input *)
mutable auxiliary_input_size : int
; (* V.t's corresponding to constant values. We reuse them so we don't need to
use a fresh generic constraint each time to create a constant. *)
cached_constants : ('f, V.t) Core_kernel.Hashtbl.t
(* The [equivalence_classes] field keeps track of the positions which must be
enforced to be equivalent due to the fact that they correspond to the same V.t value.
I.e., positions that are different usages of the same [V.t].
We use a union-find data structure to track equalities that a constraint system wants
enforced *between* [V.t] values. Then, at the end, for all [V.t]s that have been unioned
together, we combine their equivalence classes in the [equivalence_classes] table into
a single equivalence class, so that the permutation argument enforces these desired equalities
as well. *)
; union_finds : V.t Core_kernel.Union_find.t V.Table.t
Backend.Tick.R1CS_constraint_system.create()会对约束系统初始化为：
(* initializes a constraint system *)
let create () : t =
public_input_size = Set_once.create ()
; internal_vars = Internal_var.Table.create ()
; gates = `Unfinalized_rev [] (* Gates.create () *)
; rows_rev = []
; next_row = 0
; equivalence_classes = V.Table.create ()
; hash = Hash_state.empty
; auxiliary_input_size = 0
; cached_constants = Hashtbl.create (module Fp)
; union_finds = V.Table.create ()
3. Impls.Step.Constraint定义
Impls.Step.Constraint为递归结构：
(** Rank-1 constraints over !type:Field.ts. *)
module rec Constraint : sig
type t = (Field.t, Field.Constant.t) Constraint0.t
。。。。。
(* Constraint0.t结构为： *)
type ('v, 'f) t = ('v, 'f) basic_with_annotation list [@@deriving sexp]
type ('v, 'f) basic_with_annotation =
basic: ('v, 'f) basic; annotation: string option
4. Pickles.ml中测试用例代码解析
Pickles.ml中的测试用例中的约束规则为：
~choices:(fun ~self ->
[ identifier = "main"
; prevs = [ self; self ]
; main =
(fun [ prev; _ ] self ->
let is_base_case = Field.equal Field.zero self in
let proof_must_verify = Boolean.not is_base_case in
let self_correct = Field.(equal (one + prev) self) in
Boolean.Assert.any [ self_correct; is_base_case ] ;
[ proof_must_verify; Boolean.false_ ])
; main_value =
(fun _ self ->
let is_base_case = Field.Constant.(equal zero self) in
let proof_must_verify = not is_base_case in
[ proof_must_verify; false ])
])
相应的Pickles proof system对应的inductive rule规则为：
(* This type models an "inductive rule". It includes
- the list of previous statements which this one assumes
- the snarky main function
- an unchecked version of the main function which computes the "should verify" flags that
allow predecessor proofs to conditionally fail to verify
*)
type ('prev_vars, 'prev_values, 'widths, 'heights, 'a_var, 'a_value) t =
identifier : string
; prevs : ('prev_vars, 'prev_values, 'widths, 'heights) H4.T(Tag).t
; main : 'prev_vars H1.T(Id).t -> 'a_var -> 'prev_vars H1.T(E01(B)).t
; main_value :
'prev_values H1.T(Id).t -> 'a_value -> 'prev_vars H1.T(E01(Bool)).t
在step_main.ml的step_main()内构建的main函数会调用choices中的main函数构建约束系统：
let proofs_should_verify =
with_label "rule_main" (fun () -> rule.main prev_statements app_state)
in 。。。。。
4.1 log_step
let log_step main typ name index =
let module Constraints = Snarky_log.Constraints (Impls.Step.Internal_Basic) in
let log =
let weight =
let sys = Backend.Tick.R1CS_constraint_system.create () in (* 只调用一次 *)
fun (c : Impls.Step.Constraint.t) -> (* 该函数会被多次调用 *)
let prev = sys.next_row in
List.iter c ~f:(fun annotation; basic ->
Backend.Tick.R1CS_constraint_system.add_constraint sys
?label:annotation basic) ;
let next = sys.next_row in
next - prev
in
Constraints.log ~weight
Impls.Step.(
make_checked (fun () : unit ->
let x = with_label __LOC__ (fun () -> exists typ) in
main x ()))
in
if profile_constraints then
Snarky_log.to_file
(sprintf "step-snark-%s-%d.json" name (Index.to_int index))
log
其中的make_checked为：【为Direct类型-》Pure类型。】
let make_checked x = Types.Checked.Direct (as_stateful x, fun x -> Pure x)
val make_checked : (unit -> 'a) -> ('a, prover_state, field) Types.Checked.t
对应在snarky/src/base/checked.ml的constraint_count_aux递归函数，会依次进入Direct和Pure两个分支条件内，在Direct分支内会将run_state（为用于run a checked computation的internal state）初始化为：
let state =
Run_state.
system= None
; input= Vector.null
; aux= Vector.null
; eval_constraints= false
; num_inputs= 0
; next_auxiliary= ref 1
; prover_state= None
; stack= []
; handler= Request.Handler.fail
; is_running= true
; as_prover= ref false
; log_constraint= Some log_constraint
(** run_state.ml中：The internal state used to run a checked computation. *)
type ('prover_state, '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
; prover_state: 'prover_state option
; 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
snarky/src/base/checked.ml的constraint_count_aux递归函数的Direct分支内的d state，实际调用的是step_main()函数内构建的main函数。
在step_main.ml的step_main()内构建的main函数会调用choices中的main函数构建约束系统：
let proofs_should_verify =
with_label "rule_main" (fun () -> rule.main prev_statements app_state)
in 。。。。。
将choices中的main函数内定义的规则转换为约束系统，具体见snark0.ml中的实现。
以let proof_must_verify = Boolean.not is_base_case为例，对应为：
(* 第一个为变量名，第二个为变量值 *)
let not (x : var) : var = create Cvar.((true_ :> Cvar.t) - (x :> Cvar.t))
附录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中的约束系统代码解析的主要内容，如果未能解决你的问题，请参考以下文章