Skip to content

Latest commit

 

History

History
262 lines (236 loc) · 53.1 KB

PROPERTIES.md

File metadata and controls

262 lines (236 loc) · 53.1 KB
Raw

Introduction

This file lists all the currently implemented Echidna property tests for ERC20, ERC721, ERC4626 and ABDKMath64x64. For each property, there is a permalink to the file implementing it in the repository and a small description of the invariant tested.

Table of contents

ERC20

Basic properties for standard functions

ID Name Invariant tested
ERC20-BASE-001 test_ERC20_constantSupply Total supply should be constant for non-mintable and non-burnable tokens.
ERC20-BASE-002 test_ERC20_userBalanceNotHigherThanSupply No user balance should be greater than the token's total supply.
ERC20-BASE-003 test_ERC20_usersBalancesNotHigherThanSupply The sum of users balances should not be greater than the token's total supply.
ERC20-BASE-004 test_ERC20_zeroAddressBalance Token balance for address zero should be zero.
ERC20-BASE-005 test_ERC20_transferToZeroAddress transfers to zero address should not be allowed.
ERC20-BASE-006 test_ERC20_transferFromToZeroAddress transferFroms to zero address should not be allowed.
ERC20-BASE-007 test_ERC20_selfTransfer Self transfers should not break accounting.
ERC20-BASE-008 test_ERC20_selfTransferFrom Self transferFroms should not break accounting.
ERC20-BASE-009 test_ERC20_transferMoreThanBalance transfers for more than account balance should not be allowed.
ERC20-BASE-010 test_ERC20_transferFromMoreThanBalance transferFroms for more than account balance should not be allowed.
ERC20-BASE-011 test_ERC20_transferZeroAmount transfers for zero amount should not break accounting.
ERC20-BASE-012 test_ERC20_transferFromZeroAmount transferFroms for zero amount should not break accounting.
ERC20-BASE-013 test_ERC20_transfer Valid transfers should update accounting correctly.
ERC20-BASE-014 test_ERC20_transferFrom Valid transferFroms should update accounting correctly.
ERC20-BASE-015 test_ERC20_setAllowance Allowances should be set correctly when approve is called.
ERC20-BASE-016 test_ERC20_setAllowanceTwice Allowances should be updated correctly when approve is called twice.
ERC20-BASE-017 test_ERC20_spendAllowanceAfterTransfer After transferFrom, allowances should be updated correctly.

Tests for burnable tokens

ID Name Invariant tested
ERC20-BURNABLE-001 test_ERC20_burn User balance and total supply should be updated correctly when burn is called.
ERC20-BURNABLE-002 test_ERC20_burnFrom User balance and total supply should be updated correctly when burnFrom is called.
ERC20-BURNABLE-003 test_ERC20_burnFromUpdateAllowance Allowances should be updated correctly when burnFrom is called.

Tests for mintable tokens

ID Name Invariant tested
ERC20-MINTABLE-001 test_ERC20_mintTokens User balance and total supply should be updated correctly after minting.

Tests for pausable tokens

ID Name Invariant tested
ERC20-PAUSABLE-001 test_ERC20_pausedTransfer Token transfers should not be possible when paused state is enabled.
ERC20-PAUSABLE-002 test_ERC20_pausedTransferFrom Token transferFroms should not be possible when paused state is enabled.

Tests for tokens implementing increaseAllowance and decreaseAllowance

ID Name Invariant tested
ERC20-ALLOWANCE-001 test_ERC20_setAndIncreaseAllowance Allowance should be updated correctly when increaseAllowance is called.
ERC20-ALLOWANCE-002 test_ERC20_setAndDecreaseAllowance Allowance should be updated correctly when decreaseAllowance is called.

ERC721

Basic properties for standard functions

ID Name Invariant tested
ERC721-BASE-001 test_ERC721_balanceOfZeroAddressMustRevert Calling balanceOf for the zero address should revert.
ERC721-BASE-002 test_ERC721_ownerOfInvalidTokenMustRevert Calling ownerOf for an invalid token should revert.
ERC721-BASE-003 test_ERC721_approvingInvalidTokenMustRevert approve() should revert on invalid token.
ERC721-BASE-004 test_ERC721_transferFromNotApproved transferFrom() should revert if caller is not operator.
ERC721-BASE-005 test_ERC721_transferFromResetApproval transferFrom() should reset approvals.
ERC721-BASE-006 test_ERC721_transferFromUpdatesOwner transferFrom() should update the token owner.
ERC721-BASE-007 test_ERC721_transferFromZeroAddress transferFrom() should revert if from is the zero address.
ERC721-BASE-008 test_ERC721_transferToZeroAddress transferFrom() should revert if to is the zero address.
ERC721-BASE-009 test_ERC721_transferFromSelf transferFrom() to self should not break accounting.
ERC721-BASE-010 test_ERC721_transferFromSelfResetsApproval transferFrom() to self should reset approvals.
ERC721-BASE-011 test_ERC721_safeTransferFromRevertsOnNoncontractReceiver safeTransferFrom() should revert if receiver is a contract that does not implement onERC721Received()

Tests for burnable tokens

ID Name Invariant tested
ERC721-BURNABLE-001 test_ERC721_burnReducesTotalSupply User balance and total supply should be updated correctly when burn is called.
ERC721-BURNABLE-002 test_ERC721_burnRevertOnTransferFromPreviousOwner A token that has been burned cannot be transferred.
ERC721-BURNABLE-003 test_ERC721_burnRevertOnTransferFromZeroAddress A token that has been burned cannot be transferred.
ERC721-BURNABLE-004 test_ERC721_burnRevertOnApprove A burned token should have its approvals reset.
ERC721-BURNABLE-005 test_ERC721_burnRevertOnGetApproved getApproved() should revert if the token is burned.
ERC721-BURNABLE-006 test_ERC721_burnRevertOnOwnerOf ownerOf() should revert if the token has been burned.

Tests for mintable tokens

ID Name Invariant tested
ERC721-MINTABLE-001 test_ERC721_mintIncreasesSupply User balance and total supply should be updated correctly after minting.
ERC721-MINTABLE-002 test_ERC721_mintCreatesFreshToken User balance and total supply should be updated correctly after minting.

ERC4626

ID Name Invariant tested
ERC4626-001 verify_assetMustNotRevert asset must not revert.
ERC4626-002 verify_totalAssetsMustNotRevert totalAssets must not revert.
ERC4626-003 verify_convertToAssetsMustNotRevert convertToAssets must not revert for reasonable values.
ERC4626-004 verify_convertToSharesMustNotRevert convertToShares must not revert for reasonable values.
ERC4626-005 verify_maxDepositMustNotRevert maxDeposit must not revert.
ERC4626-006 verify_maxMintMustNotRevert maxMint must not revert.
ERC4626-007 verify_maxRedeemMustNotRevert maxRedeem must not revert.
ERC4626-008 verify_maxWithdrawMustNotRevert maxWithdraw must not revert.
ERC4626-009 verify_redeemViaApprovalProxy Redeem via approval proxy.
ERC4626-010 verify_withdrawViaApprovalProxy Withdraw via approval proxy.
ERC4626-011 verify_withdrawRequiresTokenApproval Withdraw requires approval for third parties.
ERC4626-012 verify_redeemRequiresTokenApproval Redeem requires approval for third parties.
ERC4626-013 verify_previewDepositRoundingDirection checks previewDeposit rounding direction
ERC4626-014 verify_previewMintRoundingDirection checks previewMint rounding direction
ERC4626-015 verify_convertToSharesRoundingDirection checks convertToShares rounding direction
ERC4626-016 verify_previewRedeemRoundingDirection checks previewRedeem rounding direction
ERC4626-017 verify_previewWithdrawRoundingDirection checks previewWithdraw rounding direction
ERC4626-018 verify_convertToAssetsRoundingDirection checks convertToAssets rounding direction
ERC4626-019 verify_depositRoundingDirection checks deposit rounding direction
ERC4626-020 verify_mintRoundingDirection checks mint rounding direction
ERC4626-021 verify_withdrawRoundingDirection checks withdraw rounding direction
ERC4626-022 verify_redeemRoundingDirection checks redeem rounding direction
ERC4626-023 verify_maxDepositIgnoresSenderAssets maxDeposit must assume the agent has infinite assets.
ERC4626-024 verify_maxMintIgnoresSenderAssets maxMint must assume the agent has infinite assets.
ERC4626-025 verify_previewMintIgnoresSender previewMint must not be dependent on msg.sender.
ERC4626-026 verify_previewDepositIgnoresSender previewDeposit must not be dependent on msg.sender.
ERC4626-027 verify_previewWithdrawIgnoresSender previewWithdraw must not be dependent on msg.sender.
ERC4626-028 verify_previewRedeemIgnoresSender previewRedeem must not be dependent on msg.sender.
ERC4626-029 verify_depositProperties deposit assets and shares handling.
ERC4626-030 verify_mintProperties mint assets and shares handling.
ERC4626-031 verify_redeemProperties redeem assets and shares handling.
ERC4626-032 verify_withdrawProperties withdraw assets and shares handling.
ERC4626-033 verify_sharePriceInflationAttack Checks for share inflation attacks.
ERC4626-034 verify_assetDecimalsLessThanVault Compares vault decimals with asset decimals.
ERC4626-035 verify_withdrawRequiresTokenApproval Verifies that withdraw requires token approval.
ERC4626-036 verify_redeemRequiresTokenApproval Verifies that redeem requires token approval.
ERC4626-037 verify_convertToSharesMustNotRevert convertToShares must not revert for reasonable values.

ABDKMath64x64

ID Name Invariant tested
ABDKMATH-001 add_test_commutative Commutative property for addition.
ABDKMATH-002 add_test_associative Associative property for addition.
ABDKMATH-003 add_test_identity Identity operation for addition.
ABDKMATH-004 add_test_values Addition result should increase or decrease depending on operands signs.
ABDKMATH-005 add_test_range Addition result should be in the valid 64x64-arithmetic range.
ABDKMATH-006 add_test_maximum_value Addition edge case: maximum value plus zero should be maximum value.
ABDKMATH-007 add_test_maximum_value_plus_one Addition edge case: maximum value plus one should revert (out of range).
ABDKMATH-008 add_test_minimum_value Addition edge case: minimum value plus zero should be minimum value.
ABDKMATH-009 add_test_minimum_value_plus_negative_one Addition edge case: minimum value plus minus one should revert (out of range).
ABDKMATH-010 sub_test_equivalence_to_addition Subtraction should be equal to addition with opposite sign.
ABDKMATH-011 sub_test_non_commutative Anti-commutative property for subtraction.
ABDKMATH-012 sub_test_identity Identity operation for subtraction.
ABDKMATH-013 sub_test_neutrality Adding and subtracting the same value should not affect original value.
ABDKMATH-014 sub_test_values Subtraction result should increase or decrease depending on operands signs.
ABDKMATH-015 sub_test_range Subtraction result should be in the valid 64x64-arithmetic range.
ABDKMATH-016 sub_test_maximum_value Subtraction edge case: maximum value minus zero should be maximum value.
ABDKMATH-017 sub_test_maximum_value_minus_neg_one Subtraction edge case: maximum value minus negative one should revert (out of range).
ABDKMATH-018 sub_test_minimum_value Subtraction edge case: minimum value minus zero should be minimum value.
ABDKMATH-019 sub_test_minimum_value_minus_one Subtraction edge case: minimum value minus one should revert (out of range).
ABDKMATH-020 mul_test_commutative Commutative property for multiplication.
ABDKMATH-021 mul_test_associative Associative property for multiplication.
ABDKMATH-022 mul_test_distributive Distributive property for multiplication.
ABDKMATH-023 mul_test_identity Identity operation for multiplication.
ABDKMATH-024 mul_test_values Multiplication result should increase or decrease depending on operands signs.
ABDKMATH-025 mul_test_range Multiplication result should be in the valid 64x64-arithmetic range.
ABDKMATH-026 mul_test_maximum_value Multiplication edge case: maximum value times one should be maximum value
ABDKMATH-027 mul_test_minimum_value Multiplication edge case: minimum value times one should be minimum value
ABDKMATH-028 div_test_division_identity Identity operation for division.
ABDKMATH-029 div_test_negative_divisor Division result sign should change according to divisor sign.
ABDKMATH-030 div_test_division_num_zero Division with zero numerator should be zero.
ABDKMATH-031 div_test_values Division result should increase or decrease (in absolute value) depending on divisor's absolute value.
ABDKMATH-032 div_test_div_by_zero Division edge case: Divisor zero should revert.
ABDKMATH-033 div_test_maximum_denominator Division edge case: Division result by a large number should be less than one.
ABDKMATH-034 div_test_maximum_numerator Division edge case: Division result of maximum value should revert if divisor is less than one.
ABDKMATH-035 div_test_range Division result should be in the valid 64x64-arithmetic range.
ABDKMATH-036 neg_test_double_negation Double sign negation should be equal to the original operand.
ABDKMATH-037 neg_test_identity Identity operation for sign negation.
ABDKMATH-038 neg_test_zero Negation edge case: Negation of zero should be zero.
ABDKMATH-039 neg_test_maximum Negation edge case: Negation of maximum value minus epsilon should not revert.
ABDKMATH-040 neg_test_minimum Negation edge case: Negation of minimum value plus epsilon should not revert.
ABDKMATH-041 abs_test_positive Absolute value should be always positive.
ABDKMATH-042 abs_test_negative Absolute value of a number and its negation should be equal.
ABDKMATH-043 abs_test_multiplicativeness Multiplicativeness property for absolute value.
ABDKMATH-044 abs_test_subadditivity Subadditivity property for absolute value.
ABDKMATH-045 abs_test_zero Absolute value edge case: absolute value of zero is zero.
ABDKMATH-046 abs_test_maximum Absolute value edge case: absolute value of maximum value is maximum value.
ABDKMATH-047 abs_test_minimum Absolute value edge case: absolute value of minimum value is the negation of minimum value.
ABDKMATH-048 inv_test_double_inverse Result of double inverse should be close enough to the original operand.
ABDKMATH-049 inv_test_division Inverse should be equivalent to division.
ABDKMATH-050 inv_test_division_noncommutativity Anticommutative property for inverse operation.
ABDKMATH-051 inv_test_multiplication Multiplication of inverses should be equal to inverse of multiplication.
ABDKMATH-052 inv_test_identity Identity property for inverse.
ABDKMATH-053 inv_test_values Inverse result should be in range (0, 1) if operand is greater than one.
ABDKMATH-054 inv_test_sign Inverse result should keep operand's sign.
ABDKMATH-055 inv_test_zero Inverse edge case: Inverse of zero should revert.
ABDKMATH-056 inv_test_maximum Inverse edge case: Inverse of maximum value should be close to zero.
ABDKMATH-057 inv_test_minimum Inverse edge case: Inverse of minimum value should be close to zero.
ABDKMATH-058 avg_test_values_in_range Average result should be between operands.
ABDKMATH-059 avg_test_one_value Average of the same number twice is the number itself.
ABDKMATH-060 avg_test_operand_order Average result does not depend on the order of operands.
ABDKMATH-061 avg_test_maximum Average edge case: Average of maximum value twice is the maximum value.
ABDKMATH-062 avg_test_minimum Average edge case: Average of minimum value twice is the minimum value.
ABDKMATH-063 gavg_test_values_in_range Geometric average result should be between operands.
ABDKMATH-064 gavg_test_one_value Geometric average of the same number twice is the number itself.
ABDKMATH-065 gavg_test_operand_order Geometric average result does not depend on the order of operands.
ABDKMATH-066 gavg_test_maximum Geometric average edge case: Average of maximum value twice is the maximum value.
ABDKMATH-067 gavg_test_minimum Geometric average edge case: Average of minimum value twice is the minimum value.
ABDKMATH-068 pow_test_zero_exponent Power of zero should be one.
ABDKMATH-069 pow_test_zero_base Zero to the power of any number should be zero.
ABDKMATH-070 pow_test_one_exponent Power of one should be equal to the operand.
ABDKMATH-071 pow_test_base_one One to the power of any number should be one.
ABDKMATH-072 pow_test_product_same_base Product of powers of the same base property
ABDKMATH-073 pow_test_power_of_an_exponentiation Power of an exponentiation property
ABDKMATH-074 pow_test_product_same_base Distributive property for power of a product
ABDKMATH-075 pow_test_values Power result should increase or decrease (in absolute value) depending on exponent's absolute value.
ABDKMATH-076 pow_test_sign Power result sign should change according to the exponent sign.
ABDKMATH-077 pow_test_maximum_base Power edge case: Power of the maximum value should revert if exponent > 1.
ABDKMATH-078 pow_test_high_exponent Power edge case: Result should be zero if base is small and exponent is large.
ABDKMATH-079 sqrt_test_inverse_mul Square root inverse as multiplication.
ABDKMATH-080 sqrt_test_inverse_pow Square root inverse as power.
ABDKMATH-081 sqrt_test_distributive Square root distributive property respect to multiplication.
ABDKMATH-082 sqrt_test_zero Square root edge case: square root of zero should be zero.
ABDKMATH-083 sqrt_test_maximum Square root edge case: square root of maximum value should not revert.
ABDKMATH-084 sqrt_test_minimum Square root edge case: square root of minimum value should revert (negative).
ABDKMATH-085 sqrt_test_negative Square root edge case: square root of a negative value should revert.
ABDKMATH-086 log2_test_distributive_mul Base-2 logarithm distributive property respect to multiplication.
ABDKMATH-087 log2_test_power Base-2 logarithm of a power property.
ABDKMATH-088 log2_test_zero Base-2 logarithm edge case: Logarithm of zero should revert.
ABDKMATH-089 log2_test_maximum Base-2 logarithm edge case: Logarithm of maximum value should not revert.
ABDKMATH-090 log2_test_negative Base-2 logarithm edge case: Logarithm of a negative value should revert.
ABDKMATH-091 ln_test_distributive_mul Natural logarithm distributive property respect to multiplication.
ABDKMATH-092 ln_test_power Natural logarithm of a power property.
ABDKMATH-093 ln_test_zero Natural logarithm edge case: Logarithm of zero should revert.
ABDKMATH-094 ln_test_maximum Natural logarithm edge case: Logarithm of maximum value should not revert.
ABDKMATH-095 ln_test_negative Natural logarithm edge case: Logarithm of a negative value should revert.
ABDKMATH-096 exp2_test_equivalence_pow Base-2 exponentiation should be equal to power.
ABDKMATH-097 exp2_test_inverse Base-2 exponentiation inverse function.
ABDKMATH-098 exp2_test_negative_exponent Base-2 exponentiation with negative exponent should equal the inverse.
ABDKMATH-099 exp2_test_zero Base-2 exponentiation edge case: exponent zero result should be one.
ABDKMATH-100 exp2_test_maximum Base-2 exponentiation edge case: exponent maximum value should revert.
ABDKMATH-101 exp2_test_minimum Base-2 exponentiation edge case: exponent minimum value result should be zero.
ABDKMATH-102 exp_test_inverse Natural exponentiation inverse function.
ABDKMATH-103 exp_test_negative_exponent Natural exponentiation with negative exponent should equal the inverse.
ABDKMATH-104 exp_test_zero Natural exponentiation edge case: exponent zero result should be one.
ABDKMATH-105 exp_test_maximum Natural exponentiation edge case: exponent maximum value should revert.
ABDKMATH-106 exp_test_minimum Natural exponentiation edge case: exponent minimum value result should be zero.