Ts additions prime spec cert steps

eras/shelley/test-suite/src/Test/Cardano/Ledger/Shelley/Generator/Utxo.hs

@@ -460,7 +460,7 @@ genNextDelta
                           vkeyPairs
                           (mkScriptWits @era msigPairs mempty)
                           (hashAnnotated txBody)
-                  pure
+                  pure $
                     delta
                       { extraWitnesses = extraWitnesses <> newWits
                       , extraInputs = extraInputs <> Set.fromList inputs

libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal

@@ -23,6 +23,7 @@ library
         Test.Cardano.Ledger.Conformance
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Core
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway
+        Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
 
     hs-source-dirs:   src
     other-modules:
@@ -35,7 +36,6 @@ library
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Certs
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Gov
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert
-        Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert

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

@@ -1,5 +1,6 @@
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (
   module X,
+  ConwayRatifyExecContext (..),
 ) where
 
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base as X (
@@ -11,7 +12,7 @@ import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base as X (
   nameGovAction,
  )
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert as X (nameTxCert)
-import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs as X ()
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs as X (nameCerts)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg as X (nameDelegCert)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov as X ()
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert as X (nameGovCert)

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

@@ -10,16 +10,21 @@
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
-module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs () where
+module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs (nameCerts) where
 
 import Cardano.Ledger.Conway
+import Cardano.Ledger.Conway.TxCert
+import Constrained
 import Data.Bifunctor (first)
 import qualified Data.List.NonEmpty as NE
+import qualified Data.Map.Strict as Map
+import Data.Sequence (Seq)
 import qualified Data.Text as T
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base
 import Test.Cardano.Ledger.Constrained.Conway
+import Test.Cardano.Ledger.Imp.Common hiding (context)
 
 instance
   IsConwayUniv fn =>
@@ -29,11 +34,45 @@ instance
 
   environmentSpec _ = certsEnvSpec
 
-  stateSpec _ _ = certStateSpec
+  stateSpec context _ =
+    constrained $ \x ->
+      match x $ \vstate pstate dstate ->
+        [ satisfies vstate vStateSpec
+        , satisfies pstate pStateSpec
+        , -- temporary workaround because Spec does some extra tests, that the implementation does not, in the bootstrap phase.
+          satisfies dstate (bootstrapDStateSpec (ccecWithdrawals context))
+        ]
 
-  signalSpec _ _ _ = txCertsSpec
+  signalSpec _ env state = txCertsSpec env state
 
   runAgdaRule env st sig =
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
       . computationResultToEither
       $ Agda.certsStep' env st sig
+  classOf = Just . nameCerts
+
+  testConformance ctx 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 snd (ccecWithdrawals ctx)))
+    (implResTest, agdaResTest) <- runConformance @"CERTS" @fn @Conway ctx env st sig
+    case (implResTest, agdaResTest) of
+      (Right haskell, Right spec) ->
+        checkConformance @"CERTS" @Conway @fn
+          ctx
+          env
+          st
+          sig
+          (Right (fixRewards specWithdrawalCredSet haskell))
+          (Right spec)
+        where
+          -- Zero out the rewards for credentials that are the key of some withdrawal
+          -- (found in the ctx) as this happens in the Spec, but not in the implementation.
+          fixRewards (Agda.MkHSSet creds) x =
+            x {Agda.dState' = (Agda.dState' x) {Agda.rewards' = zeroRewards (Agda.rewards' (Agda.dState' x))}}
+            where
+              zeroRewards (Agda.MkHSMap pairs) = Agda.MkHSMap (map (\(c, r) -> if elem c creds then (c, 0) else (c, r)) pairs)
+      _ -> checkConformance @"CERTS" @Conway @fn ctx env st sig implResTest agdaResTest
+
+nameCerts :: Seq (ConwayTxCert Conway) -> String
+nameCerts x = "Certs length " ++ show (length x)

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

@@ -20,6 +20,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
   runConformance,
   checkConformance,
   defaultTestConformance,
+  translateWithContext,
 ) where
 
 import Cardano.Ledger.BaseTypes (Inject (..), ShelleyBase)
@@ -463,3 +464,11 @@ inputsGenerateWithin timeout =
     genSig `generatesWithin` timeout
   where
     aName = show (typeRep $ Proxy @rule)
+
+-- | Translate a Haskell type 'a' whose translation context is 'ctx' into its Agda type, in the ImpTest monad.
+translateWithContext :: SpecTranslate ctx a => ctx -> a -> ImpTestM era (SpecRep a)
+translateWithContext ctx x = do
+  let
+    expectRight' (Right y) = pure y
+    expectRight' (Left e) = assertFailure (T.unpack e)
+  expectRight' . runSpecTransM ctx $ toSpecRep x

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

@@ -32,6 +32,7 @@ import Test.Cardano.Ledger.Generic.Proof
 
 -- \| This is where most of the ExecSpecRule instances are defined
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway (
+  nameCerts,
   nameDelegCert,
   nameEnact,
   nameEpoch,
@@ -76,7 +77,7 @@ minitraceEither witrule Proxy n0 = do
                 pure
                   ( Left
                       ( [ "\nSIGNAL = " ++ show (prettyA signal2)
-                        , "\nState = " ++ show (prettyA state)
+                        , "\nSTATE = " ++ show (prettyA state)
                         , "\nPredicateFailures"
                         ]
                           ++ map show (NE.toList ps)
@@ -163,6 +164,7 @@ spec = do
     prop "DELEG" (withMaxSuccess 50 (minitraceProp (DELEG Conway) (Proxy @ConwayFn) 50 nameDelegCert))
     prop "GOVCERT" (withMaxSuccess 50 (minitraceProp (GOVCERT Conway) (Proxy @ConwayFn) 50 nameGovCert))
     prop "CERT" (withMaxSuccess 50 (minitraceProp (CERT Conway) (Proxy @ConwayFn) 50 nameTxCert))
+    prop "CERTS" (withMaxSuccess 50 (minitraceProp (CERTS Conway) (Proxy @ConwayFn) 50 nameCerts))
     prop "RATIFY" (withMaxSuccess 50 (minitraceProp (RATIFY Conway) (Proxy @ConwayFn) 50 nameRatify))
     prop "ENACT" (withMaxSuccess 50 (minitraceProp (ENACT Conway) (Proxy @ConwayFn) 50 nameEnact))
     -- These properties do not have working 'signalSpec' Specifications yet.

libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Spec/Conway.hs

@@ -29,9 +29,10 @@ spec = do
       prop "DELEG" $ conformsToImpl @"DELEG" @ConwayFn @Conway
       prop "GOVCERT" $ conformsToImpl @"GOVCERT" @ConwayFn @Conway
       prop "POOL" $ conformsToImpl @"POOL" @ConwayFn @Conway
-      xprop "CERTS" $ conformsToImpl @"CERTS" @ConwayFn @Conway
       prop "CERT" $ conformsToImpl @"CERT" @ConwayFn @Conway
+      prop "CERTS" $ conformsToImpl @"CERTS" @ConwayFn @Conway
       prop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway
+
       xprop "UTXO" $ conformsToImpl @"UTXO" @ConwayFn @Conway
     describe "ImpTests" $ do
       RatifyImp.spec

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

@@ -25,8 +25,9 @@ certEnvSpec ::
   Specification fn (CertEnv (ConwayEra StandardCrypto))
 certEnvSpec =
   constrained $ \ce ->
-    match ce $ \_ pp _ _ _ ->
-      satisfies pp pparamsSpec
+    match ce $ \_slot pp _currEpoch _currCommittee _proposals ->
+      [ satisfies pp pparamsSpec
+      ]
 
 certStateSpec ::
   IsConwayUniv fn =>

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

@@ -1,25 +1,176 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE QuasiQuotes #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ViewPatterns #-}
 
 -- | Specs necessary to generate, environment, state, and signal
 -- for the CERTS rule
 module Test.Cardano.Ledger.Constrained.Conway.Certs where
 
-import Cardano.Ledger.Conway (ConwayEra)
+import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..), IsValid (..))
+import Cardano.Ledger.BaseTypes (Network (..))
+import Cardano.Ledger.CertState
+import Cardano.Ledger.Coin (Coin (..))
+import Cardano.Ledger.Conway (Conway)
 import Cardano.Ledger.Conway.Rules
 import Cardano.Ledger.Conway.TxCert
-import Cardano.Ledger.Crypto (StandardCrypto)
+import Cardano.Ledger.Core
+import Cardano.Ledger.Credential (Credential (..))
+import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..))
+import Cardano.Ledger.PoolParams (PoolParams (ppId))
+import Cardano.Ledger.UMap (dRepMap)
 import Constrained
-import Data.Sequence (Seq)
+import Constrained.Base (Pred (..))
+import Data.Default.Class
+import Data.Foldable (toList)
+import Data.Map.Strict (Map)
+import qualified Data.Map.Strict as Map
+import Data.Sequence (Seq, fromList)
+import qualified Data.Set as Set
+import Data.Word (Word64)
+import Test.Cardano.Ledger.Constrained.Conway.Cert (txCertSpec)
+import Test.Cardano.Ledger.Constrained.Conway.Deleg (someZeros)
 import Test.Cardano.Ledger.Constrained.Conway.Instances
 import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
+import Test.Cardano.Ledger.Generic.PrettyCore
+import Test.QuickCheck hiding (forAll)
+
+main :: IO ()
+main = do
+  context <- generate $ genFromSpec @ConwayFn (constrained $ \x -> sizeOf_ x ==. 3)
+  state <- generate $ genFromSpec @ConwayFn (bootstrapDStateSpec context)
+  putStrLn ("\n\nDRepDelegs\n" ++ show (prettyA (dRepMap (dsUnified state))))
+  putStrLn ("\n\nContext\n" ++ show (prettyA context))
+
+-- =======================================================
+
+-- The current spec is written to specify the phase when Voting goes into effect (the Post BootStrap phase)
+-- The implementation is written to implement the phase before Voting goes into effect (the BootStrap phase)
+-- This affects the Certs rule beacuse in the Post Bootstrap Phase, the spec tests that the (Credential 'Staking c)
+-- of every withdrawal, is delegated to some DRep, and that every Withdrawal is consistent with some Rewards entry.
+-- This is tested in the Spec, but it is not tested in implementation.
+-- A hardfork, sometime in the future will turn this test on.
+-- So to satisfy both we add this more refined DState spec, that make sure these post bootstrap tests are always True.
+-- The implementation does not test these, so the extra refinement has no effect here, the Spec will test them so refinement does matter there.
+-- Note that only the keyhash credentials need be delegated to a DRep.
+bootstrapDStateSpec ::
+  IsConwayUniv fn =>
+  CertsContext Conway ->
+  Specification fn (DState Conway)
+bootstrapDStateSpec withdrawals =
+  let isKey (ScriptHashObj _) = False
+      isKey (KeyHashObj _) = True
+      withdrawalPairs = Map.toList (Map.mapKeys snd (Map.map coinToWord64 withdrawals))
+      withdrawalKeys = Map.keysSet (Map.mapKeys snd withdrawals)
+   in constrained $ \ [var| dstate |] ->
+        match dstate $ \ [var| rewardMap |] _futureGenDelegs _genDelegs _rewards ->
+          [ assert $ sizeOf_ _futureGenDelegs ==. 0
+          , match _genDelegs $ \gd -> assert $ sizeOf_ gd ==. 0
+          , match _rewards $ \w x y z -> [sizeOf_ w ==. 0, sizeOf_ x ==. 0, y ==. lit mempty, z ==. lit mempty]
+          , match [var| rewardMap |] $ \ [var| rdMap |] [var| ptrMap |] [var| sPoolMap |] dRepDelegs ->
+              [ assertExplain (pure "dom sPoolMap is a subset of dom rdMap") $ dom_ sPoolMap `subset_` dom_ rdMap
+              , assertExplain (pure "dom ptrMap is empty") $ dom_ ptrMap ==. mempty
+              , assertExplain (pure "some rewards (not in withdrawals) are zero") $
+                  forAll rdMap $
+                    \ [var| keycoinpair |] -> match keycoinpair $ \cred [var| rdpair |] ->
+                      -- Apply this only to entries NOT IN the withdrawal set, since withdrawals already set the reward in the RDPair.
+                      whenTrue (not_ (member_ cred (lit withdrawalKeys))) (satisfies rdpair someZeros)
+              , forAll (lit (Set.filter isKey withdrawalKeys)) $ \cred -> assert $ member_ cred (dom_ dRepDelegs)
+              , forAll (lit withdrawalPairs) $ \ [var| pair |] ->
+                  match pair $ \ [var| cred |] [var| coin |] ->
+                    [ assert $ member_ cred (dom_ rdMap)
+                    , (caseOn (lookup_ cred rdMap))
+                        -- Nothing
+                        ( branch $ \_ -> FalsePred (pure ("credential " ++ show cred ++ " not in rdMap, bootstrapCertStateSpec"))
+                        )
+                        -- Just
+                        ( branch $ \ [var| rdpair |] ->
+                            match rdpair $ \rew _deposit -> assert $ rew ==. coin
+                        )
+                    ]
+              ]
+          ]
+
+coinToWord64 :: Coin -> Word64
+coinToWord64 (Coin n) = fromIntegral n
+
+type CertsContext era = (Map (Network, Credential 'Staking (EraCrypto era)) Coin)
+
+txZero :: AlonzoTx Conway
+txZero = AlonzoTx mkBasicTxBody mempty (IsValid True) def
 
 certsEnvSpec ::
   IsConwayUniv fn =>
-  Specification fn (CertsEnv (ConwayEra StandardCrypto))
-certsEnvSpec = constrained $ \env ->
-  match env $ \_ pp _ _ _ _ ->
-    satisfies pp pparamsSpec
+  Specification fn (CertsEnv Conway)
+certsEnvSpec = constrained $ \ce ->
+  match ce $ \tx pp _slot _currepoch _currcommittee commproposals ->
+    [ satisfies pp pparamsSpec
+    , assert $ tx ==. lit txZero
+    , genHint 3 commproposals
+    ]
+
+-- | Project a CertEnv out of a CertsEnv (i.e drop the Tx)
+projectEnv :: CertsEnv Conway -> CertEnv Conway
+projectEnv x =
+  CertEnv
+    { cePParams = certsPParams x
+    , ceSlotNo = certsSlotNo x
+    , ceCurrentEpoch = certsCurrentEpoch x
+    , ceCurrentCommittee = certsCurrentCommittee x
+    , ceCommitteeProposals = certsCommitteeProposals x
+    }
+
+-- | Specify a pair of List and Seq, where they have essentially the same elements
+--   EXCEPT, the Seq has duplicate keys filtered out.
+listSeqPairSpec ::
+  IsConwayUniv fn =>
+  CertsEnv Conway ->
+  CertState Conway ->
+  Specification fn ([ConwayTxCert Conway], Seq (ConwayTxCert Conway))
+listSeqPairSpec env state =
+  constrained' $ \list seqs ->
+    [ assert $ sizeOf_ list <=. 5
+    , forAll list $ \x -> satisfies x (txCertSpec (projectEnv env) state)
+    , reify list (fromList . noSameKeys) (\x -> seqs ==. x)
+    ]
 
 txCertsSpec ::
-  Specification fn (Seq (ConwayTxCert (ConwayEra StandardCrypto)))
-txCertsSpec = TrueSpec
+  IsConwayUniv fn =>
+  CertsEnv Conway ->
+  CertState Conway ->
+  Specification fn (Seq (ConwayTxCert Conway))
+txCertsSpec env state =
+  constrained $ \seqs ->
+    exists
+      (\eval -> pure $ toList (eval seqs))
+      (\list -> satisfies (pair_ list seqs) (listSeqPairSpec env state))
+
+-- | 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)
+  deriving (Eq, Show, Ord)
+
+-- | Compute the aggregate key type of a Certificater
+txCertKey :: ConwayTxCert era -> CertKey (EraCrypto era)
+txCertKey (ConwayTxCertDeleg (ConwayRegCert x _)) = StakeKey x
+txCertKey (ConwayTxCertDeleg (ConwayUnRegCert x _)) = StakeKey x
+txCertKey (ConwayTxCertDeleg (ConwayDelegCert x _)) = StakeKey x
+txCertKey (ConwayTxCertDeleg (ConwayRegDelegCert x _ _)) = StakeKey x
+txCertKey (ConwayTxCertPool (RegPool x)) = PoolKey (ppId x)
+txCertKey (ConwayTxCertPool (RetirePool x _)) = PoolKey x
+txCertKey (ConwayTxCertGov (ConwayRegDRep x _ _)) = DRepKey x
+txCertKey (ConwayTxCertGov (ConwayUnRegDRep x _)) = DRepKey x
+txCertKey (ConwayTxCertGov (ConwayUpdateDRep x _)) = DRepKey x
+txCertKey (ConwayTxCertGov (ConwayAuthCommitteeHotKey x _)) = ColdKey x
+txCertKey (ConwayTxCertGov (ConwayResignCommitteeColdKey x _)) = ColdKey x
+
+noSameKeys :: [ConwayTxCert era] -> [ConwayTxCert era]
+noSameKeys [] = []
+noSameKeys (x : xs) = x : noSameKeys (filter (\y -> txCertKey x /= txCertKey y) xs)