drafts/ChainSpec.lean (NOT in Proofs/, NOT in check.sh — carries a
sorry, so nothing is claimed proven; H1/H2 hold):
- chainFoldN: the mathematical s-fold of the opaque hash F, threading
the hash-address (i, i+1, …, i+s-1) and index exactly as the extracted
loop body does. Equational spec (chain_free_loop = chainFoldN) — chosen
over a WP triple so it needs no assumption that the opaque oracle.f
succeeds (both sides fail together if it does).
- chain_free_loop_eq: induction on the step count via loop.eq_1.
BASE CASE PROVEN (empty range start..start reduces to ok tmp,
PartialOrdU32.lt start start = false). Step case is the one open
front: align the loop's monadic forward_checked with the fold's
start+1 (u32 add-spec from the no-overflow bound) and fold the loop
continuation back for the IH — the dalek loop-spec pattern, tractable.
De-plumbing (prior commit bde63f5) means this cone will carry only the
kernel three + oracle.f once closed. First real certificate incoming.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The verify cone iterates u32 ranges (for j in i..i+s). Aeneas.Std ships
a real Step instance only for usize (StepUsize), so u32 ranges extracted
as three opaque axioms (forward_checked / backward_checked /
steps_between) — which would poison every loop-bearing cone, i.e. chain
and everything above it.
Discharged in the hand-written external file (H4-sanctioned) with
FAITHFUL real definitions mirroring Rust's impl Step for u32
(core/src/iter/range.rs) and Aeneas.Std's StepUsize: forward/backward via
u32::try_from(n)-then-checked_{add,sub}, steps_between = saturating
difference. Verified in isolation (axiom-clean) and in place:
#print axioms on the u32 Step instance now reports exactly
[propext, Classical.choice, Quot.sound]. Model still compiles.
These are ordinary loop control, NOT the deployed hash boundary — the
five oracle axioms remain the only cryptographic externals.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The skeleton-era docs said 'six hash oracles' including prf — written
before the cone analysis showed prf/prf_msg are sign-side only. The
extracted model and FunsExternal carry exactly FIVE oracle axioms
(h_msg, f, h, t_l, t_len); the documented boundary now matches the
real one in README, TRUSTED-BASE, and extract.sh. Caught by the
post-flip drill's cross-consistency pass.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Full re-verification of the phase-1 window from primary sources, per the
standing drill after a model flip. Results:
- diff surface since snapshot 5dca0db: 414 additive lines only; every
generic algorithm file byte-untouched
- mechanical normalized diff: all 6 mono functions byte-identical to
their origins under ONLY the documented transforms (oracle renames,
call renames, single-slice M', is_err idiom)
- oracle wiring == deployed 128s HASHERS instance incl. the t_len: t_l
alias; constants == lib.rs 128s module; exactly 5 oracles in the cone
- FULL upstream suite in release WITH the patches: 13 lib + 3 ACVP KAT
integration + 12 py_vectors + 37 doc-tests, zero failures (stronger
regression evidence than the original window collected)
- extraction reproducible: regen byte-identical to committed gen/
- check.sh re-run green; commit-message numerics re-verified (62 defs,
0 sorry, 5+13 axioms, apex 63/30); remote heads match local
- hand externals proven to be header + template body exactly
One catch, fixed here: extract.sh still carried the pre-phase-1
'expect non-green' wording.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
The gate-0 fn-pointer blocker is cleared. This commits the phase-1
deliverable:
- verification/extract.sh: re-pointed at the monomorphic root
crate::verify_mono::slh_verify_128s with crate::verify_mono::oracle as
the opaque SHA-2 boundary (against fips205-source @ 2d89ee3).
- verification/gen/SlhVerify: the extracted Lean model — 62 defs, the
full verify cone (chain -> wots -> xmss -> ht -> fors ->
slh_verify_internal) up to the apex verify_mono.slh_verify_128s. No
sorry, no admit.
- verification/gen/SlhVerify/FunsExternal.lean + TypesExternal.lean:
hand-maintained externals with the two-class justification header —
(1) the five SHA-2 hash oracles = the deliberate cryptographic
boundary (the only axioms the apex certificate will carry beyond
Lean's three); (2) transpiler plumbing (try_from, is_err, iterator
Step/Take, zeroize) adopted as axioms for the phase-1 type-check, to
be discharged in the proof phase.
- verification/check.sh: real Phase-1 button — compiles the model under
lean-guard (memory-capped, serialized). GREEN. Still says NOTHING
PROVEN: a well-formed model is not a correct one.
Zero certificates. Proof layers (chain semantics -> ... -> acceptance
equation) are the next task.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Subject pinned: integritychain/fips205 @ 30bac08 via
saymrwulf/fips205-source @ 5dca0db. Parameter set SLH-DSA-SHA2-128s.
Scope: verify path only (slh_verify -> ... -> chain); six SHA-2 hash
oracles opaque per the standing boundary.
Gate-0 record (2026-07-22): charon clean on the full verify cone;
aeneas translates everything except the Hashers fn-pointer struct
(3 unique errors, the sole obstruction) -> phase 1 = named-opaque-
free-function compat patch in the snapshot repo, the established
dalek sha512-shim pattern.
check.sh exits non-green and says NOTHING PROVEN YET (H5, R3).
lean-guard copied; every future compile runs under it (S1, S2).
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
