Require reference inputs to be disjoint from regular inputs (#393)

IntersectMBO · Apr 17, 2024 · ea9a7fb · ea9a7fb
1 parent bda4a57
commit ea9a7fb
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git 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
@@ -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)