Fix errors discovered during conformance testing of valid chains agai…

…nst the implementation in `cardano-ledger`.

- Fix the implementation of `PVBUMP`: the last proposal was being taken instead of the first one.
- Simplify the `EPOCH` rule.
- Count the block endorsement when registering it.
- Remove `cfmThd` use `upAdptThd` instead, since these are the same value, and we have no compelling reasons for using different ones here. This closes #623
- Perform application version change, even when there are not votes in the block.
- Generate the update id's based on the `pwd` set (otherwise we would be generating duplicated proposal id's).
- Add a constant `c` to `GlobalParams` which is used to bound the concrete size. We use this constant when choosing the next `B` factor, and when elaborating this factor into a concrete one.

CODEOWNERS

@@ -10,6 +10,6 @@ shelley/chain-and-ledger/executable-spec/ @mgudemann @JaredCorduan
 shelley/chain-and-ledger/formal-spec/ @JaredCorduan @mgudemann
 nix/ @nc6 @ruhatch
 scripts/ @nc6 @ruhatch
-byron/chain/ @nc6 @mdimjasevic
+byron/chain/ @nc6
 byron/ledger/ @nc6 @dnadales
 byron/semantics/ @nc6 @dnadales

byron/chain/executable-spec/cs-blockchain.cabal

@@ -24,7 +24,6 @@ flag development
 library
   exposed-modules:     Cardano.Spec.Chain.STS.Block
                      , Cardano.Spec.Chain.STS.Rule.BBody
-                     , Cardano.Spec.Chain.STS.Rule.BHead
                      , Cardano.Spec.Chain.STS.Rule.Bupi
                      , Cardano.Spec.Chain.STS.Rule.Chain
                      , Cardano.Spec.Chain.STS.Rule.Epoch

byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Block.hs

@@ -83,15 +83,18 @@ data Block
 instance HasTypeReps Block
 makeLenses ''Block
 
--- | Block update payload
-bUpdPayload :: Block -> (Maybe UProp, [Vote])
-bUpdPayload b = (b ^. bBody ^. bUpdProp, b ^. bBody ^. bUpdVotes)
-
-
 -- | Protocol version endorsment
 bEndorsment :: Block -> (ProtVer, VKey)
 bEndorsment b = (b ^. bBody ^. bProtVer, b ^. bHeader ^. bhIssuer)
 
+-- | Slot the block is published in
+bSlot :: Block -> Slot
+bSlot b = b ^. bHeader ^. bhSlot
+
+-- | Block update payload
+bUpdPayload :: Block -> (Maybe UProp, [Vote])
+bUpdPayload b = (b ^. bBody ^. bUpdProp, b ^. bBody ^. bUpdVotes)
+
 -- | Compute the abstract size (in words) that a block takes.
 bSize :: Block -> Natural
 bSize b = bHeaderSize (b ^. bHeader) + bBodySize (b ^. bBody)

byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/Chain.hs

@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
@@ -37,7 +38,6 @@ import           Ledger.UTxO (UTxO)
 
 import           Cardano.Spec.Chain.STS.Block
 import           Cardano.Spec.Chain.STS.Rule.BBody
-import           Cardano.Spec.Chain.STS.Rule.BHead
 import           Cardano.Spec.Chain.STS.Rule.Epoch (EPOCH, sEpoch)
 import           Cardano.Spec.Chain.STS.Rule.Pbft
 import qualified Cardano.Spec.Chain.STS.Rule.SigCnt as SigCntGen
@@ -70,7 +70,8 @@ instance STS CHAIN where
   type Signal CHAIN = Block
 
   data PredicateFailure CHAIN
-    = BHeadFailure (PredicateFailure BHEAD)
+    = EpochFailure (PredicateFailure EPOCH)
+    | HeaderSizeTooBig BlockHeader Natural (Threshold Natural)
     | BBodyFailure (PredicateFailure BBODY)
     | PBFTFailure (PredicateFailure PBFT)
     | MaximumBlockSize Natural Natural
@@ -133,25 +134,26 @@ instance STS CHAIN where
       TRC ((sNow, utxoGenesis, ads, _pps, k), (sLast, sgs, h, utxoSt, ds, us), b) <- judgmentContext
       let dm = _dIStateDelegationMap ds :: Bimap VKeyGenesis VKey
       us' <-
-        trans @BHEAD $ TRC ((dm, sLast, k), us, b ^. bHeader)
+        trans @EPOCH $ TRC ((sEpoch sLast k, k), us, bSlot b)
+      headerIsValid us' (b ^. bHeader)
       let ppsUs' = snd (us' ^. _1)
-      (h', sgs') <-
-        trans @PBFT  $ TRC ((ppsUs', dm, sLast, sNow, k), (h, sgs), b ^. bHeader)
       (utxoSt', ds', us'') <- trans @BBODY $ TRC
         (
           ( ppsUs'
-          , sEpoch (b ^. bHeader ^. bhSlot) k
+          , sEpoch (bSlot b) k
           , utxoGenesis
           , fromIntegral (Set.size ads)
           , k
           )
         , (utxoSt, ds, us')
         , b
         )
-      pure $! (b ^. bHeader ^. bhSlot, sgs', h', utxoSt', ds', us'')
+      (h', sgs') <-
+        trans @PBFT  $ TRC ((ppsUs', dm, sLast, sNow, k), (h, sgs), b ^. bHeader)
+      pure $! (bSlot b, sgs', h', utxoSt', ds', us'')
 
-instance Embed BHEAD CHAIN where
-  wrapFailed = BHeadFailure
+instance Embed EPOCH CHAIN where
+  wrapFailed = EpochFailure
 
 instance Embed BBODY CHAIN where
   wrapFailed = BBodyFailure
@@ -169,6 +171,12 @@ genesisHash :: Hash
 -- Not sure we need a concrete hash in the specs ...
 genesisHash = Hash $ H.hash ("" :: ByteString)
 
+headerIsValid :: UPIState -> BlockHeader -> Rule CHAIN 'Transition ()
+headerIsValid us bh = do
+  let sMax = snd (us ^. _1) ^. maxHdrSz
+  bHeaderSize bh <= sMax
+    ?! HeaderSizeTooBig bh (bHeaderSize bh) (Threshold sMax)
+
 -- | Lens for the delegation interface state contained in the chain state.
 disL :: Lens' (State CHAIN) DIState
 disL = _5

byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/Epoch.hs

@@ -39,7 +39,7 @@ instance STS EPOCH where
     [ do
         TRC ((e_c, k), us, s) <- judgmentContext
         if sEpoch s k <= e_c
-          then do
+          then
             pure $! us
           else do
             us' <- trans @UPIEC $ TRC ((s, k), us, ())