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.
