Смарт-контракты в Tezos

Введение в смарт-контракты в Tezos

Что такое Michelson?

Michelson является предметно-ориентированным (специфическим) языком, используемым для написания смарт-контрактов в блокчейне Tezos. Michelson - язык, основанный на стеке; в нем нет переменных. Языки, ориентированные на стеки, работают с одним или несколькими стеками, каждый из которых может быть предназначен для разных целей.См. документацию Michelson и здесь - серию учебных пособий Michelson по camlCase.

Какие существуют высокоуровневые языки смарт-контрактов?

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

Текущие варианты в разработке включают:

  • LIGO: Язык смарт-контрактов, предлагающий синтаксические формы Pascal, Ocaml, и ReasonML

  • SmartPy: библиотека Python с инструментами написания и тестирования (проверки) смарт-контрактов

  • Morley/Lorentz: eDSL с Haskell для написания смарт-контрактов

Чем отличаются высокоуровневые языки смарт-контрактов и Michelson?

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

Что такое OCaml, язык Tezos протокола?

Протокол Tezos написан на OCaml, универсальном промышленном языке программирования с упором на выразительность и безопасность. Это технология выбора компаний, в которых скорость имеет решающее значение, а одна ошибка может стоить миллионы. У него большая стандартная библиотека, что делает его полезным для многих приложений, таких как Python и Perl, и обеспечивает надежные модульные и объектно-ориентированные программные конструкции, которые делают его применимым в крупномасштабной разработке ПО. OCaml используют многие ведущие компании, в том числе Facebook, Bloomberg, Docker и Jane Street.

Что такое функциональное программирование? Чем оно отличается от других парадигм?

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

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

Данная диаграмма демонстрирует высокоуровневые различия между EVM (Ethereum Virtual Machine), WASM (Web Assembly) и Michelson:

Язык 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?" (Автор Milo Davis)

На первый взгляд, 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 был тщательно разработан, чтобы быть этим инструментом.

Материалы по языкам

Michelson:

Высокоуровневые языки смарт-контрактов:

LIGO:

SmartPy:

Morley/Lorentz:

OCaml:

Материалы разработаны TQ Tezos переведены на русский язык Tezos Ukraine