Function _handlePayout(address recipient, uint256 payout_, ERC20 underlying_, uint48) internal

1. Intended behavior.

   • The function is supposed to handle the payout of payout tokens to the user. Not covered directly because it’s an internal function.

2. Negative behavior.

   • It shouldn’t transfer tokens to user if the vesting has not expired.

   • It shouldn’t allow any _underlying to be transferred.

   • It shouldn’t allow transfer on behalf of other users.

   • It shouldn’t allow transfer of untrusted tokens.

   • It shouldn’t call mint function of untrusted bondToken.

3. Preconditions.

   • That there exist enough underlying_ tokens from the market creator/owner.

   • bondToken for corresponding underlying_ token and expiry time should exist.

4. Postconditions.

   • user bondTokens[underyling][expiry] balance >= payout_+ oldBalance;

     OR

   • user underlying balance ++ and BondFixedExpiryTeller underlying balance--

5. Inputs.

   • address recipient_: controlled - the destination of minted bondToken or transferred underlying.

   • uint256 payout_: controlled - the amount of underlying or minted bondTokens

   • ERC20 underlying_ : uncontrolled

   • uint48 vesting_: uncontrolled - period in time until which the bond mature

6. Examine all function calls the function makes.

   a. Call to underyling.safeTransfer:

   • What is controllable? (callee, params, return value): everything is controllable. However, it’s an internal function, so all checks take place outside of this function

   • If the return value is 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: will be reverted if the contract doesn't have enough underlying tokens

   b. Call to bondToken.mint:

   • What is controllable? (callee, params, return value): recipient* is controllable, payout* is controllable.

   • 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: only in case totalSupply will reach the uint256 max value.