08 Working with Invariants : Property description and hint do not match

The following description regarding ReserveLists in Tutorial 8 is contradictory.

There should not be a token saved at an index greater or equal to reserve counter.

This suggests that a deletion at index i should be filled in by moving the token at the last index to ith location, thereby maintaining no token at i >= reserveCount

Hint: If index i is nonzero and token t is a valid address then t.id equals i iff the i-th reserve is t. If i is zero, i-th token is t implies t.id equals i.

This suggests that on deletion, i=0 ie t doesn’t need to be a valid address when i=0. There is no requirement on token address for i>= reserveCount to be zero

In addition, the implementation itself leaves holes in the mapping, ie for i<reserveCount, token address can be zero or non-zero, maintaining only the number of tokens. When a new token is added, the token will fill a hole so the number of non-zero token addresses in the reserveList will be more than the number of valid indices. This will create a collision on id of two different tokens.

Is this intentional? Is ReserveListFixed.sol actually fixed or should it not be assumed to be the correct contract when comparing with the buggy contracts? Some clarification on this will be great.

You are absolutely right.
The 1st property you’ve mentioned is wrong and should be edit out of the tutorial. The deletion system in this contract leaves holes, and therefore the index number of a non-zero token can exceed the number of tokens stored.

Thanks for pointing it out, we will remove it from the tutorial soon.