{-# 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 x. EpochExecEnv era -> Rep (EpochExecEnv era) x)
-> (forall x. Rep (EpochExecEnv era) x -> EpochExecEnv era)
-> Generic (EpochExecEnv era)
forall x. Rep (EpochExecEnv era) x -> EpochExecEnv era
forall x. EpochExecEnv era -> Rep (EpochExecEnv era) x
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
$cfrom :: forall era x. EpochExecEnv era -> Rep (EpochExecEnv era) x
from :: forall x. EpochExecEnv era -> Rep (EpochExecEnv era) x
$cto :: forall era x. Rep (EpochExecEnv era) x -> EpochExecEnv era
to :: forall x. Rep (EpochExecEnv era) x -> EpochExecEnv era
Generic, EpochExecEnv era -> EpochExecEnv era -> Bool
(EpochExecEnv era -> EpochExecEnv era -> Bool)
-> (EpochExecEnv era -> EpochExecEnv era -> Bool)
-> Eq (EpochExecEnv era)
forall era. EpochExecEnv era -> EpochExecEnv era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era. EpochExecEnv era -> EpochExecEnv era -> Bool
== :: EpochExecEnv era -> EpochExecEnv era -> Bool
$c/= :: forall era. EpochExecEnv era -> EpochExecEnv era -> Bool
/= :: EpochExecEnv era -> EpochExecEnv era -> Bool
Eq, Int -> EpochExecEnv era -> ShowS
[EpochExecEnv era] -> ShowS
EpochExecEnv era -> String
(Int -> EpochExecEnv era -> ShowS)
-> (EpochExecEnv era -> String)
-> ([EpochExecEnv era] -> ShowS)
-> Show (EpochExecEnv era)
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
$cshowsPrec :: forall era. Int -> EpochExecEnv era -> ShowS
showsPrec :: Int -> EpochExecEnv era -> ShowS
$cshow :: forall era. EpochExecEnv era -> String
show :: EpochExecEnv era -> String
$cshowList :: forall era. [EpochExecEnv era] -> ShowS
showList :: [EpochExecEnv era] -> ShowS
Show)

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

epochStateSpec ::
  Term EpochNo ->
  Specification (EpochState ConwayEra)
epochStateSpec :: Term EpochNo -> Specification (EpochState ConwayEra)
epochStateSpec Term EpochNo
epochNo = (Term (EpochState ConwayEra) -> Pred)
-> Specification (EpochState ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (EpochState ConwayEra) -> Pred)
 -> Specification (EpochState ConwayEra))
-> (Term (EpochState ConwayEra) -> Pred)
-> Specification (EpochState ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (EpochState ConwayEra)
es ->
  Term (EpochState ConwayEra)
-> FunTy (MapList Term (ProductAsList (EpochState ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (EpochState ConwayEra)
es (FunTy (MapList Term (ProductAsList (EpochState ConwayEra))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (EpochState ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps ChainAccountState
_accountState Term (LedgerState ConwayEra)
ledgerState TermD Deps SnapShots
_snapShots TermD Deps NonMyopic
_nonMyopic ->
    Term (LedgerState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (LedgerState ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (LedgerState ConwayEra)
ledgerState (FunTy (MapList Term (ProductAsList (LedgerState ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (LedgerState ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (UTxOState ConwayEra)
utxoState TermD Deps (ConwayCertState ConwayEra)
certState ->
      Term (UTxOState ConwayEra)
-> FunTy (MapList Term (ProductAsList (UTxOState ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (UTxOState ConwayEra)
utxoState (FunTy (MapList Term (ProductAsList (UTxOState ConwayEra))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (UTxOState ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps (UTxO ConwayEra)
_utxo TermD Deps Coin
_deposited TermD Deps Coin
_fees Term (ConwayGovState ConwayEra)
govState TermD Deps (ConwayInstantStake ConwayEra)
_stakeDistr TermD Deps Coin
_donation ->
        Term (ConwayGovState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ConwayGovState ConwayEra))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ConwayGovState ConwayEra)
govState (FunTy
   (MapList Term (ProductAsList (ConwayGovState ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayGovState ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Proposals ConwayEra)
[var|proposals|] TermD Deps (StrictMaybe (Committee ConwayEra))
_committee Term (Constitution ConwayEra)
constitution TermD Deps (PParams ConwayEra)
_curPParams TermD Deps (PParams ConwayEra)
_prevPParams TermD Deps (FuturePParams ConwayEra)
_futPParams Term (DRepPulsingState ConwayEra)
drepPulsingState ->
          [ Term (Constitution ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (Constitution ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Constitution ConwayEra)
constitution (FunTy (MapList Term (ProductAsList (Constitution ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (Constitution ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps Anchor
_ Term (StrictMaybe ScriptHash)
policy ->
              Term (Proposals ConwayEra)
proposals Term (Proposals ConwayEra)
-> Specification (Proposals ConwayEra) -> Pred
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 (CertState ConwayEra)
TermD Deps (ConwayCertState ConwayEra)
certState
          , Term (DRepPulsingState ConwayEra)
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (DRepPulsingState ConwayEra))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn
              Term (DRepPulsingState ConwayEra)
drepPulsingState
              -- DRPulsing
              ( FunTy
  (MapList
     Term
     (Args (DRepPulser ConwayEra Identity (RatifyState ConwayEra))))
  Pred
-> Weighted
     (BinderD Deps)
     (DRepPulser ConwayEra Identity (RatifyState ConwayEra))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args (DRepPulser ConwayEra Identity (RatifyState ConwayEra))))
   Pred
 -> Weighted
      (BinderD Deps)
      (DRepPulser ConwayEra Identity (RatifyState ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args (DRepPulser ConwayEra Identity (RatifyState ConwayEra))))
     Pred
-> Weighted
     (BinderD Deps)
     (DRepPulser ConwayEra Identity (RatifyState ConwayEra))
forall a b. (a -> b) -> a -> b
$ \Term (DRepPulser ConwayEra Identity (RatifyState ConwayEra))
pulser ->
                  Term (DRepPulser ConwayEra Identity (RatifyState ConwayEra))
-> FunTy
     (MapList
        Term
        (ProductAsList
           (DRepPulser ConwayEra Identity (RatifyState ConwayEra))))
     [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (DRepPulser ConwayEra Identity (RatifyState ConwayEra))
pulser (FunTy
   (MapList
      Term
      (ProductAsList
         (DRepPulser ConwayEra Identity (RatifyState ConwayEra))))
   [Pred]
 -> Pred)
-> FunTy
     (MapList
        Term
        (ProductAsList
           (DRepPulser ConwayEra Identity (RatifyState ConwayEra))))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps Int
_size TermD Deps UMap
_stakeMap TermD Deps Int
_index TermD Deps (ConwayInstantStake ConwayEra)
_stakeDistr TermD Deps PoolDistr
_stakePoolDistr TermD Deps (Map DRep (CompactForm Coin))
_drepDistr TermD Deps (Map (Credential 'DRepRole) DRepState)
_drepState Term EpochNo
pulseEpoch TermD Deps (CommitteeState ConwayEra)
_committeeState TermD Deps (EnactState ConwayEra)
_enactState Term (StrictSeq (GovActionState ConwayEra))
pulseProposals TermD Deps (Map (Credential 'Staking) (CompactForm Coin))
_proposalDeposits TermD Deps (Map (KeyHash 'StakePool) PoolParams)
_poolParams ->
                    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term EpochNo
pulseEpoch Term EpochNo -> Term EpochNo -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term EpochNo
epochNo
                    , Term (StrictSeq (GovActionState ConwayEra))
-> (Term (GovActionState ConwayEra) -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (StrictSeq (GovActionState ConwayEra))
pulseProposals ((Term (GovActionState ConwayEra) -> Pred) -> Pred)
-> (Term (GovActionState ConwayEra) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (GovActionState ConwayEra)
gas ->
                        Term (GovActionState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (GovActionState ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (GovActionState ConwayEra)
gas (FunTy
   (MapList Term (ProductAsList (GovActionState ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (GovActionState ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term GovActionId
gasId TermD Deps (Map (Credential 'HotCommitteeRole) Vote)
_ TermD Deps (Map (Credential 'DRepRole) Vote)
_ TermD Deps (Map (KeyHash 'StakePool) Vote)
_ TermD Deps (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
                      Bool -> Pred
forall p. IsPred p => p -> Pred
assert Bool
False
                    ]
              )
              -- DRComplete
              ( FunTy
  (MapList
     Term
     (Args (Prod (PulsingSnapshot ConwayEra) (RatifyState ConwayEra))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod (PulsingSnapshot ConwayEra) (RatifyState ConwayEra))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args (Prod (PulsingSnapshot ConwayEra) (RatifyState ConwayEra))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod (PulsingSnapshot ConwayEra) (RatifyState ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args (Prod (PulsingSnapshot ConwayEra) (RatifyState ConwayEra))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod (PulsingSnapshot ConwayEra) (RatifyState ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (PulsingSnapshot ConwayEra)
_snap Term (RatifyState ConwayEra)
ratifyState ->
                  Term (RatifyState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (RatifyState ConwayEra))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (RatifyState ConwayEra)
ratifyState (FunTy
   (MapList Term (ProductAsList (RatifyState ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (RatifyState ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps (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.
                      Term (Proposals ConwayEra)
-> (Proposals ConwayEra -> Integer)
-> (Term Integer -> [Pred])
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Proposals ConwayEra)
proposals (Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer)
-> (Proposals ConwayEra -> Int) -> Proposals ConwayEra -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proposals ConwayEra -> Int
forall era. Proposals era -> Int
proposalsSize) ((Term Integer -> [Pred]) -> Pred)
-> (Term Integer -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Integer
[var|sz|] ->
                        [ Term Bool -> Term Bool -> Term Bool -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
                            (Term Integer
sz Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
0)
                            (Term (Set GovActionId)
expired Term (Set GovActionId) -> Term (Set GovActionId) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (Set GovActionId)
forall a. Monoid a => a
mempty)
                            (Term (Set GovActionId) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Set GovActionId)
expired Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Integer
sz)
                        ]
                    , Term (Set GovActionId) -> (Term GovActionId -> Pred) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Set GovActionId)
expired ((Term GovActionId -> Pred) -> Pred)
-> (Term GovActionId -> Pred) -> Pred
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
                      Term (Seq (GovActionState ConwayEra))
-> (Term (GovActionState ConwayEra) -> [Pred]) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Seq (GovActionState ConwayEra))
enacted ((Term (GovActionState ConwayEra) -> [Pred]) -> Pred)
-> (Term (GovActionState ConwayEra) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (GovActionState ConwayEra)
[var|govact|] ->
                        [ Term (Proposals ConwayEra)
-> (Proposals ConwayEra -> [GovActionState ConwayEra])
-> (Term [GovActionState ConwayEra] -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Proposals ConwayEra)
proposals Proposals ConwayEra -> [GovActionState ConwayEra]
forall era. Proposals era -> [GovActionState era]
enactableProposals ((Term [GovActionState ConwayEra] -> Term Bool) -> Pred)
-> (Term [GovActionState ConwayEra] -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term [GovActionState ConwayEra]
[var|enactable|] -> Term (GovActionState ConwayEra)
govact Term (GovActionState ConwayEra)
-> Term [GovActionState ConwayEra] -> Term Bool
forall a. HasSpec a => Term a -> Term [a] -> Term Bool
`elem_` Term [GovActionState ConwayEra]
enactable
                        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term Bool -> Term Bool) -> Term Bool -> Term Bool
forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra) -> Term GovActionId
gasId_ Term (GovActionState ConwayEra)
govact Term GovActionId -> Term (Set GovActionId) -> Term Bool
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!
                      Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Seq (GovActionState ConwayEra)) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Seq (GovActionState ConwayEra))
enacted Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Integer
1
                    , TermD Deps (EnactState ConwayEra)
-> FunTy (MapList Term (ProductAsList (EnactState ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match TermD Deps (EnactState ConwayEra)
enactState (FunTy (MapList Term (ProductAsList (EnactState ConwayEra))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (EnactState ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$
                        \TermD Deps (StrictMaybe (Committee ConwayEra))
_cc Term (Constitution ConwayEra)
_con TermD Deps (PParams ConwayEra)
_cpp TermD Deps (PParams ConwayEra)
_ppp TermD Deps Coin
_tr TermD Deps (Map (Credential 'Staking) Coin)
_wth Term (GovRelation StrictMaybe)
prevGACTIDS ->
                          Term (Proposals ConwayEra)
-> (Proposals ConwayEra -> GovRelation StrictMaybe)
-> (Term (GovRelation StrictMaybe) -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Proposals ConwayEra)
proposals (GovRelation PRoot -> GovRelation StrictMaybe
toPrevGovActionIds (GovRelation PRoot -> GovRelation StrictMaybe)
-> (Proposals ConwayEra -> GovRelation PRoot)
-> Proposals ConwayEra
-> GovRelation StrictMaybe
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Getting
  (GovRelation PRoot) (Proposals ConwayEra) (GovRelation PRoot)
-> Proposals ConwayEra -> GovRelation PRoot
forall a s. Getting a s a -> s -> a
view Getting
  (GovRelation PRoot) (Proposals ConwayEra) (GovRelation PRoot)
forall era (f :: * -> *).
Functor f =>
(GovRelation PRoot -> f (GovRelation PRoot))
-> Proposals era -> f (Proposals era)
pRootsL) (Term (GovRelation StrictMaybe)
prevGACTIDS Term (GovRelation StrictMaybe)
-> Term (GovRelation StrictMaybe) -> Term Bool
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 =
  Term (Proposals ConwayEra)
-> (Proposals ConwayEra
    -> Map GovActionId (GovActionState ConwayEra))
-> (Term (Map GovActionId (GovActionState ConwayEra)) -> Term Bool)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Proposals ConwayEra)
proposals Proposals ConwayEra -> Map GovActionId (GovActionState ConwayEra)
forall era. Proposals era -> Map GovActionId (GovActionState era)
proposalsActionsMap ((Term (Map GovActionId (GovActionState ConwayEra)) -> Term Bool)
 -> Pred)
-> (Term (Map GovActionId (GovActionState ConwayEra)) -> Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map GovActionId (GovActionState ConwayEra))
[var|actionMap|] ->
    Term GovActionId
gasId Term GovActionId
-> Term (Map GovActionId (GovActionState ConwayEra)) -> Term Bool
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term k -> Term (Map k v) -> Term Bool
`mapMember_` Term (Map GovActionId (GovActionState ConwayEra))
actionMap

epochSignalSpec :: EpochNo -> Specification EpochNo
epochSignalSpec :: EpochNo -> Specification EpochNo
epochSignalSpec EpochNo
curEpoch = (Term EpochNo -> Term Bool) -> Specification EpochNo
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term EpochNo -> Term Bool) -> Specification EpochNo)
-> (Term EpochNo -> Term Bool) -> Specification EpochNo
forall a b. (a -> b) -> a -> b
$ \Term EpochNo
e ->
  Term EpochNo -> Term [EpochNo] -> Term Bool
forall a. HasSpec a => Term a -> Term [a] -> Term Bool
elem_ Term EpochNo
e ([EpochNo] -> Term [EpochNo]
forall a. HasSpec a => a -> Term a
lit [EpochNo
curEpoch, EpochNo -> EpochNo
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 <- StrictSeq (GovActionState era) -> [GovActionState era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (Proposals era -> StrictSeq (GovActionState era)
forall era. Proposals era -> StrictSeq (GovActionState era)
proposalsActions Proposals era
proposals)
  , GovActionState era
gact' <- GovActionState era
-> [GovActionState era]
-> (forall {p :: GovActionPurpose}.
    (forall (f1 :: * -> *) (f2 :: * -> *).
     Functor f2 =>
     (f1 (GovPurposeId p) -> f2 (f1 (GovPurposeId p)))
     -> GovRelation f1 -> f2 (GovRelation f1))
    -> StrictMaybe (GovPurposeId p)
    -> GovPurposeId p
    -> [GovActionState era])
-> [GovActionState era]
forall era a.
GovActionState era
-> a
-> (forall (p :: GovActionPurpose).
    (forall (f1 :: * -> *) (f2 :: * -> *).
     Functor f2 =>
     (f1 (GovPurposeId p) -> f2 (f1 (GovPurposeId p)))
     -> GovRelation f1 -> f2 (GovRelation f1))
    -> StrictMaybe (GovPurposeId p) -> GovPurposeId p -> a)
-> a
withGovActionParent GovActionState era
gact [GovActionState era
gact] ((forall {p :: GovActionPurpose}.
  (forall (f1 :: * -> *) (f2 :: * -> *).
   Functor f2 =>
   (f1 (GovPurposeId p) -> f2 (f1 (GovPurposeId p)))
   -> GovRelation f1 -> f2 (GovRelation f1))
  -> StrictMaybe (GovPurposeId p)
  -> GovPurposeId p
  -> [GovActionState era])
 -> [GovActionState era])
-> (forall {p :: GovActionPurpose}.
    (forall (f1 :: * -> *) (f2 :: * -> *).
     Functor f2 =>
     (f1 (GovPurposeId p) -> f2 (f1 (GovPurposeId p)))
     -> GovRelation f1 -> f2 (GovRelation f1))
    -> StrictMaybe (GovPurposeId p)
    -> GovPurposeId p
    -> [GovActionState era])
-> [GovActionState era]
forall a b. (a -> b) -> a -> b
$
      \forall (f1 :: * -> *) (f2 :: * -> *).
Functor f2 =>
(f1 (GovPurposeId p) -> f2 (f1 (GovPurposeId p)))
-> GovRelation f1 -> f2 (GovRelation f1)
_ StrictMaybe (GovPurposeId p)
mparent GovPurposeId p
_ ->
        case StrictMaybe (GovPurposeId p)
mparent of
          StrictMaybe (GovPurposeId p)
SNothing -> [GovActionState era
gact]
          SJust (GovPurposeId GovActionId
gpid')
            | GovActionId -> Proposals era -> Bool
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 (Getting (GovRelation PRoot) (Proposals era) (GovRelation PRoot)
-> Proposals era -> GovRelation PRoot
forall a s. Getting a s a -> s -> a
view Getting (GovRelation PRoot) (Proposals era) (GovRelation PRoot)
forall era (f :: * -> *).
Functor f =>
(GovRelation PRoot -> f (GovRelation PRoot))
-> Proposals era -> f (Proposals era)
pRootsL -> GovRelation {PRoot (GovPurposeId 'PParamUpdatePurpose)
PRoot (GovPurposeId 'HardForkPurpose)
PRoot (GovPurposeId 'CommitteePurpose)
PRoot (GovPurposeId 'ConstitutionPurpose)
grPParamUpdate :: PRoot (GovPurposeId 'PParamUpdatePurpose)
grHardFork :: PRoot (GovPurposeId 'HardForkPurpose)
grCommittee :: PRoot (GovPurposeId 'CommitteePurpose)
grConstitution :: PRoot (GovPurposeId 'ConstitutionPurpose)
grPParamUpdate :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'PParamUpdatePurpose)
grHardFork :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'HardForkPurpose)
grCommittee :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'CommitteePurpose)
grConstitution :: forall (f :: * -> *).
GovRelation f -> f (GovPurposeId 'ConstitutionPurpose)
..}) =
  GovActionId -> StrictMaybe GovActionId
forall a. a -> StrictMaybe a
SJust GovActionId
gid
    StrictMaybe GovActionId -> [StrictMaybe GovActionId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PRoot (GovPurposeId 'PParamUpdatePurpose)
-> StrictMaybe GovActionId
forall {p :: GovActionPurpose}.
PRoot (GovPurposeId p) -> StrictMaybe GovActionId
getGID PRoot (GovPurposeId 'PParamUpdatePurpose)
grPParamUpdate, PRoot (GovPurposeId 'HardForkPurpose) -> StrictMaybe GovActionId
forall {p :: GovActionPurpose}.
PRoot (GovPurposeId p) -> StrictMaybe GovActionId
getGID PRoot (GovPurposeId 'HardForkPurpose)
grHardFork, PRoot (GovPurposeId 'CommitteePurpose) -> StrictMaybe GovActionId
forall {p :: GovActionPurpose}.
PRoot (GovPurposeId p) -> StrictMaybe GovActionId
getGID PRoot (GovPurposeId 'CommitteePurpose)
grCommittee, PRoot (GovPurposeId 'ConstitutionPurpose)
-> StrictMaybe GovActionId
forall {p :: GovActionPurpose}.
PRoot (GovPurposeId p) -> StrictMaybe GovActionId
getGID PRoot (GovPurposeId 'ConstitutionPurpose)
grConstitution]
  where
    getGID :: PRoot (GovPurposeId p) -> StrictMaybe GovActionId
getGID = (GovPurposeId p -> GovActionId)
-> StrictMaybe (GovPurposeId p) -> StrictMaybe GovActionId
forall a b. (a -> b) -> StrictMaybe a -> StrictMaybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap GovPurposeId p -> GovActionId
forall (p :: GovActionPurpose). GovPurposeId p -> GovActionId
unGovPurposeId (StrictMaybe (GovPurposeId p) -> StrictMaybe GovActionId)
-> (PRoot (GovPurposeId p) -> StrictMaybe (GovPurposeId p))
-> PRoot (GovPurposeId p)
-> StrictMaybe GovActionId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRoot (GovPurposeId p) -> StrictMaybe (GovPurposeId p)
forall a. PRoot a -> StrictMaybe a
prRoot