0.9.2 — body equations and array immutability

Fixes

Body equations survive method calls and modular calls in returned object literals. Two silent drops killed in one class of false positive:

• Pure method contracts now inline into the function body's SSA bindings, not just predicates and call sites — const d = a.sub(b); const e = d; keeps both bindings.
• Object-literal return props route through the modular rewriter instead of raw translation: registered calls become memoized __ret vars, so two props built from identical call trees stay equal even when the call's arguments are untranslatable (optional chains included).

Before, a tautological ensures like output().second.equals(output().first) over const second = first; return { first, second } refuted with disconnected free variables. Now it proves.

Features

seqEq(xs, old(xs)) — array immutability as a contract. Over versioned heap arrays, the ensures translates as extensional equality between the current and initial array versions: an in-place .sort() (modeled as havoc) refutes it, sorting a copy proves it. Catches functions that silently mutate arrays they receive.

Docs

• README: modifies() frame conditions get a worked example (undeclared write = violation, declared frame = clean) and the seqEq immutability pattern.

🤖 Generated with Claude Code