round 8: self-deriving harness pins, honest extraction guarantees, attestation basis

Third reviewer returned ATTEST-with-conditions at 1bc4f39. Its conditions are
committed verbatim as ATTESTATION-BASIS.md so the limits travel with the
artifact instead of living in a review document a consumer never sees. Condition
9 — that extract.sh's byte-identical regeneration has never been observed by any
party but the author — is the campaign's last open item, and the file records
that both reviewers are now blocked on it for different environmental reasons.

HARNESS PINS ARE NOW SELF-DERIVING. My round-7 fix hardcoded the required pin
names, which the reviewer correctly called a second thing to keep in sync, and
it supplied the boundary the harness does have: the executable bit. check.sh now
requires every executable file in verification/ to be pinned (itself excluded —
it cannot pin itself), plus Proofs/Audit.lean. A new harness script therefore
fails closed until pinned. Consequence, and the reviewer argued for it:
check-selftest.sh, drill.sh and extract.sh are now pinned too — the self-test is
the only artifact demonstrating the gates work, and its assertions have been
defective in four consecutive rounds, so weakening it should be a reviewable
rotation rather than an unnoticed edit.

THE EXTRACTION SCRIPT'S GUARANTEES ARE NOW STATED HONESTLY. The reviewer found a
tautological assert in it — comparing a dict against the comprehension that had
just built it — in the script written to fix a provenance-honesty defect. My
first repair (comparing kept[k] against t[k]) was tautological for the same
reason, which I confirmed by negative test. No check inside a transformer can
detect a corrupted input, because the transformer defines the output from that
input; that lesson is now recorded in the code. Both fake checks are gone and
the header and provenance text name what actually protects the result — the
pinned SOURCE_SHA256, the sk-must-be-present check, the group and test counts,
and verify mode — each of which I negative-tested.

Also: the self-test keeps its backups outside verification/ (cp -p preserves the
executable bit, so an in-tree backup would have looked like an unpinned harness
file and failed a run for an unrelated reason); the Phase-0 banner no longer
says a file 'differs' when an entry is simply absent; and attack 18's assertion
follows the renamed diagnostic and now requires both missing pins to be named.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>

ATTESTATION-BASIS.md

@@ -0,0 +1,105 @@
+# Attestation basis — independent technical review
+
+This file records the **reviewer's own words**, verbatim, as the conditions
+attached to any attestation of this repository. It is committed here so that the
+limits travel with the artifact rather than living in a review document the
+consumer never sees.
+
+Nothing in this file is a decision to attest. The signing-key halt and the
+paper-appeal gate are the operator's, and an attest verdict from a reviewer is a
+technical input to that decision, not the decision.
+
+---
+
+## Verdict
+
+**Round 8, third reviewer, 2026-07-28: ATTEST, with the conditions below.**
+
+Basis the reviewer performed on hardware, an OS and a toolchain build that are
+not the author's: `check.sh` ALL GREEN at `1bc4f39` with six pins verified and
+the audit digest `d83e297a…`; `check-selftest.sh` green (17 attacks + the
+digest-coverage check); the audit digest recomputed *outside* `check.sh` from a
+bare `lean Proofs/Audit.lean` and matched byte-for-byte against the committed
+`AUDIT-MANIFEST.txt`; NEW-13 attacked five ways; the NIST vector file
+independently re-derived from the official 30.7 MB upstream file and found
+byte-identical; the full empirical bridge executed on stable Rust; and the ACVP
+harness mutation-tested (a flipped bit in a valid vector and a deleted NIST test
+both correctly fail).
+
+Not performed by any reviewer: `verification/extract.sh`. See condition 9.
+
+---
+
+## Conditions, verbatim from the reviewer
+
+> What is established: eleven Lean 4 theorems over the Charon/Aeneas-extracted
+> model of `verify_mono::slh_verify_128s`, the private monomorphic re-expression
+> of the SLH-DSA-SHA2-128s verify path. Ten are loop-fidelity theorems; the apex,
+> `fips205.slh_verify_128s_accepts_iff`, characterises acceptance — the extracted
+> verifier returns `ok true` if and only if the recomputed hypertree root
+> byte-equals the pinned public-key root. Every certificate's axiom cone is
+> exactly Lean's three kernel axioms plus the named SHA-2 oracles that layer
+> reaches, machine-checked inside Lean and bound by a SHA-256 digest over the
+> policy constants, the elaborated statements and the specification bodies.
+>
+> This attestation carries the following limits, all of which are stated in the
+> repository's own `TRUSTED-BASE.md` and all of which I verified are accurate:
+>
+> 1. **The five SHA-2 hash oracles are opaque assumptions.** Their conformance to
+>    FIPS 180-4 is not proven here. `oracle.t_l` and `oracle.t_len` are two
+>    independent axioms over one Rust primitive — conservative, but the model
+>    cannot express that they agree.
+> 2. **The ten loop certificates are transliteration-fidelity results, not
+>    conformance results.** Each equates a generated loop with a hand-written
+>    reference fold built from the *same* extracted primitives, so it pins what
+>    the extracted code does at each index and makes it visible; it does not
+>    exclude a wrong ADRS field or a wrong schedule relative to FIPS 205. Mapping
+>    each fold onto the standard remains a human reading step.
+> 3. **The apex does not compose the ten.** It is a structural factorization of
+>    the extracted verifier around its final equality check and references none
+>    of them; it would remain provable if one were deleted.
+> 4. **`base_2b`'s inner accumulation loop has no certificate.** It determines
+>    the FORS indices and WOTS+ digits, so a defect there could change the
+>    recomputed root while all eleven theorems still hold.
+> 5. **Everything above the extraction root is uncovered:** M′ assembly, the
+>    pure-versus-prehash domain-separator byte, the `ctx.len() > 255` bound, and
+>    signature/public-key deserialization.
+> 6. **The bridge from the proved `verify_mono` facade to the deployed generic
+>    `pk.verify()` is empirical, not a machine-checked refinement:** 137 evaluated
+>    input/verdict cases on the proved path, of which 20 are NIST ACVP
+>    known-answer tests and 127 compare mono against the deployed verifier. A
+>    passing differential test is evidence, not a proof.
+> 7. **Trusted and unbound by anything the button can check:** the Lean kernel and
+>    its three axioms; the Charon/Aeneas transpilation pair; `verification/check.sh`
+>    itself; `~/aeneas-toolchain/env.sh`; the `$AENEAS_HOME` Aeneas/Lean library
+>    the proofs are checked against; `python3`; and the Lean toolchain.
+>    `lean-guard` and `Proofs/Audit.lean` are sha256-pinned, so tampering with
+>    either is a build failure rather than a silent green; an author who edits one
+>    *and* rotates its pin in the same commit is caught only by reading the diff
+>    at the pin.
+> 8. **Scope is SLH-DSA-SHA2-128s only**, verify path only. Key generation and
+>    signing are out of scope. No reproducible-builds claim: the proof is about
+>    the pinned source, not any compiled binary.
+> 9. **`verification/extract.sh`'s byte-identical regeneration of the Lean model
+>    from the pinned Rust source has never been observed by any party other than
+>    the author.** Every other load-bearing claim in this repository has been
+>    reproduced by an independent reviewer on different hardware; this one has
+>    not, and it is the claim that ties the Lean model to the Rust source. Until a
+>    third party re-runs `extract.sh` at the pinned Charon/Aeneas commits and
+>    obtains the four `model_integrity_sha256` hashes, the correspondence between
+>    `fips205-source@c945821` and `verification/gen/SlhVerify/*.lean` rests on the
+>    author's attestation alone.
+
+The reviewer's instruction on condition 9: if a third party later succeeds at
+`extract.sh`, sentence 9 is to be **replaced with a statement of what was
+reproduced, by whom, on what platform and at which commits — not deleted.**
+
+---
+
+## Status of condition 9 as of 2026-07-28
+
+Still open. Two independent reviewers have now been unable to close it for
+different environmental reasons: one sandbox blocks `static.rust-lang.org` and
+`opam.ocaml.org` so Charon and Aeneas cannot be built there; the other declined
+the task of building the two pinned tools from source. The claim therefore
+remains author-attested only, exactly as condition 9 states.

verification/PROVENANCE.json

@@ -45,9 +45,12 @@
     "gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f"
   },
   "harness_integrity_sha256": {
-    "_comment": "The harness is part of the trusted computing base. check.sh shells out to lean-guard for every compile (round-5 NEW-3: stubbing it alone yielded ALL GREEN in 3.6s over destroyed proofs), and Proofs/Audit.lean is the program that COMPUTES the digest it is judged by (round-6 NEW-7: flipping two fail-closed guards to `unless true` let a repo proving False pass with the digest BYTE-IDENTICAL \u2014 the digest binds the audit's DATA, never its LOGIC). Both are sha256-pinned by Phase 0, so tampering with either is a build failure rather than a silent green, and any legitimate change is a reviewable pin rotation. STILL trusted and unbound, disclosed in TRUSTED-BASE.md item 11: check.sh itself, ~/aeneas-toolchain/env.sh, $AENEAS_HOME, python3, and the Lean toolchain.",
+    "_comment": "The harness is part of the trusted computing base and its membership is now SELF-DERIVING: check.sh requires every executable file in verification/ to appear here (round-8 review \u2014 a hardcoded list was itself a second thing to keep in sync), plus Proofs/Audit.lean, which is not executable but computes the digest it is judged by. check.sh itself is excluded: it cannot pin itself, and is disclosed as trusted-unbound in TRUSTED-BASE.md item 11. Pinning check-selftest.sh matters beyond the button: it is the only artifact demonstrating the gates work, and its assertions have been defective in four consecutive rounds, so weakening it is now a reviewable pin rotation rather than an unnoticed edit.",
     "lean-guard": "690d861cfd81b327604ffd5ef85599ee01b2bcd943907f5b71b8b6f99bad418f",
-    "Proofs/Audit.lean": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e"
+    "Proofs/Audit.lean": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e",
+    "check-selftest.sh": "c6811482e25ae6e1fffa6ca50e60541e8e609a70c951db6bec4d2d39a4849e9a",
+    "drill.sh": "915cf9310fa168c14ca5d76a1b84fd3b19acdfef9dfd0b03b01b19883548719e",
+    "extract.sh": "2829b863301e1e6677376dd2c948673341e934c81dd55a19ff764f563ff22665"
   },
   "audit_gate": "verification/Proofs/Audit.lean \u2014 in-Lean audit (round 5). Per certificate: exact cone equality (collectAxioms) + elaborated-statement check. Enumeration: EVERY declaration kind (def/theorem/opaque/axiom \u2014 round 4 matched theorems only, so a `def : False` passed) in the eight certificate modules AND in Audit.lean itself (the auditor is not exempt). Binding digest: check.sh binds to the SHA-256 of a canonical AUDIT-MANIFEST block covering the POLICY constants (allowedBoundary + certModules \u2014 round-5 NEW-1: widening allowedBoundary previously re-opened the False-proof with the fingerprint byte-identical), every certificate's fully-elaborated statement, and every reachable specification definition's fully-elaborated BODY (round-5 NEW-2: redefining a reference fold to *be* the extracted loop previously left cone and fingerprint intact while the certificate degenerated to `loop = loop`). The 32-bit Expr.hash is retained only as a per-certificate diagnostic, not as the binding. Fail-closed; adversarially exercised by check-selftest.sh. check.sh Phase 0 additionally purges stale .olean files, forbids stray .lean outside gen/ and Proofs/, and pins model + harness bytes."
 }

verification/RECORDED-RUN.md

@@ -450,3 +450,82 @@ statements, hand-edited models, dropped manifest rows, widened policy,
 specification folds redefined to the loop, a False-proof in the auditor,
 a stubbed harness, stray modules, and a shortened pin map.
 ```
+
+## Round-8 — author-agent run, 20260728T124039Z, proof repo @ (this commit)
+
+Captured with `tee`. The third reviewer independently ran check.sh and
+check-selftest.sh to green at 1bc4f39 on its own hardware and toolchain, and
+recomputed the audit digest outside check.sh — see ATTESTATION-BASIS.md.
+PIN ROTATIONS: harness_integrity_sha256 GAINS check-selftest.sh, drill.sh and
+extract.sh (the harness set is now self-derived from the executable bit);
+check-selftest.sh re-pinned twice during this round as it was edited. No model
+pin rotated; the audit digest is unchanged at d83e297a….
+
+### check.sh
+```
+fips205-slhdsa-verified — check
+===============================
+=== Phase 0: build hygiene + model/harness integrity ===
+  ✓ Proofs/Audit.lean
+  ✓ check-selftest.sh
+  ✓ drill.sh
+  ✓ extract.sh
+  ✓ gen/SlhVerify/Funs.lean
+  ✓ gen/SlhVerify/FunsExternal.lean
+  ✓ gen/SlhVerify/Types.lean
+  ✓ gen/SlhVerify/TypesExternal.lean
+  ✓ lean-guard
+=== Phase 1: compile the extracted model ===
+  · gen/SlhVerify/TypesExternal
+  · gen/SlhVerify/Types
+  · gen/SlhVerify/FunsExternal
+  · gen/SlhVerify/Funs
+=== Phase 2: compile the proofs ===
+  · ChainSpec
+  · WotsSpec
+  · XmssSpec
+  · HtSpec
+  · ForsInnerSpec
+  · ForsOuterSpec
+  · InputPrepSpec
+  · ApexSpec
+=== Phase 3: in-Lean audit (cones + statement fingerprints + enumeration) ===
+  ✓ exact-cone audit PASSED
+  ✓ audit-manifest digest matches (sha256 d83e297a49094c97…)
+
+ALL GREEN — model compiles, proofs compile, and every certificate cone
+equals EXACTLY the three kernel axioms plus its documented SHA-2 oracles.
+Certificates proven: fips205.chain_free_loop_eq fips205.wots_loop1_eq fips205.xmss_loop_eq fips205.ht_loop_eq fips205.fors_inner_loop_eq fips205.fors_outer_loop_eq fips205.to_int_loop_eq fips205.to_byte_loop_eq fips205.wots_csum_loop_eq fips205.base2b_outer_loop_eq fips205.slh_verify_128s_accepts_iff
+```
+
+### check-selftest.sh (17 attacks + digest-coverage check)
+```
+check-selftest: attacking the gates
+====================================
+✓ attack 1 rejected (dead-file gate)
+✓ attack 2 rejected (extra-axiom detection — evil_ax named)
+✓ attack 3 rejected (missing-oracle detection — exact cone, not subset)
+✓ attack 4 rejected (existence check — a vanished cert cannot pass as 0-axiom)
+✓ attack 5 rejected (enumeration — an un-manifested False theorem cannot pass)
+✓ attack 6 rejected (statement check — a gutted statement of the same cone cannot pass)
+✓ attack 7 rejected (Phase 0 model-byte integrity)
+✓ attack 8 rejected (audit-manifest digest — a silently-dropped cert cannot pass)
+✓ attack 9 rejected (digest covers allowedBoundary — the policy cannot be widened silently)
+✓ attack 10 rejected (a specification fold cannot be silently redefined to the loop)
+✓ attack 11 rejected (enumeration covers every declaration kind, not just theorems)
+✓ attack 12 rejected (the auditor audits itself — no exemption)
+✓ attack 13 rejected (Phase 0 pins lean-guard — the harness is in the TCB and bound)
+✓ attack 14 rejected (no .lean may sit outside gen/ and Proofs/)
+✓ attack 16 rejected (Phase 0 purges every .olean under verification/, so an
+  orphan compiled module with no source cannot satisfy an import)
+✓ attack 17 rejected (Phase 0 pins Audit.lean — its LOGIC cannot be silently switched off)
+✓ attack 18 rejected (the pin map cannot be silently shortened — required names are in check.sh)
+✓ check 15 passed (the hashed block carries all 12 reference-fold bodies,
+  including the recursive _f companions and their extracted-primitive calls)
+
+SELFTEST GREEN: 17 attacks rejected + digest-coverage check — dead files, extra axioms, dropped
+oracles, vanished certs, un-manifested False theorems AND defs, gutted
+statements, hand-edited models, dropped manifest rows, widened policy,
+specification folds redefined to the loop, a False-proof in the auditor,
+a stubbed harness, stray modules, and a shortened pin map.
+```

verification/check-selftest.sh

@@ -36,9 +36,18 @@ HERE="$(cd "$(dirname "$0")" && pwd)"
 cd "$HERE"
 source ~/aeneas-toolchain/env.sh
 
+# Backups live OUTSIDE verification/. Round-8 added a self-deriving harness rule:
+# every executable file in this directory must be pinned. `cp -p` preserves the
+# executable bit, so an in-tree `check.sh.sfbak` would look like an unpinned
+# harness file and fail the run for a reason unrelated to the attack — the
+# defect class this suite exists to catch.
+SFBAK="$(mktemp -d)"
 BAKS=()
-save()    { cp -p "$1" "$1.sfbak"; BAKS+=("$1"); }
+save()    { cp -p "$1" "$SFBAK/$(printf %s "$1" | tr / _)"; BAKS+=("$1"); }
-restore() { for f in "${BAKS[@]:-}"; do [ -f "$f.sfbak" ] && mv -f "$f.sfbak" "$f"; done; BAKS=(); }
+restore() { for f in "${BAKS[@]:-}"; do
+              b="$SFBAK/$(printf %s "$f" | tr / _)"
+              [ -f "$b" ] && cp -p "$b" "$f" && rm -f "$b"
+            done; BAKS=(); }
 # Proofs/Audit.lean is sha256-pinned by Phase 0 since round 6 (NEW-7). An attack
 # that mutates the audit's DATA must therefore ALSO rotate that pin, otherwise it
 # is stopped by the byte pin and never reaches the mechanism it means to test —
@@ -56,6 +65,7 @@ PY
 }
 cleanup() {
   restore
+  rm -rf "$SFBAK" 2>/dev/null
   rm -f Proofs/Stray.lean Proofs/EvilSpec.lean Evil.lean Evil.olean \
         Proofs/*.olean gen/SlhVerify/*.olean *.olean .audit-manifest.observed 2>/dev/null
   return 0
@@ -342,8 +352,12 @@ del d["harness_integrity_sha256"]
 json.dump(d, open(p, "w"), indent=2); open(p, "a").write("\n")
 PY
 ./check.sh > /tmp/sf18.out 2>&1 && fail "ATTACK 18 SUCCEEDED: the harness pins were deleted and the button stayed GREEN!" /tmp/sf18.out
-grep -q "pin map INCOMPLETE" /tmp/sf18.out || fail "ATTACK 18: rejected but not via the pin-map completeness check" /tmp/sf18.out
+# The diagnostic is "UNPINNED harness file" since round 8, when the required set
-grep -q "Proofs/Audit.lean" /tmp/sf18.out || fail "ATTACK 18: rejected but did not name the missing pin" /tmp/sf18.out
+# became self-deriving from the executable bit: deleting the map now reports ALL
+# five harness entries as unpinned, not just the two that used to be hardcoded.
+grep -q "UNPINNED harness file" /tmp/sf18.out || fail "ATTACK 18: rejected but not via the pin-map completeness check" /tmp/sf18.out
+grep -q "Proofs/Audit.lean" /tmp/sf18.out || fail "ATTACK 18: rejected but did not name the audit driver" /tmp/sf18.out
+grep -q "lean-guard" /tmp/sf18.out || fail "ATTACK 18: rejected but did not name lean-guard" /tmp/sf18.out
 restore
 echo "✓ attack 18 rejected (the pin map cannot be silently shortened — required names are in check.sh)"
 

verification/check.sh

@@ -75,7 +75,7 @@ fi
 #     trusted computing base: round 5 demonstrated that stubbing it alone yields
 #     ALL GREEN in 3.6s over destroyed proofs. It is KEPT (it is the memory cap
 #     that protects this machine after the 12.2GB OOM incident) and pinned.
-python3 - "$HERE/PROVENANCE.json" "$HERE" <<'PY' || { echo "INTEGRITY FAILED (a pinned file differs from PROVENANCE.json — hand-edited model or harness?)"; exit 1; }
+python3 - "$HERE/PROVENANCE.json" "$HERE" <<'PY' || { echo "INTEGRITY FAILED (a pinned file differs from PROVENANCE.json, or a required file is unpinned — see the specific line above)"; exit 1; }
 import json, sys, hashlib, os
 prov = json.load(open(sys.argv[1])); here = sys.argv[2]
 files = {k: v for k, v in prov.get("model_integrity_sha256", {}).items() if not k.startswith("_")}
@@ -92,15 +92,27 @@ bad = 0
 # proving False, digest byte-identical. The model side self-protected only
 # because the gen/ set assertion below derives its requirement from the
 # filesystem; the harness side had no such cross-check.
-REQUIRED = {
+# SELF-DERIVING, so a NEW harness file cannot be forgotten. Round-8 review
-    "lean-guard", "Proofs/Audit.lean",
+# observed that a hardcoded list is itself a second thing to keep in sync, and
-    "gen/SlhVerify/Types.lean", "gen/SlhVerify/Funs.lean",
+# supplied the natural boundary the harness does have: THE EXECUTABLE BIT. Every
-    "gen/SlhVerify/TypesExternal.lean", "gen/SlhVerify/FunsExternal.lean",
+# executable file in verification/ is something this script can shell out to, so
+# every one must be pinned; a new script therefore fails closed until it is.
+# check.sh is excluded because it cannot pin itself — it is the root of trust,
+# and TRUSTED-BASE.md item 11 says so. Proofs/Audit.lean is added explicitly: it
+# is not executable but it computes the digest it is judged by.
+# Backup files are excluded by extension only because check-selftest.sh keeps its
+# backups OUTSIDE this directory now; nothing here is expected to match.
+harness = {
+    f for f in os.listdir(here)
+    if os.path.isfile(os.path.join(here, f))
+    and os.access(os.path.join(here, f), os.X_OK)
+    and f != "check.sh"
 }
-missing = REQUIRED - set(files)
+harness.add("Proofs/Audit.lean")
+missing = harness - set(files)
 if missing:
     for m in sorted(missing):
-        print(f"  ✗ pin map INCOMPLETE — no entry for {m}")
+        print(f"  ✗ UNPINNED harness file (executable, or the audit driver): {m}")
     bad = 1
 for rel, want in sorted(files.items()):
     p = os.path.join(here, rel)