L3/12 — The trap and interrupt obligations

Edge: this file is the theorem the node carries — the proof that the trap/interrupt machinery refines the machine-mode ISA, part of the L3→L4 refinement edge. The trap/interrupt mechanism as an object is the node, 07.

Statement

Prove the trap and interrupt machinery refines the machine-mode spec: the imported Sail subset for everything standard. The mechanism itself — the CSRs, the CLINT/PLIC wiring, the synchronous surface — is the node, 07. The proof obligations:

  1. Trap-entry atomicity: mepc/mcause/mstatus update and the redirect to mtvec happen as one spec step — no observable intermediate, no partially-retired instruction underneath (08's disjunction stays clean).
  2. mret unstacks and redirects exactly per the spec.
  3. Preemption only at retirement boundaries: an instruction in flight is either retired or flushed, never half-committed — an invariant clause (09), and the reason the simulation cell needs no third case.
  4. Delivery gating: a trap step is taken exactly when mstatus.MIE ∧ (mip ∧ mie) ≠ 0 at a boundary (or a synchronous exception retires); no lost interrupts — the persistence of a source lives in the CLINT and the PLIC's gateway/pending machinery (a device-model property plus software's claim/complete discipline), hence a Sys(F)-level claim, split explicitly.
  5. Precise exceptions on the memory path: a faulting access (denied response, misaligned, PMP-refused) traps with the correct cause and no side effect — the lemma family where the memory system meets the trap machinery.
  6. Non-interference: with mstatus.MIE clear and no traps raised, behaviour is exactly the trap-free machine — the lemma that lets every other L3 file ignore this one, quarantining the risk.

Anchors against spec-side error

The imported half is anchored by the standard's own artifacts: the riscv-arch-test suite run against the imported model, and RVFI-style retirement checking for what "an interrupt retired correctly" observably means. The device half (CLINT/CLINT-compare semantics, PLIC claim/complete) is anchored by the de-facto and ratified documents those devices implement, formalised first and then diffed against the generated RTL. The working-software corpus — the ecosystem's own interrupt-handling code and test suites — is what the composed spec must make correct; extracting the interrupt-facing paths and running them against the draft spec is the standing check.

Obligations

  1. The six proof obligations above, non-interference (6) first.
  2. The delivery split stated precisely: core-side gating proved here, source-side persistence delegated to L5/03's CLINT/PLIC models by name.
  3. The software corpus: extract interrupt-facing code paths from the ecosystem's test programs; run each against the draft spec.

Effort

Months, but mostly standard months: the imported half rides the Sail model and existing compliance machinery, and the interrupt sources are standard devices with documents. The open-ended risk — spec fidelity for the small authored residue — is priced in the ledger as S3.