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

• Introduction
  • Table of contents
  • ERC20
    • Basic properties for standard functions
    • Tests for burnable tokens
    • Tests for mintable tokens
    • Tests for pausable tokens
    • Tests for tokens implementing increaseAllowance and decreaseAllowance
• ERC721
  • Basic properties for standard functions
  • Tests for burnable tokens
  • Tests for mintable tokens
  • ERC4626
  • ABDKMath64x64

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_distributive	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.