Walks every src/**/*.S, parses each function's @stack annotation and
its call/tail/jal outgoing edges, builds a call graph rooted at
_reset, and reports the deepest cumulative stack along any reachable
path. Fails the build if the deepest path exceeds STACK_SIZE from
src/include/config.S.
Cycles are flagged as recursion (recursion is forbidden today; allowing
it needs a separate ADR). Functions reachable from _reset whose .S is
absent are reported as warnings.
Wired into 'make ci': registry → stack → test. Current binary:
deepest path _reset → _main → log_event → log_hex = 48 bytes,
well under STACK_SIZE = 16384.
OQ-4 resolved in docs/open-questions.md.
154 tests, all green.
kiss_decode_reset — single-shot state clear (in_frame, escaped,
saw_type bytes plus buf_len word).
kiss_decode_byte — byte-at-a-time KISS state machine. Returns 0
(no frame yet), 1 (frame complete; caller reads kiss_buf and
kiss_buf_len), or -1 (framing error; state self-resets). Mirrors
the Python oracle in tests/harness/oracle.py.
kiss_encode_frame — pure data: src buffer → escaped output with
FEND brackets. Returns bytes-written or -1 on dst overflow. No
allocation; both buffers are caller-provided.
src/state/kiss.S holds the .bss for the decoder (in_frame /
escaped / saw_type / buf_len / KISS_MAX_FRAME-byte buf). Per
ADR-0002 it lives under src/state/ and exposes globals as data
symbols (no .type @function so check_registry skips them).
tools/check_registry.py: function detection now requires both
.global AND .type @function so data globals in src/state/ no
longer trigger 'unregistered global' errors.
_main: post-boot loop now reads UART → kiss_decode_byte → log
either kiss.rx_frame or kiss.rx_error per result. The integration
test sends KISS-encoded payloads (and a deliberately malformed
escape) via qemu's stdin and asserts the right log events come
back. End-to-end RX path proven for the first time.
130 tests, all green.
Lays the verifier-loop infrastructure that every subsequent function
goes through. Every change is wired to make ci.
Tooling (tools/):
- parse_spec.py validates the ADR-0007 spec block on every .S file
(required fields, @function ↔ basename, @module ↔ directory, @adrs ↔
Accepted ADRs, @verify/@tests path existence, unbounded-cycles ↔
not-required-ct).
- check_registry.py cross-checks FUNCTIONS.md against src/ — every
registered global has a source file (and vice versa), every
depends-on resolves, status disagreements raise warnings.
Test harness (tests/harness/):
- log_parser.py parses the ADR-0004 log line format with selectors.
- target.py: Target ABC + NullTarget loopback + Emu/Hw skeletons
that detect tool availability and raise TargetUnavailable until
wired (deferred until there's a binary to drive end-to-end).
- oracle.py: pure-Python KISS encode/decode reference + RNS.Packet
shim for differential testing.
- verify.py + verify_cli.py + ./verify wrapper: the dispatcher.
Runs spec-validate, pytest, and the @verify-pointed tool
(kat-only, .saw, .tla, .py); reports pass/fail/skip/not-implemented.
Build chain (toolchain/):
- qemu-virt.ld: DRAM @ 0x80000000, __global_pointer$ anchored,
16 KiB stack reserved at top. C6 linker script lands with hardware
bring-up.
- versions.lock pinned to riscv64-elf-binutils 2.46 + qemu 11.0 +
Python 3.12 + RNS 1.2 (per ADR-0008).
Includes (src/include/):
- psabi.S with the RISC-V ABI register aliases (ADR-0001).
- config.S with capacity constants (stack, ring buffers, KISS frame).
- regs.S with the qemu-virt NS16550A UART addresses; C6 stub with
.error until populated.
ADR-0008: bundles four decisions surfaced during bring-up:
1. Rename verify/ → proofs/ to free ./verify for the dispatcher.
2. Adopt vanilla riscv64-elf-binutils (homebrew) over the Espressif
crosstool-NG fork; -march=rv32imac -mabi=ilp32.
3. Log timestamps are 8 hex digits emitted by log_hex(width=8).
4. Spec-block prefix is # (RISC-V GAS line comment), not ;;.
ADR-0006/0007 status lines flagged as partially superseded; ADR-0004
flagged as refined. ADR index updated. parse_spec accepts both ;; and
# prefixes during the transition. open-questions.md tracks OQ-1..OQ-3
as resolved by ADR-0008 and OQ-4 (check_stack.py) deferred.
make ci: 51 tests, all green.
