From c6430c5f43329130b2886d4ef146e8301d1f9e8d Mon Sep 17 00:00:00 2001 From: Maximilian Algehed Date: Wed, 17 Nov 2021 14:28:00 +0100 Subject: [PATCH] This commit introduces an approach to testing contracts that dynamically create tokens using the `ContractModel` interface and introduces a `ContractModel` test-suite for the `Plutus.Contracts.Uniswap` contract. --- doc/plutus-doc.cabal | 1 + doc/plutus/tutorials/GameModel.hs | 46 +- doc/plutus/tutorials/contract-testing.rst | 22 +- .../.plan.nix/plutus-contract.nix | 1 + .../.plan.nix/plutus-doc.nix | 1 + .../.plan.nix/plutus-contract.nix | 1 + .../.plan.nix/plutus-doc.nix | 1 + .../.plan.nix/plutus-contract.nix | 1 + .../.plan.nix/plutus-doc.nix | 1 + plutus-contract/plutus-contract.cabal | 1 + .../src/Plutus/Contract/Test/ContractModel.hs | 17 + .../Test/ContractModel/CrashTolerance.hs | 57 +- .../Contract/Test/ContractModel/Internal.hs | 615 +++++++++++++----- .../Contract/Test/ContractModel/Symbolics.hs | 75 +++ .../src/Plutus/Contract/Test/Coverage.hs | 18 +- plutus-contract/src/Plutus/Trace/Emulator.hs | 16 +- .../src/Plutus/Trace/Emulator/Types.hs | 4 + plutus-contract/test/Spec/ErrorChecking.hs | 20 +- .../src/Plutus/Contracts/Uniswap/OffChain.hs | 8 + .../src/Plutus/Contracts/Uniswap/OnChain.hs | 1 + .../src/Plutus/Contracts/Uniswap/Pool.hs | 1 + plutus-use-cases/test/Spec/Auction.hs | 57 +- plutus-use-cases/test/Spec/Crowdfunding.hs | 38 +- plutus-use-cases/test/Spec/Escrow.hs | 22 +- .../test/Spec/GameStateMachine.hs | 51 +- plutus-use-cases/test/Spec/Prism.hs | 21 +- .../test/Spec/SealedBidAuction.hs | 59 +- plutus-use-cases/test/Spec/Uniswap.hs | 517 ++++++++++++++- plutus-use-cases/test/Spec/Vesting.hs | 21 +- .../src/Test/QuickCheck/DynamicLogic.hs | 108 ++- .../src/Test/QuickCheck/DynamicLogic/Monad.hs | 19 + .../src/Test/QuickCheck/StateModel.hs | 30 +- 32 files changed, 1404 insertions(+), 447 deletions(-) create mode 100644 plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs diff --git a/doc/plutus-doc.cabal b/doc/plutus-doc.cabal index f92122ff45..eb7add55c2 100644 --- a/doc/plutus-doc.cabal +++ b/doc/plutus-doc.cabal @@ -71,6 +71,7 @@ executable doc-doctests plutus-contract -any, playground-common -any, plutus-use-cases -any, + quickcheck-dynamic -any, prettyprinter -any, containers -any, freer-extras -any, diff --git a/doc/plutus/tutorials/GameModel.hs b/doc/plutus/tutorials/GameModel.hs index c1066937a9..fb551658fd 100644 --- a/doc/plutus/tutorials/GameModel.hs +++ b/doc/plutus/tutorials/GameModel.hs @@ -35,6 +35,7 @@ import Plutus.Contract.Test.ContractModel -- END import ContractModel import Plutus.Contract.Test.ContractModel as ContractModel +import Test.QuickCheck.StateModel hiding (Action, Actions) -- START import Game import Plutus.Contracts.GameStateMachine as G @@ -96,11 +97,15 @@ instance ContractModel GameModel where -- END initialState -- START initialHandleSpecs - initialHandleSpecs = [ ContractInstanceSpec (WalletKey w) w G.contract | w <- wallets ] + initialInstances = Key . WalletKey <$> wallets + + instanceContract _ _ WalletKey{} = G.contract + + instanceWallet (WalletKey w) = w -- END initialHandleSpecs -- START perform - perform handle s cmd = case cmd of + perform handle _ s cmd = case cmd of Lock w new val -> do callEndpoint @"lock" (handle $ WalletKey w) LockArgs{ lockArgsSecret = secretArg new @@ -197,7 +202,7 @@ prop_Game actions = propRunActions_ actions -- START propGame' propGame' :: LogLevel -> Actions GameModel -> Property propGame' l s = propRunActionsWithOptions - (set minLogLevel l defaultCheckOptions) + (set minLogLevel l defaultCheckOptionsContractModel) defaultCoverageOptions (\ _ -> pure True) s @@ -222,11 +227,6 @@ shrinkWallet w = [w' | w' <- wallets, w' < w] guesses :: [String] guesses = ["hello", "secret", "hunter2", "*******"] --- START delay -delay :: Int -> EmulatorTraceNoStartContract () -delay n = void $ waitNSlots (fromIntegral n) --- END delay - -- Dynamic Logic ---------------------------------------------------------- prop_UnitTest :: Property @@ -251,9 +251,9 @@ badUnitTest :: DLTest GameModel badUnitTest = BadPrecondition [Witness (1 :: Integer), - Do $ Lock w1 "hello" 1, - Do $ GiveToken w2] - [Action (Guess w2 "hello" "new secret" 3)] + Do $ NoBind (Var 1) $ Lock w1 "hello" 1, + Do $ NoBind (Var 2) $ GiveToken w2] + [Action (NoBind (Var 3) (Guess w2 "hello" "new secret" 3))] (GameModel {_gameValue = 1, _hasToken = Just w2, _currentSecret = "hello"}) -- END badUnitTest @@ -282,7 +282,7 @@ noLockedFunds = do monitor $ label "Unlocking funds" action $ GiveToken w action $ Guess w secret "" val - assertModel "Locked funds should be zero" $ isZero . lockedValue + assertModel "Locked funds should be zero" $ symIsZero . lockedValue -- END noLockedFunds -- | Check that we can always get the money out of the guessing game (by guessing correctly). @@ -305,7 +305,7 @@ gameTokenVal = -- START testLock v1 testLock :: Property -testLock = prop_Game $ Actions [Lock w1 "hunter2" 0] +testLock = prop_Game $ actionsFromList [Lock w1 "hunter2" 0] -- END testLock v1 testLockWithMaxSuccess :: () @@ -313,13 +313,13 @@ testLockWithMaxSuccess = () where -- START testLock withMaxSuccess testLock :: Property - testLock = withMaxSuccess 1 . prop_Game $ Actions [Lock w1 "hunter2" 0] + testLock = withMaxSuccess 1 . prop_Game $ actionsFromList [Lock w1 "hunter2" 0] -- END testLock withMaxSuccess -- START testDoubleLock testDoubleLock :: Property testDoubleLock = prop_Game $ - Actions + actionsFromList [Lock w1 "*******" 0, Lock w1 "secret" 0] -- END testDoubleLock @@ -382,9 +382,9 @@ v1_model = () precondition s _ = True -- END precondition v1 - perform :: HandleFun GameModel -> ModelState GameModel -> Action GameModel -> EmulatorTraceNoStartContract () + perform :: HandleFun GameModel -> (SymToken -> AssetClass) -> ModelState GameModel -> Action GameModel -> SpecificationEmulatorTrace () -- START perform v1 - perform handle s cmd = case cmd of + perform handle _ s cmd = case cmd of Lock w new val -> do callEndpoint @"lock" (handle $ WalletKey w) LockArgs{ lockArgsSecret = secretArg new @@ -487,7 +487,7 @@ noLockedFunds_v1 = () noLockedFunds :: DL GameModel () noLockedFunds = do anyActions_ - assertModel "Locked funds should be zero" $ isZero . lockedValue + assertModel "Locked funds should be zero" $ symIsZero . lockedValue -- END noLockedFunds v1 noLockedFunds_v2 :: () @@ -501,7 +501,7 @@ noLockedFunds_v2 = () secret <- viewContractState currentSecret val <- viewContractState gameValue action $ Guess w "" secret val - assertModel "Locked funds should be zero" $ isZero . lockedValue + assertModel "Locked funds should be zero" $ symIsZero . lockedValue -- END noLockedFunds v2 noLockedFunds_v3 :: () @@ -516,7 +516,7 @@ noLockedFunds_v3 = () val <- viewContractState gameValue when (val > 0) $ do action $ Guess w "" secret val - assertModel "Locked funds should be zero" $ isZero . lockedValue + assertModel "Locked funds should be zero" $ symIsZero . lockedValue -- END noLockedFunds v3 noLockedFunds_v4 :: () @@ -532,7 +532,7 @@ noLockedFunds_v4 = () when (val > 0) $ do action $ GiveToken w action $ Guess w "" secret val - assertModel "Locked funds should be zero" $ isZero . lockedValue + assertModel "Locked funds should be zero" $ symIsZero . lockedValue -- END noLockedFunds v4 noLockedFunds_v5 :: () @@ -549,7 +549,7 @@ noLockedFunds_v5 = () monitor $ label "Unlocking funds" action $ GiveToken w action $ Guess w secret "" val - assertModel "Locked funds should be zero" $ isZero . lockedValue + assertModel "Locked funds should be zero" $ symIsZero . lockedValue -- END noLockedFunds v5 typeSignatures :: forall state. ContractModel state => state -> state @@ -564,7 +564,7 @@ typeSignatures = id -- END precondition type precondition = ContractModel.precondition -- START perform type - perform :: HandleFun state -> ModelState state -> Action state -> EmulatorTraceNoStartContract () + perform :: HandleFun state -> (SymToken -> AssetClass) -> ModelState state -> Action state -> SpecificationEmulatorTrace () -- END perform type perform = ContractModel.perform -- START shrinkAction type diff --git a/doc/plutus/tutorials/contract-testing.rst b/doc/plutus/tutorials/contract-testing.rst index cc4be16832..1a60ef5388 100644 --- a/doc/plutus/tutorials/contract-testing.rst +++ b/doc/plutus/tutorials/contract-testing.rst @@ -211,17 +211,19 @@ we simply distinguish contract instance keys by the wallet they are running in: :start-after: START ContractInstanceKey :end-before: END ContractInstanceKey -Once this type is defined, we can construct our :hsobj:`Plutus.Contract.Test.ContractModel.ContractInstanceSpec` by filling -in the :hsobj:`Plutus.Contract.Test.ContractModel.initialHandleSpecs` field of the ``ContractModel`` class: +Once this type is defined, we can tell QuickCheck what code to run for a given +contract by filling in the +:hsobj:`Plutus.Contract.Test.ContractModel.initialInstances`, +:hsobj:`Plutus.Contract.Test.ContractModel.instanceWallet`, and +:hsobj:`Plutus.Contract.Test.ContractModel.instanceContract` fields of the +``ContractModel`` class: .. literalinclude:: GameModel.hs :start-after: START initialHandleSpecs :end-before: END initialHandleSpecs -This specifies (reading from right to left) that we should create one -contract instance per wallet, running ``G.contract``, the contract -under test, in emulated wallet ``w``, and distinguished by a -:hsobj:`Plutus.Contract.Test.ContractModel.ContractInstanceKey` of the form ``WalletKey w``. +This specifies (reading top to bottom) that we should create one +contract instance per wallet ``w``, that will run ``G.contract``, in wallet ``w``. Now we can run tests, although of course they will not yet succeed: @@ -516,7 +518,7 @@ transfer the game :term:`token` from one wallet to another as specified by :end-before: END perform v1 Every call to an end-point must be associated with one of the contract -instances defined in our ``initialHandleSpecs``; the ``handle`` argument to +instances defined in our ``initialInstances``; the ``handle`` argument to :hsobj:`Plutus.Contract.Test.ContractModel.perform` lets us find the contract handle associated with each :hsobj:`Plutus.Contract.Test.ContractModel.ContractInstanceKey`. @@ -672,12 +674,6 @@ blockchain. Likewise, we delay one slot after each of the other actions. (If the delays we insert are too short, we will discover this later via failed tests). -We can cause the emulator to delay a number of slots like this: - -.. literalinclude:: GameModel.hs - :start-after: START delay - :end-before: END delay - We add a call to ``delay`` in each branch of :hsobj:`Plutus.Contract.Test.ContractModel.perform`: .. literalinclude:: GameModel.hs diff --git a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-contract.nix b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-contract.nix index 727f2ae35a..55ce848302 100644 --- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-contract.nix +++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-contract.nix @@ -151,6 +151,7 @@ "Plutus/Contract/Test/Coverage" "Plutus/Contract/Test/ContractModel" "Plutus/Contract/Test/ContractModel/Internal" + "Plutus/Contract/Test/ContractModel/Symbolics" "Plutus/Contract/Test/ContractModel/CrashTolerance" ]; hsSourceDirs = [ "src" ]; diff --git a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-doc.nix b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-doc.nix index 7cd2f584e0..175c0fb1b9 100644 --- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-doc.nix +++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-doc.nix @@ -48,6 +48,7 @@ (hsPkgs."plutus-contract" or (errorHandler.buildDepError "plutus-contract")) (hsPkgs."playground-common" or (errorHandler.buildDepError "playground-common")) (hsPkgs."plutus-use-cases" or (errorHandler.buildDepError "plutus-use-cases")) + (hsPkgs."quickcheck-dynamic" or (errorHandler.buildDepError "quickcheck-dynamic")) (hsPkgs."prettyprinter" or (errorHandler.buildDepError "prettyprinter")) (hsPkgs."containers" or (errorHandler.buildDepError "containers")) (hsPkgs."freer-extras" or (errorHandler.buildDepError "freer-extras")) diff --git a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-contract.nix b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-contract.nix index 727f2ae35a..55ce848302 100644 --- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-contract.nix +++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-contract.nix @@ -151,6 +151,7 @@ "Plutus/Contract/Test/Coverage" "Plutus/Contract/Test/ContractModel" "Plutus/Contract/Test/ContractModel/Internal" + "Plutus/Contract/Test/ContractModel/Symbolics" "Plutus/Contract/Test/ContractModel/CrashTolerance" ]; hsSourceDirs = [ "src" ]; diff --git a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-doc.nix b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-doc.nix index 7cd2f584e0..175c0fb1b9 100644 --- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-doc.nix +++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-doc.nix @@ -48,6 +48,7 @@ (hsPkgs."plutus-contract" or (errorHandler.buildDepError "plutus-contract")) (hsPkgs."playground-common" or (errorHandler.buildDepError "playground-common")) (hsPkgs."plutus-use-cases" or (errorHandler.buildDepError "plutus-use-cases")) + (hsPkgs."quickcheck-dynamic" or (errorHandler.buildDepError "quickcheck-dynamic")) (hsPkgs."prettyprinter" or (errorHandler.buildDepError "prettyprinter")) (hsPkgs."containers" or (errorHandler.buildDepError "containers")) (hsPkgs."freer-extras" or (errorHandler.buildDepError "freer-extras")) diff --git a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-contract.nix b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-contract.nix index 727f2ae35a..55ce848302 100644 --- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-contract.nix +++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-contract.nix @@ -151,6 +151,7 @@ "Plutus/Contract/Test/Coverage" "Plutus/Contract/Test/ContractModel" "Plutus/Contract/Test/ContractModel/Internal" + "Plutus/Contract/Test/ContractModel/Symbolics" "Plutus/Contract/Test/ContractModel/CrashTolerance" ]; hsSourceDirs = [ "src" ]; diff --git a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-doc.nix b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-doc.nix index 7cd2f584e0..175c0fb1b9 100644 --- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-doc.nix +++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-doc.nix @@ -48,6 +48,7 @@ (hsPkgs."plutus-contract" or (errorHandler.buildDepError "plutus-contract")) (hsPkgs."playground-common" or (errorHandler.buildDepError "playground-common")) (hsPkgs."plutus-use-cases" or (errorHandler.buildDepError "plutus-use-cases")) + (hsPkgs."quickcheck-dynamic" or (errorHandler.buildDepError "quickcheck-dynamic")) (hsPkgs."prettyprinter" or (errorHandler.buildDepError "prettyprinter")) (hsPkgs."containers" or (errorHandler.buildDepError "containers")) (hsPkgs."freer-extras" or (errorHandler.buildDepError "freer-extras")) diff --git a/plutus-contract/plutus-contract.cabal b/plutus-contract/plutus-contract.cabal index 11285fdee5..376ea33db8 100644 --- a/plutus-contract/plutus-contract.cabal +++ b/plutus-contract/plutus-contract.cabal @@ -161,6 +161,7 @@ library Plutus.Contract.Test.Coverage Plutus.Contract.Test.ContractModel Plutus.Contract.Test.ContractModel.Internal + Plutus.Contract.Test.ContractModel.Symbolics Plutus.Contract.Test.ContractModel.CrashTolerance build-depends: tasty -any, diff --git a/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs b/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs index ae68c7fea2..e367531438 100644 --- a/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs +++ b/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE PatternSynonyms #-} module Plutus.Contract.Test.ContractModel ( -- * Contract models -- @@ -11,12 +12,15 @@ module Plutus.Contract.Test.ContractModel , balanceChange , minted , lockedValue + , symIsZero , GetModelState(..) , getContractState , askModelState , askContractState , viewModelState , viewContractState + , SymToken + , symAssetClassValue -- ** The Spec monad -- -- $specMonad @@ -29,8 +33,13 @@ module Plutus.Contract.Test.ContractModel , withdraw , transfer , modifyContractState + , createToken , ($=) , ($~) + -- * Helper functions for writing perform functions + , SpecificationEmulatorTrace + , registerToken + , delay -- * Test scenarios -- -- $dynamicLogic @@ -63,11 +72,15 @@ module Plutus.Contract.Test.ContractModel -- -- $runningProperties , Actions(..) + , Act(..) + , pattern Actions + , actionsFromList -- ** Wallet contract handles -- -- $walletHandles , SchemaConstraints , ContractInstanceSpec(..) + , SomeContractInstanceKey(..) , HandleFun -- ** Model properties , propSanityCheckModel @@ -82,6 +95,7 @@ module Plutus.Contract.Test.ContractModel , propRunActions_ , propRunActions , propRunActionsWithOptions + , defaultCheckOptionsContractModel -- ** DL properties , forAllDL -- ** Test cases @@ -97,6 +111,9 @@ module Plutus.Contract.Test.ContractModel -- $noLockedFunds , NoLockedFundsProof(..) , checkNoLockedFundsProof + , checkNoLockedFundsProofFast + , checkNoLockedFundsProofWithWiggleRoom + , checkNoLockedFundsProofWithWiggleRoomFast -- $checkNoPartiality , Whitelist , whitelistOk diff --git a/plutus-contract/src/Plutus/Contract/Test/ContractModel/CrashTolerance.hs b/plutus-contract/src/Plutus/Contract/Test/ContractModel/CrashTolerance.hs index f23f96ea84..70e9253802 100644 --- a/plutus-contract/src/Plutus/Contract/Test/ContractModel/CrashTolerance.hs +++ b/plutus-contract/src/Plutus/Contract/Test/ContractModel/CrashTolerance.hs @@ -29,82 +29,85 @@ import Data.Functor.Compose import Data.Typeable import Plutus.Contract.Test.ContractModel.Internal import Plutus.Trace.Effects.EmulatorControl -import Plutus.Trace.Emulator qualified as Trace import Plutus.Trace.Emulator.Types import Test.QuickCheck as QC -- | This derived state is used to derive a new `ContractModel` on top of the `state` contract model -- that also specifies how the contract(s) behave when contract instances crash and restart. data WithCrashTolerance state = WithCrashTolerance { _underlyingModelState :: state - , _aliveContractInstances :: [ContractInstanceSpec state] - , _deadContractInstances :: [ContractInstanceSpec state] } + , _aliveContractInstances :: [SomeContractInstanceKey state] + , _deadContractInstances :: [SomeContractInstanceKey state] } makeLenses ''WithCrashTolerance -deriving instance (Show state, Show (ContractInstanceSpec state)) => Show (WithCrashTolerance state) -deriving instance (Eq state, Eq (ContractInstanceSpec state)) => Eq (WithCrashTolerance state) +deriving instance ContractModel state => Show (WithCrashTolerance state) +deriving instance (Eq state, ContractModel state) => Eq (WithCrashTolerance state) class ContractModel state => CrashTolerance state where -- | Specifiy what happens when a contract instance crashes - crash :: ContractInstanceSpec state -> Spec state () + crash :: SomeContractInstanceKey state -> Spec state () crash _ = return () -- | Specify what happens when a contract instance is restarted - restart :: ContractInstanceSpec state -> Spec state () + restart :: SomeContractInstanceKey state -> Spec state () restart _ = return () -- | Check if an action is available given a list of alive -- contract instances. - available :: Action state -> [ContractInstanceSpec state] -> Bool + available :: Action state -> [SomeContractInstanceKey state] -> Bool -instance (Show (ContractInstanceSpec state), Show (Action state)) => Show (Action (WithCrashTolerance state)) where +instance ContractModel state => Show (Action (WithCrashTolerance state)) where showsPrec p (Crash cis) = showParen (p >= 11) $ showString "Crash " . showsPrec 11 cis showsPrec p (Restart cis) = showParen (p >= 11) $ showString "Restart " . showsPrec 11 cis showsPrec p (UnderlyingAction a) = showsPrec p a -deriving instance (Typeable state, forall w s e. Eq (ContractInstanceKey state w s e), Eq (Action state)) => Eq (Action (WithCrashTolerance state)) +deriving instance ContractModel state => Eq (Action (WithCrashTolerance state)) deriving instance Show (ContractInstanceKey state w s e) => Show (ContractInstanceKey (WithCrashTolerance state) w s e) deriving instance Eq (ContractInstanceKey state w s e) => Eq (ContractInstanceKey (WithCrashTolerance state) w s e) -liftContractInstance :: ContractInstanceSpec state -> ContractInstanceSpec (WithCrashTolerance state) -liftContractInstance (ContractInstanceSpec k w c) = ContractInstanceSpec (UnderlyingContractInstanceKey k) w c +liftSomeContractInstanceKey :: SomeContractInstanceKey state -> SomeContractInstanceKey (WithCrashTolerance state) +liftSomeContractInstanceKey (Key k) = Key (UnderlyingContractInstanceKey k) -lowerContractInstance :: ContractInstanceSpec (WithCrashTolerance state) -> ContractInstanceSpec state -lowerContractInstance (ContractInstanceSpec (UnderlyingContractInstanceKey k) w c) = ContractInstanceSpec k w c +lowerSomeContractInstanceKey :: SomeContractInstanceKey (WithCrashTolerance state) -> SomeContractInstanceKey state +lowerSomeContractInstanceKey (Key (UnderlyingContractInstanceKey k)) = Key k instance ( Typeable state , Show (ContractInstanceSpec state) , Eq (ContractInstanceSpec state) , CrashTolerance state) => ContractModel (WithCrashTolerance state) where - data Action (WithCrashTolerance state) = Crash (ContractInstanceSpec state) - | Restart (ContractInstanceSpec state) + data Action (WithCrashTolerance state) = Crash (SomeContractInstanceKey state) + | Restart (SomeContractInstanceKey state) | UnderlyingAction (Action state) data ContractInstanceKey (WithCrashTolerance state) w s e where UnderlyingContractInstanceKey :: ContractInstanceKey state w s e -> ContractInstanceKey (WithCrashTolerance state) w s e - initialState = WithCrashTolerance initialState initialHandleSpecs [] + initialState = WithCrashTolerance initialState initialInstances [] - initialHandleSpecs = liftContractInstance <$> initialHandleSpecs + initialInstances = liftSomeContractInstanceKey <$> initialInstances + + instanceWallet (UnderlyingContractInstanceKey k) = instanceWallet k + + instanceContract s sa (UnderlyingContractInstanceKey k) = instanceContract (_underlyingModelState <$> s) sa k -- We piggy-back on the underlying mechanism for starting contract instances that we -- get from - startInstances _ (Restart cis) = [liftContractInstance cis] - startInstances s (UnderlyingAction a) = liftContractInstance <$> startInstances (_underlyingModelState <$> s) a + startInstances _ (Restart cis) = [liftSomeContractInstanceKey cis] + startInstances s (UnderlyingAction a) = liftSomeContractInstanceKey <$> startInstances (_underlyingModelState <$> s) a startInstances _ _ = [] - perform h s a = case a of - Crash (ContractInstanceSpec key _ _) -> do + perform h t s a = case a of + Crash (Key key) -> do -- I'm not sure why this has to take two slots but if you don't make it take -- two slots the crash doesn't happen if its the first action - Trace.waitNSlots 1 + delay 1 -- This turns out to be enough. Restarting a contract instance overrides the handle -- for the contract instance and the existing instance becomes garbage. This does -- leak memory, but only relatively little and only during a test. freezeContractInstance . chInstanceId $ h (UnderlyingContractInstanceKey key) - void $ Trace.waitNSlots 1 + delay 1 Restart _ -> do - void $ Trace.waitNSlots 1 + delay 1 UnderlyingAction a -> do - perform (h . UnderlyingContractInstanceKey) (_underlyingModelState <$> s) a + perform (h . UnderlyingContractInstanceKey) t (_underlyingModelState <$> s) a precondition s a = case a of -- Only crash alive contract instances @@ -130,7 +133,7 @@ instance ( Typeable state embed $ nextState a s <- Spec get -- An action may start its own contract instances and we need to keep track of them - aliveContractInstances %= ((lowerContractInstance <$> startInstances s (UnderlyingAction a)) ++) + aliveContractInstances %= ((lowerSomeContractInstanceKey <$> startInstances s (UnderlyingAction a)) ++) where embed :: Spec state a -> Spec (WithCrashTolerance state) a embed (Spec comp) = Spec (zoom (liftL _contractState underlyingModelState) comp) diff --git a/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs b/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs index 437e5644c0..127f93b12a 100644 --- a/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs +++ b/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs @@ -18,7 +18,9 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} @@ -43,12 +45,15 @@ module Plutus.Contract.Test.ContractModel.Internal , balanceChange , minted , lockedValue + , symIsZero , GetModelState(..) , getContractState , askModelState , askContractState , viewModelState , viewContractState + , SymToken + , symAssetClassValue -- ** The Spec monad -- -- $specMonad @@ -61,8 +66,12 @@ module Plutus.Contract.Test.ContractModel.Internal , withdraw , transfer , modifyContractState + , createToken , ($=) , ($~) + , SpecificationEmulatorTrace + , registerToken + , delay -- * Test scenarios -- -- $dynamicLogic @@ -85,11 +94,15 @@ module Plutus.Contract.Test.ContractModel.Internal -- -- $runningProperties , Actions(..) + , Act(..) + , pattern Actions + , actionsFromList -- ** Wallet contract handles -- -- $walletHandles , SchemaConstraints , ContractInstanceSpec(..) + , SomeContractInstanceKey(..) , HandleFun -- ** Model properties , propSanityCheckModel @@ -104,8 +117,10 @@ module Plutus.Contract.Test.ContractModel.Internal , propRunActions_ , propRunActions , propRunActionsWithOptions + , defaultCheckOptionsContractModel -- ** DL properties , forAllDL + , forAllDL_ -- ** Test cases -- -- $testCases @@ -119,6 +134,9 @@ module Plutus.Contract.Test.ContractModel.Internal -- $noLockedFunds , NoLockedFundsProof(..) , checkNoLockedFundsProof + , checkNoLockedFundsProofFast + , checkNoLockedFundsProofWithWiggleRoom + , checkNoLockedFundsProofWithWiggleRoomFast -- $checkNoPartiality , Whitelist , whitelistOk @@ -129,12 +147,28 @@ module Plutus.Contract.Test.ContractModel.Internal , checkErrorWhitelistWithOptions ) where +import Control.DeepSeq +import Control.Monad.Freer.Error (Error) +import Plutus.Trace.Effects.Assert (Assert) +import Plutus.Trace.Effects.EmulatedWalletAPI (EmulatedWalletAPI) +import Plutus.Trace.Effects.EmulatorControl (EmulatorControl) +import Plutus.Trace.Effects.RunContract (RunContract) +import Plutus.Trace.Effects.Waiting (Waiting) +import Plutus.Trace.Emulator (initialChainState) +import Plutus.Trace.Emulator.Types (ContractHandle (..), ContractInstanceMsg (..), ContractInstanceTag, + EmulatorRuntimeError (..), UserThreadMsg (..), cilMessage) + +import PlutusTx.Prelude qualified as P + +import Control.Foldl qualified as L import Control.Lens import Control.Monad.Cont import Control.Monad.Freer (Eff, raise, run) -import Control.Monad.Freer.Extras.Log (LogMessage, logMessageContent) +import Control.Monad.Freer.Extras.Log (LogMessage, LogMsg, logMessageContent) +import Control.Monad.Reader import Control.Monad.State (MonadState, State) import Control.Monad.State qualified as State +import Control.Monad.Writer qualified as Writer import Data.Aeson qualified as JSON import Data.Foldable import Data.IORef @@ -149,30 +183,30 @@ import Data.Set qualified as Set import Data.Text qualified as Text import Data.Typeable +import Ledger.Ada qualified as Ada import Ledger.Index import Ledger.Slot -import Ledger.Value (Value, isZero, leq) -import Plutus.Contract (Contract, ContractInstanceId) +import Ledger.Value (AssetClass) +import Plutus.Contract (Contract, ContractError, ContractInstanceId, Endpoint, endpoint) import Plutus.Contract.Schema (Input) import Plutus.Contract.Test +import Plutus.Contract.Test.ContractModel.Symbolics import Plutus.Contract.Test.Coverage import Plutus.Trace.Effects.EmulatorControl (discardWallets) -import Plutus.Trace.Emulator as Trace (ContractHandle (..), ContractInstanceTag, EmulatorTrace, - EmulatorTraceNoStartContract, activateContract, freezeContractInstance, - runEmulatorStream, walletInstanceTag) -import Plutus.Trace.Emulator.Types (UserThreadMsg (UserThreadErr), unContractInstanceTag) +import Plutus.Trace.Emulator as Trace (EmulatorTrace, activateContract, callEndpoint, freezeContractInstance, + runEmulatorStream, waitNSlots, walletInstanceTag) +import Plutus.Trace.Emulator.Types (unContractInstanceTag) import Plutus.V1.Ledger.Scripts import PlutusTx.Builtins qualified as Builtins import PlutusTx.Coverage import PlutusTx.ErrorCodes -import PlutusTx.Monoid (inv) import Streaming qualified as S import Test.QuickCheck.DynamicLogic.Monad qualified as DL -import Test.QuickCheck.StateModel hiding (Action, Actions, arbitraryAction, initialState, monitoring, nextState, - perform, precondition, shrinkAction, stateAfter) +import Test.QuickCheck.StateModel hiding (Action, Actions, ActionsWithShrinkState, arbitraryAction, initialState, + monitoring, nextState, perform, precondition, shrinkAction, stateAfter) import Test.QuickCheck.StateModel qualified as StateModel -import Test.QuickCheck hiding (checkCoverage, (.&&.), (.||.)) +import Test.QuickCheck hiding (ShrinkState, checkCoverage, (.&&.), (.||.)) import Test.QuickCheck qualified as QC import Test.QuickCheck.Monadic (PropertyM, monadic) import Test.QuickCheck.Monadic qualified as QC @@ -181,6 +215,15 @@ import Wallet.Emulator.Chain hiding (_currentSlot, currentSlot) import Wallet.Emulator.MultiAgent (EmulatorEvent, eteEvent) import Wallet.Emulator.Stream (EmulatorErr) +import Wallet.Emulator.Folds (postMapM) +import Wallet.Emulator.Folds qualified as Folds + +import Control.Monad.Freer.Reader qualified as Freer +import Control.Monad.Freer.Writer (Writer (..), runWriter, tell) +import Data.Void +import Plutus.Contract.Types (IsContract (..)) +import Prettyprinter + -- | Key-value map where keys and values have three indices that can vary between different elements -- of the map. Used to store `ContractHandle`s, which are indexed over observable state, schema, -- and error type. @@ -262,11 +305,12 @@ instancesForOtherWallets w (IMCons _ (WalletContractHandle w' h) m) | w /= w' = chInstanceId h : instancesForOtherWallets w m | otherwise = instancesForOtherWallets w m -activateWallets :: forall state. ContractModel state => [ContractInstanceSpec state] -> EmulatorTrace (Handles state) -activateWallets [] = return IMNil -activateWallets (ContractInstanceSpec key wallet contract : spec) = do - h <- activateContract wallet contract (instanceTag key wallet) - m <- activateWallets spec +activateWallets :: forall state. ContractModel state => ModelState state -> (SymToken -> AssetClass) -> [SomeContractInstanceKey state] -> EmulatorTrace (Handles state) +activateWallets _ _ [] = return IMNil +activateWallets st sa (Key key : keys) = do + let wallet = instanceWallet key + h <- activateContract wallet (instanceContract st sa key) (instanceTag key) + m <- activateWallets st sa keys return $ IMCons key (WalletContractHandle wallet h) m -- | A function returning the `ContractHandle` corresponding to a `ContractInstanceKey`. A @@ -282,8 +326,8 @@ type HandleFun state = forall w schema err. (Typeable w, Typeable schema, Typeab -- * the amount that has been minted (`minted`) data ModelState state = ModelState { _currentSlot :: Slot - , _balanceChanges :: Map Wallet Value - , _minted :: Value + , _balanceChanges :: Map Wallet SymValue + , _minted :: SymValue , _contractState :: state } deriving (Show) @@ -294,9 +338,10 @@ instance Functor ModelState where dummyModelState :: state -> ModelState state dummyModelState s = ModelState 0 Map.empty mempty s --- | The `Spec` monad is a state monad over the `ModelState`. It is used exclusively by the --- `nextState` function to model the effects of an action on the blockchain. -newtype Spec state a = Spec (State (ModelState state) a) +-- | The `Spec` monad is a state monad over the `ModelState` with reader and writer components to keep track +-- of newly created symbolic tokens. It is used exclusively by the `nextState` function to model the effects +-- of an action on the blockchain. +newtype Spec state a = Spec { unSpec :: Writer.WriterT [SymToken] (ReaderT (Var AssetKey) (State (ModelState state))) a } deriving (Functor, Applicative, Monad) instance MonadState state (Spec state) where @@ -310,6 +355,26 @@ instance MonadState state (Spec state) where put cs = Spec $ State.modify' $ \s -> s { _contractState = cs } {-# INLINE put #-} +data SomeContractInstanceKey state where + Key :: SchemaConstraints w s e => ContractInstanceKey state w s e -> SomeContractInstanceKey state + +instance ContractModel state => Eq (SomeContractInstanceKey state) where + Key k == Key k' = Just k == cast k' + +instance ContractModel state => Show (SomeContractInstanceKey state) where + showsPrec d (Key k) = showsPrec d k + +type SpecificationEmulatorTrace a = + Eff '[ Writer [(String, AssetClass)] + , RunContract + , Assert + , Waiting + , EmulatorControl + , EmulatedWalletAPI + , LogMsg String + , Error EmulatorRuntimeError + ] a + -- $contractModel -- -- A contract model is a type @state@ with a `ContractModel` instance. The state type should @@ -354,10 +419,14 @@ class ( Typeable state -- > Seller :: ContractInstanceKey MyModel MyObsState MySchema MyError data ContractInstanceKey state :: * -> Row * -> * -> * + -- | Get the wallet that the contract running at a specific `ContractInstanceKey` should run + -- in + instanceWallet :: ContractInstanceKey state w s e -> Wallet + -- | The 'ContractInstanceTag' of an instance key for a wallet. Defaults to 'walletInstanceTag'. -- You must override this if you have multiple instances per wallet. - instanceTag :: forall a b c. ContractInstanceKey state a b c -> Wallet -> ContractInstanceTag - instanceTag _ = walletInstanceTag + instanceTag :: forall w s e. SchemaConstraints w s e => ContractInstanceKey state w s e -> ContractInstanceTag + instanceTag = walletInstanceTag . instanceWallet -- | Given the current model state, provide a QuickCheck generator for a random next action. -- This is used in the `Arbitrary` instance for `Actions`s as well as by `anyAction` and @@ -368,7 +437,7 @@ class ( Typeable state initialState :: state -- | The initial handles - initialHandleSpecs :: [ContractInstanceSpec state] + initialInstances :: [SomeContractInstanceKey state] -- | The `precondition` function decides if a given action is valid in a given state. Typically -- actions generated by `arbitraryAction` will satisfy the precondition, but if they don't @@ -393,16 +462,25 @@ class ( Typeable state -- | Start new contract instances startInstances :: ModelState state -> Action state - -> [ContractInstanceSpec state] + -> [SomeContractInstanceKey state] startInstances _ _ = [] + -- | Map a `ContractInstanceKey` `k` to the `Contract` that is started when we start + -- `k` in a given `ModelState` with a given semantics of `SymToken`s + instanceContract :: ModelState state + -> (SymToken -> AssetClass) + -> ContractInstanceKey state w s e + -> Contract w s e () + -- | While `nextState` models the behaviour of the actions, `perform` contains the code for -- running the actions in the emulator (see "Plutus.Trace.Emulator"). It gets access to the -- wallet contract handles, the current model state, and the action to be performed. perform :: HandleFun state -- ^ Function from `ContractInstanceKey` to `ContractHandle` + -> (SymToken -> AssetClass) -- ^ Map from symbolic tokens (that may appear in actions or the state) + -- to assset class of actual blockchain token -> ModelState state -- ^ The model state before peforming the action -> Action state -- ^ The action to perform - -> EmulatorTraceNoStartContract () + -> SpecificationEmulatorTrace () -- | When a test involving random sequences of actions fails, the framework tries to find a -- minimal failing test case by shrinking the original failure. Action sequences are shrunk by @@ -439,6 +517,7 @@ makeLensesFor [("_currentSlot", "currentSlotL")] 'ModelState makeLensesFor [("_lastSlot", "lastSlotL")] 'ModelState makeLensesFor [("_balanceChanges", "balanceChangesL")] 'ModelState makeLensesFor [("_minted", "mintedL")] 'ModelState +makeLensesFor [("_tokenNameIndex", "tokenNameIndex")] 'ModelState -- | Get the current slot. -- @@ -451,7 +530,7 @@ currentSlot = currentSlotL -- argument to `propRunActionsWithOptions`. -- -- `Spec` monad update functions: `withdraw`, `deposit`, `transfer`. -balanceChanges :: Getter (ModelState state) (Map Wallet Value) +balanceChanges :: Getter (ModelState state) (Map Wallet SymValue) balanceChanges = balanceChangesL -- | Get the current balance change for a wallet. This is the delta balance, so it starts out at zero and @@ -459,18 +538,18 @@ balanceChanges = balanceChangesL -- argument to `propRunActionsWithOptions`. -- -- `Spec` monad update functions: `withdraw`, `deposit`, `transfer`. -balanceChange :: Wallet -> Getter (ModelState state) Value +balanceChange :: Wallet -> Getter (ModelState state) SymValue balanceChange w = balanceChangesL . at w . non mempty -- | Get the amount of tokens minted so far. This is used to compute `lockedValue`. -- -- `Spec` monad update functions: `mint` and `burn`. -minted :: Getter (ModelState state) Value +minted :: Getter (ModelState state) SymValue minted = mintedL -- | How much value is currently locked by contracts. This computed by subtracting the wallet -- `balances` from the `minted` value. -lockedValue :: ModelState s -> Value +lockedValue :: ModelState s -> SymValue lockedValue s = s ^. minted <> inv (fold $ s ^. balanceChanges) -- | Monads with read access to the model state: the `Spec` monad used in `nextState`, and the `DL` @@ -518,9 +597,20 @@ viewContractState l = viewModelState (contractState . l) -- Another option is to model the starting funds of each contract in the contract state and check -- that enough funds are available before performing a transfer. -runSpec :: Spec state () -> ModelState state -> ModelState state -runSpec (Spec spec) s = State.execState spec s +runSpec :: Spec state () + -> Var AssetKey + -> ModelState state + -> ModelState state +runSpec (Spec spec) v s = State.execState (runReaderT (fst <$> Writer.runWriterT spec) v) s +-- | Check if a given action creates new symbolic tokens in a given `ModelState` +createsTokens :: ContractModel state + => ModelState state + -> Action state + -> Bool +createsTokens s a = ([] /=) $ State.evalState (runReaderT (snd <$> Writer.runWriterT (unSpec (nextState a))) (Var 0)) s + +-- | Modify a field in the `ModelState` modState :: forall state a. Setter' (ModelState state) a -> (a -> a) -> Spec state () modState l f = Spec $ State.modify $ over l f @@ -540,27 +630,28 @@ waitUntil (Slot n) = do -- | Mint tokens. Minted tokens start out as `lockedValue` (i.e. owned by the contract) and can be -- transferred to wallets using `deposit`. -mint :: Value -> Spec state () -mint v = modState mintedL (<> v) +mint :: SymValueLike v => v -> Spec state () +mint v = modState mintedL (<> toSymValue v) -- | Burn tokens. Equivalent to @`mint` . `inv`@. -burn :: Value -> Spec state () -burn = mint . inv +burn :: SymValueLike v => v -> Spec state () +burn = mint . inv . toSymValue -- | Add tokens to the `balanceChange` of a wallet. The added tokens are subtracted from the -- `lockedValue` of tokens held by contracts. -deposit :: Wallet -> Value -> Spec state () -deposit w val = modState (balanceChangesL . at w) (Just . maybe val (<> val)) +deposit :: SymValueLike v => Wallet -> v -> Spec state () +deposit w val = modState (balanceChangesL . at w) (Just . maybe (toSymValue val) (<> toSymValue val)) -- | Withdraw tokens from a wallet. The withdrawn tokens are added to the `lockedValue` of tokens -- held by contracts. -withdraw :: Wallet -> Value -> Spec state () -withdraw w val = deposit w (inv val) +withdraw :: SymValueLike v => Wallet -> v -> Spec state () +withdraw w val = deposit w (inv . toSymValue $ val) -- | Transfer tokens between wallets, updating their `balances`. -transfer :: Wallet -- ^ Transfer from this wallet +transfer :: SymValueLike v + => Wallet -- ^ Transfer from this wallet -> Wallet -- ^ to this wallet - -> Value -- ^ this many tokens + -> v -- ^ this many tokens -> Spec state () transfer fromW toW val = withdraw fromW val >> deposit toW val @@ -576,6 +667,23 @@ modifyContractState f = modState contractState f ($~) :: Setter' state a -> (a -> a) -> Spec state () ($~) = (%=) +-- | Create a new symbolic token in `nextState` - must have a +-- corresponding `registerToken` call in `perform` +createToken :: String -> Spec state SymToken +createToken key = Spec $ do + var <- ask + Writer.tell [SymToken var key] + pure $ SymToken var key + +-- | Register the real token corresponding to a symbolic token created +-- in `createToken`. +registerToken :: String -> AssetClass -> SpecificationEmulatorTrace () +registerToken s ac = tell [(s, ac)] + +-- | `delay n` delays emulator execution by `n` slots +delay :: Integer -> SpecificationEmulatorTrace () +delay = void . Trace.waitNSlots . fromInteger + instance GetModelState (Spec state) where type StateType (Spec state) = state getModelState = Spec State.get @@ -586,6 +694,8 @@ handle handles key = Just (WalletContractHandle _ h) -> h Nothing -> error $ "handle: No handle for " ++ show key +type AssetMap = Map AssetKey (Map String AssetClass) + -- | 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@. -- This means that we can't use `EmulatorTrace` as the action monad in the `StateModel`. Instead @@ -593,17 +703,10 @@ handle handles key = -- (by `finalChecks`). We also need access to the contract handles, so what we are building is a -- function from the handles to an emulator trace computation returning potentially updated -- handles. -type ContractMonad state = State.State (ContractMonadState state) - -data ContractMonadState state = ContractMonadState (EmulatorAction state) [ContractInstanceSpec state] -instance Semigroup (ContractMonadState state) where - ContractMonadState f xs <> ContractMonadState g ys = ContractMonadState (f <> g) (xs <> ys) - -instance Monoid (ContractMonadState state) where - mempty = ContractMonadState mempty mempty - -newtype EmulatorAction state = EmulatorAction { runEmulatorAction :: Handles state -> EmulatorTrace (Handles state) } +-- TODO: Refactor this(!) +type EmulatorMonad = State.StateT AssetMap EmulatorTrace +newtype EmulatorAction state = EmulatorAction { runEmulatorAction :: Handles state -> EmulatorMonad (Handles state) } instance Semigroup (EmulatorAction state) where EmulatorAction f <> EmulatorAction g = EmulatorAction (f >=> g) @@ -612,29 +715,51 @@ instance Monoid (EmulatorAction state) where mempty = EmulatorAction pure mappend = (<>) -runEmulator_ :: (Handles state -> EmulatorTrace ()) -> ContractMonad state () -runEmulator_ a = State.modify (<> ContractMonadState (EmulatorAction (\ h -> h <$ a h)) []) +type ContractMonad state = State.State (ContractMonadState state) + +data ContractMonadState state = ContractMonadState { _cmsEmulatorAction :: (EmulatorAction state) + , _cmsContractInstances :: [SomeContractInstanceKey state] + , _cmsNextVarIdx :: AssetKey } + +makeLenses ''ContractMonadState + +instance Semigroup (ContractMonadState state) where + ContractMonadState f xs idx <> ContractMonadState g ys idx' = ContractMonadState (f <> g) (xs <> ys) (max idx idx') + +instance Monoid (ContractMonadState state) where + mempty = ContractMonadState mempty mempty 0 + +runEmulator_ :: (Handles state -> EmulatorMonad ()) -> ContractMonad state () +runEmulator_ a = cmsEmulatorAction %= (<> EmulatorAction (\ h -> h <$ a h)) + +runEmulator :: (Handles state -> EmulatorMonad (Handles state)) -> ContractMonad state () +runEmulator a = cmsEmulatorAction %= (<> EmulatorAction (\ h -> a h)) + +addInstances :: [SomeContractInstanceKey state] -> ContractMonad state () +addInstances keys = cmsContractInstances <>= keys -runEmulator :: (Handles state -> EmulatorTrace (Handles state)) -> ContractMonad state () -runEmulator a = State.modify (<> ContractMonadState (EmulatorAction (\ h -> a h)) []) +setHandles :: EmulatorMonad (Handles state) -> ContractMonad state () +setHandles a = cmsEmulatorAction %= (<> EmulatorAction (const a)) --- TODO: probably all this could be done more nicely. -addInstanceSpecs :: [ContractInstanceSpec state] -> ContractMonad state () -addInstanceSpecs keys = State.modify (ContractMonadState mempty keys <>) +makeVariable :: ContractMonad state AssetKey +makeVariable = do + i <- use cmsNextVarIdx + cmsNextVarIdx += 1 + pure i -setHandles :: EmulatorTrace (Handles state) -> ContractMonad state () -setHandles a = State.modify (<> ContractMonadState (EmulatorAction (const a)) []) +contractAction :: ContractModel state => ModelState state -> Action state -> StateModel.Action (ModelState state) AssetKey +contractAction s a = ContractAction (createsTokens s a) 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 + 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) () + ContractAction :: Bool -> Action state -> StateModel.Action (ModelState state) AssetKey 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 @@ -645,39 +770,51 @@ instance ContractModel state => StateModel (ModelState state) where arbitraryAction s = do a <- arbitraryAction s - return (Some @() (ContractAction a)) + return (Some (ContractAction (createsTokens s a) a)) - shrinkAction s (ContractAction a) = [ Some @() (ContractAction a') | a' <- shrinkAction s a ] - shrinkAction _ _ = [] + shrinkAction s (ContractAction _ a) = [ Some (contractAction s a') | a' <- shrinkAction s a ] + shrinkAction _ _ = [] initialState = ModelState { _currentSlot = 0 , _balanceChanges = Map.empty , _minted = mempty - , _contractState = initialState } + , _contractState = initialState + } - nextState s (ContractAction cmd) _v = runSpec (nextState cmd) s - nextState s Unilateral{} _ = s + nextState s (ContractAction _ cmd) v = runSpec (nextState cmd) v s + nextState s Unilateral{} _ = s - precondition s (ContractAction cmd) = precondition s cmd - precondition _ _ = True + precondition s (ContractAction _ cmd) = precondition s cmd + precondition _ _ = True - perform s (ContractAction cmd) _env = do + perform s (ContractAction _ cmd) envOuter = do let newKeys = startInstances s cmd - addInstanceSpecs newKeys + addInstances newKeys + v <- makeVariable runEmulator $ \ h -> do - newHandles <- activateWallets newKeys + envInner <- State.get + let lookup (SymToken outerVar idx) = case Map.lookup idx $ fold (Map.lookup (envOuter outerVar) envInner) of + Just tok -> tok + Nothing -> error $ "Missing registerToken call for token: " ++ show idx + newHandles <- lift $ activateWallets s lookup newKeys let h' = handlesAppend newHandles h - raise $ perform (handle h') s cmd + (_, result) <- lift . raise . runWriter $ perform (handle h') lookup s cmd + -- Ensure that each call to `createToken` in the spec corresponds to a call to + -- `registerToken` during execution + when (Set.size (Set.fromList . map fst $ result) /= length result) $ do + error $ "Non-unique registered token in call to perform with tokens: " ++ show result + State.modify (Map.insert v (Map.fromList result)) return h' - perform _ (Unilateral w) _env = runEmulator_ $ \ h -> do + return v + perform _ (Unilateral w) _env = runEmulator_ $ \ h -> lift $ 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 _ _ _ _ = id + monitoring (s0, s1) (ContractAction _ cmd) _env _res = monitoring (s0, s1) cmd + monitoring _ _ _ _ = 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. @@ -700,7 +837,36 @@ instance ContractModel state => StateModel (ModelState state) where -- Now the failing test can be rerun to check if changes code or model has fixed the problem. -- | A `Actions` is a list of `Action`s. -newtype Actions s = Actions [Action s] +data Actions s = ActionsWithShrinkState ShrinkState [Act s] + +{-# COMPLETE Actions #-} +pattern Actions :: [Act s] -> Actions s +pattern Actions as <- ActionsWithShrinkState _ as where + Actions as = ActionsWithShrinkState initialShrinkState as + +data Act s = Bind (Var AssetKey) (Action s) + | NoBind (Var AssetKey) (Action s) + +deriving instance ContractModel s => Eq (Act s) + +actionOf :: Act s -> Action s +actionOf (Bind _ a) = a +actionOf (NoBind _ a) = a + +varOf :: Act s -> Var AssetKey +varOf (Bind v _) = v +varOf (NoBind v _) = v + +isBind :: Act s -> Bool +isBind Bind{} = True +isBind _ = False + +actionsFromList :: [Action s] -> Actions s +actionsFromList = Actions . zipWith NoBind (Var <$> [0..]) + +instance ContractModel state => Show (Act state) where + showsPrec d (Bind (Var i) a) = showParen (d >= 11) $ showString ("tok" ++ show i ++ " := ") . showsPrec 0 a + showsPrec d (NoBind _ a) = showsPrec d a instance ContractModel state => Show (Actions state) where showsPrec d (Actions as) @@ -716,12 +882,12 @@ instance ContractModel s => Arbitrary (Actions s) where toStateModelActions :: ContractModel state => Actions state -> StateModel.Actions (ModelState state) -toStateModelActions (Actions s) = - StateModel.Actions [ Var i := ContractAction act | (i,act) <- zip [1..] s ] +toStateModelActions (ActionsWithShrinkState ss s) = + StateModel.ActionsWithShrinkState ss [ varOf act := ContractAction (isBind act) (actionOf act) | act <- s ] fromStateModelActions :: StateModel.Actions (ModelState s) -> Actions s -fromStateModelActions (StateModel.Actions s) = - Actions [act | Var _i := ContractAction act <- s] +fromStateModelActions (StateModel.ActionsWithShrinkState ss s) = + ActionsWithShrinkState ss [if b then Bind (Var i) act else NoBind (Var i) act | Var i := ContractAction b act <- s] -- | An instance of a `DL` scenario generated by `forAllDL`. It is turned into a `Actions` before -- being passed to the property argument of `forAllDL`, but in case of a failure the generated @@ -743,14 +909,17 @@ data DLTest state = -- ^ A successfully generated test case. -- | This type captures the two different kinds of `BadPrecondition`s that can occur. -data FailedStep state = Action (Action state) +data FailedStep state = Action (Act state) -- ^ A call to `action` that does not satisfy its `precondition`. | Assert String -- ^ A call to `DL.assert` or `assertModel` failed, or a `fail` in the `DL` -- monad. Stores the string argument of the corresponding call. deriving instance ContractModel s => Show (FailedStep s) -deriving instance ContractModel s => Eq (FailedStep s) +instance ContractModel s => Eq (FailedStep s) where + Assert s == Assert s' = s == s' + Action a == Action a' = actionOf a == actionOf a' + _ == _ = False instance ContractModel s => Show (DLTest s) where show (BadPrecondition as bads s) = @@ -775,7 +944,7 @@ bracket (first:rest) = [" ["++first++", "] ++ -- | One step of a test case. Either an `Action` (`Do`) or a value generated by a `DL.forAllQ` -- (`Witness`). When a `DLTest` is turned into a `Actions` to be executed the witnesses are -- stripped away. -data TestStep s = Do (Action s) +data TestStep s = Do (Act s) | forall a. (Eq a, Show a, Typeable a) => Witness a instance ContractModel s => Show (TestStep s) where @@ -787,7 +956,7 @@ toDLTest :: ContractModel state => toDLTest (BadPrecondition steps acts s) = DL.BadPrecondition (toDLTestSteps steps) (map conv acts) (dummyModelState s) where - conv (Action a) = Some (ContractAction a) + conv (Action a) = Some (ContractAction (isBind a) (actionOf a)) conv (Assert e) = Error e toDLTest (Looping steps) = DL.Looping (toDLTestSteps steps) @@ -802,16 +971,16 @@ toDLTestSteps steps = map toDLTestStep steps toDLTestStep :: ContractModel state => TestStep state -> DL.TestStep (ModelState state) -toDLTestStep (Do act) = DL.Do $ StateModel.Var 0 StateModel.:= ContractAction act +toDLTestStep (Do act) = DL.Do $ varOf act StateModel.:= ContractAction (isBind act) (actionOf act) toDLTestStep (Witness a) = DL.Witness a fromDLTest :: forall s. DL.DynLogicTest (ModelState s) -> DLTest s fromDLTest (DL.BadPrecondition steps acts s) = 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] + conv (Some (ContractAction _ act)) = [Action $ NoBind (Var 0) act] + conv (Some Unilateral{}) = [] + conv (Error e) = [Assert e] fromDLTest (DL.Looping steps) = Looping (fromDLTestSteps steps) fromDLTest (DL.Stuck steps s) = @@ -823,9 +992,9 @@ fromDLTestSteps :: [DL.TestStep (ModelState state)] -> [TestStep state] fromDLTestSteps steps = concatMap fromDLTestStep steps fromDLTestStep :: DL.TestStep (ModelState state) -> [TestStep state] -fromDLTestStep (DL.Do (_ := ContractAction act)) = [Do act] -fromDLTestStep (DL.Do (_ := Unilateral{})) = [] -fromDLTestStep (DL.Witness a) = [Witness a] +fromDLTestStep (DL.Do (v := ContractAction b act)) = [Do $ if b then Bind v act else NoBind v 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 @@ -915,7 +1084,9 @@ type DL state = DL.DL (ModelState state) -- | Generate a specific action. Fails if the action's `precondition` is not satisfied. action :: ContractModel state => Action state -> DL state () -action cmd = DL.action (ContractAction cmd) +action cmd = do + s <- getModelState + DL.action (contractAction s cmd) -- | Generate a random action using `arbitraryAction`. The generated action is guaranteed to satisfy -- its `precondition`. Fails with `Stuck` if no action satisfying the precondition can be found @@ -1036,9 +1207,15 @@ assertModel = DL.assertModel forAllDL :: (ContractModel state, Testable p) => DL state () -> (Actions state -> p) -> Property forAllDL dl prop = DL.forAllMappedDL toDLTest fromDLTest fromStateModelActions dl prop +forAllDL_ :: (ContractModel state, Testable p) => DL state () -> (Actions state -> p) -> Property +forAllDL_ dl prop = DL.forAllMappedDL_ toDLTest fromDLTest fromStateModelActions dl prop + +forAllUniqueDL :: (ContractModel state, Testable p) => Int -> ModelState state -> DL state () -> (Actions state -> p) -> Property +forAllUniqueDL nextVar state dl prop = DL.forAllUniqueDL nextVar state dl (prop . fromStateModelActions) + instance ContractModel s => DL.DynLogicModel (ModelState s) where - restricted (ContractAction act) = restricted act - restricted Unilateral{} = True + restricted (ContractAction _ act) = restricted act + restricted Unilateral{} = True instance GetModelState (DL state) where type StateType (DL state) = state @@ -1105,15 +1282,22 @@ quickCheckWithCoverage copts prop = do putStrLn . show $ pprCoverageReport (copts ^. coverageIndex) report return report -finalChecks :: CheckOptions +finalChecks :: ContractModel state + => CheckOptions -> CoverageOptions - -> ([ContractInstanceSpec state] -> TracePredicate) - -> PropertyM (ContractMonad state) a - -> PropertyM (ContractMonad state) a + -> ([SomeContractInstanceKey state] -> Env {- Outer env -} -> TracePredicate) + -> PropertyM (ContractMonad state) Env + -> PropertyM (ContractMonad state) () finalChecks opts copts predicate prop = do - x <- prop - ContractMonadState tr handleSpecs' <- QC.run State.get - let action = void $ runEmulatorAction tr IMNil + outerEnv <- prop + ContractMonadState tr keys' _ <- QC.run State.get + let innerAction :: EmulatorTrace AssetMap + innerAction = State.execStateT (runEmulatorAction tr IMNil) Map.empty + action = do + -- see note [The Env contract] + env <- innerAction + hdl <- activateContract w1 (getEnvContract @()) envContractInstanceTag + void $ callEndpoint @"register-token-env" hdl env stream :: forall effs. S.Stream (S.Of (LogMessage EmulatorEvent)) (Eff effs) (Maybe EmulatorErr) stream = fst <$> runEmulatorStream (opts ^. emulatorConfig) action (errorResult, events) = S.streamFold (,[]) run (\ (msg S.:> es) -> (fst es, (msg ^. logMessageContent) : snd es)) stream @@ -1122,8 +1306,7 @@ finalChecks opts copts predicate prop = do QC.monitor $ counterexample (show err) QC.assert False _ -> return () - addEndpointCoverage copts handleSpecs' events $ - x <$ checkPredicateInnerStream opts (noMainThreadDumbdums .&&. (predicate handleSpecs')) (void stream) debugOutput assertResult + addEndpointCoverage copts keys' events $ checkPredicateInnerStream opts (noMainThreadCrashes .&&. predicate keys' outerEnv) (void stream) debugOutput assertResult where debugOutput :: Monad m => String -> PropertyM m () debugOutput = QC.monitor . whenFail . putStrLn @@ -1132,41 +1315,40 @@ finalChecks opts copts predicate prop = do assertResult = QC.assert -- don't accept traces where the main thread crashes - noMainThreadDumbdums :: TracePredicate - noMainThreadDumbdums = assertUserLog $ \ log -> null [ () | UserThreadErr _ <- view eteEvent <$> log ] + noMainThreadCrashes :: TracePredicate + noMainThreadCrashes = assertUserLog $ \ log -> null [ () | UserThreadErr _ <- view eteEvent <$> log ] -- | Check endpoint coverage -addEndpointCoverage :: CoverageOptions - -> [ContractInstanceSpec state] +addEndpointCoverage :: ContractModel state + => CoverageOptions + -> [SomeContractInstanceKey state] -> [EmulatorEvent] -> PropertyM (ContractMonad state) a -> PropertyM (ContractMonad state) a -addEndpointCoverage copts specs es pm +addEndpointCoverage copts keys es pm | copts ^. checkCoverage, Just ref <- copts ^. coverageIORef = do x <- pm let -- Endpoint covereage - epsToCover = [(contractInstanceSpecTag s, contractInstanceEndpoints s) | s <- specs] + epsToCover = [(instanceTag k, contractInstanceEndpoints k) | Key k <- keys] epsCovered = getInvokedEndpoints es endpointCovers = [ QC.cover (view endpointCoverageReq copts t e) (e `elem` fold (Map.lookup t epsCovered)) (Text.unpack (unContractInstanceTag t) ++ " at endpoint " ++ e) | (t, eps) <- epsToCover , e <- eps ] - QC.monitor . foldr (.) id $ endpointCovers - QC.monitor $ \ p -> ioProperty $ do - modifyIORef ref (getCoverageReport es <>) - return p + coverageReport = getCoverageReport es + endpointCovers `deepseq` + (QC.monitor . foldr (.) id $ endpointCovers) + coverageReport `deepseq` + (QC.monitor $ \ p -> ioProperty $ do + modifyIORef ref (coverageReport<>) + return p) QC.monitor QC.checkCoverage return x | otherwise = pm -contractInstanceEndpoints :: ContractInstanceSpec state -> [String] -contractInstanceEndpoints (ContractInstanceSpec _ _ (_ :: Contract w schema err ())) = labels' @(Input schema) - -contractInstanceSpecTag :: ContractInstanceSpec state -> ContractInstanceTag -contractInstanceSpecTag (ContractInstanceSpec _ w _) = walletInstanceTag w - - +contractInstanceEndpoints :: forall state w s e. SchemaConstraints w s e => ContractInstanceKey state w s e -> [String] +contractInstanceEndpoints _ = labels' @(Input s) -- | Run a `Actions` in the emulator and check that the model and the emulator agree on the final -- wallet balance changes. Equivalent to @@ -1181,29 +1363,29 @@ propRunActions_ :: propRunActions_ actions = propRunActions (\ _ -> pure True) actions +-- | Default check options that include a large amount of Ada in the initial distributions to avoid having +-- to write `ContractModel`s that keep track of balances. +defaultCheckOptionsContractModel :: CheckOptions +defaultCheckOptionsContractModel = + defaultCheckOptions & emulatorConfig . initialChainState .~ (Left . Map.fromList $ zip knownWallets (repeat (Ada.lovelaceValueOf 100_000_000_000_000_000))) + -- | Run a `Actions` in the emulator and check that the model and the emulator agree on the final -- wallet balance changes, and that the given `TracePredicate` holds at the end. Equivalent to: -- -- @ --- propRunActions = `propRunActionsWithOptions` `defaultCheckOptions` +-- propRunActions = `propRunActionsWithOptions` `defaultCheckOptionsContractModel` `defaultCoverageOptions` -- @ propRunActions :: ContractModel state => (ModelState state -> TracePredicate) -- ^ Predicate to check at the end -> Actions state -- ^ The actions to run -> Property -propRunActions = propRunActionsWithOptions defaultCheckOptions defaultCoverageOptions +propRunActions = propRunActionsWithOptions defaultCheckOptionsContractModel defaultCoverageOptions -- | Run a `Actions` in the emulator and check that the model and the emulator agree on the final -- wallet balance changes, that no off-chain contract instance crashed, and that the given -- `TracePredicate` holds at the end. The predicate has access to the final model state. -- --- TODO: Remove this bit and move it to be a docstring above instead --- The `ContractInstanceSpec` argument lists the contract instances that should be created for the wallets --- involved in the test. Before the actions are run, contracts are activated using --- `activateContractWallet` and a mapping from `ContractInstanceKey`s to the resulting `ContractHandle`s is --- provided to the `perform` function. --- -- The `Actions` argument can be generated by a `forAllDL` from a `DL` scenario, or using the -- `Arbitrary` instance for actions which generates random actions using `arbitraryAction`: -- @@ -1236,8 +1418,8 @@ propRunActionsWithOptions opts copts predicate actions' = initiateWallets :: ContractModel state => ContractMonad state () initiateWallets = do - addInstanceSpecs initialHandleSpecs - setHandles $ activateWallets initialHandleSpecs + addInstances initialInstances + setHandles $ lift (activateWallets StateModel.initialState (\ _ -> error "activateWallets: no sym tokens should have been created yet") initialInstances) return () propRunActionsWithOptions' :: forall state. @@ -1250,31 +1432,87 @@ propRunActionsWithOptions' :: forall state. propRunActionsWithOptions' opts copts predicate actions = monadic (flip State.evalState mempty) $ finalChecks opts copts finalPredicate $ do QC.run initiateWallets - void $ runActionsInState StateModel.initialState actions + snd <$> runActionsInState StateModel.initialState actions where finalState = StateModel.stateAfter actions - finalPredicate handleSpecs' = predicate finalState .&&. checkBalances finalState - .&&. checkNoCrashes handleSpecs' + finalPredicate keys' outerEnv = predicate finalState .&&. checkBalances finalState outerEnv + .&&. checkNoCrashes keys' + .&&. checkNoOverlappingTokens 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) +{- Note [The Env contract] -checkNoCrashes :: forall state. ContractModel state => [ContractInstanceSpec state] -> TracePredicate -checkNoCrashes = foldr (\ (ContractInstanceSpec k w c) -> (assertOutcome c (instanceTag k w) notError "Contract instance stopped with error" .&&.)) + In order to get the environment that maps symbolic variables to actual + tokens out of the emulator we need to use a contract and the `instanceOutcome` + fold. All this contract does is it materialises the `AssetMap` that we carry + around inside the emulator. + + At the end of an emulator execution in which we want to check a property + of the symbolic tokens we need to add a call to to the `register-token-env` + endpoint and make sure that the `getEnvContract` is running. +-} + + +type EnvContractSchema = Endpoint "register-token-env" AssetMap + +envContractInstanceTag :: ContractInstanceTag +envContractInstanceTag = "supercalifragilisticexpialidocious" + +getEnvContract :: Contract w EnvContractSchema ContractError AssetMap +getEnvContract = toContract $ endpoint @"register-token-env" pure + +checkBalances :: ModelState state + -> Env -- ^ Outer env + -> TracePredicate +checkBalances s envOuter = Map.foldrWithKey (\ w sval p -> walletFundsChange w sval .&&. p) (pure True) (s ^. balanceChanges) + where + walletFundsChange w sval = + -- see Note [The Env contract] + flip postMapM ((,) <$> Folds.instanceOutcome @() (toContract getEnvContract) envContractInstanceTag + <*> L.generalize ((,) <$> Folds.walletFunds w <*> Folds.walletFees w)) $ \(outcome, (finalValue', fees)) -> do + dist <- Freer.ask @InitialDistribution + case outcome of + Done envInner -> do + let lookup (SymToken outerVar idx) = fromJust . Map.lookup idx $ fold (Map.lookup (lookUpVar envOuter outerVar) envInner) + dlt = toValue lookup sval + initialValue = fold (dist ^. at w) + finalValue = finalValue' P.+ fees + result = initialValue P.+ dlt == finalValue + unless result $ do + tell @(Doc Void) $ vsep $ + [ "Expected funds of" <+> pretty w <+> "to change by" + , " " <+> viaShow dlt] ++ + if initialValue == finalValue + then ["but they did not change"] + else ["but they changed by", " " <+> viaShow (finalValue P.- initialValue)] + pure result + _ -> error "I am the pope" + +-- See the uniqueness requirement in Note [Symbolic Tokens and Symbolic Values] +checkNoOverlappingTokens :: TracePredicate +checkNoOverlappingTokens = flip postMapM (Folds.instanceOutcome @() (toContract getEnvContract) envContractInstanceTag) $ \ outcome -> + case outcome of + Done envInner -> do + let tokens = concatMap Map.elems $ Map.elems envInner + result = Set.size (Set.fromList tokens) == length tokens + unless result $ + tell @(Doc Void) $ "Tokens:" <+> pretty tokens <+> "contain overlapping tokens at end of execution." + pure result + _ -> error "I am the pope" + +checkNoCrashes :: forall state. ContractModel state => [SomeContractInstanceKey state] -> TracePredicate +checkNoCrashes = foldr (\ (Key k) -> (assertInstanceLog (instanceTag k) notError .&&.)) (pure True) where - notError Failed{} = False - notError Done{} = True - notError NotDone{} = True + notError log = null [ () | StoppedWithError _ <- view (eteEvent . cilMessage) <$> log ] -- | Sanity check a `ContractModel`. Ensures that wallet balances are not always unchanged. propSanityCheckModel :: forall state. ContractModel state => Property propSanityCheckModel = QC.expectFailure $ noBalanceChanges . stateAfter @state where - noBalanceChanges s = all isZero (s ^. balanceChanges) + noBalanceChanges s = all symIsZero (s ^. balanceChanges) -- $noLockedFunds -- Showing that funds can not be locked in the contract forever. @@ -1305,39 +1543,66 @@ data NoLockedFundsProof model = NoLockedFundsProof -- 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 -> NoLockedFundsProof model -> Property -checkNoLockedFundsProof options 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) ] +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 + where + prop = propRunActionsWithOptions' options defaultCoverageOptions (\ _ -> pure True) . toStateModelActions + +checkNoLockedFundsProofWithWiggleRoomFast + :: (ContractModel model) + => Integer + -> NoLockedFundsProof model + -> Property +checkNoLockedFundsProofWithWiggleRoomFast wiggle = checkNoLockedFundsProofWithWiggleRoom' wiggle (const $ property True) + +checkNoLockedFundsProofWithWiggleRoom' + :: (ContractModel model) + => Integer + -> (Actions model -> Property) + -> NoLockedFundsProof model + -> Property +checkNoLockedFundsProofWithWiggleRoom' wiggle run NoLockedFundsProof{nlfpMainStrategy = mainStrat, + nlfpWalletStrategy = walletStrat } = + forAllDL anyActions_ $ \ (Actions as) -> + forAllUniqueDL (nextVarIdx as) (stateAfter $ Actions as) mainStrat $ \ (Actions as') -> + let s = stateAfter $ Actions (as ++ as') in + foldl (QC..&&.) (run (Actions $ as ++ as') QC..&&. (counterexample "Main strategy" . counterexample (show . Actions $ as ++ as') $ prop s)) + [ walletProp as w bal | (w, bal) <- Map.toList (s ^. balanceChanges) ] where - prop = propRunActionsWithOptions' options defaultCoverageOptions (\ _ -> 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') + nextVarIdx as = 1 + maximum ([0] ++ [ i | Var i <- varOf <$> as ]) + prop s = + let lockedVal = lockedValue s + in (counterexample ("Locked funds should be zero, but they are\n " ++ show lockedVal) $ symIsZero lockedVal) + + walletProp as w bal = forAllUniqueDL (nextVarIdx as) (stateAfter $ Actions as) (DL.action (Unilateral w) >> walletStrat w) $ \ (Actions as') -> + let err = "Unilateral strategy for " ++ show w ++ " should have gotten it at least\n" ++ + " " ++ show bal ++ "\n" ++ + "but it got\n" ++ + " " ++ show bal' + bal' = stateAfter (Actions $ as ++ as') ^. balanceChange w + in counterexample err (symLeqWiggle wiggle bal bal') + QC..&&. run (Actions $ as ++ as') -- | A whitelist entry tells you what final log entry prefixes -- are acceptable for a given error @@ -1385,7 +1650,7 @@ checkErrorWhitelist :: ContractModel m => Whitelist -> Actions m -> Property -checkErrorWhitelist = checkErrorWhitelistWithOptions defaultCheckOptions defaultCoverageOptions +checkErrorWhitelist = checkErrorWhitelistWithOptions defaultCheckOptionsContractModel defaultCoverageOptions -- | Check that running a contract model does not result in validation -- failures that are not accepted by the whitelist. @@ -1415,7 +1680,7 @@ checkErrorWhitelistWithOptions opts copts whitelist acts = property $ go check a checkEvents events = all checkEvent [ f | (TxnValidationFail _ _ _ (ScriptFailure f) _) <- events ] go :: TracePredicate -> Actions m -> Property - go check actions = monadic (flip State.evalState mempty) $ finalChecks opts copts (const check) $ do + go check actions = monadic (flip State.evalState mempty) $ finalChecks opts copts (\ _ _ -> check) $ do QC.run initiateWallets - void $ runActionsInState StateModel.initialState (toStateModelActions actions) + snd <$> runActionsInState StateModel.initialState (toStateModelActions actions) diff --git a/plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs b/plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs new file mode 100644 index 0000000000..1e3a66a82f --- /dev/null +++ b/plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs @@ -0,0 +1,75 @@ +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} +module Plutus.Contract.Test.ContractModel.Symbolics where + +import Ledger.Value (AssetClass, Value, assetClassValue, isZero, leq) +import PlutusTx.Monoid qualified as PlutusTx + +import Data.Aeson qualified as JSON +import Data.Foldable +import Data.Map (Map) +import Data.Map qualified as Map + +import Test.QuickCheck.StateModel hiding (Action, Actions, arbitraryAction, initialState, monitoring, nextState, + perform, precondition, shrinkAction, stateAfter) + +{- Note [Symbolic Tokens and Symbolic Values] + Symbolic tokens represent tokens that are created during runtime of a `ContractModel` test. + It is important that these tokens are *symbolic* as there needs to be a phase-separation + between the generation and execution part of a `ContractModel` test in order to ensure that + failing test cases can be shrunk - which is crucial for debugging. + + An important invariant of symbolic values is that different symbolic tokens represent + different actual tokens. This is enforced by a uniqueness check in the `ContractModel` + tests. + + A symbolic token is a Var Int. You might expect it to be a Var [AssetClass] but because the + execution of test code is split between two monads we end up needing two indirections. + + See Note [The Env contract] on how to get the meaning of the symbolic tokens out of the + inner monad. +-} + +-- | Symbolic tokens and values +newtype AssetKey = AssetKey Int deriving (Ord, Eq, Show, Num, JSON.FromJSONKey, JSON.ToJSONKey) +data SymToken = SymToken { symVar :: Var AssetKey, symVarIdx :: String } deriving (Ord, Eq) +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 + mempty = SymValue mempty mempty +instance Eq SymValue where + (SymValue m v) == (SymValue m' v') = Map.filter (/= 0) m == Map.filter (/= 0) m' + && v == v' +-- | Check if a symbolic value is zero +symIsZero :: SymValue -> Bool +symIsZero (SymValue m v) = all (==0) m && isZero v + +-- | Check if one symbolic value is less than or equal to another +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 + +toValue :: (SymToken -> AssetClass) -> SymValue -> Value +toValue symTokenMap (SymValue m v) = v <> fold [ assetClassValue (symTokenMap t) v | (t, v) <- Map.toList m ] + +class SymValueLike v where + toSymValue :: v -> SymValue + +instance SymValueLike Value where + toSymValue = SymValue mempty + +instance SymValueLike SymValue where + toSymValue = id + +inv :: SymValue -> SymValue +inv (SymValue m v) = SymValue (negate <$> m) (PlutusTx.inv v) diff --git a/plutus-contract/src/Plutus/Contract/Test/Coverage.hs b/plutus-contract/src/Plutus/Contract/Test/Coverage.hs index 4f130e3476..ff481a12ca 100644 --- a/plutus-contract/src/Plutus/Contract/Test/Coverage.hs +++ b/plutus-contract/src/Plutus/Contract/Test/Coverage.hs @@ -1,4 +1,5 @@ {-# OPTIONS_GHC -fno-warn-name-shadowing #-} +{-# OPTIONS_GHC -fno-warn-orphans #-} module Plutus.Contract.Test.Coverage ( getInvokedEndpoints , getCoverageReport @@ -12,6 +13,7 @@ import Data.Set qualified as Set import Data.Text qualified as Text +import Control.DeepSeq import Control.Lens import Ledger qualified @@ -51,4 +53,18 @@ getCoverageReport es = event <- es log <- extractLog $ event ^. eteEvent logEvent <- log - return $ coverageReportFromLogMsg (Text.unpack logEvent) + let msg = Text.unpack logEvent + return $ coverageReportFromLogMsg msg + +-- TODO: Move this to plutus core to avoid orhpan instance +instance NFData CovLoc where + rnf (CovLoc f sl el sc ec) = + rnf f `seq` + rnf sl `seq` + rnf el `seq` + rnf sc `seq` + rnf ec +instance NFData CoverageAnnotation where + rnf (CoverLocation loc) = rnf loc + rnf (CoverBool loc b) = rnf b `seq` rnf loc +deriving instance NFData CoverageReport diff --git a/plutus-contract/src/Plutus/Trace/Emulator.hs b/plutus-contract/src/Plutus/Trace/Emulator.hs index 2c52a88fc3..b689a1bb6e 100644 --- a/plutus-contract/src/Plutus/Trace/Emulator.hs +++ b/plutus-contract/src/Plutus/Trace/Emulator.hs @@ -17,7 +17,6 @@ An emulator trace is a contract trace that can be run in the Plutus emulator. module Plutus.Trace.Emulator( Emulator , EmulatorTrace - , EmulatorTraceNoStartContract , Wallet.Emulator.Stream.EmulatorErr(..) , Plutus.Trace.Emulator.Types.ContractHandle(..) , ContractInstanceTag @@ -139,18 +138,7 @@ data PrintEffect r where PrintLn :: String -> PrintEffect () makeEffect ''PrintEffect -type EmulatorTraceNoStartContract a = - Eff - '[ RunContract - , Assert - , Waiting - , EmulatorControl - , EmulatedWalletAPI - , LogMsg String - , Error EmulatorRuntimeError - ] a - -type EmulatorTrace a = +type EmulatorTrace = Eff '[ StartContract , RunContract @@ -160,7 +148,7 @@ type EmulatorTrace a = , EmulatedWalletAPI , LogMsg String , Error EmulatorRuntimeError - ] a + ] handleEmulatorTrace :: forall effs a. diff --git a/plutus-contract/src/Plutus/Trace/Emulator/Types.hs b/plutus-contract/src/Plutus/Trace/Emulator/Types.hs index 2d452d8485..537a30d773 100644 --- a/plutus-contract/src/Plutus/Trace/Emulator/Types.hs +++ b/plutus-contract/src/Plutus/Trace/Emulator/Types.hs @@ -52,6 +52,7 @@ module Plutus.Trace.Emulator.Types( , UserThreadMsg(..) ) where +import Control.DeepSeq import Control.Lens import Control.Monad.Freer.Coroutine import Control.Monad.Freer.Error @@ -176,6 +177,9 @@ data ContractInstanceTag = ContractInstanceTag { unContractInstanceTag :: Text, deriving stock (Eq, Ord, Show, Generic) deriving anyclass (ToJSON, FromJSON) +instance NFData ContractInstanceTag where + rnf (ContractInstanceTag txt txt') = rnf txt `seq` rnf txt' `seq` () + instance Pretty ContractInstanceTag where pretty = pretty . shortContractInstanceTag diff --git a/plutus-contract/test/Spec/ErrorChecking.hs b/plutus-contract/test/Spec/ErrorChecking.hs index ac1f653a95..e1b7ba4f59 100644 --- a/plutus-contract/test/Spec/ErrorChecking.hs +++ b/plutus-contract/test/Spec/ErrorChecking.hs @@ -29,7 +29,7 @@ import Plutus.Trace.Emulator as Trace import PlutusTx qualified import PlutusTx.ErrorCodes import PlutusTx.IsData.Class -import PlutusTx.Prelude +import PlutusTx.Prelude hiding ((<$)) import Prelude qualified as Haskell @@ -48,23 +48,23 @@ tests = testGroup "error checking" -- | Normal failures should be allowed prop_FailFalse :: Property -prop_FailFalse = checkErrorWhitelist defaultWhitelist (Actions [FailFalse]) +prop_FailFalse = checkErrorWhitelist defaultWhitelist (actionsFromList [FailFalse]) -- | Head Nil failure should not be allowed prop_FailHeadNil :: Property -prop_FailHeadNil = checkErrorWhitelist defaultWhitelist (Actions [FailHeadNil]) +prop_FailHeadNil = checkErrorWhitelist defaultWhitelist (actionsFromList [FailHeadNil]) -- | Division by zero failure should not be allowed prop_DivZero :: Property -prop_DivZero = checkErrorWhitelist defaultWhitelist (Actions [DivZero]) +prop_DivZero = checkErrorWhitelist defaultWhitelist (actionsFromList [DivZero]) -- | Division by zero failure should not be allowed (tracing before the failure). prop_DivZero_t :: Property -prop_DivZero_t = checkErrorWhitelist defaultWhitelist (Actions [DivZero_t]) +prop_DivZero_t = checkErrorWhitelist defaultWhitelist (actionsFromList [DivZero_t]) -- | Successful validation should be allowed prop_Success :: Property -prop_Success = checkErrorWhitelist defaultWhitelist (Actions [Success]) +prop_Success = checkErrorWhitelist defaultWhitelist (actionsFromList [Success]) -- | This QuickCheck model only provides an interface to the validators used in this -- test that are convenient for testing them in isolation. @@ -84,7 +84,7 @@ instance ContractModel DummyModel where | Success deriving (Haskell.Eq, Haskell.Show) - perform handle _ cmd = void $ case cmd of + perform handle _ _ cmd = void $ case cmd of FailFalse -> do callEndpoint @"failFalse" (handle $ WalletKey w1) () Trace.waitNSlots 2 @@ -103,7 +103,11 @@ instance ContractModel DummyModel where initialState = DummyModel - initialHandleSpecs = [ContractInstanceSpec (WalletKey w1) w1 contract] + initialInstances = [Key (WalletKey w1)] + + instanceWallet (WalletKey w) = w + + instanceContract _ _ (WalletKey _) = contract nextState _ = wait 2 diff --git a/plutus-use-cases/src/Plutus/Contracts/Uniswap/OffChain.hs b/plutus-use-cases/src/Plutus/Contracts/Uniswap/OffChain.hs index d4b9c0c98c..650c788a61 100644 --- a/plutus-use-cases/src/Plutus/Contracts/Uniswap/OffChain.hs +++ b/plutus-use-cases/src/Plutus/Contracts/Uniswap/OffChain.hs @@ -15,6 +15,7 @@ {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -g -fplugin-opt PlutusTx.Plugin:coverage-all #-} module Plutus.Contracts.Uniswap.OffChain ( poolStateCoinFromUniswapCurrency, liquidityCoin @@ -27,6 +28,7 @@ module Plutus.Contracts.Uniswap.OffChain , UniswapOwnerSchema , start, create, add, remove, close, swap, pools , ownerEndpoint, userEndpoints + , findSwapA, findSwapB, covIdx ) where import Control.Lens (view) @@ -46,6 +48,8 @@ import Plutus.Contracts.Uniswap.OnChain (mkUniswapValidator, validateLiquidityMi import Plutus.Contracts.Uniswap.Pool import Plutus.Contracts.Uniswap.Types import PlutusTx qualified +import PlutusTx.Code +import PlutusTx.Coverage import PlutusTx.Prelude hiding (Semigroup (..), dropWhile, flip, unless) import Prelude as Haskell (Int, Semigroup (..), String, div, dropWhile, flip, show, (^)) import Text.Printf (printf) @@ -112,6 +116,10 @@ liquidityPolicy us = mkMintingPolicyScript $ `PlutusTx.applyCode` PlutusTx.liftCode us `PlutusTx.applyCode` PlutusTx.liftCode poolStateTokenName +covIdx :: CoverageIndex +covIdx = getCovIdx $$(PlutusTx.compile [|| \u t -> Scripts.wrapMintingPolicy (validateLiquidityMinting u t) ||]) <> + getCovIdx $$(PlutusTx.compile [|| mkUniswapValidator ||]) + liquidityCurrency :: Uniswap -> CurrencySymbol liquidityCurrency = scriptCurrencySymbol . liquidityPolicy diff --git a/plutus-use-cases/src/Plutus/Contracts/Uniswap/OnChain.hs b/plutus-use-cases/src/Plutus/Contracts/Uniswap/OnChain.hs index 3506a66b0b..2f46b3734d 100644 --- a/plutus-use-cases/src/Plutus/Contracts/Uniswap/OnChain.hs +++ b/plutus-use-cases/src/Plutus/Contracts/Uniswap/OnChain.hs @@ -15,6 +15,7 @@ {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# options_ghc -fno-specialise #-} +{-# OPTIONS_GHC -g -fplugin-opt PlutusTx.Plugin:coverage-all #-} module Plutus.Contracts.Uniswap.OnChain ( mkUniswapValidator diff --git a/plutus-use-cases/src/Plutus/Contracts/Uniswap/Pool.hs b/plutus-use-cases/src/Plutus/Contracts/Uniswap/Pool.hs index f384c7f852..d6d4958baf 100644 --- a/plutus-use-cases/src/Plutus/Contracts/Uniswap/Pool.hs +++ b/plutus-use-cases/src/Plutus/Contracts/Uniswap/Pool.hs @@ -1,6 +1,7 @@ {-# LANGUAGE NoImplicitPrelude #-} {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +{-# OPTIONS_GHC -g -fplugin-opt PlutusTx.Plugin:coverage-all #-} module Plutus.Contracts.Uniswap.Pool ( calculateAdditionalLiquidity diff --git a/plutus-use-cases/test/Spec/Auction.hs b/plutus-use-cases/test/Spec/Auction.hs index 8bf16fb6a7..aa5bf026f3 100644 --- a/plutus-use-cases/test/Spec/Auction.hs +++ b/plutus-use-cases/test/Spec/Auction.hs @@ -70,7 +70,7 @@ theToken = -- | 'CheckOptions' that includes 'theToken' in the initial distribution of Wallet 1. options :: CheckOptions -options = defaultCheckOptions +options = defaultCheckOptionsContractModel & changeInitialWalletValue w1 ((<>) theToken) seller :: Contract AuctionOutput SellerSchema AuctionError () @@ -85,10 +85,10 @@ trace1WinningBid = Ada.adaOf 50 auctionTrace1 :: Trace.EmulatorTrace () auctionTrace1 = do sellerHdl <- Trace.activateContractWallet w1 seller - _ <- Trace.waitNSlots 3 + void $ Trace.waitNSlots 3 currency <- extractAssetClass sellerHdl hdl2 <- Trace.activateContractWallet w2 (buyer currency) - _ <- Trace.waitNSlots 1 + void $ Trace.waitNSlots 1 Trace.callEndpoint @"bid" hdl2 trace1WinningBid void $ Trace.waitUntilTime $ apEndTime params void $ Trace.waitNSlots 1 @@ -106,15 +106,15 @@ extractAssetClass handle = do auctionTrace2 :: Trace.EmulatorTrace () auctionTrace2 = do sellerHdl <- Trace.activateContractWallet w1 seller - _ <- Trace.waitNSlots 3 + void $ Trace.waitNSlots 3 currency <- extractAssetClass sellerHdl hdl2 <- Trace.activateContractWallet w2 (buyer currency) hdl3 <- Trace.activateContractWallet w3 (buyer currency) - _ <- Trace.waitNSlots 1 + void $ Trace.waitNSlots 1 Trace.callEndpoint @"bid" hdl2 (Ada.adaOf 50) - _ <- Trace.waitNSlots 15 + void $ Trace.waitNSlots 15 Trace.callEndpoint @"bid" hdl3 (Ada.adaOf 60) - _ <- Trace.waitNSlots 35 + void $ Trace.waitNSlots 35 Trace.callEndpoint @"bid" hdl2 trace2WinningBid void $ Trace.waitUntilTime $ apEndTime params void $ Trace.waitNSlots 1 @@ -189,7 +189,13 @@ instance ContractModel AuctionModel where , _phase = NotStarted } - initialHandleSpecs = ContractInstanceSpec SellerH w1 seller : [ ContractInstanceSpec (BuyerH w) w (buyer threadToken) | w <- [w2, w3, w4] ] + initialInstances = Key SellerH : [ Key (BuyerH w) | w <- [w2, w3, w4] ] + + instanceWallet SellerH = w1 + instanceWallet (BuyerH w) = w + + instanceContract _ _ SellerH = seller + instanceContract _ _ BuyerH{} = buyer threadToken arbitraryAction s | p /= NotStarted = @@ -208,19 +214,9 @@ instance ContractModel AuctionModel where -- In order to place a bid, we need to satisfy the constraint where -- each tx output must have at least N Ada. - -- - -- When we bid, we must make sure that we don't bid too high such - -- that: - -- - we can't pay for fees anymore - -- - we have a tx output of less than N Ada. - -- - -- We suppose the initial balance is 100 Ada. Needs to be changed if - -- the emulator initialises the wallets with a different value. - Bid w bid -> let currentWalletBalance = Ada.adaOf 100 + Ada.fromValue (s ^. balanceChange w) - current = s ^. contractState . currentBid - in bid > current - && bid >= Ada.getLovelace Ledger.minAdaTxOut - && currentWalletBalance - Ada.lovelaceOf bid >= (Ledger.minAdaTxOut <> Ledger.maxFee) + Bid _ bid -> let current = s ^. contractState . currentBid + in bid > current + && bid >= Ada.getLovelace Ledger.minAdaTxOut _ -> True nextReactiveState slot' = do @@ -229,7 +225,7 @@ instance ContractModel AuctionModel where when (slot' >= end && p == Bidding) $ do w <- viewContractState winner bid <- viewContractState currentBid - phase $= AuctionOver + phase .= AuctionOver deposit w $ Ada.toValue Ledger.minAdaTxOut <> theToken deposit w1 $ Ada.lovelaceValueOf bid @@ -239,7 +235,7 @@ instance ContractModel AuctionModel where end <- viewContractState endSlot case cmd of Init -> do - phase $= Bidding + phase .= Bidding withdraw w1 $ Ada.toValue Ledger.minAdaTxOut <> theToken wait 3 WaitUntil slot' -> waitUntil slot' @@ -249,12 +245,12 @@ instance ContractModel AuctionModel where when (slot < end) $ do withdraw w $ Ada.lovelaceValueOf bid deposit leader $ Ada.lovelaceValueOf current - currentBid $= bid - winner $= w + currentBid .= bid + winner .= w - perform _ _ Init = delay 3 - perform _ _ (WaitUntil slot) = void $ Trace.waitUntilSlot slot - perform handle _ (Bid w bid) = do + 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 @@ -272,9 +268,6 @@ instance ContractModel AuctionModel where monitoring _ _ = id -delay :: Integer -> Trace.EmulatorTraceNoStartContract () -delay n = void $ Trace.waitNSlots $ fromIntegral n - prop_Auction :: Actions AuctionModel -> Property prop_Auction script = propRunActionsWithOptions (set minLogLevel Info options) defaultCoverageOptions @@ -287,7 +280,7 @@ finishAuction = do anyActions_ slot <- viewModelState currentSlot when (slot < 101) $ action $ WaitUntil 101 - assertModel "Locked funds are not zero" (Value.isZero . lockedValue) + assertModel "Locked funds are not zero" (symIsZero . lockedValue) prop_FinishAuction :: Property prop_FinishAuction = forAllDL finishAuction prop_Auction diff --git a/plutus-use-cases/test/Spec/Crowdfunding.hs b/plutus-use-cases/test/Spec/Crowdfunding.hs index 840bb720d3..74cb78ce06 100644 --- a/plutus-use-cases/test/Spec/Crowdfunding.hs +++ b/plutus-use-cases/test/Spec/Crowdfunding.hs @@ -201,10 +201,15 @@ instance ContractModel CrowdfundingModel where , _endSlot = TimeSlot.posixTimeToEnclosingSlot def $ campaignDeadline params } - initialHandleSpecs = ContractInstanceSpec (OwnerKey w1) w1 (crowdfunding params) : - [ ContractInstanceSpec (ContributorKey w) w (crowdfunding params) | w <- contributorWallets ] + initialInstances = (Key $ OwnerKey w1) : [ (Key $ ContributorKey w) | w <- contributorWallets ] - perform h s a = case a of + instanceWallet (OwnerKey w) = w + instanceWallet (ContributorKey w) = w + + instanceContract _ _ OwnerKey{} = crowdfunding params + 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) () @@ -215,7 +220,7 @@ instance ContractModel CrowdfundingModel where withdraw w v contributions $~ Map.insert w v CStart -> do - ownerOnline $= True + ownerOnline .= True nextReactiveState slot' = do -- If the owner is online and its after the @@ -227,35 +232,26 @@ instance ContractModel CrowdfundingModel where owner <- viewContractState ownerWallet cMap <- viewContractState contributions deposit owner (fold cMap) - contributions $= Map.empty - ownerOnline $= False - ownerContractDone $= True + contributions .= Map.empty + ownerOnline .= False + ownerContractDone .= True -- If its after the end of the collection time range -- the remaining funds are collected by the contracts collectDeadline <- viewContractState collectDeadlineSlot when (slot' >= collectDeadline) $ do cMap <- viewContractState contributions mapM_ (uncurry deposit) (Map.toList cMap) - contributions $= Map.empty + contributions .= Map.empty -- 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. - -- - -- We must make sure that we don't contribute a too high value such that: - -- - we can't pay for fees anymore - -- - have a tx output of less than N Ada. - -- - -- We suppose the initial balance is 100 Ada. Needs to be changed if - -- the emulator initialises the wallets with a different value. - CContribute w v -> let currentWalletBalance = Ada.adaOf 100 + Ada.fromValue (s ^. balanceChange w) - in w `notElem` Map.keys (s ^. contractState . contributions) - && w /= (s ^. contractState . ownerWallet) - && s ^. currentSlot < s ^. contractState . endSlot - && Ada.fromValue v >= Ledger.minAdaTxOut - && (currentWalletBalance - Ada.fromValue v) >= (Ledger.minAdaTxOut <> Ledger.maxFee) + CContribute w v -> w `notElem` Map.keys (s ^. contractState . contributions) + && w /= (s ^. contractState . ownerWallet) + && s ^. currentSlot < s ^. contractState . endSlot + && Ada.fromValue v >= Ledger.minAdaTxOut CStart -> Prelude.not (s ^. contractState . ownerOnline || s ^. contractState . ownerContractDone) -- To generate a random test case we need to know how to generate a random diff --git a/plutus-use-cases/test/Spec/Escrow.hs b/plutus-use-cases/test/Spec/Escrow.hs index 5fa1d44d61..818fb4e5ce 100644 --- a/plutus-use-cases/test/Spec/Escrow.hs +++ b/plutus-use-cases/test/Spec/Escrow.hs @@ -72,7 +72,11 @@ instance ContractModel EscrowModel where ] } - initialHandleSpecs = [ ContractInstanceSpec (WalletKey w) w testContract | w <- testWallets ] + initialInstances = Key . WalletKey <$> testWallets + + instanceWallet (WalletKey w) = w + + instanceContract _ _ WalletKey{} = testContract where -- TODO: Lazy test contract for now testContract = selectList [void $ payEp modelParams, void $ redeemEp modelParams, void $ refundEp modelParams] >> testContract @@ -80,7 +84,7 @@ instance ContractModel EscrowModel where nextState a = void $ case a of Pay w v -> do withdraw w (Ada.adaValueOf $ fromInteger v) - contributions $~ Map.insertWith (<>) w (Ada.adaValueOf $ fromInteger v) + contributions %= Map.insertWith (<>) w (Ada.adaValueOf $ fromInteger v) wait 1 Redeem w -> do targets <- viewContractState targets @@ -88,11 +92,11 @@ instance ContractModel EscrowModel where sequence_ [ deposit w v | (w, v) <- Map.toList targets ] let leftoverValue = fold contribs <> inv (fold targets) deposit w leftoverValue - contributions $= Map.empty + contributions .= Map.empty wait 1 Refund w -> do v <- viewContractState $ contributions . at w . to fold - contributions $~ Map.delete w + contributions %= Map.delete w deposit w v wait 1 WaitUntil s -> do @@ -108,17 +112,17 @@ instance ContractModel EscrowModel where && s ^. currentSlot + 1 < s ^. contractState . refundSlot && Ada.adaValueOf (fromInteger v) `geq` Ada.toValue minAdaTxOut - perform h _ a = void $ case a of - WaitUntil slot -> Trace.waitUntilSlot slot + 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) - Trace.waitNSlots 1 + delay 1 Redeem w -> do Trace.callEndpoint @"redeem-escrow" (h $ WalletKey w) () - Trace.waitNSlots 1 + delay 1 Refund w -> do Trace.callEndpoint @"refund-escrow" (h $ WalletKey w) () - Trace.waitNSlots 1 + delay 1 arbitraryAction s = oneof $ [ Pay <$> QC.elements testWallets <*> choose @Integer (10, 30) , Redeem <$> QC.elements testWallets diff --git a/plutus-use-cases/test/Spec/GameStateMachine.hs b/plutus-use-cases/test/Spec/GameStateMachine.hs index 374324c5ed..8c5ca40344 100644 --- a/plutus-use-cases/test/Spec/GameStateMachine.hs +++ b/plutus-use-cases/test/Spec/GameStateMachine.hs @@ -36,7 +36,7 @@ import Test.Tasty.QuickCheck (testProperty) import Ledger qualified import Ledger.Ada qualified as Ada import Ledger.Typed.Scripts qualified as Scripts -import Ledger.Value (Value, isZero) +import Ledger.Value (Value) import Plutus.Contract.Secrets import Plutus.Contract.Test hiding (not) import Plutus.Contract.Test.ContractModel @@ -77,11 +77,15 @@ instance ContractModel GameModel where , _currentSecret = "" } - initialHandleSpecs = [ ContractInstanceSpec (WalletKey w) w G.contract | w <- wallets ] + initialInstances = Key . WalletKey <$> wallets + + instanceWallet (WalletKey w) = w + + instanceContract _ _ WalletKey{} = G.contract -- 'perform' gets a state, which includes the GameModel state, but also contract handles for the -- wallets and what the model thinks the current balances are. - perform handle s cmd = case cmd of + perform handle _ s cmd = case cmd of Lock w new val -> do Trace.callEndpoint @"lock" (handle $ WalletKey w) LockArgs{lockArgsSecret = secretArg new, lockArgsValue = Ada.lovelaceValueOf val} @@ -100,9 +104,9 @@ instance ContractModel GameModel where -- 'nextState' descibes how each command affects the state of the model nextState (Lock w secret val) = do - hasToken $= Just w - currentSecret $= secret - gameValue $= val + hasToken .= Just w + currentSecret .= secret + gameValue .= val mint gameTokenVal deposit w gameTokenVal withdraw w $ Ada.lovelaceValueOf val @@ -111,8 +115,8 @@ instance ContractModel GameModel where nextState (Guess w old new val) = do correct <- (old ==) <$> viewContractState currentSecret when correct $ do - currentSecret $= new - gameValue $~ subtract val + currentSecret .= new + gameValue %= subtract val deposit w $ Ada.lovelaceValueOf val wait 1 @@ -121,7 +125,7 @@ instance ContractModel GameModel where withdraw w0 $ Ada.toValue Ledger.minAdaTxOut deposit w $ Ada.toValue Ledger.minAdaTxOut transfer w0 w gameTokenVal - hasToken $= Just w + hasToken .= Just w wait 1 -- To generate a random test case we need to know how to generate a random @@ -137,22 +141,14 @@ instance ContractModel GameModel where genLockAction :: Gen (Action GameModel) genLockAction = do w <- genWallet - let currentWalletBalance = Ada.getLovelace $ Ada.adaOf 100 + Ada.fromValue (s ^. balanceChange w) - pure (Lock w) <*> genGuess <*> choose (Ada.getLovelace Ledger.minAdaTxOut, currentWalletBalance) + pure (Lock w) <*> genGuess <*> choose (Ada.getLovelace Ledger.minAdaTxOut, Ada.getLovelace (Ada.adaOf 100)) -- The 'precondition' says when a particular command is allowed. precondition s cmd = case cmd of -- In order to lock funds, we need to satifsy the constraint where -- each tx out must have at least N Ada. - -- When we lock a value, we must make sure that we don't lock too - -- much funds, such that we can't pay to fees anymore and have a tx - -- out of less than N Ada. - -- We must also leave enough funds in order to transfer the game - -- token (along with 2 Ada) to another wallet. - Lock w _ v -> let currentWalletBalance = Ada.adaOf 100 + Ada.fromValue (s ^. balanceChange w) - in currentWalletBalance - Ada.lovelaceOf v - Ledger.minAdaTxOut >= Ledger.minAdaTxOut + Ledger.maxFee - && v >= Ada.getLovelace Ledger.minAdaTxOut - && isNothing tok + Lock _ _ v -> v >= Ada.getLovelace Ledger.minAdaTxOut + && isNothing tok Guess w _ _ v -> (val == v || Ada.Lovelace (val - v) >= Ledger.minAdaTxOut) && tok == Just w GiveToken _ -> isJust tok where @@ -171,8 +167,8 @@ instance ContractModel GameModel where monitoring _ _ = id instance CrashTolerance GameModel where - available (Lock w _ _) specs = ContractInstanceSpec (WalletKey w) w G.contract `elem` specs - available (Guess w _ _ _) specs = ContractInstanceSpec (WalletKey w) w G.contract `elem` specs + available (Lock w _ _) alive = (Key $ WalletKey w) `elem` alive + available (Guess w _ _ _) alive = (Key $ WalletKey w) `elem` alive available _ _ = True -- | The main property. 'propRunActions_' checks that balances match the model after each test. @@ -188,13 +184,13 @@ prop_SanityCheckModel = propSanityCheckModel @GameModel check_prop_Game_with_coverage :: IO CoverageReport check_prop_Game_with_coverage = quickCheckWithCoverage (set coverageIndex covIdx $ defaultCoverageOptions) $ \covopts -> - propRunActionsWithOptions @GameModel defaultCheckOptions + propRunActionsWithOptions @GameModel defaultCheckOptionsContractModel covopts (const (pure True)) propGame' :: LogLevel -> Actions GameModel -> Property propGame' l = propRunActionsWithOptions - (set minLogLevel l defaultCheckOptions) + (set minLogLevel l defaultCheckOptionsContractModel) defaultCoverageOptions (\ _ -> pure True) @@ -216,9 +212,6 @@ genGuess = QC.elements ["hello", "secret", "hunter2", "*******"] genValue :: Gen Integer genValue = choose (Ada.getLovelace Ledger.minAdaTxOut, 100_000_000) -delay :: Int -> EmulatorTraceNoStartContract () -delay n = void $ Trace.waitNSlots (fromIntegral n) - -- Dynamic Logic ---------------------------------------------------------- prop_UnitTest :: Property @@ -253,7 +246,7 @@ noLockedFunds = do monitor $ label "Unlocking funds" action $ GiveToken w action $ Guess w secret "" val - assertModel "Locked funds should be zero" $ isZero . lockedValue + assertModel "Locked funds should be zero" $ symIsZero . lockedValue -- | Check that we can always get the money out of the guessing game (by guessing correctly). prop_NoLockedFunds :: Property @@ -279,7 +272,7 @@ noLockProof = NoLockedFundsProof{ when hasTok $ action (Guess w secret "" val) prop_CheckNoLockedFundsProof :: Property -prop_CheckNoLockedFundsProof = checkNoLockedFundsProof defaultCheckOptions noLockProof +prop_CheckNoLockedFundsProof = checkNoLockedFundsProof defaultCheckOptionsContractModel noLockProof -- * Unit tests diff --git a/plutus-use-cases/test/Spec/Prism.hs b/plutus-use-cases/test/Spec/Prism.hs index 61c8d957b6..d4dd72708b 100644 --- a/plutus-use-cases/test/Spec/Prism.hs +++ b/plutus-use-cases/test/Spec/Prism.hs @@ -146,7 +146,13 @@ instance ContractModel PrismModel where initialState = PrismModel { _walletState = Map.empty } - initialHandleSpecs = [ ContractInstanceSpec (UserH w) w C.subscribeSTO | w <- users ] ++ [ ContractInstanceSpec MirrorH mirror C.mirror ] + initialInstances = Key MirrorH : (Key . UserH <$> users) + + instanceWallet MirrorH = mirror + instanceWallet (UserH w) = w + + instanceContract _ _ MirrorH = C.mirror + instanceContract _ _ UserH{} = C.subscribeSTO precondition s (Issue w) = (s ^. contractState . isIssued w) /= Issued -- Multiple Issue (without Revoke) breaks the contract precondition _ _ = True @@ -155,8 +161,8 @@ instance ContractModel PrismModel where wait waitSlots case cmd of Delay -> wait 1 - Revoke w -> isIssued w $~ doRevoke - Issue w -> isIssued w $= Issued + Revoke w -> isIssued w %= doRevoke + Issue w -> isIssued w .= Issued Call w -> do iss <- (== Issued) <$> viewContractState (isIssued w) pend <- (== STOReady) <$> viewContractState (stoState w) @@ -166,22 +172,19 @@ instance ContractModel PrismModel where mint stoValue deposit w stoValue - perform handle _ cmd = case cmd of + perform handle _ _ cmd = case cmd of Delay -> wrap $ delay 1 Issue w -> wrap $ delay 1 >> Trace.callEndpoint @"issue" (handle MirrorH) CredentialOwnerReference{coTokenName=kyc, coOwner=w} Revoke w -> wrap $ Trace.callEndpoint @"revoke" (handle MirrorH) CredentialOwnerReference{coTokenName=kyc, coOwner=w} Call w -> wrap $ Trace.callEndpoint @"sto" (handle $ UserH w) stoSubscriber where -- v Wait a generous amount of blocks between calls - wrap m = m *> delay waitSlots + wrap m = () <$ m <* delay waitSlots shrinkAction _ Delay = [] shrinkAction _ _ = [Delay] monitoring (_, s) _ = counterexample (show s) -delay :: Integer -> Trace.EmulatorTraceNoStartContract () -delay n = void $ Trace.waitNSlots $ fromIntegral n - finalPredicate :: ModelState PrismModel -> TracePredicate finalPredicate _ = assertNotDone @_ @() @C.STOSubscriberSchema C.subscribeSTO (Trace.walletInstanceTag user) "User stopped" .&&. @@ -200,7 +203,7 @@ noLockProof = NoLockedFundsProof } prop_NoLock :: Property -prop_NoLock = checkNoLockedFundsProof defaultCheckOptions noLockProof +prop_NoLock = checkNoLockedFundsProof defaultCheckOptionsContractModel noLockProof tests :: TestTree tests = testGroup "PRISM" diff --git a/plutus-use-cases/test/Spec/SealedBidAuction.hs b/plutus-use-cases/test/Spec/SealedBidAuction.hs index 1a49366265..d70c5421bd 100644 --- a/plutus-use-cases/test/Spec/SealedBidAuction.hs +++ b/plutus-use-cases/test/Spec/SealedBidAuction.hs @@ -52,7 +52,7 @@ mpsHash = Value.CurrencySymbol $ PlutusTx.toBuiltin $ Crypto.hashToBytes $ Crypt -- | 'CheckOptions' that includes 'theToken' in the initial distribution of Wallet 1. options :: CheckOptions -options = defaultCheckOptions +options = defaultCheckOptionsContractModel & changeInitialWalletValue w1 ((<>) theToken) -- * QuickCheck model @@ -92,12 +92,17 @@ instance ContractModel AuctionModel where , _parameters = Nothing } - initialHandleSpecs = [] + initialInstances = [] - startInstances s StartContracts = ContractInstanceSpec SellerH w1 (sellerContract . fromJust $ s ^. contractState . parameters) - : [ ContractInstanceSpec (BidderH w) w (bidderContract . fromJust $ s ^. contractState . parameters) | w <- [w2, w3, w4] ] + startInstances _ StartContracts = Key SellerH : [ Key (BidderH w) | w <- [w2, w3, w4] ] startInstances _ _ = [] + instanceWallet SellerH = w1 + instanceWallet (BidderH w) = w + + instanceContract s _ SellerH = sellerContract (fromJust $ s ^. contractState . parameters) + instanceContract s _ BidderH{} = bidderContract (fromJust $ s ^. contractState . parameters) + arbitraryAction s | p /= NotStarted = frequency [ (1, WaitUntil . step <$> choose (1, 3 :: Integer)) @@ -109,7 +114,7 @@ instance ContractModel AuctionModel where -- Correct reveal , (20, uncurry Reveal <$> elements [ (w,i) | (i,w) <- s ^. contractState . currentBids ]) , (20, Payout <$> elements [w1, w2, w3, w4]) ] - | otherwise = Init <$> arbitrary + | otherwise = oneof [Init <$> arbitrary, pure StartContracts] where p = s ^. contractState . phase slot = s ^. currentSlot @@ -125,31 +130,26 @@ instance ContractModel AuctionModel where WaitUntil slot -> slot > s ^. currentSlot - Bid w v -> let currentWalletBalance = Ada.adaOf 100 + Ada.fromValue (s ^. balanceChange w) - in s ^. contractState . phase == Bidding - && w `notElem` fmap snd (s ^. contractState . currentBids) - && v >= Ada.getLovelace Ledger.minAdaTxOut - && currentWalletBalance - Ada.lovelaceOf v >= Ledger.minAdaTxOut <> Ledger.maxFee + Bid w v -> s ^. contractState . phase == Bidding + && w `notElem` fmap snd (s ^. contractState . currentBids) + && v >= Ada.getLovelace Ledger.minAdaTxOut - Reveal w v -> let currentWalletBalance = Ada.adaOf 100 + Ada.fromValue (s ^. balanceChange w) - in s ^. contractState . phase == AwaitingPayout - && w `elem` fmap snd (s ^. contractState . currentBids) - && v >= Ada.getLovelace Ledger.minAdaTxOut - && currentWalletBalance - Ada.lovelaceOf v >= Ledger.minAdaTxOut <> Ledger.maxFee + Reveal w v -> s ^. contractState . phase == AwaitingPayout + && w `elem` fmap snd (s ^. contractState . currentBids) + && v >= Ada.getLovelace Ledger.minAdaTxOut Payout _ -> s ^. contractState . phase == PayoutTime - - perform _ _ (Init _) = delay 3 - perform _ _ StartContracts = delay 3 - perform _ _ (WaitUntil slot) = void $ Trace.waitUntilSlot slot - perform handle _ (Bid w bid) = do + perform _ _ _ (Init _) = delay 3 + perform _ _ _ StartContracts = delay 3 + perform _ _ _ (WaitUntil slot) = void $ Trace.waitUntilSlot slot + perform handle _ _ (Bid w bid) = do Trace.callEndpoint @"bid" (handle $ BidderH w) (BidArgs (secretArg bid)) delay 1 - perform handle _ (Reveal w bid) = do + perform handle _ _ (Reveal w bid) = do Trace.callEndpoint @"reveal" (handle $ BidderH w) (RevealArgs bid) delay 1 - perform handle _ (Payout w) + perform handle _ _ (Payout w) | w == w1 = do Trace.callEndpoint @"payout" (handle SellerH) () delay 1 @@ -199,11 +199,11 @@ instance ContractModel AuctionModel where when ((bid, w) `elem` bids && bid > oldBid) $ do withdraw w $ Ada.lovelaceValueOf bid deposit w' $ Ada.lovelaceValueOf oldBid - currentWinningBid $= Just (bid, w) + currentWinningBid .= Just (bid, w) Nothing -> when ((bid, w) `elem` bids) $ do withdraw w $ Ada.lovelaceValueOf bid - currentWinningBid $= Just (bid, w) + currentWinningBid .= Just (bid, w) wait 1 Payout _ | currentPhase == PayoutTime -> do @@ -228,17 +228,12 @@ instance ContractModel AuctionModel where eSlot <- viewContractState endBidSlot pSlot <- viewContractState payoutSlot when (slot >= eSlot) $ do - phase $= AwaitingPayout + phase .= AwaitingPayout when (slot >= pSlot) $ do - phase $= PayoutTime - -delay :: Integer -> Trace.EmulatorTraceNoStartContract () -delay n = void $ Trace.waitNSlots $ fromIntegral n + phase .= PayoutTime prop_Auction :: Actions AuctionModel -> Property -prop_Auction = propRunActionsWithOptions options defaultCoverageOptions - (\ _ -> pure True) -- TODO: check termination - +prop_Auction = propRunActionsWithOptions options defaultCoverageOptions (\ _ -> pure True) tests :: TestTree tests = diff --git a/plutus-use-cases/test/Spec/Uniswap.hs b/plutus-use-cases/test/Spec/Uniswap.hs index 40e8c1f576..ab9fd92bf1 100644 --- a/plutus-use-cases/test/Spec/Uniswap.hs +++ b/plutus-use-cases/test/Spec/Uniswap.hs @@ -1,13 +1,519 @@ -{-# LANGUAGE OverloadedStrings #-} -module Spec.Uniswap( - tests - ) where +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing -fno-warn-redundant-constraints #-} +module Spec.Uniswap where -import Plutus.Contract.Test +import Control.Arrow +import Control.Lens hiding (elements) +import Control.Monad +import Plutus.Contract +import Plutus.Contract as Contract hiding (throwError) +import Plutus.Contract.Test hiding (not) +import Plutus.Contract.Test.ContractModel +import Plutus.Contract.Test.ContractModel.Symbolics +import Plutus.Contracts.Currency qualified as Currency +import Plutus.Contracts.Uniswap hiding (pools, setupTokens, tokenNames, wallets) import Plutus.Contracts.Uniswap.Trace qualified as Uniswap +import Plutus.Trace.Emulator (EmulatorRuntimeError (GenericError)) import Plutus.Trace.Emulator qualified as Trace +import Ledger qualified as Ledger +import Ledger.Ada qualified as Ada +import Ledger.Value qualified as Value + +import Data.Foldable +import Data.List +import Data.Maybe +import Data.Text qualified as Text + +import Data.Map (Map) +import Data.Map qualified as Map +import Data.Set (Set) +import Data.Set qualified as Set +import Data.String + +import Data.Void + +import Test.QuickCheck hiding ((.&&.)) import Test.Tasty +import Test.Tasty.QuickCheck (testProperty) + +import Data.Monoid (Last (..)) +import Data.Semigroup qualified as Semigroup + +import Ledger.Constraints + +data PoolIndex = PoolIndex SymToken SymToken deriving (Show) + +poolIndex :: SymToken -> SymToken -> PoolIndex +poolIndex t1 t2 = PoolIndex (min t1 t2) (max t1 t2) + +instance Eq PoolIndex where + PoolIndex t1 t2 == PoolIndex t1' t2' = (min t1 t2, max t1 t2) == (min t1' t2', max t1' t2') + +instance Ord PoolIndex where + compare (PoolIndex t1 t2) (PoolIndex t1' t2') = compare (min t1 t2, max t1 t2) (min t1' t2', max t1' t2') + +data PoolModel = PoolModel { _coinAAmount :: Amount A + , _coinBAmount :: Amount B + , _liquidities :: Map Wallet (Amount Liquidity) + , _liquidityToken :: SymToken + } deriving (Ord, Eq, Show) + +data UniswapModel = UniswapModel { _uniswapToken :: Maybe SymToken + , _exchangeableTokens :: Set SymToken + , _pools :: Map PoolIndex PoolModel + , _startedUserCode :: Set Wallet + } deriving (Show) + +makeLenses ''UniswapModel +makeLenses ''PoolModel + +open :: Getter PoolModel Bool +open = to $ \ p -> p ^. coinAAmount > 0 -- If one is bigger than zero the other one is too + +prop_Uniswap :: Actions UniswapModel -> Property +prop_Uniswap = propRunActions_ + +deriving instance Eq (Action UniswapModel) +deriving instance Show (Action UniswapModel) +deriving instance Eq (ContractInstanceKey UniswapModel w s e) +deriving instance Show (ContractInstanceKey UniswapModel w s e) + +walletOf :: Action UniswapModel -> Wallet +walletOf a = case a of + SetupTokens -> w1 + Start -> w1 + CreatePool w _ _ _ _ -> w + AddLiquidity w _ _ _ _ -> w + RemoveLiquidity w _ _ _ -> w + PerformSwap w _ _ _ -> w + ClosePool w _ _ -> w + +hasPool :: ModelState UniswapModel -> SymToken -> SymToken -> Bool +hasPool s t1 t2 = isJust (s ^. contractState . pools . at (poolIndex t1 t2)) + +hasOpenPool :: ModelState UniswapModel -> SymToken -> SymToken -> Bool +hasOpenPool s t1 t2 = hasPool s t1 t2 + && s ^. contractState . pools . at (poolIndex t1 t2) . to fromJust . open + +liquidityOf :: ModelState UniswapModel -> Wallet -> SymToken -> SymToken -> Amount Liquidity +liquidityOf s w t1 t2 = sum $ s ^? contractState . pools . at (poolIndex t1 t2) . _Just . liquidities . at w . to sum + +totalLiquidity :: ModelState UniswapModel -> SymToken -> SymToken -> Amount Liquidity +totalLiquidity s t1 t2 = sum $ s ^? contractState . pools . at (poolIndex t1 t2) . _Just . liquidities . to sum + +hasUniswapToken :: ModelState UniswapModel -> Bool +hasUniswapToken s = isJust $ s ^. contractState . uniswapToken + +swapUnless :: Bool -> (a, a) -> (a, a) +swapUnless b (a, a') = if b then (a, a') else (a', a) + +mkAmounts :: SymToken -> SymToken -> Integer -> Integer -> (Amount A, Amount B) +mkAmounts t1 t2 a1 a2 = Amount *** Amount $ swapUnless (t1 < t2) (a1, a2) + +getAToken, getBToken :: SymToken -> SymToken -> SymToken +getAToken = min +getBToken = max + +-- | Create some sample tokens and distribute them to +-- the emulated wallets +setupTokens :: Contract (Maybe (Semigroup.Last Currency.OneShotCurrency)) Currency.CurrencySchema Currency.CurrencyError () +setupTokens = do + ownPK <- Contract.ownPaymentPubKeyHash + cur <- Currency.mintContract ownPK [(fromString tn, fromIntegral (length wallets) * amount) | tn <- tokenNames] + let cs = Currency.currencySymbol cur + v = mconcat [Value.singleton cs (fromString tn) amount | tn <- tokenNames] + + forM_ wallets $ \w -> do + let pkh = mockWalletPaymentPubKeyHash w + when (pkh /= ownPK) $ do + cs <- mkTxConstraints @Void mempty (mustPayToPubKey pkh v) + submitTxConfirmed . adjustUnbalancedTx $ cs + + tell $ Just $ Semigroup.Last cur + where + amount = 1000000 + +wallets :: [Wallet] +wallets = take 9 knownWallets + +tokenNames :: [String] +tokenNames = ["A", "B", "C", "D"] + +instance ContractModel UniswapModel where + data Action UniswapModel = SetupTokens + -- ^ Give some tokens to wallets `w1..w4` + | Start + -- ^ Start the system by creating a pool-factory + | CreatePool Wallet SymToken Integer SymToken Integer + -- ^ Create a liquidity pool + | AddLiquidity Wallet SymToken Integer SymToken Integer + -- ^ Amount of liquidity added for each token by the wallet + | PerformSwap Wallet SymToken SymToken Integer + -- ^ Swap the first token for the second token + | RemoveLiquidity Wallet SymToken SymToken Integer + -- ^ Amount of liquidity to cash in + | ClosePool Wallet SymToken SymToken + -- ^ Close a liquidity pool + + data ContractInstanceKey UniswapModel w s e where + OwnerKey :: ContractInstanceKey UniswapModel (Last (Either Text.Text Uniswap)) EmptySchema ContractError + SetupKey :: ContractInstanceKey UniswapModel (Maybe (Semigroup.Last Currency.OneShotCurrency)) Currency.CurrencySchema Currency.CurrencyError + WalletKey :: Wallet -> ContractInstanceKey UniswapModel (Last (Either Text.Text UserContractState)) UniswapUserSchema Void + + initialInstances = [] + + instanceWallet OwnerKey = w1 + instanceWallet SetupKey = w1 + instanceWallet (WalletKey w) = w + + instanceContract s tokenSem key = case key of + OwnerKey -> ownerEndpoint + SetupKey -> setupTokens + WalletKey _ -> toContract . userEndpoints . Uniswap . Coin . tokenSem . fromJust . view (contractState . uniswapToken) $ s + + initialState = UniswapModel Nothing mempty mempty mempty + + arbitraryAction s = + frequency $ [ (1, pure Start) + , (1, pure SetupTokens) ] ++ + [ (3, createPool) | not . null $ s ^. contractState . exchangeableTokens ] ++ + [ (10, gen) | gen <- [createPool, add, swap, remove, close] + , not . null $ s ^. contractState . exchangeableTokens + , not . null $ s ^. contractState . pools ] + where + createPool = do + w <- elements $ wallets \\ [w1] + t1 <- elements $ s ^. contractState . exchangeableTokens . to Set.toList + t2 <- elements $ s ^. contractState . exchangeableTokens . to (Set.delete t1) . to Set.toList + a1 <- choose (1, 100) + a2 <- choose (1, 100) + return $ CreatePool w (getAToken t1 t2) a1 (getBToken t1 t2) a2 + + add = do + w <- elements $ wallets \\ [w1] + PoolIndex t1 t2 <- elements $ s ^. contractState . pools . to Map.keys + a1 <- choose (1, 100) + a2 <- choose (1, 100) + return $ AddLiquidity w (getAToken t1 t2) a1 (getBToken t1 t2) a2 + + swap = do + PoolIndex t1 t2 <- elements $ s ^. contractState . pools . to Map.keys + w <- elements $ s ^. contractState . pools . at (poolIndex t1 t2) . to fromJust . liquidities . to Map.keys + a <- choose (1, 100) + (tA, tB) <- elements [(t1, t2), (t2, t1)] + return $ PerformSwap w tA tB a + + remove = do + idx@(PoolIndex t1 t2) <- elements $ s ^. contractState . pools . to Map.keys + w <- elements . fold $ s ^? contractState . pools . at idx . _Just . liquidities . to (Map.filter (0<)) . to Map.keys + a <- choose (1, sum $ s ^? contractState . pools . at idx . _Just . liquidities . at w . _Just . to unAmount) + return $ RemoveLiquidity w (getAToken t1 t2) (getBToken t1 t2) a + + close = do + w <- elements $ wallets \\ [w1] + PoolIndex t1 t2 <- elements $ s ^. contractState . pools . to Map.keys + return $ ClosePool w (getAToken t1 t2) (getBToken t1 t2) + + startInstances s act = case act of + Start -> [ Key OwnerKey ] + SetupTokens -> [ Key SetupKey ] + _ -> [ Key . WalletKey . walletOf $ act + | walletOf act `notElem` s ^. contractState . startedUserCode ] + + precondition s Start = not $ hasUniswapToken s + precondition _ SetupTokens = True + precondition s (CreatePool _ t1 a1 t2 a2) = hasUniswapToken s + && not (hasOpenPool s t1 t2) + && t1 `elem` s ^. contractState . exchangeableTokens + && t2 `elem` s ^. contractState . exchangeableTokens + && t1 /= t2 + && 0 < a1 + && 0 < a2 + precondition s (AddLiquidity _ t1 a1 t2 a2) = hasOpenPool s t1 t2 + && t1 /= t2 + && 0 < a1 + && 0 < a2 + precondition s (PerformSwap _ t1 t2 a) = hasOpenPool s t1 t2 + && t1 /= t2 + && 0 < a + precondition s (RemoveLiquidity w t1 t2 a) = hasOpenPool s t1 t2 + && t1 /= t2 + && Amount a <= liquidityOf s w t1 t2 + && Amount a < totalLiquidity s t1 t2 + && 0 < a + precondition s (ClosePool w t1 t2) = hasOpenPool s t1 t2 + && t1 /= t2 + && liquidityOf s w t1 t2 == totalLiquidity s t1 t2 + + nextState act = case act of + SetupTokens -> do + -- Give 1000000 A, B, C, and D token to w1, w2, w3, w4 + -- The tokens will be given to each wallet in a UTxO that needs + -- to have minAdaTxOut + withdraw w1 $ Ada.toValue ((fromInteger . toInteger . length $ wallets) * Ledger.minAdaTxOut) + -- Create the tokens + ts <- forM tokenNames $ \t -> do + tok <- createToken t + mint (symAssetClassValue tok (toInteger $ length wallets * 1000000)) + return tok + -- Give the tokens to the wallets + forM_ wallets $ \ w -> do + deposit w $ Ada.toValue Ledger.minAdaTxOut + deposit w $ mconcat [ symAssetClassValue t 1000000 | t <- ts ] + exchangeableTokens %= (Set.fromList ts <>) + wait 20 + + Start -> do + -- Create the uniswap token + us <- createToken "Uniswap" + uniswapToken .= Just us + -- Pay to the UTxO for the uniswap factory + withdraw w1 (Ada.toValue Ledger.minAdaTxOut) + wait 10 + + CreatePool w t1 a1 t2 a2 -> do + startedUserCode %= Set.insert w + -- Create a new liquidity token unless we + -- have already created the token in a previous + -- version of this pool + mp <- use $ pools . at (poolIndex t1 t2) + ltok <- case mp of + Nothing -> createToken "Liquidity" + Just p -> pure $ p ^. liquidityToken + -- Compute the amount of liquidity and token + let (tokAAmount, tokBAmount) = mkAmounts t1 t2 a1 a2 + liq = calculateInitialLiquidity tokAAmount tokBAmount + when (liq > 0) $ do + -- Create the pool + pools %= Map.insert (poolIndex t1 t2) (PoolModel tokAAmount tokBAmount (Map.singleton w liq) ltok) + -- Give `w` the liquidity tokens + let liqVal = symAssetClassValue ltok (unAmount liq) + deposit w liqVal + mint liqVal + -- Pay to the pool + withdraw w $ Ada.toValue Ledger.minAdaTxOut + withdraw w $ symAssetClassValue t1 a1 + <> symAssetClassValue t2 a2 + wait 5 + + AddLiquidity w t1 a1 t2 a2 -> do + startedUserCode %= Set.insert w + p <- use $ pools . at (poolIndex t1 t2) . to fromJust + -- Compute the amount of liqiudity token we get + let (deltaA, deltaB) = mkAmounts t1 t2 a1 a2 + deltaL = calculateAdditionalLiquidity (p ^. coinAAmount) + (p ^. coinBAmount) + (p ^. liquidities . to sum) + deltaA + deltaB + when (deltaL > 0) $ do + -- Update the pool with the new token and the new liquidity + let p' = p + & liquidities . at w %~ Just . (+deltaL) . sum + & coinAAmount +~ deltaA + & coinBAmount +~ deltaB + pools . at (poolIndex t1 t2) .= Just p' + -- Give the tokens to the pool + withdraw w $ symAssetClassValue t1 a1 <> symAssetClassValue t2 a2 + -- Create liquidity token and give it to `w` + let liqVal = symAssetClassValue (p ^. liquidityToken) (unAmount deltaL) + mint liqVal + deposit w liqVal + wait 5 + + PerformSwap w t1 t2 a -> do + startedUserCode %= Set.insert w + p <- use $ pools . at (poolIndex t1 t2) . to fromJust + let oldA = p ^. coinAAmount + oldB = p ^. coinBAmount + -- Depending on whether t1 < t2 + -- we are either swapping A-token for B-token + -- or the other way around + (a', p', lens) = if t1 < t2 + then let a' = findSwapA oldA oldB (Amount a) + p' = p & coinAAmount +~ Amount a + & coinBAmount -~ Amount a' + in (a', p', coinBAmount . to unAmount) + else let a' = findSwapB oldA oldB (Amount a) + p' = p & coinBAmount +~ Amount a + & coinAAmount -~ Amount a' + in (a', p', coinAAmount . to unAmount) + when (0 < a' && a' < p ^. lens) $ do + -- Swap the coins + withdraw w $ symAssetClassValue t1 a + deposit w $ symAssetClassValue t2 a' + -- Update the pool + pools . at (poolIndex t1 t2) .= Just p' + wait 5 + + RemoveLiquidity w t1 t2 a -> do + startedUserCode %= Set.insert w + -- Update the pool + p <- use $ pools . at (poolIndex t1 t2) . to fromJust + let inA = p ^. coinAAmount + inB = p ^. coinBAmount + liquidity = sum $ p ^. liquidities + (outA, outB) = calculateRemoval inA inB liquidity (Amount a) + p' = p + & coinAAmount .~ outA + & coinBAmount .~ outB + & liquidities . at w . _Just -~ Amount a + pools . at (poolIndex t1 t2) .= Just p' + -- Take the requisite amount of coin out of the contract + deposit w $ symAssetClassValue (getAToken t1 t2) (unAmount $ inA - outA) + <> symAssetClassValue (getBToken t1 t2) (unAmount $ inB - outB) + -- Burn the liquidity tokens + let liqVal = symAssetClassValue (p ^. liquidityToken) a + withdraw w liqVal + mint $ inv liqVal + wait 5 + + ClosePool w t1 t2 -> do + startedUserCode %= Set.insert w + p <- use $ pools . at (poolIndex t1 t2) . to fromJust + -- Reset the pool + let p' = p + & coinAAmount .~ 0 + & coinBAmount .~ 0 + & liquidities .~ Map.empty + pools . at (poolIndex t1 t2) .= Just p' + -- Take the rest of the money out of the contract + deposit w $ symAssetClassValue (getAToken t1 t2) (p ^. coinAAmount . to unAmount) + <> symAssetClassValue (getBToken t1 t2) (p ^. coinBAmount . to unAmount) + let liqVal = symAssetClassValue (p ^. liquidityToken) (p ^. liquidities . at w . to fromJust . to unAmount) + -- Burn the remaining liquidity tokens + withdraw w liqVal + mint $ inv liqVal + -- Return the 2 ada at the script to the wallet + deposit w $ Ada.toValue Ledger.minAdaTxOut + wait 5 + + perform h tokenSem s act = case act of + SetupTokens -> do + delay 20 + Trace.observableState (h SetupKey) >>= \case + Just (Semigroup.Last cur) -> sequence_ [ registerToken tn (Value.assetClass (Currency.currencySymbol cur) $ fromString tn) | tn <- ["A", "B", "C", "D"]] + _ -> Trace.throwError $ GenericError "failed to create currency" + + Start -> do + delay 5 + Trace.observableState (h OwnerKey) >>= \case + Last (Just (Right (Uniswap (Coin v)))) -> registerToken "Uniswap" v + _ -> Trace.throwError $ GenericError "initialisation failed" + + CreatePool w t1 a1 t2 a2 -> do + let us = s ^. contractState . uniswapToken . to fromJust + c1 = Coin (tokenSem $ getAToken t1 t2) + c2 = Coin (tokenSem $ getBToken t1 t2) + Coin ac = liquidityCoin (fst . Value.unAssetClass . tokenSem $ us) c1 c2 + Trace.callEndpoint @"create" (h (WalletKey w)) $ CreateParams c1 c2 (Amount a1) (Amount a2) + delay 5 + when (not $ hasPool s t1 t2) $ do + registerToken "Liquidity" ac + + AddLiquidity w t1 a1 t2 a2 -> do + let c1 = Coin (tokenSem $ getAToken t1 t2) + c2 = Coin (tokenSem $ getBToken t1 t2) + Trace.callEndpoint @"add" (h (WalletKey w)) $ AddParams c1 c2 (Amount a1) (Amount a2) + delay 5 + + PerformSwap w t1 t2 a -> do + let c1 = Coin (tokenSem t1) + c2 = Coin (tokenSem t2) + Trace.callEndpoint @"swap" (h (WalletKey w)) $ SwapParams c1 c2 (Amount a) 0 + delay 5 + + RemoveLiquidity w t1 t2 a -> do + let c1 = Coin (tokenSem $ getAToken t1 t2) + c2 = Coin (tokenSem $ getBToken t1 t2) + Trace.callEndpoint @"remove" (h (WalletKey w)) $ RemoveParams c1 c2 (Amount a) + delay 5 + + ClosePool w t1 t2 -> do + let c1 = Coin (tokenSem $ getAToken t1 t2) + c2 = Coin (tokenSem $ getBToken t1 t2) + Trace.callEndpoint @"close" (h (WalletKey w)) $ CloseParams c1 c2 + delay 5 + + shrinkAction _ a = case a of + CreatePool w t1 a1 t2 a2 -> [ CreatePool w t1 a1' t2 a2' | (a1', a2') <- shrink (a1, a2), a1' >= 0, a2' >= 0 ] + AddLiquidity w t1 a1 t2 a2 -> [ AddLiquidity w t1 a1' t2 a2' | (a1', a2') <- shrink (a1, a2), a1' >= 0, a2' >= 0 ] + RemoveLiquidity w t1 t2 a -> [ RemoveLiquidity w t1 t2 a' | a' <- shrink a, a' >= 0 ] + PerformSwap w t1 t2 a -> [ PerformSwap w t1 t2 a' | a' <- shrink a, a' >= 0 ] + _ -> [] + +-- This doesn't hold +prop_liquidityValue :: Property +prop_liquidityValue = forAllDL liquidityValue (const True) + where + liquidityValue :: DL UniswapModel () + liquidityValue = do + anyActions_ + pools <- viewContractState pools + forM_ (Map.filter (view open) pools) $ \ p -> do + let cond = calculateRemoval (p ^. coinAAmount) (p ^. coinBAmount) (p ^. liquidities . to sum) (Amount 1) + /= (p ^. coinAAmount, p ^. coinBAmount) + assert ("Pool\n " ++ show p ++ "\nforgets single liquidities") cond + +-- This doesn't work +noLockProof :: NoLockedFundsProof UniswapModel +noLockProof = NoLockedFundsProof{ + nlfpMainStrategy = mainStrat, + nlfpWalletStrategy = walletStrat } + where + mainStrat = do + pools <- viewContractState pools + forM_ (Map.toList pools) $ \ (PoolIndex t1 t2, p) -> do + let liqs = Map.toList . Map.filter (>0) $ p ^. liquidities + forM_ (take (length liqs - 1) liqs) $ \ (w, l) -> + action $ RemoveLiquidity w t1 t2 (unAmount l) + when (not . null $ liqs) $ do + action $ ClosePool (fst . last $ liqs) t1 t2 + + walletStrat w = do + pools <- viewContractState pools + forM_ (Map.toList pools) $ \ (PoolIndex t1 t2, p) -> do + let liqs = p ^. liquidities . to (Map.filter (>0)) + when (w `Map.member` liqs) $ do + if Map.keys liqs == [w] + 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 + +check_propUniswapWithCoverage :: IO () +check_propUniswapWithCoverage = void $ + quickCheckWithCoverage (set endpointCoverageReq epReqs $ set coverageIndex covIdx $ defaultCoverageOptions) $ \covopts -> + withMaxSuccess 1000 $ propRunActionsWithOptions @UniswapModel defaultCheckOptionsContractModel covopts (const (pure True)) + where + epReqs t ep + | t == Trace.walletInstanceTag w1 = 0 + | ep == "create" = 20 + | ep == "swap" = 15 + | ep == "close" = 0.5 + | ep == "remove" = 15 + | ep == "add" = 20 + | otherwise = 0 + +prop_Whitelist :: Actions UniswapModel -> Property +prop_Whitelist = checkErrorWhitelist defaultWhitelist tests :: TestTree tests = testGroup "uniswap" [ @@ -17,4 +523,5 @@ tests = testGroup "uniswap" [ "setupTokens contract should be still running" .&&. assertNoFailedTransactions) Uniswap.uniswapTrace + , testProperty "prop_Uniswap" $ withMaxSuccess 20 prop_Uniswap ] diff --git a/plutus-use-cases/test/Spec/Vesting.hs b/plutus-use-cases/test/Spec/Vesting.hs index c7cf398e32..e2cdf37e8c 100644 --- a/plutus-use-cases/test/Spec/Vesting.hs +++ b/plutus-use-cases/test/Spec/Vesting.hs @@ -85,9 +85,13 @@ instance ContractModel VestingModel where , _t1Amount = vestingTrancheAmount (vestingTranche1 params) , _t2Amount = vestingTrancheAmount (vestingTranche2 params) } - initialHandleSpecs = [ ContractInstanceSpec (WalletKey w) w (vestingContract params) | w <- [w1, w2, w3] ] + initialInstances = Key . WalletKey <$> [w1, w2, w3] - perform handle _ cmd = case cmd of + instanceWallet (WalletKey w) = w + + instanceContract _ _ WalletKey{} = vestingContract params + + perform handle _ _ cmd = case cmd of Vest w -> do callEndpoint @"vest funds" (handle $ WalletKey w) () delay 1 @@ -103,8 +107,8 @@ instance ContractModel VestingModel where let amount = vestingTrancheAmount (vestingTranche1 params) <> vestingTrancheAmount (vestingTranche2 params) withdraw w amount - vestedAmount $~ (<> amount) - vested $~ (w:) + vestedAmount %= (<> amount) + vested %= (w:) wait 1 -- Retrieve `v` value as long as that leaves enough value to satisfy @@ -120,7 +124,7 @@ instance ContractModel VestingModel where && Ada.fromValue v >= Ledger.minAdaTxOut && (Ada.fromValue newAmount == 0 || Ada.fromValue newAmount >= Ledger.minAdaTxOut)) $ do deposit w v - vestedAmount $= newAmount + vestedAmount .= newAmount wait 2 nextState (WaitUntil s) = do @@ -213,7 +217,7 @@ noLockProof = NoLockedFundsProof{ | otherwise = return () prop_CheckNoLockedFundsProof :: Property -prop_CheckNoLockedFundsProof = checkNoLockedFundsProof defaultCheckOptions noLockProof +prop_CheckNoLockedFundsProof = checkNoLockedFundsProof defaultCheckOptionsContractModel noLockProof -- Tests @@ -283,8 +287,3 @@ expectedError = maxPayment = Ada.adaValueOf 20 mustRemainLocked = Ada.adaValueOf 40 in InsufficientFundsError payment maxPayment mustRemainLocked - - --- Util -delay :: Integer -> Trace.EmulatorTraceNoStartContract () -delay n = void $ Trace.waitNSlots $ fromIntegral n diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs index 480cf18629..f4e4628f54 100644 --- a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs +++ b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic.hs @@ -13,8 +13,8 @@ module Test.QuickCheck.DynamicLogic , DynLogicModel(..), DynLogicTest(..), TestStep(..) , ignore, passTest, afterAny, after, (|||), forAllQ, weight, toStop , done, errorDL, monitorDL, always - , forAllScripts, withDLScript, withDLScriptPrefix, forAllMappedScripts - , propPruningGeneratedScriptIsNoop + , forAllScripts, forAllScripts_, withDLScript, withDLScriptPrefix, forAllMappedScripts, forAllMappedScripts_ + , forAllUniqueScripts, propPruningGeneratedScriptIsNoop ) where import Data.List @@ -22,7 +22,7 @@ import Data.Typeable import Control.Applicative -import Test.QuickCheck +import Test.QuickCheck hiding (generate) import Test.QuickCheck.DynamicLogic.CanGenerate import Test.QuickCheck.DynamicLogic.Quantify @@ -113,7 +113,6 @@ instance StateModel s => Show (TestStep s) where show (Do step) = "Do $ "++show step show (Witness a) = "Witness ("++show a++" :: "++show (typeOf a)++")" - instance StateModel s => Show (DynLogicTest s) where show (BadPrecondition as bads s) = unlines $ ["BadPrecondition"] ++ @@ -143,12 +142,24 @@ class StateModel s => DynLogicModel s where restricted :: Action s a -> Bool restricted _ = False +forAllUniqueScripts :: (DynLogicModel s, Testable a) => + Int -> s -> DynLogic s -> (Actions s -> a) -> Property +forAllUniqueScripts n s d k = case generate chooseUniqueNextStep d n s 500 [] of + Nothing -> counterexample "Generating Non-unique script in forAllUniqueScripts" False + Just test -> validDLTest d test .&&. (applyMonitoring d test . property $ k (scriptFromDL test)) + forAllScripts :: (DynLogicModel s, Testable a) => DynLogic s -> (Actions s -> a) -> Property forAllScripts d k = forAllShrink (sized $ generateDLTest d) (shrinkDLTest d) $ withDLScript d k +forAllScripts_ :: (DynLogicModel s, Testable a) => + DynLogic s -> (Actions s -> a) -> Property +forAllScripts_ d k = + forAll (sized $ generateDLTest d) $ + withDLScript d k + forAllMappedScripts :: (DynLogicModel s, Testable a, Show rep) => (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> DynLogic s -> (Actions s -> a) -> Property @@ -156,6 +167,13 @@ forAllMappedScripts to from d k = forAllShrink (sized $ (from<$>) . generateDLTest d) ((from<$>) . shrinkDLTest d . to) $ withDLScript d k . to +forAllMappedScripts_ :: + (DynLogicModel s, Testable a, Show rep) => + (rep -> DynLogicTest s) -> (DynLogicTest s -> rep) -> DynLogic s -> (Actions s -> a) -> Property +forAllMappedScripts_ to from d k = + forAll (sized $ (from<$>) . generateDLTest d) $ + withDLScript d k . to + withDLScript :: (DynLogicModel s, Testable a) => DynLogic s -> (Actions s -> a) -> DynLogicTest s -> Property withDLScript d k test = validDLTest d test .&&. (applyMonitoring d test . property $ k (scriptFromDL test)) @@ -167,28 +185,43 @@ withDLScriptPrefix d k test = test' = unfailDLTest d test generateDLTest :: DynLogicModel s => DynLogic s -> Int -> Gen (DynLogicTest s) -generateDLTest d size = generate d 0 (initialStateFor d) [] - where - generate d n s as = - case badActions d s of - [] -> - if n > sizeLimit size then - return $ Looping (reverse as) - else do - let preferred = if n > size then stopping d else noStopping d - useStep StoppingStep _ = return $ DLScript (reverse as) - useStep (Stepping (Do (var := act)) d') _ = - generate d' - (n+1) - (nextState s act var) - (Do (var := act):as) - useStep (Stepping (Witness a) d') _ = - generate d' n s (Witness a:as) - useStep NoStep alt = alt - foldr (\ step k -> do try <- chooseNextStep s n step; useStep try k) - (return $ Stuck (reverse as) s) - [preferred, noAny preferred, d, noAny d] - bs -> return $ BadPrecondition (reverse as) bs s +generateDLTest d size = generate chooseNextStep d 0 (initialStateFor d) size [] + +generate :: (Monad m, DynLogicModel s) + => (s -> Int -> DynLogic s -> m (NextStep s)) + -> DynLogic s + -> Int + -> s + -> Int + -> [TestStep s] + -> m (DynLogicTest s) +generate chooseNextStepFun d n s size as = + case badActions d s of + [] -> + if n > sizeLimit size then + return $ Looping (reverse as) + else do + let preferred = if n > size then stopping d else noStopping d + useStep StoppingStep _ = return $ DLScript (reverse as) + useStep (Stepping (Do (var := act)) d') _ = + generate chooseNextStepFun + d' + (n+1) + (nextState s act var) + size + (Do (var := act):as) + useStep (Stepping (Witness a) d') _ = + generate chooseNextStepFun + d' + n + s + size + (Witness a:as) + useStep NoStep alt = alt + foldr (\ step k -> do try <- chooseNextStepFun s n step; useStep try k) + (return $ Stuck (reverse as) s) + [preferred, noAny preferred, d, noAny d] + bs -> return $ BadPrecondition (reverse as) bs s sizeLimit :: Int -> Int sizeLimit size = 2 * size + 20 @@ -232,7 +265,7 @@ noAny (Monitor f d) = Monitor f (noAny d) nextSteps :: DynLogic s -> [(Double, DynLogic s)] nextSteps EmptySpec = [] nextSteps Stop = [(1, Stop)] -nextSteps (After act k)=[(1, After act k)] +nextSteps (After act k) = [(1, After act k)] nextSteps (AfterAny k) = [(1, AfterAny k)] nextSteps (Alt _ d d') = nextSteps d ++ nextSteps d' nextSteps (Stopping d) = nextSteps d @@ -281,6 +314,15 @@ chooseNextStep s n d = Weight{} -> error "chooseNextStep: Weight" Monitor{} -> error "chooseNextStep: Monitor" +chooseUniqueNextStep :: (MonadFail m, DynLogicModel s) => s -> Int -> DynLogic s -> m (NextStep s) +chooseUniqueNextStep s n d = + case snd <$> nextSteps d of + [] -> return NoStep + [EmptySpec] -> return NoStep + [Stop] -> return StoppingStep + [After (Some a) k] -> return $ Stepping (Do $ Var n := a) (k (nextState s a (Var n))) + _ -> fail "chooseUniqueNextStep: non-unique action in DynLogic" + keepTryingUntil :: Int -> Gen a -> (a -> Bool) -> Gen (Maybe a) keepTryingUntil 0 _ _ = return Nothing keepTryingUntil n g p = do @@ -288,6 +330,7 @@ keepTryingUntil n g p = do if p x then return $ Just x else scale (+1) $ keepTryingUntil (n-1) g p +-- TODO: Add shrink state to this following what we do with actions shrinkDLTest :: DynLogicModel s => DynLogic s -> DynLogicTest s -> [DynLogicTest s] shrinkDLTest _ (Looping _) = [] shrinkDLTest d tc = @@ -433,9 +476,14 @@ stuck (Weight w d) s = w < never || stuck d s stuck (ForAll _ _) _ = False stuck (Monitor _ d)s = stuck d s -validDLTest :: DynLogic s -> DynLogicTest s -> Bool -validDLTest _ (DLScript _) = True -validDLTest _ _ = False +validDLTest :: StateModel s => DynLogic s -> DynLogicTest s -> Property +validDLTest _ (DLScript _) = property True +validDLTest _ (Stuck as _) = counterexample ("Stuck\n" ++ (unlines . map (" "++) . lines $ show as)) False +validDLTest _ (Looping as) = counterexample ("Looping\n" ++ (unlines . map (" "++) . lines $ show as)) False +validDLTest _ (BadPrecondition as bads s) = counterexample ("BadPrecondition\n" ++ show as ++ "\n" ++ unlines (showBad <$> bads)) $ False + where + showBad (Error s) = s + showBad a = show a scriptFromDL :: DynLogicTest s -> Actions s scriptFromDL (DLScript s) = Actions [a | Do a <- s] diff --git a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Monad.hs b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Monad.hs index 624e8f1a02..8261c1f7cf 100644 --- a/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Monad.hs +++ b/quickcheck-dynamic/src/Test/QuickCheck/DynamicLogic/Monad.hs @@ -1,4 +1,5 @@ {-# LANGUAGE FlexibleContexts #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} module Test.QuickCheck.DynamicLogic.Monad ( DL , action @@ -13,7 +14,10 @@ module Test.QuickCheck.DynamicLogic.Monad , monitorDL , forAllQ , forAllDL + , forAllDL_ , forAllMappedDL + , forAllMappedDL_ + , forAllUniqueDL , withDLTest , DL.DynLogic , DL.DynLogicModel(..) @@ -102,10 +106,18 @@ instance MonadFail (DL s) where runDL :: s -> DL s () -> DL.DynLogic s runDL s dl = unDL dl s $ \ _ _ -> DL.passTest +forAllUniqueDL :: (DL.DynLogicModel s, Testable a) => + Int -> s -> DL s () -> (Actions s -> a) -> Property +forAllUniqueDL nextVar initialState d prop = DL.forAllUniqueScripts nextVar initialState (runDL initialState d) prop + forAllDL :: (DL.DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> Property forAllDL d prop = DL.forAllScripts (runDL initialState d) prop +forAllDL_ :: (DL.DynLogicModel s, Testable a) => + DL s () -> (Actions s -> a) -> Property +forAllDL_ d prop = DL.forAllScripts_ (runDL initialState d) prop + forAllMappedDL :: (DL.DynLogicModel s, Testable a, Show rep) => (rep -> DL.DynLogicTest s) -> (DL.DynLogicTest s -> rep) -> (Actions s -> srep) @@ -113,6 +125,13 @@ forAllMappedDL :: forAllMappedDL to from fromScript d prop = DL.forAllMappedScripts to from (runDL initialState d) (prop . fromScript) +forAllMappedDL_ :: + (DL.DynLogicModel s, Testable a, Show rep) => + (rep -> DL.DynLogicTest s) -> (DL.DynLogicTest s -> rep) -> (Actions s -> srep) + -> DL s () -> (srep -> a) -> Property +forAllMappedDL_ to from fromScript d prop = + DL.forAllMappedScripts_ to from (runDL initialState d) (prop . fromScript) + withDLTest :: (DL.DynLogicModel s, Testable a) => DL s () -> (Actions s -> a) -> DL.DynLogicTest s -> Property withDLTest d prop test = DL.withDLScriptPrefix (runDL initialState d) prop test diff --git a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs index 838d637999..b54673b79b 100644 --- a/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs +++ b/quickcheck-dynamic/src/Test/QuickCheck/StateModel.hs @@ -4,12 +4,14 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} module Test.QuickCheck.StateModel( StateModel(..) @@ -17,14 +19,20 @@ module Test.QuickCheck.StateModel( , Step(..) , LookUp, Var(..) -- we export the constructors so that users can construct test cases , Actions(..) + , pattern Actions + , ShrinkState + , initialShrinkState + , EnvEntry(..) + , Env , stateAfter , runActions , runActionsInState + , lookUpVar ) where import Data.Typeable -import Test.QuickCheck as QC +import Test.QuickCheck as QC hiding (ShrinkState) import Test.QuickCheck.Monadic class (forall a. Show (Action state a), @@ -98,14 +106,18 @@ instance Eq (Step state) where (Var i := act) == (Var j := act') = (i==j) && Some act == Some act' -newtype Actions state = Actions [Step state] +data Actions state = ActionsWithShrinkState ShrinkState [Step state] deriving Eq -instance Semigroup (Actions state) where - Actions as <> Actions as' = Actions (as <> as') +data ShrinkState = ShrinkState { lastShrinkIndex :: Int } deriving Eq -instance Monoid (Actions state) where - mempty = Actions [] +initialShrinkState :: ShrinkState +initialShrinkState = ShrinkState 0 + +{-# COMPLETE Actions #-} +pattern Actions :: [Step state] -> Actions state +pattern Actions as <- ActionsWithShrinkState _ as where + Actions as = ActionsWithShrinkState initialShrinkState as instance (forall a. Show (Action state a)) => Show (Actions state) where showsPrec d (Actions as) @@ -134,9 +146,11 @@ instance (Typeable state, StateModel state) => Arbitrary (Actions state) where Nothing -> return [])] - shrink (Actions as) = - map (Actions . prune . map fst) (shrinkList shrinker (withStates as)) + shrink (ActionsWithShrinkState s as) = + rotate (lastShrinkIndex s) $ zipWith mkActions [0..] (map fst <$> shrinkList shrinker (withStates as)) where shrinker ((Var i := act),s) = [((Var i := act'),s) | Some act' <- shrinkAction s act] + mkActions i as = ActionsWithShrinkState (ShrinkState i) (prune as) + rotate i as = let (hds, tls) = splitAt (max 0 (i-1)) as in tls ++ hds prune :: StateModel state => [Step state] -> [Step state] prune = loop initialState