Artifacts generated from 2bdc4c2dd1f07efed63ce8101e066b97c66c5909
Home /
Input Output /
formal-ledger-specifications
May 21, 1-2 PM (1)
May 21, 2-3 PM (0)
May 21, 3-4 PM (0)
May 21, 4-5 PM (0)
May 21, 5-6 PM (0)
May 21, 6-7 PM (1)
May 21, 7-8 PM (0)
May 21, 8-9 PM (0)
May 21, 9-10 PM (0)
May 21, 10-11 PM (1)
May 21, 11-12 AM (0)
May 22, 12-1 AM (0)
May 22, 1-2 AM (0)
May 22, 2-3 AM (0)
May 22, 3-4 AM (0)
May 22, 4-5 AM (0)
May 22, 5-6 AM (0)
May 22, 6-7 AM (0)
May 22, 7-8 AM (0)
May 22, 8-9 AM (0)
May 22, 9-10 AM (0)
May 22, 10-11 AM (0)
May 22, 11-12 PM (0)
May 22, 12-1 PM (0)
May 22, 1-2 PM (0)
May 22, 2-3 PM (0)
May 22, 3-4 PM (0)
May 22, 4-5 PM (0)
May 22, 5-6 PM (0)
May 22, 6-7 PM (0)
May 22, 7-8 PM (0)
May 22, 8-9 PM (0)
May 22, 9-10 PM (0)
May 22, 10-11 PM (0)
May 22, 11-12 AM (0)
May 23, 12-1 AM (0)
May 23, 1-2 AM (0)
May 23, 2-3 AM (0)
May 23, 3-4 AM (0)
May 23, 4-5 AM (0)
May 23, 5-6 AM (0)
May 23, 6-7 AM (0)
May 23, 7-8 AM (0)
May 23, 8-9 AM (0)
May 23, 9-10 AM (0)
May 23, 10-11 AM (0)
May 23, 11-12 PM (0)
May 23, 12-1 PM (0)
May 23, 1-2 PM (0)
May 23, 2-3 PM (0)
May 23, 3-4 PM (0)
May 23, 4-5 PM (0)
May 23, 5-6 PM (0)
May 23, 6-7 PM (0)
May 23, 7-8 PM (0)
May 23, 8-9 PM (0)
May 23, 9-10 PM (0)
May 23, 10-11 PM (0)
May 23, 11-12 AM (0)
May 24, 12-1 AM (0)
May 24, 1-2 AM (0)
May 24, 2-3 AM (0)
May 24, 3-4 AM (0)
May 24, 4-5 AM (0)
May 24, 5-6 AM (0)
May 24, 6-7 AM (0)
May 24, 7-8 AM (0)
May 24, 8-9 AM (0)
May 24, 9-10 AM (0)
May 24, 10-11 AM (0)
May 24, 11-12 PM (0)
May 24, 12-1 PM (0)
May 24, 1-2 PM (0)
May 24, 2-3 PM (0)
May 24, 3-4 PM (0)
May 24, 4-5 PM (0)
May 24, 5-6 PM (0)
May 24, 6-7 PM (0)
May 24, 7-8 PM (0)
May 24, 8-9 PM (0)
May 24, 9-10 PM (0)
May 24, 10-11 PM (0)
May 24, 11-12 AM (0)
May 25, 12-1 AM (0)
May 25, 1-2 AM (0)
May 25, 2-3 AM (0)
May 25, 3-4 AM (0)
May 25, 4-5 AM (0)
May 25, 5-6 AM (0)
May 25, 6-7 AM (0)
May 25, 7-8 AM (0)
May 25, 8-9 AM (3)
May 25, 9-10 AM (0)
May 25, 10-11 AM (0)
May 25, 11-12 PM (0)
May 25, 12-1 PM (0)
May 25, 1-2 PM (0)
May 25, 2-3 PM (0)
May 25, 3-4 PM (0)
May 25, 4-5 PM (0)
May 25, 5-6 PM (0)
May 25, 6-7 PM (0)
May 25, 7-8 PM (0)
May 25, 8-9 PM (0)
May 25, 9-10 PM (0)
May 25, 10-11 PM (0)
May 25, 11-12 AM (0)
May 26, 12-1 AM (0)
May 26, 1-2 AM (0)
May 26, 2-3 AM (0)
May 26, 3-4 AM (0)
May 26, 4-5 AM (0)
May 26, 5-6 AM (0)
May 26, 6-7 AM (4)
May 26, 7-8 AM (5)
May 26, 8-9 AM (0)
May 26, 9-10 AM (1)
May 26, 10-11 AM (0)
May 26, 11-12 PM (0)
May 26, 12-1 PM (0)
May 26, 1-2 PM (1)
May 26, 2-3 PM (7)
May 26, 3-4 PM (0)
May 26, 4-5 PM (0)
May 26, 5-6 PM (0)
May 26, 6-7 PM (0)
May 26, 7-8 PM (0)
May 26, 8-9 PM (0)
May 26, 9-10 PM (0)
May 26, 10-11 PM (0)
May 26, 11-12 AM (0)
May 27, 12-1 AM (0)
May 27, 1-2 AM (0)
May 27, 2-3 AM (0)
May 27, 3-4 AM (1)
May 27, 4-5 AM (0)
May 27, 5-6 AM (0)
May 27, 6-7 AM (0)
May 27, 7-8 AM (0)
May 27, 8-9 AM (0)
May 27, 9-10 AM (1)
May 27, 10-11 AM (0)
May 27, 11-12 PM (0)
May 27, 12-1 PM (0)
May 27, 1-2 PM (0)
May 27, 2-3 PM (0)
May 27, 3-4 PM (0)
May 27, 4-5 PM (0)
May 27, 5-6 PM (0)
May 27, 6-7 PM (0)
May 27, 7-8 PM (0)
May 27, 8-9 PM (0)
May 27, 9-10 PM (1)
May 27, 10-11 PM (1)
May 27, 11-12 AM (0)
May 28, 12-1 AM (0)
May 28, 1-2 AM (1)
May 28, 2-3 AM (0)
May 28, 3-4 AM (0)
May 28, 4-5 AM (3)
May 28, 5-6 AM (0)
May 28, 6-7 AM (0)
May 28, 7-8 AM (0)
May 28, 8-9 AM (0)
May 28, 9-10 AM (1)
May 28, 10-11 AM (0)
May 28, 11-12 PM (2)
May 28, 12-1 PM (1)
May 28, 1-2 PM (4)
40 commits this week
May 21, 2026
-
May 28, 2026
Artifacts generated from af302d66e6331745fb2e47d5ff44584449d06189
Cleanup Foreign/ modules in favour of this in agda-stdlib-meta (#1211)
Fix hs-src build (2)
Fix hs-src build
Trace imports during build
Artifacts generated from 27fbce25f7a55e044c0dcb810ab637a5756044ad
Artifacts generated from 379377c30032f10ace18f986940018da70e0899c
Add Certs PoV: per-step ≡ᵐᵗ + coin bridges, RTC lift
New modules under src/Ledger/Dijkstra/Specification/Certs/Properties/: + PoVLemmas.lagda.md (CERT-level) + PoV.lagda.md (CERTS-level) PoVLemmas exports: + CERT-pov: preservation of value at one CERT step + CERT-pots-≡ᵐᵗ: per-step ≡ᵐ-componentwise triple bridge + CERT-coinFromDeposits-step: per-step coin bridge (derived) + Triple machinery: pots, coinFromDeposits-pots, updateCertDeposit-list, pots-updateCertDeposits + PoolDepositsAligned, Is-just-isPoolRegistered⇒∈-dom PoV exports a bundled Certs-PoV module parameterised by indexedSumᵛ'-∪ and PoolDepositsAligned-CERT, providing: + CERTS-pov: preservation across the closure + CERTS-Deposits-Bridge.CERTS-coinFromDeposits-updateCertDeposits: the closed-form coin bridge consumed by LEDGER-pov The triple-form per-step bridge from the previous Ledger-PoV branch required a deferred propositional equation m ∪ˡ ❴ k , v ❵ ≡ m (when k ∈ dom m). This PR drops that parameter, using instead the upstream ≡ᵐ-componentwise singleton-∈-∪ˡ plumbed through the closed form via ∪⁺-cong-r, ∪ˡ-cong, restrict-cong, and collapsed to a coin equality via ≡ᵉ-getCoin. Refs #1185
Add Certs PoV: per-step ≡ᵐᵗ + coin bridges, RTC lift
New modules under src/Ledger/Dijkstra/Specification/Certs/Properties/: + PoVLemmas.lagda.md (CERT-level) + PoV.lagda.md (CERTS-level) PoVLemmas exports: + CERT-pov: preservation of value at one CERT step + CERT-pots-≡ᵐᵗ: per-step ≡ᵐ-componentwise triple bridge + CERT-coinFromDeposits-step: per-step coin bridge (derived) + Triple machinery: pots, coinFromDeposits-pots, updateCertDeposit-list, pots-updateCertDeposits + PoolDepositsAligned, Is-just-isPoolRegistered⇒∈-dom PoV exports a bundled Certs-PoV module parameterised by indexedSumᵛ'-∪ and PoolDepositsAligned-CERT, providing: + CERTS-pov: preservation across the closure + CERTS-Deposits-Bridge.CERTS-coinFromDeposits-updateCertDeposits: the closed-form coin bridge consumed by LEDGER-pov The triple-form per-step bridge from the previous Ledger-PoV branch required a deferred propositional equation m ∪ˡ ❴ k , v ❵ ≡ m (when k ∈ dom m). This PR drops that parameter, using instead the upstream ≡ᵐ-componentwise singleton-∈-∪ˡ plumbed through the closed form via ∪⁺-cong-r, ∪ˡ-cong, restrict-cong, and collapsed to a coin equality via ≡ᵉ-getCoin. Refs #1185
adopt Ledger.Prelude helper lemmas from earlier PR
Hoist cert-deposit helpers from Utxo to Certs (#1208)
Move six closed-form cert-deposit helpers from
src/Ledger/Dijkstra/Specification/Utxo.lagda.md to
src/Ledger/Dijkstra/Specification/Certs.lagda.md:
+ updateCertDeposit
+ updateCertDepositsStep (new named extraction of the fold body)
+ updateCertDeposits
+ coinFromDeposits
+ depositsChange
+ newCertDeposits
+ refundCertDeposits
These helpers depend only on Certs-level definitions, so their natural
home is Certs.lagda.md. Their placement in Utxo.lagda.md forced any
proof referencing them to take the larger TransactionStructure /
AbstractFunctions parameter set, blocking proofs in
Certs.Properties.PoV(Lemmas) (parameterised only by GovStructure) from
referring to them.
govProposalsDeposits stays in Utxo.lagda.md — it depends on GovProposal
from Gov.Actions, not on a Certs-level type.
Bundled bug fixes to updateCertDeposits:
+ Typo: DState.deposits was being set from the GState delta instead
of the DState delta.
+ Fold direction: was foldr (right-to-left). CERTS processes certs
left-to-right via BS-ind's head-first decomposition. Changed to
foldl, matching Conway's left-to-right recursion and Dijkstra's
own applyToRewards. Counterexample under foldr:
[delegate c d, dereg c (just d)] on a fresh credential should
leave c ∉ deposits per CERTS, but foldr processes dereg first
(a no-op) then delegate, ending with c ∈ deposits.
updateCertDepositsStep is the inner fold body extracted as a named
function so downstream proofs in Certs.Properties.PoV can state and
use a per-step pots equation about it.
Also: add HasCoin-UTxOState (Utxo.lagda.md) and HasCoin-LedgerState
(Ledger.lagda.md). HasCoin-LedgerState sums UTxO state total, DState
rewards balance, and the three deposit pots via the hoisted
coinFromDeposits — the form needed to balance against the UTXO
batch-balance equation.
Closes #1208.
add proof of Is-just-isPoolRegistered⇒∈-dom
Trace imports during build
Bridge CERTS evolution to closed-form cert-deposit accounting
Adds the per-step and RTC-induction bridging lemmas that prove the actual `CertState` produced by a `CERTS` chain has the same three deposit pots (and hence the same `coinFromDeposits`) as the closed-form `updateCertDeposits` applied to the initial state and the cert list. This is the cert-deposit half of the `LEDGER-pov` chain; combined with the `posNeg-deposits` cancellation identity, it closes the deposit-accounting equation against the UTXO batch-balance equation.
New proofs (PR branch):
+ `CERT-deposits-updateCertDeposit` in `Certs.Properties.PoVLemmas`. Per-step, case-split on the `CERT` rule's eight `DCert` constructors; `refl` in seven cases, `POOL-rereg` discharged via the pool-deposit alignment invariant.
+ `CERTS-deposits-updateCertDeposits` in `Certs.Properties.PoV`. RTC induction mirroring `CERTS-pov`. Factored through `updateCertDeposit-list`, a pure pot-only `foldl` that is the rule-intrinsic counterpart of `updateCertDeposits`; the bridge `pots-updateCertDeposits` handles the inheritance of non-deposit `CertState` fields.
+ `CERTS-coinFromDeposits-updateCertDeposits`. Coin projection of the main lemma, immediately usable by `LEDGER-pov`.
Both bridging lemmas are parameterised over (a) two deferred set/map facts (`∪ˡ-singleton-mem-≡`, `Is-just-isPoolRegistered⇒∈-dom`) to be discharged from the standard library; and (b) the pool-deposit alignment invariant `PoolDepositsAligned` plus, for the RTC sibling, its `CERT`-step preservation lemma — both follow by inspection of the `POOL` sub-rules.
Master-touching changes
+ **Bug fix in `updateCertDeposits`**. Was setting `DState.deposits` to `depositsᵍ` (the `GState` delta) instead of `depositsᵈ`. The `depositsᵈ` name was bound by destructuring but otherwise unused — almost certainly an unintended typo.
+ **Bug fix in `updateCertDeposits`**. Was using `foldr`, processing certs right-to-left. The `CERTS` rule processes certs left-to-right (via `BS-ind`'s head-first decomposition). For non-commutative cert sequences this is unsound: e.g. `[delegate c keyDeposit, dereg c (just keyDeposit)]` for a fresh credential should end with `c ∉ deposits` per `CERTS`, but `foldr` (which processes the `dereg` on the fresh state first as a no-op, then the `delegate`) ends with `c ∈ deposits`. Switched to `foldl`. Conway's `updateCertDeposits` is recursive left-to-right (equivalent to `foldl`); Dijkstra's own `applyToRewards` uses `foldl`.
+ **Refactor**. Extracted `updateCertDepositsStep` as a named function from `updateCertDeposits`' inner lambda, so that downstream proofs can state and use its per-step pots equation.
+ **Hoist**. Moved `updateCertDeposit`, `updateCertDeposits`, `coinFromDeposits`, `depositsChange`, `newCertDeposits`, `refundCertDeposits` from `Utxo.lagda.md` to `Certs.lagda.md`. These depend only on `Certs`-level definitions (`PParams`, `DCert`, `CertState`); the previous location forced any proof referencing them to take the larger `TransactionStructure` / `AbstractFunctions` parameter set, blocking placement of the bridging lemmas in `Certs.Properties.PoV{,Lemmas}`. `govProposalsDeposits` remains in `Utxo.lagda.md` (depends on `GovProposal`).
PR-branch-only changes:
+ `Ledger.lagda.md`. Replaced the local `coinFromDeposit` (singular) with the hoisted `coinFromDeposits` (plural). `HasCoin-LedgerState` has three summands: `getCoin(UTxOState) + rewardsBalance(DState) + coinFromDeposits(CertState)`. Gov-action deposits are stored in `GState.deposits` (keyed by `returnAddr`'s stake credential) and are therefore already counted by the third summand.
Remove dead links from readme
Add "Modules" hierarchy to Dijkstra mkdocs
Add missing modules to mkdocs.yaml
Illiterate Foreign* modules
Fix bug in fls-shake
mkdocs .md files weren't being generated even when .lagda.md files changed.
Artifacts generated from 9451bc1d7bcf5a0a67f3c8f08f6a53800f828e29
[Dijkstra] Add missing premises to UTXOW (#1176)
* Add utxo0 binding in UTXOW For consistency with SUBUTXOW * Add missing premises * Improve tc time of Utxo.Computational
Improve tc time of Utxo.Computational