Merge pull request #820 from input-output-hk/shelley/exec_spec/delega…

…tion_properties

Adapt  and implement `DELEG` STS rule properties

shelley/chain-and-ledger/executable-spec/src/EpochBoundary.hs

@@ -37,7 +37,7 @@ import           Keys (KeyHash)
 import           PParams (PParams (..))
 import           Slot (Epoch, Slot, slotFromEpoch, (-*))
 import           TxData (Addr (..), PoolParams, Ptr, RewardAcnt, StakeCredential, TxOut (..),
-                     getRwdHK)
+                     getRwdCred)
 import           UTxO (UTxO (..))
 
 import qualified Data.Map.Strict as Map
@@ -119,7 +119,7 @@ rewardStake
 rewardStake rewards =
   map convert $ Map.toList rewards
   where
-    convert (rwdKey, c) = (getRwdHK rwdKey, c)
+    convert (rwdKey, c) = (getRwdCred rwdKey, c)
 
 -- | Get stake of one pool
 poolStake

shelley/chain-and-ledger/executable-spec/src/LedgerState.hs

@@ -144,8 +144,8 @@ import           Slot (Duration (..), Epoch (..), Slot (..), epochFromSlot, firs
 import           Tx (extractKeyHash)
 import           TxData (Addr (..), Credential (..), Delegation (..), Ix, PoolParams, Ptr (..),
                      RewardAcnt (..), StakeCredential, Tx (..), TxBody (..), TxId (..), TxIn (..),
-                     TxOut (..), body, certs, getRwdHK, inputs, poolOwners, poolPledge, poolPubKey,
-                     poolRAcnt, ttl, txfee, wdrls, witKeyHash)
+                     TxOut (..), body, certs, getRwdCred, inputs, poolOwners, poolPledge,
+                     poolPubKey, poolRAcnt, ttl, txfee, wdrls, witKeyHash)
 import           Updates (AVUpdate (..), Applications, PPUpdate (..), Update (..), emptyUpdate,
                      emptyUpdateState)
 import           UTxO (UTxO (..), balance, deposits, txinLookup, txins, txouts, txup, verifyWitVKey)
@@ -584,7 +584,7 @@ witsVKeyNeeded utxo' tx@(Tx txbody _ _) _dms =
         _                               -> hkeys
 
     wdrlAuthors =
-      Set.fromList $ extractKeyHash $ map getRwdHK (Map.keys (txbody ^. wdrls))
+      Set.fromList $ extractKeyHash $ map getRwdCred (Map.keys (txbody ^. wdrls))
     owners = foldl Set.union Set.empty
                [pool ^. poolOwners . to (Set.map undiscriminateKeyHash) | RegPool pool <- toList $ txbody ^. certs]
     certAuthors = Set.fromList $ extractKeyHash (fmap getCertHK (toList $ txbody ^. certs))

shelley/chain-and-ledger/executable-spec/src/TxData.hs

@@ -51,9 +51,9 @@ data PoolParams hashAlgo dsignAlgo =
     , _poolOwners  :: Set (KeyHash hashAlgo dsignAlgo)
     } deriving (Show, Eq)
 
--- |An account based address for a rewards
+-- |An account based address for rewards
 newtype RewardAcnt hashAlgo signAlgo = RewardAcnt
-  { getRwdHK :: Credential hashAlgo signAlgo
+  { getRwdCred :: StakeCredential hashAlgo signAlgo
   } deriving (Show, Eq, Ord)
 
 -- | Script hash or key hash for a payment or a staking object.
@@ -394,7 +394,7 @@ instance (HashAlgorithm hashAlgo, DSIGNAlgorithm dsignAlgo)
   => ToCBOR (RewardAcnt hashAlgo dsignAlgo) where
   toCBOR rwdAcnt =
     encodeListLen 1
-      <> toCBOR (getRwdHK rwdAcnt)
+      <> toCBOR (getRwdCred rwdAcnt)
 
 instance Relation (StakeKeys hashAlgo dsignAlgo) where
   type Domain (StakeKeys hashAlgo dsignAlgo) = StakeCredential hashAlgo dsignAlgo

shelley/chain-and-ledger/executable-spec/src/UTxO.hs

@@ -50,8 +50,8 @@ import           Keys (DSIGNAlgorithm, HashAlgorithm, KeyDiscriminator (..), Key
 import           Ledger.Core (Relation (..))
 import           PParams (PParams (..))
 import           TxData (Addr (..), Credential (..), ScriptHash, StakeCredential, Tx (..),
-                     TxBody (..), TxId (..), TxIn (..), TxOut (..), WitVKey (..), getRwdHK, inputs,
-                     outputs, poolPubKey, txUpdate)
+                     TxBody (..), TxId (..), TxIn (..), TxOut (..), WitVKey (..), getRwdCred,
+                     inputs, outputs, poolPubKey, txUpdate)
 import           Updates (Update)
 
 import           Delegation.Certificates (DCert (..), StakePools (..), cwitness, dvalue)
@@ -215,7 +215,7 @@ scriptsNeeded
 scriptsNeeded u tx =
   Set.fromList (Map.elems $ Map.mapMaybe (getScriptHash . unTxOut) u'')
   `Set.union`
-  Set.fromList (Maybe.mapMaybe (scriptStakeCred . getRwdHK) $ Map.keys withdrawals)
+  Set.fromList (Maybe.mapMaybe (scriptStakeCred . getRwdCred) $ Map.keys withdrawals)
   `Set.union`
   Set.fromList (Maybe.mapMaybe (scriptStakeCred . cwitness) certificates)
   where unTxOut (TxOut a _) = a

shelley/chain-and-ledger/executable-spec/test/Rules/TestDeleg.hs

@@ -10,6 +10,7 @@ import           Data.Map (Map)
 import qualified Data.Map.Strict as Map (lookup)
 import qualified Data.Maybe as Maybe (maybe)
 import           Data.Set (Set)
+import qualified Data.Set as Set (singleton, size)
 
 import           Hedgehog (Property, forAll, property, withTests, (===))
 
@@ -19,14 +20,14 @@ import           Control.State.Transition.Trace (sourceSignalTargets, traceLengt
 import           Address (mkRwdAcnt)
 import           BaseTypes ((==>))
 import           Coin (Coin)
-import           LedgerState (_delegationState, _delegations, _dstate, _pstate, _retiring, _rewards,
-                     _stKeys, _stPools)
+import           LedgerState (_delegationState, _delegations, _pstate, _retiring, _rewards, _stKeys,
+                     _stPools)
 import           MockTypes (DELEG, DState, KeyHash, LedgerState, RewardAcnt, StakeCredential,
                      StakePools)
 import           Slot (Epoch)
-import           TxData (pattern RegKey)
+import           TxData (pattern DeRegKey, pattern Delegate, pattern Delegation, pattern RegKey)
 
-import           Ledger.Core (dom, (∈), (∉))
+import           Ledger.Core (dom, range, (∈), (∉), (◁))
 
 -------------------------------
 -- helper accessor functions --
@@ -38,8 +39,8 @@ getStDelegs l = dom $ _stKeys l
 getRewards :: DState -> Map RewardAcnt Coin
 getRewards l = _rewards l
 
-getDelegations :: LedgerState -> Map StakeCredential KeyHash
-getDelegations l = _delegations $ _dstate $ _delegationState l
+getDelegations :: DState -> Map StakeCredential KeyHash
+getDelegations l = _delegations l
 
 getStPools :: LedgerState -> StakePools
 getStPools l = _stPools $ _pstate $ _delegationState l
@@ -72,10 +73,49 @@ rewardZeroAfterReg = withTests (fromIntegral numberOfTests) . property $ do
     tr = sourceSignalTargets t
 
   when (n > 1) $
-    True === (all credNewlyRegisteredAndRewardZero tr)
+    [] === filter (not . credNewlyRegisteredAndRewardZero) tr
 
   where credNewlyRegisteredAndRewardZero (d, RegKey hk, d') =
           (hk ∉ getStDelegs d) ==>
           (   hk ∈ getStDelegs d'
            && (Maybe.maybe True (== 0) $ Map.lookup (mkRwdAcnt hk) (getRewards d')))
         credNewlyRegisteredAndRewardZero (_, _, _) = True
+
+-- | Check that when a stake credential is deregistered, it will not be in the
+-- rewards mapping or delegation mapping of the target state.
+credentialRemovedAfterDereg :: Property
+credentialRemovedAfterDereg = withTests (fromIntegral numberOfTests) . property $ do
+  t <- forAll (trace @DELEG $ fromIntegral traceLen)
+  let
+    n :: Integer
+    n = fromIntegral $ traceLength t
+    tr = sourceSignalTargets t
+
+  when (n > 1) $
+    [] === filter (not . removedDeregCredential) tr
+
+  where removedDeregCredential (_, DeRegKey cred, d') =
+             cred ∉ getStDelegs d'
+          && mkRwdAcnt cred ∉ dom (getRewards d')
+          && cred ∉ dom (getDelegations d')
+        removedDeregCredential (_, _, _) = True
+
+-- |Check that a registered stake credential get correctly delegated when
+-- applying a delegation certificate.
+credentialMappingAfterDelegation :: Property
+credentialMappingAfterDelegation = withTests (fromIntegral numberOfTests) . property $ do
+  t <- forAll (trace @DELEG $ fromIntegral traceLen)
+  let
+    n :: Integer
+    n = fromIntegral $ traceLength t
+    tr = sourceSignalTargets t
+
+  when (n > 1) $
+    [] === filter (not . delegatedCredential) tr
+
+  where delegatedCredential (_, Delegate (Delegation cred to), d') =
+          let credImage = range ((Set.singleton cred) ◁ (getDelegations d')) in
+             cred ∈ getStDelegs d'
+          && to ∈ credImage
+          && Set.size credImage == 1
+        delegatedCredential (_, _, _) = True

shelley/chain-and-ledger/formal-spec/properties.tex

@@ -201,15 +201,14 @@ \subsection{Ledger State Properties for Delegation Transitions}
                                     ((\var{stDelegs}, \wcard,
                                     \wcard,\wcard,\wcard,\wcard) \to \var{stDelegs} \\
                       &&\\
-    \fun{getRewards} & \in & \LState \to (\AddrRWD \mapsto \Coin) \\
-    \fun{getRewards} & \coloneqq & (\wcard,
-                                   ((\wcard, \var{rewards},
-                                   \wcard,\wcard,\wcard,\wcard), \wcard))
+    \fun{getRewards} & \in & \DState \to (\AddrRWD \mapsto \Coin) \\
+    \fun{getRewards} & \coloneqq & (\wcard, \var{rewards},
+                                   \wcard,\wcard,\wcard,\wcard)
                                    \to \var{rewards} \\
                       &&\\
-    \fun{getDelegations} & \in & \LState \to (\Credential \mapsto \KeyHash) \\
-    \fun{getDelegations} & \coloneqq & (\wcard, ((\wcard, \wcard,
-                                       \var{delegations},\wcard,\wcard,\wcard), \wcard)) \to
+    \fun{getDelegations} & \in & \DState \to (\Credential \mapsto \KeyHash) \\
+    \fun{getDelegations} & \coloneqq & (\wcard, \wcard,
+                                       \var{delegations},\wcard,\wcard,\wcard) \to
                                        \var{delegations} \\
                       &&\\
     \fun{getStPools} & \in & \LState \to (\KeyHash \mapsto \DCertRegPool) \\
@@ -247,13 +246,14 @@ \subsection{Ledger State Properties for Delegation Transitions}
 \begin{property}[\textbf{Deregistered Staking Credential}]
   \begin{multline*}
     \forall \var{l}, \var{l'} \in \ledgerState: \applyFun{validLedgerstate}{l},
-    l = (\wcard, dp), l' = (\wcard, dp'), dpsEnv\in\DPSEnv \\
-    \implies \forall \var{c} \in \DCertDeRegKey, dpsEnv\vdash\var{dp}
-    \trans{delegs}{c} \var{dp'} \implies \applyFun{cwitness}{c} = \var{hk}\\
-    \implies \var{hk} \not\in \applyFun{getStDelegs}{l'} \wedge
-    hk\not\in({\fun{stakeCred_{r}}~sc\vert
-      sc\in\fun{dom}(\applyFun{getRewards}{l'})} \cup
-    \fun{dom}(\applyFun{getDelegations}{l'}))
+    l = (\wcard, (d, \wcard)), l' = (\wcard, (d', \wcard)), dEnv\in\DEnv \\
+    \implies \forall \var{c} \in \DCertDeRegKey, dEnv\vdash\var{d}
+    \trans{deleg}{c} \var{d'} \implies \applyFun{cwitness}{c} = \var{hk}\\
+    \implies \var{hk} \not\in \applyFun{getStDelegs}{d'} \wedge hk\not\in
+    \left\{ \fun{stakeCred_{r}}~sc\vert
+      sc\in\fun{dom}(\applyFun{getRewards}{d'})
+    \right\}\\
+    \wedge hk \not\in \fun{dom}(\applyFun{getDelegations}{d'}))
   \end{multline*}
   \label{prop:ledger-properties-7}
 \end{property}
@@ -267,11 +267,11 @@ \subsection{Ledger State Properties for Delegation Transitions}
 \begin{property}[\textbf{Delegated Stake}]
   \begin{multline*}
     \forall \var{l}, \var{l'} \in \ledgerState: \applyFun{validLedgerstate}{l},
-    l = (\wcard, dp), l' = (\wcard, dp'), dpsEnv\in\DPSEnv \\
-    \implies \forall \var{c} \in \DCertDeleg, dpsEnv \vdash\var{dp}
-    \trans{delegs}{c} \var{dp'} \implies \applyFun{cwitness}{c} = \var{hk}\\
-    \implies \var{hk} \in \applyFun{getStDelegs}{l} \wedge
-    (\applyFun{getDelegations}{l'})[hk] = \applyFun{pool}{c}
+    l = (\wcard, (d,\wcard)), l' = (\wcard, (d',\wcard)), dEnv\in\DEnv \\
+    \implies \forall \var{c} \in \DCertDeleg, dEnv \vdash\var{d}
+    \trans{deleg}{c} \var{d'} \implies \applyFun{cwitness}{c} = \var{hk}\\
+    \implies \var{hk} \in \applyFun{getStDelegs}{d'} \wedge
+    (\applyFun{getDelegations}{d'})[hk] = \applyFun{dpool}{c}
   \end{multline*}
   \label{prop:ledger-properties-8}
 \end{property}