TL;DR

• Рекурсивное доказательство работает в основной сети, масштабируя приложения StarkEx, а также StarkNet с помощью одного доказательства.
• Это повышает масштабируемость и обеспечивает преимущества в плане затрат и задержки (редкий и захватывающий случай, когда масштаб и задержка движутся в тандеме, а не являются компромиссом).
• Это готовит почву для L3 и других преимуществ
• Прочтите статью в блоге о рекурсивном доказательстве . Это крутая штука 😉

Масштабирование!

Рекурсивные доказательства, основанные на общих вычислениях Каира, сейчас находятся в производстве. Это знаменует собой значительное повышение мощности масштабирования L2 с помощью STARK. Это быстро обеспечит многократное увеличение количества транзакций, которые могут быть записаны в Ethereum с помощью одного доказательства.

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

Этот метод в настоящее время используется для множества приложений на основе Cairo: приложений, работающих на StarkEx, механизма масштабирования StarkWare SaaS и StarkNet, не требующего разрешения накопительного пакета.

История до сих пор

С момента первого доказательства в основной сети в марте 2020 года следующие разработки повлияли на то, как используются STARK.

Масштабирование на основе STARK

В июне 2020 года первое решение для масштабирования на основе STARK — StarkEx — было развернуто в основной сети Ethereum. У StarkEx есть Prover, который выполняет большие вычисления вне сети и создает STARK-доказательство их правильности, а также Verifier, который проверяет это доказательство в сети. Ограничения для этого первого развертывания были «написаны от руки» инженерами StarkWare, что значительно ограничивало скорость запуска StarkEx. Мы пришли к выводу, что необходим язык программирования для поддержки общих вычислений — Cairo.

Cairo

Летом 2020 года Cairo впервые появился в основной сети Ethereum . Cairo означает CPU Algebraic Intermediate Representation (AIR) и включает в себя один AIR, который проверяет набор инструкций этого «CPU». Это открыло двери для кодирования доказательств для более сложной бизнес-логики, для произвольных вычислительных операторов и для более быстрого и безопасного способа. Программа Cairo может подтвердить выполнение логики одного приложения. Но программа Cairo также может быть конкатенацией нескольких таких приложений — SHARP.

SHARP

SHARP — SHARed Prover — берет транзакции из нескольких отдельных приложений и доказывает их все в одном STARK-доказательстве. Приложения объединяют свои пакеты транзакций, быстрее заполняя емкость STARK-доказательств. Транзакции обрабатываются с улучшенной скоростью и задержкой. Следующий рубеж: рекурсивные доказательства, но не только для какой-то жестко закодированной логики, но и для общих вычислений .

Чтобы понять все преимущества рекурсивного доказательства, стоит немного больше узнать о том, как (нерекурсивное) доказательство выполнялось SHARP до сих пор. На рисунке 1 изображен типичный нерекурсивный поток:

Здесь заявления приходят с течением времени. Когда достигается определенный порог мощности (или времени), генерируется большой комбинированный оператор (он же Train). Это комбинированное утверждение доказано только после того, как будут получены все отдельные утверждения. Это доказательство требует много времени для доказательства (примерно сумма времени, необходимого для доказательства каждого утверждения в отдельности).

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

Что такое рекурсивное доказательство?

С доказательствами STARK время, необходимое для доказательства утверждения, примерно линейно со временем, которое требуется для выполнения утверждения. Кроме того, если доказательство утверждения занимает T времени, то проверка доказательства занимает примерно log(T) времени, которое обычно называется «логарифмическим сжатием». Другими словами, в STARK вы тратите гораздо меньше времени на проверку утверждения, чем на его вычисление.

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

Вот где появляется возможность выполнить рекурсию : так же, как мы пишем программу Cairo, которая доказывает правильность тысяч транзакций, мы также можем написать программу Cairo, которая проверяет несколько доказательств STARK. Мы можем сгенерировать одно доказательство, свидетельствующее о достоверности нескольких «восходящих» доказательств. Это то, что мы называем рекурсивным доказательством.

Из-за логарифмического сжатия и примерно линейного времени доказательства проверка доказательства СТАРКа занимает относительно короткое время (ожидается, что в ближайшем будущем это будет всего несколько минут).

При реализации рекурсии SHARP может проверять утверждения по их поступлению. Их доказательства можно снова и снова объединять в рекурсивные доказательства по различным шаблонам, пока в определенный момент полученное доказательство не будет отправлено в контракт с верификатором в цепочке. Типичная схема изображена на рисунке 2:

В этом примере в SHARP отправляются четыре оператора (возможно, из четырех разных источников). Каждое из этих утверждений доказывается параллельно. Затем каждая пара доказательств проверяется оператором Recursive Verifier — программой Cairo, которая проверяет доказательство STARK, — для которого генерируется доказательство. Это утверждение утверждает, что правильность двух доказательств проверена. Затем два доказательства снова объединяются оператором Recursive Verifier. Это приводит к одному доказательству, подтверждающему все четыре исходных утверждения. Затем это доказательство может быть окончательно отправлено в цепочку для проверки смарт-контрактом верификатора Solidity.

Непосредственные преимущества рекурсивного доказательства

Сниженная стоимость внутри сети

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

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

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

Уменьшенная задержка

Шаблон рекурсивного доказательства уменьшает задержку при проверке больших последовательностей утверждений. Это результат двух факторов:

1. Входящие утверждения могут быть доказаны параллельно (в отличие от доказательства очень большого комбинированного утверждения).
2. Нет необходимости ждать, пока прибудет последнее утверждение в поезде, чтобы начать доказывать. Скорее, доказательства могут быть объединены с новыми утверждениями по мере их поступления. Это означает, что задержка последнего утверждения, присоединяющегося к поезду, примерно равна времени, которое требуется для подтверждения этого самого последнего утверждения, плюс время, необходимое для подтверждения утверждения рекурсивного верификатора (которое подтверждает все те утверждения, которые уже «встроены» в этот поезд). конкретный поезд).

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

Содействие L3

Разработка оператора Recursive Verifier в Каире также открывает возможность отправки доказательств в StarkNet, поскольку этот оператор может быть встроен в смарт-контракт StarkNet. Это позволяет создавать развертывания L3 поверх общедоступной сети StarkNet (сеть L2).

Рекурсивный шаблон также применяется к агрегированию доказательств из L3, которые должны быть проверены одним доказательством из L2. Следовательно, гипер-масштабирование достигается и там.

Более тонкие преимущества

Аппликативная рекурсия

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

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

Если рекурсивному оператору разрешено быть осведомленным о приложении , т. е. распознавать семантику самого приложения, он может как сжать два доказательства в одно , так и объединить два входа в один. Результирующее утверждение подтверждает достоверность входной комбинации на основе семантики приложения, отсюда и название «Аппликативная рекурсия» (см., например, рисунок 3).

Здесь Утверждение 1 свидетельствует об обновлении состояния с А на В, а Утверждение 2 свидетельствует о дальнейшем обновлении с В на С. Доказательства Утверждения 1 и Утверждения 2 могут быть объединены в третье утверждение, свидетельствующее о прямом обновлении с А на С. , Рекурсивно применяя подобную логику, можно очень значительно снизить стоимость обновлений состояния вплоть до требования конечной задержки.

Еще одним важным примером аппликативной рекурсии является сжатие сводных данных из нескольких доказательств. Например, для накопительного пакета достоверности, такого как StarkNet, каждое обновление хранилища на L2 также включается в качестве данных передачи на L1, чтобы обеспечить доступность данных. Однако нет необходимости отправлять несколько обновлений для одного и того же элемента хранилища, поскольку для доступности данных требуется только окончательная стоимость транзакций, подтвержденная подтвержденным доказательством. Эта оптимизация уже выполняется в пределах одного блока StarkNet. Однако, генерируя доказательство для каждого блока, Applicative Recursion может сжимать эти сводные данные по нескольким блокам L2. Это может привести к значительному снижению затрат, позволяя сократить интервалы между блоками на уровне 2 без ущерба для масштабируемости обновлений уровня 1.

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

Снижение сложности внутрисетевого верификатора

Сложность верификатора STARK зависит от типа утверждений, для проверки которых он предназначен. В частности, для операторов Cairo сложность верификатора зависит от конкретных элементов, разрешенных в языке Cairo, а точнее, от поддерживаемых встроенных модулей (если использовать метафору процессора для Cairo, то встроенные модули эквивалентны микро -схемы в ЦП: вычисления выполняются настолько часто, что требуют собственных оптимизированных вычислений).

Язык Cairo продолжает развиваться и предлагает все больше и больше полезных встроенных функций. С другой стороны, Recursive Verifier требует использования только небольшого подмножества этих встроенных модулей. Следовательно, рекурсивный SHARP может успешно поддерживать любой оператор в Cairo, поддерживая полный язык в рекурсивных верификаторах. В частности, верификатору L1 Solidity Verifier нужно только проверять рекурсивные доказательства, и поэтому его можно ограничить более стабильным подмножеством языка Cairo: верификатору L1 не нужно идти в ногу с последними и лучшими встроенными модулями. Другими словами, проверка постоянно меняющихся сложных утверждений относится к L2, оставляя L1 Verifier для проверки более простых и более устойчивых утверждений.

Уменьшенный объем вычислительных ресурсов

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

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

Резюме

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

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

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

Гиди Кемпфер , руководитель отдела базовой разработки, StarkWare