Смарт-контракты в Tezos
Michelson является предметно-ориентированным (специфическим) языком, используемым для написания смарт-контрактов в блокчейне Tezos. Michelson - язык, основанный на стеке; в нем нет переменных. Языки, ориентированные на стеки, работают с одним или несколькими стеками, каждый из которых может быть предназначен для разных целей.См. документацию Michelson и здесь - серию учебных пособий Michelson по camlCase.
Для программирования смарт-контрактов для Tezos доступны различные высокоуровневые языки. Цель этих языков - облегчить процесс разработки, чтобы Вы могли сосредоточиться на содержании Ваших смарт-контрактов, а не на их реализации.
Текущие варианты в разработке включают:
- LIGO: Язык смарт-контрактов, предлагающий синтаксические формы Pascal, Ocaml, и ReasonML
- SmartPy: библиотека Python с инструментами написания и тестирования (проверки) смарт-контрактов
- Morley/Lorentz: eDSL с Haskell для написания смарт-контрактов
Высокоуровневые языки компилируются или интерпретируются с целью создания действительного Michelson. Многим разработчикам легче работать с языками, так как они имеют более простые синтаксисы и включают в себя такие функции, как локальные переменные и высокоуровневые типы, а не стековые манипуляции.
Протокол Tezos написан на OCaml, универсальном промышленном языке программирования с упором на выразительность и безопасность. Это технология выбора компаний, в которых скорость имеет решающее значение, а одна ошибка может стоить миллионы. У него большая стандартная библиотека, что делает его полезным для многих приложений, таких как Python и Perl, и обеспечивает надежные модульные и объектно-ориентированные программные конструкции, которые делают его применимым в крупномасштабной разработке ПО. OCaml используют многие ведущие компании, в том числе Facebook, Bloomberg, Docker и Jane Street.
Функциональное программирование (парадигма программирования) - стиль построения структуры и элементов компьютерных программ, который рассматривает вычисления как оценку математических функций и избегает изменяющихся переменных данных.
Это описательна (декларативная) парадигма программирования, которая означает, что программирование выполняется с помощью выражений или объявлений вместо предписаний. В функциональном коде выходное значение функции зависит только от аргументов, которые передаются функции, так что при вызове функции f дважды с одним и тем же значением аргумента x каждый раз получается один и тот же результат f (x). Это отличается от процедур, которые зависят от локального или глобального состояния, которые могут давать разные результаты в разное время при вызове с одинаковыми аргументами, но с другим состоянием программы. Устранение побочных эффектов, т.е. изменений в состоянии, которые не зависят от входных данных функции, может значительно облегчить понимание и прогнозирование поведения программы, что является одним из ключевых мотивов развития функционального программирования.
Данная диаграмма демонстрирует высокоуровневые различия между EVM (Ethereum Virtual Machine), WASM (Web Assembly) и Michelson:
Michelson - это низкоуровневый язык программирования, основанный на стеке, который используется для написания смарт-контрактов в блокчейне Tezos. Michelson был разработан для облегчения процесса формальной верификации, позволяя пользователям подтверждать свойства своих контрактов. Он использует парадигму перезаписи стека, посредством которой каждая функция переписывает входной стек в выходной. (Полное объяснение будет приведено ниже.) Это работает чисто функционально и ни в коей мере не изменяет входные данные. Таким образом, все структуры данных остаются неизменными.
Стек - это абстрактный тип данных, являющийся собранием элементов с двумя основными операциями: push (добавляет элемент в коллекцию) и pop (удаляет последний добавленный элемент, который еще не был удален). Порядок, в котором элементы выходят из стека, порождает его альтернативное имя, LIFO (последний вошел, первый вышел). Кроме того, операция просмотра может предоставить доступ к верхушке без изменения стека.
Источник: Wikipedia.
Чтобы понять, что значит переписывать стеки, мы проведем транзакцию используя Michelson. Во-первых, перед выполнением транзакции положение блокчейна в определенном хеше преобразуется и помещается в стек как переменная
storage. У нас есть функция from , которая получает данные транзакции amount , количество прикрепленных ꜩ, и parameter , параметры функции.from [ (Pair (Pair amount parameter) storage) ]
После запуска функции, без каких-либо обновлений в стеке, программа вызывает функцию
to, содержащую параметры result, которые являются результатом функции, и выход storage, который преобразуется и хранится в блокчейне.to [ (Pair result storage) ]
В этом примере Michelson лишь функционально управляет стеком, а новый стек перед ается от функции к функции.
На первый взгляд, Michelson кажется довольно странным языком. Он не предусматривает такие функции, как полиморфизм, замыкания или именованные функции. В сравнении с Haskell или OCaml, он кажется недостаточно мощным. С его стеком не всегда легко разобраться, и нет стандартной библиотеки. Однако эти ограничения в значительной степени объясняются целями разработки языка.
У Michelson есть две основные цели (мотивации):
- 1.Предоставить читаемый байт-код
- 2.Быть обозримым
Tezos несколько отличается от Ethereum в отношении значения смарт-контрактов. Мы рассматриваем нашу платформу в качестве способа реализации определенных составляющих бизнес-логики нежели общего «мирового компьютера». В Ethereum большинство контрактов реализуют такие вещи, как multisig кошельки, правила передачи и распределения и т. д. Michelson нацелен на эти приложения.
Michelson разработан как читаемая целевая платформа для компиляции, хотя он может быть написан от руки. Цель состоит в том, чтобы понять даже вывод компилятора. Мы рассчитываем на то, что язык будет достаточно простым, чтобы разработчики могли создавать свои собственные инструменты анализа и компиляторы, если они того пожелают. Это отход от байт-кода EVM, который больше похож на сборку. Байт-код более низкого уровня обычно требует доверия как к Вашей программе, так и к цепочке инструментов компилятора. С Michelson Вы можете легко проверить и подтвердить свойства программы, которая фактически выполняется.
Использование высокоуровневого байт-кода также упрощает процесс проверки свойств скомпилированного вывода. Программы, написанные на Michelson, могут быть разумно проанализированы SMT-разрешителями и формализованы в Coq без необходимости применения более сложных методов, таких как логика разделения. Точно так же ограничения, накладываемые принудительным отступом и капитализацией (выделением заглавными буквами), гарантируют, что источник не может быть сбит с помощью приемов с отступами и выравниванием.
Текущая реализация Michelson основана на OCaml GADT, который мы использовали для проверки правильности языка. Кроме того, реализация языка на основе стека отображается непосредственно в семантике. То же самое не относится к любой эффективной реализации лямбда-исчисления. Также известны две формально верифицированные реализации Michelson: одна в Coq и одна в F *. Однажды мы надеемся заменить нашу текущую реализацию проверенной.
В заключение, одно из главных преимуществ Tezos заключается в том, что система может быть изменяемой. Мы хотим начать с небольшого базового языка, в котором мы уверены и добавить функции, поскольку для них создаются достойные варианты использования. Мы не хотим сразу перегружать язык, а затем нарушать обратную совместимость.
Итак, почему Michelson? Ответ таков: для того, чтобы обеспечить простую платформу для бизнес-логики, читаемый байт-код и обозримость. Когда я работал с Оли ном Шиверсом, он очень любил говорить, что всегда нужно использовать «инструмент, достаточно маленький для работы». Michelson был тщательно разработан, чтобы быть этим инструментом.
Last modified 2yr ago