Test ledger properties

[mrBliss]

We expect the following properties to hold for each ledger. Formulate them abstractly (for blk) and test them for each ledger, in particular the Byron ledger.

• Lemma 1:

  for all s >= ledgerTipSlot st,
       anachronisticProtocolLedgerView cfg st s 
    == protocolLedgerView (applyChainTick cfg s st)
  

• Lemma 2:

       protocolLedgerView (applyLedgerBlock cfg blk state)
    == protocolLedgerView (applyChainTick cfg (blockSlot blk) state)
  

• Lemma 3:

      applyLedgerBlock cfg blk st
   == repeatedlyM (applyTx cfg) (extractTxs blk)
                  (applyChainTick cfg (blockSlot blk) st)
  

[edsko]

Lemma (3) isn't quite true. For example, in Byron, endorsements come from the protocol version in the header, and aren't an explicit transaction. Perhaps we could generalize the lemma somewhat.

[mrBliss]

We moved lemma 3 to IntersectMBO/ouroboros-consensus#699. The other two are checked by #1775.