Ранее в этом месяце мы опубликовали исходный код блокчейн-языка 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 с формальной корректностью криптографических протоколов для создания полностью верифицированных смарт-контрактов.
Мы надеемся, что вы присоединитесь к нашему проекту.