🇧🇷 Tutorial Marlowe 7/14

[cabral_joselmo]

Tutorial completo em Tutorial Marlowe 3.0 (Parte 7) – Educação Cardano

7. Tipos de dados na Marlowe

Este tutorial apresenta formalmente Marlowe como um tipo de dado Haskell, além de apresentar os diferentes tipos usados pelo modelo e discutir várias suposições sobre a infraestrutura na qual os contratos serão executados. O código que descrevemos aqui vem dos módulos Haskell Semantics.hs e Util.hs.

7.1 Marlowe

A linguagem específica de domínio (DSL) Marlowe é modelada como uma coleção de tipos algébricos em Haskell, com contratos sendo dados pelo tipo de Contract (contrato):

Vimos no tutorial anterior o que esses contratos fazem. No restante deste tutorial, aprofundaremos um pouco os tipos de Haskell usados para representar os vários componentes dos contratos, incluindo contas, valores, observações e ações. Também examinaremos os tipos relacionados à execução de contratos, incluindo insumos, estados e o ambiente.

7.2 Componentes Básicos

Na modelagem de partes básicas de Marlowe, usamos uma combinação de tipos de dados Haskell, que definem novos tipos e sinônimos de tipo que dão um novo nome a um tipo existente. [7]

Uma conta Marlowe possui quantidades de várias moedas e / ou tokens fungíveis e não fungíveis. Uma quantia concreta é indexada por um Token, que é um par de CurrencySymbol e TokenName. Você pode pensar em uma conta como um Map Token Integer, em que:

O token Ada de Cardano é token adaSymbol adaToken. Mas você é livre para criar suas próprias moedas e tokens.

Os tokens de uma moeda podem representar funções em um contrato, por exemplo, “comprador” e “vendedor”. Pense em um contrato legal no sentido de “doravante referido como Artista / Fornecedor / Artista / Consultor”. Dessa forma, podemos dissociar a noção de propriedade de uma função de contrato e torná-la negociável. Assim, você pode vender seu empréstimo ou comprar uma parte de uma função em algum contrato.

Aqui, account contém um token de buyer da moeda “TradeRoles” e 1000 Ada.

Uma Party (Parte) é representada como um hash de chave pública ou um nome de função.

Para progredir em um contrato da Marlowe, uma parte deve fornecer uma evidência. Para a parte PK, isso seria uma assinatura válida de uma transação assinada por uma chave privada de uma chave pública com hash para a parte PubKeyHash, semelhante ao mecanismo Pay to Public Key Hash do Bitcoin. Para uma parte de Role, a evidência está gastando um role token na mesma transação, geralmente para o mesmo proprietário.

Assim, os partidos Role se parecerão com (Role “alice”), (Role “bob”) e assim por diante. No entanto, Haskell nos permite apresentar e ler esses valores de forma mais concisa (declarando uma instância personalizada de Show e usando strings sobrecarregadas ) para que elas possam ser inseridas e lidas como “alice“, “bob” etc.

Os números dos slots e as quantias de dinheiro são tratados de maneira semelhante; com a mesma abordagem de exibição / sobrecarga, eles aparecerão nos contratos como números:

As contas têm um número NumAccount e um proprietário, que é Party no contrato.

e um exemplo seria AccountId 0 “alice”. Observe que “alice” é a proprietária aqui no sentido de que ela receberá qualquer dinheiro da conta quando o contrato for rescindido.

Como em muitos contratos, cada parte possui no máximo uma conta, podemos usar strings sobrecarregadas para nos permitir abreviar essa conta – número de conta 0 para qualquer proprietário – pelo nome de seu proprietário: neste caso “alice“.

Um pagamento pode ser feito a uma das partes do contrato ou a uma das contas do contrato, e isso se reflete na definição

As escolhas – de números inteiros – são identificadas pelo ChoiceId, que combina um nome para a escolha com a Party que fez a escolha:

Valores definidos utilizando Let, também são identificados por inteiros. [8]

7.3 Valores, observações e ações

Com base nos tipos básicos, podemos descrever três componentes de contratos de nível superior: um tipo de valores , além disso, um tipo de observação e também um tipo de ações , que acionam casos particulares. Primeiro, olhando para o Value (valor) que temos

Os diferentes tipos de valores – todos Integer (inteiros) – são praticamente auto-explicativos, mas, para ser completo, temos

• Pesquisa do valor em uma conta AvailableMoney, feita em ChoiceValue e em um identificador que já foi definido UseValue.

• Constantes e operadores aritméticos.

• Scale multiplica um Value por uma constante racional, digamos, 2/3, e arredonda o resultado usando o arredondamento “meio par” ou “bancário”. Portanto, 14/10 é arredondado para 1, 15/10 e 25/10 é arredondado para 2.

• O início e o fim do intervalo atual do slot ; veja abaixo para uma discussão mais aprofundada sobre isso.

• Cond representa expressões if, ou seja – o primeiro argumento para Cond é uma condição (Observation) a ser verificada, o segundo é um Value a ser adotado quando a condição é satisfeita e o último é um Value para a condição não satisfeita; por exemplo: (Cond FalseObs (Constante 1) (Constante 2)) é equivalente a (Constante 2).

Em seguida, temos observações

Isso é realmente autoexplicativo: podemos comparar valores para (des)igualdade e ordenação e combinar observações usando os conectivos booleanos. A única outra construção ChoseSomething indica se alguma escolha foi feita para um determinado ChoiceId.

Casos e ações são dados por estes tipos:

Três tipos de ação são possíveis:

• Um Deposit n p t v faz um depósito do valor v do token t no número da conta n pertencente à parte p.

• É feita uma escolha para um ID específico com uma lista de limites nos valores aceitáveis. Por exemplo, [Bound 0 0, Bound 3 5] oferece a opção de um de 0, 3, 4 e 5.

• O contrato é notificado de que é feita uma observação específica. Normalmente, isso seria feito por uma das partes ou por uma de suas carteiras agindo automaticamente.

Isso completa nossa discussão sobre os tipos que compõem os contratos da Marlowe.

7.4 Dados dinâmicos

Como observamos anteriormente, a semântica de Marlowe consiste em construir transações , assim:

Uma transação é construída a partir de uma série de etapas, algumas das quais consomem um valor de entrada e outras produzem efeitos ou pagamentos. Ao descrever isso, explicamos que uma transação modificou um contrato (para sua continuação) e o estado, mas mais precisamente temos uma função

Onde os tipos são definidos dessa maneira:

A notação usada aqui adiciona nomes de campo aos argumentos dos construtores, fornecendo seletores para os dados e tornando mais claro o objetivo de cada campo.

O tipo TransactionInput possui dois componentes: o SlotInterval no qual ele pode ser adicionado validamente à blockchain e uma sequência ordenada de valores de Input a serem processados nessa transação.

Um valor TransactionOutput possui quatro componentes: os dois últimos são o State (estado) e o Contract (contrato) atualizados, enquanto o segundo fornece uma sequência ordenada de Payments (pagamentos) produzidos pela transação. O primeiro componente contém uma lista de todos os avisos produzidos pelo processamento da transação.

7.5 Intervalos de slots

Isso faz parte da arquitetura da Cardano / Plutus, que reconhece que não é possível prever com precisão em qual slot uma transação específica será processada. Portanto, as transações recebem um intervalo de slots no qual se espera que sejam processadas, e isso é transferido para Marlowe: cada etapa de um contrato da Marlowe é processada no contexto de um intervalo de slots.

Como isso afeta o processamento de um contrato da Marlowe? Cada etapa é processada em relação a um intervalo de slot, e o valor atual do slot precisa estar dentro desse intervalo.

Os pontos iniciais e finais do intervalo são acessíveis como os valores SlotIntervalStart e SlotIntervalEnd, respectivamente, e eles podem ser usados ​​em observações. Os tempos limite precisam ser processados ​​ sem ambiguidade , para que todos os valores no intervalo do slot tenham excedido o tempo limite para que ele entre em vigor ou caiam antes do tempo limite para que a execução normal entre em vigor. Em outras palavras, o valor do tempo limite precisa ser menor ou igual a SlotIntervalStart (para que o tempo limite entre em vigor) ou ser estritamente maior que SlotIntervalEnd (para que a execução normal ocorra).

Notas

O modelo faz várias suposições sobre a infraestrutura de blockchain na qual é executada.

• Supõe-se que funções e operações criptográficas sejam fornecidas por uma camada externa a Marlowe e, portanto, não precisam ser modeladas explicitamente.

• Assumimos que o tempo é “granulado grosseiramente” e medido pelo número do bloco ou slot, de modo que, em particular, os tempos limite sejam delimitados usando números de bloco / slot.

• Fazer um depósito não é algo que um contrato possa executar; em vez disso, pode solicitar que um depósito seja feito, mas que deve ser estabelecido externamente: daí a entrada de (uma coleção de) depósitos para cada transação.

• O modelo gerencia o reembolso dos fundos de volta ao proprietário de uma conta específica quando um contrato chega ao ponto de Close.

[7] De fato, usamos declarações newtype em vez de tipos data, porque elas são implementadas com mais eficiência.

[8] Isso pode ser modificado no futuro para permitir que valores sejam identificados por strings.