Added example Tx specification (#4677)

* Added classes EraSpecPParams, EraSpecTxBody, EraSpecDeleg, EraSpecCert for specifying Era parametric things
Made Era parametric HasSpec instances for all type family instances of Tx TxBody TxWits TxAuxData
Added example Tx specification (bodyspec)

* Added second TxBody spec example.
All Conway HasSpec instances and EraSpecXX instances are exported
  by Test.Cardano.Ledger.Constrained.Conway.Instances
Added LedgerType.Tests

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs

@@ -109,7 +109,7 @@ import Test.Cardano.Ledger.Constrained.Conway (
   epochStateSpec,
   newEpochStateSpec,
  )
-import Test.Cardano.Ledger.Constrained.Conway.SimplePParams (
+import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams (
   committeeMaxTermLength_,
   committeeMinSize_,
   protocolVersion_,

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs

@@ -25,7 +25,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "DELEG" Conway where
 
   stateSpec _ _ = certStateSpec
 
-  signalSpec _ = delegCertSpec
+  signalSpec _ = conwayDelegCertSpec
 
   runAgdaRule env (Agda.MkCertState dState pState vState) sig =
     bimap

libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs

@@ -18,7 +18,7 @@ import Test.Cardano.Ledger.Constrained.Conway
 govEnv :: GovEnv (ConwayEra StandardCrypto)
 govEnv = genFromSpecWithSeed 10 30 (govEnvSpec @ConwayFn)
 
-singleProposalTreeSpec :: Specification ConwayFn ProposalTree
+singleProposalTreeSpec :: Specification ConwayFn (ProposalTree Conway)
 singleProposalTreeSpec = constrained $ \ppupTree ->
   [ wellFormedChildren ppupTree
   , satisfies

libs/cardano-ledger-test/cardano-ledger-test.cabal

@@ -60,16 +60,21 @@ library
         Test.Cardano.Ledger.Constrained.Conway.Epoch
         Test.Cardano.Ledger.Constrained.Conway.Gov
         Test.Cardano.Ledger.Constrained.Conway.GovCert
-        Test.Cardano.Ledger.Constrained.Conway.InstancesBasic
+        Test.Cardano.Ledger.Constrained.Conway.Instances.Basic
+        Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger
+        Test.Cardano.Ledger.Constrained.Conway.Instances.TxBody
+        Test.Cardano.Ledger.Constrained.Conway.Instances.PParams
         Test.Cardano.Ledger.Constrained.Conway.Instances
+        Test.Cardano.Ledger.Constrained.Conway.TxBodySpec
         Test.Cardano.Ledger.Constrained.Conway.Ledger
         Test.Cardano.Ledger.Constrained.Conway.NewEpoch
         Test.Cardano.Ledger.Constrained.Conway.PParams
         Test.Cardano.Ledger.Constrained.Conway.Pool
         Test.Cardano.Ledger.Constrained.Conway.Utxo
-        Test.Cardano.Ledger.Constrained.Conway.SimplePParams
+        Test.Cardano.Ledger.Constrained.Conway.ParametricSpec
         Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs
         Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.WellFormed
+        Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Tests
         Test.Cardano.Ledger.Examples.BabbageFeatures
         Test.Cardano.Ledger.Examples.AlonzoValidTxUTXOW
         Test.Cardano.Ledger.Examples.AlonzoBBODY
@@ -177,7 +182,8 @@ test-suite cardano-ledger-test
         base,
         cardano-ledger-test,
         tasty,
-        data-default-class
+        data-default-class,
+        cardano-ledger-core:testlib
 
 benchmark bench
     type:             exitcode-stdio-1.0

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Cert.hs

@@ -1,37 +1,63 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstrainedClassMethods #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ExplicitForAll #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE TypeSynonymInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+{-# LANGUAGE ViewPatterns #-}
+{-# OPTIONS_GHC -Wno-redundant-constraints #-}
 
 -- | Specs necessary to generate, environment, state, and signal
 -- for the CERT rule
 module Test.Cardano.Ledger.Constrained.Conway.Cert where
 
+import Cardano.Ledger.Allegra (Allegra)
+import Cardano.Ledger.Alonzo (Alonzo)
+import Cardano.Ledger.Babbage (Babbage, BabbageEra)
 import Cardano.Ledger.CertState
+import Cardano.Ledger.Conway (Conway, ConwayEra)
 import Cardano.Ledger.Conway.Rules
 import Cardano.Ledger.Conway.TxCert
+import Cardano.Ledger.Core
+import Cardano.Ledger.Crypto (StandardCrypto)
+import Cardano.Ledger.Mary (Mary)
+import Cardano.Ledger.Shelley (Shelley)
 import Cardano.Ledger.Shelley.API.Types
-
+import Cardano.Ledger.Shelley.TxCert (ShelleyTxCert (..))
 import Constrained
-
-import Cardano.Ledger.Conway (ConwayEra)
-import Cardano.Ledger.Crypto (StandardCrypto)
+import qualified Data.Map as Map
+import Data.Set (Set)
+import qualified Data.Set as Set
 import Test.Cardano.Ledger.Constrained.Conway.Deleg
 import Test.Cardano.Ledger.Constrained.Conway.GovCert
-import Test.Cardano.Ledger.Constrained.Conway.Instances
+import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger
 import Test.Cardano.Ledger.Constrained.Conway.PParams
 import Test.Cardano.Ledger.Constrained.Conway.Pool
+import Test.QuickCheck hiding (forAll)
 
 certEnvSpec ::
-  IsConwayUniv fn =>
-  Specification fn (CertEnv (ConwayEra StandardCrypto))
+  forall fn era.
+  (EraSpecPParams era, IsConwayUniv fn) =>
+  Specification fn (CertEnv era)
 certEnvSpec =
   constrained $ \ce ->
     match ce $ \_slot pp _currEpoch _currCommittee _proposals ->
       [ satisfies pp pparamsSpec
       ]
 
 certStateSpec ::
-  IsConwayUniv fn =>
-  Specification fn (CertState (ConwayEra StandardCrypto))
+  (IsConwayUniv fn, EraSpecDeleg era) =>
+  Specification fn (CertState era)
 certStateSpec =
   constrained $ \cs ->
     match cs $ \vState pState dState ->
@@ -40,21 +66,202 @@ certStateSpec =
       , satisfies dState dStateSpec
       ]
 
-txCertSpec ::
+conwayTxCertSpec ::
   IsConwayUniv fn =>
   CertEnv (ConwayEra StandardCrypto) ->
   CertState (ConwayEra StandardCrypto) ->
   Specification fn (ConwayTxCert (ConwayEra StandardCrypto))
-txCertSpec (CertEnv slot pp ce cc cp) certState@CertState {..} =
+conwayTxCertSpec (CertEnv slot pp ce cc cp) certState@CertState {..} =
   constrained $ \txCert ->
     caseOn
       txCert
       -- These weights try to make it equally likely that each of the many certs
       -- across the 3 categories are chosen at similar frequencies.
-      (branchW 3 $ \delegCert -> satisfies delegCert $ delegCertSpec delegEnv certState)
+      (branchW 3 $ \delegCert -> satisfies delegCert $ conwayDelegCertSpec delegEnv certState)
       (branchW 1 $ \poolCert -> satisfies poolCert $ poolCertSpec poolEnv certPState)
-      (branchW 3 $ \govCert -> satisfies govCert $ govCertSpec govCertEnv certState)
+      (branchW 2 $ \govCert -> satisfies govCert $ govCertSpec govCertEnv certState)
   where
     delegEnv = ConwayDelegEnv pp (psStakePoolParams certPState)
     poolEnv = PoolEnv slot pp
     govCertEnv = ConwayGovCertEnv pp ce cc cp
+
+-- ==============================================================
+-- Shelley Certs
+
+-- | Genesis delegations only work through the Babbage era. Hence the (AtMostEra BabbageEra era)
+genesisDelegCertSpec ::
+  forall fn era.
+  (AtMostEra BabbageEra era, IsConwayUniv fn, Era era) =>
+  DState era -> Specification fn (GenesisDelegCert (EraCrypto era))
+genesisDelegCertSpec ds =
+  let (vrfKeyHashes, coldKeyHashes) = computeSets ds
+      GenDelegs genDelegs = dsGenDelegs ds
+   in constrained $ \ [var|gdc|] ->
+        match gdc $ \ [var|gkh|] [var|vkh|] [var|hashVrf|] ->
+          [ assert $ member_ gkh (dom_ (lit genDelegs))
+          , reify gkh coldKeyHashes (\ [var|coldkeys|] -> member_ vkh coldkeys)
+          , reify gkh vrfKeyHashes (\ [var|vrfkeys|] -> member_ hashVrf vrfkeys)
+          ]
+
+-- | Compute 2 functions from the DState. Each function, given a KeyHash,
+--   returns a Set of 'Hashes', we expect certain things to be in those sets.
+--   This mimics what happens in the Cardano.Ledger.Shelley.Rules.Deleg module
+computeSets ::
+  DState era ->
+  ( KeyHash 'Genesis (EraCrypto era) -> Set (Hash (EraCrypto era) (VerKeyVRF (EraCrypto era)))
+  , KeyHash 'Genesis (EraCrypto era) -> Set (KeyHash 'GenesisDelegate (EraCrypto era))
+  )
+computeSets ds =
+  let genDelegs = unGenDelegs (dsGenDelegs ds)
+      futureGenDelegs = dsFutureGenDelegs ds
+      cod gkh = Set.fromList $ Map.elems $ Map.delete gkh genDelegs
+      fod gkh =
+        Set.fromList $ Map.elems $ Map.filterWithKey (\(FutureGenDeleg _ g) _ -> g /= gkh) futureGenDelegs
+      currentColdKeyHashes gkh = Set.map genDelegKeyHash (cod gkh)
+      currentVrfKeyHashes gkh = Set.map genDelegVrfHash (cod gkh)
+      futureColdKeyHashes gkh = Set.map genDelegKeyHash (fod gkh)
+      futureVrfKeyHashes gkh = Set.map genDelegVrfHash (fod gkh)
+      coldKeyHashes gkh = currentColdKeyHashes gkh <> futureColdKeyHashes gkh
+      vrfKeyHashes gkh = currentVrfKeyHashes gkh <> futureVrfKeyHashes gkh
+   in (vrfKeyHashes, coldKeyHashes)
+
+-- =======================================
+
+shelleyTxCertSpec ::
+  forall fn era.
+  (AtMostEra BabbageEra era, EraSpecPParams era, IsConwayUniv fn) =>
+  CertEnv era ->
+  CertState era ->
+  Specification fn (ShelleyTxCert era)
+shelleyTxCertSpec (CertEnv slot pp _ _ _) (CertState _vstate pstate dstate) =
+  constrained $ \ [var|shelleyTxCert|] ->
+    -- These weights try to make it equally likely that each of the many certs
+    -- across the 3 categories are chosen at similar frequencies.
+    (caseOn shelleyTxCert)
+      ( branchW 5 $ \ [var|deleg|] ->
+          satisfies
+            deleg
+            ( shelleyDelegCertSpec @fn @era
+                (ConwayDelegEnv pp (psStakePoolParams pstate))
+                dstate
+            )
+      )
+      (branchW 3 $ \ [var|poolCert|] -> satisfies poolCert $ poolCertSpec (PoolEnv slot pp) pstate)
+      (branchW 1 $ \ [var|genesis|] -> satisfies genesis (genesisDelegCertSpec @fn @era dstate))
+      (branchW 1 $ \ [var|_mir|] -> False) -- By design, we never generate a MIR cert
+
+-- =========================================================================
+-- Making Cert Era parametric with the EraSpecCert class
+
+class
+  ( Era era
+  , IsConwayUniv fn
+  , HasSpec fn (TxCert era)
+  ) =>
+  EraSpecCert era fn
+  where
+  txCertSpec :: CertEnv era -> CertState era -> Specification fn (TxCert era)
+  txCertKey :: TxCert era -> CertKey (EraCrypto era)
+
+instance IsConwayUniv fn => EraSpecCert Shelley fn where
+  txCertSpec = shelleyTxCertSpec
+  txCertKey = shelleyTxCertKey
+instance IsConwayUniv fn => EraSpecCert Allegra fn where
+  txCertSpec = shelleyTxCertSpec
+  txCertKey = shelleyTxCertKey
+instance IsConwayUniv fn => EraSpecCert Mary fn where
+  txCertSpec = shelleyTxCertSpec
+  txCertKey = shelleyTxCertKey
+instance IsConwayUniv fn => EraSpecCert Alonzo fn where
+  txCertSpec = shelleyTxCertSpec
+  txCertKey = shelleyTxCertKey
+instance IsConwayUniv fn => EraSpecCert Babbage fn where
+  txCertSpec = shelleyTxCertSpec
+  txCertKey = shelleyTxCertKey
+instance IsConwayUniv fn => EraSpecCert Conway fn where
+  txCertSpec = conwayTxCertSpec
+  txCertKey = conwayTxCertKey
+
+-- | Used to aggregate the key used in registering a Certificate. Different
+--   certificates use different kinds of Keys, that allows us to use one
+--   type to represent all kinds of keys (Similar to DepositPurpose)
+data CertKey c
+  = StakeKey !(Credential 'Staking c)
+  | PoolKey !(KeyHash 'StakePool c)
+  | DRepKey !(Credential 'DRepRole c)
+  | ColdKey !(Credential 'ColdCommitteeRole c)
+  | GenesisKey !(KeyHash 'Genesis c)
+  | MirKey !MIRPot
+  deriving (Eq, Show, Ord)
+
+-- | Compute the aggregate key type of a Certificater
+conwayTxCertKey :: ConwayTxCert era -> CertKey (EraCrypto era)
+conwayTxCertKey (ConwayTxCertDeleg (ConwayRegCert x _)) = StakeKey x
+conwayTxCertKey (ConwayTxCertDeleg (ConwayUnRegCert x _)) = StakeKey x
+conwayTxCertKey (ConwayTxCertDeleg (ConwayDelegCert x _)) = StakeKey x
+conwayTxCertKey (ConwayTxCertDeleg (ConwayRegDelegCert x _ _)) = StakeKey x
+conwayTxCertKey (ConwayTxCertPool (RegPool x)) = PoolKey (ppId x)
+conwayTxCertKey (ConwayTxCertPool (RetirePool x _)) = PoolKey x
+conwayTxCertKey (ConwayTxCertGov (ConwayRegDRep x _ _)) = DRepKey x
+conwayTxCertKey (ConwayTxCertGov (ConwayUnRegDRep x _)) = DRepKey x
+conwayTxCertKey (ConwayTxCertGov (ConwayUpdateDRep x _)) = DRepKey x
+conwayTxCertKey (ConwayTxCertGov (ConwayAuthCommitteeHotKey x _)) = ColdKey x
+conwayTxCertKey (ConwayTxCertGov (ConwayResignCommitteeColdKey x _)) = ColdKey x
+
+shelleyTxCertKey :: ShelleyTxCert era -> CertKey (EraCrypto era)
+shelleyTxCertKey (ShelleyTxCertDelegCert (ShelleyRegCert x)) = StakeKey x
+shelleyTxCertKey (ShelleyTxCertDelegCert (ShelleyUnRegCert x)) = StakeKey x
+shelleyTxCertKey (ShelleyTxCertDelegCert (ShelleyDelegCert x _)) = StakeKey x
+shelleyTxCertKey (ShelleyTxCertPool (RegPool x)) = PoolKey (ppId x)
+shelleyTxCertKey (ShelleyTxCertPool (RetirePool x _)) = PoolKey x
+shelleyTxCertKey (ShelleyTxCertGenesisDeleg (GenesisDelegCert a _ _)) = GenesisKey a
+shelleyTxCertKey (ShelleyTxCertMir (MIRCert p _)) = MirKey p
+
+-- =====================================================
+
+testGenesisCert ::
+  forall era. (AtMostEra BabbageEra era, EraSpecDeleg era, EraSpecPParams era) => Gen Property
+testGenesisCert = do
+  dstate <- genFromSpec @ConwayFn @(DState era) dStateSpec
+  let spec = genesisDelegCertSpec @ConwayFn dstate
+  ans <- genFromSpec @ConwayFn spec
+  pure $ property (conformsToSpec ans spec)
+
+testShelleyCert ::
+  forall era. (AtMostEra BabbageEra era, EraSpecPParams era, EraSpecDeleg era) => Gen Property
+testShelleyCert = do
+  env <- genFromSpec @ConwayFn @(CertEnv era) certEnvSpec
+  dstate <- genFromSpec @ConwayFn @(CertState era) certStateSpec
+  let spec = shelleyTxCertSpec env dstate
+  ans <- genFromSpec @ConwayFn spec
+  let tag = case ans of
+        ShelleyTxCertDelegCert x -> case x of
+          ShelleyRegCert {} -> "Register"
+          ShelleyUnRegCert {} -> "UnRegister"
+          ShelleyDelegCert {} -> "Delegate"
+        ShelleyTxCertPool x -> case x of
+          RegPool {} -> "RegPool"
+          RetirePool {} -> "RetirePool"
+        ShelleyTxCertGenesisDeleg _ -> "Genesis"
+        ShelleyTxCertMir _ -> "Mir"
+  pure (classify True tag (property (conformsToSpec ans spec)))
+
+testConwayCert :: Gen Property
+testConwayCert = do
+  env <- genFromSpec @ConwayFn @(CertEnv Conway) certEnvSpec
+  dstate <- genFromSpec @ConwayFn @(CertState Conway) certStateSpec
+  let spec = conwayTxCertSpec env dstate
+  ans <- genFromSpec @ConwayFn spec
+  let tag = case ans of
+        (ConwayTxCertDeleg (ConwayRegCert _ _)) -> "Register"
+        (ConwayTxCertDeleg (ConwayUnRegCert _ _)) -> "UnRegister"
+        (ConwayTxCertDeleg (ConwayDelegCert _ _)) -> "Delegate"
+        (ConwayTxCertDeleg (ConwayRegDelegCert _ _ _)) -> "Register&Delegate"
+        (ConwayTxCertPool (RegPool _)) -> "RegPool"
+        (ConwayTxCertPool (RetirePool _ _)) -> "RetirePool"
+        (ConwayTxCertGov (ConwayRegDRep _ _ _)) -> "RegDRep"
+        (ConwayTxCertGov (ConwayUnRegDRep _ _)) -> "UnRegDRep"
+        (ConwayTxCertGov (ConwayUpdateDRep _ _)) -> "UpdateDRep"
+        (ConwayTxCertGov (ConwayAuthCommitteeHotKey _ _)) -> "AuthCommittee"
+        (ConwayTxCertGov (ConwayResignCommitteeColdKey _ _)) -> "ResignCommittee"
+  pure (classify True tag (conformsToSpec ans spec))