Artifacts generated from 16e84c221596cf15579871ba903464559e1acb9e
Home /
IntersectMBO /
formal-ledger-specifications
Jan 19, 4-5 AM (0)
Jan 19, 5-6 AM (0)
Jan 19, 6-7 AM (0)
Jan 19, 7-8 AM (0)
Jan 19, 8-9 AM (0)
Jan 19, 9-10 AM (0)
Jan 19, 10-11 AM (0)
Jan 19, 11-12 PM (0)
Jan 19, 12-1 PM (0)
Jan 19, 1-2 PM (0)
Jan 19, 2-3 PM (1)
Jan 19, 3-4 PM (0)
Jan 19, 4-5 PM (0)
Jan 19, 5-6 PM (0)
Jan 19, 6-7 PM (0)
Jan 19, 7-8 PM (0)
Jan 19, 8-9 PM (0)
Jan 19, 9-10 PM (0)
Jan 19, 10-11 PM (0)
Jan 19, 11-12 AM (0)
Jan 20, 12-1 AM (0)
Jan 20, 1-2 AM (0)
Jan 20, 2-3 AM (0)
Jan 20, 3-4 AM (0)
Jan 20, 4-5 AM (0)
Jan 20, 5-6 AM (0)
Jan 20, 6-7 AM (0)
Jan 20, 7-8 AM (0)
Jan 20, 8-9 AM (0)
Jan 20, 9-10 AM (0)
Jan 20, 10-11 AM (0)
Jan 20, 11-12 PM (0)
Jan 20, 12-1 PM (0)
Jan 20, 1-2 PM (0)
Jan 20, 2-3 PM (0)
Jan 20, 3-4 PM (0)
Jan 20, 4-5 PM (0)
Jan 20, 5-6 PM (0)
Jan 20, 6-7 PM (0)
Jan 20, 7-8 PM (0)
Jan 20, 8-9 PM (0)
Jan 20, 9-10 PM (0)
Jan 20, 10-11 PM (0)
Jan 20, 11-12 AM (0)
Jan 21, 12-1 AM (0)
Jan 21, 1-2 AM (0)
Jan 21, 2-3 AM (0)
Jan 21, 3-4 AM (0)
Jan 21, 4-5 AM (2)
Jan 21, 5-6 AM (0)
Jan 21, 6-7 AM (0)
Jan 21, 7-8 AM (0)
Jan 21, 8-9 AM (0)
Jan 21, 9-10 AM (0)
Jan 21, 10-11 AM (0)
Jan 21, 11-12 PM (0)
Jan 21, 12-1 PM (0)
Jan 21, 1-2 PM (0)
Jan 21, 2-3 PM (0)
Jan 21, 3-4 PM (0)
Jan 21, 4-5 PM (0)
Jan 21, 5-6 PM (0)
Jan 21, 6-7 PM (0)
Jan 21, 7-8 PM (0)
Jan 21, 8-9 PM (0)
Jan 21, 9-10 PM (0)
Jan 21, 10-11 PM (2)
Jan 21, 11-12 AM (2)
Jan 22, 12-1 AM (0)
Jan 22, 1-2 AM (1)
Jan 22, 2-3 AM (0)
Jan 22, 3-4 AM (0)
Jan 22, 4-5 AM (0)
Jan 22, 5-6 AM (0)
Jan 22, 6-7 AM (0)
Jan 22, 7-8 AM (0)
Jan 22, 8-9 AM (0)
Jan 22, 9-10 AM (0)
Jan 22, 10-11 AM (1)
Jan 22, 11-12 PM (0)
Jan 22, 12-1 PM (0)
Jan 22, 1-2 PM (0)
Jan 22, 2-3 PM (0)
Jan 22, 3-4 PM (0)
Jan 22, 4-5 PM (0)
Jan 22, 5-6 PM (0)
Jan 22, 6-7 PM (0)
Jan 22, 7-8 PM (0)
Jan 22, 8-9 PM (0)
Jan 22, 9-10 PM (0)
Jan 22, 10-11 PM (0)
Jan 22, 11-12 AM (0)
Jan 23, 12-1 AM (0)
Jan 23, 1-2 AM (0)
Jan 23, 2-3 AM (0)
Jan 23, 3-4 AM (1)
Jan 23, 4-5 AM (1)
Jan 23, 5-6 AM (0)
Jan 23, 6-7 AM (0)
Jan 23, 7-8 AM (0)
Jan 23, 8-9 AM (0)
Jan 23, 9-10 AM (2)
Jan 23, 10-11 AM (0)
Jan 23, 11-12 PM (0)
Jan 23, 12-1 PM (0)
Jan 23, 1-2 PM (0)
Jan 23, 2-3 PM (1)
Jan 23, 3-4 PM (0)
Jan 23, 4-5 PM (1)
Jan 23, 5-6 PM (0)
Jan 23, 6-7 PM (3)
Jan 23, 7-8 PM (0)
Jan 23, 8-9 PM (0)
Jan 23, 9-10 PM (0)
Jan 23, 10-11 PM (0)
Jan 23, 11-12 AM (0)
Jan 24, 12-1 AM (0)
Jan 24, 1-2 AM (0)
Jan 24, 2-3 AM (0)
Jan 24, 3-4 AM (1)
Jan 24, 4-5 AM (0)
Jan 24, 5-6 AM (0)
Jan 24, 6-7 AM (0)
Jan 24, 7-8 AM (0)
Jan 24, 8-9 AM (0)
Jan 24, 9-10 AM (0)
Jan 24, 10-11 AM (0)
Jan 24, 11-12 PM (0)
Jan 24, 12-1 PM (0)
Jan 24, 1-2 PM (0)
Jan 24, 2-3 PM (0)
Jan 24, 3-4 PM (0)
Jan 24, 4-5 PM (0)
Jan 24, 5-6 PM (0)
Jan 24, 6-7 PM (0)
Jan 24, 7-8 PM (0)
Jan 24, 8-9 PM (0)
Jan 24, 9-10 PM (0)
Jan 24, 10-11 PM (0)
Jan 24, 11-12 AM (0)
Jan 25, 12-1 AM (0)
Jan 25, 1-2 AM (0)
Jan 25, 2-3 AM (0)
Jan 25, 3-4 AM (0)
Jan 25, 4-5 AM (0)
Jan 25, 5-6 AM (0)
Jan 25, 6-7 AM (0)
Jan 25, 7-8 AM (0)
Jan 25, 8-9 AM (0)
Jan 25, 9-10 AM (0)
Jan 25, 10-11 AM (0)
Jan 25, 11-12 PM (0)
Jan 25, 12-1 PM (0)
Jan 25, 1-2 PM (0)
Jan 25, 2-3 PM (0)
Jan 25, 3-4 PM (0)
Jan 25, 4-5 PM (0)
Jan 25, 5-6 PM (0)
Jan 25, 6-7 PM (0)
Jan 25, 7-8 PM (0)
Jan 25, 8-9 PM (0)
Jan 25, 9-10 PM (0)
Jan 25, 10-11 PM (0)
Jan 25, 11-12 AM (0)
Jan 26, 12-1 AM (0)
Jan 26, 1-2 AM (0)
Jan 26, 2-3 AM (0)
Jan 26, 3-4 AM (0)
Jan 26, 4-5 AM (0)
19 commits this week
Jan 19, 2026
-
Jan 26, 2026
fix UTXOS and UTXO rules
clean up txInfoForPurpose
Add premise on epochInfoSlotToUTCTime to UTXO rule
Artifacts generated from ccdf3e8a7ff09d3798471d3d96a6ddfa77494b03
Add allowedLanguages and languages
Move getLanguage to Script
clean up Ledger; add `rmOrphanDRepVotes`
Not sure why `rmOrphanDRepVotes` was commented out. Does it need to be adjusted for Dijkstra?
Implement Gov and GOVS for Dijkstra
As a first pass we simply copy over four Conway modules to Dijkstra: + Enact + Gov + Ratify + Script.Base And make the following actual Dijkstra modules (instead of just importing the Conway version): + Certs + Gov + Gov.Actions + PParams
Move ProtVer to its own module; add GovActionsStructure
changed globalScripts type; fixed Transaction docs
Artifacts generated from b673f681c190cc5d243f8b5d02c66098b8977a0c
Clean up Utxo module, removing redundancies
+ `Γ.globalScripts` is already batch-scoped via `getAllScripts tx utxo₀` (top + subs). + `Γ.globalData` is already batch-scoped via `getAllData tx utxo₀` (top + subs) and then hashed into a map. + `collectP2ScriptsWithContext` (still) unions `txDataMap tx` with `extraData` (so tx-local witness data take precedence).
minor note about union bias
...just to be sure, but probably unnecessary
Fix bugs in Utxo module
+ `collectP2ScriptsWithContext` now sees batch-shared scripts (witness inputs + ref inputs + outputs across all transactions in the batch). + datum-by-hash lookup (`getDatum ... (inj₂ h)`) now has an `extraData` pool containing everything in the batch view, hashed into a map, plus `Γ.globalData`. + no cyclic dependency: `Utxo` computes the batch wiring; `Script.Validation` remains generic.
Artifacts generated from 647a9b48dc5a761a344bb139ae58706ca66d6586
fix collectP2ScriptsWithContext
Artifacts generated from f638b68807018f8b1f38229d9634d26281a9550f