Apr 09, 11-12 AM (15)
Apr 10, 12-1 AM (5)
Apr 10, 1-2 AM (4)
Apr 10, 2-3 AM (4)
Apr 10, 3-4 AM (12)
Apr 10, 4-5 AM (3)
Apr 10, 5-6 AM (9)
Apr 10, 6-7 AM (30)
Apr 10, 7-8 AM (46)
Apr 10, 8-9 AM (47)
Apr 10, 9-10 AM (20)
Apr 10, 10-11 AM (61)
Apr 10, 11-12 PM (70)
Apr 10, 12-1 PM (46)
Apr 10, 1-2 PM (24)
Apr 10, 2-3 PM (36)
Apr 10, 3-4 PM (33)
Apr 10, 4-5 PM (38)
Apr 10, 5-6 PM (30)
Apr 10, 6-7 PM (11)
Apr 10, 7-8 PM (13)
Apr 10, 8-9 PM (7)
Apr 10, 9-10 PM (25)
Apr 10, 10-11 PM (47)
Apr 10, 11-12 AM (18)
Apr 11, 12-1 AM (6)
Apr 11, 1-2 AM (4)
Apr 11, 2-3 AM (2)
Apr 11, 3-4 AM (0)
Apr 11, 4-5 AM (8)
Apr 11, 5-6 AM (4)
Apr 11, 6-7 AM (5)
Apr 11, 7-8 AM (7)
Apr 11, 8-9 AM (3)
Apr 11, 9-10 AM (0)
Apr 11, 10-11 AM (10)
Apr 11, 11-12 PM (4)
Apr 11, 12-1 PM (7)
Apr 11, 1-2 PM (3)
Apr 11, 2-3 PM (7)
Apr 11, 3-4 PM (12)
Apr 11, 4-5 PM (18)
Apr 11, 5-6 PM (39)
Apr 11, 6-7 PM (0)
Apr 11, 7-8 PM (0)
Apr 11, 8-9 PM (2)
Apr 11, 9-10 PM (1)
Apr 11, 10-11 PM (19)
Apr 11, 11-12 AM (23)
Apr 12, 12-1 AM (4)
Apr 12, 1-2 AM (1)
Apr 12, 2-3 AM (9)
Apr 12, 3-4 AM (2)
Apr 12, 4-5 AM (0)
Apr 12, 5-6 AM (2)
Apr 12, 6-7 AM (2)
Apr 12, 7-8 AM (1)
Apr 12, 8-9 AM (3)
Apr 12, 9-10 AM (2)
Apr 12, 10-11 AM (11)
Apr 12, 11-12 PM (4)
Apr 12, 12-1 PM (1)
Apr 12, 1-2 PM (10)
Apr 12, 2-3 PM (24)
Apr 12, 3-4 PM (7)
Apr 12, 4-5 PM (7)
Apr 12, 5-6 PM (17)
Apr 12, 6-7 PM (2)
Apr 12, 7-8 PM (1)
Apr 12, 8-9 PM (8)
Apr 12, 9-10 PM (9)
Apr 12, 10-11 PM (38)
Apr 12, 11-12 AM (23)
Apr 13, 12-1 AM (5)
Apr 13, 1-2 AM (6)
Apr 13, 2-3 AM (5)
Apr 13, 3-4 AM (6)
Apr 13, 4-5 AM (2)
Apr 13, 5-6 AM (18)
Apr 13, 6-7 AM (23)
Apr 13, 7-8 AM (39)
Apr 13, 8-9 AM (43)
Apr 13, 9-10 AM (51)
Apr 13, 10-11 AM (75)
Apr 13, 11-12 PM (35)
Apr 13, 12-1 PM (55)
Apr 13, 1-2 PM (80)
Apr 13, 2-3 PM (42)
Apr 13, 3-4 PM (20)
Apr 13, 4-5 PM (31)
Apr 13, 5-6 PM (25)
Apr 13, 6-7 PM (18)
Apr 13, 7-8 PM (13)
Apr 13, 8-9 PM (15)
Apr 13, 9-10 PM (22)
Apr 13, 10-11 PM (29)
Apr 13, 11-12 AM (13)
Apr 14, 12-1 AM (6)
Apr 14, 1-2 AM (8)
Apr 14, 2-3 AM (15)
Apr 14, 3-4 AM (4)
Apr 14, 4-5 AM (4)
Apr 14, 5-6 AM (63)
Apr 14, 6-7 AM (50)
Apr 14, 7-8 AM (100)
Apr 14, 8-9 AM (33)
Apr 14, 9-10 AM (21)
Apr 14, 10-11 AM (34)
Apr 14, 11-12 PM (42)
Apr 14, 12-1 PM (72)
Apr 14, 1-2 PM (96)
Apr 14, 2-3 PM (44)
Apr 14, 3-4 PM (35)
Apr 14, 4-5 PM (9)
Apr 14, 5-6 PM (20)
Apr 14, 6-7 PM (22)
Apr 14, 7-8 PM (14)
Apr 14, 8-9 PM (10)
Apr 14, 9-10 PM (11)
Apr 14, 10-11 PM (24)
Apr 14, 11-12 AM (24)
Apr 15, 12-1 AM (3)
Apr 15, 1-2 AM (9)
Apr 15, 2-3 AM (8)
Apr 15, 3-4 AM (1)
Apr 15, 4-5 AM (1)
Apr 15, 5-6 AM (32)
Apr 15, 6-7 AM (6)
Apr 15, 7-8 AM (18)
Apr 15, 8-9 AM (46)
Apr 15, 9-10 AM (40)
Apr 15, 10-11 AM (126)
Apr 15, 11-12 PM (53)
Apr 15, 12-1 PM (59)
Apr 15, 1-2 PM (43)
Apr 15, 2-3 PM (45)
Apr 15, 3-4 PM (28)
Apr 15, 4-5 PM (43)
Apr 15, 5-6 PM (21)
Apr 15, 6-7 PM (33)
Apr 15, 7-8 PM (15)
Apr 15, 8-9 PM (17)
Apr 15, 9-10 PM (5)
Apr 15, 10-11 PM (20)
Apr 15, 11-12 AM (16)
Apr 16, 12-1 AM (12)
Apr 16, 1-2 AM (6)
Apr 16, 2-3 AM (7)
Apr 16, 3-4 AM (3)
Apr 16, 4-5 AM (4)
Apr 16, 5-6 AM (8)
Apr 16, 6-7 AM (33)
Apr 16, 7-8 AM (31)
Apr 16, 8-9 AM (29)
Apr 16, 9-10 AM (27)
Apr 16, 10-11 AM (50)
Apr 16, 11-12 PM (56)
Apr 16, 12-1 PM (57)
Apr 16, 1-2 PM (28)
Apr 16, 2-3 PM (35)
Apr 16, 3-4 PM (45)
Apr 16, 4-5 PM (46)
Apr 16, 5-6 PM (56)
Apr 16, 6-7 PM (15)
Apr 16, 7-8 PM (68)
Apr 16, 8-9 PM (38)
Apr 16, 9-10 PM (6)
Apr 16, 10-11 PM (23)
Apr 16, 11-12 AM (11)
3,825 commits this week Apr 10, 2026 - Apr 17, 2026
williamdemeo
williamdemeo · · formal-ledger-specifications
CIP-159-11: LEDGER-pov structure with LEDGER-I proved (#1123) 
State and partially prove the Dijkstra LEDGER preservation-of-value
theorem with the corrected HasCoin-LedgerState that includes deposits.

- LEDGER-I (invalid case): Fully proved via utxow-pov-invalid.
- LEDGER-V (valid case): Equational chain with holes, to be filled.

The HasCoin-LedgerState total is:
  getCoin utxoSt + rewardsBalance(certState) + coinFromDeposits(certState)

Key insight: SUBLEDGERS-pov cannot be proved independently because
individual SUBUTXO rules have no balance premise — only the batch-level
consumedBatch ≡ producedBatch constrains the total. The LEDGER-V proof
must reason about the entire step at once.
431ec1bc · 1123-cip-159-11-prove-pov-and-invariants · 4/233 ++ 57 --
Showing 25 of 3825 recent commits.