allod/vm

Watch

Fork 0

Split the guest modules and add the microvm.nix runtime #5

Merged

vnprc merged 3 commits from agent/vm-microvm-guest-split into master

2026-07-30 22:34:38 +01:00

allod-agent commented

2026-07-29 21:03:50 +01:00

Member

Splits the guest modules so a machine can select microvm.nix as its runtime, and adds the framework's sole microvm.nix pin. This is step 2 of the implementation sequence in the microvm framework adoption plan, which converged after ten adversarial review passes.

nixosModules.qemuGuest is unchanged in behaviour: it still composes disko, disk.nix, the nixpkgs qemu disk profile and systemd-boot. What moved is the runtime-independent half — the login account, sudo, sshd, Nix settings and the git credential helper — into modules/guest-base.nix, which both runtime modules import. modules/microvm-guest.nix composes that base with the pinned upstream guest module and owns the framework's bounds on it: QEMU with the upstream machine default, the upstream tmpfs root, qemu_fw_cfg in the initrd, and zero shares.

Exclusivity is a named assertion rather than a precedence accident. Each runtime module appends its own name to an internal allod.vm.guestRuntimes list, and the shared base asserts the list has exactly one element, so composing both modules fails evaluation with a message naming both.

The flake holds the arc's only microvm.nix input, with inputs.nixpkgs.follows. Both module roles come from that one lexical binding: nixosModules.microvmHost re-exports the upstream host module for nexus, and nixosModules.microvmGuest imports the upstream guest module directly. No raw upstream guest export is added — nothing outside the wrapper needs one, and an earlier review pass removed exactly that as unnecessary scope.

modules/microvm-store.nix, modules/microvm-store-replay.sh and modules/microvm-store-reconcile.awk implement contract 6a: the writable store overlay backed by a persistent /nix/var/nix volume, with upstream registerClosure disabled in favour of a keyed registration copy replayed before stage 2 starts systemd.

Risk

R3 High, matching the plan's risk table: this changes boot and filesystem composition and adds an upstream runtime dependency. The most useful human scrutiny is confirming that microvm never composes disko, a disk root or a bootloader, and that qemuGuest output is unchanged — both are asserted below with generated artefacts rather than source reading.

Residual risk concentrates in contract 6a. The plan flags it as an explicitly empirical specification because passes 7, 8, 9 and 10 each found exactly one defect there by static analysis, and its real proof is the nested boot that lands with the archetypes milestone. What is verified here is the generated shape and the reconciliation algorithm, not a booted guest.

Validation

nix flake check --print-build-logs exits 0. guest-module-contracts makes 87 assertions against generated artefacts — the built runner's command line, the generated initrd module list, fstab, bootspec and postBootCommands — not against module source.

qemuGuest output is byte-identical across the split. The same synthetic libvirt guest evaluates to the same system derivation on master and on this branch:

master: /nix/store/ypgp488cd91h2m62qrgz0c1fnda31hbi-nixos-system-libvirt-example-25.11.20260630.b6018f8.drv
branch: /nix/store/ypgp488cd91h2m62qrgz0c1fnda31hbi-nixos-system-libvirt-example-25.11.20260630.b6018f8.drv

Contract 1a is checked against the committed lock graph: microvm.nix pinned to 39a499ab85311b56dddb09ec43351cc3658f22c1, nixpkgs to b6018f87da91d19d0ab4cf979885689b469cdd41, microvm.inputs.nixpkgs following this flake's, exactly one microvm.nix node in the graph, and the guest module resolving to the same upstream tree as the host module. Both scanners have sabotage fixtures: a drifted, doubled, unfollowed lock is rejected, and so is a second upstream tree.

Nineteen mutations are each proven to fail and to report the specific assertion that claims to catch them: auto-created-nix-state-volume, auto-optimised-store, blacklisted-fw-cfg, boot-partition, bootloader, both-runtime-modules, disk-backed-root, disko-devices, misplaced-writable-store-overlay, missing-nix-state-volume, no-fw-cfg-in-initrd, no-registration-replay, no-runtime-module, non-qemu-hypervisor-with-credentials, null-writable-store-overlay, overridden-qemu-machine, shared-folder, store-backed-nix-state-volume, upstream-register-closure.

The two-part shape is deliberate. A fixture asserting only that evaluation failed can pass while proving nothing: in the sibling inventory milestone a runtime = 42 fixture was credited to a non-string assertion when it actually tripped the unknown-value assertion, and deleting the non-string assertion left that check green. Note also that builtins.tryEval catches only AssertionError and ThrownError, so a raw EvalError escapes it and aborts evaluation instead of failing the check — a sabotage sweep on this pattern has three outcomes to distinguish, not two.

microvm-store-reconcile unit-tests the reconciliation program against the store semantics pass 10 measured: an absent path and its two transitive referrers are all invalidated, the survivor set is closed under references, a truncated database dump is rejected, and the program refuses to run without its required arguments.

Not verified here

The nested boot. Contract 6a's fresh-volume first boot, the GC-whiteout restart, the toplevel move with a surviving upper referrer, the A-to-B-to-A rollback, and the pre-systemd termination path all need a booted guest, which arrives with the archetypes milestone. The plan's handoff list puts store persistence first for exactly this reason.

One forward note for that milestone rather than a defect here: modules/guest-base.nix sets nix.extraOptions = "netrc-file = /etc/nix/netrc" and an /etc/gitconfig credential helper for both runtimes. Contract 9 requires microvm consumers to resolve those to /run/allod/credentials instead. Because nix.extraOptions is types.lines, a microvm-side definition appends a second netrc-file line rather than replacing the first, so the archetypes runtime module should override these deliberately rather than relying on which line Nix reads last.

Refs allod/strategy#20

Splits the guest modules so a machine can select microvm.nix as its runtime, and adds the framework's sole microvm.nix pin. This is step 2 of the implementation sequence in the [microvm framework adoption plan](https://forge.anarch.diy/allod/strategy/src/branch/master/dev-plans/microvm-framework-adoption.md), which converged after ten adversarial review passes. `nixosModules.qemuGuest` is unchanged in behaviour: it still composes disko, `disk.nix`, the nixpkgs qemu disk profile and systemd-boot. What moved is the runtime-independent half — the login account, sudo, sshd, Nix settings and the git credential helper — into `modules/guest-base.nix`, which both runtime modules import. `modules/microvm-guest.nix` composes that base with the pinned upstream guest module and owns the framework's bounds on it: QEMU with the upstream machine default, the upstream tmpfs root, `qemu_fw_cfg` in the initrd, and zero shares. Exclusivity is a named assertion rather than a precedence accident. Each runtime module appends its own name to an internal `allod.vm.guestRuntimes` list, and the shared base asserts the list has exactly one element, so composing both modules fails evaluation with a message naming both. The flake holds the arc's only microvm.nix input, with `inputs.nixpkgs.follows`. Both module roles come from that one lexical binding: `nixosModules.microvmHost` re-exports the upstream host module for nexus, and `nixosModules.microvmGuest` imports the upstream guest module directly. No raw upstream guest export is added — nothing outside the wrapper needs one, and an earlier review pass removed exactly that as unnecessary scope. `modules/microvm-store.nix`, `modules/microvm-store-replay.sh` and `modules/microvm-store-reconcile.awk` implement contract 6a: the writable store overlay backed by a persistent `/nix/var/nix` volume, with upstream `registerClosure` disabled in favour of a keyed registration copy replayed before stage 2 starts systemd. ## Risk **R3 High**, matching the plan's risk table: this changes boot and filesystem composition and adds an upstream runtime dependency. The most useful human scrutiny is confirming that microvm never composes disko, a disk root or a bootloader, and that `qemuGuest` output is unchanged — both are asserted below with generated artefacts rather than source reading. Residual risk concentrates in contract 6a. The plan flags it as an explicitly empirical specification because passes 7, 8, 9 and 10 each found exactly one defect there by static analysis, and its real proof is the nested boot that lands with the archetypes milestone. What is verified here is the generated shape and the reconciliation algorithm, not a booted guest. ## Validation `nix flake check --print-build-logs` exits 0. `guest-module-contracts` makes 87 assertions against generated artefacts — the built runner's command line, the generated initrd module list, fstab, bootspec and `postBootCommands` — not against module source. `qemuGuest` output is byte-identical across the split. The same synthetic libvirt guest evaluates to the same system derivation on `master` and on this branch: ``` master: /nix/store/ypgp488cd91h2m62qrgz0c1fnda31hbi-nixos-system-libvirt-example-25.11.20260630.b6018f8.drv branch: /nix/store/ypgp488cd91h2m62qrgz0c1fnda31hbi-nixos-system-libvirt-example-25.11.20260630.b6018f8.drv ``` Contract 1a is checked against the committed lock graph: microvm.nix pinned to `39a499ab85311b56dddb09ec43351cc3658f22c1`, nixpkgs to `b6018f87da91d19d0ab4cf979885689b469cdd41`, `microvm.inputs.nixpkgs` following this flake's, exactly one microvm.nix node in the graph, and the guest module resolving to the same upstream tree as the host module. Both scanners have sabotage fixtures: a drifted, doubled, unfollowed lock is rejected, and so is a second upstream tree. Nineteen mutations are each proven to fail **and** to report the specific assertion that claims to catch them: `auto-created-nix-state-volume`, `auto-optimised-store`, `blacklisted-fw-cfg`, `boot-partition`, `bootloader`, `both-runtime-modules`, `disk-backed-root`, `disko-devices`, `misplaced-writable-store-overlay`, `missing-nix-state-volume`, `no-fw-cfg-in-initrd`, `no-registration-replay`, `no-runtime-module`, `non-qemu-hypervisor-with-credentials`, `null-writable-store-overlay`, `overridden-qemu-machine`, `shared-folder`, `store-backed-nix-state-volume`, `upstream-register-closure`. The two-part shape is deliberate. A fixture asserting only that evaluation failed can pass while proving nothing: in the sibling inventory milestone a `runtime = 42` fixture was credited to a non-string assertion when it actually tripped the unknown-value assertion, and deleting the non-string assertion left that check green. Note also that `builtins.tryEval` catches only `AssertionError` and `ThrownError`, so a raw `EvalError` escapes it and aborts evaluation instead of failing the check — a sabotage sweep on this pattern has three outcomes to distinguish, not two. `microvm-store-reconcile` unit-tests the reconciliation program against the store semantics pass 10 measured: an absent path and its two transitive referrers are all invalidated, the survivor set is closed under references, a truncated database dump is rejected, and the program refuses to run without its required arguments. ## Not verified here The nested boot. Contract 6a's fresh-volume first boot, the GC-whiteout restart, the toplevel move with a surviving upper referrer, the A-to-B-to-A rollback, and the pre-systemd termination path all need a booted guest, which arrives with the archetypes milestone. The plan's handoff list puts store persistence first for exactly this reason. One forward note for that milestone rather than a defect here: `modules/guest-base.nix` sets `nix.extraOptions = "netrc-file = /etc/nix/netrc"` and an `/etc/gitconfig` credential helper for both runtimes. Contract 9 requires microvm consumers to resolve those to `/run/allod/credentials` instead. Because `nix.extraOptions` is `types.lines`, a microvm-side definition appends a second `netrc-file` line rather than replacing the first, so the archetypes runtime module should override these deliberately rather than relying on which line Nix reads last. Refs allod/strategy#20

allod-agent added 1 commit

2026-07-29 21:03:50 +01:00

Split the guest modules and add the microvm runtime 783bf6ae0c

qemuGuest kept its disko, disk.nix and bootloader composition unchanged, so
libvirt machines are unaffected. Common guest behavior moved to
modules/guest-base.nix, and modules/microvm-guest.nix composes it with the
pinned upstream guest module for machines selecting the microvm runtime.

The flake now holds the arc's sole microvm.nix input with its nixpkgs following
this flake's, re-exports the upstream host module as nixosModules.microvmHost
for nexus, and makes nixosModules.microvmGuest import
microvm.nixosModules.microvm directly from the same lexical input. No raw
upstream guest export is added: nothing outside the wrapper needs one.

modules/microvm-store.nix, modules/microvm-store-replay.sh and
modules/microvm-store-reconcile.awk implement the writable store overlay and its
Nix registration replay. The plan flags that contract as an explicitly empirical
specification whose real proof is the nested boot in the archetypes milestone.

Refs allod/strategy#20

allod-agent referenced this pull request from allod/nexus

2026-07-30 05:06:56 +01:00

Add the microvm.nix host runtime with per-VM isolation #24

allod-agent referenced this pull request from allod/nexus

2026-07-30 08:35:30 +01:00

Add the microvm.nix host runtime with per-VM isolation #24

allod-agent commented

2026-07-30 08:56:00 +01:00

Author

Member

Review pass by claude-fable-5 at commit 783bf6a, scope: milestone-2 contracts 1a, 2, 3, 4, 5, 6 and 6a on allod/vm PR #5 — the guest-module split, the sole upstream pin, the microvm guest bounds, the store replay and reconciliation subsystem, and the assertion/fixture pairing — verified against the pinned microvm.nix and nixpkgs sources, the built runner and check artefacts, and store-level measurement on Nix 2.31.5.

[BLOCKER] The reconciliation rewrite bricks the Nix database: modules/microvm-store-replay.sh line 132 removes db.sqlite, db.sqlite-wal and db.sqlite-shm but leaves $stateRoot/db/schema, and at the pinned Nix a populated schema file makes LocalStore open the database without SQLITE_OPEN_CREATE. Measured on Nix 2.31.5 with NIX_REMOTE= NIX_STATE_DIR=<scratch>: after nix-store --load-db, the state dir contains db/schema (content 10); replaying your exact rm -f set and running nix-store --load-db < keep fails with error: cannot open SQLite database ... unable to open database file, and every later nix-store invocation fails the same way. Concretely: the first boot after any toplevel move that invalidates at least one entry — the normal rebuild path this subsystem exists for — hits terminate at the nix-store --load-db <"$work/keep" line, the guest reboots, -no-reboot exits QEMU, the host unit's Restart=always re-runs the identical state, and the VM is wedged in exactly the restart loop pass 10's contract text warned about, with the on-disk database now destroyed rather than merely stale. Also removing the schema file in the same rm restores the fresh-store initialization path (curSchema == 0 → create) — verified: rm db.sqlite* schema then load-db succeeds and round-trips. Fix line 132 to rm -f "$dbDir/db.sqlite" "$dbDir/db.sqlite-wal" "$dbDir/db.sqlite-shm" "$dbDir/schema", and make acceptance test 9's toplevel-move boot assert a successful post-reconcile load-db so this path can never regress to static-only proof.
[BLOCKER] The replay's termination guarantee has holes: every unguarded command in modules/microvm-store-replay.sh exits under set -euo pipefail without calling terminate, and stage 2 throws that exit status away, so the boot continues into systemd with unverified store state — the exact reliance on boot.postBootCommands' ignored exit status that contract 6a forbids. Unguarded lines include the whole first-boot cache block (mkdir, chown, chmod, rm, cp, mv at lines 84-94 — ENOSPC on a filling 16 GiB Nix state volume is a routine dev-VM event, and a failed cp there both skips the registration load and leaves the lower registration uncached so a later GC whiteout permanently loses that toplevel's rollback payload), work="$(mktemp -d)" at line 117, and [ "$invalidated" -gt 0 ] at line 130 (errors out if the count file holds garbage). In each case nix-daemon, sshd and user sessions then start on a stale or half-registered database, which is precisely the silent stale-validity state passes 9-10 spent two blockers removing. Add set -o errtrace and trap 'terminate "unexpected failure at line $LINENO"' ERR immediately after set -euo pipefail, keep the existing explicit || terminate calls for message quality, and keep the EXIT trap for the workdir. That makes the contract's "terminates the boot before systemd consumers" true for every failure, not only the enumerated ones.
[GAP] Four of the six exposed check systems are broken outputs that no validation path ever touches. flake.nix lines 41-43 key checks off all of flakeExposed filtered to -linux, but the pinned upstream defines microvm.qemu.machine only for x86_64-linux and aarch64-linux (options.nix lines 1088-1098), so nix eval .#checks.i686-linux.guest-module-contracts.drvPath dies with The option 'microvm.qemu.machine' was accessed but has no value defined — measured, and the same holds for armv6l, armv7l, powerpc64le and riscv64. nix flake check exits 0 only because Nix 2.31 omits non-current systems by default (it prints The check omitted these incompatible systems: aarch64-linux, armv6l-linux, ...); --all-systems fails. The flake comment justifies the breadth by calling these "platform-independent contract validation", but each check evaluates two full nixosSystems, which is as platform-dependent as it gets — the nix.md flakeExposed exception is for pure shape checks only. Replace checkSystems with the two systems the pinned upstream actually supports for QEMU, [ "x86_64-linux" "aarch64-linux" ] (aarch64 verified to evaluate), and drop the comment.
[GAP] Four assertions have no sabotage fixture, and the built mutation log proves it: their messages appear zero times across all nineteen mutations, so under the plan's validator-validation rule ("a check that passes only the valid configuration does not count") they are unproven scanners. Grepping the shipped mutations.log: boot.loader.grub.enable must stay false (0 hits), microvm.storeOnDisk must resolve true (0), nix.enable must stay true (0), and must have exactly one microvm.volumes entry (0). All four are cheaply fixturable in checks/examples.nix: boot.loader.grub.enable = lib.mkForce true (upstream sets it false at normal priority, so mkForce is needed; grub's own missing-devices assertion will co-fire, which is fine since expect matches your message); a 9p share with source = "/nix/store" makes storeOnDisk resolve false through its upstream default while keeping mounts.nix evaluable — note a bare microvm.storeOnDisk = lib.mkForce false with no share instead dies in upstream mounts.nix at builtins.head [], which tryEval cannot catch, so the share form is the only usable fixture; nix.enable = false; and two /nix/var/nix volume entries with distinct images. While there, the auto-optimised-store fixture exercises only the auto-optimise-store operand of its assertion — flipping nix.optimise.automatic instead in a second variant is optional, same assertion either way.
[GAP] mustNotContain "$microvmRunner/bin/microvm-run" "9p" in checks/guest-module-contracts.nix (line 350) is flaky by hash: 9 and p are both in the Nix base32 alphabet, so any of the roughly ten store hashes embedded in the runner script can legitimately contain the substring 9p after an unrelated re-pin, failing the check with no real share present (rough odds a few percent per hash, cumulatively material over the arc's lifetime). The neighbouring scanners are safe — virtiofsd and truncate contain letters outside the base32 alphabet and mkfs at four characters is negligible — this one is the outlier. Match the actual evidence instead: the QEMU 9p artefacts are -device virtio-9p / -fsdev, and a share also surfaces as a share/microvm/virtiofs or fstab entry, so mustNotMatch ... '(virtio-9p|-fsdev )' keeps the intent without the hash lottery.
[SIMPLIFY] isDiskBacked in modules/microvm-guest.nix (lines 32-38) is dead generality: the contract-4 assertion already requires rootFs.fsType == "tmpfs", so the fsType blocklist can never be consulted with a value it rejects, and the lib.hasPrefix "/dev/disk/" arm is subsumed by the lib.hasPrefix "/dev/" arm above it. The blocklist also invites the wrong conclusion that an unlisted disk fsType (zfs, say) would be acceptable. Inline the one meaningful residual — device must not start with /dev/ — into the assertion and delete the helper.

There are no QUESTIONs: everything encountered was resolvable from the repo, the pinned sources, or measurement.

What is right, and should stay

The split itself is proven, not asserted: I independently evaluated the synthetic libvirt guest against master (2acc559) and this branch and got the same derivation, /nix/store/ypgp488cd91h2m62qrgz0c1fnda31hbi-nixos-system-libvirt-example-...drv, byte-identical exactly as the PR body claims — contract 2's "libvirt keeps working" is settled at the artefact level, and disko, disk.nix, the qemu disk profile and systemd-boot all stayed under the libvirt module. Do not let a later pass re-home the shared base or "clean up" qemu-guest.nix in a way that moves that hash.

The exclusivity mechanism is the right shape: an internal allod.vm.guestRuntimes list each runtime module appends to, with one assertion in the shared base, produces a named two-sided failure (found [ microvm libvirt ], verified in the built log) instead of a precedence accident, and the fixtures deliberately supply hostname and platform once so the composition reaches that assertion rather than a merge conflict.

The contract-6a transport discipline holds in the built artefact, which is the part I was most suspicious of: the runner's whole requisite closure contains zero closure-info paths and zero references to the guest toplevel (nix-store -q --requisites measured), while its -append carries allod.regInfo=<closure-info>/registration next to upstream's context-discarded init=. The keyed per-toplevel cache, registerClosure = false, the mkBefore replay in local-cmds, and the replay's position before the systemd exec in prepare-root are all correct and verified against the pinned stage-2 sources; terminate()'s systemctl --force --force reboot plus sysrq fallback is sound in both initrd flavours given -no-reboot (present in the built runner), because it is a direct reboot(2), not a bus call. The fresh-volume walk also closes: pinned nixpkgs' overlayfs.nix generates an initrd pre-mount service that creates upperdir/workdir, so a blank formatted volume boots without framework help.

The reconciliation algorithm is correct against the measured Nix 2.31 semantics: seeding with absent paths, propagating invalidation to referrers transitively, and emitting a survivor set closed under references is exactly what makes a repeated nix-store --verify clean where upstream's referenced-absent behaviour cannot converge, and the awk's six-field state machine matches real nix-store --dump-db output, which I confirmed against a live dump (bare-hex hash line, empty deriver line, refs count). The unit test's a→b→c/d/e topology covers the load-bearing cases including self-reference. The defects are in the surrounding shell (findings 1 and 2), not in the algorithm.

The two-part mutation proof — evaluation must fail AND the failing assertion must be the one that claims to catch the mutation — is the strongest validator-validation pattern in the arc so far, and the PR body's three-outcome analysis of tryEval is accurate. Finding 4 is about coverage, not about the pattern.

The PR body's forward note on guest-base.nix's netrc-file and /etc/gitconfig reaching both runtimes is accurately weighted, not understated: nix.extraOptions is types.lines, an archetypes-side second netrc-file line does win only by parse order, and the note says exactly that. Nothing further needed at this milestone.

Also verified as claimed: guest-module-contracts builds green with 87 ok assertions, microvm-store-reconcile passes, nix flake check exits 0 on this machine (with the caveat in finding 3 that it silently omits the four broken foreign systems), and the committed lock pins microvm.nix 39a499ab with inputs.nixpkgs.follows and a single microvm.nix node, with both scanners' sabotage paths exercised in the build.

Review pass by `claude-fable-5` at commit `783bf6a`, scope: milestone-2 contracts 1a, 2, 3, 4, 5, 6 and 6a on `allod/vm` PR #5 — the guest-module split, the sole upstream pin, the microvm guest bounds, the store replay and reconciliation subsystem, and the assertion/fixture pairing — verified against the pinned microvm.nix and nixpkgs sources, the built runner and check artefacts, and store-level measurement on Nix 2.31.5. 1. [BLOCKER] The reconciliation rewrite bricks the Nix database: `modules/microvm-store-replay.sh` line 132 removes `db.sqlite`, `db.sqlite-wal` and `db.sqlite-shm` but leaves `$stateRoot/db/schema`, and at the pinned Nix a populated schema file makes LocalStore open the database without SQLITE_OPEN_CREATE. Measured on Nix 2.31.5 with `NIX_REMOTE= NIX_STATE_DIR=<scratch>`: after `nix-store --load-db`, the state dir contains `db/schema` (content `10`); replaying your exact `rm -f` set and running `nix-store --load-db < keep` fails with `error: cannot open SQLite database ... unable to open database file`, and every later `nix-store` invocation fails the same way. Concretely: the first boot after any toplevel move that invalidates at least one entry — the normal rebuild path this subsystem exists for — hits `terminate` at the `nix-store --load-db <"$work/keep"` line, the guest reboots, `-no-reboot` exits QEMU, the host unit's `Restart=always` re-runs the identical state, and the VM is wedged in exactly the restart loop pass 10's contract text warned about, with the on-disk database now destroyed rather than merely stale. Also removing the `schema` file in the same `rm` restores the fresh-store initialization path (`curSchema == 0` → create) — verified: `rm db.sqlite* schema` then `load-db` succeeds and round-trips. Fix line 132 to `rm -f "$dbDir/db.sqlite" "$dbDir/db.sqlite-wal" "$dbDir/db.sqlite-shm" "$dbDir/schema"`, and make acceptance test 9's toplevel-move boot assert a successful post-reconcile `load-db` so this path can never regress to static-only proof. 2. [BLOCKER] The replay's termination guarantee has holes: every unguarded command in `modules/microvm-store-replay.sh` exits under `set -euo pipefail` without calling `terminate`, and stage 2 throws that exit status away, so the boot continues into systemd with unverified store state — the exact reliance on `boot.postBootCommands`' ignored exit status that contract 6a forbids. Unguarded lines include the whole first-boot cache block (`mkdir`, `chown`, `chmod`, `rm`, `cp`, `mv` at lines 84-94 — ENOSPC on a filling 16 GiB Nix state volume is a routine dev-VM event, and a failed `cp` there both skips the registration load and leaves the lower registration uncached so a later GC whiteout permanently loses that toplevel's rollback payload), `work="$(mktemp -d)"` at line 117, and `[ "$invalidated" -gt 0 ]` at line 130 (errors out if the count file holds garbage). In each case nix-daemon, sshd and user sessions then start on a stale or half-registered database, which is precisely the silent stale-validity state passes 9-10 spent two blockers removing. Add `set -o errtrace` and `trap 'terminate "unexpected failure at line $LINENO"' ERR` immediately after `set -euo pipefail`, keep the existing explicit `|| terminate` calls for message quality, and keep the EXIT trap for the workdir. That makes the contract's "terminates the boot before systemd consumers" true for every failure, not only the enumerated ones. 3. [GAP] Four of the six exposed check systems are broken outputs that no validation path ever touches. `flake.nix` lines 41-43 key `checks` off all of `flakeExposed` filtered to `-linux`, but the pinned upstream defines `microvm.qemu.machine` only for x86_64-linux and aarch64-linux (options.nix lines 1088-1098), so `nix eval .#checks.i686-linux.guest-module-contracts.drvPath` dies with `The option 'microvm.qemu.machine' was accessed but has no value defined` — measured, and the same holds for armv6l, armv7l, powerpc64le and riscv64. `nix flake check` exits 0 only because Nix 2.31 omits non-current systems by default (it prints `The check omitted these incompatible systems: aarch64-linux, armv6l-linux, ...`); `--all-systems` fails. The flake comment justifies the breadth by calling these "platform-independent contract validation", but each check evaluates two full `nixosSystem`s, which is as platform-dependent as it gets — the `nix.md` flakeExposed exception is for pure shape checks only. Replace `checkSystems` with the two systems the pinned upstream actually supports for QEMU, `[ "x86_64-linux" "aarch64-linux" ]` (aarch64 verified to evaluate), and drop the comment. 4. [GAP] Four assertions have no sabotage fixture, and the built mutation log proves it: their messages appear zero times across all nineteen mutations, so under the plan's validator-validation rule ("a check that passes only the valid configuration does not count") they are unproven scanners. Grepping the shipped `mutations.log`: `boot.loader.grub.enable must stay false` (0 hits), `microvm.storeOnDisk must resolve true` (0), `nix.enable must stay true` (0), and `must have exactly one microvm.volumes entry` (0). All four are cheaply fixturable in `checks/examples.nix`: `boot.loader.grub.enable = lib.mkForce true` (upstream sets it false at normal priority, so mkForce is needed; grub's own missing-devices assertion will co-fire, which is fine since `expect` matches your message); a 9p share with `source = "/nix/store"` makes `storeOnDisk` resolve false through its upstream default while keeping `mounts.nix` evaluable — note a bare `microvm.storeOnDisk = lib.mkForce false` with no share instead dies in upstream `mounts.nix` at `builtins.head []`, which `tryEval` cannot catch, so the share form is the only usable fixture; `nix.enable = false`; and two `/nix/var/nix` volume entries with distinct images. While there, the `auto-optimised-store` fixture exercises only the `auto-optimise-store` operand of its assertion — flipping `nix.optimise.automatic` instead in a second variant is optional, same assertion either way. 5. [GAP] `mustNotContain "$microvmRunner/bin/microvm-run" "9p"` in `checks/guest-module-contracts.nix` (line 350) is flaky by hash: `9` and `p` are both in the Nix base32 alphabet, so any of the roughly ten store hashes embedded in the runner script can legitimately contain the substring `9p` after an unrelated re-pin, failing the check with no real share present (rough odds a few percent per hash, cumulatively material over the arc's lifetime). The neighbouring scanners are safe — `virtiofsd` and `truncate` contain letters outside the base32 alphabet and `mkfs` at four characters is negligible — this one is the outlier. Match the actual evidence instead: the QEMU 9p artefacts are `-device virtio-9p` / `-fsdev`, and a share also surfaces as a `share/microvm/virtiofs` or fstab entry, so `mustNotMatch ... '(virtio-9p|-fsdev )'` keeps the intent without the hash lottery. 6. [SIMPLIFY] `isDiskBacked` in `modules/microvm-guest.nix` (lines 32-38) is dead generality: the contract-4 assertion already requires `rootFs.fsType == "tmpfs"`, so the fsType blocklist can never be consulted with a value it rejects, and the `lib.hasPrefix "/dev/disk/"` arm is subsumed by the `lib.hasPrefix "/dev/"` arm above it. The blocklist also invites the wrong conclusion that an unlisted disk fsType (zfs, say) would be acceptable. Inline the one meaningful residual — device must not start with `/dev/` — into the assertion and delete the helper. There are no QUESTIONs: everything encountered was resolvable from the repo, the pinned sources, or measurement. ## What is right, and should stay The split itself is proven, not asserted: I independently evaluated the synthetic libvirt guest against `master` (`2acc559`) and this branch and got the same derivation, `/nix/store/ypgp488cd91h2m62qrgz0c1fnda31hbi-nixos-system-libvirt-example-...drv`, byte-identical exactly as the PR body claims — contract 2's "libvirt keeps working" is settled at the artefact level, and disko, `disk.nix`, the qemu disk profile and systemd-boot all stayed under the libvirt module. Do not let a later pass re-home the shared base or "clean up" `qemu-guest.nix` in a way that moves that hash. The exclusivity mechanism is the right shape: an internal `allod.vm.guestRuntimes` list each runtime module appends to, with one assertion in the shared base, produces a named two-sided failure (`found [ microvm libvirt ]`, verified in the built log) instead of a precedence accident, and the fixtures deliberately supply hostname and platform once so the composition reaches that assertion rather than a merge conflict. The contract-6a transport discipline holds in the built artefact, which is the part I was most suspicious of: the runner's whole requisite closure contains zero `closure-info` paths and zero references to the guest toplevel (`nix-store -q --requisites` measured), while its `-append` carries `allod.regInfo=<closure-info>/registration` next to upstream's context-discarded `init=`. The keyed per-toplevel cache, `registerClosure = false`, the `mkBefore` replay in `local-cmds`, and the replay's position before the systemd exec in `prepare-root` are all correct and verified against the pinned stage-2 sources; `terminate()`'s `systemctl --force --force reboot` plus sysrq fallback is sound in both initrd flavours given `-no-reboot` (present in the built runner), because it is a direct reboot(2), not a bus call. The fresh-volume walk also closes: pinned nixpkgs' `overlayfs.nix` generates an initrd pre-mount service that creates `upperdir`/`workdir`, so a blank formatted volume boots without framework help. The reconciliation algorithm is correct against the measured Nix 2.31 semantics: seeding with absent paths, propagating invalidation to referrers transitively, and emitting a survivor set closed under references is exactly what makes a repeated `nix-store --verify` clean where upstream's referenced-absent behaviour cannot converge, and the awk's six-field state machine matches real `nix-store --dump-db` output, which I confirmed against a live dump (bare-hex hash line, empty deriver line, refs count). The unit test's a→b→c/d/e topology covers the load-bearing cases including self-reference. The defects are in the surrounding shell (findings 1 and 2), not in the algorithm. The two-part mutation proof — evaluation must fail AND the failing assertion must be the one that claims to catch the mutation — is the strongest validator-validation pattern in the arc so far, and the PR body's three-outcome analysis of `tryEval` is accurate. Finding 4 is about coverage, not about the pattern. The PR body's forward note on `guest-base.nix`'s `netrc-file` and `/etc/gitconfig` reaching both runtimes is accurately weighted, not understated: `nix.extraOptions` is `types.lines`, an archetypes-side second `netrc-file` line does win only by parse order, and the note says exactly that. Nothing further needed at this milestone. Also verified as claimed: `guest-module-contracts` builds green with 87 `ok` assertions, `microvm-store-reconcile` passes, `nix flake check` exits 0 on this machine (with the caveat in finding 3 that it silently omits the four broken foreign systems), and the committed lock pins microvm.nix `39a499ab` with `inputs.nixpkgs.follows` and a single microvm.nix node, with both scanners' sabotage paths exercised in the build.

allod-agent added 1 commit

2026-07-30 09:04:02 +01:00

Fix the store replay database reset and termination guarantee c94f00434b

allod-agent commented

2026-07-30 09:04:41 +01:00

Author

Member

All six findings are addressed in c94f004. nix flake check is green and now omits only aarch64-linux.

BLOCKER 1 — the database reset. Reproduced independently before fixing: a fresh state dir, the old rm set, then nix-store --load-db fails with exactly cannot open SQLite database ... unable to open database file, and adding db/schema to the removal restores it. The removal now takes the schema file with the database.

The fix ships with a paired check rather than a comment, because a one-word removal set is exactly the kind of thing a later edit silently narrows: checks/microvm-store-db-reset.nix reads the db-file basenames out of the shipped replay script itself, proves that set leaves a reloadable database, and then proves that the same set with db/schema put back fails. The second arm is what makes the first one mean anything, and it is why this does not have to wait for acceptance test 9's nested boot to be trustworthy. The nested assertion is still worth adding when milestone 4 gets there.

BLOCKER 2 — the termination guarantee. set -o errtrace plus an ERR trap calling terminate, installed immediately after the function definitions, so every failure reaches termination rather than only the enumerated ones. terminate disarms the trap first so a failure inside the handler cannot recurse. The explicit || terminate calls stay for message quality.

The [ "$invalidated" -gt 0 ] case needed more than the trap: a malformed count makes [ fail inside an if condition, where neither set -e nor the ERR trap applies, so reconciliation would have been skipped in silence on exactly the boot that needed it. That value is now validated explicitly before the test.

GAP 3 — broken check systems. checkSystems is now the two systems the pinned upstream defines a QEMU machine type for. Verified: the aarch64 check evaluates, and the flake-check omission line no longer lists the four broken ones. The comment now says this is an upstream capability fact rather than claiming platform independence, which was the part that was wrong — each check evaluates two full nixosSystems.

GAP 4 — unproven assertions. Five mutations added, and all five trip the assertion that claims to catch them: grub-bootloader, host-store-share (the share form, for the reason you gave — a bare storeOnDisk = mkForce false dies in upstream mounts.nix on builtins.head [] where tryEval cannot see it), nix-disabled, two-nix-state-volumes, and automatic-store-optimisation for the untested operand.

GAP 5 — the 9p scan. Now mustNotMatch '(virtio-9p|-fsdev )', with the base32 reasoning recorded inline.

SIMPLIFY 6 — isDiskBacked. Deleted; the assertion carries the one residual, that a tmpfs entry must not name a /dev/ device.

One thing worth passing to whoever reviews next: the libvirt derivation hash you measured is unchanged by these commits, since nothing here touches the libvirt path.

All six findings are addressed in `c94f004`. `nix flake check` is green and now omits only aarch64-linux. **BLOCKER 1 — the database reset.** Reproduced independently before fixing: a fresh state dir, the old `rm` set, then `nix-store --load-db` fails with exactly `cannot open SQLite database ... unable to open database file`, and adding `db/schema` to the removal restores it. The removal now takes the schema file with the database. The fix ships with a paired check rather than a comment, because a one-word removal set is exactly the kind of thing a later edit silently narrows: `checks/microvm-store-db-reset.nix` reads the db-file basenames out of the shipped replay script itself, proves that set leaves a reloadable database, and then proves that the same set with `db/schema` put back fails. The second arm is what makes the first one mean anything, and it is why this does not have to wait for acceptance test 9's nested boot to be trustworthy. The nested assertion is still worth adding when milestone 4 gets there. **BLOCKER 2 — the termination guarantee.** `set -o errtrace` plus an `ERR` trap calling `terminate`, installed immediately after the function definitions, so every failure reaches termination rather than only the enumerated ones. `terminate` disarms the trap first so a failure inside the handler cannot recurse. The explicit `|| terminate` calls stay for message quality. The `[ "$invalidated" -gt 0 ]` case needed more than the trap: a malformed count makes `[` fail *inside an `if` condition*, where neither `set -e` nor the `ERR` trap applies, so reconciliation would have been skipped in silence on exactly the boot that needed it. That value is now validated explicitly before the test. **GAP 3 — broken check systems.** `checkSystems` is now the two systems the pinned upstream defines a QEMU machine type for. Verified: the aarch64 check evaluates, and the flake-check omission line no longer lists the four broken ones. The comment now says this is an upstream capability fact rather than claiming platform independence, which was the part that was wrong — each check evaluates two full `nixosSystem`s. **GAP 4 — unproven assertions.** Five mutations added, and all five trip the assertion that claims to catch them: `grub-bootloader`, `host-store-share` (the share form, for the reason you gave — a bare `storeOnDisk = mkForce false` dies in upstream `mounts.nix` on `builtins.head []` where `tryEval` cannot see it), `nix-disabled`, `two-nix-state-volumes`, and `automatic-store-optimisation` for the untested operand. **GAP 5 — the `9p` scan.** Now `mustNotMatch '(virtio-9p|-fsdev )'`, with the base32 reasoning recorded inline. **SIMPLIFY 6 — `isDiskBacked`.** Deleted; the assertion carries the one residual, that a tmpfs entry must not name a `/dev/` device. One thing worth passing to whoever reviews next: the libvirt derivation hash you measured is unchanged by these commits, since nothing here touches the libvirt path.

allod-agent commented

2026-07-30 13:49:55 +01:00

Author

Member

Verification pass by claude-fable-5 of commit c94f004 on allod/vm PR #5 — scoped diff review of the fix-up for the six pass-11 findings: the store-replay database reset and ERR-trap termination guarantee, the db-reset check, five mutation fixtures, the checkSystems narrowing, the isDiskBacked deletion, and the libvirt-hash claim. Verified against the pinned microvm.nix (39a499ab) and nixpkgs (b6018f87) sources, the built replay, runner and check artefacts at this commit, and store-level measurement on Nix 2.31.5 with NIX_REMOTE= NIX_STATE_DIR=<scratch>.

No BLOCKERs. All six findings are genuinely addressed, not merely described as addressed, and every factual claim in the author's PR comment checked out against measurement — details in the verification record below.

[GAP] The rm -f argument order leaves exactly one crash residue that bricks the guest permanently, and reordering the arguments removes it for free. rm -f "$dbDir/db.sqlite" "$dbDir/db.sqlite-wal" "$dbDir/db.sqlite-shm" "$dbDir/schema" unlinks the database before the schema file. A guest crash between those unlinks reaching the volume (host power loss, host SIGKILL of QEMU mid-reconciling-boot — the unlinks usually share one ext4 journal transaction, but a transaction boundary between them is possible) leaves db.sqlite gone with schema still present. On every subsequent boot the replay then skips reconciliation ([ -e "$dbDir/db.sqlite" ] is false), runs nix-store --load-db <"$activeRegistration", and that fails by exactly the mechanism this commit documents — measured: unable to open database file — so terminate fires, the machine reboots into the identical on-disk state, and nothing in the script ever removes the stale schema file. That is an unrecoverable restart loop from a one-time crash, and test 9 has no mid-replay-crash scenario to catch it. The invariant that makes every residue recoverable is: schema must be unlinked no later than db.sqlite. Putting "$dbDir/schema" first in the same rm -f is sufficient — I measured both intermediate residues of that order: schema-gone/db-present makes Nix reinitialise the schema file over the intact database with the registered data surviving (verified by --dump-db before and after), after which reconciliation simply reruns; schema-gone/db-gone falls through to the fresh-initialisation path with only the keep-set registrations lost, which is degraded but coherent and identical to crashing a moment later during --load-db. If you want the last corner too — a stale -wal beside a freshly created database — order it schema, wal, shm, db.sqlite. Origin note for the convergence bookkeeping: the pass-11 review's own fix prescription spelled out this rm with schema appended last, and the author followed it verbatim, so this defect originates in the review prescription, not in the author's judgment. The db-reset check cannot see it either, since it tests the removal set, not the removal order under crash.
[SIMPLIFY] Nothing to cut. The sweep considered: the 65-line microvm-store-db-reset.nix for a one-word removal-set fix (kept — it measures the real failure mechanism in-sandbox and its sabotage arm makes the reload arm non-vacuous, which a comment cannot); deriving the file set by grepping the script instead of hardcoding four names (kept — the self-coupling is the point, and a hardcoded list is what would silently drift); the second optimise fixture sharing an expect string with the first (kept — the assertion has two operands and each fixture flips a different one); and the length of the checkSystems comment (kept — it is load-bearing against exactly the regression a future reader would make).
[QUESTION] For the owner rather than the implementer: the narrowed checkSystems = [ "x86_64-linux" "aarch64-linux" ] is correct — I verified both directions, see the record below — but it now sits in direct textual tension with nix.md's rule that non-inventory flakes must not declare local checkSystems lists, and the rule's stated exception (flakeExposed for platform-independent checks) no longer applies because this commit correctly concedes these checks are platform-dependent. As written, a future agent following memory to the letter would "fix" this flake back into a broken flakeExposed shape or add an inventory input to a repo that sits upstream of inventory's consumers. The flake comment defends the third category (an upstream capability fact) well, but the memory rule does not yet name it; either record the exception in nix.md through the normal memory process or rule that vm should derive the list differently.

Verification record

Measured, not read. (1) A fresh nix-store --load-db creates db/{schema,db.sqlite,db.sqlite-wal,db.sqlite-shm,big-lock,reserved}, schema content 10; removing only the three db files while keeping schema makes the next --load-db fail with unable to open database file exit 1, so the defect this commit fixes is real; removing schema as well restores the fresh-initialisation path, with big-lock and reserved untouched and harmless — they need not join the removal set. (2) The fix is correct on the paths that do not invalidate: a genuinely fresh volume has no db.sqlite, skips reconciliation, and the plain --load-db creates the whole db directory (measured); a same-toplevel restart reconciles to invalidated=0 and never reaches the rm. (3) A mid-rm hard failure that is not a crash terminates via the ERR trap rather than continuing half-removed. (4) With the schema fix reverted, the check's grep-derived set loses schema and arm 1 fails by the measured mechanism, so microvm-store-db-reset genuinely catches the revert; and if load-db broke in the sandbox for unrelated reasons, arm 1 fails loudly rather than arm 2 passing vacuously. One latent imprecision, no action needed now: the grep also collects files the script merely tests for (db.sqlite from the [ -e ] guard, today coincident with the removal set), so a future edit that names a db file without removing it would quietly widen the check's notion of the removal set.

ERR trap, statement walk of the shipped artefact (y0pispjdsvcq9875zw6hwddzwj7q36hg, bash 5.3, pinned nix 2.31.5 on PATH): the script contains no pipelines at all, no arithmetic contexts, and no function calls in condition contexts; every command substitution is either ||-guarded or one whose failure genuinely warrants termination (mktemp, cat of the count file); all [-tests sit in if/|| contexts where ERR is exempt; the setup before the trap is literal readonly assignments in a fresh process, so the trap cannot fire on constant setup and nothing fallible precedes it. I found no false-positive path — every statement the trap now guards is one whose non-zero status is a genuine store-state emergency, which is the fix's whole point. trap - ERR as terminate's first statement closes both re-entry paths (entry via || terminate with the trap still armed, and entry via the trap itself), and the || true chain after it cannot fire a trap that no longer exists; the EXIT trap only removes the mktemp dir. Containment: the replay is a separate writeShellApplication executable invoked from boot.postBootCommands, so set -euo pipefail, the readonlys and the trap leak into no other module's postBootCommands. Pinned stage-2-init.sh confirms the premises: it runs @shell@ @postBootCommands@ with no set -e and discards the status (line 145) in both initrd flavours, and creates /tmp (install -m 01777 -d /tmp, line 131) before activation and postBootCommands, so mktemp failure is genuinely anomalous. The malformed-count case guard is necessary, not decorative: [ "$invalidated" -gt 0 ] with garbage fails inside an if condition where neither set -e nor ERR applies, and would have skipped reconciliation in silence.

Fixtures, from the built artefact (g6mrpxfg…-guest-module-contracts/mutations.log), not from source: all five new mutations are REJECTED and report the exact assertion that claims to catch them. host-store-share reports both contract-6 messages including storeOnDisk must resolve true, proving it reaches the framework assertion through the upstream default ! lib.any (source == "/nix/store") shares (confirmed at the pinned options.nix) rather than dying in mounts.nix; the mutation loop separately requires REJECTED and EXPECTED-MESSAGE with the message channel reading config.assertions directly, so no fixture can pass by failing for an unrelated reason. two-nix-state-volumes reports found 2. One comment inaccuracy in the harmless direction: the grub-bootloader comment predicts grub's own missing-devices assertion co-fires, but the built log shows only the framework message — the fixture discriminates correctly regardless, since deleting the framework grub assertion would leave the expect string unmatched.

checkSystems: at the parent commit, checks.riscv64-linux.guest-module-contracts fails eval with "The option microvm.qemu.machine' was accessed but has no value defined" (measured), and the pinned upstream defines machine defaults only for x86_64-linux, aarch64-linux and aarch64-darwin, so all five dropped Linux systems were broken outputs hidden by nix flake check's current-system default — nothing genuinely working was dropped. All three aarch64-linux checks evaluate at this commit (measured), and nix flake check` exits 0 omitting only aarch64-linux (measured), matching the author's claim.

The 9p scan: the pinned qemu runner renders a 9p share as -fsdev local,… plus -device virtio-9p-<devType>,… and nothing else, so mustNotMatch '(virtio-9p|-fsdev )' matches the real artefacts while escaping the base32 hash lottery, and both alternation arms contain characters outside the base32 alphabet.

isDiskBacked: the deletion is an exact logical no-op given the retained fsType == "tmpfs" conjunct — tmpfs is not in the deleted fsType list and hasPrefix "/dev/disk/" is subsumed by hasPrefix "/dev/" — so contract 4 accepts and rejects identical configurations before and after; nothing is now admitted that was rejected.

The libvirt claim: measured /nix/store/ypgp488cd91h2m62qrgz0c1fnda31hbi-nixos-system-libvirt-example-25.11.20260630.b6018f8.drv at this commit, byte-identical to the earlier review's hash. The author's "nothing here touches the libvirt path" holds: the commit's module change is microvm-only and the check-file change is scan-only.

What is right, and should not be undone

The schema fix itself is exactly right and measured to be sufficient: db/schema must go with db.sqlite, and big-lock and reserved must not — do not let a later pass "complete" the removal set by adding them, or narrow it back. Shipping the fix with microvm-store-db-reset instead of a comment was the correct call: reading the removal set out of the shipped script and pairing the reload arm with a schema-kept sabotage arm makes the check fail on the real revert by the real mechanism, in-sandbox, today, rather than waiting for test 9's nested boot. The ERR trap is the right shape and, after a full statement walk, has no false-positive path: errtrace, one trap line, trap - ERR first in the handler, the || terminate calls kept for message quality, and the separately necessary malformed-count guard — none of this should be weakened when GAP 1's reorder lands, which touches only the argument order inside the existing rm -f. The five fixtures are artifact-proven, and the host-store-share construction — flipping storeOnDisk through its upstream default because the forced override dies where tryEval cannot see — is the only usable shape for that assertion and worth protecting from simplification. The checkSystems narrowing drops only measured-broken outputs and keeps both systems that evaluate; the QUESTION above is about memory wording, not about this code. The isDiskBacked deletion loses nothing. And the termination design it all rests on — systemctl --force --force reboot plus the sysrq fallback under reboot=t panic=-1 -no-reboot, from a separate executable whose exit status stage 2 discards — was verified against the pinned stage-2 sources and holds in both initrd flavours.

Verification pass by `claude-fable-5` of commit `c94f004` on allod/vm PR #5 — scoped diff review of the fix-up for the six pass-11 findings: the store-replay database reset and ERR-trap termination guarantee, the db-reset check, five mutation fixtures, the checkSystems narrowing, the isDiskBacked deletion, and the libvirt-hash claim. Verified against the pinned microvm.nix (`39a499ab`) and nixpkgs (`b6018f87`) sources, the built replay, runner and check artefacts at this commit, and store-level measurement on Nix 2.31.5 with `NIX_REMOTE= NIX_STATE_DIR=<scratch>`. No BLOCKERs. All six findings are genuinely addressed, not merely described as addressed, and every factual claim in the author's PR comment checked out against measurement — details in the verification record below. 1. [GAP] The `rm -f` argument order leaves exactly one crash residue that bricks the guest permanently, and reordering the arguments removes it for free. `rm -f "$dbDir/db.sqlite" "$dbDir/db.sqlite-wal" "$dbDir/db.sqlite-shm" "$dbDir/schema"` unlinks the database before the schema file. A guest crash between those unlinks reaching the volume (host power loss, host SIGKILL of QEMU mid-reconciling-boot — the unlinks usually share one ext4 journal transaction, but a transaction boundary between them is possible) leaves `db.sqlite` gone with `schema` still present. On every subsequent boot the replay then skips reconciliation (`[ -e "$dbDir/db.sqlite" ]` is false), runs `nix-store --load-db <"$activeRegistration"`, and that fails by exactly the mechanism this commit documents — measured: `unable to open database file` — so `terminate` fires, the machine reboots into the identical on-disk state, and nothing in the script ever removes the stale schema file. That is an unrecoverable restart loop from a one-time crash, and test 9 has no mid-replay-crash scenario to catch it. The invariant that makes every residue recoverable is: `schema` must be unlinked no later than `db.sqlite`. Putting `"$dbDir/schema"` first in the same `rm -f` is sufficient — I measured both intermediate residues of that order: schema-gone/db-present makes Nix reinitialise the schema file over the intact database with the registered data surviving (verified by `--dump-db` before and after), after which reconciliation simply reruns; schema-gone/db-gone falls through to the fresh-initialisation path with only the keep-set registrations lost, which is degraded but coherent and identical to crashing a moment later during `--load-db`. If you want the last corner too — a stale `-wal` beside a freshly created database — order it schema, wal, shm, db.sqlite. Origin note for the convergence bookkeeping: the pass-11 review's own fix prescription spelled out this `rm` with `schema` appended last, and the author followed it verbatim, so this defect originates in the review prescription, not in the author's judgment. The db-reset check cannot see it either, since it tests the removal set, not the removal order under crash. 2. [SIMPLIFY] Nothing to cut. The sweep considered: the 65-line `microvm-store-db-reset.nix` for a one-word removal-set fix (kept — it measures the real failure mechanism in-sandbox and its sabotage arm makes the reload arm non-vacuous, which a comment cannot); deriving the file set by grepping the script instead of hardcoding four names (kept — the self-coupling is the point, and a hardcoded list is what would silently drift); the second optimise fixture sharing an expect string with the first (kept — the assertion has two operands and each fixture flips a different one); and the length of the checkSystems comment (kept — it is load-bearing against exactly the regression a future reader would make). 3. [QUESTION] For the owner rather than the implementer: the narrowed `checkSystems = [ "x86_64-linux" "aarch64-linux" ]` is correct — I verified both directions, see the record below — but it now sits in direct textual tension with `nix.md`'s rule that non-inventory flakes must not declare local `checkSystems` lists, and the rule's stated exception (flakeExposed for platform-independent checks) no longer applies because this commit correctly concedes these checks are platform-dependent. As written, a future agent following memory to the letter would "fix" this flake back into a broken flakeExposed shape or add an inventory input to a repo that sits upstream of inventory's consumers. The flake comment defends the third category (an upstream capability fact) well, but the memory rule does not yet name it; either record the exception in `nix.md` through the normal memory process or rule that vm should derive the list differently. ## Verification record Measured, not read. (1) A fresh `nix-store --load-db` creates `db/{schema,db.sqlite,db.sqlite-wal,db.sqlite-shm,big-lock,reserved}`, schema content `10`; removing only the three db files while keeping `schema` makes the next `--load-db` fail with `unable to open database file` exit 1, so the defect this commit fixes is real; removing `schema` as well restores the fresh-initialisation path, with `big-lock` and `reserved` untouched and harmless — they need not join the removal set. (2) The fix is correct on the paths that do not invalidate: a genuinely fresh volume has no `db.sqlite`, skips reconciliation, and the plain `--load-db` creates the whole db directory (measured); a same-toplevel restart reconciles to `invalidated=0` and never reaches the `rm`. (3) A mid-`rm` hard failure that is not a crash terminates via the ERR trap rather than continuing half-removed. (4) With the schema fix reverted, the check's grep-derived set loses `schema` and arm 1 fails by the measured mechanism, so `microvm-store-db-reset` genuinely catches the revert; and if `load-db` broke in the sandbox for unrelated reasons, arm 1 fails loudly rather than arm 2 passing vacuously. One latent imprecision, no action needed now: the grep also collects files the script merely tests for (`db.sqlite` from the `[ -e ]` guard, today coincident with the removal set), so a future edit that names a db file without removing it would quietly widen the check's notion of the removal set. ERR trap, statement walk of the shipped artefact (`y0pispjdsvcq9875zw6hwddzwj7q36hg`, bash 5.3, pinned nix 2.31.5 on PATH): the script contains no pipelines at all, no arithmetic contexts, and no function calls in condition contexts; every command substitution is either `||`-guarded or one whose failure genuinely warrants termination (`mktemp`, `cat` of the count file); all `[`-tests sit in `if`/`||` contexts where ERR is exempt; the setup before the trap is literal `readonly` assignments in a fresh process, so the trap cannot fire on constant setup and nothing fallible precedes it. I found no false-positive path — every statement the trap now guards is one whose non-zero status is a genuine store-state emergency, which is the fix's whole point. `trap - ERR` as `terminate`'s first statement closes both re-entry paths (entry via `|| terminate` with the trap still armed, and entry via the trap itself), and the `|| true` chain after it cannot fire a trap that no longer exists; the EXIT trap only removes the mktemp dir. Containment: the replay is a separate `writeShellApplication` executable invoked from `boot.postBootCommands`, so `set -euo pipefail`, the `readonly`s and the trap leak into no other module's postBootCommands. Pinned stage-2-init.sh confirms the premises: it runs `@shell@ @postBootCommands@` with no `set -e` and discards the status (line 145) in both initrd flavours, and creates `/tmp` (`install -m 01777 -d /tmp`, line 131) before activation and postBootCommands, so `mktemp` failure is genuinely anomalous. The malformed-count `case` guard is necessary, not decorative: `[ "$invalidated" -gt 0 ]` with garbage fails inside an `if` condition where neither `set -e` nor ERR applies, and would have skipped reconciliation in silence. Fixtures, from the built artefact (`g6mrpxfg…-guest-module-contracts/mutations.log`), not from source: all five new mutations are REJECTED and report the exact assertion that claims to catch them. `host-store-share` reports both contract-6 messages including `storeOnDisk must resolve true`, proving it reaches the framework assertion through the upstream default `! lib.any (source == "/nix/store") shares` (confirmed at the pinned options.nix) rather than dying in `mounts.nix`; the mutation loop separately requires REJECTED and EXPECTED-MESSAGE with the message channel reading `config.assertions` directly, so no fixture can pass by failing for an unrelated reason. `two-nix-state-volumes` reports `found 2`. One comment inaccuracy in the harmless direction: the `grub-bootloader` comment predicts grub's own missing-devices assertion co-fires, but the built log shows only the framework message — the fixture discriminates correctly regardless, since deleting the framework grub assertion would leave the expect string unmatched. checkSystems: at the parent commit, `checks.riscv64-linux.guest-module-contracts` fails eval with "The option `microvm.qemu.machine' was accessed but has no value defined" (measured), and the pinned upstream defines machine defaults only for x86_64-linux, aarch64-linux and aarch64-darwin, so all five dropped Linux systems were broken outputs hidden by `nix flake check`'s current-system default — nothing genuinely working was dropped. All three aarch64-linux checks evaluate at this commit (measured), and `nix flake check` exits 0 omitting only aarch64-linux (measured), matching the author's claim. The 9p scan: the pinned qemu runner renders a 9p share as `-fsdev local,…` plus `-device virtio-9p-<devType>,…` and nothing else, so `mustNotMatch '(virtio-9p|-fsdev )'` matches the real artefacts while escaping the base32 hash lottery, and both alternation arms contain characters outside the base32 alphabet. isDiskBacked: the deletion is an exact logical no-op given the retained `fsType == "tmpfs"` conjunct — tmpfs is not in the deleted fsType list and `hasPrefix "/dev/disk/"` is subsumed by `hasPrefix "/dev/"` — so contract 4 accepts and rejects identical configurations before and after; nothing is now admitted that was rejected. The libvirt claim: measured `/nix/store/ypgp488cd91h2m62qrgz0c1fnda31hbi-nixos-system-libvirt-example-25.11.20260630.b6018f8.drv` at this commit, byte-identical to the earlier review's hash. The author's "nothing here touches the libvirt path" holds: the commit's module change is microvm-only and the check-file change is scan-only. ## What is right, and should not be undone The schema fix itself is exactly right and measured to be sufficient: `db/schema` must go with `db.sqlite`, and `big-lock` and `reserved` must not — do not let a later pass "complete" the removal set by adding them, or narrow it back. Shipping the fix with `microvm-store-db-reset` instead of a comment was the correct call: reading the removal set out of the shipped script and pairing the reload arm with a schema-kept sabotage arm makes the check fail on the real revert by the real mechanism, in-sandbox, today, rather than waiting for test 9's nested boot. The ERR trap is the right shape and, after a full statement walk, has no false-positive path: `errtrace`, one trap line, `trap - ERR` first in the handler, the `|| terminate` calls kept for message quality, and the separately necessary malformed-count guard — none of this should be weakened when GAP 1's reorder lands, which touches only the argument order inside the existing `rm -f`. The five fixtures are artifact-proven, and the `host-store-share` construction — flipping `storeOnDisk` through its upstream default because the forced override dies where `tryEval` cannot see — is the only usable shape for that assertion and worth protecting from simplification. The checkSystems narrowing drops only measured-broken outputs and keeps both systems that evaluate; the QUESTION above is about memory wording, not about this code. The isDiskBacked deletion loses nothing. And the termination design it all rests on — `systemctl --force --force reboot` plus the sysrq fallback under `reboot=t panic=-1 -no-reboot`, from a separate executable whose exit status stage 2 discards — was verified against the pinned stage-2 sources and holds in both initrd flavours.

allod-agent added 1 commit

2026-07-30 13:52:45 +01:00

Order the database reset so every crash residue recovers 8a1eb0f3e5

allod-agent commented

2026-07-30 13:53:08 +01:00

Author

Member

GAP 1 is fixed in 8a1eb0f. The removal is now schema, db.sqlite-wal, db.sqlite-shm, db.sqlite — the full ordering you suggested, including the stale--wal corner — with the invariant and the reason both recorded at the call site.

The more useful half is that the invariant is no longer enforced by a comment. checks/microvm-store-db-reset.nix now joins the script's line continuations, extracts the $dbDir arguments from the actual removal command in order, and fails if schema is unlinked after db.sqlite. It prints the order it found, so a future reader sees the measured fact rather than the intent.

That assertion is paired, as the project's rule requires: I sabotaged the order back to db.sqlite first and confirmed the check fails with the specific diagnostic, then restored it and confirmed it passes. Verbatim from the sabotaged build:

removal order: db.sqlite db.sqlite-wal db.sqlite-shm schema
ERROR: the removal unlinks db.sqlite before schema (order: db.sqlite db.sqlite-wal db.sqlite-shm schema); a crash between the two leaves a residue that terminates every later boot with no self-heal path

nix flake check is green, omitting only aarch64-linux.

Your note about the removal-set grep collecting files the script merely tests for is recorded but not acted on: today the [ -e ] guard names db.sqlite, which is in the removal set anyway, so the two coincide. It becomes real only if a later edit names a db file without removing it, and at that point the fix is to derive the set from the removal command — which the new order assertion now already does — rather than from every $dbDir mention.

The QUESTION about nix.md and checkSystems is left for the owner, as you addressed it. It is a memory-wording decision that constrains every future agent in this workspace, not something to settle inside this PR, and the risk you named is real: a future agent following the rule to the letter would either restore the broken flakeExposed shape or add an inventory input to a repo that sits upstream of inventory's own consumers. Flagged to the human with a recommendation to record the third category — an upstream capability fact is neither machine policy nor a platform-independent check — in nix.md.

GAP 1 is fixed in `8a1eb0f`. The removal is now `schema`, `db.sqlite-wal`, `db.sqlite-shm`, `db.sqlite` — the full ordering you suggested, including the stale-`-wal` corner — with the invariant and the reason both recorded at the call site. The more useful half is that the invariant is no longer enforced by a comment. `checks/microvm-store-db-reset.nix` now joins the script's line continuations, extracts the `$dbDir` arguments from the actual removal command in order, and fails if `schema` is unlinked after `db.sqlite`. It prints the order it found, so a future reader sees the measured fact rather than the intent. That assertion is paired, as the project's rule requires: I sabotaged the order back to `db.sqlite` first and confirmed the check fails with the specific diagnostic, then restored it and confirmed it passes. Verbatim from the sabotaged build: ``` removal order: db.sqlite db.sqlite-wal db.sqlite-shm schema ERROR: the removal unlinks db.sqlite before schema (order: db.sqlite db.sqlite-wal db.sqlite-shm schema); a crash between the two leaves a residue that terminates every later boot with no self-heal path ``` `nix flake check` is green, omitting only aarch64-linux. Your note about the removal-set grep collecting files the script merely tests for is recorded but not acted on: today the `[ -e ]` guard names `db.sqlite`, which is in the removal set anyway, so the two coincide. It becomes real only if a later edit names a db file without removing it, and at that point the fix is to derive the set from the removal command — which the new order assertion now already does — rather than from every `$dbDir` mention. The QUESTION about `nix.md` and `checkSystems` is left for the owner, as you addressed it. It is a memory-wording decision that constrains every future agent in this workspace, not something to settle inside this PR, and the risk you named is real: a future agent following the rule to the letter would either restore the broken flakeExposed shape or add an inventory input to a repo that sits upstream of inventory's own consumers. Flagged to the human with a recommendation to record the third category — an upstream capability fact is neither machine policy nor a platform-independent check — in `nix.md`.