Function: proRataRedeem(BasketManagerStorage self, uint256 totalSupplyBefore, uint256 burnedShares, address to)

This function allows redemption of shares when no rebalancing is in process. Shares are redeemed for each underlying asset in the basket, rather than for the initial base asset.

Inputs

• self

  • Control: Fully controlled by the calling contract.

  • Constraints: None.

  • Impact: The storage reference.

• totalSupplyBefore

  • Control: Fully controlled by the calling contract.

  • Constraints: Checked to not be zero at this level.

  • Impact: The supply of basket tokens before burning.

• burnedShares

  • Control: Fully controlled by the calling contract.

  • Constraints: Ensured that it is not zero and that it is less than totalSupplyBefore.

  • Impact: The shares that have been burned.

• to

  • Control: Fully controlled by the calling contract.

  • Constraints: Checked to not be zero at this level.

  • Impact: The address to which the redeemed assets are sent.

Branches and code coverage

Intended branches

• Assume that parameters are legitimate, as they are controlled by the calling contract.

  Test coverage

• Calculate the amount to withdraw based on the burnedShares, current basket balance, and totalSupplyBefore.

  Test coverage

• Update the basketBalanceOf mapping for each asset in the basket based on the amount that is withdrawn.

  Test coverage

• Transfer the assets to the to address.

  Test coverage

Negative behavior

• Revert if totalSupplyBefore is zero.

  Negative test

• Revert if burnedShares is zero.

  Negative test

• Revert if burnedShares is greater than totalSupplyBefore.

  Negative test

• Revert if to is the zero address.

  Negative test

• Revert if the basket is currently rebalancing.

  Negative test

• Should not transfer any assets if the amount to withdraw is zero.

  Negative test