[model generation] Add `DENOM` information in metadata argument for pure functions

## Current solution: use a single `int` to encode the funds sent with the message

Currently, the metadata argument of pure functions we ask the LLM to generate looks like this:

```quint
type Metadata = {
sender: Addr,
funds: int, // TODO we probably want to increase granularity here, store denom->amount map
block_time: int,
}
```

That is, we send a single `int` (the `funds` field) to represent any tokens sent with the message. This is opposed to being able to receive multiple token `DENOM`s (such as in the `funds` field of the `MessageInfo` struct):

```quint
type MessageInfo = {
sender: str,
funds: List[Coin]
}
```

The initial reason for this design was to maintain simplicity and a "flat" arguments structure for message and blockchain metadata sent to the pure functions.

## The Problem: loss of generality

Our current solution resulted in a loss of generality for two reasons:

1. Some CosmWasm handlers / pure functions may require handling multiple `DENOM`s.
2. Some handlers/functions' behavior may depend on whether 0 tokens of a specific `DENOM` are sent, or whether no `DENOM`s are sent at all. Consequently, error handling behavior is changed by sending a single `int` instead of a richer data structure that can encode this difference.

## Proposed Solution: a `str -> int` map to encode `DENOM` information (solution #1)

We want to maintain full generality. Instead of sending a single `int`, we can change the `Metadata` struct to the following:

```quint
type Metadata = {
sender: Addr,
funds: str -> int,
block_time: int,
}
```

This solution aligns nicely with our current format for the contract state and I/O examples, e.g.:

```quint
bank: Map(
"" -> Map("d1" -> 200, "d2" -> 200),
"s1" -> Map("d1" -> 0, "d2" -> 200),
"s2" -> Map("d1" -> 100, "d2" -> 200),
"s3" -> Map("d1" -> 100, "d2" -> 200)
),
```

Maps of this kind (e.g. `Map("d1" -> 0, "d2" -> 200)`) are used to encode address balances on the blockchain and to keep contract internal balances. Now, we would also use them within the `metadata` parameter for pure functions.

* Pros: we do not increase the complexity of I/O examples significantly (as these maps are already present in them)
* Cons: we have to re-implement CW utilities such as `one_coin` and `must_pay` directly

## Alternative solution: keeping closer to CosmWasm (solution #2)

Alternatively, we can change `Metadata` to the following:

```quint
type Metadata = {
sender: Addr,
funds: List[Coin],
block_time: int,
}
```

This solution copies the `funds` field of `MessageInfo` directly.

* Pros: LLM-generated code can use CW utilities such as `one_coin` and `must_pay` directly
* Cons: I/O examples harder to specify for users and less intuitive