Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Expose event logging downstream #2405

Merged
merged 3 commits into from
Aug 3, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,8 @@ applySTSValidateSuchThat cond =
opts =
ApplySTSOpts
{ asoAssertions = AssertionsOff,
asoValidation = ValidateSuchThat cond
asoValidation = ValidateSuchThat cond,
asoEvents = EPDiscard
}

--------------------------------------------------------------------------------
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,8 @@ module Control.State.Transition.Extended
liftSTS,
tellEvent,
tellEvents,
EventReturnTypeRep,
mapEventReturn,

-- * Apply STS
AssertionPolicy (..),
Expand All @@ -60,6 +62,7 @@ module Control.State.Transition.Extended
applySTS,
applySTSIndifferently,
reapplySTS,
globalAssertionPolicy,

-- * Exported to allow running rules independently
applySTSInternal,
Expand Down Expand Up @@ -253,6 +256,15 @@ type family EventReturnType ep sts a :: Type where
EventReturnType 'EventPolicyReturn sts a = (a, [Event sts])
EventReturnType _ _ a = a

class EventReturnTypeRep ert where
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

maybe EventReturnTypeRep -> ReifyEventPolicy or something

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I went for consistency with RuleTypeRep, in the same file.

eventReturnTypeRep :: SingEP ert

instance EventReturnTypeRep 'EventPolicyReturn where
eventReturnTypeRep = EPReturn

instance EventReturnTypeRep 'EventPolicyDiscard where
eventReturnTypeRep = EPDiscard

discardEvents :: forall ep a. SingEP ep -> forall s. EventReturnType ep s a -> a
discardEvents ep = case ep of
EPReturn -> fst
Expand All @@ -263,6 +275,17 @@ getEvents ep ert = case ep of
EPReturn -> snd ert
EPDiscard -> []

-- | Map over an arbitrary 'EventReturnType'.
mapEventReturn ::
forall ep sts a b.
EventReturnTypeRep ep =>
(a -> b) ->
EventReturnType ep sts a ->
EventReturnType ep sts b
mapEventReturn f ert = case eventReturnTypeRep @ep of
EPReturn -> first f ert
EPDiscard -> f ert

data Clause sts (rtype :: RuleType) a where
Lift ::
STS sts =>
Expand Down Expand Up @@ -369,13 +392,15 @@ data ValidationPolicy
| ValidateNone
| ValidateSuchThat ([Label] -> Bool)

data ApplySTSOpts = ApplySTSOpts
data ApplySTSOpts ep = ApplySTSOpts
{ -- | Enable assertions during STS processing.
-- If this option is enabled, STS processing will terminate on violation
-- of an assertion.
asoAssertions :: AssertionPolicy,
-- | Validation policy
asoValidation :: ValidationPolicy
asoValidation :: ValidationPolicy,
-- | Event policy
asoEvents :: SingEP ep
}

type STSInterpreter ep =
Expand All @@ -396,30 +421,36 @@ type RuleInterpreter ep =
applySTSOpts ::
forall s m rtype ep.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
SingEP ep ->
ApplySTSOpts ->
ApplySTSOpts ep ->
RuleContext rtype s ->
m (EventReturnType ep s (State s, [PredicateFailure s]))
applySTSOpts ep ApplySTSOpts {asoAssertions, asoValidation} ctx =
applySTSOpts ApplySTSOpts {asoAssertions, asoValidation, asoEvents} ctx =
let goRule :: RuleInterpreter ep
goRule = applyRuleInternal ep asoValidation goSTS
goRule = applyRuleInternal asoEvents asoValidation goSTS
goSTS :: STSInterpreter ep
goSTS c =
runExceptT (applySTSInternal ep asoAssertions goRule c) >>= \case
runExceptT (applySTSInternal asoEvents asoAssertions goRule c) >>= \case
Left err -> throw $! AssertionException err
Right res -> pure $! res
in goSTS ctx

applySTSOptsEither ::
forall s m rtype.
forall s m rtype ep.
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
ApplySTSOpts ->
ApplySTSOpts ep ->
RuleContext rtype s ->
m (Either [PredicateFailure s] (State s))
m (Either [PredicateFailure s] (EventReturnType ep s (State s)))
applySTSOptsEither opts ctx =
applySTSOpts EPDiscard opts ctx <&> \case
(st, []) -> Right st
(_, pfs) -> Left pfs
let r1 = applySTSOpts opts ctx
in case asoEvents opts of
EPDiscard ->
r1 <&> \case
(st, []) -> Right st
(_, pfs) -> Left pfs
EPReturn ->
r1 <&> \case
((st, []), evts) -> Right (st, evts)
((_, pfs), _) -> Left pfs

applySTS ::
forall s m rtype.
Expand All @@ -431,15 +462,17 @@ applySTS = applySTSOptsEither defaultOpts
defaultOpts =
ApplySTSOpts
{ asoAssertions = globalAssertionPolicy,
asoValidation = ValidateAll
asoValidation = ValidateAll,
asoEvents = EPDiscard
}

globalAssertionPolicy :: AssertionPolicy

#ifdef STS_ASSERT
nc6 marked this conversation as resolved.
Show resolved Hide resolved
globalAssertionPolicy = AssertionsAll
#else
globalAssertionPolicy = AssertionsOff
#endif
globalAssertionPolicy :: AssertionPolicy

-- | Re-apply an STS.
--
Expand All @@ -451,12 +484,13 @@ reapplySTS ::
(STS s, RuleTypeRep rtype, m ~ BaseM s) =>
RuleContext rtype s ->
m (State s)
reapplySTS ctx = applySTSOpts EPDiscard defaultOpts ctx <&> fst
reapplySTS ctx = applySTSOpts defaultOpts ctx <&> fst
where
defaultOpts =
ApplySTSOpts
{ asoAssertions = AssertionsOff,
asoValidation = ValidateNone
asoValidation = ValidateNone,
asoEvents = EPDiscard
}

applySTSIndifferently ::
Expand All @@ -466,10 +500,10 @@ applySTSIndifferently ::
m (State s, [PredicateFailure s])
applySTSIndifferently =
applySTSOpts
EPDiscard
ApplySTSOpts
{ asoAssertions = AssertionsAll,
asoValidation = ValidateAll
asoValidation = ValidateAll,
asoEvents = EPDiscard
}

-- | Apply a rule even if its predicates fail.
Expand Down Expand Up @@ -519,7 +553,7 @@ applyRuleInternal ep vp goSTS jc r = do
runClause $ Writer (wrapEvent @sub @s <$> sevs) ()
pure $ next ss
runClause (Writer w a) = case ep of
EPReturn -> modify (second (\es -> es <> w)) $> a
EPReturn -> modify (second (<> w)) $> a
EPDiscard -> pure a
validateIf lbls = case vp of
ValidateAll -> True
Expand All @@ -542,7 +576,7 @@ applySTSInternal ep ap goRule ctx =
[EventReturnType ep s (State s, [PredicateFailure s])] ->
EventReturnType ep s (State s, [PredicateFailure s])
successOrFirstFailure xs =
case find (\x -> null $ snd $ (discardEvents ep @s x :: (State s, [PredicateFailure s]))) xs of
case find (\x -> null $ snd (discardEvents ep @s x :: (State s, [PredicateFailure s]))) xs of
Nothing ->
case xs of
[] -> error "applySTSInternal was called with an empty set of rules"
Expand Down Expand Up @@ -578,7 +612,7 @@ applySTSInternal ep ap goRule ctx =
when (assertPost ap) $
let res' :: (EventReturnType ep s (State s, [PredicateFailure s]))
res' = successOrFirstFailure res
in case discardEvents ep @s res' :: ((State s, [PredicateFailure s])) of
in case discardEvents ep @s res' :: (State s, [PredicateFailure s]) of
(st, []) ->
sfor_ (assertions @s) $! \case
PostCondition msg cond
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -496,5 +496,6 @@ applySTSTest = applySTSOptsEither defaultOpts
defaultOpts =
ApplySTSOpts
{ asoAssertions = AssertionsAll,
asoValidation = ValidateAll
asoValidation = ValidateAll,
asoEvents = EPDiscard
}
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,8 @@
-- API.
module Shelley.Spec.Ledger.API.Validation
( ApplyBlock (..),
applyBlock,
applyTick,
TickTransitionError (..),
BlockTransitionError (..),
chainChecks,
Expand Down Expand Up @@ -71,46 +73,58 @@ class
--
-- This handles checks and updates that happen on a slot tick, as well as a
-- few header level checks, such as size constraints.
applyTick ::
applyTickOpts ::
ApplySTSOpts ep ->
Globals ->
NewEpochState era ->
SlotNo ->
NewEpochState era
default applyTick ::
EventReturnType ep (Core.EraRule "TICK" era) (NewEpochState era)
default applyTickOpts ::
ApplySTSOpts ep ->
Globals ->
NewEpochState era ->
SlotNo ->
NewEpochState era
applyTick globals state hdr =
either err id . flip runReader globals
. applySTS @(Core.EraRule "TICK" era)
EventReturnType ep (Core.EraRule "TICK" era) (NewEpochState era)
applyTickOpts opts globals state hdr =
either err id
. flip runReader globals
. applySTSOptsEither @(Core.EraRule "TICK" era) opts
$ TRC ((), state, hdr)
where
err :: Show a => a -> b
err msg = error $ "Panic! applyTick failed: " <> show msg

-- | Apply the block level ledger transition.
applyBlock ::
MonadError (BlockTransitionError era) m =>
applyBlockOpts ::
forall ep m.
(EventReturnTypeRep ep, MonadError (BlockTransitionError era) m) =>
ApplySTSOpts ep ->
Globals ->
NewEpochState era ->
Block era ->
m (NewEpochState era)
default applyBlock ::
(MonadError (BlockTransitionError era) m) =>
m (EventReturnType ep (Core.EraRule "BBODY" era) (NewEpochState era))
default applyBlockOpts ::
forall ep m.
(EventReturnTypeRep ep, MonadError (BlockTransitionError era) m) =>
ApplySTSOpts ep ->
Globals ->
NewEpochState era ->
Block era ->
m (NewEpochState era)
applyBlock globals state blk =
m (EventReturnType ep (Core.EraRule "BBODY" era) (NewEpochState era))
applyBlockOpts opts globals state blk =
liftEither
. right (updateNewEpochState state)
. left BlockTransitionError
. right
( mapEventReturn @ep @(Core.EraRule "BBODY" era) $
updateNewEpochState state
)
$ res
where
res =
flip runReader globals . applySTS @(Core.EraRule "BBODY" era) $
TRC (mkBbodyEnv state, bbs, blk)
flip runReader globals
. applySTSOptsEither @(Core.EraRule "BBODY" era)
opts
$ TRC (mkBbodyEnv state, bbs, blk)
bbs =
STS.BbodyState
(LedgerState.esLState $ LedgerState.nesEs state)
Expand Down Expand Up @@ -142,6 +156,36 @@ class
(LedgerState.esLState $ LedgerState.nesEs state)
(LedgerState.nesBcur state)

applyTick ::
ApplyBlock era =>
Globals ->
NewEpochState era ->
SlotNo ->
NewEpochState era
applyTick =
applyTickOpts $
ApplySTSOpts
{ asoAssertions = globalAssertionPolicy,
asoValidation = ValidateAll,
asoEvents = EPDiscard
}

applyBlock ::
( ApplyBlock era,
MonadError (BlockTransitionError era) m
) =>
Globals ->
NewEpochState era ->
Block era ->
m (NewEpochState era)
applyBlock =
applyBlockOpts $
ApplySTSOpts
{ asoAssertions = globalAssertionPolicy,
asoValidation = ValidateAll,
asoEvents = EPDiscard
}

instance PraosCrypto crypto => ApplyBlock (ShelleyEra crypto)

{-------------------------------------------------------------------------------
Expand Down