FS-FRI по Block–Tiwari

Аннотация

Расчёт проводится для двух исходных предпосылок: доказанной RBR-границы History и Гипотезы 1 Block–Tiwari. В обоих случаях минимум по целочисленному бюджету запросов находится без вычислений с плавающей точкой.

В сравнении Block и Tiwari каждая конфигурация FRI получает три значения: заявленный целевой уровень, доказуемую оценку после Fiat–Shamir и оценку при Гипотезе 1. Первые восемь строк таблицы взяты из их работы; последняя рассчитана для History B64/B255 по тому же определению и с тем же представлением в целых битах.

Организация	Репозиторий или конфигурация	Целевая безопасность 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	History B64 / B255	128	92	126

Как читать строку Parano1d

128 бит — целевой уровень. Оценка в 92 бита следует из доказанной RBR-границы History; оценка в 126 бит получается при использовании Гипотезы 1 Block–Tiwari. Как и в исходной таблице, показатели округляются вниз до целого числа битов; точные сертификаты приведены ниже.

Почему Fiat–Shamir меняет расчёт

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

Block и Tiwari формализуют эту стоимость в статье On the Concrete Security of Non-interactive FRI. Исходя из пораундовой (round-by-round, RBR) ошибки корректности интерактивного протокола, они применяют границу компилятора Fiat–Shamir и минимизируют ожидаемую стоимость атаки по всем бюджетам запросов.

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

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

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

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

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

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

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

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

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

Протокол имеет $\lambda$ бит безопасности по этому определению тогда и только тогда, когда $W(Q)\ge2^\lambda$ для каждого положительного целого $Q$ . Минимизация по $Q$ является частью метрики: произвольно выбрать удобный бюджет злоумышленника нельзя.

Параметры History B64/B255

Параметры протокола сверены с версией Parano1d 2cce53fc31a0bc173661bf5e07efaa56d8dc661b. HistoryStep — рекурсивное доказательство точного перехода блока от родительского State к дочернему State. B64 и B255 проверяют одно и то же отношение перехода, но рассчитаны соответственно на 64 и 255 пользовательских страниц транзакций. Их кодовые слова BaseFold содержат $2^{20}$ и $2^{21}$ позиций, тогда как скорость кода и число запросов у обоих классов одинаковы.

Точная арифметика, тексты теорем и регрессионные тесты для приведённых ниже расчётов опубликованы в исследовательском репозитории Parano1d QROM.

Параметр Block–Tiwari	Значение	Роль в расчёте
Поле	GF(2¹²⁸)	Ветвь размера поля в Гипотезе 1
Скорость FRI-кода $\rho$	1/4	Согласие и RBR-слагаемое при гипотезе
Число FRI-запросов $\ell$	125	Вероятность пропустить ошибку на финальных запросах
Длина выхода случайного оракула $\kappa$	256 бит	Слагаемое компилятора Fiat–Shamir
Целевой уровень в таблице	128 бит	Столбец цели в сравнении
Учёт proof of work	Нет	Строка непосредственно следует расчёту запросов Block–Tiwari

Размер поля и $\kappa$ — разные параметры. GF(2¹²⁸) определяет ветвь $2^{-128}$ ниже, а 256-битный дайджест — слагаемое Fiat–Shamir с множителем $2^{-256}$ . Block и Tiwari также фиксируют $\kappa=256$ , сравнивая протоколы над полями разных размеров.

Две RBR-предпосылки для одного набора параметров

Доказанная RBR-граница History

RBR-теорема для History рассматривает IOP над GF(2¹²⁸) с публичными случайными монетами, где обязательства заменены прямым доступом к оракулам. При относительном расстоянии $2/5$ каждый кандидат, сохранившийся до финального шага запросов, совпадает с исходным 32-столбцовым оракулом не более чем в доле $3/5$ позиций, если только один из более ранних вызовов проверяющей стороны не попал в явно учтённое исключительное множество.

Тридцать два столбца упаковываются в одно слово Рида—Соломона над фиксированным расширением степени 32. Списочное декодирование кратности пять оставляет не более одиннадцати исходных кандидатов. Теорема list-correlated agreement — коррелированного согласия списков — связывает каждый кандидат после свёрток с этим фиксированным списком. При переключении между кандидатами на алгебраическом вызове в границу включается объединение их множеств корней; фиксированность кандидата не предполагается. Наибольшая алгебраическая степень для одного кандидата равна 127.

Семейство RBR-шагов	Граница B64	Граница B255
Исключение list-correlated для свёрток	28 150 638 096 / 2¹²⁸	56 300 954 059 / 2¹²⁸
Алгебраическое переключение кандидатов	11 · 127 / 2¹²⁸
Совместное отношение sidecar	11 · 24 / 2¹²⁸
125 полных путей запросов	(3/5)¹²⁵

Для обоих классов наибольшим из четырёх значений оказывается слагаемое полных путей. Поэтому обобщённая RBR-ошибка знания равна

\varepsilon_{\mathrm{RBR}}^{\mathrm{proved}} =\max\!\left\{ \frac{U_5(n)}{2^{128}}, \frac{11\cdot127}{2^{128}}, \frac{11\cdot24}{2^{128}}, \left(\frac35\right)^{125} \right\} =\left(\frac35\right)^{125}.

Вне этих событий экстрактор возвращает корректный свидетель History. Значит, если проверяющая сторона принимает ложное утверждение, экстрактор обязательно завершился неудачей. Поэтому та же величина подходит в качестве RBR-предпосылки корректности для компилятора Block–Tiwari:

\boxed{ \varepsilon_{\mathrm{RBR}}^{\mathrm{proved}} =\left(\frac35\right)^{125}.}

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

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

\varepsilon_{\mathrm{RBR}}^{\mathrm{conj}} =\max\!\left\{\frac1{|\mathbb F|},\rho^\ell\right\}.

Подстановка поля, скорости и числа запросов даёт

\boxed{ \varepsilon_{\mathrm{RBR}}^{\mathrm{conj}} =\max\!\left\{2^{-128},(1/4)^{125}\right\} =\max\!\left\{2^{-128},2^{-250}\right\} =2^{-128}.}

Максимум определяется ветвью размера поля. Поэтому оба класса History входят в дальнейший расчёт с одинаковой доказанной величиной и одинаковой величиной при гипотезе.

Почему глобальная оптимизация сводится к двум целым числам

Обозначим $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$ и строго возрастает. Поэтому глобальный минимум находится в одной из двух соседних точек: в наибольшем $Q_0$ , где неотсечённая ошибка ещё меньше единицы, либо в $Q_1=Q_0+1$ — первой точке с отсечением.

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

Точное вычисление двух столбцов

Доказуемая безопасность FS-FRI

Для $a=(3/5)^{125}$ положим

D=5^{125}2^{256}, \qquad N(Q)=Q3^{125}2^{256}+3(Q^2+1)5^{125}.

Неотсечённая ошибка в точности равна $N(Q)/D$ . Целочисленное сравнение даёт единственную границу:

Q0 = 5,383,859,304,820,033,230,077,561,761   и N(Q0) < D
Q1 = 5,383,859,304,820,033,230,077,561,762   и N(Q1) ≥ D

В точке $Q_0$ :

epsilon_BT(Q0) = 0.999999999999999999999999999827291815635045301984…
W(Q0)          = 5,383,859,304,820,033,230,077,561,761.929836565411835132…

Точные рациональные сравнения доказывают $W(Q_0)\lt Q_1$ и

2^{92}\le W(Q_0)\lt2^{93}.

Следовательно, $Q_0$ — глобальная точка минимума, сертифицированное целое значение равно 92, а десятичное представление показателя составляет

\boxed{\lambda_{\mathrm{BT}}^{\mathrm{proved}} =92{,}120699270775770802\ldots\ \text{бита}.}

Безопасность FS-FRI при гипотезе

При $a=2^{-128}$ неотсечённая ошибка имеет точную целочисленную форму

\varepsilon_{\mathrm{BT}}^{\mathrm{conj}}(Q) =\frac{Q2^{128}+3(Q^2+1)}{2^{256}}.

Два соседних целых числа на границе отсечения равны

Q0 = 147,770,525,858,126,068,760,353,057,306,253,383,503
Q1 = 147,770,525,858,126,068,760,353,057,306,253,383,504

Q0·2^128 + 3(Q0^2+1) <  2^256
Q1·2^128 + 3(Q1^2+1) ≥ 2^256

Неотсечённый кандидат снова даёт меньшую работу:

epsilon_BT(Q0) = 0.999999999999999999999999999999999999995931834736…
W(Q0)          = 147,770,525,858,126,068,760,353,057,306,253,383,503.601154920268…

Точное сравнение даёт $W(Q_0)\lt Q_1$ и

2^{126}\le W(Q_0)\lt2^{127}.

Сертифицированное целое значение равно 126, а десятичное представление показателя составляет

\boxed{\lambda_{\mathrm{BT}}^{\mathrm{conj}} =126{,}796626145577656957\ldots\ \text{бита}.}

Что показывают два столбца

Доказуемое значение Parano1d выше всех значений в сравнении Block и Tiwari, кроме lambdaworks, включая 67 для 128-битной конфигурации Miden. Среди трёх строк lambdaworks оно выше 80-битной конфигурации и ниже конфигураций на 100 и 128 бит. Block и Tiwari отдельно отмечают lambdaworks как единственное семейство в своём сравнении, у которого доказанные значения остаются близки ко всем трём целям.

Показатель Parano1d при гипотезе на $1{,}203373854422\ldots$ бита ниже цели 128 бит, что после взятия целой части отображается как 126. Разность точных показателей Parano1d равна

126{,}796626145577\ldots -92{,}120699270775\ldots =34{,}675926874802\ldots\ \text{бита}.

В этой методике разность имеет точный смысл: столько дополнительной конкретной безопасности FS-FRI получается при замене доказанной RBR-предпосылки $(3/5)^{125}$ на предпосылку $2^{-128}$ из Гипотезы 1. Это не эффект округления и не величина, скрытая в столбце цели.

Воспроизведение целочисленных сертификатов

В публичном репозитории точный оптимизатор находится в crates/block-tiwari-rom, а оба результата проверяются регрессионными тестами:

git clone https://github.com/ignotusnemo/parano1d-qrom.git
cd parano1d-qrom

cargo test --release --locked --workspace
cargo run --release --locked -p scenarios -- block-tiwari-rom

Ни одно значение с плавающей точкой не участвует в выборе публикуемого целого числа. Для воспроизведения достаточно целых чисел произвольной точности и четырёх шагов:

задать числитель неотсечённой ошибки для выбранной RBR-предпосылки;
двоичным поиском найти наибольшее положительное целое $Q_0$ , при котором числитель меньше знаменателя;
точно как рациональные числа сравнить $W(Q_0)$ и $Q_0+1$ ;
сравнить выигравшее рациональное число с соседними степенями двойки.

Для доказанной предпосылки две проверки степеней двойки записываются без деления:

2^{92}N(Q_0)\le Q_0D\lt2^{93}N(Q_0).

Для предпосылки при гипотезе нужно заменить $D$ на $2^{256}$ , а $N(Q)$ — на $Q2^{128}+3(Q^2+1)$ . Напечатанных выше целых чисел на границе достаточно как регрессионных векторов для независимой реализации на SageMath, Rust, Python или в другой системе компьютерной алгебры. Репозиторий авторов на SageMath содержит эталонную реализацию их более широкого анализа параметров.

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

Ignotus Nemo, репозиторий Parano1d QROM: точная арифметика, тексты теорем, параметры и регрессионные тесты.
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.
Block, Garreta, Tiwari и Zając, Fiat–Shamir Security of FRI and Related SNARKs.
Версия Parano1d, использованная в этих расчётах.
Корректность Parano1d в отраслевых метриках — предыдущее исследование тех же конфигураций History в других опубликованных соглашениях.

Ignotus Nemo