.gitignore

@@ -1,10 +1,5 @@
 *.olean
 target/
 .lake/
-# *_Template.lean is NO LONGER ignored: it is Aeneas's own statement of what
+*_Template.lean
-# the extraction needs from outside, and it is the only artifact against which
+SlhVerify.llbc
-# "does the model ANSWER the extraction" can be asked. Committed and pinned.
-# SlhVerify.llbc is NO LONGER ignored. It is the intermediate Charon produces
-# and Aeneas consumes, and committing it is what makes the LLBC->Lean half of
-# extraction independently re-runnable. Round-9 review (GPT-5.6) found
-# TRUSTED-BASE claiming it was committed while .gitignore excluded it.

ATTESTATION-BASIS.md

@@ -86,11 +86,8 @@ 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 two EXTRACTION-GENERATED hashes in `model_integrity_sha256`
+>    obtains the four `model_integrity_sha256` hashes, the correspondence between
->    (`Types.lean` and `Funs.lean` — the other two entries, `TypesExternal.lean`
+>    `fips205-source@c945821` and `verification/gen/SlhVerify/*.lean` rests on the
->    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

README.md

@@ -5,13 +5,12 @@ path**, extracted from a pure-Rust implementation into Lean 4 via
 Charon/Aeneas — the same pipeline, discipline, and honesty rules as the
 four ed25519 campaigns (`dalek/anza/risc0/betrusted-ed25519-verified`).
 
-## STATUS: eleven certificates over the extracted verify model (external review rounds 1–9 applied)
+## STATUS: eleven certificates over the extracted verify model (external review rounds 1–6 applied)
 
 `verification/check.sh` is **green** (exit 0): the model compiles, the proofs
-compile, and the audit passes. It binds **seven** things, each added because an
+compile, and the audit passes. The audit runs **inside Lean**
-external reviewer *demonstrated* the button going green without it. Three are
+(`verification/Proofs/Audit.lean`) and binds four things, each added because an
-checked **inside Lean** by `verification/Proofs/Audit.lean`; the other four are
+external reviewer *demonstrated* the button going green without it:
-separate phases that deliberately do **not** rely on that file:
 
 - **axiom cones** — each certificate's cone is read from the kernel via
   `collectAxioms` and must equal its expected set EXACTLY, so an added axiom
@@ -27,41 +26,9 @@ separate phases that deliberately do **not** rely on that file:
   *body*. Round 5 showed why the last part is essential: redefining a fold to
   *be* the extracted loop left every earlier fingerprint bit-identical while the
   certificate degenerated to "the loop equals the loop";
-- **bytes** — Phase 0 sha256-pins the five model files and the compiler harness
+- **bytes** — Phase 0 sha256-pins the four model files and the compiler harness
   `lean-guard`, purges stale `.olean`s, and forbids stray `.lean` files, so the
-  verdict depends on committed bytes rather than build-directory state;
+  verdict depends on committed bytes rather than build-directory state.
-- **correspondence** (Phase 0d) — byte pins say the model did not *change*; they
-  say nothing about whether it *answers the extraction*. Aeneas states what the
-  extracted Rust needs from outside in `FunsExternal_Template.lean`, and every
-  such name must be answered by the hand-written model or by a real definition
-  in the corpus. An **extra axiom** in the model — an assumption no template
-  asks for — fails the button rather than passing as a silent row. This
-  repository previously deleted the template on every run, which is exactly why
-  it shipped a Template/model pair with no correspondence check at all
-  (round-8 estate review, GPT-5.6);
-- **the object files** (Phase 3b) — a second, independently implemented axiom
-  gate that reads the compiled `.olean`s via `readModuleData` instead of the
-  elaboration-time environment. Phase 3's view has a demonstrated blind spot: a
-  declaration made *after* the command that performs the walk sits in the object
-  file but not in the environment while the walk runs, so the walker reports "no
-  axiom" and is telling the truth about what it could see. Verified here by
-  planting `axiom cheat : ∀ (P : Prop), P` after the audit command — Phase 3
-  passed it, Phase 3b rejected it.
-- **which declarations exist** (Phase 3c) — the checks above prove each
-  certificate's cone is exact and that nothing in scope carries a disallowed
-  axiom. They do not pin WHICH declarations exist: a new one that happens to be
-  clean, and a silently vanished one, both pass. `inventory-allowlist.txt` (265
-  rows) and `driver-allowlist.txt` (35 rows) pin the corpus and the audit
-  instrument's own surface as `module|name|kind|cone`, diffed in **both**
-  directions — UNCLASSIFIED for a declaration no row describes, STALE for a row
-  with no declaration behind it. The instrument surface carries cones because
-  enumeration is not audit: a claim planted in an instrument is counted and then
-  examined by nothing if its row has no cone and no allowlist covers it.
-  Finally the **accounting identity**, as set containment rather than
-  arithmetic: every constant the kernel holds must appear in one of the two
-  walks — `kernel 300 = corpus 265 + instrument 35`, residual none. A residual
-  that has to be explained is a fudge term waiting to absorb the next real
-  finding.
 
 What the button still does **not** bind is stated plainly in
 [TRUSTED-BASE.md](TRUSTED-BASE.md) item 11 — `check.sh` itself, the toolchain
@@ -248,15 +215,9 @@ 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 **`a3ce8e8`** — the NIST ACVP SHA2-128s sigVer
+  The current snapshot head is **`797b4ef`** (the round-2 reproducibility
-  vectors plus an expanded differential bridge. That commit is TEST-ONLY: no
+  commit — committed `Cargo.lock` + pinned `rust-toolchain.toml` — on top of
-  verify-path function changed, and re-running `extract.sh` against it
+  de-plumbing round 2, `bea1051`); the model in this repo is extracted from
-  reproduces the two Aeneas-generated model files byte-identically. Its
-  lineage is `bea1051` (de-plumbing round 2) → `797b4ef` → `3153988` (NIST
-  ACVP vectors + randomized bridge) → `c945821` (vectors made re-derivable) →
-  `a3ce8e8` (extract-script wording); `797b4ef` is (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
@@ -331,7 +292,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 `a3ce8e8` and TRUSTED-BASE.md item 7.
+  at head `797b4ef` and TRUSTED-BASE.md item 7.
 
 ## What is claimed (the button is green)
 
@@ -362,10 +323,7 @@ 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 **in its second stage only**
+runs on stable Rust. Extraction is reproducible: the
-(see TRUSTED-BASE item 3: the committed `.llbc` lets anyone re-run Aeneas and
-reproduce the model byte-identically; re-running Charon against the Rust
-requires charon and has never been done by anyone but the author): 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

TRUSTED-BASE.md

@@ -20,43 +20,6 @@ proceeds and is part of every claim.
    toolchain) are trusted to preserve semantics from Rust (MIR) to the
    Lean model. Divergence between rustc's semantics and the extracted
    model is trusted base.
-
-   **What is now reproducible, and what is not.** Extraction is two steps:
-   `Rust --charon--> SlhVerify.llbc --aeneas--> gen/SlhVerify/*.lean`.
-
-   The `.llbc` is committed **as of 2026-08-03** and byte-pinned in
-   `generated_artifacts_sha256`, which `check.sh` Phase 0 now verifies. So the
-   SECOND step can be re-run by anyone with the pinned Aeneas and this
-   repository, and doing so reproduces `Types.lean` and `Funs.lean`
-   byte-identically.
-
-   THE FIRST STEP CANNOT BE. It requires charon, which no reviewer has yet had
-   available, and this repository ships no charon output anyone can check
-   against — the committed `.llbc` IS that output, so verifying it against
-   itself establishes nothing. What the committed `.llbc` gives a reader is
-   this and only this: the Lean model in `gen/` is the faithful Aeneas image of
-   THAT intermediate. Whether that intermediate is the faithful Charon image of
-   `fips205-source@a3ce8e8` rests on the author's attestation alone, and
-   continues to do so until a third party runs Charon. **Do not read the second
-   half as evidence for the first.**
-
-   This paragraph previously said the `.llbc` was committed while `.gitignore`
-   excluded it — round-9 review (GPT-5.6) — so the claim was false for every
-   reader and true only on the author's disk. Chasing it found the larger
-   defect: `generated_artifacts_sha256` was read by nothing, and its `.llbc`
-   entry had been stale since review round 2, naming an artifact that did not
-   produce the committed model.
-
-3b. **The correspondence check is textual, not a Lean query.** Phase 0d parses
-   `FunsExternal_Template.lean` and the hand-written model as SOURCE TEXT. It
-   establishes that every external the extraction names is answered by a
-   declaration of the right name in the pinned model, and that the model
-   declares no axiom the extraction never asked for. It does **not** ask Lean
-   how those names resolve at elaboration — the four ed25519 repositories have
-   a second, semantic phase for that; this one does not. All eleven externals
-   here are answered by the model itself (none by the proven corpus), which is
-   the narrow case where the textual answer and the semantic one coincide, but
-   that is a property of today's corpus and not a guarantee of the check.
 4. **The Lean kernel and its three axioms**
    (`propext, Classical.choice, Quot.sound`).
 5. **Build correspondence.** No reproducible-builds claim: the proof is
@@ -68,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 `a3ce8e8`) 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

verification/MODEL-CORRESPONDENCE.txt

@@ -1,12 +0,0 @@
-SlhVerify/FunsExternal|Array.Insts.ZeroizeZeroize.zeroize|MODEL
-SlhVerify/FunsExternal|U32.Insts.CoreIterRangeStep.backward_checked|MODEL
-SlhVerify/FunsExternal|U32.Insts.CoreIterRangeStep.forward_checked|MODEL
-SlhVerify/FunsExternal|U32.Insts.CoreIterRangeStep.steps_between|MODEL
-SlhVerify/FunsExternal|verify_mono.oracle.f|MODEL
-SlhVerify/FunsExternal|verify_mono.oracle.h|MODEL
-SlhVerify/FunsExternal|verify_mono.oracle.h_msg|MODEL
-SlhVerify/FunsExternal|verify_mono.oracle.t_l|MODEL
-SlhVerify/FunsExternal|verify_mono.oracle.t_len|MODEL
-SlhVerify/FunsExternal|zeroize.Zeroize.Blanket.zeroize|MODEL
-SlhVerify/FunsExternal|zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop|MODEL
-CORRESPONDENCE-COUNT|11

verification/PROVENANCE.json

@@ -28,7 +28,7 @@
     "aeneas": "aeneas -backend lean -split-files -subdir SlhVerify -dest gen SlhVerify.llbc"
   },
   "generated_artifacts_sha256": {
-    "SlhVerify.llbc": "69666ddc43a4d5e02ca8eaa64eb740f8849eac64e0cd9df76506ab4f68f2af55",
+    "SlhVerify.llbc": "d8ec0b00593eee1778bc4cc0cc1801fb6415bb294425f01384434849c6443f58",
     "gen/SlhVerify/Types.lean": "db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384",
     "gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f"
   },
@@ -42,21 +42,15 @@
     "gen/SlhVerify/TypesExternal.lean": "2988c04c5fc8c634aff4d9bd13604b8a47e677daa1f45e8f4f321368606cdd0a",
     "gen/SlhVerify/FunsExternal.lean": "5efe551c35969c9da28b2f3eaed4a6a67c410c62a1926aab390e3abf010390f8",
     "gen/SlhVerify/Types.lean": "db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384",
-    "gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f",
+    "gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f"
-    "gen/SlhVerify/FunsExternal_Template.lean": "b4f9c6ecdbd55599bc4d35720fff1accc71475b5702410b5a0666456439a4042"
   },
   "harness_integrity_sha256": {
     "_comment": "The harness is part of the trusted computing base and its membership is now SELF-DERIVING: check.sh requires every executable file in verification/ to appear here (round-8 review \u2014 a hardcoded list was itself a second thing to keep in sync), plus Proofs/Audit.lean, which is not executable but computes the digest it is judged by. check.sh itself is excluded: it cannot pin itself, and is disclosed as trusted-unbound in TRUSTED-BASE.md item 11. Pinning check-selftest.sh matters beyond the button: it is the only artifact demonstrating the gates work, and its assertions have been defective in four consecutive rounds, so weakening it is now a reviewable pin rotation rather than an unnoticed edit.",
     "lean-guard": "690d861cfd81b327604ffd5ef85599ee01b2bcd943907f5b71b8b6f99bad418f",
-    "Proofs/Audit.lean": "3a1540187622c47ee2de4bf1dd2379fbbabf4a3d6ec902f2b602dcf486731691",
+    "Proofs/Audit.lean": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e",
     "check-selftest.sh": "c6811482e25ae6e1fffa6ca50e60541e8e609a70c951db6bec4d2d39a4849e9a",
     "drill.sh": "915cf9310fa168c14ca5d76a1b84fd3b19acdfef9dfd0b03b01b19883548719e",
-    "extract.sh": "01cff43c350ed8eaac0e65ccd7599b68fef47c9434cdb5ad01c92d2127a3bbe9",
+    "extract.sh": "01cff43c350ed8eaac0e65ccd7599b68fef47c9434cdb5ad01c92d2127a3bbe9"
-    "model-correspondence.py": "1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427",
-    "MODEL-CORRESPONDENCE.txt": "77bd374a60152689edcb3350c2a2547c6aaad192629e39e86d8548d2bad3f748",
-    "inventory_gate.sh": "3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e",
-    "inventory-allowlist.txt": "6b27fb410f61d0d6e0d17f9089a5dc1f53027bec507c6c7c180554c5c8f40ede",
-    "driver-allowlist.txt": "5f9a4167068407ae5e31ec0c7c55d78af455a7ed7f1913b79912f6ae50c13686"
   },
   "audit_gate": "verification/Proofs/Audit.lean \u2014 in-Lean audit (round 5). Per certificate: exact cone equality (collectAxioms) + elaborated-statement check. Enumeration: EVERY declaration kind (def/theorem/opaque/axiom \u2014 round 4 matched theorems only, so a `def : False` passed) in the eight certificate modules AND in Audit.lean itself (the auditor is not exempt). Binding digest: check.sh binds to the SHA-256 of a canonical AUDIT-MANIFEST block covering the POLICY constants (allowedBoundary + certModules \u2014 round-5 NEW-1: widening allowedBoundary previously re-opened the False-proof with the fingerprint byte-identical), every certificate's fully-elaborated statement, and every reachable specification definition's fully-elaborated BODY (round-5 NEW-2: redefining a reference fold to *be* the extracted loop previously left cone and fingerprint intact while the certificate degenerated to `loop = loop`). The 32-bit Expr.hash is retained only as a per-certificate diagnostic, not as the binding. Fail-closed; adversarially exercised by check-selftest.sh. check.sh Phase 0 additionally purges stale .olean files, forbids stray .lean outside gen/ and Proofs/, and pins model + harness bytes."
 }

verification/Proofs/Audit.lean

@@ -93,21 +93,6 @@ def manifest : List (Name × List Name × UInt64) :=
     (`fips205.base2b_outer_loop_eq,        kernel3,                                           324621577),
     (`fips205.slh_verify_128s_accepts_iff, kernel3 ++ [oracleF, oracleH, oracleTL, oracleTLen, oracleHMsg], 2489587792) ]
 
-/-- Declaration kind, in the vocabulary the estate's allowlists already use.
-    A KIND is part of the record because "the name is still there" and "the
-    thing behind the name is still the same kind of thing" are different
-    facts: a theorem quietly replaced by a `def` keeps its name and loses its
-    meaning. -/
-def kindOf : ConstantInfo → String
-  | .axiomInfo _  => "axiom"
-  | .thmInfo _    => "theorem"
-  | .opaqueInfo _ => "opaque"
-  | .defnInfo _   => "def"
-  | .quotInfo _   => "quot"
-  | .inductInfo _ => "inductive"
-  | .ctorInfo _   => "ctor"
-  | .recInfo _    => "rec"
-
 /-- Deterministic name ordering for the canonical serialization. -/
 def sortNames (l : List Name) : List Name :=
   ((l.map toString).toArray.qsort (· < ·)).toList.map (·.toName)
@@ -187,39 +172,18 @@ elab "auditCones" : command => do
   let manifestNames := manifest.map (·.1)
   let mut nEnum := 0
   let mut certsSeen : Array Name := #[]
-  let mut invRows : Array String := #[]
-  let mut drvRows : Array String := #[]
   for (nm, ci) in env.constants.toList do
     let scope : Option String :=
       match env.getModuleIdxFor? nm with
       | some idx =>
           let m := env.header.moduleNames[idx.toNat]!
           if certModules.contains m then some (toString m) else none
-      -- INTERNAL NAMES ARE NO LONGER EXEMPT. They were skipped here, which
+      | none => if nm.isInternal then none else some "Proofs.Audit (this file)"
-      -- was harmless while nothing compared this walk against the kernel's
-      -- view — and became a hole the moment it did: Phase 3b reads the object
-      -- files, which contain the compiler's auxiliaries, so exempting them
-      -- here would leave the accounting identity permanently short and force
-      -- it to be "explained" by a constant. A residual that has to be
-      -- explained away is the shape of the fudge term four-fork data refuted
-      -- in the ed25519 repos.
-      | none => some "Proofs.Audit"
     match scope with
     | none => pure ()
     | some where_ =>
       nEnum := nEnum + 1
       if manifestNames.contains nm then certsSeen := certsSeen.push nm
-      -- THE ROW. Same shape as the corpus walks in the ed25519 repositories:
-      -- module, name, kind, cone. The originating module is part of the record
-      -- because two modules may legitimately declare the same name, and keyed
-      -- on name alone one would be covered by the other's entry.
-      let rowCone := (← collectAxioms nm).toList
-      let rowKind := kindOf ci
-      let rowStr := s!"{where_}|{nm}|{rowKind}|{String.intercalate "," ((sortNames rowCone).map toString)}"
-      if where_ == "Proofs.Audit" then
-        drvRows := drvRows.push s!"DRV|{rowStr}"
-      else
-        invRows := invRows.push s!"INV|{rowStr}"
       match ci with
       | .axiomInfo _ =>
           -- the five oracle axioms live in gen/ (Phase-0 pinned); an axiom
@@ -268,13 +232,6 @@ elab "auditCones" : command => do
   -- check.sh prints the certificate list it gets from HERE, not from a hand-kept
   -- bash array (drill finding: the one authoritative claim string was the one
   -- thing nothing bound — adding a name to it printed a cert that never existed).
-  -- The two walks, emitted for check.sh to diff against committed allowlists in
-  -- BOTH directions. A trailer per walk, so a truncated or crashed emission can
-  -- never pass as an empty diff.
-  for r in invRows.qsort (· < ·) do IO.println r
-  IO.println s!"INV-COUNT|{invRows.size}"
-  for r in drvRows.qsort (· < ·) do IO.println r
-  IO.println s!"DRV-COUNT|{drvRows.size}"
   logInfo s!"CERTIFICATES: {String.intercalate " " (manifestNames.map toString)}"
   logInfo s!"exact-cone audit PASSED: {manifest.length} certificates (cones + statements), {specs.toList.length} specification constants pinned, {nEnum} declarations enumerated clean"
 

verification/RECORDED-RUN.md

@@ -1,15 +1,5 @@
 # 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).
@@ -152,146 +142,14 @@ 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 ⠋
+[?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 ✔️
-Applied prepasses:  [------------------------------------------------]   1/142 ⠋
+[?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 ✔️
-Applied prepasses:  [###---------------------------------------------]  11/142 ⠋
+[?25h[?25lTranslated trait declarations:  [--------------------------------------]  0/33 ⠋
Translated trait declarations:  [##############------------------------] 13/33 ✔️
-
+[?25h[?25lTranslated trait impls:  [---------------------------------------------]  0/50 ⠋
Translated trait impls:  [######################-----------------------] 25/50 ✔️
-Applied prepasses:  [#################-------------------------------]  52/142 ⠙
+[?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 ✔️
-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

verification/check.sh

@@ -5,14 +5,8 @@
 #
 #   Phase 0 — build hygiene + integrity: purge stale .olean (the verdict must
 #             depend on committed bytes, not untracked build state), forbid any
-#             .lean outside gen/ and Proofs/, and sha256-pin the five model files,
+#             .lean outside gen/ and Proofs/, and sha256-pin the four model files
-#             the committed SlhVerify.llbc, and the self-derived harness set
+#             AND the compiler harness `lean-guard` to PROVENANCE.json.
-#             (every executable here + Proofs/Audit.lean) to PROVENANCE.json.
-#   Phase 0d— template/model correspondence: every external Aeneas states the
-#             extracted Rust needs (FunsExternal_Template.lean, committed and
-#             pinned) must be answered by the hand-written model or by a real
-#             definition in the corpus. An EXTRA AXIOM in the model — an
-#             assumption no template asks for — is a failure, not a silent row.
 #   Phase 1 — compile the extracted Lean model (gen/SlhVerify).
 #   Phase 2 — compile the proof files (Proofs/).
 #   Phase 3 — the in-Lean audit (Proofs/Audit.lean): per certificate, the cone
@@ -23,18 +17,6 @@
 #             POLICY constants, every certificate STATEMENT, and every reachable
 #             SPECIFICATION DEFINITION BODY. Any mismatch → non-zero exit →
 #             fail-closed. No text parsing of axiom cones.
-#   Phase 3b— kernel-side axiom-declaration gate: reads the compiled OBJECT
-#             FILES (`readModuleData`) rather than the elaboration-time
-#             environment, and rejects any axiom declared under Proofs/. This is
-#             a SECOND, independently implemented gate on the same property,
-#             because Phase 3's view has a demonstrated blind spot: a
-#             declaration made after the command that performs the walk is in
-#             the object file but not in the environment while the walk runs.
-#             It runs after Phase 3 because Proofs/Audit.lean is compiled there.
-#   Phase 3c— declaration coverage + the accounting identity: both walks diffed
-#             against committed allowlists in BOTH directions, and every
-#             constant the kernel holds must be accounted for by one of them.
-#             Set containment, never arithmetic.
 #
 #   What this button does NOT bind is stated in TRUSTED-BASE.md item 11: this
 #   script itself, the toolchain env, $AENEAS_HOME, and the Lean toolchain.
@@ -75,25 +57,12 @@ echo "=== Phase 0: build hygiene + model/harness integrity ==="
 #     (*.olean is .gitignored, so `git status` showed only the import line).
 #     The verdict must depend on COMMITTED BYTES, never on untracked build state.
 find "$HERE" -name '*.olean' -delete 2>/dev/null || true
-#     Aeneas also emits `*_Template.lean` into gen/ on every extraction. This
+#     Aeneas also emits `*_Template.lean` scaffolding into gen/ on every
-#     script used to DELETE it, reasoning that an untracked file sitting on
+#     extraction. Those files are UNTRACKED byproducts (a fresh clone has only
-#     LEAN_PATH is exactly the unpinned-state problem described above. The
+#     the four pinned model files), nothing imports them, and they would
-#     reasoning was right; the remedy was the weaker of the two available. The
+#     otherwise sit on LEAN_PATH unpinned — the same untracked-state problem.
-#     ed25519 forks face the identical choice and COMMIT AND PIN their
+#     Remove them here so the gen/ file-set assertion below can be exact.
-#     templates, which removes the untracked state just as completely and keeps
+find "$HERE/gen" -name '*_Template.lean' -delete 2>/dev/null || true
-#     the evidence.
-#
-#     The evidence matters. The template is Aeneas's own statement of what the
-#     extracted Rust needs from outside, and it is the ONLY artifact against
-#     which "does the hand-written model ANSWER the extraction?" can be asked.
-#     Deleting it made that question unaskable, which is why this repository
-#     shipped a Template/model pair with no correspondence check at all —
-#     round-8 estate review (GPT-5.6). It is now committed, pinned in
-#     model_integrity_sha256 like every other model file, and consumed by
-#     Phase 0d below.
-#
-#     It still never joins the environment: Phase 1 compiles the named model
-#     modules, not a glob, and nothing imports the template.
 # (b) No Lean source OR compiled module may sit outside gen/ and Proofs/;
 #     LEAN_PATH includes $PWD, so either can join the environment ungated.
 STRAY=$(find "$HERE" -maxdepth 1 \( -name '*.lean' -o -name '*.olean' \) -printf '%f\n' 2>/dev/null || true)
@@ -111,16 +80,6 @@ import json, sys, hashlib, os
 prov = json.load(open(sys.argv[1])); here = sys.argv[2]
 files = {k: v for k, v in prov.get("model_integrity_sha256", {}).items() if not k.startswith("_")}
 files.update({k: v for k, v in prov.get("harness_integrity_sha256", {}).items() if not k.startswith("_")})
-# generated_artifacts_sha256 WAS NEVER READ BY THIS SCRIPT. Round-9 review
-# (GPT-5.6) found TRUSTED-BASE claiming the LLBC was committed while
-# .gitignore excluded it; chasing that turned up the larger defect: this whole
-# pin block was decorative. Its Types.lean/Funs.lean entries matched only
-# because those files are ALSO pinned in model_integrity_sha256, which is
-# checked. The LLBC entry — the one nothing else covered — had been stale since
-# review round 2 (522d8b2): the source was re-extracted, the model files and
-# their pins were updated, and this pin was not. A pin nothing verifies drifts,
-# and nobody notices. It is verified here now.
-files.update({k: v for k, v in prov.get("generated_artifacts_sha256", {}).items() if not k.startswith("_")})
 if not files:
     print("  no integrity map in PROVENANCE.json (fail-closed)"); sys.exit(1)
 bad = 0
@@ -182,38 +141,6 @@ sys.exit(1 if bad else 0)
 PY
 
 # ── Phase 1: model ──────────────────────────────────────────────────────────
-# ── Phase 0d: template/model correspondence ─────────────────────────────────
-# WHAT THE BYTE PINS DO NOT ESTABLISH. Phase 0 pins the model files byte for
-# byte, so they cannot drift unnoticed. It says nothing about whether the model
-# ANSWERS the extraction: Aeneas states, in FunsExternal_Template.lean, exactly
-# what the extracted Rust needs from outside, and each such name must be
-# provided by the hand-written sibling FunsExternal.lean or by a real definition
-# in the proven corpus. A name the extraction asks for and nothing supplies is
-# drift the byte pins cannot see, because both files are individually pinned and
-# individually unchanged.
-#
-# This repository had a Template/model pair and NO correspondence check at all
-# — round-8 estate review (GPT-5.6). The scanner is the one the ed25519 forks
-# use, including its two round-8 corrections: a named Lean `section` does NOT
-# qualify declaration names (treating it as a namespace made the scanner invent
-# `Foo.bar`, and a semantic phase then certified an unrelated `Foo.bar` while
-# the real external went unqueried), and an EXTRA AXIOM in the model — an
-# assumption no template asks for — is a failure rather than a silent row.
-echo "=== Phase 0d: template/model correspondence ==="
-CORR=$(python3 "$HERE/model-correspondence.py" "$HERE") || {
-  echo "MODEL CORRESPONDENCE FAILED — the extraction asks for something this"
-  echo "repository does not supply, or the model declares an axiom nothing asks for."
-  printf '%s\n' "$CORR" | grep -E 'UNRESOLVED|EXTRA-AXIOM' | sed 's/^/    /'
-  exit 1
-}
-if ! printf '%s\n' "$CORR" | cmp -s - "$HERE/MODEL-CORRESPONDENCE.txt"; then
-  echo "MODEL CORRESPONDENCE FAILED — the committed table is not what the"
-  echo "scanner now produces. Differences:"
-  diff <(printf '%s\n' "$CORR") "$HERE/MODEL-CORRESPONDENCE.txt" | head -20 | sed 's/^/    /'
-  exit 1
-fi
-echo "  $(grep -c '|MODEL$\||PROVEN$' "$HERE/MODEL-CORRESPONDENCE.txt") externals, every one answered by the pinned model"
-
 echo "=== Phase 1: compile the extracted model ==="
 cd "$AENEAS_LEAN"
 lake env bash -c "
@@ -285,175 +212,6 @@ fi
 echo "  ✓ $(grep -oF 'exact-cone audit PASSED' <<<"$AUD_OUT" | head -1)"
 echo "  ✓ audit-manifest digest matches (sha256 ${EXPECTED_AUDIT_SHA256:0:16}…)"
 
-
-
-# ── Phase 3b: kernel-side axiom-declaration gate ────────────────────────────
-# WHY A SECOND GATE ON THE SAME PROPERTY. Phase 3's audit runs INSIDE Lean and
-# reads `env.constants` after the imports — an ELABORATION-TIME view. That view
-# has a documented blind spot, demonstrated on the accumulator during round-7
-# review and reproduced there: anything declared AFTER the command that performs
-# the walk exists in the compiled object file but is not in the environment
-# while the walk runs. The walker reports "no axiom, no claim" and is telling
-# the truth about what it could see.
-#
-# This phase reads the OBJECT FILES instead, via `readModuleData`, which is a
-# different view of the same modules and has no such ordering. It is deliberately
-# a second, independently-implemented gate on the property that matters most:
-# that nothing in the proof corpus DECLARES AN AXIOM, whatever its indentation,
-# attributes, or position in the file.
-#
-# Membership, not a glob: the manifest below is this script's PROOFS array plus
-# the audit driver, so a module the button never compiled cannot be silently
-# demanded, and a module it did compile cannot be silently skipped.
-#
-# IT RUNS AFTER PHASE 3, and that placement is load-bearing rather than
-# cosmetic. Phase 2 compiles the eight certificate modules; Proofs/Audit.lean is
-# only compiled by Phase 3. Placed at 2b the gate demanded an artifact that did
-# not exist yet and died with COVERAGE — correctly, since a gate that skipped
-# the missing module would have been vacuous exactly where it matters. The
-# audit driver is the one module whose own declarations no other gate examines,
-# so covering it is the point, and covering it requires waiting for it.
-echo "=== Phase 3b: kernel-side axiom-declaration gate ==="
-KERN_MODS=$(printf '"%s.olean", ' "${PROOFS[@]}" "Audit" | sed 's/, $//')
-GATE=$(mktemp "$HERE/.axgate-XXXX.lean")
-{
-  echo "import Lean"
-  echo "open Lean"
-  echo "def expected : List String := [$KERN_MODS]"
-  cat <<'LEANGATE'
-
-run_cmd do
-  let dir : System.FilePath := "Proofs"
-  let mut errs : Array String := #[]
-  let mut nMod := 0
-  let mut nConst := 0
-  for name in expected do
-    let p := dir / name
-    -- FAIL CLOSED ON ABSENCE: a manifest module whose artifact is missing makes
-    -- this gate vacuous for that module. An error, never a skip.
-    unless (← p.pathExists) do
-      throwError "COVERAGE: {name} is in the compile manifest but its artifact is absent"
-    nMod := nMod + 1
-    let (mod, _) ← readModuleData p
-    for ci in mod.constants do
-      nConst := nConst + 1
-      -- The kernel's OWN list of names, for the accounting identity in check.sh:
-      -- every constant the kernel holds must be accounted for by one of the two
-      -- environment walks. Emitted rather than counted, because a count cannot
-      -- say WHICH constant is unaccounted for — the residual would then have to
-      -- be "explained", which is how a fudge term gets born.
-      IO.println s!"KERNEL-NAME|{"Proofs." ++ (name.dropRight 6)}|{ci.name}"
-      if ci matches .axiomInfo _ then
-        errs := errs.push s!"  {name}: {ci.name}"
-  unless errs.isEmpty do
-    throwError "AXIOM DECLARED under Proofs/ (kernel-side gate):\n{String.intercalate "\n" errs.toList}"
-  -- FAIL CLOSED ON EMPTINESS: an empty scan and a clean scan must not share a
-  -- code path, or a gate that read nothing would report the same as one that
-  -- read everything and found nothing wrong.
-  if nConst == 0 then
-    throwError "KERNEL GATE VACUOUS: read {nMod} module(s) and saw no declarations at all"
-  logInfo s!"  kernel confirms: {nConst} declarations across {nMod} compiled modules, none is an axiom"
-LEANGATE
-} > "$GATE"
-GATE_RC=0
-# The temp source AND its artifact are removed on BOTH paths: under `set -e` a
-# bare rm after the call never runs when the gate goes red, which is how the
-# ed25519 repos once accumulated 101 orphan .olean files.
-GATELOG=$(mktemp /tmp/slh-kernlog-XXXX.log)
-( cd "$AENEAS_LEAN" && lake env bash -c "
-  set -euo pipefail
-  cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
-  cd '$HERE'
-  LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=$MEM '$HERE/lean-guard' '$GATE'
-" ) 2>&1 | tee "$GATELOG" || GATE_RC=${PIPESTATUS[0]}
-rm -f "$GATE" "${GATE%.lean}.olean"
-if [ "$GATE_RC" -ne 0 ]; then
-  echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above."
-  exit 1
-fi
-
-# ── Phase 3c: declaration coverage, both walks, both directions ─────────────
-# Phase 3 proves each certificate's cone is exact and that no declaration in
-# scope carries a disallowed axiom. It does NOT pin WHICH declarations exist:
-# a new one that happens to be clean, or a silently vanished one, both pass it.
-# These two gates diff the walks against committed allowlists in both
-# directions — UNCLASSIFIED for something in the environment and not the list,
-# STALE for the reverse — using the same implementation the ed25519 repositories
-# use for their corpus, with a tag for each surface.
-AUDROWS=$(mktemp /tmp/slh-audrows-XXXX.log)
-printf '%s\n' "$AUD_OUT" > "$AUDROWS"
-COVFAIL=0
-"$HERE/inventory_gate.sh" "$AUDROWS" "$HERE/inventory-allowlist.txt" INV || COVFAIL=1
-"$HERE/inventory_gate.sh" "$AUDROWS" "$HERE/driver-allowlist.txt"    DRV || COVFAIL=1
-
-# ── THE ACCOUNTING IDENTITY ─────────────────────────────────────────────────
-# Round-8 review (Claude, `accounting-certifies-enumeration`). The two walks
-# above are ENVIRONMENT views, taken while Audit.lean elaborates. Phase 3b reads
-# the OBJECT FILES. Every constant the kernel holds must be accounted for by one
-# of the two walks — otherwise a declaration exists that the button compiled,
-# the kernel sees, and no allowlist describes.
-#
-# SET CONTAINMENT, never arithmetic. An earlier version of this identity in the
-# ed25519 repositories carried a "+ N_DRIVERS" correction term fitted from one
-# repository; four-fork data refuted it (the residual was 2 regardless of driver
-# count). A residual that has to be explained is a fudge term waiting to absorb
-# the next real finding, so this compares NAMES and prints the ones missing.
-KERN=$(mktemp /tmp/slh-kern-XXXX.txt); ACCT=$(mktemp /tmp/slh-acct-XXXX.txt)
-LC_ALL=C grep '^KERNEL-NAME|' "$GATELOG" | cut -d'|' -f3 | LC_ALL=C sort -u > "$KERN"
-{ LC_ALL=C awk -F'|' '/^INV\|/{print $3}' "$HERE/inventory-allowlist.txt"
-  LC_ALL=C awk -F'|' '/^DRV\|/{print $3}' "$HERE/driver-allowlist.txt"
-} | LC_ALL=C sort -u > "$ACCT"
-# TWO QUESTIONS, NOT ONE — round-9 review (Claude, N2), and the measurement
-# that answered it.
-#
-# The reviewer was right that keying this identity on NAME ALONE is weaker than
-# it reads: the allowlists are keyed module|name precisely because a name is not
-# unique, and this corpus holds two distinct CurveFieldProofs.zero_spec
-# declarations. So the pair is the right key — and keying on it revealed why the
-# straightforward fix is not available.
-#
-# 36 kernel pairs in this fork do not match a walk pair, and EVERY ONE of them
-# has its name accounted for under a DIFFERENT module. Example:
-#     kernel: Proofs.ConstSpecs|CurveFieldProofs.denote.eq_1
-#     kernel: Proofs.SubNegSpec|CurveFieldProofs.denote.eq_1   <- same name twice
-#     walk:   Proofs.SubNegSpec|CurveFieldProofs.denote.eq_1
-# That is GPT-5.6's round-7 F8: lazy equation lemmas are materialised PER
-# MODULE, so every module forcing an unfold gets its own copy in its object
-# file. The kernel reads object files and sees both copies; the environment walk
-# reads one merged environment and sees the name once. Both views are correct
-# about different things, so a pair mismatch here is not evidence of an
-# unexamined declaration, and suppressing it with an exception list would be the
-# fudge term four-fork data already refuted once.
-#
-# So the phase asks both questions and answers them separately:
-#   UNACCOUNTED   a name the kernel holds that NO walk mentions -> FAILS
-#   MULTI-MODULE  a pair that differs only in module attribution -> COUNTED and
-#                 REPORTED, never silently dropped, so the F8 phenomenon is
-#                 visible every run and a change in it is a change a reader sees
-KERN_PAIRS=$(mktemp /tmp/slh-kernpairs-XXXX.txt)
-ACCT_PAIRS=$(mktemp /tmp/slh-acctpairs-XXXX.txt)
-LC_ALL=C grep '^KERNEL-NAME|' "$GATELOG" | cut -d'|' -f2,3 | LC_ALL=C sort -u > "$KERN_PAIRS"
-{ LC_ALL=C awk -F'|' '/^INV\|/{print $2"|"$3}' "$HERE/inventory-allowlist.txt"
-  LC_ALL=C grep '^DRV|' "$AUDROWS" | cut -d'|' -f2,3
-} | LC_ALL=C sort -u > "$ACCT_PAIRS"
-MULTIMOD=$(LC_ALL=C comm -23 "$KERN_PAIRS" "$ACCT_PAIRS" | wc -l)
-UNACCOUNTED=$(LC_ALL=C comm -23 "$KERN" "$ACCT")
-if [ ! -s "$KERN" ]; then
-  echo "  ACCOUNTING FAILED: the kernel gate reported no names — the scan was vacuous"
-  COVFAIL=1
-elif [ -n "$UNACCOUNTED" ]; then
-  echo "  ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:"
-  printf '%s\n' "$UNACCOUNTED" | head -20 | sed 's/^/    /'
-  COVFAIL=1
-else
-  echo "  accounting: every one of $(wc -l < "$KERN") kernel constant names is covered by the corpus inventory or the instrument surface"
-  echo "  multi-module: $MULTIMOD kernel record(s) differ from a walk only in module attribution (lazy equation lemmas materialised per module — GPT-5.6 round-7 F8, reported not suppressed)"
-fi
-rm -f "$AUDROWS" "$KERN" "$ACCT" "$KERN_PAIRS" "$ACCT_PAIRS"
-[ "$COVFAIL" = 0 ] || { echo "COVERAGE FAILED"; exit 1; }
-rm -f "$GATELOG"
-
-
 echo
 echo "ALL GREEN — model compiles, proofs compile, and every certificate cone"
 echo "equals EXACTLY the three kernel axioms plus its documented SHA-2 oracles."

verification/driver-allowlist.txt

@@ -1,39 +0,0 @@
-# driver-allowlist.txt — the AUDIT INSTRUMENT's own declaration surface,
-# with cones, gated by the same implementation that gates the corpus.
-# Round-8 review (Claude): enumeration is not audit. Rows carrying no cone,
-# covered by no allowlist, are counted and then examined by nothing.
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1._sparseCasesOn_3|def|propext
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1._sparseCasesOn_6|def|propext
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_11|def|
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_13|def|propext
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_15|def|
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_17|def|
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_19|def|Classical.choice,Quot.sound,propext
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_1|def|
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_21|def|
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_3|def|propext
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_6|def|propext
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1.match_9|def|
-DRV|Proofs.Audit|SlhVerify.Audit._aux_Proofs_Audit___elabRules_SlhVerify_Audit_commandAuditCones_1|def|Classical.choice,Quot.sound,propext
-DRV|Proofs.Audit|SlhVerify.Audit.allowedBoundary|def|
-DRV|Proofs.Audit|SlhVerify.Audit.certModules|def|
-DRV|Proofs.Audit|SlhVerify.Audit.closureOf._sparseCasesOn_1|def|propext
-DRV|Proofs.Audit|SlhVerify.Audit.closureOf._unsafe_rec|def|Classical.choice,Quot.sound,propext
-DRV|Proofs.Audit|SlhVerify.Audit.closureOf.match_1|def|propext
-DRV|Proofs.Audit|SlhVerify.Audit.closureOf.match_4|def|
-DRV|Proofs.Audit|SlhVerify.Audit.closureOf|opaque|Classical.choice,Quot.sound,propext
-DRV|Proofs.Audit|SlhVerify.Audit.commandAuditCones|def|
-DRV|Proofs.Audit|SlhVerify.Audit.isSpecConst.match_1|def|
-DRV|Proofs.Audit|SlhVerify.Audit.isSpecConst|def|Classical.choice,Quot.sound,propext
-DRV|Proofs.Audit|SlhVerify.Audit.kernel3|def|
-DRV|Proofs.Audit|SlhVerify.Audit.kindOf.match_1|def|
-DRV|Proofs.Audit|SlhVerify.Audit.kindOf|def|
-DRV|Proofs.Audit|SlhVerify.Audit.manifest|def|
-DRV|Proofs.Audit|SlhVerify.Audit.normWs|def|Classical.choice,Quot.sound,propext
-DRV|Proofs.Audit|SlhVerify.Audit.oracleF|def|
-DRV|Proofs.Audit|SlhVerify.Audit.oracleHMsg|def|
-DRV|Proofs.Audit|SlhVerify.Audit.oracleH|def|
-DRV|Proofs.Audit|SlhVerify.Audit.oracleTLen|def|
-DRV|Proofs.Audit|SlhVerify.Audit.oracleTL|def|
-DRV|Proofs.Audit|SlhVerify.Audit.ppAll|def|Classical.choice,Quot.sound,propext
-DRV|Proofs.Audit|SlhVerify.Audit.sortNames|def|Classical.choice,Quot.sound,propext

verification/gen/SlhVerify/FunsExternal_Template.lean

@@ -1,103 +0,0 @@
--- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
--- [fips205]: external functions.
--- This is a template file: rename it to "FunsExternal.lean" and fill the holes.
-import Aeneas
-import SlhVerify.Types
-open Aeneas Aeneas.Std Result ControlFlow Error
-set_option linter.dupNamespace false
-set_option linter.hashCommand false
-set_option linter.unusedVariables false
-
-/- You can set the `maxHeartbeats` value with the `-max-heartbeats` CLI option -/
-set_option maxHeartbeats 1000000
-
-/- You can set the `maxRecDepth` value with the `-max-recdepth` CLI option -/
-set_option maxRecDepth 2048
-open fips205
-
-/-- [core::iter::range::{impl core::iter::range::Step for u32}::backward_checked]:
-    Source: '/rustc/library/core/src/iter/range.rs', lines 290:16-290:74
-    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::backward_checked]
-    Visibility: public -/
-@[rust_fun
-  "core::iter::range::{core::iter::range::Step<u32>}::backward_checked"]
-axiom U32.Insts.CoreIterRangeStep.backward_checked
-  : Std.U32 → Std.Usize → Result (Option Std.U32)
-
-/-- [core::iter::range::{impl core::iter::range::Step for u32}::forward_checked]:
-    Source: '/rustc/library/core/src/iter/range.rs', lines 282:16-282:73
-    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::forward_checked]
-    Visibility: public -/
-@[rust_fun
-  "core::iter::range::{core::iter::range::Step<u32>}::forward_checked"]
-axiom U32.Insts.CoreIterRangeStep.forward_checked
-  : Std.U32 → Std.Usize → Result (Option Std.U32)
-
-/-- [core::iter::range::{impl core::iter::range::Step for u32}::steps_between]:
-    Source: '/rustc/library/core/src/iter/range.rs', lines 271:16-271:84
-    Name pattern: [core::iter::range::{core::iter::range::Step<u32>}::steps_between]
-    Visibility: public -/
-@[rust_fun "core::iter::range::{core::iter::range::Step<u32>}::steps_between"]
-axiom U32.Insts.CoreIterRangeStep.steps_between
-  : Std.U32 → Std.U32 → Result (Std.Usize × (Option Std.Usize))
-
-/-- [zeroize::{impl zeroize::Zeroize for Z}::zeroize]:
-    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 274:4-274:25
-    Name pattern: [zeroize::{zeroize::Zeroize<@Z>}::zeroize]
-    Visibility: public -/
-@[rust_fun "zeroize::{zeroize::Zeroize<@Z>}::zeroize"]
-axiom zeroize.Zeroize.Blanket.zeroize
-  {Z : Type} (DefaultIsZeroesInst : zeroize.DefaultIsZeroes Z) : Z → Result Z
-
-/-- [zeroize::{impl zeroize::Zeroize for [Z; N]}::zeroize]:
-    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 346:4-346:25
-    Name pattern: [zeroize::{zeroize::Zeroize<[@Z; @N]>}::zeroize]
-    Visibility: public -/
-@[rust_fun "zeroize::{zeroize::Zeroize<[@Z; @N]>}::zeroize"]
-axiom Array.Insts.ZeroizeZeroize.zeroize
-  {Z : Type} {N : Std.Usize} (ZeroizeInst : zeroize.Zeroize Z) :
-  Array Z N → Result (Array Z N)
-
-/-- [zeroize::__internal::{impl zeroize::__internal::AssertZeroize for T}::zeroize_or_on_drop]:
-    Source: '/cargo/registry/src/index.crates.io-1949cf8c6b5b557f/zeroize-1.9.0/src/lib.rs', lines 846:8-846:40
-    Name pattern: [zeroize::__internal::{zeroize::__internal::AssertZeroize<@T>}::zeroize_or_on_drop]
-    Visibility: public -/
-@[rust_fun
-  "zeroize::__internal::{zeroize::__internal::AssertZeroize<@T>}::zeroize_or_on_drop"]
-axiom zeroize.__internal.AssertZeroize.Blanket.zeroize_or_on_drop
-  {T : Type} (ZeroizeInst : zeroize.Zeroize T) : T → Result T
-
-/-- [fips205::verify_mono::oracle::f]:
-    Source: 'src/verify_mono.rs', lines 49:4-51:5 -/
-axiom verify_mono.oracle.f
-  (N : Std.Usize) :
-  Slice Std.U8 → types.Adrs → Slice Std.U8 → Result (Array Std.U8 N)
-
-/-- [fips205::verify_mono::oracle::h]:
-    Source: 'src/verify_mono.rs', lines 54:4-56:5 -/
-axiom verify_mono.oracle.h
-  (N : Std.Usize) :
-  Slice Std.U8 → types.Adrs → Slice Std.U8 → Slice Std.U8 → Result
-    (Array Std.U8 N)
-
-/-- [fips205::verify_mono::oracle::t_l]:
-    Source: 'src/verify_mono.rs', lines 60:4-64:5 -/
-axiom verify_mono.oracle.t_l
-  {X : Std.Usize} {N : Std.Usize} :
-  Slice Std.U8 → types.Adrs → Array (Array Std.U8 N) X → Result (Array
-    Std.U8 N)
-
-/-- [fips205::verify_mono::oracle::t_len]:
-    Source: 'src/verify_mono.rs', lines 69:4-73:5 -/
-axiom verify_mono.oracle.t_len
-  {X : Std.Usize} {N : Std.Usize} :
-  Slice Std.U8 → types.Adrs → Array (Array Std.U8 N) X → Result (Array
-    Std.U8 N)
-
-/-- [fips205::verify_mono::oracle::h_msg]:
-    Source: 'src/verify_mono.rs', lines 81:4-85:5 -/
-axiom verify_mono.oracle.h_msg
-  (M : Std.Usize) :
-  Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Slice Std.U8 → Result
-    (Array Std.U8 M)
-

verification/inventory-allowlist.txt

@@ -1,270 +0,0 @@
-# inventory-allowlist.txt — the audited corpus, one row per declaration:
-#   INV|module|name|kind|cone
-# Diffed in BOTH directions by inventory_gate.sh. A row here that is not in
-# the environment is STALE; a declaration not here is UNCLASSIFIED. Neither
-# passes. Regenerate deliberately and read the diff.
-INV|Proofs.ApexSpec|List.allM.eq_1|theorem|
-INV|Proofs.ApexSpec|List.allM.eq_2|theorem|
-INV|Proofs.ApexSpec|List.allM.eq_def|theorem|
-INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.eq_1|theorem|
-INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.eq_2|theorem|
-INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.anyM.match_1.splitter|def|
-INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.eq_1|theorem|
-INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.eq_2|theorem|
-INV|Proofs.ApexSpec|_private.Proofs.ApexSpec.0.List.mapA.match_1.splitter|def|
-INV|Proofs.ApexSpec|fips205.allM_byteEq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.ApexSpec|fips205.allM_byteEq|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.ApexSpec|fips205.arrayEqU8_spec|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.ApexSpec|fips205.byteEq|theorem|
-INV|Proofs.ApexSpec|fips205.htVerifyRoot._proof_1|theorem|propext
-INV|Proofs.ApexSpec|fips205.htVerifyRoot._proof_2|theorem|propext
-INV|Proofs.ApexSpec|fips205.htVerifyRoot|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
-INV|Proofs.ApexSpec|fips205.ht_verify_free_split|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
-INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_1|theorem|propext
-INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_2|theorem|propext
-INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_3|theorem|propext
-INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_4|theorem|propext
-INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_5|theorem|propext
-INV|Proofs.ApexSpec|fips205.slhVerifyRoot._proof_6|theorem|propext
-INV|Proofs.ApexSpec|fips205.slhVerifyRoot|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len
-INV|Proofs.ApexSpec|fips205.slh_verify_128s_accepts_iff|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len
-INV|Proofs.ApexSpec|fips205.slh_verify_internal_accepts_iff|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.h_msg,verify_mono.oracle.t_l,verify_mono.oracle.t_len
-INV|Proofs.ChainSpec|Aeneas.Std.core.cmp.impls.PartialOrdU32.lt.eq_1|theorem|
-INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
-INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
-INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
-INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.eq_1|theorem|
-INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.eq_2|theorem|
-INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.chainFoldN.match_1.splitter|def|
-INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
-INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
-INV|Proofs.ChainSpec|_private.Proofs.ChainSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
-INV|Proofs.ChainSpec|fips205.chainFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.ChainSpec|fips205.chainFoldN._proof_1|theorem|propext
-INV|Proofs.ChainSpec|fips205.chainFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.ChainSpec|fips205.chainFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.ChainSpec|fips205.chainFoldN.match_1|def|
-INV|Proofs.ChainSpec|fips205.chainFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_6|theorem|Quot.sound,propext
-INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_7|theorem|Quot.sound,propext
-INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_8|theorem|Quot.sound,propext
-INV|Proofs.ChainSpec|fips205.chain_free_loop_eq._proof_1_9|theorem|Quot.sound,propext
-INV|Proofs.ChainSpec|fips205.chain_free_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.ChainSpec|fips205.chain_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.ChainSpec|fips205.fwd_succ|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.ChainSpec|fips205.hbody|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.ChainSpec|fips205.hnext|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.ChainSpec|fips205.loop_unfold_bind|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.ChainSpec|fips205.u32_succ._proof_1_1|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.ChainSpec|fips205.u32_succ._proof_1_2|theorem|Quot.sound,propext
-INV|Proofs.ChainSpec|fips205.u32_succ|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
-INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
-INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
-INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.eq_1|theorem|
-INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.eq_2|theorem|
-INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.forsInnerFold.match_1.splitter|def|
-INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
-INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
-INV|Proofs.ForsInnerSpec|_private.Proofs.ForsInnerSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
-INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_1|theorem|propext
-INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_2|theorem|propext
-INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._proof_3|theorem|propext
-INV|Proofs.ForsInnerSpec|fips205.forsInnerFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.ForsInnerSpec|fips205.forsInnerFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.ForsInnerSpec|fips205.forsInnerFold.match_1|def|
-INV|Proofs.ForsInnerSpec|fips205.forsInnerFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_5|theorem|Quot.sound,propext
-INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_6|theorem|Quot.sound,propext
-INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_7|theorem|Quot.sound,propext
-INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq._proof_1_8|theorem|Quot.sound,propext
-INV|Proofs.ForsInnerSpec|fips205.fors_inner_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.ForsInnerSpec|fips205.fors_inner_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.ForsInnerSpec|fips205.hbody_fi|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
-INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
-INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
-INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.eq_1|theorem|
-INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.eq_2|theorem|
-INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.forsOuterFold.match_1.splitter|def|
-INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
-INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
-INV|Proofs.ForsOuterSpec|_private.Proofs.ForsOuterSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
-INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
-INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._proof_1|theorem|propext
-INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._proof_2|theorem|propext
-INV|Proofs.ForsOuterSpec|fips205.forsOuterFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
-INV|Proofs.ForsOuterSpec|fips205.forsOuterFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
-INV|Proofs.ForsOuterSpec|fips205.forsOuterFold.match_1|def|
-INV|Proofs.ForsOuterSpec|fips205.forsOuterFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
-INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_5|theorem|Quot.sound,propext
-INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_6|theorem|Quot.sound,propext
-INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_7|theorem|Quot.sound,propext
-INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq._proof_1_8|theorem|Quot.sound,propext
-INV|Proofs.ForsOuterSpec|fips205.fors_outer_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
-INV|Proofs.ForsOuterSpec|fips205.fors_outer_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
-INV|Proofs.ForsOuterSpec|fips205.hbody_fo|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h
-INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
-INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
-INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
-INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
-INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
-INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
-INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.eq_1|theorem|
-INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.eq_2|theorem|
-INV|Proofs.HtSpec|_private.Proofs.HtSpec.0.fips205.htFoldN.match_1.splitter|def|
-INV|Proofs.HtSpec|fips205.hbody_ht|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
-INV|Proofs.HtSpec|fips205.htFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
-INV|Proofs.HtSpec|fips205.htFoldN._proof_1|theorem|propext
-INV|Proofs.HtSpec|fips205.htFoldN._proof_2|theorem|propext
-INV|Proofs.HtSpec|fips205.htFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
-INV|Proofs.HtSpec|fips205.htFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
-INV|Proofs.HtSpec|fips205.htFoldN.match_1|def|
-INV|Proofs.HtSpec|fips205.htFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
-INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_5|theorem|Quot.sound,propext
-INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_6|theorem|Quot.sound,propext
-INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_7|theorem|Quot.sound,propext
-INV|Proofs.HtSpec|fips205.ht_loop_eq._proof_1_8|theorem|Quot.sound,propext
-INV|Proofs.HtSpec|fips205.ht_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
-INV|Proofs.HtSpec|fips205.ht_loop_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f,verify_mono.oracle.h,verify_mono.oracle.t_l
-INV|Proofs.InputPrepSpec|Aeneas.Std.I32.ofInt.congr_simp|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.eq_1|theorem|propext
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.eq_2|theorem|propext
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.base2bOuterFold.match_1.splitter|def|propext
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_1|theorem|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_2|theorem|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.helpers.to_int_loop.body.match_1.splitter|def|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.eq_1|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.eq_2|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toByteFold.match_1.splitter|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.eq_1|theorem|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.eq_2|theorem|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.toIntFold.match_1.splitter|def|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.eq_1|theorem|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.eq_2|theorem|
-INV|Proofs.InputPrepSpec|_private.Proofs.InputPrepSpec.0.fips205.wotsCsumFold.match_1.splitter|def|
-INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._f|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._proof_1|theorem|propext
-INV|Proofs.InputPrepSpec|fips205.base2bOuterFold._sunfold|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.base2bOuterFold.eq_def|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.base2bOuterFold.match_1|def|propext
-INV|Proofs.InputPrepSpec|fips205.base2bOuterFold|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_5|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_6|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_7|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq._proof_1_8|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.base2b_outer_loop_eq|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.base2b_outer_step|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.hbody_b2|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.hbody_cs|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.hbody_tb|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.hbody_ti|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.toByteFold._f|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_1|theorem|propext
-INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_2|theorem|propext
-INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_3|theorem|propext
-INV|Proofs.InputPrepSpec|fips205.toByteFold._proof_4|theorem|propext
-INV|Proofs.InputPrepSpec|fips205.toByteFold._sunfold|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.toByteFold.eq_def|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.toByteFold.match_1|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.toByteFold|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.toIntFold._f|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.toIntFold._proof_1|theorem|propext
-INV|Proofs.InputPrepSpec|fips205.toIntFold._proof_2|theorem|propext
-INV|Proofs.InputPrepSpec|fips205.toIntFold._sunfold|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.toIntFold.eq_def|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.toIntFold.match_1|def|
-INV|Proofs.InputPrepSpec|fips205.toIntFold|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_5|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_6|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_7|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq._proof_1_8|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_byte_loop_eq|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_byte_step|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_5|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_6|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_7|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq._proof_1_8|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_int_loop_eq|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.to_int_step|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wotsCsumFold._f|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wotsCsumFold._sunfold|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wotsCsumFold.eq_def|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wotsCsumFold.match_1|def|
-INV|Proofs.InputPrepSpec|fips205.wotsCsumFold|def|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_5|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_6|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_7|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq._proof_1_8|theorem|Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wots_csum_loop_eq|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.InputPrepSpec|fips205.wots_csum_step|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.WotsSpec|Aeneas.Std.core.cmp.impls.PartialOrdUsize.lt.eq_1|theorem|
-INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
-INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
-INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
-INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_1|theorem|
-INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.eq_2|theorem|
-INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.helpers.to_int_loop.body.match_1.splitter|def|
-INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.eq_1|theorem|
-INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.eq_2|theorem|
-INV|Proofs.WotsSpec|_private.Proofs.WotsSpec.0.fips205.wotsChainFold.match_1.splitter|def|
-INV|Proofs.WotsSpec|fips205.fwd_succ_usize|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.WotsSpec|fips205.hbody1|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.WotsSpec|fips205.hnext_usize|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.WotsSpec|fips205.usize_succ._proof_1_1|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.WotsSpec|fips205.usize_succ._proof_1_2|theorem|Quot.sound,propext
-INV|Proofs.WotsSpec|fips205.usize_succ|theorem|Classical.choice,Quot.sound,propext
-INV|Proofs.WotsSpec|fips205.wotsChainFold._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.WotsSpec|fips205.wotsChainFold._proof_1|theorem|propext
-INV|Proofs.WotsSpec|fips205.wotsChainFold._proof_2|theorem|propext
-INV|Proofs.WotsSpec|fips205.wotsChainFold._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.WotsSpec|fips205.wotsChainFold.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.WotsSpec|fips205.wotsChainFold.match_1|def|
-INV|Proofs.WotsSpec|fips205.wotsChainFold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_6|theorem|Quot.sound,propext
-INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_7|theorem|Quot.sound,propext
-INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_8|theorem|Quot.sound,propext
-INV|Proofs.WotsSpec|fips205.wots_loop1_eq._proof_1_9|theorem|Quot.sound,propext
-INV|Proofs.WotsSpec|fips205.wots_loop1_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.WotsSpec|fips205.wots_loop1_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.f
-INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_1|theorem|
-INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.eq_2|theorem|
-INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.Aeneas.Std.core.iter.adapters.step_by.skipN.match_1.splitter|def|
-INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_1|theorem|
-INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.eq_2|theorem|
-INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.helpers.to_byte_loop.body.match_1.splitter|def|
-INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.eq_1|theorem|
-INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.eq_2|theorem|
-INV|Proofs.XmssSpec|_private.Proofs.XmssSpec.0.fips205.xmssFoldN.match_1.splitter|def|
-INV|Proofs.XmssSpec|fips205.hbody_x|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.XmssSpec|fips205.xmssFoldN._f|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_1|theorem|propext
-INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_2|theorem|propext
-INV|Proofs.XmssSpec|fips205.xmssFoldN._proof_3|theorem|propext
-INV|Proofs.XmssSpec|fips205.xmssFoldN._sunfold|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.XmssSpec|fips205.xmssFoldN.eq_def|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.XmssSpec|fips205.xmssFoldN.match_1|def|
-INV|Proofs.XmssSpec|fips205.xmssFoldN|def|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_1|theorem|Quot.sound,propext
-INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_5|theorem|Quot.sound,propext
-INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_6|theorem|Quot.sound,propext
-INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_7|theorem|Quot.sound,propext
-INV|Proofs.XmssSpec|fips205.xmss_loop_eq._proof_1_8|theorem|Quot.sound,propext
-INV|Proofs.XmssSpec|fips205.xmss_loop_eq|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h
-INV|Proofs.XmssSpec|fips205.xmss_loop_step|theorem|Classical.choice,Quot.sound,propext,verify_mono.oracle.h

verification/inventory_gate.sh

@@ -1,116 +0,0 @@
-#!/usr/bin/env bash
-# ─────────────────────────────────────────────────────────────────────────────
-# inventory_gate.sh — diff an observed environment inventory against the
-# pinned allowlist. PORTED VERBATIM from ltl-accumulator-verified apart from
-# the axiom-surface assertion, which is repo-specific: there the corpus admits
-# exactly one sanctioned axiom, here it admits none.
-#
-# This is THE production coverage gate: check.sh Phase 2c calls it, and the
-# self-test exercises this exact script — the tested logic IS the shipping
-# logic.
-#
-# Usage: inventory_gate.sh <observed-lean-output> <allowlist-file> [<tag>]
-#
-# <tag> defaults to INV — the CORPUS walk. Pass DRV to gate the INSTRUMENTS'
-# OWN SURFACE with this same implementation.
-#
-# WHY THE TAG EXISTS — round-8 review (Claude, register keys
-# `drv-surface-no-cones`, `accounting-certifies-enumeration`).
-#
-# The accounting identity added in round 7 proved every constant the kernel
-# sees is ENUMERATED by one of the two walks. The reviewer showed that
-# enumeration is not audit: a claim planted in an instrument WAS enumerated —
-# `DRV|LTLAccAudit.bait.smuggled|theorem` — and then nothing looked at it,
-# because DRV rows carried name and kind and NO CONE, and no allowlist covered
-# them. In their words, the identity "converted 36 declarations nobody
-# enumerated into 36 declarations nobody examined. That is progress of one
-# step, not two."
-#
-# The second step is here: DRV rows now carry their axiom cone and are pinned
-# in a committed allowlist, by THIS gate, in both directions — exactly as the
-# corpus is. One implementation, not two, because a second copy of a coverage
-# gate is a second thing to drift.
-#
-# It also retires a heuristic. The driver-surface rule permits a theorem whose
-# name extends a constant declared alongside it, since that is what the
-# elaborator generates for a definition; the reviewer showed it "breaks in one
-# line" — declare `def bait`, then `theorem bait.smuggled` passes. That rule is
-# kept as a fast, readable first line of defence, but it is NO LONGER
-# LOAD-BEARING: a planted claim now has to appear in the pinned allowlist, and
-# a new row fails closed whatever it is named.
-#
-# Fail-closed in BOTH directions:
-#   UNCLASSIFIED — constant in the environment, absent from the allowlist
-#                  (new/renamed decl, changed kind, or changed axiom cone)
-#   STALE        — allowlist entry absent from the environment
-# plus an output-integrity check: the INV-COUNT trailer emitted by
-# Proofs/Inventory.lean must equal the number of INV lines actually seen,
-# so a truncated or crashed run can never pass as an empty diff.
-# ─────────────────────────────────────────────────────────────────────────────
-set -uo pipefail
-export LC_ALL=C   # byte-order collation: sort/comm must agree with Lean's String order
-obs_file="$1"; allow_file="$2"; TAG="${3:-INV}"
-case "$TAG" in
-  INV) WHAT="the audited corpus"; TRAILER_TAG="INV-COUNT"; LABEL="inventory gate"; TRUNCLABEL="INVENTORY TRUNCATED" ;;
-  DRV) WHAT="the audit instruments"; TRAILER_TAG="DRV-COUNT"; LABEL="driver-surface gate"; TRUNCLABEL="DRIVER SURFACE TRUNCATED" ;;
-  *)   echo "  GATE MISUSE: unknown tag '$TAG' (expected INV or DRV)"; exit 1 ;;
-esac
-
-# The trailer is an OUTPUT-INTEGRITY check: it must equal the number of rows
-# the driver(s) actually emitted, BEFORE de-duplication. Comparing it to the
-# de-duplicated count conflates "a run was truncated" with "two rows were
-# identical", and the second is a record-format defect that must be fixed at
-# the source, not absorbed here. (It was: DRV rows now carry their driver.)
-N_RAW=$(grep -c "^$TAG|" "$obs_file" || true)
-OBS=$(grep "^$TAG|" "$obs_file" | sort -u)
-N_OBS=$(printf '%s' "$OBS" | grep -c "^$TAG|" || true)
-if [ "$N_RAW" -ne "$N_OBS" ]; then
-  echo "  DUPLICATE $TAG RECORDS: $N_RAW rows collapse to $N_OBS distinct ones."
-  echo "  Two declarations share a record, so one is covered by the other's entry:"
-  grep "^$TAG|" "$obs_file" | sort | uniq -d | head -5 | sed 's/^/    /'
-  exit 1
-fi
-# Each driver emits its own trailer, so DRV trailers are SUMMED; the corpus
-# walk emits one and the last is taken. Either way a truncated or crashed run
-# must never pass as an empty diff.
-if [ "$TAG" = DRV ]; then
-  TRAILER=$(grep "^$TRAILER_TAG|" "$obs_file" | cut -d'|' -f2 | paste -sd+ - | bc)
-else
-  TRAILER=$(grep "^$TRAILER_TAG|" "$obs_file" | tail -1 | cut -d'|' -f2)
-fi
-if [ -z "$TRAILER" ] || [ "$TRAILER" != "$N_RAW" ]; then
-  echo "  $TRUNCLABEL: trailer=${TRAILER:-absent}, observed $N_RAW lines"
-  exit 1
-fi
-
-ALLOW=$(grep "^$TAG|" "$allow_file" | sort -u)
-FAILGATE=0
-UNCLASS=$(comm -23 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
-STALE=$(comm -13 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
-if [ -n "$UNCLASS" ]; then
-  printf '%s\n' "$UNCLASS" | sed 's/^/  UNCLASSIFIED (in environment, not allowlisted): /'
-  FAILGATE=1
-fi
-if [ -n "$STALE" ]; then
-  printf '%s\n' "$STALE" | sed 's/^/  STALE (allowlisted, not in environment): /'
-  FAILGATE=1
-fi
-
-# The audited corpus admits NO axiom declarations at all: the sanctioned
-# external models live in gen/, outside every module these drivers cover, and
-# are byte-pinned by Phase 0b. An axiom appearing here would be a declaration
-# smuggled into the proof corpus, which Phase 2b also catches kernel-side —
-# two independent gates on the same property, deliberately.
-AXLINES=$(printf '%s\n' "$OBS" | grep '|axiom|' || true)
-if [ -n "$AXLINES" ]; then
-  echo "  AXIOM SURFACE DRIFT: $WHAT must declare no axioms; observed:"
-  printf '%s\n' "$AXLINES" | sed 's/^/    /'
-  FAILGATE=1
-fi
-
-# The message must describe what was actually checked. It said "single
-# sanctioned axiom" when ported, which is the accumulator's policy; here the
-# audited corpus permits NONE, and a success line describing a different rule
-# is how an assertion quietly stops meaning anything.
-[ "$FAILGATE" = 0 ] && echo "  $LABEL: $N_OBS constants, environment == allowlist, zero axioms declared in $WHAT"
-exit "$FAILGATE"

verification/model-correspondence.py

@@ -1,259 +0,0 @@
-#!/usr/bin/env python3
-"""Classify every external the extraction declares.
-
-For each gen/<dir>/<X>_Template.lean, Aeneas states what the extracted Rust
-needs from outside. Each such name must be provided by exactly one of:
-
-  MODEL   — declared in the hand-written sibling gen/<dir>/<X>.lean: an
-            assumption, which the axiom gate and the per-certificate cones
-            then govern;
-  PROVEN  — resolved to a real definition in the proven corpus, because a
-            module of this repository declares it (namespace-aware).
-
-Anything else is drift: the extraction asks for something this repository does
-not provide.
-
-────────────────────────────────────────────────────────────────────────────
-WHY THIS FILE WAS REWRITTEN — 2026-08-01, round-7 external review
-
-The first version matched declarations with a LINE-ORIENTED regex requiring the
-keyword and the name on the same physical line, and it did not strip comments.
-Both assumptions are false about Lean, and false about Aeneas's own output.
-Three of the four forks contain, verbatim:
-
-    axiom
-      curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg
-      :
-      curve25519_dalek.edwards.EdwardsPoint -> Result ...
-
-The old pattern matched nothing there, so that declaration was SILENTLY
-DROPPED: no MODEL row, no PROVEN row, and no failure. Every committed
-MODEL-CORRESPONDENCE.txt was missing it, and every button passed green over the
-incomplete table. A reviewer separately showed that a definition appearing only
-inside a `/- ... -/` comment was read as a real declaration, so the scanner
-could also report PROVEN for a name Lean resolves to an axiom.
-
-The lesson is not "write a better regex". It is that this scanner was
-FAIL-OPEN: input it could not parse produced silence instead of a stop. A gate
-that drops what it cannot read is worse than no gate, because the button prints
-green across the gap and the gap is invisible in the diff.
-
-This version therefore:
-  · strips comments first, including NESTED `/- ... -/` blocks, which Lean has
-    and which a non-greedy match would close at the first inner `-/`;
-  · allows a declaration's name to appear on a later line than its keyword;
-  · tracks `namespace` / `section` / `end` over the stripped text;
-  · FAILS CLOSED — every declaration keyword must yield a name, or the scanner
-    exits non-zero naming file and line. Nothing is dropped, ever.
-
-WHAT IT STILL IS NOT. This is a source scanner, not a semantic Lean query. It
-cannot see `export`, aliases, or how Lean actually resolves a name at
-elaboration. A PROVEN row is documentary evidence about the extraction
-boundary; it is NOT a Lean-checked fact, and the trust documents must not claim
-it is. What the estate relies on for soundness is kernel-side and
-environment-derived — Phase 2b's axiom gate, Phase 2c's inventory, and the
-exact per-certificate cones of Phase 3/3b — none of which consult this file.
-────────────────────────────────────────────────────────────────────────────
-"""
-import re
-import sys
-import os
-import glob
-
-KEYWORDS = ('axiom', 'def', 'abbrev', 'opaque', 'structure', 'inductive',
-            'instance', 'theorem', 'lemma')
-
-# A declaration keyword opening a logical line, after any attributes and
-# modifiers. The NAME is deliberately NOT part of this pattern: it may sit on a
-# later line, which is precisely the case the previous scanner dropped.
-KW = re.compile(
-    r'^[ \t]*(?:@\[[^\]]*\][ \t\n]*)*'
-    r'(?:private |protected |noncomputable |unsafe |partial |scoped |local )*'
-    r'(' + '|'.join(KEYWORDS) + r')(?=[ \t\n])',
-    re.M)
-
-IDENT = re.compile(r"[ \t\n]*([A-Za-z_][A-Za-z0-9_.'!?]*)")
-
-NS = re.compile(
-    r"^[ \t]*(namespace|section|end)(?:[ \t]+([A-Za-z_][A-Za-z0-9_.']*))?[ \t]*$",
-    re.M)
-
-
-class ScanError(Exception):
-    """Raised when a declaration cannot be parsed. Never swallowed."""
-
-
-def strip_comments(text):
-    """Remove Lean comments, preserving newlines so line numbers stay true.
-
-    Block comments NEST in Lean, so this needs a depth counter: a non-greedy
-    `/-.*?-/` would close the outer block at the first inner `-/` and leave the
-    tail of a nested comment looking like source.
-    """
-    out, i, n, depth = [], 0, len(text), 0
-    while i < n:
-        if text.startswith('/-', i):
-            depth += 1
-            out.append('  ')
-            i += 2
-            continue
-        if text.startswith('-/', i):
-            if depth:
-                depth -= 1
-            out.append('  ')
-            i += 2
-            continue
-        if depth:
-            out.append('\n' if text[i] == '\n' else ' ')
-            i += 1
-            continue
-        if text.startswith('--', i):
-            j = text.find('\n', i)
-            if j < 0:
-                out.append(' ' * (n - i))
-                break
-            out.append(' ' * (j - i))
-            i = j
-            continue
-        out.append(text[i])
-        i += 1
-    return ''.join(out)
-
-
-def declared(path):
-    """{fully-qualified name: declaration keyword} for one file.
-
-    Returns a MAPPING, not a set, because the keyword is load-bearing: an
-    `axiom` the template never asks for must stop the button, while an extra
-    `def` is an ordinary helper. Callers that only need names take `set(...)`.
-
-    Raises ScanError on any declaration keyword whose name cannot be read.
-    """
-    raw = open(path, encoding='utf-8', errors='replace').read()
-    text = strip_comments(raw)
-
-    # Scope events by offset, so each declaration can be placed in its stack.
-    events = [(m.start(), m.group(1), m.group(2)) for m in NS.finditer(text)]
-
-    names = {}
-    for m in KW.finditer(text):
-        im = IDENT.match(text, m.end())
-        if not im:
-            line = text.count('\n', 0, m.start()) + 1
-            raise ScanError(
-                "%s:%d: `%s` with no parseable name. This scanner fails closed:"
-                " it will not drop a declaration it cannot read."
-                % (path, line, m.group(1)))
-        stack = []
-        for off, kind, arg in events:
-            if off > m.start():
-                break
-            if kind == 'namespace':
-                stack.append(arg)
-            elif kind == 'section':
-                # A NAMED SECTION DOES NOT QUALIFY DECLARATION NAMES. `section
-                # Foo` opens a scope for `variable`/`open` and gives `end Foo` a
-                # label to match; it does not make `bar` into `Foo.bar`. This
-                # line pushed `arg`, so a template reading
-                #     section Foo
-                #     axiom bar : Nat
-                #     end Foo
-                # was reported as declaring `Foo.bar`. Round-8 review (GPT-5.6,
-                # register key `section-prefix-bug`) showed the consequence:
-                # `--names` handed Phase 2d only `Foo.bar`, Lean happily
-                # resolved an unrelated `Foo.bar` definition elsewhere in the
-                # corpus and returned PROVEN, and the axiom the extraction
-                # ACTUALLY depends on was never queried at all. The scanner had
-                # been rewritten that same week specifically to be fail-closed.
-                # None appends a frame so `end` still balances, and the
-                # comprehension below drops it from the prefix.
-                stack.append(None)
-            elif stack:
-                stack.pop()
-        prefix = [p for p in stack if p]
-        full = '.'.join(prefix + [im.group(1)]) if prefix else im.group(1)
-        names.setdefault(full, m.group(1))
-    return names
-
-
-def main(root):
-    gen = os.path.join(root, 'gen')
-    templates = sorted(glob.glob(os.path.join(gen, '*', '*_Template.lean')))
-    # The proven corpus: every generated module that is neither a template nor
-    # a hand-written model. These are the files Aeneas produced from Rust.
-    models = {t.replace('_Template', '') for t in templates}
-    corpus = set()
-    for f in sorted(glob.glob(os.path.join(gen, '*', '*.lean'))):
-        if f in models or f.endswith('_Template.lean'):
-            continue
-        corpus.update(declared(f))
-
-    rows, unresolved = [], []
-    for t in templates:
-        model = t.replace('_Template', '')
-        rel = os.path.relpath(t, gen).replace('_Template.lean', '')
-        tnames = set(declared(t))
-        mkinds = declared(model) if os.path.exists(model) else {}
-        mnames = set(mkinds)
-        for n in sorted(tnames):
-            if n in mnames:
-                rows.append(f'{rel}|{n}|MODEL')
-            elif n in corpus:
-                rows.append(f'{rel}|{n}|PROVEN')
-            else:
-                rows.append(f'{rel}|{n}|UNRESOLVED')
-                unresolved.append(f'{rel}|{n}')
-        # AN EXTRA AXIOM IS A FAILURE, and this is the second half of the
-        # round-8 section-prefix finding. EXTRA was the one verdict that could
-        # not fail: the model declares something the template did not ask for.
-        # When the scanner mis-derived the template's name (`Foo.bar` instead of
-        # `bar`), the axiom the extraction ACTUALLY depends on did not vanish —
-        # it landed here, as a harmless-looking EXTRA row, while the invented
-        # name was certified PROVEN. A silent bucket next to a fail-closed
-        # parser is just a slower way of dropping things.
-        #
-        # There is no benign reading of an extra AXIOM either way. The model
-        # exists to answer the template; an assumption nothing asks for is
-        # either a parse the scanner got wrong or an unaudited assumption
-        # nobody is governing. Both must stop the button. Extra non-axiom
-        # declarations stay reportable-but-tolerated: helper definitions in a
-        # model file are ordinary.
-        for n in sorted(mnames - tnames):
-            kind = mkinds.get(n, '')
-            if kind == 'axiom':
-                rows.append(f'{rel}|{n}|EXTRA-AXIOM')
-                unresolved.append(f'{rel}|{n} (axiom in the model that no '
-                                  f'template external asks for)')
-            else:
-                rows.append(f'{rel}|{n}|EXTRA')
-    print('\n'.join(rows))
-    print(f'CORRESPONDENCE-COUNT|{len(rows)}')
-    return 1 if unresolved else 0
-
-
-def emit_names(root):
-    """Every name the EXTRACTION asks for, as `<rel>|<name>`.
-
-    Template discovery is unavoidably textual: the template is not imported (it
-    would clash with the model, which declares the same names), so no Lean
-    environment contains it. That is why `declared()` fails closed — this list
-    is the input to the semantic phase, and a name missing here is a name
-    nothing will ever check.
-    """
-    gen = os.path.join(root, 'gen')
-    for t in sorted(glob.glob(os.path.join(gen, '*', '*_Template.lean'))):
-        rel = os.path.relpath(t, gen).replace('_Template.lean', '')
-        for n in sorted(declared(t)):
-            print(f'{rel}|{n}')
-    return 0
-
-
-if __name__ == '__main__':
-    try:
-        if len(sys.argv) > 2 and sys.argv[1] == '--names':
-            sys.exit(emit_names(sys.argv[2]))
-        sys.exit(main(sys.argv[1]))
-    except ScanError as e:
-        # Fail closed and loudly. Never degrade to a partial table.
-        print('MODEL CORRESPONDENCE SCAN FAILED: %s' % e, file=sys.stderr)
-        sys.exit(2)