plan: 0064 iter 4 (final) — partition_eithers double-consume rewrite (class 4) (#57)

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
2026-06-01 18:18:40 +02:00
parent be259f9d46
commit dea93a99fc
1 changed files with 247 additions and 0 deletions
@@ -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).