v0.2.3

Highlights

• Upgrade note: Nat is the non-negative i64, and every integer literal is an Int. A @Nat holds 0 .. 9223372036854775807, the { @Int | @Int.0 >= 0 } that spec §2.2 defines, where the compiler held an unsigned 64-bit integer. A program that held a @Nat above 9223372036854775807 cannot now: @Nat arithmetic that would pass the bound traps (overflow) unless a requires that keeps it in range proves it, parse_nat returns Err("out of range") for a numeral above the bound, and vera run refuses such an argument. An integer literal above the bound is E149 wherever it is written, a @Nat context and a literal pattern included: write the value in range. A literal no longer takes its type from its value, so in a @Nat context it is a narrowing, checked as any @Int narrowing is: let @Nat = 0 - 3 is E503, and so is a negative literal argument of a generic call bound into a @Nat, and @Nat.0 - 1 is an @Int subtraction, which bound into a @Nat is E503 where it was E502, discharged by the same requires(@Nat.0 >= 1) (#1700)
• A construct code generation cannot lower is refused at check, where it is written. vera/lowering.py holds one rule per construct, which the checker applies and code generation asks again at its own refusal site, and the new E340 refuses a handler for any effect but State and Exn, a State cell holding a String or an Array, a user-declared ability's operation, and an effect row that names a user-declared effect, or a row variable in a function's own row, each of which passed check and verify and was then dropped at compile or compiled to a module that failed to load (#1687, #1699)
• An effect operation is held to the effect row in force, wherever it is performed (breaking). Random.random_int(3, 3) in an effects(<IO>) function ran, and is now E125; a closure's body is checked under the closure's own row, and a State or Exn operation in a closure needs a handler written inside the closure (E340). A program that performed an effect its row did not name adds the effect to the effects clause of the function or closure that performs it, as the diagnostic's fix writes it (#1703)
• An array literal, an if and a match have the type all their parts give them. Every element of an array literal is held to the literal's element type (E162), and a position one part leaves open, a None's T or an empty literal's element, takes its type from the part that fills it: [None, Some("abc")] is an Array<Option<String>>, where it passed check and verify as an @Array<Option<Nat>> argument and vera run read the "abc" as a @Nat (#1669, #1683)
• A match over a scrutinee already in error is reported once, at the scrutinee. The exhaustiveness check no longer judges a scrutinee the checker typed unknown after an error, so the error behind it is not followed by an E313 at the match (#1701)
• &&, || and ==> short-circuit, in compiled code and in the verifier's premises. The right operand runs only where the left one does not decide the result, and the verifier takes the left operand as a premise of the right, so the guard idiom @Int.0 != 0 && 10 / @Int.0 > 0 verifies and returns false at 0, where vera verify refused it (E526) and the compiled code trapped (#1704)
• A nested pattern is read to its full depth. One module, vera/patterns.py, reads it for the exhaustiveness check and for the verifier's condition on an arm, so the arms Some(Red) and None over an Option<Colour> are E311, naming Some(Green), where they checked clean, and an ensures the verifier proved over a function that returns 7 for Some(Some(7)) is refuted (E500) (#1705)
• A result reference is held to the function's return type. ensures(@Nat.result == 1) on a function returning @Int is the new E163, where it was proved at Tier 1 (#1672)
• A bug report names its mechanism, its effect and its reach. A new issue is for a mechanism no open issue names, and an instance of an open class is a checklist line on that issue; 44 open bugs were consolidated into seven class issues, one per mechanism, and twelve defects of the tests, the tooling, the language server and the documentation left the bug label, so KNOWN_ISSUES.md's Bugs table lists the language's defects (#1693)

Added

• vera/lowering.py holds what code generation lowers, one rule per construct, and E340 refuses at check what it does not lower (#1597, #1512, #1499). The rules are the effect a handler handles, a State cell and an Exn payload, a State clause's resume, a quantifier's predicate and bound, the abilities lowered, and E339's shadowing judgement with its re-entry cap. The checker applies each where its construct is written, and code generation asks the same function at its own refusal site, where a refusal is an internal error (E699) that names the rule. E340, "Code generation cannot lower this construct", is new; E179, E128 and E339 keep their rules.

Changed

• An effect row code generation cannot lower is refused at check, at the row entry, and so is a call of a user-declared effect's operation (#1681). A function whose row named a user-declared effect, State or Exn without a type argument, or a row variable (forall<E> with effects(<E>)), passed vera check and vera verify, and code generation dropped it (E603, E606, E611), for a row variable the template and every clone. Rule 6 in vera/lowering.py refuses each such entry with E340: a user-declared effect and State or Exn without a type argument in every row (a function's, a where helper's, a closure literal's and a function type's), and a row variable in a function's own row, since code generation compiles each instantiation's types and never its row. A row variable in a function type's row, a parameter's or a closure literal's, compiled and still does. A closure or a function type whose row named a user-declared effect compiled, and nothing could apply it, since applying it needs the effect in the caller's row. An operation of a user-declared effect called where no row names it, Counter.tick(()) in an effects(<IO>) function, in a closure whose row is a row variable or in a refinement predicate a function uses, passed check and verify and compiled to a module that does not load, and a type alias or a data type nothing uses whose refinement predicate calls the operation ran, with the predicate never compiled; each is refused at the call (E340), and that is the call's one refusal: the purity check (E122) does not count it. So a user-declared effect is a declaration only: the effect block checks, and nothing that uses it does; a handler for one was already refused (E340). Code generation's own refusal of a row entry is an internal error (E699) that no checked program reaches. A function whose own row names a row variable and that nothing calls ran at the base as dead code, the function dropped, and is refused now. tests/test_lowering_boundary.py holds the rule over 16 kinds of row entry (the registry's eight built-in effects without a type parameter, State<Int>, Exn<Int>, State, Exn, a user-declared effect, a row variable, and each of the last two beside IO) in five places (a function's row, a where helper's, a constrained generic's, a closure literal's and a function type's), over an operation performed in a closure whose row is a row variable (a user-declared and a built-in operation, applied and not, under a pure and an <IO> row), and over one in a refinement predicate (an alias's, a data field's, a signature's and a where helper's).
  • examples/effect_handler.vera counts with a State<Int> row in place of its user-declared Counter, and examples/maximum_syntax.vera keeps its Counter and Logger<T> declarations and drops the two functions whose rows named them.
  • Spec §5.9.1, §7.2, §7.3, §7.6, §7.6.1 and §11.4.1, SKILL.md and ROADMAP.md state the rule, and spec §6.4.3 and §11.17 and SKILL.md say a user-declared effect operation's argument is unreached because its row is refused at check. The #294 limitation rows say a row variable is refused in a function's own row and accepted in a parameter's function type. DESIGN.md's effects paragraph no longer says user-defined effects follow the built-in effects' pattern.
• A construct code generation cannot lower is refused at check, where it is written (#1597, #1512, #1506, #1499, #1522). Each passed vera check and vera verify, and was then dropped at compile (E602, E607, E612, E613) or compiled to a module that failed to load.
  • A handler for any effect but State<T> and Exn<E>, a host effect's (handle[Http] as a mock) or a user-declared one's (#1597): E340 at the handler.
  • A State cell whose value is a (ptr, len) pair (String, Array<T>, a refinement or alias of either) or has no representation (Unit), in a handler or a declared row, an Exn payload with no representation, and an inline refinement as a handler's cell type (#1512): E340 at the type. The fix for a pair cell is a one-constructor data wrapper, private data Text { T(String) } and State<Text>.
  • A State clause whose body does not end in exactly one resume(...), or whose with update holds one: E340 at the clause, whether an operation reaches it or not.
  • A quantifier predicate whose parameter or result is a type parameter, and a bound typed by one (#1506): E179 and E128 at the generic, for every instantiation. A type parameter as the index type is still accepted, since it lowers at every instantiation.
  • A call to a user-declared ability's operation, a where constraint naming a user-declared ability, and a qualified ability call such as Eq.eq(1, 1) (#1499): E340. The qualified call was E220, whose fix said to declare an effect named Eq; its fix is the bare call now. A qualified call to an operation the ability does not declare, Eq.nope(1), stays E220, whose message now names the ability and the missing operation, and whose fix declares a function under its own name.
  • A clause-body State operation that a type-parameter cell can shadow (#1522): E339 at the generic, conservatively, so g(true), which ran, is refused with g(5), which was dropped.
  • Code generation's refusal sites for these rules are internal errors (E699), which no checked program reaches. E607 and E612 stay user-facing for a State<T> or Exn<T> clone instantiated at a type the rule refuses, which the checker cannot see without the instantiation set (#1679).
  • DESIGN.md's effects sentence, FAQ.md, SKILL.md, EXAMPLES.md and spec §6.3.3, §7.3.3, §7.5, §8.9.3, §9.8 and §11 state what is implemented.
• Nat is the non-negative Int its definition says it is, 0 .. 2^63 - 1, and every integer literal is an Int. This change is breaking (#1504). Spec §2.2 defines Nat as { @Int | @Int.0 >= 0 }, and the compiler held it as an unsigned 64-bit integer in a signed slot, with a range no Int can hold: a literal could reach 2^64 - 1, @Nat arithmetic was checked against the unsigned range, every place a @Nat met an @Int carried its own obligation and guard, and the operations that read a value's sign read a @Nat above 2^63 - 1 as the negative number its bits spell. A @Nat is now an i64 whose value is non-negative. Reading one as an @Int is a no-op; its arithmetic, comparisons, division and rendering are the @Int instructions; its + and * are checked against the i64 range, and its - against zero (nat_sub, as before).
  • A literal is an Int wherever it is written. In a @Nat or refined context it is a narrowing, obligated as any @Int narrowing is: let @Nat = 5 verifies and let @Nat = 0 - 3 is refused (E503). The sign of a literal no longer decides a type: 5 - 2 is an Int, id(5) with nothing expected is id at Int, and an expected Nat fixes a type argument whatever the literals' signs, so let @Nat = second(-3, 5) and let @Nat = array_reverse([0 - 3, 5])[0], each of which verified and returned 5, are refused (E503) and trap at the negative literal (spec §4.2).
  • Upgrade note. A program that held a @Nat above 9223372036854775807 cannot now. A literal above that bound is E149 wherever it is written, a @Nat context and a literal pattern included, and a pattern over a @Byte is held to 0..255. An operation whose @Nat result would pass the bound carries the i64 overflow obligation, and traps (overflow) where the obligation is not proved; abs(-9223372036854775808) is one, since its result 2^63 is no Nat. parse_nat returns Err("out of range") for a numeral above the bound, and vera run refuses a @Nat argument outside 0 .. 9223372036854775807, an @Int one outside the i64 range, and a @Byte one outside 0 .. 255, instead of wrapping it. nat_to_int stays, the identity, and is never needed to widen: a @Nat is an @Int as it stands. A subtraction with a literal operand, @Nat.0 - 1, is an @Int subtraction: bound into a @Nat it is obligated there (nat_bind, E503) rather than as a @Nat subtraction (nat_sub, E502), and read as an @Int its value at 0 is -1 rather than an underflow trap.

Removed

• E603, E606 and E611 (#1681). Code generation's warnings for a function whose row named an effect it does not compile, or State or Exn without a type argument. The check refuses each such row entry (E340), so nothing emits them, and vera errors no longer lists them.
• The @Nat → @Int widening check, the range check on a @Nat termination measure, and the typing of a literal by its value (#1504). With Nat the non-negative i64 none of them has anything to check. Gone: the nat_to_int_coerce obligation and check kind, its diagnostics E530 (a widening provably above i64.MAX) and E531 (a widening neither proved nor guarded), the widen_guard trap kind and every widening guard spec §11.2.1 listed; the decreases_bound obligation and its diagnostics E536 and E537, which held a @Nat measure to the i64 range the guard compares in; the u64 range of the overflow obligations; the sign-provenance classifiers of vera/narrowing.py; and spec §4.2's rule 3 (a type argument fixed by its literals' values) and rule 2's exception for a negative literal beside a non-negative one. The change takes 4,413 lines out of vera/ and adds 1,157, most of them vera/verifier.py's (1,367), vera/narrowing.py's (930) and vera/wasm/operators.py's (691).

Fixed

• &&, || and ==> do not evaluate a right operand the left one decides, in compiled code and in the verifier (#1501). Spec §4.6 says the right operand of && and || is not evaluated if the left operand determines the result, but code generation lowered the three operators to an instruction over two evaluated operands (i32.and, i32.or, and i32.eqz then i32.or for ==>), so a right operand that traps or performs an effect ran after the left one had decided: @Int.0 != 0 && 10 / @Int.0 > 0 trapped on 0, @Int.0 >= 0 && @Int.0 < 3 && @Array<Int>.0[@Int.0] > 15 trapped at the index on 5 and on -1, and true || say(()) printed. The verifier matched that lowering and took no left operand as a premise of its right one, so the same division was refused E526 and the index recorded Tier 3. The one lowering every compiled position reaches (a body, a compiled requires or ensures, a refinement guard, a quantifier predicate) now compiles a && b to if a then b else 0, a || b to if a then 1 else b and a ==> b to if a then b else 1, and the SMT translation and the walks that obligate an expression (primitive operations, binding-site @Nat narrowings, the decreases measure's recursive calls) take the left operand as the premise of the right one, its negation for ||, as an if arm takes its condition: an obligation in the right operand is discharged under it, and a fact learned there (a callee's assumed ensures, a refined binder's predicate) is assumed under it. A left operand the verifier cannot translate is stood for by a fresh Boolean, so a fact learned in the right operand stays conditional on a value nothing states. Spec §5.2.2's equivalence of several requires clauses with one joined by && now holds: requires(@Int.0 >= 1 && need_pos(@Int.0) > 0) verifies as requires(@Int.0 >= 1) requires(need_pos(@Int.0) > 0) does, where it was refused E501, and on 0 both fail the function's own precondition without calling need_pos. The first decision of PR #1486, that && and || are not premises while both operands are evaluated, is reversed with it: { @Nat | @Nat.0 == 3 || @Nat.0 - string_length("abcde") > 0 } accepts 3 where its guard trapped, and a postcondition that rested on a refined binder bound in &&'s right operand, which now does not run where the left operand is false, is left to its runtime check (E522) where it was proved. Spec §4.6 now names ==> among the short-circuiting operators, §11.3.3's table gives the three lowerings, and §2.6, §5.2.2 and §6.4.3 state the premise. tests/test_short_circuit_1501.py holds the class: 105 cells over the position (a body, a requires, an ensures over @result, a refinement predicate at a boundary, a forall predicate, a where helper, a closure, an assert), the operator, and what the right operand holds (a division, an index, a call whose requires the left operand establishes, an @Int narrowed into a @Nat parameter, and an IO.print in the three effectful positions), each compiled, run, verified and reconciled with the checks its module holds beside the if §4.6 defines it as, and held to the same records, runs and reconciliation, all 105 red at fa95873; and 27 cells for the issue's programs, each operator's truth table, the premise ending with the right operand, an operation in the left operand, an untranslatable left operand, the premise's own translation and each walk. tests/conformance/ch04_short_circuit.vera runs the guards, the effects and the joined requires.
• A result reference is held to the function's return type (#1517). The checker resolved a result reference's type arguments and then typed the reference as the return type whatever its head named, so on a function returning @Int, ensures(@Qzt.result == 1), ensures(@Nat.result == 1) and ensures(@String.result == 1) each passed vera check and was proved at Tier 1, and on a function returning @Bool an @Int.result reached code generation, which wrote a module that does not validate. A result reference now names the result only where its name is the return type's, judged as a slot reference is matched to its binding (spec §3.6, §3.8): the reference's name and the name a binding of the declared return type is bound under come from one renderer and are compared, so an alias at the head stays opaque (@Cnt.result for a @Cnt return, never @Int.result), type arguments resolve through aliases (@Option<Cnt>.result and @Option<Int>.result both name an Option<Int> result), a refinement written out is named by its base, and a function type written out is @Fn.result. A reference of any other type is the new E163, reported at the reference: its message quotes the reference as written and the return type as the signature spells it, and its fix names the reference in that spelling, which the program accepts in place of the refused one; the reference then types as unknown, as an unresolved slot reference does. A return type the check refuses where it is written is not judged, so its own error stands alone, as before. tests/test_result_reference_type_1517.py holds the class: 135 cells over where the function is declared (at the top level, as a where helper, in an imported module), fifteen return types and fourteen ways a reference's type can differ from the return type, each of which also checks the program clean with the fix's reference written in, and 69 cells of references that name the result, chapter 3's examples among them, which check clean and whose postconditions verify as they did. Every examples/ program, conformance program and documentation block still passes its gate, and the new negative fixture ch03_result_reference_type is refused with E163.
• Every element of an array literal is held to the literal's element type (#1584). The checker took an array literal's element type from its first typed element and never compared the other elements with it, so array_length(["a", 5]) passed vera check and code generation wrote a module that failed to load, and [@T.0, 0] passed in a forall<T> body, where T is rigid, and failed to load once instantiated at String. Each element after the first typed one is now held to the element type by the judgement a call argument is held to its parameter by, one method the two share (_fits): a subtype, or a type that a type variable still unresolved on either side leaves compatible, so [None, Some(1)] checks as before. An element it refuses is the new E162, reported at the element and naming its position, its type and the element type. The element type is still the first typed element's, a literal's type is unchanged wherever every element fits, and a zero-size element type is still refused once for the whole literal (E135). tests/test_array_literal_elements_1584.py holds the class: 183 cells over where the element is, what it is and fifteen positions the literal stands in, 400 pairs of element types against an oracle of their own, and 41 literals that check with the type they had. The examples/ and tests/conformance/ programs check exactly as before, and the new negative fixture ch04_array_literal_element_type is refused with E162.
  • An array literal whose first element leaves a type position open, a None's T or an empty literal's element, keeps that position open and accepts elements that fill it with different types; it is filed as #1668.
• An array literal, an if and a match have the type all their parts give them, an open position included (#1668). A part whose type leaves a position open, the T of a None or the element type of an empty literal [], was held to the other parts with the position a wildcard, and the position stayed open in the type the whole was given. So second([None, Some("abc")]) passed vera check and vera verify into an @Array<Option<Nat>> parameter and vera run read the "abc" as a @Nat, array_length([None, Some(1), Some("abc")]) checked, let @Array<Array<Nat>> = [[], ["abc"]]; checked and failed to load, as did first(if true then { ["abc"] } else { [] }) into an @Array<Nat> parameter, and match @Nat.0 { 0 -> None, _ -> 5 } and if @Bool.0 then { None } else { Ok(1) } checked. The parts are now joined by one function, CallsMixin._join: the type of the first typed part, with each position it leaves open given by the first later part that fills it, and each open type variable bound by name, so that one occurring twice takes one type. It does not fill a type variable where code generation compiles behaviour for it, inside a function type or under a data type's parameter that a constructor field holds a function over: code generation finds a generic call's instantiation from its arguments and the type it is expected at, not from a join. Nor does it fill a built-in's variable that a parameter of the call mentions and the arguments left unbound, which stands for a type a failed substitution lost (#1684); a built-in's variable that no parameter mentions, as map_new()'s K and V, is marked free at the call, an open position as a constructor's type parameter no field holds is, and filled. The shapes the join leaves keep the verdict each site gave them, bar a match arm a variable withheld for behaviour would have to take the type of, which is now refused (E302) where the arm's type was taken without comparing the two. An array literal has that element type, so [None, Some(1)] is an Array<Option<Nat>>, and an element that does not fit it is E162, which names the elements the type comes from (the type of element 0, completed by element 1). An if whose branches no open position reconciles is E301, and such a match arm is E302, which now shows an open position as ? and so is reported once where an arm is checked more than once. Branches and arms that agree once their open positions are filled now check: match @Nat.0 { 0 -> Ok(1), _ -> Err("e") } was refused E302 and is a Result<Nat, String>. A position no part fills stays open for the context to fill, as before. tests/test_array_literal_open_position_1668.py holds the class: 1,584 cells over the site, the type that leaves the position open, how deep it sits, what fills it and where the whole stands, each expectation stated by rule, 162 of them strict xfails for #1684: a let or a return refuses a type variable the parts leave open, which an argument fills; 48 cells over a variable that occurs twice, a built-in's fresh variable and each shape the join does not fill, at each site, and four programs refused at check that f3b4415 ran or trapped on. The examples/ and tests/conformance/ programs pass as before.
• A stress test runs under a budget of 600 s, and a test can name a budget of its own (#1670). tests/pipeline.py ends the process when a stage call is still running at the end of its budget, 120 s for a call that names none, and the stress-marked tests named none. The 10,000-insert map_insert chain of tests/test_codegen_gc_reclamation.py::TestHostHandleReclamation573::test_map_chain_reclaims_transients, which took from 48.1 s to 94.3 s of call time in three runs on a 12-core Mac, ran past it on a GitHub runner five times in the runs of #1669 and #1672, three times in a row at one head, and each time ended the stress job before the stress tests after it ran. The new budget(seconds) marker runs a test under a budget of its own, and a stress-marked test that names none runs under 600 s: tests/conftest.py holds the whole test to it, so each stage call in the test that names no budget_s= runs under the test's budget, a call that names its own keeps it, and a test with neither marker runs as before. tests/test_budget_marker_1670.py holds this in eight cells, under pytest-xdist and without it, with the default lowered to 0.5 s and a stage call that takes 1.5 s: unmarked, the call is ended and the run names the test; marked budget(5) or stress, the test passes; and inside a budget(5) test, a call that passes budget_s=0.5 is ended at its own budget. The stress workflow now also runs on a pull request that changes tests/conftest.py or tests/pipeline.py, the two files that decide the budget a stress test runs under.
• A match whose scrutinee is already an error is not also reported non-exhaustive (#1671). The checker types an expression it has refused as unknown, and the exhaustiveness check judged an unknown scrutinee as a type with an infinite domain, so match @Option<Int>.0 { Some(@Int) -> @Int.0, None -> 0 } with no Option<Int> binding in scope was reported E130 at the reference and then E313 at the match, whose arms cover both of Option's constructors. Every scrutinee the check types unknown after an error drew the same E313: an undefined call (E200), a result reference naming another type (E163) or written outside a postcondition (E131), an undefined constructor (E210), an index into a value that is no collection (E161), the slot inside a block or in both branches of an if, a let declaring the removed alias Float (an error with no code), a constructor of a declaration refused as E158, and a call two imports supply (E155), the last two with their error placed at the declaration or the import. A scrutinee typed unknown, a refinement of one included, once the check has reported an error is now not judged for coverage (spec §4.9.2). Its arms are still checked, so an error inside one is still reported, and an arm after a catch-all is still reported (E310), since that reads the arms alone; the pattern-fit rule (E314) already withheld itself from an unknown scrutinee. Every error reported by the time the scrutinee is typed counts, because the error behind it can sit at a declaration or an import. A scrutinee typed unknown with no error reported, an apply_fn over a type variable in a forall body, is judged as before: its E313 is the one error that refuses the program, which without it passes check and verify and has its functions dropped by code generation (E620). tests/test_match_unknown_scrutinee_1671.py holds the class: 297 cells over ten ways a scrutinee comes to be in error, eleven arm shapes and three positions (a function body, an ensures, a where helper), each reporting exactly the scrutinee's own codes and then what its arms report whatever the scrutinee, 216 of them red at a5b5de8 by one trailing E313; 197 cells over the same arms over the scrutinee written correctly, each keeping its verdict (E310, E311, E312, E313 or E314) and, where the arms draw none, verifying with every obligation proved; 99 over a scrutinee whose error leaves it a type (a call with the wrong arity, a let whose initialiser is in error, an if with one branch in error), and 11 over an unknown scrutinee with no error reported, each judged as before. The six cells of tests/test_result_reference_type_1517.py that expected E313 after a refused result reference now expect E163 alone. The examples/ and tests/conformance/ programs and the documentation blocks pass their gates as before.
• A match is judged and verified to the full depth of every pattern (#1697). The exhaustiveness check covered a data type by the constructors its arms name at the top, so match W(Green) { W(Red) -> 1 } over data Wrap { W(Colour) } checked clean and ran the W(Red) arm, match Some(Green) { Some(Red) -> 1, None -> 0 } printed 0 (#1540), and a tuple was not judged at all, so Tuple(Some(@Int), @Int) -> @Int.0 alone returned 3 for Tuple(None, 3). The verifier took an arm to be taken whenever its outer constructor matched, so after Some(None) -> 0 the arm Some(Some(@Int)) -> @Int.0 was unreachable to the proof and ensures(@Int.result == 0 || @Int.result == 1) was proved over a function that returns 7 for Some(Some(7)) (#1562). One module, vera/patterns.py, now reads a pattern to its full depth for both. The check reports E311 whenever a value of the scrutinee's type matches no arm, naming the cases missing at the first position that leaves one: a constructor missing at the top by its name, as before, and a case inside a constructor as a pattern, W(Green), Some(_), Tuple(None, _). A field whose type is a type parameter the function declares is covered only by a wildcard or a binder there, as a match over a T needs a catch-all (E313), since T may be Int: Some(None) -> 1, Some(Some(_)) -> 2, None -> 0 over Option<T> checked clean and returned 0 for Some(5), and is now E311 naming Some(_). The verifier's condition for an arm is every test its pattern makes, each on the field its path reaches, so the ensures of #1562 is refuted (E500), a guarded refined binder under a nested pattern carries its predicate in its arm, and an arm after a nested one is reached by exactly the values the earlier arm does not take. No pattern condition models a String literal, so a match with a String literal inside a constructor in an earlier arm is not translated and its ensures is Tier 3 (E522), where ensures(@Int.result != 2) over Ok(_) -> 0, Err("a") -> 1, Err(_) -> 2 was proved. A match with no refutable pattern inside a constructor is judged and verified as before, message for message. tests/test_nested_patterns_1697.py holds the class over eight scrutinee types (Option<Colour>, a one-constructor wrapper, Option<Option<Int>>, Result<Option<Int>, String>, Option<Bool>, Option<Int>, a three-constructor type with payloads to depth 3, and Tuple<Option<Int>, Bool>) and the arm sets over each, every expectation checked against an oracle that enumerates the type's values: 131 check cells, 42 of them red at fa95873; 66 cells over the ensures of every set that covers its type, 36 red; and 51 cells that run each value of the type and find the arm the spec selects, as code generation always did. The new negative fixture ch04_match_nested_missing is refused with E311, and the examples/ and tests/conformance/ programs pass their gates as before.
  • A pattern under a refined scrutinee is checked as under its base: a constructor's fields and a tuple's components are read at the base type's arguments, as the coverage reading reads them, so Some(Red) over a refinement of Option<Int> is E314, as over Option<Int>, where its sub-pattern was checked against the declaration's T and accepted.
• An effect operation is held to the effect row in force, wherever it is performed (#1702). A call to a function was held to the row in force at the call (E125), and an operation of a built-in effect was compared with its row only when the row was pure (E122), so effects(<IO>) performing Random.random_int(3, 3) passed check and verify and ran. So did IO.print in a handle[State<Int>] body inside a pure function, a Random operation in a requires clause or a where helper's body under <IO>, and a bare throw under <IO>, which code generation then dropped. A closure literal's body was checked under the row around it, so the closure's own row held none of its operations: a closure declared effects(<E>) performing Random inside an <IO> function ran, and one declared effects(pure) performing Random inside a <Random> function was given a pure type. An operation is now permitted where the row in force names its effect, at any instance of it (<State<Int>> permits put), and a row variable names no effect, so <IO, E> permits IO's operations and no others; elsewhere the call is refused E125, or under effects(pure) the function E122, as before, with no second code at the call. A closure's body is checked under the closure's own row, and a pure closure that performs an effect is refused E122 at the closure. Where the row in force is pure, a closure that performs an effect, directly or through a closure written in it, is still refused E122, at the function or closure it is written in, whether or not it is applied, and wherever a closure is applied the row in force must permit the closure's row (E125). A handler's body is checked under the row around it with the handled effect added, as before. A quantifier applies its predicate, a closure literal code generation inlines, where it is written, so it is held to the predicate's row as apply_fn is (E125, its effects counted for the purity check): a pure function whose forall predicate performs IO is refused at the quantifier (E125) as well as at the function (E122), and one whose row names Random and not the predicate's IO, which passed check before, at the quantifier. A function's signature, a where helper's included, is checked where no row is in force, as a top-level one always was. Upgrading: a program that performed a built-in effect's operation under a row that did not name the effect now fails check with E125: add the effect to the effects clause of the function or closure that performs it, as the diagnostic's fix writes it.
• A State or Exn operation in a closure's body is refused at check unless a handler for its effect is written inside the closure (#1702). Code generation compiles a closure as a function of its own, which registers no cell or tag from its row, so such a closure passed check and its function was then lost at compile: bare put and throw with E602, qualified State.put and Exn.throw with a module that did not assemble. vera.lowering rule 7 refuses the operation at the call (E340), the call's one refusal. A handler written inside the closure lowers it, and a handler around the closure does not, since the closure can be applied outside it; a quantifier's predicate, compiled into the function around it, is not read by the rule. tests/test_operation_row_1702.py holds both rules: 502 cells over each built-in effect's operation, put and throw bare and qualified, under the rows pure, one naming the effect, one naming another and one naming both (and, for a closure, an open row naming either), at a function's body, a let initialiser, an if arm, a match arm, a where helper's body, a handler's body for the effect and for another, a handler's clause, a closure inside a pure function, one naming the effect and one naming another, a closure inside a handler for the effect, and a closure with that handler written inside it, and 108 over a quantifier's predicate at each declared row under a function whose row is pure, names the effect or names both. 309 of the 610 cells are red at fa95873, each a refusal the base did not make or made elsewhere; the 227 accepted cells check with no diagnostic and verify with every obligation proved, the 38 accepted closures compile and run, and the 27 accepted quantifiers compile. The eight closure cells tests/test_lowering_boundary.py held accepted under <IO>, or refused at the function, are now refused at the call.
• A quantifier predicate whose parameter is a parameterised alias of Int or Nat reads the counter (#1506). Code generation bound the counter under the alias's head, Id for fn(@Id<Int> -> @Bool), while the body's @Id<Int>.0 looks itself up under Id<Int>, so the reference dangled and compile stopped at E699, in a body and in a contract alike; where the enclosing function had a parameter of the same type, the reference read that parameter instead, and forall(@Int, 3, fn(@Id<Int> -> @Bool) effects(pure) { @Id<Int>.0 < 3 }) answered false at a parameter of 7. The counter is bound under the name the checker binds the parameter by.
• A @Nat is never read as a negative number (#1504, #1590, #1592, #1628). Comparison, /, %, negation, nat_to_int and every renderer read a @Nat above 2^63 - 1 as the negative number its bits spell, so last_digit(18446744073709551615) returned -1, -@Nat.0 at 2^63 + 5 returned a positive number, and a @Nat passed to a built-in's @Int parameter, int_to_float(nat_to_int(@Nat.0)), returned -1.0 from a module recorded as checking it. No @Nat holds such a value now, and each of these is the @Int operation on the value it holds.
• A @Nat read at an @Int position is neither checked nor reinterpreted (#1546, #1586, #1589). A heterogeneous @Nat/@Int join built as a tuple component or produced by a handle returned u64.MAX as -1 with no check; a match arm's @Int binder guarded a @Nat that an earlier arm takes; and a @Nat above i64.MAX bound out of a tuple, a constructor pattern or an array trapped as a negative value. The widening is a no-op, so none of these sites has a check to miss or to misplace.
• Arithmetic with a literal operand runs at the signed width (#1543, #1591, #1593). A non-negative literal was a Nat and an if over literals took its else branch's type, so @Nat.0 + 1 at i64.MAX came back from an @Int slot as -2^63, @Nat.0 + (if @Bool.0 then { 0 - 1 } else { 0 }) trapped as an overflow at 5, and a @Nat sum holding a negative literal part was read as an @Int unchecked. The literal is an Int, the operation an @Int one checked against the i64 range, and each returns the true value or traps on overflow.
• A literal above i64.MAX is E149 wherever it is written (#1587). Each literal was range-checked against its own target, a Nat reaching 2^64 - 1, so 0 - 18446744073709551615 proved ensures(@Int.result < 0) and returned 1, and a literal pattern was checked against no range, so match @Int.0 { 9223372036854775808 -> 1, _ -> 0 } matched -2^63.
• parse_int refuses a numeral outside the Int range (#1698). It accumulated its digits unchecked, so parse_int("9223372036854775808") returned Ok(-9223372036854775808) and a 20-digit numeral a wrapped value. It now accumulates in the negative half of the i64 range, whose one bound serves both signs, and returns Err("out of range") past it, as parse_nat does; -9223372036854775808 still parses.
• A generic call's argument is checked where it narrows into a Nat instantiation (an instance of #1695). A type argument the expected @Nat fixes named a clone after the arguments' own types, whose parameters carried no @Nat check, and a built-in checked a type-variable parameter only as a map's value: vera run returned -3 from a @Nat function for id(0 - 3), option_unwrap_or(None, -3), result_unwrap_or(Err("e"), -3) and an array_fold accumulator of -3, each of which vera verify refuses, and an argument whose sign the verifier could not decide was counted as a run-time check the module did not hold (E541 under vera verify --reconcile). The argument is now checked where the verifier records it, in every user, prelude and built-in generic.