Remove the (now invalid) circulationDepositsInvariant property

IntersectMBO · May 5, 2020 · fc77f8f · fc77f8f
1 parent cdd1d11
commit fc77f8f
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 44 deletions.
diff --git a/shelley/chain-and-ledger/executable-spec/test/Test/Shelley/Spec/Ledger/Rules/TestChain.hs b/shelley/chain-and-ledger/executable-spec/test/Test/Shelley/Spec/Ledger/Rules/TestChain.hs
@@ -8,7 +8,6 @@ module Test.Shelley.Spec.Ledger.Rules.TestChain
   , nonNegativeDeposits
   , removedAfterPoolreap
     -- TestNewEpoch
-  , circulationDepositsInvariant
   , preservationOfAda)
 where
 
@@ -75,12 +74,6 @@ preservationOfAda =
     let sst = map chainToNewEpochSst (sourceSignalTargets tr)
     in TestNewEpoch.preservationOfAda sst
 
-circulationDepositsInvariant :: Property
-circulationDepositsInvariant =
-  forAllChainTrace $ \tr ->
-    let sst = map chainToNewEpochSst (sourceSignalTargets tr)
-    in TestNewEpoch.circulationDepositsInvariant sst
-
 ---------------------------
 -- Utils --
 ---------------------------
@@ -131,7 +124,7 @@ chainToNewEpochSst (SourceSignalTarget ChainState {chainNes = nes}
 
 -- | Transform the [(source, signal, target)] of a CHAIN Trace
 -- by manually applying the Chain TICK Rule to each source and producing
--- [(source, signal, target)].
+-- [(source, signal, target')].
 --
 -- This allows for testing properties on traces that exclude effects of the
 -- "UTXO branches" of the STS Rule tree.

diff --git a/shelley/chain-and-ledger/executable-spec/test/Test/Shelley/Spec/Ledger/Rules/TestNewEpoch.hs b/shelley/chain-and-ledger/executable-spec/test/Test/Shelley/Spec/Ledger/Rules/TestNewEpoch.hs
@@ -1,14 +1,12 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeSynonymInstances #-}
 
 module Test.Shelley.Spec.Ledger.Rules.TestNewEpoch
-  ( preservationOfAda
-  , circulationDepositsInvariant)
+  ( preservationOfAda )
 where
 
-import           Test.QuickCheck (Property, conjoin, counterexample, (===))
+import           Test.QuickCheck (Property, conjoin)
 
 import           Control.State.Transition.Trace (SourceSignalTarget, pattern SourceSignalTarget,
                      source, target)
@@ -82,35 +80,3 @@ preservationOfAda tr =
           ) =
           reserves + treasury + sum_ rewards + balance utxo + fees + deposits_
           == reserves' + treasury' + sum_ rewards' + balance utxo' + fees' + deposits'
-
--- | Check that the circulation and deposits do not change in a NEWEPOCH
--- transition.
-circulationDepositsInvariant
-  :: [SourceSignalTarget NEWEPOCH]
-  -> Property
-circulationDepositsInvariant tr =
-  conjoin $
-    map circulationDepositsNoChange tr
-
-  where circulationDepositsNoChange
-          (SourceSignalTarget
-            { source = NewEpochState
-              { nesEs = EpochState
-                { esLState = LedgerState
-                  { _utxoState = UTxOState
-                    { _utxo = u
-                    , _deposited = d
-                    }}}}
-            , target = NewEpochState
-              { nesEs = EpochState
-                { esLState = LedgerState
-                  { _utxoState = UTxOState
-                    { _utxo = u'
-                    , _deposited = d'
-                    }}}}}
-            ) =
-          counterexample ("circulationDepositsInvariant: balance delta= "
-                          <> show (balance u - balance u')
-                          <> " && deposit delta= " <> show (d - d'))
-            $ conjoin
-              [d === d', (balance u) === (balance u')]