04 — Axiomatik, Tags und TruthProfile¶

Status: Normativer Konsolidierungsentwurf

1. Ziel¶

Die Axiomatik trennt Absicht von Beweis.

Benutzer schreibt Intention:
    Tags, Meta-Records, Refinements

Compiler erzeugt Beweis:
    TruthProfile, Labels, Proof-Trace

ASCII:

User Source
  |
  v
Tags + Meta-Records
  |
  v
Normalized Meta
  |
  v
Closure Rules
  |
  v
TruthProfile
  |
  v
proven / excluded / unproven

2. Tags sind Intention, keine Garantie¶

tag TaskLocal
    :> Own(Unique)
    :> Share(Local)

Das ist eine deklarierte Policy.

Der Compiler darf daraus erst Rechte ableiten, wenn die Closure die entsprechenden Labels bewiesen hat.

TaskLocal-Meta:
    own: Unique
    share: Local

Closure:
    -> proven(Own(Unique))
    -> proven(Share(Local))
    -> ggf. excluded(Share(Send))
    -> ggf. excluded(Share(Sync))

Der Name TaskLocal ist kein Beweis. Namen lügen. Compiler sollten das wissen, Benutzer sowieso.

3. Labelzustände¶

Jedes Label hat nach der Closure einen Zustand:

proven(X)
    X gilt. Der Compiler darf darauf bauen.

excluded(X)
    X ist aktiv ausgeschlossen. Der Compiler darf X nicht annehmen.

unproven(X)
    Kein Beweis vorhanden. Kein Fehler an sich.

Fehler entsteht erst, wenn ein Kontext proven(X) verlangt und nur unproven(X) oder excluded(X) vorhanden ist.

4. Source-Kind-Erweiterung¶

Bisherige Provenienzquellen:

user
structural_rule
combinational_rule
profile

Neue Quellen:

tag
meta_record
typefn

Empfohlene Provenienz:

source_kind: tag
source_id:   tag:TaskLocal
trace:       TaskLocal -> Own(Unique), Share(Local)

Für direkte Refinements:

source_kind: typefn
source_id:   typefn:Share
trace:       Share(Local) -> <{ share: Local }>

profile entfällt als technische Provenienzquelle. In älteren Diagnosen kann es als Benutzerbegriff weiter erklärt werden:

Profile `TaskLocal` ist ein Tag mit Meta-Record.

5. Strukturregeln lesen normalisierte Meta-Records¶

Strukturregeln laufen nicht auf roher Syntax.

Sie lesen:

- Typstruktur
- normalisierte Meta-Records
- Tag-Meta nach Expansion
- TypeFn-Ergebnisse

Beispiel:

tag TaskLocal
    :> Own(Unique)
    :> Share(Local)

type Cache : struct {
    entries: Map[str, str]
} :> TaskLocal

Vor Closure:

Cache.meta = <{ own: Unique, share: Local }>

Nicht:

Cache.meta = <{ tag: TaskLocal }>

Der Tag wird normalisiert, nicht als magischer Restzustand mitgeschleppt.

6. Tag-Domains und Konflikte¶

Falsche Domain:

type Cache : struct { ... } :> Share(Unique)

Das ist kein Closure-Konflikt, sondern ein TypeFn-Argumentfehler.

Unique gehört zu OwnPolicy.
Share erwartet SharePolicy.

Widersprüchliche Policies:

type Cache : struct { ... }
    :> Share(Local)
    :> Share(Sync)

Das ist ein Meta-/Closure-Konflikt.

Share(Local) und Share(Sync) schließen sich aus.

7. Derived/Sealed Labels¶

Derived/Sealed Labels dürfen nicht direkt durch Tags gesetzt werden.

Ungültig:

tag VeryFast
    :> <{ Retryable: true }>

Falls Retryable eine derived Garantie ist, muss sie bewiesen werden.

Gültig:

tag WantsRetry
    :> <{ want_retry: true }>

Closure:

Fallible + Pure + want_retry
    -> proven(Retryable)

Nur falls die Prämissen erfüllt sind.

8. JME-Bezug¶

JME-Policies sind Intentionen im Meta-Record.

tag RequestArena : ArenaKind

type RequestData : struct {
    body: str
} :> Memory(Arena[RequestArena])

Die Type Engine normalisiert:

memory: Arena[RequestArena]

Die Closure beweist:

proven(Memory(Arena[RequestArena]))

Der Generator/JME verwendet danach den bewiesenen Zustand.

9. Normative Regeln¶

A-1: Tags und Meta-Records drücken Intention aus.
A-2: Labels drücken bewiesene Garantien aus.
A-3: Kein Tag darf ein sealed/derived Label direkt setzen.
A-4: Tag-Meta muss vor Strukturregeln normalisiert werden.
A-5: TypeFn-Argumentfehler entstehen vor Closure.
A-6: Policy-Konflikte entstehen während Meta-Normalisierung oder Closure.
A-7: Provenienz muss Tags und TypeFns sichtbar machen.
A-8: `profile` wird als Provenienzbegriff durch `tag` ersetzt.