Tools for constrained generation of types that need witnessing

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

@@ -21,6 +21,7 @@
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
   ConwayCertExecContext (..),
+  conwayCertExecContextSpec,
   ConwayRatifyExecContext (..),
   nameEpoch,
   nameEnact,
@@ -110,6 +111,7 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
   signatureFromInteger,
  )
 import Test.Cardano.Ledger.Constrained.Conway (
+  delegateeSpec,
   newEpochStateSpec,
  )
 import Test.Cardano.Ledger.Constrained.Conway.Epoch
@@ -123,18 +125,50 @@ import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams (
 import Cardano.Crypto.Hash (ByteString, Hash)
 import Cardano.Ledger.Crypto (DSIGN, HASH)
 import Cardano.Ledger.Keys (KeyRole (..), VKey (..))
+import Test.Cardano.Ledger.Constrained.Conway.Utxo (witnessDepositPurpose)
+import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse (WitUniv (..), witness)
 import Test.Cardano.Ledger.Conway.Arbitrary ()
-import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var)
-
-data ConwayCertExecContext era = ConwayCertExecContext
-  { ccecWithdrawals :: !(Map RewardAccount Coin)
-  , ccecDeposits :: !(Map DepositPurpose Coin)
-  , ccecVotes :: !(VotingProcedures era)
-  , ccecDelegatees :: !(Set (Credential 'DRepRole))
-  }
+import Test.Cardano.Ledger.Generic.Proof (Reflect)
+import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var, witness)
+
+-- ================================================================
+
+data ConwayCertExecContext era
+  = -- | The UMap of the DState has a field with type: Map (Credential 'Staking) DRep
+    --   The VState field vsDReps has type: Map (Credential DRepRole) DRepState
+    --   The DRepState field drepDelegs has type: Set (Credential Staking)
+    --   Every (Credential 'DRepRole c) corresponds to a unique (DRep)
+    -- the ccecDelegatees field helps maintain that correspondance, It is used in
+    -- vstateSpec and bootstrapDStateSpec. Also see
+    -- getDelegatees :: DState era -> Map (Credential 'DRepRole) (Set (Credential 'Staking))
+    -- in Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs, which defines the exact correspondance.  }
+    ConwayCertExecContext
+    { ccecWithdrawals :: !(Map RewardAccount Coin)
+    , ccecDeposits :: !(Map DepositPurpose Coin)
+    , ccecVotes :: !(VotingProcedures era)
+    , ccecDelegatees :: !(Set (Credential 'DRepRole))
+    }
   deriving (Generic, Eq, Show)
 
-instance Era era => Arbitrary (ConwayCertExecContext era) where
+instance HasSimpleRep (ConwayCertExecContext era)
+instance (IsConwayUniv fn, Era era) => HasSpec fn (ConwayCertExecContext era)
+
+-- No particular constraints, other than witnessing
+conwayCertExecContextSpec ::
+  forall fn era.
+  (Reflect era, IsConwayUniv fn) =>
+  WitUniv era -> Integer -> Specification fn (ConwayCertExecContext era)
+conwayCertExecContextSpec univ wdrlsize = constrained $ \ [var|ccec|] ->
+  match ccec $ \ [var|withdrawals|] [var|deposits|] _ [var|delegatees|] ->
+    [ assert $
+        [ witness univ (dom_ withdrawals)
+        , assert $ sizeOf_ (dom_ withdrawals) <=. (lit wdrlsize)
+        ]
+    , forAll (dom_ deposits) $ \dp -> satisfies dp (witnessDepositPurpose univ)
+    , satisfies delegatees (delegateeSpec @fn @era univ)
+    ]
+
+instance Reflect era => Arbitrary (ConwayCertExecContext era) where
   arbitrary =
     ConwayCertExecContext
       <$> arbitrary
@@ -152,7 +186,7 @@ instance Era era => EncCBOR (ConwayCertExecContext era) where
             !> To ccecVotes
             !> To ccecDelegatees
 
-instance Era era => DecCBOR (ConwayCertExecContext era) where
+instance Reflect era => DecCBOR (ConwayCertExecContext era) where
   decCBOR =
     decode $
       RecD ConwayCertExecContext

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

@@ -2,39 +2,50 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert (nameTxCert) where
 
-import Cardano.Ledger.Address (RewardAccount)
-import Cardano.Ledger.BaseTypes (Inject)
-import Cardano.Ledger.Coin (Coin)
 import Cardano.Ledger.Conway
 import Cardano.Ledger.Conway.TxCert (ConwayTxCert (..))
-import Constrained (lit)
-import Data.Map.Strict (Map)
+import Constrained
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert (nameGovCert)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool (namePoolCert)
 import Test.Cardano.Ledger.Constrained.Conway
+import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
 
 instance
-  ( IsConwayUniv fn
-  , Inject (ConwayCertExecContext ConwayEra) (Map RewardAccount Coin)
-  ) =>
+  IsConwayUniv fn =>
   ExecSpecRule fn "CERT" ConwayEra
   where
-  type ExecContext fn "CERT" ConwayEra = ConwayCertExecContext ConwayEra
-  environmentSpec _ = certEnvSpec
-  stateSpec ctx _ = certStateSpec (lit $ ccecDelegatees ctx)
-  signalSpec _ = txCertSpec
-  runAgdaRule env st sig = unComputationResult $ Agda.certStep env st sig
+  type ExecContext fn "CERT" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
+
+  genExecContext = do
+    univ <- genWitUniv @ConwayEra 300
+    ccec <- genFromSpec @ConwayFn (conwayCertExecContextSpec univ 5)
+    pure (univ, ccec)
+
+  environmentSpec (univ, _) = certEnvSpec @fn @ConwayEra univ
+
+  stateSpec (univ, ccec) _ =
+    certStateSpec @fn @ConwayEra univ (ccecDelegatees ccec) (ccecWithdrawals ccec)
+
+  signalSpec (univ, _) env state = conwayTxCertSpec @fn @ConwayEra univ env state
+
+  runAgdaRule env st sig =
+    unComputationResult $
+      Agda.certStep env st sig
 
   classOf = Just . nameTxCert
 

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

@@ -21,35 +21,42 @@ import qualified Data.Set as Set
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert ()
 import Test.Cardano.Ledger.Constrained.Conway
+import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
 import Test.Cardano.Ledger.Imp.Common hiding (context)
 
 instance
   IsConwayUniv fn =>
   ExecSpecRule fn "CERTS" ConwayEra
   where
-  type ExecContext fn "CERTS" ConwayEra = ConwayCertExecContext ConwayEra
+  type ExecContext fn "CERTS" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
+
+  genExecContext = do
+    univ <- genWitUniv @ConwayEra 300
+    ccec <- genFromSpec @fn (conwayCertExecContextSpec univ 5)
+    pure (univ, ccec)
 
   environmentSpec _ = certsEnvSpec
 
-  stateSpec context _ =
+  stateSpec (univ, context) _ =
     constrained $ \x ->
       match x $ \vstate pstate dstate ->
-        [ satisfies vstate (vStateSpec (lit $ ccecDelegatees context))
-        , satisfies pstate pStateSpec
+        [ satisfies vstate (vStateSpec @_ @ConwayEra univ (ccecDelegatees context))
+        , satisfies pstate (pStateSpec @_ @ConwayEra univ)
         , -- temporary workaround because Spec does some extra tests, that the implementation does not, in the bootstrap phase.
-          satisfies dstate (bootstrapDStateSpec (ccecDelegatees context) (ccecWithdrawals context))
+          satisfies dstate (bootstrapDStateSpec univ (ccecDelegatees context) (ccecWithdrawals context))
         ]
 
-  signalSpec _ = txCertsSpec
+  signalSpec (univ, _) env state = txCertsSpec @ConwayEra @fn univ env state
 
   runAgdaRule env st sig = unComputationResult $ Agda.certsStep env st sig
   classOf = Just . nameCerts
 
-  testConformance ctx env st sig = property $ do
+  testConformance ctx@(_, ccec) env st sig = property $ do
     -- The results of runConformance are Agda types, the `ctx` is a Haskell type, we extract and translate the Withdrawal keys.
     specWithdrawalCredSet <-
-      translateWithContext () (Map.keysSet (Map.mapKeys raCredential (ccecWithdrawals ctx)))
+      translateWithContext () (Map.keysSet (Map.mapKeys raCredential (ccecWithdrawals ccec)))
     (implResTest, agdaResTest, _) <- runConformance @"CERTS" @fn @ConwayEra ctx env st sig
     case (implResTest, agdaResTest) of
       (Right haskell, Right spec) ->

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

@@ -2,33 +2,53 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert) where
 
+import Cardano.Ledger.BaseTypes (Inject (..))
 import Cardano.Ledger.Conway
 import Cardano.Ledger.Conway.TxCert (ConwayDelegCert (..))
 import Cardano.Ledger.Credential (Credential)
 import Cardano.Ledger.Keys (KeyRole (..))
-import Constrained (lit)
-import Data.Bifunctor (Bifunctor (..))
+import Constrained
+import Data.Bifunctor (second)
 import Data.Set (Set)
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
+  ConwayCertExecContext (..),
+  conwayCertExecContextSpec,
+ )
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core ()
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert ()
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()
 import Test.Cardano.Ledger.Constrained.Conway
+import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
+
+instance
+  Inject
+    (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
+    (Set (Credential 'DRepRole))
+  where
+  inject (_, x) = ccecDelegatees x
 
 instance IsConwayUniv fn => ExecSpecRule fn "DELEG" ConwayEra where
-  type ExecContext fn "DELEG" ConwayEra = Set (Credential 'DRepRole)
+  type ExecContext fn "DELEG" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
+
+  genExecContext = do
+    univ <- genWitUniv @ConwayEra 300
+    ccec <- genFromSpec @ConwayFn (conwayCertExecContextSpec univ 5)
+    pure (univ, ccec)
 
   environmentSpec _ = delegEnvSpec
 
-  stateSpec ctx _ = certStateSpec (lit ctx)
+  stateSpec (univ, ccec) _env =
+    certStateSpec @_ @ConwayEra univ (ccecDelegatees ccec) (ccecWithdrawals ccec)
 
   signalSpec _ = conwayDelegCertSpec
 

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

@@ -3,37 +3,54 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert (nameGovCert) where
 
-import Cardano.Ledger.BaseTypes (Inject)
+import Cardano.Ledger.Address (RewardAccount)
+import Cardano.Ledger.BaseTypes (Inject (..))
 import Cardano.Ledger.Coin (Coin)
 import Cardano.Ledger.Conway
+import Cardano.Ledger.Conway.Governance (VotingProcedures)
 import Cardano.Ledger.Conway.TxCert
-import Constrained (lit)
+import Constrained
 import Data.Bifunctor (Bifunctor (..))
 import Data.Map.Strict (Map)
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance
-import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
+  ConwayCertExecContext (..),
+  conwayCertExecContextSpec,
+ )
 import Test.Cardano.Ledger.Constrained.Conway
+import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
+
+instance Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (Map RewardAccount Coin) where
+  inject (_, x) = ccecWithdrawals x
+
+instance Inject (WitUniv ConwayEra, ConwayCertExecContext ConwayEra) (VotingProcedures ConwayEra) where
+  inject (_, x) = ccecVotes x
 
 instance
-  ( IsConwayUniv fn
-  , Inject (ConwayCertExecContext ConwayEra) (Map DepositPurpose Coin)
-  ) =>
+  IsConwayUniv fn =>
   ExecSpecRule fn "GOVCERT" ConwayEra
   where
-  type ExecContext fn "GOVCERT" ConwayEra = ConwayCertExecContext ConwayEra
+  type ExecContext fn "GOVCERT" ConwayEra = (WitUniv ConwayEra, ConwayCertExecContext ConwayEra)
+
+  genExecContext = do
+    univ <- genWitUniv @ConwayEra 300
+    ccec <- genFromSpec @ConwayFn (conwayCertExecContextSpec univ 5)
+    pure (univ, ccec)
 
-  environmentSpec _ctx = govCertEnvSpec
+  environmentSpec (univ, _) = govCertEnvSpec univ
 
-  stateSpec ctx _env = certStateSpec (lit $ ccecDelegatees ctx)
+  stateSpec (univ, ccec) _env =
+    certStateSpec @fn @ConwayEra univ (ccecDelegatees ccec) (ccecWithdrawals ccec)
 
-  signalSpec _ctx = govCertSpec
+  signalSpec (univ, _) = govCertSpec univ
 
   classOf = Just . nameGovCert
 

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

@@ -2,6 +2,9 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
@@ -15,13 +18,15 @@ import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core ()
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool ()
 import Test.Cardano.Ledger.Constrained.Conway
+import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
 
 instance IsConwayUniv fn => ExecSpecRule fn "POOL" ConwayEra where
-  environmentSpec _ = poolEnvSpec
+  type ExecContext fn "POOL" ConwayEra = WitUniv ConwayEra
+  environmentSpec ctx = poolEnvSpec ctx
 
-  stateSpec _ _ = pStateSpec
+  stateSpec ctx _ = pStateSpec ctx
 
-  signalSpec _ = poolCertSpec
+  signalSpec wituniv env st = poolCertSpec @fn @ConwayEra wituniv env st
 
   runAgdaRule env st sig = unComputationResult $ Agda.poolStep env st sig
 

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

@@ -11,6 +11,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
   ExecSpecRule (..),

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs

@@ -149,8 +149,8 @@ instance NFData LEnv
 instance ToExpr a => ToExpr (HSSet a)
 
 instance ToExpr Credential where
-  toExpr (KeyHashObj h) = App "KeyHashObj" [agdaHashToExpr standardHashSize h]
-  toExpr (ScriptObj h) = App "ScriptObj" [agdaHashToExpr standardHashSize h]
+  toExpr (KeyHashObj h) = App "KeyHashObj" [agdaHashToExpr 28 h, toExpr h]
+  toExpr (ScriptObj h) = App "ScriptObj" [agdaHashToExpr 28 h, toExpr h]
 
 instance (ToExpr k, ToExpr v) => ToExpr (HSMap k v)
 

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

@@ -1211,9 +1211,6 @@ committeeCredentialToStrictMaybe ::
 committeeCredentialToStrictMaybe (CommitteeHotCredential c) = SJust c
 committeeCredentialToStrictMaybe (CommitteeMemberResigned _) = SNothing
 
-instance HasSimpleRep DepositPurpose
-instance IsConwayUniv fn => HasSpec fn DepositPurpose
-
 instance SpecTranslate ctx DepositPurpose where
   type SpecRep DepositPurpose = Agda.DepositPurpose
   toSpecRep (CredentialDeposit cred) =