{-# 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
  !ctx
ctxt <- Gen ctx
cgbContextGen
  !Environment (EraRule rule era)
env <- Specification (Environment (EraRule rule era))
-> Gen (Environment (EraRule rule era))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (Specification (Environment (EraRule rule era))
 -> Gen (Environment (EraRule rule era)))
-> Specification (Environment (EraRule rule era))
-> Gen (Environment (EraRule rule era))
forall a b. (a -> b) -> a -> b
$ ctx -> Specification (Environment (EraRule rule era))
cgbEnvironmentSpec ctx
ctxt
  !State (EraRule rule era)
state <- Specification (State (EraRule rule era))
-> Gen (State (EraRule rule era))
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (Specification (State (EraRule rule era))
 -> Gen (State (EraRule rule era)))
-> Specification (State (EraRule rule era))
-> Gen (State (EraRule rule era))
forall a b. (a -> b) -> a -> b
$ ctx
-> Environment (EraRule rule era)
-> Specification (State (EraRule rule era))
cgbStateSpec ctx
ctxt Environment (EraRule rule era)
env
  let go :: State (EraRule rule era) -> Int -> Gen (Either [String] [Signal (EraRule rule era)])
      go :: State (EraRule rule era)
-> Int -> Gen (Either [[Char]] [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 (EraRule rule era)
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
        forall (s :: Symbol) e ans env state sig.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e),
 env ~ Environment (EraRule s e), state ~ State (EraRule s e),
 sig ~ Signal (EraRule s e)) =>
env
-> state
-> sig
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
goSTS @rule @era @(Gen (Either [String] [Signal (EraRule rule era)]))
          Environment (EraRule rule era)
env
          State (EraRule rule era)
st
          Signal (EraRule rule era)
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
                Either [[Char]] [Signal (EraRule rule era)]
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 Either [[Char]] [Signal (EraRule rule era)]
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))
          )
  State (EraRule rule era)
-> Int -> Gen (Either [[Char]] [Signal (EraRule rule era)])
go State (EraRule rule era)
state Int
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
  Either [[Char]] [Signal (EraRule rule era)]
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]) -> [t] -> Property -> Property
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 Either [[Char]] [Signal (EraRule rule era)]
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 ConwayEra
witUniv <- Int -> Gen (WitUniv ConwayEra)
forall era.
(GenScript era, HasWitness ScriptHash era) =>
Int -> Gen (WitUniv era)
genWitUniv Int
300
  ConwayCertGenContext ConwayEra
ccec <- Specification (ConwayCertGenContext ConwayEra)
-> Gen (ConwayCertGenContext ConwayEra)
forall a. (HasCallStack, HasSpec a) => Specification a -> Gen a
genFromSpec (Specification (ConwayCertGenContext ConwayEra)
 -> Gen (ConwayCertGenContext ConwayEra))
-> Specification (ConwayCertGenContext ConwayEra)
-> Gen (ConwayCertGenContext ConwayEra)
forall a b. (a -> b) -> a -> b
$ WitUniv ConwayEra
-> Integer -> Specification (ConwayCertGenContext ConwayEra)
forall era.
Era era =>
WitUniv era -> Integer -> Specification (ConwayCertGenContext era)
conwayCertExecContextSpec WitUniv ConwayEra
witUniv Integer
4
  (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
-> Gen (WitUniv ConwayEra, ConwayCertGenContext ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (WitUniv ConwayEra
witUniv, ConwayCertGenContext ConwayEra
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))
ccccWithdrawals :: forall era. ConwayCertGenContext era -> Map RewardAccount Coin
ccccVotes :: forall era. ConwayCertGenContext era -> VotingProcedures era
ccccDelegatees :: forall era.
ConwayCertGenContext era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
..}) =
  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
PoolDistr
CommitteeState ConwayEra
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
reInstantStake :: forall era. RatifyEnv era -> InstantStake era
reStakePoolDistr :: forall era. RatifyEnv era -> PoolDistr
reDRepDistr :: forall era. RatifyEnv era -> Map DRep (CompactForm Coin)
reDRepState :: forall era. RatifyEnv era -> Map (Credential 'DRepRole) DRepState
reCurrentEpoch :: forall era. RatifyEnv era -> EpochNo
reCommitteeState :: forall era. RatifyEnv era -> CommitteeState era
reAccounts :: forall era. RatifyEnv era -> Accounts era
reStakePools :: forall era.
RatifyEnv era -> Map (KeyHash 'StakePool) StakePoolState
..} =
  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
ensCommittee :: forall era. EnactState era -> StrictMaybe (Committee era)
ensConstitution :: forall era. EnactState era -> Constitution era
ensCurPParams :: forall era. EnactState era -> PParams era
ensPrevPParams :: forall era. EnactState era -> PParams era
ensTreasury :: forall era. EnactState era -> Coin
ensWithdrawals :: forall era. EnactState era -> Map (Credential 'Staking) Coin
ensPrevGovActionIds :: forall era. EnactState era -> GovRelation StrictMaybe
..} =
  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 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 era)) =>
Specification (CertsEnv era)
certsEnvSpec)
    ( \(WitUniv ConwayEra
u, ConwayCertGenContext {Map RewardAccount Coin
Map (Credential 'DRepRole) (Set (Credential 'Staking))
VotingProcedures ConwayEra
ccccWithdrawals :: forall era. ConwayCertGenContext era -> Map RewardAccount Coin
ccccVotes :: forall era. ConwayCertGenContext era -> VotingProcedures era
ccccDelegatees :: forall era.
ConwayCertGenContext era
-> Map (Credential 'DRepRole) (Set (Credential 'Staking))
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 ConwayEra)
forall era.
HasSpec (Tx era) =>
UtxoExecContext era -> Specification (Tx 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)