🛠 Juli Neueste Entwickler-Update – Aufbau des Kerns von Tau Nets TestNet Alpha Das Team hat den Fortschritt in Richtung TestNet Alpha vorangetrieben, indem es die Blockerstellung abgeschlossen, die Parsing-Leistung verbessert und neue Algorithmen zur Normalisierung von Formeln entwickelt hat. Höhepunkte: - TestNet Alpha: Blockerstellung, Verlinkung und Speicherung der Merkle-Wurzel abgeschlossen - SAT-Löser: Migration von Z3 zu CVC5 hat eine bessere Normalisierung und Erfüllbarkeit freigeschaltet - Parsing-Engine: 60% Leistungssteigerung + potenzielles neues Parsing-Patent - Sprach-F&E: Anti-Präfix-Normalisierung & Spezifikation zur Eliminierung von booleschen Quantoren bereit. Ohad hat die neuesten Arbeiten zur temporalen Logik überprüft. Tau Net und $AGRS liegen weit vor dem aktuellen akademischen Fortschritt auf diesem Gebiet. Zeitstempel: 00:12 - Karims Zusammenfassung 03:48 - David (Leitender Entwickler) - Erfolgreich von Z3 auf CVC5 umgeschaltet, was die Gesamtleistung des Lösers verbessert hat. - Arbeit an Normalisierung, Erfüllbarkeit und Interpretermodulen mit CVC5 abgeschlossen. - Ohads vorgeschlagene Methode zur Verzögerung der Literalauflösung für Bitvektor-Gleichungen implementiert. - Umar bei Code-Reviews und Debugging unterstützt. 05:36 - Lucca (Tau-Sprachentwickler) - Die erste Spezifikation für einen Algorithmus zur Eliminierung von Funktionsquantoren für die Verwendung in Taus Tabellenfunktion entwickelt. - In den Anti-Präfix-Normalisierungsalgorithmus integriert, um Formeln zu behandeln, die nicht von CVC5 abgedeckt sind. - Bereitet die Implementierung dieses Algorithmus vor, jetzt da der Pseudocode abgeschlossen ist. - Begann, Tomáš' neue Baumimplementierung zu verwenden und half, die letzten Probleme zu lösen. 08:30 - Andrei Korotkoff (Senior Developer) - Testnet-Alpha-Meilenstein für die Blockproduktion und -speicherung abgeschlossen, einschließlich Mempool-Verwaltung, Blockverlinkung, Berechnung der Merkle-Wurzel und Datenbankpersistenz. - Diese Arbeit legt die Grundlage für den nächsten Meilenstein: persistenter Kettenzustand basierend auf der Blockhistorie. - Ein komplexes Lasttestwerkzeug entwickelt, um das Verhalten des Tau-Interpreters und die Dynamik der Blockchain unter punktueller Revision zu simulieren. 11:20 - Tomáš Klapka (Senior Developer) - Mehrere Probleme beim Wechsel des Baums behoben, einschließlich Negationsbehandlung, Grammatikfehler und Typinferenzfehler. - Die Parser-Bibliothek so umgestaltet, dass sie nur Header enthält. - Docker-Unterstützung und nächtliche Releases für das TGF-Tool und den Parser erstellt. - Die Tau-Sprache aktualisiert, um den verbesserten Parser zu integrieren. 12:26 - Ohad (Gründer & CTO) - Konzentrierte sich auf das Design neuer Algorithmen und die Zusammenarbeit im Team. - Erforschte domänenunabhängige Sprachen zur Verbesserung der Entscheidungsverfahren. - Überprüfte aktuelle akademische Arbeiten zur temporalen Logik und bestätigte, dass Tau weiterhin der aktuellen Forschung voraus ist.