Update QuickCheck properties to match Delegation.agda

Author: HeinrichApfelmus

lib/wallet/src/Cardano/Wallet/Delegation/Model.hs

@@ -8,11 +8,16 @@
 -- Data types that represents a history of delegations and its changes.
 module Cardano.Wallet.Delegation.Model
     ( Operation (..)
-    , Transition (..)
     , slotOf
+
+    , Transition (..)
+    , applyTransition
+
     , Status (..)
+
     , History
     , status
+
     , pattern Register
     , pattern Delegate
     , pattern Vote
@@ -41,13 +46,13 @@ import qualified Data.Map.Strict as Map
 data Transition drep pool
     = VoteAndDelegate (Maybe drep) (Maybe pool)
     | Deregister
-    deriving (Show)
+    deriving (Eq, Show)
 
 -- | Delta type for the delegation 'History'.
 data Operation slot drep pool
     = ApplyTransition (Transition drep pool) slot
     | Rollback slot
-    deriving (Show)
+    deriving (Eq, Show)
 
 -- | Target slot of each 'Operation'.
 slotOf :: Operation slot drep pool -> slot

lib/wallet/src/Cardano/Wallet/Delegation/Properties.hs

@@ -1,15 +1,14 @@
 {-# LANGUAGE FlexibleContexts #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE NamedFieldPuns #-}
 
 -- |
 -- Copyright: © 2022–2023 IOHK
 -- License: Apache-2.0
 --
 -- Properties of the delegations-history model.
 module Cardano.Wallet.Delegation.Properties
-    ( GenSlot
-    , Step (..)
+    ( Step (..)
     , properties
     )
 where
@@ -20,16 +19,14 @@ import Cardano.Wallet.Delegation.Model
     ( History
     , Operation (..)
     , Status (..)
-    , Transition (..)
+    , applyTransition
     , slotOf
     , status
     )
-import Control.Applicative
-    ( (<|>)
-    )
 import Test.QuickCheck
     ( Gen
     , Property
+    , conjoin
     , counterexample
     , forAll
     , (===)
@@ -44,70 +41,45 @@ data Step slot drep pool = Step
     }
     deriving (Show)
 
--- | Compute a not so random slot from a 'History' of delegations.
-type GenSlot slot drep pool = History slot drep pool -> Gen slot
-
-property'
-    :: (Ord a, Show a, Show drep, Show pool, Eq drep, Eq pool)
-    => (History a drep pool -> Gen a)
-    -> Step a drep pool
-    -> (Status drep pool -> Status drep pool -> Property)
+setsTheFuture
+    :: (Ord slot, Show slot, Show drep, Show pool, Eq drep, Eq pool)
+    => (History slot drep pool -> Gen slot)
+    -> Step slot drep pool
+    -> (slot -> Operation slot drep pool)
+    -> (Status drep pool -> Status drep pool)
     -> Property
-property' genSlot Step{old_ = xs, new_ = xs', delta_ = diff} change =
-    let x = slotOf diff
-        old = status x xs
-    in  forAll (genSlot xs') $ \y ->
-            let new = status y xs'
+setsTheFuture genSlot Step{old_=history, new_=history', delta_} op transition =
+    let x = slotOf delta_
+        old = status x history
+    in  conjoin
+        [ delta_ === op x
+        , forAll (genSlot history') $ \y ->
+            let new = status y history'
             in  case compare y x of
-                    LT -> new === status y xs
-                    _ -> change old new
-
-precond
-    :: (Eq drep, Eq pool, Show drep, Show pool)
-    => (Status drep pool -> (Bool, Maybe x))
-    -> (Maybe x -> Status drep pool)
-    -> Status drep pool
-    -> Status drep pool
-    -> Property
-precond check target old new
-    | (fst $ check old) = counterexample "new target"
-        $ new === (target (snd $ check old))
-    | otherwise = counterexample "no changes"
-        $ new === old
+                    LT -> new === status y history
+                    _ -> new === transition old
+        ]
 
--- | Properties replicated verbatim from specifications. See
--- 'specifications/Cardano/Wallet/delegation.lean'
+-- | Properties replicated verbatim from specifications.
+-- See 'specifications/Cardano/Wallet/Delegation.agda'.
 properties
     :: (Show slot, Show drep, Show pool, Ord slot, Eq drep, Eq pool)
     => (History slot drep pool -> Gen slot)
     -> Step slot drep pool
     -> Property
 properties genSlot step =
     let that msg = counterexample ("falsified: " <> msg)
-        prop cond target =
+        setsTheFuture' op =
             counterexample (show step)
-                $ property' genSlot step
-                $ precond cond target
+                . setsTheFuture genSlot step op
     in  case delta_ step of
-            ApplyTransition Deregister _ ->
-                that "deregister invariant is respected"
-                    $ prop
-                        ( \case
-                            Active _ _ -> (True, Nothing)
-                            _ -> (False, Nothing)
-                        )
-                        (const Inactive)
-            ApplyTransition (VoteAndDelegate v p) _ -> do
-                that "delegate and/or vote invariant is respected"
-                    $ prop
-                        ( \case
-                            Inactive -> (True, Just Inactive)
-                            Active v' p'-> (True, Just (Active v' p'))
-                        )
-                        $ \case
-                            Just (Active v' p') -> Active (v <|> v') (p <|> p')
-                            Just Inactive -> Active v p
-                            _ -> error "VoteAndDelegate branch broke"
+            ApplyTransition t _ ->
+                that "ApplyTransition invariant is respected"
+                    $ setsTheFuture'
+                        (ApplyTransition t)
+                        (applyTransition t)
             Rollback _ ->
-                that "rollback invariant is respected"
-                    $ property' genSlot step (===)
+                that "Rollback invariant is respected"
+                    $ setsTheFuture'
+                        Rollback
+                        id

specifications/Cardano/Wallet/Delegation.agda

@@ -77,14 +77,11 @@ record HistoryLaws (api : HistoryApi) : Set₁ where
   field
     prop-transitions
       : ∀ (t : Transition)
-          (history : History api)
       → setsTheFuture api
           (ApplyTransition t)
           (applyTransition t)
 
     prop-rollback
-      : ∀ (slot : Slot)
-          (history : History api)
-      → setsTheFuture api
+      : setsTheFuture api
           Rollback
           (λ old → old)