diff --git a/KNOWN-GAPS.md b/KNOWN-GAPS.md index 2d4da14..eb2334e 100644 --- a/KNOWN-GAPS.md +++ b/KNOWN-GAPS.md @@ -9,7 +9,8 @@ list is COMPLETE, not merely that the items are acceptable. 2. **No consistency-completeness theorem** (honest ConsRec acceptance). Matches the paper (its Theorem 1 is inclusion-only); honest consistency behavior is covered by the fidelity harness's honest - cases (164,224-case agreement with the deployed verifier). + cases (within the 230,016-case consistency agreement with the + deployed verifier). 3. **Lemma 2 is mechanized as specializations, not as one general theorem.** The paper's Lemma 2 is a single statement quantified over an abstract hash-fold `F` and a connected subtree `S`. The corpus has @@ -58,3 +59,21 @@ list is COMPLETE, not merely that the items are acceptable. the out-of-range families (`m ≥ n`). `Root` alone still accepts out-of-range `m`; that is by design (it is the reconstruction, not the accept predicate). +12. **Audit-gate lineage** (candor; was round-2 GPT H1 / Claude NEW-1, + both round-1 "fail-closed" claims were overclaims). The round-2 + coverage gate enumerated declarations with a source regex and was + evadable (attributes, indentation, private/protected, `instance`, + nested-namespace basename collisions). Round 3 replaced it with an + environment-derived inventory (`Proofs/Inventory.lean` + + `inventory-allowlist.txt`, fully-qualified names, no filtering) and + `selftest_audit.sh`, which runs the published evasion table plus a + namespace collision, an axiom smuggle, a stale-entry case, and two + unmanifested-module cases against the exact production gate. + Residual honesty: the inventory sees what the compiled environment + contains; it cannot see source that is never compiled (which the + dead-file checks cover) or defeat a hostile Lean toolchain. +13. **Review-kit fidelity target was not self-contained in round 2** + (GPT H2: missing load-time imports made `run_fidelity.py` unrunnable + from the kit). Round 3 ships the complete stdlib-only import closure + of `pacta.transparency`, content-addressed against pacta commit + `3d81d53`, plus the clean-extraction transcript with exit code. diff --git a/README.md b/README.md index b910657..158677b 100644 --- a/README.md +++ b/README.md @@ -10,10 +10,13 @@ the same discipline as the four `*-ed25519-verified` subject corpora. All paper-§10 mechanization targets are kernel-checked; the audit surface is defined and green (`verification/check.sh`, exit 0). See [STATEMENT-MAP.md](STATEMENT-MAP.md) for the paper↔Lean review surface and -[KNOWN-GAPS.md](KNOWN-GAPS.md) for the honest scope ledger. Revised after review round 1 (GPT-5.6 + second Claude): audit surface -now fail-closed enforced, acceptIncl named, fidelity families extended -(230,271 / 230,016), docs reconciled. No changes -until the external review round (second model instance + GPT + author) +[KNOWN-GAPS.md](KNOWN-GAPS.md) for the honest scope ledger. +Revised after review round 1 (GPT-5.6 + second Claude) and round 2: +the audit surface is now an environment-derived inventory +(`Proofs/Inventory.lean` + pinned allowlist, self-tested by +`selftest_audit.sh`), the review kit's fidelity target is +self-contained, `acceptIncl` routes Theorems 1–2, fidelity families +extended (230,271 / 230,016). No changes until the external review completes. The finished certificates' attestation into the LTL is a separate, explicitly-authorized operator decision. @@ -21,13 +24,12 @@ separate, explicitly-authorized operator decision. |---|---|---| | L1 | bytes, hleaf/hnode, domain separation (Lemma 1) | **done** (domsep: axiom-free) | | L2 | MTH, Root, ConsRec definitions + termination | **done** (cones: propext, LTLAcc.sha256, Quot.sound) | -| L3 | inclusion completeness (Theorem 1) | **done** (incl_complete: propext, Classical.choice, LTLAcc.sha256, Quot.sound) | -| L4 | frontier binding content (Lemma 2) | **inlined in the extractor walk** (extractIncl); standalone receipt-uniqueness theorem queued for S4 restoration in extractor form | -| L5 | inclusion soundness = EXPLICIT extractor `extractIncl` (Theorem 2) **done, non-vacuous** | -| L6a | descent extractor `extractMTH` (Theorem 3 step 3 = Lemma 2, WHOLE-TREE instance) **done, non-vacuous** | -| — | Lemma 2, PATH instance (receipt-uniqueness of `Root`): deleted with the vacuous `root_binding` in S3.5 and **not yet restored**; optional, not needed for Theorem 3 | -| L6b | **Theorem 3 (consistency soundness) DONE** — consRecBinding (steps 1-2) is the kernel-checked link between ConsRec acceptance and extractConsNode's output; extractCons/extractCons_correct (assembly, joins extractMTH); non-vacuity pinned | -| L6 | pin-store state machine safety (Proposition 1) | pending | +| L3 | inclusion completeness (Theorem 1) + named acceptance `acceptIncl` | **done** (incl_complete: propext, Classical.choice, LTLAcc.sha256, Quot.sound) | +| L4 | frontier binding content (Lemma 2) | **done as specializations** — inlined in the extractor walk (`extractIncl`), whole-tree (`extractMTH`), ConsRec (`consRecBinding`); the standalone `Root` receipt-uniqueness instance was deleted with the vacuous `root_binding` in S3.5 and deliberately NOT restored (optional, unused — KNOWN-GAPS gap 3) | +| L5 | inclusion soundness = EXPLICIT extractor `extractIncl` (Theorem 2) | **done, non-vacuous** | +| L6a | descent extractor `extractMTH` (Theorem 3 step 3 = Lemma 2, whole-tree instance) | **done, non-vacuous** | +| L6b | Theorem 3 (consistency soundness): `consRecBinding` (steps 1–2) + `extractCons`/`extractCons_correct` (+ `_paper` at the paper's exact quantifiers) | **done, non-vacuous** | +| L6c | pin-store state machine safety (Proposition 1): `pinAccept_monotone`, `pin_prefix_correct`, `fork_distinct` | **done, non-vacuous** (per-step; multi-step chain = gap 7) | ## Discipline (identical to the subject corpora) diff --git a/RESPONSE-TO-REVIEWERS.md b/RESPONSE-TO-REVIEWERS.md new file mode 100644 index 0000000..5c51068 --- /dev/null +++ b/RESPONSE-TO-REVIEWERS.md @@ -0,0 +1,136 @@ +# Response to reviewers — round 3 + +Corpus: `ltl-accumulator-verified`. Round-2 reviews received against the +round-2 freeze `260ad64` (GPT-5.6 second adversarial review; second +Claude round-2 findings). Every finding was independently re-verified +against the corpus before any change; all confirmed findings are fixed +in this freeze. No theorem statement changed except the one interface +tightening both reviewers requested (L1/NEW-2). + +## Disposition of round-2 findings + +### GPT H1 / Claude NEW-1 — coverage gate evadable (CONFIRMED, fixed structurally) + +Both reviewers were right, and GPT's namespace-collision attack +(`LTLAcc.Hidden.MTH` classified against `CONES[LTLAcc.MTH]`) showed that +regex hardening (Claude's proposed fix) would not have closed the class. +We adopted GPT's required correction in full — the inventory is now +derived from the Lean environment, not from source: + +- **`Proofs/Inventory.lean`** imports every corpus module and emits + EVERY constant whose originating module is a corpus module: fully + qualified name, declaration kind, and axiom cone. There is **no + filtering** — compiler-generated auxiliaries and `_private.*` mangles + are emitted and pinned too, so there is no name shape that can hide. + A corpus module missing from the import list is an elaboration error. +- The axiom cone is computed by our own walker AND cross-checked + in-process against core `collectAxioms` (the machinery `#print axioms` + uses) for every constant — divergence is a hard error. (This caught a + real toolchain subtlety during development: `ConstantInfo.value?` + returns `none` for theorems on 4.30.0-rc2, which would have silently + truncated cones; the direct constructor match avoids it, and the + cross-check would have refused to ship it.) +- **`verification/inventory-allowlist.txt`** pins all 218 constants; + **`inventory_gate.sh`** diffs environment vs allowlist fail-closed in + BOTH directions (UNCLASSIFIED / STALE), requires the INV-COUNT + trailer (a truncated Lean run cannot pass as an empty diff), and + asserts the whole corpus contains exactly one axiom-kind constant: + `LTLAcc.sha256`. +- check.sh Phase 3b additionally verifies: the inventory's module list + == the compile manifest (both directions), every CONES entry appears + in the allowlist **with an identical cone** (two independent cone + computations must agree), and every CONES entry is queried by + AxiomCheck. +- **GPT release condition 2 (adversarial tests) is met by + `verification/selftest_audit.sh`**, which attacks the exact production + gate: attributed, indented, private, and instance declarations, the + nested-namespace basename collision, a smuggled axiom, a deleted + declaration (STALE direction), and unmanifested `Proofs/` and `gen/` + modules through the full check.sh — plus a positive control so the + self-test cannot pass vacuously. Transcript in the kit + (`selftest-transcript.txt`). + +### GPT H2 — fidelity target could not run (CONFIRMED, fixed) + +Reproduced exactly (`ModuleNotFoundError: pacta.postquantum`). The +round-3 `pacta-fidelity-target` ships the complete **load-time import +closure** of `pacta.transparency` (`__init__`, `transparency`, +`postquantum`, `signing`, `yamlio`) — all stdlib-only, so a bare +Python 3 runs it with no pip installs — content-addressed in +`MANIFEST.sha256` against pacta commit `3d81d538…` with verification +instructions (`TARGET-PROVENANCE.md`). The kit includes the complete +terminal transcript AND exit code of `run_fidelity.py` executed from a +clean extraction: exit 0, `230,271 + 230,016`, zero mismatches +(`fidelity-clean-run-transcript.txt`), plus the full green `check.sh` +transcript ending in `ATTESTATION GREEN` with fidelity not skipped +(`check-transcript.txt`) — GPT release conditions 3 and 5. + +### GPT M1 — audit narrower outside Proofs/ (CONFIRMED, fixed) + +- Orphan-olean guard is now recursive over the whole tree (it caught a + stray development artifact on its first run). +- gen/ has the same unmanifested-source ("dead file") check as Proofs/. +- The axiom surface is pinned corpus-wide twice: textually (exactly one + `axiom` line under gen/, none under Proofs/) and semantically (the + inventory admits exactly one axiom-kind constant anywhere). +- Declaration discovery under gen/ now goes through the environment + inventory like everything else. + +### GPT M2 — stale fidelity counts in STATEMENT-MAP (CONFIRMED, fixed) + +The row now reads 230,271 + 230,016 with the expanded families named. +Process note: the round-2 Claude review certified this row as already +fixed; it was not. Consistent with this project's experience, "verified" +claims by reviewers are themselves re-verified now. + +### GPT M3 — "not choice-dischargeable" overclaims (CONFIRMED, fixed) + +STATEMENT-MAP now uses (essentially) GPT's safer wording: the guards +show each named extractor returns a non-collision on at least one +canonical honest input, ruling out the globally-inhabited-existential +degeneration; they do NOT establish logical dependence on every +hypothesis, nor exclude other classical arguments on restricted domains. + +### GPT L1 / Claude NEW-2 — redundant `hm` in `acceptIncl_sound` (CONFIRMED, fixed) + +The hypothesis is gone; the range fact is derived from `hacc.1`, so the +theorem is stated purely in terms of acceptance + wrong-leaf premise. +Cone unchanged (`propext, Classical.choice, LTLAcc.sha256, Quot.sound`), +re-verified by `#print axioms` and the inventory. + +### GPT ledger additions (adopted, as history) + +KNOWN-GAPS gains gap 12 (audit-gate lineage: the round-2 gate was +evadable, what replaced it, and the residual limits of an +environment-derived inventory — it cannot see never-compiled source, +which the dead-file checks cover, nor defeat a hostile toolchain) and +gap 13 (the round-2 kit's fidelity target was not self-contained). + +## Found in round-3 self-review (neither reviewer caught) + +- **README layer table was still stale at `260ad64`**: L4 carried + "queued for S4 restoration" and the pin-store row said "pending", + despite round-1 F2 being certified as fixed by the round-2 Claude + review. The table now matches the frozen state (all layers done, + L4 explicitly "done as specializations" per gap 3). +- KNOWN-GAPS gap 2 still cited the old 164,224 count; updated. + +## Round-2 Claude review, remaining notes + +NEW-1 was correct in direction; we implemented the stronger +environment-based fix rather than the proposed regex broadening, since +the namespace collision defeats any basename-keyed source scan. The +round-2 Claude claim that the fidelity harness was "confirmed green +against the real pacta code" was obtained by hand-stubbing the missing +modules — with the round-3 self-contained target, that result is now +reproducible by anyone from the kit alone. + +## What did NOT change + +All theorem statements and proofs except the `acceptIncl_sound` +signature tightening; the axiom boundary (single opaque `sha256`); the +pinned CONES table (59 entries, all cones byte-identical to round 2); +the fidelity counts. The live transparency log remains frozen at +12 leaves (root `bcd15f9d…`) and is untouched by this round; +attestation remains blocked pending the ePrint decision, author +review, and an explicit operator order. diff --git a/STATEMENT-MAP.md b/STATEMENT-MAP.md index c1809a0..a362426 100644 --- a/STATEMENT-MAP.md +++ b/STATEMENT-MAP.md @@ -25,7 +25,7 @@ mechanization to items i–v). | Prop 1(1) (pin monotonicity + prefix) | `pinAccept`, `pinAccept_monotone`, `pin_prefix_correct` | PinStore | sha256 (+choice) | | Prop 1(2), Merkle share | `fork_distinct` (different roots ⇒ different content); transferability = signature layer, out of scope | PinStore | sha256 | | non-vacuity guards (anti-pigeonhole) | `extractIncl_nonvacuous`, `extractMTH_nonvacuous`, `extractCons_nonvacuous`, `pin_prefix_nonvacuous` | Extract/Descent/Theorem3/PinStore | sha256 | -| definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 164,479 + 164,224 (paper's exact case set) | fidelity | (testing) | +| definition fidelity vs deployed verifier | `fidelity/` harness: MTH==merkle_root, Path==inclusion_proof, verifier agreement 230,271 inclusion + 230,016 consistency (paper's case set + out-of-range families m≥n, n₀>n₁, n₀=0; round-2 M2 fixed the stale pre-expansion counts here) | fidelity | (testing) | Note on "assumption-free" (paper §10(i)): `incl_complete`'s cone lists `LTLAcc.sha256`, but the theorem assumes **no property** of it — it @@ -37,11 +37,25 @@ Design invariant of every soundness statement: the collision is the output of a **named extractor function** and correctness is a claim about that output. A bare `∃ x y, x ≠ y ∧ sha256 x = sha256 y` is provable by pigeonhole alone (sha256 maps an infinite domain into the finite 32-byte -type), so it carries no cryptographic content; the guards above prove each -extractor's conclusion is *false* on honest inputs, hence not -choice-dischargeable. +type), so it carries no cryptographic content. What the guards certify +(precisely — round-2 M3): each named extractor does **not** return a +collision on at least one canonical honest input, which rules out the +degeneration where the conclusion is a globally inhabited bare collision +existential. They do NOT establish logical dependence on every listed +hypothesis, nor that no other classical argument could reach the +conclusion on some restricted domain. Audit surface (enforced by `verification/check.sh`, exit 0 = green): -every theorem/def under `Proofs/` (52) plus the two load-bearing `gen/` -instances; excluded by nature: the sanctioned axiom `sha256` (it *is* the -boundary) and `abbrev Bytes` (alias, no cone content). +the FULL compiled environment of the corpus modules — 218 constants, +read from the Lean environment by `Proofs/Inventory.lean` (fully +qualified names, kinds, axiom cones) and pinned in +`verification/inventory-allowlist.txt`, diffed fail-closed both +directions on every run (round-3 replacement for the round-2 source-regex +gate, which GPT H1 showed was evadable). The 59 human-reviewed statement +cones above are additionally checked via `#print axioms` and +cross-checked against the inventory's independently computed cones. +`verification/selftest_audit.sh` attacks the gate with nine injection +cases (attributed/indented/private/instance declarations, a nested +namespace reusing an audited basename, a smuggled axiom, a deleted +declaration, and unmanifested Proofs/ and gen/ modules) — each must +fail the exact production gate. diff --git a/verification/Proofs/Extract.lean b/verification/Proofs/Extract.lean index 6764d78..bd2efc9 100644 --- a/verification/Proofs/Extract.lean +++ b/verification/Proofs/Extract.lean @@ -210,11 +210,14 @@ theorem extractIncl_nonvacuous : /-- Inclusion soundness through the named acceptance predicate (review F1): if `acceptIncl` holds for a wrong leaf, `extractIncl` outputs a - collision. Ties the object the harness tests to the security theorem. -/ -theorem acceptIncl_sound (m : Nat) (D : List Bytes) (hm : m < D.length) + collision. Ties the object the harness tests to the security theorem. + The range fact `m < |D|` is `hacc.1` — acceptance carries it, so the + caller owes nothing beyond acceptance and the wrong-leaf premise + (review round 2, L1/NEW-2). -/ +theorem acceptIncl_sound (m : Nat) (D : List Bytes) (d : Bytes) (P : List Hash) (hd : d ≠ D.getD m []) (hacc : acceptIncl d m D.length P (MTH D)) : IsCollision (extractIncl m D d P).1 (extractIncl m D d P).2 := - extractIncl_correct m D d P hm hd hacc.2 + extractIncl_correct m D d P hacc.1 hd hacc.2 end LTLAcc diff --git a/verification/Proofs/Inventory.lean b/verification/Proofs/Inventory.lean new file mode 100644 index 0000000..b920003 --- /dev/null +++ b/verification/Proofs/Inventory.lean @@ -0,0 +1,123 @@ +/- Environment-derived declaration inventory (Phase 3b of check.sh). + + Review round 2 (GPT H1) proved the previous source-regex enumerator + evadable: attributed / private / indented / `instance` declarations + were invisible, and a nested `namespace Hidden theorem MTH` collided + with the basename of an audited declaration. This module replaces + source scanning entirely: the inventory is read from the compiled + Lean ENVIRONMENT, so it sees exactly what the kernel saw. + + Design (fail-closed by construction): + · The corpus module list below must match check.sh's compile + manifest (check.sh verifies this textually, both directions). + A listed module that is not actually imported is an elaboration + ERROR here, not a silent skip. + · EVERY constant whose originating module is a corpus module is + emitted — fully qualified, NO filtering. Compiler-generated + auxiliaries (equation lemmas, match/eq/induct helpers, private + mangles) are emitted too and pinned in the allowlist; anything + new, renamed, or removed shows up as a diff. There is no name + shape that can hide. + · Each constant carries its declaration KIND and its full axiom + cone, computed by the independent walker below (not by + #print axioms — Phase 3 still runs #print axioms separately, so + the two cone computations cross-check each other in check.sh). + · Output lines are prefixed `INV|` and sorted, so check.sh can + extract them robustly from compiler chatter. + + This file is audit INFRASTRUCTURE, not corpus: it is excluded from + the compile manifest (like AxiomCheck.lean) and its own constants + are not inventoried (they live in the current module, which has no + module index). It proves nothing and is imported by nothing. -/ +import Lean +import LTLAcc.HashExternal +import Proofs.Basic +import Proofs.Completeness +import Proofs.Extract +import Proofs.Descent +import Proofs.Consistency +import Proofs.Binding3 +import Proofs.Refactor +import Proofs.Theorem3 +import Proofs.PinStore + +open Lean + +namespace LTLAccAudit + +/-- Exactly check.sh's GEN_MODULES ++ PROOFS, as module names. -/ +def corpusModules : Array Name := + #[`LTLAcc.HashExternal, + `Proofs.Basic, `Proofs.Completeness, `Proofs.Extract, `Proofs.Descent, + `Proofs.Consistency, `Proofs.Binding3, `Proofs.Refactor, + `Proofs.Theorem3, `Proofs.PinStore] + +def kindOf : ConstantInfo → String + | .axiomInfo _ => "axiom" + | .defnInfo _ => "def" + | .thmInfo _ => "theorem" + | .opaqueInfo _ => "opaque" + | .quotInfo _ => "quot" + | .inductInfo _ => "inductive" + | .ctorInfo _ => "ctor" + | .recInfo _ => "recursor" + +/-- Proof/definition body of a constant. NOTE: `ConstantInfo.value?` + returns `none` for theorems on this toolchain (observed on + 4.30.0-rc2), which would silently truncate every cone at the first + theorem — so we match constructors directly. The cross-check against + core `collectAxioms` below would catch any such truncation. -/ +def valueOf : ConstantInfo → Option Expr + | .defnInfo v => some v.value + | .thmInfo v => some v.value + | .opaqueInfo v => some v.value + | _ => none + +/-- Full axiom cone of `root`: transitive closure over types AND values. + Written independently of core's `CollectAxioms`; the `#eval` below + insists both agree on every constant, and Phase 3 of check.sh + additionally cross-checks the audited names against `#print axioms` + output. -/ +def axiomCone (env : Environment) (root : Name) : Array Name := Id.run do + let mut visited : NameSet := {} + let mut axioms : Array Name := #[] + let mut stack : Array Name := #[root] + while h : stack.size > 0 do + let n := stack[stack.size - 1]'(by omega) + stack := stack.pop + unless visited.contains n do + visited := visited.insert n + if let some ci := env.find? n then + if ci matches .axiomInfo _ then + axioms := axioms.push n + stack := stack ++ ci.type.getUsedConstants + if let some v := valueOf ci then + stack := stack ++ v.getUsedConstants + return (axioms.qsort (fun a b => a.toString < b.toString)) + +#eval show CoreM Unit from do + let env ← getEnv + -- Resolve every corpus module to its index; a miss is a hard error. + let mut idxs : Array Nat := #[] + for m in corpusModules do + match env.getModuleIdx? m with + | some i => idxs := idxs.push i + | none => throwError "INVENTORY ERROR: corpus module {m} is not imported" + let mut lines : Array String := #[] + for (n, ci) in env.constants.toList do + if let some i := env.getModuleIdxFor? n then + if idxs.contains i then + let cone := axiomCone env n + -- Cross-check against core's collector (the same machinery + -- `#print axioms` uses): any divergence is a hard error. + let coreCone := (← collectAxioms n).qsort (fun a b => a.toString < b.toString) + unless cone == coreCone do + throwError "INVENTORY ERROR: cone divergence on {n}: walker={cone} core={coreCone}" + let coneStr := ",".intercalate (cone.toList.map (·.toString)) + lines := lines.push s!"INV|{n}|{kindOf ci}|{coneStr}" + let sorted := lines.qsort (· < ·) + for l in sorted do + IO.println l + IO.println s!"INV-COUNT|{sorted.size}" + +end LTLAccAudit diff --git a/verification/check.sh b/verification/check.sh index 500f7bc..2ee90d3 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -21,10 +21,11 @@ PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theore # Certificates and their exact expected cones (observed via #print axioms, # never guessed; any drift in EITHER direction is a failure). -# AUDIT SURFACE: every theorem/def under Proofs/ (52) + the two load-bearing -# gen/ instances (Inhabited/DecidableEq Hash). Excluded by nature: the -# sanctioned axiom itself (sha256 IS the boundary) and `abbrev Bytes` -# (a bare type alias, no cone content). +# AUDIT SURFACE: Phase 3b pins the FULL environment of the corpus modules +# (inventory-allowlist.txt, 218 constants incl. compiler-generated +# auxiliaries); the 59 entries below are the human-reviewed statement +# surface, additionally queried through #print axioms in Phase 3 and +# cross-checked against the inventory's independently computed cones. declare -A CONES=( [LTLAcc.domsep]="" [LTLAcc.kbelow_pos]="propext, Quot.sound" @@ -87,10 +88,9 @@ declare -A CONES=( [LTLAcc.extractCons_correct_paper]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" ) -# Sanctioned exclusions from the cone audit (documented, not silent): -# sha256 = THE boundary axiom (it IS the assumption) -# Bytes = bare type alias (abbrev), no cone content -declare -A EXCLUDE=( [sha256]=1 [Bytes]=1 ) +# (The former EXCLUDE table is gone: since Phase 3b reads the environment, +# sha256 and Bytes are ordinary allowlist entries — the axiom is pinned as +# the SINGLE axiom-kind constant, the abbrev carries its empty cone.) free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}' echo "=== Phase 0: source integrity ===" @@ -101,10 +101,11 @@ for f in "$HERE"/gen/LTLAcc/*.lean "$HERE"/Proofs/*.lean; do fi done echo " all sources valid" -for o in "$HERE"/Proofs/*.olean; do - [ -f "$o" ] || continue +# Recursive: no compiled artifact anywhere in the tree may lack its source +# (review round 2, GPT M1 — previously scanned Proofs/*.olean only). +while IFS= read -r -d '' o; do [ -f "${o%.olean}.lean" ] || { echo "ORPHAN OLEAN: $o has no sibling .lean (stale artifact)"; exit 1; } -done +done < <(find "$HERE" -name '*.olean' -print0) echo "=== Phase 1: stub + axiom-smuggling audit ===" if grep -rn 'by trivial' "$HERE"/Proofs/*.lean 2>/dev/null; then @@ -114,6 +115,11 @@ if grep -rn ' : True :=' "$HERE"/Proofs/*.lean 2>/dev/null; then if grep -rnE '^(private |protected |noncomputable )*axiom ' "$HERE"/Proofs/*.lean 2>/dev/null; then echo "AXIOM SMUGGLING DETECTED: axiom under Proofs/ — gen/ is the only sanctioned site."; exit 1 fi +# gen/ is the sanctioned site for exactly ONE axiom (review round 2, GPT M1). +# This textual pin is the fast belt; the semantic guarantee is Phase 3b's +# environment inventory (exactly one axiom-kind constant, LTLAcc.sha256). +AXCOUNT=$(grep -hcE '^(private |protected |noncomputable )*axiom ' "$HERE"/gen/LTLAcc/*.lean | paste -sd+ - | bc) +[ "$AXCOUNT" = 1 ] || { echo "AXIOM COUNT DRIFT: gen/ declares $AXCOUNT axioms, sanctioned: 1 (sha256)"; exit 1; } echo " clean" echo "=== Phase 2: compile ===" @@ -134,9 +140,15 @@ lake env bash -c " done for f in Proofs/*.lean; do b=\$(basename \"\$f\" .lean) - [ \"\$b\" = AxiomCheck ] && continue + [ \"\$b\" = AxiomCheck ] && continue # audit infrastructure, compiled in Phase 3 + [ \"\$b\" = Inventory ] && continue # audit infrastructure, compiled in Phase 3b case \" ${PROOFS[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE: \$f\"; exit 1;; esac done + # gen/ gets the same unmanifested-source check (review round 2, GPT M1) + for f in gen/LTLAcc/*.lean; do + b=\"LTLAcc/\$(basename \"\$f\" .lean)\" + case \" ${GEN_MODULES[*]} \" in (*\" \$b \"*) ;; (*) echo \"DEAD FILE (gen): \$f\"; exit 1;; esac + done " if grep -q "uses 'sorry'" "$LOG"; then echo "STUB: sorry detected"; exit 1; fi rm -f "$LOG" @@ -167,28 +179,64 @@ for cert in "${!CONES[@]}"; do done rm -f "$AUD" -# -- Phase 3b: audit-surface COVERAGE (fail-closed; review H1) -------------- -echo "=== Phase 3b: audit-surface coverage ===" +# -- Phase 3b: ENVIRONMENT-derived audit-surface coverage (fail-closed) ------ +# Review round 2 (GPT H1 / Claude NEW-1): the previous source-regex +# enumerator was evadable (attributes, indentation, private/protected, +# instance, and namespace-nested basename collisions). Replaced entirely: +# Proofs/Inventory.lean reads the compiled Lean ENVIRONMENT and emits every +# constant of every corpus module — fully qualified, unfiltered, each with +# kind and axiom cone (its own walker, cross-checked in-process against +# core collectAxioms). inventory_gate.sh diffs that against the pinned +# allowlist, fail-closed BOTH directions. No name shape can hide: what the +# kernel saw is what gets audited. +echo "=== Phase 3b: environment-derived audit-surface coverage ===" COVFAIL=0 -DECLS=$(grep -hoE "^(theorem|noncomputable def|def|abbrev) [A-Za-z0-9_?]+" \ - "$HERE"/Proofs/*.lean "$HERE"/gen/LTLAcc/*.lean | awk '{print $NF}' | sort -u) -for d in $DECLS; do - if [ -n "${CONES[LTLAcc.$d]+x}" ] || [ -n "${EXCLUDE[$d]+x}" ]; then :; else - echo " UNCLASSIFIED DECLARATION: $d (not in CONES, not a sanctioned exclusion)"; COVFAIL=1 - fi +INVLOG=$(mktemp /tmp/acc-inv-XXXX.log) +cd "$AENEAS_LEAN" +lake env bash -c " + cd '$HERE' && export LEAN_PATH=\"\$LEAN_PATH:$HERE/gen:$HERE\" + LEAN_TIMEOUT=600 LEAN_MAX_CORES=$CORES '$HERE/lean-guard' Proofs/Inventory.lean +" > "$INVLOG" 2>&1 || { cat "$INVLOG"; echo "INVENTORY COMPILE FAILED"; exit 1; } +"$HERE/inventory_gate.sh" "$INVLOG" "$HERE/inventory-allowlist.txt" || COVFAIL=1 + +# The inventory's corpus-module list must BE the compile manifest — both +# directions, so neither can drift from the other silently. +for m in "${GEN_MODULES[@]}" "${PROOFS[@]}"; do + mod=$(echo "$m" | sed 's|^LTLAcc/|LTLAcc.|; s|^\([A-Z]\)|Proofs.\1|; s|^Proofs\.LTLAcc\.|LTLAcc.|') + grep -qF "\`$mod" "$HERE/Proofs/Inventory.lean" || { + echo " MANIFEST DRIFT: $mod compiled by check.sh but not inventoried"; COVFAIL=1; } done -# anonymous instances live only in gen/ (a controlled file); pin their count -GENINST=$(grep -cE "^instance" "$HERE"/gen/LTLAcc/*.lean) -CONEINST=$(printf '%s\n' "${!CONES[@]}" | grep -cE "LTLAcc\.inst") -if [ "$GENINST" != "$CONEINST" ]; then - echo " INSTANCE COUNT DRIFT: gen has $GENINST instances, CONES pins $CONEINST"; COVFAIL=1 -fi +NMANIFEST=$(( ${#GEN_MODULES[@]} + ${#PROOFS[@]} )) +NINV=$(grep -oE '`(LTLAcc|Proofs)\.[A-Za-z0-9_.]+' "$HERE/Proofs/Inventory.lean" | wc -l) +[ "$NMANIFEST" = "$NINV" ] || { + echo " MANIFEST DRIFT: check.sh compiles $NMANIFEST modules, Inventory lists $NINV"; COVFAIL=1; } + +# CONES ⊆ allowlist with IDENTICAL cones: the #print-axioms-pinned table +# and the environment inventory are two independent computations of the +# same facts — any disagreement is a failure of one of them. +# (cones are compared as SETS: CONES keeps #print-axioms order, the +# inventory emits byte-sorted order — canonicalize both before comparing) +canon() { tr -d ' ' <<<"$1" | tr ',' '\n' | LC_ALL=C sort | paste -sd, -; } +while IFS='|' read -r _ name _ cone; do + if [ -n "${CONES[$name]+x}" ]; then + want=$(canon "${CONES[$name]}") + got=$(canon "$cone") + [ "$want" = "$got" ] || { + echo " CONE CROSS-CHECK FAILED: $name CONES=[$want] inventory=[$got]"; COVFAIL=1; } + fi +done < <(grep '^INV|' "$HERE/inventory-allowlist.txt") +for cert in "${!CONES[@]}"; do + grep -q "^INV|$cert|" "$HERE/inventory-allowlist.txt" || { + echo " PINNED BUT NOT INVENTORIED: $cert (in CONES, not in allowlist)"; COVFAIL=1; } +done +rm -f "$INVLOG" + # every pinned cert must actually be queried by AxiomCheck (no pin-but-never-check) for cert in "${!CONES[@]}"; do grep -qF "#print axioms $cert" "$HERE/Proofs/AxiomCheck.lean" || { echo " PINNED BUT NOT QUERIED: $cert (in CONES, absent from AxiomCheck.lean)"; COVFAIL=1; } done -[ "$COVFAIL" = 0 ] && echo " coverage complete: every declaration classified (audited or sanctioned-excluded)" +[ "$COVFAIL" = 0 ] && echo " coverage complete: environment == allowlist, CONES cross-checked" [ "$COVFAIL" = 0 ] || { echo "COVERAGE FAILED"; FAIL=1; } [ "$FAIL" = 0 ] || exit 1 # -- Phase 4: definition fidelity (Lean defs vs deployed pacta verifiers) -- diff --git a/verification/inventory-allowlist.txt b/verification/inventory-allowlist.txt new file mode 100644 index 0000000..65e14c7 --- /dev/null +++ b/verification/inventory-allowlist.txt @@ -0,0 +1,235 @@ +# inventory-allowlist.txt — the pinned audit surface (Phase 3b). +# +# One line per constant in the compiled environment of the corpus +# modules (GEN_MODULES + PROOFS in check.sh), emitted by +# Proofs/Inventory.lean: INV||| +# +# EVERYTHING the kernel saw is here — including compiler-generated +# auxiliaries (match_*/eq_*/induct/_proof_*/_unary and _private.* +# mangles). There is no filtering, so there is no name shape that can +# escape: a new, renamed, re-namespaced, private, attributed, indented, +# or instance declaration changes the environment and fails the diff. +# Regenerate ONLY by reviewing `lean-guard Proofs/Inventory.lean` output +# line by line; every addition must be justified in STATEMENT-MAP.md or +# be a compiler-generated auxiliary of a justified declaration. +# +# Invariant checked by check.sh on top of the diff: +# exactly ONE axiom line in this file, and it is LTLAcc.sha256. +INV|LTLAcc.acceptCons|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.acceptIncl|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.acceptIncl_complete|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.acceptIncl_sound|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Bytes|def| +INV|LTLAcc.ConsRec|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.consRec_base_false_eq|theorem|Classical.choice,Quot.sound,propext +INV|LTLAcc.consRec_base_false_eq.match_1|def|propext +INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_1|def|propext +INV|LTLAcc.consRec_base_false_eq._sparseCasesOn_2|def|propext +INV|LTLAcc.consRec_base_true_eq|theorem|propext +INV|LTLAcc.consRec_base_true_eq.match_1|def|propext +INV|LTLAcc.consRecBinding|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.consRecBinding.match_1|def| +INV|LTLAcc.consRecBinding._proof_1_10|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_11|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_12|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_13|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_14|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_15|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_16|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_17|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_5|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_6|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_7|theorem|Quot.sound,propext +INV|LTLAcc.consRecBinding._proof_1_8|theorem|Quot.sound,propext +INV|LTLAcc.ConsRec.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.ConsRec.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.ConsRec.induct|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.ConsRec.match_1|def| +INV|LTLAcc.ConsRec._unary|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.ConsRec._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.ConsRec._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.ConsRec._unary._proof_1|theorem|Quot.sound,propext +INV|LTLAcc.ConsRec._unary._proof_2|theorem|Quot.sound,propext +INV|LTLAcc.domsep|theorem| +INV|LTLAcc.eq_dropLast_append_of_getLast?|theorem|propext +INV|LTLAcc.exists_singleton_of_length_one|theorem|Classical.choice,Quot.sound,propext +INV|LTLAcc.extractCons|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractCons_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractCons_correct_paper|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractCons_correct_paper._proof_1_1|theorem|Quot.sound,propext +INV|LTLAcc.extractCons_correct._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.extractCons_correct._proof_1_3|theorem|Quot.sound,propext +INV|LTLAcc.extractCons.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractCons.match_1|def| +INV|LTLAcc.extractConsNode|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractConsNode.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractConsNode.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractConsNode.match_1|def| +INV|LTLAcc.extractConsNode._unary|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractConsNode._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractConsNode._unary._proof_1|theorem|Quot.sound,propext +INV|LTLAcc.extractConsNode._unary._proof_2|theorem|Quot.sound,propext +INV|LTLAcc.extractCons_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractCons_nonvacuous._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractIncl_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractIncl_correct._proof_1_1|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl_correct._proof_1_3|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl_correct._proof_1_4|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl_correct._proof_1_5|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl_correct._proof_1_6|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl_correct._proof_1_7|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl_correct._proof_1_8|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl_correct._proof_1_9|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractIncl.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractIncl.match_1|def| +INV|LTLAcc.extractIncl_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractIncl_nonvacuous._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl._unary|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractIncl._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractIncl._unary._proof_1|theorem|Quot.sound,propext +INV|LTLAcc.extractIncl._unary._proof_2|theorem|Quot.sound,propext +INV|LTLAcc.extractMTH|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractMTH_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractMTH_correct._proof_1_10|theorem|Quot.sound,propext +INV|LTLAcc.extractMTH_correct._proof_1_4|theorem|Quot.sound,propext +INV|LTLAcc.extractMTH_correct._proof_1_5|theorem|Quot.sound,propext +INV|LTLAcc.extractMTH_correct._proof_1_6|theorem|Quot.sound,propext +INV|LTLAcc.extractMTH_correct._proof_1_7|theorem|Quot.sound,propext +INV|LTLAcc.extractMTH_correct._proof_1_8|theorem|Quot.sound,propext +INV|LTLAcc.extractMTH_correct._proof_1_9|theorem|Quot.sound,propext +INV|LTLAcc.extractMTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractMTH.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractMTH.induct|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractMTH_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractMTH_nonvacuous._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.extractMTH._unary|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractMTH._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractMTH._unary.induct|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.extractMTH._unary._proof_1|theorem|Quot.sound,propext +INV|LTLAcc.extractMTH._unary._proof_2|theorem|Quot.sound,propext +INV|LTLAcc.fork_distinct|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.getD_drop|theorem|Quot.sound,propext +INV|LTLAcc.getD_drop._proof_1_1|theorem|Quot.sound,propext +INV|LTLAcc.getD_take|theorem|Quot.sound,propext +INV|LTLAcc.getD_take._proof_1_1|theorem|Quot.sound,propext +INV|LTLAcc.getD_take._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.Hash|def| +INV|LTLAcc.hleaf|def|LTLAcc.sha256 +INV|LTLAcc.hnode|def|LTLAcc.sha256 +INV|LTLAcc.hnode_preimage_inj|theorem|propext +INV|LTLAcc.incl_complete|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.incl_complete._proof_1_3|theorem|Quot.sound,propext +INV|LTLAcc.incl_complete._proof_1_5|theorem|Quot.sound,propext +INV|LTLAcc.incl_complete._proof_1_6|theorem|Quot.sound,propext +INV|LTLAcc.incl_complete._proof_1_7|theorem|Quot.sound,propext +INV|LTLAcc.incl_complete._proof_1_8|theorem|Quot.sound,propext +INV|LTLAcc.incl_complete._proof_1_9|theorem|Quot.sound,propext +INV|LTLAcc.instDecidableEqHash|def| +INV|LTLAcc.instDecidableEqHash._proof_1|theorem| +INV|LTLAcc.instInhabitedHash|def|propext +INV|LTLAcc.instInhabitedHash._proof_1|theorem|propext +INV|LTLAcc.IsCollision|def|LTLAcc.sha256 +INV|LTLAcc.kbelow|def|Quot.sound,propext +INV|LTLAcc.kbelow.eq_1|theorem|Quot.sound,propext +INV|LTLAcc.kbelow.eq_def|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_eq_of_pow2_between|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_1|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_3|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_eq_of_pow2_between._proof_1_4|theorem|Quot.sound,propext +INV|LTLAcc.kbelow.induct|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_lt|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_lt._proof_1_3|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_lt._proof_1_4|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_lt._proof_1_5|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_pos|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_pow2|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_prefix_eq|theorem|Quot.sound,propext +INV|LTLAcc.kbelow_prefix_eq._proof_1_1|theorem|Quot.sound,propext +INV|LTLAcc.kbelow._proof_1|theorem|Quot.sound,propext +INV|LTLAcc.kbelow._unsafe_rec|def| +INV|LTLAcc.le_two_kbelow|theorem|Quot.sound,propext +INV|LTLAcc.le_two_kbelow._proof_1_3|theorem|Quot.sound,propext +INV|LTLAcc.le_two_kbelow._proof_1_4|theorem|Quot.sound,propext +INV|LTLAcc.MTH|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.MTH.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.MTH.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.MTH._proof_1|theorem|Quot.sound,propext +INV|LTLAcc.MTH._proof_2|theorem|Quot.sound,propext +INV|LTLAcc.MTH_single|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.MTH_split|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.MTH_split._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.MTH_split._proof_1_3|theorem|Quot.sound,propext +INV|LTLAcc.Path|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Path.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Path.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Path.induct|theorem|Quot.sound,propext +INV|LTLAcc.Path._unary|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Path._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Path._unary.induct|theorem|Quot.sound,propext +INV|LTLAcc.Path._unary._proof_1|theorem|Quot.sound,propext +INV|LTLAcc.Path._unary._proof_2|theorem|Quot.sound,propext +INV|LTLAcc.pinAccept|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.pinAccept_monotone|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.pinAccept_monotone._proof_1_1|theorem|Quot.sound,propext +INV|LTLAcc.pinAccept_monotone._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.pinExtract|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.pinExtract.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.pin_prefix_correct|theorem|Classical.choice,LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.pin_prefix_correct._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.pin_prefix_nonvacuous|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.pin_prefix_nonvacuous._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.pow2_exp_unique|theorem|Quot.sound,propext +INV|LTLAcc.pow2_exp_unique._proof_1_1|theorem|Quot.sound,propext +INV|LTLAcc.pow2_exp_unique._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.pow2_exp_unique._proof_1_3|theorem|Quot.sound,propext +INV|LTLAcc.Root|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Root.eq_1|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Root.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Root_left|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Root_left._proof_1_1|theorem|Quot.sound,propext +INV|LTLAcc.Root_left._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.Root.match_1|def| +INV|LTLAcc.Root_one|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Root_one_cons|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Root_right|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Root_right._proof_1_1|theorem|Quot.sound,propext +INV|LTLAcc.Root_right._proof_1_2|theorem|Quot.sound,propext +INV|LTLAcc.Root._unary|def|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Root._unary.eq_def|theorem|LTLAcc.sha256,Quot.sound,propext +INV|LTLAcc.Root._unary._proof_1|theorem|Quot.sound,propext +INV|LTLAcc.Root._unary._proof_2|theorem|Quot.sound,propext +INV|LTLAcc.sha256|axiom|LTLAcc.sha256 +INV|LTLAcc.take_all|theorem|propext +INV|LTLAcc.take_append_drop|theorem| +INV|LTLAcc.take_drop_prefix|theorem|Classical.choice,Quot.sound,propext +INV|LTLAcc.take_take_le|theorem|Quot.sound,propext +INV|LTLAcc.take_take_le._proof_1_1|theorem|Quot.sound,propext +INV|_private.Proofs.Basic.0.LTLAcc.ConsRec.match_1.eq_1|theorem| +INV|_private.Proofs.Basic.0.LTLAcc.ConsRec.match_1.eq_2|theorem| +INV|_private.Proofs.Basic.0.LTLAcc.ConsRec.match_1.splitter|def| +INV|_private.Proofs.Basic.0.LTLAcc.Root.match_1.eq_1|theorem| +INV|_private.Proofs.Basic.0.LTLAcc.Root.match_1.eq_2|theorem| +INV|_private.Proofs.Basic.0.LTLAcc.Root.match_1.splitter|def| +INV|_private.Proofs.Basic.0.PSigma.casesOn._arg_pusher|theorem| +INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.eq_1|theorem| +INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.eq_2|theorem| +INV|_private.Proofs.Binding3.0.LTLAcc.consRecBinding.match_1.splitter|def| +INV|_private.Proofs.Binding3.0.LTLAcc.ConsRec.match_1.eq_1|theorem| +INV|_private.Proofs.Binding3.0.LTLAcc.ConsRec.match_1.eq_2|theorem| +INV|_private.Proofs.Binding3.0.LTLAcc.ConsRec.match_1.splitter|def| +INV|_private.Proofs.Binding3.0.LTLAcc.Root.match_1.eq_1|theorem| +INV|_private.Proofs.Binding3.0.LTLAcc.Root.match_1.eq_2|theorem| +INV|_private.Proofs.Binding3.0.LTLAcc.Root.match_1.splitter|def| +INV|_private.Proofs.Completeness.0.PSigma.casesOn._arg_pusher|theorem| +INV|_private.Proofs.Consistency.0.LTLAcc.extractConsNode.match_1.eq_1|theorem| +INV|_private.Proofs.Consistency.0.LTLAcc.extractConsNode.match_1.eq_2|theorem| +INV|_private.Proofs.Consistency.0.LTLAcc.extractConsNode.match_1.splitter|def| +INV|_private.Proofs.Consistency.0.PSigma.casesOn._arg_pusher|theorem| +INV|_private.Proofs.Descent.0.PSigma.casesOn._arg_pusher|theorem| +INV|_private.Proofs.Extract.0.LTLAcc.extractIncl.match_1.eq_1|theorem| +INV|_private.Proofs.Extract.0.LTLAcc.extractIncl.match_1.eq_2|theorem| +INV|_private.Proofs.Extract.0.LTLAcc.extractIncl.match_1.splitter|def| +INV|_private.Proofs.Extract.0.PSigma.casesOn._arg_pusher|theorem| diff --git a/verification/inventory_gate.sh b/verification/inventory_gate.sh new file mode 100755 index 0000000..01a7e82 --- /dev/null +++ b/verification/inventory_gate.sh @@ -0,0 +1,52 @@ +#!/usr/bin/env bash +# ───────────────────────────────────────────────────────────────────────────── +# inventory_gate.sh — diff an observed environment inventory against the +# pinned allowlist. This is THE production coverage gate: check.sh Phase 3b +# calls it, and selftest_audit.sh exercises this exact script against +# injected evader declarations — the tested logic IS the shipping logic. +# +# Usage: inventory_gate.sh +# +# Fail-closed in BOTH directions: +# UNCLASSIFIED — constant in the environment, absent from the allowlist +# (new/renamed decl, changed kind, or changed axiom cone) +# STALE — allowlist entry absent from the environment +# plus an output-integrity check: the INV-COUNT trailer emitted by +# Proofs/Inventory.lean must equal the number of INV lines actually seen, +# so a truncated or crashed run can never pass as an empty diff. +# ───────────────────────────────────────────────────────────────────────────── +set -uo pipefail +export LC_ALL=C # byte-order collation: sort/comm must agree with Lean's String order +obs_file="$1"; allow_file="$2" + +OBS=$(grep '^INV|' "$obs_file" | sort -u) +N_OBS=$(printf '%s' "$OBS" | grep -c '^INV|' || true) +TRAILER=$(grep '^INV-COUNT|' "$obs_file" | tail -1 | cut -d'|' -f2) +if [ -z "$TRAILER" ] || [ "$TRAILER" != "$N_OBS" ]; then + echo " INVENTORY TRUNCATED: trailer=${TRAILER:-absent}, observed $N_OBS lines" + exit 1 +fi + +ALLOW=$(grep '^INV|' "$allow_file" | sort -u) +FAILGATE=0 +UNCLASS=$(comm -23 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW")) +STALE=$(comm -13 <(printf '%s\n' "$OBS") <(printf '%s\n' "$ALLOW")) +if [ -n "$UNCLASS" ]; then + printf '%s\n' "$UNCLASS" | sed 's/^/ UNCLASSIFIED (in environment, not allowlisted): /' + FAILGATE=1 +fi +if [ -n "$STALE" ]; then + printf '%s\n' "$STALE" | sed 's/^/ STALE (allowlisted, not in environment): /' + FAILGATE=1 +fi + +# The corpus admits exactly one axiom, and it is the sanctioned boundary. +AXLINES=$(printf '%s\n' "$OBS" | grep '|axiom|' || true) +if [ "$AXLINES" != "INV|LTLAcc.sha256|axiom|LTLAcc.sha256" ]; then + echo " AXIOM SURFACE DRIFT: expected exactly LTLAcc.sha256, observed:" + printf '%s\n' "${AXLINES:- (none)}" | sed 's/^/ /' + FAILGATE=1 +fi + +[ "$FAILGATE" = 0 ] && echo " inventory gate: $N_OBS constants, environment == allowlist, single sanctioned axiom" +exit "$FAILGATE" diff --git a/verification/selftest_audit.sh b/verification/selftest_audit.sh new file mode 100755 index 0000000..8308cc7 --- /dev/null +++ b/verification/selftest_audit.sh @@ -0,0 +1,135 @@ +#!/usr/bin/env bash +# ───────────────────────────────────────────────────────────────────────────── +# selftest_audit.sh — adversarial self-test of the audit gate. +# +# Review round 2 (GPT H1 / Claude NEW-1) demonstrated that the old +# source-regex coverage gate was evadable. This script proves the +# replacement is not, by ATTACKING THE SHIPPING LOGIC: every case copies +# the corpus to a scratch tree, injects a declaration the old gate could +# not see, recompiles through lean-guard, and asserts that the exact +# inventory_gate.sh used by check.sh Phase 3b FAILS with the expected +# diagnosis. The two unmanifested-module cases run the full check.sh. +# +# Cases (release condition 2 of the round-2 GPT review, plus two): +# 0 positive control: pristine tree must PASS (guards against a gate +# that fails everything — a vacuous self-test) +# 1 attributed theorem @[simp] theorem … +# 2 indented theorem (leading whitespace) +# 3 private theorem private theorem … +# 4 instance declaration instance … : Nonempty Nat +# 5 nested namespace collision LTLAcc.Hidden.MTH vs audited LTLAcc.MTH +# 6 smuggled axiom axiom rogue : True +# 7 deleted declaration STALE direction of the diff +# 8 unmanifested Proofs/ module full check.sh must die: DEAD FILE +# 9 unmanifested gen/ module full check.sh must die: DEAD FILE (gen) +# +# Run AFTER a green check.sh (needs compiled .oleans in the tree). +# All Lean work goes through lean-guard (memory-capped, single-flight). +# ───────────────────────────────────────────────────────────────────────────── +set -euo pipefail +source ~/aeneas-toolchain/env.sh +SRC="$(cd "$(dirname "$0")" && pwd)" +AENEAS_LEAN="$AENEAS_HOME/backends/lean" +CORES="${LEAN_MAX_CORES:-0-3}" + +WORK=$(mktemp -d /tmp/acc-selftest-XXXX) +trap 'echo "(scratch tree kept for inspection: $WORK)"' ERR +echo "=== audit-gate self-test (scratch: $WORK) ===" +cp -a "$SRC" "$WORK/verification" +T="$WORK/verification" +cp "$T/Proofs/PinStore.lean" "$T/PinStore.pristine" + +# Recompile the injected leaf module + the inventory, then run the gate. +# Returns the gate's exit code; gate output goes to $T/gate.out. +run_gate() { + cd "$AENEAS_LEAN" + lake env bash -c " + set -euo pipefail + cd '$T' && export LEAN_PATH=\"\$LEAN_PATH:$T/gen:$T\" + LEAN_TIMEOUT=600 LEAN_MAX_CORES=$CORES '$T/lean-guard' Proofs/PinStore.lean >/dev/null 2>&1 + LEAN_TIMEOUT=600 LEAN_MAX_CORES=$CORES '$T/lean-guard' Proofs/Inventory.lean + " > "$T/inv.out" 2>&1 || { echo " (inventory compile failed — see $T/inv.out)"; return 99; } + "$T/inventory_gate.sh" "$T/inv.out" "$T/inventory-allowlist.txt" > "$T/gate.out" 2>&1 +} + +expect_fail() { # $1=case label $2=grep pattern expected in gate output + local rc=0; run_gate || rc=$? + if [ "$rc" = 0 ]; then + echo " ✗ $1: gate PASSED but must fail"; echo "SELF-TEST FAILED"; exit 1 + elif [ "$rc" = 99 ]; then + echo " ✗ $1: injected code did not compile (case is vacuous)"; exit 1 + elif ! grep -q "$2" "$T/gate.out"; then + echo " ✗ $1: gate failed but without expected diagnosis '$2':" + sed 's/^/ /' "$T/gate.out"; exit 1 + fi + echo " ✓ $1: gate fails with $(grep -c "$2" "$T/gate.out") '$2' line(s)" +} + +restore() { cp "$T/PinStore.pristine" "$T/Proofs/PinStore.lean"; } + +# 0 — positive control +if run_gate; then echo " ✓ case 0 control: pristine tree passes the gate"; else + echo " ✗ case 0 control: pristine tree FAILED the gate:"; sed 's/^/ /' "$T/gate.out"; exit 1; fi + +# 1 — attributed +restore; printf '\n@[simp] theorem smuggled_attr : 1 = 1 := rfl\n' >> "$T/Proofs/PinStore.lean" +expect_fail "case 1 attributed theorem" "UNCLASSIFIED.*smuggled_attr" + +# 2 — indented +restore; printf '\n theorem smuggled_indent : 3 = 3 := rfl\n' >> "$T/Proofs/PinStore.lean" +expect_fail "case 2 indented theorem" "UNCLASSIFIED.*smuggled_indent" + +# 3 — private +restore; printf '\nprivate theorem smuggled_private : 2 = 2 := rfl\n' >> "$T/Proofs/PinStore.lean" +expect_fail "case 3 private theorem" "UNCLASSIFIED.*_private.*smuggled_private" + +# 4 — instance +restore; printf '\ninstance smuggledInst : Nonempty Nat := ⟨0⟩\n' >> "$T/Proofs/PinStore.lean" +expect_fail "case 4 instance" "UNCLASSIFIED.*smuggledInst" + +# 5 — nested namespace reusing an audited basename +restore; printf '\nnamespace LTLAcc.Hidden\ntheorem MTH : 1 = 1 := rfl\nend LTLAcc.Hidden\n' >> "$T/Proofs/PinStore.lean" +expect_fail "case 5 namespace collision (LTLAcc.Hidden.MTH)" "UNCLASSIFIED.*LTLAcc\.Hidden\.MTH" + +# 6 — smuggled axiom +restore; printf '\naxiom rogue : True\n' >> "$T/Proofs/PinStore.lean" +expect_fail "case 6 smuggled axiom" "AXIOM SURFACE DRIFT" + +# 7 — deleted declaration (STALE direction) +restore +python3 - "$T/Proofs/PinStore.lean" <<'EOF' +import sys +p = sys.argv[1]; s = open(p).read() +# drop the trailing nonvacuity guard (a leaf theorem nothing imports), +# including its doc comment — an orphaned /-- ... -/ would not compile +i = s.rindex("/-- Permanent non-vacuity witness for pin_prefix_correct") +j = s.index("end LTLAcc", i) +open(p, "w").write(s[:i] + s[j:]) +EOF +expect_fail "case 7 deleted declaration" "STALE.*pin_prefix_nonvacuous" + +restore +rm -f "$T/PinStore.pristine" + +# 8 — unmanifested Proofs/ module (full check.sh; dies in Phase 2) +printf '/- rogue -/\ntheorem rogue_thm : 1 = 1 := rfl\n' > "$T/Proofs/Rogue.lean" +if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check8.out" 2>&1; then + echo " ✗ case 8: check.sh PASSED with unmanifested Proofs/Rogue.lean"; exit 1 +fi +grep -q "DEAD FILE: Proofs/Rogue.lean" "$T/check8.out" || { + echo " ✗ case 8: check.sh failed without DEAD FILE diagnosis"; tail -5 "$T/check8.out"; exit 1; } +echo " ✓ case 8 unmanifested Proofs module: check.sh dies with DEAD FILE" +rm -f "$T/Proofs/Rogue.lean" + +# 9 — unmanifested gen/ module (full check.sh; dies in Phase 2) +printf '/- rogue -/\ntheorem rogue_gen : 1 = 1 := rfl\n' > "$T/gen/LTLAcc/Rogue.lean" +if SKIP_FIDELITY=1 "$T/check.sh" > "$T/check9.out" 2>&1; then + echo " ✗ case 9: check.sh PASSED with unmanifested gen/LTLAcc/Rogue.lean"; exit 1 +fi +grep -q "DEAD FILE (gen): gen/LTLAcc/Rogue.lean" "$T/check9.out" || { + echo " ✗ case 9: check.sh failed without DEAD FILE (gen) diagnosis"; tail -5 "$T/check9.out"; exit 1; } +echo " ✓ case 9 unmanifested gen module: check.sh dies with DEAD FILE (gen)" + +rm -rf "$WORK" +trap - ERR +echo "=== SELF-TEST GREEN: 9 attack cases defeated + positive control ==="