From dea93a99fcd49941426144a6a71eb03511c5e774 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 1 Jun 2026 18:18:40 +0200 Subject: [PATCH] =?UTF-8?q?plan:=200064=20iter=204=20(final)=20=E2=80=94?= =?UTF-8?q?=20partition=5Feithers=20double-consume=20rewrite=20(class=204)?= =?UTF-8?q?=20(#57)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Final iteration of spec 0064. Closes class 4, the one genuine corpus bug (not a false positive): partition_eithers projects both (app Pair.fst rest) and (app Pair.snd rest) from one owned rest; fst/snd are own-param projections that move a field out, so rest is consumed twice. Universal linearity activation (#55) would reject it. Fix is a body rewrite (destructure rest once via match), not a check change. Latent-bug nature: partition_eithers has a bare (Implicit) param slot today, so the check is skipped on it -- no RED->GREEN flip on the real fixture. The rewrite's correctness is proven by the unchanged 2 3 2 3 E2E output (std_either_list_demo) and by the explicit-mode c4_double_consume must-stay-RED fixture (the double-projection shape IS rejected, verifiable today). Orchestrator verified the rewrite this session: ail check std_either_list -> exit 0; ail run the demo -> 2 3 2 3 (applied, ran, reverted for the implementer to re-apply). Two tasks: Task 1 rewrites partition_eithers + gates on the unchanged E2E output; Task 2 adds c4_double_consume (must-stay-RED, folded into a generalised harden_ownership_heap_double_consume_still_errors loop) and c4_rewrite (stays-clean, added to the false-positives-clean array). plan-recon confirmed no hash-pin on std_either_list (only the e2e 2 3 2 3 output pin, preserved). No check/schema/codegen change. This is the last of the four #57 hardening classes; after it lands, spec 0064 is code-complete and the cycle is ready for audit. refs #57 --- .../0125-harden-ownership-part2-class4.md | 247 ++++++++++++++++++ 1 file changed, 247 insertions(+) create mode 100644 docs/plans/0125-harden-ownership-part2-class4.md diff --git a/docs/plans/0125-harden-ownership-part2-class4.md b/docs/plans/0125-harden-ownership-part2-class4.md new file mode 100644 index 0000000..80451a5 --- /dev/null +++ b/docs/plans/0125-harden-ownership-part2-class4.md @@ -0,0 +1,247 @@ +# Harden ownership part 2 — iteration 4 (final): partition_eithers double-consume rewrite (class 4) — Implementation Plan + +> **Parent spec:** `docs/specs/0064-harden-ownership-analysis-part-2.md` +> +> **For agentic workers:** REQUIRED SUB-SKILL: use the `implement` +> skill to run this plan. Steps use `- [ ]` checkboxes for tracking. + +**Goal:** Rewrite `std_either_list.partition_eithers` to destructure +its recursive result once, removing the genuine double-consume that +universal linearity activation would reject — and pin the rejected +shape so the check's correctness is documented. + +**Architecture:** `partition_eithers` projects both `(app Pair.fst +rest)` and `(app Pair.snd rest)` from one owned `rest`; `fst`/`snd` are +`own`-param projections that move a field out, so each consumes `rest` +→ a genuine double-consume. This is a real corpus bug, NOT a +false positive: the fix is a body rewrite (destructure `rest` once via +`(match rest (case (pat-ctor MkPair ls rs) …))`), not a check change. +The check is correct and unchanged. Two standalone fixtures pin the two +shapes: `c4_double_consume` (the rejected double-projection, must stay +RED) and `c4_rewrite` (the accepted destructure-once shape). + +**Tech Stack:** `examples/std_either_list.ail` (the corpus fix), +`examples/` fixtures, `crates/ailang-check/tests/workspace.rs` +assertions, gated by the existing `std_either_list_demo` E2E +(`crates/ail/tests/e2e.rs`). + +**Scope:** FOURTH and final iteration of spec 0064 — class 4 only. +Classes 1/2/3 shipped in iters 1-3. No check change, no schema/type +change, no codegen change. + +**Latent-bug note.** `partition_eithers`'s param is a bare (Implicit) +slot today, so the linearity check is *skipped* on it — the +double-consume is not observable as RED on the real fixture until #55 +activates the check universally. There is therefore no RED→GREEN flip +on `std_either_list.ail`; the rewrite is a pre-emptive corpus fix whose +correctness is proven by (a) the unchanged `2 3 2 3` E2E output and (b) +the `c4_double_consume` must-stay-RED fixture, which demonstrates — with +explicit modes, so the check is active today — that the +double-projection shape IS rejected. The orchestrator verified the +rewrite this session: `ail check examples/std_either_list.ail` → exit 0, +`ail run examples/std_either_list_demo.ail` → `2 3 2 3`. + +--- + +**Files this plan creates or modifies:** + +- Modify: `examples/std_either_list.ail:61-71` — `partition_eithers` + Cons arm rewritten to destructure `rest` once. +- Create: `examples/c4_double_consume.ail` — must-stay-RED fixture (the + rejected double-projection). +- Create: `examples/c4_rewrite.ail` — stays-clean fixture (the accepted + destructure-once shape). +- Test: `crates/ailang-check/tests/workspace.rs:745-753` — generalise + `harden_ownership_heap_double_consume_still_errors` to also assert + `c4_double_consume` fires. +- Test: `crates/ailang-check/tests/workspace.rs:728` — add `c4_rewrite` + to `harden_ownership_false_positives_are_clean`. + +--- + +### Task 1: Rewrite partition_eithers and confirm behaviour unchanged + +**Files:** +- Modify: `examples/std_either_list.ail:61-71` + +- [ ] **Step 1: Rewrite the Cons arm** + +In `examples/std_either_list.ail`, the `partition_eithers` Cons arm +(`:61-71`) is currently: + +```text + (case (pat-ctor Cons h t) + (let rest (app partition_eithers t) + (match h + (case (pat-ctor Left l) + (term-ctor Pair MkPair + (term-ctor List Cons l (app Pair.fst rest)) + (app Pair.snd rest))) + (case (pat-ctor Right r) + (term-ctor Pair MkPair + (app Pair.fst rest) + (term-ctor List Cons r (app Pair.snd rest))))))))))) +``` + +Replace it with (destructure `rest` once; `ls` = lefts, `rs` = rights; +each consumed once per independent match-arm): + +```text + (case (pat-ctor Cons h t) + (let rest (app partition_eithers t) + (match rest + (case (pat-ctor MkPair ls rs) + (match h + (case (pat-ctor Left l) + (term-ctor Pair MkPair + (term-ctor List Cons l ls) + rs)) + (case (pat-ctor Right r) + (term-ctor Pair MkPair + ls + (term-ctor List Cons r rs)))))))))))) +``` + +(`MkPair` is the `Pair` ctor from the imported `std_pair`, +`examples/std_pair.ail:12`. The Nil arm `:57-60` is unchanged.) + +- [ ] **Step 2: Confirm the module checks clean** + +Run: `target/debug/ail check examples/std_either_list.ail` +Expected: `ok (65 symbols across 7 modules)`, exit 0. (Build the CLI +first if stale: `cargo build --bin ail`.) + +- [ ] **Step 3: Confirm the E2E demo output is unchanged** + +Run: `cargo test -p ail --test e2e std_either_list_demo` +Expected: PASS — `std_either_list_demo` still asserts stdout +`["2", "3", "2", "3"]`. The rewrite is semantically identical (same +lefts/rights partition), so the output is preserved. + +--- + +### Task 2: Pin the rejected and accepted shapes + +**Files:** +- Create: `examples/c4_double_consume.ail` +- Create: `examples/c4_rewrite.ail` +- Test: `crates/ailang-check/tests/workspace.rs:745-753`, `:728` + +- [ ] **Step 1: Create the must-stay-RED fixture** + +Create `examples/c4_double_consume.ail` with exactly: + +```ail +(module c4_double_consume + (data Pair + (doc "boxed pair of ints") + (ctor MkPair (con Int) (con Int))) + (fn fst (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p) + (body (match p (case (pat-ctor MkPair a b) a)))) + (fn snd (type (fn-type (params (own (con Pair))) (ret (own (con Int))))) (params p) + (body (match p (case (pat-ctor MkPair a b) b)))) + (fn both + (doc "MUST STAY RED: rest projected by fst AND snd = consumed twice") + (type (fn-type (params (own (con Pair))) (ret (own (con Pair))))) + (params rest) + (body (term-ctor Pair MkPair (app fst rest) (app snd rest))))) +``` + +- [ ] **Step 2: Create the stays-clean fixture** + +Create `examples/c4_rewrite.ail` with exactly: + +```ail +(module c4_rewrite + (data Pair + (doc "boxed pair of ints") + (ctor MkPair (con Int) (con Int))) + (fn both + (doc "rewrite: destructure rest once via match") + (type (fn-type (params (own (con Pair))) (ret (own (con Pair))))) + (params rest) + (body (match rest (case (pat-ctor MkPair a b) (term-ctor Pair MkPair a b)))))) +``` + +- [ ] **Step 3: Generalise the heap-double-consume assertion to cover c4_double_consume** + +In `crates/ailang-check/tests/workspace.rs`, the test +`harden_ownership_heap_double_consume_still_errors` (`:744-753`) is +currently single-fixture. Replace its doc comment and body: + +```rust +/// #56 type-gating: the exemption is value-type-only. A heap param +/// consumed twice (`real_consume.dup`, `(term-ctor Pair Pair b b)`) MUST +/// still fire use-after-consume — proving the fix did not blanket-silence +/// genuine multi-consume. +#[test] +fn harden_ownership_heap_double_consume_still_errors() { + let entry = examples_dir().join("real_consume.ail"); + let ws = load_workspace(&entry).expect("load real_consume"); + let diags = check_workspace(&ws); + assert!( + diags.iter().any(|d| d.code == "use-after-consume"), + "real_consume.dup must still fire use-after-consume; got: {diags:#?}" + ); +} +``` + +with (loop over both genuine double-consume fixtures): + +```rust +/// #56 type-gating + #57 class 4: a heap value consumed twice MUST still +/// fire use-after-consume — `real_consume.dup` (`(term-ctor Pair Pair b +/// b)`) and `c4_double_consume.both` (`rest` projected by both `fst` and +/// `snd`, the genuine double-consume the partition_eithers rewrite +/// removes). Proves the hardening did not blanket-silence genuine +/// multi-consume. +#[test] +fn harden_ownership_heap_double_consume_still_errors() { + for name in ["real_consume", "c4_double_consume"] { + let entry = examples_dir().join(format!("{name}.ail")); + let ws = load_workspace(&entry).unwrap_or_else(|e| panic!("load {name}: {e:?}")); + let diags = check_workspace(&ws); + assert!( + diags.iter().any(|d| d.code == "use-after-consume"), + "{name} must still fire use-after-consume; got: {diags:#?}" + ); + } +} +``` + +- [ ] **Step 4: Add c4_rewrite to the clean array** + +In `crates/ailang-check/tests/workspace.rs`, the +`harden_ownership_false_positives_are_clean` array (`:728`). Change: + +```rust + for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof", "c2_let_alias"] { +``` + +to: + +```rust + for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof", "c2_let_alias", "c4_rewrite"] { +``` + +- [ ] **Step 5: Run both harden assertions** + +Run: `cargo test -p ailang-check --test workspace harden_ownership` +Expected: PASS — both `harden_ownership_heap_double_consume_still_errors` +(now asserting `real_consume` AND `c4_double_consume` fire +use-after-consume) and `harden_ownership_false_positives_are_clean` (now +including `c4_rewrite`) green. + +- [ ] **Step 6: Full crate + workspace regression** + +Run: `cargo test -p ailang-check` +Expected: PASS — whole `ailang-check` suite green. + +Run: `cargo test --workspace` +Expected: PASS — including `std_either_list_demo` (output `2 3 2 3` +unchanged). Per the typed-MIR re-synth strictness memory, run the whole +workspace, not just e2e. + +Run: `python3 bench/check.py` then `python3 bench/compile_check.py` +Expected: both green — no check or compile-baseline change (a corpus +body rewrite + standalone fixtures only).