{-# 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, EraCrypto)
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 a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized Term era Size
currentDRepStateSize forall era.
Era era =>
Term
  era
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
currentDRepState
    , forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
5 Int
7) (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (Credential 'ColdCommitteeRole (EraCrypto era))
     (CommitteeAuthorization (EraCrypto era)))
committeeState)
    , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
currentDRepState) forall era.
Era era =>
Term era (Set (Credential 'DRepRole (EraCrypto era)))
voteUniv
    , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (Credential 'ColdCommitteeRole (EraCrypto era))
     (CommitteeAuthorization (EraCrypto era)))
committeeState) forall era.
Era era =>
Term era (Set (Credential 'ColdCommitteeRole (EraCrypto era)))
voteCredUniv
    , forall a era. Sizeable a => Term era Size -> Term era a -> 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 a r.
(Era era, FromList a r, Eq r) =>
Term era Size -> Term era a -> Pat era r -> [Pred era] -> Pred era
ForEach
        Term era Size
currentDRepStateSize
        Term era [DRepState (EraCrypto era)]
drepStateList
        (forall era t. Rep era t -> [Arg era t] -> Pat era t
Pat forall era. Era era => Rep era (DRepState (EraCrypto era))
DRepStateR [forall era t a. Field era t a -> Arg era t
Arg Field era (DRepState (EraCrypto era)) EpochNo
expire, forall era t a. Field era t a -> Arg era t
Arg Field
  era (DRepState (EraCrypto era)) (Maybe (Anchor (EraCrypto era)))
anchor, forall era t a. Field era t a -> Arg era t
Arg Field era (DRepState (EraCrypto era)) Coin
deposit])
        [ forall era a. Term era a -> Pred era
Random (forall era rec field. Field era rec field -> Term era field
fieldToTerm Field
  era (DRepState (EraCrypto era)) (Maybe (Anchor (EraCrypto era)))
anchor)
        , forall era a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom
            (forall era rec field. Field era rec field -> Term era field
fieldToTerm Field era (DRepState (EraCrypto era)) EpochNo
expire)
            (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 (EraCrypto era)) Coin
deposit)
        ]
    , Term era [DRepState (EraCrypto era)]
drepStateList forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: (forall a r era. (Ord a, Eq r) => Term era (Map a r) -> Term era [r]
Elems forall era.
Era era =>
Term
  era
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
currentDRepState)
    , forall era a.
(Era era, Adds a) =>
Direct a -> Term era a -> OrdCond -> [Sum era a] -> Pred era
SumsTo (forall a b. a -> Either a b
Left (Integer -> Coin
Coin Integer
1)) Term era Coin
totalDRepDeposit OrdCond
EQL [forall a c r era.
Adds c =>
Rep era c -> Lens' a c -> Term era (Map r a) -> Sum era c
ProjMap forall era. Rep era Coin
CoinR forall c. Lens' (DRepState c) Coin
drepDepositL forall era.
Era era =>
Term
  era
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
currentDRepState]
    ]
  PParamsWit era
_ ->
    [ forall a era. Sizeable a => Term era Size -> Term era a -> 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 (EraCrypto era)) (DRepState (EraCrypto era)))
currentDRepState
    , forall a era. Sizeable a => Term era Size -> Term era a -> 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 (EraCrypto era))
     (CommitteeAuthorization (EraCrypto era)))
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 a. Term era a -> Pred era
Random forall era.
Era era =>
Term
  era
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
currentDRepState
    ]
  where
    drepStateList :: Term era [DRepState (EraCrypto era)]
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 (EraCrypto era))
DRepStateR) forall era s t. Access era s t
No
    deposit :: Field era (DRepState (EraCrypto era)) 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 (EraCrypto era))
DRepStateR forall c. Lens' (DRepState c) Coin
drepDepositL
    anchor :: Field
  era (DRepState (EraCrypto era)) (Maybe (Anchor (EraCrypto era)))
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 a. Rep era a -> Rep era (Maybe a)
MaybeR forall era. Era era => Rep era (Anchor (EraCrypto era))
AnchorR) forall era. Era era => Rep era (DRepState (EraCrypto era))
DRepStateR (forall c. Lens' (DRepState c) (StrictMaybe (Anchor c))
drepAnchorL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x. Lens' (StrictMaybe x) (Maybe x)
strictMaybeToMaybeL)
    expire :: Field era (DRepState (EraCrypto era)) 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 (EraCrypto era))
DRepStateR forall c. Lens' (DRepState c) 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 StandardCrypto)
proof = Proof (ConwayEra StandardCrypto)
Conway
  Env (ConwayEra StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst (ConwayEra StandardCrypto)
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 StandardCrypto)
subst forall era. Env era
emptyEnv)
      )
  VState (ConwayEra StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
vstate))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof (ConwayEra StandardCrypto)
proof Env (ConwayEra StandardCrypto)
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 a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
5) forall era.
Era era =>
Term era (Map (KeyHash 'StakePool (EraCrypto era)) EpochNo)
retiring
  , forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
20) forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
regPools
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
regPools) forall era.
Era era =>
Term era (Set (KeyHash 'StakePool (EraCrypto era)))
poolHashUniv
  , forall a era. Sizeable a => Term era Size -> Term era a -> 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 (EraCrypto era)) (PoolParams (EraCrypto era)))
futureRegPools
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
futureRegPools) forall era.
Era era =>
Term era (Set (KeyHash 'StakePool (EraCrypto era)))
poolHashUniv
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
poolDeposits) forall era.
Era era =>
Term era (Set (KeyHash 'StakePool (EraCrypto era)))
poolHashUniv
  , forall era a.
(Era era, Eq a) =>
Term era Size
-> Term era [a] -> [(Int, Target era a, [Pred era])] -> Pred era
Choose
      (forall era. Era era => Int -> Term era Size
ExactSize Int
3)
      Term era [EpochNo]
epochs
      [ (Int
1, forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 a era. Count a => Term era a -> Term era a -> Pred era
CanFollow Term era EpochNo
e forall era. Era era => Term era EpochNo
currentEpoch])
      , (Int
1, forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 a era. Count a => Term era a -> Term era a -> Pred era
CanFollow Term era EpochNo
e forall era. Era era => Term era EpochNo
currentEpoch])
      , (Int
1, forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 a era. Count a => Term era a -> Term era a -> Pred era
CanFollow Term era EpochNo
e forall era. Era era => Term era EpochNo
currentEpoch])
      , (Int
1, forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 a era. Count a => Term era a -> Term era a -> 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 r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool (EraCrypto era)) EpochNo)
retiring) (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
regPools) -- Note regPools must be bigger than retiring
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
regPools forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'StakePool (EraCrypto era)) 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 r era.
(Ord a, Ord r) =>
Term era (Map a r) -> Term era (Set r)
Rng forall era.
Era era =>
Term era (Map (KeyHash 'StakePool (EraCrypto era)) Coin)
poolDeposits)
  , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
regPools) (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
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 StandardCrypto)
proof = Proof (BabbageEra StandardCrypto)
Babbage
  Env (BabbageEra StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst (BabbageEra StandardCrypto)
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 StandardCrypto)
subst forall era. Env era
emptyEnv)
      )
  PState (BabbageEra StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
pstate))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof (BabbageEra StandardCrypto)
proof Env (BabbageEra StandardCrypto)
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 (EraCrypto era))
    (KeyHash 'Witness (EraCrypto era))
gdKeyHashField :: forall era.
Era era =>
Field
  era
  (GenDelegPair (EraCrypto era))
  (KeyHash 'Witness (EraCrypto era))
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 (EraCrypto era))
WitHashR
    forall era. Era era => Rep era (GenDelegPair (EraCrypto era))
GenDelegPairR
    ( forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
        (\(GenDelegPair KeyHash 'GenesisDelegate (EraCrypto era)
x VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
_) -> forall (a :: KeyRole -> * -> *) (r :: KeyRole) c.
HasKeyRole a =>
a r c -> a 'Witness c
asWitness KeyHash 'GenesisDelegate (EraCrypto era)
x)
        (\(GenDelegPair KeyHash 'GenesisDelegate (EraCrypto era)
_ VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
y) KeyHash 'Witness (EraCrypto era)
x -> forall c.
KeyHash 'GenesisDelegate c
-> VRFVerKeyHash 'GenDelegVRF c -> GenDelegPair c
GenDelegPair (forall (a :: KeyRole -> * -> *) (r :: KeyRole) c (r' :: KeyRole).
HasKeyRole a =>
a r c -> a r' c
coerceKeyRole KeyHash 'Witness (EraCrypto era)
x) VRFVerKeyHash 'GenDelegVRF (EraCrypto era)
y)
    )

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

gdkeyL :: Lens' (GenDelegPair c) (KeyHash 'Witness c)
gdkeyL :: forall c. Lens' (GenDelegPair c) (KeyHash 'Witness c)
gdkeyL =
  ( forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens
      (\(GenDelegPair KeyHash 'GenesisDelegate c
x VRFVerKeyHash 'GenDelegVRF c
_) -> forall (a :: KeyRole -> * -> *) (r :: KeyRole) c.
HasKeyRole a =>
a r c -> a 'Witness c
asWitness KeyHash 'GenesisDelegate c
x)
      (\(GenDelegPair KeyHash 'GenesisDelegate c
_ VRFVerKeyHash 'GenDelegVRF c
y) KeyHash 'Witness c
x -> forall c.
KeyHash 'GenesisDelegate c
-> VRFVerKeyHash 'GenDelegVRF c -> GenDelegPair c
GenDelegPair (forall (a :: KeyRole -> * -> *) (r :: KeyRole) c (r' :: KeyRole).
HasKeyRole a =>
a r c -> a r' c
coerceKeyRole KeyHash 'Witness c
x) VRFVerKeyHash 'GenDelegVRF c
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 a r. Term era a -> RootTarget era r (Gen a) -> 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 a r. Term era a -> RootTarget era r (Gen a) -> 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 a r. Term era a -> RootTarget era r (Gen a) -> 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 a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized Term era Size
rewardSize forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
rewards
  , -- If 'instanReserves' or 'instanTreasury' have size zero, the SumsTo can't be solved
    forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
instanReserves
  , forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtLeast Int
1) forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
instanTreasury
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) 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 (EraCrypto era)))
credsUniv
  , forall era a r. Term era a -> RootTarget era r (Gen a) -> Pred era
GenFrom Term era [Coin]
rewardRange (forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
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 r era. (Ord a, Eq r) => Term era (Map a r) -> Term era [r]
Elems forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) 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 r era.
(Ord a, Ord r) =>
Term era (Map a r) -> Term era (Set r)
Rng forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
stakeDeposits)
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
stakeDeposits
  , forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
AtMost Int
8) forall era.
Era era =>
Term
  era
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegations
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
rewards
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
incrementalStake
  , forall a r era.
(Ord a, Ord r) =>
Term era (Map a r) -> Term era (Set r)
Rng forall era.
Era era =>
Term
  era
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
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 StandardCrypto)
Conway
      then forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
0) forall era.
Era era =>
Term era (Map Ptr (Credential 'Staking (EraCrypto era)))
ptrs
      else forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a r era.
(Ord a, Ord r) =>
Term era (Map a r) -> Term era (Set r)
Rng forall era.
Era era =>
Term era (Map Ptr (Credential 'Staking (EraCrypto era)))
ptrs
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map (Credential 'Staking (EraCrypto era)) (DRep (EraCrypto era)))
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 (EraCrypto era)))
credsUniv
  , forall a r era.
(Ord a, Ord r) =>
Term era (Map a r) -> Term era (Set r)
Rng forall era.
Era era =>
Term
  era
  (Map (Credential 'Staking (EraCrypto era)) (DRep (EraCrypto era)))
drepDelegation forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (DRep (EraCrypto era)))
drepUniv
  , -- Preds to compute genDelegs
    -- First, a set of GenDelegPairs, where no keyHash is repeated.
    forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized Term era Size
genDelegSize Term era (Set (GenDelegPair (EraCrypto era)))
gdKeyHashSet
  , forall a r era.
(Ord a, Ord r) =>
Lens' a r -> Rep era r -> Term era (Set a) -> Term era (Set r)
ProjS forall c. Lens' (GenDelegPair c) (KeyHash 'Witness c)
gdkeyL forall era. Era era => Rep era (KeyHash 'Witness (EraCrypto era))
WitHashR Term era (Set (GenDelegPair (EraCrypto era)))
gdKeyHashSet forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv)
  , Term era [GenDelegPair (EraCrypto era)]
gdKeyHashList forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: forall era x. Term era (Set x) -> Target era [x]
setToListTarget Term era (Set (GenDelegPair (EraCrypto era)))
gdKeyHashSet
  , forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized Term era Size
genDelegSize forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)))
genDelegs
  , Term era [GenDelegPair (EraCrypto era)]
gdKeyHashList forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a r era. (Ord a, Eq r) => Term era (Map a r) -> Term era [r]
Elems forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)))
genDelegs
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)))
genDelegs forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)))
genesisHashUniv
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) 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 (EraCrypto era)))
credsUniv
  , forall era a.
(Era era, Adds a) =>
Direct a -> Term era a -> OrdCond -> [Sum era a] -> 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 (EraCrypto era)) Coin)
instanReserves]
  , forall era a.
(Era era, Adds a) =>
Direct a -> Term era a -> OrdCond -> [Sum era a] -> 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 r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) 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 (EraCrypto era)))
credsUniv
  , forall a r era.
(Ord a, Ord r) =>
Lens' a r -> Rep era r -> Term era (Set a) -> Term era (Set r)
ProjS forall c. Lens' (FutureGenDeleg c) (KeyHash 'Genesis c)
fGenDelegGenKeyHashL forall era. Era era => Rep era (KeyHash 'Genesis (EraCrypto era))
GenHashR (forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (FutureGenDeleg (EraCrypto era)) (GenDelegPair (EraCrypto era)))
futureGenDelegs) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)))
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 r era.
(Ord a, Ord r) =>
Term era (Map a r) -> Term era (Set r)
Rng forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
instanTreasury)
  , forall era a.
(Era era, Adds a) =>
Direct a -> Term era a -> OrdCond -> [Sum era a] -> 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 (EraCrypto era)) Coin)
instanTreasury]
  , forall era a.
(Era era, Adds a) =>
Direct a -> Term era a -> OrdCond -> [Sum era a] -> 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 a r. Term era a -> RootTarget era r a -> Pred era
:<-: ( forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"computeAvailTreasury" (forall c. MIRPot -> AccountState -> InstantaneousRewards c -> Coin
availableAfterMIR MIRPot
TreasuryMIR)
              forall era r a b.
RootTarget era r (a -> b)
-> RootTarget era r a -> RootTarget era r b
:$ forall era a a. RootTarget era a a -> RootTarget era Void a
Mask forall era. Era era => RootTarget era AccountState AccountState
accountStateT
              forall era r a b.
RootTarget era r (a -> b)
-> RootTarget era r a -> RootTarget era r b
:$ forall era a a. RootTarget era a a -> RootTarget era Void a
Mask forall era.
Era era =>
RootTarget
  era
  (InstantaneousRewards (EraCrypto era))
  (InstantaneousRewards (EraCrypto era))
instantaneousRewardsT
           )
  , forall era. Era era => Term era Coin
mirAvailReserves
      forall era a r. Term era a -> RootTarget era r a -> Pred era
:<-: ( forall a r era. String -> (a -> r) -> RootTarget era Void (a -> r)
Constr String
"computeAvailReserves" (forall c. MIRPot -> AccountState -> InstantaneousRewards c -> Coin
availableAfterMIR MIRPot
ReservesMIR)
              forall era r a b.
RootTarget era r (a -> b)
-> RootTarget era r a -> RootTarget era r b
:$ forall era a a. RootTarget era a a -> RootTarget era Void a
Mask forall era. Era era => RootTarget era AccountState AccountState
accountStateT
              forall era r a b.
RootTarget era r (a -> b)
-> RootTarget era r a -> RootTarget era r b
:$ forall era a a. RootTarget era a a -> RootTarget era Void a
Mask forall era.
Era era =>
RootTarget
  era
  (InstantaneousRewards (EraCrypto era))
  (InstantaneousRewards (EraCrypto era))
instantaneousRewardsT
           )
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map (Credential 'Staking (EraCrypto era)) (DRep (EraCrypto era)))
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 (EraCrypto era)))
credsUniv
  , forall a r era.
(Ord a, Ord r) =>
Term era (Map a r) -> Term era (Set r)
Rng forall era.
Era era =>
Term
  era
  (Map (Credential 'Staking (EraCrypto era)) (DRep (EraCrypto era)))
drepDelegation forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall era. Era era => Term era (Set (DRep (EraCrypto era)))
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 (EraCrypto era)))
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 (EraCrypto era))
GenDelegPairR)
    gdKeyHashList :: Term era [GenDelegPair (EraCrypto era)]
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 (EraCrypto era))
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 r era.
(Ord a, Ord r) =>
Term era (Map a r) -> Term era (Set r)
Rng forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
stakeDeposits)
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
stakeDeposits
  , forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term
  era
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegations forall era a.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
:⊆: forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) 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 StandardCrypto)
Conway
      then forall a era. Sizeable a => Term era Size -> Term era a -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
0) forall era.
Era era =>
Term era (Map Ptr (Credential 'Staking (EraCrypto era)))
ptrs
      else forall a era r. Ord a => Term era (Map a r) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
rewards forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a r era.
(Ord a, Ord r) =>
Term era (Map a r) -> Term era (Set r)
Rng forall era.
Era era =>
Term era (Map Ptr (Credential 'Staking (EraCrypto era)))
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 StandardCrypto)
proof = Proof (BabbageEra StandardCrypto)
Babbage
  Env (BabbageEra StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst (BabbageEra StandardCrypto)
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 StandardCrypto)
subst forall era. Env era
emptyEnv)
      )
  DState (BabbageEra StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
dState))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof (BabbageEra StandardCrypto)
proof Env (BabbageEra StandardCrypto)
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 StandardCrypto)
proof = Proof (ConwayEra StandardCrypto)
Conway
  Env (ConwayEra StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst (ConwayEra StandardCrypto)
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 StandardCrypto)
subst forall era. Env era
emptyEnv)
      )
  CertState (ConwayEra StandardCrypto)
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 StandardCrypto)
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 StandardCrypto)
certState))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof (ConwayEra StandardCrypto)
proof Env (ConwayEra StandardCrypto)
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]