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.

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

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 audit-echo # the same, for the echo application theorem
make audit-tree # the same, for the tree application's closed theorem
make audit-all  # the system and echo audits, run concurrently
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.

make audit-echo is the same audit of the application theorem (iris/EchoAssumptions.v, Print Assumptions UInitBootAdequacy.echo_adequacy_echoΣ), and it is not a duplicate: neither theorem's cone contains the other. The system theorem is the chain at the trivial application and never walks the Uk*/USh*/UInit*/UEcho* user-program tier, so it cannot see an undischarged module parameter hiding behind a seal there. make audit-all runs the two concurrently — they are independent processes over a built tree, so the pair costs the longer of them rather than the sum. CI runs both on every push and reports each list, plus the trusted base of each adequacy statement, in the run's step summary.

make audit-tree is the third of the family (iris/TreeAssumptions.v, Print Assumptions UTreeAdequacy.tree_adequacy_treeΣ) and its cone is walked by neither of the other two. The tree application — subtree ownership as an application claim, claude-notes/design/user-tree.md — is a second closed instance of the whole-system theorem: same machine, same mkfs image, with the file-system claim "the live namespace is a rooted tree partitioned among its owners, or the taint records a move nobody paid for". Its conclusion is reducibility, because that claim's break is a ghost fact no observable event witnesses (§9.3 of that file says why no stronger pure conclusion exists); what the audit checks is that the claim pays every obligation of the theorem at the real image, era 0's included. No program is yet verified against it — the era's first process spends the era's licence and the claim records that at boot.

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, pinned by opam/xv6rocq.export): Rocq 9.0.1, Iris master (rocq-iris dev.2026-09-24.0.8e490959), stdpp master (rocq-stdpp dev.2026-09-17.0.d510b616), rocq-sail-stdpp 0.20.3, plus riscv64-linux-gnu-gcc/objdump and python3 for the images and dumper.

opam/xv6rocq.export is the whole toolchain, exactly (a full, frozen opam switch export; opam/README.md has the package table and the reasons). To set a machine up, or to move a shared switch to a new toolchain, make a fresh switch from it and rebuild every tree from clean -- never opam install into the shared switch, and never upgrade it in place:

opam switch create /shared/xv6rocq ocaml-base-compiler.5.3.0 \
     --repos default,rocq-released=https://rocq-prover.org/opam/released
opam switch import --switch /shared/xv6rocq opam/xv6rocq.export
make toolchain-check          # the switch re-exports byte-identical to the file
for d in model-xv6iris kernel-rocq user-rocq iris; do (cd $d && make -f CoqMakefile cleanall); done
make

make toolchain-check (tools/toolchain_check.sh [SWITCH]) answers "is my switch the one this tree expects?"; a .vo built against a different switch is rejected with inconsistent assumptions, which make cannot see by timestamps. CI imports the same file and keys its switch cache on its hash; the toolchain changes only by changing the file (see opam/README.md).

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.

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.

The regen needs sail 0.20.3 (the version of rocq-sail-stdpp the model compiles against) and z3 on PATH (sail's type checker calls it). One step is not sail's own output: stdpp ≥ 1.13 puts {[ x ]} at level 0, while sail's coq backend emits the record-update notations at level 1, and the two cannot both parse in a file importing the model and stdpp; the script rewrites the generated (at level 1) annotations of rv64d_types.v to level 0 (and fails if one is left). In the agent container z3 is installed (apt) and sail is in the opam switch /work/opam/sail-0.20.3: PATH=$PATH:/work/opam/sail-0.20.3/bin make model-gen (appended, so the proofs' coqc stays the default switch's).

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.

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