Zusammenstellung der Formalitäten zum EVM – Victor Maia

Kosten einer Beta-Reduktion: ~ 200 Gas

Das ursprüngliche Ethereum-Back-End für Formality ist in Version 0.1.239 implementiert! Auf diese Weise können Sie Funktionsprogramme höherer Ordnung innerhalb der Blockchain bewerten. Hier werde ich diese neue Funktion dokumentieren.

Erstellung der Formalitäten zum EVM

Die Benutzung ist einfach. Schreiben Sie zunächst ein Formalitätsprogramm:

T Nat
| Null
| succ (pred: Nat)Doppel (n: Nat): Nat
Fall n
| null => null
| succ => succ (succ (double (n.pred)))Hauptleitung: Nat
double (succ (succ (succ (succ (null)))))

Das ist ein reines Funktionsprogramm, das die natürliche Zahl 4 verdoppelt. Beachten Sie, dass dies nur ein Beispiel für die algebraische Datentyp-Manipulation ist: Für tatsächliche Zahlen würden Sie offensichtlich stattdessen native Ints verwenden. Um dies in Ethereum zu kompilieren, speichern Sie es als main.fm, dann tippe fm -E main / main. Dies wird Folgendes ausgeben:

6023600060051b526022600160051b526003600260051b526042600360051b526003600460051b526062600560051b526003600660051b526082600760051b526003600860051b526013600960051b5263ffffffff6002600060005b8063ffffffff1415156106ff5782600f166101a10261007601565b6305f5b9f0505050505b8063ffffffff1415156100c55782600f166002148215166100a3575050506100c0565b6305f5b9f150600191508260041c60010160051b516000826100c6565b610080565b5b6106fa56000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000 00000000000000000000000000000000000000000000000000000000000000000000005b6305f5b9f2508260041c60051b518063ffffffff146102415760041c8160041b9060051b52610243565b505b90506001908260041c60010160051b516000826001016106fa56000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005b6305f5b9f3508260041c60051b516305f5b9f45080600f166001146103df5760008261045d565b6305f5b9f5508060 041c60051b518063ffffffff1415610405576305f5b9f7505061041f565b6305f5b9f6508460041c60010160051b519060041c60051b525b6305f5b9f85060041c60010160051b51925050508163ffffffff141561044c57806000526000600061045c565b8360041c830160051b5290506000905b5b6106fa56000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005b6305f5b9f95063ffffffff59525960011c8360041c60550261057701565b80607001595280602101595263ffffffff595280604101595280606001595280606201595263ffffffff595263ffffffff595260016106cb560000000000000000000000000000000000000000000000000000005b80603001595280602101595263ffff ffff595263ffffffff595260016106cb56000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000005b80604001595280602201595280604201595280606101595263ffffffff5952601359528060d0015952806082015952600359528060a2015952600359528060c20159526023595263ffffffff595260016106cb565b6023595280602201595260035952806042015952600359528060620159526003595280608201595260035952601359526002000000000000000000000000000000000000000000000000000000000000000000005b01925050508163ffffffff14156106e95780600052600060006106f9565b8360041c830160051b5290506000905b5b61005b565b00

Dies ist ein Ethereum-Bytecode, der bei der Auswertung ein reines Formalitätsprogramm in der Blockchain reduziert und das Ergebnis dieser Berechnung im Speicher des Vertrags belässt. So wird beispielsweise im obigen Programm die natürliche Zahl 8 im Speicher belassen, wobei die Lambda-Byte-Darstellung von Formality verwendet wird.

Wie viel kostet es?

Das oben genannte Programm kostet 37750 Benzin in der Blockchain von Ethereum. Zum Vergleich: Reduziert durch Interaktionsnetze (der optimale Algorithmus für die Reduktion von Funktionen höherer Ordnung) kostet es 141 Graph-Rewrites. Das gibt uns ungefähr 267 Gas pro Beta-Reduktion, was wirklich niedrig ist: nur 33x mehr als ein natives MULMOD und dasselbe wie ein SLOAD.

Natürlich beinhalten Graph-Rewrites nicht nur Beta-Reduktionen, sondern auch die Kosten für das Kopieren von Daten. Daher variiert dieser Durchschnitt je nach Eingangsbedingung zwischen 150 und 400 Gasen pro Beta-Reduktion. Dies ist zwar nicht so billig wie Solidity, ermöglicht es uns jedoch, formal überprüfte, elegante Funktionsprogramme zu absolut akzeptablen Kosten auszuführen. Ich würde sogar sagen, dass es das Konzept der "funktionalen Blockketten" fast überflüssig macht (insbesondere, wenn sie nicht einmal eine richtige Beweissprache enthalten), aber ich möchte keinen Flammenkrieg beginnen!

Einschränkungen, zukünftige Arbeit

Im Moment werden nur reine Programme auf Ethereum evaluiert. Es gibt noch keine Smart-Contract-Integration. Dazu ist eine ABI-konforme, nebenwirkungsfreie Laufzeit erforderlich. Anschließend erstellen wir einen neuen Blog-Beitrag, in dem erklärt wird, wie formal überprüfte Formalitätsprogramme für Ethereum bereitgestellt werden. Wenn Sie es derzeit in einem Smart-Vertrag verwenden möchten, müssen Sie seine Bedingungen manuell codieren.

Dies ist auch nur mit der schnellsten Teilmenge der Formalität vereinbar, nämlich den affinen Begriffen. Der Typprüfer teilt Ihnen mit, ob Ihr Programm geeignet ist, indem er seinen Typ mit einem markiert . Die Dokumentation enthält Hinweise zum Erstellen affiner Programme. Muttersprachliche Nummern sind noch nicht verfügbar, werden aber in Kürze hinzugefügt. Zukünftig könnten auch elementare und exponentielle Programme hinzugefügt werden, aber diese werden wahrscheinlich zu langsam sein, um überhaupt einen Wert zu haben.

Diese Funktion kompiliert native Formalitätsprogramme direkt in Ethereum, einschließlich Funktionen und Schließungen höherer Ordnung. Soweit ich weiß, wurde dies als erstes versucht. Wenn jemand Interesse daran hat, die bestmögliche Leistung zu erzielen, kann er es sich möglicherweise nicht leisten, die Abschlüsse in der Blockchain zu bewerten. In diesem Fall ist möglicherweise ein konservativerer und schnellerer Ansatz für die Erstellung eines formal verifizierten DSL vorzuziehen. Wir werden Ihnen in Zukunft erklären, wie das geht.

Beispiel

Ein vollständiges Beispiel finden Sie in diesem Github-Repository. Es kompiliert ein Formalitätsprogramm mit EVM-Bytecode, führt es im EVM aus und dekompiliert den Speicher zurück, um den normalisierten Term wiederherzustellen. Versuch es!