From 2769e50a359bf51629257c8f2726a18589a32db5 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 1 Jun 2026 18:22:59 +0200 Subject: [PATCH] fix(examples): destructure partition_eithers result once (#57, 0064 iter 4) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 | 28 +++++++++++++++----------- examples/c4_double_consume.ail | 13 ++++++++++++ examples/c4_rewrite.ail | 9 +++++++++ examples/std_either_list.ail | 22 +++++++++++--------- 4 files changed, 50 insertions(+), 22 deletions(-) create mode 100644 examples/c4_double_consume.ail create mode 100644 examples/c4_rewrite.ail diff --git a/crates/ailang-check/tests/workspace.rs b/crates/ailang-check/tests/workspace.rs index 0b46754..e3d86eb 100644 --- a/crates/ailang-check/tests/workspace.rs +++ b/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 -/// 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. +/// #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() { - 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:#?}" - ); + 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:#?}" + ); + } } /// RED for fieldtest finding B1 (docs/specs/0058): reading a diff --git a/examples/c4_double_consume.ail b/examples/c4_double_consume.ail new file mode 100644 index 0000000..638bc41 --- /dev/null +++ b/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))))) diff --git a/examples/c4_rewrite.ail b/examples/c4_rewrite.ail new file mode 100644 index 0000000..2dc0d81 --- /dev/null +++ b/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)))))) diff --git a/examples/std_either_list.ail b/examples/std_either_list.ail index df4deeb..b883584 100644 --- a/examples/std_either_list.ail +++ 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>: 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>: 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 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))))))))))) + (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))))))))))))