mirror of
https://github.com/ratspeak/C6-Reticulum-ASM
synced 2026-08-12 18:07:18 -04:00
f3d0d690d0
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.
62 lines
2.8 KiB
Text
62 lines
2.8 KiB
Text
# Pinned tool versions. Updated only when ./verify --all is green with the new versions.
|
|
# Format: <tool> = <version> [# notes]
|
|
#
|
|
# Toolchain choice locked in by ADR-0008 (build) and ADR-0009 (verifier stack).
|
|
# Build: vanilla riscv64-elf-binutils + qemu-system-riscv32, no Espressif fork.
|
|
# Verify: full Galois stack (Cryptol+SAW) + Binsec/Rel + angr+pcode + Sail-RISCV.
|
|
# All verifier binaries live under ~/opt and are symlinked into toolchain/local/bin.
|
|
|
|
# --- assembler / linker / objcopy / objdump ---
|
|
riscv64-elf-binutils = 2.46.0 # macOS: brew install riscv64-elf-binutils
|
|
|
|
# --- emulation ---
|
|
qemu-system-riscv32 = 11.0.0 # macOS: brew install qemu
|
|
|
|
# --- flashing ---
|
|
esptool = TBD # `esptool version` once first flash is attempted
|
|
|
|
# --- harness ---
|
|
python = 3.12.4 # min 3.11
|
|
pyserial = 3.5
|
|
pytest = 9.0.2
|
|
rns = 1.2.0 # upstream Python Reticulum (oracle)
|
|
|
|
# --- formal verification (per ADR-0009) ---
|
|
# Galois stack: algorithmic spec + Cryptol-Cryptol equivalence proofs.
|
|
saw = 1.5 # GaloisInc/saw-script v1.5 (957290e), arm64-darwin with-solvers
|
|
cryptol = 3.5.0 # GaloisInc/cryptol v3.5.0, arm64-darwin with-solvers
|
|
# SMT solvers bundled inside SAW + Cryptol with-solvers tarballs:
|
|
z3 = 4.8.14
|
|
cvc4 = bundled
|
|
cvc5 = bundled
|
|
yices = bundled
|
|
boolector = bundled
|
|
bitwuzla = bundled
|
|
abc = bundled # SAW's AIG backend
|
|
|
|
# RV32 binary symbolic execution (binary-equivalence tier until macaw-riscv lands in SAW).
|
|
angr = 9.2.213
|
|
pypcode = 3.3.3 # provides RISCV:LE:32:RV32IMC lifter via Ghidra
|
|
|
|
# Constant-time verification (relational symbolic execution).
|
|
binsec = 0.11.1 # opam install binsec; switch=binsec, OCaml 5.1.1
|
|
ocaml = 5.1.1
|
|
|
|
# RISC-V ISA formal model (reference).
|
|
sail = 0.20.1 # opam install sail; vendored ISA model under references/sail-riscv
|
|
sail-riscv = 4d5530b # github.com/riscv/sail-riscv pinned commit
|
|
|
|
# Verified field arithmetic (X25519 oracle for milestone 2 elliptic curves).
|
|
fiat-crypto = 412e8af # github.com/mit-plv/fiat-crypto pinned commit
|
|
coq = 9.1.1 # opam install coq (renamed Rocq Prover; coqc still works)
|
|
|
|
# State machines (added in milestone 5).
|
|
tla2tools = 2.19 # tlaplus/tlaplus v1.7.4 jar
|
|
|
|
# Haskell toolchain (path to building macaw-riscv into SAW upstream; see ADR-0009).
|
|
ghc = 9.6.7 # via ghcup
|
|
cabal = 3.10.3.0 # via ghcup
|
|
opam = 2.5.1 # macOS: brew install opam
|
|
|
|
# --- runtime / shell ---
|
|
java = 17.0.18 # for TLC; brew install openjdk@17 if missing
|