Reuse updateCertDeposits from Ledger in Conformance
Home /
IntersectMBO /
formal-ledger-specifications
Nov 14, 1-2 PM (0)
Nov 14, 2-3 PM (0)
Nov 14, 3-4 PM (0)
Nov 14, 4-5 PM (2)
Nov 14, 5-6 PM (0)
Nov 14, 6-7 PM (0)
Nov 14, 7-8 PM (0)
Nov 14, 8-9 PM (0)
Nov 14, 9-10 PM (0)
Nov 14, 10-11 PM (0)
Nov 14, 11-12 AM (0)
Nov 15, 12-1 AM (0)
Nov 15, 1-2 AM (0)
Nov 15, 2-3 AM (0)
Nov 15, 3-4 AM (0)
Nov 15, 4-5 AM (0)
Nov 15, 5-6 AM (0)
Nov 15, 6-7 AM (0)
Nov 15, 7-8 AM (3)
Nov 15, 8-9 AM (0)
Nov 15, 9-10 AM (0)
Nov 15, 10-11 AM (0)
Nov 15, 11-12 PM (0)
Nov 15, 12-1 PM (2)
Nov 15, 1-2 PM (3)
Nov 15, 2-3 PM (0)
Nov 15, 3-4 PM (0)
Nov 15, 4-5 PM (0)
Nov 15, 5-6 PM (0)
Nov 15, 6-7 PM (0)
Nov 15, 7-8 PM (0)
Nov 15, 8-9 PM (0)
Nov 15, 9-10 PM (0)
Nov 15, 10-11 PM (0)
Nov 15, 11-12 AM (0)
Nov 16, 12-1 AM (0)
Nov 16, 1-2 AM (0)
Nov 16, 2-3 AM (0)
Nov 16, 3-4 AM (0)
Nov 16, 4-5 AM (0)
Nov 16, 5-6 AM (0)
Nov 16, 6-7 AM (0)
Nov 16, 7-8 AM (0)
Nov 16, 8-9 AM (0)
Nov 16, 9-10 AM (0)
Nov 16, 10-11 AM (0)
Nov 16, 11-12 PM (0)
Nov 16, 12-1 PM (0)
Nov 16, 1-2 PM (0)
Nov 16, 2-3 PM (0)
Nov 16, 3-4 PM (0)
Nov 16, 4-5 PM (0)
Nov 16, 5-6 PM (0)
Nov 16, 6-7 PM (0)
Nov 16, 7-8 PM (0)
Nov 16, 8-9 PM (0)
Nov 16, 9-10 PM (0)
Nov 16, 10-11 PM (0)
Nov 16, 11-12 AM (0)
Nov 17, 12-1 AM (0)
Nov 17, 1-2 AM (0)
Nov 17, 2-3 AM (0)
Nov 17, 3-4 AM (0)
Nov 17, 4-5 AM (0)
Nov 17, 5-6 AM (0)
Nov 17, 6-7 AM (0)
Nov 17, 7-8 AM (0)
Nov 17, 8-9 AM (0)
Nov 17, 9-10 AM (0)
Nov 17, 10-11 AM (0)
Nov 17, 11-12 PM (0)
Nov 17, 12-1 PM (0)
Nov 17, 1-2 PM (0)
Nov 17, 2-3 PM (0)
Nov 17, 3-4 PM (0)
Nov 17, 4-5 PM (0)
Nov 17, 5-6 PM (0)
Nov 17, 6-7 PM (0)
Nov 17, 7-8 PM (0)
Nov 17, 8-9 PM (0)
Nov 17, 9-10 PM (0)
Nov 17, 10-11 PM (0)
Nov 17, 11-12 AM (0)
Nov 18, 12-1 AM (0)
Nov 18, 1-2 AM (0)
Nov 18, 2-3 AM (0)
Nov 18, 3-4 AM (0)
Nov 18, 4-5 AM (0)
Nov 18, 5-6 AM (0)
Nov 18, 6-7 AM (0)
Nov 18, 7-8 AM (0)
Nov 18, 8-9 AM (0)
Nov 18, 9-10 AM (0)
Nov 18, 10-11 AM (0)
Nov 18, 11-12 PM (1)
Nov 18, 12-1 PM (1)
Nov 18, 1-2 PM (2)
Nov 18, 2-3 PM (0)
Nov 18, 3-4 PM (0)
Nov 18, 4-5 PM (0)
Nov 18, 5-6 PM (0)
Nov 18, 6-7 PM (0)
Nov 18, 7-8 PM (0)
Nov 18, 8-9 PM (0)
Nov 18, 9-10 PM (0)
Nov 18, 10-11 PM (0)
Nov 18, 11-12 AM (0)
Nov 19, 12-1 AM (0)
Nov 19, 1-2 AM (0)
Nov 19, 2-3 AM (0)
Nov 19, 3-4 AM (0)
Nov 19, 4-5 AM (0)
Nov 19, 5-6 AM (0)
Nov 19, 6-7 AM (0)
Nov 19, 7-8 AM (0)
Nov 19, 8-9 AM (2)
Nov 19, 9-10 AM (1)
Nov 19, 10-11 AM (0)
Nov 19, 11-12 PM (5)
Nov 19, 12-1 PM (23)
Nov 19, 1-2 PM (0)
Nov 19, 2-3 PM (0)
Nov 19, 3-4 PM (4)
Nov 19, 4-5 PM (0)
Nov 19, 5-6 PM (0)
Nov 19, 6-7 PM (0)
Nov 19, 7-8 PM (0)
Nov 19, 8-9 PM (0)
Nov 19, 9-10 PM (0)
Nov 19, 10-11 PM (0)
Nov 19, 11-12 AM (0)
Nov 20, 12-1 AM (0)
Nov 20, 1-2 AM (2)
Nov 20, 2-3 AM (0)
Nov 20, 3-4 AM (0)
Nov 20, 4-5 AM (0)
Nov 20, 5-6 AM (0)
Nov 20, 6-7 AM (0)
Nov 20, 7-8 AM (0)
Nov 20, 8-9 AM (1)
Nov 20, 9-10 AM (0)
Nov 20, 10-11 AM (0)
Nov 20, 11-12 PM (0)
Nov 20, 12-1 PM (0)
Nov 20, 1-2 PM (0)
Nov 20, 2-3 PM (0)
Nov 20, 3-4 PM (0)
Nov 20, 4-5 PM (0)
Nov 20, 5-6 PM (0)
Nov 20, 6-7 PM (0)
Nov 20, 7-8 PM (0)
Nov 20, 8-9 PM (0)
Nov 20, 9-10 PM (0)
Nov 20, 10-11 PM (0)
Nov 20, 11-12 AM (0)
Nov 21, 12-1 AM (0)
Nov 21, 1-2 AM (0)
Nov 21, 2-3 AM (0)
Nov 21, 3-4 AM (0)
Nov 21, 4-5 AM (0)
Nov 21, 5-6 AM (0)
Nov 21, 6-7 AM (0)
Nov 21, 7-8 AM (0)
Nov 21, 8-9 AM (0)
Nov 21, 9-10 AM (0)
Nov 21, 10-11 AM (0)
Nov 21, 11-12 PM (8)
Nov 21, 12-1 PM (1)
Nov 21, 1-2 PM (0)
61 commits this week
Nov 14, 2024
-
Nov 21, 2024
Updated for 363b1f6f6fe3f4eeb6a89456659413a4ad35e79a
Wip equivalence for UTXO rule
split equivalence proof in multiple modules
Add equivalence proof to Everything.agda
Adapt to changes on master
Start on equivalence proof
Generate code for GH-614
Prepare for conformance equivalence (#614)
* Remove Conformance version of Ratify * Remove conformance version of ScriptValidation * Reuse Ledger code in Conformance.Utxow * Reuse Ledger code in Conformance.Utxo * spell out conformance updateCertDeposit for each DCert to make it line up with ledger * Fix wrong PParams in Conformance GOVCERT rules * Remove unused conformance ratify modules
Bug fixes and trace implementation
Generate code for ecdc428c837e48d2a9f3dae4b466688ea7fe5ab2
Merge branch 'master' into 545-certs-base-case-first
fixme: updateCertDeposits
Conformance proof for GOV
Reuse updateCertDeposits from Ledger in Conformance
Add equivalence proof to Everything.agda
Remove conformance version of ScriptValidation
Reuse Ledger code in Conformance.Utxow
Wip equivalence for UTXO rule
Reuse Ledger code in Conformance.Utxo
Adapt to changes on master
better approach to CERTS
wip: progress on LEDGER-V to Conformance