[roodboi]

Summary

Linear: HACK-1195. This implements the bounded October 2 follow-up: tell a verified retained-disk restart apart from a fresh disk allocation.

Development admission now treats an exactly clean stopped pool like a verified running pool for the disk budget. A restart reuses the pool's retained 32 GiB storage disk and 10 GiB overlay. So admission charges only the 16 GiB host reserve (disk_budget_basis: verified-stopped-owned-pool-host-reserve), not the 58 GiB fresh-allocation floor. This is the October 2 M3 Event Agent case, where a start with 58,010,112,000 free bytes was refused even though it would allocate nothing new.

This revision fixes the defects the verifier found at ea0d434b.

Final behavior

"Clean" is a marker that only down can complete

• The owner receipt has a new optional field, clean_stop. It holds {guest_boot_id, daemon_pid, daemon_start}.
• Only down writes it, through finish_quiesced_stop. That write happens in the same receipt write as its stopped phase, after three things are proven: the guest acknowledged flush and shutdown of a quiesced engine, the provider is gone, and the provider released the VM lock, disk handles and sockets.
• phase() clears the marker on every phase other than stopped, and Owner::begin_boot clears it on every new boot.
• A start that is refused before boot still rewrites the phase to stopped (lifecycle.rs pre-boot refusal). That rewrite now:
  • keeps a clean stop clean, because nothing has booted since down;
  • can never turn an unclean stop into a clean one.
• The relabelling path is therefore closed. That path was: down writes quiescence.json, then hits stop_uncertain; recover writes recovered-unclean; a later start is refused before boot and writes stopped. The stopped-before-engine rewrite is closed the same way.
• stopped() requires a marker that matches the receipt's boot and engine identity, as well as the existing matching quiescence receipt.
• A pool stopped by an earlier candidate has no marker. It keeps the fresh budget until its next clean down.

Two layers of checks, and no provider lock outside the lease

• Receipt checks run around every sample, including the read-only runtime probe. They are read-only, take no lock and run no host tool. They require:
  • profile Development and phase exactly stopped;
  • the clean-stop marker and a matching quiescence receipt;
  • no owner.pending;
  • created, a rootfs pin, both disk identities and the declared 32/10 GiB sizes;
  • the machine-name file;
  • the recorded executable and uid;
  • a dead recorded PID. A live, reused or unobservable PID refuses.
• Release checks (released) run only while the startup lease is held. They need a &state::Lock, whose path is verified. They require a free VM lock (flock), no open disk handle (lsof), no owned listener, and an unchanged audited provider configuration (config_audit::verify, which is new at selection). They run at three points: once after the lease is acquired, again before any restart effect (restart_only), and in the final recheck before machine start.
• So the VM-lock flock and lsof no longer run unlocked in select(), in samples taken before the lease, or in runtime development probe. They cannot contend with another operation that is handing the VM lock to a provider.
• The short-HOME alias is checked on every Owner::load. The rootfs content is checked against its pin by prepare_rootfs before boot. Both are unchanged.

The boot gate is typed

• machine create now goes through create_machine(.., FreshCreate). Only admission_pool::fresh_create issues a FreshCreate, and it refuses whenever a reserve selection exists.
• machine start now goes through start_machine(.., StartPermit). A StartPermit comes only from:
  1. admission_pool::admit_boot, the pre-boot sample on the same basis as qualification, with the selection rechecked around the sample and swapouts compared with the baseline;
  2. followed by BootAdmission::release, the final leased recheck.
• Because of this, removing the final recheck or reverting the pre-boot probe to the fresh basis now happens inside admission_pool, where tests cover it.
• A pre-boot refusal still records stopped and returns admission_rejected, as before.

Diagnostics

• Admission has a new optional field, retained_reserve_refusal. It appears on a fresh-budget sample when a created stopped pool failed the receipt checks, and holds the closed code: retained_reserve_{foreign,active,dirty,stale}_owner.
• The field is omitted when it is empty, so existing reports are byte-compatible.
• A never-created owner reports nothing, because there are no retained disks to explain.
• A selected pool that fails a later check refuses the start with its closed code.

Unchanged

• Fresh Development still requires 58 GiB. Research keeps its 100 GiB floor. The running basis is unchanged.
• The pressure, thermal, swapout and memory-headroom predicates are untouched.

Docs

• packages/runtime-core/README.md now describes the marker, the two check layers, the typed gates and the diagnostic field.
• docs/guides/native-candidate.md no longer says Development always reserves 58 GiB before startup. It now describes the running and stopped reserve bases.

Validation (local, macOS arm64, RUSTUP_TOOLCHAIN=1.97.1)

• bun run check:local (rustfmt check plus clippy --all-targets -D warnings): exit 0.
• bun run test:local: exit 0. The lib suite ran 1003 passed, 0 failed and 58 ignored, and every integration target passed.
• Focused cargo test --lib admission_pool: 20 passed, three runs in a row. The wider admission filter: 70 passed, 2 ignored. On a heavily loaded shared host, a run of that filter can time out inside lsof (see Remaining gaps).
• bun test tests/integration-ownership.test.ts tests/cli-spawn-env-isolation.test.ts: 16 pass.
• bun run --cwd packages/cli typecheck: exit 0. bun run --cwd packages/cli check: 0 errors and 34 existing warnings. No TS files changed.
• bun run privacy:check: ok.
• The all-features clippy run could not build here, because native-stream-relay requires Zig 0.15.2. No changed code depends on a feature.
• The tests use private temp pools with sparse disks, a sleeping fake provider, a /private/tmp alias and a fixture smolvm.db. They make no Docker, OrbStack, real HOME, keychain or sudo calls. Read-only lsof is the only host tool they run. Tests that run lsof are serialized within the module.

Negative controls (admission_pool/tests.rs)

• Relabelling:
  • A later boot's down quiesces, recover writes recovered-unclean, then a pre-boot refusal rewrites the phase to stopped: refused as Dirty.
  • The same rewrite after recovered-unclean or stopped-before-engine on the clean boot itself: refused as Dirty.
  • The marker is missing, or names another boot, daemon pid or daemon start: refused as Dirty.
  • stopped recorded by finish_stopped instead of down's finish_quiesced_stop: refused as Dirty.
  • finish_quiesced_stop while the VM lock is held writes nothing.
• Positive:
  • A pre-boot refusal after a clean down keeps the pool eligible.
  • finish_quiesced_stop records the marker, and the pool then qualifies.
• Foreign: machine name, executable or uid differs (receipt checks); the VM lock is hard-linked, the provider record carries another owner label, or the provider database is missing (leased checks).
• Active: the recorded PID is alive (receipt checks); the VM lock is held, a disk handle is open, or agent.sock is listening (leased checks).
• Dirty and stale: the phase list, the quiescence receipt mismatches, owner.pending is present, and missing fields, replaced, missing or mis-sized disks, or a missing VM lock. These are unchanged from the previous revision.
• Receipt checks take no lock: selection, reverification and a probe sample all succeed while the VM lock is held elsewhere.
• Boot gate:
  • A stopped selection is sampled with OwnedPool::Stopped, no selection with Fresh, and a live selection with Running.
  • A refused sample, or swapouts that changed or are missing, gives BootGate::Refused(admission_rejected).
  • Receipt drift during the sample refuses with retained_reserve_dirty_owner.
  • A selection that drifted before the sample is never sampled.
• Start permit: after admission, a newly held VM lock, an open disk handle or a pending owner update makes release refuse.
• Restart and create:
  • restart_only refuses a running selection, a held owner that differs from the selection, and a held VM lock.
  • fresh_create refuses any selection.
  • With no selection, both pass.
• Diagnostics: a created dirty pool reports retained_reserve_dirty_owner in the sample and its JSON. A never-created pool reports nothing.

Mutation proof

I applied each of 18 mutations alone and ran cargo test --lib admission_pool. 17 were killed:

• stopped() ignores the marker;
• phase() keeps the marker on an unclean write;
• begin_boot keeps the marker;
• down never records the marker;
• release skips the final recheck (the verifier's mutation B);
• the boot gate samples the fresh basis (mutation C, now inside admit_boot);
• the stopped basis maps to fresh;
• restart_only ignores the held owner;
• restart_only uses lock-free checks instead of leased ones;
• fresh_create allows a selection;
• reverify_leased skips the release checks;
• released skips the config audit;
• a fresh sample drops the refusal code;
• an uncreated owner reports a refusal;
• the post-sample recheck is removed;
• the pre-sample recheck is removed;
• the receipt checks take the VM lock.

The survivor is removing !owner.created from restart_only. That is an equivalent mutant, because restart_only also requires the held owner to equal the selected owner, and stopped() requires created. I kept the check as defense in depth.

Under host load, some kills also failed unrelated tests because of the lsof bound. The listed tests fail deterministically for their mutation.

Remaining gaps

• No native proof. Still needed: an ordinary retained restart with measured free space between 16 and 58 GiB, the same machine and disks, retained-marker readback, and negative controls at each recheck window on a real pool. This needs a prepared macOS provider slot.
• start_pool is still not driven end to end in a test, because it needs artifacts and a provider. The typed FreshCreate and StartPermit mean that skipping the admission-pool gates would now require deliberately bypassing create_machine or start_machine, not a one-line mutation. Removing the restart_only call in start_pool is not detected by a test; fresh_create and the leased release still guard create and boot.
• Receipt compatibility. Owner uses deny_unknown_fields. An earlier candidate build cannot load a receipt that carries clean_stop until a new boot clears it. This matches the earlier previous_guest_boot_id and reclamation additions.
• lsof bound. The release probe keeps its 5 s lsof bound. On a heavily loaded host the probe can time out. That correctly refuses as retained_reserve_active_owner, and it makes a selected start fail instead of falling back. It can also make lsof-based unit tests flaky under heavy parallel load.
• Unlocked disk reads. The receipt checks still open the disks to read their identities while no lock is held, just as the running basis already does. A concurrent down or recover lsof could briefly observe that read handle and report stop_uncertain. I have not observed this.
• Still open in HACK-1195: resource attribution and the matched v4/OrbStack CPU/memory/disk comparison.

Rework 2

Head before this round: c3ccabdd. New commits: da798965 (fix) and 82d3ffaa (docs).

Verifier defects

1. Linux dead-code lint at 6698f47b. Already fixed by c3ccabdd, which gates into_selection and refusal to cfg(all(test, target_os = "macos")). I checked the hosted run on c3ccabdd before this push: all 16 checks passed, including Candidate core (ubuntu-latest), Candidate core (macos-latest) and all four Config compiler jobs. The readiness claims in this body now refer to the heads named here, not to 6698f47b.
2. The 5 s lsof bound refused clean stopped restarts that the base branch admitted. Fixed in da798965.
   • Once the startup lease is held, the new admission_pool::settle replaces the old leased recheck. A stopped selection's receipt is rechecked first. Then, if every qualifying sample (including the lease recheck) also fits the unchanged 58 GiB fresh budget, the selection is dropped. Those samples are recorded on the fresh basis, and the start continues exactly as a start without a selection: no release checks, no lsof, a fresh pre-boot sample, and a StartPermit without the leased release.
   • Only a start whose free disk lies between the 16 GiB reserve and 58 GiB keeps the selection. Its release checks bound lsof at 30 s (RELEASE_HANDLE_WAIT) instead of 5 s. down, recover, the short-HOME and host-filesystem paths keep the 5 s bound (STOP_HANDLE_WAIT).
   • So a clean stopped pool with 58 GiB or more free restarts with no lsof scan, as it does on next. An lsof timeout can refuse only a start that next would also refuse (admission_rejected on the fresh budget). It now refuses with retained_reserve_active_owner instead.
   • A live selection is rechecked as before. Its leased recheck was already the plain receipt recheck.
   • 82d3ffaa adds a README note: runtime probe takes no lease and settles no basis, so it reports the reserve basis for any qualifying stopped pool. The start's admission.json records the basis that start actually used.

New tests and mutation proof

• admission::tests::only_an_admitted_development_sample_with_fresh_headroom_rebases_to_the_fresh_budget: the inclusive 58 GiB boundary, the October 2 value (58,010,112,000 bytes), unobserved disk, refused and explained samples, and Research.
• admission_pool::tests::a_start_with_fresh_headroom_drops_the_reserve_and_runs_no_release_check:
  • With the VM lock held, an all-fresh window settles without error and drops the selection. It rebases every sample, and the rest of the gate takes the fresh path.
  • A window with one sample below 58 GiB keeps the selection and is refused with retained_reserve_active_owner. Once the lock is released, the same window settles on the reserve basis.
  • A drifted receipt (owner.pending) is refused before any basis is settled, even when there is enough room for the fresh budget.
  • A live selection keeps its own basis.
• Each of these 11 mutations fails its test: settle always runs release checks; all becomes any; the receipt recheck is skipped; the selection is kept; samples are not rebased; the live branch is removed; fits_fresh_budget ignores admitted, reasons or profile; it compares against the reserve floor; rebase_fresh keeps the reserve basis.
• No test covers the 30 s value. lsof is a fixed host path, and no test injects a slow scan.

Gates on 82d3ffaa (macOS arm64)

• cargo +1.97.1 fmt --check passed, and cargo +1.97.1 clippy --all-targets -- -D warnings reported no warnings. A local Linux cross-clippy could not build ring (no cross C compiler), so hosted Candidate core (ubuntu-latest) is the Linux lint proof.
• Running cargo test --lib admission at load average 10 gave 72 passed and 0 failed.
• gitleaks over origin/next..HEAD found no leaks. CLI typecheck reported 0 errors, and CLI check reported 0 errors (34 existing warnings).
• Full bun run test did not pass on this host: 6,958 passed, 240 failed and 149 skipped, at load average 15–58. This PR changes no TS, JS or JSON (git diff --stat 3b530068 HEAD lists only .rs and .md files). The only test that reads the changed docs is tests/prerelease-plan.test.ts, and it passes (57/57); tests/env-command-matrix.test.ts also passes.
  • The failures began in tests/native-authored-project-start.test.ts. A timing failure there leaves "Startup fixture settlement unconfirmed; roots retained", and in the shared process its fixture home then leaks into later files.
  • I reran each failing file on its own, serially, with --timeout 60000. 41 of 48 passed.
  • Still failing on this loaded host: native-compose-down-command (13; the CLI was killed, exit 137), native-compose-file-command (3), native-compose-proxy-probe (2), native-authored-project-recovery (2), native-authored-process-incarnation (1), test-config-compiler (1), and native-authored-project-start (20; it cascades after its first timing failure).
  • The first failing test in native-authored-project-start passes when run alone.
  • The hosted macOS test job, which runs this same TS code, passed on c3ccabdd. I am reporting these as load-only flakes rather than masking them.
• Load-only flakes. At load average 30–58, lsof alone took 4.1–6.0 s on this host, which has about 2,200 processes. The full cargo test run had 6 failures, and a serial rerun of provider::lifecycle:: had 2. Every failure was provider_timeout_uncertain, and every failing test exercises the unchanged 5 s stop-path bound (short_home, host_filesystem, interrupted, and the two admission_pool tests that call finish_stopped or finish_quiesced_stop). None of them runs the code this round changed. Run alone, only_a_completed_quiesced_down_records_a_clean_stop passed; the others still failed whenever lsof took more than 5 s. In these runs, no admission test failed with retained_reserve_active_owner, the failure the verifier saw from the release-check bound.

Still open

• No native proof. No retained restart with free disk between 16 and 58 GiB has run on a real macOS provider. A run is also needed to show that a start with 58 GiB or more drops the reserve.
• start_pool is not run end to end in any test. Removing its settle or restart_only call would not fail a test.
• Receipt compatibility. An earlier build cannot load a receipt that carries clean_stop until a new boot clears it. This is the same deny_unknown_fields policy that applied to the earlier receipt fields.
• Stop-path lsof bound. down and recover keep the 5 s bound, unchanged from next. On a loaded host, down can return provider_timeout_uncertain. It then never records the clean-stop marker, so the next restart uses the fresh budget.
• Unlocked disk reads. The receipt checks still read disk identities without a lock. I have not observed a problem from this.
• Still open in HACK-1195: resource attribution and the matched v4/OrbStack comparison.

🤖 Generated with Claude Code