Prototype 1: complete executable driver derivation

Four different device descriptions

The prototype's conceptual GPIO ports, USART2 and DMA1 stream 5 are not a vendor part. The checked-in devices/generated/rp2040 modules describe the bounded real RP2040 register selection, using retained official metadata and independent header oracles. The registers this driver binds, their provenance, corrections, reset masks and offline regeneration are unchanged; the selection around them grew for the first board's clocks, resets and pads.

The executable application binds five of those modules at synthetic bases:

GPIO0/1 function 2 selects UART in the real image vocabulary; the model keeps all override/reserved bits of its initial GPIO control images. There is no conceptual 16-pin MODER/AFR or electrical speed register on this binding. SIO bit 0 is a synthetic indicator independent of the UART pin multiplexer. The model has an already clocked/enabled UART, a declared 48 MHz input clock, byte receive requests, immediately available transmit capacity and no serial line timing. It does not purport to configure an RP2040 board's clocks, resets, pads or UART CR. Tick is an explicit test stimulus for the modeled alarm, not wall-clock timing or an RP2040 timer emulator.

QEMU's accepted microbit Cortex-M0/ARMv6-M CPU profile is a separate lane: 32 KiB flash, 16 KiB RAM, little endian, top 4 KiB reserved for stack. It runs the actual linked application's compiler-owned reset to entry and into the ordinary call path, with poisoned RAM and a second reset. The same QEMU executes that application's MMIO and interrupt behavior against DriverPeripheral in environments/cortex-m/models.py, which the harness in machine.py serves from QEMU's debugger stub at every access to the model's window. Neither synthetic map is QEMU's Nordic hardware or a faithful RP2040 emulator.

The shared command loop and the board

commands/commands.ldn is what the application does with the bytes it receives: each echoed, ASCII 1 setting the indicator and ASCII 0 clearing it, through the indicator and the transmitter its program passes it as function values, so the module names no device (D645). The board port in compiler/tests/board/rp2040 runs the same module at the RP2040's own bases with GPIO3 as its indicator, and keeps this driver's public receive contract over the RP2040's own protocol: a live count rather than the drain below, and an abort for stop (D593, D594); the STM32H753 board in compiler/tests/board/stm32h753 runs it with LD1 on PB0 and USART3, over that chip's stream taken in laps (D648). The echo and the indicator are the outcome the two compare, and the board's run says how the board's side is checked; everything below that depends on the synthetic drain stays the emulator's. The application's transmitter waits on UARTFR's TXFF before each byte, which the model answers as always having room.

Public receive contract

open(rate, budget, escaping buf) configures fixed GPIO0/1, UART0 RX and DMA channel 0, then returns rx from buf. The caller supplies exclusive authority over those registers and NVIC routing. The buffer is an initialized ordinary mutable byte slice in DMA-accessible RAM. Its length is a power of two from 2 through 256 and its absolute address is aligned to that length. The budget is from the capacity through 65535. Only 115200 baud is supported in this bounded derivation: at the declared 48 MHz clock, IBRD=26 and FBRD=3 implement the rounded divisor. Other rates are recoverable bad_baud, not a range trap. This explicit bound keeps the complete program within the original board; it does not claim a general UART configuration API.

Checks run in this order, before any device write or descriptor publication: empty -> buffer_empty; length above 256 -> buffer_too_big; length below 2, non-power-of-two, misaligned address or invalid budget -> bad_buffer; unsupported rate -> bad_baud; existing EN/BUSY/error state -> busy. busy, bad_baud, buffer_empty and buffer_too_big retain the prototype's names. bad_buffer, overrun, transfer_error, exhausted and stop_timeout are this derivation's explicit library decisions for conditions the sketch left open. They are declared atom outcomes; none uses panic for foreseeable conditions.

The model's device writes cannot fail after successful preflight under its exclusive-authority premise. A real bus fault or concurrent register writer is outside this interface, rather than falsely covered by rollback. The returned descriptor is published only after the complete device descriptor, interrupt acknowledgment/enable, memory boundary and DMA enable are issued. There is no hidden allocator, module initializer or reporting allocation.

available(inout r) obtains a quiescent snapshot and returns unread bytes; it does not consume them. It resumes an active, non-exhausted epoch after a successful observation. The answer is a snapshot, not a reservation. read(inout r, out_buf) takes a fresh snapshot, copies the shorter of unread bytes and destination length in stream order, advances absolute consumption by exactly that count, and resumes if active. Empty input returns zero; a zero-length destination consumes nothing. Exact capacity is full, not empty. Partial consumption and physical wrap are independent of the epoch counter. A stopped descriptor can still be read without resuming DMA. The destination must be valid, writable and disjoint from the DMA backing storage. That is a manual aliasing obligation, not an ownership guarantee.

stop(inout r) clears the driver's desired-active state, requests device drain and observes BUSY clear. Success establishes quiet; failure reports stop_timeout, retains the descriptor, and establishes no storage-release permission. Repeating stop can finish an outstanding drain. restart first stops, refuses a still-faulted device with transfer_error, resets destination and finite count, acknowledges pending notification, discards all unread bytes, clears software loss/error latches, and starts a new epoch. External maintenance of an errored synthetic device is explicit (Repair in the test model); the driver does not invent a vendor error-clear accessor. Restart never treats an interrupt acknowledgment as an abort acknowledgment.

Producer, consumer and completion

Within an epoch, the device maintains a non-reloading, monotonically decreasing remaining count. It writes each byte before decrementing that count. Ring addresses wrap; the count does not. The driver computes produced = budget - remaining, retains absolute consumed, and uses produced - consumed for unread bytes. The physical index is consumed & (capacity - 1). After validated bounds, wrapping arithmetic here has the same result as mathematical subtraction/addition: all progress is at most 65535 and a copied interval is at most 256 bytes. The narrow unchecked copy indexes only these proved extents; it does not skip a device, encoding, alignment or user configuration check.

Before inspecting ordinary storage, the driver clears EN and polls BUSY at most eight times. Synthetic premise: EN-clear requests drain, and BUSY clear acknowledges that every admitted write has completed and no further write can access the descriptor until re-enabled. The model can complete an in-flight byte during that drain, delay acknowledgment, or exceed the polling bound. After acknowledgment, a device/compiler barrier makes externally written ordinary storage visible to following ordinary reads. Count/status are read only in that quiescent interval. An interrupt is only a notification; a barrier alone is not completion, and masking interrupts does not stop DMA.

This drain rule deliberately differs from the RP2040 datasheet: clearing EN pauses its channel with BUSY remaining asserted. The real hardware's trigger/ count reload and abort protocol, including E12/E13, cannot be inferred from this model. No physical RP2040 stop/restart or serial-loss guarantee follows. The chosen derivation is an executable synthetic driver with vendor-derived register images, not a partly implemented vendor board port.

If unread progress exceeds capacity, overrun latches and all unread bytes are discarded logically by advancing consumption to observed production. No potentially overwritten interval is returned. Repeated reads keep failing until explicit restart. The exact number of overwritten bytes is not a public result. Hardware error bits, a count above budget, or progress behind consumption produce sticky transfer_error. Exhaustion stops the epoch; its final unread bytes remain readable, and only an empty exhausted epoch reports exhausted. A count of zero is never silently reloaded by read or available.

Half-ring, whole-ring and terminal/error events coalesce into one pending bit. The handler reads and acknowledges that bit with a one-clears command; neither interrupt count nor pending-bit state is used as producer progress. The tests advance through more than two ring lengths while PRIMASK masks notification, then deliver only one interrupt and still detect loss. A modulo-only counter could not distinguish that case from little or no progress; it was rejected. No interrupt-delivery bound is needed for detection within an epoch. To avoid loss, service must quiesce before unread production exceeds capacity. A finite budget prevents counter ambiguity if service stops entirely; further requests are rejected until restart. The model records rejected DMA requests explicitly. It does not claim an infinite UART FIFO or delivery of bytes from a physical serial line during pauses, exhaustion, faults or restart.

Storage may be read/reused/released only under the relevant quiet observation and software lifetime contract. After a successful final stop and disposal of all retained references, the caller can reuse/release it. During active DMA or a failed stop, it must remain valid and reserved. Integer-pointer round trips can erase origins; protocol uses one explicitly only after successful stop to test reuse. Local origin checks reject handing a frame buffer to open, but do not enforce exclusive ownership, descriptor linearity, correct stop, external device state or arbitrary aliasing. Do not copy or mutate descriptors to manufacture those obligations away.

Application and executable assertions

The application owns a statically aligned 256-byte ring and a 64-byte scratch buffer. It initializes in start, enables IRQ0/1, polls on timer alarms and DMA hints, drains full scratch chunks immediately, echoes bytes, sets its synthetic GPIO indicator for ASCII 1, and clears it for ASCII 0. The shared notification is a latch. Interrupt-mask save/restore protects its acknowledgment; masked predicate/WFI prevents a lost wakeup. There are no exclusive accesses, hidden atomics, scheduler or fibres. Counter telemetry wraps explicitly and is not a DMA producer counter.

Overrun/exhaustion cause explicit discard/restart and increment recovery telemetry. Device error requires external repair; failure to restart, initial configuration failure, or stop timeout enters an observable nonreturning halt state, retaining static storage. This application policy handles its declared errors without turning them into implicit panic checks. D231/D232 still govern unexpected compiler checks; default panic has no mandatory source table. The protocol client independently exercises recovery and subsequent successful operation even for outcomes the application elects to halt on.

environments/cortex-m/driver.py retains literal assertions and exact MMIO traces, source inputs, compiler identity, tool hashes, commands/timeouts, compiler-generated startup/linker scripts, assembly/object/ELF/map, disassembly/relocations, closure, fresh-build comparisons and results. QEMU asserts cold boot, initialized data, BSS, immutable flash, RAM-code copying, vectors, stack/frame entry and a second poisoned reset. The device lane asserts the actual application plus empty/partial/short/full/wrapped/repeated reads, half/full/error hints, coalescing while masked, DMA progress while masked, multi-wrap overrun, sticky failures, exhaustion, delayed drain, timeout, retry, restart and storage reuse. Configuration refusals leave registers and publication state unchanged. check_sources.py checks precise lifetime and permission refusals against the same driver interface.

The separate layout control independently requires 32-bit usize, a 24-byte receiver aligned to four bytes, a 48-byte two-receiver array, and field offsets 8/12/16/20/21/22/23 for consumed/budget/config/active/quiet/lost/broken. It executes target sizeof, alignof and actual field-address differences; it is not substituted for the application's link budget.

The Python model consumes no generated declaration or generator metadata. Its literal addresses/masks and expected traces are reviewed separately from the Landin code. The inherited Cortex-M controls still execute their separate C/asm startup, hosted line transport, packed-image destructive/RO/WO/reserved/ encoded checks, source refusals and private helper controls. Those are not relabeled as compiler-owned application startup or as this full protocol. All six existing optimization/specialization profiles use unchanged protocol oracles. Link closure allows only the generated object, pinned thumb/v6-m/nofp/libgcc.a and applicable linker stubs. Resource extents and stack paint are bounded observations; complete measured firmware/stack and Landin source-debugging evidence come from environments/cortex-m/evidence.py.

Declaration, operation and historical-finding mapping

Prototype 3 Z3/Z5/Z8/Z10/Z16/Z19 and existing core/mem, core/vec, core/pool supply the relevant cross-prototype constraints: honest initialized slices, explicit origin derivation, explicit allocator capabilities, complete initialization before publication, failure rollback and manual lifetime. This driver chooses caller-provided initialized static bytes and needs no allocator. It neither forges an initialized generic slice nor stores a hidden provider. Allocator alignment/zero-size/overflow/exhaustion/rollback rules and the broader library disposition are unchanged.

Documentation facts and model premises

Vendor facts use retained RP2040 Datasheet, build 2025-02-20, version 3184e62-clean, DMA chapter and errata E12/E13, with the exact SVD/header versions/hashes and redistribution terms recorded in devices/inputs.json, devices/policies/rp2040.json and devices/README.md. The current official CMSIS-SVD register documentation was consulted on 2026-09-18 for access, modified-write and read-action metadata: <https://open-cmsis-pack.github.io/svd-spec/main/elem_registers.html>. The official vendor document is <https://datasheets.raspberrypi.com/rp2040/rp2040-datasheet.pdf>. No additional register selection or generator policy was introduced here. GNU ld's output-section LMA rules and NOLOAD behavior explain the explicit RAM LMA on compiler-generated BSS: no file payload is present, but an ELF zero-fill segment must not inherit the preceding RAM-code flash address. The nearly full application exposes this independently in the device lane; QEMU's poisoned reset verifies that the compiler still clears BSS.

Architectural CPU/exception/barrier facts retain ARMv6-M Architecture Reference Manual DDI 0419E, the pinned Arm ABI/ELF documents and GNU assembler/ linker 2.44 contracts recorded in environments/cortex-m/README.md and docs/targets.md. The GNU linker KEEP reference is <https://sourceware.org/binutils/docs/ld/Input-Section-Keep.html>. There is no VTOR, cache, FPU, exclusive-access or later-Thumb assumption. The drain acknowledgment, finite non-reloading epoch, half-ring hint, UART readiness and test-controlled timer are synthetic model premises, not architectural or vendor facts. Physical-device integration, general SVD tools, package acquisition and sandboxed orchestration remain open work in ROADMAP.md.

The freestanding evidence runner, environments/cortex-m/evidence.py, consumes this unchanged complete application and protocol. Its source-debug and resource assertions do not redefine the public driver, synthetic drain protocol, service bound or vendor adaptation above. Debugger source snapshots include the imported driver, core and generated device modules; host-side stack observations never display device registers. This mapping is not a second work authority.