X Cr

---
name: x-cr
description: |
  软件正确性调查 skill。用于用户说“XX 不太对”“这个功能有 bug”“结果和预期不一致”“帮我查原因”，也用于 review 模块、文件、diff 或 PR 的正确性。遇到已知异常、模块不变量、信任边界、授权范围扩张、服务端校验、租户/会话隔离或持久化一致性问题时优先使用本 skill。
  本 skill 先读取归属 spec 的“影响边界与不变量”，再从模块入口、契约邻居、状态/权限所有者、失败路径和调用方寻找遗漏候选，随后构造最小反例，并用日志、代码路径、测试、diff、spec 等证据做贝叶斯根因调查。
  x-cr 独立于 x-verify / x-qa-gate 自动门禁，产出 task 内或仓库级 `reports/cr/cr-report-*.md`，x-fix 可按稳定 Bn 问题 ID 继续修复。
---

# x-cr · 软件正确性调查

x-cr 是手动软件正确性调查入口，覆盖两种场景：

1. 已知问题：用户给出错误现象、复现步骤或异常链路，需要确认根因。
2. 模块正确性 review：用户要求检查模块、文件、diff 或 PR，需要主动寻找真实正确性风险。

两种场景共用同一主线：

```text
现象/变更
→ 归属 spec 与已声明不变量
→ 模块模型与遗漏候选不变量
→ 最小反例与可达路径
→ 候选根因
→ 贝叶斯证据更新
→ 不变量结论、严重度与置信度
→ CR 报告
```

不变量提供判断软件正确性的固定判尺；贝叶斯审查解释判尺被击穿的原因和证据强度。

## 与相邻 skill 的边界

| 结果 | 归属 |
|------|------|
| 有可达错误路径、安全/权限绕过、状态错误、数据错误或公开契约违背 | x-cr |
| 有结构腐化、分层错位或重复事实源，当前缺少可达错误结果 | x-audit-arch |
| 有命名、格式、排版或纯代码风格问题 | x-audit-style |
| verify 后的流水线 R1/R2/R3 自动质量门禁 | x-qa-gate |

结构问题已经形成错误路径时，x-cr 负责正确性结论；相邻 audit skill 继续负责结构和风格治理。

## 按需加载的参考

调查开始时加载：

1. `references/invariant-review.md`：spec 优先的不变量提取、遗漏发现和最小反例方法。
2. `references/bayesian-review.md`：候选根因与证据更新方法。
3. `references/checklist-general.md`：不变量状态、严重度和证据要求。

写报告前加载：

4. `references/report-template.md`：CR 报告固定 schema。

语言知识只用于判断运行时错误、类型逃逸、异步错误、资源泄漏、并发和数据边界。历史语言 reference 不参与当前流程。

## 输入模式

### 模式 A：已知问题

触发例子：

- “这个登录状态不太对，帮我查原因”
- “这个 bug 是配置读取导致的吗”
- “刷新 token 后还是失败，继续查”

目标：

- 把用户现象映射到归属 spec、不变量和实际代码路径。
- 构造最小复现，更新候选根因置信度。
- 解释用户为何看到该现象及其影响。

### 模式 B：模块正确性 review

触发例子：

- “review 一下这个模块有没有正确性问题”
- “检查当前 diff 有没有破坏模块不变量”
- “审批路径会不会把子命令权限扩大到根命令”
- “服务端会不会相信客户端伪造的 role 或 tenant_id”

目标：

- 读取 spec 已声明不变量并逐条验证。
- 主动寻找 spec 可能遗漏的安全、状态、数据和调用链规则。
- 对每个受影响不变量给出保持、破坏、未验证或来源冲突结论。

## 审查范围与报告路径

- 用户指定文件、目录、diff、PR 或模块时，按指定范围执行，并展开到维持相关不变量所需的契约邻居。
- 用户只说 `x-cr` / `review` / `检查一下` 时，使用当前 git diff。
- 当前 git diff 为空且用户未指定范围时，请用户给出模块、文件、PR 或现象。

报告路径：

- 归属当前 task：`docs/spec/<spec>/tasks/<task>/reports/cr/cr-report-YYYYMMDD-HHmmss.md`
- 普通仓库调查：`reports/cr/cr-report-YYYYMMDD-HHmmss.md`

## 执行流程

### 1. 建立调查对象

先写清：

| 字段 | 内容 |
|------|------|
| 模式 | 已知问题 / 模块正确性 review |
| 用户现象或审查目标 | 用户看到的错误、疑点或指定检查目标 |
| 期望行为 | 用户期望、产品期望或 spec 期望 |
| 实际行为 | 日志、测试、代码路径、diff 或用户描述 |
| 审查范围 | 文件、目录、diff、PR、模块 |

模式 A 把用户现象作为第一证据。模式 B 把 spec、不变量和模块入口作为第一证据。

### 2. 读取归属 spec 与已声明不变量

spec 是模块不变量的第一事实源。

在 task 中执行时：

1. 从 `dev-checklist.md` 的 `> spec:` 指针定位 `docs/spec/<spec>/spec.md`。
2. 读取 `任务目标`、`影响边界与不变量`、`判断依据`、`建模覆盖声明`及本 task 引用的 Scenarios。
3. 只提取本次范围中的目标、上游、下游和相关模块行。
4. 给每条相关规则分配稳定 `INV-SPEC-NN`，保留原始模块、依据 J-ID/Scenario 和证据路径。

普通仓库调查按以下顺序定位契约：

1. 用户指定或仓库现有 spec。
2. 安全策略、权限模型、schema、协议和公开 API 文档。
3. PR/issue、模块 README、调用方契约和负向测试。
4. 当前实现、日志和运行时行为作为事实证据。

当前用户约束与既有 spec 出现差异时，记录 `来源冲突` 和双方证据，等待权威契约确认。

### 3. 建立模块模型并寻找遗漏不变量

按以下顺序展开：

```text
主模块
→ 契约邻居
→ 状态与权限所有者
→ 入口适配层
→ 副作用与下游消费者
→ 证据与测试
```

记录每一层的可信输入、非可信输入、guard、状态所有者、副作用、失败返回和生命周期。

随后按 `references/invariant-review.md` 的原则寻找 spec 遗漏候选。候选使用 `INV-CAND-NN`，并归类为：

| 关系 | 含义 |
|------|------|
| 已被 spec 覆盖 | 链接对应 `INV-SPEC-NN`，合并验证 |
| spec 缺口 | 仓库证据支持该规则且 spec 未记录 |
| 待确认 | 不同规则会改变实现或验收，权威来源尚未明确 |
| 来源冲突 | spec、策略、调用方或用户约束给出不同规则 |

遗漏候选用于发现设计阶段未显式写出的真实规则，不能静默覆盖 spec。

### 4. 构造最小反例并判断变更触达

对每个相关不变量记录：

- 规则在本次范围中的执行者和状态所有者。
- diff 或现象经过的入口、guard、状态写入和副作用路径。
- 能击穿规则的最小输入或状态组合。
- 预期保持结果和可观察失败结果。
- 当前证据位置与仍缺少的证据。

未被本次范围触达的不变量写 `未触达` 和依据。受影响不变量继续进入贝叶斯调查。

### 5. 建立候选根因

围绕现象或可能被击穿的不变量建立候选 H。通常从 3-6 个高解释力候选开始，数量随模块范围和证据调整；覆盖闭环决定调查完成。

候选方向包括：

| 根因类型 | 例子 |
|----------|------|
| H_spec_mismatch | 当前行为与明确 spec/不变量冲突 |
| H_impl_drift | spec 清楚，实现漏做、做偏、回归 |
| H_state_boundary | 状态、输入、错误、并发或生命周期边界异常 |
| H_trust_authority | 非可信输入绕过服务端校验或授权范围扩大 |
| H_config_data | 配置、环境、数据形状或迁移状态异常 |
| H_test_gap | 测试未击穿错误实现 |
| H_spec_gap | 关键规则在 spec 中缺失或存在歧义 |

每个候选写明先验、触发条件、失败路径、影响和最短取证动作。

### 6. 用证据更新置信度

按贝叶斯公式组织推理：

```text
P(H | E) = P(E | H) * P(H) / P(E)
```

报告使用定性置信度：`低 / 中 / 高 / 已确认`。

每轮更新记录 H、证据 E、支持/削弱/中性、更新后置信度和下一步。高置信候选检查调用方保护、schema/运行时校验、配置默认值、已有测试、错误处理兜底及权威契约变更。

### 7. 判断不变量和 spec 关系

每个相关不变量给出：

| 结论 | 含义 |
|------|------|
| 保持 | 最小反例被正确拒绝或处理，证据覆盖真实执行路径 |
| 破坏 | 存在可达路径使规则失效 |
| 未验证 | 关键代码、日志、测试或运行环境证据缺失 |
| 来源冲突 | 权威来源给出不同规则，当前无法选定判尺 |
| 未触达 | 本次范围不经过该规则的执行路径 |

确认或高置信根因继续归类为：原始 spec 不一致、实现过程偏移、spec 缺口、环境/数据问题或证据不足。

### 8. 分开判定严重度与置信度

严重度回答影响，置信度回答证据强度：

| 等级 | 影响 |
|------|------|
| P0 | 授权/隔离绕过、数据破坏或丢失、核心不变量破坏、核心路径不可用 |
| P1 | 可达的用户可见错误、状态/边界/失败路径错误，影响可恢复或范围受限 |
| P2 | 当前缺少可达破坏路径的 spec、测试、日志、可观测性或来源证据 |

同一问题同时记录严重度和 `低 / 中 / 高 / 已确认` 置信度。

### 9. 输出报告与下游交接

报告必须保留：

1. `> Schema: x-cr-v2`
2. `不变量覆盖`
3. `审查结论`
4. `问题详情`

审查结论中的每条问题使用稳定 `B1`、`B2` 编号，并与 `### Bn:` 详情一一对应。

- 写入 x-cr-v2 报告后运行：
  `python3 skills/x-cr/scripts/validate_report.py <CR_REPORT_PATH>`。
- 校验失败时先修复报告结构，再向 x-fix 交接。
- 用户要求修复时，调用 x-fix 并传入 CR 报告完整路径。
- 用户只要求调查时，输出报告路径、P0/P1/P2 数量和最高优先级结论。
- `未验证`、`来源冲突` 和 P2 都给出最短补证或确认路径。

## 覆盖收口

调查结束前逐项声明：

- spec 中与本次范围相关的不变量已全部进入覆盖表。
- 主模块、契约邻居、状态/权限所有者、入口适配层、副作用和证据/tests 已检查。
- 每个受影响不变量已有最小反例和可达路径结论。
- 每个补充候选已有 spec 关系。
- 每个 Bn 结论都有代码、spec、测试、日志、diff 或调用链证据。

覆盖存在缺口时，把缺口写入 P2，并保持报告结论为“覆盖不完整”。

## 关键约束

- spec 声明的不变量优先进入调查，遗漏发现紧随其后。
- 对抗性检验服务于不变量验证和根因调查，必须落到触发条件、失败路径、影响和证据。
- 测试通过只证明被测试路径；确认断言能够击穿错误实现。
- 风格、命名、排版和纯抽象偏好退出 x-cr 报告。
- 手动正确性调查归 x-cr；流水线自动门禁归 x-qa-gate。