Skip to content

Commit df60978

Browse files
paolinopaolino
authored
[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
2 parents d7bac0f + 500bb48 commit df60978

File tree

9 files changed

+213
-202
lines changed

9 files changed

+213
-202
lines changed

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

+17-33
Original file line numberDiff line numberDiff line change
@@ -40,8 +40,16 @@ import Cardano.Wallet.DB.Store.Delegations.Store
4040
( mkStoreDelegations
4141
)
4242
import Cardano.Wallet.Delegation.Model
43-
( Operation (..)
44-
, Status (..)
43+
( Status (Inactive)
44+
, pattern Delegate
45+
, pattern DelegateAndVote
46+
, pattern Delegating
47+
, pattern DelegatingAndVoting
48+
, pattern Deregister'
49+
, pattern Register
50+
, pattern Registered
51+
, pattern Vote
52+
, pattern Voting
4553
, status
4654
)
4755
import Cardano.Wallet.Delegation.ModelSpec
@@ -111,30 +119,6 @@ conf =
111119
, genNewDRep = \xs -> arbitrary `suchThat` (not . (`elem` xs))
112120
}
113121

114-
pattern Register :: slot -> Operation slot drep pool
115-
pattern Register i = VoteAndDelegate Nothing Nothing i
116-
117-
pattern Delegate :: pool -> slot -> Operation slot drep pool
118-
pattern Delegate p i = VoteAndDelegate Nothing (Just p) i
119-
120-
pattern Vote :: drep -> slot -> Operation slot drep pool
121-
pattern Vote v i = VoteAndDelegate (Just v) Nothing i
122-
123-
pattern DelegateAndVote :: pool -> drep -> slot -> Operation slot drep pool
124-
pattern DelegateAndVote p v i = VoteAndDelegate (Just v) (Just p) i
125-
126-
pattern Registered :: Status drep pool
127-
pattern Registered = Active Nothing Nothing
128-
129-
pattern Delegating :: pool -> Status drep pool
130-
pattern Delegating p = Active Nothing (Just p)
131-
132-
pattern Voting :: drep -> Status drep pool
133-
pattern Voting v = Active (Just v) Nothing
134-
135-
pattern DelegatingAndVoting :: pool -> drep -> Status drep pool
136-
pattern DelegatingAndVoting p v = Active (Just v) (Just p)
137-
138122
units :: WalletProperty
139123
units = withInitializedWalletProp $ \_ runQ -> do
140124
[p0 :: PoolId, p1, _p2] <-
@@ -151,20 +135,20 @@ units = withInitializedWalletProp $ \_ runQ -> do
151135
runQ $ unitTestStore mempty mkStoreDelegations $ do
152136
unit "reg-dereg" $ do
153137
applyS $ Register 0
154-
applyS $ Deregister 0
138+
applyS $ Deregister' 0
155139
observeStatus 0 Inactive
156140
unit "reg-dereg, different time" $ do
157141
applyS $ Register 0
158142
observeStatus 0 Registered
159-
applyS $ Deregister 1
143+
applyS $ Deregister' 1
160144
observeStatus 0 Registered
161145
observeStatus 1 Inactive
162146
unit "dereg-reg" $ do
163-
applyS $ Deregister 0
147+
applyS $ Deregister' 0
164148
applyS $ Register 0
165149
observeStatus 0 Registered
166150
unit "dereg-reg different time" $ do
167-
applyS $ Deregister 0
151+
applyS $ Deregister' 0
168152
applyS $ Register 1
169153
observeStatus 1 Registered
170154
unit "reg-deleg" $ do
@@ -184,7 +168,7 @@ units = withInitializedWalletProp $ \_ runQ -> do
184168
unit "reg-deleg-dereg" $ do
185169
applyS $ Register 0
186170
applyS $ Delegate p0 0
187-
applyS $ Deregister 1
171+
applyS $ Deregister' 1
188172
observeStatus 2 Inactive
189173
unit "reg-vote" $ do
190174
applyS $ Register 0
@@ -203,7 +187,7 @@ units = withInitializedWalletProp $ \_ runQ -> do
203187
unit "reg-vote-dereg" $ do
204188
applyS $ Register 0
205189
applyS $ Vote v0 0
206-
applyS $ Deregister 1
190+
applyS $ Deregister' 1
207191
observeStatus 2 Inactive
208192
unit "reg-deleg-and-vote" $ do
209193
applyS $ Register 0
@@ -222,7 +206,7 @@ units = withInitializedWalletProp $ \_ runQ -> do
222206
unit "reg-deleg-and-vote-dereg" $ do
223207
applyS $ Register 0
224208
applyS $ DelegateAndVote p0 v0 0
225-
applyS $ Deregister 1
209+
applyS $ Deregister' 1
226210
observeStatus 2 Inactive
227211
unit "reg-deleg-then-vote" $ do
228212
applyS $ Register 0

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

+9-3
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
{-# LANGUAGE ConstraintKinds #-}
22
{-# LANGUAGE FlexibleContexts #-}
33
{-# LANGUAGE MonoLocalBinds #-}
4+
{-# LANGUAGE PatternSynonyms #-}
45
{-# LANGUAGE ScopedTypeVariables #-}
56
{-# LANGUAGE TypeApplications #-}
67

@@ -22,6 +23,10 @@ import Cardano.Wallet.Delegation.Model
2223
( History
2324
, Operation (..)
2425
, Status (Active)
26+
, pattern Delegate
27+
, pattern DelegateAndVote
28+
, pattern Deregister'
29+
, pattern Vote
2530
)
2631
import Cardano.Wallet.Delegation.Properties
2732
( Step (Step)
@@ -89,9 +94,10 @@ genDelta c h = do
8994
pool <- genPool c h
9095
drep <- genRep c h
9196
elements
92-
[ VoteAndDelegate (Just drep) (Just pool) slot
93-
, VoteAndDelegate Nothing (Just pool) slot
94-
, VoteAndDelegate (Just drep) Nothing slot
97+
[ DelegateAndVote pool drep slot
98+
, Delegate pool slot
99+
, Vote drep slot
100+
, Deregister' slot
95101
, Rollback slot
96102
]
97103

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

+4-2
Original file line numberDiff line numberDiff line change
@@ -25,6 +25,7 @@ import Cardano.Wallet.DB.Store.Delegations.Model
2525
import Cardano.Wallet.Delegation.Model
2626
( Operation (..)
2727
, Status (..)
28+
, Transition (..)
2829
)
2930
import Cardano.Wallet.Primitive.Slotting
3031
( TimeInterpreter
@@ -87,8 +88,9 @@ putDelegationCertificate
8788
-> SlotNo
8889
-> DeltaDelegations
8990
putDelegationCertificate cert sl = case cert of
90-
CertDelegateNone _ -> Deregister sl
91-
CertVoteAndDelegate _ pool drep -> VoteAndDelegate drep pool sl
91+
CertDelegateNone _ -> ApplyTransition Deregister sl
92+
CertVoteAndDelegate _ pool drep -> ApplyTransition
93+
(VoteAndDelegate drep pool) sl
9294

9395
-- | Arguments to 'readDelegation'.
9496
data CurrentEpochSlotting = CurrentEpochSlotting

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

+3-2
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@ import Cardano.Pool.Types
1515
import Cardano.Wallet.Delegation.Model
1616
( History
1717
, Operation (..)
18+
, Transition (..)
1819
)
1920
import Cardano.Wallet.Primitive.Types
2021
( SlotNo
@@ -35,8 +36,8 @@ type DeltaDelegations = Operation SlotNo DRep PoolId
3536

3637
instance Buildable DeltaDelegations where
3738
build = \case
38-
Deregister slot -> "Deregister " <> build slot
39-
VoteAndDelegate vote pool slot ->
39+
ApplyTransition Deregister slot -> "Deregister " <> build slot
40+
ApplyTransition (VoteAndDelegate vote pool) slot ->
4041
"Delegate " <> build pool
4142
<> " and vote "<> build vote <> " " <> build slot
4243
Rollback slot -> "Rollback " <> build slot

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

+59-11
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
{-# LANGUAGE PatternSynonyms #-}
12
{-# LANGUAGE TypeFamilies #-}
23

34
-- |
@@ -8,9 +9,24 @@
89
module Cardano.Wallet.Delegation.Model
910
( Operation (..)
1011
, slotOf
12+
13+
, Transition (..)
14+
, applyTransition
15+
1116
, Status (..)
17+
1218
, History
1319
, status
20+
21+
, pattern Register
22+
, pattern Delegate
23+
, pattern Vote
24+
, pattern Deregister'
25+
, pattern DelegateAndVote
26+
, pattern Registered
27+
, pattern Delegating
28+
, pattern Voting
29+
, pattern DelegatingAndVoting
1430
) where
1531

1632
import Prelude
@@ -27,18 +43,21 @@ import Data.Map.Strict
2743

2844
import qualified Data.Map.Strict as Map
2945

46+
data Transition drep pool
47+
= VoteAndDelegate (Maybe drep) (Maybe pool)
48+
| Deregister
49+
deriving (Eq, Show)
50+
3051
-- | Delta type for the delegation 'History'.
3152
data Operation slot drep pool
32-
= VoteAndDelegate (Maybe drep) (Maybe pool) slot
33-
| Deregister slot
53+
= ApplyTransition (Transition drep pool) slot
3454
| Rollback slot
35-
deriving (Show)
55+
deriving (Eq, Show)
3656

3757
-- | Target slot of each 'Operation'.
3858
slotOf :: Operation slot drep pool -> slot
39-
slotOf (Deregister x) = x
4059
slotOf (Rollback x) = x
41-
slotOf (VoteAndDelegate _ _ x) = x
60+
slotOf (ApplyTransition _ x) = x
4261

4362
-- | Valid state for the delegations, independent of time.
4463
data Status drep pool
@@ -56,16 +75,17 @@ instance (Ord slot, Eq pool, Eq drep) => Delta (Operation slot drep pool) where
5675
slot = slotOf r
5776
hist' = cut (< slot) hist
5877
miss = status slot hist'
59-
wanted = transition r $ status slot hist
78+
wanted = case r of
79+
ApplyTransition t _ -> applyTransition t $ status slot hist
80+
Rollback _ -> status slot hist
6081

61-
transition :: Operation slot drep pool -> Status drep pool -> Status drep pool
62-
transition (Deregister _) _ = Inactive
63-
transition (VoteAndDelegate d p _) (Active d' p') = Active d'' p''
82+
applyTransition :: Transition drep pool -> Status drep pool -> Status drep pool
83+
applyTransition Deregister _ = Inactive
84+
applyTransition (VoteAndDelegate d p) (Active d' p') = Active d'' p''
6485
where
6586
d'' = insertIfJust d d'
6687
p'' = insertIfJust p p'
67-
transition (VoteAndDelegate d p _) _ = Active d p
68-
transition _ s = s
88+
applyTransition (VoteAndDelegate d p) _ = Active d p
6989

7090
insertIfJust :: Maybe a -> Maybe a -> Maybe a
7191
insertIfJust (Just y) _ = Just y
@@ -79,3 +99,31 @@ cut op = fst . Map.spanAntitone op
7999
-- | Status of the delegation at a given slot.
80100
status :: Ord slot => slot -> Map slot (Status drep pool) -> Status drep pool
81101
status x = maybe Inactive snd . Map.lookupMax . cut (<= x)
102+
103+
pattern Register :: slot -> Operation slot drep pool
104+
pattern Register i = ApplyTransition (VoteAndDelegate Nothing Nothing) i
105+
106+
pattern Delegate :: pool -> slot -> Operation slot drep pool
107+
pattern Delegate p i = ApplyTransition (VoteAndDelegate Nothing (Just p)) i
108+
109+
pattern Vote :: drep -> slot -> Operation slot drep pool
110+
pattern Vote v i = ApplyTransition (VoteAndDelegate (Just v) Nothing) i
111+
112+
pattern Deregister' :: slot -> Operation slot drep pool
113+
pattern Deregister' i = ApplyTransition Deregister i
114+
115+
pattern DelegateAndVote :: pool -> drep -> slot -> Operation slot drep pool
116+
pattern DelegateAndVote p v i
117+
= ApplyTransition (VoteAndDelegate (Just v) (Just p)) i
118+
119+
pattern Registered :: Status drep pool
120+
pattern Registered = Active Nothing Nothing
121+
122+
pattern Delegating :: pool -> Status drep pool
123+
pattern Delegating p = Active Nothing (Just p)
124+
125+
pattern Voting :: drep -> Status drep pool
126+
pattern Voting v = Active (Just v) Nothing
127+
128+
pattern DelegatingAndVoting :: pool -> drep -> Status drep pool
129+
pattern DelegatingAndVoting p v = Active (Just v) (Just p)

0 commit comments

Comments
 (0)