From a3b8b3ecea35b0d2f39092ab19fe437c3540d361 Mon Sep 17 00:00:00 2001 From: mrwulf Date: Sat, 11 Jul 2026 21:07:08 +0200 Subject: [PATCH] S7 drill (2nd pass): pin the load-bearing gen/ instance cones; document audit surface MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Audit-of-the-coverage-audit. Its 18 added cone values re-verified against the observed #print outputs (all match). Methodology blind spots found: abbrev Bytes (bare alias, no cone content — excluded by nature) and the two ANONYMOUS gen/ instances, which are silently load-bearing (DecidableEq Hash powers ConsRec's 'if C = []' and pinAccept's root compare; Inhabited Hash powers every getD default). Transitivity covered them, but no hand-waves before external review: cones read and pinned — instInhabitedHash = [propext], instDecidableEqHash = AXIOM-FREE. The audit-surface definition is now documented in check.sh itself. Button verified by exit code: EXIT 0, ALL GREEN, FIDELITY GREEN. 54 pinned cones. LTL untouched. Co-Authored-By: Claude Fable 5 --- verification/Proofs/AxiomCheck.lean | 2 ++ verification/check.sh | 10 ++++++++-- 2 files changed, 10 insertions(+), 2 deletions(-) diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean index a0345a5..c33ab76 100644 --- a/verification/Proofs/AxiomCheck.lean +++ b/verification/Proofs/AxiomCheck.lean @@ -61,3 +61,5 @@ import Proofs.PinStore #print axioms LTLAcc.pinExtract #print axioms LTLAcc.pow2_exp_unique #print axioms LTLAcc.take_append_drop +#print axioms LTLAcc.instInhabitedHash +#print axioms LTLAcc.instDecidableEqHash diff --git a/verification/check.sh b/verification/check.sh index 8e1a5e6..8d53d0d 100755 --- a/verification/check.sh +++ b/verification/check.sh @@ -19,8 +19,12 @@ CORES="${LEAN_MAX_CORES:-0-3}" GEN_MODULES=( LTLAcc/HashExternal ) PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theorem3 PinStore ) -# Certificates and their exact expected cones (observed at first green -# compile, 2026-07-10; any drift in EITHER direction is a failure). +# 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). declare -A CONES=( [LTLAcc.domsep]="" [LTLAcc.kbelow_pos]="propext, Quot.sound" @@ -74,6 +78,8 @@ declare -A CONES=( [LTLAcc.pow2_exp_unique]="propext, Quot.sound" [LTLAcc.take_append_drop]="" [LTLAcc.eq_dropLast_append_of_getLast?]="propext" + [LTLAcc.instInhabitedHash]="propext" + [LTLAcc.instDecidableEqHash]="" ) free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'