Merge pull request #1086 from input-output-hk/shelley/property_based_…

…tests/MIR_certs

Properties for generated MIR certificates

shelley/chain-and-ledger/executable-spec/test/PropertyTests.hs

@@ -26,7 +26,8 @@ import           LedgerState hiding (genDelegs)
 import           PParams
 import           Rules.ClassifyTraces (onlyValidLedgerSignalsAreGenerated, relevantCasesAreCovered)
 import           Rules.TestLedger (credentialRemovedAfterDereg, pStateIsInternallyConsistent,
-                     poolIsMarkedForRetirement, registeredPoolIsAdded, rewardZeroAfterReg)
+                     poolIsMarkedForRetirement, prop_MIRValuesEndUpInMap,
+                     prop_MIRentriesEndUpInMap, registeredPoolIsAdded, rewardZeroAfterReg)
 import           Slot
 import           Tx (pattern TxIn, pattern TxOut, body, certs, inputs, outputs, witnessVKeySet,
                      _body, _witnessVKeySet)
@@ -175,6 +176,14 @@ propertyTests = testGroup "Property-Based Testing"
                   , testProperty "pool state is internally consistent"
                                  pStateIsInternallyConsistent
                   ]
+                , testGroup "STS Rules - MIR certificates"
+                  [ TQC.testProperty "entries of MIR certificate are added to\
+                                 \ irwd mapping"
+                    prop_MIRentriesEndUpInMap
+                  , TQC.testProperty "coin values of entries of a MIR certificate\
+                                     \ are added to the irwd mapping"
+                    prop_MIRValuesEndUpInMap
+                  ]
                 , testGroup "Ledger Genesis State"
                   [testProperty
                     "non-empty genesis ledger state has non-zero balance"

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

@@ -9,17 +9,21 @@ module Rules.TestDeleg
   , credentialRemovedAfterDereg
   , rewardZeroAfterReg
   , rewardsSumInvariant
+  , instantaneousRewardsAdded
+  , instantaneousRewardsValue
   )
 where
 
 import           Data.Map (Map)
-import qualified Data.Map.Strict as Map (difference, filter, lookup)
+import qualified Data.Map.Strict as Map (difference, filter, foldl, keysSet, lookup, (\\))
 import qualified Data.Maybe as Maybe (maybe)
 import           Data.Set (Set)
-import qualified Data.Set as Set (singleton, size)
+import qualified Data.Set as Set (isSubsetOf, singleton, size)
 import           Data.Word (Word64)
 import           Hedgehog (MonadTest, Property, TestLimit, forAll, property, withTests)
 
+import qualified Test.QuickCheck as QC
+
 import           Address (mkRwdAcnt)
 import           BaseTypes ((==>))
 
@@ -30,10 +34,11 @@ import           Generator.LedgerTrace ()
 import           Ledger.Core (dom, range, (∈), (∉), (◁))
 
 import           Coin (Coin, pattern Coin)
-import           LedgerState (_delegations, _rewards, _stkCreds)
+import           LedgerState (_delegations, _irwd, _rewards, _stkCreds)
 import           MockTypes (DELEG, DState, KeyHash, RewardAcnt, StakeCredential)
 import           Test.Utils (assertAll)
-import           TxData (pattern DeRegKey, pattern Delegate, pattern Delegation, pattern RegKey)
+import           TxData (pattern DeRegKey, pattern Delegate, pattern Delegation,
+                     pattern InstantaneousRewards, pattern RegKey)
 
 -------------------------------
 -- helper accessor functions --
@@ -133,3 +138,31 @@ rewardsSumInvariant = withTests (fromIntegral numberOfTests) . property $ do
              null (Map.filter (/= Coin 0) $ rew `Map.difference` rew')
           && -- added elements have a zero reward balance
              null (Map.filter (/= Coin 0) $ rew' `Map.difference` rew)
+
+-- | Check that an accepted MIR certificate adds all entries to the `irwd` mapping
+instantaneousRewardsAdded ::  [SourceSignalTarget DELEG] -> QC.Property
+instantaneousRewardsAdded ssts =
+  QC.conjoin (map checkMIR ssts)
+  where
+    checkMIR :: SourceSignalTarget DELEG -> QC.Property
+    checkMIR (SourceSignalTarget _ t sig) =
+      case sig of
+        InstantaneousRewards irwd -> QC.property $ Map.keysSet irwd `Set.isSubsetOf` Map.keysSet (_irwd t)
+        _                         -> QC.property ()
+
+-- | Check that an accepted MIR certificate adds the overall value in the
+-- certificate to the existing value in the `irwd` map, overwriting any entries
+-- that already existed.
+instantaneousRewardsValue ::  [SourceSignalTarget DELEG] -> QC.Property
+instantaneousRewardsValue ssts =
+  QC.conjoin (map checkMIR ssts)
+  where
+    checkMIR :: SourceSignalTarget DELEG -> QC.Property
+    checkMIR (SourceSignalTarget s t sig) =
+      case sig of
+        InstantaneousRewards irwd ->
+          QC.property $
+          ((Map.foldl (+) (Coin 0) $ _irwd s Map.\\ irwd) +
+           (Map.foldl (+) (Coin 0) $ irwd) ==
+           (Map.foldl (+) (Coin 0) $ _irwd t))
+        _                         -> QC.property ()

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

@@ -12,6 +12,8 @@ module Rules.TestLedger
   , registeredPoolIsAdded
   , poolIsMarkedForRetirement
   , pStateIsInternallyConsistent
+  , prop_MIRentriesEndUpInMap
+  , prop_MIRValuesEndUpInMap
   )
 where
 
@@ -137,6 +139,24 @@ poolIsMarkedForRetirement = do
       let sst = concatMap ledgerToPoolSsts (sourceSignalTargets tr)
         in TestPool.poolIsMarkedForRetirement sst
 
+-- | Check that `InstantaneousRewards` certificate entries are added to the
+-- Instantaneous Rewards map.
+prop_MIRentriesEndUpInMap :: QC.Property
+prop_MIRentriesEndUpInMap =
+  QC.withMaxSuccess (fromIntegral numberOfTests) . QC.property $ do
+  TQC.forAllTraceFromInitState traceLen traceLen (Just GQ.mkGenesisLedgerState) $ \tr ->
+    let sst = concatMap ledgerToDelegSsts (sourceSignalTargets tr)
+    in  TestDeleg.instantaneousRewardsAdded sst
+
+-- | Check that the coin values in `InstantaneousRewards` certificate entries
+-- are added to the Instantaneous Rewards map.
+prop_MIRValuesEndUpInMap :: QC.Property
+prop_MIRValuesEndUpInMap =
+  QC.withMaxSuccess (fromIntegral numberOfTests) . QC.property $ do
+  TQC.forAllTraceFromInitState traceLen traceLen (Just GQ.mkGenesisLedgerState) $ \tr ->
+    let sst = concatMap ledgerToDelegSsts (sourceSignalTargets tr)
+    in  TestDeleg.instantaneousRewardsValue sst
+
 pStateIsInternallyConsistent :: Property
 pStateIsInternallyConsistent = do
   withTests (fromIntegral numberOfTests) . property $ do