This post is a German translation of the blogpost ‘New Shelley formal specifications complete’ by Philipp Kant
Neue formale Spezifikationen für Shelley fertiggestellt
Formale Spezifikationen für Delegation und Incentives veröffentlicht
Das Ziel der Cardano Shelley-Ära ist es, Cardano vollständig zu dezentralisieren, über die föderierte Epoche hinauszugehen und die Kontrolle über das Ledger, über Stake-Pools an die Community zu übergeben.
Im Rahmen des Lieferprozesses von Shelley erstellen wir formale Spezifikationen, mit denen wir überprüfen können, ob der endgültige Code mit dem übereinstimmt, was die Forscher ursprünglich in ihren Publikationen vorgesehen hatten. Durch die Erstellung von implementierungs-unabhängigen Spezifikationen können wir Komponenten des Systems in verschiedenen Sprachen erstellen, mit der Gewissheit, dass sie richtig zusammenarbeiten.
Wir freuen uns, Ihnen mitteilen zu können, dass wir einen wichtigen Meilenstein auf dem Weg zu Shelley erfolgreich erreicht haben, wobei die wichtigsten Spezifikationen nun abgeschlossen sind. Das sind die fertiggestelltn Spezifikationen:
-
Technische Spezifikation für Delegation und Anreize in Cardano-Shelley: Beschreibt die Anforderungen und das Design für die Delegations- und Anreizmechanismen, die bei der Freigabe von Shelley von Cardano zu verwenden sind.
-
Eine formale Spezifikation des Cardano Ledgers: Gibt die Ledger-Regeln für Shelley an, einschließlich Delegation und Anreize.
-
Eine Spezifikation der nicht-integralen Berechnungen im Ledger: Dieses Dokument definiert eine Möglichkeit, nicht-integrale Berechnungen im Ledger von Shelley, die elementare mathematische Funktionen verwenden, genau zu berechnen. Das Hauptziel ist es, eine eindeutige Spezifikation bereitzustellen, die unabhängig von der Architektur oder der Programmiersprache die gleichen Ergebnisse liefert, um Forks aufgrund geringfügiger Unterschiede in den berechneten Ergebnissen zu vermeiden.
Um einen reibungslosen Übergang von der Byron- zur Shelley-Ära zu gewährleisten, muss der Shelley-Code mit den Byron-Regeln kompatibel sein. Um dies zu ermöglichen, haben wir auch Spezifikationen für die Byron-Ära erstellt:
-
Eine formale Spezifikation des Cardano Ledgers für die Byron Veröffentlichung: Dieser Beleg definiert die Regeln für die Erweiterung eines Ledgers um Transaktionen, wie sie in der Byron-Version des Cardano Ledgers implementiert sind.
-
Spezifikation der Blockchain-Layer (Byron): Dieses Dokument definiert Inferenzregeln für Operationen auf einer Blockchain als Spezifikation der Blockchain-Layer von Cardano in der Byron-Version und in einem Übergang zur Shelley-Version.
Der Prozess der Umsetzung dieser Spezifikationen in den aktuell erarbeiteten Code ist in vollem Gange, und die Spezifikationen werden sich durch das Feedback aus den Bereichen Mathematik, Forschung und Entwicklung weiter verbessern.
Die aktuellste Version der Spezifikationen finden Sie im GitHub-Repository Formale Modelle für Ledger-Regeln.