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

1. Giới thiệu

Một trong những lý do chính khiến STARKs có hiệu suất thấp là hầu hết các giá trị trong các 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, khi sử dụng mã Reed-Solomon để mở rộng dữ liệu, nhiều giá trị dư thừa bổ sung sẽ 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ệ 1 là 252 bit, thế hệ 2 là 64 bit, thế hệ 3 là 32 bit, nhưng độ rộng mã hóa 32 bit vẫn tồn tại 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 trên bit, mã hóa chặt chẽ hiệu quả không có lãng phí tùy ý, tức là STARKs thế hệ 4.

So với các nghiên cứu gần đây về Goldilocks, BabyBear, Mersenne31 và các trường hữu hạn khác, nghiên cứu về trường nhị phân có thể được truy ngược đến những năm 1980, đã được ứng dụng rộng rãi trong mật mã, như lĩnh vực AES(F28, lĩnh vực GMAC)F2128, mã QR(F28 và mã Reed-Solomon).

Binius sử dụng miền nhị phân, cần hoàn toàn phụ thuộc vào 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 toán Prover hoạt động hiệu quả dưới miền cơ sở, kiểm tra điểm ngẫu nhiên và tính toán FRI cần phải mở rộng miền sâu để đảm bảo tính an toàn.

Binius sử dụng đa biến đa thức để lấy giá trị trên "khối siêu" đại diện cho đường đi tính toán, coi khối siêu như hình vuông để mở rộng Reed-Solomon, đồng thời đảm bảo an toàn và nâng cao hiệu suất mã hóa cũng như hiệu suất tính toán.

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

Binius: HyperPlonk PIOP + Brakedown PCS + miền nhị phân.

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

1. Cơ sở tính toán của cấu trúc số học 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, đảm bảo kiểm tra tính nhất quán của biến và hoán vị.

3. Lý thuyết chứng minh dịch chuyển đ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ỏ.

4. Phiên bản cải tiến của Lasso tìm kiếm chứng minh, cung cấp tính linh hoạt và an toàn cho cơ chế tìm kiếm.

5. Giải pháp 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.

( 2.1 Tập hợp hữu hạn: Toán tử 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ả và quy trình số học đơn giản hóa, đặc biệt phù hợp với hệ thống chứng minh có thể mở rộng như Binius.

Chuỗi 128 bit có thể được coi là một phần tử duy nhất trong miền nhị phân 128 bit, hoặc phân tích thành hai phần tử miền 64 bit, bốn phần tử miền 32 bit, mười sáu phần tử miền 8 bit, hoặc một trăm hai mươi tám phần tử miền F2. Sự linh hoạt này không cần chi phí tính toán, chỉ là một chuyển đổi kiểu cho chuỗi bit.

![Bitlayer Research：Phân tích nguyên lý Binius STARKs và suy nghĩ tối ưu hóa])https://img-cdn.gateio.im/webp-social/moments-1fb9ecbf9b3b2beaec758f3ab686a012.webp###

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

Binius PIOP tham khảo HyperPlonk, áp dụng 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 đa biến, bao gồm GateCheck, PermutationCheck, LookupCheck, MultisetCheck, ProductCheck, ZeroCheck, SumCheck, BatchCheck.

Binius đã cải tiến ở 3 lĩnh vực sau:

• Tối ưu hóa ProductCheck: Chuyên biệt hóa giá trị thành 1, đơn giản hóa quy trình kiểm tra và giảm độ phức tạp tính toán.

• Xử lý vấn đề chia cho 0: Xử lý đúng trường hợp mẫu số bằng 0, cho phép mở rộng đến bất kỳ giá trị tích nào

• Kiểm tra hoán vị đa cột: Hỗ trợ kiểm tra hoán vị giữa nhiều cột, xử lý các trường hợp sắp xếp đa thức phức tạp hơn.

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

Cấu trúc và xử lý đa thức ảo trong Binius là công nghệ then chốt:

• Packing: Gói các phần tử có vị trí từ điển liền kề nhỏ hơn thành các phần tử lớn hơn để tối ưu hóa thao tác.

• Toán tử dịch chuyển: sắp xếp lại các phần tử trong khối, dựa trên độ dịch chuyển đã cho để dịch chuyển vòng.

![Bitlayer Research：Phân tích nguyên lý Binius STARKs và suy nghĩ tối ưu hóa]###https://img-cdn.gateio.im/webp-social/moments-a5d031be4711f29ef910057f4e44a118.webp###

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

Giao thức Lasso cho phép bên chứng minh cam kết vector a ∈ Fm và chứng minh rằng tất cả các phần tử tồn tại trong bảng đã chỉ định trước t ∈ Fn.

Binius đã điều chỉnh Lasso cho các phép toán trên trường nhị phân, 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 và bên xác minh hợp tác thực hiện phép toán "đếm bộ nhớ" theo dạng giao thức tăng dần, thông qua phép nhân trên trường nhị phân để tạo ra sự gia tăng của phần tử.

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

Xây dựng tư tưởng cốt lõi của BiniusPCS là packing. Cung cấp 2 loại giải pháp cam kết đa thức Brakedown dựa trên miền nhị phân:

1. Áp dụng mã nối để 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

Giải pháp thứ hai đơn giản hóa quy trình chứng minh và xác minh, kích thước chứng minh hơi lớn nhưng những lợi thế về đơn giản hóa và thực hiện là đáng giá.

![Bitlayer Research：Phân tích nguyên lý Binius STARKs và suy nghĩ tối ưu hóa]###https://img-cdn.gateio.im/webp-social/moments-d74bdd8bc21dcfc05e21f9c0074461c3.webp###

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

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

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ó đúng không", giúp giảm đáng kể chi phí cam kết nhờ vào giao thức GKR.

Phép nhân dựa trên GKR chỉ cần một cam kết phụ, bằng cách giảm chi phí Sumchecks khiến thuật toán hiệu quả hơn, đặc biệt là trong các trường hợp mà thao tác Sumchecks rẻ hơn việc tạo cam kết.

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

Giảm truyền dữ liệu của bên chứng minh: Chuyển một phần công việc cho bên xác minh, giảm lượng dữ liệu gửi từ bên chứng minh.

Giảm số lượng điểm đánh giá của bên chứng minh: Sửa đổi cách gửi đa thức, giảm số lượng điểm đánh giá.

Tối ưu hóa nội suy đại số: Xây dựng phân tích có thứ tự thông qua phép chia đại số đa thức, đạt được tối ưu hóa nội suy.

![Bitlayer Research：Phân tích nguyên lý Binius STARKs và những suy nghĩ tối ưu hóa])https://img-cdn.gateio.im/webp-social/moments-7f96976952fd0f8da0e93ff1042a966d.webp###

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

Tác động và yếu tố cải tiến của việc chuyển đổi vòng: Việc lựa chọn vòng t chuyển đổi ảnh hưởng đến hiệu suất, yếu tố cải tiến cho điểm chuyển đổi tốt nhất đạt giá trị tối đa.

Tác động của kích thước trường cơ sở đến hiệu suất: Trường cơ sở nhỏ ) như GF###( có lợi thế tối ưu hóa rõ rệt hơn.

Tối ưu hóa lợi ích của thuật toán Karatsuba: Nâng cao đáng kể hiệu suất Sumcheck trên các miền nhỏ, thuật toán 4 hiệu quả gấp năm lần so với thuật toán 3.

Nâng cao hiệu suất bộ nhớ: yêu cầu bộ nhớ của thuật toán 4 là O[2]d·t), thuật toán 3 là O(2d·t), phù hợp với môi trường tài nguyên hạn chế.

( 3.4 PCS tối ưu: FRI-Binius giảm kích thước bằng chứng Binius

FRI-Binius thực hiện cơ chế gập FRI trong miền nhị phân, mang đến 4 đổ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

Nhờ vào FRI-Binius, có thể giảm kích thước chứng minh Binius xuống một bậc, gần với hệ thống tiên tiến nhất.

![Bitlayer Research：Phân tích nguyên lý Binius STARKs và suy nghĩ tối ưu hóa])https://img-cdn.gateio.im/webp-social/moments-16690fad3bc761b99c40e8e82ab2297c.webp###

4. Tóm tắt

Binius đã cơ bản loại bỏ nút thắt cam kết Prover, nút thắt mới nằm ở giao thức Sumcheck. Giải pháp FRI-Binius là biến thể của FRI, có thể loại bỏ chi phí nhúng từ tầng chứng minh miền.

Đội ngũ 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 để cải thiện hiệu suất đệ quy. Ingonyama triển khai phiên bản FPGA của Binius.