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
|
/// Iter 19a.1, positive: a fn with `(own IntList)` whose body
|
||||||
/// is `match xs { Nil => 0, Cons(h, t) => h }` returns the
|
/// is `match xs { Nil => 0, Cons(h, t) => h }` returns the
|
||||||
/// **primitive-typed** `h` (`Int`) and never moves the
|
/// **primitive-typed** `h` (`Int`) and never moves the
|
||||||
|
|||||||
Reference in New Issue
Block a user