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.
239 lines
7.4 KiB
Python
239 lines
7.4 KiB
Python
"""Tests for tools/parse_spec.py."""
|
|
|
|
from __future__ import annotations
|
|
|
|
import textwrap
|
|
from pathlib import Path
|
|
|
|
import pytest
|
|
|
|
import parse_spec
|
|
|
|
REPO_ROOT = Path(__file__).resolve().parent.parent.parent
|
|
|
|
|
|
def _write(tmp: Path, name: str, body: str) -> Path:
|
|
p = tmp / name
|
|
p.parent.mkdir(parents=True, exist_ok=True)
|
|
p.write_text(textwrap.dedent(body), encoding="utf-8")
|
|
return p
|
|
|
|
|
|
# --- structural parse ----------------------------------------------------
|
|
|
|
|
|
def test_parse_minimum_block(tmp_path: Path) -> None:
|
|
src = _write(
|
|
tmp_path,
|
|
"foo.S",
|
|
"""\
|
|
;; ============================================================================
|
|
;; @function: foo
|
|
;; @module: bar
|
|
;; @inputs: a0 = thing
|
|
;; @outputs: a0 = result
|
|
;; @clobbers: t0
|
|
;; @preserves:
|
|
;; @stack: 0
|
|
;; @cycles: 10
|
|
;; @ct: not-required
|
|
;; @spec: none
|
|
;; @verify: kat-only; trivial helper, no functional contract
|
|
;; @tests: tests/bar/test_foo.py
|
|
;; @adrs: 0001
|
|
;; @status: draft
|
|
;; ============================================================================
|
|
.global foo
|
|
foo: ret
|
|
""",
|
|
)
|
|
spec = parse_spec.parse_spec(src)
|
|
assert spec.fields["function"] == "foo"
|
|
assert spec.fields["module"] == "bar"
|
|
assert spec.fields["status"] == "draft"
|
|
assert spec.line_range[0] == 1
|
|
|
|
|
|
def test_missing_opening_fence_raises(tmp_path: Path) -> None:
|
|
src = _write(
|
|
tmp_path,
|
|
"foo.S",
|
|
"""\
|
|
;; @function: foo
|
|
""",
|
|
)
|
|
with pytest.raises(parse_spec.SpecError):
|
|
parse_spec.parse_spec(src)
|
|
|
|
|
|
def test_missing_closing_fence_raises(tmp_path: Path) -> None:
|
|
src = _write(
|
|
tmp_path,
|
|
"foo.S",
|
|
"""\
|
|
;; ============================================================================
|
|
;; @function: foo
|
|
""",
|
|
)
|
|
with pytest.raises(parse_spec.SpecError):
|
|
parse_spec.parse_spec(src)
|
|
|
|
|
|
def test_duplicate_field_raises(tmp_path: Path) -> None:
|
|
src = _write(
|
|
tmp_path,
|
|
"foo.S",
|
|
"""\
|
|
;; ============================================================================
|
|
;; @function: foo
|
|
;; @function: bar
|
|
;; ============================================================================
|
|
""",
|
|
)
|
|
with pytest.raises(parse_spec.SpecError, match="duplicate field"):
|
|
parse_spec.parse_spec(src)
|
|
|
|
|
|
def test_inline_comment_stripped(tmp_path: Path) -> None:
|
|
src = _write(
|
|
tmp_path,
|
|
"foo.S",
|
|
"""\
|
|
;; ============================================================================
|
|
;; @stack: 16 # one frame for ra
|
|
;; ============================================================================
|
|
""",
|
|
)
|
|
spec = parse_spec.parse_spec(src)
|
|
assert spec.fields["stack"] == "16"
|
|
|
|
|
|
# --- validation ----------------------------------------------------------
|
|
|
|
|
|
def _fake_repo(tmp_path: Path) -> Path:
|
|
"""Build a minimal repo with one Accepted ADR and the dirs validate_spec
|
|
inspects.
|
|
"""
|
|
(tmp_path / "src").mkdir()
|
|
(tmp_path / "tests" / "bar").mkdir(parents=True)
|
|
(tmp_path / "tests" / "bar" / "test_foo.py").touch()
|
|
adr_dir = tmp_path / "docs" / "adr"
|
|
adr_dir.mkdir(parents=True)
|
|
(adr_dir / "0001-fake.md").write_text(
|
|
"# ADR-0001: Fake\n\n- **Status:** Accepted\n",
|
|
encoding="utf-8",
|
|
)
|
|
return tmp_path
|
|
|
|
|
|
def _good_spec_body(extra: str = "") -> str:
|
|
return (
|
|
";; ============================================================================\n"
|
|
";; @function: foo\n"
|
|
";; @module: bar\n"
|
|
";; @inputs: a0 = thing\n"
|
|
";; @outputs: a0 = result\n"
|
|
";; @clobbers: t0\n"
|
|
";; @preserves:\n"
|
|
";; @stack: 0\n"
|
|
";; @cycles: 10\n"
|
|
";; @ct: not-required\n"
|
|
";; @spec: none\n"
|
|
";; @verify: kat-only; trivial\n"
|
|
";; @tests: tests/bar/test_foo.py\n"
|
|
";; @adrs: 0001\n"
|
|
";; @status: draft\n"
|
|
";; ============================================================================\n"
|
|
+ extra
|
|
)
|
|
|
|
|
|
def test_valid_spec_no_errors(tmp_path: Path) -> None:
|
|
repo = _fake_repo(tmp_path)
|
|
src = repo / "src" / "bar"
|
|
src.mkdir()
|
|
f = src / "foo.S"
|
|
f.write_text(_good_spec_body(), encoding="utf-8")
|
|
spec = parse_spec.parse_spec(f)
|
|
errors = parse_spec.validate_spec(spec, repo_root=repo)
|
|
assert errors == [], errors
|
|
|
|
|
|
def test_function_must_match_basename(tmp_path: Path) -> None:
|
|
repo = _fake_repo(tmp_path)
|
|
src = repo / "src" / "bar"
|
|
src.mkdir()
|
|
body = _good_spec_body().replace("@function: foo", "@function: nope")
|
|
f = src / "foo.S"
|
|
f.write_text(body, encoding="utf-8")
|
|
spec = parse_spec.parse_spec(f)
|
|
errs = parse_spec.validate_spec(spec, repo_root=repo)
|
|
assert any("does not match file basename" in e for e in errs), errs
|
|
|
|
|
|
def test_unaccepted_adr_rejected(tmp_path: Path) -> None:
|
|
repo = _fake_repo(tmp_path)
|
|
src = repo / "src" / "bar"
|
|
src.mkdir()
|
|
body = _good_spec_body().replace("@adrs: 0001", "@adrs: 0099")
|
|
f = src / "foo.S"
|
|
f.write_text(body, encoding="utf-8")
|
|
spec = parse_spec.parse_spec(f)
|
|
errs = parse_spec.validate_spec(spec, repo_root=repo)
|
|
assert any("ADR-0099" in e for e in errs), errs
|
|
|
|
|
|
def test_kat_only_requires_rationale(tmp_path: Path) -> None:
|
|
repo = _fake_repo(tmp_path)
|
|
src = repo / "src" / "bar"
|
|
src.mkdir()
|
|
body = _good_spec_body().replace(
|
|
"@verify: kat-only; trivial",
|
|
"@verify: kat-only",
|
|
)
|
|
f = src / "foo.S"
|
|
f.write_text(body, encoding="utf-8")
|
|
spec = parse_spec.parse_spec(f)
|
|
errs = parse_spec.validate_spec(spec, repo_root=repo)
|
|
assert any("rationale" in e for e in errs), errs
|
|
|
|
|
|
def test_unbounded_cycles_requires_no_ct(tmp_path: Path) -> None:
|
|
repo = _fake_repo(tmp_path)
|
|
src = repo / "src" / "bar"
|
|
src.mkdir()
|
|
body = _good_spec_body()
|
|
body = body.replace("@cycles: 10", "@cycles: unbounded")
|
|
body = body.replace("@ct: not-required", "@ct: required")
|
|
f = src / "foo.S"
|
|
f.write_text(body, encoding="utf-8")
|
|
spec = parse_spec.parse_spec(f)
|
|
errs = parse_spec.validate_spec(spec, repo_root=repo)
|
|
assert any("unbounded" in e and "ct" in e for e in errs), errs
|
|
|
|
|
|
def test_module_must_match_directory(tmp_path: Path) -> None:
|
|
repo = _fake_repo(tmp_path)
|
|
src = repo / "src" / "bar"
|
|
src.mkdir()
|
|
body = _good_spec_body().replace("@module: bar", "@module: baz")
|
|
f = src / "foo.S"
|
|
f.write_text(body, encoding="utf-8")
|
|
spec = parse_spec.parse_spec(f)
|
|
errs = parse_spec.validate_spec(spec, repo_root=repo)
|
|
assert any("does not match directory" in e for e in errs), errs
|
|
|
|
|
|
def test_missing_field_reported(tmp_path: Path) -> None:
|
|
repo = _fake_repo(tmp_path)
|
|
src = repo / "src" / "bar"
|
|
src.mkdir()
|
|
body = _good_spec_body().replace(
|
|
";; @stack: 0\n", ""
|
|
)
|
|
f = src / "foo.S"
|
|
f.write_text(body, encoding="utf-8")
|
|
spec = parse_spec.parse_spec(f)
|
|
errs = parse_spec.validate_spec(spec, repo_root=repo)
|
|
assert any("missing field @stack" in e for e in errs), errs
|