Simplicity: надежные смарт-контракты
Blockstream Research

Simplicity: надежные смарт-контракты

Andrew Poelstra

Ранее в этом месяце мы опубликовали исходный код блокчейн-языка Simplicity.

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

Simplicity является совместимым с платформой Elements компании Blockstream. Это означает, что разработчики, создающие сайдчейны или независимые блокчейны в Elements, скоро смогут воспользоваться возможностями, которые предоставляются Simplicity. Сеть Liquid, как имплементация Elements,  также будет поддерживать Simplicity, а это откроет пользователям Liquid такие интересные приложения, как эскроу с минимальным доверием, “сейфы” и другие более сложные смарт-контракты.

Релиз, произошедший в этом месяце, включает:

  • Денотационная семантика ядра языка Simplicity и его расширений, официально описанных при помощи Coq.
  • Операционная семантика основного языка Simplicity, официально принятая в Coq.
  • Интерпретация, проверка типов и сериализация в языке Simplicity, написанные на Haskell.
  • Выражения на Simplicity, приведенные в качестве примера, включая криптографические операции, связанные с подписями SHA-256 и EC-Schnorr.
  • Технический отчет с описанием языка Simplicity.

Зачем нужен Simplicity?

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

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

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

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

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

Что такое Simplicity?

Simplicity – это низкоуровневый язык программирования и машинная модель для смарт-контрактов на блокчейне. Он разработан с нуля, чтобы иметь простую семантику, которая поддается статическому анализу и формальной верификации. Язык Simplicity определяется по его имплементации в  ассистенте доказательств Coq.

Хотя основа языка проста настолько, что может поместиться на футболке, простота языка не означает простоту разработки. Есть несколько причин для этого:

  • Блокчейны используют модель принципиально отличную от обычного программирования. Работа блокчейна заключается в верификации вычислений, а не в их выполнении. Это тонкое, но чрезвычайно важное различие, поскольку оно позволяет верифицировать выполнение произвольного кода без необходимости проверки полноты по Тьюрингу.
  • После развертывания смарт- контракт остается неизменным, и это не оставляет места для исправления ошибок. Simplicity решает эту проблему, позволяя пользователям создавать формальные доказательства правильности их смарт-контрактов.
  • Simplicity - это чрезвычайно низкоуровневый язык для прямого исполнения, больше похожий на язык ассемблера, чем на Java или Python. В конечном итоге мы ожидаем, что пользователи напишут свои контракты на одном или нескольких языках более высокого уровня, которые затем будут скомпилированы в Simplicity.

Что нового?

С момента нашего последнего блога о Simplicity мы приложили все усилия для перехода от экспериментального исследования языка к более формальной его спецификации.

Мы реимплементировали язык Simplicity  в ассистенте доказательств Coq:

  • У нас есть денотационная семантика полного языка Simplicity, включая языковые расширения, которые поддерживают данные доказательств, утверждения и делегирование.
  • Формальная спецификация абстрактной машины под названием «битовая машина», основанная на свободных категориях, обеспечивает операционную семантику для основного языка Simplicity.
  • Имплементация Haskell, разработанная в неразмеченном конечном стиле, позволяет экспериментировать с оценкой, исполнением и проверкой выражений Simplicity.
  • Модульный подход к языковым расширениям Simplicity позволяет игнорировать эффекты языковых расширений тогда, когда вы их не используете.
  • У нас есть множество выражений Simplicity для криптографических примитивов, включая нашу собственную реимплементацию libsecp256k1 в Simplicity.

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

Что дальше

Продвигаясь вперед, мы видим много разных направлений развития Simplicity.

В наши планы входит:

  • завершить интерпретатор С.
  • имплементировать библиотеку примитивов для распространенных криптографических функций.
  • Использовать Verifiable C для подтверждения корректности интерпретатора С и примитивов.
  • Интегрировать Simplicity в блокчейн платформу Elements.

Другие направления развития включают:

  • Разработку оптимизаторов кода Simplicity.
  • Создание новых или адаптация существующих высокоуровневых платформ смарт-контрактов, таких как Ivy, для генерации кода Simplicity.
  • Объединение функциональной корректности криптографических примитивов Simplicity с формальной корректностью криптографических протоколов для создания полностью верифицированных смарт-контрактов.

Мы надеемся, что вы присоединитесь к нашему проекту.

If you have specific preferences, please, mark the topic(s) you would like to read: