@@ -20,7 +20,6 @@ import Data.Time.Clock.POSIX (posixSecondsToUTCTime)
20
20
import Hydra.Cardano.Api (
21
21
SlotNo (.. ),
22
22
mkTxOutDatumInline ,
23
- renderUTxO ,
24
23
selectLovelace ,
25
24
throwError ,
26
25
txOutAddress ,
@@ -40,7 +39,7 @@ import Hydra.Ledger (hashUTxO, utxoFromTx)
40
39
import Hydra.Ledger.Cardano (Tx , adjustUTxO , genTxOut , genUTxO1 )
41
40
import Hydra.Ledger.Cardano.Evaluate (evaluateTx )
42
41
import Hydra.Party (partyToChain )
43
- import Hydra.Snapshot (ConfirmedSnapshot (.. ), Snapshot (.. ), SnapshotNumber (.. ), getSnapshot , number )
42
+ import Hydra.Snapshot (ConfirmedSnapshot (.. ), Snapshot (.. ), SnapshotNumber (.. ), number )
44
43
import PlutusTx.Builtins (toBuiltin )
45
44
import Test.Hydra.Fixture qualified as Fixture
46
45
import Test.QuickCheck (Property , Smart (.. ), checkCoverage , cover , elements , forAll , frequency , ioProperty , oneof )
@@ -50,7 +49,7 @@ import Test.QuickCheck.StateModel (
50
49
Actions (.. ),
51
50
Any (.. ),
52
51
HasVariables (getAllVariables ),
53
- Polarity (PosPolarity ),
52
+ Polarity (.. ),
54
53
PostconditionM ,
55
54
Realized ,
56
55
RunModel (.. ),
@@ -80,6 +79,7 @@ prop_traces =
80
79
& cover 1 (countContests steps >= 2 ) " has multiple contests"
81
80
& cover 5 (closeNonInitial steps) " close with non initial snapshots"
82
81
& cover 5 (hasDecrement steps) " has successful decrements"
82
+ & cover 1 (hasNegativeDecrement steps) " has negative decrements"
83
83
where
84
84
hasFanout =
85
85
any $
@@ -118,10 +118,16 @@ prop_traces =
118
118
Decrement {} -> polarity == PosPolarity
119
119
_ -> False
120
120
121
+ hasNegativeDecrement =
122
+ any $
123
+ \ (_ := ActionWithPolarity {polarAction, polarity}) -> case polarAction of
124
+ Decrement {} -> polarity == NegPolarity
125
+ _ -> False
126
+
121
127
prop_runActions :: Actions Model -> Property
122
128
prop_runActions actions =
123
129
monadic runAppMProperty $ do
124
- print actions
130
+ -- print actions
125
131
void (runActions actions)
126
132
where
127
133
runAppMProperty :: AppM Property -> Property
@@ -209,13 +215,16 @@ instance StateModel Model where
209
215
oneof $
210
216
[ do
211
217
actor <- elements allActors
218
+ someUTxOToDecrement <-
219
+ if not (null utxoInHead) then oneof $ pure <$> [utxoInHead] else pure $ Set. fromList []
220
+
212
221
snapshot <-
213
222
ModelSnapshot
214
223
{ snapshotNumber = latestSnapshot
215
224
, snapshotUTxO = utxoInHead
216
- , decommitUTxO = mempty
225
+ , decommitUTxO = someUTxOToDecrement
217
226
}
218
- `orSometimes ` arbitrary
227
+ `orArbitrary ` arbitrary
219
228
pure $ Some $ Close {actor, snapshot}
220
229
]
221
230
<> [ do
@@ -227,20 +236,22 @@ instance StateModel Model where
227
236
, snapshotUTxO = Set. delete someUTxOToDecrement utxoInHead
228
237
, decommitUTxO = Set. fromList [someUTxOToDecrement]
229
238
}
230
- `orSometimes ` arbitrary
239
+ `orArbitrary ` arbitrary
231
240
pure $ Some Decrement {actor, snapshot}
232
241
| not (null utxoInHead)
233
242
]
234
243
Closed {} ->
235
244
oneof $
236
245
[ do
237
- let snapshot =
238
- ModelSnapshot
239
- { snapshotNumber = latestSnapshot
240
- , snapshotUTxO = utxoInHead
241
- , decommitUTxO = mempty
242
- }
243
- -- `orSometimes` arbitrary
246
+ someUTxOToDecrement <-
247
+ if not (null utxoInHead) then oneof $ pure <$> [utxoInHead] else pure $ Set. fromList []
248
+ snapshot <-
249
+ ModelSnapshot
250
+ { snapshotNumber = latestSnapshot
251
+ , snapshotUTxO = utxoInHead
252
+ , decommitUTxO = someUTxOToDecrement
253
+ }
254
+ `orArbitrary` arbitrary
244
255
pure $ Some $ Fanout {snapshot}
245
256
]
246
257
<> [ do
@@ -253,7 +264,7 @@ instance StateModel Model where
253
264
, snapshotUTxO = Set. delete someUTxOToDecrement utxoInHead
254
265
, decommitUTxO = Set. fromList [someUTxOToDecrement]
255
266
}
256
- `orSometimes ` arbitrary
267
+ `orArbitrary ` arbitrary
257
268
pure $ Some Contest {actor, snapshot}
258
269
| not (null utxoInHead)
259
270
]
@@ -265,7 +276,6 @@ instance StateModel Model where
265
276
Decrement {snapshot} ->
266
277
headState == Open
267
278
&& snapshotNumber snapshot > latestSnapshot
268
- && decommitUTxO snapshot `Set.isSubsetOf` utxoInHead
269
279
Close {snapshot} ->
270
280
headState == Open
271
281
&& if snapshotNumber snapshot == 0
@@ -277,11 +287,32 @@ instance StateModel Model where
277
287
headState == Closed
278
288
&& actor `notElem` alreadyContested
279
289
&& snapshotNumber snapshot > latestSnapshot
280
- && decommitUTxO snapshot `Set.isSubsetOf` utxoInHead
281
290
Fanout {snapshot} ->
282
291
headState == Closed
283
292
&& snapshotUTxO snapshot == utxoInHead
284
293
294
+ validFailingAction :: Model -> Action Model a -> Bool
295
+ validFailingAction Model {headState, latestSnapshot, alreadyContested, utxoInHead} = \ case
296
+ Decrement {snapshot} ->
297
+ headState == Open
298
+ && ( snapshotNumber snapshot <= latestSnapshot
299
+ || decommitUTxO snapshot `Set.isSubsetOf` utxoInHead
300
+ )
301
+ Close {snapshot} ->
302
+ headState == Open
303
+ && snapshotNumber snapshot < latestSnapshot
304
+ Contest {actor, snapshot} ->
305
+ headState == Closed
306
+ && ( snapshotNumber snapshot <= latestSnapshot
307
+ || actor `elem` alreadyContested
308
+ )
309
+ Fanout {snapshot} ->
310
+ headState == Closed
311
+ && ( snapshotNumber snapshot /= latestSnapshot
312
+ || snapshotUTxO snapshot /= utxoInHead
313
+ )
314
+ _ -> False
315
+
285
316
nextState :: Model -> Action Model a -> Var a -> Model
286
317
nextState m t _result =
287
318
case t of
@@ -535,17 +566,15 @@ newDecrementTx actor (snapshot, signatures) = do
535
566
newCloseTx :: HasCallStack => Actor -> ConfirmedSnapshot Tx -> AppM Tx
536
567
newCloseTx actor snapshot = do
537
568
spendableUTxO <- get
538
- traceShow " close utxo" $
539
- traceShow (renderUTxO $ utxo $ getSnapshot snapshot) $
540
- either (failure . show ) pure $
541
- close
542
- (actorChainContext actor)
543
- spendableUTxO
544
- (mkHeadId Fixture. testPolicyId)
545
- Fixture. testHeadParameters
546
- snapshot
547
- lowerBound
548
- upperBound
569
+ either (failure . show ) pure $
570
+ close
571
+ (actorChainContext actor)
572
+ spendableUTxO
573
+ (mkHeadId Fixture. testPolicyId)
574
+ Fixture. testHeadParameters
575
+ snapshot
576
+ lowerBound
577
+ upperBound
549
578
where
550
579
lowerBound = 0
551
580
@@ -557,16 +586,14 @@ newCloseTx actor snapshot = do
557
586
newContestTx :: HasCallStack => Actor -> ConfirmedSnapshot Tx -> AppM Tx
558
587
newContestTx actor snapshot = do
559
588
spendableUTxO <- get
560
- traceShow " contest utxo" $
561
- traceShow (renderUTxO $ utxo $ getSnapshot snapshot) $
562
- either (failure . show ) pure $
563
- contest
564
- (actorChainContext actor)
565
- spendableUTxO
566
- (mkHeadId Fixture. testPolicyId)
567
- Fixture. cperiod
568
- snapshot
569
- currentTime
589
+ either (failure . show ) pure $
590
+ contest
591
+ (actorChainContext actor)
592
+ spendableUTxO
593
+ (mkHeadId Fixture. testPolicyId)
594
+ Fixture. cperiod
595
+ snapshot
596
+ currentTime
570
597
where
571
598
currentTime = (0 , posixSecondsToUTCTime 0 )
572
599
@@ -577,16 +604,14 @@ newFanoutTx :: Actor -> ModelSnapshot -> AppM (Either FanoutTxError Tx)
577
604
newFanoutTx actor snapshot = do
578
605
spendableUTxO <- get
579
606
let (snapshot', _) = signedSnapshot snapshot
580
- traceShow " fanout utxo" $
581
- traceShow (renderUTxO $ utxo snapshot') $
582
- pure $
583
- fanout
584
- (actorChainContext actor)
585
- spendableUTxO
586
- Fixture. testSeedInput
587
- (utxo snapshot')
588
- (utxoToDecommit snapshot')
589
- deadline
607
+ pure $
608
+ fanout
609
+ (actorChainContext actor)
610
+ spendableUTxO
611
+ Fixture. testSeedInput
612
+ (utxo snapshot')
613
+ (utxoToDecommit snapshot')
614
+ deadline
590
615
where
591
616
CP. UnsafeContestationPeriod contestationPeriod = Fixture. cperiod
592
617
deadline = SlotNo $ fromIntegral contestationPeriod * fromIntegral (length allActors)
@@ -655,5 +680,5 @@ expectInvalid = \case
655
680
656
681
-- | Generate sometimes a value with given generator, bur more often just use
657
682
-- the given value.
658
- orSometimes :: a -> Gen a -> Gen a
659
- orSometimes a gen = frequency [(2 , pure a), (1 , gen)]
683
+ orArbitrary :: a -> Gen a -> Gen a
684
+ orArbitrary a gen = frequency [(1 , pure a), (1 , gen)]
0 commit comments