From 1bc4f39f356b79c9be6314345c3f91a85808b106 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Tue, 28 Jul 2026 13:03:35 +0200 Subject: [PATCH] round 7: assert pin-map completeness (NEW-13), correct the count to 137, fix the regeneration-scope contradiction MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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 --- README.md | 25 +++++--- TRUSTED-BASE.md | 49 ++++++++++++---- verification/PROVENANCE.json | 6 +- verification/RECORDED-RUN.md | 101 +++++++++++++++++++++++++++++++++ verification/check-selftest.sh | 35 +++++++++++- verification/check.sh | 19 +++++++ verification/extract.sh | 2 +- 7 files changed, 210 insertions(+), 27 deletions(-) diff --git a/README.md b/README.md index 345a1e1..c766dd1 100644 --- a/README.md +++ b/README.md @@ -66,13 +66,17 @@ cannot translate the deployed `Hashers` function-pointer struct): - **Not the deployed public verifier:** the proved subject is the private `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": **131 assertion points**, - of which **20 are NIST ACVP SHA2-128s known-answer tests run against the - proved path** (see TRUSTED-BASE.md item 9). Until 2026-07-28 it was nine - points 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 (provenance recorded in the vector file). + 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. @@ -314,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 diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index 8f7fb47..a3da70c 100644 --- 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 `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 @@ -47,17 +47,34 @@ proceeds and is part of every claim. 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): - - **131 assertion points** (was 9 until 2026-07-28: three rounds from one - fixed seed, corrupting one fixed byte of a 7856-byte signature); - - of those, **20 are NIST ACVP SHA2-128s known-answer tests run against the - proved path** — 10 from the `internal` group, whose message *is* M′ and so - is exactly what `slh_verify_128s` consumes, and 10 from the `external pure` - group where mono, the deployed verifier and NIST must all three agree. - NIST's negatives cover structurally distinct corruption sites (modified R, - SIGFORS, SIGHT, modified message) rather than one arbitrary byte; - - the remaining 108 are randomized: 12 rounds, varying message lengths - including empty, corruption spread across the whole signature, plus - wrong-public-key and wrong-context cases. + - **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. @@ -97,6 +114,14 @@ proceeds and is part of every claim. 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`, diff --git a/verification/PROVENANCE.json b/verification/PROVENANCE.json index dfde3ea..b576c48 100644 --- a/verification/PROVENANCE.json +++ b/verification/PROVENANCE.json @@ -3,9 +3,9 @@ "parameter_set": "SLH-DSA-SHA2-128s", "source": { "repo": "github.com/saymrwulf/fips205-source", - "head": "3153988c4e89df66c41e698329f2ae5460880875", + "head": "c945821bf964a78bed3ba920ad5aa021083e6237", "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 all four model files byte-identically)", + "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,7 +36,7 @@ "gen/SlhVerify/TypesExternal.lean", "gen/SlhVerify/FunsExternal.lean" ], - "byte_identical_regeneration_verified": "2026-07-28 (re-verified after the test/vector commit: all four pinned model files unchanged)", + "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": "2988c04c5fc8c634aff4d9bd13604b8a47e677daa1f45e8f4f321368606cdd0a", diff --git a/verification/RECORDED-RUN.md b/verification/RECORDED-RUN.md index 0c23705..b0add11 100644 --- a/verification/RECORDED-RUN.md +++ b/verification/RECORDED-RUN.md @@ -349,3 +349,104 @@ 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. +``` diff --git a/verification/check-selftest.sh b/verification/check-selftest.sh index 1989e26..88c1a50 100755 --- a/verification/check-selftest.sh +++ b/verification/check-selftest.sh @@ -25,6 +25,9 @@ # 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. @@ -281,7 +284,12 @@ EOF rm -f Evil.lean # the SOURCE is gone; only the .olean remains printf '\nimport Evil\n' >> Proofs/ChainSpec.lean if [ ! -f Evil.olean ]; then - echo " (note: could not build Evil.olean; attack 16 inconclusive)"; rm -f Evil.olean + # 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 @@ -318,6 +326,27 @@ grep -q "INTEGRITY FAILED" /tmp/sf17.out || fail "ATTACK 17: rejected but not vi 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 +grep -q "pin map INCOMPLETE" /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 missing pin" /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 @@ -348,8 +377,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: 16 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." diff --git a/verification/check.sh b/verification/check.sh index 75dafe4..4ced28a 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -83,6 +83,25 @@ 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. +REQUIRED = { + "lean-guard", "Proofs/Audit.lean", + "gen/SlhVerify/Types.lean", "gen/SlhVerify/Funs.lean", + "gen/SlhVerify/TypesExternal.lean", "gen/SlhVerify/FunsExternal.lean", +} +missing = REQUIRED - set(files) +if missing: + for m in sorted(missing): + print(f" ✗ pin map INCOMPLETE — no entry for {m}") + bad = 1 for rel, want in sorted(files.items()): p = os.path.join(here, rel) if not os.path.exists(p): diff --git a/verification/extract.sh b/verification/extract.sh index 3599c53..a3114e4 100755 --- 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:-3153988c4e89df66c41e698329f2ae5460880875}" +EXPECTED_SRC_COMMIT="${EXPECTED_SRC_COMMIT:-c945821bf964a78bed3ba920ad5aa021083e6237}" # ── 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; }