v0.1.12

Added

• The examples are now RUN in CI, not only checked, verified and compiled (scripts/check_examples_run.py). check_examples.py type-checks and verifies all 42, and check_e602_clean.py compiles all 42 as a side effect of policing silent translator skips — but nothing executed them as a set, and an audit of every referencing test found seventeen examples that no test ran at all: array_utilities, async_http_fanout, collections, database, fizzbuzz, html, http, inference, io_operations, json, life, maximum_syntax, modules, nested_closures, read_char, scoreboard and string_utilities, plus file_io, which ran only under the browser runtime, where the file IO it demonstrates is a deliberate Err stub. Between them they demonstrate Map/Set, the <DB> effect, JSON and HTML parsing, module imports and the whole string-utility family, so a runtime regression in any of it could reach a release with every gate green. The gate now runs 34 of the 42 under the native runtime and asserts a trap-free exit; the other 8 carry a documented skip property (network, api-key, stdin, non-scalar-entry, long-running) which the report prints with its reason on every run. Output pinning deliberately stays in the dedicated tests that already do it, so the gate does not go red on a cosmetic edit to an example. The load-bearing part is not the runs but the coverage rule: the script enumerates examples/*.vera from disk and requires every name to be in exactly one of its two tables, so an unclassified example is an error and adding one forces the author to decide whether the harness can drive it — and a table key whose file is gone is an error too, so a suppression cannot outlive its example and mask a later program of the same name. The classification is cross-checked against a new execution-coverage table in TESTING.md on the check_doc_counts.py model, the codebase being the oracle and the documentation having to match it, so the execution model stops living in maintainers' heads. Trap-freedom is asserted on two signals, the discipline check_examples.py already applies: the exit code, and an output signal. Either alone accepts a measured failure. Every spec names its entry point rather than relying on vera run's first-export fallback — with main privatised, array_utilities.vera ran a different function and the gate passed; it now exits 1 on the name. And the three examples that reach outside the process (sqlitedb.vera for its committed fixture, database.vera for an in-memory database, file_io.vera for the filesystem) answer a failure by printing a message and completing normally, so each pins a substring only its success path prints — deleting examples/sqlitedb.sqlite left the gate green on the graceful in-memory arm, and now fails on the sentinel. Runs are hermetic: an ambient VERA_DB_URL or inference-provider key is stripped from the environment, so a gate run cannot be pointed at a real database or turned into a billed API request, and each example gets a scratch working directory so file_io.vera stops dropping hello.txt beside the sources. TESTING.md's round-trip section is corrected with them — it claimed all 42 examples were tested through "every pipeline stage ... WASM compilation, and execution", where the directory-globbing parametrised tests in fact stop at verification and canonical form.
• The grammar-alignment gate now compares terminals and production bodies, not only rule names (#1290). scripts/check_grammar_alignment.py held rule-name headers together and was blind to three drift classes, each demonstrated green on a live file during #1279's review: a fabricated terminal added to spec 10.2 (the header pattern requires a lowercase lead, so no terminal was seen at all), a rule reference restored to a right-hand side, and a production body edited on one side only — the class most grammar edits actually fall into. Three checks close them. A terminal audit in both directions, within each file: a terminal declared and never referenced, or referenced and never declared, is now an error — the shapes SOME/NONE/OK/ERR/COLON and DOUBLE_COLON had between them, found by hand and fixed in #1279 with the gate itself unable to see either. A cross-file terminal-pattern check: every terminal the chapter publishes as a bare regex must have that pattern in vera/grammar.lark, as a named terminal or an %ignore, after a semantics-preserving normalisation of Lark's \\/ and \\" escapes — which is the whole of the difference between how the two files spell STRING_LIT and ANNOTATION_COMMENT, and which BLOCK_COMMENT failed. And a production-body comparison over the 80 rules both files declare, of the rules and the terminals each right-hand side refers to, with Lark's quoted literals mapped through the chapter's own terminal table rather than a hand-written one. Two notational differences are folded rather than reported: a rule's reference to itself, since Lark spells repetition with left recursion where the chapter uses a Kleene star, and a waived spec-only production, which the existing ALLOWLIST already pins to the Lark rule that inlines it. The body comparison needs no waivers of its own, and the six-entry rule-name allowlist is unchanged.
• KNOWN_ISSUES.md's Bugs table is gated one row per open bug issue. The structural half is pure text and always on: each row's Issue column must hold exactly one [#N](…/issues/N) link whose number matches its URL, no two rows may claim one issue, and an empty section must be written No known bugs. rather than left as a bare table. The parity half needs the tracker, and a pre-commit hook must not depend on a network call, so it is opt-in through scripts/check_doc_counts.py --check-bug-issues for the release PR — mid-burndown the two legitimately disagree, a bug filed against an open PR's branch having an issue before it has a row.
• TESTING.md's dual-target conformance row is gated against the manifest and a live run. The row states a run-level total, a tested/skipped split and three category counts, and claims the excluded set "stays accurate as programs are added" — a claim nothing measured. The total now comes from the conformance manifest and the rest from a three-second -rs run of the differential itself, with two arithmetic checks the individual figures cannot make: tested plus skipped must be the run-level total, and the three categories must be the skip total. A skip whose reason matches none of the three documented properties fails rather than being folded into one of them.
• check_examples_run.py derives which examples need an output sentinel instead of naming them. The rule was a hard-coded triple — database, file_io, sqlitedb — so a fourth example reaching outside the process could be added with nothing but an exit code asserted, exactly the gap the sentinel exists to close. The set now comes from each program's own declarations: a resource effect in a function's effect row, or a call to a resource operation, read off the parsed AST rather than the source text so a header comment mentioning <DB> is prose. Both halves are needed, and the measurement said so: FileIO and Time are not effects in this language — file and clock operations live under IO — so file_io.vera declares exactly the bare <IO> that hello_world.vera does, and only the operation it calls separates them. What stays hand-written is a short list of registry names, and those are validated against the live effect registry, so a renamed or deleted effect or operation fails loudly rather than silently matching no example. The derived set must equal the specs carrying a sentinel in both directions, so a sentinel on an example with no resource signal is an error too.
• The corpus differential and the grammar gate are hardened against the platform they run on and the patterns they read (PR #1329 review). _first_error stripped the compiled file's path from a diagnostic by matching str(path) alone, which ties the strip to the host's separator: on Windows a diagnostic carrying the POSIX spelling went unstripped and its absolute path pushed the message past the truncation. Both spellings are stripped now, and the parameter is a PurePath so a test can render a Windows path on any host rather than waiting for the Windows CI cell. The grammar gate's comment scanner had the same shape of defect with worse consequences: a / inside a regex character class was read as the closing delimiter, so the chapter's ANNOTATION_COMMENT — which spells the class [^/*] where the Lark grammar escapes it [^\/*] — was truncated, and a truncated body is not a bare regex, so the terminal was skipped from the pattern comparison entirely. That gate was green on it by never looking. Both now have cells that fail on any host. Alongside them: the differential rejects a non-positive --timeout (which would fail every compile and report "no movers" over a corpus that never compiled), decodes compiler output leniently (a stray byte otherwise raised out of subprocess.run and aborted the whole run), checks the base revision out repository-locally rather than under a predictable shared temporary path whose contents it puts on PYTHONPATH, and prints a reproduction command that names the same input it actually compared. check_doc_counts.py reads a pytest summary that omits a zero-count category, and its two external calls — the dual-target run and the tracker query — join the script's own error convention instead of ending the run on a traceback. The chapter's BLOCK_COMMENT production excludes both delimiters from its character alternative, so {- {- -} is no longer derivable from a rule describing a construct the implementation rejects as unterminated.
• scripts/check_corpus_differential.py promotes the burndown's ad-hoc corpus differential to a first-class instrument: it compiles every corpus program at two revisions and reports the movers, including the programs that compile on one side only. It is deliberately not a pre-commit hook — it compiles the whole corpus twice — and is documented as a CI-optional burndown instrument.

Fixed

• Spec §1.4's reserved-keyword MUST is now enforced, for twenty-one names that nothing held (#1296). §1.4 says its keywords must not be used as function names; E153 held that for eleven of them, and private fn with(@Int -> @Int) — with then, else, data, type, module, import, public, private, requires, ensures, invariant, decreases, effect, in, where and pure — declared, type-checked, verified, compiled, ran and round-tripped vera fmt. They were not traps: a bare with(1) resolved to the declaration and returned its value, and stayed working inside a contract clause, inside an if/then/else, in a function carrying its own where { } block, and after a let. The comment above _KEYWORD_FN_NAMES gave the opposite as the reason they were absent from the set — that the contextual lexer "does not admit them as a function name, so no declaration reaches this checker at all" — so the omission rested on a premise the tree refuted, and the divergence was between the specification and the implementation rather than in any program's behaviour: a model trusting §1.4 and a model trusting the compiler derived different programs from one source of truth, with no tool contradicting either. DESIGN principle 1 (checkability) makes an unenforced MUST a defect whatever the program does at runtime, principle 6 (fewer valid programs) chooses enforcement over narrowing §1.4, and principle 3 supplies the precedent — E152 rejects even a faithful re-declaration of a built-in effect, because a second textual spelling is itself the problem. The reserved set is now derived from vera/grammar.lark rather than hand-listed, the shape builtin_effect_names() already uses for E152, so a keyword added to the grammar is reserved the moment it is added; the hand-list this replaces had fallen twenty-one names behind the grammar with no gate able to see the drift. The derivation is what found the other four: ability, effects, op and result are grammar keywords §1.4 never listed and were accepted as function names on the same footing, and §1.4's list is reconciled to the grammar (gaining those four plus old and new, which E153 already reserved). They join E153 as a fourth branch with its own rationale: the existing keyword wording asserts that no call site can reach the declaration, which is false for every one of these names, so reusing it would have told authors a falsehood about their own program — the new branch argues from the reservation instead, and carries a per-name rename suggestion because the generic <name>_fn template produces in_fn / type_fn / pure_fn. handle stays legal, carved out as the host-invoked vera serve / wasi:http entry point; the reservation remains on the whole identifier, so older, with_it and then_value are ordinary names. §1.4's "type names" half is corrected rather than enforced: every type-namespace binder in the grammar is an UPPER_IDENT and every keyword is lowercase, so that half was never violable. New conformance negative ch05_reserved_contextual_keyword_fn_rejected plus 110 tests in tests/test_checker_modules.py — five parametrized batteries over all 21 (declaration, visibility, where-helper, rationale-free-of-the-false-claim, and a usable fix suggestion) with handle and fifteen keyword-containing names as controls; mutation-validated by dropping one keyword from the derivation, which flips that name's five cells and both set pins red while the other twenty stay green. Corpus differential: zero movers, no program in examples/ or tests/conformance/ having used such a name.

• Two imports supplying one bare name are refused, in every namespace (#1304). Spec §8.5 ordered a local declaration against an import (§8.5.2) and gave the module-qualified form for reaching what a clash hides (§8.5.3), but defined no order between two imports that both supply one name. Neither did the implementation, and the gap was reachable: a module importing two dependencies that each export forall<T> fn gen — one returning @Int, one @Bool — bound its bare call to whichever supplier a set of module paths happened to yield first, so one unchanged file was vera check-green on one run and [E121] body has type Bool on the next. Measured at the branch point across eight consecutive runs and eight hash seeds: accepted on seeds 0, 2 and 3, rejected on 1, 4, 5, 6 and 7, with the winner tracking module-name hash order rather than which import is written first. Codegen's E608 rail caught the entry-visible pair before it could matter there; the flap lived in the shapes the rail only reached at compile, from inside a module the entry program merely imports. Spec §8.5.2.2 now states the rule — a program MUST NOT leave a namespace with two imports supplying one bare function name — and the checker enforces it as E155, a check-phase code for a scope question that had been enforced by a codegen rail at the wrong layer. Refusing is what removes the flap rather than merely labelling it: with no pick to make, there is no iteration order left to expose, which a deterministic first-wins order would not have achieved (it would make the resolved declaration implicit in import sequence, §0.2.2, and let a library adding an export silently rebind a downstream bare call). The refusal is definition-gated, matching the rail it generalises: it fires because the import pair exists, not because a body names it, so an entry program importing two suppliers and never calling either is refused exactly as E608 already refused it, and rewriting a bare call in module-qualified form does not lift it. Two shapes clear it, both exercised through to their runtime value: a local declaration of the name (§8.5.2 — every bare call is then the local one, and each import stays reachable through dep::name(...)), or a selective import narrowing the other module's list. The ambiguity predicate is the one namespace_fn_names already derived for #1281 and #1299, now exposed per namespace as well as unioned, so the layer that refuses early and the layer that backstops it cannot disagree about which shape is ambiguous; the E608 condition keeps its cell, driven through a door that bypasses the checker. An ambiguous name is not injected into the type environment at all — reporting the clash while binding one supplier would leave the follow-on diagnostics keyed to whichever module the injection loop reached first, which is the nondeterminism the refusal exists to remove — so a bare call to it misses with an ordinary E200 instead — an E-coded diagnostic emitted at warning severity, which the --json envelope reports in warnings rather than diagnostics and which does not fail the check on its own (measured: a program whose only diagnostic is E200 reports ok: true and exits 0). The W-series is the separate W001/W002 code namespace, and this is not one of them. The data namespaces flapped the same way and are folded in. Spec §8.5.4 gives constructor names the same shadowing rules as function names, which a function-only refusal would have made false: two modules each exporting a public data Shape with different constructor field types type-checked on some hash seeds and reported [E213] on others (accepted on seeds 2, 8, 9, 10 and 11; rejected on 0, 1, 3, 4, 5, 6 and 7), and the accepting seeds were the worse half — check and verify both passed, and the program died at run with an E609 located at line 0 of the entry file, naming two modules the entry never imported. Data types are now E156 and constructors E157, one code per declaration namespace exactly as codegen splits E608/E609/E610, and reported independently because they come apart: two modules exporting differently-named types that share a constructor name clash on the constructor alone. Their remedy differs from the function one and says so — E609/E610 refuse two modules' same-named data declarations by DECLARATION, consulting neither visibility nor the importer's filter nor local shadowing (the relaxation E608 received in #1281 has no data-side twin), so narrowing an import or shadowing the name locally leaves the program E609 at compile. Both were measured against the fixture and both fail — as does marking one declaration private — so the two diagnostics prescribe renaming, and a cell pins that measurement so the fix text cannot drift into offering remedies that do not work. That rail over-breadth is now tracked as #1317. A name the built-in registry already owns is not a clash — the injection loops are setdefault over a TypeEnv the built-ins populate first, so a dependency exporting its own option_map never wins the bare name (measured as E201 against the prelude's two-argument signature). The first cut of this refusal did not pass the built-in snapshot and reported two such dependencies as a clash, which was a new rejection rather than an earlier one; namespace_fn_names' claim that its ambiguity half is identical with or without the prelude argument was wrong for the same reason and is corrected, with the codegen call ordering it depends on now pinned by a cell.

• A throw payload is runtime-guarded, not only obligated (#1268). throw(v) narrows v into the Exn<E> payload, and since the static half of this issue the narrowing carries the same obligation every other binding site does — but codegen emitted no guard, so the obligation's Tier-3 leg promised a runtime check that did not exist and an unverified vera compile/run delivered the violating value anyway. throw(0 - 5) under effects(<Exn<Nat>>) ran to completion and returned -5 through the @Nat payload; the refined spelling (type Pos = { @Int | @Int.0 > 0 }) did the same. Worse than a wrong answer: a handler clause binds the payload at its declared type, so the verifier hands every downstream consumer the invariant the payload just broke — a @Nat-taking function discharging ensures(@Bool.result) at Tier 1 from its parameter's type alone reported a postcondition violation at run time on a postcondition vera verify had proved. throw now takes the write boundary's guards at its op-call site, beside put's (#1203): the @Int -> @Nat sign guard, the @Nat -> @Int widening guard, and — refined FIRST, as at every other narrowing site — the §2.6.5 predicate guard for a refined payload, which traps through $vera.contract_fail naming the predicate that failed (Refinement violation in throw(@Pos) / payload: @Int.0 > 0 failed). The three arms mirror the verifier's own obligation triple one-for-one, so the obligation stream and the emitted guards stay in lock-step: the payload obligation is now guarded at all three arms and its Tier-3 leg is counted in tier3_runtime rather than disclosed as tier3_unguarded, and the refined arm's guarded claim is intersected with the same _refined_boundary_codegen_guardable test every other refined site uses, so an erased @Unit base or a nested refinement — which codegen emits no guard for — stays honestly unguarded. That mirror needed one repair to be true: it answered "guarded" for a refinement OVER a refinement, which _refinement_guard_parts refuses outright with a loud E618 because the outer predicate alone would silently drop the inner membership — so vera verify exited 0 recording a Tier-3 runtime check for a program vera compile then refuses, a promise about a run that can never happen. It now bails on a refinement base, and the obligation discloses tier3_unguarded while E618 still refuses. The same audit found the qualified spelling recording something different from the bare one: the QualifiedCall arm hardcoded guarded=False behind a comment stale since #1203, so Exn.throw(v) — which codegen lowers by synthesizing a bare node and delegating to the very dispatcher that emits the guards — disclosed E504/E506 for a boundary that traps, and State.put(v) had been doing the same since #1203. Both now take the bare arm's rule on the same key (op.parent_effect), so the two spellings of one operation record identical statuses. The review of that fix found the arm had been hand-written as a refined-then-@Nat chain with no widening branch at all, so State.put(@Nat.0) / Exn.throw(@Nat.0) into an @Int cell recorded no obligation whatever while codegen emitted the @Nat -> @Int widening guard on both spellings — a guard the obligation stream never mentioned, the mirror image of the claim-without-a-guard this issue started from. It now routes through the shared _obligate_binding_triple, so the three arms cannot drift apart again by omission. The triple itself then turned out to be missing the #820 INTERSECTION at these boundaries: its three arms are an elif chain, so a refinement OVER @Int claimed the value and the widening check never ran — and codegen mirrored that exactly, so both sides agreed to skip a check the UNREFINED spelling performs. A refinement predicate does not imply fit-in-i64, and { @Int | true } is satisfied by the negative a @Nat above i64.MAX reinterprets to, so adding a refinement WEAKENED the boundary: Exn<Int> fed u64.MAX trapped on the widening guard while Exn<{ @Int | true }> fed the same value returned -1. The widening obligation and its guard now ride beside the refined pair rather than being replaced by it, and the two spellings trap alike; a user-declared effect's operation and IO.sleep's @Nat formal stay the honest #754 unguarded class. Two diagnostic rationales (E504, E531) that listed the throw payload among the unguarded sites — false once the guard landed, and contradicting the spec sentences this change amends — no longer do. Reaching the predicate needed the payload's TYPE, which neither of a cell's two names carries: family renders the predicate and base strips it, so CellNames now carries the type expression its producer already held rather than parsing one back out of a mangled family name. The predicate lowering itself is injected into the translation context (set_refinement_guard_emitter), because the two halves of a §2.6.5 guard sit on opposite sides of that seam — which local at what width is the context's question, while the trap message, the contract-fail import and the E617/E618 diagnostics are the generator's. An unrefined payload's WAT is byte-identical to before: a differential over all 278 pre-existing corpus programs — every examples/ and tests/conformance/ program, compiled and verified on both trees — moves nothing, in emitted WAT or in the obligation and diagnostic streams.

• Spec §6.4.3 and KNOWN_ISSUES.md now name every unguarded @Nat narrowing site (release-PR review). §6.4.3 said two sites stay unguarded — a user-declared effect operation's argument and the generic-instantiated constructor field — and the #754 row said the value-position tuple component was "runtime-guarded at the function boundary". Measured, a tuple component at construction is a third: Tuple(float_to_int(x), 5) narrowing into a @Tuple<Nat, Int> records tier3_unguarded with an E504 that names the site (@Int value narrowing into a @Nat tuple component), and the emitted function carries no guard — at construction, in return position, or at a call argument alike. The only guard is the one the consumer emits when it destructures, so a tuple that is only returned or passed on is never checked. Both documents now say so; the behaviour is unchanged and the residual stays disclosed statically.

• json_parse accepts one domain, and both runtimes accept it (#1306). The reference host parsed with json.loads, whose default parse_constant admits NaN, Infinity and -Infinity; the browser gated with JSON.parse, which refuses them as RFC 8259 requires. So the two hosts disagreed about which call rejects a non-finite value: the browser at the parse with a handled Err, the reference host at json_stringify — and there as a raw Python traceback rather than a Vera error (#1302 below). Spec §9.7.1 now states the accepted domain instead of leaving each host to inherit its parser's: RFC 8259-valid text that decodes to finite numbers and strings of Unicode scalar values, everything else Err at the parse with the same message on every runtime. A non-finite number has two entry routes and the domain closes both. The constants are one; the other is a syntactically valid number that overflows — 1e999, -1e999, [1e999], {"a":1e309} — which both host parsers accept, decoding to an infinite JNumber that then died at json_stringify, the same divergent-refusal-point defect one syntax over. RFC 8259 §6 sets no limit on a number's range and says an implementation may set one; Vera's is the finite Float64 values, which is exactly what json_stringify can write back. The refusal covers the integer spelling too, and that half was reference-host-only: json.loads returns a Python int for a digit string with no fraction and no exponent, so 1 followed by 309 zeros never met a float range check — and then had to become an f64 at the WASM boundary, where float() raises. It died with int too large to convert to float where JSON.parse, which has no int/float split and sees an Infinity either way, returned the shared sentence. The integer bound is the double rounding boundary (2**1024 - 2**970) rather than sys.float_info.max, and compared in integer arithmetic: an integer larger than the largest finite double still rounds to it and both hosts accept it, so the obvious bound would have traded this divergence for its mirror image, and a bound implemented as float(value) would be the very overflow it is looking for. Underflow is not the same question and is not refused: 1e-999 decodes to 0, finite and in the domain, pinned as a control beside 1e308 and the largest representable double so a refusal cannot generalise from "unrepresentable magnitude" to "large". Both value-level exclusions — overflow and lone surrogate — are found by ONE document-order walk returning the sentence itself, so "whichever comes first names the refusal" is the rule rather than a precedence table the two hosts could implement differently. The domain is the parse-side counterpart of the canonical output form #1293 pinned — a non-finite number has no JSON representation in either direction — and with no entry route through json_parse, the output-side refusal is now reachable only from a JNumber a program constructed from nan() or infinity(). The reference host's parse_constant hook records rather than raises, and the refusal is decided after the parse completes. Raising on sight would have made it answer a different question from the browser's: Python's scanner calls the hook the moment it sees the token, so [Infinity_x] — malformed for a reason that has nothing to do with the constant — would have reported the non-finite sentence natively while the browser reported a syntax error. Recording and continuing asks what the browser asks, by substituting 0 for each bare constant and re-parsing: would this text be valid JSON if the constants were admitted? Only then is the constant the whole story, and only then do both hosts say the same sentence; text malformed for any other reason keeps its host-native syntax message, as every syntax error always has. The browser's scan also only considers a token where a value may begin — the start of the text, or after [, , or :. Without that it found NaN at offset 1 of -NaN, substituted, re-parsed -0 successfully and reported the shared sentence, where the reference host's parser never reaches the token at all and gives a syntax error. -NaN, [-NaN], +Infinity, infinity, nan, NaNx and -Infinityx are all pinned as host-native on both hosts. The parity battery pins all four probe inputs from the issue's table plus the container and multi-constant shapes, compares the whole Err message across hosts rather than which arm was taken, and runs beside controls the refusal must not disturb — "NaN" as an ordinary string value among them.

• A lone-surrogate escape is refused at the parse, on both runtimes (#1308). {"k":"a\ud800b"} is grammatically legal RFC 8259 whose decoded value is not a sequence of Unicode scalar values, and a Vera String is — so the value has no UTF-8 encoding and cannot cross the WASM boundary at all. Both host parsers accepted the text and the memory boundary decided what happened next, differently and by accident: the browser's TextEncoder substituted U+FFFD, so json_stringify printed {"k":"a�b"} with nothing to tell the caller the value had changed, while the reference host died inside _alloc_string with a raw UnicodeEncodeError. Neither is a value the program can handle. The refusal now happens where the decoded value is known and before anything is marshalled, with one sentence naming the code point in canonical \uXXXX form so both escape casings produce the same message. Keys are covered as well as values, at any nesting depth — the key position is the one the issue's own reproduction used. The check does not overshoot: a matched high-then-low pair denotes one astral scalar value and still parses, which the batteries pin with matched pairs in every position, two pairs adjacent, and a pair at the end of a string. The two hosts' scans differ in a way worth recording, because the same rule reads differently against the two representations of a decoded value — json.loads has already combined a well-formed escape pair into one astral code point, so a plain D800–DFFF range test is complete on the reference host, while a JS string is UTF-16 and its scan must consume pairs before judging anything lone. With this and #1306, md_parse is the only operation on the shared surface still diverging (§12.9.3).

• A host callback's failure is a Vera error, not a Python traceback (#1302). execute() converted an escaping exception into WasmTrapError only when its type name was Trap or WasmtimeError. A host import raising an ordinary Python exception — json_stringify refusing a non-finite JNumber, the case that surfaced it — is re-raised through wasmtime's trampoline and arrives as, say, a ValueError, so the branch was skipped entirely: no classification, no source-map resolution, and the captured stdout/stderr dropped as the exception unwound. Measured on a program printing "before" and then json_stringify(JNumber(nan())): 63 lines of stderr across 17 Python stack frames, none of them naming the user's .vera file — and in --json mode no envelope at all, so a machine consumer got nothing parseable. It is now one line: Error: json_stringify: NaN is not representable in JSON — RFC 8259 has no NaN or Infinity. Guard with float_is_nan / float_is_infinite before serialising. The refusal itself was always right and is an instruction (DESIGN principle 1); only its presentation was wrong. The conversion is keyed on the boundary rather than on the exception's type, which is what makes the fix general: the guarded region is the guest invocation and nothing else, so everything arriving there is either a wasmtime trap or a host callback that raised, and every compiler phase has already finished. The taxonomy gains a host_error kind, carried in the JSON envelope's trap_kind beside the captured stdout (per #522); its Fix paragraph is empty for the same reason contract_violation's is — the description already carries the specific instruction, and a canned paragraph beneath it would be noise. The original exception stays reachable as __cause__ for anyone debugging the binding itself, and VERA_DEBUG_HOST_ERRORS=1 re-raises it untouched so the Python frames are still one environment variable away (ENVIRONMENT.md). This closes the gap against the invariant already written on host_print in vera/codegen/api.py: a user-level program must never produce a Python traceback regardless of what it does.

• A type alias sharing a prelude ADT's name emits the alias target's width (#1309). Spec §8.4.1 makes the prelude's data types ordinary declarations a program names and shadows, and the checker resolves such a name the way vera/naming.py's _resolve_named documents — type parameter, primitive, alias, declared ADT. Codegen's _type_expr_to_wasm_type tested _adt_layouts (and Array / Map / Set / Decimal, none of which are primitives) before the alias table, so type Option = Int; emitted its parameter as the ADT's i32 pointer where the checker and verifier had both agreed it was an i64 — check-green, verify-green, dead at load with type mismatch: expected i64, found i32. The alias branch now sits where the checker puts it: after the primitives, ahead of every ADT and container branch. The issue predicted the disagreement would be silently wrong wherever the two widths coincide; measured across every built-in ADT name against every representation, that is not where the silence is. A matching width (Bool, Byte, Map, Set, Decimal, all i32) emits WAT byte-identical to the same program under a fresh alias name — inert. The silent cases are the pair types, whose widths differ: an i32_pair is two words, the ADT branch's single i32 dropped the length, and nothing trapped — type Option = String; returned two junk bytes for string_concat("ab", "ab") and type Option = Array<Int>; reported length 0 for a three-element array, both at exit 0. Of the 16 built-in ADT and container names, 14 now compile and run correctly where 1 did before. Json and HtmlNode still fail, in a prelude body (json_get, html_attr) rather than the user's, because those bodies render their own parameters against the flat alias map a main-file shadow pollutes — an alias-env scoping defect (#1316) this branch-order fix does not reach. It does, however, MOVE that failure: the reorder flips 17 prelude json_* signatures from (param $p0 i32) to (param $p0 i64), reverses the mismatch the loader reports (expected i64, found i32 becomes expected i32, found i64), shifts its offset, and costs html_attr one shadow-stack push. Same defect, same frame, later point — not, as an earlier draft of this entry claimed, an identical failure. A generated battery pins every name in the live built-in ADT registry against every representation class, comparing the emitted twice signature to a fresh-name control, so a reintroduced ordering cannot hide behind matching widths.

• A match on a String or Array<T> scrutinee compiles (#1305). _translate_match saved the scrutinee into one local at its inferred WAT type, and a pair-represented scrutinee infers i32_pair — the internal two-word spelling, not a value type — so the module carried (local $l1 i32_pair) and never assembled. The scrutinee and any binding pattern over it now take two consecutive i32 locals, the same (ptr, len) convention parameters and constructor fields already use. Programs as ordinary as match @String.0 { @String -> string_length(@String.0) } and match @Array<Int>.0 { @Array<Int> -> array_length(@Array<Int>.0) } were check-green and failed vera compile at the branch point; both run now. The issue reached this through json_keys and framed it as an Option<Array<String>> payload binder, which measurement does not support: json_keys returns Array<String> (see vera/environment.py and the prelude body), so its result was never a binder problem and array_length(json_keys(j)) compiled and ran throughout — the trigger is the scrutinee's representation, with nothing JSON-specific about it. The issue's own repro additionally matches Some / None against that array; a pair carries no constructor tag, so codegen now refuses that arm with an E602 naming it, at the pattern's own location, instead of emitting a local that stops the whole module from assembling. That the checker accepts such a match over a constructor-less container ADT at all is filed separately as #1315.

• A Future-named type alias no longer makes an array return print as text. _return_type_is_string — which decides whether vera run decodes a function's (ptr, len) result as UTF-8 — tested the representation-transparent Future<T> strip before the alias table, and Future is an ADT name rather than one of vera.types.PRIMITIVES, so an alias of that name shadows it. Under type Future<T> = Array<T>; a @Future<String> return was therefore classified a string while the width derivation resolved the alias and lowered an Array<String>, and the array's backing bytes were decoded as text: two NULs where the same program under a non-ADT alias name printed the pointer. This is the third consumer of the branch-order defect #1309 fixed in _type_expr_to_wasm_type, found by review on the PR rather than by the original issue, and it misclassifies identically at that PR's branch point — pre-existing, not introduced by the reorder. String keeps its place ahead of the alias branch, being the one primitive involved, and the #841/#1047 transparent-Future decode and PR #1041's alias-to-Future shape are held by over-correction controls.

• The ch09_json conformance entry cites the section that exists. Its manifest spec_ref read Section 9.4.4, a section Chapter 9 does not have — the chapter's 9.4 runs to 9.4.3 Map<K, V> and Json is 9.7.1.

• The Vera-level type namers join over a conditional instead of reading one branch (#1286). #1276 fixed the WAT result-type deciders to take the first branch that yields a type; their Vera-level siblings kept the one-branch read — InferenceMixin._infer_vera_type (the WASM call-rewrite consultor) read then_branch only and arms[0] only, and Monomorphizer._infer_vera_type_name (the instantiation-discovery consultor) read then_branch only and had no MatchExpr arm at all. A branch whose every path throws names no type, so reading only that branch answered "unknown" for the whole expression, and the issue's latency estimate was wrong in the program's favour: the shape is constructible, and it is loud in two different ways from check-green source. As an array-literal element ([if false then { throw(true) } else { 42 }, 7], and the match and String spellings of the same position) the unknown element type raised CodegenSkip, so a declared public fn main — vera check-green and vera verify-green at 2 Tier 1 — was absent from the compiled exports behind an [E602] note. As a generic argument (idg(if false then { throw(true) } else { 42 }), verify-green at 4 Tier 1) the type variable bound nothing and the clone fell to the phantom-var default: the module carried idg$Bool, an i32 clone, reached with an i64 argument, and failed to load with Invalid input WebAssembly code at offset 73: type mismatch: expected i32, found i64. The same reading through a constructor field mis-instantiated the unboxing clone the other way round (expected i64, found i32). The repair lands on both consultors together because the match case was broken in both directions: with every arm completing and nothing diverging, the rewrite named idg$Int from arm 0 while discovery, having no arm for MatchExpr, named the phantom default, and the caller was dropped on a dangling target — the clone-name agreement contract (#772) makes the pair, not either function, the unit of repair. All 291 pre-existing corpus programs (examples/ plus tests/conformance/, recursive) emit byte-identical WAT, since the join only changes an answer that was previously unknown; ch02_generic_arg_branch_join promotes the witness into the conformance suite at level run. The review round closed the same divergence in two further shapes, both of them the one gap — the discovery consultor must stay structurally parallel to the rewrite one, arm for arm. It had no Block arm, and the transformer leaves a braced match-arm body AS a Block, so idg(match … { Some(@Int) -> { let @Int = @Int.0 + 1; @Int.0 }, None -> throw(true) }) named nothing on the discovery side and idg$Int on the rewrite side: a dangling target that dropped main from check-green source. A braced if branch whose tail is itself braced does the same, and so does a handle in argument position, which likewise had no arm. An IndexExpr argument is measured to dangle identically and is deliberately left for its own change (#1327): the rewrite's arm resolves chained indexing, aliases and Future payloads against codegen tables the monomorphizer does not have, so a partial mirror would replace a shape where both consultors answer "unknown" with one where they disagree.

• A GitHub Release body that would exceed the 125,000-character limit is condensed instead of failing (#1288). release.yml's Tag and create GitHub Release step 422'd on v0.1.10, whose CHANGELOG section extracts to 147,918 characters, and it failed after PyPI had accepted the immutable archives and after the tag was cut — the one point in the pipeline where a step must not fail. scripts/release.py notes is now total: within budget it publishes the section verbatim, and past it, it regenerates the shape the v0.1.10 release was completed by hand with — the section's ### subsection headers, one condensed line per bullet carrying its lead-in and its last issue or pull-request reference, and a link to the canonical section in the CHANGELOG at the tag. Run against v0.1.10's section the generated index reproduces the released body's 73 index lines byte for byte. In the pathological case where even the index overflows it is truncated and says so, so the builder cannot be the thing that fails.

• Four production-level divergences between spec Chapter 10 and the parser are closed (#1290). Typed holes have been in grammar.lark since 2026-03-30 and appeared nowhere in the chapter: 10.2 now declares HOLE and primary_expr carries the alternative, so the chapter's expression grammar is the parser's. 10.2's BLOCK_COMMENT published a non-nesting regex, contradicting 1.3 ("They nest") and the implementation, which counts depth in vera/lexical.py because a regular expression cannot; it is now a nesting production with that fact recorded beside it. The other two the new body comparison found: slot_ref and result_ref admitted an arbitrary type_expr, where the parser accepts only UPPER_IDENT type_args? — a refinement-typed slot reference is a syntax error, and the published grammar said it was legal; and effect_list carried a second alternative ambiguous with the one beside it, effect_ref already admitting a bare UPPER_IDENT, the same redundancy #1279 removed from statement.

• README's project-status line has every count gated, not just its test count. The check_readme helper returned silently when a pattern matched nothing, and four of its five patterns matched no README text at all — so the conformance count sitting beside the gated test count drifted through two rebases unseen. The line's four countable figures — tests, conformance programs, examples and spec chapters — are now read from that line alone, and a figure that has gone missing is an error rather than a skip.

• A user-defined fn get / fn put is no longer hijacked by an enclosing handler (#1284). Three sites answered "does this get mean the user's declaration or the effect operation?" independently. The checker answers user-fn-first — _check_call_with_args looks a bare name up as a function before it looks it up as an operation, so a declaration named get owns every bare get(...) in its scope, which an arity or argument-type error at such a call site proves by reporting the user's signature (E201/E202). Codegen answered twice more: the declared-effect row in vera/codegen/functions.py withheld the intrinsic when _fn_sigs already owned the name, and the handler expression in vera/wasm/calls_handlers.py installed get/put unconditionally. From vera check-green source that produced, depending on the nesting shape, a silently wrong value (nat_to_int(get(3)) under handle[State<Int>](@Int = 5) returned the cell's 5 for the function's 4, and the argument was not even emitted), a module WASM validation rejects (a @Bool-returning user get took state_get_Int's i64 into an i32 position; different-family nesting took the enclosing cell's getter at the wrong width), or a spurious [E602] in which the #1233 unaddressable-cell gate refused main outright, naming "a bare or qualified State operation get" the program never contained. The repair is one predicate, vera.slots.bare_call_denotes_user_fn, stating the checker's rule once and consumed by the bare-call dispatch in vera/wasm/calls.py (which now gates the clause-inline registry, the host-cell intrinsics and the addressability gate together), by the three bare-FnCall result-type inference sites, and by the monomorphizer's discovery walk — each passing its own name table, so the sites cannot answer differently about the table they share. Gating the dispatch rather than the registries is what makes it correct rather than merely consistent: the registries record which cell an op name reaches, which is true whatever the program's declarations are called, and withholding an entry answered both questions with one table. That is why the gate-only fix measured during PR #1283's review turned the loud skip into a differently-broken module, and why it also cost the qualified spelling its cell — State.put(5) in a function that also declares fn put compiled to call $vera.put and failed to link, which now lowers to the intrinsic the checker always meant. Discovery's MonoContext.fn_names moves to the same lookup-time question, so a get(()) fixing a generic's type variable under a handler names the clone the rewrite emits. All 256 conformance and example programs emit byte-identical WAT. The W002 async-commutativity warning was the same defect in the checker's own file and is corrected with them: _collect_expr_effects asked lookup_effect_op before the scoped function lookup — the last op-first consumer — so a user function named after an operation contributed the operation's parent effect to the commutativity analysis instead of its own declared row, wrong in both directions. A pure fn get, in a program containing no State at all, drew async argument performs State effects; a fn get that performs IO, under a row naming Http first, drew no warning, because the walk bound the name to Http.get, which is inside the commutative whitelist, and silently withheld the eager-evaluation warning the program is owed. Both are pinned with rename controls — the byte-identical program with the helper called gett / fetch was correct throughout — beside a control that an unshadowed bare get(()) under a State<Int> row still warns, so the fix cannot degenerate into never reporting State. The walk's comment claiming it resolves "like the call checker above" is now true. One caveat the predicate did not close on its own: codegen's name table was not scope-accurate, so a name the call site cannot see still answered "user-owned" there — a property of the table rather than of the rule, closed by #1299 below.

• A bare call is lowered against the names its call site can see (#1299). The #1284 ownership predicate is one rule read over two tables, and only one of them was a scope. The checker's is a lexical walk; codegen passed set(_fn_sigs.keys()) — a flat mirror of every symbol the whole compilation absorbed — so a bare get(()) the checker had resolved to a State operation was lowered as a call to a declaration the body cannot name. Four source shapes reach it, all vera check-green and all one defect: an imported module's private fn get (invisible, but still compiled in because the module's own bodies call it), a public one a selective import excludes, a where helper of a forall<T> parent (which keeps a bare _fn_sigs key beside its clone-qualified one where a non-generic parent's helper does not), and the ability operation show, which E151 does not reserve and which reaches the same table through the intrinsic gate rather than the operation one. How it lands is a property of the widths, not of the route: where the invisible declaration and the cell share a WAT type the module loads and returns the wrong value (7007 where the cell holds 42007), where they differ it fails to load (type mismatch: expected i64, found i32), and the generic-where route is always loud — the bare key exists in the signature table while no bare symbol is emitted, so the call dies at WAT assembly on unknown func: failed to find name $get with no E-code. The repair splits the two questions the one set was answering. _known_fns keeps the flat registry for _translate_call's guard rail, which asks whether a resolved target — already mono-mangled, already mod$… rerouted — has an implementation, and is flat by nature. A new _scoped_fns carries the names visible in the compiling declaration's lexical scope, and that is what the ownership predicate reads: its namespace's own declarations plus the public, in-filter names of the imports that namespace makes (spec §8.6.4 — imports are never inherited, so a transitively-reached module contributes nothing to the entry program), the prelude, and the where helpers of every enclosing function. Module scope alone would not have closed the third route: a generic's helper is in the module and still is not in a sibling's scope. The narrowing is a strict subset of the registry by construction — every $-bearing key is admitted unconditionally, since $ cannot occur in a Vera identifier and a mangled name is never what a bare source call spells — so it can only withdraw a name the flat table wrongly claimed.

  Three consumers read that question, not one, and the third is reached by wrapping the same call in a generic. Instantiation discovery (MonoContext.fn_names) types a bare call to NAME the clone, and its table is program-wide by nature — the guard rail needs every symbol in it — so idg(get(())) beside an invisible fn get(@Unit -> @Bool) discovered idg<Bool> where the checker had typed the State<Int> cell. Discovery now enters the namespace of the declaration it is walking (Monomorphizer.namespace_scope, accumulating each function's own where helpers as it descends, exactly as it already accumulates forall binders), and both sides enter it at all ten walks between them — six on codegen's side, four on the verifier's — from the same shared derivation, so narrowing one and not the other would leave a clone verified that nobody emits. The tenth is the one worth naming: collect_generic_helper_instances, the leaf under a generic's where family, is driven directly by both, so leaving it unscoped left them agreeing while both read the flat table — and two sides being wrong together is exactly what a differential cannot see. It is pinned against the checker's answer instead, and an instrumented audit over the corpus reports zero entries into the scoped region with no scope entered. Behind them the WASM call-rewrite's clone-naming override (_declared_return_clone_name, which beats the general inference for #899's benefit) read the same flat return-type registry and is gated on the same predicate. Depending on the widths, the shapes landed as a load failure (expected i32, found i64), a live clone of the wrong signedness reached by a negative cell, or — with discovery corrected and the override not — an [E602] drop of the caller.

  All 258 pre-existing conformance and example programs emit byte-identical WAT, and all three gates now have conformance coverage: reverting any one of them turns the suite red.

• E608 no longer refuses two modules' provably distinct generics (#1281). The flat-namespace collision rail exists because Pass 2.5 emits every imported function under one WASM name — but a generic emits nothing under its bare name, and since #1274 its clones live in a namespace chosen per owner: gen$Bool for a generic that owns the importer's bare name, mod$<path>$gen$Bool for one that does not. A diamond where base declares a public forall<T> fn gen and mid1 a private one occupies two different namespaces and was refused outright with Function 'gen' is defined in both imported module 'mid1' and 'base', while vera verify returned rc=0 on the same program — a loud verify-vs-compile disagreement. The rail now reads the same ownership classification the clone namespace does, and fires only when the pair really can collide: when either declaration is not a top-level generic (a non-generic is emitted under the bare $name), when both own the bare name, or when some namespace can name both — a module importing two dependencies that each export gen would resolve its own bare call to one of them, and spec §8.5 now refuses the name outright rather than ordering the two imports, so that shape keeps its refusal here as the backstop behind the check-phase refusal described below (#1304). The registration moved with the message, as defence in depth: a qualified-only generic no longer injects a bare _fn_sigs or _fn_ret_type_exprs entry at all. Those two registries are read per name by consumers the clone classification says nothing about — MonoContext.fn_names, the #1207 shadow guard, and the WASM call-rewrite's return-type lookup — where first-module-wins would make the answer depend on registration order. What actually closes that shape is the #1299 scope narrowing above, which reaches the same consultors through the call site: reverting both withholdings leaves every suite and all 224 conformance programs green. They are kept, and pinned structurally on the tables they act on with one cell each, because nothing but those four consumers' current internals stops any of them from picking a winner.

• A module's data type no longer empties a prelude one out of every other namespace, and the shape that silently dropped functions is now an error (#1277). Codegen keeps ONE flat _adt_layouts map while the checker gives every namespace the prelude's data types from the start, and the two halves of that gap failed differently. Membership: _adt_members_in_scope recovered global infrastructure by SUBTRACTING what the namespaces declare from the registered layouts, which is sound only while "declared by a namespace" and "global infrastructure" are disjoint — and §8.4.1 makes them overlap on purpose, since the prelude's data types are ordinary public declarations a program may name and shadow. So one file's data Json removed Json from the member set of every OTHER namespace, including the entry program's, while the checker's TypeEnv carried it in all of them; measured as a straight disagreement, Json a data type in a module's namespace for the checker and not for codegen. The Pass-0.5 built-in snapshot unioned in as a floor could not protect the four demand-injected prelude ADTs, because it is taken before Pass 1.2 injects them — the same asymmetry #1253 fixed, one layer down. The floor is now stated positively rather than recovered by elimination: vera.prelude.prelude_adt_names() parses the prelude's own data blocks with the same parser inject_prelude uses, so a new prelude ADT joins the set by being written, and a differential holds the two against each other; the cached prelude_data_decls() behind it hands back a read-only mapping, since one cached object is shared by every caller in the process. Scoping the subtraction per namespace instead — the other direction the issue left open — is refuted by tests/test_adt_membership_scope_1253.py, which it re-opens: a sibling module's ADT would become infrastructure for every namespace but its own. Contention: where a MODULE declares one of the prelude's data type names with a DIFFERENT SHAPE and the prelude is also compiling its own, the two contend for the one layout slot and the module's wins. The prelude's ADT was then never registered, its own combinators hit unknown constructor (an [E602] inside <prelude>), and every user function touching the type was dropped behind an [E620] cascade — all of it reported as WARNINGS, so a vera check-green program compiled with exit 0 to a module with a function silently missing from its exports, and nothing named the declaration that caused it. That is now E621, an error located at the module's declaration in the module's own file, refused by the same Pass-1.9 severity gate E608/E609/E610 use. It covers all eight of the prelude's data types, which required reading the DECLARATIONS rather than the registered layouts: the layout harvest skips a built-in name outright, because the throwaway registrar holds Option, Result, Ordering and UrlParts for every module whether it declares them or not, so a layout-keyed rail saw data Json and never data Option. The two halves differ only in when the prelude is present — the demand-injected four not until the entry program uses them, the always-injected four in every program — so a differently-shaped module data Ordering contends unconditionally, which upgrades that shape from an [E602]/[E620] cascade to one instruction. What decides contention is the two declarations' SHAPES: the same constructors, in the same order (the tag is the position), with the same field types, type parameters compared positionally — and each declaration's field types are resolved through the alias maps of the namespace it was WRITTEN in, the module's own for the module's declaration and none at all for the prelude's. Both halves of that are load-bearing. A module that restates the prelude's type through its own alias (type Payload = String;) is still a restatement, and comparing raw spellings refused it. Resolving the prelude's spelling through a module's aliases would go wrong the other way: type Array<T> = Int; in a module makes its JArray(Array<Json>) an Int field, and with both sides resolved the two keys collapse — which is how that program compiles today, with the module's layout in the slot, the entry's json_array_length reading it, and no diagnostic at all. A module that restates the prelude's type shares the one layout — measured legal for all eight, and kept legal, which is what stops the rail from becoming the reservation §8.4.1 forbids. That is not a hypothetical: examples/vera/collections.vera declares public data Option<T> { None, Some(T) } and examples/modules.vera imports it, so a rail that fired on the name alone refuses a shipped example — vera compile on examples/modules.vera returns E621 under that mutation, which scripts/check_e602_clean.py catches as a COMPILE_ERROR (measured; check_examples.py does not, running only check and verify). The rail's first form refused four of the synthetic restatements. Every declaring module is asked, not the first: a library that restates the prelude's Ordering otherwise answered for a sibling declaring a different one, so with the restating module imported first the sibling's contention went unseen — check-green, exit 0, the caller silently dropped — and the reverse import order caught it. An order-dependent rail is not a rail, and the battery now carries both orders. The module-versus-module pair for a name the prelude does NOT provide stays E609's, which a control pins. The acceptance battery is a parameterized test over all eight names in both shapes plus the restatement control, asserting that no cell reports [E602]/[E620] and that no zero-exit compile is missing a function, so the four-of-eight coverage the rail started with cannot return silently; ch08_module_prelude_adt_contention_rejected pins the same refusal at conformance level, paired with the positive that imports the same module and never names the type. The conformance manifest gained an expected_error_stage key for it ("check", the default, or "compile"): a compile-stage negative asserts that the program type-checks CLEANLY and is then refused by vera compile with the declared code, which is the property a codegen-phase diagnostic exists for and which the check-only negative path could not express. Reserving the prelude's names is not the fix and is not done: §8.4.1 forbids it.

• The prelude's declaration-index block no longer depends on what the main file declares (#1287). _stamp_decl_order guarded its PRELUDE write on _decl_order, the ACTIVE (main-file) namespace — but _prelude_decl_order is not a namespace: _module_alias_scope builds every module's index space as {**prelude, **module_own}, so it is the base layer under all of them and its contents are a fact about what inject_prelude laid down. A main-file type Option = Int is accepted (§8.4.1 again) and, being an alias rather than a data, does not suppress the prelude's own data Option<T>, so the guard fired on the prelude stamp: Option was left out of the block entirely, and every later prelude declaration shifted one place earlier because the skipped stamp never advanced the counter. Inside a module namespace the prelude's Option then reached AliasEnv.data_types at _BUILTIN_DECL_INDEX — below _PRELUDE_DECL_BASE, so ordered ahead of every other prelude declaration rather than among them — which is exactly the cross-namespace leak _decl_order and _module_decl_order were split apart to prevent. Latent at emission: that map changes a rendering only for Decimal and the single REMOVED_ALIASES entry Float, and no prelude ADT is either, so no WAT moves; the defect is the wrong value reaching the consumer. The prelude write is now unconditional and the ACTIVE space still takes the main file's stamp, so the shadow keeps winning its own namespace. Pinned as an invariance — the same program with and without the shadowing alias must stamp an identical prelude block — with the main-namespace control that a fix stamping _decl_order unconditionally would fail.

• new(State<T>) reads the cell its contract names (#1285). old(State<T>) has been keyed on the resolved cell family since #1205/#1209; new(State<T>) read the name-keyed _effect_ops["get"], which holds whichever State the effect row registered first. Under a single-State row the two keyings coincide, which is why the corpus agreed; under a multi-State row the two sides of one ensures clause read different cells. effects(<State<Int>, State<Bool>>) with ensures(new(State<Bool>) == false) was check-green and verify-green, emitted state_get_Int's i64 into the Bool comparison's i32.eq, and died at load with wasmtime's raw type mismatch: expected i32, found i64. The type mismatch is the symptom rather than the defect: where both cells share a machine width — State<Int> beside State<Nat> — the module loaded and answered about the other cell, so ensures(new(State<Nat>) == old(State<Nat>)) on a function that writes neither was refuted at runtime on a contract the verifier had discharged. Codegen now carries a family→getter registry populated at the declared-row registration site from the per-family CellNames it already computes, and _translate_new_expr keys on _state_effect_family exactly as _translate_old_expr does. A bare get(()) names no family and so is right to keep reading the name-keyed registry, source-order-first-wins; a contract names one and must not.

• decimal_from_string ignores one stated whitespace set, and a leading byte-order mark survives the browser boundary (#856 review). §9.7.2 said the grammar is applied "after ignoring surrounding whitespace" and that the accepted domain is defined by the grammar "rather than inherited from whatever the host library parses" — but the whitespace half was inherited, from str.strip on the reference host and String.prototype.trim in the browser, and those two sets differ in both directions. Measured through identical module bytes: U+001C–U+001F and U+0085 around a decimal were Some natively and None in the browser, U+FEFF was None natively and Some in the browser, and U+00A0 with the Unicode space separators were accepted by both for reasons neither specification names. §9.7.2 now states the set, and it is the one the language already had: the six code points is_whitespace names. The U+FEFF half turned out not to be about trimming at all — new TextDecoder('utf-8') defaults to ignoreBOM: false, whose meaning is the reverse of its name, so the browser's readString removed a byte-order mark from the front of every string crossing into a host binding. IO.print("\u{FEFF}x") printed x, json_parse accepted a BOM-prefixed document the reference host refuses, and md_parse dropped the character from its text. The decoder now passes it through, matching safe_utf8_decode, which never stripped one. The exponent bound |exp| <= 999999 is unchanged in force and in value; only its keyword is, from a lowercase "must" to the RFC 2119 MUST it was always enforced as.

• Three constructed MdBlock values the renderer could not write back (#1294 review). All three are reachable only from a value a program builds, which is why a round-trip corpus could not find them: the parser never produces the shape that breaks. A code span whose content starts and ends with a space was eaten by the parser's own strip — _parse_inlines removes one such pair whenever the fenced text is two characters or longer, so MdCode(" x ") rendered ` x ` and read back as MdCode("x"), and MdCode(" x ") rendered to the same bytes as MdCode("`x`"), which made the loss unrecoverable even by guessing. The renderer now pads those spans the same way it already padded backtick-bounded ones, so the strip removes the pad instead of the content; spec §9.7.3 loses one of its three documented round-trip losses as a result. A list item with no blocks was dropped outright, though - is exactly what the parser reads back as one — and in an ordered list dropping it silently renumbered every item after it. It now renders as its marker plus the space both item patterns require (a bare - is a paragraph). A container that renders to nothing — a list with no items, a table with no rows — still drew the document's blank-line separator, so MdDocument([MdList([]), p]) rendered "\nafter": a blank line standing for an absent block, which the next parse cannot attribute to anything and which cost the render its fixed-point property. A zero-line child now contributes no separator, in MdBlockQuote as well as MdDocument. Both runtimes move together and the two spec rules are restated; the change is held to a zero-regression bar over the 6,078-case Markdown corpus — ADT agreement, render agreement and each host's fixed-point property all show no ok→broken transition. §9.7.3's two normative sentences are stated at the strength the batteries enforce while the section is open: the fixed point is unconditional, so it reads MUST with no carve-out, and the round-trip property reads MUST with an exception clause that now names both families outside it — the two unwriteable code spans, and a container with nothing in it to write, since an MdList with no items renders to no lines and so re-parses to no block. The earlier clause named only the code spans, which made the property false for the empty containers it did not mention. Each rule cluster also gains a compiled, contract-verified example, because every one of them is reachable only from a constructed value and the section had no executable form of that.

• A block quote separates and keeps its children, on both runtimes (#1294 review). The reference renderer emitted no separator between a blockquote's children, so MdBlockQuote([Para, Para]) — the shape md_parse builds from > a\n>\n> b — rendered as two adjacent quoted lines and read back as one paragraph. Structure lost silently, on both hosts, and the round-trip property spec §9.7.3 states did not hold for it. A quote with no children was the same defect one size down: it rendered as no lines at all, so a > in a document vanished on the round trip and left the enclosing separator dangling (---\n> came back as ---). Both arms now mirror MdDocument's: a bare > between children, and > for an empty quote. Two more mirrors land with them. The browser parser's blockquote reader required > with the space where the reference accepts ^>\s?, and had no lazy-continuation branch at all, so >no space parsed as literal text and > a\nb pushed the second line out of the quote — both inside #1294's stated scope and neither closed by the renderer fix. And a code span is now fenced with one backtick more than its longest internal run rather than a fixed two, padded only when the content starts or ends with a backtick: the old rule was right for one backtick and wrong for two, since `` a``b `` closes on the run inside the content. The browser's inline parser scanned for the next single backtick rather than a run of equal length, so it could not read that back either; it now counts runs like the reference. Spec §9.7.3 states all four rules. Measured on a 1,471-input adversarial corpus: md_render is a fixed point on every input on both hosts (from 65 and 54 unstable), and cross-host render divergence falls from 489 inputs to 34; on 4,850 sections of the project's own documentation, render divergence falls from 40 to 11 and the reference round trip is a fixed point everywhere. The remaining md_parse divergences are a separate tracked bug, listed in KNOWN_ISSUES.md with a measured class-by-class breakdown. Alongside them: the browser's json_stringify no longer falls back to "null" when JSON.stringify returns undefined — unreachable from readJson, but the same silent substitution #1293 removed one layer up, and an unreachable branch is where a silent wrong answer survives; and the non-finite parity test now asserts the whole shared sentence, taken from the reference implementation so the browser's hand-copied duplicate is held against the original, plus that neither host printed anything before failing.

• The browser runtime's md_render mirrors the reference renderer, holds the round-trip property, and is a fixed point (#1294). It preserved a paragraph's internal soft line breaks and did not re-apply a container's prefix (> , list-item indent) on output, so it broke the round-trip property spec §9.7.3 states for md_render and, with it, §12.9.3's identical-results requirement. The scope was any multi-line paragraph, not the list lazy continuation first observed, and the render was not stable: re-rendering its own output moved content out of its container (> a b → > a\nb → > a\n\nb, where b is no longer quoted), and on a blockquote wrapping a heading and a fenced block the second render fragmented the fence into three and lifted the code clean out of the quote, past recovery by any subsequent parse. Two defects underlay it, in two different phases, and both are fixed because neither alone closes the issue. The parser joined a paragraph's lines with \n where the reference parser joins with a space: §9.7.3's design note excludes hard and soft line breaks from the ADT — "collapsed into paragraph text" — so a break that survives into MdText is one no renderer can tell from text the author wrote, and md_parse itself therefore returned different ADTs on the two hosts. The renderer returned one string and threaded the container prefix down as an argument, which a container could only apply to the first line of each child; it is now line-based, mirroring _render_block in vera/markdown.py, so every caller re-applies its own prefix to every line it receives — the property that makes the render a fixed point. A third mirror lands with them: a code span containing a backtick now renders with the longer … fence, which the reference renderer has always done and neither parser can produce, so it was reachable only from a constructed ADT. Spec §9.7.3 states both rules rather than leaving them as an implementation detail two hosts had to rediscover. tests/test_browser.py's two pinned-divergence assertions collapse into parity assertions, and the battery around them is now three-layered — cross-host equality, the expected string, and stability under re-render — because equality alone passes two hosts that agree on a wrong answer and a single render passes a renderer that drifts on the second pass. The §9.7.3 round-trip property is exercised over a nineteen-case corpus: the eight the reference renderer is already held to in tests/test_markdown.py, every one of which is single-line or fence-only and therefore blind to exactly this defect, plus the container and multi-line shapes the bug was about. Three further cases render ADTs a Vera program built rather than parsed, since the parser only reaches the shapes it happens to produce.

• json_stringify has one canonical output form, and both runtimes produce it (#1293). The two hosts disagreed: the reference runtime called json.dumps(value, ensure_ascii=False, allow_nan=False) — ", " / ": " separators, and since read_json hands it Python floats, a JNumber parsed from 1 re-rendered as 1.0 — where the browser called bare JSON.stringify. Spec §12.9.3 requires every non-IO operation to produce identical results in both runtimes, so the divergence itself was the defect, and §9.7.1 now states the resolution: the compact form, , and : with no padding, object members in insertion order, strings escaped with non-ASCII emitted literally, and numbers rendered by ECMAScript's Number::toString. The browser already emitted that form; the reference host moved to it. Measuring the gap first showed it was wider than the issue's two axes — json.dumps renders floats with repr, hard-wired inside json.encoder and not reachable through any separator setting, and repr disagrees with Number::toString on four independent boundaries, not one: the fractional part of an integral value (1.0 vs 1), the threshold for exponential notation at each end of the range (1e+16 vs 10000000000000000, 1e-06 vs 0.000001), and the spelling of the exponent itself (1e-07 vs 1e-7), plus negative zero (-0.0 vs 0). Fixing only the reported symptom would have left the other three diverging, so vera/wasm/json_serde.py gains format_json_number, an implementation of ECMA-262 §6.1.6.1.20 that takes its shortest-round-trip digits from repr and recomputes only their placement; string escaping is still delegated to json.dumps, which already agrees with JSON.stringify byte for byte. The claim "matches ECMAScript" is checked differentially against the real JSON.stringify over 2,000 doubles drawn from raw bit patterns, not only against a hand-written boundary table, since a table proves the cases its author thought of and those are the cases the code was written to handle. Alongside the formatting, the third asymmetry the issue folds in is closed in the other direction: a JNumber holding NaN or an infinity now fails on both hosts with the same sentence, where the browser used to emit null — swapping a value RFC 8259 cannot carry for a different, perfectly valid one that no consumer could tell from a genuine JNull. The eleven Node-only tag assertions in tests/test_browser.py become full parity assertions, the two pinned-divergence strings collapse into single-truth ones, and the battery gains the number boundaries, a three-pass idempotence check on every case, and the two-sided failure assertion for non-finite values (it must raise and print nothing, so a host that emitted null before failing cannot read as a pass). Review of the change found the browser host breaking the insertion order clause of that same canonical form, which no test covered because every JSON object in the suite had alphabetically-ordered, non-numeric keys: vera/browser/runtime.mjs reached the WASM-side Map<String, Json> through ordinary JS objects on both sides of the boundary — JSON.parse returns one, writeJson enumerated it with Object.entries, readJson rebuilt one key by key — and an ordinary object cannot carry insertion order, because ES OrdinaryOwnPropertyKeys lists array-index keys first in ascending numeric order. {"2":1,"1":2} round-tripped to {"2":1,"1":2} natively and {"1":2,"2":1} in the browser. The same intermediate lost a field named __proto__ outright — assigning it runs Object.prototype's setter and creates no own property — so {"__proto__":{"a":1}} came back {}. Both are now carried in a JS Map from parse through serialization: json_parse keeps JSON.parse as the accept/reject decision (so the Err domain and its message are unchanged) and rebuilds the tree with an order-preserving re-scan that hands every leaf back to JSON.parse on its own slice, and json_stringify walks the result with a canonical emitter mirroring dumps_canonical rather than calling JSON.stringify, which does not know about Map. Both losses were silent, and both sat inside the property this entry claims to establish.