JDL — Compile-Zeit-Code und die Meta-Phase

Status: Konsolidierungsentwurf, Arbeitsstand Version: 0.3.1 Datum: 2026-10-02 Vorfassung: 0.3.0 vom 2026-09-29 Ersetzt: jdl-typefn-spec.md — nicht als Fortschreibung, sondern als Rettung Geltungsbereich: was Code darf, der während der Übersetzung läuft — Beschränkungen, Auswertungsfenster, Totalitätsnachweis, semantische Proof-Grundbegriffe, Importregeln, Ring-Schichtung des Meta-Records, Konsum von Meta-Einträgen Quellen: jdl-typefn-spec §2, §3.1, §6, §7, §8, §9, jdl-sprachreferenz v0.1.0 §15, jade-service-typekind-arbeitsnotiz §8, jade-compiler-db-spec §8, §9, jdl-engine-descriptor-model §3.2, 00-refinements, 01-refinements-meta-tags, jdl-blueprint-spec 0.5.2 §4.9, §6.1, §8.1 und BP-20, wie-jade-uebersetzt §3.7, §4.5, §6.1, §6.2, wie-jade-ausfuehrt §10, Entscheidungen aus den Arbeitsgesprächen (Stand 2026-10-02)

---

0. Über dieses Dokument

0.1 Warum es existiert

jdl-typefn-spec beschrieb typefn als eigene Deklarationsform. Diese Entscheidung ist zurückgenommen: Compile-Zeit-Auswertung ist eine gewöhnliche Funktion in einer anderen Phase, das Schlüsselwort entfällt [N] jdl-sprachreferenz §15.1.

Damit fällt das Thema jenes Dokuments weg, nicht aber sein Inhalt. Die Sprachreferenz hält in §15.2 ausdrücklich fest, dass die Beschränkungen aus jdl-typefn-spec §2.1 und §2.2 der Sache nach weitergelten und beim Umschreiben zu übernehmen sind. Genau das leistet dieses Dokument.

0.2 Kennzeichnung

Marke	Bedeutung
[N]	bestehend normativ belegt, Fundstelle genannt
[A]	aus bestehendem Material ableitbar, aber nirgends ausgeschrieben
[D]	Entscheidung der Fassung 0.2
[E]	entschieden in den Arbeitsgesprächen, noch in keinem Quelldokument ausgeschrieben
[V]	Vorschlag, ausgearbeitet, aber nicht entschieden
[O]	offen

Die ursprüngliche 0.1-Fassung traf keine neuen Entscheidungen. Version 0.2 schließt gezielt den offenen Eigentümer des Totalitätsnachweises und präzisiert die Grenze zwischen globalem Meta-Fixpoint, lokaler endlicher Analyse und CompilerDB-Query-Zyklen. Diese Festlegungen sind mit [D] markiert.

Version 0.3 gleicht das Dokument an Entscheidungen an, die seitdem gefallen sind ([E]), und schlägt für den Widerspruch „Teilsprache oder nicht“ eine Lösung vor ([V]). Wo ein [E] einer [N]-Quelle widerspricht, gilt das [E]; die Quelle ist dann in diesem Punkt veraltet.

0.3 Begriffe

Die Literatur und die Vorgängerdokumente nennen diese Funktionen TypeFn — als Suchwort brauchbar, als Erklärung nicht. Hier heißen sie Compile-Zeit-Funktionen: Funktionen, deren Rumpf während der Übersetzung ausgeführt wird und die zur Laufzeit nicht mehr existieren.

Die Meta-Phase ist die Phase, in der das geschieht. Der Gegensatz ist die Runtime-Phase, in der gewöhnlicher Code läuft.

0.4 Syntax

Die Phase steht am Pfeil vor der Row: ->Meta{...} [E] (§2.1). Alle übrigen Formen in den Beispielen sind nicht normiert und tragen // spekulativ. Auf spekulative Formen wird nichts gestützt.

---

1. Zweck und Geltungsbereich

1.1 Was dieses Dokument festlegt

Die Beschränkungen für Compile-Zeit-Code, das Zeitfenster seiner Auswertung, den Eigentümer und die Reichweite des Totalitätsnachweises, was er importieren darf, wie der Meta-Record nach Ringen geschichtet ist, wie ein Beweis abgeschwächt werden kann und wer einen fertigen Meta-Eintrag liest.

1.2 Was es nicht behandelt

Die db-Fassade. Steht vollständig und neuer in jade-compiler-db-spec §9. Die Fassung in jdl-typefn-spec §5 war ein älteres Duplikat und wird nicht übernommen. Eine Arbeitsrichtung, Fragen als Daten zu stellen — Query-Records mit Buildern —, beschreibt wie-jade-uebersetzt §3.7.

Den Auswertungskontext. MetaContext und ApplyRefinement stehen in jade-compiler-db-spec §8.5 und jdl-engine-descriptor-model §3.2.

Die Refinement-Mechanik. :>, Meta-Records, Präfix- und Suffixform, Merge-Regeln: 00-refinements und 01-refinements-meta-tags.

Die Phase als Teil des Funktionstyps im Detail. Die Schreibweise ist entschieden (§2.1); wie sich die Phase formal zur Effect Row verhält, ist Gegenstand von jade-service-typekind-arbeitsnotiz §8.

---

2. Die Phase

2.1 Zwei Phasen, mehr nicht [A] jade-service-typekind-arbeitsnotiz §8.4

Die Phasenachse beantwortet genau eine Frage: Läuft der Rumpf dieser Funktion während der Übersetzung oder während der Ausführung?

Darauf gibt es zwei Antworten, und eine dritte gehörte zu einer anderen Frage. Das ist die tragende Begründung — nicht Sparsamkeit.

Eine fehlende Phasenangabe bedeutet Runtime, nicht „irgendeine". Das ist dieselbe Konstruktion wie bei der Effect Row, wo eine fehlende Effektmenge die leere Menge bedeutet und nicht eine unbestimmte (Regel R-3).

In fast allem Code ist die Phase damit unsichtbar. Markiert wird nur Meta.

Die Schreibweise [E]: Die Phase steht am Pfeil, vor der Row.

// spekulativ, bis auf die Phasenmarkierung
def describe(spec: CodecSpec) ->Meta{CompilerDb, Throw[DiagnosticSet]} PatchSet

• ->Meta{...} heißt: Der Rumpf läuft in der Meta-Phase, und in den geschweiften Klammern steht seine Row.
• CompilerDb steht in der Row, weil describe die CompilerDB befragt (§3.3).
• Ohne Meta am Pfeil ist es eine gewöhnliche Funktion.

Die Phase steht vor der Row und nicht in ihr, weil Meta sich nicht wie ein Row-Element verhält: Es gibt keinen Handler, keine Installation und keine Differenz (jade-service-typekind-arbeitsnotiz §8.3). Damit ist der frühere offene Punkt 1 geschlossen.

[V] Die Parserfrage aus der Arbeitsnotiz — liest ->Meta{...} eindeutig gegen einen Rückgabetyp namens Meta? — lässt sich schließen, indem Meta direkt nach dem Pfeil reserviert ist. Siehe §8, Punkt 10.

2.2 Spurlosigkeit [N] jdl-typefn-spec §2

Compile-Zeit-Code existiert zur Laufzeit nicht. Weder im Bytecode noch in einer VM-Struktur.

Das ist dieselbe Eigenschaft, die Regel L-1 für die Effect Row festhält, und aus demselben Grund: Was nur der Übersetzung dient, hat in der Ausführung nichts verloren.

---

3. Was Compile-Zeit-Code darf

3.1 Was Compile-Zeit-Code garantieren muss

Totalität           Terminiert garantiert. Nachgewiesen durch den
                    Totalitätsbeweis (§4.3, §4.4).                     [N] / [D]
Determinismus       Selbe Eingabe, selbes Ergebnis. Gesichert über
                    die Meta-Row (§3.3).                               [N] / [E]
Spurlosigkeit       Existiert zur Laufzeit nicht (§2.2).               [N]
Kein Laufzeit-      Keine Resources, Handles oder Services der
zugriff             Laufzeit-Domäne.                                   [E]
Keine Rückgabe      Gibt keine Compile-Zeit-Funktion zurück;
einer Compile-      Komposition erfolgt durch Aufruf (MP-4).           [N]
Zeit-Funktion

Der Zweck dieser Liste ist ein einziger: Der Compiler muss fertig werden, und zwar immer mit demselben Ergebnis. Eine Compile-Zeit-Funktion, die nicht terminiert, hängt nicht das Programm auf, sondern die Übersetzung — und zwar ohne Fehlermeldung, weil niemand da ist, der sie schreiben könnte.

Allokation ist erlaubt [E]. Die frühere „Speicheragnostik“ (keine Allokation, keine Handles, keine Arenas) ist überholt. Meta-Werte sind gewöhnliche JME-Objekte (wie-jade-uebersetzt §6.2), Allokation läuft in der Meta-Phase normal, und nur wer vom Standard abweicht, trägt Storage in der Row (jdl-blueprint-spec §6.1). Was von der Speicheragnostik bleibt, ist der eigentliche Kern: kein Zugriff auf Resources und Services der Laufzeit. Damit ist der frühere offene Punkt 2 geschlossen.

3.2 Gewöhnliches JDL statt Verbotsliste [V]

Die Fassungen bis 0.2 sicherten die Terminierung grammatisch: Eine Liste erlaubter und verbotener Konstrukte sorgte dafür, dass sich eine endlose Schleife gar nicht erst hinschreiben ließ. Verboten waren unter anderem while, loop, var und return.

Seit 0.2 gibt es einen semantischen Weg: den Totalitätsbeweis (§4.3, §4.4). Er prüft, ob eine Funktion endet, gleich wie sie geschrieben ist. Die Verbotsliste ist damit überflüssig — und sie widerspricht inzwischen der Praxis: Blueprint-Provider und Beispiele für Meta-Funktionen benutzen ret, var und for (jdl-blueprint-spec §4.9, wie-jade-uebersetzt §3.7).

Vorschlag: Der Rumpf einer Compile-Zeit-Funktion ist gewöhnliches JDL. Die Beschränkungen sind keine Grammatik mehr, sondern zwei Prüfungen:

Terminierung    Der Rumpf ist als total bewiesen (MP-18).
                Was nicht bewiesen ist, wird nicht ausgeführt.

Determinismus   Die Meta-Row enthält keinen Service, der nach außen greift (§3.3).

Die zweite Prüfung ist bereits entschieden (§3.3). Vorgeschlagen ist, die Verbotsliste durch die erste zu ersetzen.

Was das für die früheren Verbote bedeutet:

früher verboten	jetzt
while, loop	zulässig, wenn der Beweis ein nachweislich fallendes Maß findet
var	zulässig; lokaler Zustand gefährdet weder Terminierung noch Determinismus
return	ret zulässig
I/O	ausgeschlossen über die Row (§3.3)
Aufruf von def-Funktionen	geregelt über die Row (§3.4)
Closures als Werte	bleibt vorerst verboten: Beweisregeln für Aufrufe unbekannter Funktionswerte fehlen noch
Rückgabe einer Compile-Zeit-Funktion	bleibt verboten (MP-4)
direktes <{}>	offen (§8, Punkt 4)

Trusted Core: Mit diesem Vorschlag wird der Totalitätsbeweis tragend. Solange Stage 1 ihn über einen Zig-BootstrapProvider liefert (§4.3), muss dieser streng konservativ sein: im Zweifel „nicht bewiesen“. Ein Beweiser, der eine nicht terminierende Funktion durchlässt, hängt die Übersetzung auf.

3.3 Determinismus über die Row [E]

Was Compile-Zeit-Code von außen erreichen darf, steht in seiner Meta-Row. Zulässig sind Einträge, die das Ergebnis nicht von der Build-Umgebung abhängig machen:

zulässig    CompilerDb        Anfragen an die CompilerDB, mit Abhängigkeitskanten
            Throw[...]        Fehlschlag, etwa mit DiagnosticSet
            Storage           nur bei Abweichung vom Standardspeicher

unzulässig  jeder Service, der nach außen greift: Datei, Netz, Uhr, Zufall

Der Grund ist derselbe wie in jdl-blueprint-spec BP-20: Ein Build darf nicht von seiner Build-Umgebung abhängen, sonst gibt es keinen reproduzierbaren Build und keinen inhaltsadressierten Cache.

3.4 Aufruf gewöhnlicher Funktionen [E]

Die frühere Regel „kein Aufruf von def-Funktionen“ stammt aus der Zeit, als Compile-Zeit-Funktionen eine eigene Deklarationsform typefn hatten. Heute ist jede Funktion ein def; die Regel sagt in ihrer alten Form nichts mehr.

Compile-Zeit-Code darf jede Funktion aufrufen, deren Row in seine eigene Meta-Row passt. Das ist derselbe Teilmengentest, der für Rows überall gilt:

aufgerufene Funktion         passt in eine Meta-Row?
->{}                         ja, immer
->{Throw[E]}                 ja, wenn die Meta-Row Throw[E] trägt
->{Net} / ->{Fs}             nein, nie (§3.3)

Das braucht die Architektur: Die Query-Builder aus wie-jade-uebersetzt §3.7 sind Funktionen mit leerer Row, die Meta-Code aufruft. Und eine Hilfsfunktion, etwa für Zeichenketten, muss nicht für jede Phase ein zweites Mal geschrieben werden. Eine Prüfung wie requireAtLeast in jdl-blueprint-spec §4.9 fängt Fehler damit schon beim Übersetzen ab, obwohl sie eine gewöhnliche Funktion ist.

Die Spurlosigkeit bleibt gewahrt: Ein Aufruf aus der Meta-Phase hinterlässt nichts im Artefakt. Existiert die aufgerufene Funktion zur Laufzeit, dann aus eigenem Recht, weil Laufzeitcode sie braucht. Umgekehrt gilt weiterhin: Laufzeitcode kann keine Funktion mit Meta am Pfeil aufrufen.

3.5 „Keine zweite Sprache“ [V]

Die Sprachreferenz §15.1 begründet die Abschaffung von typefn so:

Damit gelten für Compile-Zeit-Funktionen alle Regeln aus §6, §7 und §13 unverändert — Parametergrammatik, Row-Algebra, Constraints. Es gibt keine zweite Sprache im Sprachkörper.

Bis 0.2 widersprach dem die Verbotsliste: var, loop, while, return und Closures waren verboten, obwohl sie in gewöhnlichem JDL zulässig sind. Mit §3.2 bis §3.4 fällt der Widerspruch weg. Compile-Zeit-Code ist gewöhnliches JDL; was ihn unterscheidet, ist ein Beweis (Terminierung) und eine Row (Determinismus) — beides Mechanismen, die es ohnehin gibt.

Einzige verbleibende Ausnahme sind Closures als Werte (§3.2). Sie ist als offener Punkt geführt und nicht als Grammatikregel: Sobald es Beweisregeln für Aufrufe von Funktionswerten gibt, entfällt sie.

Damit liegt für den offenen Punkt 3 ein Vorschlag vor.

---

4. Wann ausgewertet wird

4.1 Das Auswertungsfenster [N] jdl-typefn-spec §3.1

Die Auswertung findet während der Meta- und Typauflösung statt: nachdem TypeSubjects und Namen ausreichend aufgelöst sind, bevor Layout-Finalisierung, IR-Builder und Generator harte Annahmen über Typen, Provides oder Dispatch treffen.

Beide Grenzen sind notwendig. Vor der Namensauflösung wüsste die Funktion nicht, worüber sie redet. Nach der Layout-Finalisierung käme ihr Ergebnis zu spät, um noch etwas zu ändern.

Das Fenster ist damit keine Implementierungsfreiheit, sondern eine Anforderung an die Phasenordnung im Trusted Core.

4.2 Auflösung ohne globalen Fixpoint [D]

Jeder Compile-Zeit-Aufruf muss zu einem konkreten Ergebnis auflösen. Die Meta-Phase wird nicht global oder phasenübergreifend „bis zur Stabilität“ wiederholt. Nach dem jeweiligen Auswertungsfenster enthält die CompilerDB nur vollständig aufgelöste Ergebnisse.

Ein lokaler, intern begrenzter Worklist-/Fixpunktalgorithmus innerhalb einer einzelnen Compile-Zeit-Auswertung ist dagegen zulässig, wenn seine Faktendomäne explizit endlich ist und seine Terminierung nach den Regeln dieses Dokuments nachweisbar bleibt. Eine monotone Label-Closure über eine endliche Labelmenge ist das kanonische Beispiel.

CompilerDB-Query-Zyklen sind davon strikt getrennt. Bei zyklischer Query-Abhängigkeit liefert die CompilerDB ein strukturiertes Diagnostic mit Query-Trace; ein lokaler Proof-Algorithmus darf einen solchen Zyklus nicht als zulässige Rekursion umdeuten.

4.3 Eigentümer des Totalitätsnachweises [D]

Die konkrete Totalitätsprüfung gehört der Meta-Semantik, nicht Ring 0 und nicht dem Plugin-System. Sie ist ein deterministischer CompilerDB-Query-Vertrag. Stage 1 darf ihn durch einen vertrauenswürdigen Zig-BootstrapProvider tragen; Stage 2+ soll denselben Vertrag durch JDL-Semantik erfüllen.

Der konkrete Queryname ist API-Design, keine Sprachsyntax. Konzeptionell:

ProveMetaTotality(MetaSubject) -> TotalityJudgement

Ring 0 stellt Query-Ausführung, Cache, Dependency-Tracking, Cycle Detection und Bootstrap bereit. Die Beweisregeln selbst gehören in JDL.

Der Provider konsumiert semantische Projektionen des Meta-Rumpfes, also gewöhnliche Derived Queries wie Control-Flow-, Call- oder Progress-Views. Semantic Views sind dabei kein eigenes Sprachkonstrukt und keine zweite CompilerDB-Kategorie.

4.4 Konservativer Totalitätsbeweis [D]

Ein fehlender Totalitätsbeweis ist kein Beweis von Nichtterminierung. Allgemeine Terminierung ist für eine hinreichend ausdrucksstarke Sprache nicht vollständig entscheidbar. Jade akzeptiert deshalb nur Formen, für die seine expliziten Regeln einen Nachweis liefern, beispielsweise:

endliche Iteration
strukturelle Rekursion
nachweislich streng fallendes, unten beschränktes Maß
Komposition bereits bewiesener totaler Compile-Zeit-Funktionen

Unbekannte oder zu komplexe Formen bleiben unbewiesen und dürfen dort nicht ausgeführt werden, wo MP-1 Totalität verlangt. TotalityJudgement muss nicht das Drei-Zustands-Modell der Label-Semantik übernehmen.

4.5 Facts, Obligations und Proofs [D]

Für Meta-Proofs gelten drei allgemeine Begriffe:

Fact        bereits bekannte semantische Aussage
Obligation  von einer Proof-Regel zusätzlich geforderte Aussage
Proof       nachvollziehbare Ableitung aus Facts und erfüllten Obligations

Das konkrete Judgement bleibt fachdomänenspezifisch. Provenance wird getrennt gehalten und kann Diagnostics beziehungsweise :why speisen. Fehlender Beweis ist kein Gegenbeweis.

4.6 Bootstrap ohne Selbstbeweis [D]

Der erste Stage-2-Totalitätsprovider darf seine eigene Zulässigkeit nicht durch sich selbst beweisen. Seine zur Aktivierung notwendige Compile-Zeit-Form muss noch unter dem Stage-1-BootstrapProvider geprüft und materialisiert werden. Erst danach darf die ProviderRegistry auf die JDL-Implementierung umschalten.

Dasselbe Prinzip gilt für weitere compilerkritische JDL-Provider, deren Ausführung einen Proof voraussetzt, den sie später selbst erzeugen: Bootstrap validiert die erste vertrauenswürdige Instanz; danach darf die JDL-Semantik denselben Query-Vertrag fortführen. Stage-1- und Stage-2-Ergebnisse desselben Vertrags müssen referenztestbar semantisch äquivalent sein.

4.7 Schreiben heißt Patchen [N] jade-compiler-db-spec §8.4

Ein schreibender Zugriff aus Compile-Zeit-Code mutiert nichts. Er erzeugt einen Patch. Erst der Materializer prüft Ring-Ebene, Ring-0-Facts, Subject-Kompatibilität, Schema, Coherence und Konflikte — und committed dann atomar.

Der Grund ist Rollback: Eine Direktmutation aus einem Rumpf, der danach noch fehlschlagen kann, hinterlässt einen halb geänderten Compilerzustand.

---

5. Inline-Imports [N] jdl-typefn-spec §8

Ein Compile-Zeit-Rumpf darf voll qualifiziert importieren. Der Import ist lokal zum Rumpf und wird gecacht.

// spekulativ
def Own(policy: OwnPolicy) ->Meta{} MetaPatch {
    import jdl::protocols::Sync
    import jdl::tags::SharePolicy
    // ...
}

Erlaubt:   Tags, Typen, Protocols, Phantoms, Funktionen
Verboten:  Services, Handles, Intrinsics

Funktionen sind importierbar [E]. Ob ein Aufruf zulässig ist, entscheidet nicht der Import, sondern die Row (§3.4). Früher standen hier „def-Funktionen“ auf der Verbotsseite; das stammt aus der Zeit von typefn.

Die Verbotsseite ist dieselbe Trennlinie wie in §3.1 und §3.3, nur auf der Importebene. Was zur Laufzeit gehört, darf nicht über einen Import in die Meta-Phase gelangen.

---

6. Der Meta-Record ist nach Ringen geschichtet

6.1 Die Schichtung [N] jdl-typefn-spec §6

Ring 0 (JME):          handle_type, memory_layout
Ring 1 (Type Engine):  own, share, init, destruct, type_constraints
Ring 2 (User):         queryable, versioned, metrics, custom

Ein höherer Ring darf einen tieferen lesen, aber nicht überschreiben. Die Prüfung passiert nicht im Rumpf, sondern beim Commit durch den Materializer.

arena_policy ist aus der Ring-0-Zeile entfallen [A]. Arena ist kein Merkmal eines Typs mehr, sondern ein Speichermuster, das ein Context über StorageRoles an Regionen bindet (wie-jade-ausfuehrt §10.1, §10.4; jdl-storage-memoryregion-empfehlung).

Ring-0-Facts primitiver Typen — Größe, Alignment, Registerklasse, Speicherart — sind axiomatisch. Sie sind lesbar und nicht überschreibbar [N] jade-compiler-db-spec §8.6.

// spekulativ
i32 :> Derive([Inspectable])   // zulässig
i32 :> Memory(Ref)             // Fehler: memory ist Ring-0-Fact

6.2 Beweisspur [N] jdl-typefn-spec §6.2, [A] für den Ort

Zu jedem Meta-Record-Eintrag lässt sich die Kette der Aufrufe und Validierungsschritte ablesen, die zu ihm geführt haben. Sie ist für Diagnostics, Tooling und :why lesbar.

Ohne diese Spur ist ein abgeleitetes Label eine Behauptung. Mit ihr ist es nachprüfbar — und zwar bis auf ein konkretes Feld.

Die Spur liegt nicht im Eintrag, sondern getrennt im ProvenanceStore (wie-jade-uebersetzt §4.5). Der Grund ist das Interning: Zwei Ableitungswege können denselben Eintrag ergeben, und die Herkunft darf die Gleichheit nicht stören. Die frühere Formulierung „jeder Eintrag trägt die Kette“ gilt deshalb nicht mehr wörtlich.

Die Spur darf veralten. Der ProvenanceStore darf Einträge verwerfen oder verdichten. Der Meta-Record-Eintrag bleibt dann gültig, nur :why verliert die Erklärung. Nachprüfbar bis aufs Feld ist ein Eintrag also, solange seine Provenance aufbewahrt wird. Das folgt aus der Regel, dass Funktionsfähigkeit nicht von Erklärbarkeit abhängen darf (wie-jade-uebersetzt §4.8).

6.3 Abschwächung mit @trust [N] jdl-typefn-spec §6.3

@trust("Begründung") senkt die Severity einer Validierung von Error auf Warning. Die Begründung wird in der Beweisspur vermerkt.

@trust kann keine Ringebene überspringen. Es macht aus einem verweigerten Beweis eine dokumentierte Ausnahme, nicht aus Ring 2 einen Schlüssel für Ring 0.

Diese Konstruktion habe ich in den durchgesehenen Dokumenten nur hier gefunden. Sie ist damit der einzige Ort, an dem eine Abschwächung überhaupt geregelt ist.

Die Abschwächung gehört ins Ergebnis, nicht nur in die Erklärung [V]. Seit die Beweisspur verworfen werden darf (§6.2), reicht der Vermerk dort nicht mehr. Ein Eintrag, der nur dank @trust zugelassen wurde, und einer, der regulär bewiesen wurde, wären nach dem Verwerfen nicht mehr zu unterscheiden.

Deshalb steht die Tatsache der Abschwächung samt Begründung im Urteil selbst und geht in dessen Hash ein. Die ausführliche Herleitung darf zusätzlich in der Provenance stehen.

Trusted Core: Eine Abschwächung ist eine Aussage über die Gültigkeit, keine Erklärung. Könnte sie mit der Provenance verschwinden, wäre die Vertrauenskette an genau dieser Stelle unterbrochen.

---

7. Wer den Eintrag liest [N] jdl-typefn-spec §9

Ein Refinement erzeugt einen Meta-Record-Eintrag. Wer ihn konsumiert, wird über ein provide MetaConsumer festgelegt.

Die Zuständigkeiten liegen nach Ring getrennt:

Ring 0   Facts vom Bootstrapper gesetzt, von JME und VM konsumiert
Ring 1   Policies wie own, share, drop — durch Beweis materialisiert
Ring 2   Runtime-orchestrierende Einträge — über MetaConsumer-Provides

Die CompilerDB indexiert alle MetaConsumer-Provides. Daraus folgt eine Tooling-Eigenschaft, die zum Nulltarif kommt: :> kann in der IDE nur die Refinements anbieten, für die im aktuellen Kontext überhaupt ein Konsument existiert.

[O] Das Beispiel in der Quelle steht im alten Engine-Vokabular. Siehe §8, Punkt 5.

---

8. Offene Punkte

#	Punkt	Abschnitt
3	Teilsprache oder nicht — Vorschlag liegt vor	§3.2, §3.5
4	<{}> user-facing oder Darstellungsform	§3.2
5	MetaConsumer im alten Engine-Vokabular	§7
8	Closures als Werte in der Meta-Phase: Beweisregeln für Aufrufe von Funktionswerten	§3.2
9	@trust im Ergebnis statt nur in der Provenance — Vorschlag liegt vor	§6.3
10	Parser: Meta direkt nach dem Pfeil reserviert — Vorschlag liegt vor	§2.1

Punkt 3 hängt noch an Punkt 8. Punkt 7 ist entschieden (§3.4). Nimmt man §3.2 an, bleibt als einzige Abweichung von gewöhnlichem JDL das Verbot von Closures als Werten, und das ist als Beweisfrage formuliert, nicht als Grammatikregel.

Punkt 4. §3.2 führt direkte Meta-Record-Literale außerhalb von Compile-Zeit-Rümpfen als offen. jdl-typefn-spec §4.2 erklärt <{}> zur reinen Darstellungsform für Diagnostics und Specs. 00-refinements §2 und 01-refinements-meta-tags §2 führen die Präfixform dagegen als gleichwertige, user-facing Schreibweise vor. jdl-blueprint-spec §10.1 benutzt <{ }> als Schreibweise für einen vollständig aufgelösten Record. Beides steht in Dokumenten mit Konsolidierungsanspruch.

Punkt 5. Das MetaConsumer-Beispiel arbeitet mit LifecycleHook.AroundExecute und einem Result-Rückgabewert. Der normative Engine-Vertrag lautet inzwischen describe → Descriptor → instantiate. Wo ein MetaConsumer in dieser Kette hängt, ist nicht abgeglichen.

Punkt 8 ist eine Frage an den Totalitätsbeweis, nicht an die Grammatik. Ruft eine Compile-Zeit-Funktion einen Funktionswert auf, den sie als Parameter bekommen hat, muss der Beweis wissen, dass auch dieser endet. Ohne Regeln dafür bleibt das Verbot.

Geschlossen in 0.3.1:

• Punkt 7, Aufruf gewöhnlicher Funktionen: Compile-Zeit-Code darf jede Funktion aufrufen, deren Row in seine Meta-Row passt [E], §3.4, MP-21.

Geschlossen in 0.3.0:

• Punkt 1, Schreibweise der Phasenmarkierung: ->Meta{...} [E], §2.1.
• Punkt 2, Allokation in der Meta-Phase: Allokation läuft normal, nur Abweichungen tragen Storage [E], §3.1. MP-3 ist entsprechend umgeschrieben.

Geschlossen in 0.2.0: Eigentümer der Totalitätsprüfung. §4.3–§4.6 legen die Zuständigkeit in die Meta-Semantik, trennen lokalen Totalitätsproof von CompilerDB-Zyklusbehandlung und schließen den Stage-2-Selbstbeweis durch Bootstrap-Validierung aus.

---

9. Normative Regeln

MP-1   Compile-Zeit-Code terminiert garantiert. Nachgewiesen wird das
       durch den Totalitätsbeweis (MP-16, MP-18), nicht durch eine
       Liste verbotener Konstrukte.
       [N] jdl-typefn-spec §2 / [V] für den Nachweis statt Verbotsliste

MP-2   Compile-Zeit-Code ist deterministisch. Gesichert wird das über
       die Meta-Row: Sie enthält keinen Service, der nach außen greift.
       [N] jdl-typefn-spec §2 / [E] für die Row, vgl. jdl-blueprint-spec BP-20

MP-3   Compile-Zeit-Code greift auf keine Resources, Handles oder
       Services der Laufzeit-Domäne zu. Allokation läuft normal; nur
       Abweichungen vom Standardspeicher tragen Storage in der Row.
       [E] ersetzt die Speicheragnostik aus jdl-typefn-spec §2

MP-4   Eine Compile-Zeit-Funktion gibt keine Compile-Zeit-Funktion
       zurück. Komposition erfolgt durch Aufruf.
       [N] jdl-typefn-spec §2

MP-5   Compile-Zeit-Code existiert zur Laufzeit nicht.
       [N] jdl-typefn-spec §2

MP-6   Jeder Aufruf löst zu einem konkreten Ergebnis auf. Kein globaler
       Meta-/Query-Fixpoint und kein phasenweites Wiederholen bis Stabilität.
       Lokale endliche Worklist-/Fixpunktalgorithmen sind nach MP-17 zulässig.
       [D] präzisiert die historische Regel aus jdl-typefn-spec §7; siehe §4.2

MP-7   Das Auswertungsfenster liegt nach der Namens- und
       Subject-Auflösung und vor Layout-Finalisierung, IR-Builder und
       Generator.
       [N] jdl-typefn-spec §3.1

MP-8   Schreibende Zugriffe erzeugen Patches, nie Direktmutation. Der
       Commit ist Sache des Materializers.
       [N] jade-compiler-db-spec §8.4

MP-9   Kein committed Meta-Record-Eintrag ohne Beweis.
       [N] jdl-typefn-spec §4.1

MP-10  Ein höherer Ring liest tiefere Meta-Ebenen, überschreibt sie
       aber nicht.
       [N] jdl-typefn-spec §6

MP-11  Ring-0-Facts sind lesbar und nicht überschreibbar.
       [N] jade-compiler-db-spec §8.6

MP-12  Inline-Imports sind voll qualifiziert und lokal zum Rumpf.
       Erlaubt sind Tags, Typen, Protocols, Phantoms und Funktionen;
       verboten sind Services, Handles und Intrinsics. Ob ein Aufruf
       zulässig ist, entscheidet die Row (MP-21).
       [N] jdl-typefn-spec §8 / [E] für Funktionen

MP-13  @trust senkt die Severity einer Validierung von Error auf
       Warning. Die Abschwächung steht samt Begründung im Urteil und
       geht in dessen Hash ein; die Herleitung darf zusätzlich in der
       Provenance stehen. Es überspringt keine Ringgrenze.
       [N] jdl-typefn-spec §6.3 / [V] für den Ort im Urteil

MP-14  Wer einen Meta-Record-Eintrag konsumiert, wird über ein
       provide MetaConsumer festgelegt.
       [N] jdl-typefn-spec §9

MP-15  Eine fehlende Phasenangabe bedeutet Runtime, nicht "irgendeine".
       [A] jade-service-typekind-arbeitsnotiz §8.4 (Status: Konsens
       einer Arbeitsnotiz, nicht normiert)

MP-16  Der Totalitätsnachweis gehört der Meta-Semantik und wird als
       deterministischer CompilerDB-Query-Vertrag bereitgestellt. Stage 1 darf
       einen Zig-BootstrapProvider nutzen; Stage 2+ darf denselben Vertrag durch
       JDL-Semantik erfüllen.
       [D] §4.3

MP-17  Ein lokaler Worklist-/Fixpunktalgorithmus ist nur innerhalb einer einzelnen
       Compile-Zeit-Auswertung zulässig, wenn seine Arbeitsdomäne explizit endlich
       und seine Terminierung nachweisbar ist. Er darf keine CompilerDB-Query-Zyklen
       als Rekursion verwenden.
       [D] §4.2, §4.4

MP-18  Fehlender Totalitätsbeweis ist kein Beweis von Nichtterminierung. Wo MP-1
       einen Totalitätsnachweis verlangt, darf ein unbewiesener Rumpf nicht
       ausgeführt werden.
       [D] §4.4

MP-19  Der erste Stage-2-Provider eines compilerkritischen Proof-Vertrags darf seine
       eigene Zulässigkeit nicht selbst beweisen. Seine Aktivierungsform wird noch
       durch den Stage-1-BootstrapProvider geprüft.
       [D] §4.6

MP-20  Die Phase steht am Pfeil vor der Row: ->Meta{...}.
       [E] §2.1

MP-21  Compile-Zeit-Code darf jede Funktion aufrufen, deren Row in seine
       Meta-Row passt. Eine leere Row passt immer; eine Row mit einem
       nach außen greifenden Service nie.
       [E] §3.4

MP-22  Der Rumpf einer Compile-Zeit-Funktion ist gewöhnliches JDL. Er
       unterscheidet sich nur durch den Totalitätsbeweis und die
       Meta-Row. Einzige Ausnahme, bis Beweisregeln dafür existieren:
       keine Closures als Werte.
       [V] §3.2, §3.5

---

10. Herkunft und Streichliste

10.1 Übernommen

jdl-typefn-spec	Hier
§2 Harte Constraints	§3.1, in 0.3 umgeschrieben
§2.1 Erlaubte Konstrukte	§3.2, in 0.3 als Vorher-Nachher-Tabelle
§2.2 Verbotene Konstrukte	§3.2, in 0.3 großteils aufgehoben [V]
§3.1 Auswertungsfenster	§4.1
§6 Ring-Schichtung	§6.1
§6.2 Proof Trace	§6.2
§6.3 @trust	§6.3
§7 Auflösungsregel	§4.2
§8 Inline-Imports	§5
§9 MetaConsumer	§7
§11 Invarianten	§9, umgestellt und umnummeriert (siehe Protokoll 0.1.0)

10.2 Nicht übernommen — steht neuer woanders

jdl-typefn-spec	Gültige Fassung
§3.2 historischer TypeFnContext	MetaContext in jade-compiler-db-spec §8.5, jdl-engine-descriptor-model §3.2
§3.3 :>-Desugaring, ApplyRefinement	jade-compiler-db-spec §8.5, 00-refinements §1.2
§4 Refinements als TypeFn-Anwendungen	00-refinements §1.1, jdl-engine-descriptor-model §5
§4.1.1 Ring-0-Facts	jade-compiler-db-spec §8.6
§5 komplett (db-Fassade)	jade-compiler-db-spec §9 — dort umfangreicher

Die Sprachreferenz §22.1 nannte §5 als zu rettend. Das hat sich beim Abgleich erledigt: Die Fassung in der CompilerDB-Spec ist neuer und enthält zusätzlich db.typeKind, db.ring0Fact, db.isRing0Fact und db.addProvide.

10.3 Ersatzlos gestrichen

jdl-typefn-spec	Grund
§1 Zweck, typefn als Schnittstelle	Deklarationsform entfällt (jdl-sprachreferenz §15.1)
typefn-Schreibweise in allen Beispielen	dito
§10 Bootstrap-Integration, Stage 1 (D)	Trusted Core ist Zig; Stage-Übergang steht in jade-compiler-db-spec §21.6
§4.2 <{}> nicht user-facing	widersprochen, jetzt offener Punkt 4 (§8)

---

Änderungsprotokoll

0.3.1 (2026-10-02) — Kohärenzprüfung. §3.4 entschieden: Compile-Zeit-Code darf jede Funktion aufrufen, deren Row in seine Meta-Row passt; offener Punkt 7 geschlossen, MP-21 und MP-12 auf [E], Import von Funktionen (§5) auf [E]. §2.1: Beispiel trägt CompilerDb in der Meta-Row. §3.2: klargestellt, dass die Determinismus-Prüfung schon entschieden ist und nur der Ersatz der Verbotsliste vorgeschlagen. §5: Beispiel Own liefert MetaPatch statt MetaRecord (Schreiben heißt Patchen, §4.7). §6.1: Beispiel als spekulativ markiert. §10.1 und §10.3: Verweise berichtigt.

0.3.0 (2026-09-29) — An den Stand seit 0.2 angeglichen. Marken [E] und [V] eingeführt. Offene Punkte 1 und 2 geschlossen: Phase am Pfeil ->Meta{...} (§2.1, MP-20); Allokation in der Meta-Phase läuft normal, MP-3 auf „kein Zugriff auf die Laufzeit-Domäne“ umgeschrieben. Kapitel 3 neu gegliedert: Garantien (§3.1), Vorschlag „gewöhnliches JDL statt Verbotsliste“ mit Terminierung über den Beweis und Determinismus über die Row (§3.2, §3.3), Aufruf gewöhnlicher Funktionen über den Row-Teilmengentest (§3.4), Auflösung des Widerspruchs „keine zweite Sprache“ (§3.5). Imports um Funktionen erweitert (§5, MP-12). arena_policy aus Ring 0 entfernt (§6.1). Beweisspur auf den getrennten ProvenanceStore umgestellt (§6.2). @trust ins Urteil verlegt (§6.3, MP-13). Neue offene Punkte 7 bis 10, neue Regeln MP-20 bis MP-22.

0.2.0 — Totalitäts- und Proof-Modell konsolidiert; Auswertungskontext auf MetaContext-Vokabular der aktuellen Constitution abgeglichen. Eigentümer des Totalitätsnachweises in die Meta-Semantik gelegt; Semantic Views als gewöhnliche CompilerDB-Queries eingeordnet; konservative Totalitätsbeweise, Facts/Obligations/Proofs, lokale endliche Worklists gegenüber globalem Meta-Fixpoint und Query-Zyklen abgegrenzt; Stage-2-Selbstbeweis durch Bootstrap-Regel ausgeschlossen; offener Punkt 6 geschlossen.

0.1.0 — Erste Fassung. Rettung aus jdl-typefn-spec nach der Entscheidung, typefn als Deklarationsform abzuschaffen. Duplikate zur CompilerDB-Spec entfernt statt mitgeschleppt, Bezug auf D durch Zig ersetzt, Invarianten von 13 auf 15 umgestellt (Phasen-Default ergänzt, Context- und Target-Invarianten an die CompilerDB-Spec abgegeben). Sechs offene Punkte erstmals geführt, darunter der Widerspruch zwischen der Verbotsliste und dem Grundsatz „keine zweite Sprache im Sprachkörper".