Installs the full Godmode verifier stack — Cryptol 3.5.0, SAW 1.5,
Binsec 0.11.1, angr 9.2.213 + pypcode 3.3.3, TLA+ Tools 2.19,
Sail 0.20.1 + sail-riscv 4d5530b, fiat-crypto 412e8af, GHC 9.6.7,
cabal 3.10.3.0, Coq 9.1.1 — symlinked into toolchain/local/bin via
the new install.sh, with Python deps in toolchain/venv. ADR-0009
codifies the per-tier responsibility (A=algorithmic Cryptol/SAW,
B=ct Binsec/Rel, C=binary-equivalence angr+pcode, D=state-machine
TLA+, E=ISA reference Sail) and the comma-separated @verify path
syntax the dispatcher now consumes. The Tier C-future path (true
SAW-on-RV32 via macaw-riscv + a forked saw-script) is documented;
GHC + cabal are pre-installed against that day.
sha256_init flips from tested to verified — first crypto function
to clear the new bar. Cryptol model proves the FIPS 180-4 §5.3.3
IVs, LE serialisation, and word_to_le_bytes bijection over [32];
SAW driver discharges them via z3; angr proves the RV32IMC binary
writes the 8 IV words LE, zeros length_bits + block_len, leaves the
partial-block buffer + pad untouched, and preserves all 14 callee-
saved registers, returning within a bounded basic-block budget.
End-to-end ./verify sha256_init runs in ~3 s.
Cleanup found while sweeping: state/ files have no verifiable
function so are skipped by parse_spec; @ct accepts an optional
parenthesized rationale (matches existing AES annotations); five
AES @tests fields pointed at non-existent per-function test files
and now point at the combined ones that actually exercise them.
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.
