{-# 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.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 (..))
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 forall a. a -> [a] -> [a]
:) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Int -> Gen a -> Gen [a]
vectorOf (Int
n forall a. Num a => a -> a -> a
- Int
1) Gen Coin
variedCoin

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

vstatePreds :: Era era => Proof era -> [Pred era]
vstatePreds :: forall era. Era era => Proof era -> [Pred era]
vstatePreds Proof era
p = forall era. Era era => Proof era -> [Pred era]
vstateGenPreds Proof era
p forall a. [a] -> [a] -> [a]
++ forall era. Proof era -> [Pred era]
vstateCheckPreds Proof era
p

vstateGenPreds :: forall era. Era era => Proof era -> [Pred era]
vstateGenPreds :: forall era. Era era => Proof era -> [Pred era]
vstateGenPreds Proof era
p = case forall era. Proof era -> PParamsWit era
whichPParams Proof era
p of
  PParamsWit era
PParamsConwayToConway ->
    [ forall era. Size -> Term era Size -> Pred era
MetaSize (Int -> Int -> Size
SzRng Int
5 Int
15) Term era Size
currentDRepStateSize
    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
currentDRepStateSize forall era.
Era era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState
    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
5 Int
7) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
committeeState)
    , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState) forall era. Era era => Term era (Set (Credential 'DRepRole))
voteUniv
    , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
committeeState) forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole))
voteCredUniv
    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
5) forall era. Era era => Term era EpochNo
numDormantEpochs
    , 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
        (forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat forall era. Era era => Rep era DRepState
DRepStateR [forall era t s. Field era t s -> Arg era t
Arg Field era DRepState EpochNo
expire, forall era t s. Field era t s -> Arg era t
Arg Field era DRepState (Maybe Anchor)
anchor, forall era t s. Field era t s -> Arg era t
Arg Field era DRepState Coin
deposit])
        [ forall era t. Term era t -> Pred era
Random (forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era DRepState (Maybe Anchor)
anchor)
        , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom
            (forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era DRepState EpochNo
expire)
            (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"+200To500" (\(EpochNo Word64
n) -> Word64 -> EpochNo
EpochNo forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Word64
n forall a. Num a => a -> a -> a
+ Word64
200, Word64
n forall a. Num a => a -> a -> a
+ Word64
500)) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era EpochNo
currentEpoch)
        , forall era. ConwayEraPParams era => Proof era -> Term era Coin
drepDeposit Proof era
p forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era DRepState Coin
deposit)
        ]
    , Term era [DRepState]
drepStateList forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems forall era.
Era era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState)
    , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. a -> Either a b
Left (Integer -> Coin
Coin Integer
1)) Term era Coin
totalDRepDeposit OrdCond
EQL [forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap forall era. Rep era Coin
CoinR Lens' DRepState Coin
drepDepositL forall era.
Era era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState]
    ]
  PParamsWit era
_ ->
    [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
0) forall era.
Era era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState
    , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
0) forall era.
Era era =>
Term
  era (Map (Credential 'ColdCommitteeRole) CommitteeAuthorization)
committeeState
    , forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era EpochNo
EpochR (Word64 -> EpochNo
EpochNo Word64
0) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era EpochNo
numDormantEpochs
    , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState
    ]
  where
    drepStateList :: Term era [DRepState]
drepStateList = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"drepStateList" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era DRepState
DRepStateR) 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" forall era. Rep era Coin
CoinR forall era. Era era => Rep era DRepState
DRepStateR 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" (forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR forall era. Era era => Rep era Anchor
AnchorR) forall era. Era era => Rep era DRepState
DRepStateR (Lens' DRepState (StrictMaybe Anchor)
drepAnchorL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Lens' (StrictMaybe x) (Maybe 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" forall era. Rep era EpochNo
EpochR forall era. Era era => Rep era DRepState
DRepStateR Lens' DRepState EpochNo
drepExpiryL
    totalDRepDeposit :: Term era Coin
totalDRepDeposit = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"totalDRepDeposit" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No
    currentDRepStateSize :: Term era Size
currentDRepStateSize = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> String -> Rep era t -> Access era s t -> V era t
pV Proof era
p String
"currentDRepStateSize" forall era. Rep era Size
SizeR 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 = forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (forall era. Era 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 <-
    forall a. Gen a -> IO a
generate
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage forall a. Default a => a
def Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst ConwayEra
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ConwayEra
subst forall era. Env era
emptyEnv)
      )
  VState ConwayEra
vstate <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env ConwayEra
env forall era. Era era => RootTarget era (VState era) (VState era)
vstateT
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall era. VState era -> PDoc
pcVState VState ConwayEra
vstate))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof ConwayEra
proof Env ConwayEra
env String
""

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

mainV :: IO ()
mainV :: IO ()
mainV = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ 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 :: Era era => Proof era -> [Pred era]
pstatePreds :: forall era. Era era => Proof era -> [Pred era]
pstatePreds Proof era
p = forall era. Era era => Proof era -> [Pred era]
pstateGenPreds Proof era
p forall a. [a] -> [a] -> [a]
++ forall era. Era era => Proof era -> [Pred era]
pstateCheckPreds Proof era
p

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

pstateCheckPreds :: Era era => Proof era -> [Pred era]
pstateCheckPreds :: forall era. Era era => Proof era -> [Pred era]
pstateCheckPreds Proof era
_ =
  [ forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) EpochNo)
retiring) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) -- Note regPools must be bigger than retiring
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits
  , forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era. Era era => Term era (Map (KeyHash 'StakePool) Coin)
poolDeposits)
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools) (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era 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 = forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (forall era. Era 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 <-
    forall a. Gen a -> IO a
generate
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage forall a. Default a => a
def Proof BabbageEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof BabbageEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst BabbageEra
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst BabbageEra
subst forall era. Env era
emptyEnv)
      )
  PState BabbageEra
pstate <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env BabbageEra
env forall era. Era era => RootTarget era (PState era) (PState era)
pstateT
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) forall a b. (a -> b) -> a -> b
$ do
    String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall era. PState era -> PDoc
pcPState PState BabbageEra
pstate))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof BabbageEra
proof Env BabbageEra
env String
""

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

mainP :: IO ()
mainP :: IO ()
mainP = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ 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 =
  forall era t s.
Era era =>
String -> Rep era t -> Rep era s -> Lens' s t -> Field era s t
Field
    String
"gdKeyHash1"
    forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR
    forall era. Era era => Rep era GenDelegPair
GenDelegPairR
    ( forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
        (\(GenDelegPair KeyHash 'GenesisDelegate
x VRFVerKeyHash 'GenDelegVRF
_) -> 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 (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 = forall era rec field. Field era rec field -> Term era field
fieldToTerm forall era. Era era => Field era GenDelegPair (KeyHash 'Witness)
gdKeyHashField

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

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

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

certStateGenPreds :: Era era => Proof era -> [Pred era]
certStateGenPreds :: forall era. Era era => Proof era -> [Pred era]
certStateGenPreds Proof era
p =
  [ forall era. Size -> Term era Size -> Pred era
MetaSize (Int -> Size
SzExact (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64
quorumConstant 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.
    forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era. Era era => Term era Coin
treasury (forall t era. t -> Target era t
constTarget (Integer -> Coin
Coin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Integer
1000, Integer
4000)))
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era. Era era => Term era Coin
reserves (forall t era. t -> Target era t
constTarget (Integer -> Coin
Coin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (Integer
4000, Integer
5000)))
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom forall era. Era era => Term era DeltaCoin
deltaTreasury (forall t era. t -> Target era t
constTarget (Integer -> DeltaCoin
DeltaCoin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Random a => (a, a) -> Gen a
choose (-Integer
200, Integer
400)))
  , forall era. Term era DeltaCoin -> Term era DeltaCoin
Negate (forall era. Era era => Term era DeltaCoin
deltaReserves) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era 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
    forall era. Size -> Term era Size -> Pred era
MetaSize (Int -> Int -> Size
SzRng Int
8 Int
15) Term era Size
rewardSize
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
rewardSize forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards
  , -- If 'instanReserves' or 'instanTreasury' have size zero, the SumsTo can't be solved
    forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanReserves
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanTreasury
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall era t r. Term era t -> RootTarget era r (Gen t) -> Pred era
GenFrom Term era [Coin]
rewardRange (forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"many" Size -> Gen [Coin]
manyCoin forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Size
rewardSize)
  , Term era [Coin]
rewardRange forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards
  , forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits)
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtMost Int
8) forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
incrementalStake
  , forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools
  , if forall era. Proof era -> ProtVer
protocolVersion Proof era
p forall a. Ord a => a -> a -> Bool
>= forall era. Proof era -> ProtVer
protocolVersion Proof ConwayEra
Conway
      then forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
0) forall era. Era era => Term era (Map Ptr (Credential 'Staking))
ptrs
      else forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era. Era era => Term era (Map Ptr (Credential 'Staking))
ptrs
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) DRep)
drepDelegation forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era. Era era => Term era (Map (Credential 'Staking) DRep)
drepDelegation forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set DRep)
drepUniv
  , -- Preds to compute genDelegs
    -- First, a set of GenDelegPairs, where no keyHash is repeated.
    forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
genDelegSize Term era (Set GenDelegPair)
gdKeyHashSet
  , forall b t1 era.
(Ord b, Ord t1) =>
Lens' b t1 -> Rep era t1 -> Term era (Set b) -> Term era (Set t1)
ProjS Lens' GenDelegPair (KeyHash 'Witness)
gdkeyL forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR Term era (Set GenDelegPair)
gdKeyHashSet forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv)
  , Term era [GenDelegPair]
gdKeyHashList forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era x. Term era (Set x) -> Target era [x]
setToListTarget Term era (Set GenDelegPair)
gdKeyHashSet
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized Term era Size
genDelegSize forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
  , Term era [GenDelegPair]
gdKeyHashList forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genesisHashUniv
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanReserves forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. a -> Either a b
Left (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
instanReservesSum OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanReserves]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
      (forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1))
      (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
instanReservesSum)
      OrdCond
LTH
      [forall era c. Term era c -> Sum era c
One (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
reserves), forall era c. Term era c -> Sum era c
One forall era. Era era => Term era DeltaCoin
deltaReserves, forall era c. Term era c -> Sum era c
One (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era DeltaCoin
DeltaCoinR (Integer -> DeltaCoin
DeltaCoin (-Integer
3000)))]
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanTreasury forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall b t1 era.
(Ord b, Ord t1) =>
Lens' b t1 -> Rep era t1 -> Term era (Set b) -> Term era (Set t1)
ProjS Lens' FutureGenDeleg (KeyHash 'Genesis)
fGenDelegGenKeyHashL forall era. Era era => Rep era (KeyHash 'Genesis)
GenHashR (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map FutureGenDeleg GenDelegPair)
futureGenDelegs) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
  , forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanTreasury)
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
instanTreasurySum OrdCond
EQL [forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instanTreasury]
  , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> DeltaCoin
DeltaCoin Integer
1)) (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
instanTreasurySum) OrdCond
LTH [forall era c. Term era c -> Sum era c
One (forall era. Term era Coin -> Term era DeltaCoin
Delta forall era. Era era => Term era Coin
treasury), forall era c. Term era c -> Sum era c
One forall era. Era era => Term era DeltaCoin
deltaTreasury]
  , forall era. Era era => Term era Coin
mirAvailTreasury
      forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"computeAvailTreasury" (MIRPot -> AccountState -> InstantaneousRewards -> Coin
availableAfterMIR MIRPot
TreasuryMIR)
              forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era r t. RootTarget era r t -> RootTarget era Void t
Mask forall era. Era era => RootTarget era AccountState AccountState
accountStateT
              forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era r t. RootTarget era r t -> RootTarget era Void t
Mask forall era.
Era era =>
RootTarget era InstantaneousRewards InstantaneousRewards
instantaneousRewardsT
           )
  , forall era. Era era => Term era Coin
mirAvailReserves
      forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( forall a b era. String -> (a -> b) -> RootTarget era Void (a -> b)
Constr String
"computeAvailReserves" (MIRPot -> AccountState -> InstantaneousRewards -> Coin
availableAfterMIR MIRPot
ReservesMIR)
              forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era r t. RootTarget era r t -> RootTarget era Void t
Mask forall era. Era era => RootTarget era AccountState AccountState
accountStateT
              forall era root a t.
RootTarget era root (a -> t)
-> RootTarget era root a -> RootTarget era root t
:$ forall era r t. RootTarget era r t -> RootTarget era Void t
Mask forall era.
Era era =>
RootTarget era InstantaneousRewards InstantaneousRewards
instantaneousRewardsT
           )
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) DRep)
drepDelegation forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era. Era era => Term era (Map (Credential 'Staking) DRep)
drepDelegation forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set DRep)
drepUniv
  ]
  where
    rewardSize :: Term era Size
rewardSize = forall era t. Era era => String -> Rep era t -> Term era t
var String
"rewardSize" forall era. Rep era Size
SizeR
    rewardRange :: Term era [Coin]
rewardRange = forall era t. Era era => String -> Rep era t -> Term era t
var String
"rewardRange" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Rep era Coin
CoinR)
    genDelegSize :: Term era Size
genDelegSize = forall era t. Era era => String -> Rep era t -> Term era t
var String
"genDelegSize" forall era. Rep era Size
SizeR
    gdKeyHashSet :: Term era (Set GenDelegPair)
gdKeyHashSet = forall era t. Era era => String -> Rep era t -> Term era t
var String
"gdKeyHashSet" (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era GenDelegPair
GenDelegPairR)
    gdKeyHashList :: Term era [GenDelegPair]
gdKeyHashList = forall era t. Era era => String -> Rep era t -> Term era t
var String
"gdKeyHashList" (forall era a. Rep era a -> Rep era [a]
ListR forall era. Era era => Rep era GenDelegPair
GenDelegPairR)

certStateCheckPreds :: Era era => Proof era -> [Pred era]
certStateCheckPreds :: forall era. Era era => Proof era -> [Pred era]
certStateCheckPreds Proof era
p =
  [ forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) (forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits)
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
stakeDeposits
  , forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards
  , if forall era. Proof era -> ProtVer
protocolVersion Proof era
p forall a. Ord a => a -> a -> Bool
>= forall era. Proof era -> ProtVer
protocolVersion Proof ConwayEra
Conway
      then forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
0) forall era. Era era => Term era (Map Ptr (Credential 'Staking))
ptrs
      else forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Era era => Term era (Map (Credential 'Staking) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a b era.
(Ord a, Ord b) =>
Term era (Map a b) -> Term era (Set b)
Rng forall era. Era 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 = forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo (forall era. Era 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 <-
    forall a. Int -> Gen a -> IO a
generateWithSeed
      Int
seed
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage forall a. Default a => a
def Proof BabbageEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof BabbageEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst BabbageEra
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst BabbageEra
subst forall era. Env era
emptyEnv)
      )
  DState BabbageEra
dState <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env BabbageEra
env forall era. Era era => RootTarget era (DState era) (DState era)
dstateT
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall c. DState c -> PDoc
pcDState DState BabbageEra
dState))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof BabbageEra
proof Env BabbageEra
env String
""

demoTestD :: TestTree
demoTestD :: TestTree
demoTestD = 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 forall a b. (a -> b) -> a -> b
$ 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 <-
    forall a. Gen a -> IO a
generate
      ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage forall a. Default a => a
def Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof ConwayEra
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst ConwayEra
subst -> forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst ConwayEra
subst forall era. Env era
emptyEnv)
      )
  CertState ConwayEra
certState <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env ConwayEra
env forall era.
Era era =>
RootTarget era (CertState era) (CertState era)
certstateT
  forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) forall a b. (a -> b) -> a -> b
$ String -> IO ()
putStrLn (forall a. Show a => a -> String
show (forall era. CertState era -> PDoc
pcCertState CertState ConwayEra
certState))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof ConwayEra
proof Env ConwayEra
env String
""

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

mainC :: IO ()
mainC :: IO ()
mainC = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ 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]