Entendendo Simplicity: implementando uma linguagem de contrato inteligente em 30 linhas de Haskell

Na última segunda-feira, Chain lançou nossa linguagem de contrato inteligente de código aberto para Bitcoin, Ivy. Ivy é uma linguagem de nível superior que pode compilar para Bitcoin Script, a linguagem de baixo nível usada pelo protocolo Bitcoin para determinar se uma transação é autorizada. Ivy facilita a leitura, a escrita e o uso de contratos inteligentes para Bitcoin. Mas como foi projetado para ser compatível com o Bitcoin atualmente, suas características são limitadas pelas capacidades atuais da máquina virtual Bitcoin.

E se esses limites pudessem ser expandidos? E se fosse possível obter quase toda a segurança, simplicidade e eficiência de uma linguagem de execução pequena e non-turing-complete como o Bitcoin Script, ao mesmo tempo em que se ganha muito da flexibilidade e poder de uma linguagem de programação mais expressiva?

Para este post, vamos dar uma olhada em um futuro distante possível do protocolo Bitcoin, na forma de um paper emocionante de Russell O'Connor do Blockstream. O paper de O'Connor propõe um possível substituto para o Bitcoin Script, chamado Simplicity. Assim como o Bitcoin Script, Simplicity é uma linguagem de baixo nível de execução, destinada a ser um alvo de compilação para linguagens de nível superior como a Ivy. (Para saber mais sobre as possíveis vantagens do Simplicity sobre o Bitcoin Script e linguagens alternativas de baixo nível, você pode ver o anúncio do Blockstream, ou esta avaliação de Philip Wadler).

O paper de O'Connor apresenta tudo o que você precisa para implementar um intérprete Simplicity, mas não fornece uma implementação de referência executável (embora ele esteja trabalhando para lançar um SDK em um futuro próximo). E seguir junto com o paper pode ser um pouco assustador se, como eu, você não estiver muito familiarizado com a sintaxe do Coq ou cálculo sequencial.

Este posto tenta abordar estas duas questões, demonstrando como implementar a Simplicity do núcleo usando Haskell. Nossa implementação usará apenas Haskell elementar - especificamente, material dos capítulos 2, 4, 7 e 11 da Programação Haskell dos Primeiros Princípios. Se você já usou Haskell ou outra linguagem funcional como Elm, F#, PureScript ou OCaml, você provavelmente será capaz de seguir adiante.

Você pode experimentar esta implementação de Simplicity em seu navegador, e ver o código completo, em https://repl.it/@danrobinson/core-simplicity.

Objetivos

Estaremos implementando o núcleo Simplicity como um módulo Haskell. Este módulo exporta funções que lhe permitem escrever e executar expressões de Simplicity como código Haskell, quase sem tradução. Por exemplo, este programa Simplicity da seção 2.5 do paper:

Pode ser traduzido para o seguinte código Haskell:

not :: Bit -> Bit

not = comp (pair iden unit) (match (injr unit) (injl unit))

Nossa implementação será uma incorporação rasa. Isto significa que cada combinador e expressão em Simplicity corresponderá a uma função Haskell, e cada valor de Simplicity corresponderá a um valor Haskell. Isto nos permite usar o AST de Haskell, assim como sua inferência de tipo e seu verificador de tipo. Se uma expressão é uma expressão Haskell válida, sabemos que é também uma expressão de Simplicity válida.

Neste post, implementaremos apenas os nove combinadores básicos do núcleo Simplicity (descritos na seção 2 do artigo de O'Connor). Não tocaremos nas características mais sofisticadas de Simplicity, tais como compartilhamento de subexpressão, árvores de sintaxe abstrata merklizada e jets.

Tipos e valores

A Simplicity tem um tipo de unidade,𝟙. (Um "tipo de unidade" significa um tipo com apenas um habitante.) Para representar este tipo, usaremos o tipo de unidade embutido de Haskell, () (pronuncia-se "unidade").

Em Simplicity, o único valor do tipo de unidade se parece com ⟨⟩. Em Haskell, o valor tem o mesmo nome que o próprio tipo, ().

Simplicity também tem tipos de soma, escritos A + B, onde A e B são outros tipos de Simplicity. Cada habitante deste tipo é um valor do tipo A ou B, juntamente com uma tag indicando se é do tipo esquerdo ou do tipo direito. Para os tipos de soma, usaremos o tipo de soma canônica de Haskell, Either, que é definido como data Either a b = Left a | Right b.

Em Simplicity, os valores deste tipo se parecem com σᴸ(a) (quando o valor contido é um valor do primeiro tipo, tipo A) ou σᴿ(b) (quando o valor contido é um valor do segundo tipo, tipo B). Em Haskell, eles se parecem com Esquerda a e Direita b. Por exemplo, os dois valores que habitam o tipo Either () () são Left () e Right (). Os três habitantes do tipo Either( Either () () ) ( ) são(Left ()), Left (Right ()) e Right().

Finalmente, Simplicity tem tipos de produtos, escritos A x B. Cada habitante desse tipo é um par de valores - um do tipo A, e um do tipo B. Usaremos o tipo tupla do Haskell embutido, (a, b).

Em Simplicity, os valores de um tipo de produto se parecem com ⟨a, b⟩. Em Haskell, eles são parecidos com (a, b). Por exemplo, os quatro habitantes do tipo(Either () (), Either () () ) são (Left (), Left ()), (Left (), Right ()), (Right (), Left ()), and (Right (), Right ()).

Ao contrário de Haskell, a soma e os tipos de produtos não podem ser definidos recursivamente. Isto significa que cada tipo em Simplicity tem um número fixo e finito de possíveis habitantes.

Números e strings

Você notará que Simplicity não tem nenhum suporte integrado para tipos primitivos comuns como booleanos, inteiros ou strings. Ao invés disso, o paper Simplicity define tais tipos como combinações dos tipos descritos acima.

Por exemplo, o paper define um "bit" - um tipo com dois habitantes, zero e um - como a soma tipo 𝟙 + 𝟙. Em Haskell, isto corresponde ao tipo Either () (), e os dois valores dele são Left () e Right (). Seguindo a convenção utilizada no artigo, definiremos estes valores como significando 0 e 1, respectivamente.

Para nossa conveniência, podemos definir Bit como um sinônimo de tipo, juntamente com nomes mais descritivos para seus dois habitantes:

type Bit = Either () ()

zero :: Bit

zero = Left ()

one :: Bit

one = Right ()

E se quisermos representar não apenas um bit, mas uma "palavra" de dois bits - algo que pode representar qualquer número de 0 a 3? Podemos pegar um tipo de produto de dois bits, (Bit, Bit).

type Word2 = (Bit, Bit)

Este tipo pode ter 4 valores possíveis: (zero, zero), (zero, um), (um, zero), e (um, um). Podemos interpretar estes como os números inteiros 0, 1, 2 e 3, respectivamente. Alternativamente, podemos interpretá-los como bitstrings de tamanho 2.

O paper Simplicity define tamanhos de palavras maiores como produtos de dois tipos de tamanho de palavra menor. Uma palavra de 4 bits é definida como o produto de duas palavras de 2 bits, uma palavra de 8 bits é definida como o produto de duas palavras de 4 bits, e assim por diante.

type Word4 = (Word2, Word2)

type Word8 = (Word4, Word4)

Expressões e combinadores

Uma "expressão" em Simplicity é uma_ função_ de um valor de Simplicity para outro. Isto é um pouco incomum - você provavelmente está acostumado a expressões que podem avaliar a valores únicos. (O Simplicity também não tem funções de primeira classe - as expressões em Simplicity não são os mesmos valores de Simplicity).

As expressões em Simplicity são parecidas com estas:

pair iden unit

take (take iden)

comp (pair iden unit) (case (injr unit) (injl unit))

As expressões em Simplicity são compostas por um combinador. O Combinador é um primitivo em Simplicity que transforma 0 ou mais expressões em uma nova expressão. Há apenas nove combinadores no núcleo Simplicity.

iden :: a -> a

iden a = a

O combinador iden não é parametrizado com nenhuma outra expressão - iden por si só é uma expressão em Simplicity válida. A expressão iden é uma função que toma um valor em Simplicity e retorna o mesmo valor.

unit :: a -> ()

unit _ = ()

O combinador unit , da mesma forma, não aceita nenhuma outra expressão. unit é uma função que ignora sua entrada e retorna um único valor do tipo unity, ().

comp :: (a -> b) -> (b -> c) -> a -> c

comp s t a = t (s a)

O combinador comp. Leva duas expressões, s e t. Lembre-se, cada uma destas expressões é em si mesma uma função de um valor de Simplicity para outro. Quando parcialmente aplicada a s e t, comp retorna uma nova expressão que toma algum valor a, aplica a expressão s a ela, e então aplica a expressão t para esse resultado.

Note que o último argumento para comp, a, é um valor de Simplicity. Em contraste, todos os argumentos anteriores são expressões de Simplicity(ou seja, funções de Haskell). Devido ao curry automático de Haskell, você também pode pensar em comp como uma função que toma duas expressões s e t, e retorna uma nova expressão (ou seja, uma nova função Haskell de um valor para outro).

                                    [         expression          ]

combinator   expression  expression     input value   output value

             (* -> *)    (* -> *)    -> *          -> * 

comp ::      (a -> b) -> (b -> c)    -> a          -> c

comp         s           t              a          -> t (s a)

Esta é uma perspectiva útil e, sem dúvida, a "correta", não apenas devido à natureza diferente dos argumentos, mas também devido à diferença de quando estes argumentos são aprovados. As expressões s e t são fornecidas no momento em que o programa Simplicity é escrito (ou seja, pelo programador ou compilador), e o valor a é fornecido no momento da execução, quando o programa é executado.

injl :: (a -> b) -> a -> Either b c

injl t a = Left (t a)

injr :: (a -> c) -> a -> Either b c

injr t a = Right (t a)

Os combinadores injl e injr tomam cada um uma expressão, t. Quando aplicados a um valor, eles aplicam primeiro a expressão t, e depois injetam o resultado em um tipo de soma adicionando uma tag Left ou Right, respectivamente.

match :: ((a, c) -> d) -> ((b, c) -> d) -> (Either a b, c) -> d

match s t (Left a, c) = s (a, c)

match s t (Right b, c) = t (b, c)

O combinador match (renomeado do case Simplicity porque case é uma palavra reservada em Haskell) toma duas expressões, s e t. Quando aplicado a um valor, que deve ser um produto (ab, c), ele se encaixa no ab, e se aplica ou s ou t ao valor contido (junto com o estado extra c) com base no fato da tag a ser "Left" ou "Right", respectivamente.

pair :: (a -> b) -> (a -> c) -> a -> (b, c)

pair s t a = (s a, t a)

O combinador pair toma duas expressões, s e t. Quando aplicado a um valor, ele cria um par cujo primeiro valor é o resultado da aplicação s a a, e cujo segundo valor é o resultado da aplicação t para a.

take :: (a -> c) -> (a, b) -> c

take f (a, _) = f a

drop :: (b -> c) -> (a, b) -> c

drop f (_, b) = f b

Os combinadores take and drop (pegar e largar) pegam uma expressão, f. Quando aplicados a um valor - que deve ser um produto (a, b) - eles aplicam a expressão f ao primeiro ou segundo valor, respectivamente, e jogam o outro valor fora.

Exemplo de programas em Simplicity

Agora podemos usar estes combinadores para definir expressões que representam funções arbitrárias desde entradas até saídas.

Os exemplos a seguir são tirados quase literalmente do paper Simplicity (apenas traduzindo os nomes dos tipos e a sintaxe da anotação do tipo, e mudando o case para match ).

not :: Bit -> Bit

not = comp (pair iden unit) (match (injr unit) (injl unit))

Esta função leva um bit (zero ou um, ou seja, Left () ou Right ()) e o converte no bit oposto.

Como isso funciona? Suponhamos que aplicamos esta expressão ao valor Left (). Podemos usar o raciocínio equacional para simplificar gradualmente esta expressão, um combinador de cada vez:

comp (pair iden unit) (match (injr unit) (injl unit)) (Left ())

-- comp s t a = t (s a)

match (injr unit) (injl unit) ((pair iden unit) (Left ()))

-- pair s t a = (s a, t a)

match (injr unit) (injl unit) (iden (Left ()), unit (Left ()))

-- iden a = a

match (injr unit) (injl unit) (Left (), unit (Left ()))

-- match s t (Left a, c) = s (a, c)

injr unit ((), unit (Left ()))

-- injr s a = Right (s a)

Right (unit ((), unit (Left ())))

-- unit _ = ()

Right ()

Para experimentar, você pode usar a REPL online em https://repl.it/@danrobinson/core-simplicity, ou baixar o código de lá e experimentá-lo você mesmo em ghci:

> not zero

=> Right ()

> not zero == one

=> True

> not one == zero

=> True

Esta próxima função leva dois números de um bit, adiciona-os e retorna um bit overflow e um resultado:

halfAdder :: (Bit, Bit) -> (Bit, Bit)

halfAdder = match (drop (pair (injl unit) iden)) (drop (pair iden not))

Você pode usar este half-adder para construir uma full-adder, que leva dois números de um bit e um bit de overflow e retorna um novo bit overflow como resultado:

fullAdder1 :: ((Bit, Bit), Bit) -> (Bit, Bit)

fullAdder1 = comp (pair (take halfAdder) (drop iden))

            (comp (pair (take (take iden))

            (comp (pair (take (drop iden)) (drop iden))

              halfAdder))

            (pair (match (drop (take iden)) (injr unit))

              (drop (drop iden))))

Você também pode experimentar isso:

> fullAdder1 ((one, one), zero)

=> (Right (),Left ())

> fullAdder1 ((zero, zero), one)

=> (Left (),Right ())

Estas duas últimas funções implementam adder para palavras de 2 bits e palavras de 4 bits. (O paper Simplicity define estas repetidamente, mas fazê-lo em Haskell exigiria algum tipo de magia que está além do escopo deste post).

fullAdder2 :: ((Word2, Word2), Bit) -> (Bit, Word2)

fullAdder2 = comp (pair (take (pair (take (take iden))

                                   (drop (take iden))))

            (comp (pair (take (pair (take (drop iden))

                                    (drop (drop iden))))

                        (drop iden))

                   fullAdder1))

            (comp (pair (drop (drop iden))

                  (comp (pair (take iden)

                              (drop (take iden)))

                        fullAdder1))

            (pair (drop (take iden))

                  (pair (drop (drop iden)) (take iden))))

fullAdder4 :: ((Word4, Word4), Bit) -> (Bit, Word4)

fullAdder4 = comp (pair (take (pair (take (take iden))

                                    (drop (take iden))))

            (comp (pair (take (pair (take (drop iden))

                                    (drop (drop iden))))

                        (drop iden))

                    fullAdder2))

            (comp (pair (drop (drop iden))

                  (comp (pair (take iden)

                              (drop (take iden)))

                        fullAdder2))

            (pair (drop (take iden))

                  (pair (drop (drop iden)) (take iden))))

Conclusão

Espero que este post tenha facilitado a compreensão e a experimentação do núcleo em Simplicity. Também espero que tenha demonstrado algum do poder e flexibilidade que Haskell oferece quando se trabalha com linguagens específicas de domínio.

Obrigado a Russell O'Connor, Boyma Fahnbulleh, Bob Glickstein e Keith Rarick pela revisão de um rascunho deste post.

Artigo escrito por Dan Robinson. A versão original pode ser encontrada aqui. Traduzido e adaptado por Dimitris Calixto.