Round-9 review (GPT-5.6, R9-F2, BLOCKER). TRUSTED-BASE said:
"The .llbc is committed, so the SECOND step can be re-run by anyone with
the pinned Aeneas and this repository"
.gitignore excluded it. `git ls-files` had no LLBC. The file existed only on
the author's disk. I ran `ls`, saw it, and wrote the claim without running
`git ls-files` — so a sentence that reads as an independent-reproducibility
guarantee was true for exactly one person. The experiment itself was real:
re-running Aeneas on that LLBC did reproduce Types.lean and Funs.lean
byte-identically. What was false is that anyone else could repeat it.
CHASING IT FOUND WORSE. `generated_artifacts_sha256` was read by NOTHING —
check.sh had zero references to it. Its Types.lean and Funs.lean entries
matched only because those files are ALSO pinned in model_integrity_sha256,
which is checked. The .llbc entry, the one nothing else covered, had been
stale since review round 2 (522d8b2): the source was re-extracted on
2026-07-28, the model files and their pins were updated, and this pin was not.
It named d8ec0b00…, an artifact that did NOT produce the committed model. The
file that did is 69666ddc… — timestamped nine seconds before Types.lean and
Funs.lean, and demonstrably regenerating them byte-for-byte.
A pin nothing verifies drifts, and nobody notices. That is the finding, and it
is a sharper instance of the pattern than the one the reviewer reported.
· .gitignore no longer excludes SlhVerify.llbc; it is committed (1.6 MB)
· its pin corrected to the artifact that actually produced the model
· check.sh Phase 0 now verifies generated_artifacts_sha256, so the block
stops being decorative. Negative-tested: one appended byte gives
`✗ SlhVerify.llbc: sha256 dd5925770bc7 ≠ pinned 69666ddc43a4`, exit 1
· TRUSTED-BASE item 3 rewritten. It now says what committing the LLBC does
and does NOT buy: the Lean model is the faithful Aeneas image of THAT
intermediate, and whether the intermediate is the faithful Charon image of
fips205-source@a3ce8e8 rests on the author alone. Verifying the committed
LLBC against itself establishes nothing about Charon.
"Do not read the second half as evidence for the first."
· README qualified AT THE CLAIM SITE, not via a later link
Button green after every edit; accounting still closes at 300 with no residual.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Round-8 estate review (GPT-5.6): this repository shipped a
FunsExternal_Template.lean / FunsExternal.lean pair and NO correspondence
check at all. This commit explains why, and fixes the cause rather than
bolting a check onto a missing input.
THE TEMPLATE WAS BEING DELETED. check.sh removed `*_Template.lean` on every
run and .gitignore excluded it. The stated reason was sound — "the verdict must
depend on COMMITTED BYTES, never on untracked build state", and an untracked
file on LEAN_PATH is exactly that problem. But it is the weaker of the two
available remedies. The ed25519 forks face the identical choice and COMMIT AND
PIN their templates, which removes the untracked state just as completely and
keeps the evidence.
The evidence is the point. The template is Aeneas's own statement of what the
extracted Rust needs from outside, and it is the ONLY artifact against which
"does the hand-written model ANSWER the extraction?" can be asked. Deleting it
made that question unaskable here — which is precisely why no check existed.
· template committed and pinned in model_integrity_sha256
· .gitignore no longer excludes it
· check.sh no longer deletes it, and says why at length
· Phase 0d runs model-correspondence.py — the forks' scanner, including both
round-8 corrections: a named Lean `section` does not qualify declaration
names, and an EXTRA AXIOM in the model (an assumption no template asks for)
fails rather than passing as a silent row
· MODEL-CORRESPONDENCE.txt committed, pinned, and compared byte-for-byte
Result: 11 externals, every one answered by the pinned model, no UNRESOLVED and
no EXTRA-AXIOM. Negative-tested — deleting one `axiom` from the model yields
`verify_mono.oracle.h_msg|UNRESOLVED` and a non-zero exit; restoring it returns
to green.
AND A REPRODUCIBILITY RESULT, obtained while recovering the deleted template.
charon is not available on this machine (the same wall the reviewer hit), but
SlhVerify.llbc IS committed and Aeneas is installed, so extraction step [2/2]
was re-run alone from the committed LLBC:
Types.lean: IDENTICAL Funs.lean: IDENTICAL
The LLBC -> Lean half of the extraction reproduces byte-for-byte from committed
inputs, on demand, by anyone with Aeneas and this repository. This does NOT
close `slh-extraction-unreproduced`: the Rust -> LLBC half still requires
charon, and this was still run by the author. Half the chain, verifiable today.
Co-Authored-By: Claude Opus 4.8 <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>
