verification: pin the harness, the audit drivers and the policy files (P1-c)
Every gate this repository has was executed by scripts that nothing pinned.
Round-5 review of the companion SLH-DSA repository stubbed the compiler
wrapper alone and its button printed ALL GREEN in 3.6 seconds over
deliberately destroyed proofs; flipping two guards in the audit driver
disabled every check with the digest byte-identical. Depth of checking is
worth nothing if the thing doing the checking is unbound — and every gate
added this week made that gap more valuable to an attacker, not less.
Phase 0c requires every harness file to match HARNESS.sha256. Two design
points carry the weight:
- WHICH files must be pinned is POLICY and lives in check.sh, never in the
map being consulted. If the required set were read from the pin file,
deleting an entry would silently un-pin that file. It is instead derived
from the filesystem, so a deleted entry is a set mismatch and a build
failure. That is the exact defect SLH-DSA round-6 found, closed here by
construction.
- Membership self-derives from the executable bit: anything this script can
shell out to must be pinned, so a NEW script fails closed until someone
pins it deliberately. Load-bearing files that are not executable — the
audit driver, the committed manifests, the policy tables — cannot be
discovered that way and are listed explicitly.
lean-guard is inside the set, which finally makes the standing "lean-guard
stays hash-pinned" rule a property of the repository rather than a convention.
selftest-harness.sh replays five cases, each asserting a specific diagnostic:
an edited lean-guard, a new unpinned executable, a deleted pin entry, a
missing pin file, and a positive control. It was itself negative-tested — with
the hash comparison removed it goes red on exactly that case while cheerfully
reporting "10 harness files match their pins".
TRUSTED-BASE.md states the limit at equal length to the claim: pinning a
harness from inside that harness is circular, and an author who edits a script
and refreshes its pin in the same commit passes every phase. What the pin
changes is that the edit can no longer be SILENT — it must appear in the diff
at the commit being reviewed. A green button says "this is the apparatus that
was reviewed", never "this apparatus is trustworthy".
Also fixed, found by this sweep: both self-tests compared the working tree
against its starting state with `diff <(echo "$VAR") <(command)`, which is
asymmetric — for a clean tree the variable is empty and `echo` emits a blank
line the command does not. It reported a difference precisely when nothing was
wrong, and only surfaced once P1-a was committed and Proofs/ became clean.
Both now compare as strings.
Verified green: 20 runs across the four ed25519 repositories (four buttons,
four harness self-tests, four axiom-gate self-tests, four binding self-tests,
four scalar buttons), zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 18:13:01 +00:00
|
|
|
6c821b8e465d3b394cb3cbb4bb3757791ace064b6d1b273ba9a41402dac74e24 AUDIT-MANIFEST.txt
|
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 10:15:26 +00:00
|
|
|
6fd6275ba35ceb1c6ff38239a8377c0c1cb54dd5ecff83e77edc18f690b9bab4 check-scalar.sh
|
|
|
|
|
fb92e967d81982ede31c0deeb5c02bacaf3380ee94d2c9af3dd2634e3d73c6ad check.sh
|
|
|
|
|
e782d1c9eef71e97f3c8b97463c16abc6321cc7192dd08a877d8c42473259f84 driver-allowlist.txt
|
P2-c: classify and pin the extraction boundary
Aeneas emits a *_Template.lean naming everything the extracted code needs
from outside itself — the extraction's own statement of its boundary.
extract.sh has always said, in prose, "after regenerating, diff the template
against the hand-written file". Prose is not a gate, and the diff cannot be
one: the two files legitimately differ in almost every line, holes and
Aeneas comments against real definitions and modeling policy.
MEASURING FIRST CHANGED WHAT THIS ITEM SHOULD BE. The TODO offered two
options — enforce the diff, or pin both files — and the answer turned out to
be neither. Both files were ALREADY byte-pinned by Phase 0b. And two further
things stand here: the generated Funs.lean imports the model and CALLS these
externals, so the Lean compiler enforces their TYPES wherever the extracted
code uses them; and the per-certificate exact cones catch any external that
becomes, or stops being, an assumption anything depends on.
What none of those three sees is the CLASSIFICATION: for each name the
extraction asks for, whether this repository answers with an ASSUMPTION or
with a PROOF. That is the tier-A/B claim the documents make in prose — the
curve calls and the three curve types resolve to proven definitions rather
than axioms, because gen/CurveField/Funs.lean opens `namespace
curve25519_dalek` and so defines the very names Aeneas asks for. Nothing
checked it. A regeneration that renamed one, or a model that quietly
answered one with an axiom instead, would have left the documents claiming a
proof where the repository had an assumption.
Phase 0d recomputes the classification with model-correspondence.py
(namespace-aware, so a definition inside a namespace counts under its full
name) and requires equality with the committed MODEL-CORRESPONDENCE.txt.
UNRESOLVED — the extraction asking for something nothing here provides — is
a hard failure.
dalek 43 MODEL 8 PROVEN 3 EXTRA
anza 38 MODEL 0 PROVEN 4 EXTRA (no CurveSig crate)
risc0 36 MODEL 8 PROVEN 4 EXTRA
betrusted 35 MODEL 8 PROVEN 4 EXTRA
selftest-correspondence.sh, five cases, negative-tested by disabling the
comparison. The case that matters is 2: a PROVEN external answered by an
axiom instead. No name changes anywhere, every byte pin still matches, and
it compiles, because the signature is unchanged — before Phase 0d nothing in
the button could tell.
Trap recorded for whoever extends it: case 3 first deleted the PROVEN rows,
which was VACUOUS on anza, since anza has none — it removed nothing, the
table still matched, and the case passed while testing nothing. It now
deletes the first row whatever its verdict AND asserts the file changed.
extract.sh now points at the gate instead of asking a human to look.
Certified by a full sweep: both buttons, all four forks, purged trees,
machine otherwise idle. 8/8 green.
2026-07-31 15:53:31 +00:00
|
|
|
71244d824847311bcb3ba8ad1f1905c4b24fe8f015e3230969914019cb628b61 extract.sh
|
correspondence: a named section is not a namespace; an extra axiom is a failure
Round-8 review (GPT-5.6, register key `section-prefix-bug`, CRITICAL).
Reproduced here exactly before fixing.
model-correspondence.py treated `namespace`, `section` and `end` as one event
class and pushed a named section onto the fully-qualified-name prefix. Lean
does not: `section Foo` opens a scope for `variable`/`open` and gives `end Foo`
a label; it does not turn `bar` into `Foo.bar`. Given a template reading
section Foo
axiom bar : Nat
end Foo
the scanner reported `Foo.bar`, `--names` handed Phase 2d only `Foo.bar`, Lean
resolved an unrelated `Foo.bar` definition elsewhere in the corpus, and the
verdict came back PROVEN. The axiom the extraction ACTUALLY depends on was
never queried. This survived both the fail-closed rewrite and the new
Lean-semantic phase, in a scanner rewritten that same week specifically to
stop dropping things.
AND THE REASON IT STAYED SILENT, which is the half worth keeping. The real
external did not vanish — it landed in the table as EXTRA, the one verdict
that could not fail. A silent bucket beside a fail-closed parser is a slower
way of dropping things. An extra AXIOM is now EXTRA-AXIOM and stops the
button: the model exists to answer the template, so an assumption nothing
asks for is either a parse we got wrong or an assumption nobody governs.
Extra definitions stay tolerated; helpers in a model file are ordinary.
That gate fired on the real corpora on its first run. Each fork's
hand-maintained gen/CurveField/FunsExternal.lean carried AVX2/AVX512 backend
axioms present in no template, no proof, no cone and no allowlist — dead
assumptions in a pinned trusted-base file, reported as EXTRA and therefore
invisible. extract.sh:16 confirms these files are never overwritten by
extraction, so they were hand-written and are removed here:
dalek 2, anza 3, risc0 4, betrusted 4
Nothing referenced them, so no certificate's cone changes; the trusted base
simply gets smaller. Table rows 64->62, 51->48, 57->53, 56->52, and Phase 2d
independently resolved 62/48/53/52 externals against the regenerated tables.
GEN-MODEL.sha256 and HARNESS.sha256 both move: the model bytes changed, and
the harness pins the table and the gen manifest themselves.
Certified: round-10 sweep, 2h53m, ten instruments in each of four forks,
40/40 GREEN, 0 failing, 0 resource-limited. A full run was required — the
--audit-only staleness gate correctly refused after a source change.
Registered in formal-verification-control/review-findings.tsv as
`section-prefix-bug` and `dead-model-axioms`.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 19:29:54 +00:00
|
|
|
3898670a2cb3db74d7381372a09649f6518e49384adc935d73bd6be7f825f7b9 GEN-MODEL.sha256
|
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 10:15:26 +00:00
|
|
|
b9c907f94572c06a59135d29377d51ad8efc3f74402ac61e8644a15786d4b0ed inventory-allowlist-scalar.txt
|
verification: pin the whole declaration surface (P1-b)
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 23:20:20 +00:00
|
|
|
86ee83b703d17c1f04af654657219b344b0076bc994c0b791ca6b6c5a0090d4f inventory-allowlist.txt
|
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 10:15:26 +00:00
|
|
|
3ebc8027f14c9e037f36322ef4119183c33214658efcc1a7bc985a98a9c32e4e inventory_gate.sh
|
verification: pin the harness, the audit drivers and the policy files (P1-c)
Every gate this repository has was executed by scripts that nothing pinned.
Round-5 review of the companion SLH-DSA repository stubbed the compiler
wrapper alone and its button printed ALL GREEN in 3.6 seconds over
deliberately destroyed proofs; flipping two guards in the audit driver
disabled every check with the digest byte-identical. Depth of checking is
worth nothing if the thing doing the checking is unbound — and every gate
added this week made that gap more valuable to an attacker, not less.
Phase 0c requires every harness file to match HARNESS.sha256. Two design
points carry the weight:
- WHICH files must be pinned is POLICY and lives in check.sh, never in the
map being consulted. If the required set were read from the pin file,
deleting an entry would silently un-pin that file. It is instead derived
from the filesystem, so a deleted entry is a set mismatch and a build
failure. That is the exact defect SLH-DSA round-6 found, closed here by
construction.
- Membership self-derives from the executable bit: anything this script can
shell out to must be pinned, so a NEW script fails closed until someone
pins it deliberately. Load-bearing files that are not executable — the
audit driver, the committed manifests, the policy tables — cannot be
discovered that way and are listed explicitly.
lean-guard is inside the set, which finally makes the standing "lean-guard
stays hash-pinned" rule a property of the repository rather than a convention.
selftest-harness.sh replays five cases, each asserting a specific diagnostic:
an edited lean-guard, a new unpinned executable, a deleted pin entry, a
missing pin file, and a positive control. It was itself negative-tested — with
the hash comparison removed it goes red on exactly that case while cheerfully
reporting "10 harness files match their pins".
TRUSTED-BASE.md states the limit at equal length to the claim: pinning a
harness from inside that harness is circular, and an author who edits a script
and refreshes its pin in the same commit passes every phase. What the pin
changes is that the edit can no longer be SILENT — it must appear in the diff
at the commit being reviewed. A green button says "this is the apparatus that
was reviewed", never "this apparatus is trustworthy".
Also fixed, found by this sweep: both self-tests compared the working tree
against its starting state with `diff <(echo "$VAR") <(command)`, which is
asymmetric — for a clean tree the variable is empty and `echo` emits a blank
line the command does not. It reported a difference precisely when nothing was
wrong, and only surfaced once P1-a was committed and Proofs/ became clean.
Both now compare as strings.
Verified green: 20 runs across the four ed25519 repositories (four buttons,
four harness self-tests, four axiom-gate self-tests, four binding self-tests,
four scalar buttons), zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 18:13:01 +00:00
|
|
|
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
|
lift-guard: eleven more classes, two of them regressions I introduced
Round-9 review (Claude, N1). The brief said "assume there are more"; there
were eleven, and two were introduced by the round-8 fix itself.
INTRODUCED BY THE ARITHMETIC TOKENISATION — the round-8 fix for a false
NEGATIVE created two false POSITIVES. The interior of `$(( ))` was tokenised
with `[A-Za-z_][A-Za-z0-9_]*`, which starts matching at the letter-bearing tail
of a numeric literal:
echo $((0x1F)) -> FATAL: reads x1F
echo $((1e3)) -> FATAL: reads e3
Now anchored so a match cannot begin after a digit or word character.
INTRODUCED BY THE INDIRECT-EXPANSION REFUSAL, and this is the one that matters.
`${!...}` has three meanings and `re.search(r'\$\{!')` cannot tell them apart:
${!name} indirect expansion — genuinely unanalysable
${!arr[@]} ${!arr[*]} array KEY expansion — ordinary
${!prefix*} ${!prefix@} variable-NAME listing — ordinary
A refusal is the most expensive verdict this tool has — it hard-fails the lift
— and it was firing on two ordinary constructs with a diagnostic naming a
feature they do not use. The reviewer found it LIVE: ltl-accumulator
check.sh:274 is `for cert in "${!CONES[@]}"`, so the day lift-guard is ported
there, any lift covering that line would have refused. The four forks carry
five arrays each, so it was one ordinary edit away from firing there too.
Now matched only for genuine `${!name}`.
SEVEN MORE BINDING FORMS the driver uses and the guard demanded anyway:
let FOO=1 · (( FOO = 1 )) · BAR+=b · FOO[0]=x
for (( i=0; i<3; i++ )) · select FOO in · getopts "o" FOO
Arithmetic contexts bind as well as read, so `(( i++ ))` and the C-style `for`
now contribute to assigns — without that, the reads-extraction added by the
round-8 fix demanded the very names those expressions assign.
Verified: all eleven silent, genuine `${!n}` still refuses, `$((X+1))` and
`((Y>0))` still caught by name, the whole round-8 matrix unchanged, a genuine
missing variable still fails, and the four lifting self-tests green in all four
forks.
The reviewer also discarded one candidate rather than report it — `i=0;
(( i++ ))` looks like a demand but is silent under driver ⊇ payload, which is
how the self-tests invoke it. That restraint is worth recording: a guard edited
twice for false alarms should not be handed a false alarm by its reviewer.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-03 19:03:35 +00:00
|
|
|
cad0ae17ce506e1defeab3b9799993b3a2251c055247695832ecae2c2617772f lift-guard.sh
|
correspondence: a named section is not a namespace; an extra axiom is a failure
Round-8 review (GPT-5.6, register key `section-prefix-bug`, CRITICAL).
Reproduced here exactly before fixing.
model-correspondence.py treated `namespace`, `section` and `end` as one event
class and pushed a named section onto the fully-qualified-name prefix. Lean
does not: `section Foo` opens a scope for `variable`/`open` and gives `end Foo`
a label; it does not turn `bar` into `Foo.bar`. Given a template reading
section Foo
axiom bar : Nat
end Foo
the scanner reported `Foo.bar`, `--names` handed Phase 2d only `Foo.bar`, Lean
resolved an unrelated `Foo.bar` definition elsewhere in the corpus, and the
verdict came back PROVEN. The axiom the extraction ACTUALLY depends on was
never queried. This survived both the fail-closed rewrite and the new
Lean-semantic phase, in a scanner rewritten that same week specifically to
stop dropping things.
AND THE REASON IT STAYED SILENT, which is the half worth keeping. The real
external did not vanish — it landed in the table as EXTRA, the one verdict
that could not fail. A silent bucket beside a fail-closed parser is a slower
way of dropping things. An extra AXIOM is now EXTRA-AXIOM and stops the
button: the model exists to answer the template, so an assumption nothing
asks for is either a parse we got wrong or an assumption nobody governs.
Extra definitions stay tolerated; helpers in a model file are ordinary.
That gate fired on the real corpora on its first run. Each fork's
hand-maintained gen/CurveField/FunsExternal.lean carried AVX2/AVX512 backend
axioms present in no template, no proof, no cone and no allowlist — dead
assumptions in a pinned trusted-base file, reported as EXTRA and therefore
invisible. extract.sh:16 confirms these files are never overwritten by
extraction, so they were hand-written and are removed here:
dalek 2, anza 3, risc0 4, betrusted 4
Nothing referenced them, so no certificate's cone changes; the trusted base
simply gets smaller. Table rows 64->62, 51->48, 57->53, 56->52, and Phase 2d
independently resolved 62/48/53/52 externals against the regenerated tables.
GEN-MODEL.sha256 and HARNESS.sha256 both move: the model bytes changed, and
the harness pins the table and the gen manifest themselves.
Certified: round-10 sweep, 2h53m, ten instruments in each of four forks,
40/40 GREEN, 0 failing, 0 resource-limited. A full run was required — the
--audit-only staleness gate correctly refused after a source change.
Registered in formal-verification-control/review-findings.tsv as
`section-prefix-bug` and `dead-model-axioms`.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 19:29:54 +00:00
|
|
|
1942177f13d6ae229d87a3b0b33f7fbb4b2ae20fe1059cc83010e73f6a156427 model-correspondence.py
|
|
|
|
|
77e356f607c01ff597193f28f60b48a701ca2b9597cc9a991ac5b27b00aeaf81 MODEL-CORRESPONDENCE.txt
|
verification: pin the harness, the audit drivers and the policy files (P1-c)
Every gate this repository has was executed by scripts that nothing pinned.
Round-5 review of the companion SLH-DSA repository stubbed the compiler
wrapper alone and its button printed ALL GREEN in 3.6 seconds over
deliberately destroyed proofs; flipping two guards in the audit driver
disabled every check with the digest byte-identical. Depth of checking is
worth nothing if the thing doing the checking is unbound — and every gate
added this week made that gap more valuable to an attacker, not less.
Phase 0c requires every harness file to match HARNESS.sha256. Two design
points carry the weight:
- WHICH files must be pinned is POLICY and lives in check.sh, never in the
map being consulted. If the required set were read from the pin file,
deleting an entry would silently un-pin that file. It is instead derived
from the filesystem, so a deleted entry is a set mismatch and a build
failure. That is the exact defect SLH-DSA round-6 found, closed here by
construction.
- Membership self-derives from the executable bit: anything this script can
shell out to must be pinned, so a NEW script fails closed until someone
pins it deliberately. Load-bearing files that are not executable — the
audit driver, the committed manifests, the policy tables — cannot be
discovered that way and are listed explicitly.
lean-guard is inside the set, which finally makes the standing "lean-guard
stays hash-pinned" rule a property of the repository rather than a convention.
selftest-harness.sh replays five cases, each asserting a specific diagnostic:
an edited lean-guard, a new unpinned executable, a deleted pin entry, a
missing pin file, and a positive control. It was itself negative-tested — with
the hash comparison removed it goes red on exactly that case while cheerfully
reporting "10 harness files match their pins".
TRUSTED-BASE.md states the limit at equal length to the claim: pinning a
harness from inside that harness is circular, and an author who edits a script
and refreshes its pin in the same commit passes every phase. What the pin
changes is that the edit can no longer be SILENT — it must appear in the diff
at the commit being reviewed. A green button says "this is the apparatus that
was reviewed", never "this apparatus is trustworthy".
Also fixed, found by this sweep: both self-tests compared the working tree
against its starting state with `diff <(echo "$VAR") <(command)`, which is
asymmetric — for a clean tree the variable is empty and `echo` emits a blank
line the command does not. It reported a difference precisely when nothing was
wrong, and only surfaced once P1-a was committed and Proofs/ became clean.
Both now compare as strings.
Verified green: 20 runs across the four ed25519 repositories (four buttons,
four harness self-tests, four axiom-gate self-tests, four binding self-tests,
four scalar buttons), zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 18:13:01 +00:00
|
|
|
772ca6dd22443c83dc35d5428598c8d17a01c69db5be008474d06476fa66f7f8 Proofs/Audit.lean
|
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 10:15:26 +00:00
|
|
|
5274b1881579e24030b1aed608511640b8ba39f7e6cdb8962ce23bece655c10b Proofs/InventoryCore.lean
|
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
2026-08-01 14:10:59 +00:00
|
|
|
660d35343f5673d4bc854787b6a34063c956567bd7e2eb62955a92e3c55bfa6b Proofs/Inventory.lean
|
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 10:15:26 +00:00
|
|
|
f921d028149e41016c75db2d316f26450768c614eb8b8b9764c49da84bbf6fc8 Proofs/InventoryScalar.lean
|
|
|
|
|
907616a9386727ec6d030f9ed1c9122d5ccfe4c011b23b781ff728dbb99a2582 Proofs/ScalarAudit.lean
|
|
|
|
|
4b550a618b4d4e14be9e7646ae9d515d784d231b34fee39415002a25e370e9b7 SCALAR-AUDIT-MANIFEST.txt
|
verification: --audit-only mode, and the guard that keeps it from becoming evidence (T1)
Gate work dominates this estate's wall-clock: on 2026-07-29, 3.9 hours of a
session went to Lean re-elaborating proofs nobody had edited while the audit
phases themselves took about fifteen seconds. --audit-only runs every gate
against the artifacts a previous full run left behind: ~60s against ~1280s.
IT IS SAFE ONLY BECAUSE IT REFUSES.
- It requires every shipped .lean to be BYTE-IDENTICAL to a basis recorded by
a previous full run. Not mtimes: `touch` defeats those, and a stale-artifact
check that fails open is worse than no shortcut at all, because a green
button would then describe a corpus that is no longer on disk.
- The basis is gitignored build state, so a fresh clone cannot inherit
permission to skip compiling.
- The closing banner differs and says in words that the run is not evidence.
selftest-auditonly.sh exercises seven cases: no basis, an edited comment
character, a deleted source, a new source, a missing artifact, a truncated
basis, and — asserted as a PASS — every source's mtime touched with bytes
unchanged, which pins the bytes-not-mtimes decision rather than leaving it
implicit. Negative-tested: with the basis comparison disabled a changed source
is wrongly accepted, exit 0 and zero refusals, so the guard is load-bearing.
A PHASE TERMINATOR, because this broke twice. Every self-test lifts a phase
from check.sh by scanning to the next phase marker. The last phase had no
marker after it, so a lift ran to end-of-file and swallowed whatever was
appended later — first Phase 2c into the axgate lift, then T1's tail into the
binding lift, where it referenced $AUDIT_ONLY and died under `set -u`. Both
surfaced as the BASELINE case failing: a self-test blaming a gate for its own
extraction bug. The phases now end at an explicit sentinel and both lifters
stop there, so nothing appended below can silently become part of the last
phase from a lifter's point of view.
TRUSTED-BASE.md records what an audit-only transcript does and does not
establish, and — because it cost a confusing red run today — that lean-guard's
memory clamp presents as `FAIL: Proofs/<module>` while being a resource
condition, not a broken proof.
Verified green: 8 full button runs (four check.sh, four check-scalar.sh) and 20
self-tests across the four repositories, zero red. One earlier run failed on
the memory clamp because the author ran a test suite concurrently; re-run on a
quiet machine, green.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-30 17:16:21 +00:00
|
|
|
bf71e8d4eb312ebc687bf7e218d90b910543cd92e782078174868d012aca7250 selftest-auditonly.sh
|
verification: derive lift dependencies instead of hand-keeping them
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 11:07:28 +00:00
|
|
|
6de61b2b08ab6e05c7d38377ea8f70178da4a105bb1df21c6ba6bc05a647090d selftest-axgate.sh
|
|
|
|
|
7822c007d12d7be70003ea9de234102a2c4165cfab65a108e2960e51b87bee82 selftest-correspondence.sh
|
|
|
|
|
41d16df48b15b99512d10a805bb811db301e9d9c8b00e5e3e0186f0110d3b71a selftest-harness.sh
|
verification: pin the whole declaration surface (P1-b)
Phase 2b asks the kernel whether any AXIOM is declared under Proofs/. Phase 3
pins the cones of the named certificates. Between them sat every other
declaration in the corpus — around three thousand of them — and a helper lemma
quietly acquiring a hash oracle in its cone moved nothing either phase looked
at.
Phase 2c closes that. Ported from ltl-accumulator-verified, where a nine-attack
self-test proved a source-regex enumerator evadable by attributed, private,
indented and `instance` declarations and by a nested-namespace basename
collision. Reading the compiled environment sees what the kernel saw; no name
shape hides. Every constant contributes module, name, kind and full axiom cone,
and the observed set must equal inventory-allowlist.txt exactly in BOTH
directions, with a count trailer so a truncated run cannot pass as an empty
diff.
FOUR THINGS THIS BUILD GOT WRONG, each caught by a check rather than by review:
- The number of inventory drivers is a per-repo FACT, not an assumption.
dalek and anza cannot import their corpus as one environment (Proofs.Basic
and Proofs.ConstSpecs both declare CurveFieldProofs.zero_spec); risc0 and
betrusted have no Proofs.Basic at all. Determined by compiling a probe.
check.sh now DISCOVERS its drivers from the filesystem instead of naming
two, and the generator refuses to split out a module the repo lacks.
- The split let one real declaration hide behind another's entry. Keyed on
name alone, the two zero_specs produced byte-identical records, so 3022
declarations were covered by 3021 allowlist entries. Caught by the count
trailer. Every record now carries its originating module.
- The gate's success line said "single sanctioned axiom", inherited from the
accumulator's policy. This corpus permits NONE. A success message
describing a different rule is how an assertion stops meaning anything.
- selftest-axgate.sh lifted Phase 2b with a range ending at "Phase 3", so
inserting Phase 2c between them made it swallow the new phase and die on
variables only check.sh defines — surfacing as the BASELINE case failing,
a self-test blaming a gate for its own extraction bug. Both self-tests now
stop at the next phase marker whatever it is called, and refuse to run if
they capture more than one phase. The guard is the fix; the range was the
symptom.
WHAT THIS IS NOT, recorded in TRUSTED-BASE.md at the same length as the claim:
- No independent cone walker. The accumulator cross-checks collectAxioms
against a hand-written walker. Ported here it was wrong in BOTH directions
on mathlib's inductive shapes: EdPoint gave [] against the kernel's three
axioms, and once extended, ProjPoint gave three against the kernel's none.
Two implementations disagreeing both ways are a second wrong answer, not a
check. These cones rest on collectAxioms alone.
- Thirteen Proofs/Scalar* modules are inventoried by nothing — the
second-button seam, still open. Phase 2c names every uncovered module on
every run so the omission is visible rather than inferred.
selftest-inventory.sh exercises the shipping gate with six cases, each
asserting a specific diagnostic, including the one that matters: a cone
widened by one oracle while name, module and kind stay put. Negative-tested by
disabling the gate's diff, which turns two cases red including one for the
wrong reason, correctly reported as such.
Verified green: 20 runs across the four repositories (four buttons, four
harness, four inventory, four axgate, four binding self-tests), zero red. The
four check-scalar.sh greens from the preceding sweep stand: that script neither
reads the pin file nor changed.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-07-29 23:20:20 +00:00
|
|
|
1df031a075fc438c5229d01cbc44ee6ac489a272cd736624f7ca45ef1a4ddb7f selftest-inventory.sh
|
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 10:15:26 +00:00
|
|
|
acfa40b0f45bf7969dd6e2a26ea72e9eaf824cedb695e498f863360772fd7c06 selftest-scalar-statements.sh
|
verification: derive lift dependencies instead of hand-keeping them
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 11:07:28 +00:00
|
|
|
fc6d2905871500f2ee9c3f308fd8300cfcd1a7fa854d399d13812f7e2282f1fd selftest-shapes.sh
|
|
|
|
|
eb7367a1494f5203f0cbeace78c9522608d51825fdcbb7ae40962d2380a7bc79 selftest-statements.sh
|
|
|
|
|
7603b82c9c29a27f6659b8878d1a2e2365afb6541c3c5b2698ab2fee21bb2bde selftest-tiers.sh
|