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

1. Giới thiệu

Một trong những lý do chính khiến STARKs kém hiệu quả là hầu hết các giá trị trong các chương trình thực tế đều khá 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ải quyết vấn đề này, việc 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à 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 rất 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à STARKs thế hệ thứ tư.

Miền nhị phân mà Binius sử dụng hoàn toàn phụ thuộc vào miền mở rộng để đả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 đến tính toán Prover không cần vào miền mở rộng, mà chỉ cần hoạt động trong miền cơ bản, do đó đạt được hiệu suất cao trong miền nhỏ. Tuy nhiên, 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 an toàn cần thiết.

Binius đã đề xuất một giải pháp sáng tạo: trước tiên, sử dụng đa biến (cụ thể là đa thức nhiều tuyến tính) thay vì đ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 thị toàn bộ quỹ đạo tính toán; tiếp theo, do chiều dài của mỗi chiều trong siêu lập phương đều là 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ể coi siêu lập phương là hình vuông (square), dựa trên hình vuông đó để thực hiện mở rộng Reed-Solomon.

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

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

1. Phép toán dựa trên miền nhị phân dạng tháp
2. Phiên bản cải biên kiểm tra tích và hoán vị HyperPlonk
3. Lập luận 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. Chương trình cam kết đa thức nhỏ

2.1 miền hữu hạn: số hóa dựa trên towers of binary fields

Ư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ề cơ bản 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ợ quá trình tính toán đơn giản hóa
• Biểu diễn chuẩn: Các phần tử trong miền nhị phân có cách biểu diễn duy nhất và trực tiếp.

Lợi thế của miền nhị phân:

• Phép cộng và phép nhân không cần phải mang theo.
• Phép toán bình phương rất hiệu quả, tuân theo quy tắc đơn giản (X + Y)^2 = X^2 + Y^2
• Thể hiện tính linh hoạt: Chuỗi 128 bit có thể được coi là một yếu tố độc đáo trong miền nhị phân 128 bit, hoặc được phân tích thành sự kết hợp của nhiều yếu tố miền tháp.

2.2 PIOP: phiên bản cải biên của sản phẩm HyperPlonk và PermutationCheck

Cơ chế kiểm tra lõi PIOP của Binius:

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

Cải tiến của Binius đối với HyperPlonk:

• Tối ưu hóa ProductCheck
• Xử lý vấn đề chia cho không
• Hỗ trợ Kiểm tra Hoán vị Chéo

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

Phương pháp chính:

• Đóng gói: Tối ưu hóa thao tác thông qua việc đóng gói các phần tử liền kề
• Toán tử dịch: Sắp xếp lại các phần tử trong khối

2.4 PIOP: Phiên bản sửa đổi đối số tìm kiếm Lasso

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

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

Binius đã chỉnh sử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 vector đếm đọc không bao giờ bằng 0.

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

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

Hai loại phương án cam kết đa thức Brakedown dựa trên miền nhị phân:

1. Áp dụng mã nối kết để khởi tạo
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 chung của tiểu miền
• Mã khối và mã Reed-Solomon

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

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

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

So với lợi thế của giải pháp Binius lookup:

• Chỉ cần một cam kết phụ
• Giảm chi phí Sumchecks

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

Phương pháp 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 Tối ưu hóa PIOP Sumcheck: Giao thức Sumcheck dựa trên miền nhỏ

Điểm 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 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 bằng chứng Binius

FRI-Binius bốn đổi mới:

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

Quá trình FRI-Binius PCS:

• Giai đoạn cam kết
• Giai đoạn đánh giá

4. Tóm tắt

Giá trị đề xuất của Binius:

• Có thể sử dụng miền power-of-two tối thiểu cho các nhân chứng.
• Giải pháp thiết kế hợp tác, chứng minh nhanh với mức sử dụng bộ nhớ thấp
• Cơ bản loại bỏ nút thắt cam kết commit của Prover
• Điểm nghẽn mới nằm ở giao thức Sumcheck, có thể được giải quyết hiệu quả bằng phần cứng chuyên dụng.

FRI-Binius方案:

• Loại bỏ chi phí nhúng từ lớp chứng minh miền
• Không gây tăng chi phí lớp chứng minh tổng hợp.

Tiến độ hiện tại:

• Nhóm Irreducible phát triển lớp đệ quy, hợp tác với Polygon xây dựng zkVM dựa trên Binius
• JoltzkVM chuyển từ Lasso sang Binius
• Nhóm Ingonyama đã triển khai phiên bản FPGA của Binius