v0.2.5

Highlights

• Every name is resolved once. vera.binding gives every declaration of the entry file, each module and the prelude an identity and binds every call, data type, alias and constructor name to one declaration before any later stage asks; the checker, the verifier and code generation read that binding, and every declaration compiles under its own link name, in a namespace no function the compiler writes for itself can reach (#1694). Two modules' same-named data types are two types (breaking: a value of one meeting the other is E202 or E314), and a slot name's type argument keeps its refinement's predicate (breaking: two bindings that differ only in a predicate are two stacks).
• The prelude's names are reserved (breaking). A function or a where helper named after one of the prelude's 23 functions is refused with E151, and a data declaration, a type alias or a type parameter named after a prelude or built-in type with E158 (#1469). E608, E609, E610, E621 and E623 left with the mechanism that needed them.
• vera verify reconciles its runtime-check claims with the compiled module by default (breaking). It compiles the program in process and joins the obligations with the checks the module holds, as --reconcile did; --no-reconcile skips the join.
• A Map's or Set's String keys hash under a SipHash-1-3 key drawn for each instantiation (#1736), so keys chosen to collide no longer turn a trie into a list.
• A contract predicate is held to purity, whatever its function's effects clause names (breaking) (#1708): an effect operation inside a contract is E187.
• An if or a match that joins an @Int branch with a @Nat one is an @Int (#1756), so binding it into a @Nat position is obligated (breaking: E503 at the binding where the run trapped).
• A program generator writes whole Vera programs from a seed and feeds three nightly differentials: what checks compiles and loads with every public function exported; every obligation record has its guard and every guard its record; a Tier 1 proof meets no runtime violation on generated inputs. Its first 1,000 seeds found the join above.
• The tester reports as the source reads. vera test names a trial's arguments as the source does (#1757); --distrust attributes a trap through the reconciliation's relation (#1633) and runs the corpus at 1,000 trials a night.
• Forty-two run-level conformance programs run what their headers name (#1645).
• CI stands down where nothing it checks changed. A pull request that changes only the VS Code extension runs plan, lint, security and matrix-gate; the coverage floor is 94%; the mutation (diff) check is red for a defect and green for an unfinished run; the mutation lanes run without pytest's faulthandler (#1747); the nightly sweep tolerates a slice whose runner was lost (#1751); and test modules build their wasmtime engines on first use (#1745).

Added

• A program generator, and three differentials over what it writes, nightly. tests/program_generator.py writes a whole Vera program from a seed: up to three data declarations, up to six functions whose every slot reference is computed from the generator's own binding stack and whose contracts hold of every input their requires admits, and a main that prints each public function's value. tests/test_program_generator.py holds each program to vera check with no diagnostic, vera fmt's canonical form and a vera verify with no error and no timeout, and to three differentials: the module compiles with no E6xx diagnostic, exports exactly the public functions and runs each on the arguments the generator chose; vera/reconcile.py's join reports no mismatch outside the classes scripts/check_reconciliation.py's KNOWN names; and vera test --distrust reports no refuted proof, no trap it cannot attribute and no failing trial. A find outside the known classes is minimised and recorded with its seed, the minimal program and what the generator expected of it. .github/workflows/nightly-generator.yml runs 5,000 seeds a night at 14:17 UTC and files or updates one issue labelled generator-find when a night fails; every pull request runs ten pinned seeds, and a pull request that changes the generator runs 1,000.
  • Over the first 1,000 seeds (2,238 public functions, 2,114 of them tested and 2,056 proofs exercised in 28,529 trials), the known classes counted 1,516 mismatches of #1695's #1629 shapes in 707 programs, 792 of its #1557 shape in 480, 48 of #1598's in 40, and 3 verify refusals in 3 programs that #1525's checklist now names: a call whose argument constructs a data type its function names nowhere else loses the callee's postcondition.
  • The runs found one class of their own, #1756, which this release fixes: an if or a match joining an @Int branch with a @Nat branch was typed @Nat, so binding it into a @Nat slot recorded no narrowing; let @Nat = if @Bool.0 then { -1 } else { @Nat.0 }; passed vera verify, and the run's guard trapped on it.

Changed

• The prelude's names are reserved (#1469). The prelude is a module whose names no declaration may take, in the entry file or in any module, whatever the declaration's shape. Breaking: a function or a where helper named after one of the prelude's 23 functions (option_map, option_and_then, option_unwrap_or, result_map, result_unwrap_or, html_attr and the json_* accessors) is refused with E151, which exempted them before (#815); a data declaration, a type alias or a type parameter named after a prelude data type (Option, Result, Ordering, UrlParts, Json, HtmlNode, Request, Response), a built-in data type (MdBlock, MdInline) or a built-in type name (Array, Decimal, Future, Map, Set, Tuple) is refused with E158, which covered only a data declaration of a built-in type name. A constructor may still share a prelude constructor's name. A user json_get used to replace the prelude's inside json_get_string, so the program failed to load or returned a different value (#1495); an entry-file data Ordering { Lt, Same, Gt } beside compare passed check and code generation dropped main (#1496); a module's own data Json accepted a prelude Json value and read it through its own layout (#1560), and an entry file importing it could not name it (#1600); a type Decimal or type Array<T> alias beside a built-in value of that type built a module that fails to load (#1553); and a type parameter named Array dropped its caller at compile (#1556). To upgrade, rename the declaration and update its uses: examples/vera/collections.vera declared public data Option<T> { None, Some(T) } and now declares public data Maybe<T> { Nothing, Just(T) }, and examples/modules.vera imports Maybe. Four conformance programs that declared a prelude name are negative fixtures refused at check with E158 (ch08_alias_shadows_prelude_adt_name, ch08_prelude_adt_name_alias, ch08_module_prelude_adt_name, ch08_module_prelude_adt_contention_rejected), and the spec's blocks that show the prelude's own declarations are marked as the declarations the compiler injects. vera.prelude.reserved_function_names() and vera.prelude.reserved_type_names() are the one source of the set.
• A program's declarations and the compiler's own functions and exports are two namespaces (#1694). Every declaration's WebAssembly function is named $: followed by its link name ($:main, $:mod$util$helper for helper in module util;, $:f$where$h for a where helper, $:identity$Int for a clone), and no function the compiler writes for itself ($alloc, $gc_collect, a lifted closure's $anon_0, a derived $eq_Shape) has a : in its name, so a user function named alloc, gc_collect, anon_0 or eq_String beside a program that makes the compiler emit its own no longer fails to compile with a duplicate identifier (#1494), and under --target wasi-p2 a function named wasi_tbl, wasi_arena_ptr or cabi_realloc compiles instead of being refused as a reserved identifier. Breaking: the compiled module exports its runtime under names that start with vera., which no Vera identifier can spell: its linear memory as vera.memory, the allocator as vera.alloc, the GC globals as vera.heap_ptr, vera.gc_sp and vera.gc_stack_limit, and the wrapper registration as vera.register_wrapper (and the WASI 0.2 core module's adapter table, arena pointer and realloc as vera.wasi_tbl, vera.wasi_arena_ptr and vera.cabi_realloc), so a public function named alloc is exported as alloc beside the allocator. The browser runtime's getExports() lists the program's own functions and none of the runtime's, register_wrapper included. To upgrade, an embedder that read memory, alloc, heap_ptr, gc_sp, gc_stack_limit or register_wrapper from a compiled module's exports reads the vera.-prefixed name (instance.exports["vera.memory"]); a program's own exports keep their names. The vera compile --wat text and a backtrace wasmtime prints itself name a declaration's function with its : (Main!:handle); Vera's own trap reports name it as declared.
• Two modules' same-named data types are two types (#1694). The checker types a module's data type by its declaration, as code generation compiles it, so a module's type and another module's or the entry file's type of the same name never unify. Breaking: two modules that restate one layout under one name, with a value of one reaching code that expects the other (bone(aone(6)), with liba's aone(@Int -> @Shape) and libb's bone(@Shape -> @Int)), compiled since #1317 and are refused at check, with E202 for an argument or E314 for a pattern, by a message naming both owners (liba.Shape, libb.Shape). To upgrade, declare the type once, in one module, and import it in the other. The reverse moved too: an entry file that declares a type of a module type's name, and imports a function whose signature carries the module's type without calling it, was refused (E623) and compiles.
• A slot name's type argument keeps its refinement's predicate (#1674). A refinement in a type argument is rendered with its predicate, canonically, where it was rendered {@Int | ...}, so @Array<{ @Int | @Int.0 > 0 }> and @Array<{ @Int | @Int.0 < 0 }> are two slot names. Breaking: two bindings whose types differ only in such a predicate are two stacks, each counted from .0, where they were one, and a reference to one writes the predicate as the binding's type does (@Array<{ @Int | @Int.0 > 0 }>.0). To upgrade, a reference that reached the second of two such bindings as .1 reaches it as .0 of its own type; vera check --explain-slots prints each binding's slot name with its predicate.
• vera verify reconciles its runtime-check claims with the compiled module by default (breaking). It compiles the program in process, as vera compile does, and joins the obligations with the checks the module holds, as --reconcile did: a tier3 or timeout obligation no check answers is an E541 error, a check no obligation accounts for a W004 warning, and vera verify --json carries the reconciliation object. A program code generation refuses fails vera verify with that refusal; a program holding typed holes verifies as before, with a W005 warning that its runtime checks were not reconciled and "reconciliation": {"skipped": ...}. The text output ends with a Reconciliation: line when the program claims a runtime check. Of the 323 corpus programs and 444 documentation blocks, two newly fail vera verify: tests/conformance/ch02_adt_tuple_recursive.vera, with the E541 the reconciliation gate lists under #1695, which the conformance run accepts there and nowhere else, and the negative fixture tests/conformance/ch08_module_prelude_adt_contention_rejected.vera, which code generation refuses (E621); 44 more gain warnings, a W004 at 98 sites in 40 programs, each listed under its issue, and an E604 in 4 library modules. Upgrade: a program vera verify accepted and vera compile refuses now fails vera verify with the compile's error; vera verify --no-reconcile verifies without compiling, as the command did, and --reconcile is accepted as the default it names.
  • tests/pipeline.py's verify stays the verification stage, as vera verify --no-reconcile runs it, and verify(..., reconcile=True) is vera verify; tests/test_pipeline.py holds both to their commands over the corpus.
• The nightly stress workflow runs the distrust corpus at 1,000 trials per proved function (.github/workflows/nightly-stress.yml). The step runs once the stress tests have run, pass or fail, with a ten-minute stop; the pull request's suite runs 5 trials. At c923541 the corpus took 27.6 s of wall at 1,000 trials on four local workers (6.4 s at 5, 121 s at 3,000), and the step 1 min 44 s on the runner. A scheduled failure of either step files or comments on the stress-regression tracking issue, naming the step that failed.
• A pull request that changes only the VS Code extension's own files runs plan, lint, security and matrix-gate, and the other jobs stand down (scripts/ci_changes.py). The plan job asks whether every file the pull request changes from its merge base, a rename's old name included, is under editors/vscode/ and is the extension's code, manifests, lockfile or icon, which vscode-extension.yml builds and tests; the extension's grammar, which scripts/render_lists.py renders, and its README and CHANGELOG, which the documentation gate's coverage rule reads, are not. On inert=true, typecheck, eager-gc, browser-parity, wheel-preflight, dependency-audit, package-distribution and sbom are skipped by their if:, which reports success under each job's name, and the five shard cells skip their steps, since a matrix job skipped whole reports one check under its unexpanded name; every required check keeps its name. Of the 120 pull requests merged from 2 September to 21 October 2026, 6 changed only editors/vscode/package.json, editors/vscode/package-lock.json or both, five of them Dependabot's npm updates; no other change stands a job down, because the suite reads the documents and the workflows. tests/test_ci_changes.py reads the workflow as data: every required check reports on every pull-request event, the filtered jobs stand down on an inert pull request and run every step on any other, and a missing answer runs every job.
• The coverage job's floor is 94% (--cov-fail-under=94, where it was 80).
• scripts/check_changelog_updated.py takes the base it diffs against as its argument. Lint passes origin/<github.base_ref>, which is origin/main on every run ci.yml makes, since its pull requests target main, so no CI run's verdict changes. A base the argument names that git cannot find exits 2, and with no argument the gate resolves its base as before.
• Lint no longer repeats the suite's work. It ran scripts/check_examples.py, scripts/check_doc_examples.py and scripts/check_examples_run.py, whose work the suite does: the examples' check and verify (tests/test_verifier_contracts.py, and tests/test_pipeline.py, which holds each stage to its command); every gated document's Vera blocks and the coverage rule (tests/test_check_doc_examples.py), now with the vera run examples/... invocations each document names, which no test ran; and the examples' runs, in tests/test_check_examples_run.py's new TestRealExamples, the 36 examples RUN_SPECS names run in process and read by the gate's two signals. The scripts stay for local use, and tests/test_gate_placement.py matches the doc-example hook with a run of the whole suite.
• The eager-GC lane is one pytest run, pytest tests/test_conformance.py tests/test_check_examples_run.py::TestRealExamples -k run -n auto under VERA_EAGER_GC=1, where the examples ran through the script.
• Every context value in ci.yml reaches a shell through env:. Four run commands wrote one into their text: the shards' --shard, the test matrix's --matrix, the release-mode check's base and the JavaScript coverage report's directory. The shards' and the test matrix's pytest, which Windows runners take, run under shell: bash, since pwsh, a Windows runner's default shell, reads $SHARD as a PowerShell variable of its own, which is empty; tests/test_ci_changes.py holds every step a Windows runner takes that reads a variable to bash. tests/test_gate_placement.py reads a step's env: into its command, and accepts shell: bash beside the default bash -e.
• The mutation (diff) check is red for a defect and green for an unfinished run (scripts/mutate_diff.py). It exits 1 on a survivor, whatever stopped the run; 2 when the engine fails, mutmut reports a mutant of a function the lane did not map, or the lane itself fails; and 0 otherwise, where it exited 2 for every run its budget stopped: on #1753's final head the run took 2,410 s against its 2,400 s budget, and of 576 mutants killed 209, timed out 6 and left 361 not checked, none surviving, and the check was red. A run that its budget stops, or that leaves a mutant undecided (not checked, suspicious, segfault, interrupted), passes when no mutant survived and nothing failed, with the headline Incomplete: ... in the job summary and a ::warning:: annotation on the pull request; a failure of the engine or the mapping found after the budget ran out is red all the same. No other step of the workflow reads the exit status.

Removed

• E608, E609, E610, E621 and E623 (#1694). Code generation's name-collision errors: two imported modules' same-named function (E608), data type (E609) or constructor (E610), a module's data type beside the prelude's (E621), and the entry file's beside a module's (E623). Every declaration is compiled under its own link name, the prelude's names are reserved (E151, E158), and a value of one declaration's type that meets another's is a type mismatch at check, so nothing emits them, and vera errors no longer lists them.

Fixed

• vera test --distrust reads a trap through the reconciliation's relation, so a trap at a check whose record stands at another node is attributed (#1633). The tester joined the check a trap fired at to the verifier's record by exact span, so a refined parameter's guard (at the parameter's type, its record at the caller's argument), a destructure's or a pattern's binder guard (its record at the value it takes apart), a refined return's guard (its record at the body), an arm's guard (its record at the join) and a callee's requires check (its record at the call) joined nothing, and a false proof behind one read unattributed. _TrapIndex reads vera.reconcile.join's relation, every record with every check standing for it whatever its status (Reconciliation.answers), and the checks a function makes on entry (Reconciliation.entry), each of which stands, in a trial, for the calls written in the functions the trial's run reaches (Reconciliation.entry_calls): another caller's record is neither its proof nor its guard, and a reached call with no record, one whose precondition the verifier discharged, keeps a trap there unattributed; the exact-span reading, the return type's special case and the hand-written prologue test are gone. Over the 1,561 non-prelude checks the distrust corpus compiles at c923541, the relation joins 1,364 to a record, against 1,328 by span; the 197 it joins to none are 92 checks with no record at all (W004), 73 in imported bodies this run did not verify, and 32 requires checks whose calls' discharged preconditions the verifier does not record.
  • The join reads a decreases measure's evaluation on a tail call's arguments, which the verifier records at the call and code generation checks at the measure's own nodes before the return_call: SKILL.md's State loop helper reported its measure's @Nat.1 + 1 as an E541 under vera verify --reconcile, with the check in place.
• Forty-two run-level conformance programs run what their headers name (#1645). Each program's main reaches every function the program defines and calls every built-in its manifest features names, and prints, for each case, the value it computed, which the entry's expected_stdout pins. Eight programs had no main, so vera run executed their first public function alone; four had a main that called none of their tests or whose check could not fail; eighteen ran one case of several; three named in their header a feature the file did not contain (ch01_string_escapes now prints the character codes of \r, \0 and \u{0007} and the byte length of \u{00A0}, ch04_string_interpolation interpolates a Float64, and ch07_exn_param_alias throws and catches across alias depths); and nine had a check too weak to see a wrong value, such as ch05_capture_array_index, whose first case passed under an identity map and its second under a transpose, and which now prints each whole result. tests/test_conformance_run_reach.py holds the 42 to the first two rules, reading a call by the rule the corpus walks share (called_name): 86 cells, 46 of them red before the change. The distrust corpus (tests/test_distrust_corpus.py) runs 155 proved functions in 79 programs, where it ran 167 in 84: twelve of the old mains were pure functions the verifier proved, and their replacements print, under contracts vera test skips as trivial.
• Every name is resolved once, by the resolver pass (#1694). vera.binding gives every declaration of the entry file, each module and the prelude an identity and binds every call, data type, type alias and constructor name to one declaration, before any later stage asks; the checker resolves its calls, types and constructors by reading the binding, and code generation and the verifier compile and verify the linked program, every declaration under its link name, so no two stages read one name two ways. Each instance of the class:
  • Two same-named functions no namespace can name together compile and run: a selective import beside the other module's own f, a module declaring f over the f of a module it imports, and two modules' private helpers of one name were refused at compile with E608 (#1498).
  • A module generic called from another file at that file's own data Shape, where the module declares type Shape = Int;, compiled to a module that failed to load (#1519).
  • show() and hash() of a value whose type an imported signature names read the name through the importing file's type aliases, so an entry-file alias spelled like the imported type printed a wrong result (#1548).
  • A module generic's call to its own where helper compiled, in an importer, as a call to the module's same-named top-level generic, so an ensures proved for the helper failed at run time (#1581).
  • A user function's E602 is kept whatever its line: it was suppressed when its line fell inside a compiled prelude generic's line span, and the function was dropped with no diagnostic (#1549). Code generation now asks whether the diagnostic is about a compiled template's declaration.
  • A type alias resolves an alias declared after it in its namespace, as a data type resolves wherever it is declared; inside a cycle of mentions, source order still holds and a cycle is E132. An alias naming a later one was registered unresolved and every use of it refused with E140 or E202 at the use (#1552), in a type argument, a constructor field, a function signature, and an effect's or an ability's operation signature alike, and the verifier's own registration reads the same rule.
  • Refinements in a type argument are two slot names when their predicates differ: a slot name's argument keeps its predicate, canonically, so @Array<{ @Int | @Int.0 > 0 }> and @Array<{ @Int | @Int.0 < 0 }> are two stacks and a reference's predicate is compared with its binding's (#1674); every parser of slot-name text reads such an argument as one.
  • The verifier verifies the program code generation compiles: a callee is the declaration its call is bound to, so two where helpers of one name under one top-level function are two functions for the disclosure rule, and the caller of the one whose result is established proves at Tier 1 where it was demoted (tier3, E534).
  • A refinement predicate a module's type writes is read as the module binds its names wherever a value is checked against the type, in another file too: a module alias type Pos = { @Int | pos(@Int.0) }; checked at a call from a file that declares its own pos was proved with that file's pos, a Tier 1 the run's guard refuted, and is now reported as violated (E505) where the run traps.
  • The instances the reserved prelude names answer (Changed, #1469) are #1495, #1496, #1553, #1556, #1560 and #1600, and the one a declaration's own WebAssembly namespace answers (Changed) is #1494.
• A contract predicate is held to purity, whatever its function's effects clause names (breaking) (#1708). A contract was checked under its function's row, so requires(Random.random_int(1, 1) > 0) under effects(<Random>) passed check and verify, and the compiled precondition performed the operation; a refinement predicate on an alias, a data field or a signature was held to no row at all. Spec §7.9.1 holds every contract predicate to purity, and the checker now refuses, with E187, each place in a requires, ensures or decreases clause, an assert, an assume or a refinement predicate that performs an effect: an effect operation, a call to a function whose effects clause names an effect, an apply_fn of a function value whose type names one, and an anonymous function written in it whose body performs one. A handler written inside the predicate handles its own instance of the effect there, so what it handles is accepted, and so are old and new. A program whose contract performed an effect is refused: perform the operation in the body, bind its value with let, and check that value with assert. No program in examples/, tests/conformance/ or the documentation's Vera blocks changes its verdict.
  • Under effects(pure), an operation in a contract is E187 at the operation, where it was E122 at the function; under a row that does not name its effect it is E187, where it was E125.
• A Map's or Set's String keys hash under a key drawn for each instantiation (#1736). The trie hashed a String key by FNV-1a over its bytes through a bijective mixer, with no key, so String keys chosen to share a hash shared one collision node, which every operation searches and copies whole: a program that builds a map from keys an adversary chooses, such as the request headers vera serve builds into a Request or the members of a JSON text it parses, paid O(n) per insert on such keys, 4,000 of them taking 1.25 s natively against 9.0 ms. A String key now hashes by SipHash-1-3 over its UTF-8 bytes under a 128-bit key the module draws on its first String hash, two 64-bit words through the new hash_key host import: from os.urandom under vera run and vera serve, from crypto.getRandomValues in the browser runtime, and from wasi:random in a WASI component, which stock wasmtime run and wasmtime serve provide. The key enters the hash's state, so keys that collide under one instantiation's key do not under another's. No output depends on the key: the enumerations read insertion order, and the Hash ability's hash of a String is still the deterministic FNV-1a. With the keyed hash, 4,000 inserts take 7.6 ms natively and 10.4 ms in the browser runtime, against 9.0 ms and 9.7 ms before; every other key type hashes as before, and its module draws no key.
  • A host other than Vera's own that runs a compiled core module binds vera.hash_key for a module that declares it: no parameters, one i64 result, a fresh random word at each call.
• tests/test_wasi_target.py builds its wasmtime Engine and Linker on first use, not at import (#1745). tests/test_import_time_wasmtime_1745.py holds every test module to that (no wasmtime object constructed at module level), and a mutation slice record whose engine log holds a Python fault dump keeps the dump's first lines, which name the test, beside its last. The nightly sweep's first night, which this issue reported, stopped for the reason #1747 records.
• The mutation lanes run pytest with -p no:faulthandler, so wasmtime's trap handlers survive mutmut's second in-process session (#1747). pytest's faulthandler plugin records the process's signal handlers when a session starts and restores them when it ends; wasmtime installs its trap handlers once per process, at the first Engine. mutmut's fork runner runs the stats pass and the clean pass as two sessions in one process, so the first session's end put the pre-session handlers back over wasmtime's, and the clean pass died on its first WebAssembly trap (SIGILL, exit -4) on each of the nightly sweep's first two nights (#1745), every forked mutant run inheriting the loss. With the plugin out nothing restores the handlers. tests/test_wasmtime_traps_across_pytest_sessions_1747.py runs two sessions over a trapping module in a subprocess, with and without the plugin, on Linux, where traps are signals; and a slice record's engine tail now starts a row at a fault dump's first line wherever mutmut's spinner left it, so the record names the dying test.
• The nightly mutation sweep tolerates a slice whose runner was lost (#1751). The nights of 19 and 20 October each lost one of seven slices to a hosted runner taken away under it (GitHub's own annotations on the jobs: lost communication with the server; a shutdown signal, exit 143 at 68 minutes), which uploads no record; the stitch read the missing record as a failure and the night went red with the other six slices' work kept. A slice with no record is now noted and its work planned again the next night; more than one in a night, or more than three over the last seven nights, still ends the run red. The sweep job's failure no longer colours the run, the stitch does, and the tracking issue is filed when the stitch fails. While the engine runs, a slice prints a heartbeat line every five minutes (elapsed time, available memory, swap, load, the engine's last status), so the job log, which outlives a lost runner, carries its resource trail.
• The Http limitation row no longer says a hung server hangs the program. The native runtime gives up after a fixed 60 seconds; what is missing is a caller's control of it (#351).
• An if or a match that joins an @Int branch with a @Nat one, or with a refinement of @Nat, is an @Int, so binding it into a @Nat position is obligated (#1756). The checker joined the two through the relaxed Int <: Nat rule, which gave an if whose then-branch is an @Int (a negated literal, literal arithmetic, an @Int slot or a sum over one) and whose else-branch is a @Nat the type @Nat, as it gave a match whose later arm is the @Int, and a join with a refinement of @Nat the refined type. The verifier, reading that type, recorded no narrowing where the join was bound into a @Nat let, call argument or constructor field, while the compiled module guarded the binding: let @Nat = if @Bool.0 then { -1 } else { @Nat.0 }; passed vera verify, and its run trapped. The join is now an @Int unless every @Int branch is made only of non-negative literals and @Nat values, so the narrowing is obligated where the join is bound: refused (E503) where a branch can be negative, and recorded beside the module's guard where it cannot. No program of the corpus, the examples or the docs' Vera blocks changes its verdict, its obligations or its compiled WAT.
  • Upgrade note: a program that verified with such a join and a branch that can be negative now fails with E503 at the binding; its run trapped there before. E503's fix applies: a precondition ruling out the input its counterexample names, or a guard on the binding.
• vera test names a trial's arguments as the source does (#1757). A trial's arguments were labelled in parameter order with each type counted from 0 left to right, so the first of two @Nat parameters was reported as @Nat.0, the name the source gives the second, and the labels contradicted the function's own requires. A parameter of type T is now labelled @T.n, n the number of later parameters of type T, the De Bruijn order the source's slot references use: pair(@Nat, @Nat -> @Int) with requires(@Nat.1 <= 0 && @Nat.0 >= 5) reports @Nat.1 = 0, @Nat.0 = 5. The text report, the --json report's args and the E703 description of a refuted proof each read the corrected labels; the arguments are listed in the parameters' order, as before.