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

1 Giới thiệu

Một trong những lý do chính dẫn đến hiệu suất thấp của STARKs là: hầu hết các giá trị trong chương trình thực tế đều 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 cách sử dụng mã Reed-Solomon sẽ tạo ra nhiều giá trị dư thừa chiếm toàn bộ miền. Giảm kích thước miền trở thành chiến lược then chốt.

Độ rộng mã hóa của STARKs thế hệ đầu tiên là 252 bit, thế hệ thứ hai là 64 bit, và thế hệ thứ ba là 32 bit, nhưng độ rộng mã hóa 32 bit vẫn có 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 với 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à STARKs thế hệ thứ tư.

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 ban đầu và zk-STARK, cũng như hàm băm Grøstl vào vòng chung kết SHA-3

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ế.

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

• Sử dụng đa biến (cụ thể là đa thức bậc nhiều) thay thế cho đa thức một biến, thông qua việc lấy 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.
• Xem khối siêu lập phương như một hình vuông, dựa trên hình vuông đó để mở rộng Reed-Solomon

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

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

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

1. Căn cứ vào miền nhị phân dạng tháp.
2. Phiên bản 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 mới
4. Phiên bản cải tiến của lý thuyết tìm kiếm Lasso
5. Chương trình cam kết đa thức miền nhỏ

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

Ưu điểm của miền nhị phân dạng tháp:

• Tính toán hiệu quả: Miền nhị phân về bản chất hỗ trợ các phép toán số học hiệu quả cao.
• Tính toán hiệu quả: Cấu trúc trường nhị phân hỗ trợ quy trình tính toán đơn giản.
• Biểu diễn linh hoạt: Cùng một chuỗi có thể được giải thích theo nhiều cách trong ngữ cảnh của miền nhị phân.
• Không cần khử: miền nhị phân không cần mang theo trong các phép toán cộng và nhân.
• Tính toán bình phương hiệu quả: (X + Y)2 = X2 + Y2

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ị

Cơ chế kiểm tra chính

1. GateCheck
2. PermutationCheck
3. LookupCheck
4. MultisetCheck
5. ProductCheck
6. ZeroCheck
7. SumCheck
8. BatchCheck

So với sự cải tiến của HyperPlonk:

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

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

Phương pháp chính:

• Packing: Tối ưu hóa hoạt động 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ử dịch: Sắp xếp lại các phần tử trong khối dựa trên độ dịch đã cho để thực hiện dịch vòng.

2.4 PIOP: Phiên bản cải biên đối số tìm kiếm Lasso

Ưu điểm của giao thức Lasso:

• Chứng minh hiệu quả: Đối với m lần tìm kiếm trong bảng có kích thước n, chỉ cần cam kết m+n phần tử miền.
• Không cần cam kết bảng lớn: Nếu bảng t có cấu trúc, thì không cần cam kết nó, có thể xử lý bảng siêu lớn.

Thành phần của giao thức Lasso:

• 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

Binius đối với sự chuyển thể của Lasso:

• Giới thiệu phiên bản nhân của giao thức Lasso
• Yêu cầu bên chứng minh cam kết một vectơ đếm đọc không bằng không ở mọi nơi.

2.5 PCS: Phiên bản cải biên Brakedown PCS

Ý tưởng cốt lõi: packing

Hai phương án:

1. Sử dụng mã kết hợp
2. Áp dụng công nghệ mã hóa cấp khối, hỗ trợ sử dụng riêng mã Reed-Solomon.

Công nghệ chính:

• Cam kết đa thức nhỏ và đánh giá miền mở rộng
• Cấu trúc phổ quát nhỏ
• Mã khối và mã Reed-Solomon

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

Bốn điểm tối ưu hóa quan trọng:

1. PIOP dựa trên GKR: dành cho phép toán nhân trong miền nhị phân
2. Tối ưu ZeroCheck PIOP: Cân nhắc chi phí tính toán giữa Prover và Verifier
3. Tối ưu hóa PIOP Sumcheck: Giao thức Sumcheck dựa trên miền nhỏ
4. Tối ưu PCS: FRI-Binius giảm kích thước chứng minh Binius

3.1 PIOP dựa trên GKR: Phép nhân miền nhị phân dựa trên GKR

Ý tưởng cốt lõi:

Kiểm tra xem 2 số nguyên 32-bit A và B có thỏa mãn A·B =? C hay không. Chuyển đổi thành
"Kiểm tra (gA)B =? gC có hợp lệ không"

Ưu điểm:

• Chỉ cần một cam kết bổ sung
• Giảm chi phí của Sumchecks

3.2 ZeroCheck PIOP tối ưu

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

• Giảm thiểu 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 Sumcheck PIOP tối ưu hóa

Cải tiến trọng điểm:

• Chọn vòng chuyển đổi
• Ảnh hưởng của kích thước miền cơ bản đến hiệu suất
• Lợi ích tối ưu hóa của thuật toán Karatsuba
• Cải thiện hiệu suất bộ nhớ

Cụ thể hiệu quả:

• Trong trường hợp trường 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.
• Thuật toán 4 chỉ cần 0.26MB bộ nhớ, trong khi thuật toán 3 cần 67MB.

3.4 PCS Tối ưu:FRI-Binius

Bốn điểm đổi mới:

1. Đa thức phẳng
2. Đa thức biến mất của không gian con
3. Gói cơ sở đại số
4. Hoán đổi SumCheck

Hiệu quả: Giảm kích thước chứng nhận Binius một bậc

4 Kết luận

Ưu điểm của Binius:

• Có thể sử dụng miền power-of-two tối thiểu cho witnesses.
• Tỷ lệ sử dụng bộ nhớ thấp, chứng minh nhanh chóng
• Cơ bản hoàn toàn loại bỏ nút thắt cam kết của Prover.

FRI-Binius方案: Loại bỏ chi phí nhúng từ lớp chứng minh miền mà không làm tăng chi phí của lớp chứng minh tổng hợp.

Thông tin mới nhất:

• Nhóm Irreducible đang phát triển lớp đệ quy của mình và 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
• Nhóm Ingonyama đang triển khai phiên bản FPGA của Binius