0%

Section 10: Verification + Plan Closure

Goal: Confirm the burden architecture works as designed; verify emitted IR obeys the proven calculus; close bugs; propagate spec rewrites.

Context: Per proposal §AIMS.9 Verification Layers + §Bug Plan Closure + §Spec governance. This is the conditional-approval propagation point: Annex E §AIMS rewrites become unconditional only when §10 verification PASSES. §10 is the consumer side of the cross-plan proof↔implementation binding: aims-proofing-suite §18 proves the CHECKER trustworthy (Ori .proof ↔ Lean kernel agree) and the Lean corpus proves the CALCULUS sound; §10.7 here proves the emitted burden-op IR OBEYS that calculus (per aims-proofing-suite §18.3 scope note + §18.7 model-fidelity bridge).

Reference implementations: aims-rules.md §9 Verification Layers (existing VF-1..VF-7 framework). The proven realization + coexistence corpus: compiler_repo/aims-proof/lean/AimsProof/{Realization,Verification,Coexistence}.lean + proofs/08-realization/RL-comp.proof + proofs/11-coexistence/CH-*.proof. The existing static conformance cross-walk precedent: compiler_repo/aims-proof/scripts/check-section-05-compiler-conformance.sh (already maps proven DP-2/DP-3 → burden_elim.rs).

Depends on: Section 08 (rule-file sync + dual-discharged proof re-validation), Section 09 (predicate-stack + coexistence retirement), Section 12 (green-gate red partition — the terminal full-green criterion consumes §12’s burden-vs-orthogonal partition).

Intelligence Reconnaissance

Queries:

  • scripts/intel-query.sh --human file-symbols "compiler_repo/compiler/ori_arc/src/aims/verify" --repo ori
  • scripts/intel-query.sh --human plan-status BUG-04-118 — current bug state for closure verification
  • scripts/intel-query.sh --human callers run_aims_verify --repo ori
  • scripts/intel-query.sh --human callers eliminate_burden_ops --repo ori — burden-op decision sites the §10.7 oracle checks

Queried: 2026-05-08; 2026-06-02 (proof-corpus reconciliation — RL-comp net-preservation theorem + CH-* coexistence mirror + dual-discharge gate confirmed via aims-proofing-suite §18).

Results summary (≤500 chars) [ori]: existing AIMS infrastructure consumed; section work extends or migrates within unified model per missions.md §AIMS invariant 5. No parallel paths, no shadow trackers. §10.7 EXTENDS the VF-3 oracle + burden_balance (per §18.3); it does not author a parallel checker. Proven-antecedent set sourced from proof-lean-map.json + the aims-rules.md terminal-state table.

10.1 VF-1 burden-balance check implementation + CI integration

File(s): compiler_repo/compiler/ori_arc/src/aims/verify/burden_balance.rs (new)

The burden-balance check is the SHIPPED verification pass that enforces the PROVEN RC net-preservation invariant on emitted burden-op IR. It does not re-prove anything — it is the executable conformance of the proven realization rules applied early (on the burden-op form, before Phase-7 lowering to RcInc/RcDec).

  • Implement per proposal §AIMS.9.1.1:
    • Per-edge balance dataflow: for each CFG edge e, live reference count rc_e(v) is non-negative integer; computed via forward dataflow per the rules in the proposal.
    • SCC net-zero obligation: for every SCC, sum of (BurdenInc − BurdenDec − consuming-transfers) over instructions equals zero.
    • Terminator transfer: terminators that consume v decrement count on outgoing edge.
    • Per-path-terminal release: every reachable path’s running count reaches zero exactly at path-terminal.
  • Proof grounding (cite, do not re-derive): the check enforces proofs/08-realization/RL-comp.proof (AimsProof.Realization::RL3_elision_net_preserving — RC elision is net-preserving) + RL-2 (RL2_dec_at_last_use) / RL-4 (RL4_edge_dec_decision) / RL-5 (RL5_dead_at_entry_cleanup) dec-placement + the proofs/10-counterexample/ rc_per_path_invariant (verdict UNSAT per results.json — the proven calculus admits NO per-path RC imbalance). The burden-op form’s balance maps to the proven RcInc/RcDec balance via Phase-7 mechanical lowering (BurdenInc→RcInc, BurdenDec→RcDec) + the proven CH-1/CH-2 (burden decision = lattice DP-2/DP-3 decision).
  • On failure, emit BurdenImbalance error with offending edge or SCC + divergent counts.
  • Wire into AIMS pipeline as a verify pass; gate behind ORI_VERIFY_ARC=1 per aims-rules.md §9 shape.
  • CI integration: add to compiler_repo/test-all.sh or equivalent (locate existing verify-pass invocation).
  • Tests: balanced cases (per proposal §AIMS.9.1.1 worked examples) pass; deliberately unbalanced cases produce BurdenImbalance (negative pin — a hand-injected BurdenInc-without-BurdenDec fails the proven net-preservation).

Subsection close-out (10.1) per protocol.

10.2 VF-7 rewrite-soundness tier verification

  • Run VF-7 tier-a / tier-b / tier-c verification per aims-rules.md §9 VF-7 over the full test corpus.
  • Verify burden-emit + lattice-eliminate + Phase 7 lower roundtrip preserves observable behavior on every test program (the shipped realization of the proven RL-comp RL3_elision_net_preserving whole-suite equivalence to plain ARC).
  • Tests: VF-7 tier-c regression suite green.

Subsection close-out (10.2) per protocol.

10.3 Full ./test-all.sh + dual-execution parity confirmation

  • timeout 150 ./test-all.sh (or longer if the suite genuinely needs it — document if so).
  • Pass count IDENTICAL or strictly improved vs pre-burden baseline.
  • Zero failures, unconditional (2026-06-10): no failing test of any kind remains — burden-attributable dissolved by §09; orthogonal red FIXED (via /fix-bug per §10.4 still-open handling), never tracked-and-left or excluded.
  • Zero warnings (2026-06-10): the full ./test-all.sh output carries zero warnings of any kind (suite warnings, cargo warnings, harness warnings); every warning is fixed at source, never suppressed.
  • Zero skipped tests (2026-06-10): enumerate every #[ignore]/#skip (the ./test-all.sh Dispositions line + per-suite ignored counts); for each, fix its tracked bug via /fix-bug and re-enable the test. Close gate: 0 ignored, Dispositions: 0 total, 0 untracked.
  • Build completeness (2026-06-10): every build step green — debug + release profiles AND the wasm target build; the LLVM backend crashes on zero tests (zero ICEs, zero SIGSEGV/SIGABRT from codegen).
  • Trace-mode sweep clean (2026-06-10): VF-1 warn channel (ORI_LOG=ori_arc::pipeline::aims_pipeline::postprocess=warn) emits zero lines corpus-wide; ORI_TRACE_RC / ORI_DUMP_AFTER_ARC / ORI_DUMP_AFTER_BURDEN sweeps complete warning-free and error-free.
  • Add dual-execution parity tests for: closures-inside-loops, recursive types, Drop AUGMENT, Value/HeapType mixed sum-type variants.
  • Verify eval + LLVM produce identical observable behavior on every new test (per CLAUDE.md §Fix Completeness).
  • ORI_CHECK_LEAKS=1 reports zero leaks on memory-touching tests.

Subsection close-out (10.3) per protocol.

10.4 Bug closure verification — live AIMS-bug sweep

The closure set is NOT a list written here. It is BUILT BY A LIVE SEARCH of the bug tracker at §10 execution time (bug-tracker/open-bugs.json + bug-tracker/closed-bugs.json are the SSOT, queried fresh) so any AIMS-associated bug filed between now and §10 is automatically in scope. The 00-overview.md arrays (obe_on_completion / partial_obe / absorbed_bugs / orthogonal_bugs) + the ## Known Bugs table demote from SOURCE to CROSS-CHECK: the search MUST find at least every bug they list; any divergence is drift to reconcile, and the live tracker wins.

  • Build the set (live search). Enumerate candidates via scripts/plan_corpus/bug_tracker/api.py:query_open_bugs() + query_closed_bugs(), filtered to the AIMS-bearing subsystems (codegen-llvm, runtime-arc, plus any typeck/eval entry naming an AIMS surface). This is the LIVE re-run of the 00-overview.md §Bug Cluster Audit methodology (frozen 2026-05-13; “was incomplete” per its own HISTORY). Second discovery angle so nothing AIMS-touching is missed: scripts/intel-query.sh bugs-for aims-burden-tracking + scripts/intel-query.sh symbol-plans <aims-symbol> --repo ori over the AIMS code surface (e.g. emit_burden_ops, eliminate_burden_ops, class_payload_of, run_aims_verify); cross-reference the bug-tracker/section-04-codegen-llvm.md + section-05-runtime-arc.md + section-02-typeck.md + section-03-eval.md bodies.
  • AIMS-association predicate (apply per candidate by reading its title + repro + bug plan-dir RCA — the subsystem field is too coarse to decide alone): a bug is AIMS-associated iff its code surface is in compiler/ori_arc/src/{aims,lower,realize,borrow,drop,fbip,uniqueness,classify,rc_insert}/**, OR ori_llvm arc_emitter, OR ori_rt rc/drop, OR its governing rule is an AIMS calculus rule (DP-/RL-/CN-/TF-/IC-/PL-/VF-/CH-* per aims-rules.md). A bug merely MENTIONING “AIMS” in tooling/docs text is NOT AIMS-associated — the predicate is the code/rule surface, not the word.
  • Record the live set in this section’s body as a table (bug ID | subsystem | one-line | verified verdict), captured at execution time — NOT pre-frozen in this file.
  • Per-bug verify against the current post-burden build (repro each). Assign a VERIFIED verdict — never trust frozen array membership. Where the symptom is a runtime double-free/leak/UAF, apply the section-12 §12.2 ORI_DISABLE_BURDEN_OPS=1 proven-baseline re-check: a defect that PERSISTS with burden ops off is in the proven pre-burden baseline → orthogonal, NOT burden-dissolved.
  • Classify each by verified verdict: fixed/OBE (failure mode dissolved by §03 Phase-5 emission + §09 retirement) | partial (only a subset dissolves) | still-open AIMS-root (a genuine current AIMS defect) | orthogonal (correctness rests on a pending/unprovable_with_gap_citation rule OR a different subsystem — decide with the SAME proven-coverage guard section-12 §12.1 defines, SSOT; do NOT author a parallel classifier; cross-reference §12.2’s mapping).
  • Act — fixed/OBE: write a closure-evidence note in the bug’s plan dir (repro + verified-dissolved evidence), flip via scripts/plan_corpus/bug_tracker/api.py:flip_bug_status(bug_id, "obe"|"resolved", summary), then git mv the plan dir to bug-tracker/plans/completed/BUG-XX-NNN/ per CLAUDE.md §Bug Handling.
  • Act — absorbed-and-already-closed (closed-as-absorbed per 00-overview.md HISTORY, e.g. BUG-04-112/118): VERIFICATION-ONLY — confirm the absorption surface still holds at the full ./test-all.sh sweep (BUG-04-118’s 16/16 match_alias::*; BUG-04-112’s §05.0 IC-1 precondition); do NOT re-close.
  • Act — absorbed-OPEN-fixed-by-plan (e.g. BUG-04-121/123): close here once its fixing section (§03A/§07/§09/§12) has landed AND the verdict is verified-dissolved — NOT verification-only.
  • Act — partial: close the dissolved subset’s claim with evidence; keep or file a tracked bug for the persisting subset per routing.md §2 (e.g. BUG-04-094 drop_hint at Phase 7 lowering).
  • Act — still-open AIMS-root: §10 OWNS the fix — run /fix-bug BUG-XX-NNN to completion (full TDD rigor), then close. A still-broken AIMS bug surfacing at §10 is §10’s to fix, NOT defer (discovery IS the assignment per CLAUDE.md §Bug Handling).
  • Act — orthogonal: record the VERIFIED orthogonal disposition + its proven-coverage citation; leave the bug open + tracked; /add-bug if the search surfaced an untracked one (per routing.md §2).
  • Reconcile against the cross-check. Diff the live-search set against 00-overview.md’s four arrays + the ## Known Bugs table: every array/table entry MUST appear in the search; every search hit MUST carry a verdict. Flag any divergence (an array lists a bug the predicate now rejects, OR the search finds an AIMS bug no array carries) as drift, and cure it (update the array OR the bug’s disposition).
  • Close gate (10.4): complete only when the live search returns ZERO unresolved AIMS-associated bugs — every hit closed-with-evidence, verification-only-confirmed, or carrying a verified disposition (orthogonal/tracked).

Subsection close-out (10.4) per protocol.

10.5 /sync-aims-spec propagation

  • Invoke /sync-aims-spec (or run the equivalent sync per aims-rules.md drift-gate flow).

  • Annex E §AIMS rewrites in proposal §Spec & Grammar Impact propagate UNCONDITIONALLY: §AIMS.6 Phase 5 / Phase 6 / Phase 7 prose, §AIMS.9 §AIMS.9.1.1 Burden-Balance Check, §AIMS.4 clarifying header.

  • Per aims-spec-promotion-proposal.md precedent: conditional approval becomes unconditional via this propagation.

  • Three-surface coherence confirmed: the burden-revised calculus is identical across (1) .claude/rules/aims-rules.md (§08.2), (2) Annex E §AIMS (this propagation), and (3) the proof corpus + Lean mirror (§08.6 dual-discharged). Verify drift gate (/sync-aims-spec --check) reports clean post-propagation AND dual-discharge.sh is still green (no proof-surface drift introduced by the spec propagation).

  • Tests: drift gate clean; spec section count and clause numbering preserved.

  • TPR checkpoint — /tpr-review covering 10.1-10.5.

Subsection close-out (10.5) per protocol.

10.6 Design-oracle verification (built at §13.6 — RUN here)

ABSORBED into §13.6. aims-burden-design-oracle.sh + the frozen_rule_version producer/consumer contract are BUILT by the §13 Burden Verification Suite (§13.6). §10 RUNS it at the terminal verification gate.

  • Run compiler_repo/diagnostics/aims-burden-design-oracle.sh (built at §13.6): confirm pass/fail per shape + per invariant is clean, and the frozen_rule_version contract holds (§00 frozen_rule_version: v1 matches §05 consumes_proof_product: v1; no FROZEN_RULE_VERSION_MISMATCH).

10.7 Proven-rule conformance — calculus ↔ emitted burden-op IR (built at §13.5 — RUN here)

ABSORBED into §13.5. The burden-aware VF-3 oracle extension (oracle.rs + burden_balance.rs) + the proven-antecedent per-IR conformance + the proof-lean-map.json consumption + the §17 carve-out binding are BUILT by the §13 Burden Verification Suite (§13.5, the full six-pattern adoption). §10 RUNS that oracle at the terminal verification gate against the post-§09 emitted IR (the in-flight prototype-able-now build at §13.5 widens to full coverage once §05–§09 burden emission lands; §10 is the full-coverage run).

  • Run the §13.5 burden-aware VF-3 oracle over the full post-burden corpus: confirm each burden-op decision point on emitted IR satisfies the proven antecedent of its governing DP/RL/CH rule (DP-2 AimsProof.Decision::DP2_is_rc_dec_unnecessary_table; RL-comp AimsProof.Realization::RL3_elision_net_preserving; CH-1 AimsProof.Coexistence::CH1_burden_emitted_is_bridge; CH-comp CHcomp_handshake_union).
  • Confirm the negative pin (§13.5): an injected antecedent violation (BurdenDec eliminated where DP-2’s antecedent is false) produces a conformance error citing rule ID + site.
  • Confirm the §13.5 enforcement set is the proof_status: complete intersection (proof-lean-map.json kind: theorem | composition_folded ∩ aims-rules.md terminal-state proven_sound | reformulated_and_proven); locality-carve-out rules stay advisory per the §17 divergent-pending discipline.
  • Confirm the four legs of meaningfulness hold at §10 close: (1) dual-discharge.sh green (§13.4 burden rows); (2) Lean corpus lake build green; (3) §13.5 oracle confirms emitted IR obeys the calculus (this run); (4) §17 shipped-conformance probe matches the model.

Subsection close-out (10.7) per protocol.

10.R Third Party Review Findings

  • None.

10.N Completion Checklist (§10 verification-gate close)

  • All 10.X subsections complete.
  • VF-1 burden-balance check + VF-7 rewrite-soundness + full ./test-all.sh + dual-execution parity all verified; the §14-wired run_aims_burden_verification test-all step (§14 depends_on predecessor) is the gate the terminal ./test-all.sh runs.
  • Hardened terminal gates verified (2026-06-10): ./test-all.sh zero failures + zero warnings + 0 ignored + Dispositions: 0 total, 0 untracked; wasm build green; zero LLVM-backend crashes; trace-mode sweep clean (VF-1 warn channel zero lines; ORI_TRACE_RC/dump modes warning-free).
  • §10.7 proof↔implementation bridge landed: VF-3 oracle + burden_balance enforce the proven DP/RL/CH antecedents on emitted IR; negative pin (injected violation → conformance error) passes.
  • aims-proofing-suite §18 dual-discharge gate (dual-discharge.sh) green for all burden-touched proof rows (the antecedents §10.7 enforces are dual-verified).
  • Bug closures landed: the live AIMS-bug search (§10.4) returns ZERO unresolved AIMS-associated bugs — every hit closed-with-evidence, verification-only-confirmed, or carrying a verified disposition; the live set is reconciled against the 00-overview.md cross-check arrays + ## Known Bugs table.
  • /sync-aims-spec propagation complete; Annex E §AIMS unconditional; three-surface coherence (aims-rules.md / Annex E / proof corpus) confirmed.
  • Plan-level close is owned by §15 (terminal section), NOT §10 — all-MSC-checked, full-plan annotation cleanup, 00-overview.md + index.md status → complete, and plan-move live in §15.4 (§15.4.P1-P4) per the §15-terminal-tail topology (execution order §10 → §11 → §15). §10.N is the §10 VERIFICATION-gate close only.
  • /tpr-review passed (§10 final, full-section); /impl-hygiene-review passed.

HISTORY

  • 2026-06-10 — Terminal sweep HARDENED per user directive (plan-level Mission Success Criteria hardening, 00-overview.md HISTORY 2026-06-10). §10’s ./test-all.sh criterion is now UNCONDITIONAL green: zero failures (orthogonal red FIXED, never tracked-and-left or excluded), zero warnings of any kind, zero ignored, zero build failures incl. the wasm build, zero LLVM-backend crashes. Two NEW success criteria + matching §10.3 checkboxes: (a) zero skipped tests — every #[ignore]/#skip fixed via /fix-bug and re-enabled, close gate 0 ignored + Dispositions: 0 total, 0 untracked; (b) all trace/diagnostic modes clean — VF-1 warn channel zero lines corpus-wide, ORI_TRACE_RC/ORI_DUMP_AFTER_ARC/ORI_DUMP_AFTER_BURDEN sweeps warning-free, ORI_CHECK_LEAKS=1 zero leaks. §10.N gains the hardened-gate verification item. The Nightly-CI monitored-run gate lands at §15.4.P0 (NOT here) — §10 is the verification gate, §15 owns plan close.
  • 2026-06-03 — §10.4 reworked from a frozen closure list to a LIVE AIMS-bug tracker search. Per user directive: the closure set MUST be built by literally searching the tracker at §10 execution (so any AIMS bug filed before §10 is reached is auto-included), NOT enumerated in this plan. (1) §10.4 body rewritten as a live bug_tracker/api.py:query_{open,closed}_bugs search + an AIMS-association predicate (code surface in ori_arc/src/{aims,lower,realize,borrow,drop,fbip,uniqueness,classify,rc_insert} / ori_llvm arc_emitter / ori_rt rc-drop, OR governing AIMS calculus rule per aims-rules.md) + per-bug verify against the post-burden build + verdict-driven disposition (fixed/OBE → close+move; partial → split; still-open AIMS-root → /fix-bug here; orthogonal → verified-disposition via the §12.1 proven-coverage classifier). (2) Frozen bug-ID lists removed from success_criteria (the prior DIRECT/VERIFICATION-ONLY/LIKELY/NOT-PROMISED enumeration — 074/086/093/095 had already drifted from the 00-overview.md arrays) and from touches: (12 hardcoded BUG dirs → tracker-root surfaces). The 00-overview.md arrays demote from SOURCE to CROSS-CHECK. (3) Close gate: §10.4 is complete only when the live search returns zero unresolved AIMS-associated bugs. The 00-overview.md §Bug Cluster Audit (frozen 2026-05-13, “was incomplete” per its own HISTORY) is now re-run LIVE at §10 rather than read from frozen frontmatter. VF-1/VF-7/conformance/test-all/sync deliverables (§10.1-§10.3, §10.5-§10.7) unchanged — they are the verification machinery that produces the closure evidence.
  • 2026-06-02 — Reworked §10 to ground verification in the REAL proven calculus + rebuilt §10.7 on the real conformance machinery + DAG fix. (1) §10.1 VF-1 burden-balance check reframed as the executable enforcement of the PROVEN RC net-preservation (RL3_elision_net_preserving / RL-comp + the §10-counterexample rc_per_path_invariant UNSAT) on the burden-op form, NOT a new calculus theorem (missions §AIMS invariant 5). (2) §10.7 rebuilt: PRIMARY = extend the in-compiler VF-3 oracle + burden_balance.rs to assert proven DP/RL/CH antecedents on emitted IR (per the aims-proofing-suite §18.3 ownership note); COMPLEMENT = reference the EXISTING static cross-walk check-section-05-compiler-conformance.sh (already maps burden DP-2/DP-3 → burden_elim.rs) rather than duplicate it; proven-rule set consumed as data from proof-lean-map.json (kind: theorem|composition_folded) ∩ the aims-rules.md terminal-state table; bound to the §17 divergent-pending carve-out discipline; the four legs of meaningfulness each cite their real artifact. (3) Added a success-criterion + checklist item gating §10 close on dual-discharge.sh being green for the burden-touched rows. (4) DAG fix: depends_on corrected from ["09"] to ["08", "09", "12"] — §10’s own terminal-green criterion names §08 + §12 as predecessors it consumes (rule-sync + green-gate partition); the prior frontmatter encoded only §09 (with §08 transitive but §12 unreachable). Topological order is now 08, 09, 12 → 10 → 11 (acyclic; §12 depends_on: [] feeds §10). All theorem references use lean/AimsProof/<Module>.lean; no cross-validation/ path (does not exist).