Nixify the toolchain: flake devShell (pinned Verus + Microkit SDK + aarch64 cross), supersede the Dockerfile plan (ADR-0002)

[quinn-dougherty]

Summary

Adopt a Nix flake (nix develop devShell first) as the pinned, reproducible toolchain for VIS, superseding the "one hash-pinned Dockerfile" approach currently prescribed in CLAUDE.md §5 (Phase 0) and §8 (CI). Track the decision as ADR-0002 in docs/decisions/.

Why this fits VIS specifically

The project's thesis is reproducibility and an enumerable set of trusted inputs (CLAUDE.md §2.5, §4, §8; docs/tcb-ledger.md). A flake's flake.lock is that manifest: every compiler and every downloaded vendor binary is content-addressed by sha256. That is strictly stronger than a Docker image tag (which pins a tag, not the closure) and directly feeds the TCB-provenance story the Phase-4 spec package is meant to ship. For a formal-methods deliverable, the stronger guarantee is load-bearing, not cosmetic.

It also removes friction we already hit during Phase-0 bring-up:

• The Microkit hello-world bring-up had to guess an ARM-toolchain download URL that can 404 over time.
• We currently juggle vendor/arm-gnu-toolchain-*/bin on PATH plus a ./verus symlink into gitignored vendor/. nix develop replaces all of that with one hermetic shell.

Feasibility of the toolchain inputs

• Already in nixpkgs (one line each): qemu, z3, dtc, uv, TLA+/TLC tooling, and pkgsCross.aarch64-* cross-GCC.
• Verus (0.2026.07.05.49b8806, currently fetched as a GitHub release zip): not in nixpkgs yet, but there is an upstream in-progress flake.nix (Nix devshell verus-lang/verus#1231) and an open nixpkgs package request (Package request: verus NixOS/nixpkgs#309393). Fallback: fetchurl the pinned release + autoPatchelf (it bundles its own z3) — the same blob we already download.
• Microkit SDK (2.2.0, prebuilt tarball): seL4/Microkit's dev env explicitly supports Nix setups; package it as fetchurl + autoPatchelfHook.

Net: the majority is nixpkgs; the two vendor blobs (Verus, Microkit) become pinned fetchurl derivations, which is strictly more honest than the ad-hoc curls we do today.

Costs / risks (honest accounting)

1. Writing + maintaining the two blob derivations; autoPatchelf on prebuilt ELFs can need iteration.
2. Supersedes the Dockerfile decision baked into §5/§8 → requires an ADR (irreversible-ish tooling choice per §4). Note it is not either/or: a flake can emit an OCI image via dockerTools, so we keep a Docker artifact for anyone who wants one.
3. Onboarding curve for the convened experts (seL4 / Verus / TLA+ reviewers, §6) who may not use Nix — mitigated by nix develop being a single command.

Proposed scope (devShell-first)

• flake.nix providing a nix develop shell pinning: Verus 0.2026.07.05.49b8806, Microkit SDK 2.2.0, aarch64 cross-GCC (or aarch64-none-elf), qemu, z3, uv, TLA+/TLC, make/dtc/pdftotext.
• Pin the two vendor blobs (Verus, Microkit) via fetchurl + sha256; drop the ./verus symlink and vendor/ PATH juggling.
• Wire ci/verify-all.sh and platform/qemu/run-hello.sh to run under nix develop -c ... identically local and in CI.
• Acceptance: nix develop -c ./ci/verify-all.sh reproduces the kv-alloc Verus proof green (7 verified, 0 errors) AND nix develop -c bash platform/qemu/run-hello.sh boots Microkit to the hello, world banner — both from a clean checkout.
• Write ADR-0002 (supersede the "one Dockerfile" line in §5/§8; record the dockerTools image as the optional Docker output).
• Defer full hermetic package builds of the crates/image to a follow-up; devShell is the MVP.

Out of scope (for this issue)

• Full hermetic Nix builds of every crate / the seL4 image (follow-up).
• NixOS-as-host or CI runner migration.

References

• Nix devshell verus-lang/verus#1231 (upstream Verus flake, in progress)
• Package request: verus NixOS/nixpkgs#309393 (Verus package request)
• seL4/Microkit build & dev docs (Nix-supported dev env)
• nixpkgs pkgsCross.aarch64-* for the cross toolchain

Context: discussed during Phase-0 wrap-up after Gate G0 (kv-alloc proofs green, invariants v1, Microkit hello-world booting in QEMU). Filed per request.

[quinn-dougherty]

For the crate builds specifically, use nix-cargo-integration (nci) rather than hand-rolling derivations.

Why it fits crates/:

• It's a flake-parts module (inputs.nci.url = "github:90-008/nix-cargo-integration", imported into mkFlake) — composes cleanly with the devShell-first flake proposed above, so the per-crate build story and the shared devShell live in one place.
• Native Cargo workspace support — our crates/ (kv-alloc, scheduler, common, request-fsm, gateway, validator, sel4-sys-spec) become a single workspace nci understands, with per-crate packages + a combined dev shell for free.
• Custom toolchain override — needed because Verus pins a specific Rust toolchain (currently 1.96.0); nci lets us feed that exact rustc in rather than nixpkgs default.
• dream2nix-based (not crane) with sensible defaults, so low config burden.

One wrinkle to design around (Verus is not plain cargo): nci builds/tests the Cargo side, but our verification step is a separate verus src/main.rs invocation against the pinned Verus binary, not cargo build. So the split is:

• nci → the crate build/dev-shell/toolchain plumbing (and ordinary cargo/rust-analyzer ergonomics).
• Verus verification → a separate derivation/check that runs the pinned verus (the fetchurl blob from the parent issue) over each crate, wired as a nix flake check so nix develop -c ./ci/verify-all.sh and a pure nix flake check both gate on proofs.

This keeps the acceptance test in the parent issue intact — nix flake check should reproduce kv-alloc green (7 verified, 0 errors) — while nci handles everything that is standard cargo. Fits the "full hermetic crate builds" follow-up I marked out-of-scope above; the devShell MVP doesn't strictly need it, but nci is the right tool the moment we do that follow-up.