Aan het begin van deze maand hebben we de broncode uitgebracht voor de blockchain-taal Simplicity.
Simplicity is ons antwoord op de problemen die ontstaan wanneer we uitgebreide smart contracts proberen om te zetten naar een blockchain-omgeving. Voor de komst van Simplicity bestonden programmeertalen veelal uit een compromis tussen expressiviteit en betrouwbaarheid. Ontwikkelaars konden ervoor kiezen om complexe maar onbetrouwbare smart contracts te bouwen, of het betrouwbaar maar simpel te houden. Met Simplicity wordt het eindelijk mogelijk voor ontwikkelaars om uitgebreide smart contracts te ontwerpen die tevens betrouwbare resultaten opleveren.
Simplicity is gebouwd om compatibel te zijn met het Elements-platform van Blockstream. Dat betekent dat ontwikkelaars die sidechains of op zichzelf staande blockchains bouwen met behulp van Elements straks ook gebruik kunnen maken van de functionaliteit van Simplicity. Gezien het Liquid-netwerk een implementatie is van Elements, zal deze ook Simplicity ondersteunen. Dit geeft gebruikers van Liquid interessante nieuwe mogelijkheden, zoals escrow met minimaal vertrouwen, vaults, en complexere smart contracts.
De broncode die deze maand is uitgegeven, bevat het volgende:
- Denotationele semantiek van de Simplicity-taal en de extensies, formeel gespecificeerd in Coq.
- Operationele semantiek van de Simplicity-taal, formeel gespecificeerd in Coq.
- Een interpreter, type-checker, en serialisatie van de Simplicity-taal, geschreven in Haskell.
- Voorbeelduitdrukkingen in Simplicity, waaronder cryptografische operaties zoals SHA-256 en verificatie van EC-Schnorr signatures.
- Een technisch rapport met details over de Simplicity-taal.
Waarom Simplicity?
Blockchains bevatten een aantal unieke uitdagingen die ervoor zorgen dat traditionele programmeertalen ongeschikt zijn.
- Alle gebruikers moeten het in elke omgeving eens zijn over het resultaat van een berekening.
- Elke participant in een smart contract moet zich van tevoren bewust zijn van alle mogelijke resultaten voor alle mogelijke inputs van een programma.
- Alle gebruikers moeten denial-of-service-attacks die resulteren in overdadig gebruik van geheugen of berekeningstijd, kunnen voorkomen.
- Elke participant in een smart contract moet zich van tevoren bewust zijn van de kosten van het uitvoeren van het programma voor alle mogelijke inputs.
Bestaande programmeertalen die zijn ontwikkeld voor blockchains, zoals de EVM van Ethereum, hebben deze uitdagingen niet geheel weten op te lossen. Recentelijk is een EVM-upgrade mislukt tijdens het testen omdat de implementaties het niet eens waren over het resultaat van een berekening. Bezittingen zijn gestolen en ook onbereikbaar geworden wegens logicafouten in smart contracts en programma’s die hun verbruikslimieten overschreden.
Daarentegen is de scripttaal van Bitcoin gelimiteerd tot combinaties van verificaties van signatures, timelocks, en hashlocks. Hoewel er indrukwekkende protocollen (zoals het Lightning Network) gebouwd zijn op deze primitieven, ontbreekt er bij de scripttaal van Bitcoin de expressiviteit die nodig is voor het maken van complexe smart contracts.
Simplicity is erop gericht om genoeg flexibiliteit en expressiviteit te bieden voor elke mogelijke berekening, terwijl het alsnog mogelijk blijft om de veiligheid en kosten van de smart contracts te verifiëren.
Wat is Simplicity?
Simplicity is een low-level programmeertaal en machine model voor op blockchains gebaseerde smart contracts. Het is van de grond af ontwikkeld voor simpele semantiek die zich leent voor statische analyse en redenering aan de hand van formele methodes. De Simplicity-taal is gedefinieerd door zijn implementatie in de Coq proof assistant.
Hoewel de taal zelf simpel genoeg is om op een T-shirt te passen, vertaalt de simpliciteit van de taal zich niet in simpliciteit in de ontwikkeling. Daar zijn een aantal redenen voor:
- Blockchains hebben een fundamenteel ander programmeermodel dan normaal programmeren. De taak van een blockchain is om berekeningen te verifiëren, en niet om berekeningen uit te voeren. Dit is een subtiel verschil, maar het verschil is krachtig, want het is daardoor mogelijk om de uitvoering van willekeurige code te verifiëren zonder dat daar turingvolledigheid aan te pas komt.
- Als een smart contract eenmaal is opgezet, is het niet meer te veranderen en is er geen mogelijkheid meer om fouten te verbeteren. Simplicity lost dit probleem op door gebruikers in staat te stellen om formeel te bewijzen dat hun smart contracts correct zijn.
- De Simplicity-taal is zeer low-level voor directe uitvoering, en lijkt daardoor meer op de assembly dan Java of Python. Uiteindelijk verwachten we dat gebruikers hun smart contracts schrijven in een high-level taal die vervolgens wordt gecompileerd naar Simplicity.
Wat is er nieuw?
Sinds onze laatst blogpost over Simplicity, zijn we hard aan het werk geweest om ons experimentele taalonderzoek om te zetten tot een formele taalspecificatie.
We hebben de Simplicity-taal opnieuw geïmplementeerd in de Coq proof assistant:
- We hebben denotationele semantiek voor de volledige Simplicity-taal, waaronder taalextensies die ondersteuning bieden voor witness data, asserties en delegatie.
- Een formele specificatie van een abstracte machine genaamd de “Bit Machine” die is gebaseerd op vrije categorieën, biedt operationele semantiek voor de Simplicity-taal.
- Een Haskell-implementatie die is ontwikkeld in tagless final style, maakt het mogelijk om te experimenteren met het evalueren, uitvoeren, en type-checken van Simplicity-uitdrukkingen.
- De modulaire aanpak van de extensies van de Simplicity-taal maakt het mogelijk om de gevolgen van taalextensies te negeren wanneer die niet worden gebruikt.
- We hebben een stel Simplicity-uitdrukkingen voor cryptografische primitieven, waaronder onze eigen opnieuw geïmplementeerde libsecp256k1 in Simplicity.
- Een technisch rapport dat een informele wiskundige specificatie van de Simplicity-taal geeft, en tevens gidsen voor biedt voor de ontwikkeling in Coq en Haskell.
Hoewel Simplicity nog steeds in ontwikkeling is, zijn we nu op een punt beland waar ontwikkelaars de Simplicity-taal zelf kunnen verkennen. Daarom wordt het tijd om de ontwikkeling van Simplicity open te maken en te beginnen met een mailing list.
Wat volgt
Er zijn veel gebieden waar Simplicity kan worden doorontwikkeld.
Aan onze kant zijn we het volgende van plan:
- De C interpreter afmaken.
- De implementatie van een bibliotheek van jets voor verschillende veelvoorkomende cryptografische functies.
- Gebruikmaken van Verifiable C om aan te tonen dat onze C interpreter en jets correct zijn.
- Simplicity integreren in het Elements-blockchainplatform.
Andere punten van ontwikkeling zijn:
- De ontwikkeling van code-optimalisatie voor Simplicity.
- De creatie van of het aanpassen van bestaande high-level platforms voor smart contracts, zoals Ivy, voor het genereren van Simplicity.
- Het combineren van de functionele correctheid van de cryptografische primitieven van Simplicity, met de formele correctheid van cryptografische protocollen om volledig geverifieerde smart contracts te bouwen.
We hopen dat u wilt meedoen aan ons project.