Which of the Linux kernel's Rust code extracts to LLBC through Charon, the Rust front-end of the Aeneas verification toolchain? The verification pipeline is Charon, then Aeneas, then Lean 4. This repository measures the Charon stage across the whole kernel tree at v7.2-rc2: it inventories every Rust unit, attempts extraction against one shared stub layer, and records where each unit lands and why. It covers Phase 1 and Phase 2 of a larger effort; the Aeneas stage comes later.
The sweep found 122 units, 117 of them in scope (92,308 lines). 13 parse
untrusted input and 12 touch a union, the type Aeneas rejects
(AeneasVerif/aeneas#1199). The Charon pass ran over 40 crate-level extraction
units: 8 extract cleanly, 28 fail, and 4 are out of scope. 27 of the 28 failures
are the same missing-kernel-API error, so coverage is set by how much of the
kernel crate the shared stub models. Self-contained parsing leaves extract
cleanly against that stub, including the union-based binder deserializer; whole
driver crates and the kernel crate itself fail on the first unstubbed kernel::
path.
Phase 1 is in INVENTORY.md, with per-unit data in
inventory.csv. Phases 2 and 3 are in MAP.md, with
per-unit outcomes in results.csv. The shared stub layer is under
stubs/kernel and the harness under tools/. Environment:
kernel v7.2-rc2 (read-only), Charon commit 909ff09a, v0.1.220. Reproduce:
SP=$(mktemp -d); python3 tools/metrics.py > $SP/metrics.csv && python3 tools/classify.py # inventory.csv
python3 tools/run_all.py && python3 tools/finalize.py # results.csv
cd scratch/binder_parse_leaf && charon cargo --preset=aeneas # extract a CLEAN leaf