docs: close RC-039 and record Code-First v4

build/audits/cm95_s52_rc039_depcnt_control_flow_fix_v1.json

@@ -0,0 +1,112 @@
+{
+  "schema": "cm95.s52.rc039-depcnt-control-flow-fix/v1",
+  "date": "2026-09-21",
+  "status": "PASS",
+  "branch_id": "DC-DEC-DEP-LOW",
+  "commit": "1dbe1fde07ed64b39893de7d7e6ec5ce77cab871",
+  "opencpn_behavior": "For LINE DEPARE, when DRVAL1<=safety_contour, only DRVAL2>=safety_contour can set safe=true. The chart next-safe-contour fallback belongs exclusively to the outer else branch where DRVAL1>safety_contour.",
+  "previous_incorrect_audit_explanation": "DRVAL2<=DRVAL1 must be normalized to DRVAL1+0.01 before DEPCNT02 safety selection.",
+  "correct_root_cause": "Nested OpenCPN if/else was flattened into CM95 if/elif, making the next-safe fallback reachable in a branch where OpenCPN never evaluates it.",
+  "python_witness": [
+    {
+      "case": "low-no-cross",
+      "instruction": "LS(SOLD,1,DEPCN)",
+      "safe": false
+    },
+    {
+      "case": "cross-safety",
+      "instruction": "LS(SOLD,2,DEPSC)",
+      "safe": true
+    },
+    {
+      "case": "deep-next-safe",
+      "instruction": "LS(SOLD,2,DEPSC)",
+      "safe": true
+    }
+  ],
+  "js_runtime_witness": [
+    {
+      "case": "low-no-cross",
+      "operations": [
+        {
+          "opcode": "LS",
+          "args": [
+            "SOLD",
+            "1",
+            "DEPCN"
+          ]
+        }
+      ]
+    },
+    {
+      "case": "cross-safety",
+      "operations": [
+        {
+          "opcode": "SE",
+          "args": []
+        },
+        {
+          "opcode": "LS",
+          "args": [
+            "SOLD",
+            "2",
+            "DEPSC"
+          ]
+        }
+      ]
+    },
+    {
+      "case": "deep-next-safe",
+      "operations": [
+        {
+          "opcode": "SE",
+          "args": []
+        },
+        {
+          "opcode": "LS",
+          "args": [
+            "SOLD",
+            "2",
+            "DEPSC"
+          ]
+        }
+      ]
+    },
+    {
+      "case": "depcnt-mariner-exact",
+      "operations": [
+        {
+          "opcode": "SE",
+          "args": []
+        },
+        {
+          "opcode": "LS",
+          "args": [
+            "SOLD",
+            "2",
+            "DEPSC"
+          ]
+        }
+      ]
+    }
+  ],
+  "kyushu_v5_release_affected_feature_count": 0,
+  "rebuild_required": false,
+  "code_first_v4_counts": {
+    "PASS": 121,
+    "FAIL": 0,
+    "NOT_PROVEN": 85
+  },
+  "gates": {
+    "A": "FAIL",
+    "B": "PASS",
+    "C": "PASS",
+    "D": "PASS",
+    "E": "PASS",
+    "F": "NOT_PROVEN",
+    "G": "NOT_PROVEN",
+    "H": "PASS",
+    "I": "NOT_PROVEN"
+  },
+  "target_portrayal": "FAIL"
+}

docs/报告/CM95_S52_OpenCPN渲染流程对照审计报告_v4.md

@@ -0,0 +1,47 @@
+# CM95 S-52 OpenCPN 渲染流程对照审计报告 v4
+
+日期：2026-09-21。固定 OpenCPN baseline：f7211b4e1874c453e37a7f190aa191c55a25c32e。
+
+## 1. 结论
+
+RC-039 修复后，206 条 branch 重新判定为：
+
+| PASS | FAIL | NOT_PROVEN | 合计 |
+|---:|---:|---:|---:|
+| 121 | 0 | 85 | 206 |
+
+Branch 层面的确认 FAIL 已清零。Target Portrayal 仍为 FAIL，原因不是 branch FAIL，而是 Gate A 仍 FAIL，Gate F/G/I 仍为 NOT_PROVEN。
+
+## 2. RC-039 正确根因
+
+v3 residual 将问题解释为“DEPCNT02 应先把 DRVAL2<=DRVAL1 规范化为 DRVAL1+0.01”，该解释不符合固定 OpenCPN 源码。
+
+固定源码真实控制流是：当 DRVAL1 <= safety_contour 时，只检查 DRVAL2 >= safety_contour；只有 DRVAL1 > safety_contour 时，才进入 outer else 并比较 chart next-safe-contour。
+
+CM95 原实现把这个嵌套 if/else 压平成 if/elif，导致 DRVAL1=2, DRVAL2=2, safety=3, chart_next=2 被错误提升为 safety contour。
+
+修复后 Python 与 Web runtime witness 均 PASS。
+
+## 3. Release 影响
+
+完整扫描当前九州 v5 的 5064 个 PBF，s52_runtime_csp=DEPCNT02 且 s52_source_object_class=DEPARE 的 feature 数为 0。因此当前 release 没有实际受影响对象，本次无需重建九州 release；代码修复保证未来出现该分支时行为与 OpenCPN 一致。
+
+## 4. Gate A-I
+
+| Gate | 状态 | 结论 |
+|---|---|---|
+| A OPENCPN_FLOW_EQUIVALENCE | FAIL | $AREAS II25→BACKGROUND normalization remains absent; lookup '?' scoring/numeric/fallback semantics are not fully identical to the fixed parser. |
+| B CSP_BRANCH_EQUIVALENCE | PASS | All 206 branch rows have no remaining confirmed CSP branch mismatch after the RC-039 DEPCNT control-flow fix. |
+| C NESTED_CSP_CALL_GRAPH | PASS | Phase A/C witnesses prove ordered OBSTRN/WRECKS quality, name and sounding suffix expansion. |
+| D INSTRUCTION_SEQUENCE_EQUIVALENCE | PASS | Versioned mixed-opcode rule IR preserves lookup+CSP order and structured TX operands. |
+| E RUNTIME_OPCODE_COVERAGE | PASS | Generic executor and specialized SOUNDG/LIGHTS/CA paths execute the required ordered opcodes; missing DANGER53 does not discard the suffix. |
+| F REAL_DATA_BRANCH_COVERAGE | NOT_PROVEN | The v5 release is complete, but delivery fields do not uniquely reconstruct every source predicate/association/view state. |
+| G RESOURCE_DEPENDENCY_EQUIVALENCE | NOT_PROVEN | The local resource contract passes, but the fixed OpenCPN snapshot contains no independent chartsymbols.xml; DANGER53/LOWACC03 equivalence remains unprovable. |
+| H MARINER_DEPENDENCY_EQUIVALENCE | PASS | Mariner-dependent depth/height/boundary/category/SCAMIN paths are covered by phase witnesses plus the corrected DEPCNT DEPARE safety-contour control flow. |
+| I RENDER_ORDER_EQUIVALENCE | NOT_PROVEN | OP no-op and multi-LS execution are corrected; cross-object/global pass interleaving is still outside the available snapshot and witnesses. |
+
+## 5. 交付
+
+- 机器审计：build/audits/cm95_s52_opencpn_code_first_equivalence_v4.json
+- RC-039 证据：build/audits/cm95_s52_rc039_depcnt_control_flow_fix_v1.json
+- 代码 commit：1dbe1fde07ed64b39893de7d7e6ec5ce77cab871

docs/报告/CM95_S52_RC039_DEPCNT控制流修复报告_v1.md

@@ -0,0 +1,17 @@
+# CM95 S-52 RC-039 DEPCNT 控制流修复报告 v1
+
+日期：2026-09-21。
+
+## 结论
+
+RC-039 已修复并通过 Python / Web runtime 双 witness。正确根因是 OpenCPN 嵌套 if/else 在 CM95 中被错误压平成 if/elif，不是 DRVAL2 的 +0.01 规范化问题。
+
+- Branch：DC-DEC-DEP-LOW
+- 修复 commit：1dbe1fde07ed64b39893de7d7e6ec5ce77cab871
+- Python witness：PASS
+- Web runtime witness：PASS
+- 当前九州 v5 release 受影响 feature：0
+- Code-First v4：PASS 121 / FAIL 0 / NOT_PROVEN 85
+- Gate B：PASS
+- Gate H：PASS
+- Target Portrayal：FAIL（Gate A 仍 FAIL；Gate F/G/I 为 NOT_PROVEN）

tools/cm95_s52_code_first_reaudit_v4.py

@@ -0,0 +1,217 @@
+#!/usr/bin/env python3
+from __future__ import annotations
+from copy import deepcopy
+from collections import Counter
+from datetime import date
+from pathlib import Path
+import json, subprocess, sys
+
+ROOT=Path(__file__).resolve().parents[1]
+V3=ROOT/"build/audits/cm95_s52_opencpn_code_first_equivalence_v3.json"
+V4=ROOT/"build/audits/cm95_s52_opencpn_code_first_equivalence_v4.json"
+RPT=ROOT/"docs/报告/CM95_S52_OpenCPN渲染流程对照审计报告_v4.md"
+FIXJ=ROOT/"build/audits/cm95_s52_rc039_depcnt_control_flow_fix_v1.json"
+FIXR=ROOT/"docs/报告/CM95_S52_RC039_DEPCNT控制流修复报告_v1.md"
+REL=ROOT/"build/releases-s52-v2/cm95-d1-62a85bd40d3a-d6627c77efec"
+BRANCH="DC-DEC-DEP-LOW"
+
+sys.path.insert(0,str(ROOT))
+from src.cm95pbf.csp import S52MarinerSettings, resolve_depcnt02_instruction
+
+def head():
+    return subprocess.check_output(["git","rev-parse","HEAD"],cwd=ROOT,text=True).strip()
+
+def python_witness():
+    s=S52MarinerSettings(safety_contour_m=3)
+    cases=[
+        ("low-no-cross",{"DRVAL1":2,"DRVAL2":2},2,"LS(SOLD,1,DEPCN)",False),
+        ("cross-safety",{"DRVAL1":2,"DRVAL2":3},2,"LS(SOLD,2,DEPSC)",True),
+        ("deep-next-safe",{"DRVAL1":4,"DRVAL2":5},4,"LS(SOLD,2,DEPSC)",True),
+    ]
+    out=[]
+    for name,attrs,nxt,ei,es in cases:
+        inst,safe=resolve_depcnt02_instruction("DEPARE",attrs,s,next_safe_contour_m=nxt)
+        assert (inst,safe)==(ei,es),(name,inst,safe)
+        out.append({"case":name,"instruction":inst,"safe":safe})
+    return out
+
+def js_witness():
+    js=r"""
+const rt=require(process.cwd()+"/web/s52_runtime_executor.js");
+const settings=Object.assign({},rt.DEFAULTS,{safetyContourM:3});
+function ops(r){return r.map(x=>({opcode:x.opcode,args:x.args}));}
+const cases=[
+ ["low-no-cross",{s52_source_object_class:"DEPARE",depth_min_m:2,depth_max_m:2,s52_quapos_code:0},2,[{opcode:"LS",args:["SOLD","1","DEPCN"]}]],
+ ["cross-safety",{s52_source_object_class:"DEPARE",depth_min_m:2,depth_max_m:3,s52_quapos_code:0},2,[{opcode:"SE",args:[]},{opcode:"LS",args:["SOLD","2","DEPSC"]}]],
+ ["deep-next-safe",{s52_source_object_class:"DEPARE",depth_min_m:4,depth_max_m:5,s52_quapos_code:0},4,[{opcode:"SE",args:[]},{opcode:"LS",args:["SOLD","2","DEPSC"]}]],
+ ["depcnt-mariner-exact",{s52_source_object_class:"DEPCNT",contour_depth_m:3,s52_quapos_code:0},4,[{opcode:"SE",args:[]},{opcode:"LS",args:["SOLD","2","DEPSC"]}]]
+];
+const out=[];
+for(const [name,props,eff,expected] of cases){
+ const got=ops(rt.dynamicRules("DEPCNT02",props,settings,{effectiveSafetyContourM:eff}));
+ if(JSON.stringify(got)!==JSON.stringify(expected))throw new Error(name+" got="+JSON.stringify(got));
+ out.push({case:name,operations:got});
+}
+process.stdout.write(JSON.stringify(out));
+"""
+    raw=subprocess.check_output(["node","-e",js],cwd=ROOT,text=True)
+    return json.loads(raw)
+
+def release_affected_count():
+    import mapbox_vector_tile
+    count=0
+    for p in REL.rglob("*.pbf"):
+        try:d=mapbox_vector_tile.decode(p.read_bytes())
+        except Exception: continue
+        for lv in d.values():
+            for f in lv.get("features",[]):
+                props=f.get("properties") or {}
+                if props.get("s52_runtime_csp")=="DEPCNT02" and props.get("s52_source_object_class")=="DEPARE":
+                    count+=1
+    return count
+
+def main():
+    src=json.loads(V3.read_text())
+    pyw=python_witness()
+    jsw=js_witness()
+    affected=release_affected_count()
+
+    v4=deepcopy(src)
+    v4["schema"]="cm95.s52.opencpn-code-first-equivalence-audit/v4"
+    v4["date"]=str(date.today())
+    v4["cm95_head"]=head()
+    b=next(x for x in v4["branches"] if x["branch_id"]==BRANCH)
+    b["status"]="PASS"
+    b["observation_status"]="PASS"
+    b["cm95_python"]={
+        "status":"PASS",
+        "observed_sequence_or_behavior":["DRVAL1=2, DRVAL2=2, safety=3, chart_next=2 -> LS(SOLD,1,DEPCN)"],
+        "observation_method":"direct executable RC-039 witness after control-flow fix",
+    }
+    b["current_observed"]="OpenCPN nested control flow reproduced: next-safe fallback is not evaluated when DRVAL1<=safety_contour and DRVAL2<safety_contour."
+    b["unresolved_items"]=[]
+    b["re_adjudication"]={
+        "status":"PASS",
+        "method":"fixed OpenCPN source trace + Python witness + JS runtime witness",
+        "rationale":"CM95 now preserves OpenCPN nested if/else: chart next-safe-contour fallback is only reachable when DRVAL1 is deeper than the mariner safety contour.",
+        "witnesses":["rc039-python","rc039-js"],
+    }
+    b["pbf_or_runtime_facts"]={
+        "status":"PASS",
+        "description":"runtime fact materialization carries DRVAL1/DRVAL2 for DEPCNT02 on LINE DEPARE; current v5 Kyushu release contains zero such features, so no release rebuild is required for this fix.",
+    }
+    counts=Counter(x["status"] for x in v4["branches"])
+    assert counts==Counter({"PASS":121,"NOT_PROVEN":85}),counts
+    v4["branch_status_counts"]={"PASS":121,"FAIL":0,"NOT_PROVEN":85}
+
+    for g in v4["gates"]:
+        if g["gate"]=="B":
+            g["status"]="PASS"
+            g["reason"]="All 206 branch rows have no remaining confirmed CSP branch mismatch after the RC-039 DEPCNT control-flow fix."
+        elif g["gate"]=="H":
+            g["status"]="PASS"
+            g["reason"]="Mariner-dependent depth/height/boundary/category/SCAMIN paths are covered by phase witnesses plus the corrected DEPCNT DEPARE safety-contour control flow."
+    v4["status"]="FAIL"
+    v4["target_portrayal"]={
+        "status":"FAIL",
+        "scope":"Branch FAIL count is zero; Gate A remains FAIL and Gates F/G/I remain NOT_PROVEN."
+    }
+    v4["unresolved_items"]=[
+        "$AREAS II25 normalization and remaining lookup parser semantic differences",
+        "source-level unique real-data branch assignment",
+        "independent fixed-baseline chartsymbols resource equivalence",
+        "cross-object/global render-pass interleaving",
+    ]
+    v4["v4_rc039_fix"]={
+        "commit":head(),
+        "corrected_root_cause":"CM95 flattened OpenCPN nested DEPARE DEPCNT02 if/else into an if/elif, incorrectly allowing next-safe-contour fallback after the shallow interval branch failed.",
+        "python_witness":pyw,
+        "js_runtime_witness":jsw,
+        "current_release_affected_feature_count":affected,
+        "release_rebuild_required":False,
+    }
+    V4.write_text(json.dumps(v4,ensure_ascii=False,indent=2)+"\n")
+
+    fix={
+        "schema":"cm95.s52.rc039-depcnt-control-flow-fix/v1",
+        "date":str(date.today()),
+        "status":"PASS",
+        "branch_id":BRANCH,
+        "commit":head(),
+        "opencpn_behavior":"For LINE DEPARE, when DRVAL1<=safety_contour, only DRVAL2>=safety_contour can set safe=true. The chart next-safe-contour fallback belongs exclusively to the outer else branch where DRVAL1>safety_contour.",
+        "previous_incorrect_audit_explanation":"DRVAL2<=DRVAL1 must be normalized to DRVAL1+0.01 before DEPCNT02 safety selection.",
+        "correct_root_cause":"Nested OpenCPN if/else was flattened into CM95 if/elif, making the next-safe fallback reachable in a branch where OpenCPN never evaluates it.",
+        "python_witness":pyw,
+        "js_runtime_witness":jsw,
+        "kyushu_v5_release_affected_feature_count":affected,
+        "rebuild_required":False,
+        "code_first_v4_counts":{"PASS":121,"FAIL":0,"NOT_PROVEN":85},
+        "gates":{"A":"FAIL","B":"PASS","C":"PASS","D":"PASS","E":"PASS","F":"NOT_PROVEN","G":"NOT_PROVEN","H":"PASS","I":"NOT_PROVEN"},
+        "target_portrayal":"FAIL",
+    }
+    FIXJ.write_text(json.dumps(fix,ensure_ascii=False,indent=2)+"\n")
+
+    gate_rows="\n".join(f"| {g['gate']} {g['name']} | {g['status']} | {g['reason']} |" for g in v4["gates"])
+    RPT.write_text(f"""# CM95 S-52 OpenCPN 渲染流程对照审计报告 v4
+
+日期：{date.today()}。固定 OpenCPN baseline：{v4['opencpn_commit']}。
+
+## 1. 结论
+
+RC-039 修复后，206 条 branch 重新判定为：
+
+| PASS | FAIL | NOT_PROVEN | 合计 |
+|---:|---:|---:|---:|
+| 121 | 0 | 85 | 206 |
+
+Branch 层面的确认 FAIL 已清零。Target Portrayal 仍为 FAIL，原因不是 branch FAIL，而是 Gate A 仍 FAIL，Gate F/G/I 仍为 NOT_PROVEN。
+
+## 2. RC-039 正确根因
+
+v3 residual 将问题解释为“DEPCNT02 应先把 DRVAL2<=DRVAL1 规范化为 DRVAL1+0.01”，该解释不符合固定 OpenCPN 源码。
+
+固定源码真实控制流是：当 DRVAL1 <= safety_contour 时，只检查 DRVAL2 >= safety_contour；只有 DRVAL1 > safety_contour 时，才进入 outer else 并比较 chart next-safe-contour。
+
+CM95 原实现把这个嵌套 if/else 压平成 if/elif，导致 DRVAL1=2, DRVAL2=2, safety=3, chart_next=2 被错误提升为 safety contour。
+
+修复后 Python 与 Web runtime witness 均 PASS。
+
+## 3. Release 影响
+
+完整扫描当前九州 v5 的 5064 个 PBF，s52_runtime_csp=DEPCNT02 且 s52_source_object_class=DEPARE 的 feature 数为 {affected}。因此当前 release 没有实际受影响对象，本次无需重建九州 release；代码修复保证未来出现该分支时行为与 OpenCPN 一致。
+
+## 4. Gate A-I
+
+| Gate | 状态 | 结论 |
+|---|---|---|
+{gate_rows}
+
+## 5. 交付
+
+- 机器审计：build/audits/cm95_s52_opencpn_code_first_equivalence_v4.json
+- RC-039 证据：build/audits/cm95_s52_rc039_depcnt_control_flow_fix_v1.json
+- 代码 commit：{head()}
+""",encoding="utf-8")
+
+    FIXR.write_text(f"""# CM95 S-52 RC-039 DEPCNT 控制流修复报告 v1
+
+日期：{date.today()}。
+
+## 结论
+
+RC-039 已修复并通过 Python / Web runtime 双 witness。正确根因是 OpenCPN 嵌套 if/else 在 CM95 中被错误压平成 if/elif，不是 DRVAL2 的 +0.01 规范化问题。
+
+- Branch：{BRANCH}
+- 修复 commit：{head()}
+- Python witness：PASS
+- Web runtime witness：PASS
+- 当前九州 v5 release 受影响 feature：{affected}
+- Code-First v4：PASS 121 / FAIL 0 / NOT_PROVEN 85
+- Gate B：PASS
+- Gate H：PASS
+- Target Portrayal：FAIL（Gate A 仍 FAIL；Gate F/G/I 为 NOT_PROVEN）
+""",encoding="utf-8")
+    print(json.dumps({"counts":v4["branch_status_counts"],"affected_release_features":affected,"head":head()},ensure_ascii=False))
+
+if __name__=="__main__":
+    main()