0.11.0 — the deep-verification wave

Shaped by a forensic pass over a 2,000-file production codebase: every verification failure was classified (real / contract-wrong / tool-gap), every tool gap got a minimal repro, and the critical ones ship fixed here.

Critical fixes

Per-file contract registry. Contracts no longer attach by bare function name across files. A local definition shadows foreign same-named contracts, imported names must resolve to the contract's defining file, and declare() packages stay global. Before this, a zero-annotation file could inherit another file's contract for a same-named function — phantom failures and unsound assumed ensures.

Sound call-site scope facts. A fact recorded from a declaration initializer is dropped when the variable is reassigned in a nested branch or loop before the call — let p = ZERO; if (c) { p = f(x) } use(p) no longer "proves" obligations against ZERO. This was masking a real violation.

Runtime-safe contracts, documented. Expression-form predicates evaluate their arguments at runtime; dereferencing nullable data can throw in production. The arrow form — ensures(() => ...) — is read statically and never executed. It was already parsed; now it's the documented recommendation. (Also ships the 0.10.1 runtime hardening: absorbing output() proxy, true no-op quantifiers.)

New body shapes

• try/catch models as a branch under an unknowable condition — both completions stay reachable.
• arr.filter(f).length is bounded by [0, arr.length]; arr.map(f).length is exactly arr.length.
• xs.find(f) binds a symbolic element: quantified element facts instantiate on the found value, === undefined guards resolve to the miss case.
• Bare-ident ternary guards become named free Booleans — repeated occurrences unify.
• Int-sorted .length variables finally get their >= 0 fact (a silently-swallowed day-one gap).
• Module-constant facts reach check/assume-only functions; fold bounds accept vocabulary predicates (nonNegative(it.f)).

Diagnostics

The CLI now warns when a function has contracts but zero obligations could be translated — silent drops announce themselves.

Companion release

@theoremts/contracts-decimal 0.2.1: abs/absoluteValue are exact (output === a || output === -a); toDecimalPlaces/toDP bounded declares removed so core's exact rounding model applies.

🤖 Generated with Claude Code