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 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>
