Issue #263: WIP on no double spending property

byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXO.hs

@@ -3,7 +3,16 @@
 {-# LANGUAGE TypeFamilies               #-}
 
 -- | UTXO transition system
-module Cardano.Ledger.Spec.STS.UTXO where
+module Cardano.Ledger.Spec.STS.UTXO
+  ( UTXO
+  , UTxOEnv (UTxOEnv)
+  , UTxOState (UTxOState)
+  , utxo
+  , utxo0
+  , pps
+  , reserves
+  )
+where
 
 import qualified Data.Set as Set
 
@@ -20,11 +29,13 @@ import Control.State.Transition
   , (?!)
   , judgmentContext
   )
-
-import Ledger.Core (Lovelace, (∪), (⊆), (⋪), (◁), dom, range)
+import Control.State.Transition.Generator (HasTrace, envGen, sigGen)
+import Ledger.Core (Addr, mkAddr, Lovelace, (∪), (⊆), (⋪), (◁), dom, range)
 import Ledger.GlobalParams (lovelaceCap)
 import Ledger.Update (PParams)
-import Ledger.UTxO (Tx, UTxO, balance, pcMinFee, txins, txouts, value, unUTxO)
+import qualified Ledger.Update.Generators as UpdateGen
+import Ledger.UTxO (Tx, UTxO, balance, pcMinFee, txins, txouts, value, unUTxO, fromTxOuts)
+import qualified Ledger.UTxO.Generators as UTxOGen
 
 data UTXO
 
@@ -85,3 +96,23 @@ instance STS UTXO where
                            }
 
     ]
+
+
+-- | Constant list of addresses intended to be used in the generators.
+traceAddrs :: [Addr]
+traceAddrs = mkAddr <$> [0 .. 10]
+
+-- This is mostly copy-pasted from HasTrace UTXOW
+instance HasTrace UTXO where
+  envGen _
+    = UTxOEnv <$> genUTxO <*> UpdateGen.pparamsGen
+    where
+      genUTxO = do
+        txOuts <- UTxOGen.genInitialTxOuts traceAddrs
+        -- All the outputs in the initial UTxO need to refer to some
+        -- transaction id. Since there are no transactions where these outputs
+        -- come from we use the hash of the address as transaction id.
+        pure $ fromTxOuts txOuts
+
+  sigGen _ UTxOEnv { pps } st =
+    UTxOGen.genTxFromUTxO traceAddrs (pcMinFee pps) (utxo st)

byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs

@@ -9,14 +9,17 @@ import           Control.Lens (view, (&), (^.), _2)
 import           Control.Monad (when)
 import           Hedgehog (Property, classify, cover, forAll, property, success, withTests, (===))
 
+import           Control.State.Transition (Signal, State)
 import           Control.State.Transition.Generator (classifyTraceLength, trace)
 import           Control.State.Transition.Trace (Trace, TraceOrder (OldestFirst), firstAndLastState,
                      preStatesAndSignals, traceEnv, traceLength, traceSignals)
 
 import           Cardano.Ledger.Spec.STS.UTXO (UTxOState, pps, reserves, utxo)
+import           Cardano.Ledger.Spec.STS.UTXO (UTXO)
 import           Cardano.Ledger.Spec.STS.UTXOW (UTXOW)
-import           Ledger.Core (Lovelace, unLovelace, (◁))
-import           Ledger.UTxO (Tx (Tx), TxIn (TxIn), TxOut (TxOut), TxWits, balance, body, inputs,
+import           Data.Set (empty, intersection)
+import           Ledger.Core (Lovelace, unLovelace, (◁), dom)
+import           Ledger.UTxO (Tx (Tx), TxIn (TxIn), TxOut (TxOut), TxWits, UTxO, balance, body, inputs,
                      outputs, pcMinFee, txins, txouts)
 
 --------------------------------------------------------------------------------
@@ -29,6 +32,19 @@ moneyIsConstant = withTests 200 . property $ do
   (st0, st) <- firstAndLastState <$> forAll (trace @UTXOW 500)
   reserves st0 + balance (utxo st0) === reserves st + balance (utxo st)
 
+-- | Check that there is no double spending
+noDoubleSpending :: Property
+noDoubleSpending = property $ do
+  t <- forAll (trace @UTXO 500)
+  let
+    utxo0 = fst . firstAndLastState $ t :: State UTXO
+    txs = traceSignals OldestFirst t :: [Signal UTXO]
+  when (all (noCommonInputs $ utxo utxo0) txs) $ do
+    undefined
+  where
+    noCommonInputs :: UTxO -> Tx -> Bool
+    noCommonInputs utxo0 tx = dom (txouts tx) `intersection` dom utxo0 == empty
+
 --------------------------------------------------------------------------------
 -- Coverage guarantees for UTxO traces
 --------------------------------------------------------------------------------