virtio-9p (modern PCI 9P transport)

This is a provenance map for the in-tree virtio-9p driver: it cites the specs, summarizes only the wire-format subset the code actually implements, and points into the implementation. It is not a re-spec. The driver reuses the modern split-ring transport seam introduced for virtio-net (virtio-net) and the single-request-queue bring-up shape of virtio-blk; this page covers only the 9p-specific parts.

Status: kernel fixture serving a host-directory export, read-only by default and writable only on explicit request. The driver, its PCI discovery, its DMA ledger, and the capability module above it are gated behind any(feature = "qemu", feature = "virtio_9p_host_fixture") – either the qemu feature that carries the whole QEMU device surface, or the composable virtio_9p_host_fixture feature that carries just this fixture into a not(qemu) build so the writable-9p path can co-boot with the Phase C userspace network stack (see the host-directory proposal “Composable Fixture Feature” section). kernel/src/virtio.rs compiles in both cases; a build with neither feature substitutes kernel/src/virtio_stub.rs (the typed-negative kernel-network facade, which virtio.rs also includes for its own not(qemu) builds). PCI discovery is diagnose_virtio_9p in kernel/src/pci.rs, reached from the QEMU diagnostics path under qemu and from the dedicated diagnose_virtio_9p_host_fixture startup route under virtio_9p_host_fixture without qemu; the latter build routes claim_pci_function + attach_dmapool_record_with_remapping through the minimal kernel/src/device_manager/virtio_9p_fixture_claim.rs rather than the qemu-only qemu_full Device Driver Foundation (DDF) ledger. What is implemented today is transport bring-up, the 9P2000.L session handshake, a bounded read subset, and a bounded write subset. Userspace reaches them through two distinct kernel grant sources serving two distinct capability types:

Which one a process gets is fixed by the manifest at spawn and cannot change afterwards. There is no rights flag and no method that turns a read-only cap into a writable one, so a read-only export is not upgradeable at runtime – the attenuation is structural, per the capability model. A build with neither qemu nor virtio_9p_host_fixture can obtain neither: it has no 9p cap module at all and resolves both sources to kernel source `<name>` requires the qemu feature (or the composable virtio_9p_host_fixture feature), failing the spawn closed. The fixture is dev/proof infrastructure and never a production authority; the intended use is dev-loop payload injection and artifact export, per the host-directory proposal, whose “Driver Boundary Decision” section records why this is a kernel-side fixture (Option A) rather than a userspace driver process.

The driver lives in the virtio-9p section of kernel/src/virtio.rs (Virtio9pDriver), and the protocol encoding/decoding is the transport-free client codec capos_lib::ninep (capos-lib/src/ninep.rs).

1. Spec basis

• Device: virtio 9P transport device, modern (virtio 1.x) PCI transport. PCI vendor 0x1af4; device 0x1049 (modern) / 0x1009 (transitional). IDs at kernel/src/pci.rs (VIRTIO_VENDOR_ID, VIRTIO_9P_MODERN_DEVICE_ID, VIRTIO_9P_TRANSITIONAL_DEVICE_ID; matched by PciDevice::is_virtio_9p). Exactly one function is bound, into the single VIRTIO_9P_DRIVER slot; a second discovered function is refused rather than silently rebinding.
• Authoritative specs:
  • Virtual I/O Device (VIRTIO) Version 1.2, OASIS Committee Specification 01 (2022-07-01). Source: https://docs.oasis-open.org/virtio/virtio/v1.2/virtio-v1.2.html. Relevant sections: 4.1 (virtio over PCI bus), 2.7 (split virtqueues), 5.7 (9P transport device).
  • 9P2000.L protocol, the Linux-flavoured 9P dialect. Source: https://github.com/chaos/diod/blob/master/protocol.md. The version string the driver negotiates is exactly 9P2000.L (capos_lib::ninep::VERSION).
• Reference: cross-checked against the QEMU 9p server (hw/9pfs/9p.c) for the session-establishment behavior, and the Linux 9pnet_virtio transport for the descriptor-chain shape.

2. Wire format (implemented subset)

• Transport discovery and negotiation: unchanged from the shared modern-PCI seam – vendor-specific capability walk, common/notify/ISR/device-config region selection, and the reset -> ACKNOWLEDGE -> DRIVER -> feature-negotiation -> FEATURES_OK -> DRIVER_OK handshake. See virtio-net §2 for the seam itself (kernel/src/virtio_transport.rs).
• Features: VIRTIO_F_VERSION_1 and VIRTIO_9P_F_MOUNT_TAG are both required and both selected; nothing else is accepted. A device that does not offer both fails bring-up closed (Ninep9pInitError::MissingRequiredFeatures).
• Device configuration: struct virtio_9p_config – a u16 tag length followed by that many mount-tag bytes. The driver maps exactly the length the transport capability advertises and validates the tag length against both VIRTIO_9P_MAX_TAG_LEN and the bytes actually present before reading the tag (Ninep9pInitError::MountTagOutOfRange).
• Queues: one request virtqueue (index 0), a split ring built by the shared Virtqueue::initialize. Size is clamped to the largest power of two not exceeding VIRTIO_9P_REQUEST_QUEUE_SIZE and the device maximum. Completion is polled (QueueInterruptPlan::polled); no MSI-X vector is programmed. Virtqueue::poll_used_within_ns enforces the five-second VIRTIO_9P_COMPLETION_BUDGET_NS as either an absolute calibrated-monotonic deadline or its tick-derived absolute-deadline equivalent. The latter polls elapsed counts from the current CPU’s periodic LAPIC timer while preserving the syscall context’s interrupt-disabled state; tick-derived clock mode keeps that local periodic timer active on BSPs and APs by disabling nohz. Before a calibrated clock or periodic LAPIC timer exists, early bring-up instead uses VIRTIO_9P_COMPLETION_FALLBACK_SPIN_LIMIT as a fail-closed backstop. The driver reports the selected mode and attributes expiry to the monotonic deadline, tick deadline, or spin backstop.
• Descriptor chain: each 9p exchange is a two-descriptor chain – a device-readable request segment followed by a device-writable reply segment, each backed by its own dedicated DMA page so the two cannot alias (Virtio9pDriver::exchange).
• Messages: session establishment plus bounded read and write subsets.
  • Tversion/Rversion – negotiates msize and the 9P2000.L version string. The requested msize is VIRTIO_9P_MSIZE (4096); QEMU’s server rejects anything below its P9_MIN_MSIZE of 4096 with Rlerror(EMSGSIZE). The server may shrink msize, and every later message is bounded by what it actually granted – each operation rebuilds its codec from the granted value.
  • Tattach/Rattach – establishes the share’s root fid (VIRTIO_9P_ROOT_FID) and yields its qid.
  • Twalk/Rwalk – clones the attached root onto the scratch fid (VIRTIO_9P_SCRATCH_FID), with zero or one path elements only (Virtio9pDriver::walk_scratch). A partial walk is treated as ENOENT; the server binds no fid in that case, so nothing is left to clunk.
  • Tlopen/Rlopen – O_RDONLY for files, O_RDONLY|O_DIRECTORY for the root before Treaddir, and O_WRONLY on the write paths. No other mode is ever sent.
  • Tgetattr/Rgetattr – entry size and the qid type bit, requested with GETATTR_ALL. Rreaddir carries an entry’s type but not its length, so a listing costs one Tgetattr per non-directory entry.
  • Treaddir/Rreaddir – the root listing, read to exhaustion, resuming from the last entry’s offset. . and .. are dropped and a non-UTF-8 host name is skipped rather than rendered as something that is not the host’s name.
  • Tread/Rread – file content, chunked by msize minus the Rread header, bounded by VIRTIO_9P_MAX_READ_BYTES. A short reply ends the read. The complete requested byte range is checked against the protocol’s u64 offset space before transport use, and every chunk offset is computed with checked addition rather than clamped or wrapped progression.
  • Tclunk/Rclunk – ends every transaction, including the error paths. A clunk can itself fail, and any failure downstream of a Twalk going on the wire leaves the fid’s state unknown, so the driver marks the scratch fid possibly-bound before it sends the walk and reclaims it at the start of the next one (Virtio9pDriver::release_scratch). Only the two replies that prove non-binding – a partial walk and an Rlerror for the walk itself – clear the mark; the reclaim also clears it on an Rlerror to the clunk, since that is the server proving it does not hold the fid. Without this, one failed teardown would collide with every later Twalk and wedge the export for the life of the boot. The fixed-field virtio-9p-scratch-fid-readback record is formatted by Virtio9pScratchFidReadbackSnapshot in kernel/src/virtio.rs. It reports current and high-water binding state plus saturating, reconcilable terminal outcomes for each walk and clunk attempt. Walk outcomes distinguish a confirmed bind, partial no-bind, server Rlerror, transport failure, and protocol failure; clunk outcomes distinguish confirmed Rclunk, server Rlerror, and preflight, transport, or protocol failure that preserves the mark. Pre-walk reclaim and defensive unbound-release mismatch counts remain separate. Virtio9pDriver::walk_scratch and Virtio9pDriver::release_scratch update this observer without changing the walk or release decisions. The record contains no path, name, tag, fid value, capability, or file-content material, and carries no self-cost tuple of its own: its bytes, Console call, and due-check misses are charged into the family aggregate published on virtio-9p-device-backing-readback.
  • Rlerror is accepted in place of any success reply and surfaces as Virtio9pHandshakeError::ServerError. ENOENT, EEXIST, and EROFS map to the typed Ninep9pRequestError::NotFound / AlreadyExists / ReadOnlyShare; every other errno collapses to Transport.
• Write subset (Tlcreate/Twrite/Tfsync/Trename/Tunlinkat), reached only from the virtio_9p_root_writable cap types. The functions that encode these messages are the ninep_create/ninep_write/ninep_fsync/ ninep_rename/ninep_unlink façade in kernel/src/virtio.rs; the read-only cap types contain no call into any of them.
  • Tlcreate/Rlcreate – creates an entry in the directory a fid refers to and rebinds that same fid to the newly created open file. The driver walks the root onto the scratch fid first and treats it as consumed either way: on Rlcreate it is an open file fid, on failure it is still the directory clone, so both outcomes stay covered by the existing possibly-bound mark. Sent with O_WRONLY|O_CREAT|O_EXCL, which makes “already exists” the server’s decision rather than a look-then-create window in the driver.
  • Twrite/Rwrite – file content at an offset, chunked by msize minus the 23-byte Twrite header (capos_lib::ninep::WRITE_REQUEST_HEADER_SIZE) and bounded in total by VIRTIO_9P_MAX_WRITE_BYTES. The codec refuses a decoded count larger than what was submitted – a caller advancing its offset by an inflated count would silently skip file content. A zero count on a non-empty submission is WriteStalled rather than an infinite resubmit loop. As on reads, an unrepresentable complete byte range is refused before transport use and later chunk offsets use checked addition. This prevents a valid prefix from reaching the host before the driver discovers that the rest of the requested range has no wire representation; it is not a rollback claim.
  • Tfsync/Rfsync – sent with datasync = 0 (a full fsync, so metadata is durable too) on a fid opened O_WRONLY, so a read-only share refuses the sync rather than reporting one it did not perform.
  • Trename/Rrename – always with the attached share root as dfid, so a rename cannot move an entry out of the export. POSIX rename would silently replace an existing target, but the Directory.rename contract fails closed on that, so an existence walk precedes the mutation. Check and rename are one driver-lock hold, so no other capOS caller can interleave. The writable QEMU proof seeds the target before boot, requires the exact Ninep9pRequestError::AlreadyExists refusal, and verifies after QEMU exits that both source and target bytes are unchanged. A host-side create landing after the existence walk but before Trename would still be replaced. That residual is accepted for a single-writer fixture share and is not an atomicity claim.
  • Tunlinkat/Runlinkat – removes a name from the attached root with flags 0 (no AT_REMOVEDIR). Operates on the root fid directly and binds no new fid, so it needs no scratch walk.
• Not implemented: Tsetattr (so File.truncate fails closed on both export variants), Tmkdir (so Directory.mkdir/sub fail closed – the export is a single flat directory), symlinks, Treadlink, and subdirectory traversal. Multiple concurrent tags, Tflush, and Tauth are also out of scope – the fixture keeps one exchange in flight at a time and each façade operation is one complete transaction under the driver lock, which is why a single scratch fid suffices.

3. capOS mapping

• Authority gate: the device is enumerated by the qemu-or-fixture-gated diagnose_virtio_9p (kernel/src/pci.rs), which claims the PCI function through the device-manager ownership ledger as DeviceOwner::Virtio9p and attaches a DMAPool authority record. Under qemu those two records come from the full qemu_full DDF ledger; under virtio_9p_host_fixture without qemu they come from the minimal device_manager::virtio_9p_fixture_claim surface (single-claim bookkeeping only – the DMA isolation is the always-built device_dma bounce ledger in both builds). Manifests without a -device virtio-9p-pci line take the pci: virtio-9p device not found path, so this is a diagnostic and never a boot dependency.

• DeviceMmio: the common, ISR, notify, and device-config regions are mapped through pci::map_bar_region with the same bounds validation the other virtio drivers use; the device-config region is mapped to exactly the advertised capability length because the 9p config is variable-length. No DeviceMmio capability is granted to userspace – the consumer reaches the share only through the typed Directory/File interfaces.

• Directory / File: kernel/src/cap/virtio_9p_fs.rs serves the existing interfaces over the driver’s subsets. No cap type holds a server-side fid – each call is a complete driver transaction (walk -> open -> op -> clunk) – so a dropped cap leaks nothing. Directory.open mints the File through a result-cap transfer whose mode follows the directory’s authority: read-only results are Copy / SameSession, while writable results are NonTransferable / SameSession.

  • virtio_9p_root (KernelCapSource::Virtio9pRoot, capnp ordinal 54) is minted by mount_root(). Virtio9pDirectoryCap is stateless; Virtio9pFileCap holds a validated name and the NinepFileIdentity observed at open: qid, size, generation/data-version, mtime, and ctime. Each read walks the name once and compares that identity before and after Tread through the same scratch fid. An atomic host rename therefore either leaves the read bound to the originally opened object or returns Ninep9pRequestError::IdentityChanged; bytes from a replacement object are never returned under the old cap. stat remains the open-time snapshot, and opening the name again observes the replacement. The writable handle instead re-stats and uses live name-based reads because its own writes intentionally change the opened object’s identity. Classified with the other genuine read-only views (read_only_fs_root, installable_image_source): Copy / SameSession, so forwarding it shares only a read view.
  • virtio_9p_root_writable (KernelCapSource::Virtio9pRootWritable, capnp ordinal 55) is minted by mount_root_writable(). Virtio9pWritableDirectoryCap delegates list to the read-only cap and serves create/remove/rename itself; Virtio9pWritableFileCap delegates read/close and serves write/sync, and re-stats the share rather than reporting the size captured at open, since the file changes under its own writes. Both the root and every File result are deliberately not in the read-only-view classification group: they carry host-write authority over a share with one writer, so each is minted NonTransferable and stays with the process that received it – the same reasoning that makes the disk-backed writable filesystem non-transferable.

  Both sources are minted only when a device is actually bound; otherwise the grant resolves to an error and the spawn fails closed rather than handing out a Directory over nothing.

  The writer can also be minted for a child. virtio_9p_root_writable is accepted as a raw kernel-source ProcessSpawner grant under the qemu or virtio_9p_host_fixture feature, so a parent that holds no writable share itself can hand one to a child it spawns. Every attenuation on that path is structural rather than a flag: the grant must be raw mode with a zero badge (both checked before the source is minted), its declared interface must equal the minted object’s Directory interface, and kernel_source_spawn_hold leaves the hold NonTransferable, so the child cannot forward it onward. The QEMU proof also opens a writable File and observes both an actual endpoint copy refusal and a raw-spawn refusal for that result. As a positive control, the child opens a fixture through a separately granted read-only root, copies that read-only File through an endpoint to a helper, and the helper reads the pinned host bytes. A kernel built with neither fixture feature refuses the writable-root grant outright.

  One writer per boot, enforced in two places. Manifest validation rejects a second virtio_9p_root_writable bootstrap grant across init and all services (capos-config/src/validation.rs); unlike terminal_session there is no forward-from-init exception, because every bootstrap grant naming this source re-mints a fresh writable root rather than forwarding one. Bootstrap grants are not the only mint site, though – a spawn grant is runtime IPC that no manifest check can see – so mount_root_writable() additionally latches on a WRITABLE_ROOT_MINTED flag and refuses every committed mint after the first, whatever the site. Bootstrap resolution commits the claim with its mint. Spawn handling instead validates the exact Directory interface before reserving the claim, retains that reservation through all later grant and process preparation, and commits it only when the child spawn commits. A failed request therefore returns the reservation because no writable cap was made reachable. Once committed, the latch is monotonic: it is not released when the holder exits, because File handles opened from a writable root are separate CapObjects that outlive it and keep a live write path to the share, so releasing on the root’s drop would admit a second writer alongside a still-writing first one. The cost is that the writer cannot be respawned within a boot; lifting that would need write-authority refcounting across both writable cap types, not a Drop impl.

• Interrupt: none. The fixture polls its used ring, so it deliberately claims no MSI-X route – interrupt_owner_for_device_owner maps DeviceOwner::Virtio9p to None, and the bring-up diagnostic records interrupt=none completion=polled-used-ring. No Interrupt capability exists for this device.

• DMAPool: the driver owns a dedicated single-queue DMA ledger (device_dma.rs, Virtio9pPoolConfig), a distinct type from the virtio-blk and virtio-net pools, so a page handle minted against one never validates against another. It holds five pages: the three split-ring pages plus one request and one reply bounce page. The ledger enforces generation-checked page handles and scrub-before-frame-free ordering. Host physical addresses stay kernel-owned; none is exposed to userspace. The bulk read paths (Tread/Treaddir) decode out of a heap frame bounded by the negotiated msize, so a full-msize reply never needs an msize-sized kernel stack frame.

  The identity-free virtio-9p-queue-readback record exposes the configured and effective queue depths, the five-page DMA ceiling, negotiated msize, the negotiated-msize transient heap-frame ceiling, service-lifetime logical-length and allocated-capacity high-waters for transient heap frames, retained read results, and retained listing-name storage, a combined allocated-capacity high-water for the intermediate name-vector and returned entry-vector element backings, plus simultaneous transient-plus-retained allocated bytes, encoded result bytes, reply-scratch bytes, and the whole-operation allocated byte peak across the driver and capability-encoding phases, plus live and high-water in-flight submissions and cumulative submissions and completions read through virtio_9p_queue_account_snapshot. Logical lengths remain separate from the allocated backing reported by Vec::capacity/String::capacity; reply scratch likewise uses its currently allocated backing length. Each listing-container charge is allocated element count multiplied by the Rust element layout size, with saturating arithmetic. While the name and entry vectors coexist during conversion, their charges are summed; other phases retain the largest live element-backing charge. The shared 8,192-byte formatter ceiling is checked against the 64-entry kernel layouts and by a host allocation test. Name bytes remain separately attributed. The existing logical-length fields remain comparable with earlier records, while the simultaneous value is capacity-derived. The whole-operation value is the greater of (a) that capacity-derived driver phase plus reply scratch already allocated before transport work and (b) retained read or listing capacity plus the encoded Cap’n Proto result and reply-scratch capacity after encoding. It also retains saturating mutually exclusive exchange outcomes for calibrated-monotonic, tick-derived, and spin-backstop poll expiry; malformed used-ring completion; DMA accounting failure; and DescriptorAlreadyActive refusal. One aggregate structural-refusal counter covers oversized capability reads and writes, overlong path elements and mount tags, unrepresentable byte ranges, directory-entry overflow, and readdir-round exhaustion. Virtio9pQueueObserver emits once after bring-up, immediately when an in-flight or allocation-byte high-water changes, and after a completed exchange when the cumulative submission or completion total reaches an exact power of two. A directory listing accumulates its allocation peaks locally and publishes at most once when the complete operation unwinds, including an error return; it does not emit per retained entry or Treaddir round. Binary live occupancy remains visible in each snapshot but does not trigger output by itself; failure and refusal counters retain their own power-of-two sampling. The production formatter is Virtio9pQueueReadbackSnapshot; it uses fixed storage and carries no path, name, fid, tag, PID, capability, or file-content material. Observation does not change admission, submission, timeout, reclaim, or recovery behavior.

• Device-page backing readback (virtio-9p-device-backing-readback): Virtio9pDeviceBackingSnapshot publishes the whole-device resident backing that the queue record excludes. fixed_device_page_backing_bytes is dma_page_budget multiplied by dma_page_bytes – 20,480 bytes from the kernel’s fixed five-page pool (three split-ring pages plus the request and reply bounce pages) – and whole_device_resident_backing_bytes_high_water adds that value to the simultaneous transient-plus-retained capacity peak republished on the same line. fixed_backing_derivation=code-owned-page-budget marks both as structural derivations of VIRTIO_9P_KERNEL_DMA_PAGE_BUDGET, not live physical-memory measurements, allocator-overhead accounts, or per-caller charges. resident_scope=fixed-pages-plus-driver-heap names what “resident” covers: device-owned backing only. The reply scratch and the encoded Cap’n Proto result are charged to the calling process’s ring (EffectiveReplyScratch over RingScratch::reply in kernel/src/cap/ring.rs, bounded by REPLY_SCRATCH_BYTES_MAX), not to the device, so they are outside this total. That is why the combined value reads below the operation_hw whole-operation peak on the paired queue record, which does include both – in the read-only proof, 25,600 against 70,656. Allocator-internal overhead, physical frames beyond the fixed pool, and QEMU-side host cost stay excluded. It is a separate record rather than extra queue-record fields because the saturated queue line already sits at its Console-call length bound with the established headroom; both records are emitted from one observer sample at the same call site, so each queue record has a matching backing record. It carries no identity material and changes no admission, submission, timeout, reclaim, or recovery decision.

• Readback self-cost (readback_cost on the device-backing record): Virtio9pReadbackOutputCost in capos-lib/src/virtio_9p_readback.rs renders saturating withheldPublications, formattedRecordBytes, and consoleCalls counters as one base-36 comma tuple. It is a single aggregate for the whole fixture readback family rather than a per-record figure: readback_cost_scope=queue,device-backing,scratch-fid names the three records it covers, and it rides this line because the queue line has no length budget left and the scratch-fid record comes from an independent observer. The tuple carries no identity material, allocates nothing, opens no new interrupt-disabled section, and changes no handshake, submission, timeout, reclaim, refusal, or recovery decision. What each counter charges, what stays uncharged, when a cost-only publication becomes due, and the remaining accounting gaps are governed by the diagnostic output descriptor inventory, which is authoritative for those rules.

• Fail-closed / validation rules: bring-up fails closed and leaves the driver unpublished on any of – missing required features, rejected FEATURES_OK, an undersized or oversized device-config/mount-tag, an absent or too-small request queue, or a failed handshake. Every reply is bounded before decoding: the device-reported written length must be at least a 9p header and no larger than the calling operation’s own reply buffer – the 256-byte stack scratch for the fixed-size messages, the msize-bounded heap frame for Tread/Treaddir – and the reply’s size prefix is cleared before each exchange so stale page contents cannot be decoded as a fresh reply. The capos_lib::ninep codec then independently validates the frame against the negotiated msize, the declared size, the expected tag, and the expected reply type before exposing a field. The host-supplied mount tag is rendered as printable ASCII only, so a hostile tag cannot forge or split a diagnostic line.

  The capability layer adds four more fail-closed rules. Traversal: a name reaching Directory.open must be exactly one ordinary path element – validate_9p_name rejects empty, ., .., any /, an interior NUL, and anything past VIRTIO_9P_MAX_NAME_LEN. It guards every façade entry point, read and write alike, and combined with the single-element Twalk and the root-anchored Trename dfid it means no mutation can land outside the share. Mutation: on a virtio_9p_root cap, Directory mkdir/remove/sub/create/rename and File write/truncate/sync all fail closed in the cap layer, and those types call nothing in the driver’s write façade. On a virtio_9p_root_writable cap, mkdir/sub/truncate still fail closed for want of Tmkdir/Tsetattr, and open still refuses CREATE/TRUNCATE because Directory.create is the fail-closed creation path (honouring them would report success for an operation that did not happen). Defense in depth: a share QEMU exported readonly=on refuses every mutation at the server with EROFS, so an over-broad manifest still cannot write a share the host meant to protect. Stable read identity: a read-only File compares its open-time NinepFileIdentity with Tgetattr on the same fid immediately before and after each read. A host-side rename, rewrite, or metadata change rejects the operation instead of mixing the open-time size with replacement bytes. Bounds: a host directory beyond VIRTIO_9P_MAX_DIR_ENTRIES (64) fails closed rather than growing an unbounded kernel allocation from outside the TCB; a read past VIRTIO_9P_MAX_READ_BYTES and a write past VIRTIO_9P_MAX_WRITE_BYTES are refused rather than silently short-read or clamped into a short write the caller cannot distinguish from host refusal. A non-empty read or write whose last requested byte would exceed u64::MAX returns the distinct Ninep9pRequestError::OffsetOverflow before any request for that range is issued.

  Entry names and file bytes are host-supplied, i.e. from outside the TCB. The cap layer passes them through unaltered (Text/Data in the ABI); every renderer is responsible for the escape seam, and the consumer demo routes each name through capos_rt::console_text::escape_console_text_bounded.

• QEMU-emulable vs hardware-only: entirely QEMU-emulable. virtio-9p is a paravirtual device with no hardware counterpart, so there is no hardware-only residue. The driver’s kernel host unit tests – including the readback formatters’ saturated Console-call-ceiling bounds – run under make test-kernel-virtio-9p-fixture, not cargo test-kernel: the default feature set substitutes virtio_stub.rs, so virtio.rs and its tests are not compiled there at all. The bring-up proof is make test-virtio-9p-bringup (tools/qemu-virtio-9p-smoke.sh, manifests/system-virtio-9p.cue), which asserts the negotiated msize and version, the mount tag read back from device config, and the attach qid’s directory type bit. The end-to-end capability proof is make test-virtio-9p-fs (tools/qemu-virtio-9p-fs-smoke.sh, manifests/system-virtio-9p-fs.cue, consumer demos/virtio-9p-fs, share built by tools/mk-virtio-9p-share.sh): a guest process lists the host share, reads exact host bytes back whole and at an offset, and observes every mutating and traversing method fail closed. The share’s pinned names, sizes, and position-dependent byte pattern are what make the read-back a proof the guest saw the host’s bytes rather than a compiled-in constant. The guest also opens a 36-byte valid wasm object, the host atomically replaces its name with a 4097-byte object carrying the same executable prefix, and a host-written completion marker synchronizes the replacement before the guest reads the old File cap. The read must fail on the changed identity. Two other fixture names differ only by escaping – one carries a real TAB, the other the literal characters \ and t – so the smoke also proves the render seam keeps distinct host names distinct. The guest additionally requests a 4096-byte read beginning at u64::MAX - 1; the capability must expose the distinct offset-overflow refusal before transport use.

  The read and write harnesses also require a complete, untruncated virtio-9p-queue-readback record with nonzero post-handshake submission and completion attribution, a nonzero structural-refusal count from the existing offset-overflow proof, and no more than 32 readback records per boot. This proves observer wiring and logarithmic successful-traffic sampling over the normal fixture; it does not inject timeout, mismatch, accounting, or stranded-slot failures and therefore establishes no recovery guarantee.

  Both harnesses then reconcile the published readback_cost tuple against the boot’s own Console transcript through tools/virtio-9p-readback-cost-check.sh. The diagnostic output descriptor inventory is authoritative for what that reconciliation requires.

  The write proof is make test-virtio-9p-write (tools/qemu-virtio-9p-write-smoke.sh, tools/qemu-virtio-9p-fsync-crash-smoke.sh, consumer demos/virtio-9p-write), which runs four stages sequentially through recursive make so their builds cannot share iso_root/. The fourth stage contains two isolated boots, for five boots total:

  1. test-virtio-9p-write-rw (manifests/system-virtio-9p-write.cue, share exported readonly=off) – the guest creates an entry, refuses a duplicate create, writes 6144 bytes in two calls, fsyncs, stats, reads back, renames, refuses a rename onto the pre-boot fixture entry with the exact Ninep9pRequestError::AlreadyExists application error, removes, and observes mkdir/sub/truncate/open(CREATE|TRUNCATE) and every traversing mutation fail closed. The first File.write submits 4096 bytes at offset 0, which exceeds the negotiated 4073-byte Twrite payload and forces the driver to resubmit the remaining 23 bytes at wire offset 4073. The guest then uses the returned count, 4096, as the offset for a 2048-byte second call. A second 4096-byte write beginning at u64::MAX - 1 must return the distinct offset-overflow refusal before transport use. After QEMU exits, the harness verifies the result on the HOST side of the share: the renamed file must exist with exactly 6144 bytes matching the guest’s position-dependent pattern, the pre-rename and removed names must be gone, no ../escaped.* may have appeared beside the share, and the pre-boot collision target must retain its exact pinned bytes. Together, the source comparison and target comparison prove that the refused collision changed neither file. That host-side check is what makes this a write proof rather than a guest self-report. The existing renamed-output pattern and absence checks have mutation evidence; the new collision-target byte comparison is direct host evidence and is not claimed as separately mutation-tested.

  2. test-virtio-9p-write-hostro (manifests/system-virtio-9p-write-hostro.cue, share exported readonly=on) – the SAME writable cap over a protected share. All five mutations must be refused with EROFS while list/open/read keep working (a share that merely failed to attach would refuse everything and prove nothing), and the host share must be unchanged afterwards. The guest matches every application exception against the driver’s exact ReadOnlyShare text before emitting a typed summary, and the harness requires both that summary and the writable grant source. The stage therefore cannot pass on a read-only cap: that cap refuses in the cap layer, with different wording, and never reaches the driver. After QEMU exits, the harness compares the pinned fixture bytes and rejects any of the proof’s mutation output names rather than treating name survival as byte immutability.

     Two precisions about what stage 2 refuses where. create, remove, and rename are refused on the wire, at Tlcreate/Tunlinkat/Trename. write and sync are refused earlier, at the Tlopen(O_WRONLY) that precedes them, so those two messages never reach the server in this stage – what is proven is that a write-intent open fails closed, which is the gate that matters, not that QEMU rejects a Twrite. And the stage pins QEMU’s choice of errno: another server answering the write-intent open with EACCES rather than EROFS would map to Transport and fail this gate loudly rather than degrade silently.

  3. test-virtio-9p-write-spawn (manifests/system-virtio-9p-write-spawn.cue, share exported readonly=off) – the writable cap reaching a child through a raw kernel-source ProcessSpawner grant. The parent holds a read-only view for the positive delegation control but no writable share, so the child’s writer is the only one this boot. The child asserts the exact Directory interface ids on arrival, writes 4096 bytes in two chunks (the second at a non-zero offset), syncs, stats and reads back. It then opens both a writable and a read-only File: endpoint copy and raw spawn refuse the writable result, while a helper receives the read-only result by endpoint copy and reads the pinned fixture through it. Raw spawn also refuses the writable root. Before the successful spawn, the parent submits raw-wire probes for a wrong writable-root interface and for a malformed later grant; both fail without consuming the one writer. It also checks non-raw mode, a non-zero badge, and a second mint after the successful child exited. After QEMU exits, the harness verifies the child’s bytes on the HOST side of the share.

     Each refusal is matched against the kernel’s own exception text rather than against is_err(), because the negative cases here exercise different mechanisms that an is_err() check could not tell apart – the pre-slice behavior, a single blanket “unsupported kernel source” rejection, would have failed all of them while proving none. For the same reason the stage does not grep the granted source the way stages 1 and 2 do: that diagnostic is emitted only for bootstrap grants, and the writable root is minted only at spawn time. What pins writable provenance instead is the host byte check, which the parent’s read-only cap cannot satisfy at all.

     Mutation-tested in both directions: disabling the WRITABLE_ROOT_MINTED latch makes the second mint succeed and fails the gate, and perturbing the child’s payload pattern fails the host comparison while the child’s own self-consistent read-back still reports match=ok – which is the point of verifying on the host rather than trusting the guest. Changing the writable File result hold back to Copy makes the actual endpoint transfer succeed and fails the gate before the read-only control call. A valid child still writing the 4096-byte host payload after each pre-commit raw-wire refusal proves those failures returned the writer reservation.

  4. test-virtio-9p-write-fsync-crash (manifests/system-virtio-9p-write-fsync-crash.cue, two shares exported readonly=off) – the positive boot creates and writes a distinct 4096-byte payload, invokes File.sync, emits its arming marker only after the call returns, and spins while the harness force-kills QEMU. The harness then requires the host file to contain the complete expected payload. A second boot uses a host-seeded selector to take the negative-control arm: it emits a distinct marker after File.write returns but before invoking File.sync, then spins at that point until the harness force-kills QEMU. The marker pair proves that the two kills landed on opposite sides of the sync call rather than letting either transcript satisfy the stage.

     On the current QEMU local 9p backend, the pre-sync control file is also present and byte-complete. Killing the QEMU process does not discard the host kernel’s filesystem page cache, so post-exit host readback cannot distinguish the synced and unsynced cases. The stage reports this as a bounded negative finding and does not promote the positive survival into a durability proof. This adds no driver path or ordering change: it exercises the already-landed ninep_write then ninep_fsync order through the existing writable File capability.

  The composable-fixture co-boot proof is make test-virtio-9p-net-coboot (tools/qemu-virtio-9p-net-coboot-smoke.sh, manifests/system-virtio-9p-net-coboot.cue). It builds ONE not(qemu) kernel under both cloud_virtio_net_userspace_sustained_receive_pool_proof and virtio_9p_host_fixture and boots it with a virtio-net device and a readonly=off virtio-9p share, asserting that the Phase C userspace Nic path and a writable Directory both serve in the same boot: the writable-9p write proof runs to completion (its 6144-byte result verified on the host side of the share) while the userspace NIC shim drains its sustained receive pool (link=up, frames_received=2). This is the proof that the fixture composes with the Phase C userspace network stack for the Host-Accessible Persistent Task Backend milestone without enabling the competing qemu virtio-net/DDF owner. Because a not(qemu) kernel has no compiled isa-debug-exit shutdown path, both services run to completion and the VM terminates on the harness timeout (exit 124).

  Known coverage residuals. The smoke proves an absent-entry lookup does not wedge the export, but it does not exercise the scratch-fid reclaim itself: a compliant server answers that lookup on the ENOENT path, where no fid is bound, so the assertion would pass with the reclaim removed. The paths the reclaim exists for – a failed Tclunk, an over-long Rwalk, an undecodable frame, a post-completion accounting failure – require a hostile or faulty 9p server that QEMU will not produce. Closing this needs a proof-only feature that injects the failure, in the shape of storage_writable_recovery.

  Three residuals belong to the write subset specifically:

  • Server short-write and WriteStalled handling are unproven. The 4096-byte first call now proves chunk resubmission under the negotiated 4073-byte payload limit, including the advancing wire offset and the guest-visible returned count. QEMU accepts every submitted chunk in full, however, and never returns zero. Exercising resubmission after a non-zero short count and the zero-count WriteStalled refusal requires a hostile or fault-injected server.
  • Tfsync durability remains unproven after a forced-poweroff negative control. test-virtio-9p-write-fsync-crash proves that a known payload is complete on the host after QEMU is force-killed following a returned File.sync. Its paired control is force-killed after File.write returns but before File.sync is invoked, and that payload is also complete. QEMU process termination leaves the host kernel and its page cache alive, so reading the same host filesystem after exit cannot isolate what Tfsync contributed. The existing proof still shows that the call is issued, accepted on a writable share, and refused with EROFS on a read-only one; the new stage bounds why this fixture cannot establish crash durability. Closing the residual needs a model that makes the storage boundary and cache-loss event observable rather than another post-exit read of the same live host filesystem.
  • The Trename existence check is not atomic against the host. See the Trename entry in §2. A target present before the guest request is proven to produce AlreadyExists with source and target bytes intact, but a host-side create in the check-to-rename window would still be replaced. Only capOS-side callers are serialized, by the driver lock.

  The non-qemu refusals are covered separately, by a host-side policy test rather than by a run. The decision itself is capos_config::virtio_9p_writable_source_refusal (capos-config/src/manifest.rs): a pure function taking the source, the mint site, and whether a virtio-9p fixture feature is compiled in. Both mint sites call it ahead of their source match, in every build, passing cfg!(any(feature = "qemu", feature = "virtio_9p_host_fixture")) – bootstrap resolution in cap/mod.rs and build_child_caps in process_spawner.rs. On the spawn-grant path that call is the only refusal for this source; the bootstrap match keeps a cfg(not(any(...))) arm only because it is exhaustive over KernelCapSource with no catch-all. That arm does not restate the refusal – it is an unreachable! asserting the guard already returned. Restating it there would leave bootstrap refusing on its own after a mutation to the shared function, which would falsify the policy test’s claim to decide production behavior.

  Passing the feature state as an argument, rather than reading cfg inside the function, is what makes this testable: cargo test-config evaluates the production decision with the feature off, which no test can do by compiling the kernel, since every stage of make test-virtio-9p-write builds --features qemu. The tests assert both directions (refused without the feature, admitted with it), that the policy passes every other source through untouched, and that each refusal names the source and the missing feature, differs per mint site, and is not the blanket “unsupported kernel source” fallthrough. That last part matters because a build without qemu would refuse the grant either way, via the fallthrough arm, so only the specific text distinguishes deliberate qemu-gating from the source merely not being wired up. Mutation-tested at both sites: flipping either branch of the shared function – spawn-grant or bootstrap – to admit the source fails cargo test-config. Under the bootstrap mutation the non-qemu kernel still compiles, which is exactly what the assertion arm buys: that site no longer refuses on its own, so the shared function is the only thing deciding.

  What that does not establish is a runtime observation. No booted kernel exercises the refusal, so the claim is that the production kernel’s own decision function refuses – not that a running production kernel was seen refusing.

  One accepted limitation is not a proof gap but a scope decision: File.write bounds the payload per call but not the offset, so a writable-cap holder can write a byte at a very large offset and make the host materialize a sparse file. That is within the authority the cap already grants (it can create, write, and unlink entries in the share), and the fixture is a QEMU-hosted dev-loop share pointed at a dedicated scratch directory. A production writable route would need a quota, which is one more reason this is not one.

Related

• Implementation: kernel/src/virtio.rs (Virtio9pDriver, Virtio9pDma, diagnose_virtio_9p_transport, and the ninep_* façade), kernel/src/pci.rs (diagnose_virtio_9p, PciDevice::is_virtio_9p), kernel/src/device_dma.rs (Virtio9pPoolConfig, SingleQueueDmaLedger).
• Capability layer: kernel/src/cap/virtio_9p_fs.rs (Virtio9pDirectoryCap, Virtio9pFileCap, mount_root; Virtio9pWritableDirectoryCap, Virtio9pWritableFileCap, mount_root_writable, WRITABLE_ROOT_MINTED); grant-source resolution in kernel/src/cap/mod.rs; the spawn-grant arm in kernel/src/cap/process_spawner.rs; the single-writer bootstrap check in capos-config/src/validation.rs; source names in capos-config/src/manifest.rs.
• Consumer proofs: demos/virtio-9p-fs, tools/qemu-virtio-9p-fs-smoke.sh, manifests/system-virtio-9p-fs.cue; demos/virtio-9p-write, tools/qemu-virtio-9p-write-smoke.sh, manifests/system-virtio-9p-write.cue, manifests/system-virtio-9p-write-hostro.cue; demos/virtio-9p-write-spawn-parent, demos/virtio-9p-write-spawn-child, manifests/system-virtio-9p-write-spawn.cue. Shared fixture share: tools/mk-virtio-9p-share.sh.
• Protocol codec: capos-lib/src/ninep.rs; fuzz target fuzz/fuzz_targets/ninep_reply_decode.rs.
• Design: Virtio-9p Host Directory Passthrough.
• Shared transport seam: virtio-net, virtio-blk.