v0.8.0 — The Quantifier Release

v0.8.0 — Quantifiers, folds, and proofs that write themselves

The quantifier release. Theorem's no-quantifier discipline gains one measured exception — Int-indexed array quantification, the fragment where e-matching is well-behaved — and an entire vocabulary grows on top of it: element facts, distinctness, order, membership, sums, counts. Loops start proving themselves (Houdini + Spacer), schemas speak the new vocabulary, and the editor turns failures into one-click fixes.

Quantified array contracts (F8)

forall(arr, (x, i) => P), exists, sorted(arr), unique(arr) desugar to real Z3 quantifiers over Int indices bounded by [0, arr.length). Recursive spec predicates and the heap stay ground — a 10-run variance gate guards the quarantine. The flagship lower-bound binary search proves all obligations (quantified invariants, termination, quantified ensures) in 0.3s; the textbook lo = mid bug is refuted on termination (examples/binary-search.ts).

Heap mode learned integer state: mutable numerics classify Int-sorted via a syntactic fixpoint, so Math.floor((lo + hi) / 2) compiles to Z3 integer division — never touching the to_int mixing on which the WASM solver diverges.

Arrays of objects

Account[] is an array of references (Array(Int → Int)) composing with the field heaps: users[i].balance is Select(heap_balance, Select(users, i)). In-array aliasing — two slots holding the same object — is a case the solver explores: per-slot ensures refute without slot distinctness and prove with it; a quantified field invariant survives an element-write loop with no distinctness hypothesis (examples/object-arrays.ts).

Collection vocabulary and folds

requires(unique(users))                         // pairwise-distinct OBJECTS — anti-aliasing in one word
requires(uniqueBy(users, (u) => u.id))          // pairwise-distinct field values
requires(sortedBy(users, (u) => u.balance))     // ordered by a field
ensures(sumBy(users, (u) => u.balance) === old(sumBy(users, (u) => u.balance)))

sumBy/countBy are heap-versioned symbols with delta axioms: every indexed write moves the fold by exactly its cell delta — valid only under unique(arr) (a duplicated reference would count twice; without uniqueness the fold is honestly unconstrained). transfer conserves the total even when i === j; the phantom fee is refuted; sum invariants chain through loop bodies (examples/collections.ts).

Invariants that write themselves

• Houdini (default on) — requires/ensures conjuncts become guess-and-check loop-invariant candidates; entry + preservation proved, failures dropped, fixpoint iterated; survivors appear marked (auto). Sound by construction: a debiting loop loses its candidate and refutes honestly.
• Spacer/CHC inference — loops encode as Horn clauses; Z3's Spacer synthesizes inductive invariants (linear combinations like paid + 3 * remaining === 3 * total). Surfaced in theorem suggest and as an editor quick-fix (💡) that inserts the inferred invariant(() => ...) lines in one click.
• Loop contracts may sit in the Dafny-style header position directly before the while.

Schemas speak the vocabulary

const OrderSchema = z.object({
  scores: z.array(z.number().min(1)),                                    // → forall
  users:  z.array(z.object({ balance: z.number().nonnegative() })),      // → forall over fields
  ids:    z.array(z.number()).refine(a => new Set(a).size === a.length), // → unique(ids)
})

Element constraints and the canonical Set-size refine become quantified facts after the parse — and the schema-derived unique opens the sumBy delta gate. Effect Schema has full parity (examples/schema-arrays.ts).

More theories put to work

• Regex: /re/.test(s) and z.string().regex() become Z3 regex membership integrated with string lengths — /^\d{5}$/ pins .length === 5. Unicode-correct negated classes; unsupported constructs are dropped, never approximated. .email()/.uuid() translate; the i flag is supported (examples/regex.ts).
• Bitwise (| & ^ << >> >>>): Int-classified state maps through BV32 with exact JS ToInt32 semantics.
• Discriminated unions: the discriminant ranges over its declared literals — exhaustiveness is provable, and a forgotten variant comes back as a counterexample naming it (p.kind = card) (examples/discriminated-unions.ts).
• Array.prototype.sort as a trusted contract: sort((a, b) => a - b) havocs the array and grants sortedness; bare .sort() grants nothing — the lexicographic footgun is caught.

A proof-backed editor

• Labeled multi-line diagnostics (Contract violated: / Unmet requires: / Call: / Counterexample:); counterexamples name aliasing (users[1] = same object as users[0]), show per-element fields (users[1].balance = -100), and narrate the execution path (path: line 33: p.kind === "boleto" → not taken).
• tsc errors suppressed by proof: for each arr[i], Theorem proves 0 <= i < arr.length from your requires; proved accesses get tsc's possibly-undefined (2532/18048) filtered at exactly that spot. The unverified ! gives way to a theorem — and the error returns by itself if a requires weakens.
• --gen-tests reconstructs heap counterexamples as executable object graphs, aliasing included (const to = from // same reference).

Soundness fixes worth naming

• Class methods and proof.fn bodies with while loops route through the honest havoc machinery — the legacy loop path (which could prove vacuously under old()) is retired for every extractable shape.
• Call-site arguments are typed by the callee's parameter sorts; quantified field requires are checked against array-literal facts (fresh object literals are distinct allocations; [a, a] is the same object).
• Metadata-preserving substitution (loc/sort survive rebuilds), schema assumes prepended before ensures snapshots, and a dozen silent-drop traps converted into either working translations or honest refutations.

467 tests across the workspace. Full details in the README, rewritten for the new feature set.