[Dijkstra] CIP-159-11c: Prove LEDGER preservation of value (#1187)#1203

Draft

williamdemeo wants to merge 13 commits into

1187-dijkstra-NEW-ENTITIES-ledger-pov

Commits on Jun 30, 2026

new helpers in Ledger.Prelude and Certs PoV
williamdemeo
committed
Add applyWithdrawals-pov and applyDirectDeposits-pov
williamdemeo
committed
Add ENTITIES preservation-of-value
williamdemeo
committed
Bridge CERTS evolution to closed-form cert-deposit accounting
williamdemeo
committed
add proof of Is-just-isPoolRegistered⇒∈-dom
williamdemeo
committed
old version of Ledger PoV
williamdemeo
committed
Fix two preservation-of-value soundness bugs (deposit sign-swap; uncounted gov deposits)

claude
authored and
williamdemeo
committed
Document post-A&B interface delta for LEDGER-pov assembly

claude
authored and
williamdemeo
committed
Add (then delete) Agda typecheck skill + SessionStart hook for Nix toolchain

claude
authored and
williamdemeo
committed
[Dijkstra] LEDGER-pov: complete the proof and address Copilot review comments.

claude
authored and
williamdemeo
committed
add props modules to barrel; other improvements
williamdemeo
committed
Make getCoin on CertState total (rewards + deposits)

claude
authored and
williamdemeo
committed
simplifications
williamdemeo
committed