{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# OPTIONS_GHC -Wno-deprecations  #-}
module Test.QuickCheck.ContractModel.Internal where

import Control.Lens
import Control.Monad.Reader
import Control.Monad.Writer
import Control.Monad.State
import Control.Monad.Error

import Test.QuickCheck
import Test.QuickCheck.Monadic
import Test.QuickCheck.StateModel qualified as StateModel
import Test.QuickCheck.ContractModel.Internal.Symbolics
import Test.QuickCheck.ContractModel.Internal.Spec
import Test.QuickCheck.ContractModel.Internal.ChainIndex
import Test.QuickCheck.ContractModel.Internal.Model
import Test.QuickCheck.ContractModel.Internal.Utils
import Test.QuickCheck.ContractModel.Internal.Common
import Data.Map (Map)
import Data.Map qualified as Map
import Data.Maybe
import Text.PrettyPrint.HughesPJClass hiding ((<>))

import Cardano.Api
import Cardano.Api.Shelley

class (ContractModel state, IsRunnable m) => RunModel state m where
  -- | Perform an `Action` in some `state` in the `Monad` `m`.  This
  -- is the function that's used to exercise the actual stateful
  -- implementation, usually through various side-effects as permitted
  -- by `m`. It produces a value of type `a`, eg. some observable
  -- output from the `Action` that should later be kept in the
  -- environment through a `Var a` also passed to the `nextState`
  -- function.
  --
  -- The `Lookup` parameter provides an /environment/ to lookup `Var
  -- a` instances from previous steps.
  perform :: ModelState state
          -> Action state
          -> (forall t. HasSymbolicRep t => Symbolic t -> t)
          -> RunMonad m ()

  -- | Allows the user to attach information to the `Property` at each step of the process.
  -- This function is given the full transition that's been executed, including the start and ending
  -- `state`, the `Action`, the current environment to `Lookup` and the value produced by `perform`
  -- while executing this step.
  monitoring :: (ModelState state, ModelState state)
             -> Action state
             -> (forall t. HasSymbolicRep t => Symbolic t -> t)
             -> SymIndex
             -> Property
             -> Property
  monitoring (ModelState state, ModelState state)
_ Action state
_ forall t. HasSymbolicRep t => Symbolic t -> t
_ SymIndex
_ Property
prop = Property
prop

-- TODO: consider putting errors in this?
newtype RunMonad m a = RunMonad { RunMonad m a -> WriterT SymIndex m a
unRunMonad :: WriterT SymIndex m a }
  deriving newtype (a -> RunMonad m b -> RunMonad m a
(a -> b) -> RunMonad m a -> RunMonad m b
(forall a b. (a -> b) -> RunMonad m a -> RunMonad m b)
-> (forall a b. a -> RunMonad m b -> RunMonad m a)
-> Functor (RunMonad m)
forall a b. a -> RunMonad m b -> RunMonad m a
forall a b. (a -> b) -> RunMonad m a -> RunMonad m b
forall (m :: * -> *) a b.
Functor m =>
a -> RunMonad m b -> RunMonad m a
forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> RunMonad m a -> RunMonad m b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> RunMonad m b -> RunMonad m a
$c<$ :: forall (m :: * -> *) a b.
Functor m =>
a -> RunMonad m b -> RunMonad m a
fmap :: (a -> b) -> RunMonad m a -> RunMonad m b
$cfmap :: forall (m :: * -> *) a b.
Functor m =>
(a -> b) -> RunMonad m a -> RunMonad m b
Functor, Functor (RunMonad m)
a -> RunMonad m a
Functor (RunMonad m)
-> (forall a. a -> RunMonad m a)
-> (forall a b.
    RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b)
-> (forall a b c.
    (a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c)
-> (forall a b. RunMonad m a -> RunMonad m b -> RunMonad m b)
-> (forall a b. RunMonad m a -> RunMonad m b -> RunMonad m a)
-> Applicative (RunMonad m)
RunMonad m a -> RunMonad m b -> RunMonad m b
RunMonad m a -> RunMonad m b -> RunMonad m a
RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b
(a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c
forall a. a -> RunMonad m a
forall a b. RunMonad m a -> RunMonad m b -> RunMonad m a
forall a b. RunMonad m a -> RunMonad m b -> RunMonad m b
forall a b. RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b
forall a b c.
(a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m 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 (m :: * -> *). Applicative m => Functor (RunMonad m)
forall (m :: * -> *) a. Applicative m => a -> RunMonad m a
forall (m :: * -> *) a b.
Applicative m =>
RunMonad m a -> RunMonad m b -> RunMonad m a
forall (m :: * -> *) a b.
Applicative m =>
RunMonad m a -> RunMonad m b -> RunMonad m b
forall (m :: * -> *) a b.
Applicative m =>
RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c
<* :: RunMonad m a -> RunMonad m b -> RunMonad m a
$c<* :: forall (m :: * -> *) a b.
Applicative m =>
RunMonad m a -> RunMonad m b -> RunMonad m a
*> :: RunMonad m a -> RunMonad m b -> RunMonad m b
$c*> :: forall (m :: * -> *) a b.
Applicative m =>
RunMonad m a -> RunMonad m b -> RunMonad m b
liftA2 :: (a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c
$cliftA2 :: forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> c) -> RunMonad m a -> RunMonad m b -> RunMonad m c
<*> :: RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b
$c<*> :: forall (m :: * -> *) a b.
Applicative m =>
RunMonad m (a -> b) -> RunMonad m a -> RunMonad m b
pure :: a -> RunMonad m a
$cpure :: forall (m :: * -> *) a. Applicative m => a -> RunMonad m a
$cp1Applicative :: forall (m :: * -> *). Applicative m => Functor (RunMonad m)
Applicative, Applicative (RunMonad m)
a -> RunMonad m a
Applicative (RunMonad m)
-> (forall a b.
    RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b)
-> (forall a b. RunMonad m a -> RunMonad m b -> RunMonad m b)
-> (forall a. a -> RunMonad m a)
-> Monad (RunMonad m)
RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b
RunMonad m a -> RunMonad m b -> RunMonad m b
forall a. a -> RunMonad m a
forall a b. RunMonad m a -> RunMonad m b -> RunMonad m b
forall a b. RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b
forall (m :: * -> *). Monad m => Applicative (RunMonad m)
forall (m :: * -> *) a. Monad m => a -> RunMonad m a
forall (m :: * -> *) a b.
Monad m =>
RunMonad m a -> RunMonad m b -> RunMonad m b
forall (m :: * -> *) a b.
Monad m =>
RunMonad m a -> (a -> RunMonad m b) -> RunMonad m 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 :: a -> RunMonad m a
$creturn :: forall (m :: * -> *) a. Monad m => a -> RunMonad m a
>> :: RunMonad m a -> RunMonad m b -> RunMonad m b
$c>> :: forall (m :: * -> *) a b.
Monad m =>
RunMonad m a -> RunMonad m b -> RunMonad m b
>>= :: RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b
$c>>= :: forall (m :: * -> *) a b.
Monad m =>
RunMonad m a -> (a -> RunMonad m b) -> RunMonad m b
$cp1Monad :: forall (m :: * -> *). Monad m => Applicative (RunMonad m)
Monad, MonadError e, MonadState s, MonadWriter SymIndex)

liftRunMonad :: (forall a. m a -> n a) -> RunMonad m a -> RunMonad n a
liftRunMonad :: (forall a. m a -> n a) -> RunMonad m a -> RunMonad n a
liftRunMonad forall a. m a -> n a
f (RunMonad (WriterT m (a, SymIndex)
m)) = WriterT SymIndex n a -> RunMonad n a
forall (m :: * -> *) a. WriterT SymIndex m a -> RunMonad m a
RunMonad (WriterT SymIndex n a -> RunMonad n a)
-> (n (a, SymIndex) -> WriterT SymIndex n a)
-> n (a, SymIndex)
-> RunMonad n a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n (a, SymIndex) -> WriterT SymIndex n a
forall w (m :: * -> *) a. m (a, w) -> WriterT w m a
WriterT (n (a, SymIndex) -> RunMonad n a)
-> n (a, SymIndex) -> RunMonad n a
forall a b. (a -> b) -> a -> b
$ m (a, SymIndex) -> n (a, SymIndex)
forall a. m a -> n a
f m (a, SymIndex)
m

instance Monad m => MonadFail (RunMonad m) where
  fail :: String -> RunMonad m a
fail = String -> RunMonad m a
forall a. HasCallStack => String -> a
error

registerSymbolic :: (Monad m, HasSymbolicRep t)
                 => String
                 -> t
                 -> RunMonad m ()
registerSymbolic :: String -> t -> RunMonad m ()
registerSymbolic String
s = SymIndex -> RunMonad m ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell (SymIndex -> RunMonad m ())
-> (t -> SymIndex) -> t -> RunMonad m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> t -> SymIndex
forall t. HasSymbolicRep t => String -> t -> SymIndex
symIndex String
s

registerToken :: Monad m => String -> AssetId -> RunMonad m ()
registerToken :: String -> AssetId -> RunMonad m ()
registerToken = String -> AssetId -> RunMonad m ()
forall (m :: * -> *) t.
(Monad m, HasSymbolicRep t) =>
String -> t -> RunMonad m ()
registerSymbolic

registerTxOut :: Monad m => String -> TxOut CtxUTxO Era -> RunMonad m ()
registerTxOut :: String -> TxOut CtxUTxO Era -> RunMonad m ()
registerTxOut = String -> TxOut CtxUTxO Era -> RunMonad m ()
forall (m :: * -> *) t.
(Monad m, HasSymbolicRep t) =>
String -> t -> RunMonad m ()
registerSymbolic

registerTxIn :: Monad m => String -> TxIn -> RunMonad m ()
registerTxIn :: String -> TxIn -> RunMonad m ()
registerTxIn = String -> TxIn -> RunMonad m ()
forall (m :: * -> *) t.
(Monad m, HasSymbolicRep t) =>
String -> t -> RunMonad m ()
registerSymbolic

withLocalSymbolics :: Monad m => RunMonad m () -> RunMonad m SymIndex
withLocalSymbolics :: RunMonad m () -> RunMonad m SymIndex
withLocalSymbolics RunMonad m ()
m = (SymIndex -> SymIndex)
-> RunMonad m SymIndex -> RunMonad m SymIndex
forall w (m :: * -> *) a. MonadWriter w m => (w -> w) -> m a -> m a
censor (SymIndex -> SymIndex -> SymIndex
forall a b. a -> b -> a
const SymIndex
forall a. Monoid a => a
mempty) (RunMonad m SymIndex -> RunMonad m SymIndex)
-> (RunMonad m () -> RunMonad m SymIndex)
-> RunMonad m ()
-> RunMonad m SymIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (((), SymIndex) -> SymIndex)
-> RunMonad m ((), SymIndex) -> RunMonad m SymIndex
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((), SymIndex) -> SymIndex
forall a b. (a, b) -> b
snd (RunMonad m ((), SymIndex) -> RunMonad m SymIndex)
-> (RunMonad m () -> RunMonad m ((), SymIndex))
-> RunMonad m ()
-> RunMonad m SymIndex
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RunMonad m () -> RunMonad m ((), SymIndex)
forall w (m :: * -> *) a. MonadWriter w m => m a -> m (a, w)
listen (RunMonad m () -> RunMonad m SymIndex)
-> RunMonad m () -> RunMonad m SymIndex
forall a b. (a -> b) -> a -> b
$ RunMonad m ()
m

instance MonadTrans RunMonad where
  lift :: m a -> RunMonad m a
lift = WriterT SymIndex m a -> RunMonad m a
forall (m :: * -> *) a. WriterT SymIndex m a -> RunMonad m a
RunMonad (WriterT SymIndex m a -> RunMonad m a)
-> (m a -> WriterT SymIndex m a) -> m a -> RunMonad m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> WriterT SymIndex m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

type instance StateModel.Realized (RunMonad m) a = StateModel.Realized m a

type DefaultRealized m = ( StateModel.Realized m SymIndex ~ SymIndex
                         , StateModel.Realized m () ~ ()
                         )

class (DefaultRealized m, HasChainIndex m, Monad m) => IsRunnable m where
  awaitSlot :: SlotNo -> m ()

instance (Monoid w, DefaultRealized m, IsRunnable m) => IsRunnable (WriterT w m) where
  awaitSlot :: SlotNo -> WriterT w m ()
awaitSlot = m () -> WriterT w m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> WriterT w m ())
-> (SlotNo -> m ()) -> SlotNo -> WriterT w m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> m ()
forall (m :: * -> *). IsRunnable m => SlotNo -> m ()
awaitSlot

instance (DefaultRealized m, IsRunnable m) => IsRunnable (StateT s m) where
  awaitSlot :: SlotNo -> StateT s m ()
awaitSlot = m () -> StateT s m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> StateT s m ())
-> (SlotNo -> m ()) -> SlotNo -> StateT s m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> m ()
forall (m :: * -> *). IsRunnable m => SlotNo -> m ()
awaitSlot

instance (DefaultRealized m, IsRunnable m) => IsRunnable (ReaderT r m) where
  awaitSlot :: SlotNo -> ReaderT r m ()
awaitSlot = m () -> ReaderT r m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> ReaderT r m ())
-> (SlotNo -> m ()) -> SlotNo -> ReaderT r m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> m ()
forall (m :: * -> *). IsRunnable m => SlotNo -> m ()
awaitSlot

instance (Monad m, HasChainIndex m) => HasChainIndex (RunMonad m) where
  getChainIndex :: RunMonad m ChainIndex
getChainIndex = m ChainIndex -> RunMonad m ChainIndex
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m ChainIndex
forall (m :: * -> *). HasChainIndex m => m ChainIndex
getChainIndex
  getChainState :: RunMonad m ChainState
getChainState = m ChainState -> RunMonad m ChainState
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m ChainState
forall (m :: * -> *). HasChainIndex m => m ChainState
getChainState

instance (Monad m, HasChainIndex m) => HasChainIndex (StateModel.PostconditionM m) where
  getChainIndex :: PostconditionM m ChainIndex
getChainIndex = m ChainIndex -> PostconditionM m ChainIndex
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m ChainIndex
forall (m :: * -> *). HasChainIndex m => m ChainIndex
getChainIndex
  getChainState :: PostconditionM m ChainState
getChainState = m ChainState -> PostconditionM m ChainState
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift m ChainState
forall (m :: * -> *). HasChainIndex m => m ChainState
getChainState

instance IsRunnable m => IsRunnable (RunMonad m) where
  awaitSlot :: SlotNo -> RunMonad m ()
awaitSlot = m () -> RunMonad m ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m () -> RunMonad m ())
-> (SlotNo -> m ()) -> SlotNo -> RunMonad m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> m ()
forall (m :: * -> *). IsRunnable m => SlotNo -> m ()
awaitSlot

-- Takes a `SymToken` and turns it into an `AssetId`
translateSymbolic :: (StateModel.Var SymIndex -> SymIndex) -> SymbolicSemantics
translateSymbolic :: (Var SymIndex -> SymIndex)
-> forall t. HasSymbolicRep t => Symbolic t -> t
translateSymbolic Var SymIndex -> SymIndex
lookup Symbolic t
token = case SymIndex -> Symbolic t -> Maybe t
forall t. HasSymbolicRep t => SymIndex -> Symbolic t -> Maybe t
lookupSymbolic (Var SymIndex -> SymIndex
lookup (Var SymIndex -> SymIndex) -> Var SymIndex -> SymIndex
forall a b. (a -> b) -> a -> b
$ Symbolic t -> Var SymIndex
forall k (t :: k). Symbolic t -> Var SymIndex
symVar Symbolic t
token) Symbolic t
token of
  Just t
v  -> t
v
  Maybe t
Nothing -> String -> t
forall a. HasCallStack => String -> a
error String
"The impossible happend: uncaught missing register for symbolic"

instance ( IsRunnable m
         , RunModel state m
         ) => StateModel.RunModel (ModelState state) (RunMonad m) where
  perform :: ModelState state
-> Action (ModelState state) a
-> LookUp (RunMonad m)
-> RunMonad m (Realized (RunMonad m) a)
perform ModelState state
st (ContractAction _ a) LookUp (RunMonad m)
lookup = do
      -- Run locally and get the registered symbolics out
      RunMonad m () -> RunMonad m SymIndex
forall (m :: * -> *).
Monad m =>
RunMonad m () -> RunMonad m SymIndex
withLocalSymbolics (RunMonad m () -> RunMonad m SymIndex)
-> RunMonad m () -> RunMonad m SymIndex
forall a b. (a -> b) -> a -> b
$ ModelState state
-> Action state
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> RunMonad m ()
forall state (m :: * -> *).
RunModel state m =>
ModelState state
-> Action state
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> RunMonad m ()
perform ModelState state
st Action state
a ((Var SymIndex -> SymIndex)
-> forall t. HasSymbolicRep t => Symbolic t -> t
translateSymbolic Var SymIndex -> SymIndex
LookUp (RunMonad m)
lookup)
  perform ModelState state
_ (WaitUntil slot) LookUp (RunMonad m)
_ = SlotNo -> RunMonad m ()
forall (m :: * -> *). IsRunnable m => SlotNo -> m ()
awaitSlot SlotNo
slot
  perform ModelState state
_ Observation{} LookUp (RunMonad m)
_ = () -> RunMonad m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  postcondition :: (ModelState state, ModelState state)
-> Action (ModelState state) a
-> LookUp (RunMonad m)
-> Realized (RunMonad m) a
-> PostconditionM (RunMonad m) Bool
postcondition (ModelState state
st, ModelState state
_) (ContractAction _ act) LookUp (RunMonad m)
_ Realized (RunMonad m) a
symIndex = do
    -- Ask the model what symbolics we expected to be registered in this run.
    -- NOTE: using `StateModel.Var 0` here is safe because we know that `StateModel` never uses `0` and we
    -- therefore get something unique. Likewise, we know that `nextState` can't observe the
    -- variables we use so it won't know the difference between having the real sym token
    -- it will get when we run `stateAfter` and this fake one.
    let expectedSymbolics :: SymCreationIndex
expectedSymbolics = Spec state ()
-> Var SymIndex -> ModelState state -> SymCreationIndex
forall state.
Spec state ()
-> Var SymIndex -> ModelState state -> SymCreationIndex
symbolicsCreatedBy (Action state -> Spec state ()
forall state. ContractModel state => Action state -> Spec state ()
nextState Action state
act) (Int -> Var SymIndex
forall a. Int -> Var a
StateModel.mkVar Int
0) ModelState state
st
        actualSymbolics :: SymCreationIndex
actualSymbolics   = SymIndex -> SymCreationIndex
toCreationIndex Realized (RunMonad m) a
SymIndex
symIndex
    String -> PostconditionM (RunMonad m) ()
forall (m :: * -> *). Monad m => String -> PostconditionM m ()
StateModel.counterexamplePost (String -> PostconditionM (RunMonad m) ())
-> String -> PostconditionM (RunMonad m) ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unlines
      [ String
"Expected symbolics do not match registered symbolics"
      , String
"  Expected: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SymCreationIndex -> String
forall a. Show a => a -> String
show SymCreationIndex
expectedSymbolics
      , String
"  Actual:   " String -> String -> String
forall a. [a] -> [a] -> [a]
++ SymCreationIndex -> String
forall a. Show a => a -> String
show SymCreationIndex
actualSymbolics ]
    Bool -> PostconditionM (RunMonad m) Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> PostconditionM (RunMonad m) Bool)
-> Bool -> PostconditionM (RunMonad m) Bool
forall a b. (a -> b) -> a -> b
$ SymCreationIndex
actualSymbolics SymCreationIndex -> SymCreationIndex -> Bool
forall a. Eq a => a -> a -> Bool
== SymCreationIndex
expectedSymbolics
  postcondition (ModelState state, ModelState state)
_ (Observation _ p) LookUp (RunMonad m)
lookup Realized (RunMonad m) a
_ = do
    ChainState
cst <- PostconditionM (RunMonad m) ChainState
forall (m :: * -> *). HasChainIndex m => m ChainState
getChainState
    Bool -> PostconditionM (RunMonad m) Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> PostconditionM (RunMonad m) Bool)
-> Bool -> PostconditionM (RunMonad m) Bool
forall a b. (a -> b) -> a -> b
$ (forall t. HasSymbolicRep t => Symbolic t -> t)
-> ChainState -> Bool
p ((Var SymIndex -> SymIndex)
-> forall t. HasSymbolicRep t => Symbolic t -> t
translateSymbolic Var SymIndex -> SymIndex
LookUp (RunMonad m)
lookup) ChainState
cst
  -- TODO: maybe add that current slot should equal the awaited slot?
  postcondition (ModelState state, ModelState state)
_ Action (ModelState state) a
_ LookUp (RunMonad m)
_ Realized (RunMonad m) a
_ = Bool -> PostconditionM (RunMonad m) Bool
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True

  monitoring :: (ModelState state, ModelState state)
-> Action (ModelState state) a
-> LookUp (RunMonad m)
-> Realized (RunMonad m) a
-> Property
-> Property
monitoring (ModelState state
s0, ModelState state
s1) (ContractAction _ act) LookUp (RunMonad m)
env Realized (RunMonad m) a
symIndex =
    (ModelState state, ModelState state)
-> Action state
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> SymIndex
-> Property
-> Property
forall state (m :: * -> *).
RunModel state m =>
(ModelState state, ModelState state)
-> Action state
-> (forall t. HasSymbolicRep t => Symbolic t -> t)
-> SymIndex
-> Property
-> Property
monitoring @_ @m (ModelState state
s0, ModelState state
s1) Action state
act forall t. HasSymbolicRep t => Symbolic t -> t
lookup Realized (RunMonad m) a
SymIndex
symIndex
    where lookup :: HasSymbolicRep t => Symbolic t -> t
          lookup :: Symbolic t -> t
lookup Symbolic t
sym = case SymIndex -> Symbolic t -> Maybe t
forall t. HasSymbolicRep t => SymIndex -> Symbolic t -> Maybe t
lookupSymbolic (Var SymIndex -> Realized (RunMonad m) SymIndex
LookUp (RunMonad m)
env (Var SymIndex -> Realized (RunMonad m) SymIndex)
-> Var SymIndex -> Realized (RunMonad m) SymIndex
forall a b. (a -> b) -> a -> b
$ Symbolic t -> Var SymIndex
forall k (t :: k). Symbolic t -> Var SymIndex
symVar Symbolic t
sym) Symbolic t
sym of
                            Maybe t
Nothing -> String -> t
forall a. HasCallStack => String -> a
error (String -> t) -> String -> t
forall a b. (a -> b) -> a -> b
$ String
"Unbound symbolic: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbolic t -> String
forall a. Show a => a -> String
show Symbolic t
sym
                            Just t
v  -> t
v
  monitoring (ModelState state
s0, ModelState state
_) (WaitUntil n@(SlotNo _n)) LookUp (RunMonad m)
_ Realized (RunMonad m) a
_ =
    String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Wait interval" (Word64 -> Word64 -> [String]
forall a. (Num a, Ord a, Show a, Integral a) => a -> a -> [String]
bucket Word64
10 Word64
diff) (Property -> Property)
-> (Property -> Property) -> Property -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    String -> [String] -> Property -> Property
forall prop.
Testable prop =>
String -> [String] -> prop -> Property
tabulate String
"Wait until" (Word64 -> Word64 -> [String]
forall a. (Num a, Ord a, Show a, Integral a) => a -> a -> [String]
bucket Word64
10 Word64
_n)
    where SlotNo Word64
diff = SlotNo
n SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
- ModelState state
s0 ModelState state
-> Getting SlotNo (ModelState state) SlotNo -> SlotNo
forall s a. s -> Getting a s a -> a
^. Getting SlotNo (ModelState state) SlotNo
forall state. Getter (ModelState state) SlotNo
currentSlot
  monitoring (ModelState state, ModelState state)
_ Observation{} LookUp (RunMonad m)
_ Realized (RunMonad m) a
_ = Property -> Property
forall a. a -> a
id

data ContractModelResult state = ContractModelResult
  { ContractModelResult state -> ModelState state
finalModelState :: ModelState state
  , ContractModelResult state -> Map SymToken AssetId
symbolicTokens  :: Map SymToken AssetId
  , ContractModelResult state -> ChainIndex
finalChainIndex :: ChainIndex
  }

runContractModel :: (ContractModel state, RunModel state m, HasChainIndex m)
                 => Actions state
                 -> PropertyM (RunMonad m) (ContractModelResult state)
runContractModel :: Actions state -> PropertyM (RunMonad m) (ContractModelResult state)
runContractModel Actions state
as = do
  (Annotated (ModelState state)
st, Env (RunMonad m)
env) <- Actions (ModelState state)
-> PropertyM
     (RunMonad m) (Annotated (ModelState state), Env (RunMonad m))
forall state (m :: * -> *).
(StateModel state, RunModel state m) =>
Actions state -> PropertyM m (Annotated state, Env m)
StateModel.runActions (Actions (ModelState state)
 -> PropertyM
      (RunMonad m) (Annotated (ModelState state), Env (RunMonad m)))
-> Actions (ModelState state)
-> PropertyM
     (RunMonad m) (Annotated (ModelState state), Env (RunMonad m))
forall a b. (a -> b) -> a -> b
$ Actions state -> Actions (ModelState state)
forall state.
ContractModel state =>
Actions state -> Actions (ModelState state)
toStateModelActions Actions state
as
  ChainIndex
ci        <- RunMonad m ChainIndex -> PropertyM (RunMonad m) ChainIndex
forall (m :: * -> *) a. Monad m => m a -> PropertyM m a
run RunMonad m ChainIndex
forall (m :: * -> *). HasChainIndex m => m ChainIndex
getChainIndex
  ContractModelResult state
-> PropertyM (RunMonad m) (ContractModelResult state)
forall (m :: * -> *) a. Monad m => a -> m a
return (ContractModelResult state
 -> PropertyM (RunMonad m) (ContractModelResult state))
-> ContractModelResult state
-> PropertyM (RunMonad m) (ContractModelResult state)
forall a b. (a -> b) -> a -> b
$ ContractModelResult :: forall state.
ModelState state
-> Map SymToken AssetId -> ChainIndex -> ContractModelResult state
ContractModelResult { finalModelState :: ModelState state
finalModelState = Annotated (ModelState state) -> ModelState state
forall state. Annotated state -> state
StateModel.underlyingState Annotated (ModelState state)
st
                               -- Note, this is safe because we know what actions there
                               -- are at the StateModel level - only waits and underlying
                               -- actions that return new symtokens.
                               , symbolicTokens :: Map SymToken AssetId
symbolicTokens = [(SymToken, AssetId)] -> Map SymToken AssetId
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(SymToken, AssetId)] -> Map SymToken AssetId)
-> [(SymToken, AssetId)] -> Map SymToken AssetId
forall a b. (a -> b) -> a -> b
$ [ (Var SymIndex -> String -> SymToken
forall k (t :: k). Var SymIndex -> String -> Symbolic t
Symbolic Var SymIndex
v String
s, AssetId
ai)
                                                                 | Var SymIndex
v StateModel.:=? Realized (RunMonad m) SymIndex
m <- Env (RunMonad m)
env
                                                                 , (String
s, AssetId
ai) <- Map String AssetId -> [(String, AssetId)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map String AssetId -> [(String, AssetId)])
-> Map String AssetId -> [(String, AssetId)]
forall a b. (a -> b) -> a -> b
$ Realized (RunMonad m) SymIndex
SymIndex
m SymIndex
-> Getting (Map String AssetId) SymIndex (Map String AssetId)
-> Map String AssetId
forall s a. s -> Getting a s a -> a
^. Getting (Map String AssetId) SymIndex (Map String AssetId)
forall (f :: * -> *). Lens' (SymIndexF f) (f AssetId)
tokens
                                                                 ]
                               , finalChainIndex :: ChainIndex
finalChainIndex = ChainIndex
ci
                               }

data BalanceChangeOptions = BalanceChangeOptions
  { BalanceChangeOptions -> Bool
observeScriptValue   :: Bool
  , BalanceChangeOptions -> FeeCalculation
feeCalucation        :: FeeCalculation
  , BalanceChangeOptions -> ProtocolParameters
protocolParameters   :: ProtocolParameters
  , BalanceChangeOptions -> AddressInEra Era -> String
addressPrettyPrinter :: AddressInEra Era -> String
  }

assertBalanceChangesMatch :: BalanceChangeOptions
                          -> ContractModelResult state
                          -> Property
assertBalanceChangesMatch :: BalanceChangeOptions -> ContractModelResult state -> Property
assertBalanceChangesMatch (BalanceChangeOptions Bool
observeScript FeeCalculation
computeFees ProtocolParameters
protoParams AddressInEra Era -> String
addressPrettyPrinter)
                          ContractModelResult{Map SymToken AssetId
ModelState state
ChainIndex
finalChainIndex :: ChainIndex
symbolicTokens :: Map SymToken AssetId
finalModelState :: ModelState state
finalChainIndex :: forall state. ContractModelResult state -> ChainIndex
symbolicTokens :: forall state. ContractModelResult state -> Map SymToken AssetId
finalModelState :: forall state. ContractModelResult state -> ModelState state
..} =
  let symbolicBalanceChanges :: Map (AddressInEra Era) SymValue
symbolicBalanceChanges  = ModelState state -> Map (AddressInEra Era) SymValue
forall state. ModelState state -> Map (AddressInEra Era) SymValue
_balanceChanges ModelState state
finalModelState
      predictedBalanceChanges :: Map (AddressInEra Era) Value
predictedBalanceChanges = Map (AddressInEra Era) Value -> Map (AddressInEra Era) Value
filterScripts (Map (AddressInEra Era) Value -> Map (AddressInEra Era) Value)
-> Map (AddressInEra Era) Value -> Map (AddressInEra Era) Value
forall a b. (a -> b) -> a -> b
$ (SymValue -> Value)
-> Map (AddressInEra Era) SymValue -> Map (AddressInEra Era) Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((SymToken -> AssetId) -> SymValue -> Value
toValue (Maybe AssetId -> AssetId
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe AssetId -> AssetId)
-> (SymToken -> Maybe AssetId) -> SymToken -> AssetId
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SymToken -> Map SymToken AssetId -> Maybe AssetId)
-> Map SymToken AssetId -> SymToken -> Maybe AssetId
forall a b c. (a -> b -> c) -> b -> a -> c
flip SymToken -> Map SymToken AssetId -> Maybe AssetId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Map SymToken AssetId
symbolicTokens)) Map (AddressInEra Era) SymValue
symbolicBalanceChanges
      actualBalanceChanges :: Map (AddressInEra Era) Value
actualBalanceChanges    = Map (AddressInEra Era) Value -> Map (AddressInEra Era) Value
filterScripts (Map (AddressInEra Era) Value -> Map (AddressInEra Era) Value)
-> Map (AddressInEra Era) Value -> Map (AddressInEra Era) Value
forall a b. (a -> b) -> a -> b
$ ChainIndex -> FeeCalculation -> Map (AddressInEra Era) Value
getBalanceChangesDiscountingFees ChainIndex
finalChainIndex FeeCalculation
computeFees
      minAda :: Lovelace
minAda                  = [Lovelace] -> Lovelace
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Lovelace] -> Lovelace) -> [Lovelace] -> Lovelace
forall a b. (a -> b) -> a -> b
$ ChainIndex -> ProtocolParameters -> [Lovelace]
allMinAda ChainIndex
finalChainIndex ProtocolParameters
protoParams
      prettyChanges :: Map (AddressInEra Era) Doc -> Doc
prettyChanges Map (AddressInEra Era) Doc
changes   = [Doc] -> Doc
vcat
                                  [ [Doc] -> Doc
sep [ String -> Doc
text (AddressInEra Era -> String
addressPrettyPrinter AddressInEra Era
addr) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
":", Int -> Doc -> Doc
nest Int
2 Doc
val ]
                                  | (AddressInEra Era
addr, Doc
val) <- Map (AddressInEra Era) Doc -> [(AddressInEra Era, Doc)]
forall k a. Map k a -> [(k, a)]
Map.toList Map (AddressInEra Era) Doc
changes ]
      msg :: String
msg = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> Doc -> String
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
             [ Doc
"Balance changes don't match:"
             , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ [Doc] -> Doc
vcat
               [ [Doc] -> Doc
sep [ Doc
"Predicted symbolic balance changes:"
                     , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Map (AddressInEra Era) Doc -> Doc
prettyChanges (Map (AddressInEra Era) Doc -> Doc)
-> Map (AddressInEra Era) Doc -> Doc
forall a b. (a -> b) -> a -> b
$ SymValue -> Doc
forall a. Pretty a => a -> Doc
pPrint (SymValue -> Doc)
-> Map (AddressInEra Era) SymValue -> Map (AddressInEra Era) Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (AddressInEra Era) SymValue
symbolicBalanceChanges ]
               , [Doc] -> Doc
sep [ Doc
"Predicted actual balance changes:"
                     , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Map (AddressInEra Era) Doc -> Doc
prettyChanges (Map (AddressInEra Era) Doc -> Doc)
-> Map (AddressInEra Era) Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Value -> Doc
pPrintValue (Value -> Doc)
-> Map (AddressInEra Era) Value -> Map (AddressInEra Era) Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (AddressInEra Era) Value
predictedBalanceChanges ]
               , [Doc] -> Doc
sep [ Doc
"Actual balance changes:"
                     , Int -> Doc -> Doc
nest Int
2 (Doc -> Doc) -> Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Map (AddressInEra Era) Doc -> Doc
prettyChanges (Map (AddressInEra Era) Doc -> Doc)
-> Map (AddressInEra Era) Doc -> Doc
forall a b. (a -> b) -> a -> b
$ Value -> Doc
pPrintValue (Value -> Doc)
-> Map (AddressInEra Era) Value -> Map (AddressInEra Era) Doc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (AddressInEra Era) Value
actualBalanceChanges ]
               , Doc
"Sum of min Lovelace:" Doc -> Doc -> Doc
<+> String -> Doc
text (Lovelace -> String
forall a. Show a => a -> String
show Lovelace
minAda)
               ]
             ]
      filterScripts :: Map (AddressInEra Era) Value -> Map (AddressInEra Era) Value
filterScripts Map (AddressInEra Era) Value
m
        | Bool
observeScript = Map (AddressInEra Era) Value
m
        | Bool
otherwise     = (AddressInEra Era -> Value -> Bool)
-> Map (AddressInEra Era) Value -> Map (AddressInEra Era) Value
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ AddressInEra Era
k Value
_ -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ AddressInEra Era -> Bool
forall era. AddressInEra era -> Bool
isScriptAddress AddressInEra Era
k) Map (AddressInEra Era) Value
m

      -- TODO: this is a hack because the module we need isn't exported. WTF?!
      isScriptAddress :: AddressInEra era -> Bool
isScriptAddress (AddressInEra (ShelleyAddressInEra ShelleyBasedEra era
_) Address addrtype
addr) = Maybe PubKeyHash -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe PubKeyHash -> Bool) -> Maybe PubKeyHash -> Bool
forall a b. (a -> b) -> a -> b
$ Address ShelleyAddr -> Maybe PubKeyHash
shelleyPayAddrToPlutusPubKHash Address addrtype
Address ShelleyAddr
addr
      isScriptAddress AddressInEra era
_ = Bool
False

  in String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
msg (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Lovelace
-> Map (AddressInEra Era) Value
-> Map (AddressInEra Era) Value
-> Bool
checkEqualUpToMinAda Lovelace
minAda Map (AddressInEra Era) Value
predictedBalanceChanges Map (AddressInEra Era) Value
actualBalanceChanges
  where
    checkEqualUpToMinAda :: Lovelace
                         -> Map (AddressInEra Era) Value
                         -> Map (AddressInEra Era) Value
                         -> Bool
    checkEqualUpToMinAda :: Lovelace
-> Map (AddressInEra Era) Value
-> Map (AddressInEra Era) Value
-> Bool
checkEqualUpToMinAda Lovelace
l Map (AddressInEra Era) Value
m Map (AddressInEra Era) Value
m' =
      (Value -> Bool) -> Map (AddressInEra Era) Value -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (((AssetId, Quantity) -> Bool) -> [(AssetId, Quantity)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (AssetId, Quantity) -> Bool
isOk ([(AssetId, Quantity)] -> Bool)
-> (Value -> [(AssetId, Quantity)]) -> Value -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value -> [(AssetId, Quantity)]
valueToList) (Map (AddressInEra Era) Value -> Bool)
-> Map (AddressInEra Era) Value -> Bool
forall a b. (a -> b) -> a -> b
$ (Value -> Value -> Value)
-> Map (AddressInEra Era) Value
-> Map (AddressInEra Era) Value
-> Map (AddressInEra Era) Value
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Value -> Value -> Value
forall a. Semigroup a => a -> a -> a
(<>) Map (AddressInEra Era) Value
m (Value -> Value
negateValue (Value -> Value)
-> Map (AddressInEra Era) Value -> Map (AddressInEra Era) Value
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map (AddressInEra Era) Value
m')
      where
        isOk :: (AssetId, Quantity) -> Bool
isOk (AssetId
AdaAssetId, Quantity
q) = Quantity -> Quantity
forall a. Num a => a -> a
abs Quantity
q Quantity -> Quantity -> Bool
forall a. Ord a => a -> a -> Bool
<= Lovelace -> Quantity
lovelaceToQuantity Lovelace
l
        isOk (AssetId
_, Quantity
q)          = Quantity
q Quantity -> Quantity -> Bool
forall a. Eq a => a -> a -> Bool
== Quantity
0