caliperforge/bsc-invariants

# bsc-invariants (v0.0.2，第 1 + 2 周) **状态。** BNB grant build-to-win 的第 1 + 2 周。PancakeSwap v3 invariants P-1 (FeeGrowthGlobalMonotonicity)、P-2 (TickInBounds)、P-3 (SqrtPriceX96InBounds)、P-4 (LiquidityEventConsistency) 和 P-5 (FeeGrowthOutsideConsistency，仅增量守恒形式) 已合入代码树，并在 `forge test` 下通过 (31 / 31 全绿)。P-1 植入式 CI 对也已落地，并在植入分支上确定性地触发 `INVARIANT VIOLATED`。 P-6、P-7、P-2 / P-3 的植入对、wrap-around P-5 变体以及 BSC-mainnet fork 测试属于第 3 周的工作，目前 不在代码树中。Venus 和 Stargate harness 属于 M2 / M3 阶段，并且 **尚未开始**。本 README 仅声明在 HEAD 发布时实际交付的内容。 ## 本库是什么 **M-status 附录 (第 2 周，HEAD)。** P-1 植入 bug 对已 落地：`invariants/planted/PancakeV3FeeGrowth.planted.t.sol` 会确定性地触发 `INVARIANT VIOLATED feeGrowth_neverDecreases`，并且 `forge test` 在植入分支上以非零状态退出。P-2 和 P-3 植入对 属于第 3 周的工作；参见 `SCOPE.md` §1。 ## 本库不声明什么 - **非审计。** 针对协议合约运行本库 fork 的 CI 通过记录，并不能证明该协议是安全的。该 库仅能捕获 invariants 所编码的 bug 类别；残余的 攻击面由协议自身承担。 - **非 runtime 监控。** 这些属性是部署前的 CI 门控。 - **尚未实现广覆盖。** 在 v0.0.2 阶段，代码树中仅有 PancakeSwap v3 包含任何 invariants 。Venus 和 Stargate 属于 M2 / M3 阶段，且明确 未开始。 - **非 PancakeSwap 生产源码的 fork。** `src/PancakeV3FeeAccountingRef.sol` 下的参考 合约是一个与所测 invariants 对应的同源 最小化孪生体。在重现 v3-core 数学 常量的地方 (`src/lib/TickMath.sol`)，上游 归属说明位于 `NOTICE` 中。 ## v0.0.2 中的 Invariants (产品) 五个 invariants 以及一对植入式 CI 对在 PancakeSwap v3 池边界处落地。每一行将 `invariants/` 中的属性映射到 它所测试的上游 v3 语句。完整文本位于 [`docs/invariants.md`](docs/invariants.md)；代码中的 NatSpec 是 精确语句的唯一事实来源。 | ID | Invariant | 被测参考 | 属性束 | |---|---|---|---| | **P-1** | FeeGrowthGlobalMonotonicity | [`PancakeV3FeeAccountingRef.sol`](src/PancakeV3FeeAccountingRef.sol) | [`PancakeV3FeeGrowth.t.sol`](invariants/PancakeV3FeeGrowth.t.sol) | | **P-2** | TickInBounds (MIN_TICK ≤ tick ≤ MAX_TICK) | [`PancakeV3FeeAccountingRef.sol`](src/PancakeV3FeeAccountingRef.sol) | [`PancakeV3TickBounds.t.sol`](invariants/PancakeV3TickBounds.t.sol) | | **P-3** | SqrtPriceX96InBounds (MIN_SQRT_RATIO ≤ sqrtPriceX96 < MAX_SQRT_RATIO) | [`PancakeV3FeeAccountingRef.sol`](src/PancakeV3FeeAccountingRef.sol) | [`PancakeV3TickBounds.t.sol`](invariants/PancakeV3TickBounds.t.sol) | | **P-4** | LiquidityEventConsistency (mint / burn 对范围内的头寸精确更新 ±Δ 活跃流动性；范围外保持不变) | [`PancakeV3LiquidityEventsRef.sol`](src/PancakeV3LiquidityEventsRef.sol) | [`PancakeV3LiquidityEvents.t.sol`](invariants/PancakeV3LiquidityEvents.t.sol) | | **P-5** | FeeGrowthOutsideConsistency (每个已初始化 tick 的 `feeGrowthOutside ≤ feeGrowthGlobal`，仅增量形式) | [`PancakeV3FeeGrowthOutsideRef.sol`](src/PancakeV3FeeGrowthOutsideRef.sol) | [`PancakeV3FeeGrowthOutside.t.sol`](invariants/PancakeV3FeeGrowthOutside.t.sol) | | **P-1 植入** | 植入式 CI 对 (植入分支触发 `INVARIANT VIOLATED feeGrowth_neverDecreases`，非零退出) | 内联 `BrokenPancakeV3FeeAccountingRef` (hyperevm-safety 约定) | [`PancakeV3FeeGrowth.planted.t.sol`](invariants/planted/PancakeV3FeeGrowth.planted.t.sol) | P-1 是最高优先级的 invariant。它所捕获的 bug 类别， 即在任意非零 swap 下减少的 fee-growth accounting，正是 Uniswap-v3-fork 分叉项目在错误移植 `feeGrowthGlobalX128 += FullMath.mulDiv(...)` 增量时的确切故障模式：这是 分叉项目在重构池时引入的典型 accounting bug。 PancakeSwap v3 invariants 及其已覆盖（和未覆盖）的层面已 编目在 [`SCOPE.md`](SCOPE.md) 中。 ## 仓库布局 ``` experiments/bsc-invariants/ README.md # this file LICENSE # Apache-2.0 (born-with-license rule) NOTICE # upstream attributions AI_DISCLOSURE.md # AI-touched surfaces + review discipline SECURITY.md # responsible disclosure SCOPE.md # protocols x invariants x status (M1/M2/M3) RUN_SUMMARY.md # Weeks 1+2 run summary (what shipped vs deferred) foundry.toml # Foundry config (solc 0.8.28, CI fuzz budgets, [fmt] pin) remappings.txt # forge-std remapping .gitignore .github/ workflows/ci.yml # path-gated CI: each M2/M3 job flips on file presence actions/foundry-setup/ # composite action: pinned Foundry + forge-std install src/ lib/TickMath.sol # v3 tick/sqrtPriceX96 constants (attributed in NOTICE) PancakeV3FeeAccountingRef.sol # minimal v3 reference for P-1/P-2/P-3 PancakeV3FeeGrowthOutsideRef.sol # per-tick feeGrowthOutside reference for P-5 PancakeV3LiquidityEventsRef.sol # mint/burn + active-liquidity reference for P-4 invariants/ PancakeV3FeeGrowth.t.sol # P-1: fee-growth global monotonicity PancakeV3TickBounds.t.sol # P-2 + P-3: tick + sqrtPriceX96 bounds PancakeV3LiquidityEvents.t.sol # P-4: liquidity-event consistency PancakeV3FeeGrowthOutside.t.sol # P-5: per-tick feeGrowthOutside conservation mocks/ # M2/Week-3: Recon Chimera CryticTester scaffold lands here planted/ PancakeV3FeeGrowth.planted.t.sol # P-1 planted twin (Week 2, LANDED) docs/ invariants.md # prose invariant descriptions + upstream citations receipts/ forge-build-*.log # forge build receipts (Weeks 1+2) forge-test-*.log # forge test receipts (Weeks 1+2) planted_demo/p1-*.log # P-1 planted-twin clean + planted leg receipts ``` ## 本地运行 ``` # 安装 Foundry (https://book.getfoundry.sh/getting-started/installation) curl -L https://foundry.paradigm.xyz | bash && foundryup # 从这个目录开始 forge install foundry-rs/forge-std@v1.9.4 --no-commit # pinned per CI forge build forge test -vv ``` 预期结果：全部五个 invariants (P-1、P-2、P-3、P-4、P-5) 加上 P-1 植入式对在干净的参考下通过 (31 / 31 全绿； 植入分支以非零状态退出并触发 `INVARIANT VIOLATED`)。 Fuzz 预算较小 (1000 次运行) 以便快速本地迭代；CI `nightly` 工作流 (M2/第 3 周) 将运行更长的测试活动。 **格式化。** `forge fmt` 样式固定在 `foundry.toml` 的 `[fmt]` 下 (行长 120，全行多行函数头)，以便 参考合约和测试中手动调整的多行参数布局 在重新格式化时得以保留。 ## CI `.github/workflows/ci.yml` 会针对干净的参考运行 `forge build` 和 `forge test`。每个 M2 / M3 PancakeSwap-extension 作业以及每个 M2 Venus / M3 Stargate 作业都是 **path-gated** (路径门控)：该作业会检查 文件系统并选择运行（当 wiring 文件存在时）或输出一条 GitHub Actions `::notice::` 日志说明被推迟的原因。这 保持了 CI 图在各里程碑间的稳定；一个新的 harness 会在 wiring 文件落地的瞬间，将其自身的作业从 `deferred` 翻转为 `real-work-green`。 当前 CI 状态（源自运行日志，而非徽章）记录 在 [`RUN_SUMMARY.md`](RUN_SUMMARY.md) §3 中。 ## 路线图 (尚未合入代码树；参见 SCOPE.md) - **M2 / 第 3 周，PancakeSwap v3 剩余部分。** P-6 protocol-fee 计提 边界，P-7 oracle observation cardinality monotonicity，P-2 + P-3 的植入式 CI 对，P-5 的 wrap-around 变体，在固定区块上针对真实 PancakeSwap v3 池的第一个 BSC-mainnet fork 测试，以及 Recon Chimera `Properties.sol` + `CryticTester.sol` 脚手架。 - **M2，Venus 借贷 invariants。** Account-liquidity 正确性， collateral-factor 边界，liquidation-incentive monotonicity，XVS reward-accrual 边界（即 2021 年 XVS-collateral 事件背后的 bug 类别）。 - **M3，Stargate-on-BSC 跨链桥 invariants。** 跨 chain-id 对的 Pool delta accounting ，LD/SD 转换安全性，credit-tracking monotonicity。 - **M3，BNB Chain AI agent-registry harness。** 针对 2026 年技术路线图 agent registry 规范的 Invariant + 可验证能力测试 harness （取决于该规范的公开落地）。 ## 许可证 Apache License 2.0；参见 [`LICENSE`](LICENSE) 和 [`NOTICE`](NOTICE)。 ## 联系方式 CaliperForge: michael@caliperforge.com, team@caliperforge.com.

标签：BSC, DeFi, Foundry, 区块链, 形式化验证, 智能合约, 测试框架