Remaining Shelley features/proofs

This issue itemizes features and proofs that are missing (i.e., not yet formalized and/or described in the full cardano-ledger.pdf) from the Shelley era:

- [ ] [CHAIN](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.75): incomplete (out of scope)
+ Dependencies:
- PRTCL: missing - now part of Consensus
- TICKN: missing - now part of Consensus
- TICK: partially missing (not missing anymore since #869)
- The NEWEPOCH logic is partially inlined in CHAIN (it has been moved to TICK)
- CHAIN is missing the logic of RUPD (implemented in TICK since #869)
+ [Functions](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.74):
- `chainChecks`: missing - now part of Consensus
- `prtlSeqChecks`: missing - now part of Consensus
- `adoptGenesisDelegs`: missing - deprecated

- [x] BBODY: partially missing. Done in #884
+ LEDGERS: logic is inlined
+ CHAIN is missing preconditions:
- `bBodySize txs = hBbsize bhb`
- `bbodyhash txs = bhash`
+ CHAIN is missing the logic to update the block via `incrBlocks`

- [x] [TICK](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.64): missing (5 days) Done in #869
+ Dependencies:
- RUPD: missing
- NEWEPOCH: partially inlined in CHAIN
+ [Functions](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.63):
- `adoptGenesisDelegs`: missing - deprecated

- [x] [RUPD](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.62): missing (10 days) Done in #869
+ Dependencies:
+ [Functions](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.63):
- `createRUpd`: missing (#706)
- monetary and treasury expansion parameters (#707)

- [x] [NEWEPOCH](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.57): incomplete. Done in #854
- Dependencies:
- EPOCH:
- MIR: missing - deprecated
- [Functions](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.56):
- `calculatePoolDistr`: missing - used by Consensus (10 days)

- [x] [EPOCH](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.45): incomplete. Done in #852
- Dependencies:
- SNAP:
- POOLREAP:
- Some of the POOLREAP logic (remove retired StakePools) is inlined in EPOCH
- NEWPP: missing - deprecated
- [Functions](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.44):
- `votedValue`: missing - deprecated (used by NEWPP)

- [x] [POOLREAP](https://github.com/intersectmbo/cardano-ledger/releases/latest/download/shelley-ledger.pdf#figure.41): missing (15 days) (#719) Done in #852
- Dependencies:
- Functions
- Notes: See issue [#455](https://github.com/IntersectMBO/formal-ledger-specifications/issues/455)
This is missing the logic to refund deposits

EDITED: Remove part that belongs to Consensus