[Dijkstra] CIP-159-11: PoV property proofs (#1123)#1169

Closed

williamdemeo wants to merge 14 commits into

1123-cip-159-11-prove-pov-and-invariants

Commits on May 5, 2026

[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)
williamdemeo
committed
add justification for batch processing of direct deposits
williamdemeo
committed
LEDGER-V: forbid direct deposits to credentials deregistered in same batch
williamdemeo
committed

Commits on May 6, 2026

Apply CIP-159 direct deposits per-transaction, not batch-wide
williamdemeo
committed
[Dijkstra] CIP-159-05: Update UTxO rules for direct deposits and balance intervals (#1117)
williamdemeo
committed
[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)
williamdemeo
committed
CIP-159-11: Initial PoV property module skeletons (#1123)
williamdemeo
committed
`indexedSumᵛ'-∪` and `sumConstZero` have proofs!
williamdemeo
committed
CIP-159-11: applyWithdrawals-pov and new library lemmas (#1123)
williamdemeo
committed
CIP-159-11: LEDGER-pov structure with LEDGER-I proved (#1123)
williamdemeo
committed
CIP-159-11: LEDGER-pov fully structured, all holes filled (#1123)
williamdemeo
committed
feat(dijkstra): add UTXO and UTXOW preservation-of-value modules
williamdemeo
committed
feat(dijkstra): discharge `coin-of-{consumed,produced}Batch` in UTXO PoV
williamdemeo
committed
feat(Dijkstra/Ledger/PoV): prove SUBLEDGERS-utxo-coin
williamdemeo
committed