v0.1.9

Added

• scripts/check_doc_counts.py pins FAQ.md's headline test count. The "by the numbers" line in FAQ.md carried a total-test figure no gate checked — only the conformance half of the sentence was pinned — and it drifted silently through two releases before being caught by hand both times. The oracle now reads the number the same way it reads README.md's status row, so the next drift fails pre-commit and CI instead of shipping.

Fixed

• vera run no longer executes a different function when the entry was dropped (#1183). When the [E620] skip propagation dropped main — or an explicit --fn target — and any public sibling survived, execute() fell through to result.exports[0]: the sibling's body ran, its result printed, exit 0, nothing on stderr. A regression of the #1178 review class, and the one outcome the loud-skip design exists to prevent, since the user could not tell the answer came from a different function. A dropped entry is now a refusal: vera run exits nonzero and names both the requested function and the root [E602]/[E620] diagnostic that removed it (--json reports ok: false with the same text). Auto-selection survives only for the never-declared case — no main anywhere in the source — and announces itself with a one-line Note: on stderr naming the function it picked, so the choice is never invisible. The Compilation notes: block is no longer gated on an empty export list; it prints on every run that has skip/drop diagnostics, which is exactly the case (a surviving sibling) where the user was least likely to notice something went missing. The same review's sibling surfaces are closed alongside: vera compile exits nonzero when a program declares a public non-generic function and the module ends up exporting nothing (a file of private helpers, or a cross-module generic library, still compiles clean — neither has an entry point to lose), and vera compile --target browser refuses to write a bundle without a main export — whether main was declared and dropped (the refusal quotes the E620 chain) or never declared at all (it names what is exported instead) — since the generated index.html calls main() on load either way. CompileResult gains dropped_fns, mapping each dropped user function to the diagnostic that explains it, so the refusal quotes the root cause rather than re-deriving it.

• [E602] diagnostics for imported function bodies locate in their own module (#1186). The root skip for a function compiled through the Pass 2.5 / 2.6 import doors carried the MAIN file's path with the MODULE's line and column, so the rendered source line quoted whatever happened to sit at that line in the importer — a stray } in the reported repro. It also kept a branch of _drop_dangling_callers permanently dark: the [E620] caller message prefixes the root location with its file when the root came from elsewhere, but the comparison was against a path that always matched. Imported bodies now compile under the module's own file and source, so the coordinates and the file agree and a cross-file drop reads … (see the [E602] warning at path/to/module.vera, line 5, column 5). Relatedly, vera test reported a PUBLIC function that codegen had dropped as not exported (private) — advice to fix a visibility modifier that was already correct, behind a # pragma: no cover claiming the branch only saw private functions. It now names the actual [E602]/[E620] root and where to find it.

• Runtime traps inside imported functions name the module's file (#1189). fn_source_map — the table vera run resolves a wasmtime trap frame against — was populated by _register_fn, which stamps every entry with the file the generator was constructed for, and that pass runs before the per-module source scope is entered. An imported non-generic function never reached the main generator's registration at all (Pass 0.5 registers module declarations into a throwaway generator), so its frame printed in scaled (<unknown>); the mod$… emission of a locally-shadowed import fared the same way, since the resolver's rightmost-$ strip yields a base that is nobody's entry. A monomorphized clone of an imported generic was registered, and so came out worse: the importer's path paired with the module's line range, coordinates that in the reported repro named a real-but-unrelated function in the importer — a backtrace that reads as correct and is not. The Pass-0.5 registrar is now given the module's own file, its source map is harvested (and mirrored onto the mangled name for a shadowed import), and clone registration runs under the same _module_source_scope Pass 2.5/2.6 already use, so registration and emission agree on which file a body belongs to. Only the file component moves; the line and column were already module-local, and main-file entries are unchanged. This completes the class #1186 opened: PR #1190 fixed the [E602]/[E620] diagnostic locations, this fixes the source maps behind runtime traps.

• old(...) and new(...) applied to an expression report a dedicated diagnostic (#1173), [E030] and [E031], instead of a generic [E005] unexpected-token error. Vera's old/new take an effect reference — old(State<Int>), spec §7.9.2 — so a model reaching for Dafny's old(<expression>) wrote requires(old(@Int.0) > 0) and got a caret on the @ inside the argument, "Expected one of: UPPER_IDENT", boilerplate fix text about missing delimiters, and a pointer to the formal-grammar chapter. Nothing named old, and nothing said what its argument has to be. Found by the VeraBench v0.0.18 sweep (VB-T5-009).

  The caret now lands on old/new itself. The message names the construct, states that the argument is an effect reference and that the call belongs in an ensures() clause, and the rationale gives the reason both rules exist: Vera has no mutable variables, so a slot holds one value for the whole call and effect state is the only thing a call can change. The fix shows both repairs — drop the wrapper for a parameter's value, or name the effect inside ensures().

  The diagnostic is raised at parse time, where the failure occurs. Letting the grammar accept old(<expression>) and rejecting it in the checker is not available: old_expr: "old" "(" expr ")" stops old(State<Int>) parsing at all (the < reads as a comparison), and carrying both alternatives is a reduce/reduce collision between effect_ref and fn_call on UPPER_IDENT. The detector fires only when the parse failed on the first token of an old(/new( argument, so old(State<Int> > 0) — whose real fault is the missing ) — still reports [E005] rather than being blamed on old.

• [E174] and [E175] explain why a precondition cannot host old()/new() (#1173). The rationale now says that a requires() or decreases() clause is itself evaluated before the body runs, so every expression in it already observes the pre-state and the after-state new() names does not yet exist. The fix adds the fact that closes off the obvious retry: a precondition cannot constrain effect state at all, because contract predicates must be pure and old()/new() are the only contract forms that name state.

• Redeclaring a built-in effect is now a compile error, E152 (#1149). An effect IO { ... } block — or State<T>, Exn<E>, Http, Random, Inference, DB, Diverge, Async, HttpServer — used to override the built-in at checker level, which spec §9.5.1 sanctioned "for backward compatibility". Code generation never honoured it: a qualified IO.print(...) is lowered to the fixed host import selected by the qualifier name, and the declaration is never read. So a block whose operation signature diverged from the built-in (op print(String, String -> Unit), op query(String -> ...)) passed both vera check and vera compile with exit 0 and no diagnostic, then trapped at vera run on structurally invalid WebAssembly. An ordinary typo in the idiomatic-but-optional declaration reached it.

  The gate is name-keyed and unconditional — a faithful redeclaration is rejected too, because it is a second textual spelling of the same program (DESIGN.md, spec §0.2 design goal 3, one canonical form). It is the sibling of E151 for built-in functions, and it reads the name set from the live effect registry rather than a hand-list, so a future built-in effect is covered the moment it is registered; a differential test pins that set equal to what vera effects --json publishes. The rejected block is not registered, so the built-in stays canonical and call sites resolve against it instead of cascading arity errors. A module redeclaring a built-in effect surfaces E152 into its importer, as E151 already did.

  Exn<E> becomes a real entry in the effect registry as part of this. It was recognised only by code generation (handle[Exn<E>]), so handle and throw needed the very effect Exn<E> { op throw(E -> Never); } block the new rule forbids; it is now in scope with no declaration, like IO and State<T>. vera effects --json reports its type_params as ["E"], matching spec §7.7.2, where the hand-written entry it replaces said ["T"].

  Spec §9.5.1 is amended: the backward-compatibility override sentence is deleted and the strict rule stated in its place. §7.7 opens with the rule as one blanket statement over the whole registered set — including the operationless markers Diverge, HttpServer and Async, where having nothing to declare does not make the block legal — rather than a per-effect sentence or a name list that would drift from the registry. §7.2 gains it as a numbered constraint on effect declarations and its examples move to user-defined effect names; §7.7 and §9.5 present each built-in's operations as a table rather than in declaration form, since that form is no longer writable. The effect IO {} / effect Exn<E> {} blocks are removed from 12 examples and 20 conformance programs, and new conformance program ch09_builtin_effect_redefinition_rejected (170, was 169) pins the divergent-print repro as an E152 negative. The #309 SQL literal-provenance gate is untouched: it still keys on the codegen routing axis rather than built-in OpInfo identity, and its tests now assert that E207 fires alongside E152 on a user effect DB shadow — defence in depth behind the new rule, not a replacement for it.

• fn old / fn new declarations are rejected at the declaration site, E153 (#1181). The grammar reserves old( and new( in expression position for the contract state forms — old_expr / new_expr in vera/grammar.lark, each of which demands an effect reference — so a bare call old(5) is always read as a malformed state reference ([E030]/[E031], #1173) and never resolves to a function — not in the declaring file, and not inside the declaring module either. One route did reach such a function: a module-qualified mod::old(...) parses through the module-call rule, so a module export named old was callable cross-module (and only cross-module) — adversarial review of the fix confirmed the shape checked and ran. The declaration is now refused outright, reserving the whole identifier rather than leaving it a trap in every unqualified position, the sibling of E151 (built-in functions) and E152 (built-in effects) under the same one-canonical-form rule. Breaking: a module export named old or new that was called via the qualified route must be renamed. The gate covers top-level and private functions, generic forall<T> functions, where-helpers (called in expression position exactly like top-level functions), and modules — a module declaring fn old surfaces E153 into its importer, as E151 and E152 already do. The reservation is on the whole identifier, so older / renew / news stay legal.

  This half of the gate covers the two contract state forms; the keyword class the contextual lexer also admits as a function name is reserved separately, by #1187 below. The probe record lives in the test docstrings. Spec §5.2 states the rule; new conformance program ch05_reserved_fn_name_rejected (172, was 171) pins it as an E153 negative. Mutation-validated: emptying the reserved set, dropping the where-helper recursion, dropping the module surfacing, and matching on prefix rather than whole identifier each flip their targeted tests RED.

• A function named after a grammar keyword is rejected at the declaration site, E153 (#1187). Lark's contextual lexer re-lexes assert, assume, forall, exists, match, if, let, fn, true and false as ordinary identifiers after fn, so each declares cleanly — and none can be written in expression position, where the spelling is always the keyword: a bare match(3) does not parse at all ([E005]), and assert(3) / assume(3) are read as the statement forms and collide ([E121] plus [E172]/[E173]). Every one is a declarable trap, so the reservation refuses the mistake at its source rather than letting it surface as whichever call-site error the spelling happens to produce — the same one-canonical-form rule that already covers the contract state forms (#1181), built-in functions (E151) and built-in effects (E152). Breaking: a module-qualified mod::match(...) parses through the module-call rule rather than any keyword rule, so a module export under one of these names was callable cross-module (and only cross-module) — probed on the pre-fix tree, the shape checked and ran. Such an export must be renamed; the breakage is loud and located at the module's declaration.

  handle is carved out and stays legal: public fn handle(@Request -> @Response) is the entry point the host invokes under vera serve and wasi:http (spec §9.5.6, examples/http_server.vera), so being uncallable from Vera source does not make it dead code. It lives in a named _HOST_INVOKED_FN_NAMES set subtracted from the reservation, so a future host-invoked entry point joins it deliberately rather than by editing a flat list. The E153 rationale branches with the reason — a keyword is not described as a contract state form — while the fix stays "rename" on both. The gate inherits the #1181 shape: top-level, private and generic forall<T> functions, where-helpers, and modules (a module declaring fn match surfaces E153 into its importer, carrying the module's own file path). Matching is on the whole identifier, so matched / letter / iffy stay legal, and op <keyword>(...) inside an effect block never reaches the gate — the lexer refuses that spelling at parse ([E005]), pinned so a grammar change that admits it shows up as a failure to widen. Spec §5.2 states both halves of the rule; new conformance program ch05_reserved_keyword_fn_rejected (176, was 175) pins it as an E153 negative. Mutation-validated: emptying the keyword set flips the ten keyword tests RED with the old/new tests still green, and emptying the carve-out flips the handle control RED (and breaks examples/http_server.vera and ch09_http_server).

• Vera-prefixed type names are reserved for the prelude, E154 (#1184 review). The prelude's combinators resolve their parameter types through generated declarations in that namespace (VeraOptionMapFn; type parameters VeraA/VeraB, #869), and inject_prelude skips any of its declarations whose name a user program already spells — so type VeraOptionMapFn = Int; silently re-typed the prelude's own signatures: check-green, then a WebAssembly validation failure at run. Declaring a type or alias whose name begins with Vera plus an uppercase letter or digit is now refused at the declaration, with module declarations surfacing the error into their importer as the E151/E152/E153 family does. Ordinary names merely containing the letters (Veranda, MyVeraThing) are unaffected, and shadowing the unprefixed prelude aliases (OptionMapFn) remains legal. New conformance program ch08_reserved_vera_prefix_rejected (175, was 174) pins the rule.

• scripts/check_site_assets.py gates the facts docs/index.html and docs/index.md both state (#1154). The Markdown companion agents fetch via rel="alternate" and llms.txt is emitted by build_index_md() in scripts/build_site.py, which holds the landing page's substance as a hand-maintained f-string. The staleness check called that generator and compared the result against the committed file — the generator on both sides of the comparison — so a generator that missed an edit to the hand-designed HTML produced a committed asset stale in exactly the same way, and the gate passed. A v0.0.7-era benchmark section survived every intervening release that way.

  check_fact_coherence() now extracts the load-bearing facts from each file independently and fails when they diverge: the VeraBench version and the Vera release it was measured against, the landing-page version badge, the problem/tier/model/provider counts, the headline perfect-Vera count, the nine-row results table (model name, tier and all three figures per row, plus each file's row count against its own stated model count), and the three editor names. An error names the fact, both values and both paths. A fact that cannot be located is itself a failure rather than a silent skip, so a reworded sentence cannot switch its own check off.

• Type aliases are module-local in codegen, matching spec §8.4.1 (#1111). Codegen merged every imported module's type aliases into one flat bare-name map (setdefault, first module won) and let the main file's aliases overwrite it, so two modules legally reusing one alias name for different targets — or a main-file alias sharing a module's alias name — re-typed one side's declarations through the other's namespace: wrong WASM signatures, invalid modules at run, an import-order-dependent victim, and (where representations coincide) silently wrong values. Each module's aliases are now captured in a per-module namespace and its declarations — Pass 2.5/2.6 bodies and monomorphized clones of its generics alike — compile and register under {prelude, module's own}; harvested return types are canonicalized against the defining module's maps before entering the shared registries, so no consumer can re-resolve them against the wrong namespace.

• A user type alias named after one of the prelude's fn-type aliases no longer disables the combinator it names (#1184). The prelude spells its closure-taking combinators' parameters through type aliases — option_map(@Option<VeraA>, @OptionMapFn<VeraA, VeraB>) — because a slot reference needs a type name, and those names were injected into the same namespace user code declares into. So a type OptionMapFn = Int; (or OptionBindFn, or ResultMapFn) re-typed the prelude's declaration: the mirror of the #1111 defect spec §8.4.1 forbids in the other direction. The two namespaces then disagreed about it, and neither was right. In the main file the user's alias won the flat maps outright, so option_map was emitted with an Int (i64) parameter where the call site passes a closure funcref, and vera run died at WASM validation. In an imported module the same collision was silent: Pass-1.5 instantiation discovery ran under the flat maps and created option_map$Int_JInt, while the module body — compiled under {prelude, module's own}, where the module's alias won — bound the combinator's return type parameter to the phantom-var default and called option_map$Int_JBool. A missing call target is an [E602] warning, so the function was skipped and its caller dropped, and check, verify and compile all reported success over a program with empty exports.

  The prelude's own combinators now resolve through reserved Vera-prefixed twins of those aliases (VeraOptionMapFn, VeraOptionBindFn, VeraResultMapFn), derived mechanically from the public declarations rather than restated, and injected with the bodies that need them rather than with the user-facing block a program can suppress. This is #869's remedy — reserved names no ordinary user declaration spells, keeping prelude internals invisible to user namespace decisions — applied to the alias names rather than the type-parameter names. The user-facing OptionMapFn, OptionBindFn, ResultMapFn, ArrayMapFn, ArrayFilterFn and ArrayFoldFn names stay injected and stay the user's to shadow: a colliding alias keeps meaning exactly what the user wrote, in both namespaces, and the combinator keeps working alongside it. The per-module alias scope also overlays its two maps as a pair in the same change, so a module alias shadowing a parameterized prelude alias with a non-parameterized one can no longer inherit the prelude's stale type-parameter list. Spec §8.4.1 states the rule.

• decreases clauses are enforced at run time — E525's promise is no longer empty (#1172). A Tier-3 termination obligation warned that the metric "will be checked at runtime", but decreases had no runtime lowering at all: a non-terminating recursion passed check, passed verify, and hung at run (found by the VeraBench v0.0.18 sweep, VB-T4-006). A function with a decreases clause now carries an entry guard (whenever the backend can express its measure — the honest limits below): on re-entry, the measure — scalars by value, ADT measures by structural size (a generated $dec_size_<T> helper), lexicographic tuples componentwise per spec §5.6.1 — must be strictly less than the previous activation's and non-negative, or the program traps through the contract-violation channel with a message naming the function. Guard state is per function and restored at every exit, and tail-call optimization is preserved for self-recursion — a self-recursive return_call carries a call-site check (arguments captured, the measure evaluated over them against the live chain state, the activation's guard state closed out before transfer), so the documented pure-iteration idiom keeps its constant-stack depth (#517's 1M-iteration property is regression-tested); only mutual-tail recursion between guarded functions falls back to plain calls, also closing #1176 in the same change. Alongside: the checker now rejects measures with no well-founded ordering (Float64/String/Bool and friends, new E127, previously accepted silently as decorative), and spec §5.6.1's own lexicographic Ackermann example is corrected — as printed its permuted arguments made it non-terminating, exactly the class its decreases clause was meant to rule out. The guard also caught examples/gc_pressure.vera declaring its accumulator as the measure (it grows every hop) — corrected to the counter. A measure of a parameterized ADT type is not yet runtime-ranked (the registered generic layout does not describe concrete construction) and stays honestly Tier-3-disclosed, as does any function declaring Exn — an unwinding throw would bypass the exit restores and leave a stale baseline that traps a later terminating call — and any measure the backend cannot translate. An independent adversarial review then hardened the tier contract: tail calls from a guarded function to an unguarded one are demoted to plain calls (an unguarded trampoline could re-enter with the chain zeroed and loop unchecked), and the verifier's decreases call-walker now descends into handler clauses, closure bodies, constructor/qualified/module-call arguments, index expressions, array literals, interpolation, and assert/assume — a measure-violating recursive call hidden there previously rode a false Tier-1 proof that the new guard exposed as a verify-green run-time trap.

• A codegen skip now propagates to its (transitive) callers instead of surfacing a raw wasmtime error (#1100). An [E602]-class skip drops a function from the emitted module, but every caller's call $f / return_call $f was still emitted, so a check- and verify-clean program whose skipped construct sat in a called helper failed at compile/run with WAT compilation failed: unknown func: failed to find name $f — loud and never a wrong answer, but a WAT internals dump instead of a Vera diagnostic (found in the #1098 adversarial review, whose negative test sidestepped it by putting the skipped construct directly in main). A new pre-assembly pass (_drop_dangling_callers, vera/codegen/core.py) now walks the emitted WAT — the exact symbol stream wasmtime resolves, so mono-mangled (f$Int), module-qualified (mod$f), and where-helper call targets are matched without re-deriving any renaming logic — and drops the whole doomed caller subgraph to a fixed point: each dropped caller gets its own new [E620] warning ("Caller of a skipped function", registered in vera errors) naming the ROOT skipped function and its skip location plus the direct call edge (calls function 'mid', which was dropped because function 'sunk' was skipped … at line 2, column 34), so the module always assembles and the user is pointed at the construct to fix rather than at generated WAT (DESIGN.md principle 1). Propagation follows the same graceful-degradation semantics as the root [E602] skip itself (spec §11.4.1): warnings, not errors — a caller-of-skipped program now behaves exactly like the skipped-construct-directly-in-main shape always did (clean compile, the subgraph absent from the exports, vera run reporting the missing export with the explanatory notes). Lifted closures participate on both sides: a closure body holding the only call $skipped dooms its parent through an explicit construction edge (the parent's WAT carries only a function-table index, invisible to a symbol scan), and a doomed closure's body is replaced by an unreachable stub rather than removed, because later closures' closure_id ↔ table-index correspondence depends on every earlier (elem …) slot staying occupied. Functions outside the doomed subgraph — including their exports — are untouched, and call-graph cycles (mutual recursion) terminate at the fixed point. Pinned by tests/test_codegen_skip_propagation_1100.py (the repro, depth-2 transitive drops in BOTH declaration-order permutations so a single-sweep propagation goes RED, an untouched-sibling run, mutual-recursion termination, the closure shape, root-cause naming with location, and a no-callers control), with four mutations — single-sweep, dropped closure edge, dropped stubbing, hop-instead-of-root threading — each killed by a named test; the CLI legs (tests/test_cli.py) pin the clean text and JSON envelopes, and the #1004 codegen-error-path warning flush keeps coverage via a typed-hole fixture, since the original dangling-caller fixture now takes the clean-drop path.

• A call_indirect is never emitted without a function table to dispatch on (#1185). The unclosed half of the #1100 class: an indirect call names no symbol, so the caller-drop pass — which scans the emitted WAT for call $f — could not see it. When an [E602] skip swallowed a module's only closure, the lift rolled back and module assembly suppressed the (table)/(elem) sections, but every surviving carrier kept its call_indirect into a table that no longer existed. The result was an uninstantiable module emitted with zero error diagnostics: running any unrelated export — a function with nothing to do with closures — raised a raw WasmtimeError: … unknown table 0: table index out of bounds. Two emission sites reproduce it, since a carrier need hold no closure of its own: the apply_fn special form, which lowers a closure-typed parameter to call_indirect unconditionally, and a monomorphized clone of a prelude combinator such as option_map. The drop now propagates to the carriers exactly as it does to ordinary callers — with no table in the module a carrier's indirect call can only have targeted a dropped closure, so the carrier is seeded into the same fixed point and dropped with its own [E620] naming the [E602] root that emptied the table, and its own callers drop transitively behind it. Emitting an empty table instead was rejected: an instantiable module whose call_indirect traps at call time with an opaque wasmtime error is strictly worse than a located refusal (DESIGN.md principle 1, fail loud). A program that applies a closure-typed parameter while never writing a closure at all — no skip, no [E602], previously no diagnostic of any kind — is the same absent table and drops the same way, with an [E620] that explains the absence on its own terms. The invariant is enforced as a differential over the two sides that must agree, the instruction stream and the table section: tests/codegen_helpers.py::_assert_no_orphan_call_indirect runs on every compile in the codegen suite, so a future desync between them cannot hide behind a green unit test the way this one did for the whole #1100 cycle. #1100's acceptance helper is hardened alongside: it checked the diagnostics plus a non-empty wasm_bytes and never handed the module to wasmtime, which is precisely why it passed on this shape — it now loads the module, so the helper catches the class itself.

Documentation

• The VeraBench section carries the v0.0.18 sweep (#1169), the first in which all 60 problems are graded — v0.0.17 took the gradeable set from 36 to 46 and v0.0.18 closed it. One problem is now worth 1.7 percentage points rather than 2.8. Six of the nine models solve every Vera problem, and Vera is highest or level with it for six of the nine. Measured against Vera v0.1.8. The section also gains the reading the wider gradeable set supports: Python is dynamically typed and TypeScript is not, Vera sits with TypeScript and goes further, and sorting the three by how much they constrain the model rather than by how much of them it has read puts the two constraining languages ahead — TypeScript with training data behind it, Vera without.

  Every figure was cross-checked cell by cell against vera-bench#120, the pending results rewrite in the benchmark repo; all 27 published cells agree, as do both headline counts. The landing page's numbers and the benchmark repo's are the same measurement, not two independent transcriptions of it.

  Propagated to every surface that carries the figures, which the HTML edit alone does not reach: build_index_md() in scripts/build_site.py — the generator that is docs/index.md, since that file is not derived from the HTML — plus README.md and FAQ.md, then docs/index.md and docs/llms-full.txt regenerated. This is the drift class #1154 describes: check_site_assets.py regenerates from the same function it compares against, so a stale generator validates as up to date and only a reader notices.