Polish Specification

[HeinrichApfelmus]

The formal specification of the Deposit Wallet describes the behavior of operations on the WalletState. Eventually, we want compiler-checked proofs in Agda that show that the implementation matches the specification.

This task is about polishing the Specification to the point where it can be published.

This task includes:

• Modularize the specification, moving Cardano concepts that we depend on, such as Tx or Slot, to their own sub-specifications.

• Updating the specification to
  • remove the createAddress function and rely on the WalletIdentity concept instead.
  • be sound and complete in the aspects relating to focus of the Deposit Wallet, here the usage Address
    • Update discussion of TxHistory
    • Update discussion of createPayment