logic-review

Logic-Lens — 逻辑审查

输出骨架契约

下游评分器（scripts/grade-iteration.py）和其他 Logic-Lens 技能会通过子字符串匹配来读取此报告，匹配的字面标记定义在 ../_shared/common.md §1（标题映射）、§2（必填字段标签和 Logic Score）以及 ../_shared/report-template.md（骨架）中。改写这些标记——哪怕换成对人类来说意思相近的同义词——也会破坏契约，无论分析质量如何。

语言决定标记集，而非结构。 下面的两个模板是同一契约的两种语言版本。在中文报告中输出英文标签，同样属于违反契约，和改写标签一样——这违反了 common.md §1（最高优先级），评分结果也同样不合格。先检测用户使用的语言，然后根据 §1 的标题映射，用该语言对应的列填写骨架。

基准测试中观察到的三种失败模式，值得在一般规则之外特别指出：

• 替换字段标签时，替代形式未包含必需的子字符串——将 Premises / 前提 替换为 前置条件构建 / 前置条件（eval-201），或将 Divergence / 偏差 替换为 根因 / 核心缺陷 / 结论（eval-252）。这些替换对人类来说意思通顺，也可能出现在章节标题或表格列中，但替代词不包含必需的子字符串，因此评分器和跨技能使用方会认为文档完全缺少该字段。请使用 common.md §1 中的字面标记；仍可在其旁添加描述性副标题。
• 将已确认的 L 代码问题降级为 ### 附加观察（非 Finding） / ### Additional observation——如果 Premises→Trace→Divergence 成立，该问题就必须放在 ## Findings（中文为 ## 发现）中，并包含五个字面字段，即使严重级别为 Suggestion 也不例外。这是 eval-279（quicksort L4）在 Sonnet 运行中反复失败的原因之一。
• 完全省略 Divergence: / 偏差： 字段——这是最常见的失败模式。许多输出正确分析了 Bug，却把偏差写成散文、表格单元格中的内容，或放在 根因、故障点、核心问题、缺陷等标题下。Divergence: 字段专门用于标记“实际行为偏离前提的地方”。它不是可选项，也没有可接受的同义词。对于无 Bug 的发现，请使用 Divergence: None — [why the premise holds]（中文为 偏差：无——[原因]）。

格式正确的发现——请用作模板：

### 🔴 Critical
**[L4] — Mutation during iteration skips elements**
Premises: `users` is `list[User]` passed by reference; `list.remove()` shifts subsequent elements left; the `for` iterator advances by index.
Trace: [1] index=0, user is inactive → `remove()` shifts list. [2] Iterator advances to index 1, which now holds the element originally at index 2 — the original index-1 element is skipped. Rebuttal check: PASSED — no defense found.
Divergence: `remove_inactive([inactive₁, inactive₂, active])` returns `[inactive₂, active]` (2 elements) instead of `[active]` (1 element) — the second inactive user is never visited.
Trigger: `remove_inactive([User(False), User(False), User(True)])` → expected 1, actual 2.
Remedy: Replace loop body with `return [u for u in users if u.is_active]`. Dry-run: ✅ divergence eliminated.

每个发现块都必须包含全部五个字面标签（Premises: / Trace: / Divergence: / Trigger: / Remedy: 或 前提： / 追踪： / 偏差： / 触发： / 修复：），并以这些标签作为行首前缀。章节标题（### Premises、## Execution Trace）不满足此要求——这些标签必须出现在发现块内部。

无 Bug 情况：输出 ## Findings（中文为 ## 发现），并包含一个使用全部五个字段标签的发现块，其中 Divergence: None — [why the premise holds]。此格式为必需，可同时满足评分和审计要求。

下面的示例特意以中文展示，以具体说明本地化后的标记集——它与上面的英文模板使用完全相同的骨架。对于英文审查，请使用英文标签；结构不变。

### ✅ 无 Bug
**[无 Bug] — defer 保证所有退出路径都会解锁**
前提：`mu.Lock()` 在第 12 行获取；`defer mu.Unlock()` 位于第 13 行（在任何条件分支或提前返回之前）。
追踪：[1] `defer` 在 `Lock()` 之后立即注册。[2] Go 规范保证 deferred 调用在所有函数退出路径上执行（return、panic、提前返回）。[3] Lock 与 defer 注册之间无条件分支。
偏差：无——`defer mu.Unlock()` 无条件置于加锁之后，保证每条退出路径都会释放，不存在锁泄漏。
触发：N/A（无 bug 可复现）。
修复：N/A（代码本身正确）。

设置

按照 ../_shared/common.md §13 使用延迟加载：

1. 仅阅读 ../_shared/common.md 中关于语言、Iron Law、Logic Score、范围管理、修复规范、配置字段和加载预算的内容。
2. 到达相应步骤时，只阅读 logic-review-guide.md 中相关的步骤。
3. 在当前步骤需要时，按需加载 ../_shared/logic-risks.md、../_shared/semiformal-guide.md、../_shared/semiformal-checklist.md 和 ../_shared/report-template.md。

流程

步骤 0. 语言与范围路由。 根据 common.md §1 检测用户使用的语言；以下所有标签和标题都必须使用该语言。确认范围是一个文件或一个函数——如果用户指向一个目录，则切换到 logic-health；如果用户描述的是已确认的故障，则切换到 logic-locate；如果涉及两个版本，则切换到 logic-diff。

步骤 1. 确定所声称的行为和审查入口（指南步骤 1）——用一句话描述代码应该执行的操作，然后选出要追踪的具体入口函数。如果文件超出 common.md §9 的限制，请说明选定的子集及原因。

步骤 2. 构建前提（指南步骤 2）——参照 semiformal-checklist.md 中的前提构建检查清单；如果被审查函数依赖另一个本地函数，则包含调用方/被调用方契约。

步骤 3. 构建风险路径清单（指南步骤 3）——在撰写问题之前，枚举 L1–L9 中可能存在的错误路径。将保留的每条路径标记为 A 类（不言自明）或 B 类（依赖不变量）。不要在成功路径上止步。分配任何 L 代码之前，请阅读 logic-risks.md 快速辨析表——其中列出了常见的错误分类。L4 优先检查： 是否有函数会修改其输入并返回同一对象？L7 优先检查： 是否有共享状态在没有显式同步的情况下，跨 await/yield/线程边界被访问？L4 与 L7 的辨析： 任何涉及多个执行上下文（线程 / goroutine / await / yield）的状态访问都属于 L7，绝不属于 L4——包括协程在 await 处交错执行的单线程 asyncio。L4 仅适用于单一上下文中的别名问题（可变默认值、原地修改陷阱、迭代期间修改）。L4 要求根因是对共享/别名状态的实际修改——变量作用域问题（const/let 可见性、构造函数作用域）属于 L1，查询模式低效问题（N+1）属于 L3。

L1 与 L6 的辨析： 如果根因是名称/标识符解析到了不同于开发者预期的定义（导入遮蔽、模块常量查找、原型链、构造函数作用域内的 const/let 对方法不可见），则属于 L1，即使症状是缺少方法的错误或返回值错误——只有在名称解析正确，但被调用方的行为与调用方的假设不同时，才适用 L6。

L2 与 L6 的辨析： 如果根因是运算符层面的隐式类型强制转换（+/-/*/== 触发字符串↔数字转换，或 as/类型转换绕过运行时类型检查），则属于 L2——L6 要求调用某个特定的被调用方，且其行为与调用方的假设不同。运算符不是被调用方。

L5 与 L7 的辨析： 如果错误代码、退出状态或异常被单一上下文结构（|| true、空 catch、缺少 set -e、裸 except）抑制，则属于 L5（控制流逃逸）——L7 要求存在多个执行上下文。单个顺序执行脚本/函数中的错误传播失败属于 L5。

L9 检查： 如果错误的根因是时区/区域设置/编码信息在数据类型层面丢失（例如，TIMESTAMP 与 TIMESTAMPTZ、无时区与有时区的 datetime、依赖区域设置的字符串排序），则属于 L9——即使看起来像“被调用方的行为与预期不同”，也不属于 L6；也不属于 L2 或 L8。 步骤 4. 深入追踪选定路径（指南步骤 4）——追踪正常路径和风险最高的边缘路径；解析每个名称，说明每种类型，跨越被调用方边界，并在确认存在偏差或确认满足安全后置条件时结束每条追踪。**Java/C++ 双重检查锁定规则：**对于双重检查锁定模式，必须追踪两个方面：(a) 缺少 volatile / 内存屏障（可见性隐患）；以及 (b) 将 instance = new X(); instance.init(); 作为两条非原子语句处理——无锁读取方可能在 init() 完成前看到非空的 instance（先发布后初始化隐患）。两者都要报告；遗漏任一项都属于分析不完整。

步骤 5. 识别偏差（指南步骤 5）——按 L1–L9 对每项偏差分类；指定严重性；应用可达性门槛（A 类直接报告；B 类需要探测——发现强制措施 → 丢弃候选项，未发现 → 指定严重性，部分发现 → 最高降至 Warning，并注明 manual verification recommended）。对于无 bug 情形，应用正确性对等原则。**无 bug 输出规范：**当最终不存在任何偏差时，仍须输出完整模板骨架——Mode 行、Scope、**Logic Score:** 100/100、## Findings（中文为 ## 发现），后接一个使用 Divergence: None — [why the premise holds]（中文为 偏差：无——[原因]）的发现块，并包含全部五个字段标签。这样可使推理可审计，并符合格式约定。如果分析明确排除了疑似 bug，须在 Trace: 字段中说明防护措施（例如，“Go 的 defer mu.Unlock() 可确保在所有退出路径上（包括提前返回）释放锁”）。不要将结论合并为自由格式的文字，也不要省略结构化字段；下游评分要求即使是无 bug 结论，也必须采用五字段格式。

步骤 5.5. 对抗式红队审查（指南步骤 5.5）——对每个候选发现，通过回答三个反驳问题（前提反驳、路径反驳、后果反驳）尝试推翻它。撤回存在已确认防护的发现；对存在部分防护的发现降级为 Suggestion。**设计意图门槛：**报告 L3 边界盲点前，先问：“代码是否在此边界显式返回错误 / 拒绝，而不是尝试继续越界运行？”如果是（例如，在 maxSize 处返回 errors.New("cache full")、429 Too Many Requests、缓冲区已满时拒绝），则撤回——这些是正确的边界强制措施，并非盲点。只有当代码尝试越界运行并悄然失败（结果错误、崩溃、无限循环）时，L3 才适用。注意：边界处的 panic 属于崩溃，而非有意设计的错误返回，因此仍可能属于 L3。

步骤 6. 应用铁律——五字段规范（指南步骤 6）——确认所有发现都完整包含 Premises → Trace → Divergence；然后填写 Trigger（具体的复现输入，Critical/Warning 级别必须提供）和 Remedy（可直接粘贴使用，参见 common.md §10）。每项发现都必须使用以下字面字段标签——英文 Premises: / Trace: / Divergence: / Trigger: / Remedy:，或中文 前提： / 追踪： / 偏差： / 触发： / 修复：。不得改写。Execution Path、Issue Found、Core Defect、执行路径、发现的逻辑隐患、核心缺陷 等标题均不能替代这些标签——它们不符合下游评分要求，也会破坏其他 Logic-Lens 技能使用的报告约定。**多项发现规范：**有多项发现时，## Findings（中文为 ## 发现）中的每个发现块都必须包含全部五个字面字段标签——Premises: / Trace: / Divergence: / Trigger: / Remedy:（或对应的中文标签）——且内容须针对该项发现。任何共享背景信息都可以放在前置章节中，但不能替代每项发现所需的字段。即使报告其他位置出现了 Premises: 或 Trace:，只要某项发现缺少 Divergence:（或任何其他必需字段），就会破坏格式约定。 步骤 6.5. 补救措施试运行（指南步骤 6.5）——在脑海中重新追踪 Trigger 输入经过修复后的代码，确认：分歧已消除、未引入回归问题、正常路径得以保留。

步骤 7. 评分并输出（指南步骤 7）——只要运行时可用，就应先执行步骤 8；该步骤会排除误报，从而改变评分。根据 common.md §6，针对通过验证的问题计算逻辑评分，并将其作为字面行 **Logic Score:** XX/100（中文 **逻辑评分：** XX/100）直接放在 Scope 行（**Scope:** / 中文 **范围：**）下方——必须使用此精确标记（不能写成 “Score: XX” 或 “Quality: XX”），以便评分器识别并供其他技能使用。然后使用本地化标题呈现报告模板的其余内容。

步骤 8. 执行验证关卡（指南步骤 8）——只要目标语言的运行时可用，对每个 Critical 和 Warning 问题都必须执行此步骤；只有此步骤能够推翻分析结果，因此即使推理过程非常确定，也不能跳过。根据 Trigger 字段生成最小复现示例，对原始代码执行该示例，然后应用补救措施并重新执行。若复现示例在原始代码上通过，则撤回相应问题——这些问题属于误报。对仍然存在的问题标记 ✅ Execution-verified；若没有可用运行时，则标记 ⚠️ Unverified — no runtime available（中文 ⚠️ 未验证——无可用运行时）。

报告中的模式行： Logic Review（中文：逻辑审查）。