Skip to content

Commit

Permalink
Pass Constants as a parameter to forAllChainTrace
Browse files Browse the repository at this point in the history
for more flexibility in Generators
  • Loading branch information
teodanciu committed Feb 6, 2023
1 parent cd6b5b4 commit c3e94bc
Show file tree
Hide file tree
Showing 10 changed files with 32 additions and 20 deletions.
Expand Up @@ -35,6 +35,7 @@ import Test.Cardano.Ledger.Alonzo.AlonzoEraGen (sumCollateral)
import Test.Cardano.Ledger.Alonzo.EraMapping ()
import Test.Cardano.Ledger.Alonzo.Trace ()
import Test.Cardano.Ledger.EraBuffet (TestCrypto)
import Test.Cardano.Ledger.Shelley.Generator.Constants (defaultConstants)
import qualified Test.Cardano.Ledger.Shelley.PropertyTests as Shelley
import Test.Cardano.Ledger.Shelley.Rules.Chain (
CHAIN,
Expand Down Expand Up @@ -159,7 +160,7 @@ alonzoSpecificProps SourceSignalTarget {source = chainSt, signal = block} =

alonzoTraceTests :: Property
alonzoTraceTests =
forAllChainTrace @A traceLen $ \tr ->
forAllChainTrace @A traceLen defaultConstants $ \tr ->
conjoin $ map alonzoSpecificProps (sourceSignalTargets tr)

propertyTests :: TestTree
Expand Down
Expand Up @@ -133,6 +133,7 @@ import Lens.Micro ((&), (.~), (^.))
import Numeric.Natural (Natural)
import Test.Cardano.Ledger.Core.KeyPair (KeyPair (..), vKey)
import Test.Cardano.Ledger.Shelley.ConcreteCryptoTypes (C)
import Test.Cardano.Ledger.Shelley.Generator.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (genCoin, genNatural)
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
import Test.Cardano.Ledger.Shelley.Rules.Chain (ChainEvent (..), ChainState (..))
Expand Down Expand Up @@ -675,15 +676,15 @@ lastElem (_ : xs) = lastElem xs
-- | Provide a legitimate NewEpochState to make an test Property
newEpochProp :: Word64 -> (NewEpochState C -> Property) -> Property
newEpochProp tracelen propf = withMaxSuccess 100 $
forAllChainTrace @C tracelen $ \tr ->
forAllChainTrace @C tracelen defaultConstants $ \tr ->
case lastElem (sourceSignalTargets tr) of
Just SourceSignalTarget {target} -> propf (chainNes target)
_ -> property True

-- | Given a NewEpochState and [ChainEvent], test a Property at every Epoch Boundary
newEpochEventsProp :: Word64 -> ([ChainEvent C] -> NewEpochState C -> Property) -> Property
newEpochEventsProp tracelen propf = withMaxSuccess 10 $
forEachEpochTrace @C 10 tracelen $ \tr ->
forEachEpochTrace @C 10 tracelen defaultConstants $ \tr ->
case lastElem (sourceSignalTargets tr) of
Just SourceSignalTarget {target} ->
propf (concat (runShelleyBase $ getEvents tr)) (chainNes target)
Expand Down
Expand Up @@ -85,6 +85,7 @@ import Data.Map (Map)
import qualified Data.Map.Strict as Map
import Lens.Micro hiding (ix)
import Lens.Micro.Extras (view)
import Test.Cardano.Ledger.Shelley.Generator.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
Expand Down Expand Up @@ -117,7 +118,7 @@ adaPreservationProps ::
) =>
Property
adaPreservationProps =
forAllChainTrace @era longTraceLen $ \tr -> do
forAllChainTrace @era longTraceLen defaultConstants $ \tr -> do
let ssts :: [SourceSignalTarget (CHAIN era)]
-- In this test, the STS Signal has this definition
-- Signal(CHAIN era) = Block (BHeader (EraCrypto era)) era
Expand Down Expand Up @@ -169,7 +170,7 @@ adaIsPreserved ::
) =>
Property
adaIsPreserved =
forAllChainTrace @era longTraceLen $ \tr -> do
forAllChainTrace @era longTraceLen defaultConstants $ \tr -> do
let ssts :: [SourceSignalTarget (CHAIN era)]
-- Signal(CHAIN era) = Block (BHeader (EraCrypto era)) era
ssts = sourceSignalTargets tr
Expand Down
Expand Up @@ -42,6 +42,7 @@ import Data.Proxy
import Data.Set (Set)
import qualified Data.Set as Set
import Lens.Micro hiding (ix)
import Test.Cardano.Ledger.Shelley.Generator.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ScriptClass (scriptKeyCombinations)
Expand Down Expand Up @@ -69,7 +70,7 @@ collisionFreeProps ::
) =>
Property
collisionFreeProps =
forAllChainTrace @era traceLen $ \tr -> do
forAllChainTrace @era traceLen defaultConstants $ \tr -> do
let ssts = sourceSignalTargets tr
conjoin . concat $
[ -- collision freeness
Expand Down
Expand Up @@ -40,6 +40,7 @@ import Data.List (foldl')
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Lens.Micro.Extras (view)
import Test.Cardano.Ledger.Shelley.Generator.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
Expand Down Expand Up @@ -70,7 +71,7 @@ delegProps ::
) =>
Property
delegProps =
forAllChainTrace @era traceLen $ \tr -> do
forAllChainTrace @era traceLen defaultConstants $ \tr -> do
conjoin $
map chainProp (sourceSignalTargets tr)
where
Expand Down
Expand Up @@ -43,6 +43,7 @@ import Control.State.Transition.Trace (
import qualified Control.State.Transition.Trace.Generator.QuickCheck as QC
import Data.Default.Class (Default)
import qualified Data.Map.Strict as Map
import Test.Cardano.Ledger.Shelley.Generator.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
Expand All @@ -68,9 +69,9 @@ depositsProps ::
depositsProps =
testGroup
"Deposit Invariants"
[ TQC.testProperty "Non negative deposits" (shortChainTrace (nonNegativeDeposits @era))
, TQC.testProperty "Deposits = KeyDeposits + PoolDeposits" (shortChainTrace (depositInvariant @era))
, TQC.testProperty "Reward domain = Deposit domain" (shortChainTrace (rewardDepositDomainInvariant @era))
[ TQC.testProperty "Non negative deposits" (shortChainTrace defaultConstants (nonNegativeDeposits @era))
, TQC.testProperty "Deposits = KeyDeposits + PoolDeposits" (shortChainTrace defaultConstants (depositInvariant @era))
, TQC.testProperty "Reward domain = Deposit domain" (shortChainTrace defaultConstants (rewardDepositDomainInvariant @era))
]

-- | Check that deposits are always non-negative
Expand Down
Expand Up @@ -60,6 +60,7 @@ import qualified Data.Map.Strict as Map
import Data.Proxy
import qualified Data.VMap as VMap
import Lens.Micro hiding (ix)
import Test.Cardano.Ledger.Shelley.Generator.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
Expand All @@ -85,7 +86,7 @@ incrStakeComputationProp ::
) =>
Property
incrStakeComputationProp =
forAllChainTrace @era longTraceLen $ \tr -> do
forAllChainTrace @era longTraceLen defaultConstants $ \tr -> do
let ssts = sourceSignalTargets tr

conjoin . concat $
Expand Down Expand Up @@ -150,7 +151,7 @@ incrStakeComparisonProp ::
Proxy era ->
Property
incrStakeComparisonProp Proxy =
forAllChainTrace traceLen $ \tr ->
forAllChainTrace traceLen defaultConstants $ \tr ->
conjoin $
map (\(SourceSignalTarget _ target _) -> checkIncrementalStake @era ((nesEs . chainNes) target)) $
filter (not . sameEpoch) (sourceSignalTargets tr)
Expand Down
Expand Up @@ -43,6 +43,7 @@ import Data.Default.Class (Default)
import qualified Data.Map.Strict as Map
import qualified Data.Set as Set
import Lens.Micro.Extras (view)
import Test.Cardano.Ledger.Shelley.Generator.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
Expand Down Expand Up @@ -74,7 +75,7 @@ poolProps ::
) =>
Property
poolProps =
forAllChainTrace @era traceLen $ \tr -> do
forAllChainTrace @era traceLen defaultConstants $ \tr -> do
let ssts = sourceSignalTargets tr
conjoin . concat $
[ map poolRetirement ssts
Expand Down
Expand Up @@ -45,6 +45,7 @@ import Control.State.Transition.Trace (
import qualified Control.State.Transition.Trace.Generator.QuickCheck as QC
import Data.Default.Class (Default)
import qualified Data.Set as Set
import Test.Cardano.Ledger.Shelley.Generator.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
Expand Down Expand Up @@ -72,7 +73,7 @@ poolReapProps ::
) =>
Property
poolReapProps =
forAllChainTrace traceLen $ \tr ->
forAllChainTrace traceLen defaultConstants $ \tr ->
conjoin $
map removedAfterPoolreap_ $
filter (not . sameEpoch) (chainSstWithTick tr)
Expand Down
Expand Up @@ -73,7 +73,7 @@ import qualified Data.Set as Set
import Data.Word (Word64)
import Lens.Micro.Extras (view)
import Test.Cardano.Ledger.Shelley.Generator.Block (tickChainState)
import Test.Cardano.Ledger.Shelley.Generator.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Constants (Constants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import qualified Test.Cardano.Ledger.Shelley.Generator.Presets as Preset (genEnv)
Expand Down Expand Up @@ -126,9 +126,10 @@ shortChainTrace ::
, Default (PPUPState era)
, EraTallyState era
) =>
Constants ->
(SourceSignalTarget (CHAIN era) -> Property) ->
Property
shortChainTrace f = withMaxSuccess 100 $ forAllChainTrace @era 10 $ \tr -> conjoin (map f (sourceSignalTargets tr))
shortChainTrace constants f = withMaxSuccess 100 $ forAllChainTrace @era 10 constants $ \tr -> conjoin (map f (sourceSignalTargets tr))

----------------------------------------------------------------------
-- Projections of CHAIN Trace
Expand Down Expand Up @@ -304,15 +305,16 @@ forAllChainTrace ::
, EraTallyState era
) =>
Word64 -> -- trace length
Constants ->
(Trace (CHAIN era) -> prop) ->
Property
forAllChainTrace n prop =
forAllChainTrace n constants prop =
withMaxSuccess (fromIntegral numberOfTests) . property $
forAllTraceFromInitState
testGlobals
n
(Preset.genEnv p defaultConstants)
(Just $ mkGenesisChainState (Preset.genEnv p defaultConstants))
(Preset.genEnv p constants)
(Just $ mkGenesisChainState (Preset.genEnv p constants))
prop
where
p :: Proxy era
Expand All @@ -329,9 +331,10 @@ forEachEpochTrace ::
) =>
Int ->
Word64 ->
Constants ->
(Trace (CHAIN era) -> prop) ->
Property
forEachEpochTrace subtracecount tracelen f = forAllChainTrace tracelen action
forEachEpochTrace subtracecount tracelen constants f = forAllChainTrace tracelen constants action
where
-- split at contiguous elements with different Epoch numbers
p new old = (nesEL . chainNes) new /= (nesEL . chainNes) old
Expand Down

0 comments on commit c3e94bc

Please sign in to comment.