Phân tích nguyên lý Binius STARKs và suy nghĩ về tối ưu hóa
1 Giới thiệu
STARKs là một hệ thống chứng minh dựa trên băm, khác với SNARKs dựa trên đường cong ellip. Một trong những lý do chính khiến STARKs hiện tại kém hiệu quả là: hầu hết các giá trị trong chương trình thực tế đều nhỏ, như chỉ số trong vòng lặp for, giá trị true/false, bộ đếm, v.v. Tuy nhiên, để đảm bảo tính an toàn của chứng minh dựa trên cây Merkle, khi sử dụng mã hóa Reed-Solomon để mở rộng dữ liệu, nhiều giá trị dư thừa bổ sung sẽ chiếm lĩnh toàn bộ miền, ngay cả khi giá trị gốc rất nhỏ. Để giải quyết vấn đề này, giảm kích thước miền trở thành chiến lược then chốt.
Như bảng 1 cho thấy, độ rộng mã hóa của STARKs thế hệ thứ nhất là 252bit, độ rộng mã hóa của STARKs thế hệ thứ hai là 64bit, độ rộng mã hóa của STARKs thế hệ thứ ba là 32bit, nhưng độ rộng mã hóa 32bit vẫn còn rất nhiều không gian lãng phí. So với đó, miền nhị phân cho phép thao tác trực tiếp trên các bit, mã hóa chặt chẽ hiệu quả mà không có không gian lãng phí nào, tức là STARKs thế hệ thứ tư.
Bảng 1: Đường đi của STARKs
| Thế hệ | Bề rộng | Đặc điểm |
|------|------|------|
| Thế hệ 1 | 252bit | Vùng lớn, lãng phí không gian lớn |
| Thế hệ thứ 2 | 64bit | Miền trung, lãng phí không gian khá lớn |
| Thế hệ thứ 3 | 32bit | Tiểu miền, vẫn còn lãng phí không gian |
| Thế hệ thứ 4 | 1bit | Miền nhị phân, không lãng phí không gian |
So với các miền hữu hạn được phát hiện gần đây như Goldilocks, BabyBear, Mersenne31, nghiên cứu về miền nhị phân có thể truy ngược đến những năm 80 của thế kỷ trước. Hiện tại, miền nhị phân đã được ứng dụng rộng rãi trong mật mã học, ví dụ điển hình bao gồm:
Tiêu chuẩn mã hóa nâng cao (AES), dựa trên miền F28;
Mã xác thực tin nhắn Galois ( GMAC ), dựa trên miền F2128;
Mã QR, sử dụng mã hóa Reed-Solomon dựa trên F28;
Giao thức FRI gốc và zk-STARK, cùng với hàm băm Grøstl vào chung kết SHA-3, hàm này dựa trên miền F28, là một thuật toán băm rất phù hợp cho đệ quy.
Khi sử dụng miền nhỏ hơn, thao tác mở rộng miền càng trở nên quan trọng để đảm bảo tính an toàn. Miền nhị phân mà Binius sử dụng hoàn toàn phụ thuộc vào việc mở rộng miền để đảm bảo tính an toàn và khả năng sử dụng thực tế. Hầu hết các đa thức liên quan trong tính toán Prover không cần phải vào miền mở rộng, mà chỉ cần thao tác trong miền cơ sở, từ đó đạt được hiệu suất cao trong miền nhỏ. Tuy nhiên, việc kiểm tra điểm ngẫu nhiên và tính toán FRI vẫn cần phải đi sâu vào miền mở rộng lớn hơn để đảm bảo tính an toàn cần thiết.
Khi xây dựng hệ thống chứng minh dựa trên miền nhị phân, có 2 vấn đề thực tế: Khi tính toán trace trong STARKs, kích thước miền sử dụng phải lớn hơn bậc của đa thức; Khi cam kết Merkle tree trong STARKs, cần thực hiện mã hóa Reed-Solomon, kích thước miền sử dụng phải lớn hơn kích thước sau khi mở rộng mã.
Binius đã đề xuất một giải pháp đổi mới, xử lý hai vấn đề này một cách riêng biệt và thể hiện cùng một dữ liệu theo hai cách khác nhau: trước hết, sử dụng đa biến ( cụ thể là đa thức nhiều tuyến tính ) thay thế cho đa thức một biến, thông qua giá trị của nó trên "siêu lập phương" ( hypercubes ) để thể hiện toàn bộ quỹ đạo tính toán; thứ hai, do chiều dài của mỗi chiều của siêu lập phương đều là 2, nên không thể thực hiện mở rộng Reed-Solomon tiêu chuẩn như STARKs, nhưng có thể coi siêu lập phương như hình vuông ( square ), dựa trên hình vuông đó để thực hiện mở rộng Reed-Solomon. Phương pháp này đảm bảo tính an toàn trong khi cải thiện đáng kể hiệu quả mã hóa và hiệu suất tính toán.
2 Phân tích nguyên lý
Hiện tại, việc xây dựng hầu hết các hệ thống SNARKs thường bao gồm hai phần sau:
Chứng minh Oracle Tương tác Đa thức Thông tin Lý thuyết (, PIOP ): PIOP là cốt lõi của hệ thống chứng minh, chuyển đổi quan hệ tính toán đầu vào thành các phương trình đa thức có thể xác minh. Các giao thức PIOP khác nhau cho phép người chứng minh gửi từng bước đa thức thông qua tương tác với người xác minh, giúp người xác minh chỉ cần truy vấn một lượng nhỏ kết quả đánh giá của đa thức để xác minh tính chính xác của tính toán. Các giao thức PIOP hiện có bao gồm: PLONK PIOP, Spartan PIOP và HyperPlonk PIOP, mỗi cái trong số đó có cách xử lý các biểu thức đa thức khác nhau, từ đó ảnh hưởng đến hiệu suất và hiệu quả của toàn bộ hệ thống SNARK.
Kế hoạch cam kết đa thức ( Polynomial Commitment Scheme, PCS ): Kế hoạch cam kết đa thức được sử dụng để chứng minh liệu các phương trình đa thức được tạo ra bởi PIOP có hợp lệ hay không. PCS là một công cụ mật mã, thông qua đó, người chứng minh có thể cam kết một đa thức và sau đó xác minh kết quả đánh giá của đa thức đó, đồng thời ẩn đi các thông tin khác của đa thức. Các kế hoạch cam kết đa thức phổ biến bao gồm KZG, Bulletproofs, FRI ( Fast Reed-Solomon IOPP ) và Brakedown, v.v. Các PCS khác nhau có hiệu suất, độ an toàn và场景适用 khác nhau.
Dựa trên nhu cầu cụ thể, chọn PIOP và PCS khác nhau, và kết hợp với miền hữu hạn hoặc đường cong elliptic phù hợp, có thể xây dựng hệ thống chứng minh với các thuộc tính khác nhau. Ví dụ:
• Halo2: Kết hợp giữa PLONK PIOP và Bulletproofs PCS, dựa trên đường cong Pasta. Halo2 được thiết kế với trọng tâm là khả năng mở rộng và loại bỏ thiết lập tin cậy trong giao thức ZCash.
• Plonky2: áp dụng PLONK PIOP và FRI PCS kết hợp, và dựa trên miền Goldilocks. Plonky2 được thiết kế để đạt được tính đệ quy hiệu quả. Khi thiết kế những hệ thống này, PIOP và PCS được chọn phải phù hợp với miền hữu hạn hoặc đường cong elip được sử dụng, để đảm bảo tính chính xác, hiệu suất và an toàn của hệ thống. Sự lựa chọn của những sự kết hợp này không chỉ ảnh hưởng đến kích thước chứng minh SNARK và hiệu quả xác minh, mà còn quyết định xem hệ thống có thể đạt được tính minh bạch mà không cần thiết lập đáng tin cậy hay không, và có thể hỗ trợ các chức năng mở rộng như chứng minh đệ quy hoặc chứng minh tổng hợp hay không.
Binius: HyperPlonk PIOP + Brakedown PCS + miền nhị phân. Cụ thể, Binius bao gồm năm công nghệ chính để đạt được hiệu quả và an toàn của nó. Đầu tiên, dựa trên miền nhị phân hình tháp (towers of binary fields), cấu trúc số học đã tạo thành nền tảng cho tính toán của nó, cho phép thực hiện các phép toán đơn giản hóa trong miền nhị phân. Thứ hai, Binius trong giao thức chứng minh Oracle tương tác (PIOP) của mình, đã điều chỉnh HyperPlonk sản phẩm và kiểm tra hoán đổi, đảm bảo sự kiểm tra tính nhất quán an toàn và hiệu quả giữa các biến và các hoán đổi của chúng. Thứ ba, giao thức đã đưa vào một chứng minh dịch chuyển đa tuyến mới, tối ưu hóa hiệu quả xác minh các mối quan hệ đa tuyến trên miền nhỏ. Thứ tư, Binius đã áp dụng phiên bản cải tiến của chứng minh tìm kiếm Lasso, cung cấp tính linh hoạt và an ninh mạnh mẽ cho cơ chế tìm kiếm. Cuối cùng, giao thức sử dụng kế hoạch cam kết đa thức miền nhỏ (Small-Field PCS), cho phép nó thực hiện hệ thống chứng minh hiệu quả trên miền nhị phân, và giảm thiểu các chi phí thường liên quan đến miền lớn.
2.1 Miền hữu hạn: Toán tử hóa dựa trên towers of binary fields
Miền nhị phân tháp là yếu tố then chốt trong việc thực hiện tính toán có thể xác minh nhanh chóng, chủ yếu nhờ vào hai khía cạnh: tính toán hiệu quả và tính toán hình thức hiệu quả. Miền nhị phân về bản chất hỗ trợ các phép toán hình thức cực kỳ hiệu quả, khiến nó trở thành lựa chọn lý tưởng cho các ứng dụng mật mã nhạy cảm với yêu cầu hiệu suất. Hơn nữa, cấu trúc miền nhị phân hỗ trợ quy trình hình thức hóa được đơn giản hóa, tức là các phép toán thực hiện trên miền nhị phân có thể được biểu diễn dưới dạng đại số ngắn gọn và dễ xác minh. Những đặc tính này, cộng với khả năng tận dụng triệt để các đặc điểm phân cấp thông qua cấu trúc tháp, khiến miền nhị phân đặc biệt phù hợp cho các hệ thống chứng minh có thể mở rộng như Binius.
Trong đó, "canonical" đề cập đến cách thức biểu diễn duy nhất và trực tiếp của các phần tử trong miền nhị phân. Ví dụ, trong miền nhị phân cơ bản F2, bất kỳ chuỗi k bit nào cũng có thể được ánh xạ trực tiếp thành một phần tử miền nhị phân k bit. Điều này khác với miền số nguyên tố, miền số nguyên tố không thể cung cấp cách biểu diễn chuẩn như vậy trong một số bit nhất định. Mặc dù miền số nguyên tố 32 bit có thể chứa trong 32 bit, nhưng không phải mỗi chuỗi 32 bit đều có thể tương ứng duy nhất với một phần tử miền, trong khi miền nhị phân lại có sự thuận lợi của ánh xạ một-một này. Trong miền số nguyên tố Fp, các phương pháp giảm phổ biến bao gồm giảm Barrett, giảm Montgomery, và các phương pháp giảm đặc biệt cho các miền hữu hạn cụ thể như Mersenne-31 hoặc Goldilocks-64. Trong miền nhị phân F2k, các phương pháp giảm thường được sử dụng bao gồm giảm đặc biệt ( như trong AES sử dụng ), giảm Montgomery ( như trong POLYVAL sử dụng ) và giảm đệ quy ( như Tower ). Bài báo "Khám Phá Không Gian Thiết Kế của So Sánh Trường Số Nguyên Tố và Trường Nhị Phân ECC-Hardware Implementations" chỉ ra rằng, miền nhị phân không cần phải đưa vào carry trong các phép toán cộng và nhân, và phép toán bình phương của miền nhị phân rất hiệu quả, vì nó tuân theo quy tắc đơn giản (X + Y )2 = X2 + Y2.
Như hình 1 cho thấy, một chuỗi 128 bit: Chuỗi này có thể được giải thích theo nhiều cách trong ngữ cảnh của miền nhị phân. Nó có thể được coi là một phần tử duy nhất trong miền nhị phân 128 bit, hoặc được phân tích thành hai phần tử miền tháp 64 bit, bốn phần tử miền tháp 32 bit, mười sáu phần tử miền tháp 8 bit, hoặc 128 phần tử miền F2. Sự linh hoạt trong cách biểu diễn này không yêu cầu bất kỳ chi phí tính toán nào, chỉ là chuyển đổi kiểu chuỗi bit (typecast), là một thuộc tính rất thú vị và hữu ích. Đồng thời, các phần tử miền nhỏ có thể được gói lại thành các phần tử miền lớn hơn mà không cần chi phí tính toán bổ sung. Giao thức Binius đã tận dụng đặc điểm này để nâng cao hiệu quả tính toán. Hơn nữa, tài liệu "On Efficient Inversion in Tower Fields of Characteristic Two" đã khám phá độ phức tạp tính toán của phép nhân, bình phương và phép nghịch đảo trong miền tháp nhị phân n bit ( có thể phân tích thành miền con m bit ).
2.2 PIOP: Phiên bản cải biên của sản phẩm HyperPlonk và Kiểm tra hoán vị------Áp dụng cho trường nhị phân
Thiết kế PIOP trong giao thức Binius đã mượn ý tưởng từ HyperPlonk, áp dụng một loạt các cơ chế kiểm tra cốt lõi, được sử dụng để xác minh tính chính xác của đa thức và tập hợp đa biến. Những kiểm tra cốt lõi này bao gồm:
GateCheck: Xác minh chứng nhận bảo mật ω và đầu vào công khai x có thỏa mãn quan hệ toán tử của mạch C(x, ω)=0, để đảm bảo mạch hoạt động chính xác.
PermutationCheck: Xác thực kết quả đánh giá của hai đa thức nhiều biến f và g trên hypercube Boole là quan hệ hoán vị f(x) = f(π(x)), để đảm bảo tính nhất quán của sự sắp xếp giữa các biến đa thức.
LookupCheck: Kiểm tra xem giá trị của đa thức có nằm trong bảng tra cứu đã cho hay không, tức là f(Bµ) ⊆ T(Bµ), đảm bảo một số giá trị nằm trong khoảng đã chỉ định.
MultisetCheck: Kiểm tra xem hai tập hợp đa biến có bằng nhau hay không, tức là {(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H, đảm bảo tính nhất quán giữa nhiều tập hợp.
ProductCheck: Kiểm tra xem việc đánh giá đa thức hợp lý trên siêu lập phương Bool có bằng một giá trị đã tuyên bố nào đó ∏x∈Hµ f(x) = s, để đảm bảo tính chính xác của tích đa thức.
ZeroCheck: Xác minh một đa thức nhiều biến trên siêu khối Boolean tại bất kỳ điểm nào có phải là không ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, để đảm bảo phân bố của các điểm không của đa thức.
SumCheck: Kiểm tra xem tổng của đa thức nhiều biến có bằng giá trị đã khai báo hay không ∑x∈Hµ f(x) = s. Bằng cách chuyển đổi bài toán đánh giá đa thức nhiều biến thành bài toán đánh giá đa thức một biến, giảm độ phức tạp tính toán của bên xác minh. Ngoài ra, SumCheck còn cho phép xử lý hàng loạt, bằng cách giới thiệu số ngẫu nhiên, xây dựng tổ hợp tuyến tính để thực hiện xử lý hàng loạt cho nhiều trường hợp kiểm tra tổng.
BatchCheck: Dựa trên SumCheck, xác minh tính chính xác của việc đánh giá nhiều đa thức nhiều biến để nâng cao hiệu quả của giao thức.
Mặc dù Binius và HyperPlonk có nhiều điểm tương đồng trong thiết kế giao thức, nhưng Binius đã cải tiến ở 3 điểm sau:
Tối ưu hóa ProductCheck: Trong HyperPlonk, ProductCheck yêu cầu mẫu số U không được bằng 0 ở mọi điểm trên khối siêu lập phương, và tích phải bằng một giá trị cụ thể; Binius đã đơn giản hóa quy trình kiểm tra này bằng cách đặc trưng giá trị đó thành 1, từ đó giảm độ phức tạp tính toán.
Xử lý vấn đề chia cho zero: HyperPlonk không xử lý đầy đủ tình huống chia cho zero, dẫn đến không thể khẳng định rằng U không bằng không trên hypercube; Binius đã xử lý đúng vấn đề này, ngay cả khi mẫu số bằng zero, ProductCheck của Binius vẫn có thể tiếp tục xử lý, cho phép mở rộng đến bất kỳ giá trị tích nào.
Kiểm tra hoán vị giữa các cột: HyperPlonk không có tính năng này; Binius hỗ trợ kiểm tra hoán vị giữa nhiều cột, điều này cho phép Binius xử lý các trường hợp sắp xếp đa thức phức tạp hơn.
Do đó, Binius đã cải tiến cơ chế PIOPSumCheck hiện có, nâng cao tính linh hoạt và hiệu quả của giao thức, đặc biệt là trong việc xử lý xác minh đa thức đa biến phức tạp hơn, cung cấp hỗ trợ chức năng mạnh mẽ hơn. Những cải tiến này không chỉ giải quyết những hạn chế trong HyperPlonk, mà còn cho những điều chưa...
Xem bản gốc
Trang này có thể chứa nội dung của bên thứ ba, được cung cấp chỉ nhằm mục đích thông tin (không phải là tuyên bố/bảo đảm) và không được coi là sự chứng thực cho quan điểm của Gate hoặc là lời khuyên về tài chính hoặc chuyên môn. Xem Tuyên bố từ chối trách nhiệm để biết chi tiết.
8 thích
Phần thưởng
8
5
Chia sẻ
Bình luận
0/400
SelfCustodyIssues
· 07-11 16:18
Tốc độ phát triển này thực sự giảm pit.
Xem bản gốcTrả lời0
CryptoTarotReader
· 07-11 09:56
Lập trình viên lại bắt đầu cạnh tranh trong lĩnh vực này, có cần thiết không?
Binius miền nhị phân STARKs: Phân tích nguyên lý và đổi mới tối ưu hóa
Phân tích nguyên lý Binius STARKs và suy nghĩ về tối ưu hóa
1 Giới thiệu
STARKs là một hệ thống chứng minh dựa trên băm, khác với SNARKs dựa trên đường cong ellip. Một trong những lý do chính khiến STARKs hiện tại kém hiệu quả là: hầu hết các giá trị trong chương trình thực tế đều nhỏ, như chỉ số trong vòng lặp for, giá trị true/false, bộ đếm, v.v. Tuy nhiên, để đảm bảo tính an toàn của chứng minh dựa trên cây Merkle, khi sử dụng mã hóa Reed-Solomon để mở rộng dữ liệu, nhiều giá trị dư thừa bổ sung sẽ chiếm lĩnh toàn bộ miền, ngay cả khi giá trị gốc rất nhỏ. Để giải quyết vấn đề này, giảm kích thước miền trở thành chiến lược then chốt.
Như bảng 1 cho thấy, độ rộng mã hóa của STARKs thế hệ thứ nhất là 252bit, độ rộng mã hóa của STARKs thế hệ thứ hai là 64bit, độ rộng mã hóa của STARKs thế hệ thứ ba là 32bit, nhưng độ rộng mã hóa 32bit vẫn còn rất nhiều không gian lãng phí. So với đó, miền nhị phân cho phép thao tác trực tiếp trên các bit, mã hóa chặt chẽ hiệu quả mà không có không gian lãng phí nào, tức là STARKs thế hệ thứ tư.
Bảng 1: Đường đi của STARKs
| Thế hệ | Bề rộng | Đặc điểm | |------|------|------| | Thế hệ 1 | 252bit | Vùng lớn, lãng phí không gian lớn | | Thế hệ thứ 2 | 64bit | Miền trung, lãng phí không gian khá lớn |
| Thế hệ thứ 3 | 32bit | Tiểu miền, vẫn còn lãng phí không gian | | Thế hệ thứ 4 | 1bit | Miền nhị phân, không lãng phí không gian |
So với các miền hữu hạn được phát hiện gần đây như Goldilocks, BabyBear, Mersenne31, nghiên cứu về miền nhị phân có thể truy ngược đến những năm 80 của thế kỷ trước. Hiện tại, miền nhị phân đã được ứng dụng rộng rãi trong mật mã học, ví dụ điển hình bao gồm:
Tiêu chuẩn mã hóa nâng cao (AES), dựa trên miền F28;
Mã xác thực tin nhắn Galois ( GMAC ), dựa trên miền F2128;
Mã QR, sử dụng mã hóa Reed-Solomon dựa trên F28;
Giao thức FRI gốc và zk-STARK, cùng với hàm băm Grøstl vào chung kết SHA-3, hàm này dựa trên miền F28, là một thuật toán băm rất phù hợp cho đệ quy.
Khi sử dụng miền nhỏ hơn, thao tác mở rộng miền càng trở nên quan trọng để đảm bảo tính an toàn. Miền nhị phân mà Binius sử dụng hoàn toàn phụ thuộc vào việc mở rộng miền để đảm bảo tính an toàn và khả năng sử dụng thực tế. Hầu hết các đa thức liên quan trong tính toán Prover không cần phải vào miền mở rộng, mà chỉ cần thao tác trong miền cơ sở, từ đó đạt được hiệu suất cao trong miền nhỏ. Tuy nhiên, việc kiểm tra điểm ngẫu nhiên và tính toán FRI vẫn cần phải đi sâu vào miền mở rộng lớn hơn để đảm bảo tính an toàn cần thiết.
Khi xây dựng hệ thống chứng minh dựa trên miền nhị phân, có 2 vấn đề thực tế: Khi tính toán trace trong STARKs, kích thước miền sử dụng phải lớn hơn bậc của đa thức; Khi cam kết Merkle tree trong STARKs, cần thực hiện mã hóa Reed-Solomon, kích thước miền sử dụng phải lớn hơn kích thước sau khi mở rộng mã.
Binius đã đề xuất một giải pháp đổi mới, xử lý hai vấn đề này một cách riêng biệt và thể hiện cùng một dữ liệu theo hai cách khác nhau: trước hết, sử dụng đa biến ( cụ thể là đa thức nhiều tuyến tính ) thay thế cho đa thức một biến, thông qua giá trị của nó trên "siêu lập phương" ( hypercubes ) để thể hiện toàn bộ quỹ đạo tính toán; thứ hai, do chiều dài của mỗi chiều của siêu lập phương đều là 2, nên không thể thực hiện mở rộng Reed-Solomon tiêu chuẩn như STARKs, nhưng có thể coi siêu lập phương như hình vuông ( square ), dựa trên hình vuông đó để thực hiện mở rộng Reed-Solomon. Phương pháp này đảm bảo tính an toàn trong khi cải thiện đáng kể hiệu quả mã hóa và hiệu suất tính toán.
2 Phân tích nguyên lý
Hiện tại, việc xây dựng hầu hết các hệ thống SNARKs thường bao gồm hai phần sau:
Chứng minh Oracle Tương tác Đa thức Thông tin Lý thuyết (, PIOP ): PIOP là cốt lõi của hệ thống chứng minh, chuyển đổi quan hệ tính toán đầu vào thành các phương trình đa thức có thể xác minh. Các giao thức PIOP khác nhau cho phép người chứng minh gửi từng bước đa thức thông qua tương tác với người xác minh, giúp người xác minh chỉ cần truy vấn một lượng nhỏ kết quả đánh giá của đa thức để xác minh tính chính xác của tính toán. Các giao thức PIOP hiện có bao gồm: PLONK PIOP, Spartan PIOP và HyperPlonk PIOP, mỗi cái trong số đó có cách xử lý các biểu thức đa thức khác nhau, từ đó ảnh hưởng đến hiệu suất và hiệu quả của toàn bộ hệ thống SNARK.
Kế hoạch cam kết đa thức ( Polynomial Commitment Scheme, PCS ): Kế hoạch cam kết đa thức được sử dụng để chứng minh liệu các phương trình đa thức được tạo ra bởi PIOP có hợp lệ hay không. PCS là một công cụ mật mã, thông qua đó, người chứng minh có thể cam kết một đa thức và sau đó xác minh kết quả đánh giá của đa thức đó, đồng thời ẩn đi các thông tin khác của đa thức. Các kế hoạch cam kết đa thức phổ biến bao gồm KZG, Bulletproofs, FRI ( Fast Reed-Solomon IOPP ) và Brakedown, v.v. Các PCS khác nhau có hiệu suất, độ an toàn và场景适用 khác nhau.
Dựa trên nhu cầu cụ thể, chọn PIOP và PCS khác nhau, và kết hợp với miền hữu hạn hoặc đường cong elliptic phù hợp, có thể xây dựng hệ thống chứng minh với các thuộc tính khác nhau. Ví dụ:
• Halo2: Kết hợp giữa PLONK PIOP và Bulletproofs PCS, dựa trên đường cong Pasta. Halo2 được thiết kế với trọng tâm là khả năng mở rộng và loại bỏ thiết lập tin cậy trong giao thức ZCash.
• Plonky2: áp dụng PLONK PIOP và FRI PCS kết hợp, và dựa trên miền Goldilocks. Plonky2 được thiết kế để đạt được tính đệ quy hiệu quả. Khi thiết kế những hệ thống này, PIOP và PCS được chọn phải phù hợp với miền hữu hạn hoặc đường cong elip được sử dụng, để đảm bảo tính chính xác, hiệu suất và an toàn của hệ thống. Sự lựa chọn của những sự kết hợp này không chỉ ảnh hưởng đến kích thước chứng minh SNARK và hiệu quả xác minh, mà còn quyết định xem hệ thống có thể đạt được tính minh bạch mà không cần thiết lập đáng tin cậy hay không, và có thể hỗ trợ các chức năng mở rộng như chứng minh đệ quy hoặc chứng minh tổng hợp hay không.
Binius: HyperPlonk PIOP + Brakedown PCS + miền nhị phân. Cụ thể, Binius bao gồm năm công nghệ chính để đạt được hiệu quả và an toàn của nó. Đầu tiên, dựa trên miền nhị phân hình tháp (towers of binary fields), cấu trúc số học đã tạo thành nền tảng cho tính toán của nó, cho phép thực hiện các phép toán đơn giản hóa trong miền nhị phân. Thứ hai, Binius trong giao thức chứng minh Oracle tương tác (PIOP) của mình, đã điều chỉnh HyperPlonk sản phẩm và kiểm tra hoán đổi, đảm bảo sự kiểm tra tính nhất quán an toàn và hiệu quả giữa các biến và các hoán đổi của chúng. Thứ ba, giao thức đã đưa vào một chứng minh dịch chuyển đa tuyến mới, tối ưu hóa hiệu quả xác minh các mối quan hệ đa tuyến trên miền nhỏ. Thứ tư, Binius đã áp dụng phiên bản cải tiến của chứng minh tìm kiếm Lasso, cung cấp tính linh hoạt và an ninh mạnh mẽ cho cơ chế tìm kiếm. Cuối cùng, giao thức sử dụng kế hoạch cam kết đa thức miền nhỏ (Small-Field PCS), cho phép nó thực hiện hệ thống chứng minh hiệu quả trên miền nhị phân, và giảm thiểu các chi phí thường liên quan đến miền lớn.
2.1 Miền hữu hạn: Toán tử hóa dựa trên towers of binary fields
Miền nhị phân tháp là yếu tố then chốt trong việc thực hiện tính toán có thể xác minh nhanh chóng, chủ yếu nhờ vào hai khía cạnh: tính toán hiệu quả và tính toán hình thức hiệu quả. Miền nhị phân về bản chất hỗ trợ các phép toán hình thức cực kỳ hiệu quả, khiến nó trở thành lựa chọn lý tưởng cho các ứng dụng mật mã nhạy cảm với yêu cầu hiệu suất. Hơn nữa, cấu trúc miền nhị phân hỗ trợ quy trình hình thức hóa được đơn giản hóa, tức là các phép toán thực hiện trên miền nhị phân có thể được biểu diễn dưới dạng đại số ngắn gọn và dễ xác minh. Những đặc tính này, cộng với khả năng tận dụng triệt để các đặc điểm phân cấp thông qua cấu trúc tháp, khiến miền nhị phân đặc biệt phù hợp cho các hệ thống chứng minh có thể mở rộng như Binius.
Trong đó, "canonical" đề cập đến cách thức biểu diễn duy nhất và trực tiếp của các phần tử trong miền nhị phân. Ví dụ, trong miền nhị phân cơ bản F2, bất kỳ chuỗi k bit nào cũng có thể được ánh xạ trực tiếp thành một phần tử miền nhị phân k bit. Điều này khác với miền số nguyên tố, miền số nguyên tố không thể cung cấp cách biểu diễn chuẩn như vậy trong một số bit nhất định. Mặc dù miền số nguyên tố 32 bit có thể chứa trong 32 bit, nhưng không phải mỗi chuỗi 32 bit đều có thể tương ứng duy nhất với một phần tử miền, trong khi miền nhị phân lại có sự thuận lợi của ánh xạ một-một này. Trong miền số nguyên tố Fp, các phương pháp giảm phổ biến bao gồm giảm Barrett, giảm Montgomery, và các phương pháp giảm đặc biệt cho các miền hữu hạn cụ thể như Mersenne-31 hoặc Goldilocks-64. Trong miền nhị phân F2k, các phương pháp giảm thường được sử dụng bao gồm giảm đặc biệt ( như trong AES sử dụng ), giảm Montgomery ( như trong POLYVAL sử dụng ) và giảm đệ quy ( như Tower ). Bài báo "Khám Phá Không Gian Thiết Kế của So Sánh Trường Số Nguyên Tố và Trường Nhị Phân ECC-Hardware Implementations" chỉ ra rằng, miền nhị phân không cần phải đưa vào carry trong các phép toán cộng và nhân, và phép toán bình phương của miền nhị phân rất hiệu quả, vì nó tuân theo quy tắc đơn giản (X + Y )2 = X2 + Y2.
Như hình 1 cho thấy, một chuỗi 128 bit: Chuỗi này có thể được giải thích theo nhiều cách trong ngữ cảnh của miền nhị phân. Nó có thể được coi là một phần tử duy nhất trong miền nhị phân 128 bit, hoặc được phân tích thành hai phần tử miền tháp 64 bit, bốn phần tử miền tháp 32 bit, mười sáu phần tử miền tháp 8 bit, hoặc 128 phần tử miền F2. Sự linh hoạt trong cách biểu diễn này không yêu cầu bất kỳ chi phí tính toán nào, chỉ là chuyển đổi kiểu chuỗi bit (typecast), là một thuộc tính rất thú vị và hữu ích. Đồng thời, các phần tử miền nhỏ có thể được gói lại thành các phần tử miền lớn hơn mà không cần chi phí tính toán bổ sung. Giao thức Binius đã tận dụng đặc điểm này để nâng cao hiệu quả tính toán. Hơn nữa, tài liệu "On Efficient Inversion in Tower Fields of Characteristic Two" đã khám phá độ phức tạp tính toán của phép nhân, bình phương và phép nghịch đảo trong miền tháp nhị phân n bit ( có thể phân tích thành miền con m bit ).
2.2 PIOP: Phiên bản cải biên của sản phẩm HyperPlonk và Kiểm tra hoán vị------Áp dụng cho trường nhị phân
Thiết kế PIOP trong giao thức Binius đã mượn ý tưởng từ HyperPlonk, áp dụng một loạt các cơ chế kiểm tra cốt lõi, được sử dụng để xác minh tính chính xác của đa thức và tập hợp đa biến. Những kiểm tra cốt lõi này bao gồm:
GateCheck: Xác minh chứng nhận bảo mật ω và đầu vào công khai x có thỏa mãn quan hệ toán tử của mạch C(x, ω)=0, để đảm bảo mạch hoạt động chính xác.
PermutationCheck: Xác thực kết quả đánh giá của hai đa thức nhiều biến f và g trên hypercube Boole là quan hệ hoán vị f(x) = f(π(x)), để đảm bảo tính nhất quán của sự sắp xếp giữa các biến đa thức.
LookupCheck: Kiểm tra xem giá trị của đa thức có nằm trong bảng tra cứu đã cho hay không, tức là f(Bµ) ⊆ T(Bµ), đảm bảo một số giá trị nằm trong khoảng đã chỉ định.
MultisetCheck: Kiểm tra xem hai tập hợp đa biến có bằng nhau hay không, tức là {(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H, đảm bảo tính nhất quán giữa nhiều tập hợp.
ProductCheck: Kiểm tra xem việc đánh giá đa thức hợp lý trên siêu lập phương Bool có bằng một giá trị đã tuyên bố nào đó ∏x∈Hµ f(x) = s, để đảm bảo tính chính xác của tích đa thức.
ZeroCheck: Xác minh một đa thức nhiều biến trên siêu khối Boolean tại bất kỳ điểm nào có phải là không ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, để đảm bảo phân bố của các điểm không của đa thức.
SumCheck: Kiểm tra xem tổng của đa thức nhiều biến có bằng giá trị đã khai báo hay không ∑x∈Hµ f(x) = s. Bằng cách chuyển đổi bài toán đánh giá đa thức nhiều biến thành bài toán đánh giá đa thức một biến, giảm độ phức tạp tính toán của bên xác minh. Ngoài ra, SumCheck còn cho phép xử lý hàng loạt, bằng cách giới thiệu số ngẫu nhiên, xây dựng tổ hợp tuyến tính để thực hiện xử lý hàng loạt cho nhiều trường hợp kiểm tra tổng.
BatchCheck: Dựa trên SumCheck, xác minh tính chính xác của việc đánh giá nhiều đa thức nhiều biến để nâng cao hiệu quả của giao thức.
Mặc dù Binius và HyperPlonk có nhiều điểm tương đồng trong thiết kế giao thức, nhưng Binius đã cải tiến ở 3 điểm sau:
Tối ưu hóa ProductCheck: Trong HyperPlonk, ProductCheck yêu cầu mẫu số U không được bằng 0 ở mọi điểm trên khối siêu lập phương, và tích phải bằng một giá trị cụ thể; Binius đã đơn giản hóa quy trình kiểm tra này bằng cách đặc trưng giá trị đó thành 1, từ đó giảm độ phức tạp tính toán.
Xử lý vấn đề chia cho zero: HyperPlonk không xử lý đầy đủ tình huống chia cho zero, dẫn đến không thể khẳng định rằng U không bằng không trên hypercube; Binius đã xử lý đúng vấn đề này, ngay cả khi mẫu số bằng zero, ProductCheck của Binius vẫn có thể tiếp tục xử lý, cho phép mở rộng đến bất kỳ giá trị tích nào.
Kiểm tra hoán vị giữa các cột: HyperPlonk không có tính năng này; Binius hỗ trợ kiểm tra hoán vị giữa nhiều cột, điều này cho phép Binius xử lý các trường hợp sắp xếp đa thức phức tạp hơn.
Do đó, Binius đã cải tiến cơ chế PIOPSumCheck hiện có, nâng cao tính linh hoạt và hiệu quả của giao thức, đặc biệt là trong việc xử lý xác minh đa thức đa biến phức tạp hơn, cung cấp hỗ trợ chức năng mạnh mẽ hơn. Những cải tiến này không chỉ giải quyết những hạn chế trong HyperPlonk, mà còn cho những điều chưa...