{-# 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
import Constrained.Base (Pred (..))
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 ::
  IsConwayUniv fn =>
  Specification fn (GovEnv ConwayEra)
govEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (GovEnv ConwayEra)
govEnvSpec = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \Term fn (GovEnv ConwayEra)
ge ->
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (GovEnv ConwayEra)
ge forall a b. (a -> b) -> a -> b
$ \Term fn TxId
_ Term fn EpochNo
_ Term fn (PParams ConwayEra)
pp Term fn (StrictMaybe ScriptHash)
_ Term fn (ConwayCertState ConwayEra)
_ ->
    forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PParams ConwayEra)
pp forall (fn :: [*] -> * -> *) era.
(EraSpecPParams era, BaseUniverse fn) =>
Specification fn (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 ::
  IsConwayUniv fn =>
  GovEnv ConwayEra ->
  Specification fn (Proposals ConwayEra)
govProposalsSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
GovEnv ConwayEra -> Specification fn (Proposals ConwayEra)
govProposalsSpec GovEnv {EpochNo
geEpoch :: forall era. GovEnv era -> EpochNo
geEpoch :: EpochNo
geEpoch, StrictMaybe ScriptHash
gePPolicy :: forall era. GovEnv era -> StrictMaybe ScriptHash
gePPolicy :: StrictMaybe ScriptHash
gePPolicy, CertState ConwayEra
geCertState :: forall era. GovEnv era -> CertState era
geCertState :: CertState ConwayEra
geCertState} =
  forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn EpochNo
-> Term fn (StrictMaybe ScriptHash)
-> Term fn (CertState ConwayEra)
-> Specification fn (Proposals ConwayEra)
proposalsSpec (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit EpochNo
geEpoch) (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit StrictMaybe ScriptHash
gePPolicy) (forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit CertState ConwayEra
geCertState)

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

allGASInTree ::
  (IsConwayUniv fn, IsPred p fn) =>
  (Term fn (GovActionState ConwayEra) -> p) ->
  Specification fn (ProposalTree ConwayEra)
allGASInTree :: forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
(Term fn (GAS ConwayEra) -> p)
-> Specification fn (ProposalTree ConwayEra)
allGASInTree Term fn (GAS ConwayEra) -> p
k = forall a (fn :: [*] -> * -> *) p.
(IsPred p fn, HasSpec fn a) =>
(Term fn a -> p) -> Specification fn a
constrained forall a b. (a -> b) -> a -> b
$ \ Term fn (ProposalTree ConwayEra)
[var|proposalTree|] ->
  forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn b
snd_ Term fn (ProposalTree ConwayEra)
proposalTree) forall a b. (a -> b) -> a -> b
$ \ Term fn (Tree (GAS ConwayEra))
[var|subtree|] ->
    forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term fn (Tree (GAS ConwayEra))
subtree forall a b. (a -> b) -> a -> b
$ \ Term fn (GAS ConwayEra)
[var|gas|] Term fn [Tree (GAS ConwayEra)]
_ ->
      Term fn (GAS ConwayEra) -> p
k Term fn (GAS ConwayEra)
gas

allGASAndChildInTree ::
  (IsConwayUniv fn, IsPred p fn) =>
  Term fn (ProposalTree ConwayEra) ->
  ( Term fn (GovActionState ConwayEra) ->
    Term fn (GovActionState ConwayEra) ->
    p
  ) ->
  Pred fn
allGASAndChildInTree :: forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
Term fn (ProposalTree ConwayEra)
-> (Term fn (GAS ConwayEra) -> Term fn (GAS ConwayEra) -> p)
-> Pred fn
allGASAndChildInTree Term fn (ProposalTree ConwayEra)
t Term fn (GAS ConwayEra) -> Term fn (GAS ConwayEra) -> p
k =
  forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll (forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn (a, b) -> Term fn b
snd_ Term fn (ProposalTree ConwayEra)
t) forall a b. (a -> b) -> a -> b
$ \ Term fn (Tree (GAS ConwayEra))
[var|subtree|] ->
    forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term fn (Tree (GAS ConwayEra))
subtree forall a b. (a -> b) -> a -> b
$ \ Term fn (GAS ConwayEra)
[var|gas|] Term fn [Tree (GAS ConwayEra)]
[var|cs|] ->
      forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn [Tree (GAS ConwayEra)]
cs forall a b. (a -> b) -> a -> b
$ \ Term fn (Tree (GAS ConwayEra))
[var|t''|] ->
        Term fn (GAS ConwayEra) -> Term fn (GAS ConwayEra) -> p
k Term fn (GAS ConwayEra)
gas (forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ Term fn (Tree (GAS ConwayEra))
t'')

wellFormedChildren ::
  IsConwayUniv fn =>
  Term fn (ProposalTree ConwayEra) ->
  Pred fn
wellFormedChildren :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (ProposalTree ConwayEra) -> Pred fn
wellFormedChildren Term fn (ProposalTree ConwayEra)
rootAndTrees =
  forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn (ProposalTree ConwayEra)
rootAndTrees forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe GovActionId)
root Term fn [Tree (GAS ConwayEra)]
trees ->
    [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ProposalTree ConwayEra)
rootAndTrees Term fn (StrictMaybe GovActionId)
root
    , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ProposalTree ConwayEra)
rootAndTrees Term fn [Tree (GAS ConwayEra)]
trees
    , forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn [Tree (GAS ConwayEra)]
trees forall a b. (a -> b) -> a -> b
$ \Term fn (Tree (GAS ConwayEra))
t ->
        [ -- Every node just below the root has the root as its parent
          forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (GAS ConwayEra)
-> (Term fn (StrictMaybe GovActionId) -> Pred fn) -> Pred fn
withPrevActId (forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ Term fn (Tree (GAS ConwayEra))
t) (forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (StrictMaybe GovActionId)
root))
        , -- Every node's children have the id of the node as its parent
          forall (fn :: [*] -> * -> *) t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a), HasSpec fn t,
 HasSpec fn (SimpleRep a), HasSimpleRep a,
 All (HasSpec fn) (Args (SimpleRep a)), IsPred p fn,
 IsProd (SimpleRep a), HasSpec fn a) =>
Term fn t
-> FunTy (MapList (Term fn) (Args (SimpleRep a))) p -> Pred fn
forAll' Term fn (Tree (GAS ConwayEra))
t forall a b. (a -> b) -> a -> b
$ \Term fn (GAS ConwayEra)
gas Term fn [Tree (GAS ConwayEra)]
children ->
            [ forall t a (fn :: [*] -> * -> *) p.
(Forallable t a, HasSpec fn t, HasSpec fn a, IsPred p fn) =>
Term fn t -> (Term fn a -> p) -> Pred fn
forAll Term fn [Tree (GAS ConwayEra)]
children forall a b. (a -> b) -> a -> b
$ \Term fn (Tree (GAS ConwayEra))
t' ->
                [ forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (GAS ConwayEra)
-> (Term fn (StrictMaybe GovActionId) -> Pred fn) -> Pred fn
withPrevActId (forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ Term fn (Tree (GAS ConwayEra))
t') (forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn a -> Term fn (StrictMaybe a)
cSJust_ (forall (fn :: [*] -> * -> *).
(EraSpecPParams ConwayEra, IsConwayUniv fn) =>
Term fn (GAS ConwayEra) -> Term fn GovActionId
gasId_ Term fn (GAS ConwayEra)
gas)))
                -- TODO: figure out why this causes a crash!
                -- , t' `dependsOn` gas
                ]
            , Term fn [Tree (GAS ConwayEra)]
children forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term fn (GAS ConwayEra)
gas
            ]
        ]
    ]

withPrevActId ::
  IsConwayUniv fn =>
  Term fn (GovActionState ConwayEra) ->
  (Term fn (StrictMaybe GovActionId) -> Pred fn) ->
  Pred fn
withPrevActId :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (GAS ConwayEra)
-> (Term fn (StrictMaybe GovActionId) -> Pred fn) -> Pred fn
withPrevActId Term fn (GAS ConwayEra)
gas Term fn (StrictMaybe GovActionId) -> Pred fn
k =
  forall (fn :: [*] -> * -> *). [Pred fn] -> Pred fn
Block
    [ forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match (forall (fn :: [*] -> * -> *).
(EraSpecPParams ConwayEra, IsConwayUniv fn) =>
Term fn (GAS ConwayEra) -> Term fn (ProposalProcedure ConwayEra)
gasProposalProcedure_ Term fn (GAS ConwayEra)
gas) forall a b. (a -> b) -> a -> b
$ \Term fn Coin
_deposit Term fn RewardAccount
[var|retAddr|] Term fn (GovAction ConwayEra)
_action Term fn Anchor
_anchor ->
        forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, IsProductType fn a, IsPred p fn) =>
Term fn a
-> FunTy (MapList (Term fn) (ProductAsList a)) p -> Pred fn
match Term fn RewardAccount
retAddr forall a b. (a -> b) -> a -> b
$ \ Term fn Network
[var|net|] Term fn (Credential 'Staking)
_ -> [forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (GAS ConwayEra)
gas Term fn Network
net, forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn Network
net forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Network
Testnet]
    , forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
        (forall (fn :: [*] -> * -> *).
(EraSpecPParams ConwayEra, IsConwayUniv fn) =>
Term fn (ProposalProcedure ConwayEra)
-> Term fn (GovAction ConwayEra)
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *).
(EraSpecPParams ConwayEra, IsConwayUniv fn) =>
Term fn (GAS ConwayEra) -> Term fn (ProposalProcedure ConwayEra)
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term fn (GAS ConwayEra)
gas)
        -- ParameterChange
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
mPrevActionId Term fn (PParamsUpdate ConwayEra)
_ Term fn (StrictMaybe ScriptHash)
_ ->
            forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
              Term fn (StrictMaybe (GovPurposeId 'PParamUpdatePurpose ConwayEra))
mPrevActionId
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Term fn (StrictMaybe GovActionId) -> Pred fn
k forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn (StrictMaybe a)
cSNothing_)
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (GovPurposeId 'PParamUpdatePurpose ConwayEra)
i -> Term fn (StrictMaybe GovActionId) -> Pred fn
k (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn a -> Term fn (StrictMaybe a)
cSJust_ forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn a -> Term fn (SimpleRep a)
toGeneric_ Term fn (GovPurposeId 'PParamUpdatePurpose ConwayEra)
i))
        )
        -- HardForkInitiation
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
mPrevActionId Term fn ProtVer
_ ->
            forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
              Term fn (StrictMaybe (GovPurposeId 'HardForkPurpose ConwayEra))
mPrevActionId
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Term fn (StrictMaybe GovActionId) -> Pred fn
k forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn (StrictMaybe a)
cSNothing_)
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (GovPurposeId 'HardForkPurpose ConwayEra)
i -> Term fn (StrictMaybe GovActionId) -> Pred fn
k (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn a -> Term fn (StrictMaybe a)
cSJust_ forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn a -> Term fn (SimpleRep a)
toGeneric_ Term fn (GovPurposeId 'HardForkPurpose ConwayEra)
i))
        )
        -- TreasuryWithdrawals
        (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (Map RewardAccount Coin)
_ Term fn (StrictMaybe ScriptHash)
_ -> Bool
True)
        -- NoConfidence
        --   !(StrictMaybe (PrevGovActionId 'CommitteePurpose (EraCrypto era)))
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId ->
            forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
              Term fn (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Term fn (StrictMaybe GovActionId) -> Pred fn
k forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn (StrictMaybe a)
cSNothing_)
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (GovPurposeId 'CommitteePurpose ConwayEra)
i -> Term fn (StrictMaybe GovActionId) -> Pred fn
k (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn a -> Term fn (StrictMaybe a)
cSJust_ forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn a -> Term fn (SimpleRep a)
toGeneric_ Term fn (GovPurposeId 'CommitteePurpose ConwayEra)
i))
        )
        -- UpdateCommittee
        --   !(StrictMaybe (PrevGovActionId 'CommitteePurpose (EraCrypto era)))
        --   !(Set (Credential 'ColdCommitteeRole (EraCrypto era)))
        --   !(Map (Credential 'ColdCommitteeRole (EraCrypto era)) EpochNo)
        --   !UnitInterval
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId Term fn (Set (Credential 'ColdCommitteeRole))
_ Term fn (Map (Credential 'ColdCommitteeRole) EpochNo)
_ Term fn UnitInterval
_ ->
            forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
              Term fn (StrictMaybe (GovPurposeId 'CommitteePurpose ConwayEra))
mPrevActionId
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Term fn (StrictMaybe GovActionId) -> Pred fn
k forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn (StrictMaybe a)
cSNothing_)
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (GovPurposeId 'CommitteePurpose ConwayEra)
i -> Term fn (StrictMaybe GovActionId) -> Pred fn
k (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn a -> Term fn (StrictMaybe a)
cSJust_ forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn a -> Term fn (SimpleRep a)
toGeneric_ Term fn (GovPurposeId 'CommitteePurpose ConwayEra)
i))
        )
        -- NewConstitution
        --  !(StrictMaybe (PrevGovActionId 'ConstitutionPurpose (EraCrypto era)))
        --  !(Constitution era)
        ( forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
mPrevActionId Term fn (Constitution ConwayEra)
_ ->
            forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a),
 SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term fn a
-> FunTy
     (MapList (Weighted (Binder fn)) (Cases (SimpleRep a))) (Pred fn)
caseOn
              Term fn (StrictMaybe (GovPurposeId 'ConstitutionPurpose ConwayEra))
mPrevActionId
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Term fn (StrictMaybe GovActionId) -> Pred fn
k forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn (StrictMaybe a)
cSNothing_)
              (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn (GovPurposeId 'ConstitutionPurpose ConwayEra)
i -> Term fn (StrictMaybe GovActionId) -> Pred fn
k (forall (fn :: [*] -> * -> *) a.
(HasSpec fn a, IsNormalType a) =>
Term fn a -> Term fn (StrictMaybe a)
cSJust_ forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *).
(HasSpec fn a, HasSpec fn (SimpleRep a), HasSimpleRep a,
 TypeSpec fn a ~ TypeSpec fn (SimpleRep a)) =>
Term fn a -> Term fn (SimpleRep a)
toGeneric_ Term fn (GovPurposeId 'ConstitutionPurpose ConwayEra)
i))
        )
        -- InfoAction
        (forall (fn :: [*] -> * -> *) p a.
(HasSpec fn a, All (HasSpec fn) (Args a), IsPred p fn, IsProd a) =>
FunTy (MapList (Term fn) (Args a)) p -> Weighted (Binder fn) a
branch forall a b. (a -> b) -> a -> b
$ \Term fn ()
_ -> Bool
True)
    ]

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

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

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

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

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

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

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

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