[model generation] Make pure functions use `mustPay` and bank utils that mimic CosmWasm

## Current state
In Quint models (and stubs) for CW contracts, `mustPay` is called by `extract_metadata`. This function turns the `funds: List[Coin]` field of `MessageInfo` into a single `funds: int` from `Metadata`. This is done outside of the pure functions.

## The problem
As explained in [the `DENOM` issue](https://github.com/informalsystems/FuzzMo/issues/4), this results in a loss of generality.

## Proposed solution
Generated pure functions should call `mustPay` themselves. In that case, their code will look very similar to the related CosmWasm Rust code for message handlers, which also has to call `mustPay` (the Rust/CW version).