Section 06: Verification

Status: Not Started Goal: Prove that all ARC optimizations from Sections 01-05 are correct, produce identical observable behavior to the unoptimized baseline, maintain zero leaks, and provide measurable performance improvement.

Governing verification tier — cite aims-rules.md §9 VF-7: Sections 03-05 ship aims-rules.md’s already-proven-but-target-only RL-9/RL-22-RL-26 rules (per each section’s own governing-spec note). VF-7 requires ALL THREE tiers for an active rewrite to count as sound: (a) compile-time structural verification, (b) test-time behavioral verification, (c) a documented proof sketch. This section’s 06.1-06.5 work satisfies tiers (a)+(b) (test matrix, ORI_DISABLE_ARC_OPTS A/B, code journey, leak/valgrind/codegen-audit); tier (c) is satisfied by CITING the already-compiled Lean proof for the shipped rule (compiler_repo/aims-proof/proofs/08-realization/RL-{9,22,23,24,25,26}.proof + Lean mirror in AimsProof.Realization/Coexistence) — do not re-derive a proof sketch from scratch, cite the existing one. 06.6 closes the loop with the arc.md §CP-2 four-surface sync.

Depends on: All prior sections.

06.1 Test Matrix

Build a comprehensive test matrix covering every optimization through every relevant type × pattern × CFG combination.

Section 01 (Statistics):
- Verify SynergyMetrics fields are correctly populated for all test programs
- rc_ops_post_emission > 0 for programs with heap types (str, [int], closures)
- rc_ops_post_emission == 0 for int-only programs
- coalesce_reduction_percent() returns plausible values (0-100%)
- CoalesceStats counts match manual IR inspection for 3+ programs
- Statistics do not regress program output (pure instrumentation)
Section 02 (Barriers):
- Type: str, [int], Option<str>, closures, {str: int} map, Set<str>
- Call pattern: all-borrowed, all-owned, mixed, no-contract (FFI)
- CFG: linear, loop body, conditional call
Section 03 (KnownSafe):
- Type: str, [int], Option<str>, closures, structs with heap fields
- Nesting: 1-deep (no elim), 2-deep (one pair), 3-deep (two pairs)
- CFG: linear, diamond (both arms increment), loop (invariant RC)
Section 04 (COW Contraction):
- Type: struct with mutable field, [int], {str: int}
- CowMode: StaticUnique, Dynamic, StaticShared
- Pattern: single mutation, loop mutation, conditional mutation
- Executor: evaluator oracle, VM, LLVM debug, LLVM release, AOT
- Resource: shared ownership/drop/unwind order, zero leaks, bounded error cleanup
Section 05 (RC Motion):
- Type: str, [int], Option<str>, closures, maps
- CFG: diamond (retain in pred, release in succs), triangle, loop, nested loop, early return
- Pattern: same-block pair, cross-block pair, loop-invariant RC

06.1.1 Discovered Gaps

Gap	Roadmap Location	Test	Severity
(to be filled during implementation)

/tpr-review passed — independent review found no critical or major issues (or all findings triaged)
/impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.
Subsection close-out (06.1) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-06.1 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 06.1: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.
/sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.
Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

06.2 Behavioral Equivalence

Verify that optimized programs produce identical output to unoptimized.

Implement layer-specific, centrally registered ablation inputs; do not create one ORI_DISABLE_ARC_OPTS switch that conflates the calculus and physical adapters:
- Register via the SAME mechanism every other toggle in arc.md §Debugging uses — debug_flags.rs’s flags! macro (per impl-hygiene.md COVER-33/COVER-34/SPEC-71’s central-enumeration + check-debug-flags.sh verification requirement), NOT a hand-rolled std::env::var + OnceLock outside that registry. A toggle read via a separate ad-hoc mechanism is invisible to check-debug-flags.sh and to arc.md’s “Toggle convention” documentation sweep.
- One diagnostic input may disable the Section-02 logical event-ordering refinement at closed AIMS realization; it cannot affect physical plan selection
- Separate explicit VmPhysicalOptions / CompiledPhysicalOptions fields disable Sections 03/04-physical/05 after layout/mechanism selection; neither enters AimsPipelineConfig
- Resolve environment flags once in oric into those typed inputs; pure planners and AIMS receive values, never read ambient environment state
- A/B results report logical-plan identity and physical-plan identity separately, preventing a physical win from masquerading as a calculus change
- Give the logical and physical ablations distinct centrally registered names and // Env: documentation, each with a path-exercising test and arc.md/physical-plan documentation naming exactly what it bisects
- Add COVER-33-shaped negative pins proving each flag independently restores only its own prior behavior; the physical flag must leave the AIMS trace byte-identical, and the logical flag must not change target-plan selection policy
Build comparison harness:
- Execute the evaluator oracle plus VM, LLVM debug, LLVM release, and AOT lanes
- Run every physical lane with and without new optimizations
- Compare value, typed error, stdout, stderr, exit state, panic, and timeout classification
- Compare ownership/drop/unwind event order between VM and compiled lanes
- Require zero live allocations, zero leaked resources, and bounded cleanup in every physical lane
- Report any mismatch; generic/physical agreement inside one backend is not an absolute parity result
Extend the canonical parity harness to execute the full spec corpus under a 2×2 matrix: logical event coalescing on/off × selected physical ownership optimization on/off, for VM, LLVM debug/release, and AOT. The evaluator remains the representation-abstract behavioral oracle. Every physical lane must match its behavior, the two physical settings must preserve the exact AIMS trace identity, and all physical lanes must satisfy the shared ownership/drop/unwind and resource gates. Do not implement this as a chat-owned shell loop or stdout-only diff.
Track and investigate every mismatch.
/tpr-review passed — independent review found no critical or major issues (or all findings triaged)
/impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.
Subsection close-out (06.2) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-06.2 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 06.2: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.
/sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.
Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

06.3 Code Journey

Run /code-journey to test the full pipeline end-to-end with progressively complex programs.

Run /code-journey — journeys escalate until the compiler breaks down
All CRITICAL findings from journey results triaged (fixed or tracked)
Evaluator, VM, LLVM debug/release, and AOT produce identical results for all passing journeys
VM and compiled journeys preserve shared ownership/drop/unwind events and clear resource gates
Journey results archived in plans/code-journeys/
/tpr-review passed — independent review found no critical or major issues (or all findings triaged)
/impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.
Subsection close-out (06.3) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-06.3 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 06.3: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.
/sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.
Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

06.4 Safety Verification

RC balance: diagnostics/rc-stats.sh on all test programs → balanced
Leak check: ORI_CHECK_LEAKS=1 on all test programs → zero leaks
VM resource check: zero live heap/value-arena objects after success, error, panic, and quota exit
Event check: VM and compiled ownership/drop/unwind traces preserve the shared artifact order
Valgrind: diagnostics/valgrind-aot.sh on representative programs → no memory errors
Codegen audit: ORI_AUDIT_CODEGEN=1 ORI_AUDIT_STRICT=1 on all test programs → no findings
Stress test: 1000+ allocations, 100+ recursion depth, 1000+ list elements — all clean
/tpr-review passed — independent review found no critical or major issues (or all findings triaged)
/impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.
Subsection close-out (06.4) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-06.4 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 06.4: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.
/sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.
Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

06.5 Performance Validation

RC operation reduction:
- Baseline: ORI_LOG=ori_arc=info ori build tests/spec/ with Sections 02-05 disabled
- Optimized: same with all sections enabled
- Target: 30%+ total RC operation reduction on typical programs
- Note: aims-compare.sh was removed (used non-existent --features aims). RC operation measurement requires a new tool — use ORI_AUDIT_CODEGEN=1 + diagnostics/rc-stats.sh as an interim approach for counting RC ops.
Compile-time overhead:
- Measure compilation time with and without new passes
- Target: < 5% compile-time regression
- Run cargo bench -p oric if parser/typeck benchmarks exist
Runtime performance:
- Benchmark programs in tests/benchmarks/
- Measure execution time with and without optimizations
- Target: measurable improvement on RC-heavy programs
/tpr-review passed — independent review found no critical or major issues (or all findings triaged)
/impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.
Subsection close-out (06.5) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-06.5 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 06.5: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.
/sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.
Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

06.6 Documentation and Cleanup

Update CLAUDE.md with new pipeline steps if applicable
Update .claude/rules/arc.md with new pass descriptions
Update compiler/ori_arc/src/aims/mod.rs module docs
Add architecture notes to compiler/ori_arc/src/aims/knownsafe/mod.rs
Add architecture notes to compiler/ori_arc/src/aims/rc_motion/mod.rs
arc.md §CP-2 four-surface sync (MANDATORY, not optional doc polish): RL-9/RL-22-RL-26 move from target-only to shipped in this section — the compiled Lean + .proof stay unchanged (already proven), but the other two surfaces MUST flip in the same change set:
- .claude/rules/aims-rules.md top-of-file carve-out list: remove “§8 RL-22 thru RL-26 (post-pipeline): target-only” (or narrow it if a subset ships)
- .claude/rules/arc.md “Where AIMS is HEADED” section: remove the “Clang ARC patterns (plans/clang-arc-lessons/) - KnownSafe flag, barrier analysis, RC motion, COW contraction, per-phase elimination statistics” bullet; fold the shipped capabilities into “What AIMS does TODAY (shipped, not roadmap)”
- Add an aims-rules.md HISTORY entry recording the conformance shipping per the file’s own per-rule provenance-table convention (terminal state stays proven_sound; this is a shipped-conformance note, not a calculus change)
Plan annotation cleanup: strip ALL code annotations referencing this plan (clang-arc-lessons, section numbers 01-06, any plan-specific markers) from all source files. Run bash .claude/skills/impl-hygiene-review/plan-annotations.sh --plan clang-arc-lessons and verify 0 annotations remain. Only spec references (Spec: Clause N.M) are permanent.
/tpr-review passed — independent review found no critical or major issues (or all findings triaged)
/impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.
Subsection close-out (06.6) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-06.6 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 06.6: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.
/sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.
Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

06.7 Completion Checklist

Test matrix covers all sections (01-05) × types × patterns × CFG combinations
ORI_DISABLE_ARC_OPTS flag implemented, registered in debug_flags.rs, documented in arc.md §Debugging, and functional
Behavioral equivalence verified — 0 evaluator/VM/LLVM-debug/LLVM-release/AOT mismatches
VM and compiled ownership/drop/unwind traces match the shared artifact; every resource gate is clean
Code journey passes — all evaluator/VM/compiled lanes match, no CRITICAL findings
RC balance verified via rc-stats.sh — all functions balanced
ORI_CHECK_LEAKS=1 — zero leaks on all test programs
Valgrind clean on representative programs
Codegen audit clean (ORI_AUDIT_STRICT=1)
Stress tests pass
30%+ total RC operation reduction on typical programs
< 5% compile-time regression
All documentation updated
Plan annotation cleanup: plan-annotations.sh returns 0 annotations for this plan
./test-all.sh green
./clippy-all.sh green
/tpr-review passed — independent Codex review clean
/impl-hygiene-review passed — hygiene review clean
/improve-tooling retrospective completed — MANDATORY at section close, after both reviews are clean. Reflect on the section’s debugging journey (which diagnostics/ scripts you ran, which command sequences you repeated, where you added ad-hoc dbg!/tracing calls, where output was hard to interpret) and identify any tool/log/diagnostic improvement that would have made this section materially easier OR that would help the next section touching this area. Implement every accepted improvement NOW (zero deferral) and commit each via SEPARATE /commit-push. The retrospective is mandatory even when nothing felt painful — that is exactly when blind spots accumulate. See .claude/skills/improve-tooling/SKILL.md “Retrospective Mode” for the full protocol.

Exit Criteria: All test programs produce identical output with and without optimizations. Zero leaks. Zero valgrind errors. Zero codegen audit findings. ./test-all.sh passes with 0 regressions across all ~N tests. RC operation reduction measured and documented. Compile-time overhead < 5%.