mirror of
https://github.com/saymrwulf/risc0-ed25519-verified.git
synced 2026-09-04 20:03:41 +00:00
12 commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
| 9c6c3b16a3 |
correspondence: a named section is not a namespace; an extra axiom is a failure
Round-8 review (GPT-5.6, register key `section-prefix-bug`, CRITICAL).
Reproduced here exactly before fixing.
model-correspondence.py treated `namespace`, `section` and `end` as one event
class and pushed a named section onto the fully-qualified-name prefix. Lean
does not: `section Foo` opens a scope for `variable`/`open` and gives `end Foo`
a label; it does not turn `bar` into `Foo.bar`. Given a template reading
section Foo
axiom bar : Nat
end Foo
the scanner reported `Foo.bar`, `--names` handed Phase 2d only `Foo.bar`, Lean
resolved an unrelated `Foo.bar` definition elsewhere in the corpus, and the
verdict came back PROVEN. The axiom the extraction ACTUALLY depends on was
never queried. This survived both the fail-closed rewrite and the new
Lean-semantic phase, in a scanner rewritten that same week specifically to
stop dropping things.
AND THE REASON IT STAYED SILENT, which is the half worth keeping. The real
external did not vanish — it landed in the table as EXTRA, the one verdict
that could not fail. A silent bucket beside a fail-closed parser is a slower
way of dropping things. An extra AXIOM is now EXTRA-AXIOM and stops the
button: the model exists to answer the template, so an assumption nothing
asks for is either a parse we got wrong or an assumption nobody governs.
Extra definitions stay tolerated; helpers in a model file are ordinary.
That gate fired on the real corpora on its first run. Each fork's
hand-maintained gen/CurveField/FunsExternal.lean carried AVX2/AVX512 backend
axioms present in no template, no proof, no cone and no allowlist — dead
assumptions in a pinned trusted-base file, reported as EXTRA and therefore
invisible. extract.sh:16 confirms these files are never overwritten by
extraction, so they were hand-written and are removed here:
dalek 2, anza 3, risc0 4, betrusted 4
Nothing referenced them, so no certificate's cone changes; the trusted base
simply gets smaller. Table rows 64->62, 51->48, 57->53, 56->52, and Phase 2d
independently resolved 62/48/53/52 externals against the regenerated tables.
GEN-MODEL.sha256 and HARNESS.sha256 both move: the model bytes changed, and
the harness pins the table and the gen manifest themselves.
Certified: round-10 sweep, 2h53m, ten instruments in each of four forks,
40/40 GREEN, 0 failing, 0 resource-limited. A full run was required — the
--audit-only staleness gate correctly refused after a source change.
Registered in formal-verification-control/review-findings.tsv as
`section-prefix-bug` and `dead-model-axioms`.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
|||
| cc571bf163 |
verification: derive lift dependencies instead of hand-keeping them
Round-9 swept all ten instruments per fork instead of only the two buttons,
and found selftest-axgate.sh red in all four. Root cause, identical to the
KERNLOG defect fixed the day before: a self-test lifts one phase out of
check.sh and supplies its variables from a HAND-WRITTEN preamble, and the
phase later grew a dependency nobody told the preamble about.
Phase 2b stopped globbing Proofs/*.olean and started reading $PROOFS by
membership. Bash does not error on an unset array under `set -u` — it
expands to nothing — so the gate silently received
expected := [".olean"]
one entry with an empty name, and rejected the baseline via its own
fail-closed absence check. Exit code right, reason wrong.
· lift-guard.sh (new, pinned): derives every variable the lifted payload
reads, subtracts what the driver defines, and fails AT LIFT TIME naming
the remainder. Wired into all five lifting self-tests; selftest-shapes.sh
drops its inline copy. One implementation, not five, since drifting out
of sync is the entire failure mode.
· selftest-axgate.sh: lifts PROOFS verbatim, and its case 2 now poisons a
MANIFESTED leaf module rather than adding a stray file. The stray-file
attack was a no-op against membership semantics — that is the dead-file
gate's job, proven by selftest-harness case 8 — and it is also the
weaker attack, since adding files to Proofs/ must clear a gate that
editing an already-manifested module does not.
· Phase 2c's accounting identity moves behind its own marker with its own
ACCTFAIL verdict, so the phase is liftable by construction rather than
by a self-test knowing where to stop. Truncating the lift range alone
would have dropped Phase 2c's own verdict and left the test unable to fail.
· The other four lifting self-tests assert on the PAYLOAD rather than the
assembled driver, so a marker in the preamble cannot satisfy a check
meant to prove the lift landed.
Certified: 8/8 self-tests green in all four forks (~212 assertions, none
failing); check.sh bytes unchanged and still matching the pin written before
the 3h08m round-9 sweep, whose 36 GREEN button rows therefore stand.
--audit-only re-run against the new HARNESS.sha256 in every fork.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
|||
| 4fafaab608 |
Round-7 F1: make model/template correspondence SEMANTIC, and fail closed
THE DEFECT, as found. GPT-5.6 showed the textual classifier could report
PROVEN for a name Lean resolves to an axiom: a definition appearing only
inside a `/- -/` comment was read as real. Repairing that exposed something
larger and already live. Aeneas wraps long declarations:
axiom
curve25519_dalek.edwards.EdwardsPoint.Insts.CoreOpsArithNegEdwardsPoint.neg
The old scanner required keyword and name on one physical line, so it matched
nothing there and SILENTLY DROPPED the declaration — no MODEL row, no PROVEN
row, no failure. Nine to ten externals per fork had no row at all, and the
tier-A/B `neg` was missing from every committed table while the trust
documents claimed that class was machine-checked. Four pinned tables were
wrong, in four repositories, with the buttons green over them. No attacker
was required; Aeneas's own formatting did it.
The lesson is not "write a better regex". The scanner was FAIL-OPEN: input it
could not parse produced silence instead of a stop. A gate that drops what it
cannot read is worse than no gate, because the green covers a gap that is
invisible in the diff.
THE REPAIR, in three layers that each do only what they honestly can.
· DISCOVERY stays textual, because the template cannot be imported — it
declares the same names as the model and they would clash. It now strips
NESTED `/- -/` blocks, reads a name that wraps to a later line, tracks
namespace/section/end, and FAILS CLOSED: an unparseable keyword exits 2
naming file and line.
· Phase 0d keeps the cheap pre-compile comparison against the table.
· Phase 2d is new and authoritative. After compilation it generates a temp
Lean driver (the Phase 2b idiom, so no permanent module and no manifest
churn), imports every non-template gen module, and asks env.find? what
each external IS: kind and originating module. Model module -> MODEL;
non-axiom in a generated module -> PROVEN; an axiom outside the model, or
a name that does not resolve, is a failure. Lean's verdict must equal the
committed table's, and the answer count must equal the question count so
a truncated resolver cannot pass.
THE TABLES were regenerated and verified three ways before being committed:
an independently written second scanner agreed on 228/228 rows across the
four forks; all 47 changed rows carry file:line evidence; and the PROVEN row
was put to Lean directly — kind = def, module = CurveField.Funs.
dalek 54 -> 64 rows anza 42 -> 51 risc0 48 -> 57 betrusted 47 -> 56
Also corrected: `from_residual` was recorded EXTRA in every fork; the
template does demand it, so it is MODEL. anza carried a spurious `hash|EXTRA`
row from a mis-parse.
NEGATIVE-TESTED. With Phase 0d neutered so Phase 2d was the gate under test,
a PROVEN row edited to MODEL produces:
SEMANTIC DRIFT: ...neg — table says MODEL, Lean says PROVEN
selftest-correspondence.sh grew 4 cases -> 7: GPT's comment counterexample,
the wrapped declaration that was actually live, and a fail-closed check.
WHAT THIS DOES NOT CLOSE. Phase 2d resolves names in the environment built
from gen/. It establishes what a name IS — assumption or proof, and where —
not that the extraction faithfully represents the Rust. That remains the
Charon/Aeneas trust assumption and no gate here can close it.
Certified: both buttons, all four forks, purged trees. 8/8 green, with
62/48/53/52 externals resolved by Lean and every verdict matching.
|
|||
| 08811d9118 |
Account for every constant the kernel sees, by set containment
THE GAP. The capability matrix in the control repo — built after the author
answered a capability question by grepping for a FILENAME rather than for the
property, three times in one session — asked whether each repository's auditor
enumerates itself. The four ed25519 forks answered no. Following that up found
something larger: `Proofs/Audit.lean`, the statement-binding driver from P1-a,
is compiled, is a member of the manifest, and was enumerated by NOTHING. The
kernel counted 3058 declarations where the inventory accounted for 3022, and
26 of the 36 missing were its.
THE PROPERTY, now enforced: every constant the kernel sees under this button's
manifest must appear, BY NAME, in either the corpus inventory or the
instruments' own surface. `emitDrivers` in InventoryCore walks the audit
modules and fails closed on an axiom (which would widen the trusted base
outside every cone) or on a standalone claim (which no certificate covers and
no allowlist pins), while admitting the obligations the elaborator generates
for a definition declared alongside it.
TWO WRONG FORMULATIONS FIRST, both recorded because the second is instructive:
· `kernel = corpus + instruments + N_DRIVERS`, where the last term was
justified as a per-driver "self-observation blind spot". It fitted dalek
and anza (2 drivers, residual 2) and broke on risc0 and betrusted
(1 driver, residual 2). The residual is 2 everywhere and has nothing to do
with drivers. This was curve-fitting from a sample of one, and it was named
as the highest-risk claim in the round-7 self-assessment BEFORE the data
refuted it.
· distinct-by-name counting, which collapses `CurveFieldProofs.zero_spec` —
a name that genuinely denotes two different declarations, in Proofs.Basic
and Proofs.ConstSpecs, walked by two drivers with separate environments.
THE MEASURED CAUSE of the residual. Lean materialises equation lemmas lazily,
when something forces an unfold, and each module that forces one gets its own
copy in its object file. `CurveFieldProofs.denote.eq_1` sits in both
SubNegSpec.olean and ConstSpecs.olean; `CurveFieldProofs.limbsVal.eq_1` in both
ReduceSpec.olean and ConstSpecs.olean. The kernel gate reads object files and
counts both copies; the environment holds one constant per name. Counts cannot
relate those two views in either direction — so the check compares SETS, which
is the idiom the rest of this estate already uses, and no constant remains that
could be widened to make a red run green.
Negative-tested: with the instrument walk disabled, the check names
Proofs.Audit's declarations as unaccounted.
ANZA also lacked one allowlist row, `subtle.Choice...from.eq_1`, the same
lazy-materialisation effect seen from the other side. Verified rather than
assumed before adding it: the parent is declared in gen/CurveField/
FunsExternal.lean — the model, pinned by bytes and not inventoried by
declaration — the lemma materialised in Proofs.CompressSpec which forced the
unfold, and all three other forks carry the lemma row while none carries the
parent.
CONSEQUENCE WORTH DISCLOSING: the audited declaration surface is not purely a
function of the corpus source. It depends on which proofs forced which
unfolds. This is now a known gap in the round-7 kit.
Also corrected here: Proofs/Inventory.lean's header claimed the audit drivers
were excluded from the compile manifest. They are lines 42-44 of PROOFS.
Certified by a full sweep: both buttons, all four forks, purged trees. 8/8.
|
|||
| 92f3229761 |
P2-c: classify and pin the extraction boundary
Aeneas emits a *_Template.lean naming everything the extracted code needs from outside itself — the extraction's own statement of its boundary. extract.sh has always said, in prose, "after regenerating, diff the template against the hand-written file". Prose is not a gate, and the diff cannot be one: the two files legitimately differ in almost every line, holes and Aeneas comments against real definitions and modeling policy. MEASURING FIRST CHANGED WHAT THIS ITEM SHOULD BE. The TODO offered two options — enforce the diff, or pin both files — and the answer turned out to be neither. Both files were ALREADY byte-pinned by Phase 0b. And two further things stand here: the generated Funs.lean imports the model and CALLS these externals, so the Lean compiler enforces their TYPES wherever the extracted code uses them; and the per-certificate exact cones catch any external that becomes, or stops being, an assumption anything depends on. What none of those three sees is the CLASSIFICATION: for each name the extraction asks for, whether this repository answers with an ASSUMPTION or with a PROOF. That is the tier-A/B claim the documents make in prose — the curve calls and the three curve types resolve to proven definitions rather than axioms, because gen/CurveField/Funs.lean opens `namespace curve25519_dalek` and so defines the very names Aeneas asks for. Nothing checked it. A regeneration that renamed one, or a model that quietly answered one with an axiom instead, would have left the documents claiming a proof where the repository had an assumption. Phase 0d recomputes the classification with model-correspondence.py (namespace-aware, so a definition inside a namespace counts under its full name) and requires equality with the committed MODEL-CORRESPONDENCE.txt. UNRESOLVED — the extraction asking for something nothing here provides — is a hard failure. dalek 43 MODEL 8 PROVEN 3 EXTRA anza 38 MODEL 0 PROVEN 4 EXTRA (no CurveSig crate) risc0 36 MODEL 8 PROVEN 4 EXTRA betrusted 35 MODEL 8 PROVEN 4 EXTRA selftest-correspondence.sh, five cases, negative-tested by disabling the comparison. The case that matters is 2: a PROVEN external answered by an axiom instead. No name changes anywhere, every byte pin still matches, and it compiles, because the signature is unchanged — before Phase 0d nothing in the button could tell. Trap recorded for whoever extends it: case 3 first deleted the PROVEN rows, which was VACUOUS on anza, since anza has none — it removed nothing, the table still matched, and the case passed while testing nothing. It now deletes the first row whatever its verdict AND asserts the file changed. extract.sh now points at the gate instead of asking a human to look. Certified by a full sweep: both buttons, all four forks, purged trees, machine otherwise idle. 8/8 green. |
|||
| 96765ea721 |
P2-a': can a declaration hide from the inventory walker?
Phase 2c exists because a source-regex enumerator proved evadable in ltl-accumulator-verified: attributed, private and `instance` declarations and a nested-namespace basename collision all slipped past it. The fix was to stop reading source text and ask the Lean environment, and that fix was ported here. But a fix ported is not a fix tested. selftest-inventory.sh proves the GATE reacts to a difference; it feeds synthetic observations and never runs the walker. Nothing here had ever asked whether the WALKER SEES a declaration written in an evasive shape. selftest-shapes.sh adds all four shapes to an audited module, recompiles it, runs the real Phase 2c, and requires each one to be NAMED in the UNCLASSIFIED list. Asserting that the gate merely failed would not do: one shape surfacing fails the run while the other three ride along unseen. All four forks report all four. Negative-tested by removing the injection — the run then reports the walker blind and fails. The victim module is derived from each repo's own manifest, not named: the forks do not share a corpus (dalek/anza attack Proofs.Basic, risc0/betrusted Proofs.DecompressMain), and a hard-coded name would have silently found nothing on half of them. It must be manifested, must not be an inventory or audit driver, and must be imported by no other manifest module. Two notes for whoever edits this next. When re-deriving a leaf module, the inventory drivers must be excluded from the set of IMPORTERS as well as from the candidates: they import the whole corpus, so leaving them in makes every module look imported, finds no leaf, and the test silently has no victim at all. And a lift of Phase 2c needs SCALAR_SH/SCALAR_MANIFEST alongside PROOFS, or the coverage check dies on an unbound variable. New executable pinned in HARNESS.sha256. Certified by a full sweep: both buttons, all four forks, purged trees, machine otherwise idle. 8/8 green. |
|||
| 2a0041dd9c |
P2-a: attack the arithmetic/apex tier boundary itself
selftest-tiers.sh tests the property this repository exists to assert and
that nothing had tested: the arithmetic tier rests on the three kernel
axioms and NOTHING else. Five cases, all green.
control both tiers pass on the untouched tree
case 1 an apex axiom injected into an ARITHMETIC certificate's proof,
statement untouched so only the cone moves -> Phase 3 rejects
case 2 apex boundary widened by one name -> Phase 3 rejects
case 3 apex boundary narrowed by one name -> Phase 3 rejects
restored both tiers pass again
Which axiom to inject is derived per fork from this repo's own documented
boundary intersected with the victim module's import closure; no name is
hard-coded, so the same script ships unchanged in all four forks.
Two defects in the test were found and fixed before it was trusted. The
lifted driver first omitted `set -euo pipefail`: the phase's Lean work runs
in a subshell and the phase ends in a bare `echo ""`, so without -e the
subshell's exit 1 was masked and the driver reported GREEN while printing
APEX AUDIT FAILED. And a line-count sanity check passed an empty driver
because the CERTS array padded it; the guard now looks for the diagnostics
it means to provoke. Both are recorded in the script's comments.
The test restores what it touches and rebuilds the module it edits, so it
leaves the tree exactly as it found it. New executable is pinned in
HARNESS.sha256 (Phase 0c fails closed on an unpinned one).
Certified by a full sweep: both buttons, all four forks, from purged trees,
machine otherwise idle. 8/8 green, 0 errors.
|
|||
| 9ab8f15694 |
verification: build hygiene, and the hidden dependency it exposed (P0-a)
Phase 0a purges every .olean before compiling, bans stray Lean files at the
verification root (LEAN_PATH contains $PWD, so they join the build unaudited),
and requires gen/ to be exactly the model manifest plus its pinned templates.
The templates are KEPT, unlike SLH-DSA which deletes them: extract.sh directs
the operator to diff the hand-written external models against them, so they are
the reference for that comparison and P2-c will enforce it.
The purge is skipped under --audit-only, which exists to audit the artifacts a
previous full run produced. Those two features would otherwise destroy each
other, and it is a further reason an audit-only transcript is not evidence: it
has not had this hygiene applied.
WHAT THE PURGE EXPOSED, and it is the point of the whole item:
This button had never compiled the corpus from nothing. The signature apex
rests on scalar arithmetic — PointLiftSpec -> ScalarPackSpec ->
ScalarFromBytesSpec, and SigApexSpec -> ScalarDenote — and TWELVE of the scalar
layer's thirteen modules are transitive prerequisites of this manifest. They
were never compiled here. The button worked because check-scalar.sh had run at
some earlier point and left its .olean files behind. .olean is gitignored, so
no git status could ever have shown that the verdict rested on untracked
artifacts produced by a different script.
Nothing about the proofs was wrong. The evidence was resting on something
invisible, for the entire life of these repositories, and it surfaced the
moment something finally cleaned up before verifying.
Those twelve are now compiled here as PREREQ — BORROWED, NOT OWNED.
check-scalar.sh still audits them; Phase 1b asserts every borrowed name belongs
to the other manifest and to neither twice, so the list cannot become a second
ownership claim.
Two consequences fixed along the way, both the spelling-versus-membership error
that ScalarPackSpec has now taught four times:
- Phase 2b globbed Proofs/*.olean and would have demanded artifacts this
button never builds. It now scans its manifest by membership and fails
closed on a missing one.
- The three inventory drivers were exempted from the dead-file gate and
compiled in a later phase; after a purge they were absent when Phase 2b
ran. They are now in the manifest like everything else, and three
exemptions are gone.
The sweep runner now reports RESOURCE rather than RED when it sees a
memory_exception: lean-guard's clamp is not a broken proof, and it has misled
the operator once and the author once.
Verified green: 8 full runs from completely purged trees — four check.sh, four
check-scalar.sh — zero red, zero resource. Every artifact rebuilt from
committed source. These are the first runs in this repository's history whose
verdict provably depends on nothing but the bytes in git.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
|||
| e8d7924113 |
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>
|
|||
| afc545e408 |
verification: close the two-button seam and level up the scalar button (P0-b)
THE SEAM. This repository is checked by two scripts, and until now neither
asserted anything about the other's scope. check.sh's dead-file gate simply
SKIPPED anything named Scalar*, so a new Proofs/ScalarX.lean was gated by
nothing at all: absent from one manifest by exemption, from the other by
omission, compiled by neither, inventoried by neither. Each button now reads
the other's manifest and requires every shipped proof source to belong to
EXACTLY ONE of them — neither orphaned nor double-claimed, both directions,
plus a phantom check on entries naming files that do not exist. Negative-tested
four ways, including the exact hole this item names.
THE SCALAR BUTTON. Closing the seam exposed it as the estate's weakest link,
having been left behind by every hardening round while the main button gained
five phases. 45 lines to 227:
- source-integrity check over its sources;
- harness-pin verification, so running THIS button alone is protected and not
only running it after check.sh;
- a kernel-side axiom-declaration gate over the compiled artifacts, replacing
a source-text grep that is evadable four ways on v4.30.0-rc2;
- a declaration inventory of ~1880 constants against its own allowlist,
diffed both directions with a count trailer. These 13 modules were the only
part of the proof corpus with no inventory: check.sh Phase 2c named them as
uncovered on every run, and now names the button that covers them instead;
- per-certificate exact-cone assertions replacing `-eq 13` over matching
output lines. A count cannot say WHICH certificate is clean and passes just
as happily if one cone is reported twice.
Every fork-specific fact was read from the existing script rather than assumed:
risc0 and betrusted audit sub_loop1_one_spec where dalek and anza audit
cond_add_l_one_spec, untouched.
THREE BUGS, ONE ROOT CAUSE, all found by the gates rather than by review. Each
reasoned about how a thing is SPELLED instead of what it BELONGS TO, and the
corpus punished each: Proofs/ScalarPackSpec.lean is named like the scalar layer
and owned by the main button.
- the scalar dead-file gate globbed Scalar* and demanded ScalarPackSpec be
scalar-owned. REMOVED rather than special-cased: the seam check tests
membership in exactly one manifest, which is strictly stronger than any
prefix;
- the scalar axiom gate scanned Scalar*.olean, reporting "14 modules" for a
13-module manifest. On a tree where check.sh had not run that artifact is
absent and the button would have failed for a false reason. It now scans
the manifest by membership and fails closed on a missing artifact;
- Phase 2c's driver discovery globbed Inventory*.lean and claimed the other
button's driver, then correctly complained its own manifest lacked those
modules.
This is the family the campaign began with: a source-text axiom grep reasoning
about spelling. Recorded in TRUSTED-BASE.md because it generalises.
Also fixed: the first negative test of the scalar gate's absence check passed
for the wrong reason — the button recompiles before the gate runs, so removing
an artifact merely caused it to be rebuilt. Retested against the lifted phase,
where absence is a persistent condition.
Verified green: 24 runs across the four repositories — four main buttons, four
scalar buttons, and sixteen self-tests — zero red.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
|||
| 847613eb76 |
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>
|
|||
| d2760e41ab |
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>
|
