Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Run Targets, Init Mandate, And Default-Run Integration

This backlog captures three intertwined make-target and manifest-policy requirements raised against the current Makefile and system-*.cue set. They share manifests, harness scripts, and review surface, so they should land as one mainline track rather than scattered fixes.

Policy Statements

  1. make run and make run-display are the only operator run targets. Every focused proof and every alternate manifest, firmware, device, or measurement QEMU variant uses test-*, even when its recipe only starts QEMU. Scripted input driving, transcript assertions, timeout-based pass/fail, log greps, and harness script wrapping must never live in the run or run-display recipes.
  2. init usage is MANDATORY in every boot manifest. The boot init binary must be init (the capos-init ELF). Service or demo binaries such as capos-shell, credential-store, terminal-session, network-client, revocable-read, memoryobject-shared-parent, and per-demo entrypoints must be declared as services and launched by init, never as the top-level init binary.
  3. make run stays the default user-facing target demonstrating a sane, safe, full-featured (as of the current state) capOS instance. Milestone closeout follows the authoritative CLAUDE.md integration checklist.

Current State

Representative run-* recipes that contain test logic

This non-exhaustive snapshot identifies early migration families. Every listed target embeds input drivers, asserts, or harness invocations and therefore violates policy 1, but Gate C closure requires auditing all current run-* recipes in Makefile rather than treating this list as a complete inventory:

  • run-smoke, run-uefi, run-net
  • run-spawn
  • run-chat, run-adventure, run-terminal
  • run-credential
  • run-tcp-listen-authority
  • run-measure

Migrated Gate C families:

  • SSH focused proofs (2026-07-27 08:49 UTC): test-ssh-host-key, test-ssh-authorized-key, test-ssh-public-key-session, test-ssh-public-key-auth, and test-ssh-feature-policy. Their manifests, ISO names, harness locations, and positive transcript assertions are unchanged. The public-key harness leak guards omit the ambiguous seed substring because it matches the unrelated kernel preseeded paging diagnostic; they continue to reject direct private and secret terms.

  • Memory and IPC capability proofs (2026-07-27 11:13 UTC): test-revocable-read, test-memoryobject-shared, test-memoryobject-final-release-ordering, test-tlb-frame-reuse-ordering, test-ipc-zerocopy, and test-ringtap-failing-call. Their manifests, ISO names, harness locations, timeouts, transcript assertions, and the two ordering proofs’ -smp 2 and feature overrides are unchanged.

  • RAM-backed storage capability service proofs (2026-07-27 14:58 UTC): test-file-server-smoke, test-directory-server-smoke, test-store-namespace-smoke, test-storage-naming, test-userspace-store-smoke, and test-userspace-directory-file-smoke. Their manifests, ISO names, harness locations, timeouts, and transcript assertions are unchanged.

  • WASI and wasm-host language/runtime proofs (2026-07-27 17:34 UTC): test-wasm-host, test-wasi-hello-rust, test-wasi-hello-c, test-wasi-cli-args, test-wasi-env, test-wasi-random, test-wasi-random-ungranted, test-wasi-clock, test-wasi-clock-ungranted, test-wasi-poll, test-wasi-poll-realtime, test-wasi-poll-realtime-ungranted, test-wasi-preview1-refusals, test-wasi-stdio-fd, test-wasi-fs, and test-wasi-path-rename. Their manifests, ISO names, harness locations, timeouts, cargo feature overrides, and transcript assertions are unchanged. test-wasi-9p-reload and its fail-closed companion were already compliant and were not part of this wave.

  • CPU-isolation, SQPOLL, and AutoNoHz scheduler proofs (2026-07-27 20:14 UTC): test-scheduler-cpu-isolation-lease, test-scheduler-generic-sqpoll-nohz, test-scheduler-autonohz-policy-service, test-scheduler-cpu-isolation-create-fault, test-scheduler-cpu-isolation-pool-grant, and test-scheduler-cpu-isolation-pool-grant-default. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, -smp 4 settings, cargo feature overrides, and transcript assertions are unchanged.

  • libcapos and libcapos-posix C-substrate proofs (2026-07-27 23:09 UTC; evidence reconciled 2026-07-28 16:51 UTC): test-c-hello, test-c-wall-clock, test-c-wall-clock-ungranted, test-c-pipe, test-c-multifile, and test-c-libc-surface. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, cargo feature overrides, and transcript assertions are unchanged. Post-integration verification passed the wall-clock, ungranted wall-clock, pipe, multifile, and libc-surface proofs. A subsequent test-c-hello rerun exited through isa-debug-exit with status 1 and passed every existing harness assertion, completing six-proof green acceptance. The failed and passing test-c-hello controls used byte-identical QEMU commands in one session. Four attempts expired after 60 seconds with near-zero CPU use and empty UART logs, including KVM, TCG, and a sibling proof; the next identical KVM invocation completed in 14.47 seconds with 23,182 bytes of kernel UART output. This isolates an intermittent QEMU start stall on the host, not an invocation-mode difference. Its underlying mechanism remains unresolved, so a status-124 empty-UART result requires a rerun and is not evidence that the proof assertions failed.

  • Crypto key-custody proofs (2026-07-28 03:13 UTC; evidence corrected 2026-07-28 16:51 UTC): test-crypto-keyvault-custody, test-crypto-symmetric-key, and test-crypto-keysource-bootstrap. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, cargo feature overrides, and transcript assertions are unchanged. Initial implementation-worker attempts timed out before either UART emitted output. Subsequent independent artifact-level reruns used the same branch-built ISOs and recipe QEMU arguments: all three exited with the expected status 1 and passed their harness assertions. The three proofs are green post-migration. The status-124 runs match the same intermittent empty-UART startup-stall pattern seen by the C-substrate controls; the evidence does not isolate host contention or invocation mode as its cause.

  • Disk-backed storage and filesystem proofs (2026-07-28 09:51 UTC; evidence corrected 2026-07-28 10:11 UTC): test-storage-fs, test-storage-fat-read, test-file-read-window-limit, test-storage-persist, test-storage-persist-service, test-storage-writable, and test-storage-writable-recovery, plus the combined test-storage-fat32-timestamp-provenance aggregator. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, multi-pass disk sequencing, forced-poweroff windows, and transcript assertions are unchanged. Independent review executed the seven renamed recipes; all exited 0 with their harness assertions passing.

  • Installable-system proofs (2026-07-28 10:35 UTC; evidence completed 2026-07-28 11:42 UTC): test-installable-image-source, test-installable-data-region, test-installable-overlay, test-installable-generation, test-installable-provision, test-installable-update, test-installable-disk, and test-installable-install. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, multi-pass disk sequencing, and transcript assertions are unchanged. Post-migration verification executed all eight renamed recipes; all exited 0 with their harness assertions passing.

  • Block-device, record-store, and durable-coordinator proofs (2026-07-28 14:49 UTC): test-virtio-blk, test-multi-virtio-blk, test-blockdevice-target-identity, test-virtio-blk-failover, test-record-store, test-record-store-compaction, and test-task-coordinator-persist. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, multi-pass disk sequencing, forced-poweroff windows, and transcript assertions are unchanged. Post-migration verification executed all seven renamed recipes; all exited 0 with their harness assertions passing.

  • Boot-source proofs (2026-07-28 20:38 UTC): test-boot-iso, test-boot-iso-read, test-boot-iso-failclosed, test-init-embedding, test-limine-disk-boot-modules, and test-limine-disk-boot-modules-failclosed. Their manifest sources, manifest bins, ISO names, ISO_BOOT_BINS, harness locations, timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions are unchanged. Verification completed 2026-07-28 21:33 UTC with these per-recipe outcomes: test-boot-iso exited 0; test-boot-iso-read exited 0; test-boot-iso-failclosed exited 0; test-init-embedding exited 0; test-limine-disk-boot-modules exited 0; and test-limine-disk-boot-modules-failclosed exited 0 after passing its missing, length-mismatch, SHA-mismatch, duplicate, and undeclared cases. All six recipes passed their existing harness assertions. test-boot-iso-read, test-init-embedding, test-limine-disk-boot-modules, and test-limine-disk-boot-modules-failclosed first encountered the documented empty-UART startup stall; their reruns passed without recipe or assertion changes. run-smoke, including its shared tools/qemu-boot-iso-smoke.sh and CAPOS_PREBUILT_ISO path, and the wider default-boot gate run-default-boot are explicitly outside this wave and remain unchanged.

  • Hardware-audit and hardware-grant-cycle proofs (2026-07-29 00:15 UTC): test-hardware-audit, test-hardware-audit-dmabuffer, test-hardware-audit-drain-cursor, test-hardware-audit-grant-source, test-hardware-audit-interrupt-waiter, and test-hardware-grant-cycle. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions are unchanged. Post-migration verification executed all six renamed recipes; all exited 0 with their existing harness assertions passing. test-hardware-audit first encountered the documented status-124 empty-UART startup stall twice; an identical rerun without a PTY passed without recipe or assertion changes.

  • Endpoint queue/facet, crash-disconnect, and untrusted-exhaustion proofs (2026-07-29 01:52 UTC): test-endpoint-queue-limit, test-endpoint-oversized-params, test-endpoint-recv-drain-refill-race, test-endpoint-drop-inflight-uaf, test-endpoint-facet-redelegation, test-crash-disconnect, test-crash-disconnect-multithread, test-untrusted-exhaustion, test-untrusted-exhaustion-core, test-untrusted-exhaustion-spawn-oom-fault, and test-untrusted-exhaustion-captable. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets (including the two -smp 4 proofs), cargo feature overrides, CUE tags, aggregator sequencing, and transcript assertions are unchanged. Post-migration verification executed every renamed recipe: the five endpoint proofs and two crash proofs each exited 0, and the exhaustion aggregator exited 0 after each of its three member recipes exited 0. All existing harness assertions passed without a status-124 empty-UART startup stall.

  • Resource-limit proofs (2026-07-29 03:21 UTC): test-in-flight-call-limit, test-ring-scratch-limit, and test-reply-scratch-limit. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions are unchanged. Post-migration verification executed all three renamed recipes: test-in-flight-call-limit exited 0; test-ring-scratch-limit exited 0; and test-reply-scratch-limit exited 0. All existing harness assertions passed without a status-124 empty-UART startup stall.

  • Shell, login, and local-user proofs (completed 2026-07-29 10:07 UTC): test-shell, test-shell-uptime, test-shell-log, test-shell-fs, test-system-manual-smoke, test-restricted-shell-launcher, test-login, test-login-setup, and test-local-users. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, granted/ungranted sequencing, and transcript assertions are unchanged. Post-migration verification executed every renamed recipe; each exited 0 with its existing harness assertions passing, without a status-124 empty-UART startup stall. The launcher proof was migrated after the focused launcher repair restored its denial-then-legitimate-launch sequence.

  • Scheduler fairness, scale, and baseline proofs (completed 2026-07-29 11:44 UTC): test-thread-fairness, test-thread-fairness-interactive, test-thread-fairness-weight-change, test-thread-fairness-sleeper-floor, test-thread-scale, test-smp-process-scale, test-smp2-smokes, and test-linux-thread-scale-baseline. Their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, CPU/thread counts, and transcript assertions are unchanged. Post-migration verification executed every renamed recipe; each exited 0 with its existing harness assertions passing. The four fairness recipes each encountered two status-124 attempts with zero-byte console and terminal UART logs before passing in a serialized no-PTY rerun. The first two test-smp2-smokes attempts passed their run-smoke member and then encountered the same status-124 empty-UART stall in the run-spawn member; the serialized no-PTY rerun passed both members. The scale harnesses and Linux baseline passed on their first post-migration executions.

  • POSIX process, exec, descriptor, and stdio proofs (completed 2026-07-29 12:47 UTC): test-posix-args-smoke, test-posix-cwd, test-posix-env-smoke, test-posix-execve-inherit-smoke, test-posix-fcntl, test-posix-fd-inherit-default, test-posix-identity, test-posix-isatty, test-posix-open-dir-fd, test-posix-open-smoke, test-posix-pipe-smoke, test-posix-spawn-smoke, test-posix-stdio-smoke, and test-posix-stdio-terminal-smoke. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, granted/ungranted sequencing, and transcript assertions are unchanged. Post-migration verification executed every renamed recipe; each exited 0 with its existing harness assertions passing. test-posix-args-smoke first encountered a status-124 startup stall with zero-byte console and terminal UART logs, then passed an identical serialized no-PTY rerun. The first three test-posix-stdio-terminal-smoke attempts reached userspace but received only m-driver from the driver’s fixed-delay send. The driver now waits for the smoke’s own ready-for-input banner before sending once, preserving the fixed input and assertions while ordering the complete from-driver round trip after the TerminalSession read is ready.

  • POSIX libc, networking, and shell proofs (completed 2026-07-29 13:39 UTC): test-posix-dns-smoke, test-posix-file-backing-smoke, test-posix-getaddrinfo, test-posix-printf, test-posix-read-builtin, test-posix-setjmp, test-posix-shell-smoke, test-posix-signal-time, test-posix-socket-poll-select, test-posix-strftime, test-posix-terminal-forward, and test-posix-test-builtin. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, granted/ungranted sequencing, and transcript assertions are unchanged. Post-migration verification executed every renamed recipe. The eleven runnable proofs exited 0 with their existing assertions passing; the retired test-posix-dns-smoke target preserved its exit-2 diagnostic that the removed QEMU-only kernel socket owner cannot provide validation.

  • NVMe controller and queue bring-up proofs (completed 2026-07-29 16:00 UTC): test-cloud-provider-nvme-readonly-bind, test-cloud-provider-nvme-controller-reset, test-cloud-provider-nvme-admin-queue-materialization, test-cloud-provider-nvme-controller-enable, test-cloud-provider-nvme-admin-identify, test-cloud-provider-nvme-admin-completion-wait-ack, test-cloud-provider-nvme-io-queue-create, test-cloud-provider-nvme-io-read, test-cloud-provider-nvme-io-write, test-cloud-provider-nvme-io-second-lba, test-cloud-provider-nvme-io-multiblock, and test-cloud-provider-nvme-io-completion-interrupt. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets (including the NVMe device and backing-image arguments), cargo feature overrides, ladder order, and transcript assertions are unchanged. Post-migration verification executed every renamed recipe; all twelve passed their existing assertions. The read-only-bind proof first encountered two status-124 attempts with zero-byte console and terminal UART logs; its unchanged pre-rename control passed, followed by a passing serialized no-PTY rerun of the renamed target.

  • NVMe block-device and filesystem durability proofs (completed 2026-07-29 17:54 UTC): test-cloud-provider-nvme-blockdevice-read, test-cloud-provider-nvme-blockdevice-read-graduated, test-cloud-provider-nvme-blockdevice-arbitrary-lba-read, test-cloud-provider-nvme-blockdevice-writeblocks-durability, test-cloud-provider-nvme-blockdevice-multiprp-window, test-cloud-provider-nvme-blockdevice-flush, test-cloud-provider-nvme-blockdevice-flush-crash-consistency, test-cloud-provider-nvme-blockdevice-reboot-persistence, test-cloud-provider-nvme-consumer-sync-to-flush, test-cloud-provider-nvme-persistent-store-sync-to-flush, test-cloud-provider-readonly-fs-over-nvme, test-cloud-provider-readonly-fs-over-nvme-multifile, test-cloud-provider-writable-fs-over-nvme, test-cloud-provider-writable-fs-over-nvme-recovery, test-cloud-provider-fat-read-over-nvme, and test-cloud-provider-persistent-store-over-nvme. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets (including NVMe devices and backing-file paths), cargo feature overrides, and transcript assertions are unchanged. Per-recipe outcomes: test-cloud-provider-nvme-blockdevice-read passed; test-cloud-provider-nvme-blockdevice-read-graduated passed; test-cloud-provider-nvme-blockdevice-arbitrary-lba-read passed; test-cloud-provider-nvme-blockdevice-writeblocks-durability passed; test-cloud-provider-nvme-blockdevice-multiprp-window passed; test-cloud-provider-nvme-blockdevice-flush passed; test-cloud-provider-nvme-blockdevice-flush-crash-consistency passed; test-cloud-provider-nvme-blockdevice-reboot-persistence passed; test-cloud-provider-nvme-consumer-sync-to-flush passed; test-cloud-provider-nvme-persistent-store-sync-to-flush passed; test-cloud-provider-readonly-fs-over-nvme passed; test-cloud-provider-readonly-fs-over-nvme-multifile passed; test-cloud-provider-writable-fs-over-nvme passed; test-cloud-provider-writable-fs-over-nvme-recovery passed; test-cloud-provider-fat-read-over-nvme passed; and test-cloud-provider-persistent-store-over-nvme passed. Each recipe built and ran under its own feature set. test-cloud-provider-nvme-blockdevice-read first encountered two status-124 attempts with zero-byte console and terminal UART logs. Its no-PTY rerun booted and exposed a stale predecessor-proof regression: the proof still treated the graduated production arbitrary-window arm as fixed. Review remediation aligned its negative assertions with the production bounds (zero count, more than one PRP1 page, and namespace overrun) while retaining (startLba=2, count=2) as the proof’s successful request; no proof-only admission divergence remains. The repaired recipe passed. The other fifteen recipes passed without an empty-UART startup stall. The reboot-persistence, flush-crash-consistency, and writable-filesystem recovery recipes each created their backing file once before boot 1 and reused that same untruncated file for boot 2. All three multi-boot assertions passed, preserving their durability evidence.

  • Virtio-net bring-up, authority, and queue-materialization proofs (completed 2026-07-29 18:59 UTC): test-cloud-provider-virtio-net, test-cloud-provider-virtio-net-bringup, test-cloud-provider-virtio-net-legacy-select, test-cloud-provider-virtio-net-msix-function-enable, test-cloud-provider-virtio-net-tx-authority-bundle, test-cloud-provider-virtio-net-tx-queue-materialization, test-cloud-provider-virtio-net-rx-queue-materialization, test-cloud-provider-nic-bound-legacy, test-cloud-provider-nic-bound-legacy-large-queue, and test-cloud-provider-nic-bound-real-polled-driver. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature selection, and transcript assertions are unchanged. The headline, bring-up, MSI-X function-enable, authority-bundle, and both queue-materialization recipes retained their individual cloud_virtio_net_*_proof feature overrides; the legacy-select, two legacy-bind, and real-polled-driver recipes retained their manifest-armed default-kernel builds. Per-recipe outcomes: test-cloud-provider-virtio-net passed; test-cloud-provider-virtio-net-bringup passed; test-cloud-provider-virtio-net-legacy-select passed; test-cloud-provider-virtio-net-msix-function-enable passed; test-cloud-provider-virtio-net-tx-authority-bundle passed; test-cloud-provider-virtio-net-tx-queue-materialization passed; test-cloud-provider-virtio-net-rx-queue-materialization passed; test-cloud-provider-nic-bound-legacy passed; test-cloud-provider-nic-bound-legacy-large-queue passed; and test-cloud-provider-nic-bound-real-polled-driver passed. The ordinary and large-queue legacy targets retained identical device arguments except for the latter’s rx_queue_size=1024; legacy-select retained the ordinary legacy device shape without the datapath assertions. Every initial PTY-backed execution built its selected kernel and then encountered a status-124 startup stall with zero-byte kernel and terminal UART logs. Identical serialized no-PTY reruns passed all ten unchanged harnesses.

  • Userspace NIC-driver ownership, queue, and interrupt proofs (completed 2026-07-29 22:12 UTC): test-cloud-prod-nic-driver-userspace-features-ok, test-cloud-prod-nic-driver-userspace-ownable-vring, test-cloud-prod-nic-driver-userspace-queue-enable-driver-ok, test-cloud-prod-nic-driver-userspace-rx-bringup, test-cloud-prod-nic-driver-userspace-nic-cap-roundtrip, test-cloud-prod-nic-driver-userspace-irq-ownership, test-cloud-prod-nic-driver-userspace-clean-tx-rx-split, and test-cloud-prod-nic-driver-userspace-sustained-receive-pool. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, and cargo feature overrides are unchanged. Existing transcript assertions remain except that the descriptor-ring pinning refusal is now anchored to the exact application exception observed by the userspace proof process, rather than unanchored labels from a teardown diagnostic. Each recipe built and ran under its own cloud_virtio_net_userspace_*_proof feature. Per-recipe outcomes: test-cloud-prod-nic-driver-userspace-features-ok passed; test-cloud-prod-nic-driver-userspace-ownable-vring passed; test-cloud-prod-nic-driver-userspace-queue-enable-driver-ok passed; test-cloud-prod-nic-driver-userspace-rx-bringup initially reached its complete proof transcript but failed because its unanchored free_result and free_reason greps had historically been satisfied by a release/teardown diagnostic that no longer appeared. The proof now validates the voluntary freeBuffer application exception and emits one role-anchored refusal line; test-cloud-prod-nic-driver-userspace-nic-cap-roundtrip passed; test-cloud-prod-nic-driver-userspace-irq-ownership passed; test-cloud-prod-nic-driver-userspace-clean-tx-rx-split passed; and test-cloud-prod-nic-driver-userspace-sustained-receive-pool passed on its first run. No recipe encountered an empty-UART startup stall. The IRQ-ownership harness rejected a transcript mutation that changed every computed positive int_injected count to zero, and the clean TX/RX split harness rejected a transcript mutation that inserted the forbidden coupled receive/self-stimulus path. Both negative controls exited 1, confirming the proof call sites propagate ownership-boundary failures.

  • Virtio-net datapath, interrupt-delivery, and teardown proofs (completed 2026-07-29 23:35 UTC): test-cloud-provider-virtio-net-rx-buffer-post, test-cloud-provider-virtio-net-rx-userspace-submit, test-cloud-provider-virtio-net-rx-polled-completion, test-cloud-provider-virtio-net-rx-production-idt-dispatch, test-cloud-provider-virtio-net-rx-msix-wait-ack, test-cloud-provider-virtio-net-rx-device-autonomous-msix, test-cloud-provider-virtio-net-tx-submit-doorbell, test-cloud-provider-virtio-net-tx-msix-wait-ack, test-cloud-provider-virtio-net-polled-provider-default, test-cloud-provider-virtio-net-polled-driver-death, and test-cloud-provider-virtio-net-polled-teardown. Their manifest sources, manifest bins, ISO names, harness locations, 60-second timeouts, QEMU argument sets, MSI-X vector counts, queue sizes, cargo feature selection, and transcript assertions are unchanged. The first eight recipes retained their individual cloud_virtio_net_*_proof feature overrides; the three polled-provider recipes retained their manifest-armed default-kernel builds. Every recipe passed its existing harness on the first post-migration execution with non-empty kernel UART output: test-cloud-provider-virtio-net-rx-buffer-post passed; test-cloud-provider-virtio-net-rx-userspace-submit passed; test-cloud-provider-virtio-net-rx-polled-completion passed; test-cloud-provider-virtio-net-rx-production-idt-dispatch passed; test-cloud-provider-virtio-net-rx-msix-wait-ack passed; test-cloud-provider-virtio-net-rx-device-autonomous-msix passed with its existing recorded outcome; test-cloud-provider-virtio-net-tx-submit-doorbell passed; test-cloud-provider-virtio-net-tx-msix-wait-ack passed; test-cloud-provider-virtio-net-polled-provider-default passed; test-cloud-provider-virtio-net-polled-driver-death passed; and test-cloud-provider-virtio-net-polled-teardown passed. No recipe needed an empty-UART startup-stall rerun. Focused negative controls removed the stale_dma_buffer_blocked=true denial evidence from each teardown transcript; both harnesses rejected the altered transcript with exit 1.

  • Userspace smoltcp network-stack proofs (completed 2026-07-30 00:13 UTC): test-cloud-prod-network-stack-process-smoltcp-skeleton, test-cloud-prod-network-stack-smoltcp-socket-caps, test-cloud-prod-network-stack-smoltcp-udp-socket-cap-ipc, test-cloud-prod-network-stack-smoltcp-tcp-socket-cap-ipc, test-cloud-prod-network-stack-smoltcp-tcp-socket-cap-ipc-vm, test-cloud-prod-network-stack-smoltcp-tcp-listener-roundtrip, test-cloud-prod-network-stack-smoltcp-tcp-listener-roundtrip-vm, test-cloud-prod-userspace-network-stack-smoltcp, test-cloud-prod-userspace-network-stack-smoltcp-vm, and test-cloud-prod-network-stack-dhcp-ipv4-config. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets and user-mode forwarding options, cargo feature overrides, and transcript assertions are unchanged. The process-skeleton, in-process socket-cap, and UDP-cap IPC recipes retained cloud_virtio_net_userspace_clean_tx_rx_split_proof; the TCP, served-listener, and DHCP recipes retained cloud_virtio_net_userspace_sustained_receive_pool_proof. The subsequently migrated test-cloud-prod-icmp-echo-reply proof’s tcp_listener_regression evidence label and matching host assertion now name test-cloud-prod-userspace-network-stack-smoltcp. Its full target passed on 2026-07-30 00:31 UTC, including the renamed served-listener prerequisite and the ICMP harness’s updated evidence assertion. Per-recipe outcomes: test-cloud-prod-network-stack-process-smoltcp-skeleton passed after its initial PTY-backed execution produced zero-byte kernel and terminal UART logs and an identical serialized no-PTY rerun completed the proof; test-cloud-prod-network-stack-smoltcp-socket-caps passed; test-cloud-prod-network-stack-smoltcp-udp-socket-cap-ipc passed; test-cloud-prod-network-stack-smoltcp-tcp-socket-cap-ipc passed and drove test-cloud-prod-network-stack-smoltcp-tcp-socket-cap-ipc-vm; test-cloud-prod-network-stack-smoltcp-tcp-listener-roundtrip passed and drove test-cloud-prod-network-stack-smoltcp-tcp-listener-roundtrip-vm; test-cloud-prod-userspace-network-stack-smoltcp passed and drove test-cloud-prod-userspace-network-stack-smoltcp-vm; and test-cloud-prod-network-stack-dhcp-ipv4-config passed. Each driver/VM pair retained common build inputs but distinct launch roles: the driver invokes its host harness, while the VM sibling directly launches QEMU with its pidfile. The host harnesses retained their dynamic TCP hostfwd mappings. Negative controls changed the socket-cap queue-address refusal into a successful register read, changed the UDP malformed-send rejection into an acceptance, and changed the TCP listener receiver cookie away from its direct-listener value. The socket-cap and UDP assertion scripts exited 1, and both TCP receiver-cookie predicates rejected the altered transcript.

  • ICMP and IPv6 datapath proofs (completed 2026-07-30 01:12 UTC): test-cloud-prod-icmp-echo-reply, test-cloud-prod-icmp-echo-reply-real-nic-datapath, test-cloud-prod-icmp-echo-reply-real-nic-datapath-vm, test-cloud-prod-icmpv6-echo-reply, test-cloud-prod-ipv6-link-local-nd, test-cloud-prod-ipv6-ra-slaac, test-cloud-prod-ipv6-dhcpv6-gce-config, test-cloud-prod-ipv6-real-nic-datapath, and test-cloud-prod-ipv6-real-nic-datapath-vm. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions are unchanged. Per-recipe outcomes: the ICMPv4 echo-reply, ICMPv6 echo-reply, IPv6 link-local/ND, RA/SLAAC, and local GCE-shaped DHCPv6 configuration targets passed their status-aware harness assertions; the ICMPv4 real-NIC driver passed and drove its -vm sibling; and the IPv6 real-NIC driver passed and drove its -vm sibling. Each target built through its own recipe variables. None required an empty-UART startup-stall rerun, and every proof ran under local QEMU without a cloud resource operation. The ICMPv4 and ICMPv6 in-process proofs retain their address-family-specific manifests and assertions over the same QEMU device arguments, including the ICMPv4 proof’s served-listener prerequisite. Each real-NIC driver retains a host harness while its sibling remains the QEMU-only launch target. The ICMPv4 harness retains its legacy virtio-net socket backend (disable-modern=on,vectors=0), while the IPv6 harness retains its modern virtio-net socket backend; neither family adds a hostfwd mapping.

  • Network usability and diagnostics proofs (completed 2026-07-30 02:28 UTC): test-network-dhcpv4-lease-lifecycle, test-network-socket-readiness, test-network-transport-status, test-network-transport-timeout, test-network-status-tool, test-network-packet-trace, test-network-system-dnsresolver, test-network-ping-tool, and test-network-ping6-tool. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions are unchanged. The transport status and timeout targets continue to share the same manifest and ISO while applying distinct harness assertions. Per-recipe outcomes: all nine targets passed their existing status-aware harnesses after QEMU reached the preserved timeout path. test-network-dhcpv4-lease-lifecycle produced 20,713 bytes of kernel UART output; test-network-socket-readiness, 18,695; test-network-transport-status, 25,945; test-network-transport-timeout, 25,991; test-network-status-tool, 39,399; test-network-packet-trace, 42,080; test-network-system-dnsresolver, 20,816; test-network-ping-tool, 36,599; and test-network-ping6-tool, 36,619. No target produced the zero-byte kernel UART startup-stall signature, so none required the serialized no-PTY rerun.

  • DDF hardware-grant, interrupt, and audit-service proofs (migrated 2026-07-30 07:09 UTC): test-devicemmio-grant, test-devicemmio-grant-exit, test-dmapool-grant, test-dmapool-grant-exit, test-interrupt-grant, test-interrupt-grant-x2apic, test-ddf-interrupt-stale-notification, test-ddf-audit-reader-smoke, test-ddf-audit-service-smoke, test-ddf-audit-service-keyed-signature, test-ddf-audit-service-persist-reboot, and test-ddf-audit-reader-runtime-admission. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions are unchanged. test-ddf-interrupt-stale-notification continues to use manifests/system-ddf-provider-consumer.cue; the out-of-scope run-ddf-provider-consumer target remains named run-* because it is still a registered loopyard validation-gate value.

    Per-recipe outcomes from serialized no-PTY executions: test-devicemmio-grant passed; test-devicemmio-grant-exit passed; test-dmapool-grant reached a clean kernel halt but failed its existing harness count assertion because the kernel UART omitted the separate DMABuffer.map already has a read-only user mapping diagnostic while retaining the userspace rejection marker; test-dmapool-grant-exit passed; test-interrupt-grant passed; test-interrupt-grant-x2apic passed; test-ddf-interrupt-stale-notification passed; test-ddf-audit-reader-smoke passed; test-ddf-audit-service-smoke passed; test-ddf-audit-service-keyed-signature passed; test-ddf-audit-service-persist-reboot passed; and test-ddf-audit-reader-runtime-admission passed. The DMAPool proof initially failed the same stale kernel-log assertion on a second renamed-target execution and on an execution of the unmodified main recipe run-dmapool-grant against the same current sources. The focused repair moved the diagnostic proof to the typed userspace exception contract and passed two serialized make test-dmapool-grant runs. None of the original red executions produced the zero-byte kernel and terminal UART startup-stall signature.

  • Cloud DDF grants, provider cap waiter, IOMMU abort accounting, and NVMe synchronous-I/O proofs (migrated 2026-07-30 09:31 UTC): test-cloud-devicemmio-grant, test-cloud-dmapool-grant, test-cloud-interrupt-grant, test-cloud-provider-cap-waiter, test-ddf-iommu-abort-leak-accounting, test-cloud-provider-nvme-io-sync-read, and test-cloud-provider-nvme-io-sync-read-bytes. Their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions are unchanged. test-ddf-iommu-abort-leak-accounting remains an alias of the retained run-iommu-remapping validation-gate target. The four cloud grant/waiter recipes retain their existing target/run-*-{kernel,terminal}.log paths; the coordinated artifact-log rename remains deferred.

    The first serialized PTY-backed pass produced zero-byte kernel and terminal UART logs and exited 2 before harness assertions for every recipe except test-ddf-iommu-abort-leak-accounting, which passed with non-empty UART logs. The required serialized no-PTY reruns then passed test-cloud-devicemmio-grant, test-cloud-dmapool-grant, test-cloud-interrupt-grant, test-cloud-provider-cap-waiter, test-cloud-provider-nvme-io-sync-read, and test-cloud-provider-nvme-io-sync-read-bytes. No proof assertion or recipe content changed in response to the initial startup failures. Gate C remains open for run-smoke, run-default-boot, the remaining UEFI, raw-disk boot, general run-net, network-address ABI, and IPv6 TCP L4 proofs; the remaining service proofs; the remaining resource-profile proof (run-resource-profile); remaining language/runtime proofs; other storage families; the two retained POSIX validation-gate targets (run-posix-file and run-posix-system); the scheduler lifecycle proof (run-scheduling-context); the remote-session Web UI L4 proof family; remaining hardware, device, and cloud-provider proof families; and measurement variants still named run-* in Makefile.

(run-network-client, run-telnet(-vm), and run-ssh-gateway-terminal-host(-vm) were on this list but are now exit-2 retirement stubs with no test logic, retired with the kernel socket owner.)

Compliant run-* recipes (QEMU-only):

  • run – interactive, manifest-driven, terminal on stdio.
  • run-display – interactive variant with QEMU display.

Manifests violating the init mandate

The deferred shell-led migration list is empty. Gate B stays open for the loader validation rule and the final re-grep.

Migrated to init-owned service graphs (Gate B 4/4, 2026-07-27 04:14 UTC): system-shell-uptime.cue, system-shell-uptime-ungranted.cue, system-shell-fs.cue, system-shell-fs-ungranted.cue, and system-manual-smoke.cue now boot init and launch capos-shell as a single init-spawned service named shell under exitWhenServiceExits. The shell service keeps the exact caps it held as init. The uptime and filesystem granted/ungranted pairs preserve their timer and root asymmetry; those sources and stdio are minted per child and do not broaden init. The manual proof forwards its read-only manual grant through init. Their proofs (make test-shell-uptime, make test-shell-fs, and make test-system-manual-smoke) preserve their existing behavior assertions and add the parameterized assert_init_owned_shell_service topology pin.

Migrated to init-owned service graphs (Gate B 1/3, 2026-07-17 20:02 UTC): system-smoke.cue, system-shell.cue, system-login.cue, and system-login-setup.cue now boot init and launch capos-shell as a single init-spawned service named shell under exitWhenServiceExits. init holds only the bootstrap authority (console/boot/spawner) plus the scoped grants it forwards; the shell service receives exactly the caps it held as init (terminal moved, the rest shared – system-shell.cue adds console/wall_clock grants, with stdio (kernel:endpoint) per-child minted so init never holds it; system-login-setup.cue adds setup). Their proofs (make run-smoke, make test-shell, make test-login, make test-login-setup) pin the init-owned topology via the parameterized assert_init_owned_shell_service in tools/qemu-shell-smoke.sh (init as PID 2 with its cap count, capos-shell spawned as the shell service with its scoped cap count). No init/src/main.rs change was required: the generic manifest spawn loop already supports this shape. The init-mandate loader rule (rejecting a non-init top-level binary) is the separate successor task init-mandate-loader-validation-rule.

Migrated to init-owned service graphs (Gate B, 2026-07-17): system-local-users.cue, system-credential.cue, and system-terminal.cue now boot init and launch the former top-level binary (capos-shell, credential-store, terminal-session) as a single init-spawned service under exitWhenServiceExits. init holds only the bootstrap authority (console/boot/spawner) plus the scoped grants it forwards; each service receives exactly the caps it held as init. Their proofs (make test-local-users, make run-credential, make run-terminal) assert the same boundary properties, with the local-users boundary check relocated to assert_init_owned_shell_service in tools/qemu-shell-smoke.sh.

Migrated to init-owned service graphs (Gate B 3/3, 2026-07-17 19:44 UTC): system-revocable-read.cue and system-memoryobject-shared.cue now boot init and launch their former top-level binary (revocable-read, memoryobject-shared-parent) as a single init-spawned service under exitWhenServiceExits. Each service keeps exactly the caps it validated as init (revocable-read: console/boot/spawner, since it reads the forwarded BootPackage and spawns revocation-observer; memoryobject-shared-parent: console/frames/spawner) – init holds only console/boot/spawner, with frames a per-child-minted source the spawner grants the parent fresh. Their proofs (make test-revocable-read, make test-memoryobject-shared) were strengthened to pin the init-owned topology: the created process 2 for service 'init' / spawned process 3/spawned process 4 lines plus per-process cap counts assert init (PID 2) owns the graph and no bootstrap authority leaks into the demo processes (PID 3/4).

Manifests already compliant: system.cue, system-adventure.cue, system-chat.cue, system-spawn.cue, system-measure.cue, system-restricted-shell-launcher.cue, all remaining system-ssh-*.cue (system-telnet.cue, system-network-client.cue, and system-ssh-gateway-terminal-host.cue are removed with the kernel socket owner).

Default-run feature integration gap

make run boots system.cue, which already wires the anonymous shell, the login flow with the seeded password verifier in MOTD, the chat/adventure demos, chat/adventure spawn instructions, the host-local remote-session CapSet gateway, and (as of 2026-05-14 09:07 UTC) the self-served remote-session-web-ui service. The Telnet research demo is retired (the focused make run-telnet / system-telnet.cue path and its gateway demo are removed with the kernel socket owner). The retired SSH gateway terminal host is absent by design. Its future SSH Shell Gateway successor remains absent from the default path and its MOTD.

The default make run recipe now attaches virtio-net with host-local remote CapSet forwarding to guest port 2327 and host-local web UI forwarding to guest port 8080. Both use the same ?=-overridable host port with fallback-to-free-port behavior implemented in tools/qemu-run-hostfwd.py. Future network-backed milestones, including the SSH Shell Gateway, remain subject to the authoritative integration checklist above.

Open Gates

Gate A: Naming and contract

  • Strict split selected (2026-07-18 01:04 UTC). run and run-display are the only operator entrypoints. Every other current run-* recipe, including run-uefi, run-net, and run-measure, moves to test-* in Gate C even if the resulting recipe only starts QEMU. This accepts a larger one-time rename so the prefix remains stable when a recipe gains or loses automation. The permissive split was rejected because deciding what counts as the default manifest or a documented variation would reintroduce case-by-case review and naming drift.
  • The CLAUDE.md “Build and Test” section and REVIEW.md define the strict prefix and behavior contract. They identify the current extra run-* names as Gate C migration debt rather than precedent.

Gate B: Init mandate enforcement

  • For every non-compliant manifest above, restructure so the init binary is init and the previous top-level binary becomes a service. Preserve the focused-proof intent: the service receives the same scoped caps it had as init, init holds only the bootstrap authority needed to spawn and supervise it, and the smoke/proof transcript continues to assert the same boundary properties. (2026-07-17: the primary shell-family manifests – system-smoke.cue, system-shell.cue, system-login.cue, system-login-setup.cue – are migrated. 2026-07-27: the deferred shell-led focused proofs (system-shell-uptime*, system-shell-fs*, and system-manual-smoke.cue) are also migrated. The checkbox remains open pending the loader rule and final re-grep.)
  • Add a manifest-loader validation rule (or mkmanifest check) that rejects any manifest whose initConfig.init.binary is not init. The rule should also reject the field being missing. Update host tests to cover the negative case.
  • Update every doc that currently describes shell-led or service-led manifests as having the service as init. A 2026-04-28 12:48 UTC docs pass reconciled the current default system.cue path as standalone-init-owned. As of 2026-07-17 the primary focused shell-led manifests (system-smoke.cue, system-shell.cue, system-login.cue, system-login-setup.cue) are themselves migrated to init-owned graphs. As of 2026-07-27 the deferred shell-led proofs (system-shell-uptime*, system-shell-fs*, system-manual-smoke.cue) are migrated too. Gate B remains open until the loader/manifest validation rule lands (init-mandate-loader-validation-rule) and a final re-grep confirms no stale default-boot wording remains.

Gate C: Test split

  • Migrate the five self-contained SSH focused proofs to test-ssh-* (2026-07-27 08:49 UTC), preserving their manifests, ISO names, harness locations, and positive transcript assertions while removing the known preseeded false positive from public-key leak guards. Representative remaining families are named above; the complete closure inventory must be derived from the current Makefile.

  • Migrate the six memory and IPC capability proofs to test-* (2026-07-27 11:13 UTC), preserving their manifests, ISO names, harness locations, timeouts, transcript assertions, SMP configuration, and feature overrides. The remaining Gate C families are named above.

  • Migrate the six RAM-backed storage capability service proofs to test-* (2026-07-27 14:58 UTC), preserving their manifests, ISO names, harness locations, timeouts, and transcript assertions. The remaining Gate C families are named above.

  • Migrate the sixteen WASI and wasm-host language/runtime proofs to test-* (2026-07-27 17:34 UTC), preserving their manifests, ISO names, harness locations, timeouts, cargo feature overrides, and transcript assertions. The already-migrated test-wasi-9p-* proofs remain unchanged. The remaining Gate C families are named above.

  • Migrate the six run-scheduler-* CPU-isolation, SQPOLL, and AutoNoHz proofs to test-scheduler-* (2026-07-27 20:14 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, -smp 4 settings, cargo feature overrides, and transcript assertions. The remaining Gate C families are named above.

  • Migrate the six self-contained libcapos and libcapos-posix C-substrate proofs to test-c-* (2026-07-27 23:09 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, cargo feature overrides, and transcript assertions. The corrected evidence above records the subsequent green test-c-hello rerun and closes six-proof acceptance. The remaining Gate C families are named above.

  • Migrate the three crypto key-custody proofs to test-crypto-* (2026-07-28 03:13 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, cargo feature overrides, and transcript assertions. Independent artifact-level reruns passed all three harnesses against the branch-built ISOs after the initial intermittent pre-UART timeouts, as reconciled above at 2026-07-28 16:51 UTC.

  • Migrate the seven disk-backed storage and filesystem proofs to test-* (2026-07-28 09:51 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, multi-pass disk sequencing, forced-poweroff windows, and transcript assertions; rename the combined FAT32 timestamp/provenance aggregator to test-* as well (evidence corrected 2026-07-28 10:11 UTC). The remaining Gate C families are named above.

  • Migrate the eight installable-system proofs to test-installable-* (2026-07-28 10:35 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, multi-pass disk sequencing, and transcript assertions (evidence completed 2026-07-28 11:42 UTC). Post-migration verification executed all eight renamed recipes; all exited 0 with their harness assertions passing. The remaining Gate C families are named above.

  • Migrate the seven block-device, record-store, and durable-coordinator proofs to test-* (2026-07-28 14:49 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, multi-pass disk sequencing, forced-poweroff windows, and transcript assertions. Post-migration verification executed all seven renamed recipes; all exited 0 with their harness assertions passing. The remaining Gate C families are named above.

  • Migrate the six boot-source proofs to test-* (2026-07-28 20:38 UTC), preserving their manifest sources, manifest bins, ISO names, ISO_BOOT_BINS, harness locations, timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions. run-smoke and run-default-boot remain unchanged and are explicitly outside this wave. Per-recipe verification outcomes and the empty-UART reruns are recorded in the migrated-family entry above. The remaining Gate C families are named above.

  • Migrate the six hardware-audit and hardware-grant-cycle proofs to test-* (2026-07-29 00:15 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions. Post-migration verification executed all six renamed recipes; all exited 0 with their existing harness assertions passing. The migrated-family entry above records the two empty-UART reruns for test-hardware-audit.

  • Migrate the five endpoint queue/facet, two crash-disconnect, and four untrusted-exhaustion targets listed above to test-* (2026-07-29 01:52 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, CUE tags, aggregator sequencing, and transcript assertions. The migrated-family entry above records the successful per-recipe outcomes.

  • Migrate the three resource-limit proofs to test-* (2026-07-29 03:21 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions. Post-migration verification executed all three renamed recipes; all exited 0 with their existing harness assertions passing. The migrated-family entry above records the per-recipe outcomes.

  • Migrate the nine shell, login, and local-user proofs to test-* (completed 2026-07-29 10:07 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, granted/ungranted sequencing, and transcript assertions. The migrated-family entry above records each successful recipe and the launcher repair that cleared the original deferral.

  • Migrate the eight scheduler fairness, scale, and baseline proofs to test-* (completed 2026-07-29 11:44 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, timeouts, QEMU argument sets, cargo feature overrides, CPU/thread counts, and transcript assertions. The migrated-family entry above records every successful recipe and the status-124 empty-UART reruns.

  • Migrate the fourteen POSIX process, exec, descriptor, and stdio proofs to test-* (completed 2026-07-29 12:47 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, granted/ungranted sequencing, and transcript assertions. The migrated-family entry above records every successful recipe, the status-124 empty-UART rerun, and the terminal-input readiness handshake.

  • Migrate the twelve POSIX libc, networking, and shell proof targets to test-* (completed 2026-07-29 13:39 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, granted/ungranted sequencing, and transcript assertions. The migrated-family entry above records all eleven successful runnable recipes and the retained exit-2 DNS retirement diagnostic.

  • Migrate the twelve NVMe controller and queue bring-up proof targets to test-* (completed 2026-07-29 16:00 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, ladder order, and transcript assertions. The migrated-family entry above records all twelve passing recipes and the read-only-bind empty-UART control/rerun evidence.

  • Migrate the sixteen NVMe block-device, sync-to-flush, and filesystem-over-NVMe proofs to test-* (completed 2026-07-29 17:54 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, backing-file lifecycles, and transcript assertions. The migrated-family entry above records every per-recipe outcome, the predecessor-proof assertion repair, the two empty-UART attempts, and all three multi-boot durability checks.

  • Migrate the eight userspace NIC-driver ownership, queue, and interrupt proofs to test-* (completed 2026-07-29 22:12 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, and prior transcript coverage, with the descriptor-ring pinning refusal strengthened to an exact userspace-observed application-exception assertion. The migrated-family entry above records every per-recipe outcome and the two ownership negative controls.

  • Migrate the eleven virtio-net datapath, interrupt-delivery, and teardown proofs to test-* (completed 2026-07-29 23:35 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, MSI-X vector counts, queue sizes, cargo feature selection, and transcript assertions. The migrated-family entry above records every per-recipe outcome, the absence of empty-UART reruns, and both teardown-denial negative controls.

  • Migrate the ten userspace smoltcp network-stack proofs to test-* (completed 2026-07-30 00:13 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets and host-forwarding options, cargo feature overrides, paired driver/VM launch roles, and transcript assertions. The migrated-family entry above records every per-recipe outcome, the process-skeleton empty-UART rerun, and all three capability-refusal negative controls.

  • Migrate the nine ICMP and IPv6 datapath proofs to test-* (completed 2026-07-30 01:12 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets and socket-netdev variants, cargo feature overrides, paired driver/VM launch roles, and transcript assertions. The migrated-family entry above records every per-recipe outcome, the absence of empty-UART reruns, the distinct ICMPv4/ICMPv6 address-family inputs, and the distinct legacy/modern real-NIC launch shapes.

  • Migrate the nine network usability and diagnostics proofs to test-* (completed 2026-07-30 02:28 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, the shared transport manifest and ISO, and transcript assertions. The migrated-family entry above records every per-recipe outcome and non-empty kernel UART size; no target needed the startup-stall rerun.

  • Rename the twelve DDF hardware-grant, interrupt, and audit-service proofs to test-* (2026-07-30 07:09 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions. The migrated-family entry above records all twelve outcomes, including the original test-dmapool-grant assertion failure and its focused two-run repair. run-ddf-provider-consumer remains unchanged pending validation-gate registry reconciliation.

  • Restore test-dmapool-grant to green (2026-07-30). Application exceptions are intentionally silent in the kernel invalid-submission log, so the harness counts the marker emitted after the smoke validates the typed Failed exception in userspace. Two serialized runs passed.

  • Migrate the seven cloud DDF-grant, provider-cap-waiter, IOMMU abort-accounting, and NVMe synchronous-I/O proofs to test-* (2026-07-30 09:31 UTC), preserving their manifest sources, manifest bins, ISO names, harness locations, recipe timeouts, QEMU argument sets, cargo feature overrides, and transcript assertions. The migrated-family entry above records the passing IOMMU proof plus the six zero-byte PTY attempts and successful serialized no-PTY reruns.

  • Artifact-log prefix residual (audited 2026-07-30 09:31 UTC): the current Makefile, parsed with tools/run_target_inventory.py, has 37 migrated test-* recipes that still write 74 distinct UART artifacts under target/run-*-{kernel,terminal}.log. The complete inventory by migrated family is: - POSIX process, exec, descriptor, and stdio (14 recipes): test-posix-args-smoke, test-posix-cwd, test-posix-env-smoke, test-posix-execve-inherit-smoke, test-posix-fcntl, test-posix-fd-inherit-default, test-posix-identity, test-posix-isatty, test-posix-open-dir-fd, test-posix-open-smoke, test-posix-pipe-smoke, test-posix-spawn-smoke, test-posix-stdio-smoke, and test-posix-stdio-terminal-smoke. - POSIX libc, networking, and shell (10 recipes): test-posix-file-backing-smoke, test-posix-getaddrinfo, test-posix-printf, test-posix-read-builtin, test-posix-setjmp, test-posix-shell-smoke, test-posix-signal-time, test-posix-socket-poll-select, test-posix-strftime, and test-posix-test-builtin. - DDF hardware-grant, interrupt, and audit-service (9 recipes): test-devicemmio-grant, test-devicemmio-grant-exit, test-dmapool-grant, test-dmapool-grant-exit, test-interrupt-grant, test-interrupt-grant-x2apic, test-ddf-interrupt-stale-notification, test-ddf-audit-reader-smoke, and test-ddf-audit-service-smoke. The keyed-signature and runtime- admission targets alias the audit-service recipe and therefore reuse its two artifacts; the persist-reboot proof uses temporary files. - Cloud DDF grants and provider cap waiter (4 recipes): test-cloud-devicemmio-grant, test-cloud-dmapool-grant, test-cloud-interrupt-grant, and test-cloud-provider-cap-waiter. For every listed recipe test-<suffix>, the two paths are exactly target/run-<suffix>-kernel.log and target/run-<suffix>-terminal.log. No listed path is shared by two recipes, and no other current test-* recipe carries a run--prefixed artifact path.

    Rename these artifacts together in one dedicated follow-up after Gate C
target migration closes, not piecemeal in the remaining migration waves.
That isolates the coordinated `Makefile` and harness-argument rewrite
from active target renames and removes the misleading prefix atomically.
Prior per-recipe evidence above remains citable: those records name the
migrated `test-*` recipes and outcomes, while this residual records the
exact historical `run-*` path mapping. The follow-up changes future
artifact paths only and must not rewrite the historical evidence entries.

  • Move every scripted input driver, transcript assertion, timeout wrapper, harness invocation, and log grep currently embedded in a run-* recipe into a new test-* recipe. The run-* side, where retained, becomes a one-line qemu-system-x86_64 ... $(QEMU_COMMON) $$serial_args invocation against the same ISO.

  • Keep tools/qemu-*-smoke.sh, tools/qemu-*-harness.sh, and the ringtap viewer assertion out of run-* recipes. They are acceptable inside test-* recipes or as standalone host scripts.

  • Update CI hooks, developer docs, and loopyard task checkpoints that reference make run-<x> for verification to call make test-<x> instead. Audit the migrated review-finding task records, the REVIEW_FINDINGS.md tombstone history, and the recent changelog updates so historical entries stay accurate while new gates use the renamed targets.

Gate D: Default-run feature integration

The authoritative default-run integration checklist is the CLAUDE.md Stage Implementation Workflow. This backlog records only the backfill status.

  • Define the milestone integration checklist (2026-07-27 06:46 UTC).
  • Resolve the already-shipped milestone backfill (2026-07-27 07:02 UTC). Local-user setup and terminal-session are present in the default MOTD, with rendering asserted by make run-default-boot. The former Telnet and SSH gateway terminal-host paths are retired with the kernel socket owner, so neither is a backfill candidate. The future SSH Shell Gateway successor remains governed by the checklist and milestone checkpoint below.
  • Add the authoritative checklist to the CLAUDE.md Stage Implementation Workflow (2026-07-27 06:46 UTC).

Interaction With Paused SSH Shell Gateway Milestone

Loopyard currently pauses the SSH Shell Gateway behind Service Object Identity Migration. When SSH work resumes, it will still have a visible goal of default-boot SSH shell access plus focused make test-ssh-* proofs. Without an explicit checkpoint, that milestone can land more non-compliant proof recipes before this backlog is applied.

  • Before the SSH Shell Gateway milestone closes, add Gate A’s naming decision and Gate C’s test split as a milestone-level prerequisite: focused proofs use test-ssh-*, host harnesses live under tools/, and user-visible SSH access is integrated into make run under Gate D rather than left as a separate run-ssh-* recipe. Record the requirement in the SSH milestone checkpoint or block its closeout.

Sequencing

Gate A is purely policy and naming and unblocks the others. Gate B (init mandate) and Gate C (test split) can proceed in parallel on separate branches per affected manifest area, because they touch different files: B rewrites system-*.cue and may add services to init/src/main.rs, while C touches Makefile and the tools/qemu-* harnesses. Gate D follows once the test split lands so MOTD updates land alongside system.cue changes without competing with make run’s recipe.

Out Of Scope

  • Renaming or relocating tools/qemu-*-smoke.sh and tools/qemu-*-harness.sh scripts. They stay where they are; only their callers change.
  • Producing a new test runner that aggregates all test-* targets. That is a separate CI ergonomics task.
  • Reworking the focused-proof transcript content. The intent is to preserve current proof coverage, not extend it.