Merge pull request #18 from input-output-hk/PR-symbolic-addition

Add support for symbolic TxIn

quickcheck-contractmodel/quickcheck-contractmodel.cabal

@@ -1,6 +1,6 @@
 cabal-version:      2.4
 name:               quickcheck-contractmodel
-version:            0.1.4.0
+version:            0.1.4.1
 
 -- A short (one-line) description of the package.
 -- synopsis:

quickcheck-contractmodel/src/Test/QuickCheck/ContractModel.hs

@@ -13,8 +13,10 @@ module Test.QuickCheck.ContractModel
   , runContractModel
   , liftRunMonad
   , contractState
+  , registerSymbolic
   , registerToken
   , registerTxOut
+  , registerTxIn
     -- * Chain index
   , HasChainIndex(..)
   , ChainIndex(..)
@@ -25,11 +27,12 @@ module Test.QuickCheck.ContractModel
     --
     -- NOTE: we don't export the internals here because
     -- it's important that you can't tell the difference
-    -- between differnelty numbered SymTokens as these are
-    -- not guaranteed to be stable.
+    -- between differently numbered Symbolics as these numbers
+    -- are not guaranteed to be stable.
   , Symbolic
   , SymToken
   , SymTxOut
+  , SymTxIn
   , SymValue
   , symIsZero
   , symLeq
@@ -66,8 +69,10 @@ module Test.QuickCheck.ContractModel
   , askContractState
   , viewModelState
   , viewContractState
+  , createSymbolic
   , createToken
   , createTxOut
+  , createTxIn
   , mint
   , burn
   , deposit

quickcheck-contractmodel/src/Test/QuickCheck/ContractModel/Internal.hs

@@ -39,7 +39,7 @@ class (ContractModel state, IsRunnable m) => RunModel state m where
   -- a` instances from previous steps.
   perform :: ModelState state
           -> Action state
-          -> (SymToken -> AssetId)
+          -> (forall t. HasSymbolicRep t => Symbolic t -> t)
           -> RunMonad m ()
 
   -- | Allows the user to attach information to the `Property` at each step of the process.
@@ -48,7 +48,7 @@ class (ContractModel state, IsRunnable m) => RunModel state m where
   -- while executing this step.
   monitoring :: (ModelState state, ModelState state)
              -> Action state
-             -> (SymToken -> AssetId)
+             -> (forall t. HasSymbolicRep t => Symbolic t -> t)
              -> SymIndex
              -> Property
              -> Property
@@ -64,11 +64,20 @@ liftRunMonad f (RunMonad (WriterT m)) = RunMonad . WriterT $ f m
 instance Monad m => MonadFail (RunMonad m) where
   fail = error
 
+registerSymbolic :: (Monad m, HasSymbolicRep t)
+                 => String
+                 -> t
+                 -> RunMonad m ()
+registerSymbolic s = tell . symIndex s
+
 registerToken :: Monad m => String -> AssetId -> RunMonad m ()
-registerToken s asset = tell $ symIndex s asset
+registerToken = registerSymbolic
 
 registerTxOut :: Monad m => String -> TxOut CtxUTxO Era -> RunMonad m ()
-registerTxOut s utxo = tell $ symIndex s utxo
+registerTxOut = registerSymbolic
+
+registerTxIn :: Monad m => String -> TxIn -> RunMonad m ()
+registerTxIn = registerSymbolic
 
 withLocalSymbolics :: Monad m => RunMonad m () -> RunMonad m SymIndex
 withLocalSymbolics m = censor (const mempty) . fmap snd . listen $ m
@@ -141,9 +150,10 @@ instance ( IsRunnable m
 
   monitoring (s0, s1) (ContractAction _ act) env symIndex =
     monitoring @_ @m (s0, s1) act lookup symIndex
-    where lookup token = case lookupSymbolic (env $ symVar token) token  of
-                            Nothing  -> error $ "Unbound token: " ++ show token
-                            Just aid -> aid
+    where lookup :: HasSymbolicRep t => Symbolic t -> t
+          lookup sym = case lookupSymbolic (env $ symVar sym) sym of
+                            Nothing -> error $ "Unbound symbolic: " ++ show sym
+                            Just v  -> v
   monitoring (s0, _) (WaitUntil n@(SlotNo _n)) _ _ =
     tabulate "Wait interval" (bucket 10 diff) .
     tabulate "Wait until" (bucket 10 _n)

quickcheck-contractmodel/src/Test/QuickCheck/ContractModel/Internal/Spec.hs

@@ -150,21 +150,26 @@ symbolicsCreatedBy :: Spec state ()
                    -> SymCreationIndex
 symbolicsCreatedBy (Spec spec) v s = flip State.evalState s $ runReaderT (snd <$> Writer.runWriterT spec) v
 
+createSymbolic :: forall t state. HasSymbolicRep t => String -> Spec state (Symbolic t)
+createSymbolic key = Spec $ do
+  var <- ask
+  Writer.tell $ createIndex @t key
+  pure $ Symbolic var key
+
 -- | Create a new symbolic token in `nextState` - must have a
 -- corresponding `registerToken` call in `perform`
 createToken :: String -> Spec state SymToken
-createToken key = Spec $ do
-  var <- ask
-  Writer.tell $ createIndex @AssetId key
-  pure $ Symbolic var key
+createToken = createSymbolic
 
 -- | Create a new symbolic TxOut in `nextState` - must have a
 -- corresponding `registerTxOut` call in `perform`
 createTxOut :: String -> Spec state SymTxOut
-createTxOut key = Spec $ do
-  var <- ask
-  Writer.tell $ createIndex @(TxOut CtxUTxO Era) key
-  pure $ Symbolic var key
+createTxOut = createSymbolic
+
+-- | Create a new symbolic TxIn in `nextState` - must have a
+-- corresponding `registerTxIn` call in `perform`
+createTxIn :: String -> Spec state SymTxIn
+createTxIn = createSymbolic
 
 -- | Mint tokens. Minted tokens start out as `lockedValue` (i.e. owned by the contract) and can be
 --   transferred to wallets using `deposit`.

quickcheck-contractmodel/src/Test/QuickCheck/ContractModel/Internal/Symbolics.hs

@@ -3,7 +3,7 @@
 {-# LANGUAGE AllowAmbiguousTypes #-}
 module Test.QuickCheck.ContractModel.Internal.Symbolics where
 
-import Cardano.Api
+import Cardano.Api hiding (txIns)
 import Control.Lens
 
 import Test.QuickCheck.StateModel
@@ -26,6 +26,7 @@ import Text.PrettyPrint.HughesPJClass hiding ((<>))
 
 data SymIndexF f = SymIndex { _tokens :: f AssetId
                             , _utxos  :: f (TxOut CtxUTxO Era)
+                            , _txIns  :: f TxIn
                             } deriving stock Generic
                               deriving anyclass (ConstraintsB, FunctorB, ApplicativeB, TraversableB)
 makeLenses ''SymIndexF
@@ -37,13 +38,17 @@ class HasSymbolicRep t where
   symIndexL :: Lens' (SymIndexF f) (f t)
   symPrefix :: String
 
+instance HasSymbolicRep AssetId where
+  symIndexL = tokens
+  symPrefix = "tok"
+
 instance HasSymbolicRep (TxOut CtxUTxO Era) where
   symIndexL = utxos
   symPrefix = "txOut"
 
-instance HasSymbolicRep AssetId where
-  symIndexL = tokens
-  symPrefix = "tok"
+instance HasSymbolicRep TxIn where
+  symIndexL = txIns
+  symPrefix = "txIn"
 
 -- Semigroup and Monoids --------------------------------------------------
 
@@ -147,11 +152,14 @@ instance HasVariables (Symbolic t) where
 lookupSymbolic :: HasSymbolicRep t => SymIndex -> Symbolic t -> Maybe t
 lookupSymbolic idx s = idx ^. symIndexL . at (symVarIdx s)
 
+-- | A symbolic token is a token that is only available at runtime
+type SymToken = Symbolic AssetId
+
 -- | A SymTxOut is a `TxOut CtxUTxO Era` that is only available at runtime
 type SymTxOut = Symbolic (TxOut CtxUTxO Era)
 
--- | A symbolic token is a token that is only available at runtime
-type SymToken = Symbolic AssetId
+-- | A SymTxIn is a `TxIn` that is only available at runtime
+type SymTxIn = Symbolic TxIn
 
 -- Symbolic values --------------------------------------------------------