Zuerst stabile Identität. Dann Quelltextänderungen.
Der semantische Programmgraph macht Deklarationen, Typen, Effekte, Verträge, Ownership und Aufrufbeziehungen anhand stabiler Identitäten abfragbar. Version 0.8.0 erweitert dieses Modell um Regeln im Quellcode, geschützte Implementierungsreparaturen, umfassendere Rust-Schnittstellen und Entwicklungswerkzeuge.
entity Semaprax
status beta
snapshot 615e501
authority github.com/wavect/semaprax| Repository-Snapshot | 615e501 · 2026-10-06. Das Tag v0.8.0 verweist auf den festgehaltenen Quellcommit. Die exakte Tag-CI war erfolgreich. Daraus folgt keine allgemeine Produktions- oder Sicherheitsgarantie. |
|---|---|
| Status des Gesamtprodukts | 55 Teilweise · 0 Implementiert · 0 Fehlend |
| Graph- und Projektvertrag | Kanonischer Quellcode, stabile IDs und geprüfte Compiler-Repräsentationen verbinden Regeln, semantische Abfragen, Änderungen und Ausführung. Die je nach Feature gewählten Graph- und Project-Schemas behalten ihre eigenen Vorgaben für Zulassung, Kompatibilität und Host-Berechtigungen. |
| Veröffentlichte Betaversion | v0.8.0 · Veröffentlicht am 6. Oktober 2026 um 07:37 UTC. Alle 82 Jobs für den exakten Release-Tag waren erfolgreich. Veröffentlicht wurden drei Toolchain-Archive, SHA256SUMS, Attestierungen für jedes Archiv und eine signierte gemeinsame Herkunftsdokumentation. Der Release-Job prüfte den signierten Satz vor der Veröffentlichung unabhängig. Die Archive sind nicht notarisiert; reproduzierbare Builds werden nicht zugesichert. Eine Offline-Prüfung bestätigt keinen aktuellen Widerrufsstatus. Exakte Tag-CI. |
| Paket- und API-Vorschau | Die Veröffentlichung enthält nutzbare Profile für die Sprache, Quellcode-Regeln, Entwicklungswerkzeuge und Host-Integrationen. Für generierte Rust/npm-Pakete, öffentliche generische ABIs und weitere Plattformen gelten weiterhin eigene Entscheidungen über Veröffentlichung und Unterstützung. |
Semaprax prüft lesbaren .spx-Quellcode und löst ihn in HIR auf, die typisierte Repräsentation des Compilers. Quellcode und semantische Identitäten binden Abfragen, Beweispflichten, Kandidatenänderungen und Ausführung an das untersuchte Programm. Coding-Agenten können die Werkzeuge rund um diesen Kern nutzen. Laufzeit-Agents dekodieren separat Vorschläge, autorisieren Effekte und ändern ihren Zustand unter explizit bereitgestellten Host-Berechtigungen.
Lesbarer .spx-Quellcode bleibt die kanonische Darstellung in Git. Ein explizites @id identifiziert eine Deklaration auch nach unterstützten Änderungen ihres Anzeigenamens. Vom Compiler abgeleitete Revisionen binden Quellcode und ausgewählte Prelude; Graph-Formate machen diese Fakten zugänglich, ohne den Quellcode zu ersetzen.
Wähle Deklaration, Richtung, Tiefe, Knotenzahl und Bytegrenze. Aufgabenkontext und Projektionen als Text, Binärdaten oder model-text erhalten die exakte Replay-Prüfung anhand der ausgewählten Fakten. Der native semantische Kontextbroker kann Graft oder Graphify für zusätzliche Repository-Navigation nutzen, ohne einen externen Index zur Wahrheitsquelle des Compilers zu machen.
Native Regeldeklarationen geben Vertragsanforderungen und relationalen Anforderungen dauerhafte Identitäten. Ein gesondert ausgewähltes LawSet legt das vollständige Inventar und die strenge Prüfregel fest. Installierte Lean/Z3-Adapter beweisen zugelassene skalare, modulare, strukturierte und Listenregeln. Veraltete, nicht unterstützte, unbekannte und widerlegte Ergebnisse bleiben unterscheidbar. Reparaturkandidaten müssen die erhaltene Anforderung erfüllen.
Kontext prüfen, Kandidaten ableiten, Auswirkungen und Review ansehen, Prüfungen erneut ausführen und anschließend die Anwendung autorisieren. Begrenzter Ausdrucksersatz, strukturelle Änderungen und festgelegte Kompositionen behalten jeweils ihre Operations- und Revisionsgrenzen. Für Änderungen an Quellcode-Regeln und für Implementierungsreparaturen gelten getrennte Schutzregeln.
Verwaltete Workspace-Generationen, Kandidatennachweise und Project-Revisionsspeicher binden die Veröffentlichung an den geprüften Kandidaten. Die Rust-Einbettungs-API bietet begrenzte Eingaben und opake Sitzungen. Die Validierung mehrerer Dateien allein aktualisiert keine beliebigen Dateien, Git-Referenzen oder Editorpuffer.
Zugelassene Profile umfassen Records, Varianten, Klassen, Vererbung, Generics mit begrenzter Argumentinferenz, Option/Result, Schleifen, Iteratoren, Funktionswerte, Strings und Bytes. Das unveränderliche List<i64> ergänzt persistente nil/cons/uncons-Operationen. Allgemeine Constraints und beliebige Kombinationen benötigen weiterhin eine eigene Zulassung.
Eigene Werte, geliehene Ansichten, Aufräumpläne und ausgewählte Ressourcenkompositionen sind ausführbar. Eng begrenzte Closure-Profile umfassen eigene Bytes-Captures, kopierte skalare Snapshots, transaktionalen veränderlichen Skalarzustand und synchrone Captures geliehener Texte. Jedes Profil prüft seine Regeln für Escape, Move, Rollback und Cleanup; weitergehende Beziehungen zwischen Lebensdauern bleiben offen.
Vorbereitete Rust-API-Indizes wählen unterstützte Imports und exakte Cargo-Eingaben aus. Generierte Adapter für Besitzer, geliehene Ansichten und Callbacks verbinden geprüften Quellcode mit echten Regex/Url- und Serde/Iterator-Consumern. Eine Future-Brücke für denselben Thread verwendet einen vom Aufrufer bereitgestellten Executor. Annahmen über Fremdcode bleiben explizit; generierter Verbindungscode beweist nicht die Interna einer Crate.
Initialisieren, beobachten, vorschlagen, dekodieren, autorisieren, ausführen und Zustand reduzieren. Die Autorisierung wiederholt sich in jeder Runde; der Reducer wählt Continue, Complete, Suspend oder Fail. Live-Standardpfade verwenden den Interpreter. Optionale Bibliothekspfade akzeptieren vom Aufrufer bereitgestellte native C11- oder Core-Wasm-Hosts für Stufen mit begrenzten lokalen Paritätsnachweisen.
Explizite Adapter stellen Transport, Zugangsdaten und Speicher bereit. Dauerhafte Profile bestätigen die Ausführungsabsicht vor dem Aufruf und behandeln ungeklärte Versuche weiter als unsicher. Grenzen und Belege trennen Aufrufe, Arbeit, Bytes, Tokens und Kosten. Generische Wiederholungen und Failover im Host haben andere Verträge als der gebundene Quellmodellpfad. Dieser wechselt Anbieter nicht automatisch und wiederholt keine Arbeit mit ungeklärtem Ergebnis.
Der Interpreter bietet begrenzte sequenzielle und kontrollflussabhängige yields, ausgewählte Übergaben eigener Bytes und authentifizierte dauerhafte Quellcode-Profile. Der öffentliche Teilbereich für Agents mit Ownership hat einen Lebenszyklus mit zwei Runden und ausgewählte Prüfungen für Prozessneustarts. Die normalen Native/Wasm-Emitter lehnen Funktionen mit yield weiterhin ab; ein allgemeiner Scheduler und eine universelle Continuation-ABI bleiben offen.
Die Entwicklungswerkzeuge der vollständigen Toolchain koordinieren explizite Aufgaben, Compiler-Rückmeldungen, Anbieterbeschreibungen, projektspezifische Locks und Vertrauen, Modellauswahl, Skills und Brücken. Offizielle Ponytail/Caveman-Pakete, Graft/Graphify-Adapter und RTK-Modellansichten unterstützen ausgewählte Abläufe. Maßgebliche Befehlsergebnisse bleiben von kompakten Ausgaben für Modelle getrennt.
Eine beibehaltene Interpreter-Sitzung lässt einen Kandidaten zu, prüft die Kompatibilität und aktiviert ihn zwischen Aufrufen. Polling überwacht deklarierte Project-Eingaben; ungültige Änderungen lassen die aktive Revision nutzbar. Die VS-Code-Steuerung zeigt aktive, ausstehende und ungespeicherte Zustände. Die Journalmigration für Quellcode-Agents ist ein eigener Pfad der vollständigen Toolchain.
Ein Referenzdienst kombiniert geprüfte Entscheidungen zu Sitzungen, Aufgaben und Jobs mit einem Snapshot-Host, explizitem HTTP/TLS und ausgewählter JSON-Event- oder OTLP-Telemetrie. Der abgenommene Linux/Podman-Ablauf bleibt begrenzt; SQL-Adapter werden abgelehnt. Bei wirtschaftlich handelnden Agents bleiben Wallet, Freigabe, Signierung und Abgleich unter Kontrolle des Hosts.
Für Project-Profile mit eigenen Daten und einen privaten, vom Compiler verwalteten generischen Wasm-Endpunkt liegen Nachweise generierter Consumer vor. Öffentliche Unterstützung für Generics bleibt nicht unterstützt und unveröffentlicht. Lokal signierte Registry-Metadaten, gehaltene Generationen und an Locks gebundene Lesezugriffe stellen für sich weder eine gehostete Paketregistry noch eine Berechtigung zum Netzwerkladen bereit.
Der Lean-Job für den exakten Release-Tag prüft seinen begrenzten formalen Kern und den Export von Beweispflichten. Release-Jobs attestieren separat die drei Archive und signieren und prüfen die gemeinsame Herkunftsdokumentation. Das sind getrennte Nachweisketten; keine davon belegt vollständige Sprachkorrektheit, Notarisierung oder über Hosts hinweg reproduzierbare Builds.
module examples.meaning;
@id("math.add")
fn add(left: i64, right: i64) -> i64
requires left >= 0
requires right >= 0
ensures result == left + right
{
left + right
}
@id("app.main")
fn main() -> i64
ensures result == 42
{
add(19, 23)
}Geprüft anhand des Tags v0.8.0 und seines festgehaltenen Quellcommits. Versionierte Spezifikationen definieren Zulassung und Befugnisse; ältere Release-Überschriften in Matrix und Roadmap sind historisch. GitHub-Repository.
Das Online-Handbuch ist die englische Anleitung aus main und kann Änderungen nach 0.8.0 behandeln. Nutze den fixierten Snapshot, um diese Veröffentlichung nachzuvollziehen.
Der aktuelle englische Lernpfad, veröffentlicht aus main.
Die Handbuchdateien am exakt geprüften Release-Commit.
Aktuelle englische Anleitung zu Rechner-Manifest, Prüfungen, Tests und Builds.
Aktuelle englische Einführung in Werte, Funktionen und Quellcodestruktur.
Aktuelle englische Anleitung zu semantischem Kontext und sicheren Änderungsabläufen.
Fixierte Befehlsformen und die Abgrenzung zwischen eigenständiger CLI und vollständiger Toolchain.
Fixierte Einrichtung, semantische Navigation, Review und Entwicklungssteuerung.
Fixierte Beispiele für Sprache, Projekte, Regeln, Agents und Host-Integrationen.
Geprüft anhand des Tags v0.8.0 und seines festgehaltenen Quellcommits. Versionierte Spezifikationen definieren Zulassung und Befugnisse; ältere Release-Überschriften in Matrix und Roadmap sind historisch.
Der Compiler leitet den Kerngraphen aus geprüftem Quellcode ab, mit stabilen Deklarationen, Typen, Verträgen und Beziehungen. Die Entwicklungswerkzeuge können zusätzlich Graft oder Graphify zur Repository-Navigation nutzen. Diese externen Indizes ergänzen die semantischen Fakten des Compilers und ersetzen weder dessen Revisions- noch dessen Validierungsregeln.
Die Toolchain bietet konkrete, an Revisionen gebundene Änderungsoperationen, Kandidatenprüfung und Replay-Prüfungen. Geschützte Regelinventare halten Anforderungen von bearbeitbaren Implementierungskörpern getrennt. Ein Agent muss eine zugelassene Operation und einen autorisierten Anwendungspfad nutzen. Eine Kontextabfrage oder ein erfolgreicher Beweis erlaubt nicht das Überschreiben beliebiger Dateien.