zqel Development History¶
This document is for contributors and developers. It maps internal development-track identifiers to the features they produced. User-facing documentation uses the public feature names listed in the right column — never the track IDs.
Track identifier → public feature name¶
| Track ID | Public feature name | Status |
|---|---|---|
| T1 | Integer and bitstring type system | Frozen |
| T2 | Numerical assurance chain (MATHREAL = ℝ, Float64 representation, Gappa roundoff, Engineering Error Report) | Frozen |
| T2.2 | Float64 representation assurance | Frozen |
| T2.4 | Per-step roundoff bound (Gappa) | Frozen |
| T2.5 | Lipschitz bound and trajectory bound | Frozen |
| T2.6 | Physical input bound and step error budget | Frozen |
| T2.7/T2.8 | Roundoff-minimisation rewrite (experimental) | Frozen |
| T2.9 | Temporal discretisation and jitter analysis | Frozen |
| T2.10 | Engineering Error Report | Frozen |
| T2.11 | External Real Contract and External Implementation Warrant | Frozen |
| T3 | PARAMETER block | Frozen |
| T3b | PARAMETER block (refinement) | Frozen |
| T4 | SSFC v1 (initial implementation) | Frozen |
| T4.0 | SSFC semantic freeze | Frozen |
| T4.5 | SSFC structural claims (C-SAF, C-INT, C-DEAD, C-GUARD-SAT, C-DET, C-DATA-DEAD, C-REACH, C-HOME) | Frozen |
| T5 | Parallel regions (PARALLEL / REGION / JOIN) | Frozen |
| T6 | SSFC composition (VAR instance + WIRING block) | Frozen |
| T7 | SSFC advanced assurance (C-NO-STUCK-MARKING, C-REVERSI, C-INV, C-WITHIN, C-ASSUME, C-LIVE, C-NO-STUCK-Z3, Engineering Assurance Report) | Frozen |
| T7.2 | C-REVERSI — reversibility to initial marking | Frozen |
| T7.6 | C-LIVE — structural liveness (LIVENESS declaration) | Frozen |
| T7.7 | Engineering Assurance Report (Markdown) | Frozen |
| T7.8 | SSFC Assurance Policy Gate ([ssfc_assurance] TOML section) |
Frozen |
| T8 | (not used publicly) | — |
| CU | Component Unification — equal-rank FB/SSFC composition | Frozen |
| CU-H | Component Unification hardening (CLI --project for SSFC) |
Frozen |
| A1 | Write Ownership analysis (analyze_ownership, OwnershipReport) |
Frozen |
| A2 | Recovery and Progress analysis (analyze_recovery, RecoveryClaim) |
Frozen |
| A2-H | Recovery and Progress analysis soundness hardening | Frozen |
| AP-H | Assurance Policy hardening (CLI) | Frozen |
| D1–D6 | Documentation suite v1 (2026-08-14) | Frozen |
| D7 | Documentation integration: CU/A1/A2 across all four Diátaxis quadrants (2026-08-17) | Frozen |
| G1 | Acceptance test suite v1 | Frozen |
| G2 | Semantic implementation resolution | Frozen |
| P2 | SSFC validation pass | Frozen |
| P05 | RULE / ConstructiveEvidence decision | Frozen |
| LAC | Language Architecture Challenge — POU kind vs. behavior model (2026-08-18) | Frozen |
Design documents¶
| File | Covers |
|---|---|
docs/adr-lac-pou-behavior-model.md |
LAC: four normative decisions before PROGRAM |
docs/adr-extern-authoring-workflow.md |
EXTERN authoring workflow |
docs/adr-numerical-semantics.md |
Numerical semantics ADR |
docs/adr-registry-domain-model.md |
Registry domain model |
docs/t4.0-ssfc-semantics-freeze.md |
T4.0 normative SSFC semantics |
docs/g1-acceptance-2026-07-22.md |
G1 acceptance record |
docs/g2-*.md |
G2 planning and contract matrix |
User-facing documentation in docs/reference/, docs/how-to/, docs/concepts/,
and docs/tutorial/ must not contain the track IDs from the table
above. Use the public feature names instead. The CI gate in
tests/test_docs_hygiene.py enforces this.
Nachtrag Konsolidierung 2026-09-02 — fehlende Frozen-/Abschluss-Tracks¶
| Track | Status | Anker |
|---|---|---|
| GS (General Bounded Synthesis, GS-0…GS-4/R5) | abgeschlossen 2026-08-24 | zqel/synthesis/, 15 LM-FBs |
| PG (PROGRAM-Root, PG-11/PG-12, TC-1/2) | abgeschlossen 2026-08-19 | WIRING kanonisch, Pasteurizer |
| NRA (Native Runtime Architecture, Schritte 1–5) | FROZEN 2026-08-18 (Tag nra) |
offener Rest: Schritt 6 LionsOS (Issue #57) |
| VSC-1 (Engineering Frontend a–c) | abgeschlossen 2026-08-20 | Folge-Track: Issue #56 |
| SNC-1…SNC-5 | ACCEPTED+FROZEN, integriert 2026-08-27 | main 96ec167f |
| CRS (Ladder v2, One-Hash-Pin, Cache v2) | Pins @ ab20d5c1/91b3e431 |
— |
| PI-1/PI-2 (Prozessisolation + supervidierte CI) | abgenommen & gemergt 2026-09-02 | main e121bafd, ADR adr-process-isolation.md |
| NS-1 v3 (typisierte Relationalklauseln) | implementiert (PR #43); Integration ausstehend | ADR adr-necessary-sufficient-clauses.md |
Nachtrag 2026-09-06 — zwei Tracks, die beide Nachträge übersprungen hatten¶
Gefunden beim Abgleich der Sitzungs-Memory gegen dieses Dokument: zwei
abgeschlossene Tracks standen in keiner der beiden Tabellen, obwohl beide
eingefroren und in main sind.
| Track | Status | Anker |
|---|---|---|
| T2.3a–e (kompositionale Assurance: Vertragsbereiche, DualExpr, Ausdrucksschranke, LM-Ende-zu-Ende, WIRING) | APPROVED/FROZEN 2026-08-25 | Tags t23d @ bd2a9d20, t23e @ 791c8479; LM-Kette ε ≈ 1,02e-12 |
| AP-31 (EXTERN: Operation per Vertrag deklariert, Registry-Artefakt entlädt die Zusage) | abgeschlossen | zqel/registry.py, examples/extern/, ADR adr-extern-authoring-workflow.md |
Eine Übersicht, die sich „verbindlich" nennt, muss vollständig sein — sonst verschiebt sie die Frage nur, und die Antwort liegt wieder verstreut.
Nachtrag 2026-09-07 — Endlichkeit unter Float64, und was ein reproduzierbarer Beweis kostet¶
Ein Track, der beim Schreiben dreimal die Richtung wechselte, weil jede Stufe einen Fehler in der vorigen sichtbar machte. Er gehört hierher, weil sein Ergebnis eine Sprachaussage ist und nicht nur eine Implementierung.
| Track | Status | Anker |
|---|---|---|
| #162 (Float64-Endlichkeitspflicht: Oberfläche + Aktivierung) | abgeschlossen | zqel/float64_range.py, docs/float64-corpus.json |
| #172 (kompositionelle Abstraktion statt Entfaltung) | abgeschlossen | zqel/range_tower.py, zqel/range_envelope.py |
| #183 (Reproduzierbarkeit der Bereichssuche) | abgeschlossen | tests/test_the_range_search_is_deterministic.py |
Was die Sprache jetzt sagt. Unter einer Float64-Repräsentationsgrenze ist
Endlichkeit eine Pflicht, keine Annahme. Drei Klauseln geben drei Antworten
darauf, wer die Schranke schuldet: REQUIRE (der Aufrufer, und er darf sie
einlösen oder weitertragen), ASSUME (die Umgebung, sichtbar an der Wurzel),
keine Klausel (die Operation muss über den ganzen Profilbereich halten, sonst
Verweigerung). Ein Urteil hat vier Zustände, und CONDITIONAL — entlastet, aber
unter erklärten, von nichts durchgesetzten Auflagen — ist der häufigste.
Was der Beweis dafür kostete. Die Entfaltung der geplätteten Formel war für
LMFit in 2400 s unentscheidbar; die Komposition entscheidet sie in 2,5 s. Der
Weg dahin brauchte mehrere Korrekturen im eigenen Code — eine Speicheradresse in
einem Z3-Symbolnamen, eine Rückkopplung der Hüllen in die Prämissen, eine Leiter
ohne Vorzeichen — und zwei im Messwerkzeug, das die ersten finden sollte. Am Ende
wurde die Suche ganz ersetzt: das Zielintervall wählt jetzt der Quelltext
(zqel/static_interval.py), der Solver validiert nur noch. Damit kann
Solverstreuung einen Lauf nur zwischen grün und rot bewegen, nie zwischen zwei
verschiedenen gültigen Warrants.
Der Korpus zeigt dabei null Klassenwechsel. Das belegt, dass die beobachtete
Klassifikation erhalten bleibt — nicht, dass die neue Strategie mathematisch
nicht schwächer wäre. Ausführlich in
docs/notes/2026-09-07-reproducible-range-search.md.
Nachtrag 2026-09-07 — was die Prüfwerkzeuge über ein ℝ-Programm wirklich bewiesen¶
| Track | Stand | Beleg |
|---|---|---|
| #165 (64 abgeschaltete ℝ-Tests) | abgeschlossen | docs/notes/2026-09-07-was-kani-und-cbmc-ueber-ein-real-programm-beweisen.md |
| #184 (Komposition erreicht keine Artefaktprüfung) | offen, herausgelöst | tests/test_a_composed_block_never_reached_an_artifact_check.py |
| #186 (Pilot-Gate und Grenze schließen sich aus) | offen, herausgelöst | tests/test_foundation_c.py |
Was gefragt war. Nicht „welcher Claim gilt", sondern: was beweisen Kani und CBMC über ein Float64-Programm? Die Antwort setzte voraus, dass die Werkzeuge sagen, was sie geprüft haben — und fünf der acht Befunde saßen im Prüfwerkzeug selbst.
Der schwerste. Kanis Urteil über den Lauf war unser Urteil über die
Invarianten. Ein unbedingtes panic! an den Anfang des emittierten cycle
injiziert: Kani meldet VERIFICATION:- FAILED, und verify_program gab dafür
ok=True zurück, weil die Description den Text INVARIANT nicht trug. Beide
Ergebnistypen trennen jetzt Werkzeugurteil und Klauselurteil, fail-closed, mit
einer Vakuitätswache: eine Klausel, für die kein Status gemeldet wurde, ist nicht
bewiesen. Auf der C-Seite war der blinde Fleck vermessen — ein Lauf meldet 75
Prüfungen, drei davon unsere.
Die Naht, an der fast alles saß. Der Harness lief unter echt schwächeren Prämissen als das Modell: MATHREAL-Eingänge waren beliebige f64, NaN eingeschlossen, und Kani widerlegte damit einen Block, den das Modell beweist. Das Modell nennt seine Prämisse selbst — jeder MATHREAL-Eingang ist ein endlicher binary64, die Endlichkeit der Register wird induktiv bewiesen, nicht angenommen. Genau das injiziert der Harness jetzt und schreibt es ins Ergebnis. Dieselbe Klasse: eine erfundene Uhr, die jeden Beweis auf 16,7 Minuten Laufzeit beschränkte, und ein dt-Fenster in Millisekunden auf einem Feld, das Sekunden zählt.
Was nicht behauptet wird. Keine Komposition. Von den zwölf Programmen der
Fallliste erklärt keines einen WIRING-Block, und die Zelle steht ausdrücklich
als unmeasured in der Tabelle statt zu fehlen.