saymrwulf/ltl-accumulator-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/ltl-accumulator-verified.git synced 2026-09-04 20:03:44 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Compare commits

base: saymrwulf:8530cc73f427ab04d3f35e1d31d3c858a11f2aa3
Branches Tags
saymrwulf:main
..
compare: saymrwulf:1ae8263404c64730524988a1dca9d0bca34d2750
Branches Tags
saymrwulf:main

10 commits
8530cc73f4 ... 1ae8263404

Author SHA1 Message Date
mrwulf
1ae8263404 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
2a886b6be9 fidelity: deliberate re-pin of the pacta subject (cd3b1bc -> a036624) 
The round-16 sweep went 49 GREEN, 1 RED, and the RED was this repository's
Phase 4 refusing to run: PACTA SUBJECT MISMATCH, signing.py and
transparency.py differing from the pin. That is pacta-subject-unpinned
(round-8, GPT-5.6) firing on its first genuine drift — the gate built so that
fidelity could never again count agreement with an unnamed program.

The drift is known and intended: pacta 5e35a53 anchored the signer path to the
package (register: signer-backend-depends-on-cwd) and a036624 added the
additive slh_dsa block to make_signed_tree_head (operator decisions
2026-08-06). Re-pinned deliberately with pacta_pin.py --write: 5 modules at
pacta a036624. PACTA-PIN.sha256's own entry in HARNESS.sha256 updated.

Full instrument set re-run green at the re-pinned state: check.sh 92s,
selftest_audit 280s, selftest-harness 0s, selftest_statements 38s.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-07 01:41:18 +02:00
mrwulf
be4f742b29 verification: guard the accumulator's two lifts (port lift-guard, assert on the payload) 
The four forks ship lift-guard.sh and call it from eight files each. This
repository had no lift-guard.sh at all and called it zero times, while lifting
Phase 0c (selftest-harness.sh) and Phase 3d (selftest_statements.sh). Its lifts
got a line-count sanity check and nothing else — no analysis of which variables
the payload READS against which the driver DEFINES, and after yesterday's fix
no errexit check either. It was the one place that class could still recur.

A SECOND defect surfaced while porting, and it is the more interesting one.
Both lifts assembled the driver inline, with no payload file anywhere:

    { echo 'set -euo pipefail'; echo "HERE=..."; sed -n '...' check.sh } > DRIVER
    if [ "$(wc -l < "$DRIVER")" -lt 40 ]; then ... refuse ...

so the size check measured the CONCATENATED DRIVER — bindings included. A lift
that recovered almost nothing still cleared the threshold on the strength of
the lines the test itself prepended. That is exactly the defect round-7
lift-guard-payload-assert reported and that the forks closed with the words
"all six lift sites now assert on payload.sh". Six counted the forks. These two
were never in the count, so a finding recorded as closed was measuring the
wrong population — the same error this estate keeps finding in new costumes.
Both sites now write payload.sh / payload3d.sh and assert on those.

lift-guard.sh is byte-identical to the forks' (4f61c113). It is executable, so
this repository's own self-deriving Phase 0c rule required a pin before it
would run at all: required set == pinned set, verified.

WIRING PROVEN RATHER THAN ASSUMED. With lift-guard.sh stubbed to exit 1, each
self-test halts AT the guard, naming its phase, before a single attack case
runs. Guard restored, pins re-verified.

Certified: button + all three self-tests GREEN (check.sh 86s, selftest_audit
258s, selftest-harness 1s, selftest_statements 34s). The other five
repositories are unchanged from the tree round-15 certified 50/50 and were not
re-run; this commit does not claim they were.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-04 13:39:19 +02:00
mrwulf
a0d11b44d9 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:29 +02:00
mrwulf
888796a16e 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
212db783a9 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
b1fb6eba7c accumulator: a run that is not attestation-ready must not exit 0, and must name its subject 
Two round-7/8 findings, both closed here.

`acc-exit0-fidelity` — CRITICAL, raised INDEPENDENTLY by both reviewers
(Claude F1, GPT-5.6 F10) and lost from the round-8 work list by the F-number
collision the finding register now prevents.

check.sh emitted a careful pair of markers — ATTESTATION GREEN only when
fidelity actually ran — and then returned 0 either way. The marker discipline
was right; the exit code contradicted it. A caller doing the obvious thing

    ./check.sh && append

read success from a run whose own last line said NOT attestation-ready. And
because pacta is not part of this estate, the skip branch is the ONLY branch a
third party ever takes: for everyone but the author the button always returned
0 without ever checking definition fidelity. Reproduced here before fixing —
PACTA_SRC=/nonexistent ./check.sh printed "FIDELITY NOT RUN" and exited 0.

An exit code is what programs read. The contract is now:

    fidelity ran     exit 0   ATTESTATION GREEN
    SKIP_FIDELITY=1  exit 3   explicit opt-out, distinguishable, not success
    pacta absent     exit 1   nobody opted out; a real failure to establish
                              the property the button exists for

All three verified. The self-tests are unaffected: every SKIP_FIDELITY case
already expected a non-zero exit and asserts on a diagnostic from an earlier
phase, and the control compiles modules directly rather than invoking check.sh.
29 assertions across the three self-tests, all green.

`pacta-subject-unpinned` — HIGH, GPT-5.6 round 8.

Phase 4 compared this repository's Lean definitions against "the deployed
verifier" by importing whatever sat at $PACTA_SRC — no repository, no commit,
no clean state, no hashes. It pinned the fidelity OUTPUTS while leaving the
SUBJECT anonymous, so any program producing the same finite family of answers
passed, and the recorded result named no version of the thing it agreed with.

fidelity/pacta_pin.py pins the transitive set of pacta modules the harness
ACTUALLY LOADS — discovered by importing its entry point and reading
sys.modules, a membership property rather than a directory glob. A glob would
pin files the comparison never touches and miss anything loaded from elsewhere;
this estate has been bitten by name-shaped measurement before. Five modules at
pacta cd3b1bc — the same checkout the reviewer independently recorded.

Negative-tested, all three rejected by name: tampered bytes, a module loaded
but absent from the pin, and the pin file deleted. Refusing to pin a dirty
pacta tree is also enforced — a pin taken over uncommitted edits names a
subject nobody else can obtain.

PACTA-PIN.sha256 joins HARNESS_EXTRA. It is not executable, so it would
otherwise have sat outside the harness set, and a subject pin an attacker may
rewrite pins nothing — the same shape as the forgeable .audit-basis that
remains open as `auditonly-basis-forgeable`.

This does not widen the claim: byte identity of a source tree is not proof the
deployed service runs it, and finite-family agreement is not extensional
equality. It names the subject.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
 2026-08-02 21:40:35 +02:00
mrwulf
6212aa1624 Round-7 F2: account for every constant the kernel sees 
THE DEFECT, demonstrated by a reviewer with a working payload. The driver
surface is reported by an `#eval` inside Proofs/Inventory.lean. Anything
declared AFTER that command is in the compiled object file but does not exist
in the environment while the command runs, so the walk cannot see it. The
reviewer appended

    def bait : Nat := 0
    theorem bait.smuggled : forall n : Nat, n + 0 = n := ...

re-pinned, and ran the button. It printed "no axiom, no claim", the statement
digest was BYTE-IDENTICAL to the clean tree, and the run went green — while a
theorem with a real axiom cone sat in the environment. In neither walk: not
corpus, because an instrument is not corpus; not driver surface, because it
post-dates the emitter. In no allowlist. Pinned by nothing.

This repository also had no kernel-side scan at all. Its axiom gate was a
source-text grep, evadable by a leading space — which its own selftest case 12
already exploited.

THE FIX, ported from the ed25519 forks:

  · a kernel-side axiom-declaration gate that reads every compiled .olean via
    readModuleData. It sees what was actually stored, regardless of
    indentation, attributes, privacy, or where a declaration sits relative to
    any #eval. Membership self-derives from the manifest and the module count
    must match, so a deleted artifact cannot make the scan vacuous.
  · the ACCOUNTING IDENTITY, as set containment:

        every constant the kernel sees  in  corpus inventory  union  instrument surface

    The two walks read ENVIRONMENTS; the gate reads OBJECT FILES. What a walk
    cannot see because of where it sits in a file, the object file still holds.
    That asymmetry is the entire content of this fix.

    Compared as SETS deliberately. Counts cannot express the relation — an
    object file may hold two physical copies of one lazily-materialised
    equation lemma while an environment holds one constant per name — and
    arithmetic between those views misled the ed25519 version twice before it
    was stated as containment.

PLACEMENT differs from the forks, for a reason worth recording: there the
audit drivers are members of the compile manifest, so a gate beside the
compile phase finds them. Here AxiomCheck is compiled by Phase 3 and Inventory
by Phase 3b, so an earlier gate fails on a missing artifact — which it did,
correctly, on the first port. It runs inside Phase 3b, because the instruments
are exactly what it must see.

VERIFIED with the reviewer's own payload, which previously went green:

    ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:
      bait
      bait.smuggled

selftest_audit.sh: 14 attack cases -> 15. Note in the new case, because it
cost two iterations: `theorem bait.smuggled : True := trivial` does NOT
exercise this gate — Phase 1's stub audit greps for `: True :=` and catches it
first. Real defence in depth, but the naive payload never reaches the gate
under test, so the case uses the reviewer's original.

Two residues fixed while adding it, both the same shape: a case that was last
when written, leaving state the next case inherits. Case 13 restored
AxiomCheck.lean but not its pin; case 9 left its rogue gen file. Fixed at the
point of use so each case keeps testing what it tested before.

Button green (234 declarations across 11 modules, all accounted for),
15/15 self-test green, ATTESTATION GREEN with fidelity.
 2026-08-02 02:51:55 +02:00
mrwulf
25699a9cf7 Phase 0a: purge compiled artifacts before compiling 
P0-a was applied to the four ed25519 repositories on 2026-07-30 and never
here. Found by the control repo's capability matrix, which asks the property
rather than looking for a phase by name.

The finding that made it matter there applies verbatim: a verification that
never cleans up cannot distinguish "these proofs check" from "these proofs
check GIVEN WHATEVER IS LYING AROUND". Compiled artifacts are gitignored, so
no `git status` can show a reader that a verdict rested on an object from an
earlier run of a different script.

This repository has no --audit-only mode, so the purge is unconditional.
Button green (80s) and the 14-case self-test green after the change.
 2026-08-01 16:11:10 +02:00
mrwulf
9c78ce88ae P2-b: close classes 9 and 15 — the instruments, and the places nothing looked 
CLASS 15 — a Lean file where no phase was looking. The dead-file scan read
Proofs/*.lean and gen/LTLAcc/*.lean and nothing else. A module at the
verification root, or under any other gen/ subdirectory, was neither
compiled nor rejected — while remaining importable by name, since LEAN_PATH
contains both roots. That is a source of the corpus that no phase reads and
no pin covers, which is exactly what the dead-file gate exists to forbid; it
was simply looking in two places instead of everywhere. Now nothing may live
in either root but the two enumerated sets.

CLASS 9 — the instruments' own declaration surface. AxiomCheck.lean and
Inventory.lean perform the audit and are therefore not corpus, so nothing
inventoried what THEY declare. Inventory.lean now walks both: AxiomCheck by
module index, and itself as the module still being elaborated, whose
declarations are the ones the environment reports with no originating
module. That is what makes the inventory cover the instrument that produces
it rather than exempting itself.

The policy is not "declare nothing" — this file legitimately declares its
machinery. It is that an instrument may declare only inert definitions. An
axiom here would widen the trusted base without appearing in any
certificate's cone; a theorem here would be a claim no certificate covers
and no allowlist pins. A flat ban on theorems was WRONG and was measured to
be wrong: defining a function by well-founded recursion makes the elaborator
emit its own obligations, and axiomCone._proof_1 rejected this very file.
The distinction that holds is whether a theorem is a claim someone wrote or
an artefact of a definition declared alongside it — an artefact's name
extends the name of a constant declared with it.

Observed surface: 18 declarations, 16 def and 2 generated obligations, no
axiom, no standalone claim.

The drivers are byte-pinned already, so this does not pin WHICH definitions
they contain — that would add a thing to maintain without adding a thing to
catch. It adds the property byte-pinning cannot give: that no instrument
declares an axiom or a claim, whatever its bytes are.

selftest_audit.sh: 10 cases -> 14. Case 12 uses an INDENTED axiom, because
Phase 1's source grep catches an unindented one and the point is to reach
the kernel-side walk standing behind it.

TWO DEFECTS IN THE TEST HARNESS, found while adding the cases.

· The scratch tree copied verification/ only, but the button also reads
  README.md and STATEMENT-MAP.md from the repository root. check.sh
  therefore ALWAYS died in Phase 3c in the scratch tree, which made every
  `if check.sh; then <attack not caught>` guard unfirable — check.sh could
  not pass in there even with no attack at all. Only the diagnostic greps
  were doing any work. The documents are now copied, and the negative test
  below proves the guard is live: with the driver-surface check disabled,
  check.sh PASSES a tree whose inventory driver declares
  `axiom driver_cheat : False`.
· Case 9 was the last case when it was written and left its rogue gen file
  in place. Harmless then; the new cases inherited it. Cleaned up between
  the blocks rather than inside case 9, so that case still tests what it did.

Also fixed while here: Phase 3b compared the compile manifest against
Inventory.lean by grepping the WHOLE FILE for a backticked module name, so
prose counted — a doc comment naming a module broke the count, and in the
other direction a doc mention of a module missing from the array would have
satisfied the presence check and hidden the omission. It now reads the
arrays.

Both new gates negative-tested by removal. Button green, self-test green.
 2026-07-31 14:18:40 +02:00
15 changed files with 1135 additions and 50 deletions
Show stats Expand all files Collapse all files

2
ATTESTATION-RUNBOOK.md
View file

@ -79,7 +79,7 @@ NEW_SIZE = 13
| Forgejo mirrors | `https://zkdefi.org/saymrwulf/<repo>.git` (anonymously readable) | pull-synced by server cron nightly 03:00 UTC (`/home/admin/cloud/bin/reconcile-mirrors.py`, log `.reconcile.log`); verify per step A5 |
| log public key | `lean-transparency-log/provider.ed25519.pub` (PEM) | fingerprint `874c8a00…a56a` in `log-metadata.json` |
| log PRIVATE key | **RESOLVED 2026-07-12**: laptop-side, mode 0600, inside a gitignored state dir of the pacta working tree (exact path in operator-private notes, deliberately not in this public file); public half byte-matches `provider.ed25519.pub`. NOT on the droplet. encrypted SD backup exists (A3b, operator, 2026-07-14) | A3 done; A3b done |
| producer driver | **RESOLVED 2026-07-12**: it exists and is committed — pacta's `provider/` CLI (`python3 -m pacta_provider`: `check` → signed attestation; `log-append` → leaf + signed STH + receipt; `log-publish` → public face). Heads are signed with `signing_backend: verified-dalek-serial` (the dogfooded verified signer), `self_inclusion: verified`. Only the per-run orchestration was session work | see step A4 (rehearsal, not reconstruction) |
| producer driver | **RESOLVED 2026-07-12**: it exists and is committed — pacta's `provider/` CLI (`python3 -m pacta_provider`: `check` → signed attestation; `log-append` → leaf + signed STH + receipt; `log-publish` → public face). Heads are signed with `signing_backend: verified-dalek-serial` (the dogfooded signer binary built from the verify-path-proven dalek fork; the signing operation itself is not proven — clarification added 2026-08-08, the event is unchanged), `self_inclusion: verified`. Only the per-run orchestration was session work | see step A4 (rehearsal, not reconstruction) |
| server deployment | the private infrastructure repo (github, `master`) — since `a186bac` includes the ltl vhost/service/reconstruct.py, md5-verified == droplet | see its `DEPLOY.md` § "The LTL service" |
---

12
README.md
View file

@ -35,8 +35,10 @@ kernel-checked; the audit
surface is defined and green (`verification/check.sh`, exit 0). See
[STATEMENT-MAP.md](STATEMENT-MAP.md) for the paper↔Lean review surface and
[KNOWN-GAPS.md](KNOWN-GAPS.md) for the honest scope ledger.
Reviewed across **six** external adversarial rounds (GPT-5.6 + a second
Claude; zero broken theorems in any round; both approved). The audit
Reviewed across **six** external adversarial rounds through the entry-13
freeze (GPT-5.6 + a second Claude; zero broken theorems in any round; both
approved), plus the estate-wide rounds 7–9 whose accumulator findings are
harvested in the private register and fixed here. The audit
surface is an environment-derived inventory (`Proofs/Inventory.lean` +
pinned allowlist — 222 constants, 61 human-reviewed cones, self-tested by
`selftest_audit.sh`); the review kit is push-button reproducible
@ -44,8 +46,10 @@ pinned allowlist — 222 constants, 61 human-reviewed cones, self-tested by
`acceptIncl`/`acceptCons_sound` route the theorems through the named
acceptance predicates; fidelity = agreement over pinned families
(230,271 + 230,016 baseline; 73,573 lied-size boundary cases with
3,867 expected one-sided divergences — KNOWN-GAPS gaps 14/15, not
extensional equality). Doc counts are asserted by check.sh Phase 3c.
**0 divergences since the sn==0 fix**, pacta `ddbb5a4`, 2026-07-23 — gap 14
is CLOSED; the historical 3,867 one-sided divergence family is preserved at
tag `vulnerable/sn0-consistency-fd2f6ba`. Still finite-family testing, not
extensional equality — the open deployment boundary is gap 15). Doc counts are asserted by check.sh Phase 3c.
How the append was done — release tuple, preflight, candidate-inspection
gate, and the 12→13 structural rehearsal — is recorded in
[ATTESTATION-RUNBOOK.md](ATTESTATION-RUNBOOK.md).

35
STATEMENT-MAP.md
View file

@ -29,11 +29,11 @@ This map is the review surface.
| Lemma 2, whole-tree instance | `extractMTH` + `extractMTH_correct` | Descent | sha256 (+choice) |
| Lemma 2, ConsRec instance (Thm 3 steps 1–2) | `consRecBinding` | Binding3 | sha256 (+choice) |
| Theorem 2 (inclusion soundness, explicit 𝓔) | `extractIncl` + `extractIncl_correct` | Extract | sha256 (+choice) |
| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct`; `extractCons_correct_paper` at the paper's exact quantifiers (n₀=0 discharged); `acceptCons_sound` routes it through the named `acceptCons` predicate (size bound derived from acceptance via `consRec_some_le`). Covers the MECHANIZED accept set; transfer to the deployed verifier is conditional on the pinned-pair side condition of gap 14 | Theorem3 | sha256 (+choice) |
| Theorem 3 (consistency soundness, explicit 𝓔′) | `extractCons` + `extractCons_correct`; `extractCons_correct_paper` at the paper's exact quantifiers (n₀=0 discharged); `acceptCons_sound` routes it through the named `acceptCons` predicate (size bound derived from acceptance via `consRec_some_le`). Covers the MECHANIZED accept set; transfer to the deployed verifier is conditional on the deployment refinement invariant of gap 15 (gap 14 closed 2026-07-23) | Theorem3 | sha256 (+choice) |
| Prop 1(1) (pin monotonicity + prefix) | `pinAccept`, `pinAccept_monotone`, `pin_prefix_correct` | PinStore | sha256 (+choice) |
| Prop 1(2), Merkle share | `fork_distinct` (different roots ⇒ different content); transferability = signature layer, out of scope | PinStore | sha256 |
| non-vacuity guards (anti-pigeonhole) | `extractIncl_nonvacuous`, `extractMTH_nonvacuous`, `extractCons_nonvacuous`, `pin_prefix_nonvacuous` | Extract/Descent/Theorem3/PinStore | sha256 |
| definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 230,271 inclusion + 230,016 consistency over the pinned case families — **not extensional equality**: the lied-size family (73,573 cases) pins the known one-sided divergence of gap 14 (3,867 expected, deployed-accepts-only, direction asserted) | fidelity | (testing) |
| definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 230,271 inclusion + 230,016 consistency over the pinned case families — **not extensional equality**: the lied-size family (73,573 cases) pins **0 divergences** at the current subject (post-`ddbb5a4` pacta, see PACTA-PIN.sha256; gap 14 closed 2026-07-23 — the historical 3,867 one-sided family is recorded in its closure note) | fidelity | (testing) |
Note on "assumption-free" (paper §10(i)): `incl_complete`'s cone lists
`LTLAcc.sha256`, but the theorem assumes **no property** of it — it
@ -66,8 +66,29 @@ cross-checked against the inventory's independently computed cones.
asserted against the allowlist/CONES/harness by check.sh Phase 3c on
every run — stale-count drift is now a red button, not an erratum:
review R4-1, after three consecutive rounds of hand-edit failures.)
`verification/selftest_audit.sh` attacks the gate with nine injection
cases (attributed/indented/private/instance declarations, a nested
namespace reusing an audited basename, a smuggled axiom, a deleted
declaration, and unmanifested Proofs/ and gen/ modules) — each must
fail the exact production gate.
`verification/selftest_audit.sh` attacks the gate with fifteen
injection cases (attributed/indented/private/instance declarations, a
nested namespace reusing an audited basename, a smuggled axiom, a
deleted declaration, and unmanifested Proofs/ and gen/ modules) — each
must fail the exact production gate. Four were added on 2026-07-31 and
close two classes the earlier suite did not reach:
* **A Lean file where no phase was looking.** The dead-file scan read
`Proofs/*.lean` and `gen/LTLAcc/*.lean` and nothing else, so a module
at the verification root or under any other `gen/` subdirectory was
neither compiled nor rejected — while remaining importable by name,
since `LEAN_PATH` contains both roots. Cases 10 and 11 forbid both.
* **The instruments' own declaration surface.** `Proofs/AxiomCheck.lean`
and `Proofs/Inventory.lean` perform the audit and are therefore not
corpus, so nothing inventoried what THEY declare. `Inventory.lean` now
walks both — including itself, as the module still being elaborated —
and fails closed on an axiom, or on a theorem that is not an artefact
of a definition declared alongside it. Cases 12 and 13 attack each
driver; case 12 uses an INDENTED axiom, because Phase 1's source grep
catches an unindented one and the point is to reach the kernel-side
walk behind it.
Both new gates were negative-tested by removal. With the driver-surface
check disabled, `check.sh` PASSES a tree whose inventory driver declares
`axiom driver_cheat : False` — which is the whole reason the check
exists.

5
docs/optimistic-accountability.md
View file

@ -145,8 +145,9 @@ rollup metaphor to be remarkable.
- Mechanized statements: `STATEMENT-MAP.md` (this repo); the fraud-
proof-generator reading of Theorem 3 is `extractCons_correct` +
`acceptCons_sound`; scope boundaries in `KNOWN-GAPS.md` (esp. gap 14:
the deployed-verifier side condition; gap 4: the signature layer,
`acceptCons_sound`; scope boundaries in `KNOWN-GAPS.md` (esp. gap 15:
the deployment refinement invariant — gap 14, the historical deployed-verifier
divergence, closed 2026-07-23; gap 4: the signature layer,
where equivocation-evidence transferability lives).
- Deployed anatomy: leaf → `entries/NNNNNN.json`; head →
`latest-sth.json` (+ `sth-history.jsonl`); the head is signed by the

16
verification/HARNESS.sha256
View file

@ -1,15 +1,19 @@
e7d422f0be9a9e6f5465058292e30c711d52856428da2b01c470a57ec181540c AUDIT-MANIFEST.txt
7ab1bfbafc8ac9ab34d1e0eaa71ba2f1f9912121345cc1af281bcb1d2ec30ad2 check.sh
8d72867f96188806618be221ef6e66ff221c0bd011b8f73516ae804a5f77a24f check.sh
90fcad217c7b6507abecf37a41d57149f06a8955a72e60dc03616933f981ed6b driver-allowlist.txt
070147e2667053bd5d5e1174b969fc6c91bfcf15ded1a5bff57754e15f416885 fidelity/lean_defs.py
9661bc2d33e907453ab4378da918589a709127b2e117ef1fd578d4e0472edf87 fidelity/pacta_pin.py
5d82462a002ac9fc782e95afe78b7719ba64b6410b5d2bfa620fe5317367dbf2 fidelity/run_fidelity.py
503babb3f4e6aff82ebd59e8752469ecd60fba440ed3b11b3f97c2b655fbd9bf gen/LTLAcc/HashExternal.lean
f1eb5cdd158e30df14c59065fe2050448c77b5262b282208fa831d050f6b6a71 inventory-allowlist.txt
f66fb98d2a09503d9bd0d60dc964545eea6dc94b9bbb9246d1021195b79f2601 inventory_gate.sh
d628cc64efe920304f4ad8319d9b880a942abb6d850f4022fa1a26af7e8c34a1 inventory_gate.sh
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
ce4c4e3d87434b9663f46de25ce34b48a0cf0d392e0a320a0787b4674a2d7b61 lean-toolchain
127fecf2a6938ec24dcc7604756b6b78fcc9ed9343bab7ec9e6bb03b3a9ca0be PACTA-PIN.sha256
eda93f520546a692926b2a46bcb79332e1795879e5083327a8bf2404aca5cf87 Proofs/AxiomCheck.lean
25344c8441077277addd6b4eb769b2c0e3b173afc28d3a6e8aeba0580c22a87f Proofs/Inventory.lean
82d41c634a2e9adfc2cc74c202d025e57411687796f820765d45608f3fb4cb20 Proofs/Inventory.lean
0b8a0fc6947af1d1e600a756eb2b07dc88d189b21df3220c4501a41be8b33f1e run_bare.sh
67a44e0db818efc48dede26f73f76f1221424bb23e40e29d859b12d0d300403b selftest_audit.sh
3d5898161d663eccad162269a5a6c102319077e22e1f2d89a8bfcab6926d29f6 selftest-harness.sh
cf6d4d8210e224a054d4ab693c28c83e7a9ddebda05da47d6ec311d825a606c0 selftest_statements.sh
473e2463d9c26653c8435ad6758044742f200eb13ea0db4b8f076466c08bd87a selftest_audit.sh
733eb2cf4eaf9101433d75dbedfc45681cff44e1dbfdc841e6b9dba350ef1570 selftest-harness.sh
c85d7a0fc39fbf06ec2c85d2f42a65813c475cae7cf60e6d140948215c62eabc selftest_statements.sh
4f61c1135f8afc615e686bd267a062229bf349416caebe070eafca510036d1a4 lift-guard.sh

8
verification/PACTA-PIN.sha256 Normal file
View file

@ -0,0 +1,8 @@
# pacta subject pinned by fidelity/pacta_pin.py --write
# commit a03662438a13cd1eba2fff3c35aded5f45093b06
# 5 module(s), discovered by import, not by glob
a1bcc5d700071f531e6fe16989884412cb3fb0f2702adfdf5212d4bc84eba2bc pacta/__init__.py
31dd6ab7b3121a433c7c8b082ec2d011d1958782470481137db0513a9822532d pacta/postquantum.py
bd3c7b150f13cfb92aef84b85b659d902d0728ce8559bf09f02ad2c79f65ea50 pacta/signing.py
157bcebbe0134226060a5bf2fd5650e1ad0320d7820777389398d1cdb92bc538 pacta/transparency.py
7130d5a770db7af4d294389625cf5f0c4228ed562b78bd7ca148ca010087d834 pacta/yamlio.py

87
verification/Proofs/Inventory.lean
View file

@ -40,6 +40,7 @@ import Proofs.Binding3
import Proofs.Refactor
import Proofs.Theorem3
import Proofs.PinStore
import Proofs.AxiomCheck
open Lean
@ -52,6 +53,17 @@ def corpusModules : Array Name :=
`Proofs.Consistency, `Proofs.Binding3, `Proofs.Refactor,
`Proofs.Theorem3, `Proofs.PinStore]
/-- The audit INSTRUMENTS, as opposed to the corpus. They are Lean modules in
the audited tree, so what they declare is part of this repository's
surface — but they are not proofs, and nothing may rest on them.
`Proofs.AxiomCheck` is reachable here because this module imports it; this
module ITSELF has no module index while it is being elaborated, so its own
declarations are the ones the environment reports with no originating
module, and they are checked that way below. That is what makes this
inventory cover the instrument that produces it. -/
def driverModules : Array Name := #[`Proofs.AxiomCheck]
def kindOf : ConstantInfo → String
| .axiomInfo _ => "axiom"
| .defnInfo _ => "def"
@ -151,6 +163,81 @@ def ppAll (e : Expr) : MetaM String := do
for l in sorted do
IO.println l
IO.println s!"INV-COUNT|{sorted.size}"
-- ── CLASS 9: the instruments' own declaration surface ────────────────────
-- The loop above walks the CORPUS. It says nothing about the two modules
-- that perform the audit, and until 2026-07-31 nothing else did either: an
-- `axiom` or a `theorem` added to Proofs.AxiomCheck or to this file was
-- invisible to every phase of the button. Both are covered here.
--
-- Proofs.AxiomCheck is reachable by module index because this module imports
-- it. THIS module has no index yet — it is still being elaborated — so its
-- own declarations are exactly those the environment reports with no
-- originating module, which is how the inventory covers the instrument that
-- produces it rather than exempting itself.
--
-- The policy is not "declare nothing": this file legitimately declares the
-- machinery above. The policy is that an instrument may declare only inert
-- definitions. An `axiom` here would widen the trusted base without
-- appearing in any certificate's cone; a `theorem` here would be a claim
-- that no certificate covers and no allowlist pins.
let mut drvIdxs : Array Nat := #[]
for m in driverModules do
match env.getModuleIdx? m with
| some i => drvIdxs := drvIdxs.push i
| none => throwError "INVENTORY ERROR: driver module {m} is not imported"
let mut drvNames : Std.HashSet Name := {}
let mut drvConsts : Array (Name × ConstantInfo) := #[]
for (n, ci) in env.constants.toList do
let here : Bool :=
match env.getModuleIdxFor? n with
| some i => drvIdxs.contains i
| none => true -- declared by this file, still being elaborated
if here then
drvNames := drvNames.insert n
drvConsts := drvConsts.push (n, ci)
let mut drv : Array String := #[]
for (n, ci) in drvConsts do
let k := kindOf ci
-- An AXIOM in an instrument is never acceptable: it would widen the trusted
-- base without appearing in any certificate's cone.
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."
-- A THEOREM needs care rather than a flat ban. Defining a function by
-- well-founded recursion makes the elaborator emit its own proof
-- obligations — `LTLAccAudit.axiomCone._proof_1` is one, and a flat ban
-- rejected this very file. The distinction that matters is whether the
-- theorem is a CLAIM someone wrote or an ARTEFACT of a definition here:
-- an artefact's name extends the name of a constant declared alongside it,
-- a standalone claim's does not.
if k == "theorem" && !drvNames.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, which no certificate covers and no allowlist pins."
-- THE CONE. Round-8 review (Claude, `drv-surface-no-cones`,
-- `accounting-certifies-enumeration`): these rows carried name and kind
-- only, so when the accounting identity proved every kernel constant was
-- ENUMERATED, a claim planted in an instrument satisfied it and was then
-- examined by nothing. The reviewer's payload was exactly
-- DRV|LTLAccAudit.bait.smuggled|theorem
-- with cone [propext, Classical.choice, Quot.sound] — admitted, counted,
-- and covered by no allowlist row, no statement digest and no cone check.
-- Their verdict: the identity "converted 36 declarations nobody enumerated
-- into 36 declarations nobody examined."
--
-- With the cone here and the rows pinned in driver-allowlist.txt by the
-- same gate the corpus uses, the identity and the audit coincide. The
-- name-prefix rule above stays as a readable first check but is no longer
-- load-bearing: the reviewer showed it breaks in one line, and membership
-- in a committed allowlist does not.
let drvCone := axiomCone env n
let drvConeStr := ",".intercalate (drvCone.toList.map (·.toString))
drv := drv.push s!"DRV|{env.mainModule}|{n}|{k}|{drvConeStr}"
let drvSorted := drv.qsort (· < ·)
for l in drvSorted do
IO.println l
IO.println s!"DRV-COUNT|{drvSorted.size}"
-- FAIL CLOSED: the statement surface must cover the inventory exactly. If
-- these ever diverge, some constant is inventoried but unbound — which is
-- precisely the gap this section exists to close.

337
verification/check.sh
View file

@ -24,6 +24,13 @@ CORES="${LEAN_MAX_CORES:-0-3}"
GEN_MODULES=( LTLAcc/HashExternal )
PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theorem3 PinStore )
# The audit infrastructure, named ONCE. These are not corpus — they are the
# instruments — but they are Lean modules in the audited tree, so the dead-file
# scan must know them by membership rather than by two hard-coded basename
# comparisons, and Phase 3b must inventory what they declare. CLASS 9: until
# 2026-07-31 nothing looked at the drivers' own declaration surface, so an
# `axiom` or a `theorem` added to either was invisible to every phase.
DRIVERS=( AxiomCheck Inventory )
# Certificates and their exact expected cones (observed via #print axioms,
# never guessed; any drift in EITHER direction is a failure).
@ -110,6 +117,24 @@ for f in "$HERE"/gen/LTLAcc/*.lean "$HERE"/Proofs/*.lean; do
fi
done
echo " all sources valid"
# ── Phase 0a: build hygiene ─────────────────────────────────────────────────
# P0-a was applied to the four ed25519 repositories on 2026-07-30 and never
# here — found on 2026-07-31 by the control repo's capability matrix, which
# asks the property rather than looking for a phase by name.
#
# The finding that made it matter there applies verbatim: a verification that
# never cleans up cannot distinguish "these proofs check" from "these proofs
# check GIVEN WHATEVER IS LYING AROUND". Compiled artifacts are gitignored, so
# no `git status` can show a reader that a verdict rested on an object from an
# earlier run of a different script. Purge, and compile from source.
#
# This repository has no --audit-only mode, so there is no case in which the
# artifacts must be kept: the purge is unconditional.
echo "=== Phase 0a: build hygiene ==="
find "$HERE" -name '*.olean' -delete 2>/dev/null || true
find "$HERE" -name '*.ilean' -delete 2>/dev/null || true
echo " purged every compiled artifact — this run compiles from source"
# Recursive: no compiled artifact anywhere in the tree may lack its source
# (review round 2, GPT M1 — previously scanned Proofs/*.olean only).
while IFS= read -r -d '' o; do
@ -140,6 +165,15 @@ HARNESS_EXTRA=(
lean-toolchain # which Lean the corpus claims to have been checked by
fidelity/lean_defs.py # the Python transcription the differential compares
fidelity/run_fidelity.py # the differential itself
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, the same shape as a forgeable .audit-basis.
PACTA-PIN.sha256 # WHICH pacta the differential is entitled to compare
# against. Pinned here because it is not executable
# and would otherwise sit outside the harness set —
# a subject pin an attacker may rewrite pins nothing,
# the same shape as a forgeable .audit-basis.
Proofs/Inventory.lean # audit driver: emits the inventory AND the statements
Proofs/AxiomCheck.lean # audit driver: the #print axioms queries of Phase 3
)
@ -202,8 +236,7 @@ lake env bash -c "
done
for f in Proofs/*.lean; do
b=\$(basename \"\$f\" .lean)
[ \"\$b\" = AxiomCheck ] && continue # audit infrastructure, compiled in Phase 3
[ \"\$b\" = Inventory ] && continue # audit infrastructure, compiled in Phase 3b
case \" ${DRIVERS[*]} \" in (*\" \$b \"*) continue;; esac # audit infrastructure, compiled in Phase 3/3b
case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f\"; exit 1;; esac
done
# gen/ gets the same unmanifested-source check (review round 2, GPT M1)
@ -211,6 +244,21 @@ lake env bash -c "
b=\"LTLAcc/\$(basename \"\$f\" .lean)\"
case \" ${GEN_MODULES[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE (gen): \$f\"; exit 1;; esac
done
# CLASS 15. The two loops above look only INSIDE Proofs/ and gen/LTLAcc/, so
# until 2026-07-31 a Lean file anywhere else was invisible: one at the
# verification root, or under gen/AnythingElse/, was neither compiled nor
# rejected. It could be imported by name from a manifested module — the
# manifest names modules, and LEAN_PATH includes both roots — which is a
# source of the corpus that no phase reads and no pin covers. Nothing may
# live in either root but the two enumerated sets.
shopt -s nullglob
for f in *.lean; do echo \"DEAD FILE (verification root): \$f\"; exit 1; done
for d in gen/*/; do
[ \"\$d\" = 'gen/LTLAcc/' ] && continue
for f in \"\$d\"*.lean; do echo \"DEAD FILE (gen subdirectory): \$f\"; exit 1; done
done
for f in gen/*.lean; do echo \"DEAD FILE (gen root): \$f\"; exit 1; done
shopt -u nullglob
"
if grep -q "uses 'sorry'" "$LOG"; then echo "STUB: sorry detected"; exit 1; fi
rm -f "$LOG"
@ -261,18 +309,246 @@ lake env bash -c "
" > "$INVLOG" 2>&1 || { cat "$INVLOG"; echo "INVENTORY COMPILE FAILED"; exit 1; }
"$HERE/inventory_gate.sh" "$INVLOG" "$HERE/inventory-allowlist.txt" || COVFAIL=1
# ── Phase 3b-kernel: kernel-side axiom-declaration gate ─────────────────────
# PORTED FROM THE ed25519 FORKS after round-7 review (Claude, finding F2).
#
# What this repository had: a SOURCE-TEXT axiom grep in Phase 1, and an
# environment walk in Phase 3b that runs inside Inventory.lean. Both have the
# same blind spot from opposite directions. The grep misses ` axiom c : ...`
# with a leading space — this repo's own selftest_audit.sh case 12 exploits
# exactly that. And the environment walk is an `#eval`: a declaration placed
# AFTER it in the same file exists in the compiled object file but not in the
# environment when the walk runs, so the button reported "no axiom, no claim"
# over a claim that was sitting in the environment, with the statement digest
# byte-identical. A reviewer demonstrated it.
#
# The fix is the one the forks already carry: ask the KERNEL, by reading every
# compiled object file directly. readModuleData sees what was actually stored,
# regardless of indentation, attributes, privacy, or where in the file a
# declaration sits relative to any #eval. Membership self-derives from the
# manifest, so a new module cannot escape by being unlisted, and the module
# count must match so a deleted .olean cannot make the scan vacuous.
# PLACEMENT. This deliberately runs INSIDE Phase 3b rather than beside the
# compile phase, unlike the ed25519 forks. There the audit drivers are members
# of the compile manifest, so they exist by the time the kernel gate runs. Here
# they are not: AxiomCheck is compiled by Phase 3 and Inventory by Phase 3b, so
# an earlier gate would fail on a missing artifact — which it did, correctly,
# when this was first ported. It must run after both drivers exist, because the
# instruments are exactly what it has to see.
echo "=== Phase 3b-kernel: kernel-side axiom-declaration gate ==="
KERNLOG=$(mktemp /tmp/acc-kernel-XXXX.log)
AXGATE=$(mktemp "$HERE/.axgate-XXXX.lean")
ALL_MODULES=$(printf '"%s.olean", ' "${PROOFS[@]}" "${DRIVERS[@]}" | sed 's/, $//')
cat > "$AXGATE" <<LEANGATE
import Lean
open Lean System
#eval show CoreM Unit from do
let dir : FilePath := "$HERE/Proofs"
let expected : List String := [$ALL_MODULES]
let mut errs : Array String := #[]
let mut nConst := 0
let mut nMod := 0
let mut seen : Std.HashSet (String × Name) := {}
for name in expected do
let p := dir / name
-- FAIL CLOSED ON ABSENCE: a missing artifact would make this scan vacuous
-- for that module, so it is an error and never a skip.
unless (← p.pathExists) do
throwError "MISSING ARTIFACT: {p} — the kernel gate would be vacuous for it"
let (mod, _) ← readModuleData p
nMod := nMod + 1
for ci in mod.constants do
nConst := nConst + 1
seen := seen.insert ("Proofs." ++ (name.dropRight 6), ci.name)
if ci matches .axiomInfo _ then
errs := errs.push s!" {name}: {ci.name}"
unless errs.isEmpty do
throwError "AXIOM DECLARED under Proofs/ (kernel-side gate):\n{String.intercalate "\n" errs.toList}"
logInfo s!" kernel confirms: {nConst} declarations across {nMod} compiled modules, none is an axiom"
for (m, n) in seen do IO.println s!"KERNEL-NAME|{m}|{n}"
LEANGATE
cd "$AENEAS_LEAN"
AXGATE_RC=0
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' '$AXGATE'
" 2>&1 | tee "$KERNLOG" || AXGATE_RC=${PIPESTATUS[0]}
cd "$HERE"
rm -f "$AXGATE" "${AXGATE%.lean}.olean"
if [ "$AXGATE_RC" -ne 0 ]; then
echo "AXIOM SMUGGLING GATE FAILED (kernel-side) — see the error above."
rm -f "$KERNLOG" "$INVLOG"; exit 1
fi
echo ""
# ── THE ACCOUNTING IDENTITY ─────────────────────────────────────────────────
# Ported from the ed25519 forks, and the reason it is here is a demonstrated
# attack, not symmetry. A reviewer appended to Proofs/Inventory.lean, AFTER the
# `#eval` that performs the driver walk:
#
# def bait : Nat := 0
# theorem bait.smuggled : ... := ...
#
# re-pinned, and ran the button. It printed "no axiom, no claim", the statement
# digest was byte-identical to the clean tree, and the run went green — while a
# theorem with a real axiom cone sat in the compiled environment. It was in
# neither walk: not corpus, because an instrument is not corpus; not driver
# surface, because it post-dates the emitter that reports the driver surface.
#
# The two walks read ENVIRONMENTS. Phase 2b reads OBJECT FILES. What a walk
# cannot see because of where it sits in a file, the object file still holds.
# So the property enforced here is containment, and it is what closes the hole:
#
# every constant the kernel sees ⊆ corpus inventory ∪ instrument surface
#
# Compared as SETS, deliberately. Counts cannot express this relation: an
# object file may hold two physical copies of one lazily-materialised equation
# lemma, while an environment holds one constant per name — arithmetic between
# those views misled the ed25519 version of this check twice before it was
# stated as containment.
KERN_NAMES=$(mktemp /tmp/acc-kernnames-XXXX.txt)
ACCT_NAMES=$(mktemp /tmp/acc-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 $2}' "$INVLOG"
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"
# THIS COMPARISON IS NOT AVAILABLE HERE, and saying so beats printing a number.
# The ed25519 repositories and fips205 use INV|module|name|kind|cone; THIS
# repository uses INV|name|kind|cone — four fields, no module column. The tag is
# the same and the record is not. Keying field 2 as a module here yields
# `name|kind`, which matches nothing, and the first run of this port duly
# reported 216 of 234 records as module-attribution differences. That number was
# meaningless. A wrong number in a green banner is the failure this estate keeps
# committing, so the check now tests its own applicability from the record shape
# rather than assuming it from the tag.
INV_FIELDS=$(LC_ALL=C grep -m1 '^INV|' "$HERE/inventory-allowlist.txt" | awk -F'|' '{print NF}')
if [ "${INV_FIELDS:-0}" -ge 5 ]; then
MULTIMOD=$(LC_ALL=C comm -23 "$KERN_PAIRS" "$ACCT_PAIRS" | wc -l)
MULTIMOD_NOTE="$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)"
else
MULTIMOD=0
MULTIMOD_NOTE="not computed — this repository's INV rows carry no module column ($INV_FIELDS fields), so kernel and walk records cannot be compared as module|name pairs. Adding that column is the open follow-up; until then the identity here is name-keyed only, which is weaker (round-9 review, Claude N2)."
fi
UNACCOUNTED=$(LC_ALL=C comm -23 "$KERN_NAMES" "$ACCT_NAMES")
if [ ! -s "$KERN_NAMES" ]; then
echo " ACCOUNTING FAILED: Phase 2b reported no constant names — the scan was vacuous"
COVFAIL=1
elif [ -n "$UNACCOUNTED" ]; then
echo " ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:"
printf '%s\n' "$UNACCOUNTED" | head -20 | sed 's/^/ /'
COVFAIL=1
else
echo " accounting: every one of $(wc -l < "$KERN_NAMES") kernel constant names is covered by the corpus inventory or the instrument surface"
echo " multi-module: $MULTIMOD_NOTE"
fi
rm -f "$KERN_NAMES" "$ACCT_NAMES" "$KERNLOG"
# The inventory's corpus-module list must BE the compile manifest — both
# directions, so neither can drift from the other silently.
# Read the module LISTS, not the file. This comparison used to grep the whole
# of Inventory.lean for a backticked name, which meant any PROSE mention of a
# module counted: a doc comment naming `Proofs.AxiomCheck` broke the count, and
# — worse in the other direction — a doc mention of a module missing from the
# array would have satisfied the presence check and hidden the omission. The
# manifest is the arrays; read the arrays.
MODLISTS=$(sed -n '/^def corpusModules/,/\]/p;/^def driverModules/,/\]/p' "$HERE/Proofs/Inventory.lean")
for m in "${GEN_MODULES[@]}" "${PROOFS[@]}"; do
mod=$(echo "$m" | sed 's|^LTLAcc/|LTLAcc.|; s|^\([A-Z]\)|Proofs.\1|; s|^Proofs\.LTLAcc\.|LTLAcc.|')
grep -qF "\`$mod" "$HERE/Proofs/Inventory.lean" || {
grep -qF "\`$mod" <<<"$MODLISTS" || {
echo " MANIFEST DRIFT: $mod compiled by check.sh but not inventoried"; COVFAIL=1; }
done
NMANIFEST=$(( ${#GEN_MODULES[@]} + ${#PROOFS[@]} ))
NINV=$(grep -oE '`(LTLAcc|Proofs)\.[A-Za-z0-9_.]+' "$HERE/Proofs/Inventory.lean" | wc -l)
# The drivers are named in Inventory.lean too, now that it walks their
# declaration surface — so they count on both sides of this equality.
for d in "${DRIVERS[@]}"; do
[ "$d" = Inventory ] && continue # covered as the current module, which has
# no module index while it elaborates and
# so is not named in its own module list
grep -qF "\`Proofs.$d" <<<"$MODLISTS" || {
echo " MANIFEST DRIFT: driver Proofs.$d is not inventoried"; COVFAIL=1; }
done
NMANIFEST=$(( ${#GEN_MODULES[@]} + ${#PROOFS[@]} + ${#DRIVERS[@]} - 1 ))
NINV=$(grep -oE '`(LTLAcc|Proofs)\.[A-Za-z0-9_.]+' <<<"$MODLISTS" | wc -l)
[ "$NMANIFEST" = "$NINV" ] || {
echo " MANIFEST DRIFT: check.sh compiles $NMANIFEST modules, Inventory lists $NINV"; COVFAIL=1; }
# CLASS 9. The driver-surface block must actually have RUN. Its violations are
# raised inside Lean, so a walk that silently did not execute would look exactly
# like a clean one — the same vacuous-pass shape the INV-COUNT trailer exists to
# close. Require the trailer, and require it to agree with the lines.
NDRV=$(grep -c '^DRV|' "$INVLOG" || true)
DRVTRAILER=$(grep '^DRV-COUNT|' "$INVLOG" | tail -1 | cut -d'|' -f2)
if [ -z "$DRVTRAILER" ] || [ "$DRVTRAILER" != "$NDRV" ]; then
echo " DRIVER SURFACE NOT OBSERVED: trailer=${DRVTRAILER:-absent}, observed $NDRV lines"
COVFAIL=1
elif [ "$NDRV" -eq 0 ]; then
echo " DRIVER SURFACE NOT OBSERVED: the instruments declare nothing at all,"
echo " which cannot be true — Inventory.lean declares its own machinery."
COVFAIL=1
else
echo " driver surface: $NDRV declarations across the audit instruments, no axiom, no claim"
fi
# AND THE ROWS ARE PINNED, WITH THEIR CONES, BY THE SAME GATE THE CORPUS USES.
#
# This block used to end with a note explaining why the instruments' internals
# were deliberately NOT pinned: they are byte-pinned in HARNESS.sha256, so "a
# second policy file listing their internals would add a thing to maintain
# without adding a thing to catch."
#
# Round-8 review (Claude, register keys `drv-surface-no-cones`,
# `accounting-certifies-enumeration`) showed that reasoning was wrong, by
# demonstration. Their payload
# DRV|LTLAccAudit.bait.smuggled|theorem
# is a genuine claim with cone [propext, Classical.choice, Quot.sound]. It
# passed the name-prefix rule above — `bait` is declared alongside it, so it
# looks like an elaborator artefact — it was enumerated by the accounting
# identity, and then NOTHING examined it: the rows carried no cone, no
# allowlist covered them, and the statement digest does not reach instruments.
# Byte-pinning shows that a driver CHANGED. It does not show what appeared in
# it or what that thing rests on, and "the file changed" is not a finding a
# reader can act on.
#
# So the rows now carry their cone and are diffed against a committed
# allowlist, in both directions, by inventory_gate.sh with the DRV tag — the
# same implementation, so the two surfaces cannot drift apart in their gating.
# The axiom policy differs by surface and is enforced per surface: the corpus
# admits exactly the sanctioned hash boundary, the instruments admit none.
"$HERE/inventory_gate.sh" "$INVLOG" "$HERE/driver-allowlist.txt" DRV || COVFAIL=1
# CONES ⊆ allowlist with IDENTICAL cones: the #print-axioms-pinned table
# and the environment inventory are two independent computations of the
# same facts — any disagreement is a failure of one of them.
@ -402,18 +678,61 @@ FIDELITY_RAN=0
if [ "${SKIP_FIDELITY:-0}" = "1" ]; then
echo " skipped (SKIP_FIDELITY=1)"
elif [ -d "$PACTA_SRC/pacta" ]; then
# PIN THE SUBJECT BEFORE COMPARING AGAINST IT (round-8 review, GPT-5.6,
# register key `pacta-subject-unpinned`). This phase used to import whatever
# sat at $PACTA_SRC: no repository, no commit, no clean state, no hashes. It
# pinned the fidelity OUTPUTS while leaving the SUBJECT anonymous, so any
# program producing the same finite family of answers passed and the recorded
# result named no version of the thing it agreed with. Agreement with an
# unnamed program is not evidence about a deployed one.
PACTA_SRC="$PACTA_SRC" python3 "$HERE/fidelity/pacta_pin.py" --verify \
|| { echo "FIDELITY FAILED — the pacta subject is not the pinned one."; exit 1; }
PACTA_SRC="$PACTA_SRC" python3 "$HERE/fidelity/run_fidelity.py" || { echo "FIDELITY FAILED"; exit 1; }
FIDELITY_RAN=1
else
echo " SKIPPED: pacta repo not found at $PACTA_SRC (set PACTA_SRC to run)"
fi
# Fail-closed markers (review H2): the Lean corpus is green either way, but
# only the strong marker — required by the attestation gate — is emitted
# when fidelity actually ran. Never conflate the two.
# Fail-closed markers AND A FAIL-CLOSED EXIT CODE (round-7 review: raised
# independently by both reviewers — Claude F1, GPT-5.6 F10; register key
# `acc-exit0-fidelity`).
#
# Until now this emitted the weak marker and RETURNED 0. The marker discipline
# was right and the exit code contradicted it: a caller doing the obvious thing
#
# ./check.sh && append
#
# read success from a run whose own last line says NOT attestation-ready. And
# because pacta is not part of this estate, the skip branch is the ONLY branch
# any third party ever takes — so for everyone but the author, the button
# always returned 0 without ever checking definition fidelity. A procedure of
# the form "run the button, then append" was unsound for this component.
#
# An exit code is what programs read. If the button cannot establish
# attestation-readiness it must not return success, whatever it prints.
#
# fidelity ran -> ATTESTATION GREEN, exit 0
# SKIP_FIDELITY=1 -> exit 3: the caller opted out EXPLICITLY, so the
# code is distinguishable, but it is not 0
# pacta absent -> exit 1: nobody opted out; this is a real failure
# to establish the property the button exists for
#
# The self-tests are unaffected: every SKIP_FIDELITY=1 case already expects a
# non-zero exit and asserts on a diagnostic from an earlier phase, and the
# control case compiles modules directly rather than invoking this script.
echo "=== LEAN GREEN ==="
if [ "$FIDELITY_RAN" = 1 ]; then
echo "=== ATTESTATION GREEN (Lean + fidelity) ==="
elif [ "${SKIP_FIDELITY:-0}" = "1" ]; then
echo "=== FIDELITY SKIPPED ON REQUEST — NOT attestation-ready (exit 3) ==="
echo " The Lean corpus is green. Definition fidelity against the deployed"
echo " verifier was not checked, so this run does NOT certify that this"
echo " repository may be attested."
exit 3
else
echo "=== FIDELITY NOT RUN — NOT attestation-ready (run with pacta present) ==="
echo "=== FIDELITY NOT RUN — NOT attestation-ready (exit 1) ==="
echo " pacta was not found at: $PACTA_SRC"
echo " Set PACTA_SRC to a pacta checkout and re-run, or pass"
echo " SKIP_FIDELITY=1 to acknowledge deliberately skipping it (exit 3)."
exit 1
fi

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

@ -0,0 +1,32 @@
# 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|LTLAccAudit.axiomCone._proof_11|theorem|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|LTLAccAudit.axiomCone._proof_1|theorem|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|LTLAccAudit.axiomCone._sparseCasesOn_1|def|propext
DRV|Proofs.Inventory|LTLAccAudit.axiomCone._sparseCasesOn_4|def|propext
DRV|Proofs.Inventory|LTLAccAudit.axiomCone.match_1|def|propext
DRV|Proofs.Inventory|LTLAccAudit.axiomCone.match_4|def|propext
DRV|Proofs.Inventory|LTLAccAudit.axiomCone.match_7|def|propext
DRV|Proofs.Inventory|LTLAccAudit.axiomCone.match_9|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|LTLAccAudit.axiomCone|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|LTLAccAudit.corpusModules|def|
DRV|Proofs.Inventory|LTLAccAudit.driverModules|def|
DRV|Proofs.Inventory|LTLAccAudit.kindOf.match_1|def|
DRV|Proofs.Inventory|LTLAccAudit.kindOf|def|
DRV|Proofs.Inventory|LTLAccAudit.normWs|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|LTLAccAudit.ppAll|def|Classical.choice,Quot.sound,propext
DRV|Proofs.Inventory|LTLAccAudit.valueOf._sparseCasesOn_1|def|propext
DRV|Proofs.Inventory|LTLAccAudit.valueOf.match_1|def|propext
DRV|Proofs.Inventory|LTLAccAudit.valueOf|def|propext

159
verification/fidelity/pacta_pin.py Executable file
View file

@ -0,0 +1,159 @@
#!/usr/bin/env python3
"""Pin the pacta sources the fidelity harness actually consumes.
pacta_pin.py --write # regenerate PACTA-PIN.sha256 (deliberate act)
pacta_pin.py --verify # check the subject; exit 1 on any drift
─────────────────────────────────────────────────────────────────────────────
WHY THIS EXISTS — round-8 review (GPT-5.6, register key `pacta-subject-unpinned`)
Phase 4 compares this repository's Lean definitions against the DEPLOYED
verifier. It did so by putting `$PACTA_SRC` on `sys.path` and importing
`pacta.transparency` — whatever happened to be there. No repository URL, no
commit, no clean-state check, no source hashes.
So the fidelity counts pinned OUTPUTS while the SUBJECT was unpinned. Any
implementation producing the same finite family of answers passed, and the
recorded result named no version of the thing it agreed with. The reviewer's
zero-divergence run was specifically against pacta `cd3b1bc…` — because the
reviewer selected and recorded that checkout, not because the button required
it.
A proof about a model is not evidence about an unnamed program.
WHAT IS PINNED, AND WHY IT IS NOT A GLOB. The pin covers the transitive set of
pacta modules the harness ACTUALLY LOADS, discovered by importing the harness's
entry point and reading `sys.modules` — a membership property, not a directory
listing. Globbing `pacta/*.py` would pin files the comparison never touches
(noise that breaks the pin for unrelated edits) and would miss anything loaded
from outside that directory. The estate has been bitten by name-shaped
measurement before; this is the same error class.
WHAT THIS DOES NOT ESTABLISH. Byte identity of a source tree is not proof that
the deployed service runs it, and finite-family agreement is not extensional
equality. This pin names the subject; it does not widen the claim.
─────────────────────────────────────────────────────────────────────────────
"""
import hashlib
import os
import subprocess
import sys
HERE = os.path.dirname(os.path.abspath(__file__))
VERIF = os.path.dirname(HERE)
PIN = os.path.join(VERIF, 'PACTA-PIN.sha256')
PACTA_SRC = os.environ.get(
'PACTA_SRC', os.path.join(VERIF, '..', '..',
'proof-aware-crypto-tooling-agent', 'src'))
PACTA_SRC = os.path.abspath(PACTA_SRC)
def loaded_sources():
"""{path relative to PACTA_SRC: sha256} for every pacta module imported.
Imports the same entry point the fidelity harness does, then keeps the
modules whose file lives under PACTA_SRC. That is the consumed set by
construction: if the harness stops using a module, it leaves the pin; if it
starts using one, the pin fails until someone regenerates it deliberately.
"""
sys.path.insert(0, PACTA_SRC)
try:
import pacta.transparency # noqa: F401
except Exception as e: # pragma: no cover
print(f'PACTA PIN: cannot import pacta.transparency from {PACTA_SRC}:'
f' {e}', file=sys.stderr)
raise SystemExit(1)
out = {}
for mod in list(sys.modules.values()):
f = getattr(mod, '__file__', None)
if not f:
continue
f = os.path.abspath(f)
if not f.startswith(PACTA_SRC + os.sep) or not f.endswith('.py'):
continue
with open(f, 'rb') as fh:
out[os.path.relpath(f, PACTA_SRC)] = hashlib.sha256(
fh.read()).hexdigest()
return out
def head_commit():
"""The pacta commit, for the record. NOT the enforcement — hashes are."""
try:
r = subprocess.run(['git', '-C', PACTA_SRC, 'rev-parse', 'HEAD'],
capture_output=True, text=True, timeout=10)
c = r.stdout.strip() if r.returncode == 0 else 'unknown'
d = subprocess.run(['git', '-C', PACTA_SRC, 'status', '--porcelain'],
capture_output=True, text=True, timeout=10)
dirty = bool(d.stdout.strip()) if d.returncode == 0 else True
return c, dirty
except Exception: # pragma: no cover
return 'unknown', True
def write():
got = loaded_sources()
commit, dirty = head_commit()
if dirty:
print('PACTA PIN: refusing to pin a DIRTY pacta working tree.'
' Commit or stash first — a pin taken over uncommitted edits'
' names a subject nobody else can obtain.', file=sys.stderr)
raise SystemExit(1)
with open(PIN, 'w', encoding='utf-8') as fh:
fh.write(f'# pacta subject pinned by fidelity/pacta_pin.py --write\n')
fh.write(f'# commit {commit}\n')
fh.write(f'# {len(got)} module(s), discovered by import, not by glob\n')
for rel in sorted(got):
fh.write(f'{got[rel]} {rel}\n')
print(f'PACTA PIN: wrote {len(got)} module(s) at commit {commit[:7]}')
def verify():
if not os.path.exists(PIN):
print('PACTA PIN: PACTA-PIN.sha256 is missing — the fidelity subject'
' is unpinned. Refusing to certify agreement with an unnamed'
' program.', file=sys.stderr)
return 1
want = {}
commit = 'unknown'
for line in open(PIN, encoding='utf-8'):
if line.startswith('# commit '):
commit = line.split()[2]
if line.startswith('#') or not line.strip():
continue
h, rel = line.rstrip('\n').split(' ', 1)
want[rel] = h
got = loaded_sources()
bad = []
for rel in sorted(set(want) | set(got)):
if rel not in got:
bad.append(f' {rel}: pinned but NOT LOADED by the harness')
elif rel not in want:
bad.append(f' {rel}: loaded by the harness but NOT PINNED')
elif want[rel] != got[rel]:
bad.append(f' {rel}: bytes differ from the pin')
if bad:
print('PACTA SUBJECT MISMATCH — the fidelity comparison would be'
' against a different program than the one pinned:',
file=sys.stderr)
print('\n'.join(bad), file=sys.stderr)
print(f' pinned commit: {commit}', file=sys.stderr)
print(' Re-pin deliberately with fidelity/pacta_pin.py --write'
' if the new subject is the intended one.', file=sys.stderr)
return 1
_, dirty = head_commit()
state = ' (WORKING TREE DIRTY)' if dirty else ''
print(f' pacta subject: {len(got)} module(s) match the pin,'
f' commit {commit[:7]}{state}')
return 1 if dirty else 0
if __name__ == '__main__':
if '--write' in sys.argv:
write()
elif '--verify' in sys.argv:
raise SystemExit(verify())
else:
raise SystemExit(__doc__)

87
verification/inventory_gate.sh
View file

@ -5,7 +5,35 @@
# calls it, and selftest_audit.sh exercises this exact script against
# injected evader declarations — the tested logic IS the shipping 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:
# UNCLASSIFIED — constant in the environment, absent from the allowlist
@ -17,17 +45,34 @@
# ─────────────────────────────────────────────────────────────────────────────
set -uo pipefail
export LC_ALL=C # byte-order collation: sort/comm must agree with Lean's String order
obs_file="$1"; allow_file="$2"
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)
N_OBS=$(printf '%s' "$OBS" | grep -c '^INV|' || true)
TRAILER=$(grep '^INV-COUNT|' "$obs_file" | tail -1 | cut -d'|' -f2)
if [ -z "$TRAILER" ] || [ "$TRAILER" != "$N_OBS" ]; then
# The trailer is an OUTPUT-INTEGRITY check: it must equal the number of rows
# the driver(s) actually emitted, BEFORE de-duplication. Comparing it to the
# de-duplicated count conflates "a run was truncated" with "two rows were
# identical", and the second is a record-format defect that must be fixed at
# the source, not absorbed here. (It was: DRV rows now carry their driver.)
N_RAW=$(grep -c "^$TAG|" "$obs_file" || true)
OBS=$(grep "^$TAG|" "$obs_file" | sort -u)
N_OBS=$(printf '%s' "$OBS" | grep -c "^$TAG|" || true)
if [ "$N_RAW" -ne "$N_OBS" ]; then
echo " DUPLICATE $TAG RECORDS: $N_RAW rows collapse to $N_OBS distinct ones."
echo " Two declarations share a record, so one is covered by the other's entry:"
grep "^$TAG|" "$obs_file" | sort | uniq -d | head -5 | sed 's/^/ /'
exit 1
fi
TRAILER=$(grep "^$TRAILER_TAG|" "$obs_file" | tail -1 | cut -d'|' -f2)
if [ -z "$TRAILER" ] || [ "$TRAILER" != "$N_RAW" ]; then
echo " INVENTORY TRUNCATED: trailer=${TRAILER:-absent}, observed $N_OBS lines"
exit 1
fi
ALLOW=$(grep '^INV|' "$allow_file" | sort -u)
ALLOW=$(grep "^$TAG|" "$allow_file" | sort -u)
FAILGATE=0
UNCLASS=$(comm -23 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
STALE=$(comm -13 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW"))
@ -40,13 +85,29 @@ if [ -n "$STALE" ]; then
FAILGATE=1
fi
# The corpus admits exactly one axiom, and it is the sanctioned boundary.
# THE AXIOM POLICY IS PER-SURFACE, and conflating the two would be a silent
# inversion. The CORPUS admits exactly one axiom — the sanctioned hash boundary.
# The INSTRUMENTS admit NONE: an audit tool that declares an axiom widens the
# trusted base from inside the thing doing the auditing. Reusing the corpus rule
# for DRV would have demanded LTLAcc.sha256 appear among instrument
# declarations, where it never does, and the gate would have failed for a reason
# that has nothing to do with the property.
AXLINES=$(printf '%s\n' "$OBS" | grep '|axiom|' || true)
if [ "$AXLINES" != "INV|LTLAcc.sha256|axiom|LTLAcc.sha256" ]; then
echo " AXIOM SURFACE DRIFT: expected exactly LTLAcc.sha256, observed:"
printf '%s\n' "${AXLINES:- (none)}" | sed 's/^/ /'
FAILGATE=1
if [ "$TAG" = DRV ]; then
if [ -n "$AXLINES" ]; then
echo " AXIOM SURFACE DRIFT: $WHAT must declare no axioms; observed:"
printf '%s\n' "$AXLINES" | sed 's/^/ /'
FAILGATE=1
fi
AXNOTE="zero axioms declared by the instruments"
else
if [ "$AXLINES" != "INV|LTLAcc.sha256|axiom|LTLAcc.sha256" ]; then
echo " AXIOM SURFACE DRIFT: expected exactly LTLAcc.sha256, observed:"
printf '%s\n' "${AXLINES:- (none)}" | sed 's/^/ /'
FAILGATE=1
fi
AXNOTE="single sanctioned axiom"
fi
[ "$FAILGATE" = 0 ] && echo " inventory gate: $N_OBS constants, environment == allowlist, single sanctioned axiom"
[ "$FAILGATE" = 0 ] && echo " $LABEL: $N_OBS constants, environment == allowlist, $AXNOTE"
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

19
verification/selftest-harness.sh
View file

@ -38,18 +38,29 @@ cp "$HERE/HARNESS.sha256" "$STASH/HARNESS.sha256"
# Lift Phase 0c. The two repo families end the phase differently, so accept
# either terminator rather than hardcoding one and silently lifting nothing.
# The payload is written to its OWN file before the driver is assembled, for two
# reasons that both bit this repository. The size sanity check below has to
# measure what was LIFTED; measured on the concatenated driver it counts the
# prepended bindings too, so a lift that recovered almost nothing still clears
# the threshold (round-7 lift-guard-payload-assert, closed in the four forks
# with "all six lift sites" — six counted the forks, and these two accumulator
# lifts were never in that count). And lift-guard needs payload and driver
# separately to tell what the phase READS from what the driver DEFINES.
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\""
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'
cat "$PAYLOAD"
} > "$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 "This self-test must attack the shipping gate; refusing to run against nothing."
exit 1
fi
"$HERE/lift-guard.sh" "$PAYLOAD" "$DRIVER" "check.sh Phase 0c" || exit 1
expect() { # expect <label> <want-rc> <want-substring>
local label="$1" want_rc="$2" want_txt="$3" out rc

151
verification/selftest_audit.sh
View file

@ -39,6 +39,16 @@ trap 'echo "(scratch tree kept for inspection: $WORK)"' ERR
echo "=== audit-gate self-test (scratch: $WORK) ==="
cp -a "$SRC" "$WORK/verification"
T="$WORK/verification"
# The button also reads two documents from the REPOSITORY root, one level above
# verification/. Copying only verification/ left them missing, so check.sh in
# the scratch tree always died in Phase 3c with DOC DRIFT — which meant every
# `if check.sh; then <this attack was not caught>` guard below was unfirable:
# check.sh could not pass in here even with no attack at all, so those guards
# asserted nothing. Only the diagnostic greps were doing any work. Copy the
# documents so a genuinely-undetected attack would now show up as a PASS.
for d in README.md STATEMENT-MAP.md; do
[ -f "$SRC/../$d" ] && cp "$SRC/../$d" "$WORK/$d"
done
cp "$T/Proofs/PinStore.lean" "$T/PinStore.pristine"
# Recompile the injected leaf module + the inventory, then run the gate.
@ -148,6 +158,145 @@ grep -q "DEAD FILE (gen): gen/LTLAcc/Rogue.lean" "$T/check9b.out" || {
echo " ✗ case 9b: check.sh failed without DEAD FILE (gen) diagnosis"; tail -5 "$T/check9b.out"; exit 1; }
echo " ✓ case 9b pinned but unmanifested: check.sh dies with DEAD FILE (gen)"
# Case 9 was the last case when it was written, so it left its rogue file and
# its pin in place — harmless then, but the cases below inherit the tree. Undo
# it here rather than in case 9, so that case keeps testing exactly what it
# tested before.
rm -f "$T/gen/LTLAcc/Rogue.lean"
( cd "$T" && grep -v ' gen/LTLAcc/Rogue.lean$' HARNESS.sha256 > .h && mv .h HARNESS.sha256 )
# ── CLASS 15: a Lean file where no phase was looking ────────────────────────
# Until 2026-07-31 the dead-file scan read Proofs/*.lean and gen/LTLAcc/*.lean
# and nothing else. A module at the verification root, or under any other gen/
# subdirectory, was neither compiled nor rejected — while being importable by
# name, since LEAN_PATH contains both roots. A source of the corpus that no
# phase reads and no pin covers is precisely what the dead-file gate exists to
# forbid; it was simply looking in two places instead of everywhere.
# 10 — a stray module at the verification root. NOTE: Phase 0c does not stand
# in front of this one. Its required-pin set is executables plus
# gen/**.lean, so a root .lean is invisible to it; the Phase 2 check added
# for this class is the only gate here.
printf '/- rogue -/\ntheorem rogue_root : 1 = 1 := rfl\n' > "$T/Rogue.lean"
if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check10.out" 2>&1; then
echo " ✗ case 10: check.sh PASSED with a stray Rogue.lean at the verification root"; exit 1
fi
grep -q "DEAD FILE (verification root): Rogue.lean" "$T/check10.out" || {
echo " ✗ case 10: check.sh failed without the root diagnosis"; tail -5 "$T/check10.out"; exit 1; }
echo " ✓ case 10 stray module at the verification root: DEAD FILE (verification root)"
rm -f "$T/Rogue.lean"
# 11 — a module in a gen/ subdirectory that is not LTLAcc/. Two gates again,
# and both are exercised for the same reason as case 9.
mkdir -p "$T/gen/Rogue"
printf '/- rogue -/\ntheorem rogue_sub : 1 = 1 := rfl\n' > "$T/gen/Rogue/Extra.lean"
if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check11a.out" 2>&1; then
echo " ✗ case 11a: check.sh PASSED with an unpinned gen/Rogue/Extra.lean"; exit 1
fi
grep -q "does not match HARNESS.sha256" "$T/check11a.out" || {
echo " ✗ case 11a: check.sh failed without the harness-set diagnosis"; tail -5 "$T/check11a.out"; exit 1; }
echo " ✓ case 11a unpinned module in a foreign gen subdirectory: harness-set mismatch"
( cd "$T" && sha256sum gen/Rogue/Extra.lean >> HARNESS.sha256 )
if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check11b.out" 2>&1; then
echo " ✗ case 11b: check.sh PASSED with a pinned gen/Rogue/Extra.lean"; exit 1
fi
grep -q "DEAD FILE (gen subdirectory): gen/Rogue/Extra.lean" "$T/check11b.out" || {
echo " ✗ case 11b: check.sh failed without the subdirectory diagnosis"; tail -5 "$T/check11b.out"; exit 1; }
echo " ✓ case 11b pinned but in a foreign gen subdirectory: DEAD FILE (gen subdirectory)"
rm -rf "$T/gen/Rogue"
( cd "$T" && grep -v ' gen/Rogue/Extra.lean$' HARNESS.sha256 > .h && mv .h HARNESS.sha256 )
# ── CLASS 9: the instruments' own declaration surface ───────────────────────
# The audit drivers are not corpus, so nothing inventoried what THEY declare.
# Both are byte-pinned, so each attack must re-pin to reach the new gate —
# which is the point: byte-pinning stops drift, it does not stop an author.
# What follows is what byte-pinning cannot give.
# 12 — an axiom in the inventory driver itself, INDENTED. Phase 1 greps
# Proofs/*.lean for `^axiom `, so an unindented one is caught there and
# never reaches the new gate. Indentation is the documented evasion of
# that regex — measured on Lean v4.30.0-rc2 — so this case is the one
# that actually exercises the kernel-side driver walk rather than the
# source scan standing in front of it.
sed -i 's|^#eval show MetaM Unit| axiom driver_cheat : False\n\n#eval show MetaM Unit|' \
"$T/Proofs/Inventory.lean"
grep -q '^ axiom driver_cheat' "$T/Proofs/Inventory.lean" || {
echo " ✗ case 12: could not inject the indented axiom (case would be vacuous)"; exit 1; }
( cd "$T" && grep -v ' Proofs/Inventory.lean$' HARNESS.sha256 > .h \
&& sha256sum Proofs/Inventory.lean >> .h && mv .h HARNESS.sha256 )
if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check12.out" 2>&1; then
echo " ✗ case 12: check.sh PASSED with an axiom declared in Proofs/Inventory.lean"; exit 1
fi
grep -q "DRIVER SURFACE VIOLATION" "$T/check12.out" || {
echo " ✗ case 12: check.sh failed without the driver-surface diagnosis"; tail -5 "$T/check12.out"; exit 1; }
echo " ✓ case 12 indented axiom in the inventory driver: DRIVER SURFACE VIOLATION"
cp "$SRC/Proofs/Inventory.lean" "$T/Proofs/Inventory.lean"
( cd "$T" && grep -v ' Proofs/Inventory.lean$' HARNESS.sha256 > .h \
&& sha256sum Proofs/Inventory.lean >> .h && mv .h HARNESS.sha256 )
# 13 — a standalone claim in the OTHER driver. A theorem there is not a
# compiler artefact of any definition, which is exactly the distinction
# the gate draws: it must admit `axiomCone._proof_1` and reject this.
printf '\ntheorem driver_claim : 1 = 1 := rfl\n' >> "$T/Proofs/AxiomCheck.lean"
( cd "$T" && grep -v ' Proofs/AxiomCheck.lean$' HARNESS.sha256 > .h && sha256sum Proofs/AxiomCheck.lean >> .h && mv .h HARNESS.sha256 )
if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check13.out" 2>&1; then
echo " ✗ case 13: check.sh PASSED with a standalone theorem in Proofs/AxiomCheck.lean"; exit 1
fi
grep -q "DRIVER SURFACE VIOLATION" "$T/check13.out" || {
echo " ✗ case 13: check.sh failed without the driver-surface diagnosis"; tail -5 "$T/check13.out"; exit 1; }
echo " ✓ case 13 standalone claim in the axiom-check driver: DRIVER SURFACE VIOLATION"
cp "$SRC/Proofs/AxiomCheck.lean" "$T/Proofs/AxiomCheck.lean"
# Case 13 restores Proofs/AxiomCheck.lean but not its PIN, which it rewrote to
# match the tampered file. Harmless while 13 was last; case 14 runs check.sh and
# would die in Phase 0c on that stale pin. Re-pin here rather than in case 13,
# so that case keeps testing exactly what it tested before. (Second instance of
# this residue pattern in this file — see the note above case 10.)
( cd "$T" && grep -v ' Proofs/AxiomCheck.lean$' HARNESS.sha256 > .h \
&& sha256sum Proofs/AxiomCheck.lean >> .h && sort -k2 -o .h .h && mv .h HARNESS.sha256 )
# 14 — A DECLARATION THAT POST-DATES THE WALK THAT REPORTS IT.
# Round-7 review (Claude, finding F2), reproduced verbatim. The driver
# surface is reported by an `#eval` inside Proofs/Inventory.lean.
# Anything declared AFTER that command exists in the compiled object file
# but not in the environment while the command runs, so the walk cannot
# see it. Before Phase 3b-kernel existed this went GREEN: the button
# printed "no axiom, no claim", the statement digest was byte-identical
# to the clean tree, and a theorem with a real axiom cone sat in the
# environment — in neither walk, in no allowlist, pinned by nothing.
#
# The kernel reads OBJECT FILES, so it sees what an environment walk
# placed mid-file cannot. That is the whole point of the containment
# check, and this case is the reason it exists.
# NOTE ON THE PAYLOAD. `theorem bait.smuggled : True := trivial` does NOT
# work here, and the reason is worth keeping: Phase 1's stub audit greps
# for `: True :=` and catches it first. That is real defence in depth, but
# it means the naive payload never reaches the gate under test. The one
# below is the reviewer's original — a genuine claim with a real cone,
# invisible to every source-text check — so this case exercises the
# accounting identity and nothing else.
cat >> "$T/Proofs/Inventory.lean" <<'BAIT'
def bait : Nat := 0
theorem bait.smuggled : ∀ n : Nat, n + 0 = n := by
have _h := Classical.em True
intro n; simp
BAIT
( cd "$T" && grep -v ' Proofs/Inventory.lean$' HARNESS.sha256 > .h \
&& sha256sum Proofs/Inventory.lean >> .h && sort -k2 -o .h .h && mv .h HARNESS.sha256 )
if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check14.out" 2>&1; then
echo " ✗ case 14: check.sh PASSED with a declaration appended after the driver walk"; exit 1
fi
grep -q "ACCOUNTING FAILED" "$T/check14.out" \
&& grep -q "bait" "$T/check14.out" || {
echo " ✗ case 14: failed, but not with the accounting diagnosis naming the declaration"
tail -8 "$T/check14.out"; exit 1; }
echo " ✓ case 14 declaration after the driver walk: ACCOUNTING FAILED names it"
cp "$SRC/Proofs/Inventory.lean" "$T/Proofs/Inventory.lean"
( cd "$T" && grep -v ' Proofs/Inventory.lean$' HARNESS.sha256 > .h \
&& sha256sum Proofs/Inventory.lean >> .h && sort -k2 -o .h .h && mv .h HARNESS.sha256 )
rm -rf "$WORK"
trap - ERR
echo "=== SELF-TEST GREEN: 10 attack cases defeated + positive control ==="
echo "=== SELF-TEST GREEN: 15 attack cases defeated + positive control ==="

14
verification/selftest_statements.sh
View file

@ -46,18 +46,26 @@ cp "$T/AUDIT-MANIFEST.txt" "$T/MANIFEST.pristine"
# Phase 3d, lifted verbatim from the shipping button. HERE and INVLOG are the
# two variables it reads from its surroundings.
# Payload to its own file before the driver is assembled: the size check must
# measure what was LIFTED, not the lift plus its bindings, and lift-guard needs
# the two apart to separate what the phase READS from what the driver DEFINES.
DRIVER="$T/phase3d.sh"
PAYLOAD="$T/payload3d.sh"
sed -n '/^# -- Phase 3d/,/^# -- Phase 4/p' "$SRC/check.sh" | sed '$d' > "$PAYLOAD"
{
echo 'set -uo pipefail'
echo 'set -euo pipefail' # -e matches the button; see lift-drivers-drop-errexit
echo "HERE=\"$T\""
echo 'INVLOG="$1"'
sed -n '/^# -- Phase 3d/,/^# -- Phase 4/p' "$SRC/check.sh" | sed '$d'
cat "$PAYLOAD"
} > "$DRIVER"
if [ "$(wc -l < "$DRIVER")" -lt 40 ]; then
if [ "$(wc -l < "$PAYLOAD")" -lt 40 ]; then
echo "FATAL: could not lift Phase 3d out of check.sh — the phase markers moved."
echo "This self-test must attack the shipping gate; refusing to run against nothing."
exit 1
fi
# Guarded by the SHIPPING guard in $SRC, not the copy inside the scratch tree:
# a test that vets itself with its own copy of the instrument proves less.
"$SRC/lift-guard.sh" "$PAYLOAD" "$DRIVER" "check.sh Phase 3d" || exit 1
# Recompile the edited leaf module + the inventory into $T/inv.out.
build_inventory() {