{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}
module Test.Cardano.Ledger.Constrained.Conway.Certs where
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.State
import Constrained.API
import Data.Foldable (toList)
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,
rewDepMapSpec2,
)
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.WitnessUniverse
setMapMaybe :: Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe :: forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe t -> Maybe a
f Set t
set = forall a b. (a -> b -> b) -> b -> Set a -> b
Set.foldr' (\t
x Set a
s -> forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set a
s (forall a. Ord a => a -> Set a -> Set a
`Set.insert` Set a
s) forall a b. (a -> b) -> a -> b
$ t -> Maybe a
f t
x) forall a. Monoid a => a
mempty Set t
set
bootstrapDStateSpec ::
forall era.
EraSpecTxOut era =>
WitUniv era ->
Set (Credential 'DRepRole) ->
Map RewardAccount Coin ->
Specification (DState era)
bootstrapDStateSpec :: forall era.
EraSpecTxOut era =>
WitUniv era
-> Set (Credential 'DRepRole)
-> Map RewardAccount Coin
-> Specification (DState era)
bootstrapDStateSpec WitUniv era
univ Set (Credential 'DRepRole)
delegatees Map RewardAccount Coin
withdrawals =
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (DState era)
[var| dstate |] ->
forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (DState era)
dstate forall a b. (a -> b) -> a -> b
$ \ Term UMap
[var| uMap |] Term (Map FutureGenDeleg GenDelegPair)
futureGenDelegs Term GenDelegs
genDelegs Term InstantaneousRewards
[var|irewards|] ->
[
forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map FutureGenDeleg GenDelegPair)
futureGenDelegs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term Integer
3 else Term Integer
0)
,
forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term GenDelegs
genDelegs forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash 'Genesis) GenDelegPair)
gd ->
[ forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd)
, forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd)
, forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (KeyHash 'Genesis) GenDelegPair)
gd forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (if forall era (proxy :: * -> *). EraSpecDeleg era => proxy era -> Bool
hasGenDelegs @era [] then Term Integer
3 else Term Integer
0)
]
,
forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term InstantaneousRewards
irewards forall a b. (a -> b) -> a -> b
$ \Term (Map (Credential 'Staking) Coin)
w Term (Map (Credential 'Staking) Coin)
x Term DeltaCoin
y Term DeltaCoin
z -> [forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) Coin)
w forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0, forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map (Credential 'Staking) Coin)
x forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Integer
0, Term DeltaCoin
y forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall a. Monoid a => a
mempty, Term DeltaCoin
z forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall a. Monoid a => a
mempty]
,
forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match [var| uMap |] forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var| rdMap |] Term (Map Ptr (Credential 'Staking))
[var| ptrMap |] Term (Map (Credential 'Staking) (KeyHash 'StakePool))
[var| sPoolMap |] Term (Map (Credential 'Staking) DRep)
[var|dRepMap|] ->
[
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (Credential 'Staking) RDPair)
rdMap (forall era.
Era era =>
WitUniv era
-> Map RewardAccount Coin
-> Specification (Map (Credential 'Staking) RDPair)
rewDepMapSpec2 WitUniv era
univ Map RewardAccount Coin
withdrawals)
,
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) DRep)
dRepMap Term (Map (Credential 'Staking) RDPair)
rdMap
, forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential 'Staking) RDPair)
rdMap forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdm|] ->
[ forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap)
, forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (forall a. HasSpec a => a -> Term a
lit (Map RewardAccount Coin -> Set (Credential 'Staking)
keyHashWdrl Map RewardAccount Coin
withdrawals)) (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap)
, forall era t. Witnessed era t => WitUniv era -> Term t -> Pred
witness WitUniv era
univ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'Staking) DRep)
dRepMap)
, forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) DRep)
dRepMap) (forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) RDPair)
rdm)
,
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
HasSpec (SimpleRep a), HasSimpleRep a,
All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
HasSpec a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Map (Credential 'Staking) DRep)
dRepMap forall a b. (a -> b) -> a -> b
$ \Term (Credential 'Staking)
_ Term DRep
dRep ->
[ (forall a.
(HasSpec a, HasSpec (SimpleRep a), HasSimpleRep a,
TypeSpec a ~ TypeSpec (SimpleRep a),
SimpleRep a ~ SumOver (Cases (SimpleRep a)),
TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy (MapList (Weighted Binder) (Cases (SimpleRep a))) Pred
caseOn Term DRep
dRep)
(forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'DRepRole)
kh -> forall p. IsPred p => p -> Pred
assert (Term (KeyHash 'DRepRole)
kh forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` forall a. HasSpec a => a -> Term a
lit (forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe forall (r :: KeyRole). Credential r -> Maybe (KeyHash r)
credKeyHash Set (Credential 'DRepRole)
delegatees)))
(forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ScriptHash
sh -> forall p. IsPred p => p -> Pred
assert (Term ScriptHash
sh forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` forall a. HasSpec a => a -> Term a
lit (forall a t. Ord a => (t -> Maybe a) -> Set t -> Set a
setMapMaybe forall (kr :: KeyRole). Credential kr -> Maybe ScriptHash
credScriptHash Set (Credential 'DRepRole)
delegatees)))
(forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> forall p. IsPred p => p -> Pred
assert Bool
True)
(forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted Binder a
branch forall a b. (a -> b) -> a -> b
$ \Term ()
_ -> forall p. IsPred p => p -> Pred
assert Bool
True)
]
]
,
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap Term (Map (Credential 'Staking) RDPair)
rdMap
, forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential 'Staking) RDPair)
rdMap forall a. a -> a
id forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential 'Staking) RDPair)
[var|rdmp|] ->
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom sPoolMap is a subset of dom rdMap") forall a b. (a -> b) -> a -> b
$ forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) (KeyHash 'StakePool))
sPoolMap forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential 'Staking) RDPair)
rdmp
,
forall p. IsPred p => NonEmpty String -> p -> Pred
assertExplain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"dom ptrMap is empty") forall a b. (a -> b) -> a -> b
$ forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map Ptr (Credential 'Staking))
ptrMap forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. Monoid a => a
mempty
]
]
txZero :: EraTx era => Tx era
txZero :: forall era. EraTx era => Tx era
txZero = forall era. EraTx era => TxBody era -> Tx era
mkBasicTx forall era. EraTxBody era => TxBody era
mkBasicTxBody
certsEnvSpec ::
(EraSpecPParams era, HasSpec (Tx era)) =>
Specification (CertsEnv era)
certsEnvSpec :: forall era.
(EraSpecPParams era, HasSpec (Tx era)) =>
Specification (CertsEnv era)
certsEnvSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (CertsEnv era)
ce ->
forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CertsEnv era)
ce forall a b. (a -> b) -> a -> b
$ \Term (Tx era)
tx Term (PParams era)
pp Term EpochNo
_currepoch Term (StrictMaybe (Committee era))
_currcommittee Term
(Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
commproposals ->
[ forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParams era)
pp forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec
, forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Tx era)
tx forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall era. EraTx era => Tx era
txZero
, forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Hint
(Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
3 Term
(Map (GovPurposeId 'CommitteePurpose era) (GovActionState era))
commproposals
]
projectEnv :: CertsEnv era -> CertEnv era
projectEnv :: forall era. CertsEnv era -> CertEnv era
projectEnv CertsEnv era
x =
CertEnv
{ cePParams :: PParams era
cePParams = forall era. CertsEnv era -> PParams era
certsPParams CertsEnv era
x
, ceCurrentEpoch :: EpochNo
ceCurrentEpoch = forall era. CertsEnv era -> EpochNo
certsCurrentEpoch CertsEnv era
x
, ceCurrentCommittee :: StrictMaybe (Committee era)
ceCurrentCommittee = forall era. CertsEnv era -> StrictMaybe (Committee era)
certsCurrentCommittee CertsEnv era
x
, ceCommitteeProposals :: Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
ceCommitteeProposals = forall era.
CertsEnv era
-> Map (GovPurposeId 'CommitteePurpose era) (GovActionState era)
certsCommitteeProposals CertsEnv era
x
}
txCertsSpec ::
forall era.
EraSpecCert era =>
WitUniv era ->
CertsEnv era ->
CertState era ->
Specification (Seq (TxCert era))
txCertsSpec :: forall era.
EraSpecCert era =>
WitUniv era
-> CertsEnv era
-> CertState era
-> Specification (Seq (TxCert era))
txCertsSpec WitUniv era
univ CertsEnv era
env CertState era
state =
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (Seq (TxCert era))
seqs ->
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists
(\forall b. Term b -> b
eval -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (forall b. Term b -> b
eval Term (Seq (TxCert era))
seqs))
(\Term [TxCert era]
list -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (forall a b.
(HasSpec a, HasSpec b, IsNormalType a, IsNormalType b) =>
Term a -> Term b -> Term (a, b)
pair_ Term [TxCert era]
list Term (Seq (TxCert era))
seqs) (forall era.
EraSpecCert era =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec @era WitUniv era
univ (forall era. CertsEnv era -> CertEnv era
projectEnv @era CertsEnv era
env) CertState era
state))
noSameKeys :: forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys :: forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys [] = []
noSameKeys (TxCert era
x : [TxCert era]
xs) = TxCert era
x forall a. a -> [a] -> [a]
: forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys @era (forall a. (a -> Bool) -> [a] -> [a]
filter (\TxCert era
y -> forall era. EraSpecCert era => TxCert era -> CertKey
txCertKey @era TxCert era
x forall a. Eq a => a -> a -> Bool
/= forall era. EraSpecCert era => TxCert era -> CertKey
txCertKey @era TxCert era
y) [TxCert era]
xs)
listSeqCertPairSpec ::
forall era.
EraSpecCert era =>
WitUniv era ->
CertEnv era ->
CertState era ->
Specification ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec :: forall era.
EraSpecCert era =>
WitUniv era
-> CertEnv era
-> CertState era
-> Specification ([TxCert era], Seq (TxCert era))
listSeqCertPairSpec WitUniv era
univ CertEnv era
env CertState era
state =
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
IsProd (SimpleRep a), HasSpec a, IsPred p) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' forall a b. (a -> b) -> a -> b
$ \Term [TxCert era]
list Term (Seq (TxCert era))
seqs ->
[ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term [TxCert era]
list forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
5
, forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [TxCert era]
list forall a b. (a -> b) -> a -> b
$ \Term (TxCert era)
x -> forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (TxCert era)
x (forall era.
EraSpecCert era =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (TxCert era)
txCertSpec @era WitUniv era
univ CertEnv era
env CertState era
state)
, forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term [TxCert era]
list (forall a. [a] -> Seq a
fromList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraSpecCert era => [TxCert era] -> [TxCert era]
noSameKeys @era) (\Term (Seq (TxCert era))
x -> Term (Seq (TxCert era))
seqs forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Seq (TxCert era))
x)
]