-
Notifications
You must be signed in to change notification settings - Fork 22
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
Tame TransitionImpossible et al #364
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
A couple quick TODOs
oneForecast sno pairs (Current start AnnForecast{..}) = | ||
case annForecastEnd of | ||
oneForecast sno staticTransitions crosses (Current start AnnForecast{..}) = | ||
(\k -> maybe (neverEnd <$> forecastFor annForecast sno) k annForecastEnd) $ \case |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Accept the additional index indent for the unchanged lines instead of golfing.
@@ -583,7 +624,8 @@ inspectHardForkLedger = go | |||
map liftEvent $ | |||
inspectLedger c (currentState before) (currentState after) | |||
|
|||
, case (pss, confirmedBefore, confirmedAfter) of | |||
-- TODO assert currentStart before == currentStart after? | |||
, (\k -> case singleEraTransition' pc ps (currentStart before) of FixedTransition{} -> []; EventualTransition f -> k f) $ \f -> case (pss, f (currentState before), f (currentState after)) of |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Accept the additional index indent for the unchanged lines instead of golfing.
aa7f61c
to
ebbeff8
Compare
This commit renames TransitionImpossible to TransitionNever for two reasons. First, this is a more precise name. Second, this commit refines the singleEraTransition method so that TransitionNever is actually an absorbing state. Before this commit, TransitionImpossible could arise under certain circumstances but then the TransitionInfo for _the same era_ could later become TransitionUnknown. But now it is invariant that once the TransitionInfo for an era is ever TransitionNever then it always will be and moreover that era will indeed never end. This invariant is enforced in two ways. singleEraTransition can now induce TransitionNever, but only when that decision is independent of the ledger state, ie it must be a function only of inputs that the HFC does not vary (ledger config, EraParams, start of the era). The only other place TransitionNever arises is in the Unary.Isomorphism class, and it now has a law requiring that singleEraTransition only induce TransitionNever.
ebbeff8
to
007e239
Compare
TriggerHardForkNever -> Nothing | ||
TriggerHardForkAtEpoch epoch -> Just epoch | ||
TriggerHardForkAtVersion shelleyMajorVersion -> | ||
TriggerHardForkNever -> FixedTransition Nothing |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Bah! This line would reintroduce the bug fixed by IntersectMBO/ouroboros-network#3754
For example, I think TriggerHardForkNever
should be renamed to TriggerHardForkCannotBeKnown
. Either that, or protocolInfoCardano
should use TriggerHardForkAtVersion
(maxBound
?) even for the last era. 🤔
Single commit PR; see the message.