Function redeem(uint256 tokenId, uint256 amount_) public basically(it does a function call to internal fct)

1. Intended behavior.

   • The function should enable users to redeem matured bond tokens issued by Bond Protocol for the vested underlying tokens.

   • The function should burn the corresponding amount of tokenId tokens.

   • And transfer to msg.sender the same amount of payoutToken.

2. Negative behavior.

   • Don’t redeem bonds that have not reached maturity: if (block.timestamp < meta.expiry) revert Teller_TokenNotMatured(meta.expiry);

   • Don’t redeem “counterfeit” bonds that aren’t issued by Bond Protocol: _burnToken called only for local bonds tokens

   • Do not give out too many or too few underlying tokens: it is possible to send only the amount of payoutToken that is available on the Bond balance of msg.sender balanceOf[msg.sender][tokenId] -= amount; otherwise, the transaction will be rejected on this line

   • Don’t give out the wrong payoutToken token: payoutToken address taken from tokenMetadata for corresponding tokenId. An attacker can add any address of payoutToken to the tokenMetadata, but because of the _burnToken function call, they can only redeem their tokens.

   • Don’t give or take tokens from the wrong user.

3. Preconditions.

   • The user has locked payoutToken tokens with the teller and received bond tokens in return with tokenId which connected with this payoutToken and expiry value.

   • The bonds have reached maturity.

   • Assumes that the tokenid has active metadata (it would fail otherwise anyway due to the burnToken function, there’d be an underflow there)

   • The bonds could have not been infinitely created; since the multiple bondTokens can be created for the same payoutToken this means that there might be a way to drain the contract if there is a way to craft infinitely many bondTokens!

4. Postconditions.

   • The user has now more underlying tokens.

   • The user has now less bond tokens.

   • the protocol should still have some underlying tokens left to pay the other users.

5. Inputs.

   • tokenId_: controlled,

   • amount_: controlled,

6. Examine all function calls the function makes.

   a. Call to burnToken(msg.sender, tokenId*, amount_);

   • What is controllable? (callee, params, return value): msg.sender; tokenId - directly controlled; COULD BE USER TO burn arbitrary bond tokens, however, they would have to be minted via create in the first place; amount_ - controlled

   • If return value controllable, how is it used and how can it go wrong? there is no return value

   • What happens if it reverts or tries to reenter? No problem

   b. Call to meta.payoutToken.safeTransfer(msg.sender, amount_)

   • What is controllable? (callee, params, return value): meta.payoutToken - controlled; could be used to drain arbitrary underlying tokens, however, the bondTokens issued for them would have to be burned in the first place, so no profit could really be made; msg.sender; amount_ - controlled

   • If return value controllable, how is it used and how can it go wrong? there is no return value

   • What happens if it reverts or tries to reenter? No problem