From ea9a7fb7212869705b0dd8ae34ce09b3f255dbb7 Mon Sep 17 00:00:00 2001
From: Andre Knispel <andre.knispel@gmx.de>
Date: Wed, 17 Apr 2024 14:01:39 +0200
Subject: [PATCH] Require reference inputs to be disjoint from regular inputs
 (#393)

---
 src/Ledger/Utxo.lagda               | 4 ++--
 src/Ledger/hs-src/test/UtxowSpec.hs | 4 ++--
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/Ledger/Utxo.lagda b/src/Ledger/Utxo.lagda
index 5e2d7edd..ecc1f59d 100644
--- a/src/Ledger/Utxo.lagda
+++ b/src/Ledger/Utxo.lagda
@@ -393,8 +393,8 @@ data _⊢_⇀⦇_,UTXO⦈_ where
         open UTxOState s
         txoutsʰ = (mapValues txOutHash txouts)
     in
-    ∙ txins ≢ ∅                              ∙ txins ⊆ dom utxo
-    ∙ refInputs ⊆ dom utxo                   ∙ inInterval slot txvldt
+    ∙ txins ≢ ∅                              ∙ txins ∪ refInputs ⊆ dom utxo
+    ∙ txins ∩ refInputs ≡ ∅                  ∙ inInterval slot txvldt
     ∙ feesOK pp tx utxo ≡ true               ∙ consumed pp s txb ≡ produced pp s txb
     ∙ coin mint ≡ 0                          ∙ txsize ≤ maxTxSize pp
 
diff --git a/src/Ledger/hs-src/test/UtxowSpec.hs b/src/Ledger/hs-src/test/UtxowSpec.hs
index ed02daf4..25f173f9 100644
--- a/src/Ledger/hs-src/test/UtxowSpec.hs
+++ b/src/Ledger/hs-src/test/UtxowSpec.hs
@@ -69,7 +69,7 @@ bodyFromSimple pp stxb = let s = 5 in MkTxBody
 testTxBody1 :: TxBody
 testTxBody1 = bodyFromSimple initParams $ MkSimpleTxBody
   { stxins     = [(0, 0)]
-  , srefInputs = [(0, 0)]
+  , srefInputs = []
   , stxouts    = [ 0 .-> (a0, (890, (Nothing, Nothing)))
                  , 1 .-> (a1, (100, (Nothing, Nothing))) ]
   , stxvldt    = (Nothing, Just 10)
@@ -85,7 +85,7 @@ testTx1 = MkTx
 testTxBody2 :: TxBody
 testTxBody2 = bodyFromSimple initParams $ MkSimpleTxBody
   { stxins     = [(1, 1)]
-  , srefInputs = [(1, 1)]
+  , srefInputs = [(1, 0)]
   , stxouts    = [ 0 .-> (a2, (10, (Nothing, Nothing)))
                  , 1 .-> (a1, (80, (Nothing, Nothing))) ]
   , stxvldt    = (Nothing, Just 10)