Repository navigation
verified: validate the .t27 crypto against Wycheproof and a differential fuzz (sha256, sha512, ed25519) #8041
Description
The receipt crypto now runs from specs/tri/crypto/{sha256,sha512,ed25519}.t27 (#7594). Its evidence today is FIPS 180 / RFC 8032 vectors in the specs' own test blocks plus a byte-for-byte check against ed25519-dalek. That is not enough to call the specs validated.
Scope
- Wycheproof: run the Ed25519 (eddsa_test.json) vectors through the generated code; every
valid/invalidverdict must match. Record anyacceptablecase and the spec's choice. - NIST CAVP SHA-256/SHA-512 short and long message files (SHA2VS) through the generated code.
- Differential fuzz: N random keys/messages (and mutated signatures) through spec vs ed25519-dalek (dev-only oracle) vs OpenSSL; any disagreement is a finding.
- Honest note: the specs make no constant-time claim; state it in the spec header and in the receipt threat model.
Constraints
Only-t27: vector drivers and checks live in .t27 test blocks or t27c-run harness; hand-written Rust only within the existing exception budget. Vector files are data. Runs on the Railway lab.
Done when
A report on this issue: vector counts per file, pass/fail, every disagreement with a minimal reproducer, and fixes landed as their own PRs.
User Scenarios
- Given the Ed25519 spec at
specs/tri/crypto/ed25519.t27, when the Wycheproofeddsa_test.jsonvectors are executed through the generated code, then everyvalid/invalidverdict matches the spec's output and anyacceptablecase is recorded with the spec's choice. - Given the SHA-256 and SHA-512 specs, when the NIST CAVP SHA2VS short and long message files are executed through the generated code, then all vectors pass.
- Given the differential fuzz harness, when N random keys, messages, and mutated signatures are tested against the spec vs ed25519-dalek vs OpenSSL, then any disagreement produces a minimal reproducer.
Requirements
FR-001: The Ed25519 spec MUST validate against all Wycheproof eddsa_test.json vectors with matching valid/invalid verdicts.
FR-002: The SHA-256 and SHA-512 specs MUST pass all NIST CAVP SHA2VS short and long message test vectors.
FR-003: The differential fuzz harness MUST execute N iterations comparing spec-generated code against ed25519-dalek and OpenSSL, reporting any disagreement with a minimal reproducer.
FR-004: The spec headers for sha256.t27, sha512.t27, and ed25519.t27 MUST include an explicit note that no constant-time claim is made.
FR-005: The receipt threat model MUST document the absence of constant-time guarantees.
Success Criteria
t27c test specs/tri/crypto/ed25519.t27 --wycheproof vectors/eddsa_test.jsonexits 0 with all verdicts matchingt27c test specs/tri/crypto/sha256.t27 --cavp vectors/SHA256ShortMsg.rspexits 0 with 100% pass ratet27c test specs/tri/crypto/sha512.t27 --cavp vectors/SHA512LongMsg.rspexits 0 with 100% pass ratecargo test -p t27b differential_fuzz -- --iterations 10000exits 0 with 0 disagreements reported- Report generated at
reports/crypto-validation-8041.mdcontaining vector counts per file, pass/fail summary, and all disagreements with minimal reproducers
Boundary
- specs/tri/crypto/sha256.t27
- specs/tri/crypto/sha512.t27
- specs/tri/crypto/ed25519.t27
- specs/tri/crypto/crypto.t27
- specs/tri/t27b/fuzz.t27
- cli/t27b/tests/differential.rs
Activity
gHashTag commentedon Oct 9, 2026
Validation report (generated Rust at master, bootstrap/gen/rust/tri/crypto/{sha256,ed25519}.rs; ed25519.rs carries sha512.t27)
Harness: a throwaway cargo crate in /tmp that pulls the generated .rs in through #[path]. It was not committed. OpenSSL 3.6.4 was used through Python cryptography 46.0.3.
Disagreements: none. Acceptable cases: the v1 ed25519 file contains none, so the spec never had to make that choice. The strict choices it does make (S < L, canonical A, rejecting small-order A and R) already go beyond OpenSSL, as the spec's existing tests record. No bug was found, so no fix PR is needed. The spec already holds RFC 8032 and small-order vectors, so I did not add more Wycheproof test blocks.
Constant time: #8065 replaces the header's one-line remark with an explicit no-constant-time-claim paragraph (comment only; generated Rust is byte-identical; reseal shows 16/16). Still open from scope item 4: the same note in the receipt threat model.
Not run: SHA2VS Monte Carlo files, and the legacy testvectors/eddsa_test.json. Limit: the fuzz is random, so it almost never produces small-order or non-canonical encodings. Those edge cases are covered by Wycheproof and by the spec's own tests, not by the fuzz.
Merge master cfe753c into claude/ed25519-ct-note-8041 (Refs #8041)
verified: ed25519.t27 states it makes no constant-time claim (Refs #8041
t27b: the node scans of lower.rs move to specs/tri/t27b/ast_scan.t27 (C…