v0.2.0

Highlights

• Every recursive function terminates or says it may not (breaking). (#1492)
• Checks are obligated where the program evaluates them. (#1480)
• A contradiction proves nothing. (#1451)
• Every runtime trap names its cause. (#1479)
• vera check refuses names it cannot resolve (breaking). (#1513)
• One declaration per name. (#1433)
• Modules keep their own data types. (#1317)
• A configurable Z3 budget and a complete account. (#1350)
• Agent-facing examples are executed, not just parsed. (#1481)
• The language server will not apply an edit that loses a proof. (#1443)

Added

• Every runtime check a compiled module contains is on a record, and the checks code generation can emit have one registry (#1479)
• The enumerated negative-conformance-fixture lists are gated against the manifest.
• The verifier's seed walk infers a generic call's type arguments inside the namespace the call is written in, so an E622 raised for a desugared pipe inside an imported module body is attributed to that module rather than to the entry file — the mirror of the scoping codegen already applies.
• The burndown-header word parser rejects malformed hyphenated compounds (twenty-ten, thirty-nineteen) instead of summing them, and the diagnostic-site walker in scripts/check_diagnostic_fields.py scopes decorators, parameter defaults, annotations and base classes to the enclosing site rather than to the definition they decorate — both gaps found in review of the Stage-20 gates.
• Rendered diagnostic output in docs is now replayed against live output, for a marker-annotated subset (#954)
• error_code uniqueness is now a gate, not a manual audit (#682)
• scripts/check_doc_counts.py now cross-checks ROADMAP's burndown header word against both its own table and KNOWN_ISSUES.md
• examples/ephemeris.vera — the first floating-point example (#143)
• The Z3 budget is configurable, so a verification tier stops depending on the machine (#1350)
• The E001 doc example is single-sourced, so its five mirrors cannot drift by hand (#954)
• A generated implementation-status appendix, and one vocabulary for obligation outcomes (#1341)

Changed

• check_doc_counts.py --release runs on the pull request that raises the version, not on every pull request into main (#1536)
• A commit runs the fast gates, CI runs the full suite, and the release PR sets the headline test totals.
• Bugs are filed and fixed by class, not by manifestation.
• A generic's type argument is now refused when it cannot be inferred, instead of being guessed (#1369)
• A refined-ELEMENT position now refuses what it used to disclose (#1430)
• The VS Code extension is 0.2.2.

Fixed

• A @Nat operand of an @Int operation is a widening: obligated, guarded, and never read as a negative number (#1591)
• An integer literal takes its type from its context when it fixes a generic's type argument (#1605)
• An imported generic's decreases is proved again through the file that imports it (#1577)
• A literal-arithmetic -3 bound at @Int is -3 again: every guard and every obligation reads one classifier of an integer's sign (#1544)
• Every check the compiled program performs is obligated where the program evaluates it (#1222)
• A match arm is checked knowing that no earlier arm matched (#1562)
• A refinement narrowing over a let the verifier cannot translate is left to its guard (#1524)
• A module's qualified call to its own function checks again (#1492)
• An imported data type named like a prelude type can be constructed again (#1559)
• Every recursive function proves it terminates or says it may not (#1492)
• The measure is checked across the whole cycle, and a contract cannot call back into its own function (#1521)
• A name that resolves to nothing is an error at check, so check implies compile again (#1499)
• Every runtime trap names its cause (#1479)
• An exception that escapes an entry point is named, with its type and the value thrown (#1479)
• A function's name can no longer decide the trap kind a host reports (#1518)
• Under WASI 0.2 a trap's message arrives whole, however long it is (#1479)
• A @Nat subtraction is checked as the unsigned subtraction it is (#1504)
• vera test classifies a trial by its trap's kind (#1479)
• The generic unreachable paragraph names what the wrapper table holds (#1479)
• A vera run --target wasi-p2 that traps releases its store before it reports, so it can no longer abort at exit.
• Every example the agent-facing documents teach passes the toolchain, or says why it does not (#1481)
• A name is declared once per namespace (#1497)
• A type or effect name nothing declares is refused where it is written (#1489)
• A module's signatures are measured in the module's own namespace, imports included (#1493)
• A quantifier's predicate must be a function of the index to Bool, and its index type an Int or a Nat (#1506)
• A handler-clause State operation code generation cannot lower is refused at check (#1522)
• A generic call nested inside another compiles in a module's body, as it does in the entry file (#1509)
• A generic instantiated at a data type its declaring namespace does not hold compiles again (#1519)
• A module's call to a function of its own, or one it imports, runs that function when the entry file declares a function of the same name
• A generic called at a Set or Map named from a call's result compiles.
• Two imported modules that each declare a constructor of the same name no longer drop the importer's functions (#1535)
• show and hash of a value dispatch on the value's type, not on the compiling file's reading of its name (#1539)
• A data declaration may not take the name of the built-in type Array, Map, Set or Decimal (E158) (#1496)
• A generic called on a prelude call that unwraps a Result compiles (#1515)
• Module registration is memoised per module for the whole check (#1275)
• A boundary guard binds the whole value, so a pair-represented refinement stops refusing what it admits (#1439)
• Every obligation discharged inside a match arm reads the facts that arm establishes (#1399)
• A function's premise set is checked for satisfiability before any of its obligations is trusted (#427)
• A where helper's withheld fact says why it was withheld (#1403)
• A termination measure is no longer proved against a binding a match arm shadows (#1403)
• A correct program is no longer refused on a value the solver cannot read (#1460)
• A refinement over a refinement is modelled, so an obligation over one can be discharged (#1470)
• A constructor argument's field type is on the record (#1541)
• One derivation of whether a bind narrows a refinement (#1448)
• A provable predicate over an opaque value keeps its Tier 1 (#1460)
• A handler-clause binder is obligated and guarded (#1448)
• The binder positions the grammar has are written down (#1455)
• A call boundary obligates its argument wherever the callee is declared (#1455)
• The warm session no longer replays a proof its dependency broke (#1453)
• A call precondition is reported once per call site (#1459)
• A refined value placed into a container is checked where it goes in (#1440)
• The State write boundary checks its refinement predicate (#1439)
• The @Nat sign guard reaches the array-element and Map-value stores (#1440)
• The @Nat -> @Int widening guard names itself (#1438)
• An unclassified operand pair emits the overflow guard (#1417)
• A container's element refinements are stated once, for every container (#1430)
• A true postcondition over an Array<Refined> element is no longer refused (#1449)
• An edit that takes a proof away is no longer applied without force (#1443)
• A proposed edit reaches the server's view of a document only through the client (#1444)
• One E623 per contended name, not one per contending module (#1446)
• A refinement over a refinement means the conjunction of its predicates (#1415)
• A handler is checked by its Vera types, not by its ABI (#1442)
• One sort for a refined payload, wherever a term is rebuilt (#1360)
• Non-regular recursion in a data declaration is refused at check time (#1429)
• A verdict no longer changes when an unrelated module is added (#1423)
• A disclosed fact stays disclosed across an import (#1275)
• A burndown driven to zero can now be written down (#1401)
• check_limitations_sync.py's section scan is bounded before it finds a table (#1405)
• A refinement written inside a type is now obligated at every position that publishes it (#1410)
• Every refinement narrowed by a pattern bind is now runtime-guarded (#1268)
• A constructor field is guarded by its instantiation, not by its declaration (#821)
• A refined base with a non-plain type argument no longer discloses a guard that fires (#1034)
• An effect operation's argument is guarded from its formal, and the narrowing guard names itself (#808)
• A decreases measure's fit in the range its guard compares in is obligated, not assumed (#1222)
• The last two Tuple-component coercion sites are guarded (#1416)
• A refinement over a refinement bound by a pattern is unguarded, not refused.
• The decreases range check does not evaluate an effectful measure.
• An unguarded E506 names the cause that applies, not the one that used to
• The closure-argument guardedness derivation is pinned by measurement (#1420)
• The nested-refinement leg reads the site roster like every other one
• The construction-position obligation reaches nested containers (#1608)
• An array element narrowed at construction is obligated (#1440)
• decreases_bound's guarded flag is computed per COMPONENT
• The reach of the @Nat guarantee is stated accurately.
• #1399's cross-module chain keeps its premise (#1422)
• array_fold's accumulator root is addressed, not counted (#1384)
• Two modules may declare the same data name wherever nothing can meet them (#1029)
• A burndown driven to zero can say so
• A disclosed fact's taint follows the value, not the spelling of the call (#1433)
• A type variable reached only through a parameter's type arguments is inferred, not guessed (#1327)
• The remedy E155 prescribes now compiles (#187)
• A data declaration may not take a built-in type name the compiler special-cases (#1397)
• A constructor named after a special-cased built-in ADT is refused, closing a silent wrong value (#1408)
• A constructor name now means the declaration of the namespace that uses it (#1436)
• Two data declarations in one namespace may no longer share a constructor name (#1425)
• A user constructor no longer displaces a built-in or prelude constructor of the same name (#1414)
• Running the corpus differential no longer turns the test suite red (#1374)
• A type alias named after a prelude ADT no longer leaks into the prelude's own bodies (#1316)
• A user data declaration named after a built-in container compiles at its own width (#1321)
• That misclassification cost the whole module its exports, and no longer does (#1331)
• The entry file's data declarations meet the modules' in the one layout namespace, loudly (#1312)
• Two modules that declare the same layout are no longer a collision (#1317)
• A pattern must be able to match the scrutinee (#1381)
• A constructor pattern over a constructor-less container is refused (#1305)
• A string literal match arm compiles (#1380)
• An integer literal arm compares at the scrutinee's width, so a Byte match loads (#1381)
• A where-helper is local to its parent on the checker's table too (#1299)
• A bare call to an imported module's where-helper is refused (#1383)
• md_parse no longer hangs the browser runtime on a CRLF document with a heading (#1301)
• md_parse agrees across the two runtimes, because §9.7.3 now states the grammar (#1388)
• The garbage collector no longer writes a mark bit through a guessed pointer (#1382)
• A call's heap result is rooted where it LANDS, so a sibling cannot allocate over it (#1382)
• A GC shadow root now lives as long as its value, not as long as the frame (#1371)
• hash over a struct-shaped parameter no longer emits $gc_sp without declaring it (#1376)
• String interpolation decides on the resolved type, not the spelling (#1347)
• Interpolating an alias-typed value compiles (#1347)
• Parse errors name tokens a Vera author can write (#1349)
• A contract clause after effects is told what to do about it (#1348)
• A generic's type argument comes from the checker when neither walker can name it, and a pipe names its result (#1357)
• A @Nat narrowing claims a guard only where one is emitted — and the missing guards are planted (#1205)
• vera test reads the statuses the verifier computed, not a copy of them (#1229)
• A disclosed fact is no longer assumed at full strength downstream (#1363)
• Chapter 6's two MUST-warnings are emitted (#1345)
• The checker refuses old() / new() naming an effect the row does not declare (#1298)
• A match no longer costs GC shadow roots for the rest of the frame (#1371)
• The four sibling shadow-stack bounds are slot-complete (#860)
• A generic reached from a postcondition is instantiated at the type @T.result declares (#1327)
• examples/README.md's Demonstrates column is now gated against the example it describes (#1351)
• A Tuple nested inside a constructor no longer crashes the verifier, and verify --json always emits an envelope (#1360)
• A @Nat component narrowed at construction is obligated, not assumed (#1332)
• check_limitations_sync.py --check-states reads a table's Issue column, not its prose (#1337)
• Public claims narrowed to the assurance the compiler actually delivers (#372)
• A module generic instantiated from an effect-operation result now registers its clone (#1310)
• The nightly stress workflow now runs every stress-marked test, not just tests/test_stress.py (#1328)
• ch05_closure_nat_return's single conformance-run trap is closed as monitored, not reproduced (#1328)
• The documentation describes the compiler it ships with (#1574)