mirror of
https://github.com/saymrwulf/fips205-slhdsa-verified.git
synced 2026-09-03 19:53:49 +00:00
review round 2: in-Lean exact-cone audit + reproducibility + doc honesty
Addresses the round-2 reviewer punch-list. No theorem statement, proof term,
or fold definition changed; the eleven cones are unchanged (independent
collectAxioms dump in verification/RECORDED-RUN.md).
AUDIT GATE (both reviewers, the critical one)
- Retire the bash #print-axioms text parser (fail-open on empty/truncated
reports, and only a SUBSET check). Replace with verification/Proofs/Audit.lean:
reads each certificate's cone from the kernel via collectAxioms and asserts
EXACT set equality against its expected boundary. Extra axiom, dropped
oracle, renamed/deleted cert, or an axiom/opaque sham each throw -> non-zero
Lean exit. No text to misparse; nothing fails open. check.sh Phase 3 now just
compiles it (and still requires the explicit PASSED line).
- check-selftest.sh rewritten to attack the new gate: dead-file, smuggled extra
axiom (named), dropped-oracle (subset would pass, exact must not), and a
vanished certificate (the collectAxioms-returns-[] trap). All four rejected.
REPRODUCIBILITY (GPT B1.4 / B1.5)
- extract.sh refuses a wrong-commit or dirty source tree (fail-closed), takes
an optional source-path arg, and pins the source commit.
- verification/PROVENANCE.json: single machine-readable pin set (source +
charon + aeneas commits/channel + lean + ocaml) with generated-file sha256.
- Re-running extract.sh reproduces gen/SlhVerify/{Types,Funs}.lean
byte-identically (companion fips205-source commit adds Cargo.lock +
rust-toolchain.toml; verified not to perturb the model).
DOC HONESTY (both reviewers)
- README: fix the self-contradiction (apex "not yet proven" trailer vs the
proven apex), the false "oracles kept OUTSIDE every cone" (they are INSIDE,
by design), "deployed monomorphic path" and "semantics-identical for every
parameter set" overclaims, "only two lines changed", stale snapshot head;
retitle the stale future-tense "what will be claimed" section.
- TRUSTED-BASE: drop "nothing proven yet"; add base_2b-inner and deployment-
bridge non-claims explicitly; current pin.
- ChainSpec header: "deployed monomorphic path" -> private verify_mono facade
(comment only).
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This commit is contained in:
parent
eb1d9f108a
commit
522d8b2092
9 changed files with 434 additions and 170 deletions
116
README.md
116
README.md
|
|
@ -5,11 +5,16 @@ 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 round 1 applied)
|
||||
## STATUS: eleven certificates over the extracted verify model (external review round 2 applied)
|
||||
|
||||
`verification/check.sh` is **green** (exit 0): the model compiles, the
|
||||
proofs compile, and the axiom audit passes (the Phase-3 parser was rewritten
|
||||
to be fail-closed and wrap-safe after external review round 1, 2026-07-24).
|
||||
proofs compile, and the axiom audit passes. The audit now runs **inside
|
||||
Lean** (`verification/Proofs/Audit.lean`): it reads each certificate's cone
|
||||
from the kernel via `collectAxioms` and asserts SET EQUALITY against that
|
||||
certificate's expected boundary — so an *added* axiom and a silently
|
||||
*dropped* oracle dependency both fail, with no text parsing to misparse
|
||||
(external review round 2, 2026-07-24, replaced the earlier `#print axioms`
|
||||
text parser, which could fail open on an empty or truncated report).
|
||||
|
||||
**What is actually established** — eleven Lean theorems about the
|
||||
Aeneas-generated model of the **monomorphic `verify_mono` compatibility
|
||||
|
|
@ -56,14 +61,15 @@ The trust base and residual assumptions are stated in
|
|||
- **`fips205.chain_free_loop_eq`** (Algorithm 5, WOTS+ chaining): the
|
||||
extracted `chain_free` loop equals the explicit s-fold hash chain, with
|
||||
the hash address set to i, i+1, …, i+s−1 in turn. This rules out —
|
||||
machine-checked, for the deployed monomorphic SHA2-128s verify path — an
|
||||
machine-checked, for the monomorphic SHA2-128s `verify_mono` path — an
|
||||
off-by-one loop bound, a wrong address field, and wrong threading. Its
|
||||
`#print axioms` cone is **exactly** `[propext, Classical.choice,
|
||||
Quot.sound, verify_mono.oracle.f]` — the three kernel axioms plus the one
|
||||
hash oracle it touches, and nothing else (no transpiler plumbing; the u32
|
||||
range machinery was discharged with real definitions). check.sh Phase 3
|
||||
fails the build if any certificate cone contains anything outside the
|
||||
kernel three + the five documented SHA-2 oracles.
|
||||
(the in-Lean exact-cone audit) fails the build if any certificate's cone
|
||||
differs from its expected set — an extra axiom or a dropped oracle both
|
||||
break it.
|
||||
|
||||
- **`fips205.wots_loop1_eq`** (Algorithm 8, WOTS+ pk recomputation — the
|
||||
chain loop): the extracted `wots_pk_from_sig_free_loop1` equals the fold
|
||||
|
|
@ -103,10 +109,11 @@ exit 0); the u32 range-loop de-plumbing (faithful `Step` defs vs pinned
|
|||
rustc, axiom-clean); the 8-site source de-plumbing (snapshot commit
|
||||
`6f6a9d6`: `try_from`/`is_err`/`unwrap` on pre-masked values → plain
|
||||
casts, the WOTS+ checksum `iter().take()` + `&u32` Sub → an index loop —
|
||||
each site semantics-identical for every FIPS 205 parameter set, and the
|
||||
obsoleted transpiler axioms deleted from the external files); fidelity
|
||||
pinned by a differential test in the snapshot (valid / corrupted /
|
||||
wrong-message), re-run green after every source patch.
|
||||
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.
|
||||
|
||||
- **`fips205.fors_inner_loop_eq`** + **`fips205.fors_outer_loop_eq`**
|
||||
(Algorithm 17, FORS pk-from-sig): a nested loop, split into two theorems.
|
||||
|
|
@ -131,10 +138,14 @@ wrong-message), re-run green after every source patch.
|
|||
removing the last `Take`/`IterMut` iterator adapters; the obsoleted `Take`
|
||||
axiom was then deleted.
|
||||
|
||||
The remaining work (the digest-split composition and the apex — the top-level
|
||||
`slh_verify` accepting iff the recomputed hypertree root equals the pinned
|
||||
public-key root) is not yet proven. The pyramid rises one certificate at a
|
||||
time, each audited to the same boundary.
|
||||
The apex (`slh_verify_128s_accepts_iff`, above) sits at the top of this layer:
|
||||
the extracted `verify_mono::slh_verify_128s` accepts iff the recomputed
|
||||
hypertree root byte-equals the pinned public-key root. What remains genuinely
|
||||
unproven is stated in "What is NOT (yet) established" above — most sharply the
|
||||
opaque `base_2b` inner loop (no certificate) and the bridge from this private
|
||||
`verify_mono` facade to the deployed generic verifier (a finite differential
|
||||
test, not a machine-checked refinement). Each certificate is audited to the
|
||||
same boundary.
|
||||
|
||||
## Subject
|
||||
|
||||
|
|
@ -143,12 +154,15 @@ time, each audited to the same boundary.
|
|||
modules mirroring the FIPS 205 algorithm structure.
|
||||
- Pinned at upstream commit `30bac08580aa61f653e5436d1bbacb5ffac446c4`
|
||||
(2025-09-01), snapshotted with full history at
|
||||
`saymrwulf/fips205-source` (snapshot head `5dca0db`, whose single
|
||||
deviation from verbatim is the removal of upstream CI workflows,
|
||||
documented in that commit). Aeneas-compat patches will land in the
|
||||
snapshot repo as transparent, individually-justified commits — never
|
||||
upstream. **No affiliation with, and no changes proposed to, the
|
||||
upstream project.**
|
||||
`saymrwulf/fips205-source`. The verbatim-import base commit's only
|
||||
deviation from upstream is the removal of CI workflows (documented in
|
||||
that commit); the Aeneas-compat and de-plumbing patches then landed as
|
||||
transparent, individually-justified commits on top — never upstream.
|
||||
The current snapshot head is **`797b4ef`** (the round-2 reproducibility
|
||||
commit — committed `Cargo.lock` + pinned `rust-toolchain.toml` — on top of
|
||||
de-plumbing round 2, `bea1051`); the model in this repo is extracted from
|
||||
it, and `verification/extract.sh` refuses any other commit. **No
|
||||
affiliation with, and no changes proposed to, the upstream project.**
|
||||
- Parameter set: **SLH-DSA-SHA2-128s** first (the small-signature profile
|
||||
deployed in the firmware/code-signing lane). The architecture
|
||||
generalizes; each further parameter set is a separate claim (rigor
|
||||
|
|
@ -169,9 +183,15 @@ Key generation and signing are out of scope (trusted base), exactly as
|
|||
ed25519 signing was. The five verify-path hash oracles (`h_msg, f, h,
|
||||
t_l, t_len` — SHA-2 instantiations; `prf`/`prf_msg` are sign-side only
|
||||
and never enter the cone) are opaque external models with written
|
||||
justifications, kept outside every certificate's dependency cone
|
||||
(honesty invariant H4); their semantics are the standing SHA-2 oracle
|
||||
boundary documented in [TRUSTED-BASE.md](TRUSTED-BASE.md).
|
||||
justifications. They are the *only* things beyond Lean's three kernel
|
||||
axioms that any certificate cone contains: each cone is exactly the
|
||||
kernel three plus the specific oracles that certificate's computation
|
||||
reaches (e.g. `chain` reaches `F`, so `oracle.f` is inside its cone; the
|
||||
input-prep helpers reach no hash, so their cones are kernel-3 alone).
|
||||
That the cones contain *nothing else* — no transpiler plumbing, no
|
||||
hidden axiom — is what the audit enforces (honesty invariant H4); their
|
||||
semantics are the standing SHA-2 oracle boundary documented in
|
||||
[TRUSTED-BASE.md](TRUSTED-BASE.md).
|
||||
|
||||
## Gate-0 record (2026-07-22)
|
||||
|
||||
|
|
@ -195,32 +215,44 @@ this repository was created:
|
|||
(nested `&[&[u8]]` is untranslatable), and one `let-else` became the
|
||||
`is_err`/`unwrap` idiom. `verification/extract.sh` now re-derives the
|
||||
model from the mono root; charon + aeneas both exit 0, and
|
||||
`verification/check.sh` compiles the result. The generic paths and all
|
||||
twelve parameter sets are untouched (the only change to existing code is
|
||||
two lines wiring the module).
|
||||
`verification/check.sh` compiles the result. At this compat-patch commit
|
||||
the only change to pre-existing code was two lines wiring the new module;
|
||||
the generic paths and all twelve parameter sets stayed untouched. (The
|
||||
later de-plumbing commits — rounds 1 and 2 — then made further local edits
|
||||
to `helpers.rs`/`wots.rs`, each documented and differential-tested; see the
|
||||
snapshot history at head `797b4ef`.)
|
||||
|
||||
## What will be claimed (when the button is green, not before)
|
||||
## What is claimed (the button is green)
|
||||
|
||||
One theorem per layer, each a statement about the **extracted** functions
|
||||
(H3), compiled by `verification/check.sh` with a per-certificate
|
||||
`#print axioms` audit (H1): chain semantics, WOTS+ pk recomputation,
|
||||
XMSS path recomputation, hypertree acceptance, FORS pk recomputation,
|
||||
and the apex — `slh_verify_internal` accepts iff the recomputed
|
||||
hypertree root equals the pinned public-key root.
|
||||
Each certificate is a statement about the **extracted** functions (H3),
|
||||
compiled by `verification/check.sh` with the in-Lean exact-cone audit (H1):
|
||||
chain semantics, WOTS+ pk recomputation, XMSS path recomputation, hypertree
|
||||
acceptance, FORS pk recomputation, the input-prep helpers, and the apex —
|
||||
`verify_mono::slh_verify_128s` accepts iff the recomputed hypertree root
|
||||
equals the pinned public-key root. The precise scope and non-claims are in
|
||||
the STATUS section above.
|
||||
|
||||
**The allowed axiom set, stated precisely:** unlike the ed25519 field and
|
||||
scalar layers (whose cones are exactly `[propext, Classical.choice,
|
||||
Quot.sound]`), the hash oracles permeate *every* SLH-DSA layer — `chain`
|
||||
already calls `F`. So each certificate's cone may contain the three
|
||||
kernel axioms **plus at most the five named oracles**
|
||||
(`verify_mono.oracle.{h_msg, f, h, t_l, t_len}`) — and nothing else: the
|
||||
transpiler-plumbing axioms currently in `FunsExternal.lean` must be
|
||||
discharged before any certificate ships, and the audit fails the button
|
||||
if any of them (or anything unlisted) appears in a cone.
|
||||
already calls `F`. Each certificate's cone is therefore the three kernel
|
||||
axioms **plus exactly the named oracles its computation reaches** (and
|
||||
nothing else). The transpiler-plumbing axioms that once sat in
|
||||
`FunsExternal.lean` were discharged (de-plumbing rounds 1+2) before any
|
||||
certificate shipped; the audit fails the button if anything outside a
|
||||
certificate's expected boundary — plumbing, an extra oracle, or a dropped
|
||||
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 from
|
||||
the committed `extract.sh` against the pinned snapshot (R1). What cannot
|
||||
be proven is named in [TRUSTED-BASE.md](TRUSTED-BASE.md), not hidden (H5).
|
||||
(memory-capped, machine-wide serialized). 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
|
||||
source tree, and re-running it reproduces the aeneas-generated model
|
||||
byte-identically (verified 2026-07-24). The axiom audit runs inside Lean
|
||||
([verification/Proofs/Audit.lean](verification/Proofs/Audit.lean)): exact
|
||||
per-certificate cone equality, fail-closed, adversarially exercised by
|
||||
`verification/check-selftest.sh`. What cannot be proven is named in
|
||||
[TRUSTED-BASE.md](TRUSTED-BASE.md), not hidden (H5).
|
||||
|
|
|
|||
|
|
@ -1,7 +1,10 @@
|
|||
# TRUSTED-BASE — what the certificates will NOT cover
|
||||
# TRUSTED-BASE — what the certificates do NOT cover
|
||||
|
||||
Initial statement, written at skeleton time (nothing proven yet); this
|
||||
file is maintained as the campaign proceeds and is part of every claim.
|
||||
Eleven certificates over the extracted `verify_mono` model are now proven
|
||||
(`verification/check.sh` green; the apex is
|
||||
`fips205.slh_verify_128s_accepts_iff`). This file states what those
|
||||
certificates deliberately do NOT establish; it is maintained as the campaign
|
||||
proceeds and is part of every claim.
|
||||
|
||||
1. **The five verify-path hash oracles.** `h_msg, f, h, t_l, t_len`
|
||||
(SLH-DSA-SHA2-128s instantiations over SHA-256; `prf`/`prf_msg` are
|
||||
|
|
@ -25,7 +28,20 @@ file is maintained as the campaign proceeds and is part of every claim.
|
|||
6. **Parameter-set scope.** Claims will bind SLH-DSA-SHA2-128s only;
|
||||
other parameter sets are unverified until separately extracted and
|
||||
proven (R2).
|
||||
7. **Aeneas-compat patch surface.** The fn-pointer-to-named-oracle
|
||||
rewrite in `fips205-source` (phase 1) is part of the verified surface:
|
||||
the certificate covers the patched verify path, and the patch commits
|
||||
are the auditable delta from upstream `30bac08`.
|
||||
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
|
||||
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
|
||||
to upstream is argued in its commit and checked, for SHA2-128s, by the
|
||||
snapshot differential test — it is not itself machine-checked.
|
||||
8. **The `base_2b` inner loop.** `helpers.base_2b_loop0_loop0` (which
|
||||
determines the FORS indices and WOTS digits) is threaded opaquely and
|
||||
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.
|
||||
|
|
|
|||
36
verification/PROVENANCE.json
Normal file
36
verification/PROVENANCE.json
Normal file
|
|
@ -0,0 +1,36 @@
|
|||
{
|
||||
"_comment": "Single machine-readable pin set to reproduce the extracted Lean model in gen/SlhVerify from source. External review round 2 (2026-07-24). Running verification/extract.sh against the pinned source tree with the pinned Charon/Aeneas toolchain reproduces the two aeneas-generated files byte-identically (sha256 below). The *External*.lean files are hand-maintained (not regenerated) and are NOT part of this reproducibility claim.",
|
||||
"parameter_set": "SLH-DSA-SHA2-128s",
|
||||
"source": {
|
||||
"repo": "github.com/saymrwulf/fips205-source",
|
||||
"head": "797b4ef26338e27363683656f93cb065a77daa0e",
|
||||
"upstream_base": "integritychain/fips205 @ 30bac08580aa61f653e5436d1bbacb5ffac446c4",
|
||||
"upstream_deviation": "verbatim import minus CI workflows; then the additive monomorphic verify_mono compat module + de-plumbing rounds 1-2, each an individually-justified commit",
|
||||
"cargo_lock": "committed",
|
||||
"rust_toolchain_toml": "nightly-2026-06-01"
|
||||
},
|
||||
"transpiler": {
|
||||
"charon": { "commit": "9dd7f23c", "toolchain_channel": "nightly-2026-06-01" },
|
||||
"aeneas": { "commit": "bf13c42e" }
|
||||
},
|
||||
"proof_env": {
|
||||
"lean": "v4.30.0-rc2 (3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc)",
|
||||
"ocaml": "5.3.0"
|
||||
},
|
||||
"extraction": {
|
||||
"driver": "verification/extract.sh (refuses a wrong-commit or dirty source tree)",
|
||||
"charon": "charon cargo --preset=aeneas --start-from crate::verify_mono::slh_verify_128s --opaque crate::verify_mono::oracle --opaque sha2 --opaque sha3 --opaque zeroize --opaque rand_core --hide-marker-traits --dest-file SlhVerify.llbc -- --no-default-features --features slh_dsa_sha2_128s",
|
||||
"aeneas": "aeneas -backend lean -split-files -subdir SlhVerify -dest gen SlhVerify.llbc"
|
||||
},
|
||||
"generated_artifacts_sha256": {
|
||||
"SlhVerify.llbc": "d8ec0b00593eee1778bc4cc0cc1801fb6415bb294425f01384434849c6443f58",
|
||||
"gen/SlhVerify/Types.lean": "db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384",
|
||||
"gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f"
|
||||
},
|
||||
"hand_maintained_not_regenerated": [
|
||||
"gen/SlhVerify/TypesExternal.lean",
|
||||
"gen/SlhVerify/FunsExternal.lean"
|
||||
],
|
||||
"byte_identical_regeneration_verified": "2026-07-24",
|
||||
"audit_gate": "verification/Proofs/Audit.lean — in-Lean exact per-certificate cone equality via collectAxioms (fail-closed); compiled by check.sh Phase 3; adversarially exercised by check-selftest.sh"
|
||||
}
|
||||
97
verification/Proofs/Audit.lean
Normal file
97
verification/Proofs/Audit.lean
Normal file
|
|
@ -0,0 +1,97 @@
|
|||
/- ──────────────────────────────────────────────────────────────────────────────
|
||||
Proofs/Audit.lean — the axiom-cone audit, performed INSIDE Lean.
|
||||
|
||||
Round-2 external review (2026-07-24) showed the bash `#print axioms` text
|
||||
parser was still fragile: it fail-OPENED on an empty `[]` or a truncated
|
||||
(missing-`]`) report, and it only subset-checked (a *removed* oracle
|
||||
dependency would pass unnoticed). This file removes text parsing entirely.
|
||||
|
||||
`collectAxioms` reads the kernel's own axiom set for each certificate. We
|
||||
assert, for every one of the eleven:
|
||||
|
||||
· the certificate EXISTS and is a `theorem` (not an axiom/opaque sham,
|
||||
not a renamed/deleted name — `collectAxioms` returns `#[]` for a
|
||||
missing name, so existence is checked explicitly, fail-closed);
|
||||
· its cone equals its EXPECTED set EXACTLY — extras (a smuggled axiom)
|
||||
AND missing (a silently dropped oracle dependency) both fail.
|
||||
|
||||
Any mismatch is a `throwError`, i.e. a Lean elaboration error → non-zero
|
||||
`lean` exit. There is no text to misparse and nothing fails open. This is
|
||||
the single source of the axiom claim; check.sh Phase 3 just compiles it.
|
||||
────────────────────────────────────────────────────────────────────────────── -/
|
||||
import Proofs.ChainSpec
|
||||
import Proofs.WotsSpec
|
||||
import Proofs.XmssSpec
|
||||
import Proofs.HtSpec
|
||||
import Proofs.ForsInnerSpec
|
||||
import Proofs.ForsOuterSpec
|
||||
import Proofs.InputPrepSpec
|
||||
import Proofs.ApexSpec
|
||||
open Lean Elab Command
|
||||
|
||||
namespace SlhVerify.Audit
|
||||
|
||||
/-- Lean's three kernel axioms — permitted in every cone. -/
|
||||
def kernel3 : List Name := [`propext, `Classical.choice, `Quot.sound]
|
||||
|
||||
/-- The five SHA-2 verify-path hash oracles — the documented cryptographic
|
||||
boundary (TRUSTED-BASE.md). No other axiom may appear anywhere. -/
|
||||
def oracleF : Name := `verify_mono.oracle.f
|
||||
def oracleH : Name := `verify_mono.oracle.h
|
||||
def oracleTL : Name := `verify_mono.oracle.t_l
|
||||
def oracleTLen : Name := `verify_mono.oracle.t_len
|
||||
def oracleHMsg : Name := `verify_mono.oracle.h_msg
|
||||
|
||||
/-- The entire allowed boundary: nothing outside this set is permitted in any
|
||||
certificate cone, and the expected table below may reference nothing else. -/
|
||||
def allowedBoundary : List Name :=
|
||||
kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg]
|
||||
|
||||
/-- EXACT expected cone per certificate. Ground truth captured 2026-07-24 via
|
||||
`collectAxioms` (Probe.lean) and cross-checked against both round-1
|
||||
reviewers' independent reconstructions. Each entry is asserted for SET
|
||||
EQUALITY, so this table is a load-bearing specification of the boundary:
|
||||
changing a proof so it drops an oracle, or adds one, breaks the audit. -/
|
||||
def expectedCones : List (Name × List Name) :=
|
||||
[ (`fips205.chain_free_loop_eq, kernel3 ++ [oracleF]),
|
||||
(`fips205.wots_loop1_eq, kernel3 ++ [oracleF]),
|
||||
(`fips205.xmss_loop_eq, kernel3 ++ [oracleH]),
|
||||
(`fips205.ht_loop_eq, kernel3 ++ [oracleF, oracleH, oracleTL]),
|
||||
(`fips205.fors_inner_loop_eq, kernel3 ++ [oracleH]),
|
||||
(`fips205.fors_outer_loop_eq, kernel3 ++ [oracleF, oracleH]),
|
||||
(`fips205.to_int_loop_eq, kernel3),
|
||||
(`fips205.to_byte_loop_eq, kernel3),
|
||||
(`fips205.wots_csum_loop_eq, kernel3),
|
||||
(`fips205.base2b_outer_loop_eq, kernel3),
|
||||
(`fips205.slh_verify_128s_accepts_iff, kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg]) ]
|
||||
|
||||
elab "auditCones" : command => do
|
||||
let env ← getEnv
|
||||
-- (0) the expected table itself must stay within the boundary — guards a typo
|
||||
-- in this file from silently widening what "allowed" means.
|
||||
for (cert, expected) in expectedCones do
|
||||
for a in expected do
|
||||
unless allowedBoundary.contains a do
|
||||
throwError "audit table references non-boundary axiom {a} for {cert}"
|
||||
-- (1) per certificate: exists ∧ is a theorem ∧ cone == expected set exactly.
|
||||
let mut errs : Array String := #[]
|
||||
for (cert, expected) in expectedCones do
|
||||
match env.find? cert with
|
||||
| none => errs := errs.push s!"{cert}: NOT FOUND (renamed/deleted?)"
|
||||
| some (.thmInfo _) =>
|
||||
let got := (← collectAxioms cert).toList
|
||||
let extras := got.filter (fun a => !expected.contains a)
|
||||
let missing := expected.filter (fun a => !got.contains a)
|
||||
unless extras.isEmpty && missing.isEmpty do
|
||||
errs := errs.push s!"{cert}: extra={extras} missing={missing}"
|
||||
| some (.axiomInfo _) => errs := errs.push s!"{cert}: is an AXIOM, not a proven theorem"
|
||||
| some (.opaqueInfo _) => errs := errs.push s!"{cert}: is OPAQUE, not a proven theorem"
|
||||
| some _ => errs := errs.push s!"{cert}: not a theorem"
|
||||
unless errs.isEmpty do
|
||||
throwError "EXACT-CONE AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}"
|
||||
logInfo s!"exact-cone audit PASSED: {expectedCones.length} certificates, each cone == its expected boundary set (kernel-3 + only the named SHA-2 oracles)"
|
||||
|
||||
end SlhVerify.Audit
|
||||
|
||||
open SlhVerify.Audit in
|
||||
auditCones
|
||||
|
|
@ -3,8 +3,9 @@
|
|||
THEOREM chain_free_loop_eq: the extracted `chain_free` loop equals the
|
||||
explicit s-fold application of the hash F, with the hash-address set to
|
||||
i, i+1, …, i+s−1 in turn. This rules out — machine-checked, for the
|
||||
deployed monomorphic SHA2-128s verify path — an off-by-one loop bound, a
|
||||
wrong address field, and wrong threading. F stays opaque
|
||||
monomorphic SHA2-128s `verify_mono` path (a private facade, not the
|
||||
deployed generic verifier) — an off-by-one loop bound, a wrong address
|
||||
field, and wrong threading. F stays opaque
|
||||
(verify_mono.oracle.f), so the certificate cone is the three kernel axioms
|
||||
+ oracle.f, and nothing else (audited by check.sh Phase 3).
|
||||
|
||||
|
|
|
|||
50
verification/RECORDED-RUN.md
Normal file
50
verification/RECORDED-RUN.md
Normal file
|
|
@ -0,0 +1,50 @@
|
|||
# Recorded clean run — check.sh + independent cone dump
|
||||
|
||||
External review round 2 asked for a recorded clean run at the current pin
|
||||
by a party with the toolchain, so a reviewer who cannot run Lean has current
|
||||
evidence. Captured 2026-07-24. Pins are in [PROVENANCE.json](PROVENANCE.json).
|
||||
The cone dump below is an *independent* `collectAxioms` read (not the asserted
|
||||
table in Proofs/Audit.lean); it matches each certificate's expected boundary.
|
||||
|
||||
```
|
||||
RECORDED CLEAN RUN — fips205-slhdsa-verified
|
||||
date(UTC): 20260724T171145Z
|
||||
host lean: Lean (version 4.30.0-rc2, x86_64-unknown-linux-gnu, commit 3dc1a088b6d2d8eafe25a7cd7ec7b58d731bd7cc, Release)
|
||||
source pin: 797b4ef26338e27363683656f93cb065a77daa0e
|
||||
==============================================
|
||||
fips205-slhdsa-verified — check
|
||||
===============================
|
||||
=== 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: axiom audit (exact cone per certificate — inside Lean) ===
|
||||
✓ exact-cone audit PASSED: each of the 11 certificate cones == its expected boundary set
|
||||
|
||||
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
|
||||
|
||||
=== INDEPENDENT cone dump (collectAxioms, 20260724T171253Z) ===
|
||||
fips205.chain_free_loop_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.f
|
||||
fips205.wots_loop1_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.f
|
||||
fips205.xmss_loop_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.h
|
||||
fips205.ht_loop_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.f, verify_mono.oracle.h, verify_mono.oracle.t_l
|
||||
fips205.fors_inner_loop_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.h
|
||||
fips205.fors_outer_loop_eq :: propext, Classical.choice, Quot.sound, verify_mono.oracle.f, verify_mono.oracle.h
|
||||
fips205.to_int_loop_eq :: propext, Classical.choice, Quot.sound
|
||||
fips205.to_byte_loop_eq :: propext, Classical.choice, Quot.sound
|
||||
fips205.wots_csum_loop_eq :: propext, Classical.choice, Quot.sound
|
||||
fips205.base2b_outer_loop_eq :: propext, Classical.choice, Quot.sound
|
||||
fips205.slh_verify_128s_accepts_iff :: propext, Classical.choice, Quot.sound, verify_mono.oracle.f, verify_mono.oracle.h, verify_mono.oracle.h_msg, verify_mono.oracle.t_l, verify_mono.oracle.t_len
|
||||
```
|
||||
|
|
@ -1,25 +1,41 @@
|
|||
#!/usr/bin/env bash
|
||||
# Adversarial self-test of the check.sh gates (the R3-5 tradition: an audit
|
||||
# that cannot fail is theater). Three attacks, all MUST make check.sh fail:
|
||||
# Adversarial self-test of the check.sh gates (the R3-5 tradition: an audit that
|
||||
# cannot fail is theater). The axiom audit now runs INSIDE Lean
|
||||
# (Proofs/Audit.lean, exact cone per certificate via collectAxioms), so these
|
||||
# attacks target that gate's actual guarantees — not the retired text parser.
|
||||
# Every attack MUST make check.sh fail, via the intended gate:
|
||||
#
|
||||
# 1. DEAD FILE — a stray Proofs/*.lean not in the manifest.
|
||||
# 2. SMUGGLED AXIOM (short cone) — an axiom outside {kernel-3} ∪ {5 oracles},
|
||||
# on the FIRST line of the cone.
|
||||
# 3. SMUGGLED AXIOM (WRAPPED cone) — an axiom on a CONTINUATION line of a
|
||||
# cone that wraps (the exact fail-open exploit external review found on
|
||||
# 2026-07-24: the old single-line parser saw only line 1). This attack
|
||||
# guards the flattened-parse fix; a self-test that only plants short cones
|
||||
# cannot detect a wrapped-cone parser regression.
|
||||
# 2. SMUGGLED AXIOM — a certificate whose real cone contains a disallowed
|
||||
# axiom, declared clean. Exact-equality must report it
|
||||
# as `extra=[...]` (the classic extra-axiom detection).
|
||||
# 3. DROPPED ORACLE — a certificate whose expected cone claims an oracle
|
||||
# its real proof does NOT use. A subset checker would
|
||||
# pass this; exact-equality must report `missing=[...]`.
|
||||
# This is the property the round-2 review demanded and
|
||||
# the retired subset parser could never enforce.
|
||||
# 4. VANISHED CERT — a certificate name that no longer resolves. Since
|
||||
# `collectAxioms` returns [] for a missing name (a
|
||||
# fail-open trap), the audit must report NOT FOUND.
|
||||
#
|
||||
# Green here means: the gates genuinely reject all three. Self-cleaning.
|
||||
# Green here means: the gate genuinely rejects all four. Self-cleaning: the real
|
||||
# check.sh / Proofs/Audit.lean are backed up and restored around every attack.
|
||||
set -euo pipefail
|
||||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
cd "$HERE"
|
||||
|
||||
cleanup() { rm -f Proofs/Stray.lean Proofs/Stray.olean Proofs/EvilSpec.lean \
|
||||
Proofs/EvilSpec.olean Proofs/EvilWrapSpec.lean \
|
||||
Proofs/EvilWrapSpec.olean check-evil-tmp.sh check-evilwrap-tmp.sh; }
|
||||
restore() {
|
||||
[ -f check.sh.selftest.bak ] && mv -f check.sh.selftest.bak check.sh
|
||||
[ -f Proofs/Audit.lean.selftest.bak ] && mv -f Proofs/Audit.lean.selftest.bak Proofs/Audit.lean
|
||||
return 0
|
||||
}
|
||||
cleanup() {
|
||||
restore
|
||||
rm -f Proofs/Stray.lean Proofs/Stray.olean \
|
||||
Proofs/EvilSpec.lean Proofs/EvilSpec.olean Proofs/Audit.olean
|
||||
}
|
||||
trap cleanup EXIT
|
||||
backup() { cp -f check.sh check.sh.selftest.bak; cp -f Proofs/Audit.lean Proofs/Audit.lean.selftest.bak; }
|
||||
|
||||
echo "check-selftest: attacking the gates"
|
||||
echo "===================================="
|
||||
|
|
@ -30,76 +46,82 @@ if ./check.sh > /tmp/selftest-dead.out 2>&1; then
|
|||
echo "✗ ATTACK 1 SUCCEEDED: check.sh stayed green with a dead file"; exit 1
|
||||
fi
|
||||
grep -q "DEAD FILE" /tmp/selftest-dead.out \
|
||||
|| { echo "✗ ATTACK 1: failed, but not via the dead-file gate"; exit 1; }
|
||||
|| { echo "✗ ATTACK 1: failed, but not via the dead-file gate"; cat /tmp/selftest-dead.out; exit 1; }
|
||||
rm -f Proofs/Stray.lean Proofs/Stray.olean
|
||||
echo "✓ attack 1 rejected (dead-file gate works)"
|
||||
|
||||
# ── Attack 2: smuggled axiom ────────────────────────────────────────────────
|
||||
# ── Attack 2: smuggled disallowed axiom in a real cone ──────────────────────
|
||||
# A new certificate whose cone genuinely contains `evil_ax`, declared as clean
|
||||
# (kernel-3) in the expected table. Exact-equality must flag extra=[evil_ax].
|
||||
backup
|
||||
cat > Proofs/EvilSpec.lean <<'EOF'
|
||||
import Proofs.ChainSpec
|
||||
axiom evil_ax : True
|
||||
theorem evil_thm : True := evil_ax
|
||||
EOF
|
||||
python3 - <<'PY'
|
||||
import re
|
||||
# check.sh: add EvilSpec to PROOFS so Phase 2 builds it and the dead-file gate
|
||||
# passes (inject right after the array's opening paren — no hard-coded contents).
|
||||
s = open("check.sh").read()
|
||||
s = s.replace('PROOFS=(\n "ChainSpec"\n)', 'PROOFS=(\n "ChainSpec"\n "EvilSpec"\n)')
|
||||
# Robust to the growing PROOFS / CERTS lists (do NOT hard-code their current
|
||||
# contents — that rots the self-test as certificates are added): inject the
|
||||
# evil entries right after each array's opening paren.
|
||||
assert 'PROOFS=(\n' in s and 'CERTS=(\n' in s, "check.sh array shape changed"
|
||||
assert 'PROOFS=(\n' in s, "check.sh PROOFS array shape changed"
|
||||
s = s.replace('PROOFS=(\n', 'PROOFS=(\n "EvilSpec"\n', 1)
|
||||
s = s.replace('CERTS=(\n', 'CERTS=(\n "evil_thm"\n', 1)
|
||||
assert '{ echo "import Proofs.ChainSpec"' in s, "check.sh audit import shape changed"
|
||||
s = s.replace('{ echo "import Proofs.ChainSpec"',
|
||||
'{ echo "import Proofs.EvilSpec"; echo "import Proofs.ChainSpec"', 1)
|
||||
open("check-evil-tmp.sh","w").write(s)
|
||||
open("check.sh","w").write(s)
|
||||
# Audit.lean: import EvilSpec and claim evil_thm is kernel-3 clean.
|
||||
a = open("Proofs/Audit.lean").read()
|
||||
assert 'import Proofs.ApexSpec' in a, "Audit.lean import shape changed"
|
||||
a = a.replace('import Proofs.ApexSpec', 'import Proofs.ApexSpec\nimport Proofs.EvilSpec', 1)
|
||||
assert 'def expectedCones : List (Name × List Name) :=' in a and ' [ (' in a, "Audit.lean table shape changed"
|
||||
a = a.replace(' [ (', ' [ (`evil_thm, kernel3),\n (', 1)
|
||||
open("Proofs/Audit.lean","w").write(a)
|
||||
PY
|
||||
chmod +x check-evil-tmp.sh
|
||||
if ./check-evil-tmp.sh > /tmp/selftest-evil.out 2>&1; then
|
||||
echo "✗ ATTACK 2 SUCCEEDED: audit passed a smuggled axiom"; exit 1
|
||||
if ./check.sh > /tmp/selftest-evil.out 2>&1; then
|
||||
echo "✗ ATTACK 2 SUCCEEDED: audit passed a smuggled disallowed axiom"; exit 1
|
||||
fi
|
||||
grep -q "DISALLOWED" /tmp/selftest-evil.out \
|
||||
|| { echo "✗ ATTACK 2: failed, but not via the axiom gate"; exit 1; }
|
||||
rm -f Proofs/EvilSpec.lean Proofs/EvilSpec.olean check-evil-tmp.sh
|
||||
echo "✓ attack 2 rejected (axiom gate works)"
|
||||
grep -q "AUDIT FAILED" /tmp/selftest-evil.out \
|
||||
|| { echo "✗ ATTACK 2: failed, but not via the axiom audit"; cat /tmp/selftest-evil.out; exit 1; }
|
||||
grep -q "evil_ax" /tmp/selftest-evil.out \
|
||||
|| { echo "✗ ATTACK 2: rejected, but the audit did not name the smuggled axiom"; cat /tmp/selftest-evil.out; exit 1; }
|
||||
restore; rm -f Proofs/EvilSpec.lean Proofs/EvilSpec.olean Proofs/Audit.olean
|
||||
echo "✓ attack 2 rejected (extra-axiom detection works — evil_ax named)"
|
||||
|
||||
# ── Attack 3: smuggled axiom on a WRAPPED cone (the fail-open exploit) ───────
|
||||
# evil_wrapped_thm bundles a disallowed axiom with the apex theorem, so its cone
|
||||
# is 9 axioms and WRAPS across physical lines with review_evil_ax on a
|
||||
# continuation line — exactly what the old single-line parser missed.
|
||||
cat > Proofs/EvilWrapSpec.lean <<'EOF'
|
||||
import Proofs.ApexSpec
|
||||
open Aeneas Aeneas.Std Result
|
||||
open fips205
|
||||
axiom review_evil_ax : True
|
||||
theorem evil_wrapped_thm
|
||||
(mprime : Slice Std.U8)
|
||||
(sig : types.SlhDsaSig 12#usize 7#usize 9#usize 14#usize 35#usize 16#usize)
|
||||
(pk : types.SlhPublicKey 16#usize) :
|
||||
True ∧ (verify_mono.slh_verify_128s mprime sig pk
|
||||
= (do let root ← slhVerifyRoot 63#usize 30#usize mprime sig pk
|
||||
ok (decide (root.val = pk.pk_root.val)))) :=
|
||||
⟨review_evil_ax, slh_verify_128s_accepts_iff mprime sig pk⟩
|
||||
EOF
|
||||
# ── Attack 3: dropped-oracle (subset would pass; exact must not) ─────────────
|
||||
# Claim to_int_loop_eq depends on oracle.f. Its real cone is kernel-3 only, so
|
||||
# the audit must report missing=[verify_mono.oracle.f].
|
||||
backup
|
||||
python3 - <<'PY'
|
||||
s = open("check.sh").read()
|
||||
assert 'PROOFS=(\n' in s and 'CERTS=(\n' in s, "check.sh array shape changed"
|
||||
s = s.replace('PROOFS=(\n', 'PROOFS=(\n "EvilWrapSpec"\n', 1)
|
||||
s = s.replace('CERTS=(\n', 'CERTS=(\n "evil_wrapped_thm"\n', 1)
|
||||
assert '{ echo "import Proofs.ChainSpec"' in s, "check.sh audit import shape changed"
|
||||
s = s.replace('{ echo "import Proofs.ChainSpec"',
|
||||
'{ echo "import Proofs.EvilWrapSpec"; echo "import Proofs.ChainSpec"', 1)
|
||||
open("check-evilwrap-tmp.sh","w").write(s)
|
||||
import re
|
||||
a = open("Proofs/Audit.lean").read()
|
||||
new, n = re.subn(r'(`fips205\.to_int_loop_eq,\s*)kernel3\)', r'\1kernel3 ++ [oracleF])', a)
|
||||
assert n == 1, f"expected exactly one to_int table entry, patched {n}"
|
||||
open("Proofs/Audit.lean","w").write(new)
|
||||
PY
|
||||
chmod +x check-evilwrap-tmp.sh
|
||||
if ./check-evilwrap-tmp.sh > /tmp/selftest-evilwrap.out 2>&1; then
|
||||
echo "✗ ATTACK 3 SUCCEEDED: audit passed a smuggled axiom on a WRAPPED cone (fail-open!)"; exit 1
|
||||
if ./check.sh > /tmp/selftest-drop.out 2>&1; then
|
||||
echo "✗ ATTACK 3 SUCCEEDED: audit passed a certificate missing a claimed oracle (subset hole!)"; exit 1
|
||||
fi
|
||||
grep -q "DISALLOWED" /tmp/selftest-evilwrap.out \
|
||||
|| { echo "✗ ATTACK 3: failed, but not via the axiom gate (wrapped-cone parse?)"; exit 1; }
|
||||
grep -q "review_evil_ax" /tmp/selftest-evilwrap.out \
|
||||
|| { echo "✗ ATTACK 3: rejected, but the audit did not name the continuation-line axiom"; exit 1; }
|
||||
echo "✓ attack 3 rejected (wrapped-cone axiom gate works — the continuation-line axiom was seen)"
|
||||
grep -q "AUDIT FAILED" /tmp/selftest-drop.out \
|
||||
|| { echo "✗ ATTACK 3: failed, but not via the axiom audit"; cat /tmp/selftest-drop.out; exit 1; }
|
||||
grep -q "missing=\[verify_mono.oracle.f\]" /tmp/selftest-drop.out \
|
||||
|| { echo "✗ ATTACK 3: rejected, but not by naming the missing oracle (exact-cone not enforced?)"; cat /tmp/selftest-drop.out; exit 1; }
|
||||
restore; rm -f Proofs/Audit.olean
|
||||
echo "✓ attack 3 rejected (missing-oracle detection works — exact cone enforced, not subset)"
|
||||
|
||||
# ── Attack 4: vanished certificate (collectAxioms-returns-[] trap) ──────────
|
||||
backup
|
||||
python3 - <<'PY'
|
||||
a = open("Proofs/Audit.lean").read()
|
||||
assert a.count('`fips205.chain_free_loop_eq') >= 1
|
||||
a = a.replace('`fips205.chain_free_loop_eq,', '`fips205.chain_free_loop_eq_VANISHED,', 1)
|
||||
open("Proofs/Audit.lean","w").write(a)
|
||||
PY
|
||||
if ./check.sh > /tmp/selftest-vanish.out 2>&1; then
|
||||
echo "✗ ATTACK 4 SUCCEEDED: audit stayed green for a non-existent certificate (fail-open!)"; exit 1
|
||||
fi
|
||||
grep -q "NOT FOUND" /tmp/selftest-vanish.out \
|
||||
|| { echo "✗ ATTACK 4: failed, but not via the existence check"; cat /tmp/selftest-vanish.out; exit 1; }
|
||||
restore; rm -f Proofs/Audit.olean
|
||||
echo "✓ attack 4 rejected (existence check works — a vanished cert cannot pass as 0-axiom)"
|
||||
|
||||
echo
|
||||
echo "SELFTEST GREEN: all three gates genuinely reject their attacks."
|
||||
echo "SELFTEST GREEN: the audit genuinely rejects extra axioms, dropped oracles,"
|
||||
echo "vanished certificates, and dead proof files."
|
||||
|
|
|
|||
|
|
@ -5,9 +5,12 @@
|
|||
#
|
||||
# Phase 1 — compile the extracted Lean model (gen/SlhVerify).
|
||||
# Phase 2 — compile the proof files (Proofs/).
|
||||
# Phase 3 — axiom audit: every certificate's #print axioms cone must be a
|
||||
# subset of {propext, Classical.choice, Quot.sound} plus the five
|
||||
# SHA-2 hash oracles (the documented boundary) — nothing else.
|
||||
# Phase 3 — axiom audit, performed INSIDE Lean (Proofs/Audit.lean): each
|
||||
# certificate's cone, read from the kernel via `collectAxioms`, must
|
||||
# EQUAL its expected set EXACTLY — kernel-3 plus only the named SHA-2
|
||||
# oracles. No text parsing (round-2 review closed that class of bug);
|
||||
# any extra, any missing, a renamed/deleted cert, or an axiom/opaque
|
||||
# sham is a Lean elaboration error → non-zero exit → fail-closed.
|
||||
set -euo pipefail
|
||||
|
||||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
|
|
@ -49,9 +52,6 @@ CERTS=(
|
|||
"fips205.base2b_outer_loop_eq"
|
||||
"fips205.slh_verify_128s_accepts_iff"
|
||||
)
|
||||
ORACLES="verify_mono.oracle.f, verify_mono.oracle.h, verify_mono.oracle.t_l, verify_mono.oracle.t_len, verify_mono.oracle.h_msg"
|
||||
ALLOWED="[propext, Classical.choice, Quot.sound, ${ORACLES}]"
|
||||
|
||||
echo "fips205-slhdsa-verified — check"
|
||||
echo "==============================="
|
||||
|
||||
|
|
@ -74,49 +74,30 @@ lake env bash -c "
|
|||
compile() { echo \" · \$1\"; LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' \"Proofs/\${1}.lean\" >/dev/null || { echo \"FAIL: Proofs/\$1\"; exit 1; }; }
|
||||
for m in ${PROOFS[*]}; do compile \"\$m\"; done
|
||||
# no dead proof files: everything under Proofs/ must be in the manifest
|
||||
# (PROOFS) or be the audit driver (Audit, compiled in Phase 3).
|
||||
for f in Proofs/*.lean; do b=\$(basename \"\$f\" .lean)
|
||||
case \" ${PROOFS[*]} \" in *\" \$b \"*) ;; *) echo \"DEAD FILE: Proofs/\$b.lean not in manifest\"; exit 1 ;; esac
|
||||
case \" ${PROOFS[*]} Audit \" in *\" \$b \"*) ;; *) echo \"DEAD FILE: Proofs/\$b.lean not in manifest\"; exit 1 ;; esac
|
||||
done
|
||||
"
|
||||
|
||||
# ── Phase 3: axiom audit ────────────────────────────────────────────────────
|
||||
echo "=== Phase 3: axiom audit (cone ⊆ kernel-3 + 5 oracles) ==="
|
||||
# ── Phase 3: axiom audit (exact cone per certificate, inside Lean) ───────────
|
||||
echo "=== Phase 3: axiom audit (exact cone per certificate — inside Lean) ==="
|
||||
cd "$AENEAS_LEAN"
|
||||
AUD="$HERE/Proofs/.audit.lean"
|
||||
{ echo "import Proofs.ChainSpec"; echo "import Proofs.WotsSpec"
|
||||
echo "import Proofs.XmssSpec"; echo "import Proofs.HtSpec"
|
||||
echo "import Proofs.ForsInnerSpec"; echo "import Proofs.ForsOuterSpec"; echo "import Proofs.InputPrepSpec"; echo "import Proofs.ApexSpec"
|
||||
for c in "${CERTS[@]}"; do echo "#print axioms $c"; done
|
||||
} > "$AUD"
|
||||
OUT=$(lake env bash -c "cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\" && LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' 'Proofs/.audit.lean'" 2>&1)
|
||||
rm -f "$AUD"
|
||||
# CRITICAL: Lean WRAPS long axiom cones across physical lines. A per-line parse
|
||||
# silently drops continuation-line axioms (fail-OPEN — external review round 1,
|
||||
# 2026-07-24, demonstrated a smuggled axiom on line 2 passing). FLATTEN the whole
|
||||
# report first, then extract each cert's complete bracketed cone with a
|
||||
# literal-string (regex-safe) scan and subset-check it. Missing/empty report =>
|
||||
# fail-CLOSED.
|
||||
FLAT=$(echo "$OUT" | tr '\n' ' ' | tr -s ' ')
|
||||
fail=0
|
||||
for c in "${CERTS[@]}"; do
|
||||
marker="'$c' depends on axioms: ["
|
||||
if ! grep -qF "$marker" <<<"$FLAT"; then
|
||||
echo " ✗ $c — no axiom report (fail-closed)"; fail=1; continue
|
||||
fi
|
||||
# full cone between this cert's '[' and the next ']' (literal index, not regex)
|
||||
cone=$(awk -v m="$marker" '{ i=index($0,m); if(i>0){ r=substr($0,i+length(m)); j=index(r,"]"); if(j>0) print substr(r,1,j-1) } }' <<<"$FLAT")
|
||||
bad=$(echo "$cone" | tr ',' '\n' | sed 's/^ *//;s/ *$//' | while read -r ax; do
|
||||
[ -z "$ax" ] && continue
|
||||
case " propext Classical.choice Quot.sound verify_mono.oracle.f verify_mono.oracle.h verify_mono.oracle.t_l verify_mono.oracle.t_len verify_mono.oracle.h_msg " in
|
||||
*" $ax "*) ;; *) echo "$ax" ;;
|
||||
esac
|
||||
done)
|
||||
if [ -n "$bad" ]; then echo " ✗ $c — DISALLOWED axioms: $(echo $bad | tr '\n' ' ')"; fail=1
|
||||
else echo " ✓ $c cone ⊆ allowed ($(echo "$cone" | tr ',' '\n' | grep -c .) axioms audited)"; fi
|
||||
done
|
||||
[ "$fail" = 0 ] || { echo "AXIOM AUDIT FAILED"; exit 1; }
|
||||
# Proofs/Audit.lean reads each cert's cone from the kernel (collectAxioms) and
|
||||
# asserts SET EQUALITY against its expected boundary. Compiling it IS the audit:
|
||||
# any mismatch throws → non-zero exit. We additionally require the explicit
|
||||
# PASSED line, so a build that somehow exits 0 without running the audit still
|
||||
# fails closed.
|
||||
AUD_OUT=$(lake env bash -c "cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD/gen:\$PWD\" && LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' 'Proofs/Audit.lean'" 2>&1) || {
|
||||
echo "$AUD_OUT" | sed 's/^/ /'
|
||||
echo "AXIOM AUDIT FAILED (Audit.lean did not compile — cone mismatch, missing cert, or sham)"; exit 1; }
|
||||
if ! grep -qF "exact-cone audit PASSED" <<<"$AUD_OUT"; then
|
||||
echo "$AUD_OUT" | sed 's/^/ /'
|
||||
echo "AXIOM AUDIT FAILED (no PASSED line — fail-closed)"; exit 1
|
||||
fi
|
||||
echo " ✓ exact-cone audit PASSED: each of the ${#CERTS[@]} certificate cones == its expected boundary set"
|
||||
|
||||
echo
|
||||
echo "ALL GREEN — model compiles, proofs compile, every certificate cone is"
|
||||
echo "the three kernel axioms plus (at most) the SHA-2 hash oracles."
|
||||
echo "ALL GREEN — model compiles, proofs compile, and every certificate cone"
|
||||
echo "equals EXACTLY the three kernel axioms plus its documented SHA-2 oracles."
|
||||
echo "Certificates proven: ${CERTS[*]}"
|
||||
|
|
|
|||
|
|
@ -9,20 +9,49 @@
|
|||
#
|
||||
# Rust --charon--> SlhVerify.llbc --aeneas--> gen/SlhVerify/*.lean
|
||||
#
|
||||
# REPRODUCIBILITY (external review round 2, 2026-07-24): this script now
|
||||
# REFUSES to extract from a source tree that is not at the pinned commit or
|
||||
# is dirty (a wrong/uncommitted source would silently produce a different
|
||||
# model). The full pin set (source + charon + aeneas + lean + ocaml) is in
|
||||
# verification/PROVENANCE.json; re-running this against the pinned tree
|
||||
# reproduces gen/SlhVerify/{Types,Funs}.lean byte-identically.
|
||||
#
|
||||
# HISTORY (gate-0 finding, resolved 2026-07-22): upstream models the hash
|
||||
# family as `crate::hashers::Hashers`, a struct of plain function pointers,
|
||||
# which Aeneas cannot translate. The compat patch in fips205-source
|
||||
# (>= 2d89ee3) provides the additive monomorphic verify_mono module whose
|
||||
# hash suite is reached through named free functions — this script roots
|
||||
# there, and charon + aeneas both exit 0. Regeneration is byte-identical
|
||||
# (verified against the committed gen/ during the 2026-07-22 audit).
|
||||
# which Aeneas cannot translate. The compat patch in fips205-source provides
|
||||
# the additive monomorphic verify_mono module whose hash suite is reached
|
||||
# through named free functions — this script roots there.
|
||||
#
|
||||
# Usage: ./extract.sh
|
||||
# Usage: ./extract.sh [PATH_TO_fips205-source]
|
||||
# (default: ~/GitClone/FormalVerification/sources/fips205-source)
|
||||
# Override the required commit only for a deliberate re-pin:
|
||||
# EXPECTED_SRC_COMMIT=<full-sha> ./extract.sh [PATH]
|
||||
set -euo pipefail
|
||||
|
||||
source ~/aeneas-toolchain/env.sh
|
||||
HERE="$(cd "$(dirname "$0")" && pwd)"
|
||||
CRATE=~/GitClone/FormalVerification/sources/fips205-source
|
||||
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}"
|
||||
|
||||
# ── 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; }
|
||||
GOT_COMMIT="$(git -C "$CRATE" rev-parse HEAD)"
|
||||
if [ "$GOT_COMMIT" != "$EXPECTED_SRC_COMMIT" ]; then
|
||||
echo "ERROR: source is at ${GOT_COMMIT:0:12}, but this repo is pinned to" >&2
|
||||
echo " ${EXPECTED_SRC_COMMIT:0:12}. Check out the pin, or set" >&2
|
||||
echo " EXPECTED_SRC_COMMIT=<sha> for a deliberate re-pin." >&2
|
||||
exit 3
|
||||
fi
|
||||
if [ -n "$(git -C "$CRATE" status --porcelain)" ]; then
|
||||
echo "ERROR: source tree at '$CRATE' is dirty. Extraction must run against" >&2
|
||||
echo " a clean, committed tree so the model is reproducible." >&2
|
||||
git -C "$CRATE" status --porcelain | sed 's/^/ /' >&2
|
||||
exit 4
|
||||
fi
|
||||
echo "[0/2] provenance OK: fips205-source @ ${EXPECTED_SRC_COMMIT:0:12} (clean)"
|
||||
|
||||
echo "[1/2] charon: Rust -> LLBC (monomorphic SHA2-128s verify cone;"
|
||||
echo " crate::verify_mono::oracle is the opaque SHA-2 boundary)"
|
||||
|
|
|
|||
Loading…
Reference in a new issue