Merge pull request #786 from input-output-hk/exec_spec/shelley/fix-de…

…registration

remove stake cert pointers on dereg

byron/ledger/executable-spec/src/Ledger/Core.hs

@@ -270,6 +270,12 @@ class Relation m where
   (▷), (|>) :: Ord (Range m) => m -> Set (Range m) -> m
   s |> r = s ▷ r
 
+  -- | Range exclusion
+  --
+  -- Unicode: 22eb
+  (⋫), (|/>) :: Ord (Range m) => m -> Set (Range m) -> m
+  s |/> r = s ⋫ r
+
   -- | Union
   (∪) :: (Ord (Domain m), Ord (Range m)) => m -> m -> m
 
@@ -327,6 +333,8 @@ instance (Ord k, Ord v) => Relation (Bimap k v) where
 
   r ▷ s = Bimap.filter (\_ v -> Set.member v s) r
 
+  r ⋫ s = Bimap.filter (\_ v -> Set.notMember v s) r
+
   d0 ∪ d1 = Bimap.fold Bimap.insert d0 d1
   d0 ⨃ d1 = foldr (uncurry Bimap.insert) d0 (toList d1)
 
@@ -353,6 +361,8 @@ instance Relation (Map k v) where
 
   r ▷ s = Map.filter (flip Set.member s) r
 
+  r ⋫ s = Map.filter (flip Set.notMember s) r
+
   d0 ∪ d1 = Map.union d0 d1
   -- For union override we pass @d1@ as first argument, since 'Map.union' is
   -- left biased.
@@ -386,6 +396,8 @@ instance Relation (Set (a, b)) where
 
   r ▷ s = Set.filter (\(_,v) -> Set.member v s) r
 
+  r ⋫ s = Set.filter (\(_,v) -> Set.notMember v s) r
+
   (∪) = Set.union
 
   d0 ⨃ d1 = d1' ∪ ((dom d1') ⋪ d0)
@@ -416,6 +428,8 @@ instance Relation [(a, b)] where
 
   r ▷ s = filter ((`Set.member` toSet s) . snd) r
 
+  r ⋫ s = filter ((`Set.notMember` toSet s) . snd) r
+
   (∪) = (++)
 
   -- In principle a list of pairs allows for duplicated keys.

shelley/chain-and-ledger/executable-spec/src/STS/Deleg.hs

@@ -13,7 +13,7 @@ import           BlockChain (slotsPrior)
 import           Coin (Coin (..))
 import           Delegation.Certificates
 import           Keys
-import           Ledger.Core (dom, singleton, (∈), (∉), (∪), (⋪), (⨃))
+import           Ledger.Core (dom, singleton, (∈), (∉), (∪), (⋪), (⋫),(⨃))
 import           LedgerState
 import           Slot
 import           TxData
@@ -67,7 +67,7 @@ delegationTransition = do
         { _stKeys      = Set.singleton key              ⋪ _stKeys ds
         , _rewards     = Set.singleton (RewardAcnt key) ⋪ _rewards ds
         , _delegations = Set.singleton key              ⋪ _delegations ds
-        , _ptrs        = Set.singleton ptr_             ⋪ _ptrs ds
+        , _ptrs        = _ptrs ds                       ⋫ Set.singleton key
         }
 
     Delegate (Delegation delegator_ delegatee_) -> do

shelley/chain-and-ledger/executable-spec/src/STS/Utxo.hs

@@ -54,7 +54,7 @@ instance
     | InputSetEmptyUTxO
     | FeeTooSmallUTxO Coin Coin
     | ValueNotConservedUTxO Coin Coin
-    | NonPositiveOutputsUTxO
+    | NegativeOutputsUTxO
     | UnexpectedFailureUTXO [ValidationError] -- TODO maybe restructure Validity
                                               -- to prevent these predicate
                                               -- failures?
@@ -95,7 +95,7 @@ utxoInductive = do
   ups' <- trans @(UP hashAlgo dsignAlgo) $ TRC ((slot_, pp, dms_), u ^. ups, txup tx)
 
   let outputCoins = [c | (TxOut _ c) <- Set.toList (range (txouts txBody))]
-  all (0<) outputCoins ?! NonPositiveOutputsUTxO
+  all (0 <=) outputCoins ?! NegativeOutputsUTxO
 
   let maxTxSize_ = fromIntegral (_maxTxSize pp)
       txSize_ = txsize txBody
@@ -107,12 +107,12 @@ utxoInductive = do
 
       depositChange = deposits pp stakePools txCerts - (refunded + decayed)
 
-  pure $ UTxOState
-          { _utxo      = (txins txBody ⋪ (u ^. utxo)) ∪ txouts txBody
-          , _deposited = _deposited u + depositChange
-          , _fees      = _fees u + (txBody ^. txfee) + decayed
-          , _ups       = ups'
-          }
+  pure UTxOState
+        { _utxo      = (txins txBody ⋪ (u ^. utxo)) ∪ txouts txBody
+        , _deposited = _deposited u + depositChange
+        , _fees      = _fees u + (txBody ^. txfee) + decayed
+        , _ups       = ups'
+        }
 
 instance
   (HashAlgorithm hashAlgo, DSIGNAlgorithm dsignAlgo)

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

@@ -399,6 +399,8 @@ instance Relation (StakeKeys hashAlgo dsignAlgo) where
 
   (StakeKeys stKeys) ▷ s = StakeKeys $ stKeys ▷ s
 
+  (StakeKeys stKeys) ⋫ s = StakeKeys $ stKeys ⋫ s
+
   (StakeKeys a) ∪ (StakeKeys b) = StakeKeys $ a ∪ b
 
   (StakeKeys a) ⨃ b = StakeKeys $ a ⨃ b

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

@@ -44,8 +44,8 @@ import           Data.Set (Set)
 import qualified Data.Set as Set
 
 import           Coin (Coin (..))
-import           Keys (KeyDiscriminator(..), DSIGNAlgorithm, HashAlgorithm, KeyPair, Signable, hash, hashKey, sKey, sign,
-                     vKey, verify)
+import           Keys (DSIGNAlgorithm, HashAlgorithm, KeyDiscriminator (..), KeyPair, Signable,
+                     hash, hashKey, sKey, sign, vKey, verify)
 import           Ledger.Core (Relation (..))
 import           PParams (PParams (..))
 import           TxData (Addr (..), Credential (..), ScriptHash, StakeCredential, Tx (..),
@@ -76,6 +76,8 @@ instance Relation (UTxO hashAlgo dsignAlgo) where
 
   (UTxO utxo) ▷ s = UTxO $ utxo ▷ s
 
+  (UTxO utxo) ⋫ s = UTxO $ utxo ⋫ s
+
   (UTxO a) ∪ (UTxO b) = UTxO $ a ∪ b
 
   (UTxO a) ⨃ b = UTxO $ a ⨃ b

shelley/chain-and-ledger/executable-spec/test/Examples.hs

@@ -15,6 +15,7 @@ module Examples
   , ex2G
   , ex2H
   , ex2I
+  , ex2J
   , ex3A
   , ex3B
   , ex3C
@@ -58,8 +59,8 @@ import           BaseTypes (Seed (..), UnitInterval, mkUnitInterval, (⭒))
 import           BlockChain (pattern BHBody, pattern BHeader, pattern Block, pattern Proof,
                      ProtVer (..), TxSeq (..), bBodySize, bhHash, bhbHash, bheader, slotToSeed)
 import           Coin (Coin (..))
-import           Delegation.Certificates (pattern Delegate, pattern PoolDistr, pattern RegKey,
-                     pattern RegPool)
+import           Delegation.Certificates (pattern DeRegKey, pattern Delegate, pattern PoolDistr,
+                     pattern RegKey, pattern RegPool)
 import           EpochBoundary (BlocksMade (..), pattern Stake, emptySnapShots, _feeSS, _poolsSS,
                      _pstakeGo, _pstakeMark, _pstakeSet)
 import           Keys (pattern Dms, pattern KeyPair, pattern SKey, pattern SKeyES, pattern VKey,
@@ -516,8 +517,7 @@ ex2A :: CHAINExample
 ex2A = CHAINExample (Slot 10) initStEx2A blockEx2A expectedStEx2A
 
 
--- | Example 2B - continuing on after example 2, process a block late enough
--- in the epoch in order to create a reward update.
+-- | Example 2B - process a block late enough in the epoch in order to create a reward update.
 -- The block delegates Alice's and Bob's stake to Alice's pool.
 
 txbodyEx2B :: TxBody
@@ -614,7 +614,7 @@ expectedStEx2Bquater = expectedStEx2Bgeneric ppsExInstantDecay
 ex2B :: CHAINExample
 ex2B = CHAINExample (Slot 90) expectedStEx2A blockEx2B expectedStEx2B
 
--- | Example 2C - continuing on after example 3, process an empty block in the next epoch
+-- | Example 2C - process an empty block in the next epoch
 -- so that the (empty) reward update is applied and a stake snapshot is made.
 
 
@@ -729,7 +729,7 @@ ex2Cquater =
   CHAINExample (Slot 110) expectedStEx2Bquater blockEx2C expectedStEx2Cquater
 
 
--- | Example 2D - continuing on after example 4, process an empty block late enough
+-- | Example 2D - process an empty block late enough
 -- in the epoch in order to create a second reward update, preparing the way for
 -- the first non-empty pool distribution in this running example.
 
@@ -773,7 +773,7 @@ ex2D :: CHAINExample
 ex2D = CHAINExample (Slot 190) expectedStEx2C blockEx2D expectedStEx2D
 
 
--- | Example 2E - continuing on after example 5, create the first non-empty pool distribution
+-- | Example 2E - create the first non-empty pool distribution
 -- by creating a block in the third epoch of this running example.
 
 
@@ -845,8 +845,7 @@ ex2E :: CHAINExample
 ex2E = CHAINExample (Slot 220) expectedStEx2D blockEx2E expectedStEx2E
 
 
--- | Example 2F - continuing on after example 6, create a decentralized Praos block
--- (ie one not in the overlay schedule)
+-- | Example 2F - create a decentralized Praos block (ie one not in the overlay schedule)
 
 
 blockEx2F :: Block
@@ -891,7 +890,7 @@ ex2F :: CHAINExample
 ex2F = CHAINExample (Slot 295) expectedStEx2E blockEx2F expectedStEx2F
 
 
--- | Example 2G - continuing on after example 7, create an empty block in the next epoch
+-- | Example 2G - create an empty block in the next epoch
 -- to prepare the way for the first non-trivial reward update
 
 
@@ -951,7 +950,7 @@ ex2G :: CHAINExample
 ex2G = CHAINExample (Slot 310) expectedStEx2F blockEx2G expectedStEx2G
 
 
--- | Example 2H - continuing on after example 8, create the first non-trivial reward update
+-- | Example 2H - create the first non-trivial reward update
 
 
 blockEx2H :: Block
@@ -997,7 +996,7 @@ ex2H :: CHAINExample
 ex2H = CHAINExample (Slot 390) expectedStEx2G blockEx2H expectedStEx2H
 
 
--- | Example 2I - continuing on after example 9, apply the first non-trivial reward update
+-- | Example 2I - apply the first non-trivial reward update
 
 
 blockEx2I :: Block
@@ -1061,14 +1060,100 @@ ex2I :: CHAINExample
 ex2I = CHAINExample (Slot 410) expectedStEx2H blockEx2I expectedStEx2I
 
 
+-- | Example 2J - drain reward account and de-register stake key
+
+aliceAda2J :: Coin
+aliceAda2J = Coin 82593524514 -- reward account
+                   + 9729 -- txin we will consume (must spend at least one)
+                   + 4 -- stake registration refund
+                   - 9 -- tx fee
+
+txbodyEx2J :: TxBody
+txbodyEx2J = TxBody
+           (Set.fromList [TxIn (txid txbodyEx2B) 0]) --
+           [TxOut aliceAddr aliceAda2J]
+           (fromList [DeRegKey aliceSHK])
+           (Map.singleton (RewardAcnt aliceSHK) (Coin 82593524514))
+           (Coin 9)
+           (Slot 500)
+           emptyUpdate
+
+txEx2J :: Tx
+txEx2J = Tx
+          txbodyEx2J
+          (makeWitnessesVKey txbodyEx2J [alicePay, aliceStake])
+          Map.empty
+
+blockEx2J :: Block
+blockEx2J = mkBlock
+              blockEx2IHash
+              (coreNodeKeys 3)
+              [txEx2J]
+              (Slot 420)
+              (mkSeqNonce 7)
+              (Nonce 10)
+              zero
+              4
+
+blockEx2JHash :: Maybe HashHeader
+blockEx2JHash = Just (bhHash (bheader blockEx2J))
+
+utxoEx2J :: UTxO
+utxoEx2J = UTxO . Map.fromList $
+                   [ (TxIn genesisId 1, TxOut bobAddr bobInitCoin)
+                   , (TxIn (txid txbodyEx2J) 0, TxOut aliceAddr aliceAda2J)
+                   ]
+
+dsEx2J :: DState
+dsEx2J = dsEx1
+          { _ptrs = Map.fromList [ (Ptr (Slot 10) 0 1, bobSHK) ]
+          , _stKeys = StakeKeys $ Map.singleton bobSHK (Slot 10)
+          , _delegations = Map.singleton bobSHK (hk alicePool)
+          , _rewards = Map.singleton (RewardAcnt bobSHK) (Coin 730001159951)
+          }
+
+expectedLSEx2J :: LedgerState
+expectedLSEx2J = LedgerState
+               (UTxOState
+                 utxoEx2J
+                 (Coin 219 - 4)
+                 (Coin 18)
+                 usEx2A)
+               (DPState dsEx2J psEx2A)
+               0
+
+expectedStEx2J :: ChainState
+expectedStEx2J =
+  ( NewEpochState
+      (Epoch 4)
+      (mkSeqNonce 7)
+      (BlocksMade Map.empty)
+      (BlocksMade Map.empty)
+      (EpochState acntEx2I (snapsEx2G { _feeSS = Coin 9 }) expectedLSEx2J ppsEx1)
+      Nothing
+      pdEx2F
+      epoch1OSchedEx2I
+  , mkSeqNonce 10
+  , mkSeqNonce 10
+  , blockEx2JHash
+  , Slot 420
+  )
+
+ex2J :: CHAINExample
+ex2J = CHAINExample (Slot 420) expectedStEx2I blockEx2J expectedStEx2J
+
+
 -- | Example 3A - Setting up for a successful protocol parameter update,
 -- have three genesis keys vote on the same new parameters
 
 
+ppVote3A :: Set.Set Ppm
+ppVote3A = Set.fromList [ExtraEntropy (Nonce 123), PoolDeposit 200]
+
 ppupEx3A :: PPUpdate
-ppupEx3A = PPUpdate $ Map.fromList [ (hashKey $ coreNodeVKG 0, Set.singleton (PoolDeposit 200))
-                                   , (hashKey $ coreNodeVKG 3, Set.singleton (PoolDeposit 200))
-                                   , (hashKey $ coreNodeVKG 4, Set.singleton (PoolDeposit 200))
+ppupEx3A = PPUpdate $ Map.fromList [ (hashKey $ coreNodeVKG 0, ppVote3A)
+                                   , (hashKey $ coreNodeVKG 3, ppVote3A)
+                                   , (hashKey $ coreNodeVKG 4, ppVote3A)
                                    ]
 
 updateEx3A :: Update
@@ -1158,8 +1243,8 @@ ex3A = CHAINExample (Slot 10) initStEx2A blockEx3A expectedStEx3A
 
 
 ppupEx3B :: PPUpdate
-ppupEx3B = PPUpdate $ Map.fromList [ (hashKey $ coreNodeVKG 1, Set.singleton (PoolDeposit 200))
-                                   , (hashKey $ coreNodeVKG 5, Set.singleton (PoolDeposit 200))
+ppupEx3B = PPUpdate $ Map.fromList [ (hashKey $ coreNodeVKG 1, ppVote3A)
+                                   , (hashKey $ coreNodeVKG 5, ppVote3A)
                                    ]
 
 updateEx3B :: Update
@@ -1286,12 +1371,13 @@ expectedLSEx3C = LedgerState
 
 ppsEx3C :: PParams
 ppsEx3C = ppsEx1 { _poolDeposit = Coin 200 }
+-- Note that _extraEntropy is still NeutralSeed
 
 expectedStEx3C :: ChainState
 expectedStEx3C =
   ( NewEpochState
       (Epoch 1)
-      (mkSeqNonce 2)
+      (mkSeqNonce 2 ⭒ Nonce 123)
       (BlocksMade Map.empty)
       (BlocksMade Map.empty)
       (EpochState acntEx2A snapsEx3C expectedLSEx3C ppsEx3C)

shelley/chain-and-ledger/executable-spec/test/STSTests.hs

@@ -9,8 +9,8 @@ import           Test.Tasty (TestTree, testGroup)
 import           Test.Tasty.HUnit (Assertion, assertBool, testCase, (@?=))
 
 import           Examples (CHAINExample (..), alicePay, bobPay, carlPay, dariaPay, ex1, ex2A, ex2B,
-                     ex2C, ex2Cbis, ex2Cquater, ex2Cter, ex2D, ex2E, ex2F, ex2G, ex2H, ex2I, ex3A,
-                     ex3B, ex3C, ex4A, ex4B, ex4C)
+                     ex2C, ex2Cbis, ex2Cquater, ex2Cter, ex2D, ex2E, ex2F, ex2G, ex2H, ex2I, ex2J,
+                     ex3A, ex3B, ex3C, ex4A, ex4B, ex4C)
 import           MockTypes (CHAIN)
 import           MultiSigExamples (aliceAndBob, aliceAndBobOrCarl, aliceAndBobOrCarlAndDaria,
                      aliceAndBobOrCarlOrDaria, aliceOnly, aliceOrBob, applyTxWithScript, bobOnly)
@@ -90,6 +90,9 @@ testCHAINExample2H = testCHAINExample ex2H
 testCHAINExample2I :: Assertion
 testCHAINExample2I = testCHAINExample ex2I
 
+testCHAINExample2J :: Assertion
+testCHAINExample2J = testCHAINExample ex2J
+
 testCHAINExample3A :: Assertion
 testCHAINExample3A = testCHAINExample ex3A
 
@@ -125,6 +128,7 @@ stsTests = testGroup "STS Tests"
   , testCase "CHAIN example 2G - prelude to the first nontrivial rewards" testCHAINExample2G
   , testCase "CHAIN example 2H - create a nontrivial rewards" testCHAINExample2H
   , testCase "CHAIN example 2I - apply a nontrivial rewards" testCHAINExample2I
+  , testCase "CHAIN example 2J - drain reward account and deregister" testCHAINExample2J
   , testCase "CHAIN example 3A - get 3/7 votes for a pparam update" testCHAINExample3A
   , testCase "CHAIN example 3B - get 5/7 votes for a pparam update" testCHAINExample3B
   , testCase "CHAIN example 3C - processes a pparam update" testCHAINExample3C

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

@@ -413,7 +413,7 @@ \subsection{Delegation Rules}
         \varUpdate{\{\var{hk}\}} & \varUpdate{\subtractdom} & \varUpdate{\var{stkeys}} \\
         \varUpdate{\{\addrRw \var{hk}\}} & \varUpdate{\subtractdom} & \varUpdate{\var{rewards}} \\
         \varUpdate{\{\var{hk}\}} & \varUpdate{\subtractdom} & \varUpdate{\var{delegations}} \\
-        \varUpdate{\{ptr\}} & \varUpdate{\subtractdom} & \varUpdate{\var{ptrs}} \\
+        \varUpdate{\var{ptrs}} & \varUpdate{\subtractrange} & \varUpdate{\{\var{hk}\}} \\
         \var{fdms} \\
         \var{dms} \\
       \end{array}