-
Notifications
You must be signed in to change notification settings - Fork 526
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
Fix for recursion when max_proofs_verified = 1 #11698
Changes from all commits
742bda6
cd0495e
523dd52
5b1d23e
0c9ec0e
b102c93
225fd43
b67152a
38e73e8
47b1e7d
61fea2c
5654a4e
d202f9e
b2902c6
042735e
810728e
4dfe6da
0203539
9469443
f34bca4
95840f5
e8e8d2d
da3bc50
4866be1
b516d2c
304f757
72a2c1d
1e84d3b
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 |
---|---|---|
|
@@ -162,7 +162,7 @@ module Make_str (_ : Wire_types.Concrete) = struct | |
let (T (_proofs_verified, pi)) = HI.length xs in | ||
let module V = H2_1.To_vector (Int) in | ||
let v = V.f pi xs in | ||
Vector.extend_exn v max_proofs_verified 0 | ||
Vector.extend_front_exn v max_proofs_verified 0 | ||
end) | ||
in | ||
let module V = H2_1.To_vector (Vec) in | ||
|
@@ -194,6 +194,14 @@ module Make_str (_ : Wire_types.Concrete) = struct | |
local_max_proofs_verifieds | ||
H1.T(Proof_.Messages_for_next_proof_over_same_field.Wrap).t ) = | ||
let dummy_chals = Dummy.Ipa.Wrap.challenges in | ||
let rev_magic : | ||
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. We should fix the iterator below and remove this. Best not to lie to the typechecker! |
||
type ms. | ||
(* This type is wrong actually, the "ms" type-level list should be | ||
reversed but there's no way to do that. *) | ||
ms H1.T(Proof_.Messages_for_next_proof_over_same_field.Wrap).t | ||
-> ms H1.T(Proof_.Messages_for_next_proof_over_same_field.Wrap).t = | ||
fun xs -> Obj.magic (List.rev (Obj.magic xs)) | ||
in | ||
let rec go : | ||
type len ms ns. | ||
ms H1.T(Nat).t | ||
|
@@ -215,14 +223,17 @@ module Make_str (_ : Wire_types.Concrete) = struct | |
let messages_for_next_wrap_proof = | ||
{ messages_for_next_wrap_proof with | ||
old_bulletproof_challenges = | ||
Vector.extend_exn | ||
Vector.extend_front_exn | ||
messages_for_next_wrap_proof.old_bulletproof_challenges m | ||
dummy_chals | ||
} | ||
in | ||
messages_for_next_wrap_proof :: go maxes messages_for_next_wrap_proofs | ||
in | ||
go M.maxes messages_for_next_wrap_proofs | ||
rev_magic | ||
(go | ||
(Obj.magic (List.rev (Obj.magic M.maxes))) | ||
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. Likewise |
||
(rev_magic messages_for_next_wrap_proofs) ) | ||
|
||
module Verification_key = struct | ||
include Verification_key | ||
|
@@ -333,7 +344,9 @@ module Make_str (_ : Wire_types.Concrete) = struct | |
= | ||
fun rule -> | ||
let (T (_, l)) = HT.length rule.prevs in | ||
Vector.extend_exn (V.f l (M.f rule.prevs)) Max_proofs_verified.n 0 | ||
Vector.extend_front_exn | ||
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. It's a pity that we had to reverse all of these; probably there was just one place that was wrong before. (No need to change now though, since this works as written.) |
||
(V.f l (M.f rule.prevs)) | ||
Max_proofs_verified.n 0 | ||
end) | ||
in | ||
let module V = H4.To_vector (Local_max_proofs_verifieds) in | ||
|
@@ -1961,7 +1974,7 @@ module Make_str (_ : Wire_types.Concrete) = struct | |
(a, b, c, d) IR.t -> Local_max_proofs_verifieds.t = | ||
fun rule -> | ||
let (T (_, l)) = HT.length rule.prevs in | ||
Vector.extend_exn | ||
Vector.extend_front_exn | ||
(V.f l (M.f rule.prevs)) | ||
Max_proofs_verified.n 0 | ||
end) | ||
|
@@ -2352,7 +2365,7 @@ module Make_str (_ : Wire_types.Concrete) = struct | |
in | ||
O.create pairing_vk | ||
Vector.( | ||
map2 (Vector.trim sgs lte) prev_challenges | ||
map2 (Vector.trim_front sgs lte) prev_challenges | ||
~f:(fun commitment cs -> | ||
{ Tick.Proof.Challenge_polynomial.commitment | ||
; challenges = Vector.to_array cs | ||
|
@@ -2597,7 +2610,7 @@ module Make_str (_ : Wire_types.Concrete) = struct | |
~auxiliary:auxiliary_inputs pk | ||
~message: | ||
( Vector.map2 | ||
(Vector.extend_exn | ||
(Vector.extend_front_exn | ||
prev_statement.proof_state | ||
.messages_for_next_step_proof | ||
.challenge_polynomial_commitments | ||
|
@@ -2886,7 +2899,7 @@ module Make_str (_ : Wire_types.Concrete) = struct | |
(a, b, c, d) IR.t -> Local_max_proofs_verifieds.t = | ||
fun rule -> | ||
let (T (_, l)) = HT.length rule.prevs in | ||
Vector.extend_exn | ||
Vector.extend_front_exn | ||
(V.f l (M.f rule.prevs)) | ||
Max_proofs_verified.n 0 | ||
end) | ||
|
@@ -3277,7 +3290,7 @@ module Make_str (_ : Wire_types.Concrete) = struct | |
in | ||
O.create pairing_vk | ||
Vector.( | ||
map2 (Vector.trim sgs lte) prev_challenges | ||
map2 (Vector.trim_front sgs lte) prev_challenges | ||
~f:(fun commitment cs -> | ||
{ Tick.Proof.Challenge_polynomial.commitment | ||
; challenges = Vector.to_array cs | ||
|
@@ -3488,7 +3501,7 @@ module Make_str (_ : Wire_types.Concrete) = struct | |
~auxiliary:auxiliary_inputs pk | ||
~message: | ||
( Vector.map2 | ||
(Vector.extend_exn | ||
(Vector.extend_front_exn | ||
prev_statement.proof_state | ||
.messages_for_next_step_proof | ||
.challenge_polynomial_commitments | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -67,7 +67,7 @@ let verify_one | |
hash_messages_for_next_step_proof ~widths:d.proofs_verifieds | ||
~max_width:(Nat.Add.n d.max_proofs_verified) | ||
~proofs_verified_mask: | ||
(Vector.trim branch_data.proofs_verified_mask | ||
(Vector.trim_front branch_data.proofs_verified_mask | ||
(Nat.lte_exn | ||
(Vector.length prev_challenge_polynomial_commitments) | ||
Nat.N2.n ) ) | ||
|
@@ -130,6 +130,7 @@ let step_main : | |
and type statement = a_value | ||
and type prev_values = prev_values | ||
and type max_proofs_verified = max_proofs_verified | ||
and type proofs_verified = proofs_verified | ||
and type return_value = ret_value | ||
and type auxiliary_value = auxiliary_value ) | ||
-> (module Nat.Add.Intf with type n = max_proofs_verified) | ||
|
@@ -345,14 +346,15 @@ let step_main : | |
and prevs = | ||
exists (Prev_typ.f prev_proof_typs) ~request:(fun () -> | ||
Req.Proof_with_datas ) | ||
and unfinalized_proofs = | ||
and unfinalized_proofs_unextended = | ||
mrmr1993 marked this conversation as resolved.
Show resolved
Hide resolved
|
||
exists | ||
(Vector.typ' | ||
(Vector.map | ||
~f:(fun uses_lookup -> | ||
Unfinalized.typ ~wrap_rounds:Backend.Tock.Rounds.n | ||
~uses_lookup ) | ||
(Vector.extend lookup_usage lte Max_proofs_verified.n No) ) ) | ||
lookup_usage | ||
(* Vector.extend lookup_usage lte Max_proofs_verified.n No *) ) ) | ||
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. Delete |
||
~request:(fun () -> Req.Unfinalized_proofs) | ||
and messages_for_next_wrap_proof = | ||
exists (Vector.typ Digest.typ Max_proofs_verified.n) | ||
|
@@ -419,10 +421,10 @@ let step_main : | |
with_label "messages_for_next_wrap_proofs" (fun () -> | ||
let module V = H1.Of_vector (Digest) in | ||
V.f proofs_verified | ||
(Vector.trim messages_for_next_wrap_proof lte) ) | ||
(Vector.trim_front messages_for_next_wrap_proof lte) ) | ||
and unfinalized_proofs = | ||
let module H = H1.Of_vector (Unfinalized) in | ||
H.f proofs_verified (Vector.trim unfinalized_proofs lte) | ||
H.f proofs_verified unfinalized_proofs_unextended | ||
and datas = | ||
let self_data : | ||
( var | ||
|
@@ -513,6 +515,10 @@ let step_main : | |
bulletproof_challenges | ||
} ) | ||
in | ||
let unfinalized_proofs = | ||
Vector.extend_front unfinalized_proofs_unextended lte | ||
Max_proofs_verified.n (Unfinalized.dummy ()) | ||
in | ||
( { Types.Step.Statement.proof_state = | ||
{ unfinalized_proofs; messages_for_next_step_proof } | ||
; messages_for_next_wrap_proof | ||
|
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -106,3 +106,10 @@ let typ ~wrap_rounds ~uses_lookup : (t, Constant.t) Typ.t = | |
(Shifted_value.typ Other_field.typ) | ||
~assert_16_bits:(Step_verifier.assert_n_bits ~n:16) | ||
~zero:Common.Lookup_parameters.tick_zero ~uses_lookup | ||
|
||
let dummy () : t = | ||
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. Nit: memo-ize? |
||
let (Typ { var_of_fields; value_to_fields; _ }) = | ||
typ ~wrap_rounds:Backend.Tock.Rounds.n ~uses_lookup:No | ||
in | ||
let xs, aux = value_to_fields (Lazy.force Constant.dummy) in | ||
var_of_fields (Array.map ~f:Field.constant xs, aux) |
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.
We should revert this, since it's fairly heavy, and only for debugging.