Skip to content

Commit

Permalink
Cleanup, experiment with Tagging Invert Status
Browse files Browse the repository at this point in the history
  • Loading branch information
@TimSheard
TimSheard committed Jun 19, 2024
1 parent 54b04fb commit 397bbb3
Showing 1 changed file with 62 additions and 127 deletions.
189 changes: 62 additions & 127 deletions .../cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/NecessaryAndSufficient.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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

-- =====================================================

Expand Down Expand Up @@ -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
Expand All @@ -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
]
)
Expand Down Expand Up @@ -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.
Expand All @@ -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)
Expand Down Expand Up @@ -320,6 +231,7 @@ govRuleSpec ::
( ConwayGovCertEnv (ConwayEra StandardCrypto)
, VState (ConwayEra StandardCrypto)
, ConwayGovCert StandardCrypto
, Int
)
govRuleSpec status =
let getDeposits ::
Expand All @@ -329,32 +241,32 @@ 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
, caseOn
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
Expand All @@ -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)
Expand All @@ -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
)

Expand Down

0 comments on commit 397bbb3

Please sign in to comment.