[ADP-3290] Match delegation agda specs in the implementation (#4475)

This pull request aligns the behavior of the `Delegations` data
structure with a specification in Agda.

- [x] Add Transition datatype to the Model
- [x] Add missing Deregister value to the genDelta
- [x] Update the QC specs

ADP-3290

lib/unit/test/unit/Cardano/Wallet/DB/Store/Delegations/StoreSpec.hs

@@ -40,8 +40,16 @@ import Cardano.Wallet.DB.Store.Delegations.Store
     ( mkStoreDelegations
     )
 import Cardano.Wallet.Delegation.Model
-    ( Operation (..)
-    , Status (..)
+    ( Status (Inactive)
+    , pattern Delegate
+    , pattern DelegateAndVote
+    , pattern Delegating
+    , pattern DelegatingAndVoting
+    , pattern Deregister'
+    , pattern Register
+    , pattern Registered
+    , pattern Vote
+    , pattern Voting
     , status
     )
 import Cardano.Wallet.Delegation.ModelSpec
@@ -111,30 +119,6 @@ conf =
         , genNewDRep = \xs -> arbitrary `suchThat` (not . (`elem` xs))
         }
 
-pattern Register :: slot -> Operation slot drep pool
-pattern Register i = VoteAndDelegate Nothing Nothing i
-
-pattern Delegate :: pool -> slot -> Operation slot drep pool
-pattern Delegate p i = VoteAndDelegate Nothing (Just p) i
-
-pattern Vote :: drep -> slot -> Operation slot drep pool
-pattern Vote v i = VoteAndDelegate (Just v) Nothing i
-
-pattern DelegateAndVote :: pool -> drep -> slot -> Operation slot drep pool
-pattern DelegateAndVote p v i = VoteAndDelegate (Just v) (Just p) i
-
-pattern Registered :: Status drep pool
-pattern Registered = Active Nothing Nothing
-
-pattern Delegating :: pool -> Status drep pool
-pattern Delegating p = Active Nothing (Just p)
-
-pattern Voting :: drep -> Status drep pool
-pattern Voting v = Active (Just v) Nothing
-
-pattern DelegatingAndVoting :: pool -> drep -> Status drep pool
-pattern DelegatingAndVoting p v = Active (Just v) (Just p)
-
 units :: WalletProperty
 units = withInitializedWalletProp $ \_ runQ -> do
     [p0 :: PoolId, p1, _p2] <-
@@ -151,20 +135,20 @@ units = withInitializedWalletProp $ \_ runQ -> do
     runQ $ unitTestStore mempty mkStoreDelegations $ do
         unit "reg-dereg" $ do
             applyS $ Register 0
-            applyS $ Deregister 0
+            applyS $ Deregister' 0
             observeStatus 0 Inactive
         unit "reg-dereg, different time" $ do
             applyS $ Register 0
             observeStatus 0 Registered
-            applyS $ Deregister 1
+            applyS $ Deregister' 1
             observeStatus 0 Registered
             observeStatus 1 Inactive
         unit "dereg-reg" $ do
-            applyS $ Deregister 0
+            applyS $ Deregister' 0
             applyS $ Register 0
             observeStatus 0 Registered
         unit "dereg-reg different time" $ do
-            applyS $ Deregister 0
+            applyS $ Deregister' 0
             applyS $ Register 1
             observeStatus 1 Registered
         unit "reg-deleg" $ do
@@ -184,7 +168,7 @@ units = withInitializedWalletProp $ \_ runQ -> do
         unit "reg-deleg-dereg" $ do
             applyS $ Register 0
             applyS $ Delegate p0 0
-            applyS $ Deregister 1
+            applyS $ Deregister' 1
             observeStatus 2 Inactive
         unit "reg-vote" $ do
             applyS $ Register 0
@@ -203,7 +187,7 @@ units = withInitializedWalletProp $ \_ runQ -> do
         unit "reg-vote-dereg" $ do
             applyS $ Register 0
             applyS $ Vote v0 0
-            applyS $ Deregister 1
+            applyS $ Deregister' 1
             observeStatus 2 Inactive
         unit "reg-deleg-and-vote" $ do
             applyS $ Register 0
@@ -222,7 +206,7 @@ units = withInitializedWalletProp $ \_ runQ -> do
         unit "reg-deleg-and-vote-dereg" $ do
             applyS $ Register 0
             applyS $ DelegateAndVote p0 v0 0
-            applyS $ Deregister 1
+            applyS $ Deregister' 1
             observeStatus 2 Inactive
         unit "reg-deleg-then-vote" $ do
             applyS $ Register 0

lib/unit/test/unit/Cardano/Wallet/Delegation/ModelSpec.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE ConstraintKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 
@@ -22,6 +23,10 @@ import Cardano.Wallet.Delegation.Model
     ( History
     , Operation (..)
     , Status (Active)
+    , pattern Delegate
+    , pattern DelegateAndVote
+    , pattern Deregister'
+    , pattern Vote
     )
 import Cardano.Wallet.Delegation.Properties
     ( Step (Step)
@@ -89,9 +94,10 @@ genDelta c h = do
     pool <- genPool c h
     drep <- genRep c h
     elements
-        [ VoteAndDelegate (Just drep) (Just pool) slot
-        , VoteAndDelegate Nothing (Just pool) slot
-        , VoteAndDelegate (Just drep) Nothing slot
+        [ DelegateAndVote pool drep slot
+        , Delegate pool slot
+        , Vote drep slot
+        , Deregister' slot
         , Rollback slot
         ]
 

lib/wallet/src/Cardano/Wallet/DB/Store/Delegations/Layer.hs

@@ -25,6 +25,7 @@ import Cardano.Wallet.DB.Store.Delegations.Model
 import Cardano.Wallet.Delegation.Model
     ( Operation (..)
     , Status (..)
+    , Transition (..)
     )
 import Cardano.Wallet.Primitive.Slotting
     ( TimeInterpreter
@@ -87,8 +88,9 @@ putDelegationCertificate
     -> SlotNo
     -> DeltaDelegations
 putDelegationCertificate cert sl = case cert of
-    CertDelegateNone _ -> Deregister sl
-    CertVoteAndDelegate _ pool drep -> VoteAndDelegate drep pool sl
+    CertDelegateNone _ -> ApplyTransition Deregister sl
+    CertVoteAndDelegate _ pool drep -> ApplyTransition
+        (VoteAndDelegate drep pool) sl
 
 -- | Arguments to 'readDelegation'.
 data CurrentEpochSlotting = CurrentEpochSlotting

lib/wallet/src/Cardano/Wallet/DB/Store/Delegations/Model.hs

@@ -15,6 +15,7 @@ import Cardano.Pool.Types
 import Cardano.Wallet.Delegation.Model
     ( History
     , Operation (..)
+    , Transition (..)
     )
 import Cardano.Wallet.Primitive.Types
     ( SlotNo
@@ -35,8 +36,8 @@ type DeltaDelegations = Operation SlotNo DRep PoolId
 
 instance Buildable DeltaDelegations where
     build = \case
-            Deregister slot -> "Deregister " <> build slot
-            VoteAndDelegate vote pool slot ->
+            ApplyTransition Deregister slot -> "Deregister " <> build slot
+            ApplyTransition (VoteAndDelegate vote pool) slot ->
                     "Delegate " <> build pool
                         <> " and vote "<> build vote <> " " <> build slot
             Rollback slot -> "Rollback " <> build slot

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

@@ -1,3 +1,4 @@
+{-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE TypeFamilies #-}
 
 -- |
@@ -8,9 +9,24 @@
 module Cardano.Wallet.Delegation.Model
     ( Operation (..)
     , slotOf
+
+    , Transition (..)
+    , applyTransition
+
     , Status (..)
+
     , History
     , status
+
+    , pattern Register
+    , pattern Delegate
+    , pattern Vote
+    , pattern Deregister'
+    , pattern DelegateAndVote
+    , pattern Registered
+    , pattern Delegating
+    , pattern Voting
+    , pattern DelegatingAndVoting
     ) where
 
 import Prelude
@@ -27,18 +43,21 @@ import Data.Map.Strict
 
 import qualified Data.Map.Strict as Map
 
+data Transition drep pool
+    = VoteAndDelegate (Maybe drep) (Maybe pool)
+    | Deregister
+    deriving (Eq, Show)
+
 -- | Delta type for the delegation 'History'.
 data Operation slot drep pool
-    = VoteAndDelegate (Maybe drep) (Maybe pool) slot
-    | Deregister slot
+    = ApplyTransition (Transition drep pool) slot
     | Rollback slot
-    deriving (Show)
+    deriving (Eq, Show)
 
 -- | Target slot of each 'Operation'.
 slotOf :: Operation slot drep pool -> slot
-slotOf (Deregister x) = x
 slotOf (Rollback x) = x
-slotOf (VoteAndDelegate _ _ x) = x
+slotOf (ApplyTransition _ x) = x
 
 -- | Valid state for the delegations, independent of time.
 data Status drep pool
@@ -56,16 +75,17 @@ instance (Ord slot, Eq pool, Eq drep) => Delta (Operation slot drep pool) where
         slot = slotOf r
         hist' = cut (< slot) hist
         miss = status slot hist'
-        wanted = transition r $ status slot hist
+        wanted = case r of
+            ApplyTransition t _ -> applyTransition t $ status slot hist
+            Rollback _ -> status slot hist
 
-transition :: Operation slot drep pool -> Status drep pool -> Status drep pool
-transition (Deregister _) _ = Inactive
-transition (VoteAndDelegate d p _) (Active d' p') = Active d'' p''
+applyTransition :: Transition drep pool -> Status drep pool -> Status drep pool
+applyTransition Deregister _ = Inactive
+applyTransition (VoteAndDelegate d p) (Active d' p') = Active d'' p''
     where
         d'' = insertIfJust d d'
         p'' = insertIfJust p p'
-transition (VoteAndDelegate d p _) _ = Active d p
-transition _ s = s
+applyTransition (VoteAndDelegate d p) _ = Active d p
 
 insertIfJust :: Maybe a -> Maybe a -> Maybe a
 insertIfJust (Just y) _ = Just y
@@ -79,3 +99,31 @@ cut op = fst . Map.spanAntitone op
 -- | Status of the delegation at a given slot.
 status :: Ord slot => slot -> Map slot (Status drep pool) -> Status drep pool
 status x = maybe Inactive snd . Map.lookupMax . cut (<= x)
+
+pattern Register :: slot -> Operation slot drep pool
+pattern Register i = ApplyTransition (VoteAndDelegate Nothing Nothing) i
+
+pattern Delegate :: pool -> slot -> Operation slot drep pool
+pattern Delegate p i = ApplyTransition (VoteAndDelegate Nothing (Just p)) i
+
+pattern Vote :: drep -> slot -> Operation slot drep pool
+pattern Vote v i = ApplyTransition (VoteAndDelegate (Just v) Nothing) i
+
+pattern Deregister' :: slot -> Operation slot drep pool
+pattern Deregister' i = ApplyTransition Deregister i
+
+pattern DelegateAndVote :: pool -> drep -> slot -> Operation slot drep pool
+pattern DelegateAndVote p v i
+    = ApplyTransition (VoteAndDelegate (Just v) (Just p)) i
+
+pattern Registered :: Status drep pool
+pattern Registered = Active Nothing Nothing
+
+pattern Delegating :: pool -> Status drep pool
+pattern Delegating p = Active Nothing (Just p)
+
+pattern Voting :: drep -> Status drep pool
+pattern Voting v = Active (Just v) Nothing
+
+pattern DelegatingAndVoting :: pool -> drep -> Status drep pool
+pattern DelegatingAndVoting p v = Active (Just v) (Just p)