mirror of
https://github.com/saymrwulf/ltl-accumulator-verified.git
synced 2026-09-03 19:53:48 +00:00
4 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> |
|||
| 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. |
|||
| b575e857e3 |
verification: bind statements and specification bodies (P1-a); un-stale the fidelity pin
STATEMENT BINDING (Phase 3d). The coverage gate pins every constant's name,
kind and axiom cone, both directions, and none of selftest_audit.sh's nine
attacks defeat it. It is nevertheless blind to what a declaration SAYS — and
that is demonstrated here rather than argued:
Wrapping one branch of `LTLAcc.pinAccept`'s body in `id (…)` is
definitionally equal. Every downstream proof still compiles. The name, the
kind, the type and the axiom cone are unchanged. The inventory gate reports
"222 constants, environment == allowlist" — GREEN.
That edit is harmless by construction; the point is that nothing stood between
it and a genuinely vacuous redefinition of a specification. Proofs/Inventory.lean
now also emits, for every inventoried constant, its fully-elaborated TYPE, and
for every definition its fully-elaborated BODY — 266 lines over 222 constants.
Proof terms are deliberately absent: by proof irrelevance a theorem's content
is its statement. check.sh Phase 3d binds the SHA-256 and the block is
committed as AUDIT-MANIFEST.txt so a mismatch is DIFFED, not merely reported.
The existing gate is untouched, per the standing rule that the port flows FROM
this repo, not to it: INV lines are byte-identical, inventory_gate.sh is
unchanged, and all nine of its attacks still fail as before.
selftest_statements.sh replays the defeq edit as case 1, asserting BOTH that
the coverage gate passes it and that Phase 3d catches it — so if the coverage
gate ever grows to see this, the test says so instead of quietly re-labelling.
Cases 2-4 cover a hand-edited committed block, a truncated block, and a
constant inventoried without a statement.
FIDELITY PIN (unrelated, found while running the button). Phase 4 had been
failing since 2026-07-23: LIED_PIN_DIV expected 3,867 divergences between the
Lean model and the deployed consistency verifier, and observed 0. Cause is
pacta ddbb5a4, which restored the RFC 9162 2.1.4.2 Step-7 terminal `sn == 0`
condition; that one conjunct removes every divergence in the pinned
73,573-case family. KNOWN-GAPS gap 14 already recorded the closure on the day
it landed — only this constant was stale, so the button had been red for five
days with nobody running it. The pin now reads 0 with the history in a comment.
Nothing about the paper, public log entry 13, or the attested commit
|
|||
| 9972ab4198 |
Review round 3: environment-derived audit surface, self-contained kit
Round-2 external reviews (GPT-5.6 + second Claude) converged on the coverage gate being evadable (H1/NEW-1); GPT additionally proved the kit's fidelity target could not run (H2) and the namespace-collision attack that defeats any source-regex fix. This round adopts GPT's required correction in full: - Proofs/Inventory.lean: declaration inventory read from the compiled Lean environment — every constant of every corpus module, fully qualified, unfiltered (compiler auxiliaries and _private mangles pinned too), with kind and axiom cone; own cone walker cross-checked in-process against core collectAxioms (hard error on divergence). - verification/inventory-allowlist.txt: all 218 constants pinned. - inventory_gate.sh: fail-closed diff both directions (UNCLASSIFIED / STALE), INV-COUNT truncation guard, exactly-one-axiom invariant. - check.sh Phase 3b rewritten around the gate + manifest⇔inventory drift checks + CONES⇔inventory cone cross-check (two independent computations must agree). EXCLUDE table gone (sha256/Bytes are ordinary audited entries now). - selftest_audit.sh: 9 adversarial cases against the production gate (attributed/indented/private/instance, namespace collision, smuggled axiom, deleted decl, unmanifested Proofs/ and gen/ modules) + positive control — all defeated (GPT release condition 2). - M1: recursive orphan-olean guard (caught a stray dev artifact on its first run), gen/ dead-file check, corpus-wide single-axiom pin. - L1/NEW-2: acceptIncl_sound drops the redundant hm (derived from hacc.1); cone unchanged. - M2/M3: STATEMENT-MAP counts 230,271/230,016; non-vacuity guard wording narrowed to what the guards actually certify. - README layer table: stale L4/pin-store rows fixed (missed by both round-2 reviewers AND the round-2 revision — found in self-review). - KNOWN-GAPS 12 (audit-gate lineage + residual limits), 13 (round-2 kit target not self-contained); gap 2 count fixed. - RESPONSE-TO-REVIEWERS.md: round-3 disposition of every finding. Kit round 3 additionally ships the complete stdlib-only import closure of pacta.transparency (content-addressed vs pacta 3d81d53), the clean-extraction fidelity transcript (exit 0, 230,271+230,016, zero mismatches), the ATTESTATION GREEN check.sh transcript, and the self-test transcript. The live LTL remains untouched (12 leaves, root bcd15f9d…); attestation stays blocked pending ePrint decision + author review + explicit operator order. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> |
