[minatoaquaMK2]

Why

Related to #300. Let a tenant keep its data disk when a claim is released or replaced with a new template.
This adds the node-local managed-volume part of that plan on top of #339.

What changed

• Add tenant-scoped sparse create, list, detail, and identity-conditional delete, with Go and Python SDK methods.
• Attach managed volumes at claim time, including to warm VMs, and persist writer ownership through daemon restarts and uncertain teardown.
• Recover interrupted removal and reject storage layouts that overlap VM cleanup directories.

Scope

• Covers node-local management, tenant isolation, single-writer admission, and data reuse across templates.
• Leaves online growth, volume-aware node placement, and the requested quiesce/capture/restore lifecycle for follow-up. Attached volumes still block capture and archive policy.
• Defers archive export, live changes to managed attachments, and Kubernetes integration. This PR does not complete Per-owner persistent volumes managed at runtime: attach to warm claims, single writer, survive hibernate and image upgrades #300.

Blast Radius

Managed storage is opt-in and requires a private persistent directory. Enabling it requires explicit management credentials for volume discovery.
Mixed catalog and managed claims use durable admission and teardown. Uncertain VM removal keeps the volume busy until recovery confirms removal.

Verification

• With Go 1.27.1, all five Go modules passed race tests and Linux/Darwin lint. The Darwin daemon build passed. The Python SDK previously passed 279 tests, Ruff, and strict mypy. Service-dependent skips are listed in the verification comment.
• The clean PR head passed 15 real-service/VM cases and extra tenant-attachment and capture-refusal checks. Guest UUID and 4 MiB payload hash matched after normal ext4 unmount, read-only fsck, and remount. Owned resources were empty after cleanup.
• Native device-number JSON boundary tests and bounded formal checks passed. Model and actual-code falsifiers detected the intended exclusion, binding, and mode failures. Verification covers normal remount and the stated model assumptions; host reboot and power loss remain untested.

Scope and original case matrix. CI repair and current-head verification. Bounded formal verification.

[minatoaquaMK2]

Issue #300 scope and local verification

This is a phase-one proposal. It does not close #300 or implement the capture sequence in the maintainer's update. The later status comment is the remaining-scope checklist. #339 already supplied live read-only catalog updates. This PR adds managed-volume integration, not that earlier API.

Plan coverage

Requested capability	This PR	Direct evidence or remaining work
Runtime tenant-owned create, list, inspect, delete	Implemented for one node	MV-01 through MV-05. Both SDKs have formal request/error tests. A 20 GiB sparse raw backing starts unformatted. Identical creation returns the original ID. Reflink support is not probed or used.
Warm claim-time rw attachment and attach-only mode	Implemented	MV-06 and MV-07. The VM came from the existing warm pool and the warm-claim counter increased. First format is explicit.
One writer and holder-naming 409	Implemented	MV-07. A second writer and held-volume delete return 409. MV-08 retains exclusion after daemon SIGKILL with both sync_claims settings. MV-10/MV-14 keep ownership until controlled VM removal is confirmed.
Release preserves data and another template reuses it	Implemented	MV-09. Template B used a new VM and read the same payload and filesystem UUID.
Tenant isolation	Implemented	MV-03 plus the extra real-runtime check below. t2 can attach its own disk, but cannot see or attach t1's disk.
Hibernate/snapshot and wake	Not implemented	No guest quiesce/unmount/detach/capture or restore/reattach/remount sequence. No hibernated writer-ownership lifecycle. Requests with an attached disk still return 409.
Online growth	Not implemented	No grow API or guest filesystem-growth flow.
Placement by volume in a mesh	Not implemented	Resources expose their local node, but managed owner-node routing and unavailable-owner handling are deferred. Existing catalog redirects do not establish managed placement.
Archive with attached data	Refusal only	Setting archive policy on the held claim returns 409. Disk export and restore remain deferred.
Later S3 block device	Not implemented	The issue explicitly defers this. Backings here are node-local raw files.

Live managed attach/detach and Kubernetes lifecycle/status integration are also outside this PR. A managed claim can still use #339 to change its mounted read-only catalog entries.

Exact artifact

• PR source revision b5bc525f0ce99c31ced50452c8a0f480488aef5e. Its Git tree is cdca8478fa1e3abe014c95947d6c35a5d6656d94, identical to the previously reviewed source. The PR contains one new commit with 38 source, formal-test, and product-documentation files. Historical audit commits are excluded.
• Binary SHA-256 9442e040699a6832a55171f0d3fd33c1bd1e3aaf8f896ff265337a778338ff75. Go build metadata reports the PR revision and vcs.modified=false.
• Runtime attempt 38e5886d562e508a34e7fbadb834e496. All 15 case files and their aggregate have the same source, binary, SDK, tool, and attempt binding.
• External driver SHA-256 943cac29a0f17ae180bbe55f4289190729479e350bda73a59cfaf5154222b770. The driver and raw audit files remain outside Git. This digest identifies the external tool, not a source commit.
• Linux amd64, Go 1.27.2, Cocoon 0.7.3, Cloud Hypervisor v54, and official guest layers. The outer filesystem is an exclusively owned 12 GiB sparse ext4 image on persistent host storage.

Observed runtime results

Case	Observation
MV-01	Logical capacity 21474836480 bytes, initially 0 backing bytes allocated, owner t1.
MV-02	Same request returns the same ID. Different size/owner are refused without replacing the backing.
MV-03	Owner/root can discover the resource. Foreign management requests match unknown-volume 404 responses. Owner spoofing is refused.
MV-04	Missing/wrong delete preconditions are refused. Replay of an old deleted identity cannot delete the replacement. Deletion survives daemon restart.
MV-05	Four create statuses [200, 201, 200, 200] yield one ID. Create/delete statuses [201, 204]. Delete/claim statuses [204, 404]. These are one observed schedule, not every possible race branch.
MV-06	Explicit first format and 4194304-byte guest payload. Attach-only remains unmounted across catalog live changes and daemon restart.
MV-07	Warm-pool VM reused, warm counter 0.0 to 1.0. Payload/UUID match. Second writer and held delete return 409 naming the holder.
MV-08	Fresh claim in each sync_claims=false/true run. SIGKILL sandboxd, restart, same VMM PID/start generation, same data/UUID, writer conflict retained.
MV-09	Old VM removed. New VM from template B reads the same payload/UUID.
MV-10	Release during a post-effect catalog attachment keeps managed and catalog admission blocked until the old VM is removed. Reuse then succeeds.
MV-11	No holders before the outer-storage round trip. Resource ID and backing inode/device/size recorded.
MV-12	Normal unmount, mount absence, flush, e2fsck -f -n exit0, remount. Resource/backing identity, outer UUID, guest UUID and payload hash remain unchanged.
MV-13	A stopped unclaimed VM record is collected at startup while a managed resource already exists. This is not a spontaneous claimed-VM death test.
MV-14	Seeded durable quarantine marker and exact-VM Remove refusal. Writer/delete stay blocked until retry removes the original VMM. An ordinary failed claim remains owned until explicit release.
MV-15	Eight unsafe-layout startup refusals, including readers/goldens aliases into managed disks. Refusal precedes daemon-created files and preserves preexisting backing markers.

The same guest filesystem UUID was 420cb23a-bd39-4496-8561-742cb4968a48. The 4 MiB payload SHA-256 before and after template replacement, daemon crashes, and outer remount was c64559efb28350cc05a2c55c68fd34548a556d1df6104e00f82c2005122e6c54.

The additional acceptance check used real HTTP requests and VMs on the same PR binary. A t2 claim attached t2's own managed disk with status200. A t2 claim naming t1's disk and one naming a valid unknown disk both returned status404 with {"error":"unknown volume","code":"volume_not_found"}. The control claim and resource were removed. Hibernate, checkpoint, and renew with on_expire=archive each returned409 for a t1 claim with its disk attached. The guest remained usable and its payload hash stayed unchanged.

Commands and formal checks

The following source checks passed on the candidate tree, which is byte-identical to the committed PR tree. Python commands used an environment with pytest, Ruff, and mypy installed. On root, the Go run dropped DAC override/read-search capabilities so permission checks remained meaningful. The equivalent commands below use illustrative external output and cache paths.

setpriv --bounding-set=-dac_override,-dac_read_search -- sh -c '
for module in protocol/wire sandboxd sdk/go e2e mcp; do
	(cd "$module" && GOWORK=off go test -mod=readonly -race -count=1 ./...) || exit 1
done
'
(cd sdk/python && PYTHONDONTWRITEBYTECODE=1 python -B -m pytest -p no:cacheprovider -q)
ruff check --no-cache sdk/python
ruff format --check --no-cache sdk/python
(cd sdk/python && python -B -m mypy --cache-dir /tmp/sandbox-pr-mypy-cache)
(cd sandboxd && GOWORK=off GOOS=darwin go build -mod=readonly -o /tmp/sandboxd-pr-darwin .)

All five Go-module runs exited0. Python reported279 passed. Ruff, strict mypy, changed-Go-file formatting, and the Darwin build passed. The run did not configure PostgreSQL, an external S3 endpoint, Caddy, so their opt-in tests skipped. The separate 15-case VM run above is the real-VM local qualification, not a claim that those skipped tests ran.

Pinned golangci-lint2.13.2 exited1 in unchanged protocol/wire imports because its decoder supports export-data version4 while this Go1.27 toolchain produces version5. No Go lint pass is claimed. CI results remain separate from these local results.

Cleanup and limits

Cleanup confirmed zero owned claims, managed resources, holds, backing files, and VMs. Owned services stopped. The mount and loop were removed. All64 case-artifact file hashes matched before/after cleanup and after export; the complete retained export has71 matching regular files and preserves two fixture symlinks. The original checkout's716 file contents/permissions and three preexisting process generations were unchanged.

No tools, audit records, logs, runtime tokens, or evidence directories are in this PR. Raw ownership/fixture files remain private because they contain credentials.

This run proves a normal filesystem remount, not host reboot or abrupt power loss. MV-14 seeds quarantine state and refuses one exact runtime removal command; it does not inject a real firewall or failing fsync. Source tests cover persistence-failure boundaries with fake engines. Arbitrary external destruction of a claimed VM and every concurrent scheduling branch were not independently qualified. Host path guards assume trusted directories and do not defeat bind-mount aliases or concurrent malicious pathname swaps.

One extra-check attempt initially used an invalid unknown-volume name and received the expected validation400. The test control was shortened to a valid name before the successful 404 comparison. No product code changed, and this failed control was not counted as passing proof.

[minatoaquaMK2]

CI repair and requalification

The first sandboxd CI run failed on introduced lint findings, not infrastructure. CI uses Go 1.27.1, which can run the pinned golangci-lint 2.13.2. My earlier local Go 1.27.2 decoder failure had prevented that check from completing. Matching the CI toolchain reproduced 58 findings; later modules exposed 9 SDK findings and 2 e2e findings.

Commit a6ed90d62b1860e05adac0cde28b6f36381bb7c7 fixes those findings. Registry validation now delegates by volume, holder, and reference while preserving predicates, phase order, errors, and shared admission counts. Admission and pre-attach checks keep their locks and remain before device effects. UID comparisons widen safely. Process reads keep the distinction between missing boot metadata and a missing PID. Native device-number conversion preserves the existing numeric JSON on both Linux and Darwin, including signed Darwin values. The new six-case test covers persisted numeric boundaries. The rest is error cleanup, binding-preserving variable renames, guard flattening, formatting, and SDK literal/parameter cleanup.

Local checks

GOTOOLCHAIN=go1.27.1 GOWORK=off make go-lint

All five modules passed Linux and Darwin lint, ten runs with 0 issues, using the existing repository configuration. The run also passed each module's formatter check. A local SA4023 analyzer panic disappeared with a fresh isolated analysis cache on identical source, and the complete matrix then passed.

All five Go modules passed go test -mod=readonly -race -count=1 ./... with Go 1.27.1. The root run dropped DAC override/read-search capabilities for meaningful permission checks. PostgreSQL/S3/Caddy opt-in tests still depend on their configured services. The Darwin daemon build also passed. Source/no-comments review by a nonauthor found no blocker or weakened validation/assertion.

Real VM proof on the repaired head

• Clean binary revision a6ed90d62b1860e05adac0cde28b6f36381bb7c7, vcs.modified=false, built with Go 1.27.1. SHA-256 609138ddfefa717df3df3520b72d4ec2f7611ed6a5a6606f5847a99b65df30c1.
• All 15 cases from the earlier matrix passed again in attempt 222268d3cac2cf14addf19b23980deed, with one source/binary/SDK/driver binding. External driver SHA-256 943cac29a0f17ae180bbe55f4289190729479e350bda73a59cfaf5154222b770.
• The additional real-HTTP checks passed again. t2 attaches its own disk with status 200, foreign and valid-unknown names return identical 404 responses, and attached-volume hibernate/checkpoint/archive-policy requests return 409 while the guest remains usable.
• Normal outer ext4 unmount, absence observation, flush, read-only fsck, remount, and guest readback passed. Guest filesystem UUID 1aab7624-cd76-4beb-a334-a17471d222ed and 4 MiB payload SHA-256 6d7463e13308d75906f919b7e4e91bfb4294168e9f69666cff9a616d97d02209 matched. Resource and backing identity also matched.
• Cleanup reached zero owned claims, managed resources, holds, VMs, and backing files. The owned mount and loop were removed. All 64 artifact file hashes survived cleanup/export; all 71 retained regular files and 2 fixture symlinks matched after detach. The original checkout's 716 file contents/permissions and 3 preexisting process generations remained unchanged.

The #300 scope is unchanged. Hibernate/wake, online grow, managed node placement, archive export, live managed attachment changes, and Kubernetes integration remain follow-ups. This proof covers normal remount, not host reboot or power loss. Quarantine testing still uses seeded durable state and an exact Remove refusal, not real firewall/fsync failure. Tools, audit records, private runtime configs, and logs remain outside Git.

GitHub CI is green for this exact repaired head. sandboxd and Python both passed. The sandboxd lint, Go tests, PostgreSQL meta-store tests, and Caddy TLS step all completed successfully. The watcher reports READY with merge state CLEAN. The PR remains open for review.

[minatoaquaMK2]

Bounded formal verification on the current head

Qualified product revision a6ed90d62b1860e05adac0cde28b6f36381bb7c7. This follow-up changes the external verification model and harness only. No additional product-code change was needed after the review, and no tool, audit or log file was added to this PR.

The TLA+/TLC model checks four separate obligations for one fixed managed backing:

• Attached VM generations cannot have conflicting effective device modes.
• A new hold cannot conflict with a live generation that has, or may still acquire, device access.
• A live attached or in-flight generation must already have a durable VM-generation binding.
• Effective device modes must match admitted modes.

The startup gate uses observable inventory rather than knowledge of every physically live VM. Requested and effective modes are separate state. Registry publication, sticky write faults, process death, inventory absence, uncertain attach effects, retirement and daemon restart are separate transitions.

Results

Check	Observed result
Two-generation model, every RO/RW assignment	24,426 reachable states checked, no invariant violation.
Three-generation model, every RO/RW assignment	1,460,910 reachable states checked, no invariant violation.
Five broken-model configurations	Each failed its intended invariant, including pre-bind attachment followed by inventory loss and restart.
Actual Go manager probes, race enabled, Go 1.27.1	Ten roots and 32 subtests passed, producing 42 named results including parent results. The complete set passed again after restoration.
Four actual-source mutations in isolated exports	Removing process-death proof, moving bind after attach, skipping only bind commit, and forcing writable device mode all failed at their required test leaves and messages. All four mutations were restored byte-for-byte.
Verification-entry controls	18 built-in controls, seven actual CLI refusal cases, and 23 additional independent controls passed. Optimized Python, inherited GOFLAGS, missing coverage, wrong failure attribution and tool errors cannot qualify as success. Mutation cleanup also runs on timeout or interruption.

The new Go probes read registry.json directly at the DiskAttach boundary, check exclusion after a recorded device effect returns an error with ineffective removal, and compare two overlapping RO requests with applied volumes, durable references and actual VolumeSpec.RW arguments. These probes use controlled fake engines; this follow-up adds no new physical-VM run.

Separate nonauthor reviewers checked model/source correspondence, the Go probes and the entry. An independent cold invocation completed all 14 planned checks on the same frozen artifacts. The model and harness themselves are retained outside Git, so these are local qualification results rather than a new repository CI gate.

Artifact SHA-256 values:

• Model: c337130937feb487d2d56cfacc80aa128051e9375afdb90d50b876f9c9f62924.
• Entry: a0c67563bbe0ba044ba2edfdcf187f15e1b1d0709077f3f41d5b9b35e89c17a8.
• Boundary probes: e0662b034ae617379f1676d08f3f49e3f1865f1056816af22263bd6c0474e6f2.
• Independent cold-run receipt: 6bee2cd37359019dd5af823e53bed3b7483a927f6d8fb8ea28cd935d0d079d4f.

Limits

This is bounded model checking plus actual-code falsification, not a machine-checked refinement proof of Go. It assumes one registry writer, sound process-generation proof, complete old-or-new snapshots under daemon crashes, and trusted local tools. Claimant lifetimes are not recycled. Arbitrary scale, liveness, delete/recreate identity, multiple backings and aliases, catalog live changes, warm-specific branches, runtime/hypervisor internals, host reboot and power loss are not established by this formal run. The earlier physical-VM/remount evidence remains separate, and the partial #300 scope is unchanged.

[minatoaquaMK2]

Closing in favor of #369, which carries the current version: it adds hibernate and online growth, and fixes the gaps we found by re-checking the edge cases from #339.