zeekayandHanzo Dev eb1a184ccb proof: caught-up by acceptance not store presence (LP-304 layer 8) ...

Add the store-presence-fixed-point theorem (a node holding gossiped-but-unaccepted
blocks reports caught-up at its stale height forever), the acceptance-converges
theorem (cert-gated accept of held blocks reaches the frontier), and the
frozen-cache lemma (recognition must read the advancing finalised ledger, not the
plugin LastAccepted cache). Proven on mainnet luxd-2 (1082780 -> 1082796).

Co-authored-by: Hanzo Dev <[email protected]>

2026-09-17 13:05:50 -07:00

243 KiB

Raw Permalink History

View Raw