Home / IntersectMBO / formal-ledger-specifications
May 01, 9-10 AM (0)
May 01, 10-11 AM (0)
May 01, 11-12 PM (0)
May 01, 12-1 PM (0)
May 01, 1-2 PM (1)
May 01, 2-3 PM (0)
May 01, 3-4 PM (0)
May 01, 4-5 PM (0)
May 01, 5-6 PM (0)
May 01, 6-7 PM (0)
May 01, 7-8 PM (0)
May 01, 8-9 PM (0)
May 01, 9-10 PM (0)
May 01, 10-11 PM (0)
May 01, 11-12 AM (0)
May 02, 12-1 AM (0)
May 02, 1-2 AM (0)
May 02, 2-3 AM (0)
May 02, 3-4 AM (0)
May 02, 4-5 AM (0)
May 02, 5-6 AM (0)
May 02, 6-7 AM (0)
May 02, 7-8 AM (0)
May 02, 8-9 AM (0)
May 02, 9-10 AM (0)
May 02, 10-11 AM (0)
May 02, 11-12 PM (0)
May 02, 12-1 PM (0)
May 02, 1-2 PM (0)
May 02, 2-3 PM (0)
May 02, 3-4 PM (0)
May 02, 4-5 PM (0)
May 02, 5-6 PM (0)
May 02, 6-7 PM (0)
May 02, 7-8 PM (0)
May 02, 8-9 PM (0)
May 02, 9-10 PM (0)
May 02, 10-11 PM (0)
May 02, 11-12 AM (0)
May 03, 12-1 AM (0)
May 03, 1-2 AM (0)
May 03, 2-3 AM (0)
May 03, 3-4 AM (0)
May 03, 4-5 AM (0)
May 03, 5-6 AM (0)
May 03, 6-7 AM (0)
May 03, 7-8 AM (0)
May 03, 8-9 AM (0)
May 03, 9-10 AM (0)
May 03, 10-11 AM (0)
May 03, 11-12 PM (0)
May 03, 12-1 PM (0)
May 03, 1-2 PM (0)
May 03, 2-3 PM (0)
May 03, 3-4 PM (0)
May 03, 4-5 PM (0)
May 03, 5-6 PM (0)
May 03, 6-7 PM (0)
May 03, 7-8 PM (0)
May 03, 8-9 PM (0)
May 03, 9-10 PM (0)
May 03, 10-11 PM (0)
May 03, 11-12 AM (0)
May 04, 12-1 AM (0)
May 04, 1-2 AM (0)
May 04, 2-3 AM (0)
May 04, 3-4 AM (0)
May 04, 4-5 AM (0)
May 04, 5-6 AM (0)
May 04, 6-7 AM (0)
May 04, 7-8 AM (0)
May 04, 8-9 AM (0)
May 04, 9-10 AM (1)
May 04, 10-11 AM (0)
May 04, 11-12 PM (0)
May 04, 12-1 PM (0)
May 04, 1-2 PM (0)
May 04, 2-3 PM (0)
May 04, 3-4 PM (0)
May 04, 4-5 PM (0)
May 04, 5-6 PM (0)
May 04, 6-7 PM (0)
May 04, 7-8 PM (0)
May 04, 8-9 PM (0)
May 04, 9-10 PM (0)
May 04, 10-11 PM (0)
May 04, 11-12 AM (0)
May 05, 12-1 AM (0)
May 05, 1-2 AM (0)
May 05, 2-3 AM (0)
May 05, 3-4 AM (0)
May 05, 4-5 AM (0)
May 05, 5-6 AM (0)
May 05, 6-7 AM (0)
May 05, 7-8 AM (0)
May 05, 8-9 AM (0)
May 05, 9-10 AM (0)
May 05, 10-11 AM (0)
May 05, 11-12 PM (0)
May 05, 12-1 PM (0)
May 05, 1-2 PM (0)
May 05, 2-3 PM (0)
May 05, 3-4 PM (0)
May 05, 4-5 PM (0)
May 05, 5-6 PM (0)
May 05, 6-7 PM (0)
May 05, 7-8 PM (0)
May 05, 8-9 PM (0)
May 05, 9-10 PM (0)
May 05, 10-11 PM (0)
May 05, 11-12 AM (0)
May 06, 12-1 AM (0)
May 06, 1-2 AM (0)
May 06, 2-3 AM (0)
May 06, 3-4 AM (0)
May 06, 4-5 AM (0)
May 06, 5-6 AM (0)
May 06, 6-7 AM (0)
May 06, 7-8 AM (0)
May 06, 8-9 AM (0)
May 06, 9-10 AM (0)
May 06, 10-11 AM (0)
May 06, 11-12 PM (0)
May 06, 12-1 PM (0)
May 06, 1-2 PM (0)
May 06, 2-3 PM (0)
May 06, 3-4 PM (0)
May 06, 4-5 PM (0)
May 06, 5-6 PM (0)
May 06, 6-7 PM (0)
May 06, 7-8 PM (0)
May 06, 8-9 PM (0)
May 06, 9-10 PM (0)
May 06, 10-11 PM (0)
May 06, 11-12 AM (0)
May 07, 12-1 AM (0)
May 07, 1-2 AM (0)
May 07, 2-3 AM (0)
May 07, 3-4 AM (0)
May 07, 4-5 AM (0)
May 07, 5-6 AM (0)
May 07, 6-7 AM (0)
May 07, 7-8 AM (1)
May 07, 8-9 AM (1)
May 07, 9-10 AM (0)
May 07, 10-11 AM (0)
May 07, 11-12 PM (0)
May 07, 12-1 PM (0)
May 07, 1-2 PM (0)
May 07, 2-3 PM (0)
May 07, 3-4 PM (0)
May 07, 4-5 PM (0)
May 07, 5-6 PM (0)
May 07, 6-7 PM (1)
May 07, 7-8 PM (1)
May 07, 8-9 PM (0)
May 07, 9-10 PM (0)
May 07, 10-11 PM (0)
May 07, 11-12 AM (0)
May 08, 12-1 AM (0)
May 08, 1-2 AM (0)
May 08, 2-3 AM (0)
May 08, 3-4 AM (0)
May 08, 4-5 AM (0)
May 08, 5-6 AM (0)
May 08, 6-7 AM (0)
May 08, 7-8 AM (0)
May 08, 8-9 AM (0)
May 08, 9-10 AM (0)
6 commits this week May 01, 2026 - May 08, 2026
[Dijkstra] CIP-159-10: Apply direct deposits in POST-CERT (#1122)
Per @carlostome's review of #1161, move CIP-159 direct-deposit
application out of the LEDGER/SUBLEDGER orchestration rules and into
the POST-CERT sub-rule of CERTS, alongside the existing voteDelegs
filtering.

CertEnv gains a sixth field, directDeposits, populated by LEDGER-V
(DirectDepositsOf tx) and SUBLEDGER-V (DirectDepositsOf stx) when
constructing each CERTS invocation's environment.  POST-CERT (CERT-post)
gains a premise dom directDeposits ⊆ dom rewards and updates its
post-state's rewards to rewards ∪⁺ directDeposits.

SUBLEDGER-V and LEDGER-V revert to threading-only: certStateWithDDeps,
the certStateFinal let-binding, and the dom-check premises are removed.
Computational instances are updated correspondingly.

Per-transaction semantics are preserved (POST-CERT runs at the end of
each transaction's CERTS invocation).  Phantom-asset prevention via
NoPhantomWithdrawals is unaffected (accountBalances is fixed at the
pre-batch snapshot).  depositsChange remains orthogonal
(applyDirectDeposits touches rewards only; calculateDepositsChange
reads deposits only).

Direct-deposit documentation moves from Ledger.lagda.md to the POST-CERT
section of Certs.lagda.md.