{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Constrained.Conway.MiniTrace (
  spec,
  ConstrainedGeneratorBundle (..),
  ConwayCertGenContext (..),
  constrainedCert,
  constrainedCerts,
  constrainedDeleg,
  constrainedEnact,
  constrainedEpoch,
  constrainedGov,
  constrainedGovCert,
  constrainedNewEpoch,
  constrainedPool,
  constrainedRatify,
  constrainedUtxo,
) where

import Cardano.Ledger.Address (RewardAccount)
import Cardano.Ledger.BaseTypes (
  EpochNo (..),
  Network (..),
  ShelleyBase,
  addEpochInterval,
  natVersion,
 )
import Cardano.Ledger.Coin (Coin, CompactForm (..))
import Cardano.Ledger.Conway (ConwayEra)
import Cardano.Ledger.Conway.Governance (
  EnactState (..),
  GovActionState (..),
  RatifyEnv (..),
  RatifySignal (..),
  RatifyState,
  VotingProcedures,
 )
import Cardano.Ledger.Conway.PParams (ppCommitteeMaxTermLengthL)
import Cardano.Ledger.Conway.Rules (CertsEnv (..), EnactSignal)
import Cardano.Ledger.Conway.TxCert (ConwayDelegCert (..), ConwayGovCert (..), ConwayTxCert (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Credential (Credential)
import Cardano.Ledger.State (
  CommitteeAuthorization (..),
  CommitteeState (..),
  DRep (..),
  EraCertState (..),
  IndividualPoolStake (..),
 )
import Constrained.API
import Control.State.Transition.Extended (STS (..))
import Data.Foldable (Foldable (..))
import qualified Data.List.NonEmpty as NE
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Proxy
import Data.Sequence (Seq)
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics (Generic)
import GHC.TypeLits (KnownSymbol, Symbol, symbolVal)
import Lens.Micro ((^.))
import Test.Cardano.Ledger.Common hiding (forAll)
import Test.Cardano.Ledger.Constrained.Conway (
  EraSpecCert (..),
  UtxoExecContext,
  certEnvSpec,
  certsEnvSpec,
  coerce_,
  committeeMinSize_,
  conwayDelegCertSpec,
  conwayTxCertSpec,
  delegEnvSpec,
  epochSignalSpec,
  epochStateSpec,
  genUtxoExecContext,
  govCertSpec,
  govEnvSpec,
  govProceduresSpec,
  govProposalsSpec,
  newEpochStateSpec,
  pStateSpec,
  poolCertSpec,
  poolEnvSpec,
  protocolVersion_,
  txCertsSpec,
  utxoEnvSpec,
  utxoStateSpec,
  utxoTxSpec,
 )
import Test.Cardano.Ledger.Constrained.Conway.GovCert (govCertEnvSpec)
import Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs (
  conwayCertStateSpec,
  delegators,
  whoDelegatesSpec,
 )
import Test.Cardano.Ledger.Constrained.Conway.WitnessUniverse (WitUniv, genWitUniv)
import Test.Cardano.Ledger.Generic.Proof (goSTS)

data ConstrainedGeneratorBundle ctx rule era = ConstrainedGeneratorBundle
  { forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era -> Gen ctx
cgbContextGen :: Gen ctx
  , forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx -> Specification (Environment (EraRule rule era))
cgbEnvironmentSpec ::
      ctx ->
      Specification (Environment (EraRule rule era))
  , forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
cgbStateSpec ::
      ctx ->
      Environment (EraRule rule era) ->
      Specification (State (EraRule rule era))
  , forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
cgbSignalSpec ::
      ctx ->
      Environment (EraRule rule era) ->
      State (EraRule rule era) ->
      Specification (Signal (EraRule rule era))
  }

-- ====================================================================

-- | Generate either a list of signals, or a list of error messages
minitraceEither ::
  forall rule era ctx.
  ( HasSpec (Environment (EraRule rule era))
  , HasSpec (State (EraRule rule era))
  , HasSpec (Signal (EraRule rule era))
  , BaseM (EraRule rule era) ~ ShelleyBase
  , STS (EraRule rule era)
  , ToExpr (Signal (EraRule rule era))
  , ToExpr (State (EraRule rule era))
  ) =>
  Int ->
  ConstrainedGeneratorBundle ctx rule era ->
  Gen (Either [String] [Signal (EraRule rule era)])
minitraceEither :: forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, STS (EraRule rule era),
 ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
Int
-> ConstrainedGeneratorBundle ctx rule era
-> Gen (Either [[Char]] [Signal (EraRule rule era)])
minitraceEither Int
n0 ConstrainedGeneratorBundle {Gen ctx
ctx -> Specification (Environment (EraRule rule era))
ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
cgbContextGen :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era -> Gen ctx
cgbEnvironmentSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx -> Specification (Environment (EraRule rule era))
cgbStateSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
cgbSignalSpec :: forall ctx (rule :: Symbol) era.
ConstrainedGeneratorBundle ctx rule era
-> ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
cgbContextGen :: Gen ctx
cgbEnvironmentSpec :: ctx -> Specification (Environment (EraRule rule era))
cgbStateSpec :: ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
cgbSignalSpec :: ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
..} = do
  !ctxt <- Gen ctx
cgbContextGen
  !env <- genFromSpec $ cgbEnvironmentSpec ctxt
  !state <- genFromSpec $ cgbStateSpec ctxt env
  let go :: State (EraRule rule era) -> Int -> Gen (Either [String] [Signal (EraRule rule era)])
      go State (EraRule rule era)
_ Int
0 = Either [[Char]] [Signal (EraRule rule era)]
-> Gen (Either [[Char]] [Signal (EraRule rule era)])
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Signal (EraRule rule era)]
-> Either [[Char]] [Signal (EraRule rule era)]
forall a b. b -> Either a b
Right [])
      go State (EraRule rule era)
st Int
n = do
        !signal <- Specification (Signal (EraRule rule era))
-> Gen (Signal (EraRule rule era))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (Specification (Signal (EraRule rule era))
 -> Gen (Signal (EraRule rule era)))
-> Specification (Signal (EraRule rule era))
-> Gen (Signal (EraRule rule era))
forall a b. (a -> b) -> a -> b
$ ctx
-> Environment (EraRule rule era)
-> State (EraRule rule era)
-> Specification (Signal (EraRule rule era))
cgbSignalSpec ctx
ctxt Environment (EraRule rule era)
env State (EraRule rule era)
st
        goSTS @rule @era @(Gen (Either [String] [Signal (EraRule rule era)]))
          env
          st
          signal
          ( \case
              Left NonEmpty (PredicateFailure (EraRule rule era))
ps ->
                Either [[Char]] [Signal (EraRule rule era)]
-> Gen (Either [[Char]] [Signal (EraRule rule era)])
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                  ( [[Char]] -> Either [[Char]] [Signal (EraRule rule era)]
forall a b. a -> Either a b
Left
                      ( [ [Char]
"\nSIGNAL = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. Show a => a -> [Char]
show (Signal (EraRule rule era) -> Expr
forall a. ToExpr a => a -> Expr
toExpr Signal (EraRule rule era)
signal)
                        , [Char]
"\nSTATE = " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Expr -> [Char]
forall a. Show a => a -> [Char]
show (State (EraRule rule era) -> Expr
forall a. ToExpr a => a -> Expr
toExpr State (EraRule rule era)
state)
                        , [Char]
"\nPredicateFailures"
                        ]
                          [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ (PredicateFailure (EraRule rule era) -> [Char])
-> [PredicateFailure (EraRule rule era)] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map PredicateFailure (EraRule rule era) -> [Char]
forall a. Show a => a -> [Char]
show (NonEmpty (PredicateFailure (EraRule rule era))
-> [PredicateFailure (EraRule rule era)]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (PredicateFailure (EraRule rule era))
ps)
                      )
                  )
              Right !State (EraRule rule era)
state2 -> do
                ans <- State (EraRule rule era)
-> Int -> Gen (Either [[Char]] [Signal (EraRule rule era)])
go State (EraRule rule era)
state2 (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
                case ans of
                  Left [[Char]]
xs -> Either [[Char]] [Signal (EraRule rule era)]
-> Gen (Either [[Char]] [Signal (EraRule rule era)])
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([[Char]] -> Either [[Char]] [Signal (EraRule rule era)]
forall a b. a -> Either a b
Left [[Char]]
xs)
                  Right [Signal (EraRule rule era)]
more -> Either [[Char]] [Signal (EraRule rule era)]
-> Gen (Either [[Char]] [Signal (EraRule rule era)])
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Signal (EraRule rule era)]
-> Either [[Char]] [Signal (EraRule rule era)]
forall a b. b -> Either a b
Right (Signal (EraRule rule era)
signal Signal (EraRule rule era)
-> [Signal (EraRule rule era)] -> [Signal (EraRule rule era)]
forall a. a -> [a] -> [a]
: [Signal (EraRule rule era)]
more))
          )
  go state n0

minitraceProp ::
  forall rule era ctx.
  ( HasSpec (Environment (EraRule rule era))
  , HasSpec (State (EraRule rule era))
  , HasSpec (Signal (EraRule rule era))
  , BaseM (EraRule rule era) ~ ShelleyBase
  , STS (EraRule rule era)
  , ToExpr (Signal (EraRule rule era))
  , ToExpr (State (EraRule rule era))
  ) =>
  Int ->
  ConstrainedGeneratorBundle ctx rule era ->
  (Signal (EraRule rule era) -> String) ->
  Gen Property
minitraceProp :: forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, STS (EraRule rule era),
 ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
Int
-> ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char])
-> Gen Property
minitraceProp Int
n0 ConstrainedGeneratorBundle ctx rule era
cgb Signal (EraRule rule era) -> [Char]
classifier = do
  ans <- forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, STS (EraRule rule era),
 ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
Int
-> ConstrainedGeneratorBundle ctx rule era
-> Gen (Either [[Char]] [Signal (EraRule rule era)])
minitraceEither @rule @era Int
n0 ConstrainedGeneratorBundle ctx rule era
cgb
  let
    classifyFirst t -> [Char]
_ [] Property
p = Property
p
    classifyFirst t -> [Char]
f (t
x : [t]
_) Property
p = case t -> [Char]
f t
x of
      [Char]
"" -> Property
p
      [Char]
cl -> Bool -> [Char] -> Property -> Property
forall prop. Testable prop => Bool -> [Char] -> prop -> Property
classify Bool
True [Char]
cl Property
p
  case ans of
    Left [[Char]]
zs -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ [Char] -> Property -> Property
forall prop. Testable prop => [Char] -> prop -> Property
counterexample ([[Char]] -> [Char]
unlines [[Char]]
zs) (Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
False)
    Right [Signal (EraRule rule era)]
s -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property)
-> (Property -> Property) -> Property -> Gen Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Signal (EraRule rule era) -> [Char])
-> [Signal (EraRule rule era)] -> Property -> Property
forall {t}. (t -> [Char]) -> [t] -> Property -> Property
classifyFirst Signal (EraRule rule era) -> [Char]
classifier [Signal (EraRule rule era)]
s (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True

runMinitrace ::
  forall (rule :: Symbol) era ctx.
  ( HasSpec (Environment (EraRule rule era))
  , HasSpec (State (EraRule rule era))
  , HasSpec (Signal (EraRule rule era))
  , BaseM (EraRule rule era) ~ ShelleyBase
  , KnownSymbol rule
  , STS (EraRule rule era)
  , ToExpr (Signal (EraRule rule era))
  , ToExpr (State (EraRule rule era))
  ) =>
  ConstrainedGeneratorBundle ctx rule era ->
  (Signal (EraRule rule era) -> String) ->
  Spec
runMinitrace :: forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle ctx rule era
cgb Signal (EraRule rule era) -> [Char]
classifier =
  [Char] -> Property -> Spec
forall prop.
(HasCallStack, Testable prop) =>
[Char] -> prop -> Spec
prop
    (Proxy rule -> [Char]
forall (n :: Symbol) (proxy :: Symbol -> *).
KnownSymbol n =>
proxy n -> [Char]
symbolVal (Proxy rule -> [Char]) -> Proxy rule -> [Char]
forall a b. (a -> b) -> a -> b
$ forall {k} (t :: k). Proxy t
forall (t :: Symbol). Proxy t
Proxy @rule)
    (Int -> Gen Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
50 (forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, STS (EraRule rule era),
 ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
Int
-> ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char])
-> Gen Property
minitraceProp @rule @era Int
50 ConstrainedGeneratorBundle ctx rule era
cgb Signal (EraRule rule era) -> [Char]
classifier))

genDelegCtx :: Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
genDelegCtx :: Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
genDelegCtx = do
  witUniv <- Int -> Gen (WitUniv ConwayEra)
forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
300
  ccec <- genFromSpec $ conwayCertExecContextSpec witUniv 4
  pure (witUniv, ccec)

certStateSpec_ ::
  EraSpecCert era =>
  (WitUniv era, ConwayCertGenContext era) -> Specification (CertState era)
certStateSpec_ :: forall era.
EraSpecCert era =>
(WitUniv era, ConwayCertGenContext era)
-> Specification (CertState era)
certStateSpec_ (WitUniv era
u, ConwayCertGenContext {Map RewardAccount Coin
Map (Credential DRepRole) (Set (Credential Staking))
VotingProcedures era
ccccWithdrawals :: Map RewardAccount Coin
ccccVotes :: VotingProcedures era
ccccDelegatees :: Map (Credential DRepRole) (Set (Credential Staking))
ccccDelegatees :: forall era.
ConwayCertGenContext era
-> Map (Credential DRepRole) (Set (Credential Staking))
ccccVotes :: forall era. ConwayCertGenContext era -> VotingProcedures era
ccccWithdrawals :: forall era. ConwayCertGenContext era -> Map RewardAccount Coin
..}) =
  WitUniv era
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> SpecificationD Deps (CertState era)
forall era.
EraSpecCert era =>
WitUniv era
-> Set (Credential DRepRole)
-> Map RewardAccount Coin
-> Specification (CertState era)
certStateSpec WitUniv era
u (Map (Credential DRepRole) (Set (Credential Staking))
-> Set (Credential DRepRole)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential DRepRole) (Set (Credential Staking))
ccccDelegatees) Map RewardAccount Coin
ccccWithdrawals

ratifyEnvSpec ::
  [GovActionState era] ->
  Specification (RatifyEnv ConwayEra)
ratifyEnvSpec :: forall era.
[GovActionState era] -> Specification (RatifyEnv ConwayEra)
ratifyEnvSpec [GovActionState era]
govActionMap =
  FunTy
  (MapList Term (Args (SimpleRep (RatifyEnv ConwayEra)))) [Pred]
-> Specification (RatifyEnv ConwayEra)
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (RatifyEnv ConwayEra)))) [Pred]
 -> Specification (RatifyEnv ConwayEra))
-> FunTy
     (MapList Term (Args (SimpleRep (RatifyEnv ConwayEra)))) [Pred]
-> Specification (RatifyEnv ConwayEra)
forall a b. (a -> b) -> a -> b
$ \TermD Deps (ConwayInstantStake ConwayEra)
_ Term PoolDistr
poolDistr Term (Map DRep (CompactForm Coin))
drepDistr Term (Map (Credential DRepRole) DRepState)
drepState TermD Deps EpochNo
_ Term (CommitteeState ConwayEra)
committeeState TermD Deps (ConwayAccounts ConwayEra)
_ TermD Deps (Map (KeyHash StakePool) StakePoolState)
_ ->
    [ -- Bias the generator towards generating DReps that have stake and are registered
      ((forall b. Term b -> b) -> GE (Set DRep))
-> (Term (Set DRep) -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists
        ( \forall b. Term b -> b
eval ->
            Set DRep -> GE (Set DRep)
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
              ( Set DRep -> Set DRep -> Set DRep
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                  (Map DRep (CompactForm Coin) -> Set DRep
forall k a. Map k a -> Set k
Map.keysSet (Term (Map DRep (CompactForm Coin)) -> Map DRep (CompactForm Coin)
forall b. Term b -> b
eval Term (Map DRep (CompactForm Coin))
drepDistr))
                  ((Credential DRepRole -> DRep)
-> Set (Credential DRepRole) -> Set DRep
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential DRepRole -> DRep
DRepCredential (Set (Credential DRepRole) -> Set DRep)
-> Set (Credential DRepRole) -> Set DRep
forall a b. (a -> b) -> a -> b
$ Map (Credential DRepRole) DRepState -> Set (Credential DRepRole)
forall k a. Map k a -> Set k
Map.keysSet (Term (Map (Credential DRepRole) DRepState)
-> Map (Credential DRepRole) DRepState
forall b. Term b -> b
eval Term (Map (Credential DRepRole) DRepState)
drepState))
              )
        )
        ( \Term (Set DRep)
common ->
            [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set DRep) -> Term (Set DRep) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set DRep)
common (Term (Map DRep (CompactForm Coin)) -> Term (Set DRep)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map DRep (CompactForm Coin))
drepDistr)
            , Term (Map (Credential DRepRole) DRepState)
-> (Map (Credential DRepRole) DRepState -> Map DRep DRepState)
-> (Term (Map DRep DRepState) -> Pred)
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential DRepRole) DRepState)
drepState ((Credential DRepRole -> DRep)
-> Map (Credential DRepRole) DRepState -> Map DRep DRepState
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys Credential DRepRole -> DRep
DRepCredential) (Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred)
-> (Term (Map DRep DRepState) -> Term Bool)
-> Term (Map DRep DRepState)
-> Pred
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (Set DRep) -> Term (Set DRep) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set DRep)
common (Term (Set DRep) -> Term Bool)
-> (Term (Map DRep DRepState) -> Term (Set DRep))
-> Term (Map DRep DRepState)
-> Term Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Term (Map DRep DRepState) -> Term (Set DRep)
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_)
            , Term (Map DRep (CompactForm Coin))
drepDistr Term (Map DRep (CompactForm Coin)) -> Term (Set DRep) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Set DRep)
common
            ]
        )
    , Term PoolDistr
-> FunTy (MapList Term (ProductAsList PoolDistr)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term PoolDistr
poolDistr (FunTy (MapList Term (ProductAsList PoolDistr)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList PoolDistr)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Map (KeyHash StakePool) IndividualPoolStake)
poolStake TermD Deps (CompactForm Coin)
_ ->
        ((forall b. Term b -> b) -> GE (Set (KeyHash StakePool)))
-> (Term (Set (KeyHash StakePool)) -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists
          ( \forall b. Term b -> b
eval ->
              Set (KeyHash StakePool) -> GE (Set (KeyHash StakePool))
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                ( Set (KeyHash StakePool)
-> Set (KeyHash StakePool) -> Set (KeyHash StakePool)
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                    (Map (KeyHash StakePool) IndividualPoolStake
-> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet (Map (KeyHash StakePool) IndividualPoolStake
 -> Set (KeyHash StakePool))
-> Map (KeyHash StakePool) IndividualPoolStake
-> Set (KeyHash StakePool)
forall a b. (a -> b) -> a -> b
$ Term (Map (KeyHash StakePool) IndividualPoolStake)
-> Map (KeyHash StakePool) IndividualPoolStake
forall b. Term b -> b
eval Term (Map (KeyHash StakePool) IndividualPoolStake)
poolStake)
                    Set (KeyHash StakePool)
spoVotes
                )
          )
          ( \Term (Set (KeyHash StakePool))
common ->
              [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (KeyHash StakePool))
-> Term (Set (KeyHash StakePool)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set (KeyHash StakePool))
common (Term (Map (KeyHash StakePool) IndividualPoolStake)
-> Term (Set (KeyHash StakePool))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (KeyHash StakePool) IndividualPoolStake)
poolStake)
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (KeyHash StakePool))
-> Term (Set (KeyHash StakePool)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
subset_ Term (Set (KeyHash StakePool))
common (Set (KeyHash StakePool) -> Term (Set (KeyHash StakePool))
forall a. HasSpec a => a -> Term a
lit Set (KeyHash StakePool)
spoVotes)
              , Term (Map (KeyHash StakePool) IndividualPoolStake)
poolStake Term (Map (KeyHash StakePool) IndividualPoolStake)
-> Term (Set (KeyHash StakePool)) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Set (KeyHash StakePool))
common
              ]
          )
    , Term (CommitteeState ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (CommitteeState ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (CommitteeState ConwayEra)
committeeState (FunTy
   (MapList Term (ProductAsList (CommitteeState ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (CommitteeState ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (Credential ColdCommitteeRole) CommitteeAuthorization)
[var| cs |] ->
        ((forall b. Term b -> b) -> GE (Set CommitteeAuthorization))
-> (Term (Set CommitteeAuthorization) -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists
          ( \forall b. Term b -> b
eval ->
              Set CommitteeAuthorization -> GE (Set CommitteeAuthorization)
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set CommitteeAuthorization -> GE (Set CommitteeAuthorization))
-> Set CommitteeAuthorization -> GE (Set CommitteeAuthorization)
forall a b. (a -> b) -> a -> b
$
                (Credential HotCommitteeRole -> CommitteeAuthorization)
-> Set (Credential HotCommitteeRole) -> Set CommitteeAuthorization
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential HotCommitteeRole -> CommitteeAuthorization
CommitteeHotCredential Set (Credential HotCommitteeRole)
ccVotes
                  Set CommitteeAuthorization
-> Set CommitteeAuthorization -> Set CommitteeAuthorization
forall a. Ord a => Set a -> Set a -> Set a
`Set.intersection` (CommitteeAuthorization
 -> Set CommitteeAuthorization -> Set CommitteeAuthorization)
-> Set CommitteeAuthorization
-> Map (Credential ColdCommitteeRole) CommitteeAuthorization
-> Set CommitteeAuthorization
forall a b.
(a -> b -> b) -> b -> Map (Credential ColdCommitteeRole) a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr' CommitteeAuthorization
-> Set CommitteeAuthorization -> Set CommitteeAuthorization
forall a. Ord a => a -> Set a -> Set a
Set.insert Set CommitteeAuthorization
forall a. Monoid a => a
mempty (Term (Map (Credential ColdCommitteeRole) CommitteeAuthorization)
-> Map (Credential ColdCommitteeRole) CommitteeAuthorization
forall b. Term b -> b
eval Term (Map (Credential ColdCommitteeRole) CommitteeAuthorization)
cs)
          )
          ( \ Term (Set CommitteeAuthorization)
[var| common |] ->
              [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set CommitteeAuthorization)
common Term (Set CommitteeAuthorization)
-> Term (Set CommitteeAuthorization) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term [CommitteeAuthorization] -> Term (Set CommitteeAuthorization)
forall a. (Ord a, HasSpec a) => Term [a] -> Term (Set a)
fromList_ (Term (Map (Credential ColdCommitteeRole) CommitteeAuthorization)
-> Term [CommitteeAuthorization]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential ColdCommitteeRole) CommitteeAuthorization)
cs)
              , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set CommitteeAuthorization)
common Term (Set CommitteeAuthorization)
-> Term (Set CommitteeAuthorization) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Set CommitteeAuthorization -> Term (Set CommitteeAuthorization)
forall a. HasSpec a => a -> Term a
lit ((Credential HotCommitteeRole -> CommitteeAuthorization)
-> Set (Credential HotCommitteeRole) -> Set CommitteeAuthorization
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Credential HotCommitteeRole -> CommitteeAuthorization
CommitteeHotCredential Set (Credential HotCommitteeRole)
ccVotes)
              , Term (Map (Credential ColdCommitteeRole) CommitteeAuthorization)
cs Term (Map (Credential ColdCommitteeRole) CommitteeAuthorization)
-> Term (Set CommitteeAuthorization) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Set CommitteeAuthorization)
common
              ]
          )
    , Term PoolDistr
-> FunTy (MapList Term (ProductAsList PoolDistr)) [Pred] -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term PoolDistr
poolDistr (FunTy (MapList Term (ProductAsList PoolDistr)) [Pred] -> Pred)
-> FunTy (MapList Term (ProductAsList PoolDistr)) [Pred] -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Map (KeyHash StakePool) IndividualPoolStake)
[var| individualStakesCompact |] TermD Deps (CompactForm Coin)
[var| totalStakeCompact |] ->
        [ Pred -> Pred
forall p. IsPred p => p -> Pred
assert (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$
            Term (Map (KeyHash StakePool) IndividualPoolStake)
-> (Map (KeyHash StakePool) IndividualPoolStake -> [Word64])
-> (Term [Word64] -> [Term Bool])
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify
              Term (Map (KeyHash StakePool) IndividualPoolStake)
individualStakesCompact
              ((IndividualPoolStake -> Word64)
-> [IndividualPoolStake] -> [Word64]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\IndividualPoolStake {individualTotalPoolStake :: IndividualPoolStake -> CompactForm Coin
individualTotalPoolStake = CompactCoin Word64
c} -> Word64
c) ([IndividualPoolStake] -> [Word64])
-> (Map (KeyHash StakePool) IndividualPoolStake
    -> [IndividualPoolStake])
-> Map (KeyHash StakePool) IndividualPoolStake
-> [Word64]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map (KeyHash StakePool) IndividualPoolStake
-> [IndividualPoolStake]
forall k a. Map k a -> [a]
Map.elems)
              ( \ Term [Word64]
[var| stakes |] ->
                  [ TermD Deps (CompactForm Coin) -> Term Word64
forall a b.
(HasSpec a, HasSpec b, CoercibleLike a b) =>
Term a -> Term b
coerce_ TermD Deps (CompactForm Coin)
totalStakeCompact Term Word64 -> Term Word64 -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Term [Word64] -> Term Word64
forall a. Foldy a => Term [a] -> Term a
sum_ Term [Word64]
stakes
                  ]
              )
        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term (Map (KeyHash StakePool) IndividualPoolStake) -> Term Bool
forall a. (HasSpec a, Sized a) => Term a -> Term Bool
null_ Term (Map (KeyHash StakePool) IndividualPoolStake)
individualStakesCompact)
        -- TODO make sure individual stakes add up to 1
        ]
    ]
  where
    spoVotes :: Set (KeyHash StakePool)
spoVotes =
      (GovActionState era
 -> Set (KeyHash StakePool) -> Set (KeyHash StakePool))
-> Set (KeyHash StakePool)
-> [GovActionState era]
-> Set (KeyHash StakePool)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr'
        ( \GovActionState {Map (KeyHash StakePool) Vote
gasStakePoolVotes :: Map (KeyHash StakePool) Vote
gasStakePoolVotes :: forall era. GovActionState era -> Map (KeyHash StakePool) Vote
gasStakePoolVotes} Set (KeyHash StakePool)
s ->
            Map (KeyHash StakePool) Vote -> Set (KeyHash StakePool)
forall k a. Map k a -> Set k
Map.keysSet Map (KeyHash StakePool) Vote
gasStakePoolVotes Set (KeyHash StakePool)
-> Set (KeyHash StakePool) -> Set (KeyHash StakePool)
forall a. Semigroup a => a -> a -> a
<> Set (KeyHash StakePool)
s
        )
        Set (KeyHash StakePool)
forall a. Monoid a => a
mempty
        [GovActionState era]
govActionMap
    ccVotes :: Set (Credential HotCommitteeRole)
ccVotes =
      (GovActionState era
 -> Set (Credential HotCommitteeRole)
 -> Set (Credential HotCommitteeRole))
-> Set (Credential HotCommitteeRole)
-> [GovActionState era]
-> Set (Credential HotCommitteeRole)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr'
        ( \GovActionState {Map (Credential HotCommitteeRole) Vote
gasCommitteeVotes :: Map (Credential HotCommitteeRole) Vote
gasCommitteeVotes :: forall era.
GovActionState era -> Map (Credential HotCommitteeRole) Vote
gasCommitteeVotes} Set (Credential HotCommitteeRole)
s ->
            Map (Credential HotCommitteeRole) Vote
-> Set (Credential HotCommitteeRole)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential HotCommitteeRole) Vote
gasCommitteeVotes Set (Credential HotCommitteeRole)
-> Set (Credential HotCommitteeRole)
-> Set (Credential HotCommitteeRole)
forall a. Semigroup a => a -> a -> a
<> Set (Credential HotCommitteeRole)
s
        )
        Set (Credential HotCommitteeRole)
forall a. Monoid a => a
mempty
        [GovActionState era]
govActionMap

ratifyStateSpec ::
  RatifyEnv ConwayEra ->
  Specification (RatifyState ConwayEra)
ratifyStateSpec :: RatifyEnv ConwayEra -> Specification (RatifyState ConwayEra)
ratifyStateSpec RatifyEnv {Map (KeyHash StakePool) StakePoolState
Map DRep (CompactForm Coin)
Map (Credential DRepRole) DRepState
Accounts ConwayEra
CommitteeState ConwayEra
PoolDistr
InstantStake ConwayEra
EpochNo
reInstantStake :: InstantStake ConwayEra
reStakePoolDistr :: PoolDistr
reDRepDistr :: Map DRep (CompactForm Coin)
reDRepState :: Map (Credential DRepRole) DRepState
reCurrentEpoch :: EpochNo
reCommitteeState :: CommitteeState ConwayEra
reAccounts :: Accounts ConwayEra
reStakePools :: Map (KeyHash StakePool) StakePoolState
reStakePools :: forall era. RatifyEnv era -> Map (KeyHash StakePool) StakePoolState
reAccounts :: forall era. RatifyEnv era -> Accounts era
reCommitteeState :: forall era. RatifyEnv era -> CommitteeState era
reCurrentEpoch :: forall era. RatifyEnv era -> EpochNo
reDRepState :: forall era. RatifyEnv era -> Map (Credential DRepRole) DRepState
reDRepDistr :: forall era. RatifyEnv era -> Map DRep (CompactForm Coin)
reStakePoolDistr :: forall era. RatifyEnv era -> PoolDistr
reInstantStake :: forall era. RatifyEnv era -> InstantStake era
..} =
  FunTy
  (MapList Term (Args (SimpleRep (RatifyState ConwayEra)))) Pred
-> Specification (RatifyState ConwayEra)
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (RatifyState ConwayEra)))) Pred
 -> Specification (RatifyState ConwayEra))
-> FunTy
     (MapList Term (Args (SimpleRep (RatifyState ConwayEra)))) Pred
-> Specification (RatifyState ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (EnactState ConwayEra)
ens Term (Seq (GovActionState ConwayEra))
enacted Term (Set GovActionId)
expired Term Bool
_ ->
    [Pred] -> Pred
forall a. Monoid a => [a] -> a
mconcat
      [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Seq (GovActionState ConwayEra))
enacted Term (Seq (GovActionState ConwayEra))
-> Term (Seq (GovActionState ConwayEra)) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Seq (GovActionState ConwayEra)
-> Term (Seq (GovActionState ConwayEra))
forall a. HasSpec a => a -> Term a
lit Seq (GovActionState ConwayEra)
forall a. Monoid a => a
mempty
      , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set GovActionId)
expired Term (Set GovActionId) -> Term (Set GovActionId) -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Set GovActionId -> Term (Set GovActionId)
forall a. HasSpec a => a -> Term a
lit Set GovActionId
forall a. Monoid a => a
mempty
      , Term (EnactState ConwayEra)
-> FunTy
     (MapList Term (Args (SimpleRep (EnactState ConwayEra)))) [Pred]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (EnactState ConwayEra)
ens (FunTy
   (MapList Term (Args (SimpleRep (EnactState ConwayEra)))) [Pred]
 -> Pred)
-> FunTy
     (MapList Term (Args (SimpleRep (EnactState ConwayEra)))) [Pred]
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (Committee ConwayEra))
mbyCmt TermD Deps (Constitution ConwayEra)
_ Term (PParams ConwayEra)
pp Term (PParams ConwayEra)
_ Term Coin
_ TermD Deps (Map (Credential Staking) Coin)
_ TermD Deps (GovRelation StrictMaybe)
_ ->
          [ (Term (StrictMaybe (Committee ConwayEra))
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (StrictMaybe (Committee ConwayEra)))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (StrictMaybe (Committee ConwayEra))
mbyCmt)
              (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
              ( FunTy (MapList Term (Args (Committee ConwayEra))) Pred
-> Weighted (BinderD Deps) (Committee ConwayEra)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args (Committee ConwayEra))) Pred
 -> Weighted (BinderD Deps) (Committee ConwayEra))
-> FunTy (MapList Term (Args (Committee ConwayEra))) Pred
-> Weighted (BinderD Deps) (Committee ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (Committee ConwayEra)
cmt -> Term (Committee ConwayEra)
-> FunTy (MapList Term (ProductAsList (Committee ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (Committee ConwayEra)
cmt (FunTy (MapList Term (ProductAsList (Committee ConwayEra))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (Committee ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (Map (Credential ColdCommitteeRole) EpochNo)
cmtMap TermD Deps UnitInterval
_ ->
                  ((forall b. Term b -> b)
 -> GE (Set (Credential ColdCommitteeRole)))
-> (Term (Set (Credential ColdCommitteeRole)) -> [Pred]) -> Pred
forall a p.
(HasSpec a, IsPred p) =>
((forall b. Term b -> b) -> GE a) -> (Term a -> p) -> Pred
exists
                    ( \forall b. Term b -> b
eval ->
                        Set (Credential ColdCommitteeRole)
-> GE (Set (Credential ColdCommitteeRole))
forall a. a -> GE a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Set (Credential ColdCommitteeRole)
 -> GE (Set (Credential ColdCommitteeRole)))
-> Set (Credential ColdCommitteeRole)
-> GE (Set (Credential ColdCommitteeRole))
forall a b. (a -> b) -> a -> b
$
                          Set (Credential ColdCommitteeRole)
-> Set (Credential ColdCommitteeRole)
-> Set (Credential ColdCommitteeRole)
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection
                            Set (Credential ColdCommitteeRole)
ccColdKeys
                            (Term (Set (Credential ColdCommitteeRole))
-> Set (Credential ColdCommitteeRole)
forall b. Term b -> b
eval (Term (Set (Credential ColdCommitteeRole))
 -> Set (Credential ColdCommitteeRole))
-> Term (Set (Credential ColdCommitteeRole))
-> Set (Credential ColdCommitteeRole)
forall a b. (a -> b) -> a -> b
$ Term (Map (Credential ColdCommitteeRole) EpochNo)
-> Term (Set (Credential ColdCommitteeRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential ColdCommitteeRole) EpochNo)
cmtMap)
                    )
                    ( \Term (Set (Credential ColdCommitteeRole))
common ->
                        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential ColdCommitteeRole))
common Term (Set (Credential ColdCommitteeRole))
-> Term (Set (Credential ColdCommitteeRole)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Set (Credential ColdCommitteeRole)
-> Term (Set (Credential ColdCommitteeRole))
forall a. HasSpec a => a -> Term a
lit Set (Credential ColdCommitteeRole)
ccColdKeys
                        , Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Set (Credential ColdCommitteeRole))
common Term (Set (Credential ColdCommitteeRole))
-> Term (Set (Credential ColdCommitteeRole)) -> Term Bool
forall a.
(Ord a, HasSpec a) =>
Term (Set a) -> Term (Set a) -> Term Bool
`subset_` Term (Map (Credential ColdCommitteeRole) EpochNo)
-> Term (Set (Credential ColdCommitteeRole))
forall k v.
(HasSpec (Map k v), HasSpec v, HasSpec k, Ord k, IsNormalType k,
 IsNormalType v) =>
Term (Map k v) -> Term (Set k)
dom_ Term (Map (Credential ColdCommitteeRole) EpochNo)
cmtMap
                        , Term (Map (Credential ColdCommitteeRole) EpochNo)
cmtMap Term (Map (Credential ColdCommitteeRole) EpochNo)
-> Term (Set (Credential ColdCommitteeRole)) -> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Set (Credential ColdCommitteeRole))
common
                        ]
                    )
              )
          , Term (PParams ConwayEra) -> Pred
disableBootstrap Term (PParams ConwayEra)
pp
          , Term (PParams ConwayEra) -> Pred
preferSmallerCCMinSizeValues Term (PParams ConwayEra)
pp
          ]
      ]
  where
    ccColdKeys :: Set (Credential ColdCommitteeRole)
ccColdKeys =
      let CommitteeState Map (Credential ColdCommitteeRole) CommitteeAuthorization
m = CommitteeState ConwayEra
reCommitteeState
       in Map (Credential ColdCommitteeRole) CommitteeAuthorization
-> Set (Credential ColdCommitteeRole)
forall k a. Map k a -> Set k
Map.keysSet Map (Credential ColdCommitteeRole) CommitteeAuthorization
m
    -- Bootstrap is not in the spec
    disableBootstrap :: Term (PParams ConwayEra) -> Pred
    disableBootstrap :: Term (PParams ConwayEra) -> Pred
disableBootstrap Term (PParams ConwayEra)
pp = Term (PParams ConwayEra)
-> FunTy (MapList Term (ProductAsList (PParams ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (PParams ConwayEra)
pp (FunTy (MapList Term (ProductAsList (PParams ConwayEra))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (PParams ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (SimplePParams ConwayEra)
simplepp ->
      Term ProtVer
-> FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match (Term (SimplePParams ConwayEra) -> Term ProtVer
forall era.
EraSpecPParams era =>
Term (SimplePParams era) -> Term ProtVer
protocolVersion_ Term (SimplePParams ConwayEra)
simplepp) (FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred)
-> FunTy (MapList Term (ProductAsList ProtVer)) Pred -> Pred
forall a b. (a -> b) -> a -> b
$ \Term Version
major TermD Deps Natural
_ ->
        Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term Bool -> Term Bool
not_ (Term Version
major Term Version -> Term Version -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Version -> Term Version
forall a. HasSpec a => a -> Term a
lit (forall (v :: Natural).
(KnownNat v, MinVersion <= v, v <= MaxVersion) =>
Version
natVersion @9))

    preferSmallerCCMinSizeValues ::
      Term (PParams ConwayEra) ->
      Pred
    preferSmallerCCMinSizeValues :: Term (PParams ConwayEra) -> Pred
preferSmallerCCMinSizeValues Term (PParams ConwayEra)
pp = Term (PParams ConwayEra)
-> FunTy (MapList Term (ProductAsList (PParams ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (PParams ConwayEra)
pp (FunTy (MapList Term (ProductAsList (PParams ConwayEra))) Pred
 -> Pred)
-> FunTy (MapList Term (ProductAsList (PParams ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (SimplePParams ConwayEra)
simplepp ->
      TermD Deps Natural -> Specification Natural -> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies (Term (SimplePParams ConwayEra) -> TermD Deps Natural
forall era.
EraSpecPParams era =>
Term (SimplePParams era) -> TermD Deps Natural
committeeMinSize_ Term (SimplePParams ConwayEra)
simplepp) (Specification Natural -> Pred) -> Specification Natural -> Pred
forall a b. (a -> b) -> a -> b
$
        (Int, Specification Natural)
-> (Int, Specification Natural) -> Specification Natural
forall a.
HasSpec a =>
(Int, Specification a) -> (Int, Specification a) -> Specification a
chooseSpec
          (Int
1, Specification Natural
forall a. Specification a
trueSpec)
          (Int
1, (TermD Deps Natural -> Term Bool) -> Specification Natural
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained (TermD Deps Natural -> TermD Deps Natural -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. TermD Deps Natural
committeeSize))
      where
        committeeSize :: TermD Deps Natural
committeeSize = Natural -> TermD Deps Natural
forall a. HasSpec a => a -> Term a
lit (Natural -> TermD Deps Natural)
-> (Set (Credential ColdCommitteeRole) -> Natural)
-> Set (Credential ColdCommitteeRole)
-> TermD Deps Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural)
-> (Set (Credential ColdCommitteeRole) -> Int)
-> Set (Credential ColdCommitteeRole)
-> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Credential ColdCommitteeRole) -> Int
forall a. Set a -> Int
Set.size (Set (Credential ColdCommitteeRole) -> TermD Deps Natural)
-> Set (Credential ColdCommitteeRole) -> TermD Deps Natural
forall a b. (a -> b) -> a -> b
$ Set (Credential ColdCommitteeRole)
ccColdKeys

ratifySignalSpec ::
  [GovActionState ConwayEra] ->
  Specification (RatifySignal ConwayEra)
ratifySignalSpec :: [GovActionState ConwayEra]
-> Specification (RatifySignal ConwayEra)
ratifySignalSpec [GovActionState ConwayEra]
govActions =
  (Term (RatifySignal ConwayEra) -> Pred)
-> Specification (RatifySignal ConwayEra)
forall a p.
(IsPred p, HasSpec a) =>
(Term a -> p) -> Specification a
constrained ((Term (RatifySignal ConwayEra) -> Pred)
 -> Specification (RatifySignal ConwayEra))
-> (Term (RatifySignal ConwayEra) -> Pred)
-> Specification (RatifySignal ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (RatifySignal ConwayEra)
sig ->
    Term (RatifySignal ConwayEra)
-> FunTy
     (MapList Term (ProductAsList (RatifySignal ConwayEra))) Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (RatifySignal ConwayEra)
sig (FunTy (MapList Term (ProductAsList (RatifySignal ConwayEra))) Pred
 -> Pred)
-> FunTy
     (MapList Term (ProductAsList (RatifySignal ConwayEra))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term (StrictSeq (GovActionState ConwayEra))
gasS ->
      Term (StrictSeq (GovActionState ConwayEra))
-> FunTy
     (MapList
        Term (ProductAsList (StrictSeq (GovActionState ConwayEra))))
     Pred
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term (StrictSeq (GovActionState ConwayEra))
gasS (FunTy
   (MapList
      Term (ProductAsList (StrictSeq (GovActionState ConwayEra))))
   Pred
 -> Pred)
-> FunTy
     (MapList
        Term (ProductAsList (StrictSeq (GovActionState ConwayEra))))
     Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term [GovActionState ConwayEra]
gasL ->
        Term [GovActionState ConwayEra]
-> (Term (GovActionState ConwayEra) -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll Term [GovActionState ConwayEra]
gasL ((Term (GovActionState ConwayEra) -> Term Bool) -> Pred)
-> (Term (GovActionState ConwayEra) -> Term Bool) -> Pred
forall a b. (a -> b) -> a -> b
$ \Term (GovActionState ConwayEra)
gas ->
          Term (GovActionState ConwayEra)
gas Term (GovActionState ConwayEra)
-> Term [GovActionState ConwayEra] -> Term Bool
forall a. HasSpec a => Term a -> Term [a] -> Term Bool
`elem_` [GovActionState ConwayEra] -> Term [GovActionState ConwayEra]
forall a. HasSpec a => a -> Term a
lit [GovActionState ConwayEra]
govActions

enactSignalSpec ::
  EpochNo ->
  EnactState ConwayEra ->
  Specification (EnactSignal ConwayEra)
enactSignalSpec :: EpochNo
-> EnactState ConwayEra -> Specification (EnactSignal ConwayEra)
enactSignalSpec EpochNo
epoch EnactState {Map (Credential Staking) Coin
StrictMaybe (Committee ConwayEra)
PParams ConwayEra
Constitution ConwayEra
GovRelation StrictMaybe
Coin
ensCommittee :: StrictMaybe (Committee ConwayEra)
ensConstitution :: Constitution ConwayEra
ensCurPParams :: PParams ConwayEra
ensPrevPParams :: PParams ConwayEra
ensTreasury :: Coin
ensWithdrawals :: Map (Credential Staking) Coin
ensPrevGovActionIds :: GovRelation StrictMaybe
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe
ensWithdrawals :: forall era. EnactState era -> Map (Credential Staking) Coin
ensTreasury :: forall era. EnactState era -> Coin
ensPrevPParams :: forall era. EnactState era -> PParams era
ensCurPParams :: forall era. EnactState era -> PParams era
ensConstitution :: forall era. EnactState era -> Constitution era
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
..} =
  FunTy
  (MapList Term (Args (SimpleRep (EnactSignal ConwayEra)))) [Pred]
-> Specification (EnactSignal ConwayEra)
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (EnactSignal ConwayEra)))) [Pred]
 -> Specification (EnactSignal ConwayEra))
-> FunTy
     (MapList Term (Args (SimpleRep (EnactSignal ConwayEra)))) [Pred]
-> Specification (EnactSignal ConwayEra)
forall a b. (a -> b) -> a -> b
$ \TermD Deps GovActionId
_gid Term (GovAction ConwayEra)
action ->
    [ -- TODO get rid of this by modifying the spec so that ENACT can't fail.
      -- Right now this constraint makes the generator avoid cases where
      -- the spec would fail, because such proposals would be handled in RATIFY
      -- and wouldn't make it to ENACT.
      (Term (GovAction ConwayEra)
-> FunTy
     (MapList
        (Weighted (BinderD Deps))
        (Cases (SimpleRep (GovAction ConwayEra))))
     Pred
forall a.
(GenericRequires a, SimpleRep a ~ SumOver (Cases (SimpleRep a)),
 TypeList (Cases (SimpleRep a))) =>
Term a
-> FunTy
     (MapList (Weighted (BinderD Deps)) (Cases (SimpleRep a))) Pred
caseOn Term (GovAction ConwayEra)
action)
        (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
           (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
            (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
         (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
              (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
        (Prod (PParamsUpdate ConwayEra) (StrictMaybe ScriptHash)))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'PParamUpdatePurpose))
_ TermD Deps (PParamsUpdate ConwayEra)
_ TermD Deps (StrictMaybe ScriptHash)
_ -> Bool
True)
        (FunTy
  (MapList
     Term
     (Args
        (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer)))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer)
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer)))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer))
-> FunTy
     (MapList
        Term
        (Args
           (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer)))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod (StrictMaybe (GovPurposeId 'HardForkPurpose)) ProtVer)
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'HardForkPurpose))
_ Term ProtVer
_ -> Bool
True)
        ( FunTy
  (MapList
     Term
     (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
  [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
   [Pred]
 -> Weighted
      (BinderD Deps)
      (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash)))
-> FunTy
     (MapList
        Term
        (Args (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))))
     [Pred]
-> Weighted
     (BinderD Deps)
     (Prod (Map RewardAccount Coin) (StrictMaybe ScriptHash))
forall a b. (a -> b) -> a -> b
$ \Term (Map RewardAccount Coin)
newWdrls TermD Deps (StrictMaybe ScriptHash)
_ ->
            [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [Coin] -> Term Coin
forall a. Foldy a => Term [a] -> Term a
sum_ (Term (Map RewardAccount Coin) -> Term [Coin]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map RewardAccount Coin)
newWdrls) Term Coin -> Term Coin -> Term Coin
forall a. Num a => a -> a -> a
+ Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit (Map (Credential Staking) Coin -> Coin
forall a. Num a => Map (Credential Staking) a -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum Map (Credential Staking) Coin
ensWithdrawals) Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Coin -> Term Coin
forall a. HasSpec a => a -> Term a
lit Coin
ensTreasury
            , Pred -> Pred
forall p. IsPred p => p -> Pred
assert (Pred -> Pred) -> Pred -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map RewardAccount Coin)
-> FunTy
     (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Map RewardAccount Coin)
newWdrls (FunTy (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
 -> Pred)
-> FunTy
     (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term RewardAccount
acct Term Coin
_ ->
                Term RewardAccount
-> FunTy (MapList Term (ProductAsList RewardAccount)) (Term Bool)
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
acct (FunTy (MapList Term (ProductAsList RewardAccount)) (Term Bool)
 -> Pred)
-> FunTy (MapList Term (ProductAsList RewardAccount)) (Term Bool)
-> Pred
forall a b. (a -> b) -> a -> b
$ \Term Network
network TermD Deps (Credential Staking)
_ ->
                  Term Network
network Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit Network
Testnet
            ]
        )
        (FunTy
  (MapList
     Term (Args (StrictMaybe (GovPurposeId 'CommitteePurpose))))
  Bool
-> Weighted
     (BinderD Deps) (StrictMaybe (GovPurposeId 'CommitteePurpose))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term (Args (StrictMaybe (GovPurposeId 'CommitteePurpose))))
   Bool
 -> Weighted
      (BinderD Deps) (StrictMaybe (GovPurposeId 'CommitteePurpose)))
-> FunTy
     (MapList
        Term (Args (StrictMaybe (GovPurposeId 'CommitteePurpose))))
     Bool
-> Weighted
     (BinderD Deps) (StrictMaybe (GovPurposeId 'CommitteePurpose))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose))
_ -> Bool
True)
        ( FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'CommitteePurpose))
           (Prod
              (Set (Credential ColdCommitteeRole))
              (Prod
                 (Map (Credential ColdCommitteeRole) EpochNo) UnitInterval)))))
  Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose))
        (Prod
           (Set (Credential ColdCommitteeRole))
           (Prod (Map (Credential ColdCommitteeRole) EpochNo) UnitInterval)))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (StrictMaybe (GovPurposeId 'CommitteePurpose))
            (Prod
               (Set (Credential ColdCommitteeRole))
               (Prod
                  (Map (Credential ColdCommitteeRole) EpochNo) UnitInterval)))))
   Pred
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'CommitteePurpose))
         (Prod
            (Set (Credential ColdCommitteeRole))
            (Prod (Map (Credential ColdCommitteeRole) EpochNo) UnitInterval))))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'CommitteePurpose))
              (Prod
                 (Set (Credential ColdCommitteeRole))
                 (Prod
                    (Map (Credential ColdCommitteeRole) EpochNo) UnitInterval)))))
     Pred
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'CommitteePurpose))
        (Prod
           (Set (Credential ColdCommitteeRole))
           (Prod (Map (Credential ColdCommitteeRole) EpochNo) UnitInterval)))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'CommitteePurpose))
_ Term (Set (Credential ColdCommitteeRole))
_ Term (Map (Credential ColdCommitteeRole) EpochNo)
newMembers TermD Deps UnitInterval
_ ->
            let expiry :: EpochNo
expiry = EpochNo -> EpochInterval -> EpochNo
addEpochInterval EpochNo
epoch (PParams ConwayEra
ensCurPParams PParams ConwayEra
-> Getting EpochInterval (PParams ConwayEra) EpochInterval
-> EpochInterval
forall s a. s -> Getting a s a -> a
^. Getting EpochInterval (PParams ConwayEra) EpochInterval
forall era.
ConwayEraPParams era =>
Lens' (PParams era) EpochInterval
Lens' (PParams ConwayEra) EpochInterval
ppCommitteeMaxTermLengthL)
             in Term [EpochNo] -> (TermD Deps EpochNo -> Term Bool) -> Pred
forall p t a.
(Forallable t a, HasSpec t, HasSpec a, IsPred p) =>
Term t -> (Term a -> p) -> Pred
forAll (Term (Map (Credential ColdCommitteeRole) EpochNo) -> Term [EpochNo]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ Term (Map (Credential ColdCommitteeRole) EpochNo)
newMembers) (TermD Deps EpochNo -> TermD Deps EpochNo -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. EpochNo -> TermD Deps EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
expiry)
        )
        (FunTy
  (MapList
     Term
     (Args
        (Prod
           (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
           (Constitution ConwayEra))))
  Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
        (Constitution ConwayEra))
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy
   (MapList
      Term
      (Args
         (Prod
            (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
            (Constitution ConwayEra))))
   Bool
 -> Weighted
      (BinderD Deps)
      (Prod
         (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
         (Constitution ConwayEra)))
-> FunTy
     (MapList
        Term
        (Args
           (Prod
              (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
              (Constitution ConwayEra))))
     Bool
-> Weighted
     (BinderD Deps)
     (Prod
        (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
        (Constitution ConwayEra))
forall a b. (a -> b) -> a -> b
$ \TermD Deps (StrictMaybe (GovPurposeId 'ConstitutionPurpose))
_ TermD Deps (Constitution ConwayEra)
_ -> Bool
True)
        (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ()
forall p a.
(HasSpec a, All HasSpec (Args a), IsPred p, IsProd a) =>
FunTy (MapList Term (Args a)) p -> Weighted (BinderD Deps) a
branch (FunTy (MapList Term (Args ())) Bool -> Weighted (BinderD Deps) ())
-> FunTy (MapList Term (Args ())) Bool
-> Weighted (BinderD Deps) ()
forall a b. (a -> b) -> a -> b
$ \TermD Deps ()
_ -> Bool
True)
    ]

enactStateSpec ::
  Specification (EnactState ConwayEra)
enactStateSpec :: Specification (EnactState ConwayEra)
enactStateSpec =
  FunTy
  (MapList Term (Args (SimpleRep (EnactState ConwayEra)))) [Pred]
-> Specification (EnactState ConwayEra)
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (EnactState ConwayEra)))) [Pred]
 -> Specification (EnactState ConwayEra))
-> FunTy
     (MapList Term (Args (SimpleRep (EnactState ConwayEra)))) [Pred]
-> Specification (EnactState ConwayEra)
forall a b. (a -> b) -> a -> b
$ \Term (StrictMaybe (Committee ConwayEra))
_ TermD Deps (Constitution ConwayEra)
_ Term (PParams ConwayEra)
_ Term (PParams ConwayEra)
_ Term Coin
treasury TermD Deps (Map (Credential Staking) Coin)
wdrls TermD Deps (GovRelation StrictMaybe)
_ ->
    [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term [Coin] -> Term Coin
forall a. Foldy a => Term [a] -> Term a
sum_ (TermD Deps (Map (Credential Staking) Coin) -> Term [Coin]
forall k v.
(HasSpec k, HasSpec v, Ord k, IsNormalType k, IsNormalType v) =>
Term (Map k v) -> Term [v]
rng_ TermD Deps (Map (Credential Staking) Coin)
wdrls) Term Coin -> Term Coin -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Term Coin
treasury
    ]

namePoolCert :: PoolCert -> String
namePoolCert :: PoolCert -> [Char]
namePoolCert RegPool {} = [Char]
"RegPool"
namePoolCert RetirePool {} = [Char]
"RetirePool"

nameDelegCert :: ConwayDelegCert -> String
nameDelegCert :: ConwayDelegCert -> [Char]
nameDelegCert ConwayRegCert {} = [Char]
"RegKey"
nameDelegCert ConwayUnRegCert {} = [Char]
"UnRegKey"
nameDelegCert ConwayDelegCert {} = [Char]
"DelegateWithKey"
nameDelegCert ConwayRegDelegCert {} = [Char]
"RegK&DelegateWithKey"

nameGovCert :: ConwayGovCert -> String
nameGovCert :: ConwayGovCert -> [Char]
nameGovCert (ConwayRegDRep {}) = [Char]
"ConwayRegDRep"
nameGovCert (ConwayUnRegDRep {}) = [Char]
"ConwayUnRegDRep"
nameGovCert (ConwayUpdateDRep {}) = [Char]
"ConwayUpdateDRep"
nameGovCert (ConwayAuthCommitteeHotKey {}) = [Char]
"ConwayAuthCommitteeHotKey"
nameGovCert (ConwayResignCommitteeColdKey {}) = [Char]
"ConwayResignCommitteeColdKey"

nameTxCert :: ConwayTxCert ConwayEra -> String
nameTxCert :: ConwayTxCert ConwayEra -> [Char]
nameTxCert (ConwayTxCertDeleg ConwayDelegCert
x) = ConwayDelegCert -> [Char]
nameDelegCert ConwayDelegCert
x
nameTxCert (ConwayTxCertPool PoolCert
x) = PoolCert -> [Char]
namePoolCert PoolCert
x
nameTxCert (ConwayTxCertGov ConwayGovCert
x) = ConwayGovCert -> [Char]
nameGovCert ConwayGovCert
x

nameCerts :: Seq (ConwayTxCert ConwayEra) -> String
nameCerts :: Seq (ConwayTxCert ConwayEra) -> [Char]
nameCerts Seq (ConwayTxCert ConwayEra)
x = [Char]
"Certs length " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Seq (ConwayTxCert ConwayEra) -> Int
forall a. Seq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length Seq (ConwayTxCert ConwayEra)
x)

-- | Run a minitrace for every instance of ExecRuleSpec
spec :: Spec
spec :: Spec
spec = do
  [Char] -> Spec -> Spec
forall a. HasCallStack => [Char] -> SpecWith a -> SpecWith a
describe [Char]
"50 MiniTrace tests with trace length of 50" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
    ConstrainedGeneratorBundle (WitUniv ConwayEra) "POOL" ConwayEra
-> (Signal (EraRule "POOL" ConwayEra) -> [Char]) -> Spec
forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle (WitUniv ConwayEra) "POOL" ConwayEra
constrainedPool PoolCert -> [Char]
Signal (EraRule "POOL" ConwayEra) -> [Char]
namePoolCert
    ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "DELEG"
  ConwayEra
-> (Signal (EraRule "DELEG" ConwayEra) -> [Char]) -> Spec
forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "DELEG"
  ConwayEra
constrainedDeleg ConwayDelegCert -> [Char]
Signal (EraRule "DELEG" ConwayEra) -> [Char]
nameDelegCert
    ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "GOVCERT"
  ConwayEra
-> (Signal (EraRule "GOVCERT" ConwayEra) -> [Char]) -> Spec
forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "GOVCERT"
  ConwayEra
constrainedGovCert ConwayGovCert -> [Char]
Signal (EraRule "GOVCERT" ConwayEra) -> [Char]
nameGovCert
    ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "CERT"
  ConwayEra
-> (Signal (EraRule "CERT" ConwayEra) -> [Char]) -> Spec
forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "CERT"
  ConwayEra
constrainedCert ConwayTxCert ConwayEra -> [Char]
Signal (EraRule "CERT" ConwayEra) -> [Char]
nameTxCert
    ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "CERTS"
  ConwayEra
-> (Signal (EraRule "CERTS" ConwayEra) -> [Char]) -> Spec
forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "CERTS"
  ConwayEra
constrainedCerts Seq (ConwayTxCert ConwayEra) -> [Char]
Signal (EraRule "CERTS" ConwayEra) -> [Char]
nameCerts
    ConstrainedGeneratorBundle
  [GovActionState ConwayEra] "RATIFY" ConwayEra
-> (Signal (EraRule "RATIFY" ConwayEra) -> [Char]) -> Spec
forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle
  [GovActionState ConwayEra] "RATIFY" ConwayEra
constrainedRatify ([Char] -> RatifySignal ConwayEra -> [Char]
forall a b. a -> b -> a
const [Char]
"")

    -- These properties do not have working 'signalSpec' Specifications yet.
    [Char] -> Spec -> Spec
forall a. HasCallStack => [Char] -> SpecWith a -> SpecWith a
xdescribe [Char]
"Pending tests" (Spec -> Spec) -> Spec -> Spec
forall a b. (a -> b) -> a -> b
$ do
      ConstrainedGeneratorBundle () "GOV" ConwayEra
-> (Signal (EraRule "GOV" ConwayEra) -> [Char]) -> Spec
forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle () "GOV" ConwayEra
constrainedGov ([Char] -> GovSignal ConwayEra -> [Char]
forall a b. a -> b -> a
const [Char]
"")
      ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
-> (Signal (EraRule "UTXO" ConwayEra) -> [Char]) -> Spec
forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
constrainedUtxo ([Char] -> Tx TopTx ConwayEra -> [Char]
forall a b. a -> b -> a
const [Char]
"")
      ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra
-> (Signal (EraRule "EPOCH" ConwayEra) -> [Char]) -> Spec
forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra
constrainedEpoch ([Char] -> EpochNo -> [Char]
forall a b. a -> b -> a
const [Char]
"")
      ConstrainedGeneratorBundle EpochNo "NEWEPOCH" ConwayEra
-> (Signal (EraRule "NEWEPOCH" ConwayEra) -> [Char]) -> Spec
forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace ConstrainedGeneratorBundle EpochNo "NEWEPOCH" ConwayEra
constrainedNewEpoch ([Char] -> EpochNo -> [Char]
forall a b. a -> b -> a
const [Char]
"")
      forall (rule :: Symbol) era ctx.
(HasSpec (Environment (EraRule rule era)),
 HasSpec (State (EraRule rule era)),
 HasSpec (Signal (EraRule rule era)),
 BaseM (EraRule rule era) ~ ShelleyBase, KnownSymbol rule,
 STS (EraRule rule era), ToExpr (Signal (EraRule rule era)),
 ToExpr (State (EraRule rule era))) =>
ConstrainedGeneratorBundle ctx rule era
-> (Signal (EraRule rule era) -> [Char]) -> Spec
runMinitrace @"ENACT" @ConwayEra
        ConstrainedGeneratorBundle EpochNo "ENACT" ConwayEra
constrainedEnact
        ([Char] -> EnactSignal ConwayEra -> [Char]
forall a b. a -> b -> a
const [Char]
"")

data ConwayCertGenContext era = ConwayCertGenContext
  { forall era. ConwayCertGenContext era -> Map RewardAccount Coin
ccccWithdrawals :: !(Map RewardAccount Coin)
  , forall era. ConwayCertGenContext era -> VotingProcedures era
ccccVotes :: !(VotingProcedures era)
  , forall era.
ConwayCertGenContext era
-> Map (Credential DRepRole) (Set (Credential Staking))
ccccDelegatees :: !(Map (Credential DRepRole) (Set (Credential Staking)))
  }
  deriving ((forall x.
 ConwayCertGenContext era -> Rep (ConwayCertGenContext era) x)
-> (forall x.
    Rep (ConwayCertGenContext era) x -> ConwayCertGenContext era)
-> Generic (ConwayCertGenContext era)
forall x.
Rep (ConwayCertGenContext era) x -> ConwayCertGenContext era
forall x.
ConwayCertGenContext era -> Rep (ConwayCertGenContext era) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall era x.
Rep (ConwayCertGenContext era) x -> ConwayCertGenContext era
forall era x.
ConwayCertGenContext era -> Rep (ConwayCertGenContext era) x
$cfrom :: forall era x.
ConwayCertGenContext era -> Rep (ConwayCertGenContext era) x
from :: forall x.
ConwayCertGenContext era -> Rep (ConwayCertGenContext era) x
$cto :: forall era x.
Rep (ConwayCertGenContext era) x -> ConwayCertGenContext era
to :: forall x.
Rep (ConwayCertGenContext era) x -> ConwayCertGenContext era
Generic, ConwayCertGenContext era -> ConwayCertGenContext era -> Bool
(ConwayCertGenContext era -> ConwayCertGenContext era -> Bool)
-> (ConwayCertGenContext era -> ConwayCertGenContext era -> Bool)
-> Eq (ConwayCertGenContext era)
forall era.
ConwayCertGenContext era -> ConwayCertGenContext era -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall era.
ConwayCertGenContext era -> ConwayCertGenContext era -> Bool
== :: ConwayCertGenContext era -> ConwayCertGenContext era -> Bool
$c/= :: forall era.
ConwayCertGenContext era -> ConwayCertGenContext era -> Bool
/= :: ConwayCertGenContext era -> ConwayCertGenContext era -> Bool
Eq, Int -> ConwayCertGenContext era -> [Char] -> [Char]
[ConwayCertGenContext era] -> [Char] -> [Char]
ConwayCertGenContext era -> [Char]
(Int -> ConwayCertGenContext era -> [Char] -> [Char])
-> (ConwayCertGenContext era -> [Char])
-> ([ConwayCertGenContext era] -> [Char] -> [Char])
-> Show (ConwayCertGenContext era)
forall era. Int -> ConwayCertGenContext era -> [Char] -> [Char]
forall era. [ConwayCertGenContext era] -> [Char] -> [Char]
forall era. ConwayCertGenContext era -> [Char]
forall a.
(Int -> a -> [Char] -> [Char])
-> (a -> [Char]) -> ([a] -> [Char] -> [Char]) -> Show a
$cshowsPrec :: forall era. Int -> ConwayCertGenContext era -> [Char] -> [Char]
showsPrec :: Int -> ConwayCertGenContext era -> [Char] -> [Char]
$cshow :: forall era. ConwayCertGenContext era -> [Char]
show :: ConwayCertGenContext era -> [Char]
$cshowList :: forall era. [ConwayCertGenContext era] -> [Char] -> [Char]
showList :: [ConwayCertGenContext era] -> [Char] -> [Char]
Show)

instance Era era => HasSimpleRep (ConwayCertGenContext era)

instance Era era => HasSpec (ConwayCertGenContext era)

-- | A Specification version of `Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.Specs.genCertContext`
--   Makes sure all the subtle invariants of `type WhoDelegates` are met.
conwayCertExecContextSpec ::
  forall era. Era era => WitUniv era -> Integer -> Specification (ConwayCertGenContext era)
conwayCertExecContextSpec :: forall era.
Era era =>
WitUniv era -> Integer -> Specification (ConwayCertGenContext era)
conwayCertExecContextSpec WitUniv era
univ Integer
wdrlsize = FunTy
  (MapList Term (Args (SimpleRep (ConwayCertGenContext era)))) [Pred]
-> Specification (ConwayCertGenContext era)
forall a p.
(Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec (SimpleRep a),
 HasSimpleRep a, All HasSpec (Args (SimpleRep a)),
 IsProd (SimpleRep a), HasSpec a, IsProductType a, IsPred p,
 GenericRequires a, ProdAsListComputes a) =>
FunTy (MapList Term (Args (SimpleRep a))) p -> Specification a
constrained' (FunTy
   (MapList Term (Args (SimpleRep (ConwayCertGenContext era)))) [Pred]
 -> Specification (ConwayCertGenContext era))
-> FunTy
     (MapList Term (Args (SimpleRep (ConwayCertGenContext era)))) [Pred]
-> Specification (ConwayCertGenContext era)
forall a b. (a -> b) -> a -> b
$
  \ Term (Map RewardAccount Coin)
[var|withdrawals|] TermD Deps (VotingProcedures era)
_voteProcs Term (Map (Credential DRepRole) (Set (Credential Staking)))
[var|delegatees|] ->
    [ Term (Map RewardAccount Coin)
withdrawals Term (Map RewardAccount Coin)
-> Term (Map (Credential DRepRole) (Set (Credential Staking)))
-> Pred
forall a b. (HasSpec a, HasSpec b) => Term a -> Term b -> Pred
`dependsOn` Term (Map (Credential DRepRole) (Set (Credential Staking)))
delegatees
    , Term (Map (Credential DRepRole) (Set (Credential Staking)))
-> Specification
     (Map (Credential DRepRole) (Set (Credential Staking)))
-> Pred
forall a. HasSpec a => Term a -> Specification a -> Pred
satisfies Term (Map (Credential DRepRole) (Set (Credential Staking)))
delegatees (WitUniv era
-> Specification
     (Map (Credential DRepRole) (Set (Credential Staking)))
forall era.
Era era =>
WitUniv era
-> Specification
     (Map (Credential DRepRole) (Set (Credential Staking)))
whoDelegatesSpec WitUniv era
univ)
    , [Pred] -> Pred
forall p. IsPred p => p -> Pred
assert
        [ Term Bool -> Pred
forall p. IsPred p => p -> Pred
assert (Term Bool -> Pred) -> Term Bool -> Pred
forall a b. (a -> b) -> a -> b
$ Term (Map RewardAccount Coin) -> Term Integer
forall a. (HasSpec a, Sized a) => Term a -> Term Integer
sizeOf_ Term (Map RewardAccount Coin)
withdrawals Term Integer -> Term Integer -> Term Bool
forall a. OrdLike a => Term a -> Term a -> Term Bool
<=. Integer -> Term Integer
forall a. HasSpec a => a -> Term a
lit Integer
wdrlsize
        , Term (Map (Credential DRepRole) (Set (Credential Staking)))
-> (Map (Credential DRepRole) (Set (Credential Staking))
    -> Set (Credential Staking))
-> (Term (Set (Credential Staking)) -> [Pred])
-> Pred
forall a b p.
(HasSpec a, HasSpec b, IsPred p) =>
Term a -> (a -> b) -> (Term b -> p) -> Pred
reify Term (Map (Credential DRepRole) (Set (Credential Staking)))
delegatees Map (Credential DRepRole) (Set (Credential Staking))
-> Set (Credential Staking)
delegators ((Term (Set (Credential Staking)) -> [Pred]) -> Pred)
-> (Term (Set (Credential Staking)) -> [Pred]) -> Pred
forall a b. (a -> b) -> a -> b
$ \ Term (Set (Credential Staking))
[var|credStakeSet|] ->
            [ Term (Map RewardAccount Coin)
-> FunTy
     (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
-> Pred
forall t a p.
(Forallable t a, Cases (SimpleRep a) ~ '[SimpleRep a],
 TypeSpec a ~ TypeSpec (SimpleRep a), HasSpec t,
 HasSpec (SimpleRep a), HasSimpleRep a,
 All HasSpec (Args (SimpleRep a)), IsPred p, IsProd (SimpleRep a),
 IsProductType a, HasSpec a, GenericRequires a,
 ProdAsListComputes a) =>
Term t -> FunTy (MapList Term (Args (SimpleRep a))) p -> Pred
forAll' Term (Map RewardAccount Coin)
withdrawals (FunTy (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
 -> Pred)
-> FunTy
     (MapList Term (Args (SimpleRep (RewardAccount, Coin)))) Pred
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term RewardAccount
[var|rewAccount|] Term Coin
[var|_wCoin|] ->
                Term RewardAccount
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Term Bool]
-> Pred
forall p a.
(IsProductType a, IsPred p, GenericRequires a,
 ProdAsListComputes a) =>
Term a -> FunTy (MapList Term (ProductAsList a)) p -> Pred
match Term RewardAccount
rewAccount (FunTy (MapList Term (ProductAsList RewardAccount)) [Term Bool]
 -> Pred)
-> FunTy (MapList Term (ProductAsList RewardAccount)) [Term Bool]
-> Pred
forall a b. (a -> b) -> a -> b
$ \ Term Network
[var|network|] TermD Deps (Credential Staking)
[var|rewcred|] ->
                  [Term Network
network Term Network -> Term Network -> Term Bool
forall a. HasSpec a => Term a -> Term a -> Term Bool
==. Network -> Term Network
forall a. HasSpec a => a -> Term a
lit Network
Testnet, TermD Deps (Credential Staking)
-> Term (Set (Credential Staking)) -> Term Bool
forall a. (Ord a, HasSpec a) => Term a -> Term (Set a) -> Term Bool
member_ TermD Deps (Credential Staking)
rewcred Term (Set (Credential Staking))
credStakeSet]
            ]
        ]
    ]

-- Constrained generator bundles for each rule

constrainedPool :: ConstrainedGeneratorBundle (WitUniv ConwayEra) "POOL" ConwayEra
constrainedPool :: ConstrainedGeneratorBundle (WitUniv ConwayEra) "POOL" ConwayEra
constrainedPool =
  Gen (WitUniv ConwayEra)
-> (WitUniv ConwayEra
    -> Specification (Environment (EraRule "POOL" ConwayEra)))
-> (WitUniv ConwayEra
    -> Environment (EraRule "POOL" ConwayEra)
    -> Specification (State (EraRule "POOL" ConwayEra)))
-> (WitUniv ConwayEra
    -> Environment (EraRule "POOL" ConwayEra)
    -> State (EraRule "POOL" ConwayEra)
    -> Specification (Signal (EraRule "POOL" ConwayEra)))
-> ConstrainedGeneratorBundle (WitUniv ConwayEra) "POOL" ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    (Int -> Gen (WitUniv ConwayEra)
forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
50)
    WitUniv ConwayEra -> Specification (PoolEnv ConwayEra)
WitUniv ConwayEra
-> Specification (Environment (EraRule "POOL" ConwayEra))
forall era.
EraSpecPParams era =>
WitUniv era -> Specification (PoolEnv era)
poolEnvSpec
    (\WitUniv ConwayEra
ctx Environment (EraRule "POOL" ConwayEra)
_ -> WitUniv ConwayEra -> Specification (PState ConwayEra)
forall era. Era era => WitUniv era -> Specification (PState era)
pStateSpec WitUniv ConwayEra
ctx)
    WitUniv ConwayEra
-> PoolEnv ConwayEra -> PState ConwayEra -> Specification PoolCert
WitUniv ConwayEra
-> Environment (EraRule "POOL" ConwayEra)
-> State (EraRule "POOL" ConwayEra)
-> Specification (Signal (EraRule "POOL" ConwayEra))
forall era.
EraSpecPParams era =>
WitUniv era -> PoolEnv era -> PState era -> Specification PoolCert
poolCertSpec

constrainedDeleg ::
  ConstrainedGeneratorBundle
    (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    "DELEG"
    ConwayEra
constrainedDeleg :: ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "DELEG"
  ConwayEra
constrainedDeleg =
  Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Specification (Environment (EraRule "DELEG" ConwayEra)))
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "DELEG" ConwayEra)
    -> Specification (State (EraRule "DELEG" ConwayEra)))
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "DELEG" ConwayEra)
    -> State (EraRule "DELEG" ConwayEra)
    -> Specification (Signal (EraRule "DELEG" ConwayEra)))
-> ConstrainedGeneratorBundle
     (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
     "DELEG"
     ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
genDelegCtx
    (Specification (ConwayDelegEnv ConwayEra)
-> (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> Specification (ConwayDelegEnv ConwayEra)
forall a b. a -> b -> a
const Specification (ConwayDelegEnv ConwayEra)
forall era.
EraSpecPParams era =>
Specification (ConwayDelegEnv era)
delegEnvSpec)
    (\(WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
ctx Environment (EraRule "DELEG" ConwayEra)
_ -> (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> Specification (CertState ConwayEra)
forall era.
EraSpecCert era =>
(WitUniv era, ConwayCertGenContext era)
-> Specification (CertState era)
certStateSpec_ (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
ctx)
    ((ConwayDelegEnv ConwayEra
 -> ConwayCertState ConwayEra -> Specification ConwayDelegCert)
-> (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> ConwayDelegEnv ConwayEra
-> ConwayCertState ConwayEra
-> Specification ConwayDelegCert
forall a b. a -> b -> a
const ConwayDelegEnv ConwayEra
-> CertState ConwayEra -> Specification ConwayDelegCert
ConwayDelegEnv ConwayEra
-> ConwayCertState ConwayEra -> Specification ConwayDelegCert
forall era.
(EraPParams era, ConwayEraCertState era) =>
ConwayDelegEnv era
-> CertState era -> Specification ConwayDelegCert
conwayDelegCertSpec)

constrainedGovCert ::
  ConstrainedGeneratorBundle
    (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    "GOVCERT"
    ConwayEra
constrainedGovCert :: ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "GOVCERT"
  ConwayEra
constrainedGovCert =
  Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Specification (Environment (EraRule "GOVCERT" ConwayEra)))
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "GOVCERT" ConwayEra)
    -> Specification (State (EraRule "GOVCERT" ConwayEra)))
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "GOVCERT" ConwayEra)
    -> State (EraRule "GOVCERT" ConwayEra)
    -> Specification (Signal (EraRule "GOVCERT" ConwayEra)))
-> ConstrainedGeneratorBundle
     (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
     "GOVCERT"
     ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
genDelegCtx
    (\(WitUniv ConwayEra
u, ConwayCertGenContext ConwayEra
_) -> WitUniv ConwayEra -> Specification (ConwayGovCertEnv ConwayEra)
govCertEnvSpec WitUniv ConwayEra
u)
    (\(WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
ctx Environment (EraRule "GOVCERT" ConwayEra)
_ -> (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> Specification (CertState ConwayEra)
forall era.
EraSpecCert era =>
(WitUniv era, ConwayCertGenContext era)
-> Specification (CertState era)
certStateSpec_ (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
ctx)
    (\(WitUniv ConwayEra
u, ConwayCertGenContext ConwayEra
_) -> WitUniv ConwayEra
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
forall era.
EraCertState era =>
WitUniv era
-> ConwayGovCertEnv ConwayEra
-> CertState ConwayEra
-> Specification ConwayGovCert
govCertSpec WitUniv ConwayEra
u)

constrainedCert ::
  ConstrainedGeneratorBundle
    (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    "CERT"
    ConwayEra
constrainedCert :: ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "CERT"
  ConwayEra
constrainedCert =
  Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Specification (Environment (EraRule "CERT" ConwayEra)))
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "CERT" ConwayEra)
    -> Specification (State (EraRule "CERT" ConwayEra)))
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "CERT" ConwayEra)
    -> State (EraRule "CERT" ConwayEra)
    -> Specification (Signal (EraRule "CERT" ConwayEra)))
-> ConstrainedGeneratorBundle
     (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
     "CERT"
     ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
genDelegCtx
    (\(WitUniv ConwayEra
u, ConwayCertGenContext ConwayEra
_) -> WitUniv ConwayEra -> Specification (CertEnv ConwayEra)
forall era.
EraSpecPParams era =>
WitUniv era -> Specification (CertEnv era)
certEnvSpec WitUniv ConwayEra
u)
    (\(WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
ctx Environment (EraRule "CERT" ConwayEra)
_ -> (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> Specification (CertState ConwayEra)
forall era.
EraSpecCert era =>
(WitUniv era, ConwayCertGenContext era)
-> Specification (CertState era)
certStateSpec_ (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
ctx)
    (\(WitUniv ConwayEra
u, ConwayCertGenContext ConwayEra
_) -> WitUniv ConwayEra
-> CertEnv ConwayEra
-> CertState ConwayEra
-> Specification (ConwayTxCert ConwayEra)
forall era.
(era ~ ConwayEra) =>
WitUniv era
-> CertEnv era -> CertState era -> Specification (ConwayTxCert era)
conwayTxCertSpec WitUniv ConwayEra
u)

constrainedCerts ::
  ConstrainedGeneratorBundle
    (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    "CERTS"
    ConwayEra
constrainedCerts :: ConstrainedGeneratorBundle
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
  "CERTS"
  ConwayEra
constrainedCerts =
  Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Specification (Environment (EraRule "CERTS" ConwayEra)))
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "CERTS" ConwayEra)
    -> Specification (State (EraRule "CERTS" ConwayEra)))
-> ((WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
    -> Environment (EraRule "CERTS" ConwayEra)
    -> State (EraRule "CERTS" ConwayEra)
    -> Specification (Signal (EraRule "CERTS" ConwayEra)))
-> ConstrainedGeneratorBundle
     (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
     "CERTS"
     ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
genDelegCtx
    (Specification (CertsEnv ConwayEra)
-> (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> Specification (CertsEnv ConwayEra)
forall a b. a -> b -> a
const Specification (CertsEnv ConwayEra)
forall era.
(EraSpecPParams era, HasSpec (Tx TopTx era)) =>
Specification (CertsEnv era)
certsEnvSpec)
    ( \(WitUniv ConwayEra
u, ConwayCertGenContext {Map RewardAccount Coin
Map (Credential DRepRole) (Set (Credential Staking))
VotingProcedures ConwayEra
ccccDelegatees :: forall era.
ConwayCertGenContext era
-> Map (Credential DRepRole) (Set (Credential Staking))
ccccVotes :: forall era. ConwayCertGenContext era -> VotingProcedures era
ccccWithdrawals :: forall era. ConwayCertGenContext era -> Map RewardAccount Coin
ccccWithdrawals :: Map RewardAccount Coin
ccccVotes :: VotingProcedures ConwayEra
ccccDelegatees :: Map (Credential DRepRole) (Set (Credential Staking))
..}) CertsEnv {EpochNo
certsCurrentEpoch :: EpochNo
certsCurrentEpoch :: forall era. CertsEnv era -> EpochNo
certsCurrentEpoch} ->
        WitUniv ConwayEra
-> (Map (Credential DRepRole) (Set (Credential Staking)),
    Map RewardAccount Coin)
-> TermD Deps EpochNo
-> Specification (ConwayCertState ConwayEra)
conwayCertStateSpec WitUniv ConwayEra
u (Map (Credential DRepRole) (Set (Credential Staking))
ccccDelegatees, Map RewardAccount Coin
ccccWithdrawals) (EpochNo -> TermD Deps EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
certsCurrentEpoch)
    )
    (\(WitUniv ConwayEra
u, ConwayCertGenContext ConwayEra
_) -> WitUniv ConwayEra
-> CertsEnv ConwayEra
-> CertState ConwayEra
-> Specification (Seq (TxCert ConwayEra))
forall era.
EraSpecCert era =>
WitUniv era
-> CertsEnv era
-> CertState era
-> Specification (Seq (TxCert era))
txCertsSpec WitUniv ConwayEra
u)

constrainedRatify :: ConstrainedGeneratorBundle [GovActionState ConwayEra] "RATIFY" ConwayEra
constrainedRatify :: ConstrainedGeneratorBundle
  [GovActionState ConwayEra] "RATIFY" ConwayEra
constrainedRatify =
  Gen [GovActionState ConwayEra]
-> ([GovActionState ConwayEra]
    -> Specification (Environment (EraRule "RATIFY" ConwayEra)))
-> ([GovActionState ConwayEra]
    -> Environment (EraRule "RATIFY" ConwayEra)
    -> Specification (State (EraRule "RATIFY" ConwayEra)))
-> ([GovActionState ConwayEra]
    -> Environment (EraRule "RATIFY" ConwayEra)
    -> State (EraRule "RATIFY" ConwayEra)
    -> Specification (Signal (EraRule "RATIFY" ConwayEra)))
-> ConstrainedGeneratorBundle
     [GovActionState ConwayEra] "RATIFY" ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    Gen [GovActionState ConwayEra]
forall a. Arbitrary a => Gen a
arbitrary
    [GovActionState ConwayEra] -> Specification (RatifyEnv ConwayEra)
[GovActionState ConwayEra]
-> Specification (Environment (EraRule "RATIFY" ConwayEra))
forall era.
[GovActionState era] -> Specification (RatifyEnv ConwayEra)
ratifyEnvSpec
    (\[GovActionState ConwayEra]
_ Environment (EraRule "RATIFY" ConwayEra)
env -> RatifyEnv ConwayEra -> Specification (RatifyState ConwayEra)
ratifyStateSpec RatifyEnv ConwayEra
Environment (EraRule "RATIFY" ConwayEra)
env)
    (\[GovActionState ConwayEra]
ctx Environment (EraRule "RATIFY" ConwayEra)
_ State (EraRule "RATIFY" ConwayEra)
_ -> [GovActionState ConwayEra]
-> Specification (RatifySignal ConwayEra)
ratifySignalSpec [GovActionState ConwayEra]
ctx)

constrainedGov :: ConstrainedGeneratorBundle () "GOV" ConwayEra
constrainedGov :: ConstrainedGeneratorBundle () "GOV" ConwayEra
constrainedGov =
  Gen ()
-> (() -> Specification (Environment (EraRule "GOV" ConwayEra)))
-> (()
    -> Environment (EraRule "GOV" ConwayEra)
    -> Specification (State (EraRule "GOV" ConwayEra)))
-> (()
    -> Environment (EraRule "GOV" ConwayEra)
    -> State (EraRule "GOV" ConwayEra)
    -> Specification (Signal (EraRule "GOV" ConwayEra)))
-> ConstrainedGeneratorBundle () "GOV" ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    (() -> Gen ()
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())
    (Specification (GovEnv ConwayEra)
-> () -> Specification (GovEnv ConwayEra)
forall a b. a -> b -> a
const Specification (GovEnv ConwayEra)
govEnvSpec)
    ((GovEnv ConwayEra -> Specification (Proposals ConwayEra))
-> () -> GovEnv ConwayEra -> Specification (Proposals ConwayEra)
forall a b. a -> b -> a
const GovEnv ConwayEra -> Specification (Proposals ConwayEra)
govProposalsSpec)
    ((GovEnv ConwayEra
 -> Proposals ConwayEra -> Specification (GovSignal ConwayEra))
-> ()
-> GovEnv ConwayEra
-> Proposals ConwayEra
-> Specification (GovSignal ConwayEra)
forall a b. a -> b -> a
const GovEnv ConwayEra
-> Proposals ConwayEra -> Specification (GovSignal ConwayEra)
govProceduresSpec)

constrainedUtxo ::
  ConstrainedGeneratorBundle (UtxoExecContext ConwayEra) "UTXO" ConwayEra
constrainedUtxo :: ConstrainedGeneratorBundle
  (UtxoExecContext ConwayEra) "UTXO" ConwayEra
constrainedUtxo =
  Gen (UtxoExecContext ConwayEra)
-> (UtxoExecContext ConwayEra
    -> Specification (Environment (EraRule "UTXO" ConwayEra)))
-> (UtxoExecContext ConwayEra
    -> Environment (EraRule "UTXO" ConwayEra)
    -> Specification (State (EraRule "UTXO" ConwayEra)))
-> (UtxoExecContext ConwayEra
    -> Environment (EraRule "UTXO" ConwayEra)
    -> State (EraRule "UTXO" ConwayEra)
    -> Specification (Signal (EraRule "UTXO" ConwayEra)))
-> ConstrainedGeneratorBundle
     (UtxoExecContext ConwayEra) "UTXO" ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    Gen (UtxoExecContext ConwayEra)
genUtxoExecContext
    UtxoExecContext ConwayEra -> Specification (UtxoEnv ConwayEra)
UtxoExecContext ConwayEra
-> Specification (Environment (EraRule "UTXO" ConwayEra))
utxoEnvSpec
    UtxoExecContext ConwayEra
-> UtxoEnv ConwayEra -> Specification (UTxOState ConwayEra)
UtxoExecContext ConwayEra
-> Environment (EraRule "UTXO" ConwayEra)
-> Specification (State (EraRule "UTXO" ConwayEra))
utxoStateSpec
    (\UtxoExecContext ConwayEra
ctx Environment (EraRule "UTXO" ConwayEra)
_ State (EraRule "UTXO" ConwayEra)
_ -> UtxoExecContext ConwayEra -> Specification (Tx TopTx ConwayEra)
forall era.
HasSpec (Tx TopTx era) =>
UtxoExecContext era -> Specification (Tx TopTx era)
utxoTxSpec UtxoExecContext ConwayEra
ctx)

constrainedEpoch :: ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra
constrainedEpoch :: ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra
constrainedEpoch =
  Gen EpochNo
-> (EpochNo
    -> Specification (Environment (EraRule "EPOCH" ConwayEra)))
-> (EpochNo
    -> Environment (EraRule "EPOCH" ConwayEra)
    -> Specification (State (EraRule "EPOCH" ConwayEra)))
-> (EpochNo
    -> Environment (EraRule "EPOCH" ConwayEra)
    -> State (EraRule "EPOCH" ConwayEra)
    -> Specification (Signal (EraRule "EPOCH" ConwayEra)))
-> ConstrainedGeneratorBundle EpochNo "EPOCH" ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    Gen EpochNo
forall a. Arbitrary a => Gen a
arbitrary
    (Specification () -> EpochNo -> Specification ()
forall a b. a -> b -> a
const Specification ()
forall a. Specification a
trueSpec)
    (\EpochNo
ctx Environment (EraRule "EPOCH" ConwayEra)
_ -> TermD Deps EpochNo -> Specification (EpochState ConwayEra)
epochStateSpec (EpochNo -> TermD Deps EpochNo
forall a. HasSpec a => a -> Term a
lit EpochNo
ctx))
    (\EpochNo
ctx Environment (EraRule "EPOCH" ConwayEra)
_ State (EraRule "EPOCH" ConwayEra)
_ -> EpochNo -> Specification EpochNo
epochSignalSpec EpochNo
ctx)

constrainedNewEpoch :: ConstrainedGeneratorBundle EpochNo "NEWEPOCH" ConwayEra
constrainedNewEpoch :: ConstrainedGeneratorBundle EpochNo "NEWEPOCH" ConwayEra
constrainedNewEpoch =
  Gen EpochNo
-> (EpochNo
    -> Specification (Environment (EraRule "NEWEPOCH" ConwayEra)))
-> (EpochNo
    -> Environment (EraRule "NEWEPOCH" ConwayEra)
    -> Specification (State (EraRule "NEWEPOCH" ConwayEra)))
-> (EpochNo
    -> Environment (EraRule "NEWEPOCH" ConwayEra)
    -> State (EraRule "NEWEPOCH" ConwayEra)
    -> Specification (Signal (EraRule "NEWEPOCH" ConwayEra)))
-> ConstrainedGeneratorBundle EpochNo "NEWEPOCH" ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    Gen EpochNo
forall a. Arbitrary a => Gen a
arbitrary
    (Specification () -> EpochNo -> Specification ()
forall a b. a -> b -> a
const Specification ()
forall a. Specification a
trueSpec)
    (\EpochNo
_ Environment (EraRule "NEWEPOCH" ConwayEra)
_ -> Specification (State (EraRule "NEWEPOCH" ConwayEra))
Specification (NewEpochState ConwayEra)
newEpochStateSpec)
    (\EpochNo
ctx Environment (EraRule "NEWEPOCH" ConwayEra)
_ State (EraRule "NEWEPOCH" ConwayEra)
_ -> EpochNo -> Specification EpochNo
epochSignalSpec EpochNo
ctx)

constrainedEnact :: ConstrainedGeneratorBundle EpochNo "ENACT" ConwayEra
constrainedEnact :: ConstrainedGeneratorBundle EpochNo "ENACT" ConwayEra
constrainedEnact =
  Gen EpochNo
-> (EpochNo
    -> Specification (Environment (EraRule "ENACT" ConwayEra)))
-> (EpochNo
    -> Environment (EraRule "ENACT" ConwayEra)
    -> Specification (State (EraRule "ENACT" ConwayEra)))
-> (EpochNo
    -> Environment (EraRule "ENACT" ConwayEra)
    -> State (EraRule "ENACT" ConwayEra)
    -> Specification (Signal (EraRule "ENACT" ConwayEra)))
-> ConstrainedGeneratorBundle EpochNo "ENACT" ConwayEra
forall ctx (rule :: Symbol) era.
Gen ctx
-> (ctx -> Specification (Environment (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> Specification (State (EraRule rule era)))
-> (ctx
    -> Environment (EraRule rule era)
    -> State (EraRule rule era)
    -> Specification (Signal (EraRule rule era)))
-> ConstrainedGeneratorBundle ctx rule era
ConstrainedGeneratorBundle
    Gen EpochNo
forall a. Arbitrary a => Gen a
arbitrary
    (Specification () -> EpochNo -> Specification ()
forall a b. a -> b -> a
const Specification ()
forall a. Specification a
trueSpec)
    (\EpochNo
_ Environment (EraRule "ENACT" ConwayEra)
_ -> Specification (EnactState ConwayEra)
Specification (State (EraRule "ENACT" ConwayEra))
enactStateSpec)
    (\EpochNo
epoch Environment (EraRule "ENACT" ConwayEra)
_ State (EraRule "ENACT" ConwayEra)
st -> EpochNo
-> EnactState ConwayEra -> Specification (EnactSignal ConwayEra)
enactSignalSpec EpochNo
epoch EnactState ConwayEra
State (EraRule "ENACT" ConwayEra)
st)