{-# 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.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 (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 -> b) -> TraceM era a -> TraceM era b)
-> (forall a b. a -> TraceM era b -> TraceM era a)
-> Functor (TraceM era)
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
$cfmap :: forall era a b. (a -> b) -> TraceM era a -> TraceM era b
fmap :: forall a b. (a -> b) -> TraceM era a -> TraceM era b
$c<$ :: forall era a b. a -> TraceM era b -> TraceM era a
<$ :: forall a b. a -> TraceM era b -> TraceM era a
Functor, Functor (TraceM era)
Functor (TraceM era) =>
(forall a. a -> TraceM era a)
-> (forall 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 a b. TraceM era a -> TraceM era b -> TraceM era b)
-> (forall a b. TraceM era a -> TraceM era b -> TraceM era a)
-> Applicative (TraceM era)
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
$cpure :: forall era a. a -> TraceM era a
pure :: forall a. a -> TraceM era a
$c<*> :: forall era a b. TraceM era (a -> b) -> TraceM era a -> TraceM era b
<*> :: forall a b. TraceM era (a -> b) -> TraceM era a -> TraceM era b
$cliftA2 :: forall era a b c.
(a -> b -> c) -> TraceM era a -> TraceM era b -> TraceM era c
liftA2 :: forall a b c.
(a -> b -> c) -> TraceM era a -> TraceM era b -> TraceM era c
$c*> :: forall era a b. TraceM era a -> TraceM era b -> TraceM era b
*> :: 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 a
<* :: forall a b. TraceM era a -> TraceM era b -> TraceM era a
Applicative, Applicative (TraceM era)
Applicative (TraceM era) =>
(forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b)
-> (forall a b. TraceM era a -> TraceM era b -> TraceM era b)
-> (forall a. a -> TraceM era a)
-> Monad (TraceM era)
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
$c>>= :: forall era a b. TraceM era a -> (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 -> TraceM era b -> TraceM era b
>> :: forall a b. TraceM era a -> TraceM era b -> TraceM era b
$creturn :: forall era a. a -> TraceM era a
return :: forall a. a -> TraceM era a
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 <- ExceptT [String] Gen (a, TraceState era)
-> Gen (Either [String] (a, TraceState era))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (StateT (TraceState era) (ExceptT [String] Gen) a
-> TraceState era -> ExceptT [String] Gen (a, TraceState era)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT StateT (TraceState era) (ExceptT [String] Gen) a
x (Int -> Env era -> TraceState era
forall era. Int -> Env era -> TraceState era
TraceState Int
n Env era
env))
  case Either [String] (a, TraceState era)
y of
    Left [String]
xs -> String -> Gen (a, Int, Env era)
forall a. HasCallStack => String -> a
error ([String] -> String
unlines [String]
xs)
    Right (a
z, TraceState Int
i Env era
s) -> (a, Int, Env era) -> Gen (a, Int, Env era)
forall a. a -> Gen a
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 = (a, Int, Env era) -> a
forall a b c. (a, b, c) -> a
fstTriple ((a, Int, Env era) -> a) -> Gen (a, Int, Env era) -> Gen a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Env era -> TraceM era a -> Gen (a, Int, Env era)
forall era a.
Int -> Env era -> TraceM era a -> Gen (a, Int, Env era)
runTraceM Int
0 Env era
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 = StateT (TraceState era) (ExceptT [String] Gen) a -> TraceM era a
forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM (ExceptT [String] Gen a
-> StateT (TraceState era) (ExceptT [String] Gen) a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (TraceState era) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ([String] -> ExceptT [String] Gen a
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 = [String] -> TraceM era a
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 Typed a -> Either [String] a
forall x. Typed x -> Either [String] x
runTyped Typed a
x of
    Left [String]
ss -> [String] -> TraceM era a
forall era a. [String] -> TraceM era a
failTrace [String]
ss
    Right a
a -> a -> TraceM era a
forall a. a -> TraceM era 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 = StateT (TraceState era) (ExceptT [String] Gen) a -> TraceM era a
forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM (ExceptT [String] Gen a
-> StateT (TraceState era) (ExceptT [String] Gen) a
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (TraceState era) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Gen a -> ExceptT [String] Gen a
forall (m :: * -> *) a. Monad m => m a -> ExceptT [String] m a
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 = StateT (TraceState era) (ExceptT [String] Gen) (Env era)
-> TraceM era (Env era)
forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM ((TraceState era -> (Env era, TraceState era))
-> StateT (TraceState era) (ExceptT [String] Gen) (Env era)
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 = StateT (TraceState era) (ExceptT [String] Gen) Int
-> TraceM era Int
forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM ((TraceState era -> (Int, TraceState era))
-> StateT (TraceState era) (ExceptT [String] Gen) Int
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 = StateT (TraceState era) (ExceptT [String] Gen) (Env era)
-> TraceM era (Env era)
forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM ((TraceState era -> (Env era, TraceState era))
-> StateT (TraceState era) (ExceptT [String] Gen) (Env era)
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state (\(TraceState Int
i Env era
_) -> (Env era
env, Int -> Env era -> TraceState era
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 = StateT (TraceState era) (ExceptT [String] Gen) () -> TraceM era ()
forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM ((TraceState era -> ((), TraceState era))
-> StateT (TraceState era) (ExceptT [String] Gen) ()
forall (m :: * -> *) s a. Monad m => (s -> (a, s)) -> StateT s m a
state (\(TraceState Int
_ !Env era
e) -> ((), Int -> Env era -> TraceState era
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 <- TraceM era Int
forall era. TraceM era Int
getCount
  (!Int
j, !b
b) <- Gen (Int, b) -> TraceM era (Int, b)
forall a era. Gen a -> TraceM era a
liftGen ((Int, a) -> Gen (Int, b)
f (Int
i, a
a))
  Int -> TraceM era ()
forall era. Int -> TraceM era ()
putCount Int
j
  b -> TraceM era b
forall a. a -> TraceM era a
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 <- TraceM era (Env era)
forall era. TraceM era (Env era)
getEnv
  case Typed a -> Either [String] a
forall x. Typed x -> Either [String] x
runTyped (Env era -> Term era a -> Typed a
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
term) of
    Right a
a -> a -> TraceM era a
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
    Left [String]
ss -> [String] -> TraceM era a
forall era a. [String] -> TraceM era a
failTrace ([String]
ss [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"in call to (getTerm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term era a -> String
forall a. Show a => a -> String
show Term era a
term String -> String -> String
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 <- TraceM era (Env era)
forall era. TraceM era (Env era)
getEnv
  case Typed a -> Either [String] a
forall x. Typed x -> Either [String] x
runTyped (Env era -> RootTarget era r a -> Typed a
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 -> a -> TraceM era a
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
a
    Left [String]
ss -> [String] -> TraceM era a
forall era a. [String] -> TraceM era a
failTrace ([String]
ss [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"in call to (getTarget " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RootTarget era r a -> String
forall a. Show a => a -> String
show RootTarget era r a
tar String -> String -> String
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 <- Term era (Map k a) -> TraceM era (Map k a)
forall era a. Term era a -> TraceM era a
getTerm Term era (Map k a)
term
  Gen (k, a) -> TraceM era (k, a)
forall a era. Gen a -> TraceM era a
liftGen (Gen (k, a) -> TraceM era (k, a))
-> Gen (k, a) -> TraceM era (k, a)
forall a b. (a -> b) -> a -> b
$ [String] -> Map k a -> Gen (k, a)
forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"fromMapTerm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term era (Map k a) -> String
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 <- Term era (Map k a) -> TraceM era (Map k a)
forall era a. Term era a -> TraceM era a
getTerm Term era (Map k a)
term
  let n :: Int
n = Map k a -> Int
forall k a. Map k a -> Int
Map.size Map k a
u
  Gen (k, a) -> TraceM era (k, a)
forall a era. Gen a -> TraceM era a
liftGen (Gen (k, a) -> TraceM era (k, a))
-> Gen (k, a) -> TraceM era (k, a)
forall a b. (a -> b) -> a -> b
$
    [String] -> Gen (k, a) -> ((k, a) -> Bool) -> Gen (k, a)
forall a. [String] -> Gen a -> (a -> Bool) -> Gen a
suchThatErr
      [String
"suchThatErr call (fromMapTermSuchThat " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term era (Map k a) -> String
forall a. Show a => a -> String
show Term era (Map k a)
term String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" size = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n]
      ([String] -> Map k a -> Gen (k, a)
forall k a. [String] -> Map k a -> Gen (k, a)
genFromMap [String
"fromMapTerm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term era (Map k a) -> String
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 <- Term era (Set b) -> TraceM era (Set b)
forall era a. Term era a -> TraceM era a
getTerm Term era (Set b)
term
  Gen b -> TraceM era b
forall a era. Gen a -> TraceM era a
liftGen ((b, Set b) -> b
forall a b. (a, b) -> a
fst ((b, Set b) -> b) -> Gen (b, Set b) -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ([String] -> Set b -> Gen (b, Set b)
forall a. [String] -> Set a -> Gen (a, Set a)
itemFromSet [String
"fromSetTerm " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Term era (Set b) -> String
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 = TraceM era (Env era)
forall era. TraceM era (Env era)
getEnv TraceM era (Env era)
-> (Env era -> TraceM era (Env era)) -> TraceM era (Env era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Env era -> TraceM era (Env era)
f TraceM era (Env era)
-> (Env era -> TraceM era (Env era)) -> TraceM era (Env era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Env era -> TraceM era (Env era)
forall era. Env era -> TraceM era (Env era)
putEnv TraceM era (Env era) -> TraceM era () -> TraceM era ()
forall a b. TraceM era a -> TraceM era b -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> () -> TraceM era ()
forall a. a -> TraceM era a
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 = StateT (TraceState era) (ExceptT [String] Gen) () -> TraceM era ()
forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM (StateT (TraceState era) (ExceptT [String] Gen) ()
 -> TraceM era ())
-> StateT (TraceState era) (ExceptT [String] Gen) ()
-> TraceM era ()
forall a b. (a -> b) -> a -> b
$ do
  TraceState Int
i Env era
env <- StateT (TraceState era) (ExceptT [String] Gen) (TraceState era)
forall (m :: * -> *) s. Monad m => StateT s m s
get
  case Typed t -> Either [String] t
forall x. Typed x -> Either [String] x
runTyped (Env era -> Term era t -> Typed t
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era t
term) of
    Right t
valA -> TraceState era -> StateT (TraceState era) (ExceptT [String] Gen) ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int -> Env era -> TraceState era
forall era. Int -> Env era -> TraceState era
TraceState Int
i (V era t -> t -> Env era -> Env era
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 -> ExceptT [String] Gen ()
-> StateT (TraceState era) (ExceptT [String] Gen) ()
forall (m :: * -> *) a.
Monad m =>
m a -> StateT (TraceState era) m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift ([String] -> ExceptT [String] Gen ()
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE ([String]
ss [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"in call to 'updateVar'"]))
updateVar Term era t
term t -> t
_ = [String] -> TraceM era ()
forall era a. [String] -> TraceM era a
failTrace [String
"Non Var term in call to 'updateVar'", Term era t -> String
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 = StateT (TraceState era) (ExceptT [String] Gen) () -> TraceM era ()
forall era x.
StateT (TraceState era) (ExceptT [String] Gen) x -> TraceM era x
TraceM (StateT (TraceState era) (ExceptT [String] Gen) ()
 -> TraceM era ())
-> StateT (TraceState era) (ExceptT [String] Gen) ()
-> TraceM era ()
forall a b. (a -> b) -> a -> b
$ do
  TraceState Int
i Env era
env <- StateT (TraceState era) (ExceptT [String] Gen) (TraceState era)
forall (m :: * -> *) s. Monad m => StateT s m s
get
  TraceState era -> StateT (TraceState era) (ExceptT [String] Gen) ()
forall (m :: * -> *) s. Monad m => s -> StateT s m ()
put (Int -> Env era -> TraceState era
forall era. Int -> Env era -> TraceState era
TraceState Int
i (V era t -> t -> Env era -> Env era
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
_ = [String] -> TraceM era ()
forall era a. [String] -> TraceM era a
failTrace [String
"Non Var term in call to 'setVar'", Term era t -> String
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
refInputs :: forall era. Proof era -> TxBody era -> Set TxIn
refInputs Proof era
Shelley TxBody era
_ = Set TxIn
forall a. Set a
Set.empty
refInputs Proof era
Allegra TxBody era
_ = Set TxIn
forall a. Set a
Set.empty
refInputs Proof era
Mary TxBody era
_ = Set TxIn
forall a. Set a
Set.empty
refInputs Proof era
Alonzo TxBody era
_ = Set TxIn
forall a. Set a
Set.empty
refInputs Proof era
Babbage TxBody era
txb = TxBody era
txb TxBody era
-> Getting (Set TxIn) (TxBody era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody era) (Set TxIn)
forall era. BabbageEraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody era) (Set TxIn)
referenceInputsTxBodyL
refInputs Proof era
Conway TxBody era
txb = TxBody era
txb TxBody era
-> Getting (Set TxIn) (TxBody era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody era) (Set TxIn)
forall era. BabbageEraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody era) (Set TxIn)
referenceInputsTxBodyL

reqSig :: Proof era -> TxBody era -> Set (KeyHash 'Witness)
reqSig :: forall era. Proof era -> TxBody era -> Set (KeyHash 'Witness)
reqSig Proof era
Shelley TxBody era
_ = Set (KeyHash 'Witness)
forall a. Set a
Set.empty
reqSig Proof era
Allegra TxBody era
_ = Set (KeyHash 'Witness)
forall a. Set a
Set.empty
reqSig Proof era
Mary TxBody era
_ = Set (KeyHash 'Witness)
forall a. Set a
Set.empty
reqSig Proof era
Alonzo TxBody era
_ = Set (KeyHash 'Witness)
forall a. Set a
Set.empty
reqSig Proof era
Babbage TxBody era
txb = TxBody era
txb TxBody era
-> Getting
     (Set (KeyHash 'Witness)) (TxBody era) (Set (KeyHash 'Witness))
-> Set (KeyHash 'Witness)
forall s a. s -> Getting a s a -> a
^. Getting
  (Set (KeyHash 'Witness)) (TxBody era) (Set (KeyHash 'Witness))
forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (Set (KeyHash 'Witness))
Lens' (TxBody era) (Set (KeyHash 'Witness))
reqSignerHashesTxBodyL
reqSig Proof era
Conway TxBody era
txb = TxBody era
txb TxBody era
-> Getting
     (Set (KeyHash 'Witness)) (TxBody era) (Set (KeyHash 'Witness))
-> Set (KeyHash 'Witness)
forall s a. s -> Getting a s a -> a
^. Getting
  (Set (KeyHash 'Witness)) (TxBody era) (Set (KeyHash 'Witness))
forall era.
AlonzoEraTxBody era =>
Lens' (TxBody era) (Set (KeyHash 'Witness))
Lens' (TxBody era) (Set (KeyHash 'Witness))
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 <- ((Int, [Pred era]) -> Gen (Int, [Pred era]))
-> [Pred era] -> TraceM era [Pred era]
forall a b era. ((Int, a) -> Gen (Int, b)) -> a -> TraceM era b
liftCounter (Int, [Pred era]) -> Gen (Int, [Pred era])
forall era. Era era => (Int, [Pred era]) -> Gen (Int, [Pred era])
rewriteGen [Pred era]
cs0
  DependGraph era
graph <- Typed (DependGraph era) -> TraceM era (DependGraph era)
forall a era. Typed a -> TraceM era a
liftTyped (Typed (DependGraph era) -> TraceM era (DependGraph era))
-> Typed (DependGraph era) -> TraceM era (DependGraph era)
forall a b. (a -> b) -> a -> b
$ do
    let instanPreds :: [Pred era]
instanPreds = (Pred era -> Pred era) -> [Pred era] -> [Pred era]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst era -> Pred era -> Pred era
forall era. Subst era -> Pred era -> Pred era
substPredWithVarTest Subst era
subst0) [Pred era]
simple
    [Name era]
orderedNames <- OrderInfo -> [Pred era] -> Typed [Name era]
forall era. Era era => OrderInfo -> [Pred era] -> Typed [Name era]
initialOrder OrderInfo
info [Pred era]
instanPreds
    Int
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
forall era.
Era era =>
Int
-> [([Name era], [Pred era])]
-> HashSet (Name era)
-> [Name era]
-> [Name era]
-> [Pred era]
-> Typed (DependGraph era)
mkDependGraph ([Name era] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Name era]
orderedNames) [] HashSet (Name era)
forall a. HashSet a
HashSet.empty [Name era]
orderedNames [] ([Pred era] -> Typed (DependGraph era))
-> [Pred era] -> Typed (DependGraph era)
forall a b. (a -> b) -> a -> b
$
      (Pred era -> Bool) -> [Pred era] -> [Pred era]
forall a. (a -> Bool) -> [a] -> [a]
Prelude.filter Pred era -> Bool
forall era. Pred era -> Bool
notBefore [Pred era]
instanPreds
  DependGraph era -> TraceM era (DependGraph era)
forall a. a -> TraceM era a
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) <- OrderInfo
-> Subst era -> [Pred era] -> TraceM era (DependGraph era)
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 <- Gen (Subst era) -> TraceM era (Subst era)
forall a era. Gen a -> TraceM era a
liftGen ((Subst era -> ([Name era], [Pred era]) -> Gen (Subst era))
-> Subst era -> [([Name era], [Pred era])] -> Gen (Subst era)
forall (t :: * -> *) (m :: * -> *) ans k.
(Foldable t, Monad m) =>
(ans -> k -> m ans) -> ans -> t k -> m ans
foldlM' Subst era -> ([Name era], [Pred era]) -> Gen (Subst era)
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 (Char -> t Char -> Bool
forall a. Eq a => a -> t a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Char
'.' t Char
k)
  Subst era -> TraceM era (Subst era)
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Subst era -> TraceM era (Subst era))
-> Subst era -> TraceM era (Subst era)
forall a b. (a -> b) -> a -> b
$ (Map String (SubstElem era) -> Subst era
forall era. Map String (SubstElem era) -> Subst era
Subst ((String -> SubstElem era -> Bool)
-> Map String (SubstElem era) -> Map String (SubstElem era)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\String
k SubstElem era
_ -> String -> Bool
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 = Gen (Subst era) -> TraceM era (Subst era)
forall a era. Gen a -> TraceM era a
liftGen (UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
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 = Gen (Subst era) -> TraceM era (Subst era)
forall a era. Gen a -> TraceM era a
liftGen (Proof era -> Subst era -> Gen (Subst era)
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 = Gen (Subst era) -> TraceM era (Subst era)
forall a era. Gen a -> TraceM era a
liftGen (UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
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 = Gen (Subst era) -> TraceM era (Subst era)
forall a era. Gen a -> TraceM era a
liftGen (Proof era -> Subst era -> Gen (Subst era)
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 = Gen (Subst era) -> TraceM era (Subst era)
forall a era. Gen a -> TraceM era a
liftGen (Proof era -> Subst era -> Gen (Subst era)
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 = Gen (Subst era) -> TraceM era (Subst era)
forall a era. Gen a -> TraceM era a
liftGen (Proof era -> Subst era -> Gen (Subst era)
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 = Gen (Subst era) -> TraceM era (Subst era)
forall a era. Gen a -> TraceM era a
liftGen (UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
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 = Gen (Subst era) -> TraceM era (Subst era)
forall a era. Gen a -> TraceM era a
liftGen (Proof era -> Subst era -> Gen (Subst era)
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 = Gen (Subst era) -> TraceM era (Subst era)
forall a era. Gen a -> TraceM era a
liftGen (Proof era -> Subst era -> Gen (Subst era)
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
_ = [(Env era, a)] -> TraceM era [(Env era, a)]
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
makeTrace Int
n TraceM era a
make = do
  Env era
env0 <- TraceM era (Env era)
forall era. TraceM era (Env era)
getEnv
  a
a <- TraceM era a
make
  [(Env era, a)]
xs <- Int -> TraceM era a -> TraceM era [(Env era, a)]
forall era a. Int -> TraceM era a -> TraceM era [(Env era, a)]
makeTrace (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) TraceM era a
make
  [(Env era, a)] -> TraceM era [(Env era, a)]
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Env era
env0, a
a) (Env era, a) -> [(Env era, a)] -> [(Env era, 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
_ = [TraceStep era a] -> TraceM era [TraceStep era a]
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
beforeAfterTrace !Int
n Int -> TraceM era a
make = do
  !Env era
beforeEnv <- TraceM era (Env era)
forall era. TraceM era (Env era)
getEnv
  !a
a <- Int -> TraceM era a
make Int
n
  !Env era
afterEnv <- TraceM era (Env era)
forall era. TraceM era (Env era)
getEnv
  [TraceStep era a]
xs <- Int -> (Int -> TraceM era a) -> TraceM era [TraceStep era a]
forall era a.
Int -> (Int -> TraceM era a) -> TraceM era [TraceStep era a]
beforeAfterTrace (Int
n Int -> Int -> Int
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} TraceStep era a -> [TraceStep era a] -> [TraceStep era a]
forall a. a -> [a] -> [a]
: [TraceStep era a]
xs
  [TraceStep era a] -> TraceM era [TraceStep era a]
forall a. a -> TraceM era a
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 <-
    Subst era -> TraceM era (Subst era)
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
forall era. Subst era
emptySubst
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
pparamsTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
universeTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
utxoTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
vstateTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
pstateTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
dstateTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
ledgerStateTrace Proof era
proof
  Env era
env <- Typed (Env era) -> TraceM era (Env era)
forall a era. Typed a -> TraceM era a
liftTyped (Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv)
  Env era -> TraceM era (Env era)
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 <-
    Subst era -> TraceM era (Subst era)
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
forall era. Subst era
emptySubst
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
pparamsTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
universeTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
utxoTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
vstateTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
pstateTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
dstateTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
ledgerStateTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
epochStateTrace Proof era
proof
      TraceM era (Subst era)
-> (Subst era -> TraceM era (Subst era)) -> TraceM era (Subst era)
forall a b. TraceM era a -> (a -> TraceM era b) -> TraceM era b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> TraceM era (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> TraceM era (Subst era)
newEpochStateTrace Proof era
proof
  Env era
env <- Typed (Env era) -> TraceM era (Env era)
forall a era. Typed a -> TraceM era a
liftTyped (Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv)
  Env era -> TraceM era (Env era)
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
_) = Doc Ann -> String
forall a. Show a => a -> String
show (((StrictSeq (Tx era), SlotNo) -> Doc Ann)
-> [(StrictSeq (Tx era), SlotNo)] -> Doc Ann
forall x ann. (x -> Doc ann) -> [x] -> Doc ann
ppList ((StrictSeq (Tx era) -> Doc Ann)
-> (SlotNo -> Doc Ann) -> (StrictSeq (Tx era), SlotNo) -> Doc Ann
forall t1 t2.
(t1 -> Doc Ann) -> (t2 -> Doc Ann) -> (t1, t2) -> Doc Ann
ppPair ((Tx era -> Doc Ann) -> StrictSeq (Tx era) -> Doc Ann
forall a ann. (a -> Doc ann) -> StrictSeq a -> Doc ann
ppStrictSeq (Proof era -> Tx era -> Doc Ann
forall era. Proof era -> Tx era -> Doc Ann
pcTx Proof era
forall era. Reflect era => Proof era
reify)) (SlotNo -> Doc Ann
pcSlotNo)) (Vector (StrictSeq (Tx era), SlotNo)
-> [(StrictSeq (Tx era), SlotNo)]
forall a. Vector a -> [a]
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 = Identity a -> a
forall a. Identity a -> a
runIdentity (Identity a -> a) -> Identity a -> a
forall a b. (a -> b) -> a -> b
$ ReaderT Globals Identity a -> Globals -> Identity a
forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
runReaderT ReaderT Globals Identity a
BaseM (MOCKCHAIN era) a
act Globals
BaseEnv (MOCKCHAIN era)
globals

  envGen :: HasCallStack => PredGen era -> Gen (Environment (MOCKCHAIN era))
envGen PredGen era
_gstate = () -> Gen ()
forall a. a -> Gen a
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
_ BlocksMade
_ EpochState era
_epochstate StrictMaybe PulsingRewUpdate
_ PoolDistr
pooldistr StashedAVVMAddresses era
_ = NewEpochState era
newepoch
    KeyHash 'StakePool
issuerkey <- EpochNo -> Word64 -> Int -> PoolDistr -> Gen (KeyHash 'StakePool)
chooseIssuer EpochNo
epochnum Word64
lastSlot Int
count PoolDistr
pooldistr
    let (StrictSeq (Tx era)
txs, SlotNo
nextSlotNo) = Vector (StrictSeq (Tx era), SlotNo)
txss Vector (StrictSeq (Tx era), SlotNo)
-> Int -> (StrictSeq (Tx era), SlotNo)
forall a. Vector a -> Int -> a
! Int
count
    -- Assmble it into a MockBlock
    let mockblock :: MockBlock era
mockblock = KeyHash 'StakePool -> SlotNo -> StrictSeq (Tx era) -> MockBlock era
forall era.
KeyHash 'StakePool -> SlotNo -> StrictSeq (Tx era) -> MockBlock era
MockBlock KeyHash 'StakePool
issuerkey SlotNo
nextSlotNo StrictSeq (Tx era)
txs
    -- Run the STS Rules for MOCKCHAIN with generated signal
    case ShelleyBase
  (Either
     (NonEmpty (PredicateFailure (MOCKCHAIN era)))
     (State (MOCKCHAIN era)))
-> Either
     (NonEmpty (PredicateFailure (MOCKCHAIN era)))
     (State (MOCKCHAIN era))
forall a. ShelleyBase a -> a
runShelleyBase (RuleContext 'Transition (MOCKCHAIN era)
-> ShelleyBase
     (Either
        (NonEmpty (PredicateFailure (MOCKCHAIN era)))
        (State (MOCKCHAIN era)))
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, Signal (MOCKCHAIN era)
MockBlock era
mockblock))) of
      Left NonEmpty (PredicateFailure (MOCKCHAIN era))
pdfs ->
        let _txsl :: [Tx era]
_txsl = StrictSeq (Tx era) -> [Tx era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Fold.toList StrictSeq (Tx era)
txs
         in String -> Gen (MockBlock era)
forall a. HasCallStack => String -> a
error (String -> Gen (MockBlock era))
-> ([String] -> String) -> [String] -> Gen (MockBlock era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> String
unlines ([String] -> Gen (MockBlock era))
-> [String] -> Gen (MockBlock era)
forall a b. (a -> b) -> a -> b
$
              ( String
"FAILS"
                  String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String
"epochNum " String -> String -> String
forall a. [a] -> [a] -> [a]
++ EpochNo -> String
forall a. Show a => a -> String
show EpochNo
epochnum, String
"slot " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Word64 -> String
forall a. Show a => a -> String
show Word64
lastSlot]
                  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (Tx era -> String) -> [Tx era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Doc Ann -> String
forall a. Show a => a -> String
show (Doc Ann -> String) -> (Tx era -> Doc Ann) -> Tx era -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof era -> Tx era -> Doc Ann
forall era. Proof era -> Tx era -> Doc Ann
pcTx Proof era
forall era. Reflect era => Proof era
reify) (StrictSeq (Tx era) -> [Tx era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (Tx era)
txs)
                  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ (PredicateFailure (MOCKCHAIN era) -> String)
-> [PredicateFailure (MOCKCHAIN era)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map PredicateFailure (MOCKCHAIN era) -> String
forall a. Show a => a -> String
show (NonEmpty (PredicateFailure (MOCKCHAIN era))
-> [PredicateFailure (MOCKCHAIN era)]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (PredicateFailure (MOCKCHAIN era))
pdfs)
                  [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [Doc Ann -> String
forall a. Show a => a -> String
show (Proof era -> NewEpochState era -> Doc Ann
forall era.
Reflect era =>
Proof era -> NewEpochState era -> Doc Ann
psNewEpochState Proof era
forall era. Reflect era => Proof era
reify NewEpochState era
newepoch)]
              )
      Right State (MOCKCHAIN era)
mcs2 -> State (MOCKCHAIN era) -> Gen (MockBlock era) -> Gen (MockBlock era)
forall a b. a -> b -> b
seq State (MOCKCHAIN era)
mcs2 (MockBlock era -> Gen (MockBlock era)
forall a. a -> Gen a
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 <- Proof era -> TraceM era (Env era)
forall era. Reflect era => Proof era -> TraceM era (Env era)
genNewEpochStateEnv Proof era
proof
  NewEpochState era
newepochstate <- Typed (NewEpochState era) -> TraceM era (NewEpochState era)
forall a era. Typed a -> TraceM era a
liftTyped (Typed (NewEpochState era) -> TraceM era (NewEpochState era))
-> Typed (NewEpochState era) -> TraceM era (NewEpochState era)
forall a b. (a -> b) -> a -> b
$ Env era
-> RootTarget era (NewEpochState era) (NewEpochState era)
-> Typed (NewEpochState era)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env0 (Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
forall era.
Reflect era =>
Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
newEpochStateT Proof era
proof)
  SlotNo Word64
currslot <- Typed SlotNo -> TraceM era SlotNo
forall a era. Typed a -> TraceM era a
liftTyped (Typed SlotNo -> TraceM era SlotNo)
-> Typed SlotNo -> TraceM era SlotNo
forall a b. (a -> b) -> a -> b
$ Env era -> Term era SlotNo -> Typed SlotNo
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env0 Term era SlotNo
forall era. Era era => Term era SlotNo
currentSlot
  let initStateFun :: Maybe (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era)))
initStateFun =
        (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era)))
-> Maybe
     (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era)))
forall a. a -> Maybe a
Just
          ( \(IRC ()) ->
              Either a (MockChainState era)
-> Gen (Either a (MockChainState era))
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MockChainState era -> Either a (MockChainState era)
forall a b. b -> Either a b
Right (NewEpochState era
-> NewEpochState era -> SlotNo -> Int -> MockChainState era
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 <- Int
-> (Int -> TraceM era (Tx era))
-> TraceM era [TraceStep era (Tx era)]
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 <- (TraceStep era (Tx era) -> Tx era)
-> [TraceStep era (Tx era)]
-> Word64
-> [([Tx era], SlotNo)]
-> TraceM era (Vector (StrictSeq (Tx era), SlotNo))
forall step era.
(step -> Tx era)
-> [step]
-> Word64
-> [([Tx era], SlotNo)]
-> TraceM era (Vector (StrictSeq (Tx era), SlotNo))
traceStepToVector TraceStep era (Tx era) -> Tx era
forall era a. TraceStep era a -> a
getTx [TraceStep era (Tx era)]
steps (Word64
currslot Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1) []
  ([TraceStep era (Tx era)],
 Maybe (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era))),
 PredGen era)
-> TraceM
     era
     ([TraceStep era (Tx era)],
      Maybe (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era))),
      PredGen era)
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TraceStep era (Tx era)]
steps, Maybe (IRC (MOCKCHAIN era) -> Gen (Either a (MockChainState era)))
initStateFun, Vector (StrictSeq (Tx era), SlotNo) -> Env era -> PredGen era
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 = Vector (StrictSeq (Tx era), SlotNo)
-> TraceM era (Vector (StrictSeq (Tx era), SlotNo))
forall a. a -> TraceM era a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(StrictSeq (Tx era), SlotNo)]
-> Vector (StrictSeq (Tx era), SlotNo)
forall a. [a] -> Vector a
fromList ([(StrictSeq (Tx era), SlotNo)] -> [(StrictSeq (Tx era), SlotNo)]
forall a. [a] -> [a]
reverse ((([Tx era], SlotNo) -> (StrictSeq (Tx era), SlotNo))
-> [([Tx era], SlotNo)] -> [(StrictSeq (Tx era), SlotNo)]
forall a b. (a -> b) -> [a] -> [b]
map (\([Tx era]
x, SlotNo
y) -> ([Tx era] -> StrictSeq (Tx era)
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 <- Gen Int -> TraceM era Int
forall a era. Gen a -> TraceM era a
liftGen (Gen Int -> TraceM era Int) -> Gen Int -> TraceM era Int
forall a b. (a -> b) -> a -> b
$ (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
choose (Int
1, Int
2)
  let steplist :: [step]
steplist = Int -> [step] -> [step]
forall a. Int -> [a] -> [a]
take Int
n [step]
steps
  Word64
nextslot <- Gen Word64 -> TraceM era Word64
forall a era. Gen a -> TraceM era a
liftGen ((Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
m) (Word64 -> Word64) -> Gen Word64 -> Gen Word64
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, Gen Word64)] -> Gen Word64
forall a. HasCallStack => [(Int, Gen a)] -> Gen a
frequency [(Int
2, Word64 -> Gen Word64
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
2), (Int
1, Word64 -> Gen Word64
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Word64
3), (Int
1, Word64 -> Gen Word64
forall a. a -> Gen a
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
  (step -> Tx era)
-> [step]
-> Word64
-> [([Tx era], SlotNo)]
-> TraceM era (Vector (StrictSeq (Tx era), SlotNo))
forall step era.
(step -> Tx era)
-> [step]
-> Word64
-> [([Tx era], SlotNo)]
-> TraceM era (Vector (StrictSeq (Tx era), SlotNo))
traceStepToVector step -> Tx era
getTx (Int -> [step] -> [step]
forall a. Int -> [a] -> [a]
drop Int
n [step]
steps) Word64
nextslot (((step -> Tx era) -> [step] -> [Tx era]
forall a b. (a -> b) -> [a] -> [b]
map step -> Tx era
getTx [step]
steplist, Word64 -> SlotNo
SlotNo Word64
m) ([Tx era], SlotNo) -> [([Tx era], SlotNo)] -> [([Tx era], SlotNo)]
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
_)) <- TraceM
  era
  ([TraceStep era (Tx era)],
   Maybe
     (IRC (MOCKCHAIN era)
      -> Gen
           (Either (NonEmpty (MockChainFailure era)) (MockChainState era))),
   PredGen era)
-> Gen
     ([TraceStep era (Tx era)],
      Maybe
        (IRC (MOCKCHAIN era)
         -> Gen
              (Either (NonEmpty (MockChainFailure era)) (MockChainState era))),
      PredGen era)
forall era a. TraceM era a -> Gen a
toGen (TraceM
   era
   ([TraceStep era (Tx era)],
    Maybe
      (IRC (MOCKCHAIN era)
       -> Gen
            (Either (NonEmpty (MockChainFailure era)) (MockChainState era))),
    PredGen era)
 -> Gen
      ([TraceStep era (Tx era)],
       Maybe
         (IRC (MOCKCHAIN era)
          -> Gen
               (Either (NonEmpty (MockChainFailure era)) (MockChainState era))),
       PredGen era))
-> TraceM
     era
     ([TraceStep era (Tx era)],
      Maybe
        (IRC (MOCKCHAIN era)
         -> Gen
              (Either (NonEmpty (MockChainFailure era)) (MockChainState era))),
      PredGen era)
-> Gen
     ([TraceStep era (Tx era)],
      Maybe
        (IRC (MOCKCHAIN era)
         -> Gen
              (Either (NonEmpty (MockChainFailure era)) (MockChainState era))),
      PredGen era)
forall a b. (a -> b) -> a -> b
$ Proof era
-> Int
-> (Proof era -> TraceM era (Tx era))
-> TraceM
     era
     ([TraceStep era (Tx era)],
      Maybe
        (IRC (MOCKCHAIN era)
         -> Gen
              (Either (NonEmpty (MockChainFailure era)) (MockChainState era))),
      PredGen era)
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
  BaseEnv (MOCKCHAIN era)
-> Word64
-> PredGen era
-> Maybe
     (IRC (MOCKCHAIN era)
      -> Gen
           (Either
              (NonEmpty (PredicateFailure (MOCKCHAIN era)))
              (State (MOCKCHAIN era))))
-> Gen (Trace (MOCKCHAIN era))
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
BaseEnv (MOCKCHAIN era)
testGlobals (Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Vector (StrictSeq (Tx era), SlotNo) -> Int
forall a. Vector a -> Int
Vector.length Vector (StrictSeq (Tx era), SlotNo)
zs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) PredGen era
predgen Maybe
  (IRC (MOCKCHAIN era)
   -> Gen
        (Either
           (NonEmpty (PredicateFailure (MOCKCHAIN era)))
           (State (MOCKCHAIN era))))
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 = Proof era
-> Int
-> (Proof era -> TraceM era (Tx era))
-> Gen (Trace (MOCKCHAIN era))
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
  Gen (Trace (MOCKCHAIN era))
-> (Trace (MOCKCHAIN era) -> [Trace (MOCKCHAIN era)])
-> (Trace (MOCKCHAIN era) -> Property)
-> Property
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
BaseEnv (MOCKCHAIN era)
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 (MockBlock era -> MockChainState era -> Property)
-> [MockBlock era] -> [MockChainState era] -> [Property]
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)]
[MockBlock era]
sigs [State (MOCKCHAIN era)]
[MockChainState era]
states of
  [] -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
  (Property
_ : [Property]
more) -> [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin [Property]
more
  where
    state0 :: MockChainState era
state0 = Trace (MOCKCHAIN era)
tr Trace (MOCKCHAIN era)
-> Getting
     (MockChainState era) (Trace (MOCKCHAIN era)) (MockChainState era)
-> MockChainState era
forall s a. s -> Getting a s a -> a
^. (State (MOCKCHAIN era)
 -> Const (MockChainState era) (State (MOCKCHAIN era)))
-> Trace (MOCKCHAIN era)
-> Const (MockChainState era) (Trace (MOCKCHAIN era))
Getting
  (MockChainState era) (Trace (MOCKCHAIN era)) (MockChainState era)
forall s (f :: * -> *).
Functor f =>
(State s -> f (State s)) -> Trace s -> f (Trace s)
traceInitState
    states :: [State (MOCKCHAIN era)]
states = TraceOrder -> Trace (MOCKCHAIN era) -> [State (MOCKCHAIN era)]
forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace (MOCKCHAIN era)
tr
    sigs :: [Signal (MOCKCHAIN era)]
sigs = TraceOrder -> Trace (MOCKCHAIN era) -> [Signal (MOCKCHAIN era)]
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
  [] -> Bool -> Property
forall prop. Testable prop => prop -> Property
property Bool
True
  State (MOCKCHAIN era)
_ : [State (MOCKCHAIN era)]
more -> [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ((MockChainState era
 -> MockBlock era -> MockChainState era -> Property)
-> [MockChainState era]
-> [MockBlock era]
-> [MockChainState era]
-> [Property]
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)]
[MockChainState era]
states [Signal (MOCKCHAIN era)]
[MockBlock era]
sigs [State (MOCKCHAIN era)]
[MockChainState era]
more)
  where
    states :: [State (MOCKCHAIN era)]
states = TraceOrder -> Trace (MOCKCHAIN era) -> [State (MOCKCHAIN era)]
forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace (MOCKCHAIN era)
tr
    sigs :: [Signal (MOCKCHAIN era)]
sigs = TraceOrder -> Trace (MOCKCHAIN era) -> [Signal (MOCKCHAIN era)]
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)
MockChainState era
stateN
  where
    state0 :: MockChainState era
state0 = Trace (MOCKCHAIN era)
tr Trace (MOCKCHAIN era)
-> Getting
     (MockChainState era) (Trace (MOCKCHAIN era)) (MockChainState era)
-> MockChainState era
forall s a. s -> Getting a s a -> a
^. (State (MOCKCHAIN era)
 -> Const (MockChainState era) (State (MOCKCHAIN era)))
-> Trace (MOCKCHAIN era)
-> Const (MockChainState era) (Trace (MOCKCHAIN era))
Getting
  (MockChainState era) (Trace (MOCKCHAIN era)) (MockChainState era)
forall s (f :: * -> *).
Functor f =>
(State s -> f (State s)) -> Trace s -> f (Trace s)
traceInitState
    stateN :: State (MOCKCHAIN era)
stateN = Trace (MOCKCHAIN era) -> State (MOCKCHAIN era)
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 =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
message (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ((NonEmpty (MockChainState era) -> Property)
-> [NonEmpty (MockChainState era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (\NonEmpty (MockChainState era)
epoch -> (MockChainState era -> MockChainState era -> Property
p (NonEmpty (MockChainState era) -> MockChainState era
forall a. NonEmpty a -> a
NE.head NonEmpty (MockChainState era)
epoch) (NonEmpty (MockChainState era) -> MockChainState era
forall a. NonEmpty a -> a
NE.last NonEmpty (MockChainState era)
epoch))) [NonEmpty (MockChainState era)]
epochs)
  where
    states :: [State (MOCKCHAIN era)]
states = TraceOrder -> Trace (MOCKCHAIN era) -> [State (MOCKCHAIN era)]
forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace (MOCKCHAIN era)
tr
    epochs :: [NonEmpty (MockChainState era)]
epochs = [MockChainState era] -> [NonEmpty (MockChainState era)]
forall era. [MockChainState era] -> [NonEmpty (MockChainState era)]
splitEpochs [State (MOCKCHAIN era)]
[MockChainState era]
states
    showEpoch :: NonEmpty (MockChainState era) -> a -> String
showEpoch NonEmpty (MockChainState era)
epoch a
n = [String] -> String
unlines ((String
"EPOCH " String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (MockChainState era -> String) -> [MockChainState era] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map MockChainState era -> String
forall era. ConwayEraGov era => MockChainState era -> String
showPulserState (NonEmpty (MockChainState era) -> [MockChainState era]
forall a. NonEmpty a -> [a]
NE.toList NonEmpty (MockChainState era)
epoch))
    message :: String
message =
      [String] -> String
unlines ((String
"Trace length " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show ([MockChainState era] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [State (MOCKCHAIN era)]
[MockChainState era]
states)) String -> [String] -> [String]
forall a. a -> [a] -> [a]
: (NonEmpty (MockChainState era) -> Int -> String)
-> [NonEmpty (MockChainState era)] -> [Int] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith NonEmpty (MockChainState era) -> Int -> String
forall {era} {a}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 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
  [NonEmpty (MockChainState era)] -> [NonEmpty (MockChainState era)]
forall a. [a] -> [a]
reverse ([NonEmpty (MockChainState era)]
 -> [NonEmpty (MockChainState era)])
-> [NonEmpty (MockChainState era)]
-> [NonEmpty (MockChainState era)]
forall a b. (a -> b) -> a -> b
$ Int
-> [NonEmpty (MockChainState era)]
-> [NonEmpty (MockChainState era)]
forall a. Int -> [a] -> [a]
drop Int
1 ([NonEmpty (MockChainState era)]
 -> [NonEmpty (MockChainState era)])
-> [NonEmpty (MockChainState era)]
-> [NonEmpty (MockChainState era)]
forall a b. (a -> b) -> a -> b
$ [NonEmpty (MockChainState era)] -> [NonEmpty (MockChainState era)]
forall a. [a] -> [a]
reverse ([NonEmpty (MockChainState era)] -> [NonEmpty (MockChainState era)]
forall a. [a] -> [a]
removeFirst ([NonEmpty (MockChainState era)]
 -> [NonEmpty (MockChainState era)])
-> [NonEmpty (MockChainState era)]
-> [NonEmpty (MockChainState era)]
forall a b. (a -> b) -> a -> b
$ (MockChainState era -> MockChainState era -> Bool)
-> [MockChainState era] -> [NonEmpty (MockChainState era)]
forall (f :: * -> *) a.
Foldable f =>
(a -> a -> Bool) -> f a -> [NonEmpty a]
NE.groupBy (EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
(==) (EpochNo -> EpochNo -> Bool)
-> (MockChainState era -> EpochNo)
-> MockChainState era
-> MockChainState era
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (NewEpochState era -> EpochNo)
-> (MockChainState era -> NewEpochState era)
-> MockChainState era
-> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockChainState era -> NewEpochState era
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 = Int -> [a] -> [a]
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 = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SlotNo -> String
forall a. Show a => a -> String
show SlotNo
slot String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"   " String -> String -> String
forall a. [a] -> [a] -> [a]
++ DRepPulsingState era -> String
forall {era}. DRepPulsingState era -> String
getPulserInfo (NewEpochState era
nes NewEpochState era
-> Getting
     (DRepPulsingState era) (NewEpochState era) (DRepPulsingState era)
-> DRepPulsingState era
forall s a. s -> Getting a s a -> a
^. Getting
  (DRepPulsingState era) (NewEpochState era) (DRepPulsingState era)
forall era.
ConwayEraGov era =>
Lens' (NewEpochState era) (DRepPulsingState era)
Lens' (NewEpochState era) (DRepPulsingState era)
newEpochStateDRepPulsingStateL)
  where
    getPulserInfo :: DRepPulsingState era -> String
getPulserInfo (DRPulsing DRepPulser era Identity (RatifyState era)
x) =
      String
"Index = "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Any -> String
forall a. Show a => a -> String
show (Int -> Doc Any
forall a. Int -> Doc a
ppInt (DRepPulser era Identity (RatifyState era) -> Int
forall era ans (m :: * -> *). DRepPulser era m ans -> Int
dpIndex DRepPulser era Identity (RatifyState era)
x))
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"    DRepDistr = "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Ann -> String
forall a. Show a => a -> String
show (Map DRep (CompactForm Coin) -> Doc Ann
forall a. Map a (CompactForm Coin) -> Doc Ann
summaryMapCompact (DRepPulser era Identity (RatifyState era)
-> Map DRep (CompactForm Coin)
forall era ans (m :: * -> *).
DRepPulser era m ans -> Map DRep (CompactForm Coin)
dpDRepDistr DRepPulser era Identity (RatifyState era)
x))
    getPulserInfo (DRComplete PulsingSnapshot era
psnap RatifyState era
_) =
      String
"Complete DRepDistr = "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc Ann -> String
forall a. Show a => a -> String
show (Map DRep (CompactForm Coin) -> Doc Ann
forall a. Map a (CompactForm Coin) -> Doc Ann
summaryMapCompact (PulsingSnapshot era -> Map DRep (CompactForm Coin)
forall era. PulsingSnapshot era -> Map DRep (CompactForm Coin)
psDRepDistr PulsingSnapshot era
psnap))