From db45c0e33f882d58b3c766ef77da7f4e8c127ee5 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 11 Jul 2026 20:56:17 +0200 Subject: [PATCH] S7 Fable re-audit: close the cone-audit COVERAGE gap (52/52), verify button by exit code MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Re-derived S7 as Fable, practicing the standing rule (check exit code + ALL GREEN, not tail). Confirmed committed button genuinely exits 0. FINDING: the cone audit had a COVERAGE gap — 34 of 52 proven objects were pinned; 18 (incl. core defs kbelow/hleaf/hnode and the pin-store defs pinAccept/pinExtract/acceptCons, plus intermediate lemmas) were never cone-audited. Transitively safe (Phase 1 forbids axiom under Proofs/, Phase 2 forbids sorry, universally) — but 'transitively covered' is not good enough for an externally-reviewed corpus. Closed: every proven theorem/def now has its EXACT cone pinned, read from #print axioms (not guessed). Coverage now 52/52, empty unaudited list. Cones of note: hleaf/hnode = [LTLAcc.sha256] only; kbelow and the pure arithmetic/list helpers = no hash axiom; the def-level objects that touch MTH carry the single sha256 boundary. No surprise axioms anywhere. Button verified: EXIT 0, ALL GREEN, FIDELITY GREEN, 164,479/164,224 pinned. LTL untouched. Co-Authored-By: Claude Fable 5 --- verification/Proofs/AxiomCheck.lean | 20 ++++++++++++++++++++ verification/check.sh | 19 +++++++++++++++++++ 2 files changed, 39 insertions(+) diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean index baa0878..a0345a5 100644 --- a/verification/Proofs/AxiomCheck.lean +++ b/verification/Proofs/AxiomCheck.lean @@ -41,3 +41,23 @@ import Proofs.PinStore #print axioms LTLAcc.pin_prefix_correct #print axioms LTLAcc.fork_distinct #print axioms LTLAcc.pin_prefix_nonvacuous + +#print axioms LTLAcc.MTH_single +#print axioms LTLAcc.MTH_split +#print axioms LTLAcc.Root_left +#print axioms LTLAcc.Root_one +#print axioms LTLAcc.Root_one_cons +#print axioms LTLAcc.Root_right +#print axioms LTLAcc.acceptCons +#print axioms LTLAcc.eq_dropLast_append_of_getLast? +#print axioms LTLAcc.exists_singleton_of_length_one +#print axioms LTLAcc.getD_drop +#print axioms LTLAcc.getD_take +#print axioms LTLAcc.hleaf +#print axioms LTLAcc.hnode +#print axioms LTLAcc.kbelow +#print axioms LTLAcc.kbelow_eq_of_pow2_between +#print axioms LTLAcc.pinAccept +#print axioms LTLAcc.pinExtract +#print axioms LTLAcc.pow2_exp_unique +#print axioms LTLAcc.take_append_drop diff --git a/verification/check.sh b/verification/check.sh index dd7ec7f..8e1a5e6 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -55,6 +55,25 @@ declare -A CONES=( [LTLAcc.pin_prefix_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound" [LTLAcc.fork_distinct]="propext, LTLAcc.sha256, Quot.sound" [LTLAcc.pin_prefix_nonvacuous]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.MTH_single]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.MTH_split]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.Root_left]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.Root_one]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.Root_one_cons]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.Root_right]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.acceptCons]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.exists_singleton_of_length_one]="propext, Classical.choice, Quot.sound" + [LTLAcc.getD_drop]="propext, Quot.sound" + [LTLAcc.getD_take]="propext, Quot.sound" + [LTLAcc.hleaf]="LTLAcc.sha256" + [LTLAcc.hnode]="LTLAcc.sha256" + [LTLAcc.kbelow]="propext, Quot.sound" + [LTLAcc.kbelow_eq_of_pow2_between]="propext, Quot.sound" + [LTLAcc.pinAccept]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.pinExtract]="propext, LTLAcc.sha256, Quot.sound" + [LTLAcc.pow2_exp_unique]="propext, Quot.sound" + [LTLAcc.take_append_drop]="" + [LTLAcc.eq_dropLast_append_of_getLast?]="propext" ) free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'