0%

Section 08A: aims-rules.md Internal Drift vs Proof Corpus

Goal: Reconcile three internally-inconsistent aims-rules.md statements against the proof corpus + contract code. Doc-only; extends the §08 aims-rules.md ↔ proof-corpus coherence edge. No calculus change, no rule weakened.

Discovery provenance: /condensate round-2 cold-context decodability agent (2026-06-12) flagged all three as cold-reader CANNOT-DECODE items; routed here via /add-bug relatedness verdict (symbol overlap with this plan) + routing.md §3 case (b) classification (independently-workable sibling; §08 complete, §07B scope-mismatched).

Grounding evidence already verified at insertion time (re-verify at execution; per Zero Assumptions):

  • IC-7-convergence.proof lines 23-76: spec per-param height = 13 (omits may_escape); shipped = 17 (retains the stored carrier, contract/mod.rs:269); EffectSummary spec 6 vs shipped 5; dominance (17×p + 8 + 5 + 4) >= (13×p + 8 + 6 + 4) for all p >= 0 discharged. The aims-rules.md provenance-table IC-7 Notes mislabels ×17 as “target formula” — the proof calls 17 SHIPPED.
  • ParamContract.iter_consumes shipped at compiler_repo/compiler/ori_arc/src/aims/contract/mod.rs:386 with join documentation at mod.rs:259; absent from the aims-rules.md §5 IC-3 join enumeration that §8 RL-2 cites.
  • No proof_status: field exists in aims-rules.md; the flip-state lives in §04B proven_by entries + the HISTORY terminal-state table per 00-overview.md §Mission reground.

Intelligence Reconnaissance

Queries (run 2026-06-12):

  • scripts/intel-query.sh --human callers iter_consumes --repo ori — no callers indexed (the field is consumed via struct access, not call edges).
  • scripts/intel-query.sh --human file-symbols "aims/contract" --repo ori — 30 symbols; ContextBehavior + join + default in context.rs; ParamContract join surface in mod.rs.

Results summary (≤500 chars) [ori]:

  • [ori:compiler/ori_arc/src/aims/contract/mod.rs] iter_consumes: bool at :386, join doc at :259, init false at :473 — the IC-3 join surface §08A.2 grounds on. [ori:compiler/ori_arc/src/aims/contract/context.rs] join at :70 (ContextBehavior PL-11 join, distinct surface). Direct artifact reads supplement the graph: IC-7-convergence.proof lines 23-76 carry the spec-13 / shipped-17 attribution §08A.1 reconciles.

Rules woven in (binding on every subsection)

  • Spec/rule edits are reviewer-gated by mechanical lints only (per CLAUDE.md §HYGIENE scope carve-out: .md rule files get no TDD matrix / dual-exec parity); the gates here are prose-lint.py, sync-aims-spec/check.py, and the rule-preservation read.
  • arc.md §CP-2 four-surface sync: these edits touch surface 3 (rule files) ONLY as label/citation corrections; surfaces 1/2/4 (compiled Lean, .proof, Annex E) are NOT edited. Any finding that the PROOF is wrong escalates — never silently edit the corpus.
  • section-08-rule-file-sync.md §08.2 coordination: do NOT re-introduce or contradict the IC-3 may_escape removal direction (plans/locality-representation-unification/ owns it); the IC-7 carve-out note cites the locality plan, not a re-derivation.
  • Public-repo hygiene: aims-rules.md is wrapper-internal — plan-path citations permitted there; NEVER copy them into compiler_repo/ surfaces.

08A.1 IC-7 convergence-bound label reconciliation

  • Read compiler_repo/aims-proof/proofs/06-interprocedural/IC-7-convergence.proof in full; extract the proof’s own spec-vs-shipped formula labels + per-constant attribution (13 vs 17 = may_escape; 6 vs 5 = EffectSummary field count) + the dominance discharge.
  • Edit aims-rules.md §5 IC-7: keep the spec formula param_count × 13 + 8 + 6 + 4 as the target-system bound (the file defines the COMPLETE TARGET system); append a shipped carve-out note — shipped formula param_count × 17 + 8 + 5 + 4 (retains the may_escape stored carrier per the ArgEscaping carve-out; dominance over the spec bound proven) — matching the top-of-file shipped-status block pattern.
  • Edit the HISTORY provenance-table IC-7 Notes: correct “target formula param_count × 17 + 8 + 5 + 4” to label ×17 as the SHIPPED formula and ×13 as the spec/target, mirroring the proof’s wording (“dual obligation discharged: spec formula AND shipped formula dominance”).
  • Cross-check the corrected text against plans/locality-representation-unification/ direction (post-locality, may_escape becomes derived and the shipped height converges toward spec) — the carve-out note names that plan as the convergence owner.

08A.2 IC-3 iter_consumes join component

  • Read the IC-3 join implementation in compiler_repo/compiler/ori_arc/src/aims/contract/ (field mod.rs:386, join doc mod.rs:259, init mod.rs:473); extract the actual join operator for iter_consumes (expected OR, like may_share — VERIFY, never assume).
  • Edit aims-rules.md §5 IC-3: add iter_consumes(<operator>) to the componentwise-join enumeration with a one-clause pointer to §8 RL-2 (the sole consumer).
  • Confirm §8 RL-2’s “(IC-3 join)” citation now resolves; no RL-2 text change expected.

08A.3 proof_status flip-state deciding-artifact citation

  • Edit the aims-rules.md §Mission authority-flip sentence to name where proven_by: / proof_status: complete is recorded: the §04B prototype-gate proven_by entries (plans/aims-burden-tracking/section-04B-prototype-gate.md + decisions/gate-criterion-1-evidence.md) and the HISTORY per-rule terminal-state table as the within-coverage discriminator.
  • Keep the sentence’s normative force identical (ADVISORY-until-landed semantics unchanged); the edit adds the artifact citation only.

08A.R Third Party Review Findings

  • None yet.

08A.N Completion Checklist

  • python3 scripts/prose-lint.py .claude/rules/aims-rules.md exits 0.
  • python3 .claude/skills/sync-aims-spec/check.py clean.
  • Rule-preservation read: every normative statement in the pre-edit file survives with identical force (no MUST→SHOULD, no dropped carve-out).
  • Zero proof-corpus files touched (git status compiler_repo/aims-proof/ clean) OR the §CP-2 escalation path was taken and is recorded here.
  • Plan sync: 00-overview.md Quick Reference row flipped; this section’s frontmatter status: complete via the atomic-flip discipline.