Phân tích nguyên lý Binius STARKs và suy nghĩ về tối ưu hóa
1 Giới thiệu
Khác với SNARKs dựa trên đường cong ellip, STARKs có thể được coi là SNARKs dựa trên băm. Hiện tại, một lý do chính khiến STARKs kém hiệu quả là: hầu hết các giá trị trong chương trình thực tế đều nhỏ, chẳng hạn như chỉ số vòng lặp, giá trị boolean, bộ đếm, v.v. Tuy nhiên, để đảm bảo tính an toàn của các chứng minh dựa trên cây Merkle, khi sử dụng mã Reed-Solomon để mở rộng dữ liệu, nhiều giá trị dư thừa 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, việc giảm kích thước miền trở thành chiến lược chủ chốt.
Kích thước mã hóa của STARKs thế hệ đầu tiên là 252 bit, thế hệ thứ hai là 64 bit, thế hệ thứ ba là 32 bit, nhưng mã hóa 32 bit vẫn có nhiều không gian lãng phí. So với điều đó, 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ẽ và hiệu quả mà không lãng phí, có thể được coi là STARKs thế hệ thứ tư.
So với các miền hữu hạn như Goldilocks, BabyBear, Mersenne31 được phát hiện trong những năm gần đây, nghiên cứu về miền nhị phân có thể được truy nguyên từ những năm 1980. Hiện nay, miền nhị phân đã được ứng dụng rộng rãi trong mật mã, chẳng hạn như miền AES(F28, miền GMAC)F2128, mã QR(F28 với mã hóa Reed-Solomon), v.v. Giao thức FRI gốc và zk-STARK, cũng như hàm băm Grøstl được chọn vào vòng chung kết SHA-3 cũng dựa trên miền F28.
Khi sử dụng miền nhỏ hơn, việc mở rộng miền ngày 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. Hầu hết các phép tính của Prover liên quan đến các đa thức chỉ cần thực hiện trên miền cơ sở, từ đó đạt được hiệu quả 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 được thực hiện trong 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ó hai vấn đề thực tiễn tồn tại:
Khi tính toán trace trong STARKs, kích thước miền sử dụng nên lớn hơn bậc của đa thức.
Trong cam kết Merkle tree của STARKs, cần thực hiện mã hóa Reed-Solomon, kích thước miền sử dụng nên lớn hơn kích thước sau khi mở rộng mã.
Binius đưa ra giải pháp đổi mới, xử lý hai vấn đề này:
Sử dụng đa biến ( đa tuyến tính ) đa thức thay thế cho đa thức đơn biến, thông qua giá trị của nó trên "siêu lập phương" để biểu diễn toàn bộ quỹ đạo tính toán.
Do chiều dài mỗi chiều của siêu lập phương là 2, 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ư một hình vuông, dựa trên hình vuông đó để thực hiện mở rộng Reed-Solomon.
Phương pháp này nâng cao hiệu quả mã hóa và hiệu suất tính toán một cách đáng kể trong khi vẫn đảm bảo tính bảo mật.
2 Phân tích nguyên lý
Hiện tại, hầu hết các hệ thống SNARKs thường bao gồm hai phần:
Chứng minh máy tiên tri tương tác đa thức lý thuyết thông tin ( PIOP ):
Làm hệ thống chứng minh cốt lõi, chuyển đổi các mố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. Thông qua việc tương tác với người xác minh, người chứng minh dần dần gửi đa thức, để người xác minh có thể xác minh độ chính xác của tính toán thông qua việc truy vấn một số lượng nhỏ các kết quả đa thức. Các giao thức PIOP hiện có bao gồm PLONK PIOP, Spartan PIOP và HyperPlonk PIOP.
Giải pháp cam kết đa thức (PCS):
Được sử dụng để chứng minh xem 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ã, 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 nó, trong khi ẩn thông tin khác của đa thức. Các PCS phổ biến bao gồm KZG, Bulletproofs, FRI và Brakedown.
Dựa trên nhu cầu, 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 elip 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:PLONK PIOP + Bulletproofs PCS + đường cong Pasta
Plonky2:PLONK PIOP + FRI PCS + miền Goldilocks
Binius: HyperPlonk PIOP + Brakedown PCS + 二进制域
Binius bao gồm năm công nghệ then chốt:
Cơ sở tính toán dựa trên miền nhị phân tháp: cấu thành nền tảng tính toán, thực hiện phép toán đơn giản trong miền nhị phân
Chỉnh sửa kiểm tra tích và hoán vị HyperPlonk: đảm bảo kiểm tra tính nhất quán hiệu quả giữa các biến và hoán vị
Chứng minh đa tuyến tính mới: Tối ưu hóa hiệu suất xác minh quan hệ đa tuyến tính trên miền nhỏ.
Cải tiến lập luận tìm kiếm Lasso: Cung cấp tính linh hoạt và an toàn cho cơ chế tìm kiếm.
Phương án cam kết đa thức nhỏ: Thực hiện hệ thống chứng minh hiệu quả trên trường nhị phân, giảm chi phí liên quan đến trường lớn.
( 2.1 Trường hữu hạn: Phép toán dựa trên tháp của các trường nhị phân
Miền nhị phân tháp là chìa khóa để thực hiện tính toán có thể xác minh nhanh chóng, chủ yếu nhờ vào tính toán hiệu quả và tính toán hóa hiệu quả. Miền nhị phân về cơ bản hỗ trợ các phép toán số học rất hiệu quả, 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 hiệu suất. Cấu trúc miền nhị phân hỗ trợ quy trình tính toán hóa đơn giản, 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 dễ xác minh. Những đặc điểm này cộng với khả năng tận dụng đầy đủ các đặc tính 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 với các hệ thống chứng minh có thể mở rộng như Binius.
"canonical" chỉ cách 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 đến các 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 nà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 có sự tiệ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 rút gọn phổ biến bao gồm rút gọn Barrett, rút gọn Montgomery, cũng như các phương pháp rút gọn đặ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 rút gọn thường dùng bao gồm rút gọn đặc biệt ) như AES sử dụng ###, rút gọn Montgomery ( như POLYVAL sử dụng ) và rút gọn đệ quy ( như Tower ).
Bài báo "Khám Phá Không Gian Thiết Kế của Các Triển Khai Phần Cứng ECC-Trường Số Nguyên So Với Trường Nhị Phân" chỉ ra rằng, trong trường nhị phân, không cần phải đưa vào phép cộng và phép nhân, và phép bình phương trong trường nhị phân rất hiệu quả, vì nó tuân theo quy tắc đơn giản (X + Y)2 = X2 + Y2.
Một chuỗi 128 bit có thể được giải thích theo nhiều cách trong ngữ cảnh 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. Tính linh hoạt trong biểu diễn này không cần bất kỳ chi phí tính toán nào, chỉ là chuyển đổi kiểu của 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 chi phí tính toán bổ sung. Giao thức Binius tận dụng đặc điểm này để cải thiện hiệu quả tính toán.
Bài báo "On Efficient Inversion in Tower Fields of Characteristic Two" đã thảo luận về độ phức tạp tính toán của phép nhân, phép bình phương và phép đảo ngược khi ( được phân rã thành trường con m-bit ) trong miền nhị phân tháp n-bit.
( 2.2 PIOP: Phiên bản cải biên HyperPlonk Product và PermutationCheck------Áp dụng cho trường nhị phân
Thiết kế PIOP trong giao thức Binius đã tham khảo HyperPlonk, sử 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:
GateCheck: xác thực chứng nhận bí mật ω và đầu vào công khai x có thỏa mãn quan hệ toán tử mạch C)x, ω###=0, đảm bảo mạch hoạt động đúng.
PermutationCheck: Xác minh xem kết quả đánh giá của hai đa thức nhiều biến f và g trên hypercube Boolean có phải là quan hệ hoán vị hay không f(x) = f(π)x((, đảm bảo sự nhất quán trong việc sắp xếp các biến đa thức.
LookupCheck: Xác minh 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 rằng một số giá trị nằm trong phạm vi chỉ định.
MultisetCheck: Kiểm tra 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 giá trị của đa thức hợp lý trên hypercube Boolean 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 biến đa thức tại bất kỳ điểm nào trên hypercube boolean có phải là không ∏x∈Hμ f(x) = 0, ∀x ∈ Bμ, đảm bảo phân bố đ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 vấn đề đánh giá đa thức nhiều biến thành đá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 đưa vào số ngẫu nhiên, xây dựng tổ hợp tuyến tính để xử lý hàng loạt 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 nhiều giá trị đa biến đa thức, nhằm 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 khía cạnh sau:
Tối ưu hóa ProductCheck: Trong HyperPlonk, ProductCheck yêu cầu mẫu số U phải khác không tại mọi điểm trên hypercube, 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 biệt hóa giá trị đó thành 1, giảm độ phức tạp tính toán.
Xử lý vấn đề chia cho số không: HyperPlonk không xử lý đầy đủ các trường hợp chia cho số không, dẫn đến không thể khẳng định U có khác không trên siêu lập phương; Binius đã xử lý đúng vấn đề này, ngay cả khi mẫu số là số không, 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ó chức năng này; Binius hỗ trợ kiểm tra hoán vị giữa nhiều cột, giúp Binius xử lý các tình huống sắp xếp đa thức phức tạp hơn.
Do đó, Binius đã cải tiến cơ chế PIOP SumCheck hiện có, nâng cao tính linh hoạt và hiệu quả của giao thức, đặc biệt trong việc xử lý xác minh đa biến đa thức 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 được những hạn chế trong HyperPlonk mà còn đặt nền tảng cho các hệ thống chứng minh dựa trên miền nhị phân trong tương lai.
( 2.3 PIOP: đối số dịch đa tuyến mới------ áp dụng cho hypercube boolean
Trong giao thức Binius, 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ó khả năng tạo ra và vận hành các đa thức phát sinh từ tay cầm đầu vào hoặc các đa thức ảo khác một cách hiệu quả. Dưới đây là hai phương pháp then chốt:
Packing: Phương pháp này tối ưu hóa các thao tác bằng cách đóng gói các phần tử nhỏ hơn ở vị trí liền kề trong thứ tự từ điển thành các phần tử lớn hơn. Toán tử Pack nhắm đến các thao tác trên khối có kích thước 2κ và kết hợp chúng thành một phần tử trong miền bậc cao. Thông qua mở rộng đa tuyến tính ) Multilinear Extension, MLE ###, đa thức ảo này có thể được đánh giá và xử lý hiệu quả, chuyển đổi hàm t thành một đa thức khác, từ đó 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 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 áp dụng cho các khối có kích thước 2b, 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 định nghĩa bằng cách kiểm tra sự hỗ trợ của hàm, đảm bảo tính nhất quán và hiệu quả khi xử lý đa thức ảo. Đánh giá độ phức tạp của cấu trúc này tăng theo kích thước khối theo chiều tuyến tính, đặc biệt thích hợp cho việc xử lý các tập dữ liệu lớn hoặc các cảnh đa chiều trong siêu khối Boole.
( 2.4 PIOP: Phiên bản sửa đổi của đối số tìm kiếm Lasso------Áp dụng cho miền nhị phân
Giao thức Lasso cho phép bên chứng minh cam kết một vector a ∈ Fm, và chứng minh rằng tất cả các phần tử của nó đều tồn tại trong một bảng đã chỉ định trước t ∈ Fn. Lasso đã mở khóa khái niệm "tìm kiếm điểm kỳ dị" )lookup singularities### và có thể áp dụng cho các phương án cam kết đa thức nhiều biến. Hiệu quả của nó thể hiện ở hai khía cạnh sau:
Hiệu suất chứng minh: Đối với m lần tìm kiếm trong bảng có kích thước n, bên chứng minh chỉ cần cam kết m+n phần tử miền. Những phần tử miền này rất nhỏ, đều nằm trong tập hợp {0,...,m}. Trong kế hoạch cam kết dựa trên phép lũy thừa nhiều lần, chi phí tính toán của bên chứng minh là O(m + n) phép toán nhóm( như
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.
13 thích
Phần thưởng
13
5
Đăng lại
Chia sẻ
Bình luận
0/400
NestedFox
· 08-12 10:22
Lại làm trò gì mới vậy, Hard Fork sao không nói rõ ra nhỉ?
Xem bản gốcTrả lời0
DeadTrades_Walking
· 08-10 16:37
Chơi nén miền đã bắt đầu rồi ha
Xem bản gốcTrả lời0
zkProofInThePudding
· 08-10 16:35
Không có khả năng gì, chỉ là lãng phí một chút không gian.
Binius: Tối ưu hóa và đổi mới STARKs dựa trên miền nhị phân
Phân tích nguyên lý Binius STARKs và suy nghĩ về tối ưu hóa
1 Giới thiệu
Khác với SNARKs dựa trên đường cong ellip, STARKs có thể được coi là SNARKs dựa trên băm. Hiện tại, một lý do chính khiến STARKs kém hiệu quả là: hầu hết các giá trị trong chương trình thực tế đều nhỏ, chẳng hạn như chỉ số vòng lặp, giá trị boolean, bộ đếm, v.v. Tuy nhiên, để đảm bảo tính an toàn của các chứng minh dựa trên cây Merkle, khi sử dụng mã Reed-Solomon để mở rộng dữ liệu, nhiều giá trị dư thừa 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, việc giảm kích thước miền trở thành chiến lược chủ chốt.
Kích thước mã hóa của STARKs thế hệ đầu tiên là 252 bit, thế hệ thứ hai là 64 bit, thế hệ thứ ba là 32 bit, nhưng mã hóa 32 bit vẫn có nhiều không gian lãng phí. So với điều đó, 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ẽ và hiệu quả mà không lãng phí, có thể được coi là STARKs thế hệ thứ tư.
So với các miền hữu hạn như Goldilocks, BabyBear, Mersenne31 được phát hiện trong những năm gần đây, nghiên cứu về miền nhị phân có thể được truy nguyên từ những năm 1980. Hiện nay, miền nhị phân đã được ứng dụng rộng rãi trong mật mã, chẳng hạn như miền AES(F28, miền GMAC)F2128, mã QR(F28 với mã hóa Reed-Solomon), v.v. Giao thức FRI gốc và zk-STARK, cũng như hàm băm Grøstl được chọn vào vòng chung kết SHA-3 cũng dựa trên miền F28.
Khi sử dụng miền nhỏ hơn, việc mở rộng miền ngày 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. Hầu hết các phép tính của Prover liên quan đến các đa thức chỉ cần thực hiện trên miền cơ sở, từ đó đạt được hiệu quả 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 được thực hiện trong 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ó hai vấn đề thực tiễn tồn tại:
Binius đưa ra giải pháp đổi mới, xử lý hai vấn đề này:
Phương pháp này nâng cao hiệu quả mã hóa và hiệu suất tính toán một cách đáng kể trong khi vẫn đảm bảo tính bảo mật.
2 Phân tích nguyên lý
Hiện tại, hầu hết các hệ thống SNARKs thường bao gồm hai phần:
Chứng minh máy tiên tri tương tác đa thức lý thuyết thông tin ( PIOP ): Làm hệ thống chứng minh cốt lõi, chuyển đổi các mố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. Thông qua việc tương tác với người xác minh, người chứng minh dần dần gửi đa thức, để người xác minh có thể xác minh độ chính xác của tính toán thông qua việc truy vấn một số lượng nhỏ các kết quả đa thức. Các giao thức PIOP hiện có bao gồm PLONK PIOP, Spartan PIOP và HyperPlonk PIOP.
Giải pháp cam kết đa thức (PCS): Được sử dụng để chứng minh xem 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ã, 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 nó, trong khi ẩn thông tin khác của đa thức. Các PCS phổ biến bao gồm KZG, Bulletproofs, FRI và Brakedown.
Dựa trên nhu cầu, 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 elip 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ụ:
Binius bao gồm năm công nghệ then chốt:
Cơ sở tính toán dựa trên miền nhị phân tháp: cấu thành nền tảng tính toán, thực hiện phép toán đơn giản trong miền nhị phân
Chỉnh sửa kiểm tra tích và hoán vị HyperPlonk: đảm bảo kiểm tra tính nhất quán hiệu quả giữa các biến và hoán vị
Chứng minh đa tuyến tính mới: Tối ưu hóa hiệu suất xác minh quan hệ đa tuyến tính trên miền nhỏ.
Cải tiến lập luận tìm kiếm Lasso: Cung cấp tính linh hoạt và an toàn cho cơ chế tìm kiếm.
Phương án cam kết đa thức nhỏ: Thực hiện hệ thống chứng minh hiệu quả trên trường nhị phân, giảm chi phí liên quan đến trường lớn.
( 2.1 Trường hữu hạn: Phép toán dựa trên tháp của các trường nhị phân
Miền nhị phân tháp là chìa khóa để thực hiện tính toán có thể xác minh nhanh chóng, chủ yếu nhờ vào tính toán hiệu quả và tính toán hóa hiệu quả. Miền nhị phân về cơ bản hỗ trợ các phép toán số học rất hiệu quả, 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 hiệu suất. Cấu trúc miền nhị phân hỗ trợ quy trình tính toán hóa đơn giản, 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 dễ xác minh. Những đặc điểm này cộng với khả năng tận dụng đầy đủ các đặc tính 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 với các hệ thống chứng minh có thể mở rộng như Binius.
"canonical" chỉ cách 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 đến các 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 nà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 có sự tiệ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 rút gọn phổ biến bao gồm rút gọn Barrett, rút gọn Montgomery, cũng như các phương pháp rút gọn đặ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 rút gọn thường dùng bao gồm rút gọn đặc biệt ) như AES sử dụng ###, rút gọn Montgomery ( như POLYVAL sử dụng ) và rút gọn đệ quy ( như Tower ).
Bài báo "Khám Phá Không Gian Thiết Kế của Các Triển Khai Phần Cứng ECC-Trường Số Nguyên So Với Trường Nhị Phân" chỉ ra rằng, trong trường nhị phân, không cần phải đưa vào phép cộng và phép nhân, và phép bình phương trong trường nhị phân rất hiệu quả, vì nó tuân theo quy tắc đơn giản (X + Y)2 = X2 + Y2.
Một chuỗi 128 bit có thể được giải thích theo nhiều cách trong ngữ cảnh 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. Tính linh hoạt trong biểu diễn này không cần bất kỳ chi phí tính toán nào, chỉ là chuyển đổi kiểu của 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 chi phí tính toán bổ sung. Giao thức Binius tận dụng đặc điểm này để cải thiện hiệu quả tính toán.
Bài báo "On Efficient Inversion in Tower Fields of Characteristic Two" đã thảo luận về độ phức tạp tính toán của phép nhân, phép bình phương và phép đảo ngược khi ( được phân rã thành trường con m-bit ) trong miền nhị phân tháp n-bit.
( 2.2 PIOP: Phiên bản cải biên HyperPlonk Product và PermutationCheck------Áp dụng cho trường nhị phân
Thiết kế PIOP trong giao thức Binius đã tham khảo HyperPlonk, sử 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:
GateCheck: xác thực chứng nhận bí mật ω và đầu vào công khai x có thỏa mãn quan hệ toán tử mạch C)x, ω###=0, đảm bảo mạch hoạt động đúng.
PermutationCheck: Xác minh xem kết quả đánh giá của hai đa thức nhiều biến f và g trên hypercube Boolean có phải là quan hệ hoán vị hay không f(x) = f(π)x((, đảm bảo sự nhất quán trong việc sắp xếp các biến đa thức.
LookupCheck: Xác minh 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 rằng một số giá trị nằm trong phạm vi chỉ định.
MultisetCheck: Kiểm tra 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 giá trị của đa thức hợp lý trên hypercube Boolean 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 biến đa thức tại bất kỳ điểm nào trên hypercube boolean có phải là không ∏x∈Hμ f(x) = 0, ∀x ∈ Bμ, đảm bảo phân bố đ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 vấn đề đánh giá đa thức nhiều biến thành đá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 đưa vào số ngẫu nhiên, xây dựng tổ hợp tuyến tính để xử lý hàng loạt 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 nhiều giá trị đa biến đa thức, nhằm 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 khía cạnh sau:
Tối ưu hóa ProductCheck: Trong HyperPlonk, ProductCheck yêu cầu mẫu số U phải khác không tại mọi điểm trên hypercube, 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 biệt hóa giá trị đó thành 1, giảm độ phức tạp tính toán.
Xử lý vấn đề chia cho số không: HyperPlonk không xử lý đầy đủ các trường hợp chia cho số không, dẫn đến không thể khẳng định U có khác không trên siêu lập phương; Binius đã xử lý đúng vấn đề này, ngay cả khi mẫu số là số không, 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ó chức năng này; Binius hỗ trợ kiểm tra hoán vị giữa nhiều cột, giúp Binius xử lý các tình huống sắp xếp đa thức phức tạp hơn.
Do đó, Binius đã cải tiến cơ chế PIOP SumCheck hiện có, nâng cao tính linh hoạt và hiệu quả của giao thức, đặc biệt trong việc xử lý xác minh đa biến đa thức 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 được những hạn chế trong HyperPlonk mà còn đặt nền tảng cho các hệ thống chứng minh dựa trên miền nhị phân trong tương lai.
( 2.3 PIOP: đối số dịch đa tuyến mới------ áp dụng cho hypercube boolean
Trong giao thức Binius, 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ó khả năng tạo ra và vận hành các đa thức phát sinh từ tay cầm đầu vào hoặc các đa thức ảo khác một cách hiệu quả. Dưới đây là hai phương pháp then chốt:
Packing: Phương pháp này tối ưu hóa các thao tác bằng cách đóng gói các phần tử nhỏ hơn ở vị trí liền kề trong thứ tự từ điển thành các phần tử lớn hơn. Toán tử Pack nhắm đến các thao tác trên khối có kích thước 2κ và kết hợp chúng thành một phần tử trong miền bậc cao. Thông qua mở rộng đa tuyến tính ) Multilinear Extension, MLE ###, đa thức ảo này có thể được đánh giá và xử lý hiệu quả, chuyển đổi hàm t thành một đa thức khác, từ đó 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 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 áp dụng cho các khối có kích thước 2b, 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 định nghĩa bằng cách kiểm tra sự hỗ trợ của hàm, đảm bảo tính nhất quán và hiệu quả khi xử lý đa thức ảo. Đánh giá độ phức tạp của cấu trúc này tăng theo kích thước khối theo chiều tuyến tính, đặc biệt thích hợp cho việc xử lý các tập dữ liệu lớn hoặc các cảnh đa chiều trong siêu khối Boole.
( 2.4 PIOP: Phiên bản sửa đổi của đối số tìm kiếm Lasso------Áp dụng cho miền nhị phân
Giao thức Lasso cho phép bên chứng minh cam kết một vector a ∈ Fm, và chứng minh rằng tất cả các phần tử của nó đều tồn tại trong một bảng đã chỉ định trước t ∈ Fn. Lasso đã mở khóa khái niệm "tìm kiếm điểm kỳ dị" )lookup singularities### và có thể áp dụng cho các phương án cam kết đa thức nhiều biến. Hiệu quả của nó thể hiện ở hai khía cạnh sau: