complete migration of Validation.{agda,lagda.md}
Home /
IntersectMBO /
formal-ledger-specifications
Sep 29, 11-12 AM (0)
Sep 30, 12-1 AM (0)
Sep 30, 1-2 AM (0)
Sep 30, 2-3 AM (0)
Sep 30, 3-4 AM (0)
Sep 30, 4-5 AM (0)
Sep 30, 5-6 AM (0)
Sep 30, 6-7 AM (0)
Sep 30, 7-8 AM (0)
Sep 30, 8-9 AM (0)
Sep 30, 9-10 AM (0)
Sep 30, 10-11 AM (0)
Sep 30, 11-12 PM (0)
Sep 30, 12-1 PM (0)
Sep 30, 1-2 PM (0)
Sep 30, 2-3 PM (0)
Sep 30, 3-4 PM (0)
Sep 30, 4-5 PM (0)
Sep 30, 5-6 PM (0)
Sep 30, 6-7 PM (0)
Sep 30, 7-8 PM (1)
Sep 30, 8-9 PM (13)
Sep 30, 9-10 PM (0)
Sep 30, 10-11 PM (0)
Sep 30, 11-12 AM (0)
Oct 01, 12-1 AM (0)
Oct 01, 1-2 AM (0)
Oct 01, 2-3 AM (1)
Oct 01, 3-4 AM (0)
Oct 01, 4-5 AM (0)
Oct 01, 5-6 AM (0)
Oct 01, 6-7 AM (0)
Oct 01, 7-8 AM (0)
Oct 01, 8-9 AM (0)
Oct 01, 9-10 AM (0)
Oct 01, 10-11 AM (0)
Oct 01, 11-12 PM (0)
Oct 01, 12-1 PM (0)
Oct 01, 1-2 PM (0)
Oct 01, 2-3 PM (0)
Oct 01, 3-4 PM (0)
Oct 01, 4-5 PM (0)
Oct 01, 5-6 PM (0)
Oct 01, 6-7 PM (0)
Oct 01, 7-8 PM (0)
Oct 01, 8-9 PM (0)
Oct 01, 9-10 PM (0)
Oct 01, 10-11 PM (0)
Oct 01, 11-12 AM (0)
Oct 02, 12-1 AM (0)
Oct 02, 1-2 AM (0)
Oct 02, 2-3 AM (0)
Oct 02, 3-4 AM (0)
Oct 02, 4-5 AM (0)
Oct 02, 5-6 AM (0)
Oct 02, 6-7 AM (0)
Oct 02, 7-8 AM (0)
Oct 02, 8-9 AM (0)
Oct 02, 9-10 AM (0)
Oct 02, 10-11 AM (0)
Oct 02, 11-12 PM (0)
Oct 02, 12-1 PM (0)
Oct 02, 1-2 PM (0)
Oct 02, 2-3 PM (0)
Oct 02, 3-4 PM (0)
Oct 02, 4-5 PM (0)
Oct 02, 5-6 PM (0)
Oct 02, 6-7 PM (0)
Oct 02, 7-8 PM (0)
Oct 02, 8-9 PM (0)
Oct 02, 9-10 PM (0)
Oct 02, 10-11 PM (0)
Oct 02, 11-12 AM (0)
Oct 03, 12-1 AM (0)
Oct 03, 1-2 AM (0)
Oct 03, 2-3 AM (0)
Oct 03, 3-4 AM (1)
Oct 03, 4-5 AM (0)
Oct 03, 5-6 AM (0)
Oct 03, 6-7 AM (0)
Oct 03, 7-8 AM (0)
Oct 03, 8-9 AM (0)
Oct 03, 9-10 AM (0)
Oct 03, 10-11 AM (0)
Oct 03, 11-12 PM (0)
Oct 03, 12-1 PM (0)
Oct 03, 1-2 PM (0)
Oct 03, 2-3 PM (0)
Oct 03, 3-4 PM (0)
Oct 03, 4-5 PM (0)
Oct 03, 5-6 PM (0)
Oct 03, 6-7 PM (0)
Oct 03, 7-8 PM (0)
Oct 03, 8-9 PM (0)
Oct 03, 9-10 PM (0)
Oct 03, 10-11 PM (0)
Oct 03, 11-12 AM (0)
Oct 04, 12-1 AM (0)
Oct 04, 1-2 AM (0)
Oct 04, 2-3 AM (0)
Oct 04, 3-4 AM (0)
Oct 04, 4-5 AM (0)
Oct 04, 5-6 AM (0)
Oct 04, 6-7 AM (0)
Oct 04, 7-8 AM (0)
Oct 04, 8-9 AM (0)
Oct 04, 9-10 AM (0)
Oct 04, 10-11 AM (0)
Oct 04, 11-12 PM (0)
Oct 04, 12-1 PM (0)
Oct 04, 1-2 PM (0)
Oct 04, 2-3 PM (0)
Oct 04, 3-4 PM (0)
Oct 04, 4-5 PM (0)
Oct 04, 5-6 PM (0)
Oct 04, 6-7 PM (0)
Oct 04, 7-8 PM (0)
Oct 04, 8-9 PM (0)
Oct 04, 9-10 PM (0)
Oct 04, 10-11 PM (0)
Oct 04, 11-12 AM (0)
Oct 05, 12-1 AM (0)
Oct 05, 1-2 AM (0)
Oct 05, 2-3 AM (0)
Oct 05, 3-4 AM (0)
Oct 05, 4-5 AM (0)
Oct 05, 5-6 AM (0)
Oct 05, 6-7 AM (0)
Oct 05, 7-8 AM (0)
Oct 05, 8-9 AM (0)
Oct 05, 9-10 AM (0)
Oct 05, 10-11 AM (0)
Oct 05, 11-12 PM (0)
Oct 05, 12-1 PM (0)
Oct 05, 1-2 PM (0)
Oct 05, 2-3 PM (0)
Oct 05, 3-4 PM (0)
Oct 05, 4-5 PM (0)
Oct 05, 5-6 PM (0)
Oct 05, 6-7 PM (0)
Oct 05, 7-8 PM (0)
Oct 05, 8-9 PM (0)
Oct 05, 9-10 PM (0)
Oct 05, 10-11 PM (0)
Oct 05, 11-12 AM (0)
Oct 06, 12-1 AM (0)
Oct 06, 1-2 AM (0)
Oct 06, 2-3 AM (0)
Oct 06, 3-4 AM (0)
Oct 06, 4-5 AM (0)
Oct 06, 5-6 AM (0)
Oct 06, 6-7 AM (0)
Oct 06, 7-8 AM (0)
Oct 06, 8-9 AM (0)
Oct 06, 9-10 AM (0)
Oct 06, 10-11 AM (0)
Oct 06, 11-12 PM (0)
Oct 06, 12-1 PM (0)
Oct 06, 1-2 PM (0)
Oct 06, 2-3 PM (0)
Oct 06, 3-4 PM (0)
Oct 06, 4-5 PM (0)
Oct 06, 5-6 PM (0)
Oct 06, 6-7 PM (0)
Oct 06, 7-8 PM (0)
Oct 06, 8-9 PM (0)
Oct 06, 9-10 PM (0)
Oct 06, 10-11 PM (0)
Oct 06, 11-12 AM (0)
16 commits this week
Sep 30, 2025
-
Oct 07, 2025
complete migration of Transaction.lagda{,.md}
fix bug introduced by merge
fix bug that somehow crept in
incorporate Carlos's change requests
fix some formatting in Ledger module
Also, removed `AgdaInductiveConstructor` class from occurrences of "DRep" in the text; this makes it easier to be consistent throughout the document, but even if we do want to use Agda high-lighting for "DRep", it's not clear to me that `AgdaInductiveConstructor` is the right class to use.
migrate STS and ComputationalRelation
prepare to migrate STS and ComputationalRelation
Refactor equivalence proofs for new CERTS rule.
PoV proofs for new CERTS rule
Computational-RunTraceAfterAndThen proof done!
Also added computational proofs for new pre-cert and post-cert rules.
prepare to migrate Certs.lagda{,.md}
migrate Certs.lagda{,.md}
revert CERTS rule in conformance version
revert CERTS rule to do CERTBASE last
This is a first step to refactoring the CERTS rule. Ultimately we will deprecate the "CERTBASE" rule and replace it with "preCerts" and "postCerts" functions that will run before and after the CERTS sts. Some of the things that currently happen in CERTBASE may be moved into the LEDGER rule. revert CERTS rule in conformance version
![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&s=80)
Artifacts generated from 07fe940fcacb994e48b3eae3f2de7e60328085f6