Add statistics and NoLockedFunds tests to Escrow

Extend Escrow tests, add negative testing
Add NoLockedFunds to Escrow tests

plutus-use-cases/plutus-use-cases.cabal

@@ -108,6 +108,7 @@ test-suite plutus-use-cases-test
         Spec.Currency
         Spec.ErrorHandling
         Spec.Escrow
+        Spec.Escrow.Endpoints
         Spec.SimpleEscrow
         Spec.Future
         Spec.Game
@@ -175,6 +176,7 @@ executable plutus-use-cases-scripts
         Spec.Currency
         Spec.ErrorHandling
         Spec.Escrow
+        Spec.Escrow.Endpoints
         Spec.SimpleEscrow
         Spec.Future
         Spec.Game

plutus-use-cases/src/Plutus/Contracts/Escrow.hs

@@ -38,6 +38,8 @@ module Plutus.Contracts.Escrow(
     , RedeemSuccess(..)
     , RefundSuccess(..)
     , EscrowSchema
+    -- * Exposed for test endpoints
+    , Action(..)
     ) where
 
 import Control.Lens (makeClassyPrisms, review, view)

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

@@ -6,10 +6,10 @@
 {-# LANGUAGE TypeApplications   #-}
 {-# LANGUAGE TypeFamilies       #-}
 {-# OPTIONS_GHC -fno-warn-name-shadowing #-}
-module Spec.Escrow(tests, redeemTrace, redeem2Trace, refundTrace, prop_Escrow) where
+module Spec.Escrow(tests, redeemTrace, redeem2Trace, refundTrace, prop_Escrow, prop_FinishEscrow, prop_NoLockedFunds) where
 
 import Control.Lens hiding (both)
-import Control.Monad (void)
+import Control.Monad (void, when)
 import Data.Default (Default (def))
 import Data.Foldable
 import Data.Map (Map)
@@ -25,7 +25,7 @@ import Plutus.Contract hiding (currentSlot)
 import Plutus.Contract.Test
 import Plutus.Contract.Test.ContractModel
 
-import Plutus.Contracts.Escrow
+import Plutus.Contracts.Escrow hiding (Action (..))
 import Plutus.Trace.Emulator qualified as Trace
 import PlutusTx.Monoid (inv)
 
@@ -34,6 +34,8 @@ import Test.Tasty
 import Test.Tasty.HUnit qualified as HUnit
 import Test.Tasty.QuickCheck hiding ((.&&.))
 
+import Spec.Escrow.Endpoints
+
 data EscrowModel = EscrowModel { _contributions :: Map Wallet Value
                                , _refundSlot    :: Slot
                                , _targets       :: Map Wallet Value
@@ -54,10 +56,11 @@ instance ContractModel EscrowModel where
   data Action EscrowModel = Pay Wallet Integer
                           | Redeem Wallet
                           | Refund Wallet
+                          | BadRefund Wallet Wallet
                           | WaitUntil Slot
 
   data ContractInstanceKey EscrowModel w s e params where
-    WalletKey :: Wallet -> ContractInstanceKey EscrowModel () EscrowSchema EscrowError ()
+    WalletKey :: Wallet -> ContractInstanceKey EscrowModel () EscrowTestSchema EscrowError ()
 
   initialState = EscrowModel { _contributions = Map.empty
                              , _refundSlot    = TimeSlot.posixTimeToEnclosingSlot def
@@ -79,7 +82,11 @@ instance ContractModel EscrowModel where
   instanceContract _ WalletKey{} _ = testContract
     where
       -- TODO: Lazy test contract for now
-      testContract = selectList [void $ payEp modelParams, void $ redeemEp modelParams, void $ refundEp modelParams] >> testContract
+      testContract = selectList [ void $ payEp modelParams
+                                , void $ redeemEp modelParams
+                                , void $ refundEp modelParams
+                                , void $ badRefundEp modelParams
+                                ] >> testContract
 
   nextState a = void $ case a of
     Pay w v -> do
@@ -101,16 +108,19 @@ instance ContractModel EscrowModel where
       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
+    Refund w -> s ^. currentSlot >= s ^. contractState . refundSlot
              && Nothing /= (s ^. contractState . contributions . at w)
-    Pay w v -> Nothing == s ^. contractState . contributions . at w
-            && s ^. currentSlot + 1 < s ^. contractState . refundSlot
+    Pay w v -> s ^. currentSlot + 1 < s ^. contractState . refundSlot
             && Ada.adaValueOf (fromInteger v) `geq` Ada.toValue minAdaTxOut
+    BadRefund w w' -> s ^. currentSlot < s ^. contractState . refundSlot - 2  -- why -2?
+                   || w /= w'
 
   perform h _ _ a = case a of
     WaitUntil slot -> void $ Trace.waitUntilSlot slot
@@ -123,26 +133,65 @@ instance ContractModel EscrowModel where
     Refund w       -> do
       Trace.callEndpoint @"refund-escrow" (h $ WalletKey w) ()
       delay 1
-
-  arbitraryAction s = oneof $ [ Pay <$> QC.elements testWallets <*> choose @Integer (10, 30)
-                              , Redeem <$> QC.elements testWallets
-                              , WaitUntil . step <$> choose @Int (1, 10) ] ++
-                              [ Refund <$> QC.elements (s ^. contractState . contributions . to Map.keys)
-                              | Prelude.not . null $ s ^. contractState . contributions . to Map.keys ]
+    BadRefund w w' -> do
+      Trace.callEndpoint @"badrefund-escrow" (h $ WalletKey w) (mockWalletPaymentPubKeyHash w')
+      delay 2
+
+  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"
+    where redeemable s = precondition s (Redeem undefined)
+
 testWallets :: [Wallet]
-testWallets = [w1, w2, w3, w4, w5, w6, w7, w8, w9, w10]
+testWallets = [w1, w2, w3, w4, w5] -- removed five to increase collisions (, w6, w7, w8, w9, w10])
 
 prop_Escrow :: Actions EscrowModel -> Property
 prop_Escrow = propRunActions_
 
+finishEscrow :: DL EscrowModel ()
+finishEscrow = do
+    anyActions_
+    finishingStrategy (const True)
+    assertModel "Locked funds are not zero" (symIsZero . lockedValue)
+
+finishingStrategy :: (Wallet -> Bool) -> DL EscrowModel ()
+finishingStrategy walletAlive = do
+    now <- viewModelState currentSlot
+    slot <- viewContractState refundSlot
+    when (now < slot+1) $ action $ WaitUntil $ 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]
+
+prop_FinishEscrow :: Property
+prop_FinishEscrow = forAllDL finishEscrow prop_Escrow
+
+noLockProof :: NoLockedFundsProof EscrowModel
+noLockProof = NoLockedFundsProof
+  { nlfpMainStrategy   = finishingStrategy (const True)
+  , nlfpWalletStrategy = finishingStrategy . (==) }
+
+prop_NoLockedFunds :: Property
+prop_NoLockedFunds = checkNoLockedFundsProof defaultCheckOptionsContractModel noLockProof
+
+
 tests :: TestTree
 tests = testGroup "escrow"
     [ let con = void $ payEp @() @EscrowSchema @EscrowError (escrowParams startTime) in
@@ -209,6 +258,7 @@ tests = testGroup "escrow"
                                32000
 
     , testProperty "QuickCheck ContractModel" $ withMaxSuccess 10 prop_Escrow
+    , testProperty "QuickCheck NoLockedFunds" $ withMaxSuccess 10 prop_NoLockedFunds
     ]
 
     where
@@ -217,7 +267,7 @@ tests = testGroup "escrow"
 escrowParams :: POSIXTime -> EscrowParams d
 escrowParams startTime =
   EscrowParams
-    { escrowDeadline = startTime + 10000
+    { escrowDeadline = startTime + 40000
     , escrowTargets  =
         [ payToPaymentPubKeyTarget (mockWalletPaymentPubKeyHash w1) (Ada.adaValueOf 10)
         , payToPaymentPubKeyTarget (mockWalletPaymentPubKeyHash w2) (Ada.adaValueOf 20)

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

@@ -0,0 +1,59 @@
+{-# LANGUAGE DataKinds        #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE MonoLocalBinds   #-}
+{-# LANGUAGE RankNTypes       #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators    #-}
+
+module Spec.Escrow.Endpoints where
+
+import Data.Text (unpack)
+
+import Control.Monad (void)
+
+import Ledger (Datum (..), PaymentPubKeyHash)
+import Ledger qualified
+import Ledger.Constraints qualified as Constraints
+import Ledger.Interval (from)
+import Ledger.Tx qualified as Tx
+import Ledger.Typed.Scripts (TypedValidator)
+import Ledger.Typed.Scripts qualified as Scripts
+
+import Plutus.Contract
+import Plutus.Contract.Typed.Tx qualified as Typed
+import PlutusTx qualified
+import PlutusTx.Prelude hiding (Applicative (..), Semigroup (..), check, foldMap)
+
+import Prelude (Semigroup (..))
+
+import Plutus.Contracts.Escrow
+
+type EscrowTestSchema = Endpoint "badrefund-escrow" PaymentPubKeyHash .\/ EscrowSchema
+
+-- | 'badRefund' with an endpoint.
+badRefundEp ::
+    forall w s.
+    ( HasEndpoint "badrefund-escrow" PaymentPubKeyHash s
+    )
+    => EscrowParams Datum
+    -> Promise w s EscrowError ()
+badRefundEp escrow = endpoint @"badrefund-escrow" $ \pk -> badRefund (typedValidator escrow) pk
+
+-- Submit a transaction attempting to take the refund belonging to the given pk.
+badRefund ::
+    forall w s.
+    TypedValidator Escrow
+    -> PaymentPubKeyHash
+    -> Contract w s EscrowError ()
+badRefund inst pk = do
+    unspentOutputs <- utxosAt (Scripts.validatorAddress inst)
+    current <- currentTime
+    let flt _ ciTxOut = either id Ledger.datumHash (Tx._ciTxOutDatum ciTxOut) == Ledger.datumHash (Datum (PlutusTx.toBuiltinData pk))
+        tx' = Typed.collectFromScriptFilter flt unspentOutputs Refund
+           <> Constraints.mustValidateIn (from (current - 1))
+    utx <- mkTxConstraints ( Constraints.typedValidatorLookups inst
+                          <> Constraints.unspentOutputs unspentOutputs
+                           ) tx'
+    handleError (\err -> logError $ "Caught error: " ++ unpack err) $
+      void $ submitUnbalancedTx (Constraints.adjustUnbalancedTx utx)
+