AILang/docs/plans/0125-harden-ownership-part2-class4.md

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:

        (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):

        (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:

(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:

(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:

/// #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):

/// #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:

    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof", "c2_let_alias"] {

to:

    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).