From a11cb7cc9f912a0d7ee8a56b3f53255bd101e327 Mon Sep 17 00:00:00 2001 From: Brummel Date: Mon, 18 May 2026 23:39:31 +0200 Subject: [PATCH] =?UTF-8?q?test(check):=20RED=20=E2=80=94=20over-strict-mo?= =?UTF-8?q?de=20false-positive=20on=20ctor-rebuild=20consume?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit RED-first audit trail (debug skill; fix follows as a separate GREEN commit). Test-only, +97 lines in the linearity in-source test module, no production change. Bug: the [over-strict-mode] lint emits a conservative false-positive. The consume-detection (any_sub_binder_consumed_for / pattern_has_consumed_heap_binder, crates/ailang-check/src/linearity.rs :853,942) only recognises a consume of an (own (con T)) param when a heap-typed pattern-binder is moved out of `match p`. When p is destructured into purely primitive fields (e.g. Float/Int) that are fed into a Term::Ctor rebuilding p's own ctor, that rebuild's re-consumption of the dismantled allocation is invisible, so the lint wrongly tells the author `(borrow ...)` would suffice. It is over-strict, never under-strict (exit 0; codegen/ABI unaffected) — but an LLM author "fixing" the spurious warning by flipping an export's declared mode own->borrow would silently invert the ABI ownership contract, which is why a low-severity advisory FP gets a real RED-first fix. The carrier's initial hypothesis (nested inner `match` is the discriminator) was disproved during diagnosis: the M3 embed_backtest_step_record.ail is silent only because its implicit-mode scalar Float param disables the lint via the activation gate (linearity.rs:327), not because it handles the rebuild; the defect reproduces with a single param and no nesting. The RED unit is therefore the general synthetic shape — an (own (con T)) param consumed by a term-ctor rebuild of its own ctor — not the embed fixtures. RED test (fails now, goes GREEN when consume-detection sees the ctor-rebuild re-consumption): crates/ailang-check/src/linearity.rs :: linearity::tests::over_strict_mode_silent_when_ctor_rebuilt_from_primitive_fields --- crates/ailang-check/src/linearity.rs | 97 ++++++++++++++++++++++++++++ 1 file changed, 97 insertions(+) diff --git a/crates/ailang-check/src/linearity.rs b/crates/ailang-check/src/linearity.rs index 1848ca3..70477a8 100644 --- a/crates/ailang-check/src/linearity.rs +++ b/crates/ailang-check/src/linearity.rs @@ -1464,6 +1464,103 @@ mod tests { ); } + /// RED (over-strict-mode FP on ctor-rebuild): a `State(Float, + /// Int)` ADT def. Both fields are primitive — the lint's + /// `pattern_has_consumed_heap_binder` filters them out — yet a + /// body that destructures `State` and rebuilds it still consumes + /// the scrutinee's allocation. + fn state_typedef() -> Def { + Def::Type(ailang_core::ast::TypeDef { + name: "State".into(), + vars: vec![], + ctors: vec![Ctor { + name: "State".into(), + fields: vec![Type::float(), Type::int()], + }], + doc: None, + drop_iterative: false, + }) + } + + /// RED helper: a fn whose single param is `(own State)` and whose + /// body is `body`. Mirrors `fn_own_intlist` but over `State` so + /// the ctor-field-type lookup resolves to `(Float, Int)`. + fn fn_own_state(name: &str, body: Term) -> Def { + Def::Fn(FnDef { + name: name.into(), + ty: Type::Fn { + params: vec![Type::Con { name: "State".into(), args: vec![] }], + param_modes: vec![ParamMode::Own], + ret: Box::new(Type::Con { name: "State".into(), args: vec![] }), + ret_mode: ParamMode::Implicit, + effects: vec![], + }, + params: vec!["st".into()], + body, + suppress: vec![], + doc: None, + export: None, + }) + } + + /// RED, negative property: a fn with `(own State)` whose body is + /// `match st { State(acc, n) => State(acc, n) }` — it + /// destructures the owned scrutinee and **rebuilds the same + /// ctor** from the extracted fields. The old `State` allocation + /// is dismantled by the rebuild, so `(own State)` is genuinely + /// required; `(borrow State)` would NOT suffice. The lint must + /// therefore stay silent. + /// + /// This is the minimal isolating shape behind the + /// `embed_backtest_step_tick` over-strict-mode false positive: + /// `any_sub_binder_consumed_for` only recognises a consume when a + /// *heap-typed* pattern-binder is moved out. When every + /// destructured field is primitive (`acc: Float`, `n: Int`) but + /// they feed a `term-ctor` rebuilding the scrutinee's own ctor, + /// the rebuild's re-consumption of the payload is invisible to + /// the check and the lint spuriously fires. No nested `match` and + /// no second param are needed to trigger it — the defect is the + /// unrecognised ctor-rebuild consume, not match nesting. + #[test] + fn over_strict_mode_silent_when_ctor_rebuilt_from_primitive_fields() { + // Body: (match st + // ((pat-ctor State (pat-var acc) (pat-var n)) + // (term-ctor State (var acc) (var n)))) + let body = Term::Match { + scrutinee: Box::new(Term::Var { name: "st".into() }), + arms: vec![Arm { + pat: Pattern::Ctor { + ctor: "State".into(), + fields: vec![ + Pattern::Var { name: "acc".into() }, + Pattern::Var { name: "n".into() }, + ], + }, + body: Term::Ctor { + type_name: "State".into(), + ctor: "State".into(), + args: vec![ + Term::Var { name: "acc".into() }, + Term::Var { name: "n".into() }, + ], + }, + }], + }; + let m = Module { + schema: ailang_core::SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![state_typedef(), fn_own_state("f", body)], + }; + let diags = check_module(&m); + assert!( + !diags.iter().any(|d| d.code == "over-strict-mode"), + "no over-strict-mode expected: the `term-ctor State` rebuild \ + re-consumes the destructured payload of the `(own State)` \ + scrutinee, so `(own)` is genuinely required; got {diags:?}" + ); + } + /// Iter 19a.1, positive: a fn with `(own IntList)` whose body /// is `match xs { Nil => 0, Cons(h, t) => h }` returns the /// **primitive-typed** `h` (`Int`) and never moves the