0%

Section 13: Burden Verification Suite

Goal: Adopt the six transferable methodologies plans/completed/aims-proofing-suite invented, applied BURDEN-SPECIFIC: mechanically bind the shipped burden emission/elimination/lowering sites to their governing proven calculus (CH-1..CH-comp, RL-comp RL3_elision_net_preserving, DP-2/DP-3) so drift is caught at build-time + test-all-time. This is the tooling §10’s terminal verification RUNS; §13 BUILDS it. Replaces the generic copy-paste verification of plans/llvm-verification-tooling (stripped by §14) with proof-bound, burden-aware conformance.

Context: The completed proofing suite shipped a reusable methodology, not just proofs:

  1. AST-probe-binds-proof-to-shipped-code — aims-proof/checker/build.rs parses compiler source AST and emits pub const probe markers the conformance gate consumes; drift between proof and code is mechanical, not reviewer-time.
  2. Conformance cross-walk with 3-verdict manifest — check-section-05-compiler-conformance.sh (DP-1..DP-10 → impl tokens) + run-locality-conformance.sh + shipped-conformance-manifest.json (pass / divergent / divergent-pending).
  3. Dual-prover agreement — dual-discharge.sh + proof-lean-map.json: Ori-checker verdict ↔ Lean kernel verdict must agree (statement-parity prelude defeats vacuous Lean proofs).
  4. SMT counterexample adequacy — proofs/10-counterexample/ .smt2+.lean shapes, Expected UNSAT, with an asymmetric encoder-validation guard (known-SAT→SAT, known-UNSAT→UNSAT) so no UNSAT is vacuous.
  5. proven_by criterion binding — proven_by: frontmatter maps criteria to .proof artifacts + proof_status; FAIL-on-complete routes to /fix-bug not redesign (per §04B.N coverage guard).
  6. Affected-set checking — lefthook glob runs proof/conformance checks zero-cost on non-touching commits; env-var widening for full-corpus.

The burden architecture already grew its own real verification primitives (burden_balance.rs VF-1, burden_delta.rs, the VF-3 oracle.rs, the static check-section-05-compiler-conformance.sh DP-2/DP-3 burden cross-walk). §13 completes the methodology adoption on top of those primitives — burden-specific AST-probe + burden SMT shapes + burden dual-discharge rows + burden proven_by + burden-aware oracle — never a parallel mechanism (missions.md §AIMS invariant 5).

Why a section (not §10 subsections): §10.6/§10.7 carried the lighter proto-versions (a single design-oracle script + a single oracle-extension item). The full six-pattern adoption is independently-workable (its proof-bound deliverables depend only on the proof corpus + emission sites, buildable in parallel with §08/§09 per routing.md §4 independence test), has its own success criteria, and is a closed unit of value. §10.6/§10.7 are absorbed here; §10 re-points to consume.

Depends on: TWO-HALF split (the corpus-wide assertion gates on §09, NOT §07B). The TOOLING-BUILD half (13.1 probe, 13.2 cross-walk, 13.3 SMT shapes, 13.4 dual-discharge, 13.5 proven_by binding, 13.6 design-oracle) is §07B-CLASSIFICATION-gated: it depends on §07B’s frozen probe-gateable burden emission shape + the §07B classification of which shapes are §09.2-owned (the frozen_burden_shape_version contract), and on the proof corpus + emission sites — authored IN PARALLEL with §08/§09. The CORPUS-ASSERTION half (the corpus-wide VF-1=0 conformance run + the oracle asserting the burden path is the real RC emitter on EVERY value shape) is §09-ACTIVATION-gated: it cannot pass until §09.2 retires the predicate stack + completes the Phase-5 broad-shape emission (the burden path is the sole RC emitter corpus-wide ONLY after §09.2, NOT after §07B — §07B proves the probe-gateable surface self-sufficient + classifies the §09.2-territory residual but does NOT deliver corpus-wide completion). depends_on: ["07B", "09"] carries both halves; the §10 verification join already gates the corpus run on depends_on [09, 13], and this section’s dependency now aligns with that. §07A delivered the narrow-shape self-sufficiency; §07B proves the broad probe-gateable shapes (iterator-from-collection / fat-pointer-matrix / collection-element / SSO / generic) self-sufficient; §09.2 completes the JOINT remainder + is the TRUE corpus-wide sole-RC-emitter milestone §13’s corpus-assertion half binds against. FEEDS §10 (verification RUNS this suite).

Reference implementations: compiler_repo/aims-proof/checker/build.rs (AST-probe), scripts/check-section-05-compiler-conformance.sh (3-verdict cross-walk), scripts/dual-discharge.sh + scripts/proof-lean-map.json (dual-prover), proofs/10-counterexample/{README.md,results.json,bug-04-118.smt2} (SMT shape template + encoder-validation guard), plans/completed/aims-proofing-suite/section-13-04b-criterion-binding.md (proven_by binding), plans/completed/aims-proofing-suite/section-17-locality-shipped-conformance.md (manifest/probe/cross-walk), lean/AimsProof/Coexistence.lean (the CH-* mirror the burden shapes discharge against).

Intelligence Reconnaissance

Queries:

  • scripts/intel-query.sh --human file-symbols "compiler_repo/aims-proof/checker" --repo ori — checker/build.rs probe surface
  • scripts/intel-query.sh --human callers eliminate_burden_ops --repo ori — burden-op decision sites the probe + oracle bind
  • scripts/intel-query.sh --human callers emit_burden_ops --repo ori — Step-4b emission site the CH-5 phase-ordering probe checks
  • scripts/intel-query.sh --human file-symbols "compiler_repo/compiler/ori_arc/src/aims/verify" --repo ori — oracle.rs + burden_balance.rs extension surface

Queried: 2026-06-03.

Results summary (≤500 chars) [ori]: §13 EXTENDS existing infrastructure per missions.md §AIMS invariant 5 — build.rs probe pattern (proofing-suite), check-section-NN-compiler-conformance.sh cross-walk pattern, dual-discharge.sh + proof-lean-map.json, proofs/10-counterexample/ SMT corpus, VF-3 oracle.rs + burden_balance.rs. Zero parallel checkers; every burden-specific deliverable binds to a real CH-*/RL-comp/DP .proof + its Lean mirror. The static DP-2/DP-3 burden cross-walk already exists; §13 adds CH-2/CH-4/CH-5 + RL-comp + the runtime per-IR strengthening.

13.1 AST-probe conformance — binds burden emission sites to the proven calculus

File(s): compiler_repo/aims-proof/checker/build.rs (EXTEND the existing syn-AST probe)

  • Extend build.rs (mirroring its locality-variant + may_escape probe) to parse the burden emission/elimination sites via syn and emit pub const markers:
    • BURDEN_EMIT_AT_STEP_4B: bool — emit_burden_ops invoked after analyze_function, before realize_rc_reuse (CH-5 phase-ordering / PL-2).
    • BURDEN_ELIM_READS_FROZEN_STATEMAP: bool — eliminate_burden_ops takes &AimsStateMap (read-only), never &mut (CH-4 immutability).
    • BURDEN_ELIM_CONSUMES_DP2_DP3: bool — is_rc_dec_unnecessary (DP-2) + is_rc_inc_elidable (DP-3) called at burden-op sites in burden_elim.rs (CH-2 single-elimination).
  • Each marker carries cargo:rerun-if-changed= for its probed source path so a stale probe cannot bake into the binary (per build.rs precedent).
  • A renamed / moved / deleted site flips its marker → the 13.2 cross-walk reports divergent (FATAL). This is the mechanical drift detector that makes the CH-2/CH-4/CH-5 proofs mean something about shipped code.
  • Banned: a shell grep reflection of the source (the probe is AST-level per build.rs; grep is the cross-walk’s job, not the probe’s). Banned: probing for a value outside the recognized set without amending the manifest first (per build.rs forward-invariant — an unrecognized tuple routes to FATAL).

Subsection close-out (13.1) per protocol.

13.2 check-burden-conformance.sh — 3-verdict cross-walk

File(s): compiler_repo/aims-proof/scripts/check-burden-conformance.sh (new — extends the check-section-NN-compiler-conformance.sh family)

  • Author the cross-walk with a BURDEN_ROWS table ("RULE | target-file | required-token | description") mapping each burden-governing rule to its implementation token, following check-section-05-compiler-conformance.sh exactly:
    • CH-2 | burden_elim.rs | eliminate_burden_ops | single-elimination over the burden baseline
    • CH-4 | burden_elim.rs | fn eliminate_burden_ops(.*&AimsStateMap | reads frozen state map, never mutates
    • CH-5 | pipeline/aims_pipeline | emit_burden_ops | Step-4b emission after analyze_function
    • DP-2 | burden_elim.rs | is_rc_dec_unnecessary | dec-unnecessary at burden-op site
    • DP-3 | burden_elim.rs | is_rc_inc_elidable | inc-elidable at burden-op site
    • RL-comp | burden_balance.rs | verify_burden_balance | net-preservation conformance
  • 3-verdict output: pass (token present), divergent (token absent — FATAL, exit 2), divergent-pending (locality-carve-out rule blocked by plans/locality-representation-unification per the §17 shipped-conformance-manifest.json discipline — non-fatal, exit 0). Exit 3 on infrastructure failure (per check-proofs.sh exit-code contract).
  • Grep-based, sub-second, NO cargo build (the AST probe owns the build-time leg; this is the fast text leg) so it folds into test-all.sh preamble alongside check-debug-flags.sh (§14 wires it).
  • Tests: a token-present fixture → pass; a deliberately-renamed-token fixture → divergent exit 2; a carve-out rule → divergent-pending exit 0.

Subsection close-out (13.2) per protocol.

13.3 Burden SMT counterexample shapes

File(s): compiler_repo/aims-proof/proofs/10-counterexample/burden-{under-elim,over-elim,phase-ordering,stale-statemap}.{smt2,lean} + results.json + README.md (new shapes; extend the existing corpus)

  • Author four .smt2 + paired .lean shapes, each with the bug-04-118.smt2 header template (shape description, Expected: UNSAT, SAT would mean the calculus is defective, shape_id, source, fixture_path, Cited proven rules: list naming each rule ID + its .proof path):
    • burden-under-elim — eliminate_burden_ops removes a BurdenDec where DP-2’s antecedent (cardinality = Absent ∨ consumption = Dead) is FALSE → leak. Refuted by DP-2.proof + CH-2.proof → UNSAT.
    • burden-over-elim — Phase-7 lowering (BurdenInc→RcInc / BurdenDec→RcDec) nets ±1 over a path/SCC → double-free or leak. Refuted by RL-comp.proof (RL3_elision_net_preserving) → UNSAT.
    • burden-phase-ordering — burden emission fires before lattice convergence → violates CH-5 + PL-2. Refuted by CH-5.proof + PL-2.proof → UNSAT.
    • burden-stale-statemap — eliminate_burden_ops mutates the state map → violates CH-4. Refuted by CH-4.proof → UNSAT.
  • The asymmetric encoder-validation guard (fixtures/encoder-validation.smt2 known-SAT must return SAT, known-UNSAT must return UNSAT) covers these shapes — a vacuous-UNSAT encoder is caught before any burden-shape verdict is trusted (per proofs/10-counterexample/README.md lines 34-41).
  • Record each in results.json with route_target: feeds_burden_adequacy_verdict + the Z3 verdict; add a README.md row per shape (shape inventory pattern).
  • Banned: trusting an UNSAT verdict when the known-SAT fixture returns UNSAT (encoder-invalid → halt, fix encoding first, per the README routing table).

Subsection close-out (13.3) per protocol.

13.4 Dual-discharge + proof-lean-map rows for burden surface

File(s): compiler_repo/aims-proof/scripts/proof-lean-map.json (add rows) + lean/AimsProof/Coexistence.lean (the burden CH-* mirror — already exists; confirm coverage)

  • Add kind: theorem rows to proof-lean-map.json for every burden-governing CH-* rule (CH-1..CH-5 + CH-comp → lean_module: AimsProof.Coexistence, with parity_tokens from each .proof’s Soundness property:) so dual-discharge.sh enforces Ori-checker↔Lean verdict agreement on the coexistence surface the burden path depends on.
  • Add rows for the four 13.3 .smt2↔.lean burden shapes so the Lean kernel cross-validates each Z3 UNSAT (a Lean rejection of a claimed-UNSAT shape = ENCODER_INVALID halt per the counterexample methodology).
  • Confirm dual-discharge.sh (statement-parity prelude → Ori-checker full-corpus → lake build → per-theorem verdict comparison) exits 0 for every burden row. The statement-parity prelude is load-bearing: it prevents a vacuous Lean proof (True := by trivial) from falsely agreeing.
  • Banned: a burden row with kind: theorem and a null lean_theorem (parity-enforced kinds require a real Lean theorem; a foundation-only row is kind: foundation / unimplemented_engine_shape).

Subsection close-out (13.4) per protocol.

13.5 proven_by binding + burden-aware VF-3 oracle extension (absorbs §10.7)

File(s): this section’s frontmatter (proven_by: block) + compiler_repo/compiler/ori_arc/src/aims/verify/oracle.rs + burden_balance.rs (EXTEND — never parallel, per aims-proofing-suite §18.3 ownership note)

  • Add a proven_by: frontmatter block to this section mapping each suite-criterion to its governing .proof artifact + proof_status (per section-13-04b-criterion-binding.md schema): AST-probe/conformance → CH-2/CH-4/CH-5 (proven_sound); SMT shapes → DP-2/DP-3/RL-comp/CH-5 (proven_sound / reformulated_and_proven); oracle → DP/RL/CH proven-complete set. A FAIL on a proof_status: complete criterion routes to /fix-bug against the divergent site (NEVER redesign / NEVER void §05), gated by the §04B.N within-coverage guard (the aims-rules.md HISTORY 2026-05-28 terminal-state table is the deciding artifact).
  • PRIMARY — burden-aware per-IR oracle (absorbs §10.7 PRIMARY): extend the VF-3 oracle (oracle.rs) to assert on emitted burden-op IR that each burden-op decision point satisfies the proven antecedent of its governing rule — a BurdenDec-eliminated site satisfies DP-2 (AimsProof.Decision::DP2_is_rc_dec_unnecessary_table); a burden ledger that nets 0 over every SCC/path satisfies RL3_elision_net_preserving; a burden-emitted site satisfies CH-1 (AimsProof.Coexistence::CH1_burden_emitted_is_bridge: burden_emitted = burden_owned); the per-class coverage partition satisfies CH-comp.
  • COMPLEMENT — static cross-walk (do NOT duplicate, absorbs §10.7 COMPLEMENT): the DP-2/DP-3 burden-op-site mapping is ALREADY static-cross-walked by check-section-05-compiler-conformance.sh; the 13.2 check-burden-conformance.sh extends it to CH-2/CH-4/CH-5 + RL-comp. The oracle is the per-IR runtime strengthening over the SAME proven antecedents — not a parallel mechanism.
  • Consume proven-rule set as data: enforce ONLY proof_status: complete rules (kind: theorem | composition_folded in proof-lean-map.json ∩ proven_sound | reformulated_and_proven in the aims-rules.md terminal-state table). Locality-carve-out rules whose §17 manifest verdict is divergent-pending stay advisory (do NOT hard-fail a target-only rule the shipped 4-variant lattice cannot satisfy).
  • Tests: a burden-op IR fixture obeying the antecedents passes; an injected violation (BurdenDec eliminated where DP-2’s antecedent is false) → conformance error citing rule ID + site (negative pin). The asserted antecedent is the SAME one proof-lean-map.json maps to the kernel-checked Lean theorem (no second copy of the rule).
  • TPR checkpoint — /tpr-review covering 13.1-13.5.

Subsection close-out (13.5) per protocol.

13.6 aims-burden-design-oracle.sh + frozen_rule_version (absorbs §10.6)

File(s): compiler_repo/diagnostics/aims-burden-design-oracle.sh (new — absorbed from §10.6)

  • Author aims-burden-design-oracle.sh consuming the §00.1 walkthrough document + the 12-risk-shape matrix + the Five-Invariant matrix + decisions/01–04 dispositions, outputting pass/fail per shape + per invariant (per §00.3 + blind-spots cross_cutting[2]).
  • The script enforces the frozen_rule_version producer/consumer contract: VERIFY §00 frontmatter frozen_rule_version: v1 matches §05 frontmatter consumes_proof_product: v1 (drift → FROZEN_RULE_VERSION_MISMATCH error).
  • Record in §10’s body that §10.6 is absorbed here (§10 re-points; this section is the SSOT for the design-oracle).

Subsection close-out (13.6) per protocol.

13.R Third Party Review Findings

  • None.

13.N Completion Checklist

  • AST-probe ships (13.1); a renamed emission site flips the probe → cross-walk divergent.
  • check-burden-conformance.sh ships 3-verdict (13.2); folds into test-all preamble (wired by §14); token-rename → divergent exit 2.
  • Four burden SMT shapes ship UNSAT with encoder-validation guard green (13.3); results.json + README.md updated.
  • proof-lean-map.json burden rows added; dual-discharge.sh exit 0 for every burden row (13.4).
  • proven_by: block authored + coherence.py validates the rule: atoms; burden-aware VF-3 oracle extended; negative pin (injected DP-2 violation → error) passes (13.5).
  • aims-burden-design-oracle.sh + frozen_rule_version contract land (13.6); §10.6 absorbed.
  • §10 re-pointed: §10.6/§10.7 consume §13’s deliverables (§10 frontmatter depends_on includes 13; §10.6/§10.7 bodies reference §13 as the builder).
  • Affected-set lefthook glob added (burden_elim.rs + aims_pipeline + burden .smt2); ORI_RUN_BURDEN_CONFORMANCE=1 widening works; full proof corpus stays in aims-proofs.yml.
  • Plan annotation cleanup.
  • Plan sync per protocol.
  • /tpr-review passed (final); /impl-hygiene-review passed.

HISTORY

  • 2026-06-03 — §13 created via /create-plan --inline (routing.md §3 case b) — the Burden Verification Suite. User directive: close out aims-burden-tracking with insanely-overkill, proof-tightly-integrated verification tooling by adopting the six methodologies the completed aims-proofing-suite invented (AST-probe-binds-proof-to-shipped-code, 3-verdict conformance cross-walk, dual-prover agreement, SMT counterexample adequacy, proven_by criterion binding, affected-set checking) BURDEN-SPECIFIC — replacing the generic copy-paste verification of plans/llvm-verification-tooling (stripped by §14). Topology (user-approved 2026-06-03): §13 depends_on §07A, built in parallel with §08/§09, FEEDS §10; absorbs §10.6 (aims-burden-design-oracle.sh + frozen_rule_version) + §10.7 (VF-3 oracle extension + static cross-walk + proof-lean-map.json binding) into the full methodology. Every deliverable EXTENDS the unified model per missions.md §AIMS invariant 5 — zero parallel checkers; each burden-specific artifact binds to a real CH-*/RL-comp/DP .proof + its Lean mirror. CI disposition (user-approved): the fast grep cross-walk + VF-1 corpus gate fold into test-all.sh; the full proof corpus + Lean dual-discharge stay in aims-proofs.yml (the ~30min corpus cannot fit test-all’s 150s budget); nightly-verification.yml (sanitizers + Alive2) is deleted by §14.