Cortex-M execution profile

Selected lanes and pins

tools.lock.json pins URLs and SHA-256 for every downloaded package: QEMU and GDB, and the whole Debian 13 runtime closure they load, down to the libraries and embedded Python 3.13 a Debian 13 base image would have supplied. GCC and binutils come from the arm-elf archive whose version and checksum environments/pins.sh holds beside the host GNAT's; its GDB is built without the Python the debugger sessions run, so GDB stays Debian's. The installer verifies archives before extraction. Each probe verifies the installation inventory and versions before execution, checks it again afterward, and retains that inventory. The host supplies only the C and C++ runtimes and the Python that drives the probes, so any glibc 2.38 host runs the same locked binaries; the newest of them asks for exactly that glibc. This is a supported host profile, not a hermetic operating-system image.

These C probe flags select base AAPCS soft-float transport and ELF32 EABI. The internal Landin transport is selected separately, as the target guide describes. The compiler-generated assembly lane retains external startup/linking test support. The firmware lane uses compiler-owned reset, vectors and linking. The general C source surface remains disabled.

Memory and device map

The prototype is a sketch combining M0 CPU pressure with vendor-like registers; it does not identify a real part matching that whole map. The model is deliberately named PrototypePeripheral, not micro:bit or STM32, and lives in QEMU's unimplemented 0x40000000 window, above every Nordic device the lane touches. GPIO B, unused streams and unspecified UART registers are absent. Unknown modeled registers, invalid access directions and unsupported bus widths raise Refused, which fails the runner. Explicit halfword support covers the 16-bit count and GPIO data, without automatic read/modify/write translation. The linker refuses initialized data (this probe startup only clears BSS), a wrong vector extent, flash overflow and BSS entering the reserved stack area.

Why one QEMU

Current official QEMU documentation identifies the micro:bit's M0 and Nordic devices. Selection also inspects the pinned SoC implementation and runs the controls below. Device presence does not prove the prototype's behavior: Nordic GPIO/UART addresses differ, clock registers include stubs, and this is not a prototype DMA model. QEMU retains the mandatory CPU/startup role and the derived driver's QEMU obligation is unchanged.

The synthetic devices run on that same QEMU. The pinned SoC leaves 0x40000000..0x5fffffff to an unimplemented-device region, and QEMU's Arm target stops before an access a watchpoint covers. machine.py sets an access watchpoint on each model's window, and at every stop decodes the Thumb load or store at PC, performs it against the Python model in models.py, writes a load's destination register and moves PC past the instruction. decode accepts only the register- and immediate-offset single loads and stores; PC- and SP-relative forms and every multiple transfer are refused, so no access reaches a model unexamined. Its decoding is checked against the pinned objdump over every load and store in every image the lanes build. A DMA transfer writes RAM while the CPU is stopped, and an interrupt line is level-sensitive, as ARMv6-M and Renode's NVIC both treat it: while asserted and not the active exception, the harness keeps it pending through the NVIC's set-pending register.

Nothing here extends QEMU: the lane needs no emulator build of its own, and the CPU that executes the peripheral lanes is the one the CPU lanes execute. The harness is single-threaded and owns the only stream it reads. It replaced Renode 1.17.0, whose own threads twice put text on the console a lane's result was read from, and whose CPU descends from QEMU as this one does.

One QEMU binary still means one emulator, but not one machine. QEMU's micro:bit is a Cortex-M0 whatever -cpu says, so a corpus fixture executed at armv7-m (D255) runs on the MPS2 AN385's Cortex-M3 from the same locked binary. Its memory puts writable SSRAM at 0 and RAM at 0x20000000, so the external harness's 32 KiB/16 KiB map, vectors and stack reservation hold unchanged; the probe stub assembles under -march=armv7-m, the image must carry Tag_CPU_arch: v7 with Thumb-2, and libgcc comes from thumb/v7-m/nofp. Only the corpus runs there. The AN385 has real devices at 0x40020000, where PrototypePeripheral lives, and its flash is RAM, so no peripheral, firmware or flash-protection lane moves to it. Each image run at armv7-m is disassembled and required to divide in hardware and to ask libgcc for no 32-bit quotient, so the level is shown to have reached the bytes that ran. The three division fixtures the corpus runs at armv7-m add 12 QEMU sessions.

Executable routes and limits

Feeds happen while the CPU is stopped. The firmware then runs until it is idle -- at a WFI with nothing to take, at a branch to itself, or in a polling loop whose registers, RAM and model state repeat exactly -- or until a named stage word changes, and the lane checks it there. No host sleep and no interval decides firmware success; QEMU counts instructions for its clock, and only the debugger socket startup uses a bounded readiness poll. Stopped time is execution scheduling, not physical bus timing. The model's transfer order is an explicit harness assumption. The ordinary C buffer is reloaded across opaque memory-clobber barriers; that is no definition of Landin DMA visibility. D227 defines races, tearing, atomics, compiler/hardware barriers and cache maintenance, with models for behaviors this cacheless M0 profile cannot expose. Supplemental hardware can test actual bus/interrupt timing, electrical behavior and a real device's DMA visibility; it cannot replace the emulator gates or by itself establish language concurrency semantics.

Reproduction and evidence

On the documented native Linux host, with Python 3, dpkg-deb and tar:

python3 environments/cortex-m/setup.py
python3 environments/cortex-m/test.py
./scripts/build.sh
python3 environments/cortex-m/run.py \
  --refine compiler/ada/build/linux-amd64/debug/bin/refine \
  --output /absolute/new/evidence-directory

The default private tool root is ~/work/.cortex-m; --tools selects another installation. Every lane refuses a root holding no installation before it builds anything, naming the directory it looked in and --tools. Setup refuses an existing root; install deliberately into a new root to change tools. No sudo, host package replacement, Linux container on the Mac, Nix job or compiler dependency is introduced. Missing tools, wrong pins/host, subprocess failures, deadline expiration, model refusals, unexpected QEMU diagnostics and absent assertions all fail. A peripheral lane's result is the lane's own assertions in the process that ran the model; there is no console to scan. QEMU's log may hold only its instruction-count notice and the harness's own termination of it.

Each subprocess has a 30-second deadline, GDB 20 seconds, and QEMU startup three seconds; timeout cleanup terminates the owned process group, escalating after two seconds. A failed command's line names the command, how it ended, the limit it reached and the log it left, and the firmware lane names its case and profile ahead of it. A corpus program whose debugger session ran out says how long the program had run under QEMU and that it, not the debugger, took too long; an emulator that exited first says that instead. Each run needs a new output directory and retains failure logs as well as successes. Evidence includes exact commands, version replies, installed file hashes, input hashes, linker maps, ELF headers/attributes, sizes, ELFs, generated GDB scripts, logs, UART bytes, model traces and result.json.

The retired Linux acceptance's documents job executed both the failure controls and these live probes from the same committed archive as every native job, and job.py copied its cortex-m evidence into the exported, hash-verified bundle. Thus the annotated dual-native approval bound the environment's actual run, not only this document or a development transcript. Darwin retains native compiler/workload/LLDB evidence and does not impersonate this probe host. The environment's debugger control checks ran at routine scope with debugger coverage, which is not the full milestone matrix.

The retained development result is indexed by validation.json. Its successful probe images contain 643 and 836 text bytes respectively, no initialized data and 24 BSS bytes each. These are environment-control sizes, not measurements of the future Landin driver or a stack-usage guarantee.

Layout and ABI evidence

The same mandatory run.py also builds probes/abi.c and abi.S with the original pinned flags, startup and memory limits, then executes them in QEMU. The peripheral lane is separate; its result is never counted as ABI evidence. No library or tool pin changes. The additional ELF, disassembly, macro dump, GDB script/log, measured JSON and both layout contract inputs are retained in the run.py output directory.

Three independent comparisons meet:

1. The Ada cortex ABI suite computes scalar, aggregate, variant, evidence, any and multiple-result layouts and physical call plans from compiler packages, comparing with compiler/tests/cortex-m.contract. It also checks eight existing source fixtures through lowering and entry/direct/indirect planning under Cortex-M0 and synthetic-32, comparing detailed neutral IR. These are compiler-host tests, not target execution.
2. abi.py compares the contract with every original synthetic-32 row in layout.targets, without regenerating that golden. GCC independently lays out C control structures, unions and tables. QEMU/GDB reads their emitted measurements and compares them with the contract. Static assertions also cover data/code pointers, slices, ILP32, plain-char policy and 64-bit alignment. The C union is a representation control, not C semantics for a Landin variant.
3. Independently written assembly captures actual GCC-produced r0–r3, incoming sp and stack argument words. Assertions compare meaningful words with the compiler plan for double-word gaps, split 12-byte records, narrow stack arguments, soft floats, float-only records, promoted varargs and result-pointer displacement. Separate hand callers check GCC callees, and C callers check hand returns/callbacks, including 3/4/5-byte records and integer/double 64-bit results. Padding and skipped registers are unspecified and are not asserted as values.

The Landin convention has a separate handwritten witness: hidden aggregate result and direct/parent evidence addresses, an address-passed value, a stacked u64, successful and failing r12 outcomes, r0/r1 scalar results, multiple-result storage, and erased data/table dispatch through Thumb code pointers. GDB checks the nested r11 frame records, saved lr, chain termination and aligned sp; firmware checks callee-save registers and restoration. These execute the selected contract with real M0 instructions; they are not compiler-generated Landin calls or Landin source-debugging evidence.

Compiler refusal/boundary controls cover wrong targets, unavailable C and emission capabilities, narrow extension, the four-byte C result threshold, empty C carriers, unpromoted varargs, declared C errors, stack-budget rounding and a target-overflowing argument without materializing it. Source checks cover pointer-sized integer/address overflow and the array byte-extent boundary. The Python controls refuse duplicate/missing/invalid contract rows, synthetic mismatches, missing markers, subprocess errors and timeouts.

Every subprocess retains the original deadlines (GDB 20 seconds, build/tools 30, debugger readiness three) and owned process-group cleanup. In the retired exact-archive acceptance, the Linux documents job repeated all lanes and retained tool/input hashes alongside the ABI artifacts. Its dual-native approval bound those results to the same revision as the hosted checks. The current cortex-m gate job runs these controls through run.py. Development results are indexed separately in abi-validation.json; validation.json keeps its historical meaning as the CPU and peripheral environment's record.

These bounded probes establish neither floating arithmetic helpers, general unwind support, a complete C language ABI surface, firmware stack bounds, physical hardware behavior nor a Cortex-M compiler backend. The backend consumes the plans with native selection and frame code, compiler-owned firmware implements image placement and startup, and the freestanding evidence below establishes the bounded Landin debugging and stack evidence. D227 and D228 cover concurrency and invalid packed encodings.

Memory evidence

The mandatory run.py path additionally executes memory.py, without changing the CPU, peripheral or independent ABI obligations above. probes/memory.c executes GCC's scalar 8/16/32-bit atomic loads/stores, DMB, DSB and ISB, nested PRIMASK save/restore, pending interrupt exclusion and ordinary RAM publication in both directions across handler delivery. QEMU/GDB requires result 0x630 and no fault. These are independent C/assembly controls, not compiler-generated Cortex-M code. GCC separately compiles an atomic RMW control to an object whose unresolved __atomic_fetch_add_4 is asserted; no helper is linked or inferred as a Landin capability.

memory_model.py explores a finite FIFO store-buffer machine and compares its fenced outcomes with an independently enumerated SC permutation oracle and a separate reads-from/SC-fence constraint oracle. It checks twelve release-sequence source cases, including plain-store interruption. It also enumerates payload/notification propagation with and without the device ordering premise, split-byte tearing, DMA progress while IRQ delivery is masked, and a write-back cache-line model. The cache controls require stale reads without invalidation, visible bytes after invalidation, destructive post-receive cleaning, and loss of an unrelated dirty byte on a shared line. These assertions test the stated abstractions, not the complete Arm model or cache instructions. No absence of a weak emulator outcome counts as proof.

The prototype peripheral lane remains the executable DMA witness: static ordinary byte storage, circular overwrite, count/status updates and delayed IRQ while masked. Feeds are serialized while the CPU is stopped. D227 supplies the language contract; the model supplies only its explicit device premise. A cached profile needs platform-specific maintenance, cache levels/aliases and visibility-point evidence before it can be admitted. M0 has no cache and supplies none of that evidence. Hardware testing stays supplemental.

Each new subprocess uses the existing 30-second tool and 20-second debugger limits, three-second readiness deadline and owned process-group cleanup. Commands, logs, ELF/map/disassembly, generated controls and GDB input, tool/input hashes and memory-model.json are retained under the same run.py output directory. Native Linux and Darwin separately execute the Landin scalar and pthread ABI fixtures over their selected optimization profiles. Those results are compiler-generated hosted execution, not embedded or model evidence.

Image and access controls in development

The mandatory run.py path executes packed.py and packed_native.py. It preserves every earlier lane. EncodingPeripheral in models.py is a separate, synthetic peripheral at 0x40030000:

Pinned GCC compiles probes/packed.c to real M0 instructions. Its ordinary unsigned images enumerate all byte inputs, four two-bit indexed elements and every three-bit encoding of the independently tabulated named set 0/1/4. Firmware then performs the device accesses. packed.py asserts a literal 16-event oracle, including each direction, width, address and value; that oracle is neither generated from the C code nor derived from the model. Reading the model's final properties does not access its registers. Eight invalid direction/width/reserved operations must raise without adding an event. A destructive read is consumed once locally; a second explicit read returns zero. Write-only and one-clears commands issue no preparatory read. The count is never widened to the neighboring halfword.

The runner retains the ELF/map/disassembly, trace, tool identities, exact commands and hashes under the same run.py output directory. The existing subprocess limits and process-group cleanup apply. The new initial firmware had 660 text bytes, zero data and 16 BSS bytes before the write-one reserved-bit register was added; current sizes are retained in size-packed.log. These are control sizes, not Landin firmware or stack bounds. packed-validation.json indexes the successful development run and its independent local copy.

The C firmware is one independent control. packed_native.py separately compiles probes/packed-native.ldn using the actual native Linux compiler at six optimization/specialization profiles. Its C peer only transports explicit width/address/value commands and replies; it performs no field arithmetic, encoding validation or expected-image calculation. The native Landin program computes packed indexed updates and images, and the runner performs each transaction the peer writes against the same device model; no CPU sits between them. Every run must match the literal 16-event oracle and final register values. This is compiler-generated hosted execution against an actual peripheral harness, not compiler-generated M0 firmware. The Ada algebra suite and abstract oracle remain distinct evidence.

At each of the same six profiles, probes/packed-native-hole.ldn starts a fresh peripheral, reads the destructive register once, and extracts its unnamed mode inside unchecked. The independently specified reply is 0x9b and the complete trace is r32:4:0000009b. The native process must terminate with SIGILL, without a second access or the normal completion reply, after writing one line to stderr: the hosted trap report naming the probe's source by its file name, line 16, column 13, and bad_conversion. Discarding the extracted value cannot remove validation. The transport disables core dumps; it still contains no encoding logic. This negative compiler-generated lane complements the positive raw copy of the same invalid image and the independent C membership control.

The runner requires --refine, retains its SHA256 and --identify output, the native GCC identity, Landin/C input hashes, assembly, executable, transport commands, device trace and assertions. Compilation is bounded to 60 seconds; the native peer has a 10-second bound and a 17-command positive limit; the negative case permits exactly one command, and anything the peer writes to stderr other than the negative case's one trap report fails the lane. Tool inventories are checked before and after execution. The retired exact-revision acceptance built the committed debug compiler in its documents job and retained this lane in its verified cortex-m export. The current gate runs the lane through run.py with its built compiler. The hosted transport remains distinct from the Cortex-M emitter and generated vendor fixture lanes below. The original DMA lane continues to test ordinary externally written buffer storage under D227's explicit serialized-device premise.

The current official CMSIS-SVD register description distinguishes access permission, modified writes, read actions and reset metadata. Its format guide identifies omitted fields as reserved, without supplying one universal reserved-bit write policy. The Arm Cortex-M0 user guide requires aligned accesses for this core. These documents were consulted on 2026-09-16; they inform the explicit control contracts, not an assertion that this synthetic map describes vendor hardware. The generated device fixtures keep their own provenance, and general SVD tooling remains companion-tool work.

Compiler-generated execution

run.py preserves every earlier lane, then requires backend_acceptance.py. The same installed tool inventory is verified before and after all lanes. backend/corpus retains the complete shared runtime/ABI inventory from compiler/tests/cortex-m/corpus.json. Every ordinary runtime case uses the four inherited profiles; specialization cases add none/all and speed/all. Eleven explicit 32-bit/architecture counterparts retain the original hosted sources and independent numeric expectations. counterparts.json records exact reviewed textual differences, checked before execution. Missing/new fixtures or counterpart drift fail the supervisor. Compiler-verdict and neutral-IR golden fixtures retain their native compiler-host checks; they have no independent execution oracle.

The UTF-8 ordinal trap counterpart uses 4294967295, the largest Cortex-M0 usize, to trap outside a three-scalar view. The hosted original keeps its 4294967296 ordinal, which tests type-checking and lowering beyond u32.

The corpus keeps source refusals, the disabled general C surface and physical image limits distinct from executed programs. Every whitelisted image-limit profile is still compiled and attempted within the materialization guard; when it fits, it must execute successfully. Only a demonstrated oversized frame/static extent or the selected linker's flash/RAM overflow can produce a limit record. Missing helpers, bad instructions, wrong results and timeouts cannot. The original multi-gigabyte image and oversized hosted stress programs retain their original oracles and recorded image-limit dispositions. Their unchanged hosted execution does not become a Cortex execution claim.

The corpus inventory

compiler/tests/cortex-m/corpus.json has one row for every shared runtime/ and abi/ fixture, hosted-only ones included, keyed by the fixture's directory under compiler/tests/fixtures. A fixture with no row, or a row with no fixture, stops the corpus before it builds anything, and the refusal names each one and the row to write. A row's mode is one of:

A fixture that reads standard input cannot be execute: firmware has none to give it. A fixture with a trap_report: keeps an execute row and does not name cortex-m0: firmware keeps D232's bare trap and writes no report (D361), so the corpus runs it to its trap and checks no line, which is less than the fixture's oracle; runtime/computed-array-index-traps is one. check.py refuses such a fixture that names cortex-m0, naming this rule. Every program's line gives its verdict and its image against the map: FLASH used of 32768, RAM used of 12288 (the 16 KiB less the 4 KiB stack), each with the sections inside it, how far over the region an image that overflowed is, which the corpus measures by relinking the same objects against an enlarged copy of the map that never runs, and its three largest routines, largest routines every_kind 2940, .... Each program's result.json under the output gives every routine's size, image.routines, read with the pinned nm from the image that ran or from the measured one, so where an overflowing image's bytes go is read from the corpus rather than from tools run by hand. A profile limit no profile meets any more fails an unfiltered run, naming the fixture, its largest image, and the row to change: remove profile_limit and reason, and add cortex-m0 to the fixture's targets:. An overflow in a row with no limit fails naming its sizes and the same row.

--profile takes none-off or none/off, as the corpus line prints it. A filtered run judges no limit stale, because the profile that still overflows may be one it did not run.

backend-start.S and backend-memory.ld are small external test support: reset/vector words, bytewise initialized-data copying, BSS clearing, a stack watermark and result/fault observation. Its reset, fault and unexpected entries are _landin_harness_reset, _landin_harness_hardfault and _landin_harness_unexpected, in the _landin prefix the compiler keeps for its own symbols, so a program's own public reset links beside them. The compiler emits ordinary routines, not reset or interrupt entries. The map remains 32 KiB flash, 16 KiB RAM and 4 KiB stack. A single routine requiring more than that stack reservation is recorded as a profile limit. Returned SP, terminated r11 chain, callee-saved sentinels and a bottom watermark are asserted. The lowest changed watermark word is retained as an observation, explicitly not a proved stack bound. Freestanding evidence below records measured stack/firmware and source debugging.

QEMU uses exactly microbit, single-threaded TCG and a loopback-only GDB port. Each program has a bounded startup wait and a 20-second debugger deadline; process groups are stopped on failure. Expected traps require HardFault at the emitted UDF #1, not merely any fault. Normal results use the shared fixture's exit-byte oracle and require r12 zero. Build reports, sources, compiler identity, requested runtime helpers, the exact v6-M/nofp archive hash, empty unresolved symbol set, ELF attributes, map, disassembly and commands are retained. Assembly expansion is bounded before invoking GNU as, including nested compact repetitions, so a multi-gigabyte source image cannot materialize in the harness.

Independent controls are kept separate:

ABI, memory, frame/boundary and all four peripheral controls run all six profiles. The standalone encoding control remains independent assembly. PrototypePeripheral's count-width telemetry leaves its earlier C control and interrupt behavior intact. The hosted Landin packed-image transport remains separately identified and required.

For focused development on the supported native Linux host:

python3 environments/cortex-m/backend_corpus.py --refine PATH_TO_REFINE --output NEW_DIRECTORY --case runtime/r640-packed-hole --profile speed-all
python3 environments/cortex-m/backend_controls.py --refine PATH_TO_REFINE --output NEW_DIRECTORY
python3 environments/cortex-m/backend_peripheral.py --refine PATH_TO_REFINE --output NEW_DIRECTORY --all-profiles

Filtered commands are development feedback. The current cortex-m gate job runs run.py with the built compiler. Its mandatory backend_acceptance.py lane executes the complete compiler-generated corpus and controls under the pinned tools and records their results in backend/result.json. The retired exact-revision native acceptance separately exported artifacts/cortex-m/backend with all prior evidence. That acceptance no longer runs or approves revisions. The target guide records instruction, allocation, ABI, runtime-helper and memory decisions. Language startup/linking/sections/interrupt/naked/inline-assembly surfaces, the freestanding core and noreturn, the checked-in device fixtures and the complete driver each have their own lane below. General SVD generation stays with its companion tool. No scheduler, interrupt-masking abstraction, C source expansion or new DMA ownership model is introduced.

Compiler-owned firmware

firmware.py is mandatory in run.py. It writes records under the run's firmware output directory, separate from every earlier lane. It invokes the compiler with --target=cortex-m0 --firmware-entry=start --emit=exe and the pinned Arm GCC path. The compiler generates reset, vectors and the linker script; neither backend-start.S nor backend-memory.ld supplies these semantics. The older 533-fixture corpus, 72 generated controls and independent controls remain mandatory and retain their own startup and applicability records.

The fixed image remains 32 KiB flash, 16 KiB RAM and a 4 KiB stack reservation. D229/[1990] specify the source/request, convention, section and assembly contracts. Initialized data and .ramtext.* have separate flash load and RAM execution addresses; compiler reset copies both and clears BSS. Immutable images stay in flash. The compiler retains .s, .o, .ld, .map and ELF; the probe also retains readelf sections/program headers/relocations/attributes, disassembly, symbols, independently decoded load extents, tool identities, commands, timeouts, debugger assertions and device traces. Empty undefined symbols and explicit runtime-archive identity supplement map-based closure checks. The archive must be the pinned thumb/v6-m/nofp/libgcc.a.

The six optimization/specialization profiles each exercise:

• Two fresh builds, each cold-booted and reset again after poisoning RAM. Assertions observe initial SP/reset Thumb identity, zero reserved vectors, copied data, cleared BSS, source entry and the entry-return HardFault trap.
• Generated SVC, ordinary helper and higher-priority nested IRQ0, checking hardware frames, EXC_RETURN, every preserved register, flags, r11 records, eight-byte stack alignment and source results. A painted 4 KiB stack retains an untouched lower guard; its observed write extent is evidence for this small execution, never a whole-program bound.
• A fibre on a prepared stack (D450, D460) taking IRQ0. The handler's first instruction sees EXC_RETURN 0xfffffffd and MSP exactly where start left it when it switched away, the eight-word hardware frame at PSP inside the fibre's backing with the fibre's pc, and the painted backing below that frame untouched through the handler and a call it makes, whose frames stand below on MSP (D461). The fibre resumes on PSP with every stacked register, switches back, and start returns on MSP with CONTROL's SPSEL clear. A second build with line information is stepped through both switches an instruction at a time: GDB's walk names the leaving context's frames until CONTROL selects the resumed stack and the resumed one's after, and a prepared stack's walk ends at its start routine.
• Naked source entry selecting PSP, naked SVC returning through EXC_RETURN, and a specialized generic opaque-assembly memory write with live values. A separate naked-fallthrough image reaches its appended trap without a frame.
• Copied RAM code and RAM handler, flash/RAM veneers, integer libgcc helpers and private success/failure transport through checked ordinary calls.
• Four synthetic-device runs: DMA IRQ0 half/completion notifications, packed register images, invalid-encoding HardFault and byte transactions. The latter three execute ordinary generated programs inside a generated SVC handler. Expected values and exact access traces remain independent device-side observations. DMA continues with PRIMASK set; half notification is not completion; only observed completion plus the explicit boundary precedes ordinary slice reads.

This adds 49 QEMU sessions (48 generated, one independent C/assembly control) and 24 generated device runs. The independent control establishes PSP/MSP, four-byte interrupted SP with hardware alignment padding, nested exception returns and C callee saves independently of Landin emission. Twelve retained failure programs cover flash overflow, stack overlap, the image budget's giant image, flash and RAM (D537), missing symbol, invalid instruction encoding, later-core instruction, wrong vector placement, owned reset slot, invalid entry and reserved symbol. The flash overflow is an image the budget admits and the linker refuses once the vectors and reset code are added, so the linker stays the map's authority. A compact-images case runs scripts/image_bounds.py with this lane's assembler: compact shapes at two sizes keep the assembly and the assembler's memory to the source's size and the object to the image (D536), and the giant image is refused before any tool runs. Source unit controls additionally refuse incompatible conventions/calls, invalid naked bodies, duplicate directives, unavailable slots and hosted use.

Equivalent inputs in fresh directories must produce byte-identical ELF, object, assembly, script and map for every generated scenario/profile. ELF identity includes sections and relocations. Log paths, TCP debugger ports, command durations and host/compiler identity records intentionally vary and are retained as execution metadata, not image bytes. run.py writes these records under its firmware output directory.

For a focused development run on the supported Linux host:

python3 environments/cortex-m/firmware.py --refine PATH_TO_REFINE --output NEW_DIRECTORY --all-profiles

The contract was checked against Arm's ARMv6-M Architecture Reference Manual DDI0419E, Cortex-M0 Devices Generic User Guide, AAPCS32 and AAELF32 2025Q4, the selected-device nRF51 reference manual, and GNU binutils' section flags, retention, load addresses and Arm veneers. Executable controls establish behavior on the pinned microbit/ARMv6-M profile; they do not generalize to another core, board, real peripheral or timing model. Core/CPU-library packaging and noreturn, the generated fixtures, the complete driver, source debugging and complete measured stack/firmware evidence have their own lanes below. General SVD generation remains companion-tool work.

Freestanding library consumers

freestanding.py compiles rooted ordinary modules through the same generated reset/vector/linker path. It is mandatory after firmware.py in run.py, with its own freestanding output directory. The old 533-fixture backend corpus and the firmware lane's 49 QEMU/24 device sessions and 300 comparisons are unchanged. The shared inventory adds two explicitly restricted hosted C peers for D231/D232; neither replaces an inherited case. The declared additional lane has eleven consumers at six profiles: 198 QEMU sessions, six device runs and 336 fresh-directory comparisons. Panic consumers additionally compare optional source-map bytes. A focused run is development feedback, not a complete gate run.

The runner copies only its declared core/mem, core/vec, core/pool and platform/cortex_m/core/panic import closure. Maps must list the generated object and pinned thumb/v6-m/nofp/libgcc.a, with optional GNU linker stubs and no other LOAD input. Closure records include source hashes, selected archive members, all symbols and decoded image extents. Undefined symbols and hosted runtime names fail. This permits private compiler/toolchain helpers, not general C source. Per-command timeouts, process cleanup and independent failure markers use the existing supervisor unchanged. Standalone failures retain their logs, artifacts and failed result record.

For development on the supported Linux host:

python3 environments/cortex-m/freestanding.py --refine PATH_TO_REFINE --output NEW_DIRECTORY --case cpu
python3 environments/cortex-m/freestanding.py --refine PATH_TO_REFINE --output NEW_DIRECTORY --all-profiles

PRIMASK/WFI premises follow the official Arm architecture and M0 guides cited above; argument/result and linker-stub obligations retain the cited AAPCS32, AAELF32 and GNU contracts. Actual controls run on ARMv6-M. WFI is not a completion proof and masking does not stop DMA. The selected profile remains 32 KiB flash/16 KiB RAM/4 KiB reserved stack. Stack paint measures observed writes only. The core guide documents the public surface; ROADMAP.md owns the successor measurement gates.

Checked-in generated devices

The device guide records pinned RP2040 provenance, manual corrections, regeneration, public interfaces and unsupported metadata. devices.py follows all inherited probes in run.py, retaining its own devices output directory. Five firmware consumers at the six inherited profiles supply six QEMU sessions, 24 generated device runs and 168 deterministic artifact comparisons; a separate C/assembly control adds one device run. Seven precise source refusals and independent vendor-header/literal oracles run without network or companion tooling. The 30 selected registers are vendor data, not a faithful RP2040 model or a larger execution board.

python3 environments/cortex-m/devices.py --refine PATH_TO_REFINE --output NEW_DIRECTORY --case images
python3 environments/cortex-m/devices.py --refine PATH_TO_REFINE --output NEW_DIRECTORY --all-profiles

Compiler-owned reset/vectors/linker scripts remain distinct from the independent C/assembly startup. The new synthetic model asserts exact word transaction traces, FIFO reads, commands and bounded interrupt/DMA handoff. Its feeds and half notification are explicit premises; no circular-buffer or physical timing claim follows. Linker closure, stack paint and optional panic maps are retained with the fixed map and runtime contract. The runner uses unchanged process cleanup. The complete derived driver, source debugging and full measurements have their own lanes below.

Device descriptions

descriptions.py follows devices.py in run.py, in its own descriptions output directory, and runs nothing: RP2040 is a chip, and emulators cover cores. It builds RP2040's description, devices/descriptions/rp2040 imported under --root=devices, and the constrained reference, which a program importing no description is given (D543), and compares every fact of each linked image and its build report with descriptions.json: the device, core, boot kind, regions and placements, the vector address and length, the stack top, every reserved vector word, the handler's word, RP2040's 256 zero bytes of second stage at the start of flash and a datum placed in its SCRATCH_X. Those expectations are recorded from pico-sdk 2.2.0's memmap_default.ld, its flash-region template, its Pico board header and its intctrl.h, each by URL and SHA-256, and from [1990]; none is read from the descriptions or the compiler, so a wrong or absent fact fails. RP2040's slot 21, USBCTRL_IRQ, holds its handler, and the reference refuses slot 21 as L0347 and links zero there. It then links RP2040's program with a copy of the derived script and with four scripts each breaking one clause of D546's contract, each refused as L0519 naming its clause, and refuses link(region: "NOWHERE") as L0517. Last, a 100,000-byte static image links for RP2040, inside its 256 KiB RAM, and overflows the reference's: the image budget (D537) is the selected profile's.

python3 environments/cortex-m/descriptions.py --refine PATH_TO_REFINE --output NEW_DIRECTORY

The lanes that stage their own library, devices.py, driver.py and freestanding.py, stage platform/cortex_m/reference beside the modules their programs import, since the reference is part of every program that imports no description. The corpus still links with its probe script, which holds the reference's map, so its capacity verdicts are linked against the reference; backend_corpus.py then holds every limited verdict's measured image, largest frame or materialization to each description's capacities in descriptions.json and records them under profiles in its result. Against RP2040 and the STM32H753 that is a measurement from the images' sizes and frames, not a link or a run against their maps.

Complete derived driver

compiler/tests/driver/DERIVATION.md is the subordinate declaration/finding map and public driver contract. driver.py runs the complete application and a public-API client through the compiler-owned firmware path, across the six inherited profiles. QEMU executes two poisoned resets per linked program, checking data/BSS, vectors, immutable flash and application RAM-code copying. DriverPeripheral in models.py, served by machine.py on the same QEMU, executes GPIO, timer, UART, interrupts and ordinary-slice DMA consumption, loss detection, stop and recovery. Existing models and C/assembly/hosted transport controls retain their separate identities.

The model uses unchanged generated RP2040 images/accessors at explicit synthetic bases. Its finite, non-reloading count and EN-clear/BUSY-clear drain protocol are not RP2040 hardware claims. Masked/coalesced notifications cannot hide producer progress. More-than-capacity unread data fails with sticky overrun and explicit discard/restart. Device faults require external maintenance; an eight-poll stop timeout preserves the storage lifetime obligation. The application executes echo/GPIO commands, periodic partial-data polling, overrun recovery and observable terminal policy. Detailed premises and limitations are in the derivation.

Evidence under the run.py output's driver directory retains compiler/tool identities, source roots, assertions, timeouts, QEMU/GDB scripts, device traces, startup/linker inputs, ELF/map/assembly/object/disassembly/relocations, private runtime closure and fresh-build comparisons. NOLOAD BSS has a RAM LMA, checked independently from ELF headers; the original memory map is unchanged. Stack paint is an observation, not a worst-case bound. A model refusal or unexpected QEMU diagnostic fails the lane.

For focused development on the supported Linux host:

python3 environments/cortex-m/driver.py --refine PATH/TO/refine \
  --output /ABSOLUTE/NEW/EVIDENCE --profile size-auto --case protocol

Use --all-profiles for this complete lane. The current cortex-m gate job invokes it through run.py, preserving every earlier mandatory lane. Source refusal checks are also safe compiler-host feedback via compiler/tests/driver/check_sources.py.

Freestanding evidence

The mandatory run.py entry invokes evidence.py after every inherited lane. It builds the complete application, protocol client and layout control with --target=cortex-m0 --firmware-entry=start --emit=exe --debug=lines in all six optimization/specialization profiles. The Cortex debugging contract is line/function debugging with ordinary-frame CFI; full variable/type debug remains refused. QEMU runs source breakpoints, stepping and call-stack assertions, including imported core/device code, copied RAM code, veneers, interrupts, generic/specialized allocation, noreturn and panic paths; the application's session runs GDB through the harness's relay, so the driver's device serves it and monitor feed, tick and delay_stop drive it. Separate symbol selection refuses stale executable, assembly, table and source inputs.

scripts/cortex_debug.py reads ELF32 headers directly. Flash is the highest physical end of a nonempty PT_LOAD payload, measured from flash address zero, including vectors, gaps, immutable data, private helpers, veneers, initialized RAM and RAM-code load images. Static RAM is the highest RAM PT_LOAD memory end minus 0x20000000, including alignment and zero-fill. Segment payload sums and section/symbol extents are retained separately, so neither ELF file size nor a sum that omits alignment substitutes for the occupied extents. Linker maps retain the exact compiler object, pinned private archive members and linker stubs. Section flags and file ranges establish that debug metadata is not loaded. Debug and nondebug LOAD contents/addresses/zero-fill extents must match.

resources.py executes the unchanged complete application through cold boot, partial and wrapped reads, coalesced half/full notifications, delayed drain, overrun/discard/restart, later successful echo, timeout, open failure, external repair-required failure and a complete finite 65535-byte epoch. The epoch services each 256-byte batch before the next, checks every cumulative count, echoes the final short read and then observes exhaustion/restart. The separate protocol client preserves its independent exact transaction and unsafe-source oracles; these application scenarios do not replace it.

Stack paint reports the lowest changed byte, not a worst-case bound. A retained disassembly-derived site list observes every emitted SP-changing instruction's successor, every function entry, including private helpers and veneers, and every exception handler's entry. StackObserver in resources.py reads SP, frame/LR and IPSR on the host at a breakpoint on each site; it adds no firmware instructions, storage or device reads. Its minimum retains the actual ordinary frame records and stops following an EXC_RETURN record. Guards, written extent, reserved extent, scenario and sample counts are retained. Hardware exception stacking is observed at handler entry. The independent stack-control.S uses external startup, deliberately reserves 256 unwritten bytes, then exercises 36-byte aligned exception entry, 8 software-save bytes and 32-byte nested entry. QEMU register assertions and the observer independently distinguish 256 reserved bytes from 80 painted bytes. Application measurements do not claim every possible interrupt arrival, nesting, future input or stack bound.

The observer's breakpoints are debugger breakpoints: QEMU checks them in translated code, so a site in copied RAM code is observed without patching its bytes, and a breakpoint's instruction is executed by a single step. Each sample is a debugger round trip, so the exhaustion scenario -- 65,535 bytes through the ring, about four million samples -- is measured by paint alone; every other scenario, the helper and veneer controls and the independent calibration run under the observer. The fixed Cortex profile and firmware bytes are unchanged. Every process has a bounded timeout and failure record.

Two controls at every profile serve the stack switch. switch builds runtime/stack-switch-frames as firmware, its main entered from a start, and runs the session every target runs (compiler/tests/debugging/switch_frames.py, D469): stopped in a fibre the backtrace ends at landin.stack_start, and stepping two switches an instruction at a time the frames above landin.stack_switch are the leaving context's until MSP, PSP or CONTROL is written and the resumed one's after. capacity measures probes/fibre-capacity.ldn, a taker and an answerer fibre admitted to a group over core/fibre's round of turns, whose idler waits for an interrupt, exchanging six requests through a ring while SysTick counts ticks, their stacks cut from one fixed 2,992-byte module buffer (D470). accounting() identifies that buffer and the round's state in static RAM from nm -S, the main stack below the reset pointer and the whole buffer are painted at start, and each fibre's peak is read below its stack's top when the firmware returns. The control writes capacity.json and capacity.txt beside it and fails unless the consumer fits; the evidence directory's capacity.json and capacity.txt hold every profile's, and the gate's cortex-m job keeps them. Its tick is core/atomic's sole_add in SysTick's handler (D511). At none/off it uses 23,268 bytes of flash and 3,072 of static RAM, of which the fibre buffer is 2,992; with the 4,096-byte main-stack reservation, painted to 1,644, that is 7,168 bytes of reserved RAM, counted once. Each fibre's backing is 1,472 bytes, a 32-byte record and a 1,440-byte stack whose limit stands 384 bytes above its base (D472), painted to 904, 940 with D461's exception frame; both are live at once, 2,944 bytes. The size and speed profiles use 20,632 to 20,660 bytes of flash and paint at most 848 in a fibre and 1,396 on the main stack. With the tick written over the builtins directly, as it was before the wrapper, the same compiler used 22,492 and 19,916 to 19,944 bytes of flash and painted the main stack to 1,472 and 1,248: a firmware image keeps every scalar's cell entries, since a program without a public main keeps everything (D296), and the handler's two calls deepen the main stack. Every profile fits the 32 KiB flash, 16 KiB RAM profile. Paint is this run's deepest write, not a bound.

Artifacts under the run.py output's evidence directory retain sources, identities, commands/assertions/timeouts, ELF/object/assembly/linker/map/disassembly/debug records, closure and resource JSON, source-selection failures, measured SP/frame snapshots and repeat-emission comparisons. Debug CUs retain their compilation directory, so deterministic debug comparisons repeat within that directory; relocation does not imply identical source identity. The current cortex-m gate job runs this lane through run.py with the compiler built from its checkout. Physical board testing remains supplemental and is not claimed by these emulator lanes.