L-13: Non-Fungible Asset Replacement Is Mis-Encoded as a Pure Removal in the Account Delta

Every vault mutation records the affected asset in a link map keyed by asset ID, holding the value at the start of the transaction alongside the current value. [`update_asset`](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/account_update.masm#L785) preserves the first initial value it observes and overwrites the final value on every subsequent mutation. For an asset whose composition is none, [`compute_asset_delta`](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/account_update.masm#L845) infers the operation solely from whether the initial value is empty, and when it is not, reports a removal carrying the initial value while discarding the final one. Its documentation justifies this by stating that the final value [must be empty according to the asset vault guarantees](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/account_update.masm#L823). No such guarantee holds across two operations. Addition requires the vault leaf to be [empty](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/asset_vault.masm#L191) and removal is [all or nothing](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/asset_vault.masm#L302-L306) for such assets, so each invariant holds per operation only, and nothing rejects an entry whose initial and final values are both non-empty.

Reaching that entry requires two distinct values under one asset ID, which the kernel permits because a non-fungible asset ID binds only the first two elements of the value, as [`validate`](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/non_fungible_asset.masm#L38) documents and enforces. Since the commit loop [skips entries whose initial and final values are equal](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/account_update.masm#L515), the mis-encoding is triggered by exactly one shape: the first operation on the ID is a removal, the last is an addition, and the two values differ in their third or fourth element. Asset preservation constrains the rest of the route:

1. The native account is the issuer of asset `X` and holds it in its own vault with value `V1`.
2. Its code removes `V1` from the account vault, leaving the link map entry at `V1` and the empty word.
3. It then adds `V2`, which shares the asset ID of `V1`, leaving the entry with two non-empty values.
4. It [burns](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/faucet.masm#L64) `V1` and [mints](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/faucet.masm#L24) `V2`, which mutate the input vault so that the [asset preservation check](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/epilogue.masm#L272) still passes. Without the faucet operations the transaction traps here.
5. The transaction executes, proves and verifies. The committed delta states that `X` with value `V1` was removed, and omits the re-addition entirely.

Consider enforcing the invariant that, for an asset whose composition is none, the delta entry `(INITIAL_ASSET_VALUE, FINAL_ASSET_VALUE)` never holds two distinct non-empty values, so that it is always reducible to a single addition, a single removal, or a no-op. The preferred place to enforce it is [`update_asset`](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/account_update.masm#L785); this fails at the mutation that creates the unencodable entry and makes the assumption in `compute_asset_delta`'s documentation hold by construction. The new check must be scoped to assets whose composition is none, since for fungible assets a non-empty to non-empty transition with unequal values is exactly a partial transfer. Asserting instead inside `compute_asset_delta`'s composition-none branch is a weaker alternative: it is sufficient and nearly free, but it validates only the final entry rather than every write and reports the failure far from its cause. In either case the [documentation](https://github.com/0xMiden/protocol/blob/07ef8323cfa773e16e860311ea5b4a0c3086e3ed/crates/miden-protocol/asm/kernels/transaction-core/src/account_update.masm#L823) should be corrected to point at the new assertion rather than at an asset vault guarantee that holds per operation but not across two.

---

_Copied verbatim from finding L-13 (low) of the OpenZeppelin [tx kernel programmable assets diff audit](https://audits.openzeppelin.com/miden/miden-q3-06-tx-kernel-programable-assets-diff)._