verification: grow Lean coverage, extract 558 more functions, fix what the proofs found - #590
Merged
Merged
Conversation
fold_caps was one of the two extracted functions carrying no theorem. The extracted loop is proven against a fold specification, and the word it returns grants a capability exactly when the starting word did or the table lists it. Composed with select_caps, a table folded from zero resolves back to itself. Standard axioms only. proven 421 to 422, substantive 159 to 160, unproven 2 to 1.
The last extracted function with no theorem. An accepted non-empty table has the stride of a program header and ends inside the image, so every header parse_program_header_at reads is in bounds; this assumes only that Option::ok_or returns no value it was not given. On every header whose offset fits a usize the function returns the verdict of Nonos.ElfPhdr, the core corpus model, and a table whose end wraps is refused. The four standard-library calls Aeneas leaves opaque (usize::try_from, map_err, ok_or, size_of) are registered in ASSUMPTIONS.md, and their documented behaviour is a named hypothesis where a theorem needs it. proven 422 to 423, substantive 160 to 161, unproven 1 to 0.
ProcessContext::has_capability is the process branch of the capability gate. It returns true exactly when the mask sits below the process's word in the tier-one delegation order, reads one bit for a single-capability mask, and the empty word holds only the empty mask. A fresh context's decision depends only on its capability argument, and neither privilege predicate calls a missing context a kernel or a process.
from_user and from_kernel read only the RPL bits of the saved CS, and rings one and two are neither. Each page-fault reader tests the one bit the paging constants name; reserved_write is RSVD, not the write bit. The present and write bits decoded here route a fault as the demand-paging model does. Bits.lean holds the shared mask lemmas, without bv_decide.
overlaps is "not disjoint", contains is membership and contains_range is the subset order of Nonos.Interval, for every word. Overlap is symmetric, non-empty ranges overlap exactly when they share an address, and a range inside another keeps its addresses there. An empty range strictly inside another is reported as overlapping though it holds no address; that conservative edge is pinned by two theorems.
In production should_log_debug is false whatever the output level reads, and out of production serial output is on. Debug logging happens exactly out of production at level Debug or above, and never without serial output. Entering production writes the minimal level back, leaving it writes only the flag, and both statics are built for a production start. The atomics stay opaque, and the section says what that leaves out.
within_ceiling, grant_within_manifest and install_caps equal the Nonos.SpawnCaps predicates and installed set for every 64-bit input, so the model's theorems hold of the extracted code: a capsule installs no capability outside its certificate ceiling whatever the grant, passing both checks bounds the grant too, and required capabilities ignore the grant. Bits.lean gains the not, high-bit and zero-word lemmas this needs.
For a power-of-two alignment the region allocator's align_down gives the largest multiple at or below the value, and align_up and align_size the least multiple at or above it, exactly when value + align fits the word. Past that they abort under overflow checks, including the last aligned page below the top whose rounded value would fit, and a zero alignment aborts on align - 1. align_up and align_down were counted by a name collision with another crate and now carry theorems of their own.
Every kernel file with public functions that includes nothing from the rest of the crate and holds no atomic, lock, allocation or unsafe was put through mirror_crate, Charon and Aeneas: 64 files, 96 functions, each regenerated here without drift and carrying its wrapper theorem. Four crates name their Rust module after the crate, because the file stem also named a parameter and the Lean namespace shadowed it. Seven files whose last two path parts collided with each other get longer names. No new axiom appears. Properties beyond the wrappers come next.
The attribute set: containment is the order union defines, intersection holds exactly what both hold, each predicate reads its own bit, and truncation to the low byte changes no defined flag. It also records that the secure boot cache stores DEFAULT_NV_BS_RT instead of the word firmware returned, which contradicts SecureBoot and PK. The memory counters: the mebibyte readings round down and add up, and usage_percent is the rounded ratio, zero on an empty total and aborting exactly past the multiplication bound.
The AW an AGAW programs into a context entry is its level count less two, the VT-d encoding, and distinct AGAWs give distinct widths and depths. Every DMA direction asks for at least one cache maintenance step, the one-way directions for exactly their own. None of the MMU layer's named kernel permission sets is writable and executable or reaches user mode; only kernel_rx executes and only device is uncached.
Each PTE builder sets exactly its own bit and keeps the rest, each reader reads its own, and is_leaf reads R, W or X and nothing else. That records two defects in that predicate, which has no caller: an entry with R set and V clear is called a leaf though is_leaf_entry and the hardware see it as invalid, and so is the reserved W-without-R encoding. The satp modes encode as the privileged specification says and fit the MODE field, and levels and address bits agree; Unknown encodes as Bare, translation off, which address_space::switch would write back if it ever read one.
The pipe length is the ring distance and complements the space left to write, a new pipe is an empty zeroed ring of its capacity, and each endpoint predicate reads only its own counter. remove_reader and remove_writer undo add with no zero guard, which is recorded. A source id splits into bus, device and function and reassembles, at every field edge, and the id constructors return what they were given.
Boot exception contexts, key types, IOMMU device addresses, VGA colour codes, benchmark samples, memory sanitization settings, ELF section kinds and aarch64 translation faults each carry exact theorems on the extracted code. Recorded, because the code does it: the boot context counts vectors 29 and 30 as pushing an error code where the IDT table does not; DeviceAddress::pci does not mask the device to five bits, so device 32 aliases into the bus field; a bright VGA background decodes as blinking; is_symtab accepts SHT_DYNSYM where the bootloader does not; and the FSC decoders miss the FEAT_LPA2 level -1 and level 0 codes.
ACPI RSDP checksums as the twenty-byte sum with exactly one passing checksum byte, SRAT and UEFI memory ranges, PCI addresses and errors, port ranges, stack regions, pipe and inbox types, mmap placement, the constant-time AES table lookup, sanitization levels and stack canaries, and the remaining leaf types each carry exact theorems on the extracted code, each checked against a mutant that breaks it. Recorded where the code does it: SRAT and port range ends saturate so the top address or port is never contained, PciDevice::bdf does not mask its fields, the RSDP table address has no revision gate, and hidden_only changes nothing.
tools/extraction/closure_crate.py follows a file's crate:: and super:: paths, and the pub use re-exports in each mod.rs, to the files that define what it names, and rebuilds that part of the module tree with real directories and #[path] so the included source resolves unchanged. Run over every public-function file with no unsafe, atomic or lock that was not already extracted, 130 closed without an external crate or an unbounded closure: 467 functions, each regenerated here without drift, each with its wrapper theorem, and no new axiom. Where Aeneas names a method after a field it collides with, the wrapper names impl.method. The duplicate-mirror check now also reads a closure crate's target.
Each crate builds in its own directory and translates into its own scratch directory, so regen.py now runs them side by side, one per CPU by default, and prints results in manifest order. All 285 crates regenerate here in two and a half minutes without drift.
Firmware returns errors with bit 63 set, so GetVariable probing a size answers 0x8000000000000005, while the status constants are the bare codes. read_variable_raw compared the raw status against EFI_BUFFER_TOO_SMALL and so refused every variable firmware holds, and from_efi_status mapped every real error to VariableReadFailed. Both now go through status::code, which clears the error bit.
GetVariable fills in the variable's attributes, and both caching paths, get_variable and cache_security_variables, read that word and then cached every variable as DEFAULT_NV_BS_RT (0x07). For SecureBoot, 0x06 in the specification, the cache claimed non-volatile; for PK, KEK, db and dbx, 0x27, it dropped time-based authenticated write. The read now returns the attributes with the data and the cache stores them; read_variable_raw keeps its data-only form for the other callers.
The kernel UEFI manager and variable code are included by path and run against a runtime services table whose GetVariable answers with the specification words (SecureBoot 0x06, PK and dbx 0x27) and the real error encoding (0x8000000000000005 for the size probe). Both tests fail against either old behaviour: the bare status comparison refuses every read, and the default word replaces the reported one.
The theorem about DEFAULT_NV_BS_RT against the firmware words stays; it now says why the cache must keep the word GetVariable returns and points at the kernel_proofs test that checks the cache does.
The classifier matched a function's leaf name anywhere in any refinement file, so a name shared across crates (ct_select_u8, is_present, leaf) counted as proven and substantive without a theorem about it. A name now counts only in files that import its own crate's generated module, and SUBSTANTIVE_FLOOR moves to that count. The one function the tightening left unproven, the ct crate's ct_eq_32, now has a theorem: whenever the call returns, it answers true exactly when the two arrays are equal.
A missing argument, a source that is not a Rust file under src/, a crate name that is not lower case with digits and underscores, or a file bound below one now gives a usage message instead of a traceback.
eKisNonos
force-pushed
the
lean/substantive
branch
from
September 29, 2026 17:09
ccdbd7d to
99b512d
Compare
The extraction gate failed on 18 names. Six were atomics already in the register, printed short because one refinement file opens core.sync.atomic where its axiom profile runs; the open now ends before the profile. The other twelve are new: library calls with no model, and the kernel's own PhysAddr comparison, which only two wrapper theorems reach.
The UEFI cache test includes kernel files that clippy flags: two unsafe functions with their safety note as a line comment, three manual multiple-of tests in is_leap_year and one in as_string, a Default impl a derive covers, and a variable module inside variable. Each is fixed in the kernel and the #[allow] on the test's module is gone. is_leap_year is extracted, so tables_time is regenerated; it now calls Aeneas's modelled U16::is_multiple_of and no axiom appears.
DeviceAddress::pci and PciDevice::bdf shifted the device number into place without masking it to five bits, so device 32 on bus 0 packed as device 0 on bus 1 and named another device's IOMMU context; bdf did not mask the function either. Both now mask device to 0x1F and function to 0x7. No caller passes an out-of-range number today. The extracted crates are regenerated. The theorems that recorded the aliasing now state the exact masked value for every input and that the bus field is the bus whatever device and function are passed.
Runs both kernel encoders over every device and function number and checks the bus, device and function read back. Both tests fail against the unmasked encoders.
exception_has_error_code omitted VMM communication (#VC, 29) and security exception (#SX, 30). Both push an error code, so an entry stub built from the table would read that code as the return address. The boot exception context already listed both. Adds the two vector constants and their names. The theorem that recorded the disagreement now points at a proof that the IDT and boot tables agree on every vector.
Checks exception_has_error_code on every vector against the SDM and APM list. Both tests fail against the table without 29 and 30.
PortRange::contains, SratMemoryAffinity::contains_address and NumaMemoryRegion::contains compared with a saturated end, so a range reaching the top of its space never held its last port or byte. PortRange::overlaps had the same flaw, and reserve_range uses it: a range reserved at 0xFFF0 for 16 ports did not overlap a later request for port 0xFFFF, so that port could be handed out twice. Membership now compares the offset from the start with the count, and overlaps compares the true ends in 32-bit arithmetic. The extracted crates are regenerated and overlaps is added to the types_range entry points. The theorems that recorded the lost last unit now state membership on the true sum for every range, and that two non-empty port ranges overlap exactly when a port lies in both.
AcpiRsdp::table_address returned a nonzero XSDT pointer whatever the revision, although below revision 2 verify_extended_checksum returns true without computing a sum, so the pointer is covered by no checksum. It now returns the RSDT address below revision 2, as the ACPI parser's RsdpExtended::has_xsdt does. The theorem that recorded the unchecked pointer is replaced by one that any address other than the RSDT comes from the XSDT field of a revision 2 or later RSDP.
range_ends runs the kernel's PortRange, SRAT entry and NUMA region at the top of their spaces, including the 0xFFFF double reservation case. rsdp_address checks table_address across revisions. All four tests fail against the saturated ends and the ungated XSDT.
The previous commit left end_address without a caller, and the unreachable check matches by name, so it also reported the UEFI memory descriptor's end_address. contains_address compares with end_address again and falls back to the offset test only where that comparison fails, which is exactly the saturated case. The theorem stating membership on the true sum is reproved against the new shape.
MmuMode::satp_mode encoded Unknown as 0, which is Bare, and address_space::switch re-encoded whatever mmu_mode() read from satp. A switch made before paging was on, or with a satp that read back as an unnamed mode, wrote a satp with translation off and ran the target address space untranslated. satp_mode now returns None for Unknown and make_satp returns an Option. switch and init_mmu encode KERNEL_MMU_MODE, Sv39, the mode every table is built for, which is checked at compile time to have an encoding. The mmu_mode extraction is regenerated and the theorem that recorded the fail-open encoding now states that only Unknown lacks an encoding and only Bare encodes as translation off.
PteFlags::is_leaf read R, W or X and ignored V, so an invalid entry with R set was a leaf, and it accepted W without R, an encoding the privileged specification reserves and that faults. is_leaf now requires V and R or X and rejects W without R; page_table's is_leaf_entry, which had the same reserved-encoding gap, calls it. PteFlags derives Default to satisfy clippy where the file is compiled on the host. The rv_flags extraction is regenerated and the two theorems that recorded the invalid and reserved leaves now state that neither is a leaf, with an exact characterisation over the four permission bits.
Checks that Unknown has no satp encoding, that named modes encode distinctly and the kernel mode is Sv39, and is_leaf over every combination of V, R, W and X. The leaf test fails against the old predicate; the satp test does not build against the old usize encoder.
ProcessFdTable::fork dropped every entry marked close-on-exec, so a child lost those descriptors before it called exec. The flag closes a descriptor at exec, which close_cloexec already does. fork now copies the whole table. No caller forks a table today: fork_fd_table, its only user, has no caller. Also adds Default and uses range contains, which clippy asks for where the file is compiled on the host.
lookup_root parsed a name as an i32 and numbered its directory pid as u64 * 1000 + 100, so the name -1 cast to 2^64 - 1 and overflowed the product: a panic in a debug build, a wrapped inode in a release one. procfs_readdir had the same expression. Both now go through pid_dir_inode, which answers None for a negative pid, and lookup_root accepts only names made of ASCII digits, so +5 no longer aliases 5. pid_dir_inode is its own file so it can be extracted. Its refinement proves it never fails, is None exactly for a negative pid, is pid * 1000 + 100 otherwise, and separates pids.
sys_pipe2 handed its PipeReader and PipeWriter to register_pipe_reader and register_pipe_writer, which were generic and discarded them, so both endpoints were dropped on return and the new pipe had no reader and no writer. The registry now stores each endpoint under its descriptor and unregister_pipe_fd drops it. A failed copy of the descriptor pair to user memory unregisters both. PipeReader::close and PipeWriter::close decremented the count and their Drop decremented it again, so close then drop took the last count past zero to usize::MAX and the pipe reported a reader or writer forever. close now consumes the endpoint so drop is the only decrement, and remove_reader and remove_writer stop at zero. sys_pipe2 still has no caller, and fs::allocate_fd opens a null path, so it cannot succeed yet; that is left as it is. PipeBuffer gains Default and iterator copy loops for clippy on the host. The theorems that recorded the missing zero guard now state that the counts stop at zero.
fd_fork forks a table holding a close-on-exec descriptor and checks it survives until close_cloexec. procfs_inode checks negative pids have no directory inode. pipe_counts removes one reader and writer too many and checks the pipe then has none, and copies bytes across the ring end. The fork and pipe count tests fail against the old code; the procfs test does not build against it, which had no pid_dir_inode.
eKisNonos
changed the title
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Numbers
Percentages are of the 11,450 functions in src/. Target: 1,717 substantive.
The ratchet now counts a function only in refinement files that import its own crate's generated module. Before, a leaf name shared across crates (
new,is_present,leaf,ct_select_u8) counted anywhere, which put main's figure at 159 where the per-crate count was 126. FLOOR is 981, GAP_CEILING is 0, and SUBSTANTIVE_FLOOR is 336, equal to the count. The one function the tighter count left without a theorem, the ct crate'sct_eq_32, now has one: whenever the call returns, it answers true exactly when the two arrays are equal.The two unproven functions
fold_caps: the extracted loop computes the fold of the table's bits; the returned word grants a capability exactly when the starting word or the table does; folding then resolving returns the table. Standard axioms only.program_header_bounds: an accepted non-empty table has the program header stride and ends inside the image, so every read inparse_program_header_atis in bounds, assuming only thatOption::ok_orreturns no value it was not given. On every header whose offset fits a usize the function returns the verdict ofNonos.ElfPhdr. The four opaque standard-library calls (usize::try_from,map_err,ok_or,size_of) are registered in ASSUMPTIONS.md and stated as hypotheses where a theorem needs them.UEFI variable reads: two kernel fixes, with a test
uefi: compare status codes with the error bit cleared. Firmware returns errors with bit 63 set, so the GetVariable size probe answers0x8000000000000005, while the status constants are the bare codes.read_variable_rawcompared the raw status againstEFI_BUFFER_TOO_SMALLand so refused every variable firmware holds;from_efi_statusmapped every real error toVariableReadFailed. Both now go throughstatus::code.uefi: cache the attribute word firmware returns. Both caching paths read the attribute word GetVariable reports and then cached every variable asDEFAULT_NV_BS_RT(0x07): wrong for SecureBoot (0x06, volatile) and for PK, KEK, db and dbx (0x27, time-based authenticated write). No code reads cached attributes today, so nothing depended on the wrong word yet; the first caller that did would have got it.kernel_proofs: the UEFI cache keeps the firmware attribute wordruns the kernel's manager and variable code, included by path, against a runtime services table that answers with the specification's words and error encoding. Both tests fail against either old behaviour.The Lean theorem about
DEFAULT_NV_BS_RTagainst the firmware words is restated to point at the fixed cache and the test.uefi: fix the lints the cache test surfaced, and drop the allow. The test includes kernel UEFI files that clippy flags; all eight findings are fixed in the kernel (safety sections as doc comments,is_multiple_offor the manual multiple-of tests, a derivedDefault, the innervariablemodule renamedentrywithout renaming the file), and the test module carries no#[allow].is_leap_yearis extracted, sotables_timeis regenerated; it now calls Aeneas's modelledU16::is_multiple_ofand no axiom appears.Kernel
cargo check(x86_64, microkernel-core) passes with the same 43 warnings as main. The hygiene checks report no new allow, stub, unreachable site or dark feature.Properties added on extracted code
Spawn gate equals
Nonos.SpawnCaps(no capability outside the certificate ceiling whatever the grant); process capability check is subset order in the tier-one delegation order; trap ring and every page-fault error bit; region overlap equalsNonos.Interval; production mode keeps debug output off; exact rounding of the region alignment helpers and where they abort; IOMMU AW encoding, DMA directions, kernel mapping permissions, RISC-V PTE flags and satp modes; the shared constant-time comparison; and exact properties for 50 further crates. Each property was checked against a mutant of the generated code that makes it false.Extraction
tools/extraction/closure_crate.py: extracts a file with the modules it names throughcrate::andsuper::, rebuilding that part of the module tree with#[path]. 130 files, 467 functions. Arguments go through argparse with validation.regen.pyregenerates crates in parallel. All 285 crates regenerate without drift in about 2.5 minutes on 4 cores.verification: register the axioms the new crates bring inadds to ASSUMPTIONS.md the opaque models the closure crates' wrapper theorems print.Defects the theorems recorded, now fixed
Each fix is its own commit with the extraction regenerated and the recording theorem restated to the fixed behaviour, followed by a
kernel_proofstest that runs the kernel file by#[path]and fails against the old code. Every restated theorem was checked against a mutant of the new generated code that makes it false. None of these had a caller that reached the defect, except the port range overlap, whichreserve_rangeuses.pci: mask device and function when packing a requester id.DeviceAddress::pci(0, 32, 0)packed as bus 1 device 0 and named another device's IOMMU context;PciDevice::bdfalso let function 8 reach the device field. Both mask to five and three bits. Proved: the exact masked value for every input, and the bus field is the bus whatever device and function are passed.idt: vectors 29 and 30 push an error code.exception_has_error_codeomitted #VC and #SX, so a stub built from it would take the error code for the return address. Proved: the IDT table and the boot exception context's table agree on every vector.acpi, port: test range membership against the true end, with the follow-upacpi: keep end_address in the SRAT membership test. PortRange, SRAT and NUMA membership compared with a saturated end, so a range reaching the top never held its last port or byte. The live case: a reservation of 16 ports at 0xFFF0 did not overlap a later request for port 0xFFFF, soreserve_rangecould hand that port out twice.PortRange::overlapsis now extracted. Proved: membership on the true sum for every range, and two non-empty port ranges overlap exactly when a port lies in both. (An empty range is still reported as overlapping a range around its start, which only refuses more; the theorem states that.)multiboot: use the RSDP XSDT field only from revision 2.table_addressreturned a nonzero XSDT pointer from a revision 0 RSDP, whose extended checksum is never computed. Proved: any address other than the RSDT comes from the XSDT field of a revision 2 or later RSDP.riscv64: refuse to encode an unknown satp mode.satp_mode(Unknown)was 0, Bare, andaddress_space::switchre-encoded the live mode, so a switch before paging was on, or with an unreadable satp, ran the target with translation off.satp_modeandmake_satpreturnOption;switchandinit_mmuencodeKERNEL_MMU_MODE(Sv39), checked at compile time to have an encoding. Proved: only Unknown lacks an encoding and only Bare encodes as translation off.riscv64: a leaf PTE is valid, readable or executable, not write-only.PteFlags::is_leafignored V and accepted the reserved W-without-R encoding;page_table.rs::is_leaf_entryshared the second gap and now calls it. Proved: an exact characterisation over V, R, W and X.process: keep close-on-exec descriptors across fork.forkdropped close-on-exec entries, which only exec should close.procfs: refuse a negative pid when numbering its directory. The name-1overflowedpid as u64 * 1000 + 100.pid_dir_inodeis a new extracted function. Proved: never fails,Noneexactly for a negative pid,pid * 1000 + 100otherwise, distinct pids get distinct inodes.pipe: descriptors own their endpoints, and counts stop at zero.sys_pipe2handed its endpoints to registry functions that discarded them, and close followed by drop decremented a count twice, wrapping it tousize::MAX. The registry now owns each endpoint,closeconsumes it, and the counts stop at zero. Proved:remove_readerandremove_writerstore the loaded count less one, or nothing at zero.Found while fixing, not fixed:
fs::allocate_fdopens a null path, sosys_pipe2can only return EMFILE today. It has no caller. The riscv64 build fails on main with 92 resolve errors outside the files touched here, so the RISC-V changes were checked by the host tests overmode.rsandflags.rsand by comparing the riscv64 error list before and after, which is unchanged.Checks run locally
Full extraction
lake build,stated_axioms.py,proven_functions.py,regen.pyover every crate,collect-evidence.shagainst a clean worktree of each proof commit, kernelcargo checkafter every kernel commit (43 warnings, as main),kernel_proofstests (59) and clippy with warnings denied, and the hygiene scripts.