diff --git a/ATTESTATION-BASIS.md b/ATTESTATION-BASIS.md index 8d4d47b..8da93ec 100644 --- a/ATTESTATION-BASIS.md +++ b/ATTESTATION-BASIS.md @@ -86,8 +86,11 @@ Not performed by any reviewer: `verification/extract.sh`. See condition 9. > 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 +> obtains the two EXTRACTION-GENERATED hashes in `model_integrity_sha256` +> (`Types.lean` and `Funs.lean` — the other two entries, `TypesExternal.lean` +> and `FunsExternal.lean`, are HAND-MAINTAINED and are not regenerated by +> `extract.sh`; they are separately byte-pinned), the correspondence between +> `fips205-source@a3ce8e8` 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 diff --git a/README.md b/README.md index c766dd1..0c571ec 100644 --- a/README.md +++ b/README.md @@ -215,9 +215,13 @@ same boundary. 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 + The current snapshot head is **`a3ce8e8`** — the NIST ACVP SHA2-128s sigVer + vectors plus an expanded differential bridge. That commit is TEST-ONLY: no + verify-path function changed, and re-running `extract.sh` against it + reproduces the two Aeneas-generated model files byte-identically. Its + lineage is `bea1051` (de-plumbing round 2) → `797b4ef` (the round-2 + reproducibility commit: committed `Cargo.lock` + pinned + `rust-toolchain.toml`) → `a3ce8e8`; 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 @@ -292,7 +296,7 @@ this repository was created: one the differential test compares against — is itself patched relative to upstream `30bac08`. `src/wots.rs` was never modified by any patch commit (an earlier revision of this README wrongly named it). See the snapshot history - at head `797b4ef` and TRUSTED-BASE.md item 7. + at head `a3ce8e8` and TRUSTED-BASE.md item 7. ## What is claimed (the button is green) diff --git a/TRUSTED-BASE.md b/TRUSTED-BASE.md index a3da70c..7cdee30 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 `3153988`) are + de-plumbing round 2 at `bea1051`; current snapshot head `a3ce8e8`) 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 diff --git a/verification/RECORDED-RUN.md b/verification/RECORDED-RUN.md index b515704..fa72efa 100644 --- a/verification/RECORDED-RUN.md +++ b/verification/RECORDED-RUN.md @@ -1,5 +1,15 @@ # Recorded clean run — check.sh + independent cone dump +> **HISTORICAL RECORD — read the pin below, not as the current one.** This +> captures a run that really happened on 2026-07-24 against fips205-source +> `797b4ef`. The CURRENT machine-enforced source pin is `a3ce8e8` (see +> PROVENANCE.json). The revision named throughout this file is deliberately +> left as it was: this is a record of what ran, and editing the identity of a +> past run to match today's pin would be falsifying the record rather than +> correcting it. Round-8 review (GPT-5.6) flagged that the pin appeared in no +> markdown file; the fix is to name it here and correct the CLAIMS elsewhere. + + 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). @@ -142,14 +152,146 @@ Certificates proven: fips205.chain_free_loop_eq fips205.wots_loop1_eq fips205.xm hand-maintained TypesExternal.lean / FunsExternal.lean are NOT overwritten once they exist) [Info ] Imported: SlhVerify.llbc -[?25lApplied prepasses: [------------------------------------------------] 0/142 ⠋ Applied prepasses: [------------------------------------------------] 1/142 ⠋ Applied prepasses: [###---------------------------------------------] 11/142 ⠋ Applied prepasses: [#################-------------------------------] 52/142 ⠙ Applied prepasses: [########################################--------] 120/142 ⠙ Applied prepasses: [################################################] 142/142 ✔️ -[?25h[?25lTranslated globals: [-------------------------------------------------] 0/10 ⠋ Translated globals: [#################################################] 10/10 ✔️ -[?25h[?25lTranslated opaque functions: [----------------------------------------] 0/76 ⠋ Translated opaque functions: [########################################] 76/76 ✔️ -[?25h[?25lTranslated transparent functions: [-----------------------------------] 0/42 ⠋ Translated transparent functions: [-----------------------------------] 1/42 ⠙ Translated transparent functions: [#######----------------------------] 9/42 ⠹ Translated transparent functions: [########---------------------------] 10/42 ⠹ Translated transparent functions: [##########-------------------------] 12/42 ⠹ Translated transparent functions: [##########-------------------------] 13/42 ⠹ Translated transparent functions: [###########------------------------] 14/42 ⠸ Translated transparent functions: [############-----------------------] 15/42 ⠸ Translated transparent functions: [##############---------------------] 17/42 ⠸ Translated transparent functions: [###############--------------------] 19/42 ⠸ Translated transparent functions: [################-------------------] 20/42 ⠼ Translated transparent functions: [##################-----------------] 22/42 ⠼ Translated transparent functions: [####################---------------] 24/42 ⠼ Translated transparent functions: [#####################--------------] 26/42 ⠴ Translated transparent functions: [######################-------------] 27/42 ⠴ Translated transparent functions: [#######################------------] 28/42 ⠦ Translated transparent functions: [########################-----------] 29/42 ⠦ Translated transparent functions: [#########################----------] 30/42 ⠦ Translated transparent functions: [#########################----------] 31/42 ⠧ Translated transparent functions: [###########################--------] 33/42 ⠇ Translated transparent functions: [#############################------] 35/42 ⠏ Translated transparent functions: [##############################-----] 36/42 ⠏ Translated transparent functions: [##############################-----] 37/42 ⠋ Translated transparent functions: [###############################----] 38/42 ⠙ Translated transparent functions: [################################---] 39/42 ⠹ Translated transparent functions: [#################################--] 40/42 ⠸ Translated transparent functions: [##################################-] 41/42 ⠸ Translated transparent functions: [###################################] 42/42 ⠼ Translated transparent functions: [###################################] 42/42 ✔️ -[?25h[?25lTranslated trait declarations: [--------------------------------------] 0/33 ⠋ Translated trait declarations: [##############------------------------] 13/33 ✔️ -[?25h[?25lTranslated trait impls: [---------------------------------------------] 0/50 ⠋ Translated trait impls: [######################-----------------------] 25/50 ✔️ -[?25h[?25lPost-processed translated opaque functions: [-------------------------] 0/76 ⠋ Post-processed translated opaque functions: [-------------------------] 1/76 ⠙ Post-processed translated opaque functions: [#########################] 76/76 ✔️ -[?25h[?25lPost-processed translated transparent functions: [--------------------] 0/42 ⠋ Post-processed translated transparent functions: [--------------------] 1/42 ⠙ Post-processed translated transparent functions: [###-----------------] 7/42 ⠙ Post-processed translated transparent functions: [####----------------] 9/42 ⠙ Post-processed translated transparent functions: [####----------------] 10/42 ⠹ Post-processed translated transparent functions: [#####---------------] 11/42 ⠹ Post-processed translated transparent functions: [#####---------------] 12/42 ⠸ Post-processed translated transparent functions: [######--------------] 13/42 ⠸ Post-processed translated transparent functions: [######--------------] 14/42 ⠸ Post-processed translated transparent functions: [#######-------------] 15/42 ⠼ Post-processed translated transparent functions: [#######-------------] 16/42 ⠼ Post-processed translated transparent functions: [########------------] 17/42 ⠼ Post-processed translated transparent functions: [#########-----------] 19/42 ⠴ Post-processed translated transparent functions: [#########-----------] 20/42 ⠴ Post-processed translated transparent functions: [##########----------] 21/42 ⠴ Post-processed translated transparent functions: [##########----------] 22/42 ⠦ Post-processed translated transparent functions: [##########----------] 23/42 ⠦ Post-processed translated transparent functions: [###########---------] 25/42 ⠦ Post-processed translated transparent functions: [############--------] 26/42 ⠧ Post-processed translated transparent functions: [############--------] 27/42 ⠧ Post-processed translated transparent functions: [#############-------] 28/42 ⠧ Post-processed translated transparent functions: [##############------] 30/42 ⠇ Post-processed translated transparent functions: [###############-----] 32/42 ⠇ Post-processed translated transparent functions: [###############-----] 33/42 ⠏ Post-processed translated transparent functions: [################----] 34/42 ⠏ Post-processed translated transparent functions: [#################---] 37/42 ⠋ Post-processed translated transparent functions: [##################--] 38/42 ⠋ Post-processed translated transparent functions: [##################--] 39/42 ⠙ Post-processed translated transparent functions: [###################-] 40/42 ⠹ Post-processed translated transparent functions: [###################-] 41/42 ⠸ Post-processed translated transparent functions: [####################] 42/42 ⠼ Post-processed translated transparent functions: [####################] 42/42 ✔️ +[?25lApplied prepasses: [------------------------------------------------] 0/142 ⠋ + +Applied prepasses: [------------------------------------------------] 1/142 ⠋ + +Applied prepasses: [###---------------------------------------------] 11/142 ⠋ + +Applied prepasses: [#################-------------------------------] 52/142 ⠙ + +Applied prepasses: [########################################--------] 120/142 ⠙ +Applied prepasses: [################################################] 142/142 ✔️ +[?25h[?25lTranslated globals: [-------------------------------------------------] 0/10 ⠋ +Translated globals: [#################################################] 10/10 ✔️ +[?25h[?25lTranslated opaque functions: [----------------------------------------] 0/76 ⠋ +Translated opaque functions: [########################################] 76/76 ✔️ +[?25h[?25lTranslated transparent functions: [-----------------------------------] 0/42 ⠋ + +Translated transparent functions: [-----------------------------------] 1/42 ⠙ + +Translated transparent functions: [#######----------------------------] 9/42 ⠹ + +Translated transparent functions: [########---------------------------] 10/42 ⠹ + +Translated transparent functions: [##########-------------------------] 12/42 ⠹ + +Translated transparent functions: [##########-------------------------] 13/42 ⠹ + +Translated transparent functions: [###########------------------------] 14/42 ⠸ + +Translated transparent functions: [############-----------------------] 15/42 ⠸ + +Translated transparent functions: [##############---------------------] 17/42 ⠸ + +Translated transparent functions: [###############--------------------] 19/42 ⠸ + +Translated transparent functions: [################-------------------] 20/42 ⠼ + +Translated transparent functions: [##################-----------------] 22/42 ⠼ + +Translated transparent functions: [####################---------------] 24/42 ⠼ + +Translated transparent functions: [#####################--------------] 26/42 ⠴ + +Translated transparent functions: [######################-------------] 27/42 ⠴ + +Translated transparent functions: [#######################------------] 28/42 ⠦ + +Translated transparent functions: [########################-----------] 29/42 ⠦ + +Translated transparent functions: [#########################----------] 30/42 ⠦ + +Translated transparent functions: [#########################----------] 31/42 ⠧ + +Translated transparent functions: [###########################--------] 33/42 ⠇ + +Translated transparent functions: [#############################------] 35/42 ⠏ + +Translated transparent functions: [##############################-----] 36/42 ⠏ + +Translated transparent functions: [##############################-----] 37/42 ⠋ + +Translated transparent functions: [###############################----] 38/42 ⠙ + +Translated transparent functions: [################################---] 39/42 ⠹ + +Translated transparent functions: [#################################--] 40/42 ⠸ + +Translated transparent functions: [##################################-] 41/42 ⠸ + +Translated transparent functions: [###################################] 42/42 ⠼ +Translated transparent functions: [###################################] 42/42 ✔️ +[?25h[?25lTranslated trait declarations: [--------------------------------------] 0/33 ⠋ +Translated trait declarations: [##############------------------------] 13/33 ✔️ +[?25h[?25lTranslated trait impls: [---------------------------------------------] 0/50 ⠋ +Translated trait impls: [######################-----------------------] 25/50 ✔️ +[?25h[?25lPost-processed translated opaque functions: [-------------------------] 0/76 ⠋ + +Post-processed translated opaque functions: [-------------------------] 1/76 ⠙ +Post-processed translated opaque functions: [#########################] 76/76 ✔️ +[?25h[?25lPost-processed translated transparent functions: [--------------------] 0/42 ⠋ + +Post-processed translated transparent functions: [--------------------] 1/42 ⠙ + +Post-processed translated transparent functions: [###-----------------] 7/42 ⠙ + +Post-processed translated transparent functions: [####----------------] 9/42 ⠙ + +Post-processed translated transparent functions: [####----------------] 10/42 ⠹ + +Post-processed translated transparent functions: [#####---------------] 11/42 ⠹ + +Post-processed translated transparent functions: [#####---------------] 12/42 ⠸ + +Post-processed translated transparent functions: [######--------------] 13/42 ⠸ + +Post-processed translated transparent functions: [######--------------] 14/42 ⠸ + +Post-processed translated transparent functions: [#######-------------] 15/42 ⠼ + +Post-processed translated transparent functions: [#######-------------] 16/42 ⠼ + +Post-processed translated transparent functions: [########------------] 17/42 ⠼ + +Post-processed translated transparent functions: [#########-----------] 19/42 ⠴ + +Post-processed translated transparent functions: [#########-----------] 20/42 ⠴ + +Post-processed translated transparent functions: [##########----------] 21/42 ⠴ + +Post-processed translated transparent functions: [##########----------] 22/42 ⠦ + +Post-processed translated transparent functions: [##########----------] 23/42 ⠦ + +Post-processed translated transparent functions: [###########---------] 25/42 ⠦ + +Post-processed translated transparent functions: [############--------] 26/42 ⠧ + +Post-processed translated transparent functions: [############--------] 27/42 ⠧ + +Post-processed translated transparent functions: [#############-------] 28/42 ⠧ + +Post-processed translated transparent functions: [##############------] 30/42 ⠇ + +Post-processed translated transparent functions: [###############-----] 32/42 ⠇ + +Post-processed translated transparent functions: [###############-----] 33/42 ⠏ + +Post-processed translated transparent functions: [################----] 34/42 ⠏ + +Post-processed translated transparent functions: [#################---] 37/42 ⠋ + +Post-processed translated transparent functions: [##################--] 38/42 ⠋ + +Post-processed translated transparent functions: [##################--] 39/42 ⠙ + +Post-processed translated transparent functions: [###################-] 40/42 ⠹ + +Post-processed translated transparent functions: [###################-] 41/42 ⠸ + +Post-processed translated transparent functions: [####################] 42/42 ⠼ +Post-processed translated transparent functions: [####################] 42/42 ✔️ [?25h[Info ] Generated: gen/SlhVerify/Types.lean [Info ] Generated: gen/SlhVerify/FunsExternal_Template.lean [Info ] Generated: gen/SlhVerify/Funs.lean