Artifacts generated from c8f5feabc766cda9f243e24616506aeda313f664
Home /
Input Output /
formal-ledger-specifications
Aug 21, 3-4 PM (0)
Aug 21, 4-5 PM (0)
Aug 21, 5-6 PM (0)
Aug 21, 6-7 PM (0)
Aug 21, 7-8 PM (1)
Aug 21, 8-9 PM (3)
Aug 21, 9-10 PM (2)
Aug 21, 10-11 PM (0)
Aug 21, 11-12 AM (0)
Aug 22, 12-1 AM (0)
Aug 22, 1-2 AM (0)
Aug 22, 2-3 AM (0)
Aug 22, 3-4 AM (3)
Aug 22, 4-5 AM (2)
Aug 22, 5-6 AM (1)
Aug 22, 6-7 AM (1)
Aug 22, 7-8 AM (0)
Aug 22, 8-9 AM (0)
Aug 22, 9-10 AM (22)
Aug 22, 10-11 AM (2)
Aug 22, 11-12 PM (0)
Aug 22, 12-1 PM (1)
Aug 22, 1-2 PM (1)
Aug 22, 2-3 PM (0)
Aug 22, 3-4 PM (0)
Aug 22, 4-5 PM (0)
Aug 22, 5-6 PM (3)
Aug 22, 6-7 PM (0)
Aug 22, 7-8 PM (0)
Aug 22, 8-9 PM (5)
Aug 22, 9-10 PM (0)
Aug 22, 10-11 PM (0)
Aug 22, 11-12 AM (0)
Aug 23, 12-1 AM (0)
Aug 23, 1-2 AM (0)
Aug 23, 2-3 AM (0)
Aug 23, 3-4 AM (0)
Aug 23, 4-5 AM (0)
Aug 23, 5-6 AM (0)
Aug 23, 6-7 AM (0)
Aug 23, 7-8 AM (0)
Aug 23, 8-9 AM (0)
Aug 23, 9-10 AM (0)
Aug 23, 10-11 AM (0)
Aug 23, 11-12 PM (0)
Aug 23, 12-1 PM (0)
Aug 23, 1-2 PM (0)
Aug 23, 2-3 PM (0)
Aug 23, 3-4 PM (0)
Aug 23, 4-5 PM (0)
Aug 23, 5-6 PM (0)
Aug 23, 6-7 PM (0)
Aug 23, 7-8 PM (0)
Aug 23, 8-9 PM (0)
Aug 23, 9-10 PM (0)
Aug 23, 10-11 PM (0)
Aug 23, 11-12 AM (0)
Aug 24, 12-1 AM (0)
Aug 24, 1-2 AM (0)
Aug 24, 2-3 AM (0)
Aug 24, 3-4 AM (0)
Aug 24, 4-5 AM (0)
Aug 24, 5-6 AM (0)
Aug 24, 6-7 AM (0)
Aug 24, 7-8 AM (0)
Aug 24, 8-9 AM (0)
Aug 24, 9-10 AM (0)
Aug 24, 10-11 AM (0)
Aug 24, 11-12 PM (0)
Aug 24, 12-1 PM (0)
Aug 24, 1-2 PM (0)
Aug 24, 2-3 PM (0)
Aug 24, 3-4 PM (0)
Aug 24, 4-5 PM (0)
Aug 24, 5-6 PM (0)
Aug 24, 6-7 PM (0)
Aug 24, 7-8 PM (0)
Aug 24, 8-9 PM (0)
Aug 24, 9-10 PM (0)
Aug 24, 10-11 PM (0)
Aug 24, 11-12 AM (0)
Aug 25, 12-1 AM (0)
Aug 25, 1-2 AM (0)
Aug 25, 2-3 AM (0)
Aug 25, 3-4 AM (0)
Aug 25, 4-5 AM (0)
Aug 25, 5-6 AM (0)
Aug 25, 6-7 AM (0)
Aug 25, 7-8 AM (0)
Aug 25, 8-9 AM (3)
Aug 25, 9-10 AM (1)
Aug 25, 10-11 AM (0)
Aug 25, 11-12 PM (0)
Aug 25, 12-1 PM (0)
Aug 25, 1-2 PM (4)
Aug 25, 2-3 PM (1)
Aug 25, 3-4 PM (0)
Aug 25, 4-5 PM (0)
Aug 25, 5-6 PM (0)
Aug 25, 6-7 PM (6)
Aug 25, 7-8 PM (4)
Aug 25, 8-9 PM (0)
Aug 25, 9-10 PM (0)
Aug 25, 10-11 PM (1)
Aug 25, 11-12 AM (1)
Aug 26, 12-1 AM (2)
Aug 26, 1-2 AM (2)
Aug 26, 2-3 AM (2)
Aug 26, 3-4 AM (0)
Aug 26, 4-5 AM (0)
Aug 26, 5-6 AM (0)
Aug 26, 6-7 AM (0)
Aug 26, 7-8 AM (0)
Aug 26, 8-9 AM (0)
Aug 26, 9-10 AM (0)
Aug 26, 10-11 AM (0)
Aug 26, 11-12 PM (15)
Aug 26, 12-1 PM (2)
Aug 26, 1-2 PM (3)
Aug 26, 2-3 PM (1)
Aug 26, 3-4 PM (1)
Aug 26, 4-5 PM (0)
Aug 26, 5-6 PM (0)
Aug 26, 6-7 PM (7)
Aug 26, 7-8 PM (7)
Aug 26, 8-9 PM (0)
Aug 26, 9-10 PM (0)
Aug 26, 10-11 PM (0)
Aug 26, 11-12 AM (0)
Aug 27, 12-1 AM (1)
Aug 27, 1-2 AM (8)
Aug 27, 2-3 AM (0)
Aug 27, 3-4 AM (0)
Aug 27, 4-5 AM (0)
Aug 27, 5-6 AM (0)
Aug 27, 6-7 AM (0)
Aug 27, 7-8 AM (0)
Aug 27, 8-9 AM (0)
Aug 27, 9-10 AM (0)
Aug 27, 10-11 AM (0)
Aug 27, 11-12 PM (4)
Aug 27, 12-1 PM (1)
Aug 27, 1-2 PM (2)
Aug 27, 2-3 PM (5)
Aug 27, 3-4 PM (1)
Aug 27, 4-5 PM (0)
Aug 27, 5-6 PM (0)
Aug 27, 6-7 PM (8)
Aug 27, 7-8 PM (5)
Aug 27, 8-9 PM (4)
Aug 27, 9-10 PM (0)
Aug 27, 10-11 PM (0)
Aug 27, 11-12 AM (0)
Aug 28, 12-1 AM (0)
Aug 28, 1-2 AM (7)
Aug 28, 2-3 AM (7)
Aug 28, 3-4 AM (0)
Aug 28, 4-5 AM (0)
Aug 28, 5-6 AM (0)
Aug 28, 6-7 AM (0)
Aug 28, 7-8 AM (0)
Aug 28, 8-9 AM (0)
Aug 28, 9-10 AM (0)
Aug 28, 10-11 AM (10)
Aug 28, 11-12 PM (0)
Aug 28, 12-1 PM (0)
Aug 28, 1-2 PM (0)
Aug 28, 2-3 PM (3)
Aug 28, 3-4 PM (0)
176 commits this week
Aug 21, 2025
-
Aug 28, 2025
Generalize composition to relations
Use aggregate₊ instead of aggregateBy
Artifacts generated from 59a083ccff97f056b7be7c9d127e61e03af0c059
Rename calculatePoolDistr to calculatePoolDelegatedStake
Remove VRF bits
Add reference to shelley spec and explain why we do not use PoolDistr
Co-authored-by: Carlos Tomé Cortiñas <[email protected]>
Make import list explicit for UnitInterval
Replace PoolDistr with PoolDelegatedStake
Explain aggregateBy
Update proofs after introducing calculatePoolDistr
Implement calculatePoolDistr
Remove trailing whitespace
Artifacts generated from 9b8786addc42402dff6e9a2f820290fd2db42865
Artifacts generated from 4bed2b9aeb7dbc0b4cdc2de971850ba12ceda158
Artifacts generated from 5c10de11f7b66f20b9e57a945888e5f8c50a79fb
inline tikz in standalone tex files
+ improvements and prepare to migrate Utxo module
+ major improvements to Utxo.lagda.md
+ Update build-tools/static/md/mkdocs/includes/links.md
+ Update src/Ledger/Conway/Specification/Rewards.lagda.md Co-authored-by: Carlos Tomé Cortiñas <[email protected]>
+ add luatex and dvisvgm programs to nix config
+ update CONTRIBUTING + fix background colors of css class for svg images
add svg version of Heinrich's diagram
partial completion of migration of Rewards
Update and regenerate tikz diagram
+ modify CardanoLedger.tex tikz diagram + add STS-Diagram.tex with instructions + generate new svg version of diagram and copy to `static/md/common/src/img/STS-Diagram.svg`
+ add Heinrich's second diagram
+ improve Rewards.lagda.md + add important note about new static tex files
prepare for migration of Rewards module