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

20 lines
1.6 KiB
Text
Raw Permalink Normal View History

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>
2026-07-29 18:13:21 +00:00
e7d422f0be9a9e6f5465058292e30c711d52856428da2b01c470a57ec181540c AUDIT-MANIFEST.txt
verification: separate the two accounting questions (round-9 review, Claude N2) Phase 2c-accounting asked one question with a name-keyed identity: is every kernel constant covered by the corpus inventory or the instrument surface? Keying on the name alone conflates that with a second, different question -- does the kernel attribute a declaration to the same module the walk does? Pair-keying the identity (module|name) was the obvious fix and is wrong: it fails on legitimate per-module duplicates. Lean materialises equation lemmas lazily, so each module forcing an unfold gets its own copy in its object file (GPT-5.6 round-7 F8). Those records differ from the walk only in module attribution, and every one of their names is accounted for elsewhere. So the block now asks both questions and reports them separately: coverage stays name-keyed and fail-closed, module attribution is counted and printed rather than suppressed. A divergence is now visible instead of either passing silently or failing for the wrong reason. The accumulator declines the second question and says why: its INV rows carry no module column (4 fields), so its records cannot be compared as pairs at all. Gating on the field count rather than on the row tag -- the shape of the record, not the spelling of its label. Adding that column is the open follow-up; until then the identity there is name-keyed only, which is weaker and now says so. Certified by the round-14 sweep: 50/50 green across all six repositories, both buttons and every self-test. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-04 01:17:05 +00:00
8d72867f96188806618be221ef6e66ff221c0bd011b8f73516ae804a5f77a24f check.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
90fcad217c7b6507abecf37a41d57149f06a8955a72e60dc03616933f981ed6b driver-allowlist.txt
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>
2026-07-29 18:13:21 +00:00
070147e2667053bd5d5e1174b969fc6c91bfcf15ded1a5bff57754e15f416885 fidelity/lean_defs.py
accumulator: a run that is not attestation-ready must not exit 0, and must name its subject Two round-7/8 findings, both closed here. `acc-exit0-fidelity` — CRITICAL, raised INDEPENDENTLY by both reviewers (Claude F1, GPT-5.6 F10) and lost from the round-8 work list by the F-number collision the finding register now prevents. check.sh emitted a careful pair of markers — ATTESTATION GREEN only when fidelity actually ran — and then returned 0 either way. The marker discipline was right; the exit code contradicted it. A caller doing the obvious thing ./check.sh && append read success from a run whose own last line said NOT attestation-ready. And because pacta is not part of this estate, the skip branch is the ONLY branch a third party ever takes: for everyone but the author the button always returned 0 without ever checking definition fidelity. Reproduced here before fixing — PACTA_SRC=/nonexistent ./check.sh printed "FIDELITY NOT RUN" and exited 0. An exit code is what programs read. The contract is now: fidelity ran exit 0 ATTESTATION GREEN SKIP_FIDELITY=1 exit 3 explicit opt-out, distinguishable, not success pacta absent exit 1 nobody opted out; a real failure to establish the property the button exists for All three verified. The self-tests are unaffected: every SKIP_FIDELITY case already expected a non-zero exit and asserts on a diagnostic from an earlier phase, and the control compiles modules directly rather than invoking check.sh. 29 assertions across the three self-tests, all green. `pacta-subject-unpinned` — HIGH, GPT-5.6 round 8. Phase 4 compared this repository's Lean definitions against "the deployed verifier" by importing whatever sat at $PACTA_SRC — no repository, no commit, no clean state, no hashes. It pinned the fidelity OUTPUTS while leaving the SUBJECT anonymous, so any program producing the same finite family of answers passed, and the recorded result named no version of the thing it agreed with. fidelity/pacta_pin.py pins the transitive set of pacta modules the harness ACTUALLY LOADS — discovered by importing its entry point and reading sys.modules, a membership property rather than a directory glob. A glob would pin files the comparison never touches and miss anything loaded from elsewhere; this estate has been bitten by name-shaped measurement before. Five modules at pacta cd3b1bc — the same checkout the reviewer independently recorded. Negative-tested, all three rejected by name: tampered bytes, a module loaded but absent from the pin, and the pin file deleted. Refusing to pin a dirty pacta tree is also enforced — a pin taken over uncommitted edits names a subject nobody else can obtain. PACTA-PIN.sha256 joins HARNESS_EXTRA. It is not executable, so it would otherwise have sat outside the harness set, and a subject pin an attacker may rewrite pins nothing — the same shape as the forgeable .audit-basis that remains open as `auditonly-basis-forgeable`. This does not widen the claim: byte identity of a source tree is not proof the deployed service runs it, and finite-family agreement is not extensional equality. It names the subject. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-02 19:40:35 +00:00
9661bc2d33e907453ab4378da918589a709127b2e117ef1fd578d4e0472edf87 fidelity/pacta_pin.py
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>
2026-07-29 18:13:21 +00:00
5d82462a002ac9fc782e95afe78b7719ba64b6410b5d2bfa620fe5317367dbf2 fidelity/run_fidelity.py
503babb3f4e6aff82ebd59e8752469ecd60fba440ed3b11b3f97c2b655fbd9bf gen/LTLAcc/HashExternal.lean
f1eb5cdd158e30df14c59065fe2050448c77b5262b282208fa831d050f6b6a71 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
d628cc64efe920304f4ad8319d9b880a942abb6d850f4022fa1a26af7e8c34a1 inventory_gate.sh
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>
2026-07-29 18:13:21 +00:00
736ea4be712e1b5bcda10ecb466f0dec7008a2a36eabdfd77563976299c43cce lean-guard
ce4c4e3d87434b9663f46de25ce34b48a0cf0d392e0a320a0787b4674a2d7b61 lean-toolchain
fidelity: deliberate re-pin of the pacta subject (cd3b1bc -> a036624) The round-16 sweep went 49 GREEN, 1 RED, and the RED was this repository's Phase 4 refusing to run: PACTA SUBJECT MISMATCH, signing.py and transparency.py differing from the pin. That is pacta-subject-unpinned (round-8, GPT-5.6) firing on its first genuine drift — the gate built so that fidelity could never again count agreement with an unnamed program. The drift is known and intended: pacta 5e35a53 anchored the signer path to the package (register: signer-backend-depends-on-cwd) and a036624 added the additive slh_dsa block to make_signed_tree_head (operator decisions 2026-08-06). Re-pinned deliberately with pacta_pin.py --write: 5 modules at pacta a036624. PACTA-PIN.sha256's own entry in HARNESS.sha256 updated. Full instrument set re-run green at the re-pinned state: check.sh 92s, selftest_audit 280s, selftest-harness 0s, selftest_statements 38s. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-06 23:41:18 +00:00
127fecf2a6938ec24dcc7604756b6b78fcc9ed9343bab7ec9e6bb03b3a9ca0be PACTA-PIN.sha256
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>
2026-07-29 18:13:21 +00:00
eda93f520546a692926b2a46bcb79332e1795879e5083327a8bf2404aca5cf87 Proofs/AxiomCheck.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
82d41c634a2e9adfc2cc74c202d025e57411687796f820765d45608f3fb4cb20 Proofs/Inventory.lean
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>
2026-07-29 18:13:21 +00:00
0b8a0fc6947af1d1e600a756eb2b07dc88d189b21df3220c4501a41be8b33f1e run_bare.sh
Round-7 F2: account for every constant the kernel sees THE DEFECT, demonstrated by a reviewer with a working payload. The driver surface is reported by an `#eval` inside Proofs/Inventory.lean. Anything declared AFTER that command is in the compiled object file but does not exist in the environment while the command runs, so the walk cannot see it. The reviewer appended def bait : Nat := 0 theorem bait.smuggled : forall n : Nat, n + 0 = n := ... re-pinned, and ran the button. It printed "no axiom, no claim", the statement digest was BYTE-IDENTICAL to the clean tree, and the run went green — while a theorem with a real axiom cone sat in the environment. In neither walk: not corpus, because an instrument is not corpus; not driver surface, because it post-dates the emitter. In no allowlist. Pinned by nothing. This repository also had no kernel-side scan at all. Its axiom gate was a source-text grep, evadable by a leading space — which its own selftest case 12 already exploited. THE FIX, ported from the ed25519 forks: · a kernel-side axiom-declaration gate that reads every compiled .olean via readModuleData. It sees what was actually stored, regardless of indentation, attributes, privacy, or where a declaration sits relative to any #eval. Membership self-derives from the manifest and the module count must match, so a deleted artifact cannot make the scan vacuous. · the ACCOUNTING IDENTITY, as set containment: every constant the kernel sees in corpus inventory union instrument surface The two walks read ENVIRONMENTS; the gate reads OBJECT FILES. What a walk cannot see because of where it sits in a file, the object file still holds. That asymmetry is the entire content of this fix. Compared as SETS deliberately. Counts cannot express the relation — an object file may hold two physical copies of one lazily-materialised equation lemma while an environment holds one constant per name — and arithmetic between those views misled the ed25519 version twice before it was stated as containment. PLACEMENT differs from the forks, for a reason worth recording: there the audit drivers are members of the compile manifest, so a gate beside the compile phase finds them. Here AxiomCheck is compiled by Phase 3 and Inventory by Phase 3b, so an earlier gate fails on a missing artifact — which it did, correctly, on the first port. It runs inside Phase 3b, because the instruments are exactly what it must see. VERIFIED with the reviewer's own payload, which previously went green: ACCOUNTING FAILED: the kernel holds constants that neither walk accounts for: bait bait.smuggled selftest_audit.sh: 14 attack cases -> 15. Note in the new case, because it cost two iterations: `theorem bait.smuggled : True := trivial` does NOT exercise this gate — Phase 1's stub audit greps for `: True :=` and catches it first. Real defence in depth, but the naive payload never reaches the gate under test, so the case uses the reviewer's original. Two residues fixed while adding it, both the same shape: a case that was last when written, leaving state the next case inherits. Case 13 restored AxiomCheck.lean but not its pin; case 9 left its rogue gen file. Fixed at the point of use so each case keeps testing what it tested before. Button green (234 declarations across 11 modules, all accounted for), 15/15 self-test green, ATTESTATION GREEN with fidelity.
2026-08-02 00:51:55 +00:00
473e2463d9c26653c8435ad6758044742f200eb13ea0db4b8f076466c08bd87a selftest_audit.sh
verification: guard the accumulator's two lifts (port lift-guard, assert on the payload) The four forks ship lift-guard.sh and call it from eight files each. This repository had no lift-guard.sh at all and called it zero times, while lifting Phase 0c (selftest-harness.sh) and Phase 3d (selftest_statements.sh). Its lifts got a line-count sanity check and nothing else — no analysis of which variables the payload READS against which the driver DEFINES, and after yesterday's fix no errexit check either. It was the one place that class could still recur. A SECOND defect surfaced while porting, and it is the more interesting one. Both lifts assembled the driver inline, with no payload file anywhere: { echo 'set -euo pipefail'; echo "HERE=..."; sed -n '...' check.sh } > DRIVER if [ "$(wc -l < "$DRIVER")" -lt 40 ]; then ... refuse ... so the size check measured the CONCATENATED DRIVER — bindings included. A lift that recovered almost nothing still cleared the threshold on the strength of the lines the test itself prepended. That is exactly the defect round-7 lift-guard-payload-assert reported and that the forks closed with the words "all six lift sites now assert on payload.sh". Six counted the forks. These two were never in the count, so a finding recorded as closed was measuring the wrong population — the same error this estate keeps finding in new costumes. Both sites now write payload.sh / payload3d.sh and assert on those. lift-guard.sh is byte-identical to the forks' (4f61c113). It is executable, so this repository's own self-deriving Phase 0c rule required a pin before it would run at all: required set == pinned set, verified. WIRING PROVEN RATHER THAN ASSUMED. With lift-guard.sh stubbed to exit 1, each self-test halts AT the guard, naming its phase, before a single attack case runs. Guard restored, pins re-verified. Certified: button + all three self-tests GREEN (check.sh 86s, selftest_audit 258s, selftest-harness 1s, selftest_statements 34s). The other five repositories are unchanged from the tree round-15 certified 50/50 and were not re-run; this commit does not claim they were. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
2026-08-04 11:39:19 +00:00
733eb2cf4eaf9101433d75dbedfc45681cff44e1dbfdc841e6b9dba350ef1570 selftest-harness.sh
c85d7a0fc39fbf06ec2c85d2f42a65813c475cae7cf60e6d140948215c62eabc selftest_statements.sh
4f61c1135f8afc615e686bd267a062229bf349416caebe070eafca510036d1a4 lift-guard.sh
Reference in a new issue Copy permalink