-
Notifications
You must be signed in to change notification settings - Fork 548
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Cosmetics/Refactoring #14870
Cosmetics/Refactoring #14870
Changes from 6 commits
2791ef9
d79fc01
410d5da
7f4c46e
d838df3
ad151ac
580cccf
e6337f1
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -87,8 +87,8 @@ module Proof = Plonk_dlog_proof.Make (struct | |
let batch_verify vks ts = | ||
Promise.run_in_thread (fun () -> batch_verify vks ts) | ||
|
||
let create_aux ~f:create (pk : Keypair.t) ~primary ~auxiliary ~prev_chals | ||
~prev_comms = | ||
let create_aux ~f:backend_create (pk : Keypair.t) ~primary ~auxiliary | ||
~prev_chals ~prev_comms = | ||
(* external values contains [1, primary..., auxiliary ] *) | ||
let external_values i = | ||
let open Field.Vector in | ||
|
@@ -111,17 +111,19 @@ module Proof = Plonk_dlog_proof.Make (struct | |
done ; | ||
witness ) | ||
in | ||
create pk.index witness_cols runtime_tables prev_chals prev_comms | ||
backend_create pk.index witness_cols runtime_tables prev_chals prev_comms | ||
|
||
let create_async (pk : Keypair.t) ~primary ~auxiliary ~prev_chals | ||
~prev_comms = | ||
create_aux pk ~primary ~auxiliary ~prev_chals ~prev_comms | ||
~f:(fun pk auxiliary_input runtime_tables prev_challenges prev_sgs -> | ||
~f:(fun index witness runtime_tables prev_chals prev_sgs -> | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I imagine the prev_chals change is related to homogeneity, right? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Yes, it's just more homogenous w.r.t. the other call in the same file. |
||
Promise.run_in_thread (fun () -> | ||
create pk auxiliary_input runtime_tables prev_challenges prev_sgs ) ) | ||
Kimchi_bindings.Protocol.Proof.Fq.create index witness | ||
runtime_tables prev_chals prev_sgs ) ) | ||
|
||
let create (pk : Keypair.t) ~primary ~auxiliary ~prev_chals ~prev_comms = | ||
create_aux pk ~primary ~auxiliary ~prev_chals ~prev_comms ~f:create | ||
create_aux pk ~primary ~auxiliary ~prev_chals ~prev_comms | ||
~f:Kimchi_bindings.Protocol.Proof.Fq.create | ||
end | ||
|
||
module Verifier_index = Kimchi_bindings.Protocol.VerifierIndex.Fq | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -2,7 +2,6 @@ open Pickles_types | |
open Hlist | ||
open Import | ||
open Impls.Step | ||
open Step_verifier | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Wow. Vicious ;-) Some people will not like that. I'm in favor, though There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm very much a fan of explicit imports, everything else is often really unreadable without some external tooling like IDE... |
||
module B = Inductive_rule.B | ||
|
||
(* Converts from the one hot vector representation of a number | ||
|
@@ -16,6 +15,7 @@ module B = Inductive_rule.B | |
let _one_hot_vector_to_num (type n) (v : n Per_proof_witness.One_hot_vector.t) : | ||
Field.t = | ||
let n = Vector.length (v :> (Boolean.var, n) Vector.t) in | ||
let open Step_verifier in | ||
Pseudo.choose (v, Vector.init n ~f:Field.of_int) ~f:Fn.id | ||
Comment on lines
15
to
19
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Could have removed the function altogether, maybe ;-) |
||
|
||
let verify_one ~srs | ||
|
@@ -28,8 +28,8 @@ let verify_one ~srs | |
} : | ||
_ Per_proof_witness.t ) (d : _ Types_map.For_step.t) | ||
(messages_for_next_wrap_proof : Digest.t) (unfinalized : Unfinalized.t) | ||
(should_verify : B.t) : _ Vector.t * B.t = | ||
Boolean.Assert.( = ) unfinalized.should_finalize should_verify ; | ||
(must_verify : B.t) : _ Vector.t * B.t = | ||
Boolean.Assert.( = ) unfinalized.should_finalize must_verify ; | ||
let deferred_values = proof_state.deferred_values in | ||
let finalized, chals = | ||
with_label __LOC__ (fun () -> | ||
|
@@ -41,9 +41,9 @@ let verify_one ~srs | |
sponge | ||
in | ||
(* TODO: Refactor args into an "unfinalized proof" struct *) | ||
finalize_other_proof d.max_proofs_verified ~step_domains:d.step_domains | ||
~zk_rows:d.zk_rows ~sponge ~prev_challenges deferred_values | ||
prev_proof_evals ) | ||
Step_verifier.finalize_other_proof d.max_proofs_verified | ||
~step_domains:d.step_domains ~zk_rows:d.zk_rows ~sponge | ||
~prev_challenges deferred_values prev_proof_evals ) | ||
in | ||
let branch_data = deferred_values.branch_data in | ||
let sponge_after_index, hash_messages_for_next_step_proof = | ||
|
@@ -53,7 +53,8 @@ let verify_one ~srs | |
in | ||
let sponge_after_index, hash_messages_for_next_step_proof = | ||
(* TODO: Don't rehash when it's not necessary *) | ||
hash_messages_for_next_step_proof_opt ~index:d.wrap_key to_field_elements | ||
Step_verifier.hash_messages_for_next_step_proof_opt ~index:d.wrap_key | ||
to_field_elements | ||
in | ||
(sponge_after_index, unstage hash_messages_for_next_step_proof) | ||
in | ||
|
@@ -87,7 +88,7 @@ let verify_one ~srs | |
statement *) | ||
let verified = | ||
with_label __LOC__ (fun () -> | ||
verify ~srs | ||
Step_verifier.verify ~srs | ||
~feature_flags:(Plonk_types.Features.of_full d.feature_flags) | ||
~lookup_parameters: | ||
{ use = d.feature_flags.uses_lookups | ||
|
@@ -104,22 +105,21 @@ let verify_one ~srs | |
} | ||
} | ||
~proofs_verified:d.max_proofs_verified ~wrap_domain:d.wrap_domain | ||
~is_base_case:(Boolean.not should_verify) | ||
~sponge_after_index ~sg_old:prev_challenge_polynomial_commitments | ||
~proof:wrap_proof ~wrap_verification_key:d.wrap_key statement | ||
unfinalized ) | ||
~is_base_case:(Boolean.not must_verify) ~sponge_after_index | ||
~sg_old:prev_challenge_polynomial_commitments ~proof:wrap_proof | ||
~wrap_verification_key:d.wrap_key statement unfinalized ) | ||
in | ||
if debug then | ||
as_prover | ||
As_prover.( | ||
fun () -> | ||
let finalized = read Boolean.typ finalized in | ||
let verified = read Boolean.typ verified in | ||
let should_verify = read Boolean.typ should_verify in | ||
let must_verify = read Boolean.typ must_verify in | ||
printf "finalized: %b\n%!" finalized ; | ||
printf "verified: %b\n%!" verified ; | ||
printf "should_verify: %b\n\n%!" should_verify) ; | ||
(chals, Boolean.(verified &&& finalized ||| not should_verify)) | ||
printf "must_verify: %b\n\n%!" must_verify) ; | ||
(chals, Boolean.(verified &&& finalized ||| not must_verify)) | ||
|
||
(* The SNARK function corresponding to the input inductive rule. *) | ||
let step_main : | ||
|
@@ -349,7 +349,7 @@ let step_main : | |
exists | ||
~request:(fun () -> Req.Wrap_index) | ||
(Plonk_verification_key_evals.typ | ||
(Typ.array ~length:num_chunks Inner_curve.typ) ) | ||
(Typ.array ~length:num_chunks Step_verifier.Inner_curve.typ) ) | ||
and prevs = | ||
exists (Prev_typ.f prev_proof_typs) ~request:(fun () -> | ||
Req.Proof_with_datas ) | ||
|
@@ -369,7 +369,7 @@ let step_main : | |
(Vector.typ (Typ.Internal.ref ()) (Length.to_nat proofs_verified)) | ||
~request:(fun () -> Req.Wrap_domain_indices) | ||
in | ||
let prevs = | ||
let proof_witnesses = | ||
(* Inject the app-state values into the per-proof witnesses. *) | ||
let rec go : | ||
type vars ns1 ns2. | ||
|
@@ -402,10 +402,10 @@ let step_main : | |
, n ) | ||
Vector.t | ||
-> (_, n) Vector.t * B.t list = | ||
fun proofs datas messages_for_next_wrap_proofs unfinalizeds stmts | ||
pi ~actual_wrap_domains -> | ||
fun proof_witnesses datas messages_for_next_wrap_proofs | ||
unfinalizeds stmts pi ~actual_wrap_domains -> | ||
match | ||
( proofs | ||
( proof_witnesses | ||
, datas | ||
, messages_for_next_wrap_proofs | ||
, unfinalizeds | ||
|
@@ -415,12 +415,12 @@ let step_main : | |
with | ||
| [], [], [], [], [], Z, [] -> | ||
([], []) | ||
| ( p :: proofs | ||
| ( pw :: proof_witnesses | ||
, d :: datas | ||
, messages_for_next_wrap_proof | ||
:: messages_for_next_wrap_proofs | ||
, unfinalized :: unfinalizeds | ||
, { proof_must_verify = should_verify; _ } :: stmts | ||
, { proof_must_verify = must_verify; _ } :: stmts | ||
, S pi | ||
, actual_wrap_domain :: actual_wrap_domains ) -> | ||
let () = | ||
|
@@ -456,12 +456,12 @@ let step_main : | |
() | ||
in | ||
let chals, v = | ||
verify_one ~srs p d messages_for_next_wrap_proof | ||
unfinalized should_verify | ||
verify_one ~srs pw d messages_for_next_wrap_proof | ||
unfinalized must_verify | ||
in | ||
let chalss, vs = | ||
go proofs datas messages_for_next_wrap_proofs unfinalizeds | ||
stmts pi ~actual_wrap_domains | ||
go proof_witnesses datas messages_for_next_wrap_proofs | ||
unfinalizeds stmts pi ~actual_wrap_domains | ||
in | ||
(chals :: chalss, v :: vs) | ||
in | ||
|
@@ -518,26 +518,28 @@ let step_main : | |
in | ||
M.f rule.prevs | ||
in | ||
go prevs datas messages_for_next_wrap_proofs unfinalized_proofs | ||
previous_proof_statements proofs_verified ~actual_wrap_domains | ||
go proof_witnesses datas messages_for_next_wrap_proofs | ||
unfinalized_proofs previous_proof_statements proofs_verified | ||
~actual_wrap_domains | ||
in | ||
Boolean.Assert.all vs ; chalss ) | ||
in | ||
[%log internal] "Step_compute_bulletproof_challenges_done" ; | ||
let messages_for_next_step_proof = | ||
let challenge_polynomial_commitments = | ||
let module M = | ||
H3.Map (Per_proof_witness) (E03 (Inner_curve)) | ||
H3.Map (Per_proof_witness) (E03 (Step_verifier.Inner_curve)) | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This here actually helps. We have so many |
||
(struct | ||
let f : | ||
type a b c. (a, b, c) Per_proof_witness.t -> Inner_curve.t | ||
= | ||
type a b c. | ||
(a, b, c) Per_proof_witness.t | ||
-> Step_verifier.Inner_curve.t = | ||
fun acc -> | ||
acc.wrap_proof.opening.challenge_polynomial_commitment | ||
end) | ||
in | ||
let module V = H3.To_vector (Inner_curve) in | ||
V.f proofs_verified (M.f prevs) | ||
let module V = H3.To_vector (Step_verifier.Inner_curve) in | ||
V.f proofs_verified (M.f proof_witnesses) | ||
in | ||
with_label "hash_messages_for_next_step_proof" (fun () -> | ||
let hash_messages_for_next_step_proof = | ||
|
@@ -546,8 +548,8 @@ let step_main : | |
fun x -> fst (typ.var_to_fields x) | ||
in | ||
unstage | ||
(hash_messages_for_next_step_proof ~index:dlog_plonk_index | ||
to_field_elements ) | ||
(Step_verifier.hash_messages_for_next_step_proof | ||
~index:dlog_plonk_index to_field_elements ) | ||
in | ||
let (app_state : var) = | ||
match public_input with | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Good catch
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think it might need to depend on the concrete type of building one's doing, but that's a task for the future.