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流程和本地開發。雖然不能保證完全正確，但它為行為等價性提供了強有力的保障。