Zuerst stabile Identität. Dann Quelltextänderungen.
Stabile Identitäten verbinden geprüften Quellcode, semantische Abfragen, Beweispflichten und Änderungen. In v0.9.0 verbindet ein gemeinsamer Entscheidungskern auch die Modellwahl in Entwicklung und Laufzeit; Deployment-Befugnisse bleiben beim Host. Native Kommando-, Daten- und Ownership-Erweiterungen bleiben explizit gewählte Profile.
entity Semaprax
status beta
snapshot 933196b
authority github.com/wavect/semapraxSemaprax 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.
Wähle eine Stufe, um ihre Teile der Architektur unten hervorzuheben.
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 prüft einen begrenzten formalen Kern und Obligationsexport. Release-Jobs attestieren fünf Archive, prüfen den signierten Gesamtsatz und durchlaufen vor Veröffentlichung native Installationsabläufe. Daraus folgt kein Beweis vollständiger Sprachkorrektheit, Notarisierung oder hostübergreifender Reproduzierbarkeit.
Vor einem Router prüfen feste Regeln Vertraulichkeit, Werkzeuge, Modalitäten, Kontext und Budget. Entwicklungsphasen und Laufzeit-Deployments teilen Code, aber keine Qualifikationsnachweise. Regelrouting ruft kein Router-Modell auf; der datierte Supportstand bestätigt keinen live getesteten oder qualifizierten lernenden Adapter.
Nur eine bestätigte abgeschlossene Runde öffnet eine neue Route. Übergaben enthalten höchstens 16 KiB Zustand, Ausgabedigests und Ergebnisreferenzen, kein Transkript. Delegation reserviert Elternbudget und übernimmt die Frist. Werkzeug- und Spezialistenwahl wird anhand aktueller Grants und Schemas erneut autorisiert; Ungewissheit stoppt zur Klärung.
Project-v26/v28-Kommandos sind rein nativ. v28 erlaubt 1 MiB je String und 1 MiB gemeinsame gepufferte Ausgabe mit begrenztem Append; Dateilese- und Befugnisgrenzen bleiben erhalten. std.data.json.scan prüft vollständiges UTF-8-JSON mit expliziter Duplikatregel; std.pattern ist ein begrenzter ASCII-Byte-Matcher. Andere Interpreter-, Wasm- oder öffentliche API-Profile werden dadurch nicht erweitert.
Installierte Diagnosethemen nennen genaue Imports, Effekte, Ownership-Reparaturen und zugelassene Syntax. Manifestformatierung hat einen expliziten Modus fmt –manifest. Optimierungen im Tag erhalten Identitäten, HIR-Replay, Loan-Abrechnung und Ressourcenlimits; einzelne Belege und offene Gates bleiben sichtbar, ohne gemessene Projektbeschleunigung zu behaupten.
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)
}| Repository-Snapshot | 933196b · 2026-10-15. Das Tag v0.9.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.9.0 · Veröffentlicht am 11. Oktober 2026 um 15:07 UTC. Alle 91 Jobs des Veröffentlichungslaufs für den exakten Tag waren erfolgreich. Fünf Toolchain-Archive und zwei Installer enthalten SHA256SUMS, fünf Archiv-Attestierungen und unabhängig geprüfte signierte Gesamtnachweise. Native Installationsabläufe sind Veröffentlichungsgates. Keine Notarisierung oder Zusage reproduzierbarer Builds; 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. |
Am 15. Oktober 2026 anhand von v0.9.0, veröffentlichten Dateien und Release-Lauf geprüft. Installationshandbuch und Kanalregister im Tag zeigen noch Beispiele für v0.8.0; nutze die hier festgehaltenen v0.9.0-Downloads. Ältere Matrix- und Roadmap-Überschriften sind historisch. Das Live-Handbuch folgt main und kann neuere Arbeit beschreiben. GitHub-Repository.
Das Online-Handbuch ist die englische Anleitung aus main und kann Änderungen nach 0.9.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.
Am 15. Oktober 2026 anhand von v0.9.0, veröffentlichten Dateien und Release-Lauf geprüft. Installationshandbuch und Kanalregister im Tag zeigen noch Beispiele für v0.8.0; nutze die hier festgehaltenen v0.9.0-Downloads. Ältere Matrix- und Roadmap-Überschriften sind historisch. Das Live-Handbuch folgt main und kann neuere Arbeit beschreiben.
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.