This file lists all the currently implemented Echidna property tests for ERC20, ERC4626, ABDKMath64x64, PRBMath SD59x18 and PRBMath UD60x18. For each property, there is a permalink to the file implementing it in the repository and a small description of the invariant tested.
| 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. |
| 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. |
| ID | Name | Invariant tested |
|---|---|---|
| ERC20-MINTABLE-001 | test_ERC20_mintTokens | User balance and total supply should be updated correctly after minting. |
| 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. |
| 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. |
| 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() |
| 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. |
| 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. |
| 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. |
| 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. |
| ID | Name | Invariant tested |
|---|---|---|
| SD59x18-001 | add_test_commutative | Commutative property for addition. |
| SD59x18-002 | add_test_associative | Associative property for addition. |
| SD59x18-003 | add_test_identity | Identity operation for addition. |
| SD59x18-004 | add_test_values | Addition result should increase or decrease depending on operands signs. |
| SD59x18-005 | add_test_range | Addition result should be in the valid 59x18-arithmetic range. |
| SD59x18-006 | add_test_maximum_value | Addition edge case: maximum value plus zero should be maximum value. |
| SD59x18-007 | add_test_maximum_value_plus_one | Addition edge case: maximum value plus one should revert (out of range). |
| SD59x18-008 | add_test_minimum_value | Addition edge case: minimum value plus zero should be minimum value. |
| SD59x18-009 | add_test_minimum_value_plus_negative_one | Addition edge case: minimum value plus minus one should revert (out of range). |
| SD59x18-010 | sub_test_equivalence_to_addition | Subtraction should be equal to addition with opposite sign. |
| SD59x18-011 | sub_test_non_commutative | Anti-commutative property for subtraction. |
| SD59x18-012 | sub_test_identity | Identity operation for subtraction. |
| SD59x18-013 | sub_test_neutrality | Adding and subtracting the same value should not affect original value. |
| SD59x18-014 | sub_test_values | Subtraction result should increase or decrease depending on operands signs. |
| SD59x18-015 | sub_test_range | Subtraction result should be in the valid 59x18-arithmetic range. |
| SD59x18-016 | sub_test_maximum_value | Subtraction edge case: maximum value minus zero should be maximum value. |
| SD59x18-017 | sub_test_maximum_value_minus_neg_one | Subtraction edge case: maximum value minus negative one should revert (out of range). |
| SD59x18-018 | sub_test_minimum_value | Subtraction edge case: minimum value minus zero should be minimum value. |
| SD59x18-019 | sub_test_minimum_value_minus_one | Subtraction edge case: minimum value minus one should revert (out of range). |
| SD59x18-020 | mul_test_commutative | Commutative property for multiplication. |
| SD59x18-021 | mul_test_associative | Associative property for multiplication. |
| SD59x18-022 | mul_test_distributive | Distributive property for multiplication. |
| SD59x18-023 | mul_test_identity | Identity operation for multiplication. |
| SD59x18-024 | mul_test_x_positive | Multiplication result should increase or decrease depending on operands signs. |
| SD59x18-025 | mul_test_x_negative | Multiplication result should increase or decrease depending on operands signs. |
| SD59x18-026 | mul_test_range | Multiplication result should be in the valid 59x18-arithmetic range. |
| SD59x18-027 | mul_test_maximum_value | Multiplication edge case: maximum value times one should be maximum value |
| SD59x18-028 | mul_test_minimum_value | Multiplication edge case: minimum value times one should be minimum value |
| SD59x18-029 | div_test_division_identity_x_div_1 | Identity operation for division. x / 1 == x |
| SD59x18-030 | div_test_division_identity_x_div_x | Identity operation for division. x / x == 1 |
| SD59x18-031 | div_test_negative_divisor | Division result sign should change according to divisor sign. |
| SD59x18-032 | div_test_division_num_zero | Division with zero numerator should be zero. |
| SD59x18-033 | div_test_values | Division result should increase or decrease (in absolute value) depending on divisor's absolute value. |
| SD59x18-034 | div_test_div_by_zero | Division edge case: Divisor zero should revert. |
| SD59x18-035 | div_test_maximum_denominator | Division edge case: Division result by a large number should be less than one. |
| SD59x18-036 | div_test_maximum_numerator | Division edge case: Division result of maximum value should revert if divisor is less than one. |
| SD59x18-037 | div_test_range | Division result should be in the valid 64x64-arithmetic range. |
| SD59x18-038 | neg_test_double_negation | Double sign negation should be equal to the original operand. |
| SD59x18-039 | neg_test_identity | Identity operation for sign negation. |
| SD59x18-040 | neg_test_zero | Negation edge case: Negation of zero should be zero. |
| SD59x18-041 | neg_test_maximum | Negation edge case: Negation of maximum value minus epsilon should not revert. |
| SD59x18-042 | neg_test_minimum | Negation edge case: Negation of minimum value plus epsilon should not revert. |
| SD59x18-043 | abs_test_positive | Absolute value should be always positive. |
| SD59x18-044 | abs_test_negative | Absolute value of a number and its negation should be equal. |
| SD59x18-045 | abs_test_multiplicativeness | Multiplicativeness property for absolute value. |
| SD59x18-046 | abs_test_subadditivity | Subadditivity property for absolute value. |
| SD59x18-047 | abs_test_zero | Absolute value edge case: absolute value of zero is zero. |
| SD59x18-048 | abs_test_maximum | Absolute value edge case: absolute value of maximum value is maximum value. |
| SD59x18-049 | abs_test_minimum_revert | Absolute value edge case: absolute value of minimum value should revert |
| SD59x18-050 | abs_test_minimum_allowed | Absolute value edge case: absolute value of minimum permitted value is the negation of minimum value. |
| SD59x18-051 | inv_test_double_inverse | Result of double inverse should be close enough to the original operand. |
| SD59x18-052 | inv_test_division | Inverse should be equivalent to division. |
| SD59x18-053 | inv_test_division_noncommutativity | Anticommutative property for inverse operation. |
| SD59x18-054 | inv_test_multiplication | Multiplication of inverses should be equal to inverse of multiplication. |
| SD59x18-055 | inv_test_identity | Identity property for inverse. |
| SD59x18-056 | inv_test_values | Inverse result should be in range (0, 1) if operand is greater than one. |
| SD59x18-057 | inv_test_sign | Inverse result should keep operand's sign. |
| SD59x18-058 | inv_test_zero | Inverse edge case: Inverse of zero should revert. |
| SD59x18-059 | inv_test_maximum | Inverse edge case: Inverse of maximum value should be close to zero. |
| SD59x18-060 | inv_test_minimum | Inverse edge case: Inverse of minimum value should be close to zero. |
| SD59x18-061 | avg_test_values_in_range | Average result should be between operands. |
| SD59x18-062 | avg_test_one_value | Average of the same number twice is the number itself. |
| SD59x18-063 | avg_test_operand_order | Average result does not depend on the order of operands. |
| SD59x18-064 | avg_test_maximum | Average edge case: Average of maximum value twice is the maximum value. |
| SD59x18-065 | avg_test_minimum | Average edge case: Average of minimum value twice is the minimum value. |
| SD59x18-066 | pow_test_zero_exponent | Power of zero should be one. |
| SD59x18-067 | pow_test_zero_base_non_zero_exponent | Zero to the power of any number should be zero. |
| SD59x18-068 | pow_test_zero_base_zero_exponent | Zero to the power of zero should be one |
| SD59x18-069 | pow_test_one_exponent | Power of one should be equal to the operand. |
| SD59x18-070 | pow_test_base_one | One to the power of any number should be one. |
| SD59x18-071 | pow_test_product_same_base | Product of powers of the same base property |
| SD59x18-072 | pow_test_power_of_an_exponentiation | Power of an exponentiation property |
| SD59x18-073 | pow_test_product_power | Distributive property for power of a product |
| SD59x18-074 | pow_test_positive_exponent | Power result should increase or decrease (in absolute value) depending on exponent's absolute value. |
| SD59x18-075 | pow_test_negative_exponent | Power result should increase or decrease (in absolute value) depending on exponent's absolute value. |
| SD59x18-076 | pow_test_sign | Power result sign should change according to the exponent sign. |
| SD59x18-077 | pow_test_exp2_equivalence | Base-2 exponentiation should be equal to power. |
| SD59x18-078 | pow_test_maximum_base | Power edge case: Power of the maximum value should revert if exponent > 1. |
| SD59x18-079 | pow_test_high_exponent | Power edge case: Result should be zero if base is small and exponent is large. |
| SD59x18-080 | sqrt_test_inverse_mul | Square root inverse as multiplication. |
| SD59x18-081 | sqrt_test_inverse_pow | Square root inverse as power. |
| SD59x18-082 | sqrt_test_distributive | Square root distributive property respect to multiplication. |
| SD59x18-083 | sqrt_test_is_increasing | Square root should be strictly increasing for any x |
| SD59x18-084 | sqrt_test_zero | Square root edge case: square root of zero should be zero. |
| SD59x18-085 | sqrt_test_maximum | Square root edge case: square root of maximum value should not revert. |
| SD59x18-086 | sqrt_test_minimum | Square root edge case: square root of minimum value should revert (negative). |
| SD59x18-087 | sqrt_test_negative | Square root edge case: square root of a negative value should revert. |
| SD59x18-088 | log2_test_distributive_mul | Base-2 logarithm distributive property respect to multiplication. |
| SD59x18-089 | log2_test_power | Base-2 logarithm of a power property. |
| SD59x18-090 | log2_test_zero | Base-2 logarithm edge case: Logarithm of zero should revert. |
| SD59x18-091 | log2_test_maximum | Base-2 logarithm edge case: Logarithm of maximum value should not revert. |
| SD59x18-092 | log2_test_negative | Base-2 logarithm edge case: Logarithm of a negative value should revert. |
| SD59x18-093 | ln_test_distributive_mul | Natural logarithm distributive property respect to multiplication. |
| SD59x18-094 | ln_test_power | Natural logarithm of a power property. |
| SD59x18-095 | ln_test_zero | Natural logarithm edge case: Logarithm of zero should revert. |
| SD59x18-096 | ln_test_maximum | Natural logarithm edge case: Logarithm of maximum value should not revert. |
| SD59x18-097 | ln_test_negative | Natural logarithm edge case: Logarithm of a negative value should revert. |
| SD59x18-098 | exp2_test_equivalence_pow | Base-2 exponentiation should be equal to power. |
| SD59x18-099 | exp2_test_inverse | Base-2 exponentiation inverse function. |
| SD59x18-100 | exp2_test_negative_exponent | Base-2 exponentiation with negative exponent should equal the inverse. |
| SD59x18-101 | exp2_test_zero | Base-2 exponentiation edge case: exponent zero result should be one. |
| SD59x18-102 | exp2_test_maximum | Base-2 exponentiation edge case: exponent maximum value should revert. |
| SD59x18-103 | exp2_test_maximum_permitted | Base-2 exponentiation edge case: exponent maximum permitted value should not revert. |
| SD59x18-104 | exp2_test_minimum | Base-2 exponentiation edge case: exponent minimum value result should be zero. |
| SD59x18-105 | exp_test_inverse | Natural exponentiation inverse function. |
| SD59x18-106 | exp_test_negative_exponent | Natural exponentiation with negative exponent should equal the inverse. |
| SD59x18-107 | exp_test_strictly_increasing | Natural exponentiation should be strictly increasing for any x |
| SD59x18-108 | exp_test_zero | Natural exponentiation edge case: exponent zero result should be one. |
| SD59x18-109 | exp_test_maximum | Natural exponentiation edge case: exponent maximum value should revert. |
| SD59x18-110 | exp_test_maximum_permitted | Natural exponentiation edge case: exponent maximum value should revert. |
| SD59x18-111 | exp_test_minimum | Natural exponentiation edge case: exponent minimum value result should be zero. |
| SD59x18-112 | powu_test_zero_exponent | Power of zero should be one. |
| SD59x18-113 | powu_test_zero_base | Zero to the power of any number should be zero. |
| SD59x18-114 | powu_test_one_exponent | Power of one should be equal to the operand. |
| SD59x18-115 | powu_test_base_one | One to the power of any number should be one. |
| SD59x18-116 | powu_test_product_same_base | Product of powers of the same base property |
| SD59x18-117 | powu_test_power_of_an_exponentiation | Power of an exponentiation property |
| SD59x18-118 | powu_test_product_power | Distributive property for power of a product |
| SD59x18-119 | powu_test_values | Power result should increase or decrease (in absolute value) depending on exponent's absolute value. |
| SD59x18-120 | powu_test_sign | Power result sign should change according to the exponent sign. |
| SD59x18-121 | powu_test_maximum_base | Power edge case: Power of the maximum value should revert if exponent > 1. |
| SD59x18-122 | powu_test_high_exponent | Power edge case: Result should be zero if base is small and exponent is large. |
| SD59x18-123 | log10_test_distributive_mul | Base-10 logarithm distributive property respect to multiplication. |
| SD59x18-124 | log10_test_power | Base-10 logarithm of a power property. |
| SD59x18-125 | log10_test_zero | Base-10 logarithm edge case: Logarithm of zero should revert. |
| SD59x18-126 | log10_test_maximum | Base-10 logarithm edge case: Logarithm of maximum value should not revert. |
| SD59x18-127 | log10_test_negative | Base-10 logarithm edge case: Logarithm of a negative value should revert. |
| SD59x18-128 | gm_test_product | Product of the values should be equal to the geometric mean raised to the power of N |
| SD59x18-129 | gm_test_positive_set_avg | The geometric mean of a set of positive values should be less than the arithmetic mean |
| SD59x18-130 | gm_test_positive_equal_set_avg | The geometric mean of a set of equal positive values should be equal to the arithmetic mean |
| SD59x18-131 | gm_test_zero | GM edge case: if a set contains zero, the result is zero |
| SD59x18-132 | gm_test_negative | GM edge case: The geometric mean is not defined when the set contains an odd number of negative values |
| ID | Name | Invariant tested |
|---|---|---|
| UD60x18-001 | add_test_commutative | Commutative property for addition. |
| UD60x18-002 | add_test_associative | Associative property for addition. |
| UD60x18-003 | add_test_identity | Identity operation for addition. |
| UD60x18-004 | add_test_values | Addition result should increase or decrease depending on operands signs. |
| UD60x18-005 | add_test_range | Addition result should be in the valid 60x18-arithmetic range. |
| UD60x18-006 | add_test_maximum_value | Addition edge case: maximum value plus zero should be maximum value. |
| UD60x18-007 | add_test_maximum_value_plus_one | Addition edge case: maximum value plus one should revert (out of range). |
| UD60x18-008 | add_test_minimum_value | Addition edge case: minimum value plus zero should be minimum value. |
| UD60x18-009 | sub_test_identity | Identity operation for subtraction. |
| UD60x18-010 | sub_test_neutrality | Adding and subtracting the same value should not affect original value. |
| UD60x18-011 | sub_test_values | Subtraction result should increase or decrease depending on operands signs. |
| UD60x18-012 | sub_test_range | Subtraction result should be in the valid 60x18-arithmetic range. |
| UD60x18-013 | sub_test_maximum_value | Subtraction edge case: maximum value minus zero should be maximum value. |
| UD60x18-014 | sub_test_minimum_value | Subtraction edge case: minimum value minus zero should be minimum value. |
| UD60x18-015 | sub_test_minimum_value_minus_one | Subtraction edge case: minimum value minus one should revert (out of range). |
| UD60x18-016 | mul_test_commutative | Commutative property for multiplication. |
| UD60x18-017 | mul_test_associative | Associative property for multiplication. |
| UD60x18-018 | mul_test_distributive | Distributive property for multiplication. |
| UD60x18-019 | mul_test_identity | Identity operation for multiplication. |
| UD60x18-020 | mul_test_values | Multiplication result should increase or decrease depending on operands signs. |
| UD60x18-021 | mul_test_range | Multiplication result should be in the valid 59x18-arithmetic range. |
| UD60x18-022 | mul_test_maximum_value | Multiplication edge case: maximum value times one should be maximum value |
| UD60x18-023 | div_test_division_identity_x_div_1 | Identity operation for division. x / 1 == x |
| UD60x18-024 | div_test_division_identity_x_div_x | Identity operation for division. x / x == 1 |
| UD60x18-025 | div_test_division_num_zero | Division with zero numerator should be zero. |
| UD60x18-026 | div_test_values | Division result should increase or decrease (in absolute value) depending on divisor's absolute value. |
| UD60x18-027 | div_test_div_by_zero | Division edge case: Divisor zero should revert. |
| UD60x18-028 | div_test_maximum_denominator | Division edge case: Division result by a large number should be less than one. |
| UD60x18-029 | div_test_maximum_numerator | Division edge case: Division result of maximum value should revert if divisor is less than one. |
| UD60x18-030 | div_test_range | Division result should be in the valid 60x18-arithmetic range. |
| UD60x18-031 | inv_test_double_inverse | Result of double inverse should be close enough to the original operand. |
| UD60x18-032 | inv_test_division | Inverse should be equivalent to division. |
| UD60x18-033 | inv_test_division_noncommutativity | Anticommutative property for inverse operation. |
| UD60x18-034 | inv_test_multiplication | Multiplication of inverses should be equal to inverse of multiplication. |
| UD60x18-035 | inv_test_identity | Identity property for inverse. |
| UD60x18-036 | inv_test_values | Inverse result should be in range (0, 1) if operand is greater than one. |
| UD60x18-037 | inv_test_zero | Inverse edge case: Inverse of zero should revert. |
| UD60x18-038 | inv_test_maximum | Inverse edge case: Inverse of maximum value should be close to zero. |
| UD60x18-039 | inv_test_minimum | Inverse edge case: Inverse of minimum value should be close to zero. |
| UD60x18-040 | avg_test_values_in_range | Average result should be between operands. |
| UD60x18-041 | avg_test_one_value | Average of the same number twice is the number itself. |
| UD60x18-042 | avg_test_operand_order | Average result does not depend on the order of operands. |
| UD60x18-043 | avg_test_maximum | Average edge case: Average of maximum value twice is the maximum value. |
| UD60x18-044 | pow_test_zero_exponent | Power of zero should be one. |
| UD60x18-045 | pow_test_zero_base | Zero to the power of any number should be zero. |
| UD60x18-046 | pow_test_one_exponent | Power of one should be equal to the operand. |
| UD60x18-047 | pow_test_base_one | One to the power of any number should be one. |
| UD60x18-048 | pow_test_product_same_base | Product of powers of the same base property |
| UD60x18-049 | pow_test_power_of_an_exponentiation | Power of an exponentiation property |
| UD60x18-050 | pow_test_product_power | Distributive property for power of a product |
| UD60x18-051 | pow_test_values | Power result should increase or decrease (in absolute value) depending on exponent's absolute value. |
| UD60x18-052 | pow_test_maximum_base | Power edge case: Power of the maximum value should revert if exponent > 1. |
| UD60x18-053 | pow_test_maximum_exponent | Power edge case: Power of the maximum value should revert if exponent > 1. |
| UD60x18-054 | pow_test_high_exponent | Power edge case: Result should be zero if base is small and exponent is large. |
| UD60x18-055 | sqrt_test_inverse_mul | Square root inverse as multiplication. |
| UD60x18-056 | sqrt_test_inverse_pow | Square root inverse as power. |
| UD60x18-057 | sqrt_test_distributive | Square root distributive property respect to multiplication. |
| UD60x18-058 | sqrt_test_zero | Square root edge case: square root of zero should be zero. |
| UD60x18-059 | sqrt_test_maximum | Square root edge case: square root of maximum value should not revert. |
| UD60x18-060 | log2_test_distributive_mul | Base-2 logarithm distributive property respect to multiplication. |
| UD60x18-061 | log2_test_power | Base-2 logarithm of a power property. |
| UD60x18-062 | log2_test_zero | Base-2 logarithm edge case: Logarithm of zero should revert. |
| UD60x18-063 | log2_test_maximum | Base-2 logarithm edge case: Logarithm of maximum value should not revert. |
| UD60x18-064 | log2_test_less_than_unit | Base-2 logarithm edge case: Logarithm of a negative value should revert. |
| UD60x18-065 | ln_test_distributive_mul | Natural logarithm distributive property respect to multiplication. |
| UD60x18-066 | ln_test_power | Natural logarithm of a power property. |
| UD60x18-067 | ln_test_zero | Natural logarithm edge case: Logarithm of zero should revert. |
| UD60x18-068 | ln_test_maximum | Natural logarithm edge case: Logarithm of maximum value should not revert. |
| UD60x18-069 | ln_test_less_than_unit | Natural logarithm edge case: Logarithm of a negative value should revert. |
| UD60x18-070 | exp2_test_equivalence_pow | Base-2 exponentiation should be equal to power. |
| UD60x18-071 | exp2_test_inverse | Base-2 exponentiation inverse function. |
| UD60x18-072 | exp2_test_zero | Base-2 exponentiation edge case: exponent zero result should be one. |
| UD60x18-073 | exp2_test_maximum | Base-2 exponentiation edge case: exponent maximum value should revert. |
| UD60x18-075 | exp_test_inverse | Natural exponentiation inverse function. |
| UD60x18-076 | exp_test_zero | Natural exponentiation edge case: exponent zero result should be one. |
| UD60x18-077 | exp_test_maximum | Natural exponentiation edge case: exponent maximum value should revert. |
| UD60x18-078 | powu_test_zero_exponent | Power of zero should be one. |
| UD60x18-079 | powu_test_zero_base | Zero to the power of any number should be zero. |
| UD60x18-080 | powu_test_one_exponent | Power of one should be equal to the operand. |
| UD60x18-081 | powu_test_base_one | One to the power of any number should be one. |
| UD60x18-082 | powu_test_product_same_base | Product of powers of the same base property |
| UD60x18-083 | powu_test_power_of_an_exponentiation | Power of an exponentiation property |
| UD60x18-084 | powu_test_product_power | Distributive property for power of a product |
| UD60x18-085 | powu_test_values | Power result should increase or decrease (in absolute value) depending on exponent's absolute value. |
| UD60x18-086 | powu_test_maximum_base | Power edge case: Power of the maximum value should revert if exponent > 1. |
| UD60x18-087 | powu_test_high_exponent | Power edge case: Result should be zero if base is small and exponent is large. |
| UD60x18-088 | log10_test_distributive_mul | Base-10 logarithm distributive property respect to multiplication. |
| UD60x18-089 | log10_test_power | Base-10 logarithm of a power property. |
| UD60x18-090 | log10_test_zero | Base-10 logarithm edge case: Logarithm of zero should revert. |
| UD60x18-091 | log10_test_maximum | Base-10 logarithm edge case: Logarithm of maximum value should not revert. |
| UD60x18-092 | log10_test_less_than_unit | Base-10 logarithm edge case: Logarithm of a negative value should revert. |
| UD60x18-093 | gm_test_product | Product of the values should be equal to the geometric mean raised to the power of N |
| UD60x18-094 | gm_test_positive_set_avg | The geometric mean of a set of positive values should be less than the arithmetic mean |
| UD60x18-095 | gm_test_positive_equal_set_avg | The geometric mean of a set of equal positive values should be equal to the arithmetic mean |
| UD60x18-096 | gm_test_zero | GM edge case: if a set contains zero, the result is zero |