Nghiên cứu Bitlayer: Phân tích nguyên tắc và suy nghĩ tối ưu hóa của Binius STARK

Tiêu đề gốc: Phân tích và tối ưu hóa Binius STARKs
Tác giả gốc: mutourend & lynndell, Bitlayer Labs

1 Giới thiệu

Khác với SNARK dựa trên đường cong elip, STARK có thể được coi là SNARK dựa trên hàm băm. Một trong những lý do chính khiến STARK hiện không hiệu quả là hầu hết các giá trị trong các chương trình thực đều nhỏ, chẳng hạn như chỉ mục, giá trị đúng và sai, bộ đếm, v.v. trong vòng lặp for. Tuy nhiên, để đảm bảo tính bảo mật cho các bằng chứng dựa trên cây Merkle, khi dữ liệu được mở rộng bằng mã hóa Reed-Solomon, nhiều giá trị dư thừa bổ sung sẽ chiếm toàn bộ miền, ngay cả khi bản thân các giá trị ban đầu rất nhỏ. Để giải quyết vấn đề này, việc giảm kích thước tên miền trở thành một chiến lược quan trọng.

Như được hiển thị trong Bảng 1, độ rộng bit mã hóa của STARK thế hệ thứ nhất là 252 bit, độ rộng bit mã hóa của STARK thế hệ thứ hai là 64 bit và độ rộng bit mã hóa của STARK thế hệ thứ ba là 32 bit, nhưng vẫn còn rất nhiều không gian bị lãng phí trong độ rộng bit mã hóa 32 bit. Để so sánh, miền nhị phân cho phép thao tác trực tiếp với các bit, mã hóa nhỏ gọn và hiệu quả mà không lãng phí không gian, tức là STARK thế hệ thứ 4.

Bảng 1: Đường dẫn xuất STARKs

So với các trường hữu hạn được phát hiện bởi các nghiên cứu mới trong những năm gần đây như Goldilocks, BabyBear, Mersenne31, v.v., nghiên cứu về trường nhị phân có thể bắt nguồn từ những năm 1980. Hiện nay, miền nhị phân đã được sử dụng rộng rãi trong mật mã. Cá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 Tên miền F28;

· Mã xác thực tin nhắn Galois (GMAC), dựa trên tên miền F2128;

· Mã QR, sử dụng mã hóa Reed-Solomon dựa trên F28;

· Bản gốc FRI và Giao thức zk-STARK, cũng như hàm băm Grøstl cuối cùng của SHA-3, dựa trên miền F28 và là thuật toán băm rất phù hợp cho đệ quy.

Khi sử dụng tên miền nhỏ hơn, hoạt động mở rộng tên miền ngày càng trở nên quan trọng để đảm bảo an ninh. Miền nhị phân được Binius sử dụng hoàn toàn dựa vào các miền mở rộng để đảm bảo tính bảo mật và khả năng sử dụng thực tế của nó. Các đa thức liên quan đến hầu hết các phép tính của Prover không cần nhập miền mở rộng mà chỉ hoạt động trong miền cơ sở nên đạt hiệu quả cao trong các 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 đi sâu hơn vào các phần mở rộng lớn hơn để đảm bảo tính bảo mật 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ó hai vấn đề thực tế: khi tính toán biểu diễn dấu vết trong STARK, kích thước miền được sử dụng phải lớn hơn thứ tự của đa thức; Khi chuyển sang cây Merkle, cần phải mã hóa Reed-Solomon và kích thước miền được sử dụng phải lớn hơn kích thước sau khi mở rộng mã hóa.

Binius đề xuất một giải pháp đổi mới có thể xử lý hai vấn đề này một cách riêng biệt và thực hiện điều đó bằng cách biểu diễn cùng một dữ liệu theo hai cách khác nhau: thứ nhất, Sử dụng đa biến (cụ thể là đa biến). -tuyến tính) đa thức thay vì đa thức một biến để biểu diễn toàn bộ quỹ đạo tính toán thông qua các giá trị của nó trên "siêu khối" thứ hai, vì chiều dài của mỗi chiều của siêu khối là 2 nên không thể thực hiện tiêu chuẩn Khai triển Reed-Solomon giống như STARK, nhưng có thể coi siêu lập phương là một hình vuông và thực hiện khai triển Reed-Solomon dựa trên hình vuông này. Phương pháp này cải thiện đáng kể hiệu quả mã hóa và hiệu suất tính toán trong khi vẫn đảm bảo tính bảo mật.

2 Phân tích nguyên tắc

Việc xây dựng hầu hết các hệ thống SNARK hiện nay thường bao gồm hai phần sau :

· Chứng minh Oracle tương tác đa thức lý thuyết thông tin (PIOP):PIOP là cốt lõi của hệ thống chứng minh, chuyển đổi phép tính đầu vào mối quan hệ thành một phương trình đa thức có thể kiểm chứng được. Các giao thức PIOP khác nhau cho phép người chứng minh gửi dần dần các đa thức thông qua tương tác với người xác minh, để người xác minh có thể xác minh xem phép tính có đúng hay không bằng cách truy vấn kết quả đánh giá của một số lượng nhỏ đa thức. Các giao thức PIOP hiện tại bao gồm: PLONK PIOP, Spartan PIOP và HyperPlonk PIOP, v.v. Mỗi giao thức xử lý các biểu thức đa thức khác nhau, do đó ảnh hưởng đến hiệu suất và hiệu quả của toàn bộ hệ thống SNARK.

·Chế độ cam kết đa thức (PCS):Lược đồ cam kết đa thức được sử dụng để chứng minh liệu phương trình đa thức do PIOP tạo ra có đúng hay không. PCS là một công cụ mật mã cho phép người chứng minh cam kết với một đa thức và sau đó xác minh việc đánh giá đa thức đó, đồng thời ẩn các thông tin khác về đa thức đó. Các sơ đồ 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, bảo mật và các tình huống áp dụng khác nhau.

Theo nhu cầu cụ thể, bằng cách chọn các PIOP và PCS khác nhau và kết hợp chúng với các trường hữu hạn hoặc đường cong elip thích hợp, có thể xây dựng các hệ thống chứng minh với các tính chất khác nhau. Ví dụ:

à   Halo2: Được cung cấp bởi PLONK PIOP kết hợp với Bulletproofs PCS và dựa trên các đường cong Pasta. Halo2 được thiết kế tập trung vào khả năng mở rộng và loại bỏ thiết lập đáng tin cậy khỏi giao thức ZCash.

→   Plonky2: Sử dụng PLONK PIOP kết hợp với FRI PCS và dựa trên miền Goldilocks. Plonky2 được thiết kế để đạt được đệ quy hiệu quả. Khi thiết kế các hệ thống này, PIOP và PCS được chọn phải khớp với các trường 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. Việc lựa chọn các kết hợp này không chỉ ảnh hưởng đến kích thước bằng chứng và hiệu quả xác minh của SNARK mà còn xác định liệu hệ thống có thể đạt được tính minh bạch mà không cần cài đặt đáng tin cậy hay không và liệu nó có thể hỗ trợ các chức năng mở rộng như bằng chứng đệ quy hoặc bằng chứng tổng hợp hay không.

Binius: HyperPlonk PIOP + Brakedown PCS + Tên miền nhị phân. Cụ thể, Binius bao gồm năm công nghệ chính để đạt được hiệu quả và tính bảo mật. Đầu tiên, số học dựa trên tháp của các trường nhị phân tạo thành cơ sở 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 các trường nhị phân. Thứ hai, Binius đã điều chỉnh sản phẩm HyperPlonk và kiểm tra hoán vị trong Giao thức chứng minh Oracle tương tác (PIOP) để đảm bảo kiểm tra tính nhất quán an toàn và hiệu quả giữa các biến và hoán vị của chúng. Thứ ba, giao thức giới thiệu mộtđối số dịch chuyển đa tuyến tính mới, giúp tối ưu hóa hiệu quả của việc xác minh mối quan hệ đa tuyến tính trên các miền nhỏ. Thứ tư, Binius sử dụng phiên bản cải tiến của Đối số tra cứu Lasso, mang lại tính linh hoạt và bảo mật mạnh mẽ cho cơ chế tra cứu. Cuối cùng, giao thức sử dụng Lược đồ cam kết đa thức trường nhỏ (PCS trường nhỏ), cho phép nó triển khai hệ thống chứng minh hiệu quả trên miền nhị phân và giảm chi phí thường liên quan đến các miền lớn.

2.1 Trường hữu hạn: số học dựa trên tháp trường nhị phân

Trường nhị phân dạng tháp là chìa khóa để đạt được khả năng tính toán nhanh và có thể kiểm chứng, chủ yếu nhờ vào hai khía cạnh: tính toán hiệu quả và số học hiệu quả. Miền nhị phân vốn đã hỗ trợ các phép tính số học hiệu quả cao, khiến nó trở nên lý tưởng cho các ứng dụng mật mã nhạy cảm với các yêu cầu về hiệu suất. Hơn nữa, cấu trúc trường nhị phân hỗ trợ quy trình số học đơn giản hóa, tức là các phép toán được thực hiện trên trường nhị phân có thể được biểu diễn dưới dạng đại số nhỏ gọn và dễ kiểm chứng. Những đặc tính này, cùng với khả năng khai thác triệt để bản chất phân cấp của nó thông qua cấu trúc tháp, làm cho miền nhị phân đặc biệt phù hợp với các hệ thống chứng minh có thể mở rộng như Binius.

Trong đó "chuẩn" đề cập đến phần tử duy nhất và trực tiếp trong miền nhị phân cách diễn đạt. Ví dụ, trong trường nhị phân cơ bản nhất F2, bất kỳ chuỗi k-bit nào cũng có thể được ánh xạ trực tiếp tới phần tử trường nhị phân k-bit. Điều này không giống như trường nguyên tố, không thể cung cấp biểu diễn chuẩn như vậy trong một chữ số nhất định. Mặc dù trường nguyên tố 32 bit có thể được chứa trong 32 bit, nhưng không phải mọi chuỗi 32 bit đều tương ứng duy nhất với một phần tử trường và các trường nhị phân có sự tiện lợi của ánh xạ một-một này. Trong trường nguyên tố Fp, các phương pháp rút gọn phổ biến bao gồm rút gọn Brút gọn arrett, rút gọn Montgomery và các phương pháp đặc biệt dành cho các trường hữu hạn cụ thể nhưPhương pháp rút gọn Mersenne-31 hoặc Goldilocks-64 . Trong miền nhị phân F2k, các phương pháp rút gọn thường được sử dụng bao gồmGiảm đặc biệt (như được sử dụng trong AES), rút gọn Montgomery (như được sử dụng trong POLYVAL) và rút gọn đệ quy (như được sử dụng trong Tower). Bài báo "Khám phá không gian thiết kế của trường chính so với việc triển khai phần cứng ECC-trường nhị phân" chỉ ra rằng trường nhị phân không cần đưa vào các phép toán cộng và nhân, và phép toán bình phương của trường nhị phân rất hiệu quả vì nó tuân theo (X + Y) Quy tắc đơn giản hóa cho 2 = X2 + Y 2.

Như được hiển thị trong Hình 1, chuỗi 128 bit: Chuỗi này có thể được diễn giải theo nhiều cách khác nhau 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 trường nhị phân 128 bit hoặc được phân tích thành hai phần tử trường tháp 64 bit, bốn phần tử trường tháp 32 bit, 16 phần tử trường tháp 8 bit hoặc 128 phần tử trường F2. Tính linh hoạt của việc biểu diễn này, không yêu cầu bất kỳ chi phí tính toán nào ngoài việc định kiểu thành chuỗi bit, 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 đóng gói thành các phần tử miền lớn hơn mà không cần thêm chi phí tính toán. Giao thức Binius tận dụng tính năng này để cải thiện hiệu quả tính toán. Ngoài ra, bài viết "Về nghịch đảo hiệu quả trong các trường tháp có đặc tính hai" khám phá độ phức tạp tính toán của các phép nhân, bình phương và đảo ngược trong các trường nhị phân của tháp n-bit (có thể phân tách thành các trường con m-bit).

Hình 1: Miền nhị phân dạng tháp

2.2 PIOP: Sản phẩm HyperPlonk được điều chỉnh và PermutationCheck - dành cho miền nhị phân

Thiết kế PIOP trong giao thức Binius dựa trên HyperPlonk và áp dụng một loạt cơ chế kiểm tra cốt lõi để xác minh tính chính xác của đa thức và tập hợp nhiều biến. Các bước kiểm tra cốt lõi này bao gồm:

1.GateCheck:Xác minh xem nhân chứng bí mật ω và đầu vào công khai x có đáp ứng mối quan hệ vận hành mạch C hay không (x, ω)=0 để đảm bảo mạch hoạt động chính xác.

2.PermutationCheck:Xác minh xem kết quả đánh giá của hai đa thức đa biến f và g trên siêu khối Boolean có phải là quan hệ hoán vị f(x ) = f(π(x)) để đảm bảo sự sắp xếp nhất quán giữa các biến đa thức.

3.LookupCheck:Xác minh xem kết quả đánh giá 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 rằng các giá trị nhất định nằm trong phạm vi được chỉ định.

4.MultisetCheck: Kiểm tra xem hai tập hợp nhiều 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 bộ.

5. Kiểm tra sản phẩm: Phát hiện xem việc đánh giá đa thức hữu tỉ trên siêu khối Boolean có bằng một giá trị được khai báo nhất định hay không ∏x∈ Hµ f(x) = s để đảm bảo rằng tích đa thức là đúng.

6.ZeroCheck:Xác minh xem một đa thức nhiều biến có bằng 0 tại bất kỳ điểm nào trên siêu khối Boolean ∏x∈Hµ f( x) = 0,∀x ∈ Bµ để đảm bảo phân bố các số 0 của đa thức.

7.SumCheck:Kiểm tra xem giá trị tổng của đa thức nhiều biến có phải là giá trị khai báo ∑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 đánh giá đa thức một biến, độ phức tạp tính toán của trình xác minh sẽ giảm đi. Ngoài ra, SumCheck còn cho phép xử lý hàng loạt, bằng cách đưa ra các số ngẫu nhiên và xây dựng các tổ hợp tuyến tính để thực hiện xử lý hàng loạt nhiều trường hợp kiểm tra tổng.

8.BatchCheck:Dựa trên SumCheck, xác minh tính chính xác của nhiều đánh giá đa thức nhiều biến để cải thiện 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ó những cải tiến ở ba khía cạnh sau:

· Tối ưu hóa ProductCheck:Trong HyperPlonk, ProductCheck yêu cầu mẫu số U khác 0 ở mọi nơi trên hypercube và sản phẩm phải bằng một giá trị cụ thể Binius chuyên hóa giá trị này; được thay đổi thành 1 để đơn giản hóa quá trình kiểm tra, do đó giảm độ phức tạp tính toán.

· Xử lý vấn đề chia cho 0: HyperPlonk không giải quyết thỏa đáng tình huống chia cho 0, dẫn đến không thể khẳng định rằng U khác 0 trên siêu khối. Bài toán số 0 Binius xử lý vấn đề này một cách chính xác và ProductCheck của Binius tiếp tục xử lý ngay cả khi mẫu số bằng 0, cho phép khái quát hóa thành các giá trị tích tùy ý.

· PermutationCheck trên nhiều cột: HyperPlonk không có tính năng này; Binius hỗ trợ PermutationCheck trên nhiều cột, cho phép Binius xử lý Thêm hoán vị đa thức phức tạp.

Do đó, Binius cải thiện tính linh hoạt và hiệu quả của giao thức bằng cách cải thiện cơ chế PIOPSumCheck hiện có, đặc biệt khi xử lý xác minh đa thức đa biến phức tạp hơn. Cung cấp chức năng mạnh mẽ hơn. ủng hộ. Những cải tiến này không chỉ giải quyết các hạn chế trong HyperPlonk mà còn đặt nền tảng cho các hệ thống chứng minh trong tương lai dựa trên miền nhị phân.

2.3 PIOP: Đối số dịch chuyển đa tuyến tính mới - cho siêu khối boolean

Trong Binius Trong giao thức , việc xây dựng và xử lý đa thức ảo là một trong những công nghệ then chốt, có thể tạo và vận hành hiệu quả các đa thức rút ra từ các thẻ điều khiển đầu vào hoặc các đa thức ảo khác. Sau đây là hai phương pháp chính:

· Đóng gói: Phương pháp này hoạt động bằng cách đóng gói các phần tử nhỏ hơn ở các vị trí liền kề theo thứ tự từ điển thành các phần tử lớn hơn để tối ưu hóa hoạt động. Toán tử Pack hoạt động trên các khối có kích thước 2κ và kết hợp chúng thành một phần tử duy nhất trong miền nhiều chiều. Thông qua Mở rộng đa tuyến tính (MLE), đa thức ảo này có thể được đánh giá và xử lý một cách hiệu quả, chuyển đổi hàm t thành đa thức khác, do đó cải thiện hiệu suất tính toán.

· Toán tử dịch chuyển:Toán tử dịch chuyển sắp xếp lại các phần tử trong một khối, thực hiện dịch chuyển vòng dựa trên độ lệch cho trước o. Phương pháp này hoạt động trên các khối có kích thước 2b, với mỗi khối thực hiện dịch chuyển dựa trên độ lệch. Toán tử dịch chuyển được xác định bằng cách phát hiện sự hỗ trợ cho các hàm, đảm bảo tính nhất quán và hiệu quả khi làm việc với đa thức ảo. Độ phức tạp của việc đánh giá cấu trúc này tăng tuyến tính theo kích thước khối, khiến nó đặc biệt phù hợp để xử lý các tập dữ liệu lớn hoặc các kịch bản nhiều chiều trong siêu khối Boolean.

2.4 PIOP: Đối số tra cứu Lasso thích ứng - phù hợp với miền nhị phân

Giao thức Lasso Người chứng minh được phép cam kết với một vectơ a ∈ Fm và chứng minh rằng tất cả các phần tử của nó tồn tại trong một danh sách xác định trước t ∈ Fn. Lasso mở ra khái niệm "tra cứu điểm kỳ dị" và có thể được áp dụng cho các sơ đồ cam kết đa thức đa tuyến tính. Hiệu quả của nó được thể hiện ở hai khía cạnh sau:

· Hiệu quả chứng minh:Đối với m tra cứu trong bảng có kích thước n, hãy chứng minh The bên chỉ cần cam kết với các thành phần miền m+n. Các phần tử miền này có kích thước nhỏ và nằm trong tập {0,...,m}. Trong sơ đồ cam kết dựa trên nhiều phép toán lũy thừa, chi phí tính toán của phép chứng minh là các phép toán nhóm con O(m + n) (chẳng hạn như phép cộng điểm trên đường cong elip), cộng với việc chứng minh xem đa thức đa tuyến có phải là một phần tử bảng trên giá trị siêu khối Boolean hay không. chi phí.

· Không cần commit các bảng lớn: Nếu bảng t đã có cấu trúc thì không cần commit các bảng lớn, vì vậy rất lớn các bảng có thể được xử lý (ví dụ 2128 hoặc lớn hơn). Thời gian chạy của bộ chứng minh chỉ liên quan đến các mục trong bảng được truy cập. Đối với bất kỳ đối số nguyên c > 1, chi phí chính đối với người chứng minh là kích thước bằng chứng, cam kết các phần tử miền 3·c m + c·n1/c. Các phần tử miền này đều nhỏ và nằm trong tập {0,...,max{m,n1/c,q} − 1}, trong đó q là giá trị lớn nhất trong a.

Giao thức Lasso bao gồm ba thành phần sau:

· Bảng lớn Trừu tượng hóa đa thức ảo:Bằng cách kết hợp các đa thức ảo, các thao tác trên các bảng lớn được triển khai để đảm bảo tìm kiếm và xử lý hiệu quả trong bảng.

· Tra cứu bảng nhỏ: Cốt lõi của Lasso là tra cứu bảng nhỏ. Là cấu trúc cốt lõi của giao thức đa thức ảo, nó là. được xác minh bằng cách phát hiện bộ nhớ ngoại tuyến Liệu việc đánh giá một đa thức ảo trên siêu khối Boolean có phải là tập hợp con của việc đánh giá một đa thức ảo khác hay không. Quá trình tìm kiếm này được giảm xuống thành nhiệm vụ phát hiện nhiều tập hợp.

·Kiểm tra nhiều bộ:Lasso giới thiệu một giao thức ảo để thực hiện kiểm tra nhiều bộ, xác minh xem các phần tử của hai bộ có bằng nhau hay đáp ứng yêu cầu cụ thể hay không điều kiện.

Giao thức Binius điều chỉnh Lasso để hoạt động trên các trường nhị phân, giả sử rằng trường hiện tại là trường nguyên tố có đặc điểm lớn (lớn hơn nhiều so với độ dài của cột đang được nhìn lên). Binius giới thiệu một phiên bản nhân của giao thức Lasso, yêu cầu người chứng minh và người xác minh cùng tăng hoạt động "đếm bộ nhớ" của giao thức, không phải bằng cách tăng đơn giản thêm 1 mà bằng một trình tạo nhân trong miền nhị phân. Tuy nhiên, sự thích ứng nhân này gây ra độ phức tạp cao hơn, không giống như thao tác tăng, bộ tạo nhân không tăng trong mọi trường hợp, có một quỹ đạo duy nhất ở mức 0, có thể trở thành điểm tấn công. Để ngăn chặn cuộc tấn công tiềm ẩn này, người chứng minh phải cam kết một vectơ số lần đọc ở mọi nơi khác 0 để đảm bảo tính bảo mật của giao thức.

2.5 PCS: Bộ giảm tốc được điều chỉnh - thích hợp cho sân nhỏ

Xây dựng BiniusPCS Cốt lõi ý tưởng là bao bì. Bài viết Binius cung cấp hai sơ đồ cam kết đa thức Brakedown dựa trên miền nhị phân: một sơ đồ được khởi tạo bằng mã nối; sơ đồ kia sử dụng công nghệ mã hóa cấp khối để chỉ hỗ trợ việc sử dụng mã Reed-Solomon. Giải pháp Brakedown PCS thứ hai đơn giản hóa quá trình chứng minh và xác minh, tuy nhiên kích thước chứng minh lớn hơn một chút so với giải pháp đầu tiên, nhưng những lợi thế về đơn giản hóa và triển khai mà nó mang lại khiến cho sự đánh đổi này trở nên đáng giá.

Cam kết đa thức Binius chủ yếu sử dụng cam kết đa thức trường nhỏ và đánh giá trường mở rộng, xây dựng chung trường nhỏ và mã hóa cấp khối cũng như kỹ thuật mã Reed-Solomon.

Cam kết đa thức miền nhỏ và đánh giá miền mở rộng: Cam kết trong giao thức Binius là cam kết đa thức trên miền nhỏ K và trong Việc đánh giá được thực hiện trong miền mở rộng L/K lớn hơn. Cách tiếp cận này đảm bảo rằng mỗi đa thức đa tuyến tính t(X0,...,Xℓ−1) thuộc về miền K[X0,...,Xℓ−1], trong khi các điểm đánh giá có thể nằm trong miền mở rộng L lớn hơn. Sơ đồ cam kết được thiết kế đặc biệt để hoạt động với các đa thức miền nhỏ và cho phép truy vấn trên các miền mở rộng đồng thời đảm bảo tính bảo mật và hiệu quả của các cam kết.

Cấu trúc tổng quát của miền nhỏ: Cấu trúc tổng quát của miền nhỏ đảm bảo rằng bằng cách xác định tham số ℓ, miền K và mã khối tuyến tính liên quan của nó là C Miền mở rộng L đủ lớn để hỗ trợ đánh giá bảo mật. Để cải thiện tính bảo mật trong khi vẫn duy trì hiệu quả tính toán, giao thức đảm bảo tính chắc chắn của cam kết thông qua các thuộc tính của miền mở rộng và việc sử dụng mã khối tuyến tính để mã hóa đa thức.

Mã hóa cấp khối và mã Reed-Solomon: Đối với các đa thức có trường nhỏ hơn bảng chữ cái mã khối tuyến tính, Binius đã đề xuất sơ đồ mã hóa cấp khối . Với sơ đồ này, ngay cả các đa thức được xác định trong các trường nhỏ (như F2) cũng có thể được xác nhận một cách hiệu quả bằng cách sử dụng mã Reed-Solomon với bảng chữ cái lớn như F216. Mã Reed-Solomon được chọn vì tính hiệu quả và tính chất phân tách khoảng cách tối đa của nó. Giải pháp này đơn giản hóa độ phức tạp của hoạt động bằng cách đóng gói tin nhắn và mã hóa từng dòng một, sau đó sử dụng cây Merkle để cam kết. Mã hóa cấp khối cho phép cam kết hiệu quả các đa thức trong các miền nhỏ mà không phát sinh chi phí tính toán cao thường liên quan đến các miền lớn, giúp có thể cam kết đa thức trong các miền nhỏ như F2 và duy trì hiệu quả tính toán trong việc tạo bằng chứng và xác minh.

3 Ý tưởng tối ưu hóa

Để cải thiện hơn nữa hiệu suất của giao thức Binius, điều này bài viết đề xuất bốn điểm tối ưu hóa chính:

1. PIOP dựa trên GKR:Đối với các hoạt động nhân miền nhị phân, hãy sử dụng giao thức GKR để thay thế bài viết Binius Thuật toán Tra cứu Lasso có thể giảm đáng kể chi phí cam kết của Binius;

2. Tối ưu hóa ZeroCheck PIOP: Giữa Nhà cung cấp và Người xác minh. Thực hiện cân bằng chi phí tính toán để giúp hoạt động ZeroCheck hiệu quả hơn;

3.Tối ưu hóa Sumcheck PIOP:Tối ưu hóa Sumcheck cho các miền nhỏ để giảm thêm Giảm gánh nặng tính toán trên các miền nhỏ;

4 Tối ưu hóa PCS:Thông qua tối ưu hóa FRI-Binius, kích thước bằng chứng được giảm xuống. và hiệu suất giao thức được cải thiện.

3.1 PIOP dựa trên GKR: Phép nhân trường nhị phân dựa trên GKR

Giới thiệu bài báo Binius 1 Một sơ đồ dựa trên tra cứu được thiết kế để đạt được các phép nhân trường nhị phân hiệu quả. Thuật toán nhân trường nhị phân được điều chỉnh từ đối số tra cứu Lasso dựa trên mối quan hệ tuyến tính giữa tra cứu và các phép toán cộng tỷ lệ thuận với số nhánh trong một từ. Mặc dù thuật toán này tối ưu hóa các phép tính nhân ở một mức độ nào đó nhưng nó vẫn yêu cầu các cam kết phụ có liên quan tuyến tính với số nhánh.

Ý tưởng cốt lõi trong giao thức GKR (Goldwasser-Kalai-Rothblum) là người chứng minh (P) và người xác minh (V) tiếp cận mạch số học phân lớp trên trường hữu hạn F nhất quán. Mỗi nút của mạch này có hai đầu vào được sử dụng để tính toán hàm mong muốn. Để giảm độ phức tạp tính toán của trình xác minh, giao thức sử dụng giao thức SumCheck, giao thức này giảm dần các câu lệnh về các giá trị cổng đầu ra của mạch thành các câu lệnh giá trị cổng cấp thấp hơn, cho đến khi câu lệnh cuối cùng được giảm xuống thành các câu lệnh về đầu vào. Bằng cách này, người xác minh chỉ cần kiểm tra tính chính xác của đầu vào mạch.

Thuật toán nhân số nguyên dựa trên GKR chuyển đổi "kiểm tra xem hai số nguyên 32-bit A và B có thỏa mãn A·B =? C" thành "Kiểm tra xem (gA) )B =? gC được thiết lập", chi phí cam kết giảm đáng kể nhờ sự trợ giúp của giao thức GKR. So với sơ đồ tra cứu Binius trước đây, phép nhân trường nhị phân dựa trên GKR chỉ yêu cầu một lời hứa phụ và làm cho thuật toán hiệu quả hơn bằng cách giảm chi phí hoạt động của Sumchecks, đặc biệt là trong các trường hợp mà hoạt động của Sumchecks rẻ hơn so với việc tạo lời hứa. Với sự tiến bộ của tối ưu hóa Binius, các phép nhân dựa trên GKR đã dần trở thành một cách hiệu quả để giảm chi phí cam kết của đa thức trong miền nhị phân.

3.2 Tối ưu hóa ZeroCheck PIOP: Sự cân bằng chi phí tính toán giữa Prover và Verifier

Bài viết "Một số cải tiến cho PIOP cho ZeroCheck" điều chỉnh việc phân bổ khối lượng công việc giữa người chứng minh (P) và người xác minh (V) đồng thời đề xuất nhiều giải pháp tối ưu hóa khác nhau để cân nhắc chi phí. Công việc này khám phá các cấu hình giá trị k khác nhau nhằm đạt được sự cân bằng chi phí giữa người chứng minh và người xác minh, đặc biệt là về mặt giảm dữ liệu truyền tải và giảm độ phức tạp tính toán.

Giảm việc truyền dữ liệu của người chứng minh: Bằng cách chuyển một phần tác phẩm sang người xác minh V, từ đó giảm lượng dữ liệu được gửi của nhà tục ngữ P. Ở vòng thứ i, người chứng minh P cần gửi vi+1(X) đến người xác minh V, trong đó X=0,...,d + 1. Người xác minh V kiểm tra phương trình sau để xác minh tính chính xác của dữ liệu

vi = vi+1(0) + vi+1(1).

Phương pháp tối ưu hóa: Prover P có thể chọn không gửi vi+1(1) mà để verifier V tự tính giá trị theo cách sau

vi+1(1) = vi − vi+1(0).

Ngoài ra, ở vòng 0, người chứng minh trung thực P luôn gửi v1 (0) = v1(1) = 0, có nghĩa là không cần tính toán đánh giá, giảm đáng kể chi phí tính toán và truyền tải xuống d2n−1CF + (d + 1)2n−1CG.

Giảm số điểm đánh giá người chứng minh: Ở vòng thứ i của giao thức, người xác minh đã gửi ở vòng thứ i trước đó -round Thu được chuỗi giá trị r =(r0,...,ri−1). Giao thức hiện tại yêu cầu người chứng minh (P) gửi đa thức

vi+1(X) = ∑ δˆn(α,(r,X,x)) C(r , p>

vi(X) = vi′(X)·δi+1((α0,...,αi),(r,X))

Trong số đó δˆi+1 hoàn toàn được biết vì người xác minh sở hữu α và r. Lợi ích của việc sửa đổi này là vi′(X) có ít hơn vi(X) 1 bậc, có nghĩa là người chứng minh có ít điểm hơn để đánh giá. Do đó, những thay đổi giao thức chính đã xảy ra trong phiên kiểm tra giữa các vòng.

Ngoài ra, ràng buộc ban đầu vi = vi+1(0)+vi+1(1) được tối ưu hóa thành (1−αi)vi′+1 ( 0)+αivi′+1(1) = vi′(X). Sau đó, người hoạt động cần đánh giá và gửi ít dữ liệu hơn, tiếp tục giảm lượng dữ liệu được truyền đi. Tính toán δˆn−i−1 cũng hiệu quả hơn tính toán δˆn. Với hai cải tiến này, chi phí giảm xuống còn xấp xỉ: 2n−1(d− 1)CF + 2n−1dCG. Trong trường hợp chung d=3, những tối ưu hóa này giúp giảm chi phí xuống hệ số 5/3.

Tối ưu hóa nội suy đại số: Đối với một người chứng minh trung thực, C(x0,...,xn−1) trên Hn bằng 0, có thể được biểu diễn dưới dạng: C(x0,...,xn-1)= ∑xi(xi-1)Qi(x0,...,xn-1). Mặc dù Qi không phải là duy nhất, nhưng một phân rã có thứ tự có thể được xây dựng bằng phép chia dài đa thức: bắt đầu từ Rn=C, chia liên tiếp cho xi(xi−1) để tính Qi và Ri, trong đó R0 là đa tuyến tính của C trên Hn. Mở rộng và giả sử nó bằng không. Phân tích độ Khí, có thể kết luận rằng đối với j> độ Qj trên xi bằng C; đối với j = i thì độ giảm đi 2; nhất 1. Cho một vectơ r = (r0,...,ri), Qj(r,X) là đa tuyến với mọi j ≤ i. Hơn nữa 1)Qj(r,X) là đa thức đa tuyến duy nhất bằng C(r,X) trên Hn−i. Với mọi X và x ∈ Hn−i−1, nó có thể được biểu diễn dưới dạng:

C(r,X,x) − Qi(r,X,x) = X(X − 1)Qi+1(r,X,x)

Do đó, trong mỗi vòng của giao thức, chỉ một Q mới được đưa ra, giá trị đánh giá của nó có thể được tính từ C và Q trước đó, đạt được tối ưu hóa nội suy.

3.3 Tối ưu hóa Sumcheck PIOP: Giao thức Sumcheck dựa trên miền nhỏ

STARK được triển khai bởi sơ đồ Binius , chi phí cam kết của nó rất thấp, do đó điểm nghẽn của bộ chuẩn không còn là PCS nữa mà là giao thức kiểm tra tổng. Ingonyama đề xuất phương án cải tiến giao thức Sumcheck dựa trên các miền nhỏ vào năm 2024 (tương ứng với thuật toán Algo3 và Algo4 trong Hình 2), đồng thời mã nguồn mở triển khai. Thuật toán 4 tập trung vào việc kết hợp thuật toán Karatsub vào Thuật toán 3 để giảm thiểu số lượng phép nhân trường mở rộng với chi phí là các phép nhân trường cơ sở bổ sung, do đó, Thuật toán 4 hoạt động tốt hơn khi phép nhân trường mở rộng đắt hơn nhiều so với phép nhân trường cơ sở.

· Tác động và các yếu tố cải thiện của vòng chuyển đổi

Cải tiến giao thức Sumcheck dựa trên các miền nhỏ tập trung vào việc lựa chọn chuyển mạch vòng t. Vòng chuyển đổi đề cập đến thời điểm chuyển từ thuật toán tối ưu hóa về thuật toán đơn giản. Các thử nghiệm của bài báo cho thấy tại điểm chuyển đổi tối ưu, hệ số cải tiến đạt giá trị tối đa và sau đó thể hiện xu hướng parabol. Nếu vượt quá điểm chuyển đổi này, lợi thế về hiệu suất của thuật toán tối ưu hóa sẽ bị suy yếu và hiệu quả sẽ giảm. Điều này là do phép nhân trường cơ sở trên các trường nhỏ có tỷ lệ thời gian cao hơn so với phép nhân trường mở rộng, do đó điều quan trọng là phải chuyển về thuật toán đơn giản vào thời điểm thích hợp.

Hình 2: Mối quan hệ giữa các vòng chuyển đổi và các yếu tố cải tiến

Đối với các ứng dụng cụ thể, chẳng hạn như trường hợp liên quan đến Cubic Sumcheck (d = 3), sự cải tiến của giao thức Sumcheck dựa trên các miền nhỏ so với thuật toán đơn giản đã đạt đến mức độ lớn . Ví dụ: trong trường hợp miền cơ sở là GF[2], hiệu suất của Thuật toán 4 cao hơn gần 30 lần so với thuật toán đơn giản.

· Tác động của kích thước tên miền cơ sở đến hiệu suất

Bài báo Kết quả thực nghiệm cho thấy miền cơ sở nhỏ hơn (chẳng hạn như GF[2]) có thể làm cho thuật toán tối ưu hóa có nhiều ưu điểm đáng kể hơn. Điều này là do tỷ lệ thời gian của phép nhân miền mở rộng với phép nhân miền cơ sở cao hơn trên các miền cơ sở nhỏ hơn và do đó thuật toán tối ưu hóa thể hiện hệ số cải thiện cao hơn trong điều kiện này.

· Lợi ích tối ưu hóa của thuật toán Karatsuba

Thuật toán Karatsuba cải thiện hiệu suất dựa trên tên miền Sumcheck cho thấy kết quả đáng chú ý về mặt hiệu suất. Đối với miền cơ sở GF[2], hệ số cải thiện cao nhất của Thuật toán 3 và Thuật toán 4 lần lượt là 6 và 30, cho thấy Thuật toán 4 hiệu quả hơn Thuật toán 3 gấp 5 lần. Tối ưu hóa Karatsuba không chỉ nâng cao hiệu quả vận hành mà còn tối ưu hóa điểm chuyển đổi của thuật toán, đạt mức tốt nhất lần lượt là t=5 ở Thuật toán 3 và t=8 ở Thuật toán 4.

· Cải thiện hiệu quả bộ nhớ

Dựa trên các miền nhỏ Ngoài việc cải thiện thời gian chạy, giao thức Sumcheck còn cho thấy những ưu điểm đáng kể về hiệu quả bộ nhớ. Yêu cầu bộ nhớ của Thuật toán 4 là O(d·t), trong khi yêu cầu bộ nhớ của Thuật toán 3 là O(2d·t). Khi t=8, Thuật toán 4 chỉ cần 0,26 MB bộ nhớ, trong khi Thuật toán 3 yêu cầu 67 MB để lưu trữ tích của các trường cơ sở. Điều này làm cho Thuật toán 4 có khả năng thích ứng cao hơn trên các thiết bị có bộ nhớ hạn chế, đặc biệt phù hợp với môi trường kiểm chứng phía máy khách với nguồn lực hạn chế.

Tối ưu hóa 3.4 PCS: FRI-Binius giảm kích thước bằng chứng Binius

Một khía cạnh chính của Giao thức Binius Hạn chế là kích thước bằng chứng tương đối lớn của nó, tỷ lệ với căn bậc hai của kích thước nhân chứng là O(√N). Bằng chứng có kích thước căn bậc hai này là một hạn chế so với các hệ thống hiệu quả hơn. Ngược lại, kích thước bằng chứng đa logarit là rất quan trọng để đạt được trình xác nhận thực sự “đơn giản”, như đã được chứng minh trong các hệ thống tiên tiến như Plonky3, hệ thống triển khai bằng chứng logarit thông qua các kỹ thuật tiên tiến như FRI.

Bài báo "Chứng minh đa logarit cho đa tuyến tính trên tháp nhị phân", gọi tắt là FRI-Binius, thực hiện cơ chế gấp FRI miền nhị phân và mang lại sự đổi mới ở bốn khía cạnh:

· Đa thức phẳng: Các đa thức đa tuyến tính ban đầu được chuyển đổi thành các cơ sở đa thức mới LCH (Chiều cao mã thấp).

· Đa thức biến đổi không gian con: Được sử dụng để thực hiện FRI trên miền hệ số và đạt được kết quả tương tự thông qua phép phân tích NTT (biến đổi lý thuyết số) cộng của FFT.

· Đóng gói cơ sở đại số: Hỗ trợ đóng gói thông tin hiệu quả trong giao thức, có thể loại bỏ chi phí nhúng.

· SumCheck hoán đổi vòng: Một cách tiếp cận SumCheck mới tận dụng công nghệ hoán đổi vòng để tối ưu hóa hiệu suất.

Ý tưởng cốt lõi của sơ đồ cam kết đa thức đa tuyến tính (PCS) dựa trên miền nhị phân FRI-Binius là: giao thức FRI-Binius chuyển đổi miền nhị phân ban đầu đa thức đa tuyến tính vào (được xác định trên F2) được đóng gói để hoạt động như một đa thức đa tuyến tính được xác định trên miền K lớn hơn.

Trong FRI-BiniusPCS dựa trên miền nhị phân, quy trình như sau:

· Giai đoạn cam kết:Cam kết về đa thức đa tuyến tính của biến ℓ (được xác định trên F2) được chuyển thành cam kết về đa thức đa tuyến tính đóng gói của biến ℓ′ (được xác định trên F2128), với các hệ số The do đó số lượng giảm đi 128 lần.

· Giai đoạn đánh giá:Người chứng minh và người kiểm chứng thực hiện ℓ′ chuyển mạch vòng chéo SumCheck và bằng chứng tương tác FRI (IOPP):

–Bản in thử mở FRI chiếm phần lớn kích thước bản in thử.

–Chi phí SumCheck của người chứng minh tương tự như chi phí SumCheck trên một miền lớn thông thường.

–Chi phí FRI của người chứng minh bằng với chi phí FRI trên một miền lớn thông thường.

–Trình xác minh nhận 128 phần tử từ F2128 và thực hiện thêm 128 phép tính nhân.

Với FRI-Binius, kích thước bằng chứng của Binius có thể được giảm xuống một mức độ lớn. Điều này đưa kích thước bằng chứng của Binius đến gần hơn với các hệ thống tiên tiến nhất trong khi vẫn duy trì khả năng tương thích với miền nhị phân. Công nghệ gấp FRI được tùy chỉnh cho miền nhị phân, kết hợp với việc đóng gói đại số và tối ưu hóa SumCheck, cho phép Binius tạo ra các bằng chứng ngắn gọn hơn trong khi vẫn duy trì xác minh hiệu quả.

Bảng 2: Binius so với FRI-Binius Proof Size

Bảng 3: Plonky3 FRI so với FRI-Binius

4 Tóm tắt

Toàn bộ đề xuất giá trị của Binius là sử dụng sức mạnh hai miền nhỏ nhất cho nhân chứng, vì vậy chỉ cần chọn kích thước miền theo nhu cầu của bạn. Binius là một giải pháp đồng thiết kế "sử dụng phần cứng, phần mềm và giao thức Sumcheck được tăng tốc trong FPGA" có thể được chứng minh nhanh chóng với mức sử dụng bộ nhớ rất thấp. Các hệ thống chứng minh như Halo2 và Plonky3 có bốn bước chính đảm nhiệm hầu hết các phép tính: tạo dữ liệu nhân chứng, cam kết dữ liệu nhân chứng, biến mất lập luận và chống mở. Lấy Keccak trong Plonky3 và hàm băm Grøstl trong Binius làm ví dụ, tỷ lệ tính toán của bốn bước chính trên tương ứng với hai bước được thể hiện trong Hình 3:

Hình 3: Chi phí cam kết nhỏ hơn

Có thể thấy rằng Binius Nút thắt cam kết của Prover về cơ bản đã được loại bỏ hoàn toàn. Nút thắt cổ chai mới nằm ở giao thức Sumcheck. Các vấn đề như một số lượng lớn các đánh giá đa thức và phép nhân miền trong giao thức Sumcheck có thể được giải quyết một cách hiệu quả với sự trợ giúp của phần cứng chuyên dụng. Sơ đồ FRI-Binius, một biến thể của FRI, cung cấp một tùy chọn rất hấp dẫn - loại bỏ chi phí nhúng khỏi lớp chứng minh miền mà không làm phát sinh sự bùng nổ chi phí của lớp chứng minh tổng hợp. Hiện tại, nhóm Irreducible đang phát triển lớp đệ quy và công bố hợp tác với nhóm Polygon để xây dựng zkVM dựa trên Binius; JoltzkVM đang chuyển từ Lasso sang Binius để cải thiện hiệu suất đệ quy của nó và nhóm Ingonyama đang triển khai phiên bản FPGA của Binius.

Tài liệu tham khảo:

2024.04 Các lập luận ngắn gọn của Binius về Tháp trường nhị phân

2024.07 Bằng chứng đa giác Fri-Binius cho đa tuyến tính trên Tháp nhị phân

2024.08 Phép nhân số nguyên trong Binius: Cách tiếp cận dựa trên GKR

2024.06 zkStudyClub - FRI-Binius: Bằng chứng đa logarit cho đa tuyến tính trên tháp nhị phân

2024.04 ZK11 : Binius: SNARK được tối ưu hóa phần cứng - Jim Posen

2023.12 Tập 303: Đi sâu vào Binius với Ulvetanna

2024.09 Thiết kế zkVM hiệu suất cao

2024.07 Sumcheck và Open-Binius

2024.04 Binius: bằng chứng hiệu quả cao trên các trường nhị phân

2023.12 SNARK trên trường nhị phân: Binius - Phần 1

2024.06 SNARK trên trường nhị phân : Binius - Phần 2

2022.10 HyperPlonk, một hệ thống chống zk dành cho ZKEVM

Liên kết gốc