{-# 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, ForAllExecTypes HasSpec 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, ForAllExecTypes HasSpec 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, ForAllExecTypes HasSpec 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, ForAllExecTypes HasSpec 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 RewardAccount Coin
Map (Credential DRepRole) (Set (Credential Staking))
VotingProcedures ConwayEra
ccccWithdrawals :: Map RewardAccount 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 RewardAccount 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, ForAllExecTypes HasSpec 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, ForAllExecTypes HasSpec 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, ForAllExecTypes HasSpec 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, ForAllExecTypes HasSpec 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 RewardAccount 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 RewardAccount Coin
ccccWithdrawals :: Map RewardAccount 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 RewardAccount Coin
ccecWithdrawals = Map RewardAccount 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, ForAllExecTypes HasSpec rule era,
 Arbitrary (ExecContext rule era)) =>
ConstrainedGeneratorBundle ctx rule era -> Property
conformsToImplConstrained_ ConstrainedGeneratorBundle () "GOV" ConwayEra
constrainedGov
      -- UTXO is disabled due to: https://github.com/IntersectMBO/cardano-ledger/issues/4876
      String -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> Spec
xprop 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, ForAllExecTypes HasSpec 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
xprop 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, ForAllExecTypes HasSpec 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
xprop 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, ForAllExecTypes HasSpec 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
xprop 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, ForAllExecTypes HasSpec 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