prototype-baseline-regression-recovery
Work Items
- Restore the full canonical test-all run to green by case identity: every applicable suite passes with zero failures, observed skips, declared ignores, doctest ignores, disposition inventory, LCFails, RC leak tests, RC leaked allocations, process leak tests, or infrastructure failures; explain every changed case. Cluster every red case deterministically by failure signature (error code, failing phase, diverging executor, suspected producer symbol), localize the dominant family to its shared producer via an evaluator-oracle diff, and repair it there under strict artifact/oracle validation with at least one positive and one negative pin per family — never mask a red case via
#skip,#[ignore], a gate, or an early return. After each producer fix, re-run progressively broader suites and track the terminal family-failure total; if three consecutive producer fixes fail to strictly decrease it (a fix relocates or re-fragments failures instead of shrinking them), treat the families as entangled and Mikado-reorder — revert the interfering fix, ship the upstream leaf producer first, then reapply — rather than continuing to patch symptoms. Keep performance promotion plus VM semantic expansion suspended until the terminal structured test-all summary proves the gate by case identity.
Recovery Method
Use content/reviews/claude_review_1.md plus the latest canonical structured test-all result as the failure inventory. Repair one dominant semantic family at its shared producer, retain strict artifact/oracle validation, add receiver/type/control-flow-negative pins, and rerun progressively broader existing suites. Do not resume VM optimization, benchmarking, JIT promotion, or new semantic coverage until the canonical test-all run is fully green by case identity.
The recovery obeys these producer-locus and validation-invariant decision rules:
- Producer locus is the frontend/realization seam, never the backend. The shared producer for the missing-callee, duplicate-parent, and operator-target families is the census/inventory rewrite in
oric::realization(CallableCensusBuilderincallable_census.rs,MonoFunctionInventoryinmono_inventory.rs) or theori_canon/ori_typesfrontend that feeds it — never an LLVM/AOT backend patch. Fix the census fixed-point; its whole-program mono-item census/dedup shape is the rustc-partitioning reference to read before designing it, but Ori keeps one closed batch (no incremental-CGU constraint) and validates coherence-checked derived identity before freezing an immutable presorted artifact. - Generated bodies must not resolve back to the backend-local derive path.
derive_codegen(ori_llvm) andprocess_derives/DefaultFieldTypeRegistry(ori_eval) are dead-ends kept alive only until parity; a generatedEq/Clonefamily that lowers toType$eq/eq$derived$Nre-derives frontend meaning in the backend (LEAK:frontend-reimplementation/backend-ownership-calculus-fork). IR-level negative pins reject any reference from a shared generated family to those legacy derived symbols, and the derive paths are deleted only after shared-form struct/sum/nested/generic/managed-value parity passes. ExecutableProgramschema changes are a cross-cutting contract, not a private edit. The schema-v9 changes this recovery landed (FunctionIdfreeze after body-sort,ProjectionFacts/FunctionFamilyTopologysidecar) are inherited by every consumer of that contract —backend-boundary,native-backend,aims-provenance-ledger,repr-opt,semantic-optimization-pipeline, and the in-progressenum-layout-ssot. Plan-boundaries are impl-boundaries: coordinate any furtherExecutableProgramschema change with those owners rather than editing it locally.- AIMS demand / scalar-projection edits are calculus-first and identity-preserving. Any change to demand meaning proves in the compiled Lean first and syncs all four AIMS surfaces; the
iter_consumesinward-transfer carrier’s projected-field extension must be an explicit join-semilattice (Absent < Exact(field) < Conflict) with exact Rust/Lean parity because the ad-hocOption<u32>join is non-associative (a known dead-end).resolve_fullymust not erase newtype or method-target identity when callable edges are keyed. Do not weaken TF-14, CN-1, L-9, or the VF-2/VF-3 verifiers to make a family green. - The const-generic-derive gate and the iter-consume double-free are genuine forks, not mechanical repairs. Const-generic derives have no stable pool identity under the current
ImplEntry; production either rejects a const-generic derive at the boundary with an actionable diagnostic or first lands a kinded const impl-pattern carrier — the deleted arity-mismatch fallback stays deleted. The projected-field iter-consume double-free is proof-gated at the shared calculus seam. - Leak-family diagnosis runs under the burden-sole gated probe; a default-path RC count is false-green. For the AOT process-leak and LCFail residual, rank survivor cause-clusters under
ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1— theori-rc-remarks --statscause.lattice_dimnames the calculus dimension to extend, not a per-site RC edit; never cite a plaincargo test/ori buildRC count as a leak verdict. - The intel graph is partial for this terrain — read producer structure from source. Resolved caller/callee adjacency is dark and GDS-derived recon was stale at serve; compensate with full source reads of the producer files, and never treat a dark recon tier or a formal
bugs-for = 0as clean. The open high/criticalcodegen-llvm/runtime-arcbugs this section umbrellas are discovered by title+subsystem, not by a plan-to-code graph link. - Every producer fix carries the monotonic-decrease convergence monitor. Track the terminal family-failure total across fixes; if three consecutive producer fixes fail to strictly decrease it (a fix relocates or re-fragments failures), the single-shared-producer hypothesis is falsified for that family — re-cluster at a finer signature and Mikado-reorder (revert the interfering fix, ship the upstream leaf producer first, reapply) rather than continuing to patch symptoms.
Live Evidence — 2026-07-14
| Recovery family | Owning-seam change | Focused evidence | Promotion state |
|---|---|---|---|
| Type-only modules | Executable root freezing accepts an empty root set only when the module has no functions and no CLI entry; nonempty programs still fail closed. | Type-only library 1/1; imported generic filter 2/2. | Retained for broad verification. |
| Lambda specialization | Removed same-arity concrete-function guessing; detached generic partial-apply slots are tombstoned only after def/use removal is proven. | Multi-instantiation 5/5; higher-order AOT 72/72; imported generic 2/2. | Retained for broad verification. |
| Associated versus free calls | ARC records type-checker-selected method owner/form by stable destination; realization and executable closure validate and project that fact; bound LLVM direct calls consume the exact artifact target rather than selecting a same-spelled method. | Associated-only implementation 6/6 with one intentional ignore; unit factories 3/3; free/method collision 1/1. | Architecture seam demonstrated; remaining runtime/external LLVM dispatch must become exhaustive RuntimeCall projection before production close. |
| Compiler-synthesized method calls | Every compiler-generated method call publishes the same exact receiver/form fact as source method lowering. Missing facts were added for for/for yield iter calls and collection/string-index len calls instead of weakening artifact validation. | Focused list loop, list comprehension, string-index, and AIMS cases pass. | Retained; the producer rule applies to every future synthesized call. |
| External exact calls | The executable freezes external callables in stable artifact order and bound LLVM maps CallableTarget::External to that exact declared import ABI. | Concrete imports 8/8. | Retained; no symbol-spelling fallback. |
AIMS may_deallocate coherence | Post-emission evidence now OR-joins rather than overwrites converged effects, propagates through direct Apply/Invoke edges to an SCC-safe least fixpoint, then recomputes FIP. The oracle remains strict. | 4/4: preexisting truth, real Invoke/unwind, chain plus recursive SCC/order independence, and disconnected false precision. | Dominant 5,042-record family repaired locally; broad AOT and canonical test-all confirmation pending. |
| Registry-owned string runtime identity | ori_registry::MethodRuntime::Str owns the nine admitted string operations; executable realization projects typed identities and no longer classifies them by symbol spelling. | Registry identity 1/1; executable receiver-exact positive/negative surface 1/1. | Retained for broad verification. |
User-defined Drop boundary | The exact language role must prescribe a finalization borrow of self: caller-owned drop glue invokes the body while fields remain live, then walks fields and releases storage. A representative implementation’s raw unrestricted analysis is Owned/Unrestricted/Many; treating that as its external boundary makes the body recursively destroy itself. The type checker now assigns exact ImplMethodId plus ImplMethodRole::UserDrop { logical } at impl registration, realization consumes that role rather than searching for a method spelled drop, and artifact-backed LLVM declaration/binding/emission is ordered so the exact destructor target is bound before any destructor body is emitted. Projection-owned physical symbols prevent inherent/other-trait methods named drop from aliasing the language destructor. | Boundary unit pins 3/3; representative scalar-user-drop AOT compiles and runs under ORI_VERIFY_ARC=1; typed role pins pass in both source orders; all five inherent/other-trait collision and negative end-to-end pins pass. | Not yet promotable: the current access-only receiver clamp leaves locality Unknown and escape/share bits permissive, so it does not discharge CN-8 and is formally unsound. Treat it as scratch code until a compiled Lean finalization-boundary theorem precedes retention and a path-total body validator proves every receiver alias/view is read-only, non-escaping, non-owning, non-consuming, and non-returned. The projection must be idempotent, join-preserving, image-closed across SCC iteration, and validated again after convergence and realization. Invalid or generic-unrealized roles fail closed. Production also moves exact impl identity to the canonical IR, threads it through MonoInstance/MonoFunction, seeds concrete generic destructor specializations from implicit destruction obligations, and removes the remaining positional LLVM impl inventory. |
| Derived callable closure | Accepted derives are registered with invalid bodies and never enter the shared ARC batch; evaluator and LLVM independently synthesize behavior. Direct derived methods therefore lack exact artifact functions, and custom derived to_str can be misclassified as primitive runtime conversion. | DerivedImplId/AcceptedDerivedImpl is now prototyped after validation/coherence. Generic owners use the same Applied(owner, binders) identity as manual impls; method and operator dispatch now share one structural matcher. ori_types is 1,221/0, evaluator nested-generic derive is 10/0, and LLVM advances from poison to the expected missing generated body. | Complete deterministic two-phase Canon body census/synthesis before representation planning and AIMS. VM and LLVM then consume the same functions; backend-local derive dispatch/codegen is retired. |
| Operators and primitive facts | Current operator lowering contradicts the approved semantics: exact Eq/Comparable implementations are not resolved before AIMS, equality and ordering are both treated structurally, and generic extension shorthand can carry Idx::ERROR. Set equality is also absent from the registry primitive table. | Dynamic records isolate compound equality to eleven Set<int> Eq/NotEq primitive sites repeated across 17 tests; six nested-generic derive sites were separately traced to Idx::ERROR results and repaired at generic impl registration. | Make compound OpDefs the semantic registry SSOT, freeze one pre-AIMS operator-resolution fact, and fail poison before classification. Set Eq/NotEq promotion requires both LLVM and VM physical projections from that same fact; no backend may independently decide semantic eligibility. |
| Shorthand field type provenance | Canonical shorthand fields synthesize an Ident with TypeId::ERROR; ARC trusts that poison instead of the already-bound source variable type, so live parameter uses are classified scalar/absent and VF-2 correctly rejects them. Spread-generated shorthand/projections share the latent gap. | Both AbsentParamHasUses families traced to the same producer defect. | Planned immediate repair: source variable is the authoritative ARC type with non-poison agreement validation. Production seam: type checking freezes a substituted typed struct-desugar plan consumed by canonical lowering, with executable closure rejecting concrete ERROR types. |
The latest completed broad AOT measurement was 2,870 passed, 120 failed, and 46 ignored out of 3,036. That run preceded the exact external-call repair, synthesized string-len fact, and correction of one prototype assertion whose expected value (111) disagreed with both its own arithmetic and evaluator result (121), so a fresh 3,036-case sweep is required before attributing aggregate recovery. The remaining failures are concentrated in derived callables, user-defined drop, operator/primitive facts, shorthand type provenance, and a smaller collection/mutation tail. The canonical test-all baseline is not yet restored, so all performance evidence remains suspended.
Canonical run 1784124380846671351-553e68d2 settled with terminal phase failed and overall state infrastructure_failed: the ori_vm and ori_llvm Rust prebuild actions found five test-only ArcFunction literals missing the newly mandatory method_call_facts field. All runnable slices nevertheless settled. LLVM spec is 4,405 passed, 786 failed, 83 skipped, 731 LCFail, 0 leaks in 75.1s—617 passes below and 639 failures above the required baseline. Evaluator is 5,170/44/65, AOT is 2,898/97 with 9 leaks, Rust runtime is 366/0, and doctests are 15 passed plus 65 skipped; aggregate runnable totals are 12,854 passed, 927 failed, 213 skipped, 731 LCFail, and 9 AOT leaks. The run is diagnostic evidence, not a valid gate measurement, until the prebuild exclusions are repaired and a new fully canonical run settles. Exact record inspection corrects the original 147-record label: 134 are operator-resolution-before-specialization failures caused by a forked JIT preparation order, while 13 are true surviving-BoundVar specialization failures. The remaining leverage order is those two producer families; residual callable-signature mismatches (55 + 35 + 9 exact repeats); derived-body closure (clone, debug, hash, compare, default, and eq families); stale or missing primitive facts; then the localized type-check and registry-test defects.
Review Delta — 2026-07-15
The updated third verification pass in content/reviews/claude_review_1.md supersedes the original raw failure classification for live state. It independently verifies the dominant may_deallocate coherence family, operator-call resolution, lambda-specialization seam, the OpDefs 20-byte pin, and registry-owned string runtime identities as fixed in the worktree. It leaves executable body closure for derived methods and residual callable signatures open, and localizes the cross-backend sum_types.ori cluster to unconditional builtin-Error identifier precedence over a user sum variant. It also records C6 (OpStrategy test expects two bytes while the compile-time invariant is one), N1 (the prelude completeness list omits thread_id), and N2 (the no-heap registry lint mistakes ToString/StringConcat/StringEqual identifier substrings for the heap type String). The review’s N3 trace-toggle finding is already obsolete: the temporary ORI_TRACE_DROP_ROLE probes were removed after the exact collision was diagnosed. No fresh canonical test-all exists after these repairs, so none of these focused successes promotes the baseline gate.
The canonical-run prebuild blocker is now repaired at the five exact test fixtures; both ori_vm and ori_llvm library prebuilds complete. The stale OpStrategy byte pin, missing thread_id registry pin, and identifier-substring no-heap scan are repaired with positive and negative registry tests; ori_registry is 331/331. User Error variants now win at the typed identifier seam, while the builtin constructor remains available when unshadowed. Canonical lowering consumes that typed decision rather than classifying by spelling, and ARC builtin-Error construction is gated by the registered Error receiver identity. tests/spec/types/sum_types.ori is 18/18 on interpreter and LLVM; tests/spec/declarations/sum_types.ori is 35/35 on both after the callable fix below. The prior LLVM ICE from sending the user enum through Pool::struct_fields is gone.
Residual callable-signature validation was correct and remains exact. It exposed two producer asymmetries in lambda lowering: parameters were collapsed through resolve_fully, losing the closure’s nominal Named/Applied identity, and targets used the narrower inferred body result instead of the callable’s declared result (for example DoubleEndedIterator<T> under Iterator<T>). Lambda parameters now consume the same body-type substitution seam as their closure, the target result comes from the declared Function child, and the shared post-lowering materializer remains the sole deep Var/BoundVar substitution owner. A unit pin failed on concrete-versus-nominal result and parameter identities before the repair, then passed. Focused LLVM results are declarations/sum_types.ori 35/35, flat_map_with_bool_inner 1/1, and flat_map_str 1/1. Those three canonical failure groups comprise 99 records (python .claude/skills/calc/calc.py '55 + 35 + 9' → 99), but promotion still requires the broad case-identity gate.
The callable recovery also exposed a preparation-order fork that must be removed rather than patched per caller. Current local realization, AOT preparation, and JIT test preparation order mono-target rewriting, lambda specialization, impl lowering/flattening, operator resolution, and impl-target rewriting differently; one path even flattens impl parent/lambda groups before specialization can consume them. Production shape is one backend-neutral grouped ArcBatch: preserve every local/imported/mono/test/impl parent with its lambdas, rewrite mono direct targets, specialize every group, flatten exactly once, resolve typed operator targets over that specialized flat batch, rewrite exact impl targets, then freeze AIMS and the executable artifact. JIT, VM, LLVM, native, compiled WebAssembly, and any JIT tier consume that one preparation result; no backend or command owns a private ordering.
The live seam prototype now represents that transition as consuming LoweredArcBatch::prepare -> PreparedArcBatch, and local realization, AOT, and the LLVM JIT runner all route through it. Impl lowering retains (parent, lambdas) families instead of flattening impl lambdas into ownerless bodies; specialization and target closure therefore see the same complete family inventory on every path. Preparation occurs before rebuilding the resolved-type burden registry, because lambda specialization can append exact compound identities to the realization pool. An automatically resubmitted canonical run captured an intermediate compile-incomplete edit and correctly became stale; after completing the wiring, cargo check -p oric --features llvm and cargo build -p oric --bin ori --features llvm both pass. The full dominant family is now green on LLVM: lambda_mono.ori 17/17, lambdas.ori 30/30, multi_lambda_type_selection.ori 4/4, expressions/syntax.ori 21/21, and lexical/delimiters.ori 57/57—129/129 executable tests, corresponding to all 134 review records when the five file records are included. This is focused recovery evidence, not baseline promotion.
That five-file run repeatedly emitted ori_repr::range::signatures: SCC budget exhausted — remaining functions get Top, with 68–130 remaining SCCs depending on the unit. The warning is not the AIMS ParamContract height issue and must not be conflated with it. It independently shows that the representation-range fixed-point budget is not scaling to combined lambda-heavy units, loses precision by forcing Top, and floods one warning per affected analysis invocation. Diagnose its convergence carrier/bound and make the diagnostic once-per-unit plus actionable; do not silence it or raise a magic constant.
The range warning’s exact cause is now proven and repaired: the former max_total_scc_iterations = 50 counted every acyclic SCC as an iteration, so ordinary program size—not convergence—silently skipped every component after the fiftieth. The global field and its API pin are removed. Every acyclic SCC is processed exactly once; only a genuinely recursive SCC consumes max_scc_iterations; exhausted recursive summaries are reset to Top and cannot be resurrected by return feedback; one aggregate warning names the optimization-only consequence plus ORI_LOG=ori_repr::range::signatures=debug and --no-repr-opt actions. Call-site collection now consumes the shared CallGraph::callers_of index rather than rescanning every unrelated function. New pins cover 129 acyclic functions beyond the former cutoff, per-SCC recursive exhaustion, acyclic precision after an unrelated exhausted SCC, and feedback non-resurrection; all pass in the 741-test ori_repr run. The combined five-file LLVM suite passed 129/129 with the former 68–130-warning flood absent.
The production form is stricter than merely sharing an ordering helper. Input families are canonicalized before any pool mutation; duplicate parent or child identities fail before mutation; post-specialization identities are validated again; one deterministic flat body vector plus names-only family topology replaces grouped/flat dual body authority; exact mono lookup rejects conflicting instance/signature mappings instead of hash-map overwrite/first-match behavior; and ArcProgramRealizationInput accepts the prepared type-state rather than a caller-assembled raw function vector. The topology is frozen only after multi-instantiation, becomes part of the validated executable artifact, and is the sole shape input for LLVM parent/lambda/test/impl projection. Roots remain parents only. Physical backends never receive a pre-AIMS batch, and the shared artifact pool—not clone pointer identity—is authoritative. The quick adapter may privately reconstruct LLVM’s legacy grouped cache from artifact bodies plus topology, but that cache is not a semantic authority and must disappear when artifact-native preparation covers tests and impls.
That topology seam is now realized in the prototype rather than remaining architectural prose. PreparedArcBatch consumes each deterministic parent/lambda group into one flat body vector plus FunctionFamilyTopology; no grouped accessor, mutable grouped cache, or physical into_groups escape remains. ExecutableProgram schema version 9 freezes names to stable FunctionIds after body sorting, preserves producer lambda order, requires every body to occupy exactly one family position, rejects unknown/duplicate/uncovered members, and forbids a lambda as a program root. ArcProgramRealizationInput accepts only the prepared type-state. LLVM top-level, imported, monomorphized, test, and impl preparation clones exact artifact families; Canon and pre-AIMS caches are no longer fallback authorities. The JIT evaluator also takes its pool from the bound artifact and no longer retains a second pool identity. ARC text and DOT dumps render the already-realized artifact instead of cloning bodies and running AIMS a second time. Focused construction evidence is ori_repr 741 passed, 0 failed, 7 ignored; cargo check -p oric --features llvm and the LLVM-enabled ori binary build pass. poly_lambda_with_imported_generic.ori passed 10/10 and lambda_with_empty_literal_generalized.ori passed 1/1, so the 11/11 generalized-BoundVar probe no longer reaches the former physical re-lowering failure. The broader combined lambda suite passed 129/129.
Snapshot run 1784129419630066069-5415c1be completed all 13 LLVM slices at 4,590 passed, 601 failed, 83 skipped, 536 LCFail, 0 leaks, then failed the whole-run prebuild on the already-removed ori_repr test variable captured by that stale snapshot. It is therefore a complete LLVM failure census but not a canonical promotion result. The pass gap is 432 and the LCFail excess is 444; 469 LCFail identities are new while 25 former baseline LCFail identities no longer fail (python .claude/skills/calc/calc.py '[5022-4590, 536-92, 536-67, 92-67, 291+84+6]' -> [432, 444, 469, 25, 381]). Exact clustering assigns the new artifact-construction regressions to 291 missing realized derived/core callees, 84 duplicate mono parents, and six missing closure-ABI targets: 381 tests before file-record duplication. A newer isolated snapshot is running against the repaired prebuild/topology/range tree, but its 11:43 snapshot predates the mono-inventory and primitive-fact repairs below. It provides the stable pre-repair anchor, not validation of those edits; one further canonical run is required after they are focused-green.
The 84 duplicate-parent failures exposed an ownership ambiguity before the strict family seam rather than a reason to weaken it. A new checked MonoFunctionInventory now binds every final mono identity to one source namespace before lowering. Imported source bodies own only collector records explicitly marked imported and carrying compatible exact metadata; dispatch IDs merge into that survivor. Same-origin duplicates, genuinely local/imported source collisions, conflicting signatures/substitutions, and imported metadata without a source body fail closed with the readable callable name and ORI_LOG=oric::realization::mono_inventory=debug. JIT and AOT both lower only local_bodies() and use the same unique all() inventory for target rewrite/declaration. Positive, negative, and actionable-diagnostic unit pins are present; focused validation waits for the isolated pre-repair snapshot to release the Cargo lane.
The 48 stale primitive-fact failures have a separate mechanical cause: dead-block compaction removed PrimOp definitions while retaining facts keyed to those removed SSA destinations. Frozen semantic classification remains immutable. The structural block transform now retires only facts whose defining destinations disappeared, preserves every surviving fact byte-for-byte, and validates exact coverage immediately after block merging. A dead-block pin freezes a valid primitive fact, compacts its instruction, and requires an empty valid table. The remaining typed-descriptor failures are not folded into this repair; their distinct registry/type-provenance root remains under investigation.
Snapshot run 1784131092643648741-79b3f92e is the first complete, source-stable measurement of the mono-inventory plus primitive-retirement wave: 22,960 passed, 694 failed, 213 skipped, 488 LCFail, and 9 AOT process leaks overall; LLVM spec is 4,638 passed, 553 failed, 83 skipped, 488 LCFail, 0 RC leaks. Relative to the 4,590/601/536 anchor, primitive retirement recovered exactly 48 passes and removed exactly 48 failures/LCFails; stale frozen primitive facts are now zero. The remaining 488 LLVM LCFails partition exhaustively into 302 missing realized callees, 84 duplicate parents, 27 missing typed primitive descriptors, 28 unsupported structural physical projections, 17 type-error-blocked cases, 10 unresolved to_str, eight wrong-layout extracts, six missing closure-ABI targets, three generic-codegen cases, two LLVM call-parameter mismatches, and one flatten/Never failure. The mono inventory did not change the 84 duplicate-parent cases and introduced one red diagnostic assertion, so it is not promoted and must be corrected or replaced before the next canonical run.
The 27 typed-descriptor records are two causes, not one registry list. Seventeen repeated compound_equals.ori tests arise from eleven Set<int> Eq/NotEq sites: TypeTag::Set has no canonical compound equality strategy. Merely adding Set to ori_types’ handwritten structural list is forbidden because LLVM has no Set arm in structural element equality and the VM currently rejects all structural equality/ordering facts. The vertical repair makes registry OpDefs authoritative for compound operator semantics, removes the type-checker list, and adds total LLVM and VM physical Set-equality realizations—order-independent, length-checked, and using the registry-selected element equality/hash semantics—from one frozen fact. The other ten records in derive_nested_generic_enum.ori came from six Idx::ERROR receivers: derived generic impls used bare Named(owner) while concrete calls used Applied(owner, args). The prototype now records Applied(owner, Named(binders)) consistently in the impl, signature, accepted-derived fact, supertrait check, and coherence key, deletes the operator-only positional-zip workaround, and pins same-head bare/applied rejection plus arity drift. The file now passes evaluator 10/0 and reaches LLVM executable closure, where it correctly exposes the next shared-body blocker (clone has no realized function body) instead of failing primitive classification.
That generic-self repair is deliberately type-binder-only. Const-generic derives cannot be represented soundly by the current ImplEntry: declaration registration drops const binders, ParsedType::ConstExpr has no stable pool identity, and the old arity-mismatch fallback returned an empty substitution that silently skipped bounds. Keep that fallback deleted. Production must either reject a const-generic derive before publishing AcceptedDerivedImpl, with a specific actionable diagnostic, or first add a kinded type/const impl-pattern carrier plus const metadata, matching, substitution, coherence, and mono identity. Coherence also needs alpha-equivalent binder identity: Box<T> and impl<U> Box<U>: Eq are the same pattern even though exact pool indices differ. Canonical binder ordinals/kinds, or an alpha-equivalent pattern comparison, must decide override/duplication before generated bodies are admitted.
The derived-callable closure now has an explicit production architecture rather than a generic “synthesize before AIMS” instruction. Type checking mints a stable DerivedImplId and publishes one AcceptedDerivedImpl only after derive validation and coherence registration succeed; rejected, duplicate, or shadowed derives publish no fact. That fact owns the exact receiver, trait identity, method identity, generic bounds, signature, and source span. ori_canon::lower_module consumes only those accepted facts plus typed TypeEntry shape—never raw Module.types[*].derives—and creates one ordinary generated body template per accepted fact before Lowerer::finish. The leaf ori_ir::CanonResult cannot own ori_types::FunctionSig or Idx without creating a crate cycle; it instead freezes a joinable generated-root projection carrying DerivedImplId, owner/method names, parameter names, body CanId, and generated-root origin. Realization joins that ID exactly once to TypedModule.accepted_derives, rejects absent or duplicate joins, and retains the accepted fact as the sole signature/type authority. Concrete non-generic and reachable generic instances then lower through the ordinary Canon-to-ARC path into ArcFunctionGroup families before the single LoweredArcBatch::prepare, representation planning, AIMS, and executable closure. Generated field calls retain exact method-owner facts; Clone emits no hand-authored RC, and AIMS remains the only ownership calculus. Artifact validation requires every derived target to resolve to CallableTarget::Function, every generated body to occupy exactly one family, and every type to be concrete. Evaluator registration consumes the same generated Canon roots as ordinary user methods; after parity pins pass, evaluator process_derives/DefaultFieldTypeRegistry and LLVM derive_codegen/mono-derived fallback are deleted. The first-class builtin Error constructor can later use the same generated-root inventory under a distinct Builtin(ErrorConstructor) origin, but is not conflated with derive synthesis.
Generic closure is frontend-seeded, not discovered by a physical backend scanning its pool. The callable-selection/mono carrier must identify the selected template (Function, source Impl, or Derived(DerivedImplId)); a deterministic worklist then closes nested derived dependencies and deduplicates by derived identity plus concrete semantic receiver. Newtype identity must not be erased through resolve_fully when method targets are keyed. Hashable promotion is additionally blocked on one spec-pinned seed/tag-fold definition because the current evaluator and LLVM enum hashing disagree. Until the Canon generator is complete, a direct-ARC bridge may generate a small recovery slice using only ordinary Project/Construct/Apply/control-flow operations, zero manual RC, and insertion before the same AIMS batch. That bridge is prototype evidence only: it may measure recovery and exercise the calculus seam, but it cannot replace the shared Canon body or justify deleting either existing semantic interpreter.
The first dynamic generic-closure trace confirms that the frontend carrier already exists and is correctly receiver-specific. derive_nested_generic_enum.ori publishes four method instances—two concrete clone receivers and two concrete hash receivers—with impl arguments, concrete receiver types, and body substitution maps. collect_mono_functions then rejects all four solely because its method signature inventory consults source ImplSig and has no AcceptedDerivedImpl input (impl_sig_keys=0); executable closure consequently sees the original bare clone. The recovery prototype therefore extends the neutral mono inventory with an explicit Source | Derived(DerivedImplId) body origin, selects accepted-derived signatures only after ordinary source impl lookup, keeps the existing MonoInstanceId -> mangled target rewrite, and generates the Clone identity body under that exact concrete signature. This is a producer-seam experiment, not pool scanning or a physical-backend fallback. Its first correctness hypothesis is Ori-specific: for an immutable/COW value, derived Clone can be an ownership-credit alias of self rather than a field-by-field rebuild. The generated Arc body contains only Return(self); AIMS must infer every retain/release and the existing LLVM/VM projections must preserve value independence and leak freedom. Existing nested/fat/COW clone fixtures decide whether that stronger design survives.
That carrier and the first shared generated body now execute end to end. MonoFunctionOrigin::Derived(DerivedImplId) joins a concrete mono instance to exactly one accepted derive; ordinary source impls retain precedence. Non-generic and concrete generic Clone bodies use the same checked ori_arc identity constructor, contain zero hand-authored ownership instructions, and enter the ordinary grouped preparation, representation, AIMS, and executable-validation path. ori_repr is 742 passed, 0 failed, 7 ignored and the focused constructor pins are 7/7. LLVM no longer scans Canon/mono inputs to rediscover these bodies: one generic artifact-family declaration pass selects only parent families left unclaimed by source/import/mono roles, explicitly defers qualified impl and test-wrapper roles, derives each physical ABI directly from the frozen function contract and realized parameter shape, and hands the exact stable executable FunctionId inventory to preparation. A predeclared role is checked against the same projected physical ABI; lambdas remain owned by their parent family. This declaration occurs before impl emission, so impl-to-generated calls are forward-declarable. With ORI_VERIFY_ARC=1, tests/spec/traits/derive/clone.ori is now 7 passed, 0 failed on LLVM, matching evaluator behavior and replacing the prior fourteen unresolved clone$derived$N codegen errors. This proves callable closure for the non-generic Clone slice only; generic Clone, AOT execution/leaks, nested COW independence, and the canonical baseline remain mandatory gates.
The focused artifact and ABI layer is now independently pinned: the checked shared ABI constructor projects both ordinary and artifact-only parents; mixed source/generated/lambda/impl/test role selection returns only the one unclaimed generated parent; and parameter type, passing mode, readonly status, return type, and return passing mismatches all fail closed. cargo check -p oric --features llvm, the 13-test shared derived-body constructor slice, and the nine-test artifact-projection slice pass. The LLVM test runner also preserves the typed is_main role when a module combines @main with tests, rather than inferring entry status from the absence of a process wrapper. Exact bound Function/External calls no longer fall through to spelling-based runtime/builtin dispatch after declaration failure; Apply and Invoke now report that the artifact target was not declared and give the ORI_VERIFY_ARC=1 reproduction action instead of suggesting a missing mono instance.
The direct-ARC Eq experiment separates callable-closure success from semantic-seam success. A checked two-parameter constructor produces one typed PrimOp(Eq), no manual ownership events, and a bool result; all 13 constructor pins pass. Verified LLVM execution passes the struct spec 21/21, the heterogeneous-sum spec 16/16 including an explicit .eq call, and Clone 7/7. Native AOT passes both Clone fixtures 2/2 and twelve Eq fixtures 12/12 under the harness’s always-on ORI_CHECK_LEAKS=1. However, an LLVM IR trace proves that operators still call backend-local Type$eq functions directly and the new eq$derived$N artifact lowers its PrimOp(Eq) to a call to that same backend-local function. The experiment therefore proves accepted-derive identity, artifact family closure, ABI projection, AIMS traversal, execution parity, and leak freedom for the wrapper, but it does not yet prove backend-neutral Eq semantics and is not promotable as production architecture.
The next prototype gate is structural-semantic independence. A generated derived body must not resolve any operation back to the backend-local derive implementation for the same trait. The preferred production form is ordinary shared Canon/ARC control and data flow over the accepted typed shape: field projections and short-circuit Eq calls for products, tag discrimination plus per-variant payload projections for sums, and exact concrete substitutions for generic instances. If a dedicated structural semantic operation is temporarily needed, it must be a typed frozen logical fact with total evaluator, VM, and LLVM projections and no spelling or pool-shape rediscovery in a physical backend; it cannot merely wrap derive_codegen. IR-level negative pins must reject references from a shared generated family to legacy derived symbols. Only after the shared form passes struct/sum/nested/generic/managed-value parity and leak tests may the corresponding evaluator and LLVM derive paths be deleted. Performance work remains suspended until this seam and the canonical baseline are both recovered.
Production removes the temporary notion of a backend “remainder.” ExecutableProgram must freeze a physical-role projection table for every parent (Internal, exported source symbol, qualified impl symbol, test body/wrapper, entry point, or external linkage), with one stable artifact identity and no spelling-based role inference. LLVM then performs a single declare-all pass over that table, followed by a single prepare-all/emit batch; impls and generated bodies no longer have separate immediate-emission paths. The current explicit deferred-role list is a bounded migration adapter demonstrating the correct ABI/body authority and forward-declaration ordering, not the final inventory API. Compiled native and compiled WebAssembly consume the same role-neutral body/AIMS identities and select only target-specific symbols and ABIs through validated physical plans.
After strengthening the generic-owner pin to require exact Applied(owner, [Named(T)]) arguments, declaration-template type_params, exact self-bearing parameter/return identities, and both integer and string instantiations, the full ori_types library suite is 1,223 passed, 0 failed. This supersedes the earlier 1,221-test focused count and closes only registration/dispatch identity; it does not promote executable-body closure.
Generic Default makes the concrete-instance carrier mandatory for evaluator parity, not merely an optimization. A receiver-driven generic derive can recover its concrete owner from the runtime receiver, but Pair<int>.default() has no receiver; the current evaluator has neither the shared Pool nor a typed TypeRef, which is why its DefaultFieldTypeRegistry guesses from parsed names. Every concrete generated instance therefore needs an exact identity plus substitution attached to source and synthetic canonical call sites. Eval must either interpret the one generated template under a frozen read-only type substitution or consume a mechanically specialized Canon root; nested defaults receive exact generated/runtime targets. Name-only lookup and parsed-type reconstruction are prohibited.
The remaining post-artifact LLVM ownership decisions collapse into three shared authorities. ExecutableOwnershipPlan owns exact typed runtime call-site dispositions and guarded logical retain/release actions, reusing CallSite and RetainPlanId; ExecutableDropPlanTable is one closed transitive graph for type, closure-environment, runtime-state, partial-field, and variant cleanup, with child DropPlanId edges plus exact user-drop bindings; strengthened FunctionEffectFacts.may_throw is the sole function/drop-plan unwind fixed point. Runtime-call identity must move before AIMS so these plans are calculus inputs rather than LLVM discoveries. Borrowed iterator roots, join yielded-element ownership, returned mutation-receiver lineage, Option/Result/list/map adapter retains, and early-drop releases become exact per-site logical facts. Logical plans contain no offsets, tags, headers, helper symbols, counter mechanics, ABI, or atomicity; CompiledLayoutPlan and PhysicalVmPlan each provide total validated realizations keyed by the same fact IDs. LLVM pool/tag walks, provenance scans, inline adapter RC, and nounwind inference are shadow-compared during migration, then deleted with static seam pins.
The post-topology residual audit also prevents a false architecture-complete claim. LLVM still re-derives logical borrowed-root/iterator ownership, join-element release, returned-receiver lineage, child drop/retain topology, inline builtin adapter RC actions, and nounwind/drop-effect policy from ARC shape, pool tags, and names after artifact closure. Direct LLVM derive and Error constructor synthesis still bypass shared ARC/AIMS and emit local RC behavior. Production closure requires stable per-function/per-callsite logical carriers and generated semantic bodies in ExecutableProgram; CompiledLayoutPlan(TargetSpec) may then select only storage, ABI, helper, counter/header, atomicity, and instruction details. Dormant/test-only Canon and ARC-cache APIs do not count as production consumers, but must be removed or test-scoped so the boundary is mechanically enforceable.
The review’s remaining proof/checker obligations stay part of production acceptance rather than deferred cleanup: falsifiable RL-14a/RL-15 checker witnesses, the RL-15a TF-13/CN-8 composed discharge, rejecting lifetime/visibility/unwind fixtures, and a concrete validated physical plan are required before the VM architecture can claim calculus conformance. The open VM shift/float/catch parity rows, LLVM memory-effect overclaim/test-only fork, and generic user-Drop realization remain explicit correctness blockers after baseline recovery.
The finalization-boundary proof reconnaissance exposed a pre-existing Rust/Lean carrier mismatch that must be repaired at the shared calculus seam. Rust joins iter_consumes_projected_field: Option<u32> with None both as the optimistic/no-claim identity and as the poison produced by disagreeing exact fields. That operation is non-associative: (Exact(1) ⊔ Exact(2)) ⊔ Exact(2) = Exact(2), while Exact(1) ⊔ (Exact(2) ⊔ Exact(2)) = None. The compiled Lean ParamContract omits this and other newer Rust facets while the IC-3 surface claims full associativity and SCC fold-order independence; the SCC driver also hard-codes a stale height of 17 instead of deriving rank from the carrier SSOT. Production repair requires an explicit join-semilattice carrier (Absent < Exact(field) < Conflict), exact Rust/Lean field parity, property pins for commutativity/associativity/idempotence/monotonicity, and then the UserDrop projection proof over that corrected product. No VM or LLVM optimization may rely on the current field join as an order-independent fact.
UserDrop admission must be a type-state seam, not a boolean attached to signature validation: role/signature validation freezes exact identity, typed primitive facts freeze next, a path-total body validator upgrades the boundary to body-admitted, and only that admitted state exposes receiver contract projection before SCC analysis. Reuse the existing interprocedural alias-to-parameter map plus intraprocedural project-alias table; do not add a third alias calculus. The conservative first implementation rejects receiver/view forwarding to local or indirect calls, return/store/capture, owned calls, credit creation or discharge, release/drop, COW mutation, reuse, and iterator consumption; post-realization validation recomputes the receiver/view closure and rejects every RC/burden event or mutation/reuse sink. Nonrecursive extraction, recursive SCC iteration, and TRMC refresh must consume one centralized join-then-project operation. The distinct FinalizationBorrow capability is non-transferable and creates no owner credit while the physical count is zero; exact normal and unwind sequencing is user body, reverse-declaration child walk, then exactly-once storage reclaim. The contradictory field-before-destructor text in 08-types.md must be reconciled with 21-memory-model.md, Annex E, and current glue before RL-DROP is promoted.
Structural Eq and AIMS Demand Evidence - 2026-07-15
-
The sixth review pass independently accepts the generated-body architecture:
AcceptedDerivedImplis the typed authority,MonoFunctionOrigin::Derivedpreserves concrete identity, generated bodies enter the ordinary ARC/AIMS batch, and VM/LLVM consume the sameExecutableProgramfamily. -
The initial Eq wrapper is rejected as semantic-seam evidence. Its generated body called LLVM’s existing derived
Type$eq, so it proved artifact closure and ABI projection only. -
The replacement generated Eq body uses shared field projections, short-circuit control flow, primitive equality for registry-admitted leaves, and exact method-call facts for user fields. It contains no hand-authored ownership events.
-
Verified struct and sum execution reached 21/21 and 16/16 respectively before the AIMS checker found a real coherence defect. These counts remain focused evidence only.
-
Annex E IA-5, TF-11, and TF-14 require independent cardinality and consumption. The shortcut that reconstructed consumption from cardinality is rejected because
Many + Affineis valid. -
BackwardDemandnow carries both dimensions. Direct uses contributeOnce + Linear; one live projection contributesOnce + Affine; repeated use of one projected view producesMany + Affine; two projection instructions produceMany + Unrestricted. -
IA-5 step (1) transfers full demand through
Letand bothSelectoperands, transfersProjectcardinality/locality plus one Affine consumption, promotes aggregate-builder arguments to Owned while transferring destination locality, and promotes aSetvalue to Owned with base locality. VF-3 remains independently derived. -
The existing cross-block
project_alias_sourcesconsumer used latticejoin; TF-14 requires sequential cardinality composition plus one Affine projection demand. The prototype now applies the exact mutation instead of weakening the verifier. -
Compiled Lean currently maps the whole IA-5 step-one artifact to the Project-only
TF14_propagation_spec. Before production promotion, add a compiledia5Step1theorem covering Let, Project, Select, all aggregate builders, Set, and the non-aliasing cases; the Rust checker enumeration is not a substitute for the calculus authority. -
The fieldwise sum prototype exposed a separate semantic-IR blocker:
ArcInstr::Project { field }cannot distinguish two variants that share field ordinal and type. A physical backend must not guess a payload offset from layout coincidence. -
Production projection identity must distinguish struct field, tuple element, sum tag, and sum payload
{ variant, field }before physical layout. AIMS consumes only the shared borrow identity;PhysicalVmPlanandCompiledLayoutPlan(TargetSpec)independently map that identity to offsets/tags and validate total coverage. -
Live inventory selects a destination-keyed
ProjectionFactssidecar onArcFunctionas the smallest production-shaped carrier:ProductField { field },SumTag, orSumPayload { variant, field }. It preserves the existing logicalProjectinstruction and AIMS borrow rule while making declaration-level identity mandatory before backend selection. LLVM must delete its current first-variant(field ordinal, resolved type)guess and fallback offset; VM validates the fact and may erase variant identity only when mapping to its active-payload representation. Artifact validation rejects missing/orphaned facts, raw-field disagreement, wrong base shape, invalid variant/field, and result-type mismatch; block transforms retire destination facts; serialization and executable identity include the sidecar. -
The current
field + 1sum-layout adapter is scratch evidence and cannot be promoted. Add an ambiguous multi-variant payload matrix whose field ordinals and types collide; require evaluator, VM, LLVM debug/release, native AOT, and compiled WebAssembly parity from the same semantic projection facts. -
The ambiguous-layout pin uses variants whose payload field 1 has the same
booltype but different preceding physical widths (for exampleNarrow(prefix: int, flag: bool)versusWide(prefix: (int, int), flag: bool)). Declaration order must not affect generated facts, LLVM offsets, VM active-payload indexing, equality results, serialization identity, or malformed-fact rejection. -
The updated review also records open implementation-hygiene gates in this wave: split generated Clone/Eq production modules and tests, remove duplicate fact-freezing skeletons, replace fail-open
debug_assert!invariants, and close the reviewed proof/checker and VM parity findings before branch acceptance. -
Canonical snapshot test-all remains the only baseline verdict. The active snapshot predates this demand repair, and performance/JIT promotion remains suspended until a later source-stable terminal run meets the exact pre-VM case-identity and leak gates.
-
Snapshot
1784137415119337228-7f9c51c2reached terminal phasecompletewith overall statefailed: 23,014 passed, 671 failed, 213 skipped, 463 LCFail, and 9 AOT process leaks. LLVM spec is 4,644 passed, 548 failed, 83 skipped, 463 LCFail, and 0 RC leaks; evaluator is 5,189/26/65; AOT is 2,921/74 with nine process leaks; Rust workspace is 9,247/15; Rust LLVM is 632/8; runtime is 366/0; doctests are 15 passed plus 65 skipped. The run predates the explicit two-dimensional IA-5 demand repair, so it is a diagnostic anchor rather than promotion evidence. -
Canonical generation
1784152040048560798-895db0cereached a source-stable terminalfailedverdict after the repaired runtime automatically replaced stale generation1784150161933278400-8ed134fa: 23,063 passed, 676 failed, 213 skipped, 463 LCFail, and 9 AOT process leaks. Relative to snapshot G this is +49 passes but +5 failures. LLVM spec is 4,646 passed, 548 failed, 83 skipped, 463 LCFail, and 0 RC leaks (+2 passes, failures unchanged); evaluator is 5,189/28/65 (two new failures); AOT is 2,924/73 with nine process leaks (+3 passes, one fewer failure); Rust workspace is 9,291/19 (+44 passes, four new failures); Rust LLVM is 632/8; runtime is 366/0; doctests are 15 passed plus 65 skipped. The exact baseline gate remains missed by 376 LLVM passes, 401 LLVM failures, 371 LCFail cases, and nine process leaks; performance/JIT promotion remains frozen. -
Canonical validation first exposed test-all storage exhaustion rather than a compiler deadlock: runtime-owned stores had retained about 207 GiB because terminal Cargo targets stayed inside evidence bundles and read-only AOT snapshots made quarantine expiry fail. The runtime now removes terminal
work/caches; protects current/completion/live evidence; intersects count, age, and allocated-byte budgets as one newest prefix; and maintains the store before admission.A physically allocated 64 KiB reserve plus bounded emergency journal survives report-time ENOSPC, while a missing reserve on an already-full filesystem bootstraps only from reconstructible terminal cache, expired quarantine, then unprotected expired terminal evidence. Cleanup enumerates persisted worker, slot, action, and process-group identities even after a group leader exits; action identity writes and direct/queued supervisor activation are failure-atomic behind durable reservations and deferred-start gates; one proven-dead supervisor may be repaired, while a second death or unproved cleanup fails closed and blocks FIFO promotion.
The live store is 567 MiB with 231 GiB free, the canonical current/completion pointers still name
1784152040048560798-895db0ce, and the reserve is physically present at mode 0600. Verification is 54/54 focused retention/process/activation tests, 44/44 autonomous/status/supervisor tests, the runtime self-test, compile check, diff check, and a clean live GC.This infrastructure repair makes the canonical delta trustworthy but does not promote compiler parity.
-
The compiled Lean gap is now closed for IA-5 step (1).
IA5Step1Instr, backend-neutral operand carriers,ia5Step1, an independent conformance relation, exhaustiveIA5_step1_sound, per-case lemmas, and negative witnesses cover Let, Project, both Select identities, every aggregate-builder kind, Set, SetTag, and non-aliasing cases. IA-5 now maps directly to this theorem rather than the Project-only TF-14 theorem. Focused and fulllake build, placeholder lint, generated-map equality, statement parity (130 checked/53 classified), and the affected proof checker are green; full dual discharge and canonical test-all remain open. -
The independent VF-3 demand oracle now retains cardinality and consumption as an exact two-dimensional
DemandShapethrough sequential endpoint composition. It proves that a dead Project alone observes asAbsent + Dead, while the same unconditional TF-14 Affine contribution composed with an independentOnce + Linearsource use observes asOnce + Unrestricted; alternative paths canonicalize independently before their join. -
Focused Rust evidence exposed a production-ordering mismatch rather than an oracle defect. Transfer tests are 66/66, but intraprocedural tests are 240/241: immediate CN-1 canonicalization can erase a dead Project’s raw Affine contribution before an earlier source-order direct/alias use is encountered by the backward walk, making the result instruction-order-dependent. Annex E simultaneously requires canonicalization after every transfer and exact unconditional TF-14 composition. Do not weaken TF-14, CN-1, or the verifier.
-
Three independent consultations converge on the production boundary: introduce a distinct private raw-demand accumulation type, share one cardinality/consumption algebra with the independent oracle, and expose one
observe()conversion that canonicalizes before block-entry publication, alternative joins, contract extraction, decision-predicate queries, or terminal aggregation. Do not represent the raw chain as an uncanonicalizedAimsState: two dead projections legitimately form rawAbsent + Unrestricted, which collides bit-for-bit with theSCALARsentinel and could silently exclude a managed value. The calculus-first gate is compiled Lean associativity/permutation, eager-canonicalization non-commutation, single/lone projection observation, and folded block-walk composition; only then may Rust move canonicalization to the typed observation boundary and Annex E/rules narrow “after every transfer” to “after alternative joins and completed sequential accumulation.” -
The raw-demand Lean carrier is now implemented and focused-green:
RawDemandkeeps cardinality and consumption independent; component and carrierseqAddare associative and commutative; left/right folds agree; pre-observation folds are permutation-invariant; eager CN-1 canonicalization has a compiled non-commutation witness; the raw Project-plus-direct-use fold observes asOnce + Unrestricted; a lone Project observes as Dead; and TF-14/IA-5 bridge lemmas connect the carrier to the existing calculus. Full proof, map, parity, and checker gates remain in progress before the Rust carrier may turn green. -
The full calculus gate is now green: 21-job
lake build, placeholder lint, generated proof-map equality, 130-row statement parity, changed.proofchecker validation, and diff check all pass. Rust now shares only the pureRawDemandpair algebra between production and VF-3; production keeps product-state installation in a privateBlockState, and the oracle retains its independent endpoint/CFG derivation. The paired source-order pins are 2/2, transfer is 66/66, intraprocedural is 242/242, oracle is 57/57, and structural verification is 25/25. The previously red may-share ordering pin now derives post-alias occurrence from raw evidence without canonicalizing or exposing the raw pair as anAimsState. -
Full
ori_arc --libreached 1,701 passed, 3 failed, 1 ignored. One failure is a stale indirect-ABI expectation that asks a monomorphized concrete contract to specialize an indirect call despite the frozen uniform-borrowed residual ABI; preserve direct-call monomorphized lookup and keep indirect ownership target-independent. Two failures expose the scalar-projection boundary: managed dead projections correctly observe Dead, but an excluded scalar destination currently erases the real source read and yields an Absent/Dead parameter where existing pins require Once/Affine. Third-party adjudication is in flight before changing TF-14/L-9, the oracle, Lean, or tests; no assertion will be weakened to hide the seam. -
Third-party adjudication is complete: the two scalar-projection failures are correct regression witnesses. L-9 exclusion currently conflates “no scalar product-lattice state” with “no source read,” under-approximating a retained scalar field load and permitting an early logical release before the load. The single calculus distinguishes a managed Project borrow from a scalar copy-out: managed destination demand continues through TF-14; a live scalar destination contributes exactly
Once + Affineat that Project instruction, independent of how many times the copied scalar is later reused; a dead scalar destination contributes the existing dead-projection shape. A private monotonelive_scalarsbitset runs beside the product state in the same backward fixed point, is seeded across successor entries, and never installs SCALAR inAimsStateorRawDemand, preserving L-9. Lean TF-14 coverage lands first, then Rust, the independent oracle, and a matrix covering same-block, cross-block, copy-out cap, dead scalar projection, VF-2 coherence, and a fresh-local aggregate read with leak checking across executors. -
The unrelated indirect-ABI failure is now resolved at the architecture it was meant to pin: a direct
Applyproves monomorphized-contract merging can yield Owned, whileApplyIndirectproves every explicit residual argument remains Borrowed even when its known target contract is Owned. Annotation now returns a structured verification failure if any call-site ownership vector is not total; the release path no longer depends ondebug_assert!, and a malformed indirect call is a rejecting fixture. Focused ownership tests are 4/4 and the general verifier remains 25/25; a fullori_arcrerun waits for the scalar-projection decision. -
The consultation also surfaced a distinct generic-closure coverage question: closure-adapter freezing resolves a
PartialApplytarget and contract by exactName, while the direct call annotator alone still carries mono-base merging. Before declaring the old indirect fixture fully disposed, pin whether specialization rewrites every genericPartialApply.functo its concrete mono name before adapter freezing; otherwise move the exact identity mapping to the shared pre-AIMS callable seam rather than teaching indirect-call ownership to inspect dynamic targets. -
Paired reverse-source-order pins now fail red on both production inference and the independent oracle: each reports
Once + Linearwhere the theorem requiresOnce + Unrestricted. This confirms both implementations canonicalize too early when the dead Project is encountered first by the reverse walk; the oracle’s subject independence does not exempt it from the shared observation-boundary law. -
The sixth review pass also found evaluator-only negative list/string indexing. Intel confirms one shared
resolve_indexproducer for both cases. Two isolated spec pins fail on the pre-fix evaluator binary (0/2) and pass after rejecting negative indices on both evaluator and LLVM JIT (2/2 each); dedicated native AOT list/string pins pass in both debug and release profiles (2/2 each) and assert the bounds diagnostic, the fullori_evallibrary is 379/379, and the broader indexing evaluator corpus remains 37 passed, 0 failed, 1 skipped. Canonical case-identity evidence remains required before promotion. -
The same review finds range analysis assigning
count,len,abs,byte_to_int, andchar_to_intsemantics from bare interned spelling. The defect reaches bodyApply, forwardInvoke, and narrowingInvoke; a poisoned local summary can meet the false builtin range to produce Bottom, and LLVM physically truncates or extends every non-Top narrowed local.byte_to_intandchar_to_intare additionally dead aliases for the real typedByte.to_intandChar.to_intmethods. This is a correctness-sensitive semantic seam even though the first two exploit probes remained behaviorally correct. -
Production range transfer must consume the same pre-resolved call-target sidecar later frozen into
CallableTarget, never compareNameand never independently invoke runtime resolution. Split call-target closure into a pre-AIMS identity phase with exact local-body > external > runtime precedence and a post-AIMS validation/freezing phase; use staged stable names if numericFunctionIdorExternalFunctionIdallocation is not yet available. Registry-owned pure-dataRangeSemantics, selected through exactRegisteredMethodIdorRegisteredPreludeFunctionId, supplies only authorized builtin transfer behavior. Pair every positive Length/Count/Int.abs/Byte.to_int/Char.to_int case with same-spelled free, wrong-receiver, local-body, and imported-alias negatives across both Apply and Invoke, plus narrowing-sensitive evaluator/VM/LLVM debug/release/AOT parity. -
A separate diagnostic-hygiene pin now rejects executable linking without
@mainbefore invoking the system linker, names the Ori fix, and preserves--emit=llvm-irfor library-style modules. Its end-to-end integration slice is 2/2. -
The seventh review pass (
claude_review_1.mdSHA-256fb6ab2059c226a798db7467ed262cef4510f8df204ef76a128be50c24290d959) independently confirms the negative-index parity repair and rates the AIMS transfer/oracle pin matrix clean: paired positive/negative tests, explicit rejected-approach guards, and exhaustiveArcInstr/TerminalUsegrids. Its attempted snapshots are not promotion evidence: one was staled by the live-log forwarding harness change and one captured the transient unused-import compile failure. Snapshot G therefore remains the latest valid canonical anchor, while the newer localori_arc1,701/3 result is focused evidence only. -
Newly banked branch-acceptance work from that pass is explicit rather than allowed to disappear into review prose: make the indirect-argument ownership invariant release-active with a rejecting fixture; remove wrapper-private BUG IDs and session-history narrative from public AIMS source; delete the orphaned
UnionFinddoc fragment; propagate Alive2 capture-directory creation failure; replace codegen’s decorative box banners with plain section comments; and repair import detection so apub use "./..."-only module follows the multi-file path. The range seam repair also owns the three verified contradictory range docs and must ensure tracing never mutates the type pool merely to construct a disabled trace field. File-splitting and the broader comment inventory remain production-hygiene gates after semantic recovery, not reasons to perturb the calculus while the scalar-projection question is under adjudication. -
The seventh-pass snapshot’s transient oracle compile blocker is now repaired without changing demand semantics:
Cardinalityis imported only for the test-only dimension helper, while production keeps the unconditionalConsumptionimport.cargo check -p ori_arc --libis green in 9.16s, so the next snapshot will not repeat that invalid-D unusedinfrastructure failure. -
The scalar Project calculus-first gate is complete. Lean
RawDemand.scalarProjectContribution(live)selects exactlyOnce + Affinefor a live scalar copy-out and the existing dead-projection contribution for a dead result; theorems prove equivalence to a managed Once projection, cap the source occurrence at Once for every downstream scalar cardinality, and compose the obligation into the mapped TF-14 and IA-5 theorem surfaces. FocusedTransfer.lean, the 21-job fulllake build, placeholder lint, 130-row statement parity, generated-map equality, the two affected.proofchecks, and diff hygiene all pass. Rust may now implement only this proven distinction through a private scalar-liveness sidecar; neither backend may infer or compensate for it.
Scalar Project Recovery and Callable Target Closure Checkpoint - 2026-07-15
- Rust now implements the proven scalar-copy distinction through a private monotone liveness sidecar in the same backward fixed point. Managed projections retain TF-14 borrow behavior; a live scalar copy-out contributes exactly
Once + Affine; a dead scalar result contributes the dead-projection shape; repeated uses of the copied scalar never promote the source beyond Once. - Scalar
Projectno longer publishes false borrow provenance or project aliases. Copy-out therefore cannot manufacture an aggregate borrow that blocks otherwise valid COW or in-place decisions. - Positive and negative pins cover same-block reuse, live and unused
Jumpparameters, cross-CFG propagation, unconditional scalar capture byPartialApplyeven when the closure result is dead, nested scalar projections, dead copy-out, and the Once cap. Current Rust gates are scalar 67/67, intraprocedural 127/127, independent oracle 62/62, synergy 11/11, and fullori_arc --lib1,723 passed, 0 failed, 1 ignored; the additional passing test pins the sidecar update itself as a monotone OR-join that cannot shrink. - The oracle shares only pure demand algebra and frozen representation facts. It independently derives scalar liveness and constructs the live/dead contribution; it does not call the production scalar policy helper. The preceding Lean scalar-contribution, fold, map, parity, checker, and full-build gates remain green.
- A separate target-closure defect is now confirmed for named generic function values. One generic caller can instantiate the same expression site with several concrete callees, so a bare
Name, a site-onlyMonoInstanceId, or a duplicate-bearing sparse lookup cannot identify the selected edge. Freeze the exact callable edge before AIMS as(concrete caller BodyInstanceId, ExprId) -> MonoInstanceId, with an explicit source-body identity for nongeneric callers; require direct calls, invokes, andPartialApplyto consume that target-closed artifact and reject missing, duplicate, or ambiguous edges. No downstream AIMS, evaluator, VM, LLVM, native, compiled-WebAssembly, or JIT layer may recover a target by spelling. - Required closure pins include
generic_chain_multiple_specializations.ori, where one generic caller/site is realized forint,bool,str, andfloat; the corresponding named-function-value/PartialApplymatrix; imported and aliased generic targets; and negative fixtures for missing or conflicting exact edges. Performance and JIT promotion remain frozen until this seam is closed and a source-stable canonicaltest-allrestores the exact LLVM baseline and leak gates. - A fresh producer-inventory audit of canonical run
1784152040048560798-895db0celocalizes the next recovery wave without weakening either validator: 179 LLVM missing-callee records, 84 duplicate-parent records, 52 unresolved operator targets (all Eq), and 37 AOT missing-realized-callee records. The concrete causes are silently omitted accepted derive bodies; loss of concrete receiverIdxin mono method identity; raw parser-declaration enumeration in local/JIT/AOT paths; non-unique test display names; builtin impl receivers emitted under unqualified method names; import route/binding conflation; incomplete private/transitive helper closure; mono target binding before lambda specialization; and omission of Extend/DefImpl owners. The production-shaped repair is oneoric::realization::CallableCensusBuilderkeyed by semantic origin, typed method/owner or derived identity, concrete substitution, and stableTestId; names are linkage/presentation only. Its fixed-point close resolves alias convergence and shadowing, seeds roots, discovers helpers/generics/derives, specializes lambdas, binds exact Body/External/Runtime/Registry/Capability targets, emits oneLoweredArcBatch, and leaves independent artifact validation unchanged. First pins cover guard-clause coalescing, duplicate test display names, convergent imports, local shadowing and ambiguity, primitive receiver collisions, generic manual/derived Eq, specialization ordering, complete accepted-derive bodies, transitive imported helpers, Extend/DefImpl inventory, named Error registry dispatch, integer printing, const-only generics, and nested generic-body discovery.
Intel dossier — pointer and tier disposition
Dossier: prototype-baseline-regression-recovery--s-6afd2e99.intel.md (this section’s content/intel/ sidecar)
Read that dossier from line 1 through EOF before acting on this section. This block is a pointer and an audit record, never a substitute: not the BLUF, not a summary, not selected tiers.
| Dossier tier | Title | Lines | Disposition | Where / why |
|---|---|---|---|---|
| 0 | 0. Bottom line up front | 26 | integrated | Recovery Method |
| 1 | 1. The target — verbatim from the section | 19 | not_applicable | Tier 1 is the dossier’s verbatim restatement of the section’s own target (work item + Recovery Method + prescribed CallableCensusBuilder shape). It imposes no external constraint, and it quotes the abandoned w-786e6acf; the current work item w-61a0782d already supersedes it and already carries the recombined recovery design. |
| 2 | 2. The terrain — symbols named in the body (with files) | 45 | integrated | Recovery Method |
| 3 | 3. Code-graph recon | 47 | integrated | Recovery Method |
| 3D | 3D. Diagnostic / observability surface (relevance-gated — RELEVANT) | 21 | integrated | Recovery Method |
| 3H | 3H. Hygiene constraints (feed the design, not a code audit) | 24 | integrated | Recovery Method |
| 4 | 4. Cluster / family — the OPEN bug cluster this section umbrellas | 26 | integrated | Recovery Method |
| 5 | 5. Conformance audit — MISSING_ABSTRACTION (refreshed mid-session; LOW signal) | 19 | not_applicable | MISSING_ABSTRACTION is explicitly LOW-signal and provisional (scores 0.44-0.54, stale-then-fresh at serve) and the dossier itself calls it ‘not a mandate.’ The near-duplicate fact-accessor cleanup (external_function/external_functions, fresh_return_facts/param_disjointness) is opportunistic litter-pickup the census consolidation may collapse when it touches those accessors; it imposes no binding constraint on the section’s contract. |
| 6 | 6. Plan ownership — who owns this code now | 18 | integrated | Recovery Method |
| 7 | 7. Prior art — solved elsewhere (INTERROGATE, do not reproduce) | 44 | integrated | Recovery Method |
| 8 | 8. Sentiment — LIGHT (internal-recovery terrain) | 5 | not_applicable | Sentiment is LIGHT internal-recovery terrain: Ori’s issue corpus is empty and there is no community-heat signal for an internal stabilization section. The dossier states there is no test-bar change from sentiment; the raised bar it points to (the masking ban and the monotonic-decrease monitor) is already carried by the 3H and 7 integrations into Recovery Method, so tier 8 imposes nothing of its own. |
| 9 | 9. Declared coverage gaps (intel is honest about what it cannot see) | 17 | integrated | Recovery Method |
| 10 | 10. Recommended recon entry points (for /continue-roadmap execution) | 22 | not_applicable | Tier 10 is execution-time recon sequencing for /continue-roadmap (which files to read, which diagnostic to run, which bug plans to open, in what order), not a constraint on the section’s plan content. Its load-bearing items are already imposed via the 3D burden-sole leak-diagnostic rule, the 7 monotonic-monitor/Mikado rule, and the 9 read-producer-structure-from-source rule integrated into Recovery Method. |