remove duplicate typeclass instance
Home /
Input Output /
formal-ledger-specifications
Jan 04, 6-7 PM (0)
Jan 04, 7-8 PM (0)
Jan 04, 8-9 PM (0)
Jan 04, 9-10 PM (0)
Jan 04, 10-11 PM (0)
Jan 04, 11-12 AM (0)
Jan 05, 12-1 AM (0)
Jan 05, 1-2 AM (0)
Jan 05, 2-3 AM (0)
Jan 05, 3-4 AM (0)
Jan 05, 4-5 AM (0)
Jan 05, 5-6 AM (0)
Jan 05, 6-7 AM (0)
Jan 05, 7-8 AM (0)
Jan 05, 8-9 AM (0)
Jan 05, 9-10 AM (3)
Jan 05, 10-11 AM (1)
Jan 05, 11-12 PM (0)
Jan 05, 12-1 PM (0)
Jan 05, 1-2 PM (0)
Jan 05, 2-3 PM (3)
Jan 05, 3-4 PM (1)
Jan 05, 4-5 PM (0)
Jan 05, 5-6 PM (0)
Jan 05, 6-7 PM (0)
Jan 05, 7-8 PM (0)
Jan 05, 8-9 PM (0)
Jan 05, 9-10 PM (0)
Jan 05, 10-11 PM (0)
Jan 05, 11-12 AM (2)
Jan 06, 12-1 AM (0)
Jan 06, 1-2 AM (0)
Jan 06, 2-3 AM (0)
Jan 06, 3-4 AM (0)
Jan 06, 4-5 AM (12)
Jan 06, 5-6 AM (0)
Jan 06, 6-7 AM (0)
Jan 06, 7-8 AM (0)
Jan 06, 8-9 AM (0)
Jan 06, 9-10 AM (0)
Jan 06, 10-11 AM (0)
Jan 06, 11-12 PM (0)
Jan 06, 12-1 PM (0)
Jan 06, 1-2 PM (0)
Jan 06, 2-3 PM (0)
Jan 06, 3-4 PM (0)
Jan 06, 4-5 PM (0)
Jan 06, 5-6 PM (0)
Jan 06, 6-7 PM (0)
Jan 06, 7-8 PM (0)
Jan 06, 8-9 PM (0)
Jan 06, 9-10 PM (0)
Jan 06, 10-11 PM (0)
Jan 06, 11-12 AM (8)
Jan 07, 12-1 AM (9)
Jan 07, 1-2 AM (7)
Jan 07, 2-3 AM (0)
Jan 07, 3-4 AM (0)
Jan 07, 4-5 AM (0)
Jan 07, 5-6 AM (0)
Jan 07, 6-7 AM (0)
Jan 07, 7-8 AM (0)
Jan 07, 8-9 AM (0)
Jan 07, 9-10 AM (0)
Jan 07, 10-11 AM (0)
Jan 07, 11-12 PM (0)
Jan 07, 12-1 PM (14)
Jan 07, 1-2 PM (27)
Jan 07, 2-3 PM (0)
Jan 07, 3-4 PM (0)
Jan 07, 4-5 PM (0)
Jan 07, 5-6 PM (0)
Jan 07, 6-7 PM (0)
Jan 07, 7-8 PM (0)
Jan 07, 8-9 PM (0)
Jan 07, 9-10 PM (0)
Jan 07, 10-11 PM (0)
Jan 07, 11-12 AM (0)
Jan 08, 12-1 AM (0)
Jan 08, 1-2 AM (0)
Jan 08, 2-3 AM (0)
Jan 08, 3-4 AM (1)
Jan 08, 4-5 AM (1)
Jan 08, 5-6 AM (0)
Jan 08, 6-7 AM (0)
Jan 08, 7-8 AM (0)
Jan 08, 8-9 AM (0)
Jan 08, 9-10 AM (1)
Jan 08, 10-11 AM (0)
Jan 08, 11-12 PM (0)
Jan 08, 12-1 PM (1)
Jan 08, 1-2 PM (1)
Jan 08, 2-3 PM (18)
Jan 08, 3-4 PM (5)
Jan 08, 4-5 PM (1)
Jan 08, 5-6 PM (0)
Jan 08, 6-7 PM (0)
Jan 08, 7-8 PM (0)
Jan 08, 8-9 PM (0)
Jan 08, 9-10 PM (0)
Jan 08, 10-11 PM (0)
Jan 08, 11-12 AM (0)
Jan 09, 12-1 AM (0)
Jan 09, 1-2 AM (13)
Jan 09, 2-3 AM (6)
Jan 09, 3-4 AM (3)
Jan 09, 4-5 AM (2)
Jan 09, 5-6 AM (7)
Jan 09, 6-7 AM (0)
Jan 09, 7-8 AM (0)
Jan 09, 8-9 AM (0)
Jan 09, 9-10 AM (15)
Jan 09, 10-11 AM (0)
Jan 09, 11-12 PM (0)
Jan 09, 12-1 PM (0)
Jan 09, 1-2 PM (1)
Jan 09, 2-3 PM (13)
Jan 09, 3-4 PM (0)
Jan 09, 4-5 PM (0)
Jan 09, 5-6 PM (0)
Jan 09, 6-7 PM (0)
Jan 09, 7-8 PM (0)
Jan 09, 8-9 PM (0)
Jan 09, 9-10 PM (0)
Jan 09, 10-11 PM (0)
Jan 09, 11-12 AM (10)
Jan 10, 12-1 AM (1)
Jan 10, 1-2 AM (0)
Jan 10, 2-3 AM (0)
Jan 10, 3-4 AM (0)
Jan 10, 4-5 AM (0)
Jan 10, 5-6 AM (0)
Jan 10, 6-7 AM (0)
Jan 10, 7-8 AM (0)
Jan 10, 8-9 AM (0)
Jan 10, 9-10 AM (0)
Jan 10, 10-11 AM (0)
Jan 10, 11-12 PM (0)
Jan 10, 12-1 PM (0)
Jan 10, 1-2 PM (0)
Jan 10, 2-3 PM (0)
Jan 10, 3-4 PM (0)
Jan 10, 4-5 PM (0)
Jan 10, 5-6 PM (0)
Jan 10, 6-7 PM (0)
Jan 10, 7-8 PM (0)
Jan 10, 8-9 PM (0)
Jan 10, 9-10 PM (0)
Jan 10, 10-11 PM (0)
Jan 10, 11-12 AM (0)
Jan 11, 12-1 AM (0)
Jan 11, 1-2 AM (0)
Jan 11, 2-3 AM (0)
Jan 11, 3-4 AM (0)
Jan 11, 4-5 AM (0)
Jan 11, 5-6 AM (0)
Jan 11, 6-7 AM (0)
Jan 11, 7-8 AM (0)
Jan 11, 8-9 AM (0)
Jan 11, 9-10 AM (0)
Jan 11, 10-11 AM (0)
Jan 11, 11-12 PM (0)
Jan 11, 12-1 PM (0)
Jan 11, 1-2 PM (0)
Jan 11, 2-3 PM (0)
Jan 11, 3-4 PM (0)
Jan 11, 4-5 PM (0)
Jan 11, 5-6 PM (0)
Jan 11, 6-7 PM (0)
187 commits this week
Jan 04, 2026
-
Jan 11, 2026
first pass at the UTXOS rule
Add support for batch-level validity checking
Add batch-level coin mint constraint to prevent Ada forgery (#1023)
* improvements * Initial plan * Add batchMintedCoin constraint to prevent Ada forgery Co-authored-by: williamdemeo <[email protected]> * Add documentation for batchMintedCoin security constraint Co-authored-by: williamdemeo <[email protected]> * Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <[email protected]> --------- Co-authored-by: William DeMeo <[email protected]> Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: williamdemeo <[email protected]>
[Dijkstra] Fix collectP2ScriptsWithContext: TxLevel-indexed txInfo + split UTxO views
- Update collectP2ScriptsWithContext to take both utxoSpendâ‚€ (initial snapshot) and utxoRefView (for reference lookups), preparing for batch-aware collection and single phase-2 eval. - Use txInfoForPurpose to construct validation context (TxLevel-indexed) instead of Conway's language-indexed txInfo. Dijkstra txInfo is indexed by TxLevel, not by Plutus language.
Add batch-level coin mint constraint to prevent Ada forgery (#1023)
* improvements * Initial plan * Add batchMintedCoin constraint to prevent Ada forgery Co-authored-by: williamdemeo <[email protected]> * Add documentation for batchMintedCoin security constraint Co-authored-by: williamdemeo <[email protected]> * Use consistent aggregation syntax for batchMintedCoin Co-authored-by: williamdemeo <[email protected]> --------- Co-authored-by: William DeMeo <[email protected]> Co-authored-by: copilot-swe-agent[bot] <[email protected]> Co-authored-by: williamdemeo <[email protected]>
[Dijkstra] Fix collectP2ScriptsWithContext: TxLevel-indexed txInfo + split UTxO views
- Update collectP2ScriptsWithContext to take both utxoSpendâ‚€ (initial snapshot) and utxoRefView (for reference lookups), preparing for batch-aware collection and single phase-2 eval. - Use txInfoForPurpose to construct validation context (TxLevel-indexed) instead of Conway's language-indexed txInfo. Dijkstra txInfo is indexed by TxLevel, not by Plutus language.
Add preliminary check that txIns exist in the UTxO prior to any changes
Update src/Ledger/Dijkstra/Specification/Transaction.lagda.md
Co-authored-by: Copilot <[email protected]>
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).
Fix prose explaining CIP 118.
+ Remove contradiction between "ref inputs may refer to earlier tx outputs in the batch" vs "all inputs must exist before applying any tx in the batch." The new text punts the exact constraint to the UTxO rules (where it belongs). + Fix Plutus bullet (old "nor earlier versions" reads like "no Plutus at all"). + Align fees with current Agda (`txFee : InTopLevel …`), but leave room for later CIP-driven updates.
Update CHANGELOG.md
Co-authored-by: Copilot <[email protected]>