Function create(ERC20 underlying_, uint48 expiry_, uint256 amount)

1. Intended behavior.

   • This function is supposed to mint the bondToken pair of underlying, expiry to the sender, drawing underlying from the sender.

2. Negative behavior.

   • Disallow mint bond tokens with a expiry that’s in the past. (or != 0)

   • Shouldn’t leave the user with too little bondTokens minted (maybe add some slippage check)

   • Shouldn’t allow infinite minting of the bondToken, since it could theoretically have the same underlying as other tokens.

3. Preconditions.

   • That a bond token already exists for the (underlying, expiry_) pair.

   • That the user has enough balance of underlying_ to deposit.

4. Postconditions.

   • underlying_.balanceOf(address(BondFixedExpiryTeller)) ≥ oldBalance+amount

   • bondToken.balanceOf(msg.sender) ≥ oldBalance + (amount_ - fee)

   • if (protocolFee > createFeeDiscount) fee value should be assigned to the protocol owner

5. Inputs.

   • ERC20 underlying*: controllable - it’s the underlying that’s about to be sent to the contract (forming the (underlying, expiry*) pair. checked that a pair with it and the expiry exists

   • uint48 expiry_: controllable - it’s part of the pair

   • uint256 amount_: controllable - it first needs to send the particular underlying from the user and then based on that it mints the bond tokens; apparently no need to check it

6. Examine all function calls the function makes.

   a. Call to underlying_.balanceOf

   • What is controllable? (callee, params, return value): address(this) - uncontrolled by the user, the return value is controllable.

   • If return value controllable, how is it used and how can it go wrong: the user can transfer tokens directly to this address and increase the balance, but there is no bad impact.

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

   b. Call to underyling_.transferFrom(msg.sender, address(this), amount_)

   • What is controllable? (callee, params, return value): amount and underlying are controllable(internal function!)

   • 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: will be reverted if msg.sender doesn’t have enough underyling_ tokens.

   c. Call to bondToken.mint(msg.sender, amount_)

   • What is controllable? (callee, params, return value): amount_ is controllable, but that’s after the transferFrom happens, so it’s safe.

   • 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: No problem