以太坊 - 介绍

  • crytic
  • 发布于 2025-11-27 20:53
  • 阅读 17

本文档列出了当前为 ERC20、ERC721、ERC4626 和 ABDKMath64x64 实现的所有 Echidna 属性测试。对于每个属性，都有一个指向存储库中实现它的文件的永久链接，以及测试的不变式的简短描述。主要分为ERC20、ERC721、ERC4626、ABDKMath64x64 四个部分，分别介绍了各自的基本功能属性，以及可燃烧、可铸造和可暂停代币的测试。

介绍

本文件列出了当前为 ERC20、ERC721、ERC4626 和 ABDKMath64x64 实现的所有 Echidna 属性测试。 对于每个属性，都有一个指向存储库中实现它的文件的永久链接，以及对所测试不变量的简短描述。

目录

ERC20

标准函数的基本属性

ID 名称 测试的不变量
ERC20-BASE-001 test_ERC20_constantSupply 对于不可铸造和不可销毁的代币，总供应量应保持不变。
ERC20-BASE-002 test_ERC20_userBalanceNotHigherThanSupply 没有用户的余额应该大于代币的总供应量。
ERC20-BASE-003 test_ERC20_usersBalancesNotHigherThanSupply 用户余额的总和不应大于代币的总供应量。
ERC20-BASE-004 test_ERC20_zeroAddressBalance 地址零的代币余额应为零。
ERC20-BASE-005 test_ERC20_transferToZeroAddress 不应允许 transfer 到零地址。
ERC20-BASE-006 test_ERC20_transferFromToZeroAddress 不应允许 transferFrom 到零地址。
ERC20-BASE-007 test_ERC20_selfTransfer 自我 transfer 不应破坏会计。
ERC20-BASE-008 test_ERC20_selfTransferFrom 自我 transferFrom 不应破坏会计。
ERC20-BASE-009 test_ERC20_transferMoreThanBalance 不应允许 transfer 超过帐户余额。
ERC20-BASE-010 test_ERC20_transferFromMoreThanBalance 不应允许 transferFrom 超过帐户余额。
ERC20-BASE-011 test_ERC20_transferZeroAmount 零金额的 transfer 不应破坏会计。
ERC20-BASE-012 test_ERC20_transferFromZeroAmount 零金额的 transferFrom 不应破坏会计。
ERC20-BASE-013 test_ERC20_transfer 有效的 transfer 应正确更新会计。
ERC20-BASE-014 test_ERC20_transferFrom 有效的 transferFrom 应正确更新会计。
ERC20-BASE-015 test_ERC20_setAllowance 调用 approve 时，应正确设置授权额度。
ERC20-BASE-016 test_ERC20_setAllowanceTwice 当调用两次 approve 时，应正确更新授权额度。
ERC20-BASE-017 test_ERC20_spendAllowanceAfterTransfer 在 transferFrom 之后，应正确更新授权额度。

可销毁代币的测试

ID 名称 测试的不变量
ERC20-BURNABLE-001 test_ERC20_burn 调用 burn 时，应正确更新用户余额和总供应量。
ERC20-BURNABLE-002 test_ERC20_burnFrom 调用 burnFrom 时，应正确更新用户余额和总供应量。
ERC20-BURNABLE-003 test_ERC20_burnFromUpdateAllowance 调用 burnFrom 时，应正确更新授权额度。

可铸造代币的测试

ID 名称 测试的不变量
ERC20-MINTABLE-001 test_ERC20_mintTokens 薄荷之后，应正确更新用户余额和总供应量。

可暂停代币的测试

ID 名称 测试的不变量
ERC20-PAUSABLE-001 test_ERC20_pausedTransfer 启用暂停状态时，不应允许代币 transfer。
ERC20-PAUSABLE-002 test_ERC20_pausedTransferFrom 启用暂停状态时，不应允许代币 transferFrom。

为实现 increaseAllowance 和 decreaseAllowance 的代币进行的测试

ID 名称 测试的不变量
ERC20-ALLOWANCE-001 test_ERC20_setAndIncreaseAllowance 调用 increaseAllowance 时，应正确更新授权额度。
ERC20-ALLOWANCE-002 test_ERC20_setAndDecreaseAllowance 调用 decreaseAllowance 时，应正确更新授权额度。

ERC721

标准函数的基本属性

ID 名称 测试的不变量
ERC721-BASE-001 test_ERC721_balanceOfZeroAddressMustRevert 为零地址调用 balanceOf 应该 revert。
ERC721-BASE-002 test_ERC721_ownerOfInvalidTokenMustRevert 为无效 token 调用 ownerOf 应该 revert。
ERC721-BASE-003 test_ERC721_approvingInvalidTokenMustRevert approve() 应该 revert 无效 token。
ERC721-BASE-004 test_ERC721_transferFromNotApproved 如果调用者不是 operator，transferFrom() 应该 revert。
ERC721-BASE-005 test_ERC721_transferFromResetApproval transferFrom() 应该重置 approvals。
ERC721-BASE-006 test_ERC721_transferFromUpdatesOwner transferFrom() 应该更新 token owner。
ERC721-BASE-007 test_ERC721_transferFromZeroAddress 如果 from 是零地址，transferFrom() 应该 revert。
ERC721-BASE-008 test_ERC721_transferToZeroAddress 如果 to 是零地址，transferFrom() 应该 revert。
ERC721-BASE-009 test_ERC721_transferFromSelf 对自己 transferFrom() 不应破坏 accounting。
ERC721-BASE-010 test_ERC721_transferFromSelfResetsApproval 对自己 transferFrom() 应该重置 approvals。
ERC721-BASE-011 test_ERC721_safeTransferFromRevertsOnNoncontractReceiver 如果接收者是一个没有实现 onERC721Received() 的合约，safeTransferFrom() 应该 revert

可销毁代币的测试

ID 名称 测试的不变量
ERC721-BURNABLE-001 test_ERC721_burnReducesTotalSupply 调用 burn 时，应该正确更新用户余额和总供应量。
ERC721-BURNABLE-002 test_ERC721_burnRevertOnTransferFromPreviousOwner 已经被销毁的 token 不能被 transfer。
ERC721-BURNABLE-003 test_ERC721_burnRevertOnTransferFromZeroAddress 已经被销毁的 token 不能被 transfer。
ERC721-BURNABLE-004 test_ERC721_burnRevertOnApprove 一个被销毁的 token 应该重置它的 approvals。
ERC721-BURNABLE-005 test_ERC721_burnRevertOnGetApproved 如果 token 被销毁，getApproved() 应该 revert。
ERC721-BURNABLE-006 test_ERC721_burnRevertOnOwnerOf 如果 token 已经被销毁，ownerOf() 应该 revert。

可铸造代币的测试

ID 名称 测试的不变量
ERC721-MINTABLE-001 test_ERC721_mintIncreasesSupply 在铸造后，应该正确更新用户余额和总供应量。
ERC721-MINTABLE-002 test_ERC721_mintCreatesFreshToken 在铸造后，应该正确更新用户余额和总供应量。

ERC4626

ID 名称 测试的不变量
ERC4626-001 verify_assetMustNotRevert asset 必须不能 revert。
ERC4626-002 verify_totalAssetsMustNotRevert totalAssets 必须不能 revert。
ERC4626-003 verify_convertToAssetsMustNotRevert 对于合理的值，convertToAssets 必须不能 revert。
ERC4626-004 verify_convertToSharesMustNotRevert 对于合理的值，convertToShares 必须不能 revert。
ERC4626-005 verify_maxDepositMustNotRevert maxDeposit 必须不能 revert。
ERC4626-006 verify_maxMintMustNotRevert maxMint 必须不能 revert。
ERC4626-007 verify_maxRedeemMustNotRevert maxRedeem 必须不能 revert。
ERC4626-008 verify_maxWithdrawMustNotRevert maxWithdraw 必须不能 revert。
ERC4626-009 verify_redeemViaApprovalProxy 通过 approval 代理 redeem。
ERC4626-010 verify_withdrawViaApprovalProxy 通过 approval 代理 withdraw。
ERC4626-011 verify_withdrawRequiresTokenApproval Withdraw 需要对第三方进行 approval。
ERC4626-012 verify_redeemRequiresTokenApproval Redeem 需要对第三方进行 approval。
ERC4626-013 verify_previewDepositRoundingDirection 检查 previewDeposit 舍入方向
ERC4626-014 verify_previewMintRoundingDirection 检查 previewMint 舍入方向
ERC4626-015 verify_convertToSharesRoundingDirection 检查 convertToShares 舍入方向
ERC4626-016 verify_previewRedeemRoundingDirection 检查 previewRedeem 舍入方向
ERC4626-017 verify_previewWithdrawRoundingDirection 检查 previewWithdraw 舍入方向
ERC4626-018 verify_convertToAssetsRoundingDirection 检查 convertToAssets 舍入方向
ERC4626-019 verify_depositRoundingDirection 检查 deposit 舍入方向
ERC4626-020 verify_mintRoundingDirection 检查 mint 舍入方向
ERC4626-021 verify_withdrawRoundingDirection 检查 withdraw 舍入方向
ERC4626-022 verify_redeemRoundingDirection 检查 redeem 舍入方向
ERC4626-023 verify_maxDepositIgnoresSenderAssets maxDeposit 必须假定 agent 具有无限的资产。
ERC4626-024 verify_maxMintIgnoresSenderAssets maxMint 必须假定 agent 具有无限的资产。
ERC4626-025 verify_previewMintIgnoresSender previewMint 必须不依赖于 msg.sender。
ERC4626-026 verify_previewDepositIgnoresSender previewDeposit 必须不依赖于 msg.sender。
ERC4626-027 verify_previewWithdrawIgnoresSender previewWithdraw 必须不依赖于 msg.sender。
ERC4626-028 verify_previewRedeemIgnoresSender previewRedeem 必须不依赖于 msg.sender。
ERC4626-029 verify_depositProperties deposit 资产和 shares 处理。
ERC4626-030 verify_mintProperties mint 资产和 shares 处理。
ERC4626-031 verify_redeemProperties redeem 资产和 shares 处理。
ERC4626-032 verify_withdrawProperties withdraw 资产和 shares 处理。
ERC4626-033 verify_sharePriceInflationAttack 检查 share inflation attacks。
ERC4626-034 verify_assetDecimalsLessThanVault 比较 vault 小数位数与 asset 小数位数。
ERC4626-035 verify_withdrawRequiresTokenApproval 验证 withdraw 需要 token approval。
ERC4626-036 verify_redeemRequiresTokenApproval 验证 redeem 需要 token approval。
ERC4626-037 verify_convertToSharesMustNotRevert 对于合理的值，convertToShares 必须不能 revert。

ABDKMath64x64

ID 名称 测试的不变性
ABDKMATH-001 add_test_commutative 加法的交换律。
ABDKMATH-002 add_test_associative 加法的结合律。
ABDKMATH-003 add_test_identity 加法的单位元运算。
ABDKMATH-004 add_test_values 加法结果应根据操作数符号增加或减少。
ABDKMATH-005 add_test_range 加法结果应在有效的64x64算术范围内。
ABDKMATH-006 add_test_maximum_value 加法边界情况：最大值加零应为最大值。
ABDKMATH-007 add_test_maximum_value_plus_one 加法边界情况：最大值加一应回退（超出范围）。
ABDKMATH-008 add_test_minimum_value 加法边界情况：最小值加零应为最小值。
ABDKMATH-009 add_test_minimum_value_plus_negative_one 加法边界情况：最小值加负一应回退（超出范围）。
ABDKMATH-010 sub_test_equivalence_to_addition 减法应等于带相反符号的加法。
ABDKMATH-011 sub_test_non_commutative 减法的反交换律。
ABDKMATH-012 sub_test_identity 减法的单位元运算。
ABDKMATH-013 sub_test_neutrality 添加和减去相同的值不应影响原始值。
ABDKMATH-014 sub_test_values 减法结果应根据操作数符号增加或减少。
ABDKMATH-015 sub_test_range 减法结果应在有效的64x64算术范围内。
ABDKMATH-016 sub_test_maximum_value 减法边界情况：最大值减零应为最大值。
ABDKMATH-017 sub_test_maximum_value_minus_neg_one 减法边界情况：最大值减负一应回退（超出范围）。
ABDKMATH-018 sub_test_minimum_value 减法边界情况：最小值减零应为最小值。
ABDKMATH-019 sub_test_minimum_value_minus_one 减法边界情况：最小值减一应回退（超出范围）。
ABDKMATH-020 mul_test_commutative 乘法的交换律。
ABDKMATH-021 mul_test_associative 乘法的结合律。
ABDKMATH-022 mul_test_distributive 乘法的分配律。
ABDKMATH-023 mul_test_identity 乘法的单位元运算。
ABDKMATH-024 mul_test_values 乘法结果应根据操作数符号增加或减少。
ABDKMATH-025 mul_test_range 乘法结果应在有效的64x64算术范围内。
ABDKMATH-026 mul_test_maximum_value 乘法边界情况：最大值乘以一应为最大值。
ABDKMATH-027 mul_test_minimum_value 乘法边界情况：最小值乘以一应为最小值。
ABDKMATH-028 div_test_division_identity 除法的单位元运算。
ABDKMATH-029 div_test_negative_divisor 除法结果的符号应根据除数的符号而变化。
ABDKMATH-030 div_test_division_num_zero 分子为零的除法应为零。
ABDKMATH-031 div_test_values 除法结果应根据除数的绝对值增加或减少（绝对值）。
ABDKMATH-032 div_test_div_by_zero 除法边界情况：除数为零应回退。
ABDKMATH-033 div_test_maximum_denominator 除法边界情况：除以大数的除法结果应小于一。
ABDKMATH-034 div_test_maximum_numerator 除法边界情况：如果除数小于一，则最大值的除法结果应回退。
ABDKMATH-035 div_test_range 除法结果应在有效的64x64算术范围内。
ABDKMATH-036 neg_test_double_negation 双重符号取反应等于原始操作数。
ABDKMATH-037 neg_test_identity 符号取反的单位元运算。
ABDKMATH-038 neg_test_zero 取反边界情况：零的取反应为零。
ABDKMATH-039 neg_test_maximum 取反边界情况：最大值减去 epsilon 的取反不应回退。
ABDKMATH-040 neg_test_minimum 取反边界情况：最小值加上 epsilon 的取反不应回退。
ABDKMATH-041 abs_test_positive 绝对值应始终为正。
ABDKMATH-042 abs_test_negative 一个数及其取反的绝对值应相等。
ABDKMATH-043 abs_test_multiplicativeness 绝对值的可乘性。
ABDKMATH-044 abs_test_subadditivity 绝对值的次可加性。
ABDKMATH-045 abs_test_zero 绝对值边界情况：零的绝对值为零。
ABDKMATH-046 abs_test_maximum 绝对值边界情况：最大值的绝对值为最大值。
ABDKMATH-047 abs_test_minimum 绝对值边界情况：最小值的绝对值为最小值的取反。
ABDKMATH-048 inv_test_double_inverse 双重倒数的结果应足够接近原始操作数。
ABDKMATH-049 inv_test_division 倒数应等同于除法。
ABDKMATH-050 inv_test_division_noncommutativity 倒数运算的反交换律。
ABDKMATH-051 inv_test_multiplication 倒数的乘积应等于乘积的倒数。
ABDKMATH-052 inv_test_identity 倒数的单位元性质。
ABDKMATH-053 inv_test_values 如果操作数大于一，则倒数结果应在范围 (0, 1) 内。
ABDKMATH-054 inv_test_sign 倒数结果应保持操作数的符号。
ABDKMATH-055 inv_test_zero 倒数边界情况：零的倒数应回退。
ABDKMATH-056 inv_test_maximum 倒数边界情况：最大值的倒数应接近于零。
ABDKMATH-057 inv_test_minimum 倒数边界情况：最小值的倒数应接近于零。
ABDKMATH-058 avg_test_values_in_range 平均值结果应在操作数之间。
ABDKMATH-059 avg_test_one_value 相同数字的两次平均值是该数字本身。
ABDKMATH-060 avg_test_operand_order 平均值结果不取决于操作数的顺序。
ABDKMATH-061 avg_test_maximum 平均值边界情况：最大值的两次平均值是最大值。
ABDKMATH-062 avg_test_minimum 平均值边界情况：最小值的两次平均值是最小值。
ABDKMATH-063 gavg_test_values_in_range 几何平均值结果应在操作数之间。
ABDKMATH-064 gavg_test_one_value 相同数字的两次几何平均值是该数字本身。
ABDKMATH-065 gavg_test_operand_order 几何平均值结果不取决于操作数的顺序。
ABDKMATH-066 gavg_test_maximum 几何平均值边界情况：最大值的两次平均值是最大值。
ABDKMATH-067 gavg_test_minimum 几何平均值边界情况：最小值的两次平均值是最小值。
ABDKMATH-068 pow_test_zero_exponent 零次幂应为一。
ABDKMATH-069 pow_test_zero_base 零的任何次幂应为零。
ABDKMATH-070 pow_test_one_exponent 一次幂应等于操作数。
ABDKMATH-071 pow_test_base_one 一的任何次幂应为一。
ABDKMATH-072 pow_test_product_same_base 同底数幂的乘积性质。
ABDKMATH-073 pow_test_power_of_an_exponentiation 幂的幂的性质。
ABDKMATH-074 pow_test_distributive 乘积的幂的分配律。
ABDKMATH-075 pow_test_values 幂的结果应根据指数的绝对值增加或减少（绝对值）。
ABDKMATH-076 pow_test_sign 幂的结果符号应根据指数符号更改。
ABDKMATH-077 pow_test_maximum_base 幂的边界情况：如果指数 > 1，则最大值的幂应回退。
ABDKMATH-078 pow_test_high_exponent 幂的边界情况：如果底数小且指数大，则结果应为零。
ABDKMATH-079 sqrt_test_inverse_mul 作为乘法的平方根倒数。
ABDKMATH-080 sqrt_test_inverse_pow 作为幂的平方根倒数。
ABDKMATH-081 sqrt_test_distributive 平方根对乘法的分配律。
ABDKMATH-082 sqrt_test_zero 平方根边界情况：零的平方根应为零。
ABDKMATH-083 sqrt_test_maximum 平方根边界情况：最大值的平方根不应回退。
ABDKMATH-084 sqrt_test_minimum 平方根边界情况：最小值的平方根应回退（负数）。
ABDKMATH-085 sqrt_test_negative 平方根边界情况：负值的平方根应回退。
ABDKMATH-086 log2_test_distributive_mul 以 2 为底的对数对乘法的分配律。
ABDKMATH-087 log2_test_power 幂的以 2 为底的对数。
ABDKMATH-088 log2_test_zero 以 2 为底的对数边界情况：零的对数应回退。
ABDKMATH-089 log2_test_maximum 以 2 为底的对数边界情况：最大值的对数不应回退。
ABDKMATH-090 log2_test_negative 以 2 为底的对数边界情况：负值的对数应回退。
ABDKMATH-091 ln_test_distributive_mul 自然对数对乘法的分配律。
ABDKMATH-092 ln_test_power 幂的自然对数。
ABDKMATH-093 ln_test_zero 自然对数边界情况：零的对数应回退。
ABDKMATH-094 ln_test_maximum 自然对数边界情况：最大值的对数不应回退。
ABDKMATH-095 ln_test_negative 自然对数边界情况：负值的对数应回退。
ABDKMATH-096 exp2_test_equivalence_pow 以 2 为底的指数应等于幂。
ABDKMATH-097 exp2_test_inverse 以 2 为底的指数反函数。
ABDKMATH-098 exp2_test_negative_exponent 具有负指数的以 2 为底的指数应等于倒数。
ABDKMATH-099 [exp2_test_zero](
  • 原文链接： github.com/crytic/proper...
  • 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ，好文好收益，欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
crytic
crytic
江湖只有他的大名，没有他的介绍。

crytic

如果觉得我的文章对您有用，请随意打赏。你的支持将鼓励我继续创作！