Specify cross-era ticking/forecasting for Cardano

[nfrisby]

The Consensus Team needs assistance with Issue IntersectMBO/ouroboros-consensus#418.

Right now, there is no separate specification for how to tick/forecast ledger states across era boundaries, there is only code. Other than Byron-to-Shelley, it's "obvious for the most part". But there are plenty of subtleties buried in the implementation.

This Issue is to create a proper specification of the relation that must hold between two ledger states X and Tick(X, S) --- X is the ledger state that results from applying the final block of some era, and S is the slot of the first block of the next era, which will be validated against the Tick(X, S) ledger state.

[nfrisby]

For the record, translating txs etc from one era to the next also deserves a specification. But it's less error-prone, in our experience.

[amesgen]

But there are plenty of subtleties buried in the implementation.

One such subtlety is on ticking from Babbage to Conway:

• The Babbage->Conway hack (Minimal workaround for updating protocol params on Babbage→Conway ouroboros-consensus#366) became unnecessary once @lehins changed how ticking applies updates to protocol params (see the corresponding ADR for an explanation).
• However, we didn't revert it before the Conway HF, as that didn't seem strictly necessary. (Probably should have done that immediately, I even tested that it works fine...)
• However, there actually is a small semantic difference between them: Due to the hack, when ticking across the era/epoch boundary using the Conway logic, the ticking logic thinks that the current protocol version is 9 (instead of 8 without the hack). Therefore, it already un-delegates stake from pointer addresses, which would otherwise (without the hack) only have happened at the next epoch boundary.
• Therefore, in order to make sure that there are no disagreements regarding the stake distribution, we need to preserve the current behavior. The most direct way would be to keep the current hack, but we don't have to: I opened Minimally re-implement additional logic on Babbage->Conway ledger state translation ouroboros-consensus#1239 that re-implements the hack in a minimal fashion. It could be made even more minimal/finegrained by upstreaming the logic into Ledger.
• The actual effect on mainnet is pretty minimal: The pool abacadaba9f12a8b5382fc370e4e7e69421fb59831bb4ecca3a11d9b lost 100 ADA worth of delegation in epoch 508 instead of in epoch 509 due to the retirement of pointer addresses.

[amesgen]

This Issue is to create a proper specification of the relation that must hold between two ledger states X and Tick(X, S) --- X is the ledger state that results from applying the final block of some era, and S is the slot of the first block of the next era, which will be validated against the Tick(X, S) ledger state.

We also need sth similar for forecasting. E.g. one weird thing at the moment is that forecasting and ticking work differently/symmetrically:

• Ticking from era A to era B works by first translating the ledger state from A to B, and then ticking across the era/epoch boundary using the logic from era B.
• Forecasting from era A to era B works by first forecasting from the ledger state in A to a ledger view from A (but for a slot in B), and then translating the ledger view from A to B.

Consensus requires that these things agree as long as forecasting is defined (the "forecasting lemma", see e.g. here), which isn't actually immediately obvious here.