Equiv：检查AI重构是否改变了代码行为

随着AI生成代码的普及，确保AI重构不引入隐藏的行为变化变得至关重要。Equiv正是为此而设计的工具——它通过确定性测试来验证函数在重构后是否保持行为等价。

工作原理

Equiv的核心机制是：针对指定的函数，在其原有版本和修改后的版本上运行相同的确定性生成的输入，然后比较输出结果。如果输出不同，工具会提供导致差异的具体输入；如果相同，则会生成一份可复现的签名收据。这份收据可以在任何机器上重新验证，而无需依赖任何模型的判断。

所有核心计算都在Rust中完成，从固定种子生成输入并得出判决。语言运行时仅作为求值器使用，不参与任何影响收据的决策。收据在不同主机上完全一致，并可以使用本地ed25519密钥或Sigstore无密钥签名（OIDC）进行签署。后者将签名与可验证的CI身份绑定，无需存储密钥。

快速入门：PR门控

用户可以在仓库根目录创建清单文件（.equiv-review），列出需要保持行为不变的函数及其参数类型。格式为“文件路径 : 函数名 : 参数类型”，例如“src/math.py : total : int”。然后在.github/workflows/下添加工作流文件，集成Equiv Action。当PR提交时，Action会自动检查清单中的所有函数，并在PR下评论结果。如果发现行为变化，PR检查将失败，并给出导致差异的具体输入。

清单示例：

src/math.py : total : int
src/utils.py : process : str, list[int]

工作流文件示例：

on: pull_request
permissions: { contents: read, pull-requests: write, id-token: write }
jobs:
  review:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
        with: { fetch-depth: 0 }
      - uses: Neelagiri65/[email protected]
        with: { keyless: "true" }

注意要固定到发行标签@v0.1.0而非@main，以确保运行的可复现性。

命令行接口

除了GitHub集成，Equiv也提供了命令行接口。使用以下命令安装：

curl --proto '=https' --tlsv1.2 -LsSf https://github.com/Neelagiri65/equiv/releases/latest/download/equiv-cli-installer.sh | sh

然后使用equiv review candidate.py reference.py比较两个文件中的函数，或使用equiv verify-receipt验证收据。

退出码含义：0表示等价，1表示行为不同并打印反例，2表示无法检查。

范围与限制

Equiv进行的是有界随机测试，而非穷举验证。通过测试并不代表完全正确，它可能遗漏某些未生成的输入下的边缘情况。此外，该工具不检查意图、架构或安全性，也不适用于没有参考版本的新功能。通过结果仅表示行为在测试输入上得到保留，不意味着修改是正确的。

目前支持的参数类型包括int、str和list[int]。未来可能会扩展更多类型。

技术细节

输入生成和判决在Rust中从固定种子计算得出。语言运行时仅作为求值器。收据在所有主机上相同。收据可以使用本地ed25519密钥或Sigstore无密钥签名（OIDC）签署。无密钥路径将签名绑定到可验证的CI身份，而不是存储的秘密。该工具是单个静态二进制文件，无运行时依赖，预编译支持macOS、Linux和Windows。

Equiv采用Apache-2.0许可证。项目包含Rust工作区（equiv-core, equiv-engine, equiv-review, equiv-cli），以及文档（docs/signing-model.md, docs/RELEASING.md）。

总结

在AI编写代码日益普遍的今天，Equiv提供了一种确定性的验证方法，确保代码重构不改变原有行为。它通过签名收据提供可复现的验证，适用于CI/CD流程和本地开发。虽然不能保证完全正确，但它为行为等价性提供了强有力的保障。