{-# 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 = (Term (GovEnv ConwayEra) -> Pred)
-> Specification (GovEnv ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (GovEnv ConwayEra) -> Pred)
 -> Specification (GovEnv ConwayEra))
-> (Term (GovEnv ConwayEra) -> Pred)
-> Specification (GovEnv ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (GovEnv ConwayEra)
ge ->
  Term (GovEnv ConwayEra)
-> FunTy (MapList Term (ProductAsList (GovEnv 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 (GovEnv ConwayEra)
ge (FunTy (MapList Term (ProductAsList (GovEnv ConwayEra))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (GovEnv ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps TxId
_ TermD Deps EpochNo
_ Term (PParams ConwayEra)
pp TermD Deps (StrictMaybe ScriptHash)
_ TermD Deps (ConwayCertState ConwayEra)
_ ->
    Term (PParams ConwayEra)
-> Specification (PParams ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParams ConwayEra)
pp Specification (PParams ConwayEra)
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 :: EpochNo
geEpoch :: forall era. GovEnv era -> EpochNo
geEpoch, StrictMaybe ScriptHash
gePPolicy :: StrictMaybe ScriptHash
gePPolicy :: forall era. GovEnv era -> StrictMaybe ScriptHash
gePPolicy, CertState ConwayEra
geCertState :: CertState ConwayEra
geCertState :: forall era. GovEnv era -> CertState era
geCertState} =
  TermD Deps EpochNo
-> TermD Deps (StrictMaybe ScriptHash)
-> Term (CertState ConwayEra)
-> Specification (Proposals ConwayEra)
proposalsSpec (EpochNo -> TermD Deps EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
geEpoch) (StrictMaybe ScriptHash -> TermD Deps (StrictMaybe ScriptHash)
forall a. HasSpec a => a -> Term a
lit StrictMaybe ScriptHash
gePPolicy) (ConwayCertState ConwayEra -> TermD Deps (ConwayCertState ConwayEra)
forall a. HasSpec a => a -> Term a
lit CertState ConwayEra
ConwayCertState ConwayEra
geCertState)

proposalsSpec ::
  Term EpochNo ->
  Term (StrictMaybe ScriptHash) ->
  Term (CertState ConwayEra) ->
  Specification (Proposals ConwayEra)
proposalsSpec :: TermD Deps EpochNo
-> TermD Deps (StrictMaybe ScriptHash)
-> Term (CertState ConwayEra)
-> Specification (Proposals ConwayEra)
proposalsSpec TermD Deps EpochNo
geEpoch TermD Deps (StrictMaybe ScriptHash)
gePPolicy Term (CertState ConwayEra)
geCertState =
  (Term (Proposals ConwayEra) -> Pred)
-> Specification (Proposals ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (Proposals ConwayEra) -> Pred)
 -> Specification (Proposals ConwayEra))
-> (Term (Proposals ConwayEra) -> Pred)
-> Specification (Proposals ConwayEra)
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])
    Term (Proposals ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (Proposals 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 (Proposals ConwayEra)
props (FunTy (MapList Term (ProductAsList (Proposals ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (Proposals ConwayEra))) [Pred]
-> Pred
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
      , Term (ProposalTree ConwayEra)
-> Specification (ProposalTree ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
          Term (ProposalTree ConwayEra)
ppupTree
          ( (Term (GovActionState ConwayEra) -> [Pred])
-> Specification (ProposalTree ConwayEra)
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),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) =>
Term a -> Pred
isCon @"ParameterChange" (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra))
-> (Term (GovActionState ConwayEra)
    -> Term (ProposalProcedure ConwayEra))
-> Term (GovActionState ConwayEra)
-> Term (GovAction ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ (Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra))
-> Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra)
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),
 GenericRequires 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_ (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra))
-> (Term (GovActionState ConwayEra)
    -> Term (ProposalProcedure ConwayEra))
-> Term (GovActionState ConwayEra)
-> Term (GovAction ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ (Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra))
-> Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra)
forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasPpup) (FunTy
   (MapList
      Term (ConstrOf "ParameterChange" (TheSop (GovAction ConwayEra))))
   [Pred]
 -> Pred)
-> FunTy
     (MapList
        Term (ConstrOf "ParameterChange" (TheSop (GovAction ConwayEra))))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$
                      \TermD
  Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
_ Term (PParamsUpdate ConwayEra)
ppup TermD Deps (StrictMaybe ScriptHash)
policy ->
                        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (PParamsUpdate ConwayEra)
ppup Term (PParamsUpdate ConwayEra)
-> Term (PParamsUpdate ConwayEra) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. PParamsUpdate ConwayEra -> Term (PParamsUpdate ConwayEra)
forall a. HasSpec a => a -> Term a
lit PParamsUpdate ConwayEra
forall era. EraPParams era => PParamsUpdate era
emptyPParamsUpdate
                        , Term (PParamsUpdate ConwayEra)
-> Specification (PParamsUpdate ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParamsUpdate ConwayEra)
ppup Specification (PParamsUpdate ConwayEra)
wfPParamsUpdateSpec
                        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps (StrictMaybe ScriptHash)
policy TermD Deps (StrictMaybe ScriptHash)
-> TermD Deps (StrictMaybe ScriptHash) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. TermD Deps (StrictMaybe ScriptHash)
gePPolicy
                        ]
                  ]
              )
          )
      , Term [Tree (GovActionState ConwayEra)]
-> (Term (Tree (GovActionState ConwayEra)) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)]
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
ppupTree) (Hint (Tree (GovActionState ConwayEra))
-> Term (Tree (GovActionState ConwayEra)) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer, Integer)
Hint (Tree (GovActionState ConwayEra))
treeGenHint)
      , Hint [Tree (GovActionState ConwayEra)]
-> Term [Tree (GovActionState ConwayEra)] -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint [Tree (GovActionState ConwayEra)]
listSizeHint (Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)]
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
      , Term (ProposalTree ConwayEra)
-> Specification (ProposalTree ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
          Term (ProposalTree ConwayEra)
hardForkTree
          ( (Term (GovActionState ConwayEra) -> Pred)
-> Specification (ProposalTree ConwayEra)
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),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) =>
Term a -> Pred
isCon @"HardForkInitiation" (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra))
-> (Term (GovActionState ConwayEra)
    -> Term (ProposalProcedure ConwayEra))
-> Term (GovActionState ConwayEra)
-> Term (GovAction ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ (Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra))
-> Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra)
forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasHfork)
              )
          )
      , Term (ProposalTree ConwayEra)
-> (Term (GovActionState ConwayEra)
    -> Term (GovActionState ConwayEra) -> [Pred])
-> Pred
forall p.
IsPred p =>
Term (ProposalTree ConwayEra)
-> (Term (GovActionState ConwayEra)
    -> Term (GovActionState ConwayEra) -> p)
-> Pred
allGASAndChildInTree Term (ProposalTree ConwayEra)
hardForkTree ((Term (GovActionState ConwayEra)
  -> Term (GovActionState ConwayEra) -> [Pred])
 -> Pred)
-> (Term (GovActionState ConwayEra)
    -> Term (GovActionState ConwayEra) -> [Pred])
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (GovActionState ConwayEra)
gas Term (GovActionState ConwayEra)
gas' ->
          [ Term (GovActionState ConwayEra)
-> (Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
    -> Term ProtVer -> Pred)
-> Pred
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 -> Pred)
 -> Pred)
-> (Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
    -> Term ProtVer -> Pred)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
_ Term ProtVer
pv ->
              Term (GovActionState ConwayEra)
-> (Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
    -> Term ProtVer -> Pred)
-> Pred
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 -> Pred)
 -> Pred)
-> (Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
    -> Term ProtVer -> Pred)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
_ Term ProtVer
pv' ->
                Term ProtVer
-> FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ProtVer
pv (FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Version
majV Term Natural
minV ->
                  Term ProtVer
-> FunTy (MapList Term (ProductAsList ProtVer)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ProtVer
pv' (FunTy (MapList Term (ProductAsList ProtVer)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList ProtVer)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Version
majV' Term Natural
minV' ->
                    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Version
majV Term Version -> Term Version -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Version
majV'
                    , Term Bool -> Term Bool -> Term Bool -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
                        (Term Version
majV Term Version -> Term Version -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Version -> Term Version
forall a. HasSpec a => a -> Term a
lit Version
forall a. Bounded a => a
maxBound)
                        (Term Version
majV' Term Version -> Term Version -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Version
majV)
                        (Term Version
majV' Term Version -> Term Version -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Version -> Term Version
succV_ Term Version
majV)
                    , Term Bool -> Term Bool -> Term Bool -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
                        (Term Version
majV Term Version -> Term Version -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Version
majV')
                        (Term Natural
minV' Term Natural -> Term Natural -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
minV Term Natural -> Term Natural -> Term Natural
forall a. Num a => a -> a -> a
+ Term Natural
1)
                        (Term Natural
minV' Term Natural -> Term Natural -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
0)
                    ]
          ]
      , Term [Tree (GovActionState ConwayEra)]
-> (Term (Tree (GovActionState ConwayEra)) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)]
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
hardForkTree) (Hint (Tree (GovActionState ConwayEra))
-> Term (Tree (GovActionState ConwayEra)) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer, Integer)
Hint (Tree (GovActionState ConwayEra))
treeGenHint)
      , Hint [Tree (GovActionState ConwayEra)]
-> Term [Tree (GovActionState ConwayEra)] -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint [Tree (GovActionState ConwayEra)]
listSizeHint (Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)]
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.
        Term (ProposalTree ConwayEra)
-> Specification (ProposalTree ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
          Term (ProposalTree ConwayEra)
committeeTree
          ( (Term (GovActionState ConwayEra) -> Pred)
-> Specification (ProposalTree ConwayEra)
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
                  Term (GovAction ConwayEra)
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (GovAction 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 (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra))
-> (Term (GovActionState ConwayEra)
    -> Term (ProposalProcedure ConwayEra))
-> Term (GovActionState ConwayEra)
-> Term (GovAction ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ (Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra))
-> Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra)
forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasComm)
                    (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
           (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
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
            (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
            (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
         (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
              (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
forall a b. (a -> b) -> a -> b
$ \TermD
  Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
_ Term (PParamsUpdate ConwayEra)
_ TermD Deps (StrictMaybe ScriptHash)
_ -> Bool
False)
                    (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)
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
            (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)
forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
_ Term ProtVer
_ -> Bool
False)
                    (FunTy
  (MapList
     Term
     (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
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 (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash)))
-> FunTy
     (MapList
        Term
        (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (Map RewardAccount Coin)
_ TermD Deps (StrictMaybe ScriptHash)
_ -> Bool
False)
                    (FunTy
  (MapList
     Term
     (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
  Bool
-> Weighted
     (BinderD Deps)
     (StrictMaybe (GovPurposeId 'CommitteePurpose 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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
   Bool
 -> Weighted
      (BinderD Deps)
      (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
     Bool
-> Weighted
     (BinderD Deps)
     (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ -> Bool
True)
                    -- UpdateCommittee - We are only interested in this case
                    ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
           (Prod
              (Set (Credential 'ColdCommitteeRole))
              (Prod
                 (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
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
            (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
            (Prod
               (Set (Credential 'ColdCommitteeRole))
               (Prod
                  (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
         (Prod
            (Set (Credential 'ColdCommitteeRole))
            (Prod
               (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
              (Prod
                 (Set (Credential 'ColdCommitteeRole))
                 (Prod
                    (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ TermD Deps (Set (Credential 'ColdCommitteeRole))
_ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
added TermD Deps UnitInterval
_ ->
                        Term [EpochNo] -> (TermD Deps EpochNo -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map (Credential 'ColdCommitteeRole) EpochNo)
-> Term [EpochNo]
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) ((TermD Deps EpochNo -> Term Bool) -> Pred)
-> (TermD Deps EpochNo -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps EpochNo
epoch ->
                          TermD Deps EpochNo
geEpoch TermD Deps EpochNo -> TermD Deps EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. TermD Deps EpochNo
epoch
                    )
                    (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
           (Constitution ConwayEra))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
        (Constitution 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
            (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
            (Constitution ConwayEra))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
         (Constitution ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
              (Constitution ConwayEra))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
        (Constitution ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD
  Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
_ TermD Deps (Constitution ConwayEra)
_ -> Bool
False)
                    (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
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 ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
False)
              )
          )
      , Term [Tree (GovActionState ConwayEra)]
-> (Term (Tree (GovActionState ConwayEra)) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)]
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
committeeTree) (Hint (Tree (GovActionState ConwayEra))
-> Term (Tree (GovActionState ConwayEra)) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer, Integer)
Hint (Tree (GovActionState ConwayEra))
treeGenHint)
      , Hint [Tree (GovActionState ConwayEra)]
-> Term [Tree (GovActionState ConwayEra)] -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint [Tree (GovActionState ConwayEra)]
listSizeHint (Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)]
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
      , Term (ProposalTree ConwayEra)
-> Specification (ProposalTree ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies
          Term (ProposalTree ConwayEra)
constitutionTree
          ( (Term (GovActionState ConwayEra) -> Pred)
-> Specification (ProposalTree ConwayEra)
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),
 SumOver (Cases (SOP (TheSop a))) ~ SimpleRep a,
 All HasSpec (Cases (SOP (TheSop a))),
 HasSpec (ProdOver (ConstrOf c (TheSop a))), GenericRequires a) =>
Term a -> Pred
isCon @"NewConstitution" (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra))
-> (Term (GovActionState ConwayEra)
    -> Term (ProposalProcedure ConwayEra))
-> Term (GovActionState ConwayEra)
-> Term (GovAction ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ (Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra))
-> Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra)
forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasNewConst)
              )
          )
      , Term [Tree (GovActionState ConwayEra)]
-> (Term (Tree (GovActionState ConwayEra)) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)]
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
constitutionTree) (Hint (Tree (GovActionState ConwayEra))
-> Term (Tree (GovActionState ConwayEra)) -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint (Maybe Integer, Integer)
Hint (Tree (GovActionState ConwayEra))
treeGenHint)
      , Hint [Tree (GovActionState ConwayEra)]
-> Term [Tree (GovActionState ConwayEra)] -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint [Tree (GovActionState ConwayEra)]
listSizeHint (Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)]
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
        Term [GovActionState ConwayEra]
-> (Term (GovActionState ConwayEra) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [GovActionState ConwayEra]
unorderedProposals ((Term (GovActionState ConwayEra) -> Pred) -> Pred)
-> (Term (GovActionState ConwayEra) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (GovActionState ConwayEra)
[var|gasOther|] ->
          Term (GovAction ConwayEra)
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (GovAction 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 (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra))
-> (Term (GovActionState ConwayEra)
    -> Term (ProposalProcedure ConwayEra))
-> Term (GovActionState ConwayEra)
-> Term (GovAction ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ (Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra))
-> Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra)
forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gasOther)
            (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
           (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
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
            (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
            (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
         (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
              (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
forall a b. (a -> b) -> a -> b
$ \TermD
  Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
_ Term (PParamsUpdate ConwayEra)
_ TermD Deps (StrictMaybe ScriptHash)
_ -> Bool
False) -- Parameter Change
            (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)
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
            (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)
forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
_ Term ProtVer
_ -> Bool
False) -- HardForkInitiation
            -- Treasury Withdrawal
            ( FunTy
  (MapList
     Term
     (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
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 (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash)))
-> FunTy
     (MapList
        Term
        (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
forall a b. (a -> b) -> a -> b
$ \ TermD Deps (Map RewardAccount Coin)
[var|withdrawMap|] TermD Deps (StrictMaybe ScriptHash)
[var|policy|] ->
                NonEmpty String -> Pred -> Pred
forall deps. NonEmpty String -> PredD deps -> PredD deps
Explain (String -> NonEmpty String
forall a. a -> NonEmpty a
forall (f :: * -> *) a. Applicative f => a -> f a
pure String
"TreasuryWithdrawal fails") (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
                  [Pred] -> Pred
forall deps. [PredD deps] -> PredD deps
And
                    [ Term (GovActionState ConwayEra)
-> TermD Deps (Map RewardAccount Coin) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (GovActionState ConwayEra)
gasOther TermD Deps (Map RewardAccount Coin)
withdrawMap
                    , TermD Deps (ConwayCertState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ConwayCertState 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 (CertState ConwayEra)
TermD Deps (ConwayCertState ConwayEra)
geCertState (FunTy
   (MapList Term (ProductAsList (ConwayCertState ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ConwayCertState ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps (VState ConwayEra)
_vState TermD Deps (PState ConwayEra)
_pState Term (DState ConwayEra)
[var|dState|] ->
                        Term (DState ConwayEra)
-> FunTy (MapList Term (ProductAsList (DState 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 (DState ConwayEra)
dState (FunTy (MapList Term (ProductAsList (DState ConwayEra))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (DState ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term UMap
[var|rewardMap|] TermD Deps (Map FutureGenDeleg GenDelegPair)
_ TermD Deps GenDelegs
_ TermD Deps InstantaneousRewards
_ ->
                          Term UMap
-> (UMap -> Set (Credential 'Staking))
-> (Term (Set (Credential 'Staking)) -> Pred)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term UMap
rewardMap (Map (Credential 'Staking) UMElem -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet (Map (Credential 'Staking) UMElem -> Set (Credential 'Staking))
-> (UMap -> Map (Credential 'Staking) UMElem)
-> UMap
-> Set (Credential 'Staking)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UMap -> Map (Credential 'Staking) UMElem
umElems) ((Term (Set (Credential 'Staking)) -> Pred) -> Pred)
-> (Term (Set (Credential 'Staking)) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Set (Credential 'Staking))
[var|registeredCredentials|] ->
                            Term (Set RewardAccount) -> (Term RewardAccount -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (TermD Deps (Map RewardAccount Coin) -> Term (Set RewardAccount)
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_ TermD Deps (Map RewardAccount Coin)
withdrawMap) ((Term RewardAccount -> Pred) -> Pred)
-> (Term RewardAccount -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term RewardAccount
[var|rewAcnt|] ->
                              Term RewardAccount
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
rewAcnt (FunTy (MapList Term (ProductAsList RewardAccount)) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|network|] Term (Credential 'Staking)
[var|credential|] ->
                                [ Term Network
network Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit Network
Testnet
                                , Term (Credential 'Staking)
credential Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Term (Set (Credential 'Staking))
registeredCredentials
                                ]
                    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps (StrictMaybe ScriptHash)
policy TermD Deps (StrictMaybe ScriptHash)
-> TermD Deps (StrictMaybe ScriptHash) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. TermD Deps (StrictMaybe ScriptHash)
gePPolicy
                    ]
            )
            (FunTy
  (MapList
     Term
     (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
  Bool
-> Weighted
     (BinderD Deps)
     (StrictMaybe (GovPurposeId 'CommitteePurpose 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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
   Bool
 -> Weighted
      (BinderD Deps)
      (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
     Bool
-> Weighted
     (BinderD Deps)
     (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ -> Bool
False) -- NoConfidence
            (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
           (Prod
              (Set (Credential 'ColdCommitteeRole))
              (Prod
                 (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
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
            (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
            (Prod
               (Set (Credential 'ColdCommitteeRole))
               (Prod
                  (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
         (Prod
            (Set (Credential 'ColdCommitteeRole))
            (Prod
               (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
              (Prod
                 (Set (Credential 'ColdCommitteeRole))
                 (Prod
                    (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
_ TermD Deps (Set (Credential 'ColdCommitteeRole))
_ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
_ TermD Deps UnitInterval
_ -> Bool
False) -- Update Committee
            (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
           (Constitution ConwayEra))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
        (Constitution 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
            (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
            (Constitution ConwayEra))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
         (Constitution ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
              (Constitution ConwayEra))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
        (Constitution ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD
  Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
_ TermD Deps (Constitution ConwayEra)
_ -> Bool
False) -- NewConstitution
            -- Info
            (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
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 ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True) -- InfoAction
      , Hint [GovActionState ConwayEra]
-> Term [GovActionState ConwayEra] -> Pred
forall t. HasGenHint t => Hint t -> Term t -> Pred
genHint Integer
Hint [GovActionState ConwayEra]
listSizeHint Term [GovActionState ConwayEra]
unorderedProposals
      ]
  where
    treeGenHint :: (Maybe Integer, Integer)
treeGenHint = (Integer -> Maybe Integer
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 = (Term (ProposalTree ConwayEra) -> Pred)
-> Specification (ProposalTree ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (ProposalTree ConwayEra) -> Pred)
 -> Specification (ProposalTree ConwayEra))
-> (Term (ProposalTree ConwayEra) -> Pred)
-> Specification (ProposalTree ConwayEra)
forall a b. (a -> b) -> a -> b
$ \ Term (ProposalTree ConwayEra)
[var|proposalTree|] ->
  Term [Tree (GovActionState ConwayEra)]
-> (Term (Tree (GovActionState ConwayEra)) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)]
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
proposalTree) ((Term (Tree (GovActionState ConwayEra)) -> Pred) -> Pred)
-> (Term (Tree (GovActionState ConwayEra)) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Tree (GovActionState ConwayEra))
[var|subtree|] ->
    Term (Tree (GovActionState ConwayEra))
-> FunTy
     (MapList
        Term
        (Args
           (SimpleRep
              (GovActionState ConwayEra, [Tree (GovActionState ConwayEra)]))))
     p
-> Pred
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),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (GovActionState ConwayEra))
subtree (FunTy
   (MapList
      Term
      (Args
         (SimpleRep
            (GovActionState ConwayEra, [Tree (GovActionState ConwayEra)]))))
   p
 -> Pred)
-> FunTy
     (MapList
        Term
        (Args
           (SimpleRep
              (GovActionState ConwayEra, [Tree (GovActionState ConwayEra)]))))
     p
-> Pred
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 =
  Term [Tree (GovActionState ConwayEra)]
-> (Term (Tree (GovActionState ConwayEra)) -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)]
forall x y. (HasSpec x, HasSpec y) => Term (x, y) -> Term y
snd_ Term (ProposalTree ConwayEra)
t) ((Term (Tree (GovActionState ConwayEra)) -> Pred) -> Pred)
-> (Term (Tree (GovActionState ConwayEra)) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Tree (GovActionState ConwayEra))
[var|subtree|] ->
    Term (Tree (GovActionState ConwayEra))
-> FunTy
     (MapList
        Term
        (Args
           (SimpleRep
              (GovActionState ConwayEra, [Tree (GovActionState ConwayEra)]))))
     Pred
-> Pred
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),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (GovActionState ConwayEra))
subtree (FunTy
   (MapList
      Term
      (Args
         (SimpleRep
            (GovActionState ConwayEra, [Tree (GovActionState ConwayEra)]))))
   Pred
 -> Pred)
-> FunTy
     (MapList
        Term
        (Args
           (SimpleRep
              (GovActionState ConwayEra, [Tree (GovActionState ConwayEra)]))))
     Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (GovActionState ConwayEra)
[var|gas|] Term [Tree (GovActionState ConwayEra)]
[var|cs|] ->
      Term [Tree (GovActionState ConwayEra)]
-> (Term (Tree (GovActionState ConwayEra)) -> p) -> Pred
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 ((Term (Tree (GovActionState ConwayEra)) -> p) -> Pred)
-> (Term (Tree (GovActionState ConwayEra)) -> p) -> Pred
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 (Term (Tree (GovActionState ConwayEra))
-> Term (GovActionState ConwayEra)
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 =
  Term (ProposalTree ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ProposalTree 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 (ProposalTree ConwayEra)
rootAndTrees (FunTy
   (MapList Term (ProductAsList (ProposalTree ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ProposalTree ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe GovActionId)
root Term [Tree (GovActionState ConwayEra)]
trees ->
    [ Term (ProposalTree ConwayEra)
-> Term (StrictMaybe GovActionId) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (ProposalTree ConwayEra)
rootAndTrees Term (StrictMaybe GovActionId)
root
    , Term (ProposalTree ConwayEra)
-> Term [Tree (GovActionState ConwayEra)] -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (ProposalTree ConwayEra)
rootAndTrees Term [Tree (GovActionState ConwayEra)]
trees
    , Term [Tree (GovActionState ConwayEra)]
-> (Term (Tree (GovActionState ConwayEra)) -> [Pred]) -> Pred
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 ((Term (Tree (GovActionState ConwayEra)) -> [Pred]) -> Pred)
-> (Term (Tree (GovActionState ConwayEra)) -> [Pred]) -> Pred
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 (Term (Tree (GovActionState ConwayEra))
-> Term (GovActionState ConwayEra)
forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree (GovActionState ConwayEra))
t) (Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred)
-> (Term (StrictMaybe GovActionId) -> Term Bool)
-> Term (StrictMaybe GovActionId)
-> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term (StrictMaybe GovActionId)
-> Term (StrictMaybe GovActionId) -> Term Bool
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
          Term (Tree (GovActionState ConwayEra))
-> FunTy
     (MapList
        Term
        (Args
           (SimpleRep
              (GovActionState ConwayEra, [Tree (GovActionState ConwayEra)]))))
     [Pred]
-> Pred
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),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Tree (GovActionState ConwayEra))
t (FunTy
   (MapList
      Term
      (Args
         (SimpleRep
            (GovActionState ConwayEra, [Tree (GovActionState ConwayEra)]))))
   [Pred]
 -> Pred)
-> FunTy
     (MapList
        Term
        (Args
           (SimpleRep
              (GovActionState ConwayEra, [Tree (GovActionState ConwayEra)]))))
     [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (GovActionState ConwayEra)
gas Term [Tree (GovActionState ConwayEra)]
children ->
            [ Term [Tree (GovActionState ConwayEra)]
-> (Term (Tree (GovActionState ConwayEra)) -> [Pred]) -> Pred
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 ((Term (Tree (GovActionState ConwayEra)) -> [Pred]) -> Pred)
-> (Term (Tree (GovActionState ConwayEra)) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Tree (GovActionState ConwayEra))
t' ->
                [ Term (GovActionState ConwayEra)
-> (Term (StrictMaybe GovActionId) -> Pred) -> Pred
withPrevActId (Term (Tree (GovActionState ConwayEra))
-> Term (GovActionState ConwayEra)
forall a. HasSpec a => Term (Tree a) -> Term a
rootLabel_ Term (Tree (GovActionState ConwayEra))
t') (Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred)
-> (Term (StrictMaybe GovActionId) -> Term Bool)
-> Term (StrictMaybe GovActionId)
-> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Term (StrictMaybe GovActionId)
-> Term (StrictMaybe GovActionId) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term GovActionId -> Term (StrictMaybe GovActionId)
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 Term [Tree (GovActionState ConwayEra)]
-> Term (GovActionState ConwayEra) -> Pred
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
forall deps. [PredD deps] -> PredD deps
And
    [ Term (ProposalProcedure ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ProposalProcedure 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)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ Term (GovActionState ConwayEra)
gas) (FunTy
   (MapList Term (ProductAsList (ProposalProcedure ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ProposalProcedure ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps Coin
_deposit Term RewardAccount
[var|retAddr|] Term (GovAction ConwayEra)
_action TermD Deps Anchor
_anchor ->
        Term RewardAccount
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
retAddr (FunTy (MapList Term (ProductAsList RewardAccount)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|net|] Term (Credential 'Staking)
_ -> [Term (GovActionState ConwayEra) -> Term Network -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (GovActionState ConwayEra)
gas Term Network
net, Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Network
net Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit Network
Testnet]
    , Term (GovAction ConwayEra)
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (GovAction 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 (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra)
pProcGovAction_ (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra))
-> (Term (GovActionState ConwayEra)
    -> Term (ProposalProcedure ConwayEra))
-> Term (GovActionState ConwayEra)
-> Term (GovAction ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ (Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra))
-> Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra)
forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gas)
        -- ParameterChange
        ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
           (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
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
            (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
            (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
         (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
              (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
forall a b. (a -> b) -> a -> b
$ \TermD
  Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
mPrevActionId Term (PParamsUpdate ConwayEra)
_ TermD Deps (StrictMaybe ScriptHash)
_ ->
            TermD
  Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases
           (SimpleRep
              (StrictMaybe (GovPurposeId 'PParamUpdatePurpose 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
              TermD
  Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
mPrevActionId
              (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ()
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 ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Term (StrictMaybe GovActionId) -> Pred
k Term (StrictMaybe GovActionId)
forall a. (HasSpec a, IsNormalType a) => Term (StrictMaybe a)
cSNothing_)
              (FunTy
  (MapList Term (Args (GovPurposeId 'PParamUpdatePurpose ConwayEra)))
  Pred
-> Weighted
     (BinderD Deps) (GovPurposeId 'PParamUpdatePurpose 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 (GovPurposeId 'PParamUpdatePurpose ConwayEra)))
   Pred
 -> Weighted
      (BinderD Deps) (GovPurposeId 'PParamUpdatePurpose ConwayEra))
-> FunTy
     (MapList Term (Args (GovPurposeId 'PParamUpdatePurpose ConwayEra)))
     Pred
-> Weighted
     (BinderD Deps) (GovPurposeId 'PParamUpdatePurpose ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (GovPurposeId 'PParamUpdatePurpose ConwayEra)
i -> Term (StrictMaybe GovActionId) -> Pred
k (Term GovActionId -> Term (StrictMaybe GovActionId)
forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ (Term GovActionId -> Term (StrictMaybe GovActionId))
-> Term GovActionId -> Term (StrictMaybe GovActionId)
forall a b. (a -> b) -> a -> b
$ Term (GovPurposeId 'PParamUpdatePurpose ConwayEra)
-> Term (SimpleRep (GovPurposeId 'PParamUpdatePurpose ConwayEra))
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (GovPurposeId 'PParamUpdatePurpose ConwayEra)
i))
        )
        -- HardForkInitiation
        ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)
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
            (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)
forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
mPrevActionId Term ProtVer
_ ->
            Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases
           (SimpleRep
              (StrictMaybe (GovPurposeId 'HardForkPurpose 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 (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
mPrevActionId
              (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ()
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 ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Term (StrictMaybe GovActionId) -> Pred
k Term (StrictMaybe GovActionId)
forall a. (HasSpec a, IsNormalType a) => Term (StrictMaybe a)
cSNothing_)
              (FunTy
  (MapList Term (Args (GovPurposeId 'HardForkPurpose ConwayEra)))
  Pred
-> Weighted
     (BinderD Deps) (GovPurposeId 'HardForkPurpose 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 (GovPurposeId 'HardForkPurpose ConwayEra)))
   Pred
 -> Weighted
      (BinderD Deps) (GovPurposeId 'HardForkPurpose ConwayEra))
-> FunTy
     (MapList Term (Args (GovPurposeId 'HardForkPurpose ConwayEra)))
     Pred
-> Weighted
     (BinderD Deps) (GovPurposeId 'HardForkPurpose ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (GovPurposeId 'HardForkPurpose ConwayEra)
i -> Term (StrictMaybe GovActionId) -> Pred
k (Term GovActionId -> Term (StrictMaybe GovActionId)
forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ (Term GovActionId -> Term (StrictMaybe GovActionId))
-> Term GovActionId -> Term (StrictMaybe GovActionId)
forall a b. (a -> b) -> a -> b
$ Term (GovPurposeId 'HardForkPurpose ConwayEra)
-> Term (SimpleRep (GovPurposeId 'HardForkPurpose ConwayEra))
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (GovPurposeId 'HardForkPurpose ConwayEra)
i))
        )
        -- TreasuryWithdrawals
        (FunTy
  (MapList
     Term
     (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
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 (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash)))
-> FunTy
     (MapList
        Term
        (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (Map RewardAccount Coin)
_ TermD Deps (StrictMaybe ScriptHash)
_ -> Bool
True)
        -- NoConfidence
        --   !(StrictMaybe (PrevGovActionId 'CommitteePurpose (EraCrypto era)))
        ( FunTy
  (MapList
     Term
     (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
  Pred
-> Weighted
     (BinderD Deps)
     (StrictMaybe (GovPurposeId 'CommitteePurpose 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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
   Pred
 -> Weighted
      (BinderD Deps)
      (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
     Pred
-> Weighted
     (BinderD Deps)
     (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId ->
            TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases
           (SimpleRep
              (StrictMaybe (GovPurposeId 'CommitteePurpose 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
              TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId
              (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ()
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 ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Term (StrictMaybe GovActionId) -> Pred
k Term (StrictMaybe GovActionId)
forall a. (HasSpec a, IsNormalType a) => Term (StrictMaybe a)
cSNothing_)
              (FunTy
  (MapList Term (Args (GovPurposeId 'CommitteePurpose ConwayEra)))
  Pred
-> Weighted
     (BinderD Deps) (GovPurposeId 'CommitteePurpose 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 (GovPurposeId 'CommitteePurpose ConwayEra)))
   Pred
 -> Weighted
      (BinderD Deps) (GovPurposeId 'CommitteePurpose ConwayEra))
-> FunTy
     (MapList Term (Args (GovPurposeId 'CommitteePurpose ConwayEra)))
     Pred
-> Weighted
     (BinderD Deps) (GovPurposeId 'CommitteePurpose ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (GovPurposeId 'CommitteePurpose ConwayEra)
i -> Term (StrictMaybe GovActionId) -> Pred
k (Term GovActionId -> Term (StrictMaybe GovActionId)
forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ (Term GovActionId -> Term (StrictMaybe GovActionId))
-> Term GovActionId -> Term (StrictMaybe GovActionId)
forall a b. (a -> b) -> a -> b
$ Term (GovPurposeId 'CommitteePurpose ConwayEra)
-> Term (SimpleRep (GovPurposeId 'CommitteePurpose ConwayEra))
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
        ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
           (Prod
              (Set (Credential 'ColdCommitteeRole))
              (Prod
                 (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
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
            (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
            (Prod
               (Set (Credential 'ColdCommitteeRole))
               (Prod
                  (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
         (Prod
            (Set (Credential 'ColdCommitteeRole))
            (Prod
               (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
              (Prod
                 (Set (Credential 'ColdCommitteeRole))
                 (Prod
                    (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId TermD Deps (Set (Credential 'ColdCommitteeRole))
_ Term (Map (Credential 'ColdCommitteeRole) EpochNo)
_ TermD Deps UnitInterval
_ ->
            TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases
           (SimpleRep
              (StrictMaybe (GovPurposeId 'CommitteePurpose 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
              TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId
              (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ()
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 ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Term (StrictMaybe GovActionId) -> Pred
k Term (StrictMaybe GovActionId)
forall a. (HasSpec a, IsNormalType a) => Term (StrictMaybe a)
cSNothing_)
              (FunTy
  (MapList Term (Args (GovPurposeId 'CommitteePurpose ConwayEra)))
  Pred
-> Weighted
     (BinderD Deps) (GovPurposeId 'CommitteePurpose 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 (GovPurposeId 'CommitteePurpose ConwayEra)))
   Pred
 -> Weighted
      (BinderD Deps) (GovPurposeId 'CommitteePurpose ConwayEra))
-> FunTy
     (MapList Term (Args (GovPurposeId 'CommitteePurpose ConwayEra)))
     Pred
-> Weighted
     (BinderD Deps) (GovPurposeId 'CommitteePurpose ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (GovPurposeId 'CommitteePurpose ConwayEra)
i -> Term (StrictMaybe GovActionId) -> Pred
k (Term GovActionId -> Term (StrictMaybe GovActionId)
forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ (Term GovActionId -> Term (StrictMaybe GovActionId))
-> Term GovActionId -> Term (StrictMaybe GovActionId)
forall a b. (a -> b) -> a -> b
$ Term (GovPurposeId 'CommitteePurpose ConwayEra)
-> Term (SimpleRep (GovPurposeId 'CommitteePurpose ConwayEra))
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (GovPurposeId 'CommitteePurpose ConwayEra)
i))
        )
        -- NewConstitution
        --  !(StrictMaybe (PrevGovActionId 'ConstitutionPurpose (EraCrypto era)))
        --  !(Constitution era)
        ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
           (Constitution ConwayEra))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
        (Constitution 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
            (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
            (Constitution ConwayEra))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
         (Constitution ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
              (Constitution ConwayEra))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
        (Constitution ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD
  Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
mPrevActionId TermD Deps (Constitution ConwayEra)
_ ->
            TermD
  Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases
           (SimpleRep
              (StrictMaybe (GovPurposeId 'ConstitutionPurpose 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
              TermD
  Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
mPrevActionId
              (FunTy (MapList Term (Args ())) Pred -> Weighted (BinderD Deps) ()
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 ())) Pred -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Pred
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Term (StrictMaybe GovActionId) -> Pred
k Term (StrictMaybe GovActionId)
forall a. (HasSpec a, IsNormalType a) => Term (StrictMaybe a)
cSNothing_)
              (FunTy
  (MapList Term (Args (GovPurposeId 'ConstitutionPurpose ConwayEra)))
  Pred
-> Weighted
     (BinderD Deps) (GovPurposeId 'ConstitutionPurpose 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 (GovPurposeId 'ConstitutionPurpose ConwayEra)))
   Pred
 -> Weighted
      (BinderD Deps) (GovPurposeId 'ConstitutionPurpose ConwayEra))
-> FunTy
     (MapList Term (Args (GovPurposeId 'ConstitutionPurpose ConwayEra)))
     Pred
-> Weighted
     (BinderD Deps) (GovPurposeId 'ConstitutionPurpose ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (GovPurposeId 'ConstitutionPurpose ConwayEra)
i -> Term (StrictMaybe GovActionId) -> Pred
k (Term GovActionId -> Term (StrictMaybe GovActionId)
forall a.
(HasSpec a, IsNormalType a) =>
Term a -> Term (StrictMaybe a)
cSJust_ (Term GovActionId -> Term (StrictMaybe GovActionId))
-> Term GovActionId -> Term (StrictMaybe GovActionId)
forall a b. (a -> b) -> a -> b
$ Term (GovPurposeId 'ConstitutionPurpose ConwayEra)
-> Term (SimpleRep (GovPurposeId 'ConstitutionPurpose ConwayEra))
forall a. GenericRequires a => Term a -> Term (SimpleRep a)
toGeneric_ Term (GovPurposeId 'ConstitutionPurpose ConwayEra)
i))
        )
        -- InfoAction
        (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
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 ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> 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),
 GenericRequires 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_ (Term (ProposalProcedure ConwayEra) -> Term (GovAction ConwayEra))
-> (Term (GovActionState ConwayEra)
    -> Term (ProposalProcedure ConwayEra))
-> Term (GovActionState ConwayEra)
-> Term (GovAction ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (GovActionState ConwayEra)
-> Term (ProposalProcedure ConwayEra)
gasProposalProcedure_ (Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra))
-> Term (GovActionState ConwayEra) -> Term (GovAction ConwayEra)
forall a b. (a -> b) -> a -> b
$ Term (GovActionState ConwayEra)
gas) FunTy
  (MapList
     Term
     (ConstrOf "HardForkInitiation" (TheSop (GovAction ConwayEra))))
  p
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 {StrictMaybe ScriptHash
PParams ConwayEra
CertState ConwayEra
TxId
EpochNo
geEpoch :: forall era. GovEnv era -> EpochNo
gePPolicy :: forall era. GovEnv era -> StrictMaybe ScriptHash
geCertState :: forall era. GovEnv era -> CertState era
geTxId :: TxId
geEpoch :: EpochNo
gePParams :: PParams ConwayEra
gePPolicy :: StrictMaybe ScriptHash
geCertState :: CertState ConwayEra
geTxId :: forall era. GovEnv era -> TxId
gePParams :: forall era. GovEnv era -> PParams era
..} Proposals ConwayEra
ps =
  let actions :: (GovAction ConwayEra -> Bool) -> [GovActionId]
actions GovAction ConwayEra -> Bool
f =
        [ GovActionId
gid
        | (GovActionId
gid, GovActionState ConwayEra
act) <- Map GovActionId (GovActionState ConwayEra)
-> [(GovActionId, GovActionState ConwayEra)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map GovActionId (GovActionState ConwayEra)
 -> [(GovActionId, GovActionState ConwayEra)])
-> Map GovActionId (GovActionState ConwayEra)
-> [(GovActionId, GovActionState ConwayEra)]
forall a b. (a -> b) -> a -> b
$ Proposals ConwayEra -> Map GovActionId (GovActionState ConwayEra)
forall era. Proposals era -> Map GovActionId (GovActionState era)
proposalsActionsMap Proposals ConwayEra
ps
        , EpochNo
geEpoch EpochNo -> EpochNo -> Bool
forall a. Ord a => a -> a -> Bool
<= GovActionState ConwayEra
act GovActionState ConwayEra
-> Getting EpochNo (GovActionState ConwayEra) EpochNo -> EpochNo
forall s a. s -> Getting a s a -> a
^. Getting EpochNo (GovActionState ConwayEra) EpochNo
forall era (f :: * -> *).
Functor f =>
(EpochNo -> f EpochNo)
-> GovActionState era -> f (GovActionState era)
gasExpiresAfterL
        , GovAction ConwayEra -> Bool
f (GovActionState ConwayEra -> GovAction ConwayEra
forall era. GovActionState era -> GovAction era
gasAction GovActionState ConwayEra
act)
        ]
      committeeState :: CommitteeState ConwayEra
committeeState = CertState ConwayEra
ConwayCertState ConwayEra
geCertState ConwayCertState ConwayEra
-> Getting
     (CommitteeState ConwayEra)
     (ConwayCertState ConwayEra)
     (CommitteeState ConwayEra)
-> CommitteeState ConwayEra
forall s a. s -> Getting a s a -> a
^. (VState ConwayEra
 -> Const (CommitteeState ConwayEra) (VState ConwayEra))
-> CertState ConwayEra
-> Const (CommitteeState ConwayEra) (CertState ConwayEra)
(VState ConwayEra
 -> Const (CommitteeState ConwayEra) (VState ConwayEra))
-> ConwayCertState ConwayEra
-> Const (CommitteeState ConwayEra) (ConwayCertState ConwayEra)
forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
Lens' (CertState ConwayEra) (VState ConwayEra)
certVStateL ((VState ConwayEra
  -> Const (CommitteeState ConwayEra) (VState ConwayEra))
 -> ConwayCertState ConwayEra
 -> Const (CommitteeState ConwayEra) (ConwayCertState ConwayEra))
-> ((CommitteeState ConwayEra
     -> Const (CommitteeState ConwayEra) (CommitteeState ConwayEra))
    -> VState ConwayEra
    -> Const (CommitteeState ConwayEra) (VState ConwayEra))
-> Getting
     (CommitteeState ConwayEra)
     (ConwayCertState ConwayEra)
     (CommitteeState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CommitteeState ConwayEra
 -> Const (CommitteeState ConwayEra) (CommitteeState ConwayEra))
-> VState ConwayEra
-> Const (CommitteeState ConwayEra) (VState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(CommitteeState era -> f (CommitteeState era))
-> VState era -> f (VState era)
vsCommitteeStateL
      knownDReps :: Set (Credential 'DRepRole)
knownDReps = Map (Credential 'DRepRole) DRepState -> Set (Credential 'DRepRole)
forall k a. Map k a -> Set k
Map.keysSet (Map (Credential 'DRepRole) DRepState
 -> Set (Credential 'DRepRole))
-> Map (Credential 'DRepRole) DRepState
-> Set (Credential 'DRepRole)
forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
ConwayCertState ConwayEra
geCertState ConwayCertState ConwayEra
-> Getting
     (Map (Credential 'DRepRole) DRepState)
     (ConwayCertState ConwayEra)
     (Map (Credential 'DRepRole) DRepState)
-> Map (Credential 'DRepRole) DRepState
forall s a. s -> Getting a s a -> a
^. (VState ConwayEra
 -> Const (Map (Credential 'DRepRole) DRepState) (VState ConwayEra))
-> CertState ConwayEra
-> Const
     (Map (Credential 'DRepRole) DRepState) (CertState ConwayEra)
(VState ConwayEra
 -> Const (Map (Credential 'DRepRole) DRepState) (VState ConwayEra))
-> ConwayCertState ConwayEra
-> Const
     (Map (Credential 'DRepRole) DRepState) (ConwayCertState ConwayEra)
forall era.
ConwayEraCertState era =>
Lens' (CertState era) (VState era)
Lens' (CertState ConwayEra) (VState ConwayEra)
certVStateL ((VState ConwayEra
  -> Const (Map (Credential 'DRepRole) DRepState) (VState ConwayEra))
 -> ConwayCertState ConwayEra
 -> Const
      (Map (Credential 'DRepRole) DRepState) (ConwayCertState ConwayEra))
-> ((Map (Credential 'DRepRole) DRepState
     -> Const
          (Map (Credential 'DRepRole) DRepState)
          (Map (Credential 'DRepRole) DRepState))
    -> VState ConwayEra
    -> Const (Map (Credential 'DRepRole) DRepState) (VState ConwayEra))
-> Getting
     (Map (Credential 'DRepRole) DRepState)
     (ConwayCertState ConwayEra)
     (Map (Credential 'DRepRole) DRepState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'DRepRole) DRepState
 -> Const
      (Map (Credential 'DRepRole) DRepState)
      (Map (Credential 'DRepRole) DRepState))
-> VState ConwayEra
-> Const (Map (Credential 'DRepRole) DRepState) (VState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(Map (Credential 'DRepRole) DRepState
 -> f (Map (Credential 'DRepRole) DRepState))
-> VState era -> f (VState era)
vsDRepsL
      knownStakePools :: Set (KeyHash 'StakePool)
knownStakePools = Map (KeyHash 'StakePool) PoolParams -> Set (KeyHash 'StakePool)
forall k a. Map k a -> Set k
Map.keysSet (Map (KeyHash 'StakePool) PoolParams -> Set (KeyHash 'StakePool))
-> Map (KeyHash 'StakePool) PoolParams -> Set (KeyHash 'StakePool)
forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
ConwayCertState ConwayEra
geCertState ConwayCertState ConwayEra
-> Getting
     (Map (KeyHash 'StakePool) PoolParams)
     (ConwayCertState ConwayEra)
     (Map (KeyHash 'StakePool) PoolParams)
-> Map (KeyHash 'StakePool) PoolParams
forall s a. s -> Getting a s a -> a
^. (PState ConwayEra
 -> Const (Map (KeyHash 'StakePool) PoolParams) (PState ConwayEra))
-> CertState ConwayEra
-> Const
     (Map (KeyHash 'StakePool) PoolParams) (CertState ConwayEra)
(PState ConwayEra
 -> Const (Map (KeyHash 'StakePool) PoolParams) (PState ConwayEra))
-> ConwayCertState ConwayEra
-> Const
     (Map (KeyHash 'StakePool) PoolParams) (ConwayCertState ConwayEra)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState ConwayEra) (PState ConwayEra)
certPStateL ((PState ConwayEra
  -> Const (Map (KeyHash 'StakePool) PoolParams) (PState ConwayEra))
 -> ConwayCertState ConwayEra
 -> Const
      (Map (KeyHash 'StakePool) PoolParams) (ConwayCertState ConwayEra))
-> ((Map (KeyHash 'StakePool) PoolParams
     -> Const
          (Map (KeyHash 'StakePool) PoolParams)
          (Map (KeyHash 'StakePool) PoolParams))
    -> PState ConwayEra
    -> Const (Map (KeyHash 'StakePool) PoolParams) (PState ConwayEra))
-> Getting
     (Map (KeyHash 'StakePool) PoolParams)
     (ConwayCertState ConwayEra)
     (Map (KeyHash 'StakePool) PoolParams)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) PoolParams
 -> Const
      (Map (KeyHash 'StakePool) PoolParams)
      (Map (KeyHash 'StakePool) PoolParams))
-> PState ConwayEra
-> Const (Map (KeyHash 'StakePool) PoolParams) (PState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) PoolParams
 -> f (Map (KeyHash 'StakePool) PoolParams))
-> PState era -> f (PState era)
psStakePoolParamsL
      knownCommitteeAuthorizations :: Set (Credential 'HotCommitteeRole)
knownCommitteeAuthorizations = CommitteeState ConwayEra -> Set (Credential 'HotCommitteeRole)
forall era.
CommitteeState era -> Set (Credential 'HotCommitteeRole)
authorizedHotCommitteeCredentials CommitteeState ConwayEra
committeeState
      committeeVotableActionIds :: [GovActionId]
committeeVotableActionIds =
        (GovAction ConwayEra -> Bool) -> [GovActionId]
actions (EpochNo -> CommitteeState ConwayEra -> GovAction ConwayEra -> Bool
forall era.
ConwayEraPParams era =>
EpochNo -> CommitteeState era -> GovAction era -> Bool
isCommitteeVotingAllowed EpochNo
geEpoch CommitteeState ConwayEra
committeeState)
      drepVotableActionIds :: [GovActionId]
drepVotableActionIds =
        (GovAction ConwayEra -> Bool) -> [GovActionId]
actions GovAction ConwayEra -> Bool
forall era. ConwayEraPParams era => GovAction era -> Bool
isDRepVotingAllowed
      stakepoolVotableActionIds :: [GovActionId]
stakepoolVotableActionIds =
        (GovAction ConwayEra -> Bool) -> [GovActionId]
actions GovAction ConwayEra -> Bool
forall era. ConwayEraPParams era => GovAction era -> Bool
isStakePoolVotingAllowed
      registeredCredentials :: Set (Credential 'Staking)
registeredCredentials = Map (Credential 'Staking) UMElem -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet (Map (Credential 'Staking) UMElem -> Set (Credential 'Staking))
-> Map (Credential 'Staking) UMElem -> Set (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
ConwayCertState ConwayEra
geCertState ConwayCertState ConwayEra
-> Getting
     (Map (Credential 'Staking) UMElem)
     (ConwayCertState ConwayEra)
     (Map (Credential 'Staking) UMElem)
-> Map (Credential 'Staking) UMElem
forall s a. s -> Getting a s a -> a
^. (DState ConwayEra
 -> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra))
-> CertState ConwayEra
-> Const (Map (Credential 'Staking) UMElem) (CertState ConwayEra)
(DState ConwayEra
 -> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra))
-> ConwayCertState ConwayEra
-> Const
     (Map (Credential 'Staking) UMElem) (ConwayCertState ConwayEra)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState ConwayEra) (DState ConwayEra)
certDStateL ((DState ConwayEra
  -> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra))
 -> ConwayCertState ConwayEra
 -> Const
      (Map (Credential 'Staking) UMElem) (ConwayCertState ConwayEra))
-> ((Map (Credential 'Staking) UMElem
     -> Const
          (Map (Credential 'Staking) UMElem)
          (Map (Credential 'Staking) UMElem))
    -> DState ConwayEra
    -> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra))
-> Getting
     (Map (Credential 'Staking) UMElem)
     (ConwayCertState ConwayEra)
     (Map (Credential 'Staking) UMElem)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UMap -> Const (Map (Credential 'Staking) UMElem) UMap)
-> DState ConwayEra
-> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(UMap -> f UMap) -> DState era -> f (DState era)
dsUnifiedL ((UMap -> Const (Map (Credential 'Staking) UMElem) UMap)
 -> DState ConwayEra
 -> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra))
-> ((Map (Credential 'Staking) UMElem
     -> Const
          (Map (Credential 'Staking) UMElem)
          (Map (Credential 'Staking) UMElem))
    -> UMap -> Const (Map (Credential 'Staking) UMElem) UMap)
-> (Map (Credential 'Staking) UMElem
    -> Const
         (Map (Credential 'Staking) UMElem)
         (Map (Credential 'Staking) UMElem))
-> DState ConwayEra
-> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'Staking) UMElem
 -> Const
      (Map (Credential 'Staking) UMElem)
      (Map (Credential 'Staking) UMElem))
-> UMap -> Const (Map (Credential 'Staking) UMElem) UMap
Lens' UMap (Map (Credential 'Staking) UMElem)
umElemsL
   in (Term (GovSignal ConwayEra) -> Pred)
-> Specification (GovSignal ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (GovSignal ConwayEra) -> Pred)
 -> Specification (GovSignal ConwayEra))
-> (Term (GovSignal ConwayEra) -> Pred)
-> Specification (GovSignal ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (GovSignal ConwayEra)
govSignal ->
        Term (GovSignal ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (GovSignal 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 (GovSignal ConwayEra)
govSignal (FunTy (MapList Term (ProductAsList (GovSignal ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (GovSignal ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (VotingProcedures ConwayEra)
votingProcs Term (OSet (ProposalProcedure ConwayEra))
proposalProcs TermD Deps (StrictSeq (ConwayTxCert ConwayEra))
_certificates ->
          [ Term (VotingProcedures ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (VotingProcedures 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 (VotingProcedures ConwayEra)
votingProcs (FunTy
   (MapList Term (ProductAsList (VotingProcedures ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (VotingProcedures ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Map Voter (Map GovActionId (VotingProcedure ConwayEra)))
votingProcsMap ->
              Term (Map Voter (Map GovActionId (VotingProcedure ConwayEra)))
-> (Term (Voter, Map GovActionId (VotingProcedure ConwayEra))
    -> Pred)
-> Pred
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 ((Term (Voter, Map GovActionId (VotingProcedure ConwayEra))
  -> Pred)
 -> Pred)
-> (Term (Voter, Map GovActionId (VotingProcedure ConwayEra))
    -> Pred)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Voter, Map GovActionId (VotingProcedure ConwayEra))
kvp ->
                Term (Voter, Map GovActionId (VotingProcedure ConwayEra))
-> FunTy
     (MapList
        Term
        (ProductAsList
           (Voter, Map GovActionId (VotingProcedure 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 (Voter, Map GovActionId (VotingProcedure ConwayEra))
kvp (FunTy
   (MapList
      Term
      (ProductAsList
         (Voter, Map GovActionId (VotingProcedure ConwayEra))))
   Pred
 -> Pred)
-> FunTy
     (MapList
        Term
        (ProductAsList
           (Voter, Map GovActionId (VotingProcedure ConwayEra))))
     Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Voter
voter Term (Map GovActionId (VotingProcedure ConwayEra))
mapActVote ->
                  (Term Voter
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep Voter))) 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 Voter
voter)
                    ( FunTy
  (MapList Term (Args (Credential 'HotCommitteeRole))) [Term Bool]
-> Weighted (BinderD Deps) (Credential 'HotCommitteeRole)
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 (Credential 'HotCommitteeRole))) [Term Bool]
 -> Weighted (BinderD Deps) (Credential 'HotCommitteeRole))
-> FunTy
     (MapList Term (Args (Credential 'HotCommitteeRole))) [Term Bool]
-> Weighted (BinderD Deps) (Credential 'HotCommitteeRole)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'HotCommitteeRole)
committeeHotCred ->
                        [ Term (Set GovActionId) -> Term (Set GovActionId) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map GovActionId (VotingProcedure ConwayEra))
-> Term (Set GovActionId)
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) (Set GovActionId -> Term (Set GovActionId)
forall a. HasSpec a => a -> Term a
lit (Set GovActionId -> Term (Set GovActionId))
-> Set GovActionId -> Term (Set GovActionId)
forall a b. (a -> b) -> a -> b
$ [GovActionId] -> Set GovActionId
forall a. Ord a => [a] -> Set a
Set.fromList [GovActionId]
committeeVotableActionIds)
                        , Term (Credential 'HotCommitteeRole)
-> Term (Set (Credential 'HotCommitteeRole)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'HotCommitteeRole)
committeeHotCred (Term (Set (Credential 'HotCommitteeRole)) -> Term Bool)
-> Term (Set (Credential 'HotCommitteeRole)) -> Term Bool
forall a b. (a -> b) -> a -> b
$ Set (Credential 'HotCommitteeRole)
-> Term (Set (Credential 'HotCommitteeRole))
forall a. HasSpec a => a -> Term a
lit Set (Credential 'HotCommitteeRole)
knownCommitteeAuthorizations
                        ]
                    )
                    ( FunTy (MapList Term (Args (Credential 'DRepRole))) [Term Bool]
-> Weighted (BinderD Deps) (Credential 'DRepRole)
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 (Credential 'DRepRole))) [Term Bool]
 -> Weighted (BinderD Deps) (Credential 'DRepRole))
-> FunTy (MapList Term (Args (Credential 'DRepRole))) [Term Bool]
-> Weighted (BinderD Deps) (Credential 'DRepRole)
forall a b. (a -> b) -> a -> b
$ \Term (Credential 'DRepRole)
drepCred ->
                        [ Term (Set GovActionId) -> Term (Set GovActionId) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map GovActionId (VotingProcedure ConwayEra))
-> Term (Set GovActionId)
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) (Set GovActionId -> Term (Set GovActionId)
forall a. HasSpec a => a -> Term a
lit (Set GovActionId -> Term (Set GovActionId))
-> Set GovActionId -> Term (Set GovActionId)
forall a b. (a -> b) -> a -> b
$ [GovActionId] -> Set GovActionId
forall a. Ord a => [a] -> Set a
Set.fromList [GovActionId]
drepVotableActionIds)
                        , Term (Credential 'DRepRole)
-> Term (Set (Credential 'DRepRole)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (Credential 'DRepRole)
drepCred (Term (Set (Credential 'DRepRole)) -> Term Bool)
-> Term (Set (Credential 'DRepRole)) -> Term Bool
forall a b. (a -> b) -> a -> b
$ Set (Credential 'DRepRole) -> Term (Set (Credential 'DRepRole))
forall a. HasSpec a => a -> Term a
lit Set (Credential 'DRepRole)
knownDReps
                        ]
                    )
                    ( FunTy (MapList Term (Args (KeyHash 'StakePool))) [Term Bool]
-> Weighted (BinderD Deps) (KeyHash 'StakePool)
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 (KeyHash 'StakePool))) [Term Bool]
 -> Weighted (BinderD Deps) (KeyHash 'StakePool))
-> FunTy (MapList Term (Args (KeyHash 'StakePool))) [Term Bool]
-> Weighted (BinderD Deps) (KeyHash 'StakePool)
forall a b. (a -> b) -> a -> b
$ \Term (KeyHash 'StakePool)
poolKeyHash ->
                        [ Term (Set GovActionId) -> Term (Set GovActionId) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ (Term (Map GovActionId (VotingProcedure ConwayEra))
-> Term (Set GovActionId)
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) (Set GovActionId -> Term (Set GovActionId)
forall a. HasSpec a => a -> Term a
lit (Set GovActionId -> Term (Set GovActionId))
-> Set GovActionId -> Term (Set GovActionId)
forall a b. (a -> b) -> a -> b
$ [GovActionId] -> Set GovActionId
forall a. Ord a => [a] -> Set a
Set.fromList [GovActionId]
stakepoolVotableActionIds)
                        , Term (KeyHash 'StakePool)
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ Term (KeyHash 'StakePool)
poolKeyHash (Term (Set (KeyHash 'StakePool)) -> Term Bool)
-> Term (Set (KeyHash 'StakePool)) -> Term Bool
forall a b. (a -> b) -> a -> b
$ Set (KeyHash 'StakePool) -> Term (Set (KeyHash 'StakePool))
forall a. HasSpec a => a -> Term a
lit Set (KeyHash 'StakePool)
knownStakePools
                        ]
                    )
          , Term (OSet (ProposalProcedure ConwayEra))
-> (Term (ProposalProcedure ConwayEra) -> Pred) -> Pred
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 ((Term (ProposalProcedure ConwayEra) -> Pred) -> Pred)
-> (Term (ProposalProcedure ConwayEra) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (ProposalProcedure ConwayEra)
proc ->
              Term (ProposalProcedure ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (ProposalProcedure 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 (ProposalProcedure ConwayEra)
proc (FunTy
   (MapList Term (ProductAsList (ProposalProcedure ConwayEra))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (ProposalProcedure ConwayEra))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps Coin
deposit Term RewardAccount
returnAddr Term (GovAction ConwayEra)
govAction TermD Deps Anchor
_ ->
                [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps Coin
deposit TermD Deps Coin -> TermD Deps Coin -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Coin -> TermD Deps Coin
forall a. HasSpec a => a -> Term a
lit (PParams ConwayEra
gePParams PParams ConwayEra -> Getting Coin (PParams ConwayEra) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (PParams ConwayEra) Coin
forall era. ConwayEraPParams era => Lens' (PParams era) Coin
Lens' (PParams ConwayEra) Coin
ppGovActionDepositL)
                , Term RewardAccount
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
returnAddr (FunTy (MapList Term (ProductAsList RewardAccount)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Network
net Term (Credential 'Staking)
cred ->
                    [ Term (ProposalProcedure ConwayEra) -> Term Network -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
dependsOn Term (ProposalProcedure ConwayEra)
proc Term Network
net
                    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Network
net Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit Network
Testnet
                    , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Credential 'Staking)
cred Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
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 :: forall era. GovEnv era -> StrictMaybe ScriptHash
gePPolicy :: StrictMaybe ScriptHash
gePPolicy, EpochNo
geEpoch :: forall era. GovEnv era -> EpochNo
geEpoch :: EpochNo
geEpoch, PParams ConwayEra
gePParams :: forall era. GovEnv era -> PParams era
gePParams :: PParams ConwayEra
gePParams, CertState ConwayEra
geCertState :: forall era. GovEnv era -> CertState era
geCertState :: CertState ConwayEra
geCertState} Proposals ConwayEra
ps Term (GovAction ConwayEra)
govAction =
  Term (GovAction ConwayEra)
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (GovAction 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 (GovAction ConwayEra)
govAction
    -- ParameterChange
    ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
           (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
  [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
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
            (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
            (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
         (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
              (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
forall a b. (a -> b) -> a -> b
$ \TermD
  Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
mPrevActionId Term (PParamsUpdate ConwayEra)
ppUpdate TermD Deps (StrictMaybe ScriptHash)
policy ->
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD
  Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
mPrevActionId TermD
  Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
-> Term [StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)]
-> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)]
-> Term [StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)]
forall a. HasSpec a => a -> Term a
lit [StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)]
ppupIds
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (PParamsUpdate ConwayEra)
ppUpdate Term (PParamsUpdate ConwayEra)
-> Term (PParamsUpdate ConwayEra) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
/=. PParamsUpdate ConwayEra -> Term (PParamsUpdate ConwayEra)
forall a. HasSpec a => a -> Term a
lit PParamsUpdate ConwayEra
forall era. EraPParams era => PParamsUpdate era
emptyPParamsUpdate
        , Term (PParamsUpdate ConwayEra)
-> Specification (PParamsUpdate ConwayEra) -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (PParamsUpdate ConwayEra)
ppUpdate Specification (PParamsUpdate ConwayEra)
wfPParamsUpdateSpec
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps (StrictMaybe ScriptHash)
policy TermD Deps (StrictMaybe ScriptHash)
-> TermD Deps (StrictMaybe ScriptHash) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. StrictMaybe ScriptHash -> TermD Deps (StrictMaybe ScriptHash)
forall a. HasSpec a => a -> Term a
lit StrictMaybe ScriptHash
gePPolicy
        ]
    )
    -- HardForkInitiation
    ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
  [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)
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
            (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)) ProtVer)
forall a b. (a -> b) -> a -> b
$ \ Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
[var|mPrevActionId|] Term ProtVer
[var|protVer|] ->
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
mPrevActionId Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
-> Term [StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)]
-> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)]
-> Term [StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)]
forall a. HasSpec a => a -> Term a
lit [StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)]
hardForkIds
        , Term ProtVer
-> FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term ProtVer
protVer (FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Version
[var|majorVersion|] Term Natural
[var|minorVersion|] ->
            Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
-> (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)
    -> (Version, Maybe Version))
-> (Term (Version, Maybe Version) -> Pred)
-> Pred
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 StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)
-> (Version, Maybe Version)
forall {p}.
Coercible p (StrictMaybe GovActionId) =>
p -> (Version, Maybe Version)
hfIdMajorVer ((Term (Version, Maybe Version) -> Pred) -> Pred)
-> (Term (Version, Maybe Version) -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Version, Maybe Version)
[var|pvpair|] -> Term (Version, Maybe Version)
-> FunTy
     (MapList Term (ProductAsList (Version, Maybe Version))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Version, Maybe Version)
pvpair (FunTy (MapList Term (ProductAsList (Version, Maybe Version))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (Version, Maybe Version))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Version
[var|currentMajorVersion|] Term (Maybe Version)
[var|mSuccMajorVersion|] ->
              Term (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
-> (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)
    -> Natural)
-> (Term Natural -> Pred)
-> Pred
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 StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra) -> Natural
forall {p}. Coercible p (StrictMaybe GovActionId) => p -> Natural
hfIdMinorVer ((Term Natural -> Pred) -> Pred) -> (Term Natural -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Natural
[var|currentMinorVersion|] ->
                Term (Maybe Version)
-> FunTy
     (MapList
        (Weighted (BinderD Deps)) (Cases (SimpleRep (Maybe Version))))
     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 (Maybe Version)
mSuccMajorVersion
                  ( FunTy (MapList Term (Args ())) [Term Bool]
-> Weighted (BinderD Deps) ()
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 ())) [Term Bool]
 -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) [Term Bool]
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ ->
                      [ Term Version
majorVersion Term Version -> Term Version -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Version
currentMajorVersion
                      , Term Natural
minorVersion Term Natural -> Term Natural -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
currentMinorVersion Term Natural -> Term Natural -> Term Natural
forall a. Num a => a -> a -> a
+ Term Natural
1
                      ]
                  )
                  ( FunTy (MapList Term (Args Version)) [Pred]
-> Weighted (BinderD Deps) Version
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 Version)) [Pred]
 -> Weighted (BinderD Deps) Version)
-> FunTy (MapList Term (Args Version)) [Pred]
-> Weighted (BinderD Deps) Version
forall a b. (a -> b) -> a -> b
$ \ Term Version
[var|majorVersionPrime|] ->
                      [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Version
majorVersion Term Version -> Term (Set Version) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` (Term Version -> Term (Set Version)
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ Term Version
currentMajorVersion Term (Set Version) -> Term (Set Version) -> Term (Set Version)
forall a. Semigroup a => a -> a -> a
<> Term Version -> Term (Set Version)
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a)
singleton_ Term Version
majorVersionPrime)
                      , Term Bool -> Term Bool -> Term Bool -> Pred
forall p q. (IsPred p, IsPred q) => Term Bool -> p -> q -> Pred
ifElse
                          (Term Version
currentMajorVersion Term Version -> Term Version -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. Term Version
majorVersion)
                          (Term Natural
minorVersion Term Natural -> Term Natural -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
0)
                          (Term Natural
minorVersion Term Natural -> Term Natural -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term Natural
currentMinorVersion Term Natural -> Term Natural -> Term Natural
forall a. Num a => a -> a -> a
+ Term Natural
1)
                      ]
                  )
        ]
    )
    -- TreasuryWithdrawals
    ( FunTy
  (MapList
     Term
     (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
  [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
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 (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash)))
-> FunTy
     (MapList
        Term
        (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (Map RewardAccount Coin)
withdrawMap TermD Deps (StrictMaybe ScriptHash)
policy ->
        [ Term (Set RewardAccount) -> (Term RewardAccount -> Pred) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (TermD Deps (Map RewardAccount Coin) -> Term (Set RewardAccount)
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_ TermD Deps (Map RewardAccount Coin)
withdrawMap) ((Term RewardAccount -> Pred) -> Pred)
-> (Term RewardAccount -> Pred) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term RewardAccount
rewAcnt ->
            Term RewardAccount
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
rewAcnt (FunTy (MapList Term (ProductAsList RewardAccount)) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Network
net Term (Credential 'Staking)
cred ->
              [ Term Network
net Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit Network
Testnet
              , Term (Credential 'Staking)
cred Term (Credential 'Staking)
-> Term (Set (Credential 'Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
`member_` Set (Credential 'Staking) -> Term (Set (Credential 'Staking))
forall a. HasSpec a => a -> Term a
lit Set (Credential 'Staking)
registeredCredentials
              ]
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [Coin] -> TermD Deps Coin
forall a. Foldy a => Term [a] -> Term a
sum_ (TermD Deps (Map RewardAccount Coin) -> Term [Coin]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ TermD Deps (Map RewardAccount Coin)
withdrawMap) TermD Deps Coin -> TermD Deps Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
>. Coin -> TermD Deps Coin
forall a. HasSpec a => a -> Term a
lit (Integer -> Coin
Coin Integer
0)
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps (StrictMaybe ScriptHash)
policy TermD Deps (StrictMaybe ScriptHash)
-> TermD Deps (StrictMaybe ScriptHash) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. StrictMaybe ScriptHash -> TermD Deps (StrictMaybe ScriptHash)
forall a. HasSpec a => a -> Term a
lit StrictMaybe ScriptHash
gePPolicy
        , Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Bool -> Pred) -> Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ProtVer -> Bool
HardForks.bootstrapPhase (PParams ConwayEra
gePParams PParams ConwayEra
-> Getting ProtVer (PParams ConwayEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams ConwayEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL)
        ]
    )
    -- NoConfidence
    ( FunTy
  (MapList
     Term
     (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
  [Pred]
-> Weighted
     (BinderD Deps)
     (StrictMaybe (GovPurposeId 'CommitteePurpose 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 (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId ->
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
-> Term [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
-> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
-> Term [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
forall a. HasSpec a => a -> Term a
lit [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
committeeIds
        , Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Bool -> Pred) -> Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ProtVer -> Bool
HardForks.bootstrapPhase (PParams ConwayEra
gePParams PParams ConwayEra
-> Getting ProtVer (PParams ConwayEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams ConwayEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL)
        ]
    )
    -- UpdateCommittee
    ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
           (Prod
              (Set (Credential 'ColdCommitteeRole))
              (Prod
                 (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
  [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
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
            (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
            (Prod
               (Set (Credential 'ColdCommitteeRole))
               (Prod
                  (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
         (Prod
            (Set (Credential 'ColdCommitteeRole))
            (Prod
               (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
              (Prod
                 (Set (Credential 'ColdCommitteeRole))
                 (Prod
                    (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
        (Prod
           (Set (Credential 'ColdCommitteeRole))
           (Prod (Map (Credential 'ColdCommitteeRole) EpochNo) UnitInterval)))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId TermD Deps (Set (Credential 'ColdCommitteeRole))
_removed Term (Map (Credential 'ColdCommitteeRole) EpochNo)
added TermD Deps UnitInterval
_quorum ->
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
-> Term [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
-> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
-> Term [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
forall a. HasSpec a => a -> Term a
lit [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
committeeIds
        , Term [EpochNo] -> (TermD Deps EpochNo -> Term Bool) -> Pred
forall t a p.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map (Credential 'ColdCommitteeRole) EpochNo)
-> Term [EpochNo]
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) ((TermD Deps EpochNo -> Term Bool) -> Pred)
-> (TermD Deps EpochNo -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \TermD Deps EpochNo
epoch ->
            EpochNo -> TermD Deps EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
geEpoch TermD Deps EpochNo -> TermD Deps EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<. TermD Deps EpochNo
epoch
        , Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Bool -> Pred) -> Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ProtVer -> Bool
HardForks.bootstrapPhase (PParams ConwayEra
gePParams PParams ConwayEra
-> Getting ProtVer (PParams ConwayEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams ConwayEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL)
        ]
    )
    -- NewConstitution
    ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
           (Constitution ConwayEra))))
  [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
        (Constitution 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
            (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
            (Constitution ConwayEra))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
         (Constitution ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
              (Constitution ConwayEra))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
        (Constitution ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD
  Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
mPrevActionId TermD Deps (Constitution ConwayEra)
_c ->
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ TermD
  Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
mPrevActionId TermD
  Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
-> Term [StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)]
-> Term Bool
forall a. (Sized [a], HasSpec a) => Term a -> Term [a] -> Term Bool
`elem_` [StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)]
-> Term [StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)]
forall a. HasSpec a => a -> Term a
lit [StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)]
constitutionIds
        , Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Bool -> Pred) -> Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ProtVer -> Bool
HardForks.bootstrapPhase (PParams ConwayEra
gePParams PParams ConwayEra
-> Getting ProtVer (PParams ConwayEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams ConwayEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL)
        ]
    )
    -- InfoAction
    (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
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 ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
  where
    registeredCredentials :: Set (Credential 'Staking)
registeredCredentials = Map (Credential 'Staking) UMElem -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet (Map (Credential 'Staking) UMElem -> Set (Credential 'Staking))
-> Map (Credential 'Staking) UMElem -> Set (Credential 'Staking)
forall a b. (a -> b) -> a -> b
$ CertState ConwayEra
ConwayCertState ConwayEra
geCertState ConwayCertState ConwayEra
-> Getting
     (Map (Credential 'Staking) UMElem)
     (ConwayCertState ConwayEra)
     (Map (Credential 'Staking) UMElem)
-> Map (Credential 'Staking) UMElem
forall s a. s -> Getting a s a -> a
^. (DState ConwayEra
 -> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra))
-> CertState ConwayEra
-> Const (Map (Credential 'Staking) UMElem) (CertState ConwayEra)
(DState ConwayEra
 -> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra))
-> ConwayCertState ConwayEra
-> Const
     (Map (Credential 'Staking) UMElem) (ConwayCertState ConwayEra)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState ConwayEra) (DState ConwayEra)
certDStateL ((DState ConwayEra
  -> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra))
 -> ConwayCertState ConwayEra
 -> Const
      (Map (Credential 'Staking) UMElem) (ConwayCertState ConwayEra))
-> ((Map (Credential 'Staking) UMElem
     -> Const
          (Map (Credential 'Staking) UMElem)
          (Map (Credential 'Staking) UMElem))
    -> DState ConwayEra
    -> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra))
-> Getting
     (Map (Credential 'Staking) UMElem)
     (ConwayCertState ConwayEra)
     (Map (Credential 'Staking) UMElem)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UMap -> Const (Map (Credential 'Staking) UMElem) UMap)
-> DState ConwayEra
-> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra)
forall era (f :: * -> *).
Functor f =>
(UMap -> f UMap) -> DState era -> f (DState era)
dsUnifiedL ((UMap -> Const (Map (Credential 'Staking) UMElem) UMap)
 -> DState ConwayEra
 -> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra))
-> ((Map (Credential 'Staking) UMElem
     -> Const
          (Map (Credential 'Staking) UMElem)
          (Map (Credential 'Staking) UMElem))
    -> UMap -> Const (Map (Credential 'Staking) UMElem) UMap)
-> (Map (Credential 'Staking) UMElem
    -> Const
         (Map (Credential 'Staking) UMElem)
         (Map (Credential 'Staking) UMElem))
-> DState ConwayEra
-> Const (Map (Credential 'Staking) UMElem) (DState ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (Credential 'Staking) UMElem
 -> Const
      (Map (Credential 'Staking) UMElem)
      (Map (Credential 'Staking) UMElem))
-> UMap -> Const (Map (Credential 'Staking) UMElem) UMap
Lens' UMap (Map (Credential 'Staking) UMElem)
umElemsL
    prevGovActionIds :: GovRelation StrictMaybe ConwayEra
prevGovActionIds = Proposals ConwayEra
ps Proposals ConwayEra
-> Getting
     (GovRelation StrictMaybe ConwayEra)
     (Proposals ConwayEra)
     (GovRelation StrictMaybe ConwayEra)
-> GovRelation StrictMaybe ConwayEra
forall s a. s -> Getting a s a -> a
^. (GovRelation PRoot ConwayEra
 -> Const
      (GovRelation StrictMaybe ConwayEra) (GovRelation PRoot ConwayEra))
-> Proposals ConwayEra
-> Const (GovRelation StrictMaybe ConwayEra) (Proposals ConwayEra)
forall era (f :: * -> *).
Functor f =>
(GovRelation PRoot era -> f (GovRelation PRoot era))
-> Proposals era -> f (Proposals era)
pRootsL ((GovRelation PRoot ConwayEra
  -> Const
       (GovRelation StrictMaybe ConwayEra) (GovRelation PRoot ConwayEra))
 -> Proposals ConwayEra
 -> Const (GovRelation StrictMaybe ConwayEra) (Proposals ConwayEra))
-> ((GovRelation StrictMaybe ConwayEra
     -> Const
          (GovRelation StrictMaybe ConwayEra)
          (GovRelation StrictMaybe ConwayEra))
    -> GovRelation PRoot ConwayEra
    -> Const
         (GovRelation StrictMaybe ConwayEra) (GovRelation PRoot ConwayEra))
-> Getting
     (GovRelation StrictMaybe ConwayEra)
     (Proposals ConwayEra)
     (GovRelation StrictMaybe ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GovRelation PRoot ConwayEra -> GovRelation StrictMaybe ConwayEra)
-> SimpleGetter
     (GovRelation PRoot ConwayEra) (GovRelation StrictMaybe ConwayEra)
forall s a. (s -> a) -> SimpleGetter s a
L.to GovRelation PRoot ConwayEra -> GovRelation StrictMaybe ConwayEra
forall era. GovRelation PRoot era -> GovRelation StrictMaybe era
toPrevGovActionIds
    constitutionIds :: [StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)]
constitutionIds =
      (GovRelation StrictMaybe ConwayEra
prevGovActionIds GovRelation StrictMaybe ConwayEra
-> Getting
     (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
     (GovRelation StrictMaybe ConwayEra)
     (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
  (GovRelation StrictMaybe ConwayEra)
  (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
forall (f1 :: * -> *) era (f2 :: * -> *).
Functor f2 =>
(f1 (GovPurposeId 'ConstitutionPurpose era)
 -> f2 (f1 (GovPurposeId 'ConstitutionPurpose era)))
-> GovRelation f1 era -> f2 (GovRelation f1 era)
grConstitutionL)
        StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)
-> [StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)]
-> [StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)]
forall a. a -> [a] -> [a]
: [ GovPurposeId 'ConstitutionPurpose ConwayEra
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)
forall a. a -> StrictMaybe a
SJust (GovPurposeId 'ConstitutionPurpose ConwayEra
 -> StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
-> GovPurposeId 'ConstitutionPurpose ConwayEra
-> StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra)
forall a b. (a -> b) -> a -> b
$ GovActionId -> GovPurposeId 'ConstitutionPurpose ConwayEra
forall a b. Coercible a b => a -> b
coerce (GovActionId -> GovPurposeId 'ConstitutionPurpose ConwayEra)
-> GovActionId -> GovPurposeId 'ConstitutionPurpose ConwayEra
forall a b. (a -> b) -> a -> b
$ GovActionState ConwayEra -> GovActionId
forall era. GovActionState era -> GovActionId
gasId GovActionState ConwayEra
gas
          | GovActionState ConwayEra
gas <- [GovActionState ConwayEra]
actions
          , NewConstitution {} <- [ProposalProcedure ConwayEra -> GovAction ConwayEra
forall era. ProposalProcedure era -> GovAction era
pProcGovAction (ProposalProcedure ConwayEra -> GovAction ConwayEra)
-> ProposalProcedure ConwayEra -> GovAction ConwayEra
forall a b. (a -> b) -> a -> b
$ GovActionState ConwayEra -> ProposalProcedure ConwayEra
forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure GovActionState ConwayEra
gas]
          ]
    committeeIds :: [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
committeeIds =
      (GovRelation StrictMaybe ConwayEra
prevGovActionIds GovRelation StrictMaybe ConwayEra
-> Getting
     (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
     (GovRelation StrictMaybe ConwayEra)
     (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
-> StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
  (GovRelation StrictMaybe ConwayEra)
  (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
forall (f1 :: * -> *) era (f2 :: * -> *).
Functor f2 =>
(f1 (GovPurposeId 'CommitteePurpose era)
 -> f2 (f1 (GovPurposeId 'CommitteePurpose era)))
-> GovRelation f1 era -> f2 (GovRelation f1 era)
grCommitteeL)
        StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)
-> [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
-> [StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)]
forall a. a -> [a] -> [a]
: [ GovPurposeId 'CommitteePurpose ConwayEra
-> StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)
forall a. a -> StrictMaybe a
SJust (GovPurposeId 'CommitteePurpose ConwayEra
 -> StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
-> GovPurposeId 'CommitteePurpose ConwayEra
-> StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra)
forall a b. (a -> b) -> a -> b
$ GovActionId -> GovPurposeId 'CommitteePurpose ConwayEra
forall a b. Coercible a b => a -> b
coerce (GovActionId -> GovPurposeId 'CommitteePurpose ConwayEra)
-> GovActionId -> GovPurposeId 'CommitteePurpose ConwayEra
forall a b. (a -> b) -> a -> b
$ GovActionState ConwayEra -> GovActionId
forall era. GovActionState era -> GovActionId
gasId GovActionState ConwayEra
gas
          | GovActionState ConwayEra
gas <- [GovActionState ConwayEra]
actions
          , GovAction ConwayEra -> Bool
forall {era}. GovAction era -> Bool
isCommitteeAction (ProposalProcedure ConwayEra -> GovAction ConwayEra
forall era. ProposalProcedure era -> GovAction era
pProcGovAction (ProposalProcedure ConwayEra -> GovAction ConwayEra)
-> ProposalProcedure ConwayEra -> GovAction ConwayEra
forall a b. (a -> b) -> a -> b
$ GovActionState ConwayEra -> ProposalProcedure ConwayEra
forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure GovActionState ConwayEra
gas)
          ]
    ppupIds :: [StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)]
ppupIds =
      (GovRelation StrictMaybe ConwayEra
prevGovActionIds GovRelation StrictMaybe ConwayEra
-> Getting
     (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
     (GovRelation StrictMaybe ConwayEra)
     (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
  (GovRelation StrictMaybe ConwayEra)
  (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
forall (f1 :: * -> *) era (f2 :: * -> *).
Functor f2 =>
(f1 (GovPurposeId 'PParamUpdatePurpose era)
 -> f2 (f1 (GovPurposeId 'PParamUpdatePurpose era)))
-> GovRelation f1 era -> f2 (GovRelation f1 era)
grPParamUpdateL)
        StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)
-> [StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)]
-> [StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)]
forall a. a -> [a] -> [a]
: [ GovPurposeId 'PParamUpdatePurpose ConwayEra
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)
forall a. a -> StrictMaybe a
SJust (GovPurposeId 'PParamUpdatePurpose ConwayEra
 -> StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
-> GovPurposeId 'PParamUpdatePurpose ConwayEra
-> StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra)
forall a b. (a -> b) -> a -> b
$ GovActionId -> GovPurposeId 'PParamUpdatePurpose ConwayEra
forall a b. Coercible a b => a -> b
coerce (GovActionId -> GovPurposeId 'PParamUpdatePurpose ConwayEra)
-> GovActionId -> GovPurposeId 'PParamUpdatePurpose ConwayEra
forall a b. (a -> b) -> a -> b
$ GovActionState ConwayEra -> GovActionId
forall era. GovActionState era -> GovActionId
gasId GovActionState ConwayEra
gas
          | GovActionState ConwayEra
gas <- [GovActionState ConwayEra]
actions
          , ParameterChange {} <- [ProposalProcedure ConwayEra -> GovAction ConwayEra
forall era. ProposalProcedure era -> GovAction era
pProcGovAction (ProposalProcedure ConwayEra -> GovAction ConwayEra)
-> ProposalProcedure ConwayEra -> GovAction ConwayEra
forall a b. (a -> b) -> a -> b
$ GovActionState ConwayEra -> ProposalProcedure ConwayEra
forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure GovActionState ConwayEra
gas]
          ]
    hardForkIds :: [StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)]
hardForkIds =
      (GovRelation StrictMaybe ConwayEra
prevGovActionIds GovRelation StrictMaybe ConwayEra
-> Getting
     (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
     (GovRelation StrictMaybe ConwayEra)
     (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
-> StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
  (GovRelation StrictMaybe ConwayEra)
  (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
forall (f1 :: * -> *) era (f2 :: * -> *).
Functor f2 =>
(f1 (GovPurposeId 'HardForkPurpose era)
 -> f2 (f1 (GovPurposeId 'HardForkPurpose era)))
-> GovRelation f1 era -> f2 (GovRelation f1 era)
grHardForkL)
        StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)
-> [StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)]
-> [StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)]
forall a. a -> [a] -> [a]
: [ GovPurposeId 'HardForkPurpose ConwayEra
-> StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)
forall a. a -> StrictMaybe a
SJust (GovPurposeId 'HardForkPurpose ConwayEra
 -> StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
-> GovPurposeId 'HardForkPurpose ConwayEra
-> StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra)
forall a b. (a -> b) -> a -> b
$ GovActionId -> GovPurposeId 'HardForkPurpose ConwayEra
forall a b. Coercible a b => a -> b
coerce (GovActionId -> GovPurposeId 'HardForkPurpose ConwayEra)
-> GovActionId -> GovPurposeId 'HardForkPurpose ConwayEra
forall a b. (a -> b) -> a -> b
$ GovActionState ConwayEra -> GovActionId
forall era. GovActionState era -> GovActionId
gasId GovActionState ConwayEra
gas
          | GovActionState ConwayEra
gas <- [GovActionState ConwayEra]
actions
          , HardForkInitiation {} <- [ProposalProcedure ConwayEra -> GovAction ConwayEra
forall era. ProposalProcedure era -> GovAction era
pProcGovAction (ProposalProcedure ConwayEra -> GovAction ConwayEra)
-> ProposalProcedure ConwayEra -> GovAction ConwayEra
forall a b. (a -> b) -> a -> b
$ GovActionState ConwayEra -> ProposalProcedure ConwayEra
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 PParams ConwayEra
-> Getting ProtVer (PParams ConwayEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams ConwayEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL
    findProtVer (SJust GovActionId
hid) =
      case GovActionId
-> Proposals ConwayEra -> Maybe (GovActionState ConwayEra)
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 <- ProposalProcedure ConwayEra -> GovAction ConwayEra
forall era. ProposalProcedure era -> GovAction era
pProcGovAction (ProposalProcedure ConwayEra -> GovAction ConwayEra)
-> ProposalProcedure ConwayEra -> GovAction ConwayEra
forall a b. (a -> b) -> a -> b
$ GovActionState ConwayEra -> ProposalProcedure ConwayEra
forall era. GovActionState era -> ProposalProcedure era
gasProposalProcedure GovActionState ConwayEra
gas -> ProtVer
protVer
        Maybe (GovActionState ConwayEra)
_ -> PParams ConwayEra
gePParams PParams ConwayEra
-> Getting ProtVer (PParams ConwayEra) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams ConwayEra) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams ConwayEra) ProtVer
ppProtocolVersionL

    hfIdMajorVer :: p -> (Version, Maybe Version)
hfIdMajorVer p
mId =
      let ProtVer Version
currentMajorVersion Natural
_ = StrictMaybe GovActionId -> ProtVer
findProtVer (p -> StrictMaybe GovActionId
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 (p -> StrictMaybe GovActionId
forall a b. Coercible a b => a -> b
coerce p
mId)
       in Natural
currentMinorVersion

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

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