Artifacts generated from 3603bd6f3c05305f414cbefe3e56059f91989af0
Home /
Input Output /
formal-ledger-specifications
Jul 26, 9-10 AM (0)
Jul 26, 10-11 AM (0)
Jul 26, 11-12 PM (0)
Jul 26, 12-1 PM (0)
Jul 26, 1-2 PM (0)
Jul 26, 2-3 PM (0)
Jul 26, 3-4 PM (0)
Jul 26, 4-5 PM (0)
Jul 26, 5-6 PM (0)
Jul 26, 6-7 PM (0)
Jul 26, 7-8 PM (0)
Jul 26, 8-9 PM (0)
Jul 26, 9-10 PM (0)
Jul 26, 10-11 PM (0)
Jul 26, 11-12 AM (1)
Jul 27, 12-1 AM (1)
Jul 27, 1-2 AM (2)
Jul 27, 2-3 AM (0)
Jul 27, 3-4 AM (0)
Jul 27, 4-5 AM (0)
Jul 27, 5-6 AM (0)
Jul 27, 6-7 AM (0)
Jul 27, 7-8 AM (0)
Jul 27, 8-9 AM (0)
Jul 27, 9-10 AM (0)
Jul 27, 10-11 AM (0)
Jul 27, 11-12 PM (0)
Jul 27, 12-1 PM (0)
Jul 27, 1-2 PM (0)
Jul 27, 2-3 PM (0)
Jul 27, 3-4 PM (0)
Jul 27, 4-5 PM (0)
Jul 27, 5-6 PM (0)
Jul 27, 6-7 PM (0)
Jul 27, 7-8 PM (0)
Jul 27, 8-9 PM (0)
Jul 27, 9-10 PM (0)
Jul 27, 10-11 PM (0)
Jul 27, 11-12 AM (0)
Jul 28, 12-1 AM (0)
Jul 28, 1-2 AM (0)
Jul 28, 2-3 AM (0)
Jul 28, 3-4 AM (0)
Jul 28, 4-5 AM (0)
Jul 28, 5-6 AM (0)
Jul 28, 6-7 AM (0)
Jul 28, 7-8 AM (0)
Jul 28, 8-9 AM (0)
Jul 28, 9-10 AM (0)
Jul 28, 10-11 AM (0)
Jul 28, 11-12 PM (0)
Jul 28, 12-1 PM (3)
Jul 28, 1-2 PM (0)
Jul 28, 2-3 PM (0)
Jul 28, 3-4 PM (1)
Jul 28, 4-5 PM (0)
Jul 28, 5-6 PM (0)
Jul 28, 6-7 PM (0)
Jul 28, 7-8 PM (0)
Jul 28, 8-9 PM (0)
Jul 28, 9-10 PM (0)
Jul 28, 10-11 PM (0)
Jul 28, 11-12 AM (0)
Jul 29, 12-1 AM (0)
Jul 29, 1-2 AM (0)
Jul 29, 2-3 AM (0)
Jul 29, 3-4 AM (2)
Jul 29, 4-5 AM (2)
Jul 29, 5-6 AM (2)
Jul 29, 6-7 AM (0)
Jul 29, 7-8 AM (0)
Jul 29, 8-9 AM (0)
Jul 29, 9-10 AM (0)
Jul 29, 10-11 AM (0)
Jul 29, 11-12 PM (0)
Jul 29, 12-1 PM (0)
Jul 29, 1-2 PM (0)
Jul 29, 2-3 PM (0)
Jul 29, 3-4 PM (0)
Jul 29, 4-5 PM (0)
Jul 29, 5-6 PM (0)
Jul 29, 6-7 PM (1)
Jul 29, 7-8 PM (0)
Jul 29, 8-9 PM (0)
Jul 29, 9-10 PM (0)
Jul 29, 10-11 PM (0)
Jul 29, 11-12 AM (0)
Jul 30, 12-1 AM (0)
Jul 30, 1-2 AM (0)
Jul 30, 2-3 AM (0)
Jul 30, 3-4 AM (0)
Jul 30, 4-5 AM (0)
Jul 30, 5-6 AM (0)
Jul 30, 6-7 AM (0)
Jul 30, 7-8 AM (0)
Jul 30, 8-9 AM (0)
Jul 30, 9-10 AM (0)
Jul 30, 10-11 AM (2)
Jul 30, 11-12 PM (1)
Jul 30, 12-1 PM (3)
Jul 30, 1-2 PM (0)
Jul 30, 2-3 PM (0)
Jul 30, 3-4 PM (0)
Jul 30, 4-5 PM (0)
Jul 30, 5-6 PM (0)
Jul 30, 6-7 PM (0)
Jul 30, 7-8 PM (0)
Jul 30, 8-9 PM (0)
Jul 30, 9-10 PM (2)
Jul 30, 10-11 PM (0)
Jul 30, 11-12 AM (0)
Jul 31, 12-1 AM (0)
Jul 31, 1-2 AM (0)
Jul 31, 2-3 AM (0)
Jul 31, 3-4 AM (0)
Jul 31, 4-5 AM (0)
Jul 31, 5-6 AM (0)
Jul 31, 6-7 AM (0)
Jul 31, 7-8 AM (0)
Jul 31, 8-9 AM (0)
Jul 31, 9-10 AM (0)
Jul 31, 10-11 AM (18)
Jul 31, 11-12 PM (0)
Jul 31, 12-1 PM (0)
Jul 31, 1-2 PM (2)
Jul 31, 2-3 PM (1)
Jul 31, 3-4 PM (0)
Jul 31, 4-5 PM (0)
Jul 31, 5-6 PM (0)
Jul 31, 6-7 PM (0)
Jul 31, 7-8 PM (0)
Jul 31, 8-9 PM (1)
Jul 31, 9-10 PM (0)
Jul 31, 10-11 PM (0)
Jul 31, 11-12 AM (0)
Aug 01, 12-1 AM (0)
Aug 01, 1-2 AM (0)
Aug 01, 2-3 AM (0)
Aug 01, 3-4 AM (2)
Aug 01, 4-5 AM (0)
Aug 01, 5-6 AM (0)
Aug 01, 6-7 AM (0)
Aug 01, 7-8 AM (0)
Aug 01, 8-9 AM (0)
Aug 01, 9-10 AM (0)
Aug 01, 10-11 AM (0)
Aug 01, 11-12 PM (0)
Aug 01, 12-1 PM (4)
Aug 01, 1-2 PM (1)
Aug 01, 2-3 PM (0)
Aug 01, 3-4 PM (0)
Aug 01, 4-5 PM (1)
Aug 01, 5-6 PM (0)
Aug 01, 6-7 PM (0)
Aug 01, 7-8 PM (0)
Aug 01, 8-9 PM (0)
Aug 01, 9-10 PM (0)
Aug 01, 10-11 PM (0)
Aug 01, 11-12 AM (0)
Aug 02, 12-1 AM (0)
Aug 02, 1-2 AM (1)
Aug 02, 2-3 AM (0)
Aug 02, 3-4 AM (0)
Aug 02, 4-5 AM (0)
Aug 02, 5-6 AM (0)
Aug 02, 6-7 AM (0)
Aug 02, 7-8 AM (0)
Aug 02, 8-9 AM (0)
Aug 02, 9-10 AM (0)
54 commits this week
Jul 26, 2025
-
Aug 02, 2025
Outline prove of dropRetiredDeposits
Artifacts generated from 3d08be2d8dfbff1911d90f87ef5d7161b20fb405
fix AgdaArgument deletion
Artifacts generated from 7fba1fa4de3229811862f0e67d03df1c50ef312b
Artifacts generated from 031bc4a374045131f7ec303a072bf7df85a4712b
Artifacts generated from bb2feaef93d12f5c9c548839abbd049e70396278
Complete implementation of `stakeDistr` (#802)
* Refactor EPOCH-complete * Complete implementation of `stakeDistr` * Fix html build --------- Co-authored-by: Carlos Tomé Cortiñas <[email protected]>
wip: Make more explicit the structure of EPOCH-govDepsMatch
Complete implementation of `stakeDistr`
Refactor EPOCH-complete
Qualify names from the update modules to clarify procedence
remove more unnecessary imports
use type classes to remove some imports
Duplicate let bindings of EPOCH in another module to be used for proofs
Make POOLREAP happen after RATIFIES
Remove trailing space
Use POOLREAP from EPOCH
Simplify rewardAcnts'
Ignore donations in POOLREAP
Handle donations and deposits update
Implement mRefunds and unclaimed. Update stakeDelegs.
Implement rewardsAcnts'