89%

S01 Lean foundations - the calculus-first gate

Goal

Every theorem the ledger algorithm rests on is kernel-checked in the committed corpus BEFORE any emitter code ships. Zero existing theorems are modified; five additive obligations land (T1-T5) plus the composition extension covering the partition side-table.

Deliverables

  • T1 partition soundness (promoted from compiler_repo/aims-proof/lean/scratch/PerFieldBirthSiteUnionFind.lean): parametric samerep_birthsite_sound (RST-closure induction over admitted edges) + distinct_birthsite_no_phi_admission (over-unification unrepresentable under the singleton witness).
  • T3 running-refcount surface (promoted from scratch/KeepAliveRedundancyPrefixMin.lean): whole-pair elision under live same-class sibling sound; inc-only split unsound; bridged to proven RL-22/RL-23/RL-25.
  • T2 compositional placement (NEW, the main authoring): a CFG model (blocks/edges/back-edges/unwind/TRMC-rewritten tail calls) with events from the RL-2 twelve-kind table over partition classes, proving the three-clause invariant: net=0 per class per path; running count >= 1 at every READ; count >= 1 + live-siblings at Dynamic-COW MUTATE. The attempt-287 lesson binds: model events from REAL realization semantics (RL-2 kinds + real partition admission), and the gated probe stays the empirical arbiter over any model claim.
  • T4 contract-boundary composition + T5 frame-limited robustness; CH/PL/VF-comp extension for the partition as Invariant-5 avenue (c) typed input.
  • Cross-plan RASI decision record (repr-opt, locality-representation-unification, semantic-optimization-pipeline, ffi-boundary-safety).

Work Items

  • Promote T1 partition soundness from scratch/PerFieldBirthSiteUnionFind.lean into committed AimsProof (parametric over node universe + birth-site map: samerep_birthsite_sound by RST-closure induction; distinct_birthsite_no_phi_admission kill-criterion); lake build clean
  • Promote T3 keep-alive/whole-pair running-refcount theorem from scratch/KeepAliveRedundancyPrefixMin.lean into committed AimsProof, bridged to the proven RL-22/RL-23/RL-25 KnownSafe family (same-class sibling liveness = dominating-inc evidence; inc-only split proven unsound)
  • Author T2 compositional placement theorem: CFG-ledger model (blocks, edges, back-edges, unwind edges, TRMC-rewritten tail-call CFGs) with events derived from the RL-2 twelve-kind table + partition classes; prove the 3-clause invariant (per class per path net=0; running count >=1 at every READ; count >=1+live-siblings at Dynamic-COW MUTATE); model events from REAL realization semantics per the attempt-287 lesson - the gated probe stays the empirical arbiter
  • Author T4 contract-boundary composition lemma (owned param = BIRTH, owned arg = CONSUME, iter_consumes && !transfers_through_return = CONSUME, borrowed = READ, transfers_through_return = passthrough, sharing-view producer = CREDIT) + T5 frame-limited robustness (class ledger invariant under tier-1-edge-introducing transformations)
  • Extend CH-comp/PL-comp/VF-comp composition theorems to cover the partition as a typed side-table input (Invariant 5 avenue (c)); four-surface sync per arc.md CP-2 (compiled Lean, .proof mirrors, aims-rules.md + arc.md, Annex E AIMS)
  • Author cross-plan RASI decision record (decisions/) enumerating repr-opt, locality-representation-unification, semantic-optimization-pipeline, ffi-boundary-safety RC/placement assumptions vs the ledger design; declare interaction constraints
  • Section close gate (CP-1 checkpoint gating S03+): lake build clean zero sorry; dual-discharge.sh green; check-proofs.sh green; proof-lean-map.json rows for every new theorem

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).
  • Dual-execution parity (interp == LLVM) + ORI_CHECK_LEAKS=1 leak-freedom are per-section backend legs (layer-coverage L9 + L10); debug AND release both green.

Test strategy

  • lake build clean, zero sorry; dual-discharge.sh (Ori-checker <-> Lean verdict agreement); check-proofs.sh regression gate; proof-lean-map.json rows per theorem.
  • Negative witnesses in-corpus per theorem (the buggy shape provably rejected: non-witnessed phi union, inc-only split, pre-read release).
  • No Rust behavior change this section: full ./test-all.sh green as a no-op check.

Items

  • Section close gate (CP-1 checkpoint gating S03+): lake build clean zero sorry; dual-discharge.sh green; check-proofs.sh green; proof-lean-map.json rows for every new theorem; /sync-aims-spec —check green confirming aims-rules.md + Annex E §AIMS carry T1-T5 + composition theorem content (CP-2 four-surface sync closed before S02 begins, not deferred)
  • Sync aims-rules.md + arc.md + Annex E §AIMS with T1 (partition soundness), T2 (compositional placement), T3 (keep-alive whole-pair elision), T4 (contract-boundary composition), T5 (frame-limited robustness): each new theorem gets its own rule-anchor entry in aims-rules.md, a shipped-surface note in arc.md, and a description in Annex E §AIMS, per arc.md CP-2 four-surface sync (compiled Lean is authoritative; the other three surfaces are projections that MUST match, in the same change set — the section’s own Governing rules already commit to this on every AIMS change); verify via /sync-aims-spec —check green

Fresh intel (regenerated)

S01’s own “author 5 new Lean theorems” framing is STALE. The compiled Lean corpus this section’s Deliverables describe as pending (T1 partition soundness, T2 compositional placement “NEW, the main authoring”, T3 keep-alive, T4 contract-boundary composition, T5 frame-limited robustness, plus the CH/PL/VF-comp composition extension) is already landed on HEAD, zero sorry, checker-verified clean — compiler_repo/aims-proof/lean/AimsProof/{Partition,Ledger,RunningCount,ContractBoundary,ProvenanceComposition}.lean (368/1499/260/1777/745 lines) all shipped in ONE commit, 3fa52183a (feat(arc): add AIMS birth-site partition analysis and provenance proofs, 2026-07-03 06:46:33, --bypass), which is an ancestor of the current HEAD. aims-proof/scripts/check-proofs.sh on the six 12-provenance/*.proof artifacts reports “6 proofs checked, 0 definition_only skipped, 0 regressions” right now (§3.9). The SAME commit shipped an executable Rust prototype of the T1 population pass (birth_site_partition.rs + birth_site_population.rs), test-verified for parity against (and provable divergence from) the legacy compute_genuine_same_alloc_reps union-find. CORRECTION (section-close TPR, 2026-07-05): the population pass IS wired into the production AIMS pipeline (aims_pipeline/mod.rs populates state_map.set_birth_site_partition after Step 4a — the S02 partition-infrastructure deliverable, read-only downstream per PL-5/PL-comp); the partition side table has no downstream CONSUMER until the S03 emitter ships, so the wiring is behavior-neutral, but it is NOT a disconnected prototype.

Yet the plan’s own recorded success criterion for this section (sc-5086f7f8, gated on dual-discharge.sh) still reads verdict_status: pending / no-evidence-recorded (§6). Nobody has re-run the verification-and-close step since the code landed two days before this dossier was generated.

Decisions this package forces before any Lean is written or any work item is touched:

  1. Do NOT re-author T1–T5. Run compiler_repo/aims-proof/scripts/dual-discharge.sh + check-proofs.sh (full corpus) + cd compiler_repo/aims-proof/lean && lake build to close out sc-5086f7f8 and verify-and-complete the section’s work items against what already exists. The scratch files this section’s Fresh-intel fold points at (PerFieldBirthSiteUnionFind.lean, KeepAliveRedundancyPrefixMin.lean) are the ALREADY-PROMOTED sources — Partition.lean’s Part A–D structure is a byte-for-byte structural match to PerFieldBirthSiteUnionFind.lean’s Part A–D (§3.9); RunningCount.lean’s keep_alive_redundancy_sound_iff_whole_pair matches KeepAliveRedundancyPrefixMin.lean’s theorem of the same name.
  2. The real remaining work is CP-2 sync verification + close-out, not authorship. Confirm the four-surface sync (Lean ↔ .proof ↔ aims-rules.md/arc.md ↔ Annex E §AIMS) is genuinely complete — the rule-file HISTORY entries date 2026-07-02 (one calendar day off from the 2026-07-03 commit date; §9 coverage gap) and were landed in the SAME /commit-push cross-repo commit pair as the Lean corpus (wrapper commit 7d4fee71c, same timestamp 06:46:33), so the sync is plausible but UNVERIFIED against /sync-aims-spec --check (§9).
  3. The commit that landed T1–T5 is a Two-Hats violation — it also shipped unrelated ori_fmt/ori_parse grammar work (multiline params, sum-type leading-pipe, where-clause placement) in the SAME --bypass commit (§3.9, §8). This makes git-archaeology on this file set unreliable for isolating AIMS-only history; treat the commit as a single opaque landing event, not a signal source.
  4. A THIRD near-duplicate same-allocation union-find now exists in the codebase — compute_genuine_same_alloc_reps (project_aliases.rs), ForwarderUnionFind (ownership_scans/union_find.rs), compute_same_alloc_reps (emit_rc/edge_cleanup.rs), and now BirthSitePartition (birth_site_partition.rs) — four independent same-allocation identity mechanisms over overlapping edge subsets, with an in-tree parity test PROVING BirthSitePartition deliberately diverges from compute_genuine_same_alloc_reps (refuses the over-approximating split-site case). This is a live LEAK:algorithmic-duplication risk the S02+ emitter work MUST resolve by consolidation, not further proliferation (§5, §3H).
  5. aims-burden-tracking/s-cba6624a (“per-field-allocation-identity-provenance-infrastructure”) is confirmed still open with pending success criteria and its own committed decision record (decisions/19-per-field-allocation-identity-union-find-lean-license.md) and intel dossier — the plan body’s “flag for absorption at S11” instinct is corroborated; do not let S02+ silently re-derive what s-cba6624a already scoped (§6).
  6. No external system proves what T2 needs — independently reconfirmed, with sharper precision than the prior fold. Perceus requires explicit control flow and states this “requirement is in tension with functions that have non-linear control flow” (§7.1). RustBelt explicitly does not model stack unwinding — the community’s own assessment calls it a still-unsolved modular-reasoning gap analogous to C++ exception safety (§7.2). Aeneas’s own maintainers state, in the imperative present, that it “does not support return inside nested loops, or break/continue to outer loops” — a stated ENGINEERING gap they plan to close, not a proof-theoretic wall like RustBelt’s (§7.3). CompCert’s Kildall dataflow framework is the strongest available ENGINEERING-SHAPE precedent (a verified, reusable worklist fixpoint solver reused across multiple analyses) even though it targets forward/backward dataflow, not RC-soundness with unwind edges (§7.4). None of the four provides a transferable soundness proof for T2’s CFG-with-back-edges-and-unwind-edges shape — the recombined synthesis in §7.5 is the design S01 should carry forward, refuted against its own kill-criterion.

DIG DEEPER

cd compiler_repo && aims-proof/scripts/check-proofs.sh aims-proof/proofs/12-provenance/*.proof
cd compiler_repo/aims-proof/lean && lake build   # full kernel re-verify (slow; incremental artifacts already present)
python -m scripts.plan_corpus.read plans/aims-provenance-ledger --criteria --section s-4ea2cc83
git -C compiler_repo show --stat 3fa52183a

(full dossier: lean-foundations—s-4ea2cc83.intel.md)