{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module Test.Cardano.Ledger.Constrained.Trace.TraceMonad where

import Cardano.Ledger.BaseTypes (Globals, SlotNo (..))
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Conway.Governance (
  ConwayEraGov,
  DRepPulser (..),
  DRepPulsingState (..),
  PulsingSnapshot (..),
  newEpochStateDRepPulsingStateL,
 )
import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..))
import Cardano.Ledger.Shelley.LedgerState (NewEpochState (..))
import Cardano.Ledger.Shelley.Rules (runIdentity)
import Cardano.Ledger.TxIn (TxIn)
import Control.Monad.Trans (lift)
import Control.Monad.Trans.Except
import Control.Monad.Trans.Reader (runReaderT)
import Control.Monad.Trans.State.Strict hiding (State)
import Control.State.Transition.Extended (IRC (..), STS, TRC (..))
import Data.Default.Class (Default (def))
import Data.Foldable (toList)
import qualified Data.Foldable as Fold (toList)
import Data.Function (on)
import qualified Data.HashSet as HashSet
import qualified Data.List.NonEmpty as NE
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Pulse (foldlM')
import Data.Sequence.Strict (StrictSeq)
import qualified Data.Sequence.Strict as SS (fromList)
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Vector (Vector, fromList, (!))
import qualified Data.Vector as Vector (length)
import Data.Word (Word64)
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Ast (
  Pred (..),
  RootTarget (..),
  Subst (..),
  Term (..),
  emptySubst,
  runTarget,
  runTerm,
  substPredWithVarTest,
  substToEnv,
 )
import Test.Cardano.Ledger.Constrained.Combinators (genFromMap, itemFromSet, suchThatErr)
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Monad (Typed (..), runTyped)
import Test.Cardano.Ledger.Constrained.Preds.CertState (
  dstateStage,
  pstateStage,
  vstateStage,
 )
import Test.Cardano.Ledger.Constrained.Preds.LedgerState (ledgerStateStage)
import Test.Cardano.Ledger.Constrained.Preds.NewEpochState (epochStateStage, newEpochStateStage)
import Test.Cardano.Ledger.Constrained.Preds.PParams (pParamsStage)
import Test.Cardano.Ledger.Constrained.Preds.UTxO (utxoStage)
import Test.Cardano.Ledger.Constrained.Preds.Universes (universeStage)
import Test.Cardano.Ledger.Constrained.Rewrite (
  DependGraph (..),
  OrderInfo,
  initialOrder,
  mkDependGraph,
  notBefore,
  rewriteGen,
 )
import Test.Cardano.Ledger.Constrained.Solver (solveOneVar)
import Test.Cardano.Ledger.Constrained.Vars (currentSlot, newEpochStateT)
import Test.Cardano.Ledger.Generic.MockChain (MOCKCHAIN, MockBlock (..), MockChainState (..))
import Test.Cardano.Ledger.Generic.PrettyCore (
  pcSlotNo,
  pcTx,
  ppInt,
  ppList,
  ppPair,
  ppStrictSeq,
  psNewEpochState,
  summaryMapCompact,
 )
import Test.Cardano.Ledger.Generic.Proof hiding (lift)
import Test.Cardano.Ledger.Generic.Trace (chooseIssuer)
import Test.Cardano.Ledger.Shelley.Utils (applySTSTest, runShelleyBase, testGlobals)
import Test.Control.State.Transition.Trace (
  Trace (..),
  TraceOrder (OldestFirst),
  lastState,
  traceInitState,
  traceSignals,
  traceStates,
 )
import Test.Control.State.Transition.Trace.Generator.QuickCheck (
  HasTrace (..),
  shrinkTrace,
  traceFromInitState,
 )
import Test.Tasty.QuickCheck

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

data TraceState era = TraceState !Int !(Env era)

newtype TraceM era x = TraceM (StateT (TraceState era) (ExceptT [String] Gen) x)
  deriving (forall a b. a -> TraceM era b -> TraceM era a
forall a b. (a -> b) -> TraceM era a -> TraceM era b
forall era a b. a -> TraceM era b -> TraceM era a
forall era a b. (a -> b) -> TraceM era a -> TraceM era b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: forall a b. a -> TraceM era b -> TraceM era a
$c<$ :: forall era a b. a -> TraceM era b -> TraceM era a
fmap :: forall a b. (a -> b) -> TraceM era a -> TraceM era b
$cfmap :: forall era a b. (a -> b) -> TraceM era a -> TraceM era b
Functor, forall era. Functor (TraceM era)
forall a. a -> TraceM era a
forall era a. a -> TraceM era a
forall a b. TraceM era a -> TraceM era b -> TraceM era a
forall a b. TraceM era a -> TraceM era b -> TraceM era b
forall a b. TraceM era (a -> b) -> TraceM era a -> TraceM era b
forall era a b. TraceM era a -> TraceM era b -> TraceM era a
forall era a b. TraceM era a -> TraceM era b -> TraceM era b
forall era a b. TraceM era (a -> b) -> TraceM era a -> TraceM era b
forall a b c.
(a -> b -> c) -> TraceM era a -> TraceM era b -> TraceM era c
forall era a b c.
(a -> b -> c) -> TraceM era a -> TraceM era b -> TraceM era c
forall (f :: * -> *).
Functor f
-> (forall a. a -> f a)
-> (forall a b. f (a -> b) -> f a -> f b)
-> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
-> (forall a b. f a -> f b -> f b)
-> (forall a b. f a -> f b -> f a)
-> Applicative f
<* :: forall a b. TraceM era a -> TraceM era b -> TraceM era a
$c<* :: forall era a b. TraceM era a -> TraceM era b -> TraceM era a
*> :: forall a b. TraceM era a -> TraceM era b -> TraceM era b
$c*> :: forall era a b. TraceM era a -> TraceM era b -> TraceM era b
liftA2 :: forall a b c.
(a -> b -> c) -> TraceM era a -> TraceM era b -> TraceM era c
$cliftA2 :: forall era a b c.
(a -> b -> c) -> TraceM era a -> TraceM era b -> TraceM era c
<*> :: forall a b. TraceM era (a -> b) -> TraceM era a -> TraceM era b
$c<*> :: forall era a b. TraceM era (a -> b) -> TraceM era a -> TraceM era b
pure :: forall a. a -> TraceM era a
$cpure :: forall era a. a -> TraceM era a
Applicative, forall era. Applicative (TraceM era)
forall a. a -> TraceM era a
forall era a. a -> TraceM era a
forall a b. TraceM era a -> TraceM era b -> TraceM era b
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall era a b. TraceM era a -> TraceM era b -> TraceM era b
forall era a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *).
Applicative m
-> (forall a b. m a -> (a -> m b) -> m b)
-> (forall a b. m a -> m b -> m b)
-> (forall a. a -> m a)
-> Monad m
return :: forall a. a -> TraceM era a
$creturn :: forall era a. a -> TraceM era a
>> :: forall a b. TraceM era a -> TraceM era b -> TraceM era b
$c>> :: forall era a b. TraceM era a -> TraceM era b -> TraceM era b
>>= :: forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
$c>>= :: forall era a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
Monad)

runTraceM :: Int -> Env era -> TraceM era a -> Gen (a, Int, Env era)
runTraceM :: forall era a.
Int -> Env era -> TraceM era a -> Gen (a, Int, Env era)
runTraceM Int
n Env era
env (TraceM StateT (TraceState era) (ExceptT [String] Gen) a
x) = do
  Either [String] (a, TraceState era)
y <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT (TraceState era) (ExceptT [String] Gen) a
x (forall era. Int -> Env era -> TraceState era
TraceState Int
n Env era
env))
  case Either [String] (a, TraceState era)
y of
    Left [String]
xs -> forall a. HasCallStack => String -> a
error ([String] -> String
unlines [String]
xs)
    Right (a
z, TraceState Int
i Env era
s) -> forall (f :: * -> *) a. Applicative f => a -> f a
pure (a
z, Int
i, Env era
s)

fstTriple :: (a, b, c) -> a
fstTriple :: forall a b c. (a, b, c) -> a
fstTriple = (\(a
p, b
_, c
_) -> a
p)

toGen :: TraceM era a -> Gen a
toGen :: forall era a. TraceM era a -> Gen a
toGen TraceM era a
ax = forall a b c. (a, b, c) -> a
fstTriple forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall era a.
Int -> Env era -> TraceM era a -> Gen (a, Int, Env era)
runTraceM Int
0 forall era. Env era
emptyEnv TraceM era a
ax

failTrace :: [String] -> TraceM era a
failTrace :: forall era a. [String] -> TraceM era a
failTrace [String]
ss = forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE [String]
ss))

instance MonadFail (TraceM era) where
  fail :: forall a. String -> TraceM era a
fail String
err = forall era a. [String] -> TraceM era a
failTrace [String
err]

-- ==============================
-- Lift a (Type era a) to (TraceM era a)

liftTyped :: Typed a -> TraceM era a
liftTyped :: forall a era. Typed a -> TraceM era a
liftTyped Typed a
x = do
  case forall x. Typed x -> Either [String] x
runTyped Typed a
x of
    Left [String]
ss -> forall era a. [String] -> TraceM era a
failTrace [String]
ss
    Right a
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a

liftGen :: Gen a -> TraceM era a
liftGen :: forall a era. Gen a -> TraceM era a
liftGen Gen a
g = forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift Gen a
g))

getEnv :: TraceM era (Env era)
getEnv :: forall era. TraceM era (Env era)
getEnv = forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM (forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state (\s :: TraceState era
s@(TraceState Int
_ !Env era
e) -> (Env era
e, TraceState era
s)))

getCount :: TraceM era Int
getCount :: forall era. TraceM era Int
getCount = forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM (forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state (\s :: TraceState era
s@(TraceState !Int
i Env era
_) -> (Int
i, TraceState era
s)))

putEnv :: Env era -> TraceM era (Env era)
putEnv :: forall era. Env era -> TraceM era (Env era)
putEnv Env era
env = forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM (forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state (\(TraceState Int
i Env era
_) -> (Env era
env, forall era. Int -> Env era -> TraceState era
TraceState Int
i Env era
env)))

putCount :: Int -> TraceM era ()
putCount :: forall era. Int -> TraceM era ()
putCount Int
i = forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM (forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state (\(TraceState Int
_ !Env era
e) -> ((), forall era. Int -> Env era -> TraceState era
TraceState Int
i Env era
e)))

liftCounter :: ((Int, a) -> Gen (Int, b)) -> a -> TraceM era b
liftCounter :: forall a b era. ((Int, a) -> Gen (Int, b)) -> a -> TraceM era b
liftCounter (Int, a) -> Gen (Int, b)
f a
a = do
  !Int
i <- forall era. TraceM era Int
getCount
  (!Int
j, !b
b) <- forall a era. Gen a -> TraceM era a
liftGen ((Int, a) -> Gen (Int, b)
f (Int
i, a
a))
  forall era. Int -> TraceM era ()
putCount Int
j
  forall (f :: * -> *) a. Applicative f => a -> f a
pure b
b

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

-- | Lookup the value of a Term in the Env internal to TraceM.
getTerm :: Term era a -> TraceM era a
getTerm :: forall era a. Term era a -> TraceM era a
getTerm Term era a
term = do
  Env era
env <- forall era. TraceM era (Env era)
getEnv
  case forall x. Typed x -> Either [String] x
runTyped (forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
term) of
    Right a
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
    Left [String]
ss -> forall era a. [String] -> TraceM era a
failTrace ([String]
ss forall a. [a] -> [a] -> [a]
++ [String
"in call to (getTerm " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term era a
term forall a. [a] -> [a] -> [a]
++ String
")"])

getTarget :: RootTarget era r a -> TraceM era a
getTarget :: forall era r a. RootTarget era r a -> TraceM era a
getTarget RootTarget era r a
tar = do
  Env era
env <- forall era. TraceM era (Env era)
getEnv
  case forall x. Typed x -> Either [String] x
runTyped (forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env RootTarget era r a
tar) of
    Right a
a -> forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
    Left [String]
ss -> forall era a. [String] -> TraceM era a
failTrace ([String]
ss forall a. [a] -> [a] -> [a]
++ [String
"in call to (getTarget " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show RootTarget era r a
tar forall a. [a] -> [a] -> [a]
++ String
")"])

-- | Pick a random (key,value) pair from a Map
fromMapTerm :: Term era (Map k a) -> TraceM era (k, a)
fromMapTerm :: forall era k a. Term era (Map k a) -> TraceM era (k, a)
fromMapTerm Term era (Map k a)
term = do
  Map k a
u <- forall era a. Term era a -> TraceM era a
getTerm Term era (Map k a)
term
  forall a era. Gen a -> TraceM era a
liftGen forall a b. (a -> b) -> a -> b
$ forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"fromMapTerm " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term era (Map k a)
term] Map k a
u

-- | Pick a random (key,value) pair from a Map such that the (key,value) pair meets predicate 'p'
fromMapTermSuchThat :: Term era (Map k a) -> ((k, a) -> Bool) -> TraceM era (k, a)
fromMapTermSuchThat :: forall era k a.
Term era (Map k a) -> ((k, a) -> Bool) -> TraceM era (k, a)
fromMapTermSuchThat Term era (Map k a)
term (k, a) -> Bool
p = do
  Map k a
u <- forall era a. Term era a -> TraceM era a
getTerm Term era (Map k a)
term
  let n :: Int
n = forall k a. Map k a -> Int
Map.size Map k a
u
  forall a era. Gen a -> TraceM era a
liftGen forall a b. (a -> b) -> a -> b
$
    forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr
      [String
"suchThatErr call (fromMapTermSuchThat " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term era (Map k a)
term forall a. [a] -> [a] -> [a]
++ String
" size = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n]
      (forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"fromMapTerm " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term era (Map k a)
term] Map k a
u)
      (k, a) -> Bool
p

-- | Pick a random element from a Set
fromSetTerm :: Term era (Set b) -> TraceM era b
fromSetTerm :: forall era b. Term era (Set b) -> TraceM era b
fromSetTerm Term era (Set b)
term = do
  Set b
u <- forall era a. Term era a -> TraceM era a
getTerm Term era (Set b)
term
  forall a era. Gen a -> TraceM era a
liftGen (forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet [String
"fromSetTerm " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Term era (Set b)
term] Set b
u))

-- | Update the Env internal to TraceM.
update :: (Env era -> TraceM era (Env era)) -> TraceM era ()
update :: forall era. (Env era -> TraceM era (Env era)) -> TraceM era ()
update Env era -> TraceM era (Env era)
f = forall era. TraceM era (Env era)
getEnv forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Env era -> TraceM era (Env era)
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era. Env era -> TraceM era (Env era)
putEnv forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Update the value of one variable stored in the Env internal to TraceM.
updateVar :: Term era t -> (t -> t) -> TraceM era ()
updateVar :: forall era t. Term era t -> (t -> t) -> TraceM era ()
updateVar term :: Term era t
term@(Var V era t
v) t -> t
adjust = forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM forall a b. (a -> b) -> a -> b
$ do
  TraceState Int
i Env era
env <- forall (m :: * -> *) s. Monad m => StateT s m s
get
  case forall x. Typed x -> Either [String] x
runTyped (forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
term) of
    Right t
valA -> forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (forall era. Int -> Env era -> TraceState era
TraceState Int
i (forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v (t -> t
adjust t
valA) Env era
env))
    Left [String]
ss -> forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ([String]
ss forall a. [a] -> [a] -> [a]
++ [String
"in call to 'updateVar'"]))
updateVar Term era t
term t -> t
_ = forall era a. [String] -> TraceM era a
failTrace [String
"Non Var term in call to 'updateVar'", forall a. Show a => a -> String
show Term era t
term]

setVar :: Term era t -> t -> TraceM era ()
setVar :: forall era t. Term era t -> t -> TraceM era ()
setVar (Var V era t
v) t
t = forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM forall a b. (a -> b) -> a -> b
$ do
  TraceState Int
i Env era
env <- forall (m :: * -> *) s. Monad m => StateT s m s
get
  forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (forall era. Int -> Env era -> TraceState era
TraceState Int
i (forall era t. V era t -> t -> Env era -> Env era
storeVar V era t
v t
t Env era
env))
setVar Term era t
term t
_ = forall era a. [String] -> TraceM era a
failTrace [String
"Non Var term in call to 'setVar'", forall a. Show a => a -> String
show Term era t
term]

-- ============================================================================
-- A few helper functions that need to do different things in different Eras.

refInputs :: Proof era -> TxBody era -> Set (TxIn (EraCrypto era))
refInputs :: forall era. Proof era -> TxBody era -> Set (TxIn (EraCrypto era))
refInputs Proof era
Shelley TxBody era
_ = forall a. Set a
Set.empty
refInputs Proof era
Allegra TxBody era
_ = forall a. Set a
Set.empty
refInputs Proof era
Mary TxBody era
_ = forall a. Set a
Set.empty
refInputs Proof era
Alonzo TxBody era
_ = forall a. Set a
Set.empty
refInputs Proof era
Babbage TxBody era
txb = TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
referenceInputsTxBodyL
refInputs Proof era
Conway TxBody era
txb = TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
BabbageEraTxBody era =>
Lens' (TxBody era) (Set (TxIn (EraCrypto era)))
referenceInputsTxBodyL

reqSig :: Proof era -> TxBody era -> Set (KeyHash 'Witness (EraCrypto era))
reqSig :: forall era.
Proof era -> TxBody era -> Set (KeyHash 'Witness (EraCrypto era))
reqSig Proof era
Shelley TxBody era
_ = forall a. Set a
Set.empty
reqSig Proof era
Allegra TxBody era
_ = forall a. Set a
Set.empty
reqSig Proof era
Mary TxBody era
_ = forall a. Set a
Set.empty
reqSig Proof era
Alonzo TxBody era
_ = forall a. Set a
Set.empty
reqSig Proof era
Babbage TxBody era
txb = TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (Set (KeyHash 'Witness (EraCrypto era)))
reqSignerHashesTxBodyL
reqSig Proof era
Conway TxBody era
txb = TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (Set (KeyHash 'Witness (EraCrypto era)))
reqSignerHashesTxBodyL

-- =======================================================================================
-- Code to run the standard [Pred era] found in the Preds directory in the TraceM monad
-- First code to compile in the TraceM monad, and then use the compiled version to run
-- the solver in the TraceM monad

-- | Compile [Pred era] in the TraceM monad
--   First: Apply the Rewriter
--   Second: appy the Subst
--   Third: Construct the DependGraph
compileTraceWithSubst ::
  Era era => OrderInfo -> Subst era -> [Pred era] -> TraceM era (DependGraph era)
compileTraceWithSubst :: forall era.
Era era =>
OrderInfo
-> Subst era -> [Pred era] -> TraceM era (DependGraph era)
compileTraceWithSubst OrderInfo
info Subst era
subst0 [Pred era]
cs0 = do
  [Pred era]
simple <- forall a b era. ((Int, a) -> Gen (Int, b)) -> a -> TraceM era b
liftCounter forall era. Era era => (Int, [Pred era]) -> Gen (Int, [Pred era])
rewriteGen [Pred era]
cs0
  DependGraph era
graph <- forall a era. Typed a -> TraceM era a
liftTyped forall a b. (a -> b) -> a -> b
$ do
    let instanPreds :: [Pred era]
instanPreds = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall era. Subst era -> Pred era -> Pred era
substPredWithVarTest Subst era
subst0) [Pred era]
simple
    [Name era]
orderedNames <- forall era. Era era => OrderInfo -> [Pred era] -> Typed [Name era]
initialOrder OrderInfo
info [Pred era]
instanPreds
    forall era.
Era era =>
Int
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name era]
orderedNames) [] forall a. HashSet a
HashSet.empty [Name era]
orderedNames [] forall a b. (a -> b) -> a -> b
$
      forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter forall era. Pred era -> Bool
notBefore [Pred era]
instanPreds
  forall (f :: * -> *) a. Applicative f => a -> f a
pure DependGraph era
graph

-- | Use the tool chain to generate a Subst from a list of Pred, in the TraceM monad.
toolChainTrace ::
  Era era => Proof era -> OrderInfo -> [Pred era] -> Subst era -> TraceM era (Subst era)
toolChainTrace :: forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> TraceM era (Subst era)
toolChainTrace Proof era
_proof OrderInfo
order [Pred era]
cs Subst era
subst0 = do
  (DependGraph [([Name era], [Pred era])]
pairs) <- forall era.
Era era =>
OrderInfo
-> Subst era -> [Pred era] -> TraceM era (DependGraph era)
compileTraceWithSubst OrderInfo
order Subst era
subst0 [Pred era]
cs
  Subst Map String (SubstElem era)
subst <- forall a era. Gen a -> TraceM era a
liftGen (forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' forall era.
Era era =>
Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
solveOneVar Subst era
subst0 [([Name era], [Pred era])]
pairs)
  let isTempV :: t Char -> Bool
isTempV t Char
k = Bool -> Bool
not (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
'.' t Char
k)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (forall era. Map String (SubstElem era) -> Subst era
Subst (forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\String
k SubstElem era
_ -> forall {t :: * -> *}. Foldable t => t Char -> Bool
isTempV String
k) Map String (SubstElem era)
subst))

-- =====================================================================
-- Lift some [Pred era] into TraceM (monadic) (Subst era) transformers
-- Create tool (TraceM era (Subst era)) functions that can be chained together

universeTrace :: Reflect era => Proof era -> Subst era -> TraceM era (Subst era)
universeTrace :: forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
universeTrace Proof era
proof Subst era
subst = forall a era. Gen a -> TraceM era a
liftGen (forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage forall a. Default a => a
def Proof era
proof Subst era
subst)

pparamsTrace :: Reflect era => Proof era -> Subst era -> TraceM era (Subst era)
pparamsTrace :: forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
pparamsTrace Proof era
proof Subst era
subst = forall a era. Gen a -> TraceM era a
liftGen (forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof Subst era
subst)

utxoTrace :: Reflect era => Proof era -> Subst era -> TraceM era (Subst era)
utxoTrace :: forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
utxoTrace Proof era
proof Subst era
subst = forall a era. Gen a -> TraceM era a
liftGen (forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage forall a. Default a => a
def Proof era
proof Subst era
subst)

pstateTrace :: Reflect era => Proof era -> Subst era -> TraceM era (Subst era)
pstateTrace :: forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
pstateTrace Proof era
proof Subst era
subst = forall a era. Gen a -> TraceM era a
liftGen (forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof era
proof Subst era
subst)

vstateTrace :: Reflect era => Proof era -> Subst era -> TraceM era (Subst era)
vstateTrace :: forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
vstateTrace Proof era
proof Subst era
subst = forall a era. Gen a -> TraceM era a
liftGen (forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof era
proof Subst era
subst)

dstateTrace :: Reflect era => Proof era -> Subst era -> TraceM era (Subst era)
dstateTrace :: forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
dstateTrace Proof era
proof Subst era
subst = forall a era. Gen a -> TraceM era a
liftGen (forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof era
proof Subst era
subst)

ledgerStateTrace :: Reflect era => Proof era -> Subst era -> TraceM era (Subst era)
ledgerStateTrace :: forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
ledgerStateTrace Proof era
proof Subst era
subst = forall a era. Gen a -> TraceM era a
liftGen (forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage forall a. Default a => a
def Proof era
proof Subst era
subst)

epochStateTrace :: Reflect era => Proof era -> Subst era -> TraceM era (Subst era)
epochStateTrace :: forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
epochStateTrace Proof era
proof Subst era
subst = forall a era. Gen a -> TraceM era a
liftGen (forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
epochStateStage Proof era
proof Subst era
subst)

newEpochStateTrace :: Reflect era => Proof era -> Subst era -> TraceM era (Subst era)
newEpochStateTrace :: forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
newEpochStateTrace Proof era
proof Subst era
subst = forall a era. Gen a -> TraceM era a
liftGen (forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
newEpochStateStage Proof era
proof Subst era
subst)

-- ==============================================================
-- Code to make Traces

-- | Iterate a function 'make' to make a trace of length 'n'. Each call to 'make' gets the
--   most recent value of the Env internal to TraceM. The function 'make' is
--   supposed to compute 'a', and (possibly) update the Env internal to TraceM.
makeTrace :: Int -> TraceM era a -> TraceM era [(Env era, a)]
makeTrace :: forall era a. Int -> TraceM era a -> TraceM era [(Env era, a)]
makeTrace Int
0 TraceM era a
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
makeTrace Int
n TraceM era a
make = do
  Env era
env0 <- forall era. TraceM era (Env era)
getEnv
  a
a <- TraceM era a
make
  [(Env era, a)]
xs <- forall era a. Int -> TraceM era a -> TraceM era [(Env era, a)]
makeTrace (Int
n forall a. Num a => a -> a -> a
- Int
1) TraceM era a
make
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Env era
env0, a
a) forall a. a -> [a] -> [a]
: [(Env era, a)]
xs)

data TraceStep era a = TraceStep {forall era a. TraceStep era a -> Env era
tsBefore :: !(Env era), forall era a. TraceStep era a -> Env era
tsAfter :: !(Env era), forall era a. TraceStep era a -> a
tsA :: !a}

beforeAfterTrace :: Int -> (Int -> TraceM era a) -> TraceM era [TraceStep era a]
beforeAfterTrace :: forall era a.
Int -> (Int -> TraceM era a) -> TraceM era [TraceStep era a]
beforeAfterTrace Int
0 Int -> TraceM era a
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure []
beforeAfterTrace !Int
n Int -> TraceM era a
make = do
  !Env era
beforeEnv <- forall era. TraceM era (Env era)
getEnv
  !a
a <- Int -> TraceM era a
make Int
n
  !Env era
afterEnv <- forall era. TraceM era (Env era)
getEnv
  [TraceStep era a]
xs <- forall era a.
Int -> (Int -> TraceM era a) -> TraceM era [TraceStep era a]
beforeAfterTrace (Int
n forall a. Num a => a -> a -> a
- Int
1) Int -> TraceM era a
make
  let !ans :: [TraceStep era a]
ans = TraceStep {tsBefore :: Env era
tsBefore = Env era
beforeEnv, tsAfter :: Env era
tsAfter = Env era
afterEnv, tsA :: a
tsA = a
a} forall a. a -> [a] -> [a]
: [TraceStep era a]
xs
  forall (f :: * -> *) a. Applicative f => a -> f a
pure [TraceStep era a]
ans

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

-- | Generate an Env that contains the pieces of the LedgerState
--   by chaining smaller pieces together.
genLedgerStateEnv :: Reflect era => Proof era -> TraceM era (Env era)
genLedgerStateEnv :: forall era. Reflect era => Proof era -> TraceM era (Env era)
genLedgerStateEnv Proof era
proof = do
  Subst era
subst <-
    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 -> TraceM era (Subst era)
pparamsTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
universeTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
utxoTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
vstateTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
pstateTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
dstateTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
ledgerStateTrace Proof era
proof
  Env era
env <- forall a era. Typed a -> TraceM era a
liftTyped (forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv)
  forall era. Env era -> TraceM era (Env era)
putEnv Env era
env

-- | Generate an Env that contains the pieces of the NewEpochState
--   by chaining smaller pieces together.
genNewEpochStateEnv :: Reflect era => Proof era -> TraceM era (Env era)
genNewEpochStateEnv :: forall era. Reflect era => Proof era -> TraceM era (Env era)
genNewEpochStateEnv Proof era
proof = do
  Subst era
subst <-
    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 -> TraceM era (Subst era)
pparamsTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
universeTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
utxoTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
vstateTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
pstateTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
dstateTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
ledgerStateTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
epochStateTrace Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
newEpochStateTrace Proof era
proof
  Env era
env <- forall a era. Typed a -> TraceM era a
liftTyped (forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv)
  forall era. Env era -> TraceM era (Env era)
putEnv Env era
env

-- ======================================================================
-- Using traces by running the MOCKCHAIN STS instance
-- ======================================================================

-- | How we encode a trace, when we run STS of (MOCKCHAIN era)
data PredGen era = PredGen (Vector (StrictSeq (Tx era), SlotNo)) (Env era)

instance Reflect era => Show (PredGen era) where
  show :: PredGen era -> String
show (PredGen Vector (StrictSeq (Tx era), SlotNo)
xs Env era
_) = forall a. Show a => a -> String
show (forall x ann. (x -> Doc ann) -> [x] -> Doc ann
ppList (forall t1 t2.
(t1 -> Doc Ann) -> (t2 -> Doc Ann) -> (t1, t2) -> Doc Ann
ppPair (forall a ann. (a -> Doc ann) -> StrictSeq a -> Doc ann
ppStrictSeq (forall era. Proof era -> Tx era -> Doc Ann
pcTx forall era. Reflect era => Proof era
reify)) (SlotNo -> Doc Ann
pcSlotNo)) (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Vector (StrictSeq (Tx era), SlotNo)
xs))

instance
  ( STS (MOCKCHAIN era)
  , Reflect era
  ) =>
  HasTrace (MOCKCHAIN era) (PredGen era)
  where
  type BaseEnv (MOCKCHAIN era) = Globals

  interpretSTS :: forall a.
HasCallStack =>
BaseEnv (MOCKCHAIN era) -> BaseM (MOCKCHAIN era) a -> a
interpretSTS BaseEnv (MOCKCHAIN era)
globals BaseM (MOCKCHAIN era) a
act = forall a. Identity a -> a
runIdentity forall a b. (a -> b) -> a -> b
$ forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT BaseM (MOCKCHAIN era) a
act BaseEnv (MOCKCHAIN era)
globals

  envGen :: HasCallStack => PredGen era -> Gen (Environment (MOCKCHAIN era))
envGen PredGen era
_gstate = forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  sigGen :: HasCallStack =>
PredGen era
-> Environment (MOCKCHAIN era)
-> State (MOCKCHAIN era)
-> Gen (Signal (MOCKCHAIN era))
sigGen (PredGen Vector (StrictSeq (Tx era), SlotNo)
txss Env era
_) () mcs :: State (MOCKCHAIN era)
mcs@(MockChainState NewEpochState era
newepoch NewEpochState era
_ (SlotNo Word64
lastSlot) Int
count) = do
    let NewEpochState EpochNo
epochnum BlocksMade (EraCrypto era)
_ BlocksMade (EraCrypto era)
_ EpochState era
_epochstate StrictMaybe (PulsingRewUpdate (EraCrypto era))
_ PoolDistr (EraCrypto era)
pooldistr StashedAVVMAddresses era
_ = NewEpochState era
newepoch
    KeyHash 'StakePool StandardCrypto
issuerkey <- forall c.
EpochNo
-> Word64 -> Int -> PoolDistr c -> Gen (KeyHash 'StakePool c)
chooseIssuer EpochNo
epochnum Word64
lastSlot Int
count PoolDistr (EraCrypto era)
pooldistr
    let (StrictSeq (Tx era)
txs, SlotNo
nextSlotNo) = Vector (StrictSeq (Tx era), SlotNo)
txss forall a. Vector a -> Int -> a
! Int
count
    -- Assmble it into a MockBlock
    let mockblock :: MockBlock era
mockblock = forall era.
KeyHash 'StakePool (EraCrypto era)
-> SlotNo -> StrictSeq (Tx era) -> MockBlock era
MockBlock KeyHash 'StakePool StandardCrypto
issuerkey SlotNo
nextSlotNo StrictSeq (Tx era)
txs
    -- Run the STS Rules for MOCKCHAIN with generated signal
    case forall a. ShelleyBase a -> a
runShelleyBase (forall s (m :: * -> *) (rtype :: RuleType).
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s
-> m (Either (NonEmpty (PredicateFailure s)) (State s))
applySTSTest (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC @(MOCKCHAIN era) ((), State (MOCKCHAIN era)
mcs, MockBlock era
mockblock))) of
      Left NonEmpty (PredicateFailure (MOCKCHAIN era))
pdfs ->
        let _txsl :: [Tx era]
_txsl = forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList StrictSeq (Tx era)
txs
         in forall a. HasCallStack => String -> a
error forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines forall a b. (a -> b) -> a -> b
$
              ( String
"FAILS"
                  forall a. a -> [a] -> [a]
: [String
"epochNum " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show EpochNo
epochnum, String
"slot " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Word64
lastSlot]
                  forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Show a => a -> String
show forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Proof era -> Tx era -> Doc Ann
pcTx forall era. Reflect era => Proof era
reify) (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (Tx era)
txs)
                  forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (PredicateFailure (MOCKCHAIN era))
pdfs)
                  forall a. [a] -> [a] -> [a]
++ [forall a. Show a => a -> String
show (forall era.
Reflect era =>
Proof era -> NewEpochState era -> Doc Ann
psNewEpochState forall era. Reflect era => Proof era
reify NewEpochState era
newepoch)]
              )
      Right State (MOCKCHAIN era)
mcs2 -> seq :: forall a b. a -> b -> b
seq State (MOCKCHAIN era)
mcs2 (forall (f :: * -> *) a. Applicative f => a -> f a
pure MockBlock era
mockblock)

  shrinkSignal :: HasCallStack => Signal (MOCKCHAIN era) -> [Signal (MOCKCHAIN era)]
shrinkSignal Signal (MOCKCHAIN era)
_ = []

-- ==================================================
-- Now to run a Property test we need two things
-- 1) An initial (MockChainState newepochstate tickNes slot count)
-- 2) A (PredGen blocks env)
-- We need to generate these together so that the trace is valid, i.e. it passes all the STS rules

genTraceParts ::
  Reflect era =>
  Proof era ->
  Int ->
  (Proof era -> TraceM era (Tx era)) ->
  TraceM
    era
    ( [TraceStep era (Tx era)]
    , Maybe (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era)))
    , PredGen era
    )
genTraceParts :: forall era a.
Reflect era =>
Proof era
-> Int
-> (Proof era -> TraceM era (Tx era))
-> TraceM
     era
     ([TraceStep era (Tx era)],
      Maybe (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era))),
      PredGen era)
genTraceParts Proof era
proof Int
len Proof era -> TraceM era (Tx era)
genTx = do
  Env era
env0 <- forall era. Reflect era => Proof era -> TraceM era (Env era)
genNewEpochStateEnv Proof era
proof
  NewEpochState era
newepochstate <- forall a era. Typed a -> TraceM era a
liftTyped forall a b. (a -> b) -> a -> b
$ forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env0 (forall era.
EraGov era =>
Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
newEpochStateT Proof era
proof)
  SlotNo Word64
currslot <- forall a era. Typed a -> TraceM era a
liftTyped forall a b. (a -> b) -> a -> b
$ forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env0 forall era. Era era => Term era SlotNo
currentSlot
  let initStateFun :: Maybe (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era)))
initStateFun =
        forall a. a -> Maybe a
Just
          ( \(IRC ()) ->
              forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a b. b -> Either a b
Right (forall era.
NewEpochState era
-> NewEpochState era -> SlotNo -> Int -> MockChainState era
MockChainState NewEpochState era
newepochstate NewEpochState era
newepochstate (Word64 -> SlotNo
SlotNo Word64
currslot) Int
0))
          )
  [TraceStep era (Tx era)]
steps <- forall era a.
Int -> (Int -> TraceM era a) -> TraceM era [TraceStep era a]
beforeAfterTrace Int
len (\Int
_ -> Proof era -> TraceM era (Tx era)
genTx Proof era
proof)
  let getTx :: TraceStep era a -> a
getTx (TraceStep Env era
_ Env era
_ a
x) = a
x
  Vector (StrictSeq (Tx era), SlotNo)
zs <- forall step era.
(step -> Tx era)
-> [step]
-> Word64
-> [([Tx era], SlotNo)]
-> TraceM era (Vector (StrictSeq (Tx era), SlotNo))
traceStepToVector forall era a. TraceStep era a -> a
getTx [TraceStep era (Tx era)]
steps (Word64
currslot forall a. Num a => a -> a -> a
+ Word64
1) []
  forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TraceStep era (Tx era)]
steps, Maybe (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era)))
initStateFun, forall era.
Vector (StrictSeq (Tx era), SlotNo) -> Env era -> PredGen era
PredGen Vector (StrictSeq (Tx era), SlotNo)
zs Env era
env0)

traceStepToVector ::
  (step -> Tx era) ->
  [step] ->
  Word64 ->
  [([Tx era], SlotNo)] ->
  TraceM era (Vector (StrictSeq (Tx era), SlotNo))
traceStepToVector :: forall step era.
(step -> Tx era)
-> [step]
-> Word64
-> [([Tx era], SlotNo)]
-> TraceM era (Vector (StrictSeq (Tx era), SlotNo))
traceStepToVector step -> Tx era
_ [] Word64
_ [([Tx era], SlotNo)]
zs = forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. [a] -> Vector a
fromList (forall a. [a] -> [a]
reverse (forall a b. (a -> b) -> [a] -> [b]
map (\([Tx era]
x, SlotNo
y) -> (forall a. [a] -> StrictSeq a
SS.fromList [Tx era]
x, SlotNo
y)) [([Tx era], SlotNo)]
zs)))
traceStepToVector step -> Tx era
getTx [step]
steps Word64
m [([Tx era], SlotNo)]
prev = do
  Int
n <- forall a era. Gen a -> TraceM era a
liftGen forall a b. (a -> b) -> a -> b
$ forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
2)
  let steplist :: [step]
steplist = forall a. Int -> [a] -> [a]
take Int
n [step]
steps
  Word64
nextslot <- forall a era. Gen a -> TraceM era a
liftGen ((forall a. Num a => a -> a -> a
+ Word64
m) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
2, forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
2), (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
3), (Int
1, forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
4)])
  -- Longtraces, with large inter block slot changes may exceed the Maximum validity of
  -- the Validity interval in generated scripts, so try for an average slot difference
  -- less than 3, that should suport Traces up to length 300 since Sized (Range 900 1000)
  -- endSlotDelta, should always be at east 900
  forall step era.
(step -> Tx era)
-> [step]
-> Word64
-> [([Tx era], SlotNo)]
-> TraceM era (Vector (StrictSeq (Tx era), SlotNo))
traceStepToVector step -> Tx era
getTx (forall a. Int -> [a] -> [a]
drop Int
n [step]
steps) Word64
nextslot ((forall a b. (a -> b) -> [a] -> [b]
map step -> Tx era
getTx [step]
steplist, Word64 -> SlotNo
SlotNo Word64
m) forall a. a -> [a] -> [a]
: [([Tx era], SlotNo)]
prev)

-- | Generate a Control.State.Transition.Trace(Trace) from a (TraceM era (Tx era))
newStsTrace ::
  ( Reflect era
  , STS (MOCKCHAIN era)
  ) =>
  Proof era ->
  Int ->
  (Proof era -> TraceM era (Tx era)) ->
  Gen (Trace (MOCKCHAIN era))
newStsTrace :: forall era.
(Reflect era, STS (MOCKCHAIN era)) =>
Proof era
-> Int
-> (Proof era -> TraceM era (Tx era))
-> Gen (Trace (MOCKCHAIN era))
newStsTrace Proof era
proof Int
len Proof era -> TraceM era (Tx era)
genTx = do
  ([TraceStep era (Tx era)]
_, Maybe
  (IRC (MOCKCHAIN era)
   -> Gen
        (Either (NonEmpty (MockChainFailure era)) (MockChainState era)))
initfun, predgen :: PredGen era
predgen@(PredGen Vector (StrictSeq (Tx era), SlotNo)
zs Env era
_)) <- forall era a. TraceM era a -> Gen a
toGen forall a b. (a -> b) -> a -> b
$ forall era a.
Reflect era =>
Proof era
-> Int
-> (Proof era -> TraceM era (Tx era))
-> TraceM
     era
     ([TraceStep era (Tx era)],
      Maybe (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era))),
      PredGen era)
genTraceParts Proof era
proof Int
len Proof era -> TraceM era (Tx era)
genTx
  forall sts traceGenEnv.
(HasTrace sts traceGenEnv, Show (Environment sts), HasCallStack) =>
BaseEnv sts
-> Word64
-> traceGenEnv
-> Maybe
     (IRC sts
      -> Gen (Either (NonEmpty (PredicateFailure sts)) (State sts)))
-> Gen (Trace sts)
traceFromInitState Globals
testGlobals (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Vector a -> Int
Vector.length Vector (StrictSeq (Tx era), SlotNo)
zs forall a. Num a => a -> a -> a
- Int
1)) PredGen era
predgen Maybe
  (IRC (MOCKCHAIN era)
   -> Gen
        (Either (NonEmpty (MockChainFailure era)) (MockChainState era)))
initfun

-- | Create a testable Property from two things
--   1) A function that generates Tx
--   2) A function that creates a property from a (Trace (MOCKCHAIN era))
mockChainProp ::
  forall era.
  (Reflect era, STS (MOCKCHAIN era)) =>
  Proof era ->
  Int ->
  (Proof era -> TraceM era (Tx era)) ->
  (Trace (MOCKCHAIN era) -> Property) ->
  Property
mockChainProp :: forall era.
(Reflect era, STS (MOCKCHAIN era)) =>
Proof era
-> Int
-> (Proof era -> TraceM era (Tx era))
-> (Trace (MOCKCHAIN era) -> Property)
-> Property
mockChainProp Proof era
proof Int
n Proof era -> TraceM era (Tx era)
genTxAndUpdateEnv Trace (MOCKCHAIN era) -> Property
propf = do
  let genTrace :: Gen (Trace (MOCKCHAIN era))
genTrace = forall era.
(Reflect era, STS (MOCKCHAIN era)) =>
Proof era
-> Int
-> (Proof era -> TraceM era (Tx era))
-> Gen (Trace (MOCKCHAIN era))
newStsTrace Proof era
proof Int
n Proof era -> TraceM era (Tx era)
genTxAndUpdateEnv
  forall prop a.
Testable prop =>
Gen a -> (a -> [a]) -> (a -> prop) -> Property
forAllShrinkBlind
    Gen (Trace (MOCKCHAIN era))
genTrace
    ( if Bool
False
        then forall sts traceGenEnv.
HasTrace sts traceGenEnv =>
BaseEnv sts -> Trace sts -> [Trace sts]
shrinkTrace @(MOCKCHAIN era) @(PredGen era) Globals
testGlobals
        else (\Trace (MOCKCHAIN era)
_ -> [])
    )
    Trace (MOCKCHAIN era) -> Property
propf

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

-- | Given trace [(sig0,state0),(sig1,state1),(sig2,state2),(sig3,state3)]
--   conjoin [p pstate0 sig1 state1, p state0 sig2 state2, p state0 sig3 state3]
-- test that 'p' holds between state0 and stateN for all N
stepProp ::
  (MockChainState era -> MockBlock era -> MockChainState era -> Property) ->
  (Trace (MOCKCHAIN era) -> Property)
stepProp :: forall era.
(MockChainState era
 -> MockBlock era -> MockChainState era -> Property)
-> Trace (MOCKCHAIN era) -> Property
stepProp MockChainState era
-> MockBlock era -> MockChainState era -> Property
p Trace (MOCKCHAIN era)
tr = case forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (MockChainState era
-> MockBlock era -> MockChainState era -> Property
p MockChainState era
state0) [Signal (MOCKCHAIN era)]
sigs [State (MOCKCHAIN era)]
states of
  [] -> forall prop. Testable prop => prop -> Property
property Bool
True
  (Property
_ : [Property]
more) -> forall prop. Testable prop => [prop] -> Property
conjoin [Property]
more
  where
    state0 :: MockChainState era
state0 = Trace (MOCKCHAIN era)
tr forall s a. s -> Getting a s a -> a
^. forall s. Lens' (Trace s) (State s)
traceInitState
    states :: [State (MOCKCHAIN era)]
states = forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace (MOCKCHAIN era)
tr
    sigs :: [Signal (MOCKCHAIN era)]
sigs = forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace (MOCKCHAIN era)
tr

-- | Given trace [(sig0,state0),(sig1,state1),(sig2,state2),(sig3,state3)]
--   conjoin [p pstate0 sig1 state1, p state1 sig2 state2, p state2 sig3 state3]
--   test that 'p' holds bteween (state0 stateN sig(N+1) state(N+1) for all N
deltaProp ::
  (MockChainState era -> MockBlock era -> MockChainState era -> Property) ->
  Trace (MOCKCHAIN era) ->
  Property
deltaProp :: forall era.
(MockChainState era
 -> MockBlock era -> MockChainState era -> Property)
-> Trace (MOCKCHAIN era) -> Property
deltaProp MockChainState era
-> MockBlock era -> MockChainState era -> Property
p Trace (MOCKCHAIN era)
tr = case [State (MOCKCHAIN era)]
states of
  [] -> forall prop. Testable prop => prop -> Property
property Bool
True
  State (MOCKCHAIN era)
_ : [State (MOCKCHAIN era)]
more -> forall prop. Testable prop => [prop] -> Property
conjoin (forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 MockChainState era
-> MockBlock era -> MockChainState era -> Property
p [State (MOCKCHAIN era)]
states [Signal (MOCKCHAIN era)]
sigs [State (MOCKCHAIN era)]
more)
  where
    states :: [State (MOCKCHAIN era)]
states = forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace (MOCKCHAIN era)
tr
    sigs :: [Signal (MOCKCHAIN era)]
sigs = forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace (MOCKCHAIN era)
tr

-- | Given trace [(sig0,state0),(sig1,state1),(sig2,state2),(sig3,state3)]
--   test that (p state0 stateN),  where stateN is the last state in the trace
preserveProp ::
  (MockChainState era -> MockChainState era -> Property) -> (Trace (MOCKCHAIN era) -> Property)
preserveProp :: forall era.
(MockChainState era -> MockChainState era -> Property)
-> Trace (MOCKCHAIN era) -> Property
preserveProp MockChainState era -> MockChainState era -> Property
p Trace (MOCKCHAIN era)
tr = MockChainState era -> MockChainState era -> Property
p MockChainState era
state0 State (MOCKCHAIN era)
stateN
  where
    state0 :: MockChainState era
state0 = Trace (MOCKCHAIN era)
tr forall s a. s -> Getting a s a -> a
^. forall s. Lens' (Trace s) (State s)
traceInitState
    stateN :: State (MOCKCHAIN era)
stateN = forall s. Trace s -> State s
lastState Trace (MOCKCHAIN era)
tr

-- | Apply '(preserveProp p)' to each full Epoch in a Trace. A partial epoch at the end of
-- the trace is not tested.
epochProp ::
  ConwayEraGov era =>
  (MockChainState era -> MockChainState era -> Property) ->
  (Trace (MOCKCHAIN era) -> Property)
epochProp :: forall era.
ConwayEraGov era =>
(MockChainState era -> MockChainState era -> Property)
-> Trace (MOCKCHAIN era) -> Property
epochProp MockChainState era -> MockChainState era -> Property
p Trace (MOCKCHAIN era)
tr =
  forall prop. Testable prop => String -> prop -> Property
counterexample String
message forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => [prop] -> Property
conjoin (forall a b. (a -> b) -> [a] -> [b]
map (\NonEmpty (MockChainState era)
epoch -> (MockChainState era -> MockChainState era -> Property
p (forall a. NonEmpty a -> a
NE.head NonEmpty (MockChainState era)
epoch) (forall a. NonEmpty a -> a
NE.last NonEmpty (MockChainState era)
epoch))) [NonEmpty (MockChainState era)]
epochs)
  where
    states :: [State (MOCKCHAIN era)]
states = forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace (MOCKCHAIN era)
tr
    epochs :: [NonEmpty (MockChainState era)]
epochs = forall era. [MockChainState era] -> [NonEmpty (MockChainState era)]
splitEpochs [State (MOCKCHAIN era)]
states
    showEpoch :: NonEmpty (MockChainState era) -> a -> String
showEpoch NonEmpty (MockChainState era)
epoch a
n = [String] -> String
unlines ((String
"EPOCH " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show a
n) forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map forall era. ConwayEraGov era => MockChainState era -> String
showPulserState (forall a. NonEmpty a -> [a]
NE.toList NonEmpty (MockChainState era)
epoch))
    message :: String
message =
      [String] -> String
unlines ((String
"Trace length " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall (t :: * -> *) a. Foldable t => t a -> Int
length [State (MOCKCHAIN era)]
states)) forall a. a -> [a] -> [a]
: forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall {era} {a}.
(ConwayEraGov era, Show a) =>
NonEmpty (MockChainState era) -> a -> String
showEpoch [NonEmpty (MockChainState era)]
epochs [Int
0 :: Int ..])

splitEpochs :: [MockChainState era] -> [NE.NonEmpty (MockChainState era)]
splitEpochs :: forall era. [MockChainState era] -> [NonEmpty (MockChainState era)]
splitEpochs [MockChainState era]
xs =
  -- We only want full traces, so we drop the last potential trace
  forall a. [a] -> [a]
reverse forall a b. (a -> b) -> a -> b
$ forall a. Int -> [a] -> [a]
drop Int
1 forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
reverse (forall a. [a] -> [a]
removeFirst forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
NE.groupBy (forall a. Eq a => a -> a -> Bool
(==) forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (forall era. NewEpochState era -> EpochNo
nesEL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. MockChainState era -> NewEpochState era
mcsNes)) [MockChainState era]
xs)
  where
    -- FIXME: It seems that initialization of DRep pulser is not implemented correctly for
    -- the first trace. Needs investigation and a fix.
    removeFirst :: [a] -> [a]
removeFirst = forall a. Int -> [a] -> [a]
drop Int
1

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

showPulserState :: ConwayEraGov era => MockChainState era -> String
showPulserState :: forall era. ConwayEraGov era => MockChainState era -> String
showPulserState (MockChainState NewEpochState era
nes NewEpochState era
_ SlotNo
slot Int
_) =
  String
"Slot = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show SlotNo
slot forall a. [a] -> [a] -> [a]
++ String
"   " forall a. [a] -> [a] -> [a]
++ forall {era}. DRepPulsingState era -> String
getPulserInfo (NewEpochState era
nes forall s a. s -> Getting a s a -> a
^. forall era.
ConwayEraGov era =>
Lens' (NewEpochState era) (DRepPulsingState era)
newEpochStateDRepPulsingStateL)
  where
    getPulserInfo :: DRepPulsingState era -> String
getPulserInfo (DRPulsing DRepPulser era Identity (RatifyState era)
x) =
      String
"Index = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Int -> Doc a
ppInt (forall era ans (m :: * -> *). DRepPulser era m ans -> Int
dpIndex DRepPulser era Identity (RatifyState era)
x))
        forall a. [a] -> [a] -> [a]
++ String
"    DRepDistr = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Map a (CompactForm Coin) -> Doc Ann
summaryMapCompact (forall era ans (m :: * -> *).
DRepPulser era m ans
-> Map (DRep (EraCrypto era)) (CompactForm Coin)
dpDRepDistr DRepPulser era Identity (RatifyState era)
x))
    getPulserInfo (DRComplete PulsingSnapshot era
psnap RatifyState era
_) =
      String
"Complete DRepDistr = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show (forall a. Map a (CompactForm Coin) -> Doc Ann
summaryMapCompact (forall era.
PulsingSnapshot era
-> Map (DRep (EraCrypto era)) (CompactForm Coin)
psDRepDistr PulsingSnapshot era
psnap))