Im Gegensatz zu den meisten Programmiersprachen werden Simplicity-Ausdrücke aus einer Reihe von Kombinatoren erstellt, die Ausdrücke aus kleineren aufbauen. Solche Ausdrücke stellen Funktionen dar, die eine Eingabe entgegennehmen und diese einer Ausgabe zuordnen.

Hier ist das einfachste Simplicity-Programm:

main := iden

Programm nimmt eine leere Eingabe und erzeugt eine leere Ausgabe. Machen wir etwas Interessanteres, indem wir ein Bit nehmen und es invertieren:

   bit0 := injl unit : 1 * 1 -> 2
   bit1 := injr unit : 1 * 1 -> 2

   padR := pair iden unit     : 2 -> 2 * 1 
   bitflip := case bit1 bit0  : 2 * 1 -> 2
   main := comp padR bitflip  : 2 -> 2

Hier ist der endgültige Simplicity Ausdruck unsere main Funktion. Wenn wir von unten nach oben lesen, können wir erkennen, dass es sich um die Zusammensetzung mehrerer kleinerer Funktionen handelt, die schließlich in unit Kombinatoren münden. Unit Kmbinatoren erzeugen eine leere Ausgabe. Zusammen mit iden, das eine beliebige Eingabe annimmt und unverändert zurückgibt, und witness, das einen extern bereitgestellten Wert ausgibt, bilden unit Kombinatoren die Grundlage für jeden Simplicity-Ausdruck.

In diesem Codeausschnitt haben wir Typ Annotationen bereitgestellt, um anzugeben, welche Daten von jedem Teil des Ausdrucks zum nächsten fließen. Hier stellt „1“ den unit Typ dar, den wir als „leeren Output“ bezeichnet haben. „2“ stellt ein Bit dar, das den Wert 0 oder 1 annehmen kann.

Machen Sie sich keine Sorgen, wenn Sie diesem Ausschnitt nicht im Detail gefolgt sind. Es dient nur dazu, visuell zu zeigen, wie Simplicity-Code aussieht. Später in diesem Beitrag werden wir ein interessanteres Programm genauer analysieren.

Eine Spezifikationssprache

Letztendlich drücken alle Programmiersprachen die Idee aus, Berechnungen zu kombinieren, um größere Berechnungen zu erstellen. Bitcoin Script (wie Forth oder PostScript) erledigt dies mithilfe einer Stackmaschine, in der jede Berechnung nacheinander eine Liste von Datenobjekten manipuliert. Das EVM von Ethereum verwendet eine Funktionsaufrufarchitektur, bei der Code andere Codeblöcke (möglicherweise in anderen Verträgen) aufrufen kann, die Daten als Eingabe verwenden und Daten als Ausgabe zurückgeben. Dies ist auch das Modell, das heute von nahezu allen gängigen Programmiersprachen verwendet wird.

Programmiersprachen nutzen Seiteneffekte, um mit der Aussenwelt zu interagieren, beispielsweise dass eine Transaktion ausgeführt wird. In EVM haben Verträge auch Zugriff auf Key-Value-Speicher, die es ihnen ermöglichen, den Status über Transaktionen hinweg aufrechtzuerhalten, ohne ihn explizit weiterzugeben.

Sowohl in Bitcoin Script als auch in EVM kann die Bit Invertierung mit einem einzigen Opcode durchgeführt werden (obwohl die Bitcoin-Version viele verschiedene Eingaben annehmen kann, von denen die meisten nicht wie Bits aussehen, während die EVM-Version bitweise, aber immer auf 256 Bits gleichzeitig agiert). Es ist vernünftig zu fragen, warum das Simplicity-Modell bei so einfachen Dingen zu einer solchen Ausführlichkeit führt.

Unser Ziel mit Simplicity ist es, die Semantik von Programmen formal zu spezifizieren, sowohl im Hinblick darauf, welche Funktionen sie darstellen, als auch darauf, welche Rechenressourcen für ihre Auswertung erforderlich sind. Im Prinzip wäre es möglich, eine Sprache formal zu spezifizieren, die wie Bitcoin Script oder EVM funktioniert, aber die Aufgabe wäre äußerst schwierig und das Ergebnis wäre für jedermann fast genauso schwer zu überprüfen. Stattdessen haben wir mit Simplicity einen kleinen Satz grundlegender Kombinatoren definiert, von denen jeder eine mathematisch grundlegende Art der Kombination von Funktionen widerspiegelt. Die Semantik der resultierenden Sprache ist so klein, dass sie auf ein T-Shirt passt.

In der Praxis wird dieser Code für Dinge wie die Bit Inversion nur einmal geschrieben und dann wiederverwendet. Tatsächlich haben wir das Schreiben für Sie übernommen und es bereits in die Sprache integriert. Wenn Sie Ihren eigenen Code schreiben, können Sie anstelle des obigen Codes einfach die Kurzform jet_not verwenden. Wir werden im nächsten Abschnitt mehr über jets sprechen.

Irgendwann wird in der Praxis fast niemand mehr Simplicity-Code schreiben. Simplicity bietet eine klar definierte Grundlage für Blockchain-Programme, aber sie ist auch nur das: eine Grundlage. Die eigentliche Arbeit wird in höheren Sprachen erledigt, die zusammen mit Beweisen für ihre korrekte Funktionsweise bis zum Simplicity-Code kompiliert werden.

Programme versus Ausdrücke

Ausdrücke mit trivialen Eingabe- und Ausgabewerten haben einen speziellen Namen. Wir nennen diese Ausdrücke Programme. Mathematisch gesehen gibt es nur eine Funktion, die eine triviale Eingabe einer trivialen Ausgabe zuordnet, daher ist es nicht offensichtlich, dass solche Simplicity-Ausdrücke überhaupt nützlich wären. Aber sie sind nicht nur nützlich, sie sind auch die einzigen derartigen Ausdrücke, die in der Blockchain zulässig sind!

Was ist also die Strategie? Es gibt tatsächlich deren zwei: Erstens weisen die in Adressen festgeschriebenen Simplicity-Programme Löcher auf, die erst dann gefüllt werden, wenn Coins tatsächlich ausgegeben werden; Das andere ist, dass Simplicity-Programme Seiteneffekte haben, die es ihnen ermöglichen, auf Blockchain-Daten zuzugreifen oder vorzeitig abzubrechen, wodurch sie die Grenzen reiner mathematischer Funktionen verlassen.

Es gibt zwei Möglichkeiten, Lücken in Simplicity-Programmen zu spezifizieren: die disconnect- und witness-Kombinatoren. Disconnect ist etwas subtil und wir haben in der Vergangenheit darüber gesprochen. Aber Witnesses sind sehr einfach: Der witness Kombinator gibt einen Wert eines bestimmten Typs namens witness zurück (z. B. eine digitale Signatur, ein Hash-Preimage oder eine bestimmte Auswahl an Signaturschlüsseln).

Es gibt auch zwei Möglichkeiten, wie Simplicity Seiteneffekte unterstützt: zum einen durch die Introspektion von Transaktionsdaten (auf die wir in einem späteren Beitrag noch näher eingehen werden) und zum anderen durch assertions. Assertions stoppen die Programmausführung. In Bitcoin Script wird der VERIFY-Opcode für assertions verwendet und ermöglicht, dass das Programm fehlschlägt, wenn es auf eine ungültige Signatur oder andere Daten stößt. EVM verwendet den STOP-Opcode für denselben Zweck.

Wir können nun sehen, wie ein Programm, dessen Eingabe- und Ausgabetypen nominell trivial sind, tatsächlich eine nützliche Berechnung durchführen kann: Witnesses dienen der Funktion von Programmeingaben, während assertions eine “pass/fail“-Programmausgabe liefern.

Betrachten wir ein anderes Beispiel. Hier ist ein Programm, das zwei Witnesses nimmt und sie auf Gleichheit prüft:

-- Witnesses
wit1 := witness : 1 -> 2^32 
wit2 := witness : 1 -> 2^32 

-- Program code
pr1 := pair wit1 wit2 : 1 -> 2^64
jt2 := jet_eq_32      : 2^64 -> 2
cp3 := comp pr1 jt2   : 1 -> 2
jt4 := jet_verify     : 2 -> 1

main := comp cp3 jt4  : 1 -> 1

Wir können dieses Programm von unten nach oben lesen: Das Programm selbst ist ein einzelner Ausdruck namens main vom Typ 1->1. Dabei gibt der „Typ“ eines Ausdrucks an, welche Art von Werten er als Eingabe und Ausgabe annimmt. Der Typ 1 hat nur einen einzigen Wert und beschreibt daher keine Informationen. Der Typ 2 hat zwei mögliche Werte, kann also ein einzelnes Bit darstellen, 2^32 ist eine 32-Bit-Zeichenfolge und so weiter.

Aus der unteren Gleichung sehen wir, dass main die Composition der Ausdrücke mit den Namen cp3 und jt4 ist. Dann ist cp3 selbst die Composition von pr1 und jt2 und so weiter. In diesem Programm werden fünf Kombinatoren verwendet:

• comp, oder Composition, nimmt zwei Ausdrücke und wertet den zweiten aus, wobei die Ausgabe des ersten als Eingabe dient.
• pair nimmt zwei Ausdrücke und erzeugt einen neuen Ausdruck, dessen Ausgabe ein Wertepaar ist: Der linke Teil ist die Ausgabe des ersten Ausdrucks und der rechte Teil die Ausgabe des zweiten.
• witness nimmt keine Eingabe, hat aber einen polymorphen Typ als Ausgabe: Welcher Typ auch immer benötigt wird, damit das Programm einen Sinn ergibt, das ist sein Typ. Und der von ihm erzeugte Wert wird zum Evaluierungszeitpunkt bereitgestellt.
• jet_eq_32 ist ein jet, was bedeutet, dass es sich um einen einzelnen Kombinator handelt, der einen größeren Simplicity-Ausdruck ersetzt. Der ersetzte Ausdruck wird seine Specification genannt, und ein Simplicity-Interpreter kann den Jet entweder durch Auswertung der Spezifikation oder durch die Verwendung von optimiertem Maschinencode auswerten, der den gleichen Effekt hat. Dieser spezielle Jet nimmt zwei 32-Bit-Werte und gibt ein einzelnes Bit aus, das angibt, ob die beiden Werte gleich (1) oder ungleich (0) waren.
• jet_verify ist auch ein jet. Dieser verwendet ein einzelnes Bit als Eingabe und bricht das Programm ab, wenn dieses Bit 0 ist. Es gibt keine Ausgabe.

Zusammenfassung

Dies war ein ausführlicher Blogbeitrag, in dem wir gesehen haben, wie Simplicity-Code aussieht, und festgestellt haben, dass selbst scheinbar einfach erscheinende Funktionen ziemlich komplex aussehen können, wenn sie explizit geschrieben werden. Aber diese Komplexität spiegelt wider, was tatsächlich im Inneren vor sich geht. Als Spezifikationssprache ermöglicht uns Simplicity, alles explizit zu machen, sodass wir es mathematisch modellieren und die wesentlichen Eigenschaften beweisen können, die wir für unsere Anwendungen benötigen, und das dann einkapseln können, in der Gewissheit, dass wir eine grundsolide Grundlage für die Dinge haben, an die wir in unserem Code glauben..

Simplicity verfügt über mehrere weitere Kombinatoren und viele Jets, über die wir in zukünftigen Beiträgen sprechen werden. Während wir die Sprache aufbauen, werden wir weitere praktische Beispiele untersuchen und uns ansehen, was es bedeutet, Eigenschaften von Programmen zu „beweisen“.

In meinem nächsten Beitrag werde ich das Konzept des Teilens vorstellen, das die Verschmelzung zweier identischer Ausdrücke zu einem ermöglicht, und einige Feinheiten im Zusammenhang mit der Bedeutung von „identisch“ vorstellen.

Nehmen Sie an den Simplicity-Diskussionen auf GitHub teil, um Fragen zu stellen, mit der Community in Kontakt zu treten und Ihre Erkenntnisse zu teilen. Und folgen Sie uns unter @blksresearch auf Twitter, um über die neuesten Veröffentlichungen von Simplicity-Blogbeiträgen auf dem Laufenden zu bleiben.