End-to-end bring-up: _reset → _init_bss → _init_data → clock_init →
uart_init → uart_tx_bytes → bytes on UART. _main calls each in
order, then forwards a hard-coded "00000000\tboot\tready\r\n"
banner (same shape as the eventual log_event output) and halts in
wfi.
EmuTarget wired to qemu-system-riscv32:
qemu -machine virt -cpu rv32 -bios none -kernel <elf>
-display none -serial stdio -monitor none -no-reboot
A daemon thread drains qemu's stdout into an internal buffer; read()
serves from it with a timeout. is_available() now requires both
qemu on PATH and a built .elf in config.binary.
Integration test (test__main.py): boot the firmware, read UART for
2 s, assert the parsed log line has module=boot, event=ready,
ts_raw=00000000. First test in the project that actually runs the
binary; the boot chain breaks loudly if any link regresses.
FUNCTIONS.md: _main → ◉ verified; depends-on updated to match the
real call sites (log_init removed, uart_tx_bytes added — log_init
returns when the log primitives ship).
Word-by-word copy from .data's LMA (__data_load_start) to its VMA
(__data_start..__data_end). On qemu-virt LMA == VMA so the loop is
identity; on the C6 it pulls flash → SRAM. Same asm shape, target-
selected behaviour driven entirely by the linker script.
toolchain/qemu-virt.ld: defines __data_load_start = LOADADDR(.data)
so the symbol resolves at link time on either target.
Static disassembly checks: three auipc/addi pairs for the bounds,
matched lw/sw word pair, two increments per iteration, ret, no
callee-saved writes.
Loop zeroes [.bss_start, .bss_end). Two auipc/addi pairs load the
bounds, then sw zero / addi t0,4 / j until t0 == t1, then ret.
5 static-disassembly checks confirm the prologue, store-word, branch,
return, and ABI compliance (no callee-saved writes).
@verify: kat-only — refinement against memset(.bss, 0, N) is
implicit in the static checks. Integration coverage (an actual
.bss-resident variable observed zero post-boot) lands with _main.
First asm function through the canonical loop end-to-end:
make build → firmware.elf → ./verify _reset → green
(spec-validate, 4 tests, kat-only verifier).
_reset: real implementation. Sets sp ← __stack_top, gp ←
__global_pointer$, calls _main, defensive wfi/j loop. Tests assert
ELF entry point matches _reset, prologue order (sp before gp before
call), and the halt-loop tail.
_init_bss / _init_data / _main: stubs (unimp body) per CLAUDE.md
workflow step 3. Test files exist with @pytest.mark.skip so the
spec-block @tests references resolve.
tests/harness/build.py: thin shell over `make build`, plus objdump
helpers (entry_point, symbol_address, per-symbol disassemble) used
by the boot tests.
FUNCTIONS.md: _reset → ◉ verified; the three stubs → ◐ in-progress.
