Аналіз принципів Binius STARKs та їх оптимізація

1. Вступ

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

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

На відміну від обмежених полів, які досліджувалися в останні роки, таких як Goldilocks, BabyBear, Mersenne31, дослідження бінарних полів можна простежити до 80-х років минулого століття і вони були широко використані в криптографії, таких як AES(F28 поле ), GMAC(F2128 поле ), QR-код (F28 поле кодування Ріда-Соломона ) тощо.

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

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

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

Binius: HyperPlonk PIOP + Brakedown PCS + Binary Domain.

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

1. Арфметична структура обчислень на основі пірамідальної двійкової області

2. Адаптувати перевірку добутку та перестановки HyperPlonk, щоб забезпечити узгодженість перевірки змінних та перестановок

3. Нова багатолінійна зсувна теорія, оптимізація ефективності перевірки багатолінійних відносин на малих полях

4. Покращена версія Lasso пошуку доведення, що надає гнучкість і безпеку механізму пошуку

5. Схема зобов'язань на малих полях багаторазових поліномів, що реалізує ефективну систему доказів над бінарними полями

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

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

128-бітний рядок може розглядатися як унікальний елемент у 128-бітному бінарному полі або бути розкладеним на два елементи 64-бітного поля, чотири елементи 32-бітного поля, 16 елементів 8-бітного поля або 128 елементів F2 поля. Ця гнучкість не потребує обчислювальних витрат, а лише є перетворенням типу бітового рядка.

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

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

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

Binius покращився в наступних 3 аспектах:

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

• Обробка проблеми ділення на нуль: правильна обробка ситуацій, коли знаменник дорівнює нулю, дозволяє розширення на будь-яке значення добутку

• Перевірка перестановок між стовпцями: підтримує перевірку перестановок між кількома стовпцями, обробляючи більш складні випадки перестановок многочленів.

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

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

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

• Оператор зсуву: перетасування елементів у блоці на основі заданого зсуву.

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

Протокол Lasso дозволяє стороні, що доводить, зобов'язатися вектором a ∈ Fm та довести, що всі елементи знаходяться у заздалегідь визначеній таблиці t ∈ Fn.

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

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

Основна ідея побудови BiniusPCS полягає в упаковці. Пропонує 2 варіанти схем обіцянок на основі бінарних полів:

1. Ініціалізація з використанням конкатенованого коду

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

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

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

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

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

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

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

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

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

Зменшити кількість точок оцінки доказуючої сторони: змінити спосіб відправки многочленів, зменшити кількість точок оцінки.

Алгебраічна інтерполяційна оптимізація: побудова впорядкованого розкладу за допомогою ділення многочленів, щоб досягти оптимізації інтерполяції.

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

Вплив і покращувальні фактори зміни раундів: вибір зміни раунду t впливає на продуктивність, оптимальна точка зміни досягає максимального значення.

Вплив розміру базової області на продуктивність: переваги оптимізаційного алгоритму стають більш помітними для маленької базової області (, такої як GF[2]).

Оптимізація алгоритму Карацуби: значне підвищення продуктивності Sumcheck на основі малих полів, алгоритм 4 ефективніший за алгоритм 3 у п'ять разів.

Покращення ефективності пам'яті: вимоги до пам'яті алгоритму 4 O(d·t), алгоритм 3 має O(2d·t), підходить для обмежених ресурсів середовища.

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

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

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

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

Завдяки FRI-Binius можна зменшити розмір доказу Binius на один порядок, наближаючи його до найбільш сучасних систем.

4. Підсумок

Binius вже в основному усунув вузьке місце зобов'язання Prover commit, нове вузьке місце полягає в протоколі Sumcheck. FRI-Binius схема є варіантом FRI, який може усунути накладні витрати на вбудовування з рівня доказів полів.

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

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