Phân tích nguyên lý Binius STARKs và những suy nghĩ tối ưu hóa
1. Giới thiệu
Khác với SNARKs dựa trên đường cong elip, STARKs có thể được coi là SNARKs dựa trên hàm băm. 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ị boolean, 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, việc sử dụng mã hóa Reed-Solomon để mở rộng dữ liệu sẽ tạo ra nhiều giá trị dư thừa bổ sung chiếm 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 quan trọng.
Thế hệ 1 STARKs có bề rộng mã 252bit, thế hệ 2 STARKs có bề rộng mã 64bit, thế hệ 3 STARKs có bề rộng mã 32bit, nhưng bề rộng mã 32bit vẫn còn 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 có không gian lãng phí nào, tức là thế hệ 4 STARKs.
So với Goldilocks, BabyBear, Mersenne31 và các phát hiện nghiên cứu gần đây về miền hữu hạn, nghiên cứu về miền nhị phân có thể được truy ngược tới thập niên 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 trường F28;
Mã xác thực thông điệp Galois ( GMAC ), dựa trên trường 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 như hàm băm Grøstl vào vòng 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 ngày càng quan trọng để đảm bảo tính bảo mật. 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 bảo mật và khả năng sử dụng thực tế. Hầu hết các đa thức liên quan trong các phép tính Prover không cần phải vào miền mở rộng, mà chỉ cần hoạt động trong miền cơ sở, do đó đạ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 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ó 2 vấn đề thực tế: Khi tính toán biểu diễ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 sáng tạo để xử lý hai vấn đề này một cách riêng biệt, và đạt được điều đó bằng cách biểu diễn cùng một dữ liệu theo hai cách khác nhau: đầu tiên, sử dụng đa biến ( cụ thể là đa thức nhiều tuyến tính ) 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" ( hypercubes ) để biểu diễn toàn bộ quỹ đạo tính toán; thứ hai, do chiều dài của mỗi chiều trong siêu lập phương đều bằng 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ể xem siêu lập phương như một hình vuông ( square ), và thực hiện mở rộng Reed-Solomon dựa trên hình vuông đó. 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 an toàn.
2. Phân tích nguyên lý
Hiện tại, hầu hết các hệ thống SNARKs được xây dựng 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 (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP): PIOP, như 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 qua sự tương tác với người xác minh, giúp người xác minh chỉ cần truy vấn kết quả đánh giá của một số ít đa thức để xác minh tính đúng đắn của phép tính. Các giao thức PIOP hiện có bao gồm: PLONK PIOP, Spartan PIOP và HyperPlonk PIOP, mỗi cái có cách xử lý khác nhau đối với biểu thức đa thức, 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 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ã, 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 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. Các PCS khác nhau có hiệu suất, tính bảo mật và các tình huống áp dụng 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 các miền hữu hạn hoặc đường cong elip phù hợp, có thể xây dựng các 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ế chú trọng đến khả năng mở rộng và loại bỏ thiết lập tin cậy trong giao thức ZCash.
• Plonky2: Kết hợp PLONK PIOP và FRI PCS, dựa trên miền Goldilocks. Plonky2 được thiết kế để đạt được tính tái diễn hiệu quả. Khi thiết kế các 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, nhằm đả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 tổ hợp này không chỉ ảnh hưởng đến kích thước chứng minh và hiệu quả xác minh của SNARK, 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à liệu có thể hỗ trợ chứng minh tái diễn hoặc chứng minh tổng hợp và các chức năng mở rộng khác.
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 suất và độ an toàn của nó. Đầu tiên, cấu trúc số học dựa trên tháp miền nhị phân (towers of binary fields) tạo thành nền tảng cho tính toán của nó, có khả năng thực hiện các phép toán đơn giản trong miền nhị phân. Thứ hai, Binius trong giao thức chứng nhận Oracle tương tác (PIOP) đã điều chỉnh kiểm tra sản phẩm và hoán vị HyperPlonk, đảm bảo tính nhất quán an toàn và hiệu quả giữa các biến và sự hoán vị của chúng. Thứ ba, giao thức giới thiệu một chứng nhận chuyển vị đa thức mới, tối ưu hóa hiệu suất xác minh các mối quan hệ đa thức trên miền nhỏ. Thứ tư, Binius áp dụng chứng nhận tìm kiếm Lasso cải tiến, mang lại tính linh hoạt và độ an toàn 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 nhận hiệu quả trên miền nhị phân và giảm thiểu 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 tháp của các trường nhị phân
Trường 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 hai yếu tố: tính toán hiệu quả và toán học hiệu quả. Trường nhị phân về bản chất hỗ trợ các phép toán toán học hiệu quả cao, 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 về hiệu suất. Hơn nữa, cấu trúc trường nhị phân hỗ trợ quá trình toán 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ố gọn gàng và 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 điểm phân cấp của nó thông qua cấu trúc tháp, khiến cho trường 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 biểu diễn duy nhất và trực tiếp của các yếu 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 một yếu tố miền nhị phân k bit. Điều này khác với miền số nguyên tố, nơi mà 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 yếu 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 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ư được sử dụng trong AES ), giảm Montgomery ( như trong POLYVAL ) và giảm đệ quy ( như Tower ). Bài báo "Khám Phá Không Gian Thiết Kế Của ECC-Hardware Implementations Trên Miền Số Nguyên Tố So Với Miền Nhị Phân" chỉ ra rằng miền nhị phân không cần phải đưa vào việc mang khi thực hiện các phép toán cộng và nhân, và phép toán bình phương trong miền nhị phân rất hiệu quả, vì nó tuân theo quy tắc đơn giản hóa (X + Y )2 = X2 + Y 2.
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. Tính linh hoạt của biểu diễn này không cần bất kỳ chi phí tính toán nào, chỉ là việc chuyển đổi kiểu chuỗi bit (typecast), đây 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. Ngoài ra, bài báo "Về việc đảo ngược hiệu quả trong các miền tháp có đặc trưng là hai" đã khám phá độ 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 trong miền nhị phân tháp n bit ( có thể phân rã thành miền con m bit ).
2.2 PIOP: phiên bản chuyển thể HyperPlonk Product và PermutationCheck------ áp dụng cho trường nhị phân
Thiết kế PIOP trong giao thức Binius dựa trên 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 các đ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 minh bí 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 minh kết quả đánh giá của hai đa thức nhiều biến f và g trên hypercube Boole có phải là mối quan hệ hoán vị hay không 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: 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 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 giá trị của đa thức hữu tỷ trên siêu khối Boolean có bằng với một giá trị đã tuyên bố ∏x∈Hμ f(x) = s, nhằm đả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 tại bất kỳ điểm nào trên khối siêu Boole có phải là zero ∏x∈Hμ f(x) = 0, ∀x ∈ Bμ, để đảm bảo phân bố điểm zero 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ị đã tuyên bố 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, thông qua việc 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ý 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 đa biến 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 trên 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 biệt hóa giá trị đó thành 1, từ đó giảm độ phức tạp tính toán.
Xử lý vấn đề chia cho 0: HyperPlonk không xử lý đầy đủ trường hợp chia cho 0, dẫn đến không thể khẳng định vấn đề không bằng 0 của U trên siêu hình hộp; Binius đã xử lý đúng vấn đề này, ngay cả trong trường hợp mẫu số bằng 0, 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ị PermutationCheck: 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, điều này giúp Binius có thể xử lý các trường hợp sắp xếp đa thức phức tạp hơn.
Do đó, Binius thông qua việc
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.
Binius STARKs: Hệ thống chứng minh không kiến thức hiệu quả trên miền nhị phân
Phân tích nguyên lý Binius STARKs và những suy nghĩ tối ưu hóa
1. Giới thiệu
Khác với SNARKs dựa trên đường cong elip, STARKs có thể được coi là SNARKs dựa trên hàm băm. 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ị boolean, 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, việc sử dụng mã hóa Reed-Solomon để mở rộng dữ liệu sẽ tạo ra nhiều giá trị dư thừa bổ sung chiếm 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 quan trọng.
Thế hệ 1 STARKs có bề rộng mã 252bit, thế hệ 2 STARKs có bề rộng mã 64bit, thế hệ 3 STARKs có bề rộng mã 32bit, nhưng bề rộng mã 32bit vẫn còn 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 có không gian lãng phí nào, tức là thế hệ 4 STARKs.
So với Goldilocks, BabyBear, Mersenne31 và các phát hiện nghiên cứu gần đây về miền hữu hạn, nghiên cứu về miền nhị phân có thể được truy ngược tới thập niên 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 trường F28;
Mã xác thực thông điệp Galois ( GMAC ), dựa trên trường 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 như hàm băm Grøstl vào vòng 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 ngày càng quan trọng để đảm bảo tính bảo mật. 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 bảo mật và khả năng sử dụng thực tế. Hầu hết các đa thức liên quan trong các phép tính Prover không cần phải vào miền mở rộng, mà chỉ cần hoạt động trong miền cơ sở, do đó đạ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 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ó 2 vấn đề thực tế: Khi tính toán biểu diễ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 sáng tạo để xử lý hai vấn đề này một cách riêng biệt, và đạt được điều đó bằng cách biểu diễn cùng một dữ liệu theo hai cách khác nhau: đầu tiên, sử dụng đa biến ( cụ thể là đa thức nhiều tuyến tính ) 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" ( hypercubes ) để biểu diễn toàn bộ quỹ đạo tính toán; thứ hai, do chiều dài của mỗi chiều trong siêu lập phương đều bằng 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ể xem siêu lập phương như một hình vuông ( square ), và thực hiện mở rộng Reed-Solomon dựa trên hình vuông đó. 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 an toàn.
2. Phân tích nguyên lý
Hiện tại, hầu hết các hệ thống SNARKs được xây dựng 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 (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP): PIOP, như 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 qua sự tương tác với người xác minh, giúp người xác minh chỉ cần truy vấn kết quả đánh giá của một số ít đa thức để xác minh tính đúng đắn của phép tính. Các giao thức PIOP hiện có bao gồm: PLONK PIOP, Spartan PIOP và HyperPlonk PIOP, mỗi cái có cách xử lý khác nhau đối với biểu thức đa thức, 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 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ã, 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 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. Các PCS khác nhau có hiệu suất, tính bảo mật và các tình huống áp dụng 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 các miền hữu hạn hoặc đường cong elip phù hợp, có thể xây dựng các 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ế chú trọng đến khả năng mở rộng và loại bỏ thiết lập tin cậy trong giao thức ZCash.
• Plonky2: Kết hợp PLONK PIOP và FRI PCS, dựa trên miền Goldilocks. Plonky2 được thiết kế để đạt được tính tái diễn hiệu quả. Khi thiết kế các 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, nhằm đả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 tổ hợp này không chỉ ảnh hưởng đến kích thước chứng minh và hiệu quả xác minh của SNARK, 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à liệu có thể hỗ trợ chứng minh tái diễn hoặc chứng minh tổng hợp và các chức năng mở rộng khác.
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 suất và độ an toàn của nó. Đầu tiên, cấu trúc số học dựa trên tháp miền nhị phân (towers of binary fields) tạo thành nền tảng cho tính toán của nó, có khả năng thực hiện các phép toán đơn giản trong miền nhị phân. Thứ hai, Binius trong giao thức chứng nhận Oracle tương tác (PIOP) đã điều chỉnh kiểm tra sản phẩm và hoán vị HyperPlonk, đảm bảo tính nhất quán an toàn và hiệu quả giữa các biến và sự hoán vị của chúng. Thứ ba, giao thức giới thiệu một chứng nhận chuyển vị đa thức mới, tối ưu hóa hiệu suất xác minh các mối quan hệ đa thức trên miền nhỏ. Thứ tư, Binius áp dụng chứng nhận tìm kiếm Lasso cải tiến, mang lại tính linh hoạt và độ an toàn 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 nhận hiệu quả trên miền nhị phân và giảm thiểu 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 tháp của các trường nhị phân
Trường 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 hai yếu tố: tính toán hiệu quả và toán học hiệu quả. Trường nhị phân về bản chất hỗ trợ các phép toán toán học hiệu quả cao, 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 về hiệu suất. Hơn nữa, cấu trúc trường nhị phân hỗ trợ quá trình toán 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ố gọn gàng và 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 điểm phân cấp của nó thông qua cấu trúc tháp, khiến cho trường 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 biểu diễn duy nhất và trực tiếp của các yếu 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 một yếu tố miền nhị phân k bit. Điều này khác với miền số nguyên tố, nơi mà 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 yếu 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 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ư được sử dụng trong AES ), giảm Montgomery ( như trong POLYVAL ) và giảm đệ quy ( như Tower ). Bài báo "Khám Phá Không Gian Thiết Kế Của ECC-Hardware Implementations Trên Miền Số Nguyên Tố So Với Miền Nhị Phân" chỉ ra rằng miền nhị phân không cần phải đưa vào việc mang khi thực hiện các phép toán cộng và nhân, và phép toán bình phương trong miền nhị phân rất hiệu quả, vì nó tuân theo quy tắc đơn giản hóa (X + Y )2 = X2 + Y 2.
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. Tính linh hoạt của biểu diễn này không cần bất kỳ chi phí tính toán nào, chỉ là việc chuyển đổi kiểu chuỗi bit (typecast), đây 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. Ngoài ra, bài báo "Về việc đảo ngược hiệu quả trong các miền tháp có đặc trưng là hai" đã khám phá độ 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 trong miền nhị phân tháp n bit ( có thể phân rã thành miền con m bit ).
2.2 PIOP: phiên bản chuyển thể HyperPlonk Product và PermutationCheck------ áp dụng cho trường nhị phân
Thiết kế PIOP trong giao thức Binius dựa trên 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 các đ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 minh bí 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 minh kết quả đánh giá của hai đa thức nhiều biến f và g trên hypercube Boole có phải là mối quan hệ hoán vị hay không 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: 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 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 giá trị của đa thức hữu tỷ trên siêu khối Boolean có bằng với một giá trị đã tuyên bố ∏x∈Hμ f(x) = s, nhằm đả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 tại bất kỳ điểm nào trên khối siêu Boole có phải là zero ∏x∈Hμ f(x) = 0, ∀x ∈ Bμ, để đảm bảo phân bố điểm zero 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ị đã tuyên bố 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, thông qua việc 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ý 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 đa biến 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 trên 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 biệt hóa giá trị đó thành 1, từ đó giảm độ phức tạp tính toán.
Xử lý vấn đề chia cho 0: HyperPlonk không xử lý đầy đủ trường hợp chia cho 0, dẫn đến không thể khẳng định vấn đề không bằng 0 của U trên siêu hình hộp; Binius đã xử lý đúng vấn đề này, ngay cả trong trường hợp mẫu số bằng 0, 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ị PermutationCheck: 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, điều này giúp Binius có thể xử lý các trường hợp sắp xếp đa thức phức tạp hơn.
Do đó, Binius thông qua việc