remnient / romulus

Lean 4 model of hypervisor physical page ownership. It has an
executable transition system, a two level page table and MMU, an event
and scheduler layer and machine checked isolation theorems
Mappings are a two level `PageTable` walked by `walk`. When a table
represents the machine, every successful walk is authorised:
 [code] 
`access` is the same walk behind a cache. `accessWithFill` returns the frame and
updated state, installing the mapping's exact permissions on a successful cache
miss. Hits retain the state and denied accesses return an error. The operation
preserves `WellFormed`, and a fill is authorised by the current mapping. Cached
access authorisation requires coherence because revocation retains stale entries
until a flush.
`reclaimFrame` constructs a finite hypercall trace for an owned, unpinned frame.
It begins reclamation, revokes capabilities for the frame, removes its remaining
mappings, flushes every guest page and reclaims the frame. `reclaimFrame_succeeds`
proves that this trace executes from any such `WellFormed` state, preserves the
invariant, zeroes the contents and increments the epoch. This is a sequential
cleanup construction with a full cache flush, and assumes no intervening calls.
Every hypercall, event and finite execution preserves `WellFormed`:
 [code] 
Guest isolation is noninterference over a guesta translations, reads, ownership
and notices. An unrelated step preserves it and access outcomes with it:
 [code] 
`observable_change_requires_affects` declassifies the only intended content
channel. `no_timing_channel` shows unrelated events never change a guests view,
whatever their number or order while devices are guests bounded by the same
authorisation + reclamation + revocation safety are proved separately.
## Example
Guest 0 shares frame 0 read only with guest 1. Guest 1's read access succeeds,
its write access faults and a writable mapping is rejected:
 [code]