Upgrade the high level Balance module spec in Polkadot Verification repo

[drskalman]

Many functions has changed name and parameters has been changed and so the high level spec of the module in K also deserve to be upgraded, least it gives an opportunity for us to practicing specing runtime in K.

[drskalman]

@FlorianFranzen will update the issue with current existential problem with calling out to other paletts.

[FlorianFranzen]

So far we only used the node template runtime for the analysis, which seems to inline or not contain a lot of the balance pallet functions. This however does not seem to be a problem when using the latest Polkadot runtime (v19), so the decision for now was to just use the correct runtime right away. So more technical details can be found in the meeting log.
We are on a break for two weeks now, but I will get back to writing some more k specs in the two weeks to come.