generalize ApplyBlock.

IntersectMBO · Apr 8, 2021 · b2fb3b9 · b2fb3b9
1 parent 0a7052a
commit b2fb3b9
Show file tree

Hide file tree

Showing 4 changed files with 466 additions and 40 deletions.
diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -50,6 +50,7 @@ module Control.State.Transition.Extended
     applySTS,
     applySTSIndifferently,
     reapplySTS,
+    applySTSList, applySTSList_,
 
     -- * Random thing
     Threshold (..),
@@ -551,3 +552,29 @@ straverse_ f = foldr c (pure ())
 sfor_ :: (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
 {-# INLINE sfor_ #-}
 sfor_ = flip straverse_
+
+applySTSList
+  :: forall sts proxy.  (STS sts, Environment sts ~ ())
+  => proxy sts
+  -> State sts
+  -> [Signal sts]
+  -> BaseM sts (Either [[PredicateFailure sts]] (State sts))
+applySTSList = applySTSList_ (pure ())
+
+applySTSList_
+  :: forall sts proxy.  (STS sts)
+  => BaseM sts (Environment sts)
+  -> proxy sts
+  -> State sts
+  -> [Signal sts]
+  -> BaseM sts (Either [[PredicateFailure sts]] (State sts))
+applySTSList_ mkEnv _ = go
+  where
+    go :: State sts -> [Signal sts] -> BaseM sts (Either [[PredicateFailure sts]] (State sts))
+    go st [] = pure $ Right st
+    go st (x:xs) = do
+      env <- mkEnv
+      applySTS @sts (TRC (env, st, x)) >>= \case
+        Right st' -> go st' xs
+        st'@(Left _) -> pure st'
+
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/API/Validation.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/API/Validation.hs
@@ -17,6 +17,7 @@ module Shelley.Spec.Ledger.API.Validation
     TickTransitionError (..),
     BlockTransitionError (..),
     chainChecks,
+    ApplyBlock'(..)
   )
 where
 
@@ -26,12 +27,12 @@ import Cardano.Ledger.Era (Crypto, Era)
 import Cardano.Ledger.Shelley (ShelleyEra)
 import Control.Arrow (left, right)
 import Control.Monad.Except
-import Control.Monad.Trans.Reader (runReader)
+import Control.Monad.Trans.Reader (runReader, Reader)
 import Control.State.Transition.Extended
 import GHC.Generics (Generic)
 import NoThunks.Class (NoThunks (..))
 import Shelley.Spec.Ledger.API.Protocol (PraosCrypto)
-import Shelley.Spec.Ledger.BaseTypes (Globals (..), ShelleyBase)
+import Shelley.Spec.Ledger.BaseTypes (Globals (..))
 import Shelley.Spec.Ledger.BlockChain
 import Shelley.Spec.Ledger.LedgerState (NewEpochState)
 import qualified Shelley.Spec.Ledger.LedgerState as LedgerState
@@ -40,13 +41,134 @@ import qualified Shelley.Spec.Ledger.STS.Bbody as STS
 import qualified Shelley.Spec.Ledger.STS.Chain as STS
 import Shelley.Spec.Ledger.STS.EraMapping ()
 import Shelley.Spec.Ledger.Slot (SlotNo)
+import Data.Proxy
 
 {-------------------------------------------------------------------------------
   Block validation API
 -------------------------------------------------------------------------------}
 
+
+-- TODO: get rid of GlobalEnvironment and use BaseM directly
+-- TOD: pass ApplySTSOpts
 class
-  ( ChainData (Block era),
+    ( STS (Core.EraRule "TICK" era)
+    , STS (Core.EraRule "BBODY" era)
+    , Environment (Core.EraRule "TICK" era) ~ ()
+    , BaseM (Core.EraRule "TICK" era) ~ BaseM (Core.EraRule "BBODY" era)
+    ) => ApplyBlock' era where
+  type GlobalEnvironment era
+  type BTError era
+
+  -- | Apply the header level ledger transition.
+  --
+  -- This handles checks and updates that happen on a slot tick, as well as a
+  -- few header level checks, such as size constraints.
+  applyTick' :: proxy era
+    -> GlobalEnvironment era
+    -> State (Core.EraRule "TICK" era)
+    -> Signal (Core.EraRule "TICK" era)
+    -> State (Core.EraRule "TICK" era)
+  default applyTick' ::
+    (BaseM (Core.EraRule "TICK" era) ~ Reader (GlobalEnvironment era))
+    => proxy era
+    -> GlobalEnvironment era
+    -> State (Core.EraRule "TICK" era)
+    -> Signal (Core.EraRule "TICK" era)
+    -> State (Core.EraRule "TICK" era)
+  applyTick' _ globals state hdr =
+    either err id . flip runReader globals
+      . applySTS @(Core.EraRule "TICK" era)
+      $ TRC ((), state, hdr)
+    where
+      err :: Show a => a -> b
+      err msg = error $ "Panic! applyTick failed: " <> show msg
+  {-# INLINE applyTick' #-}
+
+  getBBodyState :: proxy era -> State (Core.EraRule "TICK" era) -> State (Core.EraRule "BBODY" era)
+  setBBodyState :: proxy era -> State (Core.EraRule "TICK" era) -> State (Core.EraRule "BBODY" era) -> State (Core.EraRule "TICK" era)
+  getBBodyEnv :: proxy era -> State (Core.EraRule "TICK" era) -> Environment (Core.EraRule "BBODY" era)
+  wrapBlockError :: proxy era -> [[PredicateFailure (Core.EraRule "BBODY" era)]] -> BTError era
+
+  -- | Apply the block level ledger transition.
+  applyBlock' :: proxy era
+    -> GlobalEnvironment era
+    -> State (Core.EraRule "TICK" era)
+    -> Signal (Core.EraRule "BBODY" era)
+    -> Either (BTError era) (State (Core.EraRule "TICK" era))
+  default applyBlock' ::
+    (BaseM (Core.EraRule "TICK" era) ~ Reader (GlobalEnvironment era))
+    => proxy era
+    -> GlobalEnvironment era
+    -> State (Core.EraRule "TICK" era)
+    -> Signal (Core.EraRule "BBODY" era)
+    -> Either (BTError era) (State (Core.EraRule "TICK" era))
+  applyBlock' _ globals state blk =
+        right (setBBodyState proxy state)
+      . left (wrapBlockError proxy)
+      $ res
+    where
+      proxy :: Proxy era
+      proxy = Proxy
+
+      res =
+        flip runReader globals . applySTS @(Core.EraRule "BBODY" era) $
+          TRC (getBBodyEnv proxy state, bbs, blk)
+      bbs = getBBodyState proxy state
+  {-# INLINE applyBlock' #-}
+
+
+  -- | Re-apply a ledger block to the same state it has been applied to before.
+  --
+  -- This function does no validation of whether the block applies successfully;
+  -- the caller implicitly guarantees that they have previously called
+  -- 'applyBlockTransition' on the same block and that this was successful.
+  reapplyBlock' :: proxy era
+    -> GlobalEnvironment era
+    -> State (Core.EraRule "TICK" era)
+    -> Signal (Core.EraRule "BBODY" era)
+    -> State (Core.EraRule "TICK" era)
+  default reapplyBlock' ::
+    (BaseM (Core.EraRule "TICK" era) ~ Reader (GlobalEnvironment era))
+    => proxy era
+    -> GlobalEnvironment era
+    -> State (Core.EraRule "TICK" era)
+    -> Signal (Core.EraRule "BBODY" era)
+    -> State (Core.EraRule "TICK" era)
+  reapplyBlock' _ globals state blk =
+    setBBodyState proxy state res
+    where
+      proxy :: Proxy era
+      proxy = Proxy
+      res =
+        flip runReader globals . reapplySTS @(Core.EraRule "BBODY" era) $
+          TRC (getBBodyEnv proxy state, bbs, blk)
+      bbs = getBBodyState proxy state
+  {-# INLINE reapplyBlock' #-}
+
+
+instance PraosCrypto crypto => ApplyBlock' (ShelleyEra crypto) where
+
+  type GlobalEnvironment (ShelleyEra crypto) = Globals
+  type BTError (ShelleyEra crypto) = BlockTransitionError (ShelleyEra crypto)
+
+  getBBodyState _ state = STS.BbodyState
+          (LedgerState.esLState $ LedgerState.nesEs state)
+          (LedgerState.nesBcur state)
+  {-# INLINE getBBodyState #-}
+  setBBodyState _ = updateNewEpochState
+  {-# INLINE setBBodyState #-}
+  getBBodyEnv _ = mkBbodyEnv
+  {-# INLINE getBBodyEnv #-}
+  wrapBlockError _ = BlockTransitionError . join
+  {-# INLINE wrapBlockError #-}
+
+
+
+class
+  ( BaseM (Core.EraRule "TICK" era) ~ BaseM (Core.EraRule "BBODY" era),
+    Signal (Core.EraRule "BBODY" era) ~ Block era,
+    BTError era ~ BlockTransitionError era,
+    ChainData (Block era),
     AnnotatedData (Block era),
     ChainData (BHeader (Crypto era)),
     AnnotatedData (BHeader (Crypto era)),
@@ -55,15 +177,10 @@ class
     ChainData (BlockTransitionError era),
     ChainData (STS.PredicateFailure (STS.CHAIN era)),
     STS (Core.EraRule "TICK" era),
-    BaseM (Core.EraRule "TICK" era) ~ ShelleyBase,
     Environment (Core.EraRule "TICK" era) ~ (),
     State (Core.EraRule "TICK" era) ~ NewEpochState era,
     Signal (Core.EraRule "TICK" era) ~ SlotNo,
-    STS (Core.EraRule "BBODY" era),
-    BaseM (Core.EraRule "BBODY" era) ~ ShelleyBase,
-    Environment (Core.EraRule "BBODY" era) ~ STS.BbodyEnv era,
-    State (Core.EraRule "BBODY" era) ~ STS.BbodyState era,
-    Signal (Core.EraRule "BBODY" era) ~ Block era
+    STS (Core.EraRule "BBODY" era)
   ) =>
   ApplyBlock era
   where
@@ -76,18 +193,13 @@ class
     NewEpochState era ->
     SlotNo ->
     NewEpochState era
-  default applyTick ::
+  default applyTick :: (ApplyBlock' era, GlobalEnvironment era ~ Globals) =>
     Globals ->
     NewEpochState era ->
     SlotNo ->
     NewEpochState era
-  applyTick globals state hdr =
-    either err id . flip runReader globals
-      . applySTS @(Core.EraRule "TICK" era)
-      $ TRC ((), state, hdr)
-    where
-      err :: Show a => a -> b
-      err msg = error $ "Panic! applyTick failed: " <> show msg
+  applyTick = applyTick' (Proxy :: Proxy era)
+  {-# INLINE applyTick #-}
 
   -- | Apply the block level ledger transition.
   applyBlock ::
@@ -96,25 +208,16 @@ class
     NewEpochState era ->
     Block era ->
     m (NewEpochState era)
-  default applyBlock ::
+  default applyBlock ::  (ApplyBlock' era, GlobalEnvironment era ~ Globals) =>
     (MonadError (BlockTransitionError era) m) =>
     Globals ->
     NewEpochState era ->
     Block era ->
     m (NewEpochState era)
   applyBlock globals state blk =
     liftEither
-      . right (updateNewEpochState state)
-      . left (BlockTransitionError . join)
-      $ res
-    where
-      res =
-        flip runReader globals . applySTS @(Core.EraRule "BBODY" era) $
-          TRC (mkBbodyEnv state, bbs, blk)
-      bbs =
-        STS.BbodyState
-          (LedgerState.esLState $ LedgerState.nesEs state)
-          (LedgerState.nesBcur state)
+      $ applyBlock' (Proxy :: Proxy era) globals state blk
+  {-# INLINE applyBlock #-}
 
   -- | Re-apply a ledger block to the same state it has been applied to before.
   --
@@ -126,21 +229,13 @@ class
     NewEpochState era ->
     Block era ->
     NewEpochState era
-  default reapplyBlock ::
+  default reapplyBlock :: (ApplyBlock' era, GlobalEnvironment era ~ Globals) =>
     Globals ->
     NewEpochState era ->
     Block era ->
     NewEpochState era
-  reapplyBlock globals state blk =
-    updateNewEpochState state res
-    where
-      res =
-        flip runReader globals . reapplySTS @(Core.EraRule "BBODY" era) $
-          TRC (mkBbodyEnv state, bbs, blk)
-      bbs =
-        STS.BbodyState
-          (LedgerState.esLState $ LedgerState.nesEs state)
-          (LedgerState.nesBcur state)
+  reapplyBlock = reapplyBlock' (Proxy :: Proxy era)
+  {-# INLINE reapplyBlock #-}
 
 instance PraosCrypto crypto => ApplyBlock (ShelleyEra crypto)
 

diff --git a/shelley/chain-and-ledger/shelley-spec-ledger-test/shelley-spec-ledger-test.cabal b/shelley/chain-and-ledger/shelley-spec-ledger-test/shelley-spec-ledger-test.cabal
@@ -46,6 +46,7 @@ library
     Test.Cardano.Crypto.VRF.Fake
     Test.Shelley.Spec.Ledger.BenchmarkFunctions
     Test.Shelley.Spec.Ledger.ConcreteCryptoTypes
+    Test.Shelley.Spec.Ledger.Example
     Test.Shelley.Spec.Ledger.Generator.Block
     Test.Shelley.Spec.Ledger.Generator.Constants
     Test.Shelley.Spec.Ledger.Generator.Core
@@ -116,6 +117,9 @@ library
     tasty,
     text,
     time,
+    mtl,
+    data-default,
+    groups,
     transformers
 
 test-suite shelley-spec-ledger-test