Implement lemmas 1 & 2 from #1765

[mrBliss]

• Add assertWithMsg

• Use Except for anachronisticProtocolLedgerView

  To be consistent with the other ledger methods, e.g., applyLedgerBlock.

• Check Lemma 1 from Test ledger properties #1765

• Check Lemma 2 from Test ledger properties #1765

• Switch the order of validation in applyExtLedgerState

  Fixes Switch the order in applyExtLedgerState #1771.

[mrBliss]

Lemma 3 is harder to check, because of #1765 (comment), but also because we suddenly have ApplyTx blk and HasTxs blk constraints on applyExtLedger, which are rather annoying. Adding them as superclasses of LedgerSupportsProtocol is convenient, but annoying in ouroboros-consensus-byron, because the instances are defined in separate modules. Moreover, DualByronBlock doesn't support HasTxs, so that's a no go 🙁.

[edsko]

Nice, I like it :)

[edsko]

bors r+

[iohk-bors]

Build succeeded

• buildkite/ouroboros-network
• ci/hydra:Cardano:ouroboros-network:required