🇮🇹 "Smart Contracts Actus in Marlowe"

[lordwotton]

Traduzione italiana di “Actus smart contracts in Marlowe” scritto dal prof. Simon Thompson nel blog IOG il 13 ottobre 2020.

Traduzione italiana a cura di Lordwotton di RIOT Stake Pools

---

Contratti intelligenti Actus in Marlowe

Scrivere nel linguaggio della finanza, piuttosto che nel linguaggio della blockchain

Nella nostra serie di blog tecnici occasionali Developer Deep Dive, invitiamo i ricercatori e gli ingegneri di IOHK a discutere i loro ultimi lavori e approfondimenti.

Marlowe è un linguaggio specifico per i contratti finanziari sicuri e intelligenti che IOHK sta sviluppando per le capacità Goguen della blockchain Cardano. Dopo il mio post introduttivo su Marlowe, in questo post di Deep Dive, esamineremo i dettagli del linguaggio e i vari modi di scrivere i contratti intelligenti Marlowe mentre entriamo nell’era della finanza decentralizzata (DeFi). Dopo aver spiegato il nostro approccio agli oracoli, che importano le informazioni del “mondo reale” in un contratto in corso, esamineremo gli Algorithmic Contract Types Unified Standard (Actus) per i contratti finanziari, e spiegheremo come abbiamo implementato questa innovazione in Marlowe.

Marlowe in poche parole

Marlowe è un piccolo linguaggio, con una manciata di costrutti che, per ogni contratto, descrivono un comportamento che coinvolge un insieme fisso e finito di ruoli.

• Un contratto in corso di esecuzione può effettuare un pagamento a un ruolo o a una chiave pubblica.

• In modo complementare, un contratto può attendere un’azione da parte di uno dei ruoli, come un deposito di valuta, o una scelta da un insieme di opzioni. Fondamentalmente, un contratto non può aspettare a tempo indeterminato: se non è stata avviata alcuna azione entro un determinato periodo di tempo (il timeout), allora il contratto continuerà con un altro comportamento, come il rimborso di eventuali fondi nel contratto.

• A seconda dello stato attuale di un contratto, si può scegliere tra due azioni future, che sono a loro volta contratti.

• Quando non sono necessarie altre azioni, il contratto si chiuderà, e qualsiasi valuta rimanente nel contratto sarà rimborsata.

Quando un contratto viene eseguito, i ruoli che esso comporta sono svolti dai partecipanti, che sono identità sulla blockchain. Questo modello permette di trasferire un ruolo durante l’esecuzione del contratto, in modo che i ruoli in un contratto in corso possano essere scambiati. Ogni ruolo è rappresentato da un token sulla catena, e il trasferimento di questo trasferisce la capacità di eseguire le azioni del ruolo. Andando oltre, possiamo rappresentare un unico ruolo con più gettoni, permettendo così di condividere il ruolo: questo potrebbe essere definito come “cartolarizzato”.

Il sistema Marlowe

Abbiamo deliberatamente scelto di rendere il linguaggio il più semplice possibile, in modo che sia semplice da implementare su Cardano e nel Marlowe Playground. Marlowe descrive il flusso di criptovalute tra i partecipanti, e perché questo sia implementato in pratica sulla blockchain di Cardano, il codice deve essere eseguito sia on-chain che off-chain: ricordate, però, che un solo contratto Marlowe descrive entrambe le parti. La parte on-chain accetta e convalida le transazioni che sono conformi ai requisiti del contratto smart: questa parte è implementata come un unico script Plutus per tutti i contratti Marlowe, con il particolare contratto Marlowe che comprende un dato passato attraverso le transazioni. Off-chain, il contratto Marlowe sarà presentato attraverso l’interfaccia utente e il portafoglio, offrendo o, addirittura, automatizzando depositi e scelte e ricevendo pagamenti in criptovaluta.

Figura 1. Marlowe Playground simula il comportamento dei contratti

Nel Playground siamo in grado di simulare il comportamento dei contratti, in modo che i potenziali utenti possano camminare attraverso diverse modalità in cui i contratti si evolveranno, secondo le diverse azioni intraprese dai partecipanti. Nella simulazione principale, Figura 1, gli utenti hanno un punto di vista onnisciente e sono in grado di eseguire azioni da parte di qualsiasi partecipante, con la possibilità in ogni punto di annullare le azioni intraprese, e quindi di prendere un percorso diverso. La simulazione del portafoglio permette agli utenti di vedere il comportamento dal punto di vista di un particolare partecipante, simulando così come quell’utente interagirà con il contratto in corso una volta che questo sarà distribuito sulla blockchain.

Questa semplicità ci permette anche di modellare i contratti Marlowe in un solver SMT, un sistema logico per il controllo automatico delle proprietà dei sistemi. Utilizzando questo modello, che noi chiamiamo analisi statica, per ogni contratto siamo in grado di verificare se può fallire o meno un pagamento, e se il contratto può fallire otteniamo la prova di come fallisce, aiutando l’autore a riscrivere il contratto se lo desidera.

Possiamo costruire un modello formale della nostra implementazione in un assistente di prova, in cui siamo in grado di produrre prove di come il linguaggio si comporta. Mentre il solver SMT lavora per i singoli contratti, l’assistente di prova può provare le proprietà dei modelli di contratto, così come il sistema stesso: ad esempio, possiamo dimostrare che in qualsiasi contratto in corso, i conti a cui fa riferimento non possono mai essere a debito. La simulazione, l’analisi statica e la prova forniscono livelli di garanzia complementari per un contratto a cui gli utenti si impegneranno per garantire che il contratto si comporti come dovrebbe.

Scrittura dei contratti Marlowe

Abbiamo visto come i contratti Marlowe possono essere analizzati in vari modi, ma come fanno gli autori a scrivere contratti intelligenti in Marlowe? Il Playground offre diversi modi per produrre i contratti Marlowe. Gli utenti possono scrivere Marlowe direttamente, ma i principianti spesso scelgono di costruire i contratti visivamente, utilizzando un editor interattivo Blockly. La Figura 2 mostra una sezione di un contratto di deposito a garanzia (escrow).

Figura 2. Un contratto di deposito a garanzia nell’editor interattivo Blockly di Playground

Lavorare in questo editor visuale ha il vantaggio di mostrare tutte le opzioni mentre si seleziona come compilare una parte del contratto che si sta sviluppando. In alternativa, è possibile sviluppare contratti in Haskell, perché il DSL Marlowe è di fatto incorporato in Haskell. La Figura 3 mostra lo stesso contratto in Haskell: le parti blu e viola sono Marlowe, e le componenti nere sono definite in Haskell, come abbreviazioni che rendono il contratto complessivo più leggibile. Questo approccio permette agli utenti di costruire un contratto intelligente passo dopo passo a partire dai componenti. Nel codice mostrato in Figura 3, ai ruoli, Alice e Bob, viene chiesto a ciascuno di fare una scelta: se le loro scelte coincidono, sono d’accordo, e il contratto procede in un modo; in caso contrario, ad un terzo partecipante, Carol, viene chiesto di arbitrare tra loro. L’accordo contrattuale e l’arbitrato sono definiti più avanti nel file Haskell.

Figura 3. Il contratto di deposito a garanzia a Haskell

Gli utenti saranno anche in grado di scrivere i loro contratti finanziari intelligenti utilizzando JavaScript, pur godendo di tutti i vantaggi dell’analisi, della simulazione e della prova, come previsto dall’implementazione Marlowe.

Oracoli

Una delle prime domande che ci vengono poste quando descriviamo Marlowe riguarda gli oracoli finanziari, o come possiamo ottenere un contratto che tenga conto dei valori dei dati esterni, come il tasso di cambio tra ada e bitcoin. Astrattamente, un oracolo è proprio come un partecipante che fa una scelta, e quindi la semantica di Marlowe può già occuparsi di valori esterni. Tuttavia, abbiamo in programma di supportare i valori dell’oracolo come parte dell’implementazione, permettendo ai contratti di accedere ai valori direttamente da un ticker di borsa o da un data feed come Coinbase. Allo stesso tempo, il team di Plutus sta cercando il modo migliore per trattare con gli oracoli in generale, e possiamo aspettarci un supporto per questo a tempo debito, anche se forse non nella prima versione completa di Marlowe e del Plutus Application Framework.

Actus per i contratti finanziari

Marlowe ha il potenziale per dare alle persone la possibilità di assumere impegni finanziari e di negoziare senza che una terza parte lo faciliti: la blockchain assicura che il contratto sia seguito.

Stiamo costruendo un’implementazione Marlowe di contratti disintermediata da offrire agli utenti finali che vogliono fare accordi finanziari peer-to-peer direttamente senza l’intervento di terzi.

La Actus Financial Research Foundation classifica i contratti finanziari in base a una tassonomia che viene descritta in una specifica tecnica dettagliata.

Actus si basa sull’intesa che i contratti finanziari sono accordi legali tra due (o più) controparti sullo scambio di flussi di cassa futuri. Storicamente, tali accordi legali sono descritti in linguaggio naturale, il che porta all’ambiguità e alla diversità artificiale. Come risposta, Actus definisce i contratti attraverso una serie di termini contrattuali e funzioni deterministiche che mappano questi termini agli obblighi di pagamento futuri. In tal modo, è possibile descrivere la maggior parte degli strumenti finanziari attraverso 31 tipi di contratto o modelli modulari.

In seguito, guardiamo a un semplice esempio, e poi spieghiamo il nostro approccio completo all’implementazione di Actus, con approcci complementari che forniscono diversi pro e contro.

Un primo esempio di Actus

Un’obbligazione a cedola zero è un titolo di debito che non paga interessi (una cedola) ma è emesso a sconto, rendendo il profitto alla scadenza quando l’obbligazione viene rimborsata per l’intero valore nominale.

Ad esempio, la Figura 4 descrive un contratto in base al quale un investitore può acquistare un’obbligazione che costa 1.000 ada con uno sconto del 15%. Paga 850 ada all’emittente dell’obbligazione prima dell’ora di inizio, qui slot 10.

Più tardi, dopo la data di scadenza, qui slot 20, l’investitore può scambiare l’obbligazione con il suo valore nozionale completo, cioè 1.000 ada.

Figura 4. Contratto per un’obbligazione a tasso zero con uno sconto del 15%.

Questo contratto ha un notevole svantaggio. Una volta che l’investitore ha depositato gli 850 ada, questi saranno immediatamente pagati all’emittente; se l’investitore non investe abbastanza rapidamente, cioè prima del timeout, il contratto termina. Dopo di che, sono possibili due risultati:

• l’emittente deposita 1.000 ada sul conto dell’investitore, e questa somma viene immediatamente pagata all’investitore per intero;
• se l’investitore non effettua il deposito, allora il contratto viene chiuso e tutti i soldi del contratto vengono rimborsati, ma non ci sono soldi nel contratto a questo punto, quindi l’investitore perde i suoi soldi.

Come si può evitare il problema dell’inadempienza dell’emittente di obbligazioni? Ci sono almeno due modi per risolvere il problema: potremmo chiedere all’emittente di depositare l’intero importo prima dell’inizio del contratto, ma questo sconfiggerebbe in primo luogo l’oggetto dell’emissione dell’obbligazione. Più realisticamente, potremmo chiedere a una terza parte di essere garante dell’accordo, come espresso qui.

Figura 5. Miglioramento del contratto con un garante

Actus in Marlowe

I prodotti della tassonomia Actus, come il contratto principale alla scadenza, possono essere presentati in Marlowe in modi diversi, a seconda del grado in cui possono accettare modifiche alle loro condizioni durante la durata del contratto (Figura 6).

Figura 6. Tassonomia Actus e Marlowe

Nel caso più semplice, tutti i flussi di cassa sono fissati, o congelati, all’inizio del contratto, in modo che sia del tutto prevedibile il funzionamento del contratto, supponendo che tutti i partecipanti continuino a impegnarsi con il contratto durante la sua durata. I contratti di questo tipo si chiamano Actus-F (per fisso o congelato).

Il dinamismo - cioè il cambiamento durante l’evoluzione del contratto - può avvenire in due modi. I partecipanti possono effettuare pagamenti non programmati che richiedono il ricalcolo dei flussi di cassa rimanenti, e anche i flussi di cassa possono essere modificati tenendo conto di fattori di rischio esterni. La generalità completa dei contratti che fanno entrambe le cose è modellata in Actus-M (per Marlowe).

Esistono anche livelli intermedi: I modelli Actus-FS prevedono scadenze fisse: consentono di tenere conto dei fattori di rischio, ma senza pagamenti inattesi; al contrario, i contratti Actus-FR consentono di effettuare pagamenti in punti inattesi, ma non tengono conto di alcun fattore di rischio.

Infine, spostandosi al di fuori di Marlowe, Actus-H (H per Haskell) modella i contratti direttamente come programmi in Plutus o Haskell, utilizzando Marlowe per la validazione di ogni transazione nel corso della durata del contratto, generando il codice Plutus dalla descrizione Marlowe della logica del contratto.

Perché offriamo questi diversi modelli di contratti Actus? Il motivo è che c’è un compromesso tra la natura dinamica dei contratti e la garanzia che possiamo dare agli utenti su come i contratti si svolgeranno prima dell’esecuzione del contratto.

• I contratti Actus-F presentano un calendario di pagamenti interamente fisso, che può essere esaminato direttamente dai partecipanti in modo che sia semplice vedere, ad esempio, che tutti i pagamenti di un contratto di questo tipo avranno successo.

• I contratti Actus-FS e -FR presentano un maggiore dinamismo, ma i contratti sono leggibili e facili da controllare. Inoltre, sono soggetti ad un’analisi statica (più lenta) per stabilire, ad esempio, che tutti i pagamenti avranno successo.

• I contratti Actus-M sono espressi in Marlowe, e quindi possono essere analizzati. L’analisi è, tuttavia, sostanzialmente più lenta a causa dell’imprevedibilità delle azioni che il contratto subirà in un determinato momento. Si noti che la garanzia può essere offerta per le versioni ridimensionate dei contratti, che hanno lo stesso contenuto computazionale, ma che si evolvono in un tempo più breve, coinvolgendo quindi meno interazioni.

• I contratti Actus-H sono scritti in una combinazione di Plutus e Marlowe, e quindi non sono suscettibili di controllo statico come gli altri. Tuttavia, questa piattaforma offre ai clienti aziendali la piena estensibilità e la personalizzazione dell’implementazione dello standard Actus.

Nella nostra implementazione di Actus, disponibile in versione pre-release nella scheda Labs del Playground, gli utenti sono in grado di generare contratti Actus-F e -FS a partire dai termini del contratto, utilizzando una presentazione visiva dei dati richiesti.

Figura 7. Le tre voci con asterisco sono richieste per un contratto di capitale alla scadenza

Per un contratto di capitale alla scadenza, sono richieste tre voci: la data di inizio e di fine, e l’importo nozionale del contratto (da cui le voci che figurano nel modello). Tale contratto comprenderà un carico semplice, in cui l’importo nozionale è trasferito dalla controparte alla parte all’inizio del contratto, e in senso inverso alla data di scadenza.

L’aggiunta di ulteriori elementi modificherà il contratto generato di conseguenza. Nella Figura 7, la parte dovrà trasferire il nozionale più il premio alla controparte alla data di scadenza, dando così alla controparte un incentivo per effettuare il prestito in primo luogo.

Entrare nel mondo DeFi con contratti smart

Come abbiamo visto, i professionisti della finanza e gli sviluppatori hanno ora un modo per iniziare a creare contratti finanziari intelligenti direttamente in Haskell o in Marlowe puro, o visivamente, utilizzando il Marlowe Playground, a seconda della loro esperienza di programmazione. Nel Playground, è possibile simulare e analizzare i contratti creati per verificare che funzionino correttamente e che siano pronti per essere rilasciati nel mondo della finanza decentralizzata quando la fase Goguen di Cardano sarà implementata. Il team Marlowe di IOHK continuerà a implementare gli esempi dello standard Actus, mentre ci prepariamo a finalizzare l’implementazione di Marlowe su Cardano, e a portare i contratti finanziari intelligenti nella blockchain stessa.