divyangchauhan/kleros-v2-invariant-tests

# Kleros V2 不变性测试 [](https://github.com/divyangchauhan/kleros-v2-invariant-tests/actions/workflows/tests.yml) 用于 Kleros V2 仲裁合约的 Foundry、Halmos 和 Echidna 测试套件。该仓库将不变性模糊测试、符号/形式化属性、差分模型以及 Echidna 状态化测试工具打包到了一个小巧、可复现的公开项目中。 这不是一份审计报告，也不声明具备审计范围。这是一个专注的验证测试包：上游合约保持未修改状态，本地代码仅限于测试、测试工具、fixture、配置和文档。 ## 核心亮点 - Foundry 不变性测试套件，涵盖质押、争议生命周期和抽签树行为。 - 兼容 Halmos 的符号测试，用于验证算术、奖励分配、阶段转换和延迟质押队列逻辑。 - 差分、跨合约和经济模糊模型，用于参考检查和激励推理。 - Echidna 状态化测试工具，驱动质押、解除质押、争议创建、抽签、投票、执行和延迟质押处理。 - 针对测试发现的 133 个已验证正向属性和 4 个问题的详细文档。 ## 测试范围 | 领域 | 工具 | 文件 | 属性 | | --- | --- | --- | --- | | 质押不变性 | Foundry 不变性模糊测试 | `test/foundry/KlerosCore_StakingInvariant.t.sol` | PNK 守恒、质押记账、锁定覆盖范围、延迟质押游标边界、法庭父级有效性 | | 争议生命周期不变性 | Foundry 不变性模糊测试 | `test/foundry/KlerosCore_DisputeLifecycleInvariant.t.sol` | 抽签/投票/执行生命周期边界、奖励和费用上限、周期有效性、处于风险中的 PNK (PNK-at-stake) 一致性 | | 抽签树不变性 | Foundry 不变性模糊测试 | `test/foundry/KlerosCore_SortitionTreeInvariant.t.sol` | 父/子树一致性、法庭列表完整性、争议工具包一致性 | | 算术和状态机属性 | Halmos / Foundry 风格的符号测试 | `test/halmos/*.t.sol` | 惩罚边界、锁定/解锁算术、奖励分配、阶段转换、延迟质押索引完整性 | | 差分、跨合约和经济模型 | Foundry 模糊测试 | `test/foundry/fuzz/*.t.sol` | 参考模型一致性、跨合约守恒、激励和舍入属性 | | 状态化属性测试工具 | Echidna | `test/echidna/EchidnaStaking.sol` | 通过公开的 `echidna_` 属性执行长时间运行的质押和抽签活动 | Kleros V2 子模块固定在以下提交： ``` 595a219e50b38aa20fabcfeda31d4ac2c51a780e ``` ## 测试发现 由测试套件发现的最重要问题如下： | 发现 | 严重程度 | 来源 | | --- | --- | --- | | 多法庭惩罚后的陈旧抽签树值 | Medium | `INV-10`, `INV-ST4`, `echidna_courtStakeSumConsistency` | | 父法庭树值可能低于子法庭树值 | Medium | `INV-ST1`, `echidna_parentGeChildTreeValue` | | `lockedPnk` 可能超过 `stakedPnk` 及核心 PNK 余额 | Low | `INV-2`, `FV-LU8`, `echidna_coreCoversLocked` | | 独立的整数除法可能留下最多 1 wei 的锁定余额 | Info | `FV-LU11`, `DIFF-5` | 有关更完整的属性列表和基本原理，请参阅 [docs/findings.md](docs/findings.md) 和 [docs/invariants.md](docs/invariants.md)。 ## 快速开始 ``` git clone --recurse-submodules https://github.com/divyangchauhan/kleros-v2-invariant-tests.git cd kleros-v2-invariant-tests npm install forge build npm test ``` 如果在克隆时未包含子模块： ``` git submodule update --init --recursive ``` 安装验证工具： ``` curl -L https://foundry.paradigm.xyz | bash foundryup pip install halmos ``` 对于 Echidna，可以安装原生二进制文件，或者通过 `scripts/run-echidna.sh` 使用 Docker。 ## 命令 运行通过的 Forge 冒烟测试套件： ``` npm test ``` 使用 Halmos 运行符号/形式化测试套件： ``` halmos --match-contract 'FV_.*' --function test ``` Halmos 的求解时间取决于本地求解器和超时设置。如果完整运行在算术密集型用例中发生超时，可以使用 `--match-contract FV_DelayedStakes` 运行单个套件，或者增加求解器超时时间。 运行不变性测试套件以重现已记录的问题： ``` forge test --match-path 'test/foundry/KlerosCore_*Invariant.t.sol' -vv ``` 某些不变性测试套件有意包含了上述发现中已知会失败的属性，因此在上述上游行为被更改之前，预期不变性命令会返回失败。 运行 Echidna 质押活动： ``` ./scripts/run-echidna.sh ``` 如需快速的 Docker 冒烟测试： ``` ./scripts/run-echidna.sh --test-limit 1 --seq-len 1 ``` ## 目录结构 ``` . |-- foundry.toml |-- remappings.txt |-- echidna.yaml |-- lib/ | `-- kleros-v2/ # upstream Kleros V2 submodule, unmodified |-- test/ | |-- echidna/ # Echidna harness and juror proxy | |-- fixtures/ # local test-only mock helpers | |-- foundry/ # invariant and fuzz tests | `-- halmos/ # symbolic/formal property tests |-- docs/ | |-- findings.md | `-- invariants.md `-- scripts/ `-- run-echidna.sh ``` ## 与上游代码库的关系 这些测试套件针对上文提到的已固定的 Kleros V2 提交版本。本仓库中的上游合约未作修改。额外的 `test/fixtures/KlerosCoreMock.sol` 文件是一个本地测试 fixture，它通过不变性所需的只读辅助函数扩展了 Kleros 的 mock。 ## 许可证 测试套件、测试工具、fixture mock、文档和配置：MIT，版权所有 (c) 2026 Divyang Chauhan。 `lib/kleros-v2` 下的合约：MIT，版权所有 Kleros。请参阅 `lib/kleros-v2/LICENSE`。

标签：Solidity, 代码质量检查, 区块链, 形式化验证, 智能合约, 暗色界面, 请求拦截