ūüáßūüá∑ Tutorial Marlowe 7/14

Tutorial completo em https://educacaocardano.wordpress.com/2020/05/18/marlowe-7/

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.

1 Like