Target contracts

The Linux x86-64, Linux arm64 and Darwin descriptions all use 64-bit pointers, eight-byte pointer alignment, sixteen-byte stack alignment and little-endian storage. Equal widths do not imply equal calling conventions, and an equal architecture does not either: linux-arm64 and darwin-arm64 are both compiler.arch == arm64 and select different C ABIs, object formats and hosted systems. Darwin enables C signatures, C records, variadic calls and native Mach-O emission. --target=darwin-arm64 --emit=exe selects /usr/bin/clang -arch arm64; --toolchain=PATH explicitly overrides the driver. A build that names no target is for the compiler's own host (D257): the triplet refine was built for, so a Mac's compiler defaults to darwin-arm64 and Linux arm64's to linux-arm64, and cross-compilation is always explicit. --debug=full selects native DWARF and dSYM packaging on Darwin; the synthetic target has no debug capability. The synthetic 32-bit seam has no emitter, object format or C ABI.

Darwin transport follows Apple's ARM64 platform ABI and the Arm procedure-call standard, checked against the Apple tools and SDK pinned in environments/macos-arm64/policy.json. Integer/pointer arguments use x0–x7, float arguments v0–v7. Homogeneous float aggregates of up to four leaves use the float bank. Other aggregates through sixteen bytes use integer chunks; larger values use caller copies and pointers. Indirect results use x8 without consuming x0. Fixed scalar and homogeneous floating aggregate stack arguments keep their natural size and alignment; other fixed aggregates occupy whole eight-byte slots aligned to at least eight. Promoted variadic tails use eight-byte stack slots. Narrow integer arguments are extended by the caller. The native C differential corpus covers both call directions, bank exhaustion, partial chunks, nested arrays, callbacks and large results.

Every emitted routine keeps an x29/x30 frame record; sp is sixteen-byte aligned and x18 is unused. Native Landin calls use eight integer bit carriers then stack slots, address-based aggregate transport and a separate w8 declared-error carrier. The backend emits already verified cleanup edges. Stack growth touches each 4 KiB page. Frame/incoming/outgoing/copy preflight retains a signed-2-GiB budget. Conditional transfers to local labels use one direct branch when conservative byte accounting proves the target is in range (±32 KiB for test-bit branches, ±1 MiB for other conditional branches). Distant or unproven targets retain an adjacent inverted conditional branch followed by b; that branch still requires the architecture's 128-MiB reach. The recorded broader resource/scaling limitations remain; this adds no recovery guarantee for arbitrary exhaustion.

Darwin's hosted providers reach libSystem through platform/posix over platform/libc: anonymous mappings for the heap's size classes, open/read/write/close and immediate errno capture through __error, with Apple's open flags. open is called as the variadic function it is, so its mode takes Apple's variadic placement, every unnamed argument in its own eight-byte stack slot. The platform's ordinary startup and libSystem come from the native Apple driver.

Every ELF backend, x86-64, arm64 and RV64 on Linux and FreeBSD alike, emits each routine, datum and conformance table in its own input section and links with -Wl,--gc-sections; Cortex-M does the same under its own linker script. An executable keeps only what the entry, a C object or another kept section reaches: a library routine that is declared but never called, or reached only from an unreachable routine or datum, is absent along with its libc dependency. Darwin's Mach-O assembly splits into atoms at its symbols (.subsections_via_symbols) and links with -Wl,-dead_strip, which drops the same. The hosted entry calls platform/posix's C-callable argument initializer when the program defines it, and a C-owned startup can call it by the same name.

Library requests retain source order and repetition, and each reaches the driver as -lNAME after the assembly on every hosted target (D523), so the driver resolves it as it would for C, a shared library before an archive of the same name where its linker prefers one. Each -L and linker.directory directory comes before the assembly as -LDIR and -Wl,-rpath,DIR, -L's first (D524). Only after a failed link does the toolchain package name the files a library may be, libNAME.tbd, .dylib and .a on Darwin and libNAME.so and .a elsewhere, for the driver to look for them (D525). Linux keeps GNU build-id arguments; no GNU build-id flags reach the Darwin driver. Caller-source sidecars use the Mach-O identity contract below.

Only an export is a global symbol (D415): the hosted or firmware entry, C imports and public C definitions, anything with a link name, a public definition in a machine convention and a Cortex-M placement. Every other routine and datum is local to the image under its own name, on every backend, so it can neither collide with nor replace a C library's or a linked object's symbol. Inside the one assembly file a program emits, an item whose name another item holds and that is not an export takes its module-qualified spelling, core.arena.reset, as [1975] states (D417); symbol allocation is the same in every backend. On ELF a local symbol is STB_LOCAL, t or d in nm; on Mach-O it lacks N_EXT.

A logical external name such as _entry stays unchanged in checking and IR. The target mapping yields _entry on ELF and __entry on Darwin. Quoting an assembly operand is a later rendering step, and a leading underscore in source does not escape the platform prefix. The same mapping applies to explicit native names and C imports/exports, the argument initializer among them. Local labels are allocated separately. Existing ELF spelling and golden records remain valid.

Linux link modes

--link=static|libc chooses how a hosted executable is linked (D280), and Linux is the one hosted system with a choice. The default, static, links the program alone: the driver adds platform/linux from the library beside the compiler as an implicit root, and passes -nostdlib -static -no-pie -Wl,-e,_landin_start and -Wl,--gc-sections to the target's driver, so no C runtime object, C library or dynamic loader is linked and the process starts at platform/linux's _landin_start (D279). --link=libc keeps the C runtime's link, main called by C's startup, library requests and libc among them. Darwin and FreeBSD reach their systems only through their C libraries, so libc is their only mode and --link=static there is L0002, as is --link for a target with no hosted system or without --emit=exe or --emit=asm.

A static request is refused with L0500 before any tool runs, and the note names --link=libc, when no library holding platform/linux was found, when the program asks for linker.library or linker.directory or the request names -L, or when it refers to a bodyless external symbol that no program item defines. That last check counts only what the entry reaches, as the link keeps it: every Linux backend collects per-item sections, so a reference from an unreached routine never reaches the linker. It follows calls and addresses taken from _landin_start, a C name to the routine that defines it, main, the argument initializer and the panic handler, and counts whatever a datum or an evidence table names whole. -v, --dry-run and the build report name the mode. An emitted .s under static mode includes platform/linux, and it still links under an ordinary C driver; with no library holding platform/linux, --emit=asm is refused as an executable is rather than written without its entry (D363).

The driver is the first of the GCCs a distribution installs that the host can start (D364): the target's own triplet name, x86_64-pc-linux-gnu-gcc on x86-64, then MACHINE-linux-gnu-gcc (Debian and Ubuntu), MACHINE-redhat-linux-gcc (Fedora) and the other vendor spelling, then gcc when the target is the compiler's own host and never for a cross target. --toolchain=NAME is the only one tried when given. Whether one can be started is asked after the program's own refusals, D280's among them, and before anything is written; with none, L0500 names every name looked for and the package to install. The executable's assembly is removed after the link unless --keep-asm keeps it or a source map beside the executable names it, and refine compile program.s -o program links an assembly file with the same driver and arguments (D362).

Linux arm64

--target=linux-arm64 is the arm64 backend's second description. Instruction selection, frames, the native Landin convention and the levels are Darwin's; what differs is chosen by three questions, each asked of the description rather than by comparing it with Darwin's:

The driver is aarch64-linux-gnu-gcc, the name the pinned aarch64 GNAT installs and Debian's cross compiler too, then the others D364 names. Under --link=libc the program links as a position-independent executable, the driver's default, which the arm64 addressing already is; the default static link is fixed-address, as on x86-64. Linux's library spelling and build identity apply as on x86-64. The assembler is held to the level at every level with -Wa,-march=, the baseline's armv8-a included; an arm64 executable carries no level note. x18 is never allocated and stays reserved for assembly blocks, as on Darwin. The hosted entry and the panic edges are Darwin's instructions; hosted/system, hosted/blocking and hosted/events make Linux system calls through platform/posix and platform/linux.

C aliases and generated bindings

platform/c asserts compiler.c_sysv_lp64 or compiler.c_darwin_lp64 or compiler.c_aapcs64_lp64 or compiler.c_riscv_lp64d, and its c_char is u8 under standard AAPCS64 and RISC-V LP64D and i8 otherwise. Each fact identifies its own implemented ABI, not LP64 generally. Generated bindings assert the selected fact. The generator supports x86_64-pc-linux-gnu, the pinned arm64-apple-macos26.0.0 deployment triple and aarch64-unknown-linux-gnu, independently probing Clang's triple, macros, data model and plain char. The native Apple corpus regenerates all binding categories, including TLS, nullable callbacks and incoming-varargs adapters, and compiler/tests/linux-arm64/bindings.py does the same natively on Linux arm64; existing Linux x86-64 generated files remain unchanged.

CPU feature levels

A build assumes one CPU feature level of its target's family (D255), given with --level=NAME or the language server's level option and resolved after the target, so a level of another family is L0009. refine --identify lists each target's levels. The level is a value beside Target_Facts, so every capability query above, and every layout, calling convention and C ABI, is the same at every level of a family.

The x86-64 assembler is held to the level at every level, the baseline's plain -Wa,-march=generic64 included, so an assembler.block using a v3 instruction is refused by the assembler unless the build assumes v3. All arm64 targets emit .arch at both levels, and Linux arm64 also passes the level to the assembler, so an assembler.block using an LSE instruction is refused unless the build assumes armv8.1-a. The test program holds each Linux lane's own assembler to that, below and at the level, and a build that names a family's default is the build that names none, byte for byte in its assembly, its tool invocation and its build report. The default Cortex armv6-m level likewise names its CPU in both tool arguments and assembly directive. The pinned GNU assembler does not accept the psABI's x86-64-v3 spelling as -march, so the level is spelled generic64 with its extensions; above the baseline the linker's -z x86-64-vN writes the level into the executable's GNU property note. A libc-linked executable is refused by glibc's loader when the processor lacks its level; a static Linux executable carries the same note, which no loader reads, and platform/linux's entry refuses it instead, before main, with status 127 and one line on standard error (D284). Linux arm64 and RV64 executables carry no note: a static build is held to its level by the entry, through AT_HWCAP and riscv_hwprobe (XTheadBa excepted), and a libc build is not held to it. Darwin's lowest processor, Apple's M1, has more than armv8-a; the default assumes less than any Mac has, which is sound, and a build for Apple silicon may select armv8.1-a. Each test lane runs the levels a runtime fixture's levels: names for its own family, and runs one only once the processor that runs the lane confirms every feature of it. A native Linux lane reads its host's /proc/cpuinfo; a cross Linux lane asks its runner rather than assuming an emulator has everything, because QEMU's -cpu cortex-a53 has no LSE, so a C program the lane's driver links copies /proc/cpuinfo as the runner presents it; on a Mac the test program asks the hw.optional.arm sysctls FEAT_LSE, FEAT_CRC32 and FEAT_RDM, and the Darwin lane FEAT_LSE. A level nothing confirmed fails as UNVERIFIED rather than being skipped, and is never inferred from the default's run or from another target's lane. The test program says on standard error which levels were confirmed and by what. Each lane requires the executable it ran to show the level: the ISA note on Linux x86-64; on arm64 the LSE instructions and no exclusive loop, ldxr or ldaxr and stxr or stlxr, at armv8.1-a, and no LSE instruction in the default's image of the same fixture; and hardware division and no 32-bit helper on Cortex-M, where armv7-m runs on QEMU's Cortex-M3.

FreeBSD hosted targets

freebsd-x86-64 and freebsd-arm64 use the existing x86-64 and arm64 ELF emitters. Their LP64 C transports are SysV AMD64 and standard AAPCS64, respectively, with the existing C ABI configuration facts, plain-char signedness, alignment and arm64 register rules. The hosted system is selected separately: __error supplies thread-local errno and the create/truncate open flags are BSD values. compiler.os == freebsd selects the private 224-byte stat record in hosted/system; a C peer checks the actual headers, record extent, alignment and field offsets on each architecture.

The cross driver is Clang against the checked FreeBSD 14.4 sysroot, using LLD and FreeBSD startup and libc. A caller can name its driver with --toolchain=. The default names are x86_64-unknown-freebsd14.4-clang and aarch64-unknown-freebsd14.4-clang, wrappers supplying that sysroot. Clang's integrated x86 assembler does not restrict every instruction by -march, so Landin's x86 driver requests GNU as and supplies the selected feature whitelist. Arm64 selects the architecture in both assembly and Clang's -march= and preserves public dot-prefixed foreign symbols with -Wa,-L. That keeps every private .L label as a local symbol too, so every FreeBSD link passes -Wl,--discard-locals, which drops the local ones and keeps the global; without it LLDB named a routine after a label at its address (D475). FreeBSD emits no CPU-level loader-refusal contract.

The FreeBSD lanes emit on Linux and execute in official, checksum-locked FreeBSD VMs. Each architecture has separate runtime, ABI and LLDB verdicts. The guest confirms x86-64 v3 using CPUID and enabled AVX state, or armv8.1-a using FreeBSD's auxiliary-vector LSE, CRC32 and RDM bits, before higher-level execution. The shift and atomic fixtures execute at both levels; disassembly checks the linked executables. A missing feature fails the lane. The ABI selection is nonempty and uses independently compiled C peers for imported/exported scalar, aggregate, callback and variadic transport.

The native guest LLDB sessions run at four optimization/specialization profiles and inspect nested source stops, callee and caller local values, frame chains and return unwinding. ELF range/location references carry section relocations, so preceding DWARF contributions from FreeBSD startup objects cannot redirect a lexical scope to another object's range list.

Native source debugging

refine --target=darwin-arm64 --debug=full --emit=exe program.ldn -o program produces program.s, program.o, program, program.dSYM and program.sources.json. Apple Clang receives -gdwarf-4 -x assembler and -save-temps=obj; explicit assembler input prevents preprocessing from rewriting the compiler assembly. The language selection resets before library arguments. Clang invokes its native dsymutil after linking. Output preflight protects the retained object and dSYM bundle as well as existing artifacts.

Open lldb ./program, then use breakpoint set -n main, breakpoint set -f program.ldn -l 12, run, next, step, bt and frame variable. The dSYM can accompany a deployed executable without its object file; source text must remain available for source listing, or be remapped using LLDB's target.source-map setting.

Backend.Dwarf shares represented type, scope and availability serialization. Each backend supplies the same placement plan it uses to emit instructions. Darwin's frame base is DWARF register 29 (x29), with negative frame-relative homes and dereferences for indirect bindings. CFI describes x29/x30 saves, the CFA at x29+16 and each return's restoration. The frame pointer remains present with debugging disabled. No Darwin fact enters parsing, checking or neutral IR semantics.

Apple's dsymutil requires a relocatable compilation-unit low address when rewriting the selected location/range lists. The Darwin encoder supplies it; ELF retains its existing address-base convention. Both formats now describe empty payload structures without claiming child DIEs, avoiding the native verifier warning while retaining the same represented byte size. Native object and dSYM verification and LLDB sessions check the result. Compilation-unit and assembler line tables use DWARF 4; the native CIE is version 1. These are output encodings, not IR versions or language rules.

Debuggers display Landin's represented types through their C presentation. A variant is a truthful tag plus named payload overlays; users select the active payload using the tag. An atom set is an enumeration of its atoms with this program's codes, so a value prints as its atom's name (D423). A generic instance is a local symbol named after its routine (D421), as nm, perf and a backtrace show it.

A file of a library module is recorded in the line table and the source map as /landin-library/, its module path and its name (D422), so neither depends on where the library was installed. Map the prefix to the directory refine version prints to read those files in a debugger:

gdb -ex "set substitute-path /landin-library $(refine version | sed -n 's/^library: //p')" ./program
lldb -o "settings set target.source-map /landin-library /path/to/library" ./program

In GDB a breakpoint by a library file's module path, core/vec/vec.ldn:120, needs no mapping; showing its source does.

LLDB canonicalizes scalar display names, such as i32 to int. It does not evaluate Landin expressions. Source aliases from matches, named-result destructuring and loops remain inspectable in their live scopes. On arm64 source slots keep stack homes without optimization and at size; at speed a slot may hold a general or d register, and its location follows that register over its interval. Uninitialized or unavailable variables have no valid location, and ranges end before frame restoration. The complete parser, containers and hosted application run in the native LLDB matrix, using the existing Linux source/value oracles.

An assembly block has the line its source gives it: the instruction's line entry covers the loads of its inputs, the text and the stores of its outputs, and a source breakpoint on it stops before any of them. Each output is an ordinary local from the next line on. A callee-saved register the block declares is saved with the others and described by the same CFI, so the caller's frame shows its own value; the GDB session asserts rbx there on every profile on Linux x86-64 and x19 on Linux arm64, and the LLDB session x19.

Linux arm64 debugs as Linux x86-64 does: the same ELF DWARF 4, the same GDB sessions over the same sources and workloads, the same GNU build ID and source maps, with the frame base x29 and the CFA at x29+16 that Darwin's CFI describes. ./scripts/debug.sh on an arm64 Linux host runs them with the GDB the pinned aarch64 GNAT bundles; --target=linux-arm64 --qemu qemu-aarch64 --driver DRIVER runs them anywhere else under QEMU's GDB stub. On either, GDB's backtrace ends at main by default; set backtrace past-main on shows the _landin_start_main and _landin_start frames below it, as the panic sessions do.

Exact identity and optional deployment

The map's build_id is the full SHA-256 digest of the compiler assembly and its selected source snapshots, including filename bytes and source hashes. The backend adds that digest to __TEXT,__landin_id, without filenames. It therefore contributes to the native linker's LC_UUID, including when only a source comment changes. The map separately hashes the final emitted assembly. The Apple-generated UUID matches the linked executable to its dSYM; the full Landin digest matches that executable to its caller/source table. The original caller sidecars alone did not provide this Mach-O binding.

python3 scripts/source-location.py program.sources.json 2 11 12 \
    --macho program --dsym program.dSYM/Contents/Resources/DWARF/program

Lookup refuses a mismatched digest or dSYM UUID. The native reader supports the implemented thin arm64 Mach-O target and validates load-command bounds; universal binaries are outside this target contract. --assembly remains available, and Linux retains --build-id with the full GNU build ID. These identities match builds; they are not signatures or tamper-proof attestations against a modified executable.

--debug=none remains the default and emits only a caller-needed source map. Neither that map nor source filenames need deployment. strip -S -x removes optional source-debugging information from a copy while preserving executable behavior, the identity section and UUID. When debugger acceptance is selected, it runs the copy alone in a fresh deployment directory, refuses source breakpoints without debug artifacts, and separately resolves its caller coordinates against retained matching data.

Platform references, checked against the pinned Apple tools: Apple debug artifacts and UUIDs, dsymutil, Arm DWARF register assignments, and LLDB scripting.

Cortex source debugging

refine --target=cortex-m0 --firmware-entry=start --emit=exe --debug=lines adds DWARF 4 line tables, source function identities and ordinary-frame CFI. The pinned Linux-hosted GDB 16.3 connects to the QEMU microbit CPU lane, or through the peripheral harness's relay to the same QEMU with the driver's synthetic device behind it. Native Linux GDB and Darwin LLDB acceptance remain separate.

--debug=full remains refused on Cortex. lines advertises no source locals, arguments, types, expression evaluation or optimized-value locations. It emits no variable/type DIEs or location lists. A source line removed by optimization has no guaranteed stopping address; emitted generic specializations retain the template's source name/coordinates, and a source breakpoint can select multiple instances. Hosted targets retain their existing full contract and refuse lines, rather than silently substituting a different interface.

Ordinary routine CFI describes callee saves and the changing CFA through prologue/epilogue. Framed routines describe their previous-r11/incoming-lr record; eligible leaves describe SP-relative homes without that record. Interrupt and naked routine CFI explicitly makes LR undefined: ordinary unwinding stops there. EXC_RETURN is never an ordinary return PC. Hardware exception entry, alignment padding, nested exception records and restoration have independent executable controls. An ordinary block has its source line, and the platform/cortex_m source session stops on disable_interrupts' block with PRIMASK clear and steps past it to find it set. Naked assembly has a source function/declaration boundary, not line-by-line locations inside its assembly string or an inferred stack frame. Linker veneers have no Landin source line. Use an explicit callee breakpoint when source stepping across a veneer skips the callee; call stacks in the Landin caller/callee and returns through flash/RAM veneers are tested.

The shared DWARF encoder consumes existing source provenance; Cortex register numbers and CFI stay in the backend, outside target-neutral IR. Reset and unhandled-exception CFI terminate unwinding. Copied RAM code carries its RAM execution address, while resource accounting includes its flash load image.

Before attachment, scripts/cortex_debug.py checks the selected ELF32 ARM load image against the symbol ELF, their nonallocated .landin_id against the source table, the assembly digest and every source snapshot digest. The reference runner fails on missing debug sections, a changed executable, stale assembly/table or changed source. A stripped deployment image can use matching separate symbols; ordinary debug stripping retains the nonallocated identity. This is artifact matching, not authentication against forged inputs or protection against concurrent filesystem replacement.

python3 scripts/cortex_debug.py firmware.elf --symbols firmware.elf \
  --sources firmware.elf.sources.json --assembly firmware.elf.s \
  --source-root BUILD_DIRECTORY

Debug sections, source snapshots, optional panic maps and generator provenance are off target. Acceptance compares complete ELF LOAD images between none and lines, including zero-fill extents, and checks that debug sections neither allocate storage nor overlap load payloads. No debugger helper dereferences a source device pointer or reads destructive registers to display a value.

The decisions use GNU CFI directives, GDB ARM behavior, DWARF 4, and Arm DWARF32 2025Q4, consulted on 2026-09-18. The acceptance tool versions remain pinned; no network access is needed to repeat these tests.

Hosted parity and physical limits

The shared target applicability matrix and native parity path distinguish language behavior from platform transport and packaging. The two hosted backends run the same runtime profiles and complete prototype derivatives. Architecture-selecting source, C register rules, symbol prefixes, archive availability and native trap delivery have explicit executable counterparts. The fault-endpoint adapter changes only fixture host services, never parsing, checking, neutral IR or the Landin program's expected failure behavior.

The existing 2 GiB zero-reserved-global regression exposes a limitation of the pinned Darwin default executable layout: dyld aborts before main when the image reaches the shared-cache region. The native Clang control has the same failure. Apple's shared-region constants place the arm64 shared region at 0x180000000; the default executable starts at 0x100000000. These observed layout limits do not define different array semantics. Darwin now emits the complete wide element address, and all four profiles retain successful assembly/linking followed by the original failed status-42 execution and matching control. The result is explicitly platform-limited; no passing runtime verdict or general large-image support is claimed. Large-image placement and preflight belong to the scale and self-hosting successor, with an explicit activation condition. No giant materialized object sweep or new exhaustion guarantee is introduced.

Deterministic artifacts

[1550] says the compiler emits deterministic assembly text and relies on the platform's assembler and linker. The relation that sentence needs is stated here and gated by compiler/tests/test_determinism.py, which the gate runs with both compiler build modes on Linux and on macOS. The test exercises each target's default CPU feature level.

Two compilations are equivalent closures when they agree on the source bytes, the module closure, the target, the selected CPU feature level (default or explicit), --optimize, --specialize, --build-mode and the pinned compiler. They may differ in the absolute build directory, the working directory, the output path and name, the whole environment and in how often and in what order they run.

The last row is measured, not assumed. On the pinned Linux toolchain two links of one unchanged assembly differ in six bytes, in the same directory and from the same command, because x86_64-pc-linux-gnu-gcc writes its random temporary object name (ccXXXXXX.o) into the symbol table, and the Linux arm64 driver does the same. Darwin's came out identical, which is one toolchain's tidiness rather than a contract. The gate therefore checks that the assembly the link consumed was byte-identical and reports the image residue; a reproducible hosted image belongs to the release readiness successor.

The debug row is a declared record and not a defect: comp_dir and .file are how a debugger finds source, and the panic map resolves an off-target check site back to the file the caller named. Canonicalizing them away would buy byte-identity across directories at the price of a debugger that cannot find source. What the gate does instead is pin how they may vary — when only the compilation directory moves, the debug assembly may differ in the recorded directory and the identity derived from it and in nothing else, so an instruction that followed the build directory fails.

Caller coordinates emit a source map even at the default --debug=none. Changing only the source-path spelling changes its path_hex file entries, the map's build_id, the identity comment and any identity section in assembly, and therefore the map's assembly_sha256. --panic-map has the same path dependence. The path-independent assembly claim applies only when no source map is produced; a changed caller path does not change the program instructions.

The Cortex-M device check builds each fixture in two output directories with the same relative source-path spelling. Its artifact comparison therefore does not claim identity when the source-path spelling changes.

Cortex-M environment boundary

The execution profile pins QEMU's Cortex-M0 micro:bit CPU lane and a synthetic peripheral lane on the same QEMU. C/assembly probes establish the environment. Layout and ABI planning follow below, then compiler-generated M0 execution and compiler-owned firmware startup and linking. The original synthetic-32 goldens remain unchanged.

Cortex-M0 layout and ABI planning

Targets.Cortex_M (cortex-m0) defaults to ARMv6-M Thumb, little endian and base AAPCS32 soft-float identity. refine --target=cortex-m0 checks source and emits ARMv6-M assembly at the default armv6-m level; selecting armv7-m or armv7e-m permits instructions from that higher level while retaining the same layout and ABI. The toolchain identity is arm-none-eabi. Executable requests require the explicit --firmware-entry=NAME source identity (D229); missing or invalid entries report L0502. C signatures, records, varargs and standalone object output remain disabled; the explicit lines source-debug contract is described above. The independent external startup/linker harness remains distinct from the compiler-owned firmware path. platform/c accepts the explicitly implemented hosted C ABIs; the separate header generator supports its declared target set, and Cortex C remains disabled.

D231's infallible noreturn is shared across target descriptions. Its signature identity survives ordinary function values, generics and erased evidence. An ordinary Cortex firmware entry may use it; interrupt/naked signatures remain ()->none. A violated nonreturning-call promise traps after the call on every backend. Hosted C signatures support it within their existing ABI; Cortex continues to refuse the general C source surface.

The existing scalar and recursive shape machinery supplies all byte placement; there is no separate Cortex layout algorithm in checking or neutral IR.

Distinct wrappers retain their base representation. Caller coordinates retain D192's three u32 fields (12 bytes), rather than turning into pointer-sized integers. The 32-bit maximum object extent is 4294967295 bytes; it is a layout arithmetic limit, not an available-RAM promise. The selected probe image still has 32 KiB flash, 16 KiB RAM and a 4 KiB stack reservation. D228 packed images use the same target facts; over-aligned source types and deferred scalar widths remain unavailable.

Backend.Arm32_ABI derives placement from neutral signature parts, including entry signatures and direct/indirect call operands. It selects the convention explicitly; a four-byte pointer never implies compatibility. The external C planner follows AAPCS32 2025Q4: r0–r3 precede the stack, double-word arguments start at even registers or 8-byte stack addresses, and a composite may split at the register/stack boundary. Narrow integers extend to 32 bits. Stack argument extents round to four bytes; the total outgoing area rounds to eight. Soft-float values use core bit carriers, including float-only records; there is no HFA register bank. C composite results through four bytes use r0; larger results use a hidden address in r0, consuming that argument position. Scalar 64-bit results use r0/r1. Variadic tails use this same base PCS after default promotions, with unpromoted tails refused by the planner. Empty/non-C/variant records and Landin errors or multiple results are outside the C boundary.

The internal Landin convention uses the same scalar/word placement but passes aggregate, array, slice and any values by address, with the required callee value copy. inout instead carries the original place address. Aggregate and multiple results always use caller-owned storage, even below five bytes. Its address comes first; the existing signature's generic evidence pointers follow in D144 order, then written parameters. Static type/fixed parameters consume no runtime position. Erased dispatch inserts its data pointer in the provider's self position, without a hidden table argument. Declared failure uses r12: zero on success, otherwise the nonzero atom code. Successful scalar results remain in r0/r1, and failed calls promise no successful result. C calls do not preserve this internal error carrier. Linker call veneers may clobber r12 on entry; it is only an outcome after the called routine returns.

Call-bearing and other framed Landin routines keep r11 pointing to an eight-byte record: previous r11 then incoming lr. Publish the frame pointer only after constructing that record. Eligible leaves use SP-relative homes, leave r11 and LR untouched, and save only the low registers their body uses. Preserve r4–r11 and sp, reserve r9 from allocation, treat r0–r3/r12/lr and condition flags as call-clobbered, maintain sp modulo four at all times and modulo eight at calls, and allocate no red zone below sp. The backend implements this record and checks framed construction through instruction stepping, including nested calls. Eligible leaves have separate SP-based unwind evidence, including selection of the interrupted hardware context. Ordinary unwinding still stops at interrupt entry. The earlier handwritten witness remains independent evidence. GCC's C routines may use r7 as a local frame base; no continuous mixed-C r11 chain or foreign-exception unwinding is promised. Code addresses retain the Thumb low bit for tables and indirect calls; data pointers gain no such bit. Arm ELF32, GNU Arm directives and GCC Arm options are checked against the pinned tools. Their unsigned plain C char and ILP32 model are measured, not inherited from the hosted platform/c aliases.

The probe guide distinguishes Ada planner/IR tests, GCC layout measurements and executed C/assembly witnesses. No language semantic decision, instruction selection, Landin startup or source debugger is supplied by these plans.

Explicit memory operations

D227 admits unsigned scalar memory primitives through Targets.Capabilities.Memory_Access, independently of backend availability. Widths are 1/2/4/8 bytes on hosted targets and 1/2/4 on Cortex-M0. Every implemented access checks natural alignment at runtime, including inside unchecked. The M0 source contract refuses exchange/add/compare-exchange. The backend emits the admitted loads/stores and barriers; it introduces no atomic runtime helper. Synthetic-32 refuses these operations.

Each atomic is lowered by its ordering (D499), by its architecture's published mapping of the C/C++11 orderings, and is a full compiler memory boundary whatever its ordering. In the table l and s are RV64's load and store at the access's width.

A compare-exchange is lowered by its success ordering, which is never weaker than its failure ordering (D227), so its acquiring read serves a failed comparison too; a failed exclusive comparison on arm64 clears the reservation with CLREX. The arm64 exclusive loops need no LSE extension or out-of-line atomic helper at the default armv8-a level; at armv8.1-a (D255) each read-modify-write is one LSE instruction at the access's width, and RV64's one- and two-byte read-modify-writes are LR/SC loops on the aligned word that holds them, which keep every byte outside the access. ARMv6-M's DMB has only the SY option. Retry loops promise no wait-free bound. Scalar volatile accesses use exactly one width-matched load/store and no implicit hardware fence.

Compiler barriers have no hardware instruction. Device barriers use MFENCE, DMB SY or FENCE IORW,IORW; completion barriers use MFENCE, DSB SY or FENCE IORW,IORW. CPU atomic contracts assume ordinary coherent RAM (x86 write-back; Arm Normal shareable memory). Device/MMIO behavior requires platform mappings, permitted bus width and the device's completion protocol. A fence cannot turn an arbitrary user pointer into a valid device mapping or drain a device's internal command queue. On x86, MFENCE provides global visibility ordering, not instruction serialization or a peripheral acknowledgment; posted writes can require a device-specific readback. On Arm, DSB waits for architectural completion, which also does not imply peripheral-command completion. No portable cache-maintenance builtin is enabled.

The mappings for x86-64, arm64 and Cortex-M0 are those collected in Sewell's C/C++11 mappings to processors, x86-TSO's and ARMv8's, and ARMv7's for a core without acquire and release instructions; RV64's is Table A.6 of the memory model appendix of the RISC-V unprivileged ISA.

Official architecture and toolchain references checked on 2026-09-16: Armv6-M reference manual DDI0419E, Arm A-profile manual entry and Arm's explanation of SC instruction sequences, Intel architecture manuals, GCC atomic builtins, GCC memory clobbers, and Arm CMSIS cache operations. The pinned M0 tools execute the supported load/store/barrier and nested PRIMASK controls, and independently show GCC's RMW needs an unresolved helper. The cache model demonstrates stale reads and destructive maintenance, under an explicit two-byte cache-line abstraction; the cacheless emulator cannot test physical cache behavior. See the probe guide.

D228 connects Targets.Packed to source declarations and neutral field geometry. One carrier of 1/2/4/8 bytes uses the selected target's size and alignment, with least-significant-bit numbering and little-endian byte order. Unsigned field widths through 64 bits do not add ordinary scalar widths or calling conventions. Natural, C and optimal layouts retain their contracts. Native x86-64 and Darwin arm64 lowering extract and insert that carrier and validate encoded members. M0 remains limited to one-, two- and four-byte volatile transactions; describing an eight-byte ordinary image does not enable an eight-byte MMIO access. The Cortex emitter preserves this distinction.

Packed debug types expose one unsigned raw member and their true storage size. This preserves unnamed encodings without claiming independently addressable fields or ordinary array strides. Full named bitfield/bit-array presentation is a retained debugger limit; the DWARF 4 specification and bit-offset clarification distinguish those representations. Native debugger controls inspect a raw image containing an unnamed pattern. The probe guide distinguishes compiler-generated hosted peripheral execution, independent M0 C controls, and abstract model assertions.

x86-64 assembly implementation

Backend.X86_64 emits a block's text as written, one instruction a line and outside selection, so no rewrite reaches it; body sharing still compares it. Each input is moved into its register at its type's width, zero- or sign-extended to the whole register (movz/movs, movl, movslq), and each output is stored from its register into its slot. In a routine with assembly the allocator hands out only rbx and r12-r15, and none a block of the routine declares: that register is marked saved instead, so the prologue stores it with a .cfi_offset and every epilogue restores it. No value therefore lives in a register a block names or overwrites, which is what lets inputs and outputs move directly.

arm64 assembly implementation

Backend.Arm64 keeps assembly operands in frame homes, and source slots too except at speed in a routine without assembly, where an eligible scalar slot may hold a register over its live interval: x0-x7, or d18-d31 for a float, where no call crosses it, else x19-x24 or d8-d15. Its optimized value plan reuses nonoverlapping scalar homes and at speed may hold eligible values in the same registers, x19-x28 standing for x19-x24; assembly leaves values only x19-x28 and d8-d15, which no block may name. A block's declared registers are excluded from that plan. Each input is loaded through its own register, which addresses its home first, and extended to the whole register (sxtb, sxth, sxtw); the text is emitted as written; and each output is stored through a register no waiting output holds. A block whose outputs hold all of x0-x17 moves its first aside into d16, which every block may overwrite and none may name, and stores it last. A declared x19-x28 gets a frame home: the prologue stores it after reserving the frame, with a .cfi_offset from the CFA at x29+16, and every epilogue restores it before the frame record.

Cortex-M0 assembly implementation

Backend.Cortex_M consumes verified IR and Backend.Arm32_ABI entry/call plans. It does not change ordinary, C or optimal layout. Source slots remain pinned; verified block-local scalar temporaries reuse eight-byte stack homes only after their last operand read. Heap-owned work arrays keep allocation scratch off the Ada host stack. r0-r7 are selector scratch, with r4-r7 saved in framed routines and only used low registers saved in leaves, r8/r10 untouched, r9 reserved, and r11 the frame pointer in framed routines. Their prologue saves r4-r7, constructs the eight-byte previous-r11/lr record, publishes r11, then reserves aligned homes and incoming-register staging. Eligible leaves use SP-relative homes and preserve LR and r11 in registers. Epilogues restore only their own saved registers. Incoming stack arguments begin above the actual save area. Outgoing arguments use the planner's aligned stack area plus private r0-r3 staging.

The instruction envelope follows the official ARMv6-M Architecture Reference Manual, with executable legal/illegal encoding controls under the pinned assembler. Per-routine ELF input sections let the external test linker place and garbage-collect routines. The compiler-owned Cortex firmware path also accepts link(section: ...) for explicit placement and link(keep) to retain the containing input section under the fixed flash/RAM map described below. The flash-to-SRAM control forces a real call veneer while preserving the selected core and physical RAM map.

The emitter performs no body sharing. Shared optimization and specialization still transform verified IR before selection, preserving atom domains, stored array/struct shapes, memory effects and private call-status validation. Hosted body-sharing repairs remain unchanged. Code size is a retained physical-image constraint, not a competitive-optimization claim.

An ordinary assembler.block loads each input straight into its register, addressing its home through that same register, extends a signed byte or halfword to the whole register, and emits the text one instruction a line. Each output is then stored through a low register no output still waiting holds; a block whose outputs hold all of r0-r7 moves its first aside into r12, which no block may name and every block may overwrite, and stores it last. A branch then skips the literal pool the text may have used. D230's shorthand is one inout operand at r0. The existing low-register/flag clobbers and full opaque effects remain; no high-register, frame or naked-body restriction is relaxed. platform/cortex_m uses MRS PRIMASK/CPSID I, MSR PRIMASK/ISB SY and DSB SY/WFI through general operands. CPU functions retain ordinary framed Landin calls in both thread and handler mode. Its explicit barriers preserve D227, including the difference between a compiler boundary and device completion. The freestanding consumers retain map/module/helper closure evidence under the same fixed image profile.

Runtime helper boundary

The external test link selects the pinned GCC 14.2.1 thumb/v6-m/nofp/libgcc.a (SHA-256 137aa204587d2cefcc3eea90685a29d1e2f058a0a9cbdc29329e6f27c6249903). Helpers use the Arm base runtime ABI, not Landin's r12 failure outcome. The Arm runtime ABI and GCC runtime description are checked against actual linked code and execution.

The linked archive is an external pinned compiler runtime dependency. Source provenance includes GCC's Arm integer routines and soft-float routines; their headers carry GPLv3 with GCC Runtime Library Exception 3.1. Every image retains requested helper names, archive path/hash, ELF/map/disassembly and an empty undefined-symbol inventory. This links no libc, allocator, scheduler or atomic emulation. Division guards prevent entering the archive's divide-zero fallback; dependency members remain visible in the map. The firmware linker explicitly selects the pinned thumb/v6-m/nofp archive with -lgcc. Runtime and CPU-library packaging belong to the freestanding core slice.

At armv7-m (D255) the emitter names .arch armv7-m instead of .cpu cortex-m0, a 32-bit quotient is SDIV or UDIV and its remainder MLS after it, after the same zero-divisor and minimum-over-minus-one guards, and the link selects the pinned thumb/v7-m/nofp/libgcc.a with -march=armv7-m. Every other selection above, the r0-r7 selector and the 64-bit helpers, is unchanged. Inline assembly keeps the ordinary block's straight-line and register restrictions, but the ARMv6-M instruction allowlist applies only at armv6-m; at higher levels the assembler checks instructions against the selected .arch.

The execution guide separates generated code, independent controls, target refusals and physical limits. Compiler-owned startup is D229; the bounded Landin source-debugging contract is above.

Cortex-M0 firmware images

--target=cortex-m0 --firmware-entry=NAME --emit=exe selects the entry-module source definition; its exported symbol may differ. Backend.Firmware generates the reset source and linker script for the existing 32 KiB flash/16 KiB RAM profile. The top 4 KiB of RAM is reserved for stacks, with eight-byte-aligned initial MSP 0x20004000. Static images cannot overlap 0x20003000. The driver refuses a known compiler-framed routine larger than the 4 KiB reservation, counting its saved registers and reserved homes. This per-routine check does not bound stack use through calls or interrupt nesting. The 48-word vector image starts at zero. There is no VTOR relocation, FPU, exclusive-access implementation or change of board. D229 owns the exact implemented/reserved slots, typed handlers and ordinary/naked obligations.

The driver retains OUTPUT.s, OUTPUT.o, OUTPUT.ld, OUTPUT.map and the ELF. With --build-report=PATH, a successful firmware executable also reports post-link occupied flash and static RAM extents, their limits and remaining capacity, the reserved stack size, and the selected libgcc archive members. The sizes come from ELF load segments; the helper names come from the linker map. Assembly-only reports have no linked capacity measurement. The assembler uses Cortex-M0/Thumb/soft-float/AAPCS flags and fatal warnings. The linker uses those flags plus -nostdlib -nostartfiles -nodefaultlibs, the explicit generated script, --gc-sections --build-id=none --emit-relocs and -lgcc. Host writes and invocations pass through Landin.Platform. There is no implicit hosted startup, libc, allocator or scheduler. Source library requests refuse. Assembler/linker failures retain the invoked tool's diagnostic and driver failure status. ELF attributes and helper selection do not enable the general C source surface.

.text.* and .rodata.* reside in flash; .data.*, .bss.* and .ramtext.* execute in RAM, with flash load images for initialized data and RAM code. Each conformance evidence table has its own .rodata.landin_evidence_* input section, so section garbage collection can discard an unused table and its provider references independently of live tables. Startup copies both load images and clears BSS before source entry. GNU ARM veneers handle out-of-range calls between flash and RAM. Link assertions bound physical images; L0505 independently bounds pre-GC static materialization to 8 MiB. Explicit symbol/section collisions and alignment/convention violations refuse rather than silently changing requested placement. Section retention is independent of calling convention, and a kept vector image retains its referenced handlers. Linker symbols are private fixed assembly inputs, not user-code module initialization or general static address arithmetic.

D232 enables the same canonical core/panic handler contract on Linux, Darwin and Cortex. Default checks retain UD2/BRK/UDF termination. A selected handler uses the ordinary two-scalar ABI and a four-byte private entry latch, with process-wide exchange/exclusive synchronization on hosted targets and ordinary single-core word accesses on ARMv6-M. No source atomics, FPU, cache, VTOR or interrupt-masking helper are added on Cortex. Compiler startup clears the latch; synthetic entry/root violations use site zero. Naked fallthrough and hardware faults retain separate machine obligations. --panic-map is optional off-target mapping, not Cortex source-debugger acceptance.

The device fixture interface preserves vendor 32-bit transaction sizes independently of field masks. Its real RP2040 address constants are data, not a target/board selection. Execution explicitly remaps a bounded peripheral subset while retaining the accepted M0 map and ABI; RP2040's dual M0+ hardware is not claimed as an executable target.

The driver evidence uses the same 32 KiB flash, 16 KiB RAM and 4 KiB stack reservation. Compiler-owned firmware links NOLOAD BSS with an explicit RAM LMA; initialized data and RAM code retain flash load images. This prevents a zero-fill ELF segment inheriting a spurious flash address. QEMU checks poisoned reset and vector/frame state; a separately named synthetic model executes the complete program's GPIO/timer/UART/DMA path. Its finite count and drain acknowledgment are synthetic premises, not RP2040 or microbit peripheral behavior. No target layout, MMIO width or ABI changes.

RV64 Linux

linux-rv64 selects the native RISC-V ELF backend and the LP64D C convention. The RV64 instruction selector is separate from the emitter so its baseline and extension decisions can be reused with another integer width. ISA strings select sets of extensions; zba and xtheadba are independent facts, with no ordering that makes one imply the other. The baseline is rv64gc. The default external driver is riscv64-linux-gnu-gcc; a caller can select another driver with --toolchain=. GNU tools receive the selected -march and -mabi=lp64d when linking Landin's own assembly.

The RV64 lanes cross-emit on a supported Linux compiler host and execute source-matching, checksum-verified payloads on physical RISE runners. Runtime, GDB, C ABI and ISA-level execution each have their own verdict. The selected vendor extension is confirmed by an isolated instruction probe before extended programs run. The baseline and extended operation are both inspected in the linked routine and executed; a separate assembly block establishes baseline refusal. This supplies no claim of native RV64 Ada compiler-host support.

The RV64 C planner flattens eligible floating and mixed records at actual field offsets, assigns independent a0–a7 and fa0–fa7 banks, and falls back to the integer convention when either required bank cannot hold a whole value. Two integer chunks may split between a7 and the stack; records above sixteen bytes use a pointer to a caller-owned copy. The hidden indirect result consumes a0. Every unnamed variadic argument uses integer transport, including floating bit patterns. This placement remains outside the verified target-neutral IR.

The target fact compiler.c_riscv_lp64d selects platform/c's LP64 aliases, including unsigned plain c_char. Linux libc record selection stays separate; the generic 128-byte stat is checked against independently compiled headers.

Integer assembly operands name x5–x7 or x9–x31. x0, return address x1, stack pointer x2, global pointer x3, thread pointer x4 and frame pointer x8 remain reserved. general allocates caller-clobbered registers; declared saved registers acquire routine saves. Ordinary blocks cannot transfer control or change assembly directives. ELF DWARF and CFI use x8 as the entry CFA, with saved return address at CFA−8 and caller frame at CFA−16. The GNU target driver receives both -march=ISA and -mabi=lp64d, keeping user assembly within the selected extension set. Modern vector support and Zbb are not assumed; the native execution lane confirms XTheadBa before executing it.