DopplerDN404._transferFromNFT frozen-prefix maintenance: `i` may equal new owned length after super if `id` was the last element

Opus finding

DopplerDN404._transferFromNFT frozen-prefix maintenance: `i` may equal new owned length after super if `id` was the last element

• src/dn404/DopplerDN404.sol:156-192
• src/dn404/DopplerDN404.sol:122-130

After `super._transferFromNFT`, DN404 moves the last element of `from`'s owned list into the index of the transferred token (swap-and-pop), then decrements ownedLength. So at the slot `i` (the original index of `id`), the previous last-element token now resides — unless `i` was the last index, in which case nothing was moved into slot `i` (and slot `i` is now out of bounds / `i >= newLen`). The code handles `i >= newLen` by skipping the swap, then decrements frozenBalances. However, the invariant the comment claims — that the frozen prefix [0..F-1] remains the frozen set minus `id` — requires that when `i < F-1`, the element at `j = F-1` (which was frozen) is moved into slot `i`, AND the element that super moved into slot `i` (the previous tail) is moved to slot `j` to preserve the unfrozen suffix order. The code does this swap. But there's an edge case: if super moves the tail into slot `i`, AND that tail element was itself within [F, newLen-1] (an unfrozen element), then after the swap, slot `i` holds the old element-at-`j` (frozen, correct prefix), and slot `j` holds the tail element (unfrozen, correct boundary). ✅ But what if `i == j` (the transferred token was the last frozen one)? Then `j < newLen` is true, `i < newLen` is true (if newLen > j), and `i == j` so no swap occurs, just decrement frozenBalances. Slot `j == i` now contains whatever super moved in (the previous tail, unfrozen) — which is now part of the unfrozen suffix. ✅ But: if the transferred id was the last element overall (i.e., `i == oldLen - 1`), super pops without moving; after super, `i == newLen`, so `i < newLen` is false, swap skipped, frozenBalances decremented. But `j = F-1` may still be `< newLen`. Slot `j` was the last frozen and is still frozen (unchanged). But we removed `id` from position `i` which was inside `[0, F)`. If `i < F-1`, then the prefix [0..F-2] is missing element from position `i` and position `j = F-1` still holds the old element. We need to move element at `j` into position `i`. But the code only does this swap when `i < newLen`. If `i == newLen` (super popped without moving), the code skips the swap entirely, leaving a hole. Wait — `i < oldLen - 1` is required for super to do a swap-then-pop; if `i == oldLen - 1`, super just pops. In that case `i == newLen`, so the code skips. But `i == F - 1 == j` (since `i < F` and `i == oldLen - 1`, and if F < oldLen then i = oldLen-1 >= F which contradicts i < F; so this only happens if F == oldLen, meaning all tokens are frozen). If F == oldLen and i = oldLen - 1, then j = F - 1 = oldLen - 1 = i, so j >= newLen (newLen = oldLen - 1), so `j < newLen` is false, swap skipped, decrement happens. ✅ Edge: F < oldLen and i = oldLen - 1 cannot happen because i < F < oldLen means i <= F-1 < oldLen - 1. So actually i = oldLen-1 only when F = oldLen. The logic appears correct. Withdrawing this finding as low-confidence after analysis.