verification: grow Lean coverage, extract 558 more functions, fix what the proofs found - #590

Merged

eKisNonos merged 40 commits into

mainfrom

lean/substantive

Sep 29, 2026

Commits on Sep 29, 2026

verification: prove fold_caps ORs in exactly the table's bits
eKisNonos
committed
5ec52ff
verification: prove program_header_bounds keeps the table in the image
eKisNonos
committed
8a85db6
verification: a process holds a capability mask only bit for bit
eKisNonos
committed
64ea062
verification: which ring a trap came from, and which fault bit is which
eKisNonos
committed
0b740dc
verification: the region range algebra is the tier-one interval algebra
eKisNonos
committed
e38ea52
verification: production mode keeps debug output off whatever the level
eKisNonos
committed
d4f31d0
verification: the spawn gate computes the tier-one spawn model exactly
eKisNonos
committed
5d5f89e
verification: exact rounding and the abort edge of the region helpers
eKisNonos
committed
01cc565
verification: extract 64 more self-contained kernel files
eKisNonos
committed
c1de768
verification: the UEFI attribute set and the memory counters
eKisNonos
committed
4414383
verification: IOMMU widths, DMA directions and kernel permissions
eKisNonos
committed
4fb5dad
verification: RISC-V PTE flags bit by bit, and the satp mode encoding
eKisNonos
committed
e442726
verification: pipe buffer counters and IOMMU requester ids
eKisNonos
committed
f5f9c84
verification: eight more crates, with the disagreements they expose
eKisNonos
committed
7748e47
verification: twenty-one more crates carry properties of their own
eKisNonos
committed
6524025
verification: extract 130 kernel files with the modules they name
eKisNonos
committed
0259a39
verification: regenerate extraction crates in parallel
eKisNonos
committed
5388147
uefi: compare status codes with the error bit cleared
eKisNonos
committed
4a753c3
uefi: cache the attribute word firmware returns
eKisNonos
committed
0a0162c
kernel_proofs: the UEFI cache keeps the firmware attribute word
eKisNonos
committed
edfec58
verification: restate the UEFI theorem now the cache keeps the word
eKisNonos
committed
bedb377
verification: count a function only in its own crate's proof files
eKisNonos
committed
2f6ffa7
tools: closure_crate.py takes its arguments through argparse
eKisNonos
committed
99b512d
verification: register the axioms the new crates bring in
eKisNonos
committed
5586b90
uefi: fix the lints the cache test surfaced, and drop the allow
eKisNonos
committed
aeec6ec
pci: mask device and function when packing a requester id
eKisNonos
committed
44489ac
kernel_proofs: PCI requester ids stay on their bus
eKisNonos
committed
87c8d21
idt: vectors 29 and 30 push an error code
eKisNonos
committed
82e345e
kernel_proofs: the IDT error-code table is the architectural one
eKisNonos
committed
488a7a8
acpi, port: test range membership against the true end
eKisNonos
committed
00a281a
multiboot: use the RSDP XSDT field only from revision 2
eKisNonos
committed
dc8e97f
kernel_proofs: ranges hold their last unit, RSDP gates the XSDT
eKisNonos
committed
6c3f068
acpi: keep end_address in the SRAT membership test
eKisNonos
committed
eb30946
riscv64: refuse to encode an unknown satp mode
eKisNonos
committed
8ccfd3d
riscv64: a leaf PTE is valid, readable or executable, not write-only
eKisNonos
committed
0cd88ec
kernel_proofs: RISC-V satp and leaf encodings fail closed
eKisNonos
committed
ac08987
process: keep close-on-exec descriptors across fork
eKisNonos
committed
ca99e8b
procfs: refuse a negative pid when numbering its directory
eKisNonos
committed
eddefbf
pipe: descriptors own their endpoints, and counts stop at zero
eKisNonos
committed
3615b61
kernel_proofs: fork, procfs pid inodes and pipe counts
eKisNonos
committed
81001af