mirror of
https://github.com/saymrwulf/ltl-accumulator-verified.git
synced 2026-09-04 20:03:44 +00:00
6 commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
| 212db783a9 |
audit: bind the scalar statements, and make the accounting identity mean audit
Closes four round-7/8 findings. Certified by the round-12 sweep: five repositories, both buttons and every self-test, 48/48 GREEN. ── `scalar-statements-unbound` (gpt, round 7, CRITICAL) ──────────────────── The main button bound its 31 certificates' elaborated statements and reachable specification bodies. This button bound NONE of its thirteen, while TRUSTED-BASE item 8 said the audit covers "every certificate" — false across the 44-certificate surface. The finding was raised in round 7, lost from the round-8 work list by an F-number collision between two reviewers, and re-raised in round 8. Proofs/ScalarAudit.lean is generated from each fork's OWN Audit.lean, so the canonicalisation is provably the same code: pp.all rendering, whitespace normalisation, transitive specification closure. check-scalar.sh Phase 3c pins the block's digest, requires the committed copy to match byte-for-byte so a mismatch can be DIFFED, and cross-checks the auditor's certificate set against the button's CERTS array. dalek ecf3a3f8 · anza 0d942e47 · risc0 4b550a61 · betrusted 4b550a61 risc0 and betrusted share a digest and that is correct, not a collision: their ScalarSubSpec.lean differs only in doc prose and in `black_box` entries inside `simp only [...]` lists AFTER `:= by`. Proof scripts. They bind the same statements over the same specifications, which is the documented scope. selftest-scalar-statements.sh ships the two attacks the reviewer asked for: ok gutted statement caught (cone unchanged) ok rewritten specification body caught (name and cone unchanged) The second rewrites a reachable reference body to `id (…)` — DEFINITIONALLY EQUAL, so the corpus compiles and every proof typechecks and the cone is byte-identical. Every earlier phase is blind to it. ── `drv-surface-no-cones` + `accounting-certifies-enumeration` (claude) ──── The round-7 accounting identity proved every kernel constant was ENUMERATED. The reviewer showed enumeration is not audit: their planted claim WAS enumerated, as DRV|LTLAccAudit.bait.smuggled|theorem with a real cone, and nothing examined it — rows had no cone, no allowlist covered them, the statement digest does not reach instruments, and Phase 2b gates DECLARED AXIOMS, a different question. "Progress of one step, not two." DRV rows now carry their axiom cone and are pinned in driver-allowlist.txt by inventory_gate.sh with a DRV tag — the same implementation that pins the corpus, in both directions, because a second copy of a coverage gate is a second thing to drift. The axiom policy is per-surface and enforced per surface: the corpus admits exactly the sanctioned boundary, the instruments admit none, and an instrument axiom fails EVEN WHEN ALLOWLISTED. Verified with the reviewer's own payload, both placements: before the walk -> UNCLASSIFIED: DRV|…|bait.smuggled|theorem|Classical.choice,Quot.sound,propext after the walk -> ACCOUNTING FAILED names it (kernel-side) ── `drv-naming-heuristic` (claude, round 7) ──────────────────────────────── Retired as load-bearing rather than patched. The rule admits a theorem whose name extends a constant declared alongside it, and "breaks in one line" — declare `def bait`, then `theorem bait.smuggled` walks through. It stays as a fast readable first check; membership in a committed allowlist is what now carries the weight, and a new row fails closed whatever it is called. ── what round 11 caught, which was mine ─────────────────────────────────── DRV rows first shipped WITHOUT their originating driver. dalek and anza run two drivers, each declaring its own `corpus`; keyed on name alone those two distinct declarations produced one byte-identical row, `sort -u` collapsed them, and the trailers summed to 37 against 36. The estate had already learned this on the corpus walk — INV rows carry their module because two modules both declare CurveFieldProofs.zero_spec — and I rebuilt the record without it. Rows now carry their driver, and the gate FAILS CLOSED ON DUPLICATE RECORDS naming the collision: two declarations sharing one entry means one is covered by the other's, which is exactly how a real declaration hides. The trailer now checks what the drivers EMITTED, not what survives de-duplication — conflating "the run was truncated" with "two rows were identical" is what let a record-format defect present itself as an arithmetic complaint. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> |
|||
| b1fb6eba7c |
accumulator: a run that is not attestation-ready must not exit 0, and must name its subject
Two round-7/8 findings, both closed here.
`acc-exit0-fidelity` — CRITICAL, raised INDEPENDENTLY by both reviewers
(Claude F1, GPT-5.6 F10) and lost from the round-8 work list by the F-number
collision the finding register now prevents.
check.sh emitted a careful pair of markers — ATTESTATION GREEN only when
fidelity actually ran — and then returned 0 either way. The marker discipline
was right; the exit code contradicted it. A caller doing the obvious thing
./check.sh && append
read success from a run whose own last line said NOT attestation-ready. And
because pacta is not part of this estate, the skip branch is the ONLY branch a
third party ever takes: for everyone but the author the button always returned
0 without ever checking definition fidelity. Reproduced here before fixing —
PACTA_SRC=/nonexistent ./check.sh printed "FIDELITY NOT RUN" and exited 0.
An exit code is what programs read. The contract is now:
fidelity ran exit 0 ATTESTATION GREEN
SKIP_FIDELITY=1 exit 3 explicit opt-out, distinguishable, not success
pacta absent exit 1 nobody opted out; a real failure to establish
the property the button exists for
All three verified. The self-tests are unaffected: every SKIP_FIDELITY case
already expected a non-zero exit and asserts on a diagnostic from an earlier
phase, and the control compiles modules directly rather than invoking check.sh.
29 assertions across the three self-tests, all green.
`pacta-subject-unpinned` — HIGH, GPT-5.6 round 8.
Phase 4 compared this repository's Lean definitions against "the deployed
verifier" by importing whatever sat at $PACTA_SRC — no repository, no commit,
no clean state, no hashes. It pinned the fidelity OUTPUTS while leaving the
SUBJECT anonymous, so any program producing the same finite family of answers
passed, and the recorded result named no version of the thing it agreed with.
fidelity/pacta_pin.py pins the transitive set of pacta modules the harness
ACTUALLY LOADS — discovered by importing its entry point and reading
sys.modules, a membership property rather than a directory glob. A glob would
pin files the comparison never touches and miss anything loaded from elsewhere;
this estate has been bitten by name-shaped measurement before. Five modules at
pacta cd3b1bc — the same checkout the reviewer independently recorded.
Negative-tested, all three rejected by name: tampered bytes, a module loaded
but absent from the pin, and the pin file deleted. Refusing to pin a dirty
pacta tree is also enforced — a pin taken over uncommitted edits names a
subject nobody else can obtain.
PACTA-PIN.sha256 joins HARNESS_EXTRA. It is not executable, so it would
otherwise have sat outside the harness set, and a subject pin an attacker may
rewrite pins nothing — the same shape as the forgeable .audit-basis that
remains open as `auditonly-basis-forgeable`.
This does not widen the claim: byte identity of a source tree is not proof the
deployed service runs it, and finite-family agreement is not extensional
equality. It names the subject.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
|
|||
| 6212aa1624 |
Round-7 F2: account for every constant the kernel sees
THE DEFECT, demonstrated by a reviewer with a working payload. The driver
surface is reported by an `#eval` inside Proofs/Inventory.lean. Anything
declared AFTER that command is in the compiled object file but does not exist
in the environment while the command runs, so the walk cannot see it. The
reviewer appended
def bait : Nat := 0
theorem bait.smuggled : forall n : Nat, n + 0 = n := ...
re-pinned, and ran the button. It printed "no axiom, no claim", the statement
digest was BYTE-IDENTICAL to the clean tree, and the run went green — while a
theorem with a real axiom cone sat in the environment. In neither walk: not
corpus, because an instrument is not corpus; not driver surface, because it
post-dates the emitter. In no allowlist. Pinned by nothing.
This repository also had no kernel-side scan at all. Its axiom gate was a
source-text grep, evadable by a leading space — which its own selftest case 12
already exploited.
THE FIX, ported from the ed25519 forks:
· a kernel-side axiom-declaration gate that reads every compiled .olean via
readModuleData. It sees what was actually stored, regardless of
indentation, attributes, privacy, or where a declaration sits relative to
any #eval. Membership self-derives from the manifest and the module count
must match, so a deleted artifact cannot make the scan vacuous.
· the ACCOUNTING IDENTITY, as set containment:
every constant the kernel sees in corpus inventory union instrument surface
The two walks read ENVIRONMENTS; the gate reads OBJECT FILES. What a walk
cannot see because of where it sits in a file, the object file still holds.
That asymmetry is the entire content of this fix.
Compared as SETS deliberately. Counts cannot express the relation — an
object file may hold two physical copies of one lazily-materialised
equation lemma while an environment holds one constant per name — and
arithmetic between those views misled the ed25519 version twice before it
was stated as containment.
PLACEMENT differs from the forks, for a reason worth recording: there the
audit drivers are members of the compile manifest, so a gate beside the
compile phase finds them. Here AxiomCheck is compiled by Phase 3 and Inventory
by Phase 3b, so an earlier gate fails on a missing artifact — which it did,
correctly, on the first port. It runs inside Phase 3b, because the instruments
are exactly what it must see.
VERIFIED with the reviewer's own payload, which previously went green:
ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for:
bait
bait.smuggled
selftest_audit.sh: 14 attack cases -> 15. Note in the new case, because it
cost two iterations: `theorem bait.smuggled : True := trivial` does NOT
exercise this gate — Phase 1's stub audit greps for `: True :=` and catches it
first. Real defence in depth, but the naive payload never reaches the gate
under test, so the case uses the reviewer's original.
Two residues fixed while adding it, both the same shape: a case that was last
when written, leaving state the next case inherits. Case 13 restored
AxiomCheck.lean but not its pin; case 9 left its rogue gen file. Fixed at the
point of use so each case keeps testing what it tested before.
Button green (234 declarations across 11 modules, all accounted for),
15/15 self-test green, ATTESTATION GREEN with fidelity.
|
|||
| 25699a9cf7 |
Phase 0a: purge compiled artifacts before compiling
P0-a was applied to the four ed25519 repositories on 2026-07-30 and never here. Found by the control repo's capability matrix, which asks the property rather than looking for a phase by name. The finding that made it matter there applies verbatim: a verification that never cleans up cannot distinguish "these proofs check" from "these proofs check GIVEN WHATEVER IS LYING AROUND". Compiled artifacts are gitignored, so no `git status` can show a reader that a verdict rested on an object from an earlier run of a different script. This repository has no --audit-only mode, so the purge is unconditional. Button green (80s) and the 14-case self-test green after the change. |
|||
| 9c78ce88ae |
P2-b: close classes 9 and 15 — the instruments, and the places nothing looked
CLASS 15 — a Lean file where no phase was looking. The dead-file scan read Proofs/*.lean and gen/LTLAcc/*.lean and nothing else. A module at the verification root, or under any other gen/ subdirectory, was neither compiled nor rejected — while remaining importable by name, since LEAN_PATH contains both roots. That is a source of the corpus that no phase reads and no pin covers, which is exactly what the dead-file gate exists to forbid; it was simply looking in two places instead of everywhere. Now nothing may live in either root but the two enumerated sets. CLASS 9 — the instruments' own declaration surface. AxiomCheck.lean and Inventory.lean perform the audit and are therefore not corpus, so nothing inventoried what THEY declare. Inventory.lean now walks both: AxiomCheck by module index, and itself as the module still being elaborated, whose declarations are the ones the environment reports with no originating module. That is what makes the inventory cover the instrument that produces it rather than exempting itself. The policy is not "declare nothing" — this file legitimately declares its machinery. It is that an instrument may declare only inert definitions. An axiom here would widen the trusted base without appearing in any certificate's cone; a theorem here would be a claim no certificate covers and no allowlist pins. A flat ban on theorems was WRONG and was measured to be wrong: defining a function by well-founded recursion makes the elaborator emit its own obligations, and axiomCone._proof_1 rejected this very file. The distinction that holds is whether a theorem is a claim someone wrote or an artefact of a definition declared alongside it — an artefact's name extends the name of a constant declared with it. Observed surface: 18 declarations, 16 def and 2 generated obligations, no axiom, no standalone claim. The drivers are byte-pinned already, so this does not pin WHICH definitions they contain — that would add a thing to maintain without adding a thing to catch. It adds the property byte-pinning cannot give: that no instrument declares an axiom or a claim, whatever its bytes are. selftest_audit.sh: 10 cases -> 14. Case 12 uses an INDENTED axiom, because Phase 1's source grep catches an unindented one and the point is to reach the kernel-side walk standing behind it. TWO DEFECTS IN THE TEST HARNESS, found while adding the cases. · The scratch tree copied verification/ only, but the button also reads README.md and STATEMENT-MAP.md from the repository root. check.sh therefore ALWAYS died in Phase 3c in the scratch tree, which made every `if check.sh; then <attack not caught>` guard unfirable — check.sh could not pass in there even with no attack at all. Only the diagnostic greps were doing any work. The documents are now copied, and the negative test below proves the guard is live: with the driver-surface check disabled, check.sh PASSES a tree whose inventory driver declares `axiom driver_cheat : False`. · Case 9 was the last case when it was written and left its rogue gen file in place. Harmless then; the new cases inherited it. Cleaned up between the blocks rather than inside case 9, so that case still tests what it did. Also fixed while here: Phase 3b compared the compile manifest against Inventory.lean by grepping the WHOLE FILE for a backticked module name, so prose counted — a doc comment naming a module broke the count, and in the other direction a doc mention of a module missing from the array would have satisfied the presence check and hidden the omission. It now reads the arrays. Both new gates negative-tested by removal. Button green, self-test green. |
|||
| 8530cc73f4 |
verification: pin the harness, audit drivers and policy files (P1-c)
This repository has the estate's strongest gates, which makes them the most valuable to switch off. Until now every one of them was executed by scripts that nothing pinned. Phase 0c requires every harness file to match HARNESS.sha256 — 15 files: check.sh, lean-guard, inventory_gate.sh, run_bare.sh, all three self-tests, both audit drivers (Proofs/Inventory.lean, Proofs/AxiomCheck.lean), the policy tables (inventory-allowlist.txt, AUDIT-MANIFEST.txt), the toolchain pin, the fidelity harness and its Python transcription, and the extracted model. WHICH files must be pinned is policy and lives in check.sh, never in the map being consulted: the required set is derived from the filesystem (the executable bit, plus gen/**.lean, plus an explicit list for the rest), so deleting a pin entry is a set mismatch rather than a silent un-pinning. gen/LTLAcc/HashExternal.lean was previously bound by nothing at all — it was compiled and trusted. It is now pinned, and the derivation is by set, so a new model file fails closed. selftest_audit.sh case 9 is split rather than relabelled. Phase 0c now catches an unpinned rogue gen module BEFORE the dead-file gate runs, so asserting only the new diagnostic would have quietly retired the dead-file gate from the test suite. 9a asserts the harness-set mismatch on the unpinned file; 9b pins it — an author who added it deliberately — and asserts Phase 2 still dies with DEAD FILE (gen). Ten cases now, all defeated. KNOWN-GAPS and the trusted base record the circularity plainly: an author who edits a script and refreshes its pin in one commit passes every phase. The pin removes the silent path, not the possibility. Review at the pinned commit remains the consumer's protection. Verified green after the fix: button (75s), harness self-test, binding self-test, and the ten-case audit self-test. ATTESTATION GREEN (Lean + fidelity), all fidelity case counts identical to the pre-change run. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> |
