v0.18.0 Persistent Semantic Authority Record

This document records the completed v0.18.0 Phase 3 migration and its qualification rationale. It is not the current owner of crate internals: type and persistent-storage contracts belong to the nocter-model, nocter-persistent, and nocter-checking READMEs. It does not define Nocter source-language behavior. The milestone completion gate remains authoritative for phase status.

Problem Boundary

Before Phase 3, body checking mutated the canonical type store, copyability table, and closure builder. It captured three rollback boundaries before each body. Success committed copyability and closure journals; failure cloned complete type and copyability state when member recovery needed provisional facts, then rolled all three authorities back.

That rollback contract was negative: every future mutation had to remember to join the journal. Recovery cost also scaled with the complete semantic store rather than the facts introduced by the failed body. Moving only the type store would have retained the same failure mode in copyability and closure construction.

Adopted Authority Model

Prepared and recovery products own one immutable SemanticAuthority. It keeps the construction-owning TypeAuthority and CopyabilityTable together, while exposing only &TypeStore and &CopyabilityTable as read contracts. Body checking adds closure construction and opens one branch-local transaction containing three coordinated overlays. Finishing body checking produces one CheckedSemanticAuthority, whose private construction boundary seals the accepted semantic generation together with the only ClosureTable built from it:

SemanticAuthority (TypeAuthority + CopyabilityTable)
    |
    `-- BodySemanticAuthority (+ ClosureAuthority)
            |
            `-- BodySemanticTransaction
                    |-- TypeTransaction
                    |-- CopyabilityTransaction
                    `-- ClosureTransaction
            |
            `-- CheckedSemanticAuthority
                    |-- accepted SemanticAuthority
                    `-- finalized ClosureTable

SemanticAuthority remains intact through preparation, body recovery, checked-program completion, member queries, and concrete specialization. BodySemanticAuthority temporarily adds closure construction without splitting type and copyability ownership. Callers cannot assemble a transaction from components belonging to different bodies. Success consumes the transaction into one descendant authority. Failure cannot modify the base: it discards the branch or freezes that exact branch as a tooling capability. Preparation owns the sole production seal operation for a type/copyability pair; the empty SemanticAuthority default exists only in test builds.

Program-wide facts that do not branch with type construction have a separate single owner, ProgramEnvironment. Declaration graph, implementation selection, construction surface, instance operations, body assumptions, destruction, standard roles, and source access move together from prepared input into checked output. Preparation and checking do not repeat those fields in phase-specific carrier structs.

No compiler consumer receives a persistent chunk, intern index, mutation journal, or lineage implementation. The dependency-free nocter-persistent crate owns only path-copying collection mechanics. nocter-model wraps those mechanics in type and semantic-ID authority, while nocter-checking owns copyability, closure, and body-transaction policy. Read-only algorithms consume an immutable &TypeStore. TypeStore has no branch-opening or mutation API; only TypeAuthority can create and accept a TypeTransaction. Algorithms that may intern structural types receive that transaction through an owning semantic transaction. The same separation applies to copyability and closure state.

Identity and Lineage

A type identity is meaningful only in its owning authority. Descendants preserve the complete ancestor prefix, so checked bodies committed earlier remain valid in later sequential descendants. Sibling branches are independent and cannot be merged or exchange bare branch-local identities.

Every component transaction records its exact base lineage. SemanticTransaction atomically owns the type and copyability branches; BodySemanticTransaction adds the closure branch and is the only body-level commit boundary. Commit consumes the composite and rejects a stale or foreign component base without mutating any accepted authority. Recovery freezes the required branch together with its authority; editor APIs never separate a provisional TypeId from that value. A self-contained TypeProjection remains the boundary for isolated type presentation.

Storage Contract

Fork and immutable snapshot are constant-time authority operations. Newly interned types and proof facts occupy branch-local storage. Persistent storage may use immutable chunks and a structurally shared index, but those choices are private and replaceable.

An Arc<Vec<_>> followed by copy-on-write mutation is not sufficient: it moves the complete clone from snapshot creation to the next write. A layered linear lookup is also not a final design because its cost grows with the number of committed bodies. The selected implementation must keep lookup and interning bounded independently of body count and must preserve deterministic identity.

Nested mutable values follow the same rule. A closure draft and its final definition share one immutable definition core and keep callable requirements in a persistent sequence. Adding a requirement copies neither the environment nor the existing requirement list; final ClosureTable construction linearizes that sequence exactly once. The model exposes only the closure-identity sequence contract, not its generic persistent arena or storage debug tree.

Structural type properties that depend only on a type and its already-interned children are fixed at interning time. Storage-carrying and concreteness queries are therefore constant-time reads, rather than repeated graph traversals. Final copyability closure advances monotonically over newly appended type identities instead of rescanning the full store after substitution adds a type.

Pipeline Contract

prepared authority
    |
    | fork
    v
body transaction -- success --> commit descendant --> next body
    |
    `-- failure --> discard
              `-> freeze typed recovery

Source projection is published alongside a successful checked body, not before it. Independently successful bodies may remain sparse editor evidence after another body fails, but no recovery value can enter ownership, provenance, target closure, MIR, or backend construction as a checked program.

Editor Contract

Construction, structural-field, enum-pattern, and associated-type interruptions retain only their selected identities. Outcome repair retains one closed TypeProjection. Member selection retains one frozen semantic branch because ordinary method selection needs provisional receiver types and copyability facts.

Member completion opens one semantic query transaction from that branch. Generation-local query state may retain the query delta, but immutable compiler products remain unchanged and no complete store is cloned on first use. Each query session verifies the composite authority supplied by the query. Checked completion accepts a body-node identity and obtains its receiver type from the same checked body. The checked body also owns the exact source used for visibility, so callers cannot combine a body from the current program with a stale raw TypeId or an unrelated SourceId. Recovery queries derive their source from the interruption origin. Reusing a session with another compiler generation or another recovery interruption is an error rather than silent cross-branch identity reuse.

Downstream Boundary

nocter-persistent is a dependency-free storage-mechanics crate. Only nocter-model and nocter-checking may depend on it directly. Target closure, MIR, Machine, and runtime code consume immutable TypeStore and checked or executable contracts; their production source cannot name a type, copyability, closure, or body transaction and cannot name a persistent collection. Concrete specialization remains a checking-owned capability: its dispatch, associated-type, copy, and destruction work share one SemanticTransaction. Target code asks ConcreteDispatchResolver for specialized identities and finally receives one frozen descendant TypeStore.

Executable architecture tests enumerate workspace manifests to enforce dependency direction. Warnings-denied Clippy resolves the actual Rust type behind imports, aliases, and fully qualified paths and rejects construction authorities, transactions, closure construction sequences, and persistent collections outside their reviewed owner boundaries. Declaration and lowering exemptions cover only their program/type-construction modules. This replaces source-text scanning, which could be bypassed by renaming an import and could also reject comments accidentally. Tests may construct isolated type authorities for fixtures through local lint allowances, but no production backend phase can extend semantic state itself.

Qualification

The structural qualification compares authority operations rather than relying only on noisy wall clock measurements:

Warm success, multi-error recovery, and repeated-completion timings are recorded before final qualification. A result above the milestone regression thresholds blocks completion until explained and corrected.