Prove properties of UTxOHistory

[HeinrichApfelmus]

The formal specification of the Deposit Wallet describes the behavior of operations on the WalletState. Compiler-checked proofs in Agda ensure that the implementation matches the specification.

One key aspect of the WalletState is to keep track of the current funds available for spending, represented in terms of unspent transaction outputs (UTxO). These UTxO must be updated when a new block is added to the chain, but the UTxO must also be reverted when the chain is rolled back to an earlier state.

The data type UTxOHistory keeps track of the wallet UTxO in a way that supports both rollBackward and rollBackward. This task is about:

• Specifying relevant properties of the operations on UTxOHistory.
• Implementing UTxOHistory.
• Proving that the implementation of UTxOHistory matches the specification.