mirror of
https://github.com/ratspeak/C6-Reticulum-ASM
synced 2026-08-12 18:07:18 -04:00
36e23ab975
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.
19 lines
511 B
Python
19 lines
511 B
Python
#!/usr/bin/env python3
|
|
"""Repo-root entrypoint that forwards to tests/harness/verify.py.
|
|
|
|
The shell wrapper `./verify` execs this so users get a uniform command from
|
|
the repo root regardless of platform conventions for shell scripts.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import sys
|
|
from pathlib import Path
|
|
|
|
REPO_ROOT = Path(__file__).resolve().parent
|
|
sys.path.insert(0, str(REPO_ROOT / "tests"))
|
|
|
|
from harness import verify # noqa: E402
|
|
|
|
if __name__ == "__main__":
|
|
sys.exit(verify.main(sys.argv[1:]))
|