{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Constrained.Preds.CertState where

import Cardano.Ledger.BaseTypes (EpochNo (..))
import Cardano.Ledger.Coin (Coin (..), DeltaCoin (..))
import Cardano.Ledger.Conway.State (ConwayEraCertState, EraCertState)
import Cardano.Ledger.Core (Era)
import Cardano.Ledger.DRep (drepAnchorL, drepDepositL, drepExpiryL)
import Cardano.Ledger.Keys (GenDelegPair (..), KeyHash, KeyRole (..), asWitness, coerceKeyRole)
import Cardano.Ledger.Shelley.LedgerState (availableAfterMIR)
import Cardano.Ledger.Shelley.TxCert (MIRPot (..))
import Control.Monad (when)
import Data.Default (Default (def))
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes (OrdCond (..), unCertStateF)
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Lenses (fGenDelegGenKeyHashL, strictMaybeToMaybeL)
import Test.Cardano.Ledger.Constrained.Monad (generateWithSeed, monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.PParams (pParamsStage)
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.Universes hiding (demo, demoTest, main)
import Test.Cardano.Ledger.Constrained.Rewrite (standardOrderInfo)
import Test.Cardano.Ledger.Constrained.Size (Size (..), genFromSize)
import Test.Cardano.Ledger.Constrained.Solver
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (testIO)
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.Functions (protocolVersion)
import Test.Cardano.Ledger.Generic.PrettyCore (
  pcCertState,
  pcDState,
  pcPState,
  pcVState,
 )
import Test.Cardano.Ledger.Generic.Proof
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain, testGroup)

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

-- | A good spread of Coins with at least one (Coin 0)
manyCoin :: Size -> Gen [Coin]
manyCoin :: Size -> Gen [Coin]
manyCoin Size
size = do
  Int
n <- Size -> Gen Int
genFromSize Size
size
  (Integer -> Coin
Coin Integer
0 Coin -> [Coin] -> [Coin]
forall a. a -> [a] -> [a]
:) ([Coin] -> [Coin]) -> Gen [Coin] -> Gen [Coin]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen Coin -> Gen [Coin]
forall a. Int -> Gen a -> Gen [a]
vectorOf (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Gen Coin
variedCoin

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

vstatePreds :: Proof era -> [Pred era]
vstatePreds :: forall era. Proof era -> [Pred era]
vstatePreds Proof era
p = case Proof era -> CertStateWit era
forall era. Proof era -> CertStateWit era
whichCertState Proof era
p of
  CertStateWit era
CertStateShelleyToBabbage -> []
  CertStateWit era
CertStateConwayToConway -> Proof era -> [Pred era]
forall era. ConwayEraCertState era => Proof era -> [Pred era]
vstateGenPreds Proof era
p [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ Proof era -> [Pred era]
forall era. Proof era -> [Pred era]
vstateCheckPreds Proof era
p

vstateGenPreds :: forall era. ConwayEraCertState era => Proof era -> [Pred era]
vstateGenPreds :: forall era. ConwayEraCertState era => Proof era -> [Pred era]
vstateGenPreds Proof era
p = case Proof era -> PParamsWit era
forall era. Proof era -> PParamsWit era
whichPParams Proof era
p of
  PParamsWit era
PParamsConwayToConway ->
    [ Size -> Term era Size -> Pred era
forall era. Size -> Term era Size -> Pred era
MetaSize (Int -> Int -> Size
SzRng Int
5 Int
15) Term era Size
currentDRepStateSize
    , Term era Size
-> Term era (Map (Credential 'DRepRole) DRepState) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
currentDRepStateSize Term era (Map (Credential 'DRepRole) DRepState)
forall era.
ConwayEraCertState era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState
    , Term era Size
-> Term era (Set (Credential 'ColdCommitteeRole)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
5 Int
7) (Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> Term era (Set (Credential 'ColdCommitteeRole))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
forall era.
ConwayEraCertState era =>
Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
committeeState)
    , Term era (Set (Credential 'DRepRole))
-> Term era (Set (Credential 'DRepRole)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term era (Map (Credential 'DRepRole) DRepState)
-> Term era (Set (Credential 'DRepRole))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'DRepRole) DRepState)
forall era.
ConwayEraCertState era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState) Term era (Set (Credential 'DRepRole))
forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
    , Term era (Set (Credential 'ColdCommitteeRole))
-> Term era (Set (Credential 'ColdCommitteeRole)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> Term era (Set (Credential 'ColdCommitteeRole))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
forall era.
ConwayEraCertState era =>
Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
committeeState) Term era (Set (Credential 'ColdCommitteeRole))
forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole))
voteCredUniv
    , Term era Size -> Term era EpochNo -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
5) Term era EpochNo
forall era. ConwayEraCertState era => Term era EpochNo
numDormantEpochs
    , Term era Size
-> Term era [DRepState]
-> Pat era DRepState
-> [Pred era]
-> Pred era
forall era fs t.
(Era era, FromList fs t, Eq t) =>
Term era Size -> Term era fs -> Pat era t -> [Pred era] -> Pred era
ForEach
        Term era Size
currentDRepStateSize
        Term era [DRepState]
drepStateList
        (Rep era DRepState -> [Arg era DRepState] -> Pat era DRepState
forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat Rep era DRepState
forall era. Era era => Rep era DRepState
DRepStateR [Field era DRepState EpochNo -> Arg era DRepState
forall era t s. Field era t s -> Arg era t
Arg Field era DRepState EpochNo
expire, Field era DRepState (Maybe Anchor) -> Arg era DRepState
forall era t s. Field era t s -> Arg era t
Arg Field era DRepState (Maybe Anchor)
anchor, Field era DRepState Coin -> Arg era DRepState
forall era t s. Field era t s -> Arg era t
Arg Field era DRepState Coin
deposit])
        [ Term era (Maybe Anchor) -> Pred era
forall era t. Term era t -> Pred era
Random (Field era DRepState (Maybe Anchor) -> Term era (Maybe Anchor)
forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era DRepState (Maybe Anchor)
anchor)
        , Term era EpochNo -> RootTarget era Void (Gen EpochNo) -> Pred era
forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom
            (Field era DRepState EpochNo -> Term era EpochNo
forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era DRepState EpochNo
expire)
            (String
-> (EpochNo -> Gen EpochNo)
-> RootTarget era Void (EpochNo -> Gen EpochNo)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"+200To500" (\(EpochNo Word64
n) -> Word64 -> EpochNo
EpochNo (Word64 -> EpochNo) -> Gen Word64 -> Gen EpochNo
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word64, Word64) -> Gen Word64
forall a. Random a => (a, a) -> Gen a
choose (Word64
n Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
200, Word64
n Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
500)) RootTarget era Void (EpochNo -> Gen EpochNo)
-> Term era EpochNo -> RootTarget era Void (Gen EpochNo)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
forall era. Era era => Term era EpochNo
currentEpoch)
        , Proof era -> Term era Coin
forall era. ConwayEraPParams era => Proof era -> Term era Coin
drepDeposit Proof era
p Term era Coin -> Term era Coin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (Field era DRepState Coin -> Term era Coin
forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era DRepState Coin
deposit)
        ]
    , Term era [DRepState]
drepStateList Term era [DRepState] -> Term era [DRepState] -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (Term era (Map (Credential 'DRepRole) DRepState)
-> Term era [DRepState]
forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems Term era (Map (Credential 'DRepRole) DRepState)
forall era.
ConwayEraCertState era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState)
    , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. a -> Either a b
Left (Integer -> Coin
Coin Integer
1)) Term era Coin
totalDRepDeposit OrdCond
EQL [Rep era Coin
-> Lens' DRepState Coin
-> Term era (Map (Credential 'DRepRole) DRepState)
-> Sum era Coin
forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap Rep era Coin
forall era. Rep era Coin
CoinR (Coin -> f Coin) -> DRepState -> f DRepState
Lens' DRepState Coin
drepDepositL Term era (Map (Credential 'DRepRole) DRepState)
forall era.
ConwayEraCertState era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState]
    ]
  PParamsWit era
_ ->
    [ Term era Size
-> Term era (Map (Credential 'DRepRole) DRepState) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
0) Term era (Map (Credential 'DRepRole) DRepState)
forall era.
ConwayEraCertState era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState
    , Term era Size
-> Term
     era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
-> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
0) Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
forall era.
ConwayEraCertState era =>
Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
committeeState
    , Rep era EpochNo -> EpochNo -> Term era EpochNo
forall era t. Rep era t -> t -> Term era t
Lit Rep era EpochNo
forall era. Rep era EpochNo
EpochR (Word64 -> EpochNo
EpochNo Word64
0) Term era EpochNo -> Term era EpochNo -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era EpochNo
forall era. ConwayEraCertState era => Term era EpochNo
numDormantEpochs
    , Term era (Map (Credential 'DRepRole) DRepState) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (Credential 'DRepRole) DRepState)
forall era.
ConwayEraCertState era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState
    ]
  where
    drepStateList :: Term era [DRepState]
drepStateList = V era [DRepState] -> Term era [DRepState]
forall era t. V era t -> Term era t
Var (V era [DRepState] -> Term era [DRepState])
-> V era [DRepState] -> Term era [DRepState]
forall a b. (a -> b) -> a -> b
$ Proof era
-> String
-> Rep era [DRepState]
-> Access era Any [DRepState]
-> V era [DRepState]
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drepStateList" (Rep era DRepState -> Rep era [DRepState]
forall era a. Rep era a -> Rep era [a]
ListR Rep era DRepState
forall era. Era era => Rep era DRepState
DRepStateR) Access era Any [DRepState]
forall era s t. Access era s t
No
    deposit :: Field era DRepState Coin
deposit = forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field @era String
"deposit" Rep era Coin
forall era. Rep era Coin
CoinR Rep era DRepState
forall era. Era era => Rep era DRepState
DRepStateR (Coin -> f Coin) -> DRepState -> f DRepState
Lens' DRepState Coin
drepDepositL
    anchor :: Field era DRepState (Maybe Anchor)
anchor = forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field @era String
"anchor" (Rep era Anchor -> Rep era (Maybe Anchor)
forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR Rep era Anchor
forall era. Era era => Rep era Anchor
AnchorR) Rep era DRepState
forall era. Era era => Rep era DRepState
DRepStateR ((StrictMaybe Anchor -> f (StrictMaybe Anchor))
-> DRepState -> f DRepState
Lens' DRepState (StrictMaybe Anchor)
drepAnchorL ((StrictMaybe Anchor -> f (StrictMaybe Anchor))
 -> DRepState -> f DRepState)
-> ((Maybe Anchor -> f (Maybe Anchor))
    -> StrictMaybe Anchor -> f (StrictMaybe Anchor))
-> (Maybe Anchor -> f (Maybe Anchor))
-> DRepState
-> f DRepState
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe Anchor -> f (Maybe Anchor))
-> StrictMaybe Anchor -> f (StrictMaybe Anchor)
forall x (f :: * -> *).
Functor f =>
(Maybe x -> f (Maybe x)) -> StrictMaybe x -> f (StrictMaybe x)
strictMaybeToMaybeL)
    expire :: Field era DRepState EpochNo
expire = forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field @era String
"expire" Rep era EpochNo
forall era. Rep era EpochNo
EpochR Rep era DRepState
forall era. Era era => Rep era DRepState
DRepStateR (EpochNo -> f EpochNo) -> DRepState -> f DRepState
Lens' DRepState EpochNo
drepExpiryL
    totalDRepDeposit :: Term era Coin
totalDRepDeposit = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var (V era Coin -> Term era Coin) -> V era Coin -> Term era Coin
forall a b. (a -> b) -> a -> b
$ Proof era
-> String -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"totalDRepDeposit" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No
    currentDRepStateSize :: Term era Size
currentDRepStateSize = V era Size -> Term era Size
forall era t. V era t -> Term era t
Var (V era Size -> Term era Size) -> V era Size -> Term era Size
forall a b. (a -> b) -> a -> b
$ Proof era
-> String -> Rep era Size -> Access era Any Size -> V era Size
forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"currentDRepStateSize" Rep era Size
forall era. Rep era Size
SizeR Access era Any Size
forall era s t. Access era s t
No

vstateCheckPreds :: Proof era -> [Pred era]
vstateCheckPreds :: forall era. Proof era -> [Pred era]
vstateCheckPreds Proof era
_p = []

vstateStage ::
  Reflect era =>
  Proof era ->
  Subst era ->
  Gen (Subst era)
vstateStage :: forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof era
proof = Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (Proof era -> [Pred era]
forall era. Proof era -> [Pred era]
vstatePreds Proof era
proof)

demoV :: ReplMode -> IO ()
demoV :: ReplMode -> IO ()
demoV ReplMode
mode = do
  let proof :: Proof ConwayEra
proof = Proof ConwayEra
Conway
  Env ConwayEra
env <-
    Gen (Env ConwayEra) -> IO (Env ConwayEra)
forall a. Gen a -> IO a
generate
      ( Subst ConwayEra -> Gen (Subst ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst ConwayEra
forall era. Subst era
emptySubst
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
forall a. Default a => a
def Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Env ConwayEra)) -> Gen (Env ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst ConwayEra
subst -> Typed (Env ConwayEra) -> Gen (Env ConwayEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env ConwayEra) -> Gen (Env ConwayEra))
-> Typed (Env ConwayEra) -> Gen (Env ConwayEra)
forall a b. (a -> b) -> a -> b
$ Subst ConwayEra -> Env ConwayEra -> Typed (Env ConwayEra)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ConwayEra
subst Env ConwayEra
forall era. Env era
emptyEnv)
      )
  VState ConwayEra
vstate <- Typed (VState ConwayEra) -> IO (VState ConwayEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (VState ConwayEra) -> IO (VState ConwayEra))
-> Typed (VState ConwayEra) -> IO (VState ConwayEra)
forall a b. (a -> b) -> a -> b
$ Env ConwayEra
-> RootTarget ConwayEra (VState ConwayEra) (VState ConwayEra)
-> Typed (VState ConwayEra)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env ConwayEra
env RootTarget ConwayEra (VState ConwayEra) (VState ConwayEra)
forall era.
ConwayEraCertState era =>
RootTarget era (VState era) (VState era)
vstateT
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (PDoc -> String
forall a. Show a => a -> String
show (VState ConwayEra -> PDoc
forall era. VState era -> PDoc
pcVState VState ConwayEra
vstate))
  ReplMode -> Proof ConwayEra -> Env ConwayEra -> String -> IO ()
forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof ConwayEra
proof Env ConwayEra
env String
""

demoTestV :: TestTree
demoTestV :: TestTree
demoTestV = String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing VState Stage" (ReplMode -> IO ()
demoV ReplMode
CI)

mainV :: IO ()
mainV :: IO ()
mainV = TestTree -> IO ()
defaultMain (TestTree -> IO ()) -> TestTree -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing VState Stage" (ReplMode -> IO ()
demoV ReplMode
Interactive)

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

pstateNames :: [String]
pstateNames :: [String]
pstateNames =
  [ String
"regPools"
  , String
"futureRegPools"
  , String
"retiring"
  , String
"poolDeposits"
  ]

pstatePreds :: EraCertState era => Proof era -> [Pred era]
pstatePreds :: forall era. EraCertState era => Proof era -> [Pred era]
pstatePreds Proof era
p = Proof era -> [Pred era]
forall era. EraCertState era => Proof era -> [Pred era]
pstateGenPreds Proof era
p [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ Proof era -> [Pred era]
forall era. EraCertState era => Proof era -> [Pred era]
pstateCheckPreds Proof era
p

pstateGenPreds :: EraCertState era => Proof era -> [Pred era]
pstateGenPreds :: forall era. EraCertState era => Proof era -> [Pred era]
pstateGenPreds Proof era
_ =
  [ -- These Sized constraints are needd to be ensure that regPools is bigger than retiring
    Term era Size
-> Term era (Map (KeyHash 'StakePool) EpochNo) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
5) Term era (Map (KeyHash 'StakePool) EpochNo)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) EpochNo)
retiring
  , Term era Size
-> Term era (Map (KeyHash 'StakePool) PoolParams) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
20) Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools
  , Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era Size
-> Term era (Map (KeyHash 'StakePool) PoolParams) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
10 Int
15) Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools
  , Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools) Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term era (Map (KeyHash 'StakePool) Coin)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Coin)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits) Term era (Set (KeyHash 'StakePool))
forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , Term era Size
-> Term era [EpochNo]
-> [(Int, Target era EpochNo, [Pred era])]
-> Pred era
forall era t.
(Era era, Eq t) =>
Term era Size
-> Term era [t] -> [(Int, Target era t, [Pred era])] -> Pred era
Choose
      (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
3)
      Term era [EpochNo]
epochs
      [ (Int
1, String
-> (EpochNo -> EpochNo) -> RootTarget era Void (EpochNo -> EpochNo)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"id" EpochNo -> EpochNo
forall a. a -> a
id RootTarget era Void (EpochNo -> EpochNo)
-> Term era EpochNo -> Target era EpochNo
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
e, [Term era EpochNo -> Term era EpochNo -> Pred era
forall n era. Count n => Term era n -> Term era n -> Pred era
CanFollow Term era EpochNo
e Term era EpochNo
forall era. Era era => Term era EpochNo
currentEpoch])
      , (Int
1, String
-> (EpochNo -> EpochNo) -> RootTarget era Void (EpochNo -> EpochNo)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"(+1)" (EpochNo -> EpochNo -> EpochNo
forall a. Num a => a -> a -> a
+ EpochNo
1) RootTarget era Void (EpochNo -> EpochNo)
-> Term era EpochNo -> Target era EpochNo
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
e, [Term era EpochNo -> Term era EpochNo -> Pred era
forall n era. Count n => Term era n -> Term era n -> Pred era
CanFollow Term era EpochNo
e Term era EpochNo
forall era. Era era => Term era EpochNo
currentEpoch])
      , (Int
1, String
-> (EpochNo -> EpochNo) -> RootTarget era Void (EpochNo -> EpochNo)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"(+3)" (EpochNo -> EpochNo -> EpochNo
forall a. Num a => a -> a -> a
+ EpochNo
3) RootTarget era Void (EpochNo -> EpochNo)
-> Term era EpochNo -> Target era EpochNo
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
e, [Term era EpochNo -> Term era EpochNo -> Pred era
forall n era. Count n => Term era n -> Term era n -> Pred era
CanFollow Term era EpochNo
e Term era EpochNo
forall era. Era era => Term era EpochNo
currentEpoch])
      , (Int
1, String
-> (EpochNo -> EpochNo) -> RootTarget era Void (EpochNo -> EpochNo)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"(+5)" (EpochNo -> EpochNo -> EpochNo
forall a. Num a => a -> a -> a
+ EpochNo
5) RootTarget era Void (EpochNo -> EpochNo)
-> Term era EpochNo -> Target era EpochNo
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era EpochNo
e, [Term era EpochNo -> Term era EpochNo -> Pred era
forall n era. Count n => Term era n -> Term era n -> Pred era
CanFollow Term era EpochNo
e Term era EpochNo
forall era. Era era => Term era EpochNo
currentEpoch])
      ]
  ]
  where
    e :: Term era EpochNo
e = String -> Rep era EpochNo -> Term era EpochNo
forall era t. Era era => String -> Rep era t -> Term era t
var String
"e" Rep era EpochNo
forall era. Rep era EpochNo
EpochR
    epochs :: Term era [EpochNo]
epochs = String -> Rep era [EpochNo] -> Term era [EpochNo]
forall era t. Era era => String -> Rep era t -> Term era t
var String
"epochs" (Rep era EpochNo -> Rep era [EpochNo]
forall era a. Rep era a -> Rep era [a]
ListR Rep era EpochNo
forall era. Rep era EpochNo
EpochR)

pstateCheckPreds :: EraCertState era => Proof era -> [Pred era]
pstateCheckPreds :: forall era. EraCertState era => Proof era -> [Pred era]
pstateCheckPreds Proof era
_ =
  [ Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (Term era (Map (KeyHash 'StakePool) EpochNo)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) EpochNo)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) EpochNo)
retiring) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) -- Note regPools must be bigger than retiring
  , Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (KeyHash 'StakePool) Coin)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) Coin)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits
  , Term era Coin -> Term era (Set Coin) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (Term era (Map (KeyHash 'StakePool) Coin) -> Term era (Set Coin)
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map (KeyHash 'StakePool) Coin)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits)
  , Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) (Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
futureRegPools)
  ]

pstateStage ::
  Reflect era =>
  Proof era ->
  Subst era ->
  Gen (Subst era)
pstateStage :: forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof era
proof = Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (Proof era -> [Pred era]
forall era. EraCertState era => Proof era -> [Pred era]
pstatePreds Proof era
proof)

demoP :: ReplMode -> IO ()
demoP :: ReplMode -> IO ()
demoP ReplMode
mode = do
  let proof :: Proof BabbageEra
proof = Proof BabbageEra
Babbage
  Env BabbageEra
env <-
    Gen (Env BabbageEra) -> IO (Env BabbageEra)
forall a. Gen a -> IO a
generate
      ( Subst BabbageEra -> Gen (Subst BabbageEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst BabbageEra
forall era. Subst era
emptySubst
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
forall a. Default a => a
def Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Env BabbageEra))
-> Gen (Env BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst BabbageEra
subst -> Typed (Env BabbageEra) -> Gen (Env BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env BabbageEra) -> Gen (Env BabbageEra))
-> Typed (Env BabbageEra) -> Gen (Env BabbageEra)
forall a b. (a -> b) -> a -> b
$ Subst BabbageEra -> Env BabbageEra -> Typed (Env BabbageEra)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst BabbageEra
subst Env BabbageEra
forall era. Env era
emptyEnv)
      )
  PState BabbageEra
pstate <- Typed (PState BabbageEra) -> IO (PState BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (PState BabbageEra) -> IO (PState BabbageEra))
-> Typed (PState BabbageEra) -> IO (PState BabbageEra)
forall a b. (a -> b) -> a -> b
$ Env BabbageEra
-> RootTarget BabbageEra (PState BabbageEra) (PState BabbageEra)
-> Typed (PState BabbageEra)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env BabbageEra
env RootTarget BabbageEra (PState BabbageEra) (PState BabbageEra)
forall era.
EraCertState era =>
RootTarget era (PState era) (PState era)
pstateT
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ do
    String -> IO ()
putStrLn (PDoc -> String
forall a. Show a => a -> String
show (PState BabbageEra -> PDoc
forall era. PState era -> PDoc
pcPState PState BabbageEra
pstate))
  ReplMode -> Proof BabbageEra -> Env BabbageEra -> String -> IO ()
forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof BabbageEra
proof Env BabbageEra
env String
""

demoTestP :: TestTree
demoTestP :: TestTree
demoTestP = String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing PState Stage" (ReplMode -> IO ()
demoP ReplMode
CI)

mainP :: IO ()
mainP :: IO ()
mainP = TestTree -> IO ()
defaultMain (TestTree -> IO ()) -> TestTree -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing PState Stage" (ReplMode -> IO ()
demoP ReplMode
Interactive)

-- =================================================
-- A Field used to compute 'genDelegs'

-- | A field that selects the 'genDelegKeyHash' field from a 'GenDelegPair'
--   It also silently casts the 'KeyRole. from 'Genesis to 'Witness
gdKeyHashField :: Era era => Field era GenDelegPair (KeyHash 'Witness)
gdKeyHashField :: forall era. Era era => Field era GenDelegPair (KeyHash 'Witness)
gdKeyHashField =
  String
-> Rep era (KeyHash 'Witness)
-> Rep era GenDelegPair
-> Lens' GenDelegPair (KeyHash 'Witness)
-> Field era GenDelegPair (KeyHash 'Witness)
forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field
    String
"gdKeyHash1"
    Rep era (KeyHash 'Witness)
forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR
    Rep era GenDelegPair
forall era. Era era => Rep era GenDelegPair
GenDelegPairR
    ( (GenDelegPair -> KeyHash 'Witness)
-> (GenDelegPair -> KeyHash 'Witness -> GenDelegPair)
-> Lens' GenDelegPair (KeyHash 'Witness)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
        (\(GenDelegPair KeyHash 'GenesisDelegate
x VRFVerKeyHash 'GenDelegVRF
_) -> KeyHash 'GenesisDelegate -> KeyHash 'Witness
forall (a :: KeyRole -> *) (r :: KeyRole).
HasKeyRole a =>
a r -> a 'Witness
asWitness KeyHash 'GenesisDelegate
x)
        (\(GenDelegPair KeyHash 'GenesisDelegate
_ VRFVerKeyHash 'GenDelegVRF
y) KeyHash 'Witness
x -> KeyHash 'GenesisDelegate
-> VRFVerKeyHash 'GenDelegVRF -> GenDelegPair
GenDelegPair (KeyHash 'Witness -> KeyHash 'GenesisDelegate
forall (r :: KeyRole) (r' :: KeyRole). KeyHash r -> KeyHash r'
forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole KeyHash 'Witness
x) VRFVerKeyHash 'GenDelegVRF
y)
    )

-- | A Var Term that pairs the Field 'gdKeyHashField'
gdKeyHash :: Era era => Term era (KeyHash 'Witness)
gdKeyHash :: forall era. Era era => Term era (KeyHash 'Witness)
gdKeyHash = Field era GenDelegPair (KeyHash 'Witness)
-> Term era (KeyHash 'Witness)
forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era GenDelegPair (KeyHash 'Witness)
forall era. Era era => Field era GenDelegPair (KeyHash 'Witness)
gdKeyHashField

gdkeyL :: Lens' GenDelegPair (KeyHash 'Witness)
gdkeyL :: Lens' GenDelegPair (KeyHash 'Witness)
gdkeyL =
  (GenDelegPair -> KeyHash 'Witness)
-> (GenDelegPair -> KeyHash 'Witness -> GenDelegPair)
-> Lens' GenDelegPair (KeyHash 'Witness)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
    (\(GenDelegPair KeyHash 'GenesisDelegate
x VRFVerKeyHash 'GenDelegVRF
_) -> KeyHash 'GenesisDelegate -> KeyHash 'Witness
forall (a :: KeyRole -> *) (r :: KeyRole).
HasKeyRole a =>
a r -> a 'Witness
asWitness KeyHash 'GenesisDelegate
x)
    (\(GenDelegPair KeyHash 'GenesisDelegate
_ VRFVerKeyHash 'GenDelegVRF
y) KeyHash 'Witness
x -> KeyHash 'GenesisDelegate
-> VRFVerKeyHash 'GenDelegVRF -> GenDelegPair
GenDelegPair (KeyHash 'Witness -> KeyHash 'GenesisDelegate
forall (r :: KeyRole) (r' :: KeyRole). KeyHash r -> KeyHash r'
forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole KeyHash 'Witness
x) VRFVerKeyHash 'GenDelegVRF
y)

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

certStatePreds :: EraCertState era => Proof era -> [Pred era]
certStatePreds :: forall era. EraCertState era => Proof era -> [Pred era]
certStatePreds Proof era
p = Proof era -> [Pred era]
forall era. EraCertState era => Proof era -> [Pred era]
certStateGenPreds Proof era
p [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ Proof era -> [Pred era]
forall era. EraCertState era => Proof era -> [Pred era]
certStateCheckPreds Proof era
p

certStateGenPreds :: EraCertState era => Proof era -> [Pred era]
certStateGenPreds :: forall era. EraCertState era => Proof era -> [Pred era]
certStateGenPreds Proof era
p =
  [ Size -> Term era Size -> Pred era
forall era. Size -> Term era Size -> Pred era
MetaSize (Int -> Size
SzExact (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64
quorumConstant Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
2))) Term era Size
genDelegSize
  , --  , GenFrom quorum (constTarget (pure (fromIntegral quorumConstant)))

    -- These really belong in the AccountState in the EpochState, But they are the only pieces of the EpochState we use.
    -- and are necessary to compute the instantaneous rewards, which are in the DState.
    Term era Coin -> RootTarget era Void (Gen Coin) -> Pred era
forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom Term era Coin
forall era. Era era => Term era Coin
treasury (Gen Coin -> RootTarget era Void (Gen Coin)
forall t era. t -> Target era t
constTarget (Integer -> Coin
Coin (Integer -> Coin) -> Gen Integer -> Gen Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
1000, Integer
4000)))
  , Term era Coin -> RootTarget era Void (Gen Coin) -> Pred era
forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom Term era Coin
forall era. Era era => Term era Coin
reserves (Gen Coin -> RootTarget era Void (Gen Coin)
forall t era. t -> Target era t
constTarget (Integer -> Coin
Coin (Integer -> Coin) -> Gen Integer -> Gen Coin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (Integer
4000, Integer
5000)))
  , Term era DeltaCoin
-> RootTarget era Void (Gen DeltaCoin) -> Pred era
forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom Term era DeltaCoin
forall era. EraCertState era => Term era DeltaCoin
deltaTreasury (Gen DeltaCoin -> RootTarget era Void (Gen DeltaCoin)
forall t era. t -> Target era t
constTarget (Integer -> DeltaCoin
DeltaCoin (Integer -> DeltaCoin) -> Gen Integer -> Gen DeltaCoin
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Integer, Integer) -> Gen Integer
forall a. Random a => (a, a) -> Gen a
choose (-Integer
200, Integer
400)))
  , Term era DeltaCoin -> Term era DeltaCoin
forall era. Term era DeltaCoin -> Term era DeltaCoin
Negate Term era DeltaCoin
forall era. EraCertState era => Term era DeltaCoin
deltaReserves Term era DeltaCoin -> Term era DeltaCoin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era DeltaCoin
forall era. EraCertState era => Term era DeltaCoin
deltaTreasury -- Means deltaReserves ranges from (-400,200)
  , -- 'rewards' needs to be small enough that it leaves some slack with
    -- credUniv (size about 30), but it also cannot be empty
    Size -> Term era Size -> Pred era
forall era. Size -> Term era Size -> Pred era
MetaSize (Int -> Int -> Size
SzRng Int
8 Int
15) Term era Size
rewardSize
  , Term era Size
-> Term era (Map (Credential 'Staking) Coin) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
rewardSize Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
  , -- If 'instanReserves' or 'instanTreasury' have size zero, the SumsTo can't be solved
    Term era Size
-> Term era (Map (Credential 'Staking) Coin) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanReserves
  , Term era Size
-> Term era (Map (Credential 'Staking) Coin) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtLeast Int
1) Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanTreasury
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era [Coin] -> RootTarget era Void (Gen [Coin]) -> Pred era
forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom Term era [Coin]
rewardRange (String
-> (Size -> Gen [Coin]) -> RootTarget era Void (Size -> Gen [Coin])
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"many" Size -> Gen [Coin]
manyCoin RootTarget era Void (Size -> Gen [Coin])
-> Term era Size -> RootTarget era Void (Gen [Coin])
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Size
rewardSize)
  , Term era [Coin]
rewardRange Term era [Coin] -> Term era [Coin] -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (Credential 'Staking) Coin) -> Term era [Coin]
forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
  , Term era Coin -> Term era (Set Coin) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (Term era (Map (Credential 'Staking) Coin) -> Term era (Set Coin)
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits)
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits
  , Term era Size
-> Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
AtMost Int
8) Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instantStakeTerm
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool))
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations Term era (Set (KeyHash 'StakePool))
-> Term era (Set (KeyHash 'StakePool)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Map (KeyHash 'StakePool) PoolParams)
-> Term era (Set (KeyHash 'StakePool))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools
  , if Proof era -> ProtVer
forall era. Proof era -> ProtVer
protocolVersion Proof era
p ProtVer -> ProtVer -> Bool
forall a. Ord a => a -> a -> Bool
>= Proof ConwayEra -> ProtVer
forall era. Proof era -> ProtVer
protocolVersion Proof ConwayEra
Conway
      then Term era Size
-> Term era (Map Ptr (Credential 'Staking)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
0) Term era (Map Ptr (Credential 'Staking))
forall era.
EraCertState era =>
Term era (Map Ptr (Credential 'Staking))
ptrs
      else Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map Ptr (Credential 'Staking))
-> Term era (Set (Credential 'Staking))
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map Ptr (Credential 'Staking))
forall era.
EraCertState era =>
Term era (Map Ptr (Credential 'Staking))
ptrs
  , Term era (Map (Credential 'Staking) DRep)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) DRep)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) DRep)
drepDelegation Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era (Map (Credential 'Staking) DRep) -> Term era (Set DRep)
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map (Credential 'Staking) DRep)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) DRep)
drepDelegation Term era (Set DRep) -> Term era (Set DRep) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set DRep)
forall era. Era era => Term era (Set DRep)
drepUniv
  , -- Preds to compute genDelegs
    -- First, a set of GenDelegPairs, where no keyHash is repeated.
    Term era Size -> Term era (Set GenDelegPair) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
genDelegSize Term era (Set GenDelegPair)
gdKeyHashSet
  , Lens' GenDelegPair (KeyHash 'Witness)
-> Rep era (KeyHash 'Witness)
-> Term era (Set GenDelegPair)
-> Term era (Set (KeyHash 'Witness))
forall b t1 era.
(Ord b, Ord t1) =>
Lens' b t1 -> Rep era t1 -> Term era (Set b) -> Term era (Set t1)
ProjS (KeyHash 'Witness -> f (KeyHash 'Witness))
-> GenDelegPair -> f GenDelegPair
Lens' GenDelegPair (KeyHash 'Witness)
gdkeyL Rep era (KeyHash 'Witness)
forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR Term era (Set GenDelegPair)
gdKeyHashSet Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
-> Term era (Set (KeyHash 'Witness))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv
  , Term era [GenDelegPair]
gdKeyHashList Term era [GenDelegPair]
-> RootTarget era Void [GenDelegPair] -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era (Set GenDelegPair) -> RootTarget era Void [GenDelegPair]
forall era x. Term era (Set x) -> Target era [x]
setToListTarget Term era (Set GenDelegPair)
gdKeyHashSet
  , Term era Size
-> Term era (Map (KeyHash 'Genesis) GenDelegPair) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
genDelegSize Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
  , Term era [GenDelegPair]
gdKeyHashList Term era [GenDelegPair] -> Term era [GenDelegPair] -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (KeyHash 'Genesis) GenDelegPair)
-> Term era [GenDelegPair]
forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
  , Term era (Map (KeyHash 'Genesis) GenDelegPair)
-> Term era (Set (KeyHash 'Genesis))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs Term era (Set (KeyHash 'Genesis))
-> Term era (Set (KeyHash 'Genesis)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Map (KeyHash 'Genesis) GenDelegPair)
-> Term era (Set (KeyHash 'Genesis))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genesisHashUniv
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanReserves Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. a -> Either a b
Left (Integer -> Coin
Coin Integer
1)) Term era Coin
forall era. Era era => Term era Coin
instanReservesSum OrdCond
EQL [Term era (Map (Credential 'Staking) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanReserves]
  , Direct DeltaCoin
-> Term era DeltaCoin -> OrdCond -> [Sum era DeltaCoin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
      (DeltaCoin -> Direct DeltaCoin
forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1))
      (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
forall era. Era era => Term era Coin
instanReservesSum)
      OrdCond
LTH
      [Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
forall era. Era era => Term era Coin
reserves), Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One Term era DeltaCoin
forall era. EraCertState era => Term era DeltaCoin
deltaReserves, Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One (Rep era DeltaCoin -> DeltaCoin -> Term era DeltaCoin
forall era t. Rep era t -> t -> Term era t
Lit Rep era DeltaCoin
forall era. Rep era DeltaCoin
DeltaCoinR (Integer -> DeltaCoin
DeltaCoin (-Integer
3000)))]
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanTreasury Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Lens' FutureGenDeleg (KeyHash 'Genesis)
-> Rep era (KeyHash 'Genesis)
-> Term era (Set FutureGenDeleg)
-> Term era (Set (KeyHash 'Genesis))
forall b t1 era.
(Ord b, Ord t1) =>
Lens' b t1 -> Rep era t1 -> Term era (Set b) -> Term era (Set t1)
ProjS (KeyHash 'Genesis -> f (KeyHash 'Genesis))
-> FutureGenDeleg -> f FutureGenDeleg
Lens' FutureGenDeleg (KeyHash 'Genesis)
fGenDelegGenKeyHashL Rep era (KeyHash 'Genesis)
forall era. Era era => Rep era (KeyHash 'Genesis)
GenHashR (Term era (Map FutureGenDeleg GenDelegPair)
-> Term era (Set FutureGenDeleg)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map FutureGenDeleg GenDelegPair)
forall era.
EraCertState era =>
Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs) Term era (Set (KeyHash 'Genesis))
-> Term era (Set (KeyHash 'Genesis)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (KeyHash 'Genesis) GenDelegPair)
-> Term era (Set (KeyHash 'Genesis))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
  , Term era Coin -> Term era (Set Coin) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (Term era (Map (Credential 'Staking) Coin) -> Term era (Set Coin)
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanTreasury)
  , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term era Coin
forall era. Era era => Term era Coin
instanTreasurySum OrdCond
EQL [Term era (Map (Credential 'Staking) Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
instanTreasury]
  , Direct DeltaCoin
-> Term era DeltaCoin -> OrdCond -> [Sum era DeltaCoin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (DeltaCoin -> Direct DeltaCoin
forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1)) (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
forall era. Era era => Term era Coin
instanTreasurySum) OrdCond
LTH [Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One (Term era Coin -> Term era DeltaCoin
forall era. Term era Coin -> Term era DeltaCoin
Delta Term era Coin
forall era. Era era => Term era Coin
treasury), Term era DeltaCoin -> Sum era DeltaCoin
forall era c. Term era c -> Sum era c
One Term era DeltaCoin
forall era. EraCertState era => Term era DeltaCoin
deltaTreasury]
  , Term era Coin
forall era. Era era => Term era Coin
mirAvailTreasury
      Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( String
-> (ChainAccountState -> InstantaneousRewards -> Coin)
-> RootTarget
     era Void (ChainAccountState -> InstantaneousRewards -> Coin)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"computeAvailTreasury" (MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin
availableAfterMIR MIRPot
TreasuryMIR)
               RootTarget
  era Void (ChainAccountState -> InstantaneousRewards -> Coin)
-> RootTarget era Void ChainAccountState
-> RootTarget era Void (InstantaneousRewards -> Coin)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ RootTarget era ChainAccountState ChainAccountState
-> RootTarget era Void ChainAccountState
forall era r t. RootTarget era r t -> RootTarget era Void t
Mask RootTarget era ChainAccountState ChainAccountState
forall era.
Era era =>
RootTarget era ChainAccountState ChainAccountState
accountStateT
               RootTarget era Void (InstantaneousRewards -> Coin)
-> RootTarget era Void InstantaneousRewards
-> RootTarget era Void Coin
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ RootTarget era InstantaneousRewards InstantaneousRewards
-> RootTarget era Void InstantaneousRewards
forall era r t. RootTarget era r t -> RootTarget era Void t
Mask RootTarget era InstantaneousRewards InstantaneousRewards
forall era.
EraCertState era =>
RootTarget era InstantaneousRewards InstantaneousRewards
instantaneousRewardsT
           )
  , Term era Coin
forall era. Era era => Term era Coin
mirAvailReserves
      Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( String
-> (ChainAccountState -> InstantaneousRewards -> Coin)
-> RootTarget
     era Void (ChainAccountState -> InstantaneousRewards -> Coin)
forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"computeAvailReserves" (MIRPot -> ChainAccountState -> InstantaneousRewards -> Coin
availableAfterMIR MIRPot
ReservesMIR)
               RootTarget
  era Void (ChainAccountState -> InstantaneousRewards -> Coin)
-> RootTarget era Void ChainAccountState
-> RootTarget era Void (InstantaneousRewards -> Coin)
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ RootTarget era ChainAccountState ChainAccountState
-> RootTarget era Void ChainAccountState
forall era r t. RootTarget era r t -> RootTarget era Void t
Mask RootTarget era ChainAccountState ChainAccountState
forall era.
Era era =>
RootTarget era ChainAccountState ChainAccountState
accountStateT
               RootTarget era Void (InstantaneousRewards -> Coin)
-> RootTarget era Void InstantaneousRewards
-> RootTarget era Void Coin
forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ RootTarget era InstantaneousRewards InstantaneousRewards
-> RootTarget era Void InstantaneousRewards
forall era r t. RootTarget era r t -> RootTarget era Void t
Mask RootTarget era InstantaneousRewards InstantaneousRewards
forall era.
EraCertState era =>
RootTarget era InstantaneousRewards InstantaneousRewards
instantaneousRewardsT
           )
  , Term era (Map (Credential 'Staking) DRep)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) DRep)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) DRep)
drepDelegation Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set (Credential 'Staking))
forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , Term era (Map (Credential 'Staking) DRep) -> Term era (Set DRep)
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map (Credential 'Staking) DRep)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) DRep)
drepDelegation Term era (Set DRep) -> Term era (Set DRep) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Set DRep)
forall era. Era era => Term era (Set DRep)
drepUniv
  ]
  where
    rewardSize :: Term era Size
rewardSize = String -> Rep era Size -> Term era Size
forall era t. Era era => String -> Rep era t -> Term era t
var String
"rewardSize" Rep era Size
forall era. Rep era Size
SizeR
    rewardRange :: Term era [Coin]
rewardRange = String -> Rep era [Coin] -> Term era [Coin]
forall era t. Era era => String -> Rep era t -> Term era t
var String
"rewardRange" (Rep era Coin -> Rep era [Coin]
forall era a. Rep era a -> Rep era [a]
ListR Rep era Coin
forall era. Rep era Coin
CoinR)
    genDelegSize :: Term era Size
genDelegSize = String -> Rep era Size -> Term era Size
forall era t. Era era => String -> Rep era t -> Term era t
var String
"genDelegSize" Rep era Size
forall era. Rep era Size
SizeR
    gdKeyHashSet :: Term era (Set GenDelegPair)
gdKeyHashSet = String -> Rep era (Set GenDelegPair) -> Term era (Set GenDelegPair)
forall era t. Era era => String -> Rep era t -> Term era t
var String
"gdKeyHashSet" (Rep era GenDelegPair -> Rep era (Set GenDelegPair)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era GenDelegPair
forall era. Era era => Rep era GenDelegPair
GenDelegPairR)
    gdKeyHashList :: Term era [GenDelegPair]
gdKeyHashList = String -> Rep era [GenDelegPair] -> Term era [GenDelegPair]
forall era t. Era era => String -> Rep era t -> Term era t
var String
"gdKeyHashList" (Rep era GenDelegPair -> Rep era [GenDelegPair]
forall era a. Rep era a -> Rep era [a]
ListR Rep era GenDelegPair
forall era. Era era => Rep era GenDelegPair
GenDelegPairR)

certStateCheckPreds :: EraCertState era => Proof era -> [Pred era]
certStateCheckPreds :: forall era. EraCertState era => Proof era -> [Pred era]
certStateCheckPreds Proof era
p =
  [ Term era Coin -> Term era (Set Coin) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (Term era (Map (Credential 'Staking) Coin) -> Term era (Set Coin)
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits)
  , Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits
  , Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
  , if Proof era -> ProtVer
forall era. Proof era -> ProtVer
protocolVersion Proof era
p ProtVer -> ProtVer -> Bool
forall a. Ord a => a -> a -> Bool
>= Proof ConwayEra -> ProtVer
forall era. Proof era -> ProtVer
protocolVersion Proof ConwayEra
Conway
      then Term era Size
-> Term era (Map Ptr (Credential 'Staking)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
0) Term era (Map Ptr (Credential 'Staking))
forall era.
EraCertState era =>
Term era (Map Ptr (Credential 'Staking))
ptrs
      else Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map Ptr (Credential 'Staking))
-> Term era (Set (Credential 'Staking))
forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng Term era (Map Ptr (Credential 'Staking))
forall era.
EraCertState era =>
Term era (Map Ptr (Credential 'Staking))
ptrs
  ]

dstateStage ::
  Reflect era =>
  Proof era ->
  Subst era ->
  Gen (Subst era)
dstateStage :: forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof era
proof = Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (Proof era -> [Pred era]
forall era. EraCertState era => Proof era -> [Pred era]
certStatePreds Proof era
proof)

demoD :: ReplMode -> Int -> IO ()
demoD :: ReplMode -> Int -> IO ()
demoD ReplMode
mode Int
seed = do
  let proof :: Proof BabbageEra
proof = Proof BabbageEra
Babbage
  Env BabbageEra
env <-
    Int -> Gen (Env BabbageEra) -> IO (Env BabbageEra)
forall a. Int -> Gen a -> IO a
generateWithSeed
      Int
seed
      ( Subst BabbageEra -> Gen (Subst BabbageEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst BabbageEra
forall era. Subst era
emptySubst
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
forall a. Default a => a
def Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Env BabbageEra))
-> Gen (Env BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst BabbageEra
subst -> Typed (Env BabbageEra) -> Gen (Env BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env BabbageEra) -> Gen (Env BabbageEra))
-> Typed (Env BabbageEra) -> Gen (Env BabbageEra)
forall a b. (a -> b) -> a -> b
$ Subst BabbageEra -> Env BabbageEra -> Typed (Env BabbageEra)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst BabbageEra
subst Env BabbageEra
forall era. Env era
emptyEnv)
      )
  DState BabbageEra
dState <- Typed (DState BabbageEra) -> IO (DState BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (DState BabbageEra) -> IO (DState BabbageEra))
-> Typed (DState BabbageEra) -> IO (DState BabbageEra)
forall a b. (a -> b) -> a -> b
$ Env BabbageEra
-> RootTarget BabbageEra (DState BabbageEra) (DState BabbageEra)
-> Typed (DState BabbageEra)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env BabbageEra
env RootTarget BabbageEra (DState BabbageEra) (DState BabbageEra)
forall era.
EraCertState era =>
RootTarget era (DState era) (DState era)
dstateT
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (PDoc -> String
forall a. Show a => a -> String
show (DState BabbageEra -> PDoc
forall c. DState c -> PDoc
pcDState DState BabbageEra
dState))
  ReplMode -> Proof BabbageEra -> Env BabbageEra -> String -> IO ()
forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof BabbageEra
proof Env BabbageEra
env String
""

demoTestD :: TestTree
demoTestD :: TestTree
demoTestD = String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing DState Stage" (ReplMode -> Int -> IO ()
demoD ReplMode
CI Int
99)

mainD :: Int -> IO ()
mainD :: Int -> IO ()
mainD Int
seed = TestTree -> IO ()
defaultMain (TestTree -> IO ()) -> TestTree -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing DState Stage" (ReplMode -> Int -> IO ()
demoD ReplMode
Interactive Int
seed)

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

demoC :: ReplMode -> IO ()
demoC :: ReplMode -> IO ()
demoC ReplMode
mode = do
  let proof :: Proof ConwayEra
proof = Proof ConwayEra
Conway
  Env ConwayEra
env <-
    Gen (Env ConwayEra) -> IO (Env ConwayEra)
forall a. Gen a -> IO a
generate
      ( Subst ConwayEra -> Gen (Subst ConwayEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst ConwayEra
forall era. Subst era
emptySubst
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
forall a. Default a => a
def Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Subst ConwayEra))
-> Gen (Subst ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof ConwayEra -> Subst ConwayEra -> Gen (Subst ConwayEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof ConwayEra
proof
          Gen (Subst ConwayEra)
-> (Subst ConwayEra -> Gen (Env ConwayEra)) -> Gen (Env ConwayEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst ConwayEra
subst -> Typed (Env ConwayEra) -> Gen (Env ConwayEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env ConwayEra) -> Gen (Env ConwayEra))
-> Typed (Env ConwayEra) -> Gen (Env ConwayEra)
forall a b. (a -> b) -> a -> b
$ Subst ConwayEra -> Env ConwayEra -> Typed (Env ConwayEra)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ConwayEra
subst Env ConwayEra
forall era. Env era
emptyEnv)
      )
  CertStateF ConwayEra
certState <- Typed (CertStateF ConwayEra) -> IO (CertStateF ConwayEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (CertStateF ConwayEra) -> IO (CertStateF ConwayEra))
-> (RootTarget
      ConwayEra (CertStateF ConwayEra) (CertStateF ConwayEra)
    -> Typed (CertStateF ConwayEra))
-> RootTarget
     ConwayEra (CertStateF ConwayEra) (CertStateF ConwayEra)
-> IO (CertStateF ConwayEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env ConwayEra
-> RootTarget
     ConwayEra (CertStateF ConwayEra) (CertStateF ConwayEra)
-> Typed (CertStateF ConwayEra)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env ConwayEra
env (RootTarget ConwayEra (CertStateF ConwayEra) (CertStateF ConwayEra)
 -> IO (CertStateF ConwayEra))
-> RootTarget
     ConwayEra (CertStateF ConwayEra) (CertStateF ConwayEra)
-> IO (CertStateF ConwayEra)
forall a b. (a -> b) -> a -> b
$ RootTarget ConwayEra (CertStateF ConwayEra) (CertStateF ConwayEra)
forall era.
Reflect era =>
RootTarget era (CertStateF era) (CertStateF era)
certStateT
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (PDoc -> String
forall a. Show a => a -> String
show (CertState ConwayEra -> PDoc
forall era. Reflect era => CertState era -> PDoc
pcCertState (CertStateF ConwayEra -> CertState ConwayEra
forall era. CertStateF era -> CertState era
unCertStateF CertStateF ConwayEra
certState)))
  ReplMode -> Proof ConwayEra -> Env ConwayEra -> String -> IO ()
forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof ConwayEra
proof Env ConwayEra
env String
""

demoTestC :: TestTree
demoTestC :: TestTree
demoTestC = String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing CertState Stage" (ReplMode -> IO ()
demoC ReplMode
CI)

mainC :: IO ()
mainC :: IO ()
mainC = TestTree -> IO ()
defaultMain (TestTree -> IO ()) -> TestTree -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> IO () -> TestTree
forall a. String -> IO a -> TestTree
testIO String
"Testing CertState Stage" (ReplMode -> IO ()
demoC ReplMode
Interactive)

demoTest :: TestTree
demoTest :: TestTree
demoTest =
  String -> [TestTree] -> TestTree
testGroup
    String
"CertState tests"
    [TestTree
demoTestV, TestTree
demoTestP, TestTree
demoTestD, TestTree
demoTestC]