{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ViewPatterns #-}

-- | Specs necessary to generate, environment, state, and signal
-- for the EPOCH rule
module Test.Cardano.Ledger.Constrained.Conway.Epoch where

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Coin
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Shelley.API.Types
import Constrained.API
import Data.Foldable
import Data.Map.Strict (Map)
import GHC.Generics (Generic)
import Lens.Micro.Extras
import Test.Cardano.Ledger.Constrained.Conway.Gov
import Test.Cardano.Ledger.Constrained.Conway.Instances

data EpochExecEnv era = EpochExecEnv
  { forall era.
EpochExecEnv era -> Map (Credential 'Staking) (CompactForm Coin)
eeeStakeDistr :: Map (Credential 'Staking) (CompactForm Coin)
  , forall era. EpochExecEnv era -> EpochNo
eeeEpochNo :: EpochNo
  }
  deriving (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x. Rep (EpochExecEnv era) x -> EpochExecEnv era
forall era x. EpochExecEnv era -> Rep (EpochExecEnv era) x
$cto :: forall era x. Rep (EpochExecEnv era) x -> EpochExecEnv era
$cfrom :: forall era x. EpochExecEnv era -> Rep (EpochExecEnv era) x
Generic, EpochExecEnv era -> EpochExecEnv era -> Bool
forall era. EpochExecEnv era -> EpochExecEnv era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: EpochExecEnv era -> EpochExecEnv era -> Bool
$c/= :: forall era. EpochExecEnv era -> EpochExecEnv era -> Bool
== :: EpochExecEnv era -> EpochExecEnv era -> Bool
$c== :: forall era. EpochExecEnv era -> EpochExecEnv era -> Bool
Eq, Int -> EpochExecEnv era -> ShowS
forall era. Int -> EpochExecEnv era -> ShowS
forall era. [EpochExecEnv era] -> ShowS
forall era. EpochExecEnv era -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [EpochExecEnv era] -> ShowS
$cshowList :: forall era. [EpochExecEnv era] -> ShowS
show :: EpochExecEnv era -> String
$cshow :: forall era. EpochExecEnv era -> String
showsPrec :: Int -> EpochExecEnv era -> ShowS
$cshowsPrec :: forall era. Int -> EpochExecEnv era -> ShowS
Show)

epochEnvSpec :: Specification (EpochExecEnv ConwayEra)
epochEnvSpec :: Specification (EpochExecEnv ConwayEra)
epochEnvSpec = forall a. Specification a
TrueSpec

epochStateSpec ::
  Term EpochNo ->
  Specification (EpochState ConwayEra)
epochStateSpec :: Term EpochNo -> Specification (EpochState ConwayEra)
epochStateSpec Term EpochNo
epochNo = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (EpochState ConwayEra)
es ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (EpochState ConwayEra)
es forall a b. (a -> b) -> a -> b
$ \Term ChainAccountState
_accountState Term (LedgerState ConwayEra)
ledgerState Term SnapShots
_snapShots Term NonMyopic
_nonMyopic ->
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (LedgerState ConwayEra)
ledgerState forall a b. (a -> b) -> a -> b
$ \Term (UTxOState ConwayEra)
utxoState Term (ConwayCertState ConwayEra)
certState ->
      forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (UTxOState ConwayEra)
utxoState forall a b. (a -> b) -> a -> b
$ \Term (UTxO ConwayEra)
_utxo Term Coin
_deposited Term Coin
_fees Term (ConwayGovState ConwayEra)
govState Term (ConwayInstantStake ConwayEra)
_stakeDistr Term Coin
_donation ->
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayGovState ConwayEra)
govState forall a b. (a -> b) -> a -> b
$ \ Term (Proposals ConwayEra)
[var|proposals|] Term (StrictMaybe (Committee ConwayEra))
_committee Term (Constitution ConwayEra)
constitution Term (PParams ConwayEra)
_curPParams Term (PParams ConwayEra)
_prevPParams Term (FuturePParams ConwayEra)
_futPParams Term (DRepPulsingState ConwayEra)
drepPulsingState ->
          [ forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Constitution ConwayEra)
constitution forall a b. (a -> b) -> a -> b
$ \Term Anchor
_ Term (StrictMaybe ScriptHash)
policy ->
              Term (Proposals ConwayEra)
proposals forall a. HasSpec a => Term a -> Specification a -> Pred
`satisfies` Term EpochNo
-> Term (StrictMaybe ScriptHash)
-> Term (CertState ConwayEra)
-> Specification (Proposals ConwayEra)
proposalsSpec Term EpochNo
epochNo Term (StrictMaybe ScriptHash)
policy Term (ConwayCertState ConwayEra)
certState
          , 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 (DRepPulsingState ConwayEra)
drepPulsingState
              -- DRPulsing
              ( 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 (DRepPulser ConwayEra Identity (RatifyState ConwayEra))
pulser ->
                  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (DRepPulser ConwayEra Identity (RatifyState ConwayEra))
pulser forall a b. (a -> b) -> a -> b
$ \Term Int
_size Term UMap
_stakeMap Term Int
_index Term (ConwayInstantStake ConwayEra)
_stakeDistr Term PoolDistr
_stakePoolDistr Term (Map DRep (CompactForm Coin))
_drepDistr Term (Map (Credential 'DRepRole) DRepState)
_drepState Term EpochNo
pulseEpoch Term (CommitteeState ConwayEra)
_committeeState Term (EnactState ConwayEra)
_enactState Term (StrictSeq (GovActionState ConwayEra))
pulseProposals Term (Map (Credential 'Staking) (CompactForm Coin))
_proposalDeposits Term (Map (KeyHash 'StakePool) PoolParams)
_poolParams ->
                    [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term EpochNo
pulseEpoch forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term EpochNo
epochNo
                    , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (StrictSeq (GovActionState ConwayEra))
pulseProposals forall a b. (a -> b) -> a -> b
$ \Term (GovActionState ConwayEra)
gas ->
                        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (GovActionState ConwayEra)
gas forall a b. (a -> b) -> a -> b
$ \Term GovActionId
gasId Term (Map (Credential 'HotCommitteeRole) Vote)
_ Term (Map (Credential 'DRepRole) Vote)
_ Term (Map (KeyHash 'StakePool) Vote)
_ Term (ProposalProcedure ConwayEra)
_ Term EpochNo
_ Term EpochNo
_ ->
                          Term GovActionId -> Term (Proposals ConwayEra) -> Pred
proposalExists Term GovActionId
gasId Term (Proposals ConwayEra)
proposals
                    , -- TODO: something is wrong in this case and I haven't figured out what yet
                      forall p. IsPred p => p -> Pred
assert Bool
False
                    ]
              )
              -- DRComplete
              ( 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 (PulsingSnapshot ConwayEra)
_snap Term (RatifyState ConwayEra)
ratifyState ->
                  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (RatifyState ConwayEra)
ratifyState forall a b. (a -> b) -> a -> b
$ \Term (EnactState ConwayEra)
enactState Term (Seq (GovActionState ConwayEra))
[var|enacted|] Term (Set GovActionId)
[var|expired|] Term Bool
_delayed ->
                    [ -- This may seem strange, but if expired is too big, the 'forAll expired' will fail
                      -- There can't exist more expired proposals, than there are proposals.
                      forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Proposals ConwayEra)
proposals (forall a. Integral a => a -> Integer
toInteger forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Proposals era -> Int
proposalsSize) forall a b. (a -> b) -> a -> b
$ \ Term Integer
[var|sz|] ->
                        [ forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
                            (Term Integer
sz forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
0)
                            (Term (Set GovActionId)
expired forall a. HasSpec a => Term a -> Term a -> Term Bool
==. (forall a. (Typeable a, Eq a, Show a) => a -> Term a
Lit forall a. Monoid a => a
mempty))
                            (forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set GovActionId)
expired forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Integer
sz)
                        ]
                    , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set GovActionId)
expired forall a b. (a -> b) -> a -> b
$ \ Term GovActionId
[var| gasId |] ->
                        Term GovActionId -> Term (Proposals ConwayEra) -> Pred
proposalExists Term GovActionId
gasId Term (Proposals ConwayEra)
proposals
                    , -- TODO: this isn't enough, we need to ensure it's at most
                      -- one of each type of action that's being enacted
                      forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Seq (GovActionState ConwayEra))
enacted forall a b. (a -> b) -> a -> b
$ \ Term (GovActionState ConwayEra)
[var|govact|] ->
                        [ forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Proposals ConwayEra)
proposals forall era. Proposals era -> [GovActionState era]
enactableProposals forall a b. (a -> b) -> a -> b
$ \ Term [GovActionState ConwayEra]
[var|enactable|] -> Term (GovActionState ConwayEra)
govact forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` Term [GovActionState ConwayEra]
enactable
                        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra) -> Term GovActionId
gasId_ Term (GovActionState ConwayEra)
govact forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Term (Set GovActionId)
expired
                        ]
                    , -- TODO: this is a hack to get around the todo above!
                      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 (Seq (GovActionState ConwayEra))
enacted forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
1
                    , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (EnactState ConwayEra)
enactState forall a b. (a -> b) -> a -> b
$
                        \Term (StrictMaybe (Committee ConwayEra))
_cc Term (Constitution ConwayEra)
_con Term (PParams ConwayEra)
_cpp Term (PParams ConwayEra)
_ppp Term Coin
_tr Term (Map (Credential 'Staking) Coin)
_wth Term (GovRelation StrictMaybe ConwayEra)
prevGACTIDS ->
                          forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Proposals ConwayEra)
proposals (forall era. GovRelation PRoot era -> GovRelation StrictMaybe era
toPrevGovActionIds forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era. Lens' (Proposals era) (GovRelation PRoot era)
pRootsL) (Term (GovRelation StrictMaybe ConwayEra)
prevGACTIDS forall a. HasSpec a => Term a -> Term a -> Term Bool
==.)
                    ]
              )
          ]

proposalExists ::
  Term GovActionId ->
  Term (Proposals ConwayEra) ->
  Pred
proposalExists :: Term GovActionId -> Term (Proposals ConwayEra) -> Pred
proposalExists Term GovActionId
gasId Term (Proposals ConwayEra)
proposals =
  forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Proposals ConwayEra)
proposals forall era. Proposals era -> Map GovActionId (GovActionState era)
proposalsActionsMap forall a b. (a -> b) -> a -> b
$ \ Term (Map GovActionId (GovActionState ConwayEra))
[var|actionMap|] ->
    Term GovActionId
gasId forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` 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 GovActionId (GovActionState ConwayEra))
actionMap

epochSignalSpec :: EpochNo -> Specification EpochNo
epochSignalSpec :: EpochNo -> Specification EpochNo
epochSignalSpec EpochNo
curEpoch = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term EpochNo
e ->
  forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
elem_ Term EpochNo
e (forall a. HasSpec a => a -> Term a
lit [EpochNo
curEpoch, forall a. Enum a => a -> a
succ EpochNo
curEpoch])

enactableProposals :: Proposals era -> [GovActionState era]
enactableProposals :: forall era. Proposals era -> [GovActionState era]
enactableProposals Proposals era
proposals =
  [ GovActionState era
gact'
  | GovActionState era
gact <- forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (forall era. Proposals era -> StrictSeq (GovActionState era)
proposalsActions Proposals era
proposals)
  , GovActionState era
gact' <- forall era a.
GovActionState era
-> a
-> (forall (p :: GovActionPurpose).
    (forall (f :: * -> *).
     Lens' (GovRelation f era) (f (GovPurposeId p era)))
    -> StrictMaybe (GovPurposeId p era) -> GovPurposeId p era -> a)
-> a
withGovActionParent GovActionState era
gact [GovActionState era
gact] forall a b. (a -> b) -> a -> b
$
      \forall (f :: * -> *).
Lens' (GovRelation f era) (f (GovPurposeId p era))
_ StrictMaybe (GovPurposeId p era)
mparent GovPurposeId p era
_ ->
        case StrictMaybe (GovPurposeId p era)
mparent of
          StrictMaybe (GovPurposeId p era)
SNothing -> [GovActionState era
gact]
          SJust (GovPurposeId GovActionId
gpid')
            | forall era. GovActionId -> Proposals era -> Bool
isRoot GovActionId
gpid' Proposals era
proposals -> [GovActionState era
gact]
            | Bool
otherwise -> []
  ]

isRoot :: GovActionId -> Proposals era -> Bool
isRoot :: forall era. GovActionId -> Proposals era -> Bool
isRoot GovActionId
gid (forall a s. Getting a s a -> s -> a
view forall era. Lens' (Proposals era) (GovRelation PRoot era)
pRootsL -> GovRelation {PRoot (GovPurposeId 'PParamUpdatePurpose era)
PRoot (GovPurposeId 'HardForkPurpose era)
PRoot (GovPurposeId 'CommitteePurpose era)
PRoot (GovPurposeId 'ConstitutionPurpose era)
grConstitution :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'ConstitutionPurpose era)
grCommittee :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'CommitteePurpose era)
grHardFork :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'HardForkPurpose era)
grPParamUpdate :: forall (f :: * -> *) era.
GovRelation f era -> f (GovPurposeId 'PParamUpdatePurpose era)
grConstitution :: PRoot (GovPurposeId 'ConstitutionPurpose era)
grCommittee :: PRoot (GovPurposeId 'CommitteePurpose era)
grHardFork :: PRoot (GovPurposeId 'HardForkPurpose era)
grPParamUpdate :: PRoot (GovPurposeId 'PParamUpdatePurpose era)
..}) =
  forall a. a -> StrictMaybe a
SJust GovActionId
gid
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [forall {p :: GovActionPurpose} {era}.
PRoot (GovPurposeId p era) -> StrictMaybe GovActionId
getGID PRoot (GovPurposeId 'PParamUpdatePurpose era)
grPParamUpdate, forall {p :: GovActionPurpose} {era}.
PRoot (GovPurposeId p era) -> StrictMaybe GovActionId
getGID PRoot (GovPurposeId 'HardForkPurpose era)
grHardFork, forall {p :: GovActionPurpose} {era}.
PRoot (GovPurposeId p era) -> StrictMaybe GovActionId
getGID PRoot (GovPurposeId 'CommitteePurpose era)
grCommittee, forall {p :: GovActionPurpose} {era}.
PRoot (GovPurposeId p era) -> StrictMaybe GovActionId
getGID PRoot (GovPurposeId 'ConstitutionPurpose era)
grConstitution]
  where
    getGID :: PRoot (GovPurposeId p era) -> StrictMaybe GovActionId
getGID = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (p :: GovActionPurpose) era.
GovPurposeId p era -> GovActionId
unGovPurposeId forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. PRoot a -> StrictMaybe a
prRoot