参考文档 / ZLIB × LEAN

证明变异

此页源文件快照 · 371fd62b1584eab7 · 对应提交的原文 ↗

例如，一个函数先检查写入边界，再写入字节；若删掉这个检查后，原证明仍被接受，就需要调查证明是否覆盖了这次访问。证明必须拒绝被验证函数中的故意错误。证明变异在临时副本中修改一个翻译后的函数，并要求失败发生在该函数的证明中。必须先确认未修改的证明通过，这一步称为正向基线。否则，“修改后失败”可能只是原版本来就无法检查。

这不同于 tests/selftest.sh 中的差分自测，后者要求执行比较发现变异。如果只有测试发现变异，可能暴露缺失的证明覆盖。证明拒绝变异说明它对变化敏感，但不证明变异改变了可观察行为，也不证明定理覆盖每种错误。审阅必须确认所需变异确实在允许输入上改变行为。

运行检查

在仓库根目录、已有预热 .lake 构建缓存时运行：

python3 scripts/verification.py mutants
bash tests/audit/proofmut.sh tests/audit/proofmut/adler32.tsv
bash tests/audit/proofmut.sh tests/audit/proofmut/crc32.tsv '^combine'

第一条命令构建项目，检查解析后的公开变异边界，重放原来的精确公开证明，并以严格模式运行模型列表和每个被引用的公开函数列表。其余命令运行单个旧列表，可按变异名称筛选。它们用于开发，不能替代最终验收。

列表执行器将工作区和预热缓存复制到临时目录，先构建未修改的指定证明模块，再对每个替换恰好应用一次，只构建指定模块。第一个报告的错误必须位于预期证明模块。原缓存保持不变。一次只运行一个变异。

判定	含义
`KILLED`	第一个错误位于预期证明模块。变异检查通过。
`SAME ok`	显式标为等价的变异仍能构建。应审阅等价理由。
`GAP (known)`	已记录的证明缺口在开发模式下存活。它不算覆盖，严格验收会失败。
`SURVIVED`	没有正当豁免的变异仍能构建。调查缺失覆盖或等价性。
`BAD MUTANT`	翻译或证明树以外的文件失败。修复变异。
`WRONG PLACE`	另一个证明先失败。不满足指定函数的检查。
`NO ERROR`	即使重试一次，构建失败仍没有可识别错误。未建立证明拒绝的证据。
`UNEXPECTED`	标为等价的变异失败。审阅标记和变异。
`NOT APPLIED`	替换文本没有恰好出现一次，或者内容未改变。更新变异。

被拒绝的变异若仍带过时的 gap: 标记，也会失败。缺口关闭后，通过经过审阅的审计更新移除该标记。严格模式强制执行正向基线，并拒绝已知缺口。跳过基线不能支持最终验收。

公开入口的要求

每个已有精确证明的公开入口都需要 tests/audit/public-mutants.json 中的记录。记录指定该函数翻译后主体的变异，并保持签名不变。解析器在不加载候选导入的情况下检查两个版本。修改另一个函数、只改规范、注入声明或标记的证明缺口都不算。

除重新构建指定证明模块外，公开检查还取出原来已登记的精确证明，只在其依赖闭包中替换变化的源码声明。全新内核重放必须接受原版并拒绝变异。无关定理的失败，或带额外前提的更强定理，都不足以满足要求。权威依据和锁定规则见防止取巧的规则。

列表格式

列表每个变异占一行，字段以制表符分隔。以 # 开头的行是注释。

NAME <TAB> FILE <TAB> OLD <TAB> NEW <TAB> PROOF_MODULES [<TAB> same:REASON | gap:REASON]

字段	含义
`FILE`	相对仓库根目录的翻译源码路径，例如 `ZlibF/Zlib/adler32.c.lean`。
`OLD`、`NEW`	替换文本。字面量 `\n` 表示换行；`OLD` 必须恰好出现一次。
`PROOF_MODULES`	`ZlibF/Proof` 下用逗号分隔的路径，不带 `.lean`，指明预期的函数证明。
可选标记	`same:` 解释等价性；`gap:` 仅为开发记录缺失覆盖。所需公开变异记录中两者都不允许。

有用的变异会删除检查或赋值，改变界限或比较，改变下标或移位，或返回错误结果。应选择已证明函数的不同部分。语法错误，或仅破坏源码相等性引理的变异，都不足以证明其执行契约的敏感性。

已提交的 tests/audit/proofmut/ 列表覆盖校验和、辅助函数、树、inflate、deflate 和解码表证明组。其他列表位于 tests/proof-mutants/ 和 tests/proofmut/。文件和公开映射决定精确范围；列表存在或历史结果都不证明相应 C 文件中的每个函数已被覆盖。

执行器设置

PROOFMUT_CACHE 选择预热缓存。PROOFMUT_TIMEOUT 设置每次构建的秒数，默认 3600。PROOFMUT_KEEP=1 保留临时副本；PROOFMUT_SHOWLOG=1 输出失败细节。PROOFMUT_BASELINE=0 仅为本地诊断跳过正向构建。PROOFMUT_STRICT=1 会覆盖这个跳过设置，并拒绝所有已知缺口。

最终验收会以严格模式运行三个支持目录中的每个列表。CI 还会执行公开／模型变异命令。建议中的工作流片段，或未执行的列表，都不能算检查通过。当前覆盖工作见进度。