[ZIPs 226 and 227] The relative ordering of accesses to issuedAssets(AssetBase).balance for issuance and burning is undefined

[daira]

(This interacts with #950, but I am filing it as a separate issue because #950 is about the current protocol prior to ZSAs.)

ZIP 227 - Rationale for Global Issuance State says:

It is necessary to ensure that the balance of any issued Custom Asset never becomes negative within a shielded pool, along the lines of ZIP 209 8. However, unlike for the shielded ZEC pools, there is no individual transaction field that directly corresponds to both the issued and burnt amounts for a given Asset. Therefore, we require that all nodes maintain a record of the current amount in circulation for every issued Custom Asset, and update this record at the block boundary based on the issuance and burn transactions within the block. This allows for efficient detection of balance violations for any Asset, in which scenario we specify a consensus rule to reject the block.

Like other pools, the balance of any issued Custom Asset should never become negative at any transaction boundary; not just at block boundaries (see #950, which is only to clarify the spec: checking at transaction boundaries is how it is implemented). So this should say:

[...] Therefore, we require that validators maintain a record of the current amount in circulation for every issued Custom Asset, and update this record at each transaction boundary based on the issuance and burn transactions within the block. Within a transaction, issuance is considered to take place before burning for this purpose. This allows for efficient detection of balance violations for any Asset, in which scenario we specify a consensus rule to reject the block.

Note that this is in a Rationale section and therefore non-normative. The actual specification is split between ZIPs 227 (for issuance) and 226 (for burning).

For issuance, the proposed changes are in ZIP 227 - Specification: Consensus Rule Changes:

If all of the above checks pass, do the following:

For each note,

• [...]
• Increase the value of $\mathsf{issuedAssets}(\mathsf{AssetBase})\mathsf{.balance}$ by the value of the note, $v$.

The proposed consensus rule for burning of Custom Assets is rule 4 in ZIP 226 - Burn Mechanism - Additional Consensus Rules:

1. Check that for every $(\mathsf{AssetBase}, \mathsf{v}) \in \mathsf{assetBurn}$, $\mathsf{AssetBase} \neq \mathcal{V}^{\mathsf{Orchard}}$. That is, ZEC or TAZ is not allowed to be burnt by this mechanism.
2. Check that for every $(\mathsf{AssetBase}, \mathsf{v}) \in \mathsf{assetBurn}$, $\mathsf{v} \neq 0$.
3. Check that there is no duplication of Custom Assets in the $\mathsf{assetBurn}$ set. That is, every $\mathsf{AssetBase}$ has at most one entry in $\mathsf{assetBurn}$.
4. Check that for every $(\mathsf{AssetBase}, \mathsf{v}) \in \mathsf{assetBurn}$, $\mathsf{v} \leq \mathsf{issuedAssets}(\mathsf{AssetBase})\mathsf{.balance}$, where the map $\mathsf{issuedAssets}$ is defined in ZIP 227. That is, it is not possible to burn more of an Asset than is currently in circulation.

If all these checks pass, then for every $(\mathsf{AssetBase}, \mathsf{v}) \in \mathsf{assetBurn}$, reduce the value of $\mathsf{issuedAssets}(\mathsf{AssetBase})\mathsf{.balance}$ in the global state by $v$.

The relative ordering of accesses to the global state is not defined. It must be, because checking $\mathsf{v} \leq \mathsf{issuedAssets}(\mathsf{AssetBase})\mathsf{.balance}$ might give different results depending on whether it is done before or after the state update for issuance. (IMHO it makes more sense either to do issuance first, or to prohibit issuing and burning the same asset in a transaction.)

This is a consequence of the use of imperative statements like "reduce the value" or "increase the value". I don't want to claim these are strictly never used in existing consensus rules, but it is undesirable to use them because of ambiguities like that above. It is far preferable to refer explicitly to indexed states, i.e. to define notation for the global state before and after the transaction. Then a consensus rule that performs an "update" can be rephrased as imposing a relation between the before-state and after-state, which resolves a lot of potential ambiguities (in particular, conflicting requirements automatically do the right thing which is to reject the transaction).