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: six layers / ten theorems; no plumbing axioms on the verify path

Browse source 
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-24 09:01:50 +02:00
parent c28effd85e
commit c7c750f945
1 changed files with 21 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
README.md
View file

@ -5,11 +5,13 @@ 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: FIVE LAYERS PROVEN — chain (5), WOTS+ loop (8), XMSS (10), hypertree (12), FORS (17) ## STATUS: SIX LAYERS PROVEN — chain (5), WOTS+ (8), XMSS (10), hypertree (12), FORS (17), input-prep (2/3/4)
`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. **Six theorems across five proofs compile, and the axiom audit passes. **Ten theorems across six
verify-path layers, proven bottom-up:** verify-path layers, proven bottom-up. After de-plumbing round 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
@ -77,9 +79,22 @@ wrong-message), re-run green after every source patch.
peeling its 16-bind body with `bind_congr` (a bare `rfl` there whnf-times- peeling its 16-bind body with `bind_congr` (a bare `rfl` there whnf-times-
out over the nested inner `loop`). out over the nested inner `loop`).
The remaining layers (the input-prep/digest-split composition and the apex) - **input-prep** (`fips205.to_int_loop_eq`, `to_byte_loop_eq`,
are not yet proven — the pyramid rises one certificate at a time, each `wots_csum_loop_eq`, `base2b_outer_loop_eq` — Algorithms 2/3/4 + the WOTS+
audited to the same boundary. checksum): the byte→integer, integer→byte, checksum, and digit-decomposition
loops that prepare the verifier's inputs. All four cones are **exactly**
`[propext, Classical.choice, Quot.sound]` — pure kernel-3, no hash oracle
(byte/bit arithmetic touches no hash). `base_2b`'s inner `while` loop is
threaded opaquely, as every layer treats its sub-loops. These proofs became
possible after **de-plumbing round 2** (snapshot `bea1051`) rewrote
`to_int`'s `iter().take()` and `base_2b`'s `iter_mut()` as index loops,
removing the last `Take`/`IterMut` iterator adapters; the obsoleted `Take`
axiom was then deleted.
The remaining work (the digest-split composition and the apex — the top-level
`slh_verify` accepting iff the recomputed hypertree root equals the pinned
public-key root) is not yet proven. The pyramid rises one certificate at a
time, each audited to the same boundary.
## Subject ## Subject