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

1. Вступ

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

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

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

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

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

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

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

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

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

Переваги баштової двійкової області:

• Висока ефективність обчислень: двійкове поле по суті підтримує високоефективні арфметичні операції
• Ефективна арифметика: структура бінарного поля підтримує спрощений арифметичний процес
• Нормативне представлення: елементи в бінарній області мають унікальний і прямий спосіб представлення.

Переваги двійкової області:

• Операції додавання та множення не вимагають переносу
• Квадратні обчислення дуже ефективні, дотримуються спрощених правил (X + Y)^2 = X^2 + Y^2
• Відображення гнучкості: 128-бітовий рядок може розглядатися як унікальний елемент у 128-бітному бінарному полі або розглядатися як комбінація різних елементів у баштовому полі.

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

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

Ядро механізму перевірки Binius PIOP:

• Перевірка воріт
• Перевірка перестановки
• Перевірка пошуку
• Функція MultisetCheck
• Перевірка товару
• Нульовий чек
• Перевірка суми
• Пакетна перевірка

Покращення Binius для HyperPlonk:

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

2.3 PIOP: новий мультилінійний зсув аргумент

Ключовий метод:

• Упаковка: оптимізація операцій шляхом упаковки сусідніх елементів
• Оператор зсуву: перерозподіл елементів у блоці

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

Склад протоколу Lasso:

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

Binius адаптація Lasso:

• Введення версії Lasso протоколу з множенням
• Вимагати, щоб сторона, що підтверджує, зобов'язалася надати вектор лічильників читання, що не є нульовим у всіх елементах.

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

Основна ідея: packing

Два варіанти поліноміальних зобов'язань Brakedown на основі бінарних полів:

1. Використання екземпляра конкатенованого коду
2. Використання технології кодування на рівні блоків, підтримка окремого використання кодів Ріда-Соломона

Основна технологія:

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

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

Чотири ключові точки оптимізації:

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

Переваги порівняно з рішенням Binius lookup:

• Потрібен лише один допоміжний зобов'язання
• Зменшити витрати на Sumchecks

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

Оптимізаційний метод:

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

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

Ключові моменти:

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

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

Чотири інновації FRI-Binius:

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

Процес FRI-Binius PCS:

• Етап зобов'язань
• Етап оцінки

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

4. Підсумок

Ціннісна пропозиція Binius:

• Може використовувати найменше поле степеня двійки для свідків
• Спільний проект, низьке використання пам'яті, швидке доведення
• Основне усунення вузького місця зобов'язання Prover
• Новий вузол полягає в протоколі Sumcheck, який можна ефективно вирішити за допомогою спеціалізованого апаратного забезпечення.

FRI-Binius рішення:

• Видалення вбудованих витрат з рівня доказу домену
• Не призведе до різкого зростання витрат на рівні агрегатного доказу

Поточний прогрес:

• Команда Irreducible розробляє рекурсивний шар, співпрацюючи з Polygon для створення zkVM на базі Binius
• JoltzkVM перейшов з Lasso на Binius
• Команда Ingonyama реалізувала FPGA версію Binius

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