{-# 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.CertState
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Conway (Conway, ConwayEra)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance
import Cardano.Ledger.Conway.Rules
import Cardano.Ledger.Crypto (StandardCrypto)
import Cardano.Ledger.Shelley.HardForks qualified as HardForks
import Cardano.Ledger.UMap (umElems)
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 StandardCrypto))
govEnvSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (GovEnv (ConwayEra StandardCrypto))
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 StandardCrypto))
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 StandardCrypto))
ge forall a b. (a -> b) -> a -> b
$ \Term fn (TxId StandardCrypto)
_ Term fn EpochNo
_ Term fn (PParams (ConwayEra StandardCrypto))
pp Term fn (StrictMaybe (ScriptHash StandardCrypto))
_ Term fn (CertState (ConwayEra StandardCrypto))
_ ->
    forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies Term fn (PParams (ConwayEra StandardCrypto))
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 StandardCrypto) ->
  Specification fn (Proposals (ConwayEra StandardCrypto))
govProposalsSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
GovEnv (ConwayEra StandardCrypto)
-> Specification fn (Proposals (ConwayEra StandardCrypto))
govProposalsSpec GovEnv {EpochNo
geEpoch :: forall era. GovEnv era -> EpochNo
geEpoch :: EpochNo
geEpoch, StrictMaybe (ScriptHash (EraCrypto (ConwayEra StandardCrypto)))
gePPolicy :: forall era. GovEnv era -> StrictMaybe (ScriptHash (EraCrypto era))
gePPolicy :: StrictMaybe (ScriptHash (EraCrypto (ConwayEra StandardCrypto)))
gePPolicy, CertState (ConwayEra StandardCrypto)
geCertState :: forall era. GovEnv era -> CertState era
geCertState :: CertState (ConwayEra StandardCrypto)
geCertState} =
  forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn EpochNo
-> Term fn (StrictMaybe (ScriptHash StandardCrypto))
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (Proposals (ConwayEra StandardCrypto))
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 (EraCrypto (ConwayEra StandardCrypto)))
gePPolicy) CertState (ConwayEra StandardCrypto)
geCertState

proposalsSpec ::
  IsConwayUniv fn =>
  Term fn EpochNo ->
  Term fn (StrictMaybe (ScriptHash StandardCrypto)) ->
  CertState Conway ->
  Specification fn (Proposals Conway)
proposalsSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn EpochNo
-> Term fn (StrictMaybe (ScriptHash StandardCrypto))
-> CertState (ConwayEra StandardCrypto)
-> Specification fn (Proposals (ConwayEra StandardCrypto))
proposalsSpec Term fn EpochNo
geEpoch Term fn (StrictMaybe (ScriptHash StandardCrypto))
gePPolicy CertState (ConwayEra StandardCrypto)
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 StandardCrypto))
[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 StandardCrypto))
props forall a b. (a -> b) -> a -> b
$ \ Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
[var|ppupTree|] Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
[var|hardForkTree|] Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
[var|committeeTree|] Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
[var|constitutionTree|] Term fn [GAS (ConwayEra StandardCrypto)]
[var|unorderedProposals|] ->
      [ -- Protocol parameter updates
        forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (ProposalTree (ConwayEra StandardCrypto)) -> Pred fn
wellFormedChildren Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
ppupTree
      , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies
          Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
ppupTree
          ( forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
(Term fn (GAS (ConwayEra StandardCrypto)) -> p)
-> Specification fn (ProposalTree (ConwayEra StandardCrypto))
allGASInTree
              ( \ Term fn (GAS (ConwayEra StandardCrypto))
[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 StandardCrypto), IsConwayUniv fn) =>
Term fn (ProposalProcedure (ConwayEra StandardCrypto))
-> Term fn (GovAction (ConwayEra StandardCrypto))
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *).
(EraSpecPParams (ConwayEra StandardCrypto), IsConwayUniv fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (ProposalProcedure (ConwayEra StandardCrypto))
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term fn (GAS (ConwayEra StandardCrypto))
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 StandardCrypto), IsConwayUniv fn) =>
Term fn (ProposalProcedure (ConwayEra StandardCrypto))
-> Term fn (GovAction (ConwayEra StandardCrypto))
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *).
(EraSpecPParams (ConwayEra StandardCrypto), IsConwayUniv fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (ProposalProcedure (ConwayEra StandardCrypto))
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term fn (GAS (ConwayEra StandardCrypto))
gasPpup) forall a b. (a -> b) -> a -> b
$
                      \Term
  fn
  (StrictMaybe
     (GovPurposeId 'PParamUpdatePurpose (ConwayEra StandardCrypto)))
_ Term fn (PParamsUpdate (ConwayEra StandardCrypto))
ppup Term fn (StrictMaybe (ScriptHash StandardCrypto))
policy ->
                        [ forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (PParamsUpdate (ConwayEra StandardCrypto))
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 StandardCrypto))
ppup forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (PParamsUpdate (ConwayEra StandardCrypto))
wfPParamsUpdateSpec
                        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (StrictMaybe (ScriptHash StandardCrypto))
policy forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (StrictMaybe (ScriptHash StandardCrypto))
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
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
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
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
ppupTree)
      , -- Hard forks
        forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (ProposalTree (ConwayEra StandardCrypto)) -> Pred fn
wellFormedChildren Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
hardForkTree
      , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies
          Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
hardForkTree
          ( forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
(Term fn (GAS (ConwayEra StandardCrypto)) -> p)
-> Specification fn (ProposalTree (ConwayEra StandardCrypto))
allGASInTree
              ( \ Term fn (GAS (ConwayEra StandardCrypto))
[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 StandardCrypto), IsConwayUniv fn) =>
Term fn (ProposalProcedure (ConwayEra StandardCrypto))
-> Term fn (GovAction (ConwayEra StandardCrypto))
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *).
(EraSpecPParams (ConwayEra StandardCrypto), IsConwayUniv fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (ProposalProcedure (ConwayEra StandardCrypto))
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term fn (GAS (ConwayEra StandardCrypto))
gasHfork)
              )
          )
      , forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
Term fn (ProposalTree (ConwayEra StandardCrypto))
-> (Term fn (GAS (ConwayEra StandardCrypto))
    -> Term fn (GAS (ConwayEra StandardCrypto)) -> p)
-> Pred fn
allGASAndChildInTree Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
hardForkTree forall a b. (a -> b) -> a -> b
$ \Term fn (GAS (ConwayEra StandardCrypto))
gas Term fn (GAS (ConwayEra StandardCrypto))
gas' ->
          [ forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> (Term
      fn
      (StrictMaybe
         (GovPurposeId 'HardForkPurpose (ConwayEra StandardCrypto)))
    -> Term fn ProtVer -> p)
-> Pred fn
onHardFork Term fn (GAS (ConwayEra StandardCrypto))
gas forall a b. (a -> b) -> a -> b
$ \Term
  fn
  (StrictMaybe
     (GovPurposeId 'HardForkPurpose (ConwayEra StandardCrypto)))
_ Term fn ProtVer
pv ->
              forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> (Term
      fn
      (StrictMaybe
         (GovPurposeId 'HardForkPurpose (ConwayEra StandardCrypto)))
    -> Term fn ProtVer -> p)
-> Pred fn
onHardFork Term fn (GAS (ConwayEra StandardCrypto))
gas' forall a b. (a -> b) -> a -> b
$ \Term
  fn
  (StrictMaybe
     (GovPurposeId 'HardForkPurpose (ConwayEra StandardCrypto)))
_ 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
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
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
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
hardForkTree)
      , -- Committee
        forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (ProposalTree (ConwayEra StandardCrypto)) -> Pred fn
wellFormedChildren Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
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
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
committeeTree
          ( forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
(Term fn (GAS (ConwayEra StandardCrypto)) -> p)
-> Specification fn (ProposalTree (ConwayEra StandardCrypto))
allGASInTree
              ( \ Term fn (GAS (ConwayEra StandardCrypto))
[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 StandardCrypto), IsConwayUniv fn) =>
Term fn (ProposalProcedure (ConwayEra StandardCrypto))
-> Term fn (GovAction (ConwayEra StandardCrypto))
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *).
(EraSpecPParams (ConwayEra StandardCrypto), IsConwayUniv fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (ProposalProcedure (ConwayEra StandardCrypto))
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term fn (GAS (ConwayEra StandardCrypto))
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 StandardCrypto)))
_ Term fn (PParamsUpdate (ConwayEra StandardCrypto))
_ Term fn (StrictMaybe (ScriptHash StandardCrypto))
_ -> 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 StandardCrypto)))
_ 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 StandardCrypto) Coin)
_ Term fn (StrictMaybe (ScriptHash StandardCrypto))
_ -> 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 StandardCrypto)))
_ -> 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 StandardCrypto)))
_ Term fn (Set (Credential 'ColdCommitteeRole StandardCrypto))
_ Term
  fn (Map (Credential 'ColdCommitteeRole StandardCrypto) 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 StandardCrypto) 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 StandardCrypto)))
_ Term fn (Constitution (ConwayEra StandardCrypto))
_ -> 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
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
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
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
committeeTree)
      , -- Constitution
        forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (ProposalTree (ConwayEra StandardCrypto)) -> Pred fn
wellFormedChildren Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
constitutionTree
      , forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Specification fn a -> Pred fn
satisfies
          Term
  fn
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
constitutionTree
          ( forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
(Term fn (GAS (ConwayEra StandardCrypto)) -> p)
-> Specification fn (ProposalTree (ConwayEra StandardCrypto))
allGASInTree -- Extract the GovAction from the GovActionID and match against the constructor NewConstitution
              ( \ Term fn (GAS (ConwayEra StandardCrypto))
[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 StandardCrypto), IsConwayUniv fn) =>
Term fn (ProposalProcedure (ConwayEra StandardCrypto))
-> Term fn (GovAction (ConwayEra StandardCrypto))
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *).
(EraSpecPParams (ConwayEra StandardCrypto), IsConwayUniv fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (ProposalProcedure (ConwayEra StandardCrypto))
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term fn (GAS (ConwayEra StandardCrypto))
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
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
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
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
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 StandardCrypto)]
unorderedProposals forall a b. (a -> b) -> a -> b
$ \ Term fn (GAS (ConwayEra StandardCrypto))
[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 StandardCrypto), IsConwayUniv fn) =>
Term fn (ProposalProcedure (ConwayEra StandardCrypto))
-> Term fn (GovAction (ConwayEra StandardCrypto))
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *).
(EraSpecPParams (ConwayEra StandardCrypto), IsConwayUniv fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (ProposalProcedure (ConwayEra StandardCrypto))
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term fn (GAS (ConwayEra StandardCrypto))
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 StandardCrypto)))
_ Term fn (PParamsUpdate (ConwayEra StandardCrypto))
_ Term fn (StrictMaybe (ScriptHash StandardCrypto))
_ -> 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 StandardCrypto)))
_ 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 StandardCrypto) Coin)
[var|withdrawMap|] Term fn (StrictMaybe (ScriptHash StandardCrypto))
[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 StandardCrypto))
gasOther Term fn (Map (RewardAccount StandardCrypto) Coin)
withdrawMap
                    , 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 StandardCrypto) Coin)
withdrawMap) forall a b. (a -> b) -> a -> b
$ \ Term fn (RewardAccount StandardCrypto)
[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 StandardCrypto)
rewAcnt forall a b. (a -> b) -> a -> b
$ \ Term fn Network
[var|network|] Term fn (Credential 'Staking StandardCrypto)
[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 StandardCrypto)
credential 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 StandardCrypto)
registeredCredentials
                          ]
                    , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (StrictMaybe (ScriptHash StandardCrypto))
policy forall (fn :: [*] -> * -> *) a.
HasSpec fn a =>
Term fn a -> Term fn a -> Term fn Bool
==. Term fn (StrictMaybe (ScriptHash StandardCrypto))
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 StandardCrypto)))
_ -> 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 StandardCrypto)))
_ Term fn (Set (Credential 'ColdCommitteeRole StandardCrypto))
_ Term
  fn (Map (Credential 'ColdCommitteeRole StandardCrypto) 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 StandardCrypto)))
_ Term fn (Constitution (ConwayEra StandardCrypto))
_ -> 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 StandardCrypto)]
unorderedProposals
      ]
  where
    treeGenHint :: (Maybe Integer, Integer)
treeGenHint = (forall a. a -> Maybe a
Just Integer
2, Integer
10)
    listSizeHint :: Integer
listSizeHint = Integer
5
    registeredCredentials :: Set (Credential 'Staking StandardCrypto)
registeredCredentials = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ forall c. UMap c -> Map (Credential 'Staking c) (UMElem c)
umElems forall a b. (a -> b) -> a -> b
$ forall era. DState era -> UMap (EraCrypto era)
dsUnified forall a b. (a -> b) -> a -> b
$ forall era. CertState era -> DState era
certDState CertState (ConwayEra StandardCrypto)
geCertState

allGASInTree ::
  (IsConwayUniv fn, IsPred p fn) =>
  (Term fn (GovActionState (ConwayEra StandardCrypto)) -> p) ->
  Specification fn (ProposalTree (ConwayEra StandardCrypto))
allGASInTree :: forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
(Term fn (GAS (ConwayEra StandardCrypto)) -> p)
-> Specification fn (ProposalTree (ConwayEra StandardCrypto))
allGASInTree Term fn (GAS (ConwayEra StandardCrypto)) -> 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 StandardCrypto))
[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
  (StrictMaybe (GovActionId StandardCrypto),
   [Tree (GAS (ConwayEra StandardCrypto))])
proposalTree) forall a b. (a -> b) -> a -> b
$ \ Term fn (Tree (GAS (ConwayEra StandardCrypto)))
[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 StandardCrypto)))
subtree forall a b. (a -> b) -> a -> b
$ \ Term fn (GAS (ConwayEra StandardCrypto))
[var|gas|] Term fn [Tree (GAS (ConwayEra StandardCrypto))]
_ ->
      Term fn (GAS (ConwayEra StandardCrypto)) -> p
k Term fn (GAS (ConwayEra StandardCrypto))
gas

allGASAndChildInTree ::
  (IsConwayUniv fn, IsPred p fn) =>
  Term fn (ProposalTree (ConwayEra StandardCrypto)) ->
  ( Term fn (GovActionState (ConwayEra StandardCrypto)) ->
    Term fn (GovActionState (ConwayEra StandardCrypto)) ->
    p
  ) ->
  Pred fn
allGASAndChildInTree :: forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
Term fn (ProposalTree (ConwayEra StandardCrypto))
-> (Term fn (GAS (ConwayEra StandardCrypto))
    -> Term fn (GAS (ConwayEra StandardCrypto)) -> p)
-> Pred fn
allGASAndChildInTree Term fn (ProposalTree (ConwayEra StandardCrypto))
t Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (GAS (ConwayEra StandardCrypto)) -> 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 StandardCrypto))
t) forall a b. (a -> b) -> a -> b
$ \ Term fn (Tree (GAS (ConwayEra StandardCrypto)))
[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 StandardCrypto)))
subtree forall a b. (a -> b) -> a -> b
$ \ Term fn (GAS (ConwayEra StandardCrypto))
[var|gas|] Term fn [Tree (GAS (ConwayEra StandardCrypto))]
[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 StandardCrypto))]
cs forall a b. (a -> b) -> a -> b
$ \ Term fn (Tree (GAS (ConwayEra StandardCrypto)))
[var|t''|] ->
        Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (GAS (ConwayEra StandardCrypto)) -> p
k Term fn (GAS (ConwayEra StandardCrypto))
gas (forall (fn :: [*] -> * -> *) a.
(Member (TreeFn fn) fn, HasSpec fn a) =>
Term fn (Tree a) -> Term fn a
rootLabel_ Term fn (Tree (GAS (ConwayEra StandardCrypto)))
t'')

wellFormedChildren ::
  IsConwayUniv fn =>
  Term fn (ProposalTree (ConwayEra StandardCrypto)) ->
  Pred fn
wellFormedChildren :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (ProposalTree (ConwayEra StandardCrypto)) -> Pred fn
wellFormedChildren Term fn (ProposalTree (ConwayEra StandardCrypto))
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 StandardCrypto))
rootAndTrees forall a b. (a -> b) -> a -> b
$ \Term fn (StrictMaybe (GovActionId StandardCrypto))
root Term fn [Tree (GAS (ConwayEra StandardCrypto))]
trees ->
    [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ProposalTree (ConwayEra StandardCrypto))
rootAndTrees Term fn (StrictMaybe (GovActionId StandardCrypto))
root
    , forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ProposalTree (ConwayEra StandardCrypto))
rootAndTrees Term fn [Tree (GAS (ConwayEra StandardCrypto))]
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 StandardCrypto))]
trees forall a b. (a -> b) -> a -> b
$ \Term fn (Tree (GAS (ConwayEra StandardCrypto)))
t ->
        [ -- Every node just below the root has the root as its parent
          forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (GAS (ConwayEra StandardCrypto))
-> (Term fn (StrictMaybe (GovActionId StandardCrypto)) -> 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 StandardCrypto)))
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 StandardCrypto))
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 StandardCrypto)))
t forall a b. (a -> b) -> a -> b
$ \Term fn (GAS (ConwayEra StandardCrypto))
gas Term fn [Tree (GAS (ConwayEra StandardCrypto))]
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 StandardCrypto))]
children forall a b. (a -> b) -> a -> b
$ \Term fn (Tree (GAS (ConwayEra StandardCrypto)))
t' ->
                [ forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (GAS (ConwayEra StandardCrypto))
-> (Term fn (StrictMaybe (GovActionId StandardCrypto)) -> 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 StandardCrypto)))
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 StandardCrypto), IsConwayUniv fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (GovActionId StandardCrypto)
gasId_ Term fn (GAS (ConwayEra StandardCrypto))
gas)))
                -- TODO: figure out why this causes a crash!
                -- , t' `dependsOn` gas
                ]
            , Term fn [Tree (GAS (ConwayEra StandardCrypto))]
children forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
`dependsOn` Term fn (GAS (ConwayEra StandardCrypto))
gas
            ]
        ]
    ]

withPrevActId ::
  IsConwayUniv fn =>
  Term fn (GovActionState (ConwayEra StandardCrypto)) ->
  (Term fn (StrictMaybe (GovActionId StandardCrypto)) -> Pred fn) ->
  Pred fn
withPrevActId :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Term fn (GAS (ConwayEra StandardCrypto))
-> (Term fn (StrictMaybe (GovActionId StandardCrypto)) -> Pred fn)
-> Pred fn
withPrevActId Term fn (GAS (ConwayEra StandardCrypto))
gas Term fn (StrictMaybe (GovActionId StandardCrypto)) -> 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 StandardCrypto), IsConwayUniv fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (ProposalProcedure (ConwayEra StandardCrypto))
gasProposalProcedure_ Term fn (GAS (ConwayEra StandardCrypto))
gas) forall a b. (a -> b) -> a -> b
$ \Term fn Coin
_deposit Term fn (RewardAccount StandardCrypto)
[var|retAddr|] Term fn (GovAction (ConwayEra StandardCrypto))
_action Term fn (Anchor StandardCrypto)
_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 StandardCrypto)
retAddr forall a b. (a -> b) -> a -> b
$ \ Term fn Network
[var|net|] Term fn (Credential 'Staking StandardCrypto)
_ -> [forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (GAS (ConwayEra StandardCrypto))
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 StandardCrypto), IsConwayUniv fn) =>
Term fn (ProposalProcedure (ConwayEra StandardCrypto))
-> Term fn (GovAction (ConwayEra StandardCrypto))
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *).
(EraSpecPParams (ConwayEra StandardCrypto), IsConwayUniv fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (ProposalProcedure (ConwayEra StandardCrypto))
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term fn (GAS (ConwayEra StandardCrypto))
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 StandardCrypto)))
mPrevActionId Term fn (PParamsUpdate (ConwayEra StandardCrypto))
_ Term fn (StrictMaybe (ScriptHash StandardCrypto))
_ ->
            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 StandardCrypto)))
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 StandardCrypto)) -> 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 StandardCrypto))
i -> Term fn (StrictMaybe (GovActionId StandardCrypto)) -> 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 StandardCrypto))
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 StandardCrypto)))
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 StandardCrypto)))
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 StandardCrypto)) -> 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 StandardCrypto))
i -> Term fn (StrictMaybe (GovActionId StandardCrypto)) -> 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 StandardCrypto))
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 StandardCrypto) Coin)
_ Term fn (StrictMaybe (ScriptHash StandardCrypto))
_ -> 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 StandardCrypto)))
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 StandardCrypto)))
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 StandardCrypto)) -> 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 StandardCrypto))
i -> Term fn (StrictMaybe (GovActionId StandardCrypto)) -> 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 StandardCrypto))
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 StandardCrypto)))
mPrevActionId Term fn (Set (Credential 'ColdCommitteeRole StandardCrypto))
_ Term
  fn (Map (Credential 'ColdCommitteeRole StandardCrypto) 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 StandardCrypto)))
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 StandardCrypto)) -> 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 StandardCrypto))
i -> Term fn (StrictMaybe (GovActionId StandardCrypto)) -> 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 StandardCrypto))
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 StandardCrypto)))
mPrevActionId Term fn (Constitution (ConwayEra StandardCrypto))
_ ->
            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 StandardCrypto)))
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 StandardCrypto)) -> 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 StandardCrypto))
i -> Term fn (StrictMaybe (GovActionId StandardCrypto)) -> 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 StandardCrypto))
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 StandardCrypto)) ->
  ( Term fn (StrictMaybe (GovPurposeId 'HardForkPurpose (ConwayEra StandardCrypto))) ->
    Term fn ProtVer ->
    p
  ) ->
  Pred fn
onHardFork :: forall (fn :: [*] -> * -> *) p.
(IsConwayUniv fn, IsPred p fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> (Term
      fn
      (StrictMaybe
         (GovPurposeId 'HardForkPurpose (ConwayEra StandardCrypto)))
    -> Term fn ProtVer -> p)
-> Pred fn
onHardFork Term fn (GAS (ConwayEra StandardCrypto))
gas Term
  fn
  (StrictMaybe
     (GovPurposeId 'HardForkPurpose (ConwayEra StandardCrypto)))
-> 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 StandardCrypto), IsConwayUniv fn) =>
Term fn (ProposalProcedure (ConwayEra StandardCrypto))
-> Term fn (GovAction (ConwayEra StandardCrypto))
pProcGovAction_ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (fn :: [*] -> * -> *).
(EraSpecPParams (ConwayEra StandardCrypto), IsConwayUniv fn) =>
Term fn (GAS (ConwayEra StandardCrypto))
-> Term fn (ProposalProcedure (ConwayEra StandardCrypto))
gasProposalProcedure_ forall a b. (a -> b) -> a -> b
$ Term fn (GAS (ConwayEra StandardCrypto))
gas) Term
  fn
  (StrictMaybe
     (GovPurposeId 'HardForkPurpose (ConwayEra StandardCrypto)))
-> Term fn ProtVer -> p
k

govProceduresSpec ::
  IsConwayUniv fn =>
  GovEnv (ConwayEra StandardCrypto) ->
  Proposals (ConwayEra StandardCrypto) ->
  Specification fn (GovSignal (ConwayEra StandardCrypto))
govProceduresSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
GovEnv (ConwayEra StandardCrypto)
-> Proposals (ConwayEra StandardCrypto)
-> Specification fn (GovSignal (ConwayEra StandardCrypto))
govProceduresSpec ge :: GovEnv (ConwayEra StandardCrypto)
ge@GovEnv {PParams (ConwayEra StandardCrypto)
StrictMaybe (ScriptHash (EraCrypto (ConwayEra StandardCrypto)))
TxId (EraCrypto (ConwayEra StandardCrypto))
CertState (ConwayEra StandardCrypto)
EpochNo
geTxId :: forall era. GovEnv era -> TxId (EraCrypto era)
gePParams :: forall era. GovEnv era -> PParams era
geCertState :: CertState (ConwayEra StandardCrypto)
gePPolicy :: StrictMaybe (ScriptHash (EraCrypto (ConwayEra StandardCrypto)))
gePParams :: PParams (ConwayEra StandardCrypto)
geEpoch :: EpochNo
geTxId :: TxId (EraCrypto (ConwayEra StandardCrypto))
geCertState :: forall era. GovEnv era -> CertState era
gePPolicy :: forall era. GovEnv era -> StrictMaybe (ScriptHash (EraCrypto era))
geEpoch :: forall era. GovEnv era -> EpochNo
..} Proposals (ConwayEra StandardCrypto)
ps =
  let actions :: (GovAction (ConwayEra StandardCrypto) -> Bool)
-> [GovActionId StandardCrypto]
actions GovAction (ConwayEra StandardCrypto) -> Bool
f =
        [ GovActionId StandardCrypto
gid
        | (GovActionId StandardCrypto
gid, GAS (ConwayEra StandardCrypto)
act) <- forall k a. Map k a -> [(k, a)]
Map.toList forall a b. (a -> b) -> a -> b
$ forall era.
Proposals era
-> Map (GovActionId (EraCrypto era)) (GovActionState era)
proposalsActionsMap Proposals (ConwayEra StandardCrypto)
ps
        , EpochNo
geEpoch forall a. Ord a => a -> a -> Bool
<= GAS (ConwayEra StandardCrypto)
act forall s a. s -> Getting a s a -> a
^. forall era. Lens' (GovActionState era) EpochNo
gasExpiresAfterL
        , GovAction (ConwayEra StandardCrypto) -> Bool
f (forall era. GovActionState era -> GovAction era
gasAction GAS (ConwayEra StandardCrypto)
act)
        ]
      committeeState :: CommitteeState (ConwayEra StandardCrypto)
committeeState = forall era. VState era -> CommitteeState era
vsCommitteeState (forall era. CertState era -> VState era
certVState CertState (ConwayEra StandardCrypto)
geCertState)
      knownDReps :: Set (Credential 'DRepRole StandardCrypto)
knownDReps = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ forall era.
VState era
-> Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era))
vsDReps (forall era. CertState era -> VState era
certVState CertState (ConwayEra StandardCrypto)
geCertState)
      knownStakePools :: Set (KeyHash 'StakePool StandardCrypto)
knownStakePools = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ forall era.
PState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
psStakePoolParams (forall era. CertState era -> PState era
certPState CertState (ConwayEra StandardCrypto)
geCertState)
      knownCommitteeAuthorizations :: Set
  (Credential
     'HotCommitteeRole (EraCrypto (ConwayEra StandardCrypto)))
knownCommitteeAuthorizations = forall era.
CommitteeState era
-> Set (Credential 'HotCommitteeRole (EraCrypto era))
authorizedHotCommitteeCredentials CommitteeState (ConwayEra StandardCrypto)
committeeState
      committeeVotableActionIds :: [GovActionId StandardCrypto]
committeeVotableActionIds =
        (GovAction (ConwayEra StandardCrypto) -> Bool)
-> [GovActionId StandardCrypto]
actions (forall era.
ConwayEraPParams era =>
EpochNo -> CommitteeState era -> GovAction era -> Bool
isCommitteeVotingAllowed EpochNo
geEpoch CommitteeState (ConwayEra StandardCrypto)
committeeState)
      drepVotableActionIds :: [GovActionId StandardCrypto]
drepVotableActionIds =
        (GovAction (ConwayEra StandardCrypto) -> Bool)
-> [GovActionId StandardCrypto]
actions forall era. ConwayEraPParams era => GovAction era -> Bool
isDRepVotingAllowed
      stakepoolVotableActionIds :: [GovActionId StandardCrypto]
stakepoolVotableActionIds =
        (GovAction (ConwayEra StandardCrypto) -> Bool)
-> [GovActionId StandardCrypto]
actions forall era. ConwayEraPParams era => GovAction era -> Bool
isStakePoolVotingAllowed
      registeredCredentials :: Set (Credential 'Staking StandardCrypto)
registeredCredentials = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ forall c. UMap c -> Map (Credential 'Staking c) (UMElem c)
umElems forall a b. (a -> b) -> a -> b
$ forall era. DState era -> UMap (EraCrypto era)
dsUnified forall a b. (a -> b) -> a -> b
$ forall era. CertState era -> DState era
certDState CertState (ConwayEra StandardCrypto)
geCertState
   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 StandardCrypto))
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 StandardCrypto))
govSignal forall a b. (a -> b) -> a -> b
$ \Term fn (VotingProcedures (ConwayEra StandardCrypto))
votingProcs Term fn (OSet (ProposalProcedure (ConwayEra StandardCrypto)))
proposalProcs Term fn (StrictSeq (ConwayTxCert (ConwayEra StandardCrypto)))
_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 StandardCrypto))
votingProcs forall a b. (a -> b) -> a -> b
$ \Term
  fn
  (Map
     (Voter StandardCrypto)
     (Map
        (GovActionId StandardCrypto)
        (VotingProcedure (ConwayEra StandardCrypto))))
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 StandardCrypto)
     (Map
        (GovActionId StandardCrypto)
        (VotingProcedure (ConwayEra StandardCrypto))))
votingProcsMap forall a b. (a -> b) -> a -> b
$ \Term
  fn
  (Voter StandardCrypto,
   Map
     (GovActionId StandardCrypto)
     (VotingProcedure (ConwayEra StandardCrypto)))
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 StandardCrypto,
   Map
     (GovActionId StandardCrypto)
     (VotingProcedure (ConwayEra StandardCrypto)))
kvp forall a b. (a -> b) -> a -> b
$ \Term fn (Voter StandardCrypto)
voter Term
  fn
  (Map
     (GovActionId StandardCrypto)
     (VotingProcedure (ConwayEra StandardCrypto)))
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
     (VotingProcedure (ConwayEra StandardCrypto)))
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 StandardCrypto]
committeeVotableActionIds)
                        , forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'HotCommitteeRole StandardCrypto)
committeeHotCred forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set (Credential 'HotCommitteeRole StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
     (VotingProcedure (ConwayEra StandardCrypto)))
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 StandardCrypto]
drepVotableActionIds)
                        , forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (Credential 'DRepRole StandardCrypto)
drepCred forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set (Credential 'DRepRole StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
     (VotingProcedure (ConwayEra StandardCrypto)))
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 StandardCrypto]
stakepoolVotableActionIds)
                        , forall a (fn :: [*] -> * -> *).
(HasSpec fn a, Ord a) =>
Term fn a -> Term fn (Set a) -> Term fn Bool
member_ Term fn (KeyHash 'StakePool StandardCrypto)
poolKeyHash forall a b. (a -> b) -> a -> b
$ forall a (fn :: [*] -> * -> *). Show a => a -> Term fn a
lit Set (KeyHash 'StakePool StandardCrypto)
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 StandardCrypto)))
proposalProcs forall a b. (a -> b) -> a -> b
$ \Term fn (ProposalProcedure (ConwayEra StandardCrypto))
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 StandardCrypto))
proc forall a b. (a -> b) -> a -> b
$ \Term fn Coin
deposit Term fn (RewardAccount StandardCrypto)
returnAddr Term fn (GovAction (ConwayEra StandardCrypto))
govAction Term fn (Anchor StandardCrypto)
_ ->
                [ 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 StandardCrypto)
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 StandardCrypto)
returnAddr forall a b. (a -> b) -> a -> b
$ \Term fn Network
net Term fn (Credential 'Staking StandardCrypto)
cred ->
                    [ forall (fn :: [*] -> * -> *) a b.
(HasSpec fn a, HasSpec fn b) =>
Term fn a -> Term fn b -> Pred fn
dependsOn Term fn (ProposalProcedure (ConwayEra StandardCrypto))
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 StandardCrypto)
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 StandardCrypto)
registeredCredentials
                    ]
                , forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
GovEnv (ConwayEra StandardCrypto)
-> Proposals (ConwayEra StandardCrypto)
-> Term fn (GovAction (ConwayEra StandardCrypto))
-> Pred fn
wfGovAction GovEnv (ConwayEra StandardCrypto)
ge Proposals (ConwayEra StandardCrypto)
ps Term fn (GovAction (ConwayEra StandardCrypto))
govAction
                ]
          ]

wfGovAction ::
  IsConwayUniv fn =>
  GovEnv (ConwayEra StandardCrypto) ->
  Proposals (ConwayEra StandardCrypto) ->
  Term fn (GovAction (ConwayEra StandardCrypto)) ->
  Pred fn
wfGovAction :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
GovEnv (ConwayEra StandardCrypto)
-> Proposals (ConwayEra StandardCrypto)
-> Term fn (GovAction (ConwayEra StandardCrypto))
-> Pred fn
wfGovAction GovEnv {StrictMaybe (ScriptHash (EraCrypto (ConwayEra StandardCrypto)))
gePPolicy :: StrictMaybe (ScriptHash (EraCrypto (ConwayEra StandardCrypto)))
gePPolicy :: forall era. GovEnv era -> StrictMaybe (ScriptHash (EraCrypto era))
gePPolicy, EpochNo
geEpoch :: EpochNo
geEpoch :: forall era. GovEnv era -> EpochNo
geEpoch, PParams (ConwayEra StandardCrypto)
gePParams :: PParams (ConwayEra StandardCrypto)
gePParams :: forall era. GovEnv era -> PParams era
gePParams, CertState (ConwayEra StandardCrypto)
geCertState :: CertState (ConwayEra StandardCrypto)
geCertState :: forall era. GovEnv era -> CertState era
geCertState} Proposals (ConwayEra StandardCrypto)
ps Term fn (GovAction (ConwayEra StandardCrypto))
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 StandardCrypto))
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 StandardCrypto)))
mPrevActionId Term fn (PParamsUpdate (ConwayEra StandardCrypto))
ppUpdate Term fn (StrictMaybe (ScriptHash StandardCrypto))
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 StandardCrypto)))
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 StandardCrypto))]
ppupIds
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (PParamsUpdate (ConwayEra StandardCrypto))
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 StandardCrypto))
ppUpdate forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (PParamsUpdate (ConwayEra StandardCrypto))
wfPParamsUpdateSpec
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ Term fn (StrictMaybe (ScriptHash StandardCrypto))
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 (EraCrypto (ConwayEra StandardCrypto)))
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 StandardCrypto)))
[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 StandardCrypto)))
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 StandardCrypto))]
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 StandardCrypto)))
mPrevActionId forall {p}.
Coercible p (StrictMaybe (GovActionId StandardCrypto)) =>
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 StandardCrypto)))
mPrevActionId forall {p}.
Coercible p (StrictMaybe (GovActionId StandardCrypto)) =>
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 StandardCrypto) Coin)
withdrawMap Term fn (StrictMaybe (ScriptHash StandardCrypto))
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 StandardCrypto) Coin)
withdrawMap) forall a b. (a -> b) -> a -> b
$ \Term fn (RewardAccount StandardCrypto)
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 StandardCrypto)
rewAcnt forall a b. (a -> b) -> a -> b
$ \Term fn Network
net Term fn (Credential 'Staking StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
registeredCredentials
              ]
        , forall (fn :: [*] -> * -> *) p.
(BaseUniverse fn, IsPred p fn) =>
p -> Pred fn
assert forall a b. (a -> b) -> a -> b
$ forall (fn :: [*] -> * -> *) a.
(BaseUniverse fn, Member (FunFn fn) fn, 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 StandardCrypto) 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 StandardCrypto))
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 (EraCrypto (ConwayEra StandardCrypto)))
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 StandardCrypto)
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 StandardCrypto)))
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 StandardCrypto)))
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 StandardCrypto))]
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 StandardCrypto)
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 StandardCrypto)))
mPrevActionId Term fn (Set (Credential 'ColdCommitteeRole StandardCrypto))
_removed Term
  fn (Map (Credential 'ColdCommitteeRole StandardCrypto) 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 StandardCrypto)))
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 StandardCrypto))]
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 StandardCrypto) 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 StandardCrypto)
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 StandardCrypto)))
mPrevActionId Term fn (Constitution (ConwayEra StandardCrypto))
_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 StandardCrypto)))
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 StandardCrypto))]
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 StandardCrypto)
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 StandardCrypto)
registeredCredentials = forall k a. Map k a -> Set k
Map.keysSet forall a b. (a -> b) -> a -> b
$ forall c. UMap c -> Map (Credential 'Staking c) (UMElem c)
umElems forall a b. (a -> b) -> a -> b
$ forall era. DState era -> UMap (EraCrypto era)
dsUnified forall a b. (a -> b) -> a -> b
$ forall era. CertState era -> DState era
certDState CertState (ConwayEra StandardCrypto)
geCertState
    prevGovActionIds :: GovRelation StrictMaybe (ConwayEra StandardCrypto)
prevGovActionIds = Proposals (ConwayEra StandardCrypto)
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 StandardCrypto))]
constitutionIds =
      (GovRelation StrictMaybe (ConwayEra StandardCrypto)
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 (EraCrypto era)
gasId GAS (ConwayEra StandardCrypto)
gas
          | GAS (ConwayEra StandardCrypto)
gas <- [GAS (ConwayEra StandardCrypto)]
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 StandardCrypto)
gas]
          ]
    committeeIds :: [StrictMaybe
   (GovPurposeId 'CommitteePurpose (ConwayEra StandardCrypto))]
committeeIds =
      (GovRelation StrictMaybe (ConwayEra StandardCrypto)
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 (EraCrypto era)
gasId GAS (ConwayEra StandardCrypto)
gas
          | GAS (ConwayEra StandardCrypto)
gas <- [GAS (ConwayEra StandardCrypto)]
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 StandardCrypto)
gas)
          ]
    ppupIds :: [StrictMaybe
   (GovPurposeId 'PParamUpdatePurpose (ConwayEra StandardCrypto))]
ppupIds =
      (GovRelation StrictMaybe (ConwayEra StandardCrypto)
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 (EraCrypto era)
gasId GAS (ConwayEra StandardCrypto)
gas
          | GAS (ConwayEra StandardCrypto)
gas <- [GAS (ConwayEra StandardCrypto)]
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 StandardCrypto)
gas]
          ]
    hardForkIds :: [StrictMaybe
   (GovPurposeId 'HardForkPurpose (ConwayEra StandardCrypto))]
hardForkIds =
      (GovRelation StrictMaybe (ConwayEra StandardCrypto)
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 (EraCrypto era)
gasId GAS (ConwayEra StandardCrypto)
gas
          | GAS (ConwayEra StandardCrypto)
gas <- [GAS (ConwayEra StandardCrypto)]
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 StandardCrypto)
gas]
          ]
    isCommitteeAction :: GovAction era -> Bool
isCommitteeAction UpdateCommittee {} = Bool
True
    isCommitteeAction NoConfidence {} = Bool
True
    isCommitteeAction GovAction era
_ = Bool
False

    findProtVer :: StrictMaybe (GovActionId StandardCrypto) -> ProtVer
findProtVer StrictMaybe (GovActionId StandardCrypto)
SNothing = PParams (ConwayEra StandardCrypto)
gePParams forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL
    findProtVer (SJust GovActionId StandardCrypto
hid) =
      case forall era.
GovActionId (EraCrypto era)
-> Proposals era -> Maybe (GovActionState era)
proposalsLookupId GovActionId StandardCrypto
hid Proposals (ConwayEra StandardCrypto)
ps of
        Just GAS (ConwayEra StandardCrypto)
gas
          | HardForkInitiation StrictMaybe
  (GovPurposeId 'HardForkPurpose (ConwayEra StandardCrypto))
_ 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 StandardCrypto)
gas -> ProtVer
protVer
        Maybe (GAS (ConwayEra StandardCrypto))
_ -> PParams (ConwayEra StandardCrypto)
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 StandardCrypto) -> 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 StandardCrypto) -> ProtVer
findProtVer (coerce :: forall a b. Coercible a b => a -> b
coerce p
mId)
       in Natural
currentMinorVersion

    actions :: [GAS (ConwayEra StandardCrypto)]
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 StandardCrypto)
ps

wfPParamsUpdateSpec :: forall fn. IsConwayUniv fn => Specification fn (PParamsUpdate Conway)
wfPParamsUpdateSpec :: forall (fn :: [*] -> * -> *).
IsConwayUniv fn =>
Specification fn (PParamsUpdate (ConwayEra StandardCrypto))
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 Natural)
_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
          ]