C6-Reticulum-ASM

mirror of https://github.com/ratspeak/C6-Reticulum-ASM synced 2026-08-12 18:07:18 -04:00

History

DeFiDude f3d0d690d0 verifier toolchain (ADR-0009): sha256_init verified end-to-end (Cryptol + SAW + angr) 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.	2026-05-02 06:00:40 -06:00
..
install.sh	verifier toolchain (ADR-0009): sha256_init verified end-to-end (Cryptol + SAW + angr)	2026-05-02 06:00:40 -06:00

DeFiDude f3d0d690d0 verifier toolchain (ADR-0009): sha256_init verified end-to-end (Cryptol + SAW + angr)

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.

2026-05-02 06:00:40 -06:00

install.sh

verifier toolchain (ADR-0009): sha256_init verified end-to-end (Cryptol + SAW + angr)

2026-05-02 06:00:40 -06:00