Balance of fee flow controller of a bought asset is always 0 after buy
Balance of asset receiver is incremented by balance of fee flow controller after buy
Balance of buyer is reduced by payment amount, and never by more than max payment amount
Balance of payment receiver is increased by payment amount
Payment amount returned on buy is never higher than maximum payout
Epoch Id is always incremented by 1 after buy (and becomes 0 if it reaches max uint16)
NOTE:
Most of the balance check rules had to have the following assumptions in order to pass:
require(assetsReceiver != feeFlowController); // make sure the receiver is not feeFlowController
require(assets[0] != getPaymentToken()); // make sure the asset is not the payment token
require(getPaymentReceiver() != e.msg.sender); // make sure the payment receiver is not the buyer
Also the tests are done with optimistic dispatches of standard ERC20 tokens. With weird tokens with fee on transfer tokens, the rules might break
The github actions are set to run on every push. I wanted to set them on pull_request sync but there is a weird issue that setup the github submodules are not fetched and the actions can't find the remote repos.
added the rules suggested:
NOTE: Most of the balance check rules had to have the following assumptions in order to pass:
Also the tests are done with optimistic dispatches of standard ERC20 tokens. With weird tokens with fee on transfer tokens, the rules might break
The github actions are set to run on every push. I wanted to set them on
pull_request
sync but there is a weird issue that setup the github submodules are not fetched and the actions can't find the remote repos.