diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/NecessaryAndSufficient.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/NecessaryAndSufficient.hs index a6b56af18ea..6552d45a1cc 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/NecessaryAndSufficient.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/NecessaryAndSufficient.hs @@ -6,132 +6,43 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} module Test.Cardano.Ledger.Constrained.Conway.NecessaryAndSufficient where --- import Cardano.Crypto.Hash hiding (Blake2b_224) --- import Cardano.Crypto.Hashing (AbstractHash, abstractHashFromBytes) --- import Cardano.Ledger.Address --- import Cardano.Ledger.Allegra.Scripts --- import Cardano.Ledger.Alonzo.PParams --- import Cardano.Ledger.Alonzo.Scripts (AlonzoScript (..)) --- import Cardano.Ledger.Alonzo.Tx --- import Cardano.Ledger.Alonzo.TxAuxData (AlonzoTxAuxData (..), AuxiliaryDataHash) --- import Cardano.Ledger.Alonzo.TxOut --- import Cardano.Ledger.Alonzo.TxWits --- import Cardano.Ledger.Babbage.TxBody (BabbageTxOut (..)) +import qualified Cardano.Crypto.Hash.Class as Hash import Cardano.Ledger.BaseTypes hiding (inject) - --- import Cardano.Ledger.Binary (Sized (..)) import Cardano.Ledger.CertState import Cardano.Ledger.Coin - --- import Cardano.Ledger.Compactible import Cardano.Ledger.Conway (Conway, ConwayEra) import Cardano.Ledger.Conway.Core - --- import Cardano.Ledger.Conway.Governance --- import Cardano.Ledger.Conway.PParams import Cardano.Ledger.Conway.Rules import Cardano.Ledger.Conway.Scripts () - --- import Cardano.Ledger.Conway.TxBody import Cardano.Ledger.Conway.TxCert import Cardano.Ledger.Credential import Cardano.Ledger.Crypto (Crypto, HASH, StandardCrypto) - --- import Cardano.Ledger.EpochBoundary --- import Cardano.Ledger.HKD -import Cardano.Ledger.Keys ( - -- BootstrapWitness, - -- GenDelegPair (..), - -- GenDelegs (..), - KeyHash, - KeyRole (..), - -- WitVKey, - ) - --- import Cardano.Ledger.Mary.Value (AssetName (..), MaryValue (..), MultiAsset (..), PolicyID (..)) --- import Cardano.Ledger.MemoBytes --- import Cardano.Ledger.Plutus.CostModels --- import Cardano.Ledger.Plutus.Data --- import Cardano.Ledger.Plutus.ExUnits --- import Cardano.Ledger.Plutus.Language --- import Cardano.Ledger.PoolDistr +import Cardano.Ledger.Keys (KeyHash, KeyRole (..)) import Cardano.Ledger.PoolParams - --- import Cardano.Ledger.SafeHash --- import Cardano.Ledger.Shelley.LedgerState hiding (ptrMap) --- import Cardano.Ledger.Shelley.PoolRank import Cardano.Ledger.Shelley.Rules - --- import Cardano.Ledger.Shelley.TxAuxData (Metadatum) --- import Cardano.Ledger.TxIn (TxId (..), TxIn (..)) import Cardano.Ledger.UMap - --- import Cardano.Ledger.UTxO --- import Cardano.Ledger.Val (Val) import Constrained hiding (Value) - --- import qualified Constrained as C import Constrained.Base - --- import Constrained.Spec.Map --- import Constrained.Univ --- import Control.Monad.Trans.Fail.String --- import Crypto.Hash (Blake2b_224) --- import qualified Data.ByteString as BS --- import Data.ByteString.Short (ShortByteString) --- import qualified Data.ByteString.Short as SBS --- import Data.Coerce +import Control.State.Transition.Extended (BaseM, STS (Environment, Signal)) import Data.Default.Class (Default (def)) - --- import Data.Foldable --- import Data.Int --- import Data.Kind import Data.Map (Map) import qualified Data.Map.Strict as Map - --- import Data.Maybe --- import qualified Data.OMap.Strict as OMap --- import qualified Data.OSet.Strict as SOS --- import Data.Sequence (Seq) --- import qualified Data.Sequence as Seq --- import Data.Sequence.Strict (StrictSeq) --- import qualified Data.Sequence.Strict as StrictSeq --- import Data.Set (Set) --- import qualified Data.Set as Set --- import Data.Text (Text) --- import Data.Tree --- import Data.Typeable --- import Data.VMap (VMap) --- import qualified Data.VMap as VMap --- import Data.Word --- import GHC.Generics (Generic) import Lens.Micro - --- import Numeric.Natural (Natural) --- import qualified PlutusLedgerApi.V1 as PV1 --- import System.Random import Test.Cardano.Ledger.Allegra.Arbitrary () import Test.Cardano.Ledger.Alonzo.Arbitrary () import Test.Cardano.Ledger.Constrained.Conway.Instances - --- import Test.Cardano.Ledger.Core.Utils -import Test.Cardano.Ledger.Generic.PrettyCore - --- import Test.Cardano.Ledger.TreeDiff (ToExpr) -import Test.QuickCheck hiding (Args, Fun, forAll) - -import qualified Cardano.Crypto.Hash.Class as Hash - --- import Cardano.Ledger.Conway.Rules (ConwayDelegEnv) import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec) +import Test.Cardano.Ledger.Generic.PrettyCore import Test.Cardano.Ledger.Generic.Proof (Proof (..), WitRule (DELEG, GOVCERT, POOL), goSTS) import Test.Cardano.Ledger.Shelley.Utils (epochFromSlotNo) +import Test.QuickCheck hiding (Args, Fun, forAll) -import Control.State.Transition.Extended (BaseM, STS (Environment, Signal)) +import Debug.Trace -- ===================================================== @@ -172,27 +83,27 @@ delegCertSpec :: IsConwayUniv fn => Status -> PParams Conway -> - Specification fn (ConwayDelegEnv Conway, DState Conway, ConwayDelegCert StandardCrypto) + Specification fn (ConwayDelegEnv Conway, DState Conway, ConwayDelegCert StandardCrypto, Int) delegCertSpec status pp = constrained $ \triple -> - match triple $ \env dstate dcert -> + match triple $ \env dstate dcert int -> match env $ \pparams poolregs -> match dstate $ \umap _futgenD _genD _iRewards -> match umap $ \regpairs _ptrs delegstake _ -> [ forAll' regpairs $ \_ rd -> match rd $ \rew _ -> satisfies rew (chooseSpec (1, equalSpec 0) (3, TrueSpec)) , assert $ pparams ==. (lit pp) - , -- , assert $ not_ (disjoint_ (dom_ regpairs) (dom_ delegstake)) - (caseOn dcert) + , dependsOn int dcert + , (caseOn dcert) -- ConwayRegCert !(StakeCredential c) !(StrictMaybe Coin) ( branchW 1 $ \cred mcoin -> [ assert $ mcoin ==. lit (SJust (pp ^. ppKeyDepositL)) - , assertWith 1 status $ not_ (member_ cred (dom_ regpairs)) + , assertWith int 1 status $ not_ (member_ cred (dom_ regpairs)) ] ) -- ConwayUnRegCert !(StakeCredential c) !(StrictMaybe Coin) ( branchW 1 $ \cred mcoin -> [ -- You can only unregister things with 0 reward, so the pair (cred, RDPair 0 _) must be in the map - assertWith 2 status $ member_ cred $ dom_ regpairs + assertWith int 2 status $ member_ cred $ dom_ regpairs , dependsOn mcoin cred , forAll' regpairs $ \key rdpair -> [ whenTrue @@ -204,14 +115,14 @@ delegCertSpec status pp = -- ConwayDelegCert !(StakeCredential c) !(Delegatee c) ( branchW 1 $ \cred delegatee -> [ assert $ not_ (member_ cred (dom_ delegstake)) - , assertWith 3 status $ member_ cred (dom_ regpairs) + , assertWith int 3 status $ member_ cred (dom_ regpairs) , delegateeInPools poolregs delegatee ] ) -- ConwayRegDelegCert !(StakeCredential c) !(Delegatee c) !Coin ( branchW 1 $ \cred delegatee c -> [ assert $ c ==. lit (pp ^. ppKeyDepositL) - , assertWith 4 status $ not_ (member_ cred (dom_ regpairs)) + , assertWith int 4 status $ not_ (member_ cred (dom_ regpairs)) , delegateeInPools poolregs delegatee ] ) @@ -257,21 +168,21 @@ poolRuleSpec :: IsConwayUniv fn => Status -> PParams Conway -> - Specification fn (PoolEnv Conway, PState Conway, PoolCert StandardCrypto) + Specification fn (PoolEnv Conway, PState Conway, PoolCert StandardCrypto, Int) poolRuleSpec status pp = constrained $ \triple -> - match triple $ \poolenv pstate poolcert -> + match triple $ \poolenv pstate poolcert int -> match poolenv $ \slot pparams -> [ assert $ pparams ==. lit (pp) , (caseOn poolcert) -- RegPool :: PoolParams c -> PoolCert c ( branchW 1 $ \poolparam -> [ match poolparam $ \_ident _vrf _pledge cost _margin rewAccnt _owners _relays mMetadata -> - [ assertWith 1 status $ cost >=. lit (pp ^. ppMinPoolCostL) - , match rewAccnt $ \net' _ -> [assertWith 2 status $ net' ==. lit Testnet] + [ assertWith int 1 status $ cost >=. lit (pp ^. ppMinPoolCostL) + , match rewAccnt $ \net' _ -> [assertWith int 2 status $ net' ==. lit Testnet] , onJust' mMetadata $ \metadata -> - match metadata $ \_ hash -> [assertWith 3 status $ strLen_ hash <=. lit (maxMetaLen - 1)] + match metadata $ \_ hash -> [assertWith int 3 status $ strLen_ hash <=. lit (maxMetaLen - 1)] -- Aside form these constraints - -- registering a poolparam is very flexible. The ppol can already be registered. + -- registering a poolparam is very flexible. The pool can already be registered. -- It can be schedled for retirement. It can aleady be in the future pool params. -- The only thing that can cause a failure (in Conway Era) is malformed poolparams -- properties. There are no properties relating the Poolparams to the Env or State. @@ -282,7 +193,7 @@ poolRuleSpec status pp = constrained $ \triple -> ( branchW 1 $ \keyhash epochNo -> match pstate $ \curPoolparams _futpoolparams _retiring _pooldeposits -> [ curPoolparams `dependsOn` keyhash - , assertWith 4 status $ member_ keyhash (dom_ curPoolparams) + , assertWith int 4 status $ member_ keyhash (dom_ curPoolparams) , reify slot (epochFromSlotNo) @@ -320,6 +231,7 @@ govRuleSpec :: ( ConwayGovCertEnv (ConwayEra StandardCrypto) , VState (ConwayEra StandardCrypto) , ConwayGovCert StandardCrypto + , Int ) govRuleSpec status = let getDeposits :: @@ -329,7 +241,7 @@ govRuleSpec status = getDRepDeposit :: ConwayEraPParams era => PParams era -> Coin getDRepDeposit pp = pp ^. ppDRepDepositL in constrained $ \triple -> - match triple $ \env vstate govcert -> + match triple $ \env vstate govcert int -> match env $ \pp _ -> match vstate $ \voteDelegation _comState _dormantEpochs -> [ satisfies pp pparamsSpec @@ -337,24 +249,24 @@ govRuleSpec status = govcert -- ConwayRegDRep:: Credential 'DRepRole c -> Coin -> StrictMaybe (Anchor c) -> ConwayGovCert c ( branchW 3 $ \key coin _ -> - [ assertWith 1 status $ not_ $ member_ key (dom_ voteDelegation) + [ assertWith int 1 status $ not_ $ member_ key (dom_ voteDelegation) , reify pp getDRepDeposit (\deposit -> coin ==. deposit) ] ) -- ConwayUnRegDRep:: Credential 'DRepRole c -> Coin -> ConayGovCert ( branchW 6 $ \cred coin -> [ dependsOn voteDelegation (pair_ cred coin) - , reify voteDelegation getDeposits $ \deposits -> assertWith 1 status $ elem_ (pair_ cred coin) deposits + , reify voteDelegation getDeposits $ \deposits -> assertWith int 1 status $ elem_ (pair_ cred coin) deposits ] ) -- ConwayUpdateDRep :: Credential 'DRepRole c -> StrictMaybe (Anchor c) -> ConwayGovCert ( branchW 2 $ \key _ -> - assertWith 1 status $ member_ key (dom_ voteDelegation) + assertWith int 1 status $ member_ key (dom_ voteDelegation) ) -- ConwayAuthCommitteeHotKey:: Credential 'ColdCommitteeRole c -> Credential 'HotCommitteeRole c -> ConwayGovCert - (branchW 1 $ \c _ -> assertWith 1 status (c ==. c)) + (branchW 1 $ \c _ -> assertWith int 1 status (c ==. c)) -- ConwayResignCommitteeColdKey :: Credential 'ColdCommitteeRole c -> StrictMaybe (Anchor c) -> ConwayGovCert - (branchW 1 $ \c _ -> assertWith 1 status (c ==. c)) + (branchW 1 $ \c _ -> assertWith int 1 status (c ==. c)) ] govName :: ConwayGovCert c -> String @@ -368,12 +280,18 @@ govName x = case x of -- ================================================================= -- A test for every Rule -data Status = Apply | Invert | Remove deriving (Show) +data Status = Apply | Invert Int | Remove deriving (Show) -assertWith :: IsConwayUniv fn => Int -> Status -> Term fn Bool -> Pred fn -assertWith n Apply x = assertExplain ["Status Apply " ++ show n ++ " (" ++ show x ++ ")"] x -assertWith n Invert x = assertExplain ["Status Negate " ++ show n ++ " (" ++ show x ++ ")"] (not_ x) -assertWith n Remove x = assertExplain ["Status Remove " ++ show n ++ " (" ++ show x ++ ")"] TruePred +assertWith :: IsConwayUniv fn => Term fn Int -> Int -> Status -> Term fn Bool -> Pred fn +assertWith _termi n Apply x = assertExplain ["Status Apply " ++ show n ++ " (" ++ show x ++ ")"] x +assertWith _termi n (Invert m) x = + if n == m + then assertExplain ["Status Invert " ++ show n ++ " (" ++ show x ++ ")"] [not_ x] -- termi ==. lit n] + else + assertExplain + ["Status Nonmatching Invert (" ++ show n ++ " /= " ++ show m ++ " (" ++ show x ++ ")"] + [x] -- termi ==. lit 0] +assertWith _termi n Remove x = assertExplain ["Status Remove " ++ show n ++ " (" ++ show x ++ ")"] TruePred testRule :: ( STS (EraRule s a) @@ -384,23 +302,40 @@ testRule :: ) => WitRule s a -> Status -> - Specification ConwayFn (Environment (EraRule s a), State (EraRule s a), Signal (EraRule s a)) -> + Specification ConwayFn (Environment (EraRule s a), State (EraRule s a), Signal (EraRule s a), Int) -> (Signal (EraRule s a) -> String) -> Gen Property testRule witrule status thespec name = do - (env, state, signal) <- genFromSpec @ConwayFn thespec + (env, state, signal, n) <- genFromSpec @ConwayFn thespec goSTS witrule env state - signal + (trace ("\nThe tag " ++ show n ++ " " ++ show status) signal) ( \x -> case (x, status) of (Left fails, Apply) -> pure $ counterexample ("Apply " ++ show signal ++ "\n" ++ show fails) (property False) - (Left _fails, Invert) -> pure $ classify True (name signal ++ ", Does not pass, as expected.") $ property True + (Left _fails, Invert m) -> + if n == m + then pure $ classify True (name signal ++ ", Does not pass, as expected.") $ property True + else + pure $ + counterexample + ( "Invert with non-matching tags (" + ++ show n + ++ " /= " + ++ show m + ++ ") " + ++ show signal + ++ "\nIt should pass, but it does not" + ) + (property False) (Left _fails, Remove) -> pure $ classify True (name signal ++ " Fails") $ property True (Right _newdstate, Apply) -> pure $ classify True (name signal) $ property True - (Right _newdstate, Invert) -> pure $ counterexample ("Invert " ++ show signal ++ "\nfails.") (property False) + (Right _newdstate, Invert m) -> + if n == m -- This is the term inverted, it should fail, if n /= m, it should succeed + then pure $ counterexample ("Invert " ++ show m ++ " " ++ show signal ++ "\nfails.") (property False) + else pure $ classify True (name signal) (property True) (Right _newdstate, Remove) -> pure $ classify True (name signal ++ " We got lucky, it randomly succeeds.") $ property True )