Lean verification: prove 164 more functions and fix the kernel bugs the proofs found - #591

Merged

eKisNonos merged 48 commits into

mainfrom

lean/substantive

Sep 30, 2026

Commits on Sep 29, 2026

verification: prove six functions the ratchet counted from names alone
eKisNonos
committed
abf7199
ratchet: count a function as substantive only from theorem statements
eKisNonos
committed
5846987
iommu: refuse a unit whose registers lie past the mapped page
eKisNonos
committed
915d4bb
kernel_proofs: IOMMU register sets past the page are refused
eKisNonos
committed
bd7a1a0
aarch64: a NOP is not a BTI landing pad
eKisNonos
committed
663de9c
kernel_proofs: only real BTI landing pads pass the check
eKisNonos
committed
3e241e1
layout: keep a guard page between every two per-CPU stacks
eKisNonos
committed
483342f
kernel_proofs: no stack guard page is a page of another stack
eKisNonos
committed
941a956
procfs: number pid directories so no two inodes collide
eKisNonos
committed
28db55f
kernel_proofs: procfs pid directory inodes miss every other inode
eKisNonos
committed
558a4fc
pci: mask device and function in the 0xCF8 configuration address
eKisNonos
committed
7e084c3
kernel_proofs: the PCI configuration address stays on its bus
eKisNonos
committed
eee6ae3
multiboot: check all 36 RSDP bytes for the extended checksum
eKisNonos
committed
bb762af
kernel_proofs: the RSDP extended checksum covers every byte
eKisNonos
committed
987845a
memory, acpi, uefi: saturate arithmetic on firmware and counter values
eKisNonos
committed
a3eb0f1
kernel_proofs: firmware and counter arithmetic saturates
eKisNonos
committed
a0fa67c
elf: is_symtab names the full symbol table only
eKisNonos
committed
1184dcb
kernel_proofs: only SHT_SYMTAB passes is_symtab
eKisNonos
committed
981a75c
vga: keep three bits of background so bright colours never blink
eKisNonos
committed
52fd38b
kernel_proofs: no background makes boot VGA text blink
eKisNonos
committed
70cad49
uefi: pack revision constants the way the specification does
eKisNonos
committed
83270d8
kernel_proofs: UEFI revision constants follow the specification
eKisNonos
committed
a76834a
uefi: count the count-based authenticated write flag
eKisNonos
committed
f7229be
kernel_proofs: each authenticated write flag needs authentication
eKisNonos
committed
3c9b455
fs: make ScanConfig::hidden_only admit only hidden files
eKisNonos
committed
bafb454
kernel_proofs: a hidden-only scan admits only hidden files
eKisNonos
committed
78322e4
uefi: check EFI dates against the calendar and count back to 1900
eKisNonos
committed
145d4a0
kernel_proofs: EFI dates follow the calendar and count back to 1900
eKisNonos
committed
ca27380
verification: prove is_user_space is the lower canonical half
eKisNonos
committed
c1edcb5
verification: prove where the VT-d invalidation registers are
eKisNonos
committed
15d97d5
verification: prove where the VT-d fault records are
eKisNonos
committed
975de15
verification: a kernel stack's upper guard page is unmapped
eKisNonos
committed
d546218
verification: prove what the tick counter operations ask of the atomic
eKisNonos
committed
eb1814a
memory: round addresses to any alignment, not only powers of two
eKisNonos
committed
8c38d5e
kernel_proofs: address rounding lands on a multiple of the alignment
eKisNonos
committed
2b2844d
port: saturate the statistics totals rather than abort
eKisNonos
committed
b1eede3
kernel_proofs: port statistics totals saturate
eKisNonos
committed
b46af29

Commits on Sep 30, 2026