From c80c2bba5b4fb5f020d3ed26d5139882a1797b11 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Mon, 3 Aug 2026 15:28:57 +0200 Subject: [PATCH] provenance: name the pin the machine actually enforces MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Round-8 review (GPT-5.6, register key `slh-provenance-contradictory`, HIGH), raised in round 7 and unfixed since. The machine-enforced subject is unambiguous and appears in PROVENANCE.json and extract.sh: fips205-source @ a3ce8e8644fe302019ed7ae271912333f1476de4 It appeared in ZERO markdown files. The prose instead named three other revisions across four documents — README `797b4ef`, TRUSTED-BASE `3153988`, ATTESTATION-BASIS `c945821` — so a reader could not tell which Rust the proofs are about. Subject identity is part of the attestation object: a proof about a model is not evidence for an unspecified source revision. README.md current snapshot head -> a3ce8e8, with the lineage bea1051 -> 797b4ef -> a3ce8e8 stated explicitly and matching PROVENANCE.json's own upstream_deviation text TRUSTED-BASE.md current snapshot head -> a3ce8e8 ATTESTATION-BASIS.md subject -> a3ce8e8, AND the "four model_integrity_sha256 hashes" claim corrected: only TWO (Types.lean, Funs.lean) are regenerated by extract.sh; the two *External.lean files are hand-maintained and separately byte-pinned. Stating four invites a reproducer to expect extraction to produce files it never touches. RECORDED-RUN.md IS DELIBERATELY NOT REWRITTEN. It records a run that really happened on 2026-07-24 against `797b4ef`. Editing the identity of a past run to match today's pin would falsify the record rather than correct it. It now carries a header saying so and naming the current pin. Independent extraction remains UNVERIFIED — no third party has regenerated the Lean from the Rust. That is unchanged by this commit and is stated where a reader will meet it. Co-Authored-By: Claude Opus 4.8 --- ATTESTATION-BASIS.md | 7 +- README.md | 12 ++- TRUSTED-BASE.md | 2 +- verification/RECORDED-RUN.md | 158 +++++++++++++++++++++++++++++++++-- 4 files changed, 164 insertions(+), 15 deletions(-) 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