0.10.0 — records, exact rounding, and the coverage sweep

Features

String-keyed records. Record<string, T> parameters are modeled as uninterpreted String→Real maps: dynamic-key lookups get congruence — rates[currency] reads the same value everywhere in the proof, rates[a] and rates[b] stay independent unless a === b. Record lookups stop being free variables.

Exact decimal rounding. x.toDecimalPlaces(d, mode) with a literal digit count is modeled exactly: ROUND_HALF_EVEN ties go to the even neighbour, ROUND_HALF_UP ties go away from zero (both signs). Rounding-policy divergence becomes refutable: the classic "tax of the sum vs sum of per-line taxes" conservation property produces a genuine counterexample instead of being absorbed by an error bound.

Module constants: strings too. const STATUS = "paid" is now a fact in bodies and at call sites, alongside the numeric constants from 0.9.0.

Destructured returns. const { net, fee } = split(x) binds each property through the modular rewriter — the callee's object ensures attach to the bindings, renames included.

Single-file verify sees its imports. Runs of ≤12 files expand the contract registry one hop through imports (relative + tsconfig aliases): verifying one file no longer misses the requires/ensures of callees defined elsewhere.

seqEq(xs, old(xs)) over heap arrays: in-place .sort() refutes it, sorting a copy proves it (from 0.9.2, now documented).

Fixes

• Early-exit guards over variables reassigned between the guard and the call are discarded — the stale guard no longer vouches for the new value.
• Class methods with inline requires/ensures and no @invariant now extract and verify (previously a silent zero-task skip).
• Windows: module-const import resolution keys on path.isAbsolute.

Docs

README now covers the whole 0.9.x–0.10 surface: module constants, destructured params/returns, call-site guards, Zod dedup transforms, string fields and referential-integrity guards, string-keyed records, exact rounding and money conservation, modifies() frames.

🤖 Generated with Claude Code