Phân tích nguyên lý Binius STARKs và những suy nghĩ tối ưu hóa

1 Giới thiệu

Một trong những lý do chính gây ra sự kém hiệu quả của STARKs là hầu hết các giá trị trong chương trình thực tế là rất nhỏ, nhưng để đảm bảo tính an toàn của chứng minh dựa trên cây Merkle, việc mở rộng dữ liệu bằng mã Reed-Solomon sẽ chiếm nhiều giá trị dư thừa trong toàn bộ miền. Giảm kích thước miền trở thành một chiến lược then chốt.

Độ rộng mã hóa của STARKs thế hệ đầu tiên là 252bit, thế hệ thứ hai là 64bit, thế hệ thứ ba là 32bit, nhưng độ rộng mã hóa 32bit vẫn còn lãng phí rất nhiều không gian. Miền nhị phân cho phép thao tác trực tiếp trên bit, mã hóa chặt chẽ hiệu quả mà không có không gian lãng phí nào, có thể trở thành STARKs thế hệ thứ tư.

Miền nhị phân đã được ứng dụng rộng rãi trong mật mã học, chẳng hạn như AES, GMAC, mã QR, FRI nguyên thủy và giao thức zk-STARK.

Khi Binius sử dụng miền nhị phân, nó cần 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 các phép tính Prover không cần vào miền mở rộng, mà chỉ cần thao tác trong miền cơ bản, từ đó đạt được hiệu suất cao trong miền nhỏ.

Binius đưa ra giải pháp đổi mới:

1. Sử dụng đa biến đa thức thay thế cho đa thức đơn biến, thông qua các giá trị của nó trên "siêu khối" để biểu thị toàn bộ quỹ đạo tính toán.
2. xem siêu khối như hình vuông để mở rộng Reed-Solomon

2 Phân tích nguyên lý

Binius = HyperPlonk PIOP + Brakedown PCS + 二进制域

Bao gồm năm công nghệ chính:

1. Dựa trên miền nhị phân dạng tháp
2. Chỉnh sửa kiểm tra tích và hoán vị HyperPlonk
3. Chứng minh dịch chuyển đa tuyến tính mới
4. Phiên bản cải tiến của lý thuyết tìm kiếm Lasso
5. Giải pháp cam kết đa thức miền nhỏ

2.1 Trường hữu hạn: Toán tử hóa dựa trên tháp của các trường nhị phân

Miền nhị phân dạng tháp hỗ trợ các phép toán số học hiệu quả cao và quy trình số học đơn giản hóa.

Chuỗi 128 bit có thể được coi là một phần 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 cách biểu diễn này không cần chi phí tính toán thêm.

2.2 PIOP: Phiên bản cải biên HyperPlonk Product và PermutationCheck

Thiết kế PIOP trong giao thức Binius đã tham khảo HyperPlonk, áp dụng một loạt các cơ chế kiểm tra cốt lõi:

• GateCheck
• PermutationCheck
• LookupCheck
• MultisetCheck
• ProductCheck
• ZeroCheck
• SumCheck
• BatchCheck

Binius đã cải tiến ở 3 khía cạnh sau:

• Tối ưu hóa ProductCheck
• Xử lý vấn đề chia cho không
• Kiểm tra hoán vị trên cột

2.3 PIOP：Lập luận dịch chuyển đa tuyến mới

Phương pháp chính để xây dựng và xử lý đa thức ảo trong giao thức Binius:

• Đóng gói
• Toán tử dịch bit

2.4 PIOP: Phiên bản cải biên Lasso lookup argument

Giao thức Lasso được cấu thành từ ba thành phần:

• Trừu tượng đa thức ảo lớn
• Tìm kiếm bảng nhỏ
• Kiểm tra đa tập hợp

Giao thức Binius đã điều chỉnh Lasso cho hoạt động trong miền nhị phân, giới thiệu phiên bản nhân của giao thức Lasso.

2.5 PCS：phiên bản cải biên Brakedown PCS

Binius tài liệu cung cấp 2 loại phương án cam kết đa thức Brakedown dựa trên miền nhị phân:

1. Sử dụng mã nối để khởi tạo
2. sử dụng công nghệ mã hóa cấp khối, hỗ trợ việc sử dụng riêng biệt mã Reed-Solomon

Cam kết đa thức nhỏ và đánh giá miền mở rộng, cấu trúc tổng quát miền nhỏ và mã hóa cấp khối với mã Reed-Solomon và các công nghệ khác được sử dụng để xây dựng cam kết đa thức Binius.

3 Tối ưu hóa tư duy

Bốn điểm tối ưu hóa chính:

1. PIOP dựa trên GKR: Đối với phép toán nhân trong miền nhị phân, thay thế thuật toán Lasso Lookup bằng giao thức GKR.

2. Tối ưu hóa ZeroCheck PIOP: Cân nhắc chi phí tính toán giữa Prover và Verifier

3. Tối ưu hóa Sumcheck PIOP: Tối ưu hóa cho Sumcheck miền nhỏ

4. Tối ưu PCS: Giảm kích thước chứng minh thông qua FRI-Binius

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

Thuật toán nhân nguyên dựa trên GKR, bằng cách chuyển đổi "kiểm tra 2 số nguyên 32-bit A và B có thỏa mãn A·B =? C" thành "kiểm tra (gA)B =? gC có hợp lệ không", đã giảm đáng kể chi phí cam kết nhờ vào giao thức GKR.

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

Hướng tối ưu hóa chính:

• Giảm bớt việc truyền dữ liệu của bên chứng minh
• Giảm số lượng điểm đánh giá của bên chứng minh
• Tối ưu hóa nội suy đại số

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

Các điểm tối ưu chính:

• Ảnh hưởng và yếu tố cải tiến của việc chuyển đổi vòng
• Ảnh hưởng của kích thước miền cơ sở đến hiệu suất
• Lợi ích tối ưu hóa của thuật toán Karatsuba
• Nâng cao hiệu suất bộ nhớ

3.4 PCS tối ưu: FRI-Binius giảm kích thước proof Binius

FRI-Binius đã hiện thực hóa cơ chế gập FRI trong miền nhị phân, mang lại 4 khía cạnh đổi mới:

• Đa thức phẳng
• Đa thức biến mất của không gian con
• Đóng gói cơ sở đại số
• Hoán đổi SumCheck

4 Kết luận

Giá trị của Binius là có thể sử dụng miền power-of-two tối thiểu cho các witnesses. Trong Binius, đã cơ bản loại bỏ hoàn toàn nút thắt cam kết của Prover, nút thắt mới nằm ở giao thức Sumcheck.

Giải pháp FRI-Binius là một biến thể của FRI, có thể loại bỏ chi phí nhúng từ lớp chứng minh miền mà không làm tăng đáng kể chi phí của lớp chứng minh tổng hợp.

Hiện tại, đội ngũ Irreducible đang phát triển lớp đệ quy của mình và hợp tác với đội ngũ Polygon để xây dựng zkVM dựa trên Binius; JoltzkVM đang chuyển từ Lasso sang Binius; đội ngũ Ingonyama đang thực hiện phiên bản FPGA của Binius.