Home / Input Output / formal-ledger-specifications
Insights Pull Requests
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)
Jan 11, 7-8 PM (0)
Jan 11, 8-9 PM (0)
Jan 11, 9-10 PM (0)
Jan 11, 10-11 PM (0)
Jan 11, 11-12 AM (0)
Jan 12, 12-1 AM (0)
Jan 12, 1-2 AM (0)
Jan 12, 2-3 AM (0)
Jan 12, 3-4 AM (0)
Jan 12, 4-5 AM (0)
Jan 12, 5-6 AM (0)
Jan 12, 6-7 AM (0)
Jan 12, 7-8 AM (0)
Jan 12, 8-9 AM (0)
Jan 12, 9-10 AM (0)
Jan 12, 10-11 AM (0)
Jan 12, 11-12 PM (0)
Jan 12, 12-1 PM (0)
Jan 12, 1-2 PM (1)
Jan 12, 2-3 PM (1)
Jan 12, 3-4 PM (24)
Jan 12, 4-5 PM (1)
Jan 12, 5-6 PM (1)
Jan 12, 6-7 PM (0)
Jan 12, 7-8 PM (0)
Jan 12, 8-9 PM (0)
Jan 12, 9-10 PM (0)
Jan 12, 10-11 PM (0)
Jan 12, 11-12 AM (0)
Jan 13, 12-1 AM (0)
Jan 13, 1-2 AM (0)
Jan 13, 2-3 AM (0)
Jan 13, 3-4 AM (0)
Jan 13, 4-5 AM (2)
Jan 13, 5-6 AM (20)
Jan 13, 6-7 AM (0)
Jan 13, 7-8 AM (0)
Jan 13, 8-9 AM (0)
Jan 13, 9-10 AM (0)
Jan 13, 10-11 AM (0)
215 commits this week Jan 06, 2026 - Jan 13, 2026
Copilot
Copilot · · formal-ledger-specifications
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]>
a02a47b9 · 1007-dijkstra-utxos-batch-level-validity · 1/12 ++ 0 --
williamdemeo
williamdemeo · · formal-ledger-specifications
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.
e5c47fda · 1007-dijkstra-utxos-batch-level-validity · 1/1 ++ 1 --
williamdemeo
williamdemeo · · formal-ledger-specifications
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)
44e7076d · 1007-dijkstra-utxos-batch-level-validity · 1/2 ++ 0 --
williamdemeo
williamdemeo · · formal-ledger-specifications
[Dijkstra] batch-aware `collectP2ScriptsWithContext` (#1015) 
+  [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.

+  cleanup and explain two utxo arguments
b978ae24 · 1007-dijkstra-utxos-batch-level-validity · 5/234 ++ 122 --
Showing 25 of 215 recent commits. Check out Input Output on GitHub to see more.