18 KiB
CM95 S-52 语义守恒与运行时能力审计标准 v2
日期：2026-09-20。适用目标：绑定固定 OpenCPN 源码、明确 Production Plan 与具体 target renderer 的流程等价审计。
1. v2 的作用与生产边界
本标准升级 v1 的 source/presentation/delivery/runtime 守恒要求，新增代码优先的 Gate A–I。它是审计标准，不表示现有生产 gate 已经实现这些新增检查，也不改变产品功能、registry、PBF schema 或 importer。
Data Release PASS 与 Target Portrayal PASS 必须继续分开。资源齐全、PBF可解码、delivery字段存在、capability写IMPLEMENTED、截图看起来接近，分别只能说明局部事实。
审计真值链：
固定 OpenCPN 源码 → typed CM93/S57 object view → Lookup与初始规则 → CSP分支/子调用 → 返回有序指令 → parser规则 → 分阶段renderer及副作用
随后正向对照：
CM95 Source → s52.py → csp.py → presentation / PBF facts → style compiler → target runtime → 每条primitive consumer
不得从最终截图、输出symbol或已损失的PBF反推原始OpenCPN分支，再据此声称等价。
2. 固定基线与证据绑定
每次审计必须记录：
- OpenCPN完整commit、固定目录、源码文件SHA-256；先校验，失败立即停止。
- CM95起始HEAD、branch、
git status --short --branch、实际审阅文件SHA；HEAD不能代表工作区未提交代码。 - dataset/fingerprint、Plan ID、Builder/Production版本、AOI、zoom/scale ladder、mapping/policy、FID manifest、Lookup IR、resource contract与release/PBF目录及哈希。
- target renderer及版本、运行时设置快照、display category、point/boundary table、颜色表、depth/height单位、SCAMIN、display scale、DPI/pixel ratio、raster/vector与GL/DC等适用条件。
唯一固定源码不包含的上游资源或关联对象实现应标证据不足。历史artifact中的commit字符串或资源hash一致可以证明链路一致性，不能自动补足独立上游定义证明。无正式release时允许count=null并说明evidence unavailable，但代码分支审计仍须完成。
v2 本轮固定源码为 docs/外部参考/OpenCPN源码基线_f7211b4e/，commit f7211b4e1874c453e37a7f190aa191c55a25c32e；未来换基线必须新建目录，不能覆盖旧目录或移动冻结tag。
本轮实例绑定：CM95 审计输入 HEAD 1a07406e6e11fde0425f81b54c7f4a3d2aff6d49；Production Plan ID 57e72826db1d3e3e69f0b3b084bef4fb9469b5edc47dc0030fc2ec3e46adecf9；release cm95-d1-62a85bd40d3a-57e72826db1d。配套报告与 JSON 记录 12 组、206 条组合式 branch 记录，以及已完成扫描的 5064 个 PBF、1976 个交付 signature；这些数量不等于已证明等价的完整输入数量。总体 Target Portrayal 为 FAIL；Gate A/B/C/D/E/H/I 为 FAIL，Gate F/G 为 NOT_PROVEN。Data Release PASS 仅引用既有 manifest，本轮没有重新验收或提升任何运行时能力状态。
3. 继承 v1 的语义守恒不变量
3.1 Physical Entity 与 Presentation 分离
同一relation group可以把多个source components合成一个物理delivery Feature，但必须保留component trace。若有N条独立LIGHTS source record，则必须保留N条独立presentation，不能以物理实体去重删除presentation。
审计分别计算source entity数、presentation数、instruction数、resource数和tile occurrence数。数量相等还不够，必须比较canonical signature multiset，避免A+B变成A+A。
3.2 Presentation Signature 与 Tile Occurrence
每条LIGHTS signature至少覆盖source_record_index、CSP、display category/priority、light mode/symbol、CA outline/color/width、start/end/radius/sector radius、sector sweep、nominal range、rotation/obscured、label/text。
同一个稳定Feature ID的expected signature multiset必须与actual相等；跨tile出现时signature集合必须守恒。合法按tile选取的不同source成员应先按production实际选择逻辑定义expected，不能把范围差异伪装成payload drift，也不能忽略真实drift。
多个LIGHTS必须保留s52_light_presentations完整数组；主scalar只用于兼容。CA、SY、TX分别审计数组consumer，CA消费数组不推出其他两者也消费数组。
3.3 Production Scope
Source expected scope必须重放Plan＋policy＋coverage＋tile buffer，而不只是裸AOI bbox：
- 每个计划tile计算生产相同的buffer expanded bounds。
- 按zoom scale ladder顺序，以finer coverage先占区域，coarser仅进入剩余visible region。
- AOI边缘合法buffer带入的source同样计入；不能直接按AOI删除。
- 在该tile/native_scale/visible region内实际selected成员上重新选relation base和LIGHTS。
- expected/actual tile occurrence set与signature multiset逐项相等。
source→presentation、presentation→PBF、PBF→consumer是独立阶段；只扫描PBF不能证明第一段未丢数据。
3.4 CA 与资源
CA使用屏幕毫米语义，不得预烘焙成地理圆。完整证据包括outline、arc、sector angles/legs、bearing转换、设备像素/逻辑像素、尺度相关缩放及render order。固定上游GL/DC可能有不同路径，必须明确target比较哪一路。
SY/AP/LC资源存在性、制作正确性、branch实际引用、target实际消费是四个独立检查。资源存在不等于primitive完整执行。
4. 审计状态及维度
| 状态 | 定义 |
|---|---|
| PASS | 在声明输入域与环境内，有完整固定源码→决策→中间事实→consumer证据证明等价 |
| PARTIAL | 已实现部分分支、primitive或近似表现；不得用于strict portrayal PASS |
| FAIL | 有明确缺失、多出、错误条件、参数、次序或副作用 |
| NOT_IMPLEMENTED | 对应层没有实现 |
| NOT_PROVEN | 有实现但证据不足，或上游该路径行为不确定；必须记录缺证及如何补证 |
| NOT_OBSERVED_IN_REAL_DATA | 源码分支保留，完整正式数据扫描未观察到；不是实现状态，也不是PASS |
| UPSTREAM_RESOURCE_MISSING | 已证明固定上游资源缺失；若仅历史contract报告而固定定义不可得，另记reported anomaly，独立验证保持NOT_PROVEN |
每条记录分别保存Python/decision、PBF/facts、consumer、overall、observation状态。某branch族FAIL不意味着其全部具体输入必然出错，例如Q/T可为空；必须写明失败的条件或反例。
PREVIEW_ONLY、NOT_IMPLEMENTED、capability missing、IMPLEMENTED缺实现证据均不能strict PASS。branch内部有FAIL不能被CSP总体PARTIAL或资源PASS覆盖。无数据或缺失属性不能按0计数；源码缺失不能按“常见规范应如此”猜测。
5. Gate A — OPENCPN_FLOW_EQUIVALENCE
进入CSP之前必须逐项证明：
- CM93 class substitution、typed attribute conversion、原始属性presence与null/unknown语义。
- geometry及S57/S52 class、point/boundary/line table选择。
- Lookup条件排序、数值/字符串/list/空suffix/wildcard/undefined匹配、fallback及没有Lookup的行为。
- initial instruction string、DISC、DPRI、radar priority及初始普通指令与CS的相对位置。
- SCAMIN、display scale、对象category mutable等入口及会改变CSP可达性的转换。
至少核对ITDARE→DEPARE、SPOGRD→DMPGRD、FSHHAV→FSHFAC、OFSPRD→CTNARE，以及$AREAS的$SCODE=II25属性值变为BACKGROUND。不能把后一项误写为对象class改为BACKGROUND。
源geometry与delivery geometry分别记录，AREA生成outline或代表点不能因此按LINE/POINT CSP重算。Lookup IR如果只来自CM95当前resource input，须注明无法独立证明与固定上游资源一致的边界。
6. Gate B — CSP_BRANCH_EQUIVALENCE
第一批必须覆盖12组：OBSTRN04、WRECKS02、UDWHAZ03、SOUNDG03、LIGHTS05/LIGHTS06、DEPARE01/DEPARE02、DEPCNT02、SOUNDG02、QUAPOS01/QUAPNT01/QUALIN01、SLCONS03、RESTRN01、RESARE02。
每个branch至少包含：稳定branch_id、procedure、source geometry/class、typed attributes的presence/value条件、mariner参数、关联对象条件、阈值、nested calls、完整有序sequence、category/priority/SCAMIN副作用、资源、各层实际行为、real_data_count及计数单位、状态、文件/函数/行号证据与unresolved items。
允许组合式矩阵：共享前缀、后缀、数值格式化、阈值选择分别编号，但必须给出明确组合顺序、父子引用、互斥/覆盖条件。参数stage不得冒充完整terminal branch；branch记录数不得冒充互斥输入域数量或测试覆盖率。SOUNDG数字、Q、OBJNAM后缀不能仅用不展开的名称“支持”。
必须区分可达实现、注释、#if 0、early return后的死代码和注册为NULL的占位。LIGHTS05实际进入LIGHTS06；DEPARE02调度到DEPARE01；hazard调用_UDWHAZ03不等于直接CS(UDWHAZ03)。上游未初始化变量或失败转换不应自行“修正”成理想算法，标NOT_PROVEN并保存源码证据。
7. Gate C — NESTED_CSP_CALL_GRAPH
从固定源码提取真实图，记录caller/callee、调用条件、参数、返回串插入位置、side effect及所在层。至少包括：
- OBSTRN04/WRECKS02→_UDWHAZ03、SNDFRM02（sounding formatting）、CSQUAPNT01。
- LIGHTS05→LIGHTS06→_selSYcol/_LITDSN01。
- SOUNDG02→MP→RenderMPS→每点SOUNDG03→SNDFRM02。
- QUAPOS01→CSQUALIN01/CSQUAPNT01；RESTRN01→_RESCSP01。
画出primitive和mariner-dependent node，标注Python、PBF、style、JS中的决策位置及精确断点。必须另有文字解释，不能只给Mermaid。普通C++ helper串拼接和generic CS opcode递归是不同路径，不能混为一谈。
8. Gate D — INSTRUCTION_SEQUENCE_EQUIVALENCE
以完整ordered Rule Chain比较，不能只比较SY代码集合。分别记录：
- initial LUP instruction。
- CSP raw returned string（含必要的record separators/异常格式）。
- parser得到的规则及参数/顺序。
- renderer各pass执行、visibility/filter、state mutations及最终消费。
至少识别SY、TX、TE、SOUNDG glyph chain、MP、CA、AP、AC、LS、LC、OP、CS；nested展开保留provenance。必须检测missing/extra primitive、次序变化、参数变化、side effect变化、扁平化损失、初始规则被dict覆盖、多个CS/多个同类opcode被压缩。
不得先假设OP有priority执行语义；固定parser若忽略OP，就以忽略作为本基线实际行为。面积AC/AP与对象pass独立时，返回串顺序不自动等于跨pass屏幕次序。
精确反例必须记录输入、完整expected/actual、源码anchor和差异类别。手工推导expected与实际运行OpenCPN oracle应分开标注；Python/Node直接执行当前代码的结果不能包装成OpenCPN执行结果。字符串空白/浮点格式差异不一定是语义差异，必须落到参数或consumer行为。
9. Gate E — RUNTIME_OPCODE_COVERAGE
release实际出现的每个CSP必须从branch expected sequence逐opcode找到consumer，说明参数来源、执行条件和次序。RUNTIME_OBSTRN/RUNTIME_WRECKS等粗capability只能作目录索引。
例如SY + S(V) + Q + TX必须逐项证明：主symbol、全部sounding glyph、quality symbol、文本/布局均存在，并在正确pass及状态下执行。只画主SY和普通深度text，整个完整branch不可PASS。
runtime kind范围至少包含CA、DEPARE、DEPCNT、SOUNDG、OBSTRN、WRECKS；新kind须加入usage scanner、capability registry、审计与实际执行证据。unknown kind不得因没有映射就静默忽略。
每opcode覆盖记录至少包括opcode、branch_id、实现路径/函数、输入字段、参数映射、order/pass、status、证据及缺失处理。marker字符串存在只能证明代码位置存在，不能证明release所有分支完整。
10. Gate F — REAL_DATA_BRANCH_COVERAGE
完整扫描正式Plan实际release；核对计划jobs、PBF footprint、explicit empty tiles、decode错误及artifact哈希。计数区分source objects、distinct delivery(layer,FID)、presentation与tile occurrences。
branch signature至少包含：source与delivery geometry、class、VALSOU presence/值域、WATLEV、EXPSOU、CATOBS/CATWRK、QUASOU/QUAPOS、TECSOU/STATUS、关联DRVAL1/2及对象身份/geometry、safety contour/depth、isolated结果、scale/display依赖。静态CSP还应有RESTRN/CATREA、CONDTN/CATSLC、LIGHTS相关属性等。
每个实际signature必须唯一映射到上游组合路径，或明确保存候选branch_ids＋NOT_PROVEN＋缺失字段。候选映射不等于full coverage PASS。允许在source unavailable时完成delivery扫描并将完整源级branch count置null；不得把缺失字段当源属性absent、把null当0，或用最终SY猜原始限制属性。
必须保留未观察到的上游分支。nested procedure不能因没有同名顶层CSP字段就判NOT_OBSERVED。实际出现而没有完整expected/actual覆盖的分支阻止Target Portrayal PASS。
11. Gate G — RESOURCE_DEPENDENCY_EQUIVALENCE
每个branch逐项列SY/AP/LC等资源名，动态SOUNDG家族须按可生成symbol universe展开。检查：
- 固定上游引用及定义证据；当前CM95 resource universe。
- metadata/sprite/pattern/line key是否构建，是否被style/runtime过滤掉。
- resource参数（pivot、mm、颜色表、位图/矢量等）的消费证据。
- 缺失时fail-closed或fallback路径是否与实际上游对应。
DANGER53等代码引用而缺资源应单独记录。禁止补造fallback把审计改PASS；也不能认为所有“问号fallback”在不同opcode中等价。上游SY/LC/AP fallback必须分别核实，不凭历史contract注释推断。
资源检查的局部PASS与branch总体FAIL/NOT_PROVEN可以同时存在，机器schema必须支持这种分离。
12. Gate H — MARINER_DEPENDENCY_EQUIVALENCE
至少逐项检查safety contour/depth、shallow/deep contour、two_shades、symbolized boundaries、point/boundary table、display category、priority/SCAMIN、display scale；还应包括depth/height units、文本/测深显示、灯描述/航标文本开关、屏幕毫米/缩放、颜色表与碰撞状态。
PBF保留原始稳定事实和presence，不固化随设置变化的最终color、safety contour、sounding family、isolated danger或promotion。reference模式允许明确固定profile，必须与runtime交付区分。
mariner-dependent不能仅等于当前六个水深CSP：RESARE的symbolized boundaries、LIGHTS的height unit与render尺度同样需要依赖证明。静态materialization宣称成立，须证明其输出在全部允许runtime settings下不变。
surrounding max/min scalar若不能保持关联对象geometry、membership与相同选择范围，不足以证明UDWHAZ。有效contour catalog不能仅凭当前viewport已加载线的最小值默认等价于chart catalog。
13. Gate I — RENDER_ORDER_EQUIVALENCE
分别证明同对象多primitive顺序、fill/pattern/line/symbol/text跨pass、initial/current display category与priority、CSP DisplayBase promotion、SCAMIN变化、静态层与runtime overlay、不同对象与symbol/text碰撞顺序。
MapLibre按priority/source-layer/opcode分层不是自动等价于OpenCPN rule execution。canvas overlay在全部style层上方必须提供排序证据；无法证明严格等价时为NOT_PROVEN。已证明缺失/多出的priority或primitive仍为FAIL。
同一设置变更应使用同一snapshot并失效相应cache，不得让DEPARE、DEPCNT、hazard与SOUNDG混用旧/新设置。截图仅作为最后视觉材料，不能替代code/rule/consumer证据。
14. Data Release 与 Target Portrayal 两道独立门槛
14.1 当前生产行为（截至本轮实际代码）
src/cm95pbf/release.py对Builder0.4.11+要求presentation conservation artifact，校验schema、PASS、plan_id和pbf_dir。runtime capability artifact在提供时为硬门槛；未提供时保持NOT_AUDITED，不能称target已审计。
tools/cm95_s52_runtime_capability_audit.py目前检查粗runtime kind、IMPLEMENTED和evidence marker。本标准新增的branch/sequence/opcode/source coverage要求尚不是该工具的已实现功能。
14.2 v2 声明 strict Target Portrayal PASS 的必要条件
- A–I在明确输入域/target/settings下均有完整PASS证据。
- source→presentation→delivery invariants PASS。
- 实际所需的全部runtime consumers完整实现，不能用PREVIEW_ONLY替代。
- 对应release的resource、branch、sequence、nested、settings、render-order结果绑定同一Plan和PBF；不能复用其他release或缩小AOI的PASS。
- 无实际出现的FAIL/NOT_IMPLEMENTED/NOT_PROVEN；未观察分支保留观察状态及未来覆盖责任。
Data Release可以继续使用它自己的数据验收结论；本轮审计FAIL不擅自改写既有release manifest，也不声称它证明了portrayal。
15. 机器产物与报告最小合同
JSON至少包含OpenCPN commit/root/hash校验、CM95 HEAD/worktree input hashes、Plan/release绑定、gate statuses、完整branch rows、真实调用图、ordered expected instructions、observed instructions/consumer、opcode coverage、resource dependencies、签名与计数单位、evidence paths/lines、unresolved items、验证方法及限制。
Markdown中每组CSP至少一张表，列为：branch_id、geometry、condition、mariner_dependency、nested_csp、expected_sequence、cm95_python、pbf_or_runtime_facts、style_or_runtime_consumer、real_data_count、status、evidence。
同时回答重复Python/JS决策、已确认不等价、同结构风险、是否建立统一Decision/Runtime Rule IR、runtime必须保留的字段、通用executor与专用renderer边界、scalar hint损失这七项架构问题。
临时分析器只在/tmp等非仓库位置；不新增Jest，不修改产品来制造PASS。本轮正式输出仅v2报告、v2标准和build/audits/cm95_s52_opencpn_code_first_equivalence_v2.json。
16. 历史、已关闭事项和后续阶段
v1 multi-LIGHTS source→PBF修复及正负回归是已记录的历史验收，不能把旧问题继续写成当前必然存在，也不能用旧PASS覆盖本次完整LIGHTS调用/文本/renderer审计。
本轮当前结论见流程对照报告v2：Target Portrayal FAIL；F源级branch覆盖、固定上游资源独立定义与全局renderer环境存在NOT_PROVEN。具体branch内部状态以报告和JSON为准。
统一IR、产品缺陷修复、自动gate实现、全输入域执行回归均为尚未启动的后续阶段。本标准不授权修改已有功能，也不暗示这些后续工作已经完成。