| ID | NAME | PROPERTY DEFINITION |
|---|---|---|
| ERC20-STDPROP-01 | prove_transfer | transfer succeeds if receiver is not the zero address, the amount on sender is enough and doesn't overflow receiver's balance |
| ERC20-STDPROP-02 | prove_transferToSelf | self-transfers succeeds if amount does not exceeds sender's balance |
| ERC20-STDPROP-03 | prove_transferCorrectAmount | non-self succesful transfer calls should correctly handle the amount on sender and receiver |
| ERC20-STDPROP-04 | prove_transferSelfCorrectAmount | self-transfer calls should not break accounting |
| ERC20-STDPROP-05 | prove_transferChangeState | transfer should not have any unexpected state changes on non-revert calls |
| ERC20-STDPROP-06 | prove_transferZeroAmount | successful zero amount transfer calls should not break accounting |
| ERC20-STDPROP-07 | prove_transferToZeroAddressReverts | any transfer call to the zero address should fail and revert. |
| ERC20-STDPROP-08 | prove_transferNotEnoughBalanceReverts | transfer should fail and revert if account balance is lowers than total amount trying to be sent |
| ERC20-STDPROP-09 | prove_transferOverflowReceiverReverts | transfer should prevent overflow on receiver and revert |
| ERC20-STDPROP-10 | prove_transferNeverReturnsFalse | transfer should not return false on failure, it should revert instead |
| ERC20-STDPROP-11 | prove_transferSuccessReturnsTrue | transfer calls returns true to indicate it succeeded |
| ID | NAME | PROPERTY DEFINITION |
|---|---|---|
| ERC20-STDPROP-12 | prove_transferFrom | transferFrom calls should update accounting accordingly when succeeding |
| ERC20-STDPROP-13 | prove_transferFromToSelf | a call where from and to address are the same on transferFrom should not break accounting |
| ERC20-STDPROP-14 | prove_transferFromCorrectAmount | non-self transferFrom calls sends the correct amount |
| ERC20-STDPROP-15 | prove_transferFromToSelfCorrectAmount | self transferFrom calls send the correct amount (meaning balance won't change) |
| ERC20-STDPROP-16 | prove_transferFromChangeState | transferFrom should not have any unexpected state changes on non-revert calls |
| ERC20-STDPROP-17 | prove_transferFromZeroAmount | zero amount transferFrom calls should not break accounting |
| ERC20-STDPROP-18 | prove_transferFromCorrectAllowance | non-reverting transferFrom calls updates allowance correctly |
| ERC20-STDPROP-19 | prove_transferFromToZeroAddressReverts | all transferFrom calls to zero address should revert |
| ERC20-STDPROP-20 | prove_transferFromNotEnoughBalanceReverts | all transferFrom calls where amount is higher than the available balance should revert |
| ERC20-STDPROP-21 | prove_transferFromNotEnoughAllowanceReverts | all transferFrom calls where amount is higher than the allowance available should revert |
| ERC20-STDPROP-22 | prove_transferFromOverflowReceiverReverts | transferFrom should prevent overflow on the receiver |
| ERC20-STDPROP-23 | prove_transferFromNeverReturnsFalse | transferFrom should not return false on failure, it should revert instead |
| ERC20-STDPROP-24 | prove_transferFromSuccessReturnsTrue | transferFrom calls returns true to indicate it succeeded |
| ID | NAME | PROPERTY DEFINITION |
|---|---|---|
| ERC20-STDPROP-25 | prove_approve | approve should succeed if the spender is not the zero address and amount approved is higher than 0 |
| ERC20-STDPROP-26 | prove_approveCorrectAmount | non-reverting approve calls should update allowance correctly |
| ERC20-STDPROP-27 | prove_approveCorrectAmountTwice | any number of non-reverting approve calls should update allowance correctly |
| ERC20-STDPROP-28 | prove_approveDoesNotChangeState | any non-reverting approve call should not change the state of other variables |
| ERC20-STDPROP-29 | prove_approveRevertZeroAddress | any call to approve where spender is the zero address should revert |
| ERC20-STDPROP-30 | prove_approveNeverReturnFalse | approve should not return false to indicate that it failed |
| ERC20-STDPROP-31 | prove_approveSuccessReturnsTrue | approve should return true to indicate it succeeded |