xv6iris — verifying xv6-riscv in Rocq/Iris over the Sail RISC-V semantics

Sandbox Theorem

Following our blog post. This is the repo containing the sandbox and proof.

To run the demo you need to set up the machine with nix, binutils, and gcc.

bash tools/proof-toolchain/setup.sh
source tools/proof-toolchain/env.sh
JOBS=96 bash tools/build-sandbox-goal.sh 2>&1 | tee /tmp/goal-build.log

You should see:

1 FunctionalExtensionality
7 PrimInt63
4 PrimString
67 rv64d

Which are the assumptions printed at the end.

The statement that we proved is vmm_sandbox_statement_u2 which is in this Rocq file.

-- Below Is Original --

This project proves, in the Rocq Prover with the Iris separation logic, weakest-precondition specifications for the xv6-riscv kernel — reasoning about the actual kernel binary, instruction by instruction, against the official Sail RISC-V ISA semantics compiled to Rocq (see "Regenerating the Sail model"). The kernel ELF is disassembled into Rocq data, an Iris language is built over the Sail model's execution monad, and machine code is specified with separation-logic points-to assertions for registers, memory, and devices.

A paper about this project: https://arxiv.org/abs/2609.04043.

Layout

xv6iris/
├── vmm/             # current VMM kernel sources, upstream integration, and Nix build
├── xv6-riscv/       # optional upstream reference kernel checkout
├── sail-riscv/      # the Sail ISA sources (only needed to regenerate the model)
├── model-xv6iris/   # the Sail RISC-V model compiled to Rocq (checked in; logical name `Riscv`)
├── kernel-rocq/     # the kernel image as Rocq data, generated by the dumper (logical name `Kernel`)
├── user-rocq/       # the xv6 USER programs (user/_sync, ...) as Rocq data (logical name `User`)
├── iris/            # the Iris development: language, points-to, WP lemmas, function specs & proofs
├── tools/           # dump_elf.py (ELF -> Rocq), gen_code.py, proof_coverage.py, proof_profile.py, regen_sail_model.sh
├── claude-notes/    # the durable development notes (design docs, worklists) — see below
└── Makefile         # top-level build

Build

The VMM proof development uses the actual tracked sources in iris/ and model-xv6iris/. The default image is built from the current vmm/ working tree, including uncommitted changes. With the supplied Nix toolchain:

bash tools/proof-toolchain/setup.sh       # install/smoke-check the proof tools
JOBS=32 bash tools/proof-build            # attempt SystemAdequacy.vo
JOBS=32 bash tools/proof-build ProofMyproc.vo VmmImageCheck.vo

tools/proof-build selects Rocq 9.0.1 and invokes the root Makefile on the current source files. PROOF_LOG=/path/to/fresh-prefix optionally captures output and the exit status. No source snapshots or repository revisions are required.

The Makefile also supports an existing opam switch through SWITCH/RUN. After sourcing tools/proof-toolchain/env.sh, pass RUN= to use Nix's tools:

make            # == make proofs: build the model, the kernel dump, and all Iris proofs
make audit      # build, then Print Assumptions on the system theorem (see below)
make model      # compile only model-xv6iris/ (the Sail-generated Rocq model)
make kernel     # build the current VMM kernel and filesystem
make user       # build the current VMM kernel and filesystem
make vmm-proof-image # regenerate tracked dumps/decodes from the current VMM build
make dump       # compile kernel-rocq/ and user-rocq/ (re-dumping if an ELF changed)
make dump-force # force a re-dump of every image from the ELFs on disk
make clean      # remove Rocq build artifacts; make distclean also cleans the xv6 tree

bash tools/proof-build audit-only (or make RUN= audit-only) compiles iris/SystemAssumptions.v after a successful system build. This is Print Assumptions on the system theorem — the only check that sees through every functor and seal. It is deliberately not part of make proofs: the statement alone measures ~95 s on the build's serial tail, roughly 30 % of a clean build's wall clock, so it is run on demand and by CI (which puts its output in the run's step summary) rather than on every developer build. That is also why iris/_CoqProject carries it as a commented-out row.

Build graph: each ELF is disassembled by tools/dump_elf.py — the kernel into kernel-rocq/*.v, each user program into user-rocq/*.v; iris/ depends on kernel-rocq/ and the Sail model in model-xv6iris/. Toolchain (in the opam switch): Rocq 9.0.1, coq-iris 4.4.0, coq-sail-stdpp 0.20.1, plus riscv64-linux-gnu-gcc/objdump and python3 for the images and dumper.

The generated .v files are checked in; image build artifacts live under vmm/build/. tools/import_vmm_image.py updates kernel-rocq/, user-rocq/, and the generated iris/ decode files from the current VMM kernel and actual filesystem contents. vmm/build/proof-image/manifest.json records the resulting image hashes. Unchanged generated files keep their timestamps, so repeated builds remain incremental.

The upstream xv6 base and external toolchain versions remain package inputs in vmm/guest/sources.lock.json and vmm/flake.lock. KERNEL_CONFIG=xv6 selects the optional upstream reference build using XV6_REV; the active proof port targets KERNEL_CONFIG=vmm, the default.

The proofs' instruction addresses are symbol-relative (KernelSyms.bpin + 0x14) and so survive a relayout, but each decode fact also states the raw encoding word and the decoded pc-relative immediate, and those do not — they drift even in functions whose C source did not change, via re-encoded call targets and linker relaxation. That whole layer — iris/KernelDecode*.v and the per-function iris/Code<F>.v — is therefore GENERATED from the tracked dump: make gen-code regenerates it, and make check-decode compares it with fresh output without changing source files or consulting Git history. Run make check-decode after every re-dump.

Regenerating the Sail model

The generated model .v files in model-xv6iris/ are checked in; a normal build never regenerates them. The source dependency is official riscv/sail-riscv, pinned by SAIL_RISCV_REV in the Makefile. It requires Sail 0.20.2 with the Rocq backend. The compiler pin in tools/proof-toolchain/default.nix includes the subsequent upstream fix for pattern-exhaustiveness time/memory blow-up. Install it alongside the proof toolchain, then regenerate from Bash:

bash tools/proof-toolchain/setup.sh --model
source tools/proof-toolchain/env.sh
make RUN= model-gen
make RUN= model

tools/regen_sail_model.sh can also be invoked directly. It enforces the source checkout's minimum Sail version and compile-checks the generated files before installing them into model-xv6iris/.

Like xv6-riscv/, the checkout is .gitignored and cloned on demand (detached, at the pinned revision); make sail-rev-check warns when it has moved off that revision, because a model regenerated elsewhere is not the model the proofs are about.

Generation and build inputs live in model-xv6iris/:

• sail-config-rv64d.json — the resolved RV64 configuration, with H enabled and 512 MiB RAM for the VMM. Its comments document the project-specific choices and the substitutions to redo after an upstream bump.
• sail-modules.txt — the curated module subset, including H, FD_instructions and Zfbfmin. The last supplies a probe called by FD's half-width load/store decoder; omitting it makes that path get stuck. Extension configuration and module inclusion are separate inputs.
• rocq-externs.sail — arithmetic and platform-hook bindings, supplied with Sail's --splice option. Both coq: and rocq: spellings preserve the intended Z.quot/Z.rem implementations and bind reservation/terminal-output calls to the qualified definitions in xv6iris_extras.v. It also connects external IRQ sampling to the device fabric's wires while SIG's overlapping test-device MMIO window stays disabled.
• phys_mem_interface.sail — the physical-memory interface with Read_ttw and its AK_ttw mapping. The generator stages the dependency's model sources and selects this tracked file; Sail's splice facility cannot extend enums.
• memory-access.sail — the checked-read implementation with access-aware read-kind selection: instruction fetches use AK_ifetch, ordinary page-walk reads use AK_ttw, and reserved/data reads retain their flag-derived kinds. It retains upstream's permission checks, splitting and fault handling.
• ptw-atomic.sail — shared leaf validation and exclusive-read/conditional-write PTE A/D updates, used by both TLB-hit and TLB-miss paths. VS PTE addresses are G-stage-translated before opening the atomic update window.
• pma-atomic-pte.sail — PMA checking that permits those internal PTE access flags while retaining architectural LR/SC payload validation.
• _CoqProject — the compile order: rv64d_types.v → riscv_extras.v → xv6iris_extras.v → rv64d.v → ModelSmoke.v.
• ModelSmoke.v — concrete checks of configuration validity, the model's full reset chain, ISA reset, host and load-reserved instructions, HS→VS entry, two-stage FP loads/stores, guest faults, HFENCE invalidation, PLIC wire delivery, separate clock/interrupt updates, memory-read event tags, A/D-clear two-stage accesses, fresh-PTE validation, and three-level 4-KiB walks. They run during generation's compile-check and the normal model build, independently of the Iris proof port.

xv6iris_extras.v is hand-written platform support in model-xv6iris/: a regen passes it to Sail using --rocq-lib and never overwrites it. The tracked extern file supplies the bindings that official upstream lacks. Its reservation predicates retain the existing fixed-function interpretation; native LR/SC reservation lifetime and interference remain part of the model/contract port.

The regen needs no cmake: nothing in the model's .sail sources is generated by sail-riscv's build, so the source tree plus those files is everything sail needs. Splice sources are staged under stable relative names, so generated assertion locations contain no checkout or temporary-directory paths.

Review jj diff model-xv6iris/ after regeneration and rebuild the model before its proof dependents. The H-capable upstream also changes translation, traps, register types and decoder coverage. Fetch/page-walk tagging and atomic PTE A/D updates are supplied by the tracked model inputs.

Documentation

• claude-notes/README.md — the entry point to the development notes: build/proof-engineering guidance (durable-notes.md), per-subsystem design docs (claude-notes/design/ — execution model, devices, page tables, interrupts, multi-CPU, kernel-proof architecture, …), and per-effort worklists. Read it before working on the proofs under iris/.
• MANUAL-NOTES.md — high-level ideas and open directions, in note form.
• tools/proof_coverage.py — reports which xv6 kernel functions have a proven spec (python3 tools/proof_coverage.py).
• tools/gen_code.py — generates iris/'s instruction-decode layer (iris/KernelDecode*.v + iris/Code<F>.v) from the tracked image (make gen-code).