Анализ принципов Binius STARKs и размышления об оптимизации

1. Введение

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

Первое поколение кодирования STARKs имеет ширину в 252 бита, второе поколение — 64 бита, третье поколение — 32 бита, но 32-битное кодирование по-прежнему имеет много неиспользуемого пространства. В сравнении, двоичное поле позволяет напрямую управлять битами, что делает кодирование компактным и эффективным без произвольных потерь пространства, то есть четвертое поколение STARKs.

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

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

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

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

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

2.1 Ограниченные области: арифметика на основе башен двоичных полей

Преимущества башенной двоичной области:

• Высокоэффективные вычисления: бинарное поле по своей сути поддерживает высокоэффективные арифметические операции
• Эффективная арифметика: структура двоичного поля поддерживает упрощенный арифметический процесс
• Нормативное представление: элементы в двоичном поле имеют уникальный и прямой способ представления.

Преимущества двоичных областей:

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

2.2 PIOP: адаптированная версия HyperPlonk Product и PermutationCheck

Механизм проверки ядра Binius PIOP:

• ГейтЧек
• Проверка перестановок
• LookupCheck (LookupCheck)
• МультисетЧек
• Проверка продукта
• Нулевой чек
• СуммЧек
• Пакетная проверка

Улучшения Binius для HyperPlonk:

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

2.3 PIOP: новый аргумент многомерного сдвига

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

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

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

Состав протокола Lasso:

• Абстракция виртуальных многочленов больших таблиц
• Поиск по малой таблице
• Множественная проверка

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

• Введение версии Lasso-протокола с мультипликацией
• Требуется, чтобы доказательная сторона пообещала вектор счётчиков чтения, который никогда не равен нулю.

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

Основная идея: упаковка

Два варианта многочленной обязательной схемы 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 процесс:

• Этап обязательств
• Этап оценки

4. Резюме

Ценностное предложение Binius:

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

Решение FRI-Binius:

• Устранение накладных расходов на встраивание из уровня доказательства домена
• Не приведет к резкому росту затрат на уровень агрегированных доказательств

Текущий прогресс:

• Команда Irreducible разрабатывает рекурсивный уровень в сотрудничестве с Polygon для создания zkVM на основе Binius
• JoltzkVM переходит от Lasso к Binius
• Команда Ingonyama реализовала FPGA версию Binius

! Исследование Bitlayer: Анализ принципов Биниуса СТАРКСА и оптимизационное мышление