saymrwulf/fips205-slhdsa-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/fips205-slhdsa-verified.git synced 2026-09-09 20:50:53 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: saymrwulf:dce0473013f232e4d0bd76b62cc6899b2ca3522a
Branches Tags
saymrwulf:main
...
compare: saymrwulf:0d680333e311d9350650b3432f7b4669a771d11f
Branches Tags
saymrwulf:main

6 commits
dce0473013 ... 0d680333e3

Author SHA1 Message Date
mrwulf
0d680333e3 re-pin source @ a3ce8e8 (extraction-script honesty fixes) and rotate extract.sh's harness pin 2026-07-28 14:42:46 +02:00
mrwulf
05c4412168 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>
 2026-07-28 14:40:39 +02:00
mrwulf
1bc4f39f35 round 7: assert pin-map completeness (NEW-13), correct the count to 137, fix the regeneration-scope contradiction 
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>
 2026-07-28 13:03:35 +02:00
mrwulf
1e50295619 TypesExternal: correct a header that described a type the file no longer contains 
Round-6 NEW-12: the header claimed 'the single external type is a core-library
error type introduced by u32::try_from', but de-plumbing deleted that
declaration and the file defines nothing at all; the Aeneas 'rename this
template and fill the holes' boilerplate had also never been removed. Both
corrected. Comment-only, so the audit digest is unchanged (d83e297a…); the
Phase-0 model pin rotates 37958beb -> 2988c04c.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-07-28 10:16:57 +02:00
mrwulf
476f669f5c bridge: re-pin to the NIST-ACVP source commit; state the real coverage numbers 
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>
 2026-07-28 09:46:29 +02:00
mrwulf
e6ffd16277 review round 6: pin the auditor, purge every olean, pin gen/ as a set 
Round 6 confirmed the digest redesign closed NEW-1/NEW-2/NEW-5 at the mechanism
("the first time in three rounds I have not been able to gut a certificate"),
then demonstrated two more ways to reach ALL GREEN with the committed digest
BYTE-IDENTICAL over a repository proving False. Both are fixed.

NEW-7 — the digest bound the audit's DATA, never its LOGIC. Flipping the two
fail-closed guards in Proofs/Audit.lean to `unless true` disabled every in-Lean
check; the block's inputs genuinely had not changed, so the digest still
matched. Total attacker diff: 2 files, 6 insertions. Worse, TRUSTED-BASE item 11
listed the trusted-unbound set and did NOT mention Audit.lean, so a reviewer
using it as a map of what to read by hand would have skipped the file that
computes the number it is judged by.
FIX: Proofs/Audit.lean is now sha256-pinned in harness_integrity_sha256,
symmetric with lean-guard, and item 11 says so — including the honest residue:
an author who edits the logic AND rotates its pin is caught only by reading the
diff at the pin.

NEW-8 — Phase 0's purge covered gen/ and Proofs/ while the stray check greped
only *.lean, so an ORPHAN verification/Evil.olean whose source had been DELETED
fell between them, satisfied an import, and was invisible to git status
(*.olean is gitignored).
FIX: purge every .olean under verification/, and forbid stray .lean AND .olean.

NEW-9 (partial) — gen/ was pinned by four NAMES, not as a SET, so a new file
there was neither hashed nor forbidden while LEAN_PATH contains $PWD/gen.
FIX: Phase 0 asserts the gen/*.lean file set equals the pin map exactly. This
found a real gap on its first run: Aeneas emits *_Template.lean scaffolding into
gen/ on every extraction — untracked byproducts (a fresh clone has only the four
pinned files) that nothing imports but that sat on LEAN_PATH unpinned. They are
now purged as byproducts before the set assertion.

Also, from the reviewer's §3 suggestion: the canonical block is now COMMITTED as
verification/AUDIT-MANIFEST.txt, so a digest mismatch prints a real diff instead
of writing an observed file with nothing to compare against; check.sh also fails
if the committed copy drifts from what Lean emits.

check-selftest.sh: 16 attacks, all rejected, plus the coverage check. Attacks 16
and 17 are the reviewer's two demonstrations. Attacks that mutate the audit's
DATA now re-pin Audit.lean first, so they still test the digest/enumeration
rather than being stopped by the byte pin; attack 17 deliberately does not
re-pin, because the pin is what it tests.

Housekeeping: PROVENANCE.json trailing newline restored (NEW-12).

Disclosed rather than buried: two more of my own assertion bugs this round —
attack 16 asserted the hygiene message when the correct rejection is the purge
plus a failed import, and the earlier gen/ set check surfaced the template files
only because it was written strictly. Both are the wrong-diagnostic class.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-07-28 09:22:12 +02:00
10 changed files with 725 additions and 48 deletions
Show stats Expand all files Collapse all files

105
ATTESTATION-BASIS.md Normal file
View file

@ -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.

30
README.md
View file

@ -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–5 applied)
## STATUS: eleven certificates over the extracted verify model (external review rounds 1–6 applied)
`verification/check.sh` is **green** (exit 0): the model compiles, the proofs
compile, and the audit passes. The audit runs **inside Lean**
@ -64,8 +64,19 @@ 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 the
finite in-snapshot **differential test**, not a machine-checked refinement.
`verify_mono` facade; the bridge to upstream's generic `pk.verify()` is a
finite **differential test**, not a machine-checked refinement. Its size is
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.
@ -156,8 +167,10 @@ 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 (valid / corrupted / wrong-message),
re-run green after every source patch.
differential test in the snapshot — since 2026-07-28 a randomized bridge
(12 rounds, corruption across the whole signature, wrong-key and wrong-context
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.
@ -305,7 +318,12 @@ one — appears in its cone.
## Discipline
Every Lean compile in this repository runs under `verification/lean-guard`
(memory-capped, machine-wide serialized). Extraction is reproducible: the
(memory-capped, machine-wide serialized). It is Linux-oriented but **degrades
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

63
TRUSTED-BASE.md
View file

@ -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 `797b4ef`) are
de-plumbing round 2 at `bea1051`; current snapshot head `3153988`) 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,9 +42,42 @@ 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
the finite in-snapshot differential test, not a machine-checked
refinement.
`verify_mono` facade. The bridge to upstream's generic `pk.verify()` is a
finite differential test, **not** a machine-checked refinement — no theorem
here says the two agree; the evidence is empirical and its size is stated so
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
@ -69,7 +102,27 @@ 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). Still trusted, and NOT bound by anything the button can check:
down).
**`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

53
verification/AUDIT-MANIFEST.txt Normal file
View file

File diff suppressed because one or more lines are too long

20
verification/PROVENANCE.json
View file

@ -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 — 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 \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.",
"parameter_set": "SLH-DSA-SHA2-128s",
"source": {
"repo": "github.com/saymrwulf/fips205-source",
"head": "797b4ef26338e27363683656f93cb065a77daa0e",
"head": "a3ce8e8644fe302019ed7ae271912333f1476de4",
"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",
"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)",
"cargo_lock": "committed",
"rust_toolchain_toml": "nightly-2026-06-01"
},
@ -36,17 +36,21 @@
"gen/SlhVerify/TypesExternal.lean",
"gen/SlhVerify/FunsExternal.lean"
],
"byte_identical_regeneration_verified": "2026-07-24",
"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.",
"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": "37958beb7c90b649497a20b0802f98f0fb2d975c245eca956d7396af74d7759f",
"gen/SlhVerify/TypesExternal.lean": "2988c04c5fc8c634aff4d9bd13604b8a47e677daa1f45e8f4f321368606cdd0a",
"gen/SlhVerify/FunsExternal.lean": "5efe551c35969c9da28b2f3eaed4a6a67c410c62a1926aab390e3abf010390f8",
"gen/SlhVerify/Types.lean": "db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384",
"gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f"
},
"harness_integrity_sha256": {
"_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"
"_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",
"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."
}
}

252
verification/RECORDED-RUN.md
View file

@ -277,3 +277,255 @@ 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.
```

145
verification/check-selftest.sh
View file

@ -20,6 +20,14 @@
# 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.
@ -28,13 +36,38 @@ 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"); }
restore() { for f in "${BAKS[@]:-}"; do [ -f "$f.sfbak" ] && mv -f "$f.sfbak" "$f"; done; BAKS=(); }
save() { cp -p "$1" "$SFBAK/$(printf %s "$1" | tr / _)"; BAKS+=("$1"); }
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 —
# 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 -f Proofs/Stray.lean Proofs/EvilSpec.lean Evil.lean \
Proofs/*.olean gen/SlhVerify/*.olean .audit-manifest.observed 2>/dev/null
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
}
trap cleanup EXIT
@ -52,7 +85,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 check.sh; save Proofs/Audit.lean; save PROVENANCE.json
# 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'
@ -69,13 +102,14 @@ 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 Proofs/Audit.lean; save PROVENANCE.json
python3 - <<'PY'
import re
a = open("Proofs/Audit.lean").read()
@ -83,18 +117,20 @@ 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 Proofs/Audit.lean; save PROVENANCE.json
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
@ -131,7 +167,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 Proofs/Audit.lean; save PROVENANCE.json
python3 - <<'PY'
import re
a = open("Proofs/Audit.lean").read()
@ -139,6 +175,7 @@ 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
@ -152,13 +189,14 @@ 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 Proofs/Audit.lean; save PROVENANCE.json
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
@ -203,13 +241,14 @@ 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 Proofs/Audit.lean; save PROVENANCE.json
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
@ -240,6 +279,88 @@ 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
@ -270,8 +391,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: 14 attacks rejected + digest-coverage check — dead files, extra axioms, dropped"
echo "SELFTEST GREEN: 17 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, and stray modules."
echo "a stubbed harness, stray modules, and a shortened pin map."

88
verification/check.sh
View file

@ -50,24 +50,32 @@ echo "==============================="
# ── Phase 0: build hygiene + model & harness integrity ───────────────────────
echo "=== Phase 0: build hygiene + model/harness integrity ==="
# (a) Purge every .olean first. Round-5 NEW-4: the button's verdict must depend
# on COMMITTED BYTES, never on untracked build state — a stale .olean from a
# module that no longer exists (and *.olean is .gitignored, so invisible to
# `git status`) could otherwise satisfy an import and go green.
find "$HERE/gen" "$HERE/Proofs" -name '*.olean' -delete 2>/dev/null || true
# (b) No Lean source may sit outside gen/ and Proofs/. LEAN_PATH includes $PWD,
# so a stray verification/*.lean can join the environment ungated (NEW-4).
STRAY=$(find "$HERE" -maxdepth 1 -name '*.lean' -printf '%f\n' 2>/dev/null || true)
# (a) Purge EVERY .olean under verification/ — round-6 NEW-8: the round-5 purge
# covered only gen/ and Proofs/ while the stray check greped only *.lean, so
# an ORPHAN `verification/Evil.olean` WITH NO SOURCE AT ALL fell between them,
# satisfied an `import Evil`, and went ALL GREEN with the digest untouched
# (*.olean is .gitignored, so `git status` showed only the import line).
# The verdict must depend on COMMITTED BYTES, never on untracked build state.
find "$HERE" -name '*.olean' -delete 2>/dev/null || true
# Aeneas also emits `*_Template.lean` scaffolding into gen/ on every
# 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 source outside gen\/ and Proofs\/: /'
echo "BUILD HYGIENE FAILED (a .lean outside the audited directories can join LEAN_PATH)"; exit 1
echo "$STRAY" | sed 's/^/ ✗ stray Lean file outside gen\/ and Proofs\/: /'
echo "BUILD HYGIENE FAILED (a .lean/.olean 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 — 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("_")}
@ -75,6 +83,37 @@ 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):
@ -84,6 +123,20 @@ 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
@ -143,10 +196,19 @@ 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. The observed block was"
echo " written to verification/.audit-manifest.observed — diff it to see what."
echo " definition changed without a reviewed rotation."
echo " What moved (committed block vs observed):"
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}…)"

2
verification/extract.sh
View file

@ -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:-797b4ef26338e27363683656f93cb065a77daa0e}"
EXPECTED_SRC_COMMIT="${EXPECTED_SRC_COMMIT:-a3ce8e8644fe302019ed7ae271912333f1476de4}"
# ── 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; }

15
verification/gen/SlhVerify/TypesExternal.lean
View file

@ -1,7 +1,16 @@
/- gen/SlhVerify/TypesExternal.lean — hand-maintained external types.
The single external type is a core-library error type introduced by
u32::try_from; it carries no cryptographic content. -/
-- This is a template file: rename it to "TypesExternal.lean" and fill the holes.
THIS FILE DECLARES NO TYPES, deliberately. It once carried a core-library
error type introduced by `u32::try_from`; the de-plumbing patches removed
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