Repository navigation
[TS] Constrain Array.includes to element membership #435
Description
Resolution (2026-10-14)
Audited against usvm main at 19866c959d.
The bounded Array.includes source model checks SameValueZero membership and fromIndex, including NaN, instead of returning an unconstrained Boolean. Implementation: usvm #443, usvm #450.
Validation: All 41 TsSequenceEtsIrModelTest regressions passed, including membership, NaN and offset cases.
Original report and acceptance context, retained for traceability
Problem
The Array.includes approximation returns a completely unconstrained Boolean.
Minimal TypeScript example
export function includes(): boolean {
return [1, 2].includes(3);
}Expected behavior
includes() is always false. Check elements using JavaScript SameValueZero semantics in the supported array domain, including NaN and the optional start index.
Current source evidence
Checked against USVM main 53dce8f3bca2713642c783ba8308a6a360a9e516. This exact snippet is a proposed regression from source audit; it has not yet been run as a new end-to-end test. #368 audits the existing call approximations but does not implement these individual fixes.
Acceptance criteria
- A focused test checks the symbolic outcome without reporting an approximation as exact semantics.
- The supported case agrees with concrete TypeScript/Node.js replay.
- Unsupported operand or environment cases remain explicit.
Activity