L4 — The ISA specification
Node — the ISA:
ISA = Sail-RV32(config, incl. machine mode) ⊕ authored residue ⊕ S4-choices(00–03) — the transition system L3's invariant refines into, and the core of L5'sSys(F). Edge up: none of its own — L3 carries the refinement up into this node, and L5 carries theISA ⊕ devices ⟹ Syscomposition out of it. A definition node — specification authoring, not proof; the place where being wrong is least detectable, because a wrong definition yields a true theorem about the wrong machine. Consumes: the RISC-V standard, the configuration record.
Background
An ISA — instruction set architecture — is the contract between hardware and software: the instructions, their encodings, and their exact effects on architectural state. This layer fixes that contract as a mathematical object, because L3's refinement theorem is only as meaningful as the spec it refines against. The object has three components with three different levels of trust: RISC-V's official formal model is imported — the base ISA and, because the shipped core implements the standard machine-mode trap machinery, the ratified machine-mode subset of the privileged architecture with it (00); the small pieces of behaviour that live outside the ratified model — the generated core's custom extension and the platform interrupt controllers' register conventions, chiefly — must be authored or imported from de-facto documents (01); and where the standard is deliberately loose, the choices this implementation embodies are recorded rather than silently assumed (02). A totality sweep (03) then makes the spec answer for all 2³² instruction words, not just the meaningful ones.
Statement
What L3's theorem is stated against: Sail-RV32(config) ⊕ authored residue ⊕ S4-choices ⊕ spec-UB clause — the last assigning the reserved encoding space unspecified behaviour (03) — its authored components carrying the three fidelity axioms — S2 (the official model's small residue, now covering the machine-mode subset as well as the base), S3 (the authored residue: the custom extension and anything else outside the ratified model), S4 (the recorded choices). It is not the top of the tower — the pad-level system spec is L5's — and the boundary test is portability: the same core in a different SoC keeps this layer's spec while L5's is replaced wholesale.
Subcomponents
| status | ||
|---|---|---|
| 00 | How RISC-V is structured (volumes, base + extension letters, formats, encoding space) and how Sail specifies it — with addi/beq worked; the machine-mode subset; S2 and the import path | weeks |
| 01 | S3 — the authored residue: the custom extension, the performance-counter event space, the debug exclusion; the anchor methodology against circularity | weeks; the thinking |
| 02 | S4 — the choice register: pick, record, flow down; mid-proof stalls become filing operations | days to seed; discipline thereafter |
| 03 | The encoding sweep: implemented ↔ Sail clauses, everything else ⟹ traps-correctly — across both the 32-bit space and the compressed 16-bit space | months of mechanised typing |
Interfaces
Consumes: the standard, sail-riscv, the configuration record (which derives the subset boundary), the RTL + generator sources + test software as S3's anchors. Exports: ISA to L3 (refinement target) and L5 (core of Sys); the partition of the encoding space to L3/10; the choice register to L3's lemmas.
Axioms introduced
S2 (Sail faithful — small: the model is the standard's official golden model; residue is fidelity to the ratified manuals plus the pinned translation path — now covering the machine-mode subset too), S3 (the authored residue is what was intended — unfalsifiable, anchored), S4 (the recorded choices are acceptable — legislative by nature). X4 lives in L5.
The layer's shape
Entropy sorted by kind: 00 receives the bulk for free (official golden model, structured encoding space — and, for this core, the trap machinery too), 03 turns the remaining width into independent SAT-shaped typing, and the thinking is deliberately concentrated into two small artifacts — 01's authored residue and 02's choices — because those are the two places an error is invisible downstream. The honest end statement this layer serves: not "the core is correct" but the device refines this specification, modulo these axioms — with unbounded proof capacity the axiom list is the achievement, which is why axioms.md precedes any proof.
The ISA is rightly silent about power: its reset section is the power-on hook (X ⊑ reset nondeterminism), prefix-closed small-step refinement is the power-off hook; everything else power-shaped is L5's epoch model. Resist adding power events here — the layering is doing its job.
Open problems
- Author the residue (01) — gates L3/07; the highest-risk specification work left in the layer.
- Seed and enforce the S4 register (02) before L3's proofs start.
- The Sail→prover translation's trust status, pinned and stated (00) — now including the privileged-subset clauses.
First experiments
- Import
sail-riscvat a pinned commit, carve the configuration's subset, and run the architectural compliance suite against the imported model (00) — the only handle on S2. - Draft the custom-extension residue from the generator source first, then diff against the emitted RTL's behaviour; log every discrepancy (01).
- Generate the encoding partition from the configuration record (03).
Effort
6–9 months. Small in proof content, disproportionate in consequence: an error here is invisible to every layer below and produces a true theorem about the wrong machine.
Reading
sail-riscv and the Sail language papers. The RISC-V unprivileged spec (Volume I) and the machine-mode chapters of the privileged spec (Volume II) — both short and readable, and 00's tour is a map into them. ARM's CHERI/Morello work — the best existing example of an ISA-level property proved against a shipping architecture spec.