Refactor nonce transitions in the exec spec.

We also introduce functions in the API to manage the chain transition,
meaning that the consumer should not need to call `applySTS` themselves.

shelley/chain-and-ledger/executable-spec/shelley-spec-ledger.cabal

@@ -28,25 +28,21 @@ library
                      Shelley.Spec.Ledger.Coin
                      Shelley.Spec.Ledger.Core
                      Shelley.Spec.Ledger.Credential
+                     Shelley.Spec.Ledger.Delegation.Certificates
+                     Shelley.Spec.Ledger.Delegation.PoolParams
+                     Shelley.Spec.Ledger.EpochBoundary
                      Shelley.Spec.Ledger.Genesis
                      Shelley.Spec.Ledger.Keys
-                     Shelley.Spec.Ledger.UTxO
-                     Shelley.Spec.Ledger.Slot
-                     Shelley.Spec.Ledger.PParams
-                     Shelley.Spec.Ledger.Rewards
-                     Shelley.Spec.Ledger.EpochBoundary
                      Shelley.Spec.Ledger.LedgerState
                      Shelley.Spec.Ledger.MetaData
-                     Shelley.Spec.Ledger.Serialization
-                     Shelley.Spec.Ledger.Delegation.PoolParams
-                     Shelley.Spec.Ledger.Delegation.Certificates
                      Shelley.Spec.Ledger.OCert
                      Shelley.Spec.Ledger.Orphans
-                     Shelley.Spec.Ledger.Tx
-                     Shelley.Spec.Ledger.TxData
+                     Shelley.Spec.Ledger.PParams
+                     Shelley.Spec.Ledger.Rewards
                      Shelley.Spec.Ledger.Scripts
+                     Shelley.Spec.Ledger.Serialization
+                     Shelley.Spec.Ledger.Slot
                      Shelley.Spec.Ledger.STS.Bbody
-                     Shelley.Spec.Ledger.STS.Tick
                      Shelley.Spec.Ledger.STS.Chain
                      Shelley.Spec.Ledger.STS.Deleg
                      Shelley.Spec.Ledger.STS.Delegs
@@ -65,9 +61,14 @@ library
                      Shelley.Spec.Ledger.STS.Prtcl
                      Shelley.Spec.Ledger.STS.Rupd
                      Shelley.Spec.Ledger.STS.Snap
+                     Shelley.Spec.Ledger.STS.Tick
+                     Shelley.Spec.Ledger.STS.Tickn
                      Shelley.Spec.Ledger.STS.Updn
                      Shelley.Spec.Ledger.STS.Utxo
                      Shelley.Spec.Ledger.STS.Utxow
+                     Shelley.Spec.Ledger.Tx
+                     Shelley.Spec.Ledger.TxData
+                     Shelley.Spec.Ledger.UTxO
 
                      Shelley.Spec.Ledger.Crypto
 

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/API/Protocol.hs

@@ -2,6 +2,7 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE StrictData #-}
 {-# LANGUAGE TypeApplications #-}
 
@@ -12,24 +13,34 @@
 -- state needed for protocol execution, both now and in a 2k-slot window.
 module Shelley.Spec.Ledger.API.Protocol
   ( STS.Prtcl.PrtclEnv,
-    mkPrtclEnv,
     LedgerView (..),
     currentLedgerView,
     -- $timetravel
     futureLedgerView,
+    -- $chainstate
+    ChainState(..),
+    ChainTransitionError(..),
+    tickChainState,
+    updateChainState,
   )
 where
 
 import Cardano.Binary (FromCBOR (..), ToCBOR (..), decodeListLenOf, encodeListLen)
+import Cardano.Crypto.DSIGN.Class
+import Cardano.Crypto.KES.Class
+import Cardano.Crypto.VRF.Class
 import Cardano.Prelude (NoUnexpectedThunks (..))
 import Control.Arrow (left, right)
 import Control.Monad.Except
 import Control.Monad.Trans.Reader (runReader)
 import Control.State.Transition.Extended (PredicateFailure, TRC (..), applySTS)
+import Data.Either (fromRight)
 import Data.Map.Strict (Map)
 import GHC.Generics (Generic)
+import GHC.Natural
 import Shelley.Spec.Ledger.API.Validation
-import Shelley.Spec.Ledger.BaseTypes (Globals, Nonce)
+import Shelley.Spec.Ledger.BaseTypes (Globals, Nonce, Seed)
+import Shelley.Spec.Ledger.BlockChain (BHBody, BHeader)
 import Shelley.Spec.Ledger.Crypto
 import Shelley.Spec.Ledger.Delegation.Certificates (PoolDistr)
 import Shelley.Spec.Ledger.Keys (GenDelegs)
@@ -42,9 +53,11 @@ import Shelley.Spec.Ledger.LedgerState
     _dstate,
     _genDelegs,
   )
+import Shelley.Spec.Ledger.OCert (KESPeriod)
 import Shelley.Spec.Ledger.PParams (PParams)
 import qualified Shelley.Spec.Ledger.STS.Prtcl as STS.Prtcl
 import Shelley.Spec.Ledger.STS.Tick (TICK, TickEnv (..))
+import qualified Shelley.Spec.Ledger.STS.Tickn as STS.Tickn
 import Shelley.Spec.Ledger.Slot (SlotNo)
 
 -- | Data required by the Transitional Praos protocol from the Shelley ledger.
@@ -88,20 +101,16 @@ instance Crypto crypto => ToCBOR (LedgerView crypto) where
 -- epoch.
 mkPrtclEnv ::
   LedgerView crypto ->
-  -- | New epoch marker. This should be true iff this execution of the PRTCL
-  -- rule is being run on the first block in a new epoch.
-  Bool ->
+  -- | Epoch nonce
   Nonce ->
   STS.Prtcl.PrtclEnv crypto
 mkPrtclEnv
   LedgerView
-    { lvProtParams,
-      lvOverlaySched,
+    { lvOverlaySched,
       lvPoolDistr,
       lvGenDelegs
     } =
     STS.Prtcl.PrtclEnv
-      lvProtParams
       lvOverlaySched
       lvPoolDistr
       lvGenDelegs
@@ -187,3 +196,101 @@ futureLedgerView globals ss slot =
     tickEnv =
       TickEnv
         (getGKeys ss)
+
+-- $chainstate
+--
+-- Chain state operations
+--
+-- The chain state is an amalgam of the protocol state and the ticked nonce.
+
+data ChainState c = ChainState
+  { csProtocol :: !(STS.Prtcl.PrtclState c),
+    csTickn :: !STS.Tickn.TicknState
+  }
+  deriving (Eq, Show, Generic)
+
+instance Crypto c => NoUnexpectedThunks (ChainState c)
+
+newtype ChainTransitionError crypto
+  = ChainTransitionError [PredicateFailure (STS.Prtcl.PRTCL crypto)]
+  deriving (Generic)
+
+instance (Crypto crypto) => NoUnexpectedThunks (ChainTransitionError crypto)
+
+deriving instance (Crypto crypto) => Eq (ChainTransitionError crypto)
+
+deriving instance (Crypto crypto) => Show (ChainTransitionError crypto)
+
+-- | Tick the chain state to a new epoch.
+tickChainState ::
+  Globals ->
+  LedgerView c ->
+  -- | Are we in a new epoch?
+  Bool ->
+  -- | Previous hash as nonce
+  Nonce ->
+  ChainState c ->
+  ChainState c
+tickChainState
+  globals
+  LedgerView {lvProtParams}
+  isNewEpoch
+  prevHashAsNonce
+  cs@ChainState {csProtocol, csTickn} = cs {csTickn = newTickState}
+    where
+      STS.Prtcl.PrtclState _ _ candidateNonce = csProtocol
+      err = error "Panic! tickChainState failed."
+      newTickState =
+        fromRight err . flip runReader globals
+          . applySTS @STS.Tickn.TICKN
+          $ TRC
+            ( STS.Tickn.TicknEnv
+                lvProtParams
+                candidateNonce
+                prevHashAsNonce,
+              csTickn,
+              isNewEpoch
+            )
+
+-- | Update the chain state based upon a
+updateChainState ::
+  forall crypto m.
+  ( Crypto crypto,
+    MonadError (ChainTransitionError crypto) m,
+    Cardano.Crypto.DSIGN.Class.Signable
+      (DSIGN crypto)
+      ( Cardano.Crypto.KES.Class.VerKeyKES (KES crypto),
+        Natural,
+        Shelley.Spec.Ledger.OCert.KESPeriod
+      ),
+    Cardano.Crypto.KES.Class.Signable
+      (KES crypto)
+      (Shelley.Spec.Ledger.BlockChain.BHBody crypto),
+    Cardano.Crypto.VRF.Class.Signable
+      (VRF crypto)
+      Shelley.Spec.Ledger.BaseTypes.Seed
+  ) =>
+  Globals ->
+  LedgerView crypto ->
+  BHeader crypto ->
+  ChainState crypto ->
+  m (ChainState crypto)
+updateChainState
+  globals
+  lv
+  bh
+  cs@ChainState {csProtocol, csTickn} =
+    liftEither
+      . right (\newPrtclState -> cs {csProtocol = newPrtclState})
+      . left (ChainTransitionError . join)
+      $ res
+    where
+      res =
+        flip runReader globals
+          . applySTS @(STS.Prtcl.PRTCL crypto)
+          $ TRC
+            ( mkPrtclEnv lv epochNonce,
+              csProtocol,
+              bh
+            )
+      STS.Tickn.TicknState _ epochNonce = csTickn

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs

@@ -113,6 +113,7 @@ import Shelley.Spec.Ledger.STS.Prtcl
     prtlSeqChecks,
   )
 import Shelley.Spec.Ledger.STS.Tick (TICK, TickEnv (..))
+import Shelley.Spec.Ledger.STS.Tickn
 import Shelley.Spec.Ledger.Slot (EpochNo, SlotNo)
 import Shelley.Spec.Ledger.Tx (TxBody)
 import Shelley.Spec.Ledger.UTxO (UTxO (..), balance)
@@ -210,6 +211,7 @@ instance
         !Natural -- max protocol version
     | BbodyFailure !(PredicateFailure (BBODY crypto)) -- Subtransition Failures
     | TickFailure !(PredicateFailure (TICK crypto)) -- Subtransition Failures
+    | TicknFailure !(PredicateFailure TICKN) -- Subtransition Failures
     | PrtclFailure !(PredicateFailure (PRTCL crypto)) -- Subtransition Failures
     | PrtclSeqFailure !(PrtlSeqFailure crypto) -- Subtransition Failures
     deriving (Show, Eq, Generic)
@@ -272,11 +274,20 @@ chainTransition =
 
       let ph = lastAppliedHash lab
           etaPH = prevHashToNonce ph
-      PrtclState cs' eta0' etaV' etaC' etaH' <-
+
+      TicknState eta0' etaH' <-
+        trans @TICKN $
+          TRC
+            ( TicknEnv pp' etaC etaPH,
+              TicknState eta0 etaH,
+              (e1 /= e2)
+            )
+
+      PrtclState cs' etaV' etaC' <-
         trans @(PRTCL crypto) $
           TRC
-            ( PrtclEnv pp' osched _pd _genDelegs (e1 /= e2) etaPH,
-              PrtclState cs eta0 etaV etaC etaH,
+            ( PrtclEnv osched _pd _genDelegs eta0',
+              PrtclState cs etaV etaC,
               bh
             )
 
@@ -306,6 +317,17 @@ instance
   where
   wrapFailed = BbodyFailure
 
+instance
+  ( Crypto crypto,
+    DSignable crypto (VerKeyKES crypto, Natural, KESPeriod),
+    DSignable crypto (Hash crypto (TxBody crypto)),
+    KESignable crypto (BHBody crypto),
+    VRF.Signable (VRF crypto) Seed
+  ) =>
+  Embed TICKN (CHAIN crypto)
+  where
+  wrapFailed = TicknFailure
+
 instance
   ( Crypto crypto,
     DSignable crypto (VerKeyKES crypto, Natural, KESPeriod),

shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs

@@ -61,7 +61,6 @@ import Shelley.Spec.Ledger.Keys
   )
 import Shelley.Spec.Ledger.LedgerState (OBftSlot)
 import Shelley.Spec.Ledger.OCert (KESPeriod)
-import Shelley.Spec.Ledger.PParams (PParams)
 import Shelley.Spec.Ledger.STS.Overlay (OVERLAY, OverlayEnv (..))
 import Shelley.Spec.Ledger.STS.Updn (UPDN, UpdnEnv (..), UpdnState (..))
 import Shelley.Spec.Ledger.Slot (BlockNo, SlotNo)
@@ -73,24 +72,18 @@ data PrtclState crypto
       !(Map (KeyHash 'BlockIssuer crypto) Natural)
       -- ^ Operation Certificate counters
       !Nonce
-      -- ^ Current epoch nonce
-      !Nonce
       -- ^ Evolving nonce
       !Nonce
       -- ^ Candidate nonce
-      !Nonce
-      -- ^ Prev epoch hash nonce
   deriving (Generic, Show, Eq)
 
 instance Crypto crypto => ToCBOR (PrtclState crypto) where
-  toCBOR (PrtclState m n1 n2 n3 n4) =
+  toCBOR (PrtclState m n2 n3) =
     mconcat
       [ encodeListLen 5,
         toCBOR m,
-        toCBOR n1,
         toCBOR n2,
-        toCBOR n3,
-        toCBOR n4
+        toCBOR n3
       ]
 
 instance Crypto crypto => FromCBOR (PrtclState crypto) where
@@ -100,19 +93,14 @@ instance Crypto crypto => FromCBOR (PrtclState crypto) where
       <$> fromCBOR
       <*> fromCBOR
       <*> fromCBOR
-      <*> fromCBOR
-      <*> fromCBOR
 
 instance Crypto crypto => NoUnexpectedThunks (PrtclState crypto)
 
 data PrtclEnv crypto
-  = -- | New epoch marker
-    PrtclEnv
-      PParams
+  = PrtclEnv
       (Map SlotNo (OBftSlot crypto))
       (PoolDistr crypto)
       (GenDelegs crypto)
-      Bool
       Nonce
   deriving (Generic)
 
@@ -163,33 +151,31 @@ prtclTransition ::
   TransitionRule (PRTCL crypto)
 prtclTransition = do
   TRC
-    ( PrtclEnv pp osched pd dms ne etaPH,
-      PrtclState cs eta0 etaV etaC etaH,
+    ( PrtclEnv osched pd dms eta0,
+      PrtclState cs etaV etaC,
       bh
       ) <-
     judgmentContext
   let bhb = bhbody bh
       slot = bheaderSlotNo bhb
       eta = mkNonceFromOutputVRF . VRF.certifiedOutput $ bheaderEta bhb
 
-  UpdnState eta0' etaV' etaC' etaH' <-
+  UpdnState etaV' etaC' <-
     trans @(UPDN crypto) $
       TRC
-        ( UpdnEnv eta pp etaPH ne,
-          UpdnState eta0 etaV etaC etaH,
+        ( UpdnEnv eta,
+          UpdnState etaV etaC,
           slot
         )
   cs' <-
     trans @(OVERLAY crypto) $
-      TRC (OverlayEnv osched eta0' pd dms, cs, bh)
+      TRC (OverlayEnv osched eta0 pd dms, cs, bh)
 
   pure $
     PrtclState
       cs'
-      eta0'
       etaV'
       etaC'
-      etaH'
 
 instance (Crypto crypto) => NoUnexpectedThunks (PredicateFailure (PRTCL crypto))