fix(examples): destructure partition_eithers result once (#57, 0064 iter 4)

Final iteration of spec 0064 (the #55-cutover hardening, #57). Closes
class 4, the one genuine corpus bug among the four (not a false
positive): std_either_list.partition_eithers projected both
(app Pair.fst rest) and (app Pair.snd rest) from one owned `rest`.
Pair.fst/snd are own-param projections that move a field out, so each
consumes `rest` -> a genuine double-consume that universal linearity
activation (#55) would correctly reject. The fix is a body rewrite
(destructure `rest` once via (match rest (case (pat-ctor MkPair ls rs)
…)) then dispatch on the head), NOT a check change -- the check is
right.

Latent until activation: partition_eithers' param is a bare (Implicit)
slot today, so the check is skipped on it -- no RED->GREEN flip on the
real fixture. The rewrite is a pre-emptive corpus fix. Its correctness
rests on the unchanged 2 3 2 3 E2E output (std_either_list_demo, a
semantically-identical partition) and on the new c4_double_consume
must-stay-RED fixture, which -- with explicit modes, so the check is
active today -- demonstrates the double-projection shape IS rejected.

- examples/std_either_list.ail: partition_eithers Cons arm rewritten;
  doc updated (destructure-once, no longer "projections").
- examples/c4_double_consume.ail: must-stay-RED pin (the rejected
  shape), folded into a generalised
  harden_ownership_heap_double_consume_still_errors loop over
  {real_consume, c4_double_consume}.
- examples/c4_rewrite.ail: stays-clean pin (the accepted
  destructure-once shape), added to
  harden_ownership_false_positives_are_clean.

No hash-pin on std_either_list (verified); the e2e 2 3 2 3 output pin
is the content pin and is preserved. No check/schema/codegen change.
Verified: std_either_list checks clean; demo 2 3 2 3; both harden
assertions green; cargo test --workspace green; bench/check.py 34/34,
compile_check.py 24/24 stable.

This is the last of the four #57 hardening classes. Spec 0064 is now
code-complete: classes 1 (local fn-param modes), 2 (let-alias redirect),
3 (value-typed let-binder), and 4 (this) all shipped. The cycle is ready
for audit; the #55 cutover precondition is met.

refs #57

crates/ailang-check/tests/workspace.rs

@@ -725,7 +725,7 @@ fn borrow_own_demo_is_linearity_clean() {
 /// is active today) and were RED before the hardening (docs/specs/0063).
 #[test]
 fn harden_ownership_false_positives_are_clean() {
-    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof", "c2_let_alias"] {
+    for name in ["fp_value", "fp_hof", "fp_map", "c3_value_let", "c1_local_hof", "c2_let_alias", "c4_rewrite"] {
         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);
@@ -737,19 +737,23 @@ fn harden_ownership_false_positives_are_clean() {
     }
 }
 
-/// #56 type-gating: the exemption is value-type-only. A heap param
+/// #56 type-gating + #57 class 4: a heap value consumed twice MUST still
-/// consumed twice (`real_consume.dup`, `(term-ctor Pair Pair b b)`) MUST
+/// fire use-after-consume — `real_consume.dup` (`(term-ctor Pair Pair b
-/// still fire use-after-consume — proving the fix did not blanket-silence
+/// b)`) and `c4_double_consume.both` (`rest` projected by both `fst` and
-/// genuine multi-consume.
+/// `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() {
-    let entry = examples_dir().join("real_consume.ail");
+    for name in ["real_consume", "c4_double_consume"] {
-    let ws = load_workspace(&entry).expect("load real_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"),
-        "real_consume.dup must still fire use-after-consume; got: {diags:#?}"
+            "{name} must still fire use-after-consume; got: {diags:#?}"
         );
+    }
 }
 
 /// RED for fieldtest finding B1 (docs/specs/0058): reading a

examples/c4_double_consume.ail

@@ -0,0 +1,13 @@
+(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)))))

examples/c4_rewrite.ail

@@ -0,0 +1,9 @@
+(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))))))

examples/std_either_list.ail

@@ -45,7 +45,7 @@
         (case _ (term-ctor List Nil)))))
 
   (fn partition_eithers
-    (doc "Partition a list of Eithers into a Pair<List<e>, List<a>>: lefts on the left, rights on the right. Single pass via direct recursion; head dispatch is a flat match on the recursive result's projections.")
+    (doc "Partition a list of Eithers into a Pair<List<e>, List<a>>: lefts on the left, rights on the right. Single pass via direct recursion; the recursive result is destructured once and the head dispatches into the matching side.")
     (type
       (forall (vars e a)
         (fn-type
@@ -60,12 +60,14 @@
             (term-ctor List Nil)))
         (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 (app Pair.fst rest))
+                      (term-ctor List Cons l ls)
-                  (app Pair.snd rest)))
+                      rs))
                   (case (pat-ctor Right r)
                     (term-ctor Pair MkPair
-                  (app Pair.fst rest)
+                      ls
-                  (term-ctor List Cons r (app Pair.snd rest)))))))))))
+                      (term-ctor List Cons r rs))))))))))))