mirror of
https://github.com/saymrwulf/ltl-accumulator-verified.git
synced 2026-09-06 20:20:48 +00:00
5 commits
| Author | SHA1 | Message | Date | |
|---|---|---|---|---|
| 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> |
