Часть 3 из 4

Обратите внимание: этот пост в блоге содержит много математических обозначений. Поскольку не все мобильные телефоны поддерживают их в полной мере, мы рекомендуем вам прочитать его на настольном компьютере.

Введение

Это третья часть нашего глубокого погружения в StarkDEX, где мы описываем общую систему проверки STARK, одним из примеров которой является реализация StarkDEX. Если вы еще этого не сделали и хотите понять полную картину StarkDEX, мы рекомендуем прочитать части 1 и 2 , но вы также можете прочитать этот пост отдельно. Мы также рекомендуем вам прочитать нашу серию STARK Math для более глубокого обсуждения математических конструкций, необходимых для понимания этого поста.

В этом посте мы описываем систему доказательства STARK как интерактивный протокол между двумя сторонами, доказывающей и проверяющей. Доказывающая сторона отправляет серию сообщений, пытаясь убедить проверяющую, что определенное вычисление на некоторых входных данных было выполнено правильно (доказанное утверждение ). Верификатор отвечает на сообщения случайными значениями. В конце концов, верификатор принимает доказательство, если вычисления выполнены правильно, или отклоняет его (с высокой вероятностью), если это не так.

Хотя мы описываем систему как интерактивный протокол, следует отметить, что в альфа-версии StarkDEX эта интерактивность в конечном итоге заменяется преобразованием в неинтерактивную систему, в которой доказывающий предоставляет доказательство, а проверяющий решает, принять его или отклонить. .

Системы доказательства STARK

Если вы хотите обновить свое представление о трассировках выполнения и полиномиальных ограничениях, взгляните на наши публикации Arithmetization I и II из серии Stark Math.

След

Трассировка выполнения вычисления или, короче, трассировка — это последовательность состояний машины, по одному за такт. Если вычисление требует w регистров и длится N циклов, трассировка выполнения может быть представлена ​​таблицей размера N x w . Получив утверждение о правильности вычисления, доказывающая сторона сначала вычисляет трассу.

Обозначим столбцы трассы через f₁, f₂,…, fs. Каждое fⱼ имеет длину N=2ⁿ для некоторого фиксированного n. Значения в ячейках трассировки являются элементами большого поля F. В нашей альфа-версии F — это 252-битное поле простых чисел. Область оценки трассировки определяется как <g>, где g — генератор в подгруппе мультипликативной группы F. По сути, мы нумеруем строки трассировки элементами <g>. Каждый столбец трассировки интерпретируется как N точечных оценок полинома степени меньше N по области оценки трассы. Эти полиномы называются полиномами столбцов трассировки или , короче , полиномами столбцов .

Trace Low Degree Extension and Commitment

Как упоминалось выше, каждый столбец трассировки рассматривается как N оценок полинома степени меньше N. Для обеспечения безопасного протокола каждый такой полином оценивается в большей области, которую мы называем областью оценки. Например, в нашей StarkDEX Alpha размер оценочного домена обычно составляет 16*N. Мы называем эту оценку расширением низкой степени трассировки (LDE) , а отношение между размером области оценки и областью трассировки — коэффициентом расширения (те, кто знаком с обозначениями теории кодирования, заметят, что коэффициент расширения равен 1/скорость и LDE на самом деле является просто кодом трассы Рида-Соломона).

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

Листья дерева Меркла выбираются таким образом, что, если списание может включать несколько элементов поля вместе, они группируются в один лист Меркла. В случае LDE трассы это означает, что мы группируем все элементы поля в «строке» LDE трассы (оценка всех полиномов столбца в точке gⁱ) в один лист Меркла.

Ограничения

Трассировка выполнения действительна , если (1) выполняются определенные граничные ограничения и (2) каждая пара последовательных состояний удовлетворяет ограничениям, продиктованным вычислением. Например, если в момент времени t вычисление должно добавить содержимое 1-го и 2-го регистров и поместить результат в 3-й регистр, соответствующее ограничение будет иметь вид Trace[t,1]+Trace[t,2]-Trace[t+ 1, 3] = 0.

Ограничения выражаются в виде полиномов, составленных по ячейкам трассировки, которые удовлетворяются тогда и только тогда, когда вычисления верны. Следовательно, они называются полиномиальными ограничениями алгебраического промежуточного представления (AIR) на трассе. Например, в контексте доказательства правильности выполнения пакета транзакций на децентрализованной бирже (DEX) ограничения таковы, что все они выполняются тогда и только тогда, когда пакет транзакций действителен.

Давайте рассмотрим несколько примеров различных ограничений на ячейки трассировки.

1. f₂(x)-a = 0 для x=g⁷ (значение в столбце 2 строки g⁷ равно a ).
2. f₆²(x) -f₆(g³x) = 0 для всех x (квадрат значения в каждой строке столбца 6 равен значению на три строки вперед).
3. f₃(x) -f₄(gx) = 0 для всех x, кроме g⁵ (значение каждой строки в столбце 3 равно значению в столбце 4 на одну строку впереди во всех строках, кроме строки g⁵).
4. f₂(x) -2*f₅(x) = 0 для всех x в нечетной строке (значение каждой нечетной строки в столбце 2 равно удвоенному значению той же нечетной строки в столбце 5).

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

От полиномиальных ограничений к проблеме тестирования низкой степени

Далее мы представляем каждое ограничение как рациональную функцию. Ограничение (1) выше переводится в

Это многочлен степени не выше deg(f₂)-1 тогда и только тогда, когда выполняется ограничение (1) (подробнее см. в посте « Арифметизация 1» ). Чтобы понять преобразование ограничений (2), (3) и (4), вспомним сначала, что следующее множество {x∈ F | xᴺ-1=0} - это в точности все x в мультипликативной группе F. Следовательно, мы получаем следующие сокращения:

• Ограничение (2) выполняется тогда и только тогда, когда следующая рациональная функция является полиномом степени не выше 2*deg(f₆)-N:

• Ограничение (3) выполняется тогда и только тогда, когда следующая рациональная функция является полиномом степени не выше max{deg(f₃), deg(f₄)} — N+1:

• Ограничение (4) выполняется тогда и только тогда, когда следующая рациональная функция является полиномом степени не выше max{deg(f₂), deg(f₅)} — N/2:

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

Полиномиальная композиция

Чтобы эффективно доказать достоверность трассировки выполнения, мы стремимся к достижению следующих трех целей:

1. Составьте ограничения поверх полиномов трассы, чтобы применить их к трассе.
2. Отрегулируйте степени ограничений до одной степени, чтобы их можно было объединить в один полином этой степени.
3. Объедините ограничения в один (больший) полином, называемый составным полиномом , чтобы можно было использовать один тест низкой степени для подтверждения их (низкой) степени.

В этом разделе мы опишем, как выполняется вышеописанное.

Регулировка степени

Чтобы гарантировать надежность, нам нужно показать, что все отдельные ограничения, составленные из полиномов столбца трассировки, имеют низкую степень. По этой причине мы корректируем степень ограничений до наивысшей степени D из всех ограничений (а если D не является степенью двойки, до ближайшей степени двойки, большей, чем D). В результате это также становится степенью многочлена композиции.

Регулировка степени выполняется следующим образом:

Для ограничения Cⱼ(x) степени Dⱼ мы добавляем к многочлену композиции член вида

где 𝛼ⱼ и βⱼ — случайные элементы поля, отправленные верификатором. В результате, если композиционный многочлен имеет низкую степень, из этого автоматически следует, что отдельные ограничения также имеют низкую степень Dⱼ, как и требовалось. Результатом является составной полином вида:

где k — количество ограничений.

Объединение ограничений

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

Поскольку ограничения, используемые в нашей альфа-версии, имеют степень два или ниже, степень полинома композиции равна 2N. Следовательно, мы можем представить многочлен композиции H(x) в виде одного столбца оценок длины 2N или, как мы предпочитаем, в виде двух столбцов H₁(x) и H₂(x) длины N, где H(x) =H₁(x²)+xH₂(x²).

Соблюдение полинома композиции

Затем доказывающий выполняет еще одно расширение низкой степени двух столбцов полинома композиции, представляющих H₁ и H₂. Поскольку эти столбцы имеют ту же длину N, что и столбцы трассировки, мы иногда называем их полиномиальной трассировкой композиции и адресуем их расширение и фиксацию таким же образом, как и трассировку выполнения. Это делается путем их расширения на один и тот же коэффициент увеличения, группировки строк (пар элементов поля) в листья дерева Меркла, вычисления хеш-значений и отправки корня дерева в качестве обязательства.

Проверка согласованности в случайной точке (метод DEEP)

Обратите внимание, что значение H(x) для данной точки (элемента поля) z можно получить двумя способами: из H₁(z²) и H₂(z²) или путем вычисления упомянутой выше линейной комбинации ограничений. Это вычисление создает набор точек над столбцами трассировки, которые необходимо вычислить, чтобы выполнить необходимые вычисления. Набор точек, необходимый для вычисления H(x) для одной точки, называется маской . Следовательно, учитывая точку x = z, мы можем проверить согласованность между H и трассой, если нам даны значения H₁ (z²) и H₂ (z²) и значения индуцированной маски на трассе.

На этом этапе верификатор отправляет случайно выбранную точку z∊F. Доказывающая сторона отправляет обратно оценки H₁(z²) и H₂(z²) вместе с оценкой соответствующих элементов в маске, необходимой для вычисления H(z). Обозначим этот набор значений, отправленных доказывающим, через {yⱼ}. Для честного доказывающего значение каждого yⱼ равно fₖ(zgˢ), где k — столбец соответствующей ячейки, а sэто его смещение строки. Затем верификатор может вычислить H(z) двумя способами: на основе H₁ и H₂ (используя H(z)=H₁(z²)+z*H₂(z²)) и на основе значений маски yⱼ. Он подтверждает, что два результата идентичны. Остается показать, что значения, отправленные доказывающим на этом этапе, верны (т. е. действительно равны значениям маски точки z), что будет сделано в следующем разделе. Этот метод проверки согласованности между двумя полиномами путем выборки случайной точки из большого домена называется расширением домена для устранения претендентов (DEEP). Заинтересованный читатель может найти более подробную информацию в статье DEEP-FRI .

DEEP Композиционный полином

Чтобы убедиться, что значения DEEP, отправленные доказывающим, верны, мы создаем второй набор ограничений, а затем переводим его в задачу тестирования низкой степени, аналогично полиному композиции, определенному выше.

Для каждого значения yⱼ мы определяем следующее ограничение:

Рациональная функция является полиномом степени deg(fₖ)-1 тогда и только тогда, когда fₖ(zgˢ) = yⱼ. Обозначим размер маски через M. Проверяющий выбирает M+2 случайных элемента из поля {𝛼ⱼ}ⱼ . Мы называем полином, который является предметом тестирования низкой степени, полиномом композиции DEEP. Он определяется следующим образом:

(заметим, что в первом члене k и zgˢ, конечно, не константы, а зависят от j). Это (случайная) линейная комбинация ограничений вида:

где f — либо полином столбца трассировки, либо полином H₁/H₂. Таким образом, доказательство того, что эта линейная комбинация имеет низкую степень, подразумевает доказательство низкой степени полиномов столбца трассировки и полиномов H₁ и H₂, а также то, что значения DEEP верны.

Тестирование низкой степени

Протокол FRI для тестирования низкой степени

Для низкоуровневого тестирования мы используем оптимизированный вариант протокола, известного как FRI (что расшифровывается как Fast Reed - Solomon Interactive Oracle Proof of Proximity), и заинтересованный читатель может подробнее прочитать о нем здесь . Используемые оптимизации описаны в отдельном разделе ниже.

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

Фиксация фазы

В базовой версии FRI доказывающий разбивает исходный полином DEEP Constraint, обозначенный здесь как p₀(x), на два полинома степени меньше d/2, g₀(x) и h₀(x), удовлетворяющие p₀(x)=g₀ (x²)+x*h₀(x²). Верификатор выбирает случайное значение 𝛼₀, отправляет его доказывающему и просит доказывающего зафиксировать полином p₁(x)=g₀(x) + 𝛼₀*h₀(x). Обратите внимание, что p₁(x) имеет степень меньше d/2.

Затем мы продолжаем рекурсивно, разбивая p₁(x) на g₁(x) и h₁(x), затем выбирая значение 𝛼₁, строя p₂(x) и так далее. Каждый раз степень многочлена уменьшается вдвое. Следовательно, после log(d) шагов у нас остается постоянный многочлен, и доказывающая сторона может просто отправить постоянное значение верификатору.

Как может ожидать читатель, все вышеупомянутые обязательства по полиномиальным оценкам выполняются с использованием схемы обязательств Меркла, как описано выше.

Чтобы приведенный выше протокол работал, нам нужно свойство, состоящее в том, что для каждого z в домене L верно, что -z также находится в L. Более того, обязательство по p₁(x) будет не над L, а над L²={x² : х ∊ L}. Поскольку мы итеративно применяем шаг FRI, L² также должен удовлетворять свойству {z, -z} и т. д. Эти алгебраические требования удовлетворяются благодаря нашему выбору использования мультипликативного смежного класса в качестве области оценки.

Этап запроса

Теперь нам нужно проверить, не обманул ли доказывающий. Верификатор выбирает случайный z из L и запрашивает p₀(z) и p₀(-z). Этих двух значений достаточно, чтобы определить значения g₀(z²) и h₀(z²), как это видно из следующих двух линейных уравнений с двумя «переменными» g₀(z²) и h₀(z²):

Проверяющий может решить эту систему уравнений и вывести значения g₀(z²) и h₀(z²). Отсюда следует, что он может вычислить значение p₁(z²), которое является линейной комбинацией двух. Теперь верификатор запрашивает p₁(z²) и убеждается, что оно равно значению, вычисленному выше. Это служит указанием на то, что подтверждение p₁(x), которое было отправлено доказывающим на этапе фиксации, действительно правильное. Проверяющий может продолжить, запросив p₁(-z²) (напомним, что

(-z²)∊ L² и что обязательство по p₁(x) было дано на L²), и вывести из него p₂(z⁴).

Верификатор продолжает таким образом до тех пор, пока не использует все эти запросы для окончательного вывода значения P_h (z) для h=log(d). Но вспомните, что P_h (z) — это постоянный многочлен, постоянное значение которого было отправлено доказывающим на этапе фиксации до выбора z. Верификатор должен проверить, что значение, отправленное проверяющим, действительно равно значению, которое верификатор вычислил из запросов к предыдущим функциям.

Все ответы на запросы, полученные верификатором, также должны быть проверены на соответствие обязательствам Merkle, отправленным проверяющим на этапе фиксации. Следовательно, доказывающая сторона отправляет информацию о снятии фиксации (пути Меркла) вместе с этими ответами, чтобы позволить проверяющей стороне применить это.

Кроме того, верификатор также должен обеспечивать согласованность между полиномом p0 и исходными трассами, из которых он был получен (fⱼ и Hⱼ). Для этого для одного из двух запрошенных значений p₀(z) и p₀(-z) на этапе запроса доказывающая сторона также отправляет значения fⱼ и Hⱼ, индуцированные полиномом композиции DEEP, вместе с их снятием обязательств. Затем верификатор проверяет соответствие этих значений обязательствам на трассах, вычисляет значение p₀ и проверяет его соответствие значению p₀(z), отправленному проверяющим.

Для достижения требуемой надежности протокола фаза запроса повторяется несколько раз. Для коэффициента расширения 2ⁿ каждый запрос вносит примерно n битов безопасности.

Переход на неинтерактивный протокол (Fiat-Shamir)

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

Удаление интерактивности достигается с помощью конструкции BCS , метода, который сочетает Interactive Oracle Proof (IOP) , такой как протокол, описанный выше, с криптографической хэш-функцией для получения криптографического доказательства. Немного информации об этом механизме см. в нашем блоге .

Фундаментальные идеи, лежащие в основе этой конструкции, заключаются в том, что доказывающий имитирует получение случайности от верификатора. Это делается путем извлечения случайности из хеш-функции, которая применяется к предыдущим данным, отправленным доказывающим (и добавленным к доказательству). Такую конструкцию часто называют хэш-цепочкой . В нашей альфа-версии цепочка хеширования инициализируется путем хеширования общедоступных входных данных, известных как доказывающему, так и проверяющему. Дальнейшие технические детали опущены для простоты.

Оптимизация длины доказательства

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

Пропуск слоя FRI

Вместо того, чтобы фиксировать каждый из уровней FRI на этапе фиксации протокола FRI, доказывающая сторона может пропустить слои и зафиксировать только их подмножество. Делая это, доказывающая сторона сохраняет создание некоторых деревьев Меркла, а это означает, что на этапе запроса у нее остается меньше путей дефиксации для отправки верификатору. Однако есть компромисс. Если, например, прувер фиксирует только на каждом третьем слое, чтобы ответить на запрос, ему нужно декоммитировать 8 элементов первого слоя (вместо 2, которые он отправляет в стандартном случае). Доказывающая принимает этот факт во внимание на этапе подтверждения. Он упаковывает соседние элементы в каждом листе дерева Меркла. Таким образом, цена пропуска слоев заключается в отправке большего количества элементов поля, но не дополнительных путей аутентификации.

Последний слой FRI

Другая оптимизация FRI, используемая для уменьшения размера доказательства, заключается в завершении протокола FRI раньше, чем когда последний уровень достигает постоянного значения. В таком случае вместо того, чтобы доказывающая сторона отправляла только постоянное значение последнего слоя в качестве обязательства, доказывающая сторона вместо этого отправляет коэффициенты полинома, представляющего последний слой. Это позволяет верификатору завершить протокол, как и раньше, без необходимости принятия обязательств (и отправки отказов для элементов поля в меньших последних слоях). В нашей альфа-версии фаза фиксации FRI обычно завершается, когда достигается полином pⱼ степени меньше 64. Точное число может варьироваться в зависимости от размера трассы.

Шлифовка

Как упоминалось выше, каждый запрос добавляет определенное количество битов к безопасности (надежности) доказательства. Тем не менее, это также подразумевает отправку доказывающим большего количества отказов, что увеличивает размер доказательства. Одним из механизмов снижения потребности во многих запросах является увеличение стоимости создания ложного доказательства злоумышленником. Мы достигаем этого, добавляя к приведенному выше протоколу требование, согласно которому после всех обязательств, сделанных доказывающим, он также находит 256-битный одноразовый номер, который хешируется вместе с состоянием хеш-цепочки, что приводит к предварительно определенному шаблону требуемой длины. Длина шаблона определяет определенный объем работы, которую должен выполнить доказывающий, прежде чем сгенерировать случайность, представляющую запросы. Как результат, злонамеренный доказывающий, который пытается генерировать благоприятные запросы, должен будет повторять процесс измельчения каждый раз, когда изменяется обязательство. С другой стороны, честный прувер должен выполнить шлифование только один раз.

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

В нашей альфа-версии прувер должен выполнять шлифовку 32 бит. В результате количество запросов, необходимых для достижения определенного уровня безопасности, может быть уменьшено. С коэффициентом расширения 2⁴ это позволяет сократить количество запросов на 8.

Количество битов, используемых для измельчения, сообщается верификатору в качестве параметра. В случае несоответствия между доказательством и этим параметром верификатор отклоняет доказательство.

Периодические столбцы

Многие криптографические примитивы используют некоторые константы списка. Когда мы многократно применяем один и тот же криптографический примитив, мы получаем периодический список констант. Одним из вариантов использования этого списка в AIR является добавление его значений в трассировку и предоставление ограничений, гарантирующих правильность значений. Однако это расточительно, так как верификатор знает список значений и, таким образом, вычисление LDE и фиксация их не имеет смысла. Вместо этого мы используем метод, который мы называем периодическими столбцами . Периодическая структура каждого такого столбца приводит к полиному столбца, который может быть представлен кратко.В классическом представлении многочлена a₀+a₁*x+a₂*x²+…aₙ*xⁿ в виде вектора его коэффициента (a₀,…,aₖ) краткое представление означает, что большинство aⱼ являются нулями. Это позволяет верификатору эффективно вычислять точечные оценки этих полиномов.

Резюме

На этом завершается описание общей системы доказательства STARK, используемой системой StarkDEX. Описанная система проверки STARK сохраняет известные преимущества, такие как прозрачность (устранение доверенной установки), высокомасштабируемая проверка и постквантовая безопасность. Кроме того, он включает в себя несколько нововведений и оптимизаций, которые значительно уменьшают размер доказательства и повышают выразительную силу эффективно доказуемых утверждений способами, ранее не описанными в литературе.

В следующем и последнем посте этой серии мы опишем, как мы построили AIR (алгебраическое промежуточное представление) для StarkDEX. Как всегда, если у вас есть какие-либо вопросы или комментарии, обращайтесь к нам здесь или в твиттере @StarkWareLTD .

Кинерет Сигал и Гидеон Кемпфер

StarkWare