docs: add OpenCPN code-first S-52 audit task
This commit is contained in:
OpenAI Codex
517
docs/CM95_S52_OpenCPN代码优先流程等价审计_Codex任务_v1.md
Normal file
517
docs/CM95_S52_OpenCPN代码优先流程等价审计_Codex任务_v1.md
Normal file
@@ -0,0 +1,517 @@
|
||||
# CM95 S-52 OpenCPN 代码优先流程等价审计 Codex 任务 v1
|
||||
|
||||
日期：2026-09-20
|
||||
|
||||
## 1. 任务性质
|
||||
|
||||
本任务是**只读代码审计任务**。核心不是继续从最终截图寻找差异，而是以仓库内固定的 OpenCPN 源码快照为 Source of Truth，正向还原 OpenCPN 的 S-52 渲染流程，再与当前 CM95 实现逐层比较。
|
||||
|
||||
本轮原则：
|
||||
|
||||
- 先审计，后修改。
|
||||
- 不修改 CM95 功能代码。
|
||||
- 不修改 Web runtime renderer。
|
||||
- 不修改 builder、CSP resolver、style compiler、PBF schema 或 release gate。
|
||||
- 不把任何 PREVIEW_ONLY / NOT_IMPLEMENTED 状态改成 IMPLEMENTED。
|
||||
- 不通过“截图看起来接近”替代代码流程等价证明。
|
||||
- 不新增或修改 Jest 测试。
|
||||
- 如需临时分析脚本，只能放在 `/tmp` 或其他非仓库临时位置，不提交。
|
||||
|
||||
## 2. 仓库与 Git 边界
|
||||
|
||||
仓库：`/root/sourceserver/cm95`
|
||||
|
||||
分支：`main`
|
||||
|
||||
开始任务时必须记录：
|
||||
|
||||
- `git rev-parse HEAD`
|
||||
- `git status --short --branch`
|
||||
- 当前工作区是否存在与本任务无关的未提交修改。
|
||||
|
||||
本任务不得清理、重置、覆盖或提交与本任务无关的现有修改。最终如提交 Git，只允许显式 stage 本任务新增/修改的审计文档和审计产物。
|
||||
|
||||
## 3. 固定 OpenCPN 对照基线
|
||||
|
||||
不要依赖 `/tmp/opencpn-s52-audit/` 作为必要输入。统一使用仓库内已固定的上游参考快照：
|
||||
|
||||
`docs/外部参考/OpenCPN源码基线_f7211b4e/`
|
||||
|
||||
固定 OpenCPN commit：
|
||||
|
||||
`f7211b4e1874c453e37a7f190aa191c55a25c32e`
|
||||
|
||||
关键源码：
|
||||
|
||||
- `docs/外部参考/OpenCPN源码基线_f7211b4e/上游源码/gui/src/cm93.cpp`
|
||||
- `docs/外部参考/OpenCPN源码基线_f7211b4e/上游源码/libs/s52plib/src/s52cnsy.cpp`
|
||||
- `docs/外部参考/OpenCPN源码基线_f7211b4e/上游源码/libs/s52plib/src/s52plib.cpp`
|
||||
- `docs/外部参考/OpenCPN源码基线_f7211b4e/上游源码/libs/s52plib/src/s52plib.h`
|
||||
- `docs/外部参考/OpenCPN源码基线_f7211b4e/上游源码/libs/s52plib/src/s52utils.cpp`
|
||||
- `docs/外部参考/OpenCPN源码基线_f7211b4e/上游源码/libs/s52plib/src/s52utils.h`
|
||||
- 以及该快照中完整的 `libs/s52plib/src/`。
|
||||
|
||||
开始审计前先运行 SHA-256 校验，确认参考源码未被修改；若校验失败，停止并报告，不得继续以损坏快照作为基准。
|
||||
|
||||
## 4. 当前 CM95 对照范围
|
||||
|
||||
至少审阅以下当前实际实现：
|
||||
|
||||
- `src/cm95pbf/s52.py`
|
||||
- `src/cm95pbf/csp.py`
|
||||
- `src/cm95pbf/presentation.py`
|
||||
|
||||
- `tools/cm95_s52_style_compiler.py`
|
||||
- `tools/cm95_s52_runtime_capability_audit.py`
|
||||
- `config/s52/cm95_s52_runtime_capabilities_web_compare_v1.json`
|
||||
- `web/kyushu_compare.html`
|
||||
- 与上述文件直接相关的 lookup、resource、presentation、release audit 代码。
|
||||
|
||||
同时阅读已有文档，避免重复调查：
|
||||
|
||||
- `docs/报告/CM95_S52_OpenCPN渲染流程对照审计报告_v1.md`
|
||||
- `docs/CM95_S52_语义守恒与运行时能力审计标准_v1.md`
|
||||
- `docs/CM95_S52_静态物化与运行时呈现边界_v1.md`
|
||||
- `docs/CM95_S52_NavSea运行时呈现契约_v1.md`
|
||||
|
||||
已有报告中的结论只能作为线索，最终判断必须重新落到 OpenCPN 固定源码和当前 CM95 实现。
|
||||
|
||||
## 5. 审计总流程
|
||||
|
||||
必须从 OpenCPN 正向建立以下链路，不允许从当前 PBF 或截图反推 OpenCPN：
|
||||
|
||||
`CM93 Object`
|
||||
→ `CreateS57Obj / class normalization`
|
||||
→ `S-52 Lookup`
|
||||
→ `initial Rule chain`
|
||||
→ `CS(...)`
|
||||
→ `CSP branch`
|
||||
→ `nested CSP calls`
|
||||
→ `ordered instruction sequence`
|
||||
→ `primitive opcode`
|
||||
→ `resource dependency`
|
||||
→ `mariner dependency`
|
||||
→ `display category / priority / render order`
|
||||
→ `renderer`
|
||||
|
||||
然后对照 CM95 对应链路：
|
||||
|
||||
`CM95 source`
|
||||
→ `s52.py`
|
||||
→ `csp.py`
|
||||
→ `presentation.py / PBF runtime facts`
|
||||
→ `style compiler`
|
||||
→ `Web runtime`
|
||||
→ `primitive consumer`
|
||||
|
||||
## 6. 第一批强制审计 CSP
|
||||
|
||||
按以下优先级执行，并建立完整调用关系，不得把它们当成孤立函数：
|
||||
|
||||
1. `OBSTRN04`
|
||||
2. `WRECKS02`
|
||||
3. `UDWHAZ03`
|
||||
4. `SOUNDG03`
|
||||
5. `LIGHTS05 / LIGHTS06`
|
||||
6. `DEPARE01 / DEPARE02`
|
||||
7. `DEPCNT02`
|
||||
8. `SOUNDG02`
|
||||
9. `QUAPOS01 / QUAPNT01 / QUALIN01`
|
||||
10. `SLCONS03`
|
||||
11. `RESTRN01`
|
||||
12. `RESARE02`
|
||||
|
||||
注意：OpenCPN 当前源码中 `LIGHTS05()` 会进入 `LIGHTS06()`；审计必须以真实可达执行链为准，不能只按旧函数名或注释判断。
|
||||
|
||||
## 7. Gate A：OPENCPN_FLOW_EQUIVALENCE
|
||||
|
||||
先确认对象在进入 CSP 前已经走到了与 OpenCPN 等价的对象视图和 Lookup。
|
||||
|
||||
至少核对：
|
||||
|
||||
- CM93 class substitution；
|
||||
- geometry type；
|
||||
- S-57/S-52 object class；
|
||||
- Lookup table 选择；
|
||||
- initial instruction string；
|
||||
- display category；
|
||||
- display priority；
|
||||
- point/boundary table 相关选择；
|
||||
- SCAMIN / scale 相关入口；
|
||||
- 任何会影响后续 CSP 选择的对象属性转换。
|
||||
|
||||
已知至少检查：
|
||||
|
||||
- `ITDARE → DEPARE`
|
||||
- `SPOGRD → DMPGRD`
|
||||
- `FSHHAV → FSHFAC`
|
||||
- `OFSPRD → CTNARE`
|
||||
- `$AREAS + $SCODE=II25 → BACKGROUND`
|
||||
|
||||
## 8. Gate B：CSP_BRANCH_EQUIVALENCE
|
||||
|
||||
对每个目标 CSP，从 OpenCPN 源码抽取完整 branch matrix。
|
||||
|
||||
每个 branch 至少记录：
|
||||
|
||||
- procedure；
|
||||
- geometry；
|
||||
- object class；
|
||||
- attribute presence / value condition；
|
||||
- mariner parameter condition；
|
||||
- surrounding DEPARE/DRGARE 等关联对象条件；
|
||||
- safety contour / safety depth 等阈值；
|
||||
- 分支中调用的 nested CSP；
|
||||
- 最终有序 instruction sequence；
|
||||
- display category / priority side effect；
|
||||
- resource dependency。
|
||||
|
||||
不能只记录“支持 OBSTRN04”或“支持 WRECKS02”。
|
||||
|
||||
如果 OpenCPN 某个分支是：
|
||||
|
||||
`SY(DANGER51) + SOUNDG03 + QUAPNT01 + TX(...)`
|
||||
|
||||
而当前实现只得到：
|
||||
|
||||
`SY(DANGER51) + SOUNDG03`
|
||||
|
||||
必须判定该 branch 为 FAIL。
|
||||
|
||||
## 9. Gate C：NESTED_CSP_CALL_GRAPH
|
||||
|
||||
建立第一批 CSP 的真实调用图。
|
||||
|
||||
重点确认：
|
||||
|
||||
- `OBSTRN04 → UDWHAZ03`
|
||||
- `OBSTRN04 → SOUNDG03 / sounding formatting path`
|
||||
- `OBSTRN04 → QUAPNT01`
|
||||
- `WRECKS02 → UDWHAZ03`
|
||||
- `WRECKS02 → SOUNDG03 / sounding formatting path`
|
||||
- `WRECKS02 → QUAPNT01`
|
||||
- `LIGHTS05 → LIGHTS06`
|
||||
|
||||
如果 nested CSP 的输出在 Python、PBF、style compiler 或 Web runtime 任意一层被截断，必须在调用图中标出具体断点。
|
||||
|
||||
## 10. Gate D：INSTRUCTION_SEQUENCE_EQUIVALENCE
|
||||
|
||||
OpenCPN 的审计单位是**完整、有序 Rule Chain**，不是单个 symbol code。
|
||||
|
||||
对每个 branch 比较：
|
||||
|
||||
`OpenCPN expected ordered sequence`
|
||||
|
||||
与：
|
||||
|
||||
`CM95 resolver / runtime actual ordered sequence`
|
||||
|
||||
至少识别并展开：
|
||||
|
||||
- `SY`
|
||||
- `TX`
|
||||
- `TE`
|
||||
- `SOUNDG / sounding symbol chain`
|
||||
- `CA`
|
||||
- `AP`
|
||||
- `AC`
|
||||
- `LS`
|
||||
- `LC`
|
||||
- `OP`
|
||||
- `CS`
|
||||
|
||||
需要区分：
|
||||
|
||||
- primitive 缺失；
|
||||
- primitive 多出；
|
||||
- 顺序变化；
|
||||
- 参数变化；
|
||||
- nested CSP 被扁平化后语义丢失；
|
||||
- display side effect 丢失。
|
||||
|
||||
## 11. Gate E：RUNTIME_OPCODE_COVERAGE
|
||||
|
||||
对 release 实际出现且由 runtime 处理的 CSP，不能再只使用粗粒度 `RUNTIME_OBSTRN`、`RUNTIME_WRECKS` 等 capability 名称证明完整性。
|
||||
|
||||
必须从 branch expected sequence 逐 opcode 检查实际 consumer。
|
||||
|
||||
例如 OBSTRN04 某 branch 需要：
|
||||
|
||||
`SY + SOUNDG03 + QUAPNT01 + TX`
|
||||
|
||||
则必须分别回答：
|
||||
|
||||
- SY 谁执行；
|
||||
- SOUNDG03 谁执行；
|
||||
- QUAPNT01 谁执行；
|
||||
- TX 谁执行；
|
||||
- 参数来源是否与 OpenCPN 等价；
|
||||
- 执行顺序是否守恒。
|
||||
|
||||
只实现其中一部分，整个 branch FAIL。
|
||||
|
||||
## 12. Gate F：REAL_DATA_BRANCH_COVERAGE
|
||||
|
||||
基于当前正式 Production Plan 与 release 数据扫描实际出现的条件组合。
|
||||
|
||||
当前已知正式基线：
|
||||
|
||||
- Builder：`cm95pbf-builder/0.4.12-opencpn-cm93-coverage`
|
||||
- Production：`cm95pbf-production/2.3-opencpn-cm93-coverage`
|
||||
- Plan：`build/production/cm95_s52_kyushu_production_plan_v4_opencpn_coverage.json`
|
||||
- Plan ID：`57e72826db1d3e3e69f0b3b084bef4fb9469b5edc47dc0030fc2ec3e46adecf9`
|
||||
- Release：`cm95-d1-62a85bd40d3a-57e72826db1d`
|
||||
- Release root：`build/releases-s52-v2/cm95-d1-62a85bd40d3a-57e72826db1d`
|
||||
|
||||
如这些产物在当前机器不存在，记录为 evidence unavailable，不得伪造统计。
|
||||
|
||||
对实际数据生成 branch signature，至少覆盖与目标 CSP 相关的：
|
||||
|
||||
- geometry；
|
||||
- object class；
|
||||
- VALSOU present/absent/value band；
|
||||
- WATLEV；
|
||||
- EXPSOU；
|
||||
- CATOBS / CATWRK 等类别属性；
|
||||
- QUASOU / QUAPOS；
|
||||
- TECSOU / STATUS；
|
||||
- surrounding DRVAL1 / DRVAL2；
|
||||
- safety contour / safety depth；
|
||||
- isolated danger result；
|
||||
- scale / display dependency。
|
||||
|
||||
每个真实出现的 branch signature 必须映射到 OpenCPN branch matrix，并标记当前 CM95 是否完整覆盖。
|
||||
|
||||
## 13. Gate G：RESOURCE_DEPENDENCY_EQUIVALENCE
|
||||
|
||||
对 branch 中引用的 `SY/AP/LC` 等资源逐项核对：
|
||||
|
||||
- OpenCPN 引用的资源名；
|
||||
- CM95 resource universe 是否存在；
|
||||
- style/runtime 是否能消费；
|
||||
- 缺失时是否 fail-closed；
|
||||
- 是否存在未经 OpenCPN 依据自行造出的 fallback。
|
||||
|
||||
已知 `DANGER53` 这类“代码可能引用但资源不存在”的情况必须单独记录为 upstream/resource anomaly，不能为了让审计 PASS 自行补造资源。
|
||||
|
||||
## 14. Gate H：MARINER_DEPENDENCY_EQUIVALENCE
|
||||
|
||||
至少核对：
|
||||
|
||||
- safety contour；
|
||||
- safety depth；
|
||||
- shallow contour；
|
||||
- deep contour；
|
||||
- symbolized boundaries；
|
||||
- point table；
|
||||
- boundary table；
|
||||
- display category；
|
||||
- SCAMIN；
|
||||
- display scale；
|
||||
- 其他会改变 CSP branch 或 primitive 参数的 mariner setting。
|
||||
|
||||
必须明确哪些值应保留到 runtime 才决定。
|
||||
|
||||
禁止把 mariner-dependent 最终表现提前写死进 PBF，再宣称与 OpenCPN 等价。
|
||||
|
||||
## 15. Gate I：RENDER_ORDER_EQUIVALENCE
|
||||
|
||||
检查 OpenCPN Rule Chain、display priority、display category、对象 geometry 与 MapLibre/style/runtime 实际绘制顺序之间是否存在语义变化。
|
||||
|
||||
至少识别：
|
||||
|
||||
- 同一对象多个 primitive 的相对顺序；
|
||||
- fill / pattern / line / symbol / text 的先后关系；
|
||||
- CSP side effect 导致的 DisplayBase promotion；
|
||||
- runtime overlay 与静态 style layer 之间是否破坏 OpenCPN 的优先级语义。
|
||||
|
||||
如果当前架构无法证明严格顺序等价，应明确标记 UNKNOWN / NOT_PROVEN，不得默认 PASS。
|
||||
|
||||
## 16. 已知问题作为回归检查点
|
||||
|
||||
已有 v1 报告发现的以下问题必须重新从固定源码验证，不可直接抄结论：
|
||||
|
||||
- OBSTRN04 POINT 的 QUAPNT01；
|
||||
- OBSTRN04 的 OBJNAM TX；
|
||||
- OBSTRN04 LINE sounding；
|
||||
- OBSTRN04 AREA sounding / QUAPNT01；
|
||||
- isolated AREA 的 QUAPNT01；
|
||||
- WRECKS02 POINT / AREA 的 QUAPNT01；
|
||||
- WRECKS 的 `TX('Wk')` / `WRECKS07`；
|
||||
- 当前 Web hazard depth text 与 OpenCPN SOUNDG03 glyph chain 的差异；
|
||||
- LIGHTS05 实际进入 LIGHTS06。
|
||||
|
||||
## 17. 审计状态定义
|
||||
|
||||
每个 CSP / branch / opcode 至少使用以下状态之一：
|
||||
|
||||
- `PASS`：当前实现能够证明与固定 OpenCPN 基线等价。
|
||||
- `PARTIAL`：只实现了部分 branch、部分 primitive 或近似表现。
|
||||
- `FAIL`：存在明确缺失、错误条件、错误参数、错误顺序或错误 side effect。
|
||||
- `NOT_IMPLEMENTED`：当前系统无对应实现。
|
||||
- `NOT_PROVEN`：存在实现，但证据不足以证明流程等价。
|
||||
- `NOT_OBSERVED_IN_REAL_DATA`：OpenCPN 代码存在该分支，但当前正式数据未观察到。
|
||||
- `UPSTREAM_RESOURCE_MISSING`：OpenCPN 代码引用资源，但固定上游资源本身缺失；不得自行造资源后标 PASS。
|
||||
|
||||
不要用一个 CSP 的总体标签覆盖内部 branch 状态。
|
||||
|
||||
## 18. 必须输出的 branch 表
|
||||
|
||||
报告中第一批每个 CSP 至少给出一张表，列包含：
|
||||
|
||||
| 字段 | 含义 |
|
||||
|---|---|
|
||||
| branch_id | 稳定 branch 编号 |
|
||||
| geometry | POINT / LINE / AREA 等 |
|
||||
| condition | OpenCPN 分支条件 |
|
||||
| mariner_dependency | 使用的 mariner 参数 |
|
||||
| nested_csp | 调用的子 CSP |
|
||||
| expected_sequence | OpenCPN 有序 instruction sequence |
|
||||
| cm95_python | Python resolver 对应状态 |
|
||||
| pbf_or_runtime_facts | 中间语义是否守恒 |
|
||||
| style_or_runtime_consumer | 最终 consumer |
|
||||
| real_data_count | 正式数据实际命中数 |
|
||||
| status | PASS / PARTIAL / FAIL 等 |
|
||||
| evidence | 文件、函数、行号或 artifact 证据 |
|
||||
|
||||
## 19. 必须输出的调用图
|
||||
|
||||
至少给出第一批 CSP 的调用图，明确：
|
||||
|
||||
- 顶层 CSP；
|
||||
- nested CSP；
|
||||
- 最终 primitive；
|
||||
- mariner-dependent node；
|
||||
- 当前 CM95 决策发生在哪一层；
|
||||
- 语义在哪一层可能被截断。
|
||||
|
||||
调用图可以使用 Mermaid，但必须同时有文字说明，避免只靠图形表达关键结论。
|
||||
|
||||
## 20. 必须输出的架构结论
|
||||
|
||||
审计结束后必须回答：
|
||||
|
||||
1. 当前是否存在同一 OpenCPN branch condition 在 Python 与 JS 中重复手写；
|
||||
2. 哪些 CSP 已经因此产生已确认的不等价；
|
||||
3. 哪些 CSP 即使当前画面没有暴露问题，也存在相同结构风险；
|
||||
4. 是否应建立统一的 OpenCPN-compatible CSP Decision IR / Runtime Rule IR；
|
||||
5. 如果建立 IR，哪些字段必须保留到 runtime；
|
||||
6. 哪些 opcode 可以由通用 executor 执行，哪些需要专用 renderer；
|
||||
7. 哪些现有 PBF scalar hint 会压缩或丢失有序 Rule Chain。
|
||||
|
||||
## 21. 本轮正式输出
|
||||
|
||||
本轮只允许生成/更新审计资料，不修改产品实现。
|
||||
|
||||
必须输出：
|
||||
|
||||
1. `docs/报告/CM95_S52_OpenCPN渲染流程对照审计报告_v2.md`
|
||||
- 在现有 v1 基础上升级；
|
||||
- 以代码流程等价为主线；
|
||||
- 包含 branch matrix、call graph、instruction sequence、runtime opcode coverage、real-data branch coverage 和明确缺口。
|
||||
|
||||
2. `docs/CM95_S52_语义守恒与运行时能力审计标准_v2.md`
|
||||
- 在现有 v1 基础上升级；
|
||||
- 正式加入：
|
||||
- CSP_BRANCH_EQUIVALENCE
|
||||
- NESTED_CSP_CALL_GRAPH
|
||||
- INSTRUCTION_SEQUENCE_EQUIVALENCE
|
||||
- RUNTIME_OPCODE_COVERAGE
|
||||
- REAL_DATA_BRANCH_COVERAGE
|
||||
- RESOURCE_DEPENDENCY_EQUIVALENCE
|
||||
- MARINER_DEPENDENCY_EQUIVALENCE
|
||||
- RENDER_ORDER_EQUIVALENCE
|
||||
- 明确 Data Release PASS 与 Target Portrayal PASS 继续分离。
|
||||
|
||||
3. 机器可读审计产物：
|
||||
`build/audits/cm95_s52_opencpn_code_first_equivalence_v2.json`
|
||||
|
||||
机器可读产物至少记录：
|
||||
|
||||
- OpenCPN commit；
|
||||
- CM95 HEAD；
|
||||
- Production Plan ID；
|
||||
- CSP；
|
||||
- branch_id；
|
||||
- branch signature；
|
||||
- expected ordered instructions；
|
||||
- CM95 observed instructions / consumers；
|
||||
- real_data_count；
|
||||
- status；
|
||||
- evidence paths；
|
||||
- unresolved items。
|
||||
|
||||
如果当前机器缺少正式 release 数据，可允许 `real_data_count=null` 并记录 evidence unavailable，但代码流程审计仍必须完成。
|
||||
|
||||
## 22. 禁止事项
|
||||
|
||||
本轮禁止：
|
||||
|
||||
- 因发现缺陷直接修改 `src/cm95pbf/csp.py`；
|
||||
- 修改 `web/kyushu_compare.html` 来让截图接近；
|
||||
- 修改 runtime capability registry 把 FAIL 改成 PASS；
|
||||
- 修改 style compiler 掩盖 opcode 缺口；
|
||||
- 增加未经 OpenCPN 依据的 symbol fallback；
|
||||
- 删除或弱化已有 release gate；
|
||||
- 用人工截图作为 branch equivalence 的主要证据；
|
||||
- 因当前真实数据没有命中某分支就删除该 OpenCPN 分支；
|
||||
- 把“当前 Web 有一段文字/图标”当作完整 SOUNDG03/SY/TX executor 的证明。
|
||||
|
||||
## 23. 完成前必做对照清单
|
||||
|
||||
结束前逐项确认，不得静默跳过：
|
||||
|
||||
- [ ] 已校验仓库内 OpenCPN 固定源码快照 SHA-256。
|
||||
- [ ] 已记录 CM95 HEAD 与工作区状态。
|
||||
- [ ] 已从 OpenCPN 正向还原 Object → Lookup → CSP → Rule Chain → primitive 流程。
|
||||
- [ ] 已完成第一批 12 组 CSP 的 branch matrix。
|
||||
- [ ] 已建立 nested CSP call graph。
|
||||
- [ ] 已逐 branch 比较完整有序 instruction sequence。
|
||||
- [ ] 已检查 runtime opcode consumer，不再只看粗粒度 capability。
|
||||
- [ ] 已扫描或明确说明无法扫描正式 real-data branch coverage。
|
||||
- [ ] 已检查 resource dependency。
|
||||
- [ ] 已检查 mariner dependency。
|
||||
- [ ] 已检查 render order / DisplayBase 等 side effect。
|
||||
- [ ] 已重新验证 v1 已知 OBSTRN/WRECKS/SOUNDG/LIGHTS 缺口。
|
||||
- [ ] 已输出 v2 审计报告。
|
||||
- [ ] 已输出 v2 审计标准。
|
||||
- [ ] 已输出机器可读 JSON。
|
||||
- [ ] 未修改任何产品功能代码。
|
||||
- [ ] 未把 PREVIEW_ONLY / FAIL 人为改成 PASS。
|
||||
- [ ] 未新增或修改 Jest 测试。
|
||||
- [ ] 已逐项回看本任务文件，确认无必做项遗漏。
|
||||
|
||||
无法完成的项目必须在报告中明确写出原因、缺少的证据和后续需要什么，不得静默省略。
|
||||
|
||||
## 24. Git 收尾
|
||||
|
||||
由于当前仓库可能存在与本任务无关的未提交修改，必须严格隔离提交范围。
|
||||
|
||||
只允许提交本任务产生的：
|
||||
|
||||
- `docs/报告/CM95_S52_OpenCPN渲染流程对照审计报告_v2.md`
|
||||
- `docs/CM95_S52_语义守恒与运行时能力审计标准_v2.md`
|
||||
- `build/audits/cm95_s52_opencpn_code_first_equivalence_v2.json`
|
||||
|
||||
不得使用会把其他工作区修改一起带入的宽泛 `git add .`。
|
||||
|
||||
完成后：
|
||||
|
||||
1. 显式 stage 上述文件；
|
||||
2. 检查 staged diff；
|
||||
3. 提交到当前 `main`；
|
||||
4. push 到 `origin/main`；
|
||||
5. 在完成报告末尾记录 commit hash、commit message、push 结果；
|
||||
6. push 失败时明确报告失败，不得声称远端已完成。
|
||||
|
||||
## 25. 最终判定原则
|
||||
|
||||
这次审计的目标不是让结果变成 PASS，而是让“不等价发生在哪里”可被机器和人准确定位。
|
||||
|
||||
如果当前实现只能证明部分等价，应保留 PARTIAL / FAIL / NOT_PROVEN。
|
||||
|
||||
截图只作为最后的视觉验证材料。真正的主证据必须是：
|
||||
|
||||
`OpenCPN source branch → expected Rule Chain → CM95 decision/facts → runtime primitive consumer`
|
||||
|
||||
只有这条链完整守恒，才允许将对应 branch 判为 PASS。
|
||||
Reference in New Issue
Block a user