Apr 30, 8-9 PM (28)
Apr 30, 9-10 PM (13)
Apr 30, 10-11 PM (25)
Apr 30, 11-12 AM (15)
May 01, 12-1 AM (18)
May 01, 1-2 AM (15)
May 01, 2-3 AM (6)
May 01, 3-4 AM (7)
May 01, 4-5 AM (3)
May 01, 5-6 AM (5)
May 01, 6-7 AM (8)
May 01, 7-8 AM (15)
May 01, 8-9 AM (24)
May 01, 9-10 AM (17)
May 01, 10-11 AM (16)
May 01, 11-12 PM (17)
May 01, 12-1 PM (39)
May 01, 1-2 PM (32)
May 01, 2-3 PM (19)
May 01, 3-4 PM (16)
May 01, 4-5 PM (25)
May 01, 5-6 PM (11)
May 01, 6-7 PM (20)
May 01, 7-8 PM (22)
May 01, 8-9 PM (65)
May 01, 9-10 PM (15)
May 01, 10-11 PM (40)
May 01, 11-12 AM (61)
May 02, 12-1 AM (6)
May 02, 1-2 AM (11)
May 02, 2-3 AM (5)
May 02, 3-4 AM (8)
May 02, 4-5 AM (6)
May 02, 5-6 AM (2)
May 02, 6-7 AM (2)
May 02, 7-8 AM (14)
May 02, 8-9 AM (7)
May 02, 9-10 AM (8)
May 02, 10-11 AM (11)
May 02, 11-12 PM (7)
May 02, 12-1 PM (7)
May 02, 1-2 PM (3)
May 02, 2-3 PM (14)
May 02, 3-4 PM (9)
May 02, 4-5 PM (27)
May 02, 5-6 PM (9)
May 02, 6-7 PM (29)
May 02, 7-8 PM (11)
May 02, 8-9 PM (15)
May 02, 9-10 PM (1)
May 02, 10-11 PM (20)
May 02, 11-12 AM (18)
May 03, 12-1 AM (8)
May 03, 1-2 AM (1)
May 03, 2-3 AM (4)
May 03, 3-4 AM (7)
May 03, 4-5 AM (1)
May 03, 5-6 AM (4)
May 03, 6-7 AM (32)
May 03, 7-8 AM (5)
May 03, 8-9 AM (1)
May 03, 9-10 AM (3)
May 03, 10-11 AM (10)
May 03, 11-12 PM (11)
May 03, 12-1 PM (16)
May 03, 1-2 PM (11)
May 03, 2-3 PM (2)
May 03, 3-4 PM (2)
May 03, 4-5 PM (5)
May 03, 5-6 PM (0)
May 03, 6-7 PM (5)
May 03, 7-8 PM (6)
May 03, 8-9 PM (8)
May 03, 9-10 PM (15)
May 03, 10-11 PM (23)
May 03, 11-12 AM (17)
May 04, 12-1 AM (4)
May 04, 1-2 AM (4)
May 04, 2-3 AM (10)
May 04, 3-4 AM (9)
May 04, 4-5 AM (5)
May 04, 5-6 AM (6)
May 04, 6-7 AM (6)
May 04, 7-8 AM (28)
May 04, 8-9 AM (26)
May 04, 9-10 AM (43)
May 04, 10-11 AM (36)
May 04, 11-12 PM (61)
May 04, 12-1 PM (34)
May 04, 1-2 PM (49)
May 04, 2-3 PM (64)
May 04, 3-4 PM (33)
May 04, 4-5 PM (64)
May 04, 5-6 PM (49)
May 04, 6-7 PM (13)
May 04, 7-8 PM (32)
May 04, 8-9 PM (45)
May 04, 9-10 PM (9)
May 04, 10-11 PM (54)
May 04, 11-12 AM (24)
May 05, 12-1 AM (4)
May 05, 1-2 AM (5)
May 05, 2-3 AM (5)
May 05, 3-4 AM (11)
May 05, 4-5 AM (11)
May 05, 5-6 AM (50)
May 05, 6-7 AM (16)
May 05, 7-8 AM (37)
May 05, 8-9 AM (81)
May 05, 9-10 AM (68)
May 05, 10-11 AM (34)
May 05, 11-12 PM (72)
May 05, 12-1 PM (115)
May 05, 1-2 PM (118)
May 05, 2-3 PM (66)
May 05, 3-4 PM (91)
May 05, 4-5 PM (41)
May 05, 5-6 PM (26)
May 05, 6-7 PM (28)
May 05, 7-8 PM (73)
May 05, 8-9 PM (31)
May 05, 9-10 PM (18)
May 05, 10-11 PM (25)
May 05, 11-12 AM (17)
May 06, 12-1 AM (10)
May 06, 1-2 AM (5)
May 06, 2-3 AM (9)
May 06, 3-4 AM (23)
May 06, 4-5 AM (7)
May 06, 5-6 AM (13)
May 06, 6-7 AM (30)
May 06, 7-8 AM (11)
May 06, 8-9 AM (106)
May 06, 9-10 AM (27)
May 06, 10-11 AM (41)
May 06, 11-12 PM (46)
May 06, 12-1 PM (86)
May 06, 1-2 PM (53)
May 06, 2-3 PM (43)
May 06, 3-4 PM (33)
May 06, 4-5 PM (18)
May 06, 5-6 PM (8)
May 06, 6-7 PM (12)
May 06, 7-8 PM (26)
May 06, 8-9 PM (13)
May 06, 9-10 PM (9)
May 06, 10-11 PM (30)
May 06, 11-12 AM (23)
May 07, 12-1 AM (7)
May 07, 1-2 AM (2)
May 07, 2-3 AM (1)
May 07, 3-4 AM (10)
May 07, 4-5 AM (4)
May 07, 5-6 AM (33)
May 07, 6-7 AM (97)
May 07, 7-8 AM (235)
May 07, 8-9 AM (42)
May 07, 9-10 AM (29)
May 07, 10-11 AM (55)
May 07, 11-12 PM (39)
May 07, 12-1 PM (46)
May 07, 1-2 PM (46)
May 07, 2-3 PM (47)
May 07, 3-4 PM (42)
May 07, 4-5 PM (58)
May 07, 5-6 PM (10)
May 07, 6-7 PM (24)
May 07, 7-8 PM (30)
May 07, 8-9 PM (4)
4,318 commits this week Apr 30, 2026 - May 07, 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.
LEDGER-V: forbid direct deposits to credentials deregistered in same batch
`applyDirectDeposits` uses `∪⁺` (union-with-addition) on the `rewards`
map, so a credential not present in `RewardsOf certState₂` is added as a
new entry rather than rejected.  The pre-existing SUBUTXO/UTXO premise
`dom (DirectDepositsOf tx) ⊆ dom (AccountBalancesOf Γ)` only checks
against the pre-batch balances `RewardsOf certState₀`, so it does not
catch the case where a credential is registered pre-batch, deregistered
during `CERTS`, and direct-deposited to in the same batch.  Without the
new premise, the resulting `certStateFinal` is internally inconsistent:
the credential has a positive `rewards` entry but no corresponding
`voteDelegs`, `stakeDelegs`, or `deposits` entry — effectively re-
registering the credential without a key deposit.

Add the phase-1 premise

    dom (allDirectDeposits tx) ⊆ dom (RewardsOf certState₂)

to `LEDGER-V` to rule this out.  Filtering `allDirectDeposits tx` by
`dom (RewardsOf certState₂)` would be an alternative, but it would
silently destroy user funds when a deposit and a deregistration race in
the same batch.  The premise is symmetric to (and complements) the
existing pre-batch SUBUTXO/UTXO check.

Update `Ledger/Properties/Computational.lagda.md` for the new premise,
and pass `UTxOStateOf s₁` explicitly to `computeUtxow` in the LEDGER
valid branch (the previous `_` resolved by chained unification through
the LEDGER-V constructor, which was fragile and obscured intent).

TODO: fix `Ledger/Properties/Computational.lagda.md`; it's choking on
the new premise.
[Dijkstra] CIP-159-10: Apply batch-wide direct deposits in LEDGER rule (#1122)
After all sub-rule transitions (`SUBLEDGERS`, `CERTS`, `GOVS`, `UTXOW`),
apply batch-wide direct deposits to the final CertState via
`applyDirectDeposits` and `allDirectDeposits`.

`Ledger.lagda.md`:
+  Update `LEDGER-V` output: compute `certStateFinal` by applying
   `allDirectDeposits` to `certState₂`, use `certStateFinal` in the
   output `LedgerState` and in `rmOrphanDRepVotes`;
+  `LEDGER-I` unchanged (invalid batches don't apply deposits);
+  Document direct deposit application ordering and phantom asset
   prevention rationale.

`Ledger/Properties/Computational.lagda.md`:
+  Update `computeProof` valid branch to compute `certStateFinal` and use
   it in the output `LedgerState`.
+  Clean up redundant code.
Apply CIP-159 direct deposits per-transaction, not batch-wide
Each transaction's `txDirectDeposits` are now applied to the threaded
`CertState` immediately after that transaction's `CERTS` step, replacing
the batch-wide application introduced earlier on this branch.

  * `SUBLEDGER-V` applies `DirectDepositsOf stx` to `certState₁` after
    `CERTS` and emits the result.
  * `LEDGER-V` still applies the top-level transaction's deposits to
    `certState₂` after the top-level `CERTS`, but the premise now bounds
    `dom (DirectDepositsOf tx)` rather than the batch aggregate
    `dom (allDirectDeposits tx)`.
  * `certStateWithDDeps` is generalised to
    `∀ {ℓ} → Tx ℓ → CertState → CertState` so both rules can invoke it
    with the local `DirectDepositsOf`.

The original draft of this branch argued that batch-wide application
made CIP-159's phantom-asset prohibition manifest in the rule
structure.  Per-transaction application is equally safe: the prohibition
is enforced separately by `NoPhantomWithdrawals` in the `Utxo` module,
which bounds batch-wide withdrawal totals against the `accountBalances`
field of `UTxOEnv`/`SubUTxOEnv` — fixed at the pre-batch snapshot
`RewardsOf certState₀` regardless of when (or how) deposits are applied
to the threaded `CertState`.  Per-transaction application also mirrors
the Haskell ledger executor's sequential per-transaction processing,
which simplifies the conformance proof and avoids a structural gap
between the spec and the implementation.

A direct-deposit registration premise is added to each rule to prevent
`applyDirectDeposits` from silently re-introducing a credential into
`rewards` after deregistration earlier in the same transaction:

  * `SUBLEDGER-V` requires
    `dom (DirectDepositsOf stx) ⊆ dom (RewardsOf certState₁)`.
  * `LEDGER-V` requires
    `dom (DirectDepositsOf tx)  ⊆ dom (RewardsOf certState₂)`.

The check is local to each transaction's post-`CERTS` state, so a
sub-transaction whose deposit targets a credential deregistered by an
earlier sub-transaction in the same batch will fail the premise.

`Computational-SUBLEDGER` and `Computational-LEDGER` are updated to
dispatch on these decidable premises in `computeProof` and
`completeness`.  `depositsChange` is unaffected: it reads only the
protocol-deposit fields of `DState`/`PState`/`GState`, which
`applyDirectDeposits` does not touch.

Refs: #1122
Add specification index page with format motivation
Introduces a new Specifications section under References on the website.
The index page documents:
- The specification format (Quint-flavored pseudocode, concrete examples,
  module-qualified references, stable rule/invariant IDs)
- Design principles grounded in research on LLM-consumable specs
- Prior art survey (Ethereum consensus specs, IBC/Cosmos, SDD tools)
- Limitations of the existing Agda spec that motivate this work
- Relationship to other documentation layers (L1-L5)