diff --git a/doc/default.nix b/doc/default.nix index 3a278421a0..2347e214d7 100644 --- a/doc/default.nix +++ b/doc/default.nix @@ -1,7 +1,7 @@ { stdenv, lib, pythonPackages, sphinxcontrib-domaintools, sphinxcontrib-haddock, sphinx-markdown-tables, sphinxemoji, combined-haddock, ... }: stdenv.mkDerivation { name = "plutus-docs"; - src = lib.sourceFilesBySuffices ./. [ ".py" ".rst" ".hs" ".png" ".svg" ".bib" ".csv" ".css" ]; + src = lib.sourceFilesBySuffices ./. [ ".py" ".rst" ".hs" ".png" ".svg" ".bib" ".csv" ".css" ".html" ]; buildInputs = with pythonPackages; [ sphinx sphinx_rtd_theme diff --git a/doc/plutus-doc.cabal b/doc/plutus-doc.cabal index 7673ff7d5a..e44cd4ab2a 100644 --- a/doc/plutus-doc.cabal +++ b/doc/plutus-doc.cabal @@ -56,6 +56,13 @@ executable doc-doctests HandlingBlockchainEvents HelloWorldApp WriteScriptsTo + Escrow + Escrow2 + Escrow3 + Escrow4 + Escrow5 + Escrow6 + EscrowImpl build-depends: base >=4.9 && <5, template-haskell >=2.13.0.0, @@ -80,6 +87,8 @@ executable doc-doctests random -any, text -any, aeson -any, + tasty -any, + tasty-quickcheck -any if !(impl(ghcjs) || os(ghcjs)) build-depends: plutus-tx-plugin -any diff --git a/doc/plutus/tutorials/Auction.hs b/doc/plutus/tutorials/Auction.hs new file mode 100644 index 0000000000..232485325e --- /dev/null +++ b/doc/plutus/tutorials/Auction.hs @@ -0,0 +1,390 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NumericUnderscores #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +module Spec.Auction + ( tests + , options + , auctionTrace1 + , auctionTrace2 + , AuctionModel + , prop_Auction + , prop_FinishAuction + , prop_NoLockedFunds + , prop_NoLockedFundsFast + , prop_SanityCheckAssertions + , prop_Whitelist + , prop_CrashTolerance + , check_propAuctionWithCoverage + ) where + +import Control.Lens hiding (elements) +import Control.Monad (void, when) +import Control.Monad.Freer qualified as Freer +import Control.Monad.Freer.Error qualified as Freer +import Control.Monad.Freer.Extras.Log (LogLevel (..)) +import Data.Data +import Data.Default (Default (def)) +import Data.Monoid (Last (..)) + +import Ledger (Ada, Slot (..), Value) +import Ledger.Ada qualified as Ada +import Ledger.Generators (someTokenValue) +import Plutus.Contract hiding (currentSlot) +import Plutus.Contract.Test hiding (not) +import Streaming.Prelude qualified as S +import Wallet.Emulator.Folds qualified as Folds +import Wallet.Emulator.Stream qualified as Stream + +import Ledger qualified +import Ledger.TimeSlot (SlotConfig) +import Ledger.TimeSlot qualified as TimeSlot +import Plutus.Contract.Test.ContractModel +import Plutus.Contract.Test.ContractModel.CrashTolerance +import Plutus.Contract.Test.ContractModel.Symbolics (toSymValue) +import Plutus.Contract.Test.Coverage +import Plutus.Contracts.Auction hiding (Bid) +import Plutus.Trace.Emulator qualified as Trace +import PlutusTx.Monoid (inv) + +import Test.QuickCheck hiding ((.&&.)) +import Test.Tasty +import Test.Tasty.QuickCheck (testProperty) + +slotCfg :: SlotConfig +slotCfg = def + +params :: AuctionParams +params = + AuctionParams + { apOwner = mockWalletPaymentPubKeyHash w1 + , apAsset = theToken + , apEndTime = TimeSlot.scSlotZeroTime slotCfg + 100000 + } + +{- START options -} +-- | The token that we are auctioning off. +theToken :: Value +theToken = + -- This currency is created by the initial transaction. + someTokenValue "token" 1 + +-- | 'CheckOptions' that includes 'theToken' in the initial distribution of Wallet 1. +options :: CheckOptions +options = defaultCheckOptionsContractModel + & changeInitialWalletValue w1 ((<>) theToken) +{- END options -} +seller :: Contract AuctionOutput SellerSchema AuctionError () +seller = auctionSeller (apAsset params) (apEndTime params) + +buyer :: ThreadToken -> Contract AuctionOutput BuyerSchema AuctionError () +buyer cur = auctionBuyer cur params + +trace1WinningBid :: Ada +trace1WinningBid = Ada.adaOf 50 + +auctionTrace1 :: Trace.EmulatorTrace () +auctionTrace1 = do + sellerHdl <- Trace.activateContractWallet w1 seller + void $ Trace.waitNSlots 3 + currency <- extractAssetClass sellerHdl + hdl2 <- Trace.activateContractWallet w2 (buyer currency) + void $ Trace.waitNSlots 1 + Trace.callEndpoint @"bid" hdl2 trace1WinningBid + void $ Trace.waitUntilTime $ apEndTime params + void $ Trace.waitNSlots 1 + +trace2WinningBid :: Ada +trace2WinningBid = Ada.adaOf 70 + +extractAssetClass :: Trace.ContractHandle AuctionOutput SellerSchema AuctionError -> Trace.EmulatorTrace ThreadToken +extractAssetClass handle = do + t <- auctionThreadToken <$> Trace.observableState handle + case t of + Last (Just currency) -> pure currency + _ -> Trace.throwError (Trace.GenericError "currency not found") + +auctionTrace2 :: Trace.EmulatorTrace () +auctionTrace2 = do + sellerHdl <- Trace.activateContractWallet w1 seller + void $ Trace.waitNSlots 3 + currency <- extractAssetClass sellerHdl + hdl2 <- Trace.activateContractWallet w2 (buyer currency) + hdl3 <- Trace.activateContractWallet w3 (buyer currency) + void $ Trace.waitNSlots 1 + Trace.callEndpoint @"bid" hdl2 (Ada.adaOf 50) + void $ Trace.waitNSlots 15 + Trace.callEndpoint @"bid" hdl3 (Ada.adaOf 60) + void $ Trace.waitNSlots 35 + Trace.callEndpoint @"bid" hdl2 trace2WinningBid + void $ Trace.waitUntilTime $ apEndTime params + void $ Trace.waitNSlots 1 + +trace1FinalState :: AuctionOutput +trace1FinalState = + AuctionOutput + { auctionState = Last $ Just $ Finished $ HighestBid + { highestBid = trace1WinningBid + , highestBidder = mockWalletPaymentPubKeyHash w2 + } + , auctionThreadToken = Last $ Just threadToken + } + +trace2FinalState :: AuctionOutput +trace2FinalState = + AuctionOutput + { auctionState = Last $ Just $ Finished $ HighestBid + { highestBid = trace2WinningBid + , highestBidder = mockWalletPaymentPubKeyHash w2 + } + , auctionThreadToken = Last $ Just threadToken + } + +threadToken :: ThreadToken +threadToken = + let con = getThreadToken :: Contract AuctionOutput SellerSchema AuctionError ThreadToken + fld = Folds.instanceOutcome con (Trace.walletInstanceTag w1) + getOutcome (Folds.Done a) = a + getOutcome e = error $ "not finished: " <> show e + in + either (error . show) (getOutcome . S.fst') + $ Freer.run + $ Freer.runError @Folds.EmulatorFoldErr + $ Stream.foldEmulatorStreamM fld + $ Stream.takeUntilSlot 10 + $ Trace.runEmulatorStream (options ^. emulatorConfig) + $ do + void $ Trace.activateContractWallet w1 (void con) + Trace.waitNSlots 3 + +-- * QuickCheck model +{- START model -} +data AuctionModel = AuctionModel + { _currentBid :: Integer + , _winner :: Wallet + , _endSlot :: Slot + , _phase :: Phase + } deriving (Show, Eq, Data) + +data Phase = NotStarted | Bidding | AuctionOver + deriving (Eq, Show, Data) +{- END model -} +makeLenses 'AuctionModel + +deriving instance Eq (ContractInstanceKey AuctionModel w s e params) +deriving instance Show (ContractInstanceKey AuctionModel w s e params) + +instance ContractModel AuctionModel where + + data ContractInstanceKey AuctionModel w s e params where + SellerH :: ContractInstanceKey AuctionModel AuctionOutput SellerSchema AuctionError () + BuyerH :: Wallet -> ContractInstanceKey AuctionModel AuctionOutput BuyerSchema AuctionError () + +{- START Action -} + data Action AuctionModel = Init | Bid Wallet Integer + deriving (Eq, Show, Data) +{- END Action -} + + initialState = AuctionModel + { _currentBid = 0 + , _winner = w1 + , _endSlot = TimeSlot.posixTimeToEnclosingSlot def $ apEndTime params + , _phase = NotStarted + } + + initialInstances = [ StartContract (BuyerH w) () | w <- [w2, w3, w4] ] + + startInstances _ Init = [StartContract SellerH ()] + startInstances _ _ = [] + + instanceWallet SellerH = w1 + instanceWallet (BuyerH w) = w + + instanceContract _ SellerH _ = seller + instanceContract _ BuyerH{} _ = buyer threadToken + + arbitraryAction s + | p /= NotStarted = do + oneof [ Bid w <$> validBid + | w <- [w2, w3, w4] ] + | otherwise = pure $ Init + where + p = s ^. contractState . phase + b = s ^. contractState . currentBid + validBid = choose ((b+1) `max` Ada.getLovelace Ledger.minAdaTxOut, + b + Ada.getLovelace (Ada.adaOf 100)) +{- START precondition -} + precondition s Init = s ^. contractState . phase == NotStarted + precondition s (Bid w bid) = + -- In order to place a bid, we need to satisfy the constraint where + -- each tx output must have at least N Ada. + s ^. contractState . phase /= NotStarted && + bid >= Ada.getLovelace (Ledger.minAdaTxOut) && + bid > s ^. contractState . currentBid +{-END precondition -} +{- START nextReactiveState -} + nextReactiveState slot' = do + end <- viewContractState endSlot + p <- viewContractState phase + when (slot' >= end && p == Bidding) $ do + w <- viewContractState winner + bid <- viewContractState currentBid + phase .= AuctionOver + deposit w $ Ada.toValue Ledger.minAdaTxOut <> theToken + deposit w1 $ Ada.lovelaceValueOf bid +{- END nextReactiveState -} + + {- +{- START extendedNextReactiveState -} + nextReactiveState slot' = do + end <- viewContractState endSlot + p <- viewContractState phase + when (slot' >= end && p == Bidding) $ do + w <- viewContractState winner + bid <- viewContractState currentBid + phase .= AuctionOver + deposit w $ Ada.toValue Ledger.minAdaTxOut <> theToken + deposit w1 $ Ada.lovelaceValueOf bid + -- NEW!!! + w1change <- viewModelState $ balanceChange w1 -- since the start of the test + assertSpec ("w1 final balance is wrong:\n "++show w1change) $ + w1change == toSymValue (inv theToken <> Ada.lovelaceValueOf bid) || + w1change == mempty +{- END extendedNextReactiveState -} + -} + +{- START nextState -} + nextState cmd = do + case cmd of + Init -> do + phase .= Bidding + withdraw w1 $ Ada.toValue Ledger.minAdaTxOut <> theToken + wait 3 + Bid w bid -> do + currentPhase <- viewContractState phase + when (currentPhase == Bidding) $ do + current <- viewContractState currentBid + leader <- viewContractState winner + withdraw w $ Ada.lovelaceValueOf bid + deposit leader $ Ada.lovelaceValueOf current + currentBid .= bid + winner .= w + wait 2 +{- END nextState -} + + perform _ _ _ Init = delay 3 + perform handle _ _ (Bid w bid) = do + -- FIXME: You cannot bid in certain slots when the off-chain code is busy, so to make the + -- tests pass we send two identical bids in consecutive slots. The off-chain code is + -- never busy for more than one slot at a time so at least one of the bids is + -- guaranteed to go through. If both reaches the off-chain code the second will be + -- discarded since it's not higher than the current highest bid. + Trace.callEndpoint @"bid" (handle $ BuyerH w) (Ada.lovelaceOf bid) + delay 1 + Trace.callEndpoint @"bid" (handle $ BuyerH w) (Ada.lovelaceOf bid) + delay 1 + + shrinkAction _ Init = [] + shrinkAction _ (Bid w v) = [ Bid w v' | v' <- shrink v ] + +{- START prop_Auction -} +prop_Auction :: Actions AuctionModel -> Property +prop_Auction script = + propRunActionsWithOptions (set minLogLevel Info options) defaultCoverageOptions + (\ _ -> pure True) -- TODO: check termination + script +{- END prop_Auction -} + +{- START prop_FinishAuction -} +finishAuction :: DL AuctionModel () +finishAuction = do + anyActions_ + finishingStrategy + assertModel "Locked funds are not zero" (symIsZero . lockedValue) + +finishingStrategy :: DL AuctionModel () +finishingStrategy = do + slot <- viewModelState currentSlot + end <- viewContractState endSlot + when (slot < end) $ waitUntilDL end + +prop_FinishAuction :: Property +prop_FinishAuction = forAllDL finishAuction prop_Auction +{- END prop_FinishAuction -} +-- | This does not hold! The Payout transition is triggered by the sellers off-chain code, so if the +-- seller walks away the buyer will not get their token (unless going around the off-chain code +-- and building a Payout transaction manually). +{- START noLockProof -} +noLockProof :: NoLockedFundsProof AuctionModel +noLockProof = defaultNLFP + { nlfpMainStrategy = finishingStrategy + , nlfpWalletStrategy = const finishingStrategy } +{- END noLockProof -} + +prop_NoLockedFunds :: Property +prop_NoLockedFunds = checkNoLockedFundsProofWithOptions (set minLogLevel Critical options) noLockProof + +prop_NoLockedFundsFast :: Property +prop_NoLockedFundsFast = checkNoLockedFundsProofFast noLockProof + +prop_SanityCheckAssertions :: Actions AuctionModel -> Property +prop_SanityCheckAssertions = propSanityCheckAssertions + +prop_Whitelist :: Actions AuctionModel -> Property +prop_Whitelist = checkErrorWhitelist defaultWhitelist + +{- START crashTolerance -} +instance CrashTolerance AuctionModel where + available (Bid w _) alive = (Key $ BuyerH w) `elem` alive + available Init alive = True + + restartArguments _ BuyerH{} = () + restartArguments _ SellerH{} = () + +prop_CrashTolerance :: Actions (WithCrashTolerance AuctionModel) -> Property +prop_CrashTolerance = + propRunActionsWithOptions (set minLogLevel Critical options) defaultCoverageOptions + (\ _ -> pure True) +{- END crashTolerance -} + +check_propAuctionWithCoverage :: IO () +check_propAuctionWithCoverage = do + cr <- quickCheckWithCoverage (set coverageIndex covIdx $ defaultCoverageOptions) $ \covopts -> + withMaxSuccess 1000 $ + propRunActionsWithOptions @AuctionModel + (set minLogLevel Critical options) covopts (const (pure True)) + writeCoverageReport "Auction" covIdx cr + +tests :: TestTree +tests = + testGroup "auction" + [ checkPredicateOptions options "run an auction" + (assertDone seller (Trace.walletInstanceTag w1) (const True) "seller should be done" + .&&. assertDone (buyer threadToken) (Trace.walletInstanceTag w2) (const True) "buyer should be done" + .&&. assertAccumState (buyer threadToken) (Trace.walletInstanceTag w2) ((==) trace1FinalState ) "wallet 2 final state should be OK" + .&&. walletFundsChange w1 (Ada.toValue (-Ledger.minAdaTxOut) <> Ada.toValue trace1WinningBid <> inv theToken) + .&&. walletFundsChange w2 (Ada.toValue Ledger.minAdaTxOut <> inv (Ada.toValue trace1WinningBid) <> theToken)) + auctionTrace1 + , checkPredicateOptions options "run an auction with multiple bids" + (assertDone seller (Trace.walletInstanceTag w1) (const True) "seller should be done" + .&&. assertDone (buyer threadToken) (Trace.walletInstanceTag w2) (const True) "buyer should be done" + .&&. assertDone (buyer threadToken) (Trace.walletInstanceTag w3) (const True) "3rd party should be done" + .&&. assertAccumState (buyer threadToken) (Trace.walletInstanceTag w2) ((==) trace2FinalState) "wallet 2 final state should be OK" + .&&. assertAccumState (buyer threadToken) (Trace.walletInstanceTag w3) ((==) trace2FinalState) "wallet 3 final state should be OK" + .&&. walletFundsChange w1 (Ada.toValue (-Ledger.minAdaTxOut) <> Ada.toValue trace2WinningBid <> inv theToken) + .&&. walletFundsChange w2 (Ada.toValue Ledger.minAdaTxOut <> inv (Ada.toValue trace2WinningBid) <> theToken) + .&&. walletFundsChange w3 mempty) + auctionTrace2 + , testProperty "QuickCheck property" $ + withMaxSuccess 10 prop_FinishAuction + , testProperty "NLFP fails" $ + expectFailure $ noShrinking prop_NoLockedFunds + , testProperty "prop_Reactive" $ + withMaxSuccess 1000 (propSanityCheckReactive @AuctionModel) + ] diff --git a/doc/plutus/tutorials/Auction.html b/doc/plutus/tutorials/Auction.html new file mode 100644 index 0000000000..8c3252e833 --- /dev/null +++ b/doc/plutus/tutorials/Auction.html @@ -0,0 +1,47 @@ +
+ 124 auctionTransition + 125 :: AuctionParams + 126 -> State AuctionState + 127 -> AuctionInput + 128 -> Maybe (TxConstraints Void Void, State AuctionState) + 129 auctionTransition AuctionParams{apOwner, apAsset, apEndTime} State{stateData=oldStateData, stateValue=oldStateValue} input = + 130 case (oldStateData, input) of + 131 + 132 (Ongoing HighestBid{highestBid, highestBidder}, Bid{newBid, newBidder}) | newBid > highestBid -> -- if the new bid is higher, + 133 let constraints = if highestBid == 0 then mempty else + 134 Constraints.mustPayToPubKey highestBidder (Ada.toValue highestBid) -- we pay back the previous highest bid + 135 <> Constraints.mustValidateIn (Interval.to $ apEndTime - 1) -- but only if we haven't gone past 'apEndTime' + 136 newState = + 137 State + 138 { stateData = Ongoing HighestBid{highestBid = newBid, highestBidder = newBidder} + 139 , stateValue = Value.noAdaValue oldStateValue + 140 <> Ada.toValue (Ada.fromValue oldStateValue - highestBid) + 141 <> Ada.toValue newBid -- and lock the new bid in the script output + 142 } + 143 in Just (constraints, newState) + 144 + 145 (Ongoing h@HighestBid{highestBidder, highestBid}, Payout) -> + 146 let constraints = + 147 Constraints.mustValidateIn (Interval.from apEndTime) -- When the auction has ended, + 148 <> Constraints.mustPayToPubKey apOwner (Ada.toValue highestBid) -- the owner receives the payment + 149 <> Constraints.mustPayToPubKey highestBidder apAsset -- and the highest bidder the asset + 150 newState = State { stateData = Finished h, stateValue = mempty } + 151 in Just (constraints, newState) + 152 + 153 -- Any other combination of 'AuctionState' and 'AuctionInput' is disallowed. + 154 -- This rules out new bids that don't go over the current highest bid. + 155 _ -> Nothing + 156 + 157 + 158 {-# INLINABLE auctionStateMachine #-} + 159 auctionStateMachine :: (ThreadToken, AuctionParams) -> AuctionMachine + 160 auctionStateMachine (threadToken, auctionParams) = + 161 SM.mkStateMachine (Just threadToken) (auctionTransition auctionParams) isFinal + 162 where + 163 isFinal Finished{} = True + 164 isFinal _ = False + 165 + 166 {-# INLINABLE mkValidator #-} + 167 mkValidator :: (ThreadToken, AuctionParams) -> Scripts.ValidatorType AuctionMachine + 168 mkValidator = SM.mkValidator . auctionStateMachine +diff --git a/doc/plutus/tutorials/Escrow.hs b/doc/plutus/tutorials/Escrow.hs new file mode 100644 index 0000000000..66cb44c105 --- /dev/null +++ b/doc/plutus/tutorials/Escrow.hs @@ -0,0 +1,279 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} +module Escrow + ( tests + , prop_Escrow + , EscrowModel + ) where + +import Control.Lens hiding (both, elements) +import Control.Monad (void) +import Data.Data +import Data.Foldable +import Data.Map (Map) +import Data.Map qualified as Map + +import Ledger (minAdaTxOut) +import Ledger.Ada qualified as Ada +import Ledger.Typed.Scripts qualified as Scripts +import Ledger.Value +import Plutus.Contract hiding (currentSlot) +import Plutus.Contract.Test +import Plutus.Contract.Test.ContractModel + +import Plutus.Contracts.Tutorial.Escrow hiding (Action (..)) +import Plutus.Trace.Emulator qualified as Trace +import PlutusTx.Monoid (inv) + +import Test.QuickCheck as QC hiding ((.&&.)) +import Test.Tasty +import Test.Tasty.QuickCheck hiding ((.&&.)) + +{- START EscrowModel -} +data EscrowModel = EscrowModel { _contributions :: Map Wallet Value + , _targets :: Map Wallet Value + } deriving (Eq, Show, Data) + +makeLenses ''EscrowModel +{- END EscrowModel -} + +{- START ContractInstanceKeyDeriving :-} +deriving instance Eq (ContractInstanceKey EscrowModel w s e params) +deriving instance Show (ContractInstanceKey EscrowModel w s e params) +{- END ContractInstanceKeyDeriving -} +{- +{- START ContractModelInstance -} +instance ContractModel EscrowModel where ... +{- END ContractModelInstance -} +-} +instance ContractModel EscrowModel where +{- START ActionType -} + data Action EscrowModel = Pay Wallet Integer + | Redeem Wallet + deriving (Eq, Show, Data) +{- END ActionType -} + + -- | Refund Wallet + +{- START ContractInstanceKeyType -} + data ContractInstanceKey EscrowModel w s e params where + WalletKey :: Wallet -> ContractInstanceKey EscrowModel () EscrowSchema EscrowError () +{- END ContractInstanceKeyType -} + +{- START initialState -} + initialState = EscrowModel { _contributions = Map.empty + , _targets = Map.fromList [ (w1, Ada.adaValueOf 10) + , (w2, Ada.adaValueOf 20) + ] + } +{- END initialState -} + +{- +{- START testContract -} +testContract = selectList [ void $ payEp escrowParams + , void $ redeemEp escrowParams + ] >> testContract +{- END testContract -} +-} + +{- + +{- START ContractKeySemantics -} + initialInstances = [StartContract (WalletKey w) () | w <- testWallets] + + instanceWallet (WalletKey w) = w + + instanceContract _ WalletKey{} _ = testContract +{- END ContractKeySemantics -} + +-} + + instanceWallet (WalletKey w) = w + + instanceContract _ WalletKey{} _ = testContract + where + testContract = selectList [ void $ payEp escrowParams + , void $ redeemEp escrowParams + -- , void $ refundEp escrowParams + ] >> testContract +{- START initialInstances -} + initialInstances = [StartContract (WalletKey w) () | w <- testWallets] +{- END initialInstances -} +{- +{- START 0nextState -} + nextState a = case a of + Pay w v -> do + withdraw w (Ada.adaValueOf $ fromInteger v) + contributions %= Map.insertWith (<>) w (Ada.adaValueOf $ fromInteger v) + wait 1 + Redeem w -> do + targets <- viewContractState targets + sequence_ [ deposit w v | (w, v) <- Map.toList targets ] + contributions .= Map.empty + wait 1 +{- END 0nextState -} +-} +{- +{- START nextState1 -} + nextState a = case a of + Pay w v -> ... + Redeem w -> do + targets <- viewContractState targets + sequence_ [ deposit w v | (w, v) <- Map.toList targets ] + contribs <- viewContractState contributions -- NEW + let leftoverValue = fold contribs <> inv (fold targets) -- NEW + deposit w leftoverValue -- NEW + contributions .= Map.empty + wait 1 +{- END nextState1 -} +-} +{- START nextState -} + nextState a = case a of + Pay w v -> do + withdraw w (Ada.adaValueOf $ fromInteger v) + contributions %= Map.insertWith (<>) w (Ada.adaValueOf $ fromInteger v) + wait 1 + Redeem w -> do + targets <- viewContractState targets + contribs <- viewContractState contributions + sequence_ [ deposit w v | (w, v) <- Map.toList targets ] + let leftoverValue = fold contribs <> inv (fold targets) + deposit w leftoverValue + contributions .= Map.empty + wait 1 +{- END nextState -} +{- Refund w -> do + v <- viewContractState $ contributions . at w . to fold + contributions %= Map.delete w + deposit w v + wait 1 +-} + +{- +{- START precondition1 -} + precondition s a = case a of + Redeem _ -> (s ^. contractState . contributions . to fold) + `geq` + (s ^. contractState . targets . to fold) + _ -> True +{- END precondition1 -} +-} +{- +{- START precondition2 -} +precondition s a = case a of + Redeem _ -> (s ^. contractState . contributions . to fold) + `geq` + (s ^. contractState . targets . to fold) + Pay _ v -> Ada.adaValueOf (fromInteger v) `geq` Ada.toValue minAdaTxOut +{- END precondition2 -} +-} + precondition s a = case a of + Redeem _ -> (s ^. contractState . contributions . to fold) `geq` (s ^. contractState . targets . to fold) + --Redeem _ -> (s ^. contractState . contributions . to fold) == (s ^. contractState . targets . to fold) + --Refund w -> Nothing /= (s ^. contractState . contributions . at w) + Pay _ v -> Ada.adaValueOf (fromInteger v) `geq` Ada.toValue minAdaTxOut + +{- START perform -} + perform h _ _ a = case a of + Pay w v -> do + Trace.callEndpoint @"pay-escrow" (h $ WalletKey w) (Ada.adaValueOf $ fromInteger v) + delay 1 + Redeem w -> do + Trace.callEndpoint @"redeem-escrow" (h $ WalletKey w) () + delay 1 +{- END perform -} + +{- Refund w -> do + Trace.callEndpoint @"refund-escrow" (h $ WalletKey w) () + delay 1 +-} + +{- +{- START arbitraryAction1 -} + arbitraryAction _ = frequency $ [ (3, Pay <$> elements testWallets <*> choose (1, 30)) + , (1, Redeem <$> elements testWallets) ] +{- END arbitraryAction1 -} +-} + {- ++ + [ (1, Refund <$> elements (s ^. contractState . contributions . to Map.keys)) + | Prelude.not . null $ s ^. contractState . contributions . to Map.keys ] + -} + +{- START arbitraryAction2 -} + arbitraryAction s = frequency $ [ (3, Pay <$> elements testWallets <*> choose (1, 30)) ] ++ + [ (1, Redeem <$> elements testWallets) + | (s ^. contractState . contributions . to fold) -- NEW + `geq` -- NEW + (s ^. contractState . targets . to fold) -- NEW + ] +{- END arbitraryAction2 -} + + +{- START shrinkAction -} + shrinkAction _ (Pay w n) = [Pay w n' | n' <- shrink n] + shrinkAction _ _ = [] +{- END shrinkAction -} + +{- + monitoring _ (Redeem _) = classify True "Contains Redeem" + monitoring (s,s') _ = classify (redeemable s' && Prelude.not (redeemable s)) "Redeemable" + where redeemable s = precondition s (Redeem undefined) +-} +{- START testWallets -} +testWallets :: [Wallet] +testWallets = [w1, w2, w3, w4, w5] +{- END testWallets -} + +{- START prop_Escrow -} +prop_Escrow :: Actions EscrowModel -> Property +prop_Escrow = propRunActions_ +{- END prop_Escrow -} + +{- +finishEscrow :: DL EscrowModel () +finishEscrow = do + anyActions_ + finishingStrategy (const True) + assertModel "Locked funds are not zero" (symIsZero . lockedValue) + +finishingStrategy :: (Wallet -> Bool) -> DL EscrowModel () +finishingStrategy walletAlive = do + contribs <- viewContractState contributions + monitor (classify (Map.null contribs) "no need for extra refund to recover funds") + sequence_ [action $ Refund w | w <- testWallets, w `Map.member` contribs, walletAlive w] + +prop_FinishEscrow :: Property +prop_FinishEscrow = forAllDL finishEscrow prop_Escrow + +noLockProof :: NoLockedFundsProof EscrowModel +noLockProof = defaultNLFP + { nlfpMainStrategy = finishingStrategy (const True) + , nlfpWalletStrategy = finishingStrategy . (==) } + +prop_NoLockedFunds :: Property +prop_NoLockedFunds = checkNoLockedFundsProof defaultCheckOptionsContractModel noLockProof +-} + +tests :: TestTree +tests = testGroup "escrow" + [ testProperty "QuickCheck ContractModel" $ withMaxSuccess 10 prop_Escrow +-- , testProperty "QuickCheck NoLockedFunds" $ withMaxSuccess 10 prop_NoLockedFunds + ] + +{- START escrowParams -} +escrowParams :: EscrowParams d +escrowParams = + EscrowParams + { escrowTargets = + [ payToPaymentPubKeyTarget (mockWalletPaymentPubKeyHash w1) (Ada.adaValueOf 10) + , payToPaymentPubKeyTarget (mockWalletPaymentPubKeyHash w2) (Ada.adaValueOf 20) + ] + } +{- END escrowParams -} diff --git a/doc/plutus/tutorials/Escrow.html b/doc/plutus/tutorials/Escrow.html new file mode 100644 index 0000000000..4e8b351588 --- /dev/null +++ b/doc/plutus/tutorials/Escrow.html @@ -0,0 +1,43 @@ +
. +. +. + 186 -- spending transaction to be paid to target addresses. This may happen if + 187 -- the target address is also used as a change address for the spending + 188 -- transaction, and allowing the target to be exceed prevents outsiders from + 189 -- poisoning the contract by adding arbitrary outputs to the script address. + 190 meetsTarget :: TxInfo -> EscrowTarget DatumHash -> Bool + 191 meetsTarget ptx = \case + 192 PaymentPubKeyTarget pkh vl -> + 193 valuePaidTo ptx (unPaymentPubKeyHash pkh) `geq` vl + 194 ScriptTarget validatorHash dataValue vl -> + 195 case scriptOutputsAt validatorHash ptx of + 196 [(dataValue', vl')] -> + 197 traceIfFalse "dataValue" (dataValue' == dataValue) + 198 && traceIfFalse "value" (vl' `geq` vl) + 199 _ -> False + 200 + 201 {-# INLINABLE validate #-} + 202 validate :: EscrowParams DatumHash -> PaymentPubKeyHash -> Action -> ScriptContext -> Bool + 203 validate EscrowParams{escrowDeadline, escrowTargets} contributor action ScriptContext{scriptContextTxInfo} = + 204 case action of + 205 Redeem -> + 206 traceIfFalse "escrowDeadline-after" (escrowDeadline `after` txInfoValidRange scriptContextTxInfo) + 207 && traceIfFalse "meetsTarget" (all (meetsTarget scriptContextTxInfo) escrowTargets) + 208 Refund -> + 209 traceIfFalse "escrowDeadline-before" ((escrowDeadline - 1) `before` txInfoValidRange scriptContextTxInfo) + 210 && traceIfFalse "txSignedBy" (scriptContextTxInfo `txSignedBy` unPaymentPubKeyHash contributor) + 211 + 212 typedValidator :: EscrowParams Datum -> Scripts.TypedValidator Escrow + 213 typedValidator escrow = go (Haskell.fmap Ledger.datumHash escrow) where + 214 go = Scripts.mkTypedValidatorParam @Escrow + 215 $$(PlutusTx.compile [|| validate ||]) +. +. +. + 361 -- Pay the value 'vl' into the contract + 362 _ <- pay inst params vl + 363 go + 364 + 365 covIdx :: CoverageIndex + 366 covIdx = getCovIdx $$(PlutusTx.compile [|| validate ||]) +\ No newline at end of file diff --git a/doc/plutus/tutorials/Escrow2.hs b/doc/plutus/tutorials/Escrow2.hs new file mode 100644 index 0000000000..2eace2ccf1 --- /dev/null +++ b/doc/plutus/tutorials/Escrow2.hs @@ -0,0 +1,217 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} + +-- This module contains a contract model for positive testing of the +-- simplified escrow contract in Plutus.Contracts.Tutorial.Escrow, +-- with generated escrow targets. See the "Parameterising Models and +-- Dynamic Contract Instances" section of the tutorial. + +module Escrow2(prop_Escrow, EscrowModel) where + +import Control.Lens hiding (both, elements) +import Control.Monad (void) +import Data.Data +import Data.Foldable +import Data.Map (Map) +import Data.Map qualified as Map + +import Ledger (Datum, minAdaTxOut) +import Ledger.Ada qualified as Ada +import Ledger.Value +import Plutus.Contract +import Plutus.Contract.Test +import Plutus.Contract.Test.ContractModel + +import Plutus.Contracts.Tutorial.Escrow hiding (Action (..)) +import Plutus.Trace.Emulator qualified as Trace +import PlutusTx.Monoid (inv) + +import Test.QuickCheck + +{- START ModelState -} +data EscrowModel = EscrowModel { _contributions :: Map Wallet Value + , _targets :: Map Wallet Value + , _phase :: Phase -- NEW! + } deriving (Eq, Show, Data) +{- END ModelState -} + +data Phase = Initial | Running deriving (Eq, Show, Data) + +makeLenses ''EscrowModel + +deriving instance Eq (ContractInstanceKey EscrowModel w s e params) +deriving instance Show (ContractInstanceKey EscrowModel w s e params) + +instance ContractModel EscrowModel where +{- START Action -} + data Action EscrowModel = Init [(Wallet, Integer)] -- NEW! + | Redeem Wallet + | Pay Wallet Integer + deriving (Eq, Show, Data) +{- END Action -} + +{- START ContractInstanceKey -} + data ContractInstanceKey EscrowModel w s e params where + WalletKey :: Wallet -> ContractInstanceKey EscrowModel () EscrowSchema EscrowError (EscrowParams Datum) +{- END ContractInstanceKey -} + +{- START initialState -} + initialState = EscrowModel { _contributions = Map.empty + , _targets = Map.empty + , _phase = Initial + } +{- END initialState -} + +{- START initialInstances -} + initialInstances = [] +{- END initialInstances -} + +{- START startInstances -} + startInstances _ (Init wns) = + [StartContract (WalletKey w) (escrowParams wns) | w <- testWallets] + startInstances _ _ = [] +{- END startInstances -} + + instanceWallet (WalletKey w) = w + +{- START instanceContract -} + instanceContract _ WalletKey{} params = testContract params +{- END instanceContract -} + +{- +{- START nextState -} + nextState a = case a of + Init wns -> do + phase .= Running + targets .= Map.fromList [(w, Ada.adaValueOf (fromInteger n)) | (w,n) <- wns] + ... +{- END nextState -} +-} + + nextState a = case a of + Init wns -> do + phase .= Running + targets .= Map.fromList [(w, Ada.adaValueOf (fromInteger n)) | (w,n) <- wns] + Pay w v -> do + withdraw w (Ada.adaValueOf $ fromInteger v) + contributions %= Map.insertWith (<>) w (Ada.adaValueOf $ fromInteger v) + wait 1 + Redeem w -> do + targets <- viewContractState targets + contribs <- viewContractState contributions + sequence_ [ deposit w v | (w, v) <- Map.toList targets ] + -- omit next two lines to disable disbursement of the surplus + let leftoverValue = fold contribs <> inv (fold targets) + deposit w leftoverValue + contributions .= Map.empty + wait 1 + +{- +{- START precondition -} + precondition s a = case a of + Init _ -> currentPhase == Initial + Redeem _ -> currentPhase == Running && ... + Pay _ v -> currentPhase == Running && ... + where currentPhase = s ^. contractState . phase +{- END precondition -} + +{- START tightprecondition -} + precondition s a = case a of + Init tgts-> currentPhase == Initial + && and [Ada.adaValueOf (fromInteger n) `geq` Ada.toValue minAdaTxOut | (w,n) <- tgts] + ... +{- END tightprecondition -} +-} + + precondition s a = case a of + Init _ -> currentPhase == Initial + Redeem _ -> currentPhase == Running + && (s ^. contractState . contributions . to fold) `geq` (s ^. contractState . targets . to fold) + Pay _ v -> currentPhase == Running + && Ada.adaValueOf (fromInteger v) `geq` Ada.toValue minAdaTxOut + where currentPhase = s ^. contractState . phase + +{- +{- START perform -} + perform h _ _ a = case a of + Init _ -> do + return () + ... +{- END perform -} +-} + + perform h _ _ a = case a of + Init _ -> do + return () + Pay w v -> do + Trace.callEndpoint @"pay-escrow" (h $ WalletKey w) (Ada.adaValueOf $ fromInteger v) + delay 1 + Redeem w -> do + Trace.callEndpoint @"redeem-escrow" (h $ WalletKey w) () + delay 1 + +{- +{- START arbitraryAction -} + arbitraryAction s + | s ^.contractState . phase == Initial + = Init <$> arbitraryTargets + | otherwise + = ...as before... +{- END arbitraryAction -} +-} + + arbitraryAction s + | s ^.contractState . phase == Initial + = Init <$> arbitraryTargets + | otherwise + = frequency $ [ (3, Pay <$> elements testWallets <*> choose (1, 30)) ] ++ + [ (1, Redeem <$> elements testWallets) + | (s ^. contractState . contributions . to fold) `geq` (s ^. contractState . targets . to fold) + ] + +{- START shrinkAction -} + shrinkAction _ (Init tgts) = map Init (shrinkList (\(w,n)->(w,)<$>shrink n) tgts) +{- END shrinkAction -} + shrinkAction _ (Pay w n) = [Pay w n' | n' <- shrink n] + shrinkAction _ _ = [] + +{- START arbitraryTargets -} +arbitraryTargets :: Gen [(Wallet,Integer)] +arbitraryTargets = do + ws <- sublistOf testWallets + vs <- infiniteListOf $ choose (1,30) + return $ zip ws vs +{- END arbitraryTargets -} + +testWallets :: [Wallet] +testWallets = [w1, w2, w3, w4, w5] + +{- START testContract -} +testContract :: EscrowParams Datum -> Contract () EscrowSchema EscrowError () +testContract params = selectList [ void $ payEp params + , void $ redeemEp params + ] >> testContract params +{- END testContract -} + +prop_Escrow :: Actions EscrowModel -> Property +prop_Escrow = propRunActions_ + +{- START escrowParams -} +escrowParams :: [(Wallet, Integer)] -> EscrowParams d +escrowParams tgts = + EscrowParams + { escrowTargets = + [ payToPaymentPubKeyTarget (mockWalletPaymentPubKeyHash w) (Ada.adaValueOf (fromInteger n)) + | (w,n) <- tgts + ] + } +{- END escrowParams -} diff --git a/doc/plutus/tutorials/Escrow3.hs b/doc/plutus/tutorials/Escrow3.hs new file mode 100644 index 0000000000..d8774fc858 --- /dev/null +++ b/doc/plutus/tutorials/Escrow3.hs @@ -0,0 +1,296 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} + +-- This module contains a contract model for positive testing of the +-- simplified escrow contract in Plutus.Contracts.Tutorial.Escrow, +-- with generated escrow targets. See the "Parameterising Models and +-- Dynamic Contract Instances" section of the tutorial. + +module Escrow3(prop_Escrow, prop_FinishEscrow, prop_NoLockedFunds, EscrowModel) where + +import Control.Lens hiding (both, elements) +import Control.Monad (void, when) +import Data.Data +import Data.Foldable +import Data.Map (Map) +import Data.Map qualified as Map + +import Ledger (Datum, minAdaTxOut) +import Ledger.Ada qualified as Ada +import Ledger.Value +import Plutus.Contract +import Plutus.Contract.Test +import Plutus.Contract.Test.ContractModel + +import Plutus.Contracts.Tutorial.Escrow hiding (Action (..)) +import Plutus.Trace.Emulator qualified as Trace +import PlutusTx.Monoid (inv) + +import Test.QuickCheck + +data EscrowModel = EscrowModel { _contributions :: Map Wallet Value + , _targets :: Map Wallet Value + , _phase :: Phase + } deriving (Eq, Show, Data) + +data Phase = Initial | Running deriving (Eq, Show, Data) + +makeLenses ''EscrowModel + +deriving instance Eq (ContractInstanceKey EscrowModel w s e params) +deriving instance Show (ContractInstanceKey EscrowModel w s e params) + +instance ContractModel EscrowModel where +{- START EscrowModel -} + data Action EscrowModel = Init [(Wallet, Integer)] + | Redeem Wallet + | Pay Wallet Integer + | Refund Wallet -- NEW! + deriving (Eq, Show, Data) +{- END EscrowModel -} + + data ContractInstanceKey EscrowModel w s e params where + WalletKey :: Wallet -> ContractInstanceKey EscrowModel () EscrowSchema EscrowError (EscrowParams Datum) + + initialState = EscrowModel { _contributions = Map.empty + , _targets = Map.empty + , _phase = Initial + } + + initialInstances = [] + + startInstances _ (Init wns) = + [StartContract (WalletKey w) (escrowParams wns) | w <- testWallets] + startInstances _ _ = [] + + instanceWallet (WalletKey w) = w + + instanceContract _ WalletKey{} params = testContract params + + nextState a = case a of + Init wns -> do + phase .= Running + targets .= Map.fromList [(w, Ada.adaValueOf (fromInteger n)) | (w,n) <- wns] + Pay w v -> do + withdraw w (Ada.adaValueOf $ fromInteger v) + contributions %= Map.insertWith (<>) w (Ada.adaValueOf $ fromInteger v) + wait 1 + Redeem w -> do + targets <- viewContractState targets + contribs <- viewContractState contributions + sequence_ [ deposit w v | (w, v) <- Map.toList targets ] + -- omit next two lines to disable disbursement of the surplus + let leftoverValue = fold contribs <> inv (fold targets) + deposit w leftoverValue + contributions .= Map.empty + wait 1 + Refund w -> do + v <- viewContractState $ contributions . at w . to fold + contributions %= Map.delete w + deposit w v + wait 1 + + precondition s a = case a of + Init tgts -> currentPhase == Initial + && and [Ada.adaValueOf (fromInteger n) `geq` Ada.toValue minAdaTxOut | (_,n) <- tgts] + Redeem _ -> currentPhase == Running + && fold (s ^. contractState . contributions) `geq` fold (s ^. contractState . targets) + -- && fold (s ^. contractState . contributions) == fold (s ^. contractState . targets) + Pay _ v -> currentPhase == Running + && Ada.adaValueOf (fromInteger v) `geq` Ada.toValue minAdaTxOut + Refund w -> currentPhase == Running + && w `Map.member` (s ^. contractState . contributions) + where currentPhase = s ^. contractState . phase + +{- +{- START strongPrecondition -} +precondition s (Redeem _) = + currentPhase == Running + && fold (s ^. contractState . contributions) == fold (s ^. contractState . targets) +{- END strongPrecondition -} +-} + + perform h _ _ a = case a of + Init _ -> do + return () + Pay w v -> do + Trace.callEndpoint @"pay-escrow" (h $ WalletKey w) (Ada.adaValueOf $ fromInteger v) + delay 1 + Redeem w -> do + Trace.callEndpoint @"redeem-escrow" (h $ WalletKey w) () + delay 1 + Refund w -> do + Trace.callEndpoint @"refund-escrow" (h $ WalletKey w) () + delay 1 + +{- +{-START RefundModel -} + nextState (Refund w) = do + v <- viewContractState $ contributions . at w . to fold + contributions %= Map.delete w + deposit w v + wait 1 + + precondition s (Refund w) = + currentPhase == Running + && w `Map.member` (s ^. contractState . contributions) + where currentPhase = s ^. contractState . phase + + perform h _ _ (Refund w) = do + Trace.callEndpoint @"refund-escrow" (h $ WalletKey w) () + delay 1 + + arbitraryAction s + ... + = frequency $ ... ++ + [ (1, Refund <$> elements testWallets) ] +{- END RefundModel -} + -} + + arbitraryAction s + | s ^.contractState . phase == Initial + = Init <$> arbitraryTargets + | otherwise + = frequency $ [ (3, Pay <$> elements testWallets <*> choose (1, 30)) ] ++ + [ (1, Redeem <$> elements testWallets) + | (s ^. contractState . contributions . to fold) `geq` (s ^. contractState . targets . to fold) + ] ++ + [ (1, Refund <$> elements testWallets) ] + + + shrinkAction _ (Init tgts) = map Init (shrinkList (\(w,n)->(w,)<$>shrink n) tgts) + shrinkAction _ (Pay w n) = [Pay w n' | n' <- shrink n] + shrinkAction _ _ = [] + +arbitraryTargets :: Gen [(Wallet,Integer)] +arbitraryTargets = do + ws <- sublistOf testWallets + vs <- infiniteListOf $ choose (1,30) + return $ zip ws vs + +testWallets :: [Wallet] +testWallets = [w1, w2, w3, w4, w5] + +{- START testContract -} +testContract :: EscrowParams Datum -> Contract () EscrowSchema EscrowError () +testContract params = selectList [ void $ payEp params + , void $ redeemEp params + , void $ refundEp params -- NEW! + ] >> testContract params +{- END testContract -} + +prop_Escrow :: Actions EscrowModel -> Property +prop_Escrow = propRunActions_ + + +escrowParams :: [(Wallet, Integer)] -> EscrowParams d +escrowParams tgts = + EscrowParams + { escrowTargets = + [ payToPaymentPubKeyTarget (mockWalletPaymentPubKeyHash w) (Ada.adaValueOf (fromInteger n)) + | (w,n) <- tgts + ] + } + +{- +-- This is the first--bad--approach to recovering locked funds. +{- START finishEscrow -} +finishEscrow :: DL EscrowModel () +finishEscrow = do + anyActions_ + finishingStrategy w1 + assertModel "Locked funds are not zero" (symIsZero . lockedValue) +{- END finishEscrow -} + +{- START badFinishingStrategy -} +finishingStrategy :: Wallet -> DL EscrowModel () +finishingStrategy w = do + currentPhase <- viewContractState phase + when (currentPhase /= Initial) $ do + action $ Redeem w +{- END badFinishingStrategy -} + +{- START finishingStrategy -} +finishingStrategy :: Wallet -> DL EscrowModel () +finishingStrategy w = do + currentPhase <- viewContractState phase + when (currentPhase /= Initial) $ do + currentTargets <- viewContractState targets + currentContribs <- viewContractState contributions + let deficit = fold currentTargets <> inv (fold currentContribs) + when (deficit `gt` Ada.adaValueOf 0) $ + action $ Pay w $ round $ Ada.getAda $ max minAdaTxOut $ Ada.fromValue deficit + action $ Redeem w +{- END finishingStrategy -} + +-- This unilateral strategy fails. +{- START noLockProof -} +noLockProof :: NoLockedFundsProof EscrowModel +noLockProof = defaultNLFP + { nlfpMainStrategy = finishingStrategy w1 + , nlfpWalletStrategy = finishingStrategy } +{- END noLockProof -} +-} + +finishEscrow :: DL EscrowModel () +finishEscrow = do + anyActions_ + finishingStrategy + assertModel "Locked funds are not zero" (symIsZero . lockedValue) + +{- +{- START betterFinishingStrategy -} +finishingStrategy :: (Wallet -> Bool) -> DL EscrowModel () +finishingStrategy walletActive = do + contribs <- viewContractState contributions + monitor (classify (Map.null contribs) "no need for extra refund to recover funds") + sequence_ [action $ Refund w | w <- testWallets, w `Map.member` contribs, walletActive w] +{- END betterFinishingStrategy -} +-} + +{- START prop_FinishEscrow -} +prop_FinishEscrow :: Property +prop_FinishEscrow = forAllDL finishEscrow prop_Escrow +{- END prop_FinishEscrow -} + +{- START BetterNoLockProof -} +noLockProof :: NoLockedFundsProof EscrowModel +noLockProof = defaultNLFP + { nlfpMainStrategy = finishingStrategy + , nlfpWalletStrategy = walletStrategy } +{- END BetterNoLockProof -} + +{- START prop_NoLockedFunds -} +prop_NoLockedFunds :: Property +prop_NoLockedFunds = checkNoLockedFundsProof noLockProof +{- END prop_NoLockedFunds -} + +{- +{- START fixedTargets -} +fixedTargets :: DL EscrowModel () +fixedTargets = do + action $ Init [(w1,10),(w2,20)] + anyActions_ +{- END fixedTargets -} +-} + +{- START BetterStrategies -} +finishingStrategy :: DL EscrowModel () +finishingStrategy = do + contribs <- viewContractState contributions + monitor (tabulate "Refunded wallets" [show . Map.size $ contribs]) + sequence_ [action $ Refund w | w <- testWallets, w `Map.member` contribs] + +walletStrategy :: Wallet -> DL EscrowModel () +walletStrategy w = do + contribs <- viewContractState contributions + when (w `Map.member` contribs) $ action $ Refund w +{- END BetterStrategies -} diff --git a/doc/plutus/tutorials/Escrow4.hs b/doc/plutus/tutorials/Escrow4.hs new file mode 100644 index 0000000000..b5660a70f3 --- /dev/null +++ b/doc/plutus/tutorials/Escrow4.hs @@ -0,0 +1,283 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} + +-- This module contains a contract model for positive testing of the +-- simplified escrow contract in Plutus.Contracts.Tutorial.Escrow, +-- with generated escrow targets. See the "Parameterising Models and +-- Dynamic Contract Instances" section of the tutorial. + +module Escrow4(prop_Escrow, prop_FinishEscrow, prop_NoLockedFunds, EscrowModel) where + +import Control.Lens hiding (both, elements) +import Control.Monad (void, when) +import Data.Data +import Data.Default +import Data.Foldable +import Data.Map (Map) +import Data.Map qualified as Map + +import Ledger (Datum, Slot (..), minAdaTxOut) +import Ledger.Ada qualified as Ada +import Ledger.TimeSlot (SlotConfig (..)) +import Ledger.Value (Value, geq) +import Plutus.Contract (Contract, selectList) +import Plutus.Contract.Test +import Plutus.Contract.Test.ContractModel +import Plutus.V1.Ledger.Time + +import Plutus.Contracts.Escrow hiding (Action (..)) +import Plutus.Trace.Emulator qualified as Trace +import PlutusTx.Monoid (inv) + +import Test.QuickCheck + +{- START EscrowModel -} +data EscrowModel = EscrowModel { _contributions :: Map Wallet Value + , _targets :: Map Wallet Value + , _refundSlot :: Slot -- NEW!!! + , _phase :: Phase + } deriving (Eq, Show, Data) +{- END EscrowModel -} + +{- START Phase -} +data Phase = Initial | Running | Refunding deriving (Eq, Show, Data) +{- END Phase -} + +makeLenses ''EscrowModel + +deriving instance Eq (ContractInstanceKey EscrowModel w s e params) +deriving instance Show (ContractInstanceKey EscrowModel w s e params) + +instance ContractModel EscrowModel where + +{- START Action -} + data Action EscrowModel = Init Slot [(Wallet, Integer)] -- NEW!!! + | Redeem Wallet + | Pay Wallet Integer + | Refund Wallet + deriving (Eq, Show, Data) +{- END Action -} + + data ContractInstanceKey EscrowModel w s e params where + WalletKey :: Wallet -> ContractInstanceKey EscrowModel () EscrowSchema EscrowError (EscrowParams Datum) + + initialState = EscrowModel { _contributions = Map.empty + , _targets = Map.empty + , _refundSlot = 0 + , _phase = Initial + } + + initialInstances = [] + +{- START startInstances -} + startInstances _ (Init s wns) = + [StartContract (WalletKey w) (escrowParams s wns) | w <- testWallets] +{- END startInstances -} + startInstances _ _ = [] + + instanceWallet (WalletKey w) = w + + instanceContract _ WalletKey{} params = testContract params + +{- START nextState -} + nextState (Init s wns) = do + phase .= Running + targets .= Map.fromList [(w, Ada.adaValueOf (fromInteger n)) | (w,n) <- wns] + refundSlot .= s -- NEW!!! +{- END nextState -} + + nextState a = case a of + Init s wns -> do + phase .= Running + targets .= Map.fromList [(w, Ada.adaValueOf (fromInteger n)) | (w,n) <- wns] + refundSlot .= s + Pay w v -> do + withdraw w (Ada.adaValueOf $ fromInteger v) + contributions %= Map.insertWith (<>) w (Ada.adaValueOf $ fromInteger v) + wait 1 + Redeem w -> do + targets <- viewContractState targets + contribs <- viewContractState contributions + sequence_ [ deposit w v | (w, v) <- Map.toList targets ] + let leftoverValue = fold contribs <> inv (fold targets) + deposit w leftoverValue + contributions .= Map.empty + wait 1 + Refund w -> do + v <- viewContractState $ contributions . at w . to fold + contributions %= Map.delete w + deposit w v + wait 1 + +{- START nextReactiveState -} + nextReactiveState slot = do + deadline <- viewContractState refundSlot + when (slot >= deadline) $ phase .= Refunding +{- END nextReactiveState -} + +{- START precondition -} + precondition s a = case a of + Init s tgts -> currentPhase == Initial + && s > 1 + && and [Ada.adaValueOf (fromInteger n) `geq` Ada.toValue minAdaTxOut | (_,n) <- tgts] + Redeem _ -> currentPhase == Running + && fold (s ^. contractState . contributions) `geq` fold (s ^. contractState . targets) + Pay _ v -> currentPhase == Running + && Ada.adaValueOf (fromInteger v) `geq` Ada.toValue minAdaTxOut + Refund w -> currentPhase == Refunding -- NEW!!! + && w `Map.member` (s ^. contractState . contributions) + where currentPhase = s ^. contractState . phase +{- END precondition -} + + perform h _ _ a = case a of + Init _ _ -> do + return () + Pay w v -> do + Trace.callEndpoint @"pay-escrow" (h $ WalletKey w) (Ada.adaValueOf $ fromInteger v) + delay 1 + Redeem w -> do + Trace.callEndpoint @"redeem-escrow" (h $ WalletKey w) () + delay 1 + Refund w -> do + Trace.callEndpoint @"refund-escrow" (h $ WalletKey w) () + delay 1 + +{- START arbitraryAction -} + arbitraryAction s + | s ^.contractState . phase == Initial + = Init <$> (Slot . getPositive <$> arbitrary) <*> arbitraryTargets +{- END arbitraryAction -} + | otherwise + = frequency $ [ (3, Pay <$> elements testWallets <*> choose (1, 30)) ] ++ + [ (1, Redeem <$> elements testWallets) + | (s ^. contractState . contributions . to fold) `geq` (s ^. contractState . targets . to fold) + ] ++ + [ (1, Refund <$> elements testWallets) ] +{- +{- START weightedArbitraryAction -} + arbitraryAction s + | s ^.contractState . phase == Initial + = Init <$> (Slot . getPositive <$> scale (*10) arbitrary) <*> arbitraryTargets +{- END weightedArbitraryAction -} +-} + +{- START shrinkAction -} + shrinkAction _ (Init s tgts) = map (Init s) (shrinkList (\(w,n)->(w,)<$>shrink n) tgts) + ++ map (`Init` tgts) (map Slot . shrink . getSlot $ s) -- NEW!!! +{- END shrinkAction -} + shrinkAction _ (Pay w n) = [Pay w n' | n' <- shrink n] + shrinkAction _ _ = [] + +arbitraryTargets :: Gen [(Wallet,Integer)] +arbitraryTargets = do + ws <- sublistOf testWallets + vs <- infiniteListOf $ choose (1,30) + return $ zip ws vs + +testWallets :: [Wallet] +testWallets = [w1, w2, w3, w4, w5] + +testContract :: EscrowParams Datum -> Contract () EscrowSchema EscrowError () +testContract params = selectList [ void $ payEp params + , void $ redeemEp params + , void $ refundEp params + ] >> testContract params + + +prop_Escrow :: Actions EscrowModel -> Property +prop_Escrow = propRunActions_ + +{- START escrowParams -} +escrowParams :: Slot -> [(Wallet, Integer)] -> EscrowParams d +escrowParams s tgts = + EscrowParams + { escrowTargets = + [ payToPaymentPubKeyTarget (mockWalletPaymentPubKeyHash w) (Ada.adaValueOf (fromInteger n)) + | (w,n) <- tgts + ] + , escrowDeadline = scSlotZeroTime def + POSIXTime (getSlot s * scSlotLength def) -- NEW!!! + } +{- END escrowParams -} + + +finishEscrow :: DL EscrowModel () +finishEscrow = do + anyActions_ + finishingStrategy + assertModel "Locked funds are not zero" (symIsZero . lockedValue) + +{- +{- START oldFinishingStrategy -} +finishingStrategy :: DL EscrowModel () +finishingStrategy = do + contribs <- viewContractState contributions + monitor (tabulate "Refunded wallets" [show . Map.size $ contribs]) + sequence_ [action $ Refund w | w <- testWallets, w `Map.member` contribs] +{- END oldFinishingStrategy -} +-} + +{- START finishingStrategy -} +finishingStrategy :: DL EscrowModel () +finishingStrategy = do + contribs <- viewContractState contributions + monitor (tabulate "Refunded wallets" [show . Map.size $ contribs]) + waitUntilDeadline -- NEW!!! + sequence_ [action $ Refund w | w <- testWallets, w `Map.member` contribs] +{- END finishingStrategy -} +{- +{- START monitoredFinishingStrategy -} +finishingStrategy :: DL EscrowModel () +finishingStrategy = do + contribs <- viewContractState contributions + monitor (tabulate "Refunded wallets" [show . Map.size $ contribs]) + phase <- viewContractState phase -- NEW!!! + monitor $ tabulate "Phase" [show phase] -- NEW!!! + waitUntilDeadline + sequence_ [action $ Refund w | w <- testWallets, w `Map.member` contribs] +{- END monitoredFinishingStrategy -} +-} + +walletStrategy :: Wallet -> DL EscrowModel () +walletStrategy w = do + contribs <- viewContractState contributions + when (w `Map.member` contribs) $ do + --waitUntilDeadline + action $ Refund w + +{- START waitUntilDeadline -} +waitUntilDeadline :: DL EscrowModel () +waitUntilDeadline = do + deadline <- viewContractState refundSlot + slot <- viewModelState currentSlot + when (slot < deadline) $ waitUntilDL deadline +{- END waitUntilDeadline -} + +noLockProof :: NoLockedFundsProof EscrowModel +noLockProof = defaultNLFP + { nlfpMainStrategy = finishingStrategy + , nlfpWalletStrategy = walletStrategy } + +{- START prop_FinishEscrow -} +prop_FinishEscrow :: Property +prop_FinishEscrow = forAllDL finishEscrow prop_Escrow +{- END prop_FinishEscrow -} + +{- +{- START prop_FinishFast -} +prop_FinishFast :: Property +prop_FinishFast = forAllDL finishEscrow $ const True +{- END prop_FinishFast -} +-} + +prop_NoLockedFunds :: Property +prop_NoLockedFunds = checkNoLockedFundsProof noLockProof + diff --git a/doc/plutus/tutorials/Escrow5.hs b/doc/plutus/tutorials/Escrow5.hs new file mode 100644 index 0000000000..d0d8da8066 --- /dev/null +++ b/doc/plutus/tutorials/Escrow5.hs @@ -0,0 +1,237 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} + +-- This module contains a contract model for positive testing of the +-- simplified escrow contract in Plutus.Contracts.Tutorial.Escrow, +-- with generated escrow targets. See the "Parameterising Models and +-- Dynamic Contract Instances" section of the tutorial. + +module Escrow5(prop_Escrow, prop_FinishEscrow, prop_FinishFast, prop_NoLockedFunds, prop_NoLockedFundsFast, + check_propEscrowWithCoverage, EscrowModel) where + +import Control.Lens hiding (both, elements) +import Control.Monad (void, when) +import Data.Data +import Data.Default +import Data.Foldable +import Data.Map (Map) +import Data.Map qualified as Map + +import Ledger (Datum, Slot (..), minAdaTxOut) +import Ledger.Ada qualified as Ada +import Ledger.TimeSlot (SlotConfig (..)) +import Ledger.Value (Value, geq) +import Plutus.Contract (Contract, selectList) +import Plutus.Contract.Test +import Plutus.Contract.Test.ContractModel +import Plutus.Contract.Test.Coverage +import Plutus.V1.Ledger.Time + +import Plutus.Contracts.Escrow hiding (Action (..)) +import Plutus.Trace.Emulator qualified as Trace +import PlutusTx.Monoid (inv) + +import Test.QuickCheck + +data EscrowModel = EscrowModel { _contributions :: Map Wallet Value + , _targets :: Map Wallet Value + , _refundSlot :: Slot + , _phase :: Phase + } deriving (Eq, Show, Data) + +data Phase = Initial | Running | Refunding deriving (Eq, Show, Data) + +makeLenses ''EscrowModel + +deriving instance Eq (ContractInstanceKey EscrowModel w s e params) +deriving instance Show (ContractInstanceKey EscrowModel w s e params) + +instance ContractModel EscrowModel where + data Action EscrowModel = Init Slot [(Wallet, Integer)] + | Redeem Wallet + | Pay Wallet Integer + | Refund Wallet + deriving (Eq, Show, Data) + + data ContractInstanceKey EscrowModel w s e params where + WalletKey :: Wallet -> ContractInstanceKey EscrowModel () EscrowSchema EscrowError (EscrowParams Datum) + + initialState = EscrowModel { _contributions = Map.empty + , _targets = Map.empty + , _refundSlot = 0 + , _phase = Initial + } + + initialInstances = [] + + startInstances _ (Init s wns) = + [StartContract (WalletKey w) (escrowParams s wns) | w <- testWallets] + startInstances _ _ = [] + + instanceWallet (WalletKey w) = w + + instanceContract _ WalletKey{} params = testContract params + + nextState a = case a of + Init s wns -> do + phase .= Running + targets .= Map.fromList [(w, Ada.adaValueOf (fromInteger n)) | (w,n) <- wns] + refundSlot .= s + Pay w v -> do + withdraw w (Ada.adaValueOf $ fromInteger v) + contributions %= Map.insertWith (<>) w (Ada.adaValueOf $ fromInteger v) + wait 1 + Redeem w -> do + targets <- viewContractState targets + contribs <- viewContractState contributions + sequence_ [ deposit w v | (w, v) <- Map.toList targets ] + let leftoverValue = fold contribs <> inv (fold targets) + deposit w leftoverValue + contributions .= Map.empty + wait 1 + Refund w -> do + v <- viewContractState $ contributions . at w . to fold + contributions %= Map.delete w + deposit w v + wait 1 + + + nextReactiveState slot = do + deadline <- viewContractState refundSlot + when (slot >= deadline) $ phase .= Refunding + + + precondition s a = case a of + Init s tgts -> currentPhase == Initial + && s > 1 + && and [Ada.adaValueOf (fromInteger n) `geq` Ada.toValue minAdaTxOut | (_,n) <- tgts] + Redeem _ -> currentPhase == Running + && fold (s ^. contractState . contributions) `geq` fold (s ^. contractState . targets) + Pay _ v -> currentPhase == Running + && Ada.adaValueOf (fromInteger v) `geq` Ada.toValue minAdaTxOut + Refund w -> currentPhase == Refunding + && w `Map.member` (s ^. contractState . contributions) + where currentPhase = s ^. contractState . phase + + + perform h _ _ a = case a of + Init _ _ -> do + return () + Pay w v -> do + Trace.callEndpoint @"pay-escrow" (h $ WalletKey w) (Ada.adaValueOf $ fromInteger v) + delay 1 + Redeem w -> do + Trace.callEndpoint @"redeem-escrow" (h $ WalletKey w) () + delay 1 + Refund w -> do + Trace.callEndpoint @"refund-escrow" (h $ WalletKey w) () + delay 1 + + arbitraryAction s + | s ^.contractState . phase == Initial + = Init <$> (Slot . getPositive <$> scale (*10) arbitrary) <*> arbitraryTargets + | otherwise + = frequency $ [ (3, Pay <$> elements testWallets <*> choose (1, 30)) ] ++ + [ (1, Redeem <$> elements testWallets) + | (s ^. contractState . contributions . to fold) `geq` (s ^. contractState . targets . to fold) + ] ++ + [ (1, Refund <$> elements testWallets) ] + + + shrinkAction _ (Init s tgts) = map (Init s) (shrinkList (\(w,n)->(w,)<$>shrink n) tgts) + ++ map (`Init` tgts) (map Slot . shrink . getSlot $ s) + shrinkAction _ (Pay w n) = [Pay w n' | n' <- shrink n] + shrinkAction _ _ = [] + +arbitraryTargets :: Gen [(Wallet,Integer)] +arbitraryTargets = do + ws <- sublistOf testWallets + vs <- infiniteListOf $ choose (1,30) + return $ zip ws vs + +testWallets :: [Wallet] +testWallets = [w1, w2, w3, w4, w5] + +testContract :: EscrowParams Datum -> Contract () EscrowSchema EscrowError () +testContract params = selectList [ void $ payEp params + , void $ redeemEp params + , void $ refundEp params + ] >> testContract params + + +prop_Escrow :: Actions EscrowModel -> Property +prop_Escrow = propRunActions_ + + +escrowParams :: Slot -> [(Wallet, Integer)] -> EscrowParams d +escrowParams s tgts = + EscrowParams + { escrowTargets = + [ payToPaymentPubKeyTarget (mockWalletPaymentPubKeyHash w) (Ada.adaValueOf (fromInteger n)) + | (w,n) <- tgts + ] + , escrowDeadline = scSlotZeroTime def + POSIXTime (getSlot s * scSlotLength def) + } + +finishEscrow :: DL EscrowModel () +finishEscrow = do + anyActions_ + finishingStrategy + assertModel "Locked funds are not zero" (symIsZero . lockedValue) + +finishingStrategy :: DL EscrowModel () +finishingStrategy = do + contribs <- viewContractState contributions + monitor (tabulate "Refunded wallets" [show . Map.size $ contribs]) + phase <- viewContractState phase + monitor $ tabulate "Phase" [show phase] + waitUntilDeadline + sequence_ [action $ Refund w | w <- testWallets, w `Map.member` contribs] + +walletStrategy :: Wallet -> DL EscrowModel () +walletStrategy w = do + contribs <- viewContractState contributions + --waitUntilDeadline + when (w `Map.member` contribs) $ do + action $ Refund w + +waitUntilDeadline :: DL EscrowModel () +waitUntilDeadline = do + deadline <- viewContractState refundSlot + slot <- viewModelState currentSlot + when (slot < deadline) $ waitUntilDL deadline + +noLockProof :: NoLockedFundsProof EscrowModel +noLockProof = defaultNLFP + { nlfpMainStrategy = finishingStrategy + , nlfpWalletStrategy = walletStrategy } + +prop_FinishEscrow :: Property +prop_FinishEscrow = forAllDL finishEscrow prop_Escrow + +prop_FinishFast :: Property +prop_FinishFast = forAllDL finishEscrow $ const True + +prop_NoLockedFunds :: Property +prop_NoLockedFunds = checkNoLockedFundsProof noLockProof + +prop_NoLockedFundsFast :: Property +prop_NoLockedFundsFast = checkNoLockedFundsProofFast noLockProof + +{- START check_propEscrowWithCoverage -} +check_propEscrowWithCoverage :: IO () +check_propEscrowWithCoverage = do + cr <- quickCheckWithCoverage stdArgs (set coverageIndex covIdx $ defaultCoverageOptions) $ \covopts -> + withMaxSuccess 1000 $ + propRunActionsWithOptions @EscrowModel defaultCheckOptionsContractModel covopts + (const (pure True)) + writeCoverageReport "Escrow" covIdx cr +{- END check_propEscrowWithCoverage -} diff --git a/doc/plutus/tutorials/Escrow6.hs b/doc/plutus/tutorials/Escrow6.hs new file mode 100644 index 0000000000..c7f92e02c2 --- /dev/null +++ b/doc/plutus/tutorials/Escrow6.hs @@ -0,0 +1,273 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -fno-warn-name-shadowing #-} + +-- This module contains a contract model for positive testing of the +-- simplified escrow contract in Plutus.Contracts.Tutorial.Escrow, +-- with generated escrow targets. See the "Parameterising Models and +-- Dynamic Contract Instances" section of the tutorial. + +module Escrow6 + ( prop_Escrow + , prop_FinishEscrow + , prop_FinishFast + , prop_NoLockedFunds + , prop_NoLockedFundsFast + , prop_CrashTolerance + , check_propEscrowWithCoverage + , EscrowModel + ) where + +import Control.Lens hiding (both, elements) +import Control.Monad (void, when) +import Data.Data +import Data.Default +import Data.Foldable +import Data.Map (Map) +import Data.Map qualified as Map + +import Ledger (Datum, Slot (..), minAdaTxOut) +import Ledger.Ada qualified as Ada +import Ledger.TimeSlot (SlotConfig (..)) +import Ledger.Value (Value, geq) +import Plutus.Contract (Contract, selectList) +import Plutus.Contract.Test +import Plutus.Contract.Test.ContractModel +import Plutus.Contract.Test.ContractModel.CrashTolerance +import Plutus.Contract.Test.Coverage +import Plutus.V1.Ledger.Time + +import Plutus.Contracts.Escrow hiding (Action (..)) +import Plutus.Trace.Emulator qualified as Trace +import PlutusTx.Monoid (inv) + +import Test.QuickCheck + +data EscrowModel = EscrowModel { _contributions :: Map Wallet Value + , _targets :: Map Wallet Value + , _refundSlot :: Slot + , _phase :: Phase + } deriving (Eq, Show, Data) + +data Phase = Initial | Running | Refunding deriving (Eq, Show, Data) + +makeLenses ''EscrowModel + +deriving instance Eq (ContractInstanceKey EscrowModel w s e params) +deriving instance Show (ContractInstanceKey EscrowModel w s e params) + +instance ContractModel EscrowModel where + data Action EscrowModel = Init Slot [(Wallet, Integer)] + | Redeem Wallet + | Pay Wallet Integer + | Refund Wallet + deriving (Eq, Show, Data) + + data ContractInstanceKey EscrowModel w s e params where + WalletKey :: Wallet -> ContractInstanceKey EscrowModel () EscrowSchema EscrowError (EscrowParams Datum) + + initialState = EscrowModel { _contributions = Map.empty + , _targets = Map.empty + , _refundSlot = 0 + , _phase = Initial + } + + initialInstances = [] + + startInstances _ (Init s wns) = + [StartContract (WalletKey w) (escrowParams s wns) | w <- testWallets] + startInstances _ _ = [] + + instanceWallet (WalletKey w) = w + + instanceContract _ WalletKey{} params = testContract params + + nextState a = case a of + Init s wns -> do + phase .= Running + targets .= Map.fromList [(w, Ada.adaValueOf (fromInteger n)) | (w,n) <- wns] + refundSlot .= s + Pay w v -> do + withdraw w (Ada.adaValueOf $ fromInteger v) + contributions %= Map.insertWith (<>) w (Ada.adaValueOf $ fromInteger v) + wait 1 + Redeem w -> do + targets <- viewContractState targets + contribs <- viewContractState contributions + sequence_ [ deposit w v | (w, v) <- Map.toList targets ] + let leftoverValue = fold contribs <> inv (fold targets) + deposit w leftoverValue + contributions .= Map.empty + wait 1 + Refund w -> do + v <- viewContractState $ contributions . at w . to fold + contributions %= Map.delete w + deposit w v + wait 1 + + + nextReactiveState slot = do + deadline <- viewContractState refundSlot + when (slot >= deadline) $ phase .= Refunding + + + precondition s a = case a of + Init s tgts -> currentPhase == Initial + && s > 1 + && and [Ada.adaValueOf (fromInteger n) `geq` Ada.toValue minAdaTxOut | (_,n) <- tgts] + Redeem _ -> currentPhase == Running + && fold (s ^. contractState . contributions) `geq` fold (s ^. contractState . targets) + Pay _ v -> currentPhase == Running + && Ada.adaValueOf (fromInteger v) `geq` Ada.toValue minAdaTxOut + Refund w -> currentPhase == Refunding + && w `Map.member` (s ^. contractState . contributions) + where currentPhase = s ^. contractState . phase + + + perform h _ _ a = case a of + Init _ _ -> do + return () + Pay w v -> do + Trace.callEndpoint @"pay-escrow" (h $ WalletKey w) (Ada.adaValueOf $ fromInteger v) + delay 1 + Redeem w -> do + Trace.callEndpoint @"redeem-escrow" (h $ WalletKey w) () + delay 1 + Refund w -> do + Trace.callEndpoint @"refund-escrow" (h $ WalletKey w) () + delay 1 + + arbitraryAction s + | s ^.contractState . phase == Initial + = Init <$> (Slot . getPositive <$> scale (*10) arbitrary) <*> arbitraryTargets + | otherwise + = frequency $ [ (3, Pay <$> elements testWallets <*> choose (1, 30)) ] ++ + [ (1, Redeem <$> elements testWallets) + | (s ^. contractState . contributions . to fold) `geq` (s ^. contractState . targets . to fold) + ] ++ + [ (1, Refund <$> elements testWallets) ] + + + shrinkAction _ (Init s tgts) = map (Init s) (shrinkList (\(w,n)->(w,)<$>shrink n) tgts) + ++ map (`Init` tgts) (map Slot . shrink . getSlot $ s) + shrinkAction _ (Pay w n) = [Pay w n' | n' <- shrink n] + shrinkAction _ _ = [] + +arbitraryTargets :: Gen [(Wallet,Integer)] +arbitraryTargets = do + ws <- sublistOf testWallets + vs <- infiniteListOf $ choose (1,30) + return $ zip ws vs + +testWallets :: [Wallet] +testWallets = [w1, w2, w3, w4, w5] + +testContract :: EscrowParams Datum -> Contract () EscrowSchema EscrowError () +testContract params = selectList [ void $ payEp params + , void $ redeemEp params + , void $ refundEp params + ] >> testContract params + + +prop_Escrow :: Actions EscrowModel -> Property +prop_Escrow = propRunActions_ + +{- START escrowParams -} +escrowParams :: Slot -> [(Wallet, Integer)] -> EscrowParams d +escrowParams s tgts = escrowParams' s [(w, Ada.adaValueOf (fromInteger n)) | (w,n) <- tgts] + +escrowParams' :: Slot -> [(Wallet,Value)] -> EscrowParams d +escrowParams' s tgts' = + EscrowParams + { escrowTargets = [ payToPaymentPubKeyTarget (mockWalletPaymentPubKeyHash w) v | (w,v) <- tgts' ] + , escrowDeadline = scSlotZeroTime def + POSIXTime (getSlot s * scSlotLength def) + } +{- END escrowParams -} +{- +{- START betterEscrowParams -} +escrowParams' :: Slot -> [(Wallet,Value)] -> EscrowParams d +escrowParams' s tgts' = + EscrowParams + { escrowTargets = [ payToPaymentPubKeyTarget (mockWalletPaymentPubKeyHash w) v + | (w,v) <- sortBy (compare `on` fst) tgts' ] -- NEW!! + , escrowDeadline = scSlotZeroTime def + POSIXTime (getSlot s * scSlotLength def) + } +{- END betterEscrowParams -} +-} +finishEscrow :: DL EscrowModel () +finishEscrow = do + anyActions_ + finishingStrategy + assertModel "Locked funds are not zero" (symIsZero . lockedValue) + +finishingStrategy :: DL EscrowModel () +finishingStrategy = do + contribs <- viewContractState contributions + monitor (tabulate "Refunded wallets" [show . Map.size $ contribs]) + phase <- viewContractState phase + monitor $ tabulate "Phase" [show phase] + waitUntilDeadline + sequence_ [action $ Refund w | w <- testWallets, w `Map.member` contribs] + +walletStrategy :: Wallet -> DL EscrowModel () +walletStrategy w = do + contribs <- viewContractState contributions + --waitUntilDeadline + when (w `Map.member` contribs) $ do + action $ Refund w + +waitUntilDeadline :: DL EscrowModel () +waitUntilDeadline = do + deadline <- viewContractState refundSlot + slot <- viewModelState currentSlot + when (slot < deadline) $ waitUntilDL deadline + +noLockProof :: NoLockedFundsProof EscrowModel +noLockProof = defaultNLFP + { nlfpMainStrategy = finishingStrategy + , nlfpWalletStrategy = walletStrategy } + +prop_FinishEscrow :: Property +prop_FinishEscrow = forAllDL finishEscrow prop_Escrow + +prop_FinishFast :: Property +prop_FinishFast = forAllDL finishEscrow $ const True + +prop_NoLockedFunds :: Property +prop_NoLockedFunds = checkNoLockedFundsProof noLockProof + +prop_NoLockedFundsFast :: Property +prop_NoLockedFundsFast = checkNoLockedFundsProofFast noLockProof + +{- START CrashTolerance -} +instance CrashTolerance EscrowModel where + available (Init _ _) _ = True + available a alive = (Key $ WalletKey w) `elem` alive + where w = case a of + Pay w _ -> w + Redeem w -> w + Refund w -> w + Init _ _ -> undefined + + restartArguments s WalletKey{} = escrowParams' slot tgts + where slot = s ^. contractState . refundSlot + tgts = Map.toList (s ^. contractState . targets) +{- END CrashTolerance -} + +{- START prop_CrashTolerance -} +prop_CrashTolerance :: Actions (WithCrashTolerance EscrowModel) -> Property +prop_CrashTolerance = propRunActions_ +{- END prop_CrashTolerance -} + +check_propEscrowWithCoverage :: IO () +check_propEscrowWithCoverage = do + cr <- quickCheckWithCoverage stdArgs (set coverageIndex covIdx $ defaultCoverageOptions) $ \covopts -> + withMaxSuccess 1000 $ propRunActionsWithOptions @EscrowModel defaultCheckOptionsContractModel covopts (const (pure True)) + writeCoverageReport "Escrow" covIdx cr diff --git a/doc/plutus/tutorials/EscrowImpl.hs b/doc/plutus/tutorials/EscrowImpl.hs new file mode 100644 index 0000000000..7ca6c98317 --- /dev/null +++ b/doc/plutus/tutorials/EscrowImpl.hs @@ -0,0 +1,373 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fplugin-opt PlutusTx.Plugin:debug-context #-} +{- START OPTIONS_GHC -} +{-# OPTIONS_GHC -g -fplugin-opt PlutusTx.Plugin:coverage-all #-} +{- END OPTIONS_GHC -} +-- | A general-purpose escrow contract in Plutus +module EscrowImpl( + -- $escrow + Escrow + , EscrowError(..) + , AsEscrowError(..) + , EscrowParams(..) + , EscrowTarget(..) + , payToScriptTarget + , payToPaymentPubKeyTarget + , targetTotal + , escrowContract + , payRedeemRefund + , typedValidator + -- * Actions + , pay + , payEp + , redeem + , redeemEp + , refund + , refundEp + , RedeemFailReason(..) + , RedeemSuccess(..) + , RefundSuccess(..) + , EscrowSchema + -- * Exposed for test endpoints + , Action(..) + -- * Coverage + , covIdx + ) where + +import Control.Lens (makeClassyPrisms, review, view) +import Control.Monad (void) +import Control.Monad.Error.Lens (throwing) +import Data.Aeson (FromJSON, ToJSON) +import GHC.Generics (Generic) + +import Ledger (Datum (..), DatumHash, POSIXTime, PaymentPubKeyHash (unPaymentPubKeyHash), TxId, ValidatorHash, + getCardanoTxId, interval, scriptOutputsAt, txSignedBy, valuePaidTo) +import Ledger qualified +import Ledger.Constraints (TxConstraints) +import Ledger.Constraints qualified as Constraints +import Ledger.Contexts (ScriptContext (..), TxInfo (..)) +import Ledger.Interval (after, before, from) +import Ledger.Interval qualified as Interval +import Ledger.Tx qualified as Tx +import Ledger.Typed.Scripts (TypedValidator) +import Ledger.Typed.Scripts qualified as Scripts +import Ledger.Value (Value, geq, lt) + +import Plutus.Contract +import Plutus.Contract.Typed.Tx qualified as Typed +import PlutusTx qualified +{- START imports -} +import PlutusTx.Code +import PlutusTx.Coverage +{- END imports -} +import PlutusTx.Prelude hiding (Applicative (..), Semigroup (..), check, foldMap) + +import Prelude (Semigroup (..), foldMap) +import Prelude qualified as Haskell + +type EscrowSchema = + Endpoint "pay-escrow" Value + .\/ Endpoint "redeem-escrow" () + .\/ Endpoint "refund-escrow" () + +data RedeemFailReason = DeadlinePassed | NotEnoughFundsAtAddress + deriving stock (Haskell.Eq, Haskell.Show, Generic) + deriving anyclass (ToJSON, FromJSON) + +data EscrowError = + RedeemFailed RedeemFailReason + | RefundFailed + | EContractError ContractError + deriving stock (Haskell.Show, Generic) + deriving anyclass (ToJSON, FromJSON) + +makeClassyPrisms ''EscrowError + +instance AsContractError EscrowError where + _ContractError = _EContractError + +-- $escrow +-- The escrow contract implements the exchange of value between multiple +-- parties. It is defined by a list of targets (public keys and script +-- addresses, each associated with a value). It works similar to the +-- crowdfunding contract in that the contributions can be made independently, +-- and the funds can be unlocked only by a transaction that pays the correct +-- amount to each target. A refund is possible if the outputs locked by the +-- contract have not been spent by the deadline. (Compared to the crowdfunding +-- contract, the refund policy is simpler because here because there is no +-- "collection period" during which the outputs may be spent after the deadline +-- has passed. This is because we're assuming that the participants in the +-- escrow contract will make their deposits as quickly as possible after +-- agreeing on a deal) +-- +-- The contract supports two modes of operation, manual and automatic. In +-- manual mode, all actions are driven by endpoints that exposed via 'payEp' +-- 'redeemEp' and 'refundEp'. In automatic mode, the 'pay', 'redeem' and +-- 'refund'actions start immediately. This mode is useful when the escrow is +-- called from within another contract, for example during setup (collection of +-- the initial deposits). + +-- | Defines where the money should go. Usually we have `d = Datum` (when +-- defining `EscrowTarget` values in off-chain code). Sometimes we have +-- `d = DatumHash` (when checking the hashes in on-chain code) +data EscrowTarget d = + PaymentPubKeyTarget PaymentPubKeyHash Value + | ScriptTarget ValidatorHash d Value + deriving (Haskell.Functor) + +PlutusTx.makeLift ''EscrowTarget + +-- | An 'EscrowTarget' that pays the value to a public key address. +payToPaymentPubKeyTarget :: PaymentPubKeyHash -> Value -> EscrowTarget d +payToPaymentPubKeyTarget = PaymentPubKeyTarget + +-- | An 'EscrowTarget' that pays the value to a script address, with the +-- given data script. +payToScriptTarget :: ValidatorHash -> Datum -> Value -> EscrowTarget Datum +payToScriptTarget = ScriptTarget + +-- | Definition of an escrow contract, consisting of a deadline and a list of targets +data EscrowParams d = + EscrowParams + { escrowDeadline :: POSIXTime + -- ^ Latest point at which the outputs may be spent. + , escrowTargets :: [EscrowTarget d] + -- ^ Where the money should go. For each target, the contract checks that + -- the output 'mkTxOutput' of the target is present in the spending + -- transaction. + } deriving (Haskell.Functor) + +PlutusTx.makeLift ''EscrowParams + +-- | The total 'Value' that must be paid into the escrow contract +-- before it can be unlocked +targetTotal :: EscrowParams d -> Value +targetTotal = foldl (\vl tgt -> vl + targetValue tgt) mempty . escrowTargets + +-- | The 'Value' specified by an 'EscrowTarget' +targetValue :: EscrowTarget d -> Value +targetValue = \case + PaymentPubKeyTarget _ vl -> vl + ScriptTarget _ _ vl -> vl + +-- | Create a 'Ledger.TxOut' value for the target +mkTx :: EscrowTarget Datum -> TxConstraints Action PaymentPubKeyHash +mkTx = \case + PaymentPubKeyTarget pkh vl -> + Constraints.mustPayToPubKey pkh vl + ScriptTarget vs ds vl -> + Constraints.mustPayToOtherScript vs ds vl + +data Action = Redeem | Refund + +data Escrow +instance Scripts.ValidatorTypes Escrow where + type instance RedeemerType Escrow = Action + type instance DatumType Escrow = PaymentPubKeyHash + +PlutusTx.unstableMakeIsData ''Action +PlutusTx.makeLift ''Action + +{-# INLINABLE meetsTarget #-} +-- | @ptx `meetsTarget` tgt@ if @ptx@ pays at least @targetValue tgt@ to the +-- target address. +-- +-- The reason why this does not require the target amount to be equal +-- to the actual amount is to enable any excess funds consumed by the +-- spending transaction to be paid to target addresses. This may happen if +-- the target address is also used as a change address for the spending +-- transaction, and allowing the target to be exceed prevents outsiders from +-- poisoning the contract by adding arbitrary outputs to the script address. +meetsTarget :: TxInfo -> EscrowTarget DatumHash -> Bool +meetsTarget ptx = \case + PaymentPubKeyTarget pkh vl -> + valuePaidTo ptx (unPaymentPubKeyHash pkh) `geq` vl + ScriptTarget validatorHash dataValue vl -> + case scriptOutputsAt validatorHash ptx of + [(dataValue', vl')] -> + traceIfFalse "dataValue" (dataValue' == dataValue) + && traceIfFalse "value" (vl' `geq` vl) + _ -> False + +{-# INLINABLE validate #-} +validate :: EscrowParams DatumHash -> PaymentPubKeyHash -> Action -> ScriptContext -> Bool +validate EscrowParams{escrowDeadline, escrowTargets} contributor action ScriptContext{scriptContextTxInfo} = + case action of + Redeem -> + traceIfFalse "escrowDeadline-after" (escrowDeadline `after` txInfoValidRange scriptContextTxInfo) + && traceIfFalse "meetsTarget" (all (meetsTarget scriptContextTxInfo) escrowTargets) + Refund -> + traceIfFalse "escrowDeadline-before" ((escrowDeadline - 1) `before` txInfoValidRange scriptContextTxInfo) + && traceIfFalse "txSignedBy" (scriptContextTxInfo `txSignedBy` unPaymentPubKeyHash contributor) + +{- START typedValidator -} +typedValidator :: EscrowParams Datum -> Scripts.TypedValidator Escrow +typedValidator escrow = go (Haskell.fmap Ledger.datumHash escrow) where + go = Scripts.mkTypedValidatorParam @Escrow + $$(PlutusTx.compile [|| validate ||]) + $$(PlutusTx.compile [|| wrap ||]) + wrap = Scripts.wrapValidator +{- END typedValidator -} +escrowContract + :: EscrowParams Datum + -> Contract () EscrowSchema EscrowError () +escrowContract escrow = + let inst = typedValidator escrow + payAndRefund = endpoint @"pay-escrow" $ \vl -> do + _ <- pay inst escrow vl + _ <- awaitTime $ escrowDeadline escrow + refund inst escrow + in selectList + [ void payAndRefund + , void $ redeemEp escrow + ] + +-- | 'pay' with an endpoint that gets the owner's public key and the +-- contribution. +payEp :: + forall w s e. + ( HasEndpoint "pay-escrow" Value s + , AsEscrowError e + ) + => EscrowParams Datum + -> Promise w s e TxId +payEp escrow = promiseMap + (mapError (review _EContractError)) + (endpoint @"pay-escrow" $ pay (typedValidator escrow) escrow) + +-- | Pay some money into the escrow contract. +pay :: + forall w s e. + ( AsContractError e + ) + => TypedValidator Escrow + -- ^ The instance + -> EscrowParams Datum + -- ^ The escrow contract + -> Value + -- ^ How much money to pay in + -> Contract w s e TxId +pay inst escrow vl = do + pk <- ownPaymentPubKeyHash + let tx = Constraints.mustPayToTheScript pk vl + <> Constraints.mustValidateIn (Ledger.interval 1 (escrowDeadline escrow)) + utx <- mkTxConstraints (Constraints.typedValidatorLookups inst) tx + getCardanoTxId <$> submitUnbalancedTx (Constraints.adjustUnbalancedTx utx) + +newtype RedeemSuccess = RedeemSuccess TxId + deriving (Haskell.Eq, Haskell.Show) + +-- | 'redeem' with an endpoint. +redeemEp :: + forall w s e. + ( HasEndpoint "redeem-escrow" () s + , AsEscrowError e + ) + => EscrowParams Datum + -> Promise w s e RedeemSuccess +redeemEp escrow = promiseMap + (mapError (review _EscrowError)) + (endpoint @"redeem-escrow" $ \() -> redeem (typedValidator escrow) escrow) + +-- | Redeem all outputs at the contract address using a transaction that +-- has all the outputs defined in the contract's list of targets. +redeem :: + forall w s e. + ( AsEscrowError e + ) + => TypedValidator Escrow + -> EscrowParams Datum + -> Contract w s e RedeemSuccess +redeem inst escrow = mapError (review _EscrowError) $ do + let addr = Scripts.validatorAddress inst + current <- currentTime + unspentOutputs <- utxosAt addr + let + valRange = Interval.to (Haskell.pred $ escrowDeadline escrow) + tx = Typed.collectFromScript unspentOutputs Redeem + <> foldMap mkTx (escrowTargets escrow) + <> Constraints.mustValidateIn valRange + if current >= escrowDeadline escrow + then throwing _RedeemFailed DeadlinePassed + else if foldMap (view Tx.ciTxOutValue) unspentOutputs `lt` targetTotal escrow + then throwing _RedeemFailed NotEnoughFundsAtAddress + else do + utx <- mkTxConstraints ( Constraints.typedValidatorLookups inst + <> Constraints.unspentOutputs unspentOutputs + ) tx + RedeemSuccess . getCardanoTxId <$> submitUnbalancedTx (Constraints.adjustUnbalancedTx utx) + +newtype RefundSuccess = RefundSuccess TxId + deriving newtype (Haskell.Eq, Haskell.Show, Generic) + deriving anyclass (ToJSON, FromJSON) + +-- | 'refund' with an endpoint. +refundEp :: + forall w s. + ( HasEndpoint "refund-escrow" () s + ) + => EscrowParams Datum + -> Promise w s EscrowError RefundSuccess +refundEp escrow = endpoint @"refund-escrow" $ \() -> refund (typedValidator escrow) escrow + +-- | Claim a refund of the contribution. +refund :: + forall w s. + TypedValidator Escrow + -> EscrowParams Datum + -> Contract w s EscrowError RefundSuccess +refund inst escrow = do + pk <- ownPaymentPubKeyHash + unspentOutputs <- utxosAt (Scripts.validatorAddress inst) + let flt _ ciTxOut = either id Ledger.datumHash (Tx._ciTxOutDatum ciTxOut) == Ledger.datumHash (Datum (PlutusTx.toBuiltinData pk)) + tx' = Typed.collectFromScriptFilter flt unspentOutputs Refund + <> Constraints.mustValidateIn (from (Haskell.succ $ escrowDeadline escrow)) + if Constraints.modifiesUtxoSet tx' + then do + utx <- mkTxConstraints ( Constraints.typedValidatorLookups inst + <> Constraints.unspentOutputs unspentOutputs + ) tx' + RefundSuccess . getCardanoTxId <$> submitUnbalancedTx (Constraints.adjustUnbalancedTx utx) + else throwing _RefundFailed () + +-- | Pay some money into the escrow contract. Then release all funds to their +-- specified targets if enough funds were deposited before the deadline, +-- or reclaim the contribution if the goal has not been met. +payRedeemRefund :: + forall w s. + EscrowParams Datum + -> Value + -> Contract w s EscrowError (Either RefundSuccess RedeemSuccess) +payRedeemRefund params vl = do + let inst = typedValidator params + go = do + cur <- utxosAt (Scripts.validatorAddress inst) + let presentVal = foldMap (view Tx.ciTxOutValue) cur + if presentVal `geq` targetTotal params + then Right <$> redeem inst params + else do + time <- currentTime + if time >= escrowDeadline params + then Left <$> refund inst params + else waitNSlots 1 >> go + -- Pay the value 'vl' into the contract + _ <- pay inst params vl + go + +{- START covIdx -} +covIdx :: CoverageIndex +covIdx = getCovIdx $$(PlutusTx.compile [|| validate ||]) +{- END covIdx -} diff --git a/doc/plutus/tutorials/contract-models.rst b/doc/plutus/tutorials/contract-models.rst new file mode 100644 index 0000000000..063362bee6 --- /dev/null +++ b/doc/plutus/tutorials/contract-models.rst @@ -0,0 +1,3021 @@ +.. highlight:: haskell +.. _contract_models_tutorial: + +Testing Plutus Contracts with Contract Models +============================================= + +Introduction +------------ + +In this tutorial we will see how to test Plutus contracts with +*contract models*, using the framework provided by +:hsmod:`Plutus.Contract.Test.ContractModel`. This framework generates +and runs tests on the Plutus emulator, where each test may involve a +number of emulated wallets, each running a collection of Plutus +contracts, all submitting transactions to an emulated blockchain. +Once the user has defined a suitable model, then QuickCheck can +generate and run many thousands of scenarios, taking the application +through a wide variety of states, and checking that it behaves +correctly in each one. Once the underlying contract model is in place, +then the framework can check user-defined properties specific to the +application, generic properties such as that no funds remain locked in +contracts for ever, and indeed both positive and negative +tests---where positive tests check that the contracts allow the +intended usages, and negative tests check that they do *not* allow +unintended ones. + +The `ContractModel` framework is quite rich in features, but we will +introduce them gradually and explain how they can best be used. + +Basic Contract Models +--------------------- + +Example: A Simple Escrow Contract +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +We begin by showing how to construct a model for a simplified escrow +contract, which can be found in +:hsmod:`Plutus.Contracts.Tutorial.Escrow`. This contract enables a +group of wallets to make a predetermined exchange of tokens, for +example selling an NFT for Ada. There are two endpoints, a ``pay`` +endpoint, and a ``redeem`` endpoint. Each wallet pays in its +contribution to the contract using the ``pay`` endpoint, and once all +the wallets have done so, then any wallet can trigger the +predetermined payout using the ``redeem`` endpoint. + +For simplicity, we will begin by testing the contract for a fixed set +of predetermined payouts. These are defined by the ``EscrowParams``, a +type exported by the escrow contract, and which is actually passed to +the on-chain validators. :hsmod:`Plutus.Contract.Test` provides ten +emulated wallets for use in tests, ``w1`` to ``w10``; in this case we +will use five of them: + +.. literalinclude:: Escrow.hs + :start-after: START testWallets + :end-before: END testWallets + +Let us decide arbitrarily that ``w1`` will receive a payout of 10 Ada, +and ``w2`` will receive a payout of 20, and define an ``EscrowParams`` +value to represent that: + +.. literalinclude:: Escrow.hs + :start-after: START escrowParams + :end-before: END escrowParams + +The Contract Model Type +^^^^^^^^^^^^^^^^^^^^^^^ + +In order to generate sensible tests, and to decide how they should +behave, we need to track the expected state of the system. The first +step in defining a contract model is to define a type to represent +this expected state. We usually need to refine it as the model +evolves, but for now we keep things simple. + +In this case, as wallets make payments into the escrow, we will need +to keep track of how much each wallet has paid in. So let us define an +``EscrowModel`` type that records these contributions. Once the +contributions reach the targets, then the escrow may be redeemed, so +let us keep track of these targets in the model too. We define + +.. literalinclude:: Escrow.hs + :start-after: START EscrowModel + :end-before: END EscrowModel + +Note that we use `lenses
+ 365 covIdx :: CoverageIndex + 366 covIdx = getCovIdx $$(PlutusTx.compile [|| val ++ +we see that it is the construction of the coverage index, and +parts of this code are labelled on-chain and uncovered. We can ignore +this, it's simply an artefact of the way the code labelling is done +(and could be avoided by putting the construction of the ``covIdx`` in a +different module, without coverage enabled). + +More interesting is the second section of the report: + + .. raw:: html + +
+ 201 {-# INLINABLE validate #-} + 202 validate :: EscrowParams DatumHash -> PaymentPubKeyHash -> Action -> ScriptContext -> Bool + 203 validate EscrowParams{escrowDeadline, escrowTargets} contributor action ScriptContext{scriptContextTxInfo} = + 204 case action of + 205 Redeem -> + 206 traceIfFalse "escrowDeadline-after" (escrowDeadline `after` txInfoValidRange scriptContextTxInfo) + 207 && traceIfFalse "meetsTarget" (all (meetsTarget scriptContextTxInfo) escrowTargets) + 208 Refund -> + 209 traceIfFalse "escrowDeadline-before" ((escrowDeadline - 1) `before` txInfoValidRange scriptContextTxInfo) + 210 && traceIfFalse "txSignedBy" (scriptContextTxInfo `txSignedBy` unPaymentPubKeyHash contributor) + 211 ++ +This is the main validator, and while some of its code is coloured +white, much of it is coloured green. This means the checks in this +function always returned ``True`` in our tests; we have not tested the +cases in which they return ``False``. + +This does indicate a weakness in our testing: since these checks +always passed in our tests, then those tests would *also* have passed +if the checks were removed completely (replaced by ``True``)--but the +contract would have been quite wrong. We will return to this point +later, when we discuss *negative testing*. For now, though, we just +note that *if the checks had returned* ``False``, *then the +transaction would have failed*--and the off-chain code is, of course, +designed not to submit failing transactions. So, in a sense, we should +expect this code to be coloured green--at least, when we test through +well-designed off-chain endpoints, as we have been doing. + +This code fragment also contains some entirely uncovered code--the +strings passed to ``traceIfFalse`` to be used as error messages if a +check fails. Since correct off-chain code never submits failing +transactions, then these error messages are never used--and hence the +code is labelled as 'uncovered'. Again, this is not really a problem. + +The most interesting part of the report is the first section: + + .. raw:: html + +
+ 190 meetsTarget :: TxInfo -> EscrowTarget DatumHash -> Bool + 191 meetsTarget ptx = \case + 192 PaymentPubKeyTarget pkh vl -> + 193 valuePaidTo ptx (unPaymentPubKeyHash pkh) `geq` vl + 194 ScriptTarget validatorHash dataValue vl -> + 195 case scriptOutputsAt validatorHash ptx of + 196 [(dataValue', vl')] -> + 197 traceIfFalse "dataValue" (dataValue' == dataValue) + 198 && traceIfFalse "value" (vl' `geq` vl) + 199 _ -> False ++ +This is the function that is used to check that each target payment is +made when the escrow is redeemed, and as we see from the coverage +report, there are two cases, of which only one has been tested. In +fact the two cases handle payments to a wallet, and payments to a +script, and the second kind of payment is *not tested at all* by our +tests--yet it is handled by entirely different code in the on-chain +function. + +**This exposes a serious deficiency in the tests developed so far**: +they give us no evidence at all that target payments to a script work +as intended. To test this code as well, we would need to add 'proxy' +contracts to the tests, to act as recipients for such payments. We +leave making this extension as an exercise for the reader. + +.. _CoverageReport: + +The generated coverage report +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +This is the generated coverage report in its entirety: + + .. raw:: html + :file: Escrow.html + +Crashes, and how to tolerate them +--------------------------------- + +One awkward possibility, that we cannot avoid, is that a contract +instance might crash during execution--for example, because of a power +failure to the machine it is running on. We don't want anything to be +lost permanently as a result--it should be possible to recover by +restarting the contract instance, perhaps in a different state, and +continue. Yet how should we test this? We need to deliberately crash +and restart contracts in tests, and check that they still behave as +the model says they should. + +The ``ContractModel`` framework provides a simple way to *extend* a +contract model, so that it can test crash-tolerance too. If ``m`` is a +``ContractModel`` instance, then so is ``WithCrashTolerance m``--and +testing the latter model will insert actions to crash and restart +contract instances at random. To define a property that runs these +tests, all we have to do is include ``WithCrashTolerance`` in the type +signature: + + .. literalinclude:: Escrow6.hs + :start-after: START prop_CrashTolerance + :end-before: END prop_CrashTolerance + +(The actual code here is the same as ``prop_Escrow``, only the type is different). + +We do have to provide a little more information before we can run +tests, though. + +#. Firstly, we cannot expect to include an action in a + test, when the contract(s) that should perform the action are not + running. We thus need to tell the framework whether or not an action + is *available*, given the contracts currently running. + +#. Secondly, when we restart a contract it may need to take some + recovery action, and so we must be able to give it the necessary + information to recover. We achieve this by specifying + possibly-different contract parameters to use, when a contract is + restarted. These parameters may depend on the model state. + +We provide this information by defining an instance of the +``CrashTolerance`` class: + + .. literalinclude:: Escrow6.hs + :start-after: START CrashTolerance + :end-before: END CrashTolerance + +The ``available`` method returns ``True`` if an action is available, +given a list of active contract keys ``alive``; since contract +instance keys have varying types, then the list actually contains keys +wrapped in an existential type, which is why the ``Key`` constructor +appears there. + +The ``restartArguments`` method provides the parameter for restarting +an escrow contract, which in this case can be just the same as when +the contract was first started. We need to recover the targets from +the model state, in which they are represented as a ``Map Wallet +Value``, so we convert them back to a list and refactor the +``escrowParams`` function so we can give ``escrowParams'`` a list of +``(Wallet,Value)`` pairs, rather than a list of ``(Wallet,Int)``: + + .. literalinclude:: Escrow6.hs + :start-after: START escrowParams + :end-before: END escrowParams + +It is possible to define the effect of crashing or restarting a +contract instance on the *model* too, if need be, by defining +additional methods in this class. In this case, though, crashing and +restarting ought to be entirely transparent, so we can omit them. + +Surprisingly, the tests do not pass! + + .. code-block:: text + + > quickCheck prop_CrashTolerance + *** Failed! Assertion failed (after 24 tests and 26 shrinks): + Actions + [Init (Slot {getSlot = 6}) [(Wallet 1,2),(Wallet 4,2)], + Crash (WalletKey (Wallet 4)), + Restart (WalletKey (Wallet 4)), + Pay (Wallet 4) 4, + Redeem (Wallet 1)] + Expected funds of W[4] to change by + Value (Map [(,Map [("",-2000000)])]) + but they changed by + Value (Map [(,Map [("",-4000000)])]) + a discrepancy of + Value (Map [(,Map [("",-2000000)])]) + Expected funds of W[1] to change by + Value (Map [(,Map [("",2000000)])]) + but they did not change + Contract instance log failed to validate: + ... + Slot 5: 00000000-0000-4000-8000-000000000000 {Wallet W[1]}: + Contract instance stopped with error: RedeemFailed NotEnoughFundsAtAddress + ... + +Here we simply set up targets with two beneficiaries, crash and +restart wallet 4, pay sufficient contributions to cover the targets, +and then try to redeem the escrow, which seems straightforward enough, +and yet the redemption thinks there are not enough funds in the +escrow, *even though we just paid them in*! + +This failure is a little tricky to debug. A clue is that the *payment* +was made by a contract instance that has been restarted, while the +*redemption* was made by a contract that has not. Do the payment and +redemption actually refer to the same escrow? In fact the targets +supplied to the contract instance are not necessarily exactly the +same: the contract receives a *list* of targets, but in the model we +represented them as a *map*--and converted the list of targets to a +map, and back again, when we restarted the contract. That means the +*order* of the targets might be different. + +Could that make a difference? To find out, we can just *sort* the +targets before passing them to the contract instance, thus +guaranteeing the same order every time: + + .. literalinclude:: Escrow6.hs + :start-after: START betterEscrowParams + :end-before: END betterEscrowParams + +Once we do this, the tests pass. We can also see from the resulting +statistics that quite a lot of crashing and restarting is going on: + + .. code-block:: text + + > quickCheck prop_CrashTolerance + +++ OK, passed 100 tests. + + Actions (2721 in total): + 42.48% Pay + 24.99% WaitUntil + 13.08% Crash + 9.52% Restart + 6.06% Redeem + 3.01% Init + 0.85% Refund + +Perhaps it's debatable whether or not the behaviour we uncovered here +is a *bug*, but it is certainly a feature--it was not obvious in +advance that specifying the same targets in a different order would +create an independent escrow, but that is what happens. So for +example, if a buyer and seller using an escrow contract to exchange an +NFT for Ada specify the two targets in different orders, then they +would place their assets in independent escrow that cannot be redeemed +until the refund deadline passes. Arguably a better designed contract +would sort the targets by wallet, as we have done here, before +creating any UTXOs, so that the problem cannot arise. + +Exercises +^^^^^^^^^ + +You will find the code discussed here in ``Spec.Tutorial.Escrow6``, *without* the addition of ``sortBy`` to ``escrowParams``. + +#. Run ``quickCheck prop_CrashTolerance`` to provoke a test + failure. Examine the counterexample and the test output, and make + sure you understand how the test fails. Run this test several + times: you will see the failure in several different forms, with + the same underlying cause. Make sure you understand how each + failure arises. + + Why does ``quickCheck`` always report a test case with *two* target + payments--why isn't one target enough to reveal the problem? + +#. Add sorting to the model, and verify that the tests now pass. + +#. An alternative way to fix the model is *not* to convert the targets + to a ``Map`` in the model state, but just keep them as a list of + pairs, so that exactly the same list can be supplied to the + contract instances when they are restarted. Implement this change, + and verify that the tests still pass. + + Which solution do you prefer? Arguably this one reflects the + *actual* design of the contract more closely, since the model makes + explicit that the order of the targets matters. + + +Debugging the Auction contract with model assertions +---------------------------------------------------- + +In this section, we'll apply the techniques we have seen so far to +test another contract, and we'll see how they reveal some surprising +behaviour. The contract we take this time is the auction contract in +``Plutus.Contracts.Auction``. This module actually defines *two* +contracts, a seller contract and a buyer contract. The seller puts up +a ``Value`` for sale, creating an auction UTXO containing the value, +and buyers can then bid Ada for it. When the auction deadline is +reached, the highest bidder receives the auctioned value, and the +seller receives the bid. + +Modelling the Auction contract +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +``Spec.Auction`` contains a contract model for testing this +contract. The value for sale is a custom token, wallet 1 is the +seller, and the deadline used for testing is fixed at slot 101; the +generated tests just consist of an ``Init`` action to start the +auction, and a series of ``Bid`` actions by the other wallets. + + .. literalinclude:: Auction.hs + :start-after: START Action + :end-before: END Action + +The model keeps track of the highest bid and bidder, and the current +phase the auction is in: + + .. literalinclude:: Auction.hs + :start-after: START model + :end-before: END model + +It is updated by the ``nextState`` method on each bid: + + .. literalinclude:: Auction.hs + :start-after: START nextState + :end-before: END nextState + +Note that when a higher bid is received, the previous bid is returned +to the bidder. + +We only allow bids that are larger than the previous one (which is why +``nextState`` doesn't need to check this): + + .. literalinclude:: Auction.hs + :start-after: START precondition + :end-before: END precondition + +The most interesting part of the model covers what happens when the +auction deadline is reached: in contrast to the ``Escrow`` contract, +the highest bid is paid to the seller automatically, and the buyer +receives the token. We model this using the ``nextReactiveState`` +method introduced in section :ref:`Timing` + + .. literalinclude:: Auction.hs + :start-after: START nextReactiveState + :end-before: END nextReactiveState + +Finally we can define the property to test; in this case we have to +supply some options to initialize wallet 1 with the token to be +auctioned: + + .. literalinclude:: Auction.hs + :start-after: START prop_Auction + :end-before: END prop_Auction + +The only important part here is ``options``, which is defined as follows: + + .. literalinclude:: Auction.hs + :start-after: START options + :end-before: END options + +Unsurprisingly, the tests pass. + + .. code-block:: text + + > quickCheck prop_Auction + +++ OK, passed 100 tests. + + Actions (2348 in total): + 85.82% Bid + 10.35% WaitUntil + 3.83% Init + +No locked funds? +^^^^^^^^^^^^^^^^ + +Now we have a basic working model of the auction contract, we can +begin to test more subtle properties. To begin with, can we recover +the funds held by the contract? The strategy to try is obvious: all we +have to do is wait for the deadline to pass. So ``prop_FinishAuction`` +is very simple: + + .. literalinclude:: Auction.hs + :start-after: START prop_FinishAuction + :end-before: END prop_FinishAuction + +This property passes too: + + .. code-block:: text + + > quickCheck prop_FinishAuction + +++ OK, passed 100 tests. + + Actions (3152 in total): + 84.77% Bid + 12.25% WaitUntil + 2.98% Init + +Now, to supply a ``NoLockedFundsProof`` we need a general strategy for +fund recovery, and a wallet-specific one. Since all we have to do is +wait, we can use the *same* strategy as both. + + .. literalinclude:: Auction.hs + :start-after: START noLockProof + :end-before: END noLockProof + +Surprisingly, *these tests fail*! + + .. code-block:: text + + > quickCheck prop_NoLockedFunds + *** Failed! Assertion failed (after 2 tests and 1 shrink): + DLScript + [Do $ Init, + Do $ Bid (Wallet 3) 2000000] + + The ContractModel's Unilateral behaviour for Wallet 3 does not match the + actual behaviour for actions: + Actions + [Var 0 := Init, + Var 1 := Bid (Wallet 3) 2000000, + Var 2 := Unilateral (Wallet 3), + Var 3 := WaitUntil (Slot {getSlot = 101})] + Expected funds of W[1] to change by + Value (Map [(363d...,Map [("token",-1)])]) + but they changed by + Value (Map [(,Map [("",-2000000)]),(363d...,Map [("token",-1)])]) + a discrepancy of + Value (Map [(,Map [("",-2000000)])]) + Expected funds of W[3] to change by + Value (Map [(363d...,Map [("token",1)])]) + but they changed by + Value (Map [(,Map [("",-2000000)])]) + a discrepancy of + Value (Map [(,Map [("",-2000000)]),(363d...,Map [("token",-1)])]) + Test failed. + +This test just started the auction and submitted a bid from wallet 3, +then *stopped all the other wallets* (this is what ``Unilateral +(Wallet 3)`` does), before waiting until the auction deadline. This +resulted in a different distribution of funds from the one the model +predicts. Looking at the last part of the message, we see that we +expected wallet 3 to get the token, *but it did not*; neither did it +get its bid back. Wallet 1 did lose the token, though, and in addition +lost the 2 Ada required to create the auction UTXO in the first place. + +What is going on? The strategy worked in the general case, but failed +in the unilateral case, which tells us that *the buyer requires the +cooperation of the seller* in order to recover the auctioned +token. Why? Well, our description of the contract above was a little +misleading: the proceeds of the auction *cannot* be paid out +automatically just because the deadline passes; the Cardano blockchain +won't do that. Instead, *someone must submit the payout +transaction*. In the case of this contract, it's the seller: even +though there is no *endpoint call* at the deadline, the seller's +off-chain code continues running throughout the auction, and when the +deadline comes it submits the payout transaction. So if the seller's +contract is stopped, then no payout occurs. + +This is not a *very* serious bug, because the *on-chain* code allows +anyone to submit the payout transaction, so the buyer could in +principle do so. However, the existing off-chain code does not provide +an endpoint for this, and so recovering the locked funds would require +writing a new version of the off-chain code (or rolling a suitable +transaction by hand). + + .. _AuctionAssertion: + +Model assertions, and unexpected expectations. +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +Looking back at the failed test again, the *expected* wallet contents +are actually a little *unexpected*: + + .. code-block:: text + + Actions + [Var 0 := Init, + Var 1 := Bid (Wallet 3) 2000000, + Var 2 := Unilateral (Wallet 3), + Var 3 := WaitUntil (Slot {getSlot = 101})] + Expected funds of W[1] to change by + Value (Map [(363d...,Map [("token",-1)])]) + but they changed by + Value (Map [(,Map [("",-2000000)]),(363d...,Map [("token",-1)])]) + a discrepancy of + Value (Map [(,Map [("",-2000000)])]) + +Notice that, even though wallet 3 made a bid of 2 Ada, we *expected* +the seller to end up without the token, but *with no extra +money*. Wouldn't we expect the seller to end up with 2 Ada? + +Because ``prop_Auction`` passed, then we know that in the absence of a +``Unilateral`` then the model and the contract implementation agree on +fund transfers. But does the model actually predict that the seller +gets the winning bid? This can be a little hard to infer from the +state transitions themselves; we can check that each action appears to +do the right thing, but whether the end result is as expected is not +necessarily immediately obvious. + +We can address this kind of problem by *adding assertions to the +model*. The model tracks the change in each wallet's balance since the +beginning of the test, so we can add an assertion, at the point where +the auction ends, that checks that the seller loses the token and +gains the winning bid. We just a little code to ``nextReactiveState``: + + .. literalinclude:: Auction.hs + :start-after: START extendedNextReactiveState + :end-before: END extendedNextReactiveState + +If the boolean passed to ``assertSpec`` is ``False``, then the test +fails with the first argument in the error message. + + .. note:: + + We do have to allow for the possibility that the auction never + started, which is why we include in the assertion the possibility + that wallet 1's balance remains unchanged. Without this, the tests + fail. + +Now ``prop_Auction`` fails! + + .. code-block:: text + + > quickCheck prop_Auction + *** Failed! Falsified (after 27 tests and 24 shrinks): + Actions + [Init, + Bid (Wallet 3) 2000000, + WaitUntil (Slot {getSlot = 100})] + assertSpec failed: w1 final balance is wrong: + SymValue {symValMap = fromList [], actualValPart = Value (Map [(363d...,Map [("token",-1)])])} + + .. note:: + + The balance change is actually a ``SymValue``, not a ``Value``, + but as you can see it *contains* a ``Value``, which is all we care + about right now. We will return to the purpose of the + ``symValMap`` in a later section. + +Even in this simple case, the seller does not receive the right +amount: wallet 1 lost the token, but received no payment! + +The reason has to do with the minimum Ada in each UTXO. When the +auction UTXO is created, the seller has to put in 2 Ada along with the +token. When the auction ends, one might expect that 2 Ada to be +returned to the seller. But it can't be: *it is needed to create the +UTXO that delivers the token to the buyer*! Thus the seller receives 2 +Ada (from the buyer's bid) in this example, but this only makes up for +the 2 Ada deposited in the auction UTXO, and the seller ends up giving +away the token for nothing. + +This is quite surprising behaviour, and arguably, the contract should +require that the buyer pay the seller 2 Ada *plus* the winning bid, so that +the stated bid is equal to the seller's net receipts. + + .. note:: + + Model assertions can be tested without running the emulator, by + using ``propSanityCheckAssertions`` instead of + ``propRunActions_``. This is very much faster, and enables very + thorough testing of the model. Since other tests check that the + implementation correponds to the model, then this still gives us + valuable information about the implementation. + +Crashing the auction +^^^^^^^^^^^^^^^^^^^^ + +Is the auction crash tolerant? To find out, we just declare that +``Bid`` actions are available when the corresponding buyer contract is +running, define the restart arguments, and the crash-tolerant property +(which just replicates the definition of ``prop_Auction`` with a +different type). + + .. literalinclude:: Auction.hs + :start-after: START crashTolerance + :end-before: END crashTolerance + +Perhaps unsurprisingly, this property fails: + + .. code-block:: text + + > quickCheck prop_CrashTolerance + *** Failed! Assertion failed (after 17 tests and 11 shrinks): + Actions + [Init, + Crash SellerH, + WaitUntil (Slot {getSlot = 100})] + Expected funds of W[1] to change by + Value (Map []) + but they changed by + Value (Map [(,Map [("",-2000000)]),(363d3944282b3d16b239235a112c0f6e2f1195de5067f61c0dfc0f5f,Map [("token",-1)])]) + a discrepancy of + Value (Map [(,Map [("",-2000000)]),(363d3944282b3d16b239235a112c0f6e2f1195de5067f61c0dfc0f5f,Map [("token",-1)])]) + Test failed. + +We already know that the auction payout is initiated by the seller +contract, so if that contract is not running, then no payout takes +place. (Although there are no bids in this counterexample, a payout is +still needed--to return the token to the seller). That is why this test fails. + +But this is actually not the only way the property can fail. The other +failure (which generates some rather long contract logs) looks like +this: + + .. code-block:: text + + > quickCheck prop_CrashTolerance + *** Failed! Assertion failed (after 13 tests and 9 shrinks): + Actions + [Init, + Crash SellerH, + Restart SellerH] + Contract instance log failed to validate: + ... half a megabyte of output ... + Slot 6: 00000000-0000-4000-8000-000000000004 {Wallet W[1]}: + Contract instance stopped with error: StateMachineContractError (SMCContractError (WalletContractError (InsufficientFunds "Total: Value (Map [(,Map [(\"\",9999999997645750)])]) expected: Value (Map [(363d3944282b3d16b239235a112c0f6e2f1195de5067f61c0dfc0f5f,Map [(\"token\",1)])])"))) + Test failed. + +In other words, after a crash, *the seller contract fails to +restart*. This is simply because the seller tries to put the token up +for auction when it starts, and *wallet 1 no longer holds the +token*--it is already in an auction UTXO on the blockchain. So the +seller contract fails with an ``InsufficientFunds`` error. To continue +the auction, we would really need another endpoint to resume the +seller, which the contract does not provide, or a parameter to the +seller contract which specifies whether to start or continue an +auction. + +Coverage of the Auction contract +^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + +We can generate a coverage report for the ``Auction`` contract just as +we did for the ``Escrow`` one. The interesting part of the report is: + + .. raw:: html + :file: Auction.html + +The auction is defined as a Plutus state machine, which just repeats +an ``auctionTransition`` over and over again. We can see that the +state machine itself, and most of the transition code, is +covered. However, the ``Bid`` transition has only been tested in the +case where new bid is higher than the old one. Indeed, the tests are +designed to respect that precondition. Moroever, the last clause in +the ``case`` expression has not been tested at all--but this is quite +OK, because it returns ``Nothing`` which the state machine library +interprets to mean "reject the transaction". So the uncovered code +*could* only be covered by failing transactions, which the off-chain +code is designed not to submit. + +Exercises +^^^^^^^^^ + +The code discussed here is in ``Spec.Auction``. + +#. Test the failing properties (``prop_NoLockedFunds`` and + ``prop_CrashTolerance``) and observe the failures. + +#. Add the model assertion discussed in :ref:`AuctionAssertion` to the + code, and ``quickCheck prop_SanityCheckAssertions`` to verify that + it fails. Change the assertion to say that the seller receives 2 + Ada *less* than the bid, and verify that it now passes. + +Becoming Level 1 Certification Ready +------------------------------------ + +Level 1 certification of plutus smart contracts relies on the machinery +we have discussed in this tutorial. First things first we are going to +have a look at the :hsmod:`Plutus.Contract.Test.Certification` module. + +This module defines a type ``Certification`` paramtereized over a type +``m`` that should be a ``ContractModel``. This is a record type that has +fields for: + +#. a ``CoverageIndex``, +#. two different types of ``NoLockedFundsProof`` + (a standard full proof and a light proof that does not require you to provide + a per-wallet unilateral strategy), +#. the ability to provide a specialized error whitelist, +#. a way to specify that we have an instance of ``CrashTolerance`` for ``m``, +#. unit tests in the form of a function from a ``CoverageRef`` to a ``TestTree`` + (see :hsobj:`Plutus.Contract.Test.checkPredicateCoverage` + for how to construct one of these), and +#. named dynamic logic unit tests. + +Fortunately, understanding what we need to do to get certification-ready +at this stage is simple. We just need to build a ``Certification`` object. +For example of how to do this, check out ``Spec.GameStateMachine.certification`` +and ``Spec.Uniswap.certification``. + +You can run level 1 certification locally using the +:hsobj:`Plutus.Contract.Test.Certification.Run.certify` function - but at +this stage you may find it difficult to read the output of this function. +Don't worry! A certification dashboard is on the way! + +Exercises +^^^^^^^^^ + +#. Build a certification object for the ``Auction`` and ``Escrow`` contracts. diff --git a/doc/plutus/tutorials/index.rst b/doc/plutus/tutorials/index.rst index 62f0962562..6c8d171460 100644 --- a/doc/plutus/tutorials/index.rst +++ b/doc/plutus/tutorials/index.rst @@ -13,3 +13,5 @@ Tutorials basic-validators basic-minting-policies contract-testing + contract-models + 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 640543c40a..88af4b9c6f 100644 --- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-contract.nix +++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-contract.nix @@ -57,6 +57,7 @@ (hsPkgs."freer-simple" or (errorHandler.buildDepError "freer-simple")) (hsPkgs."hashable" or (errorHandler.buildDepError "hashable")) (hsPkgs."hedgehog" or (errorHandler.buildDepError "hedgehog")) + (hsPkgs."html-entities" or (errorHandler.buildDepError "html-entities")) (hsPkgs."lens" or (errorHandler.buildDepError "lens")) (hsPkgs."memory" or (errorHandler.buildDepError "memory")) (hsPkgs."mmorph" or (errorHandler.buildDepError "mmorph")) @@ -151,6 +152,7 @@ ] ++ (pkgs.lib).optionals (!(compiler.isGhcjs && true || system.isGhcjs || system.isWindows)) [ "Plutus/Contract/Test" "Plutus/Contract/Test/Coverage" + "Plutus/Contract/Test/Coverage/ReportCoverage" "Plutus/Contract/Test/ContractModel" "Plutus/Contract/Test/ContractModel/Internal" "Plutus/Contract/Test/ContractModel/Symbolics" 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 f889dababe..f6b7f83368 100644 --- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-doc.nix +++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-doc.nix @@ -57,6 +57,8 @@ (hsPkgs."random" or (errorHandler.buildDepError "random")) (hsPkgs."text" or (errorHandler.buildDepError "text")) (hsPkgs."aeson" or (errorHandler.buildDepError "aeson")) + (hsPkgs."tasty" or (errorHandler.buildDepError "tasty")) + (hsPkgs."tasty-quickcheck" or (errorHandler.buildDepError "tasty-quickcheck")) ] ++ (pkgs.lib).optional (!(compiler.isGhcjs && true || system.isGhcjs)) (hsPkgs."plutus-tx-plugin" or (errorHandler.buildDepError "plutus-tx-plugin")); build-tools = [ (hsPkgs.buildPackages.doctest.components.exes.doctest or (pkgs.buildPackages.doctest or (errorHandler.buildToolDepError "doctest:doctest"))) @@ -73,6 +75,13 @@ "HandlingBlockchainEvents" "HelloWorldApp" "WriteScriptsTo" + "Escrow" + "Escrow2" + "Escrow3" + "Escrow4" + "Escrow5" + "Escrow6" + "EscrowImpl" ]; hsSourceDirs = [ "plutus/tutorials" "plutus/howtos" ]; mainPath = (([ diff --git a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-use-cases.nix b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-use-cases.nix index b5cd38a6bc..f80d86479e 100644 --- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-use-cases.nix +++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/plutus-use-cases.nix @@ -66,6 +66,8 @@ "Plutus/Contracts/ErrorHandling" "Plutus/Contracts/Escrow" "Plutus/Contracts/SimpleEscrow" + "Plutus/Contracts/Tutorial/Escrow" + "Plutus/Contracts/Tutorial/EscrowStrict" "Plutus/Contracts/Future" "Plutus/Contracts/Game" "Plutus/Contracts/GameStateMachine" @@ -159,8 +161,10 @@ (hsPkgs."plutus-contract" or (errorHandler.buildDepError "plutus-contract")) (hsPkgs."plutus-contract-certification" or (errorHandler.buildDepError "plutus-contract-certification")) (hsPkgs."plutus-ledger" or (errorHandler.buildDepError "plutus-ledger")) + (hsPkgs."plutus-ledger-api" or (errorHandler.buildDepError "plutus-ledger-api")) (hsPkgs."plutus-ledger-constraints" or (errorHandler.buildDepError "plutus-ledger-constraints")) (hsPkgs."plutus-use-cases" or (errorHandler.buildDepError "plutus-use-cases")) + (hsPkgs."playground-common" or (errorHandler.buildDepError "playground-common")) (hsPkgs."base" or (errorHandler.buildDepError "base")) (hsPkgs."bytestring" or (errorHandler.buildDepError "bytestring")) (hsPkgs."cardano-crypto-class" or (errorHandler.buildDepError "cardano-crypto-class")) @@ -191,6 +195,13 @@ "Spec/Escrow" "Spec/Escrow/Endpoints" "Spec/SimpleEscrow" + "Spec/Tutorial/Escrow" + "Spec/Tutorial/Escrow1" + "Spec/Tutorial/Escrow2" + "Spec/Tutorial/Escrow3" + "Spec/Tutorial/Escrow4" + "Spec/Tutorial/Escrow5" + "Spec/Tutorial/Escrow6" "Spec/Future" "Spec/Game" "Spec/GameStateMachine" @@ -203,6 +214,7 @@ "Spec/Rollup" "Spec/Stablecoin" "Spec/Uniswap" + "Spec/Uniswap/Endpoints" "Spec/TokenAccount" "Spec/Vesting" ]; diff --git a/nix/pkgs/haskell/materialized-darwin/.plan.nix/quickcheck-dynamic.nix b/nix/pkgs/haskell/materialized-darwin/.plan.nix/quickcheck-dynamic.nix index 305cd0cb25..87158f9e77 100644 --- a/nix/pkgs/haskell/materialized-darwin/.plan.nix/quickcheck-dynamic.nix +++ b/nix/pkgs/haskell/materialized-darwin/.plan.nix/quickcheck-dynamic.nix @@ -44,6 +44,7 @@ "Test/QuickCheck/DynamicLogic/Monad" "Test/QuickCheck/DynamicLogic/Quantify" "Test/QuickCheck/DynamicLogic/SmartShrinking" + "Test/QuickCheck/DynamicLogic/Utils" "Test/QuickCheck/StateModel" ]; hsSourceDirs = [ "src" ]; diff --git a/nix/pkgs/haskell/materialized-darwin/default.nix b/nix/pkgs/haskell/materialized-darwin/default.nix index 721254ab68..e7fa31333d 100644 --- a/nix/pkgs/haskell/materialized-darwin/default.nix +++ b/nix/pkgs/haskell/materialized-darwin/default.nix @@ -380,6 +380,7 @@ "blockfrost-api".revision = (((hackage."blockfrost-api")."0.3.1.0").revisions).default; "blockfrost-api".flags.production = false; "blockfrost-api".flags.buildfast = true; + "html-entities".revision = (((hackage."html-entities")."1.1.4.5").revisions).default; "cryptohash-sha1".revision = (((hackage."cryptohash-sha1")."0.11.101.0").revisions).default; "warp-tls".revision = (((hackage."warp-tls")."3.3.2").revisions).default; "digest".revision = (((hackage."digest")."0.0.1.3").revisions).default; @@ -1692,6 +1693,7 @@ "servant-websockets".components.library.planned = lib.mkOverride 900 true; "ouroboros-network-framework".components.exes."demo-connection-manager".planned = lib.mkOverride 900 true; "sqlite-simple".components.library.planned = lib.mkOverride 900 true; + "html-entities".components.library.planned = lib.mkOverride 900 true; "constraints-extras".components.library.planned = lib.mkOverride 900 true; "monad-logger".components.library.planned = lib.mkOverride 900 true; "OneTuple".components.library.planned = lib.mkOverride 900 true; 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 640543c40a..88af4b9c6f 100644 --- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-contract.nix +++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-contract.nix @@ -57,6 +57,7 @@ (hsPkgs."freer-simple" or (errorHandler.buildDepError "freer-simple")) (hsPkgs."hashable" or (errorHandler.buildDepError "hashable")) (hsPkgs."hedgehog" or (errorHandler.buildDepError "hedgehog")) + (hsPkgs."html-entities" or (errorHandler.buildDepError "html-entities")) (hsPkgs."lens" or (errorHandler.buildDepError "lens")) (hsPkgs."memory" or (errorHandler.buildDepError "memory")) (hsPkgs."mmorph" or (errorHandler.buildDepError "mmorph")) @@ -151,6 +152,7 @@ ] ++ (pkgs.lib).optionals (!(compiler.isGhcjs && true || system.isGhcjs || system.isWindows)) [ "Plutus/Contract/Test" "Plutus/Contract/Test/Coverage" + "Plutus/Contract/Test/Coverage/ReportCoverage" "Plutus/Contract/Test/ContractModel" "Plutus/Contract/Test/ContractModel/Internal" "Plutus/Contract/Test/ContractModel/Symbolics" 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 f889dababe..f6b7f83368 100644 --- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-doc.nix +++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-doc.nix @@ -57,6 +57,8 @@ (hsPkgs."random" or (errorHandler.buildDepError "random")) (hsPkgs."text" or (errorHandler.buildDepError "text")) (hsPkgs."aeson" or (errorHandler.buildDepError "aeson")) + (hsPkgs."tasty" or (errorHandler.buildDepError "tasty")) + (hsPkgs."tasty-quickcheck" or (errorHandler.buildDepError "tasty-quickcheck")) ] ++ (pkgs.lib).optional (!(compiler.isGhcjs && true || system.isGhcjs)) (hsPkgs."plutus-tx-plugin" or (errorHandler.buildDepError "plutus-tx-plugin")); build-tools = [ (hsPkgs.buildPackages.doctest.components.exes.doctest or (pkgs.buildPackages.doctest or (errorHandler.buildToolDepError "doctest:doctest"))) @@ -73,6 +75,13 @@ "HandlingBlockchainEvents" "HelloWorldApp" "WriteScriptsTo" + "Escrow" + "Escrow2" + "Escrow3" + "Escrow4" + "Escrow5" + "Escrow6" + "EscrowImpl" ]; hsSourceDirs = [ "plutus/tutorials" "plutus/howtos" ]; mainPath = (([ diff --git a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-use-cases.nix b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-use-cases.nix index b5cd38a6bc..f80d86479e 100644 --- a/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-use-cases.nix +++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/plutus-use-cases.nix @@ -66,6 +66,8 @@ "Plutus/Contracts/ErrorHandling" "Plutus/Contracts/Escrow" "Plutus/Contracts/SimpleEscrow" + "Plutus/Contracts/Tutorial/Escrow" + "Plutus/Contracts/Tutorial/EscrowStrict" "Plutus/Contracts/Future" "Plutus/Contracts/Game" "Plutus/Contracts/GameStateMachine" @@ -159,8 +161,10 @@ (hsPkgs."plutus-contract" or (errorHandler.buildDepError "plutus-contract")) (hsPkgs."plutus-contract-certification" or (errorHandler.buildDepError "plutus-contract-certification")) (hsPkgs."plutus-ledger" or (errorHandler.buildDepError "plutus-ledger")) + (hsPkgs."plutus-ledger-api" or (errorHandler.buildDepError "plutus-ledger-api")) (hsPkgs."plutus-ledger-constraints" or (errorHandler.buildDepError "plutus-ledger-constraints")) (hsPkgs."plutus-use-cases" or (errorHandler.buildDepError "plutus-use-cases")) + (hsPkgs."playground-common" or (errorHandler.buildDepError "playground-common")) (hsPkgs."base" or (errorHandler.buildDepError "base")) (hsPkgs."bytestring" or (errorHandler.buildDepError "bytestring")) (hsPkgs."cardano-crypto-class" or (errorHandler.buildDepError "cardano-crypto-class")) @@ -191,6 +195,13 @@ "Spec/Escrow" "Spec/Escrow/Endpoints" "Spec/SimpleEscrow" + "Spec/Tutorial/Escrow" + "Spec/Tutorial/Escrow1" + "Spec/Tutorial/Escrow2" + "Spec/Tutorial/Escrow3" + "Spec/Tutorial/Escrow4" + "Spec/Tutorial/Escrow5" + "Spec/Tutorial/Escrow6" "Spec/Future" "Spec/Game" "Spec/GameStateMachine" @@ -203,6 +214,7 @@ "Spec/Rollup" "Spec/Stablecoin" "Spec/Uniswap" + "Spec/Uniswap/Endpoints" "Spec/TokenAccount" "Spec/Vesting" ]; diff --git a/nix/pkgs/haskell/materialized-linux/.plan.nix/quickcheck-dynamic.nix b/nix/pkgs/haskell/materialized-linux/.plan.nix/quickcheck-dynamic.nix index 305cd0cb25..87158f9e77 100644 --- a/nix/pkgs/haskell/materialized-linux/.plan.nix/quickcheck-dynamic.nix +++ b/nix/pkgs/haskell/materialized-linux/.plan.nix/quickcheck-dynamic.nix @@ -44,6 +44,7 @@ "Test/QuickCheck/DynamicLogic/Monad" "Test/QuickCheck/DynamicLogic/Quantify" "Test/QuickCheck/DynamicLogic/SmartShrinking" + "Test/QuickCheck/DynamicLogic/Utils" "Test/QuickCheck/StateModel" ]; hsSourceDirs = [ "src" ]; diff --git a/nix/pkgs/haskell/materialized-linux/default.nix b/nix/pkgs/haskell/materialized-linux/default.nix index ddf561fc38..94247bf388 100644 --- a/nix/pkgs/haskell/materialized-linux/default.nix +++ b/nix/pkgs/haskell/materialized-linux/default.nix @@ -380,6 +380,7 @@ "blockfrost-api".revision = (((hackage."blockfrost-api")."0.3.1.0").revisions).default; "blockfrost-api".flags.production = false; "blockfrost-api".flags.buildfast = true; + "html-entities".revision = (((hackage."html-entities")."1.1.4.5").revisions).default; "cryptohash-sha1".revision = (((hackage."cryptohash-sha1")."0.11.101.0").revisions).default; "warp-tls".revision = (((hackage."warp-tls")."3.3.2").revisions).default; "digest".revision = (((hackage."digest")."0.0.1.3").revisions).default; @@ -1692,6 +1693,7 @@ "servant-websockets".components.library.planned = lib.mkOverride 900 true; "ouroboros-network-framework".components.exes."demo-connection-manager".planned = lib.mkOverride 900 true; "sqlite-simple".components.library.planned = lib.mkOverride 900 true; + "html-entities".components.library.planned = lib.mkOverride 900 true; "constraints-extras".components.library.planned = lib.mkOverride 900 true; "monad-logger".components.library.planned = lib.mkOverride 900 true; "OneTuple".components.library.planned = lib.mkOverride 900 true; 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 640543c40a..88af4b9c6f 100644 --- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-contract.nix +++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-contract.nix @@ -57,6 +57,7 @@ (hsPkgs."freer-simple" or (errorHandler.buildDepError "freer-simple")) (hsPkgs."hashable" or (errorHandler.buildDepError "hashable")) (hsPkgs."hedgehog" or (errorHandler.buildDepError "hedgehog")) + (hsPkgs."html-entities" or (errorHandler.buildDepError "html-entities")) (hsPkgs."lens" or (errorHandler.buildDepError "lens")) (hsPkgs."memory" or (errorHandler.buildDepError "memory")) (hsPkgs."mmorph" or (errorHandler.buildDepError "mmorph")) @@ -151,6 +152,7 @@ ] ++ (pkgs.lib).optionals (!(compiler.isGhcjs && true || system.isGhcjs || system.isWindows)) [ "Plutus/Contract/Test" "Plutus/Contract/Test/Coverage" + "Plutus/Contract/Test/Coverage/ReportCoverage" "Plutus/Contract/Test/ContractModel" "Plutus/Contract/Test/ContractModel/Internal" "Plutus/Contract/Test/ContractModel/Symbolics" 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 f889dababe..f6b7f83368 100644 --- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-doc.nix +++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-doc.nix @@ -57,6 +57,8 @@ (hsPkgs."random" or (errorHandler.buildDepError "random")) (hsPkgs."text" or (errorHandler.buildDepError "text")) (hsPkgs."aeson" or (errorHandler.buildDepError "aeson")) + (hsPkgs."tasty" or (errorHandler.buildDepError "tasty")) + (hsPkgs."tasty-quickcheck" or (errorHandler.buildDepError "tasty-quickcheck")) ] ++ (pkgs.lib).optional (!(compiler.isGhcjs && true || system.isGhcjs)) (hsPkgs."plutus-tx-plugin" or (errorHandler.buildDepError "plutus-tx-plugin")); build-tools = [ (hsPkgs.buildPackages.doctest.components.exes.doctest or (pkgs.buildPackages.doctest or (errorHandler.buildToolDepError "doctest:doctest"))) @@ -73,6 +75,13 @@ "HandlingBlockchainEvents" "HelloWorldApp" "WriteScriptsTo" + "Escrow" + "Escrow2" + "Escrow3" + "Escrow4" + "Escrow5" + "Escrow6" + "EscrowImpl" ]; hsSourceDirs = [ "plutus/tutorials" "plutus/howtos" ]; mainPath = (([ diff --git a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-use-cases.nix b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-use-cases.nix index b5cd38a6bc..f80d86479e 100644 --- a/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-use-cases.nix +++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/plutus-use-cases.nix @@ -66,6 +66,8 @@ "Plutus/Contracts/ErrorHandling" "Plutus/Contracts/Escrow" "Plutus/Contracts/SimpleEscrow" + "Plutus/Contracts/Tutorial/Escrow" + "Plutus/Contracts/Tutorial/EscrowStrict" "Plutus/Contracts/Future" "Plutus/Contracts/Game" "Plutus/Contracts/GameStateMachine" @@ -159,8 +161,10 @@ (hsPkgs."plutus-contract" or (errorHandler.buildDepError "plutus-contract")) (hsPkgs."plutus-contract-certification" or (errorHandler.buildDepError "plutus-contract-certification")) (hsPkgs."plutus-ledger" or (errorHandler.buildDepError "plutus-ledger")) + (hsPkgs."plutus-ledger-api" or (errorHandler.buildDepError "plutus-ledger-api")) (hsPkgs."plutus-ledger-constraints" or (errorHandler.buildDepError "plutus-ledger-constraints")) (hsPkgs."plutus-use-cases" or (errorHandler.buildDepError "plutus-use-cases")) + (hsPkgs."playground-common" or (errorHandler.buildDepError "playground-common")) (hsPkgs."base" or (errorHandler.buildDepError "base")) (hsPkgs."bytestring" or (errorHandler.buildDepError "bytestring")) (hsPkgs."cardano-crypto-class" or (errorHandler.buildDepError "cardano-crypto-class")) @@ -191,6 +195,13 @@ "Spec/Escrow" "Spec/Escrow/Endpoints" "Spec/SimpleEscrow" + "Spec/Tutorial/Escrow" + "Spec/Tutorial/Escrow1" + "Spec/Tutorial/Escrow2" + "Spec/Tutorial/Escrow3" + "Spec/Tutorial/Escrow4" + "Spec/Tutorial/Escrow5" + "Spec/Tutorial/Escrow6" "Spec/Future" "Spec/Game" "Spec/GameStateMachine" @@ -203,6 +214,7 @@ "Spec/Rollup" "Spec/Stablecoin" "Spec/Uniswap" + "Spec/Uniswap/Endpoints" "Spec/TokenAccount" "Spec/Vesting" ]; diff --git a/nix/pkgs/haskell/materialized-windows/.plan.nix/quickcheck-dynamic.nix b/nix/pkgs/haskell/materialized-windows/.plan.nix/quickcheck-dynamic.nix index 305cd0cb25..87158f9e77 100644 --- a/nix/pkgs/haskell/materialized-windows/.plan.nix/quickcheck-dynamic.nix +++ b/nix/pkgs/haskell/materialized-windows/.plan.nix/quickcheck-dynamic.nix @@ -44,6 +44,7 @@ "Test/QuickCheck/DynamicLogic/Monad" "Test/QuickCheck/DynamicLogic/Quantify" "Test/QuickCheck/DynamicLogic/SmartShrinking" + "Test/QuickCheck/DynamicLogic/Utils" "Test/QuickCheck/StateModel" ]; hsSourceDirs = [ "src" ]; diff --git a/nix/pkgs/haskell/materialized-windows/default.nix b/nix/pkgs/haskell/materialized-windows/default.nix index 513b4e6c54..9d6ef23dc4 100644 --- a/nix/pkgs/haskell/materialized-windows/default.nix +++ b/nix/pkgs/haskell/materialized-windows/default.nix @@ -376,6 +376,7 @@ "blockfrost-api".revision = (((hackage."blockfrost-api")."0.3.1.0").revisions).default; "blockfrost-api".flags.production = false; "blockfrost-api".flags.buildfast = true; + "html-entities".revision = (((hackage."html-entities")."1.1.4.5").revisions).default; "cryptohash-sha1".revision = (((hackage."cryptohash-sha1")."0.11.101.0").revisions).default; "warp-tls".revision = (((hackage."warp-tls")."3.3.2").revisions).default; "digest".revision = (((hackage."digest")."0.0.1.3").revisions).default; @@ -1672,6 +1673,7 @@ "servant-websockets".components.library.planned = lib.mkOverride 900 true; "ouroboros-network-framework".components.exes."demo-connection-manager".planned = lib.mkOverride 900 true; "sqlite-simple".components.library.planned = lib.mkOverride 900 true; + "html-entities".components.library.planned = lib.mkOverride 900 true; "constraints-extras".components.library.planned = lib.mkOverride 900 true; "monad-logger".components.library.planned = lib.mkOverride 900 true; "OneTuple".components.library.planned = lib.mkOverride 900 true; diff --git a/plutus-contract-certification/src/Plutus/Contract/Test/Certification.hs b/plutus-contract-certification/src/Plutus/Contract/Test/Certification.hs index 44b7ecabce..a9e0582acf 100644 --- a/plutus-contract-certification/src/Plutus/Contract/Test/Certification.hs +++ b/plutus-contract-certification/src/Plutus/Contract/Test/Certification.hs @@ -16,17 +16,19 @@ data Certification m = Certification { certCoverageIndex :: CoverageIndex, -- ^ Coverage locations for on-chain test coverage. certNoLockedFunds :: Maybe (NoLockedFundsProof m), certNoLockedFundsLight :: Maybe (NoLockedFundsProofLight m), - certUnitTests :: Maybe (CoverageRef -> TestTree), -- ^ Unit tests using "Test.Tasty". See e.g. 'Plutus.Contract.Test.checkPredicateCoverage'. certCrashTolerance :: Maybe (Instance CrashTolerance m), -- ^ Contract model for testing robustness against off-chain code crashes. certWhitelist :: Maybe Whitelist, -- ^ List of allowed exceptions from on-chain code. Usually `Just 'defaultWhiteList'`. + certUnitTests :: Maybe (CoverageRef -> TestTree), -- ^ Unit tests using "Test.Tasty". See e.g. 'Plutus.Contract.Test.checkPredicateCoverage'. certDLTests :: [(String, DL m ())] -- ^ Unit tests using 'Plutus.Contract.Test.ContractModel.DL'. } defaultCertification :: Certification m -defaultCertification = Certification { certCoverageIndex = mempty - , certNoLockedFunds = Nothing - , certNoLockedFundsLight = Nothing - , certUnitTests = Nothing - , certCrashTolerance = Nothing - , certWhitelist = Just defaultWhitelist - , certDLTests = [] } +defaultCertification = Certification + { certCoverageIndex = mempty + , certNoLockedFunds = Nothing + , certNoLockedFundsLight = Nothing + , certUnitTests = Nothing + , certCrashTolerance = Nothing + , certWhitelist = Just defaultWhitelist + , certDLTests = [] + } diff --git a/plutus-contract-certification/src/Plutus/Contract/Test/Certification/Run.hs b/plutus-contract-certification/src/Plutus/Contract/Test/Certification/Run.hs index b1847d81b1..48de3b1c11 100644 --- a/plutus-contract-certification/src/Plutus/Contract/Test/Certification/Run.hs +++ b/plutus-contract-certification/src/Plutus/Contract/Test/Certification/Run.hs @@ -130,12 +130,12 @@ runStandardProperty opts covIdx = liftIORep $ quickCheckWithCoverageAndResult @m defaultCheckOptionsContractModel covopts - $ const (pure True) + (\ _ -> pure True) checkNoLockedFunds :: ContractModel m => CertificationOptions -> NoLockedFundsProof m -> CertMonad QC.Result checkNoLockedFunds opts prf = lift $ quickCheckWithResult (mkQCArgs opts) - $ checkNoLockedFundsProof defaultCheckOptionsContractModel prf + $ checkNoLockedFundsProof prf checkNoLockedFundsLight :: ContractModel m => CertificationOptions -> NoLockedFundsProofLight m -> CertMonad QC.Result checkNoLockedFundsLight opts prf = diff --git a/plutus-contract/plutus-contract.cabal b/plutus-contract/plutus-contract.cabal index 0a2be11e9b..281d0591cd 100644 --- a/plutus-contract/plutus-contract.cabal +++ b/plutus-contract/plutus-contract.cabal @@ -127,6 +127,7 @@ library freer-simple -any, hashable -any, hedgehog -any, + html-entities -any, lens -any, memory -any, mmorph -any, @@ -161,6 +162,7 @@ library exposed-modules: Plutus.Contract.Test Plutus.Contract.Test.Coverage + Plutus.Contract.Test.Coverage.ReportCoverage Plutus.Contract.Test.ContractModel Plutus.Contract.Test.ContractModel.Internal Plutus.Contract.Test.ContractModel.Symbolics diff --git a/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs b/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs index f84029a113..b9f5f4f28a 100644 --- a/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs +++ b/plutus-contract/src/Plutus/Contract/Test/ContractModel.hs @@ -135,6 +135,8 @@ module Plutus.Contract.Test.ContractModel , checkNoLockedFundsProofFast , NoLockedFundsProofLight(..) , checkNoLockedFundsProofLight + , checkNoLockedFundsProofWithOptions + , checkNoLockedFundsProofFastWithOptions -- $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 c3af0f5526..3f4343564b 100644 --- a/plutus-contract/src/Plutus/Contract/Test/ContractModel/CrashTolerance.hs +++ b/plutus-contract/src/Plutus/Contract/Test/ContractModel/CrashTolerance.hs @@ -140,8 +140,11 @@ instance forall state. -- An action may start its own contract instances and we need to keep track of them aliveContractInstances %= ([Key k | StartContract (UnderlyingContractInstanceKey k) _ <- startInstances s (UnderlyingAction a)] ++) where - embed :: Spec state a -> Spec (WithCrashTolerance state) a - embed (Spec comp) = Spec (zoom (liftL _contractState underlyingModelState) comp) + + nextReactiveState slot = embed $ nextReactiveState slot + + monitoring (s,s') (UnderlyingAction a) = monitoring (_underlyingModelState <$> s,_underlyingModelState <$> s') a + monitoring _ _ = id arbitraryAction s = frequency [ (10, UnderlyingAction <$> arbitraryAction (_underlyingModelState <$> s)) , (1, Crash <$> QC.elements (s ^. contractState . aliveContractInstances)) @@ -153,3 +156,5 @@ instance forall state. liftL :: Functor t => (forall a. t a -> a) -> Lens' s a -> Lens' (t s) (t a) liftL extr l ft ts = getCompose . l (Compose . ft . (<$ ts)) $ extr ts +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 daaa04f485..d05f1e158e 100644 --- a/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs +++ b/plutus-contract/src/Plutus/Contract/Test/ContractModel/Internal.hs @@ -93,6 +93,7 @@ module Plutus.Contract.Test.ContractModel.Internal , assertModel , stopping , weight + , getSize , monitor -- * Properties @@ -147,6 +148,8 @@ module Plutus.Contract.Test.ContractModel.Internal , checkNoLockedFundsProofFast , NoLockedFundsProofLight(..) , checkNoLockedFundsProofLight + , checkNoLockedFundsProofWithOptions + , checkNoLockedFundsProofFastWithOptions -- $checkNoPartiality , Whitelist , whitelistOk @@ -199,7 +202,7 @@ import Ledger.Slot 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 hiding (not) import Plutus.Contract.Test.ContractModel.Symbolics import Plutus.Contract.Test.Coverage import Plutus.Trace.Effects.EmulatorControl (discardWallets) @@ -212,11 +215,11 @@ import PlutusTx.Coverage import PlutusTx.ErrorCodes import Streaming qualified as S import Test.QuickCheck.DynamicLogic.Monad qualified as DL -import Test.QuickCheck.StateModel hiding (Action, Actions (..), arbitraryAction, initialState, monitoring, nextState, - pattern Actions, perform, precondition, shrinkAction, stateAfter) +import Test.QuickCheck.StateModel hiding (Action, Actions (..), actionName, arbitraryAction, initialState, monitoring, + nextState, pattern Actions, perform, precondition, shrinkAction, stateAfter) import Test.QuickCheck.StateModel qualified as StateModel -import Test.QuickCheck hiding (ShrinkState, checkCoverage, (.&&.), (.||.)) +import Test.QuickCheck hiding (ShrinkState, checkCoverage, getSize, (.&&.), (.||.)) import Test.QuickCheck qualified as QC import Test.QuickCheck.Monadic (PropertyM, monadic) import Test.QuickCheck.Monadic qualified as QC @@ -456,6 +459,10 @@ class ( Typeable state -- `anyActions`. arbitraryAction :: ModelState state -> Gen (Action state) + -- | The name of an Action, used to report statistics. + actionName :: Action state -> String + actionName = head . words . show + -- | The probability that we will generate a `WaitUntil` in a given state waitProbability :: ModelState state -> Double waitProbability _ = 0.1 @@ -814,6 +821,10 @@ instance ContractModel state => StateModel (ModelState state) where type ActionMonad (ModelState state) = ContractMonad state + actionName (ContractAction _ act) = actionName act + actionName (Unilateral _) = "Unilateral" + actionName (WaitUntil _) = "WaitUntil" + arbitraryAction s = -- TODO: do we need some way to control the distribution -- between actions and waits here? @@ -834,7 +845,7 @@ instance ContractModel state => StateModel (ModelState state) where shrinkAction _ _ = [] initialState = ModelState { _currentSlot = 1 - , _balanceChanges = Map.empty + , _balanceChanges = Map.fromList [(w,mempty) | w <- knownWallets] , _minted = mempty , _assertions = mempty , _assertionsOk = True @@ -1199,7 +1210,7 @@ anyActions :: Int -> DL state () anyActions = DL.anyActions -- | Generate a sequence of random actions using `arbitraryAction`. All actions satisfy their --- `precondition`s. Actions are generated until the `stopping` stage is reached. +-- `precondition`s. Actions may be generated until the `stopping` stage is reached; the expected length is size/2. anyActions_ :: DL state () anyActions_ = DL.anyActions_ @@ -1213,15 +1224,16 @@ anyActions_ = DL.anyActions_ -- Conversely, before the stopping phase, branches starting with `stopping` -- are avoided unless there are no other possible choices. -- --- For example, here is the definition of `anyActions_`: +-- For example, here is the definition of `anyActions`: -- -- @ --- `anyActions_` = `stopping` `Control.Applicative.<|>` (`anyAction` >> `anyActions_`) +-- `anyActions` n = `stopping` `Control.Applicative.<|>` pure () +-- `Control.Applicative.<|>` (`weight` (fromIntegral n) >> `anyAction` >> `anyActions` n) -- @ -- --- The effect of this definition is that the second branch will be taken until the desired number +-- The effect of this definition is that the second or third branch will be taken until the desired number -- of actions have been generated, at which point the `stopping` branch will be taken and --- generation stops (or continues with whatever comes after the `anyActions_` call). +-- generation stops (or continues with whatever comes after the `anyActions` call). -- -- Now, it might not be possible, or too hard, to find a way to terminate a scenario. For -- instance, this scenario has no finite test cases: @@ -1259,6 +1271,20 @@ stopping = DL.stopping weight :: Double -> DL state () weight = DL.weight +-- | Sometimes test case generation should depend on QuickCheck's size +-- parameter. This can be accessed using @getSize@. For example, @anyActions_@ is defined by +-- +-- @ +-- anyActions_ = do n <- getSize +-- anyActions (n `div` 2 + 1) +-- @ +-- +-- so that we generate a random number of actions, but on average half the size (which is about the same as +-- the average random positive integer, or length of a list). + +getSize :: DL state Int +getSize = DL.getSize + -- | The `monitor` function allows you to collect statistics of your testing using QuickCheck -- functions like `Test.QuickCheck.label`, `Test.QuickCheck.collect`, `Test.QuickCheck.classify`, -- and `Test.QuickCheck.tabulate`. See also the `monitoring` method of `ContractModel` which is @@ -1706,21 +1732,33 @@ defaultNLFP = NoLockedFundsProof { nlfpMainStrategy = return () -- are killed and their private keys are deleted from the emulator state. checkNoLockedFundsProof + :: (ContractModel model) + => NoLockedFundsProof model + -> Property +checkNoLockedFundsProof = checkNoLockedFundsProofWithOptions defaultCheckOptionsContractModel + +checkNoLockedFundsProofFast + :: (ContractModel model) + => NoLockedFundsProof model + -> Property +checkNoLockedFundsProofFast = checkNoLockedFundsProofFastWithOptions defaultCheckOptionsContractModel + +checkNoLockedFundsProofWithOptions :: (ContractModel model) => CheckOptions -> NoLockedFundsProof model -> Property -checkNoLockedFundsProof options = +checkNoLockedFundsProofWithOptions options = checkNoLockedFundsProof' prop where prop = propRunActionsWithOptions' options defaultCoverageOptions (\ _ -> TracePredicate $ pure True) -checkNoLockedFundsProofFast +checkNoLockedFundsProofFastWithOptions :: (ContractModel model) => CheckOptions -> NoLockedFundsProof model -> Property -checkNoLockedFundsProofFast _ = checkNoLockedFundsProof' (const $ property True) +checkNoLockedFundsProofFastWithOptions _ = checkNoLockedFundsProof' (const $ property True) checkNoLockedFundsProof' :: (ContractModel model) @@ -1736,7 +1774,9 @@ checkNoLockedFundsProof' run NoLockedFundsProof{nlfpMainStrategy = mainStrat, let s0 = (stateAfter $ Actions as) s = stateAfter $ Actions (as ++ as') in foldl (QC..&&.) (counterexample "Main run prop" (run (toStateModelActions $ Actions $ as ++ as')) QC..&&. (counterexample "Main strategy" . counterexample (show . Actions $ as ++ as') $ prop s0 s)) - [ walletProp s0 as w bal | (w, bal) <- Map.toList (s ^. balanceChanges) ] + [ walletProp s0 as w bal | (w, bal) <- Map.toList (s ^. balanceChanges) + , not $ bal `symLeq` (s0 ^. balanceChange w) ] + -- if the main strategy leaves w with <= the starting value, then doing nothing is a good wallet strategy. where nextVarIdx as = 1 + maximum ([0] ++ [ i | i <- varNumOf <$> as ]) prop s0 s = diff --git a/plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs b/plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs index 0e4e6900ad..de1de9c724 100644 --- a/plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs +++ b/plutus-contract/src/Plutus/Contract/Test/ContractModel/Symbolics.hs @@ -37,7 +37,7 @@ newtype AssetKey = AssetKey Int deriving (Ord, Eq, Show, Num, JSON.FromJSONKey, data SymToken = SymToken { symVar :: Var AssetKey, symVarIdx :: String } deriving (Ord, Eq, Data) -- | A symbolic value is a combination of a real value and a value associating symbolic -- tokens with an amount -data SymValue = SymValue { symValMap :: Map SymToken Integer, actualValPart :: Value } deriving (Show) +data SymValue = SymValue { symValMap :: Map SymToken Integer, actualValPart :: Value } deriving (Show, Data) instance Show SymToken where show (SymToken (Var i) n) = "tok" ++ show i ++ "." ++ n diff --git a/plutus-contract/src/Plutus/Contract/Test/Coverage.hs b/plutus-contract/src/Plutus/Contract/Test/Coverage.hs index d4d8f158e4..d03e0c6c1d 100644 --- a/plutus-contract/src/Plutus/Contract/Test/Coverage.hs +++ b/plutus-contract/src/Plutus/Contract/Test/Coverage.hs @@ -8,6 +8,7 @@ module Plutus.Contract.Test.Coverage , CoverageRef(..) , newCoverageRef , readCoverageRef + , writeCoverageReport ) where import Data.Aeson (FromJSON, FromJSONKey, ToJSON, ToJSONKey) @@ -34,9 +35,10 @@ import Wallet.Emulator.MultiAgent (EmulatorEvent, EmulatorEvent' (..), EmulatorT import Wallet.Types import Data.IORef +import Plutus.Contract.Test.Coverage.ReportCoverage qualified as ReportCoverage --- | Get every endpoint name that has been invoced in the emulator events in `es` +-- | Get every endpoint name that has been invoked in the emulator events in `es` -- indexed by `ContractInstanceTag` getInvokedEndpoints :: [EmulatorEvent] -> Map ContractInstanceTag (Set String) getInvokedEndpoints es = @@ -72,6 +74,10 @@ newCoverageRef = CoverageRef <$> newIORef mempty readCoverageRef :: CoverageRef -> IO CoverageReport readCoverageRef (CoverageRef ioref) = readIORef ioref +-- | Write a coverage report to name.html for the given index. +writeCoverageReport :: String -> CoverageIndex -> CoverageReport -> IO () +writeCoverageReport = ReportCoverage.writeCoverageReport + -- TODO: Move this to plutus core to avoid orhpan instance instance NFData CovLoc where rnf (CovLoc f sl el sc ec) = diff --git a/plutus-contract/src/Plutus/Contract/Test/Coverage/ReportCoverage.hs b/plutus-contract/src/Plutus/Contract/Test/Coverage/ReportCoverage.hs new file mode 100644 index 0000000000..63c4ed87de --- /dev/null +++ b/plutus-contract/src/Plutus/Contract/Test/Coverage/ReportCoverage.hs @@ -0,0 +1,271 @@ +module Plutus.Contract.Test.Coverage.ReportCoverage(writeCoverageReport) where + +import Control.Exception +import Data.Function +import Data.List +import Data.Map qualified as Map +import Data.Ord +import Data.Set (Set) +import Data.Set qualified as Set +import Data.Text (pack, unpack) +import HTMLEntities.Text (text) + +import PlutusTx.Coverage + +-- Position (in a file), and status (of a character) + +type Pos = (Int,Int) -- line, column + +predPos, succPos :: Pos -> Pos + +predPos (l,1) = (l-1,maxBound) +predPos (l,c) = (l,c-1) + +succPos (l,c) = (l,c+1) + +data Status = AlwaysTrue | AlwaysFalse | Uncovered | OffChain | Covered + -- Covered comes last, because this means that all of the other status + -- take precedence when there are two swipes for the same interval + -- (one from the base coverage, and the other from the "uncovered" set) + deriving (Eq, Ord, Show) + +statusStyle :: Status -> String +statusStyle Covered = "background-color:white;color:black" +statusStyle AlwaysTrue = "background-color:lightgreen;color:black" +statusStyle AlwaysFalse = "background-color:lightpink;color:black" +statusStyle Uncovered = "background-color:black;color:orangered" +statusStyle OffChain = "background-color:lightgray;color:gray" + +-- A "swipe" represents colouring a region of a file with a +-- status. Our overall approach is to convert coverage information +-- into a collection of non-overlapping, but possibly nested swipes, +-- and then converting this into an orderedlist of disjoint swipes +-- which can be used for generating colours. + +data Swipe = Swipe { swipeStart :: Pos, + swipeEnd :: Pos, + swipeStatus :: Status } + deriving (Eq, Show) + +-- This surprising ordering on swipes has the property that if s1 is +-- nested within s2, then s1 <= s2. Given that no two swipes overlap, +-- then s1 <= s2 precisely if s1 precedes s2 entirely, or s1 is nested +-- within s2. It follow that, in a sorted list of swipes, the first +-- one has no other swipes nested within it, and therefore its colour +-- takes priority over all other swipes. We make use of this in +-- converting a set of swipes to a set of disjoint swipes with the +-- same coloration. + +instance Ord Swipe where + (<=) = (<=) `on` \(Swipe start end status) -> (end, Down start, status) + +precedes :: Swipe -> Swipe -> Bool +precedes sw sw' = swipeEnd sw < swipeStart sw' + +-- Is the first swipe nested within the second? + +nested :: Swipe -> Swipe -> Bool +nested (Swipe from to _) (Swipe from' to' _) = from >= from' && to <= to' + +-- Let the first swipe "swipe over" part of the second. The resulting +-- swipes do not overlap. The first swipe must be nested within the +-- second. + +combineNestedSwipes :: Swipe -> Swipe -> [Swipe] +combineNestedSwipes (Swipe from to s) (Swipe from' to' s') = + [Swipe from' (predPos from) s' | from /= from'] ++ + [Swipe from to s] ++ + [Swipe (succPos to) to' s' | to /= to'] + +-- Flatten an ordered list of swipes, to get a non-overlapping list. +-- Nested swipes "swipe over" the outer swipe. Because of the custom +-- ordering on swipes, the first swipe in the list cannot have any +-- other swipe in the listed nested within it, which means that its +-- colour "wins" over all others. + +flattenSwipes :: [Swipe] -> [Swipe] +flattenSwipes [] = [] +flattenSwipes (sw:swipes) = swipeOver sw . flattenSwipes $ swipes + +swipeOver :: Swipe -> [Swipe] -> [Swipe] +swipeOver sw [] = [sw] +swipeOver sw (sw':swipes) + | swipeEnd sw < swipeStart sw' = sw:sw':swipes + | swipeEnd sw' < swipeStart sw = sw':swipeOver sw swipes + | nested sw sw' = combineNestedSwipes sw sw' ++ swipes + | otherwise = error . unlines $ + "swipeOver: precondition violated; swipes are not nested or disjoint.": + map show (sw:sw':take 8 swipes) + +-- Convert an ordered list of non-intersecting swipes that may swipe +-- any region in a file, into a list of swipes applied to each line. + +type SwipesPerLine = [(Int,[Swipe])] + +swipesByLine :: [Swipe] -> SwipesPerLine +swipesByLine = map addLine . groupBy ((==) `on` (fst.swipeStart)) . concatMap splitSwipe + where splitSwipe s@(Swipe (fromLine,_) (toLine,_) _) + | fromLine == toLine = [s] + | otherwise = s{swipeEnd = (fromLine,maxBound)}: + splitSwipe s{swipeStart = (fromLine+1,1)} + addLine swipes = (fst . swipeStart . head $ swipes, swipes) + +-- Extend a list of swipes-per-line by including non-swiped lines that +-- are within windowLines of a swiped line. + +windowLines :: Int +windowLines = 5 + +includeNearby :: SwipesPerLine -> SwipesPerLine +includeNearby swipes = excluding 1 swipes + where excluding _ [] = [] + excluding n nSwipes + | n > nextSwiped = error . unlines $ ("Bad excluding: "++show n):map show (take 10 nSwipes) + | n == nextSwiped = including n nSwipes + | n+windowLines < nextSwiped = excluding (nextSwiped-windowLines) nSwipes + | otherwise = (n,[]):excluding (n+1) nSwipes + where nextSwiped = fst (head nSwipes) + including _ [] = [] + including n ((next,swipe):nSwipes) + | n > next = error . unlines $ ("Bad including: "++show n):map show (take 10 ((next,swipe):nSwipes)) + | n == next = + (next,swipe):including (n+1) nSwipes + | n+windowLines >= next = + (n,[]):including (n+1) ((next,swipe):nSwipes) + | n+windowLines < next = + [(i,[]) | i <- [n..n-1+windowLines]] ++ excluding (n+windowLines) ((next,swipe):nSwipes) + | otherwise = error "impossible" + +-- Extend a list of swipes-per-line to include non-swiped lines that +-- form a small gap between swiped blocks. Gaps are replaced by three +-- vertical dots; there is no sense in replacing a gap of three or +-- fewer lines this way. + +fillSmallGaps :: SwipesPerLine -> SwipesPerLine +fillSmallGaps ((n,swipes):(n',swipes'):nSwipes) + | n+4 >= n' = (n,swipes):[(i,[]) | i <- [n+1..n'-1]] ++ fillSmallGaps ((n',swipes'):nSwipes) + | otherwise = (n,swipes):fillSmallGaps ((n',swipes'):nSwipes) +fillSmallGaps swipes = swipes + +-- Generate HTML elements + +element :: String -> [(String,String)] -> String -> String +element name attrs body = + "<"++name++" "++ + concat [a++"="++b++" " | (a,b) <- attrs]++ + ">"++body++""++name++">" + +quote :: String -> String +quote s = q++s++q + where q = "\"" + +encode :: String -> String +encode = unpack . text . pack + +-- Read source files and extract coverage information. + +type FileInfo = (String, [String], Set CoverageAnnotation, Set CoverageAnnotation) + +files :: CoverageIndex -> CoverageReport -> IO [FileInfo] +files ci@(CoverageIndex metadataMap) (CoverageReport annots) = sequence [file n | n <- fileNames ci] + where file name = do + body <- either (const "" :: IOException -> String) id <$> + try (readFile name) + return (name, lines body, covx name, covs name) + covx name = Set.filter ((==name) . _covLocFile . getCovLoc) . Map.keysSet $ metadataMap + covs name = Set.filter ((==name) . _covLocFile . getCovLoc) annots + +fileNames :: CoverageIndex -> [String] +fileNames (CoverageIndex metadataMap) = + Set.toList . Set.map (_covLocFile . getCovLoc) . Map.keysSet $ metadataMap + +getCovLoc :: CoverageAnnotation -> CovLoc +getCovLoc (CoverLocation c) = c +getCovLoc (CoverBool c _) = c + +locSwipe :: CovLoc -> Status -> Swipe +locSwipe loc status = + Swipe (_covLocStartLine loc, _covLocStartCol loc) + (_covLocEndLine loc, _covLocEndCol loc) + status + +-- Generate the coverage report and write to an HTML file. + +writeCoverageReport :: String -> CoverageIndex -> CoverageReport -> IO () +writeCoverageReport name ci cr = do + fs <- files ci cr + writeFile (name++".html") . coverageReportHtml $ fs + +coverageReportHtml :: [FileInfo] -> String +coverageReportHtml fs = element "body" [] $ report + where + report = header ++ concat ["
. +. +. + 71 , highestBidder :: PaymentPubKeyHash + 72 } + 73 deriving stock (Haskell.Eq, Haskell.Show, Generic) + 74 deriving anyclass (ToJSON, FromJSON) + 75 + 76 PlutusTx.unstableMakeIsData ''HighestBid + 77 + 78 -- | The states of the auction + 79 data AuctionState + 80 = Ongoing HighestBid -- Bids can be submitted. + 81 | Finished HighestBid -- The auction is finished +. +. +. + 104 -- highest bidder is seller of the asset. So if nobody submits + 105 -- any bids, the seller gets the asset back after the auction has ended. + 106 initialState :: PaymentPubKeyHash -> AuctionState + 107 initialState self = Ongoing HighestBid{highestBid = 0, highestBidder = self} + 108 + 109 PlutusTx.unstableMakeIsData ''AuctionState + 110 + 111 -- | Transition between auction states + 112 data AuctionInput + 113 = Bid { newBid :: Ada, newBidder :: PaymentPubKeyHash } -- Increase the price + 114 | Payout +. +. +. + 124 auctionTransition + 125 :: AuctionParams + 126 -> State AuctionState + 127 -> AuctionInput + 128 -> Maybe (TxConstraints Void Void, State AuctionState) + 129 auctionTransition AuctionParams{apOwner, apAsset, apEndTime} State{stateData=oldStateData, stateValue=oldStateValue} input = + 130 case (oldStateData, input) of + 131 + 132 (Ongoing HighestBid{highestBid, highestBidder}, Bid{newBid, newBidder}) | newBid > highestBid -> -- if the new bid is higher, + 133 let constraints = if highestBid == 0 then mempty else + 134 Constraints.mustPayToPubKey highestBidder (Ada.toValue highestBid) -- we pay back the previous highest bid + 135 <> Constraints.mustValidateIn (Interval.to $ apEndTime - 1) -- but only if we haven't gone past 'apEndTime' + 136 newState = + 137 State + 138 { stateData = Ongoing HighestBid{highestBid = newBid, highestBidder = newBidder} + 139 , stateValue = Value.noAdaValue oldStateValue + 140 <> Ada.toValue (Ada.fromValue oldStateValue - highestBid) + 141 <> Ada.toValue newBid -- and lock the new bid in the script output + 142 } + 143 in Just (constraints, newState) + 144 + 145 (Ongoing h@HighestBid{highestBidder, highestBid}, Payout) -> + 146 let constraints = + 147 Constraints.mustValidateIn (Interval.from apEndTime) -- When the auction has ended, + 148 <> Constraints.mustPayToPubKey apOwner (Ada.toValue highestBid) -- the owner receives the payment + 149 <> Constraints.mustPayToPubKey highestBidder apAsset -- and the highest bidder the asset + 150 newState = State { stateData = Finished h, stateValue = mempty } + 151 in Just (constraints, newState) + 152 + 153 -- Any other combination of 'AuctionState' and 'AuctionInput' is disallowed. + 154 -- This rules out new bids that don't go over the current highest bid. + 155 _ -> Nothing + 156 + 157 + 158 {-# INLINABLE auctionStateMachine #-} + 159 auctionStateMachine :: (ThreadToken, AuctionParams) -> AuctionMachine + 160 auctionStateMachine (threadToken, auctionParams) = + 161 SM.mkStateMachine (Just threadToken) (auctionTransition auctionParams) isFinal + 162 where + 163 isFinal Finished{} = True + 164 isFinal _ = False + 165 + 166 {-# INLINABLE mkValidator #-} + 167 mkValidator :: (ThreadToken, AuctionParams) -> Scripts.ValidatorType AuctionMachine + 168 mkValidator = SM.mkValidator . auctionStateMachine + 169 + 170 -- | The script instance of the auction state machine. It contains the state + 171 -- machine compiled to a Plutus core validator script. + 172 typedValidator :: (ThreadToken, AuctionParams) -> Scripts.TypedValidator AuctionMachine + 173 typedValidator = Scripts.mkTypedValidatorParam @AuctionMachine +. +. +. + 365 Transition _ (Ongoing s) -> loop s + 366 InitialState (Ongoing s) -> loop s + 367 _ -> logWarn CurrentStateNotFound + 368 + 369 covIdx :: CoverageIndex + 370 covIdx = getCovIdx $$(PlutusTx.compile [|| mkValidator ||]) +\ No newline at end of file diff --git a/plutus-use-cases/plutus-use-cases.cabal b/plutus-use-cases/plutus-use-cases.cabal index eba8502bc8..30e0a18cf4 100644 --- a/plutus-use-cases/plutus-use-cases.cabal +++ b/plutus-use-cases/plutus-use-cases.cabal @@ -34,6 +34,8 @@ library Plutus.Contracts.ErrorHandling Plutus.Contracts.Escrow Plutus.Contracts.SimpleEscrow + Plutus.Contracts.Tutorial.Escrow + Plutus.Contracts.Tutorial.EscrowStrict Plutus.Contracts.Future Plutus.Contracts.Game Plutus.Contracts.GameStateMachine @@ -110,6 +112,13 @@ test-suite plutus-use-cases-test Spec.Escrow Spec.Escrow.Endpoints Spec.SimpleEscrow + Spec.Tutorial.Escrow + Spec.Tutorial.Escrow1 + Spec.Tutorial.Escrow2 + Spec.Tutorial.Escrow3 + Spec.Tutorial.Escrow4 + Spec.Tutorial.Escrow5 + Spec.Tutorial.Escrow6 Spec.Future Spec.Game Spec.GameStateMachine @@ -122,6 +131,7 @@ test-suite plutus-use-cases-test Spec.Rollup Spec.Stablecoin Spec.Uniswap + Spec.Uniswap.Endpoints Spec.TokenAccount Spec.Vesting default-language: Haskell2010 @@ -136,8 +146,10 @@ test-suite plutus-use-cases-test plutus-contract -any, plutus-contract-certification -any, plutus-ledger -any, + plutus-ledger-api, plutus-ledger-constraints -any, - plutus-use-cases -any + plutus-use-cases -any, + playground-common -any build-depends: base >=4.9 && <5, bytestring -any, diff --git a/plutus-use-cases/src/Plutus/Contracts/Auction.hs b/plutus-use-cases/src/Plutus/Contracts/Auction.hs index 81ec6f82d0..3d4b8bf763 100644 --- a/plutus-use-cases/src/Plutus/Contracts/Auction.hs +++ b/plutus-use-cases/src/Plutus/Contracts/Auction.hs @@ -11,6 +11,7 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-} +{-# OPTIONS_GHC -g -fplugin-opt PlutusTx.Plugin:coverage-all #-} module Plutus.Contracts.Auction( AuctionState(..), AuctionInput(..), @@ -23,7 +24,8 @@ module Plutus.Contracts.Auction( AuctionOutput(..), AuctionError(..), ThreadToken, - SM.getThreadToken + SM.getThreadToken, + covIdx ) where import Control.Lens (makeClassyPrisms) @@ -45,6 +47,8 @@ import Plutus.Contract.StateMachine (State (..), StateMachine (..), StateMachine import Plutus.Contract.StateMachine qualified as SM import Plutus.Contract.Util (loopM) import PlutusTx qualified +import PlutusTx.Code +import PlutusTx.Coverage import PlutusTx.Prelude import Prelude qualified as Haskell @@ -361,3 +365,6 @@ auctionBuyer currency params = do Transition _ (Ongoing s) -> loop s InitialState (Ongoing s) -> loop s _ -> logWarn CurrentStateNotFound + +covIdx :: CoverageIndex +covIdx = getCovIdx $$(PlutusTx.compile [|| mkValidator ||]) diff --git a/plutus-use-cases/src/Plutus/Contracts/Escrow.hs b/plutus-use-cases/src/Plutus/Contracts/Escrow.hs index 939a8bcc26..5f66e1be02 100644 --- a/plutus-use-cases/src/Plutus/Contracts/Escrow.hs +++ b/plutus-use-cases/src/Plutus/Contracts/Escrow.hs @@ -13,6 +13,7 @@ {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -fplugin-opt PlutusTx.Plugin:debug-context #-} +{-# OPTIONS_GHC -g -fplugin-opt PlutusTx.Plugin:coverage-all #-} -- | A general-purpose escrow contract in Plutus module Plutus.Contracts.Escrow( -- $escrow @@ -40,6 +41,8 @@ module Plutus.Contracts.Escrow( , EscrowSchema -- * Exposed for test endpoints , Action(..) + -- * Coverage + , covIdx ) where import Control.Lens (makeClassyPrisms, review, view) @@ -64,6 +67,8 @@ import Ledger.Value (Value, geq, lt) import Plutus.Contract import Plutus.Contract.Typed.Tx qualified as Typed import PlutusTx qualified +import PlutusTx.Code +import PlutusTx.Coverage import PlutusTx.Prelude hiding (Applicative (..), Semigroup (..), check, foldMap) import Prelude (Semigroup (..), foldMap) @@ -356,3 +361,6 @@ payRedeemRefund params vl = do -- Pay the value 'vl' into the contract _ <- pay inst params vl go + +covIdx :: CoverageIndex +covIdx = getCovIdx $$(PlutusTx.compile [|| validate ||]) diff --git a/plutus-use-cases/src/Plutus/Contracts/Tutorial/Escrow.hs b/plutus-use-cases/src/Plutus/Contracts/Tutorial/Escrow.hs new file mode 100644 index 0000000000..e1038306a8 --- /dev/null +++ b/plutus-use-cases/src/Plutus/Contracts/Tutorial/Escrow.hs @@ -0,0 +1,321 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fplugin-opt PlutusTx.Plugin:debug-context #-} +{-# OPTIONS_GHC -g -fplugin-opt PlutusTx.Plugin:coverage-all #-} + +-- | A general-purpose escrow contract in Plutus +module Plutus.Contracts.Tutorial.Escrow( + -- $escrow + Escrow + , EscrowError(..) + , AsEscrowError(..) + , EscrowParams(..) + , EscrowTarget(..) + , payToPaymentPubKeyTarget + , targetTotal + , escrowContract + , typedValidator + -- * Actions + , pay + , payEp + , redeem + , redeemEp + , refund + , refundEp + , RedeemFailReason(..) + , RedeemSuccess(..) + , RefundSuccess(..) + , EscrowSchema + -- * Exposed for test endpoints + , Action(..) + -- * Coverage + , covIdx + ) where + +import Control.Lens (makeClassyPrisms, review, view) +import Control.Monad (void) +import Control.Monad.Error.Lens (throwing) +import Data.Aeson (FromJSON, ToJSON) +import GHC.Generics (Generic) + +import Ledger (Datum (..), DatumHash, PaymentPubKeyHash (unPaymentPubKeyHash), TxId, getCardanoTxId, txSignedBy, + valuePaidTo) +import Ledger qualified +import Ledger.Constraints (TxConstraints) +import Ledger.Constraints qualified as Constraints +import Ledger.Contexts (ScriptContext (..), TxInfo (..)) +import Ledger.Tx qualified as Tx +import Ledger.Typed.Scripts (TypedValidator) +import Ledger.Typed.Scripts qualified as Scripts +import Ledger.Value (Value, geq, lt) + +import Plutus.Contract +import Plutus.Contract.Typed.Tx qualified as Typed +import PlutusTx qualified +import PlutusTx.Code +import PlutusTx.Coverage +import PlutusTx.Prelude hiding (Applicative (..), Semigroup (..), check, foldMap) + +import Prelude (Semigroup (..), foldMap) +import Prelude qualified as Haskell + +type EscrowSchema = + Endpoint "pay-escrow" Value + .\/ Endpoint "redeem-escrow" () + .\/ Endpoint "refund-escrow" () + +data RedeemFailReason = DeadlinePassed | NotEnoughFundsAtAddress + deriving stock (Haskell.Eq, Haskell.Show, Generic) + deriving anyclass (ToJSON, FromJSON) + +data EscrowError = + RedeemFailed RedeemFailReason + | RefundFailed + | EContractError ContractError + deriving stock (Haskell.Show, Generic) + deriving anyclass (ToJSON, FromJSON) + +makeClassyPrisms ''EscrowError + +instance AsContractError EscrowError where + _ContractError = _EContractError + +-- This is a simplified version of the Escrow contract, which does not +-- enforce a deadline on payments or redemption, and also allows +-- Refund actions at any time. + +-- $escrow +-- The escrow contract implements the exchange of value between multiple +-- parties. It is defined by a list of targets (public keys and script +-- addresses, each associated with a value). It works similar to the +-- crowdfunding contract in that the contributions can be made independently, +-- and the funds can be unlocked only by a transaction that pays the correct +-- amount to each target. A refund is possible if the outputs locked by the +-- contract have not been spent by the deadline. (Compared to the crowdfunding +-- contract, the refund policy is simpler because here because there is no +-- "collection period" during which the outputs may be spent after the deadline +-- has passed. This is because we're assuming that the participants in the +-- escrow contract will make their deposits as quickly as possible after +-- agreeing on a deal) +-- +-- The contract supports two modes of operation, manual and automatic. In +-- manual mode, all actions are driven by endpoints that exposed via 'payEp' +-- 'redeemEp' and 'refundEp'. In automatic mode, the 'pay', 'redeem' and +-- 'refund'actions start immediately. This mode is useful when the escrow is +-- called from within another contract, for example during setup (collection of +-- the initial deposits). + +-- | Defines where the money should go. Usually we have `d = Datum` (when +-- defining `EscrowTarget` values in off-chain code). Sometimes we have +-- `d = DatumHash` (when checking the hashes in on-chain code) +data EscrowTarget d = + PaymentPubKeyTarget PaymentPubKeyHash Value + deriving (Haskell.Functor) + +PlutusTx.makeLift ''EscrowTarget + +-- | An 'EscrowTarget' that pays the value to a public key address. +payToPaymentPubKeyTarget :: PaymentPubKeyHash -> Value -> EscrowTarget d +payToPaymentPubKeyTarget = PaymentPubKeyTarget + +-- | Definition of an escrow contract, consisting of a deadline and a list of targets +data EscrowParams d = + EscrowParams + { escrowTargets :: [EscrowTarget d] + -- ^ Where the money should go. For each target, the contract checks that + -- the output 'mkTxOutput' of the target is present in the spending + -- transaction. + } deriving (Haskell.Functor) + +PlutusTx.makeLift ''EscrowParams + +-- | The total 'Value' that must be paid into the escrow contract +-- before it can be unlocked +targetTotal :: EscrowParams d -> Value +targetTotal = foldl (\vl tgt -> vl + targetValue tgt) mempty . escrowTargets + +-- | The 'Value' specified by an 'EscrowTarget' +targetValue :: EscrowTarget d -> Value +targetValue = \case + PaymentPubKeyTarget _ vl -> vl + +-- | Create a 'Ledger.TxOut' value for the target +mkTx :: EscrowTarget Datum -> TxConstraints Action PaymentPubKeyHash +mkTx = \case + PaymentPubKeyTarget pkh vl -> + Constraints.mustPayToPubKey pkh vl + +data Action = Redeem | Refund + +data Escrow +instance Scripts.ValidatorTypes Escrow where + type instance RedeemerType Escrow = Action + type instance DatumType Escrow = PaymentPubKeyHash + +PlutusTx.unstableMakeIsData ''Action +PlutusTx.makeLift ''Action + +{-# INLINABLE meetsTarget #-} +-- | @ptx `meetsTarget` tgt@ if @ptx@ pays at least @targetValue tgt@ to the +-- target address. +-- +-- The reason why this does not require the target amount to be equal +-- to the actual amount is to enable any excess funds consumed by the +-- spending transaction to be paid to target addresses. This may happen if +-- the target address is also used as a change address for the spending +-- transaction, and allowing the target to be exceed prevents outsiders from +-- poisoning the contract by adding arbitrary outputs to the script address. +meetsTarget :: TxInfo -> EscrowTarget DatumHash -> Bool +meetsTarget ptx = \case + PaymentPubKeyTarget pkh vl -> + valuePaidTo ptx (unPaymentPubKeyHash pkh) `geq` vl + +{-# INLINABLE validate #-} +validate :: EscrowParams DatumHash -> PaymentPubKeyHash -> Action -> ScriptContext -> Bool +validate EscrowParams{escrowTargets} contributor action ScriptContext{scriptContextTxInfo} = + case action of + Redeem -> + traceIfFalse "meetsTarget" (all (meetsTarget scriptContextTxInfo) escrowTargets) + Refund -> + traceIfFalse "txSignedBy" (scriptContextTxInfo `txSignedBy` unPaymentPubKeyHash contributor) + +typedValidator :: EscrowParams Datum -> Scripts.TypedValidator Escrow +typedValidator escrow = go (Haskell.fmap Ledger.datumHash escrow) where + go = Scripts.mkTypedValidatorParam @Escrow + $$(PlutusTx.compile [|| validate ||]) + $$(PlutusTx.compile [|| wrap ||]) + wrap = Scripts.wrapValidator + +escrowContract + :: EscrowParams Datum + -> Contract () EscrowSchema EscrowError () +escrowContract escrow = + let inst = typedValidator escrow + payAndRefund = endpoint @"pay-escrow" $ \vl -> do + _ <- pay inst escrow vl + refund inst escrow + in selectList + [ void payAndRefund + , void $ redeemEp escrow + ] + +-- | 'pay' with an endpoint that gets the owner's public key and the +-- contribution. +payEp :: + forall w s e. + ( HasEndpoint "pay-escrow" Value s + , AsEscrowError e + ) + => EscrowParams Datum + -> Promise w s e TxId +payEp escrow = promiseMap + (mapError (review _EContractError)) + (endpoint @"pay-escrow" $ pay (typedValidator escrow) escrow) + +-- | Pay some money into the escrow contract. +pay :: + forall w s e. + ( AsContractError e + ) + => TypedValidator Escrow + -- ^ The instance + -> EscrowParams Datum + -- ^ The escrow contract + -> Value + -- ^ How much money to pay in + -> Contract w s e TxId +pay inst _escrow vl = do + pk <- ownPaymentPubKeyHash + let tx = Constraints.mustPayToTheScript pk vl + utx <- mkTxConstraints (Constraints.typedValidatorLookups inst) tx + getCardanoTxId <$> submitUnbalancedTx (Constraints.adjustUnbalancedTx utx) + +newtype RedeemSuccess = RedeemSuccess TxId + deriving (Haskell.Eq, Haskell.Show) + +-- | 'redeem' with an endpoint. +redeemEp :: + forall w s e. + ( HasEndpoint "redeem-escrow" () s + , AsEscrowError e + ) + => EscrowParams Datum + -> Promise w s e RedeemSuccess +redeemEp escrow = promiseMap + (mapError (review _EscrowError)) + (endpoint @"redeem-escrow" $ \() -> redeem (typedValidator escrow) escrow) + +-- | Redeem all outputs at the contract address using a transaction that +-- has all the outputs defined in the contract's list of targets. +redeem :: + forall w s e. + ( AsEscrowError e + ) + => TypedValidator Escrow + -> EscrowParams Datum + -> Contract w s e RedeemSuccess +redeem inst escrow = mapError (review _EscrowError) $ do + let addr = Scripts.validatorAddress inst + unspentOutputs <- utxosAt addr + let + tx = Typed.collectFromScript unspentOutputs Redeem + <> foldMap mkTx (escrowTargets escrow) + if foldMap (view Tx.ciTxOutValue) unspentOutputs `lt` targetTotal escrow + then throwing _RedeemFailed NotEnoughFundsAtAddress + else do + utx <- mkTxConstraints ( Constraints.typedValidatorLookups inst + <> Constraints.unspentOutputs unspentOutputs + ) tx + RedeemSuccess . getCardanoTxId <$> submitUnbalancedTx (Constraints.adjustUnbalancedTx utx) + +newtype RefundSuccess = RefundSuccess TxId + deriving newtype (Haskell.Eq, Haskell.Show, Generic) + deriving anyclass (ToJSON, FromJSON) + +-- | 'refund' with an endpoint. +refundEp :: + forall w s. + ( HasEndpoint "refund-escrow" () s + ) + => EscrowParams Datum + -> Promise w s EscrowError RefundSuccess +refundEp escrow = endpoint @"refund-escrow" $ \() -> refund (typedValidator escrow) escrow + +-- | Claim a refund of the contribution. +refund :: + forall w s. + TypedValidator Escrow + -> EscrowParams Datum + -> Contract w s EscrowError RefundSuccess +refund inst _escrow = do + pk <- ownPaymentPubKeyHash + unspentOutputs <- utxosAt (Scripts.validatorAddress inst) + let flt _ ciTxOut = either id Ledger.datumHash (Tx._ciTxOutDatum ciTxOut) == Ledger.datumHash (Datum (PlutusTx.toBuiltinData pk)) + tx' = Typed.collectFromScriptFilter flt unspentOutputs Refund + if Constraints.modifiesUtxoSet tx' + then do + utx <- mkTxConstraints ( Constraints.typedValidatorLookups inst + <> Constraints.unspentOutputs unspentOutputs + ) tx' + RefundSuccess . getCardanoTxId <$> submitUnbalancedTx (Constraints.adjustUnbalancedTx utx) + else throwing _RefundFailed () + +covIdx :: CoverageIndex +covIdx = getCovIdx $$(PlutusTx.compile [|| validate ||]) + <> getCovIdx $$(PlutusTx.compile [|| wrap ||]) + where + wrap :: (PaymentPubKeyHash -> Action -> ScriptContext -> Bool) -> + Scripts.WrappedValidatorType + wrap = Scripts.wrapValidator diff --git a/plutus-use-cases/src/Plutus/Contracts/Tutorial/EscrowStrict.hs b/plutus-use-cases/src/Plutus/Contracts/Tutorial/EscrowStrict.hs new file mode 100644 index 0000000000..8ba3c9a382 --- /dev/null +++ b/plutus-use-cases/src/Plutus/Contracts/Tutorial/EscrowStrict.hs @@ -0,0 +1,321 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE NoImplicitPrelude #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -fplugin-opt PlutusTx.Plugin:debug-context #-} +-- | A general-purpose escrow contract in Plutus +module Plutus.Contracts.Tutorial.EscrowStrict( + -- $escrow + Escrow + , EscrowError(..) + , AsEscrowError(..) + , EscrowParams(..) + , EscrowTarget(..) + , payToScriptTarget + , payToPaymentPubKeyTarget + , targetTotal + , escrowContract + , typedValidator + -- * Actions + , pay + , payEp + , redeem + , redeemEp + , refund + , refundEp + , RedeemFailReason(..) + , RedeemSuccess(..) + , RefundSuccess(..) + , EscrowSchema + -- * Exposed for test endpoints + , Action(..) + ) where + +import Control.Lens (makeClassyPrisms, review, view) +import Control.Monad (void) +import Control.Monad.Error.Lens (throwing) +import Data.Aeson (FromJSON, ToJSON) +import GHC.Generics (Generic) + +import Ledger (Datum (..), DatumHash, PaymentPubKeyHash (unPaymentPubKeyHash), TxId, ValidatorHash, getCardanoTxId, + scriptOutputsAt, txSignedBy, valuePaidTo) +import Ledger qualified +import Ledger.Constraints (TxConstraints) +import Ledger.Constraints qualified as Constraints +import Ledger.Contexts (ScriptContext (..), TxInfo (..)) +import Ledger.Tx qualified as Tx +import Ledger.Typed.Scripts (TypedValidator) +import Ledger.Typed.Scripts qualified as Scripts +import Ledger.Value (Value, geq, lt) + +import Plutus.Contract +import Plutus.Contract.Typed.Tx qualified as Typed +import PlutusTx qualified +import PlutusTx.Prelude hiding (Applicative (..), Semigroup (..), check, foldMap) + +import Prelude (Semigroup (..), foldMap) +import Prelude qualified as Haskell + +type EscrowSchema = + Endpoint "pay-escrow" Value + .\/ Endpoint "redeem-escrow" () + .\/ Endpoint "refund-escrow" () + +data RedeemFailReason = DeadlinePassed | NotEnoughFundsAtAddress + deriving stock (Haskell.Eq, Haskell.Show, Generic) + deriving anyclass (ToJSON, FromJSON) + +data EscrowError = + RedeemFailed RedeemFailReason + | RefundFailed + | EContractError ContractError + deriving stock (Haskell.Show, Generic) + deriving anyclass (ToJSON, FromJSON) + +makeClassyPrisms ''EscrowError + +instance AsContractError EscrowError where + _ContractError = _EContractError + +-- This is a simplified version of the Escrow contract, which does not +-- enforce a deadline on payments or redemption, and also allows +-- Refund actions at any time. + +-- In addition, this version only allows redeem when the contract +-- contains *exactly* the right value. + +-- $escrow +-- The escrow contract implements the exchange of value between multiple +-- parties. It is defined by a list of targets (public keys and script +-- addresses, each associated with a value). It works similar to the +-- crowdfunding contract in that the contributions can be made independently, +-- and the funds can be unlocked only by a transaction that pays the correct +-- amount to each target. A refund is possible if the outputs locked by the +-- contract have not been spent by the deadline. (Compared to the crowdfunding +-- contract, the refund policy is simpler because here because there is no +-- "collection period" during which the outputs may be spent after the deadline +-- has passed. This is because we're assuming that the participants in the +-- escrow contract will make their deposits as quickly as possible after +-- agreeing on a deal) +-- +-- The contract supports two modes of operation, manual and automatic. In +-- manual mode, all actions are driven by endpoints that exposed via 'payEp' +-- 'redeemEp' and 'refundEp'. In automatic mode, the 'pay', 'redeem' and +-- 'refund'actions start immediately. This mode is useful when the escrow is +-- called from within another contract, for example during setup (collection of +-- the initial deposits). + +-- | Defines where the money should go. Usually we have `d = Datum` (when +-- defining `EscrowTarget` values in off-chain code). Sometimes we have +-- `d = DatumHash` (when checking the hashes in on-chain code) +data EscrowTarget d = + PaymentPubKeyTarget PaymentPubKeyHash Value + | ScriptTarget ValidatorHash d Value + deriving (Haskell.Functor) + +PlutusTx.makeLift ''EscrowTarget + +-- | An 'EscrowTarget' that pays the value to a public key address. +payToPaymentPubKeyTarget :: PaymentPubKeyHash -> Value -> EscrowTarget d +payToPaymentPubKeyTarget = PaymentPubKeyTarget + +-- | An 'EscrowTarget' that pays the value to a script address, with the +-- given data script. +payToScriptTarget :: ValidatorHash -> Datum -> Value -> EscrowTarget Datum +payToScriptTarget = ScriptTarget + +-- | Definition of an escrow contract, consisting of a deadline and a list of targets +data EscrowParams d = + EscrowParams + { escrowTargets :: [EscrowTarget d] + -- ^ Where the money should go. For each target, the contract checks that + -- the output 'mkTxOutput' of the target is present in the spending + -- transaction. + } deriving (Haskell.Functor) + +PlutusTx.makeLift ''EscrowParams + +-- | The total 'Value' that must be paid into the escrow contract +-- before it can be unlocked +targetTotal :: EscrowParams d -> Value +targetTotal = foldl (\vl tgt -> vl + targetValue tgt) mempty . escrowTargets + +-- | The 'Value' specified by an 'EscrowTarget' +targetValue :: EscrowTarget d -> Value +targetValue = \case + PaymentPubKeyTarget _ vl -> vl + ScriptTarget _ _ vl -> vl + +-- | Create a 'Ledger.TxOut' value for the target +mkTx :: EscrowTarget Datum -> TxConstraints Action PaymentPubKeyHash +mkTx = \case + PaymentPubKeyTarget pkh vl -> + Constraints.mustPayToPubKey pkh vl + ScriptTarget vs ds vl -> + Constraints.mustPayToOtherScript vs ds vl + +data Action = Redeem | Refund + +data Escrow +instance Scripts.ValidatorTypes Escrow where + type instance RedeemerType Escrow = Action + type instance DatumType Escrow = PaymentPubKeyHash + +PlutusTx.unstableMakeIsData ''Action +PlutusTx.makeLift ''Action + +{-# INLINABLE meetsTarget #-} +-- | @ptx `meetsTarget` tgt@ if @ptx@ pays exactly @targetValue tgt@ to the +-- target address. This is buggy behaviour: see Spec.Escrow for an explanation. +-- +meetsTarget :: TxInfo -> EscrowTarget DatumHash -> Bool +meetsTarget ptx = \case + PaymentPubKeyTarget pkh vl -> + valuePaidTo ptx (unPaymentPubKeyHash pkh) `geq` vl + ScriptTarget validatorHash dataValue vl -> + case scriptOutputsAt validatorHash ptx of + [(dataValue', vl')] -> + traceIfFalse "dataValue" (dataValue' == dataValue) + && traceIfFalse "value" (vl' == vl) + _ -> False + +{-# INLINABLE validate #-} +validate :: EscrowParams DatumHash -> PaymentPubKeyHash -> Action -> ScriptContext -> Bool +validate EscrowParams{escrowTargets} contributor action ScriptContext{scriptContextTxInfo} = + case action of + Redeem -> + traceIfFalse "meetsTarget" (all (meetsTarget scriptContextTxInfo) escrowTargets) + Refund -> + traceIfFalse "txSignedBy" (scriptContextTxInfo `txSignedBy` unPaymentPubKeyHash contributor) + +typedValidator :: EscrowParams Datum -> Scripts.TypedValidator Escrow +typedValidator escrow = go (Haskell.fmap Ledger.datumHash escrow) where + go = Scripts.mkTypedValidatorParam @Escrow + $$(PlutusTx.compile [|| validate ||]) + $$(PlutusTx.compile [|| wrap ||]) + wrap = Scripts.wrapValidator + +escrowContract + :: EscrowParams Datum + -> Contract () EscrowSchema EscrowError () +escrowContract escrow = + let inst = typedValidator escrow + payAndRefund = endpoint @"pay-escrow" $ \vl -> do + _ <- pay inst escrow vl + refund inst escrow + in selectList + [ void payAndRefund + , void $ redeemEp escrow + ] + +-- | 'pay' with an endpoint that gets the owner's public key and the +-- contribution. +payEp :: + forall w s e. + ( HasEndpoint "pay-escrow" Value s + , AsEscrowError e + ) + => EscrowParams Datum + -> Promise w s e TxId +payEp escrow = promiseMap + (mapError (review _EContractError)) + (endpoint @"pay-escrow" $ pay (typedValidator escrow) escrow) + +-- | Pay some money into the escrow contract. +pay :: + forall w s e. + ( AsContractError e + ) + => TypedValidator Escrow + -- ^ The instance + -> EscrowParams Datum + -- ^ The escrow contract + -> Value + -- ^ How much money to pay in + -> Contract w s e TxId +pay inst _escrow vl = do + pk <- ownPaymentPubKeyHash + let tx = Constraints.mustPayToTheScript pk vl + utx <- mkTxConstraints (Constraints.typedValidatorLookups inst) tx + getCardanoTxId <$> submitUnbalancedTx (Constraints.adjustUnbalancedTx utx) + +newtype RedeemSuccess = RedeemSuccess TxId + deriving (Haskell.Eq, Haskell.Show) + +-- | 'redeem' with an endpoint. +redeemEp :: + forall w s e. + ( HasEndpoint "redeem-escrow" () s + , AsEscrowError e + ) + => EscrowParams Datum + -> Promise w s e RedeemSuccess +redeemEp escrow = promiseMap + (mapError (review _EscrowError)) + (endpoint @"redeem-escrow" $ \() -> redeem (typedValidator escrow) escrow) + +-- | Redeem all outputs at the contract address using a transaction that +-- has all the outputs defined in the contract's list of targets. +redeem :: + forall w s e. + ( AsEscrowError e + ) + => TypedValidator Escrow + -> EscrowParams Datum + -> Contract w s e RedeemSuccess +redeem inst escrow = mapError (review _EscrowError) $ do + let addr = Scripts.validatorAddress inst + unspentOutputs <- utxosAt addr + let + tx = Typed.collectFromScript unspentOutputs Redeem + <> foldMap mkTx (escrowTargets escrow) + if foldMap (view Tx.ciTxOutValue) unspentOutputs `lt` targetTotal escrow + then throwing _RedeemFailed NotEnoughFundsAtAddress + else do + utx <- mkTxConstraints ( Constraints.typedValidatorLookups inst + <> Constraints.unspentOutputs unspentOutputs + ) tx + RedeemSuccess . getCardanoTxId <$> submitUnbalancedTx (Constraints.adjustUnbalancedTx utx) + +newtype RefundSuccess = RefundSuccess TxId + deriving newtype (Haskell.Eq, Haskell.Show, Generic) + deriving anyclass (ToJSON, FromJSON) + +-- | 'refund' with an endpoint. +refundEp :: + forall w s. + ( HasEndpoint "refund-escrow" () s + ) + => EscrowParams Datum + -> Promise w s EscrowError RefundSuccess +refundEp escrow = endpoint @"refund-escrow" $ \() -> refund (typedValidator escrow) escrow + +-- | Claim a refund of the contribution. +refund :: + forall w s. + TypedValidator Escrow + -> EscrowParams Datum + -> Contract w s EscrowError RefundSuccess +refund inst _escrow = do + pk <- ownPaymentPubKeyHash + unspentOutputs <- utxosAt (Scripts.validatorAddress inst) + let flt _ ciTxOut = either id Ledger.datumHash (Tx._ciTxOutDatum ciTxOut) == Ledger.datumHash (Datum (PlutusTx.toBuiltinData pk)) + tx' = Typed.collectFromScriptFilter flt unspentOutputs Refund + if Constraints.modifiesUtxoSet tx' + then do + utx <- mkTxConstraints ( Constraints.typedValidatorLookups inst + <> Constraints.unspentOutputs unspentOutputs + ) tx' + RefundSuccess . getCardanoTxId <$> submitUnbalancedTx (Constraints.adjustUnbalancedTx utx) + else throwing _RefundFailed () + diff --git a/plutus-use-cases/src/Plutus/Contracts/Uniswap/OffChain.hs b/plutus-use-cases/src/Plutus/Contracts/Uniswap/OffChain.hs index 650c788a61..577da6789a 100644 --- a/plutus-use-cases/src/Plutus/Contracts/Uniswap/OffChain.hs +++ b/plutus-use-cases/src/Plutus/Contracts/Uniswap/OffChain.hs @@ -29,6 +29,10 @@ module Plutus.Contracts.Uniswap.OffChain , start, create, add, remove, close, swap, pools , ownerEndpoint, userEndpoints , findSwapA, findSwapB, covIdx + -- exported for defining test endpoints + , findUniswapFactoryAndPool, uniswapInstance, liquidityPolicy + , uniswapScript, poolStateCoin, liquidityCurrency, lpTicker + , calculateRemoval, funds ) where import Control.Lens (view) diff --git a/plutus-use-cases/test/Spec/Auction.hs b/plutus-use-cases/test/Spec/Auction.hs index bb771a677f..7fe8a10d15 100644 --- a/plutus-use-cases/test/Spec/Auction.hs +++ b/plutus-use-cases/test/Spec/Auction.hs @@ -17,6 +17,11 @@ module Spec.Auction , prop_Auction , prop_FinishAuction , prop_NoLockedFunds + , prop_NoLockedFundsFast + , prop_SanityCheckAssertions + , prop_Whitelist + , prop_CrashTolerance + , check_propAuctionWithCoverage ) where import Control.Lens hiding (elements) @@ -41,6 +46,8 @@ import Ledger qualified import Ledger.TimeSlot (SlotConfig) import Ledger.TimeSlot qualified as TimeSlot import Plutus.Contract.Test.ContractModel +import Plutus.Contract.Test.ContractModel.CrashTolerance +import Plutus.Contract.Test.Coverage import Plutus.Contracts.Auction hiding (Bid) import Plutus.Trace.Emulator qualified as Trace import PlutusTx.Monoid (inv) @@ -177,7 +184,7 @@ instance ContractModel AuctionModel where SellerH :: ContractInstanceKey AuctionModel AuctionOutput SellerSchema AuctionError () BuyerH :: Wallet -> ContractInstanceKey AuctionModel AuctionOutput BuyerSchema AuctionError () - data Action AuctionModel = Init Wallet | Bid Wallet Integer + data Action AuctionModel = Init | Bid Wallet Integer deriving (Eq, Show, Data) initialState = AuctionModel @@ -187,7 +194,10 @@ instance ContractModel AuctionModel where , _phase = NotStarted } - initialInstances = StartContract SellerH () : [ StartContract (BuyerH w) () | w <- [w2, w3, w4] ] + initialInstances = [ StartContract (BuyerH w) () | w <- [w2, w3, w4] ] + + startInstances _ Init = [StartContract SellerH ()] + startInstances _ _ = [] instanceWallet SellerH = w1 instanceWallet (BuyerH w) = w @@ -197,27 +207,22 @@ instance ContractModel AuctionModel where arbitraryAction s | p /= NotStarted = do - oneof [ Bid w <$> chooseBid (lo,hi) - | w <- [w2, w3, w4] - , let (lo,hi) = validBidRange s w - , lo <= hi ] - | otherwise = pure $ Init w1 + oneof [ Bid w <$> validBid + | w <- [w2, w3, w4] ] + | otherwise = pure $ Init where p = s ^. contractState . phase - - waitProbability s - | s ^. contractState . phase /= NotStarted - , all (uncurry (>) . validBidRange s) [w2, w3, w4] = 1 - | otherwise = 0.1 - - precondition s (Init _) = s ^. contractState . phase == NotStarted - precondition s cmd = s ^. contractState . phase /= NotStarted && - case cmd of - -- In order to place a bid, we need to satisfy the constraint where - -- each tx output must have at least N Ada. - Bid w bid -> let (lo,hi) = validBidRange s w in - lo <= bid && bid <= hi - _ -> True + b = s ^. contractState . currentBid + validBid = choose ((b+1) `max` Ada.getLovelace Ledger.minAdaTxOut, + b + Ada.getLovelace (Ada.adaOf 100)) + + precondition s Init = s ^. contractState . phase == NotStarted + precondition s (Bid _ bid) = + -- In order to place a bid, we need to satisfy the constraint where + -- each tx output must have at least N Ada. + s ^. contractState . phase /= NotStarted && + bid >= Ada.getLovelace (Ledger.minAdaTxOut) && + bid > s ^. contractState . currentBid nextReactiveState slot' = do end <- viewContractState endSlot @@ -228,27 +233,31 @@ instance ContractModel AuctionModel where phase .= AuctionOver deposit w $ Ada.toValue Ledger.minAdaTxOut <> theToken deposit w1 $ Ada.lovelaceValueOf bid + {- + w1change <- viewModelState $ balanceChange w1 -- since the start of the test + assertSpec ("w1 final balance is wrong:\n "++show w1change) $ + w1change == toSymValue (inv theToken <> Ada.lovelaceValueOf bid) || + w1change == mempty + -} - -- This command is only for setting up the model state with theToken nextState cmd = do - slot <- viewModelState currentSlot - end <- viewContractState endSlot case cmd of - Init _ -> do + Init -> do phase .= Bidding withdraw w1 $ Ada.toValue Ledger.minAdaTxOut <> theToken wait 3 Bid w bid -> do - current <- viewContractState currentBid - leader <- viewContractState winner - when (slot < end) $ do + currentPhase <- viewContractState phase + when (currentPhase == Bidding) $ do + current <- viewContractState currentBid + leader <- viewContractState winner withdraw w $ Ada.lovelaceValueOf bid deposit leader $ Ada.lovelaceValueOf current currentBid .= bid winner .= w wait 2 - perform _ _ _ (Init _) = delay 3 + perform _ _ _ Init = delay 3 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 @@ -260,41 +269,9 @@ instance ContractModel AuctionModel where Trace.callEndpoint @"bid" (handle $ BuyerH w) (Ada.lovelaceOf bid) delay 1 - shrinkAction _ (Init _) = [] + shrinkAction _ Init = [] shrinkAction _ (Bid w v) = [ Bid w v' | v' <- shrink v ] - monitoring _ (Bid _ bid) = - classify (Ada.lovelaceOf bid == Ada.adaOf 100 - (Ledger.minAdaTxOut <> Ledger.maxFee)) - "Maximum bid reached" - monitoring _ _ = id - --- 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. -validBidRange :: ModelState AuctionModel -> Wallet -> (Integer,Integer) -validBidRange s _w = - let currentWalletBalance = Ada.adaOf 100 -- this is approximate - current = s ^. contractState . currentBid - in ( (current+1) `max` Ada.getLovelace Ledger.minAdaTxOut, - Ada.getLovelace (currentWalletBalance - (Ledger.minAdaTxOut <> Ledger.maxFee)) - ) - --- When we choose a bid, we prefer a lower bid to a higher --- one. Otherwise longer tests very often reach the maximum possible --- bid, which makes little sense. -chooseBid :: (Integer,Integer) -> Gen Integer -chooseBid (lo,hi) - | lo==hi = pure lo - | lo