v0.2.4

Highlights

• A host operation is one row of the built-in registry, and every host binds from it. vera/builtins.py holds each built-in function as one record and each host import as one row naming its family and the WASI worlds that implement it, and the checker, code generation's dispatch and import declarations, the Python host's binders, the browser runtime's roster of imports, the WASI target's refusals and spec §9's signature tables read it. Adding a host operation is its record or effect operation, one HostImport row and its implementation in each host, then python scripts/render_lists.py --write (#1713, #1717)
• Map and Set are persistent hash tries in the module's own code. Each operation is a function the module carries, and an update copies the branches on its key's path and shares every other block with the collection it was given, so the fold of map_insert over 10,000 keys that took 50.4 s natively and 16.0 s in the browser runtime executes in 41 ms natively and runs in 0.04 s in the browser harness. No host implements a map or a set, both WASI worlds run every instance, and the order is insertion order on every host; an array of Bool or Byte that set_to_array, map_keys or map_values returns holds the elements that went in, and json_parse builds a document of any width (#1737)
• Bytes in, out and through. IO.read_bytes and IO.write_bytes move a file's bytes unchanged, string_to_bytes and bytes_to_string convert between a String and its UTF-8 bytes, and base64_encode_bytes and base64_decode_bytes are Base64 over an Array<Byte>; the four conversions are compiled in place, so every host runs the same code for them (#1734)
• One fold over the AST, and the walker-coverage gate retired. vera/fold.py holds one traversal, one dispatch table that refuses construction unless it names every Expr class, and one binder-aware scope walk, and the fourteen walkers the gate guarded are on it, code generation's expression translation, the checker's synthesis, the SMT translation and the verifier's walks among them, so a node class added to vera/ast.py is traversed by construction. The scope walk reads a destructuring let, so a closure whose body destructures a tuple compiles. Compiled WAT is byte-identical over the corpus (#1714, #1720, #1726)
• Mutation testing in CI, over a pull request's diff and over all of vera/ by night. On a pull request that changes the compiler, mutmut mutates the functions the diff changes and the job fails on a survivor; each night seven jobs measure a slice of the 2,371 functions mutmut mutates in vera/, carrying the state from night to night until every mutant is decided (#1727, #1735, #1738)
• A call's facts are assumed only where its arguments fit the callee's parameters (breaking). The verifier assumed a callee's ensures and refined return whether or not the call's arguments fit its parameters, and took them as premises of the arguments' own obligations, so nat_to_int(nat_id(@Int.0)) proved its argument's narrowing into @Nat and vera run trapped on -1. A call whose argument's narrowing rested on the callee's postcondition now fails vera verify with E503 (E505 for a refined parameter), as let @Nat = @Int.0 does, and the fix is a requires on the caller or an enclosing branch; such programs trapped before and trap now. A proof that used a callee's postcondition where the verifier holds no fact for an argument, an Array<Nat> element or a State<T> read passed to a @Nat parameter, is refused (E500) (#1715)
• A destructuring let is checked as the constructor pattern it names. let Tuple<@Int, @String> = Tuple(1, 2) passed check and verify and read the integer 2 as a string; a destructure is now held to the rules of its one-arm match (E320, E314, E321, E311, E313) and each binding to a let binding's (E170) (#1721)
• The collector marks a heap of any width. A collection with more than 16,384 values pending at once trapped in $gc_collect, so a 20,000-element Array<String> died inside array_map; a push that finds the mark worklist full is now dropped, and the objects it was dropped from are scanned again once the worklist empties (#1722)

Added

• A nightly mutation sweep measures all of vera/, a slice a night (#795; scripts/mutate_sweep.py, tests/test_mutate_sweep.py, .github/workflows/mutation-nightly.yml). mutmut makes about 110,000 mutants of the 2,371 functions it mutates in vera/, and no single run holds them: the local marathon deadlocked four times under Python 3.14. Each night seven jobs plan the same night from the state the last night left: the undecided work in the tree's order, in one bin a job of a 4.5 h budget, a function whose mutant count is known split across bins by its mutants' numbers and one not yet generated taken whole. Each job runs its bin through the diff lane's machinery, in a scratch tree narrowed to the bin's functions, with the whole tree in mutmut's copy and every test file the lane's rule admits as the oracle. A stitch job folds the slices into the state, kept as the mutation-sweep-state artifact for 90 days, keyed by each function's code hash and its pragma: no mutate lines, so a function that changes is measured again. The state is carried only from the workflow's own completed runs on this repository's main, started by the schedule or a dispatch, never from an artifact of the same name another run uploaded, and every field is checked before it is used; the engine is pinned, so a new mutmut version, which starts every function afresh, arrives by a reviewed pull request. When every function's every mutant is decided, the cycle closes, and python scripts/mutate_sweep.py summary writes its mutation-summary.csv and the README badge's mutation.json for a pull request to commit. A scheduled night that decides nothing, or whose engine or lane fails, files or updates one tracking issue (mutation-sweep); survivors never do.
  • scripts/mutate_diff.py's drop of a test that fails inside mutmut's copy is shared with the sweep (run_dropping), and its config rewrite can replace also_copy.
• Bytes in, out and through: IO.read_bytes, IO.write_bytes, string_to_bytes, bytes_to_string, base64_encode_bytes and base64_decode_bytes (#1711). A file whose bytes are not UTF-8 could not be read, nothing wrote bytes, and base64_decode returned a String. IO.read_bytes : String -> Result<Array<Byte>, String> and IO.write_bytes : String, Array<Byte> -> Result<Unit, String> move a file's bytes unchanged, with no decoding and no newline translation, on the native host and in the WASI command world; the browser runtime refuses both as it refuses IO.read_file, and --target wasi-p2 --world server refuses both at compile, naming wasi:filesystem. string_to_bytes gives a string's UTF-8 bytes, and bytes_to_string decodes bytes to a string, with Err("invalid UTF-8 at byte N") naming the offset of the first byte of the first sequence that is not well-formed UTF-8. base64_encode_bytes and base64_decode_bytes are RFC 4648 Base64 over Array<Byte>. The four conversions are compiled in place, so the Python host, the browser runtime and both WASI worlds run the same code for them. An Array<Byte> holds one byte per element in generated code, so a 3,000,000-byte file read whole is a 3,000,000-byte array.
• Mutation testing runs over a pull request's diff, in CI (scripts/mutate_diff.py, tests/test_mutate_diff.py, .github/workflows/mutation-diff.yml). On a pull request that changes a vera/**/*.py file or one of those three, mutmut mutates the functions the diff changes, a function counting as changed when its code (its ast, docstrings set aside) differs from the merge base's or it is new. It runs in a scratch tree of the head commit where every other function of a changed file carries # pragma: no mutate block, so mutmut generates the diff's mutants alone, and its oracle is the [tool.mutmut] test selection plus the pull request's own changed test files that reach the compiler in process. The job summary has a row per changed function and the survivors' mutmut show diffs, and the JSON record is an artifact. The job fails on a survivor (exit 1) and on a run that its 2,400 s budget, the engine, an undecided mutant or a mutant it cannot place stops short (exit 2), and it is not a required check.
  • [tool.mutmut] copies scripts/ and AGENTS.md into mutmut's copy of the tree and deselects the two tests that parse vera/verifier.py's own text. 21 of the selection's 6,554 tests failed inside the copy with no mutant active, and mutmut's stats pass, which runs the selection with -x, stopped every run at the first of them.

Changed

• The hosts bind a module's imports from the built-in registry, and spec §9's signature tables are rendered from it (#735). The Python host binds exactly the vera imports a module declares, each through the binder of its registry row's family (HOST_BINDERS in vera/codegen/api.py), and refuses an import no row declares, or one no binder defines, with a HostBindingError naming the row; CompileResult no longer carries the thirteen per-family *_ops_used sets, and code generation records the host imports a module's emitted code calls in one set, where it kept one per family. A call code generation never emits, under an assume or in a function it drops (E602), declares no import, a State cell's apart (its handler or its effect row declares it), so the WASI target compiles a module whose one call of a family is such a call, where it refused the module. The browser runtime holds every import to a roster of the registry's 83 rows, which scripts/render_lists.py renders into vera/browser/runtime.mjs, and refuses one no row declares or the runtime does not bind. Each row names the WASI worlds whose component implements it; the WASI target's refusal lists are derived from them, each world refuses a declared import whose row does not name it, and a refusal lists the imports the module declares, its families in the registry's order. The Signature cells of spec §9's sixteen signature tables are rendered from the records and the effects' operations in one notation, which moves 40 cells' notation and no type, and vera/monomorphize.py's two built-in return tables are read from the records. Compiled WAT is identical to the base's over the corpus.
• Map and Set are persistent hash tries in the module's own code, and their operations leave the hosts (#1676). A map or a set was a bucket every host decoded into a dictionary and encoded again on each copy-on-write operation, so an operation cost the collection's size and a fold of map_insert over n keys cost n². It is now a trie of 32-way branches in the module's heap, one branch for each five bits of a key's hash, and each of the fourteen operations is a function the module carries, generated for the key, value and element representations the program uses (vera/wasm/hamt.py). An update copies the branches on its key's path, at most thirteen, and shares every other block with the collection it was given, which it leaves as it was. The fold of map_insert over 10,000 keys that took 50.4 s natively and 16.0 s in the browser runtime executes in 41 ms natively and runs in 0.04 s in the browser harness; 100,000 keys take 1.75 s.
  • The order is insertion order for both, as spec §9.7.1 already promised a JObject's members: map_keys, map_values and set_to_array read a key inserted again at its first position, and a removed key loses its position. Keys compare by SameValueZero, a Float64 key stored canonical (-0.0 as 0.0, every NaN as one), and a String key by content.
  • No host implements a map or a set: vera/runtime/map.py, set.py and collections.py, the bucket codec in vera/runtime/heap.py, the browser runtime's map and set bindings and the WASI server world's in-guest map operations are deleted, with the registry's fourteen map_* and set_* host-import rows and the map and set families. The JSON and HTML hosts and the vera serve driver build a Map<String, V> with one call of the module's exported map_from_arrays$ks_v<t> and read one through map_keys$ks and map_values$v<t>, and so does the WASI server world's adapter for a Request's and a Response's headers.
  • A String key's hash is unseeded FNV-1a through a bijective mixer (spec §9.4.3), so String keys with equal 64-bit FNV-1a values share one collision node, which each operation searches and copies whole: a program that builds a Map<String, _> from keys an adversary chooses pays O(n) per insert on keys chosen to collide, 4,000 of them taking 1.3 s natively against 10 ms (#1736). The native host's dictionary hashed a String key with Python's per-process SipHash seed.
  • Both WASI worlds run every Map and Set instance, where the cli world refused both families and the server world every instance but Map<String, String>.
  • A module whose only wrapped values were maps and sets no longer carries the 64 KiB wrapper table, nor does a JSON or HTML module: the table holds Decimal values and pending async requests.
  • The scorecard's host built-ins hand-mirrored across hosts fall from 53 × 2, plus WASI's 10 map operations, to 39 × 2, plus none.
• A built-in function is one record in the built-in registry, vera/builtins.py, which the checker, code generation and vera builtins read (#735). Each of the 164 is a BuiltinSpec: its signature, which TypeEnv registers as it did; its since; its lowering, by an emitter of WasmContext written in place (88), through a host import (53) or as a prelude body (23); and the domain of string_char_code, from which vera/builtin_domains.py now derives its table. _translate_call lowers a built-in through one lookup of its record, in the argument convention its emitter takes, where it tested the call against 135 branches. TypeEnv's 164 registrations, the eight host-import family sets of vera/codegen/compilability.py and each built-in's version, which vera/_since.py held, are read from the records. Every (import "vera" ...) line a module declares is rendered from the registry's 83 rows over 18 families, the Map, Set and Decimal ones included, whose signatures their emitters wrote, so code generation writes each host import's WAT signature once, in its row. Compiled WAT, vera check --json and vera verify --json are identical to the base's over the examples, the conformance programs, the probes, the documentation's blocks and a call to every built-in, and vera builtins --json is byte-identical. tests/test_builtin_registry.py holds every record to the checker's arity, its emitter, the imports a call to it declares, and the hosts that bind them.
• One traversal, one dispatch and one scope walk over the AST, in vera/fold.py. children() reads a node's fields, in declaration order and a handle in evaluation order (its state, its body, its clauses), so a node class added to vera/ast.py is traversed by construction; dispatch() builds a table keyed by expression class that refuses construction unless it names every Expr class, so a new class fails the import of every module that builds a fold.dispatch table; and scoped() yields each node with the slots in scope, the binder positions read from vera/binders.py. Eight of the fourteen walkers the walker-coverage gate guarded port to it: code generation's expression translation, its void and WAT-type predicates and its Vera-type walk, the checker's synthesis and its two SQL provenance resolvers dispatch through tables, and the closure free-variable walk is the scope walk. WAT is byte-identical over the corpus.
• The verifier's @Nat-binding walk and code generation's two compilability pre-scans are on vera/fold.py, the last of the walkers the walker-coverage gate guarded. _walk_for_nat_binding_obligations is a context walk: each class whose arm obligates a binding site is a step that obligates it where the recursive walk did, between the children it walks, and every other class reads its children on its own path, so a class with children that no arm names is walked rather than passed over. A handler clause's with update is obligated against its handler's cell between the clause's body and the update, and the handled effect's name is held over the handled body alone, as before. The pre-scans, _scan_io_ops and _scan_expr_for_handlers, are the fold's traversal, which meets a handler's body before its clauses where the hand walks met the clauses first: a handler whose clause and body each hold the first handler of a State or Exn family declares the body's family first, E607 and E612 name the body's cell or payload when the clause holds one too, and an E618 on a closure in each is reported for the body's first, the order E617 already had. Verdicts and obligations are identical over the corpus, and so is WAT.
• The SMT layer's translation and two of the verifier's walks are on vera/fold.py. SmtContext.translate_expr() dispatches through a fold.dispatch table, so a new Expr class fails the import of vera.smt until it has an arm. fold.contexts() is a context walk: it yields every node with the context a consumer's step gives it, asks the step for each child's context only once the previous child's subtree has been visited, and refuses a step that leaves a child out. The verifier's decreases walk and its §6.4.3 primitive-operation walk are context walks, each class's arm a step that runs its work where the recursive walk ran it, so a class with children that no arm names is walked rather than passed over. Verdicts, obligations and WAT are identical over the corpus.

Removed

• The walker-coverage gate (scripts/check_walker_coverage.py, the walker-coverage hook and its CI step). It held a # WALKER_COVERAGE: checklist comment on each hand-written walker over Expr to every subclass, which checked that each class was named rather than that the walk reached it; every walker it guarded is on vera/fold.py, whose traversal reaches every field by construction. Its tests go with it, and the cells of tests/test_walker_defensive_branches_597.py that pin the ported walkers' behaviour move into tests/test_expr_fold.py.

Fixed

• The collector marks a heap of any width: a full mark worklist no longer traps (#1510). $gc_collect marked through a worklist of 16,384 entries, and a push that found it full executed unreachable, so a correct program died in the collector whenever a collection ran with more values pending at once than that, in a heap it had already allocated. The issue's 20,000-element Array<String> trapped inside array_map, and under ordinary collection so did an Array<String> of 16,385 strings, a list of a user data 16,384 cells long, an array of 16,385 boxed closures each capturing a String, and a string-keyed Map built by map_insert from 596 keys, natively, in the browser runtime and under --target wasi-p2. A child push that finds the worklist full is now dropped and the object being scanned recorded as dirty: the lowest dirty object with the word its push was dropped at, and the highest. Once the worklist empties, that range is walked along the allocation chain and each marked object in it scanned again, until a drain drops nothing. A walk that fills the worklist stops there, and the object and word it stopped at become the resume point: a later walk resumes that object at that word. A drop recorded below it lowers the range's bottom but not the resume point, and a walk jumps from the highest such drop straight to the object it resumes, so while the drops below the resume object lie together, a collection's walks visit each word and header of their range at most once. Against a worklist that drops nothing, the rescan adds 1.56% to the collector's instructions for an Array<String> of 100,000 strings, whose elements push nothing of their own. For records of two String values each, it adds 46% and 55% at 50,000 and 200,000 records in an array built by array_map (34% and 36% of the whole program), and 47%, 56% and 55% at 150,000, 600,000 and 1,200,000 records joined by a three-way array_concat into an array that lies above them (34%, 28% and 19%). The worklist bounds the collector's memory, not the heap it marks, and the memory layout is unchanged. The seed's push loses its capacity test, since it pushes at most one entry per shadow-stack root and the 4,096 roots always fit, and code generation refuses a layout whose worklist is smaller than its shadow stack. The unreachable trap's Fix paragraph names four causes; the mark worklist is no longer one.
• A destructuring let is checked as the constructor pattern it names (#1545). The checker bound each type a destructure writes as written and compared none of them with the value, so let Tuple<@Int, @String> = Tuple(1, 2); passed vera check and vera verify and @String.0 read the integer 2 as a string; nor did it read the head, so let Other<@Int, @Int> = Pair(1, 2), let Some<@Int> = None, let Tuple<@Int, @String> = Tuple(1, "a", true) and let Tuple<@Int, @Int> = 5 checked clean and ran on whatever the bindings' layout read, or failed to load. A destructure is now held to the rules of its one-arm match, through the functions that decide them for the arm, and each binding to a let binding's: the head names the value's type, by its name or an alias of it, or one of its constructors (E320 for neither, E314 for another type's, and for Tuple over a tuple of another width), a data constructor has one binding per field (E321), a type with another constructor is taken apart by a match (E311), a type no constructor builds, a type parameter's among them, is not destructured (E313), and each component fits its binding as a call argument fits its parameter (E170), so a @Nat component widens into an @Int binding and an @Int one narrows into a @Nat or a refined binding with the verifier's obligation, as in a plain let. The value's type is the one it synthesizes, never the bindings', so an if whose branches build Tuple(1, 2) is refused at a @String binding too. The checker reads the head as the verifier already did. tests/test_destructure_checked_against_source_1545.py holds the rule over 828 cells: seven heads, six value forms, seven relations of a component to its binding (four for the prelude's Response, which declares no Nat or refined field) and three arities.
• A call's facts are assumed only where its arguments fit the callee's parameters (#1706). The verifier modelled a call to a user function by assuming the callee's ensures, and its refined return's predicate, about a fresh result under the path's conditions alone, and it discharged the obligation each argument owes its parameter after the body was translated, with those facts among its premises. So nat_to_int(nat_id(@Int.0)), with nat_id(@Nat -> @Nat) ensuring @Nat.result == @Nat.0, recorded the argument's narrowing into @Nat verified at Tier 1 from nat_id's own ret == @Int.0 and ret >= 0, and vera run trapped on -1 (Negative value bound into a @Nat slot). The same facts discharged a refined parameter's predicate, a refinement written inside the formal (an Option<PosInt> payload, through an ensures that names it or through a match on the parameter in the callee's ensures or requires, whose binder facts were assumed of the argument, and which in a requires discharged the precondition it was part of), a constructor field inside the argument, a let narrowing of the value the call then receives, and a let whose @Nat slot is itself the argument. The callee's facts are now assumed only under what its own verification assumed of its parameters, stated over the actual arguments: >= 0 for a @Nat, a refinement's predicate, and the refinements written inside a parameter's type, for every argument whether or not it narrows at the call, and the facts a match in the callee's requires or ensures assumes about its parameter are under the same condition. A call's result now carries the refinements written inside its return type beside its head refinement, through the disclosure gate, since a result was the one producer of such a value the verifier held no fact for: consume(mk(x)), with mk returning Option<PosInt>, keeps consume's postcondition where mk proves its payload. A program whose call-argument narrowing was recorded verified only through the callee's postcondition now fails vera verify with E503 (E505 for a refined parameter) at the call, as let @Nat = @Int.0 already does, and the fix is a requires on the caller or an enclosing branch; the runtime behaviour of such programs is unchanged (they trapped before and trap now). A proof after the call that uses the callee's postcondition keeps it wherever the arguments are shown to fit, and loses it where the verifier holds no fact for an argument the types say fits: an Array<Nat> element or a State<T> read's value passed to a @Nat parameter no longer carries the callee's postcondition with it, so a proof that rested on it is refused (E500) where it had rested on the same leak. Spec §6.4.2 states the rule. tests/test_call_facts_after_obligations_1706.py holds the class: 400 cells over the formal (@Nat, a refinement of @Int, a refinement of @Nat, a refinement inside Option<PosInt>), the callee's facts (an ensures equating result and parameter, one bounding the parameter below by the result, one bounding it above, a refined return of another type related to the parameter, and ensures(true)), the argument (the bare parameter, an expression over it, the parameter under a proving requires, under a proving if) and the call's position (the return expression, a let value, an outer call's argument, an if condition, a match arm), 115 of them red at 313c04d; 20 cells crossing the argument and the position for a callee whose requires matches on its parameter, 5 of them red; and 25 tests for the issue's program, the shapes beside it, what the guard must not move and one killer per part of the guard, 17 of them red at 313c04d. The examples/ programs, the tests/conformance/ programs, the probes and the documentation blocks verify exactly as before.
• An array of Bool or Byte that set_to_array, map_keys or map_values returns holds the elements that went in (#1729). The hosts wrote such an array in four-byte cells where generated code reads one byte an element, so set_to_array of the Set<Byte> {7, 200, 3} printed 200 0 0 natively and 7 0 0 in the browser, and map_keys of a Map<Bool, Int> printed false false. The arrays are written by the module's own code now, in the cells generated code reads.
• json_parse builds a document of any width on both hosts (#1733). The native host kept every string's, array's and object's roots on the shadow stack until the whole document was built, so a document past about 4,090 of them overflowed it (#692: host shadow-stack overflow): the widest that parsed was 4,091 members for an object of numbers and for an array of strings or of arrays, 2,045 for an object of strings or of arrays and for an array of objects, and 1,363 for an object of objects, and only an array of numbers had no limit. Each string, array and object is now built in a shadow-stack window of its own and holds no root once it is written, so every one of those shapes parses at 20,000 members. The browser runtime rooted each member of an object until the object was built, so an object of 4,100 members overflowed there (GC shadow stack overflow); it builds the object from two rooted arrays now, and every shape parses at 10,000 members.
• A closure whose body destructures a tuple compiles. The closure's free-variable walk read no destructuring let: it never walked the source and never counted the bindings, so let Tuple<@Int, @Int> = …; in a closure body made a later reference look like a capture the enclosing scope does not hold, and the function holding the closure was dropped ("unsupported expressions") with every caller of it. The walk is now vera/fold.py's scope walk, which reads the destructure where vera/binders.py lists it.
• The mutation lane no longer stops on a test that fails inside mutmut's copy (scripts/mutate_diff.py). The stats pass runs the selection with -x inside mutmut's copy of the tree, where each mutant is a copy of its function, so test_checker_errors.py's collision gate, which runs scripts/check_diagnostic_fields.py over vera/, read a mutated vera/checker/core.py as emitting E121 from 198 sites and failed with no mutant active: a pull request that changed an error-emitting checker function got exit 2 before any mutant ran. [tool.mutmut] deselects that test beside the two that parse vera/verifier.py's text, and the lane drops any other test that stops its stats pass or its clean run that way, runs again, and names it under the table and in the record's dropped_tests.
  • A test that starts a Python or vera process is skipped inside the copy (tests/mutation_oracle.py, a pytest plugin [tool.mutmut] loads) and listed in the record's subprocess_tests. Each mutated module there holds a copy of a mutated function for each of its mutants, so every process compiled them afresh (a mutated TypeEnv._register_builtins makes vera/environment.py 33.6 MB where it is 49 KB, and vera check of a one-line program took 2.3 s against 0.4 s), and on a pull request that changed _register_builtins and execute a CLI test reached its 120 s timeout in the stats pass and stopped the run; the process records nothing for the stats pass, so the test was never a mutant's oracle. The plugin also takes the skipped test out of mutmut's record of the tests that reach each function, which the stats pass writes at each test's teardown whatever its outcome, so a function only such tests reach has its mutants no tests, not survivors, even when a test called it before starting its process.
• A Set enumerates its elements in insertion order on every host and in every run. The native host enumerated a set in Python's set order, which for a Set<String> changes from one process to the next with Python's string hashing (three runs, three orders) and for a Set<Int> is neither insertion nor numeric order (40, 3, 17, 9 read back as 40, 17, 3, 9), while the browser runtime kept insertion order.
• A NaN key inserted again keeps its position. The native host moved it to the end of map_keys, so a map built by inserting NaN, 1.0 and NaN read back 1.0, NaN there and NaN, 1.0 in the browser.
• A -0.0 key reads back as 0.0 on every host. -0.0 and 0.0 were one key on both hosts, and the native host kept whichever came first, so map_keys of a map whose first zero key was -0.0 read back -0.0 there and 0.0 in the browser.
• The landing page's hand-kept counts match the tree. docs/index.html's status paragraph said 164 built-in functions, a 269-program conformance suite and 43 worked examples, where the tree holds 168, 272 and 44, the counts docs/index.md states; it states 168, 272 and 44 now, and scripts/check_site_assets.py compares the three between docs/index.html and docs/index.md, so the hand-kept copy cannot drift from the one scripts/build_site.py measures.