Trying to get the tests to pass

Reworked some messages when things fail.
Removed some unused imports that were not necessary.
Changed Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs, by
  changing conwayCertStateSpec to pass one component of PState through reify to DState
  and then pass one component of DState though reify to VState.
  This replaces the use of two exists.
Made some small chages to MiniTrace.
Added Witnessing the rng of a map that was ConwayAccountState.
Added some Winessed instances that deal with AccountState type family and its instances.

Author: TimSheard

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/ImpTest.hs

@@ -149,8 +149,8 @@ import Cardano.Ledger.BaseTypes (
   textToUrl,
  )
 import Cardano.Ledger.Coin (Coin (..))
-import Cardano.Ledger.Conway (ConwayEra, hardforkConwayBootstrapPhase)
 import Cardano.Ledger.Compactible (fromCompact)
+import Cardano.Ledger.Conway (ConwayEra, hardforkConwayBootstrapPhase)
 import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Genesis (ConwayGenesis (..))
 import Cardano.Ledger.Conway.Governance

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

@@ -24,7 +24,7 @@ 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 hiding (conwayCertStateSpec)
-import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs
+import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (conwayCertStateSpec)
 import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
 import Test.Cardano.Ledger.Imp.Common hiding (context)
 
@@ -38,17 +38,9 @@ instance ExecSpecRule "CERTS" ConwayEra where
 
   environmentSpec _ = certsEnvSpec
 
-  stateSpec (univ, context) _ =
+  stateSpec (univ, _context) _ =
     conwayCertStateSpec univ (lit (EpochNo 100))
 
-  -- constrained $ \x ->
-  --   match x $ \vstate pstate dstate ->
-  --     [ 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 (conwayDStateSpec univ (ccecDelegatees context) (ccecWithdrawals context))
-  --     ]
-
   signalSpec (univ, _) env state = txCertsSpec @ConwayEra univ env state
 
   runAgdaRule env st sig = unComputationResult $ Agda.certsStep env st sig

libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/ExecSpecRule/MiniTrace.hs

@@ -22,14 +22,16 @@ import Cardano.Ledger.Conway.Governance (
 import Cardano.Ledger.Conway.Rules (GovSignal (..))
 import Cardano.Ledger.Core
 import Constrained.API
+-- \| This is where most of the ExecSpecRule instances are defined
+
+import Constrained.PrettyUtils (showType)
 import Control.State.Transition.Extended (STS (..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Map.Strict as Map
 import qualified Data.OSet.Strict as OSet
 import Data.Proxy
 import Test.Cardano.Ledger.Common
 import Test.Cardano.Ledger.Conformance
--- \| This is where most of the ExecSpecRule instances are defined
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (
   nameCerts,
   nameDelegCert,
@@ -56,15 +58,17 @@ minitraceEither ::
   Int ->
   Gen (Either [String] [Signal (EraRule s e)])
 minitraceEither witrule n0 = do
-  ctxt <- genExecContext @s @e
-  env <- genFromSpec @(ExecEnvironment s e) (environmentSpec @s @e ctxt)
+  !ctxt <- genExecContext @s @e
+
+  !env <- genFromSpec @(ExecEnvironment s e) (environmentSpec @s @e ctxt)
   let env2 :: Environment (EraRule s e)
       env2 = inject env
   !state0 <- genFromSpec @(ExecState s e) (stateSpec @s @e ctxt env)
+
   let go :: State (EraRule s e) -> Int -> Gen (Either [String] [Signal (EraRule s e)])
       go _ 0 = pure (Right [])
       go state n = do
-        signal <- genFromSpec @(ExecSignal s e) (signalSpec @s @e ctxt env state)
+        !signal <- genFromSpec @(ExecSignal s e) (signalSpec @s @e ctxt env state)
         let signal2 :: Signal (EraRule s e)
             signal2 = inject signal
         goSTS @s @e @(Gen (Either [String] [Signal (EraRule s e)]))
@@ -169,12 +173,14 @@ spec = do
     prop
       "CERT"
       (withMaxSuccess 50 (minitraceProp (CERT Conway) 50 nameTxCert))
+
     prop
       "CERTS"
       ( withMaxSuccess
           50
           (minitraceProp (CERTS Conway) 50 nameCerts)
       )
+
     prop
       "RATIFY"
       (withMaxSuccess 50 (minitraceProp (RATIFY Conway) 50 nameRatify))

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

@@ -11,26 +11,26 @@
 -- for the CERTS rule
 module Test.Cardano.Ledger.Constrained.Conway.Certs where
 
-import Cardano.Ledger.Address (RewardAccount (..))
-import Cardano.Ledger.Coin (Coin (..))
+-- import Cardano.Ledger.Address (RewardAccount (..))
+-- import Cardano.Ledger.Coin (Coin (..))
 import Cardano.Ledger.Conway.Rules
 import Cardano.Ledger.Core
-import Cardano.Ledger.Credential (Credential (..), credKeyHash, credScriptHash)
+-- import Cardano.Ledger.Credential (Credential (..), credKeyHash, credScriptHash)
 import Cardano.Ledger.State
 import Constrained.API
 import Data.Foldable (toList)
-import Data.Map.Strict (Map)
+-- import Data.Map.Strict (Map)
 import Data.Sequence (Seq, fromList)
 import Data.Set (Set)
 import qualified Data.Set as Set
 import Test.Cardano.Ledger.Constrained.Conway.Cert
-import Test.Cardano.Ledger.Constrained.Conway.Deleg (
-  hasGenDelegs,
-  keyHashWdrl,
- )
+-- import Test.Cardano.Ledger.Constrained.Conway.Deleg (
+--  hasGenDelegs,
+--  keyHashWdrl,
+--  )
 import Test.Cardano.Ledger.Constrained.Conway.Instances
 import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
-import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec (EraSpecTxOut (..))
+-- import Test.Cardano.Ledger.Constrained.Conway.ParametricSpec (EraSpecTxOut (..))
 import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse
 
 -- =======================================================

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

@@ -18,7 +18,7 @@ import Cardano.Ledger.Address
 import Cardano.Ledger.Allegra (AllegraEra)
 import Cardano.Ledger.Alonzo (AlonzoEra)
 import Cardano.Ledger.Babbage (BabbageEra)
-import Cardano.Ledger.BaseTypes (StrictMaybe (..), maybeToStrictMaybe)
+import Cardano.Ledger.BaseTypes (StrictMaybe (..))
 import Cardano.Ledger.Coin
 import Cardano.Ledger.Compactible (fromCompact)
 import Cardano.Ledger.Conway (ConwayEra)
@@ -28,6 +28,7 @@ import Cardano.Ledger.Conway.TxCert
 import Cardano.Ledger.Core
 import Cardano.Ledger.Credential
 import Cardano.Ledger.Mary (MaryEra)
+import Cardano.Ledger.PoolParams (PoolParams (..))
 import Cardano.Ledger.Shelley (ShelleyEra)
 import Cardano.Ledger.Shelley.TxCert
 import Constrained.API
@@ -62,6 +63,7 @@ accountBalanceSpec balance =
         (3, constrained (const True))
     )
 
+{-
 stakePoolDelegationPred ::
   Map (KeyHash 'StakePool) a ->
   Term (StrictMaybe (KeyHash 'StakePool)) ->
@@ -81,6 +83,8 @@ dRepDelegationPred dReps dRepDelegation =
       (branch (const True))
       (branch (dRepMembershipPred dReps))
 
+-}
+
 dRepMembershipPred :: Map (Credential 'DRepRole) a -> Term DRep -> Pred
 dRepMembershipPred dRepsMap dRep =
   assert $
@@ -90,8 +94,19 @@ dRepMembershipPred dRepsMap dRep =
       (branchW 1 $ const True)
       (branchW 1 $ const True)
   where
+    dRepsSet :: Ord a => (Credential 'DRepRole -> Maybe a) -> Set a
     dRepsSet f = Set.fromList [k' | k <- Map.keys dRepsMap, Just k' <- [f k]]
 
+-- | The DState needs a witnessed set of delegations to be usefull. Use this Spec to obtain a random one
+witnessedKeyHashPoolParamMapSpec ::
+  Era era => WitUniv era -> Specification (Map (KeyHash StakePool) PoolParams)
+witnessedKeyHashPoolParamMapSpec univ =
+  ( constrained $ \keyPoolParamMap ->
+      [witness univ (dom_ keyPoolParamMap), witness univ (rng_ keyPoolParamMap)]
+  )
+
+{-  I don't think these are necessary
+
 shelleyAccountStatePred ::
   Era era =>
   Map (KeyHash 'StakePool) a ->
@@ -175,13 +190,45 @@ conwayAccountsSpec ::
 conwayAccountsSpec univ stakePoolDelegations dRepDelegations =
   constrained $ \ [var|conwayAccountState|] ->
     match conwayAccountState $ \ [var|conwayAccountsMap|] ->
-      [ witness univ (dom_ conwayAccountsMap)
+      [ witness univ conwayAccountsMap
       , forAll conwayAccountsMap $ \ [var|accountPair|] ->
           match accountPair $ \ [var|cred|] [var|accountState|] ->
             reify (lookup_ cred stakePoolDelegations) maybeToStrictMaybe $ \stakePoolDelegationStrict ->
               reify (lookup_ cred dRepDelegations) maybeToStrictMaybe $ \dRepRepDelegationStrict ->
                 conwayAccountStatePred'' stakePoolDelegationStrict dRepRepDelegationStrict accountState
       ]
+-}
+
+conwayAccountsSpec ::
+  Era era =>
+  WitUniv era ->
+  Term (Map (KeyHash 'StakePool) PoolParams) ->
+  Specification (ConwayAccounts era)
+conwayAccountsSpec univ poolreg = constrained $ \ [var|conwayAccounts|] ->
+  match conwayAccounts $ \ [var|accountmap|] ->
+    [ witness univ (dom_ accountmap)
+    , forAll accountmap $ \ [var|pair|] ->
+        match pair $ \ [var|stakecred|] [var|accountstate|] ->
+          [ witness univ stakecred
+          , witness univ accountstate
+          , match accountstate $ \ [var|_rewardbal|] [var|_depositbal|] [var|mStakeDelegKeyhash|] [var|mDRep|] ->
+              [ ( caseOn
+                    (mStakeDelegKeyhash :: Term (StrictMaybe (KeyHash 'StakePool)))
+                    (branchW 1 $ \_ -> True)
+                    (branchW 3 $ \ [var|stakekeyhash|] -> mapMember_ stakekeyhash poolreg)
+                )
+              , (caseOn mDRep) -- This case only adds frequency info, the (witness univ accountstate) ensures witnessing
+                  (branchW 1 $ \_ -> True)
+                  ( branchW 3 $ \(drep :: Term DRep) ->
+                      (caseOn drep)
+                        (branchW 3 $ \_keyhash -> True)
+                        (branchW 3 $ \_scripthash -> True)
+                        (branchW 1 $ \_abstain -> True)
+                        (branchW 1 $ \_noconfidence -> True)
+                  )
+              ]
+          ]
+    ]
 
 stakePoolDelegationsSpec ::
   Era era =>
@@ -206,19 +253,6 @@ dRepDelegationsSpec univ =
           (branchW 1 $ const True)
     ]
 
-conwayAccountsSpec' ::
-  Era era =>
-  WitUniv era ->
-  Map (KeyHash 'StakePool) a ->
-  Map (Credential 'DRepRole) b ->
-  Specification (ConwayAccounts era)
-conwayAccountsSpec' univ stakePools dReps =
-  constrained $ \ [var|conwayAccountState|] ->
-    match conwayAccountState $ \ [var|conwayAccountsMap|] ->
-      [ witness univ (dom_ conwayAccountsMap)
-      , forAll (rng_ conwayAccountsMap) (conwayAccountStatePred stakePools dReps)
-      ]
-
 dStateSpec ::
   (Era era, HasSpec (Accounts era), IsNormalType (Accounts era)) =>
   WitUniv era ->

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

@@ -39,10 +39,10 @@ vStateSpec ::
   Set (Credential 'DRepRole) ->
   Specification (VState era)
 vStateSpec univ delegatees = constrained $ \ [var|vstate|] ->
-  match vstate $ \ [var|dreps|] [var|committeestate|] [var|_numdormant|] ->
+  match vstate $ \ [var|dreps2|] [var|committeestate|] [var|_numdormant|] ->
     [ match committeestate $ \ [var|committeemap|] -> witness univ (dom_ committeemap)
-    , assert $ dom_ dreps ==. lit delegatees -- TODO, there are missing constraints about the (rng_ dreps)
-    , forAll dreps $ \ [var|pair|] ->
+    , assert $ dom_ dreps2 ==. lit delegatees -- TODO, there are missing constraints about the (rng_ dreps)
+    , forAll dreps2 $ \ [var|pair|] ->
         match pair $ \ [var|drep|] [var|drepstate|] ->
           [ dependsOn drepstate drep
           , witness univ drep