Zellic - Audit Reports

Redemption often underpays user by one base unit

We do not consider this issue to have any impact because of how insignificant the underpayment is. However, we decided to document this behavior for the extremely unlikely scenario where this contract is configured with an asset that has few decimals and for the sake of completeness.

When determining whether the code rounds in the correct direction, we observed an interesting behavior: when redeeming, the contract often underpays what is due to the user by one base unit. The root cause is the fact that the fee is calculated (and rounded up) twice.

For the remainder of this section, we will use the following variables:

Let $n$ be the number of shares to redeem.
Let $x$ be $n$ converted to assets at the time requestRedeem is called.
Let $m$ be the amount it transfers to the user.
Let $o$ be the amount it transfers to the fee receiver.

The following invariant should exist to ensure that there is no underpayment or overpayment: the amount owed to the user, added to the amount owed to the fee receiver, must equal the shares passed in converted to assets in redeem.

That is, we want to test the invariant that $m + o = x$ .

Converting the logic of the code,

in requestRedeem

$x = x = sharesToAssets (n)$

atomically in redeem,

$m = x - ceil (x \times \frac{fee}{fee + bps})$ $o = ceil (m \times \frac{fee}{bps})$

Verifying the invariant without rounding

Ignoring ceil for now,

m m = x - (x \times \frac{fee}{fee + bps}) = x \times \frac{bps}{fee + bps}

and substituting m into o,

o o o = m \times \frac{fee}{bps} = x \times \frac{bps}{fee + bps} \times \frac{fee}{bps} = x \times \frac{fee}{fee + bps}

we now have this:

m = x \times \frac{bps}{fee + bps} o = x \times \frac{fee}{fee + bps}

Checking the invariant,

m + o \frac{bps}{fee + bps} + \frac{fee}{fee + bps} 1 = x = 1 = 1

the invariant holds without rounding.

Testing the invariant with rounding

The following counterexample shows the invariant does not hold when considering rounding:

The invariant does not hold when rounding is considered. The user would be underpaid by one base unit.

Visualizing when the bug is triggered

We graphed the behavior on Desmos.com here↗ to visualize which parameters trigger the bug. In the graph at the link, we use 20% fees. The x-axis represents the number of assets the user wants to redeem ( $x$ ), and the y-axis represents the overpayment or underpayment.

Overpayments will never occur — only underpayments by exactly one base unit.

Underpayment by one base unit occurs only if the assets are a multiple of the BPS divided by the fee, or

x (mod \frac{bps}{fee}) = 0

The bug is more likely to be triggered as the fee increases.