View on GitHub
File Changes
newtype UTxO = UTxO
  { unUTxO :: Map TxIn TxOut
  } deriving stock (Show, Data, Typeable)
-
    deriving newtype (Eq, Relation)
+
    deriving newtype (Eq, Relation, Semigroup, Monoid)

                      
addValue :: TxOut -> Lovelace -> TxOut
addValue [email protected]{ value } d = tx { value = value + d }
{-# LANGUAGE FlexibleContexts #-}
+
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

                      
module Ledger.UTxO.Properties where

                      
-
import           Control.Arrow ((***))
+
import           Control.Arrow (second, (***))
import           Control.Lens (view, (&), (^.), _2)
import           Control.Monad (when)
import           Data.Foldable (foldl', traverse_)
  allTxOuts :: [Tx] -> UTxO
  allTxOuts txs = foldl' (∪) (UTxO Map.empty) (map txouts txs)

                      
+
utxoAndTxoutsMustBeDisjoint :: Property
+
utxoAndTxoutsMustBeDisjoint = withTests 300 . property $ do
+
  t <- forAll (trace @UTXOW 100)
+
  traverse_ utxoAndTxoutsAreDisjoint
+
    $ fmap (second body)
+
    $ preStatesAndSignals OldestFirst t
+
  where
+
    utxoAndTxoutsAreDisjoint (UTxOState {utxo}, tx) =
+
      dom utxo ∩ dom (txouts tx) === mempty
+

                      
--------------------------------------------------------------------------------
-- Coverage guarantees for UTxO traces
--------------------------------------------------------------------------------
      , testProperty "Relevant UTxO traces are generated" UTxO.relevantCasesAreCovered
      , testProperty "No double spending" UTxO.noDoubleSpending
      , testProperty "UTxO is outputs minus inputs" UTxO.utxoDiff
+
      , testProperty "UTxO and txouts are disjoint" UTxO.utxoAndTxoutsMustBeDisjoint
      ]
    , testTxHasTypeReps
    , testGroup "Update examples" upiendExamples