Merge pull request #1780 from input-output-hk/nc/assertions

Additional assertions
IntersectMBO · Aug 13, 2020 · 080a535 · 080a535
2 parents 6b5e761 + 86ef88d
commit 080a535
Show file tree

Hide file tree

Showing 5 changed files with 74 additions and 13 deletions.
diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -30,6 +30,7 @@ module Control.State.Transition.Extended
     TransitionRule,
     InitialRule,
     Assertion (..),
+    AssertionViolation (..),
     STS (..),
     Embed (..),
     (?!),
@@ -134,12 +135,11 @@ data AssertionViolation sts = AssertionViolation
     avState :: Maybe (State sts)
   }
 
-instance Show (AssertionViolation sts) where
-  show (AssertionViolation sts msg _ _) =
-    "AssertionViolation (" <> sts <> "): " <> msg
+instance STS sts => Show (AssertionViolation sts) where
+  show = renderAssertionViolation
 
 instance
-  (Typeable sts) =>
+  (STS sts) =>
   Exception (AssertionViolation sts)
 
 -- | State transition system.
@@ -192,8 +192,9 @@ class
   --   Defaults to using 'show', but note that this does not know how to render
   --   the context. So for more information you should define your own renderer
   --   here.
-  renderAssertionViolation :: AssertionViolation sts -> String
-  renderAssertionViolation = show
+  renderAssertionViolation :: AssertionViolation a -> String
+  renderAssertionViolation (AssertionViolation sts msg _ _) =
+    "AssertionViolation (" <> sts <> "): " <> msg
 
 -- | Embed one STS within another.
 class (STS sub, STS super, BaseM sub ~ BaseM super) => Embed sub super where

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
@@ -4,6 +4,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -25,7 +26,9 @@ import Cardano.Binary
   )
 import Cardano.Prelude (NoUnexpectedThunks (..))
 import Control.State.Transition
-  ( Embed (..),
+  ( Assertion (..),
+    AssertionViolation (..),
+    Embed (..),
     STS (..),
     TRC (..),
     TransitionRule,
@@ -38,14 +41,15 @@ import Data.Word (Word8)
 import GHC.Generics (Generic)
 import Shelley.Spec.Ledger.BaseTypes (ShelleyBase, invalidKey)
 import Shelley.Spec.Ledger.Crypto (Crypto)
+import Shelley.Spec.Ledger.EpochBoundary (obligation)
 import Shelley.Spec.Ledger.Keys (DSignable, Hash)
 import Shelley.Spec.Ledger.LedgerState
   ( AccountState,
     DPState (..),
     DState (..),
     Ix,
     PState (..),
-    UTxOState,
+    UTxOState (..),
   )
 import Shelley.Spec.Ledger.PParams (PParams)
 import Shelley.Spec.Ledger.STS.Delegs (DELEGS, DelegsEnv (..))
@@ -95,6 +99,23 @@ instance
   initialRules = []
   transitionRules = [ledgerTransition]
 
+  renderAssertionViolation AssertionViolation {avSTS, avMsg, avCtx, avState} =
+    "AssertionViolation (" <> avSTS <> "): " <> avMsg
+      <> "\n"
+      <> show avCtx
+      <> "\n"
+      <> show avState
+
+  assertions =
+    [ PostCondition
+        "Deposit pot must equal obligation"
+        ( \(TRC (LedgerEnv {ledgerPp}, _, _))
+           (utxoSt, DPState {_dstate, _pstate}) ->
+              obligation ledgerPp (_rewards _dstate) (_pParams _pstate)
+                == _deposited utxoSt
+        )
+    ]
+
 instance (Crypto crypto) => NoUnexpectedThunks (PredicateFailure (LEDGER crypto))
 
 instance

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Mir.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Mir.hs
@@ -17,7 +17,8 @@ where
 import Cardano.Prelude (NoUnexpectedThunks (..))
 import Control.Iterate.SetAlgebra (dom, eval, (∪+), (◁))
 import Control.State.Transition
-  ( InitialRule,
+  ( Assertion (..),
+    InitialRule,
     STS (..),
     TRC (..),
     TransitionRule,
@@ -63,6 +64,15 @@ instance Typeable crypto => STS (MIR crypto) where
   initialRules = [initialMir]
   transitionRules = [mirTransition]
 
+  assertions =
+    [ PostCondition
+        "MIR may not create or remove reward accounts"
+        ( \(TRC (_, st, _)) st' ->
+            let r = _rewards . _dstate . _delegationState . esLState
+             in length (r st) == length (r st')
+        )
+    ]
+
 instance NoUnexpectedThunks (PredicateFailure (MIR crypto))
 
 initialMir :: InitialRule (MIR crypto)

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/PoolReap.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/PoolReap.hs
@@ -14,7 +14,8 @@ where
 import Cardano.Prelude (NoUnexpectedThunks (..))
 import Control.Iterate.SetAlgebra (dom, eval, (∈), (∪+), (⋪), (⋫), (▷), (◁))
 import Control.State.Transition
-  ( STS (..),
+  ( Assertion (..),
+    STS (..),
     TRC (..),
     TransitionRule,
     judgmentContext,
@@ -24,6 +25,7 @@ import qualified Data.Set as Set
 import Data.Typeable (Typeable)
 import GHC.Generics (Generic)
 import Shelley.Spec.Ledger.BaseTypes (ShelleyBase)
+import Shelley.Spec.Ledger.EpochBoundary (obligation)
 import Shelley.Spec.Ledger.LedgerState
   ( AccountState (..),
     DState (..),
@@ -61,6 +63,21 @@ instance Typeable crypto => STS (POOLREAP crypto) where
     ]
   transitionRules = [poolReapTransition]
 
+  assertions =
+    [ PostCondition
+        "Deposit pot must equal obligation"
+        ( \(TRC (pp, _, _)) st ->
+            obligation pp (_rewards $ prDState st) (_pParams $ prPState st)
+              == _deposited (prUTxOSt st)
+        ),
+      PostCondition
+        "PoolReap may not create or remove reward accounts"
+        ( \(TRC (_, st, _)) st' ->
+            let r = _rewards . prDState
+             in length (r st) == length (r st')
+        )
+    ]
+
 instance NoUnexpectedThunks (PredicateFailure (POOLREAP crypto))
 
 poolReapTransition :: TransitionRule (POOLREAP crypto)

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs
@@ -5,6 +5,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
@@ -27,6 +28,7 @@ import Cardano.Prelude (NoUnexpectedThunks (..), asks)
 import Control.Iterate.SetAlgebra (dom, eval, rng, (∪), (⊆), (⋪))
 import Control.State.Transition
   ( Assertion (..),
+    AssertionViolation (..),
     Embed,
     IRC (..),
     InitialRule,
@@ -103,7 +105,7 @@ data UtxoEnv crypto
   deriving (Show)
 
 instance
-  Crypto crypto =>
+  (Crypto crypto) =>
   STS (UTXO crypto)
   where
   type State (UTXO crypto) = UTxOState crypto
@@ -142,12 +144,22 @@ instance
   transitionRules = [utxoInductive]
   initialRules = [initialLedgerState]
 
+  renderAssertionViolation AssertionViolation {avSTS, avMsg, avCtx, avState} =
+    "AssertionViolation (" <> avSTS <> "): " <> avMsg
+      <> "\n"
+      <> show avCtx
+      <> "\n"
+      <> show avState
+
   assertions =
-    [ PostCondition
+    [ PreCondition
+        "Deposit pot must not be negative (pre)"
+        (\(TRC (_, st, _)) -> _deposited st >= 0),
+      PostCondition
         "UTxO must increase fee pot"
         (\(TRC (_, st, _)) st' -> _fees st' >= _fees st),
       PostCondition
-        "Deposit pot must not be negative"
+        "Deposit pot must not be negative (post)"
         (\_ st' -> _deposited st' >= 0),
       let utxoBalance us = _deposited us + _fees us + balance (_utxo us)
           withdrawals txb = foldl' (+) (Coin 0) $ unWdrl $ _wdrls txb