86%

S03 Logical ledger planner core - Stage B + Stage C behind one migration toggle

Goal

The class-ledger planner (logical event classification + owed-invariant placement) exists behind ONE compiled-counter migration toggle, green on the walking-skeleton family, with transfer_anchor_net’s lineage model promoted from post-hoc repairer to the planner’s verify core (the readiness gate). Transitional Burden* spellings are carrier details; the planner does not prescribe a runtime counter mechanism.

Algorithm spec (authoritative for this plan)

  • Stage B events per class member use: CONSUME = the RL-2 nine transfer kinds + owned call position + borrowed_cow_consumed position + iter-consume (iter_consumes && !transfers_through_return); READ = borrow positions, Project views, comparisons, IsShared; MUTATE = Set/mutating builtin on a Dynamic-COW class; BIRTH kinds = FRESH/FOREIGN/BORROWED/OPAQUE/MERGE; CREDIT = RL-34 anchor + sharing-view producer.
  • Stage C per class: owed equal on all edges into every merge; inc before CONSUME iff class-live-after (borrowed-rooted classes always inc at consume); RL-4 edge decs (Jump-arg exempt); RL-5 dead-at-entry decs; exactly ONE dec after the class’s last READ per path segment, local, never hoisted past a merge; per-field aggregate decomposition (skip consumed field classes); unwind edges run the same rule; RL-DROP userDrop unchanged.
  • The invariant enforced (and verified by the promoted transfer_anchor_net core) is abstract owner-credit balance: per class per path net=0; available logical credit >= 1 at every READ and >= 1 + live siblings at MUTATE. A counter-based adapter may map this to increments/decrements, but the VM or another physical plan need not.

Work Items

  • Implement Stage B event classifier over partition classes: RL-2 twelve terminal-use kinds + contract facts (iter_consumes && !transfers_through_return, borrowed_cow_consumed, owned positions, credits) -> BIRTH/CONSUME/READ/MUTATE event streams per class
  • Implement Stage C owed-invariant dataflow as the Phase-5 emitter behind ONE toggle: per-edge owed tracking equal across merge entries; BurdenInc before a CONSUME iff class-live-after (borrowed-rooted classes always inc at consume); RL-4 edge decs (Jump-arg exempt); RL-5 dead-at-entry decs; exactly one dec after the class’s last READ per path segment, never hoisted past a merge; per-field aggregate decomposition (skip consumed field classes); unwind edges same rule; RL-DROP userDrop unchanged; promote transfer_anchor_net’s lineage model as the verify core and readiness gate
  • Walking-skeleton family green under the toggle: straight-line fresh + move + read shapes; VF-1.1 burden-balance zero on covered family; gated burden-sole probe zero-new vs baseline on covered family; evaluator/VM/LLVM debug/release/AOT behavior parity, exact logical ownership/drop/unwind-event correspondence, and leak freedom green
  • Build the emitter-vs-scan differential harness: per-family A/B compare (toggle on vs off) emitting the cutover worklist consumed by S04-S06
  • Full ./test-all.sh green with toggle OFF by default; cross-executor parity plus exact ownership-event and leak legs on the skeleton corpus

Governing rules (embedded per plan self-containment)

  • Calculus-first per arc.md CP-1: the governing theorem lands in compiled Lean BEFORE the consumer ships; never weaken a theorem to pass a shape; four-surface sync per CP-2 on every AIMS change.
  • Verdict surface until S08 lands: the gated burden-sole probe ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1 via compiler_repo/diagnostics/aot-guardrail.sh --floor (debug AND release), zero-new vs compiler_repo/compiler/ori_llvm/tests/aot/fixtures/corpus_under_flag_gate/baseline_failing_ids.txt. The default path is FALSE-GREEN until S08 (per arc.md STOP); never cite it as an RC verdict.
  • test-all is the compiler-state SSOT: every section-close verdict comes from a full ./test-all.sh run (background, flock-serialized; consume test-all-summary.json), never targeted runs alone.
  • Banned cures (each a carried dead-end): use-count/type-membership PROXY discriminators (DE-150/174/175); broadening compute_genuine_same_alloc_reps / ForwarderUnionFind phi edges (DE-181); relocating a release past a multi-pred merge (DE-225/243/249/250); inc-only pair splits (attempt-287 290-UAF class); broad caller-side keep-alive incs (DE-254).
  • Every retired scan/toggle records a KEPT ledger cycle with before/after teeth (collapse metric + floor).
  • Cross-executor parity over evaluator, VM, LLVM debug/release/AOT, and admitted native/direct-WASM/JIT projections, plus exact logical ownership/drop/unwind-event correspondence and leak freedom, are per-section backend legs (L9 + L10). The AOT burden probe remains a current LLVM-projection migration gate, not the definition of AIMS correctness.

Test strategy

  • VF-1.1 burden-balance zero corpus-wide on covered family; gated probe zero-new on covered family; eval parity (ori test) green.
  • Differential harness output = the S04-S06 cutover worklist (per-family A/B diff toggle on/off).
  • Semantic pins: skeleton shapes (fresh-move, fresh-read-dec-after-last-read, dead-on-arrival) + negative pins (no dec before read; no dec past merge; borrowed consume incs).
  • Implement Stage C owed-invariant dataflow as the Phase-5 emitter behind ONE toggle: per-edge owed tracking equal across merge entries; BurdenInc before a CONSUME iff class-live-after (borrowed-rooted classes always inc at consume); RL-4 edge decs (Jump-arg exempt); RL-5 dead-at-entry decs; exactly one dec after the class’s last READ per path segment, never hoisted past a merge; per-field aggregate decomposition (skip consumed field classes); unwind edges same rule; RL-DROP userDrop unchanged; promote transfer_anchor_net’s lineage model as the verify core and readiness gate by GENERALIZING its existing classify_model-shaped check (which already gates on compute_burden_entry_nets’s converged bool before disagree_blocks before the per-path leak/negative checks) to run once per partition class, REUSING compute_burden_entry_nets’s proven freeze-on-disagree termination and fail-closed converged signal rather than authoring a parallel per-class net computation; before the promoted verify core is trusted as any family’s readiness gate (including the walking-skeleton family in this section), author and land an adversarial regression pin — a cyclic/back-edge partition-class CFG lineage reproducing BUG-04-237’s exact non-convergence shape (a loop-header whose back-edge predecessor’s exit net is a function of the header’s own entry net, non-zero per-iteration class delta) — asserting the promoted verify core reports a fail-closed non-Clean verdict, never a false Clean, on that shape

Items

  • Discharge the executable-partition bridge obligation BEFORE the emitter consumes partition classes as a proof surface (calculus-first per arc.md CP-1): prove in compiled Lean that buildPartitionUF’s computed representatives realize the inductive SameRep RST-closure of the admitted edge list (general theorem, not only the Part D concrete witnesses); lake build clean; .proof + proof-lean-map.json row + CP-2 four-surface sync. Discovered at S01 section-close TPR (codex-F2): Partition.lean asserted the correspondence in a comment; class_eq_iff_sameRep only unfolds sameRep’s own definition.

Fresh intel (regenerated)

The world changed under this section since its prior dossier (the durable sidecar at content/intel/ledger-emitter-core--s-7769cdaa.intel.md, generated when the plan was 0/11 started). Three state changes are decisive, and one brand-new source-verified finding sharpens w-d4feaddd from “discharge a stated obligation” into “the obligation is UNPROVABLE as informally stated — the executable definition must change shape first.”

First — the prior dossier’s sharpest risk is ALREADY CURED in shipped code. Its refutation verdict said the verify-core promotion is unsafe “until compute_burden_entry_nets’s convergence status is surfaced as a distinct, fail-closed signal.” That landed: BurdenEntryNets.converged: bool (aims/verify/burden_delta.rs:47, set at :137), the BalanceViolationKind::ConvergenceExhausted fail-closed verdict variant (burden_delta.rs:166-178, hard branch at :248), and transfer_anchor_net::verify::classify_model returning NetVerdict::Unprovable on !nets.converged FIRST, before any per-path check (verify.rs:83-84). w-e27a77a2’s text already reflects this (“gates on compute_burden_entry_nets’s converged bool before disagree_blocks before the per-path leak/negative checks”). What REMAINS from that work item is the adversarial regression pin: a cyclic/back-edge partition-class CFG reproducing BUG-04-237’s exact non-convergence shape, asserting the promoted verify core reports fail-closed non-Clean, never a false Clean. The mechanism exists; the pin that stops it regressing does not.

Second — the S02 substrate is real, shipped, and consumed by exactly one production reader. BirthSitePartition (intraprocedural/birth_site_partition.rs:79, per-(ArcVarId, FieldPath) union-find with per-class COW-boundary taint) is populated by compute_birth_site_partition (birth_site_population.rs:28) at the Step-4a-to-4b pipeline slot (pipeline/aims_pipeline/mod.rs:243-247) onto AimsStateMap (state_map.rs:296,515,520); the SOLE non-test reader is the Phase-6 presence debug_assert at burden_elim.rs:182-186. S03’s Stage B (w-0803928b, in-progress) is the FIRST real consumer. The phi admission is witness-gated exactly as PV-1 demands (union_phi_witnessed, birth_site_partition.rs:149 — singleton birth-site witness or refuse).

Third — the NEW load-bearing finding (source-verified this run): the w-d4feaddd bridge theorem is FALSE for the executable as currently defined. Partition.lean defines PartitionUF.find as a FUELLED walk with hard-coded partitionFuel := 16 (Partition.lean:63-68), union as link-by-root with NO rank and NO path compression (:71-75), and buildPartitionUF as a plain fold (:77). Link-by-root without rank means N chained unions (union 1 2; union 2 3; ...) build a parent chain of length N; for any admitted edge list whose chain exceeds 16, find truncates at a NON-root and sameRep reports false for genuinely-unified nodes. So the general theorem “buildPartitionUF’s computed representatives realize the inductive SameRep RST-closure of the admitted edge list” — quantified over ARBITRARY edge lists with the fuel fixed at 16 — has a concrete counterexample (a 17-union chain). The Lean file’s own obligation comment (Partition.lean:98-105) says the correspondence is “a stated model obligation discharged concretely on the T1 witness instances (Part D), not yet a kernel-checked theorem” — Part D’s witnesses (:229-262) discharge by decide on instances whose chains stay far below 16, which is why nothing has tripped. [JOIN] this is exactly the failure mode the external verified-union-find literature is organized around: Batteries (Lean 4’s own stdlib UF) avoids fuel entirely via rank-based well-founded recursion + the parentD_lt/rankD_lt structure invariants, and defines Equiv a b := rootD a = rootD b with root-preservation lemmas — the theorem SHAPE w-d4feaddd needs. Discharging w-d4feaddd therefore requires an executable-definition change (fuel parameterized by the edge list, e.g. edges.length + 1, with a proven chain-length bound — the minimal-diff option preserving Part D’s decide witnesses) or a well-founded-recursion rework (Batteries-shaped, bigger churn), THEN the two-directional closure correspondence by fold induction. Per CP-1 case (b) this is a legitimate calculus CORRECTION (the executable model is incomplete for the general case), not a weakening — and per the obligation’s own text, no consumer may rely on the executable partition as a proof surface until it lands.

Fourth — sequencing. w-0803928b (Stage B classifier) is already in-progress, and that is fine: CODE may be authored against the partition. What is gated is TRUST — the promoted verify core certifying any family, and the emitter’s placement claims being treated as PV-2-governed, both require the bridge theorem first (calculus-first, arc.md §CP-1; the section’s own Items block says “BEFORE the emitter consumes partition classes as a proof surface”). The practical order: land w-d4feaddd (Lean-only, no Rust dependency, independently committable with CP-2 four-surface sync) in parallel with or immediately after the in-flight Stage-B classifier code, and BEFORE w-b4f70683/w-e27a77a2’s verify-core promotion flips any readiness verdict.

Decisions this package forces:

  1. Treat w-d4feaddd as a definition-change + theorem, not a theorem alone. Fix the fuel (parameterize by edges.length + 1 with a chain-length-bound lemma, or rework find to well-founded recursion per the Batteries shape) before attempting the closure correspondence; a direct attempt against fixed fuel 16 will dead-end on the 17-chain counterexample. Both directions needed: soundness (sameRep = true -> SameRep) by a per-union invariant “every parent edge is closure-derivable”; completeness (SameRep -> sameRep = true) by fold induction with a roots-stay-equal preservation lemma.
  2. Do NOT discharge the general theorem by decide — that path is instance-only (Part D’s job) and the lean4 sentiment tier (§8) shows decide/native_decide-family kernel-reduction pain at the 95-100th percentile; Partition.lean already runs at maxHeartbeats 1000000. The general theorem is an induction proof.
  3. CP-2 lands with it: .proof artifact under proofs/12-provenance/, proof-lean-map.json row, aims-rules.md §12 PV-1 text updated (the “stated model obligation” clause deleted/flipped), Annex E prose untouched-or-synced, lake build + dual-discharge.sh + check-proofs.sh clean. Ledger.lean:930’s class_eq_iff_sameRep and ProvenanceComposition.lean:96-99’s consumption stay valid (they bridge executable-to-its-own-Boolean; the new theorem bridges executable-to-closure — complementary, not overlapping).
  4. Author the w-e27a77a2 adversarial pin against the SHIPPED fail-closed mechanism (the BUG-04-237 cyclic shape must yield NetVerdict::Unprovable via the verify.rs:83 converged gate), and keep it as a REGRESSION pin — the mechanism exists today; the pin’s job is stopping a future refactor from silently dropping the gate ordering.
  5. Constrained symbols unchanged (DE-181 teeth): never broaden compute_genuine_same_alloc_reps (project_aliases.rs:225), ForwarderUnionFind (ownership_scans/union_find.rs:21), or ssa_alias_classes::UnionFind (ssa_alias_classes.rs:198) — all three verified live at those lines this run. Build alongside via BirthSitePartition; the S02 close-out’s tier1_parity_with_genuine_same_alloc_reps pin is the sanctioned coexistence bridge.
  6. Coordination: BUG-04-112 (RCA/TDD/impl all in-progress) and BUG-04-120 (RCA in-progress) still actively edit emit_unified.rs (re-verified via symbol-plans this run); aims-proofing-suite is in-progress 7/21 with 135 blockers on the same Lean modules. Check both before landing Stage-C code or Lean edits.
["compute_genuine_same_alloc_reps", "ForwarderUnionFind", "ssa_alias_classes::UnionFind", "apply_sibling_moved_field_union_with", "PostDomCascadeRelocation", "PerFieldReleaseAccounting", "SoleOwnerFieldOriginCertificate", "PerFieldSameAllocUnionFind"]

DIG DEEPER

python -m scripts.plan_corpus.read plans/aims-provenance-ledger
sed -n '55,110p' compiler_repo/aims-proof/lean/AimsProof/Partition.lean   # the fuelled find + the obligation comment
sed -n '60,130p' compiler_repo/compiler/ori_arc/src/aims/realize/transfer_anchor_net/verify.rs

(full dossier: ledger-emitter-core—s-7769cdaa.intel.md)