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

Compare commits

base: saymrwulf:e8d79241138af49bf4e16032ec3dfe411ad93b16
Branches Tags
saymrwulf:main
...
compare: saymrwulf:c4b275fc93b79e8c11204d73b638f81a40d6e74f
Branches Tags
saymrwulf:main

15 commits
e8d7924113 ... c4b275fc93

Author SHA1 Message Date
mrwulf
c4b275fc93 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
076e326331 docs: state the signing exclusion (round-7 review, ed-scope-exclusions-missing) 
Every certificate here covers the VERIFICATION path; nonce derivation, the
secret scalar multiplication, s-assembly and key generation were never
extracted, never modeled, and no theorem mentions them. That was always true.
No document in this repository said it, which round-7 external review
correctly flagged as a missing required exclusion.

The new final item states it, names the concrete consequence (a nonce-reusing
signer emits key-leaking signatures the proven verifier rightly accepts, every
certificate green), and states the deployment fact for this fork. Appended
rather than renumbered: existing items are cited by number elsewhere.

The cost of the silence is recorded in the item itself: the estate's own
author twice mangled the sign/verify boundary in one session before writing
this. A trust document that states only what IS covered invites over-reading.

Doc-only: TRUSTED-BASE.md is pinned by no harness map and gated by no button.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-06 20:54:44 +02:00
mrwulf
beba65a284 verification: lifted phases run under the buttons shell options, enforced in lift-guard 
A lift is evidence about the shipping gate only if it executes the way the
shipping gate executes. Every button here runs `set -euo pipefail`. Eighteen
lift sites prefixed their driver with `set -uo pipefail` and no -e — four per
fork (selftest-harness, selftest-scalar-statements, selftest-statements twice)
and both accumulator lifts — while sixteen other sites got it right. The estate
did it both ways, which is what made this a defect and not a convention.

Without -e a failing command does not abort: execution continues and the driver
returns the LAST command status. A lifted phase can therefore reach a verdict
the shipping phase would never reach while the self-test reports the gate
"works". selftest_statements.sh:27 claims the tested logic IS the shipping
logic; in this respect it was not.

NO VERDICT CHANGED. Every self-test that passed before passes now, at the same
timings, so -e was not masking a false green at these commits. The defect was
fidelity and the claim is no larger than that.

The durable part is not the 18 edits. lift-guard.sh already inspects every
driver, so it now REFUSES any lift whose driver does not enable errexit and
prints the drivers actual shell options. Negative-tested four ways: no -e
rejects, `set -euo` passes, bare `set -e` passes, no set line at all rejects.
Byte-identical across the four forks. The nineteenth lift someone writes fails
closed rather than silently testing a more permissive shell.

Certified by the round-15 sweep: 50/50 GREEN, six repositories, both buttons
and every self-test, exit 0.

Registered and NOT fixed here: ltl-accumulator-verified has no lift-guard.sh
at all and calls it zero times, so its two lifts remain unguarded — the one
place this class can still recur silently.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-04 12:58:28 +02:00
mrwulf
75b47095fb 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
da04ac5cde lift-guard: eleven more classes, two of them regressions I introduced 
Round-9 review (Claude, N1). The brief said "assume there are more"; there
were eleven, and two were introduced by the round-8 fix itself.

INTRODUCED BY THE ARITHMETIC TOKENISATION — the round-8 fix for a false
NEGATIVE created two false POSITIVES. The interior of `$(( ))` was tokenised
with `[A-Za-z_][A-Za-z0-9_]*`, which starts matching at the letter-bearing tail
of a numeric literal:

    echo $((0x1F))   ->  FATAL: reads x1F
    echo $((1e3))    ->  FATAL: reads e3

Now anchored so a match cannot begin after a digit or word character.

INTRODUCED BY THE INDIRECT-EXPANSION REFUSAL, and this is the one that matters.
`${!...}` has three meanings and `re.search(r'\$\{!')` cannot tell them apart:

    ${!name}                indirect expansion    — genuinely unanalysable
    ${!arr[@]} ${!arr[*]}   array KEY expansion   — ordinary
    ${!prefix*} ${!prefix@} variable-NAME listing — ordinary

A refusal is the most expensive verdict this tool has — it hard-fails the lift
— and it was firing on two ordinary constructs with a diagnostic naming a
feature they do not use. The reviewer found it LIVE: ltl-accumulator
check.sh:274 is `for cert in "${!CONES[@]}"`, so the day lift-guard is ported
there, any lift covering that line would have refused. The four forks carry
five arrays each, so it was one ordinary edit away from firing there too.
Now matched only for genuine `${!name}`.

SEVEN MORE BINDING FORMS the driver uses and the guard demanded anyway:

    let FOO=1 · (( FOO = 1 )) · BAR+=b · FOO[0]=x
    for (( i=0; i<3; i++ )) · select FOO in · getopts "o" FOO

Arithmetic contexts bind as well as read, so `(( i++ ))` and the C-style `for`
now contribute to assigns — without that, the reads-extraction added by the
round-8 fix demanded the very names those expressions assign.

Verified: all eleven silent, genuine `${!n}` still refuses, `$((X+1))` and
`((Y>0))` still caught by name, the whole round-8 matrix unchanged, a genuine
missing variable still fails, and the four lifting self-tests green in all four
forks.

The reviewer also discarded one candidate rather than report it — `i=0;
(( i++ ))` looks like a demand but is silent under driver ⊇ payload, which is
how the self-tests invoke it. That restraint is worth recording: a guard edited
twice for false alarms should not be handed a false alarm by its reviewer.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-03 21:03:35 +02:00
mrwulf
cba5fa3301 lift-guard: close all nine classes the reviewer demonstrated 
Round-8 review (Claude, register key `lift-guard-regex-both-directions`).
Every class reproduced here before fixing, and re-tested after.

THREE FALSE NEGATIVES — the payload reads a name and the guard stayed silent,
which is the direction that costs something, because silence is what the tool
exists to prevent:

  echo $((X + 1))     arithmetic expansion reads X without a `$` before the
  (( Y > 0 ))         name, and the read pattern cannot match it: the
                      character after `$` is `(`. Both contexts are now
                      tokenised. `if [ $((inm + ins)) -eq 0 ]` is already live
                      at check.sh:464 — not lifted today, so latent, not absent.

  n=Q; ${!n}          indirect expansion defeats text analysis outright. The
                      guard now REFUSES the lift rather than passing it. Its
                      contract is "does not miss a dependency"; where it cannot
                      honour that it must say so, not shrug.

SIX FALSE POSITIVES — the driver defines the name and the guard cried wolf.
This direction matters too: a guard that raises false alarms gets edited away,
and then it guards nothing.

  case x in a) FOO=1 ;;      `)` added to the assignment delimiters
  if …; else FOO=1; fi       `else` added
  ! FOO=1                    `!` added
  mapfile -t FOO             binds a name with no `=` at all
  readarray -t FOO           likewise
  printf -v FOO "x"          likewise

The banner also over-claimed. It read as a completeness statement about
LIFTING; it is a completeness statement about VARIABLES. A lifted payload also
inherits functions, shell options, traps and a working directory, and this tool
models none of them — loud failures under `set -e`, but the header now says so
rather than implying otherwise.

Verified: all nine classes behave correctly, a genuine missing variable is
still caught by name, and the seven lifting self-tests pass in dalek plus the
four fast ones in each ported fork.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-03 13:14:20 +02:00
mrwulf
fa9da37f11 audit: bind the scalar statements, and make the accounting identity mean audit 
Closes four round-7/8 findings. Certified by the round-12 sweep: five
repositories, both buttons and every self-test, 48/48 GREEN.

── `scalar-statements-unbound` (gpt, round 7, CRITICAL) ────────────────────
The main button bound its 31 certificates' elaborated statements and reachable
specification bodies. This button bound NONE of its thirteen, while
TRUSTED-BASE item 8 said the audit covers "every certificate" — false across
the 44-certificate surface. The finding was raised in round 7, lost from the
round-8 work list by an F-number collision between two reviewers, and re-raised
in round 8.

Proofs/ScalarAudit.lean is generated from each fork's OWN Audit.lean, so the
canonicalisation is provably the same code: pp.all rendering, whitespace
normalisation, transitive specification closure. check-scalar.sh Phase 3c pins
the block's digest, requires the committed copy to match byte-for-byte so a
mismatch can be DIFFED, and cross-checks the auditor's certificate set against
the button's CERTS array.

  dalek ecf3a3f8 · anza 0d942e47 · risc0 4b550a61 · betrusted 4b550a61

risc0 and betrusted share a digest and that is correct, not a collision: their
ScalarSubSpec.lean differs only in doc prose and in `black_box` entries inside
`simp only [...]` lists AFTER `:= by`. Proof scripts. They bind the same
statements over the same specifications, which is the documented scope.

selftest-scalar-statements.sh ships the two attacks the reviewer asked for:

  ok  gutted statement caught (cone unchanged)
  ok  rewritten specification body caught (name and cone unchanged)

The second rewrites a reachable reference body to `id (…)` — DEFINITIONALLY
EQUAL, so the corpus compiles and every proof typechecks and the cone is
byte-identical. Every earlier phase is blind to it.

── `drv-surface-no-cones` + `accounting-certifies-enumeration` (claude) ────
The round-7 accounting identity proved every kernel constant was ENUMERATED.
The reviewer showed enumeration is not audit: their planted claim WAS
enumerated, as DRV|LTLAccAudit.bait.smuggled|theorem with a real cone, and
nothing examined it — rows had no cone, no allowlist covered them, the
statement digest does not reach instruments, and Phase 2b gates DECLARED
AXIOMS, a different question. "Progress of one step, not two."

DRV rows now carry their axiom cone and are pinned in driver-allowlist.txt by
inventory_gate.sh with a DRV tag — the same implementation that pins the
corpus, in both directions, because a second copy of a coverage gate is a
second thing to drift. The axiom policy is per-surface and enforced per
surface: the corpus admits exactly the sanctioned boundary, the instruments
admit none, and an instrument axiom fails EVEN WHEN ALLOWLISTED.

Verified with the reviewer's own payload, both placements:
  before the walk -> UNCLASSIFIED: DRV|…|bait.smuggled|theorem|Classical.choice,Quot.sound,propext
  after  the walk -> ACCOUNTING FAILED names it (kernel-side)

── `drv-naming-heuristic` (claude, round 7) ────────────────────────────────
Retired as load-bearing rather than patched. The rule admits a theorem whose
name extends a constant declared alongside it, and "breaks in one line" —
declare `def bait`, then `theorem bait.smuggled` walks through. It stays as a
fast readable first check; membership in a committed allowlist is what now
carries the weight, and a new row fails closed whatever it is called.

── what round 11 caught, which was mine ───────────────────────────────────
DRV rows first shipped WITHOUT their originating driver. dalek and anza run
two drivers, each declaring its own `corpus`; keyed on name alone those two
distinct declarations produced one byte-identical row, `sort -u` collapsed
them, and the trailers summed to 37 against 36. The estate had already learned
this on the corpus walk — INV rows carry their module because two modules both
declare CurveFieldProofs.zero_spec — and I rebuilt the record without it.

Rows now carry their driver, and the gate FAILS CLOSED ON DUPLICATE RECORDS
naming the collision: two declarations sharing one entry means one is covered
by the other's, which is exactly how a real declaration hides. The trailer
now checks what the drivers EMITTED, not what survives de-duplication —
conflating "the run was truncated" with "two rows were identical" is what let
a record-format defect present itself as an arithmetic complaint.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-03 12:15:26 +02:00
mrwulf
9c6c3b16a3 correspondence: a named section is not a namespace; an extra axiom is a failure 
Round-8 review (GPT-5.6, register key `section-prefix-bug`, CRITICAL).
Reproduced here exactly before fixing.

model-correspondence.py treated `namespace`, `section` and `end` as one event
class and pushed a named section onto the fully-qualified-name prefix. Lean
does not: `section Foo` opens a scope for `variable`/`open` and gives `end Foo`
a label; it does not turn `bar` into `Foo.bar`. Given a template reading

    section Foo
    axiom bar : Nat
    end Foo

the scanner reported `Foo.bar`, `--names` handed Phase 2d only `Foo.bar`, Lean
resolved an unrelated `Foo.bar` definition elsewhere in the corpus, and the
verdict came back PROVEN. The axiom the extraction ACTUALLY depends on was
never queried. This survived both the fail-closed rewrite and the new
Lean-semantic phase, in a scanner rewritten that same week specifically to
stop dropping things.

AND THE REASON IT STAYED SILENT, which is the half worth keeping. The real
external did not vanish — it landed in the table as EXTRA, the one verdict
that could not fail. A silent bucket beside a fail-closed parser is a slower
way of dropping things. An extra AXIOM is now EXTRA-AXIOM and stops the
button: the model exists to answer the template, so an assumption nothing
asks for is either a parse we got wrong or an assumption nobody governs.
Extra definitions stay tolerated; helpers in a model file are ordinary.

That gate fired on the real corpora on its first run. Each fork's
hand-maintained gen/CurveField/FunsExternal.lean carried AVX2/AVX512 backend
axioms present in no template, no proof, no cone and no allowlist — dead
assumptions in a pinned trusted-base file, reported as EXTRA and therefore
invisible. extract.sh:16 confirms these files are never overwritten by
extraction, so they were hand-written and are removed here:

    dalek 2, anza 3, risc0 4, betrusted 4

Nothing referenced them, so no certificate's cone changes; the trusted base
simply gets smaller. Table rows 64->62, 51->48, 57->53, 56->52, and Phase 2d
independently resolved 62/48/53/52 externals against the regenerated tables.

GEN-MODEL.sha256 and HARNESS.sha256 both move: the model bytes changed, and
the harness pins the table and the gen manifest themselves.

Certified: round-10 sweep, 2h53m, ten instruments in each of four forks,
40/40 GREEN, 0 failing, 0 resource-limited. A full run was required — the
--audit-only staleness gate correctly refused after a source change.

Registered in formal-verification-control/review-findings.tsv as
`section-prefix-bug` and `dead-model-axioms`.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-02 21:29:54 +02:00
mrwulf
cc571bf163 verification: derive lift dependencies instead of hand-keeping them 
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.

Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received

    expected := [".olean"]

one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.

  · lift-guard.sh (new, pinned): derives every variable the lifted payload
    reads, subtracts what the driver defines, and fails AT LIFT TIME naming
    the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
    drops its inline copy. One implementation, not five, since drifting out
    of sync is the entire failure mode.

  · selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
    MANIFESTED leaf module rather than adding a stray file. The stray-file
    attack was a no-op against membership semantics — that is the dead-file
    gate's job, proven by selftest-harness case 8 — and it is also the
    weaker attack, since adding files to Proofs/ must clear a gate that
    editing an already-manifested module does not.

  · Phase 2c's accounting identity moves behind its own marker with its own
    ACCTFAIL verdict, so the phase is liftable by construction rather than
    by a self-test knowing where to stop. Truncating the lift range alone
    would have dropped Phase 2c's own verdict and left the test unable to fail.

  · The other four lifting self-tests assert on the PAYLOAD rather than the
    assembled driver, so a marker in the preamble cannot satisfy a check
    meant to prove the lift landed.

Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-02 13:07:28 +02:00
mrwulf
4fafaab608 Round-7 F1: make model/template correspondence SEMANTIC, and fail closed 
THE DEFECT, as found. GPT-5.6 showed the textual classifier could report
PROVEN for a name Lean resolves to an axiom: a definition appearing only
inside a `/- -/` comment was read as real. Repairing that exposed something
larger and already live. Aeneas wraps long declarations:

    axiom
      curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg

The old scanner required keyword and name on one physical line, so it matched
nothing there and SILENTLY DROPPED the declaration — no MODEL row, no PROVEN
row, no failure. Nine to ten externals per fork had no row at all, and the
tier-A/B `neg` was missing from every committed table while the trust
documents claimed that class was machine-checked. Four pinned tables were
wrong, in four repositories, with the buttons green over them. No attacker
was required; Aeneas's own formatting did it.

The lesson is not "write a better regex". The 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 green covers a gap that is
invisible in the diff.

THE REPAIR, in three layers that each do only what they honestly can.

  · DISCOVERY stays textual, because the template cannot be imported — it
    declares the same names as the model and they would clash. It now strips
    NESTED `/- -/` blocks, reads a name that wraps to a later line, tracks
    namespace/section/end, and FAILS CLOSED: an unparseable keyword exits 2
    naming file and line.
  · Phase 0d keeps the cheap pre-compile comparison against the table.
  · Phase 2d is new and authoritative. After compilation it generates a temp
    Lean driver (the Phase 2b idiom, so no permanent module and no manifest
    churn), imports every non-template gen module, and asks env.find? what
    each external IS: kind and originating module. Model module -> MODEL;
    non-axiom in a generated module -> PROVEN; an axiom outside the model, or
    a name that does not resolve, is a failure. Lean's verdict must equal the
    committed table's, and the answer count must equal the question count so
    a truncated resolver cannot pass.

THE TABLES were regenerated and verified three ways before being committed:
an independently written second scanner agreed on 228/228 rows across the
four forks; all 47 changed rows carry file:line evidence; and the PROVEN row
was put to Lean directly — kind = def, module = CurveField.Funs.

  dalek 54 -> 64 rows   anza 42 -> 51   risc0 48 -> 57   betrusted 47 -> 56

Also corrected: `from_residual` was recorded EXTRA in every fork; the
template does demand it, so it is MODEL. anza carried a spurious `hash|EXTRA`
row from a mis-parse.

NEGATIVE-TESTED. With Phase 0d neutered so Phase 2d was the gate under test,
a PROVEN row edited to MODEL produces:

    SEMANTIC DRIFT: ...neg — table says MODEL, Lean says PROVEN

selftest-correspondence.sh grew 4 cases -> 7: GPT's comment counterexample,
the wrapped declaration that was actually live, and a fail-closed check.

WHAT THIS DOES NOT CLOSE. Phase 2d resolves names in the environment built
from gen/. It establishes what a name IS — assumption or proof, and where —
not that the extraction faithfully represents the Rust. That remains the
Charon/Aeneas trust assumption and no gate here can close it.

Certified: both buttons, all four forks, purged trees. 8/8 green, with
62/48/53/52 externals resolved by Lean and every verdict matching.
 2026-08-02 02:24:15 +02:00
mrwulf
08811d9118 Account for every constant the kernel sees, by set containment 
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.

THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.

TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:

  · `kernel = corpus + instruments + N_DRIVERS`, where the last term was
    justified as a per-driver "self-observation blind spot". It fitted dalek
    and anza (2 drivers, residual 2) and broke on risc0 and betrusted
    (1 driver, residual 2). The residual is 2 everywhere and has nothing to do
    with drivers. This was curve-fitting from a sample of one, and it was named
    as the highest-risk claim in the round-7 self-assessment BEFORE the data
    refuted it.
  · distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
    a name that genuinely denotes two different declarations, in Proofs.Basic
    and Proofs.ConstSpecs, walked by two drivers with separate environments.

THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.

Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.

ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.

CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.

Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.

Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
 2026-08-01 16:10:59 +02:00
mrwulf
92f3229761 P2-c: classify and pin the extraction boundary 
Aeneas emits a *_Template.lean naming everything the extracted code needs
from outside itself — the extraction's own statement of its boundary.
extract.sh has always said, in prose, "after regenerating, diff the template
against the hand-written file". Prose is not a gate, and the diff cannot be
one: the two files legitimately differ in almost every line, holes and
Aeneas comments against real definitions and modeling policy.

MEASURING FIRST CHANGED WHAT THIS ITEM SHOULD BE. The TODO offered two
options — enforce the diff, or pin both files — and the answer turned out to
be neither. Both files were ALREADY byte-pinned by Phase 0b. And two further
things stand here: the generated Funs.lean imports the model and CALLS these
externals, so the Lean compiler enforces their TYPES wherever the extracted
code uses them; and the per-certificate exact cones catch any external that
becomes, or stops being, an assumption anything depends on.

What none of those three sees is the CLASSIFICATION: for each name the
extraction asks for, whether this repository answers with an ASSUMPTION or
with a PROOF. That is the tier-A/B claim the documents make in prose — the
curve calls and the three curve types resolve to proven definitions rather
than axioms, because gen/CurveField/Funs.lean opens `namespace
curve25519_dalek` and so defines the very names Aeneas asks for. Nothing
checked it. A regeneration that renamed one, or a model that quietly
answered one with an axiom instead, would have left the documents claiming a
proof where the repository had an assumption.

Phase 0d recomputes the classification with model-correspondence.py
(namespace-aware, so a definition inside a namespace counts under its full
name) and requires equality with the committed MODEL-CORRESPONDENCE.txt.
UNRESOLVED — the extraction asking for something nothing here provides — is
a hard failure.

  dalek     43 MODEL   8 PROVEN   3 EXTRA
  anza      38 MODEL   0 PROVEN   4 EXTRA   (no CurveSig crate)
  risc0     36 MODEL   8 PROVEN   4 EXTRA
  betrusted 35 MODEL   8 PROVEN   4 EXTRA

selftest-correspondence.sh, five cases, negative-tested by disabling the
comparison. The case that matters is 2: a PROVEN external answered by an
axiom instead. No name changes anywhere, every byte pin still matches, and
it compiles, because the signature is unchanged — before Phase 0d nothing in
the button could tell.

Trap recorded for whoever extends it: case 3 first deleted the PROVEN rows,
which was VACUOUS on anza, since anza has none — it removed nothing, the
table still matched, and the case passed while testing nothing. It now
deletes the first row whatever its verdict AND asserts the file changed.

extract.sh now points at the gate instead of asking a human to look.

Certified by a full sweep: both buttons, all four forks, purged trees,
machine otherwise idle. 8/8 green.
 2026-07-31 17:53:31 +02:00
mrwulf
96765ea721 P2-a': can a declaration hide from the inventory walker? 
Phase 2c exists because a source-regex enumerator proved evadable in
ltl-accumulator-verified: attributed, private and `instance` declarations
and a nested-namespace basename collision all slipped past it. The fix was
to stop reading source text and ask the Lean environment, and that fix was
ported here. But a fix ported is not a fix tested. selftest-inventory.sh
proves the GATE reacts to a difference; it feeds synthetic observations and
never runs the walker. Nothing here had ever asked whether the WALKER SEES
a declaration written in an evasive shape.

selftest-shapes.sh adds all four shapes to an audited module, recompiles it,
runs the real Phase 2c, and requires each one to be NAMED in the
UNCLASSIFIED list. Asserting that the gate merely failed would not do: one
shape surfacing fails the run while the other three ride along unseen. All
four forks report all four. Negative-tested by removing the injection — the
run then reports the walker blind and fails.

The victim module is derived from each repo's own manifest, not named: the
forks do not share a corpus (dalek/anza attack Proofs.Basic, risc0/betrusted
Proofs.DecompressMain), and a hard-coded name would have silently found
nothing on half of them. It must be manifested, must not be an inventory or
audit driver, and must be imported by no other manifest module.

Two notes for whoever edits this next. When re-deriving a leaf module, the
inventory drivers must be excluded from the set of IMPORTERS as well as from
the candidates: they import the whole corpus, so leaving them in makes every
module look imported, finds no leaf, and the test silently has no victim at
all. And a lift of Phase 2c needs SCALAR_SH/SCALAR_MANIFEST alongside
PROOFS, or the coverage check dies on an unbound variable.

New executable pinned in HARNESS.sha256. Certified by a full sweep: both
buttons, all four forks, purged trees, machine otherwise idle. 8/8 green.
 2026-07-31 11:56:05 +02:00
mrwulf
2a0041dd9c P2-a: attack the arithmetic/apex tier boundary itself 
selftest-tiers.sh tests the property this repository exists to assert and
that nothing had tested: the arithmetic tier rests on the three kernel
axioms and NOTHING else. Five cases, all green.

  control   both tiers pass on the untouched tree
  case 1    an apex axiom injected into an ARITHMETIC certificate's proof,
            statement untouched so only the cone moves -> Phase 3 rejects
  case 2    apex boundary widened by one name          -> Phase 3 rejects
  case 3    apex boundary narrowed by one name         -> Phase 3 rejects
  restored  both tiers pass again

Which axiom to inject is derived per fork from this repo's own documented
boundary intersected with the victim module's import closure; no name is
hard-coded, so the same script ships unchanged in all four forks.

Two defects in the test were found and fixed before it was trusted. The
lifted driver first omitted `set -euo pipefail`: the phase's Lean work runs
in a subshell and the phase ends in a bare `echo ""`, so without -e the
subshell's exit 1 was masked and the driver reported GREEN while printing
APEX AUDIT FAILED. And a line-count sanity check passed an empty driver
because the CERTS array padded it; the guard now looks for the diagnostics
it means to provoke. Both are recorded in the script's comments.

The test restores what it touches and rebuilds the module it edits, so it
leaves the tree exactly as it found it. New executable is pinned in
HARNESS.sha256 (Phase 0c fails closed on an unpinned one).

Certified by a full sweep: both buttons, all four forks, from purged trees,
machine otherwise idle. 8/8 green, 0 errors.
 2026-07-31 02:39:34 +02:00
mrwulf
9ab8f15694 verification: build hygiene, and the hidden dependency it exposed (P0-a) 
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.

The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.

WHAT THE PURGE EXPOSED, and it is the point of the whole item:

This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.

Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.

Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.

Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
  - Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
    button never builds. It now scans its manifest by membership and fails
    closed on a missing one.
  - The three inventory drivers were exempted from the dead-file gate and
    compiled in a later phase; after a purge they were absent when Phase 2b
    ran. They are now in the manifest like everything else, and three
    exemptions are gone.

The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.

Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-07-30 22:54:05 +02:00
27 changed files with 2646 additions and 123 deletions
Show stats Expand all files Collapse all files

1
.gitignore vendored
View file

@ -2,3 +2,4 @@
.lake/ .lake/
lake-manifest.json lake-manifest.json
.audit-basis .audit-basis
__pycache__/

8
README.md
View file

@ -18,8 +18,10 @@ coherent proof pyramid in Lean 4 via the Charon/Aeneas transpilation pipeline:
Every layer states its theorems about the **actual Aeneas-transpiled Rust Every layer states its theorems about the **actual Aeneas-transpiled Rust
code** (never about a hand-written re-model), and every claim in the status code** (never about a hand-written re-model), and every claim in the status
table below is backed by a compiled proof plus an axiom audit of the named table below is backed by a compiled proof plus an axiom audit of the named
certificate. Files that do not compile under `verification/check.sh` are not certificate. Files that compile under neither `verification/check.sh` nor
in this repository. `verification/check-scalar.sh` are not in this repository — each shipped
proof source belongs to exactly one button's manifest, and the seam gate
fails the build otherwise.
## Layer status ## Layer status
@ -102,7 +104,7 @@ cones deviates from the boundary above.
source ~/aeneas-toolchain/env.sh source ~/aeneas-toolchain/env.sh
cd verification cd verification
./extract.sh # Rust → LLBC → Lean (regenerates gen/) ./extract.sh # Rust → LLBC → Lean (regenerates gen/)
./check.sh # compiles EVERY shipped file + axiom-audits EVERY certificate ./check.sh # compiles + audits everything the MAIN manifest owns (scalar layer: its own button below)
``` ```
The gen model is ONE merged universe (`gen/CurveField`: field + curve + The gen model is ONE merged universe (`gen/CurveField`: field + curve +

108
TRUSTED-BASE.md
View file

@ -4,8 +4,11 @@ What you must believe for the theorems in this repository to transfer to the
running Rust code. Everything else is machine-checked. running Rust code. Everything else is machine-checked.
1. **Lean 4 kernel** (v4.30.0-rc2) and its three foundational axioms 1. **Lean 4 kernel** (v4.30.0-rc2) and its three foundational axioms
`[propext, Classical.choice, Quot.sound]`. Every certificate is `[propext, Classical.choice, Quot.sound]`. Every arithmetic and scalar
`#print axioms`-audited against exactly this list. certificate is `#print axioms`-audited against exactly this list; the four
apex-tier certificates are audited against this list plus their documented
boundary axioms (the signature-apex item below), both enforced exactly —
nothing more, nothing less — by the button.
2. **mathlib** (prebuilt oleans fetched by `lake exe cache get`). 2. **mathlib** (prebuilt oleans fetched by `lake exe cache get`).
3. **Charon + Aeneas** (pinned `9dd7f23c` / `bf13c42e`): the translation 3. **Charon + Aeneas** (pinned `9dd7f23c` / `bf13c42e`): the translation
from Rust MIR to the Lean model is assumed faithful. The generated from Rust MIR to the Lean model is assumed faithful. The generated
@ -34,6 +37,30 @@ running Rust code. Everything else is machine-checked.
implementation itself is NOT verified. Zero curve, scalar, or backend implementation itself is NOT verified. Zero curve, scalar, or backend
axioms are in any of the four cones. The constructive decompress theorem underneath the full lift axioms are in any of the four cones. The constructive decompress theorem underneath the full lift
(`decompress_of_canonical`) carries the standard three axioms ONLY. (`decompress_of_canonical`) carries the standard three axioms ONLY.
That two-tier separation is enforced, not merely observed. Phase 3
requires every arithmetic certificate's cone to be exactly the three
kernel axioms, and every apex cone to equal the documented set above
exactly. `selftest-tiers.sh` attacks it from both sides: it injects one
of the axioms above into an arithmetic certificate's *proof*, leaving the
statement untouched so that only the cone moves, and it shifts the
documented apex boundary by one name in each direction. All three must be
rejected, and are. Before those cases existed nothing in the harness
distinguished "this tier needs no hash oracle" from "this tier happens
not to use one today".
**What answers each external, and whether it is a proof or an assumption.**
Aeneas emits a `*_Template.lean` naming everything the extracted code needs
from outside itself — the extraction's own statement of its boundary. Phase
0d requires every one of those names to be answered either by the
hand-written model beside it (an assumption, then governed by the axiom gate
and the cones) or by a real definition already in the extracted corpus, and
requires the classification to equal the committed
`MODEL-CORRESPONDENCE.txt` exactly. That second class is the tier-A/B claim
this document makes above — the curve calls and curve types resolving to
proven definitions rather than to axioms — and until 2026-07-31 it was prose
that nothing checked. `selftest-correspondence.sh` attacks it, including the
case that matters most: a PROVEN external answered by an axiom instead,
which changes no name anywhere, leaves every byte pin matching, and compiles
cleanly because the signature is unchanged.
6. **`Scalar52::sub::black_box` (scalar layer)**: this fork's v4.1.3 code 6. **`Scalar52::sub::black_box` (scalar layer)**: this fork's v4.1.3 code
implements the constant-time conditional via a local `black_box` = implements the constant-time conditional via a local `black_box` =
`unsafe { core::ptr::read_volatile(&value) }`. The volatile read is an `unsafe { core::ptr::read_volatile(&value) }`. The volatile read is an
@ -55,6 +82,15 @@ running Rust code. Everything else is machine-checked.
count of shipped sources, so a deleted `.olean` cannot make the scan pass count of shipped sources, so a deleted `.olean` cannot make the scan pass
vacuously. `selftest-axgate.sh` attacks the shipping gate rather than a vacuously. `selftest-axgate.sh` attacks the shipping gate rather than a
copy of it, and was itself negative-tested by removing the gate's error. copy of it, and was itself negative-tested by removing the gate's error.
`selftest-shapes.sh` asks the companion question about Phase 2c: can a
declaration HIDE from the walker? It adds four shapes to an audited module
— `@[simp]`, `private`, an `instance`, and a nested namespace reusing an
audited basename — and requires the walker to report every one of them by
name, not merely to fail. Those four shapes are the ones that defeated a
source-regex enumerator in ltl-accumulator-verified and caused Phase 2c to
be written against the Lean environment instead; until 2026-07-31 the fix
was ported here but never re-attacked. It too was negative-tested, by
removing the injection and confirming the run then reports the walker blind.
**The residue you must still supply yourself:** this binds *declarations*, **The residue you must still supply yourself:** this binds *declarations*,
not *statements*. Nothing in the button establishes that a certificate's not *statements*. Nothing in the button establishes that a certificate's
theorem says what its name — or this document — suggests it says. A theorem says what its name — or this document — suggests it says. A
@ -147,8 +183,10 @@ running Rust code. Everything else is machine-checked.
cross-check, its corpus being mathlib-free. cross-check, its corpus being mathlib-free.
· *The scalar layer is outside this phase.* Thirteen `Proofs/Scalar*` · *The scalar layer is outside this phase.* Thirteen `Proofs/Scalar*`
modules belong to `check-scalar.sh` and are inventoried by nothing. That modules belong to `check-scalar.sh` and sit outside `check.sh`'s
is the two-button seam, still open. Phase 2c prints every uncovered Phase 2c specifically — they are inventoried by `check-scalar.sh`'s own
Phase 2c against `inventory-allowlist-scalar.txt`, both directions. The
two-button seam itself closed 2026-07-30 (see the two-button item below). Phase 2c prints every uncovered
module by name on every run, so the omission is visible rather than module by name on every run, so the omission is visible rather than
inferred. inferred.
@ -212,3 +250,65 @@ running Rust code. Everything else is machine-checked.
condition, and the cap is what protects this machine from the global OOM condition, and the cap is what protects this machine from the global OOM
that killed a session on 2026-07-02. Check the transcript for a `clamping` that killed a session on 2026-07-02. Check the transcript for a `clamping`
line before concluding anything about the mathematics. line before concluding anything about the mathematics.
14. **The verdict depends on committed bytes, not on build state — and what
proving that revealed.** `check.sh` Phase 0a purges every `.olean` under
`verification/` before compiling, forbids stray Lean files at the
verification root (they join the build through `LEAN_PATH`, which contains
`$PWD`), and requires `gen/` to be exactly the model manifest plus its
pinned Aeneas templates. The templates are KEPT here, unlike the companion
SLH-DSA repository which deletes them: `extract.sh` directs the operator to
diff the hand-written external models against them, so they are the
reference for that comparison. The purge does not run under `--audit-only`,
which exists to audit the artifacts a previous full run produced; that is a
further reason an audit-only transcript is not evidence.
**What the purge exposed, on 2026-07-30.** This button had never in its life
compiled the corpus from nothing. The signature apex rests on scalar
arithmetic — `PointLiftSpec` → `ScalarPackSpec` → `ScalarFromBytesSpec`, and
`SigApexSpec` → `ScalarDenote` — and TWELVE of the scalar layer's thirteen
modules are transitive prerequisites of this manifest. They were never
compiled here. The button worked because `check-scalar.sh` had run at some
earlier point and left its `.olean` files behind, and `.olean` is gitignored,
so no `git status` could ever have shown a reader that the verdict rested on
untracked artifacts produced by a different script. Nothing about the proofs
was wrong; the *evidence* was resting on something invisible.
Those twelve are now compiled here as `PREREQ` — **borrowed, not owned**.
`check-scalar.sh` still audits them: their cones, their declaration
inventory, their axiom gate. Phase 1b asserts that every borrowed name
belongs to the other manifest and to neither twice, so the list cannot
quietly become a second claim of ownership.
The general lesson, which is why the purge is worth its minutes: a
verification that never cleans up cannot distinguish "these proofs check"
from "these proofs check given whatever happens to be lying around".
15. **The signing side of this library — not covered, by anything, at all.**
Every certificate in this repository is about the VERIFICATION path: the
apex is `verify_accepts_iff`, an acceptance decision over a message,
public key and candidate signature. Producing a signature is different
code — nonce derivation from the hashed secret key, the scalar
multiplication by the secret, the assembly of `s = r + H(R,A,M)·a mod ℓ` —
and none of it was extracted, none of it is modeled, and no theorem here
mentions it. Key generation likewise. This was always true; until
2026-08-06 no document in this repository said it, which round-7 external
review (GPT-5.6) correctly flagged as a missing required exclusion.
Concretely, so the consequence is not left to the reader: a defective
signer — say one that reuses or biases its nonce, the classic key-leaking
failure — would emit signatures this repository's proven verifier happily
accepts, because they are valid signatures. Every certificate would hold.
The green button says nothing about whether the private key survived the
signing operation.
Deployment note: this fork's proven verify path serves as an independent
quorum member for checking the pacta transparency log's head signatures.
That use needs only the verification half — which is the proven half. No
signing code from this repository is deployed anywhere.
The silence of this document on that point had a measured cost: the
estate's own author, in 2026-08-06 session notes, twice mangled which half
of which library the proofs cover. A trust document that states only what
IS covered invites every reader to over-read it; this item is the
counterweight.

2
verification/GEN-MODEL.sha256
View file

@ -1,4 +1,4 @@
5c8b68cc4b7d4782b467fa91bd21837774c9ac10b906f803d47779e92c15e061 CurveField/FunsExternal.lean 47bd1a4f2522b07a415eadafa25254a82da8061bb38975d07418735a175d8958 CurveField/FunsExternal.lean
c9cc095ef7ec6e1c1e914aec280468ad6bc27bdfb8c7eb0c2b647060a5cc7076 CurveField/FunsExternal_Template.lean c9cc095ef7ec6e1c1e914aec280468ad6bc27bdfb8c7eb0c2b647060a5cc7076 CurveField/FunsExternal_Template.lean
418682624b1591b6b7f5d245efa4312498255459ce47d9b507ab77d32439484a CurveField/Funs.lean 418682624b1591b6b7f5d245efa4312498255459ce47d9b507ab77d32439484a CurveField/Funs.lean
d197d7b9fe515863784eeee59a2fbb69735d10ebcf5cc4e03feb3afbeb53a2b7 CurveField/TypesExternal.lean d197d7b9fe515863784eeee59a2fbb69735d10ebcf5cc4e03feb3afbeb53a2b7 CurveField/TypesExternal.lean

34
verification/HARNESS.sha256
View file

@ -1,18 +1,28 @@
6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt 6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt
d505e4dd9283673e78fb34e25780c94334e03de4ad20400f8289d594ab004daf check-scalar.sh 6fd6275ba35ceb1c6ff38239a8377c0c1cb54dd5ecff83e77edc18f690b9bab4 check-scalar.sh
a8f560f1d46560ee8b90f90ffeeb63b1eccf0afdf1d6652a37a2047786945434 check.sh a45899490e801b7ee0e2f7de0304fa3c756c63b58223fbae8ebdcd381d22b3aa check.sh
afa13c814ba9757de8d59777524e496653351112a1a7037a56f1b0b436b28cf9 extract.sh e782d1c9eef71e97f3c8b97463c16abc6321cc7192dd08a877d8c42473259f84 driver-allowlist.txt
0ea20d74cd359da404ee3be116058374cbb9fd992ed170e5f6c64f8d7a6b2733 GEN-MODEL.sha256 9b24f501b1e92b8ae41db0729ae9fbdbf10438ae89764ed29aa07efc2c3d6dd6 extract.sh
e95982c15c7d754f0c9bcffef95d4c9d4c63589ac51ecdd40870133f377a005c inventory-allowlist-scalar.txt ed3e80ff9eeba730772242bcfb6d6f073623d4ffb86a8587c39e11b81eb6c37a GEN-MODEL.sha256
a0fb8a1a99bc991870b493796bf7bfe09463413298d83c6ae73a269712f96b55 inventory-allowlist-scalar.txt
86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt 86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt
0bb01bc4abaafa8537d460682004d1f336980b28bc4fe1968bcc9c3bc3bc71ba inventory_gate.sh 3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e inventory_gate.sh
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard 736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
4f61c1135f8afc615e686bd267a062229bf349416caebe070eafca510036d1a4 lift-guard.sh
1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py
855134c50bc2ce374eb935058f808264ea6de5ee328ef766956e7e54366f75fe MODEL-CORRESPONDENCE.txt
772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean 772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean
84bc670991fd7456d8c8569ff7b7c32410513a63d3cb7fe8877bb19a82d36a7d Proofs/InventoryCore.lean 5274b1881579e24030b1aed608511640b8ba39f7e6cdb8962ce23bece655c10b Proofs/InventoryCore.lean
4b1d7f5249a80375b4ef849a760ae8e4bbcecf103c3f8b9e8d0a5d5a9ae377fc Proofs/Inventory.lean 660d35343f5673d4bc854787b6a34063c956567bd7e2eb62955a92e3c55bfa6b Proofs/Inventory.lean
6fbeb50d3951c7c5ac593f6dec91096fc798123ed0c500fdfa39fb20b118ea78 Proofs/InventoryScalar.lean f921d028149e41016c75db2d316f26450768c614eb8b8b9764c49da84bbf6fc8 Proofs/InventoryScalar.lean
907616a9386727ec6d030f9ed1c9122d5ccfe4c011b23b781ff728dbb99a2582 Proofs/ScalarAudit.lean
4b550a618b4d4e14be9e7646ae9d515d784d231b34fee39415002a25e370e9b7 SCALAR-AUDIT-MANIFEST.txt
bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh
eb81df6d154b413b243ad282e3b1bfec92fde158a215f89993c08586a121f171 selftest-axgate.sh 6de61b2b08ab6e05c7d38377ea8f70178da4a105bb1df21c6ba6bc05a647090d selftest-axgate.sh
3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh 7822c007d12d7be70003ea9de234102a2c4165cfab65a108e2960e51b87bee82 selftest-correspondence.sh
8ca2bec8cdf88d9b46e6db1481839a60ac684dad242cd33859243750a3360ad4 selftest-harness.sh
1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh 1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh
2c591fb2a0cc50cfdf76c3328e5d72d52b69c02f5b230ebc55c977d6570ecc0f selftest-statements.sh acd485670e1022270819f72fdb1aee9ce044ab9f53158300fccc69982fa37d43 selftest-scalar-statements.sh
fc6d2905871500f2ee9c3f308fd8300cfcd1a7fa854d399d13812f7e2282f1fd selftest-shapes.sh
560987651864f21bb042fc20839a03c34ce7155893b506cf060717e6d645b6c6 selftest-statements.sh
7603b82c9c29a27f6659b8878d1a2e2365afb6541c3c5b2698ab2fee21bb2bde selftest-tiers.sh

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

@ -0,0 +1,54 @@
CurveField/FunsExternal|Array.Insts.CoreHashHash.hash|MODEL
CurveField/FunsExternal|Bool.Insts.CoreConvertFromChoice.from|MODEL
CurveField/FunsExternal|Slice.Insts.CoreFmtDebug.fmt|MODEL
CurveField/FunsExternal|Slice.Insts.SubtleConstantTimeEq.ct_eq|MODEL
CurveField/FunsExternal|U32.Insts.CoreIterRangeStep.backward_checked|MODEL
CurveField/FunsExternal|U32.Insts.CoreIterRangeStep.forward_checked|MODEL
CurveField/FunsExternal|U32.Insts.CoreIterRangeStep.steps_between|MODEL
CurveField/FunsExternal|U64.Insts.SubtleConditionallySelectable.conditional_assign|MODEL
CurveField/FunsExternal|U64.Insts.SubtleConditionallySelectable.conditional_select|MODEL
CurveField/FunsExternal|U64.Insts.SubtleConditionallySelectable.conditional_swap|MODEL
CurveField/FunsExternal|U8.Insts.CoreHashHash.hash|MODEL
CurveField/FunsExternal|U8.Insts.SubtleConstantTimeEq.ct_eq|MODEL
CurveField/FunsExternal|backend.get_selected_backend|MODEL
CurveField/FunsExternal|backend.serial.curve_models.AffineNielsPoint.Insts.SubtleConditionallySelectable.conditional_swap|MODEL
CurveField/FunsExternal|backend.serial.curve_models.ProjectiveNielsPoint.Insts.SubtleConditionallySelectable.conditional_swap|MODEL
CurveField/FunsExternal|backend.serial.scalar_mul.variable_base.mul|MODEL
CurveField/FunsExternal|backend.serial.u64.field.FieldElement51.Insts.CoreCmpEq.assert_fields_are_eq|MODEL
CurveField/FunsExternal|backend.serial.u64.scalar.Scalar52.sub.black_box|MODEL
CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get|MODEL
CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_mut|MODEL
CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_unchecked|MODEL
CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.get_unchecked_mut|MODEL
CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index|MODEL
CurveField/FunsExternal|core.ops.range.RangeFull.Insts.CoreSliceIndexSliceIndexSliceSlice.index_mut|MODEL
CurveField/FunsExternal|edwards.CompressedEdwardsY.from_slice|MODEL
CurveField/FunsExternal|edwards.EdwardsPoint.Insts.CoreCmpEq.assert_fields_are_eq|MODEL
CurveField/FunsExternal|edwards.EdwardsPoint.Insts.CoreIterTraitsAccumSum.sum|MODEL
CurveField/FunsExternal|edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_assign|MODEL
CurveField/FunsExternal|edwards.EdwardsPoint.Insts.SubtleConditionallySelectable.conditional_swap|MODEL
CurveField/FunsExternal|subtle.Choice.Insts.CoreConvertFromU8.from|MODEL
CurveField/FunsExternal|subtle.Choice.Insts.CoreOpsBitBitAndChoiceChoice.bitand|MODEL
CurveField/FunsExternal|subtle.Choice.Insts.CoreOpsBitBitOrChoiceChoice.bitor|MODEL
CurveField/FunsExternal|subtle.Choice.unwrap_u8|MODEL
CurveField/FunsExternal|subtle.ConditionallySelectable.conditional_assign.default|MODEL
CurveField/FunsExternal|subtle.ConditionallySelectable.conditional_swap.default|MODEL
CurveField/TypesExternal|subtle.Choice|MODEL
CurveSig/FunsExternal|core.result.Result.Insts.CoreOpsTry_traitFromResidualResultInfallibleE.from_residual|MODEL
CurveSig/FunsExternal|core.result.Result.Insts.CoreOpsTry_traitTry.branch|MODEL
CurveSig/FunsExternal|curve25519_dalek.edwards.CompressedEdwardsY.as_bytes|PROVEN
CurveSig/FunsExternal|curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg|PROVEN
CurveSig/FunsExternal|curve25519_dalek.edwards.EdwardsPoint.compress|PROVEN
CurveSig/FunsExternal|curve25519_dalek.edwards.EdwardsPoint.vartime_double_scalar_mul_basepoint|PROVEN
CurveSig/FunsExternal|curve25519_dalek.scalar.Scalar.from_bytes_mod_order|PROVEN
CurveSig/FunsExternal|curve25519_dalek.scalar.Scalar.from_bytes_mod_order_wide|PROVEN
CurveSig/FunsExternal|ed25519.Signature.to_bytes|MODEL
CurveSig/FunsExternal|signature.compressed_from_bytes|MODEL
CurveSig/FunsExternal|signature.error.Error.new|MODEL
CurveSig/FunsExternal|verifying.sha512_hash3|MODEL
CurveSig/TypesExternal|curve25519_dalek.edwards.CompressedEdwardsY|PROVEN
CurveSig/TypesExternal|curve25519_dalek.edwards.EdwardsPoint|PROVEN
CurveSig/TypesExternal|curve25519_dalek.scalar.Scalar|PROVEN
CurveSig/TypesExternal|ed25519.Signature|MODEL
CurveSig/TypesExternal|signature.error.Error|MODEL
CORRESPONDENCE-COUNT|53

8
verification/Proofs/Inventory.lean
View file

@ -10,6 +10,7 @@
a split is needed was determined by compiling a probe, per repo. a split is needed was determined by compiling a probe, per repo.
────────────────────────────────────────────────────────────────────────── -/ ────────────────────────────────────────────────────────────────────────── -/
import Proofs.InventoryCore import Proofs.InventoryCore
import Proofs.Audit
import Proofs.Denote import Proofs.Denote
import Proofs.P25519 import Proofs.P25519
import Proofs.ReduceSpec import Proofs.ReduceSpec
@ -67,4 +68,11 @@ def corpus : Array Name :=
`Proofs.SigApexSpec, `Proofs.PointLiftSpec, `Proofs.PointEqSpec, `Proofs.SigApexSpec, `Proofs.PointLiftSpec, `Proofs.PointEqSpec,
`Proofs.DecompressSpec, `Proofs.FromBytesSpec, `Proofs.DecompressMain] `Proofs.DecompressSpec, `Proofs.FromBytesSpec, `Proofs.DecompressMain]
-- The instruments. `Proofs.Audit` is the statement-binding driver: a member of
-- check.sh's compile manifest that was enumerated by NOTHING until 2026-07-31.
-- This module has no index while it is being elaborated, so `emitDrivers` picks
-- its own declarations up as the ones with no originating module.
def drivers : Array Name := #[`Proofs.InventoryCore, `Proofs.Audit]
#eval show MetaM Unit from emitInventory corpus #eval show MetaM Unit from emitInventory corpus
#eval show MetaM Unit from emitDrivers drivers

90
verification/Proofs/InventoryCore.lean
View file

@ -107,4 +107,94 @@ def emitInventory (corpus : Array Name) : MetaM Unit := do
-- received, in both directions. -- received, in both directions.
IO.println s!"INV-COUNT|{sorted.size}" IO.println s!"INV-COUNT|{sorted.size}"
/-- THE INSTRUMENTS' OWN SURFACE.
`emitInventory` walks the CORPUS. It says nothing about the modules that
perform the audit, and until 2026-07-31 nothing else enumerated them either:
the kernel counted 3058 declarations across this button's 43 modules while
the inventory accounted for 3022, and the 36-declaration difference — the
drivers' own machinery — was covered by no allowlist row.
That difference was never a soundness hole. The drivers ARE members of
check.sh's compile manifest, so Phase 2b's kernel-side gate reads their
`.olean`s and an axiom in one is rejected whatever its indentation. What was
missing is the weaker but still real property: that an instrument declares
nothing but inert machinery, and that every declaration the kernel sees is
ACCOUNTED FOR by exactly one of the two walks.
The policy is not "declare nothing" — these files legitimately declare their
own functions. It is that an instrument may not declare an AXIOM (which
would widen the trusted base outside every cone) nor a standalone CLAIM
(which no certificate covers and no allowlist pins). A theorem whose name
extends a constant declared alongside it is an artefact the elaborator
generated for a definition — well-founded recursion emits these — and is
allowed; a theorem whose parent is not a declared constant is not. -/
def emitDrivers (drivers : Array Name) : MetaM Unit := do
let env ← getEnv
let mut idxs : Array Nat := #[]
for m in drivers do
match env.getModuleIdx? m with
| some i => idxs := idxs.push i
| none => throwError "DRIVER SURFACE ERROR: driver module {m} is not imported"
-- Two passes: collect the names first, so the artefact test can ask whether a
-- theorem's parent is itself declared by an instrument.
let mut names : Std.HashSet Name := {}
let mut here : Array (Name × ConstantInfo) := #[]
for (n, ci) in env.constants.toList do
let mine : Bool :=
match env.getModuleIdxFor? n with
| some i => idxs.contains i
| none => true -- declared by the module being elaborated: this driver
if mine then
names := names.insert n
here := here.push (n, ci)
let mut lines : Array String := #[]
for (n, ci) in here do
let k := kindOf ci
if k == "axiom" then
throwError "DRIVER SURFACE VIOLATION: {n} is an axiom declared by the audit \
infrastructure. An instrument may not widen the trusted base."
if k == "theorem" && !names.contains n.getPrefix then
throwError "DRIVER SURFACE VIOLATION: {n} is a standalone theorem declared by \
the audit infrastructure. An instrument may declare definitions \
and whatever the elaborator generates for them — never a claim \
of its own."
-- THE CONE, and it is the second half of the accounting identity.
--
-- Round-8 review (Claude, register keys `drv-surface-no-cones` and
-- `accounting-certifies-enumeration`). These rows carried name and kind
-- only. The round-7 accounting identity then proved every kernel constant
-- was ENUMERATED by one of the two walks — and the reviewer demonstrated
-- that enumeration is not audit: a claim planted in an instrument WAS
-- enumerated, as `DRV|…bait.smuggled|theorem`, with a real cone of
-- [propext, Classical.choice, Quot.sound], and then nothing looked at it.
-- No allowlist row covered the instrument surface, the statement digest
-- does not reach instruments, and Phase 2b gates DECLARED AXIOMS, which is
-- a different question from cones. Their summary: the identity "converted
-- 36 declarations nobody enumerated into 36 declarations nobody examined.
-- That is progress of one step, not two."
--
-- With the cone emitted here and the rows pinned in driver-allowlist.txt
-- by the same gate the corpus uses, the identity and the audit coincide:
-- a planted claim is a new row, and a new row fails closed. The
-- name-prefix rule above is kept as a fast first line of defence but is no
-- longer load-bearing — the reviewer showed it breaks in one line.
let cone ← axiomCone n
let coneStr := ",".intercalate (cone.toList.map (·.toString))
-- THE ORIGINATING DRIVER is part of the record, for the same reason the
-- INV rows carry their module: dalek and anza run TWO drivers, each
-- declaring its own `corpus`, and keyed on name alone those two distinct
-- declarations produced one byte-identical row. `sort -u` then collapsed
-- them, the trailers summed to 37 against 36 unique rows, and the gate
-- reported the surface truncated. Two declarations must never share a
-- record — that is what let a real declaration hide behind another one's
-- entry when this mistake was made on the corpus walk.
lines := lines.push s!"DRV|{env.mainModule}|{n}|{k}|{coneStr}"
let sorted := lines.qsort (· < ·)
for l in sorted do
IO.println l
IO.println s!"DRV-COUNT|{sorted.size}"
end Ed25519Inventory end Ed25519Inventory

5
verification/Proofs/InventoryScalar.lean
View file

@ -20,11 +20,14 @@ import Proofs.ScalarWideSpec
import Proofs.ScalarBytesSpec import Proofs.ScalarBytesSpec
import Proofs.ScalarUnpackSpec import Proofs.ScalarUnpackSpec
import Proofs.ScalarFromBytesSpec import Proofs.ScalarFromBytesSpec
-- The scalar audit driver is in this button's compile manifest, exactly as
-- Proofs.Audit is in the main button's, so the inventory must cover it too.
import Proofs.ScalarAudit
open Lean Ed25519Inventory open Lean Ed25519Inventory
/-- Exactly check-scalar.sh's PROOFS manifest; that script asserts the /-- Exactly check-scalar.sh's PROOFS manifest; that script asserts the
correspondence in both directions. -/ correspondence in both directions. -/
def corpus : Array Name := def corpus : Array Name :=
#[`Proofs.ScalarDenote, `Proofs.ScalarLoop, `Proofs.ScalarSubSpec, `Proofs.ScalarAddSpec, `Proofs.ScalarMulSpec, `Proofs.ScalarMontSpec, `Proofs.ScalarReduceSpec, `Proofs.ScalarFullMulSpec, `Proofs.ScalarMain, `Proofs.ScalarWideSpec, `Proofs.ScalarBytesSpec, `Proofs.ScalarUnpackSpec, `Proofs.ScalarFromBytesSpec] #[`Proofs.ScalarDenote, `Proofs.ScalarLoop, `Proofs.ScalarSubSpec, `Proofs.ScalarAddSpec, `Proofs.ScalarMulSpec, `Proofs.ScalarMontSpec, `Proofs.ScalarReduceSpec, `Proofs.ScalarFullMulSpec, `Proofs.ScalarMain, `Proofs.ScalarWideSpec, `Proofs.ScalarBytesSpec, `Proofs.ScalarUnpackSpec, `Proofs.ScalarFromBytesSpec, `Proofs.ScalarAudit]
#eval show MetaM Unit from emitInventory corpus #eval show MetaM Unit from emitInventory corpus

171
verification/Proofs/ScalarAudit.lean Normal file
View file

@ -0,0 +1,171 @@
import Proofs.ScalarDenote
import Proofs.ScalarLoop
import Proofs.ScalarSubSpec
import Proofs.ScalarAddSpec
import Proofs.ScalarMulSpec
import Proofs.ScalarMontSpec
import Proofs.ScalarReduceSpec
import Proofs.ScalarFullMulSpec
import Proofs.ScalarMain
import Proofs.ScalarWideSpec
import Proofs.ScalarBytesSpec
import Proofs.ScalarUnpackSpec
import Proofs.ScalarFromBytesSpec
import Lean
open Lean Elab Command
namespace Ed25519ScalarAudit
/-- Lean's three kernel axioms. -/
def kernel3 : List Name := [`propext, `Classical.choice, `Quot.sound]
/-- This fork's apex boundary: the hash oracle and wire-format symbols the
signature-level certificates are permitted to rest on, and nothing else.
POLICY CONSTANT — folded into the digest, so widening it moves the hash
and fails the build. -/
def apexExtra : List Name := [] -- the scalar layer has NO apex tier
def apexBoundary : List Name := kernel3 ++ apexExtra
/-- A constant counts as SPECIFICATION if it was declared in a `Proofs.`
module — i.e. hand-written by us, as opposed to the extracted model in
`gen/` (pinned separately by Phase 0). Derived from the environment, not
from a list, so a new specification module cannot appear unnoticed. -/
def specPrefix : String := "Proofs."
/-- Per-certificate expected cone. Arithmetic tier first, apex tier last. -/
def manifest : List (Name × List Name) :=
[ (`ScalarProofs.L_val, kernel3)
, (`ScalarProofs.sub_loop_spec, kernel3)
, (`ScalarProofs.sub_loop1_one_spec, kernel3)
, (`ScalarProofs.sub_val_spec, kernel3)
, (`ScalarProofs.add_val_spec, kernel3)
, (`ScalarProofs.mul_internal_spec, kernel3)
, (`ScalarProofs.part1_spec, kernel3)
, (`ScalarProofs.montgomery_reduce_spec, kernel3)
, (`ScalarProofs.mul_spec, kernel3)
, (`ScalarProofs.scalarImplementation, kernel3)
, (`ScalarProofs.montgomery_mul_spec, kernel3)
, (`ScalarProofs.bytes_unpack_spec, kernel3)
, (`ScalarProofs.from_bytes_wide_spec, kernel3)
]
/-- Deterministic name ordering for the canonical serialization. -/
def sortNames (l : List Name) : List Name :=
((l.map toString).toArray.qsort (· < ·)).toList.map (·.toName)
/-- Whitespace-canonical: every whitespace run collapses to one space, so the
pretty-printer's line wrapping cannot perturb the digest. -/
def normWs (s : String) : String :=
(s.foldl (fun (acc : String × Bool) c =>
let c := if c.isWhitespace then ' ' else c
if c == ' ' then (if acc.2 then acc else (acc.1.push ' ', true))
else (acc.1.push c, false))
("", true)).1
/-- Was `n` hand-written by us, in a `Proofs.` module? -/
def isSpecConst (env : Environment) (n : Name) : Bool :=
match env.getModuleIdxFor? n with
| some idx => (toString env.header.moduleNames[idx.toNat]!).startsWith specPrefix
| none => false
/-- Transitive closure over specification constants, starting from a
certificate's STATEMENT and following DEFINITION bodies (a theorem
contributes its statement only). This discovers the reference definitions —
and any future one — automatically, so a new specification cannot be
introduced, or an existing one redefined, without moving the digest. -/
partial def closureOf (env : Environment) (seen : NameSet) (work : List Name) : NameSet :=
match work with
| [] => seen
| n :: rest =>
if seen.contains n || !isSpecConst env n then closureOf env seen rest
else
let seen := seen.insert n
let more := match env.find? n with
| some (.defnInfo v) => v.value.getUsedConstants.toList ++ v.type.getUsedConstants.toList
| some ci => ci.type.getUsedConstants.toList
| none => []
closureOf env seen (more ++ rest)
/-- Fully-explicit (`pp.all`) rendering, whitespace-canonicalized. Implicit
arguments, instances and universe levels are all made visible, so two
statements that merely LOOK alike cannot share a rendering. -/
def ppAll (e : Expr) : CommandElabM String := do
let s ← Command.liftCoreM <| Meta.MetaM.run' <|
withOptions (fun o => o.setBool `pp.all true) do
return (← Meta.ppExpr e).pretty
return normWs s
elab "auditScalarStatements" : command => do
let env ← getEnv
let mut errs : Array String := #[]
-- (0) The manifest may not permit an axiom outside the two declared tiers.
-- Without this, widening a cone in the manifest would be invisible.
for (cert, cone) in manifest do
for a in cone do
unless apexBoundary.contains a do
errs := errs.push s!"manifest permits {a} for {cert}, which is outside every declared tier"
-- (1) Each certificate must EXIST, be a THEOREM, and have EXACTLY its cone.
-- Exact, not subset: a certificate that stopped depending on the hash
-- oracle is as wrong as one that acquired a new axiom.
for (cert, expected) in manifest do
match env.find? cert with
| none => errs := errs.push s!"{cert}: NOT FOUND (renamed or deleted?)"
| some (.thmInfo _) =>
let got := (← collectAxioms cert).toList
let extras := got.filter (fun a => !expected.contains a)
let missing := expected.filter (fun a => !got.contains a)
unless extras.isEmpty && missing.isEmpty do
errs := errs.push s!"{cert}: cone extra={extras} missing={missing}"
| some (.axiomInfo _) => errs := errs.push s!"{cert}: is an AXIOM, not a proven theorem"
| some (.opaqueInfo _) => errs := errs.push s!"{cert}: is OPAQUE, not a proven theorem"
| some _ => errs := errs.push s!"{cert}: is not a theorem"
unless errs.isEmpty do
throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}"
-- (2) CANONICAL BLOCK: policy, then statements, then specification bodies.
let mut lines : Array String := #[]
lines := lines.push
s!"policy|kernel3={String.intercalate "," ((sortNames kernel3).map toString)}|apexExtra={String.intercalate "," ((sortNames apexExtra).map toString)}|specPrefix={specPrefix}"
let mut specs : NameSet := {}
for (cert, cone) in manifest do
let ci := (env.find? cert).get!
specs := (closureOf env {} ci.type.getUsedConstants.toList).toList.foldl (·.insert ·) specs
lines := lines.push
s!"cert|{cert}|cone={String.intercalate "," ((sortNames cone).map toString)}|type={← ppAll ci.type}"
for nm in sortNames specs.toList do
match env.find? nm with
| none => errs := errs.push s!"specification constant vanished mid-audit: {nm}"
| some ci =>
let isProp ← Command.liftCoreM <| Meta.MetaM.run' <| Meta.isProp ci.type
-- Proof irrelevance: a Prop-valued constant contributes its STATEMENT; a
-- data definition contributes its BODY, which is where fidelity lives.
if isProp then
lines := lines.push s!"spec|{nm}|prop|type={← ppAll ci.type}"
else
match ci with
| .defnInfo v => lines := lines.push s!"spec|{nm}|def|value={← ppAll v.value}"
| _ => lines := lines.push s!"spec|{nm}|other|type={← ppAll ci.type}"
unless errs.isEmpty do
throwError "AUDIT FAILED (fail-closed):\n{String.intercalate "\n" errs.toList}"
-- FAIL CLOSED ON ABSENCE: a manifest that somehow produced no specification
-- constants would emit a block that binds statements only. That is a weaker
-- claim than this file advertises, so it is an error, not a quiet pass.
if specs.toList.isEmpty then
throwError "AUDIT FAILED: statements reached ZERO specification constants — the closure is not doing its job"
logInfo ("SCALAR-AUDIT-MANIFEST-BEGIN\n" ++ String.intercalate "\n" lines.toList ++ "\nSCALAR-AUDIT-MANIFEST-END")
-- check.sh cross-checks its own CERTS array against THIS line, so the two
-- cannot drift apart without the build noticing.
logInfo s!"AUDITED-SCALAR-CERTIFICATES: {String.intercalate " " ((manifest.map (·.1)).map toString)}"
logInfo s!"statement audit PASSED: {manifest.length} certificates (exact cones + elaborated statements), {specs.toList.length} specification constants pinned"
end Ed25519ScalarAudit
open Ed25519ScalarAudit in
auditScalarStatements

23
verification/SCALAR-AUDIT-MANIFEST.txt Normal file
View file

File diff suppressed because one or more lines are too long

93
verification/check-scalar.sh
View file

@ -29,7 +29,7 @@ AENEAS_LEAN="$AENEAS_HOME/backends/lean"
TIMEOUT="${LEAN_TIMEOUT:-300}" TIMEOUT="${LEAN_TIMEOUT:-300}"
CORES="${LEAN_MAX_CORES:-0-3}" CORES="${LEAN_MAX_CORES:-0-3}"
GEN=(CurveField/TypesExternal CurveField/Types CurveField/FunsExternal CurveField/Funs) GEN=(CurveField/TypesExternal CurveField/Types CurveField/FunsExternal CurveField/Funs)
PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec ScalarMulSpec ScalarMontSpec ScalarReduceSpec ScalarFullMulSpec ScalarMain ScalarWideSpec ScalarBytesSpec ScalarUnpackSpec ScalarFromBytesSpec) PROOFS=(ScalarDenote ScalarLoop ScalarSubSpec ScalarAddSpec ScalarMulSpec ScalarMontSpec ScalarReduceSpec ScalarFullMulSpec ScalarMain ScalarWideSpec ScalarBytesSpec ScalarUnpackSpec ScalarFromBytesSpec ScalarAudit )
# Fully-qualified scalar certificates. Each must report EXACTLY the standard # Fully-qualified scalar certificates. Each must report EXACTLY the standard
# three axioms — asserted per certificate, not by counting how many lines of # three axioms — asserted per certificate, not by counting how many lines of
# output happened to match. A count cannot tell you WHICH certificate is clean. # output happened to match. A count cannot tell you WHICH certificate is clean.
@ -226,6 +226,97 @@ if [ "$AUDFAIL" != 0 ]; then
fi fi
echo " ${#CERTS[@]}/${#CERTS[@]} scalar certificates report exactly $EXPECTED" echo " ${#CERTS[@]}/${#CERTS[@]} scalar certificates report exactly $EXPECTED"
# ── Phase 3c: statement + specification binding ─────────────────────────────
# WHAT PHASE 3 DOES NOT ESTABLISH — and why this repository claimed something
# false for four rounds. Round-7 review (GPT-5.6, register key
# `scalar-statements-unbound`, CRITICAL): the main button bound its 31
# certificates' elaborated statements and reachable specification bodies; this
# button bound NONE of its thirteen. Meanwhile TRUSTED-BASE item 8 said the
# audit covers "every certificate" and each README said check.sh audits every
# certificate. Both were false across the 44-certificate repository surface.
#
# The finding was raised in round 7, was lost from the round-8 work list by an
# F-number collision between two reviewers, and was re-raised in round 8. It is
# closed here.
#
# Phase 3 proves each scalar certificate rests on exactly the standard three
# axioms. It does not say WHAT THE THEOREM SAYS. A certificate gutted to a
# tautology of the same cone passes it, and so does one whose reference
# definition has been redefined to BE the extracted code — at which point the
# theorem reads `loop = loop` and the cone is byte-identical.
#
# Proofs/ScalarAudit.lean emits a canonical block holding the policy constants,
# every scalar certificate's fully-elaborated statement (`pp.all`, so implicit
# arguments, instances and universes are all visible), and the body of every
# specification constant transitively reachable from those statements. This
# phase binds its SHA-256, and the block's INPUT is committed too, so a
# mismatch can be DIFFED rather than merely reported.
#
# To rotate deliberately: run this button, take the printed OBSERVED digest,
# and update the constant below AND SCALAR-AUDIT-MANIFEST.txt in the same
# reviewable commit. An author who edits a statement and refreshes the digest
# together is caught by reading the diff, not by this script.
EXPECTED_SCALAR_AUDIT_SHA256="4b550a618b4d4e14be9e7646ae9d515d784d231b34fee39415002a25e370e9b7"
echo "=== Phase 3c: scalar statement + specification binding ==="
cd "$AENEAS_LEAN"
# The compiler's own exit code is the primary signal; the transcript is only
# corroboration. A timeout or a memory clamp exits non-zero WITHOUT printing
# "error:", so grepping the text alone would let it through.
SAUD_RC=0
SAUD_OUT=$(lake env bash -c "
set -uo pipefail
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
cd '$HERE'
LEAN_TIMEOUT=$TIMEOUT LEAN_MEM_MB=8192 '$HERE/lean-guard' Proofs/ScalarAudit.lean 2>&1
" ) || SAUD_RC=$?
if [ "$SAUD_RC" -ne 0 ]; then
echo "SCALAR AUDIT FAILED — Proofs/ScalarAudit.lean exited $SAUD_RC:"
tail -20 <<<"$SAUD_OUT" | sed 's/^/ /'
exit 1
fi
if grep -q 'error:' <<<"$SAUD_OUT"; then
echo "SCALAR AUDIT FAILED — Proofs/ScalarAudit.lean did not elaborate cleanly:"
grep 'error:' <<<"$SAUD_OUT" | head -20 | sed 's/^/ /'
exit 1
fi
SBLOCK=$(awk '/SCALAR-AUDIT-MANIFEST-BEGIN/{f=1;next} /SCALAR-AUDIT-MANIFEST-END/{f=0} f' <<<"$SAUD_OUT")
# FAIL CLOSED ON ABSENCE: no block and a matching block must not share a path.
if [ -z "$SBLOCK" ]; then
echo "SCALAR AUDIT FAILED — no SCALAR-AUDIT-MANIFEST block was emitted (fail-closed)."; exit 1
fi
SGOT_SHA=$(printf '%s\n' "$SBLOCK" | sha256sum | cut -d' ' -f1)
if [ "$SGOT_SHA" != "$EXPECTED_SCALAR_AUDIT_SHA256" ]; then
printf '%s\n' "$SBLOCK" > "$HERE/.scalar-audit-manifest.observed"
echo "SCALAR AUDIT FAILED — audit-manifest digest mismatch."
echo " expected: $EXPECTED_SCALAR_AUDIT_SHA256"
echo " observed: $SGOT_SHA"
echo " A statement, a specification body, or a policy constant changed."
echo " First differences against the committed block:"
diff -u "$HERE/SCALAR-AUDIT-MANIFEST.txt" "$HERE/.scalar-audit-manifest.observed" 2>/dev/null \
| head -30 | sed 's/^/ /' || echo " (SCALAR-AUDIT-MANIFEST.txt absent — cannot diff)"
rm -f "$HERE/.scalar-audit-manifest.observed"
exit 1
fi
# The digest's INPUT must be committed and current, or the diff above would
# compare against a stale reference and quietly mislead the next reader.
if ! printf '%s\n' "$SBLOCK" | cmp -s - "$HERE/SCALAR-AUDIT-MANIFEST.txt"; then
echo "SCALAR AUDIT FAILED — the committed SCALAR-AUDIT-MANIFEST.txt does not match the emitted block."
echo " (the digest matched, so the committed copy is stale — refresh it)"; exit 1
fi
# CROSS-CHECK the certificate list against the CERTS array Phase 3 audits, so a
# certificate cannot be dropped from the auditor's manifest unnoticed.
SAUD_CERTS=$(grep -o 'AUDITED-SCALAR-CERTIFICATES:.*' <<<"$SAUD_OUT" \
| sed 's/AUDITED-SCALAR-CERTIFICATES: //' | tr ' ' '\n' | sort -u | sed '/^$/d')
SBASH_CERTS=$(printf '%s\n' "${CERTS[@]}" | sort -u)
if [ "$SAUD_CERTS" != "$SBASH_CERTS" ]; then
echo "SCALAR AUDIT FAILED — the auditor's certificate set differs from this button's CERTS array:"
diff <(echo "$SBASH_CERTS") <(echo "$SAUD_CERTS") | sed 's/^/ /'
exit 1
fi
echo " ${#CERTS[@]} scalar statements + reachable specification bodies bound, sha256 = $SGOT_SHA"
cd "$HERE"
echo "" echo ""
echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round" echo "SCALAR LAYER COMPLETE: add, sub, mul (Montgomery reduction, double round"
echo "through RR) proven mod ℓ; aggregate certificate scalarImplementation" echo "through RR) proven mod ℓ; aggregate certificate scalarImplementation"

466
verification/check.sh
View file

@ -122,7 +122,41 @@ PROOFS=(
DecompressSpec DecompressSpec
FromBytesSpec FromBytesSpec
DecompressMain DecompressMain
Audit # LAST: imports the certificate corpus and runs the audit Audit # imports the certificate corpus and runs the audit
InventoryCore # inventory machinery (imports only Lean)
Inventory # inventory driver: main chain
)
# Modules this button must COMPILE but does not OWN.
#
# The signature apex rests on scalar arithmetic: PointLiftSpec needs
# ScalarPackSpec which needs ScalarFromBytesSpec, and SigApexSpec needs
# ScalarDenote. Twelve of the scalar layer's thirteen modules are
# transitive prerequisites of this manifest.
#
# Until Phase 0a began purging, this button appeared to work without them:
# it silently consumed .olean files that a previous check-scalar.sh run had
# left lying about. The verdict depended on untracked build state produced
# by a DIFFERENT script — precisely the condition build hygiene exists to
# expose, and it stayed invisible for as long as nothing ever cleaned up.
#
# OWNERSHIP IS UNCHANGED: check-scalar.sh audits these — their cones, their
# declaration inventory, their axiom gate. This button only builds them so
# that running it alone is self-contained. Phase 1b asserts that every name
# here belongs to the OTHER manifest, so this list can never quietly become
# a second claim of ownership.
PREREQ=(
ScalarDenote
ScalarLoop
ScalarSubSpec
ScalarAddSpec
ScalarMulSpec
ScalarMontSpec
ScalarReduceSpec
ScalarFullMulSpec
ScalarWideSpec
ScalarBytesSpec
ScalarUnpackSpec
ScalarFromBytesSpec
) )
# Fully-qualified certificate names; each must be axiom-clean. # Fully-qualified certificate names; each must be axiom-clean.
CERTS=( CERTS=(
@ -186,6 +220,50 @@ for f in "$HERE"/gen/CurveField/*.lean "$HERE"/Proofs/*.lean; do
done done
echo " all sources valid" echo " all sources valid"
# ── Phase 0a: build hygiene ─────────────────────────────────────────────────
# The verdict must depend on COMMITTED BYTES, never on build state left behind
# by an earlier run. An orphan .olean with no source still satisfies an import,
# and .olean is gitignored, so `git status` shows a clean tree while the
# compiler happily reads a module nobody can review.
#
# NOT RUN UNDER --audit-only, for the obvious reason: that mode exists to audit
# the artifacts a previous full run produced, and purging them would make the
# two features destroy each other. That is also why an audit-only transcript is
# not evidence — it has not had this hygiene applied.
if [ "$AUDIT_ONLY" = 0 ]; then
echo "=== Phase 0a: build hygiene ==="
find "$HERE" -name '*.olean' -delete 2>/dev/null || true
echo " purged every .olean under verification/ — this run compiles from source"
else
echo "=== Phase 0a: SKIPPED (--audit-only keeps the artifacts it audits) ==="
fi
# Stray Lean files at the verification/ root join the build through LEAN_PATH,
# which contains $PWD. gen/ and Proofs/ are the only sanctioned locations.
STRAY=$(find "$HERE" -maxdepth 1 \( -name '*.lean' -o -name '*.olean' \) -printf '%f\n' 2>/dev/null || true)
if [ -n "$STRAY" ]; then
echo "$STRAY" | sed 's/^/ STRAY Lean file outside gen\/ and Proofs\/: /'
echo "These join the build via LEAN_PATH and are audited by nothing."
exit 1
fi
# gen/ as a SET, not as a list of names: every .lean under gen/ must be either
# a compiled model module or an Aeneas *_Template.lean. The templates are KEPT
# here, unlike the companion SLH-DSA repo which deletes them: extract.sh directs
# the operator to diff the hand-written external models against them, so they
# are the reference for that comparison and deleting them would destroy it.
GENFAIL=0
while read -r f; do
[ -z "$f" ] && continue
case "$f" in *_Template.lean) continue;; esac
b="${f%.lean}"
case " ${GEN_MODULES[*]} " in (*" $b "*) ;; (*) echo " DEAD MODEL FILE: gen/$f is in no manifest"; GENFAIL=1;; esac
done < <(cd "$HERE/gen" && find . -name '*.lean' -printf '%P\n' | sort)
for m in "${GEN_MODULES[@]}"; do
[ -f "$HERE/gen/$m.lean" ] || { echo " MISSING MODEL FILE: gen/$m.lean is in the manifest but absent"; GENFAIL=1; }
done
[ "$GENFAIL" = 0 ] || { echo "MODEL-SET CHECK FAILED"; exit 1; }
echo " gen/ is exactly the manifest plus its pinned templates"
# ── Phase 0b: pin the extracted model ─────────────────────────────────────── # ── Phase 0b: pin the extracted model ───────────────────────────────────────
# WHY. The certificates are stated ABOUT the extracted model in gen/. Phase 3c # WHY. The certificates are stated ABOUT the extracted model in gen/. Phase 3c
# binds their statements and the specification definitions those statements are # binds their statements and the specification definitions those statements are
@ -242,9 +320,17 @@ echo " $(wc -l < "$HERE/GEN-MODEL.sha256") extracted-model files match their pi
HARNESS_EXTRA=( HARNESS_EXTRA=(
AUDIT-MANIFEST.txt # the statement block Phase 3c's digest is taken over AUDIT-MANIFEST.txt # the statement block Phase 3c's digest is taken over
GEN-MODEL.sha256 # the extracted-model pins Phase 0b enforces GEN-MODEL.sha256 # the extracted-model pins Phase 0b enforces
MODEL-CORRESPONDENCE.txt # the extraction boundary Phase 0d recomputes
inventory-allowlist.txt # the audit surface Phase 2c diffs against inventory-allowlist.txt # the audit surface Phase 2c diffs against
inventory-allowlist-scalar.txt # the scalar layer's audit surface (second button) inventory-allowlist-scalar.txt # the scalar layer's audit surface (second button)
Proofs/Audit.lean # the audit driver: it computes the digest it is judged by Proofs/Audit.lean # the audit driver: it computes the digest it is judged by
driver-allowlist.txt # the INSTRUMENTS' own declaration surface, with cones.
# Not executable, so it would otherwise sit outside the
# harness set — and an allowlist an attacker may rewrite
# pins nothing.
Proofs/ScalarAudit.lean # the scalar audit driver, likewise
SCALAR-AUDIT-MANIFEST.txt # the block the scalar digest is taken over, committed
# so a mismatch can be DIFFED and not merely reported
Proofs/InventoryCore.lean # inventory machinery Proofs/InventoryCore.lean # inventory machinery
Proofs/InventoryScalar.lean # inventory driver: the scalar layer Proofs/InventoryScalar.lean # inventory driver: the scalar layer
Proofs/Inventory.lean # inventory driver: main chain Proofs/Inventory.lean # inventory driver: main chain
@ -274,6 +360,63 @@ if ! ( cd "$HERE" && sha256sum -c --quiet HARNESS.sha256 ) ; then
exit 1 exit 1
fi fi
echo " $(wc -l < "$HERE/HARNESS.sha256") harness files match their pins" echo " $(wc -l < "$HERE/HARNESS.sha256") harness files match their pins"
# ── Phase 0d: template/model correspondence ─────────────────────────────────
# WHAT AENEAS'S TEMPLATE IS. When Aeneas extracts the Rust it also emits, for
# each crate, a *_Template.lean naming everything the extracted code needs from
# OUTSIDE itself. That template is the extraction's own statement of its
# boundary. The hand-written *External.lean beside it is our answer to that
# statement, and `extract.sh` has always said, in prose, "after regenerating,
# diff the template against the hand-written file". Prose is not a gate.
#
# WHAT THIS ADDS, given that three other things already stand here. Phase 0b
# byte-pins both files, so neither can drift from its pin unnoticed. The
# generated Funs.lean imports the model and CALLS these externals, so the Lean
# compiler already enforces their types wherever the extracted code uses them.
# The per-certificate exact cones catch any external that becomes — or stops
# being — an assumption anything depends on. What none of those three sees is
# the CLASSIFICATION: for each name the extraction asks for, whether this
# repository answers with an assumption or with a proof.
#
# That distinction is the tier-A/B claim, and it was prose until 2026-07-31.
# The docs say the curve calls (compress, as_bytes,
# vartime_double_scalar_mul_basepoint, from_bytes_mod_order{,_wide}) and the
# three curve TYPES resolve to the PROVEN model's own definitions rather than
# to axioms — because gen/CurveField/Funs.lean opens `namespace
# curve25519_dalek`, so the names Aeneas asks for are the names it defines.
# Nothing checked it. A regeneration that renamed one of those, or a model that
# quietly answered one with an axiom instead, would have left the documents
# claiming a proof where the repository now had an assumption.
#
# model-correspondence.py recomputes the classification from the files —
# namespace-aware, so a definition inside `namespace curve25519_dalek` counts
# under its full name — and the result must equal the committed table exactly.
# UNRESOLVED is a hard failure in the tool itself: the extraction asking for
# something this repository does not provide at all.
echo "=== Phase 0d: template/model correspondence ==="
CORR_FILE="$HERE/MODEL-CORRESPONDENCE.txt"
if [ ! -s "$CORR_FILE" ]; then
echo "FATAL: MODEL-CORRESPONDENCE.txt is missing or empty — the extraction boundary is unpinned."
exit 1
fi
CORR_OBSERVED=$(cd "$HERE" && python3 model-correspondence.py .) || {
echo "$CORR_OBSERVED" | grep UNRESOLVED | sed 's/^/ /'
echo "MODEL CORRESPONDENCE FAILED: the extraction declares an external that neither"
echo "the hand-written model nor the proven corpus provides."
exit 1
}
if ! diff -u "$CORR_FILE" <(printf '%s\n' "$CORR_OBSERVED") > /tmp/corr-diff.$$ 2>&1; then
echo " MODEL CORRESPONDENCE DRIFT (< committed, > observed):"
sed -n '4,24p' /tmp/corr-diff.$$ | sed 's/^/ /'
rm -f /tmp/corr-diff.$$
echo "MODEL CORRESPONDENCE FAILED: an external changed how it is answered."
exit 1
fi
rm -f /tmp/corr-diff.$$
echo " $(grep -c '|MODEL$' "$CORR_FILE") externals answered by the hand-written model (assumptions)"
echo " $(grep -c '|PROVEN$' "$CORR_FILE") answered by PROVEN definitions in the extracted corpus"
echo " $(grep -c '|EXTRA$' "$CORR_FILE") model declarations beyond what the extraction asks for"
echo ""
# ── Phase 1: stub + axiom-smuggling audit ─────────────────────────────────── # ── Phase 1: stub + axiom-smuggling audit ───────────────────────────────────
echo "=== Phase 1: stub audit ===" echo "=== Phase 1: stub audit ==="
if grep -rn 'by trivial' "$HERE"/Proofs/*Spec*.lean 2>/dev/null; then if grep -rn 'by trivial' "$HERE"/Proofs/*Spec*.lean 2>/dev/null; then
@ -331,6 +474,14 @@ while read -r m; do
[ -z "$m" ] && continue [ -z "$m" ] && continue
[ -f "$HERE/Proofs/$m.lean" ] || { echo " PHANTOM: check-scalar.sh lists $m, which does not exist"; SEAMFAIL=1; } [ -f "$HERE/Proofs/$m.lean" ] || { echo " PHANTOM: check-scalar.sh lists $m, which does not exist"; SEAMFAIL=1; }
done <<<"$SCALAR_MANIFEST" done <<<"$SCALAR_MANIFEST"
# PREREQ is a borrowing, not a claim: every name in it must belong to the
# OTHER manifest. Without this the list could silently grow into a second
# ownership claim over modules this button never audits.
for m in "${PREREQ[@]}"; do
grep -qx "$m" <<<"$SCALAR_MANIFEST" || { echo " PREREQ NOT OWNED BY THE SCALAR BUTTON: $m"; SEAMFAIL=1; }
grep -qx "$m" <<<"$MAIN_MANIFEST" && { echo " PREREQ ALSO CLAIMED HERE: $m"; SEAMFAIL=1; }
done
[ "$SEAMFAIL" = 0 ] && echo " ${#PREREQ[@]} prerequisites borrowed from check-scalar.sh, which audits them"
[ "$SEAMFAIL" = 0 ] && echo " every proof source belongs to exactly one button ($(grep -c . <<<"$MAIN_MANIFEST") here, $(grep -c . <<<"$SCALAR_MANIFEST") scalar)" [ "$SEAMFAIL" = 0 ] && echo " every proof source belongs to exactly one button ($(grep -c . <<<"$MAIN_MANIFEST") here, $(grep -c . <<<"$SCALAR_MANIFEST") scalar)"
[ "$SEAMFAIL" = 0 ] || { echo "SEAM CHECK FAILED"; exit 1; } [ "$SEAMFAIL" = 0 ] || { echo "SEAM CHECK FAILED"; exit 1; }
# ── Phase 2: compile everything shipped ───────────────────────────────────── # ── Phase 2: compile everything shipped ─────────────────────────────────────
@ -374,6 +525,12 @@ lake env bash -c "
} }
for m in ${GEN_MODULES[*]}; do compile \"\$m\"; done for m in ${GEN_MODULES[*]}; do compile \"\$m\"; done
cd '$HERE' cd '$HERE'
# Prerequisites first: owned and audited by check-scalar.sh, built here so
# this run does not depend on artifacts another script may have left behind.
for m in ${PREREQ[*]}; do
[ -f \"Proofs/\$m.lean\" ] || { echo \"MISSING PREREQ: Proofs/\$m.lean\"; exit 1; }
compile \"Proofs/\$m\"
done
for m in ${PROOFS[*]}; do for m in ${PROOFS[*]}; do
[ -f \"Proofs/\$m.lean\" ] || { echo \"MISSING: Proofs/\$m.lean listed in manifest\"; exit 1; } [ -f \"Proofs/\$m.lean\" ] || { echo \"MISSING: Proofs/\$m.lean listed in manifest\"; exit 1; }
compile \"Proofs/\$m\" compile \"Proofs/\$m\"
@ -382,11 +539,8 @@ lake env bash -c "
for f in Proofs/*.lean; do for f in Proofs/*.lean; do
b=\$(basename \"\$f\" .lean) b=\$(basename \"\$f\" .lean)
[ \"\$b\" = AxiomCheck ] && continue [ \"\$b\" = AxiomCheck ] && continue
# Inventory drivers are compiled by Phase 2c, not here: they must elaborate # InventoryScalar belongs to the other button; the rest are in PROOFS above.
# with the corpus already in the environment, and the two of them cannot be case \"\$b\" in InventoryScalar) continue;; esac
# imported together. They are NOT unchecked — Phase 2b reads their compiled
# .olean like every other module, and Phase 0c pins their sources.
case \"\$b\" in Inventory|InventoryBasic|InventoryCore|InventoryScalar) continue;; esac
case \"\$b\" in Scalar*) continue;; esac # scalar layer: checked by check-scalar.sh (coherence pass 2) case \"\$b\" in Scalar*) continue;; esac # scalar layer: checked by check-scalar.sh (coherence pass 2)
case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f not in check manifest\"; exit 1;; esac case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f not in check manifest\"; exit 1;; esac
done done
@ -425,12 +579,16 @@ echo "=== Phase 2b: kernel-side axiom-declaration gate ==="
# audit and the dead-file gate both skip. Nothing is on a hand-kept list. # audit and the dead-file gate both skip. Nothing is on a hand-kept list.
# Cost is ~3 s for the whole corpus (no mathlib import), against ~53 s for a # Cost is ~3 s for the whole corpus (no mathlib import), against ~53 s for a
# single module-importing invocation. # single module-importing invocation.
N_PROOF_SRC=$(ls -1 "$HERE"/Proofs/*.lean 2>/dev/null | wc -l) # MEMBERSHIP, not a glob. Phase 0a purges every .olean and this button
# rebuilds only its own manifest; the scalar layer's artifacts belong to the
# other button. Counting Proofs/*.lean here would demand artifacts this run
# never makes — the spelling-versus-ownership error ScalarPackSpec exposed.
PROOF_OLEANS=$(printf '"%s.olean", ' "${PROOFS[@]}" | sed 's/, $//')
GATE=$(mktemp "$HERE/.axgate-XXXX.lean") GATE=$(mktemp "$HERE/.axgate-XXXX.lean")
{ {
echo "import Lean" echo "import Lean"
echo "open Lean" echo "open Lean"
echo "def expectedModules : Nat := $N_PROOF_SRC" echo "def expected : List String := [$PROOF_OLEANS]"
cat <<'LEANGATE' cat <<'LEANGATE'
run_cmd do run_cmd do
@ -438,22 +596,38 @@ run_cmd do
let mut errs : Array String := #[] let mut errs : Array String := #[]
let mut nMod := 0 let mut nMod := 0
let mut nConst := 0 let mut nConst := 0
for entry in (← dir.readDir) do let mut seen : Std.HashSet (String × Name) := {}
if entry.path.extension == some "olean" then for name in expected do
nMod := nMod + 1 let p := dir / name
let (mod, _) ← readModuleData entry.path -- FAIL CLOSED ON ABSENCE: a manifest module whose artifact is missing makes
for ci in mod.constants do -- this gate vacuous for that module. It must be an error, never a skip.
nConst := nConst + 1 unless (← p.pathExists) do
if ci matches .axiomInfo _ then throwError "COVERAGE: {name} is in the compile manifest but its artifact is absent"
errs := errs.push s!" {entry.fileName}: {ci.name}" nMod := nMod + 1
let (mod, _) ← readModuleData p
-- THE MODULE IS PART OF THE RECORD. Round-9 review (Claude, N2): this gate
-- emitted KERNEL-NAME|<name>, and check.sh compared it against allowlists
-- keyed on module|name — keys that carry the module PRECISELY BECAUSE A
-- NAME IS NOT UNIQUE. This corpus still holds two distinct declarations
-- both called CurveFieldProofs.zero_spec (Proofs.Basic and
-- Proofs.ConstSpecs), which is why the module column was added to INV rows
-- in the first place. Keyed on name alone the identity certified "every
-- declaration NAME the kernel saw is accounted for", not "every
-- declaration" — the same defect as the round-11 DRV regression, sitting
-- inside the check that caught it.
let modName := "Proofs." ++ (name.dropRight 6) -- strip ".olean"
for ci in mod.constants do
nConst := nConst + 1
seen := seen.insert (modName, ci.name)
if ci matches .axiomInfo _ then
errs := errs.push s!" {name}: {ci.name}"
unless errs.isEmpty do unless errs.isEmpty do
throwError "AXIOM DECLARED under Proofs/ (kernel-side gate):\n{String.intercalate "\n" errs.toList}" throwError "AXIOM DECLARED under Proofs/ (kernel-side gate):\n{String.intercalate "\n" errs.toList}"
-- FAIL CLOSED ON ABSENCE: an empty result and a clean result must not share -- FAIL CLOSED ON ABSENCE: an empty result and a clean result must not share
-- a code path. A deleted .olean would make the scan above vacuous; an extra -- a code path. A deleted .olean would make the scan above vacuous; an extra
-- one is orphan litter with no shipped source. -- one is orphan litter with no shipped source.
if nMod != expectedModules then logInfo s!" kernel confirms: {nConst} declarations across {nMod} compiled modules (this button's manifest, by membership), none is an axiom"
throwError "COVERAGE MISMATCH under Proofs/: scanned {nMod} compiled modules, but the directory ships {expectedModules} sources. A missing .olean makes this gate vacuous; an extra .olean is an orphan with no source." for (m, n) in seen do IO.println s!"KERNEL-NAME|{m}|{n}"
logInfo s!" kernel confirms: {nConst} declarations across {nMod} compiled Proofs modules, none is an axiom"
LEANGATE LEANGATE
} > "$GATE" } > "$GATE"
cd "$AENEAS_LEAN" cd "$AENEAS_LEAN"
@ -461,12 +635,13 @@ cd "$AENEAS_LEAN"
# `set -e` a bare `rm` after the call never runs when the gate goes red, which # `set -e` a bare `rm` after the call never runs when the gate goes red, which
# is exactly how this repo accumulated 101 orphan .olean files (fixed today). # is exactly how this repo accumulated 101 orphan .olean files (fixed today).
GATE_RC=0 GATE_RC=0
KERNLOG=$(mktemp /tmp/check-kernel-XXXX.log)
lake env bash -c " lake env bash -c "
set -euo pipefail set -euo pipefail
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\" cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
cd '$HERE' cd '$HERE'
LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' '$GATE' LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' '$GATE'
" || GATE_RC=$? " 2>&1 | tee "$KERNLOG" || GATE_RC=${PIPESTATUS[0]}
rm -f "$GATE" "${GATE%.lean}.olean" rm -f "$GATE" "${GATE%.lean}.olean"
if [ "$GATE_RC" -ne 0 ]; then if [ "$GATE_RC" -ne 0 ]; then
echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above." echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above."
@ -533,7 +708,6 @@ OBS=$(mktemp /tmp/check-inv-obs-XXXX.log)
grep '^INV|' "$INVLOG" > "$OBS" grep '^INV|' "$INVLOG" > "$OBS"
echo "INV-COUNT|${SUM:-0}" >> "$OBS" echo "INV-COUNT|${SUM:-0}" >> "$OBS"
"$HERE/inventory_gate.sh" "$OBS" "$HERE/inventory-allowlist.txt" || INVFAIL=1 "$HERE/inventory_gate.sh" "$OBS" "$HERE/inventory-allowlist.txt" || INVFAIL=1
rm -f "$INVLOG" "$OBS"
# The drivers' corpus lists must together BE the compile manifest, minus the # The drivers' corpus lists must together BE the compile manifest, minus the
# audit infrastructure and the scalar layer. Checked in both directions so a # audit infrastructure and the scalar layer. Checked in both directions so a
@ -555,6 +729,256 @@ for f in "$HERE"/Proofs/*.lean; do
grep -qx "$b" <<<"$COVERED" || echo " NOT INVENTORIED HERE (separate button): Proofs/$b.lean" grep -qx "$b" <<<"$COVERED" || echo " NOT INVENTORIED HERE (separate button): Proofs/$b.lean"
done done
[ "$INVFAIL" = 0 ] || { echo "INVENTORY COVERAGE FAILED"; exit 1; } [ "$INVFAIL" = 0 ] || { echo "INVENTORY COVERAGE FAILED"; exit 1; }
# ── Phase 2c-accounting: every kernel constant is accounted for ─────────────
# SEPARATED FROM PHASE 2c DELIBERATELY, and the reason is a self-test that
# could not pass (round-7 finding F5). This block reads $KERNLOG, created one
# phase earlier in Phase 2b. selftest-shapes.sh lifts "Phase 2c" by text marker
# and runs it standalone; once this block lived inside that range, the lifted
# driver died on its first `$KERNLOG` expansion under `set -u`. The test failed
# loudly in all four forks from the moment the block was added — so the shapes
# property went unverified, though it never produced a false green.
#
# Truncating the lift is NOT the fix: Phase 2c's own verdict
# (`INVENTORY COVERAGE FAILED`) sits after this block, so a shorter range drops
# the phase's ability to fail at all. Instead the block gets its own marker and
# its own verdict, which makes Phase 2c liftable BY CONSTRUCTION rather than by
# the self-test knowing where to stop.
# ── THE ACCOUNTING IDENTITY ───────────────────────────────────────────────
# Every declaration the kernel saw must be accounted for by exactly one walk:
# the corpus inventory, or the instruments' own surface. Until 2026-07-31 the
# two numbers were never compared — the kernel reported 3058 across this
# button's manifest, the inventory accounted for 3022, and the 36-declaration
# difference was the audit drivers' own machinery, covered by no allowlist row
# and by no other check. It was not a soundness hole (the drivers ARE in the
# manifest, so Phase 2b's kernel gate rejects an axiom in one whatever its
# indentation) but it was an unexamined remainder, and an unexamined remainder
# is where the next defect hides.
#
# Stating it as an IDENTITY rather than as two separate counts is what makes it
# fail closed: a declaration that slipped out of both walks leaves the sum
# short, and one counted twice leaves it long.
#
# COUNT DISTINCT CONSTANTS, NOT PHYSICAL DECLARATIONS. The two sides of this
# identity were, at first, counting different things, and the gap was papered
# over with a `+ N_DRIVERS` term justified as a "self-observation blind spot".
# That explanation was WRONG. It fitted dalek and anza (2 drivers, residual 2)
# and broke on risc0 and betrusted (1 driver, residual 2) — the residual is 2
# everywhere and has nothing to do with drivers.
#
# The measured cause: Lean materialises equation lemmas LAZILY, when something
# forces an unfold, and each module that forces one gets its own copy in its
# object file. On every fork, `CurveFieldProofs.denote.eq_1` sits in both
# `SubNegSpec.olean` and `ConstSpecs.olean`, and `CurveFieldProofs.limbsVal.eq_1`
# in both `ReduceSpec.olean` and `ConstSpecs.olean`. The kernel gate reads each
# object file separately and counts both copies; the environment holds one
# constant per name and the inventory sees it once. Hence exactly 2.
#
# So the gate now reports DISTINCT names and the fudge term is gone. This still
# fails closed: a declaration missing from both walks leaves the sum short, and
# one counted twice leaves it long. A future mismatch must be explained — as
# this one finally was — never absorbed into a constant.
# PIN THE INSTRUMENTS' OWN SURFACE, in both directions, with the SAME gate the
# corpus uses (round-8 review, Claude, register keys `drv-surface-no-cones`,
# `accounting-certifies-enumeration`, and it retires `drv-naming-heuristic` as
# load-bearing).
#
# The accounting identity below proves every kernel constant is ENUMERATED by
# one of the two walks. The reviewer demonstrated that enumeration is not
# audit: their planted claim WAS enumerated, carried a real axiom cone, and
# nothing examined it — DRV rows had no cone and no allowlist covered them.
# They now carry the cone, and this gate pins them exactly as the corpus is, so
# a claim smuggled into an instrument is a NEW ROW and a new row fails closed
# whatever it is called.
"$HERE/inventory_gate.sh" "$INVLOG" "$HERE/driver-allowlist.txt" DRV || ACCTFAIL=1
N_DRV=$(grep -c '^DRV|' "$INVLOG" || true)
DRV_TRAILERS=$(grep -c '^DRV-COUNT|' "$INVLOG" || true)
DRV_SUM=$(grep '^DRV-COUNT|' "$INVLOG" | cut -d'|' -f2 | paste -sd+ - | bc)
KERN_NAMES=$(mktemp /tmp/check-kernnames-XXXX.txt)
ACCT_NAMES=$(mktemp /tmp/check-acctnames-XXXX.txt)
LC_ALL=C grep '^KERNEL-NAME|' "$KERNLOG" | cut -d'|' -f3 | LC_ALL=C sort -u > "$KERN_NAMES"
{ LC_ALL=C awk -F'|' '/^INV\|/{print $3}' "$HERE/inventory-allowlist.txt"
LC_ALL=C grep '^DRV|' "$INVLOG" | cut -d'|' -f3
} | LC_ALL=C sort -u > "$ACCT_NAMES"
# 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/check-kernpairs-XXXX.txt)
ACCT_PAIRS=$(mktemp /tmp/check-acctpairs-XXXX.txt)
LC_ALL=C grep '^KERNEL-NAME|' "$KERNLOG" | 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|' "$INVLOG" | 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_NAMES" "$ACCT_NAMES")
if [ "$DRV_TRAILERS" -ne "$N_DRIVERS" ]; then
echo " DRIVER SURFACE INCOMPLETE: expected a trailer from each of the $N_DRIVERS driver(s), saw $DRV_TRAILERS"
ACCTFAIL=1
elif [ "${DRV_SUM:-0}" != "$N_DRV" ]; then
echo " DRIVER SURFACE TRUNCATED: trailers sum to ${DRV_SUM:-0}, observed $N_DRV lines"
ACCTFAIL=1
elif [ ! -s "$KERN_NAMES" ]; then
echo " ACCOUNTING FAILED: Phase 2b reported no constant names — the scan was vacuous"
ACCTFAIL=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/^/ /'
ACCTFAIL=1
else
echo " accounting: every one of $(wc -l < "$KERN_NAMES") 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 "$KERN_NAMES" "$ACCT_NAMES" "$KERN_PAIRS" "$ACCT_PAIRS"
ACCTFAIL=${ACCTFAIL:-0}
[ "$ACCTFAIL" = 0 ] || { echo "ACCOUNTING FAILED"; rm -f "$INVLOG" "$OBS" "$KERNLOG"; exit 1; }
rm -f "$INVLOG" "$OBS" "$KERNLOG"
rm -f "$INVLOG" "$OBS" "$KERNLOG"
# ── Phase 2d: SEMANTIC model/template correspondence ────────────────────────
# Phase 0d asks a text scanner what the extraction's boundary looks like. This
# phase asks LEAN what it actually is, and requires the two to agree.
#
# WHY BOTH. Round-7 review (GPT-5.6, finding F1) showed the textual classifier
# could be made to report PROVEN for a name Lean resolves to an axiom — a
# definition inside a `/- -/` comment was read as real. Worse, and found while
# repairing that: Aeneas wraps long declarations, and the old scanner required
# keyword and name on one physical line, so it SILENTLY DROPPED them. Nine to
# ten externals per fork had no row at all, and one — the tier-A/B `neg` — was
# missing from every committed table while the docs claimed that class was
# machine-checked.
#
# A source scanner cannot decide this question. Whether a name resolves to an
# assumption or to a proof is a property of the elaborated ENVIRONMENT: it turns
# on imports, namespaces, `export`, aliases and shadowing, none of which are
# visible to a regex. So the scanner's job is now only DISCOVERY — what does the
# template ask for — and even that fails closed. The verdict comes from Lean.
#
# The template itself is deliberately not imported: it declares the same names
# as the hand-written model and the two would clash. Discovery is therefore
# unavoidably textual, which is exactly why `model-correspondence.py` must stop
# rather than skip on anything it cannot parse.
echo "=== Phase 2d: semantic model/template correspondence ==="
SEMNAMES=$(mktemp /tmp/check-semnames-XXXX.txt)
SEMOUT=$(mktemp /tmp/check-semout-XXXX.txt)
python3 "$HERE/model-correspondence.py" --names "$HERE" > "$SEMNAMES" || {
echo "MODEL CORRESPONDENCE FAILED: could not enumerate the extraction's externals."
rm -f "$SEMNAMES" "$SEMOUT"; exit 1; }
SEM=$(mktemp "$HERE/.semcheck-XXXX.lean")
{
# Import every generated module that is not a template. There are no name
# clashes between crates (verified), and the crate roots transitively pull
# their own models, so this is the same environment the proofs are built on.
for m in $(cd "$HERE/gen" && find . -name '*.lean' -not -name '*_Template.lean' \
| sed 's|^\./||; s|\.lean$||; s|/|.|g' | sort); do
echo "import $m"
done
cat <<'LEANSEM'
open Lean in
#eval show CoreM Unit from do
let env ← getEnv
let path := System.FilePath.mk (← IO.getEnv "SEMNAMES").get!
for line in (← IO.FS.lines path) do
let parts := line.splitOn "|"
if h : parts.length = 2 then
let rel := parts[0]!
let nm := parts[1]!.toName
match env.find? nm with
| none => IO.println s!"SEM|{rel}|{parts[1]!}|ABSENT|-"
| some ci =>
let kind := match ci with
| .axiomInfo _ => "axiom"
| .defnInfo _ => "def"
| .thmInfo _ => "theorem"
| .opaqueInfo _ => "opaque"
| .inductInfo _ => "inductive"
| .ctorInfo _ => "ctor"
| .recInfo _ => "recursor"
| .quotInfo _ => "quot"
let mdl := match env.getModuleIdxFor? nm with
| some i => toString env.header.moduleNames[i]!
| none => "<current>"
IO.println s!"SEM|{rel}|{parts[1]!}|{kind}|{mdl}"
LEANSEM
} > "$SEM"
cd "$AENEAS_LEAN"
SEM_RC=0
SEMNAMES="$SEMNAMES" lake env bash -c "
set -uo pipefail
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
cd '$HERE'
LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' '$SEM'
" > "$SEMOUT" 2>&1 || SEM_RC=$?
cd "$HERE"
rm -f "$SEM" "${SEM%.lean}.olean"
if [ "$SEM_RC" -ne 0 ]; then
echo "SEMANTIC CORRESPONDENCE FAILED: the resolver did not run."
tail -12 "$SEMOUT" | sed 's/^/ /'
rm -f "$SEMNAMES" "$SEMOUT"; exit 1
fi
# Every name the extraction asks for must have been resolved, and its Lean
# verdict must equal the committed table's. The mapping is deliberately strict:
# resolves into the hand-written model module -> MODEL
# resolves to a NON-AXIOM in a generated module -> PROVEN
# anything else -> failure
SEMFAIL=0
NSEM=$(grep -c '^SEM|' "$SEMOUT" || true)
NWANT=$(grep -c '|' "$SEMNAMES" || true)
if [ "$NSEM" -ne "$NWANT" ]; then
echo " SEMANTIC CORRESPONDENCE TRUNCATED: asked about $NWANT externals, Lean answered for $NSEM"
SEMFAIL=1
fi
while IFS='|' read -r _tag rel name kind mdl; do
[ "$_tag" = SEM ] || continue
want=$(awk -F'|' -v r="$rel" -v n="$name" '$1==r && $2==n {print $3}' "$HERE/MODEL-CORRESPONDENCE.txt")
case "$kind:$mdl" in
axiom:"${rel//\//.}") got=MODEL ;;
*:"${rel//\//.}") got=MODEL ;;
axiom:*) got=AXIOM-OUTSIDE-MODEL ;;
ABSENT:*) got=UNRESOLVED ;;
*) got=PROVEN ;;
esac
if [ -z "$want" ]; then
echo " SEMANTIC DRIFT: $rel|$name resolves ($kind in $mdl) but has NO ROW in MODEL-CORRESPONDENCE.txt"
SEMFAIL=1
elif [ "$want" != "$got" ]; then
echo " SEMANTIC DRIFT: $rel|$name — table says $want, Lean says $got ($kind in $mdl)"
SEMFAIL=1
fi
done < "$SEMOUT"
rm -f "$SEMNAMES" "$SEMOUT"
if [ "$SEMFAIL" != 0 ]; then
echo "SEMANTIC CORRESPONDENCE FAILED: the committed table does not match what Lean resolves."
exit 1
fi
echo " $NWANT externals resolved by Lean; every verdict matches the committed table"
echo ""
# ── Phase 3: axiom audit of every certificate ─────────────────────────────── # ── Phase 3: axiom audit of every certificate ───────────────────────────────
echo "=== Phase 3: axiom audit ===" echo "=== Phase 3: axiom audit ==="
EXPECTED="[propext, Classical.choice, Quot.sound]" EXPECTED="[propext, Classical.choice, Quot.sound]"

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

@ -0,0 +1,50 @@
# driver-allowlist.txt — THE AUDIT INSTRUMENTS' OWN DECLARATION SURFACE,
# pinned with axiom cones, gated by inventory_gate.sh with the DRV tag:
# the same implementation that pins the corpus, in both directions.
#
# Round-8 review (Claude, register keys drv-surface-no-cones and
# accounting-certifies-enumeration). The accounting identity proved every
# kernel constant was ENUMERATED. It did not prove any of them was
# EXAMINED: a claim planted in an instrument was enumerated, carried a
# real cone, and nothing looked at it. These rows close that gap.
#
# Regenerate deliberately, never by hand:
# scratchpad/gen-driver-allowlists.sh
# and read the diff — a new row is a declaration that appeared in an
# instrument, which is exactly the event this file exists to surface.
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1._sparseCasesOn_3|def|propext
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_10|def|
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_12|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_1|def|
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_3|def|propext
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_6|def|propext
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1.match_8|def|
DRV|Proofs.Inventory|Ed25519Audit._aux_Proofs_Audit___elabRules_Ed25519Audit_commandAuditStatements_1|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Audit.apexBoundary|def|
DRV|Proofs.Inventory|Ed25519Audit.apexExtra|def|
DRV|Proofs.Inventory|Ed25519Audit.closureOf._sparseCasesOn_1|def|propext
DRV|Proofs.Inventory|Ed25519Audit.closureOf._unsafe_rec|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Audit.closureOf.match_1|def|propext
DRV|Proofs.Inventory|Ed25519Audit.closureOf.match_4|def|
DRV|Proofs.Inventory|Ed25519Audit.closureOf|opaque|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Audit.commandAuditStatements|def|
DRV|Proofs.Inventory|Ed25519Audit.isSpecConst.match_1|def|
DRV|Proofs.Inventory|Ed25519Audit.isSpecConst|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Audit.kernel3|def|
DRV|Proofs.Inventory|Ed25519Audit.manifest|def|
DRV|Proofs.Inventory|Ed25519Audit.normWs|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Audit.ppAll|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Audit.sortNames|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Audit.specPrefix|def|
DRV|Proofs.Inventory|Ed25519Inventory.axiomCone|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Inventory.emitDrivers.match_1|def|Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Inventory.emitDrivers|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Inventory.emitInventory._sparseCasesOn_3|def|propext
DRV|Proofs.Inventory|Ed25519Inventory.emitInventory.match_1|def|
DRV|Proofs.Inventory|Ed25519Inventory.emitInventory.match_3|def|propext
DRV|Proofs.Inventory|Ed25519Inventory.emitInventory.match_6|def|
DRV|Proofs.Inventory|Ed25519Inventory.emitInventory|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|Ed25519Inventory.kindOf.match_1|def|
DRV|Proofs.Inventory|Ed25519Inventory.kindOf|def|
DRV|Proofs.Inventory|corpus|def|
DRV|Proofs.Inventory|drivers|def|

10
verification/extract.sh
View file

@ -18,6 +18,16 @@
# After regenerating, diff the templates against the hand-written files: # After regenerating, diff the templates against the hand-written files:
# diff gen/CurveField/FunsExternal_Template.lean gen/CurveField/FunsExternal.lean # diff gen/CurveField/FunsExternal_Template.lean gen/CurveField/FunsExternal.lean
# #
# That diff is a READING aid, not a gate — the two files legitimately differ in
# almost every line (the template holds holes and Aeneas's own comments; the
# model holds real definitions and the modeling policy). What IS enforced, by
# check.sh Phase 0d, is the classification: every name the template declares
# must be answered either by the hand-written model or by a real definition in
# the proven corpus, and which of the two must match MODEL-CORRESPONDENCE.txt.
# Regenerate that table with `python3 model-correspondence.py .` and commit the
# change deliberately — a proof silently becoming an assumption is exactly what
# the phase exists to stop.
#
# Usage: ./extract.sh # Usage: ./extract.sh
set -euo pipefail set -euo pipefail

29
verification/gen/CurveField/FunsExternal.lean
View file

@ -301,40 +301,11 @@ def U64.Insts.SubtleConditionallySelectable.conditional_swap
def backend.get_selected_backend : Result backend.BackendKind := def backend.get_selected_backend : Result backend.BackendKind :=
ok backend.BackendKind.Serial ok backend.BackendKind.Serial
/-- [curve25519_dalek::backend::vector::scalar_mul::variable_base::spec_avx512ifma_avx512vl::mul]:
Source: 'curve25519-dalek/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-6:2
Visibility: public -/
axiom backend.vector.scalar_mul.variable_base.spec_avx512ifma_avx512vl.mul
: edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
/-- [curve25519_dalek::backend::vector::scalar_mul::variable_base::spec_avx2::mul]:
Source: 'curve25519-dalek/src/backend/vector/scalar_mul/variable_base.rs', lines 3:0-6:2
Visibility: public -/
axiom backend.vector.scalar_mul.variable_base.spec_avx2.mul
: edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
/-- [curve25519_dalek::backend::serial::scalar_mul::variable_base::mul]: /-- [curve25519_dalek::backend::serial::scalar_mul::variable_base::mul]:
Source: 'curve25519-dalek/src/backend/serial/scalar_mul/variable_base.rs', lines 11:0-48:1 -/ Source: 'curve25519-dalek/src/backend/serial/scalar_mul/variable_base.rs', lines 11:0-48:1 -/
axiom backend.serial.scalar_mul.variable_base.mul axiom backend.serial.scalar_mul.variable_base.mul
: edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint : edwards.EdwardsPoint → scalar.Scalar → Result edwards.EdwardsPoint
/-- [curve25519_dalek::backend::vector::scalar_mul::vartime_double_base::spec_avx512ifma_avx512vl::mul]:
Source: 'curve25519-dalek/src/backend/vector/scalar_mul/vartime_double_base.rs', lines 14:0-17:2
Visibility: public -/
axiom
backend.vector.scalar_mul.vartime_double_base.spec_avx512ifma_avx512vl.mul
:
scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result
edwards.EdwardsPoint
/-- [curve25519_dalek::backend::vector::scalar_mul::vartime_double_base::spec_avx2::mul]:
Source: 'curve25519-dalek/src/backend/vector/scalar_mul/vartime_double_base.rs', lines 14:0-17:2
Visibility: public -/
axiom backend.vector.scalar_mul.vartime_double_base.spec_avx2.mul
:
scalar.Scalar → edwards.EdwardsPoint → scalar.Scalar → Result
edwards.EdwardsPoint
/-- [curve25519_dalek::backend::serial::curve_models::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::curve_models::ProjectiveNielsPoint}::conditional_swap]: /-- [curve25519_dalek::backend::serial::curve_models::{impl subtle::ConditionallySelectable for curve25519_dalek::backend::serial::curve_models::ProjectiveNielsPoint}::conditional_swap]:
Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 295:0-311:1 Source: 'curve25519-dalek/src/backend/serial/curve_models/mod.rs', lines 295:0-311:1
Visibility: public -/ Visibility: public -/

24
verification/inventory-allowlist-scalar.txt
View file

@ -1893,3 +1893,27 @@ INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_7|theorem|Cl
INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_8|theorem|Classical.choice,Quot.sound,propext INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_8|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_9|theorem|Classical.choice,Quot.sound,propext INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec._proof_1_9|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec|theorem|Classical.choice,Quot.sound,propext INV|Proofs.ScalarWideSpec|ScalarProofs.montgomery_mul_spec|theorem|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.apexBoundary|def|
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.apexExtra|def|
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1|def|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_1|def|
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_10|def|
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_12|def|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_3|def|propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_6|def|propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1.match_8|def|
INV|Proofs.ScalarAudit|Ed25519ScalarAudit._aux_Proofs_ScalarAudit___elabRules_Ed25519ScalarAudit_commandAuditScalarStatements_1._sparseCasesOn_3|def|propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.closureOf|opaque|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.closureOf.match_1|def|propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.closureOf.match_4|def|
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.closureOf._sparseCasesOn_1|def|propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.closureOf._unsafe_rec|def|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.commandAuditScalarStatements|def|
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.isSpecConst|def|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.isSpecConst.match_1|def|
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.kernel3|def|
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.manifest|def|
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.normWs|def|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.ppAll|def|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.sortNames|def|Classical.choice,Quot.sound,propext
INV|Proofs.ScalarAudit|Ed25519ScalarAudit.specPrefix|def|

72
verification/inventory_gate.sh
View file

@ -9,7 +9,35 @@
# self-test exercises this exact script — the tested logic IS the shipping # self-test exercises this exact script — the tested logic IS the shipping
# logic. # logic.
# #
# Usage: inventory_gate.sh <observed-lean-output> <allowlist-file> # 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: # Fail-closed in BOTH directions:
# UNCLASSIFIED — constant in the environment, absent from the allowlist # UNCLASSIFIED — constant in the environment, absent from the allowlist
@ -21,17 +49,41 @@
# ───────────────────────────────────────────────────────────────────────────── # ─────────────────────────────────────────────────────────────────────────────
set -uo pipefail set -uo pipefail
export LC_ALL=C # byte-order collation: sort/comm must agree with Lean's String order export LC_ALL=C # byte-order collation: sort/comm must agree with Lean's String order
obs_file="$1"; allow_file="$2" 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
OBS=$(grep '^INV|' "$obs_file" | sort -u) # The trailer is an OUTPUT-INTEGRITY check: it must equal the number of rows
N_OBS=$(printf '%s' "$OBS" | grep -c '^INV|' || true) # the driver(s) actually emitted, BEFORE de-duplication. Comparing it to the
TRAILER=$(grep '^INV-COUNT|' "$obs_file" | tail -1 | cut -d'|' -f2) # de-duplicated count conflates "a run was truncated" with "two rows were
if [ -z "$TRAILER" ] || [ "$TRAILER" != "$N_OBS" ]; then # identical", and the second is a record-format defect that must be fixed at
echo " INVENTORY TRUNCATED: trailer=${TRAILER:-absent}, observed $N_OBS lines" # 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 exit 1
fi fi
ALLOW=$(grep '^INV|' "$allow_file" | sort -u) ALLOW=$(grep "^$TAG|" "$allow_file" | sort -u)
FAILGATE=0 FAILGATE=0
UNCLASS=$(comm -23 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW")) UNCLASS=$(comm -23 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
STALE=$(comm -13 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW")) STALE=$(comm -13 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
@ -51,7 +103,7 @@ fi
# two independent gates on the same property, deliberately. # two independent gates on the same property, deliberately.
AXLINES=$(printf '%s\n' "$OBS" | grep '|axiom|' || true) AXLINES=$(printf '%s\n' "$OBS" | grep '|axiom|' || true)
if [ -n "$AXLINES" ]; then if [ -n "$AXLINES" ]; then
echo " AXIOM SURFACE DRIFT: the audited corpus must declare no axioms; observed:" echo " AXIOM SURFACE DRIFT: $WHAT must declare no axioms; observed:"
printf '%s\n' "$AXLINES" | sed 's/^/ /' printf '%s\n' "$AXLINES" | sed 's/^/ /'
FAILGATE=1 FAILGATE=1
fi fi
@ -60,5 +112,5 @@ fi
# sanctioned axiom" when ported, which is the accumulator's policy; here the # sanctioned axiom" when ported, which is the accumulator's policy; here the
# audited corpus permits NONE, and a success line describing a different rule # audited corpus permits NONE, and a success line describing a different rule
# is how an assertion quietly stops meaning anything. # is how an assertion quietly stops meaning anything.
[ "$FAILGATE" = 0 ] && echo " inventory gate: $N_OBS constants, environment == allowlist, zero axioms declared in the audited corpus" [ "$FAILGATE" = 0 ] && echo " $LABEL: $N_OBS constants, environment == allowlist, zero axioms declared in $WHAT"
exit "$FAILGATE" exit "$FAILGATE"

221
verification/lift-guard.sh Executable file
View file

@ -0,0 +1,221 @@
#!/usr/bin/env bash
# lift-guard.sh <payload> <driver> [<phase-label>]
#
# Every VARIABLE the LIFTED PAYLOAD reads must be one the DRIVER defines.
#
# VARIABLES ONLY — and the emphasis is a round-8 correction (Claude, N1). A
# lifted payload also inherits FUNCTIONS, shell options, traps and a working
# directory from the script it was cut out of. This tool models none of those.
# A lifted phase calling a function defined in a neighbouring phase fails with
# `command not found`, loud under `set -e`, which is why it is not urgent; but
# the banner used to read as a completeness claim about lifting and it is a
# completeness claim about variables.
#
# Prints the offending names and exits 1 if any are missing.
#
# ───────────────────────────────────────────────────────────────────────────
# WHY THIS EXISTS — 2026-08-02
#
# Five of this repository's self-tests work by lifting one phase out of
# check.sh and running it standalone against a deliberately corrupted tree.
# That is the right design: the test then attacks the SHIPPING gate rather
# than a re-implementation of it. But a lifted phase is a fragment, and it
# reads variables its neighbours defined. Each self-test therefore carries a
# hand-written preamble supplying them.
#
# A hand-written preamble is a hand-kept list, and hand-kept lists drift. Twice
# in two days a phase grew a dependency and no preamble was told:
#
# · Phase 2c grew an accounting block reading $KERNLOG, a file Phase 2b
# creates. selftest-shapes.sh died on its first expansion under `set -u`.
# It could not pass on any fork from the moment that block was added.
#
# · Phase 2b changed from globbing Proofs/*.lean to reading the $PROOFS
# membership manifest — the spelling-versus-ownership fix ScalarPackSpec
# forced. selftest-axgate.sh's preamble was never told. Bash does NOT
# error on an unset array expansion under `set -u`; it expands to nothing,
# so `printf '"%s.olean", ' "${PROOFS[@]}"` silently produced
# expected := [".olean"]
# — one entry, empty name — and the gate's own fail-closed absence check
# rejected it. The baseline went red and both attack cases were then
# rejected for the WRONG REASON.
#
# Both failed loudly rather than passing vacuously, which is the only reason
# they were not false assurance. That is luck, not design: a missing variable
# that happens to make an ATTACK case die still looks like the attack being
# caught, and only the substring assertions in each `expect` helper stand
# between that and a green test measuring nothing.
#
# The fix for the CLASS is to stop maintaining the list by hand. This tool
# derives the requirement from the two artifacts themselves, so a phase that
# grows a new dependency fails AT LIFT TIME, naming it, instead of dying
# mid-run or — worse — passing for the wrong reason.
#
# WHAT IT IS NOT. This is a shell-text approximation, not a bash parser. It
# still cannot see a name built at runtime or passed through `eval`, and it
# models variables only — not functions, shell options, traps or the working
# directory a lifted phase also inherits. It is a tripwire on failure modes
# that actually occurred, not a proof of closure.
#
# Where it CANNOT bound the reads it refuses rather than staying silent:
# indirect expansion (`${!name}`) is detected and fails the lift. That is the
# round-8 correction — a guard whose contract is "does not miss a dependency"
# must say so when it cannot honour it, instead of shrugging.
# ───────────────────────────────────────────────────────────────────────────
set -euo pipefail
PAYLOAD="${1:?usage: lift-guard.sh <payload> <driver> [phase-label]}"
DRIVER="${2:?usage: lift-guard.sh <payload> <driver> [phase-label]}"
LABEL="${3:-the lifted phase}"
for f in "$PAYLOAD" "$DRIVER"; do
[ -s "$f" ] || { echo "FATAL: lift-guard: '$f' is missing or empty."; exit 1; }
done
# ── The driver must run the phase under the SAME shell options as the button ──
# A lift is only evidence about the shipping gate if it executes the way the
# shipping gate executes. Every button in this estate runs `set -euo pipefail`.
# Eighteen lift sites prefixed their driver with `set -uo pipefail` and no -e
# (four per fork, two in the accumulator) while sixteen others got it right, so
# the estate did it both ways and the self-tests silently ran a more permissive
# shell than the phase they claim to test: without -e a failing command does not
# abort, execution continues, and the driver returns the LAST command's status.
# A lifted phase can therefore reach a verdict the shipping phase would never
# reach, while the self-test reports the gate "works".
#
# This lives here rather than in each self-test because the same defect appeared
# in eighteen places and would return the nineteenth time someone writes a lift.
# Checked on the DRIVER, which is what bash actually executes; the payload is
# lifted verbatim and carries no `set` line of its own.
if ! grep -qE '^[[:space:]]*set[[:space:]]+-[a-z]*e' "$DRIVER"; then
echo "FATAL: lift-guard: the driver for $LABEL does not enable errexit."
echo " The button runs 'set -euo pipefail'; this driver does not set -e, so"
echo " the lifted phase would run past a failure the shipping phase aborts on"
echo " and the test would report a verdict the button cannot produce."
echo " Driver's shell options:"
grep -nE '^[[:space:]]*set[[:space:]]+-' "$DRIVER" | sed 's/^/ /' || echo " (none)"
exit 1
fi
UNBOUND=$(python3 - "$PAYLOAD" "$DRIVER" <<'PYGUARD'
import re, sys
payload = open(sys.argv[1]).read()
driver = open(sys.argv[2]).read()
# What the payload READS. Deliberately over-approximates: a name mentioned in a
# comment costs one lifted definition, a name missed costs a broken self-test.
reads = set(re.findall(r'\$\{?([A-Za-z_][A-Za-z0-9_]*)', payload))
# ARITHMETIC CONTEXTS READ NAMES WITHOUT A `$`. Round-8 review (Claude, N1):
# echo $((X + 1)) reads X
# (( Y > 0 )) && ... reads Y
# and the pattern above cannot see either, because the character after `$` is
# `(`. This is the guard's own failure mode — a phase growing a dependency the
# guard is blind to — and `if [ $((inm + ins)) -eq 0 ]` is already live in
# check.sh's Phase 1b. Not lifted today, which made it latent, not absent.
for expr in (re.findall(r'\$\(\((.*?)\)\)', payload, re.S)
+ re.findall(r'(?<!\$)\(\((.*?)\)\)', payload, re.S)):
# NOT PRECEDED BY A DIGIT OR WORD CHARACTER. Round-9 review (Claude, N1):
# `$((0x1F))` was read as a variable `x1F`, and `$((1e3))` as `e3`, because
# the pattern happily starts matching at the letter-bearing tail of a
# numeric literal. Two false alarms introduced by the round-8 fix for a
# false NEGATIVE — the guard was made to see more and started seeing things
# that are not there, which is the failure mode that gets a guard deleted.
for tok in re.findall(r'(?<![0-9A-Za-z_])[A-Za-z_][A-Za-z0-9_]*', expr):
reads.add(tok)
# What the DRIVER defines, in every form these scripts actually use.
# `TIMEOUT=$T; CORES="$C"` is one line with two assignments, and a
# start-anchored pattern sees only the first.
# An assignment may open a line or follow `;`, `&&`, `||`, `then`, `do`, `{`,
# and — round-8 review (Claude, N1) — `else`, a `case` branch's `)`, and `!`.
# Six false-positive classes were demonstrated. A guard that cries wolf gets
# edited away, so over-strictness here is not the safe direction.
assigns = set(re.findall(
r'(?:^|;|&&|\|\||\)|!|\bthen\b|\bdo\b|\belse\b|\{)\s*'
r'([A-Za-z_][A-Za-z0-9_]*)=', driver, re.M))
# `mapfile`/`readarray` and `printf -v` bind a name without an `=` at all.
assigns |= set(re.findall(
r'\b(?:mapfile|readarray)\b(?:\s+-[A-Za-z]\s*\S*)*\s+([A-Za-z_][A-Za-z0-9_]*)',
driver))
assigns |= set(re.findall(r'\bprintf\b[^\n]*?\s-v\s+([A-Za-z_][A-Za-z0-9_]*)', driver))
# SEVEN MORE BINDING FORMS — round-9 review (Claude, N1). Each was a false
# alarm: the driver binds the name and the guard demanded it anyway. Listed in
# the order reported, so the next reader can check the list against that report.
assigns |= set(re.findall(r'\blet\s+([A-Za-z_][A-Za-z0-9_]*)\s*=', driver))
assigns |= set(re.findall(r'\bselect\s+([A-Za-z_][A-Za-z0-9_]*)\s+in\b', driver))
assigns |= set(re.findall(r'\bgetopts\b\s+\S+\s+([A-Za-z_][A-Za-z0-9_]*)', driver))
assigns |= set(re.findall(r'(?:^|;|&&|\|\||\)|!|\bthen\b|\bdo\b|\belse\b|\{)\s*'
r'([A-Za-z_][A-Za-z0-9_]*)\+=', driver, re.M)) # BAR+=b
assigns |= set(re.findall(r'(?:^|;|&&|\|\||\)|!|\bthen\b|\bdo\b|\belse\b|\{)\s*'
r'([A-Za-z_][A-Za-z0-9_]*)\[[^]]*\]=', driver, re.M)) # FOO[0]=x
# Arithmetic CONTEXTS BIND TOO — `(( FOO = 1 ))`, `(( i++ ))`, and the C-style
# `for (( i=0; i<3; i++ ))`. The reads-extraction above adds every identifier it
# finds inside `(( ))`, so without this the guard demands the very names those
# expressions assign.
for expr in (re.findall(r'\$\(\((.*?)\)\)', driver, re.S)
+ re.findall(r'(?<!\$)\(\((.*?)\)\)', driver, re.S)):
assigns |= set(re.findall(r'(?<![0-9A-Za-z_])([A-Za-z_][A-Za-z0-9_]*)\s*(?:=[^=]|\+\+|--)', expr))
assigns |= set(re.findall(r'\b(?:export|declare|local|readonly)\s+(?:-\w+\s+)*'
r'([A-Za-z_][A-Za-z0-9_]*)', driver))
assigns |= set(re.findall(r'\bfor\s+([A-Za-z_][A-Za-z0-9_]*)\s+in\b', driver))
# `read` binds names too, and it is almost never at end of line: the shape that
# matters here is `while read -r n; do`. An end-anchored pattern misses it and
# the guard then demands a definition for a loop variable the payload binds
# itself — a false alarm, which is the one failure a guard cannot afford.
for m in re.finditer(r'\bread\b((?:\s+-\w+)*(?:\s+[A-Za-z_][A-Za-z0-9_]*)+)', driver):
assigns |= set(re.findall(r'[A-Za-z_][A-Za-z0-9_]*', m.group(1)))
# Names the driver INHERITS rather than defines: the shell's own, and the ones
# `source ~/aeneas-toolchain/env.sh` puts in the environment. Keep this list
# short and justified — every entry is a hole in the guard.
ENV = {'PWD', 'HOME', 'PATH', 'IFS', 'PIPESTATUS', 'BASH_SOURCE', 'FUNCNAME',
'LINENO', 'RANDOM', 'SECONDS', 'OSTYPE', 'HOSTNAME', 'USER', 'SHELL',
'TMPDIR', 'LC_ALL', 'LANG', 'BASH_REMATCH', 'REPLY', 'PS4',
'AENEAS_HOME', 'LEAN_PATH', 'LEAN_MEM_MB', 'LEAN_TIMEOUT',
'LEAN_MAX_CORES'}
# INDIRECT EXPANSION DEFEATS TEXT ANALYSIS, so say so instead of staying
# silent. `n=Q; echo "${!n}"` reads Q, and no amount of pattern-matching
# recovers that from the source. The guard's contract is that it does not miss
# a dependency; where it cannot honour that it must refuse, not shrug.
# `${!...}` HAS THREE MEANINGS IN BASH and only one of them is indirection:
# ${!name} indirect expansion — genuinely unanalysable
# ${!arr[@]} ${!arr[*]} array KEY expansion — ordinary, and LIVE at
# ltl-accumulator check.sh:274, `for cert in
# "${!CONES[@]}"`
# ${!prefix*} ${!prefix@} variable-NAME listing — ordinary
# Round-9 review (Claude, N1). The round-8 refusal tested for `${!` and could
# not tell them apart, so a legitimate construct would have hard-failed a lift
# with a diagnostic naming a feature it does not use. A refusal is the most
# expensive verdict this tool has; it must be reserved for the case it is
# actually about.
INDIRECT = re.compile(r'\$\{!\s*[A-Za-z_][A-Za-z0-9_]*\s*\}')
if INDIRECT.search(payload):
print('INDIRECT-EXPANSION')
else:
print(' '.join(sorted(n for n in reads - assigns - ENV if not n.isdigit())))
PYGUARD
)
if [ "$UNBOUND" = "INDIRECT-EXPANSION" ]; then
cat <<EOF
FATAL: $LABEL uses indirect expansion (\${!name}).
The set of variables it reads cannot be derived from its text, so this
guard cannot certify that the lift carries them. Rewrite the phase
without indirection, or lift it with a driver that is known-complete by
other means and say so in the self-test.
EOF
exit 1
fi
if [ -n "$UNBOUND" ]; then
cat <<EOF
FATAL: $LABEL reads variables this lift does not define: $UNBOUND
Either lift their definitions too — VERBATIM from check.sh, with a
sed range, so this test cannot drift away from the button's idea of
them — or end the lift range before the block that uses them.
Do NOT stub them: a stub makes the test measure something the button
never runs, which is how a self-test becomes decoration.
EOF
exit 1
fi

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)

126
verification/selftest-axgate.sh
View file

@ -27,9 +27,19 @@ FAILURES=0
# reality rather than assuming a pristine checkout. # reality rather than assuming a pristine checkout.
TREE_AT_START="$(cd "$(dirname "$0")/.." && git status --porcelain -- verification/Proofs)" TREE_AT_START="$(cd "$(dirname "$0")/.." && git status --porcelain -- verification/Proofs)"
# Declared before the trap: cleanup reads it, and under `set -u` an unset name
# turns any early abort into a second, misleading failure.
VICTIM=""
cleanup() { cleanup() {
rm -f "$ATTACK" "${ATTACK%.lean}.olean" rm -f "$ATTACK" "${ATTACK%.lean}.olean"
[ -f "$STASH/FeQ.olean" ] && mv "$STASH/FeQ.olean" "$HERE/Proofs/FeQ.olean" [ -f "$STASH/FeQ.olean" ] && mv "$STASH/FeQ.olean" "$HERE/Proofs/FeQ.olean"
# Restore the poisoned module on EVERY path. A self-test that aborts midway
# must not leave a proof module carrying `axiom cheat : ∀ P, P` behind it.
if [ -n "$VICTIM" ] && [ -f "$STASH/victim.lean" ]; then
cp "$STASH/victim.lean" "$HERE/Proofs/$VICTIM.lean"
[ -f "$STASH/victim.olean" ] && cp "$STASH/victim.olean" "$HERE/Proofs/$VICTIM.olean"
fi
rm -rf "$STASH" rm -rf "$STASH"
rm -f "$HERE"/.axgate-*.lean "$HERE"/.axgate-*.olean rm -f "$HERE"/.axgate-*.lean "$HERE"/.axgate-*.olean
} }
@ -37,30 +47,48 @@ trap cleanup EXIT INT TERM
# Phase 2b, lifted verbatim from the shipping button. # Phase 2b, lifted verbatim from the shipping button.
DRIVER="$STASH/phase2b.sh" DRIVER="$STASH/phase2b.sh"
PAYLOAD="$STASH/payload.sh"
# Stop at the NEXT phase marker, whatever it is called. A hardcoded terminator
# ("...to Phase 3") silently widens the moment a phase is inserted between the
# two: adding Phase 2c made this driver swallow 2c as well and die on variables
# that phase expects check.sh to have defined, which surfaced as the BASELINE
# failing — a self-test blaming a gate for its own extraction bug.
awk '/^# ── Phase 2b/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 2b/{exit} f{print}' \
"$HERE/check.sh" > "$PAYLOAD"
{ {
echo 'set -euo pipefail' echo 'set -euo pipefail'
echo 'source ~/aeneas-toolchain/env.sh' echo 'source ~/aeneas-toolchain/env.sh'
echo "HERE=\"$HERE\"" echo "HERE=\"$HERE\""
echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"' echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\"" echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\""
# Stop at the NEXT phase marker, whatever it is called. A hardcoded # THE COMPILE MANIFEST. Phase 2b used to glob Proofs/*.lean; it now reads
# terminator ("...to Phase 3") silently widens the moment a phase is # $PROOFS by MEMBERSHIP, because a glob demands artifacts this button never
# inserted between the two: adding Phase 2c made this driver swallow 2c as # makes (the spelling-versus-ownership error ScalarPackSpec exposed). This
# well and die on variables that phase expects check.sh to have defined, # preamble was not told, and bash does not error on an unset array under
# which surfaced as the BASELINE failing — a self-test blaming a gate for # `set -u` — it expands to nothing, so the gate got `expected := [".olean"]`
# its own extraction bug. # and rejected the baseline for a reason that had nothing to do with axioms.
awk '/^# ── Phase 2b/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 2b/{exit} f{print}' "$HERE/check.sh" # Lifted VERBATIM, never re-derived: a re-derivation lets this test's idea of
# the manifest drift away from the button's, and then the test checks its own
# opinion. lift-guard.sh below is what makes the omission impossible to
# repeat silently.
sed -n '/^PROOFS=(/,/^)/p' "$HERE/check.sh"
cat "$PAYLOAD"
} > "$DRIVER" } > "$DRIVER"
if [ "$(wc -l < "$DRIVER")" -lt 40 ]; then # Guard on the PAYLOAD, not the concatenation: a marker appearing in the
# preamble or in a lifted definition would otherwise satisfy these.
if [ "$(wc -l < "$PAYLOAD")" -lt 40 ]; then
echo "FATAL: could not lift Phase 2b out of check.sh — the phase markers moved." echo "FATAL: could not lift Phase 2b out of check.sh — the phase markers moved."
echo "This self-test must attack the shipping gate; refusing to run against nothing." echo "This self-test must attack the shipping gate; refusing to run against nothing."
exit 1 exit 1
fi fi
if [ "$(grep -c '^# ── Phase ' "$DRIVER")" -ne 1 ]; then if [ "$(grep -c '^# ── Phase ' "$PAYLOAD")" -ne 1 ]; then
echo "FATAL: the lifted block spans more than one phase; the extraction is wrong." echo "FATAL: the lifted block spans more than one phase; the extraction is wrong."
grep '^# ── Phase ' "$DRIVER" | sed 's/^/ /' grep '^# ── Phase ' "$PAYLOAD" | sed 's/^/ /'
exit 1 exit 1
fi fi
grep -qF 'PROOFS=(' "$DRIVER" || {
echo "FATAL: the lift carries no 'PROOFS=(' — the compile manifest is missing."; exit 1; }
"$HERE/lift-guard.sh" "$PAYLOAD" "$DRIVER" "check.sh Phase 2b" || exit 1
expect() { # expect <name> <expected-rc> <required-substring> expect() { # expect <name> <expected-rc> <required-substring>
local name="$1" want_rc="$2" want_txt="$3" local name="$1" want_rc="$2" want_txt="$3"
@ -85,31 +113,79 @@ expect "baseline green, coverage reported" 0 "none is an axiom"
# ── 2. The attack Phase 1's grep cannot see: an indented top-level axiom. # ── 2. The attack Phase 1's grep cannot see: an indented top-level axiom.
# Lean accepts it; the repo then proves False; the source-text gate is blind. # Lean accepts it; the repo then proves False; the source-text gate is blind.
cat > "$ATTACK" <<'EOF' #
# THE ATTACK GOES INTO A MANIFESTED MODULE, and that is the whole point of
# this case. Until 2026-08-02 it created a NEW file, Proofs/ZZSelftestAttack
# .lean, which worked while Phase 2b globbed Proofs/*.olean. Phase 2b now
# reads $PROOFS by MEMBERSHIP, so a stray module is simply not this gate's
# business — it is the dead-file gate's, and selftest-harness.sh case 8
# already proves check.sh dies with DEAD FILE on exactly that. Against
# membership, the stray-file attack passed the gate and the case went red.
# It is also the WEAKER attack: an adversary who can add files to Proofs/
# has to get past the dead-file gate, whereas an adversary who edits a
# module that is already manifested does not. So the case now poisons a
# real manifested module, which is what the kernel gate exists to catch.
MANIFEST=$(sed -n '/^PROOFS=(/,/^)/p' "$HERE/check.sh" \
| sed 's/#.*//; s/PROOFS=(//; s/)//' | tr -s ' \t' '\n' | sed '/^$/d')
# A LEAF: nothing else in the manifest imports it, so poisoning it cannot make
# a sibling's artifact stale. Smallest such module, to keep the recompile cheap.
#
# The SEARCH SET excludes Inventory* and Audit, and that exclusion is
# load-bearing: those are the aggregators, they import the whole corpus, and
# grepping them makes every module look imported. Leave them in and the loop
# finds no leaf at all — which is precisely how this case first reported
# "the corpus shape changed" against a corpus that had not changed.
SEARCHERS=$(for m in $MANIFEST; do
case $m in Inventory*|Audit) ;; *) echo "$HERE/Proofs/$m.lean";; esac
done)
_best=999999
for m in $MANIFEST; do
case $m in Inventory*|Audit) continue;; esac
[ -f "$HERE/Proofs/$m.lean" ] || continue
grep -qE "^import Proofs\.$m\$" $SEARCHERS 2>/dev/null && continue
n=$(wc -l < "$HERE/Proofs/$m.lean")
if [ "$n" -lt "$_best" ]; then _best=$n; VICTIM=$m; fi
done
if [ -z "$VICTIM" ]; then
echo " FAIL premise: no manifested leaf module to poison — the corpus shape changed."
FAILURES=$((FAILURES+1))
else
cp "$HERE/Proofs/$VICTIM.lean" "$STASH/victim.lean"
cp "$HERE/Proofs/$VICTIM.olean" "$STASH/victim.olean"
cat >> "$HERE/Proofs/$VICTIM.lean" <<'EOF'
namespace ZZSelftestAttack namespace ZZSelftestAttack
axiom cheat : ∀ (P : Prop), P axiom cheat : ∀ (P : Prop), P
theorem repo_proves_false : False := cheat _ theorem repo_proves_false : False := cheat _
end ZZSelftestAttack end ZZSelftestAttack
EOF EOF
if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lean >/dev/null 2>&1; then if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lean >/dev/null 2>&1; then
echo " FAIL premise: Phase 1's grep sees the attack — this test no longer tests what it claims" echo " FAIL premise: Phase 1's grep sees the attack — this test no longer tests what it claims"
FAILURES=$((FAILURES+1)) FAILURES=$((FAILURES+1))
else else
echo " ok premise: Phase 1's source-text grep is blind to this attack" echo " ok premise: Phase 1's source-text grep is blind to this attack"
fi
(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_MAX_CORES=$CORES '$HERE/lean-guard' 'Proofs/$VICTIM.lean'
") >/dev/null 2>&1 || { echo " FAIL setup: the poisoned module did not compile"; FAILURES=$((FAILURES+1)); }
expect "indented axiom in a manifested module caught kernel-side" 1 "AXIOM DECLARED under Proofs/"
cp "$STASH/victim.lean" "$HERE/Proofs/$VICTIM.lean"
cp "$STASH/victim.olean" "$HERE/Proofs/$VICTIM.olean"
fi fi
(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_MAX_CORES=$CORES '$HERE/lean-guard' 'Proofs/ZZSelftestAttack.lean'
") >/dev/null 2>&1 || { echo " FAIL setup: the attack module did not compile"; FAILURES=$((FAILURES+1)); }
expect "indented axiom caught kernel-side" 1 "AXIOM DECLARED under Proofs/"
rm -f "$ATTACK" "${ATTACK%.lean}.olean"
# ── 3. Vacuity: delete a compiled module. "Nothing found" must not pass for # ── 3. Vacuity: delete a compiled module. "Nothing found" must not pass for
# "nothing wrong" — the gate has to notice it stopped covering something. # "nothing wrong" — the gate has to notice it stopped covering something.
# The expected wording tracks the SHIPPING diagnostic: it read "COVERAGE
# MISMATCH" while the gate compared two counts, and became a per-module
# message when the gate started walking $PROOFS by membership. Asserting
# the reason and not merely the exit code is deliberate — a gate that goes
# red for an unrelated cause has not been tested.
mv "$HERE/Proofs/FeQ.olean" "$STASH/FeQ.olean" mv "$HERE/Proofs/FeQ.olean" "$STASH/FeQ.olean"
expect "missing .olean is a failure, not a vacuous pass" 1 "COVERAGE MISMATCH" expect "missing .olean is a failure, not a vacuous pass" 1 \
"is in the compile manifest but its artifact is absent"
mv "$STASH/FeQ.olean" "$HERE/Proofs/FeQ.olean" mv "$STASH/FeQ.olean" "$HERE/Proofs/FeQ.olean"
# ── 4. Litter: neither path may leave the temp gate source or its artifact # ── 4. Litter: neither path may leave the temp gate source or its artifact

174
verification/selftest-correspondence.sh Executable file
View file

@ -0,0 +1,174 @@
#!/usr/bin/env bash
# ─────────────────────────────────────────────────────────────────────────────
# selftest-correspondence.sh — attacks check.sh Phase 0d.
#
# Phase 0d asserts HOW each external the extraction asks for is answered: with
# an assumption in the hand-written model, or with a proof already in the
# extracted corpus. The second class is the one the documents make a claim
# about — the curve calls and curve types are said to resolve to the proven
# model's own definitions rather than to axioms — and that claim was prose
# until this phase existed.
#
# 0 control: the committed table matches the files
# 1 the extraction asks for something NOTHING provides -> UNRESOLVED
# 2 a PROVEN external answered by an axiom in the model instead. This is the
# attack that matters: a proof silently downgraded to an assumption, in a
# name whose spelling does not change anywhere else.
# 3 a row deleted from the committed table -> drift
# 4 a row's verdict edited in the committed table -> drift
#
# No Lean: Phase 0d is pure text over gen/. Seconds, not minutes.
# ─────────────────────────────────────────────────────────────────────────────
set -uo pipefail
HERE="$(cd "$(dirname "$0")" && pwd)"
FAILURES=0
STASH="$(mktemp -d)"
cleanup() {
[ -f "$STASH/corr" ] && cp "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt"
[ -f "$STASH/model" ] && cp "$STASH/model" "$HERE/$MODEL_REL"
[ -f "$STASH/tmpl" ] && cp "$STASH/tmpl" "$HERE/$TMPL_REL"
rm -rf "$STASH"
}
# Derive the victims from this repo rather than naming them: the forks do not
# share a gen/ layout (anza has no CurveSig crate at all, so it has no PROVEN
# rows and case 2 does not apply there).
TMPL_REL=$(cd "$HERE" && ls gen/*/FunsExternal_Template.lean | head -1)
MODEL_REL="${TMPL_REL/_Template/}"
PROVEN_ROW=$(grep -m1 '|PROVEN$' "$HERE/MODEL-CORRESPONDENCE.txt" || true)
trap cleanup EXIT INT TERM
cp "$HERE/MODEL-CORRESPONDENCE.txt" "$STASH/corr"
cp "$HERE/$MODEL_REL" "$STASH/model"
cp "$HERE/$TMPL_REL" "$STASH/tmpl"
# Phase 0d lifted from the shipping button.
awk '/^# ── Phase 0d/{f=1} f&&/^# ── (Phase 1|Phases end)/{exit} f{print}' \
"$HERE/check.sh" > "$STASH/payload.sh"
{ echo 'set -euo pipefail'
echo "HERE=\"$HERE\""
cat "$STASH/payload.sh"
} > "$STASH/p0d.sh"
# Assert on the PAYLOAD, not the concatenation: a marker appearing in the
# preamble would otherwise satisfy a check meant to prove the lift landed.
for want in 'Phase 0d' 'MODEL CORRESPONDENCE' 'model-correspondence.py'; do
grep -qF "$want" "$STASH/payload.sh" || {
echo "FATAL: the lifted driver has no '$want' — check.sh's phase markers moved."; exit 1; }
done
"$HERE/lift-guard.sh" "$STASH/payload.sh" "$STASH/p0d.sh" "check.sh Phase 0d" || exit 1
expect() { # expect <label> <want-rc> <want-substring>
local label="$1" want_rc="$2" want_txt="$3" out rc
out=$(bash "$STASH/p0d.sh" 2>&1); rc=$?
if [ "$rc" -ne "$want_rc" ]; then
echo " ✗ $label: exit $rc, expected $want_rc"; tail -6 <<<"$out" | sed 's/^/ /'
FAILURES=$((FAILURES+1)); return
fi
if ! grep -qF "$want_txt" <<<"$out"; then
echo " ✗ $label: exit code right, diagnostic wrong (rejected for the wrong reason)"
echo " wanted: $want_txt"; tail -6 <<<"$out" | sed 's/^/ /'
FAILURES=$((FAILURES+1)); return
fi
echo " ✓ $label"
}
echo "=== selftest-correspondence: attacking check.sh Phase 0d ==="
echo " template: $TMPL_REL"
expect "control: the committed table matches the files" 0 "answered by PROVEN definitions"
# ── 1. the extraction asks for something nothing provides ──────────────────
printf '\naxiom selftest_unprovided_external : Nat\n' >> "$HERE/$TMPL_REL"
expect "case 1: an external nothing provides" 1 "MODEL CORRESPONDENCE FAILED"
cp "$STASH/tmpl" "$HERE/$TMPL_REL"
# ── 2. a proof silently downgraded to an assumption ────────────────────────
# Answer a PROVEN external with an axiom in the model. The name does not change
# anywhere; only the way it is answered does. Nothing else in the button sees
# this: the byte pins still match their files, the compiler is content because
# the signature is unchanged, and no certificate's cone moves unless something
# happens to depend on it.
if [ -n "$PROVEN_ROW" ]; then
PROVEN_NAME=$(cut -d'|' -f2 <<<"$PROVEN_ROW")
PROVEN_TMPL=$(cut -d'|' -f1 <<<"$PROVEN_ROW")
VICTIM_MODEL="gen/${PROVEN_TMPL}.lean"
cp "$HERE/$VICTIM_MODEL" "$STASH/model2"
printf '\naxiom %s : Nat\n' "$PROVEN_NAME" >> "$HERE/$VICTIM_MODEL"
expect "case 2: a PROVEN external downgraded to an assumption" 1 "MODEL CORRESPONDENCE DRIFT"
cp "$STASH/model2" "$HERE/$VICTIM_MODEL"
else
echo " · case 2 skipped: this fork's extraction has no PROVEN externals"
fi
# ── 3/4. the committed table itself ────────────────────────────────────────
# Delete the FIRST row, whatever its verdict. An earlier draft deleted the
# PROVEN rows, which was vacuous on anza — that fork's extraction has none, so
# nothing was removed, the table still matched, and the case passed by testing
# nothing. Pick a row every fork is guaranteed to have.
sed '0,/|/{/|/d}' "$STASH/corr" > "$HERE/MODEL-CORRESPONDENCE.txt"
if ! diff -q "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt" >/dev/null; then
expect "case 3: a row deleted from the committed table" 1 "MODEL CORRESPONDENCE DRIFT"
else
echo " ✗ case 3: the table was not actually modified — the case is vacuous"
FAILURES=$((FAILURES+1))
fi
cp "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt"
sed -i '0,/|MODEL$/s/|MODEL$/|PROVEN/' "$HERE/MODEL-CORRESPONDENCE.txt"
expect "case 4: a verdict edited in the committed table" 1 "MODEL CORRESPONDENCE DRIFT"
cp "$STASH/corr" "$HERE/MODEL-CORRESPONDENCE.txt"
# ── 5/6. THE ROUND-7 FINDINGS, so they cannot regress ──────────────────────
# Both were real. Case 5 is GPT-5.6's constructive counterexample: a definition
# that exists ONLY inside a block comment was read as a real declaration, so the
# scanner reported PROVEN for a name Lean resolves to an axiom. Case 6 is the
# one that was live in four committed tables: Aeneas wraps long declarations,
# the old scanner required keyword and name on one physical line, and so it
# SILENTLY DROPPED them — nine to ten externals per fork had no row at all.
#
# Case 6 is the more important of the two. A gate that drops what it cannot
# read is worse than no gate: it prints green across a gap that is invisible in
# the diff. The scanner must now FAIL rather than skip.
CX=$(mktemp -d)
mkdir -p "$CX/gen/Forged"
printf 'axiom Forged.value : Nat\n' > "$CX/gen/Forged/FunsExternal_Template.lean"
printf 'axiom\n Forged.value : Nat\n' > "$CX/gen/Forged/FunsExternal.lean"
printf '/-\nnamespace Forged\ndef value : Nat := 0\nend Forged\n-/\n' > "$CX/gen/Forged/Funs.lean"
OUT=$(python3 "$HERE/model-correspondence.py" "$CX" 2>&1)
if grep -q 'Forged.value|MODEL' <<<"$OUT"; then
echo " ✓ case 5: a definition inside a block comment is not read as a declaration"
else
echo " ✗ case 5: comment-only definition mis-read — scanner says:"; sed 's/^/ /' <<<"$OUT"
FAILURES=$((FAILURES+1))
fi
printf 'axiom\n Forged.wrapped\n :\n Nat\n' >> "$CX/gen/Forged/FunsExternal_Template.lean"
OUT=$(python3 "$HERE/model-correspondence.py" "$CX" 2>&1); RC=$?
if [ "$RC" -ne 0 ] && grep -q 'UNRESOLVED\|Forged.wrapped' <<<"$OUT"; then
echo " ✓ case 6: a declaration whose name wraps to the next line is SEEN, not dropped"
else
echo " ✗ case 6: wrapped declaration dropped or mis-handled (rc=$RC):"; sed 's/^/ /' <<<"$OUT"
FAILURES=$((FAILURES+1))
fi
printf 'axiom\n' > "$CX/gen/Forged/FunsExternal_Template.lean"
OUT=$(python3 "$HERE/model-correspondence.py" "$CX" 2>&1); RC=$?
if [ "$RC" -eq 2 ] && grep -q 'fails closed' <<<"$OUT"; then
echo " ✓ case 7: an unparseable declaration stops the scanner (exit 2), never silence"
else
echo " ✗ case 7: unparseable declaration did not fail closed (rc=$RC)"
FAILURES=$((FAILURES+1))
fi
rm -rf "$CX"
expect "restored: the table matches again" 0 "answered by PROVEN definitions"
echo ""
if [ "$FAILURES" -eq 0 ]; then
echo "SELFTEST PASSED — an external cannot change how it is answered, and a"
echo "proof cannot be downgraded to an assumption, without failing the button."
exit 0
fi
echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
exit 1

11
verification/selftest-harness.sh
View file

@ -39,17 +39,20 @@ cp "$HERE/HARNESS.sha256" "$STASH/HARNESS.sha256"
# Lift Phase 0c. The two repo families end the phase differently, so accept # Lift Phase 0c. The two repo families end the phase differently, so accept
# either terminator rather than hardcoding one and silently lifting nothing. # either terminator rather than hardcoding one and silently lifting nothing.
DRIVER="$STASH/phase0c.sh" DRIVER="$STASH/phase0c.sh"
PAYLOAD="$STASH/payload.sh"
awk '/^# ── Phase 0c/{f=1} f{print} /^# ── Phase 1|^echo "=== Phase 1/{if(f && !/Phase 0c/) exit}' "$HERE/check.sh" \
| sed '/^# ── Phase 1/d; /^echo "=== Phase 1/d' > "$PAYLOAD"
{ {
echo 'set -uo pipefail' echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit
echo "HERE=\"$HERE\"" echo "HERE=\"$HERE\""
awk '/^# ── Phase 0c/{f=1} f{print} /^# ── Phase 1|^echo "=== Phase 1/{if(f && !/Phase 0c/) exit}' "$HERE/check.sh" \ cat "$PAYLOAD"
| sed '/^# ── Phase 1/d; /^echo "=== Phase 1/d'
} > "$DRIVER" } > "$DRIVER"
if [ "$(grep -c . "$DRIVER")" -lt 20 ]; then if [ "$(grep -c . "$PAYLOAD")" -lt 20 ]; then
echo "FATAL: could not lift Phase 0c out of check.sh — the phase markers moved." echo "FATAL: could not lift Phase 0c out of check.sh — the phase markers moved."
echo "This self-test must attack the shipping gate; refusing to run against nothing." echo "This self-test must attack the shipping gate; refusing to run against nothing."
exit 1 exit 1
fi fi
"$HERE/lift-guard.sh" "$PAYLOAD" "$DRIVER" "check.sh Phase 0c" || exit 1
expect() { # expect <label> <want-rc> <want-substring> expect() { # expect <label> <want-rc> <want-substring>
local label="$1" want_rc="$2" want_txt="$3" out rc local label="$1" want_rc="$2" want_txt="$3" out rc

197
verification/selftest-scalar-statements.sh Executable file
View file

@ -0,0 +1,197 @@
#!/usr/bin/env bash
# ─────────────────────────────────────────────────────────────────────────────
# selftest-scalar-statements.sh — adversarial self-test for check-scalar.sh
# Phase 3c, the scalar statement + specification binding.
#
# WHY THIS EXISTS. Round-7 review (GPT-5.6, register key
# `scalar-statements-unbound`, CRITICAL): the main button bound its 31
# certificates' elaborated statements and reachable specification bodies; this
# repository's scalar button bound NONE of its thirteen, while TRUSTED-BASE
# item 8 said the audit covers "every certificate". The binding was added in
# the same commit as this file. The reviewer asked for exactly two shipping
# attacks, and this file is those two:
#
# 1. same-cone theorem statement gutting;
# 2. a reachable reference body rewritten while name and cone remain fixed.
#
# Both are invisible to every earlier phase by construction. Phase 2b sees no
# new axiom; Phase 3's exact-cone audit sees the same three axioms; only the
# statement binding sees them.
#
# It extracts Phase 3c out of check-scalar.sh at run time, so it attacks THE
# SHIPPING GATE rather than a copy that can drift away from it.
#
# Requires a prior green scalar build. Recompiling the corpus is the expensive
# part; SKIP_SLOW=1 runs only the fast cases and SAYS SO rather than passing
# quietly over the two that matter.
# ─────────────────────────────────────────────────────────────────────────────
set -uo pipefail
source ~/aeneas-toolchain/env.sh
HERE="$(cd "$(dirname "$0")" && pwd)"
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
TIMEOUT="${LEAN_TIMEOUT:-900}"
export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}"
CORES="${LEAN_MAX_CORES:-0-3}"
SKIP_SLOW="${SKIP_SLOW:-0}"
STASH="$(mktemp -d)"
FAILURES=0
TREE_AT_START="$(cd "$HERE/.." && git status --porcelain)"
cleanup() {
[ -f "$STASH/gut.lean" ] && cp "$STASH/gut.lean" "$HERE/Proofs/ScalarMain.lean"
[ -f "$STASH/den.lean" ] && cp "$STASH/den.lean" "$HERE/Proofs/ScalarDenote.lean"
rm -rf "$STASH"
rm -f "$HERE"/.scalar-audit-manifest.observed
}
trap cleanup EXIT INT TERM
DRIVER="$STASH/phase3c.sh"
PAYLOAD="$STASH/payload.sh"
build_driver() {
awk '/^# ── Phase 3c/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 3c/{exit} f{print}' \
"$HERE/check-scalar.sh" > "$PAYLOAD"
{ echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit
echo 'source ~/aeneas-toolchain/env.sh'
echo "HERE=\"$HERE\""
echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\""
# CERTS is referenced by the cross-check inside Phase 3c. Lifted VERBATIM
# rather than re-derived, so this test cannot drift from the button's set.
sed -n '/^CERTS=(/,/^)/p' "$HERE/check-scalar.sh"
cat "$PAYLOAD"
} > "$DRIVER"
if [ "$(wc -l < "$PAYLOAD")" -lt 40 ]; then
echo "FATAL: could not lift Phase 3c out of check-scalar.sh — the markers moved."
exit 1
fi
grep -qF 'SCALAR-AUDIT-MANIFEST-BEGIN' "$PAYLOAD" || {
echo "FATAL: the lifted payload does not read the scalar audit block."; exit 1; }
"$HERE/lift-guard.sh" "$PAYLOAD" "$DRIVER" "check-scalar.sh Phase 3c" || exit 1
}
recompile() { # recompile <module>
( cd "$AENEAS_LEAN" && lake env bash -c "
set -uo pipefail
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
cd '$HERE'
LEAN_TIMEOUT=$TIMEOUT LEAN_MAX_CORES=$CORES '$HERE/lean-guard' Proofs/$1.lean
" ) >/dev/null 2>&1
}
expect() { # expect <name> <expected-rc> <required-substring>
local name="$1" want_rc="$2" want_txt="$3" out rc
out=$(bash "$DRIVER" 2>&1); rc=$?
if [ "$rc" -ne "$want_rc" ]; then
echo " FAIL $name: exit $rc, expected $want_rc"
tail -6 <<<"$out" | sed 's/^/ /'; FAILURES=$((FAILURES+1)); return
fi
if ! grep -qF "$want_txt" <<<"$out"; then
echo " FAIL $name: exit code right but diagnostic wrong (rejected for the wrong reason)"
echo " wanted substring: $want_txt"
echo " got: $(tr '\n' '|' <<<"$out" | cut -c1-260)"
FAILURES=$((FAILURES+1)); return
fi
echo " ok $name"
}
echo "=== selftest-scalar-statements: attacking check-scalar.sh Phase 3c ==="
build_driver
# ── 1. Baseline: the untouched repository passes and reports what it bound.
expect "baseline green, statements bound" 0 "statements + reachable specification bodies bound"
# ── 2. HAND-EDIT THE COMMITTED BLOCK. The digest still matches what Lean
# emits, so only the committed-copy comparison can see this.
cp "$HERE/SCALAR-AUDIT-MANIFEST.txt" "$STASH/manifest.bak"
sed -i '2s/$/ TAMPERED/' "$HERE/SCALAR-AUDIT-MANIFEST.txt"
expect "hand-edited committed block caught" 1 "does not match the emitted block"
cp "$STASH/manifest.bak" "$HERE/SCALAR-AUDIT-MANIFEST.txt"
if [ "$SKIP_SLOW" = "1" ]; then
echo " SKIPPED (SKIP_SLOW=1): the two attacks this file exists for — gutted"
echo " statement and rewritten specification body — were NOT run. The fast"
echo " case above does not cover either of them."
else
# ── 3. ATTACK ONE: gut a certificate's STATEMENT, preserving its axiom cone.
# ScalarProofs.scalarImplementation is the aggregate and is TERMINAL —
# nothing outside its own module consumes it. Gutting a load-bearing
# certificate would simply break its consumers, which demonstrates the
# compiler working, not this gate.
cp "$HERE/Proofs/ScalarMain.lean" "$STASH/gut.lean"
python3 - "$HERE/Proofs/ScalarMain.lean" <<'PY'
import sys, re
f = sys.argv[1]
s = open(f).read()
m = re.search(r'^theorem scalarImplementation\b', s, re.M)
assert m, "scalarImplementation not found"
i = m.start()
nxt = re.search(r'^(theorem|lemma|def|noncomputable def|end|/--|@\[)', s[i+10:], re.M)
assert nxt, "no following declaration"
j = i + 10 + nxt.start()
# Same cone (Classical.em pulls in Classical.choice/propext), utterly different
# claim. Every earlier phase is satisfied; only the statement binding is not.
gut = "theorem scalarImplementation : (∀ p : Prop, p ∨ ¬p) := Classical.em\n\n"
open(f, "w").write(s[:i] + gut + s[j:])
PY
recompile ScalarMain || { echo " FAIL setup: the gutted module did not compile"; FAILURES=$((FAILURES+1)); }
recompile ScalarAudit
expect "gutted statement caught (cone unchanged)" 1 "audit-manifest digest mismatch"
cp "$STASH/gut.lean" "$HERE/Proofs/ScalarMain.lean"; rm -f "$STASH/gut.lean"
recompile ScalarMain; recompile ScalarAudit
# ── 4. ATTACK TWO: rewrite a REACHABLE SPECIFICATION BODY while the
# certificate's name and cone stay fixed. This is the attack the whole
# block exists for: if a reference definition can be edited without
# notice, a certificate can be made to say `loop = loop` and every cone
# stays byte-identical.
#
# scDenote is reachable from the scalar statements and its body is
# rewritten here to `id (…)`, which is DEFINITIONALLY EQUAL — so the
# corpus still compiles and every proof still typechecks. That is the
# point: the binding must be sensitive to the body AS WRITTEN, not
# merely to what it evaluates to. If the setup fails to compile this
# case reports FAIL rather than passing quietly.
cp "$HERE/Proofs/ScalarDenote.lean" "$STASH/den.lean"
python3 - "$HERE/Proofs/ScalarDenote.lean" <<'PY'
import sys
f = sys.argv[1]
s = open(f).read()
old = "def scDenote (a : Sc) : ZMod Ell := (scVal a : ZMod Ell)"
assert old in s, "scDenote body not in the expected form"
new = "def scDenote (a : Sc) : ZMod Ell := id (scVal a : ZMod Ell)"
open(f, "w").write(s.replace(old, new, 1))
PY
if recompile ScalarDenote; then
recompile ScalarAudit
expect "rewritten specification body caught (name and cone unchanged)" 1 \
"audit-manifest digest mismatch"
else
echo " FAIL setup: the rewritten specification body did not compile —"
echo " this attack did NOT exercise the gate. Do not read the"
echo " surrounding passes as covering it."
FAILURES=$((FAILURES+1))
fi
cp "$STASH/den.lean" "$HERE/Proofs/ScalarDenote.lean"; rm -f "$STASH/den.lean"
recompile ScalarDenote; recompile ScalarAudit
fi
# ── 5. Restored: green again, and the working tree is as we found it.
expect "restored to green" 0 "statements + reachable specification bodies bound"
TREE_NOW="$(cd "$HERE/.." && git status --porcelain)"
if [ "$TREE_AT_START" != "$TREE_NOW" ]; then
echo " FAIL restore: the working tree differs from how this test found it:"
diff <(printf '%s\n' "$TREE_AT_START") <(printf '%s\n' "$TREE_NOW") | sed 's/^/ /'
FAILURES=$((FAILURES+1))
else
echo " ok working tree restored to its starting state"
fi
echo ""
if [ "$FAILURES" -eq 0 ]; then
echo "SELFTEST PASSED — scalar Phase 3c rejects statement- and specification-"
echo "level tampering that moves no axiom cone, for the stated reason."
exit 0
fi
echo "SELFTEST FAILED: $FAILURES check(s) did not behave as claimed."
exit 1

254
verification/selftest-shapes.sh Executable file
View file

@ -0,0 +1,254 @@
#!/usr/bin/env bash
# ─────────────────────────────────────────────────────────────────────────────
# selftest-shapes.sh — can a declaration HIDE from the inventory walker?
#
# check.sh Phase 2c exists because a source-regex enumerator turned out to be
# evadable: in ltl-accumulator-verified a nine-attack self-test defeated one
# with attributed, private, indented and `instance` declarations and with a
# nested-namespace basename collision. The fix was to stop reading source text
# and ask the Lean environment instead, and that fix was PORTED here — see the
# note at the head of Phase 2c.
#
# But a fix ported is not a fix tested. `selftest-inventory.sh` proves the GATE
# reacts correctly to a difference; it feeds the gate synthetic observations and
# never runs the walker. Nothing in these four forks has ever asked the question
# the accumulator's suite asks: does the WALKER SEE a declaration written in an
# evasive shape? If it silently skipped one, the observation would match the
# allowlist, the gate would be satisfied, and a hidden theorem would ride along
# inside an audited module with every button green.
#
# 0 control: the untouched tree's observation equals the allowlist
# 1 FOUR EVASIVE SHAPES added to an audited module at once:
# @[simp] theorem an attribute in front of the declaration
# private theorem not exported, name mangled by the elaborator
# instance a declaration with no `theorem`/`def` keyword
# nested namespace Ns.Hidden.X, reusing the basename of an audited
# declaration Ns.X — the spelling-vs-membership shape.
# The victim module, its namespace and X are all
# derived from this repo's own manifest below.
# EVERY ONE must be named in the gate's UNCLASSIFIED list. Asserting the
# gate merely failed is not enough: one shape surfacing would fail the run
# while the other three rode along unseen.
#
# One recompile of one leaf module, then the real Phase 2c. Run after a green
# check.sh.
# ─────────────────────────────────────────────────────────────────────────────
set -uo pipefail
source ~/aeneas-toolchain/env.sh
HERE="$(cd "$(dirname "$0")" && pwd)"
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
TIMEOUT="${LEAN_TIMEOUT:-900}"
export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}"
FAILURES=0
SAFE_EXIT=0
STASH="$(mktemp -d)"
# Pick the victim from this repo's own manifest rather than naming a module:
# the four forks do not share a corpus (dalek and anza carry Proofs.Basic;
# risc0 and betrusted do not), and a hard-coded name would silently pick
# nothing on half of them.
#
# The victim must be (a) in check.sh's PROOFS — attacking an unmanifested module
# would test the dead-file gate instead of the walker; (b) NOT an inventory
# driver or the audit driver — those are the instruments, and mutating one would
# be attacking the measuring device; (c) imported by no other manifest module,
# so one recompile cannot invalidate a second module's artifact. Of those, take
# the smallest, because this test compiles it twice.
#
# Note for anyone re-deriving this: the inventory drivers import the whole
# corpus, so they must be excluded from the set of importers as well as from the
# candidates. Leave them in and every module looks imported, no leaf is found,
# and the test silently has no victim at all.
MAIN=$(sed -n '/^PROOFS=(/,/^)/p' "$HERE/check.sh" \
| sed 's/#.*//; s/PROOFS=(//; s/)//' | tr -s ' \t' '\n' | sed '/^$/d')
SEARCHERS=$(for m in $MAIN; do case $m in Inventory*|Audit) ;; *) echo "$HERE/Proofs/$m.lean";; esac; done)
VICTIM_MOD=""; _best=999999
for m in $MAIN; do
case $m in Inventory*|Audit) continue;; esac
grep -q "^import Proofs\.$m\$" $SEARCHERS 2>/dev/null && continue
n=$(wc -l < "$HERE/Proofs/$m.lean")
if [ "$n" -lt "$_best" ]; then _best=$n; VICTIM_MOD=$m; fi
done
if [ -z "$VICTIM_MOD" ]; then
echo "FATAL: no manifested leaf module to attack — the corpus shape changed."; exit 1
fi
VICTIM_NS=$(grep -m1 '^namespace ' "$HERE/Proofs/$VICTIM_MOD.lean" | awk '{print $2}')
COLLIDE=$(grep -m1 '^theorem ' "$HERE/Proofs/$VICTIM_MOD.lean" | awk '{print $2}')
if [ -z "$VICTIM_NS" ] || [ -z "$COLLIDE" ]; then
echo "FATAL: $VICTIM_MOD has no namespace or no theorem to collide with."; exit 1
fi
cleanup() {
[ -f "$STASH/victim" ] && cp "$STASH/victim" "$HERE/Proofs/$VICTIM_MOD.lean"
[ "$SAFE_EXIT" -eq 1 ] || rm -f "$HERE/Proofs/$VICTIM_MOD.olean" "$HERE/Proofs/$VICTIM_MOD.ilean"
rm -rf "$STASH"
}
trap cleanup EXIT INT TERM
cp "$HERE/Proofs/$VICTIM_MOD.lean" "$STASH/victim"
# Phase 2c lifted from the shipping button. `set -euo pipefail` is copied from
# check.sh:32 deliberately — the phase does its Lean work in subshells, and
# without -e a failing subshell is masked by the next echo. (That exact mistake
# produced a green report for a red condition while selftest-tiers.sh was being
# built; do not "simplify" it away.)
lift() {
# THE LIFT RANGE STOPS AT THE ACCOUNTING IDENTITY, and that boundary is the
# fix for round-7 finding F5 (Claude). Phase 2c grew an accounting block that
# reads $KERNLOG — a file created in Phase 2b, one phase ABOVE the lift. Under
# `set -u` the driver aborted on its first expansion, so this self-test could
# not pass on any fork from the moment that block was added. It failed loudly
# rather than passing vacuously, which is why it was a red test and not a
# false green; but it meant the four-shapes property went unverified.
#
# This test attacks the WALKER — can a declaration hide from the inventory —
# and the accounting identity is a separate property with its own coverage.
# Lifting it here would only drag in Phase 2b's state.
awk '/^# ── Phase 2c/{f=1} f&&/^# ── (Phase 2c-accounting|Phase 3|Phases end)/{exit} f{print}' \
"$HERE/check.sh" > "$STASH/payload.sh"
{ echo 'set -euo pipefail'
echo 'source ~/aeneas-toolchain/env.sh'
echo "HERE=\"$HERE\""
echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
echo "TIMEOUT=$TIMEOUT"
# PROOFS, and the scalar manifest the coverage check consults. Both are
# lifted VERBATIM rather than re-derived here: re-deriving would let this
# test's idea of the manifest drift away from the button's, and then the
# test would be checking its own opinion instead of the shipping one.
sed -n '/^PROOFS=(/,/^)/p;/^SCALAR_SH=/p;/^SCALAR_MANIFEST=/p' "$HERE/check.sh"
cat "$STASH/payload.sh"
} > "$STASH/p2c.sh"
# Guard on the PAYLOAD, not the concatenation. The previous version grepped
# the assembled file, so a marker appearing in the preamble or in a lifted
# definition would have satisfied it — the same shape as the line-count check
# that an empty driver once passed because the CERTS array padded it.
for want in 'Phase 2c' 'inventory_gate.sh'; do
grep -qF "$want" "$STASH/payload.sh" || {
echo "FATAL: the lifted PAYLOAD has no '$want' — check.sh's phase markers moved."; exit 1; }
done
for want in 'PROOFS=(' 'SCALAR_MANIFEST='; do
grep -qF "$want" "$STASH/p2c.sh" || {
echo "FATAL: the lift carries no '$want' — a definition the phase needs is missing."; exit 1; }
done
# AND THE DURABLE GUARD: every variable the payload READS must be one the
# driver DEFINES. Derived mechanically rather than from a hand-kept list,
# because a hand-kept list is exactly what failed — the phase grew a
# dependency nobody thought to add. Shared with the other four lifting
# self-tests: ONE implementation, pinned, rather than five copies of the
# thing whose whole failure mode is drifting out of sync.
"$HERE/lift-guard.sh" "$STASH/payload.sh" "$STASH/p2c.sh" "check.sh Phase 2c" || exit 1
}
lift
recompile() {
( cd "$AENEAS_LEAN" && lake env bash -c "
set -uo pipefail
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
cd '$HERE'
LEAN_TIMEOUT=$TIMEOUT '$HERE/lean-guard' Proofs/$VICTIM_MOD.lean
" ) >/dev/null 2>&1
}
run_phase() { bash "$STASH/p2c.sh" 2>&1; }
echo "=== selftest-shapes: can a declaration hide from the walker? ==="
echo " victim: Proofs/$VICTIM_MOD.lean ($_best lines), namespace $VICTIM_NS"
echo " colliding basename: $VICTIM_NS.$COLLIDE"
if ! recompile; then
echo "FATAL: Proofs/$VICTIM_MOD.lean does not compile before any attack — fix the tree first."
exit 1
fi
# ── 0. control ─────────────────────────────────────────────────────────────
OUT=$(run_phase); RC=$?
if [ "$RC" -eq 0 ] && grep -qF "environment == allowlist" <<<"$OUT"; then
echo " ✓ control: the untouched tree's observation equals the allowlist"
else
echo " ✗ control: exit $RC — the tree is not green before the attack"
tail -8 <<<"$OUT" | sed 's/^/ /'
FAILURES=$((FAILURES+1))
fi
# ── 1. the four shapes ─────────────────────────────────────────────────────
python3 - "$HERE/Proofs/$VICTIM_MOD.lean" "$VICTIM_NS" "$COLLIDE" <<'PY'
import sys
f, ns, collide = sys.argv[1], sys.argv[2], sys.argv[3]
s = open(f).read()
end = f"\nend {ns}"
assert s.rstrip().endswith(end.strip()), "victim does not end by closing its namespace"
i = s.rstrip().rfind(end)
inject = f"""
-- selftest-shapes: four declaration shapes that defeated a source-regex
-- enumerator in ltl-accumulator-verified. Each must surface in the walker's
-- observation. Removed by this script's cleanup.
@[simp] theorem shape_attributed : True := trivial
private theorem shape_private : True := trivial
instance shape_instance : Nonempty Nat := ⟨0⟩
namespace Hidden
theorem {collide} : True := trivial
end Hidden
"""
open(f, "w").write(s[:i] + inject + s[i:])
PY
if ! recompile; then
echo " ✗ case 1: the module with the four shapes did not compile (case is vacuous)"
FAILURES=$((FAILURES+1))
else
OUT=$(run_phase); RC=$?
if [ "$RC" -eq 0 ]; then
echo " ✗ case 1: FOUR hidden declarations and the inventory passed — the walker is blind"
FAILURES=$((FAILURES+1))
else
# Not "did it fail" but "did it see each one". A gate that reports three of
# four still lets one declaration ride along inside an audited module.
MISSED=0
for n in "$VICTIM_NS.shape_attributed" "shape_private" \
"$VICTIM_NS.shape_instance" "$VICTIM_NS.Hidden.$COLLIDE"; do
if grep -qF "UNCLASSIFIED" <<<"$OUT" && grep -F "UNCLASSIFIED" <<<"$OUT" | grep -qF "$n"; then
echo " · seen: $n"
else
echo " · NOT SEEN: $n — this shape hides from the walker"
MISSED=1
fi
done
if [ "$MISSED" -eq 0 ]; then
echo " ✓ case 1: all four evasive shapes surfaced as UNCLASSIFIED"
else
echo " ✗ case 1: the gate failed, but not for every shape"
grep -F "UNCLASSIFIED" <<<"$OUT" | head -8 | sed 's/^/ /'
FAILURES=$((FAILURES+1))
fi
fi
fi
cp "$STASH/victim" "$HERE/Proofs/$VICTIM_MOD.lean"
if recompile; then
SAFE_EXIT=1
else
echo " ✗ restore: the ORIGINAL module no longer compiles — tree left for inspection"
FAILURES=$((FAILURES+1))
fi
OUT=$(run_phase); RC=$?
if [ "$RC" -eq 0 ] && grep -qF "environment == allowlist" <<<"$OUT"; then
echo " ✓ restored: the observation equals the allowlist again"
else
echo " ✗ restored: the tree did not come back green (exit $RC)"
FAILURES=$((FAILURES+1))
fi
echo ""
if [ "$FAILURES" -eq 0 ]; then
echo "SELFTEST PASSED — no declaration shape tested here can hide inside an"
echo "audited module: the walker reports each one by name."
exit 0
fi
echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
exit 1

31
verification/selftest-statements.sh
View file

@ -47,37 +47,44 @@ cp "$HERE/AUDIT-MANIFEST.txt" "$STASH/AUDIT-MANIFEST.txt"
cp "$HERE/check.sh" "$STASH/check.sh" cp "$HERE/check.sh" "$STASH/check.sh"
DRIVER0B="$STASH/phase0b.sh" DRIVER0B="$STASH/phase0b.sh"
PAYLOAD0B="$STASH/payload0b.sh"
sed -n '/^# ── Phase 0b/,/^# ── Phase 1/p' "$HERE/check.sh" | sed '$d' > "$PAYLOAD0B"
{ {
echo 'set -uo pipefail' echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit
echo "HERE=\"$HERE\"" echo "HERE=\"$HERE\""
sed -n '/^# ── Phase 0b/,/^# ── Phase 1/p' "$HERE/check.sh" | sed '$d' cat "$PAYLOAD0B"
} > "$DRIVER0B" } > "$DRIVER0B"
if [ "$(wc -l < "$DRIVER0B")" -lt 20 ]; then if [ "$(wc -l < "$PAYLOAD0B")" -lt 20 ]; then
echo "FATAL: could not lift Phase 0b out of check.sh."; exit 1 echo "FATAL: could not lift Phase 0b out of check.sh."; exit 1
fi fi
"$HERE/lift-guard.sh" "$PAYLOAD0B" "$DRIVER0B" "check.sh Phase 0b" || exit 1
DRIVER="$STASH/phase3c.sh" DRIVER="$STASH/phase3c.sh"
PAYLOAD="$STASH/payload3c.sh"
build_driver() { build_driver() {
# `$0` inside Phase 3c must resolve to the shipping check.sh, not to this
# driver, or the apex-name recovery would read the wrong file.
# Stop at the next phase marker, not at a blank echo: a terminator that is
# not itself a phase boundary breaks the moment the phase's body changes.
awk '/^# ── Phase 3c/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 3c/{exit} f{print}' "$HERE/check.sh" \
| sed "s|\"\$0\"|\"$HERE/check.sh\"|g" > "$PAYLOAD"
{ {
echo 'set -uo pipefail' echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit
echo 'source ~/aeneas-toolchain/env.sh' echo 'source ~/aeneas-toolchain/env.sh'
echo "HERE=\"$HERE\"" echo "HERE=\"$HERE\""
echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"' echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\"" echo "TIMEOUT=$TIMEOUT; CORES=\"$CORES\""
# CERTS is referenced by the cross-check inside Phase 3c. # CERTS is referenced by the cross-check inside Phase 3c. Lifted verbatim,
# never re-derived, so this test cannot drift away from the button's set.
sed -n '/^CERTS=(/,/^)/p' "$HERE/check.sh" sed -n '/^CERTS=(/,/^)/p' "$HERE/check.sh"
# `$0` inside Phase 3c must resolve to the shipping check.sh, not to this cat "$PAYLOAD"
# driver, or the apex-name recovery would read the wrong file.
# Stop at the next phase marker, not at a blank echo: a terminator that is
# not itself a phase boundary breaks the moment the phase's body changes.
awk '/^# ── Phase 3c/{f=1} f&&/^# ── (Phase |Phases end)/&&!/Phase 3c/{exit} f{print}' "$HERE/check.sh" \
| sed "s|\"\$0\"|\"$HERE/check.sh\"|g"
} > "$DRIVER" } > "$DRIVER"
if [ "$(wc -l < "$DRIVER")" -lt 60 ]; then if [ "$(wc -l < "$PAYLOAD")" -lt 60 ]; then
echo "FATAL: could not lift Phase 3c out of check.sh — the phase markers moved." echo "FATAL: could not lift Phase 3c out of check.sh — the phase markers moved."
echo "This self-test must attack the shipping gate; refusing to run against nothing." echo "This self-test must attack the shipping gate; refusing to run against nothing."
exit 1 exit 1
fi fi
"$HERE/lift-guard.sh" "$PAYLOAD" "$DRIVER" "check.sh Phase 3c" || exit 1
} }
build_driver build_driver

248
verification/selftest-tiers.sh Executable file
View file

@ -0,0 +1,248 @@
#!/usr/bin/env bash
# ─────────────────────────────────────────────────────────────────────────────
# selftest-tiers.sh — adversarial self-test for the TWO-TIER axiom boundary.
#
# This repository has two tiers and the distinction is the most valuable
# property it has:
#
# · the ARITHMETIC tier — field, curve, scalar and encoding certificates —
# must rest on Lean's three kernel axioms and NOTHING else. No hash oracle,
# no wire-format opacity. That is what makes "the curve arithmetic is
# proven" a claim about mathematics rather than about assumptions;
# · the APEX tier — the four signature certificates — legitimately carries
# this fork's SHA-512 and wire-format axioms, because a signature scheme
# cannot be verified without a hash.
#
# Collapsing the two, by widening the arithmetic tier to accept oracles, would
# destroy that property while every button stayed green — and it is exactly
# what a single careless edit to a shared lemma does. Until 2026-07-30 nothing
# tested it. These cases do.
#
# 0 control: untouched tree passes
# 1 AN APEX ORACLE LEAKED INTO AN ARITHMETIC CERTIFICATE. A hash axiom is
# introduced into the proof of an arithmetic certificate — statement
# unchanged, so only the cone moves. Phase 3 must name that certificate.
# 2 the apex boundary WIDENED by one name -> apex cones no longer match
# 3 the apex boundary NARROWED by one name -> same, from the other side
#
# Case 1 recompiles one module and is the slow one (~2 min). Cases 2 and 3 need
# no Lean at all. Run after a green check.sh.
# ─────────────────────────────────────────────────────────────────────────────
set -uo pipefail
source ~/aeneas-toolchain/env.sh
HERE="$(cd "$(dirname "$0")" && pwd)"
AENEAS_LEAN="$AENEAS_HOME/backends/lean"
TIMEOUT="${LEAN_TIMEOUT:-900}"
export LEAN_MEM_MB="${LEAN_MEM_MB:-8192}"
FAILURES=0
SAFE_EXIT=0
STASH="$(mktemp -d)"
# The audit phases write a temporary driver (.audit-XXXX.lean / .apex-XXXX.lean)
# and delete it on the way out — but a phase that exits 1 never reaches its own
# rm. This test provokes four such exits on purpose, so it is this test's job to
# clear the residue. Record what was here first and remove only what we caused;
# litter that predates the run is somebody else's finding, not ours to hide.
shopt -s nullglob
LITTER_BEFORE="$(printf '%s\n' "$HERE"/.audit-*.lean "$HERE"/.apex-*.lean | sort)"
shopt -u nullglob
VICTIM_MOD=PointEqSpec
VICTIM_CERT=CurveFieldProofs.enc_point_inj
# Which apex axiom to smuggle downward is a per-fork question, so derive it
# rather than hard-code it: take this repo's own documented apex boundary, drop
# the three kernel axioms, and keep the names that are actually declared inside
# the victim module's import closure — an axiom the victim cannot see cannot be
# injected into it. Prefer a hash oracle when one is reachable (dalek reaches
# verifying.sha512_new); the three forks that route SHA-512 through a single
# apex-only module reach only the wire-format axioms, which serve equally well:
# the property under test is that NO apex axiom may appear in this tier.
import_closure() { # every .lean file the victim module transitively imports
local -A seen=(); local -a q=("$VICTIM_MOD"); local m f i
while [ ${#q[@]} -gt 0 ]; do
m="${q[0]}"; q=("${q[@]:1}")
[ -n "${seen[$m]:-}" ] && continue
seen[$m]=1
for f in "$HERE/Proofs/$m.lean" "$HERE/gen/${m//.//}.lean"; do
[ -f "$f" ] || continue
echo "$f"
while read -r i; do q+=("$i"); done \
< <(grep '^import ' "$f" | awk '{print $2}' | sed 's/^Proofs\.//')
done
done
}
oracle_for_this_fork() {
local allowed closure m
allowed=$(grep -h "ALLOWED='" "$HERE/check.sh" | sed "s/.*ALLOWED='\[//;s/\].*//" \
| tr ',' '\n' | sed 's/^ *//;s/ *$//' \
| grep -v '^propext$\|^Classical.choice$\|^Quot.sound$')
closure=$(import_closure)
for m in $(echo "$allowed" | grep 'sha512\|sha2') $allowed; do
if grep -qE "^axiom ${m//./\\.}( |:)" $closure 2>/dev/null; then echo "$m"; return; fi
done
}
ORACLE="$(oracle_for_this_fork)"
if [ -z "$ORACLE" ]; then
echo "FATAL: this fork's apex boundary lists no axiom this test can inject."; exit 1
fi
cleanup() {
[ -f "$STASH/victim" ] && cp "$STASH/victim" "$HERE/Proofs/$VICTIM_MOD.lean"
[ -f "$STASH/check" ] && cp "$STASH/check" "$HERE/check.sh"
[ -f "$STASH/pins" ] && cp "$STASH/pins" "$HERE/HARNESS.sha256"
# If we are dying mid-case the victim's .olean may still hold the injected
# oracle while its source no longer shows it. That artifact is worse than no
# artifact: it is a poisoned object with a clean source. Remove it. Phase 3's
# vacuous-scan guard then fails loudly, and any full run rebuilds it anyway.
# On the normal path the run has already restored and rebuilt the module, so
# deleting it there would leave the tree worse than we found it — an
# --audit-only run afterwards would fail on a missing artifact we removed.
[ "$SAFE_EXIT" -eq 1 ] || rm -f "$HERE/Proofs/$VICTIM_MOD.olean" "$HERE/Proofs/$VICTIM_MOD.ilean"
local f
shopt -s nullglob
for f in "$HERE"/.audit-*.lean "$HERE"/.apex-*.lean; do
grep -qxF "$f" <<<"$LITTER_BEFORE" || rm -f "$f" "${f%.lean}.olean"
done
shopt -u nullglob
rm -rf "$STASH"
}
trap cleanup EXIT INT TERM
cp "$HERE/Proofs/$VICTIM_MOD.lean" "$STASH/victim"
cp "$HERE/check.sh" "$STASH/check"
cp "$HERE/HARNESS.sha256" "$STASH/pins"
# The axiom audit, lifted from the shipping button so the tested logic is the
# shipping logic. BOTH tiers live under the one "Phase 3" marker — the
# per-certificate arithmetic audit and, below it, the apex boundary check. An
# earlier draft of this file lifted them as two markers, got an empty driver for
# the second, and the driver still cleared a line-count sanity check because the
# CERTS array padded it. So the guard below looks for the two diagnostics we
# intend to provoke, not for a number of lines.
lift() {
# set -euo pipefail, verbatim from the button. The -e is load-bearing and was
# missing from an earlier draft: the phase's Lean work happens in a subshell
# and the phase ends with a bare `echo ""`, so without -e a subshell that
# exits 1 is masked by the echo's success and the driver reports green while
# printing APEX AUDIT FAILED. The button gets this right at check.sh:32; a
# lift that does not copy it tests something the button never runs.
awk '/^# ── Phase 3: axiom audit/{f=1} f&&/^# ── (Phase 3c|Phases end)/{exit} f{print}' \
"$HERE/check.sh" > "$STASH/payload.sh"
{ echo 'set -euo pipefail'
echo 'source ~/aeneas-toolchain/env.sh'
echo "HERE=\"$HERE\""
echo 'AENEAS_LEAN="$AENEAS_HOME/backends/lean"'
echo "TIMEOUT=$TIMEOUT"
sed -n '/^EXPECTED=/p;/^AUDIT_IMPORTS=(/,/^)/p;/^CERTS=(/,/^)/p' "$HERE/check.sh"
cat "$STASH/payload.sh"
} > "$STASH/p3.sh"
# The two diagnostics must come from the PAYLOAD; the three definitions are
# preamble, so those are asserted on the assembled driver.
for want in 'AXIOM AUDIT FAILED' 'APEX AUDIT FAILED'; do
if ! grep -qF "$want" "$STASH/payload.sh"; then
echo "FATAL: the lifted driver has no '$want' — check.sh's phase markers moved."
exit 1
fi
done
for want in 'CERTS=(' 'AUDIT_IMPORTS=(' 'EXPECTED='; do
if ! grep -qF "$want" "$STASH/p3.sh"; then
echo "FATAL: the lift carries no '$want' — a definition the phase needs is missing."
exit 1
fi
done
"$HERE/lift-guard.sh" "$STASH/payload.sh" "$STASH/p3.sh" "check.sh Phase 3" || exit 1
}
lift
recompile() {
( cd "$AENEAS_LEAN" && lake env bash -c "
set -uo pipefail
cd '$HERE/gen' && export LEAN_PATH=\"\$LEAN_PATH:\$PWD:$HERE\"
cd '$HERE'
LEAN_TIMEOUT=$TIMEOUT '$HERE/lean-guard' Proofs/$VICTIM_MOD.lean
" ) >/dev/null 2>&1
}
expect() { # expect <driver> <label> <want-rc> <want-substring>
local drv="$1" label="$2" want_rc="$3" want_txt="$4" out rc
out=$(bash "$STASH/$drv.sh" 2>&1); rc=$?
if [ "$rc" -ne "$want_rc" ]; then
echo " ✗ $label: exit $rc, expected $want_rc"; tail -5 <<<"$out" | sed 's/^/ /'
FAILURES=$((FAILURES+1)); return
fi
if ! grep -qF "$want_txt" <<<"$out"; then
echo " ✗ $label: exit code right, diagnostic wrong (rejected for the wrong reason)"
echo " wanted: $want_txt"; tail -5 <<<"$out" | sed 's/^/ /'
FAILURES=$((FAILURES+1)); return
fi
echo " ✓ $label"
}
echo "=== selftest-tiers: attacking the arithmetic/apex boundary ==="
echo " victim: $VICTIM_CERT in Proofs/$VICTIM_MOD.lean"
echo " oracle: $ORACLE (from this repo's own apex boundary)"
# Prime the victim. This test rebuilds that one module twice, and its cleanup
# deliberately deletes the .olean if it dies mid-case — so on entry the artifact
# may be missing or stale from an interrupted earlier run. Rebuilding it here
# means a red control is a real red, not leftovers.
if ! recompile; then
echo "FATAL: Proofs/$VICTIM_MOD.lean does not compile before any attack — fix the tree first."
exit 1
fi
expect p3 "control: both tiers pass" 0 "no curve/scalar/backend axioms"
# ── 1. THE ONE THAT MATTERS ────────────────────────────────────────────────
# Introduce a hash oracle into an arithmetic certificate's PROOF. The statement
# does not change, so the statement digest would not move; only the cone does.
# The arithmetic tier's whole claim is that this cannot happen unnoticed.
python3 - "$HERE/Proofs/$VICTIM_MOD.lean" "$VICTIM_CERT" "$ORACLE" <<'PY'
import sys, re
f, cert, oracle = sys.argv[1], sys.argv[2], sys.argv[3]
short = cert.split('.')[-1]
s = open(f).read()
m = re.search(r'^(theorem %s\b.*?:=\s*by\b)' % re.escape(short), s, re.M | re.S)
assert m, f"could not find a tactic proof for {short}"
inject = m.group(1) + f"\n have _oracle_leak := {oracle}"
open(f, "w").write(s[:m.start(1)] + inject + s[m.end(1):])
PY
if recompile; then
expect p3 "case 1: an apex oracle in an arithmetic certificate" 1 "AXIOM AUDIT FAILED"
else
echo " ✗ case 1: the injected module did not compile (case is vacuous)"
FAILURES=$((FAILURES+1))
fi
cp "$STASH/victim" "$HERE/Proofs/$VICTIM_MOD.lean"
if recompile; then
SAFE_EXIT=1 # victim is back to its committed source and rebuilt from it
else
echo " ✗ restore: the ORIGINAL module no longer compiles — tree left for inspection"
FAILURES=$((FAILURES+1))
fi
# ── 2/3. the apex boundary moved, either way ───────────────────────────────
# Phase 3b requires the apex cones to equal the documented boundary EXACTLY.
# Widening it is how an oracle would be smuggled in; narrowing it is how a
# real dependency would be hidden. Both must fail.
sed -i "s/ALLOWED='\[propext, /ALLOWED='[propext, Classical.byContradiction, /" "$HERE/check.sh"
lift
expect p3 "case 2: apex boundary widened by one name" 1 "APEX AUDIT FAILED"
cp "$STASH/check" "$HERE/check.sh"
sed -i "s/ALLOWED='\[propext, Classical.choice, /ALLOWED='[propext, /" "$HERE/check.sh"
lift
expect p3 "case 3: apex boundary narrowed by one name" 1 "APEX AUDIT FAILED"
cp "$STASH/check" "$HERE/check.sh"
lift
expect p3 "restored: both tiers pass again" 0 "no curve/scalar/backend axioms"
echo ""
if [ "$FAILURES" -eq 0 ]; then
echo "SELFTEST PASSED — the arithmetic tier cannot silently acquire an oracle,"
echo "and the apex boundary cannot be moved in either direction."
exit 0
fi
echo "SELFTEST FAILED: $FAILURES case(s) did not behave as claimed."
exit 1