saymrwulf/ltl-accumulator-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/ltl-accumulator-verified.git synced 2026-09-03 19:53:48 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

S7 drill (2nd pass): pin the load-bearing gen/ instance cones; document audit surface

Browse source 
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 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-11 21:07:08 +02:00
parent db45c0e33f
commit a3b8b3ecea
2 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
verification/Proofs/AxiomCheck.lean
View file

@ -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

10
verification/check.sh
View file

@ -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}}'