A static-partitioning separation kernel for AArch64/EL2, built so that its claims can be checked rather than believed.
⛔ This is a LOG, not status. It is append-only: entries describing something as “next” or
“planned” are records of what was true when written, and are deliberately not updated. For where
the project actually is, read the root README.md’s What this is, honestly.
★ It is kept in full, and moved here rather than trimmed, because the reasoning is the reusable
part — each entry says what was built, why that thing next, and what it cost. That is the record
this project’s whole discipline rests on. It lived in the root README until it was 561 of that
file’s 850 lines, where its own “read this as a log” warning was doing work that a filename can do
better: a reader who opens MILESTONES.md already knows what they are reading.
Where the metal is, in one line: two unmodified Alpine Linux kernels boot on hv-metal’s EL2 with
two vCPUs each, time-slicing one physical CPU, owning no real device MMIO at all and half the
RAM window each, hardware-refused from one another’s memory — with an SMMU denying bus-master DMA by
default in the same machine, all under required CI gates.
hv-core dispatches two toy
hypercalls, driven entirely by hv-sim with deterministic seeded replay. No
hardware, no asm.hv-core), seeded-simulated (hv-sim), and fuzzed (hv-fuzz):
hv-core::evtchn — event channels (interdomain / VIRQ / IPI ports), guarding
interdomain reciprocity, VIRQ uniqueness, and no-signal-on-free.hv-core::grant — grant tables (grant / end / map / unmap / copy), guarding the
core safety rule that a grant with a live mapping cannot be ended, plus
refcount consistency and read-only integrity.hv-core::sched — the scheduler (admit / run / preempt / block / wake / offline)
over a fixed set of physical CPUs, guarding pCPU exclusivity by reciprocity
(a vCPU is Running{pcpu} iff that CPU names it back) plus monotonic per-vCPU
time accounting. Mechanism only — scheduling policy stays above the core.hv-core::Hypervisor — the integrated core: per-domain credit plus all three
subsystems behind one typed, ABI-neutral HvCall dispatch. hv-sim drives the
whole thing through one seam, and one invariants_hold() covers the lot. This is
the real dispatch seam the M5 personality will decode wire-format calls into.All of it is generic and ABI-agnostic — wire formats (the shared_info bitmaps, the
grant_entry structs) stay in the M5 personality. Clean-room provenance discipline
is live here, the first time Xen behavior informs a core design — see
CLEANROOM.md.
hv-core::policy — the layer that picks, above
the dispatch seam (a guest never asks to be scheduled; the tick/idle path does). A
work-conserving, weighted-proportional-fair policy that runs the least-serviced-
per-weight vCPU and time-slices with a quantum, enacting only through the
mechanism’s public transitions. Wake-boost places a vCPU re-entering the
runnable pool (from Blocked, or freshly admitted) at the pool’s floor, so a
long-slept vCPU can’t monopolise a CPU to “catch up” and starve the ones that stayed
runnable — the scheduler’s version of CFS’s place_entity. Unlike a state machine
it has no safety invariant, so it is held to properties instead: work-conservation,
proportional fairness, starvation-freedom, and sleeper fairness.
㉘ machine-checked the first of the four (hv-verify’s
advance_leaves_no_legal_dispatch_unmade, at a bounded shape); the other three remain
property-tested (hv-sim) and fuzzed (hv-fuzz), and two of them — a limit and a claim about
unbounded runs — are not bounded-depth properties, so no larger Kani harness reaches them.
★ The technique is nonetheless scoped rather than unknown: Verus has a TLA embedding
(anvil-verifier/verus-tla) and Anvil used it to verify liveness of Kubernetes controllers,
on the same Verus this repository already gates with.
⚠ “A bad policy is unfair, not unsafe” used to stand here unqualified, and ㉘ is the reason it
no longer does. The work-conservation property was false: a vCPU pinned away from the lowest
idle CPU made the policy recommend a dispatch the mechanism refuses, which advance took as its
break — stalling the machine completely and permanently, every CPU idle with every vCPU
runnable. No invariant was ever violated. Unfairness is not the worst a policy can do; it can
also simply stop.hv-core::p2m — a fourth whole-system state
machine, Xen’s third historical XSA factory after event channels and grant tables.
Every machine frame carries an existence reference count and two typed counts
(allocate / get / put / get_type / put_type / free); the safety invariant is
write-xor-pagetable — get_type refuses a writable reference while a page-table
reference is live and vice-versa, so a frame is never usable as both writable memory
and a page table at once (the exact shape of the PGT_* typecount bugs that let a
guest forge a PTE and escape). Reference coherence (typed ≤ total) and owner
integrity ride alongside; a frame can only be freed once nothing references it. The
reference-moving primitives are internal — the guest-facing surface is only allocate
and free, because a raw “drop a reference” hypercall would let one domain release a
reference another holds; every acquire is balanced by exactly one release, gated on
proof of the acquire, which is how a scalar count stays sound (as in Xen). Folded into
the integrated invariants_hold(), property-tested (hv-core), seeded-simulated
(hv-sim), and fuzzed (hv-fuzz) — the seventh fuzz target. This brings hv-core’s
pure brain to four whole-system state machines, credit accounting, and a
scheduling policy over them — all green on a laptop before any hardware exists.Hypervisor owns the join.P2mPin/P2mUnpin (Xen’s MMUEXT_PIN_TABLE) —
the operation that turns one of a domain’s own frames into a page table, holding a
persistent page-table type reference until unpinned. This is what finally makes the
write-xor-pagetable invariant reachable end-to-end through the dispatch seam: pin a
frame, and a foreign domain’s writable grant map of it is refused (TypePinned) with
the grant map rolled back; conversely a writably-mapped frame cannot be pinned — so a
page is never a page table and writable at once, the exact escape (guest forges a PTE)
the whole p2m module exists to prevent. Unlike the raw type primitives, pin/unpin are
guest-facing and sound: owner-gated, and balanced by a pin bit (unpin proves a prior
pin), the second consumer of the “release gated on proof of acquire” discipline. This
completes the page-type foundation — both halves of the exclusivity are now produced by
real guest operations and exercised across the seed space and fuzzers.evtchn::send set a pending bit, and a vCPU that had
called SchedBlock sat Blocked, so a signal to a sleeping vCPU’s port was a lost
wakeup, the classic bug class. They are now welded at the dispatch seam (subsystems
stay pure and mutually ignorant): a send/unmask that makes a port deliverable
(pending and unmasked) wakes the vCPU it notify-targets if that vCPU is Blocked —
interdomain/unbound ports wake vCPU 0 (Xen’s notify_vcpu_id default), VIRQ/IPI ports
their bound vCPU. A masked port defers the wake to the later unmask. And a block
is refused when a deliverable event already waits — Xen’s SCHEDOP_block re-check —
so a vCPU can’t sleep onto work it already has. The safety invariant — no
deliverable event rests on a Blocked vCPU — is debug-asserted after every dispatch,
holds across 10k seeds (run_seam biases the stream to actually fire the wake, and
observes it), and is fuzzed through the integrated target. Only the scheduler wakeup
is the core’s business; injecting the interrupt into an already-running vCPU stays
the HAL’s job, past the fence.HvCall::DomainDestroy — the whole-system operation
that welds all four subsystems and both seams at once. Tearing a domain down means
closing its every port, offlining its every vCPU, unmapping its every grant map,
revoking its every grant, and unpinning and freeing its every frame — an ordered
sweep built entirely from the existing invariant-safe transitions, so it adds
ordering, not new mutation. It is atomic and unconditional past the authority
gate: a foreign reference into one of the target’s frames — a live grant map, or a
live cross-domain page-table entry — does not block teardown, it is force-reclaimed
by it (the map is drained, the entry severed) before the frames are freed, so no domain
can veto another’s destruction. Every step succeeds by construction, leaving an
empty but still-existent shell (domain slots are fixed-size and never removed; a peer
left Unbound still names a domain that exists). No new standing invariant: a
destroyed domain is verified by postcondition (nothing live points into it), riding
atop the existing net, which already catches every teardown-ordering bug — a freed
port with a live peer trips evtchn reciprocity, a freed on-CPU vCPU trips scheduler
occupancy, a freed foreign-mapped frame trips the grant↔page-type seam, a deliverable
event on an offlined vCPU trips lost-wakeup. Holds across 10k seeds (run_destroy
builds domains up and tears them down mid-flight, reaching both the busy-refusal and
clean-teardown paths) and is fuzzed through the integrated target.DomainDestroy
had no authority check — any domain could destroy any other, a hole under every
memory-isolation invariant. Introduce authority as the third axis after ownership
(a domain acts on its own resources) and consent (grants authorize cross-domain
memory): a per-domain privileged bit (domain 0 boots privileged, as Xen’s dom0 does),
and a gate checked first in domain_destroy — a domain may tear itself down, but
destroying a peer requires being a control domain, else HvError::Denied, a true no-op.
It lives at the dispatch seam because only the integrated core sees both the acting
caller and the target. Authorization is a transition guard, not a state predicate (an
unprivileged peer-destroy would leave a valid state — the point is it must never
happen), so its correctness is “denies/allows correctly, and a denial mutates nothing”:
unit-tested, driven by run_destroy (which now predicts and checks the authority outcome
and witnesses the denied path), and model-checked — the grant↔p2m depth-7 sweep still
closes at exactly 1,143,997 states (the gate adds no reachable states and every denied
destroy is invariant-preserving). A finer capability model (A may control specifically B)
and delegable/mutable privilege are deferred; domain creation / ID reuse remains the
natural next lifecycle step, now with an authority floor to stand on.p2m from a single page-table type into
the full four-level hierarchy (Xen’s PGT_l1..l4). A page-table type now carries its
paging level, and the write-xor invariant generalizes to per-level exclusivity: a
frame is referenced as at most one of {writable, L1, L2, L3, L4}. On top of that sits
the genuinely new invariant — hierarchical type-correctness: P2mLink/P2mUnlink
install and remove page-table entries, stored as explicit edges, and every live
entry must point exactly one level down (an Lk table’s entries reference L(k-1)
tables; an L1’s reference writable leaves). It holds by construction — a link takes a
get_type reference on the child at the required level, so a mislevelled entry (a
writable page where a table belongs, a table at the wrong level) is refused before any
edge is recorded — and it is checked as a standing predicate (MislevelledLink) after
every transition. A link also self-references its parent, so a table stays typed while
it has any entry: it can’t be freed, re-typed, or stranded under its children, and the
child can’t be re-typed or freed under its parent. Because a child always sits one level
below its parent, the page-table graph is a DAG of depth ≤ 4 — no cycle is even
representable. Holds across 10k seeds (run_ptab builds L4→L3→L2→L1→leaf trees and tears
them down, reaching every level), is fuzzed through the integrated target, and folds
into domain teardown (which unlinks a domain’s whole tree before reclaiming its frames).p2m::link now permits a
foreign child (enforcing only the type discipline — the foreign frame is kept alive and
write-locked, so its owner can neither free nor re-type it while the entry maps it), and
the dispatch seam adds the authorization it is blind to. A cross-domain entry is
allowed only when the frame’s owner has granted it to the mapping domain
(grant::authorizes) — Xen’s grant-mapped foreign page — and, at this milestone, is
restricted to L1 leaves (sharing a page-table node was later lifted — see Cross-domain
shared page-table nodes below). A grant can’t be revoked while a
foreign entry relies on it (the frame is in use), and the new cross-subsystem invariant
every cross-domain entry is backed by a live grant of matching permission
(CrossViolation::UnauthorizedForeignLink) is checked after every dispatch — the
page-table↔grant join, the core’s third cross-subsystem seam. It extends domain
teardown too: a domain whose frame is foreign-mapped can’t be destroyed
(has_foreign_link_into, the page-table cousin of the foreign-grant-map precondition),
while a mapper’s own foreign entries are released by the existing unlink_all. Holds
across 10k seeds (run_foreign grants, maps, unlinks, and revokes across the domain
boundary, reaching the authorized, unauthorized, and revoke-blocked paths) and is fuzzed
through the integrated target.L1 leaf now carries the paging
read/write bit, which sharpens the central exclusivity rule from “no reference coexists
with a page-table type” to its exact content: write-xor-pagetable. A writable leaf
holds a Writable type reference on its child (so it can never also be a page table); a
read-only leaf holds only a bare existence reference — a reader is type-agnostic,
exactly as a read-only grant map already is — so it may point at any allocated frame,
including a live page table. That is the linear-map case a guest reading its own page
tables depends on, and it is safe precisely because neither path can write the frame. The
seam authorizes a foreign leaf at its matching permission (a read-write grant for a
writable entry, any grant for a read-only one), refining UnauthorizedForeignLink. The
read-only transition is model-checked exhaustively (the grant↔p2m sweep closes at depth 7
over ≈1.14M states, zero violations, with read-only-onto-page-table reached), witnessed
by the seeded run_ptab/run_foreign drivers, and fuzzed. Shared page-table nodes
(foreign interior entries, not just leaves) landed later — see Cross-domain shared
page-table nodes below.DomainLife { Dead, Live } per slot. Domain 0 boots Live+privileged (the
primordial control domain); every other slot boots Dead. HvCall::DomainCreate {
target, privileged } is Dead→Live, privileged-caller-only, and stamps the new
domain’s authority; DomainDestroy is now Live→Dead and clears privilege on death.
The load-bearing change is a caller-liveness gate: every hypercall requires a Live
caller, checked once centrally — which is what turns “a Dead domain owns nothing” from
teardown’s one-shot postcondition into a standing invariant (a slot that can issue no
hypercall can never acquire a resource to hold), and makes target-liveness fall out for
free (a Dead domain offers no grant and owns no frame, so any op naming one already
fails naturally). Two new standing invariants join the cross-check family:
DeadDomainNotClean (every Dead slot is an empty shell across all four subsystems —
the graduated postcondition) and PrivilegedDeadDomain (privilege implies Live).
The second is the point: privilege is now stateful and constrained, so it is finally
invariant-bearing rather than a bare guard — the sole transition that confers privilege
is DomainCreate, itself privilege-gated, so no domain can self-elevate, a provenance
the model checker confirms by finding no reachable self-elevated state. New errors
NotAlive / AlreadyAlive; authority reuses Denied. dom0 may be destroyed with no
special case (minimal-sound — it just strands the system). Verified end to end: the
seeded run_destroy now cycles domains Dead→Live→Dead→Live and predicts every
create/destroy outcome; a dedicated lifecycle sweep model-checks the standing invariants
exhaustively (closes complete at depth 12 over 10,178 states); and the whole thing is
fuzzed. The grant↔p2m depth-7 sweep re-measures at 715,164 states (down from ≈1.14M:
the liveness gate and creation reshaped the reachable set — a second domain must now be
created before it can act, so the old boot-time two-domain states sit behind a creation
edge), the integrated-core sweep at 382,008 — all clean, zero violations. Finer/delegable
privilege (a capability model, mutable privilege) and domain-ID reuse policy stay
deferred; the lifecycle now has both a birth and a death to build them on.privileged bit
had bundled two powers — “may create domains” and “may destroy any domain” — so split
it. may_create (the honest residue, renamed from privileged, its invariant
PrivilegedDeadDomain → DeadDomainMayCreate) is a global capability gating only
creation, with the same provenance (only a may_create domain confers it, so none
self-elevates). controls[H][T] is the new per-target authority: H may destroy T
specifically — a capability over one named domain, not a blanket privilege. It is
rooted in creation (creating T grants the creator controls[creator][T]) and
delegable (ControlGrant/ControlRevoke hand it to, or take it from, another
domain). Pure least-privilege: no implicit transitivity, so a domain controls exactly
what it created or was delegated — dom0 holds no blanket power over a grandchild it did
not build. Destroy is gated on controls[caller][target] (or self), never a global bit;
a nice consequence is that a Dead domain has no controller, so destroying one is
Denied, indistinguishable from a live-but-uncontrolled peer (no liveness leak). New
standing invariant ControlEdgeDeadEndpoint — every control edge relates two Live
domains — and teardown clears every edge into and out of a domain, so no capability
outlives the domain it named. This is authority made fully invariant-bearing
(design-lessons #9/#10 carried to their conclusion): stateful, per-target, delegable, and
constrained. Flat delegation for now — any controller may delegate or revoke any edge,
sound because edges only ever trace back to a creation root; hierarchical (chain-restricted)
revocation is the deferred refinement. Model-checked exhaustively over every reachable edge
configuration: the lifecycle+delegation sweep closes complete at depth 12 (18,422 states),
the integrated core at depth 5 (415,417), grant↔p2m at depth 7 (738,897) — all zero
violations, with run_destroy and the fuzzer exercising create/destroy/delegate/revoke
and predicting every outcome. A domain capability delegable to specific peers is exactly
the toolstack-domain / driver-domain disaggregation Xen’s XSM/Flask does coarsely — here it
is a checked invariant.Lk table (k >= 2) pointing at another domain’s
L(k-1) table, sharing a whole page-table subtree rather than a single data page. This
is the mechanism behind a real shared address space. The lift is one deleted line: the
only thing forcing leaves was current_type(parent) == PageTable(L1) for a foreign child
in p2m_link; dropping it lets a foreign child sit at any level, authorized by the
unchanged, uniform grant::authorizes(owner, caller, child, writable) — a read-write
grant for a writable entry, any grant for a read-only one — whether the child is a data
page or a table node (design-lesson #6/#8: relaxing a check is sound only because its
replacement invariant already covers the relaxation). Transitive consent is the model
and it falls out of the existing seam rather than being built: UnauthorizedForeignLink
only fires on edges whose parent and child differ in owner, and every edge inside the
owner’s shared subtree is same-owner, so one grant of the node frame authorizes the
caller’s walk into the entire subtree beneath — the caller holds, and needs, no grants of
the leaf frames. On an interior entry writable is the traversal read/write bit the MMU
ANDs down the walk (past the fence): it gates the grant permission required but never
yields a writable type on the node (a node is always typed as a page table), so a
read-only node grant can never produce write access to the leaves beneath. Three
guarantees hold for free, confirmed not assumed: acyclicity (every edge, foreign
included, strictly decreases level, so the cross-domain graph stays a DAG of depth <= 4 —
no cycle representable); teardown & revoke-block (both key on the boundary edge, so
has_foreign_link_into/is_foreign_linked_by already refuse tearing down a domain whose
node a peer shares, or revoking the grant under a live share); and the replacement
invariant itself, which already scanned every edge at every level. Model-checked
exhaustively — the grant<->p2m depth-7 sweep now reaches a foreign interior node share and
everything under it, re-measured at 741,777 states (up from 738,897), closed complete,
zero violations — witnessed by the seeded run_foreign (now sharing and tearing down
cross-domain subtrees, with a node_links reachability witness) across 10k seeds, and
fuzzed through the integrated target.controls as a bare boolean matrix, so any controller could
revoke any edge — its own delegator’s included. Sound (revocation only removes authority)
but a policy wart. Fix it by recording provenance: each cell becomes a Control —
Absent | Root | Via(D) — so each target’s column is a delegation tree rooted at its
creator (Root, stamped at DomainCreate), every delegated edge (Via(D), stamped at
ControlGrant) recording the delegator D that handed it out. ControlRevoke becomes
chain-restricted and cascading: a caller may revoke from only within the subtree it
roots — from == caller (renounce) or a domain the caller delegated to transitively — never
upward at a delegator, sibling, or the Root from below (Denied); and removing an edge
cascades its whole delegated subtree away, so nothing is orphaned. DomainDestroy folds
delegator-death into the same cascade — a torn-down delegator’s Via edges (where it is
neither endpoint) are swept — via one shared fixpoint. Acyclicity comes from the
transition, not an ordering (there is no natural order on domains, unlike page-table
levels): a Via edge only ever attaches a fresh leaf beneath a present delegator, so no
interleaving can close a cycle — which is exactly why ControlGrant must be idempotent and
provenance-preserving (re-parenting an existing controller is the one move that could
forge a cycle). This is the diamond move the capability arc set up (design-lesson #11e): the
stored provenance upgrades “every edge traces to a creation root” from a by-construction
guard property into a checked state invariant, ControlEdgeOrphaned — walking any present
edge’s provenance must terminate at a Root within domain_count steps, catching both an
orphan (a Via whose delegator’s cell went Absent) and a cycle (no Root in bound). It
sits beside ControlEdgeDeadEndpoint (endpoint liveness); neither subsumes the other.
Model-checked exhaustively over a dedicated four-domain create/destroy/delegate world — the
smallest that can form a depth-2 delegation chain (a two-domain world cannot even represent a
Via edge) — closing complete at depth 8 with 30,992 states, zero violations; the
state_key now fingerprints provenance, not mere presence, so no two distinct trees merge.
Witnessed by run_destroy (bumped to four domains) across 10k seeds, which predicts every
revoke outcome via an independent subtree re-derivation and reaches both a chain-restricted
denial (the wart-closing refusal) and a genuine cascade (a revoke that removed a whole
subtree). A delegatee that can no longer strip its delegator, while an ancestor still can and
it cascades, is the disaggregated-toolstack authority Xen’s XSM does coarsely — here a checked
invariant.L1. A leaf terminates the walk and maps an ordinary Writable page; above
L1 it is a superpage — a 2 MiB page mapped directly by an L2 entry, a 1 GiB page by
an L3 — with its size carried by the parent entry’s level, no leaf type of its own (real
hardware’s large pages, and how EPT/Stage-2 map guest RAM). This lands between the two
prior page-table arcs, and naming which is the point. Unlike the nodes arc it is not a
one-line relaxation: leaf-vs-interior was inferred from the parent level (level == L1),
and a superpage makes an L2 entry ambiguous — a read-only superpage in particular
leaves its child untyped, so an L2→untyped-child edge is a legitimate 2 MiB leaf or a
corrupt interior edge, and only stored state tells them apart. So the entry records a
leaf bit — real hardware’s page-size / PS bit — new stored structure (design-lesson
#5), modeled with the existing bool idiom like writable, not a new PageType
(design-lesson #8). But unlike the revocation arc it earns no new named invariant: the
existing MislevelledLink hierarchy invariant generalizes to read the bit (a leaf’s child
is a valid leaf target — Writable-typed if writable, merely allocated if read-only; an
interior entry’s child is the level below), so the honest result is new structure, an
existing invariant generalized, zero new seams. ChildRef/entry_child_ref make link
(which reference to take), unlink (which to give back), and the invariant (which type the
child must be) all derive from one place, so they cannot drift. Three guarantees hold for
free, confirming design-lesson #12 a third time: write-xor-pagetable binds at superpage
size unchanged (a writable 2 MiB leaf pins its child Writable, so it can never also be a
page table); the foreign-link seam — UnauthorizedForeignLink, already a scan over
every edge — authorizes a shared 2 MiB leaf off the one grant a shared 4 KiB leaf needs,
and teardown/revoke-block key on the boundary edge, level- and shape-agnostic; and
acyclicity is untouched because a leaf is terminal (no page-table child to descend).
Frame contiguity/alignment of the 512 sub-frames a real superpage spans is deliberately
abstracted out — a leaf pins one Mfn, and the accounting is identical whether it
stands for 4 KiB or 2 MiB; contiguity is an MMU/allocator concern for hv-metal, not a
brain invariant. Model-checked exhaustively: the enumerator now drives both entry shapes
(required to keep its interior coverage once leaf is explicit) and state_key fingerprints
leaf so a superpage and a small-page mapping of the same frame never merge (design-lesson
#7); the grant<->p2m depth-7 sweep — now building 2 MiB superpage leaves as well as small
pages and node shares — re-measured at 852,085 states (up from 741,777), closed complete,
zero violations (lifecycle depth-12 likewise grew 18,422 → 45,920). Witnessed by the seeded
run_ptab (a superpages reachability witness) and run_foreign (a foreign 2 MiB leaf
shared and authorized by one grant, superpage_links) across the seed space, and fuzzed
through the integrated target. No soundness bug found.DomId is an index into a fixed slot table, and
DomainCreate reuses a Dead slot — so the same id names different domains over time. The
lifecycle arc proved a Dead slot is a clean shell outbound (owns and offers nothing); this
arc closes the inbound direction. Two references survived teardown naming a slot by bare id,
so a reborn tenant silently inherited them — a different security principal served by a
reference made for its predecessor: a grant {grantor:A, grantee:D} outlived D, so a
reborn D' could map it and reach A’s frame (a confused deputy across the reuse boundary);
and close_all(D) returned each interdomain peer to Unbound { remote: D }, so a reborn D'
could bind it, inheriting a channel the peer opened for D. A bare id is a stable identity
only if no reference to a past incarnation survives into the next. Rather than a per-slot
generation counter (Xen’s approach): an unbounded incarnation would break the enumerator’s
finite-state BFS — create/destroy/recreate would split every rebirth into a fresh state and the
search would never close — and it leaves inert dangling references around, against this brain’s
clean-by-construction grain. Instead the lifecycle loop is closed on the inbound direction,
over existing state, no new stored structure: a mint gate (reject_dead_target) refuses
EvtchnAllocUnbound/GrantAccess naming a non-Live target (NotAlive), so no inbound
reference to a Dead slot is ever created; and a teardown sweep clears every other
domain’s Unbound { remote: target } port (clear_unbound_into) and every inbound grant
{grantee: target} (revoke_grants_to), so none survives the domain it named. The new standing
invariant DeadDomainReferenced is the inbound complement of DeadDomainNotClean: together
they say a Dead slot holds nothing and nothing points at it — a truly isolated shell, so a
reborn domain inherits nothing. (A live Interdomain port naming a Dead slot needs no check:
it would already break event-channel reciprocity, since a Dead domain’s ports are all Free.)
Naming which design-lesson shape this is is the point: unlike the prior three page-table arcs
it is a new checked invariant with no new stored structure — the fourth corner of the
structure×invariant matrix (nodes = neither, revocation = both, superpages = structure only),
and a lifecycle-closure in the spirit of the create/destroy arc, carried to the inbound
direction. Model-checked exhaustively by a new reuse_cfg (grants + interdomain channels +
create + destroy — the smallest world that references a slot and reuses it, which the lifecycle
sweep could not represent): closed clean shallow, no violation at the deep 1.5M-state cap. The
coverage is not vacuous — with the mint gate and sweep removed, reuse_cfg surfaces a
counterexample at depth 1 (EvtchnAllocUnbound { remote: 1 } naming the boot-Dead slot 1).
state_key fingerprints liveness and both reference kinds but deliberately carries no
incarnation, so a slot cycled Live→Dead→Live merges with one never destroyed — which keeps
the reachable set finite, and DeadDomainReferenced is what makes that merge sound. Witnessed
by two seeded hv-core cases (a reborn domain inheriting neither a stale grant nor a stale
channel) and the run_destroy seed sweep — which cycles Dead→Live→Dead→Live with inbound
references live and asserts the invariant every step — and fuzzed through the integrated target.
No soundness bug found.Runnable vCPU could be dispatched onto
any idle pCPU. This gives the previously invariant-light scheduler its second safety
invariant. Each vCPU carries a hard-affinity mask (real hardware’s cpumask, Xen’s
cpu_hard_affinity) — the set of pCPUs it may run on — defaulting to all pCPUs so existing
“run anywhere” behaviour is unchanged until narrowed. A new SchedSetAffinity op sets it, and
SchedRun is guarded: a dispatch onto a pCPU outside the mask is refused (NotAffine). The
new standing invariant is “a Running vCPU is always on a pCPU in its affinity set”
(RunningOffAffinity); only two transitions can violate it (dispatch, and narrowing affinity),
and both are guarded, so it holds by construction. Three design calls define the shape: (1)
a per-target control operation — affinity is a resource-management decision (which pCPUs a
domain may use), so setting it is Xen’s XEN_DOMCTL_setvcpuaffinity domctl: a domain may affine
its own vCPUs, but a peer’s requires the caller control that peer
(controls[caller][target]), the same per-target authority gate DomainDestroy uses — the third
isolation axis (after ownership and consent) applied to scheduling. (It shipped self-service
first, the sound core, then had the control axis layered on; the authority check lives at the
seam, so the scheduler subsystem stays authority-agnostic.) This is a transition guard, not a
new state invariant, and the exhaustive sweep confirms it: adding the gate left the
reachable-state count exactly unchanged (a controller reaches only affinity states the domain
could set itself; a denied peer op is a no-op) — the same signature the DomainDestroy gate
showed. (2) Refuse, don’t force-migrate —
setting an affinity that excludes the pCPU a vCPU is currently running on is refused (a no-op),
not resolved by a forced migration; the brain’s gating-precondition style over side-effects (as
teardown refuses-if-busy), which keeps the invariant true by construction and set_affinity a
pure mask write. (3) Reset on offline — because affinity is behaviourally live (it gates
run, unlike runtime, which gates nothing and is dropped from the state fingerprint), offline
resets it to the all-pCPUs default, so a re-admitted vCPU — or one reborn in a reused domain
slot — inherits no stale scheduling constraint. That is a deliberate departure from Xen (which
preserves affinity across offline), made for exactly the reason the domain-ID-reuse arc chose
eager cleanup over a generation counter: a reborn domain must behave identically to a fresh one,
and a behaviourally-live field must not leak across the lifecycle. An empty mask (run nowhere)
is deliberately allowed — an unschedulable vCPU is a liveness/policy concern, not a safety one,
the same dividing line that keeps fairness out of this module. Model-checked exhaustively by a new
affinity_cfg over two pCPUs (so a mask can genuinely exclude one), driving every mask across
every placement: closed clean shallow, and coverage proven non-vacuous — with the run-guard
removed the sweep surfaces RunningOffAffinity immediately. state_key fingerprints the mask
(behaviourally live — design-lesson #7). Witnessed by six hv-core cases and the seeded
run_sched/run_hypervisor mirrors, and fuzzed through the scheduler and integrated targets with
a fuzzed mask so off-affinity dispatches are attempted directly. No soundness bug found.Free, VIRQ uniqueness, no ghost peer), grant tables (5: refcount
coherence, read-only integrity, grantee identity, writable_maps ≤ maps, no dangling map), the
scheduler (5: pCPU-exclusivity reciprocity from both sides + no ghost occupant, and Running
on-affinity), page-type accounting (5: owner integrity, write-xor-pagetable, typed ≤ refs,
pinned ⇒ page-typed, level-correct links), and the nine cross-subsystem seam invariants
(unbacked/misowned grant map, lost wakeup, unauthorized foreign link, a Dead slot
clean/unreferenced/may_create-free, a control edge live-endpointed/rooted-acyclic) — plus the
credit account’s conservation, and the ~10 transition guards proven differently (a guard is
a no-op-on-refusal, not a state predicate — design-lesson #9): the caller-liveness gate, the
reject_dead_target mint gate, the global may_create and per-target controls authority
gates, the revoke chain-restriction, the StaleGrant/Unauthorized seam checks,
the grant_end_access foreign-link block, and the sched_block deliverable re-check. Four
passes. (1) Gap hunt — for every invariant, enumerate every transition that could move the
system toward violating it (design-lesson #3) and confirm each is guarded or maintained by
construction, hunting specifically for a falsification path nothing guards. Every threatening
edge is covered; the subtle ones re-derived and reconfirmed — the grant_end_access /
revoke_grants_to ordering (a foreign page-table link into target’s frame blocks teardown
up front via has_foreign_link_into, and inbound grants are revoked only after the p2m
teardown drops target’s own outward links, so no revoke ever strands a live foreign entry);
the maps_over_frame summation (sound because two grantors with live maps over one frame is
unreachable — the misowned check would fire first, and a live map pins ownership); the cascade
fixpoint (sweep_orphaned_control_edges removes exactly a just-orphaned subtree, and the
provenance walk’s steps > n bound cannot false-positive on a legitimate depth-n chain).
(2) Redundancy / subsumption — no invariant is dead or subsumed. Two deliberate
conservatisms confirmed safe, not unsound: grant_end_access blocks a revoke on any foreign
link by the grantee, not only the one this grant authorizes (a liveness wart, never a hole); and
the L1/L2-only pin universe is isomorphic to L3/L4 (the level logic is a symmetric
match — higher levels add no reachable code path). (3) Cross-invariant interaction — every
feature pair is either model-checked together or provably decomposable: vCPU affinity is
orthogonal to grant/p2m/evtchn (no cross-invariant reads the affinity mask, and no non-scheduler
transition touches scheduler state — so the siloed two-pCPU affinity_cfg is complete), and a
delegated Via control edge drives the identical grant/evtchn teardown a creation Root
edge does (the cascade touches only the control matrix), so the 2-domain all_cfg and the
4-domain delegation_cfg cover it without an intractable four-domain-everything sweep. The
scheduling policy layer is out of scope by construction — it enacts only through the public,
invariant-checked transitions, so the same safety net covers it (its fuzz target re-asserts pCPU
exclusivity). (4) Depth consolidation — the one place verification was a lower bound: the
event↔scheduler and domain-ID-reuse deep sweeps truncated at the 1.5M-state cap. Characterizing
their closing depth showed both close exhaustively at depth 7 (≈2.12M and ≈5.66M states), so
both were upgraded from truncated lower bounds to complete theorems (depth 7, raised cap) —
and because BFS visits shallower depths first, each closure strictly subsumes the earlier
truncated run (which had not even finished the depth-≤7 states) while adding completeness. Every
deep sweep now closes. Outcome: no soundness bug, and none expected — the by-construction
design holds across all 28 invariants × every threatening transition. That is the valid,
valuable result the audit was for: it answers the direction’s own load-bearing question — how
close is the pure brain to “can’t diamond anymore”? — and the honest read is very close. The
remaining headroom is not soundness holes but (a) policy refinement with no safety content
(event-vCPU steering, richer scheduling), (b) breadth the fence defers to M3+ (wider cpumasks,
512-entry tables, the real ABIs), and (c) ever-deeper sweeps with diminishing marginal
confidence. The safety core is essentially complete; what remains is hardware.hv-metal boots under QEMU
(qemu-system-aarch64 -machine virt,virtualization=on, an EL2-capable same-architecture VM on
the Apple-Silicon dev machine) at EL2, and the proven brain now services a hypercall on the
(emulated) bare CPU. The first unsafe, weeks in rather than day one. Landed arc by arc, each one
diamonded + audited in the A→D rhythm:
hv-metal crate
(the one crate that overrides unsafe_code = "forbid"), an aarch64-unknown-none-softfloat
target, cargo xtask qemu/qemu-test, and a required metal boot (QEMU) CI check.src/pl011.rs): init (8N1 + FIFO + TX-enable),
every write gated on TXFF so output can’t drop, and core::fmt::Write — the diagnostic
substrate everything downstream reports through.src/exceptions.rs): confirm CurrentEL == EL2, install
VBAR_EL2 + a 2 KiB-aligned 16-entry vector table, and decode any synchronous fault
(EC/ELR/FAR/ESR) instead of triple-faulting — a fault becomes diagnosable. A
feature-gated BRK self-test asserts the vectors fire (EC=0x3c, vector=4).HCR_EL2.RW=1 (src/el2.rs); realize
hv_hal::TimeSource on the ARM generic timer (CNTPCT_EL0, isb-ordered, monotonicity witnessed
each boot; src/time.rs); supply a #[global_allocator] (a bump allocator over a .bss arena,
src/heap.rs) so hv-core’s alloc links; then link hv-core, construct a real Hypervisor,
and dispatch a synthetic HvCall (dom0 CreditGrant) through the actual Hypervisor::dispatch
path → balance=100. 🔍 Architecture Audit #1 — the fence
(docs/AUDIT-1-HAL-FENCE.md): the hv-hal surface is
architecture-neutral; TimeSource is realized + honored on ARM; GuestMemory/VcpuOps are
deferred to M4 with assumptions named; no soundness defect. Still pre-guest — a guest is M4.AArch64/EL2 is the first backend, chosen to lead because the dev machine is ARM, so it runs
native-architecture under QEMU with no cross-emulation; an x86-64 backend (Intel VMX / EPT, the
LAPIC) is co-equal and follows, behind the same hv-hal fence, per ARM and x86 are co-equal
targets above. Real ARM silicon is deferred until a guest needs validating on hardware (M4+) —
Apple Silicon gates EL2, so the Mac hosts QEMU, not a bare-metal hypervisor. Before reading
anything into an emulated run, see docs/QEMU-AND-METAL.md — the
fidelity contract for QEMU testing: what a green run does (functional refinement of the proven model
— CPU-access isolation) and does not (timing, memory-ordering, DMA/SMMU, errata) tell you, and why
on Apple Silicon Baleen-at-EL2 runs under pure-emulation TCG where that gap is maximal.
hv-core calls, and whose unauthorized memory accesses are faulted by real
Stage-2 tables generated from the proven p2m — the fence becomes real and load-bearing, and the
first isolation content reaches the metal.
docs/ARC-4-TRAP-AND-SERVICE.md): a trivial EL1 guest boots
behind a minimal Stage-2 (HCR_EL2.VM=1 + one 2 MiB identity block, src/guest.rs), issues
HVC, and traps to EL2 (vector slot 8, EC=0x16); a GPR save/restore frame on a dedicated
exception stack (+ a re-entry guard) resumes it. The saved registers are decoded through
hv-core’s RawHypercall/Hypercall::decode seam and routed through the actual
Hypervisor::dispatch; the result is handed back and the guest observes it — echoing the
serviced balance in a final HVC (grant 100, spend 30 → 70; 70 is no call’s input, so
the echo proves the guest saw the serviced result, across two resume cycles). VcpuOps::
set_entry realized on ARM (ELR_EL2); inject_interrupt/GuestMemory honestly deferred.
Three-way converged (spec-derived code + blind Arm-ARM auditor + QEMU). No isolation content.p2m → Stage-2 + the negative-isolation test. ✅ DONE
(docs/AUDIT-2-P2M-STAGE2.md): the guest runs behind real AArch64
Stage-2 tables emitted from the proven p2m (src/stage2.rs, a leaf-reachability refinement of
p2m::link_edges). The model is driven — via the actual Hypervisor::dispatch — into a
two-domain config (guest G, peer P granting G one frame read-write), and the guest runs the
full authorize/deny matrix in one boot (resume-past-fault): its authorized accesses succeed
(writable frame, read-only frame seeded by the now-realized GuestMemory with an un-forgeable
value, foreign granted frame), and every unauthorized access is faulted by the hardware — a
write to a read-only frame → permission fault (EC=0x24, DFSC=0x0F, WnR=1); an un-granted
peer frame, an unmapped IPA, and the guest’s own page-table frame as data (write-xor-pagetable)
→ translation faults (DFSC=0x07), each decoded from ESR_EL2/HPFAR_EL2 and confirmed against
the model. 🔍 Architecture Audit #2 — the model→page-table refinement: the emitted table denies
exactly what the model forbids and permits exactly what it authorizes, across
read / write / foreign(granted) / unmapped / write-xor-pagetable; execute (XN) and superpage are
audited by construction (runtime witness deferred). Three-way converged (spec-derived code + two
spec-blind auditors [AArch64 encodings + the model refinement] + QEMU) — verdict SOUND. A
feature-gated self-test asserts the whole matrix on every boot.docs/ROADMAP.md. (This supersedes
the earlier “PVH Linux via a Xen personality” plan — baleen-xenabi is dropped.)