2026-09-13 21:30:32 +00:00
10 changed files with 48 additions and 725 deletions
--- a/ATTESTATION-BASIS.md
+++ b/ATTESTATION-BASIS.md
@ -1,105 +0,0 @@
 # 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.
--- a/README.md
+++ b/README.md
@ -5,7 +5,7 @@ path**, extracted from a pure-Rust implementation into Lean 4 via
 Charon/Aeneas — the same pipeline, discipline, and honesty rules as the
 four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`).
-## STATUS: eleven certificates over the extracted verify model (external review rounds 1–6 applied)
+## STATUS: eleven certificates over the extracted verify model (external review rounds 1–5 applied)
 `verification/check.sh` is **green** (exit 0): the model compiles, the proofs
 compile, and the audit passes. The audit runs **inside Lean**
@ -64,19 +64,8 @@ cannot translate the deployed `Hashers` function-pointer struct):
  certificate — and it determines the FORS indices / WOTS digits, so a defect
  there could change the recomputed root while all eleven theorems still hold.
 - **Not the deployed public verifier:** the proved subject is the private
-  `verify_mono` facade; the bridge to upstream's generic `pk.verify()` is a
+  `verify_mono` facade; the bridge to upstream's generic `pk.verify()` is the
-  finite **differential test**, not a machine-checked refinement. Its size is
+  finite in-snapshot **differential test**, not a machine-checked refinement.
  now stated rather than left to the word "finite": **137 evaluated
  input/verdict cases on the proved path**, of which **20 are NIST ACVP
  SHA2-128s known-answer tests** (9 retained original + 108 randomized + 10 NIST
  internal + 10 NIST external-pure; see TRUSTED-BASE.md item 9 for the table and
  for the 3 deployed-only prehash cases counted separately). Until 2026-07-28 it
  was nine cases from a single seed, and this parameter set had *no* NIST
  verification coverage at all — the vectors vendored upstream contain no
  SHA2-128s sigVer group, so the 128s groups were extracted from the official
  NIST ACVP-Server set by a committed, re-runnable script
  (`tests/nist_acvp_vectors/extract_sha2_128s.py` in the snapshot repo) that
  pins the upstream hash and fails closed on any drift.
 - **Not closed-form FIPS 205 correctness:** the folds are transliterations of
  the extracted loops (the hash primitives stay opaque); nothing here relates
  the recomputed root to a mathematical SLH-DSA specification.
@ -167,10 +156,8 @@ casts, the WOTS+ checksum `iter().take()` + `&u32` Sub → an index loop —
 each site a local rewrite whose equivalence is argued in the commit and
 checked, for SHA2-128s, by the differential test; the obsoleted transpiler
 axioms were deleted from the external files); fidelity pinned by that
-differential test in the snapshot — since 2026-07-28 a randomized bridge
+differential test in the snapshot (valid / corrupted / wrong-message),
-(12 rounds, corruption across the whole signature, wrong-key and wrong-context
+re-run green after every source patch.
 cases) plus NIST ACVP 128s known-answer tests — re-run green after every
 source patch.
 - **`fips205.fors_inner_loop_eq`** + **`fips205.fors_outer_loop_eq`**
  (Algorithm 17, FORS pk-from-sig): a nested loop, split into two theorems.
@ -318,12 +305,7 @@ one — appears in its cone.
 ## Discipline
 Every Lean compile in this repository runs under `verification/lean-guard`
-(memory-capped, machine-wide serialized). It is Linux-oriented but **degrades
+(memory-capped, machine-wide serialized). Extraction is reproducible: the
 gracefully**: when `systemd-run` is unavailable it falls back to Lean's own
 `-M` cap, so the button runs on a stock Linux box without cgroup support — an
 external reviewer has run it green that way. Note also that the *empirical
 bridge* (`cargo test` in the snapshot repo) needs no Lean toolchain at all and
 runs on stable Rust. Extraction is reproducible: the
 full pin set (source commit, Charon/Aeneas commits + toolchain channel, Lean
 and OCaml versions) is in [verification/PROVENANCE.json](verification/PROVENANCE.json);
 `verification/extract.sh` refuses to run against a wrong-commit or dirty
--- a/TRUSTED-BASE.md
+++ b/TRUSTED-BASE.md
@ -31,7 +31,7 @@ proceeds and is part of every claim.
 7. **Aeneas-compat + de-plumbing patch surface.** The fn-pointer-to-named-
   oracle rewrite in `fips205-source` (phase 1) and the two de-plumbing
   rounds (index-loop rewrites of the iterator adapters on the verify path,
-   de-plumbing round 2 at `bea1051`; current snapshot head `3153988`) are
+   de-plumbing round 2 at `bea1051`; current snapshot head `797b4ef`) are
   part of the verified surface: the
   certificates cover the *patched* verify path, and the patch commits are
   the auditable delta from upstream `30bac08`. Each rewrite's equivalence
@ -42,42 +42,9 @@ proceeds and is part of every claim.
   has no certificate; a defect there could change the recomputed root while
   all eleven theorems still hold.
 9. **The deployed generic verifier.** The proved subject is the private
-   `verify_mono` facade. The bridge to upstream's generic `pk.verify()` is a
+   `verify_mono` facade. The bridge to upstream's generic `pk.verify()` is
-   finite differential test, **not** a machine-checked refinement — no theorem
+   the finite in-snapshot differential test, not a machine-checked
-   here says the two agree; the evidence is empirical and its size is stated so
+   refinement.
   a reader can judge it (external review, rounds 4–6, correctly objected that
   "finite" without a number is not a disclosure):
   - **137 evaluated input/verdict cases on the proved path** (was 9 until
     2026-07-28: three rounds from one fixed seed, corrupting one fixed byte of a
     7856-byte signature). The breakdown, which a reviewer can recount from
     `src/verify_mono.rs`:
     | source | cases |
     |---|---:|
     | retained original differential test (3 rounds × valid/corrupt/wrong-message) | 9 |
     | randomized differential bridge (12 rounds × valid + 6 corruptions + wrong-key + wrong-context) | 108 |
     | NIST ACVP `internal` group — M′ fed straight into `slh_verify_128s` | 10 |
     | NIST ACVP `external pure` group — mono vs deployed vs NIST | 10 |
     | **total** | **137** |
   - **20 of those are NIST known-answer tests against the proved path** (the
     two NIST rows above). NIST's negatives sit at structurally distinct sites —
     modified R, SIGFORS, SIGHT, modified message — rather than one arbitrary
     byte. The external-pure ten carry real contexts, 9 of them non-empty and one
     at the FIPS-205 maximum length of 255, which is the only empirical check of
     the domain-separator byte and context-length prefix that item 10 declares
     outside every proof.
   - **127 of the 137 compare mono against the deployed verifier** (all but the
     ten `internal` NIST cases, which compare mono against NIST directly).
   - Separately and **not** counted in the 137: **3 deployed-only prehash cases**
     (NIST `external preHash`), which exercise `hash_verify` rather than the
     proved path. Only two SHA2-512 vectors and one SHAKE-256 vector are
     executable — NIST's remaining prehash vectors use functions this crate does
     not implement — so this is *not* NIST coverage of all four supported prehash
     variants.
   - Corruption in the randomized bridge covers **72 distinct positions in the
     range 11..=7779**, not literally every byte of the signature.
   Still **not** covered by any of it: agreement on inputs nobody generated, and
   the prehash variant against the mono path (see item 10). A passing
   differential test is evidence, not a proof.
 10. **Everything above the extraction root.** The root is
    `verify_mono::slh_verify_128s = slh_verify_internal_free(M′, sig, pk)`,
    which takes the message-digest input **M′ as an argument**. The code in
@ -102,27 +69,7 @@ proceeds and is part of every claim.
    (`PROVENANCE.json → harness_integrity_sha256`); it is kept rather than
    removed because it is the memory cap and machine-wide lock that protect the
    build machine (a Lean elaboration once reached 12.2 GB and took the host
-    down).
+    down). Still trusted, and NOT bound by anything the button can check:
    **`verification/Proofs/Audit.lean` is pinned the same way, and for a sharper
    reason** (round-6 NEW-7): the digest it emits binds the audit's *data* — the
    policy constants, the statements, the specification bodies — but nothing can
    make a program hash the correctness of its own logic. Flipping this file's
    two fail-closed guards to `unless true` disabled every in-Lean check while
    the digest stayed BYTE-IDENTICAL, and a repository proving `False` passed
    ALL GREEN. The byte pin converts that from a silent green into a build
    failure; a legitimate change to the audit is now a reviewable pin rotation.
    Note the residue honestly: an author who edits the logic *and* rotates its
    pin in the same commit is not stopped by anything mechanical — that case is
    caught only by reading the diff at the pin.
    **`PROVENANCE.json` is itself load-bearing and unpinned.** It supplies the
    values for every byte pin, and round-7 review demonstrated that deleting one
    key from it silently removed both harness pins with no diagnostic, after
    which the logic mutation above ran to ALL GREEN. The *policy* — which files
    must be pinned — now lives hardcoded in `check.sh` and a missing entry is a
    build failure, so the map can no longer be quietly shortened; but the map's
    own bytes are still not pinned by anything, and could not be without moving
    the root of trust somewhere else.
    Still trusted, and NOT bound by anything the button can check:
    `check.sh` itself, `~/aeneas-toolchain/env.sh`, the `$AENEAS_HOME` tree
    (i.e. *which* Aeneas/Lean library the proofs are checked against), `python3`,
    and the Lean toolchain. An audit executed by a harness cannot defend against
--- a/verification/AUDIT-MANIFEST.txt
+++ b/verification/AUDIT-MANIFEST.txt
--- a/verification/PROVENANCE.json
+++ b/verification/PROVENANCE.json
@ -1,11 +1,11 @@
 {
-  "_comment": "Single machine-readable pin set to reproduce the extracted Lean model in gen/SlhVerify from source. External review rounds 2-5 (2026-07-24 .. 2026-07-27). Running verification/extract.sh against the pinned source tree with the pinned Charon/Aeneas toolchain reproduces the two aeneas-generated files byte-identically (generated_artifacts_sha256 below). The *External*.lean files are hand-maintained (not regenerated) and are NOT part of that reproducibility claim \u2014 but they ARE byte-pinned for integrity in model_integrity_sha256, since they carry the five oracle axioms and the discharged Step definitions. NOTE: SlhVerify.llbc is an intermediate artifact and is .gitignored, so its hash here can only be checked by a party who re-runs extract.sh.",
+  "_comment": "Single machine-readable pin set to reproduce the extracted Lean model in gen/SlhVerify from source. External review rounds 2-5 (2026-07-24 .. 2026-07-27). Running verification/extract.sh against the pinned source tree with the pinned Charon/Aeneas toolchain reproduces the two aeneas-generated files byte-identically (generated_artifacts_sha256 below). The *External*.lean files are hand-maintained (not regenerated) and are NOT part of that reproducibility claim — but they ARE byte-pinned for integrity in model_integrity_sha256, since they carry the five oracle axioms and the discharged Step definitions. NOTE: SlhVerify.llbc is an intermediate artifact and is .gitignored, so its hash here can only be checked by a party who re-runs extract.sh.",
  "parameter_set": "SLH-DSA-SHA2-128s",
  "source": {
    "repo": "github.com/saymrwulf/fips205-source",
-    "head": "a3ce8e8644fe302019ed7ae271912333f1476de4",
+    "head": "797b4ef26338e27363683656f93cb065a77daa0e",
    "upstream_base": "integritychain/fips205 @ 30bac08580aa61f653e5436d1bbacb5ffac446c4",
-    "upstream_deviation": "verbatim import minus CI workflows; then the additive monomorphic verify_mono compat module + de-plumbing rounds 1-2, each an individually-justified commit; then NIST ACVP SHA2-128s sigVer vectors + an expanded differential bridge (TEST-ONLY: no verify-path function changed, and re-running extract.sh against this commit reproduces the TWO Aeneas-generated model files (Types.lean, Funs.lean) byte-identically; the two *External.lean files are hand-maintained and are NOT regenerated by extraction \u2014 they are separately byte-pinned in model_integrity_sha256 and were unchanged by this commit)",
+    "upstream_deviation": "verbatim import minus CI workflows; then the additive monomorphic verify_mono compat module + de-plumbing rounds 1-2, each an individually-justified commit",
    "cargo_lock": "committed",
    "rust_toolchain_toml": "nightly-2026-06-01"
  },
@ -36,21 +36,17 @@
    "gen/SlhVerify/TypesExternal.lean",
    "gen/SlhVerify/FunsExternal.lean"
  ],
-  "byte_identical_regeneration_verified": "2026-07-28 \u2014 scope stated precisely (round-7 review): extraction regenerates Types.lean and Funs.lean only, and both were byte-identical across the source rotation 797b4ef->3153988. The hand-maintained TypesExternal.lean/FunsExternal.lean are byte-PINNED, not regenerated; claiming extraction 'reproduces all four' was self-contradictory against this file's own _comment.",
+  "byte_identical_regeneration_verified": "2026-07-24",
  "model_integrity_sha256": {
    "_comment": "All four Lean model files check.sh Phase 0 pins before compiling anything \u2014 the two aeneas-generated files AND the two hand-maintained *External files (which carry the five oracle axioms and the Step defs). A hand-edit of the model fails the build here (round-4 reviewer F3).",
-    "gen/SlhVerify/TypesExternal.lean": "2988c04c5fc8c634aff4d9bd13604b8a47e677daa1f45e8f4f321368606cdd0a",
+    "gen/SlhVerify/TypesExternal.lean": "37958beb7c90b649497a20b0802f98f0fb2d975c245eca956d7396af74d7759f",
    "gen/SlhVerify/FunsExternal.lean": "5efe551c35969c9da28b2f3eaed4a6a67c410c62a1926aab390e3abf010390f8",
    "gen/SlhVerify/Types.lean": "db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384",
    "gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f"
  },
  "harness_integrity_sha256": {
-    "_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.",
+    "_comment": "The compiler harness is part of the trusted computing base: check.sh shells out to lean-guard for every compile, and round-5 review demonstrated that stubbing it alone yields ALL GREEN in 3.6s over destroyed proofs. lean-guard is KEPT (it is the memory cap and machine-wide lock that protect this machine after the 12.2GB OOM incident) and sha256-pinned by Phase 0. NOT covered, and disclosed as trusted in TRUSTED-BASE.md item 11: check.sh itself, ~/aeneas-toolchain/env.sh, $AENEAS_HOME, python3, and the Lean toolchain.",
-    "lean-guard": "690d861cfd81b327604ffd5ef85599ee01b2bcd943907f5b71b8b6f99bad418f",
+    "lean-guard": "690d861cfd81b327604ffd5ef85599ee01b2bcd943907f5b71b8b6f99bad418f"
    "Proofs/Audit.lean": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e",
    "check-selftest.sh": "c6811482e25ae6e1fffa6ca50e60541e8e609a70c951db6bec4d2d39a4849e9a",
    "drill.sh": "915cf9310fa168c14ca5d76a1b84fd3b19acdfef9dfd0b03b01b19883548719e",
    "extract.sh": "01cff43c350ed8eaac0e65ccd7599b68fef47c9434cdb5ad01c92d2127a3bbe9"
  },
  "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."
 }
--- a/verification/RECORDED-RUN.md
+++ b/verification/RECORDED-RUN.md
@ -277,255 +277,3 @@ a stubbed harness, and stray modules.
 Note: the `_f: command not found` line in the selftest transcript above is a
 cosmetic shell-quoting bug in the script's own success message (backticks inside
 a double-quoted echo), fixed in this same commit. It did not affect any gate.
 ## Round-6 hardening — author-agent run, 20260728T072212Z, proof repo @ (this commit)
 Captured with `tee` from the real commands. Not independently executed.
 PIN ROTATIONS IN THIS COMMIT (stated explicitly — round-6 NEW-11):
  · harness_integrity_sha256 GAINS Proofs/Audit.lean (6108b97d…) — new pin, NEW-7.
  · no model pin rotated; gen/ bytes unchanged.
 ### check.sh
 ```
 fips205-slhdsa-verified — check
 ===============================
 === Phase 0: build hygiene + model/harness integrity ===
  ✓ Proofs/Audit.lean
  ✓ 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 (16 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)
 ✓ check 15 passed (the hashed block carries all 12 reference-fold bodies,
  including the recursive _f companions and their extracted-primitive calls)
 SELFTEST GREEN: 16 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, and stray modules.
 ```
 ## Round-7 fixes — author-agent run, 20260728T110335Z, proof repo @ (this commit)
 Captured with `tee`. NOT independently executed — but note that the third
 reviewer DID independently run check.sh and check-selftest.sh to green at
 dce0473 and 1e50295 on its own hardware and toolchain build, and recomputed
 the audit digest outside check.sh. What remains author-attested-only is
 extract.sh's byte-identical regeneration, which no reviewer has observed.
 PIN ROTATIONS: source 3153988 -> c945821 (test/vector only; all four model
 files verified byte-identical across it). No model or harness pin rotated.
 NOTE (round-7 NEW-16): the entire empirical bridge runs on STABLE Rust —
 no Charon, Aeneas, OCaml or pinned nightly required. The nightly pin exists
 only to align `charon cargo`. A third party can reproduce all 137 bridge
 cases with cargo alone.
 ### check.sh
 ```
 fips205-slhdsa-verified — check
 ===============================
 === Phase 0: build hygiene + model/harness integrity ===
  ✓ Proofs/Audit.lean
  ✓ 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
 ```
 ### cargo test on STABLE rust (rustc 1.95)
 ```
 running 6 tests
 deployed vs NIST ACVP 128s (prehash): 3 executed, 4 wrong-length, 7 skipped (hash function not implemented by this crate)
 test verify_mono::tests::deployed_matches_nist_acvp_128s_prehash ... ok
 mono vs NIST ACVP 128s (internal): 10 executed against the PROVED path, 4 rejected at deserialization (above the extraction root)
 test verify_mono::tests::mono_matches_nist_acvp_128s_internal ... ok
 mono+deployed vs NIST ACVP 128s (external pure): 10 executed (9 with a NON-EMPTY context), 4 rejected at deserialization
 test verify_mono::tests::mono_matches_nist_acvp_128s_external_pure ... ok
 test verify_mono::tests::mono_matches_deployed_verify ... ok
 test slh_dsa_sha2_128s::tests::simple_round_trips ... ok
 randomized differential bridge: 108 assertion points
 test verify_mono::tests::mono_matches_deployed_randomized ... ok
 test result: ok. 6 passed; 0 failed; 0 ignored; 0 measured; 0 filtered out; finished in 25.59s
 ```
 ### 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.
 ```
 ## 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.
 ```
--- a/verification/check-selftest.sh
+++ b/verification/check-selftest.sh
@ -20,14 +20,6 @@
 #      previously ALL GREEN in 3.6s over destroyed proofs)
 #  14  a stray .lean beside check.sh                         (round-5 NEW-4:
 #      LEAN_PATH includes $PWD, so it can join the environment ungated)
 #  16  an ORPHAN .olean whose source was deleted             (round-6 NEW-8:
 #      fell between the purge and the stray check; ALL GREEN, digest identical)
 #  17  the audit's fail-closed guards switched off           (round-6 NEW-7:
 #      the digest binds the audit's DATA, never its LOGIC; two characters in
 #      Audit.lean defeated every gate with the digest BYTE-IDENTICAL)
 #  18  the pin map shortened by one JSON key                 (round-7 NEW-13:
 #      deleting harness_integrity_sha256 silently un-pinned BOTH lean-guard and
 #      Audit.lean with no diagnostic, re-opening 17 with the digest identical)
 #
 # Self-cleaning: every mutated file is backed up and restored, and an EXIT trap
 # restores even on failure. Run from a clean tree.
@ -36,38 +28,13 @@ 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" "$SFBAK/$(printf %s "$1" | tr / _)"; BAKS+=("$1"); }
+save()    { cp -p "$1" "$1.sfbak"; BAKS+=("$1"); }
-restore() { for f in "${BAKS[@]:-}"; do
+restore() { for f in "${BAKS[@]:-}"; do [ -f "$f.sfbak" ] && mv -f "$f.sfbak" "$f"; done; BAKS=(); }
              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 —
 # the "rejected for an unrelated reason" defect class. `repin_audit` simulates an
 # author who edits and dutifully re-pins; the digest/enumeration must still bite.
 # Attack 17 deliberately does NOT re-pin: it is the test of the pin itself.
 repin_audit() {
  python3 - <<'PY'
 import json, hashlib
 p = "PROVENANCE.json"; d = json.load(open(p))
 d["harness_integrity_sha256"]["Proofs/Audit.lean"] = hashlib.sha256(
    open("Proofs/Audit.lean","rb").read()).hexdigest()
 json.dump(d, open(p,"w"), indent=2); open(p,"a").write("\n")
 PY
 }
 cleanup() {
  restore
-  rm -rf "$SFBAK" 2>/dev/null
+  rm -f Proofs/Stray.lean Proofs/EvilSpec.lean Evil.lean \
-  rm -f Proofs/Stray.lean Proofs/EvilSpec.lean Evil.lean Evil.olean \
+        Proofs/*.olean gen/SlhVerify/*.olean .audit-manifest.observed 2>/dev/null
        Proofs/*.olean gen/SlhVerify/*.olean *.olean .audit-manifest.observed 2>/dev/null
  return 0
 }
 trap cleanup EXIT
@ -85,7 +52,7 @@ rm -f Proofs/Stray.lean
 echo "✓ attack 1 rejected (dead-file gate)"
 # ── 2: smuggled disallowed axiom in a real cone ─────────────────────────────
-save check.sh; save Proofs/Audit.lean; save PROVENANCE.json
+save check.sh; save Proofs/Audit.lean
 # NB: no imports — Phase 0 now purges every .olean, so a module injected at the
 # head of the build order cannot import one that has not been compiled yet.
 cat > Proofs/EvilSpec.lean <<'EOF'
@ -102,14 +69,13 @@ a = a.replace('import Proofs.ApexSpec', 'import Proofs.ApexSpec\nimport Proofs.E
 a = a.replace('  [ (`fips205.chain_free_loop_eq', '  [ (`evil_thm, kernel3, 0),\n    (`fips205.chain_free_loop_eq', 1)
 open("Proofs/Audit.lean","w").write(a)
 PY
 repin_audit
 ./check.sh > /tmp/sf2.out 2>&1 && fail "ATTACK 2 SUCCEEDED (smuggled axiom)" /tmp/sf2.out
 grep -q "evil_ax" /tmp/sf2.out || fail "ATTACK 2: rejected but evil_ax not named" /tmp/sf2.out
 restore; rm -f Proofs/EvilSpec.lean
 echo "✓ attack 2 rejected (extra-axiom detection — evil_ax named)"
 # ── 3: dropped oracle (a subset check would pass; exact must not) ────────────
-save Proofs/Audit.lean; save PROVENANCE.json
+save Proofs/Audit.lean
 python3 - <<'PY'
 import re
 a = open("Proofs/Audit.lean").read()
@ -117,20 +83,18 @@ new, n = re.subn(r'(`fips205\.to_int_loop_eq,\s*)kernel3,', r'\1kernel3 ++ [orac
 assert n == 1, f"expected 1 to_int row, patched {n}"
 open("Proofs/Audit.lean","w").write(new)
 PY
 repin_audit
 ./check.sh > /tmp/sf3.out 2>&1 && fail "ATTACK 3 SUCCEEDED (dropped oracle — subset hole)" /tmp/sf3.out
 grep -q "missing=\[verify_mono.oracle.f\]" /tmp/sf3.out || fail "ATTACK 3: rejected but missing oracle not named" /tmp/sf3.out
 restore
 echo "✓ attack 3 rejected (missing-oracle detection — exact cone, not subset)"
 # ── 4: vanished certificate ─────────────────────────────────────────────────
-save Proofs/Audit.lean; save PROVENANCE.json
+save Proofs/Audit.lean
 python3 - <<'PY'
 a = open("Proofs/Audit.lean").read()
 assert a.count('`fips205.chain_free_loop_eq,') >= 1
 open("Proofs/Audit.lean","w").write(a.replace('`fips205.chain_free_loop_eq,', '`fips205.chain_free_loop_eq_VANISHED,', 1))
 PY
 repin_audit
 ./check.sh > /tmp/sf4.out 2>&1 && fail "ATTACK 4 SUCCEEDED (vanished cert)" /tmp/sf4.out
 grep -q "NOT FOUND" /tmp/sf4.out || fail "ATTACK 4: rejected but not via the existence check" /tmp/sf4.out
 restore
@ -167,7 +131,7 @@ restore
 echo "✓ attack 7 rejected (Phase 0 model-byte integrity)"
 # ── 8: deleted manifest row (round-4 F1, set half) ──────────────────────────
-save Proofs/Audit.lean; save PROVENANCE.json
+save Proofs/Audit.lean
 python3 - <<'PY'
 import re
 a = open("Proofs/Audit.lean").read()
@ -175,7 +139,6 @@ new, n = re.subn(r'\n\s*\(`fips205\.to_int_loop_eq,.*?\),', '', a)
 assert n == 1, f"expected 1 row, removed {n}"
 open("Proofs/Audit.lean","w").write(new)
 PY
 repin_audit
 ./check.sh > /tmp/sf8.out 2>&1 && fail "ATTACK 8 SUCCEEDED (a dropped cert row passed)" /tmp/sf8.out
 grep -q "digest mismatch" /tmp/sf8.out || fail "ATTACK 8: rejected but not via the digest binding" /tmp/sf8.out
 restore
@ -189,14 +152,13 @@ echo "✓ attack 8 rejected (audit-manifest digest — a silently-dropped cert c
 # (which now also rejects a bare `axiom` in an audited module) cannot fire and
 # the DIGEST must be what bites. `sorryAx` is used as the smuggled name because
 # admitting it would silently legalise every `sorry` in the repository.
-save Proofs/Audit.lean; save PROVENANCE.json
+save Proofs/Audit.lean
 python3 - <<'PY'
 a = open("Proofs/Audit.lean").read()
 old = "  kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg]\n"
 assert a.count(old) == 1, "allowedBoundary shape changed"
 open("Proofs/Audit.lean","w").write(a.replace(old, old.rstrip("\n") + " ++ [`sorryAx]\n", 1))
 PY
 repin_audit
 ./check.sh > /tmp/sf9.out 2>&1 && fail "ATTACK 9 SUCCEEDED: the axiom policy was widened and the button stayed GREEN!" /tmp/sf9.out
 grep -q "digest mismatch" /tmp/sf9.out || fail "ATTACK 9: rejected but not via the policy-covering digest" /tmp/sf9.out
 restore
@ -241,14 +203,13 @@ restore
 echo "✓ attack 11 rejected (enumeration covers every declaration kind, not just theorems)"
 # ── 12: a False-proof inside the AUDITOR itself (round-5 R1) ────────────────
-save Proofs/Audit.lean; save PROVENANCE.json
+save Proofs/Audit.lean
 python3 - <<'PY'
 a = open("Proofs/Audit.lean").read()
 i = a.index("elab \"auditCones\"")
 open("Proofs/Audit.lean","w").write(
    a[:i] + "axiom cheat12 : ∀ (P : Prop), P\ntheorem audit_proves_false : False := cheat12 _\n\n" + a[i:])
 PY
 repin_audit
 ./check.sh > /tmp/sf12.out 2>&1 && fail "ATTACK 12 SUCCEEDED: the auditor itself proves False, still GREEN!" /tmp/sf12.out
 grep -qE "audit_proves_false|AXIOM DECLARED" /tmp/sf12.out || fail "ATTACK 12: rejected but not via self-enumeration" /tmp/sf12.out
 restore
@ -279,88 +240,6 @@ grep -q "BUILD HYGIENE FAILED" /tmp/sf14.out || fail "ATTACK 14: rejected but no
 rm -f Evil.lean
 echo "✓ attack 14 rejected (no .lean may sit outside gen/ and Proofs/)"
 # ── 16: ORPHAN .olean WITH NO SOURCE (round-6 NEW-8) ───────────────────────
 # Previously ALL GREEN, digest byte-identical, repo proving False: the round-5
 # purge covered gen/ and Proofs/ while the stray check greped only *.lean, so a
 # compiled module with its source DELETED fell between the two — and *.olean is
 # .gitignored, so `git status` showed only the one-line import.
 save Proofs/ChainSpec.lean
 cat > Evil.lean <<'EOF'
 axiom cheat16 : ∀ (P : Prop), P
 theorem attack16_false : False := cheat16 _
 EOF
 ( cd "$AENEAS_HOME/backends/lean" && lake env bash -c \
    "cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\" && lean -o '$HERE/Evil.olean' '$HERE/Evil.lean'" ) >/dev/null 2>&1
 rm -f Evil.lean                       # the SOURCE is gone; only the .olean remains
 printf '\nimport Evil\n' >> Proofs/ChainSpec.lean
 if [ ! -f Evil.olean ]; then
  # An attack that could not be staged must FAIL the suite, never pass quietly:
  # round-7 review found this branch printed a note and fell through to the
  # unconditional "16 attacks rejected" line, so the suite could claim a
  # rejection that never happened.
  rm -f Evil.olean
  fail "ATTACK 16 could not be staged (Evil.olean did not build) — the suite must not report green on an attack it did not run"
 else
  ./check.sh > /tmp/sf16.out 2>&1 && fail "ATTACK 16 SUCCEEDED: an orphan .olean injected False and stayed GREEN!" /tmp/sf16.out
  # The defense is Phase 0's purge, which now covers ALL of verification/ and so
  # deletes the orphan BEFORE the stray check ever sees it; `import Evil` then has
  # nothing to resolve and Phase 2 fails closed. Assert that chain precisely —
  # the rejection must be the import failure AND the .olean must be gone. (An
  # earlier revision asserted the hygiene message and failed while the gate was
  # working correctly: the same wrong-diagnostic defect this suite exists to catch.)
  grep -q "FAIL: Proofs/ChainSpec" /tmp/sf16.out \
    || fail "ATTACK 16: rejected, but not by the purge+import chain" /tmp/sf16.out
  [ ! -f Evil.olean ] \
    || fail "ATTACK 16: check.sh failed but the orphan .olean survived Phase 0" /tmp/sf16.out
  echo "✓ attack 16 rejected (Phase 0 purges every .olean under verification/, so an"
  echo "  orphan compiled module with no source cannot satisfy an import)"
 fi
 restore; rm -f Evil.olean Evil.lean
 # ── 17: TAMPER THE AUDIT'S LOGIC, NOT ITS DATA (round-6 NEW-7) ─────────────
 # Switching the two fail-closed guards to `unless true` disables every in-Lean
 # check while leaving the digest BYTE-IDENTICAL — the digest binds the audit's
 # data, never the code that reads it. Note this attack does NOT re-pin
 # Audit.lean: the sha256 pin is the only thing standing here, and that is
 # exactly what is being tested.
 save Proofs/Audit.lean; save Proofs/ChainSpec.lean
 python3 - <<'PY'
 a = open("Proofs/Audit.lean").read()
 n = a.count("  unless errs.isEmpty do")
 assert n >= 1, "Audit.lean fail-closed guard shape changed"
 open("Proofs/Audit.lean","w").write(a.replace("  unless errs.isEmpty do", "  unless true do"))
 PY
 printf '\n-- SELFTEST ATTACK 17\naxiom cheat17 : ∀ (P : Prop), P\ntheorem attack17_false : False := cheat17 _\n' >> Proofs/ChainSpec.lean
 ./check.sh > /tmp/sf17.out 2>&1 && fail "ATTACK 17 SUCCEEDED: the audit's guards were disabled and it stayed GREEN!" /tmp/sf17.out
 grep -q "INTEGRITY FAILED" /tmp/sf17.out || fail "ATTACK 17: rejected but not via the Audit.lean harness pin" /tmp/sf17.out
 restore
 echo "✓ attack 17 rejected (Phase 0 pins Audit.lean — its LOGIC cannot be silently switched off)"
 # ── 18: SHORTEN THE PIN MAP (round-7 NEW-13) ───────────────────────────────
 # Previously ALL GREEN: PROVENANCE.json is a tracked file that nothing pins, and
 # the only completeness test was "is the map non-empty", so deleting the whole
 # harness_integrity_sha256 key silently un-pinned BOTH lean-guard and
 # Proofs/Audit.lean with no diagnostic — after which the attack-17 logic
 # mutation ran green over a repository proving False, digest byte-identical.
 # The required pin NAMES now live hardcoded in check.sh (the root of trust),
 # so a shortened map is a build failure.
 save PROVENANCE.json
 python3 - <<'PY'
 import json
 p = "PROVENANCE.json"; d = json.load(open(p))
 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
 # The diagnostic is "UNPINNED harness file" since round 8, when the required set
 # 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)"
 # ── 15: COVERAGE OF THE DIGEST INPUT (direct, not an attack) ───────────────
 # Attack 9 proves the digest binding fires. This proves WHAT it covers: the
 # hashed block must literally contain each reference fold's definition BODY, so
@ -391,8 +270,8 @@ echo "✓ check 15 passed (the hashed block carries all 12 reference-fold bodies
 echo '  including the recursive _f companions and their extracted-primitive calls)'
 echo
-echo "SELFTEST GREEN: 17 attacks rejected + digest-coverage check — dead files, extra axioms, dropped"
+echo "SELFTEST GREEN: 14 attacks rejected + digest-coverage check — dead files, extra axioms, dropped"
 echo "oracles, vanished certs, un-manifested False theorems AND defs, gutted"
 echo "statements, hand-edited models, dropped manifest rows, widened policy,"
 echo "specification folds redefined to the loop, a False-proof in the auditor,"
-echo "a stubbed harness, stray modules, and a shortened pin map."
+echo "a stubbed harness, and stray modules."
--- a/verification/check.sh
+++ b/verification/check.sh
@ -50,32 +50,24 @@ echo "==============================="
 # ── Phase 0: build hygiene + model & harness integrity ───────────────────────
 echo "=== Phase 0: build hygiene + model/harness integrity ==="
-# (a) Purge EVERY .olean under verification/ — round-6 NEW-8: the round-5 purge
+# (a) Purge every .olean first. Round-5 NEW-4: the button's verdict must depend
-#     covered only gen/ and Proofs/ while the stray check greped only *.lean, so
+#     on COMMITTED BYTES, never on untracked build state — a stale .olean from a
-#     an ORPHAN `verification/Evil.olean` WITH NO SOURCE AT ALL fell between them,
+#     module that no longer exists (and *.olean is .gitignored, so invisible to
-#     satisfied an `import Evil`, and went ALL GREEN with the digest untouched
+#     `git status`) could otherwise satisfy an import and go green.
-#     (*.olean is .gitignored, so `git status` showed only the import line).
+find "$HERE/gen" "$HERE/Proofs" -name '*.olean' -delete 2>/dev/null || true
-#     The verdict must depend on COMMITTED BYTES, never on untracked build state.
+# (b) No Lean source may sit outside gen/ and Proofs/. LEAN_PATH includes $PWD,
-find "$HERE" -name '*.olean' -delete 2>/dev/null || true
+#     so a stray verification/*.lean can join the environment ungated (NEW-4).
-#     Aeneas also emits `*_Template.lean` scaffolding into gen/ on every
+STRAY=$(find "$HERE" -maxdepth 1 -name '*.lean' -printf '%f\n' 2>/dev/null || true)
 #     extraction. Those files are UNTRACKED byproducts (a fresh clone has only
 #     the four pinned model files), nothing imports them, and they would
 #     otherwise sit on LEAN_PATH unpinned — the same untracked-state problem.
 #     Remove them here so the gen/ file-set assertion below can be exact.
 find "$HERE/gen" -name '*_Template.lean' -delete 2>/dev/null || true
 # (b) No Lean source OR compiled module may sit outside gen/ and Proofs/;
 #     LEAN_PATH includes $PWD, so either can join the environment ungated.
 STRAY=$(find "$HERE" -maxdepth 1 \( -name '*.lean' -o -name '*.olean' \) -printf '%f\n' 2>/dev/null || true)
 if [ -n "$STRAY" ]; then
-  echo "$STRAY" | sed 's/^/  ✗ stray Lean file outside gen\/ and Proofs\/: /'
+  echo "$STRAY" | sed 's/^/  ✗ stray Lean source outside gen\/ and Proofs\/: /'
-  echo "BUILD HYGIENE FAILED (a .lean/.olean outside the audited directories can join LEAN_PATH)"; exit 1
+  echo "BUILD HYGIENE FAILED (a .lean outside the audited directories can join LEAN_PATH)"; exit 1
 fi
 # (c) sha256-pin the extracted model AND the compiler harness. lean-guard is
 #     repo-tracked and is shelled out to for every compile, so it is part of the
 #     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, or a required file is unpinned — see the specific line above)"; exit 1; }
+python3 - "$HERE/PROVENANCE.json" "$HERE" <<'PY' || { echo "INTEGRITY FAILED (a pinned file differs from PROVENANCE.json — hand-edited model or harness?)"; 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("_")}
@ -83,37 +75,6 @@ files.update({k: v for k, v in prov.get("harness_integrity_sha256", {}).items()
 if not files:
    print("  no integrity map in PROVENANCE.json (fail-closed)"); sys.exit(1)
 bad = 0
 # WHICH files must be pinned is policy, and policy belongs in the root of trust —
 # not in the map being consulted. Round-6 review (NEW-13) demonstrated the gap:
 # PROVENANCE.json is a tracked file that nothing pins, and the only completeness
 # test was `if not files`, so deleting the whole `harness_integrity_sha256` key
 # silently un-pinned BOTH lean-guard and Proofs/Audit.lean with no diagnostic —
 # after which the round-6 NEW-7 logic mutation ran to ALL GREEN over a repository
 # 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.
 # SELF-DERIVING, so a NEW harness file cannot be forgotten. Round-8 review
 # observed that a hardcoded list is itself a second thing to keep in sync, and
 # supplied the natural boundary the harness does have: THE EXECUTABLE BIT. Every
 # 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"
 }
 harness.add("Proofs/Audit.lean")
 missing = harness - set(files)
 if missing:
    for m in sorted(missing):
        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)
    if not os.path.exists(p):
@ -123,20 +84,6 @@ for rel, want in sorted(files.items()):
        print(f"  ✗ {rel}: sha256 {got[:12]} ≠ pinned {want[:12]}"); bad = 1
    else:
        print(f"  ✓ {rel}")
 # Round-6 NEW-9: pin gen/ as a SET, not as four names. A new file under gen/ was
 # neither hashed nor forbidden, while LEAN_PATH contains $PWD/gen — so the
 # closure's premise ("everything outside certModules is pinned or disclosed")
 # was not enforced. Any .lean under gen/ must appear in the pin map.
 pinned_gen = {k for k in files if k.startswith("gen/")}
 actual_gen = set()
 for root, _, names in os.walk(os.path.join(here, "gen")):
    for n in names:
        if n.endswith(".lean"):
            actual_gen.add(os.path.relpath(os.path.join(root, n), here))
 for extra in sorted(actual_gen - pinned_gen):
    print(f"  ✗ UNPINNED model file under gen/: {extra}"); bad = 1
 for missing in sorted(pinned_gen - actual_gen):
    print(f"  ✗ pinned model file absent: {missing}"); bad = 1
 sys.exit(1 if bad else 0)
 PY
@ -196,19 +143,10 @@ if [ "$GOT_SHA" != "$EXPECTED_AUDIT_SHA256" ]; then
  echo "  expected: $EXPECTED_AUDIT_SHA256"
  echo "  observed: $GOT_SHA"
  echo "  A policy constant, a certificate statement, or a specification"
-  echo "  definition changed without a reviewed rotation."
+  echo "  definition changed without a reviewed rotation. The observed block was"
-  echo "  What moved (committed block vs observed):"
+  echo "  written to verification/.audit-manifest.observed — diff it to see what."
  diff -u "$HERE/AUDIT-MANIFEST.txt" "$HERE/.audit-manifest.observed" 2>/dev/null \
    | head -40 | sed 's/^/    /' || echo "    (AUDIT-MANIFEST.txt absent — cannot diff)"
  exit 1
 fi
 # The digest's INPUT is committed too (round-6: a mismatch previously wrote an
 # observed block with nothing to diff it against). Guard against the committed
 # copy drifting from what Lean actually emits.
 if ! printf '%s\n' "$BLOCK" | cmp -s - "$HERE/AUDIT-MANIFEST.txt"; then
  echo "AUDIT FAILED — the committed AUDIT-MANIFEST.txt does not match the emitted block"
  echo "  (digest matched, so this means the committed copy is stale — refresh it)"; exit 1
 fi
 echo "  ✓ $(grep -oF 'exact-cone audit PASSED' <<<"$AUD_OUT" | head -1)"
 echo "  ✓ audit-manifest digest matches (sha256 ${EXPECTED_AUDIT_SHA256:0:16}…)"
--- a/verification/extract.sh
+++ b/verification/extract.sh
@ -33,7 +33,7 @@ CRATE="${1:-$HOME/GitClone/FormalVerification/sources/fips205-source}"
 # The pinned source commit this repo's model + proofs were verified against.
 # Keep in lockstep with verification/PROVENANCE.json and the README snapshot.
-EXPECTED_SRC_COMMIT="${EXPECTED_SRC_COMMIT:-a3ce8e8644fe302019ed7ae271912333f1476de4}"
+EXPECTED_SRC_COMMIT="${EXPECTED_SRC_COMMIT:-797b4ef26338e27363683656f93cb065a77daa0e}"
 # ── Provenance guard: refuse a wrong or dirty source tree (fail-closed) ──────
 [ -d "$CRATE/.git" ] || { echo "ERROR: '$CRATE' is not a git checkout of fips205-source." >&2; exit 2; }
--- a/verification/gen/SlhVerify/TypesExternal.lean
+++ b/verification/gen/SlhVerify/TypesExternal.lean
@ -1,16 +1,7 @@
 /- gen/SlhVerify/TypesExternal.lean — hand-maintained external types.
-
+   The single external type is a core-library error type introduced by
-   THIS FILE DECLARES NO TYPES, deliberately. It once carried a core-library
+   u32::try_from; it carries no cryptographic content. -/
-   error type introduced by `u32::try_from`; the de-plumbing patches removed
+-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
   that idiom from the verify path at source level, so the declaration was
   deleted under the dead-stub rule and only the module shell remains (Aeneas's
   split-file layout still expects the module to exist).
   An earlier header claimed the error type was still here, and the Aeneas
   "rename this template and fill the holes" boilerplate had never been removed;
   external review (round-6 NEW-12) flagged both. Corrected 2026-07-28. The file
   is hand-maintained (Aeneas does not regenerate it) and its bytes are
   sha256-pinned by check.sh Phase 0. -/
 import Aeneas
 open Aeneas Aeneas.Std Result ControlFlow Error
 set_option linter.dupNamespace false