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

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 (from the zeldovich/sail-riscv fork — 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/
├── xv6-riscv/       # the kernel sources + built kernel/kernel ELF
├── 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

Everything is driven by the top-level Makefile, which runs all Rocq commands inside the project-local opam switch, so you do not need to eval $(opam env …) yourself.

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 xv6 kernel ELF (xv6-riscv/kernel/kernel)
make user       # build the xv6 user programs (xv6-riscv/user/_*, via fs.img)
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

make audit compiles iris/SystemAssumptions.v, which 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 are checked in but the ELFs are not (xv6-riscv/ is .gitignored), so the Makefile pins the upstream revision they were built from, XV6_REV: the clone rule checks it out detached, and make xv6-rev-check warns if the tree has moved off it. An image built from another revision has different symbol addresses, and every proof naming one breaks — so after any re-dump, check git diff kernel-rocq/. (Re-dumping is otherwise cheap: the dumper leaves an output untouched when its content is unchanged, so it never invalidates a .vo for nothing.)

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 rewrites it, and make check-decode is that regeneration plus a git diff --exit-code, so it FAILS if anything moved. 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. To regenerate (needs the sail compiler with sail_coq_backend) run make model-gen — or tools/regen_sail_model.sh directly; make model-gen prints instructions if sail is missing.

The model comes from a fork, zeldovich/sail-riscv, pinned by SAIL_RISCV_REV in the Makefile at the fork's xv6 branch (its deltas against upstream: the atomic PTE A/D-bit update, coq: bindings on the platform hooks, matching axioms in handwritten_support/riscv_extras.v, and AK_ifetch/AK_ttw tagging of fetches and page-table walks).

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.

Three files decide what comes out, all of them in model-xv6iris/:

• sail-config-rv64d.json — sail-riscv's own config/config.json.in resolved for the rv64d_v256_e64 build, with this project's deviations from the upstream default. The comment at the top documents each one, and the substitutions to redo after an upstream bump.
• sail-modules.txt — the Sail module subset to compile (sail-riscv's SAIL_MODULES, not --all-modules).
• _CoqProject — the compile order: rv64d_types.v → riscv_extras.v → xv6iris_extras.v → rv64d.v.

xv6iris_extras.v is the one hand-written file in model-xv6iris/: a regen passes it to sail as a second --coq-lib and never overwrites it. Its header explains what each hook is realised as and, for the two that stay assumed, why.

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.

On this machine the toolchain is already installed, but not in the switch the proofs build in: sail + sail_coq_backend live in the DEFAULT opam switch (/root/.opam/default/bin/sail), while coqc must stay the project switch's (/shared/xv6rocq). So APPEND the sail switch to PATH rather than prepending it — the default switch also has a coqc, and the regen script compile-checks the result:

export OPAMSWITCH=/shared/xv6rocq && eval $(opam env)
PATH="$PATH:/root/.opam/default/bin" make model-gen

The checkout asks for a newer sail than the one installed here (cmake/sail_required_version.txt vs sail --version); the script notices, passes the version it has to --require-version, and says so. If the sources ever really need the newer compiler, generation fails loudly rather than quietly producing a different model.

A regen takes ~10 min and peaks around 7 GB. Before changing the config or the module list, regen with them UNCHANGED and check git diff model-xv6iris/ is empty: that is the only way to tell an intended effect from upstream drift in the checkout, and the script installs into model-xv6iris/ on success, so git is the comparison. The same trick isolates an upstream bump from a fork delta: generate at the fork point first, then at the fork tip.

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).