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

1 Вступ

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

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

У порівнянні з такими новими дослідженнями обмежених полів, як Goldilocks, BabyBear, Mersenne31, які були виявлені в останні кілька років, дослідження бінарних полів можна простежити до 80-х років минулого століття. Наразі бінарні поля широко використовуються в криптографії,典型例子包括：

• Стандарт високої криптографії (AES), на основі поля F28;

• Galois повідомлення автентифікації ( GMAC ), на основі поля F2128;

• QR-код, що використовує кодування Ріда-Соломона на основі F28;

• Оригінальні протоколи FRI та zk-STARK, а також хеш-функція Grøstl, що потрапила до фіналу SHA-3, яка базується на полі F28, є дуже підходящим хеш-алгоритмом для рекурсії.

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

Під час побудови системи доказів на основі бінарного поля існують 2 практичні проблеми: при обчисленні траси в STARKs розмір поля повинен бути більшим за ступінь многочлена; під час зобов'язання Merkle tree в STARKs потрібно виконати кодування Ріда-Соломона, розмір поля повинен бути більшим за розмір, що розширився після кодування.

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

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

Поточна більшість систем SNARKs зазвичай складається з двох частин:

• Інформаційно-теоретичне поліно-масивне інтерактивне оракульне доведення (Information-Theoretic Polynomial Interactive Oracle Proof, PIOP): PIOP, як основа системи доведення, перетворює вхідні обчислювальні відношення на перевірні поліно-масивні рівняння. Різні протоколи PIOP, завдяки взаємодії з перевіряючим, дозволяють доводнику поетапно надсилати поліно-масиви, що дозволяє перевіряючому перевіряти правильність обчислень, запитуючи результати оцінки лише кількох поліно-масивів. Існуючі протоколи PIOP включають: PLONK PIOP, Spartan PIOP та HyperPlonk PIOP, які по-різному обробляють поліно-масивні вирази, що впливає на загальну продуктивність та ефективність системи SNARK.

• Схема зобов'язання поліномів (Polynomial Commitment Scheme, PCS): Схема зобов'язання поліномів використовується для доведення того, чи є рівність поліномів, згенерованих PIOP, істинною. PCS є криптографічним інструментом, за допомогою якого доводчик може зобов'язатись певним поліномом та пізніше перевірити результати оцінки цього полінома, одночасно приховуючи іншу інформацію про поліном. Загальновідомими схемами зобов'язання поліномів є KZG, Bulletproofs, FRI (Fast Reed-Solomon IOPP) та Brakedown тощо. Різні PCS мають різні характеристики, безпеку та сфери застосування.

Відповідно до конкретних вимог, обирайте різні PIOP та PCS, а також поєднуйте їх з відповідними скінченними полями або еліптичними кривими, можна створити системи доказів з різними властивостями. Наприклад:

• Halo2: поєднує PLONK PIOP та Bulletproofs PCS, базуючись на кривій Pasta. При проектуванні Halo2 акцент робився на масштабованості та видаленні trusted setup з протоколу ZCash.

• Plonky2: використовує PLONK PIOP у поєднанні з FRI PCS та базується на області Goldilocks. Plonky2 створено для досягнення ефективної рекурсії. При проектуванні цих систем вибір PIOP та PCS має відповідати використаній скінченній області або еліптичній кривій, щоб забезпечити правильність, продуктивність і безпеку системи. Вибір цих комбінацій впливає не лише на розмір доказу SNARK та ефективність верифікації, але й визначає, чи може система досягти прозорості без необхідності в надійній установці, чи може вона підтримувати розширені функції, такі як рекурсивні докази чи агреговані докази.

Binius: HyperPlonk PIOP + Brakedown PCS + двійкове поле. Зокрема, Binius включає п'ять ключових технологій для досягнення своєї ефективності та безпеки. По-перше, на основі баштових двійкових полів (towers of binary fields) арифметична структура є основою його обчислень, що дозволяє виконувати спрощені операції в двійковому полі. По-друге, Binius у своєму інтерактивному Oracle доказовому протоколі (PIOP) адаптував перевірки добутків та перестановок HyperPlonk, що забезпечує безпечну та ефективну перевірку узгодженості між змінними та їх перестановками. По-третє, протокол вводить новий багатолінійний зсувний доказ, який оптимізує ефективність перевірки багатолінійних зв'язків на малих полях. По-четверте, Binius використовує покращену версію Lasso пошукового доказу, яка забезпечує гнучкість і потужну безпеку для механізму пошуку. Нарешті, протокол використовує схему зобов'язань малих поліномів (Small-Field PCS), що дозволяє йому реалізувати ефективну систему доказів у двійковому полі та зменшити витрати, які зазвичай пов'язані з великими полями.

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

Таула́рне двої́чне поле є ключем до реалізації швидких перевіряємих обчислень, що головним чином зумовлено двома аспектами: ефективними обчисленнями та ефективною аритметикою. Двоїчне поле в основному підтримує надзвичайно ефективні арифметичні операції, що робить його ідеальним вибором для криптографічних застосувань, чутливих до продуктивності. Крім того, структура двоїчного поля підтримує спрощений аритметичний процес, тобто обчислення, виконувані над двоїчним полем, можуть бути представлені у компактній та легко перевіряємій алгебраїчній формі. Ці характеристики, разом із здатністю повною мірою використовувати його ієрархічні властивості через тау-структуру, роблять двоїчне поле особливо підходящим для таких масштабованих систем доказів, як Binius.

Термін "canonical" відноситься до унікального та прямого способу представлення елементів у бінарному полі. Наприклад, у найосновнішому бінарному полі F2 будь-який k-бітний рядок може бути безпосередньо відображений на k-бітний елемент бінарного поля. Це відрізняється від простих полів, які не можуть надати таке канонічне представлення в заданій кількості бітів. Хоча 32-бітне просте поле може вміститися в 32 бітах, не кожен 32-бітний рядок може унікально відповідати елементу поля, тоді як бінарне поле має цю зручність взаємно-однозначного відображення. У простому полі Fp поширеними методами редукції є редукція Барретта, редукція Монтгомері, а також спеціальні методи редукції для конкретних скінчених полів, таких як Mersenne-31 або Goldilocks-64. У бінарному полі F2k звичайні методи редукції включають спеціальну редукцію (як використано в AES), редукцію Монтгомері (як використано в POLYVAL) і рекурсивну редукцію (як Tower). У статті "Exploring the Design Space of Prime Field vs. Binary Field ECC-Hardware Implementations" зазначається, що в бінарному полі не потрібно вводити перенесення при виконанні операцій додавання та множення, а квадратична операція в бінарному полі є дуже ефективною, оскільки вона слідує спрощеному правилу (X + Y )2 = X2 + Y 2.

Як показано на малюнку 1, 128-бітний рядок: цей рядок можна інтерпретувати кількома способами в контексті бінарної області. Його можна розглядати як унікальний елемент у 128-бітній бінарній області, або ж розглядати як два елементи області висотою 64 біти, чотири елементи області висотою 32 біти, 16 елементів області висотою 8 бітів або 128 елементів області F2. Гнучкість цього представлення не вимагає жодних обчислювальних витрат, це просто перетворення типу (typecast) рядка бітів, що є дуже цікавою та корисною властивістю. Одночасно елементи малих областей можуть бути упаковані в більші елементи областей без додаткових обчислювальних витрат. Протокол Binius використовує цю характеристику для підвищення обчислювальної ефективності. Крім того, в статті "On Efficient Inversion in Tower Fields of Characteristic Two" розглядається обчислювальна складність множення, зведення до квадрату та оберненої операції в n-бітних областях висоти двох (які можна розкласти на m-бітні підобласті).

2.2 PIOP: адаптована версія HyperPlonk Product та PermutationCheck------підходить для бінарного поля

Дизайн PIOP у протоколі Binius спирається на HyperPlonk і використовує ряд основних механізмів перевірки для верифікації правильності многочленів і множин з кількома змінними. Ці основні перевірки включають:

1. GateCheck: перевіряє, чи відповідають конфіденційне свідчення ω та відкритий вхід x обчислювальному відношенню C(x,ω)=0, щоб забезпечити правильну роботу схеми.

2. PermutationCheck: перевірка, чи є результати обчислення двох багатозмінних поліномів f та g на булевому гіперкубі перестановочними відношеннями f(x) = f(π(x)), щоб забезпечити узгодженість перестановок між змінними поліномів.

3. LookupCheck: перевірка значення многочлена на наявність у заданій таблиці пошуку, тобто f(Bµ) ⊆ T(Bµ), щоб забезпечити, що деякі значення знаходяться в заданому діапазоні.

4. MultisetCheck: перевіряє, чи є два багатозначні набори рівними, тобто {(x1,i,x2,)}i∈H={(y1,i,y2,)}i∈H, забезпечуючи узгодженість між кількома наборами.

5. ProductCheck: перевірка, чи дорівнює обчислення раціонального багаточлена на булевому гіперкубі певному заявленому значенню ∏x∈Hµ f(x) = s, щоб забезпечити правильність добутку багаточленів.

6. ZeroCheck: перевірка того, чи є будь-яка точка багатозмінного багаточлена на булевому гіперкубі нульовою ∏x∈Hµ f(x) = 0, ∀x ∈ Bµ, щоб забезпечити розподіл нулів багаточлена.

7. SumCheck: Перевіряє, чи є сума значень багатозмінного многочлена заявленим значенням ∑x∈Hµ f(x) = s. Знижує обчислювальну складність для верифікатора, перетворюючи задачу оцінки багатовимірного многочлена на задачу оцінки одномірного многочлена. Крім того, SumCheck також дозволяє пакетну обробку, вводячи випадкові числа для побудови лінійних комбінацій для реалізації пакетної обробки кількох випадків перевірки суми.

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

Хоча Binius і HyperPlonk мають багато спільного в дизайні протоколу, Binius покращив такі 3 аспекти:

• Оптимізація ProductCheck: у HyperPlonk ProductCheck вимагає, щоб знаменник U був ненульовим на всіх точках гіперкуба, а добуток мав дорівнювати певному значенню; Binius спростив цей процес перевірки, спеціалізувавши це значення на 1, що зменшує обчислювальну складність.

• Обробка проблеми ділення на нуль: HyperPlonk не зміг належним чином обробити ситуацію з діленням на нуль, що призвело до неможливості стверджувати, що U є ненульовим в гіперкубі; Binius правильно вирішив цю проблему, навіть у випадку, коли знаменник дорівнює нулю, ProductCheck від Binius також може продовжити обробку, дозволяючи розширення на будь-яке добуткове значення.

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

Отже, Binius покращив існуючий механізм PIOPSumCheck, підвищивши гнучкість і ефективність протоколу, особливо при обробці більш складних перевірок багатозмінних поліномів, надаючи більш потужну функціональну підтримку. Ці покращення не лише вирішують обмеження HyperPlonk, але й закладають основу для майбутніх систем доказів на основі бінарних полів.

2.3 PIOP: новий аргумент багаторазового зсуву ------ підходить для булевого гіперкуба

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

• Упаковка: цей метод оптимізує операції шляхом упаковування менших елементів, що знаходяться поруч у словниковому порядку, в більші елементи. Оператор Pack призначений для блоків розміром 2κ і групує їх.