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

1. Введение

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

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

В отличие от исследований有限域, таких как Goldilocks, BabyBear, Mersenne31 в последние несколько лет, исследования двоичных полей восходят к 80-м годам прошлого века и широко применяются в криптографии, таких как AES(F28域), GMAC(F2128域), QR码(F28域Reed-Solomon编码) и т.д.

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. Эта гибкость не требует вычислительных затрат, это всего лишь преобразование типа для битовой строки.

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

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

Binius улучшил в следующих трех областях:

• Оптимизация ProductCheck: специализированное значение 1, упрощение процесса проверки для снижения вычислительной сложности

• Обработка проблемы деления на ноль: правильная обработка случаев, когда знаменатель равен нулю, позволяет обобщить на любое значение произведения

• Перекрестная проверка перестановок: поддержка проверки перестановок между несколькими столбцами для обработки более сложных многочленных перестановок.

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

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

• Упаковка: упаковать элементы с меньшими значениями, расположенные рядом в словаре, в более крупные элементы для оптимизации операций

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

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

Протокол Lasso позволяет стороне-доказателю заверять вектор a ∈ Fm и доказывать, что все элементы присутствуют в заранее определенной таблице t ∈ Fn.

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

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

Основная идея BiniusPCS заключается в упаковке. Предоставляет 2 решения на основе бинарного поля для многочленных обязательств Brakedown:

1. Использовать экземпляр объединенного кода

2. Использование технологии кодирования на уровне блоков, поддержка отдельного применения кодов Рида-Соломона

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

3. Оптимизация мышления

3.1 GKR-based PIOP: основанный на GKR бинарный домен умножения

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

Умножение на основе GKR требует только одного вспомогательного обязательства, что делает алгоритм более эффективным за счет сокращения накладных расходов на Sumchecks, особенно в случаях, когда операции Sumchecks дешевле генерации обязательств.

3.2 ZeroCheck PIOP оптимизация: баланс между затратами на вычисления Prover и Verifier

Уменьшение передачи данных со стороны доказателя: передача части работы на сторону проверяющего, снижение объема данных, отправляемых доказателем.

Сокращение количества оценочных точек доказательства: изменение способа отправки многочлена, уменьшение количества оценочных точек.

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

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

Влияние и фактор улучшения переключения раундов: выбор переключения раундов t влияет на производительность, фактор улучшения для оптимальной точки переключения достигает максимального значения.

Влияние размера базового поля на производительность: преимущества оптимизированного алгоритма более выражены для меньшего базового поля (, такого как GF[2]).

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

Увеличение эффективности памяти: требования к памяти алгоритма 4 O(d·t), алгоритм 3 O(2d·t), подходит для ограниченных ресурсов.

3.4 PCS оптимизация: FRI-Binius снижение размера доказательства Binius

FRI-Binius реализует механизм сжатия двоичных областей FRI, что приносит 4 основных инновации:

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

С помощью FRI-Binius можно уменьшить размер доказательства Binius на порядок, приближаясь к самым современным системам.

4. Резюме

Binius практически устранил узкие места, связанные с подтверждением коммита Prover, новое узкое место связано с протоколом Sumcheck. Решение FRI-Binius является вариантом FRI и может устранить накладные расходы на внедрение на уровне доказательства поля.

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

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