Mina 证明实现过程
2023-03-28 本文已影响0人
雪落无留痕
之前Mina项目研究的笔记
Snarker_worker 证明
Snarker worker 主要生成交易证明以及合并证明，所有在Scan State一颗子树上的所有交易状态能“合并”成一个证明。以4个交易为例，4个交易的状态“合并”到一个证明，证明从x0到x4的正确执行。
run_snark_worker
let%bind worker_state = Prod.Worker_state.create ~proof_level ()
创建过程为：
let create ~constraint_constants ~proof_level () =
let m =
match proof_level with
| Genesis_constants.Proof_level.Full ->
Some
( module Transaction_snark.Make (struct
let constraint_constants = constraint_constants
let proof_level = proof_level
end) : S )
| Check | None ->
None
in
Deferred.return { m; cache = Cache.create (); proof_level }
worker_state 的类型为：
type t =
{ m : (module S) option //其中 S = Transaction_snark.S
; cache : Cache.t
; proof_level : Genesis_constants.Proof_level.t
}
其中 cache 为存放 statement (key) 和 proof (value) 类型的Hash表缓存，size 为 100.
获取 public_key:
let public_key = fst (Lazy.force Mina_base.Sample_keypairs.keypairs).(0)
手续费：
fee = Currency.Fee.of_int 10
生成message:
message = Mina_base.Sok_message.create ~fee ~prover:public_key
message 的类型为：
type t =
{ fee : Currency.Fee.Stable.V1.t
; prover : Public_key.Compressed.Stable.V1.t
}
生成证明：
match Prod.perform_single worker_state ~message spec with
| Ok (proof, time) ->
Caml.Format.printf
!"Successfully proved in %{sexp: Time.Span.t}.@.Proof \
was:@.%{sexp: Transaction_snark.t}@."
time proof ;
exit 0
| Error err ->
Caml.Format.printf
!"Proving failed with error:@.%s"
(Error.to_string_hum err) ;
exit 1)
perform_single
计算Sok 消息的Hash 值：
let sok_digest = Mina_base.Sok_message.digest message
获取statement:
let statement = Work.Single.Spec.statement single
其中 single的类型为：
(* bin_io is for uptime service SNARK worker *)
type single_spec =
( Transaction.Stable.Latest.t
, Transaction_witness.Stable.Latest.t
, Transaction_snark.Stable.Latest.t )
Snark_work_lib.Work.Single.Spec.Stable.Latest.t
[@@deriving bin_io_unversioned, sexp]
type ('transition, 'witness, 'ledger_proof) t =
| Transition of //对应着Transition 类型
Transaction_snark.Statement.Stable.V1.t * 'transition * 'witness
| Merge of // 对应着Merge 类型
Transaction_snark.Statement.Stable.V1.t
* 'ledger_proof
* 'ledger_proof
[@@deriving sexp, to_yojson]
Work.Single.Spec.statement 函数定义为：
let statement = function Transition (s, _, _) -> s | Merge (s, _, _) -> s
返回值statement的类型为：Transaction_snark.Statement.Stable.V1.t
type ( 'ledger_hash
, 'amount
, 'pending_coinbase
, 'fee_excess
, 'token_id
, 'sok_digest )
t =
{ source : 'ledger_hash
; target : 'ledger_hash
; supply_increase : 'amount
; pending_coinbase_stack_state : 'pending_coinbase
; fee_excess : 'fee_excess
; next_available_token_before : 'token_id
; next_available_token_after : 'token_id
; sok_digest : 'sok_digest
}
[@@deriving compare, equal, hash, sexp, yojson, hlist]
对于Transition, 根据不同的交易类型，生成证明， 对于Merge类型，生成相就的Merge 证明。
match single with
| Work.Single.Spec.Transition // 生成交易的证明
(input, t, (w : Transaction_witness.t)) ->
process (fun () ->
let%bind t =
Deferred.return
@@
(* Validate the received transaction *)
match t with //匹配交易类型
| Command (Signed_command cmd) -> (
match Signed_command.check cmd with
| Some cmd ->
( Ok (Command (Signed_command cmd))
: Transaction.Valid.t Or_error.t )
| None ->
Or_error.errorf
"Command has an invalid signature" )
| Command (Parties _) ->
failwith "TODO"
| Fee_transfer ft ->
Ok (Fee_transfer ft)
| Coinbase cb ->
Ok (Coinbase cb)
in
Deferred.Or_error.try_with ~here:[%here] (fun () ->
M.of_transaction ~sok_digest ~snapp_account1:None
~snapp_account2:None
~source:input.Transaction_snark.Statement.source
~target:input.target
{ Transaction_protocol_state.Poly.transaction = t
; block_data = w.protocol_state_body
}
~init_stack:w.init_stack
~next_available_token_before:
input.next_available_token_before
~next_available_token_after:
input.next_available_token_after
~pending_coinbase_stack_state:
input
.Transaction_snark.Statement
.pending_coinbase_stack_state
(unstage (Mina_base.Sparse_ledger.handler w.ledger))))
| Merge (_, proof1, proof2) ->
process (fun () -> M.merge ~sok_digest proof1 proof2) ) // 生成Merge 的证明
Base proof
Transaction
Transaction.Stable.Latest.t的类型为：
type 'command t =
| Command of 'command
| Fee_transfer of Fee_transfer.Stable.V1.t
| Coinbase of Coinbase.Stable.V1.t
[@@deriving sexp, compare, equal, hash, yojson]
type t = User_command.Valid.Stable.V2.t Poly.Stable.V1.t
[@@deriving sexp, compare, equal, hash, yojson]
其中Command 类型为：
// Command类型：
type ('u, 's) t = Signed_command of 'u | Parties of 's
[@@deriving sexp, compare, equal, hash, yojson]
// Signed_command类型：
type ('payload, 'pk, 'signature) t =
{ payload : 'payload; signer : 'pk; signature : 'signature }
[@@deriving compare, sexp, hash, yojson, equal]
Parties类型为：
type t =
{ fee_payer : Party.Signed.Stable.V1.t
; other_parties : Party.Stable.V1.t list
; protocol_state : Snapp_predicate.Protocol_state.Stable.V1.t
}
[@@deriving sexp, compare, equal, hash, yojson]
Fee_Transfer交易类型为：
type t =
{ receiver_pk : Public_key.Compressed.Stable.V1.t // 接收者公钥
; fee : Currency.Fee.Stable.V1.t // 手续费用
; fee_token : Token_id.Stable.V1.t // 费用token
}
[@@deriving sexp, compare, equal, yojson, hash]
Coinbase交易类型：
type t =
{ receiver : Public_key.Compressed.Stable.V1.t
; amount : Currency.Amount.Stable.V1.t
; fee_transfer : Fee_transfer.Stable.V1.t option
}
[@@deriving sexp, compare, equal, hash, yojson]
Transaction_witness
Transaction_witness.Stable.Latest.t的类型为：
type t =
{ ledger : Mina_base.Sparse_ledger.Stable.V2.t
; protocol_state_body : Mina_state.Protocol_state.Body.Value.Stable.V1.t
; init_stack : Mina_base.Pending_coinbase.Stack_versioned.Stable.V1.t
; status : Mina_base.Transaction_status.Stable.V1.t
}
其中Mina_base.Sparse_ledger.Stable.V2.t 的类型为：
type t =
( Ledger_hash.Stable.V1.t
, Account_id.Stable.V1.t
, Account.Stable.V2.t
, Token_id.Stable.V1.t )
Sparse_ledger_lib.Sparse_ledger.T.Stable.V1.t
[@@deriving yojson, sexp]
// Sparse_ledger_lib.Sparse_ledger.T.Stable.V1.t类型为：
type ('hash, 'key, 'account, 'token_id) t =
{ indexes : ('key * int) list
; depth : int
; tree : ('hash, 'account) Tree.Stable.V1.t
; next_available_token : 'token_id
}
[@@deriving sexp, yojson]
Mina_state.Protocol_state.Body.Value.Stable.V1.t 类型为：
type ('state_hash, 'blockchain_state, 'consensus_state, 'constants) t =
{ genesis_state_hash : 'state_hash
; blockchain_state : 'blockchain_state
; consensus_state : 'consensus_state
; constants : 'constants
}
[@@deriving sexp, equal, compare, yojson, hash, version, hlist]
type t =
( State_hash.Stable.V1.t
, Blockchain_state.Value.Stable.V1.t
, Consensus.Data.Consensus_state.Value.Stable.V1.t
, Protocol_constants_checked.Value.Stable.V1.t )
Poly.Stable.V1.t
[@@deriving equal, ord, bin_io, hash, sexp, yojson, version]
Mina_base.Pending_coinbase.Stack_versioned.Stable.V1.t
type ('data_stack, 'state_stack) t =
{ data : 'data_stack; state : 'state_stack }
[@@deriving yojson, hash, sexp, equal, compare]
type t =
(Coinbase_stack.Stable.V1.t, State_stack.Stable.V1.t) Poly.Stable.V1.t
[@@deriving equal, yojson, hash, sexp, compare]
//Coinbase_stack.Stable.V1.t
type t = Field.t [@@deriving sexp, compare, hash, version { asserted }]
//State_stack.Stable.V1.t
type 'stack_hash t = { init : 'stack_hash; curr : 'stack_hash }
[@@deriving sexp, compare, hash, yojson, equal, hlist]
type t = Stack_hash.Stable.V1.t Poly.Stable.V1.t
[@@deriving sexp, compare, hash, equal, yojson]
Mina_base.Transaction_status.Stable.V1.t的类型为：
type t =
| Applied of Auxiliary_data.Stable.V1.t * Balance_data.Stable.V1.t
| Failed of Failure.Stable.V1.t * Balance_data.Stable.V1.t
[@@deriving sexp, yojson, equal, compare]
// Auxiliary_data.Stable.V1.t 类型：
type t =
{ fee_payer_account_creation_fee_paid :
Currency.Amount.Stable.V1.t option
; receiver_account_creation_fee_paid :
Currency.Amount.Stable.V1.t option
; created_token : Token_id.Stable.V1.t option
}
// Balance_data.Stable.V1.t 类型为：
type t =
{ fee_payer_balance : Currency.Balance.Stable.V1.t option
;
source_balance : Currency.Balance.Stable.V1.t option
; receiver_balance : Currency.Balance.Stable.V1.t option
}
[@@deriving sexp, yojson, equal, compare]
// Failure.Stable.V1.t 类型为：
type t =
| Predicate [@value 1]
| Source_not_present
| Receiver_not_present
| Amount_insufficient_to_create_account
| Cannot_pay_creation_fee_in_token
| Source_insufficient_balance
| Source_minimum_balance_violation
| Receiver_already_exists
| Not_token_owner
| Mismatched_token_permissions
| Overflow
| Signed_command_on_snapp_account
| Snapp_account_not_present
| Update_not_permitted
| Incorrect_nonce
[@@deriving sexp, yojson, equal, compare, enum]
of_transaction
函数签名为：
val of_transaction :
sok_digest:Sok_message.Digest.t
-> source:Frozen_ledger_hash.t
-> target:Frozen_ledger_hash.t
-> init_stack:Pending_coinbase.Stack.t
-> pending_coinbase_stack_state:Pending_coinbase_stack_state.t
-> next_available_token_before:Token_id.t
-> next_available_token_after:Token_id.t
-> snapp_account1:Snapp_account.t option
-> snapp_account2:Snapp_account.t option
-> Transaction.Valid.t Transaction_protocol_state.t
-> Tick.Handler.t
-> t Async.Deferred.t
返回的 t 的类型为：
// pickles.ml
module Statement_with_proof = struct
type ('s, 'max_width, _) t =
(* TODO: use Max local max branching instead of max_width *)
's * ('max_width, 'max_width) Proof.t
end
// proof.ml
type ('dlog_me_only, 'pairing_me_only) t =
('dlog_me_only, 'pairing_me_only) Stable.Latest.t =
{ statement :
( Challenge.Constant.t
, Challenge.Constant.t Scalar_challenge.t
, Tick.Field.t Shifted_value.Type1.t
, Tock.Field.t
, 'dlog_me_only
, Digest.Constant.t
, 'pairing_me_only
, Challenge.Constant.t Scalar_challenge.t Bulletproof_challenge.t
Step_bp_vec.t
, Index.t )
Types.Dlog_based.Statement.Minimal.t
; prev_evals :
(Tick.Field.t, Tick.Field.t array) Dlog_plonk_types.All_evals.t
; proof : Tock.Proof.t
}
[@@deriving compare, sexp, yojson, hash, equal]
// pallas_based_plonk.ml
type t =
( Kimchi.Foundations.Fp.t Kimchi.Foundations.or_infinity
, Kimchi.Foundations.Fq.t )
Kimchi.Protocol.prover_proof
对应着Rust中的ProverProof结构为：
/// The proof that the prover creates from a [ProverIndex] and a `witness`.
#[derive(Clone)]
pub struct ProverProof<G: AffineCurve> {
/// All the polynomial commitments required in the proof
pub commitments: ProverCommitments<G>,
/// batched commitment opening proof
pub proof: OpeningProof<G>,
/// Two evaluations over a number of committed polynomials
// TODO(mimoo): that really should be a type Evals { z: PE, zw: PE }
pub evals: [ProofEvaluations<Vec<ScalarField<G>>>; 2],
/// Required evaluation for [Maller's optimization](https://o1-labs.github.io/mina-book/crypto/plonk/maller_15.html#the-evaluation-of-l)
pub ft_eval1: ScalarField<G>,
/// The public input
pub public: Vec<ScalarField<G>>,
/// The challenges underlying the optional polynomials folded into the proof
pub prev_challenges: Vec<(Vec<ScalarField<G>>, PolyComm<G>)>,
}
constraint_system
system
约束系统的生成从下面开始：
let tag, cache_handle, p, Pickles.Provers.[ base; merge ] =
system ~proof_level ~constraint_constants
其中 proof_level 的类型Genesis_constants.Proof_level.t为：
type t = Full | Check | None [@@deriving bin_io_unversioned, equal]
constraint_constants的类型Genesis_constants.Constraint_constants.t为：
type t =
{ sub_windows_per_window : int
; ledger_depth : int
; work_delay : int
; block_window_duration_ms : int
; transaction_capacity_log_2 : int
; pending_coinbase_depth : int
; coinbase_amount : Currency.Amount.Stable.Latest.t
; supercharged_coinbase_factor : int
; account_creation_fee : Currency.Fee.Stable.Latest.t
; fork : Fork_constants.t option
}
[@@deriving bin_io_unversioned, sexp, equal, compare, yojson]
system 函数主要调用Pickles.compile函数，根据约束条件条件，生成约束系统。
let system ~proof_level ~constraint_constants =
time "Transaction_snark.system" (fun () ->
Pickles.compile ~cache:Cache_dir.cache
(module Statement.With_sok.Checked)
(module Statement.With_sok)
~typ:Statement.With_sok.typ
~branches:(module Nat.N2)
~max_branching:(module Nat.N2)
~name:"transaction-snark"
~constraint_constants:
(Genesis_constants.Constraint_constants.to_snark_keys_header
constraint_constants)
~choices:(fun ~self ->
[ Base.rule ~constraint_constants; Merge.rule ~proof_level self ]))
Base.rule
其中Base.rule函数是关键：
let rule ~constraint_constants : _ Pickles.Inductive_rule.t =
{ identifier = "transaction"
; prevs = []
; main =
(fun [] x ->
Run.run_checked (main ~constraint_constants x) ;
[])
; main_value = (fun [] _ -> [])
}
它的返回值类型Pickles.Inductive_rule.t 为：
(* 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
}
module T (Statement : T0) (Statement_value : T0) = struct
type nonrec ('prev_vars, 'prev_values, 'widths, 'heights) t =
( 'prev_vars
, 'prev_values
, 'widths
, 'heights
, Statement.t
, Statement_value.t )
t
end
main
(* spec for [main statement]:
constraints pass iff there exists
t : Tagged_transaction.t
such that
- applying [t] to ledger with merkle hash [l1] results in ledger with merkle hash [l2].
- applying [t] to [pc.source] with results in pending coinbase stack [pc.target]
- t has fee excess equal to [fee_excess]
- t has supply increase equal to [supply_increase]
where statement includes
l1 : Frozen_ledger_hash.t,
l2 : Frozen_ledger_hash.t,
fee_excess : Amount.Signed.t,
supply_increase : Amount.t
pc: Pending_coinbase_stack_state.t
*)
let%snarkydef main ~constraint_constants
(statement : Statement.With_sok.Checked.t) =
let%bind () = dummy_constraints () in
let%bind (module Shifted) = Tick.Inner_curve.Checked.Shifted.create () in
let%bind t =
with_label __LOC__
(exists Transaction_union.typ ~request:(As_prover.return Transaction))
in
let%bind pending_coinbase_init =
exists Pending_coinbase.Stack.typ ~request:(As_prover.return Init_stack)
in
let%bind state_body =
exists
(Mina_state.Protocol_state.Body.typ ~constraint_constants)
~request:(As_prover.return State_body)
in
let pc = statement.pending_coinbase_stack_state in
// 计算应用交易后的 root , fee_excess, supply_increase, next_available_token_after变化
let%bind root_after, fee_excess, supply_increase, next_available_token_after
=
apply_tagged_transaction ~constraint_constants
(module Shifted)
statement.source pending_coinbase_init pc.source pc.target
statement.next_available_token_before state_body t
in
let%bind fee_excess =
(* Use the default token for the fee excess if it is zero.
This matches the behaviour of [Fee_excess.rebalance], which allows
[verify_complete_merge] to verify a proof without knowledge of the
particular fee tokens used.
*)
let%bind fee_excess_zero =
Amount.equal_var fee_excess.magnitude Amount.(var_of_t zero)
in
let%map fee_token_l =
Token_id.Checked.if_ fee_excess_zero
~then_:Token_id.(var_of_t default)
~else_:t.payload.common.fee_token
in
{ Fee_excess.fee_token_l
; fee_excess_l = Signed_poly.map ~f:Amount.Checked.to_fee fee_excess
; fee_token_r = Token_id.(var_of_t default)
; fee_excess_r = Fee.Signed.(Checked.constant zero)
}
in
// 验证的约束条件
Checked.all_unit
[ Frozen_ledger_hash.assert_equal root_after statement.target
; Currency.Amount.Checked.assert_equal supply_increase
statement.supply_increase
; Fee_excess.assert_equal_checked fee_excess statement.fee_excess
; Token_id.Checked.Assert.equal next_available_token_after
statement.next_available_token_after
]
main函数保证apply_tagged_transaction 后的状态和statement中一致。
apply_tagged_transaction电路实现如下的功能：
- 更新pending coinbase stack
- 执行交易检查，确定交易状态
- 更新source和receiver的账户（包括fee的计算），如果交易失败，只需要更新fee
- 确保账户更新后的状态树根一致
- 更新fee excess (fee的增量信息)
- 更新next token ID（如果是mint token的操作，next Token ID需要加1）
- 更新total supply的增量（如果是coinbase交易，total supply会增加）
Base的证明电路证明了在source Ledger Hash的基础上执行某个交易，账户状态改变正确。这些状态包括：账户树树根，fee excess，next token ID，total supply增量等等。
其中fee_excess, supply_increase, next_available_token的更新方式如下：
let fee_excess
({ body = { tag; amount; _ }; common = { fee_token; fee; _ } } : t) =
match tag with
| Payment | Stake_delegation | Create_account | Mint_tokens ->
(* For all user commands, the fee excess is just the fee. *)
Fee_excess.of_single (fee_token, Fee.Signed.of_unsigned fee)
| Fee_transfer ->
let excess =
Option.value_exn (Amount.add_fee amount fee)
|> Amount.to_fee |> Fee.Signed.of_unsigned |> Fee.Signed.negate
in
Fee_excess.of_single (fee_token, excess)
| Coinbase ->
Fee_excess.of_single (Token_id.default, Fee.Signed.zero)
let supply_increase (payload : payload) =
let tag = payload.body.tag in
match tag with
| Coinbase ->
payload.body.amount
| Payment | Stake_delegation | Create_account | Mint_tokens | Fee_transfer ->
Amount.zero
let next_available_token (payload : payload) tid =
match payload.body.tag with
| Payment | Stake_delegation | Mint_tokens | Coinbase | Fee_transfer ->
tid
| Create_account when Token_id.(equal invalid) payload.body.token_id ->
(* Creating a new token. *)
Token_id.next tid
| Create_account ->
(* Creating an account for an existing token. *)
tid
Pickles.compile
let compile :
type a_var a_value prev_varss prev_valuess widthss heightss max_branching branches.
?self:(a_var, a_value, max_branching, branches) Tag.t
-> ?cache:Key_cache.Spec.t list
-> ?disk_keys:
(Cache.Step.Key.Verification.t, branches) Vector.t
* Cache.Wrap.Key.Verification.t
-> (module Statement_var_intf with type t = a_var)
-> (module Statement_value_intf with type t = a_value)
-> typ:(a_var, a_value) Impls.Step.Typ.t
-> branches:(module Nat.Intf with type n = branches)
-> max_branching:(module Nat.Add.Intf with type n = max_branching)
-> name:string
-> constraint_constants:Snark_keys_header.Constraint_constants.t
-> choices:
( self:(a_var, a_value, max_branching, branches) Tag.t
-> ( prev_varss
, prev_valuess
, widthss
, heightss
, a_var
, a_value )
H4_2.T(Inductive_rule).t)
-> (a_var, a_value, max_branching, branches) Tag.t
* Cache_handle.t
* (module Proof_intf
with type t = (max_branching, max_branching) Proof.t
and type statement = a_value)
* ( prev_valuess
, widthss
, heightss
, a_value
, (max_branching, max_branching) Proof.t Deferred.t )
H3_2.T(Prover).t =
fun ?self ?(cache = []) ?disk_keys (module A_var) (module A_value) ~typ
~branches ~max_branching ~name ~constraint_constants ~choices ->
let self =
match self with
| None ->
{ Tag.id = Type_equal.Id.create ~name sexp_of_opaque; kind = Compiled }
| Some self ->
self
in
let module M = Make (A_var) (A_value) in
let rec conv_irs :
type v1ss v2ss wss hss.
(v1ss, v2ss, wss, hss, a_var, a_value) H4_2.T(Inductive_rule).t
-> (v1ss, v2ss, wss, hss) H4.T(M.IR).t = function
| [] ->
[]
| r :: rs ->
r :: conv_irs rs
in
let provers, wrap_vk, wrap_disk_key, cache_handle =
M.compile ~self ~cache ?disk_keys ~branches ~max_branching ~name ~typ
~constraint_constants ~choices:(fun ~self -> conv_irs (choices ~self))
in
let (module Max_branching) = max_branching in
let T = Max_branching.eq in
let module P = struct
type statement = A_value.t
module Max_local_max_branching = Max_branching
module Max_branching_vec = Nvector (Max_branching)
include Proof.Make (Max_branching) (Max_local_max_branching)
let id = wrap_disk_key
let verification_key = wrap_vk
let verify ts =
verify
(module Max_branching)
(module A_value)
(Lazy.force verification_key)
ts
let statement (T p : t) = p.statement.pass_through.app_state
end in
(self, cache_handle, (module P), provers)
其中关键调用了：
let provers, wrap_vk, wrap_disk_key, cache_handle =
M.compile ~self ~cache ?disk_keys ~branches ~max_branching ~name ~typ
~constraint_constants ~choices:(fun ~self -> conv_irs (choices ~self))
在M.compile合成约束系统，生成pk 和 vk
let cs = constraint_system ~exposing:[ typ ] main
let ((pk, vk) as res) =
Common.time "step read or generate" (fun () ->
Cache.Step.read_or_generate cache k_p k_v typ main)
constraint_system
let constraint_system (type a s checked k_var) :
run:(a, s, checked) Checked.Runner.run
-> exposing:(checked, _, k_var, _) t
-> k_var
-> R1CS_constraint_system.t =
fun ~run ~exposing k -> r1cs_h ~run (ref 1) exposing k
let r1cs_h : type a s checked r2 k1 k2.
run:(a, s, checked) Checked.Runner.run
-> int ref
-> (checked, r2, k1, k2) t
-> k1
-> R1CS_constraint_system.t =
fun ~run next_input t k ->
let r = collect_input_constraints next_input t k in
let run_in_run r state =
let state, x = Checked.run r state in
run x state
in
Checked.constraint_system ~run:run_in_run ~num_inputs:(!next_input - 1) r
let constraint_system ~run ~num_inputs t : R1CS_constraint_system.t =
let input = field_vec () in
let next_auxiliary = ref (1 + num_inputs) in
let aux = field_vec () in
let system = R1CS_constraint_system.create () in
let state =
Runner.State.make ~num_inputs ~input ~next_auxiliary ~aux ~system None
in1
ignore (run t state) ;
let auxiliary_input_size = !next_auxiliary - (1 + num_inputs) in
R1CS_constraint_system.set_auxiliary_input_size system
auxiliary_input_size ;
system
其中 R1CS_constraint_system定义为：
module R1CS_constraint_system =
Plonk_constraint_system.Make (Field) (Kimchi.Protocol.Gates.Vector.Fq)
(struct
let params =
Sponge.Params.(
map pasta_q_3 ~f:(fun x ->
Field.of_bigint (Bigint256.of_decimal_string x)))
end)
R1CS_constraint_system.t 的类型为：
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
}
pk and vk
对于pk 和 vk:
module Keypair = struct
type t = {pk: Proving_key.t; vk: Verification_key.t}
[@@deriving fields, bin_io]
let create = Fields.create
let of_backend_keypair kp = {pk= Keypair.pk kp; vk= Keypair.vk kp}
let generate = Fn.compose of_backend_keypair Backend.Keypair.create
end
对应着：
module Keypair = Dlog_plonk_based_keypair.Make (struct
let name = "pallas"
module Rounds = Rounds
module Urs = Kimchi.Protocol.SRS.Fq
module Index = Kimchi.Protocol.Index.Fq // 对应着 pk
module Curve = Curve
module Poly_comm = Fq_poly_comm
module Scalar_field = Field
module Verifier_index = Kimchi.Protocol.VerifierIndex.Fq // 应对着vk
module Gate_vector = Kimchi.Protocol.Gates.Vector.Fq
module Constraint_system = R1CS_constraint_system
end)
Pickles.Provers.[ base; merge ]
let of_transaction_union sok_digest source target ~init_stack
~pending_coinbase_stack_state ~next_available_token_before
~next_available_token_after transaction state_body handler =
let s =
{ Statement.source
; target
; sok_digest
; next_available_token_before
; next_available_token_after
; fee_excess = Transaction_union.fee_excess transaction
; supply_increase = Transaction_union.supply_increase transaction
; pending_coinbase_stack_state
}
in
let%map.Async.Deferred proof =
base []
~handler:
(Base.transaction_union_handler handler transaction state_body
init_stack)
s
in
{ statement = s; proof }
Merge proof
run_ snark_work
| Merge (_, proof1, proof2) ->
process (fun () -> M.merge ~sok_digest proof1 proof2) )
其中 proof1 和 proof2 类型 Transaction_snark.Stable.Latest.t为：
type t =
{ statement : Statement.With_sok.Stable.V1.t; proof : Proof.Stable.V2.t }
[@@deriving compare, equal, fields, sexp, version, yojson, hash]
//Statement.with_sok_Stable.V1.t
type ( 'ledger_hash
, 'amount
, 'pending_coinbase
, 'fee_excess
, 'token_id
, 'sok_digest )
poly =
( 'ledger_hash
, 'amount
, 'pending_coinbase
, 'fee_excess
, 'token_id
, 'sok_digest )
Poly.t =
{ source : 'ledger_hash
; target : 'ledger_hash
; supply_increase : 'amount
; pending_coinbase_stack_state : 'pending_coinbase
; fee_excess : 'fee_excess
; next_available_token_before : 'token_id
; next_available_token_after : 'token_id
; sok_digest : 'sok_digest
}
// Proof.Stable.V2.t
type t = Pickles.Proof.Branching_2.Stable.V2.t
[@@deriving
version { asserted }, yojson, bin_io, compare, equal, sexp, hash]
Merge .rule
let rule ~proof_level self : _ Pickles.Inductive_rule.t =
let prev_should_verify =
match proof_level with
| Genesis_constants.Proof_level.Full ->
true
| _ ->
false
in
let b = Boolean.var_of_value prev_should_verify in
{ identifier = "merge"
; prevs = [ self; self ]
; main =
(fun ps x ->
Run.run_checked (main ps x) ;
[ b; b ])
; main_value = (fun _ _ -> [ prev_should_verify; prev_should_verify ])
}
main
let%snarkydef main
([ s1; s2 ] :
(Statement.With_sok.var * (Statement.With_sok.var * _))
Pickles_types.Hlist.HlistId.t) (s : Statement.With_sok.Checked.t) =
let%bind fee_excess =
Fee_excess.combine_checked s1.Statement.fee_excess s2.Statement.fee_excess
in
let%bind () =
with_label __LOC__
(let%bind valid_pending_coinbase_stack_transition =
Pending_coinbase.Stack.Checked.check_merge
~transition1:
( s1.pending_coinbase_stack_state.source
, s1.pending_coinbase_stack_state.target )
~transition2:
( s2.pending_coinbase_stack_state.source
, s2.pending_coinbase_stack_state.target )
in
Boolean.Assert.is_true valid_pending_coinbase_stack_transition)
in
let%bind supply_increase =
Amount.Checked.add s1.supply_increase s2.supply_increase
in
Checked.all_unit
[ Fee_excess.assert_equal_checked fee_excess s.fee_excess
; Amount.Checked.assert_equal supply_increase s.supply_increase
; Frozen_ledger_hash.assert_equal s.source s1.source
; Frozen_ledger_hash.assert_equal s1.target s2.source
; Frozen_ledger_hash.assert_equal s2.target s.target
; Token_id.Checked.Assert.equal s.next_available_token_before
s1.next_available_token_before
; Token_id.Checked.Assert.equal s1.next_available_token_after
s2.next_available_token_before
; Token_id.Checked.Assert.equal s2.next_available_token_after
s.next_available_token_after
]
交易证明合并的意思是，两个Base证明的状态可以合并。举个例子：
(R0 -> R1, t0, f0, p0s, p0t, nt0, ts0)
存在一个交易t0，使状态根从R0变化到R1，f0 - fee excess， nt0 - next token ID， ts0 - total supply增量，p0s/p0t - pending coinbase的source和target。
(R1 -> R2, t1, f1, p1s, p1t, nt1, ts1)
存在一个交易t1，使状态根从R1变化到R2，f1 - fee excess， nt1 - next token ID， ts1 - total supply增量，p1s/p1t - pending coinbase的source和target。
就可以通过Merge的电路证明，这两笔交易状态连续，“合并”后的状态变化为：
(R0 -> R2, t0t1, f0+f1, p0s, p1t, nt1, ts0+ts1)
总结一下Merge的电路，验证两个s1/s2对应的证明，并验证它们的“逻辑”联系，并输出新的statement，作为合并后的状态
merge
let merge ({ statement = t12; _ } as x12) ({ statement = t23; _ } as x23)
~sok_digest =
if not (Frozen_ledger_hash.( = ) t12.target t23.source) then //验证t12.targe = t23.source
failwithf
!"Transaction_snark.merge: t12.target <> t23.source \
(%{sexp:Frozen_ledger_hash.t} vs %{sexp:Frozen_ledger_hash.t})"
t12.target t23.source () ;
if
not
(Token_id.( = ) t12.next_available_token_after
t23.next_available_token_before)
// 验证 t12.next_available_token_after = t23.next_available_token_before
then
failwithf
!"Transaction_snark.merge: t12.next_available_token_befre <> \
t23.next_available_token_after (%{sexp:Token_id.t} vs \
%{sexp:Token_id.t})"
t12.next_available_token_after t23.next_available_token_before () ;
let open Async.Deferred.Or_error.Let_syntax in
let%bind fee_excess = // 合并fee_excess
Async.return @@ Fee_excess.combine t12.fee_excess t23.fee_excess
and supply_increase = // 合并supply_increase
Amount.add t12.supply_increase t23.supply_increase
|> Option.value_map ~f:Or_error.return
~default:
(Or_error.errorf
"Transaction_snark.merge: Supply change amount overflow")
|> Async.return
in
let s : Statement.With_sok.t =
{ Statement.source = t12.source
; target = t23.target
; supply_increase
; fee_excess
; next_available_token_before = t12.next_available_token_before
; next_available_token_after = t23.next_available_token_after
; pending_coinbase_stack_state =
{ source = t12.pending_coinbase_stack_state.source
; target = t23.pending_coinbase_stack_state.target
}
; sok_digest
}
in
let%map.Async.Deferred proof = // 生成证明
merge [ (x12.statement, x12.proof); (x23.statement, x23.proof) ] s
in
Ok { statement = s; proof }
区块证明
区块证明实现在lib/blockchain_snark/blockchain_snark_state.ml的step函数，证明某个区块的合法性。大体的证明思路如下：
证明存在前面一个世界状态，通过这个状态可以计算出新的Consensus信息。由新的Consensus信息和新的需证明的链的状态信息构建新的世界状态。同时存在一个Transaction证明，证明世界状态从前面一个状态变化到新的构建的世界状态。
(* Blockchain_snark ~old ~nonce ~ledger_snark ~ledger_hash ~timestamp ~new_hash
Input:
old : Blockchain.t
old_snark : proof
nonce : int
work_snark : proof
ledger_hash : Ledger_hash.t
timestamp : Time.t
new_hash : State_hash.t
Witness:
transition : Transition.t
such that
the old_snark verifies against old
new = update_with_asserts(old, nonce, timestamp, ledger_hash)
hash(new) = new_hash
the work_snark verifies against the old.ledger_hash and new_ledger_hash
new.timestamp > old.timestamp
transition consensus data is valid
new consensus state is a function of the old consensus state
*)
let%snarkydef step ~(logger : Logger.t)
~(proof_level : Genesis_constants.Proof_level.t)
~(constraint_constants : Genesis_constants.Constraint_constants.t)
Hlist.HlistId.
[ previous_state_hash
; (txn_snark : Transaction_snark.Statement.With_sok.Checked.t)
] new_state_hash : (_, _) Tick.Checked.t =
let%bind transition =
with_label __LOC__
(exists Snark_transition.typ ~request:(As_prover.return Transition))
in
let%bind previous_state, previous_state_body_hash =
let%bind t =
with_label __LOC__
(exists
(Protocol_state.typ ~constraint_constants)
~request:(As_prover.return Prev_state))
in
let%bind h, body = Protocol_state.hash_checked t in
let%map () =
with_label __LOC__ (State_hash.assert_equal h previous_state_hash)
in
(t, body)
in
let%bind `Success updated_consensus_state, consensus_state =
with_label __LOC__
(Consensus_state_hooks.next_state_checked ~constraint_constants
~prev_state:previous_state ~prev_state_hash:previous_state_hash
transition txn_snark.supply_increase)
in
let supercharge_coinbase =
Consensus.Data.Consensus_state.supercharge_coinbase_var consensus_state
in
let prev_pending_coinbase_root =
previous_state |> Protocol_state.blockchain_state
|> Blockchain_state.staged_ledger_hash
|> Staged_ledger_hash.pending_coinbase_hash_var
in
let%bind genesis_state_hash =
(*get the genesis state hash from previous state unless previous state is the genesis state itslef*)
Protocol_state.genesis_state_hash_checked ~state_hash:previous_state_hash
previous_state
in
let%bind new_state, is_base_case =
let t =
Protocol_state.create_var ~previous_state_hash ~genesis_state_hash
~blockchain_state:(Snark_transition.blockchain_state transition)
~consensus_state
~constants:(Protocol_state.constants previous_state)
in
let%bind is_base_case =
Protocol_state.consensus_state t
|> Consensus.Data.Consensus_state.is_genesis_state_var
in
let%bind previous_state_hash =
match constraint_constants.fork with
| Some { previous_state_hash = fork_prev; _ } ->
State_hash.if_ is_base_case
~then_:(State_hash.var_of_t fork_prev)
~else_:t.previous_state_hash
| None ->
Checked.return t.previous_state_hash
in
let t = { t with previous_state_hash } in
let%map () =
let%bind h, _ = Protocol_state.hash_checked t in
with_label __LOC__ (State_hash.assert_equal h new_state_hash)
in
(t, is_base_case)
in
let%bind txn_snark_should_verify, success =
let%bind ledger_hash_didn't_change =
Frozen_ledger_hash.equal_var
( previous_state |> Protocol_state.blockchain_state
|> Blockchain_state.snarked_ledger_hash )
txn_snark.target
and supply_increase_is_zero =
Currency.Amount.(equal_var txn_snark.supply_increase (var_of_t zero))
in
let%bind new_pending_coinbase_hash, deleted_stack, no_coinbases_popped =
let coinbase_receiver =
Consensus.Data.Consensus_state.coinbase_receiver_var consensus_state
in
let%bind root_after_delete, deleted_stack =
Pending_coinbase.Checked.pop_coinbases ~constraint_constants
prev_pending_coinbase_root
~proof_emitted:(Boolean.not ledger_hash_didn't_change)
in
(*If snarked ledger hash did not change (no new ledger proof) then pop_coinbases should be a no-op*)
let%bind no_coinbases_popped =
Pending_coinbase.Hash.equal_var root_after_delete
prev_pending_coinbase_root
in
(*new stack or update one*)
let%map new_root =
with_label __LOC__
(Pending_coinbase.Checked.add_coinbase ~constraint_constants
root_after_delete
(Snark_transition.pending_coinbase_update transition)
~coinbase_receiver ~supercharge_coinbase previous_state_body_hash)
in
(new_root, deleted_stack, no_coinbases_popped)
in
let pending_coinbase_source_stack =
Pending_coinbase.Stack.Checked.create_with deleted_stack
in
let%bind txn_snark_input_correct =
let lh t =
Protocol_state.blockchain_state t
|> Blockchain_state.snarked_ledger_hash
in
let open Checked in
let%bind () =
Fee_excess.(assert_equal_checked (var_of_t zero) txn_snark.fee_excess)
in
all
[ Frozen_ledger_hash.equal_var txn_snark.source (lh previous_state)
; Frozen_ledger_hash.equal_var txn_snark.target (lh new_state)
; Pending_coinbase.Stack.equal_var
txn_snark.pending_coinbase_stack_state.source
pending_coinbase_source_stack
; Pending_coinbase.Stack.equal_var
txn_snark.pending_coinbase_stack_state.target deleted_stack
; Token_id.Checked.equal txn_snark.next_available_token_before
( previous_state |> Protocol_state.blockchain_state
|> Blockchain_state.snarked_next_available_token )
; Token_id.Checked.equal txn_snark.next_available_token_after
( transition |> Snark_transition.blockchain_state
|> Blockchain_state.snarked_next_available_token )
]
>>= Boolean.all
in
let%bind nothing_changed =
let%bind next_available_token_didn't_change =
Token_id.Checked.equal txn_snark.next_available_token_after
txn_snark.next_available_token_before
in
Boolean.all
[ ledger_hash_didn't_change
; supply_increase_is_zero
; no_coinbases_popped
; next_available_token_didn't_change
]
in
let%bind correct_coinbase_status =
let new_root =
transition |> Snark_transition.blockchain_state
|> Blockchain_state.staged_ledger_hash
|> Staged_ledger_hash.pending_coinbase_hash_var
in
Pending_coinbase.Hash.equal_var new_pending_coinbase_hash new_root
in
let%bind () =
Boolean.Assert.any [ txn_snark_input_correct; nothing_changed ]
in
let transaction_snark_should_verifiy = Boolean.not nothing_changed in
let%bind result =
Boolean.all [ updated_consensus_state; correct_coinbase_status ]
in
let%map () =
as_prover
As_prover.(
Let_syntax.(
let%map txn_snark_input_correct =
read Boolean.typ txn_snark_input_correct
and nothing_changed = read Boolean.typ nothing_changed
and no_coinbases_popped = read Boolean.typ no_coinbases_popped
and updated_consensus_state =
read Boolean.typ updated_consensus_state
and correct_coinbase_status =
read Boolean.typ correct_coinbase_status
and result = read Boolean.typ result in
[%log trace]
"blockchain snark update success: $result = \
(transaction_snark_input_correct=$transaction_snark_input_correct \
∨ nothing_changed \
(no_coinbases_popped=$no_coinbases_popped)=$nothing_changed) \
∧ updated_consensus_state=$updated_consensus_state ∧ \
correct_coinbase_status=$correct_coinbase_status"
~metadata:
[ ( "transaction_snark_input_correct"
, `Bool txn_snark_input_correct )
; ("nothing_changed", `Bool nothing_changed)
; ("updated_consensus_state", `Bool updated_consensus_state)
; ("correct_coinbase_status", `Bool correct_coinbase_status)
; ("result", `Bool result)
; ("no_coinbases_popped", `Bool no_coinbases_popped)
]))
in
(transaction_snark_should_verifiy, result)
in
let txn_snark_should_verify =
match proof_level with
| Check | None ->
Boolean.false_
| Full ->
txn_snark_should_verify
in
let prev_should_verify =
match proof_level with
| Check | None ->
Boolean.false_
| Full ->
Boolean.not is_base_case
in
let%map () = Boolean.Assert.any [ is_base_case; success ] in
(prev_should_verify, txn_snark_should_verify)
Mina 数据结构
参考
https://docs.minaprotocol.com/en
https://github.com/MinaProtocol/mina
https://o1-labs.github.io/ocamlbyexample/basics-opam.html
https://docs.ocaml.pro/about.html
https://www.craigfe.io/operator-lookup/
https://mp.weixin.qq.com/s/sYe7fQSSy6Ix9xIYWMNWfw
https://mp.weixin.qq.com/s/mvh4gHaVDvdwIe157UTLZw
https://zkproof.org/2020/06/08/recursive-snarks/
https://github.com/ChainSafe/mina-rs/tree/main/protocol/test-fixtures/src/data
