Skip to content

0.9.0 — constants, destructured params, typed field views

Choose a tag to compare

View all tags
@tiagoschmitt tiagoschmitt released this 18 Aug 03:50
· 14 commits to main since this release
v0.9.0
ec5e370

Highlights

Module constants resolve themselves. const ZERO = new Decimal(0) — same file or imported (relative paths and tsconfig paths aliases) — becomes an assumed fact in every function that references it. Trusted initializers: numeric literals, new Decimal(lit), and folded arithmetic (24 * MS_PER_HOUR). No more assume(ZERO.equals(0)) hand-holding; let bindings stay free.

Destructured object parameters. function f({ lineItem, rules }: Input) now verifies like f(lineItem, rules): bindings become typed params (sorts from same-file interfaces/type literals, renames and binding defaults honored), and call sites map object-literal arguments per property, plain idents as member accesses, and missing props to their defaults. Parameter defaults also apply at call sites for positional params (setPrecision(x) checks precision := 2).

Typed field views — string and bool contexts. Element fields inside quantifiers get Int→String (__sfield_) and Int→Bool (__bfield_) views of the heap: m.appliesTo === "baseCost" translates, !m.isEnabled || guards work, and field-vs-field string equality (d.key === m.appliesTo) follows once either field is string-typed by a literal comparison. Call-site array-literal facts extended to match: string prop equalities, truthiness facts for all literal props, and pairwise string-prop (in)equalities — uniqueBy(arr, m => m.key) now proves for literal arrays with distinct string keys. Referential-integrity guards of the form forall m: !m.isEnabled || m.appliesTo === "baseCost" || exists d: d.key === m.appliesTo && d.isEnabled are now provable and refutable at call sites.

Zod dedup transforms. .transform(a => [...new Map(a.map(x => [x.key, x])).values()]) grants uniqueBy on the parsed value; .transform(a => [...new Set(a)]) grants unique. Stronger than the Set-size refine — the parse guarantees uniqueness instead of rejecting duplicates.

Nullable-object truthiness. value ? value : ZERO where value's declared type is a nullable object/array union desugars to value !== null (objects are always truthy) — the ubiquitous valueOrDefault pattern proves end-to-end.

Fixes

  • Schema-injected assume contracts were silently dropped in functions with positional check/assume steps (the bodySteps skip snapshotted assumptions before schema facts landed). Schema facts now lead the body steps.
  • Arity guards on contract resolution count source parameter positions, not expanded destructured bindings.
  • __sfield_/__bfield_ internals filtered from counterexample display.

🤖 Generated with Claude Code

Assets 2
Loading