Developing Cohesix Drivers

This is the engineering guide for creating and changing Cohesix drivers. It defines the development workflow, the boundaries between the manifest compiler, HAL, isolated runtime, root client, and subsystem, and the evidence required to call a driver correct.

This document is not a driver-status page or an incident log. Put milestone state in BUILD_PLAN.md, physical runbooks and current evidence in HARDWARE_BRINGUP.md, test procedures in TEST_PLAN.md, and temporary investigation notes outside the canonical documentation set. Update this guide only when the reusable driver development contract changes.

See the Glossary for Cohesix-specific runtime, authority, and evidence terms.

1. Start with the governing contract

Before changing a driver, read:

1. AGENTS.md for the repository-wide architecture and merge rules.
2. BUILD_PLAN.md for the exact active milestone task that authorizes the work.
3. The selected configs/root_task*.toml profile and its resolved manifest.
4. The generated seL4 headers and configuration in the selected SEL4_BUILD_DIR.
5. The relevant runtime, HAL, ABI, subsystem, and test sources listed in the source map.

The active task must authorize every touched surface. If the task, selected profile, and as-built system disagree, fix the scope in BUILD_PLAN.md before implementing driver behavior.

Use the repository task format verbatim:

Title/ID: <slug>
Milestone: <exact milestone/submilestone and task title/ID>
Goal: <one sentence>
Inputs: <artifacts, versions, paths>
Changes:
  - <file> — <summary>
Commands: <exact shell commands for the scoped host/target; default macOS ARM64>
Checks: <deterministic success criteria>
Deliverables: <files, logs, doc updates>

Every new or modified human-authored file must retain or add the required Lukas Bower author, purpose, and 2026 copyright metadata in its native comment syntax.

2. Understand the architecture before writing code

Physical drivers do not run as steady-state root-task code. Each physical device role is served by a manifest-declared isolated runtime child. Root-task constructs and admits resources through HAL, creates the child, submits bounded commands, consumes completions, and projects diagnostics. The child owns the device engine after handoff.

flowchart LR
  Manifest["Selected manifest and generated tables"] --> HAL["HAL admission"]
  Kernel["Selected seL4 build truth"] --> HAL
  HAL --> Init["Sealed runtime-init descriptor"]
  Init --> Runtime["Isolated driver runtime"]
  Client["Root driver client"] -->|"bounded command"| Runtime
  Runtime -->|"durable completion"| Client
  Runtime --> Device["Declared MMIO, DMA, IRQ, or bus link"]
  Client --> Trait["Device-independent subsystem trait"]
  Client --> Evidence["Bounded diagnostics and proof"]

2.1 Layer responsibilities

HAL owns resource admission for MMIO, IRQ, DMA, PCI, SDIO, board-level power/reset, and firmware bundles. A child may use only the capabilities and mapped pages sealed into its runtime-init descriptor.

2.2 One owner for every physical effect

Write down the ownership model before implementation. For every register bank, descriptor ring, interrupt source, DMA buffer, firmware mailbox, and recovery action, name exactly one physical owner.

The design must have:

• one path that issues a physical operation;
• one path that completes it;
• one path that retries or recovers it;
• one immutable identity from logical parent through physical child and terminal receipt; and
• no polling, compatibility, diagnostic, or emergency path that can become a second owner.

Multiple scheduling lanes may request service from one owner. They do not gain independent physical authority. A notification is a scheduling hint, not an ownership transfer and not proof that an operation completed.

Root may retain the documented emergency serial path for fatal output. That exception is not steady-state serial ownership and cannot be generalized to other devices.

2.3 Physical and compatibility drivers are different proof lanes

Pi 4 physical drivers use isolated runtime images and the fixed driver-task ABI. QEMU VirtIO and RTL8139 implementations are profile-gated compatibility drivers for virtual-device, host, and protocol tests. A QEMU success can prove shared subsystem behavior, but it cannot prove Pi MMIO, DMA, IRQ, timer, PCIe, USB, GENET, SDIO, or CYW43 behavior.

3. Design the driver on paper

Create a short design record in the task or PR before editing source. It should answer all of the following.

3.1 Role and authority

• What device-independent role does the driver provide?
• Which isolated runtime owns the hardware?
• Which HAL capability admits each resource?
• Does the device depend on another runtime? If so, which side is the client, which side is the sole physical owner, and what is the bounded bus-link protocol?
• Which root component consumes the driver, and through which narrow trait?
• What is explicitly outside the driver’s authority?

Choose devices by role, not model. Model-specific logic belongs behind the role boundary. A subsystem must not branch on a PCI ID, board name, or chip family when a trait can express the required service.

3.2 Resource inventory

List the exact requirements for:

• code, stack, IPC, ring, and shared-buffer pages;
• MMIO pages and safe register widths;
• DMA pages, alignment, bus-address rules, and coherence;
• framebuffer or firmware buffers;
• IRQ numbers, trigger modes, badges, handler slots, and notification slots;
• linked-runtime endpoints, notifications, shared ranges, epochs, and queue depths;
• scheduling class, authority class, affinity, service budgets, and queue depth; and
• elapsed-time deadlines and the selected timer source.

Treat the inventory as a bound, not a suggestion. Unknown, overlapping, misaligned, excessive, or undeclared resources must fail closed.

3.3 State machine and terminality

Describe the state machine as bounded transitions. For every command, define:

• the immutable request identity;
• preconditions and validation errors;
• the physical issue point;
• pending states and the exact condition that makes progress possible;
• a finite operation budget and elapsed-time deadline;
• success and failure terminals;
• how hardware and software ownership return to a quiescent state; and
• what evidence the final consumer records after receiving the terminal.

Never use a retry counter as a substitute for elapsed time. Never use a timeout to silently switch to another owner or implementation.

A resumable active driver may select MCS NaturalPostpone in its target manifest when one immutable physical lifetime intentionally spans multiple SC refills. That policy leaves the exact budget, period, standard-fault endpoint, explicit device deadline, owner, and terminal publication unchanged; it only prevents ordinary current-refill exhaustion from becoming a false terminal timeout fault. Generated timeout capability identity and resource accounting remain present. The selection requires target evidence for bounded progress and cannot replace a device deadline, no-progress detector, or fault-containment test. The driver TCB constructor must consume this generated policy at the actual TCB.SetTimeoutEndpoint boundary. Its bounded construction record reports both the policy and whether the timeout endpoint was installed or omitted; manifest selection without matching kernel-object construction is a failed invariant.

3.4 Acceptance plan

State the evidence needed at each tier before coding:

• model and unit-test proof;
• generated/profile proof;
• target compile and image provenance;
• media readback when applicable;
• current-image runtime identity and owner-state proof;
• useful device I/O;
• repeatability; and
• performance under the required mixed load.

This prevents a source test or generated descriptor from being mistaken for a hardware result.

4. Implement a new physical driver

The following order keeps compiler truth, authority, ABI, runtime behavior, and tests aligned. Existing drivers use the same order for material changes.

Step 1: Add the compiler-owned declaration

Add the runtime image to the applicable root_task.driver_images profile. A runtime image record declares:

• a stable image ID;
• a contract name and hot-path name;
• the packaged artifact and entry symbol;
• bounded code, stack, IPC, ring, MMIO, DMA, and shared-buffer pages;
• any role-specific root-wake notification; and
• whether root context is forbidden and hardware state is migrated.

Declare IRQs and reciprocal bus links in the same profile when they are part of the topology. Do not encode those values again in prose or infer them at runtime.

The current compiler intentionally recognizes a closed set of Pi 4 hot paths. A genuinely new role therefore normally requires coordinated changes to:

• DriverRuntimeImagePolicy and its validators in tools/coh-rtc/src/ir.rs;
• generated Rust and documentation output in tools/coh-rtc/src/codegen/;
• every selected profile that must support the role;
• affinity and feature validation;
• negative compiler tests for missing, duplicate, overlapping, excessive, and inconsistent declarations; and
• generated artifacts and their hashes.

Do not hand-edit apps/root-task/src/generated/*, configs/generated/*, scripts/cohsh/boot_v0.coh, or docs/snippets/*. Run the full generator output set defined by scripts/check-generated.sh, then run the guard again. The short generator form that emits only root-task Rust and a resolved manifest is not sufficient for an intentional regeneration.

Step 2: Define or extend the pointer-free ABI

Use pi4-driver-abi for data shared between root and the runtime. ABI records must be no_std, fixed-size, pointer-free, and validatable without trusting the sender.

Prefer existing generic records for MMIO, DMA, shared pages, IRQs, resource ranges, commands, completions, counters, and bus links. Add a role-specific record only when the generic contract cannot express the required semantics.

For every new or changed record:

1. Define magic, version, size, alignment, capacity, and reserved-field rules.
2. Use offsets, lengths, indices, physical addresses, bus addresses, epochs, and tokens rather than virtual pointers.
3. Validate arithmetic with checked operations.
4. Reject unknown flags, opcodes, versions, roles, and out-of-range values.
5. Define the publication order and terminal commit field.
6. Add positive, boundary, malformed, stale-identity, and torn-publication tests on both sides of the ABI.
7. Bump DRIVER_RUNTIME_INIT_VERSION when layout or shared protocol semantics change, and update every producer, consumer, generator check, fixture, and diagnostic that depends on it.

Do not place policy objects, trait objects, slices, references, process-local addresses, or allocator-owned structures in the ABI.

The selected Pi contract uses driver runtime-init ABI v13. It preserves v12’s descriptor size and fixed child slot 12, where HAL mints only a Write-only, badge-1 capability to the additional root-control wake notification. The CYW43-specific child-to-root notification in slot 11 remains distinct and keeps its existing meaning and consumers. ABI v13 retains the existing root-owned continuation record’s action frontier explicit without changing its 24-byte layout: low-31-bit grant_id values advance consumed_grant_id from zero, to grant_id | ACTION_ADMITTED_BIT, to the exact grant_id. Admission is not completion and cannot authorize a successor; only the exact post-action value can. The same transition applies to delegated CYW43-to-SDIO grants after their initial grant-free action publishes an exact service receipt. After a runtime commits a durable terminal, RX, TX, or completion record, it signals the existing role-specific completion or doorbell first and slot 12 second. A nonterminal root-grant action signals slot 12 only after its exact post-action value is durable. The fan-in is a coalescing scheduling hint, not completion, identity, work credit, Reply, or device authority; the consumer must acquire and recheck the sequence-last durable record before acting or sleeping. ABI v13 additionally assigns the mutually exclusive 24-byte auxiliary slot to generic MCS one-way wait records: after one bounded pending quantum the child commits exact request, action fingerprint, runtime identity, and next slice as DROW, atomically signals the shared root-control fan-in and parks on its local notification. Root may change only that exact stable record to DROA, then signals the same runtime generation once. The child resumes only after observing the exact durable acknowledgement; a badge, stale slice, gap, wrong command, wrong runtime, wrong ring, or wrong capability generation grants nothing and fails closed. Reply-bearing bootstrap commands instead use the supervised MCS Call/Reply lane so callers that immediately consume the first descriptor or QEMU smoke completion retain one causal activation. Classic bootstrap keeps its bounded one-way transport. ABI v13 preserves every role’s physical ownership, queue, retry, recovery, and fault contract.

The exact-publication and current-response corrections are scheduling-only. An exact persistent MCS CYW43 publisher reuses its bound local-notification slot 3 and generated send-only SDIO-doorbell slot 8 for one atomic prompt and park immediately after sequence-last child commit; classic and inexact publication paths retain their existing one slot-8 signal. The separately fenced later root-causal wait keeps its existing kernel-specific wait behavior. The GENET path binds its existing one-slot control sequence and current response terminal; it adds no record or tail. Neither correction changes an ABI layout or version, capability right, manifest field, generated contract, queue, owner, command, completion, retry, or recovery record.

Step 3: Add the scheduling contract

Every root service path validates a DriverTaskContract before HAL admits work. Add the role to the contract and hot-path tables in apps/root-task/src/hal/driver_task.rs.

The contract defines:

• DriverTaskKind;
• service class;
• authority class;
• isolation state;
• maximum HAL operations, bytes, frames/reports/rows, and any explicitly permitted bounded bootstrap spins per turn;
• whether a wait is permitted;
• preemptibility; and
• maximum inbound queue depth.

Reject zero or excessive budgets, unbounded waits, non-preemptible hardware turns, class/authority mismatches, and physical RootTaskCompatibility fallbacks. Affinity and scheduling values are profile-qualified; a generated value is not proof that the kernel applied it on the target.

Step 4: Implement HAL admission

Use the narrowest existing capability trait:

• DeviceHal for generic device pages, DMA frames, coverage, and IRQ binding;
• PciHal for admitted PCI topology, BAR mapping, and command-register configuration; or
• Cyw43Hal for the admitted CYW43 firmware bundle.

Add a narrower trait when a new capability class is genuinely required. Do not expand the Hardware compatibility facade just to make a call site convenient.

HAL must validate and construct every resource before the child runs. This includes:

• exact physical coverage and requested physical address;
• page order, alignment, access permissions, and non-overlap;
• DMA allocation and bus-address publication;
• IRQ handler, badged notification, trigger, and child capability slots;
• reciprocal runtime link capabilities and shared ranges;
• runtime image identity, entry point, code and stack bounds;
• child CSpace and VSpace capacity; and
• the sealed runtime-init descriptor.

Physical-address discovery, device-untyped retyping, DMA allocation, IRQ binding, PCI configuration, board power/reset admission, and firmware-resource selection must not escape HAL.

Step 5: Create the isolated runtime entry point

Add a binary under apps/pi4-driver-runtime/src/bin/ and its [[bin]] entry in apps/pi4-driver-runtime/Cargo.toml. Reuse the shared runtime machinery in apps/pi4-driver-runtime/src/lib.rs; do not create a private transport or a second ABI.

On startup, the runtime must:

1. Receive the initialization command through the fixed entry point.
2. Validate descriptor magic, ABI version, task key, artifact identity, role, hot path, flags, counts, ranges, and link identity.
3. Reject missing required resources and forbidden extra resources.
4. Construct only bounded local views over the mapped resources.
5. Initialize the device without discovering new authority.
6. Publish an explicit ready or failed terminal.
7. Enter the command/notification loop only after initialization is durable.

The runtime state must fit within statically bounded storage. Avoid large stack frames; place large queues and device state in bounded static or admitted shared storage. VM code remains no_std.

Step 6: Implement bounded service turns

A normal service turn is:

1. Root reserves the single producer lane.
2. Root writes the complete command body.
3. Root performs required cache maintenance and barriers.
4. Root commits the command sequence last.
5. Root invokes the declared endpoint or notification.
6. The runtime validates and accepts that exact command.
7. The runtime performs no more than the admitted work budget.
8. The runtime publishes one terminal, explicit pending state, or budget exhaustion result.
9. The final consumer validates and records the exact completion.

No turn may wait without a finite deadline. No turn may monopolize the event pump until hardware, firmware, another runtime, or network traffic responds. Long operations must use an explicit retained cursor whose identity and deadline survive across turns.

Step 7: Add the root client and subsystem adapter

Add root-side publication, completion consumption, and owner-state evidence to apps/root-task/src/hal/driver_task.rs or a narrowly scoped client module. The client must:

• enforce the scheduling contract;
• serialize the single producer;
• preserve one immutable request identity;
• distinguish pending, terminal success, terminal failure, and no response;
• reject stale or cross-generation completions;
• return control to the event pump after bounded work; and
• expose a narrow device-independent trait to the consuming subsystem.

Root may validate, submit, observe, and adapt. It must not duplicate device register access or implement a rescue data path.

Step 8: Add bounded diagnostics

Diagnostics are passive snapshots unless the operator command explicitly states that it starts a bounded probe. A diagnostic must report:

• selected profile and runtime identity;
• descriptor acceptance and resource totals;
• owner and generation identity;
• command issue, progress, and terminal sequence;
• typed blocker or first fault;
• IRQ, DMA, cache, timer, and queue counters relevant to the claim; and
• whether evidence is current, retained, inferred, stale, or unavailable.

Keep records short enough for the documented console bound. Rate-limit repeated hot-path output. A diagnostic must never clear a fault, issue hardware I/O, renew a lease, retry an operation, or promote cached readiness unless that mutation is the documented purpose of a separately bounded command.

Step 9: Package the runtime

The Pi image builder compiles the declared runtime binaries, packages them in the driver-runtime CPIO, embeds that payload in root-task, and stages the U-Boot image set. A new runtime must be added consistently to:

• apps/pi4-driver-runtime/Cargo.toml;
• the selected manifest image records;
• root runtime-image and bootstrap contract tables;
• the image builder’s binary and CPIO entry lists;
• CSpace preflight accounting;
• artifact-freshness checks; and
• target-qualified Test Plan actions.

Do not copy an old runtime binary into a new image or infer freshness from its filename. The packaged bytes, generated identity, source revision, target image, media readback, and boot marker are separate evidence.

5. Implement hardware access correctly

5.1 MMIO

Use MappedRegion, MappedRegisterWindow, or MappedRegisterPages derived from HAL admission. Access registers with the exact width specified by the device contract and use volatile reads/writes only inside the admitted range.

For every register operation:

• validate offset, width, alignment, and access permission;
• preserve reserved bits;
• handle read-clear and write-one-to-clear semantics explicitly;
• document ordering requirements at the call site;
• use a known-safe register for posted-write readback; and
• avoid diagnostic reads that have side effects.

volatile prevents compiler elision of the access. It does not provide a memory barrier, cache maintenance, or DMA ownership transfer.

seL4 device untypeds use a forward-moving allocation watermark. When pages in one device-untyped region are admitted to different owners, lower child-only pages may need pre-admission before a higher root mapping advances the watermark. Map multi-page apertures in ascending physical-page order, verify device coverage, and verify that the mapped frame’s reported physical address equals the request before publication.

5.2 DMA and cache maintenance

HAL allocates DMA memory and publishes primitive page or semantic range records. A runtime derives local and device-visible addresses only from those records.

For every buffer or descriptor, define an ownership cycle such as:

CPU free -> CPU prepared -> cache-maintained when cacheable -> device owned
device complete -> cache-maintained when cacheable -> CPU consumed -> CPU free

Requirements:

• clean CPU-produced data in cacheable mappings before a non-coherent device reads it;
• invalidate device-produced data in cacheable mappings before the CPU reads it;
• for seL4_ARM_Page_Uncached mappings, skip cache operations while retaining the required DMA publication and consumption barriers;
• order descriptor publication after payload preparation;
• order completion consumption after device ownership returns;
• use the selected seL4 cache operations and barriers;
• reject lengths or bus addresses outside admitted ranges; and
• keep command-ring publication separate from payload-DMA publication.

The authenticated CACHELOG operator view is diagnostic evidence, not device ownership or a DMA synchronization primitive. Root keeps the existing 1920-record bound. A synchronous network request reserves the complete bounded snapshot allocation before taking the cache-log lock, holds that lock once only while copying the selected newest-first records, then renders and transmits one record at a time after release. Allocation failure returns a typed bounded error without a partial snapshot; live-ring mutation after capture cannot change, reorder, duplicate, or extend the response. This snapshot path adds no cache-maintenance operation, device transition, DMA authority, or Pi timing change.

The Pi 4 profile uses bounded-no-iommu. It provides bounded allocation, range, ownership, and cache discipline; it is not hardware-enforced isolation from a malicious DMA-capable device. Do not claim SMMU/IOMMU protection for that profile.

5.3 IRQs and notifications

An interrupt path must be declared, generated, admitted, bound, and validated before the device source is enabled.

For a level-triggered source, the runtime normally:

1. reads and validates the exact source;
2. masks or latches it according to the device contract;
3. performs bounded source service;
4. clears the device source, or durably records the source under a defined cursor-owned mask;
5. acknowledges the seL4 IRQHandler; and
6. republishes remaining work if the service budget was exhausted.

Do not acknowledge the kernel IRQ before the device source is safely cleared or retained. A notification may coalesce and may arrive before, after, or with other state. The consumer must always recheck durable work before sleeping.

On selected MCS builds, a notification bound to the receiving TCB defines its badge but does not define the returned MessageInfo. Runtime receive classification is therefore badge-first: the exact compiler-owned 64-bit command badge with nonzero message length is endpoint IPC; any admitted low-32-bit nonzero badge is a notification even when the message length is stale; and zero, zero-length command, wrong-task, or foreign high-domain badges fail closed. Classic seL4 retains its length-first receive semantics. Device routing still validates the admitted one-hot or coalesced notification bits before performing one bounded owner quantum.

If the selected implementation is intentionally polled, report it as polled. Do not claim interrupt delivery from configuration eligibility or an unused IRQ record.

5.4 Timeouts and delays

On Pi 4, elapsed-time logic uses CNTVCT_EL0 only when the selected seL4 build enables KernelArmExportVCNTUser / CONFIG_EXPORT_VCNT_USER. Convert ticks using generated TIMER_CLOCK_HZ.

Do not use:

• CNTPCT_EL0;
• EL0 timer-control registers;
• a dummy timer for hardware acceptance;
• raw CPU-speed spin loops; or
• an unqualified poll count as elapsed time.

A fixed attempt count may bound protocol work. If it represents a real delay or timeout, pair it with a virtual-counter deadline. Performance claims require a counter-qualified target trace.

5.5 PCI and board-level setup

HAL owns PCI topology discovery, BAR admission, command-register changes, root-complex setup, firmware reset, and DMA-window policy. The isolated device runtime owns only the admitted function or controller service after handoff.

Prove identity, class, BAR shape, link state, command bits, and DMA window before giving a child credit for downstream device function. Linux or U-Boot captures may be reference material; they are not live Cohesix authority or target proof.

6. Preserve durable command and completion semantics

6.1 Publish body first and commit identity last

Shared command, completion, event, and diagnostic records use a sequence-last publication rule:

1. clear or invalidate the old commit field;
2. write the complete body;
3. perform required cache maintenance and barriers; and
4. publish the nonzero sequence, epoch, or commit value last.

Readers must take a stable snapshot, validate the identity, and reject torn, zero, stale, or mismatched records. Do not treat the highest observed sequence as sufficient when another field binds the exact request or generation.

6.2 Commit before notification

When a producer wakes another task, the terminal or durable pending condition must be visible before the signal. The order is:

terminal body -> cache clean/barrier -> sequence-last commit -> notification

The consumer must recheck the committed condition after preparing to wait and immediately before the blocking receive. This closes the wake-before-wait and signal-before-commit races without turning polling into a scheduling clock.

On the selected MCS profile, local terminal retirement is part of this order. After the sequence-last completion is durable, the runtime must update its consumed command sequence and publish receive-ready with that exact retired sequence before any syscall can wake the producer. Later idle-poll progress preserves that sequence, while zero remains reserved for initial admission. A reply-bearing terminal then uses the runtime’s sole Reply object in one atomic seL4_ReplyRecv; a committed one-way SDIO child uses one atomic slot-10 CYW43 prompt plus slot-3 local wait. The returned endpoint MR0 or bound-notification badge is classified and any immutable successor is sealed without another outer receive boundary. For the reciprocal SDIO handoff, that component prompt is the first post-retirement scheduling syscall; passive diagnostics and generic root fan-in follow only after the returned wake is classified. Terminal time and CYW43 pending state are captured before that atomic wait and published afterwards, so park time and returned-source service cannot contaminate the retired command’s evidence. If a returned CYW43/SDIO badge also carries a physical source, the runtime seals the immutable successor, publishes that captured evidence, services exactly one source quantum, and yields before foreground physical I/O; a pure peer baton continues locally. If completion publication fails, the runtime enters its generated standard- fault containment lane before local retirement, receive-ready, Reply, signal, or receive. These rules change no Reply ownership, notification authority, SC numeric, operation bound, or physical owner.

6.3 Retained operations

Use a retained operation only when a single bounded turn cannot finish the device action. Its cursor must bind:

• parent request sequence;
• operation code and immutable arguments;
• role-specific descriptor or payload fingerprint;
• logical and physical generation;
• current phase;
• remaining operation, byte, and frame budgets;
• absolute deadline; and
• exact child or IRQ work currently awaited.

Only semantic progress may advance the cursor. A notification, empty poll, duplicate completion, scheduler turn, or diagnostic read is not progress.

If the owner can block, it must publish the durable wait condition before sleeping and clear it before interpreting a wake. If it cannot establish a safe wait, fail closed through the sole recovery path.

6.4 Recovery

Recovery is part of the original ownership design, not an alternate driver. Define one recovery state machine that:

• contains an issued or possibly issued operation before reuse;
• preserves the exact first terminal cause;
• invalidates stale readiness and generations;
• quiesces IRQ and DMA ownership;
• returns resources to one known state; and
• either resumes through the canonical initialization path or terminates without claiming readiness.

Do not add a whole-bootstrap retry, root-context fallback, independent polling loop, duplicate interrupt lane, or faster command path to conceal a broken handoff.

7. Use the existing driver patterns

The selected Pi 4 manifests currently declare seven physical runtime roles. The generated manifest snippet is the authority for exact artifacts, resource counts, IRQs, bus links, and affinity. The table below describes only the reusable ownership pattern.

HAL-owned root/runtime control rings and all SHARED payload resources have identical cacheable, execute-never Normal mappings in every CPU participant, including the CYW43/SDIO and USB/PCIe reciprocal aliases. The selected SMP seL4 AArch64 makeUserPagePTE maps Page_Default as inner-shareable Normal memory; Page_Uncached means Device-nGnRnE. CPU communication must not use device attributes merely because a driver consumes the message.

Physical DMA uses separate private DMA resources with no root aliases and retains uncached attributes, as do MMIO and the device-facing framebuffer. SDIO copies shared payloads through its private DMA4 bounce arena; GENET and USB use their private DMA arenas. Firmware mailbox requests also use private DMA pages. Shared physical-address metadata does not authorize DMA to a shared page. Any future device-visible use requires an explicit mapping and cache ownership contract before admission.

Root and child use release/acquire barriers at shared publication and observation boundaries. Preserve volatile/atomic accesses, sequence-last commits, stable rereads and complete range validation. Root must not issue kernel cache-clean/invalidate calls for coherent CPU-sharing ranges; physical DMA and executable-image cache maintenance remain unchanged.

DRIVER_TASK_DMA_PROOF emits cache_policy=coherent-shared-plus-barriers. Its four existing cache_* counters are explicitly zero because CPU-sharing barriers are not cache-maintenance operations. The canonical counter record and seven-row smp activity projection retain their layouts and zero cache-operation fields. These counts do not cover driver-private DMA maintenance or executable loading. The normalizer retains historical uncached-plus-root-maintenance and uncached-plus-root-barriers receipts; both barrier policies require four explicit zero cache counters. Remaining DMA/owner proof requirements are unchanged.

7.1 Serial pattern

• On selected MCS builds, a notification bound to a runtime TCB may satisfy the seL4_NBRecv used to admit a Reply-bearing command. Apply the common badge-first MCS rule in Section 5.3 rather than trusting the notification’s unspecified message length. Route and service exactly one bounded owner quantum, then re-read the still-durable command on a later outer turn without reusing or replacing its Reply object.
• The selected Pi serial transport uses the runtime’s existing four shared pages as two independent generation-bound SPSC rings. Pages zero and one are the root-to-runtime TX ring, pages two and three are the runtime-to-root RX ring, and each two-page ring has a 64-byte header plus exactly 8,128 payload bytes. Do not reinterpret the pages as a common MPMC queue or add a second UART owner.
• Map these CPU-only ring pages with identical cacheable, execute-never Normal memory attributes in root and child. The selected AArch64 seL4 kernel maps Page_Uncached as Device-nGnRnE, which is retained for DMA/MMIO but is not a valid home for the ring’s Rust atomic acquire/release cursors. Device-facing pages require their separate DMA or MMIO mapping contract.
• Publish payload before the producer cursor and consume payload before the consumer cursor. Validate magic, version, direction, generation, capacity, cursor distance, and commit-paired cursors before access; poison and fail closed on an invalid or discontinuous cursor instead of truncating it.
• Treat wakeups as hints around durable ring state. After producing or consuming, perform the final state/epoch recheck required to close the empty-to-nonempty and full-to-not-full races. Root drains the rings through its existing cooperative EventPump polling; the transport does not claim a direct interrupt wake into root.
• While the validated root-to-runtime ring has committed nonzero occupancy, sample MU_STAT before sleeping. If the FIFO has no free slot, block only on the generated local notification in slot 3; if it exposes one through eight free slots, re-enter one bounded owner turn immediately. Admit only the exact serial IRQ badge, root doorbell badge, or their coalesced value; service at most one FIFO quantum, then re-enter the outer command poll before classifying occupancy again. Return to the combined endpoint-and-bound- notification wait at zero. An invalid live cursor or impossible FIFO level poisons the TX ring, disables TX-empty, and makes the TX-idle probe fault instead of selecting either active wait or a fallback owner.
• Keep RX and TX loops bounded by the service contract.
• Interpret the BCM2711 mini-UART IER by the hardware-validated Linux/QEMU mapping: bit 0 enables RX and bit 1 enables TX-empty. The older BCM2835 peripheral PDF labels those two sources in the opposite order, but its published errata swaps bits 1:0; do not copy the original reversal into the BCM2711 runtime. MU_LSR bit 5 proves only that at least one TX byte is admissible; derive the exact zero-through-eight-byte write prefix from MU_STAT[27:24], consume no SPSC byte on an impossible level, and keep TX-empty enabled exactly while committed TX bytes remain.
• For a level-triggered RX source, sample live level even when a notification coalesces, but never exceed the granted byte budget.
• Check queue capacity before reading a data register.
• Preserve an asserted source when the queue or budget is exhausted; drain it through the same child before IRQ acknowledgement. If a full RX ring leaves the combined mini-UART handler unacknowledged, a later software continuation after root drain must retry the same pending IRQ acknowledgement; whether that continuation itself carried an IRQ badge is irrelevant.
• Any source-polled or root-doorbell turn that consumes RX bytes, fills a TX FIFO prefix, or leaves durable RX/TX work must establish the handler-rearm obligation before it can wait. An IRQ badge is evidence of one wake, not the sole authority to restore the level handler after a coalesced edge.
• A terminal linked-serial generation poison aborts only output owned by that failed transport, records one exact SERIAL_TRANSPORT status=failed ... owner-fallback=none diagnostic in the Queen log, and retires the physical response barrier. Later serial RX and local-seat USB parsing remain serviceable, while serial-only output is explicitly retired instead of consuming its bounded queue. Root never resumes MMIO ownership as a fallback; local-seat response text and prompts continue through the existing HDMI mirror.
• Before takeover or steady-state acknowledgement, complete the IER/device writes, read back IER and non-destructive MU_STAT from the same mini-UART aperture, complete that observation, and only then invoke seL4_IRQHandler_Ack. A mask/readback mismatch or failed kernel ACK retains the handler evidence and poisons TX so the child cannot sleep waiting for an interrupt that remains masked.
• Transfer ownership without dropping bytes that arrive at the boundary.
• This transport changes no mini-UART baud, FIFO, IRQ identity, owner, MCS budget/period, response bound, timeout policy, or emergency-fatal exception.
• Treat emergency root serial as degraded diagnostics, not migrated service.

7.2 USB and local-seat pattern

• Separate PCIe prerequisite, controller readiness, device discovery, HID endpoint readiness, first valid report, parser ingress, and echoed command completion. None implies the next.
• Keep exactly one production keyboard interrupt-IN transfer active. Ring capacity is storage capacity, not permission for multiple active transfers.
• Interpret sustained queue diagnostics against that invariant: zero entries is empty, one is healthy, and more than one is a queue-depth fault. A large cumulative transfer count cannot turn the healthy one-deep state into a collapse warning. Use the current no-reply streak for liveness; retain the cumulative no-reply total as telemetry only.
• After attach or recovery, require a decoded all-zero idle report before accepting make transitions; do not turn a held key into a synthetic command.
• Emit every ordinary key once per make/release edge. Only held arrow usages repeat: use the exported virtual counter and selected TIMER_CLOCK_HZ for a 300 ms initial deadline and 50 ms interval. Evaluate a due repeat from the existing steady keyboard turn even when no new HID report arrives; report count is not elapsed time and must not become the repeat clock.
• Represent retained work as typed Pending, Complete, or Failed.
• Keep the fixed 48-byte, pointer-free DriverRuntimeUsbOldgoodReceipt ABI slot at shared-ring offset 192 reserved for compatibility, but do not stage or publish its partial or terminal state from the isolated USB runtime. Root may stable-read and passively project the reserved zero record; that projection grants no admission, scheduling, recovery, or acceptance authority.
• Give enumeration and recovery finite attempt and elapsed-time bounds.
• Expose active, outstanding, and active-without-progress state separately; cached readiness must not hide a retained request that has stopped making progress.
• Count real decoded or buffered input as operator work. Do not let cached readiness or ordinary pending polls starve the network lane.
• Treat a skipped runtime turn after higher-priority physical input as scheduling telemetry, not a transport no-reply. Transport degradation needs explicit failed recovery, no-reply, queue collapse, or dropped-byte evidence.
• A keyboard probe may report attachment only from its live Complete terminal. Cached attachment cannot promote Pending or Failed to success.
• Program HID SET_IDLE with a one-second interval on the existing endpoint lifetime. This gives an unchanged keyboard a bounded way to publish the all-zero attach baseline before the separate five-second exact-transfer watchdog; it does not add a polling path, retry owner, or second transfer.
• Keep USB_RESET_DONE inside the existing bounded extended controller-init and reset timeout class. It is the transition into the following run-stage setup, not permission to fall back to the generic three-resume allowance or to create a new retry lifetime.
• A passive liveness sentinel passes only when the linked runtime, parser ingress, parser drain, and echo counters advance without a dropped-byte increase. A latched startup gate or unchanged cumulative counter is not current physical-input proof.
• A root USB recovery request reflects an earlier status completion. The sole USB owner revalidates it after consuming current reports: a freshly decoded valid idle, release, or held-key report cancels the no-event/full-queue reason even when no command byte is produced. Explicit matched-transfer faults, rearm failures, unmatched events, recovery bounds, and the post-recovery idle-baseline guard remain unchanged. FrameReady.result is a byte count, never a queue/status bitmap or clean-poll proof. The root status cache retains the completion discriminant: only keyboard Progress with first-report ready/pending detail authorizes queue-based recovery, prompt blocking, or clean-poll advancement. A later input frame invalidates that cached queue interpretation without discarding input or its first-byte proof. Enumeration snapshots and Idle/Fault results likewise cannot be decoded as report queues. Missing-reply recovery and real pending/recovery status retain their existing guards. usb: recovery_request includes queue_valid; when it is no, its zero-valued decoded queue fields carry no queue-health evidence.
• Before a current linked-runtime HID byte is accepted, report usb-physical-input-unproven. Gate 10, command readiness, or first-report readiness alone must never be relabelled as first-byte evidence and cannot produce a usb-post-first-byte-* blocker.
• The attach sequence performs PCIe descriptor preparation and owner registration, then USB descriptor replay and runtime initialization. It registers the USB owner once controller init is ready, before enumeration. On a physical Pi profile that marks local-seat required, the deferred CYW43/SDIO supervisor cannot take its first driver turn while that PCIe/USB controller-owner chain is still retained. Its operator phase routes ordinary one-operation EventPump turns until the USB controller owner is ready, then rechecks Wi-Fi admission. While retained bootstrap work remains, a pending display milestone keeps its existing first-turn priority, but distinct non-display turns alternate one bounded linked USB/HID service unit with serial/dispatch service. Network stays fenced throughout this operator rotation, and any USB byte remains buffered for the later serial/dispatch turn. This preserves keyboard-enumeration progress without composing USB and CYW43 hardware operations or allowing either physical console to starve. Once that controller is admitted and ready, controller_ready && !command_ready remains finite bounded LocalSeat debt even before backend keyboard polling is enabled. One existing local-seat turn services that debt, then returns to serial alternation; the debt stops at command readiness. Keyboard command readiness and first-byte proof remain independent downstream USB gates and are not prerequisites for Wi-Fi. A keyboard may be unplugged at boot: controller admission precedes device enumeration, and later keyboard discovery uses the existing bounded service turns. Neither NIC startup nor TCP admission may require a physical keypress. LocalSeat does not add a second proof-scheduling phase after endpoint completion and does not cache a completion or HID bytes while waiting for another descriptor/owner pass. A valid linked input frame follows the existing parser-admission path once, and a valid first-report completion follows the existing command-ready transition. Current hardware acceptance independently requires both USB and PCIe owners to be driver-owned, both descriptors to be sealed, Gate 10, the exact one-deep queue, and real HID/parser/HDMI liveness; endpoint progress alone cannot satisfy those gates. An ordinary pending enumeration retry may retain the existing pre-prompt deferral, but that deferral is not descriptor or owner proof authority.
• Once the physical Pi keyboard is command-ready, keyboard-ready, and has completed its first valid report, a healthy empty linked-runtime poll is due at most once per shared 25-ms real-wall CNTVCT_EL0 cadence. Enumeration or readiness debt, recovery or a no-reply streak, buffered input, and the exact retained request bypass that cadence and remain immediately serviceable. First-byte evidence is deliberately not a readiness prerequisite: an untouched keyboard may have no accepted key byte for its entire lifetime, and making that absence urgent would restore an empty USB child operation on every root rotor. With no generated USB IRQ, the next cadence poll discovers a new report within 25 ms plus its existing bounded MCS scheduling delay; once decoded input is buffered, the immediate gate preserves input priority. Suppressing only the physical child operation changes no LocalSeat, runtime, Dispatch, HDMI, serial, owner, queue, retry, or MCS topology.
• Treat local HDMI readiness independently from WiFi or GENET readiness. Queue Cohesix console ready only after root and current USB command admission, and withhold the interactive prompt until that exact banner frame completes and display retry health holds. Before that boundary, project bounded controller, keyboard-enumeration, and first-report feedback through the existing EventPump output path. Emit stage changes immediately and an unchanged-stage heartbeat no more often than every two seconds. Retain the bounded canonical [local-seat] usb keyboard command-ready action=enable-command-input ... receipt exactly once in queen.log; its counter detail remains log-only. EventPump is the sole serial projector and emits that canonical receipt exactly once immediately before the passive [drivers] USB console ready timing record through the existing HighImpact output path. The pair may follow prompt release and grants no scheduling authority.
• Keep the canonical prompt/input row dirty until its matching generation receipt completes. Older FIFO output stays before that row, later output stays after it, and backspace cannot erase bytes at or before the prompt floor. An older display completion cannot acknowledge newer input.
• If an arrow arrives at the live tail while ordinary HDMI output remains pending, seal that finite prefix, drain it under generation and logical-tail receipt identity, and only then apply the bounded CSI scroll. Output queued later stays behind the fence. Identity drift, wrap, eviction, or unavailable history requests one canonical snapshot; none of these presentation paths resets or reinitializes xHCI.
• If USB command readiness is invalidated, retract the prompt and stale console-ready banner without discarding the typed suffix. Re-admit them only from fresh readiness; a stale retraction receipt cannot clear the restored row.

7.3 HDMI pattern

• Map framebuffer pages into the display child without a steady root VSpace alias.
• A boot without a firmware framebuffer has no runnable new display work. Root preserves bounded display history and any retained command completion, but does not retry display attachment, admit nonessential network mirroring, or fence event-driven idle on output that cannot render. Serial and USB input remain independent. Connecting a display later cannot create missing boot mapping authority; reboot with the display connected to exercise rendering.
• After the immutable framebuffer range, format, alignment, pitch, and geometry are admitted, the child begins takeover with one fixed two-line startup tile in the safe area: Cohesix starting... followed by Initializing services.... It validates both complete glyph rows before the first store and issues one device-store barrier after the bounded raster. This is early physical progress only: it grants no root alias, prompt, USB readiness or mailbox/HVS authority. The same immutable init command then clears the surrounding boot background through the retained frame cursor, using the existing format- and budget-scaled row bound (at most 80 physical rows per turn). It preserves every tile pixel and publishes init completion only after the full surface is cleared. This starts with the banner instead of waiting for USB or the first ordinary frame, and never blanks the screen before the banner. Invalid geometry performs zero stores. The first ordinary generation-bound frame still clears and replaces the tile through its existing takeover path.
• Before terminal takeover, a canonical empty HDMI SubmitFrame (fixed ring offset, HDMI role, zero auxiliaries/frame flags and exact generated budget) may refresh only the second tile row after two seconds in exported CNTVCT time. The fixed-width status is Initializing... 00002s, padded to erase the preceding row; elapsed seconds saturate at 99999. Missed periods coalesce into one raster, with full span admission before any store and one completion barrier. The command returns Progress with the rendered cell count only when it draws, otherwise the existing Idle. First ordinary frame admission disables these refreshes permanently, before any retained clear. Root offers the empty command at quiescent bootstrap checkpoints, at most every two elapsed seconds, through the existing synchronous command/Reply transport; it adds no timer or device authority. Pre-release UART cutover gives input and response tails priority and consumes a separate outer turn for a due display poll. After cutover, the ordinary dedicated Display phase retains one empty command across bounded service turns; serial handoff does not stop the counter at six seconds. It can continue through eight and ten seconds while the tile remains visible. USB/serial keep their intervening operator turns. A normal frame first waits for any retained empty command to retire, then disables further polls and takes over immediately; readiness is never delayed to reach a counter value. Physical cadence is bounded by the next safe checkpoint and scheduling; hardware must verify the requested visible two-second cadence. Early HAL PCIe settle waits offer a checkpoint after each bounded chunk of 50,000 original spin iterations. Every original iteration and flushed MMIO ordering remains; the chunk is not an elapsed-time clock or a shortened hardware deadline. Only the existing CNTVCT guard decides when to draw. These calls hold no driver Reply or display ticket and add no HAL reentry.
• Keep terminal state in a fixed child-private cell plane. The current Pi renderer admits at most 256 columns by 128 rows, uses a logical row ring for scrolling, and records visible damage in a fixed bitmap. Retain a generation-bound parser cursor so each immutable input byte is consumed at most once across as many bounded turns as required, coalesce the final cell values, and rasterize only dirty glyph bands. A tab advances to the next eight-column stop by exactly 1 through 8 cells, including eight cells when the cursor is already aligned. Never read live scanout to implement terminal scroll or redraw.
• On the physical Pi MCS profile only, the canonical one-way HDMI-text SubmitFrame command selects retained scheduler mask zero: exact HDMI contract and hot-path role, generated budget, zero auxiliaries, fixed frame offset, nonzero in-bound payload, and zero frame flags are all required. HDMI already owns its generated active scheduling context and has no separately scheduled bus owner, so one fresh request may fuse only the hardware-free Stage through sequence-last CommitRing transition. Endpoint notification remains the next outer turn, and completion polling and retirement remain a later outer turn. An exact completion advances directly from Issued to ReadyToComplete; it does not manufacture classic priority-boost or restore phases that cannot change MCS state. Any command, request, endpoint, ring, fingerprint, retained-lease, or committed-record identity drift fails closed before notification. This lane changes no scheduling budget, payload limit, raster operation, USB path, bus ownership, physical-operation cardinality, or QEMU behavior.
• Admit the framebuffer before rendering: the format must be RGB888 or XRGB8888, the visible area must contain a complete 8-by-16 cell, row bytes must fit the pitch, the declared framebuffer range must cover pitch * height, and XRGB8888 virtual address and pitch must be 32-bit aligned. Reject unsupported, partial-cell, oversized, truncated, or misaligned geometry rather than constructing an alternate renderer.
• Bound parsing, every wide logical-plane operation, first-takeover or form-feed clear, dirty raster, frame, and refresh work as resumable retained phases of the exact command generation. Do not advance to a later input byte until the current byte’s clear, scroll, tab, or other multi-cell effect is completely staged. Completion is published only after the final device-store barrier. The selected Pi profile reserves 2,000 us per unchanged 10,000 us period; its 1,800 us candidate WCET is a static-admission input, not measured Pi timing evidence. Store and cell ceilings scale from the generated reservation and are not an unbounded refresh loop.
• Bind every submitted frame to the shared HDMI HAL grant of exactly 1,280 dirty-cell operations, a 4,096-byte parser envelope, and 80 physical clear rows per retained turn. The unchanged pointer-free frame transport admits at most 1,536 payload bytes; 4,096 is a pure parser/grant ceiling, not a widened single-frame ABI. Reject zero, narrower, broader, or byte-insufficient frame grants before mutating the cell plane or scanout, and still cap the clear/raster implementation to the admitted fields so contract drift cannot silently widen a later turn.
• Distinguish queue acceptance from completed rendering. A ready receipt needs a completed display-runtime turn with no outstanding submission or exhausted retry; mirroring or queueing a line is insufficient.
• Bind current outstanding status to the display driver’s active request. An inactive submitted/completed counter gap remains cumulative timeout telemetry and cannot fabricate live display work. Passive acceptance requires the adjacent current hdmi: driver record with present counters, no active request, at least one completion, no no-reply streak, and no stale snapshot.
• Once a snapshot establishes the viewport, held arrows chase the requested history offset by one completed CSI S/T row per bounded display turn. Before rotating the logical row origin, retain bounded damage for the union of each old and new visible row’s nonblank columns, then clear only the newly exposed row or rows without adding redundant damage. Existing dirty cells remain ordered through the rotation. A scroll count at least as large as the viewport clears the text area while preserving the cursor. Reserve full redraw for initial materialization or recovery; do not restart it for every repeat or grow an unbounded queue.
• Allow display mirroring and redraw to degrade before serial or keyboard command liveness.
• On the deferred WiFi path, a newly accepted partial local-seat line schedules exactly one bounded Dispatch -> Display -> Serial presentation successor before Network while retaining the immutable CYW43 parent and operator fence. A reboot acknowledgement or owned physical-response tail keeps immediate Serial priority and leaves the echo queued. This ordering changes neither USB byte ownership nor HDMI’s one-command raster bounds.
• The write-only compositor does not authorize BCM DMA, mailbox/HVS ownership, a cacheable or second scanout alias, or a second framebuffer owner. Host compositor tests and target compilation can reject a candidate, but only a fresh exact-image Pi run can establish visible correctness, latency, and operator polish.
• These local-seat rules change no console grammar, physical owner, poller, retry path, or scheduling authority. The reserved fixed USB old-good slot and root projection are passive compatibility diagnostics; runtime publication is dormant. USB remains the sole xHCI/HID owner and HDMI remains the child-only framebuffer renderer.

7.4 Network-device pattern

• Expose the common network trait; keep controller and firmware details inside the driver boundary.
• The selected Pi profile binds GENET default queue 16 to the exact resolved seL4 IRQ 189 from the first ethernet@7d580000 DTS interrupt. The second line belongs to priority queues 0 through 15 and is not admitted. Runtime code must consume the generated identity and badge 1024 and must not infer a GIC offset. Non-Pi/QEMU profiles retain their existing three-IRQ declaration; the Pi-only interrupt must not leak into them.
• GENET packet completion is child-owned and IRQ-driven. One DPC turn drains at most 16 frames and 24,576 bytes into a fixed 16-frame private queue, then completes the device-store/unmask readback before its final source and ring recheck. A remaining exact IRQ lifetime stays masked and unacknowledged. An exact IRQ badge starts the ordinary lifetime; after direct ownership, an already-admitted owner/peer turn or final condition-before-sleep cut may join a raw owned interrupt level or advanced DMA index to that same sole-owner episode, then uses the existing mask, clear, bounded drain, unmask/readback, final raw-plus-index recheck, and exact handler rearm. Software-ring state, badge zero by itself, a timer, or an unadmitted poll cannot create an episode. dpc_level_adoptions counts those physical-level joins only; it grants no packet, polling, retry, acknowledgement, or recovery authority. Handler-ack or unmask-readback failure disables the runtime without retry.
• Before an admitted GENET RX command reports idle, the same sole owner also compares the durable RDMA producer with its consumer and may drain only the command’s existing operation, frame, and byte grant. This condition check cannot create or acknowledge an unseen IRQ lifetime, add a timer poller, or introduce a second DMA consumer; it prevents a coalesced notification from hiding already-produced frames while the IRQ DPC remains the eager path. Packed completion bit 30 is the cumulative, passive command_rx_drain_seen proof for that route and is exposed as runtime_cmd_drain_seen=0|1 on the existing netstats: genet_rxq row. It is set only after an admitted command successfully queues at least one durable frame; it grants no polling, IRQ, acknowledgement, DMA, or retry authority.
• GENET TX reclaim detail is a completion delta, not a sampled level. An IRQ or DPC may accumulate newly reclaimed descriptors until the next root command completion with a reclaim field consumes that aggregate exactly once. A budget-exhausted completion cannot discard it, a later zero-reclaim poll cannot erase it, and a later eligible command cannot report it again. The cumulative completion count cannot exceed submissions, while tx_free + tx_in_flight remains the fixed 32-descriptor active ring.
• QEMU direct-VirtIO retains its strict isolated lower rotor: ObserveChild, StageOutput, Disconnect, then ServiceTick. Direct GENET alone selects an exactly ready StageOutput first, then an exactly ready Disconnect; with neither ready it alternates the only blind root responsibilities, ObserveChild and ServiceTick, one unit per Network visit. After the first direct-GENET Network visit observes exactly one accepted authenticated command, the existing five-unit Pi quantum may run Serial -> LocalSeat -> Dispatch -> Network, replacing only optional Display with one exact response-stage unit. The direct child’s generation- and connection-bound response lane already retains the response through ControlCompleted plus OutputDrained, so it creates no legacy TCP flush cursor. Display remains the next debt. Stale or mismatched generation, connection, authentication, or runtime identity fails closed to the bounded legacy cursor; saturation, physical response, quarantine, containment, recovery, reboot, or no progress denies the causal fifth unit. This cannot compose a child lower-unit burst, increase a manifest or MCS budget, skip physical-input priority, create a poller, or grant NIC/child authority.
• CYW43 retains its connection-bound post-dispatch flush cursor because its ordinary smoltcp path has no isolated OutputDrained proof. The normal TX service opportunity precedes smoltcp. If the following cursor flush accepts exactly one current-generation response frame for the same nonzero active authenticated connection, and the turn has not spent its sole CYW43 operation, it may use the remaining ordinary DriverServiceBudget for one immediate op7 service call. Any prior operation, zero/multiple/saturated acceptance, identity drift, physical operator work, recovery, containment, quarantine, or reboot denies it. The existing outer-operation claim still limits the complete Network turn to one physical operation, and the 8/16 cursor bound remains unchanged.
• Prioritize ARP and TCP/ICMP control traffic, but after four consecutive control frames service the oldest data frame so control load cannot starve data. Batch drain and root consumption remain independently bounded.
• Physical GENET descriptors and DMA buffers remain private, uncached, and solely owned by the GENET child. After DHCP and an exact proof that every root-mediated GENET command, RX, and TX cursor is quiescent, root may perform the one-way generation-bound direct-data-plane handoff. It then reuses the existing 32 shared pages as CPU-only cacheable Normal/XN memory: page 0 is the control page, pages 1 through 15 are GENET-to-console RX slots, and pages 16 through 31 are console-to-GENET TX slots. Those pages have no device-visible, DMA, or physical-address authority and map only into the two child generations. GENET remains the sole MMIO/DMA/IRQ owner and console-network remains the sole smoltcp/TCP/auth owner.
• Each direction is a single-producer/single-consumer sequence-last ring with bounded frames, monotonic cursors, exact generation/length validation, and a final durable-state recheck before waiting. Fixed-badge peer notifications are coalescing hints only. The root publishes the exact generation as handoff-pending before issuing DGHO. While that phase is unfaulted, only the bounded legacy drain may run; a DGHO retry waits for its coordinator and root RX/TX queues to become empty. READY atomically removes the pending phase, while a fault at any earlier or later interleaving latches coupled containment. An invalid sequence, stale generation, corruption, descriptor drift, failed handoff terminal, IRQ unmask/acknowledgement failure, or peer fault poisons the link, signals the peer, and fails through the standard supervisor endpoint; root packet polling, copying, and packet-command service never resume as a fallback. Before its standard fault, console-network independently poisons its RX-consumer and TX-producer lines and signals the GENET peer; a reciprocal-line race cannot suppress either valid owned poison. Console containment unmaps and deletes every copied external frame cap before revoking the console anchor, while driver containment owns the original page generation.
• DGHO may publish READY only after a finite legacy interrupt/completion epoch. A quiet Ethernet wire is not a synchronization condition. The GENET child masks the admitted source, stops MAC RX, waits 10 ms in the generated CNTVCT domain for accepted pipeline work, clears only RDMA DMA_EN while retaining the default-ring enable and configuration, and requires DMA status bit 0 to report disabled within 5 ms. Only then does it snapshot the immutable producer frontier. Root may drain that finite legacy frontier, private RX, TX reclaim, pending direct cursor commits, and every retained handler lifetime while the source and ingress remain stopped. Producer movement, a cursor distance beyond the 32-descriptor hardware ring, generation/token drift, failed stop/readback, or timeout faults the pair and leaves MAC RX, RDMA, TDMA, and IRQ sources contained. While stopped and before publishing the direct generation, the child unconditionally acknowledges the exact admitted IRQHandler once at this finite empty ownership boundary. This closes a queued-but-unobserved legacy notification lifetime before RDMA, MAC RX, and the exact source resume in that order with readback. An ACK failure faults before READY. The boundary ACK grants no packet work, does not fabricate an IRQ wake, and cannot recur as a poller; durable DMA and direct ring cursors remain the only post-cutover service authority. A queued exact seL4 IRQ notification received after READY belongs to the same sole owner and is serviced as direct-epoch work.
• Direct GENET admits exactly one material packet operation per MCS-accounted DPC slice. Successive slices alternate the first TX/RX choice; an empty side donates its slice, while continuous bidirectional pressure receives exactly eight TX and eight RX slices in the retained 16-slice window. Finalizing a retained ambiguous TX or RX cursor commit consumes one of those slices and cannot be reconciled outside the same accounting. Recycling a malformed RX descriptor also consumes its slice and cannot donate that same slice to TX. A full TX ring waits for a peer rearm notification unless an independent retained cursor transition is actionable; queued RX cannot create a self-poll while smoltcp ingress is occupied. The Pi manifest gives GENET a 3,000 us / 10,000 us core-1 SC, priority 160, eight refill records in its existing 8-bit SC, exact 800 us WCET, natural-postpone policy, and a 3,400 us computed response bound. Legal sustained packet work remains hard capped by that reservation and is postponed until replenishment rather than quarantined as a device failure. Standard faults, explicit device deadlines, direct-ring/cursor faults, and pair containment remain terminal. These static bounds require fresh Pi consumed-time, latency, and throughput evidence.
• A diagnostic-only queue/receive observation binds the longest data-bearing TCP packet handoff to its producer’s completed Signal and consumer’s last completed Recv/Wait/ReplyRecv plus the last explicit GENET Yield and its existing route reason. It uses optional sequence-last page tails and generated CNTVCT timing; no new syscall, sleep, poll, queue, driver owner, scheduling context or retry is introduced. Missing or raced observations cannot affect packet acceptance. Root reads the consumer-owned peak only during requested diagnostics. INTERFACES.md defines the v3 record and unavailable semantics; fresh Pi evidence must distinguish publication, notification, receive return and post-return work before any policy change.
• In direct mode the owner retains one dense software episode only while exact durable work remains. A Reenter successor stays inside the same notification or final-prewait handler, so generic command arbitration cannot consume unguarded time between packet slices. The owner samples the elapsed MCS guard around every slice and yields at half of its 3,000 us budget or 16 attempted slices only while durable successor work remains. A final slice that proves the rings empty and the source rearmed blocks before the guard/cap/stalled Yield decision and closes only the userspace episode’s start, attempt, and stalled-retry state. A later real IRQ or reciprocal peer wake starts a new software episode on the same unchanged kernel SC; it does not manufacture a refill. A successor that first crosses the guard yields and returns to outer arbitration rather than beginning another activation inside the handler. Only TX issue, resolved reconciliation, RX publish, or malformed-descriptor recycle that advances owned state is productive; a peer wake, IRQ ACK, or unresolved cursor race cannot extend the window even though reconciliation still consumes its fair slice. One no-progress durable recheck is permitted; a second yields. Any endpoint command marks the shared SC consumption stale and forces a fresh-refill boundary before more packet work, and quiescent episode closure cannot clear that independent requirement. The compiler and generated profile require exact wcet_us=800; the handoff and runtime validate the exact 3,000/10,000 us, max-eight-refill contract. A missing/backwards counter, repeated non-advancing slice, contract drift, or invalid cursor fails closed. The kernel SC remains the sole CPU authority; continuously durable work never resets its guard, cap, or stalled boundary.
• Direct GENET copies descriptor-admitted uncached RX/TX payloads with aligned volatile 64-bit accesses plus bounded byte prefixes and tails. The source and destination range, frame length, cursor, and DMA slot remain validated before mutation; descriptor publication, cache/barrier ordering, and sequence-last direct-ring commits are unchanged. This reduces the per-frame volatile-copy operation count without widening a DMA mapping or moving device authority.
• Direct-link control page 0 reserves bytes [0,64) for its immutable header and [64,320) for the four 64-byte SPSC cursor records. The optional direct-GENET diagnostic-v6 record occupies the formerly reserved bytes [320,640), is exactly 320 bytes and cache-line aligned, and commits its publication sequence last at record offset 312. Version 6 retains offset 12 to the maximum observed bounded packet-slice duration and retains offset 108 for cumulative dpc_level_adoptions, the number of badge-zero or peer-turn joins of durable physical work to a direct IRQ episode. Offsets 160, 168, and 176 contain cumulative nonzero raw notification receipts, receipts rejected by the exact GENET route filter, and their 32-bit badge union. MCS reason bits record command-freshness, elapsed guard, counter fault, attempt cap, and stalled-retry boundaries. They are counted at the actual receive boundary before filtering and are observational only: they cannot service or acknowledge an IRQ, admit a DPC or packet, retry, or change scheduling. Count each nonzero notification once at the initial ring-aware receive or a later combined poll/wait receive; exclude zero/command wakes, synthetic grants, physical-level adoption, and unrelated local steady waits. GENET is its sole writer; root accepts it only through a stable double-read with exact nonzero direct generation, magic, version, length, flags, cursor validity, counter relations, badge width, and matching sequence/commit. Missing, torn, stale, wrong-generation, or malformed data is unavailable diagnostic evidence, not a reason to change packet, IRQ, retry, recovery, or containment behavior. Ordinary packet turns do not scan the record, and page bytes [640,4096) remain reserved, zeroed at construction, and scrubbed at containment.
• Diagnostic v6 includes one 128-byte maximum-slice receipt at record offset
  1. Its ordered counter samples separate source/reclaim, packet work, IRQ work and final durable checking; a confirmed RX publication precedes peer signalling and DMA rearm. Three formerly reserved words retain Signal entry, Signal return and completion of RX descriptor/index retirement, with an exact notification-due flag. When no notification is due, Signal samples are absent. All intervals remain inside packet elapsed time; no syscall, DMA retirement or guard moves to obtain a smaller maximum. The owner samples only a bounded header while that exact DMA slot still awaits rearm. A TX receipt uses the existing stable private frame. Direction, cursor and a validated IPv4/TCP tuple permit exact packet correlation without retaining payload. Invalid samples are discarded without affecting scheduling or service. Elapsed time includes descheduling and kernel time; neither a maximum nor its tuple proves wire arrival or SC consumption. Record publication remains restricted to diagnostic replay.
• One operator diagnostic may request one idempotent, exact-generation DGHO replay so the sole GENET owner publishes that record. Retain both the stable pre-replay snapshot and the replacement sampled before normal post-command idle service. This is a bounded causal probe, not a passive read: waking the owner can permit the existing idle path to drain durable RX. It cannot recur, admit a packet, acknowledge an IRQ, retry a command, recover a peer, create a poller, or satisfy traffic, latency, throughput, or acceptance evidence.
• Bound RX admission, TX submission, completion reclaim, and queue depth per turn.
• Preserve packet order unless a documented priority policy explicitly selects another frame.
• Treat link, address configuration, ARP, TCP, console response, throughput, and latency as separate evidence gates.
• Use a same-stack known-good device as a control when localizing a physical driver failure, but never use the control device as proof for the driver under test.

7.5 Linked SDIO/CYW43 pattern

Pi CYW43 RX-batch rejection diagnostics retain only the first failed terminal selection’s original double-read queue/header operands. The last pair from three existing queue attempts is retained for a rejection. A same-generation, internally valid queue body with a zero or changing commit is publication in progress, not a rejected batch. HAL keeps the exact op8 request active until both queue cuts and the complete terminal envelope/header validate, using the ticket’s existing finite deadline. One exact, consumable root receipt carries that validation through priority restoration and terminal retirement to the immediate payload consumer. Every frame retains both immutable header checks around its bounded copy; restart clears the receipt before sequence reuse. For op11 sideband batches, root defers before copying and leaves the ACK absent. After successful admission and copy, the still-issued parent and unchanged batch header protect the ACK; independent queue publication cannot retroactively invalidate delivery or cause a duplicate copy. Unavailable, malformed, poisoned and stale records still fail closed. The owner retains all validation, cache barriers, parent/generation fences and restart authority. The record survives recovery scrub and retires at accepted Gate 8. Explicit wifi dump-state exports eleven bounded metadata-only rows defined in USERLAND_AND_CLI.md; no frame payload is captured.

This is the reference pattern for two logical runtimes sharing one physical transport:

• SDIO is the sole physical issuer of controller, CMD52, CMD53, DMA, and card interrupt operations.
• CYW43 owns Wi-Fi firmware, control, and data semantics but requests physical SDIO work through the generated link.
• One parent identity remains bound through every child action and the final consumer receipt.
• Firmware staging borrows the existing replay transaction once per bounded payload copy, preserving sealed-parent and overlay precedence for every byte. Full baseline snapshots, replay order, saved overlapping input and partial flush offsets remain authoritative. Restoring the immutable parent aperture and flushing staged firmware may use the existing aligned volatile word stores only within one validated contiguous mapping; prefixes, suffixes and mapping seams retain byte stores. This changes copy work, not SDIO command shape, firmware bytes, physical waits, replay identity or recovery.
• A nonforeground bus-link payload copy validates both complete ranges before mutation, computes batching from the actual mapped virtual addresses, and uses naturally aligned parent words plus paired aligned owner words when the mappings share alignment. It otherwise uses the existing physical byte primitives without consulting foreground transaction state per byte. The copy cannot cross the runtime ring/shared-buffer mapping seam. Owner reads retain invalidate-before-copy ordering and owner writes retain the store barrier plus clean-after-copy ordering. Foreground sealed-parent, trace, and overlay authority is unchanged; range, length, or cursor drift fails closed without a fallback issuer.
• The event ring, command ring, child terminal, parent terminal, notification, and consumer receipt are distinct states.
• IRQ/DPC work is condition-driven and bounded. Empty polling must not become the transport clock.
• Retained CYW43/SDIO exact-grant admission may fuse no more than three pure local bookkeeping states before one existing physical-owner quantum. Source arbitration runs first. Service is a hard stop before a grant read; otherwise exactly one stable grant read is allowed. Empty alone permits one condition-before-sleep recheck, Inactive fails closed with no recheck, and Ready must revalidate and acknowledge the exact immutable grant before returning authority for one bounded physical quantum. Both root-owned and delegated CYW43-to-SDIO ACKs publish the high-bit admitted value; the runtime replaces it with the exact low-domain ID and signals the corresponding producer only after the one bounded arbitration or physical action ends. A producer cannot publish a successor while the admitted value remains. A failed ACK restores the complete pre-grant gate, including coalesced wake state, and performs zero device I/O. The fused helper performs no device operation itself. It removes scheduler edges between CheckWake, CheckGrant, and the final local admission decision. For generation-bound CYW43/SDIO only, it also intentionally supersedes the earlier source-level postphysical seL4_Yield: selected MCS charges that call’s complete remaining head refill, so the same child immediately re-enters exact-grant admission and blocks on the existing local notification when no fresh identity-matched grant exists. One physical operation or finalizer per exact fresh grant, producer/root reconciliation, every external-condition wait, owner, deadline, retry, fault/Reply rule, and MCS numeric remain unchanged. A consumed old grant performs no ACK or I/O; ambiguous, rejected, Reply-bearing, unsupported, and other-driver routes fail closed or retain their prior scheduler handoff and cannot fall back into this lane.
• Exact-743e proved that a sequence-last CYW43-to-SDIO command could remain durable behind an action-admitted outer grant while the equal-priority SDIO owner received no runnable observation. At the final retained foreground or DPC root-causal cut, CYW43 must therefore re-observe the durable peer frontier. Only a nonzero exact child sequence still in Waiting on the Cyw43Client route may execute one MCS seL4_NBSendWait: its nonblocking send uses generated send-only slot 8 to prompt SDIO, and its atomic wait uses CYW43’s bound read-only local-notification slot 3. The durable command/grant record, not either badge, remains authority. An unrelated wake may re-prompt that same command but cannot create another command, retry, physical operation, poller, or owner. Returned, Recovery, Invalid, wrong-route, zero-sequence, and post-wake identity drift perform no combined wait and select the existing fail-closed path. This atomic peer prompt is MCS-only. A classic non-MCS profile retains its prior slot-3 local-notification wait-only behavior and sends no additional slot-8 SDIO signal; unrelated runtime waits retain their existing syscall selection.
• An exact fresh foreground publication closes the earlier scheduling discontinuity at the command commit itself. Before committing the nonzero sequence-last value, CYW43 captures the executing turn, immutable parent, child and generation, healthy publication environment, exact Cyw43Client route, stable Waiting completion, and absence of issued-unknown, pair restart, or live recovery. This includes ordinary cold HOST_CONFIG as well as the previously admitted persistent exchange. After commit and the required sequence cache clean, selected MCS performs no passive read, progress publication, or semantic work before one seL4_NBSendWait prompts slot 8 and parks on slot 3. When that syscall returns, CYW43 re-proves the same sequence-last child and enters one condition-driven publication episode. A rejected publication retains its first failed predicate for the pair lifetime. Restart progress phase 446 is refined to 470..479 for route, local state, causal identity, environment, command, descriptor, grant, completion, first-action receipt, or unavailable wait respectively. The existing CYW43_COMMAND_AUX route marker, sequence, record layout, and restart latch remain unchanged. Root recognizes these bounded refinements as the same fail-closed restart and prints their names; later generic restart markers cannot erase the first rejection. The diagnostic adds no success-path publication, retry, scheduling permission, or device action, and resets only with the canonical pair runtime reset. A stable Waiting child without its exact first-action receipt parks again on the existing slot-3 notification; it never sends slot 8 again. Every returned badge is only a reason to re-read the exact child, generation, immutable command, matching terminal, aliased no-grant progress record, recovery fences, and unchanged absolute child timeout. An ordinary delegated child accepts only strict DRSP1 because slice two requires root’s later grant; an exact steady or persistent autonomous child accepts any committed monotonic slice above zero because it has no grant phase and may advance before CYW43 observes owner intake. That exact receipt or an exact terminal closes the episode; issued-unknown, pair restart, or the suppression-only recovery latch returns to canonical recovery; a mixed marker, aliased grant, identity drift, or malformed progress fails closed. An expired unchanged absolute timeout performs the existing late-terminal fence and enters the existing issued-unknown recovery path. It does not count wakes, extend a deadline, or add a retry. This event-driven condition-before-block episode covers any number of coalesced root or stale child badges that could otherwise return before the equal-priority SDIO owner runs, without adding a resend, polling cadence, spin, budget, owner, or second physical operation. A reserved-root bit is routed only through the existing immutable-arm, physical-lifetime, child-sequence, and expiry classifier before it may prompt the sole SDIO owner. Classic and every inexact, stale, replaced, recovery, or wrong-route publication perform the existing single slot-8 signal instead; they do not inherit the atomic park. Only canonical pair recovery clears the suppression latch. On either SDIO notification-return path, a valid peer badge causes an immediate stable read and local seal of the fresh one-way command before wake diagnostics, source service, or an outer-loop boundary. A coalesced physical IRQ still wins the physical action; the sealed command remains pending. SDIO remains the sole issuer and must independently validate the same immutable command and generation before touching hardware.
• A generic CYW43/SDIO notification-source pass under MCS does not call seL4_Yield merely because the runtime has that role. Source priority still consumes a separate bounded arbitration pass, retains any sealed command, and returns through ordinary immutable command/grant and recovery checks. This also covers a coalesced source after an atomic terminal handoff. NaturalPostpone remains the CPU bound; charging the remaining head after an empty or stale source is unnecessary. Classic cooperative behavior, GENET’s guarded DPC window, explicit retained-grant recovery/failure yields, physical operation limits, deadlines and sole-owner authority are unchanged. Fresh Pi evidence must measure the effect on the observed near-period CYW43/SDIO handoff delays; source inspection alone is not throughput proof.
• Within one CYW43 root-granted foreground turn, observing and consuming one exact successful SDIO child terminal under a sealed finite cold parent does not consume that turn’s sole new-submission slot. The admitted cold set is transport init, firmware prep, firmware chunk, NVRAM chunk/tail, and release; a zero-payload parent also requires zero descriptor and retained payload identity. After continuing from that exact accepted result, the runtime may publish at most one following immutable child command in that same turn. This exact-terminal exception applies after either retained source-service entry. With no command Reply, no in-flight root/delegated action, no watermark fault and remaining successor capacity, successful retirement skips the old retained-admission block and reaches the existing command body. It must not fall into the now-inactive gate’s Yield guard. A missing or rejected terminal retains the original source-service Yield; source arbitration and the independent 64-successor cap remain unchanged. The new submission consumes the slot; a second new command is forbidden. Fault terminals, every control, RX, steady, persistent, or other non-cold parent, a still-pending child, issued-unknown state, identity or generation drift, invalid replay, watermark fault, pair restart, recovery, or a previously consumed slot admits no new child and preserves the existing typed recovery/containment path. This removes one scheduler edge at a successful completion-to-next-child boundary without granting CYW43 physical-issuer authority, changing SDIO’s one-operation-per-command rule, or adding autonomous firmware progress.
• The deferred physical WiFi supervisor may retain root-control through strict Operator/Driver alternation only when generated root truth is active, admitted, consumed-time capable, and selects NaturalPostpone. Kernel budget exhaustion then postpones and resumes the exact instruction cursor instead of requiring userland to forfeit the remaining refill at a wall-time budget_us - wcet_us guess. Every full Operator, Driver, and attached Network service turn spends one of the unchanged 64 logical material-work units; productive Driver or attached Network progress also remains capped at 64. Check the generated profile and cap before each fresh phase and retire the exact one-operation outer lease before re-entry. After child Ready, an attached EventPump turn may retain the window after actual CYW43 Network activity and exactly one service-unit advance. The ordinary case still requires an immediate Network successor with durable schedulable work. A still-active authenticated response cursor may instead cross exactly Network -> Serial -> LocalSeat -> Dispatch -> Network when its connection, cursor decrement, service/flush counters, accepted-command count, and generation/pair/lifetime rotation token all remain exact. That rotation admits LocalSeat exactly once, clears its token at Dispatch, and admits only the next separately charged Network turn after the caller rechecks the NaturalPostpone profile and 64-unit caps. Real physical input or response, terminal return, identity drift, recovery, quarantine, containment, or reboot denies the continuation. Invalid generated policy, idle, no progress, handoff, output pressure, fault, or terminal state yields and resets; invalid evidence permits only one legacy logical turn. The window replaces, rather than composes with, the earlier four-Driver restart burst and changes no device deadline, operation cardinality, owner, or QEMU/generic path.
• When the selected physical Pi MCS root-control task is in the exact direct-GENET or ready WiFi topology, the compiler-owned root-control fan-in is bound to the init root-control TCB when that TCB’s temporal runtime is activated. Descriptor replay leaves the PCIe-owned timer disarmed in every mode. After a completed empty quantum, the physical-network global-idle exit consumes exactly one nonblocking multiplexed receive. If that receive is empty, root rechecks timer, endpoint, serial/local-seat/display, network, fault, recovery, containment, quarantine, and reboot state. At the first complete pre-enable idle fence only, root synchronously issues the Reply-bearing typed timer-enable Call, requires its matching completion and durable identity-bound Enabled publication, then repeats the complete idle fence before it may block on the root-control endpoint with that Reply object. Later idle entries observe Enabled and do not issue another programming operation. The bound notification and endpoint are therefore one kernel-atomic receive domain: a fan-in badge is only a coalescing hint, while an endpoint message is copied into root-owned staged storage before the IPC buffer can be reused. A wake always returns to operator/recovery-first arbitration and fresh durable producer reads. Consuming the one-shot nonblocking hint does not revoke a later blocking idle cut after another complete empty quantum: the full predicate is rechecked, routine empty USB service debt remains governed by C3, and only real operator input retains the operator fence. A persistent Retry still reaches the existing Yield instead of forming a poll loop. After a completed response, a fresh unconsumed child publication may instead admit one separately charged Serial-first recheck under the existing lane, operator, recovery and shared work-cap fences. The old response token is retired; a failed recheck cannot rearm itself. Reserve, operator, recovery, fault, and other fenced exits retain their explicit handoff; no future network request, badge, or elapsed interval is inferred. Ready WiFi can use the same timer-backed idle receive only when its physical one-way owner is Idle and every operator, output, child and recovery fence is empty. Retained commands and root-polled deadlines forbid this path; their existing causal waits remain separate. A retained WiFi parent may use its causal wait with root-polled deadline debt only after the same exact PCIe timer lifetime is live. Root polls its absolute timer before and after enable, then rechecks physical completion, child publication and operator/fault/recovery fences. Each wake returns to the existing parent-deadline observation without renewing activation caps. QEMU and classic profiles retain their selected paths.
• The existing isolated pcie-root runtime owns one additional, separately tagged Pi BCM system-timer channel-3 duty to make the global idle receive and retained WiFi parent wait deadline-complete. Its ten-page PCIe host aperture remains contiguous and separately tagged. Page eleven maps only physical 0xFE003000; level IRQ 99 uses badge 2048, handler slot 4, and the runtime’s local notification slot
  1. Because that page precedes root’s mailbox/watchdog mappings in the same monotonic device-untyped region, HAL pre-admits it as an unmapped child-only capability before any higher Pi MMIO in every network mode. WiFi admits the timer before its likewise child-only DMA page; wired and disabled modes admit only the timer. pcie-root consumes that retained capability through the exclusive child-VSpace path, leaving no root alias. Descriptor adoption publishes an identity-bound Disarmed state and does not program C3. Only the first exact physical-network synchronous enable programs C3 at 5,000 us, exactly half its unchanged generated 10,000-us period, and publishes Enabled; WiFi requires its owner-idle fence before enabling. One IRQ service clears the source, reads CLO, arms the next compare, orders and reads back the device state, signals the existing root fan-in, and acknowledges the IRQ. It then blocks on the existing combined command-endpoint/local-notification receive; a Reply-bearing command returns to ordinary dispatch, while another genuine C3 edge is serviced and acknowledged before blocking again. The selected terminal context declares four refills: an active head, two unexpired usage fragments for the 5-ms timer duties, and enable/call carry-in. This avoids the two-slot full-tail merge that repeatedly defers replenishment. There is no post-IRQ MCS Yield: the kernel’s entry budget check can fault before its nonfaulting full-head retirement body. No command Reply is held across this completed IRQ block; failure retains ordinary containment. C3 remains programmed at 5,000 us, but a pending edge may wait for the unchanged 400/10,000-us reservation. This is not a 5-ms dispatch guarantee. Classic kernels retain direct blocking. It never performs root timer work, PCIe work, catch-up, retry, polling, or a second physical action. Every tag, address, page-count, IRQ, badge, slot, trigger, period, and interval identity is checked before MMIO; malformed identity performs no device access, signal, or ACK. A retained Enabled record alone is not a live producer: root also requires the PCIe owner’s current nonzero endpoint/capability generation, open MCS command admission and idle or associated Call phase. Containment closes that admission before suspension. After the supervisor’s validated containment release, root-fault signals its existing root fan-in cap. Thus an old timer record cannot authorize another global wait after its owner faults. On Pi only, after the existing validated containment Suspend and before revoking supervisor authority, one bounded TCB.ReadRegisters(count=1) records the suspended AArch64 PC. DRIVER_FAULT_CONTAINMENT v1 then adds pc=<hex> or pc=err:<kernel-error-hex>; absence means not captured. Read failure never blocks the remaining containment, and no driver resumes or receives another budget. The PC is a fault-location discriminator tied to that exact runtime ELF, not a per-IRQ duration or successful recovery proof. USB readiness/recovery debt likewise prevents global idle, although it does not veto an exact authenticated response continuation after an operator turn. Healthy command-ready empty keyboard polling is not that readiness debt. Root never maps or programs this timer. The runtime descriptor layout and runtime-descriptor layout remain unchanged; additive internal resource tag 15 names only this exact page. The current shared protocol version is ABI v13 because of the later generic one-way wait handshake above.
• The Pi direct-GENET-feature isolated authenticated console socket, used by both selected Pi network modes, is an interactive control path, not a bulk stream. It retains smoltcp 0.13.1’s 10 ms ACK timer so a prompt response can carry the receive ACK without an additional packet handoff. Missing or slow root output cannot suppress the due ACK. Nagle remains disabled, so response data waits for neither the ACK timer nor an unacknowledged earlier response. This changes no frame, queue, listener, authentication, ownership, or MCS contract; QEMU retains its already-qualified TCP policy.
• The root’s unchanged direct-GENET ServiceTick is a timer hint, not work authority. After an empty stable control-page read, the console child starts a local service cycle only for already-retained private work or an exact due smoltcp, authentication, authenticated-idle, close, or relisten obligation. A real GENET link wake and a newly sequenced root control remain unconditional. This prevents an empty periodic wake from consuming the child’s SC on link/stack/session work while preserving every protocol timer; direct VirtIO/QEMU and mediated WiFi retain their selected behavior.
• The Pi console-network child retains eight refill records in its existing 8-bit SC, matching the Pi direct-GENET fragment-preserving selection, and runs independently on core 2 while root-control remains on core 0 at equal priority under the exact cross-core signal-only contract. Its budget, period, MCP, WCET, queue, packet authority, and operation bound are unchanged. The production QEMU console child also uses core 2, priority 200, and eight refill records. Refill capacity and affinity are bounded scheduling prerequisites, not physical latency, throughput, or August-parity evidence.
• After the CYW43 child is attached, one root-control invocation may traverse up to the existing five-turn hard cap across distinct Serial/LocalSeat/Dispatch/Display/Network phases instead of paying a scheduler edge between every phase. It admits Network at most once in that invocation and stops on a repeated phase, a return to the starting phase, quarantine, recovery, containment, or reboot. An exact productive Network-to-Network successor with fresh durable schedulable work may retain the current guarded activation. The authenticated-response exception above may also retain that activation after one complete Network/Serial/LocalSeat/Dispatch rotation, but it performs no second Network operation inside the invocation. Each phase keeps its existing one-operation bound. The post-Dispatch fence preserves Idle, UsbServiceDebt, and Input as distinct states: passive USB service debt receives its one bounded LocalSeat turn and does not then fence Network, while decoded or buffered input still does. The transient-publication probe preserves the same typed state: it may admit passive USB debt only because a minted credit installs that complete operator rotor before Network re-entry; real input still rejects. Terminal shortcuts remain strict; no SC, priority, retry, timeout, device deadline, or QEMU path changes. If the ordinary EventPump consumes exactly one existing CYW43 child-to-root wake during the post-Network operator rotor, it may retain one stack-local token bound to the current physical lifetime, authenticated response identity, and accepted-command epoch. Only a complete Serial -> LocalSeat? -> Dispatch rotor, unchanged durable identity, and a return to Network with every operator/recovery/fault fence clear may retain the caller’s activation. The wrapper performs no second Network operation; Yield destroys the token. Prior useful progress followed only by an unchanged empty snapshot yields instead of retaining an eventless polling cadence. The existing idle_admitted telemetry field remains schema-stable and stays zero for this path. The retained outer quantum’s 25 ms cap accumulates only time spent inside admitted CYW43 Network service. Replenishment gaps, exact-child waits between turns, and physical-operator phases do not consume it. The independent 25 ms real-wall physical-operator checkpoint and absolute 192-turn cap remain unchanged, so long waits cannot starve serial/local-seat service and active Network work cannot become unbounded.
• In both Pi network modes, the physical Network leaf owns timer, NIC, and display-ready reconciliation only. It does not repeat the composite root IPC/bootstrap/stream/reboot tail already serviced by the bounded Serial, LocalSeat, Dispatch, and Display leaves. The generated Pi root remains on core 0 and the console child runs on core 2 at equal priority. Direct GENET and mediated WiFi both publish durable state, perform Release, and send the exact one-hot Signal without child-SC pre-drain or SchedContext_YieldTo. An exact staged control may bridge the remaining child boundary only while its child-consumption watermark is still owed, through the condition-before-block fan-in wait after every identity and safety fence revalidates; the child remains bounded by its own SC, and QEMU retains its existing direct-VirtIO selector.
• Exact durable cross-core direct-GENET productive identity may retain root-control under the generated NaturalPostpone profile and unchanged 64-complete-quantum cap only for the current authenticated request. Every stage-bearing continuation binds generation, connection, and the exact nonzero one-slot child-control sequence. Its condition-before-block fan-in wait remains eligible while that same control level owes the child’s watermark and, after consumption, while an exact root-local response batch with the same identity records control-complete but not output-drained. No durable child publication may already be visible; a publication that wins either race returns through outer recovery/operator-first arbitration without Yield. Every quantum rechecks operator, passive, fault, recovery, containment, quarantine, reboot, handoff, and continuation-mode fences, and the root’s 5,500/10,000 us SC remains the hard execution bound. Fused stage-and-drain or OutputDrained retires the current request. A fresh unconsumed child frontier may then justify one ordinary Serial-first rotor after the complete lane and operator/recovery fences revalidate. This recheck preserves the clock, causal-wait count and 64-quantum cap; even an executed turn without progress consumes one quantum and stops. Only fresh productive progress can establish the next continuation. An absent frontier retains the existing idle/Yield route, with no post-response Network baton, empty hot tail, broad event wait or future-request authority. Stale, backpressured, faulted, or operator-owned work fails closed without a retry, second packet operation, new refill, child authority, or owner transfer. Mediated WiFi cannot acquire direct-GENET continuation authority.
• A selected CYW43 Network turn samples the existing timer prelude before deciding whether association/policy work requires its outer priority lease. Admission and the subsequent runtime body consume that same fresh sample; the next turn samples again. The active Network interval includes the prelude and intervening admission. The typed inactive-outer Join rejection, physical deadlines, ownership and recovery remain unchanged. Generic, GENET and QEMU runtime callers retain their original timer order.
• WiFi netstats adds five passive wifi_rx_dequeue* rows for copied TCP ingress. wifi_rx_dequeue schema=v1 reports connection generation, valid sample count, missing metadata, saturated Q11 metadata and invalid timing. Missing includes ordinary non-first-DATA frames and is not a packet-loss counter. Only the exact first DATA token carrying both stage metadata and root-copy time contributes the four us=sum/max intervals: s2q is DPC source to runtime queue, q2p queue to batch precommit, p2r precommit to root copy, and r2d root copy to dequeue. Source is an existing DPC episode timestamp, not wire arrival. The first two are Q11 floors; their residuals remain in p2r, and independent microsecond flooring may differ from total by up to three microseconds. Missing, saturated, invalid-clock, inconsistent or half-wrap-ambiguous observations do not enter timing sums. Populated zero low words remain valid. Counts/sums saturate and reset by generation. wifi_rx_dequeue_slow and _slow_us retain one maximum total with its same four intervals and bounded IPv4/TCP header identity, or absent=yes. Header validation makes no checksum/authentication claim; no payload is recorded. Existing paired-TX RX-split counters retain their separate meaning.
• The same validated Wi-Fi dequeue hook retains up to 96 TCP header receipts for the latest control flow, exposed through six passive wifi rx-trace pages. It reuses the existing dequeue counter read and records the IPv4 ID, TCP identity and available source/Q11/root-copy/dequeue observations, without payload, device calls, scheduling authority or a shared ABI change. Pure ACKs are excluded; repeated SYN/data receipts remain distinct. Generation/new SYN identity resets the bounded journal. A packet absent from this journal is absent at this root observation point; this alone cannot identify RF loss, firmware delay, runtime admission or earlier software loss. Bind it to the complete same-boot capture and existing driver queue/drop counters.
• Pi ordinary root polls retain elapsed phase totals, maxima and full counter pairs for the latest nonzero TCP generation/connection. smp poll-time reads eight cached rows without kernel CPU-accounting calls. Two exported-counter reads bracket each observed poll; the exclusive passive admission path is excluded to preserve its first-operation invariant. between includes unobserved outer work and waits. Wall time includes descheduling, so neither long phase intervals nor session CPU totals prove which scheduling context exhausted a refill. Command/clock identities and separate CPU, packet and service receipts remain necessary for attribution.
• A parsed Pi passive-service command whose strict reserve lease expires is retained across at most one completely new Yield/refill attempt. The retry begins from AwaitingYield, drains fresh Consumed evidence, and retains the generated strict <3,000 us budget - WCET test plus every command, session, connection, recovery, containment, and quarantine fence. A second expiry emits the same single busy detail=root-sc-reserve refusal; no within-refill resampling or sliding lease is permitted.
• The isolated console child’s Ready timestamp and the root handoff bound share the absolute CNTVCT millisecond domain. Root samples immediately before and after resume, requires identical nonzero generated/runtime timer frequency and a nondecreasing counter, uses the pre-resume sample as the inclusive publication lower bound, and derives the exclusive deadline from the post-resume sample plus the generated response bound. This admits a child publication between resume and root return while rejecting zero, pre-resume, at-boundary, late, stale-generation, identity-invalid, backwards, overflowed, or frequency-drifted evidence.
• SDIO containment and HOST_CONFIG may batch finite deterministic sole-owner register/state transitions inside one admitted turn. Containment is capped at 24 transitions; host configuration is capped at 18. Controller, command, DMA, reset, inhibit, and internal-clock-stability conditions still receive one sample per admitted turn and persist when false. The exact 100-microsecond card-clock-disable settle is different: containment consumes that timer-only interval inside the already-admitted owner SC, testing the settle condition before the unchanged outer containment deadline. The Pi implementation uses exported CNTVCT_EL0; deterministic host tests use the finite fallback. At most the two existing settle intervals run, with no SDHCI condition poll, command, DMA action, new owner, retry, or deadline extension. The HostConfigStart intake must enter that bounded containment before its first persisted outer-owner boundary; arming the immutable owner deadline and releasing before containment lets unrelated MCS admission age the request without doing device work. The first permitted post-containment boundary for the initial differing-clock request is HostConfigClock1Disable; an equal-clock request resumes at HostConfigControl, while a genuine DMA/reset/inhibit wait may persist inside containment. An unarmed or invalid retained settle cursor fails through the existing typed containment path. Preserve command identity, no replay, and the immutable first causal failure snapshot; a transition bound or cursor violation fails closed.
• At the shared-payload/private-DMA boundary, copy only between the existing shared command payload and the SDIO child’s existing private uncached DMA4 bounce region. Use an alignment-safe bounded prefix, u64 word body, and tail; validate both complete ranges, integer overflow, and discontinuity before touching either side. This is a CPU copy optimization, not permission for DMA4 to address cacheable shared pages or for CYW43 to gain controller authority.
• Current DPC-client accounting lives in one cache-isolated, exact 128-byte DriverRuntimeCyw43DpcClientRecord at shared offset 49,984 ([49,984, 50,112)). CYW43 is its sole writer and publishes at the existing initialization, quiescent owner-rearm, and terminal-fault checkpoints by committing a nonzero publication sequence in the final word after the body. Root reads it only between two identical stable live-SDIO-ring snapshots and requires the record’s physical epoch and consumer sequence to match that ring. A torn, raced, or stale sample is rerun-required evidence, not admission, notification, wake, issue, retry, rearm, recovery, deadline, scheduling, or physical-owner authority. The additive completion trace is compatibility input, not current client truth.
• A physical or logical generation change invalidates stale work; it does not authorize relabelling or replay under the new generation.
• Recovery reuses the same ownership path after containment. It does not create another bootstrap, controller, or data path.
• Preserve the exact first-recovery pre-scrub discriminator and snapshot before clearing the delegated generation. The bulk-copy change does not alter controller ordering, physical/logical owners, retry ceilings, device or aggregate deadlines, pair-restart cuts, completion layout, or IRQ mask/acknowledgement semantics.

Exact source 0696803f55d215721b4e750825a5c25daf2cac05 is the current dual-mode hardware oracle for this seam. WiFi completed Gate 8, DORA, three first-attempt .coh scripts, and 64/64 raw requests without fault or quarantine, but only at 7.196 requests/s and 159.456-ms p95. GENET completed the same functional gates and 64/64 at 47.167 requests/s and 20.052-ms p95. Its request-to-target-ACK latency, 0.545-ms median and 0.634-ms p95, is already effectively equal to the August hardware-ingress comparator, while its ACK-to-response latency remains 19.307-ms median and 19.360-ms p95. This routes the shared remaining failure to the root/isolated-console MCS response seam rather than GENET DMA/IRQ or WiFi RF/DHCP. It is convergence evidence, not current-candidate performance or acceptance proof.

• Direct GENET uses a QEMU-derived productive-micro-unit rule without copying QEMU authority. After the child publishes one exact authenticated Command or CommandBatch, it quiesces direct service until root applies a newly sequenced StageOutput for the same generation and connection. Root may compose only that adapter-local response stage. A bounded immediate terminal such as QUIT already queues its exact adapter response and therefore has no SyncCapture record to compose. Typed NoPending may proceed only when the ordinary generation-, connection-, authentication-, recovery-, flush-, and batch-drain predicate independently proves that existing response lane is stage-ready, terminal-queued, producer-closed, and contains exactly one completed response; otherwise it defers as OutputMissing. Identity drift retains fail-closed containment. A stale/empty control, peer wake, publication ACK, fault, or containment cannot release the quiesce. Due protocol obligations retain the existing three-unit service bound. When an earlier exact root output control still awaits TCP drain, retained transport work and peer wakes may also enter that bounded cycle so its ACK can arrive before root stages the next response. Pending output grants service permission only; it cannot mint a poll or replace the pending control. QEMU direct VirtIO and non-GENET backends remain on their existing paths. Before any console-network child is activated, HAL initializes all four shared protocol pages with their exact generation and empty ABI identity. Zero commit words and watermarks grant no READY or publication credit. This permits strict level reads before the first event and on the unused direct packet-egress page without accepting anonymous zero-filled or corrupt pages.
• Copied WiFi may retain the current guarded root activation across a period seam only through one opaque transient-publication credit. Minting requires one Network poll to advance exactly one material isolated-child unit while lifetime, response cursor/lane, active and authenticated connection, accepted-command count, service count, and pending flush remain exact at the mint. The next composer must admit the ordinary Serial -> LocalSeat? -> Dispatch cut. After Dispatch it may rebase the credit once only when one authenticated network command advances the command count by exactly one, the prior empty lane becomes one exact nonempty sealed completed response lane, and the prior empty flush becomes one bounded same-connection flush. Lifetime, generation, response identity, service count, operator rotor, recovery, containment, quarantine, reboot, and handoff evidence must remain exact. It then revalidates the complete rebased snapshot immediately before one Network poll and consumes the credit once. Any other change, Yield, physical operator or response work, passive admission, or identity/cursor drift revokes or rejects it. The credit is not a notification, SC refill, retry, device grant, or transferable authority.
• Pi-only causal diagnostics retain bounded in-memory aggregates, not a hot log. The composer recorder accumulates raw 54 MHz CNTVCT start-to-start periods and start-to-finish run ticks for root-control composer quanta; these are not kernel activations, SC refills, or consumed-time samples. The first period is excluded, backwards periods and invalid counter evidence are counted separately, and conversion to microseconds occurs only when an operator requests smp mcs. A separate one-assembly-block CNTVCT -> svc -> CNTVCT record measures the exact userspace hiatus around an explicit Yield. It retains one exclusive trigger, the pre-Yield pending mask, lane, and exact connection/generation. Fixed one-bit pending state distinguishes command queue, root output, child control, child egress, child event, continuation, WiFi-driver work, passive admission, operator work, and recovery; triggers distinguish reserve guard, no productive successor, passive admission, recovery fence, operator rotation, and other explicit boundaries. Guard rows additionally retain activation, attached, bootstrap-operator, and bootstrap-driver cuts. The reason-bit layout remains schema-stable; exact NaturalPostpone productive lanes now close on cap or policy rather than a userland clock/reserve cut. These observations can locate an off-CPU MCS seam but do not independently identify a kernel refill.
• The latest TCP session also retains the first longest valid Yield’s existing pre-Yield root work counters, pending mask, phase and observed child publication level. This passive cut grants no service work and cannot prove the child remained unchanged until the syscall. WiFi ACK admission retains the latest same-flow ACK immediately before a received FIN, so teardown ACKs cannot erase the body receipt. Duplicate FINs preserve that cut; SYN tuple reuse and WiFi generation replacement clear it. Missing matching headers remain absent. Child ingress completion is recorded as observed at that cut, never upgraded by later completion and never called TCP ACK retirement. Both additions use existing bounded root records without new clocks, scheduling syscalls, device operations, payload retention or shared ABI.
• Pi netstats retains six additive fast-path rows. Copied WiFi counts transient-publication candidates, mint/consume/reject totals, the sticky reason mask, and rejects at the exact probe, next-composer entry, final pre-Network, or revocation cut. cyw43_productive_window counts exact same-lifetime, authenticated-generation/connection/accepted-command window opens and closes inside the generated NaturalPostpone activation with the unchanged 64 logical/productive caps. Its schema-stable idle_admitted field records the retired transient-empty path and remains zero under event-backed continuation. The additive ready_rechecks counts durable-publication wins at the final attached WiFi wait cut. Such work spends the existing single outer-recheck allowance without requiring another notification or forfeiting a refill. Invalid identity, root-polled deadline and operator/recovery fences remain closed. The counters grant no refill, retry, or device authority. Direct GENET counts the typed response-compose outcomes composed, no_pending, not_sealed, backpressure, and identity_drift. composed proves a sealed SyncCapture moved into the adapter. no_pending may reach the same ordinary stage path only when an exact already-queued non-SyncCapture response lane is independently stage-ready; otherwise genet_defer output_missing increments. The counter alone authorizes nothing. The adjacent genet_defer row assigns every aggregate compact Deferred to exactly one of passive, command, compose_open, compose_backpressure, fence, prior_batch, control_busy, output_missing, or stage_backpressure; their sum equals the aggregate genet_compact deferred count, and compose_open is the aggregate classification for typed NotSealed. When the isolated service exposes timing, five optional millisecond seam ages cover command publication to root observation, dispatch to first StageOutput, StageOutput to the observed control-consumption watermark, StageOutput to OutputDrained, and OutputDrained to root observation. The shared control watermark has no timestamp, so stage-control-observe intentionally combines child consumption and later root observation rather than claiming to split them. On the physical Pi release target, child timestamps and every root dispatch, observation, stage, control, and drain sample use the same absolute CNTVCT_EL0 epoch scaled by generated TIMER_CLOCK_HZ; root elapsed/smoltcp time is never compared with that epoch. The GENET, CYW43, and default stack wrappers forward the exact dispatch identity and observation to the isolated adapter. Host tests and QEMU retain their caller-time fallback. Zero/backwards pairs are invalid and valid totals saturate. Collection never calls SchedContext_Consumed, changes a scheduling decision, signals a task, retries work, or executes accounting writes on the protected QEMU release path; QEMU emits none of the six rows. These rows and the explicit smp mcs batch are diagnostic only; fresh exact-image Pi traffic and benchmark evidence remain required for correctness or performance claims.

When debugging the linked pair, trace this chain with exact identities:

root parent publication
  -> CYW43 parent acceptance
  -> SDIO child publication
  -> physical issue or explicit not-issued terminal
  -> IRQ/DPC or polled terminal
  -> SDIO completion commit
  -> CYW43 child receipt
  -> CYW43 parent completion commit
  -> root consumer receipt

Stop at the first missing durable transition. Later counters or notifications cannot prove an earlier handoff.

After the current CYW43 generation has committed Gate 8 and the legacy network stack has exact DHCP/address/prefix truth, that truth exposes only a side-effect-free deferred-console predicate. The bootstrap supervisor must then select one exclusive ConsoleHandoff root-control turn: it performs no CYW43 poll, borrows HAL only to finalize and resume the already registered console-network child, and yields before a later Network turn consumes child Ready. Recovery or a runnable/waiting canonical parent keeps priority over this handoff. DHCP becoming bound inside a NetworkControl turn authorizes that handoff only when the turn began strictly before the original deadline and the committed generation remains operational both before and after activation. The authorization is retained for the exclusive following turn; raw DHCP truth alone cannot select the handoff. A successful activation replaces neither budget nor retry policy: it arms one exact-generation Ready observation window derived from the independently rounded generated response bounds for console-network-service and root-control (3 ms + 6 ms = 9 ms for the current Pi profile). Missing, zero, inactive, non-admitted, or overflowing authority fails closed. Retain the ABI-validated child publication time together with exact service identity, generation, and sequence. At or after the boundary, one final shared-page-only observation may accept only a publication strictly before the deadline; it performs no NIC work, policy advance, retry, wake, or composed Network unit. An at-boundary, late, missing, replayed, or drifted publication fails closed. A handoff failure stays failed, with no root TCP fallback, deadline renewal, or extra retry. Gate 8 and DHCP alone therefore do not prove listener readiness.

Pi display continuation diagnostics

Generic MCS one-way runtimes without a physical notification source recheck the exact durable DROA acknowledgement before a local notification wait. Only matching request, fingerprint, sealed runtime identity and slice permit clearing that acknowledgement and resuming the existing bounded action. Unacknowledged, stale or retired records do not authorize work. Serial, GENET, PCIe and CYW43/SDIO retain their physical-source arbitration boundaries. The bootstrap binding guard remains unchanged; the prewait repair alone does not prove an initial edge was received. The e11b four-boot matrix reproduced HDMI request 60 with fresh child progress still at 59/runtime-poll-ready and no DROW/DROA across several minutes. An unbound NBSend can miss the final ring-poll/endpoint-receive interval, so root may reconcile that exact initial rendezvous. Require the same active retained USB/HDMI command, fingerprint, runtime/capability generation, Issued phase, no prompted slice, no wait record or terminal, and the immediately preceding valid idle child record. Recheck the identity and frontier around the existing generated-period wake gate, then send at most one nonblocking endpoint hint and return to the outer rotation. Child progress and absence are observations restricting this hint; they never authorize physical work or a replacement command. Current-command progress, a DROW/DROA or terminal, changed identity, and every bound or physical-source runtime exclude this path. Call/Reply, the immutable child intake and one action per acknowledged slice remain unchanged.

Explicit USB diagnostics add command_frontier, command_wait and command_progress for each mapped USB/HDMI runtime. These stable per-record reads do not advance the command or grant a wake. Cross-record values can race a real child transition and must be correlated by request/slice. state=absent means no stable DROW/DROA was observed; it is not proof that the child is idle. The progress row reads the current shared record rather than a cached timeout sample. A persistent outstanding frame is a liveness failure even when timeout and no-reply counters remain zero.

8. Build diagnostics for developers, not incidents

Pi release-pi4,bootstrap-trace emits bounded, unbuffered bootstrap receipts with prefix [diag net-bootstrap/v1] backend=genet: cut=owner-proof.begin and cut=owner-proof.return surround the post-owner diagnostic snapshot; cut=stack-construction.begin and cut=stack-construction.ok surround root-side network-shell construction. The latter appears only after a successful result. The constructor also reports cut=init-guard.ok, cut=device-allocation.ok, cut=storage-reservation.ok, cut=stack-allocation.ok, and cut=tcp-sockets.ok for the exact GENET driver type. The existing fault and emergency receivers are active before this constructor. An unsealed fault reports copied operands under [critical:bootstrap-fault/v1], latches fatal state and fails closed without recovery; a missing constructor cut without a fault report remains an unclassified stop, not proof of a particular fault PC. These receipts identify the first unfinished bootstrap operation when buffered logs and the shell are unavailable. They carry no target readiness or acceptance credit, run only during GENET bootstrap, and add no steady-state sampling. Trace consumers may preserve these lines without interpreting them as driver completion, ABI records or performance evidence.

Pi bootstrap also retains [diag root-text/v1] at root entry, IPC installation, fault-receiver activation and the GENET constructor cuts. Each sample reads 4092 bytes starting four bytes after the linker text base, reports FNV-1a32 over their little-endian bytes and the word at text offset 0x34, and performs no writes, mapping changes or scheduling operations. The entry word is excluded to avoid a null Rust pointer on the selected zero-based image. Compare samples with the retained exact ELF; matching data reads alone do not prove the bytes fetched by the instruction cache. These boot-only diagnostics grant no recovery or acceptance credit and do not add steady-state sampling. The three earliest measurements use fixed private capture slots so bulk child admission cannot evict them before the console exists. Their original values are published once at the common pre-PCIe boundary after local-seat runtime construction; publication never re-samples text or substitutes a later value for an earlier measurement. The bounded capture/publication status identifies missing records or failed nonblocking publication. GENET constructor samples continue directly into the static Queen log through its explicit trusted boot audit sink. That sink also retains the original PCIe reset, readback, wait, firmware and complete-proof observations through the longer WiFi startup. A fixed reserve holds at most 63 complete 256-byte audit records and one capture-failure receipt, alongside the unchanged 2048-line ordinary ring. Only explicit trusted bootstrap emitters use the reserve; ordinary logging, driver-fault retry and user echo cannot acquire it by matching a prefix. One nonblocking ring-lock admission assigns the same sequence and payload to the saved and ordinary copies. Empty, multiline, oversized or excess captures are rejected before either copy is written; contention is also a failure.

Full /log/queen.log export merges saved records older than the ordinary ring with the ordinary records in original sequence order, removing only the duplicate copy with the same sequence. The cursor’s byte count covers this logical union at its frozen end sequence; later captures cannot enter an existing export. Each batch rechecks the bounded saved prefix so an unread audit record survives ordinary eviction between batches. Ordinary records retain their existing eviction semantics. Tails select the exact latest N records of the same union; the supported 1..256 tails and ordinary 64-record snapshots are unchanged.

Capture failures latch sticky flags: bit 0 is lock contention, bit 1 an invalid record, bit 2 reserve exhaustion, and bit 3 sequence exhaustion. Before freezing the next export cursor, the reserved slot records [diag boot-audit/v1] state=failed reason=capture-unavailable first_observed_failures=0x<mask> recorded_at=log-export at its actual later sequence. It does not pretend to be an original hardware observation. If the lifetime sequence has exhausted u64, no further sequenced record can be allocated, including the failure receipt; capture still returns failure and cannot acknowledge retention. Collectors must reject this failure receipt as well as missing, duplicate or mismatched required audit observations. A release kernel needs no DebugPutChar sink; physical UART emission remains subject to sole-owner handoff. Every required original checksum cut and ordered hardware receipt remains mandatory; retained source or a logging attempt does not prove physical integrity.

HAL’s PCIe register-page cache returns the newly mapped address on its first successful publication, or the existing winner if another publication won. The previous zero returned by a successful atomic compare-exchange is never a mapping. Cache hits, publication results and register-address construction require a nonzero page-aligned virtual base; invalid bases return pcie-reg-page-virt before any register access. This prevents a missing mapping from turning PCIe register offsets into writes to low root text. Physical mapping, capability admission and the existing PCIe owner remain unchanged.

BCM2711 cold admission begins at SW_INIT_1 (0x9210). The selected U-Boot OS-prepare removal hook asserts PERST and INIT and powers down SerDes; status, configuration and interrupt registers must not be sampled before bridge reset release. Assert INIT/PERST, retain the existing 100-us settle, clear INIT and verify its readback while PERST remains asserted. Only then clear SerDes IDDQ and retain its existing 100-us settle. Configure inbound windows and interrupt quiescence, release PERST with readback, wait the existing 100 ms, then read link status. All-one reset/SerDes readbacks or inconsistent reset bits return typed HAL errors before accessing the next register bank. The bounded receipts identify first_access=sw-init, bridge release and SerDes release; the old pre-reset status_before sample is deliberately absent. One owner admission state distinguishes idle, in-progress and complete setup. Both local-seat USB and the SDIO prerequisite handoff require the same complete proof; link/MSI flags alone are insufficient. Only full endpoint and firmware completion permits reuse, which still checks reset/SerDes release before reading status. Starting revalidation revokes consumer admission until that check completes; any failure rearms fresh reset and setup. Exact endpoint configuration remains mandatory. Physical settle intervals use an ordered exported virtual-counter read (dsb sy; isb; mrs CNTVCT_EL0; isb) and generated timer frequency with checked conversion and typed failure when the clock is invalid. Ordinary telemetry counter reads retain their existing behavior. CPU iteration counts never stand in for the 100-us, 100-ms, 5-ms or 20-ms waits. Safe early HDMI checkpoints remain bounded within these waits. The existing configuration-selector barriers, readbacks and retry bound remain; selector access has no additional invented elapsed-time requirement. The complete proof also owes one VL805 firmware reload after each actual PERST, including initial U-Boot takeover. Issue the existing NOTIFY_XHCI_RESET mailbox tag for device 0x100000 only after root windows, endpoint BAR, interrupt suppression, device control and command readbacks are ready, then retain the existing bounded settle. Reuse without reset sends no notification. A failure anywhere in the proof rearms a fresh reset before a retry; neither partial link readiness nor an uncertain mailbox completion permits firmware to be loaded twice into an unreset controller. This follows the selected U-Boot bcm2711_notify_vl805_reset contract and Linux v6.12 Raspberry Pi reset driver.

USB EngineInit hardware failure returns the existing Fault code and DeviceUnavailable detail (3), with its last same-command progress phase in result (0 when unavailable). The runtime validates marker magic, sequence and init auxiliary identity before retaining that phase. Generic failure and subsequent idle publications cannot overwrite the terminal completion. Passive usb status/usb dump-state add usb: init_failure detail=... phase=... phase_name=... on this fault and select usb-engine-init-fault with next action inspect-usb-init-failure ahead of idle progress. The raw current progress row remains available separately. A distinct failed local-seat service reason queues one bounded [local-seat] USB fault notice through the physical console and HDMI queues; queue backpressure delays it without repeated log writes. This does not bypass controller admission or change the ring layout, manifest, retry counts, timeout bounds, command grammar or completion framing.

BCM2711 HAL interrupt quiescence uses only the dedicated MSI bank at offset 0x4500, matching the selected U-Boot controller setup. The older STB interrupt bank at 0x4300 is not a second MSI bank to mask. Perform quiescence after the root reset and inbound-window setup, or after proving an already-live root. Write all 32 bits to MASK_SET (0x4510) and CLEAR (0x4508); read MASK_STATUS (0x450c) and STATUS (0x4500) instead of reading the W1S/W1C command aliases. Publish the existing masked-source proof only for mask 0xffffffff and no pending sources. Invalid addresses or a failed status check leave the proof false and return a typed HAL error. Endpoint INTx/MSI/MSI-X suppression remains part of the existing VL805 ownership proof. The bounded boot receipt identifies bank=msi, mask_status and pending; it grants no network acceptance. The selected source is third_party/u-boot/drivers/pci/pcie_brcmstb.c; Linux v6.12 brcmstb likewise selects one interrupt bank by controller revision.

Diagnostics should make the owner state machine understandable without embedding a particular failure history in this document.

8.1 Required diagnostic qualities

Use stable field names and typed values. Prefer one compact summary plus bounded detail records over an unbounded dump. A useful report answers:

• Which profile, artifact, ABI version, and runtime identity are active?
• Which resources were declared, admitted, and accepted?
• Who owns the physical operation now?
• What exact request/generation is active?
• What was the last durable transition?
• Is the runtime runnable, waiting on a declared condition, terminal, or quarantined?
• What is the strongest current blocker?
• Which counters changed during this observation, and which are merely cumulative?

Distinguish current, retained, inferred, stale, and unavailable data. A boot-time readiness latch must not be presented as current liveness. When usb: runtime_queue queue_valid=no, the queue depth, doorbell, preserved-event, transfer-event, and report-status companions render as unknown; bytes carried in an enumeration result are not HID queue telemetry.

When a verbose diagnostic can end before its causal state is shown, reserve a compact terminal summary before producing detail. For example, the Wi-Fi diagnostic summary should retain detail-complete state, current versus scrubbed scope, current and retained frontier, recovery cause, and first scheduler trigger. This terminal summary is evidence presentation only; it must not service, retry, or recover the driver.

One current compact Wi-Fi causal transaction begins with nonzero wifi: diag_begin id=<id> schema=v2 snapshot=best-effort-multi-record .... It contains at most eight preflighted body lines and closes with a matching wifi: diag_complete ... schema=v2 that repeats the first gate, status, blocker, body-line count, and body-byte count. wifi: causal_episode binds the latest stable physical epoch, logical generation, immutable parent, SDIO child, terminal, pending mask, and exit. The latest CYW43_DPC_CHILD_TIMING_ENTRY distinguishes publication, intake, issue, terminal, and final-consumer acceptance. wifi: causal_grant and the transport row expose publication/consumption and root-wake badge/counters without making either notification an authority source. This multi-record snapshot is causal triage, not Gate 7/8 acceptance; an earlier failure renders downstream work not-reached.

The current causal-progress producer carries either ring=u or the exact fixed-width lowercase result-bearing tuple command-sequence:opcode:flags:aux1>completion-sequence:code:detail:result. The normalizer separately retains the early schema-v2 row with no ring suffix and the exact historical seven-field tuple for existing evidence; neither old form can refine a blocker. Only the current result-bearing form can refine a containment stage after its nonzero publication and episode sequences, immutable parent sequence, nonzero physical epoch, matching child sequence, concrete transport-parent fault, child Fault terminal, and stable bus episode all correlate inside the unsigned 32-bit identity domain. A present short, uppercase, extended, zero-identity, or overflowing tuple/episode fails closed.

wifi dump-state retains the verbose DPC, association, maintenance, data-path, Gate 7, and Gate 8 inspection rows. Historical logs can contain the former bracketed diag_begin ... snapshot=current verbose transaction. The normalizer continues to accept that old grammar, but new compact wifi diag output cannot manufacture or replace the independently required verbose acceptance evidence.

When pair recovery is entered after an SDIO owner fault, the first-recovery snapshot may additionally expose scheduler_sdio_fault, scheduler_sdio_status, scheduler_sdio_dma, and scheduler_sdio_regs rows. Root accepts this payload only when two passive reads agree and the completion is Fault with the exact version-3 116-byte length, an aligned in-ring cursor, a contained or owner-poisoned disposition, matching magic/version, and a failure word equal to the terminal result. The retained 29 words preserve the owner’s pre-scrub SDHCI and DMA4 register cut; captured=no means unavailable evidence, not zero hardware state. These rows never acknowledge, consume, retry, reset, wake, or recover either owner and cannot satisfy a Wi-Fi gate by themselves.

Root-command generations and CYW43/SDIO link epochs are independent identities. An ordinary root grant is matched to the complete sealed parent, including its aux1 (zero is valid at cold root startup). The retained reciprocal transaction is separately matched to the nonzero live CYW43 and SDIO DPC epoch. The post-action causal wait and childless recovery cut must not require these two domains to have equal numeric values. Replacing either the exact parent or the live peer epoch still rejects continuation; no grant, Reply, physical-operation bound, or recovery authority is relaxed.

On physical Pi MCS, the exact queue-only NetData RX_POLL descriptor may compose root housekeeping within one bounded outer turn. HAL requires the unchanged canonical command budget, quiet retained flags, nonzero logical generation, sole 28-byte descriptor, and RX_STEADY_TAIL_DRAIN with every other descriptor field zero. Admission uses at most six existing calls: Stage, reservation/boost bookkeeping, sequence-last CommitRing, first PublishGrant, and NotifyRing. The MCS boost steps verify existing reservations without changing priority or the SC. Notification ends this episode, even if a child terminal races it. On a later turn, an already-stable exact terminal may close at most four existing retirement calls, including reservation release and completion consumption. Every composed call revalidates identity, lifetime, producer and recovery guards; only strict same-request phase progress permits another call. Stagnation, an unavailable frontier, a recurrent grant, notification, and completion return to outer arbitration. No child waiting, recurrent grant, physical work, deadline, batch acknowledgement, ring authority or QEMU path is changed. Existing queue-to-publication and publication-to-root receipts measure the effect; source and host checks do not establish physical performance.

An ordinary retained CYW43 timer poll is a childless bounded action, including the mandatory post-CMD0 guard. Its private per-turn witness names the exact retained deadline slot and clears on the next turn. A valid timer observation returns the admitted root action through the existing fan-in without restarting the deadline, skipping terminal replay, issuing a child, or entering recovery. An empty frontier or a previously stored deadline without that current witness does not qualify. Parent, peer epoch, payload seal, recovery, and child-ownership checks remain mandatory; the witness adds no runtime ABI field.

The first delegated boot child has a separate passive PHOF v1 record in each CYW43/SDIO local ring, at bytes 84..128 between the 20-byte completion and progress record. Its eleven words are magic; packed version/role/route; publication revision; child sequence; parent sequence (SDIO: retired engine sequence); child aux1; stage bits; detail; witness; low CNTVCT at the latest stage; and commit-last revision. Runtime-init ABI v13, command/completion layouts, grants, and all scheduling authority are unchanged. Only the respective runtime writes its record. SDIO’s child-selection predicate requires the delegated sequence domain, SDIO role/hot path, nonzero link epoch, and one-way flag; a passive reread of its retired engine command cannot consume the first-child slot. Each stage is recorded at most once for the first child, freezes on its terminal or recovery, and clears only at canonical runtime reset. No unbounded event log or steady-state publication is added. Root accepts two equal valid reads with the correct writer role and retains them before its first recovery mutation; the two roles are not an atomic cross-runtime snapshot and identities must be compared explicitly.

wifi dump-state and startup blackbox output expose two wifi: pair_handoff rows, scoped live-first-child, first-pre-fence, or unavailable. The fixed 12-line atomic recovery queue and eight-body-line compact wifi diag contract are unchanged. observed=no is unavailable/unstable evidence, not a failed syscall. Stage bits 0..13 mean armed, actual prewait, raw receive returned, stable child read, intake begun, descriptor pre-admission returned true, dispatch entered, bounded action returned, terminal committed/observed, producer precommit, producer syscall returned, recovery, child action/terminal observed, and rejected. A raw result is not classified notification proof; action return is not physical I/O proof. Route low nibble is 0 unavailable, 1 SDIO, 2 CYW43, 3 other; high nibble is 0 signal-only/unrecorded, 1 Recv, 2 Wait, 3 ReplyRecv, 4 NBSendWait. SDIO detail/witness retain the first raw badge/MessageInfo low words. CYW43 detail is its precommit rejection phase 470..479 (zero if admitted), witness its first returned wait badge. PRECOMMIT does not prove command commit or signal delivery. The new writes occur before command commit or after syscall return, never between commit and the atomic prompt-and-wait. Low CNTVCT is a wrapping stage stamp, not whole-boot timing or a substitute for the existing per-child DPC timing and packet captures. These records grant no wake, retry, recovery, gate, or performance acceptance.

Routine WiFi, GENET, and HDMI ring-call begin/return chatter is not a required steady-state record. The target may suppress it for steady, nonblocking, prompt-slice, and retained turns; initialization, descriptor non-acceptance, fault, budget-exhaustion, and non-quiet timeout evidence remains mandatory. Absence of a routine call row is therefore neither progress nor failure proof.

The complete activity-gated DRIVER_TASK_COUNTER provenance record remains a single fixed-layout row with a 1,024-byte construction bound in boot/qlog evidence. It is not a console-line ABI. smp and smp activity project the same selected snapshot into exactly seven independently bounded 256-byte rows: [smp] driver v=1 parts turn, outcome, sched, retry, cache, traffic, and role. Wi-Fi projects CYW43 then SDIO; wired mode projects GENET. The split changes no counter, activity gate, owner, or normalizer authority and cannot replace a missing canonical provenance record.

On a physical-console smp or smp activity request with Wi-Fi selected, a complete current old-good receipt is emitted before the ordinary activity report as one all-or-nothing 37-line batch. Its first six rows are compact current DRIVER_TASK_OWNER_STATE records in the exact order serial-console, usb-keyboard, hdmi-text, pcie-root, cyw43-wifi, then sdio-host; their contracts are respectively serial, usb-local-seat, hdmi-text, pcie-root, cyw43455, and sdio-host. Only USB, CYW43, and SDIO carry bus_link_seal=valid. The following 31 physically contiguous rows are one WIFI_OLDGOOD_RETAINED_BEGIN, three same-ID firmware/NVRAM/CLM SHA-256 rows, the exact 26-step SDIO-engine-through-DHCP-bound replay, and one matching WIFI_OLDGOOD_RETAINED_END ... status=complete. The beginning fixes id=pair_epoch, attempt=1, nonzero pair/generation identity, prefix_steps=26, and the concrete firmware, normalized NVRAM-upload, and CLM lengths; the NVRAM upload length is 1,744 bytes, while its SHA-256 still identifies the immutable 2,074-byte source artifact. Association proof accepts only assoc, link-up, eapol-m1, eapol-m2, or eapol-m3.

Every retained or compact-owner row is at most 243 bytes. The emitter preflights the whole batch and reserves 32 body rows for the ordinary smp activity report within the 69-row body capacity; if identity changes or the whole batch does not fit, none of it is emitted. These rows are passive retained-prefix evidence, not live traffic evidence. The normalizer accepts only the newest exact contiguous transaction, quarantines older complete proof after a later malformed/incomplete reserved record, Join, Gate 8 lifecycle, or recovery boundary, and requires later same-generation netstats, authenticated TCP, terminal nettest, and healthy DPC evidence.

Each passive usb status, usb dump-state, or usb diag response continues to project the reserved USB slot and current root snapshot as two adjacent uppercase rows before its ordinary detail:

USB_OLDGOOD_RETAINED v=1 task=<u32> token=0x<8hex> link_epoch=<u32> link_token=0x<8hex> epoch=<u32> seq=<u32> mask=0x<8hex> topology=0x<8hex> input_gen=<u32> commit=<u32> source=<linked-runtime-hid|none>
USB_OLDGOOD_CURRENT contracts=usb-local-seat+pcie-root owners=<driver-owned|missing>+<driver-owned|missing> descriptors=<sealed|missing>+<sealed|missing> command_ready=<yes|no> proof_gate=<0|14> blocker=<none|receipt-missing|usb-owner-missing|pcie-owner-missing|usb-descriptor-missing|pcie-descriptor-missing|command-not-ready> root_pointer=no

The runtime-publication repair leaves the first row truthfully at v=1 with zero identity/body fields and source=none; the ABI slot and stable root reader remain so older tooling fails closed. The second row is a fresh USB-then-PCIe root snapshot. Its current descriptor and owner fields remain independently required, but receipt-missing and proof_gate=0 do not fail physical USB acceptance while runtime publication is dormant. Current acceptance instead requires both owners driver-owned, both descriptors sealed, Gate 10, command_ready=yes, one armed interrupt-IN transfer, zero current no-reply or queue-collapse state, and real linked-runtime HID input reaching the parser and HDMI. The pair remains passive and each row is bounded to 243 bytes. Active usb enable-kbd and usb probe-kbd operations do not project either retained row.

The non-network linked runtimes publish the fixed 48-byte DriverRuntimeCadenceRecord version 2 without moving the role-local ABI slot. The current entry remains a full 64-bit CNTVCT_EL0 sample; the existing word formerly used only for last_cntvct now carries the low 32 bits of the previous entry and current publication. PI4_CADENCE schema=v2 renders prev=valid|none, true modulo-32-bit entry-to-entry gap, and independent in-episode run. A missing previous-entry validity bit renders gap=na. Neither field is scheduling authority, and the old dt duration must not be interpreted as an inter-entry gap.

Physical Pi root-control service must not multiply a driver’s generated period by serializing every independent local-operator phase across separate explicit yields. While required local-seat preflight excludes Network, root may compose one bounded Serial/LocalSeat/Dispatch/Display rotation. After terminal network quarantine, it may compose the same useful rotation plus the hardware-free quarantined Network transition. Every phase retains its existing one-operation bound, the hard poll limits are four and five respectively, and reboot or containment ends the composition immediately. The existing generated-period admission gate remains authoritative and must reject a second wake for the same driver inside its period. Active Network ownership, QEMU, device protocol state, retry/deadline logic, and SC parameters are outside this Pi-only cadence correction.

8.2 Passive versus active commands

A passive status or diagnostic command reads a bounded snapshot and performs no device service. An active probe must say that it starts work, allocate a new run or command generation, advance through normal bounded service turns, and publish a terminal result. Admission of a probe is not its result.

Operators and automated tests must wait for the command’s terminal ACK/ERR/END behavior before sending another command burst. Diagnostics must preserve the documented console output bound and must not strand a terminal response behind verbose body records.

8.3 Logging discipline

• Log state edges and terminals, not every hot-path poll.
• Include immutable identity fields needed to join parent, child, and consumer records.
• Preserve the first causal fault; report later cleanup failures separately.
• Rate-limit repeated blockers.
• Keep instrumentation out of timing-critical loops unless the active task authorizes and measures it.
• Reuse existing counters and traces before adding new high-rate telemetry.

9. Test every boundary you change

Tests cover touched logic paths, including success, bounded pending work, failure, malformed input, stale identity, resource exhaustion, timeout, recovery, and publication ordering.

9.1 Unit and model tests

Add tests at the narrowest layer that owns the invariant:

• coh-rtc: manifest validation, topology, resource limits, generated output, and negative profiles;
• pi4-driver-abi: layout, size, validation, sequence-last records, and ABI compatibility;
• pi4-driver-runtime: register-independent state machines, bounded queues, descriptor ownership, command intake, retained cursors, completion publication, and deterministic MMIO/IRQ/DMA models;
• root HAL/client: admission, scheduling contracts, CSpace/VSpace accounting, publication/consumption, typed faults, trait adaptation, and event-pump fairness; and
• subsystem: device-independent behavior and operator-visible results.

Hardware-free tests must inject register, DMA, interrupt, timer, or linked-child behavior through a bounded model. Include the exact adverse orderings that the real system permits: notification before wait, work committed during the final pre-wait window, duplicate notification, late terminal, budget exhaustion, queue full, IRQ source still asserted, and deadline expiry.

Passing models prove control flow and invariants. They do not prove electrical timing, firmware, RF, cables, peripherals, or target performance.

9.2 Focused checks

Run the checks matching the touched layer before broad workspace gates:

cargo test -p coh-rtc
cargo test -p pi4-driver-abi
cargo test -p pi4-driver-runtime -- --test-threads=1
cargo test -p root-task --no-default-features --features driver-tests-qemu --lib -- --test-threads=1 --skip drivers::driver_task_net
cargo test -p root-task --no-default-features --features driver-tests-pi4 --lib -- --test-threads=1
cargo test -p root-task --no-default-features --features cache-maintenance --test cache_maintenance
cargo test -p root-task --no-default-features --features driver-tests-qemu --lib hal::cache::tests -- --test-threads=1
python3 scripts/ci/check_driver_test_coverage.py

Use the staged Test Plan as the source of truth for the final command set:

scripts/ci/test_plan_run.sh --list
scripts/check-generated.sh
scripts/ci/check_test_plan.sh

9.3 Target compile lanes

Use the release feature bundle for the selected target. Do not assemble an ad hoc substitute feature set.

Representative target checks are:

SEL4_BUILD_DIR="$PWD/out/sel4/profile-v2/qemu-smp-production" \
  cargo check -p root-task --target aarch64-unknown-none \
  --no-default-features --features release-qemu

SEL4_BUILD_DIR="$PWD/seL4/build_UBOOT" \
  cargo check -p root-task --target aarch64-unknown-none \
  --no-default-features --features release-pi4

cargo check -p pi4-driver-runtime --target aarch64-unknown-none

The exact selected seL4 directory must already satisfy the profile validator. A compile proves source compatibility with those generated headers; it does not prove image composition or target execution.

9.4 Repository gates

Before merge, run the charter-required checks appropriate to the completed change, including:

cargo fmt --all -- --check
cargo clippy --workspace --all-targets -- -D warnings
cargo check --workspace
cargo test --workspace
cargo audit
cargo deny check advisories
git diff --check

Any new unsafe block requires a precise SAFETY: invariant at the call site and tests that exercise the boundary. Non-test unsafe, unwrap, expect, and panic! indicators must not increase without the documented audit exception.

10. Qualify the driver on hardware

Follow HARDWARE_BRINGUP.md and the target-qualified stages in TEST_PLAN.md. This section defines how to interpret the evidence, not how to flash or operate a particular board.

10.1 Evidence ladder

Keep these claims separate:

1. Scope and profile: exact build-plan task and selected manifest.
2. Kernel truth: selected seL4 build, generated headers, timer export, and target configuration.
3. Source checks: unit/model tests, lint, generated validation, and target compilation.
4. Image composition: intended runtime binaries and root image were built and packaged together.
5. Media readback: the intended files were written and independently read back. This is not boot proof.
6. Current-image boot: a fresh boot identifies the intended image and profile.
7. HAL admission: exact resources, mappings, DMA profile, IRQs, and links were accepted without undeclared authority.
8. Runtime identity and owner state: the expected child accepted its descriptor and owns the physical path without root fallback.
9. Useful device I/O: bytes, reports, pixels, frames, or device-specific protocol work reached the final consumer.
10. Operator behavior: required ACK/ERR/END, console, or namespace behavior completed within bounds.
11. Repeatability and performance: the same read-back image passes the required cold/warm matrix and load envelope.

Do not promote evidence between tiers. Generated eligibility is not a running child. A running child is not useful I/O. Eventual success is not first-attempt repeatability. An accepted image is not proof of another image.

10.2 Capture the first broken transition

Begin with passive, boot-paired evidence. Do not interact with the target until the boot has settled and one operator owns the serial lane. Then identify the strongest completed transition and the first missing or failed transition.

Useful failure classes are:

• build, packaging, or media identity mismatch;
• stale or unidentified boot image;
• HAL admission, mapping, or capability failure;
• runtime identity or resource rejection;
• command publication or endpoint failure;
• physical issue versus explicit not-issued failure;
• MMIO, DMA, cache, IRQ, or timer failure;
• child terminal or parent terminal publication failure;
• notification/wait race;
• final consumer or subsystem adaptation failure;
• operator projection failure after real device progress; or
• proof-tooling and evidence-pairing failure.

Fix the complete first broken transition and its reciprocal completion path. Do not change a later subsystem when earlier exact evidence already shows the operation failed below it.

10.3 Acceptance means function, repeatability, and quality

Define acceptance in the active task and Test Plan. At minimum, physical acceptance needs:

• the exact read-back image and current boot identity;
• isolated owner-state proof with no fallback;
• useful end-to-end I/O;
• bounded error and recovery counters;
• the required cold and warm repetition matrix; and
• latency, throughput, loss, and mixed-load behavior appropriate to the role.

For a network driver, association or link and DHCP are prerequisites, not TCP quality. Measure raw TCP before higher-level REST, gateway, or hive workloads. For a local-seat driver, controller readiness is not physical keyboard input. For HDMI, a queued line is not visible completed rendering. For serial, a prompt does not by itself prove migrated interrupt-backed ownership.

11. Review checklist

Scope and design

• The exact BUILD_PLAN.md task authorizes every change.
• The driver is selected by role and exposes a device-independent trait.
• Every physical effect has one owner, issuer, completer, and recovery path.
• There is no root-context physical fallback or duplicate polling lane.
• New paths, records, and public behavior are documented before use.

Manifest and ABI

• Every runtime, resource, IRQ, bus link, affinity, and bound is declared in the selected profile and validated by coh-rtc.
• Generated artifacts were regenerated through the full output set and were not edited by hand.
• ABI records are fixed-size, pointer-free, versioned, bounded, and validated on both sides.
• Body-before-commit and commit-before-notification ordering is tested.
• Stale, duplicate, malformed, and torn records fail closed.

HAL and runtime

• HAL alone discovers, retypes, maps, allocates, binds, and publishes physical resources.
• MMIO widths, ranges, barriers, reserved bits, and side effects are explicit.
• DMA ownership and cache transitions are explicit for payloads and descriptors.
• Device source handling precedes IRQHandler acknowledgement.
• All waits and service turns are bounded by work and elapsed time.
• Pi elapsed time uses generated virtual-counter truth.
• Recovery contains the exact operation before reuse and preserves the first terminal cause.

Tests and evidence

• Tests cover touched logic paths and adverse orderings.
• The coverage guard, generated guard, and staged Test Plan agree.
• The selected release feature and seL4 build compile.
• Source, image, media, boot, owner-state, function, and performance claims are reported separately.
• Hardware evidence belongs to the current read-back image and boot.
• Diagnostics are bounded, passive by default, and identify the first blocker without mutating the driver.

12. Source map

Use these sources rather than copying their changing details into this guide:

• Active scope and acceptance: BUILD_PLAN.md and TEST_PLAN.md
• Physical build, flash, capture, and proof: HARDWARE_BRINGUP.md
• System and scheduling boundaries: ARCHITECTURE.md and ROLES_AND_SCHEDULING.md
• Profile manifests: configs
• Generated default-profile summary: docs/snippets/root_task_manifest.md
• Manifest IR and code generation: tools/coh-rtc
• Shared pointer-free ABI: crates/pi4-driver-abi
• Isolated runtime implementation: apps/pi4-driver-runtime
• HAL and root driver client: apps/root-task/src/hal
• Root network adapter: apps/root-task/src/drivers/driver_task_net.rs
• Event-pump scheduling: apps/root-task/src/event
• Local-seat adapter: apps/root-task/src/local_seat.rs
• Pi image packaging: scripts/pi4-image-build.sh
• Driver/HAL coverage guard: scripts/ci/check_driver_test_coverage.py
• Pi trace and proof tools: scripts/pi4_trace_normalize.py and scripts/pi4_gate_proof.sh

When one of these sources changes the reusable development contract, update this guide in the same change. Do not append the investigation that led to the change.