caliperforge/euler-earn-invariants

# euler-earn-invariants 用于 Euler Earn allocator + vault 的有状态不变量测试框架 共享会计逻辑，针对真实的 Euler Earn 合约运行 （锁定 submodule，除了标准的 EVault strategy fixture 不使用任何 mock，Euler Earn 自己的测试套件已在使用该 fixture）。 初始版本中包含一个测试用例，以同源 纯净/植入孪生对的形式编码，对应 `euler-_xyz/euler-earn` 仓库的 `f07f6b1c5e1e` 提交 （这是 Pashov Audit Group 在 Euler Earn 安全审查中 M-01 漏洞的修复提交）。纯净孪生体在 256 次运行 x 深度 50 的有状态模糊测试中保持了所设定的不变量。植入孪生体是 相同的代码树，仅在 `PublicAllocator.sol` 上单块还原了 M-01 的修复；不变量测试套件在该测试分支上报告 `INVARIANT VIOLATED ` 且返回码非零。两个孪生体 都会在每次提交时运行 CI，因此该测试框架提供了持续的证明，表明 所设定的不变量确实能捕获它们声称能捕获的漏洞类别。此外， 植入孪生体已通过一组固定的 16 个种子进行认证 （见 [`docs/reachability.md`](docs/reachability.md)）：每个种子都因 不变量标记而失败，因此“植入孪生体被触发”是 该测试用例的确定性属性，而不是单次 随机游走的结果。**可达性已认证：是（按要求 16/16 全部失败）** 认证时间 2026-07-13。 ## 这是什么，以及它不是什么 - **这是**一个防御侧的回归测试 fixture，针对 Pashov Audit Group 在 Euler Earn 审查中标记为 M-01 的份额跟踪 漂移类漏洞，它在真实的 Euler Earn 合约之上被编码为有状态的多操作不变量，并作为纯净/植入孪生对提供。 - **这不是**审计、运行时守护程序，或用于 发现新漏洞类的引擎。M-01 类已经是公开的，并且已经在 引入的源代码中修复。纯净孪生体展示了修复后代码树的样貌； 植入孪生体是相同的代码树，仅还原了一行修复代码， 其存在只是为了让 CI 植入分支有一个同源的 回归测试可供捕获。 - 该测试套件并不声称它能提前发现 M-01；它只是 证明了所设定的不变量能捕获该修复所解决的漏洞类。 ## 测试用例 | 用例 | 合约 | 植入的规范回归 | 不变量标记 | 纯净分支 | 植入分支 | |---|---|---|---|---|---| | **M01** [详情](src/cases/m01-share-accounting-solvency/README.md) | `PublicAllocator`（真实子类，来自 `euler-xyz/euler-earn@f07f6b1c5e1e`） | 在 `PublicAllocator.sol` 第 120 行单块还原 M-01 修复： `IEulerEarn(vault).expectedSupplyAssets(id)` 被还原为 `id.maxWithdraw(vault)` | `INVARIANT VIOLATED m01_reallocation_movement_matches_request` 和 `INVARIANT VIOLATED m01_reallocation_flowcap_matches_movement` | 绿灯 | 红灯并附带标记 | 每个分支的形态（根据 `test/m01/` 中的不变量测试套件）： - 纯净孪生体：三个不变量（`m01_solvency`、 `m01_reallocation_movement_matches_request`、 `m01_reallocation_flowcap_matches_movement`）在针对四个 handler 原语（deposit、 directShareDeposit、reallocateToStrategy、reallocateFromStrategy）的有状态 模糊测试活动中成立。 一个确定性回归测试与 PAG 自己在同一提交中的 `testRellocateToWithDirectStrategySharesTransfer` 相呼应并通过。 - 植入孪生体：当模糊测试游走访问到可达的序列 `directShareDeposit -> reallocateFromStrategy` 时，`m01_reallocation_movement_matches_request` 和 `m01_reallocation_flowcap_matches_movement` 不变量就会失败；确定性 回归测试独立于种子触发相同的两个标记。 `m01_solvency` 依然成立（它是一个参考偿付能力不变量， 两个孪生体在构造上都满足该不变量）。 ## Pashov Audit Group 和 Euler Labs 的贡献 M-01 发现及其附带的测试（锁定提交处 `test/PublicAllocatorTest.sol` 中的 `testRellocateToWithDirectStrategySharesTransfer`）由 Pashov Audit Group 编写。该修复属于 Euler Labs 的提交 `f07f6b1c5e1e`（“M-01 fix, PAG audit”）。本仓库建立在 这两项贡献之上： ## 目录结构 - `src/cases/m01-share-accounting-solvency/{clean,planted}/PublicAllocator.sol` ，即孪生对。纯净孪生体是 Euler 修复提交处的文件， 仅针对此代码树的深度调整了其导入路径（六行 前缀重写，无逻辑更改）。植入孪生体是同一个 文件，但在第 120 行进行了单块还原。 - `test/m01/`，即不变量测试套件。`M01Base.t.sol` 继承自 Euler Earn 自己的 `IntegrationTest` fixture，因此 vault、EVC、permit2、 strategy 工厂和角色连线与 Euler Earn 自己的 测试套件所使用的完全一致。`M01Handler.sol` 暴露了四个模糊测试原语。 `M01SolvencyClean.t.sol` 和 `M01SolvencyPlanted.t.sol` 的区别仅在于它们部署了哪个孪生体的 `PublicAllocator`。 - `lib/euler-earn/`，锁定在 `f07f6b1c5e1e` 的 submodule，使用 `--recursive` 初始化，以获取传递依赖的 euler-vault-kit / EVC / permit2 / OpenZeppelin。 - `ci/{clean_leg.sh,planted_leg.sh}`，这两个 CI 分支。纯净分支 运行 `forge test --no-match-contract 'Planted$' -vv`，要求 rc=0， 并且要求输出中没有 `INVARIANT VIOLATED` 标记。植入 分支则相反：每个 `*Planted` 测试套件必须非零退出并 打印至少一个标记；这些标记会被复制到 GitHub job summary 中。 ## 工具链和锁定版本 - `solc` 精确到 0.8.26（与 Euler Earn 自己的 pragma 匹配）。 - `evm_version = "cancun"`（transient storage；EVC + euler-vault-kit 所需）。 - `via_ir = true`（与 Euler Earn 自己的 profile 匹配；如果不使用 via-IR，EVault 部署 路径会超出 24kb 的 runtime 限制）。 - `foundry-rs/foundry-toolchain@v1` 位于 `v1.7.1`。 - Invariant 活动：`runs = 256, depth = 50, fail_on_revert = false` （fuzzer 在探索 reallocation 空间时会访问许多良性的 revert 状态； `fail_on_revert = false` 可让活动专注于 守恒属性）。 ``` git clone --recursive cd euler-earn-invariants forge build bash ci/clean_leg.sh # rc=0, no markers bash ci/planted_leg.sh # rc=0, marker written to GITHUB_STEP_SUMMARY ``` ## 许可证 本仓库自己的代码（`lib/` 之外的所有内容）采用 GNU General Public License，version 2 or later 授权。有关完整文本，请参见 `LICENSE`， 有关各组件的归属说明，请参见 `NOTICE`。 Euler Earn 作为锁定的 git submodule 引入到 `lib/euler-earn` 中，位于其 GPL-2.0-or-later 分支（Euler Earn 采用双重许可 GPL-2.0-or-later OR BUSL-1.1；本仓库在 GPL 分支下使用）。位于 `src/cases/m01-share-accounting-solvency/clean/PublicAllocator.sol` 的纯净孪生体是 `euler-xyz/euler-earn/src/PublicAllocator.sol` 在提交 `f07f6b1c5e1e` 处的派生作品；植入孪生体是同一个 文件的单块还原。两者都带有与上游源代码相同的 `SPDX-License-Identifier: GPL-2.0-or-later` 头部标识。 ## AI 披露 CaliperForge 的创作堆栈是 AI 增强的。关于此仓库中哪些部分使用了 AI 以及限制它的审查机制，已在 `AI_DISCLOSURE.md` 中披露。CI 裁定和许可声明不涉及 AI。

标签：DeFi, Solidity, 不变量测试, 安全测试, 对称加密, 攻击性安全, 智能合约, 自动化审计