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