[747] BBODY STS - sync formal and exec. spec

IntersectMBO · Sep 2, 2019 · c70738a · c70738a
1 parent a3e41bc
commit c70738a
Showing 1 changed file with 12 additions and 6 deletions.
diff --git a/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs b/shelley/chain-and-ledger/executable-spec/src/STS/Bbody.hs
@@ -17,6 +17,7 @@ import qualified Data.Set as Set
 import           BlockChain
 import           EpochBoundary
 import           Keys
+import           Ledger.Core ((∈))
 import           LedgerState
 import           PParams
 import           Slot
@@ -45,6 +46,7 @@ instance
 
   data PredicateFailure (BBODY hashAlgo dsignAlgo kesAlgo)
     = WrongBlockBodySizeBBODY
+    | InvalidBodyHashBBODY
     | LedgersFailure (PredicateFailure (LEDGERS hashAlgo dsignAlgo))
     deriving (Show, Eq)
 
@@ -59,16 +61,20 @@ bbodyTransition
      )
   => TransitionRule (BBODY hashAlgo dsignAlgo kesAlgo)
 bbodyTransition = do
-  TRC ((oslots, pp), (ls, b), Block (BHeader bhb _) txs'@(TxSeq txs)) <- judgmentContext
+  TRC ( (oslots, pp)
+      , (ls, b)
+      , Block (BHeader bhb _) txsSeq@(TxSeq txs)) <- judgmentContext
   let hk = hashKey $ bvkcold bhb
-  bBodySize txs' == fromIntegral (hBbsize bhb) ?! WrongBlockBodySizeBBODY
 
-  ls' <-
-    trans @(LEDGERS hashAlgo dsignAlgo) $ TRC ((bheaderSlot bhb, pp), ls, txs)
+  bBodySize txsSeq == fromIntegral (hBbsize bhb) ?! WrongBlockBodySizeBBODY
 
-  let b' = incrBlocks (Set.member (bheaderSlot bhb) oslots) hk b
+  bhbHash txsSeq == bhash bhb ?! InvalidBodyHashBBODY
 
-  pure (ls', b')
+  ls' <- trans @(LEDGERS hashAlgo dsignAlgo)
+         $ TRC ((bheaderSlot bhb, pp), ls, txs)
+
+  pure ( ls'
+       , incrBlocks (bheaderSlot bhb ∈ oslots) hk b)
 
 instance
   ( HashAlgorithm hashAlgo