mirror of
https://github.com/saymrwulf/fips205-slhdsa-verified.git
synced 2026-09-03 19:53:49 +00:00
mrwulf
1b430dfd68
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>
10 lines
554 B
Text
10 lines
554 B
Text
*.olean
|
|
target/
|
|
.lake/
|
|
# *_Template.lean is NO LONGER ignored: it is Aeneas's own statement of what
|
|
# the extraction needs from outside, and it is the only artifact against which
|
|
# "does the model ANSWER the extraction" can be asked. Committed and pinned.
|
|
# SlhVerify.llbc is NO LONGER ignored. It is the intermediate Charon produces
|
|
# and Aeneas consumes, and committing it is what makes the LLBC->Lean half of
|
|
# extraction independently re-runnable. Round-9 review (GPT-5.6) found
|
|
# TRUSTED-BASE claiming it was committed while .gitignore excluded it.
|