{-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE ImportQualifiedPost #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeApplications #-} module Test.Cardano.Ledger.Conformance.Spec.Conway (spec) where import Data.Map.Strict qualified as Map import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (ConwayCertExecContext (..)) import Test.Cardano.Ledger.Conformance.Spec.Conway.Ratify qualified as Ratify import Test.Cardano.Ledger.Conformance.Spec.Core import Test.Cardano.Ledger.Constrained.Conway (genUtxoExecContext) import Test.Cardano.Ledger.Constrained.Conway.MiniTrace ( ConwayCertGenContext (..), constrainedCert, constrainedCerts, constrainedDeleg, constrainedEnact, constrainedEpoch, constrainedGov, constrainedGovCert, constrainedPool, constrainedUtxo, ) import Test.Cardano.Ledger.Imp.Common spec :: Spec spec :: Spec spec = do String -> Spec -> Spec forall a. HasCallStack => String -> SpecWith a -> SpecWith a describe String "Constrained Generators" (Spec -> Spec) -> Spec -> Spec forall a b. (a -> b) -> a -> b $ do String -> Spec -> Spec forall a. HasCallStack => String -> SpecWith a -> SpecWith a describe String "Ticks transition graph" (Spec -> Spec) -> Spec -> Spec forall a b. (a -> b) -> a -> b $ do String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "ENACT" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle EpochNo "ENACT" ConwayEra -> (EpochNo -> Environment (EraRule "ENACT" ConwayEra) -> State (EraRule "ENACT" ConwayEra) -> Signal (EraRule "ENACT" ConwayEra) -> Gen (ExecContext "ENACT" ConwayEra)) -> Property forall ctx (rule :: Symbol) era. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era))) => ConstrainedGeneratorBundle ctx rule era -> (ctx -> Environment (EraRule rule era) -> State (EraRule rule era) -> Signal (EraRule rule era) -> Gen (ExecContext rule era)) -> Property conformsToImplConstrained ConstrainedGeneratorBundle EpochNo "ENACT" ConwayEra constrainedEnact ((EpochNo -> Environment (EraRule "ENACT" ConwayEra) -> State (EraRule "ENACT" ConwayEra) -> Signal (EraRule "ENACT" ConwayEra) -> Gen (ExecContext "ENACT" ConwayEra)) -> Property) -> (EpochNo -> Environment (EraRule "ENACT" ConwayEra) -> State (EraRule "ENACT" ConwayEra) -> Signal (EraRule "ENACT" ConwayEra) -> Gen (ExecContext "ENACT" ConwayEra)) -> Property forall a b. (a -> b) -> a -> b $ \EpochNo curEpoch Environment (EraRule "ENACT" ConwayEra) _ State (EraRule "ENACT" ConwayEra) _ Signal (EraRule "ENACT" ConwayEra) _ -> EpochNo -> Gen EpochNo forall a. a -> Gen a forall (f :: * -> *) a. Applicative f => a -> f a pure EpochNo curEpoch Spec Ratify.spec String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec xprop String "EPOCH" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra -> Property forall (rule :: Symbol) era ctx. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era)), Arbitrary (ExecContext rule era)) => ConstrainedGeneratorBundle ctx rule era -> Property conformsToImplConstrained_ ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra constrainedEpoch String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec xprop String "NEWEPOCH" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra -> Property forall (rule :: Symbol) era ctx. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era)), Arbitrary (ExecContext rule era)) => ConstrainedGeneratorBundle ctx rule era -> Property conformsToImplConstrained_ ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra constrainedEpoch String -> Spec -> Spec forall a. HasCallStack => String -> SpecWith a -> SpecWith a describe String "Blocks transition graph" (Spec -> Spec) -> Spec -> Spec forall a b. (a -> b) -> a -> b $ do String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "DELEG" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle (WitUniv ConwayEra, ConwayCertGenContext ConwayEra) "DELEG" ConwayEra -> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra) -> Environment (EraRule "DELEG" ConwayEra) -> State (EraRule "DELEG" ConwayEra) -> Signal (EraRule "DELEG" ConwayEra) -> Gen (ExecContext "DELEG" ConwayEra)) -> Property forall ctx (rule :: Symbol) era. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era))) => ConstrainedGeneratorBundle ctx rule era -> (ctx -> Environment (EraRule rule era) -> State (EraRule rule era) -> Signal (EraRule rule era) -> Gen (ExecContext rule era)) -> Property conformsToImplConstrained ConstrainedGeneratorBundle (WitUniv ConwayEra, ConwayCertGenContext ConwayEra) "DELEG" ConwayEra constrainedDeleg (((WitUniv ConwayEra, ConwayCertGenContext ConwayEra) -> Environment (EraRule "DELEG" ConwayEra) -> State (EraRule "DELEG" ConwayEra) -> Signal (EraRule "DELEG" ConwayEra) -> Gen (ExecContext "DELEG" ConwayEra)) -> Property) -> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra) -> Environment (EraRule "DELEG" ConwayEra) -> State (EraRule "DELEG" ConwayEra) -> Signal (EraRule "DELEG" ConwayEra) -> Gen (ExecContext "DELEG" ConwayEra)) -> Property forall a b. (a -> b) -> a -> b $ \(WitUniv ConwayEra _, ConwayCertGenContext {Map AccountAddress Coin Map (Credential DRepRole) (Set (Credential Staking)) VotingProcedures ConwayEra ccccWithdrawals :: Map AccountAddress Coin ccccVotes :: VotingProcedures ConwayEra ccccDelegatees :: Map (Credential DRepRole) (Set (Credential Staking)) ccccDelegatees :: forall era. ConwayCertGenContext era -> Map (Credential DRepRole) (Set (Credential Staking)) ccccVotes :: forall era. ConwayCertGenContext era -> VotingProcedures era ccccWithdrawals :: forall era. ConwayCertGenContext era -> Map AccountAddress Coin ..}) Environment (EraRule "DELEG" ConwayEra) _ State (EraRule "DELEG" ConwayEra) _ Signal (EraRule "DELEG" ConwayEra) _ -> ExecContext "DELEG" ConwayEra -> Gen (ExecContext "DELEG" ConwayEra) forall a. a -> Gen a forall (f :: * -> *) a. Applicative f => a -> f a pure (ExecContext "DELEG" ConwayEra -> Gen (ExecContext "DELEG" ConwayEra)) -> ExecContext "DELEG" ConwayEra -> Gen (ExecContext "DELEG" ConwayEra) forall a b. (a -> b) -> a -> b $ Map (Credential DRepRole) (Set (Credential Staking)) -> Set (Credential DRepRole) forall k a. Map k a -> Set k Map.keysSet Map (Credential DRepRole) (Set (Credential Staking)) ccccDelegatees String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "GOVCERT" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle (WitUniv ConwayEra, ConwayCertGenContext ConwayEra) "GOVCERT" ConwayEra -> Property forall (rule :: Symbol) era ctx. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era)), Arbitrary (ExecContext rule era)) => ConstrainedGeneratorBundle ctx rule era -> Property conformsToImplConstrained_ ConstrainedGeneratorBundle (WitUniv ConwayEra, ConwayCertGenContext ConwayEra) "GOVCERT" ConwayEra constrainedGovCert String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "POOL" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle (WitUniv ConwayEra) "POOL" ConwayEra -> Property forall (rule :: Symbol) era ctx. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era)), Arbitrary (ExecContext rule era)) => ConstrainedGeneratorBundle ctx rule era -> Property conformsToImplConstrained_ ConstrainedGeneratorBundle (WitUniv ConwayEra) "POOL" ConwayEra constrainedPool String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "CERT" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle (WitUniv ConwayEra, ConwayCertGenContext ConwayEra) "CERT" ConwayEra -> Property forall (rule :: Symbol) era ctx. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era)), Arbitrary (ExecContext rule era)) => ConstrainedGeneratorBundle ctx rule era -> Property conformsToImplConstrained_ ConstrainedGeneratorBundle (WitUniv ConwayEra, ConwayCertGenContext ConwayEra) "CERT" ConwayEra constrainedCert String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "CERTS" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle (WitUniv ConwayEra, ConwayCertGenContext ConwayEra) "CERTS" ConwayEra -> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra) -> Environment (EraRule "CERTS" ConwayEra) -> State (EraRule "CERTS" ConwayEra) -> Signal (EraRule "CERTS" ConwayEra) -> Gen (ExecContext "CERTS" ConwayEra)) -> Property forall ctx (rule :: Symbol) era. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era))) => ConstrainedGeneratorBundle ctx rule era -> (ctx -> Environment (EraRule rule era) -> State (EraRule rule era) -> Signal (EraRule rule era) -> Gen (ExecContext rule era)) -> Property conformsToImplConstrained ConstrainedGeneratorBundle (WitUniv ConwayEra, ConwayCertGenContext ConwayEra) "CERTS" ConwayEra constrainedCerts (((WitUniv ConwayEra, ConwayCertGenContext ConwayEra) -> Environment (EraRule "CERTS" ConwayEra) -> State (EraRule "CERTS" ConwayEra) -> Signal (EraRule "CERTS" ConwayEra) -> Gen (ExecContext "CERTS" ConwayEra)) -> Property) -> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra) -> Environment (EraRule "CERTS" ConwayEra) -> State (EraRule "CERTS" ConwayEra) -> Signal (EraRule "CERTS" ConwayEra) -> Gen (ExecContext "CERTS" ConwayEra)) -> Property forall a b. (a -> b) -> a -> b $ \(WitUniv ConwayEra _, ConwayCertGenContext {Map AccountAddress Coin Map (Credential DRepRole) (Set (Credential Staking)) VotingProcedures ConwayEra ccccDelegatees :: forall era. ConwayCertGenContext era -> Map (Credential DRepRole) (Set (Credential Staking)) ccccVotes :: forall era. ConwayCertGenContext era -> VotingProcedures era ccccWithdrawals :: forall era. ConwayCertGenContext era -> Map AccountAddress Coin ccccWithdrawals :: Map AccountAddress Coin ccccVotes :: VotingProcedures ConwayEra ccccDelegatees :: Map (Credential DRepRole) (Set (Credential Staking)) ..}) Environment (EraRule "CERTS" ConwayEra) _ State (EraRule "CERTS" ConwayEra) _ Signal (EraRule "CERTS" ConwayEra) _ -> ExecContext "CERTS" ConwayEra -> Gen (ExecContext "CERTS" ConwayEra) forall a. a -> Gen a forall (f :: * -> *) a. Applicative f => a -> f a pure (ExecContext "CERTS" ConwayEra -> Gen (ExecContext "CERTS" ConwayEra)) -> ExecContext "CERTS" ConwayEra -> Gen (ExecContext "CERTS" ConwayEra) forall a b. (a -> b) -> a -> b $ ConwayCertExecContext { ccecVotes :: VotingProcedures ConwayEra ccecVotes = VotingProcedures ConwayEra ccccVotes , ccecWithdrawals :: Map AccountAddress Coin ccecWithdrawals = Map AccountAddress Coin ccccWithdrawals } String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "GOV" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle () "GOV" ConwayEra -> Property forall (rule :: Symbol) era ctx. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era)), Arbitrary (ExecContext rule era)) => ConstrainedGeneratorBundle ctx rule era -> Property conformsToImplConstrained_ ConstrainedGeneratorBundle () "GOV" ConwayEra constrainedGov String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "UTXO" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle (UtxoExecContext ConwayEra) "UTXO" ConwayEra -> (UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property forall ctx (rule :: Symbol) era. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era))) => ConstrainedGeneratorBundle ctx rule era -> (ctx -> Environment (EraRule rule era) -> State (EraRule rule era) -> Signal (EraRule rule era) -> Gen (ExecContext rule era)) -> Property conformsToImplConstrained ConstrainedGeneratorBundle (UtxoExecContext ConwayEra) "UTXO" ConwayEra constrainedUtxo ((UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property) -> (UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property forall a b. (a -> b) -> a -> b $ \UtxoExecContext ConwayEra _ Environment (EraRule "UTXO" ConwayEra) _ State (EraRule "UTXO" ConwayEra) _ Signal (EraRule "UTXO" ConwayEra) _ -> Gen (ExecContext "UTXO" ConwayEra) Gen (UtxoExecContext ConwayEra) genUtxoExecContext String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "UTXOW" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle (UtxoExecContext ConwayEra) "UTXO" ConwayEra -> (UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property forall ctx (rule :: Symbol) era. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era))) => ConstrainedGeneratorBundle ctx rule era -> (ctx -> Environment (EraRule rule era) -> State (EraRule rule era) -> Signal (EraRule rule era) -> Gen (ExecContext rule era)) -> Property conformsToImplConstrained ConstrainedGeneratorBundle (UtxoExecContext ConwayEra) "UTXO" ConwayEra constrainedUtxo ((UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property) -> (UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property forall a b. (a -> b) -> a -> b $ \UtxoExecContext ConwayEra _ Environment (EraRule "UTXO" ConwayEra) _ State (EraRule "UTXO" ConwayEra) _ Signal (EraRule "UTXO" ConwayEra) _ -> Gen (ExecContext "UTXO" ConwayEra) Gen (UtxoExecContext ConwayEra) genUtxoExecContext String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "LEDGER" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle (UtxoExecContext ConwayEra) "UTXO" ConwayEra -> (UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property forall ctx (rule :: Symbol) era. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era))) => ConstrainedGeneratorBundle ctx rule era -> (ctx -> Environment (EraRule rule era) -> State (EraRule rule era) -> Signal (EraRule rule era) -> Gen (ExecContext rule era)) -> Property conformsToImplConstrained ConstrainedGeneratorBundle (UtxoExecContext ConwayEra) "UTXO" ConwayEra constrainedUtxo ((UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property) -> (UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property forall a b. (a -> b) -> a -> b $ \UtxoExecContext ConwayEra _ Environment (EraRule "UTXO" ConwayEra) _ State (EraRule "UTXO" ConwayEra) _ Signal (EraRule "UTXO" ConwayEra) _ -> Gen (ExecContext "UTXO" ConwayEra) Gen (UtxoExecContext ConwayEra) genUtxoExecContext String -> Property -> Spec forall prop. (HasCallStack, Testable prop) => String -> prop -> Spec prop String "LEDGERS" (Property -> Spec) -> Property -> Spec forall a b. (a -> b) -> a -> b $ ConstrainedGeneratorBundle (UtxoExecContext ConwayEra) "UTXO" ConwayEra -> (UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property forall ctx (rule :: Symbol) era. (ExecSpecRule rule era, HasSpec (Environment (EraRule rule era)), HasSpec (State (EraRule rule era))) => ConstrainedGeneratorBundle ctx rule era -> (ctx -> Environment (EraRule rule era) -> State (EraRule rule era) -> Signal (EraRule rule era) -> Gen (ExecContext rule era)) -> Property conformsToImplConstrained ConstrainedGeneratorBundle (UtxoExecContext ConwayEra) "UTXO" ConwayEra constrainedUtxo ((UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property) -> (UtxoExecContext ConwayEra -> Environment (EraRule "UTXO" ConwayEra) -> State (EraRule "UTXO" ConwayEra) -> Signal (EraRule "UTXO" ConwayEra) -> Gen (ExecContext "UTXO" ConwayEra)) -> Property forall a b. (a -> b) -> a -> b $ \UtxoExecContext ConwayEra _ Environment (EraRule "UTXO" ConwayEra) _ State (EraRule "UTXO" ConwayEra) _ Signal (EraRule "UTXO" ConwayEra) _ -> Gen (ExecContext "UTXO" ConwayEra) Gen (UtxoExecContext ConwayEra) genUtxoExecContext