Тема 7: Binius: fast SNARK proofs over binary field extensions

Binius — новый SNARK-протокол, оптимизированный для работы с бинарными полями. Он разработан для повышения производительности доказательств за счёт эффективных вычислений на уровне битов, что делает его более аппаратно-оптимизированным и производительным по сравнению с традиционными SNARK/STARK-системами.

Алексей Карасев, исследователь криптографии и DeFi, преподаватель кафедры Блокчейн в МФТИ

Transcript

1. Aleksei Karasev Blockchain department, MIPT karasev.alexey@gmail.com Binius Blazingly fast post-quantum SNARKs over towers of binary fields
2. What is SNARK? Succinct • The verification cost and proof size are 𝑂(log(𝑛)) Non-interactive • Only one round of communication Argument of knowledge • Prover knows the result of some computation • Proof cannot be forged (with very high probability) by polynomial algorithms Computation Proof 2
3. Binius highlights • One of the fastest post-quantum resistant SNARKs • Works over towers of binary fields • Optimized for hardware • Open-source Rust implementation underApache 2.0 • Created by Irreducible 3
4. Binius performance System # Keccak-f (Size) Proof Size (KiB) Prove Time (s) Verify Time (ms) Scroll 3493 (464 KiB) 40 261 49 Plonky3 4096 (544 KiB) 1 790 16.2 262 Binius 8192 (1000 KiB) 561 2.2 212 Note: Keccak is #1 bottleneck in scaling ZK proofs on Ethereum and other blockchains 4
5. Why Binius is interesting Hardware native field ops • Unlike traditional SNARKs, Binius is designed around binary fields, making it highly efficient for hardware Prominent theoretical contribution • Binius made several SNARK theory advancements pushing the idea of working on binary fields Elegant System Design • Binius combines a rich set of ideas into one optimized protocol 5
6. Binius protocol stack Program execution Program Arithmerization Reductions Cryptography Comitted lists Virtual lists Flushing Rules Channels Commitment Additive NTT Ring Switching FRI Front-loaded sumcheck Fiat-shamir Comitted Polys Virtual Polynomials Zero check Eval check Multiset check Sumcheck Grand product arg 6
7. Arithmetization Transforming program correctness to list relations
8. Arithmetization: Basic overview Claims about lists relations • a[0] = b[0] = 1, c[4] = 13 • a[i] + b[i] = c[i], i = [0, 5) • a[i]=b[i-1], b[i]=c[i-1], i = [1, 5) a b c 1 1 2 1 2 3 2 3 5 3 5 8 5 8 13 Claims about program IO • fibonacci(7) == 13 Artithmetization Reductions Cryptography 8
9. Arithmetization: M3 Committed list 1 ... Committed list n Virtual list 1 ... Virtual list m 12 ... 536 548 ... 524 56 ... 33 89 ... 23 ... ... ... ... ... ... 3 ... 81 84 ... 77 Committed list 1 ... Committed list k Virtual list 1 ... Virtual list l 1235 ... 5465 493 ... 516 36 ... 3347 0 ... 22 ... ... ... ... ... ... 647 ... 234 0 ... 755 Table 1 Table 2 Push Pull Channel 1 (536, 1235) (33, 36) (..., ...) (81, 647) (548, 524) (89, 23) (..., ...) (84, 77) (536, 1235) (33, 36) (..., ...) (81, 647) (548, 524) (89, 23) (..., ...) (84, 77) Artithmetization Reductions Cryptography 9
10. Example: Lasso lookup Read ts (R) Final ts (F) W := aR 𝑟! 𝑓! 𝑟! + 1 𝑟" 𝑓" 𝑟" + 1 𝑟# 𝑓# 𝑟# + 1 𝑟$ 𝑓$ 𝑟$ + 1 Lookup Value (T) Looked up Value (U) O := 𝒂𝟎 5 8 0 6 6 0 7 6 0 8 7 0 • O, R, F, W display 𝑙𝑜𝑔& 𝑥 values • Constraints: R ≠ 0, ∃𝑛: 𝑎' = 1 Artithmetization Reductions Cryptography Push Pull (5, 0) (6, 0) (7, 0) (8, 0) (8, 1) (6, 1) (6, 2) (7, 1) (8, 0) (6, 0) (6, 1) (7, 0) (5, 0) (6, 2) (7, 1) (8, 1) Push Pull (5, 0) (6, 0) (7, 0) (8, 0) (8, 𝑟! + 1) (6, 𝑟" + 1) (6, 𝑟# + 1) (7, 𝑟$ + 1) (8, 𝑟! ) (6, 𝑟" ) (6, 𝑟# ) (7, 𝑟$ ) (5, 𝑓! ) (6, 𝑓" ) (7, 𝑓# ) (8, 𝑓$ ) Push (T, O) Push (U,W) Pull (T, F) Pull (U,R) 10
11. List elements: tower of binary fields 𝑇1 : = 𝔽 2!" = {0, 1} 𝑇3 : = 𝔽 2!# = {𝑎 + 𝑏𝑥3 , 𝑎, 𝑏 ∈ 𝑇345 } 𝑥5 2 = 1 + 𝑥5 𝑇2 : = 𝔽 2!! = {𝑎 + 𝑏𝑥2 , 𝑎, 𝑏 ∈ 𝑇5 } 𝑇5: = 𝔽 2!$ = 0, 1, 𝑥5, 1 + 𝑥5 𝑥2 2 = 1 + 𝑥5 𝑥2 𝑥3 2 = 1 + 𝑥345 𝑥3 Artithmetization Reductions Cryptography 11
12. Reductions Transforming list relations into polynomial evaluations
13. Reductions: Basic overview We aim to check certain relations between lists and channels • A linear combination of lists equaling another list • A new virtual list equaling the concatenation of two other lists • Ensuring the channel is balanced The reductions layer reduces these checks to polynomial evals using the following gadgets: • Zero check: Prove that all values in the list are zero • Multiset check: Prove that the channel is balanced • Eval check: Ensure that the virtual polynomial evals to a specific value s Artithmetization Reductions Cryptography 13
14. Lists -> Polynomials: MLE Problem • Consider a list 𝒕 of size 26 • We want to find a polynomial of 𝑙 variables ̃ 𝑡 (MLE) such that ̃ 𝑡 0,1 6 = 𝑡 Solution • Define ; : 𝑥1 , … , 𝑥645 → ∑781 645 27𝑥7 • Define ? 𝑒𝑞 𝑥1 , … , 𝑥645 , 𝑦1 , … , 𝑦645 : = ∏781 645( 1 − 𝑥7 1 − 𝑦7 + 𝑥7𝑦7) 𝒗 {𝒗} 𝒕{𝒗} = 𝒕(𝒗) (0,0,0) 0 2 2 (1,0,0) 1 5 5 (0,1,0) 2 12 12 (1,1,0) 3 1 1 (0,0,1) 4 0 0 (1,0,1) 5 3 3 (0,1,1) 6 5 5 (1,1,1) 7 7 7 • Then MLE is given by: ̃ 𝑡(𝑥1, … , 𝑥645) ≔ ∑F ∈{1,5}# 𝑡{F} ; ? 𝑒𝑞 𝑣1, … , 𝑣645, 𝑥1, … , 𝑥645 Example: MLE Artithmetization Reductions Cryptography 14
15. Virtual polynomials Leaf virtual polynomials • Committed –opaque polynomials, can be evaled by oracle • Transparent – small polynomials, can be evaled by the verifier Node virtual polynomials • Linear combinations: 𝑎!𝑡! 𝑥 + ⋯ + 𝑎"𝑡" 𝑥 • Merging: (1 − 𝑥#)𝑡! 𝑥!, … , 𝑥#$% + 𝑥#𝑡% 𝑥!, … , 𝑥#$% • Shifting • Zero-padding Artithmetization Reductions Cryptography 15
16. Evalcheck Artithmetization Reductions Cryptography Committed Sum check Committed Transparent Virtual Virtual Virtual Virtual Virtual Sum check Sum check 16
17. Basic list relations: zero check • Consider some virtual polynomial 𝐶 • We want to reduce the check 𝐶 0,1 6 = 0 to eval check of 𝐶 • H 𝐶 𝑥 ≔ ∑ ∀F∈ 1,5 % 𝐶(𝑣) ; ? 𝑒𝑞 𝑥1 , … , 𝑥645 , 𝑣1 , … , 𝑣645 • If zero check holds then H 𝐶 𝑟 = 0 for some random 𝑟 • So 0 = ∑ ∀F∈ 1,5 % 𝐶(𝑣) ; ? 𝑒𝑞 𝑟1 , … , 𝑟645 , 𝑣1 , … , 𝑣645 • Using sum check protocol we can reduce this to eval of 𝐶 𝑟I ; ? 𝑒𝑞 𝑟1 , … , 𝑟645 , 𝑟I 1 , … , 𝑟I 645 for some 𝑟I Artithmetization Reductions Cryptography 𝑨 𝑩 C=A-B 2 2 0 5 5 0 12 12 0 1 1 0 0 0 0 3 3 0 5 5 0 7 7 0 Motivational example 17
18. Channels balance: multiset check • Each 𝑇7 , 𝑈7 is a merge of polynomials that are flushed from different tables • We must check 𝑇1(𝑣), … , 𝑇L(𝑣) 𝑣 ∈ 0, 1 6} = 𝑈1(𝑣), … , 𝑈L(𝑣) 𝑣 ∈ 0, 1 6} • Sample random s and define 𝑇∗ 𝑣 ≔ ∑781 L 𝑠7𝑇7 (𝑣) • Reduce to 𝑇∗(𝑣) 𝑣 ∈ 0, 1 6} = 𝑈∗(𝑣) 𝑣 ∈ 0, 1 6} • Reduce to ∏ F∈ 1,5 % 𝑟 + 𝑇∗ 𝑣 = ∏ F∈ 1,5 % 𝑟 + 𝑈∗ 𝑣 • This is grand product argument that reduces to sumchecks Artithmetization Reductions Cryptography Push Pull 𝑻𝟎 … 𝑻𝒎 2 … 3 5 … 32 12 … 1 1 … 2 0 … 10 3 … 20 5 … 32 7 … 54 𝑼𝟎 … 𝑼𝒎 12 … 1 1 … 2 2 … 3 5 … 32 5 … 32 7 … 54 0 … 10 3 … 20 18
19. Sumcheck protocol • Problem: reduce checking 𝑠1 = ∑ F∈{1,5}% 𝐶(𝑣) to 𝑠6 = 𝐶(𝑟) • At round 𝑖 ∈ [0, 𝑙): • Prover computes 𝑔& 𝑥 ≔ ∑ '∈{!,%}!"#"$ 𝐶(𝑟!, … , 𝑟&$%, 𝑥, 𝑣!, … , 𝑣#$&$,) and sends ̅ 𝑔& 𝑥 = 𝑔& 𝑥 to verifier • Verifier checks 𝑠& = ̅ 𝑔& 0 + ̅ 𝑔& 1 • Verifier generates random 𝑟& , sends it to prover and updates 𝑠&-%: = ̅ 𝑔& 𝑟& • At round 𝑙: the verifier checks 𝑠6 = 𝐶(𝑟) • Claim: 𝑠7 = ∑ F∈{1,5}%&' 𝐶(𝑟1 , … , 𝑟745 , 𝑣1 , … , 𝑣64745 ) iff 𝑠7Q5 = ∑ F∈{1,5}%&'&$ 𝐶(𝑟1, … , 𝑟7, 𝑣1, … , 𝑣64742) Artithmetization Reductions Cryptography 19
20. Cryptography Evaluating polynomials
21. Cryptography: Basic idea • We aim to emulate an oracle that performs polynomial evaluations • The prover commits to the polynomial by sending a short hash (commitment) to the verifier • We have the protocol that ensures the prover can prove the correctness of any claimed evaluation • The verifier, having the commitment, is guaranteed soundness—the prover can’t cheat Polynomial Oracle Prover Verifier Polynomial Evals Prover Verifier Commitment Evals Artithmetization Cryptography Reductions 21
22. Commitments • Start with MLE polynomial 𝑡(𝑥1 , … 𝑥645 ) • Convert coefficients to the list of values 𝑡1 , … , 𝑡2%45 • Make an additive NTT-friendly polynomial 𝑃 𝑥 = 𝑡1 + ⋯ + 𝑡2%45 𝑝2%45 (𝑥) • Pick rate 𝑅 and Evaluate Reed-Solomon codeword 𝑏 = (𝑏1, … , 𝑏2%()45 ) as 𝑃 S , S – is a subspace of 𝑇6 • Merkle-commit the list 𝑏 (this will be the commitment of 𝑡) • Eval: FRI (Fast Reed-Solomon Interactive Oracle Proofs of Proximity) Artithmetization Cryptography Reductions 22
23. Ring swicthing: motivation • Sumcheck and other protocols work on large fields like 𝑇R • Real world arithmetization lists have small values like 𝑇ST • We can pack 8-128 small values into one large field element • Packing: 𝑡 𝑥1 , … , 𝑥645 ∈ 𝑇6 𝑥 ⇒ 𝑡 𝑥1 , … , 𝑥64U45 ∈ 𝑇6QU 𝑥 • Refinement: inverse of packing 𝒕(𝒙𝟏 , 𝒙𝟐 , 𝒙𝟑 ) 1 1 1 0 0 1 0 0 Artithmetization Cryptography Reductions 𝒕(𝒙𝟏 ) 11100100 23
24. Ring swicthing: Tensor product algebra • Consider 𝑇W /𝑇6 , 𝑘: = 𝜏 − 𝑙 • 𝑇W is a 𝑇6 -algebra with vector basis (𝛼1 , … , 𝛼2*45 ) ∈ 𝑇W 2* • Consider 𝐴 ≔ 𝑇W ⨂X% 𝑇W , then 𝐴 is a 𝑇6 -algebra • dim 𝐴 = 22U, an element of 𝐴 is a matrix 2U × 2U • Basis of 𝐴 is Artithmetization Cryptography Reductions 24 𝛼/ ⨂𝛼/ 𝛼/ ⨂𝛼! … 𝛼/ ⨂𝛼"!0! 𝛼! ⨂𝛼/ 𝛼! ⨂𝛼! … 𝛼! ⨂𝛼 "!0! … … … … 𝛼 "!0! ⨂𝛼/ 𝛼 "!0! ⨂𝛼! … 𝛼 "!0! ⨂𝛼 "!0!
25. Ring swicthing: Lifting values 2 0 0 0 5 0 0 0 12 0 0 0 1 0 0 0 (2, 5, 12, 1) ∈ 𝑇W 𝜑1 2 5 12 1 0 0 0 0 0 0 0 0 0 0 0 0 2, 5, 12, 1 ∈ 𝑇W 𝜑5 Artithmetization Cryptography Reductions 25
26. Ring swicthing: Partial evaluations Artithmetization Cryptography Reductions • We want to reduce evaluation of refined polynomial 𝑡I 𝑥1 , … , 𝑥6QU45 to evaluating 𝑡 𝑥1 , … , 𝑥645 • Evaluation of 𝑡 𝑟1, … , 𝑟645 = 𝑡{F} ;⊗781 645 (1 − 𝑟7, 𝑟7) • So it's hard to evaluate refined vector 𝑡′{F} just using the values of coarse vector 𝑡{F} • But we actually can do it if we lift 𝑡 coeffs to 𝐴 using 𝜑5 and lift 𝑟7 to 𝐴 using 𝜑1 • Then 𝜑5(𝑡)(𝜑1 𝑟1 , … , 𝜑1 𝑟645 ){F} = 𝑡I 𝑣1, … , 𝑣U45, 𝑥U, … , 𝑥UQ645 • 𝑡I 𝑟1 , … , 𝑟6QU45 = ∑ F ∈{1,5}* 𝑡I 𝑣1 , … , 𝑣U45 , 𝑟U , … , 𝑟UQ645 ; ? 𝑒𝑞 𝑟1 , … , 𝑟U45 , 𝑣1 , … , 𝑣U45 26
27. Ring swicthing: Example 𝒕′{𝒗} 𝒕{𝒗} 0 i 1 1 1 0 • Consider 𝑇5 = {0, 1} and 𝑇2 = {0, 1, 𝑖, 1 + 𝑖} • 𝜏 = 2, 𝑘 = 1, 𝑙 = 1 • 𝑡′ 𝑥1 , 𝑥5 = 𝑥1 1 − 𝑥5 + 1 − 𝑥1 𝑥5 • 𝑡′ 0, 𝑟 = 𝑟 • 𝑡′ 1, 𝑟 = 1 + 𝑟 • 𝑡 𝑥1 = 𝑖 1 − 𝑥1 + 𝑥1 = 𝑖 + 1 + 𝑖 𝑥1 0 1 0 0 𝜑%(𝑖) 1 1 0 0 𝜑%(1 + 𝑖) 𝑟/ 0 𝑟! 0 𝜑!(𝑟) 𝑡 𝑟 𝑟/ 1 + 𝑟/ 𝑟! 𝑟! 𝑟/ 𝑟/ 𝑟! 𝑟! 𝜑%(1 + 𝑖)𝜑!(𝑟) Artithmetization Cryptography Reductions 27
28. Binius: Putting it all together Artithmetization Cryptography Reductions • Pack all the committed lists 𝑡′! into 𝑡! using ring switching • Next, 𝑡! s are merged into 𝑡 and padded with zeroes if necessary • Send commitment to 𝑡 to the verifier • Run reductions and batch sum checks to reduce the proof to evals of different 𝑡′! • For each 𝑡′! eval use ring switching and reduce to sum-checks of 𝑡! , being a part of 𝑡 • Use batch sum-check to reduce that to a single claim about 𝑡 • Run the FRI protocol 28
29. Q&A