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

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

import Cardano.Ledger.Core (Era)
import Cardano.Ledger.EpochBoundary (SnapShot (..), Stake (..), calculatePoolDistr)
import Cardano.Ledger.PoolDistr (PoolDistr (..))
import Cardano.Ledger.Shelley.Core (EraGov)
import qualified Cardano.Ledger.UMap as UMap
import Control.Monad (when)
import Data.Default (Default (def))
import qualified Data.Map.Strict as Map
import qualified Data.VMap as VMap
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad (monadTyped)
import Test.Cardano.Ledger.Constrained.Preds.CertState (dstateStage, pstateStage, vstateStage)
import Test.Cardano.Ledger.Constrained.Preds.LedgerState (ledgerStateStage)
import Test.Cardano.Ledger.Constrained.Preds.PParams (pParamsStage)
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.UTxO (utxoStage)
import Test.Cardano.Ledger.Constrained.Preds.Universes (universeStage)
import Test.Cardano.Ledger.Constrained.Rewrite (OrderInfo (..), standardOrderInfo)
import Test.Cardano.Ledger.Constrained.Solver (toolChainSub)
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (testIO)
import Test.Cardano.Ledger.Constrained.Vars
import Test.Cardano.Ledger.Generic.PrettyCore (pcEpochState, pcNewEpochState)
import Test.Cardano.Ledger.Generic.Proof
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain)

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

epochstatePreds :: EraGov era => Proof era -> [Pred era]
epochstatePreds :: forall era. EraGov era => Proof era -> [Pred era]
epochstatePreds Proof era
_proof =
  [ forall era. Era era => Term era (Map (Credential 'Staking) Coin)
incrementalStake forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era (Map (Credential 'Staking) Coin)
markStake
  , forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
markDelegs
  , 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 era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
markPools
  , 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)
setStake forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , 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))
setDelegs forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` 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) (KeyHash 'StakePool))
setDelegs forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` 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
1 Int
2) forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
setPools
  , 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)
setPools forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , 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)
goStake forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` forall era. Era era => Term era (Set (Credential 'Staking))
credsUniv
  , 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))
goDelegs forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` 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) (KeyHash 'StakePool))
goDelegs forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` 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
1 Int
2) forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
goPools
  , 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)
goPools forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
snapShotFee
  , forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) IndividualPoolStake)
markPoolDistr
      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
"calculatePoolDistr"
              ( \Map (Credential 'Staking) Coin
stak Map (Credential 'Staking) (KeyHash 'StakePool)
del Map (KeyHash 'StakePool) PoolParams
pl ->
                  PoolDistr -> Map (KeyHash 'StakePool) IndividualPoolStake
unPoolDistr forall a b. (a -> b) -> a -> b
$
                    SnapShot -> PoolDistr
calculatePoolDistr
                      ( Stake
-> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
-> VMap VB VB (KeyHash 'StakePool) PoolParams
-> SnapShot
SnapShot
                          (VMap VB VP (Credential 'Staking) (CompactForm Coin) -> Stake
Stake (forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map HasCallStack => Coin -> CompactForm Coin
UMap.compactCoinOrError Map (Credential 'Staking) Coin
stak)))
                          (forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap Map (Credential 'Staking) (KeyHash 'StakePool)
del)
                          (forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap Map (KeyHash 'StakePool) PoolParams
pl)
                      )
              )
              forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Map (Credential 'Staking) Coin)
markStake
              forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
markDelegs
              forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
markPools
           )
  ]

newEpochStatePreds :: Era era => Proof era -> [Pred era]
newEpochStatePreds :: forall era. Era era => Proof era -> [Pred era]
newEpochStatePreds Proof era
_proof =
  [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
4) (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) Natural)
prevBlocksMade) -- Both prevBlocksMade and prevBlocksMadeDom will have size 4
  , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
4) (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) Natural)
currBlocksMade)
  , 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) Natural)
prevBlocksMade forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  , 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) Natural)
currBlocksMade forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
`Subset` forall era. Era era => Term era (Set (KeyHash 'StakePool))
poolHashUniv
  ]

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

epochStateStage ::
  Reflect era =>
  Proof era ->
  Subst era ->
  Gen (Subst era)
epochStateStage :: forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
epochStateStage 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. EraGov era => Proof era -> [Pred era]
epochstatePreds Proof era
proof)

demoES :: Reflect era => Proof era -> ReplMode -> IO ()
demoES :: forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoES Proof era
proof ReplMode
mode = do
  Env era
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 era
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 era
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)
utxoStage forall a. Default a => a
def Proof era
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 era
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 era
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 era
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)
ledgerStateStage forall a. Default a => a
def Proof era
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)
epochStateStage Proof era
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
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 era
subst forall era. Env era
emptyEnv)
      )
  EpochState era
epochstate <- 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 era
env (forall era.
EraGov era =>
Proof era -> RootTarget era (EpochState era) (EpochState era)
epochStateT Proof era
proof)
  let env2 :: Env era
env2 = forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget EpochState era
epochstate (forall era.
EraGov era =>
Proof era -> RootTarget era (EpochState era) (EpochState era)
epochStateT Proof era
proof) forall era. Env era
emptyEnv
  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
$ forall a. Show a => a -> IO ()
print (forall era. Reflect era => Proof era -> EpochState era -> PDoc
pcEpochState Proof era
proof EpochState era
epochstate)
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof era
proof Env era
env2 String
""

demoESTest :: TestTree
demoESTest :: TestTree
demoESTest = forall a. String -> IO a -> TestTree
testIO String
"Testing EpochState Stage" (forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoES Proof ConwayEra
Conway ReplMode
CI)

mainES :: IO ()
mainES :: IO ()
mainES = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ forall a. String -> IO a -> TestTree
testIO String
"Testing EpochState Stage" (forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoES Proof ConwayEra
Conway ReplMode
Interactive)

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

newEpochStateStage ::
  Reflect era =>
  Proof era ->
  Subst era ->
  Gen (Subst era)
newEpochStateStage :: forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
newEpochStateStage Proof era
proof = forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof (OrderInfo
standardOrderInfo {sumBeforeParts :: Bool
sumBeforeParts = Bool
False}) (forall era. Era era => Proof era -> [Pred era]
newEpochStatePreds Proof era
proof)

demoNES :: Reflect era => Proof era -> ReplMode -> IO ()
demoNES :: forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoNES Proof era
proof ReplMode
mode = do
  Env era
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 era
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 era
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 era
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 era
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 era
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)
ledgerStateStage forall a. Default a => a
def Proof era
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)
epochStateStage Proof era
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)
newEpochStateStage Proof era
proof
          forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (\Subst era
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 era
subst forall era. Env era
emptyEnv)
      )
  NewEpochState era
newepochstate <- 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 era
env (forall era.
EraGov era =>
Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
newEpochStateT Proof era
proof)
  let env2 :: Env era
env2 = forall era root t.
root -> RootTarget era root t -> Env era -> Env era
getTarget NewEpochState era
newepochstate (forall era.
EraGov era =>
Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
newEpochStateT Proof era
proof) forall era. Env era
emptyEnv
  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. Reflect era => Proof era -> NewEpochState era -> PDoc
pcNewEpochState Proof era
proof NewEpochState era
newepochstate))
  forall era. ReplMode -> Proof era -> Env era -> String -> IO ()
modeRepl ReplMode
mode Proof era
proof Env era
env2 String
""

demoNESTest :: TestTree
demoNESTest :: TestTree
demoNESTest = forall a. String -> IO a -> TestTree
testIO String
"Testing NewEpochState Stage" (forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoNES Proof ConwayEra
Conway ReplMode
CI)

mainNES :: IO ()
mainNES :: IO ()
mainNES = TestTree -> IO ()
defaultMain forall a b. (a -> b) -> a -> b
$ forall a. String -> IO a -> TestTree
testIO String
"Testing NewEpochState Stage" (forall era. Reflect era => Proof era -> ReplMode -> IO ()
demoNES Proof ConwayEra
Conway ReplMode
Interactive)

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