ContractModel: Improve error messages and statistics reporting

plutus-contract/src/Plutus/Contract/Test.hs

@@ -549,7 +549,8 @@ walletFundsChangeImpl exact w dlt =
                 (if exact then [] else ["  (excluding" <+> viaShow (Ada.getLovelace (Ada.fromValue fees)) <+> "lovelace in fees)" ]) ++
                 if initialValue == finalValue
                 then ["but they did not change"]
-                else ["but they changed by", " " <+> viaShow (finalValue P.- initialValue)]
+                else ["but they changed by", " " <+> viaShow (finalValue P.- initialValue),
+                      "a discrepancy of",    " " <+> viaShow (finalValue P.- initialValue P.- dlt)]
         pure result
 
 walletPaidFees :: Wallet -> Value -> TracePredicate

plutus-contract/src/Plutus/Contract/Test/ContractModel.hs

@@ -58,6 +58,7 @@ module Plutus.Contract.Test.ContractModel
     -- $dynamicLogic
     , DL
     , action
+    , waitUntilDL
     , anyAction
     , anyActions
     , anyActions_
@@ -99,6 +100,7 @@ module Plutus.Contract.Test.ContractModel
     -- ** Model properties
     , propSanityCheckModel
     , propSanityCheckAssertions
+    , propSanityCheckReactive
     -- ** Coverage cheking options
     , CoverageOptions
     , defaultCoverageOptions

plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs

@@ -2,7 +2,7 @@
 module Plutus.Contract.Test.ContractModel.Symbolics where
 
 import Ledger.Ada qualified as Ada
-import Ledger.Value (AssetClass, Value, assetClassValue, isZero, leq)
+import Ledger.Value (AssetClass, Value, assetClassValue, assetClassValueOf, isZero, leq)
 import PlutusTx.Monoid qualified as PlutusTx
 
 import Data.Aeson qualified as JSON
@@ -30,14 +30,15 @@ import Test.QuickCheck.StateModel hiding (Action, Actions, arbitraryAction, init
   inner monad.
 -}
 
--- | Symbolic tokens and values
 newtype AssetKey = AssetKey Int deriving (Ord, Eq, Show, Num, JSON.FromJSONKey, JSON.ToJSONKey)
+-- | A symbolic token is a token that exists only during ContractModel generation time
 data SymToken = SymToken { symVar :: Var AssetKey, symVarIdx :: String } deriving (Ord, Eq)
+-- | A symbolic value is a combination of a real value and a value associating symbolic
+-- tokens with an amount
 data SymValue = SymValue { symValMap :: Map SymToken Integer, actualValPart :: Value } deriving (Show)
 
 instance Show SymToken where
   show (SymToken (Var i) n) = "tok" ++ show i ++ "." ++ n
-
 instance Semigroup SymValue where
   (SymValue m v) <> (SymValue m' v') = SymValue (Map.unionWith (+) m m') (v <> v')
 instance Monoid SymValue where
@@ -53,19 +54,23 @@ symIsZero (SymValue m v) = all (==0) m && isZero v
 symLeq :: SymValue -> SymValue -> Bool
 symLeq (SymValue m v) (SymValue m' v') = v `leq` v' && all (<=0) (Map.unionWith (+) m (negate <$> m'))
 
-symLeqWiggle :: Integer -> SymValue -> SymValue -> Bool
-symLeqWiggle w (SymValue m v) (SymValue m' v') = v `leq` v' && all (<=w) (Map.unionWith (+) m (negate <$> m'))
-
-symAssetClassValue :: SymToken -> Integer -> SymValue
-symAssetClassValue _ 0 = SymValue mempty mempty
-symAssetClassValue t i = SymValue (Map.singleton t i) mempty
-
+-- | Using a semantics function for symbolic tokens, convert a SymValue to a Value
 toValue :: (SymToken -> AssetClass) -> SymValue -> Value
 toValue symTokenMap (SymValue m v) = v <> fold [ assetClassValue (symTokenMap t) v | (t, v) <- Map.toList m ]
 
+-- Negate a symbolic value
+inv :: SymValue -> SymValue
+inv (SymValue m v) = SymValue (negate <$> m) (PlutusTx.inv v)
+
 class SymValueLike v where
   toSymValue :: v -> SymValue
 
+class TokenLike t where
+  -- | Get the value of a specific token in a `SymValue`
+  symAssetClassValueOf :: SymValue -> t -> Integer
+  -- | Convert a token and an amount to a `SymValue`
+  symAssetClassValue :: t -> Integer -> SymValue
+
 instance SymValueLike Value where
   toSymValue = SymValue mempty
 
@@ -75,5 +80,12 @@ instance SymValueLike SymValue where
 instance SymValueLike Ada.Ada where
   toSymValue = toSymValue . Ada.toValue
 
-inv :: SymValue -> SymValue
-inv (SymValue m v) = SymValue (negate <$> m) (PlutusTx.inv v)
+instance TokenLike SymToken where
+  symAssetClassValueOf (SymValue svm _) t = sum $ Map.lookup t svm
+
+  symAssetClassValue _ 0 = SymValue mempty mempty
+  symAssetClassValue t i = SymValue (Map.singleton t i) mempty
+
+instance TokenLike AssetClass where
+  symAssetClassValueOf (SymValue _ v) t = assetClassValueOf v t
+  symAssetClassValue t i = toSymValue $ assetClassValue t i

plutus-use-cases/test/Spec/Auction.hs

@@ -12,6 +12,7 @@ module Spec.Auction
     , options
     , auctionTrace1
     , auctionTrace2
+    , AuctionModel
     , prop_Auction
     , prop_FinishAuction
     , prop_NoLockedFunds
@@ -163,7 +164,7 @@ data AuctionModel = AuctionModel
     , _winner     :: Wallet
     , _endSlot    :: Slot
     , _phase      :: Phase
-    } deriving (Show)
+    } deriving (Show, Eq)
 
 data Phase = NotStarted | Bidding | AuctionOver
     deriving (Eq, Show)
@@ -179,7 +180,7 @@ instance ContractModel AuctionModel where
         SellerH :: ContractInstanceKey AuctionModel AuctionOutput SellerSchema AuctionError ()
         BuyerH  :: Wallet -> ContractInstanceKey AuctionModel AuctionOutput BuyerSchema AuctionError ()
 
-    data Action AuctionModel = Init Wallet | Bid Wallet Integer | WaitUntil Slot
+    data Action AuctionModel = Init Wallet | Bid Wallet Integer
         deriving (Eq, Show)
 
     initialState = AuctionModel
@@ -198,23 +199,23 @@ instance ContractModel AuctionModel where
     instanceContract _ BuyerH{} _ = buyer threadToken
 
     arbitraryAction s
-        | p /= NotStarted =
-            frequency $  [ (1, WaitUntil . step <$> choose (1, 10 :: Integer)) ]
-                      ++ [ (3, Bid w <$> chooseBid (lo,hi))
-                         | w <- [w2, w3, w4]
-                         , let (lo,hi) = validBidRange s w
-                         , lo <= hi ]
+        | p /= NotStarted = do
+            oneof [ Bid w <$> chooseBid (lo,hi)
+                  | w <- [w2, w3, w4]
+                  , let (lo,hi) = validBidRange s w
+                  , lo <= hi ]
         | otherwise = pure $ Init w1
         where
             p    = s ^. contractState . phase
-            slot = s ^. currentSlot
-            step n = slot + fromIntegral n
+
+    waitProbability s
+      | s ^. contractState . phase /= NotStarted
+      , all (uncurry (>) . validBidRange s) [w2, w3, w4] = 1
+      | otherwise = 0.1
 
     precondition s (Init _) = s ^. contractState . phase == NotStarted
     precondition s cmd      = s ^. contractState . phase /= NotStarted &&
         case cmd of
-            WaitUntil slot -> slot > s ^. currentSlot
-
             -- In order to place a bid, we need to satisfy the constraint where
             -- each tx output must have at least N Ada.
             Bid w bid      -> let (lo,hi) = validBidRange s w in
@@ -240,7 +241,6 @@ instance ContractModel AuctionModel where
                 phase .= Bidding
                 withdraw w1 $ Ada.toValue Ledger.minAdaTxOut <> theToken
                 wait 3
-            WaitUntil slot' -> waitUntil slot'
             Bid w bid -> do
                 current <- viewContractState currentBid
                 leader  <- viewContractState winner
@@ -252,7 +252,6 @@ instance ContractModel AuctionModel where
                 wait 2
 
     perform _ _ _ (Init _) = delay 3
-    perform _ _ _ (WaitUntil slot) = void $ Trace.waitUntilSlot slot
     perform handle _ _ (Bid w bid) = do
         -- FIXME: You cannot bid in certain slots when the off-chain code is busy, so to make the
         --        tests pass we send two identical bids in consecutive slots. The off-chain code is
@@ -265,9 +264,7 @@ instance ContractModel AuctionModel where
         delay 1
 
     shrinkAction _ (Init _)  = []
-    shrinkAction _ (WaitUntil (Slot n))  = [ WaitUntil (Slot n') | n' <- shrink n ]
-    shrinkAction s (Bid w v) =
-        WaitUntil (s ^. currentSlot + 1) : [ Bid w v' | v' <- shrink v ]
+    shrinkAction _ (Bid w v) = [ Bid w v' | v' <- shrink v ]
 
     monitoring _ (Bid _ bid) =
       classify (Ada.lovelaceOf bid == Ada.adaOf 100 - (Ledger.minAdaTxOut <> Ledger.maxFee))
@@ -312,7 +309,7 @@ finishAuction = do
     action $ Init w1
     anyActions_
     slot <- viewModelState currentSlot
-    when (slot < 101) $ action $ WaitUntil 101
+    when (slot < 101) $ waitUntilDL 101
     assertModel "Locked funds are not zero" (symIsZero . lockedValue)
 
 prop_FinishAuction :: Property
@@ -330,10 +327,10 @@ noLockProof = defaultNLFP
       p <- viewContractState phase
       when (p == NotStarted) $ action $ Init w1
       slot <- viewModelState currentSlot
-      when (slot < 101) $ action $ WaitUntil 101
+      when (slot < 101) $ waitUntilDL 101
 
 prop_NoLockedFunds :: Property
-prop_NoLockedFunds = checkNoLockedFundsProof options noLockProof
+prop_NoLockedFunds = checkNoLockedFundsProof (set minLogLevel Critical options) noLockProof
 
 tests :: TestTree
 tests =
@@ -359,4 +356,6 @@ tests =
             withMaxSuccess 10 prop_FinishAuction
         , testProperty "NLFP fails" $
             expectFailure $ noShrinking prop_NoLockedFunds
+        , testProperty "prop_Reactive" $
+            withMaxSuccess 1000 (propSanityCheckReactive @AuctionModel)
         ]

plutus-use-cases/test/Spec/Crowdfunding.hs

@@ -186,7 +186,6 @@ deriving instance Show (ContractInstanceKey CrowdfundingModel w schema err param
 
 instance ContractModel CrowdfundingModel where
   data Action CrowdfundingModel = CContribute Wallet Value
-                                | CWaitUntil Slot
                                 | CStart
 
   data ContractInstanceKey CrowdfundingModel w schema err params where
@@ -210,12 +209,10 @@ instance ContractModel CrowdfundingModel where
   instanceContract _ ContributorKey{} _ = crowdfunding params
 
   perform h _ s a = case a of
-    CWaitUntil slot -> void $ Trace.waitUntilSlot slot
     CContribute w v -> Trace.callEndpoint @"contribute" (h $ ContributorKey w) Contribution{contribValue=v}
     CStart          -> Trace.callEndpoint @"schedule collection" (h $ OwnerKey $ s ^. contractState . ownerWallet) ()
 
   nextState a = case a of
-    CWaitUntil slot -> waitUntil slot
     CContribute w v -> do
       withdraw w v
       contributions $~ Map.insert w v
@@ -245,7 +242,6 @@ instance ContractModel CrowdfundingModel where
 
   -- The 'precondition' says when a particular command is allowed.
   precondition s cmd = case cmd of
-    CWaitUntil slot -> slot > s ^. currentSlot
     -- In order to contribute, we need to satisfy the constraint where each tx
     -- output must have at least N Ada.
     CContribute w v -> w `notElem` Map.keys (s ^. contractState . contributions)
@@ -256,9 +252,8 @@ instance ContractModel CrowdfundingModel where
 
   -- To generate a random test case we need to know how to generate a random
   -- command given the current model state.
+
   arbitraryAction s = oneof $
-    [ CWaitUntil . step <$> choose (1, 100 :: Integer) ]
-    ++
     [ CContribute <$> QC.elements availableWallets <*> (Ada.lovelaceValueOf . abs <$> choose (2000000, 100000000))
     | Prelude.not . null $ availableWallets
     , s ^. currentSlot < s ^. contractState . endSlot ]
@@ -267,12 +262,16 @@ instance ContractModel CrowdfundingModel where
     | Prelude.not (s ^. contractState . ownerOnline || s ^. contractState . ownerContractDone) ]
     where
       availableWallets = [ w | w <- contributorWallets, w `notElem` Map.keys (s ^. contractState . contributions) ]
-      slot = s ^. currentSlot
-      step n = slot + fromIntegral n
 
-  shrinkAction _ a = case a of
-    CWaitUntil s -> CWaitUntil . fromIntegral <$> (shrink . toInteger $ s)
-    _            -> []
+  waitProbability s
+    | Prelude.not . null $ availableWallets
+    , s ^. currentSlot < s ^. contractState . endSlot = 0.05
+    | Prelude.not (s ^. contractState . ownerOnline || s ^. contractState . ownerContractDone) = 0.05
+    | otherwise = 1
+    where
+      availableWallets = [ w | w <- contributorWallets, w `notElem` Map.keys (s ^. contractState . contributions) ]
+
+  shrinkAction _ _ = []
 
   monitoring _ _ = id
 

plutus-use-cases/test/Spec/Escrow.hs

@@ -6,7 +6,7 @@
 {-# LANGUAGE TypeApplications   #-}
 {-# LANGUAGE TypeFamilies       #-}
 {-# OPTIONS_GHC -fno-warn-name-shadowing #-}
-module Spec.Escrow(tests, redeemTrace, redeem2Trace, refundTrace, prop_Escrow, prop_FinishEscrow, prop_NoLockedFunds) where
+module Spec.Escrow(tests, redeemTrace, redeem2Trace, refundTrace, prop_Escrow, prop_FinishEscrow, prop_NoLockedFunds, EscrowModel) where
 
 import Control.Lens hiding (both)
 import Control.Monad (void, when)
@@ -57,7 +57,6 @@ instance ContractModel EscrowModel where
                           | Redeem Wallet
                           | Refund Wallet
                           | BadRefund Wallet Wallet
-                          | WaitUntil Slot
 
   data ContractInstanceKey EscrowModel w s e params where
     WalletKey :: Wallet -> ContractInstanceKey EscrowModel () EscrowTestSchema EscrowError ()
@@ -106,13 +105,10 @@ instance ContractModel EscrowModel where
       contributions %= Map.delete w
       deposit w v
       wait 1
-    WaitUntil s -> do
-      waitUntil s
     BadRefund _ _ -> do
       wait 2
 
   precondition s a = case a of
-    WaitUntil slot' -> s ^. currentSlot < slot'
     Redeem _ -> (s ^. contractState . contributions . to fold) `geq` (s ^. contractState . targets . to fold)
              && (s ^. currentSlot < s ^. contractState . refundSlot - 1)
     Refund w -> s ^. currentSlot >= s ^. contractState . refundSlot
@@ -123,7 +119,6 @@ instance ContractModel EscrowModel where
                    || w /= w'
 
   perform h _ _ a = case a of
-    WaitUntil slot -> void $ Trace.waitUntilSlot slot
     Pay w v        -> do
       Trace.callEndpoint @"pay-escrow" (h $ WalletKey w) (Ada.adaValueOf $ fromInteger v)
       delay 1
@@ -139,21 +134,15 @@ instance ContractModel EscrowModel where
 
   arbitraryAction s = frequency $ [ (prefer beforeRefund,  Pay <$> QC.elements testWallets <*> choose @Integer (10, 30))
                                   , (prefer beforeRefund,  Redeem <$> QC.elements testWallets)
-                                  , (1,                    WaitUntil . step <$> choose @Int (1, 10))
                                   , (prefer afterRefund,   BadRefund <$> QC.elements testWallets <*> QC.elements testWallets) ] ++
                                   [ (prefer afterRefund,   Refund <$> QC.elements (s ^. contractState . contributions . to Map.keys))
                                   | Prelude.not . null $ s ^. contractState . contributions . to Map.keys ]
                   where
                     slot = s ^. currentSlot
-                    step n = slot + fromIntegral n
                     beforeRefund = slot < s ^. contractState . refundSlot
                     afterRefund = Prelude.not beforeRefund
                     prefer b = if b then 10 else 1
 
-  shrinkAction _ (WaitUntil s) = WaitUntil . fromIntegral <$> (shrink . toInteger $ s)
-  -- TODO: This trick should be part of every model. We should make waiting a builtin thing
-  shrinkAction s _             = [WaitUntil $ s ^. currentSlot + n | n <- [1..10]]
-
   monitoring _ (Redeem _) = classify True "Contains Redeem"
   monitoring (_,_) (BadRefund w w') = tabulate "Bad refund attempts" [if w==w' then "early refund" else "steal refund"]
   monitoring (s,s') _ = classify (redeemable s' && Prelude.not (redeemable s)) "Redeemable"
@@ -175,7 +164,7 @@ finishingStrategy :: (Wallet -> Bool) -> DL EscrowModel ()
 finishingStrategy walletAlive = do
     now <- viewModelState currentSlot
     slot <- viewContractState refundSlot
-    when (now < slot+1) $ action $ WaitUntil $ slot+1
+    when (now < slot+1) $ waitUntilDL $ slot+1
     contribs <- viewContractState contributions
     monitor (classify (Map.null contribs) "no need for extra refund to recover funds")
     sequence_ [action $ Refund w | w <- testWallets, w `Map.member` contribs, walletAlive w]

plutus-use-cases/test/Spec/GameStateMachine.hs

@@ -197,8 +197,8 @@ prop_GameWhitelist = checkErrorWhitelist defaultWhitelist
 prop_SanityCheckModel :: Property
 prop_SanityCheckModel = propSanityCheckModel @GameModel
 
-prop_SanityCheckAssertions :: Property
-prop_SanityCheckAssertions = propSanityCheckAssertions @GameModel
+prop_SanityCheckAssertions :: Actions GameModel -> Property
+prop_SanityCheckAssertions = propSanityCheckAssertions
 
 check_prop_Game_with_coverage :: IO CoverageReport
 check_prop_Game_with_coverage =