Аналіз принципів Binius STARKs та роздуми про оптимізацію

1. Вступ

Основною причиною низької ефективності STARKs є те, що в реальних програмах більшість значень є досить малими, але для забезпечення безпеки доказів на основі дерева Меркла, під час розширення даних за допомогою кодування Ріда-Соломона багато додаткових надлишкових значень займають весь простір. Зменшення розміру простору стало ключовою стратегією.

Перший покоління коду STARKs має ширину кодування 252 біт, другий - 64 біти, третій - 32 біти, але 32-бітна ширина кодування все ще має величезні витрати простору. У порівнянні з цим, бінарна область дозволяє безпосередньо виконувати операції над бітом, кодуючи компактно та ефективно, без будь-яких витрат простору, тобто четверте покоління STARKs.

Binius використовує двійкове поле, яке повністю залежить від розширеного поля для забезпечення своєї безпеки та фактичної придатності. Більшість поліномів, що беруть участь у обчисленнях Prover, не потребують переходу в розширене поле, а лише виконуються в базовому полі, що забезпечує високу ефективність у малих полях. Проте перевірка випадкових точок і обчислення FRI все ще вимагають поглиблення в більше розширене поле для забезпечення необхідного рівня безпеки.

Binius запропонував інноваційне рішення: по-перше, використовуючи багатозмінні (зокрема, багатолінійні) многочлени замість однозмінних многочленів, шляхом їх значень на "гіперкубі" для представлення всієї обчислювальної траєкторії; по-друге, розглядаючи гіперкуб як квадрат, на основі цього квадрата виконати розширення Ріда-Соломона. Цей підхід, забезпечуючи безпеку, значно підвищив ефективність кодування та обчислювальну продуктивність.

2. Аналіз принципу

Binius включає п'ять ключових технологій:

1. Армування на основі двійкової області з пірамідою
2. Адаптована версія перевірки добутку та перетворення HyperPlonk
3. Новий багатолінійний зсувний доказ
4. Покращена версія доказу пошуку Lasso
5. Схема зобов'язань малих полігональних функцій

2.1 Обмежене поле: арифметика на основі веж бінарних полів

Стовпчаста двійкова область підтримує високо ефективні арифметичні операції, підтримуючи спрощений арифметичний процес. Елементи двійкової області мають унікальне та пряме представлення, що дозволяє гнучко переходити та упаковувати між областями різного розміру.

! Дослідження Bitlayer: Аналіз принципів Бініуса Старка та оптимізаційне мислення

2.2 PIOP: адаптований продукт HyperPlonk і PermutationCheck

Binius використовує ряд основних механізмів перевірки, включаючи GateCheck, PermutationCheck, LookupCheck, MultisetCheck, ProductCheck, ZeroCheck, SumCheck та BatchCheck.

В порівнянні з HyperPlonk, Binius покращив наступні аспекти:

• Оптимізація ProductCheck
• Обробка проблеми ділення на нуль
• Перевірка перестановки

2.3 PIOP: новий аргумент багатовимірного зміщення

Binius використовує два основні методи: Packing та оператори зсуву для обробки віртуальних многочленів.

2.4 PIOP: адаптована версія Lasso lookup аргумент

Протокол Lasso складається з трьох компонентів:

• Віртуальна поліноміальна абстракція великої таблиці
• Пошук малих таблиць
• Багаторазова перевірка

Binius впровадив версію протоколу Lasso з множенням, що вимагає від сторони, що доводить, та сторони, що перевіряє, спільного збільшення операції "лічильник пам'яті" не шляхом простого додавання 1, а шляхом збільшення за допомогою множення генератора в бінарному полі.

! Дослідження Bitlayer: Аналіз принципів Бініуса Старка та оптимізаційне мислення

2.5 PCS: адаптована версія Brakedown PCS

Основні використовувані політичні зобов'язання Binius:

• Малий поліноміальний зобов'язання та оцінка розширеного поля
• Загальний конструктив малих доменів
• Блочне кодування та технологія кодів Ріда-Соломона

! Дослідження Bitlayer: Аналіз принципів Бініуса Старка та оптимізаційне мислення

3. Оптимізація мислення

3.1 GKR-based PIOP: бінарне множення над полем на основі GKR

Алгоритм множення цілих чисел на основі GKR, перетворює запит "перевірити, чи 2 32-бітні цілі числа A та B задовольняють A·B =? C" на "перевірити, чи (gA)B =? gC є істинним", значно зменшуючи витрати на зобов'язання за допомогою протоколу GKR.

3.2 ZeroCheck PIOP оптимізація: баланс витрат на обчислення Prover та Verifier

• Зменшити передачу даних від доказуючої сторони
• Зменшити кількість оцінювальних пунктів для доказуючих сторін
• Оптимізація алгебраїчної інтерполяції

3.3 Sumcheck PIOP оптимізація: на основі малих областей протокол Sumcheck

• Вплив та фактори покращення змін циклів
• Вплив розміру базової області на продуктивність
• Оптимізація вигоди алгоритму Карацуби
• Підвищення ефективності пам'яті

3.4 PCS оптимізація: FRI-Binius зменшити розмір доказу Binius

FRI-Binius реалізував механізм згортання двійкової області FRI, що приніс 4 аспекти інновацій:

• Спрощений многочлен
• Поліном зникнення підпростору
• Пакування алгебраїчної бази
• Обмін кільцями SumCheck

! Дослідження Bitlayer: Аналіз принципів Бініуса Старка та оптимізаційне мислення

4. Підсумок

Binius практично повністю усунув вузьке місце комітменту Prover, нове вузьке місце полягає в протоколі Sumcheck. Схема FRI-Binius є варіантом FRI, що дозволяє усунути накладні витрати на вбудовування з рівня доказів поля. Наразі команда Irreducible розробляє свій рекурсивний рівень і співпрацює з командою Polygon для створення zkVM на основі Binius; JoltzkVM переходить з Lasso на Binius; команда Ingonyama реалізує версію Binius на FPGA.

! Дослідження Bitlayer: Аналіз принципів Бініуса Старка та оптимізаційне мислення