FS-FRI по Block–Tiwari

Аннотация

Parano1d проверяет переходы State с помощью HistoryStep, рекурсивного доказательства, которое добавляется к каждому принятому блоку. Его штатные параметры безопасности подставляются в компилятор Fiat–Shamir Block–Tiwari. Обобщённая RBR-граница выводится из теорем о согласии коррелированных списков для кодов Рида–Соломона с явным учётом переключения кандидатов, а минимум ожидаемой работы находится по всем положительным целочисленным бюджетам запросов. Оба точных минимума лежат в интервале от 127 до 128 бит.

Преобразование Fiat–Shamir заменяет случайные монеты проверяющей стороны в интерактивном FRI выходами случайного оракула. Недобросовестная доказывающая сторона может многократно обращаться к этому оракулу в поисках выгодного транскрипта, поэтому конкретная стоимость подделки зависит от полного бюджета запросов. Block и Tiwari определяют эту стоимость как минимальную ожидаемую работу успешной подделки в запросах к случайному оракулу по всем положительным целочисленным бюджетам.

К каждому принятому блоку Parano1d добавляет рекурсивное доказательство HistoryStep. Оно доказывает, что применение блока к ранее проверенному State даёт новый State, и внутри того же отношения проверяет предыдущее доказательство HistoryStep. Так текущее доказательство продолжает проверенную последовательность переходов State. В этой статье компонент FS-FRI данного рекурсивного доказательства State оценивается по методике Block–Tiwari.

Первые восемь строк ниже опубликованы Block и Tiwari. Строка Parano1d использует те же формулы, ту же настройку случайного оракула на 256 бит и то же представление в целых битах.

Организация	Репозиторий или конфигурация	Целевая стойкость FRI	Доказуемая стойкость FS-FRI	Предполагаемая стойкость FS-FRI
Polygon	Plonky2	100	38	99
StarkWare	stone-prover	96	54	99
StarkWare	SHARP Verifier	96	59	95
dYdX	dYdX Protocol	80	52	79
Polygon Miden	Miden-VM	96 / 128	45 / 67	96 / 128
Lambda Class	lambdaworks	80 / 100 / 128	81 / 99 / 127	81 / 101 / 129
RISC Zero	RISC Zero	100	37	99
Matter Labs	era-boojum	100	50	99
Parano1d	Recursive State proof (HistoryStep)	128	127	127

Строка Parano1d

Точные показатели ожидаемой работы равны $127{,}194502224322\ldots$ бита для доказанной RBR-предпосылки и $127{,}207518749639\ldots$ бита при Гипотезе 1 Block–Tiwari. Оба точных значения лежат в интервале $[127,128)$ , поэтому в обоих столбцах указано 127 бит.

Метрика Block–Tiwari

Пусть классический противник делает не более $Q$ запросов к случайному оракулу

H:\{0,1\}^{*}\longrightarrow\{0,1\}^{\kappa}.

Если пораундовая ошибка корректности исходного интерактивного протокола равна $\varepsilon_{\mathrm{RBR}}$ , то Лемма 1 Block и Tiwari даёт следующую ошибку адаптивного неинтерактивного доказательства в модели случайного оракула:

\varepsilon_{\mathrm{BT}}(Q) =\min\!\left\{ 1,\; Q\varepsilon_{\mathrm{RBR}} +\frac{3(Q^2+1)}{2^\kappa} \right\}.

Первое слагаемое переносит интерактивную RBR-ошибку на все попытки обращения противника к оракулу. Квадратичное слагаемое является конечной стоимостью компилятора Fiat–Shamir. Внешний минимум ограничивает вероятность успеха единицей.

Попытка с $Q$ запросами успешна с вероятностью не выше $\varepsilon_{\mathrm{BT}}(Q)$ . Повторение попытки до первой успешной подделки требует в среднем

W(Q)=\frac{Q}{\varepsilon_{\mathrm{BT}}(Q)}

запросов к оракулу. Поэтому Определения 1 и 2 задают показатель конкретной стойкости

\lambda_{\mathrm{BT}} =\log_2\!\left( \min_{Q\in\mathbb Z_{>0}}W(Q) \right).

Целое значение равно наибольшему $k$ , для которого $W(Q)\ge2^k$ при каждом положительном целом $Q$ . Минимизация по $Q$ входит в само определение.

Штатные параметры

Исполняемый расчёт встроен в Parano1d как crate noid_soundness. Его загрузчик штатных параметров напрямую импортирует все входные значения анализа стойкости из тех же crates, что prover и verifier, и отклоняет нарушение соответствия между компонентами. Текущий mainnet-релиз содержит тот же связанный с исходным кодом расчёт.

Расчёт безопасности одинаков для всего штатного диапазона вместимости блока. Меняется только размер трассы. B25 охватывает до 25 эффективных позиций страниц, а B255 охватывает от 26 до 255. Оба класса доказывают отношение HistoryStep с одинаковой скоростью кода, числом запросов и распределением вызовов, поэтому дают один результат по Block–Tiwari.

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

Параметр	Штатное значение
Размер трассы	B25: исходное кодовое слово 2¹⁹, слои теоремы от 2⁷ до 2¹⁹. B255: исходное кодовое слово 2²¹, слои теоремы от 2⁹ до 2²¹.
Скорость кода $\rho$	1/4
Число запросов BaseFold $\ell$	133
Поле зафиксированной трассы	GF(2¹²⁸)
Пространство алгебраических вызовов	Подмножество элементов GF(2²⁵⁶) с единичным следом, размер 2²⁵⁵
Выход случайного оракула $\kappa$	256 бит
Максимальное число алгебраических корней для одного кандидата	127
Число корней совместного sidecar для одного кандидата	36

Размер пространства вызовов и разрядность хеша являются разными параметрами. Знаменатель вероятностей неблагоприятных алгебраических ответов равен $2^{255}$ , а знаменатель слагаемого компилятора Fiat–Shamir равен $2^{256}$ . Финальный предикат nonce для proof of work не уменьшает RBR-границу.

Доказанная RBR-предпосылка

RBR-теорема формулируется для IOP с публичными случайными монетами, прямым доступом вместо Merkle-обязательств и без grinding. Пусть $m\ge3$ является целым параметром кратности декодирования Джонсона. Определим

h=m+\frac12, \qquad \gamma=\frac{m-1}{2m}, \qquad s_N=\frac{N-4}{2N}.

Для слоя Рида–Соломона длины $N$ со скоростью 1/4 приведённая скорость в принятом теоремой о согласии коррелированных списков соглашении о степенях равна

\rho_N=\frac{N/4-1}{N}=\frac14-\frac1N.

Прямое вычисление даёт $s_N^2\lt\rho_N$ . Требование к кратности выполняется на каждом штатном слое:

\left\lceil \frac{\sqrt{\rho_N}} {1-\sqrt{\rho_N}-\gamma} \right\rceil\le m.

Подстановка в Теорему 4.6 работы Ben-Sasson, Carmon, Haböck, Kopparty и Saraf с использованием строгой рациональной нижней границы $s_N\lt\sqrt{\rho_N}$ даёт целочисленную верхнюю границу числа исключительных вызовов

A_N(m)=\left\lfloor N\frac{2h^5+3h\gamma s_N^2}{3s_N^3} +\frac{h}{s_N} \right\rfloor.

Соответствующая строгая граница размера списка для исходного кодового слова равна

L_N(m)=\left\lceil\frac{h}{s_N}\right\rceil-1, \qquad L_{\max}(m)=\max\!\left\{ L_{2^{19}}(m),L_{2^{21}}(m) \right\}.

Для 133 независимо выбранных позиций слагаемое ухода от проверки при списочном декодировании имеет вид

E_q(m)=\left(\frac{m+1}{2m}\right)^{133}.

Объединение ухода от запросов, всех исключений близости в двух расписаниях слоёв, переключения кандидатов и совместного отношения sidecar даёт

\begin{aligned} \kappa_H(m)=\max\{& E_q(m),\\ &\max_{N\in\mathcal N_{25}\cup\mathcal N_{255}} \frac{A_N(m)}{2^{255}},\\ &\frac{127L_{\max}(m)}{2^{255}}, \frac{36L_{\max}(m)}{2^{255}} \}. \end{aligned}

Здесь $\mathcal N_{25}=\{2^7,\ldots,2^{19}\}$ и $\mathcal N_{255}=\{2^9,\ldots,2^{21}\}$ , причём в каждом множестве берутся последовательные степени двойки.

Как учитывается переключение кандидатов

Тридцать две перемежающиеся исходные строки упаковываются в одно слово Рида–Соломона над фиксированным расширением степени 32. Упаковка сохраняет столбцовое расстояние Хэмминга и задаёт единый исходный список размера не более $L_{\max}(m)$ . При каждом свёртывании пакета строк или позиции вне исключительного множества теорема о согласии коррелированных списков связывает выбранного после свёртки кандидата с коррелированными кандидатами до свёртки на том же взвешенном множестве совпадений. Бабочка аддитивного NTT обратима, поэтому сведение BaseFold к аддитивному FFT из работы Haböck применяется к штатному расписанию свёрток.

Каждый восстановленный кандидат совпадает с зафиксированными строками основного поля более чем в $N/2$ позициях, а его степень меньше $N/4$ . Сопряжение Фробениуса и единственность полинома вынуждают разложенные строки принадлежать вложенному подполю GF(2¹²⁸). Все последующие ложные тождества являются ненулевыми полиномами от следующего вызова проверяющей стороны. Объединение их корней по полному исходному списку даёт слагаемые с 127 и 36 корнями. Ни на одном шаге не предполагается, что доказывающая сторона сохраняет одного кандидата.

Сгруппированные эпохи Merkle только сокращают детерминированные пути свёрток и не добавляют непроверенных шагов. Взвешенный обратный граф ограничивает оставшуюся принимаемую долю для одного запроса величиной $(m+1)/(2m)$ . Независимость 133 позиций даёт $E_q(m)$ .

Полный перечень степеней для штатного верификатора:

Шаг верификатора	Максимум корней для одного кандидата
Сжатие публичного входа	7
Многолинейная точка sidecar	19
Совместное объединение девяти групп sidecar	36
Раунд sumcheck для ragged walk	8
Сжатие координат zerocheck	18
Интерполяционный вызов zerocheck	127
Отложенная внутренняя координата	63
Остальные раунды sumcheck	2
Совместная агрегация lincheck или утверждений PCS	1

Экстрактор без перемотки выполняет списочное декодирование упакованного исходного слова, раскладывает каждого кандидата на 32 строки основного поля, обращает аддитивное NTT и оставляет кандидата только после успешной проверки точного отношения History. Обратная индукция по заведомо безуспешным префиксам показывает, что принимаемый транскрипт без свидетеля должен покинуть это множество через одно из четырёх событий в $\kappa_H(m)$ . Тем самым получается обобщённая пораундовая граница знания, а не только оценка финального принятия.

Точная оптимизация кратности

При росте $m$ величина $E_q(m)$ уменьшается, а слагаемые близости и размера списка не уменьшаются. После их единственного пересечения достаточно сравнить две соседние кратности. Точный целочисленный двоичный поиск и одно рациональное сравнение выбирают

m_*=861824, \qquad L_{\max}(m_*)=1723655.

Четыре слагаемых при $m_*$ равны:

RBR-слагаемое	Точное значение
Уход от запросов	$(861825/1723648)^{133}$
Максимальное исключение близости слоя	$5317717993529868433397264455583323037/2^{255}$
Переключение кандидатов	$218904185/2^{255}$
Совместный sidecar	$62051580/2^{255}$

Точное сравнение показывает, что максимумом является слагаемое ухода от запросов. Поэтому доказанная RBR-предпосылка для компилятора Block–Tiwari равна

\boxed{ \varepsilon_{\mathrm{RBR}}^{\mathrm{provable}} =\left(\frac{861825}{1723648}\right)^{133}.}

Предпосылка Гипотезы 1

При расчёте предполагаемой стойкости Block и Tiwari считают оптимальной лучшую известную информационно-теоретическую атаку на FRI. Здесь используется размер пространства алгебраических вызовов, а не номинальный размер поля зафиксированной трассы. Подстановка штатной скорости, числа запросов и размера пространства даёт

\begin{aligned} \varepsilon_{\mathrm{RBR}}^{\mathrm{conjectured}} &=\max\!\left\{2^{-255},(1/4)^{133}\right\}\\ &=\max\!\left\{2^{-255},2^{-266}\right\}\\ &=2^{-255}. \end{aligned}

Доказанная и предполагаемая предпосылки являются разными точными вероятностями. Далее они подставляются в один компилятор Fiat–Shamir и один оптимизатор ожидаемой работы.

Точный глобальный оптимизатор

Обозначим $a=\varepsilon_{\mathrm{RBR}}$ и $b=3/2^{256}$ . До отсечения ошибки компилятора единицей

W(Q) =\frac{Q}{aQ+b(Q^2+1)} =\frac1{a+b(Q+1/Q)}.

Для положительных целых $Q$ величина $Q+1/Q$ не убывает, поэтому $W(Q)$ не возрастает на всём неотсечённом участке. После отсечения $W(Q)=Q$ строго возрастает. Следовательно, глобальный минимум находится либо в последнем неотсечённом целом, либо в первом отсечённом целом. Точный двоичный поиск находит границу, а одно рациональное сравнение выбирает минимум.

Доказуемая стойкость FS-FRI

последний неотсечённый Q = 194697534987145646766651744479049925879
первый отсечённый Q      = 194697534987145646766651744479049925880
глобальный минимум находится в последнем неотсечённом Q

Подстановка доказанной RBR-дроби и точное перекрёстное умножение дают

2^{127} \le \min_{Q\in\mathbb Z_{>0}}W_{\mathrm{provable}}(Q) \lt 2^{128}.

Десятичное представление логарифма точного рационального минимума равно

\boxed{ \lambda_{\mathrm{BT}}^{\mathrm{provable}} =127{,}194502224322\ldots\ \text{бита}.}

Предполагаемая стойкость FS-FRI

последний неотсечённый Q = 196462116142286827589391637123844718210
первый отсечённый Q      = 196462116142286827589391637123844718211
глобальный минимум находится в первом отсечённом Q

Предполагаемый минимум в точности равен первому отсечённому бюджету запросов. Целочисленное сравнение даёт

2^{127} \le \min_{Q\in\mathbb Z_{>0}}W_{\mathrm{conjectured}}(Q) \lt 2^{128},

а десятичный показатель равен

\boxed{ \lambda_{\mathrm{BT}}^{\mathrm{conjectured}} =127{,}207518749639\ldots\ \text{бита}.}

Два значения в целых битах сертифицируют не десятичные логарифмы, а точные неравенства со степенями двойки.

Как читать сравнение

Доказуемое значение Parano1d совпадает с наибольшим доказуемым целым значением в опубликованной таблице Block–Tiwari. Предполагаемое значение на один бит ниже 128-битной конфигурации Miden и на два бита ниже 128-битной конфигурации lambdaworks. Оба значения Parano1d на один целый бит ниже заданной цели 128 бит.

Совпадение двух отображаемых столбцов Parano1d не отождествляет доказанную предпосылку с Гипотезой 1. Их RBR-вероятности и точные минимумы ожидаемой работы различаются. Слагаемое коллизий 256-битного случайного оракула помещает оба минимума в один интервал целых битов.

Воспроизведение сертификата

Репозиторий Parano1d содержит связанные с исходным кодом параметры, специализацию теоремы, точный оптимизатор и регрессионные тесты. Воспроизведите расчёт из текущего mainnet-релиза:

git clone https://git.parano1d.org/ignotusnemo/parano1d.git
cd parano1d
git checkout v1.0.1
cargo run --release --locked -p noid_soundness
cargo run --release --locked -p noid_soundness -- --exact
cargo test --release --locked -p noid_soundness

Обычный запуск выводит три значения в целых битах. Запуск с --exact выводит обе RBR-дроби, выбранную кратность, обе границы отсечения, оба минимизирующих бюджета запросов и обе точные дроби ожидаемой работы. Тесты фиксируют параметры W65/H133, покрывают оба штатных размера трассы, отклоняют несогласованные межкомпонентные параметры и проверяют каждый сертификат степеней двойки в целой или рациональной арифметике произвольной точности.

Полный вывод находится в noid_soundness/docs/block-tiwari.md. Точная реализация разделена между src/local.rs с RBR-теоремой и src/block_tiwari.rs с оптимизатором Block–Tiwari.

Первоисточники

Ignotus Nemo, встроенный сертификат корректности Parano1d: связанные с исходным кодом штатные параметры, специализация теоремы, точная арифметика и регрессионные тесты.
Alexander R. Block и Pratyush Ranjan Tiwari, On the Concrete Security of Non-interactive FRI, в особенности Определения 1 и 2, Лемма 1, Гипотеза 1, Раздел 4 и Таблица 1.
Block и Tiwari, FRI Parameter Testing in SageMath.
Alexander R. Block, Albert Garreta, Jonathan Katz, Justin Thaler, Pratyush Ranjan Tiwari и Michał Zając, Fiat–Shamir Security of FRI and Related SNARKs.
Eli Ben-Sasson, Dan Carmon, Ulrich Haböck, Swastik Kopparty и Shubhangi Saraf, On Proximity Gaps for Reed–Solomon Codes, Теорема 4.6.
Ulrich Haböck, BaseFold in the List Decoding Regime.

Ignotus Nemo