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]>

Author: Copilot

src/Ledger/Dijkstra/Specification/Transaction.lagda.md

@@ -422,18 +422,6 @@ could be either of them.
     HasReferenceInputs-Tx : HasReferenceInputs (Tx txLevel)
     HasReferenceInputs-Tx .ReferenceInputsOf = ReferenceInputsOf ∘ TxBodyOf
 
-    HasSpendInputs-TxBody : HasSpendInputs (TxBody txLevel)
-    HasSpendInputs-TxBody .SpendInputsOf = TxBody.txIns
-
-    HasSpendInputs-Tx : HasSpendInputs (Tx txLevel)
-    HasSpendInputs-Tx .SpendInputsOf = SpendInputsOf ∘ TxBodyOf
-
-    HasReferenceInputs-TxBody : HasReferenceInputs (TxBody txLevel)
-    HasReferenceInputs-TxBody .ReferenceInputsOf = TxBody.refInputs
-
-    HasReferenceInputs-Tx : HasReferenceInputs (Tx txLevel)
-    HasReferenceInputs-Tx .ReferenceInputsOf = ReferenceInputsOf ∘ TxBodyOf
-
     HasIndexedOutputs-TxBody : HasIndexedOutputs (TxBody txLevel)
     HasIndexedOutputs-TxBody .IndexedOutputsOf = TxBody.txOuts
 

src/Ledger/Dijkstra/Specification/Utxo.lagda.md

@@ -346,6 +346,12 @@ module _ (Γ : UTxOEnv) (s : UTxOState) where
     batchPOV : Type
     batchPOV = batchConsumed ≡ batchProduced
 
+    -- Total Ada minted across the entire batch (top-level tx + all sub-txs).
+    -- This must equal 0 to prevent Ada forgery and maintain the total Ada supply invariant.
+    -- Analogous to Conway's `coin mint ≡ 0` constraint, but generalized to batches.
+    batchMintedCoin : Coin
+    batchMintedCoin = coin (MintedValueOf txTop) + sum (map (λ txSub → coin (MintedValueOf txSub)) (SubTransactionsOf txTop))
+
 
 
 module Batch (Γ : UTxOEnv) (s : UTxOState) (txTop : TopLevelTx) where
@@ -398,13 +404,18 @@ module Batch (Γ : UTxOEnv) (s : UTxOState) (txTop : TopLevelTx) where
 
 ## The <span class="AgdaDatatype">UTXOS</span> Rule
 
+
+<!--
 ```agda
 private variable
   Γ : UTxOEnv
   s s' : UTxOState
   tx : TopLevelTx
   stx : SubLevelTx
+```
+-->
 
+```agda
 data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState → Type where
 
   UTXO-scripts✓ :
@@ -414,6 +425,7 @@ data _⊢_⇀⦇_,UTXOS⦈_ : UTxOEnv → UTxOState → TopLevelTx → UTxOState
     ∙ Tx.isValid tx ≡ batchScripts✓ Γ s tx
     ∙ batchScripts✓ Γ s tx ≡ true
     ∙ batchPOV Γ s tx
+    ∙ batchMintedCoin Γ s tx ≡ 0
       ────────────────────────────────
       Γ ⊢ s ⇀⦇ tx ,UTXOS⦈ s'-scripts✓