The third reviewer demonstrated NEW-13: PROVENANCE.json is a tracked file that
nothing pins, and Phase 0's only completeness test was 'is the map non-empty'.
Deleting the harness_integrity_sha256 key therefore silently un-pinned BOTH
lean-guard and Proofs/Audit.lean with no diagnostic, after which the round-6
logic mutation ran to ALL GREEN over a repository proving False with the digest
byte-identical. Reproduced here before fixing. The required pin NAMES now live
hardcoded in check.sh — policy in the root of trust, values in the map — so a
shortened map is a build failure naming the missing entries. Self-test attack 18
performs the deletion.
GPT reviewer, independently: the documented '131 assertion points' was wrong.
Recounted from the code, the defensible figure is 137 mono-path evaluated cases
(9 retained original + 108 randomized + 10 NIST internal + 10 NIST
external-pure); 131 had folded in 3 deployed-only prehash cases while omitting
the retained test, and TRUSTED-BASE then decomposed it as 20 + 108 = 128,
contradicting itself. Item 9 now carries the full table, states that 127 of the
137 compare mono against deployed, keeps the 3 prehash cases explicitly outside
the total, and records that only two SHA2-512 and one SHAKE-256 vector are
executable there — so this is not NIST coverage of all four supported prehash
variants.
Also from GPT: PROVENANCE.json contradicted itself, saying extraction
'reproduces all four model files byte-identically' while its own _comment
correctly said the two *External files are hand-maintained. Extraction
regenerates two files; the other two are byte-pinned. Corrected.
TRUSTED-BASE item 11 now discloses that PROVENANCE.json is itself load-bearing
and unpinned, and item 7's stale snapshot head is fixed. README states the
lean-guard graceful fallback and that the empirical bridge runs on stable Rust
without any Lean toolchain (round-7 NEW-16), which is the first load-bearing
part of this work a third party can reproduce with cargo alone.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
The companion fips205-source commit adds NIST ACVP SHA2-128s verification
vectors and a real differential bridge. This repo re-pins to it and replaces the
word "finite" with numbers, per external review rounds 4-6.
- extract.sh + PROVENANCE re-pinned 797b4ef -> 3153988. The provenance guard
did its job first: it REFUSED the moved source until the pin was rotated
deliberately.
- VERIFIED that the test/vector commit does not perturb the proved model: after
re-extraction all four pinned model files are byte-identical
(Types db720b4a…, Funs 7b7de55f…, TypesExternal 37958beb…, FunsExternal
5efe551c…), check.sh is ALL GREEN, and the audit digest is unchanged
(d83e297a…). The only regenerated difference is the untracked Aeneas
*_Template.lean byproduct, which Phase 0 purges.
- TRUSTED-BASE item 9 and the README now state the bridge's actual size:
131 assertion points (was 9), of which 20 are NIST ACVP SHA2-128s
known-answer tests run against the proved path — 10 from the `internal`
group (whose message IS M', exactly what slh_verify_128s consumes) and 10
from `external pure` where mono, the deployed verifier and NIST must all
agree, 9 of those with a NON-EMPTY context, which is the first empirical
check of the domain-separator byte and context prefix that item 10 declares
outside every proof. Both documents keep saying plainly that a passing
differential test is evidence, not a proof.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Round 3 returned fit-once-one-item-lands (first non-DO-NOT-ATTEST verdict).
The one blocker is an independently-executed toolchain session, which is
operator-side. This commit closes the two nonblocking recommendations:
- extract.sh: source the aeneas toolchain env AFTER the provenance guard, so
a party without the toolchain gets the clean exit-2/3/4 diagnostics instead
of a confusing env error (the reviewer hit exactly this). Re-verified: exit
2/3 clean in an env-stripped shell, happy path byte-identical.
- RECORDED-RUN.md: append the locked cargo run under the pinned nightly —
the differential bridge test mono_matches_deployed_verify passes with
--locked --lib on nightly-2026-06-01, and the full default-features suite
is green (13+3+12+37 passed, 0 failed). Also documents why single-feature
integration tests cannot compile (upstream test files hardcode all twelve
parameter sets), resolving the round-1 GPT observation.
No proof, model, or gate change.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Addresses the round-2 reviewer punch-list. No theorem statement, proof term,
or fold definition changed; the eleven cones are unchanged (independent
collectAxioms dump in verification/RECORDED-RUN.md).
AUDIT GATE (both reviewers, the critical one)
- Retire the bash #print-axioms text parser (fail-open on empty/truncated
reports, and only a SUBSET check). Replace with verification/Proofs/Audit.lean:
reads each certificate's cone from the kernel via collectAxioms and asserts
EXACT set equality against its expected boundary. Extra axiom, dropped
oracle, renamed/deleted cert, or an axiom/opaque sham each throw -> non-zero
Lean exit. No text to misparse; nothing fails open. check.sh Phase 3 now just
compiles it (and still requires the explicit PASSED line).
- check-selftest.sh rewritten to attack the new gate: dead-file, smuggled extra
axiom (named), dropped-oracle (subset would pass, exact must not), and a
vanished certificate (the collectAxioms-returns-[] trap). All four rejected.
REPRODUCIBILITY (GPT B1.4 / B1.5)
- extract.sh refuses a wrong-commit or dirty source tree (fail-closed), takes
an optional source-path arg, and pins the source commit.
- verification/PROVENANCE.json: single machine-readable pin set (source +
charon + aeneas commits/channel + lean + ocaml) with generated-file sha256.
- Re-running extract.sh reproduces gen/SlhVerify/{Types,Funs}.lean
byte-identically (companion fips205-source commit adds Cargo.lock +
rust-toolchain.toml; verified not to perturb the model).
DOC HONESTY (both reviewers)
- README: fix the self-contradiction (apex "not yet proven" trailer vs the
proven apex), the false "oracles kept OUTSIDE every cone" (they are INSIDE,
by design), "deployed monomorphic path" and "semantics-identical for every
parameter set" overclaims, "only two lines changed", stale snapshot head;
retitle the stale future-tense "what will be claimed" section.
- TRUSTED-BASE: drop "nothing proven yet"; add base_2b-inner and deployment-
bridge non-claims explicitly; current pin.
- ChainSpec header: "deployed monomorphic path" -> private verify_mono facade
(comment only).
Co-Authored-By: Claude Opus 4.8 <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>
