{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

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

import Cardano.Ledger.BaseTypes
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Conway.State
import Cardano.Ledger.Shelley.HardForks qualified as HardForks
import Cardano.Ledger.UMap (umElems, umElemsL)
import Constrained.API
import Constrained.Base (IsPred (..))
import Constrained.Spec.Tree (rootLabel_)
import Data.Coerce
import Data.Foldable
import Data.Map qualified as Map
import Data.Set qualified as Set
import Lens.Micro
import Lens.Micro qualified as L
import Test.Cardano.Ledger.Constrained.Conway.Instances
import Test.Cardano.Ledger.Constrained.Conway.PParams

govEnvSpec ::
  Specification (GovEnv ConwayEra)
govEnvSpec :: Specification (GovEnv ConwayEra)
govEnvSpec = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (GovEnv ConwayEra)
ge ->
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (GovEnv ConwayEra)
ge forall a b. (a -> b) -> a -> b
$ \Term TxId
_ Term EpochNo
_ Term (PParams ConwayEra)
pp Term (StrictMaybe ScriptHash)
_ Term (ConwayCertState ConwayEra)
_ ->
    forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParams ConwayEra)
pp forall era. EraSpecPParams era => Specification (PParams era)
pparamsSpec

-- NOTE: it is probably OK not to check uniqueness of ids here, because a clash
-- is never going to be generated, and the real representation of `Proposals` doesn't
-- allow the id to appear twice.
govProposalsSpec ::
  GovEnv ConwayEra ->
  Specification (Proposals ConwayEra)
govProposalsSpec :: GovEnv ConwayEra -> Specification (Proposals ConwayEra)
govProposalsSpec GovEnv {EpochNo
geEpoch :: forall era. GovEnv era -> EpochNo
geEpoch :: EpochNo
geEpoch, StrictMaybe ScriptHash
gePPolicy :: forall era. GovEnv era -> StrictMaybe ScriptHash
gePPolicy :: StrictMaybe ScriptHash
gePPolicy, CertState ConwayEra
geCertState :: forall era. GovEnv era -> CertState era
geCertState :: CertState ConwayEra
geCertState} =
  Term EpochNo
-> Term (StrictMaybe ScriptHash)
-> Term (CertState ConwayEra)
-> Specification (Proposals ConwayEra)
proposalsSpec (forall a. HasSpec a => a -> Term a
lit EpochNo
geEpoch) (forall a. HasSpec a => a -> Term a
lit StrictMaybe ScriptHash
gePPolicy) (forall a. HasSpec a => a -> Term a
lit CertState ConwayEra
geCertState)

proposalsSpec ::
  Term EpochNo ->
  Term (StrictMaybe ScriptHash) ->
  Term (CertState ConwayEra) ->
  Specification (Proposals ConwayEra)
proposalsSpec :: Term EpochNo
-> Term (StrictMaybe ScriptHash)
-> Term (CertState ConwayEra)
-> Specification (Proposals ConwayEra)
proposalsSpec Term EpochNo
geEpoch Term (StrictMaybe ScriptHash)
gePPolicy Term (CertState ConwayEra)
geCertState =
  forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (Proposals ConwayEra)
[var|props|] ->
    -- Note each of ppupTree, hardForkTree, committeeTree, constitutionTree
    -- have the pair type ProposalTree = (StrictMaybe (GovActionId StandardCrypto), [Tree GAS])
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Proposals ConwayEra)
props forall a b. (a -> b) -> a -> b
$ \ Term (ProposalTree ConwayEra)
[var|ppupTree|] Term (ProposalTree ConwayEra)
[var|hardForkTree|] Term (ProposalTree ConwayEra)
[var|committeeTree|] Term (ProposalTree ConwayEra)
[var|constitutionTree|] Term [GovActionState ConwayEra]
[var|unorderedProposals|] ->
      [ -- Protocol parameter updates
        Term (ProposalTree ConwayEra) -> Pred
wellFormedChildren Term (ProposalTree ConwayEra)
ppupTree
      , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
          Term (ProposalTree ConwayEra)
ppupTree
          ( forall p.
IsPred p =>
(Term (GovActionState ConwayEra) -> p)
-> Specification (ProposalTree ConwayEra)
allGASInTree
              ( \ Term (GovActionState ConwayEra)
[var|gasPpup|] ->
                  -- Extract the GovAction from the GovActionID and match against the constructor ParameterChange
                  [ forall (c :: Symbol) a.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a,
 HasSpec (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> Pred
isCon @"ParameterChange" (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasPpup)
                  , forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a,
 HasSpec (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"ParameterChange" (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasPpup) forall a b. (a -> b) -> a -> b
$
                      \Term (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
_ Term (PParamsUpdate ConwayEra)
ppup Term (StrictMaybe ScriptHash)
policy ->
                        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (PParamsUpdate ConwayEra)
ppup forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit forall era. EraPParams era => PParamsUpdate era
emptyPParamsUpdate
                        , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParamsUpdate ConwayEra)
ppup Specification (PParamsUpdate ConwayEra)
wfPParamsUpdateSpec
                        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe ScriptHash)
policy forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (StrictMaybe ScriptHash)
gePPolicy
                        ]
                  ]
              )
          )
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
ppupTree) (forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer, Integer)
treeGenHint)
      , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
listSizeHint (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
ppupTree)
      , -- Hard forks
        Term (ProposalTree ConwayEra) -> Pred
wellFormedChildren Term (ProposalTree ConwayEra)
hardForkTree
      , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
          Term (ProposalTree ConwayEra)
hardForkTree
          ( forall p.
IsPred p =>
(Term (GovActionState ConwayEra) -> p)
-> Specification (ProposalTree ConwayEra)
allGASInTree
              ( \ Term (GovActionState ConwayEra)
[var|gasHfork|] ->
                  -- Extract the GovAction from the GovActionID and match against the constructor HardForkInitiation
                  forall (c :: Symbol) a.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a,
 HasSpec (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> Pred
isCon @"HardForkInitiation" (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasHfork)
              )
          )
      , forall p.
IsPred p =>
Term (ProposalTree ConwayEra)
-> (Term (GovActionState ConwayEra)
    -> Term (GovActionState ConwayEra) -> p)
-> Pred
allGASAndChildInTree Term (ProposalTree ConwayEra)
hardForkTree forall a b. (a -> b) -> a -> b
$ \Term (GovActionState ConwayEra)
gas Term (GovActionState ConwayEra)
gas' ->
          [ forall p.
IsPred p =>
Term (GovActionState ConwayEra)
-> (Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
    -> Term ProtVer -> p)
-> Pred
onHardFork Term (GovActionState ConwayEra)
gas forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
_ Term ProtVer
pv ->
              forall p.
IsPred p =>
Term (GovActionState ConwayEra)
-> (Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
    -> Term ProtVer -> p)
-> Pred
onHardFork Term (GovActionState ConwayEra)
gas' forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
_ Term ProtVer
pv' ->
                forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ProtVer
pv forall a b. (a -> b) -> a -> b
$ \Term Version
majV Term Natural
minV ->
                  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ProtVer
pv' forall a b. (a -> b) -> a -> b
$ \Term Version
majV' Term Natural
minV' ->
                    [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Version
majV forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Version
majV'
                    , forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
                        (Term Version
majV forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall a. Bounded a => a
maxBound)
                        (Term Version
majV' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Version
majV)
                        (Term Version
majV' forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Version -> Term Version
succV_ Term Version
majV)
                    , forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
                        (Term Version
majV forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Version
majV')
                        (Term Natural
minV' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
minV forall a. Num a => a -> a -> a
+ Term Natural
1)
                        (Term Natural
minV' forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
0)
                    ]
          ]
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
hardForkTree) (forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer, Integer)
treeGenHint)
      , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
listSizeHint (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
hardForkTree)
      , -- Committee
        Term (ProposalTree ConwayEra) -> Pred
wellFormedChildren Term (ProposalTree ConwayEra)
committeeTree
      , -- TODO: it would be nice to have a trick like `isCon` that can
        -- do disjunction without having to write down all the cases.
        forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
          Term (ProposalTree ConwayEra)
committeeTree
          ( forall p.
IsPred p =>
(Term (GovActionState ConwayEra) -> p)
-> Specification (ProposalTree ConwayEra)
allGASInTree
              ( \ Term (GovActionState ConwayEra)
[var|gasComm|] ->
                  -- Extract the GovAction from the GovActionID and case on it
                  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 (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasComm)
                    (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 (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
_ Term (PParamsUpdate ConwayEra)
_ Term (StrictMaybe ScriptHash)
_ -> Bool
False)
                    (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 (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
_ Term ProtVer
_ -> Bool
False)
                    (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 (Map RewardAccount Coin)
_ Term (StrictMaybe ScriptHash)
_ -> Bool
False)
                    (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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ -> Bool
True)
                    -- UpdateCommittee - We are only interested in this case
                    ( 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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ Term (Set (Credential 'ColdCommitteeRole))
_ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
added Term UnitInterval
_ ->
                        forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
added) forall a b. (a -> b) -> a -> b
$ \Term EpochNo
epoch ->
                          Term EpochNo
geEpoch forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term EpochNo
epoch
                    )
                    (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 (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
_ Term (Constitution ConwayEra)
_ -> Bool
False)
                    (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 ()
_ -> Bool
False)
              )
          )
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
committeeTree) (forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer, Integer)
treeGenHint)
      , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
listSizeHint (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
committeeTree)
      , -- Constitution
        Term (ProposalTree ConwayEra) -> Pred
wellFormedChildren Term (ProposalTree ConwayEra)
constitutionTree
      , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
          Term (ProposalTree ConwayEra)
constitutionTree
          ( forall p.
IsPred p =>
(Term (GovActionState ConwayEra) -> p)
-> Specification (ProposalTree ConwayEra)
allGASInTree -- Extract the GovAction from the GovActionID and match against the constructor NewConstitution
              ( \ Term (GovActionState ConwayEra)
[var|gasNewConst|] -> forall (c :: Symbol) a.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a,
 HasSpec (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> Pred
isCon @"NewConstitution" (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasNewConst)
              )
          )
      , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
constitutionTree) (forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer, Integer)
treeGenHint)
      , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
listSizeHint (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
constitutionTree)
      , -- TreasuryWithdrawals and InfoAction, Recall,  unorderedProposals :: [GAS]
        -- for each GAS in the list, match against the constructor
        forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [GovActionState ConwayEra]
unorderedProposals forall a b. (a -> b) -> a -> b
$ \ Term (GovActionState ConwayEra)
[var|gasOther|] ->
          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 (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasOther)
            (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 (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
_ Term (PParamsUpdate ConwayEra)
_ Term (StrictMaybe ScriptHash)
_ -> Bool
False) -- Parameter Change
            (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 (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
_ Term ProtVer
_ -> Bool
False) -- HardForkInitiation
            -- Treasury Withdrawal
            ( 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 (Map RewardAccount Coin)
[var|withdrawMap|] Term (StrictMaybe ScriptHash)
[var|policy|] ->
                NonEmpty String -> Pred -> Pred
Explain (forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"TreasuryWithdrawal fails") forall a b. (a -> b) -> a -> b
$
                  [Pred] -> Pred
And
                    [ forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (GovActionState ConwayEra)
gasOther Term (Map RewardAccount Coin)
withdrawMap
                    , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CertState ConwayEra)
geCertState forall a b. (a -> b) -> a -> b
$ \Term (VState ConwayEra)
_vState Term (PState ConwayEra)
_pState Term (DState ConwayEra)
[var|dState|] ->
                        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (DState ConwayEra)
dState forall a b. (a -> b) -> a -> b
$ \ Term UMap
[var|rewardMap|] Term (Map FutureGenDeleg GenDelegPair)
_ Term GenDelegs
_ Term InstantaneousRewards
_ ->
                          forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term UMap
rewardMap (forall k a. Map k a -> Set k
Map.keysSet forall b c a. (b -> c) -> (a -> b) -> a -> c
. UMap -> Map (Credential 'Staking) UMElem
umElems) forall a b. (a -> b) -> a -> b
$ \ Term (Set (Credential 'Staking))
[var|registeredCredentials|] ->
                            forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (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 RewardAccount Coin)
withdrawMap) forall a b. (a -> b) -> a -> b
$ \ Term RewardAccount
[var|rewAcnt|] ->
                              forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
rewAcnt forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|network|] Term (Credential 'Staking)
[var|credential|] ->
                                [ Term Network
network forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Network
Testnet
                                , Term (Credential 'Staking)
credential forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Term (Set (Credential 'Staking))
registeredCredentials
                                ]
                    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe ScriptHash)
policy forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (StrictMaybe ScriptHash)
gePPolicy
                    ]
            )
            (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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ -> Bool
False) -- NoConfidence
            (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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ Term (Set (Credential 'ColdCommitteeRole))
_ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
_ Term UnitInterval
_ -> Bool
False) -- Update Committee
            (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 (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
_ Term (Constitution ConwayEra)
_ -> Bool
False) -- NewConstitution
            -- Info
            (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 ()
_ -> Bool
True) -- InfoAction
      , forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
listSizeHint Term [GovActionState ConwayEra]
unorderedProposals
      ]
  where
    treeGenHint :: (Maybe Integer, Integer)
treeGenHint = (forall a. a -> Maybe a
Just Integer
2, Integer
6)
    listSizeHint :: Integer
listSizeHint = Integer
5

allGASInTree ::
  IsPred p =>
  (Term (GovActionState ConwayEra) -> p) ->
  Specification (ProposalTree ConwayEra)
allGASInTree :: forall p.
IsPred p =>
(Term (GovActionState ConwayEra) -> p)
-> Specification (ProposalTree ConwayEra)
allGASInTree Term (GovActionState ConwayEra) -> p
k = forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \ Term (ProposalTree ConwayEra)
[var|proposalTree|] ->
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
proposalTree) forall a b. (a -> b) -> a -> b
$ \ Term (Tree (GovActionState ConwayEra))
[var|subtree|] ->
    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 (Tree (GovActionState ConwayEra))
subtree forall a b. (a -> b) -> a -> b
$ \ Term (GovActionState ConwayEra)
[var|gas|] Term [Tree (GovActionState ConwayEra)]
_ ->
      Term (GovActionState ConwayEra) -> p
k Term (GovActionState ConwayEra)
gas

allGASAndChildInTree ::
  IsPred p =>
  Term (ProposalTree ConwayEra) ->
  ( Term (GovActionState ConwayEra) ->
    Term (GovActionState ConwayEra) ->
    p
  ) ->
  Pred
allGASAndChildInTree :: forall p.
IsPred p =>
Term (ProposalTree ConwayEra)
-> (Term (GovActionState ConwayEra)
    -> Term (GovActionState ConwayEra) -> p)
-> Pred
allGASAndChildInTree Term (ProposalTree ConwayEra)
t Term (GovActionState ConwayEra)
-> Term (GovActionState ConwayEra) -> p
k =
  forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
t) forall a b. (a -> b) -> a -> b
$ \ Term (Tree (GovActionState ConwayEra))
[var|subtree|] ->
    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 (Tree (GovActionState ConwayEra))
subtree forall a b. (a -> b) -> a -> b
$ \ Term (GovActionState ConwayEra)
[var|gas|] Term [Tree (GovActionState ConwayEra)]
[var|cs|] ->
      forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree (GovActionState ConwayEra)]
cs forall a b. (a -> b) -> a -> b
$ \ Term (Tree (GovActionState ConwayEra))
[var|t''|] ->
        Term (GovActionState ConwayEra)
-> Term (GovActionState ConwayEra) -> p
k Term (GovActionState ConwayEra)
gas (forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree (GovActionState ConwayEra))
t'')

wellFormedChildren ::
  Term (ProposalTree ConwayEra) ->
  Pred
wellFormedChildren :: Term (ProposalTree ConwayEra) -> Pred
wellFormedChildren Term (ProposalTree ConwayEra)
rootAndTrees =
  forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ProposalTree ConwayEra)
rootAndTrees forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe GovActionId)
root Term [Tree (GovActionState ConwayEra)]
trees ->
    [ forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (ProposalTree ConwayEra)
rootAndTrees Term (StrictMaybe GovActionId)
root
    , forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (ProposalTree ConwayEra)
rootAndTrees Term [Tree (GovActionState ConwayEra)]
trees
    , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree (GovActionState ConwayEra)]
trees forall a b. (a -> b) -> a -> b
$ \Term (Tree (GovActionState ConwayEra))
t ->
        [ -- Every node just below the root has the root as its parent
          Term (GovActionState ConwayEra)
-> (Term (StrictMaybe GovActionId) -> Pred) -> Pred
withPrevActId (forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree (GovActionState ConwayEra))
t) (forall p. IsPred p => p -> Pred
assert forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term (StrictMaybe GovActionId)
root))
        , -- Every node's children have the id of the node as its parent
          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 (Tree (GovActionState ConwayEra))
t forall a b. (a -> b) -> a -> b
$ \Term (GovActionState ConwayEra)
gas Term [Tree (GovActionState ConwayEra)]
children ->
            [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [Tree (GovActionState ConwayEra)]
children forall a b. (a -> b) -> a -> b
$ \Term (Tree (GovActionState ConwayEra))
t' ->
                [ Term (GovActionState ConwayEra)
-> (Term (StrictMaybe GovActionId) -> Pred) -> Pred
withPrevActId (forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree (GovActionState ConwayEra))
t') (forall p. IsPred p => p -> Pred
assert forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ (Term (GovActionState ConwayEra) -> Term GovActionId
gasId_ Term (GovActionState ConwayEra)
gas)))
                -- TODO: figure out why this causes a crash!
                -- , t' `dependsOn` gas
                ]
            , Term [Tree (GovActionState ConwayEra)]
children forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (GovActionState ConwayEra)
gas
            ]
        ]
    ]

withPrevActId ::
  Term (GovActionState ConwayEra) ->
  (Term (StrictMaybe GovActionId) -> Pred) ->
  Pred
withPrevActId :: Term (GovActionState ConwayEra)
-> (Term (StrictMaybe GovActionId) -> Pred) -> Pred
withPrevActId Term (GovActionState ConwayEra)
gas Term (StrictMaybe GovActionId) -> Pred
k =
  [Pred] -> Pred
And
    [ forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match (Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ Term (GovActionState ConwayEra)
gas) forall a b. (a -> b) -> a -> b
$ \Term Coin
_deposit Term RewardAccount
[var|retAddr|] Term (GovAction ConwayEra)
_action Term Anchor
_anchor ->
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
retAddr forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|net|] Term (Credential 'Staking)
_ -> [forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (GovActionState ConwayEra)
gas Term Network
net, forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Network
net forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Network
Testnet]
    , 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 (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gas)
        -- ParameterChange
        ( 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 (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
mPrevActionId Term (PParamsUpdate ConwayEra)
_ Term (StrictMaybe ScriptHash)
_ ->
            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 (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
mPrevActionId
              (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 ()
_ -> Term (StrictMaybe GovActionId) -> Pred
k forall a. (HasSpec a, IsNormalType a) => Term (StrictMaybe a)
cSNothing_)
              (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 (GovPurposeId 'PParamUpdatePurpose ConwayEra)
i -> Term (StrictMaybe GovActionId) -> Pred
k (forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ forall a b. (a -> b) -> a -> b
$ forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (GovPurposeId 'PParamUpdatePurpose ConwayEra)
i))
        )
        -- HardForkInitiation
        ( 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 (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
mPrevActionId Term ProtVer
_ ->
            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 (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
mPrevActionId
              (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 ()
_ -> Term (StrictMaybe GovActionId) -> Pred
k forall a. (HasSpec a, IsNormalType a) => Term (StrictMaybe a)
cSNothing_)
              (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 (GovPurposeId 'HardForkPurpose ConwayEra)
i -> Term (StrictMaybe GovActionId) -> Pred
k (forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ forall a b. (a -> b) -> a -> b
$ forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (GovPurposeId 'HardForkPurpose ConwayEra)
i))
        )
        -- TreasuryWithdrawals
        (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 (Map RewardAccount Coin)
_ Term (StrictMaybe ScriptHash)
_ -> Bool
True)
        -- NoConfidence
        --   !(StrictMaybe (PrevGovActionId 'CommitteePurpose (EraCrypto era)))
        ( 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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId ->
            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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId
              (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 ()
_ -> Term (StrictMaybe GovActionId) -> Pred
k forall a. (HasSpec a, IsNormalType a) => Term (StrictMaybe a)
cSNothing_)
              (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 (GovPurposeId 'CommitteePurpose ConwayEra)
i -> Term (StrictMaybe GovActionId) -> Pred
k (forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ forall a b. (a -> b) -> a -> b
$ forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (GovPurposeId 'CommitteePurpose ConwayEra)
i))
        )
        -- UpdateCommittee
        --   !(StrictMaybe (PrevGovActionId 'CommitteePurpose (EraCrypto era)))
        --   !(Set (Credential 'ColdCommitteeRole (EraCrypto era)))
        --   !(Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo)
        --   !UnitInterval
        ( 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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId Term (Set (Credential 'ColdCommitteeRole))
_ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
_ Term UnitInterval
_ ->
            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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId
              (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 ()
_ -> Term (StrictMaybe GovActionId) -> Pred
k forall a. (HasSpec a, IsNormalType a) => Term (StrictMaybe a)
cSNothing_)
              (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 (GovPurposeId 'CommitteePurpose ConwayEra)
i -> Term (StrictMaybe GovActionId) -> Pred
k (forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ forall a b. (a -> b) -> a -> b
$ forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (GovPurposeId 'CommitteePurpose ConwayEra)
i))
        )
        -- NewConstitution
        --  !(StrictMaybe (PrevGovActionId 'ConstitutionPurpose (EraCrypto era)))
        --  !(Constitution era)
        ( 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 (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
mPrevActionId Term (Constitution ConwayEra)
_ ->
            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 (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
mPrevActionId
              (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 ()
_ -> Term (StrictMaybe GovActionId) -> Pred
k forall a. (HasSpec a, IsNormalType a) => Term (StrictMaybe a)
cSNothing_)
              (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 (GovPurposeId 'ConstitutionPurpose ConwayEra)
i -> Term (StrictMaybe GovActionId) -> Pred
k (forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ forall a b. (a -> b) -> a -> b
$ forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (GovPurposeId 'ConstitutionPurpose ConwayEra)
i))
        )
        -- InfoAction
        (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 ()
_ -> Bool
True)
    ]

onHardFork ::
  IsPred p =>
  Term (GovActionState ConwayEra) ->
  ( Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ->
    Term ProtVer ->
    p
  ) ->
  Pred
onHardFork :: forall p.
IsPred p =>
Term (GovActionState ConwayEra)
-> (Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
    -> Term ProtVer -> p)
-> Pred
onHardFork Term (GovActionState ConwayEra)
gas Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
-> Term ProtVer -> p
k = forall (c :: Symbol) a p.
(IsConstrOf c (ProdOver (ConstrOf c (TheSop a))) (TheSop a),
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSimpleRep a, HasSpec a,
 HasSpec (SimpleRep a),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), IsPred p,
 Args (ProdOver (ConstrOf c (TheSop a))) ~ ConstrOf c (TheSop a),
 All HasSpec (ConstrOf c (TheSop a)),
 IsProd (ProdOver (ConstrOf c (TheSop a)))) =>
Term a -> FunTy (MapList Term (ConstrOf c (TheSop a))) p -> Pred
onCon @"HardForkInitiation" (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gas) Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
-> Term ProtVer -> p
k

govProceduresSpec ::
  GovEnv ConwayEra ->
  Proposals ConwayEra ->
  Specification (GovSignal ConwayEra)
govProceduresSpec :: GovEnv ConwayEra
-> Proposals ConwayEra -> Specification (GovSignal ConwayEra)
govProceduresSpec ge :: GovEnv ConwayEra
ge@GovEnv {CertState ConwayEra
PParams ConwayEra
StrictMaybe ScriptHash
TxId
EpochNo
geTxId :: forall era. GovEnv era -> TxId
gePParams :: forall era. GovEnv era -> PParams era
geCertState :: CertState ConwayEra
gePPolicy :: StrictMaybe ScriptHash
gePParams :: PParams ConwayEra
geEpoch :: EpochNo
geTxId :: TxId
geCertState :: forall era. GovEnv era -> CertState era
gePPolicy :: forall era. GovEnv era -> StrictMaybe ScriptHash
geEpoch :: forall era. GovEnv era -> EpochNo
..} Proposals ConwayEra
ps =
  let actions :: (GovAction ConwayEra -> Bool) -> [GovActionId]
actions GovAction ConwayEra -> Bool
f =
        [ GovActionId
gid
        | (GovActionId
gid, GovActionState ConwayEra
act) <- forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ forall era. Proposals era -> Map GovActionId (GovActionState era)
proposalsActionsMap Proposals ConwayEra
ps
        , EpochNo
geEpoch forall a. Ord a => a -> a -> Bool
<= GovActionState ConwayEra
act forall s a. s -> Getting a s a -> a
^. forall era. Lens' (GovActionState era) EpochNo
gasExpiresAfterL
        , GovAction ConwayEra -> Bool
f (forall era. GovActionState era -> GovAction era
gasAction GovActionState ConwayEra
act)
        ]
      committeeState :: CommitteeState ConwayEra
committeeState = CertState ConwayEra
geCertState forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
certVStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (VState era) (CommitteeState era)
vsCommitteeStateL
      knownDReps :: Set (Credential 'DRepRole)
knownDReps = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
geCertState forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
certVStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
Lens' (VState era) (Map (Credential 'DRepRole) DRepState)
vsDRepsL
      knownStakePools :: Set (KeyHash 'StakePool)
knownStakePools = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
geCertState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (PState era)
certPStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
Lens' (PState era) (Map (KeyHash 'StakePool) PoolParams)
psStakePoolParamsL
      knownCommitteeAuthorizations :: Set (Credential 'HotCommitteeRole)
knownCommitteeAuthorizations = forall era.
CommitteeState era -> Set (Credential 'HotCommitteeRole)
authorizedHotCommitteeCredentials CommitteeState ConwayEra
committeeState
      committeeVotableActionIds :: [GovActionId]
committeeVotableActionIds =
        (GovAction ConwayEra -> Bool) -> [GovActionId]
actions (forall era.
ConwayEraPParams era =>
EpochNo -> CommitteeState era -> GovAction era -> Bool
isCommitteeVotingAllowed EpochNo
geEpoch CommitteeState ConwayEra
committeeState)
      drepVotableActionIds :: [GovActionId]
drepVotableActionIds =
        (GovAction ConwayEra -> Bool) -> [GovActionId]
actions forall era. ConwayEraPParams era => GovAction era -> Bool
isDRepVotingAllowed
      stakepoolVotableActionIds :: [GovActionId]
stakepoolVotableActionIds =
        (GovAction ConwayEra -> Bool) -> [GovActionId]
actions forall era. ConwayEraPParams era => GovAction era -> Bool
isStakePoolVotingAllowed
      registeredCredentials :: Set (Credential 'Staking)
registeredCredentials = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
geCertState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) UMap
dsUnifiedL forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' UMap (Map (Credential 'Staking) UMElem)
umElemsL
   in forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained forall a b. (a -> b) -> a -> b
$ \Term (GovSignal ConwayEra)
govSignal ->
        forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (GovSignal ConwayEra)
govSignal forall a b. (a -> b) -> a -> b
$ \Term (VotingProcedures ConwayEra)
votingProcs Term (OSet (ProposalProcedure ConwayEra))
proposalProcs Term (StrictSeq (ConwayTxCert ConwayEra))
_certificates ->
          [ forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (VotingProcedures ConwayEra)
votingProcs forall a b. (a -> b) -> a -> b
$ \Term (Map Voter (Map GovActionId (VotingProcedure ConwayEra)))
votingProcsMap ->
              forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (Map Voter (Map GovActionId (VotingProcedure ConwayEra)))
votingProcsMap forall a b. (a -> b) -> a -> b
$ \Term (Voter, Map GovActionId (VotingProcedure ConwayEra))
kvp ->
                forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Voter, Map GovActionId (VotingProcedure ConwayEra))
kvp forall a b. (a -> b) -> a -> b
$ \Term Voter
voter Term (Map GovActionId (VotingProcedure ConwayEra))
mapActVote ->
                  (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 Voter
voter)
                    ( 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 (Credential 'HotCommitteeRole)
committeeHotCred ->
                        [ 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 GovActionId (VotingProcedure ConwayEra))
mapActVote) (forall a. HasSpec a => a -> Term a
lit forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [GovActionId]
committeeVotableActionIds)
                        , forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'HotCommitteeRole)
committeeHotCred forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => a -> Term a
lit Set (Credential 'HotCommitteeRole)
knownCommitteeAuthorizations
                        ]
                    )
                    ( 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 (Credential 'DRepRole)
drepCred ->
                        [ 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 GovActionId (VotingProcedure ConwayEra))
mapActVote) (forall a. HasSpec a => a -> Term a
lit forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [GovActionId]
drepVotableActionIds)
                        , forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'DRepRole)
drepCred forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => a -> Term a
lit Set (Credential 'DRepRole)
knownDReps
                        ]
                    )
                    ( 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 'StakePool)
poolKeyHash ->
                        [ 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 GovActionId (VotingProcedure ConwayEra))
mapActVote) (forall a. HasSpec a => a -> Term a
lit forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [GovActionId]
stakepoolVotableActionIds)
                        , forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (KeyHash 'StakePool)
poolKeyHash forall a b. (a -> b) -> a -> b
$ forall a. HasSpec a => a -> Term a
lit Set (KeyHash 'StakePool)
knownStakePools
                        ]
                    )
          , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term (OSet (ProposalProcedure ConwayEra))
proposalProcs forall a b. (a -> b) -> a -> b
$ \Term (ProposalProcedure ConwayEra)
proc ->
              forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (ProposalProcedure ConwayEra)
proc forall a b. (a -> b) -> a -> b
$ \Term Coin
deposit Term RewardAccount
returnAddr Term (GovAction ConwayEra)
govAction Term Anchor
_ ->
                [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Coin
deposit forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit (PParams ConwayEra
gePParams forall s a. s -> Getting a s a -> a
^. forall era. ConwayEraPParams era => Lens' (PParams era) Coin
ppGovActionDepositL)
                , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
returnAddr forall a b. (a -> b) -> a -> b
$ \Term Network
net Term (Credential 'Staking)
cred ->
                    [ forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (ProposalProcedure ConwayEra)
proc Term Network
net
                    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Network
net forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Network
Testnet
                    , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (Credential 'Staking)
cred forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` forall a. HasSpec a => a -> Term a
lit Set (Credential 'Staking)
registeredCredentials
                    ]
                , GovEnv ConwayEra
-> Proposals ConwayEra -> Term (GovAction ConwayEra) -> Pred
wfGovAction GovEnv ConwayEra
ge Proposals ConwayEra
ps Term (GovAction ConwayEra)
govAction
                ]
          ]

wfGovAction ::
  GovEnv ConwayEra ->
  Proposals ConwayEra ->
  Term (GovAction ConwayEra) ->
  Pred
wfGovAction :: GovEnv ConwayEra
-> Proposals ConwayEra -> Term (GovAction ConwayEra) -> Pred
wfGovAction GovEnv {StrictMaybe ScriptHash
gePPolicy :: StrictMaybe ScriptHash
gePPolicy :: forall era. GovEnv era -> StrictMaybe ScriptHash
gePPolicy, EpochNo
geEpoch :: EpochNo
geEpoch :: forall era. GovEnv era -> EpochNo
geEpoch, PParams ConwayEra
gePParams :: PParams ConwayEra
gePParams :: forall era. GovEnv era -> PParams era
gePParams, CertState ConwayEra
geCertState :: CertState ConwayEra
geCertState :: forall era. GovEnv era -> CertState era
geCertState} Proposals ConwayEra
ps Term (GovAction ConwayEra)
govAction =
  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 (GovAction ConwayEra)
govAction
    -- ParameterChange
    ( 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 (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
mPrevActionId Term (PParamsUpdate ConwayEra)
ppUpdate Term (StrictMaybe ScriptHash)
policy ->
        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
mPrevActionId forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)]
ppupIds
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (PParamsUpdate ConwayEra)
ppUpdate forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit forall era. EraPParams era => PParamsUpdate era
emptyPParamsUpdate
        , forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParamsUpdate ConwayEra)
ppUpdate Specification (PParamsUpdate ConwayEra)
wfPParamsUpdateSpec
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe ScriptHash)
policy forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit StrictMaybe ScriptHash
gePPolicy
        ]
    )
    -- HardForkInitiation
    ( 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 (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
[var|mPrevActionId|] Term ProtVer
[var|protVer|] ->
        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
mPrevActionId forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)]
hardForkIds
        , forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ProtVer
protVer forall a b. (a -> b) -> a -> b
$ \ Term Version
[var|majorVersion|] Term Natural
[var|minorVersion|] ->
            forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
mPrevActionId forall {p}.
Coercible p (StrictMaybe GovActionId) =>
p -> (Version, Maybe Version)
hfIdMajorVer forall a b. (a -> b) -> a -> b
$ \ Term (Version, Maybe Version)
[var|pvpair|] -> forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Version, Maybe Version)
pvpair forall a b. (a -> b) -> a -> b
$ \ Term Version
[var|currentMajorVersion|] Term (Maybe Version)
[var|mSuccMajorVersion|] ->
              forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
mPrevActionId forall {p}. Coercible p (StrictMaybe GovActionId) => p -> Natural
hfIdMinorVer forall a b. (a -> b) -> a -> b
$ \ Term Natural
[var|currentMinorVersion|] ->
                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 (Maybe Version)
mSuccMajorVersion
                  ( 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 ()
_ ->
                      [ Term Version
majorVersion forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Version
currentMajorVersion
                      , Term Natural
minorVersion forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
currentMinorVersion forall a. Num a => a -> a -> a
+ Term Natural
1
                      ]
                  )
                  ( 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 Version
[var|majorVersionPrime|] ->
                      [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term Version
majorVersion forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` (forall a. (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ Term Version
currentMajorVersion forall a. Semigroup a => a -> a -> a
<> forall a. (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ Term Version
majorVersionPrime)
                      , forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
                          (Term Version
currentMajorVersion forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Version
majorVersion)
                          (Term Natural
minorVersion forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
0)
                          (Term Natural
minorVersion forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
currentMinorVersion forall a. Num a => a -> a -> a
+ Term Natural
1)
                      ]
                  )
        ]
    )
    -- TreasuryWithdrawals
    ( 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 (Map RewardAccount Coin)
withdrawMap Term (StrictMaybe ScriptHash)
policy ->
        [ forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (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 RewardAccount Coin)
withdrawMap) forall a b. (a -> b) -> a -> b
$ \Term RewardAccount
rewAcnt ->
            forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
rewAcnt forall a b. (a -> b) -> a -> b
$ \Term Network
net Term (Credential 'Staking)
cred ->
              [ Term Network
net forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit Network
Testnet
              , Term (Credential 'Staking)
cred forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` forall a. HasSpec a => a -> Term a
lit Set (Credential 'Staking)
registeredCredentials
              ]
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ forall a. Foldy a => Term [a] -> Term a
sum_ (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map RewardAccount Coin)
withdrawMap) forall a. OrdLike a => Term a -> Term a -> Term Bool
>. forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe ScriptHash)
policy forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit StrictMaybe ScriptHash
gePPolicy
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ ProtVer -> Bool
HardForks.bootstrapPhase (PParams ConwayEra
gePParams forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL)
        ]
    )
    -- NoConfidence
    ( 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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId ->
        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
committeeIds
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ ProtVer -> Bool
HardForks.bootstrapPhase (PParams ConwayEra
gePParams forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL)
        ]
    )
    -- UpdateCommittee
    ( 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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId Term (Set (Credential 'ColdCommitteeRole))
_removed Term (Map (Credential 'ColdCommitteeRole) EpochNo)
added Term UnitInterval
_quorum ->
        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
committeeIds
        , forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
added) forall a b. (a -> b) -> a -> b
$ \Term EpochNo
epoch ->
            forall a. HasSpec a => a -> Term a
lit EpochNo
geEpoch forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term EpochNo
epoch
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ ProtVer -> Bool
HardForks.bootstrapPhase (PParams ConwayEra
gePParams forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL)
        ]
    )
    -- NewConstitution
    ( 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 (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
mPrevActionId Term (Constitution ConwayEra)
_c ->
        [ forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
mPrevActionId forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` forall a. HasSpec a => a -> Term a
lit [StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)]
constitutionIds
        , forall p. IsPred p => p -> Pred
assert forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not forall a b. (a -> b) -> a -> b
$ ProtVer -> Bool
HardForks.bootstrapPhase (PParams ConwayEra
gePParams forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL)
        ]
    )
    -- InfoAction
    (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 ()
_ -> Bool
True)
  where
    registeredCredentials :: Set (Credential 'Staking)
registeredCredentials = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
geCertState forall s a. s -> Getting a s a -> a
^. forall era. EraCertState era => Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) UMap
dsUnifiedL forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' UMap (Map (Credential 'Staking) UMElem)
umElemsL
    prevGovActionIds :: GovRelation StrictMaybe ConwayEra
prevGovActionIds = Proposals ConwayEra
ps forall s a. s -> Getting a s a -> a
^. forall era. Lens' (Proposals era) (GovRelation PRoot era)
pRootsL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s a. (s -> a) -> SimpleGetter s a
L.to forall era. GovRelation PRoot era -> GovRelation StrictMaybe era
toPrevGovActionIds
    constitutionIds :: [StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)]
constitutionIds =
      (GovRelation StrictMaybe ConwayEra
prevGovActionIds forall s a. s -> Getting a s a -> a
^. forall (f :: * -> *) era.
Lens'
  (GovRelation f era) (f (GovPurposeId 'ConstitutionPurpose era))
grConstitutionL)
        forall a. a -> [a] -> [a]
: [ forall a. a -> StrictMaybe a
SJust forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall era. GovActionState era -> GovActionId
gasId GovActionState ConwayEra
gas
          | GovActionState ConwayEra
gas <- [GovActionState ConwayEra]
actions
          , NewConstitution {} <- [forall era. ProposalProcedure era -> GovAction era
pProcGovAction forall a b. (a -> b) -> a -> b
$ forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure GovActionState ConwayEra
gas]
          ]
    committeeIds :: [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
committeeIds =
      (GovRelation StrictMaybe ConwayEra
prevGovActionIds forall s a. s -> Getting a s a -> a
^. forall (f :: * -> *) era.
Lens' (GovRelation f era) (f (GovPurposeId 'CommitteePurpose era))
grCommitteeL)
        forall a. a -> [a] -> [a]
: [ forall a. a -> StrictMaybe a
SJust forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall era. GovActionState era -> GovActionId
gasId GovActionState ConwayEra
gas
          | GovActionState ConwayEra
gas <- [GovActionState ConwayEra]
actions
          , forall {era}. GovAction era -> Bool
isCommitteeAction (forall era. ProposalProcedure era -> GovAction era
pProcGovAction forall a b. (a -> b) -> a -> b
$ forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure GovActionState ConwayEra
gas)
          ]
    ppupIds :: [StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)]
ppupIds =
      (GovRelation StrictMaybe ConwayEra
prevGovActionIds forall s a. s -> Getting a s a -> a
^. forall (f :: * -> *) era.
Lens'
  (GovRelation f era) (f (GovPurposeId 'PParamUpdatePurpose era))
grPParamUpdateL)
        forall a. a -> [a] -> [a]
: [ forall a. a -> StrictMaybe a
SJust forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall era. GovActionState era -> GovActionId
gasId GovActionState ConwayEra
gas
          | GovActionState ConwayEra
gas <- [GovActionState ConwayEra]
actions
          , ParameterChange {} <- [forall era. ProposalProcedure era -> GovAction era
pProcGovAction forall a b. (a -> b) -> a -> b
$ forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure GovActionState ConwayEra
gas]
          ]
    hardForkIds :: [StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)]
hardForkIds =
      (GovRelation StrictMaybe ConwayEra
prevGovActionIds forall s a. s -> Getting a s a -> a
^. forall (f :: * -> *) era.
Lens' (GovRelation f era) (f (GovPurposeId 'HardForkPurpose era))
grHardForkL)
        forall a. a -> [a] -> [a]
: [ forall a. a -> StrictMaybe a
SJust forall a b. (a -> b) -> a -> b
$ coerce :: forall a b. Coercible a b => a -> b
coerce forall a b. (a -> b) -> a -> b
$ forall era. GovActionState era -> GovActionId
gasId GovActionState ConwayEra
gas
          | GovActionState ConwayEra
gas <- [GovActionState ConwayEra]
actions
          , HardForkInitiation {} <- [forall era. ProposalProcedure era -> GovAction era
pProcGovAction forall a b. (a -> b) -> a -> b
$ forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure GovActionState ConwayEra
gas]
          ]
    isCommitteeAction :: GovAction era -> Bool
isCommitteeAction UpdateCommittee {} = Bool
True
    isCommitteeAction NoConfidence {} = Bool
True
    isCommitteeAction GovAction era
_ = Bool
False

    findProtVer :: StrictMaybe GovActionId -> ProtVer
findProtVer StrictMaybe GovActionId
SNothing = PParams ConwayEra
gePParams forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL
    findProtVer (SJust GovActionId
hid) =
      case forall era.
GovActionId -> Proposals era -> Maybe (GovActionState era)
proposalsLookupId GovActionId
hid Proposals ConwayEra
ps of
        Just GovActionState ConwayEra
gas
          | HardForkInitiation StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)
_ ProtVer
protVer <- forall era. ProposalProcedure era -> GovAction era
pProcGovAction forall a b. (a -> b) -> a -> b
$ forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure GovActionState ConwayEra
gas -> ProtVer
protVer
        Maybe (GovActionState ConwayEra)
_ -> PParams ConwayEra
gePParams forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL

    hfIdMajorVer :: p -> (Version, Maybe Version)
hfIdMajorVer p
mId =
      let ProtVer Version
currentMajorVersion Natural
_ = StrictMaybe GovActionId -> ProtVer
findProtVer (coerce :: forall a b. Coercible a b => a -> b
coerce p
mId)
       in (Version
currentMajorVersion, forall (m :: * -> *). MonadFail m => Version -> m Version
succVersion @Maybe Version
currentMajorVersion)

    hfIdMinorVer :: p -> Natural
hfIdMinorVer p
mId =
      let ProtVer Version
_ Natural
currentMinorVersion = StrictMaybe GovActionId -> ProtVer
findProtVer (coerce :: forall a b. Coercible a b => a -> b
coerce p
mId)
       in Natural
currentMinorVersion

    actions :: [GovActionState ConwayEra]
actions = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ forall era. Proposals era -> StrictSeq (GovActionState era)
proposalsActions Proposals ConwayEra
ps

wfPParamsUpdateSpec :: Specification (PParamsUpdate ConwayEra)
wfPParamsUpdateSpec :: Specification (PParamsUpdate ConwayEra)
wfPParamsUpdateSpec =
  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 SimplePPUpdate
ppupdate ->
    -- Note that ppupdate :: SimplePPUpdate
    forall p a.
(HasSpec a, IsProductType a, IsPred p) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term SimplePPUpdate
ppupdate forall a b. (a -> b) -> a -> b
$
      \Term (StrictMaybe Coin)
_minFeeA
       Term (StrictMaybe Coin)
_minFeeB
       Term (StrictMaybe Word32)
maxBBSize
       Term (StrictMaybe Word32)
maxTxSize
       Term (StrictMaybe Word32)
maxBHSize
       Term (StrictMaybe Coin)
_keyDeposit
       Term (StrictMaybe Coin)
poolDeposit
       Term (StrictMaybe EpochInterval)
_eMax
       Term (StrictMaybe Word16)
_nOpt
       Term (StrictMaybe NonNegativeInterval)
_a0
       Term (StrictMaybe UnitInterval)
_rho
       Term (StrictMaybe UnitInterval)
_tau
       Term (StrictMaybe UnitInterval)
_decentral
       Term (StrictMaybe ProtVer)
_protocolVersion
       Term (StrictMaybe Coin)
_minUTxOValue
       Term (StrictMaybe Coin)
_minPoolCost
       -- Alonzo
       Term (StrictMaybe Coin)
_coinsPerUTxOWord
       Term (StrictMaybe CostModels)
costModels
       Term (StrictMaybe Prices)
_prices
       Term (StrictMaybe ExUnits)
_maxTxExUnits
       Term (StrictMaybe ExUnits)
_maBlockExUnits
       Term (StrictMaybe Natural)
maxValSize
       Term (StrictMaybe Natural)
collateralPercentage
       Term (StrictMaybe Natural)
_MaxCollateralInputs
       -- Babbage
       Term (StrictMaybe Coin)
coinsPerUTxOByte
       -- Conway
       Term (StrictMaybe PoolVotingThresholds)
_poolVotingThresholds
       Term (StrictMaybe DRepVotingThresholds)
_drepVotingThresholds
       Term (StrictMaybe Natural)
_committeeMinSize
       Term (StrictMaybe EpochInterval)
committeeMaxTermLength
       Term (StrictMaybe EpochInterval)
govActionLifetime
       Term (StrictMaybe Coin)
govActionDeposit
       Term (StrictMaybe Coin)
dRepDeposit
       Term (StrictMaybe EpochInterval)
_drepActivity
       Term (StrictMaybe NonNegativeInterval)
_minFeeRefScriptCostPerByte ->
          [ Term (StrictMaybe Word32)
maxBBSize forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust Word32
0)
          , Term (StrictMaybe Word32)
maxTxSize forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust Word32
0)
          , Term (StrictMaybe Word32)
maxBHSize forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust Word32
0)
          , Term (StrictMaybe Natural)
maxValSize forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust Natural
0)
          , Term (StrictMaybe Natural)
collateralPercentage forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust Natural
0)
          , Term (StrictMaybe EpochInterval)
committeeMaxTermLength forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust forall a b. (a -> b) -> a -> b
$ Word32 -> EpochInterval
EpochInterval Word32
0)
          , Term (StrictMaybe EpochInterval)
govActionLifetime forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust forall a b. (a -> b) -> a -> b
$ Word32 -> EpochInterval
EpochInterval Word32
0)
          , Term (StrictMaybe Coin)
poolDeposit forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust forall a. Monoid a => a
mempty)
          , Term (StrictMaybe Coin)
govActionDeposit forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust forall a. Monoid a => a
mempty)
          , Term (StrictMaybe Coin)
dRepDeposit forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust forall a. Monoid a => a
mempty)
          , Term (StrictMaybe CostModels)
costModels forall a. HasSpec a => Term a -> Term a -> Term Bool
==. forall a. HasSpec a => a -> Term a
lit forall a. StrictMaybe a
SNothing -- NOTE: this is because the cost
          , Term (StrictMaybe Coin)
coinsPerUTxOByte forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. forall a. HasSpec a => a -> Term a
lit (forall a. a -> StrictMaybe a
SJust forall a. Monoid a => a
mempty)
          -- model generator is way too slow
          ]