saymrwulf/fips205-slhdsa-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/fips205-slhdsa-verified.git synced 2026-09-03 19:53:49 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

README: apex status — verify-path pyramid complete, 11 certificates

Browse source 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-24 10:15:54 +02:00
parent 2e48d9c6d0
commit bd58cea87f
1 changed files with 14 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

19
README.md
View file

@ -5,13 +5,22 @@ path**, extracted from a pure-Rust implementation into Lean 4 via
Charon/Aeneas — the same pipeline, discipline, and honesty rules as the Charon/Aeneas — the same pipeline, discipline, and honesty rules as the
four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`). four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`).
## STATUS: SIX LAYERS PROVEN — chain (5), WOTS+ (8), XMSS (10), hypertree (12), FORS (17), input-prep (2/3/4) ## STATUS: THE APEX IS PROVEN — the verify-path pyramid is complete (11 certificates)
`verification/check.sh` is **green** (exit 0): the model compiles, the `verification/check.sh` is **green** (exit 0): the model compiles, the
proofs compile, and the axiom audit passes. **Ten theorems across six proofs compile, and the axiom audit passes. **Eleven theorems across seven
verify-path layers, proven bottom-up. After de-plumbing round 2 the model layers — chain (5), WOTS+ (8), XMSS (10), hypertree (12), FORS (17),
carries no plumbing axioms on the verify path — its external surface is input-prep (2/3/4), and the apex (20): `fips205.slh_verify_128s_accepts_iff`
exactly the five SHA-2 oracles (plus off-path zeroize impls).** — the deployed SLH-DSA-SHA2-128s verifier returns `ok true` if and only if
the recomputed hypertree root byte-equals the pinned public-key root. Its
`#print axioms` cone is exactly `[propext, Classical.choice, Quot.sound]`
plus the five SHA-2 oracles, nothing else. Honest scope: the apex is an
acceptance characterization (accept = root equality over the extracted
recomputation, whose every loop is individually fidelity-certified by the
ten preceding theorems); it does not restate the recomputation as a
closed-form mathematical hypertree value. After de-plumbing rounds 1+2 the
model carries no plumbing axioms on the verify path — its external surface
is exactly the five SHA-2 oracles (plus off-path zeroize impls).**
- **`fips205.chain_free_loop_eq`** (Algorithm 5, WOTS+ chaining): the - **`fips205.chain_free_loop_eq`** (Algorithm 5, WOTS+ chaining): the
extracted `chain_free` loop equals the explicit s-fold hash chain, with extracted `chain_free` loop equals the explicit s-fold hash chain, with