Simplicity: Teilen des Witness und Disconnect

Mein letzter Beitrag über Simplicity ging auf das Typsystem der Sprache ein und definierte ein Simplicity-Programm als einen Simplicity-Ausdruck, der eine leere Eingabe einer leeren Ausgabe zuordnet. Wir haben die Idee von Assertions (Zusicherungen) eingeführt, die den Abbruch eines Programms ermöglichen, und von Witnesses (Zeugen), die es Programmierern ermöglichen, Eingabedaten genau an den Stellen in Simplicity-Programme einzufügen, an denen sie benötigt werden. Zusammengenommen bedeutet dies, dass Programme ein nichttriviales Verhalten aufweisen können, auch wenn sie nominell weder Ein- noch Ausgaben haben.

Wir haben uns auch der Komplexität gestellt, selbst einfache mathematische Funktionen in Simplicity vollständig zu spezifizieren. Ein Tool, das wir zur Reduzierung der Komplexität verwendet haben, sind Jets, die optimierte Implementierungen bestimmter Simplicity-Ausdrücke bereitstellen. Dies ist eine nützliche Optimierung für Blockchain-Validatoren, bietet aber auch einen Mehrwert für den Simplicity-Programmierer, indem potenziell komplexe Funktionen in einem einzigen Jet gekapselt werden, der als Blackbox behandelt werden kann.

Tatsächlich ist jeder Simplicity-Ausdruck eindeutig identifizierbar, und zwar durch ein Objekt, das als Identitäts-Merkle-Root (IMR) bezeichnet wird. Der IMR eines Knotens wird durch Hashing seiner Quell- und Zieltypen, seines Kombinators und seiner untergeordneten Knoten (sofern vorhanden) berechnet. Mithilfe von IMRs können wir jeden Ausdruck eindeutig identifizieren und ihn dadurch als Blackbox behandeln, auch wenn wir keinen optimierten Jet haben, der ihn ersetzt.

Bit-Flipping neu betrachtet

Zu Beginn des letzten Beitrags haben wir den folgenden Code vorgestellt, der ein einzelnes Bit umdreht:

bit0 := injl unit : 1 * 1 -> 2
-- imr 31059b22...
bit1 := injr unit : 1 * 1 -> 2
-- imr 9864ae9d...

padR := pair iden unit : 2 -> 2 * 1
-- imr 457121c2...
bitflip := case bit1 bit0 : 2 * 1 -> 2
-- imr 7d5ff8d0...
main := comp padR bitflip : 2 -> 2
-- imr a6ecc3dd...

Wie wir der Typzuweisung in der letzten Zeile entnehmen können, nimmt dieser Ausdruck ein einzelnes Bit (den Typ „2“, der so genannt wird, weil er zwei mögliche Werte hat) und gibt ein einzelnes Bit aus. In dieser Auflistung haben wir auch die IMR jedes Ausdrucks berechnet. Wenn wir in Zukunft einen Simplicity-Ausdruck sehen, dessen IMR mit einem dieser Werte übereinstimmt, wissen wir genau, was wir sehen, egal wie komplex oder unscharf er zu sein scheint.

Denken Sie jedoch daran, dass für ein Simplicity-Programm unser Hauptausdruck den Typ 1->1 haben muss. Anstatt einen Eingabewert zu verwenden, werden wir Witness Knoten verwenden, und anstatt einen Ausgabewert zu haben, werden wir einfach behaupten, dass alle Zwischenwerte die Eigenschaften haben, die wir erwarten.

Als Beispiel hierfür optimieren wir unseren Ausdruck, um ein Programm zu erhalten, das bestätigt, dass ein Witness-Bit 0 ist. Wir tun dies, indem wir ein Witness-Bit nehmen, es umdrehen und es dann an den jet_verify-Jet übergeben:

witbit := witness : 1 -> 2-- imr ???
-- Assume we have the above expression, with the name bitflip.-- Notice that its IMR is the same as above.
bitflip :: 2 -> 2-- imr a6ecc3dd...zerovfy := comp bitflip jet_verify : 2 -> 1-- imr b3bca637...
main := comp witbit zerovfy : 1 -> 1– imr ???

Hier haben wir eine interessante Beobachtung. Der IMR eines Witness Knotens wird auf der Grundlage des Witness Werts berechnet, aber beim Schreiben eines Programms wissen wir noch nicht, welchen Wert der Witness haben wird. Das bedeutet, dass wir den IMR nicht kennen und den Ausdruck nicht als Blackbox behandeln können. Das Gleiche gilt für main, das vom witness Knoten abhängt, und für alle zukünftigen Ausdrücke, die möglicherweise von main abhängen.

Die gleichen Überlegungen gelten für disconnected (abgetrennte) Ausdrücke. Wenn wir den disconnect Kombinator verwenden, können wir ganze Ausdrücke und nicht nur Werte haben, die noch nicht bestimmt sind. Wir werden in einem späteren Beitrag über disconnect sprechen.

IMRs und CMRs

Unser Fehlen von IMRs macht in gewisser Weise Sinn: Wenn ein Ausdruck von Daten abhängt, die uns nicht zur Verfügung stehen, ist es nicht möglich, ihn genau zu spezifizieren. Andererseits wissen wir tatsächlich einiges über das betrachtete Programm: Wir wissen, dass es sich um einen comp-Kombinator handelt, dessen Kinder ein witness bzw. ein anderer comp-Kombinator sind, und so weiter. In diesem Fall kennen wir sogar die genauen Quell- und Zieltypen aller Knoten.

Mit anderen Worten: Wir haben unser Programm vollständig definiert, bis hin zu Witness Daten und disconnected Ausdrücken, die wir erst später füllen möchten. Wir haben die Teile unseres Programms definiert, die wir zum Generieren von Adressen und zum Empfangen von Coins benötigen, haben jedoch einige Teile undefiniert gelassen, bis wir bereit sind, die Coins auszugeben.

In Bitcoin Script haben wir die gleiche Unterscheidung zwischen commitment time (Bindungszeitpunkt) und redemption time (Einlösungszeitpunkt). Zum Bindungszeitpunkt wählen wir aus, welche öffentlichen Schlüssel wir verwenden möchten, und erst zum Einlösungzeitpunkt erstellen wir Signaturen mit diesen Schlüsseln. Aus historischen Gründen werden Bitcoin-Skripts dadurch gebunden, dass sie ihren Hash in ein anderes Skript einbetten, das manchmal als „scriptPubKey“, aber häufiger als Adresse bezeichnet wird.

Taproot verallgemeinert diesen Hash als Wurzel eines Merkle-Trees, sodass dieselbe Adresse an mehrere Skripte übergeben werden kann, von denen jedoch nur eines zum Zeitpunkt der Verarbeitung offengelegt wird.

In Simplicity gehen wir noch einen Schritt weiter und behandeln unser gesamtes Programm als Merkle-Tree. Dazu definieren wir auf jedem Knoten einen zweiten Hash, den Commitment Merkle Root (CMR). Im Gegensatz zum IMR bindet sich das CMR nicht an Witness Daten, disconnected Ausdrücke oder Typen. Es bindet sich lediglich zur Struktur des Programms.

Beim Einbetten von Simplicity-Programmen in die Blockchain ersetzen wir die Blätter eines Taproot-Baums, bei denen es sich normalerweise um Skripte handelt, durch die CMRs von Simplicity-Programmen.

witbit := witness : 1 -> 2-- cmr bf12681a...bitflip : 2 -> 2-- cmr 8f214cce...zerovfy := comp bitflip jet_verify : 2 -> 1-- cmr ab61cadb...
main := comp witbit zerovfy : 1 -> 1– cmr 58655557...

Jeder Knoten, einschliesslich Witness- und Disconnect-Knoten, verfügt über ein CMR. Und jeder Witness Knoten in jedem Programm hat das gleiche CMR.

Nennen und Teilen

In unseren bisherigen Simplicity-Programmen haben wir eine Reihe benannter Ausdrücke geschrieben, die sich namentlich auf jeden Ausdruck in einem späteren Ausdruck beziehen. Natürlich beschränken wir uns nicht darauf, Namen nur einmal zu nennen. Dieses Konzept ist für die Nutzung von Simplicity von wesentlicher Bedeutung. Wir bezeichnen die Wiederverwendung von Namen oder allgemeiner das Zusammenfassen mehrerer Kopien desselben Ausdrucks zu einer einzigen als Teilen.

In der Blockchain gibt es eine Konsensregel, dass in Transaktionen codierte Simplicity-Ausdrücke vollständig geteilt werden. Das heisst, es ist tatsächlich illegal, zwei Knoten zu kodieren, die denselben IMR haben. Dadurch wird sichergestellt, dass Programme möglichst kompakt codiert werden und dass ihre Codierung kanonisch ist. das heisst, es besteht kein Potenzial für “Malleability” (Formbarkeit). Diese Regel nutzt jedoch die Tatsache aus, dass Programme nur On-Chain erscheinen, wenn alle Witness Knoten gefüllt sind, und daher jeder Knoten über einen IMR verfügt.

Zur Commitment-Zeit, wenn wir Programme definieren und Adressen berechnen, ist die Sache nicht so einfach. Lassen Sie uns die Feinheiten erkunden, die sich aus dem Teilen ergeben, bevor unsere IMRs in Stein gemeisselt sind.

Im Wesentlichen muss sich ein Name jedes Mal, wenn er verwendet wird, auf einen Knoten mit demselben IMR beziehen. Das Überraschende daran ist, dass der von uns geschriebene Code, wie wir gesehen haben, eigentlich nur ausreicht, um das CMR eines Knotens zu definieren, nicht aber dessen IMR.

Sehen wir uns ein einfaches Beispiel an, wo dies zu Problemen führen könnte. Werfen wir einen Blick auf unser ursprüngliches Bit-Flipping-Programm und nehmen wir an, dass wir es satt haben, das gesamte Wort unit auszuschreiben.

u := unit  -- cmr 62274a89...

und versuchen es in unserem Programm zu verwenden:

bit0 := injl u : 1 * 1 -> 2-- cmr bd0cce93...bit1 := injr u : 1 * 1 -> 2-- cmr 79a70c6a...
padR := pair iden u : 2 -> 2 * 1– cmr 7751cd1c...bitflip := case bit1 bit0 : 2 * 1 -> 2– cmr 1d4aa8f4...main := comp padR bitflip : 2 -> 2– cmr 8f214cce...

Aber wenn wir versuchen, dies zu analysieren, um eine Adresse zu erhalten, erhalten wir einen Typfehler bei der Definition von padR! Der Grund dafür ist, dass während der Typ des unit Kombinators in Bit0 und Bit1 1 * 1 -> 1 ist, der unit Kombinator in padR den Typ 2 -> 1 hat. Die Quelltypen der unit Kombinatoren sind völlig uninteressante Details eines Simplicity-Programms. Dennoch ist es wichtig[1], dass wir in dieser Hinsicht konsequent sind.

Die Lösung hier ist einfach: Wir können den Namen u in bit0 und bit1 wiederverwenden, aber für padR brauchen wir einen neuen unit Kombinator.

So weit, ist es gut; Diese Art von Problem ist jedem Programmierer bekannt, der mit stark typisierten Sprachen arbeitet, insbesondere solchen, die Typinferenz unterstützen, sodass die Variablentypen nicht sofort offensichtlich sind. Aber mit Simplicity gibt es noch ein interessanteres Problem, über das wir stolpern könnten.

Betrachten wir das folgende Programm, das prüft, ob der Benutzer einen SHA256-„Fixpunkt“ gefunden hat, d. h. eine Eingabe, deren SHA256-Hash mit sich selbst übereinstimmt. Da es sich bei SHA256 um eine kryptografische Hash-Funktion handelt, sollte dies unmöglich sein, sodass in diesem Programm gespeicherte Coins nicht mehr ausgegeben werden können.

    -- Witnesses
    -- CMR: bf12681a...
    -- IMR: [none]
    wit_input := witness

    -- All jets have source type 1; but to use the `pair` combinator
    -- we want one with source type 2^256. To get this, we compose
    -- it with unit.
    -- CMR: a520761f…
    -- IMR: 21182050...
    sha256_init : 2^256 -> _
    sha256_init := comp unit jet_sha_256_ctx_8_init

    -- Using this, we can write a self-contained "take 32 bytes and
    -- compute their sha2 hash" function.
    -- IMR: 8e341445...
    -- CMR: bf70ec35...
    sha256 : 2^256 -> 2^256
    sha256 := comp
        comp
            pair sha256_init iden
            jet_sha_256_ctx_8_add_32
        jet_sha_256_ctx_8_finalize

    -- Finally, our main function takes an input witness, hashes it,
    -- and compares the input and output to check for a fixpoint.
    -- CMR: 9b3b900a...
    -- IMR: [none]
    main := comp
        comp
            pair (comp wit_input sha256) wit_input
            jet_eq_256
        jet_verify

Hier haben wir den Namen wit_input wiederverwendet. Unsere Regel ist, dass wir Namen nur dann wiederverwenden können, wenn alle Verwendungen denselben IMR haben, aber hier haben wir nicht einmal einen IMR zum Vergleich. Wird das zum Problem werden?

Betrachten Sie nun diese alternative Version von main, die einen zweiten Witness, wit_output, nimmt und diesen mit dem Hash von wit_input vergleicht. Es ist trivial, diesen neuen wit_input zu erfüllen: Er stellt irgendetwas für wit_input bereit, und seinen SHA256-Hash für wit_output.

    -- Witnesses
    -- CMR: bf12681a...
    -- IMR: [none]
    wit_input := witness
    wit_output := witness

    [...rest of program elided...]

    -- CMR: 9b3b900a...
    main := comp
        comp
            pair (comp wit_input sha256) wit_output
            jet_eq_256
        jet_verify

Hier ist es wichtig zu beachten, dass diese beiden Programme, unser Fixpunkt-Prüfprogramm und das trivial lösbare Programm, denselben CMR und daher dieselbe Bitcoin-Adresse haben. Dies liegt daran, dass sich Simplicity nicht ans Teilen bindet. Diese subtile, aber entscheidende Tatsache bedeutet, dass unser Fixpunktprogramm trivial ist und nicht, dass es unmöglich ist, Münzen auszugeben.

Glücklicherweise verhindert Simplicity, dass wir diesen Fehler machen. Wenn wir versuchen, unsere Originalversion des Programms zusammenzustellen, erhalten wir die folgende Fehlermeldung:

Error: witness/disconnect node `wit_input` was accessible by two distinct paths from the same root

Was uns dies in etwas umgangssprachlicher Sprache sagen soll, ist, dass es uns einfach nicht gestattet ist, Witness- oder disconnect Knoten oder Ausdrücke, die sich darauf beziehen, zu teilen. Dies liegt daran, dass solche Knoten am Ende möglicherweise nicht gleich sind, selbst wenn sie identische Typen und CMRs haben.

Zum Zeitpunkt der Einlösung, wenn Witnessdaten und disconnected Ausdrücke vorhanden sind, verfügt jeder Knoten über ein IMR und es ist eindeutig, ob die Knoten gleich sind. Wenn zu diesem Zeitpunkt zwei Witnesses anwesend wären und dieselben Typen und Werte hätten, würden sie geteilt. Diese gemeinsame Nutzung hängt jedoch von den besonderen Werten ab, die für jeden Witness Knoten ausgewählt werden. Diese werden nicht zum Zeitpunkt der Bindung festgelegt und spiegeln daher nichts über die tatsächliche Struktur des Programms wider.

Um unser Programm in Ordnung zu bringen, gibt es einige Strategien, die wir verfolgen könnten. Eine wäre, zwei Witness Knoten mit unterschiedlichen Namen zu definieren und den Jet jet_eq_256 zu verwenden, um zu bestätigen, dass sie beide gleich sind. Dies würde zwar funktionieren, aber die Komplexität des Codes erhöhen, was die Überprüfung oder Erweiterung erschwert. Ein direkterer Ansatz besteht darin, die Ausgabe eines einzelnen Witness Knotens zu duplizieren.

Wir tun dies, indem wir unseren Check aus main in seinen eigenen Ausdruck ziehen, auf dessen Eingabewert der iden-Kombinator zweimal zugreift:

    -- IMR: 5ddb65c2...
    -- CMR: 198bfeb5...
    assert_fixpoint : 2^256 -> 1
    assert_fixpoint := comp
        comp
            pair (comp iden sha256) iden
            jet_eq_256
        jet_verify

    -- CMR: ac8df50b...
    -- IMR: [none]
    main := comp wit_input assert_fixpoint

Dieses Programm wird fehlerfrei akzeptiert.

Zusammenfassung

Wie bei gewöhnlichen Taproot-Transaktionen werden Adressen aus Commitments zu Programmen abgeleitet, die Programme selbst werden jedoch erst nach einiger Zeit bekannt gegeben. Ausserdem offenbaren wir, wie bei Taproot, in Simplicity nur die Teile des Programms, die tatsächlich verwendet werden.

Bitcoin Script hat eine strikte Trennung zwischen Programmcode und Witness Daten, sodass das On-Chain offengelegte Programm dasselbe ist wie das in Adressen festgelegte Programm (abgesehen vom “Pruning”). Witness Daten werden separat codiert und dem Programmcode als Eingabe bereitgestellt. Im Skript gibt es keine Vorstellung von der gemeinsamen Nutzung oder von disconnected Ausdrücken, sodass Funktionen wie Delegation fehlen (und Funktionen wie Schleifen sind sehr ineffizient zu implementieren).

In Simplicity hängen wir stattdessen Witness Daten direkt an unsere Programme an und bestehen beim Codieren von Programmen darauf, dass Knoten niemals wiederholt werden. Diese Kombination erfordert eine überraschend subtile Vorstellung von „Identität“, die es uns, wenn wir sie auf textcodierte Programme anwenden, ermöglicht, Namen auf weitgehend natürliche Weise wiederzuverwenden. Doch auch hier gibt es potenzielle Fallstricke, die mit unserem Tooling vermieden werden können.

In unserem nächsten Beitrag befassen wir uns mit dem Pruning, also dem Prozess, bei dem ungenutzte Knoten verborgen bleiben, sowie mit seinen Interaktionen mit Witness und dem Typsystem.

Beteiligen Sie sich bis dahin an den Simplicity-Diskussionen auf GitHub, um mit der Community in Kontakt zu treten, und folgen Sie uns unter @blksresearch auf Twitter, um über die neuesten Simplicity-Ankündigungen auf dem Laufenden zu bleiben.

^[1]Theoretisch hätte Simplicity polymorphe Typen unterstützen können, wodurch derselbe unit Kombinator mit unterschiedlichen Typsignaturen hätte verwendet werden können. Abgesehen von der erhöhten Komplexität bei der Verwendung und Analyse der Sprache hätte dies jedoch auch die rechnerische Komplexität der Typinferenz erhöht, eine Aufgabe, die von allen Validatoren in allen Programmen erledigt werden muss.