Это вторая часть нашей серии о математике, лежащей в основе STARK (первая часть здесь ), и первая из двух статей об арифметизации .

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

СТАРК в общих чертах

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

Сама арифметизация состоит из двух шагов: первый — генерация трассировки выполнения и полиномиальных ограничений, второй — преобразование этих двух объектов в один полином низкой степени. Что касается взаимодействия доказывающего и проверяющего, то на самом деле происходит то, что доказывающий и проверяющий заранее договариваются о полиномиальных ограничениях. Затем доказывающая сторона генерирует трассировку выполнения, и в последующем взаимодействии доказывающая сторона пытается убедить проверяющую в том, что полиномиальные ограничения удовлетворяются для этой трассировки выполнения, невидимой для верифицирующей стороны.

Резюме — Заявления о вычислительной целостности

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

Для простоты — мы рассматриваем это только как утверждение о том, что суммирование верно. Чтобы проверить, верно ли это утверждение CI, можно пройтись по списку, не пропуская ни одного пункта, чтобы вычислить общую сумму и сравнить ее с числом внизу квитанции. Это очень наивный пример, но мы будем использовать его далее в этой статье, чтобы продемонстрировать идею краткой тестируемости .

Арифметизация

Первый шаг арифметизации состоит в том, чтобы взять некоторое утверждение CI (например, «пятая транзакция в блоке 7218290 верна») и перевести его на формальный алгебраический язык. Это служит двум целям: 1) кратко и недвусмысленно определяет утверждение и 2) встраивает утверждение в алгебраическую область. Именно это вложение делает возможным второй этап арифметизации, который сводит оператор CI к утверждению о степени определенного многочлена.

Используемое нами алгебраическое представление состоит из двух основных компонентов: 1) трассировки выполнения и 2) набора полиномиальных ограничений. Трассировка выполнения — это таблица, в которой представлены шаги базовых вычислений, где каждая строка представляет собой один шаг. Набор полиномиальных ограничений строится таким образом, что все они выполняются тогда и только тогда, когда трасса представляет собой допустимое вычисление. Хотя трассировка выполнения может быть очень длинной, мы будем работать с кратким набором полиномиальных ограничений.

Трассировка выполнения

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

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

Мы можем, например, изучить эти две строки:

и убедитесь, что этот конкретный шаг вычислений (то есть число 16,41) правильный, поскольку 12,96+3,45=16,41. Обратите внимание, что одно и то же ограничение применяется к каждой паре строк. Это то, что мы подразумеваем под краткими ограничениями.

Полиномиальные ограничения

Перепишем чек супермаркета (с нарастающей суммой) в виде таблицы:

Обозначим значение ячейки в i-й строке и j-м столбце через A i,j (так мы будем обозначать нижний индекс, поскольку Medium не поддерживает LaTeX ). Теперь мы можем перефразировать условия корректности как этот набор полиномиальных ограничений:

Это линейные полиномиальные ограничения в A i,j . Если используемый нами набор полиномиальных ограничений имеет высокую степень, это отрицательно сказывается на длине доказательства и времени, необходимом для его создания. Следовательно, линейные ограничения — лучшее, на что мы можем надеяться. Обратите внимание, что (2) на самом деле является одним ограничением, применяемым несколько раз, и весь размер набора не зависит от длины квитанции.

В итоге мы взяли задачу CI о проверке чека супермаркета и преобразовали ее в краткую проверяемую трассировку выполнения и соответствующий набор полиномиальных ограничений, которые выполняются тогда и только тогда, когда общая сумма в исходном чеке верна.

Давайте рассмотрим более сложный пример.

Гипотеза Collatz

В 1937 году немецкий математик Лотар Коллатц выдвинул гипотезу в области теории чисел. На первый взгляд эта гипотеза может показаться просто милой математической головоломкой, но на самом деле это трудная нерешенная проблема в теории чисел. С годами она привлекла внимание многих математиков и приобрела множество синонимов (например, гипотеза 3 n + 1, гипотеза Улама, проблема Какутани и многие другие). Пауль Эрдёш однажды сказал об этой гипотезе: «Математика может быть не готова к таким задачам».

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

• Если предыдущий элемент четный: разделите его на 2.
• Если предыдущий элемент нечетный и больше 1: умножьте его на 3 и добавьте 1.
• Если предыдущий элемент равен 1, остановитесь.

Давайте рассмотрим простой пример, где начальный термин равен 52:

52 -> 26 -> 13 -> 40 -> 20 -> 10 -> 5 -> 16 -> 8 -> 4 -> 2 -> 1.

Гипотеза Коллатца: для любого положительного целого числа, с которого мы начинаем, последовательность всегда достигает 1.

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

Трассировка выполнения последовательности Коллатца

Утверждение CI: «Последовательность Коллатца, начинающаяся с 52, заканчивается на 1 после 11 итераций».

Пусть A будет трассировкой выполнения вычисления последовательности. i-я строка, обозначаемая A i , представляет i-е число в последовательности. Все числа представлены в виде двоичных строк, чтобы упростить выражение условия нечетности/четности с помощью полиномов. A i,j равно j-му младшему биту i-го числа последовательности. Например, A 0 =001011: первый член равен 52, его двоичное представление равно 110100, а затем мы обращаем порядок битов (обратный порядок битов упрощает индексацию в нотации полиномиальных ограничений).

Вот трассировка выполнения приведенной выше последовательности Коллатца, которая начинается с 52:

Обратите внимание, что здесь трасса имеет 6 столбцов, потому что 6 битов достаточно, чтобы представить даже самое большое число в последовательности. Если бы мы начали последовательность с 51, следующим числом было бы 154, поэтому для трассировки такой последовательности потребовалось бы не менее 8 столбцов.

Полиномиальные ограничения последовательности Collatz

Напомним, что искомые полиномиальные ограничения таковы, что все они выполняются тогда и только тогда, когда трасса A описывает заданную последовательность Коллатца (начиная с 52, заканчивая 1, и переход от любых двух последовательных строк выполнен правильно) . В нашем примере трасса A имеет размер 6x12, т. е. представляет собой последовательность Коллатца из 12 6-битных чисел. Набор полиномиальных ограничений следующий (n=12, m=6):

Давайте рассмотрим каждое из ограничений. Первые три понятны:

(1) выполняется тогда и только тогда, когда первая строка является двоичным представлением числа 52.

(2) выполняется тогда и только тогда, когда последняя строка является двоичным представлением 1.

(3) выполняется тогда и только тогда, когда след содержит только биты (число равно своему квадрату тогда и только тогда, когда оно равно 0 или 1).

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

Рассмотрим внимательно сами ограничения.

Для любого i<n-1 обозначим:

Следовательно, для каждого i<n-1 мы получаем следующее ограничение:

A i,0 — младший значащий бит i-го числа, определяющий его четность как целого числа, поэтому это ограничение описывает правило последовательности Коллатца.

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

Обратите внимание, что любая последовательность Коллатца длины n может быть представлена ​​с использованием трассы размера n*m, где m — максимальное количество битов в представлении числа в последовательности, и соответствующие полиномиальные ограничения изменяются соответствующим образом. Обратите внимание, что полиномиальные ограничения не растут с увеличением n и m, но остаются простыми и лаконичными.

При заданном первом члене последовательности Коллатца простая компьютерная программа может вывести трассировку выполнения и полиномиальные ограничения.

Вывод

В этом посте мы рассмотрели первый шаг в арифметизации операторов CI.

Мы видели, как оператор CI о последовательности Коллатца может быть преобразован в трассировку выполнения и кратко описанный набор полиномиальных ограничений. Подобные методы можно использовать для преобразования любых вычислений, и в целом любой оператор CI можно перевести в эту форму. Однако детали имеют большое значение. Хотя существует множество способов, которыми трассировка выполнения (и набор полиномиальных ограничений) может описывать конкретное вычисление, лишь немногие из них приводят к небольшому доказательству STARK, которое можно построить эффективно. Большая часть усилий в StarkWare направлена ​​на разработку сокращений, которые приводят к хорошим полиномиальным ограничениям, которые мы называем AIR (алгебраическое промежуточное представление), так как от этого во многом зависит производительность наших систем.

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

Кинерет Сигал и Шир Пелед
StarkWare