Assertions

IntersectMBO · Jul 8, 2020 · f9e19fa · f9e19fa
1 parent 8c26630
commit f9e19fa
Show file tree

Hide file tree

Showing 3 changed files with 66 additions and 9 deletions.
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
@@ -135,7 +135,11 @@ ledgerTransition = do
 
   dpstate' <-
     trans @(DELEGS crypto) $
-      TRC (DelegsEnv slot txIx pp tx account, dpstate, StrictSeq.getSeq $ _certs $ _body tx)
+      TRC
+        ( DelegsEnv slot txIx pp tx account,
+          dpstate,
+          StrictSeq.getSeq $ _certs $ _body tx
+        )
 
   let DPState dstate pstate = dpstate
       genDelegs = _genDelegs dstate

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
@@ -13,10 +13,26 @@ module Shelley.Spec.Ledger.STS.Pool
   )
 where
 
-import Cardano.Binary (FromCBOR (..), ToCBOR (..), decodeListLen, decodeWord, encodeListLen, matchSize)
+import Cardano.Binary
+  ( FromCBOR (..),
+    ToCBOR (..),
+    decodeListLen,
+    decodeWord,
+    encodeListLen,
+    matchSize,
+  )
 import Cardano.Prelude (NoUnexpectedThunks (..))
 import Control.Monad.Trans.Reader (asks)
-import Control.State.Transition (STS (..), TRC (..), TransitionRule, failBecause, judgmentContext, liftSTS, (?!))
+import Control.State.Transition
+  ( Assertion (..),
+    STS (..),
+    TRC (..),
+    TransitionRule,
+    failBecause,
+    judgmentContext,
+    liftSTS,
+    (?!),
+  )
 import Data.Kind (Type)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
@@ -25,13 +41,18 @@ import Data.Word (Word64, Word8)
 import GHC.Generics (Generic)
 import Shelley.Spec.Ledger.BaseTypes (Globals (..), ShelleyBase, invalidKey)
 import Shelley.Spec.Ledger.Coin (Coin)
-import Shelley.Spec.Ledger.Core (addpair, haskey, removekey)
+import Shelley.Spec.Ledger.Core (addpair, dom, haskey, removekey)
 import Shelley.Spec.Ledger.Crypto (Crypto)
 import Shelley.Spec.Ledger.Keys (KeyHash (..), KeyRole (..))
 import Shelley.Spec.Ledger.LedgerState (PState (..), emptyPState)
 import Shelley.Spec.Ledger.PParams (PParams, PParams' (..))
 import Shelley.Spec.Ledger.Slot (EpochNo (..), SlotNo, epochInfoEpoch)
-import Shelley.Spec.Ledger.TxData (DCert (..), PoolCert (..), PoolParams (..), StakePools (..))
+import Shelley.Spec.Ledger.TxData
+  ( DCert (..),
+    PoolCert (..),
+    PoolParams (..),
+    StakePools (..),
+  )
 
 data POOL (crypto :: Type)
 
@@ -66,6 +87,14 @@ instance Typeable crypto => STS (POOL crypto) where
 
   transitionRules = [poolDelegationTransition]
 
+  assertions =
+    [ PreCondition
+        "_stPools and _pParams must have the same domain"
+        ( \(TRC (_, st, _)) ->
+            dom (unStakePools $ _stPools st) == dom (_pParams st)
+        )
+    ]
+
 instance NoUnexpectedThunks (PredicateFailure (POOL crypto))
 
 instance

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
@@ -25,7 +25,8 @@ import Cardano.Binary
   )
 import Cardano.Prelude (NoUnexpectedThunks (..), asks)
 import Control.State.Transition
-  ( Embed,
+  ( Assertion (..),
+    Embed,
     IRC (..),
     InitialRule,
     STS (..),
@@ -37,7 +38,7 @@ import Control.State.Transition
     wrapFailed,
     (?!),
   )
-import Data.Foldable (toList)
+import Data.Foldable (foldl', toList)
 import qualified Data.Map.Strict as Map
 import Data.Set (Set)
 import qualified Data.Set as Set
@@ -70,8 +71,15 @@ import Shelley.Spec.Ledger.Serialization
   )
 import Shelley.Spec.Ledger.Slot (SlotNo)
 import Shelley.Spec.Ledger.Tx (Tx (..), TxIn, TxOut (..))
-import Shelley.Spec.Ledger.TxData (TxBody (..))
-import Shelley.Spec.Ledger.UTxO (UTxO (..), totalDeposits, txins, txouts, txup)
+import Shelley.Spec.Ledger.TxData (TxBody (..), unWdrl)
+import Shelley.Spec.Ledger.UTxO
+  ( UTxO (..),
+    balance,
+    totalDeposits,
+    txins,
+    txouts,
+    txup,
+  )
 
 data UTXO crypto
 
@@ -117,6 +125,22 @@ instance
   transitionRules = [utxoInductive]
   initialRules = [initialLedgerState]
 
+  assertions =
+    [ PostCondition
+        "UTxO must increase fee pot"
+        (\(TRC (_, st, _)) st' -> _fees st' >= _fees st),
+      PostCondition
+        "Deposit pot must not be negative"
+        (\_ st' -> _deposited st' >= 0),
+      let utxoBalance us = _deposited us + _fees us + balance (_utxo us)
+          withdrawals txb = foldl' (+) (Coin 0) $ unWdrl $ _wdrls txb
+       in PostCondition
+            "Should preserve ADA in the UTxO state"
+            ( \(TRC (_, us, tx)) us' ->
+                utxoBalance us + withdrawals (_body tx) == utxoBalance us'
+            )
+    ]
+
 instance NoUnexpectedThunks (PredicateFailure (UTXO crypto))
 
 instance