saymrwulf/ltl-accumulator-verified
1
0
Fork 0
mirror of https://github.com/saymrwulf/ltl-accumulator-verified.git synced 2026-09-05 20:10:43 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

S5 stage-2 Fable re-audit: flag load-bearing invariant, correct 'verified' overclaim

Browse source 
Re-derived the planned stage-3 binding against the extractConsNode
definition. Definition is SOUND (candidate/ConsRec hnode alignment
re-confirmed: n₀≤k hnode y s ↔ 0x01::y'++s; n₀>k hnode s y ↔ 0x01::s++y').

FINDING (protects stage 3): extractConsNode's  candidate is a
genuine collision ONLY under y_current = MTH(D₁_current) — sha256(LHS) =
hnode y' s = y_current, sha256(RHS) = MTH D₁_current, equal iff the
value-equality invariant holds. The stage-3 binding statement MUST thread
 through the recursion (Lemma 2's top-down equality). Planned
statement already carries it; note now flags it as load-bearing so it
can't be dropped.

LEDGER: cfde9b2 claimed the extractor 'verified faithful' — that
overclaimed kernel-verification; it is inspection-only until
consRecBinding is proven. README corrected to say so.

No Lean change (definition sound). 22 certs green. LTL untouched.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This commit is contained in:
mrwulf 2026-07-11 18:24:23 +02:00
parent cfde9b2cd7
commit 8cdea8ff7e
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
README.md
View file

@ -16,7 +16,7 @@ the same discipline as the four `*-ed25519-verified` subject corpora.
| 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 | ConsRec binding + Theorem 3 assembly (extractCons) | in progress (S5): stage-1 arithmetic/list infrastructure done (kbelow_prefix_eq, take surgery); stage-1 infra + extractConsNode extractor DEFINED; binding proof (steps 1-2) + extractCons assembly = stage 3 |
| L6b | ConsRec binding + Theorem 3 assembly (extractCons) | in progress (S5): stage-1 arithmetic/list infrastructure done (kbelow_prefix_eq, take surgery); stage-1 infra + extractConsNode extractor DEFINED (faithful to ConsRec by inspection — NOT yet machine-checked); binding proof + extractCons assembly = stage 3 |
| L6 | pin-store state machine safety (Proposition 1) | pending |
## Discipline (identical to the subject corpora)