Skip to content

Commit

Permalink
Added State.hs to cabal file
Browse files Browse the repository at this point in the history
  • Loading branch information
@TimSheard
TimSheard committed Apr 30, 2024
1 parent 8885359 commit d079720
Show file tree
Hide file tree
Showing 4 changed files with 48 additions and 53 deletions.
1 change: 1 addition & 0 deletions libs/cardano-ledger-test/cardano-ledger-test.cabal
View file
Original file line number Diff line number Diff line change
Expand Up @@ -64,6 +64,7 @@ library
Test.Cardano.Ledger.Constrained.Conway.PParams
Test.Cardano.Ledger.Constrained.Conway.Gov
Test.Cardano.Ledger.Constrained.Conway.Utxo
Test.Cardano.Ledger.Constrained.Conway.State
Test.Cardano.Ledger.Examples.BabbageFeatures
Test.Cardano.Ledger.Examples.AlonzoValidTxUTXOW
Test.Cardano.Ledger.Examples.AlonzoInvalidTxUTXOW
Expand Down
1 change: 1 addition & 0 deletions libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -79,6 +79,7 @@ govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} =
(minV' ==. minV + 1)
(minV' ==. 0)
]
]
, forAll (snd_ hardForkTree) (genHint treeGenHint)
, genHint listSizeHint (snd_ hardForkTree)
, -- Committee
Expand Down
4 changes: 2 additions & 2 deletions libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1318,7 +1318,7 @@ instance IsConwayUniv fn => HasSpec fn (PulsingSnapshot (ConwayEra StandardCrypt
type DRepPulserTypes =
'[ Int
, UMap StandardCrypto
, Map (Credential 'Staking StandardCrypto) (CompactForm Coin)
, Int
, Map (Credential 'Staking StandardCrypto) (CompactForm Coin)
, PoolDistr StandardCrypto
, Map (DRep StandardCrypto) (CompactForm Coin)
Expand All @@ -1339,7 +1339,7 @@ instance
inject @"DRepPulser" @'["DRepPulser" ::: DRepPulserTypes]
dpPulseSize
dpUMap
dpBalance
dpIndex
dpStakeDistr
dpStakePoolDistr
dpDRepDistr
Expand Down
95 changes: 44 additions & 51 deletions libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/State.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
Expand All @@ -11,33 +13,28 @@
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

-- | Specs necessary to generate constrained (well formed) values in the Cardano Ledger.
module Test.Cardano.Ledger.Constrained.Conway.State where

import Cardano.Ledger.Alonzo.TxOut (AlonzoTxOut (..))
import Cardano.Ledger.Api
import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..))
import Cardano.Ledger.BaseTypes (BoundedRational (..))
import Cardano.Ledger.BaseTypes hiding (inject)
import Cardano.Ledger.CertState
import Cardano.Ledger.CertState (obligationCertState, sumObligation)
import Cardano.Ledger.Coin (Coin (..), CompactForm (CompactCoin), DeltaCoin (..))
import Cardano.Ledger.Conway.PParams
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.TxCert
import Cardano.Ledger.Core
import Cardano.Ledger.Core (Value)
import Cardano.Ledger.Credential (Credential, Ptr, StakeCredential, StakeReference (..))
import Cardano.Ledger.Credential (Credential, Ptr, StakeReference (..))
import Cardano.Ledger.EpochBoundary (SnapShot (..), SnapShots (..), Stake (..), calculatePoolDistr)
import Cardano.Ledger.Keys (GenDelegs (..), KeyHash, KeyRole (..))
import Cardano.Ledger.Mary (MaryValue (..))
import Cardano.Ledger.Mary.Value (AssetName (..), MultiAsset (..), PolicyID (..))
import Cardano.Ledger.Plutus (ExUnits (..), Prices (..))
import Cardano.Ledger.Keys (KeyHash, KeyRole (..))
import Cardano.Ledger.Mary (MaryValue)
import Cardano.Ledger.PoolDistr (PoolDistr (..))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.SafeHash (SafeHash)
import Cardano.Ledger.SafeHash ()
import Cardano.Ledger.Shelley.LedgerState (
AccountState (..),
EpochState (..),
Expand All @@ -48,52 +45,32 @@ import Cardano.Ledger.Shelley.LedgerState (
UTxOState (..),
updateStakeDistribution,
)
import Cardano.Ledger.Shelley.PoolRank (Likelihood (..), NonMyopic (..))
import Cardano.Ledger.Shelley.TxOut (ShelleyTxOut (..))
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
import Cardano.Ledger.UMap (RDPair, UMap (..))
import Cardano.Ledger.TxIn (TxId (..))
import Cardano.Ledger.UMap (CompactForm (..), RDPair)
import qualified Cardano.Ledger.UMap as UMap
import Cardano.Ledger.UTxO (UTxO (..))
import Cardano.Ledger.Val (Val (..))
import Constrained hiding (Value)
import Constrained.Base (
HasGenHint (Hint),
NumSpec (..),
Pred (GenHint),
SizeSpec,
Sized (..),
hasSize,
rangeSize,
(<=.),
(==.),
)
import Constrained.GenT
import Constrained.Base (Sized (..), hasSize, rangeSize)
import Constrained.Spec.Map (rngSet_)
import Constrained.Univ
import Data.Default.Class (Default (def))
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Proxy (Proxy (..))
import Data.VMap (VB, VMap, VP)
import qualified Data.VMap as VMap
import Data.Word (Word16, Word32, Word64)
import Debug.Trace
import GHC.Generics (Generic (..))
import GHC.Natural
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Conway (ConwayFn, IsConwayUniv)
import Test.Cardano.Ledger.Constrained.Conway.Gov (canFollow, govEnvSpec, govProposalsSpec)
import Data.Word (Word64)
import Test.Cardano.Ledger.Constrained.Conway ()

-- Num EpochNo
import Test.Cardano.Ledger.Constrained.Conway.Gov (govProposalsSpec)
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
import Test.Cardano.Ledger.Constrained.Conway.Utxo
import Test.Cardano.Ledger.Constrained.Conway.Utxo (utxoStateSpec)
import Test.Cardano.Ledger.Generic.PrettyCore (
PrettyA (prettyA),
pcIRewards,
pcSnapShotL,
pcSnapShots,
ppRecord,
uMapSummary,
)
import Test.QuickCheck (Gen, arbitrary, generate)

Expand Down Expand Up @@ -252,7 +229,7 @@ betterTxOutAlonzo delegs txOut =
]
)
( branch $ \bootstrapAddr ->
match bootstrapAddr $ \_ nm _ -> False
match bootstrapAddr $ \_ _nm _ -> False
{-
(caseOn nm)
(branch $ \_ -> False)
Expand Down Expand Up @@ -291,8 +268,8 @@ delegatedStakeReference delegs =
caseOn
ref
(branch $ \base -> member_ base (dom_ delegs))
(branch $ \ptr -> False)
(branch $ \null -> False)
(branch $ \_ptr -> False)
(branch $ \_null -> False)

-- ====================================================================================
-- Some Specifications are constrained by types (say 'x') that do not appear in the type being
Expand All @@ -304,7 +281,7 @@ delegatedStakeReference delegs =
-- as inputs to the tests and examples of those 'inner' specifications.
-- ====================================================================================

testAcctState :: IsConwayUniv fn => Term fn AccountState
testAcctState :: Term fn AccountState
testAcctState = lit (AccountState (Coin 100) (Coin 100))

testGovEnv :: Era era => PParams era -> GovEnv era
Expand All @@ -317,7 +294,7 @@ testGovEnv pp =
SNothing
(CommitteeState Map.empty)

testEpochNo :: IsConwayUniv fn => Term fn EpochNo
testEpochNo :: Term fn EpochNo
testEpochNo = lit (EpochNo 99)

-- ================================================================================
Expand All @@ -341,6 +318,7 @@ instantaneousrewardsspec acct = constrained $ \irewards ->
, assert $ (toDelta_ (foldMap_ id (rng_ treasury))) - deltaTreas <=. toDelta_ acctTreas
]

go1 :: IO ()
go1 = do
acct <- generate (arbitrary :: Gen AccountState)
let xx :: Specification ConwayFn (InstantaneousRewards StandardCrypto)
Expand All @@ -362,6 +340,7 @@ drepstatespec epoch = constrained $ \drepstate ->
, assertExplain ["no deposit is 0"] $ lit (Coin 0) <=. deposit
]

go2 :: IO Bool
go2 = ioTest @(DRepState StandardCrypto) (drepstatespec testEpochNo)

vstatespec :: (IsConwayUniv fn, Era era) => Term fn EpochNo -> Specification fn (VState era)
Expand All @@ -375,6 +354,7 @@ vstatespec epoch = constrained $ \vstate ->
, match comstate $ \commap -> sizeRng commap 1 4
]

go3 :: IO Bool
go3 = ioTest @(VState Shelley) (vstatespec testEpochNo)

dstatespec ::
Expand Down Expand Up @@ -431,6 +411,7 @@ pstatespec currepoch = constrained $ \ps ->
, assert $ sizeOf_ (dom_ stakePoolParams) <=. 8
]

go5 :: IO Bool
go5 = ioTest @(PState Shelley) (pstatespec testEpochNo)

accountstatespec :: IsConwayUniv fn => Specification fn AccountState
Expand All @@ -453,6 +434,7 @@ certstatespec acct epoch = constrained $ \cs ->
, reify pState psStakePoolParams (\poolreg -> satisfies dState (dstatespec acct poolreg))
]

go6 :: IO Bool
go6 = ioTest @(CertState Shelley) (certstatespec testAcctState testEpochNo)

-- ==============================================================
Expand Down Expand Up @@ -531,6 +513,7 @@ shelleygovstatespec pp =
, assert $ curpp ==. lit pp
]

go9 :: IO Bool
go9 = ioTest @(ShelleyGovState Mary) (shelleygovstatespec @Mary @ConwayFn def)

-- | This code does not work, it does not constrain 'cm'
Expand All @@ -542,24 +525,25 @@ shelleygovstatespec2 =
match curpro $ \cm ->
match futpro $ \fm -> [satisfies cm (hasSize (rangeSize 1 2)), satisfies fm (hasSize (rangeSize 1 2))]

go10 :: IO Bool
go10 = ioTest @(ShelleyGovState Mary) shelleygovstatespec2

govenvspec ::
IsConwayUniv fn =>
PParams Conway ->
Specification fn (GovEnv Conway)
govenvspec pp = constrained $ \ge ->
match ge $ \_ _ cpp _ _ _ -> [assert $ lit pp ==. cpp]
match ge $ \_ _ cppx _ _ _ -> [assert $ lit pp ==. cppx]

conwaygovstatespec ::
forall era fn.
forall fn.
Constrain Conway fn =>
PParams Conway ->
GovEnv Conway ->
Specification fn (ConwayGovState Conway)
conwaygovstatespec pp govenv =
constrained $ \conwaygs ->
match conwaygs $ \proposals mcommittee consti curpp prevpp _derepPulstate ->
match conwaygs $ \proposals _mcommittee _consti curpp _prevpp _derepPulstate ->
[ assert $ curpp ==. lit pp
, satisfies proposals (govProposalsSpec govenv)
]
Expand All @@ -580,6 +564,7 @@ ledgerstatespec pp acct epoch =
, reify csg id (\certstate -> satisfies utxoS (utxostatespec @era @fn pp certstate))
]

go11 :: IO ()
go11 = do
ls <- generateSpec (ledgerstatespec @Shelley @ConwayFn def testAcctState testEpochNo)
let d = sumObligation $ obligationCertState $ lsCertState ls
Expand All @@ -599,6 +584,7 @@ snapshotspec =
, assert $ poolparams ==. lit VMap.empty
]

go12 :: IO ()
go12 = do
-- No PrettyA instance so we write it out
sn <- generateSpec (snapshotspec @(EraCrypto Shelley) @ConwayFn)
Expand All @@ -608,7 +594,7 @@ snapshotsspec ::
(Crypto c, IsConwayUniv fn) => Term fn (SnapShot c) -> Specification fn (SnapShots c)
snapshotsspec marksnap =
constrained $ \snap ->
match snap $ \mark pooldistr set go fee ->
match snap $ \mark pooldistr set go _fee ->
Block
[ assert $ mark ==. marksnap
, satisfies set snapshotspec
Expand All @@ -617,6 +603,7 @@ snapshotsspec marksnap =
-- , match pooldistr $ \x -> [assert $ x ==. lit Map.empty] -- TODO eventually must add up to (1 % 1)
]

go13 :: IO Bool
go13 =
ioTest @(SnapShots StandardCrypto)
(snapshotsspec (lit (SnapShot (Stake VMap.empty) VMap.empty VMap.empty)))
Expand Down Expand Up @@ -651,6 +638,7 @@ epochstatespec pp epoch =
, match nonmyopic $ \x c -> [assert $ (sizeOf_ x) ==. 0, assert $ c ==. lit (Coin 0)]
]

go14 :: IO Bool
go14 = ioTest @(EpochState Babbage) (epochstatespec def testEpochNo)

getPoolDistr :: forall era. EpochState era -> PoolDistr (EraCrypto era)
Expand All @@ -668,7 +656,7 @@ newepochstatespecUnit pp =
( \nes ->
match
(nes :: Term fn (NewEpochState era))
( \eno bm1 bm2 es mpulser pooldistr stashAvvm ->
( \eno bm1 bm2 es _mpulser pooldistr stashAvvm ->
Block
[ reify eno id (\epoch -> satisfies es (epochstatespec @era @fn pp epoch))
, satisfies stashAvvm (constrained (\x -> lit () ==. x))
Expand All @@ -691,7 +679,7 @@ newepochstatespecUTxO pp =
( \nes ->
match
(nes :: Term fn (NewEpochState era))
( \eno bm1 bm2 es mpulser pooldistr stashAvvm ->
( \eno bm1 bm2 es _mpulser pooldistr stashAvvm ->
Block
[ reify eno id (\epoch -> satisfies es (epochstatespec @era @fn pp epoch))
, satisfies stashAvvm (constrained (\u -> u ==. lit (UTxO @era Map.empty)))
Expand All @@ -702,7 +690,10 @@ newepochstatespecUTxO pp =
)
)

go15 :: IO Bool
go15 = ioTest @(NewEpochState Shelley) (newepochstatespec def)

go16 :: IO Bool
go16 = ioTest @(NewEpochState Alonzo) (newepochstatespec def)

-- ==============================================================
Expand Down Expand Up @@ -840,6 +831,7 @@ testsum =
match pair (\m1 m2 -> [assert $ foldMap_ id (rng_ m1) ==. foldMap_ id (rng_ m2)])
)

goSum1 :: IO ()
goSum1 = do
(x, y) <- genSpec testsum
putStrLn (show (prettyA x) ++ show (foldMap id x))
Expand All @@ -848,6 +840,7 @@ goSum1 = do
test1 :: Specification ConwayFn (Map Int Coin)
test1 = constrained (\x -> [assert $ foldMap_ toDelta_ (rng_ x) ==. lit (DeltaCoin 10)])

goSum2 :: IO ()
goSum2 = do
x <- genSpec test1
putStrLn (show (prettyA x) ++ show (foldMap id x))

0 comments on commit d079720

Please sign in to comment.