-
Notifications
You must be signed in to change notification settings - Fork 213
/
Auction.hs
373 lines (320 loc) · 14.1 KB
/
Auction.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
{-# 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 qualified as Ledger
import Ledger.Ada qualified as Ada
import Plutus.Contract hiding (currentSlot)
import Plutus.Contract.Test hiding (not)
import Plutus.Script.Utils.V1.Generators (someTokenValue)
import Streaming.Prelude qualified as S
import Wallet.Emulator.Folds qualified as Folds
import Wallet.Emulator.Stream qualified as Stream
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)
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
}
-- | 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)
& allowBigTransactions
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
data AuctionModel = AuctionModel
{ _currentBid :: Integer
, _winner :: Wallet
, _endSlot :: Slot
, _phase :: Phase
} deriving (Show, Eq, Data)
data Phase = NotStarted | Bidding | AuctionOver
deriving (Eq, Show, Data)
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 ()
data Action AuctionModel = Init | Bid Wallet Integer
deriving (Eq, Show, Data)
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 (Ada.adaOf 2),
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 (Ada.adaOf 2) &&
bid > s ^. contractState . currentBid
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 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
-}
nextState cmd = do
case cmd of
Init -> do
phase .= Bidding
withdraw w1 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
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 ]
monitoring _ (Bid _ bid) =
classify (Ada.lovelaceOf bid == Ada.adaOf 100 - (Ledger.minAdaTxOut <> Ledger.maxFee))
"Maximum bid reached"
monitoring _ _ = id
prop_Auction :: Actions AuctionModel -> Property
prop_Auction script =
propRunActionsWithOptions (set minLogLevel Info options) defaultCoverageOptions
(\ _ -> pure True) -- TODO: check termination
script
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
-- | This does not hold! The Payout transition is triggered by the sellers off-chain code, so if the
-- seller walks away the buyer will not get their token (unless going around the off-chain code
-- and building a Payout transaction manually).
noLockProof :: NoLockedFundsProof AuctionModel
noLockProof = defaultNLFP
{ nlfpMainStrategy = finishingStrategy
, nlfpWalletStrategy = const finishingStrategy }
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
instance CrashTolerance AuctionModel where
available (Bid w _) alive = (Key $ BuyerH w) `elem` alive
available Init _ = True
restartArguments _ BuyerH{} = ()
restartArguments _ SellerH{} = ()
prop_CrashTolerance :: Actions (WithCrashTolerance AuctionModel) -> Property
prop_CrashTolerance =
propRunActionsWithOptions (set minLogLevel Critical options) defaultCoverageOptions
(\ _ -> pure True)
check_propAuctionWithCoverage :: IO ()
check_propAuctionWithCoverage = do
cr <- quickCheckWithCoverage stdArgs (set coverageIndex covIdx $ defaultCoverageOptions) $ \covopts ->
withMaxSuccess 1000 $
propRunActionsWithOptions @AuctionModel
(set minLogLevel Critical options) covopts (const (pure True))
writeCoverageReport "Auction" cr
prop_doubleSatisfaction :: Actions AuctionModel -> Property
prop_doubleSatisfaction = checkDoubleSatisfactionWithOptions options defaultCoverageOptions
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 trace1WinningBid <> inv theToken)
.&&. walletFundsChange w2 (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 trace2WinningBid <> inv theToken)
.&&. walletFundsChange w2 (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)
, testProperty "prop_doubleSatisfaction fails" $
expectFailure $ noShrinking prop_doubleSatisfaction
]