ContractModel: Add wiggle room options to NoLockedFunds

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

@@ -125,10 +125,9 @@ module Plutus.Contract.Test.ContractModel
     --
     -- $noLockedFunds
     , NoLockedFundsProof(..)
+    , defaultNLFP
     , checkNoLockedFundsProof
     , checkNoLockedFundsProofFast
-    , checkNoLockedFundsProofWithWiggleRoom
-    , checkNoLockedFundsProofWithWiggleRoomFast
     -- $checkNoPartiality
     , Whitelist
     , whitelistOk

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

@@ -136,10 +136,9 @@ module Plutus.Contract.Test.ContractModel.Internal
     --
     -- $noLockedFunds
     , NoLockedFundsProof(..)
+    , defaultNLFP
     , checkNoLockedFundsProof
     , checkNoLockedFundsProofFast
-    , checkNoLockedFundsProofWithWiggleRoom
-    , checkNoLockedFundsProofWithWiggleRoomFast
     -- $checkNoPartiality
     , Whitelist
     , whitelistOk
@@ -1563,8 +1562,22 @@ data NoLockedFundsProof model = NoLockedFundsProof
   , 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.
+  , nlfpOverhead       :: ModelState model -> SymValue
+    -- ^ An initial amount of overhead value that may be lost - e.g. setup fees for scripts that
+    -- can't be recovered.
+  , nlfpErrorMargin    :: ModelState model -> SymValue
+    -- ^ The total amount of margin for error in the value collected by the WalletStrategy compared
+    -- to the MainStrategy. This is useful if your contract contains rounding code that makes the order
+    -- of operations have a small but predictable effect on the value collected by different wallets.
   }
 
+-- | The default skeleton of a NoLockedFundsProof - doesn't permit any overhead or error margin.
+defaultNLFP :: NoLockedFundsProof model
+defaultNLFP = NoLockedFundsProof { nlfpMainStrategy = return ()
+                                 , nlfpWalletStrategy = const (return ())
+                                 , nlfpOverhead = const mempty
+                                 , nlfpErrorMargin = const mempty }
+
 -- | 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
@@ -1578,63 +1591,55 @@ checkNoLockedFundsProof
   => CheckOptions
   -> NoLockedFundsProof model
   -> Property
-checkNoLockedFundsProof = checkNoLockedFundsProofWithWiggleRoom 0
-
-checkNoLockedFundsProofFast
-  :: (ContractModel model)
-  => CheckOptions
-  -> NoLockedFundsProof model
-  -> Property
-checkNoLockedFundsProofFast _ = checkNoLockedFundsProofWithWiggleRoomFast 0
-
-checkNoLockedFundsProofWithWiggleRoom
-  :: (ContractModel model)
-  => Integer
-  -> CheckOptions
-  -> NoLockedFundsProof model
-  -> Property
-checkNoLockedFundsProofWithWiggleRoom wiggle options =
-  checkNoLockedFundsProofWithWiggleRoom' wiggle prop
+checkNoLockedFundsProof options =
+  checkNoLockedFundsProof' prop
   where
     prop = propRunActionsWithOptions' options defaultCoverageOptions (\ _ -> pure True)
 
-checkNoLockedFundsProofWithWiggleRoomFast
+checkNoLockedFundsProofFast
   :: (ContractModel model)
-  => Integer
+  => CheckOptions
   -> NoLockedFundsProof model
   -> Property
-checkNoLockedFundsProofWithWiggleRoomFast wiggle = checkNoLockedFundsProofWithWiggleRoom' wiggle (const $ property True)
+checkNoLockedFundsProofFast _ = checkNoLockedFundsProof' (const $ property True)
 
-checkNoLockedFundsProofWithWiggleRoom'
+checkNoLockedFundsProof'
   :: (ContractModel model)
-  => Integer
-  -> (StateModel.Actions (ModelState model) -> Property)
+  => (StateModel.Actions (ModelState model) -> Property)
   -> NoLockedFundsProof model
   -> Property
-checkNoLockedFundsProofWithWiggleRoom' wiggle run NoLockedFundsProof{nlfpMainStrategy   = mainStrat,
-                                                                     nlfpWalletStrategy = walletStrat } =
+checkNoLockedFundsProof' run NoLockedFundsProof{nlfpMainStrategy   = mainStrat,
+                                                nlfpWalletStrategy = walletStrat,
+                                                nlfpOverhead       = overhead,
+                                                nlfpErrorMargin    = wiggle } =
     forAllDL anyActions_ $ \ (Actions as) ->
     forAllUniqueDL (nextVarIdx as) (stateAfter $ Actions as) mainStrat $ \ (Actions as') ->
-          let s = stateAfter $ Actions (as ++ as') in
-            foldl (QC..&&.) (counterexample "Main run prop" (run (toStateModelActions $ Actions $ as ++ as')) QC..&&. (counterexample "Main strategy" . counterexample (show . Actions $ as ++ as') $ prop s))
-                            [ walletProp as w bal | (w, bal) <- Map.toList (s ^. balanceChanges) ]
+          let s0 = (stateAfter $ Actions as)
+              s = stateAfter $ Actions (as ++ as') in
+            foldl (QC..&&.) (counterexample "Main run prop" (run (toStateModelActions $ Actions $ as ++ as')) QC..&&. (counterexample "Main strategy" . counterexample (show . Actions $ as ++ as') $ prop s0 s))
+                            [ walletProp s0 as w bal | (w, bal) <- Map.toList (s ^. balanceChanges) ]
     where
         nextVarIdx as = 1 + maximum ([0] ++ [ i | Var i <- varOf <$> as ])
-        prop s =
+        prop s0 s =
           let lockedVal = lockedValue s
-          in (counterexample ("Locked funds should be zero, but they are\n  " ++ show lockedVal) $ symIsZero lockedVal)
+          in (counterexample ("Locked funds should be at most " ++ show (overhead s0) ++ ", but they are\n  " ++ show lockedVal)
+            $ symLeq lockedVal (overhead s0))
 
-        walletProp as w bal = DL.forAllUniqueDL (nextVarIdx as) (stateAfter $ Actions as) (DL.action (Unilateral w) >> walletStrat w) $ \ acts ->
+        walletProp s0 as w bal =
+          DL.forAllUniqueDL (nextVarIdx as) s0 (DL.action (Unilateral w) >> walletStrat w) $ \ acts ->
           let Actions as' = fromStateModelActions acts
+              wig = wiggle s0
               err  = "Unilateral strategy for " ++ show w ++ " should have gotten it at least\n" ++
                      "  " ++ show bal ++ "\n" ++
+                     concat [ "with wiggle room\n" ++ "  " ++ show wig ++ "\n"
+                            | wig /= mempty ] ++
                      "but it got\n" ++
                      "  " ++ show bal'
               bal' = stateAfter (Actions $ as ++ as') ^. balanceChange w
               smacts = toStateModelActions (Actions as) <> acts
               err' = "The ContractModel's Unilateral behaviour for " ++ show w ++ " does not match the actual behaviour for actions:\n"
                    ++ show smacts
-          in counterexample err (symLeqWiggle wiggle bal bal')
+          in counterexample err (symLeq bal (bal' <> wig))
           QC..&&. counterexample err' (run smacts)
 
 -- | A whitelist entry tells you what final log entry prefixes

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

@@ -1,6 +1,7 @@
 {-# OPTIONS_GHC -fno-warn-name-shadowing #-}
 module Plutus.Contract.Test.ContractModel.Symbolics where
 
+import Ledger.Ada qualified as Ada
 import Ledger.Value (AssetClass, Value, assetClassValue, isZero, leq)
 import PlutusTx.Monoid qualified as PlutusTx
 
@@ -71,5 +72,8 @@ instance SymValueLike Value where
 instance SymValueLike SymValue where
   toSymValue = id
 
+instance SymValueLike Ada.Ada where
+  toSymValue = toSymValue . Ada.toValue
+
 inv :: SymValue -> SymValue
 inv (SymValue m v) = SymValue (negate <$> m) (PlutusTx.inv v)

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

@@ -322,7 +322,7 @@ prop_FinishAuction = forAllDL finishAuction prop_Auction
 --   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
+noLockProof = defaultNLFP
   { nlfpMainStrategy   = strat
   , nlfpWalletStrategy = const strat }
   where

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

@@ -184,7 +184,7 @@ prop_FinishEscrow :: Property
 prop_FinishEscrow = forAllDL finishEscrow prop_Escrow
 
 noLockProof :: NoLockedFundsProof EscrowModel
-noLockProof = NoLockedFundsProof
+noLockProof = defaultNLFP
   { nlfpMainStrategy   = finishingStrategy (const True)
   , nlfpWalletStrategy = finishingStrategy . (==) }
 

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

@@ -272,7 +272,7 @@ prop_NoLockedFunds :: Property
 prop_NoLockedFunds = forAllDL noLockedFunds prop_Game
 
 noLockProof :: NoLockedFundsProof GameModel
-noLockProof = NoLockedFundsProof{
+noLockProof = defaultNLFP {
       nlfpMainStrategy   = mainStrat,
       nlfpWalletStrategy = walletStrat }
     where

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

@@ -197,10 +197,7 @@ prop_Prism = propRunActions @PrismModel finalPredicate
 
 -- | The Prism contract does not lock any funds.
 noLockProof :: NoLockedFundsProof PrismModel
-noLockProof = NoLockedFundsProof
-  { nlfpMainStrategy   = return ()
-  , nlfpWalletStrategy = \ _ -> return ()
-  }
+noLockProof = defaultNLFP
 
 prop_NoLock :: Property
 prop_NoLock = checkNoLockedFundsProof defaultCheckOptionsContractModel noLockProof

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

@@ -248,7 +248,7 @@ prop_FinishAuction :: Property
 prop_FinishAuction = forAllDL finishAuction prop_Auction
 
 noLockProof :: NoLockedFundsProof AuctionModel
-noLockProof = NoLockedFundsProof
+noLockProof = defaultNLFP
   { nlfpMainStrategy   = finishingStrategy w1
   , nlfpWalletStrategy = finishingStrategy }
 

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

@@ -473,12 +473,19 @@ prop_liquidityValue = forAllDL liquidityValue (const True)
                           /= (p ^. coinAAmount, p ^. coinBAmount)
         assert ("Pool\n  " ++ show p ++ "\nforgets single liquidities") cond
 
--- This doesn't work
 noLockProof :: NoLockedFundsProof UniswapModel
-noLockProof = NoLockedFundsProof{
+noLockProof = defaultNLFP {
       nlfpMainStrategy   = mainStrat,
-      nlfpWalletStrategy = walletStrat }
+      nlfpWalletStrategy = walletStrat,
+      nlfpOverhead       = const $ toSymValue Ledger.minAdaTxOut,
+      nlfpErrorMargin    = wiggle }
     where
+        wiggle s = fold [symAssetClassValue t1 (toInteger m) <>
+                         symAssetClassValue t2 (toInteger m) <>
+                         toSymValue Ledger.minAdaTxOut
+                        | (PoolIndex t1 t2, p) <- Map.toList (s ^. contractState . pools)
+                        , let numLiqs = length $ p ^. liquidities
+                              m = max 0 (numLiqs - 1) ]
         mainStrat = do
             pools <- viewContractState pools
             forM_ (Map.toList pools) $ \ (PoolIndex t1 t2, p) -> do
@@ -497,14 +504,11 @@ noLockProof = NoLockedFundsProof{
                 then action $ ClosePool w t1 t2
                 else action $ RemoveLiquidity w t1 t2 (unAmount . sum $ Map.lookup w liqs)
 
--- This doesn't hold
 prop_CheckNoLockedFundsProof :: Property
 prop_CheckNoLockedFundsProof = checkNoLockedFundsProof defaultCheckOptionsContractModel noLockProof
 
--- In principle this property does not hold for any wiggle room! You can chain together the issues
--- you get for normal "No locked funds"
 prop_CheckNoLockedFundsProofFast :: Property
-prop_CheckNoLockedFundsProofFast = checkNoLockedFundsProofWithWiggleRoomFast 3 noLockProof
+prop_CheckNoLockedFundsProofFast = checkNoLockedFundsProofFast defaultCheckOptionsContractModel noLockProof
 
 check_propUniswapWithCoverage :: IO ()
 check_propUniswapWithCoverage = void $
@@ -533,4 +537,5 @@ tests = testGroup "uniswap" [
         Uniswap.uniswapTrace
     , testProperty "prop_Uniswap" $ withMaxSuccess 20 prop_Uniswap
     , testProperty "prop_UniswapAssertions" $ withMaxSuccess 1000 (propSanityCheckAssertions @UniswapModel)
+    , testProperty "prop_NLFP" $ withMaxSuccess 250 prop_CheckNoLockedFundsProofFast
     ]

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

@@ -197,7 +197,7 @@ prop_Vesting :: Actions VestingModel -> Property
 prop_Vesting = propRunActions_
 
 noLockProof :: NoLockedFundsProof VestingModel
-noLockProof = NoLockedFundsProof{
+noLockProof = defaultNLFP {
       nlfpMainStrategy   = mainStrat,
       nlfpWalletStrategy = walletStrat }
     where