v0.20.0 Phase 0 Interface-Prerequisite Review

Result: passed after two reopenings (2026-08-29). The initial 2026-08-28 review did not exercise entailed structural predicates through every checking descendant. Phase 0 was reopened as a design change rather than closed with local guards. A subsequent whole-range review found an unbounded closure representation and two semantic-query contract defects; those were corrected before the phase was closed again. This record covers the corrected language contract, declaration authority, body evidence, implementation proof, concrete dispatch, editor behavior, and a subsequent compiler-wide review. Hashing and associative collections remain outside Phase 0.

Review Criteria

The review traced:

• every authored interface-header predicate from parsing through direct declaration edges, specialization, implementation validation, body evidence, concrete dispatch, and editor queries;
• direct, transitive, generic-subject, structural, and inherited-associated-type prerequisites;
• dependency cycles and effective member collisions independently of declaration order;
• proof-only requirements versus evidence-bearing body facts;
• stale compatibility paths, declaration reinterpretation, duplicate graph traversal, unchecked caller obligations, panic-based evidence assumptions, and semantic decisions leaking into source projection;
• the complete compiler range, including declaration lowering, checking, provenance, loans, target specialization, analysis queries, language-server behavior, MIR, and machine lowering.

Reopened Findings and Design Remediation

Authored roots were incorrectly reused as entailed predicates

One authored T impl Derived requirement can entail equality, callable, coercion, index, or expansion predicates declared elsewhere. The first implementation attached the authored root RequirementId to every derived fact. Provenance, loan, concrete-dispatch, and signature-help code then reopened that root and expected its declaration kind to match the selected operation. Derived expansion and callable programs consequently reached internal E0900 failures.

CapabilityEvidence is now the sole downstream contract. It records the authored root, the exact prerequisite declaration reached through closure, and the specialized predicate. Static structural and inherited-interface dispatch carries only CapabilityEvidenceId; it no longer transports a second requirement identity that a consumer could reinterpret. Provenance, loans, concrete specialization, source projection, and signature help all read the same exact evidence record.

Optional evidence admitted an invalid proof/runtime state

CheckedRequirement previously stored Option<CapabilityEvidenceId>. Declaration prerequisite validation necessarily produced None, while body selection expected Some at six panic sites. A valid declaration proof could therefore enter a selector path that assumed body evidence and panic.

The model now has two representations. CheckedRequirement is proof-only and cannot carry runtime evidence. BodyRequirement always carries an evidence identity. Selection context is an exclusive None | Proof | Body state, so a proof context cannot manufacture structural dispatch and no caller must remember which optional field is populated.

Dependency cycles and member inheritance were conflated

The first graph followed only Self impl Interface edges. That is correct for inherited members but incorrect for termination: interface Recursive<T> where T impl Recursive<T> was accepted and recursive normalization silently stopped at an active-set guard.

The declaration graph now owns two distinct relations. Cycle validation follows every interface predicate exactly once through a visit-state graph. Member inheritance follows only contextual Self edge. It stores authored direct prerequisite identities; checking specializes a worklist from those identities and deduplicates normalized predicates before expanding them.

Transitive path storage made diamond closure unbounded

The first reopened design froze every direct and transitive declaration path. A layered diamond contains exponentially many paths but only linearly many distinct predicates, and invalid cyclic input reached that representation before validation rejected it. Checking also deduplicated only after expanding every path.

The declaration graph now stores direct adjacency only. Member inheritance uses a visited set, and checking expands a deterministic predicate-keyed worklist. Authored root and exact contributing requirement identities remain attached to the first canonical fact without storing path history. A 16-layer diamond regression fixes the bounded behavior.

Editor queries reconstructed recovery phase order

The session hid its recovery enum but exposed one optional getter per phase. The analysis kernel then repeated checked/body/name/declaration fallback ladders for presentation, identity validation, and body facts. Adding a query could therefore reproduce a different phase policy.

The raw getters are removed. Session now publishes complete-program, typed-body, lexical-name, typed-interruption, and exact repair capability views. Analysis consumes those contracts and has no phase-order branch. Shared presentation consumes a graph, type store, and optional typed body rather than separate checked and recovery renderers.

Signature help accepted invalid optional evidence

Static signature rendering accepted an optional capability record even though only structural dispatch required it. A missing or non-callable record silently removed signature help.

The renderer now accepts an exclusive callable-declaration or callable-contract source. Structural dispatch must resolve callable capability evidence and reports a semantic integrity error when the identity or predicate is inconsistent; interface-method dispatch no longer performs an unused evidence lookup.

Expansion could be selected but not used as implementation proof

Implementation validation had explicit proof branches for equality, ordering, index, and coercion, but expansion fell through to an interface-only prover that always returned false. The common instance-operation proof authority now selects exact expansion candidates and compares their result type. A source-defined expansion can therefore prove an expansion prerequisite without a special interface path.

Evidence ownership was coupled to body assumption storage

The initial correction placed evidence inside BodyAssumptionTable, forcing program-wide analyses to know a lexical-body table's internal role. CapabilityEvidenceTable is now an independent immutable ProgramEnvironment authority. Body assumptions retain only body-to-fact membership; checking descendants receive the evidence contract directly.

Retained Phase 0 Outcomes

• Structural requirements use semantic type identities, including contextual interface Self.
• Generic-subject prerequisites are implication edges but do not contribute inherited members.
• Inherited associated bindings retain their original declaration identity.
• Every explicit implementation proves specialized direct and transitive prerequisites; no prerequisite creates an implicit implementation fact.
• ExactSizeIterator declares Self impl Iterator, while concrete iterators still explicitly implement both interfaces.

Full-Range Boundary Assessment

• Parsing and lowering record authored predicates and do not infer prerequisites from member names.
• InterfaceCapabilityGraph is the sole accepted topology/member authority. Checking consumes its direct edges through a bounded worklist; later compiler layers do not traverse interface declarations to reconstruct them.
• Declaration proof and body dispatch evidence are distinct types. No evidence-related expect, panic, compatibility wrapper, or optional state remains.
• CapabilityEvidenceTable is the sole authority for exact structural runtime meaning. Target, provenance, loans, and LSP consume only its contract.
• Target specialization selects concrete operations once. MIR and machine lowering receive closed target plans and contain no requirement-kind reconstruction path.
• Source projection consumes exact semantic origins but cannot affect capability selection.
• The compiler-wide search found no remaining duplicate prerequisite selector, recovery-phase ladder, reverse dependency, stale root reinterpretation, or unchecked evidence obligation with current practical impact.

No unresolved correctness or responsibility-boundary finding remains in Phase 0 or in the reviewed compiler range.

Verification

Focused regression coverage now includes:

• entailed callable signature help;
• missing structural-signature capability evidence as an integrity failure;
• entailed expansion through provenance and loan analysis;
• entailed structural equality through concrete target specialization;
• expansion as explicit implementation proof;
• generic-subject prerequisite-cycle rejection;
• bounded layered-diamond prerequisite closure;
• proof-context coercion validation without panic;
• direct/transitive generic substitution, inherited methods and associated bindings, member collisions, unsatisfied implementations, and definition navigation.

The completed tree passes the complete workspace all-target test suite with one intentional ignored test, warnings-denied workspace all-target Clippy, formatter checks, generated documentation, and repository diff integrity checks.