v0.14.0 Final Design Findings

Status: complete; all findings resolved and requalified (2026-08-23).

The findings below are grouped by missing contract rather than by the file where a symptom appears. No production remediation began before the complete first-pass dependency inventory was recorded.

F1 — MIR Does Not Close Its Machine Input

Class: architectural debt; release gate.

Resolution: completed. The executable closure now consumes itself into a source-independent RuntimeEnvironment after MIR validation. MirProgram exposes the type store, complete nominal, opaque, and closure representations, and selected ABI as explicit backend facts. Test display names are rendered before MIR and remain ordinary immutable text. The MirProgram::executable() escape hatch and the production nocter-machine -> nocter-target-program dependency have been deleted.

MirProgram retains and publicly exposes the complete ExecutableProgram. Machine lowering then uses MirProgram::executable() to obtain the type store, executable type representations, selected target ABI, and primitive roles. Test-root lowering reaches farther through ExecutableProgram -> TargetProgram -> CheckedProgram -> DeclarationGraph -> SymbolTable merely to recover a test name.

• Producer: nocter-mir.
• Consumer: nocter-machine.
• Leaked facts: target-program storage nesting, checked graph, symbol table, target-program-owned representation variants and primitive role type.
• Failure mode: changing checked/target program storage or symbol ownership requires machine changes even when MIR and machine semantics are unchanged. Machine can also accidentally acquire new semantic authority through the retained executable.

Required replacement: MIR must publish a closed backend environment containing only the type store, concrete runtime representations, granted ABI, runtime primitive identities, and already rendered runtime test names. Machine must depend only on MIR/model contracts. The old MirProgram::executable() escape hatch and the production machine -> target-program dependency must be deleted together.

F2 — Target Capability Owns Source Projection Work

Class: architectural debt; release gate.

Resolution: completed. nocter-runtime-contract now owns source-independent primitive roles, registries, runtime representations, and ABI identities. Discovery resolves the bundled profile to exact declaration tokens; declaration lowering alone projects those tokens to callable identities. Target validation receives only the resulting semantic registry and validates the contract attached to each role without reconstructing identity from source paths or declaration spellings. Runtime contracts are imported from their owner rather than re-exported through declaration, target, or machine layers.

PrimitiveRegistry::resolve lives in nocter-target-program but consumes discovery's PrimitiveRoleInput syntax tokens and searches SourceIndex to recover callable IDs. primitive_source_location also places standard-library module paths and declaration names beside target primitive signature validation. This contradicts the crate's source-independent target capability contract.

• Producers: discovery and declaration lowering.
• Consumer currently making the decision: target program, invoked by session.
• Leaked facts: syntax tokens, source bindings, NodeKind, standard-library physical module paths and spellings.
• Failure mode: changing source projection or reorganizing authored standard files forces target capability changes; the semantic primitive registry can disagree with declaration lowering if source binding rules change.

Required replacement: a dependency-free runtime-contract owner must define primitive identities and the canonical registry value. Declaration lowering must perform the one syntax-to-semantic conversion while it owns both sides. Session may compose the result with target capability, but target program must receive only semantic bindings. The bundled profile alone owns physical standard-source locators.

F3 — A Re-export Is Treated as the Compile-input Owner

Class: maintenance issue.

Resolution: completed. Production imports now name nocter-compile-input directly and Cargo records that owner as a normal dependency. nocter-declaration-lowering is a dev-dependency used only where checking's unit tests intentionally compose the two phases.

Checking production code imports CompileUnitInput, ModuleIdentity, ModuleSourceInput, UseTargetInput, and StandardRoleInput through nocter-declaration-lowering, although nocter-compile-input owns those contracts and checking already has a direct dependency on it.

• Producer: nocter-compile-input.
• Consumer: nocter-checking.
• Leaked fact: declaration-lowering's convenience re-export surface.
• Failure mode: reorganizing or narrowing lowering's public API breaks checking despite no contract change; Cargo cannot show the true production dependency direction.

Required replacement: production imports name nocter-compile-input directly. Lowering remains a checking dev-dependency only where unit tests intentionally compose both phases.

F4 — Editor Version and Compiler Byte Override Are One Type

Class: architectural debt with a robustness symptom; release gate.

Resolution: completed. SourceOverride now carries only immutable bytes. OpenDocument composes a real editor version with a source override, and SourceOverlay distinguishes the two entry kinds. Speculative compilation preserves real versions and inserts closed reached sources as versionless overrides; the synthetic version-zero path has been deleted.

SourceOverlay stores only OpenDocument { version, bytes }. A speculative semantic edit must override every reached source, including closed disk files, to prevent mixed-generation reads. candidate_overlay therefore invents DocumentVersion(0) for closed files. The generated LSP edit correctly has no version for those same files, proving that the value is fabricated rather than a protocol fact.

• Producer: filesystem source-view contract.
• Consumers: analysis document state and language-server speculative compilation.
• Leaked fact: editor protocol version is required by a compiler byte-selection value.
• Failure mode: a synthetic version can escape through later workspace projection or be mistaken for accepted editor state; any future non-editor compiler override must invent the same fiction.

Required replacement: source byte overrides are versionless filesystem values. Accepted editor documents compose a real DocumentVersion with such an override. SourceOverlay exposes bytes for compilation and optional editor metadata for conditional LSP edits. Speculative edits replace bytes without creating metadata.

F5 — Executable APIs Expose Storage Navigation Instead of Facts

Class: architectural debt; grouped with F1.

Resolution: completed. Target program now owns a dedicated executable semantic-query implementation. MIR asks for checked bodies, declaration facts, opaque witnesses, standard roles, and allocation eligibility through named queries. The retained target is no longer publicly reachable from ExecutableProgram in production, so downstream crates cannot regress to storage navigation without changing the provider contract.

MIR validation and lowering repeatedly navigate ExecutableProgram::target().checked() to obtain declarations, standard semantics, opaque witnesses, and checked types. Those values are deliberate semantic contracts, but their storage path is not: it exposes how executable construction retained its input.

• Producer: nocter-target-program.
• Consumer: nocter-mir.
• Leaked fact: nesting of target and checked program containers.
• Failure mode: an internal ownership/ref-counting change in executable construction propagates throughout MIR even when every semantic query remains identical.

Required replacement: the executable contract supplies deliberate semantic query methods or a closed MIR-lowering environment. MIR may name declaration/checked algebraic contracts when it must validate their meaning, but it may not navigate provider storage to obtain them.

F6 — Convenience Re-exports Obscure Contract Ownership

Class: maintenance issue found by the adversarial second review.

Resolution: completed. PackageIdentity, PackageTargetKind, compile-input values, and diagnostic values are imported from their defining crates. Declaration lowering retains private crate-root imports only for its own modules; it no longer republishes those contracts. Shared test support now depends directly on compile input rather than declaration lowering. The only remaining cross-crate pub use is an adapter inside diagnostics' private JSON module and is not part of the crate's public surface.

The aliases did not duplicate semantic state, but they made Cargo edges and source imports name an intermediary rather than the owner. That weakens dependency review and allows an unrelated API cleanup to break consumers whose actual contract did not change.

Audited Non-findings

• Retaining DiscoveredUnit beside a compiled target in AnalysisSnapshot is deliberate: tooling needs the exact current-generation syntax graph and independent semantic/source projection.
• SourceIndex containing syntax identities is deliberate; it is the sole projection authority and semantic programs do not depend on it.
• Package-state publication may leave additional validated content-addressed packages after a later root-manifest commit failure. This does not change effective dependency selection; the root lock source remains the semantic commit point. Documentation should call the cache monotonic rather than imply rollback of immutable cache population.
• A complete CheckedProgram is a valid closed semantic contract. The finding is storage reach-through and omitted downstream facts, not the existence of a rich checked IR.
• nocter-model is broad, but no reviewed semantic phase depends on MIR identities to make a semantic decision. Splitting IDs without a concrete failure mode would add ceremony rather than improve authority.

Remediation Order

1. 1. Separate versionless source overrides from versioned editor documents (F4).
2. Introduce the runtime contract and move primitive source projection to declaration lowering (F2), including direct compile-input imports (F3). Completed.
3. Close the MIR backend environment and remove machine's target-program reach-through (F1). Completed.
4. Replace executable storage navigation with explicit semantic queries (F5). Completed.
5. Run an adversarial dependency/reach-through audit, then full clean qualification.

The adversarial audit found and removed F6. No unresolved finding remains, and the incremental and external-target clean qualification matrix passed after the final remediation.

Each step deletes its superseded path in the same commit. Compatibility aliases and duplicated authorities are not acceptable intermediate completion states.