Add LEDGER property for conservation of value in UTXO and DELEGS

shelley/chain-and-ledger/executable-spec/test/Rules/TestLedger.hs

@@ -1,37 +1,49 @@
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeSynonymInstances #-}
 
 module Rules.TestLedger
-  (rewardZeroAfterReg)
+  ( rewardZeroAfterReg
+  , consumedEqualsProduced
+  )
 where
 
 import           Data.Foldable (toList)
+import           Data.Word (Word64)
+
 import           Hedgehog (Property, forAll, property, withTests)
 
-import           Control.State.Transition.Generator (ofLengthAtLeast, traceOfLengthWithInitState)
+import           Control.State.Transition.Generator (ofLengthAtLeast, trace,
+                     traceOfLengthWithInitState)
 import           Control.State.Transition.Trace (SourceSignalTarget, pattern SourceSignalTarget,
-                     sourceSignalTargets)
+                     source, sourceSignalTargets, target)
 import           Generator.Core (mkGenesisLedgerState)
 import           Generator.LedgerTrace ()
-import           LedgerState (pattern DPState)
+
+import           Coin (pattern Coin)
+import           LedgerState (pattern DPState, pattern DState, pattern UTxOState, _deposited,
+                     _dstate, _fees, _rewards, _utxo)
 import           MockTypes (DELEG, LEDGER)
 import qualified Rules.TestDeleg as TestDeleg
 import           TxData (_body, _certs)
+import           UTxO (balance)
+
+import           Test.Utils (assertAll)
 
 ------------------------------
 -- Constants for Properties --
 ------------------------------
 
-numberOfTests :: Int
+numberOfTests :: Word64
 numberOfTests = 300
 
-traceLen :: Int
+traceLen :: Word64
 traceLen = 100
 
---------------------------
--- Properties for DELEG --
---------------------------
+---------------------------
+-- Properties for LEDGER --
+---------------------------
 
 -- | Check that a newly registered key has a reward of 0.
 rewardZeroAfterReg :: Property
@@ -49,3 +61,35 @@ rewardZeroAfterReg = withTests (fromIntegral numberOfTests) . property $ do
           -> [SourceSignalTarget DELEG]
         toCerts (SourceSignalTarget (_, DPState d _) (_, DPState d' _) tx) =
           [SourceSignalTarget d d' cert | cert <- toList . _certs . _body $ tx]
+
+
+-- | Check that the value consumed by UTXO is equal to the value produced in
+-- DELEGS
+consumedEqualsProduced :: Property
+consumedEqualsProduced = withTests (fromIntegral numberOfTests) . property $ do
+  tr <- fmap sourceSignalTargets
+        $ forAll
+        $ trace @LEDGER traceLen `ofLengthAtLeast` 1
+
+  assertAll consumedSameAsGained tr
+
+  where consumedSameAsGained (SourceSignalTarget
+                               { source = (UTxOState
+                                           { _utxo = u
+                                           , _deposited = d
+                                           , _fees = fees
+                                           }
+                                          , DPState
+                                            { _dstate = DState { _rewards = rewards }
+                                            }
+                                          )
+                               , target = (UTxOState
+                                            { _utxo = u'
+                                            , _deposited = d'
+                                            , _fees = fees'
+                                            }
+                                         , DPState
+                                           { _dstate = DState { _rewards = rewards' }})}) =
+
+          (balance u  + d  + fees  + foldl (+) (Coin 0) rewards ) ==
+          (balance u' + d' + fees' + foldl (+) (Coin 0) rewards')