JDL/Jade: Axiomatik, Profiles, Executables und sichere Übergabe-Semantik¶

Dieses Dokument fasst die Erkenntnisse aus der Diskussion zusammen und konkretisiert ein konsistentes Modell für

Meta-Records (<{ ... }>)
Refinements (:> als Modifikation von Meta-Records)
Typfunktionen (typefn)
Constraints/Abfragen (Prädikate wie T: Label in where / type-level if)
fundamentale Wahrheiten (Speicher-/Besitz-/Ausführungswahrheiten)
ableitbare (sealed) Garantien
Profiles als benannte, komponierbare Absichtspakete
Passier-Semantik (Ref, RefMut, Move, Out) und deren Bezug zu D (in/ref/out/inout)
Function Pointers vs. Closures (inkl. FFI-Trampoline + userdata)

Ziel: Intention rein, Beweis raus. Der Benutzer gibt Absichten/Policies an, Jade beweist (oder widerlegt) die Zulässigkeit anhand der fundamentalen Wahrheiten und liefert dabei präzise Diagnosen.

1. Begriffe und Grundannahmen¶

1.1 Meta-Record `<{...}>`¶

Ein Typ besitzt ein Meta-Record als Compiler-seitige Beschreibung von Policies und Eigenschaften. Es ist kein Laufzeitobjekt, solange nichts explizit reifiziert wird.

1.2 Refinement-Operator `:>`¶

T :> X modifiziert den Meta-Record von T (über eine TypeFn X oder ein Profilfragment) und produziert wieder einen Typ.

Wichtig: :> ist kein Query/Constraint.

1.3 Labels/Prädikate und Constraints¶

Abfragen/Constraints passieren als Prädikate (z.B. T: Fallible + Concurrent) in

where-Constraints von typefn oder def
type-level if T: ... { ... } else { ... }

Diese Prädikate werden gegen den resolved/normalisierten Typ geprüft (Meta-Record + Protokollmenge + Closure).

1.4 Fundamentale Wahrheiten (3 Kategorien)¶

Wir trennen axiomatische Aussagen in drei orthogonale Klassen:

1) Speicherwahrheiten (Region/Arena/Lifetime/Escape) 2) Besitzwahrheiten (Aliasing/Unique/Shared/Copy/Move) 3) Ausführungswahrheiten (Pure/Fallible/Concurrent/Reorder/Isolation)

Das ist entscheidend, um falsche Ableitungen zu vermeiden (z.B. „Concurrent ⇒ Parallelizable“ ist ohne Besitz-/Speicherannahmen nicht zulässig).

2. Intention vs. Garantie (setzbar vs. sealed/derived)¶

2.1 Warum diese Trennung nötig ist¶

Ein Qualifier/Label kann zwei sehr unterschiedliche Rollen haben:

Intention/Policy: „Ich möchte X“ oder „Bitte verwende diese Strategie“.
Garantie: „X ist nachweislich korrekt und der Compiler darf darauf optimieren/umordnen/parallelisieren“.

Regel:

Alles, was dem Compiler Rechte gibt (Optimierungen, Reordering, Auto-Parallelisierung, Retry, Move über Arenagrenzen, Thread-Send/Sync etc.), muss sealed/derived sein.
Setzbar sind primär Dinge, die einschränken (z.B. NoEscape, SequentialOnly) oder reine Policy-Entscheidungen ohne Sicherheitsbehauptung.

2.2 Beispiel: `WantsRetry` (setzbar) vs. `Retryable` (derived)¶

// setzbare Intention
typefn WantsRetry() = <{ want_retry: true }>

// derived/sealed Garantie (nicht setzbar)
protocol Retryable

// (Closure-Regel, konzeptionell)
// Fallible + Pure  => Retryable

Eine API verlangt nur die Garantie:

def retry[T](op: T, attempts: i32) -> SafeReturn[T]
  where T: Retryable
{ ... }

Der Benutzer kann WantsRetry() setzen, aber das ersetzt niemals den Beweis.

3. Abfragen/Constraints in JDL (ohne Meta-Record-Reflection)¶

3.1 „Query“ ist `T: Label` (nicht `meta(T).field`)¶

Das Projektmodell nutzt Prädikate T: ... in where und type-level if. Damit bleibt die Oberfläche klein und Parametricity wird nicht durch „typecase“ unterlaufen.

Beispiele:

typefn SafeReturn[T] =
  if T: Fallible { Result[T, JadeError] }
  else           { T }

typefn Production[T] where T: Fallible + Concurrent =
  StandardTimeout[StandardRetry[T]]

3.2 Entailment arbeitet gegen die Normalform¶

T: Label prüft nicht die „rohen“ Eingaben, sondern den closed/normalisierten Wahrheitszustand (TruthProfile, siehe Abschnitt 5).

4. Intrinsic TypeFns: minimaler Zugriff auf Typinformationen¶

4.1 Motivation¶

Wenn Labels/Truths als Bitmask/Phantom-Set geführt werden sollen (für schnelle Queries), muss eine TypeFn diese Informationen aus dem Compiler-internen TypeDescriptor beziehen können.

Das ist keine Reification (keine Laufzeit-Typobjekte), sondern eine compile-time Intrinsic, die nur im Type Engine Kontext existiert.

4.2 Minimal-API (empfohlen)¶

labels_of[T] -> LabelSet (oder getrennt pro Kategorie: mem_of, own_of, exec_of)
optional: truth_of[T] -> TruthProfile (wenn man Proof-Traces/Details strukturiert ausgeben will)

Konzeptionell:

intrinsic typefn labels_of[T] -> LabelSet

typefn entails[T, L: Label] -> bool =
  labels_has(labels_of[T], L)

4.3 Ausführung einer intrinsic typefn (Type Engine Pipeline)¶

Die Intrinsic nimmt in der regulären TypeFn-Auswertung nur den Body-Evaluationsschritt ein. Substitution, Constraint-Checks, Closure, Interning und Caching laufen wie bei normalen TypeFns.

Wichtig: - Intrinsics liefern Typen (z.B. LabelSet als Phantomtyp), keine Runtime-Werte. - Intrinsics sind nur in type-level Kontexten zulässig.

5. TruthProfile: Repräsentation, Closure und Diagnostik¶

5.1 Repräsentation (praktisch und nachrechenbar)¶

Ein Typ wird (nach Normalisierung) in einem TruthProfile zusammengefasst:

Bitmasken pro Kategorie: mem_bits, own_bits, exec_bits
Payloads für parametrisierte Wahrheiten:
Region/Arena-ID (Bound(R)), Storage-Klasse
Effect-Set/Deps (falls nicht auf wenige Bits beschränkt)
ABI/Calling Convention
Proof-Trace: für jedes abgeleitete Label: Regel + Prämissen + Herkunft (Quelle im Code)

Bitmask reicht für „endliche“ Wahrheiten (Unique/Shared, Pure/Fallible/Concurrent etc.). Für Region/Effekte braucht es „Bit + Payload“.

5.2 Closure (Fixpunkt) als Mechanik¶

Closure-Regeln sind monotone Inferenzregeln:

setzen zusätzliche Bits/Labels
erkennen Widersprüche („Konflikt“) und stoppen

Fixpunkt: wiederhole Regeln bis keine Änderung.

Wichtig: Derived/Sealed Labels entstehen ausschließlich in dieser Closure.

5.3 Diagnostik („Nein, weil A, B, C“)¶

Eine gute Fehlermeldung entsteht automatisch aus TruthProfile + Proof-Trace:

Requested: Label X
Missing: Label Y
How to derive Y: Regel R benötigt Prämissen P1..Pn
Which premise failed: z.B. SharedMut vorhanden oder Effects(Effectful)
Provenance: welche Profile/Refinements haben das gesetzt

Das ist der Kernvorteil gegenüber „Compiler-Orakel“.

6. Profiles: erwartbares Verhalten, ohne den User einzusperren¶

6.1 Profile als TypeFns (Meta-Record-Pakete)¶

Profile sind benannte Bündel von primitiven Policies:

type Profile: enum = | Safe | Default | Fast | FFI | ThreadLocal | Debug

typefn Use(p: Profile) = <{ profile: p }>

typefn ProfileSafe() = <{ exec: Sequential, own: SharedImm, mem: Local, errors: Checked }>

6.2 Merge-Regeln müssen deterministisch sein¶

Profile-Komposition darf kein Zufall sein. Empfohlen:

key-weises Merging
für manche Keys: Union (z.B. deps)
für kritische Keys: Konflikt statt „last wins“

Alles, was fundamentale Wahrheiten verletzt, ist hart illegal.

6.3 Progressive Disclosure¶

Standard-Profile decken 99% ab. Nur wer es braucht, geht in Detail-Refinements.

7. Passier-Semantik als Typ (Borrow/Move/Out)¶

7.1 Phantom-Wrapper (Stdlib)¶

type Ref[T]    = Ref(T)       // shared borrow
type RefMut[T] = RefMut(T)    // mutable borrow
type Move[T]   = Move(T)      // ownership transfer
type Out[T]    = Out(T)       // output parameter (must be assigned)

Diese Wrapper sind rein compile-time Semantik: - Ref/RefMut: kein Escape, keine Speicherung in persistentem Zustand - Move: Caller verliert Zugriff („use-after-move“ ist Fehler) - Out: wird beim Eintritt initialisiert/gesperrt und muss gesetzt werden

7.2 Bezug zu D (`in/ref/out/inout`)¶

D in ≈ Ref[T] (read-only borrow)
D ref ≈ RefMut[T] (mutable borrow)
D out ≈ Out[T] (write-first, must-assign)
D inout ist const-Polymorphie → in JDL über TypeFn, die Qualifier „spiegelt“

Beispiel LikeRef (qualifier-preserving):

typefn LikeRef[A, T] =
  if A: RefMut { RefMut[T] }
  else         { Ref[T] }

8. Function Pointers, Closures und Referenzen¶

8.1 Drei callable-Formen (nicht vermischen)¶

1) FnPtr: Code-Pointer, kein Capture, ABI-stabil 2) Closure: Code + Environment (captured), ABI nicht automatisch stabil 3) Dyn-Callable: fat pointer mit Dispatch (optional)

8.2 Typen¶

type Abi: enum = | Jade | C

type Capture: enum = | None | Env

typefn ABI(a: Abi) = <{ abi: a }>

typefn Captures(c: Capture) = <{ capture: c }>

type FnPtr[Sig]  = exec[Sig] :> Captures(None)

type CFnPtr[Sig] = FnPtr[Sig] :> ABI(C)

type Closure[Sig] = exec[Sig] :> Captures(Env)

Regel (hart): Keine implizite Konversion Closure -> FnPtr.

8.3 FFI Callback: Trampoline + userdata¶

C-APIs erwarten meist callback(data, len, user). JDL bildet das sicher ab:

CFnPtr[...] ist no-capture
Capturing State liegt explizit in userdata
Lifetime/Storage von userdata muss kompatibel sein (z.B. persistent oder explizit registriert)

// C wants: int cb(u8* data, usize len, void* user)

type CCallback = CFnPtr[(Ptr[u8], usize, Ptr[Void]) -> i32]

def trampoline(data: Ptr[u8], len: usize, user: Ptr[Void]) -> i32
{
  let env_ptr: Ptr[Env] = cast[Ptr[Env]](user)
  handler(Ref(deref(env_ptr)), data, len)
} :> Captures(None) :> ABI(C)

8.4 Referenzarten (praktische Trennung)¶

Ptr[T]: raw pointer (FFI/unsafe)
Handle[T]: JME-managed reference (arena/heap)
Ref[T]/RefMut[T]: borrows/views (non-owning, no-escape)

Diese Trennung verhindert „heimliche“ Lifetime-Probleme.

9. Was gehört in JDL, was in Jade?¶

9.1 JDL/Stdlib (Policy/Absicht, Ableitung, Constraints)¶

Profile/Refinements (:>), TypeFns, Utilities
Wrapper-Typen (Ref, Move, Out)
Label-Closure-Regeln (als Daten/Regeln, soweit möglich)
Constraint-APIs (where T: ..., type-level if)

9.2 Jade (Runtime-Physik und Trusted Core)¶

Jade muss implementieren:

tatsächliche Semantik von Move / Ref / RefMut (ownership transfer, borrow discipline)
Arena-/Storage-Regeln (inkl. Cross-Storage-Verbot)
Layout/ABI (insb. CFnPtr)
Intrinsics für die Type Engine (labels_of[T], resolved meta access)
Closure/Interning/Caching als deterministische Kernmechanik

Wichtig: Typregeln können nur das erlauben, was die Runtime tragen kann. JDL beschreibt die Absicht, Jade implementiert die Mechanik.

10. Empfehlungen für ein robustes, benutzbares System¶

1) Primitive Wahrheiten klein halten, derived Labels groß. 2) Alles, was Compiler-Rechte gibt, ist sealed/derived. 3) :> bleibt nur Refinement (Meta-Record schreiben). 4) Abfragen bleiben nur Prädikate/Constraints (T: Label). 5) TruthProfile/Normalform ist die Wahrheit; alle Queries gehen dagegen. 6) Proof-Trace immer verfügbar machen (Fehlermeldungen + Tooling). 7) Profile als Standardpfad; Detail-Refinements für Experten. 8) FFI: FnPtr strikt no-capture, Capture nur über userdata + trampoline.

11. Anhang: Phantom LabelSet als Enum/Bitmask (optional)¶

Wenn Labels als Phantom-Enum geführt werden sollen:

type Label: enum =
  | Movable | Copyable | Unique | SharedImm | SharedMut
  | Persistent | Bounded
  | Fallible | Concurrent | Serializable | Isolated

type LabelMask = u64

type LabelSet = LabelSet(LabelMask)

typefn label_bit(l: Label) -> LabelMask = ...

typefn labels_has(s: LabelSet, l: Label) -> bool = ...

intrinsic typefn labels_of[T] -> LabelSet

typefn entails[T, L: Label] -> bool = labels_has(labels_of[T], L)

labels_of[T] liefert die closed/normalisierte Sicht (inkl. abgeleiteter Labels).

Offene Punkte¶

FnPtr → Closure Konversion¶

Entscheidung: FnPtr -> Closure ist explizit, nicht implizit.

Begründung: Die Konversion erfordert Allokation eines leeren Upvalue-Arrays. Implizite Allokationen widersprechen der Design Constitution ("mache Kosten sichtbar").

Offen: Konkrete Syntax für die explizite Konversion (deferred to implementation).