contract-coherence-zero

Every remaining test-all failure is one shape: the post-AIMS realization ContractCoherenceViolation. The VF-3 oracle (ori_arc::aims::verify::oracle::verify_coherence) re-derives MemoryContract from subject-independent realized evidence and disagrees with the inferred contract. Every disagreement is in the SAME direction: the inferred contract is optimistic, the realized evidence is conservative.

Measured baseline

Source: test-all run 1785046490971773359-7aecd20f, snapshot 45b912e37480, Infrastructure failures: 0 (the harness is sound; every failure is compiler-side).

Mismatch taxonomy

Records by kind-set: 333 EffectMismatch only; 41 ParamAccess only; 17 EffectMismatch + ParamAccess; 10 ParamMayShare only.

Failing AOT integration tests (46)

Suite aot, failure_kind test_failure. Every one panics at compiler/ori_llvm/tests/aot/util/compile.rs:116 with error[E5001]: LLVM module verification failed carrying a ContractCoherenceViolation.

Failing ori_llvm spec sources (21)

Suite ori_llvm, failure_kinds llvm_compile_fail (334) + file_error (21). The 334 compile failures collapse onto these 21 distinct sources.

Deliverables

• Cure EffectMismatch { field: "may_share", inferred: false, realized: true } — 458 occurrences across 350 failure records, the dominant class. IC-5 EffectSummary derivation under-reports sharing the VF-3 oracle re-derives from realized evidence.
• Cure ParamAccess { inferred: Borrowed, realized: Owned } — 100 occurrences across 58 failure records. IC-3 ParamContract.access disagrees with the realized owned transfer.
• Cure ParamMayShare { param_index, inferred: false, realized: true } — 11 occurrences across 10 failure records. Per-param IC-3 may_share under-reports.
• Prove each cure in the compiled Lean BEFORE implementing per arc.md §CP-1, then sync all four surfaces per §CP-2 (compiled Lean, .proof, aims-rules.md + arc.md, Annex E §AIMS).
• All 46 failing ori_llvm::aot integration tests green: the arc, borrow_independence, borrowed_invoke_leak, burden_yield_identity_push_dup, generics, match_alias, fat_ptr_iter, higher_order, ir_quality_attributes, ir_checks, iterator_drop, predicate_stack_probe, memory_stress, journey_guard, derives, enum_discriminant, error_constructor, strings, iterators, multi_module_glue, default_minmax_mono_in_generic, and inc_symmetry clusters.
• All 21 distinct ori_llvm spec sources compile: tests/aims/moved_fields_partial_move.ori plus the 20 tests/spec files spanning declarations, expressions, patterns, types/sum, types/enum/niche, generics, aims, and traits (derive, index, method_resolution, traceable).
• TDD matrix BEFORE the cure: mismatch-kind x contract-dimension x call-shape, each cell carrying a positive pin and a reverted-fix negative pin that FAILS when the cure is backed out.
• Layer coverage per layer-coverage.md §1: L9 cross-executor parity (evaluator vs every affected admitted executor on one corpus) and L10 resource/ownership leak-freedom, each covered or explicitly N/A with a stated reason.
• Re-run the north-star gate to a green terminal aggregate: python -m scripts.test_all_runtime run then its emitted blocking status_command, asserting failed=0 skipped=0 lcfail=0 and zero leaks with the AIMS verifier gate ACTIVE.

Discipline

• Calculus-first per arc.md §CP-1: prove the governing theorem in the compiled Lean BEFORE implementing. A failing test is first-order evidence of an IMPLEMENTATION divergence (case a), never a licence to weaken the calculus.
• Four-surface sync per arc.md §CP-2: compiled Lean, .proof, aims-rules.md + arc.md, and Annex E §AIMS move in the same change set.
• The oracle is the conservative party in all three shapes. Suppressing the oracle, widening the inferred contract to match without proof, or gating the check on the failing inputs is INVERTED-TDD:gated-deliverable.
• Every cure carries a reverted-fix negative pin that FAILS when the cure is backed out.