Skip to content
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] Dynamic verifier doesn't require the order of AIRs #465

Merged
merged 5 commits into from
Sep 25, 2024

Conversation

nyunyunyunyu
Copy link
Contributor

Closes INT-2104

@nyunyunyunyu nyunyunyunyu added the run-benchmark triggers benchmark workflows on the pr label Sep 24, 2024
Copy link

linear bot commented Sep 24, 2024

INT-2104 Add a mapping between trace -> air idx in verifier program

The order of the vkey is still going to be determined at compile time. That gives each AIR an air_idx.

Since the traces of AIRs need to be sorted outside of th program, the program will need another input of air_idx that maps the index of trace to the air index.

For now we will do a bitmap check that each AIR is used in a trace at most once to ensure uniqueness guarantees (e.g., of Audit chip)

This comment has been minimized.

This comment has been minimized.

@nyunyunyunyu nyunyunyunyu force-pushed the fix/recursion-no-order-requir branch from 926a4d0 to 549762a Compare September 24, 2024 21:06
@nyunyunyunyu nyunyunyunyu force-pushed the fix/recursion-no-order-requir branch from 549762a to 743c50c Compare September 24, 2024 21:18

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

Copy link
Contributor

@jonathanpwang jonathanpwang left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, some comments to add more clarification comments.

Summary

There are two ways to support having non-deterministic trace height ordering in verifier.

  1. Impose assumptions on the format of the proof. For example the prover must have already sorted traces in descending order before it did MMCS commitments.
  2. Supply a permutation of the sorted indices as hint and use it to lookup the correct ordering when necessary.

(2) is more general as it allows verifying any proof in plonky3 without adding conditions to the prover. This PR implements both 1+2, where the implementation takes an optional flag to distinguish when the input is already sorted versus when permutation lookup must be done in circuit.

It currently does not support unused Air traces compared to the Air list in the vkey.

There is also an assumption currently that each AIR has exactly one partition of the partitioned main trace that is commited together in a big commitment. For each AIR any other partition, if it exists, is committed in a separate standalone commitment.

Co-authored-by: Jonathan Wang <[email protected]>

This comment has been minimized.

This comment has been minimized.

This comment has been minimized.

Copy link

vm_verify_fibair

stark_prove_excluding_trace_time_ms total_cells total_cells_used trace_gen_time_ms verify_program_compile_ms
7822.0 (-0.8%) 66134036 30479046 (+0.5%) 1666.0 (-2.1%) 51.0 (+45.7%)
chip_name rows_used
ByteXor 65536
Core 321095 (+0.4%)
FieldArithmetic 165069 (+0.6%)
FieldExtension 7914
Memory 107372 (+0.2%)
Poseidon2 3309
Program 54786 (+45.8%)
RangeChecker 131072
opcode cells_used frequency
FADD 4247464 (+0.7%) 134879 (+0.7%)
BNE 4897555 75347
STOREW 5660008 (+0.1%) 73927 (+0.2%)
LOADW 3267591 (+0.3%) 49128 (+0.2%)
LOADW2 2533721 (+2.4%) 38928 (+2.4%)
SHINTW 2791656 (+0.0%) 33234 (+0.0%)
STOREW2 1684008 (+1.0%) 21546 (+0.9%)
FMUL 702778 (-0.1%) 20720 (+0.0%)
JAL 834554 12839
FSUB 355816 (-0.2%) 9467
HINT_INPUT 310050 (+0.0%) 4770 (+0.0%)
CT_END 254865 3921
CT_START 254865 3921
BBE4MUL 258120 (-0.1%) 3759
BEQ 222885 3429
COMP_POS2 1344356 2678
FE4ADD 115016 (-0.6%) 1678
BBE4DIV 84328 1239
FE4SUB 84336 1238
PERM_POS2 316762 631
HINT_BITS 6760 104
FDIV 93 3
TERMINATE 65 1
dsl_ir frequency
For 116132 (-0.9%)
StoreHintWord 58474 (+0.0%)
AddVI 40507 (+2.4%)
Alloc 39111 (+0.0%)
StoreE 37932
LoadV 30939 (+2.7%)
LoadE 19400
LoadF 17279 (+1.2%)
IfEqI 15113 (+4.3%)
StoreV 14061 (+1.5%)
ImmV 13133 (+0.8%)
StoreF 10962 (+1.9%)
ImmF 7243
SubEF 6612
AddEI 6244
AssertEqF 5048
HintInputVec 4770 (+0.0%)
CycleTrackerEnd 3921
CycleTrackerStart 3921
SubVI 3900
MulE 3726
AssertEqV 3640
SubV 3502
AddFI 3309 (+6.7%)
MulVI 3300
MulV 3224
IfNe 2817
MulF 2682
Poseidon2CompressBabyBear 2678
AddV 2274
ImmE 2068
AddE 1678
MulEF 1656
DivE 1238
SubE 1238
IfEq 743
Poseidon2PermuteBabyBear 631
IfNeI 619
AddEFFI 524
AssertEqE 416
SubVIN 412
MulEI 165
HintBitsF 104
AssertEqVI 16
SubEI 8
DivEIN 5
AssertEqEI 4
DivFIN 3
Halt 1
MulFI 1
air_name cells constraints interactions main_cols perm_cols prep_cols quotient_deg rows
CoreAir 44564480 111 (-0.9%) 19 65 20 0 8 524288
ProgramAir 589824 4 1 1 8 9 1 65536
FieldArithmeticAir 12320768 23 15 31 16 0 8 262144
FieldExtensionArithmeticAir 884736 38 51 68 40 0 8 8192
Poseidon2VmAir 2465792 419 144 502 100 0 8 4096
XorLookupAir 589824 4 1 1 8 3 1 65536
MemoryAuditAir 3538944 19 6 19 8 0 8 131072
VariableRangeCheckerAir 1179648 4 1 1 8 2 1 131072
VmConnectorAir 20 4 2 2 8 1 2 2

Flamegraphs: link
Commit: 3b64bf9
AWS Instance Type: r7g.8xlarge
Benchmark Workflow

Copy link

tiny_e2e

group stark_prove_excluding_trace_time_ms total_cells total_cells_used trace_gen_time_ms
fibonacci_program_inner 472.0 (+2.2%) 1782300 200526 0.0
group chip_name rows_used
fibonacci_program_inner ByteXor 65536
fibonacci_program_inner Core 6
fibonacci_program_inner FieldArithmetic 90
fibonacci_program_inner Memory 35
fibonacci_program_inner Program 97
fibonacci_program_inner RangeChecker 131072
group opcode cells_used frequency
fibonacci_program_inner FADD 3360 90
fibonacci_program_inner STOREW 320 4
fibonacci_program_inner JAL 80 1
fibonacci_program_inner TERMINATE 61 1
group dsl_ir frequency
fibonacci_program_inner AddFI 60
fibonacci_program_inner AddF 30
fibonacci_program_inner ImmF 2
fibonacci_program_inner Halt 1
group air_name cells constraints interactions main_cols perm_cols prep_cols quotient_deg rows
fibonacci_program_inner CoreAir 840 113 (-0.9%) 19 61 44 0 2 8
fibonacci_program_inner ProgramAir 1152 4 1 1 8 9 1 128
fibonacci_program_inner FieldArithmeticAir 8576 28 15 31 36 0 2 128
fibonacci_program_inner XorLookupAir 589824 4 1 1 8 3 1 65536
fibonacci_program_inner MemoryAuditAir 2240 21 6 19 16 0 2 64
fibonacci_program_inner VariableRangeCheckerAir 1179648 4 1 1 8 2 1 131072
fibonacci_program_inner VmConnectorAir 20 4 2 2 8 1 2 2

Flamegraphs: link
Commit: 3b64bf9
AWS Instance Type: r7g.16xlarge
Benchmark Workflow

Copy link

small_e2e

group stark_prove_excluding_trace_time_ms total_cells total_cells_used trace_gen_time_ms verify_program_compile_ms
bench_program_inner 1224.0 (+1.4%) 1997712 287089 2.0
inner_verifier 111482.0 (-1.3%) 1191182356 633586847 (-0.0%) 34023.0 (+1.1%) 44635.0 (-4.8%)
group chip_name rows_used
bench_program_inner ByteXor 65536
bench_program_inner Core 28
bench_program_inner FieldArithmetic 13
bench_program_inner FieldExtension 1
bench_program_inner Keccak256 24
bench_program_inner Memory 59
bench_program_inner Program 37
bench_program_inner RangeChecker 131072
inner_verifier ByteXor 65536
inner_verifier Core 6484960 (-0.0%)
inner_verifier FieldArithmetic 2529110 (+0.1%)
inner_verifier FieldExtension 1492707 (-0.0%)
inner_verifier Memory 846770 (+0.2%)
inner_verifier Poseidon2 31034
inner_verifier Program 293655 (+4.1%)
inner_verifier RangeChecker 131072
group opcode cells_used frequency
bench_program_inner STOREW 1261 16
bench_program_inner FADD 398 11
bench_program_inner BNE 305 5
bench_program_inner FMUL 62 2
bench_program_inner JAL 141 2
bench_program_inner LOADW 160 2
bench_program_inner STOREW2 160 2
bench_program_inner FE4ADD 144 1
bench_program_inner KECCAK256 87752 1
bench_program_inner TERMINATE 61 1
inner_verifier LOADW 146629643 (+0.0%) 2237432 (+0.0%)
inner_verifier LOADW2 132528919 (-0.2%) 2038836 (-0.2%)
inner_verifier FADD 55784801 (+0.1%) 1750874 (+0.1%)
inner_verifier BNE 72455435 (-0.0%) 1114699 (-0.0%)
inner_verifier BBE4MUL 52045516 (-0.0%) 735011 (-0.0%)
inner_verifier FSUB 22410617 (-0.0%) 722423
inner_verifier FE4ADD 29181252 (-0.0%) 389264 (-0.0%)
inner_verifier BBE4DIV 24024280 353201
inner_verifier SHINTW 26291916 (+0.0%) 312999 (+0.0%)
inner_verifier STOREW2 14896389 (+0.5%) 220071 (+0.4%)
inner_verifier CT_END 11968775 184135
inner_verifier CT_START 11968775 184135
inner_verifier STOREW 10142136 (+0.4%) 142435 (+0.4%)
inner_verifier FMUL 1817140 (-0.0%) 55662 (+0.0%)
inner_verifier JAL 1989604 (+1.6%) 30609 (+1.6%)
inner_verifier PERM_POS2 11470700 22850
inner_verifier FE4SUB 2100240 (-0.0%) 15231 (-0.0%)
inner_verifier HINT_INPUT 696085 (+0.0%) 10709 (+0.0%)
inner_verifier BEQ 576810 8874
inner_verifier COMP_POS2 4108368 8184
inner_verifier FDIV 7493 151
inner_verifier HINT_BITS 1625 25
inner_verifier TERMINATE 65 1
group dsl_ir frequency
bench_program_inner ImmE 8
bench_program_inner For 7
bench_program_inner AddVI 6
bench_program_inner Alloc 6
bench_program_inner ImmV 3
bench_program_inner IfEqI 2
bench_program_inner ImmF 2
bench_program_inner StoreV 2
bench_program_inner AddE 1
bench_program_inner AddF 1
bench_program_inner Halt 1
bench_program_inner Keccak256 1
inner_verifier SubEF 2821704
inner_verifier For 1819266 (-0.2%)
inner_verifier LoadE 1498380
inner_verifier MulE 727856 (-0.0%)
inner_verifier StoreHintWord 614514 (+0.0%)
inner_verifier LoadF 552461 (-0.3%)
inner_verifier AddVI 439705 (+0.4%)
inner_verifier AddE 389264 (-0.0%)
inner_verifier DivE 353130
inner_verifier IfEqI 213021 (+0.9%)
inner_verifier StoreF 194952 (+0.2%)
inner_verifier CycleTrackerEnd 184135
inner_verifier CycleTrackerStart 184135
inner_verifier LoadV 81129 (-2.6%)
inner_verifier AddEI 80892 (-0.0%)
inner_verifier Alloc 69733 (+0.0%)
inner_verifier MulEI 35775
inner_verifier ImmV 32342 (+0.4%)
inner_verifier StoreV 28328 (+4.4%)
inner_verifier StoreE 25140
inner_verifier MulF 23762
inner_verifier Poseidon2PermuteBabyBear 22850
inner_verifier ImmE 17384 (-0.0%)
inner_verifier ImmF 15360
inner_verifier SubE 15231 (-0.0%)
inner_verifier SubV 15168
inner_verifier AddFI 13717 (+3.3%)
inner_verifier HintInputVec 10709 (+0.0%)
inner_verifier MulVI 9367
inner_verifier Poseidon2CompressBabyBear 8184
inner_verifier IfNe 7886
inner_verifier AddV 6728 (+0.1%)
inner_verifier IfEq 6140
inner_verifier AssertEqF 4633
inner_verifier MulEFI 2660
inner_verifier MulEF 2200
inner_verifier SubVI 1421
inner_verifier AssertEqV 1262
inner_verifier SubEFI 1248
inner_verifier IfNeI 1009
inner_verifier AddEFI 960
inner_verifier NegE 784
inner_verifier MulV 775
inner_verifier AddEFFI 696
inner_verifier SubEI 568
inner_verifier SubVIN 408
inner_verifier DivEIN 355
inner_verifier AssertEqVI 159
inner_verifier DivFIN 151
inner_verifier AssertEqE 132
inner_verifier HintBitsF 25
inner_verifier MulFI 9
inner_verifier AssertEqEI 4
inner_verifier Halt 1
group air_name cells constraints interactions main_cols perm_cols prep_cols quotient_deg rows
bench_program_inner CoreAir 2976 110 (-0.9%) 19 61 32 0 4 32
bench_program_inner ProgramAir 576 4 1 1 8 9 1 64
bench_program_inner FieldArithmeticAir 880 25 15 31 24 0 4 16
bench_program_inner FieldExtensionArithmeticAir 140 46 51 68 72 0 4 1
bench_program_inner KeccakVmAir 221664 2866 823 3631 3296 0 4 32
bench_program_inner XorLookupAir 589824 4 1 1 8 3 1 65536
bench_program_inner MemoryAuditAir 1984 20 6 19 12 0 4 64
bench_program_inner VariableRangeCheckerAir 1179648 4 1 1 8 2 1 131072
bench_program_inner VmConnectorAir 20 4 2 2 8 1 2 2
inner_verifier CoreAir 713031680 111 (-0.9%) 19 65 20 0 8 8388608
inner_verifier ProgramAir 4718592 4 1 1 8 9 1 524288
inner_verifier FieldArithmeticAir 197132288 23 15 31 16 0 8 4194304
inner_verifier FieldExtensionArithmeticAir 226492416 38 51 68 40 0 8 2097152
inner_verifier Poseidon2VmAir 19726336 419 144 502 100 0 8 32768
inner_verifier XorLookupAir 589824 4 1 1 8 3 1 65536
inner_verifier MemoryAuditAir 28311552 19 6 19 8 0 8 1048576
inner_verifier VariableRangeCheckerAir 1179648 4 1 1 8 2 1 131072
inner_verifier VmConnectorAir 20 4 2 2 8 1 2 2

Flamegraphs: link
Commit: 3b64bf9
AWS Instance Type: r7g.16xlarge
Benchmark Workflow

@nyunyunyunyu
Copy link
Contributor Author

LGTM, some comments to add more clarification comments.

Summary

There are two ways to support having non-deterministic trace height ordering in verifier.

  1. Impose assumptions on the format of the proof. For example the prover must have already sorted traces in descending order before it did MMCS commitments.
  2. Supply a permutation of the sorted indices as hint and use it to lookup the correct ordering when necessary.

(2) is more general as it allows verifying any proof in plonky3 without adding conditions to the prover. This PR implements both 1+2, where the implementation takes an optional flag to distinguish when the input is already sorted versus when permutation lookup must be done in circuit.

It currently does not support unused Air traces compared to the Air list in the vkey.

There is also an assumption currently that each AIR has exactly one partition of the partitioned main trace that is commited together in a big commitment. For each AIR any other partition, if it exists, is committed in a separate standalone commitment.

To clarify: This order thing is a requirement from FieldMerkleTreeMMCS implementation details and the prover shouldn't know it.

@nyunyunyunyu nyunyunyunyu merged commit 83233f4 into main Sep 25, 2024
18 checks passed
@nyunyunyunyu nyunyunyunyu deleted the fix/recursion-no-order-requir branch September 25, 2024 17:39
luffykai pushed a commit that referenced this pull request Dec 13, 2024
* Dynamic verifier doesn't require the order of AIRs

* Fix quotient matrices permutation

* Fix static verifier

* Fix comments

Co-authored-by: Jonathan Wang <[email protected]>

* Fix comments

---------

Co-authored-by: Jonathan Wang <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
run-benchmark triggers benchmark workflows on the pr
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants