diff --git a/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs b/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs index e60bcbe31a..3cf7f59fa1 100644 --- a/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs +++ b/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 diff --git a/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs b/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs index c7cc13fd5b..79060cbbff 100644 --- a/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs +++ b/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 diff --git a/plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs b/plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs index 1e3a66a82f..e21da9e4b3 100644 --- a/plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs +++ b/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) diff --git a/plutus-use-cases/test/Spec/Auction.hs b/plutus-use-cases/test/Spec/Auction.hs index 3fd50f3b92..c49b4fcde5 100644 --- a/plutus-use-cases/test/Spec/Auction.hs +++ b/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 diff --git a/plutus-use-cases/test/Spec/Escrow.hs b/plutus-use-cases/test/Spec/Escrow.hs index d8461209c8..d99517b285 100644 --- a/plutus-use-cases/test/Spec/Escrow.hs +++ b/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 . (==) } diff --git a/plutus-use-cases/test/Spec/GameStateMachine.hs b/plutus-use-cases/test/Spec/GameStateMachine.hs index 08b1298d60..daa32fdb4b 100644 --- a/plutus-use-cases/test/Spec/GameStateMachine.hs +++ b/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 diff --git a/plutus-use-cases/test/Spec/Prism.hs b/plutus-use-cases/test/Spec/Prism.hs index ca0fc012cd..f0057199b6 100644 --- a/plutus-use-cases/test/Spec/Prism.hs +++ b/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 diff --git a/plutus-use-cases/test/Spec/SealedBidAuction.hs b/plutus-use-cases/test/Spec/SealedBidAuction.hs index 76d584006b..29e261aa71 100644 --- a/plutus-use-cases/test/Spec/SealedBidAuction.hs +++ b/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 } diff --git a/plutus-use-cases/test/Spec/Uniswap.hs b/plutus-use-cases/test/Spec/Uniswap.hs index 46f0eebb60..6d532d1383 100644 --- a/plutus-use-cases/test/Spec/Uniswap.hs +++ b/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 ] diff --git a/plutus-use-cases/test/Spec/Vesting.hs b/plutus-use-cases/test/Spec/Vesting.hs index ebc6aecdfc..8b7f138e0f 100644 --- a/plutus-use-cases/test/Spec/Vesting.hs +++ b/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