saymrwulf/fips205-slhdsa-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/fips205-slhdsa-verified.git synced 2026-09-03 19:53:49 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: saymrwulf:0d680333e311d9350650b3432f7b4669a771d11f
Branches Tags
saymrwulf:main
...
compare: saymrwulf:a693d288fbe52dc11d8971059722c8776e6301b1
Branches Tags
saymrwulf:main

9 commits
0d680333e3 ... a693d288fb

Author SHA1 Message Date
mrwulf
a693d288fb docs: estate-wide consistency pass (workflow audit, 36 findings, all verified before fixing) 
Nine parallel readers audited every doc against measured ground truth; every
finding was re-verified against the file before any edit, and the sweep fixed
by PROPERTY, not by flag — wording the readers caught in one repo was hunted
in all siblings (the two-button README sentence existed in all four forks,
not the three flagged; likewise the cone-overclaim in TRUSTED-BASE item 1).

This repo: see the diff. Records were not rewritten; clarifications are
dated. Doc-only except where noted in the estate summary; every gated doc
change was followed by a green button run.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-07 16:00:54 +02:00
mrwulf
d44b70d806 verification: separate the two accounting questions (round-9 review, Claude N2) 
Phase 2c-accounting asked one question with a name-keyed identity: is every
kernel constant covered by the corpus inventory or the instrument surface?
Keying on the name alone conflates that with a second, different question --
does the kernel attribute a declaration to the same module the walk does?

Pair-keying the identity (module|name) was the obvious fix and is wrong: it
fails on legitimate per-module duplicates. Lean materialises equation lemmas
lazily, so each module forcing an unfold gets its own copy in its object file
(GPT-5.6 round-7 F8). Those records differ from the walk only in module
attribution, and every one of their names is accounted for elsewhere.

So the block now asks both questions and reports them separately: coverage
stays name-keyed and fail-closed, module attribution is counted and printed
rather than suppressed. A divergence is now visible instead of either passing
silently or failing for the wrong reason.

The accumulator declines the second question and says why: its INV rows carry
no module column (4 fields), so its records cannot be compared as pairs at
all. Gating on the field count rather than on the row tag -- the shape of the
record, not the spelling of its label. Adding that column is the open
follow-up; until then the identity there is name-keyed only, which is weaker
and now says so.

Certified by the round-14 sweep: 50/50 green across all six repositories,
both buttons and every self-test.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-04 03:17:05 +02:00
mrwulf
1b430dfd68 llbc: commit the artifact the claim depended on, and verify the pin block 
Round-9 review (GPT-5.6, R9-F2, BLOCKER). TRUSTED-BASE said:

    "The .llbc is committed, so the SECOND step can be re-run by anyone with
     the pinned Aeneas and this repository"

.gitignore excluded it. `git ls-files` had no LLBC. The file existed only on
the author's disk. I ran `ls`, saw it, and wrote the claim without running
`git ls-files` — so a sentence that reads as an independent-reproducibility
guarantee was true for exactly one person. The experiment itself was real:
re-running Aeneas on that LLBC did reproduce Types.lean and Funs.lean
byte-identically. What was false is that anyone else could repeat it.

CHASING IT FOUND WORSE. `generated_artifacts_sha256` was read by NOTHING —
check.sh had zero references to it. Its Types.lean and 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 on
2026-07-28, the model files and their pins were updated, and this pin was not.
It named d8ec0b00…, an artifact that did NOT produce the committed model. The
file that did is 69666ddc… — timestamped nine seconds before Types.lean and
Funs.lean, and demonstrably regenerating them byte-for-byte.

A pin nothing verifies drifts, and nobody notices. That is the finding, and it
is a sharper instance of the pattern than the one the reviewer reported.

  · .gitignore no longer excludes SlhVerify.llbc; it is committed (1.6 MB)
  · its pin corrected to the artifact that actually produced the model
  · check.sh Phase 0 now verifies generated_artifacts_sha256, so the block
    stops being decorative. Negative-tested: one appended byte gives
    `✗ SlhVerify.llbc: sha256 dd5925770bc7 ≠ pinned 69666ddc43a4`, exit 1
  · TRUSTED-BASE item 3 rewritten. It now says what committing the LLBC does
    and does NOT buy: the Lean model is the faithful Aeneas image of THAT
    intermediate, and whether the intermediate is the faithful Charon image of
    fips205-source@a3ce8e8 rests on the author alone. Verifying the committed
    LLBC against itself establishes nothing about Charon.
    "Do not read the second half as evidence for the first."
  · README qualified AT THE CLAIM SITE, not via a later link

Button green after every edit; accounting still closes at 300 with no residual.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-03 20:36:19 +02:00
mrwulf
851e976450 docs: seven bindings, not six — the documents were a phase behind again 
I wrote the README and TRUSTED-BASE to describe six bindings, then added Phase
3c an hour later and did not update them. That is exactly the drift GPT-5.6's
round-8 review is about, committed by me immediately after fixing it. Recorded
plainly rather than quietly corrected.

  README         six -> seven, with Phase 3c stated in full: both allowlists,
                 both directions (UNCLASSIFIED / STALE), why the instrument
                 surface carries cones, and the accounting identity as set
                 containment with its actual numbers — kernel 300 = corpus 265
                 + instrument 35, residual none
  check.sh       header lists Phase 3c

The failure mode is worth naming because it is cheap and recurring: a phase is
added, the button is re-run, the button is green, and nothing anywhere fails
because a document is stale. Nothing in this repository can catch it — the
gates check the corpus, not the prose. Only reading the diff catches it, which
is why the round-8 briefs asked for exactly that.

Button re-run after the edits: green, accounting over 300 kernel constants.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-03 17:53:31 +02:00
mrwulf
73a92fad53 Phase 3c: declaration coverage in both directions, and the accounting identity 
Completes the round-8 hardening of this repository. Round-8 review (Claude,
register keys `drv-surface-no-cones` and `accounting-certifies-enumeration`).

WHAT PHASE 3 DID NOT PIN. It 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, and a silently vanished
one, both pass it.

  inventory-allowlist.txt  265 rows — the audited corpus
  driver-allowlist.txt      35 rows — the audit INSTRUMENT's own surface
  both as INV|module|name|kind|CONE, diffed in BOTH directions by
  inventory_gate.sh, the same implementation the ed25519 repositories use,
  with a tag per surface.

The instrument surface carries cones because the reviewer showed enumeration is
not audit: a claim planted in an instrument is counted by an accounting identity
and then examined by nothing, if its row carries no cone and no allowlist
covers it. Here the instrument's 35 declarations are pinned exactly as the
corpus's 265 are.

INTERNAL NAMES ARE NO LONGER EXEMPT from the environment walk. They were
skipped, which was harmless while nothing compared that walk against the
kernel's view — and became a hole the moment something did: Phase 3b reads
object files, which contain the compiler's auxiliaries. Exempting them would
have left the accounting identity permanently short and forced the residual to
be "explained" by a constant. That is the shape of the fudge term four-fork data
refuted in the ed25519 repositories, and it is refused here before it can start.

THE ACCOUNTING IDENTITY, as SET CONTAINMENT and never arithmetic: every constant
the kernel holds must appear in one of the two walks. The kernel gate now emits
KERNEL-NAME rows so the comparison names what is missing rather than reporting a
count that has to be interpreted.

    kernel 300  =  inventory 265  +  instrument 35     residual: none

Negative-tested, all three rejected by name and the tree restored to green:
  · a deleted INV row      -> UNCLASSIFIED: INV|Proofs.ApexSpec|List.allM.eq_1|theorem|
  · a deleted DRV row      -> UNCLASSIFIED: DRV|Proofs.Audit|SlhVerify.Audit.sortNames|def
  · a row with no declaration behind it -> STALE: …|fips205.ghost_that_does_not_exist|…

Both allowlists join the pinned harness set: not executable, so the
executable-bit rule cannot reach them, and an allowlist an attacker may rewrite
pins nothing.

fips205-slhdsa-verified now has the ed25519 repositories' gate set: 0 hygiene,
0d correspondence, 1 model, 2 proofs, 3 in-Lean audit, 3b kernel-side axiom
gate, 3c coverage + accounting.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-03 17:34:00 +02:00
mrwulf
a2cb720dc4 docs: say what the button enforces today, and where each check stops 
Round-8 estate review (GPT-5.6). Their central complaint across the estate was
that documents promise more than code checks. Here the drift ran the other way
as well: two phases were added this week and the documents described neither,
so the repository was UNDER-claiming while its own header still listed four
phases.

  check.sh header    now lists Phase 0d and Phase 3b, each with the reason it
                     exists rather than only what it does
  README             "binds four things" -> six, and says plainly that four are
                     checked inside Lean by Proofs/Audit.lean while the last two
                     deliberately do NOT rely on that file. "four model files"
                     -> five (the template is pinned now). The Phase 3b bullet
                     carries its demonstration: axiom planted after the audit
                     command, Phase 3 passed it, Phase 3b rejected it
  TRUSTED-BASE 3     extraction reproducibility split honestly in two. The
                     committed .llbc means the LLBC -> Lean half re-runs on
                     demand and did reproduce Types.lean and Funs.lean
                     byte-identically. The Rust -> LLBC half still needs charon
                     and still rests on the author alone. "Do not read the first
                     half as evidence for the second."
  TRUSTED-BASE 3b    NEW, and it is a limit rather than a capability: Phase 0d
                     is TEXTUAL. It does not ask Lean how names resolve — the
                     ed25519 repositories have a semantic phase for that and
                     this one does not. All eleven externals here happen to be
                     answered by the model itself, the narrow case where the
                     textual and semantic answers coincide; that is a property
                     of today's corpus, not a guarantee of the check.

RECORDED-RUN.md is deliberately untouched again: its "all four model files" and
its `797b4ef` pin describe the state at the run it records. A record edited to
match today is not a corrected record.

Button re-run after every edit: green, 11 externals, 298 declarations across 9
modules, none an axiom.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-03 16:35:12 +02:00
mrwulf
f2f262ae90 Phase 3b: a kernel-side axiom gate, because the environment walk has a blind spot 
Ported from the ed25519 forks and the accumulator, where it exists because a
round-7 reviewer DEMONSTRATED the gap rather than argued it.

Phase 3's audit runs inside Lean and reads `env.constants` after the imports —
an ELABORATION-TIME view. Anything declared AFTER the command that performs the
walk is in the compiled object file but not in the environment while the walk
runs. The walker then reports "no axiom, no claim" and is telling the truth
about what it could see.

This phase reads the OBJECT FILES via `readModuleData`: a different view of the
same modules, with no such ordering. 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.

DEMONSTRATED, not asserted. An `axiom cheat : ∀ (P : Prop), P` appended to
Proofs/Audit.lean after its audit command:

    === Phase 3: in-Lean audit …            <- PASSED, saw nothing
    === Phase 3b: kernel-side axiom gate    <- AXIOM DECLARED under Proofs/
                                               Audit.olean: cheat
    exit 1

The environment walk passed it and the kernel gate caught it, which is the
whole argument for having both.

PLACEMENT IS LOAD-BEARING. Written first as Phase 2b — the forks' position — it
died with COVERAGE, because Phase 2 compiles the eight certificate modules and
Proofs/Audit.lean is only compiled by Phase 3. That failure was correct: a gate
that skipped a missing module would be vacuous exactly where it matters, since
the audit driver is the one module whose own declarations no other gate
examines. Covering it requires waiting for it, so the gate runs after Phase 3.

Fails closed three ways: a manifest module whose artifact is absent, an axiom in
any module, and a scan that read zero declarations (an empty result and a clean
result must not share a code path). Membership from this script's PROOFS array
plus the driver, never a glob.

Result: 298 declarations across 9 compiled modules, none an axiom.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-03 15:57:48 +02:00
mrwulf
7ebf9495d3 correspondence: keep the artifact that says what the model must answer 
Round-8 estate review (GPT-5.6): this repository shipped a
FunsExternal_Template.lean / FunsExternal.lean pair and NO correspondence
check at all. This commit explains why, and fixes the cause rather than
bolting a check onto a missing input.

THE TEMPLATE WAS BEING DELETED. check.sh removed `*_Template.lean` on every
run and .gitignore excluded it. The stated reason was sound — "the verdict must
depend on COMMITTED BYTES, never on untracked build state", and an untracked
file on LEAN_PATH is exactly that problem. But it is the weaker of the two
available remedies. The ed25519 forks face the identical choice and COMMIT AND
PIN their templates, which removes the untracked state just as completely and
keeps the evidence.

The evidence is the point. 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 here — which is precisely why no check existed.

  · template committed and pinned in model_integrity_sha256
  · .gitignore no longer excludes it
  · check.sh no longer deletes it, and says why at length
  · Phase 0d runs model-correspondence.py — the forks' scanner, including both
    round-8 corrections: a named Lean `section` does not qualify declaration
    names, and an EXTRA AXIOM in the model (an assumption no template asks for)
    fails rather than passing as a silent row
  · MODEL-CORRESPONDENCE.txt committed, pinned, and compared byte-for-byte

Result: 11 externals, every one answered by the pinned model, no UNRESOLVED and
no EXTRA-AXIOM. Negative-tested — deleting one `axiom` from the model yields
`verify_mono.oracle.h_msg|UNRESOLVED` and a non-zero exit; restoring it returns
to green.

AND A REPRODUCIBILITY RESULT, obtained while recovering the deleted template.
charon is not available on this machine (the same wall the reviewer hit), but
SlhVerify.llbc IS committed and Aeneas is installed, so extraction step [2/2]
was re-run alone from the committed LLBC:

    Types.lean: IDENTICAL      Funs.lean: IDENTICAL

The LLBC -> Lean half of the extraction reproduces byte-for-byte from committed
inputs, on demand, by anyone with Aeneas and this repository. This does NOT
close `slh-extraction-unreproduced`: the Rust -> LLBC half still requires
charon, and this was still run by the author. Half the chain, verifiable today.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-03 15:49:16 +02:00
mrwulf
c80c2bba5b provenance: name the pin the machine actually enforces 
Round-8 review (GPT-5.6, register key `slh-provenance-contradictory`, HIGH),
raised in round 7 and unfixed since.

The machine-enforced subject is unambiguous and appears in PROVENANCE.json and
extract.sh:

    fips205-source @ a3ce8e8644fe302019ed7ae271912333f1476de4

It appeared in ZERO markdown files. The prose instead named three other
revisions across four documents — README `797b4ef`, TRUSTED-BASE `3153988`,
ATTESTATION-BASIS `c945821` — so a reader could not tell which Rust the proofs
are about. Subject identity is part of the attestation object: a proof about a
model is not evidence for an unspecified source revision.

  README.md            current snapshot head -> a3ce8e8, with the lineage
                       bea1051 -> 797b4ef -> a3ce8e8 stated explicitly and
                       matching PROVENANCE.json's own upstream_deviation text
  TRUSTED-BASE.md      current snapshot head -> a3ce8e8
  ATTESTATION-BASIS.md subject -> a3ce8e8, AND the "four model_integrity_sha256
                       hashes" claim corrected: only TWO (Types.lean,
                       Funs.lean) are regenerated by extract.sh; the two
                       *External.lean files are hand-maintained and separately
                       byte-pinned. Stating four invites a reproducer to expect
                       extraction to produce files it never touches.

RECORDED-RUN.md IS DELIBERATELY NOT REWRITTEN. It records a run that really
happened on 2026-07-24 against `797b4ef`. Editing the identity of a past run to
match today's pin would falsify the record rather than correct it. It now
carries a header saying so and naming the current pin.

Independent extraction remains UNVERIFIED — no third party has regenerated the
Lean from the Rust. That is unchanged by this commit and is stated where a
reader will meet it.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-03 15:28:57 +02:00
15 changed files with 1358 additions and 38 deletions
Show stats Expand all files Collapse all files

9
.gitignore vendored
View file

@ -1,5 +1,10 @@
*.olean
target/
.lake/
*_Template.lean
SlhVerify.llbc
# *_Template.lean is NO LONGER ignored: it is Aeneas's own statement of what
# the extraction needs from outside, and it is the only artifact against which
# "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.

7
ATTESTATION-BASIS.md
View file

@ -86,8 +86,11 @@ Not performed by any reviewer: `verification/extract.sh`. See condition 9.
> reproduced by an independent reviewer on different hardware; this one has
> not, and it is the claim that ties the Lean model to the Rust source. Until a
> third party re-runs `extract.sh` at the pinned Charon/Aeneas commits and
> obtains the four `model_integrity_sha256` hashes, the correspondence between
> `fips205-source@c945821` and `verification/gen/SlhVerify/*.lean` rests on the
> obtains the two EXTRACTION-GENERATED hashes in `model_integrity_sha256`
> (`Types.lean` and `Funs.lean` — the other two entries, `TypesExternal.lean`
> and `FunsExternal.lean`, are HAND-MAINTAINED and are not regenerated by
> `extract.sh`; they are separately byte-pinned), the correspondence between
> `fips205-source@a3ce8e8` and `verification/gen/SlhVerify/*.lean` rests on the
> author's attestation alone.
The reviewer's instruction on condition 9: if a third party later succeeds at

64
README.md
View file

@ -5,12 +5,13 @@ 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–6 applied)
## STATUS: eleven certificates over the extracted verify model (external review rounds 1–9 applied)
`verification/check.sh` is **green** (exit 0): the model compiles, the proofs
compile, and the audit passes. The audit runs **inside Lean**
(`verification/Proofs/Audit.lean`) and binds four things, each added because an
external reviewer *demonstrated* the button going green without it:
compile, and the audit passes. It binds **seven** things, each added because an
external reviewer *demonstrated* the button going green without it. Three are
checked **inside Lean** by `verification/Proofs/Audit.lean`; the other four are
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
@ -26,9 +27,41 @@ external reviewer *demonstrated* the button going green without it:
*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 four model files and the compiler harness
- **bytes** — Phase 0 sha256-pins the five 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
@ -215,9 +248,15 @@ same boundary.
deviation from upstream is the removal of CI workflows (documented in
that commit); the Aeneas-compat and de-plumbing patches then landed as
transparent, individually-justified commits on top — never upstream.
The current snapshot head is **`797b4ef`** (the round-2 reproducibility
commit — committed `Cargo.lock` + pinned `rust-toolchain.toml` — on top of
de-plumbing round 2, `bea1051`); the model in this repo is extracted from
The current snapshot head is **`a3ce8e8`** — the NIST ACVP SHA2-128s sigVer
vectors plus an expanded differential bridge. That commit is TEST-ONLY: no
verify-path function changed, and re-running `extract.sh` against it
reproduces the two Aeneas-generated model files byte-identically. Its
lineage is `bea1051` (de-plumbing round 2) → `797b4ef` → `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
@ -292,7 +331,7 @@ this repository was created:
one the differential test compares against — is itself patched relative to
upstream `30bac08`. `src/wots.rs` was never modified by any patch commit (an
earlier revision of this README wrongly named it). See the snapshot history
at head `797b4ef` and TRUSTED-BASE.md item 7.
at head `a3ce8e8` and TRUSTED-BASE.md item 7.
## What is claimed (the button is green)
@ -323,7 +362,10 @@ gracefully**: when `systemd-run` is unavailable it falls back to Lean's own
`-M` cap, so the button runs on a stock Linux box without cgroup support — an
external reviewer has run it green that way. Note also that the *empirical
bridge* (`cargo test` in the snapshot repo) needs no Lean toolchain at all and
runs on stable Rust. Extraction is reproducible: the
runs on stable Rust. Extraction is reproducible **in its second stage only**
(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

39
TRUSTED-BASE.md
View file

@ -20,6 +20,43 @@ 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
@ -31,7 +68,7 @@ proceeds and is part of every claim.
7. **Aeneas-compat + de-plumbing patch surface.** The fn-pointer-to-named-
oracle rewrite in `fips205-source` (phase 1) and the two de-plumbing
rounds (index-loop rewrites of the iterator adapters on the verify path,
de-plumbing round 2 at `bea1051`; current snapshot head `3153988`) are
de-plumbing round 2 at `bea1051`; current snapshot head `a3ce8e8`) are
part of the verified surface: the
certificates cover the *patched* verify path, and the patch commits are
the auditable delta from upstream `30bac08`. Each rewrite's equivalence

12
verification/MODEL-CORRESPONDENCE.txt Normal file
View file

@ -0,0 +1,12 @@
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

16
verification/PROVENANCE.json
View file

@ -28,7 +28,7 @@
"aeneas": "aeneas -backend lean -split-files -subdir SlhVerify -dest gen SlhVerify.llbc"
},
"generated_artifacts_sha256": {
"SlhVerify.llbc": "d8ec0b00593eee1778bc4cc0cc1801fb6415bb294425f01384434849c6443f58",
"SlhVerify.llbc": "69666ddc43a4d5e02ca8eaa64eb740f8849eac64e0cd9df76506ab4f68f2af55",
"gen/SlhVerify/Types.lean": "db720b4a30f512e6048212a472e6853b24931a8121cb94c4cf7e6489754d6384",
"gen/SlhVerify/Funs.lean": "7b7de55fd0206142f2678a079a6ed4462292356bc7de08ecd55cac0c76a1da9f"
},
@ -42,15 +42,21 @@
"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": "6108b97d75a8a8e8e0b9bef642ba887ea1ae8b17ba5b7c11d66400bfd2847d9e",
"Proofs/Audit.lean": "3a1540187622c47ee2de4bf1dd2379fbbabf4a3d6ec902f2b602dcf486731691",
"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."
}
}

45
verification/Proofs/Audit.lean
View file

@ -93,6 +93,21 @@ 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)
@ -172,18 +187,39 @@ 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
| none => if nm.isInternal then none else some "Proofs.Audit (this file)"
-- INTERNAL NAMES ARE NO LONGER EXEMPT. They were skipped here, which
-- 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
@ -232,6 +268,13 @@ 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"

158
verification/RECORDED-RUN.md
View file

@ -1,5 +1,15 @@
# Recorded clean run — check.sh + independent cone dump
> **HISTORICAL RECORD — read the pin below, not as the current one.** This
> captures a run that really happened on 2026-07-24 against fips205-source
> `797b4ef`. The CURRENT machine-enforced source pin is `a3ce8e8` (see
> PROVENANCE.json). The revision named throughout this file is deliberately
> left as it was: this is a record of what ran, and editing the identity of a
> past run to match today's pin would be falsifying the record rather than
> correcting it. Round-8 review (GPT-5.6) flagged that the pin appeared in no
> markdown file; the fix is to name it here and correct the CLAIMS elsewhere.
External review round 2 asked for a recorded clean run at the current pin
by a party with the toolchain, so a reviewer who cannot run Lean has current
evidence. Captured 2026-07-24. Pins are in [PROVENANCE.json](PROVENANCE.json).
@ -142,14 +152,146 @@ Certificates proven: fips205.chain_free_loop_eq fips205.wots_loop1_eq fips205.xm
hand-maintained TypesExternal.lean / FunsExternal.lean are
NOT overwritten once they exist)
[Info ] Imported: SlhVerify.llbc
[?25lApplied prepasses: [------------------------------------------------] 0/142 ⠋ Applied prepasses: [------------------------------------------------] 1/142 ⠋ Applied prepasses: [###---------------------------------------------] 11/142 ⠋ Applied prepasses: [#################-------------------------------] 52/142 ⠙ Applied prepasses: [########################################--------] 120/142 ⠙ Applied prepasses: [################################################] 142/142 ✔️
[?25h[?25lTranslated globals: [-------------------------------------------------] 0/10 ⠋ Translated globals: [#################################################] 10/10 ✔️
[?25h[?25lTranslated opaque functions: [----------------------------------------] 0/76 ⠋ Translated opaque functions: [########################################] 76/76 ✔️
[?25h[?25lTranslated transparent functions: [-----------------------------------] 0/42 ⠋ Translated transparent functions: [-----------------------------------] 1/42 ⠙ Translated transparent functions: [#######----------------------------] 9/42 ⠹ Translated transparent functions: [########---------------------------] 10/42 ⠹ Translated transparent functions: [##########-------------------------] 12/42 ⠹ Translated transparent functions: [##########-------------------------] 13/42 ⠹ Translated transparent functions: [###########------------------------] 14/42 ⠸ Translated transparent functions: [############-----------------------] 15/42 ⠸ Translated transparent functions: [##############---------------------] 17/42 ⠸ Translated transparent functions: [###############--------------------] 19/42 ⠸ Translated transparent functions: [################-------------------] 20/42 ⠼ Translated transparent functions: [##################-----------------] 22/42 ⠼ Translated transparent functions: [####################---------------] 24/42 ⠼ Translated transparent functions: [#####################--------------] 26/42 ⠴ Translated transparent functions: [######################-------------] 27/42 ⠴ Translated transparent functions: [#######################------------] 28/42 ⠦ Translated transparent functions: [########################-----------] 29/42 ⠦ Translated transparent functions: [#########################----------] 30/42 ⠦ Translated transparent functions: [#########################----------] 31/42 ⠧ Translated transparent functions: [###########################--------] 33/42 ⠇ Translated transparent functions: [#############################------] 35/42 ⠏ Translated transparent functions: [##############################-----] 36/42 ⠏ Translated transparent functions: [##############################-----] 37/42 ⠋ Translated transparent functions: [###############################----] 38/42 ⠙ Translated transparent functions: [################################---] 39/42 ⠹ Translated transparent functions: [#################################--] 40/42 ⠸ Translated transparent functions: [##################################-] 41/42 ⠸ Translated transparent functions: [###################################] 42/42 ⠼ Translated transparent functions: [###################################] 42/42 ✔️
[?25h[?25lTranslated trait declarations: [--------------------------------------] 0/33 ⠋ Translated trait declarations: [##############------------------------] 13/33 ✔️
[?25h[?25lTranslated trait impls: [---------------------------------------------] 0/50 ⠋ Translated trait impls: [######################-----------------------] 25/50 ✔️
[?25h[?25lPost-processed translated opaque functions: [-------------------------] 0/76 ⠋ Post-processed translated opaque functions: [-------------------------] 1/76 ⠙ Post-processed translated opaque functions: [#########################] 76/76 ✔️
[?25h[?25lPost-processed translated transparent functions: [--------------------] 0/42 ⠋ Post-processed translated transparent functions: [--------------------] 1/42 ⠙ Post-processed translated transparent functions: [###-----------------] 7/42 ⠙ Post-processed translated transparent functions: [####----------------] 9/42 ⠙ Post-processed translated transparent functions: [####----------------] 10/42 ⠹ Post-processed translated transparent functions: [#####---------------] 11/42 ⠹ Post-processed translated transparent functions: [#####---------------] 12/42 ⠸ Post-processed translated transparent functions: [######--------------] 13/42 ⠸ Post-processed translated transparent functions: [######--------------] 14/42 ⠸ Post-processed translated transparent functions: [#######-------------] 15/42 ⠼ Post-processed translated transparent functions: [#######-------------] 16/42 ⠼ Post-processed translated transparent functions: [########------------] 17/42 ⠼ Post-processed translated transparent functions: [#########-----------] 19/42 ⠴ Post-processed translated transparent functions: [#########-----------] 20/42 ⠴ Post-processed translated transparent functions: [##########----------] 21/42 ⠴ Post-processed translated transparent functions: [##########----------] 22/42 ⠦ Post-processed translated transparent functions: [##########----------] 23/42 ⠦ Post-processed translated transparent functions: [###########---------] 25/42 ⠦ Post-processed translated transparent functions: [############--------] 26/42 ⠧ Post-processed translated transparent functions: [############--------] 27/42 ⠧ Post-processed translated transparent functions: [#############-------] 28/42 ⠧ Post-processed translated transparent functions: [##############------] 30/42 ⠇ Post-processed translated transparent functions: [###############-----] 32/42 ⠇ Post-processed translated transparent functions: [###############-----] 33/42 ⠏ Post-processed translated transparent functions: [################----] 34/42 ⠏ Post-processed translated transparent functions: [#################---] 37/42 ⠋ Post-processed translated transparent functions: [##################--] 38/42 ⠋ Post-processed translated transparent functions: [##################--] 39/42 ⠙ Post-processed translated transparent functions: [###################-] 40/42 ⠹ Post-processed translated transparent functions: [###################-] 41/42 ⠸ Post-processed translated transparent functions: [####################] 42/42 ⠼ Post-processed translated transparent functions: [####################] 42/42 ✔️
[?25lApplied prepasses: [------------------------------------------------] 0/142 ⠋
Applied prepasses: [------------------------------------------------] 1/142 ⠋
Applied prepasses: [###---------------------------------------------] 11/142 ⠋
Applied prepasses: [#################-------------------------------] 52/142 ⠙
Applied prepasses: [########################################--------] 120/142 ⠙
Applied prepasses: [################################################] 142/142 ✔️
[?25h[?25lTranslated globals: [-------------------------------------------------] 0/10 ⠋
Translated globals: [#################################################] 10/10 ✔️
[?25h[?25lTranslated opaque functions: [----------------------------------------] 0/76 ⠋
Translated opaque functions: [########################################] 76/76 ✔️
[?25h[?25lTranslated transparent functions: [-----------------------------------] 0/42 ⠋
Translated transparent functions: [-----------------------------------] 1/42 ⠙
Translated transparent functions: [#######----------------------------] 9/42 ⠹
Translated transparent functions: [########---------------------------] 10/42 ⠹
Translated transparent functions: [##########-------------------------] 12/42 ⠹
Translated transparent functions: [##########-------------------------] 13/42 ⠹
Translated transparent functions: [###########------------------------] 14/42 ⠸
Translated transparent functions: [############-----------------------] 15/42 ⠸
Translated transparent functions: [##############---------------------] 17/42 ⠸
Translated transparent functions: [###############--------------------] 19/42 ⠸
Translated transparent functions: [################-------------------] 20/42 ⠼
Translated transparent functions: [##################-----------------] 22/42 ⠼
Translated transparent functions: [####################---------------] 24/42 ⠼
Translated transparent functions: [#####################--------------] 26/42 ⠴
Translated transparent functions: [######################-------------] 27/42 ⠴
Translated transparent functions: [#######################------------] 28/42 ⠦
Translated transparent functions: [########################-----------] 29/42 ⠦
Translated transparent functions: [#########################----------] 30/42 ⠦
Translated transparent functions: [#########################----------] 31/42 ⠧
Translated transparent functions: [###########################--------] 33/42 ⠇
Translated transparent functions: [#############################------] 35/42 ⠏
Translated transparent functions: [##############################-----] 36/42 ⠏
Translated transparent functions: [##############################-----] 37/42 ⠋
Translated transparent functions: [###############################----] 38/42 ⠙
Translated transparent functions: [################################---] 39/42 ⠹
Translated transparent functions: [#################################--] 40/42 ⠸
Translated transparent functions: [##################################-] 41/42 ⠸
Translated transparent functions: [###################################] 42/42 ⠼
Translated transparent functions: [###################################] 42/42 ✔️
[?25h[?25lTranslated trait declarations: [--------------------------------------] 0/33 ⠋
Translated trait declarations: [##############------------------------] 13/33 ✔️
[?25h[?25lTranslated trait impls: [---------------------------------------------] 0/50 ⠋
Translated trait impls: [######################-----------------------] 25/50 ✔️
[?25h[?25lPost-processed translated opaque functions: [-------------------------] 0/76 ⠋
Post-processed translated opaque functions: [-------------------------] 1/76 ⠙
Post-processed translated opaque functions: [#########################] 76/76 ✔️
[?25h[?25lPost-processed translated transparent functions: [--------------------] 0/42 ⠋
Post-processed translated transparent functions: [--------------------] 1/42 ⠙
Post-processed translated transparent functions: [###-----------------] 7/42 ⠙
Post-processed translated transparent functions: [####----------------] 9/42 ⠙
Post-processed translated transparent functions: [####----------------] 10/42 ⠹
Post-processed translated transparent functions: [#####---------------] 11/42 ⠹
Post-processed translated transparent functions: [#####---------------] 12/42 ⠸
Post-processed translated transparent functions: [######--------------] 13/42 ⠸
Post-processed translated transparent functions: [######--------------] 14/42 ⠸
Post-processed translated transparent functions: [#######-------------] 15/42 ⠼
Post-processed translated transparent functions: [#######-------------] 16/42 ⠼
Post-processed translated transparent functions: [########------------] 17/42 ⠼
Post-processed translated transparent functions: [#########-----------] 19/42 ⠴
Post-processed translated transparent functions: [#########-----------] 20/42 ⠴
Post-processed translated transparent functions: [##########----------] 21/42 ⠴
Post-processed translated transparent functions: [##########----------] 22/42 ⠦
Post-processed translated transparent functions: [##########----------] 23/42 ⠦
Post-processed translated transparent functions: [###########---------] 25/42 ⠦
Post-processed translated transparent functions: [############--------] 26/42 ⠧
Post-processed translated transparent functions: [############--------] 27/42 ⠧
Post-processed translated transparent functions: [#############-------] 28/42 ⠧
Post-processed translated transparent functions: [##############------] 30/42 ⠇
Post-processed translated transparent functions: [###############-----] 32/42 ⠇
Post-processed translated transparent functions: [###############-----] 33/42 ⠏
Post-processed translated transparent functions: [################----] 34/42 ⠏
Post-processed translated transparent functions: [#################---] 37/42 ⠋
Post-processed translated transparent functions: [##################--] 38/42 ⠋
Post-processed translated transparent functions: [##################--] 39/42 ⠙
Post-processed translated transparent functions: [###################-] 40/42 ⠹
Post-processed translated transparent functions: [###################-] 41/42 ⠸
Post-processed translated transparent functions: [####################] 42/42 ⠼
Post-processed translated transparent functions: [####################] 42/42 ✔️
[?25h[Info ] Generated: gen/SlhVerify/Types.lean
[Info ] Generated: gen/SlhVerify/FunsExternal_Template.lean
[Info ] Generated: gen/SlhVerify/Funs.lean

1
verification/SlhVerify.llbc Normal file
View file

File diff suppressed because one or more lines are too long

258
verification/check.sh
View file

@ -5,8 +5,14 @@
#
# 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 four model files
# AND the compiler harness `lean-guard` to PROVENANCE.json.
# .lean outside gen/ and Proofs/, and sha256-pin the five model files,
# the committed SlhVerify.llbc, and the self-derived harness set
# (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
@ -17,6 +23,18 @@
# 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.
@ -57,12 +75,25 @@ 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` scaffolding into gen/ on every
# extraction. Those files are UNTRACKED byproducts (a fresh clone has only
# the four pinned model files), nothing imports them, and they would
# otherwise sit on LEAN_PATH unpinned — the same untracked-state problem.
# Remove them here so the gen/ file-set assertion below can be exact.
find "$HERE/gen" -name '*_Template.lean' -delete 2>/dev/null || true
# Aeneas also emits `*_Template.lean` into gen/ on every extraction. This
# script used to DELETE it, reasoning that an untracked file sitting on
# LEAN_PATH is exactly the unpinned-state problem described above. The
# reasoning was right; the remedy was the weaker of the two available. The
# ed25519 forks face the identical choice and COMMIT AND PIN their
# templates, which removes the untracked state just as completely and keeps
# 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)
@ -80,6 +111,16 @@ 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
@ -141,6 +182,38 @@ 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 "
@ -212,6 +285,175 @@ 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."

39
verification/driver-allowlist.txt Normal file
View file

@ -0,0 +1,39 @@
# 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

103
verification/gen/SlhVerify/FunsExternal_Template.lean Normal file
View file

@ -0,0 +1,103 @@
-- 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)

270
verification/inventory-allowlist.txt Normal file
View file

@ -0,0 +1,270 @@
# 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

116
verification/inventory_gate.sh Executable file
View file

@ -0,0 +1,116 @@
#!/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"

259
verification/model-correspondence.py Executable file
View file

@ -0,0 +1,259 @@
#!/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)