test(check): RED — over-strict-mode false-positive on ctor-rebuild consume
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
This commit is contained in:
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user