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

1 Вступ

Основною причиною низької ефективності STARKs є те, що більшість чисел у реальних програмах є досить маленькими, наприклад, індекси в циклах 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 Аналіз принципів

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

• Інформаційно-теоретичне поліноінтерактивне oracle-доказ (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 включає п'ять ключових технологій, щоб досягти своєї ефективності та безпеки. По-перше, аритметика, заснована на вежах двійкових полів, складає основу його обчислень, що дозволяє виконувати спрощені обчислення в двійкових полях. По-друге, Binius у своєму інтерактивному Oracle доказовому протоколі (PIOP) адаптував HyperPlonk для перевірки добутків та перестановок, що забезпечує безпечну та ефективну перевірку узгодженості між змінними та їх перестановками. По-третє, протокол вводить новий багаторазовий зсув доказу, оптимізуючи ефективність перевірки багатолінійних зв'язків на малих полях. По-четверте, Binius використовує вдосконалену Lasso доказову перевірку, що надає механізму пошуку гнучкість та потужну безпеку. Нарешті, протокол використовує схему зобов'язань для малих поліномів (Small-Field PCS), що дозволяє реалізувати ефективну доказову систему на двійкових полях та зменшує накладні витрати, які зазвичай пов'язані з великими полями.

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

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

Термін "canonical" відноситься до єдиного та прямого способу представлення елементів у двійковій області. Наприклад, у найпростіший двійковій області F2 будь-який k-бітний рядок може бути безпосередньо відображений на k-бітний елемент двійкової області. Це відрізняється від просторової області, яка не може надати таке нормативне представлення в заданій кількості бітів. Хоча 32-бітна проста область може вмістити 32 біти, не кожен 32-бітний рядок може унікально відповідати елементу області, тоді як двійкова область має цю зручність однозначного відображення. У просторовій області Fp поширеними методами редукції є редукція Barrett, редукція Montgomery та спеціальні методи редукції для конкретних скінченних областей, таких як Mersenne-31 або Goldilocks-64. У двійковій області F2k поширеними методами редукції є спеціальна редукція (використовувана, наприклад, у AES), редукція Montgomery (використовувана, наприклад, у 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 використовує цю особливість для підвищення обчислювальної ефективності. Крім того, у статті «Про ефективне обернення в торових полях характеристик двох» обговорюється обчислювальна складність множення, піднесення до квадрату та обернення в 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 вдосконалено в трьох аспектах:

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

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

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

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

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

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

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