allod/archetypes

Watch

Fork 0

Select the guest module from the inventory runtime fact #23

Merged

vnprc merged 5 commits from agent/runtime-guest-module-selection into master

2026-07-31 06:14:38 +01:00

allod-agent commented

2026-07-31 04:52:38 +01:00

Member

Makes the inventory runtime fact decide which guest module a machine composes. Before this, flake.nix hard-coded vm.nixosModules.qemuGuest into every dev and privacy VM, so a machine declaring microvm still built as an ordinary libvirt guest and the fact labelled a build it could not affect.

guestModuleFor maps the fact to a guest module and throws on anything it cannot map. There is no default branch — a fallback is precisely what made the fact decorative.

Two commits, and the split is the validation argument rather than tidiness. The first bumps the inventory and vm inputs, which are prerequisites: the locked inventory predates the runtime fact, so machines.<name>.runtime cannot resolve, and the locked vm predates the guest-module split, so there is no microvmGuest to select. The second makes the selection. Comparing derivation paths across the second commit attributes any difference to the selection alone; comparing across the PR would conflate the two and could not.

Closes #22
Refs allod/strategy#20

Risk

R2. The libvirt path — the entire current fleet — is a measured no-op, and the microvm branch is unreachable from real data: no inventory machine declares microvm, and one that did would fail evaluation on allod/vm's persistent-volume contract until that milestone lands. That fail-closed state is intended, not an oversight. Both guest modules are already contract-checked in allod/vm; this PR selects between two proven modules rather than defining guest behavior. Rollback is a straight revert of either or both commits.

Scored below the parent plan's R3 row for archetypes guest integration because that row covers all of milestone 4 — credentials, volumes, networking, extendModules, nested boot. It would flip to R3 if a fresh evaluation moved any current derivation, or if real inventory data made the microvm branch reachable.

Validation

nix flake check green, 10 checks. System derivations unchanged across the selection commit:

allod-dev   /nix/store/1lhcxfhy9iddfssp3df3r2zwkwnd3ilm-nixos-system-allod-dev-25.11.20260630.b6018f8.drv
privacy-1   /nix/store/zzzaralwv032jdmbqc1q6ms9fm15w7yf-nixos-system-privacy-1-25.11.20260630.b6018f8.drv
nexus       /nix/store/fad4pq24f8iavzr3q369alz8932jq9q3-nixos-system-nexus-25.11.20260630.b6018f8.drv

nixpkgs and disko are identical at both vm revisions, which is why the bump lands clean — archetypes sets nixpkgs.follows = "vm/nixpkgs", so a vm bump that moved nixpkgs would have moved the whole fleet.

The new runtime-module-selection check compares two independently derived facts: the inventory declaration, and the marker each guest module sets on itself (qemu-guest.nix sets [ "libvirt" ], microvm-guest.nix sets [ "microvm" ]). A selector that ignored its input would report [ "libvirt" ] against a declared "microvm" and fail. Four negative cases fail as intended, including a microvm guest missing its persistent volume — that one is what proves the fixtures' toplevel forcing is real work, since NixOS assertions hang off baseSystemAssertWarn and reading the marker alone leaves allod/vm's contracts unevaluated.

Non-vacuity was checked by sabotage in both directions — see the residual-risk section below.

Residual risk worth a human eye

Both sabotage directions pin cleanly since 50681fb. Mapping libvirt to the microvm guest reports composed guest runtime disagrees with the declared inventory fact for: allod-dev, privacy-1; mapping microvm to the qemu guest reports a machine declaring microvm composed libvirt. The selection comparison reads the marker off an unforced, volume-free fixture, so a wrongly selected module surfaces as the mismatch rather than as an unmatched microvm.volumes definition. The volume-bearing fixture is retained only for forcing allod/vm's contracts.

The vm bump adds microvm.nix and its own spectrum input (git+https://spectrum-os.org/git/spectrum, rev 24c4346e) to the lock graph. That is upstream's dependency arriving through allod/vm's sole pin, as the parent plan's contract 1a intends, but it is a new fetch source and worth a look.

vmFacts.<name>.runtime (parent contract 1) is deliberately not exported here — it changes a public output consumed host-side by nexus and interacts with the vm-facts-coherence projections. It belongs with the consumers that need it.

Issue corrections

Three claims in #22 did not survive checking, and the plan records them: inventory.lib.vmRuntimes does not exist anywhere (the capability is real via inventory.machines.<name>.runtime, which forces the same validation chain); the issue's out-of-scope volume declarations contradict its own microvm validation criterion, resolved by having the fixture supply a placeholder the builder does not; and "every piece already exists and is merged" was true of the source repos but not of this one, whose lock pinned both inputs too early.

Plan: allod/strategy dev-plans/runtime-guest-module-selection.md, reviewed by gpt-5.6-sol at high effort — 3 high and 1 medium finding, all folded in before implementation.

A dev microVM needs persistent storage (parent contract 13: the user's home and /nix/var/nix). This PR does not declare those volumes, so a machine selecting microvm fails to evaluate rather than building something unusable — fail-closed, not a supported configuration. Whether those declarations belong here is an open scope question raised in the comments.

Makes the inventory `runtime` fact decide which guest module a machine composes. Before this, `flake.nix` hard-coded `vm.nixosModules.qemuGuest` into every dev and privacy VM, so a machine declaring `microvm` still built as an ordinary libvirt guest and the fact labelled a build it could not affect. `guestModuleFor` maps the fact to a guest module and throws on anything it cannot map. There is no default branch — a fallback is precisely what made the fact decorative. Two commits, and the split is the validation argument rather than tidiness. The first bumps the `inventory` and `vm` inputs, which are prerequisites: the locked `inventory` predates the runtime fact, so `machines.<name>.runtime` cannot resolve, and the locked `vm` predates the guest-module split, so there is no `microvmGuest` to select. The second makes the selection. Comparing derivation paths across the second commit attributes any difference to the selection alone; comparing across the PR would conflate the two and could not. Closes #22 Refs allod/strategy#20 ## Risk R2. The libvirt path — the entire current fleet — is a measured no-op, and the microvm branch is unreachable from real data: no inventory machine declares `microvm`, and one that did would fail evaluation on allod/vm's persistent-volume contract until that milestone lands. That fail-closed state is intended, not an oversight. Both guest modules are already contract-checked in `allod/vm`; this PR selects between two proven modules rather than defining guest behavior. Rollback is a straight revert of either or both commits. Scored below the parent plan's R3 row for archetypes guest integration because that row covers all of milestone 4 — credentials, volumes, networking, `extendModules`, nested boot. It would flip to R3 if a fresh evaluation moved any current derivation, or if real inventory data made the microvm branch reachable. ## Validation `nix flake check` green, 10 checks. System derivations unchanged across the selection commit: ``` allod-dev /nix/store/1lhcxfhy9iddfssp3df3r2zwkwnd3ilm-nixos-system-allod-dev-25.11.20260630.b6018f8.drv privacy-1 /nix/store/zzzaralwv032jdmbqc1q6ms9fm15w7yf-nixos-system-privacy-1-25.11.20260630.b6018f8.drv nexus /nix/store/fad4pq24f8iavzr3q369alz8932jq9q3-nixos-system-nexus-25.11.20260630.b6018f8.drv ``` `nixpkgs` and `disko` are identical at both `vm` revisions, which is why the bump lands clean — `archetypes` sets `nixpkgs.follows = "vm/nixpkgs"`, so a `vm` bump that moved nixpkgs would have moved the whole fleet. The new `runtime-module-selection` check compares two independently derived facts: the inventory declaration, and the marker each guest module sets on itself (`qemu-guest.nix` sets `[ "libvirt" ]`, `microvm-guest.nix` sets `[ "microvm" ]`). A selector that ignored its input would report `[ "libvirt" ]` against a declared `"microvm"` and fail. Four negative cases fail as intended, including a microvm guest missing its persistent volume — that one is what proves the fixtures' toplevel forcing is real work, since NixOS assertions hang off `baseSystemAssertWarn` and reading the marker alone leaves allod/vm's contracts unevaluated. Non-vacuity was checked by sabotage in both directions — see the residual-risk section below. ## Residual risk worth a human eye Both sabotage directions pin cleanly since 50681fb. Mapping `libvirt` to the microvm guest reports `composed guest runtime disagrees with the declared inventory fact for: allod-dev, privacy-1`; mapping `microvm` to the qemu guest reports `a machine declaring microvm composed libvirt`. The selection comparison reads the marker off an unforced, volume-free fixture, so a wrongly selected module surfaces as the mismatch rather than as an unmatched `microvm.volumes` definition. The volume-bearing fixture is retained only for forcing allod/vm's contracts. The `vm` bump adds microvm.nix and its own `spectrum` input (`git+https://spectrum-os.org/git/spectrum`, rev `24c4346e`) to the lock graph. That is upstream's dependency arriving through allod/vm's sole pin, as the parent plan's contract 1a intends, but it is a new fetch source and worth a look. `vmFacts.<name>.runtime` (parent contract 1) is deliberately not exported here — it changes a public output consumed host-side by `nexus` and interacts with the `vm-facts-coherence` projections. It belongs with the consumers that need it. ## Issue corrections Three claims in #22 did not survive checking, and the plan records them: `inventory.lib.vmRuntimes` does not exist anywhere (the capability is real via `inventory.machines.<name>.runtime`, which forces the same validation chain); the issue's out-of-scope volume declarations contradict its own microvm validation criterion, resolved by having the fixture supply a placeholder the builder does not; and "every piece already exists and is merged" was true of the source repos but not of this one, whose lock pinned both inputs too early. Plan: `allod/strategy` `dev-plans/runtime-guest-module-selection.md`, reviewed by `gpt-5.6-sol` at `high` effort — 3 high and 1 medium finding, all folded in before implementation. A dev microVM needs persistent storage (parent contract 13: the user's home and `/nix/var/nix`). This PR does not declare those volumes, so a machine selecting `microvm` fails to evaluate rather than building something unusable — fail-closed, not a supported configuration. Whether those declarations belong here is an open scope question raised in the comments.

allod-agent added 2 commits

2026-07-31 04:52:38 +01:00

Bump inventory and vm inputs for the runtime fact and microvm guest module 34fae4fe05

Prerequisite for selecting the guest module from the inventory runtime
fact. The locked inventory predates the runtime fact and the locked vm
predates the guest-module split, so neither the selection nor its check
can be written against the previous lock.

Proven no-op: nixpkgs and disko are identical at both vm revisions, and
every machine's system derivation is unchanged.

  allod-dev  1lhcxfhy9iddfssp3df3r2zwkwnd3ilm
  privacy-1  zzzaralwv032jdmbqc1q6ms9fm15w7yf
  nexus      fad4pq24f8iavzr3q369alz8932jq9q3

Refs allod/strategy#20

Select the guest module from the inventory runtime fact dfde18f258

Every machine composed vm.nixosModules.qemuGuest regardless of what
inventory declared, so the runtime fact labelled a build it could not
affect. guestModuleFor now maps the fact to a guest module and throws on
anything it cannot map, with no default branch.

mkDevVm and mkPrivacyVm take an optional runtime defaulting to the
machine's declared fact, matching the optional-argument idiom the token
arguments already use. That lets the new check drive the production
selector with a runtime no inventory machine declares, rather than a
copy of it.

The runtime-module-selection check compares two independently derived
facts: the inventory declaration and the marker each guest module sets
on itself. Every fixture forces system.build.toplevel, because NixOS
assertions hang off baseSystemAssertWarn there and the marker alone
leaves allod/vm's guest contracts unevaluated. Four negative cases fail
as intended, including a microvm guest missing its persistent volume,
which is what proves the forcing is real work.

Hypervisors are excluded: they compose no guest module and declare no
runtime, so nexus is covered by the derivation comparison instead.
Inventory keeps enum validation; its mutation check is a build
dependency here rather than a claim restated in a comment.

Proven no-op for the fleet - derivations unchanged from the lock bump:

  allod-dev  1lhcxfhy9iddfssp3df3r2zwkwnd3ilm
  privacy-1  zzzaralwv032jdmbqc1q6ms9fm15w7yf
  nexus      fad4pq24f8iavzr3q369alz8932jq9q3

Refs allod/strategy#20

allod-agent referenced this pull request from allod/strategy

2026-07-31 04:52:55 +01:00

Add the runtime-selected guest module plan #26

allod-agent referenced this pull request

2026-07-31 04:53:15 +01:00

Select the guest module from the inventory runtime fact #22

allod-agent referenced this pull request from allod/memory

2026-07-31 04:54:22 +01:00

Record that reading a config option does not force NixOS assertions #38

vnprc reviewed

2026-07-31 05:13:35 +01:00

allod-agent added 1 commit

2026-07-31 05:20:16 +01:00

Pin the selection check in both directions and guard the hypervisor boundary 50681fbd61

Review feedback. The microvm sabotage direction could not be pinned:
the fixture carried a volume placeholder, which is meaningless under a
qemu guest, so a wrongly selected module surfaced as an unmatched
option definition during option-tree construction rather than as the
mismatch the check names.

The marker needs no volume - it reads off an unforced configuration -
so the selection comparison now uses the volume-free fixture and the
volume-bearing one is kept only for forcing allod/vm's contracts.
Sabotaging microvm to the qemu guest now reports: a machine declaring
microvm composed libvirt. The libvirt direction still names its
machines.

Also closes the hypervisor boundary the plan asked for and the first
implementation left to call-site discipline: hypervisors compose no
guest module, so the marker option must stay undeclared on them. Read
with hasAttrByPath rather than tryEval, since an undeclared option is a
raw attribute error tryEval does not catch.

Refs allod/strategy#20

allod-agent commented

2026-07-31 05:20:36 +01:00

Author

Member

A driveless dev microVM was never the design — you are right

The parent plan is explicit. Contract 6a: a guest that cannot realise a store path "cannot run nix build, nix flake check, or nix flake update" and so "does not do the job the archetype exists for". Contract 13 names the required set for the dev archetype as the user's home plus /nix/var/nix. The scope section says the framework declares those mount points.

So nothing here proposes shipping a driveless dev microVM. What this PR deferred was archetypes declaring the volumes, and the effect is that a machine selecting microvm fails to evaluate rather than building something unusable. No driveless dev microVM can be produced. That is the fail-closed state, not a supported configuration.

The open question is whether the split was worth making at all, which is the scope question at the bottom.

The disk does not break the circularity — not forcing the toplevel does

A real disk behaves exactly like the placeholder. The problem was never that the image was fake; it was that a microvm.volumes declaration is meaningless under a qemu guest, so once the wrong module is selected the definition is unmatched and Nix raises that while assembling the option tree, before any value is read.

What actually breaks it: the marker does not need a volume. Measured directly on an unforced configuration with nothing declared:

{"libvirtNoVolume":["libvirt"],"microvmNoVolume":["microvm"]}

So the two jobs are now split. The selection comparison uses the volume-free fixture and stays pinned in both directions. The volume-bearing fixture is kept only for forcing allod/vm's contracts, which is where a volume is genuinely required.

Sabotaging the direction that previously could not be pinned now reports:

error: runtime-module-selection: a machine declaring microvm composed libvirt

The other direction still names its machines: composed guest runtime disagrees with the declared inventory fact for: allod-dev, privacy-1. The caveat in this PR's description is obsolete and the code comment explaining it is gone.

The hypervisor gap is closed here

The plan said to guard the boundary rather than leave it to call-site discipline, and the first implementation left it to call-site discipline. Now the check asserts hypervisors keep the guest-runtime marker undeclared, so a later refactor routing mkHypervisor through sharedModules fails here instead of at whatever consumer notices first.

Read with lib.hasAttrByPath, not tryEval — an undeclared option is a raw attribute error, which tryEval does not catch. That is the same harness bound the plan records for the negative cases.

Still green

nix flake check passes 10 checks and the fleet derivations are unchanged from the lock bump.

Scope question for you

Do the volume declarations come into this PR, or stay a separate change?

Argument for here: it is the difference between an interface and a usable machine, and the fixture placeholder disappears once real declarations exist.

Argument against: contract 13 puts the image path in deployment data — "the private deployer explicitly creates, formats, labels, owns by that VM's runner principal, and assigns the image before enabling the VM" — so the public repo cannot declare a complete volume entry on its own. Landing half of it here would leave a second placeholder behind, which is what this change just removed.

That is a boundary judgement I should not make alone, so tell me which way and whether the follow-up belongs in a private repo.

Review feedback received: a dev microVM with no drive is useless and was never the design; can the circular logic be broken with a disk; how does the hypervisor gap get closed. Two of the three are fixed in 50681fb. The third is a scope question for you, below. ## A driveless dev microVM was never the design — you are right The parent plan is explicit. Contract 6a: a guest that cannot realise a store path "cannot run `nix build`, `nix flake check`, or `nix flake update`" and so "does not do the job the archetype exists for". Contract 13 names the required set for the dev archetype as the user's home plus `/nix/var/nix`. The scope section says the framework declares those mount points. So nothing here proposes shipping a driveless dev microVM. What this PR deferred was archetypes *declaring* the volumes, and the effect is that a machine selecting `microvm` fails to evaluate rather than building something unusable. No driveless dev microVM can be produced. That is the fail-closed state, not a supported configuration. The open question is whether the split was worth making at all, which is the scope question at the bottom. ## The disk does not break the circularity — not forcing the toplevel does A real disk behaves exactly like the placeholder. The problem was never that the image was fake; it was that a `microvm.volumes` declaration is meaningless under a qemu guest, so once the wrong module is selected the definition is unmatched and Nix raises that while assembling the option tree, before any value is read. What actually breaks it: the marker does not need a volume. Measured directly on an unforced configuration with nothing declared: ``` {"libvirtNoVolume":["libvirt"],"microvmNoVolume":["microvm"]} ``` So the two jobs are now split. The selection comparison uses the volume-free fixture and stays pinned in both directions. The volume-bearing fixture is kept only for forcing allod/vm's contracts, which is where a volume is genuinely required. Sabotaging the direction that previously could not be pinned now reports: ``` error: runtime-module-selection: a machine declaring microvm composed libvirt ``` The other direction still names its machines: `composed guest runtime disagrees with the declared inventory fact for: allod-dev, privacy-1`. The caveat in this PR's description is obsolete and the code comment explaining it is gone. ## The hypervisor gap is closed here The plan said to guard the boundary rather than leave it to call-site discipline, and the first implementation left it to call-site discipline. Now the check asserts hypervisors keep the guest-runtime marker undeclared, so a later refactor routing `mkHypervisor` through `sharedModules` fails here instead of at whatever consumer notices first. Read with `lib.hasAttrByPath`, not `tryEval` — an undeclared option is a raw attribute error, which `tryEval` does not catch. That is the same harness bound the plan records for the negative cases. ## Still green `nix flake check` passes 10 checks and the fleet derivations are unchanged from the lock bump. ## Scope question for you Do the volume declarations come into this PR, or stay a separate change? Argument for here: it is the difference between an interface and a usable machine, and the fixture placeholder disappears once real declarations exist. Argument against: contract 13 puts the image path in deployment data — "the private deployer explicitly creates, formats, labels, owns by that VM's runner principal, and assigns the image before enabling the VM" — so the public repo cannot declare a complete volume entry on its own. Landing half of it here would leave a second placeholder behind, which is what this change just removed. That is a boundary judgement I should not make alone, so tell me which way and whether the follow-up belongs in a private repo.

allod-agent added 1 commit

2026-07-31 05:32:52 +01:00

Build the selection fixtures from whichever dev machine inventory declares cc0804d495

The fixtures named allod-dev directly, which bakes one example machine's
name into a check about the runtime fact. A deploy redirecting the
inventory input at its own machine set would have had to keep that name
to stay green. They now take the first machine of type dev, and throw a
named error if inventory declares none.

Pre-existing checks still name allod-dev; those are a separate cleanup.

Refs allod/strategy#20

allod-agent commented

2026-07-31 05:33:36 +01:00

Author

Member

Two review points: allod-dev hard-coded into fixtures, and whether the microvm runtime respects the no-shared-disk boundary. The first is fixed in cc0804d. The second rests on a premise that is not the case, with evidence below — but there is a real unproven area, and it is not this one.

allod-dev no longer appears in this check

The fixtures took the machine name literally, which bakes one example machine into a check about the runtime fact — a deploy redirecting the inventory input at its own machine set would have had to keep the name to stay green. They now take the first machine of type dev and throw a named error if inventory declares none.

Pre-existing checks (netrc-activation, dev-forge-opt-out, pi-integration, agent-vm-status) still name it. Separate cleanup, not swept in here.

There is no shared disk

A microvm guest shares no filesystem with the host. allod/vm asserts it, and the message says why: microvm.shares must be empty ... A share puts virtiofsd or 9p between the host filesystem and the guest. A second assertion requires microvm.storeOnDisk so /nix/store comes from a generated disk image rather than a host share.

What the guest gets is block devices backed by host files. That is structurally the same arrangement the libvirt guests use today: disk.nix declares /dev/vda, a host image file behind a virtual disk. Neither model puts a filesystem driver across the boundary.

Microvms do have their own disks — what they lack is a persistent root

The root is tmpfs, in RAM, deliberately. Persistent state lives on explicitly declared volumes, each a separate host file attached to exactly one VM. So the property is not "no disk", it is "nothing persists unless it was declared". Contract 13 requires autoCreate = false on every one, so no framework path creates, grows or relabels an image.

On isolation this is an upgrade, and measurably so

Upstream microvm.nix runs every VM as one shared microvm:kvm principal — nexus/nix/microvm/host.nix:11 says exactly that, and that this module replaces it. Nexus gives each VM its own system user and group, with kvm held only as a supplementary group for /dev/kvm.

Each VM's QEMU then runs inside a private mount namespace containing only:

/nix/store, read-only — needed so the runner and setpriv stay reachable after pivot_root
a fresh /proc
exactly /dev/{null,zero,full,random,urandom,kvm,net/tun} and optionally /dev/vhost-net
that VM's credential directory, read-only
that VM's QMP directory, read-write
only that VM's own declared volume images
only that VM's runner symlink; the state directory is otherwise an empty directory, so no sibling entries exist

Then pivot_root, the old root detached and removed, and a single privilege drop to that VM's principal.

Compare the current libvirt host: virtualisation.libvirtd.enable = true with no per-VM user configuration at all. So the microvm path is stricter than what runs today and stricter than upstream's own default.

Can a guest reach the hypervisor

Only by breaking QEMU's device emulation, which is the same exposure libvirt has today — /dev/kvm reachability is inherent to any KVM guest. What differs is what escaped code holds afterwards: an unprivileged per-VM uid, inside a namespace with no sibling objects, no writable host path, and specifically no path the root unit executes (contract 16 tightens upstream's 0775 microvm:kvm state directory for exactly that reason).

One object genuinely is shared across guests and worth naming: the host's /nix/store, bind-mounted read-only into every namespace. It is read-only and holds public package content, but an escape could read it and learn what the host has installed.

What is actually unproven

Not the isolation — that has an implementation and a dedicated check (nexus/checks/microvm/isolation.nix) that starts two guests and has each attack the other's credentials, images, QMP socket and runner.

The unproven part is storage lifecycle. The parent plan says so itself: contract 6a "is an empirical specification, recorded as such deliberately ... no pass has executed the assembled lifecycle in a booted guest." Its acceptance test 9 is the evidence that settles it, and the plan already forbids a dev microvm landing before those boots pass.

I have not run either check in this session; both belong to allod/nexus, not this PR. If the storage lifecycle is the worry, that is the right thing to demand evidence for before any machine selects this runtime — and the plan's own sequencing already blocks on it.

Two review points: `allod-dev` hard-coded into fixtures, and whether the microvm runtime respects the no-shared-disk boundary. The first is fixed in cc0804d. The second rests on a premise that is not the case, with evidence below — but there is a real unproven area, and it is not this one. ## allod-dev no longer appears in this check The fixtures took the machine name literally, which bakes one example machine into a check about the runtime fact — a deploy redirecting the inventory input at its own machine set would have had to keep the name to stay green. They now take the first machine of type `dev` and throw a named error if inventory declares none. Pre-existing checks (`netrc-activation`, `dev-forge-opt-out`, `pi-integration`, `agent-vm-status`) still name it. Separate cleanup, not swept in here. ## There is no shared disk A microvm guest shares no filesystem with the host. `allod/vm` asserts it, and the message says why: `microvm.shares must be empty ... A share puts virtiofsd or 9p between the host filesystem and the guest.` A second assertion requires `microvm.storeOnDisk` so `/nix/store` comes from a generated disk image rather than a host share. What the guest gets is block devices backed by host files. That is structurally the same arrangement the libvirt guests use today: `disk.nix` declares `/dev/vda`, a host image file behind a virtual disk. Neither model puts a filesystem driver across the boundary. ## Microvms do have their own disks — what they lack is a persistent root The root is tmpfs, in RAM, deliberately. Persistent state lives on explicitly declared volumes, each a separate host file attached to exactly one VM. So the property is not "no disk", it is "nothing persists unless it was declared". Contract 13 requires `autoCreate = false` on every one, so no framework path creates, grows or relabels an image. ## On isolation this is an upgrade, and measurably so Upstream microvm.nix runs every VM as one shared `microvm:kvm` principal — `nexus/nix/microvm/host.nix:11` says exactly that, and that this module replaces it. Nexus gives each VM its own system user and group, with `kvm` held only as a supplementary group for `/dev/kvm`. Each VM's QEMU then runs inside a private mount namespace containing only: - `/nix/store`, read-only — needed so the runner and `setpriv` stay reachable after `pivot_root` - a fresh `/proc` - exactly `/dev/{null,zero,full,random,urandom,kvm,net/tun}` and optionally `/dev/vhost-net` - that VM's credential directory, read-only - that VM's QMP directory, read-write - only that VM's own declared volume images - only that VM's runner symlink; the state directory is otherwise an empty directory, so no sibling entries exist Then `pivot_root`, the old root detached and removed, and a single privilege drop to that VM's principal. Compare the current libvirt host: `virtualisation.libvirtd.enable = true` with no per-VM user configuration at all. So the microvm path is stricter than what runs today and stricter than upstream's own default. ## Can a guest reach the hypervisor Only by breaking QEMU's device emulation, which is the same exposure libvirt has today — `/dev/kvm` reachability is inherent to any KVM guest. What differs is what escaped code holds afterwards: an unprivileged per-VM uid, inside a namespace with no sibling objects, no writable host path, and specifically no path the root unit executes (contract 16 tightens upstream's `0775 microvm:kvm` state directory for exactly that reason). One object genuinely is shared across guests and worth naming: the host's `/nix/store`, bind-mounted read-only into every namespace. It is read-only and holds public package content, but an escape could read it and learn what the host has installed. ## What is actually unproven Not the isolation — that has an implementation and a dedicated check (`nexus/checks/microvm/isolation.nix`) that starts two guests and has each attack the other's credentials, images, QMP socket and runner. The unproven part is storage lifecycle. The parent plan says so itself: contract 6a "is an empirical specification, recorded as such deliberately ... no pass has executed the assembled lifecycle in a booted guest." Its acceptance test 9 is the evidence that settles it, and the plan already forbids a dev microvm landing before those boots pass. I have not run either check in this session; both belong to `allod/nexus`, not this PR. If the storage lifecycle is the worry, that is the right thing to demand evidence for before any machine selects this runtime — and the plan's own sequencing already blocks on it.

allod-agent added 1 commit

2026-07-31 05:56:49 +01:00

Fix code review findings in the runtime selection check b784e6da9a

Independent review of the diff found four real defects.

The dev fixtures resolved their profile definition by machine name, but
machines may share a definition through profile.definition, which the
builders honour. A deploy using that feature hit a raw missing-attribute
error inside an unrelated assertion. Resolved the same way the builders
resolve it, with a named throw.

The both-guest-modules fixture took the default runtime, so a head dev
machine declaring microvm would have composed microvmGuest twice -
guest-base dedups, the fixture would have evaluated cleanly, and the
check would have failed for a reason unrelated to exclusivity. Runtime
is now pinned to libvirt.

Two negative cases trip several assertions at once, so failing did not
prove the named contract fired. Both are now pinned to their diagnostic
by reading config.assertions, which needs no toplevel force. Deleting
the assertion each names now fails this check.

The selector throw claimed inventory admits a value archetypes cannot
map. Inventory's enum and this table hold the same two values, so no
machine datum reaches it; it guards the override paths. Message derives
its key list from the table so it cannot drift.

Also dropped two assertions whose conditions could never be false, since
forcing throws rather than returning false, and stopped hard-coding the
inventory check attribute without a diagnostic.

Refs allod/strategy#20

allod-agent commented

2026-07-31 05:57:11 +01:00

Author

Member

What it refuted

The dev fixtures assumed a machine's definition is keyed on its own name. The builders do not assume that: machineConfigurations resolves definitionName = profile.definition or name, because machines may share one definition. The reviewer executed the case — gave the dev machine a profile.definition pointing at a shared definition — and nix flake check died with a raw attribute 'allod-dev' missing, surfacing inside an unrelated assertion's stack. That is exactly the deploy-redirect scenario the previous commit was written to support, so the decoupling was half done. Now resolved the same way the builders resolve it, with a named throw.

The both-guest-modules fixture depended on the head dev machine declaring libvirt. It took the default runtime. If that machine ever declares microvm — a deploy's inventory, or the eventual first microvm machine — the fixture composes microvmGuest twice, guest-base dedups with lib.unique, exclusivity never fires, and the fixture evaluates cleanly. The check would then fail with "negative cases did not fail" for a reason having nothing to do with exclusivity. Runtime is now pinned to libvirt explicitly.

Two negative cases were not pinned to the contract they name. The reviewer probed the failed assertion set and found bothRuntimes trips six assertions, only one of which is exclusivity — delete allod/vm's exclusivity assertion and the case stays green. The check's own comment cited the "failed for some other reason" trap that allod/inventory records, without applying the lesson. Both cases now assert their specific diagnostic appears in config.assertions, which is readable without forcing the toplevel. Verified non-vacuous by sabotaging the needle:

error: runtime-module-selection: both guest modules composed did not report 'this message does not exist'

The selector's throw stated a false premise. It said inventory admits a value archetypes cannot map. Inventory's enum and this table hold the same two values, so no machine datum can reach it — it guards the override paths (runtime argument, profileData/profile-settings at machineConfigurations, a future inventory growing a third runtime). Message and comment corrected, and the key list now derives from the table so it cannot drift.

Also removed two assertions whose conditions could never be false — forced returns true or throws, so those messages could never print and only advertised a failure mode that does not exist — and stopped naming inventory's check attribute without a diagnostic if a redirected inventory lacks it.

What survived the attack

Re-measured independently, on clean trees, with --no-eval-cache: all machine derivations byte-identical, including installer, which I had not checked. The marker is genuinely independent of the selector's input. Both sabotage directions still produce their named diagnostics. The hypervisor guard is real rather than vacuous — the predicate is true for both guests and false for nexus, so it can actually fire. The call-site shadowing path (profileData merged over builder args) is defended: it flips the marker and the check catches it. The volume placeholder cannot escape into a real machine's configuration.

One correction to my earlier claim, from the reviewer: vm-facts-coherence's derivation did change. The sole delta is the inventory source store path baked into its build script, a direct consequence of the input bump; the generated vm-facts.json is byte-identical. Benign, but it will rebuild, and "nothing changed" was too broad — the accurate statement is that no machine's system derivation changed.

Still open

The volume declarations question from the previous comment is unanswered, and it is the one thing here I will not decide alone.

Ran an independent adversarial review of the diff — something I should have done when this PR opened rather than only reviewing the plan. It found four real defects, one of them introduced by the previous commit. All fixed in b784e6d. ## What it refuted **The dev fixtures assumed a machine's definition is keyed on its own name.** The builders do not assume that: `machineConfigurations` resolves `definitionName = profile.definition or name`, because machines may share one definition. The reviewer executed the case — gave the dev machine a `profile.definition` pointing at a shared definition — and `nix flake check` died with a raw `attribute 'allod-dev' missing`, surfacing inside an unrelated assertion's stack. That is exactly the deploy-redirect scenario the previous commit was written to support, so the decoupling was half done. Now resolved the same way the builders resolve it, with a named throw. **The both-guest-modules fixture depended on the head dev machine declaring libvirt.** It took the default runtime. If that machine ever declares microvm — a deploy's inventory, or the eventual first microvm machine — the fixture composes `microvmGuest` twice, `guest-base` dedups with `lib.unique`, exclusivity never fires, and the fixture evaluates cleanly. The check would then fail with "negative cases did not fail" for a reason having nothing to do with exclusivity. Runtime is now pinned to libvirt explicitly. **Two negative cases were not pinned to the contract they name.** The reviewer probed the failed assertion set and found `bothRuntimes` trips six assertions, only one of which is exclusivity — delete allod/vm's exclusivity assertion and the case stays green. The check's own comment cited the "failed for some other reason" trap that allod/inventory records, without applying the lesson. Both cases now assert their specific diagnostic appears in `config.assertions`, which is readable without forcing the toplevel. Verified non-vacuous by sabotaging the needle: ``` error: runtime-module-selection: both guest modules composed did not report 'this message does not exist' ``` **The selector's throw stated a false premise.** It said inventory admits a value archetypes cannot map. Inventory's enum and this table hold the same two values, so no machine datum can reach it — it guards the override paths (`runtime` argument, `profileData`/profile-settings at `machineConfigurations`, a future inventory growing a third runtime). Message and comment corrected, and the key list now derives from the table so it cannot drift. Also removed two assertions whose conditions could never be false — `forced` returns `true` or throws, so those messages could never print and only advertised a failure mode that does not exist — and stopped naming inventory's check attribute without a diagnostic if a redirected inventory lacks it. ## What survived the attack Re-measured independently, on clean trees, with `--no-eval-cache`: all machine derivations byte-identical, including `installer`, which I had not checked. The marker is genuinely independent of the selector's input. Both sabotage directions still produce their named diagnostics. The hypervisor guard is real rather than vacuous — the predicate is `true` for both guests and `false` for nexus, so it can actually fire. The call-site shadowing path (`profileData` merged over builder args) is defended: it flips the marker and the check catches it. The volume placeholder cannot escape into a real machine's configuration. One correction to my earlier claim, from the reviewer: `vm-facts-coherence`'s derivation *did* change. The sole delta is the inventory source store path baked into its build script, a direct consequence of the input bump; the generated `vm-facts.json` is byte-identical. Benign, but it will rebuild, and "nothing changed" was too broad — the accurate statement is that no machine's system derivation changed. ## Still open The volume declarations question from the previous comment is unanswered, and it is the one thing here I will not decide alone.

allod-agent referenced this pull request

2026-07-31 06:07:02 +01:00

Declare the persistent volumes a selected microvm archetype requires #25

vnprc approved these changes

2026-07-31 06:14:23 +01:00