L4/03 — Coverage: the encoding sweep and the cheap bulk
Background
A processor's decoder is not consulted only on the instructions the programmer meant to use. Every word that arrives from memory — a mistyped jump target landing in data, a corrupted image, a deliberately hostile input — goes through the same decode hardware, and the hardware will do something with it. An ISA therefore has to be a total specification: it must say what happens for all possible words, not just the meaningful ones. For the meaningless remainder the standard's answer is the illegal-instruction trap — the processor must recognise the word as invalid and transfer control to a handler, rather than executing whatever the decoder's don't-care logic happens to compute. A refinement claim that only covered the valid words would be false as stated: refinement quantifies over all executions, and executions containing garbage words exist.
This sounds like it demands 2³² proof obligations, and the reason it does not is worth understanding because it recurs everywhere in verification. The decoder does not treat words individually; it examines a few fields — the major opcode bits, the function-code bits — and the valid/invalid boundary is expressible as a modest set of regions of the encoding space, each region either matching one instruction's pattern or falling outside all of them. Checking a region is one query to a SAT solver ("does there exist a word in this region that decodes without raising the illegal flag?" — a question over a few dozen boolean variables, mechanical to answer). So the sweep is a few hundred solver queries, generated by a program, none requiring human thought.
That phrase — no human thought per case — is the point of this chapter's title. The project distinguishes obligations that are numerous but mechanical ("cheap bulk": generate, solve, count) from obligations that are few but deep (authoring the custom-extension spec, inventing the L3 invariant). Coverage is the model case of the first kind, and the chapter's closing advice is a useful heuristic for the whole book: the moment an individual coverage case starts to require judgment, it has been misfiled, and belongs with the thinking-dominated chapters instead.
Statement
The wide, shallow obligations that make ISA total over the instruction space: every encoding is either implemented (and matched to its Sail clause) or unimplemented (and proven to trap). Skip the second half and the refinement is simply false — a claim about all executions cannot ignore the words a program might contain.
The partition
From the configuration — rv32imac_zicsr_zifencei_zihpm_xrocket — the space partitions across two widths, because the C extension makes this a variable-length ISA:
implemented RV32I base ⊕ M (multiply/divide) ⊕ A (atomics: lr/sc, amo*)
⊕ ALL of C (the 16-bit quadrants 00/01/10, minus reserved holes)
⊕ Zicsr (csrr* against the implemented CSR set, incl. machine-mode,
PMP, counters, and the xrocket custom CSRs)
⊕ Zifencei ⊕ ecall / ebreak / mret / wfi
unimplemented F/D (no floating point), supervisor-mode CSRs (no S-mode),
reads of absent CSRs, reserved regions of both the 32-bit
space and the 16-bit quadrants
Each implemented encoding gets the decode-equivalence + execute lemma pair (L3/10, templated by 00's addi/beq example). Each unimplemented encoding gets traps-correctly: the decoder raises the illegal-instruction exception and the machine takes the imported spec's trap step — mcause/mtval included, per the S4 rows. Two subtleties the sweep must partition alongside opcode space: a csrrw to an absent CSR is a legal instruction encoding whose execution traps — CSR address space is part of the sweep — and the 16-bit space's reserved holes (including the all-zeros word, defined illegal by the standard precisely because erased memory decodes to it) are regions of their own.
The measured half is an obligation, not yet a result. The spec side comes from the official riscv-opcodes tables at a pinned commit, so the patterns rest on the standard's own machine-readable encodings, not hand transcription. The implementation side — the decoder's own legality cubes, extracted from the generated RTL and compared exactly against the spec patterns — is the checker to re-run against this core (scoreboard). Decoders routinely accept a few reserved words via minimisation don't-cares, which is why the partition is designed three-way, with the third class a deliberate piece of spec design:
implemented the spec patterns — matched to their Sail clauses
trapping words the decoder REJECTS — proven to take the illegal-instruction
trap step (a sweep against the measured rejected set)
spec-UB any reserved words the decoder ACCEPTS — the spec assigns them
UNSPECIFIED architectural behaviour; the measured set is
expected small, and the clause survives any size
Spec UB, and why it is safe to say. For the UB class the ISA transition relation simply permits any successor architectural state (a demonic havoc step); refinement on those words is then trivial — which is exactly the point: the theorem deliberately claims nothing about them, instead of claiming something false. What makes this honest rather than a cop-out is the layering: UB at the ISA layer is still bounded by every layer below it. The invariant I still holds (the machine stays a coherent pipeline), the bus guarantees still hold (no malformed transaction), retirement still happens within the measure's bound, the electrical envelope is untouched — no instruction is a halt-and-catch-fire. This is the same move as L5/05's operating-conditions clause one level down: out-of-spec behaviour is not "anything may happen" but "anything may happen to the architectural state, within a machine that keeps functioning and can be re-anchored by trap or reset." The practical corollary: an execution that never fetches a UB word gets the full correspondence theorem — and for a fixed image, "contains no UB word" is a checkable property of F, to be enforced by an image checker over the partition once the decoder extraction lands. The checker earns its result by discriminating rather than by always agreeing — it must distinguish a UB word (accepted-reserved) from an unimplemented word (trapping), which is the distinction the three-way partition exists to make.
Why this is the model case of cheap entropy
The implemented patterns and the unimplemented complement: high raw spec entropy, zero invariant entropy — each obligation is one SAT-shaped query, independent of all others, because L3's interlocks cut every cross-instruction dependency at the register file. A lot of typing, almost no thinking; the thinking concentrated in S3 (01) and S4 (02). Most of L4 has this character, and the layer's effort estimate is dominated by it.
The sweep is also where encoding-space structure pays: the partition is decided by major opcode and format fields, so the unimplemented half is a small set of regions, not 2³² cases. The custom fragment adds CSR addresses (and possibly custom opcodes — 01's enumeration settles which), handled as further rows of the same sweep.
Obligations
- Generate the partition — opcode regions across both widths and CSR addresses — from the configuration record; publish it as the single source both L3/10 and the compliance harness consume.
- The decoder extraction and exact comparison against the spec patterns (the re-anchored checker; any accepted-reserved words land in the spec-UB class and the findings).
- The traps-correctly sweep, mechanised (regions, not words).
- The absent-CSR cases (F/D, S-mode, unimplemented counters) as explicit rows of the sweep.
Effort
Months of mechanised typing once L3/10's harness exists; near-zero marginal thought per encoding — by design, and worth preserving: any coverage case that starts requiring thought belongs in 01 or 02 instead.