feat(RES-151): support for multiple calls of the same function

[oggy-dfin]

When the same function (e.g., ledger transfer) is called multiple times from an update method (e.g., disbursing a neuron, where we first burn the fees, and then transfer the disbursed amount), we need to allow the TLA model to distinguish in which context the function is being called. The contexts are defined through Pluscal labels. Thus:

1. we add a new annotation, tla_function, which can (and should) be used in functions called in multiple contexts within the same update method
2. we add a log_label macro to allow changing the context in the parent method
3. we adopt a convention where we stack labels by concatenating them (separated by an underscore). So if the transfer function uses the Transfer label, we can have, e.g., Burn_Fees_Transfer in the Burn_Fees context and Transfer_Disbursed_Transfer in Transfer_Disbursed context)

The PR also includes some unrelated improvements to TLA error reporting (including reporting the source locations).