JDL — Label-Inferenzregeln und Closure-Axiome¶

Status: Normativ
Version: 0.6
Ergänzt: 04-axiomatik-profiles-executables.md
Priorität: Bei Widerspruch mit 04-axiomatik gilt 04-axiomatik.

Zweck¶

04-axiomatik beschreibt wie die Label-Closure funktioniert — Fixpunkt, monotone Inferenzregeln, TruthProfile. Dieses Dokument beschreibt was sie enthält: die vollständigen Regeln, nach denen Labels vergeben und abgeleitet werden.

Dieses Dokument ist die normative Quelle für die TypeEngine-Implementierung. Jede Regel hier ist eine Zeile im Closure-Algorithmus.

Designprinzip¶

Das zentrale Ziel ist: Intention rein, Beweis raus.

Der Benutzer deklariert seine Absicht durch Typstruktur und Meta-Records. Der Compiler leitet aus diesen Angaben alle Garantien her — vollständig, deterministisch, und nachvollziehbar. Kein Label das dem Compiler Rechte gibt darf direkt gesetzt werden. Es muss bewiesen werden.

Das hat drei praktische Konsequenzen:

Fehlermeldungen sind präzise: nicht "Typ passt nicht", sondern "Label X fehlt, weil Regel R die Prämissen P1 und P2 benötigt, und P2 wurde durch Feld Y verhindert."
LSP-Tooling kann für jeden Typ zeigen warum er welche Labels trägt — als Hover-Information, Inlay-Hint oder auf Anfrage.
Inkrementelle Recompilierung invalidiert genau die Typen deren Label-Prämissen sich geändert haben — nicht mehr, nicht weniger.

Aufbau¶

Regeln sind in zwei Klassen eingeteilt:

Klasse S — Strukturregeln
Primitive Labels die direkt aus der Typstruktur folgen. Sie werden vor der Closure gesetzt — als Ausgangszustand des TruthProfile. Strukturregeln lesen Felder, Typkonstruktoren und explizite Meta-Record-Einträge.

Klasse C — Kombinationsregeln
Derived/Sealed Labels die aus bestehenden Labels durch Inferenz entstehen. Sie entstehen ausschließlich in der Closure. Nie direkt setzbar. Kein Benutzer kann ein sealed Label in einem Meta-Record schreiben — der Compiler würde es als Fehler zurückweisen.

Label-Kategorien (Lesehilfe)¶

Labels sind in fünf semantische Kategorien eingeteilt. Die Kategorien haben keinen Einfluss auf die Regelstruktur — sie dienen der Orientierung.

Kategorie	Labels
Speicher	`Memory(Value)`, `Memory(Rc)`, `Drop(Trivial)`, `Drop(Custom)`
Besitz	`Own(Unique)`, `Own(Shared)`, `Own(Weak)`, `Copyable`
Task-Grenzen	`Share(Local)`, `Share(Send)`, `Share(Sync)`, `CopyOnSend`, `MoveOnSend`
Ausführung	`Captures(None)`, `Captures(Env)`, `Pure`, `Fallible`, `Concurrent`, `Retryable`
Runtime-Direktiven	`AtomicRefcount` — interne Ableitungen die Jade direkt instruieren, für den Benutzer nicht sichtbar

Negationsmodell¶

Drei Labelzustände¶

Jedes Label eines Typs befindet sich nach der Closure in genau einem von drei Zuständen:

Zustand	Bedeutung
`proven(X)`	X gilt. Der Compiler darf auf X bauen.
`excluded(X)`	X ist aktiv ausgeschlossen — durch Benutzerentscheidung oder Strukturregel. Der Compiler darf X nicht annehmen.
`unproven(X)`	X ist weder bewiesen noch ausgeschlossen. Der Compiler darf X nicht annehmen.

unproven(X) ist der Defaultzustand für jedes Label vor der Closure. Es ist kein Fehlerzustand. Viele Typen bleiben dauerhaft unproven für viele Labels — das ist normal und erwartet.

Ein Fehler entsteht erst wenn ein Sprachkontext, eine Operation oder eine Constraint proven(X) voraussetzt und nur unproven(X) oder excluded(X) vorliegt.

Unterschied zwischen `excluded` und `unproven`¶

excluded(X) und unproven(X) haben operativ denselben Effekt: der Compiler darf X nicht annehmen. Sie unterscheiden sich in Diagnostik und Konfliktverhalten:

excluded(X) durch Benutzer blockiert Regelableitungen die X erzwingen würden. Wenn eine Strukturregel X trotzdem als proven setzt, entsteht ein Solver-Konflikt — kein stilles Überschreiben.
unproven(X) bedeutet nur: kein Beweis vorhanden. Spätere Regeln dürfen X noch ableiten (Monotonie bleibt intakt).

Wer darf `excluded` setzen?¶

Strukturregeln (S-Klasse): dürfen sowohl proven als auch excluded setzen — aus Typstruktur oder expliziten Meta-Record-Angaben.
Kombinationsregeln (C-Klasse): dürfen nur proven setzen. Kombinationsregeln schließen keine Labels aus — sie leiten nur positive Garantien her. Unverträgliche Kombinationen werden als Solver-Konflikt (✗) ausgedrückt, nicht als excluded.

Diese Einschränkung hält das Modell konsistent: excluded ist immer auf die initiale Strukturphase oder explizite Benutzerangaben zurückführbar, nie auf transitiven Schluss im Fixpunkt-Loop.

Provenienz (verpflichtend)¶

Jeder proven- und excluded-Eintrag muss die Herkunft mitführen:

Feld	Inhalt
`source_kind`	`user` \| `structural_rule` \| `combinational_rule` \| `profile`
`source_id`	z. B. `S-1`, `C-2`, `derive`, `profile:Server`
`trace`	rekursive Kette der Prämissen die zur Ableitung führten

unproven-Einträge tragen keine Provenienz — Abwesenheit von Beweis braucht keine Herkunft.

Solver-Ergebnis (separat vom LabelSet)¶

conflict ist kein Labelzustand. Es ist ein Ergebnis des Closure-Laufs, das außerhalb des LabelSets existiert:

Solver-Ergebnis	Bedeutung
`ok`	Gültige Klassifikation erzeugt. LabelSet ist konsistent.
`conflict`	Klassifikation gescheitert. Kein gültiges LabelSet produziert.

Wenn conflict eintritt, existiert für diesen Typ kein finales LabelSet. Der Compiler gibt Diagnostic + vollständigen Proof-Trace aus.

Würde conflict als Label im LabelSet modelliert, würde ein Fehlerzustand dieselbe ontologische Schublade wie echte Typmerkmale bewohnen — mit unerwünschten Folgefragen (kann auf Konflikt-Labels weiter geschlossen werden?). Fehlerzustände beschreiben gescheiterte Klassifikation, nicht gültige Typen.

Notation¶

S-n              Strukturregel Nummer n
C-n              Kombinationsregel Nummer n

proven(A)        A ist im LabelSet als proven eingetragen
excluded(A)      A ist im LabelSet als excluded eingetragen
not_proven(A)    Kurzform: excluded(A) oder unproven(A) 
                  — beide Fälle gemeint

A + B → L        wenn proven(A) und proven(B), wird proven(L) gesetzt
A → L            wenn proven(A), wird proven(L) gesetzt

A + not_proven(B) → L
                  wenn proven(A) und not_proven(B), 
                  wird proven(L) gesetzt

A + excluded(B) → L
                 wenn proven(A) und explizit excluded(B), 
                 wird proven(L) gesetzt

A + B → ✗        Konflikt — Solver-Ergebnis: conflict, Closure stoppt

Wenn eine Regel gezielt auf excluded(B) vs. unproven(B) reagiert, wird dies ausgeschrieben. not_proven(B) ist nur dann erlaubt, wenn wirklich beide Fälle identisch behandelt werden sollen — und dies in der Regel explizit begründet wird.

Alle Regeln sind monoton: Labels bewegen sich nur von unproven zu proven oder excluded, nie zurück. Konflikte (✗) stoppen die Closure sofort mit einem Diagnostic das den vollständigen Proof-Trace enthält.

Geltungsbereich: Strukturregeln klassifizieren deklarierte JDL-Typen und deren Meta-Records. VM-Register, temporäre Slots, JadeValue- Grenzrepräsentationen und sonstige VM-interne Laufzeitdarstellungen sind nicht Gegenstand dieser Labelableitung. Ein Register-Slot der eine HandleId trägt ist nicht ein Struct das einen Handle besitzt — es ist die VM-seitige Darstellung eines bereits klassifizierten JDL-Werts.

Beziehung zu 11-jadevalue-und-register-layout: JadeValue taucht ausschließlich an Call-, Return-, Intrinsic- und FFI-Grenzen auf. Innerhalb einer Funktion arbeitet die VM direkt auf einem typsicher angelegten Register-Buffer. Labelableitung und VM-Ausführung reden nicht übereinander, sondern nacheinander.

Klasse S — Strukturregeln¶

Strukturregeln laufen einmal vor der Closure und setzen den initialen LabelSet. Sie sind nicht iterativ — jede Regel feuert genau einmal pro Typ. Strukturregeln dürfen sowohl proven als auch excluded setzen.

S-1 Nur-Primitive-Struct¶

alle Felder in { i8, i16, i32, i64, u8, u16, u32, u64, f32, f64, bool, () }
→ proven(Memory(Value))
→ proven(Drop(Trivial))
→ proven(Copyable)

Ein Struct dessen Felder ausschließlich primitive Skalare sind, benötigt keinen Heap-Speicher, keinen JME-Handle und keinen Destruktor. Er lebt vollständig inline — auf dem Stack oder direkt in einem Parent-Struct. Das Kopieren ist eine reine Bitoperation ohne Seiteneffekte.

() (Unit) ist eingeschlossen weil es als Feld semantisch ein No-Op ist.

S-2 Enthält Handle-Typ¶

mindestens ein Feld ist str, [T], Map[K, V], oder ein JME-verwalteter Typ
→ proven(Memory(Rc))

Handle-Typen sind JME-verwaltete Objekte. Sie existieren auf dem Heap und werden über opake Handles mit Generation-Countern referenziert. Ein Struct das solche Felder hält, ist selbst JME-verwaltet und muss über Memory(Rc) alloziert werden — andernfalls würde ein Stack-Struct einen Heap-Handle halten dessen Lifetime nicht durch den Refcount gesichert ist.

Scope-Grenze: Diese Regel beschreibt deklarierte Felder in JDL-Typen. Sie beschreibt nicht VM-Register oder temporäre Slots die HandleIds transportieren. Siehe Geltungsbereich im Notation-Abschnitt.

S-3 Enthält HandleId¶

mindestens ein Feld ist HandleId
→ proven(Memory(Rc))
→ proven(Own(Unique))

HandleId ist in Jade der rohe Identifikator eines JME-Objekts im Handle-Table — per Definition immer an exklusiven Besitz gebunden. Ein Struct das eine HandleId als deklariertes Feld hält, ist der exklusive Besitzer dieses Objekts. Mehrere Besitzer einer HandleId würden zu doppelten Drops und Use-After-Free führen.

Wenn geteilter Besitz gewünscht ist, muss explizit ein Wrapper-Typ mit Own(Shared) verwendet werden.

S-4 Explizites Own(Shared)¶

own: Shared gesetzt (explizit oder via Profil)
→ proven(Copyable)

Own(Shared) bedeutet refgezählter Besitz — Arc-Semantik. Das "Kopieren" ist semantisch ein Refcount-Inkrement: kein Duplizieren, aber ein weiterer Besitzer wird registriert. Deshalb impliziert Own(Shared) zwingend proven(Copyable).

Hinweis zu Copyable-Semantik: proven(Copyable) bedeutet in Jade sprachliche Kopierbarkeit — die Operation ist erlaubt. Welcher Mechanismus darunter liegt (Bitoperation, Refcount-Inkrement) ist durch die übrigen Labels (Memory, Own) bestimmt. Die Unterscheidung ist kompositionell.

S-5 Explizites Own(Weak)¶

own: Weak gesetzt
→ proven(Copyable)
→ excluded(Own(Unique))  [source_kind: structural_rule, source_id: S-5]
→ excluded(Own(Shared))  [source_kind: structural_rule, source_id: S-5]

Ein Weak-Handle ist eine nicht-besitzende Referenz auf ein Shared-Objekt. Er trägt nicht zum Refcount bei. Die Ausschlüsse sind strukturell abgeleitete Folgen der Benutzerangabe own: Weak — abgeleitet durch S-5, nicht direkt vom Benutzer gesetzt. source_kind: structural_rule ist korrekt.

S-6 Explizites Derive([!X])¶

derive: [!X] im Meta-Record
→ excluded(X)  [source_kind: user, source_id: derive]

Explizite Benutzer-Exclusion setzt excluded mit source_kind: user. Sie blockiert spätere Regelableitungen die X erzwingen würden. Wenn eine Strukturregel X trotzdem als proven setzt, entsteht Solver-Konflikt.

S-7 FnPtr / CFnPtr¶

Typ ist FnPtr[Sig] oder CFnPtr[Sig]
→ proven(Captures(None))
→ proven(Copyable)

Funktions-Pointer sind Code-Pointer ohne Capture. Trivial kopierbar.

S-8 Closure¶

Typ ist Closure[Sig]
→ proven(Captures(Env))

wenn alle Captures proven(Copyable):
→ proven(Copyable)

sonst:
→ excluded(Copyable)  [source_kind: structural_rule, source_id: S-8]

Eine Closure ist nur dann kopierbar, wenn alle ihre Captures es ebenfalls sind. Der Compiler prüft die Capture-Umgebung strukturell. Benutzer- Assertion ohne Strukturbeweis ist nicht ausreichend — der Beweis muss aus den Labels der Captures folgen.

S-9 Enum mit ausschließlich Value-Varianten¶

alle Varianten sind Nur-Primitive (S-1)
→ proven(Memory(Value))
→ proven(Drop(Trivial))
→ proven(Copyable)

S-10 Struct enthält Feld mit Drop(Custom)¶

mindestens ein Feld hat proven(Drop(Custom))
→ proven(Drop(Custom))  am Container-Typ

Custom-Drop propagiert nach oben.

Propagation bei parametrischen Typen¶

Prinzip¶

Bei parametrischen Typen C[T] unterscheidet der Compiler zwischen zwei Kategorien von Labels:

Restriktive Labels beschränken den zulässigen Verhaltensraum eines Typs. Ihre Propagation von T auf C[T] ist eine konservative Sicherheitsableitung — der Wrapper hebt eine bestehende Einschränkung nicht auf. Restriktive Labels werden vom Compiler automatisch propagiert. Der Typautor muss nichts deklarieren.

Erlaubende Labels schreiben einem Typ zusätzliche Fähigkeiten oder Nutzungsrechte zu. Ihre Geltung auf C[T] hängt von der internen Semantik des Containers ab — davon ob seine Struktur, Speicherform und Invarianten die Fähigkeit tragen. Erlaubende Labels werden nicht automatisch propagiert. Der Typautor muss eine explizite Propagations- oder Ableitungsregel definieren.

Prüffrage für die Kategorisierung:

Ein Label ist automatisch propagierbar, wenn: - seine Weitergabe den zulässigen Verhaltensraum nur verkleinert - seine Propagation konservativ sicher ist - keine zusätzliche Implementierungsbehauptung des Wrappers nötig ist

Ein Label ist nicht automatisch propagierbar, wenn: - seine Weitergabe dem Typ zusätzliche Fähigkeiten zuschreibt - die Gültigkeit von der internen Semantik des Wrappers abhängt - der Compiler das nicht allein aus „enthält T" ableiten darf

Bekannte Kategorisierungen:

Label	Kategorie	Begründung
`Share(Local)`	restriktiv	verhindert Task-Grenzüberschreitung
`Own(Unique)`	restriktiv	verhindert Aliasing
`Drop(Custom)`	restriktiv	erzwingt Destruktor-Aufruf (S-10)
`Copyable`	erlaubend	gibt Benutzungserlaubnis, abhängig von Container-Semantik
`Share(Sync)`	erlaubend	Sync-Fähigkeit muss explizit behauptet werden
`Retryable`	erlaubend	abhängig von Container-Implementierung

S-11 Parametrischer Typ mit Share(Local) Typparameter¶

C[T] wobei proven(Share(Local)) auf T
→ proven(Share(Local))  auf C[T]

Wenn der Typparameter den Task nicht verlassen darf, darf es der instanziierte Container ebenfalls nicht. Option[RequestContext] mit RequestContext: Share(Local) ist selbst Share(Local) — ohne Benutzerangabe.

Kollidiert mit proven(Share(Send)) oder proven(Share(Sync)) via C-7 bzw. C-8 — der Solver erkennt den Konflikt.

S-12 Parametrischer Typ mit Own(Unique) Typparameter¶

C[T] wobei proven(Own(Unique)) auf T
→ proven(Own(Unique))  auf C[T]

Ein Container der einen Own(Unique)-Wert hält, ist selbst nicht kopierbar oder aliasierbar — das exklusive Ownership-Invariant muss transitiv gelten.

Ausnahme: Wrapper-Typen die Ownership explizit transferieren (z.B. Move-Semantik-Wrapper) dürfen Own(Unique) auf dem Typparameter konsumieren ohne es auf sich selbst zu setzen — aber nur durch explizite Deklaration des Typautors.

Klasse C — Kombinationsregeln¶

Kombinationsregeln laufen im Fixpunkt-Loop. Sie feuern solange bis keine Regel mehr neue Labels setzt. Kombinationsregeln setzen ausschließlich proven — niemals excluded. Unverträgliche Kombinationen werden als Solver-Konflikt (✗) ausgedrückt.

C-1 Shared + Sync → AtomicRefcount¶

proven(Own(Shared)) + proven(Share(Sync))
→ proven(AtomicRefcount)

Wenn ein refgezählter Typ über Task-Grenzen geteilt wird, muss der Refcount atomar sein. JME wählt automatisch atomare Ops.

C-2 Fallible + Pure → Retryable¶

proven(Fallible) + proven(Pure)
→ proven(Retryable)  (sealed)

Eine pure, fehlbare Operation kann beliebig oft wiederholt werden ohne Seiteneffekte. Der Compiler darf automatisch Retry-Strategien anwenden.

Quelle: 04-axiomatik §2.2

C-3 Share(Sync) → Concurrent¶

proven(Share(Sync))
→ proven(Concurrent)

Ein Typ der gleichzeitig aus mehreren Tasks nutzbar ist, trägt das Concurrent-Label.

C-4 Share(Sync) + Own(Unique) — kein pauschaler Konflikt¶

proven(Share(Sync)) + proven(Own(Unique))
→ kein automatischer Konflikt

Own(Unique) (genau ein logischer Besitzer) und Share(Sync) (concurrent nutzbar) schließen sich nicht automatisch aus. Ein Typ kann exklusiv besessen sein und trotzdem intern synchronisiert werden — etwa ein Mutex-artiger Typ: einer besitzt ihn, aber die Implementierung ermöglicht sicheren concurrent access intern.

Der eigentlich gefährliche Fall ist aliasierbarer gleichzeitiger Mehrfachbesitz — der ist durch C-9 abgedeckt.

Frühere Formulierung Concurrent + Own(Unique) → ✗ war zu pauschal und hätte gültige Sync-Wrapper verboten. Gestrichen in v0.3.

Eine Advisory-Regel für Share(Sync) + Own(Unique) + not_proven(Drop(Custom)) ist konzeptionell sinnvoll, wird aber erst eingeführt wenn die formale Behandlung von Advisories spezifiziert ist. Bis dahin hat C-4 keine normative Regelkonklusion.

C-5 Share(Send) + Copyable → CopyOnSend¶

proven(Share(Send)) + proven(Copyable)
→ proven(CopyOnSend)

An Task-Grenzen wird kopiert. Der Sender behält seinen Wert.

C-6 Share(Send) + not_proven(Copyable) → MoveOnSend¶

proven(Share(Send)) + not_proven(Copyable)
→ proven(MoveOnSend)

An Task-Grenzen wird bewegt wenn Copyable weder bewiesen noch beweisbar ist. not_proven(Copyable) ist hier bewusst als Sammelnotation verwendet: excluded(Copyable) und unproven(Copyable) werden für die Move-Entscheidung identisch behandelt — in beiden Fällen ist keine Copy-Semantik verfügbar. Der Sender verliert seinen Zugriff statisch.

Quelle: 03-runtime — Copy vs. Move bei Task-Grenzen

C-7 Share(Local) + Share(Send) → Konflikt¶

proven(Share(Local)) + proven(Share(Send))
→ ✗  KONFLIKT

Local verbietet explizit das Verlassen des Tasks. Send erlaubt es.

C-8 Share(Local) + Share(Sync) → Konflikt¶

proven(Share(Local)) + proven(Share(Sync))
→ ✗  KONFLIKT

Analog zu C-7.

C-9 Own(Unique) + Own(Shared) → Konflikt¶

proven(Own(Unique)) + proven(Own(Shared))
→ ✗  KONFLIKT

Exklusiver und geteilter Besitz schließen sich aus. Das ist die primäre Schutzregel gegen aliasierenden Mehrfachbesitz.

C-10 Memory(Value) + Own(Shared) → Konflikt¶

proven(Memory(Value)) + proven(Own(Shared))
→ ✗  KONFLIKT

Value-Typen leben auf dem Stack. Shared-Ownership erfordert Heap.

C-11 Captures(None) + Captures(Env) → Konflikt¶

proven(Captures(None)) + proven(Captures(Env))
→ ✗  KONFLIKT

Ein Callable kann nicht gleichzeitig capture-frei und capturing sein.

C-12 Drop(Trivial) + Drop(Custom) → Konflikt¶

proven(Drop(Trivial)) + proven(Drop(Custom))
→ ✗  KONFLIKT

Destruktor-Semantik muss eindeutig sein.

C-13 (AutoParallelizable) wurde in v0.3 gestrichen. Die Prämissen Retryable + Concurrent + Memory(Rc) reichen nicht als Beweis für Parallelisierbarkeit — es fehlen mindestens Pure, Deterministic, NonBlocking, NoExternalOrdering. AutoParallelizable kann als gezielte Optimierungsregel mit harten Voraussetzungen später wieder eingeführt werden.

Fixpunkt-Algorithmus (normativ)¶

1. Initialisiere LabelSet: alle Labels sind unproven
2. Wende Strukturregeln an (S-1 .. S-n):
   - Setze proven(L) oder excluded(L) mit Provenienz
   - Bei Kollision proven(X) gegen user-excluded(X): Solver-Konflikt → stoppe
3. Wiederhole (Closure):
   a. Für jede Kombinationsregel (C-1 .. C-n):
      - Prüfe Prämissen gegen aktuellen LabelSet
      - Wenn Prämissen erfüllt und Conclusion noch nicht gesetzt:
          * Konflikt-Regel (→ ✗) → Solver-Ergebnis: conflict → stoppe mit Diagnostic
          * Label-Regel (→ proven(L)) → setze proven(L) mit Provenienz,
            markiere Iteration als dirty
4. Wenn keine Iteration dirty war → Fixpunkt erreicht, fertig

Invariante: Kombinationsregeln setzen ausschließlich proven, nie excluded. Labels bewegen sich im Closure-Loop nur von unproven zu proven, nie zurück und nie zu excluded. excluded kann nach dem initialen Strukturregellauf (Schritt 2) nicht mehr neu entstehen.

Der Algorithmus terminiert weil: - Labels bewegen sich nur von unproven zu proven (Monotonie) - Die Menge aller möglichen Labels endlich ist - Konflikte sofort stoppen

Determinismus ist garantiert: die Regelreihenfolge beeinflusst nicht das Ergebnis, nur die Anzahl der Iterationen bis zum Fixpunkt.

Proof-Trace Anforderungen¶

Für jedes proven(L) und excluded(L) muss der Compiler festhalten:

Label:        welches Label gesetzt/ausgeschlossen wurde
Zustand:      proven | excluded
source_kind:  user | structural_rule | combinational_rule | profile
source_id:    S-n, C-n, "derive", "profile:Foo", usw.
Prämissen:    welche Labels die Regel ausgelöst haben
Herkunft:     bei Strukturregeln: welches Feld / welcher Typ
              bei Kombinationsregeln: welche Regeln die Prämissen gesetzt haben

Der Trace ist vollständig rekursiv: jede Prämisse hat selbst einen Trace. Das ergibt einen Beweis-Baum der für jeden Leaf-Label auf ein konkretes Feld im Quellcode zeigt.

Diagnostik-Beispiele:

FEHLER: Copyable ist an dieser Stelle erforderlich,
        aber für Typ T nicht bewiesen.
        → unproven(Copyable): keine Regel hat Copyable abgeleitet.

FEHLER: Copyable ist erforderlich,
        aber excluded(Copyable) [source: user, derive: [!Copyable], Zeile 12].

FEHLER: Copyable ist erforderlich,
        aber excluded(Copyable) [source: structural_rule S-8]:
        Capture 'callback' (Zeile 7) ist not_proven(Copyable).

Dieser Trace ist die Grundlage für: - Fehlermeldungen — präzise Herkunft jedes fehlenden Labels - LSP-Hover — Inlay-Hints zeigen warum ein Typ ein Label trägt, mit Unterscheidung zwischen proven by user, proven by rule, excluded - Inkrementelle Recompilierung — CompilerDb DepGraph invalidiert transitiv alle Typen deren Label-Prämissen sich geändert haben

Anforderung aus 04-axiomatik §5.1 und §5.3

Offene Punkte¶

~~Propagationsregeln für generische Typen~~ — geschlossen in v0.5

Gelöst durch das Restriktiv/Erlaubend-Prinzip und S-11, S-12. Restriktive Labels propagieren automatisch. Erlaubende Labels erfordern explizite Deklaration des Typautors.

Serializable-Ableitung

Wann wird Serializable aus der Struktur abgeleitet vs. explizit deklariert?

Advisory-Kategorie

Advisories (strukturelle Warnungen ohne Solver-Konflikt) sind konzeptionell vorgesehen — C-4 identifiziert einen Kandidaten (Share(Sync) + Own(Unique) + not_proven(Drop(Custom))). Die formale Behandlung (Regeloutput-Typ, Reporting, Unterdrückung, Eskalation) ist noch nicht spezifiziert. Bis zur Spezifikation haben Advisories keinen normativen Status in diesem Dokument.

Integration S-11, S-12, C-14..C-17

In v0.2 wurden Arena/Isolation/SafeReset/Cross-Arena-Regeln in einem separaten Branch definiert. Diese Integration in den Hauptzweig steht noch aus.

Änderungsprotokoll¶

Version 0.6 — Label-Kategorien als Lesehilfe eingeführt: - Fünf Kategorien: Speicher, Besitz, Task-Grenzen, Ausführung, Runtime-Direktiven - AtomicRefcount als Runtime-Direktive klassifiziert - Keine Änderung an Regelstruktur oder Semantik

Version 0.5 — Propagation bei parametrischen Typen: - Neues normatives Prinzip eingeführt: Restriktive Labels propagieren automatisch von Typparametern auf Container. Erlaubende Labels erfordern explizite Deklaration des Typautors. - Prüffrage als Entscheidungshilfe für die Kategorisierung normativ festgehalten. - Bekannte Label-Kategorisierungen als Tabelle dokumentiert. - S-11 eingeführt: Share(Local) propagiert automatisch auf parametrischen Container. - S-12 eingeführt: Own(Unique) propagiert automatisch auf parametrischen Container, mit Ausnahmeregelung für Ownership-Transfer-Wrapper. - Offener Punkt "Propagationsregeln für generische Typen" geschlossen.

Version 0.4 — Spezifikationsschärfen bereinigt: - Notation: !B gestrichen. Explizite Formen eingeführt: excluded(X), unproven(X), not_proven(X) als Sammelform (nur wenn beide Fälle identisch behandelt werden, mit Begründungspflicht) - Negationsmodell: Einschränkung normativ festgehalten — Kombinationsregeln dürfen ausschließlich proven setzen, nie excluded - Fixpunkt-Algorithmus: Invariante ergänzt — excluded kann nach Strukturregelphase nicht mehr entstehen - S-5: Provenienz-Formulierung korrigiert. excluded(Own(...)) ist strukturell regelbedingt (source_kind: structural_rule), nicht direkt vom Benutzer gesetzt. Abgrenzung zu S-6 klar - C-4: Normative Advisory-Regel entfernt. C-4 hat vorerst keine Regelkonklusion. Advisory-Kandidat in Offene Punkte verschoben - C-6: !Copyable durch not_proven(Copyable) ersetzt, mit expliziter Begründung warum Sammelnotation hier korrekt ist - Alle Regelformulierungen auf proven(...)/excluded(...) Notation vereinheitlicht - Änderungsprotokoll: fehlende Regeln S-11..C-17 als offener Integrationspunkt dokumentiert

Version 0.3 — Negationsmodell, C-4 Korrektur, C-13 Streichung: - Negationsmodell normativ eingeführt: drei Labelzustände (proven, excluded, unproven), Provenienz-Pflicht, conflict als Solver-Ergebnis außerhalb des LabelSets - unproven(X) als normaler Ruhezustand definiert - Geltungsbereich-Abgrenzung: Strukturregeln klassifizieren JDL-Typen, nicht VM-interne Repräsentationen (Verweis auf 11-jadevalue) - S-2: Scope-Hinweis ergänzt - S-8: Copyable-Ableitung strukturell an Captures gebunden - C-4: Pauschalen Konflikt gestrichen, Erklärung ergänzt - C-13: AutoParallelizable gestrichen

Version 0.2 — Erweiterung der offenen Punkte aus v0.1. Regeln S-11, S-12, C-14..C-17 (Arena/Isolation/SafeReset/Cross-Arena) in separatem Branch definiert. Integration ausstehend.

Version 0.1 — Initiale Definition. Strukturregeln S-1..S-10, Kombinationsregeln C-1..C-13. Fixpunkt-Algorithmus normativ.