No locked funds proofs (IntersectMBO#3929)

* Add discardWallets to drop wallets from the emulator state

Useful for testing that wallets can achieve desired outcomes
without the help of other wallets. Discarding the wallet state
means no transactions can be signed by the discarded wallets.

* Add NoLockedFundsProof

A no-locked-funds-proof shows (using testing) not only that
all funds can be recovered from a contract, but also that each
participant can recover "their" funds even if all the other
participants refuse to participate.

* NoLockedFundsProofs for some example contracts

Trivial for Prism, and does not actually hold for Auction since the
it's the seller's off-chain code that invokes the Payout transition.

* Add some comments

* Fix stylish haskell

Author: UlfNorell

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

@@ -106,6 +106,12 @@ module Plutus.Contract.Test.ContractModel
     , TestStep(..)
     , FailedStep(..)
     , withDLTest
+
+    -- ** Standard properties
+    --
+    -- $noLockedFunds
+    , NoLockedFundsProof(..)
+    , checkNoLockedFundsProof
     ) where
 
 import           Control.Lens
@@ -121,21 +127,25 @@ import           Data.Row                              (Row)
 import           Data.Typeable
 
 import           Ledger.Slot
-import           Ledger.Value                          (Value)
-import           Plutus.Contract                       (Contract)
+import           Ledger.Value                          (Value, isZero, leq)
+import           Plutus.Contract                       (Contract, ContractInstanceId)
 import           Plutus.Contract.Test
-import           Plutus.Trace.Emulator                 as Trace (ContractHandle, ContractInstanceTag, EmulatorTrace,
-                                                                 activateContract, walletInstanceTag)
+import           Plutus.Trace.Effects.EmulatorControl  (discardWallets)
+import           Plutus.Trace.Emulator                 as Trace (ContractHandle (..), ContractInstanceTag,
+                                                                 EmulatorTrace, activateContract,
+                                                                 freezeContractInstance, walletInstanceTag)
 import           PlutusTx.Monoid                       (inv)
 import qualified Test.QuickCheck.DynamicLogic.Monad    as DL
 import           Test.QuickCheck.DynamicLogic.Quantify (Quantifiable (..), Quantification, arbitraryQ, chooseQ,
                                                         elementsQ, exactlyQ, frequencyQ, mapQ, oneofQ, whereQ)
 import           Test.QuickCheck.StateModel            hiding (Action, Actions, arbitraryAction, initialState,
-                                                        monitoring, nextState, perform, precondition, shrinkAction)
+                                                        monitoring, nextState, perform, precondition, shrinkAction,
+                                                        stateAfter)
 import qualified Test.QuickCheck.StateModel            as StateModel
 
 import           Test.QuickCheck                       hiding ((.&&.))
-import           Test.QuickCheck.Monadic               as QC (PropertyM, monadic)
+import qualified Test.QuickCheck                       as QC
+import           Test.QuickCheck.Monadic               (PropertyM, monadic)
 import qualified Test.QuickCheck.Monadic               as QC
 
 -- | Key-value map where keys and values have three indices that can vary between different elements
@@ -188,7 +198,16 @@ data ContractInstanceSpec state where
                   -> Contract w schema err ()               -- ^ The contract that is running in the instance
                   -> ContractInstanceSpec state
 
-type Handles state = IMap (ContractInstanceKey state) ContractHandle
+data WalletContractHandle w s e = WalletContractHandle Wallet (ContractHandle w s e)
+
+type Handles state = IMap (ContractInstanceKey state) WalletContractHandle
+
+-- | Used to freeze other wallets when checking a `NoLockedFundsProof`.
+instancesForOtherWallets :: Wallet -> Handles state -> [ContractInstanceId]
+instancesForOtherWallets _ IMNil = []
+instancesForOtherWallets w (IMCons _ (WalletContractHandle w' h) m)
+  | w /= w'   = chInstanceId h : instancesForOtherWallets w m
+  | otherwise = instancesForOtherWallets w m
 
 
 -- | A function returning the `ContractHandle` corresponding to a `ContractInstanceKey`. A
@@ -473,8 +492,8 @@ instance GetModelState (Spec state) where
 handle :: (ContractModel s) => Handles s -> HandleFun s
 handle handles key =
     case imLookup key handles of
-        Just h  -> h
-        Nothing -> error $ "handle: No handle for " ++ show key
+        Just (WalletContractHandle _ h) -> h
+        Nothing                         -> error $ "handle: No handle for " ++ show key
 
 -- | The `EmulatorTrace` monad does not let you get the result of a computation out, but the way
 --   "Test.QuickCheck.Monadic" is set up requires you to provide a function @m Property -> Property@.
@@ -502,13 +521,19 @@ setHandles a = State.modify (<> EmulatorAction (const a))
 
 instance ContractModel state => Show (StateModel.Action (ModelState state) a) where
     showsPrec p (ContractAction a) = showsPrec p a
+    showsPrec p (Unilateral w)     = showParen (p >= 11) $ showString "Unilateral " . showsPrec 11 w
 
 deriving instance ContractModel state => Eq (StateModel.Action (ModelState state) a)
 
 instance ContractModel state => StateModel (ModelState state) where
 
     data Action (ModelState state) a where
         ContractAction :: Action state -> StateModel.Action (ModelState state) ()
+        Unilateral :: Wallet -> StateModel.Action (ModelState state) ()
+          -- ^ This action disables all wallets other than the given wallet, by freezing their
+          --   contract instances and removing their private keys from the emulator state. This can
+          --   be used to check that a wallet can *unilaterally* achieve a desired outcome, without
+          --   the help of other wallets.
 
     type ActionMonad (ModelState state) = ContractMonad state
 
@@ -517,21 +542,30 @@ instance ContractModel state => StateModel (ModelState state) where
         return (Some @() (ContractAction a))
 
     shrinkAction s (ContractAction a) = [ Some @() (ContractAction a') | a' <- shrinkAction s a ]
+    shrinkAction _ Unilateral{}       = []
 
     initialState = ModelState { _currentSlot    = 0
                               , _balanceChanges = Map.empty
                               , _minted         = mempty
                               , _contractState  = initialState }
 
     nextState s (ContractAction cmd) _v = runSpec (nextState cmd) s
+    nextState s Unilateral{} _          = s
 
     precondition s (ContractAction cmd) = precondition s cmd
+    precondition _ Unilateral{}         = True
 
     perform s (ContractAction cmd) _env = () <$ runEmulator (\ h -> perform (handle h) s cmd)
+    perform _ (Unilateral w) _env = () <$ runEmulator (\ h -> do
+        let insts = instancesForOtherWallets w h
+        mapM_ freezeContractInstance insts
+        discardWallets (w /=)
+      )
 
     postcondition _s _cmd _env _res = True
 
     monitoring (s0, s1) (ContractAction cmd) _env _res = monitoring (s0, s1) cmd
+    monitoring _ Unilateral{} _ _                      = id
 
 -- We present a simplified view of test sequences, and DL test cases, so
 -- that users do not need to see the variables bound to results.
@@ -661,10 +695,11 @@ toDLTestStep (Witness a) = DL.Witness a
 
 fromDLTest :: forall s. DL.DynLogicTest (ModelState s) -> DLTest s
 fromDLTest (DL.BadPrecondition steps acts s) =
-  BadPrecondition (fromDLTestSteps steps) (map conv acts) (_contractState s)
-  where conv :: Any (StateModel.Action (ModelState s)) -> FailedStep s
-        conv (Some (ContractAction act)) = Action act
-        conv (Error e)                   = Assert e
+  BadPrecondition (fromDLTestSteps steps) (concatMap conv acts) (_contractState s)
+  where conv :: Any (StateModel.Action (ModelState s)) -> [FailedStep s]
+        conv (Some (ContractAction act)) = [Action act]
+        conv (Some Unilateral{})         = []
+        conv (Error e)                   = [Assert e]
 fromDLTest (DL.Looping steps) =
   Looping (fromDLTestSteps steps)
 fromDLTest (DL.Stuck steps s) =
@@ -673,11 +708,12 @@ fromDLTest (DL.DLScript steps) =
   DLScript (fromDLTestSteps steps)
 
 fromDLTestSteps :: [DL.TestStep (ModelState state)] -> [TestStep state]
-fromDLTestSteps steps = map fromDLTestStep steps
+fromDLTestSteps steps = concatMap fromDLTestStep steps
 
-fromDLTestStep :: DL.TestStep (ModelState state) -> TestStep state
-fromDLTestStep (DL.Do (_ := ContractAction act)) = Do act
-fromDLTestStep (DL.Witness a)                    = Witness a
+fromDLTestStep :: DL.TestStep (ModelState state) -> [TestStep state]
+fromDLTestStep (DL.Do (_ := ContractAction act)) = [Do act]
+fromDLTestStep (DL.Do (_ := Unilateral{}))       = []
+fromDLTestStep (DL.Witness a)                    = [Witness a]
 
 -- | Run a specific `DLTest`. Typically this test comes from a failed run of `forAllDL`
 --   applied to the given `DL` scenario and property. Useful to check if a particular problem has
@@ -890,6 +926,7 @@ forAllDL dl prop = DL.forAllMappedDL toDLTest fromDLTest fromStateModelActions d
 
 instance ContractModel s => DL.DynLogicModel (ModelState s) where
     restricted (ContractAction act) = restricted act
+    restricted Unilateral{}         = True
 
 instance GetModelState (DL state) where
     type StateType (DL state) = state
@@ -934,7 +971,7 @@ activateWallets [] = return IMNil
 activateWallets (ContractInstanceSpec key wallet contract : spec) = do
     h <- activateContract wallet contract (instanceTag key wallet)
     m <- activateWallets spec
-    return $ IMCons key h m
+    return $ IMCons key (WalletContractHandle wallet h) m
 
 -- | Run a `Actions` in the emulator and check that the model and the emulator agree on the final
 --   wallet balance changes. Equivalent to
@@ -1001,14 +1038,26 @@ propRunActionsWithOptions ::
     -> Actions state                          -- ^ The actions to run
     -> Property
 propRunActionsWithOptions opts handleSpecs predicate actions' =
+  propRunActionsWithOptions' opts handleSpecs predicate (toStateModelActions actions')
+
+propRunActionsWithOptions' ::
+    ContractModel state
+    => CheckOptions                          -- ^ Emulator options
+    -> [ContractInstanceSpec state]          -- ^ Required wallet contract instances
+    -> (ModelState state -> TracePredicate)  -- ^ Predicate to check at the end
+    -> StateModel.Actions (ModelState state) -- ^ The actions to run
+    -> Property
+propRunActionsWithOptions' opts handleSpecs predicate actions =
     monadic (flip State.evalState mempty) $ finalChecks opts finalPredicate $ do
         QC.run $ setHandles $ activateWallets handleSpecs
         void $ runActionsInState StateModel.initialState actions
     where
-        finalState     = stateAfter actions
+        finalState     = StateModel.stateAfter actions
         finalPredicate = predicate finalState .&&. checkBalances finalState
                                               .&&. checkNoCrashes handleSpecs
-        actions = toStateModelActions actions'
+
+stateAfter :: ContractModel state => Actions state -> ModelState state
+stateAfter actions = StateModel.stateAfter (toStateModelActions actions)
 
 checkBalances :: ModelState state -> TracePredicate
 checkBalances s = Map.foldrWithKey (\ w val p -> walletFundsChange w val .&&. p) (pure True) (s ^. balanceChanges)
@@ -1020,3 +1069,68 @@ checkNoCrashes = foldr (\ (ContractInstanceSpec k w c) -> (assertOutcome c (inst
         notError Failed{}  = False
         notError Done{}    = True
         notError NotDone{} = True
+
+-- $noLockedFunds
+-- Showing that funds can not be locked in the contract forever.
+
+-- | A "proof" that you can always recover the funds locked by a contract. The first component is
+--   a strategy that from any state of the contract can get all the funds out. The second component
+--   is a strategy for each wallet that from the same state, shows how that wallet can recover the
+--   same (or bigger) amount as using the first strategy, without relying on any actions being taken
+--   by the other wallets.
+--
+--   For instance, in a two player game where each player bets some amount of funds and the winner
+--   gets the pot, there needs to be a mechanism for the players to recover their bid if the other
+--   player simply walks away (perhaps after realising the game is lost). If not, it won't be
+--   possible to construct a `NoLockedFundsProof` that works in a state where both players need to
+--   move before any funds can be collected.
+data NoLockedFundsProof model = NoLockedFundsProof
+  { nlfpMainStrategy   :: DL model ()
+    -- ^ Strategy to recover all funds from the contract in any reachable state.
+  , nlfpWalletStrategy :: Wallet -> DL model ()
+    -- ^ A strategy for each wallet to recover as much (or more) funds as the main strategy would
+    --   give them in a given state, without the assistance of any other wallet.
+  }
+
+-- | Check a `NoLockedFundsProof`. Each test will generate an arbitrary sequence of actions
+--   (`anyActions_`) and ask the `nlfpMainStrategy` to recover all funds locked by the contract
+--   after performing those actions. This results in some distribution of the contract funds to the
+--   wallets, and the test then asks each `nlfpWalletStrategy` to show how to recover their
+--   allotment of funds without any assistance from the other wallets (assuming the main strategy
+--   did not execute). When executing wallet strategies, the off-chain instances for other wallets
+--   are killed and their private keys are deleted from the emulator state.
+checkNoLockedFundsProof
+  :: (ContractModel model)
+  => CheckOptions
+  -> [ContractInstanceSpec model]
+  -> NoLockedFundsProof model
+  -> Property
+checkNoLockedFundsProof options spec NoLockedFundsProof{nlfpMainStrategy   = mainStrat,
+                                                        nlfpWalletStrategy = walletStrat } =
+    forAllDL anyActions_   $ \ (Actions as) ->
+    forAllDL (mainProp as) $ \ as' ->
+        let s    = stateAfter as'
+            as'' = toStateModelActions as' in
+        foldl (QC..&&.) (counterexample "Main strategy" $ prop as'') [ walletProp as w bal | (w, bal) <- Map.toList (s ^. balanceChanges) ]
+    where
+        prop = propRunActionsWithOptions' options spec (\ _ -> pure True)
+
+        mainProp as = do
+            mapM_ action as
+            mainStrat
+            lockedVal <- askModelState lockedValue
+            DL.assert ("Locked funds should be zero, but they are\n  " ++ show lockedVal) $ isZero lockedVal
+
+        walletProp as w bal = counterexample ("Strategy for " ++ show w) $ DL.forAllDL dl prop
+            where
+                dl = do
+                    mapM_ action as
+                    DL.action $ Unilateral w
+                    walletStrat w
+                    bal' <- viewModelState (balanceChange w)
+                    let err = "Unilateral strategy for " ++ show w ++ " should have gotten it at least\n" ++
+                              "  " ++ show bal ++ "\n" ++
+                              "but it got\n" ++
+                              "  " ++ show bal'
+                    DL.assert err (bal `leq` bal')
+

plutus-contract/src/Plutus/Trace/Effects/EmulatorControl.hs

@@ -20,17 +20,19 @@ module Plutus.Trace.Effects.EmulatorControl(
     , freezeContractInstance
     , thawContractInstance
     , chainState
+    , discardWallets
     , handleEmulatorControl
     , getSlotConfig
     ) where
 
-import           Control.Lens                           (view)
+import           Control.Lens                           (over, view)
 import           Control.Monad                          (void)
 import           Control.Monad.Freer                    (Eff, Member, type (~>))
 import           Control.Monad.Freer.Coroutine          (Yield)
 import           Control.Monad.Freer.Error              (Error)
-import           Control.Monad.Freer.State              (State, gets)
+import           Control.Monad.Freer.State              (State, gets, modify)
 import           Control.Monad.Freer.TH                 (makeEffect)
+import qualified Data.Map                               as Map
 import           Ledger.TimeSlot                        (SlotConfig)
 import           Plutus.Trace.Emulator.ContractInstance (EmulatorRuntimeError, getThread)
 import           Plutus.Trace.Emulator.Types            (EmulatorMessage (Freeze), EmulatorThreads)
@@ -69,6 +71,7 @@ data EmulatorControl r where
     ThawContractInstance :: ContractInstanceId -> EmulatorControl ()
     ChainState :: EmulatorControl ChainState
     GetSlotConfig :: EmulatorControl SlotConfig
+    DiscardWallets :: (Wallet -> Bool) -> EmulatorControl ()  -- ^ Discard wallets matching the predicate.
 
 -- | Interpret the 'EmulatorControl' effect in the 'MultiAgentEffect' and
 --   scheduler system calls.
@@ -96,5 +99,6 @@ handleEmulatorControl slotCfg = \case
         void $ mkSysCall @effs2 @EmulatorMessage Normal (Right $ Thaw threadId)
     ChainState -> gets (view EM.chainState)
     GetSlotConfig -> return slotCfg
+    DiscardWallets discard -> modify @EmulatorState $ over EM.walletStates (Map.filterWithKey (\ k _ -> not $ discard k))
 
 makeEffect ''EmulatorControl

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

@@ -13,6 +13,7 @@ module Spec.Auction
     , auctionTrace2
     , prop_Auction
     , prop_FinishAuction
+    , prop_NoLockedFunds
     ) where
 
 import           Cardano.Crypto.Hash                as Crypto
@@ -220,7 +221,7 @@ instance ContractModel AuctionModel where
             Bid w bid -> do
                 current <- viewContractState currentBid
                 leader  <- viewContractState winner
-                wait 1
+                wait 2
                 when (bid > current && slot <= end) $ do
                     withdraw w $ Ada.lovelaceValueOf bid
                     deposit leader $ Ada.lovelaceValueOf current
@@ -238,6 +239,13 @@ instance ContractModel AuctionModel where
     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
+        --        never busy for more than one slot at a time so at least one of the bids is
+        --        guaranteed to go through. If both reaches the off-chain code the second will be
+        --        discarded since it's not higher than the current highest bid.
+        Trace.callEndpoint @"bid" (handle $ BuyerH w) (Ada.lovelaceOf bid)
+        delay 1
         Trace.callEndpoint @"bid" (handle $ BuyerH w) (Ada.lovelaceOf bid)
         delay 1
 
@@ -253,12 +261,13 @@ delay n = void $ Trace.waitNSlots $ fromIntegral n
 
 prop_Auction :: Actions AuctionModel -> Property
 prop_Auction script =
-    propRunActionsWithOptions (set minLogLevel Info options) spec
+    propRunActionsWithOptions (set minLogLevel Info options) handleSpec
         (\ _ -> pure True)  -- TODO: check termination
         script
-    where
-        spec = ContractInstanceSpec SellerH w1 seller :
-               [ ContractInstanceSpec (BuyerH w) w (buyer threadToken) | w <- [w2, w3, w4] ]
+
+handleSpec :: [ContractInstanceSpec AuctionModel]
+handleSpec = ContractInstanceSpec SellerH w1 seller :
+             [ ContractInstanceSpec (BuyerH w) w (buyer threadToken) | w <- [w2, w3, w4] ]
 
 finishAuction :: DL AuctionModel ()
 finishAuction = do
@@ -271,6 +280,23 @@ finishAuction = do
 prop_FinishAuction :: Property
 prop_FinishAuction = forAllDL finishAuction prop_Auction
 
+-- | This does not hold! The Payout transition is triggered by the sellers off-chain code, so if the
+--   seller walks away the buyer will not get their token (unless going around the off-chain code
+--   and building a Payout transaction manually).
+noLockProof :: NoLockedFundsProof AuctionModel
+noLockProof = NoLockedFundsProof
+  { nlfpMainStrategy   = strat
+  , nlfpWalletStrategy = const strat }
+  where
+    strat = do
+      p <- viewContractState phase
+      when (p == NotStarted) $ action Init
+      slot <- viewModelState currentSlot
+      when (slot < 101) $ action $ WaitUntil 101
+
+prop_NoLockedFunds :: Property
+prop_NoLockedFunds = checkNoLockedFundsProof options handleSpec noLockProof
+
 tests :: TestTree
 tests =
     testGroup "auction"
@@ -291,8 +317,6 @@ tests =
             .&&. walletFundsChange w2 (inv (Ada.toValue trace2WinningBid) <> theToken)
             .&&. walletFundsChange w3 mempty)
             auctionTrace2
-        -- FIXME: Fails because you cannot bid in certain slots when the off-chain code is busy.
         , testProperty "QuickCheck property" $
-            withMaxSuccess 1 $ classify True "FIXME" True
-            -- withMaxSuccess 10 prop_FinishAuction
+            withMaxSuccess 10 prop_FinishAuction
         ]