![github-actions[bot]](https://avatars.githubusercontent.com/in/15368?v=4&s=80)
Artifacts generated from 5eb12b94b727ddd787a59bc3e437a6db044bf3f2
Home /
Input Output /
formal-ledger-specifications
Dec 17, 3-4 AM (0)
Dec 17, 4-5 AM (0)
Dec 17, 5-6 AM (0)
Dec 17, 6-7 AM (0)
Dec 17, 7-8 AM (0)
Dec 17, 8-9 AM (0)
Dec 17, 9-10 AM (0)
Dec 17, 10-11 AM (0)
Dec 17, 11-12 PM (0)
Dec 17, 12-1 PM (0)
Dec 17, 1-2 PM (0)
Dec 17, 2-3 PM (0)
Dec 17, 3-4 PM (0)
Dec 17, 4-5 PM (0)
Dec 17, 5-6 PM (0)
Dec 17, 6-7 PM (0)
Dec 17, 7-8 PM (0)
Dec 17, 8-9 PM (0)
Dec 17, 9-10 PM (0)
Dec 17, 10-11 PM (0)
Dec 17, 11-12 AM (0)
Dec 18, 12-1 AM (0)
Dec 18, 1-2 AM (0)
Dec 18, 2-3 AM (0)
Dec 18, 3-4 AM (0)
Dec 18, 4-5 AM (0)
Dec 18, 5-6 AM (0)
Dec 18, 6-7 AM (0)
Dec 18, 7-8 AM (0)
Dec 18, 8-9 AM (0)
Dec 18, 9-10 AM (0)
Dec 18, 10-11 AM (0)
Dec 18, 11-12 PM (0)
Dec 18, 12-1 PM (0)
Dec 18, 1-2 PM (0)
Dec 18, 2-3 PM (0)
Dec 18, 3-4 PM (0)
Dec 18, 4-5 PM (0)
Dec 18, 5-6 PM (1)
Dec 18, 6-7 PM (0)
Dec 18, 7-8 PM (0)
Dec 18, 8-9 PM (4)
Dec 18, 9-10 PM (0)
Dec 18, 10-11 PM (1)
Dec 18, 11-12 AM (1)
Dec 19, 12-1 AM (1)
Dec 19, 1-2 AM (0)
Dec 19, 2-3 AM (0)
Dec 19, 3-4 AM (2)
Dec 19, 4-5 AM (2)
Dec 19, 5-6 AM (2)
Dec 19, 6-7 AM (0)
Dec 19, 7-8 AM (0)
Dec 19, 8-9 AM (0)
Dec 19, 9-10 AM (0)
Dec 19, 10-11 AM (0)
Dec 19, 11-12 PM (0)
Dec 19, 12-1 PM (0)
Dec 19, 1-2 PM (0)
Dec 19, 2-3 PM (0)
Dec 19, 3-4 PM (0)
Dec 19, 4-5 PM (0)
Dec 19, 5-6 PM (0)
Dec 19, 6-7 PM (0)
Dec 19, 7-8 PM (2)
Dec 19, 8-9 PM (1)
Dec 19, 9-10 PM (1)
Dec 19, 10-11 PM (0)
Dec 19, 11-12 AM (0)
Dec 20, 12-1 AM (0)
Dec 20, 1-2 AM (0)
Dec 20, 2-3 AM (0)
Dec 20, 3-4 AM (0)
Dec 20, 4-5 AM (0)
Dec 20, 5-6 AM (0)
Dec 20, 6-7 AM (0)
Dec 20, 7-8 AM (0)
Dec 20, 8-9 AM (0)
Dec 20, 9-10 AM (0)
Dec 20, 10-11 AM (0)
Dec 20, 11-12 PM (0)
Dec 20, 12-1 PM (0)
Dec 20, 1-2 PM (0)
Dec 20, 2-3 PM (0)
Dec 20, 3-4 PM (0)
Dec 20, 4-5 PM (0)
Dec 20, 5-6 PM (0)
Dec 20, 6-7 PM (0)
Dec 20, 7-8 PM (0)
Dec 20, 8-9 PM (0)
Dec 20, 9-10 PM (0)
Dec 20, 10-11 PM (0)
Dec 20, 11-12 AM (0)
Dec 21, 12-1 AM (0)
Dec 21, 1-2 AM (0)
Dec 21, 2-3 AM (0)
Dec 21, 3-4 AM (2)
Dec 21, 4-5 AM (1)
Dec 21, 5-6 AM (2)
Dec 21, 6-7 AM (3)
Dec 21, 7-8 AM (4)
Dec 21, 8-9 AM (3)
Dec 21, 9-10 AM (0)
Dec 21, 10-11 AM (0)
Dec 21, 11-12 PM (0)
Dec 21, 12-1 PM (0)
Dec 21, 1-2 PM (0)
Dec 21, 2-3 PM (0)
Dec 21, 3-4 PM (0)
Dec 21, 4-5 PM (0)
Dec 21, 5-6 PM (0)
Dec 21, 6-7 PM (0)
Dec 21, 7-8 PM (0)
Dec 21, 8-9 PM (0)
Dec 21, 9-10 PM (0)
Dec 21, 10-11 PM (0)
Dec 21, 11-12 AM (0)
Dec 22, 12-1 AM (0)
Dec 22, 1-2 AM (0)
Dec 22, 2-3 AM (0)
Dec 22, 3-4 AM (1)
Dec 22, 4-5 AM (2)
Dec 22, 5-6 AM (2)
Dec 22, 6-7 AM (0)
Dec 22, 7-8 AM (0)
Dec 22, 8-9 AM (0)
Dec 22, 9-10 AM (0)
Dec 22, 10-11 AM (0)
Dec 22, 11-12 PM (2)
Dec 22, 12-1 PM (1)
Dec 22, 1-2 PM (0)
Dec 22, 2-3 PM (0)
Dec 22, 3-4 PM (2)
Dec 22, 4-5 PM (0)
Dec 22, 5-6 PM (0)
Dec 22, 6-7 PM (0)
Dec 22, 7-8 PM (0)
Dec 22, 8-9 PM (0)
Dec 22, 9-10 PM (0)
Dec 22, 10-11 PM (0)
Dec 22, 11-12 AM (0)
Dec 23, 12-1 AM (0)
Dec 23, 1-2 AM (0)
Dec 23, 2-3 AM (0)
Dec 23, 3-4 AM (0)
Dec 23, 4-5 AM (0)
Dec 23, 5-6 AM (0)
Dec 23, 6-7 AM (0)
Dec 23, 7-8 AM (0)
Dec 23, 8-9 AM (0)
Dec 23, 9-10 AM (0)
Dec 23, 10-11 AM (0)
Dec 23, 11-12 PM (0)
Dec 23, 12-1 PM (1)
Dec 23, 1-2 PM (0)
Dec 23, 2-3 PM (0)
Dec 23, 3-4 PM (0)
Dec 23, 4-5 PM (0)
Dec 23, 5-6 PM (0)
Dec 23, 6-7 PM (0)
Dec 23, 7-8 PM (0)
Dec 23, 8-9 PM (0)
Dec 23, 9-10 PM (0)
Dec 23, 10-11 PM (0)
Dec 23, 11-12 AM (0)
Dec 24, 12-1 AM (0)
Dec 24, 1-2 AM (0)
Dec 24, 2-3 AM (0)
Dec 24, 3-4 AM (0)
44 commits this week
Dec 17, 2025
-
Dec 24, 2025
Artifacts generated from 5a692662fe667cd179f3908c89d69352e04b213e
Update conformance model
Artifacts generated from 2751ddda7ee7142ea8edee44f68503b87c8862cd
Add reqSignerHashes to neededVKeyHashes
Artifacts generated from f8d59b1d11654f6ed4911fd80018daf69a5b5f6d
Update src/Ledger/Dijkstra/Specification/Transaction.lagda.md
Co-authored-by: Copilot <[email protected]>
Artifacts generated from 6e1977e70e47d2592fd5ebabaa719a048bfc81b5
Artifacts generated from 37edc2bcebacae645a79fe05b16a7303da13a2cb
Adapt `txOutToP2Script` to two utxo views.
Also highlight that `getDatum` gets the datum of the spent output (look up `txin` in the UTxO; if the output stores a datum hash, look it up in `DataOf tx`). It's a spending-input datum lookup (not a reference-input datum lookup).
Artifacts generated from d1287db503c24d1f70a3c745f793c3f56ec66f9d
Artifacts generated from 34800bd70f328c0d2458a0de2a29a10e2a258b77
Artifacts generated from fa72fe90b5eff38d0f37d32f051ce6a86a5e4de5
Update CHANGELOG.md
Co-authored-by: Copilot <[email protected]>
Update src/Ledger/Dijkstra/Specification/Transaction.lagda.md
Co-authored-by: Copilot <[email protected]>
Artifacts generated from 8376dad6ec3d96a394d31ee773b61498343c1941
add `TxInfo.txInfoSubTxs` field
1. Introduce subTx info type (using an alias for `TxInfo` for now). 2. Extend `TxInfo` with field `txInfoSubTxs : Maybe (List SubTxInfo)`. 3. Define a purpose-built builder: + Top-level Guard scripts ⇒ `txInfoSubTxs = just (...)` + Everything else ⇒ `txInfoSubTxs = nothing` + SubTx scripts ⇒ always `nothing` (even for `Guard` at sub level)
Make `ScriptPurpose.Guard` carry a `Credential`
Key idea: + Keep `txGuards` as a set **for now**. + Define an ordered view `guardsList : List Credential` via `setToList`. + Make `indexOfGuard` operate on that list. + Let `rdptr` compute the `Ix` using `indexOfGuard`. For the "required top-level guards requested by subTxs" (i.e., `txRequiredTopLevelGuards` requests), we don't need a new ScriptPurpose constructor yet, because: + phase-1 ensures those requested credentials are contained in top-level `txGuards` + the later work (#1004 / #1006) will decide how to construct TxInfo / datum arguments for running those guard scripts batch-wide
Artifacts generated from 847c83558c08ff069b70b9d298954cdeb3527a92
Artifacts generated from 379d4822ba87b48fac32c02b71faada8f9ca0ada
Add initial versions of Utxo and Utxow modules
+ a minimal `UTXOS` rule as a stub/hook (so `UTXO` can call something), + a minimal `UTXO` rule with just the new phase-1 premise (plus an explicit "calls UTXOS"), + a minimal `UTXOW`; just a wrapper over `UTXO` for now.
Add `requiredTopLevelGuardsSatisfied` predicate.
Artifacts generated from 6f4abbc2757544972159813933efb345dcc9234d
Update src/Ledger/Dijkstra/Specification/Transaction.lagda.md
Co-authored-by: Copilot <[email protected]>