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

Вот самая простая программа на Simplicity:

main := iden
Эта программа принимает пустой ввод и производит пустой вывод. Давайте сделаем нечто более интересное - возьмем бит и инвертируем его:

   bit0 := injl unit : 1 * 1 -> 2
   bit1 := injr unit : 1 * 1 -> 2

   padR := pair iden unit     : 2 -> 2 * 1 
   bitflip := case bit1 bit0  : 2 * 1 -> 2
   main := comp padR bitflip  : 2 -> 2

Здесь последнее выражение Simplicity представляет собой нашу функцию main. Читая снизу вверх, мы видим, что она представляет собой композицию нескольких более мелких функций, которые в конечном итоге объединяются в unit-комбинаторы. Unit-комбинаторы создают пустой вывод. Вместе с функцией iden, которая принимает произвольные входные данные и возвращает их без изменений, а также функцией witness, которая выводит значение, предоставленное извне, unit-комбинаторы составляют основу для каждого выражения Simplicity.

В этом фрагменте кода мы привели аннотации типов, чтобы обозначить, какие данные передаются из каждой части выражения в следующую. В данном случае «1» представляет тип юнита, который мы называли «пустым выводом». А «2» представляет собой бит, который может принимать значение 0 или 1.

Этот фрагмент приведен  для того, чтобы наглядно показать, как выглядит код Simplicity. Так что не стоит волноваться, если вы не уловилии все детали этого фрагмента. Далее в этой публикации мы тщательно проанализируем более интересную программу.

Язык спецификаций

В конечном итоге все языки программирования выражают идею объединения вычислений для построения более крупных моделей. Bitcoin Script (подобно Forth или PostScript) делает это с помощью стек-машины, в которой каждое вычисление поочередно обрабатывает список объектов данных. Виртуальная машина Ethereum (EVM) использует архитектуру вызовов функций,  которая позволяет вызывать другие блоки кода (возможно, в других контрактах), принимающие данные на ввод и возвращающие данные на вывод. Эта модель используется сегодня практически всеми основными языками программирования.

Языки программирования используют побочные эффекты для взаимодействия с внешним миром, например, с проводимой транзакцией. В EVM контракты также имеют доступ к хранилищам данных типа «ключ-значение», что позволяет им сохранять состояние во время транзакций, не передавая его явно.

Как в Bitcoin Script, так и в EVM инверсия битов может быть выполнена с помощью одного опкода (при этом версия Bitcoin может принимать множество различных входных данных, большинство из которых не похожи на биты, а версия EVM действует побитово, но всегда на 256 битах одновременно). Резонно спросить, почему модель Simplicity приводит к такому многословию для таких простых вещей.

Наша цель в Simplicity – формально определить семантику программ, как с точки зрения того, какие функции они представляют, так и с точки зрения того, какие вычислительные ресурсы задействованы при их вычислении. В принципе, можно было бы формально определить язык, работающий подобно Bitcoin Script или EVM, но эта задача была бы чрезвычайно сложной, и результат было бы почти так же сложно проверить. Вместо этого в Simplicity мы определили небольшой набор базовых комбинаторов, каждый из которых отражает математически фундаментальный способ комбинирования функций. Семантика получившегося языка настолько мала, что помещается на футболке.

На практике для таких операций, как инверсия битов, этот код будет написан всего один раз, а затем будет использован повторно. Фактически, мы сделали это за вас и встроили ее в язык. При написании своего собственного кода вы можете просто использовать команду jet_not вместо приведенного выше кода. Мы рассмотрим jets более подробно в следующем разделе.

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

Программы и выражения

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

Итак, в чем же заключается стратегия? На самом деле их две: первая состоит в том, что программы Simplicity, зафиксированные в адресах, имеют дыры, которые заполняются только при трате монет; вторая – в том, что программы Simplicity имеют побочные эффекты, которые позволяют им получать доступ к данным блокчейна или досрочно прерывать работу, выходя тем самым за рамки чисто математических функций.

Существует два способа указать дыры в программах Simplicity: комбинаторы disconnect и witness. Комбинатор disconnect довольно сложный, мы рассматривали его ранее. Но «свидетели» (witnesses) очень просты: комбинатор witness возвращает значение заданного типа, называемого witness (например, цифровая подпись, прообраз хеша или конкретный выбор ключей для подписи).

Кроме того, в Simplicity есть два способа работы с побочными эффектами: первый – это интроспекция данных транзакции (о чем мы также поговорим в одной из следующих публикаций), а второй – это утверждения. Утверждения останавливают выполнение программы. В Bitcoin Script опкод VERIFY используется для утверждений и позволяет  программе завершить выполнение, если она обнаружит невалидную подпись или другие данные. В EVM для этой же цели используется опкод STOP.

Теперь мы можем увидеть, как программа, входные и выходные типы которой номинально тривиальны, может производить полезные вычисления: «свидетели» служат в качестве входных данных программы, а утверждения обеспечивают вывод программы формата “pass/fail”.

Рассмотрим другой пример. Вот программа, которая берет двух «свидетелей» и проверяет их на равенство:

-- Witnesses
wit1 := witness : 1 -> 2^32 
wit2 := witness : 1 -> 2^32 

-- Program code
pr1 := pair wit1 wit2 : 1 -> 2^64
jt2 := jet_eq_32      : 2^64 -> 2
cp3 := comp pr1 jt2   : 1 -> 2
jt4 := jet_verify     : 2 -> 1

main := comp cp3 jt4  : 1 -> 1

Мы можем прочитать эту программу снизу вверх: сама программа представляет собой одно выражение main типа 1->1. Здесь «тип» выражения указывает, какие значения оно принимает в качестве входных и выходных данных. Тип 1 имеет только одно значение, поэтому не описывает никакой информации. Тип 2 имеет два возможных значения, поэтому может представлять один бит, 2^32 – 32-битную строку и так далее.

Из нижнего равенства мы видим, что main является композицией выражений с именами cp3 и jt4. Тогда cp3 сама является композицией pr1 и jt2, и так далее. В этой программе используется пять комбинаторов:

• comp, или композиция, принимает два выражения и вычисляет второе, используя в качестве входного значения вывод первого выражения.
• pair принимает два выражения и создает новое выражение, результатом которого является пара значений: левая часть – это вывод первого выражения, а правая – вывод второго.
• witness не принимает никаких входных данных, но результатом имеет полиморфный тип: какой бы тип ни был необходим для того, чтобы программа имела смысл, это он и есть.  А значение, которое он выдает, задается в момент вычисления.
• jet_eq_32 – это jet, то есть одиночный комбинатор, который заменяет большее выражение Simplicity. Замещенное выражение называется его спецификацией, и интерпретатор Simplicity может оценить jet либо путем вычисления спецификации, либо с помощью оптимизированного машинного кода, что дает тот же эффект. В данном случае jet принимает два 32-битных значения и выводит один бит, указывающий, равны ли эти два значения (1) или не равны (0).
• jet_verify также является jet. Он принимает на вход один бит, и если этот бит равен 0, то он прерывает работу программы. Выходных данных у него нет.

Заключение

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

В Simplicity есть еще несколько комбинаторов и множество “jets”, о которых мы расскажем в следующих статьях. По мере развития языка мы будем изучать больше практических примеров и рассмотрим, что значит "доказывать" свойства программ.

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

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