The question these tests answer is one-directional:

is what the real hardware did an execution our model ALLOWS?

so a test only has to EXHIBIT one model execution matching what QEMU produced. That is a computation, not a proof: no WP, no invariants, no Iris. A test is a vm_cast_no_checkd equation between a projection of the model's reached state and a literal captured from QEMU. Nothing here is restricted to what the xv6 driver's proofs assume -- a test may program the queue illegally, and the only question is whether the model has a run that matches.

The suite has one set of test cases (tests/*.S). A case declares, in its own vtest: directive, which platforms it is meaningful on. Executing a case on a platform produces a test run, so a case yields zero or more runs (QEMU, the VisionFive 2 board, the CVA6 RTL) -- and every run, whichever platform it came from, is the same kind of object and is judged by the same theorem.

/* vtest: platforms=qemu  builder=multi  budget=4000  tick=1
          proj=fields:24,48 */

Every knob defaults, so most cases declare nothing:

There is no runner-side skip list. A profile that excluded an area would be hiding a fact about a case inside a fact about a machine, and the two had already drifted apart.

vtest-rocq/VRun.v. A run is a TEST_RUN module; the theorem is stated once and parametrically:

Definition run_passes observed outcome : Prop :=
  match outcome with
  | MNoStep         => True                              (* a pass *)
  | MDone exhibited => forall o, o ∈ observed -> o ∈ exhibited
  | MUnknown | MBudget => False
  end.

Module Type TEST_PASSES (R : TEST_RUN).
  Axiom passes : run_passes R.observed R.outcome.
End TEST_PASSES.

A run passes when the model exhibits every outcome the platform observed (if the platform showed several, because the hardware itself has more than one legal execution, the model must have each), or when the model is STUCK -- which is a pass too, because a state the model cannot step from is a state no proof over the model can reach. It costs REACH, not soundness.

Stuck means MNoStep, not VStuck. exec also declines on Interface.Choose, where the relation DOES have transitions and only the interpreter will not pick one, and "our proofs can never run into this case" is false there. VExecStuck.exec_r_no_step is what makes MNoStep mean it; EChoice becomes MUnknown, which is a gap, not a pass.

outcome is COMPUTED by the SingleHart functor, not asserted by the generated module, so a run cannot claim a model execution it does not have. Every proof is then the same two tactics:

(* QEMU/CoreSmokePass.v *)
Module CoreSmokePass <: TEST_PASSES CoreSmoke.
  Lemma passes : run_passes CoreSmoke.observed CoreSmoke.outcome.
  Proof. apply run_passes_b_sound. vm_cast_no_check (eq_refl true). Qed.
End CoreSmokePass.

make vtest-table     print it
make vtest-passes    ATTEMPT every run's proof (against `_CoqProject.all`,
                     so a red one can still be tried), then rewrite the
                     green `_CoqProject` from what produced a `.vo`
make vtest-runs      rebuild the run modules from the checked-in captures

Everything in it is read off the tree -- the case's directive, whether a run module exists, whether a TEST_PASSES instantiation compiles -- so it cannot drift: the table reads the .vo, never _CoqProject membership -- membership is only an ASSERTION that a proof holds, and a table that read it would be reporting its own bookkeeping back.

A run with no passing proof is a FINDING, not a broken build. It is absent from _CoqProject, so CI stays green while the table's row for it says no proof; the findings table below says what the divergence is.

abi.h              THE ABI: regions, result layout, done handshake  (read first)
vtest.S            prologue/epilogue every test image uses
tests/<area>_<name>.S   one test program (a `vtest:` directive in it
                        carries the repeat count and backend configs)
vtest.py           builds the image, runs QEMU, captures, generates Rocq,
                   and prints THE RUN TABLE (`--check` is CI's verdict)
board.py           the same, against a real board over JTAG

../../vtest-rocq/  the model side: harness, then per (case, platform)
                   <Case><Platform>Run.v   what was run, what came back
                   <Case><Platform>Pass.v  its VRun.TEST_PASSES instance

A test is <area>_<name>, and the Rocq side is the same in CamelCase: tests/disk_rw.S -> vtest-rocq/DiskRw.v + the generated DiskRwGen.v, whose definitions are disk_rw_text, disk_rw_qemu_result, ... Areas:

The area is what the test is ABOUT, not everything it touches. disk_intr drives the PLIC and reads mip, but it exists to check the DISK's interrupt path, so it is a disk test. A plic_ test would be one whose subject is the controller -- two sources competing, a threshold that masks one, a claim while another is pending.

make vtest         regenerate from QEMU (needs qemu-system-riscv64 + the
                   riscv64 toolchain), then check the model against it
make vtest-check   check the model against the CHECKED-IN captures only
                   (no QEMU, no toolchain), stopping at the first red test
make vtest-check-ci  the same captures, but compile EVERY test (-k) and
                   report the per-test result -- this is what CI runs,
                   on every push

vtest-check is deliberately outside make proofs: a red test must not break the proof build. It needs only the ~20-file dependency cone of RiscvExec + DevModel, not all of iris/.

.github/workflows/ci.yml runs vtest-check-ci after the proof build -- against the CHECKED-IN captures, so CI never runs QEMU and never looks for new hardware behaviours; it re-checks that the executions already recorded from real hardware are still executions the model ADMITS.

Every test must pass, and a red one fails the job. There is no list of expected reds and no need for one: a known divergence is pinned on BOTH sides and proved unequal (see Recording a divergence), so it is green today and goes red exactly when the model moves -- the findings are theorems about the disagreement, not failures.

What the step adds over a plain vtest-check is the REPORT: everything is compiled (-k) before the verdict, so one red run does not hide the rest, and vtest.py table --format md puts THE RUN TABLE in the run's step summary. There is no second reporter: a run is listed in _CoqProject exactly when its proof holds, so the green set and the table's "pass" column are the same fact, read from the same .vo. --check fails the step when a listed file has none. vtest-check-ci deletes the .vo first, because a failed recompile leaves the previous one in place and a red run would otherwise be reported green off the last build.

vtest.py gen --hart 1 core_hart core_regs_gpr ...

Every capture in this suite was of a program on hart 0 until 2026-08-29, because QEMU boots hart 0 and -smp 1 is the rule. --hart N builds the same source with PRIMARY_HART=N, runs it under -smp N+1, and writes <Name>Hart<N>Gen.v with its own <name>_hartN_ definitions and a <name>_hartN_primary_hart. The model side runs it with VTest.start_hart, which is a legal schedule for exactly the reason a hart-0-only schedule is.

IT IS A DIFFERENT IMAGE, not a different schedule, and that is the one thing to keep in mind. vtest.S's prologue branches primary-vs-AP on the hart id and biases every hart's stack slot by PRIMARY_HART, so the primary is slot 0 whichever hart it is; under #if PRIMARY_HART != 0 that costs one extra instruction, which is why ra moves by 4 between the two captures. A hart-0 capture is byte-identical to what it always was.

WHY IT IS WORTH DOING. ColdBoot.cold_regs takes the hart id as an argument, and the boot chain does exactly two things with it: it stores it, so csrr mhartid reads it, and it copies it into a0. Those two claims are what make csrr mhartid the right way for a program to tell harts apart -- VConc.g0_of's header rests on them, and so does the whole multi-hart harness -- and no hart-0 test in the tree can check either of them, since on hart 0 both values are 0 and a model that ignored the argument entirely would pass.

What the hart-1 captures established, all of it new:

core_regs_ctr has no hart-1 capture on purpose: its fields are the cycle and instruction counters, which differ between two runs on the SAME hart, so a cross-hart comparison would say nothing. core_regs_fpr has none because it traps by design and never publishes a result.

By default a fault ends a run: mtvec is 0, the pc goes there, the fetch at an undeclared address faults again, and the machine trap-loops forever (see the rules below). That is fine when the trap is the ANSWER -- CoreRegsFpr.v pins the pc at two step counts and reads the story out of mcause/mepc/ mtval. It is useless when a trap is something to STEP OVER, for two reasons:

1. The loop destroys the evidence. The second trap overwrites mcause, mepc and mtval with its own. Measured on the board: core_regs_mcsr reported mcause=1 mepc=0 mtval=0, which says nothing; catching the FIRST trap with a hardware breakpoint at 0 gave mcause=2 mepc=0x8000008c mtval=0x30a022f3, i.e. csrr menvcfg, which says everything.
2. One trap ends the run, so a program can only ever report its first failure. A probe that wants to ask forty questions gets one answer.

trap.S is an M-mode handler that records the trap and resumes past the faulting instruction. A test #includes it after its body and points mtvec at _vtest_trap. It is not in vtest.S, because putting it there would add bytes to all 60 images to serve the two tests that want it. Its contract is in its header and a test using it must obey all four points -- in particular t0 and t1 are clobbered by any trap and it advances mepc by 4, so such a test needs .option norvc of its own.

Reading a CSR over JTAG is not the same question as executing csrr. All twenty of core_regs_mcsr's CSRs read fine through OpenOCD on the U74 -- menvcfg included, answering 0 -- while the hart refuses to execute a read of it. The debug module can report a value for a register the machine will not let an instruction touch, so only a csrr in the image measures what a kernel would see. This is why the probe below exists at all.

core_csrprobe (both machines) and core_csrwide (QEMU only, marked machines=qemu in its vtest: directive) split the question in two, because the model cannot be asked the second half -- see finding 32.

The control is load-bearing. Without it, a run in which the handler was never reached is indistinguishable from one in which nothing trapped -- every entry would be 0 either way. It is also the only place the MODEL's trap machinery runs in core_csrprobe, since the model refuses none of the 36, so it is what establishes that the model takes the trap, runs the handler and returns through mret correctly.

The machine has two 16550s (DevModel.uart_id), and every observation channel is indexed by port: serial_of and a run's o_uart are one wire per port in enum uart_id order, and the wire claim is TOTAL -- it says what BOTH wires hold, so a byte the model puts on the wrong port is a violation and not something nobody looked at. A one-port case therefore still pins port 1's wire as empty, and o_serial1 is emitted for every run.

The second port exists on QEMU virt only with a second -serial backend, so a uart1_ case declares platforms=qemu uarts=2. THE MODEL ALWAYS HAS BOTH -- uarts= is a fact about the machine QEMU builds, not about DevModel -- so a one-port case runs against a model whose second port simply never moves, and the only thing that would diverge is a uarts=1 program that touched 0x1000a000: the model would answer it and the machine would fault. Nothing does. It is not on the board profile at all (finding 30: that machine's UART is a different chip), and platforms=qemu there is the usual statement that the question cannot be ASKED on the other machine, not that it fails.

uart1_both is the case only a two-port machine can ask: it transmits two different strings byte-by-byte alternating between the ports, gives the two ports different scratch bytes and different MCRs, enables the FIFOs on one and reads the other's ISR, and enables the THRE interrupt in one IER and reads both ISRs. Every other uart case would pass against a model with ONE uart_state aliased at both windows. uart1_irq is the routing: port 1's line reaches the PLIC on source 12, is not delivered while only source 10 is enabled, and the claim hands back 12.

1. The RESULT region (abi.h). QEMU side: read out of guest physical memory over QMP xp. Model side: read out of gmem. The whole 4 KB is compared, untouched zeros included -- nothing is trimmed, so a difference cannot hide in the tail.
2. The disk image. QEMU side: byte-diff the raw -drive file after the process exits, reported per 512-byte sector. Model side: disk_read over v_disk. This is the channel that sees what a write request actually did.

The serial console is deliberately NOT a channel: printing a result costs ~10 instructions per character, and the model executes every one of them. an early hex-printing version was 1600 instructions / 23 s; the same observations through memory are ~40 instructions / 2 s.

They come from the ABI and from what the model is:

• Only the regions in abi.h are mapped. Anything else is a STUCK model.
• No dependence on a1/a2. a0 (hartid) agrees, but the model writes a1 to a hardcoded 0x1000 that is not the DTB address (finding 18) and never writes a2 at all.
• No LR/SC: exec treats the reservation outcomes as stuck.
• -smp 1. The model has 8 harts, but a schedule that only ever steps hart 0 is a legal execution, so this costs nothing.
• A bad FETCH is a TRAP LOOP, not VStuck. mtvec is 0 at power-on, so an illegal instruction sends the pc to 0, where the fetch at an undeclared address raises an access fault that traps back to 0 -- forever. The status is VBudget, and the way to tell it from a small budget is to pin the pc at two different step counts (CoreRegsFpr.v does). VStuck is for DATA accesses the model refuses.
• The clock never ticks. The harness always steps riscv_step false, so mcycle/cycle/time are frozen while minstret DOES advance -- which is the control showing the freeze is about the clock and not about counters in general. Consequence: no vtest image can observe elapsed time, so this suite cannot reach the timer-interrupt path at all, and mip.MTIP can only ever appear as power-on garbage.
• QEMU's -kernel boot contract passes a0 = hartid, a1 = the DTB pointer, AND a2 = 0x1028 (virt's reset ROM leaves a pointer to the fw_dynamic info struct there). The model's chain writes a0 and a1 and nothing else; a2 is admitted as a witness. See finding 18 for a1.
• Do not write FCR bit 0 in a test that receives. Flipping FIFO-enable flushes the receive path -- on BOTH machines now, uart_write offset 2 implements it -- and the host's first byte is already in QEMU's holding register before the guest's first instruction runs, so an FCR FIFO-enable at the top of the program silently eats byte 1 (measured: reads 0x42 first, 8 runs of 8). The model cannot reproduce the RACE, only the flush, which is why this is a rule for the test rather than a finding. Relatedly, with the FIFOs off QEMU delivers one character at a time and re-offers the next only after RHR is read, so any "LSR bit 0 immediately after a read" field is a race against the host rather than a fact about the device; order plus a spin before each read establishes the same property deterministically.
• A pt_ program must pin menvcfg.ADUE explicitly, before satp. Power-on ADUE DIFFERS (finding 20): clear in the model, set on the machine. So a page table written the natural way (V|R|W|X, no A/D) needs an A/D update on its first access, which FAULTS in the model and SUCCEEDS on QEMU -- and that makes an unrelated translation test diverge in a way that looks like a walk bug. Set or clear bit 61 deliberately in every pt_ program; Svadu is the natural default, being what start() gives xv6. QEMU does accept the CLEAR (verified -- ADUE is WARL, so this was not a given), so the Svade arm is testable on hardware too.
• Use lla, never la, to materialise an address. la assembles to a GOT load; the GOT is outside .text and the image is built with objcopy -j .text, so it is not in the image at all. The model then reads an undeclared address and goes STUCK -- which looks exactly like a genuine "the model does not decode this" finding. Whenever a test reports VStuck, check stuck_pc against riscv64-linux-gnu-objdump -d tools/vtest/build/<name>.elf and confirm the instruction it names is the access you meant to test.
• The QEMU command line is fixed by vtest.py, and -global virtio-mmio.force-legacy=false is part of it: without that flag QEMU presents a LEGACY virtio-mmio device (Version reads 1, not 2) and every register test disagrees for the wrong reason.

• The virt PLIC is built with num-priorities = 7 and silently ignores any priority or threshold write above 7. A probe using threshold 9 looks exactly like "the threshold does not mask". Keep every value <= 7.
• QEMU's sifive_plic_write does not recompute the context notification on an ENABLE write, so it lags by one register access. plic_mask.S re-writes the threshold with its existing value right after the enable write to force the recompute; that write is a no-op on the model side.
• QEMU defaults to LEGACY virtio-mmio (Version reads 1); -global virtio-mmio.force-legacy=false is in the fixed command line.
• A QEMU process that outlives its test holds the disk image's write lock, and the next run dies with "Failed to get write lock"; the runner quits it in a finally.

A test compares field by field, so a known divergence does not have to make the build red. The convention is to pin the value on BOTH sides:

Lemma t2_rw_model_diverging : ... = t2_model_diverging.   (* [8; 0; 512; 512] *)
Lemma t2_rw_qemu_diverging  : ... = t2_qemu_diverging.    (* [1024; 25684; 1; 513] *)
Lemma t2_rw_really_diverges : t2_model_diverging <> t2_qemu_diverging.

with a comment classifying it. This is green today and the model-side equation goes RED the day someone changes the model there -- which is exactly when the test file should be revisited, and is the property a comment alone would not give.

Sixteen of these have been FIXED rather than recorded -- the whole UART register file, its interrupt-status semantics and its bus decode; the PLIC's threshold, its M contexts and its source count; and the virtio disk's register decode, its queue sizes and its used-ring reporting. They are in Findings fixed below, with what the fix was and which test now passes because of it; they are kept because the point of this table is the register of what differential testing FOUND, not only of what is still open.

Classified as incompleteness (the model is stricter than the hardware, so some real driver has no model execution -- cannot make a proof wrong, but limits what can be verified) or defect (the model produces a value the hardware never produces, so a proof that depends on it is about a device that does not exist).

Seven more, from running the suite on a StarFive VisionFive 2 over JTAG -- though one of them, 27, is withdrawn; see below. README-hw.md is where they are written up, what a board run claims (it is narrower than a QEMU run), and how the rig works; this table stays the authority for the numbers.

Two of the first three questions asked of a board produced findings that QEMU testing structurally could not have found: every QEMU test runs on hart 0, and the harness's clock never ticks.

Finding 29 was previously attributed to core_regs_mcsr, and that was wrong: that test does not complete on the board at all (it reads for values, so the U74's refusal of menvcfg ends its run seven registers in). The board's misa was known only from a JTAG read, and a JTAG read is not this question -- see "Treating a trap as DATA" above. core_csrprobe establishes both that misa is csrr-readable on the U74 and what it answers, so the row is now a measurement.

One row where the board vindicates the MODEL against QEMU, and it is the first: mideleg. QEMU has the hypervisor extension, so VSSIP/VSTIP/VSEIP/ SGEIP are hardwired into it (0x1444, finding 19's consequence). The board has no H and reads 0 -- which is what the model reads. Every other row in this table has the model narrower or wider than the hardware; here QEMU is the outlier.

Finding 31 has a live consequence. README's rules require a pt_ program to pin menvcfg.ADUE explicitly before satp (finding 20). On this board it cannot -- the CSR does not exist -- so any port of the pt_ area to this hardware has to deal with that first.

Finding 32 stands, and getting it onto a proper footing produced the one piece of infrastructure this suite was missing. It was first written as "the model has NO TRANSITION", concluded from VStuck -- which does not establish that, because exec bails on Choose (the Sail monad's nondeterminism) exactly as it bails where the relation is genuinely stuck, and exec_run_det only runs the Some direction. That was the same error as the withdrawn finding 27, one level down.

So the gap was closed rather than the claim weakened. vtest-rocq/VExecStuck.v defines exec_r -- exec with its failure clause split into ENoStep and EChoice, proved to agree with exec everywhere -- and then

exec_r_no_step : exec_r m s = inr ENoStep -> forall x s', ~ run m s x s'

which is the converse the tree did not have. VTest.stuck_why reports which kind a run hit and stuck_why_no_step lifts it to the whole run. Measured: csrr mseccfg is Some ENoStep -- real stuckness, not a declined choice -- so the original claim was right and is now checkable. CoreCsrwide.v carries it as core_csrwide_model_really_stuck.

Finding 25 (sc.w does not evaluate) has NOT been given this treatment and is the obvious next candidate: it is an exec limit stated as one, but nobody has asked whether the relation steps there.

FINDING 27 IS WITHDRAWN, and the mistake is worth more than the finding was. I ran the default runner, saw a frozen clock, and reported a property of the MODEL. But RiscvLang.mnode_step's instruction-boundary rule is

| Interface.Ret _ => exists tick : bool, m' = riscv_step tick /\ ...

-- the language quantifies EXISTENTIALLY over the tick at every boundary (the sound weakening of the model loop's deterministic every- plat_insns_per_tick tick; plat_insns_per_tick is 2). An execution in which mtime and mcycle advance is one the model ALLOWS. VTest.run_until steps riscv_step false because that is a convenient DEFAULT for tests whose subject is not time, not because the other branch is unavailable, and VTest.run_until_tick takes it: ClintTime.v §4 exhibits a run where the model advances the clock and reports exactly what both machines reported.

AN ABSENT WITNESS WAS READ AS AN ABSENT EXECUTION, in a suite whose entire question is whether the model ALLOWS what the hardware did. That is the one-directional framing inverted, and it is available anywhere else the language quantifies existentially and a runner resolves the choice: before reporting "the model cannot", check whether the harness ever ASKED it to.

What survives is a fact about the default and not about the model: every other test here is exhibited on the non-ticking branch, so none of them observes elapsed time. A test that wants to reason about elapsed time asks for run_until_tick, as clint_time now does.

Finding 28 is the one only a board could find. ClintMsip.v carries both halves, and either alone would be misread: on QEMU's hart 0 the model's MSIP semantics are RIGHT end to end -- including raising and dropping mip.MSIP, which a "stored but inert" model would fail exactly as the UART's MCR did in finding 6 -- and on the board's hart 2 the same program completes on the machine while the model takes a load access fault at 0x8000006c with mtval = 0x2000008 and trap-loops forever. It is the same shape as findings 11 and 12, where the PLIC was indexed by hart instead of by CONTEXT and half the register file was simply absent.

tools/vtest/cva6.py asks the same question of the RTL of the OpenHW CVA6 core (cv64a6_imafdc_sv39, pinned in tools/vtest/cva6/build.py), inside CVA6's own corev_apu testharness, simulated by Verilator. It is the first platform that is a hardware design rather than an emulator or a chip, and it exists because of the effort in claude-notes/projects/hw-refinement.md: xv6 proved on a specific core. The runner's docstring says what a run claims; in short:

cva6 is in the default platforms=, so a case runs there unless it says otherwise. The simulator is built on the build VM (tools/vtest/cva6/: build.py takes CVA6's own Verilator file list and swaps in vtest_tb.cpp, which backdoor-loads DRAM, polls DONE and decodes the 16550's SOUT pin; Verilator v5.008 with CVA6's patch, as CVA6's CI pins). A run is a fraction of a second.

First sweep, 2026-09-27: 30 cases runnable, 30 captured, 19 pass (18 agree, 1 stuck -- core_csrwide, as on QEMU). Eighteen of the thirty result regions are byte-identical to QEMU's. Of the eleven red, five are the value dumps that are red on every platform (clint_raw, core_dtb, core_csrvals, core_regs_fpr, pt_tlb_set0); the other six are these:

Where CVA6 sides with the MODEL against QEMU: pt_ad. The case leaves menvcfg alone; the model's power-on ADUE is 0, CVA6's is 0 (it has no Svadu at all), QEMU's is 1 (finding 20). So CVA6 takes the page fault the model takes, and the run passes. And core_icache is stale on CVA6 exactly as on the U74 (finding 34) -- ipol_cva6=stale -- where QEMU is coherent: the model's non-coherent fetch view is right about this core too.

These are findings, not deleted rows. Each was a real difference between the model and the machine and each is now a passing test rather than a pinned divergence, but the register of what differential testing FOUND is the point of this file, so they keep their numbers, their values and their original classification. All five were in the 16550 and they went together: half of them are one modelling shortcut seen from different sides.

Finding 10 was the serious one of the PLIC three, and the only PLIC finding that was not mere incompleteness: the threshold appeared in plic_eip alone, so the model's NOTIFICATION and its CLAIM disagreed -- a source could be invisible to a context and still be what that context's claim register handed back, with its pending bit cleared on the way out. The fix is not a special case in the claim but a move: the threshold went into plic_cand, the one predicate that says what a context can see, and plic_eip became existsb (plic_cand p c) while plic_best folds the same thing. The two cannot disagree now because they are the same question asked twice ("is there one?" versus "which one?"), which PlicThresh.v states off the model as well as off the program. It also subsumed the old 0 <? p_prio guard -- a priority-0 source cannot exceed a threshold of 0 -- so the model got smaller.

Findings 11 and 12 were one change: the PLIC stopped being indexed by hart. It has CONTEXTS, the board wires two to each hart (M then S), and every per-context register family -- enable bitmap, threshold, claim/complete -- is now decoded for all of them, with dev_meip beside dev_seip and a second wire arm in RiscvLang.plic_step so that an M context's notification reaches its pin rather than being computed and dropped. Decoding the registers while leaving the pin unmodelled would have been the same half-fix as a stored-but-inert control bit. The source count went with it: 96 sources means three enable words per context and three pending words, which is what makes source 32's priority register (plic_prio0 +20) a register at all.

Finding 4 is the one that had to be got right rather than merely made. Two rules both explain "1 for a write, 513 for a read": key off the request TYPE, or key off the data descriptor's WRITE flag. disk_err is what separates them -- an unrecognised type and a FLUSH, both published through a read-shaped chain, where the device writes no data at all. The spec's wording ("bytes WRITTEN into the device-writable part") says 1; the hardware says 513, because what a real device reports is the writable SEGMENT and not the transfer. Keying off the type would have passed disk_rw and produced 1 there -- a value the machine does not produce, which is finding 4 itself moved from the read path to the error paths. So vreq_used_len reads vr_wr, the flag the parser takes off the descriptor.

Findings 3, 13, 14, 15 and 16 were all the same shape: an access the hardware answers and the model had no transition for, so a driver that made it had no model execution. Nothing about them was subtle once each register's meaning was pinned; what they cost was reach, and the two that had real drivers behind them are 15 (a narrow read of a status byte) and 16 (a driver that touches a queue this device does not have). Finding 13 needed one piece of modelling rather than decode: v_disk is a total function, so the medium has no edge of its own and the CAPACITY had to become a field of the device state, set by the machine that attaches the image.

Finding 6 was the load-bearing one of the UART five, and not because of the values. MCR bit 4 is LOOPBACK, so a readable MCR that ignored bit 4 would have been worse than the register that read as zero: a driver's self-test would have put its byte on the WIRE, which is a thing the hardware never does -- turning an incompleteness into a defect. Making the register real meant making the mode real. uart_tx_pop has two arms, and uart_state carries u_wire (what left on SOUT -- the console-observable trace, and what VTest.serial_of compares) beside u_out (what the TRANSMITTER finished with, loopback included), so that the transmitter-token argument in WpUart.v, stated on u_out ++ u_tx, is untouched by where the byte went. uart_loop checks the whole of it against the machine, serial channel included: the loopbacked byte comes back on RHR and the host sees only the byte sent after LOOP was cleared.

What these fixes deliberately did NOT change, each for the same reason -- the safe direction is the model producing MORE interrupts and accepting MORE input than the machine, never fewer:

• the RECEIVE interrupt is a level on the hardware too, so uart_rx_int is what it always was (uart_irq_rx is the evidence);
• the ISR's receive condition triggers at ONE byte rather than at FCR's trigger level. Modelling the trigger level without the character TIMEOUT interrupt would err toward FEWER interrupts, and one byte is the level xv6 and every test here select anyway (FCR bits 7:6 clear);
• the model's rx FIFO is 16 deep in both FIFO modes, where the hardware has a one-byte holding register with the FIFOs off. The model accepts more host input than the machine offers, and uart_rx_push REFUSES when full, which is the flow control QEMU's front end applies rather than an overrun.

Finding 4 is the one worth acting on. The spec defines the used element's len as the number of bytes written into the DEVICE-WRITABLE part of the chain -- the status byte alone for a write request, the data buffer plus the status byte for a read. VirtioModel.virtio_used_elem_writes writes the data descriptor's length regardless of direction, which is a value no real device produces. Nothing in the tree has noticed because xv6's driver ignores the field. The fix needs the request TYPE at that point, so it is local; what makes it a decision rather than a drive-by edit is that VirtioModel.v's reverse-dependency closure is 1286 files.

Finding 5 was the serious one, and it is RESOLVED. disk_order publishes two write requests in one batch -- eight sectors at 100 and one sector at 5 -- and records which descriptor id lands in which used-ring slot. QEMU produces BOTH orders:

The model used to have no execution for the second: virtio_req_step read the chain at position v_seen and handed back v_seen + 1, so the served order WAS the publication order. That was the other direction from findings 1--3 -- the hardware having a behaviour the model had no transition for, so a theorem proved against the model did not cover the machine -- and it was live in xv6: virtio_disk_intr reads each used element's ID and wakes disk.info[id] precisely because completions need not come back in order.

What the model does now (VirtioModel.v section 5b): the device POPS available-ring entries strictly in order (virtio_pop_step; v_seen is the pop index and v_inflight the set of popped, uncompleted descriptor HEADS) and serves any in-flight head one bus transaction at a time (virtio_fetch_step / virtio_capture_step / virtio_write_step / virtio_complete_step take the head). VSched's eager schedules differ only in which in-flight head they pick (lowest_head / highest_head), and DiskOrder.v proves the model admits both captured orders (disk_order_admits_inorder, disk_order_admits_reordered, disk_order_model_has_both) plus the general facts model_pops_in_order and model_completes_any_inflight_head. The Iris side followed: the keyed protocol serves any position (vp_srv, vp_lo, vp_uix), and the driver proofs (virtio_disk_rw, virtio_disk_intr) are stated over a per-descriptor receipt keyed by head -- claude-notes/design/virtio-driver.md and claude-notes/completed/virtio-finding5-driver-port.md.

plic_cand is pending && enabled && (0 < priority) and never mentions the threshold; the threshold appears in plic_eip alone. So the model's notification and its own claim disagree with each other: a source masked by the threshold raises no notification, yet plic_claim hands it back and clears its pending bit. QEMU returns 0 and leaves the source pending, so lowering the threshold later re-exposes it.

Like finding 5, this is not merely a wrong value: plic_read's claim arm is a pure function of plic_state, so no schedule can produce QEMU's answer.

It is not live in xv6 -- plicinithart writes threshold 0 -- but PlicPlan.v deliberately leaves the per-hart threshold completely free, so the device invariant admits exactly the states where the two disagree.

The fix is three tokens and makes the two halves agree by construction: move the threshold conjunct from plic_eip into plic_cand (where it subsumes 0 < priority), leaving plic_eip := existsb (plic_cand p h) plic_srcs.

plic_level shows the model re-forwarding a still-asserted level source after plic_complete, where QEMU does not: QEMU's PLIC takes pending off the RISING edge only. A level gateway that re-forwards is the spec-faithful behaviour -- it is why a driver acknowledges the DEVICE before completing at the PLIC -- so no model change is wanted. The model does have a matching execution (SLatch is never forced), but VSched.settle is eager and takes every enabled arm, so the harness forced a forward the RELATION never required.

Now reproduced. settle1_gated takes a latch flag (every existing caller passes true, so nothing else moves), and vtest-rocq/QEMU/PlicLevelRun.v is HAND-WRITTEN with a device schedule -- the first user of the generator's hand-written escape hatch. The schedule is a CREDIT, not a step count: what the execution is is "the gateway forwards ONCE", which is what an edge-triggered gateway does with a level that rises once and is stated without reference to the program. settle1_credit offers each round without the gateway first and spends a credit only when nothing else is enabled, so it counts FORWARDS rather than settle rounds. The run reproduces QEMU's result with zero differing bytes.

chain_at requires exactly three descriptors, so a 4-descriptor scatter-gather chain leaves the device virtio_stalled and it never completes -- run_status reads VBudget, and disk_chain confirms virtio_stalled = true after 700 instructions, so it is a real stall and not a small budget.

But this is incompleteness in practice, not unsoundness, and the difference is the whole point of the "model UB as anything, never as nothing" rule: DevStepDiskWild is enabled exactly when virtio_stalled holds, so the model's transition relation genuinely does contain QEMU's behaviour -- the device may write anything anywhere, which includes writing what QEMU wrote. What the model does not contain is anything a driver PROOF could use. DiskChain.v states both halves off the model (model_refuses_longer_chains, model_stalled_leaves_only_wild) rather than off the test.

Exhibiting it would need a hand-written schedule interleaving ~550 SCpu steps around one SDiskWild carrying ~530 (address, byte) pairs built mechanically from the capture; DiskChain.v section 5 records what that takes.

disk_err runs the UNSUPP and FLUSH paths, where the model reports used.len = 512 and QEMU reports 513 -- but the spec says 1 on both, since neither path writes the data buffer. So on these paths QEMU is not spec-conforming either, and finding 4's fix must be stated against the SPEC (bytes actually written into the device-writable part of the chain), not against QEMU's value.

conc_sb is the store-buffering litmus test -- hart 0: X=1; a=Y alongside hart 1: Y=1; b=X -- and QEMU produces (a,b) = (0,0), which no sequentially consistent machine can. Measured 55 times in 1200 runs (4.6%) by the agent, and independently re-confirmed at 4 in 200. It is not a truncated run: in the (0,0) captures X and Y are both 1, so both stores landed and both loads still returned 0.

QEMU is RIGHT. RVWMO permits a store to be reordered past a later load, the litmus program has no fence between them, and QEMU on an x86 host exposes the host's TSO. It was the MODEL that was wrong: RiscvLang stepped every hart over one byte map, so a store was global the instant it retired, and the old VConc recorded that off the model (model_hart_sees_the_one_memory, model_store_is_immediately_global) and enumerated all six interleavings of the two two-instruction sequences, none of which gives (0,0).

FIXED BY THE TSO CUTOVER. The language is now a store-buffering machine (RiscvLang.mnode_step over TsoMemPa): the era has a global append-only write log, every hart a monotone FLOOR into it, a plain store appends without moving the author's floor, and a plain load reads latest-visible at any view between the floor and the top -- below the view, or the hart's own message (which is store forwarding). A W->R fence drains. Since the load-load relaxation (claude-notes/completed/relaxed-rr.md) a plain load moves no floor either -- it raises a read WATERMARK and the per-byte COHERENCE floors, and a fence with an R->R edge acquires (floor to the watermark). The harness follows: VTso.texec is exec with those arms, its read policy is a schedule choice, and VConc.CCpuStale runs a hart reading at the lowest view the model admits. ConcSbSched.sb_00 -- align ++ [CCpuStale hart0 2; CCpuStale hart1 2] -- is the (0,0) execution: no load moved either hart's floor and conc_sb.S has no fence before the litmus load, so each hart's floor is still 0, before either litmus store, and each load reads below the other hart's store. (The two arms it uses were once stated off the model in VModelFacts; those lemmas went with the mnode_step arity change in 6e4483a3a, and the arms themselves are the record.) With sw; fence; lw the same schedule reads at the top and (0,0) is gone, so xv6's __sync_synchronize() in acquire/release is now OBSERVABLE.

The model reproduces all four observed outcomes, whole result region each (QEMU/ConcSbPass). The fresh policy (CCpu) is provably the old harness (VTso.texec_fresh_exec), so every other multi-hart run computes what it computed before.

pt_tlb rewrites a level-0 leaf without sfence.vma and reads again, at two VAs chosen to land in different TLB sets. At set 7 both machines keep the stale entry -- that is the control. At set 0 QEMU keeps it and the model has already re-walked, 20 runs of 20.

The cause is exact: tlb is a vec (option TLB_Entry) 64 and tlb_hash is literally the low num_tlb_entries_exp = 6 bits of the VPN, so the TLB is DIRECT-MAPPED -- and every fetch in a vtest image is at VPN 0x80000 with every result store at 0x80100, both = 0 (mod 64), so a set-0 entry is evicted by the next instruction.

Unlike findings 5, 10 and 24 the model is not missing a FREEDOM -- set 7 shows it can keep a stale entry. It has a smaller, less associative TLB, and both are legal implementations. The risk is directional rather than structural: a theorem over this model can conclude "the access after a PTE write uses the new mapping" where the real machine uses the old one. Only software that omits sfence.vma is exposed, and nothing in xv6 is -- but the model hands such a program the favourable answer instead of refusing it.

A fix is not more capacity: any deterministic finite TLB collides somewhere. It would have to make eviction NONDETERMINISTIC -- the DevStepDiskWild over-approximation shape applied to translate. Recorded, not proposed.

pt_adu runs two write-backs under vm_compute at ordinary cost -- no hang, no VStuck, no internal_error. The sc.w non-termination of finding 25 does not reach this path, and the reason is structural: execute_STORECON goes through the opaque platform axioms match_reservation/ cancel_reservation, which exec cannot step, whereas write_pte_conditional is mem_write_value_priv ... con = true -- an ordinary Interface.MemWrite outcome. exec answers it inl None and write_ram maps that to true.

Consequence worth knowing: the conditional write ALWAYS succeeds under exec, so the Ok false -> internal_error arm of update_and_write_pte is unreachable by this interpreter. Not a defect -- the limit of what a test in this suite can probe.

Every other row is the model being NARROWER than the hardware. Finding 22 is the reverse: the model implements CSRs that QEMU's default rv64 virt CPU answers with an illegal-instruction trap. Under this suite's premise -- QEMU-virt is the reference hardware -- the hardware's TRAP then has no model execution, which is the unsound direction.

But it may not be a bug at all: it may just mean the model is configured for a different machine than -cpu rv64 gives us (sail-config-rv64d.json decides which extensions exist). The same axis produces finding 19 in the opposite direction -- QEMU has H and the model does not.

This needs a decision that is not the suite's to make: WHICH machine is the model claiming to be? If it is QEMU's virt board, findings 19 and 22 are both real gaps and the config should be reconciled. If it is a machine with a different extension set, the QEMU command line should be pinned to match (e.g. -cpu rv64,h=false,smstateen=on) and both rows become configuration notes rather than findings. Until that is settled they are recorded, not classified.

model-xv6iris/sail-modules.txt includes FD_core -- the registers, fcsr, and the CSR plumbing -- but no F/D INSTRUCTION modules, so the decoder has no floating-point instructions at all while misa bits 3 and 5 promise them. fsd ft0,8(s11) takes an illegal-instruction trap with mstatus.FS correctly set to Initial first, so FS is not the cause. The fix is a one-liner either way: add the modules, or set F/D supported: false in the config so misa stops promising them.

QEMU's FIRST execution of a basic block costs thousands of guest instructions' worth of wall time in tb_gen_code, so a plain rendezvous does not make two harts overlap -- whichever is still in the translator loses before it starts. Measured: a 16-round lost-update loop came out at 32 in 60 runs of 60, and 2048 rounds each was still 0 lost in 25 runs.

The fix, used by all three racing tests: a two-pass structure. Both harts run the whole hot path once on PRIVATE words, leaving every block in QEMU's shared TB cache, then rendezvous, then race. With that, two rounds each is enough. conc_sb additionally gives the harts delay loops of different lengths to trim hart 0's systematic head start, which raised (0,0) from 1.3% to 4.6% of runs.

Only store->load reordering appears on an x86-64 host, which is what TSO under MTTCG can expose. Message-passing and load-buffering tests would be guaranteed single-outcome here and are worth adding only if this suite is ever run on an aarch64 host.

Because QEMU has more than one legal execution here, disk_order is captured as a SET. A vtest: directive in the .S names the repeat count and the backend configurations to union over:

/* vtest: repeat=20 drives=cache=writeback;cache=none,aio=threads */

No single configuration reliably shows both orders, so a test about nondeterminism names the ones that between them exhibit its executions; without that, make vtest-gen is itself flaky. The generated file then carries <name>_qemu_results : list (list Z) alongside the single <name>_qemu_result.

Positive results are worth recording too -- each is a way the model could have been wrong and is not.

• The request protocol (disk_rw): both status bytes, both used-ring ids, the used index, the interrupt status, and the 512 bytes DMA'd in each direction.
• The disk image (disk_rw, disk_order, disk_intr): QEMU has flushed a completed write to the backing file by the time its process exits, so the raw-file diff is a sound channel -- and the model's v_disk agrees with it byte for byte, including on a multi-sector (8-sector) request.
• THE TWO PORTS ARE TWO DEVICES (uart1_both, uart1_tx, uart1_regs, uart1_rx, uart1_irq): the second window has its own register file (scratch, MCR, IER, FCR/ISR and the THRE latch all answer per port), its own transmit and receive FIFOs, its own wire -- two interleaved strings came back on the two backends with nothing crossed -- and its own PLIC source. uart1_irq pins the routing in both directions: with only source 10 enabled port 1's still-asserted level is NOT delivered (SEIP stays clear, the claim returns 0, the source stays pending), and enabling source 12 delivers the same request and the claim returns 12.
• The UART transmit path end to end (uart_tx, uart_dlab, uart_regs): uart_write at offset 0 -> uart_tx_pop -> u_wire is exactly the byte sequence the host received, in order, nothing lost or duplicated; uart_lsr is 0x60 with the FIFO empty at every point either machine can be asked, including one instruction after a THR store, and LSR reads are pure.
• The whole UART register file, read and written (uart_regs, uart_width, uart_loop): all eight offsets, at all four access widths, in both directions -- see Findings fixed, since every one of those rows is now a confirmation. The two worth naming on their own are LOOPBACK (uart_loop: the transmitted byte comes back on RHR, the modem outputs come back on the modem inputs pin for pin, and the host sees nothing of it -- the serial channel is what proves the last part) and the ISR's LATCH (uart_regs, uart_irq_tx: two reads in a row differ, and the latch is armed by the IER write itself, so a transmitter that is already idle when the interrupt is enabled still interrupts).
• The DLAB divisor-latch aliasing (uart_dlab), which is what the whole un_dlab ghost in design/device.md exists for: LCR bit 7's polarity, offset 0 aliasing to DLL and offset 1 to DLM, IER unaffected by a DLM store, the aliasing not sticky, and a byte written to offset 0 with DLAB set NOT reaching the wire.
• PLIC arbitration, both clauses (plic_arb + plic_tie): with the disk at priority 3 and the UART at 7 the claim returns the HIGHER id 10 over the pending, enabled id 1 -- ids are scanned in order, so only the priority comparison explains it -- and the same program with equal priorities reverses the order to 1-then-10. The pair pins both clauses of plic_better; either alone is passed by a half-wrong implementation, and QEMU breaks ties the same way.
• The rest of the controller (plic_thresh, plic_mask, plic_level): the threshold gates the NOTIFICATION strictly and in both directions (equal is masked, and the pin follows down and back up); the enable bit is not the gateway (a disabled source still latches, is not claimable, and becomes claimable when the bit is set later with no new device edge); a claim clears that source's pending bit and no other and marks it claimed, and neither source re-latches while claimed; plic_complete touches p_claimed only; claiming with nothing pending returns 0 and disturbs nothing; the pending word carries two bits (0x402), which plic_pending_word's fold had never been exercised past one; and pending is sticky across the source going quiet.
• The two-device interrupt fabric: the UART raises PLIC source 10 with no serial input at all (IER bit 1, empty FIFO), and dev_irq_level's two-source dispatch agrees with the machine.
• The UART raises BOTH interrupts, all the way into mip (uart_irq_tx, uart_irq_rx): IER bit clear -> nothing pending; bit set -> the line goes high -> the gateway latches source 10 -> the wire sets mip bit 9; the ISR names the cause (2 = THRE, 4 = rx available); the S-context claim hands back 10; the condition removed and completed -> pending and SEIP clear. Identical on both machines at every step of both chains. This is the first test to raise source 10 at all, so it is the first evidence that the UART is wired to the controller AND to the right source. It also pins the GATEWAY against the ISR read: on both machines the read drops the UART's line and source 10 stays pending with SEIP still set, because the gateway holds a forwarded request until it is claimed -- plic_latch does the same.
• The virtio RESET command (disk_ident), never exercised before: Status -> 0, QueueReady -> 0 without the driver clearing it, ISR -> 0, and the offered features untouched. virtio_reset keeping only v_disk is what the hardware does.
• The error paths (disk_err): an unrecognised request type is an ANSWER, not a silence -- status 2 (UNSUPP) and a used-ring slot, with zero data movement on both channels and the disk unchanged; and a FLUSH from a driver that DECLINED VIRTIO_BLK_F_FLUSH still completes OK on QEMU, so the model's unconditional recognition of type 4 is faithful. The ISR is a bit and not a count: still 1 after three completions.
• Per-queue READS at a queue that does not exist (disk_ident): both answer 0. A driver may LOOK at queue 1; it may not TOUCH it.
• The whole S-mode CSR file, the whole PMP file, and the whole HPM file (core_regs_scsr, core_regs_pmp, core_regs_hpm) agree byte for byte over the entire result region. None is vacuous: sstatus is derived through the model's lower_mstatus window onto the board-written mstatus; satp = 0 is what makes "translation is off until start() turns it on" true OF THE MACHINE; and ArchReset.v says pmpcfg is explicitly NOT a board obligation -- the spec's own reset_pmp establishes pmp_all_off over arbitrary garbage -- so those sixteen zero entries are produced by the model's reset CODE, and this is the check that the code's answer is the machine's answer. The HPM test also exercises a permission path: an M-mode read of the UNPRIVILEGED alias with mcounteren = 0 must succeed, because mcounteren gates S and U and not M, and the model does not wrongly refuse.
• mstatus = 0xA00000000 (core_regs_mcsr): ArchReset.board_regs' power-on obligation for mstatus -- SXL = UXL = 2 and everything else clear, the part reset_sys does NOT establish -- is a true statement about this board.
• mip and tselect are WITNESSED, not findings (core_regs_mcsr): the model admits QEMU's values from a legal power-on file. tselect is the instructive one -- read_CSR 0x7A0 returns not_vec tselect, the architecture's "no trigger selectable" stub, so the default's all-ones readback is just init_regstate's zero complemented; preset the register to all-ones and the read gives QEMU's 0. This is exactly the case a raw diff would have mis-reported as a divergence.
• The UART receive datapath (uart_rx), every observation exact: bytes come out IN ORDER (u_rx really is a FIFO -- a LIFO or a one-deep register gives a different answer here); RHR pops EXACTLY one byte per read, established without a race by reading three of a four-byte queue and finding the fourth still there; LSR bit 0 tracks the FIFO across the whole sequence and is not sticky in either direction; and FCR bit 1 clears the receive FIFO -- a live uart_write arm no test had touched on the rx side, and what uartinit writes at boot -- while leaving the receive HOLDING register alone, which is what a read with DR clear hands back.
• Instruction-granularity interleaving (conc_lost): a lost-update race produces exactly three outcomes (4, 2 and 3 over two rounds) and the model has a schedule for each, floor included. It also pins that the UNSCHEDULED round-robin run is the maximally-colliding one, which is the concrete reason a race test must NAME its interleaving rather than let the harness pick.
• Sub-word store granularity under concurrent access (conc_byte): two harts holding a loaded byte while the other stores an adjacent byte of the same word, three rounds, nothing lost -- the same shape that DOES lose an update in conc_lost when the byte is shared.
• amoadd.w (conc_amo) computes the right read-modify-write and both machines answer 8. The atomicity claim is deliberately weak and the file says so: CCpu is instruction-granular, so no schedule here could split an AMO in the first place.
• S-mode with paging on, end to end (pt_ident): the PMP TOR grant that S-mode cannot run without, the satp write and sfence.vma, mret to Supervisor, a level-2 leaf taking 30 offset bits, and FETCH through translation as well as load and store.
• The A/D write-back arm against real hardware (pt_adu), for the first time -- both the A case and the D case, checked by reading the PTE word back out of the page-table page: 0x07 -> 0x47 and 0x47 -> 0xC7, upper 54 bits identical, i.e. the write-back rewrote exactly the flag bits to the same word the hardware wrote. And the Svade arm (pt_ade): the model refuses exactly where the hardware refuses, and writes nothing.
• The fault matrix (pt_fault): five refusals and one grant, with scause, sepc AND stval identical in all five. stval carries the faulting VIRTUAL address including the sub-page byte offset -- a model reporting the page-aligned VA, the PA, or the PTE address would fail here -- and the instruction-fetch case attributes sepc to the unmapped VA itself, not to the jalr. sstatus.SUM gates the identical U-page load in both directions on both machines.
• The walk really descends (pt_levels): a three-level walk to a 4 KB leaf, and a level-1 megapage whose 21-bit offset is checked by a store 1 MB in landing where it should.
• Two checks a translation model could quietly have omitted and did not: the reserved leaf encoding R=0/W=1 (pt_resv) and the misaligned superpage (pt_super). Each has a control mapping built from the same PPN that works, so the fault is attributable to the CHECK and not to the table.
• medeleg bits 12/13/15: the M-mode backstop never fired in any of the nine images, and sfence.vma flushes totally on both machines.
• The whole interrupt path (disk_intr): the device raising its line, the PLIC gateway latching source 1, the wire driving hart 0's sig_seip (visible in mip), the S-context claim returning the source and clearing pending, the device acknowledgement dropping the line, and the PLIC complete clearing the claim. All twelve observations identical. In particular the model's deliberate PROPAGATION DELAY -- the gateway latch and the wire are separate steps, not side effects of the completing MMIO write -- is faithful: the test spins on the pending bit rather than reading it once, so it would still pass if the delay were longer and would fail if the model had quietly made the pin synchronous.