Zuerst stabile Identität. Dann Quelltextänderungen.
Der semantische Programmgraph von Semaprax erfasst typisierte Deklarationen, Effekte, Verträge, Ownership-Fakten, Aufrufbeziehungen und Lowering-Identitäten unter einer inhaltsabgeleiteten Revision.
entity Semaprax
status Pre-Alpha-Forschung
snapshot b9f593c
authority github.com/wavect/semaprax| Repository-Snapshot | b9f593c · 2026-09-16. Der geprüfte main-Commit entspricht dem Tag v0.5.0. Dessen exakte Tag-CI war erfolgreich; die separate Branch-CI wurde abgebrochen. Daraus folgt keine allgemeine Produktions- oder Sicherheitsgarantie. |
|---|---|
| Status des Gesamtprodukts | 55 Teilweise · 0 Implementiert · 0 Fehlend |
| Graph- und Projektvertrag | Funktionsabhängige Graphschemas erhalten frühere Verträge. Project v1 ist die Baseline; die Owned-Data-Profile v8, v9, v10 und v11 haben eigene Zulassungs- und Supportgrenzen. |
| Veröffentlichtes Prerelease | v0.5.0 · Veröffentlicht am 16. September 2026 um 09:43 UTC. Drei Archive: Linux x86-64, macOS Apple Silicon und Windows x86-64, mit SHA256SUMS. Das enthaltene semaprax ist die vollständige Toolchain, nicht die eigenständige Cargo-CLI. Exakte Tag-CI. |
| Paket- und API-Vorschau | Eine veröffentlichte Toolchain veröffentlicht weder ihre generierten Rust/npm-Pakete noch private APIs. Supportentscheidungen für Project v8-v11, öffentliche generische Ownership, weitere Plattformen und native/Wasm-Ausführung von Agent-Stufen bleiben separat. |
Semaprax überführt maßgeblichen .spx-Quelltext in geprüftes HIR, eine Compiler-Darstellung typisierter Programmbedeutung. Stabile Identitäten verbinden Graphabfragen, Änderungskandidaten, Ausführung und Evidenz. Unterstützte Änderungen müssen zur Quellrevision passen; Laufzeit-Agentenvorschläge durchlaufen typisierte Dekodierung und deterministische Autorisierung. Graphen und Belege erteilen selbst keine Veröffentlichungs-, Netzwerk- oder Zahlungsbefugnis.
Lesbarer .spx-Quelltext bleibt die maßgebliche Darstellung in Git. Explizite @id-Werte identifizieren Deklarationen unabhängig von unterstützten Namensänderungen. Die Revision bindet kanonischen Quelltext und das implizite Compiler-Prelude, nicht zufällige Quellpositionen oder ein Graph-Drahtformat.
Context v1/v2 begrenzt Tiefe, Knoten und Bytes; v2 ergänzt gerichtete Traversierung. Aufgabenbezogener Kontext sowie Text-, Binär- und Model-Text-Projektionen ermöglichen gezielten Austausch mit Replay-Prüfungen. Weniger serialisierte Bytes bedeuten nicht automatisch weniger abgerechnete Tokens oder bessere Antworten.
Kontext prüfen, Kandidat ableiten, Auswirkungen ansehen, reviewen, Prüfungen reproduzieren und erst dann explizit anwenden. Neben Umbenennungen gibt es begrenzten Ausdrucksersatz, Strukturänderungen und definierte Rebase/Merge-Komposition. Jedes Protokoll behält eigene Revisions-, Identitäts- und Operationsgrenzen.
Verwaltete Workspace-Generationen, Kandidatenevidenz, Project-Revisionsspeicher und MCP-Workflows behalten explizite Schreib- und Veröffentlichungsbefugnisse. Multi-File-Validierung aktualisiert nicht beliebige Pfade, Git oder Editoren atomar. Die Rust-Embedding-API bietet begrenzte Eingaben, Abbruch und gekapselte Sitzungen, keinen freien Host-Zugriff.
Zugelassene Profile umfassen Records, Varianten, Klassen, Vererbung, Generics, Option/Result, explizite Mutation, Schleifen, Collections, Iteratoren, Funktionswerte und begrenzte Closures. Text, Bytes und die mitgelieferte Bibliothek ermöglichen nützliche Programme. Besitzende Closure-Captures, allgemeine Generic-Constraints und beliebige Kombinationen bleiben begrenzt.
Besessene und geliehene Werte, Cleanup-Pläne, Loan-Fakten und ausgewählte Resource/Generic-Kompositionen sind implementiert. v0.5.0 ergänzt direkte besessene String-Varianteninhalte; generische String-Substitutionen und verschachtelte besessene Records als Varianteninhalt bleiben eingeschränkt. Das ist kein vollständiges Lifetime-System und keine Rust-Kompatibilität.
Initialisieren, beobachten, vorschlagen, dekodieren, autorisieren, ausführen und Zustand reduzieren. Der geprüfte Reducer wählt Continue, Complete, Suspend oder Fail; Autorisierung erfolgt in jeder Runde erneut. Kompilierte Proposal-Schemas begrenzen Streaming und Dekodierung vor Effekten. Quellcode-Agentenstufen laufen im beibehaltenen Interpreter, nicht gleichwertig nativ/Wasm.
Explizite Host-Adapter liefern Zugangsdaten, Transport und Speicher. Grenzen können Aufrufe, Tokens, Bytes, Fristen und Kostenangebote umfassen. Dauerhafte Profile bestätigen Absichten vor Versand und wiederholen unklare Vorgänge nicht. Generische Host-Profile unterstützen begrenzten Retry/Failover; die gebundene Source-Model-Route wechselt Anbieter nicht automatisch und wiederholt nicht automatisch. Beobachteter Verbrauch garantiert keine Rechnung.
Geprüfte HTTPS-POST-Aufrufe, Rust-Host-Authentifizierung/Sitzungen und Jobs mit Checkpoints sind einzelne Integrationsprofile, kein vollständiges Web-Framework. Economic Agents untersuchen Zahlungsabsichten, Simulation, Freigabe und Abgleich mit Wallets/Signierung des Hosts. Modellvorschläge sind weder Zahlungsbefugnis noch Garantie einer genau einmaligen Abwicklung.
Project v8 überträgt Bytes und ausgewählte Option/Result-Formen; v9 ergänzt flache besessene Records, v10 besessenes UTF-8 und v11 verschachtelte besessene Records. Generierte Native/Rust- und npm/Wasm-Consumer, private Transports und öffentliche Generic-Metadaten haben eigene Verträge. Toolchain-Release, Paketveröffentlichung und öffentlicher Support sind verschiedene Entscheidungen.
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 festgehaltenen Commits und des Release-Eintrags v0.5.0. Versionierte Spezifikationen definieren Zulassung und Befugnisse. Ältere v0.4-Release-Überschriften in Matrix und Roadmap sind historisch, nicht die aktuelle Release-Identität. GitHub-Repository.
Geprüft anhand des festgehaltenen Commits und des Release-Eintrags v0.5.0. Versionierte Spezifikationen definieren Zulassung und Befugnisse. Ältere v0.4-Release-Überschriften in Matrix und Roadmap sind historisch, nicht die aktuelle Release-Identität.
Nein. Es ist eine vom Compiler abgeleitete typisierte Programmdarstellung, kein allgemeiner Dokumentenindex oder eine Embedding-Datenbank. Kanonische Quelle und Compiler-Prelude binden Revisionen; validierte HIR liefert semantische Identitäten und Fakten.
Nicht beliebig. v0.5.0 enthält mehrere begrenzte Änderungsfamilien einschließlich spezifiziertem Ausdrucksersatz, strukturellen Änderungen und Komposition. Jede hat eigene Revisions- und Zulassungsprüfungen; Evidenz und lesende Inspektion verleihen keine beliebigen Dateisystem-, Git- oder Veröffentlichungsrechte.