0%

§11 AIMS Snapshot Baseline Rebake — Burden-Pass Output Drift Verification

§11.0 Discovered Work Context

FieldValue
Discovery date2026-05-16 (via ./test-all.sh baseline run)
Routing case (per routing.md §3)(b) Independently-workable in plan’s bounded context — snapshot drift correlates with burden-pass landings the plan owns
Insertion orderinginserts_after: 10 + depends_on: ["01", "02", "10", "12"] — §10 verification must complete (the §10.7 oracle that gates the rebake) before §11 baseline rebake makes sense; rebaking against an in-flight pass would create chum. §01 supplies the registry, §02 the composition the snapshot pins, §12 the ir_checks/ir_quality re-bless routing (§12.3).
Failures absorbed1 (aims_snapshots_across_all_passes_match_baselines at compiler/oric/tests/aims_snapshots.rs:28)
Pass commits implicated7eb8ced15, 1962eac1a, 412e0b181, e186e2754, 7ef8b75de, bc309465b, 3bb8aa725, f5a37d327 (post-2026-05-14 burden + drop-walk commits)

§11.1 Mission

Three-step classification + cure, gated on the proven calculus:

  1. Read the failure diff: cargo t -p oric aims_snapshots -- --nocapture produces snapshot-vs-baseline deltas for each canonicalize/normalize/realize pass output. Identify which pass(es) drifted.
  2. Classify each drifted pass output as (a) intended drift from burden-pass landings OR (b) unintended regression. Classification uses §11.2 anchors AND the proven-antecedent gate: a delta is intended-drift ONLY when the drifted output still satisfies the proven DP/RL/CH antecedents §10.7 enforces.
  3. Cure path:
    • (a) → ORI_BLESS=1 cargo test -p oric aims_snapshots rebakes baselines; commit message documents which burden-pass commits authorized the rebake; reviewer-facing diff highlights each delta vs prior baseline AND the proven-antecedent verdict that authorized it.
    • (b) → Cure code lands in compiler/ori_arc/ (or wherever the regression introduced); baseline stays unchanged; snapshot passes via correct pass output post-cure.

§11.2 Classification Anchors

Per CLAUDE.md §Invariant-Anchoring Before Test-Chasing — classify drift against the invariant the snapshot pins. The snapshot consumes two upstream predecessors (§01 supplies the BurdenRegistry + BurdenSpec registrations the snapshot’s BurdenInc / BurdenDec markers must match; §02 supplies the monomorphized burden-composition output whose drift the rebake verifies) and the §10.7 conformance oracle (the proven-antecedent gate). The snapshot baseline cannot be rebaked or regression-classified without §01 and §02 in place — a baseline rebaked against an incomplete registry (§01) or incomplete composition (§02) would pin a wrong burden shape.

AnchorTest for (a) intended driftTest for (b) regression
Proven-antecedent gate (§10.7 conformance oracle)Every BurdenInc/BurdenDec marker in the drifted output satisfies its governing proven antecedent — DP-2/DP-3 (AimsProof.Decision), RL-2/RL-4/RL-5 dec-placement + RL-comp net-preservation (AimsProof.Realization), CH-1/CH-2 burden=lattice decision (AimsProof.Coexistence). The drift is the proven shape landing in the snapshot.A marker VIOLATES a proven antecedent (a BurdenDec where DP-2’s antecedent is false; a ledger that does not net 0 over a path per RL3_elision_net_preserving) — the pass output is wrong; cure the pass.
canon.md §7.1 Invariant #1 (FipContract::Certified ↔ realized IR)Burden markers BurdenInc/BurdenDec appear where §01/§02 registered them; no unmatched alloc/deallocRealized IR shows alloc/dealloc not justified by certified contract — regression
canon.md §7.1 Invariant #2 (active rewrites preserve observable behavior)Pass output reflects only mechanical lowering changes from burden landingsPass output diverges in ways that would change observable behavior — regression
canon.md §7.1 Invariant #3 (no pass relies on stale summaries)All summaries match the post-burden lattice statePass output shows a downstream consumer reading pre-burden summary state — regression (sequencing bug)
aims-rules.md lattice dimension extensionsBurden landings extend lattice dimensions or add new contract fields per §AIMS Invariant #5Burden landings spawn independent RC paths / parallel escape enums / shadow uniqueness trackers — Invariant #5 violation

§11.3 Implementation Sketch

PhaseDescriptionFiles touched
§11.3.0 Discovery + proven-antecedent gatecargo t -p oric aims_snapshots -- --nocapture to surface the snapshot deltas; for each drifted pass output, run the §10.7 conformance oracle (ORI_VERIFY_ARC=1 over the snapshot fixture) to verify the burden markers satisfy their proven antecedents; classify each drifted pass output (a) vs (b) per §11.2; document classification + per-delta proven-antecedent verdict in this section’s HISTORY blockNone (Read-only on snapshot baseline + pass output)
§11.3.1 If (a) — rebakeORI_BLESS=1 cargo test -p oric aims_snapshots rebakes; review the diff snapshot-by-snapshot; commit message authorizes the rebake by citing burden-pass commits responsible for each delta + the proven-antecedent verdictcompiler/oric/tests/aims_snapshots/*.snap
§11.3.2 If (b) — cureCure code in the offending pass; baseline stays; test passes post-curecompiler/ori_arc/ (specific module TBD per §11.3.0 classification)
§11.3.3 Verificationtimeout 150 cargo t -p oric clean; sibling snapshot tests un-perturbed; dual-exec parity preserved; §10.7 oracle + dual-discharge.sh green on the rebaked baselineNone
§11.3.4 Cross-coveragetimeout 150 ./test-all.sh debug + release cleanNone

§11.4 Implementation Items

  • §11.3.0 Discovery + proven-antecedent gate: run snapshot test with --nocapture; capture the failure diff verbatim; run the §10.7 conformance oracle on each drifted pass output; classify per §11.2 anchors (a delta is intended-drift ONLY when it satisfies the proven antecedents); record classification + per-delta proven-antecedent verdict in this section’s HISTORY block.
  • §11.3.1 If classification is (a) intended drift: ORI_BLESS=1 cargo test -p oric aims_snapshots; review the diff snapshot-by-snapshot vs prior baseline; commit message documents which burden-pass commits authorize the rebake + the proven-antecedent verdict.
  • §11.3.2 If classification is (b) unintended regression: cure the offending pass in compiler/ori_arc/; baseline stays unchanged; snapshot passes via correct pass output.
  • §11.3.3 Verification: timeout 150 cargo t -p oric clean; sibling snapshot tests un-perturbed; the rebaked baseline PASSES the §10.7 conformance oracle AND compiler_repo/aims-proof/scripts/dual-discharge.sh is still green.
  • §11.3.4 Cross-coverage: timeout 150 ./test-all.sh debug + release clean.
  • §11.3.5 Burden-lattice coherence: post-cure snapshots reviewed against canon.md §7.1 Invariants #1-#5; no violation visible in baseline.
  • §11.3.R /tpr-review on §11 diff returns clean. Route every emitted /tpr-review exit_reason per the global exit-reason routing table (plans/completed/scripts-first-workflow-architecture/_archive/2026-05-15-pre-fold/skill-ecosystem-coherence/decisions/31-step-6-exit-reason-table-source.md) so autopilot dispatches each terminal state (clean → advance to §11.3.N; findings → fix-and-re-run within the round cap; cap_reached_with_substantive / cap_reached_clean → record review_pipeline: round state + classify per tpr-review/SKILL.md §5.5) rather than stalling on a non-clean exit. That global table is the SSOT for the routing; consume it, never re-derive it inline.
  • §11.3.N /impl-hygiene-review on §11 diff returns clean after TPR.
  • §11.3.Close flip status: → complete via the atomic-flip API per state-discipline.md §4.

§11.5 Banned Approaches

  • ORI_BLESS=1 rebake without classification — banned per CLAUDE.md §INVERTED-TDD. Rebaking without confirming the drift is intended is the test-weakening shape INVERTED-TDD:positive-test-modification.
  • ORI_BLESS=1 rebake of a delta that VIOLATES a proven antecedent — banned. A snapshot baseline that encodes a burden marker contradicting its governing proven DP/RL/CH rule (the §10.7 oracle rejects it) is a regression to CURE, never to bless. Blessing it would pin a proof-contradicting state — the strongest form of INVERTED-TDD:positive-test-modification.
  • #[ignore] on aims_snapshots_across_all_passes_match_baselines — banned per test-disposition.md. Snapshot tests pin invariants; ignoring is the failure mode they’re designed to catch.
  • Filing the drift as a separate BUG-XX-NNN entry — banned per routing.md §3 case (b); shared bounded context with the burden-tracking plan that owns the pass commits means absorption is correct.
  • Rebaking selectively (commit only the “obvious” deltas, leave others for “later”) — banned. Either ALL deltas are authorized by burden-pass commits + the proven-antecedent gate, or §11.3.0 surfaces the unauthorized ones for cure path (b). No partial-rebake middle ground.

Intelligence Reconnaissance

Date: 2026-05-16 (snapshot surface); 2026-06-02 (proven-antecedent gate reconciliation — §10.7 oracle + dual-discharge.sh confirmed as the rebake gate). Graph: HEAD be3a7ba.

  • [ori:compiler/oric/tests/aims_snapshots/] scripts/intel-query.sh file-symbols compiler/oric/tests/aims_snapshots --repo ori — discovery surface for baseline files (run during §11.3.0 to inventory all .snap files affected).
  • [ori:compiler/ori_arc/src/aims/] scripts/intel-query.sh file-symbols compiler/ori_arc/src/aims --repo ori — discovery surface for AIMS pass code paths possibly responsible for unintended drift (cure-path (b) candidates).
  • [ori:compiler/ori_arc/src/lower/burden_lower] scripts/intel-query.sh file-symbols compiler/ori_arc/src/lower/burden_lower --repo ori — discovery surface for §03 phase-5 trivial-emission walker landed in 1962eac1a (one of the implicated commits for snapshot drift).
  • [ori:compiler/ori_ir/src/ir/instructions/] scripts/intel-query.sh symbols BurdenInc --repo ori — discovery surface for BurdenInc/BurdenDec ARC IR markers landed in 7eb8ced15 (snapshot drift consumer).
  • [ori] CPG queries (callers/callees) on burden_lower + BurdenInc/BurdenDec may return empty until intel-query.sh refresh --code runs against current HEAD; §11 verification consumes graph state via direct Read at execution-time per plan-read-discipline.md §3.1.

§11.6 References

  • compiler/oric/tests/aims_snapshots.rs:28 — failing test
  • compiler/oric/tests/aims_snapshots/*.snap — baseline files (rebake targets under cure path (a))
  • compiler/ori_arc/ — burden-pass source (cure targets under cure path (b))
  • compiler_repo/compiler/ori_arc/src/aims/verify/oracle.rs — the §10.7 proven-antecedent oracle (the rebake gate)
  • compiler_repo/aims-proof/scripts/dual-discharge.sh — proof-corpus dual-discharge (must stay green over the rebake)
  • compiler_repo/aims-proof/lean/AimsProof/{Decision,Realization,Coexistence}.lean — the proven DP/RL/CH antecedents the rebake is gated against
  • Commits implicated in burden-pass output drift: 7eb8ced15 feat(arc): add BurdenInc/BurdenDec ARC IR markers, 1962eac1a feat(ori_arc): trivial burden emission walker + symmetric VF-1 scalar filter, 412e0b181 feat(ori_arc): burden_dec variant-walk + LLVM drop_enum dispatch, bc309465b feat(ori_arc): include deeper-nested test files missed by mod-orphan triage, 7ef8b75de refactor(ori_arc): decompose emit_burden_ops; doc-comment cleanup, 63b540d42 refactor(compiler): impl lookup + ARC intraprocedural alias plumbing, e186e2754 feat(typeck): conditional-partial-move validator + pre/post-contract validation + tagged_ptr drop walk
  • .claude/rules/canon.md §7.1 — Five Load-Bearing Invariants (classification anchor)
  • .claude/rules/aims-rules.md — AIMS lattice dimension SSOT
  • .claude/rules/missions.md §AIMS — AIMS mission (parallel-pipeline ban for Invariant #5 classification)
  • CLAUDE.md §Invariant-Anchoring Before Test-Chasing
  • CLAUDE.md §INVERTED-TDD Is BANNED
  • section-10-verification.md — preceding section; §11 depends_on §10 because the §10.7 conformance oracle is the rebake gate, and rebaking against in-flight passes would create churn
  • section-12-green-gate-red-partition.md §12.3 — routes ir_checks / ir_quality_attributes FileCheck re-bless to this section’s discipline

HISTORY

  • 2026-06-02 — Reworked §11 to gate the rebake decision on the proven calculus (the §10.7 conformance oracle) + DAG fix. The (a)-intended-drift vs (b)-regression classification was strengthened from a canon-§7.1-invariant + visual-diff judgment to a PROVEN-ANTECEDENT-GATED binary: a delta is intended-drift (a) ONLY when the rebaked pass output still satisfies the proven DP/RL/CH antecedents §10.7 enforces (AimsProof.{Decision,Realization,Coexistence}); a delta that violates a proven antecedent is a regression (b) to cure, and ORI_BLESS=1-blessing it is now an explicit Banned Approach (the strongest INVERTED-TDD:positive-test-modification — pinning a proof-contradicting state). Added a proven-calculus-coherence success-criterion (the rebaked baseline passes the §10.7 oracle AND dual-discharge.sh stays green) + a §11.3.0 proven-antecedent gate step. DAG fix: depends_on corrected from ["10"] to ["01", "02", "10", "12"] — matches the §11.2 body (which already cited 01 + 02 as the registry/composition basis) and adds §12 (its §12.3 routes the ir_checks/ir_quality FileCheck re-bless into this section’s discipline). All Lean references use lean/AimsProof/<Module>.lean.
  • 2026-05-16 — Section created via /create-plan --inline inline-insertion: ./test-all.sh baseline (2026-05-16) recorded 1 failure on aims_snapshots_across_all_passes_match_baselines (compiler/oric/tests/aims_snapshots.rs:28). Snapshot drift correlates with post-2026-05-14 burden-pass landings + tagged_ptr drop walk in commit e186e2754. Routed via /create-plan --inline aims-burden-tracking per routing.md §3 case (b) — independently-workable in plan’s bounded context; commits implicated are this plan’s own deliverables. Section absorbs the classification + cure work as a sibling section AFTER §10 verification (depends_on §10 because rebaking against in-flight passes would create churn). Classification step §11.3.0 deferred until §10 reaches stable state.