Back to Details

maintain-formal-verification-skill

Compare original and translation side by side

🇺🇸

Original

English
🇨🇳

Translation

Chinese

Maintain a formal verification skill

维护形式化验证 skill

A formal check proves a property of what it describes. When the code changes and the verification does not, the check can keep passing while it describes code that no longer exists. That pass is the dangerous case, because it looks like a proof. This skill is the upkeep loop for a verify skill that 
/create-formal-verification-skill
generated, or for any project-local skill that runs a model checker, prover, or code-level verifier against named code. The project-local skill handles a change that an agent makes while it uses that skill. This skill handles the changes that skipped it: merges, edits made without the skill, and drift that builds up across many commits.
形式化检查用于证明其所描述对象满足某项属性。当代码发生变化而验证未同步时，检查可能仍然通过，但它所描述的代码已经不存在。这种通过状态很危险，因为它看起来像一份证明。本 skill 是一套持续维护流程，用于维护由 
/create-formal-verification-skill
生成的 verify skill，或任何针对指定代码运行 model checker、prover 或 code-level verifier 的项目本地 skill。项目本地 skill 负责处理 Agent 在使用该 skill 时所做的变更。本 skill 则负责处理绕过该 skill 的变更：merges、未使用该 skill 所做的编辑，以及跨多个 commit 逐渐累积的漂移。

Outcomes

结果

Give each check one outcome, and say which:
  • in sync: no change since the last sync alters what the check describes, and the check passes.
  • updated: the code changed, the verification now describes the new code, and the check passes.
  • bug: the verification describes the current code, and the code breaks the property. This is a finding about the code. It is not drift.
  • blocked: the check could not be brought back in line or could not run. Say exactly why.
A check can be both updated and bug: the update makes the verification describe the code again, and then the property fails on it.
为每项检查给出一种结果，并明确说明：
  • in sync：自上次同步以来，没有改变检查所描述内容的变更，且检查通过。
  • updated：代码已发生变化，验证现在描述新的代码，且检查通过。
  • bug：验证描述的是当前代码，但代码违反了 property。这是关于代码的发现，不是漂移。
  • blocked：无法使检查重新保持一致，或无法运行检查。请准确说明原因。
一项检查可以同时为 updated 和 bug：更新使验证重新描述代码，但随后 property 在该代码上失败。

Edit scope

编辑范围

Edit only the verification: models, harnesses, property files, and the verify skill itself. Never edit product code during a run, unless the user asks you to. When a property fails on the current code, do not weaken the property or the model to make it pass. Report the failure.
仅可编辑验证内容：models、harnesses、property files 和 verify skill 本身。除非用户明确要求，否则运行期间绝不编辑产品代码。当 property 在当前代码上失败时，不要通过削弱 property 或 model 来使其通过。应报告该失败。

Pass

执行流程

  1. Find the checks. A verify skill has no fixed name, so find it by what it does: a project skill that runs a model checker, a prover, or another verifier against named code. Read each one you find, or the one the user named. For each check, collect the property, the code it covers, the bounds and assumptions, the command that runs it, and the commit where it was last confirmed to describe the code. If no verify skill exists, stop and point at 
    /create-formal-verification-skill
    . If the skill does not record a sync commit, use the last commit that changed the verification files, and say that you did.
  2. Run it as it is. Run each check once before you change anything, and record the result. A pass here does not tell you that the code is correct. It tells you that the old description still holds. A failure here can be drift or a bug. Do not decide which until step 5.
  3. Read every change to covered code. Diff the covered files from the sync commit to the current commit, and read each commit message. Also look for code that moved: a covered function that is renamed, split, or moved to another file is still covered code. Also look for new code that touches the state that a check guards, such as a new function that writes the same fields. For each change, decide which of these it is:
    • No effect. The change does not alter anything the verification describes, such as formatting, comments, or code paths that the verification does not cover. Check this against the model or harness, not against the commit message.
    • The verification no longer describes the code. A step that was one indivisible action is now two, a branch was added or removed, a check moved, a new path reaches the guarded state, or a value now has a different range. The model or harness must change.
    • The promise changed on purpose. The change alters what the code promises, and evidence in the change says that this is intended: the doc comment, the tests, the changelog, or the commit message. The property must change, and you must cite that evidence.
    • The promise may be broken. The code changed, and no evidence says that the promise changed. Treat a failure that follows as a bug candidate.
  4. Update from the code, not from the result. Change the model or harness so that each changed part again points to code that a reviewer can open, and keep one indivisible step in the code as one step in the verification. Write the update from the code before you rerun, and do not shape it by what makes the check pass. Change a property only for a promise that changed on purpose. Write down the old wording, the new wording, and the evidence. Keep the bounds unless the change makes them wrong. If you must reduce a bound, say so in the report.
  5. Rerun and judge each result.
    • Pass: the check can now pass on a description that has lost the ability to fail. Break the new code the way the property guards against, such as removing a new check or reordering a new step, and confirm that the check catches it. Then drop the break.
    • Fail: replay the counterexample against the real code, step by step. If a step cannot happen in the code, the verification is wrong. Fix the verification, and say what was wrong. If every step can happen, it is a bug. Name the commit that introduced it, tell the counterexample as a sequence of steps in the code's own words, and state the harm in one sentence. If a cheap test or reproduction against the real code shows the bug, add it to the report as evidence. Do not commit it to the product code.
  6. Update the verify skill. Update the code that each check covers, the commands, the bounds, the assumptions, and the sync commit. Set the sync commit to the commit that you checked. Do not move the sync commit for a blocked check, and say so in the report. Then follow the verify skill once as the next agent would, so that you know its steps still run.
  1. 查找检查。 verify skill 的名称并不固定，因此应根据其功能来查找：它是针对指定代码运行 model checker、prover 或其他 verifier 的项目 skill。读取每个找到的 skill，或用户指定的 skill。对于每项检查，收集 property、覆盖的代码、边界与假设、运行命令，以及最后一次确认其准确描述代码的 commit。如果不存在 verify skill，则停止并指向 
    /create-formal-verification-skill
    。如果该 skill 未记录同步 commit，则使用最后修改验证文件的 commit，并说明你采用了这一做法。
  2. 按原样运行。 修改任何内容之前，先将每项检查运行一次并记录结果。这里的通过并不能说明代码正确；它只说明旧描述仍然成立。这里的失败可能是漂移，也可能是 bug。在第 5 步之前不要判断属于哪一种。
  3. 读取覆盖代码的所有变更。 从同步 commit 到当前 commit 对覆盖文件进行 diff，并阅读每条 commit message。还要留意移动过的代码：被重命名、拆分或移到另一个文件的受覆盖函数，仍属于覆盖代码。还要留意触及检查所保护状态的新代码，例如写入相同字段的新函数。对于每项变更，判断其属于以下哪一种：
    • 无影响。 变更没有改变验证所描述的任何内容，例如格式调整、注释，或验证未覆盖的代码路径。应对照 model 或 harness 判断，而不是依据 commit message。
    • 验证不再描述代码。 原本一个不可分割的动作现在变成了两个动作，增加或删除了一个分支，检查发生了移动，新路径可以到达受保护状态，或某个值现在具有不同范围。model 或 harness 必须随之更改。
    • 承诺有意变更。 变更改变了代码所作出的承诺，并且变更中的证据表明这是有意为之，例如 doc comment、tests、changelog 或 commit message。property 必须更改，并且必须引用该证据。
    • 承诺可能已被破坏。 代码发生了变化，但没有证据表明承诺发生了变化。将由此引发的失败视为 bug 候选。
  4. 根据代码而非结果进行更新。 修改 model 或 harness，使每个发生变化的验证部分再次指向 reviewer 能够打开的代码，并让代码中的一个不可分割步骤在验证中仍对应一个步骤。重新运行前，先根据代码编写更新，不要根据什么能让检查通过来调整更新。只有在承诺有意变更时才修改 property。记录旧措辞、新措辞和证据。除非变更使边界变得不正确，否则保留原有边界。如果必须缩小边界，要在报告中说明。
  5. 重新运行并判断每项结果。
    • 通过：检查现在能够通过，但当前描述可能已经失去发现失败的能力。像 property 所防范的那样破坏新代码，例如移除新增检查，或调换新增步骤的顺序，并确认检查能够捕获该破坏。随后移除这些破坏性改动。
    • 失败：针对真实代码逐步重放反例。如果某一步在代码中不可能发生，则验证有误。修正验证，并说明具体问题。如果每一步都可能发生，则它是 bug。指出引入该 bug 的 commit，用代码自身的措辞将反例表述为一系列步骤，并在一句话中说明危害。如果一项成本较低的测试或针对真实代码的复现能够展示该 bug，将其作为证据加入报告。不要将该复现提交到产品代码中。
  6. 更新 verify skill。 更新 verify skill 中记录的每项检查所覆盖的代码、命令、边界、假设和同步 commit。将同步 commit 设为你所检查的 commit。对于 blocked 的检查，不要移动同步 commit，并在报告中说明。随后按照下一个 Agent 会采用的方式执行一次 verify skill，以确认其步骤仍可运行。

Report

报告

Tell the user, for each check:
  • the outcome, and the commits that you read;
  • what changed in the verification and why, with a short reason for each change: the code changed shape, or the promise changed on purpose (with the evidence);
  • the rerun result, and the break that you used to show the updated check can still fail;
  • each bug, in plain words: the counterexample as steps in the code's words, the harm, and the commit that introduced it;
  • what the verification still does not cover, including new code that it should cover and does not.
Say outright which failures were drift in the verification and which were bugs in the code. For a check that passed before you updated it and fails after, say that the old pass was on a stale description.
Put the verification updates in a change of their own, separate from any product fix.
针对每项检查，向用户说明：
  • 结果，以及你阅读过的 commits；
  • 验证中发生了哪些更改及其原因，并为每项更改给出一个简短理由：代码结构发生了变化，或承诺有意变更（并附上证据）；
  • 重新运行的结果，以及你用来证明更新后的检查仍能发现失败的破坏操作；
  • 每个 bug 的通俗说明：用代码自身的措辞将反例表述为一系列步骤，说明危害，并指出引入该问题的 commit；
  • 验证仍未覆盖的内容，包括应该覆盖但目前未覆盖的新代码。
明确指出哪些失败属于验证漂移，哪些属于代码 bug。对于更新前通过、更新后失败的检查，要说明先前的通过建立在过时的描述上。
将验证更新放入独立变更中，与任何产品修复分开。