Stabile semantische Identität
Verfasste @id-Werte und Compiler-Identitäten bleiben über Quelltext, HIR, Graph, Diagnosen und generierte Symbole hinweg erhalten. NUL-Zeichen werden vor der Ausgabe abgewiesen.
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 036cc69
authority github.com/wavect/semaprax| Repository-Snapshot | 036cc69 · 2026-09-02. Die Dokumentation bestand, der aktuelle CI-Lauf wurde jedoch abgebrochen. Der separate v0.2.0-Release-Tag bestand alle 45 Jobs. |
|---|---|
| Status des Gesamtprodukts | 49 Teilweise · 0 Implementiert · 0 Fehlend |
| Graph- und Projektvertrag | Graph ≤ v24 · Project v1 Baseline · Project v8, v9, v10 Entwicklervorschau |
| Promotions-Baseline | 5f6fb965 · Das v0.2.0-Prerelease wurde veröffentlicht, nachdem alle 45 Jobs des exakten Tag-Laufs bestanden hatten. |
| Entwicklervorschau im Quellcode | Project v8-v10 sowie Paket-, Borrowing-, Transport- und Revision-Store-Pfade erhielten exakte gehostete Regressionsevidenz. Generierte Pakete bleiben unveröffentlicht und die Profile unpromotet. |
Semaprax überführt menschenlesbaren Quelltext in validiertes HIR und einen funktionsabhängig ausgewählten semantischen Graphen. Graph v22 ergänzt Fakten für besessene Records und Varianten, v23 den Shared Loan Plan und v24 Borrowing für projizierte besessene Byte-Felder. Project v1 bleibt die promotete Baseline. Project v8-v10 und ihre Paketpfade sind Entwicklervorschauen, keine unterstützten öffentlichen APIs.
Verfasste @id-Werte und Compiler-Identitäten bleiben über Quelltext, HIR, Graph, Diagnosen und generierte Symbole hinweg erhalten. NUL-Zeichen werden vor der Ausgabe abgewiesen.
Agent Context v1 und v2 liefern abhängigkeitsspezifische Graphausschnitte mit expliziten Grenzen für Knoten, Bytes, Tiefe und Traversierung.
Patch-Operationen adressieren semantische Identitäten und eine exakte Graphrevision. Veraltete Revisionen werden konsequent abgelehnt; die aktuell verfügbaren Operationen bleiben bewusst begrenzt.
Die Prüfpfade für Review, Impact, Targets und Workspaces erzeugen deterministische Artefakte und benennen ausdrücklich, was sie nicht belegen. Workspace Operations v1 erlaubt ausschließlich klar begrenzte Umbenennungen von Deklarationen und Import-Aliassen. Vor der Veröffentlichung muss die Evidenz erneut erzeugt werden.
CleanupPlan und Shared Loan Plan trennen Ownership- und Borrowing-Fakten vom Lowering. Graph v24 ergänzt projizierte Byte-Feld-Borrows. Das ist kein vollständiger, Rust-kompatibler Borrow Checker.
Workspace Operations v1 bleibt ein enger Rename-Vertrag neben separaten Change-, Replacement-, Struktur- und Veröffentlichungsebenen. Project v8-v10, Agent Transport v5, Revision Store v1, Paketberichte, Offline Locks und Kompatibilitätsevidenz bleiben unpromotet.
module examples.meaning;
@id("math.add")
fn add(left: i64, right: i64) -> i64
requires left >= 0
ensures result == left + right
{
left + right
}Die GitHub-Spezifikationen sind die normative Quelle. Diese Seite ist eine datierte Forschungszusammenfassung. GitHub-Repository.
Nein. Er ist die typisierte, versionierte Programmrepräsentation des Compilers, nicht eine Sammlung generischer Dokumente oder Embeddings.
Noch nicht. Patches für einzelne Dateien bleiben klar begrenzt. Workspace Operations v1 ergänzt lediglich durch Evidenz abgesicherte Umbenennungen von Deklarationen und Import-Aliassen in vorhandenen, verwalteten Pfaden. Das Verfahren bietet weder einen allgemeinen Zugriff auf den Quellbaum noch Git-weite Atomizität.