v0.1.11

Added

• [E130] lists the bindings in scope at the error position (#558). An unresolved slot reference reported only how many same-typed bindings existed, so recovering the right index meant tracing pattern pushes and lets by hand, or writing a typed hole and re-running — vera check --explain-slots stops at the signature and is no help several levels into a match arm. The fix text now ends with the same Available bindings: @T.n: Type; … table the W001 typed-hole warning already emits, rendered from the scope at the reference itself, so the read-time diagnostic carries what the write-time one always did — the same set from the same helper, zero-size bindings included, because the index range in the description counts them and hiding them would make one diagnostic describe two different scopes (@Unit.1 against (@Unit, @Int) reporting "valid indices: 0..0" above a table with no Unit row). A zero-size read stays E182's to explain. Nothing is appended when no binding is in scope. The table renders at most twelve rows and then ; … and K more, because the scope it reports is unbounded and the language server concatenates the fix into the hover message, so a wide function would turn one diagnostic into a wall of rows nobody reads — thirty same-typed parameters rendered a 492-character fix. Twelve sits above the measured corpus: across the 2,080 slot-reference positions in tests/**/*.vera and examples/ the table is 7 rows at the 95th percentile and 11 at the 99th, so every position through the 99th renders complete and 12 of the 2,080 elide. W001 renders through the same capped helper, so the two diagnostics still agree row for row; the LSP's typed-hole completion consumes the binding list itself and keeps every row, since there a dropped row is a missing completion item. This is the issue's option (a); the positional query (option (b), --explain-slots-at <line>:<col>) stays open on the roadmap.

• The browser runtime's untested host imports are now exercised, and the two divergences that fell out are pinned rather than papered over. tests/test_browser.py gains a battery covering the Map, Set, Decimal, readJson/json_stringify and Result.Err bindings that vera/browser/runtime.mjs registered but nothing ever invoked — several closure bodies had zero hits — taking the file from 81.74% to 86.86% lines under the VERA_JS_COVERAGE=1 pytest tests/test_browser.py command TESTING.md documents (#349). Each case compiles one .wasm and runs it under both wasmtime and Node, so a failure isolates the host import rather than codegen. Writing them surfaced two browser↔native divergences of the kind spec §12.9.3 forbids: json_stringify differs on separator padding and on integral-number rendering, and traps natively on a NaN number where the browser silently emits null (#1293); and md_render breaks the round-trip property §9.7.6 states for it on any multi-line paragraph — not just the list lazy continuation first observed — is not stable under re-render, and destroys a nested blockquote outright the second time round (#1294). Neither is fixed here, because fixing means editing runtime.mjs and this change is tests and documentation only; instead both runtimes' exact current strings are asserted separately, including the destructive blockquote case, so a fix on either side goes red until the pins are updated deliberately. Alongside them, TESTING.md drops a "91% combined" coverage figure that no documented command produces (the two collectors measure different line populations, so the blend needs a line-weighted total neither report emits), corrects a blanket claim that no action ref is pinned to a commit SHA — pypa/gh-action-pypi-publish and codecov/codecov-action both are — refreshes its ~109,000-line test-corpus estimate to the measured ~152,000, and repopulates its Open CI/Tooling Issues table, which had been emptied to "No open CI/tooling issues" while six remained open. vera/README.md and FAQ.md lose an unqualified "identical results" parity claim that the two divergences above contradict, along with a stale hand-count of parity tests and a runtime-family count that disagreed with itself in three places against the fourteen register_<effect> entry points vera/runtime/ actually defines.

• The editor grammars are gated against the effect registry. The three grammars under editors/ (vscode, TextMate, Vim) enumerate the built-in effect names by hand and nothing checked them, so they drifted: HttpServer, Inference and Random never reached the vscode and TextMate grammars, and DB reached none of the three. The drift is silent — an unknown capitalised identifier falls through to the generic type-reference rule, so DB.query(...) still highlights as something, just not as an effect — so four accumulated unnoticed. scripts/check_editor_grammars.py reads vera.introspect.effects_payload() from the checkout it is checking and requires a word-boundary occurrence of every registered name in each grammar, and in the two extension READMEs that repeat the list in prose and had gone stale in exactly the same way. Absence is conclusive, presence is optimistic, which is the right way round when the failure is omission and keeps the check immune to the formats involved (JSON, plist XML, Vim regex, Markdown). The checked list is explicit, since not every file under editors/ is a grammar, so it is paired with a completeness guard: a file in a syntax directory, or carrying a grammar extension — the tree-sitter .scm query sets and a .tmLanguage.json filed anywhere but syntaxes/ among them — that the list does not name fails the gate rather than passing unchecked. It runs as a pre-commit hook and a CI step, triggered by editors/ and by the registry files themselves, since adding an effect is what puts the grammars out of date. Registering that CI step exposed the same defect one layer out — TESTING.md's CI-pipeline table hand-enumerates the scripts the lint job runs and nothing held the two in step, so the new step left the table describing 22 of the 23 scripts the job invokes; scripts/check_doc_counts.py now compares that row against the workflow as an ordered list, treating a reworded row or a renamed job as an error rather than a skip. Abilities (Eq/Hash/Ord/Show) stay out of scope: whether they should highlight distinctly from ordinary types is an open design question, tracked separately as #1295.

• xAI (Grok) provider for the Inference effect, and one flagship model per provider (#425) — Inference.complete now supports Grok models. Set VERA_XAI_API_KEY to use. xAI's endpoint is OpenAI-compatible (bearer auth, choices[0].message.content), so this is one row in the _PROVIDERS registry with no new dispatch code. Appended last in the registry, which leaves the existing auto-detect precedence unchanged. (The issue asks for grok-3-mini-fast-beta, which xAI documents nowhere any more — neither in its model list nor in the retirement table that names the redirect target for each slug it withdrew — so the default is a currently-listed model instead.) Alongside it, every row's default_model is now that provider's flagship general-chat model rather than its cheap/fast tier: claude-opus-5, gpt-5.6-sol, kimi-k3, mistral-large-latest, and grok-4.6 for the new row. Each was verified against the vendor's own live documentation at the time of the change, which also retired two IDs their vendors no longer list (gpt-4o-mini, kimi-k2-0905-preview). A program's contracts are written against what the default model can do, so capability — not price — is what the default owes the caller; the cheap tier stays one VERA_INFERENCE_MODEL away. This raises the per-call cost of any program that relies on the default, on every provider. The provider tests now pin each model ID as a literal: test_openai_provider asserted against _PROVIDERS["openai"].default_model, which pinned the value to itself and would have stayed green through the flip, and test_anthropic_provider asserted no model at all. test_xai_provider also asserts the request's Content-Type, which its OpenAI sibling checked and it did not, so the new row's headers are pinned as completely as the row it was modelled on. The auto-detect tests assert the API key that reaches _call_inference_provider, not only the provider name it selected: with two keys set, naming the right row while reading another row's environment variable satisfies a name-only assertion, and the four-case precedence test now fails on exactly that. SKILL.md also states the detection rule the tests pin — the registry is walked in insertion order (anthropic, openai, moonshot, mistral, xai) and the first provider whose key is set wins — where it previously said only "auto-detected from whichever key is set", which answers nothing when several are. Detecting IDs that rot at the vendor still needs network access and is tracked in #1263. Closes #425.

Changed

• resume is reserved as a function name, as Chapter 1, Section 1.4 already required. The MUST was unenforced: resume is not a keyword token — vera/grammar.lark has no RESUME terminal and lexes the name as an ordinary LOWER_IDENT everywhere — so private fn resume(@Int -> @Int) parsed, type-checked, and ran, and a bare resume(7) outside a handler resolved to it. The declaration is not merely dead weight: inside every handler clause body the checker binds resume to the effect-resumption operator, and with a top-level declaration present the clause bodies resolved against its signature instead — an otherwise valid handle[State<Int>] was rejected with [E202] on put(@Int) -> { resume(()) } ("has type Unit, expected Int"), and deleting the declaration made the identical handler check clean. Declaring the name broke working code elsewhere in the file. Such a declaration is now rejected at vera check with E153, on the same rail as old/new (#1181) and the grammar keywords (#1187), in a fourth named piece (_HANDLER_OPERATOR_FN_NAMES) with its own rationale — the keyword branch's reason, that no unqualified call site can reach the declaration, is false here and would have misinformed the reader. The rejection is also the only diagnostic the program gets. A bare call resolves lexically — the enclosing where-helpers, then the top-level function of that name, then the flat registry — and the clause binding lives in that last tier, so a declared resume shadowed it and drew a second error out of clause bodies that were correct, at both top level and where-helper depth. resume now resolves against the flat registry alone, which is the only place its binding can live; in a valid program nothing changes, because the name is reserved and no declaration of it exists to be found. The reservation is on declarations only: resume(...) inside a handler clause is bound by the handler rather than declared and is untouched, as is resumed or any other longer name. A where-helper named resume is rejected one scope deeper, like every other reserved name. Covered by tests/conformance/ch05_reserved_resume_fn_rejected.vera. The neighbouring statement in Chapter 10 — that resume is a LOWER_IDENT and resume(expr) parses as an ordinary fn_call — remains true, and now says which phase enforces the reservation instead.

• vera/addEffect bounds its propagation at handlers (#725). The transitive-caller closure was handler-unaware: a caller that wrapped its call in handle[E] had E appended to its own effects(...) row even though the handler discharges it there, so the workflow wrote rows the program does not need and dragged that caller's own callers in behind it. A call site inside a handle[E] body now contributes no edge, so propagation stops at the function that discharges the effect. Three cases deliberately still propagate, because the effect really does escape them: a caller that reaches the callee on any unhandled path as well (the row is needed for that path), a call in a handler clause body, which runs outside its own handler, and a call in the handler's state initialiser, which escapes for a different reason — the initialiser is evaluated in the enclosing scope, before the handler is installed, so an effectful call there is an E125 against the caller's own row. A handler bounds the propagation only when its handle[...] head is spelled the way the request is, type arguments included and compared as written rather than as resolved. That is required in one direction: the checker discharges against EffectInstance equality, so handle[State<Nat>] leaves State<Int> escaping and a caller around it still needs the row — pruning that edge on a base-name match would leave the caller pure and fail the whole candidate on E125. In the other direction it under-prunes: handle[State<MyAlias>] with type MyAlias = Int is discharged by the checker but is not spelled the way a State<Int> request is, so that caller keeps a row it does not need — documented behaviour until #1292 keys the bound on the resolved instance. Every non-match keeps the edge, which is the safe direction: a row the program does not strictly need still type-checks. (Row identity, a separate question, remains the base name — State<Int> is not appended beside an existing State<Bool>.) Containment is structural (the handled sub-tree), not span arithmetic, so the handler bound applies inside a where-helper body exactly as it does at the top level, and a helper's bare call still attributes to its containing top-level function as before. Row rewriting is unchanged and still top-level-only: a where helper that needs the new effect does not get it, and the gate refuses the resulting candidate rather than applying a broken one. The KNOWN_ISSUES.md limitation row is retired. The LSP_SERVER.md row stated two things, only one of which is fixed, so it is replaced by a by-design row for the other: propagation still stops at the file boundary.

• DeepSeek provider for the Inference effect (#450) — Inference.complete now supports DeepSeek. Set VERA_DEEPSEEK_API_KEY to use. DeepSeek's endpoint is OpenAI-compatible (bearer auth, choices[0].message.content), so this is one row in the _PROVIDERS registry with no new dispatch code — the issue's proposed env-var fetch in host_inference_complete would have been dead code, since that function already iterates the registry. Appended last, after xai, leaving the existing auto-detect precedence unchanged. The default is deepseek-v4-pro, following the one-flagship-model-per-provider convention the other five rows adopted in #425: DeepSeek's own API reference lists exactly two current model values, deepseek-v4-flash and deepseek-v4-pro, and positions the latter as the flagship — its change log records "The GA release of DeepSeek-V4-Pro has been rolled out on the APP, Web, and API" (2026-08-13) against deepseek-v4-flash's public beta (2026-07-31), and every code sample in the documentation's first API call sends deepseek-v4-pro. Capability, not price, is what a default owes the caller, because a program's contracts are written against what the default can do; deepseek-v4-flash is one VERA_INFERENCE_MODEL away. (The issue asks for deepseek-chat with deepseek-reasoner for the reasoning model. DeepSeek's change log announced both discontinued as of 2026-07-24, a date now past, and documents neither; the default is a currently-documented model instead. There is also no reasoning model to point VERA_INFERENCE_MODEL at any more: on v4, thinking mode is a request-body field, which the registry does not send, so no model override reaches it.) The provider tests meet the #425 bar — the model ID and the endpoint as literals rather than registry-derived expressions that would pin each value to itself, the Authorization and Content-Type headers, the absence of Anthropic's x-api-key and max_tokens, the exact turn list, and the API key that reaches _call_inference_provider rather than only the provider name it selected — and the precedence battery runs one case per provider ahead of deepseek, all five, so relocating the row fails exactly the providers it jumped. Detecting IDs that rot at the vendor still needs network access and is tracked in #1263. Closes #450.

Fixed

• Chapter 10's EBNF names the rules the parser actually has (#683). The published grammar still called the assertion forms assert_stmt / assume_stmt after they became expressions (assert_expr / assume_expr in vera/grammar.lark), and three Lark rules appeared in no EBNF block at all: pure_effect and effect_set were inlined into effect_row, and with_clause was missing entirely, leaving the with form of a handler clause undocumented as a production. scripts/check_grammar_alignment.py now holds the two files together in pre-commit and CI — every rule header in one must exist in the other, with a six-entry allowlist for the pairs that differ on purpose (start / program, and the four spec headers Lark expresses as -> alias names or folds into a more general rule). Rule names only; bodies are not compared. Each allowlist entry records the side its name lives on and, where its reason rests on a Lark -> alias, both that alias and the production it must be an alternative of; those facts are checked rather than asserted, against comment-stripped text, so neither deleting the alternative nor commenting it out nor moving it to another rule can hold a waiver up, and deleting the waived spec production fails too instead of passing forever. What the alias premise does not establish is that the Lark alternative still spells the same construct as the spec production — a body-level fact a header-only gate cannot see; tuple_literal and tuple_type rest on constructor_call and named_type, general forms that would outlive tuples leaving the language, and the script says so at both the entry and the module docstring rather than claiming more. A name gone from both files is reported as a broken premise rather than as "the sides now agree" (the old symmetric-difference arithmetic pointed the reader at the deletion that turns the gate green with the construct documented nowhere), and each name yields at most one report, so a spent waiver whose premise also broke no longer asks for the waiver's deletion and its restoration in the same run. The header extractor also tolerates Lark's template parameters and rule priorities (sep{item}.2:), which previously dropped a rule from the Lark set entirely. Two further Chapter 10 defects are fixed: statement carried assert_expr SEMICOLON | assume_expr SEMICOLON alongside expr SEMICOLON, so assert(p); derived two ways in the published grammar while the reference parser has one production (expr ";"); and a RESUME: "resume" terminal was declared but referenced by no production, contradicting the neighbouring note that resume(expr) is an ordinary fn_call — under the spec's own lexer a keyword terminal shadows LOWER_IDENT, and vera/grammar.lark has no such terminal. That criterion, applied to the rest of §10.2 rather than to RESUME alone, clears five more phantom declarations and one omission. SOME / NONE / OK / ERR were declared as keyword terminals and referenced by no production: Some, None, Ok and Err are ordinary prelude ADT constructors (data Option<T> { None, Some(T) }, data Result<T, E> { Ok(T), Err(E) }), so under the spec's own lexer those four declarations would shadow UPPER_IDENT and stop Some(1) parsing as a constructor call at all — the identical defect RESUME had against LOWER_IDENT. COLON was declared for a : that no production in either file uses. All five are deleted. The converse case is fixed with them: module_call referenced a DOUBLE_COLON that §10.2 never declared, now added as DOUBLE_COLON: "::", the spelling vera/grammar.lark carries as an inline literal. The whitespace and comment terminals stay — they are labelled "(skipped)" and %ignored, so no production referencing them is correct. This fixes the six instances; auditing declared-versus-referenced terminals as a gate is #1290's scope, and the rule-name gate here does not compare terminals. The issue also asked for a qualified_call → module_call rename in the Lark grammar, which is not done and should not be: those are two different constructs (Effect.op() and mod::fn()), both already present under both names, and merging them would be a regression. The gate has a test pinning that it never reports them.

• Two documentation statements corrected in review. The FAQ's contract-testing walkthrough read requires(@Int.1 != 0) as constraining the second parameter, inverting the De Bruijn rule the same document links out to: @Int.0 is the most recent binding, so @Int.1 is the leftmost — which is exactly what examples/safe_divide.vera, the example that answer tells the reader to run, guards as its divisor. Separately, the compiler-architecture README's cross-cutting summary credited errors.py with the E-codes alone, where the registry described further down the same file also holds the W001/W002 warning codes.

• TESTING.md's conformance section counts the programs the manifest actually holds. The section states each non-run level twice — as a number in prose and as a hand-written list of program names — and ch05_reserved_resume_fn_rejected reached neither, so the check level read thirty-eight against a manifest holding thirty-nine and the negative-test subset read thirty-one against thirty-two. The parenthesised E-code sequence is aligned to that subset "respectively", so it was short by the same one entry — the thirty-one codes present did pair correctly with the thirty-one names present, which is why the omission left nothing visibly wrong to notice. The same section's parametrized-suite count read 1,035 where the runner collects 1,070 — five checks over each of the 214 programs — a number that had drifted seven programs back, before the fixture above existed. None of the four is gated: scripts/check_doc_counts.py pins the suite total, the per-file table and the skipped-stage rows, but reads neither prose list nor the count in the run instructions, which is why a fixture could land with its skipped-stage rows added and its two list entries missed. All four are corrected against the manifest, which is the oracle for every one of them.

• Three more documentation statements corrected in review. The FAQ's browser-parity answer claimed every operation but json_stringify and md_render behaves identically across the two hosts, which is not true of two whole effects: Inference and DB return an explanatory Err from every operation in the browser, because the API key or database credential they need would be readable from page source. That refusal is now stated as what it is — a deliberate platform boundary, distinct from the two divergences, which are unintended and tracked — alongside the fact that Http genuinely does work there, backed by XMLHttpRequest rather than a stub, so a server-side proxy is a real escape route rather than advice. Separately, TESTING.md described check_doc_counts.py as verifying that "counts cited in the docs match the live codebase", a blanket claim the entry above disproves; it now enumerates the citations the script actually reads, and says plainly that a count it does not name is not read at all and that hand-written program lists are outside its scope. Finally, the compiler-architecture README and its host-families diagram both counted two stateful family adapters, Decimal and State, where there are three: async_http.py's register_async takes a future_store that execute() creates up-front, publishes it as host_store_refs["future"] so its size reaches ExecuteResult.host_store_sizes, and has entries evicted by the same host_decref_handle — kind 4, which also cancels a future that never started (#841). Prose, diagram label, legend and accessible title are corrected together.

• Spec §1.4's reserved-keyword list now matches the checker: exists was missing and handle's host-invoked carve-out was unstated.