[FEAT] - Generalize how the HFC handles era transitions

[nfrisby]

Background

Today's hard fork combinator design handles transitions from one era to the next (eg Byron to Shelley, Alonzo to Babbage, etc) in a way that has so-far supported the needs of Cardano.

However, Issue #339 results from the current HFC design clashing with the current Conway design. (To be clear: the Conway design is not at fault, in my opinion.)

As part of our work on Issue 339, we've also been considering which assumptions of today's HFC design need to change. EG The draft PR #340 changes Edsko's original translate*-then-tick scheme (which made plenty of sense for Byron-to-Shelley!) to a new (tick-then-translate)*-then-tick scheme. We think the latter better matches the very reasonable intuition that the current (😞) Ledger and Consensus team members have about "when" era-to-era translations happen. However, we've finally also realized that this new scheme is still very specific to Cardano.

In these discussions around Issue 339, @dnadales early on suggested that the HFC should make even less assumptions. I've come around to that agree with him: the HFC should be as reasonably-general as possible---even beyond Cardano---and we should include helper combinators (eg (tick-then-translate)*-then-tick) for instantiating it conveniently for the Cardano use case.

Task

This Issue is to propose a new generalized interface about how the HFC handles era transitions. We don't necessarily need to implement it, but at least having "the general interface" semi-formalized will help us navigate these kinds of questions, both Issue 339 now and similar issues in the future.

Also, we should discuss that "idealized" interface with at least the Ledger Team, since they ultimately own any design decisions that are required in order to implement each concrete era transition.

[nfrisby]

The observation I'd like to start with is that only three behaviors of HardForkBlock as a block actually implement the era transitions: ticking ledger states, ticking chain-dependent-states (aka "the header-only ledger states"), and forecasting. In hindsight, this is obvious, since those are the three functions that involve advancing from a state in a slot in one era to something in a later slot, which therefore might be in the next era.

The directly corresponding methods of the Consensus type classes are applyChainTickLedgerResult (or its nub applyChainTick), tickChainDepState, and ledgerViewForecastAt. Those implementations for HardForkBlock have some important logic of their own and also invoke a secondary HFC-specific interface of singleEraTransition, crossEraForecast, translateChainDepState, and translateLedgerState. (TODO hardForkInjectTxs as well).

In particular, the Consensus flow (at least for Cardano) uses these functions as in the following rough timeline.

• A ledger state near the end of an era will be used to validate a header in the next era. This happens by creating a ledger view in the next era via crossEraForecast---which ledgerViewForecastAt ultimately knows to invoke only because of the output of singleEraTransition---passing its result to tickChainDepState to advance a ChainDepState that resulted from a header in the current era to the new header's slot to the next era, which must involve translateChainDepState. That new ChainDepState can then be used to validate the header.
• At least one node must forge the first block of the next era; this process also begins by constructing the ticked ChainDepState in the slot of the next era (ie the wall clock's slot).
• Once the header has been validated, its block will be downloaded, and hopefully worth validating, which requires advancing the ledger state of the last block of the current era into the slot of the first block of the next era, which must involve translateLedgerState.

Summary: the forecasted LedgerView is the first data to be locally constructed in the new era. Then the ChainDepState. Then the LedgerState.

Aside: the ticked ChainDepStates often carry along the LedgerView used to create them (which the Ticked data family allows), so that the subsequent functions (leadership check and header validation) can also access their data. In fact, for single-era protocols (PBft, TPraos, Praos), tickChainDepState doesn't do anything with the LedgerView other than pass it through. On the other hand, the tickChainDepState of the HFC does scrutinize the LedgerView to detect that an era transition is even necessary to create the resulting ticked ChainDepState.

[nfrisby]

My initial observation for the starting point here is that the HFC's LedgerView must carry whatever information in the forecasting ledger state X is required to tick a ChainDepState that is either at X or already ahead of it (possibly in a later era!) to the slot of the forecasted LedgerView.

In the Cardano use case, no era is empty (I'm willfully ignoring degenerate uses of TriggerHardForkAtEpoch). And so that intermediate ChainDepState has always either been in the same era as X or in its successor. Moreover, so far, the LedgerView of an era has essentially sufficed for that single era transition.

---

However, perhaps some non-Cardano chain would be able to forecast across multiple era transitions. And/or it might need some additional information from the root ledger state in order to make that translation (eg extraEntropy in TPraos or the fully-determined protocol major version update in Babbage -> Conway).

That line of thought leads me to the following generalization of the above functions.

{-
When forecasting from x to z, there are usually-but-not-necessarily blocks in between the ledger state and the future slot.
Those blocks might be in any era from x to z.
And so a cross-era forecast x to z isn't necessarily followed by a cross-era tick from x to z.
The subsequent tick does have to end in z (because of the contract on forecasting and 'tickChainDepState'), but it could start from any era from x to z.
It'll be from the predecessor of z, unless that era has no blocks in it, and so on, possibly back to x (which has at least one block in it, since we're forecasting from an unticked ledger state---I suppose this is perhaps even the genesis block in the extreme case).
-}

-- | Information necessary to tick a 'ChainDepState' after a header in @fromEra@ to a slot in @toEra@
--
-- This information is forecasted from a 'LedgerState' that is in an era possibly in an even earlier than @fromEra@.
-- An invariant on 'ledgerViewForecastAt' ensures that that 'LedgerState' cannot be in a later era than @fromEra@.
type family ChainDepTranslationContext (fromEra :: k) (toEra :: k) :: Type

-- provides x and z like Tails, but also provides every intermediate era as ys (or something isomorphic to that x ys z triple)
data Tails2 ...

-- each era between x and z has no blocks
crossEraForecast :: Tails2 (
  LedgerState x -> SlotNo -> Except PastHorizonException (NP (WrapFlipChainDepTranslationContext z) (x : ys), Ticked (LedgerView z))
  ) xs

-- each era between x and z has no blocks
crossEraTickChainDepState :: Tails (
  ChainDepState x -> SlotNo -> ChainDepTranslationContext x z -> Ticked (LedgerView z) -> Ticked (ChainDepState z)
  ) xs

-- each era between x and z has no blocks
crossEraTickLedgerState :: Tails (
  LedgerState x -> SlotNo -> Ticked (LedgerState z)
  ) xs

On Cardano, note that no Ticked (LedgerView z) could exist that spans multiple era transitions. Thus crossEraTickChainDepState would throw PastHorizon whenever such a thing was requested. We would likely define a helper combinator to simplify the instantiation of this interface for such chains.

[nfrisby]

Moved to Ready since we're checkpointing this work for now via Issue #420.