AIMS Burden Tracking — Perceus + Registry
22 sections
Overview
Replace AIMS realization-time predicate stack (PIN-1..6 + class_payload_of + ssa_alias_classes-driven emission) with two-layer architecture: (1) Phase 5 ARC lowering emits structurally-maximal burden ops (BurdenInc/BurdenDec) from per-type BurdenSpec data registered in a new BurdenRegistry; (2) Phase 6 existing lattice optimizes the burden baseline (consumption mode shifts from emission-decision to elimination-decision; algorithm unchanged). Phase 7 becomes mechanical lowering. This is Perceus (Reinking et al., PLDI 2021) integrated into Ori's data-driven registry pattern; Roc adopted Perceus directly (roc#825, roc#5258). Source: compiler_repo/docs/ori_lang/proposals/approved/aims-burden-tracking-proposal.md (Approved 2026-05-08).
In Progress
2 sections
Broad-Shape Burden-Lowering RC-Ledger Self-Sufficiency (iterator/collection-element/matrix/SSO)
Prove burden-path RC-ledger self-sufficiency for the PROBE-GATEABLE broad value
Post-Convergence Partial Retirement + PIN-1..6 Predicate Retirement (proven-equivalence-licensed)
Retire emission-side predicate-stack: class_alive_after, pin4_class_emits_dec_set,
Planned
7 sections
aims-rules.md Internal Drift vs Proof Corpus — IC-7 bound labels / IC-3 iter_consumes
Reconcile three internally-inconsistent statements in `.claude/rules/aims-rules.md`
Verification — VF-1 Burden-Balance Check + VF-7 Rewrite-Soundness + Proven-Rule Conformance + Live AIMS-Bug Sweep + Closures + /sync-aims-spec
Final verification of the burden architecture: (a) VF-1 burden-balance check (per-edge balance dataflow + SCC net-zero obligation per §AIMS.9.1.1) runs in CI, enforcing the PROVEN RC net-preservation (RL-comp `RL3_elision_net_preserving` + the §10 counterexample `rc_per_path_invariant` UNSAT) on emitted burden-op IR; (b) VF-7 rewrite-soundness tier passes; (c) full ./test-all.sh regression sweep passes; (d) dual-execution parity confirmed (eval + LLVM identical observable behavior); (e) §10.7 proof↔implementation bridge — the VF-3 oracle + burden_balance enforce the proven DP/RL/CH antecedents on emitted IR (the leg that makes the Lean/aims-proof corpus mean something about shipped code); (f) the `aims-proofing-suite §18` dual-discharge gate is green for the burden-touched proof rows; (g) bug closures — a LIVE tracker search at §10 execution enumerates every AIMS-associated bug (never a frozen list), each verified against the post-burden build then closed-or-dispositioned; (h) /sync-aims-spec propagates Annex E §AIMS conditional rewrites unconditionally per §Spec governance.
AIMS Snapshot Baseline Rebake — Burden-Pass Output Drift Verification (proven-antecedent-gated)
|
Green-Gate Red Partition + Orthogonal Routing (proven-coverage-classified)
Make the expanded full-green terminal gate (00-overview.md Mission Success Criteria, 2026-05-29 reground) BOUNDED and HONEST by partitioning the current `./test-all.sh` red into (A) BURDEN-ATTRIBUTABLE failures — implementation-fidelity divergences from a PROVEN-COMPLETE AIMS rule (the failing shape is WITHIN the coverage of a `proven_sound`/`reformulated_and_proven` rule per the `aims-rules.md` terminal-state table) that this plan dissolves via §03A emission-fidelity + §05 elimination + §07 coverage + §09 predicate-stack/coexistence retirement — and (B) ORTHOGONAL failures whose correctness rests on a rule that is `pending`/`unprovable_with_gap_citation` OR that live in a different subsystem this plan does NOT cure — each enumerated and routed per routing.md. The classifier is the SAME §04B.N proven_by coverage-guard the whole plan runs on (SSOT: the aims-rules.md terminal-state table + the §10.7 conformance oracle), NOT a parallel heuristic. The partition prevents 'all red is a burden bug' (the banned scope error) and lets §10's full-green criterion close honestly: burden set → zero by migration-completion; orthogonal set → FIXED by plan close (hardened 2026-06-10 — tracking is the mandatory interim routing instrument per routing.md, NOT a terminal disposition; every orthogonal failure is driven to fixed-and-verified before the terminal gate reads green).
Burden Verification Suite — aims-proofing methodology adopted burden-specific (AST-probe conformance + burden SMT shapes + dual-discharge + proven_by binding + burden-aware oracle)
Build a burden-tracking-SPECIFIC verification suite by adopting the six transferable patterns the completed `plans/completed/aims-proofing-suite` invented (AST-probe-binds-proof-to-shipped-code, conformance cross-walk with 3-verdict manifest, dual-prover agreement, SMT counterexample adequacy, proven_by criterion binding, affected-set checking) — NOT the generic copy-paste verification tooling of `plans/llvm-verification-tooling` (FileCheck/Alive2/sanitizers, which §14 strips). The suite mechanically binds the burden emission/elimination/lowering sites to their governing proofs so drift between the proven CH-1..CH-comp / RL-comp / DP-2/DP-3 calculus and the shipped `emit_burden_ops` / `eliminate_burden_ops` / Phase-7 lowering is caught at build-time + test-all-time, never reviewer-time only. It ABSORBS the lighter §10.6 (`aims-burden-design-oracle.sh` + `frozen_rule_version` contract) and §10.7 (VF-3 oracle extension + static cross-walk + `proof-lean-map.json` binding) into the full methodology. Per `missions.md §AIMS` invariant 5: every deliverable EXTENDS the unified model (the proof corpus, the VF-3 oracle, the `check-section-NN-compiler-conformance.sh` pattern) — zero parallel checkers, zero shadow trackers.
llvm-verification-tooling Teardown + AIMS-Foundation Absorption + test-all Fold
Retire the generic copy-paste verification tooling of `plans/llvm-verification-tooling` (FileCheck/sanitizers/Alive2 — not AIMS-burden-aware) and consolidate verification on the burden-specific suite §13 builds, folded into `test-all.sh`. Three moves: (1) DELETE the pointless standalone CI surface — `compiler_repo/.github/workflows/nightly-verification.yml` + its sanitizer/Alive2 scripts + corpora — after a verify-before-delete confirmation that each is non-burden-bearing; (2) ABSORB BY REFERENCE the genuinely-AIMS-specific foundations from llvm-verification-tooling that already ship + already run in test-all transitively (§03 AIMS pass-level snapshots, §04 lattice property tests, §05 contract oracle, §06 protocol-builtin matrix) — no rewrite, the §13 suite + §10 verification consume them; (3) WIRE `run_aims_burden_verification` into `compiler_repo/test-all.sh` (the §13 fast conformance cross-walk + the already-active burden-balance VF-1 corpus gate), and mark `plans/llvm-verification-tooling` superseded with a HISTORY pointer here, cutting its not-started §10-13 (differential fuzzing / CI / dashboard / AI-gen) while preserving the residual-RC-op-metric + differential-oracle CONCEPT in a HISTORY note (concept may inform future burden work; not built here). Per CLAUDE.md §Git Safety the deletions are file removals via `git rm` (never `git checkout`/`restore`/`reset`); per the output-style look-before-deleting rule each target is inspected before removal.
TRMC Cross-Block Admission + Must-Fire Activation (calculus-first; terminal-substrate-gated)
|
Completed
13 sections
Phase A0 — Design Validation Gate (RL-31 Burden-Aware Walkthrough)
Demonstrate via concrete code path + worked examples that BurdenSpec.field_type
Burden Registry — Data Structures + Registration API
Implement BurdenRegistry with split builtin (ori_registry::burden::BURDEN_TABLE
Burden Composition — Generic Monomorphization + DropInfo Lift
Generic types' BurdenSpecs monomorphize at type-instantiation time (not at runtime via TypeId chasing); structural-burden-signature deduplicates monomorphizations; existing DropInfo/DropKind lift into BurdenSpec; non-AIMS consumers (LLVM codegen, ARC pipeline internal callers) re-pointed via thin wrappers.
Phase 5 — Trivial Burden Emission (ori_arc::lower::burden_lower)
Phase 5 ARC lowering reads each owned non-scalar SSA value's BurdenSpec and
Emission-Fidelity Repair — Burden Emission Faithful to Proven RL-1 / RL-2 / Per-Edge RC-Balance
Repair Phase-5 burden EMISSION to the proven RL-1/RL-2 calculus in the (C) coexistence era (LEDGER §B.2). Close-gate: coexistence-mirror landed + function-exit VF-1-clean post-mirror + dual-exec parity (closes BUG-04-121). Self-sufficient emission-alone VF-1 deferred-with-anchor to §09.
Recursive Types + Closures + Drop AUGMENT + Value Empty-Burden
Cover the four value-shape composition cases that exercise BurdenSpec beyond
Minimal Lattice Adaptation — Burden-Op Pipeline Wiring + DP-2/DP-3 Burden-Op
Wire `emit_burden_ops` into the AIMS pipeline (§04A.0); audit + verify TF-N/A
Prototype Gate (BLOCKS §05+) — Seven Concrete Criteria
Evaluate the burden architecture as shipped at §00-§04A (Phase 5 trivial emission
Phase 6 Lattice Rewrite + RL-31 Burden-Aware Path
Rewrite Phase 6 lattice as pure optimizer over burden-emitted baseline. The
Phase 7 Mechanical Lowering — BurdenInc → RcInc, BurdenDec → RcDec
Phase 7 (ARC Realization) becomes mechanical: surviving BurdenInc → RcInc,
Value-Shape Coverage Migration — Apply-Aliases / Closures / Sum-Payload / Jumpargs
Migrate the remaining value-shape coverage from predicate-stack ownership to
Burden-Lowering RC-Ledger Self-Sufficiency (predicate-stack-retirement precondition)
Make emit_burden_ops / lower::burden_lower emit a COMPLETE standalone RC ledger
Rule-File Sync — arc.md / aims-rules.md / canon.md §7.1 / missions.md §AIMS
Update in-tree rules files to reflect the burden architecture AND re-validate