tei/CM95
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

docs: complete S-52 root cause fix audit

Browse Source
This commit is contained in:
OpenAI Codex
2026-09-21 09:10:14 +08:00
parent e1e3a9e00c
commit c1a9fa7a42
6 changed files with 32367 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

314
docs/报告/CM95_S52_OpenCPN渲染流程对照审计报告_v3.md Normal file
View File

@@ -0,0 +1,314 @@
# CM95 S-52 OpenCPN 渲染流程对照审计报告 v3
日期：2026-09-21。固定 OpenCPN baseline：`f7211b4e1874c453e37a7f190aa191c55a25c32e`。
## 1. 最终结论
**Target Portrayal：FAIL。** 本轮没有运行 production build，也没有重新生成 release。v5 production 只读核验为 **5065/5065 jobs PASS、5064 PBF、476120 features**。
206 条 branch record 已逐条从 v2 矩阵重新判定，结果不是用旧 FAIL 数做减法：
| PASS | FAIL | NOT_PROVEN | 合计 |
|---:|---:|---:|---:|
| 120 | 1 | 85 | 206 |
唯一 branch FAIL 是 `DC-DEC-DEP-LOW`。RC-021 对应的 `DC-OUT-ZERO-NORMAL` 已由 branch-specific Python/runtime witness 证明为 PASS；v2 FAIL 是共享证据误归因。
## 2. 固定输入与方法
- v2 矩阵：`build/audits/cm95_s52_opencpn_code_first_equivalence_v2.json`，206/206 记录全部保留并重判。
- production plan：`build/production/cm95_s52_kyushu_production_plan_v5_ordered_rule_ir.json`，plan id `d6627c77efec38d1fcd9f398870cd19519e9e948ba4515e7357829aa10087f2b`。
- release：`build/releases-s52-v2/cm95-d1-62a85bd40d3a-d6627c77efec`。
- phase A/B/C/D witness 均重新执行并 PASS；未使用 Jest。
- 原 NOT_PROVEN 不因实现存在而猜成 PASS；85 条继续保持 NOT_PROVEN。一条旧 NOT_PROVEN 因精确 witness 得到反证，改为 FAIL。
- OpenCPN 校验清单 25/25 PASS；固定源码未替换、未联网补齐缺失资源。
## 3. 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 | FAIL | All 206 rows were re-adjudicated; DC-DEC-DEP-LOW is now a branch-specific confirmed mismatch. |
| 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 | FAIL | The DEPCNT DEPARE interval path does not normalize DRVAL2<=DRVAL1 before safe-contour selection. |
| 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. |
## 4. 生产与证据边界
ordered Rule IR 已进入 v5 builder contract，release summary 的 plan/release identity、jobs、PBF 和 feature 数一致。Gate F 仍为 NOT_PROVEN，因为交付 PBF 不能唯一恢复全部原始 presence/value、关联对象与视图状态；Gate G 仍受固定快照缺少独立 chartsymbols.xml 限制；Gate I 的跨对象全局 pass interleaving 没有被局部 executor witness 证明。
## 5. 206 条 branch 复判
### OBSTRN04
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| OB-D-VAL | VALSOU != UNKNOWN(1e6) | depth=VALSOU; precompute S(VALSOU); execute terminal OB branch | full Object→Lookup→consumer equivalence and rendering parameters not proven | NOT_PROVEN |
| OB-D-EXPSOU | VALSOU absent; EXPSOU=1 | depth=UNKNOWN → _UDWHAZ03(depth) → terminal OB branch | upstream _DEPVAL01 always UNKNOWN; CM95 uses actual min DRVAL1 for AREA | NOT_PROVEN |
| OB-D-FOUL | VALSOU absent; EXPSOU!=1; CATOBS=6 | depth=0.01 → _UDWHAZ03(depth) → terminal OB branch | upstream _DEPVAL01 always UNKNOWN; CM95 uses actual min DRVAL1 for AREA | NOT_PROVEN |
| OB-D-AWASH | VALSOU absent; EXPSOU!=1; CATOBS!=6; WATLEV=5 | depth=0 → _UDWHAZ03(depth) → terminal OB branch | upstream _DEPVAL01 always UNKNOWN; CM95 uses actual min DRVAL1 for AREA | NOT_PROVEN |
| OB-D-SUBMERGED | VALSOU absent; EXPSOU!=1; CATOBS!=6; WATLEV=3 | depth=0.01 → _UDWHAZ03(depth) → terminal OB branch | upstream _DEPVAL01 always UNKNOWN; CM95 uses actual min DRVAL1 for AREA | NOT_PROVEN |
| OB-D-DEFAULT | VALSOU absent; EXPSOU!=1; CATOBS!=6; WATLEV otherwise | depth=-15 → _UDWHAZ03(depth) → terminal OB branch | upstream _DEPVAL01 always UNKNOWN; CM95 uses actual min DRVAL1 for AREA | NOT_PROVEN |
| OB-P-ISO | _UDWHAZ03 returns nonempty | SY(ISODGR51) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-ROCK-AWASH | U empty; UWTROC; V<=20; WATLEV∈{4,5} | SY(UWTROC04) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-ROCK-OTHER | U empty; UWTROC; V<=20; WATLEV absent/3/other | SY(DANGER51) → S(V) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-OBS-ABSENT | U empty; OBSTRN; V<=20; WATLEV absent | SY(DANGER01) → S(V) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-OBS-DRY | U empty; OBSTRN; V<=20; WATLEV∈{1,2} | SY(LNDARE01) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-OBS-SUBMERGED | U empty; OBSTRN; V<=20; WATLEV=3 | SY(DANGER52) → S(V) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-OBS-AWASH | U empty; OBSTRN; V<=20; WATLEV∈{4,5} | SY(DANGER53) → S(V) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-OBS-OTHER | U empty; OBSTRN; V<=20; WATLEV other | SY(DANGER51) → S(V) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-DEEP | U empty; VALSOU>20; either class | SY(DANGER52) → S(V) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-ROCK-NOV-DRY | U empty; V absent; UWTROC; WATLEV=2 | SY(LNDARE01) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-ROCK-NOV-SUB | U empty; V absent; UWTROC; WATLEV=3 | SY(UWTROC03) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-ROCK-NOV-OTHER | U empty; V absent; UWTROC; WATLEV absent/other | SY(UWTROC04) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-OBS-NOV-DRY | U empty; V absent; OBSTRN; WATLEV∈{1,2} | SY(OBSTRN11) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-OBS-NOV-AWASH | U empty; V absent; OBSTRN; WATLEV∈{4,5} | SY(OBSTRN03) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-P-OBS-NOV-OTHER | U empty; V absent; OBSTRN; WATLEV absent/3/other | SY(OBSTRN01) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-L-QLOW | Q.Len()>1 (QUAPOS 2..9) | ToLong(Q string) into uninitialized long; conditional LC(LOWACC41/31); then T | actual Q is ;SY(...)+separator, not numeric; unchecked ToLong/uninitialized quapos: do not invent deterministic expected LC | NOT_PROVEN |
| OB-L-ISO | Q.Len()<=1; U nonempty | LS(DOTT,2,CHBLK) → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-L-SHALLOW | Q.Len()<=1; U empty; V present<=20 | LS(DOTT,2,CHBLK) → S(V) → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-L-DEEP | Q.Len()<=1; U empty; V>20 | LS(DASH,2,CHBLK) → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-L-NOV | Q.Len()<=1; U empty; V absent | LS(DOTT,2,CHBLK) → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-A-ISO | U nonempty | AC(DEPVS) → AP(FOULAR01) → LS(DOTT,2,CHBLK) → SY(ISODGR51) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-A-SHALLOW | U empty; V<=20 | LS(DOTT,2,CHBLK) → S(V) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-A-DEEP | U empty; V>20 | LS(DASH,2,CHBLK) → S(V) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-A-DRY | U empty; V absent; WATLEV∈{1,2} | AC(CHBRN) → LS(SOLD,2,CSTLN) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-A-AWASH | U empty; V absent; WATLEV=4 | AC(DEPIT) → LS(DASH,2,CSTLN) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-A-FOUL | U empty; V absent; WATLEV∈{3,5}; CATOBS=6 | AC(DEPVS) → AP(FOULAR01) → LS(DOTT,2,CHBLK) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-A-DEFAULT | U empty; V absent; remaining WATLEV/CATOBS | AC(DEPVS) → LS(DOTT,2,CHBLK) → Q → T | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-T-PRESENT | OBJNAM attribute exists (including empty string) | terminal prefix → Q or S as terminal specifies → TX(OBJNAM,1,2,3,'15118',-1,-1,CHBLK,26) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| OB-T-ABSENT | OBJNAM missing | terminal prefix → Q or S as terminal specifies | OB-T is the T macro; text rendering still has separate visibility gates | NOT_PROVEN |
### WRECKS02
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| WK-D-VAL | V present | depth=V → U unless QUASOU contains 7 → terminal WK branch | fixed _DEPVAL01 is stub; unsupported present CATWRK leaves UNKNOWN upstream | NOT_PROVEN |
| WK-D-CAT1 | V absent; CATWRK=1 | depth=20 → U unless QUASOU contains 7 → terminal WK branch | fixed _DEPVAL01 is stub; unsupported present CATWRK leaves UNKNOWN upstream | NOT_PROVEN |
| WK-D-CAT2 | V absent; CATWRK=2 | depth=0 → U unless QUASOU contains 7 → terminal WK branch | fixed _DEPVAL01 is stub; unsupported present CATWRK leaves UNKNOWN upstream | NOT_PROVEN |
| WK-D-CAT45 | V absent; CATWRK∈{4,5} | depth=-15 → U unless QUASOU contains 7 → terminal WK branch | fixed _DEPVAL01 is stub; unsupported present CATWRK leaves UNKNOWN upstream | NOT_PROVEN |
| WK-D-CATOTHER | V absent; CATWRK present not 1/2/4/5 | depth=UNKNOWN → U unless QUASOU contains 7 → terminal WK branch | fixed _DEPVAL01 is stub; unsupported present CATWRK leaves UNKNOWN upstream | NOT_PROVEN |
| WK-D-WAT3 | V absent; CATWRK absent; WATLEV=3 | depth=0.01 → U unless QUASOU contains 7 → terminal WK branch | fixed _DEPVAL01 is stub; unsupported present CATWRK leaves UNKNOWN upstream | NOT_PROVEN |
| WK-D-WAT5 | V absent; CATWRK absent; WATLEV=5 | depth=0 → U unless QUASOU contains 7 → terminal WK branch | fixed _DEPVAL01 is stub; unsupported present CATWRK leaves UNKNOWN upstream | NOT_PROVEN |
| WK-D-WATDRY | V absent; CATWRK absent; WATLEV absent/1/2/4/6 | depth=-15 → U unless QUASOU contains 7 → terminal WK branch | fixed _DEPVAL01 is stub; unsupported present CATWRK leaves UNKNOWN upstream | NOT_PROVEN |
| WK-D-WATOTHER | V absent; CATWRK absent; WATLEV other | depth=UNKNOWN → U unless QUASOU contains 7 → terminal WK branch | fixed _DEPVAL01 is stub; unsupported present CATWRK leaves UNKNOWN upstream | NOT_PROVEN |
| WK-U-SKIP7 | QUASOU contains 7 | U=empty; quasou=7 → Q → terminal WK branch | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-P-ISO | U nonempty | SY(ISODGR51) → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-P-V-LT-Q0 | U empty; V < safety_contour; QUASOU excludes 7 | SY(DANGER51) → TX('Wk',3,1,2,'15110',2,0,CHBLK,21) → S(V) → U(empty) → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-P-V-LT-Q7 | U empty; V < safety_contour; QUASOU contains 7 | SY(DANGER51) → TX('Wk',3,1,2,'15110',2,0,CHBLK,21) → SY(WRECKS07) → S(V) → U(empty) → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-P-V-GE-Q0 | U empty; V >= safety_contour; QUASOU excludes 7 | SY(DANGER52) → TX('Wk',3,1,2,'15110',2,0,CHBLK,21) → S(V) → U(empty) → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-P-V-GE-Q7 | U empty; V >= safety_contour; QUASOU contains 7 | SY(DANGER52) → TX('Wk',3,1,2,'15110',2,0,CHBLK,21) → SY(WRECKS07) → S(V) → U(empty) → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-P-NOV-CAT1 | U empty; V absent; CATWRK=1 and WATLEV=3 | SY(WRECKS04) → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-P-NOV-CAT2 | U empty; V absent; CATWRK=2 and WATLEV=3 | SY(WRECKS05) → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-P-NOV-DRY | U empty; V absent; both attrs present; (CATWRK∈{4,5} or WATLEV∈{1,2,4,5}) | SY(WRECKS01) → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-P-NOV-OTHER | U empty; V absent; both attrs present; remaining values | SY(WRECKS05) → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-P-NOV-MISSING | U empty; V absent; CATWRK or WATLEV absent | Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-LINE-QLOW | QUAPOS∈[2,9] | LC(LOWACC41) → WK-TAIL selected by V/WATLEV | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-LINE-ISO | QUAPOS outside [2,9]; U nonempty | LS(DOTT,2,CHBLK) → WK-TAIL selected by V/WATLEV | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-LINE-VALSH | accurate; U empty; V<=20 | LS(DOTT,2,CHBLK) → WK-TAIL selected by V/WATLEV | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-LINE-VALDP | accurate; U empty; V>20 | LS(DASH,2,CHBLK) → WK-TAIL selected by V/WATLEV | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-LINE-DRY | accurate; U empty; V absent; WATLEV∈{1,2} | LS(SOLD,2,CSTLN) → WK-TAIL selected by V/WATLEV | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-LINE-AWASH | accurate; U empty; V absent; WATLEV=4 | LS(DASH,2,CSTLN) → WK-TAIL selected by V/WATLEV | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-LINE-DEFAULT | accurate; U empty; V absent; WATLEV other/absent | LS(DOTT,2,CSTLN) → WK-TAIL selected by V/WATLEV | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-TAIL-SHALLOW | V present<=20 | WK-LINE selected above → U → Q → S(V) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-TAIL-DEEP | V>20 | WK-LINE selected above → U → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-TAIL-DRY | V absent; WATLEV∈{1,2} | WK-LINE selected above → AC(CHBRN) → U → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-TAIL-AWASH | V absent; WATLEV=4 | WK-LINE selected above → AC(DEPIT) → U → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| WK-TAIL-DEFAULT | V absent; WATLEV other/absent | WK-LINE selected above → AC(DEPVS) → U → Q | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
### UDWHAZ03
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| UD-PUBLIC | direct CS(UDWHAZ03) | — | public registered function returns NULL; hazard callers use _UDWHAZ03 helper, not this entry | NOT_PROVEN |
| UD-UNKNOWN-DANGER | depth=UNKNOWN; EXPSOU!=1 | danger=true → UD-OUT according to danger and WATLEV | fixed snapshot lacks GetAssociatedObjects implementation; summary membership equality not proven | NOT_PROVEN |
| UD-UNKNOWN-EXPOSED | depth=UNKNOWN; EXPSOU=1 | association scan; AREA cannot promote; LINE DRVAL2<SC may promote → UD-OUT according to danger and WATLEV | fixed snapshot lacks GetAssociatedObjects implementation; summary membership equality not proven | NOT_PROVEN |
| UD-KNOWN-DEEP | known depth>SC; EXPSOU attribute ignored | danger=false → UD-OUT according to danger and WATLEV | fixed snapshot lacks GetAssociatedObjects implementation; summary membership equality not proven | NOT_PROVEN |
| UD-KNOWN-SHALLOW | known depth<=SC; local expsou remains 0 | association scan → UD-OUT according to danger and WATLEV | fixed snapshot lacks GetAssociatedObjects implementation; summary membership equality not proven | NOT_PROVEN |
| UD-ASSOC-LINE | eligible scan; any associated GEO_LINE DRVAL2(default0)<SC | danger=true → UD-OUT according to danger and WATLEV | fixed snapshot lacks GetAssociatedObjects implementation; summary membership equality not proven | NOT_PROVEN |
| UD-ASSOC-AREA | eligible scan; any associated nonline DRVAL1(default0)>=SC and local expsou!=1 | danger=true → UD-OUT according to danger and WATLEV | fixed snapshot lacks GetAssociatedObjects implementation; summary membership equality not proven | NOT_PROVEN |
| UD-ASSOC-NONE | eligible scan; no qualifying association or chart absent | danger=false → UD-OUT according to danger and WATLEV | fixed snapshot lacks GetAssociatedObjects implementation; summary membership equality not proven | NOT_PROVEN |
| UD-OUT-DRY | danger=true; WATLEV 1/2 | — | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| UD-OUT-WET | danger=true; WATLEV otherwise | SY(ISODGR51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| UD-OUT-SAFE | danger=false | — | upstream b_promote always false; DisplayBase is direct mutation, not OP; JS does not emit category | NOT_PROVEN |
### SOUNDG03
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| SG-CLAMP-HIGH | input>40000 | prelude(SG-CLAMP/UNIT/PREFIX) → B1 if swept → C2 if unreliable → SG-DIGITS selected by adjusted d | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-CLAMP-LOW | input<-1000 | prelude(SG-CLAMP/UNIT/PREFIX) → B1 if swept → C2 if unreliable → SG-DIGITS selected by adjusted d | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-METRES | unit neither 0 nor 2 | prelude(SG-CLAMP/UNIT/PREFIX) → B1 if swept → C2 if unreliable → SG-DIGITS selected by adjusted d | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-FEET | unit=0 | prelude(SG-CLAMP/UNIT/PREFIX) → B1 if swept → C2 if unreliable → SG-DIGITS selected by adjusted d | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-FATHOMS | unit=2 | prelude(SG-CLAMP/UNIT/PREFIX) → B1 if swept → C2 if unreliable → SG-DIGITS selected by adjusted d | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-SHALLOW | d after signed .01 adjustment <= converted SD | prelude(SG-CLAMP/UNIT/PREFIX) → B1 if swept → C2 if unreliable → SG-DIGITS selected by adjusted d | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-DEEP | adjusted d > converted SD | prelude(SG-CLAMP/UNIT/PREFIX) → B1 if swept → C2 if unreliable → SG-DIGITS selected by adjusted d | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-SWEPT | TECSOU contains6 | prelude(SG-CLAMP/UNIT/PREFIX) → B1 if swept → C2 if unreliable → SG-DIGITS selected by adjusted d | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-QUALITY | QUASOU intersects{3,4,5,8,9} or STATUS contains18 else QUAPOS∈[2,9] | prelude(SG-CLAMP/UNIT/PREFIX) → B1 if swept → C2 if unreliable → SG-DIGITS selected by adjusted d | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-DIGITS-ONE | abs(d)<10; feet rounding may fall through | SY(prefixB1) if swept → SY(prefixC2) if unreliable → SY(prefix1a) → SY(prefix5f) if f>0 → SY(prefixA1) if negative | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-DIGITS-TWO-FRACTION | abs(d)<31; fractional remainder !=0 | SY(prefixB1) if swept → SY(prefixC2) if unreliable → SY(prefix2a) if leading>=10 → SY(prefix1b) → SY(prefix5f) if f>0 and !feet → SY(prefixA1) if negative | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-DIGITS-TWO-NEG | previous branches not returned; abs(d)<100; d<0 | SY(prefixB1) if swept → SY(prefixC2) if unreliable → SY(prefix2a) → SY(prefix1b) → SY(prefixA1) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-DIGITS-TWO-POS | previous branches not returned; abs(d)<100; d>=0 | SY(prefixB1) if swept → SY(prefixC2) if unreliable → SY(prefix1a) → SY(prefix0b) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-DIGITS-THREE | previous branches not returned; d<1000 (signed compare) | SY(prefixB1) if swept → SY(prefixC2) if unreliable → SY(prefix2a) → SY(prefix1b) → SY(prefix0c) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-DIGITS-FOUR | previous branches not returned; d<10000 | SY(prefixB1) if swept → SY(prefixC2) if unreliable → SY(prefix2a) → SY(prefix1b) → SY(prefix0c) → SY(prefix4d) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SG-DIGITS-FIVE | remaining | SY(prefixB1) if swept → SY(prefixC2) if unreliable → SY(prefix3a) → SY(prefix2b) → SY(prefix1c) → SY(prefix0d) → SY(prefix4e) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
### SOUNDG02
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| MP-SPLIT | CS(SOUNDG02) reached | MP() → RenderMPS: for every point CS(SOUNDG03) → SNDFRM02(z) → ordered SY glyphs | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
### DEPARE01/DEPARE02
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| DA-ALIAS | CS(DEPARE02) | same DEPARE01 branch tree | full Object→Lookup→consumer equivalence and rendering parameters not proven | NOT_PROVEN |
| DA-INTERTIDAL | base: d1<0 or d2<=0; no later override | AC(DEPIT) → AP(DRGARE01),LS(DASH,1,CHGRF) iff DRGARE | assumes both DRVALs initialized. runtime lacks two_shades and DRGARE suffix; fixed hardcoded color/opacity differs from palette contract | NOT_PROVEN |
| DA-VERYSHALLOW | base: d1>=0 and d2>0; no later override | AC(DEPVS) → AP(DRGARE01),LS(DASH,1,CHGRF) iff DRGARE | assumes both DRVALs initialized. runtime lacks two_shades and DRGARE suffix; fixed hardcoded color/opacity differs from palette contract | NOT_PROVEN |
| DA-TWO-DEEP | two_shades=true; d1>=SC and d2>SC | AC(DEPDW) → AP(DRGARE01),LS(DASH,1,CHGRF) iff DRGARE | assumes both DRVALs initialized. runtime lacks two_shades and DRGARE suffix; fixed hardcoded color/opacity differs from palette contract | NOT_PROVEN |
| DA-FOUR-SHALLOW | !two_shades; d1>=shallow and d2>shallow; no later override | AC(DEPMS) → AP(DRGARE01),LS(DASH,1,CHGRF) iff DRGARE | assumes both DRVALs initialized. runtime lacks two_shades and DRGARE suffix; fixed hardcoded color/opacity differs from palette contract | NOT_PROVEN |
| DA-FOUR-SAFE | !two_shades; d1>=SC and d2>SC; no deep override | AC(DEPMD) → AP(DRGARE01),LS(DASH,1,CHGRF) iff DRGARE | assumes both DRVALs initialized. runtime lacks two_shades and DRGARE suffix; fixed hardcoded color/opacity differs from palette contract | NOT_PROVEN |
| DA-FOUR-DEEP | !two_shades; d1>=deep and d2>deep | AC(DEPDW) → AP(DRGARE01),LS(DASH,1,CHGRF) iff DRGARE | assumes both DRVALs initialized. runtime lacks two_shades and DRGARE suffix; fixed hardcoded color/opacity differs from palette contract | NOT_PROVEN |
| DA-DRG-NOD1 | DRGARE and DRVAL1 absent | AC(DEPMD) → AP(DRGARE01) → LS(DASH,1,CHGRF) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| DA-BAD-RANGE | DRVAL2<=DRVAL1 | DRVAL2=DRVAL1+0.01 → selected AC + DRGARE suffix | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| DA-MISSING-D2 | DRVAL2 absent | NOT_PROVEN: uninitialized drval2 read upstream; do not assign an expected color | upstream undefined behavior; source presence missing in delivery does not prove absent in original | NOT_PROVEN |
### DEPCNT02
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| DC-DEC-DEP-RANGE | LINE DEPARE; d1<=SC and d2>=SC | safe=true → DC-OUT selected by QUAPOS and safe | Python DEPARE fallback may mark safe despite d1<=SC,d2<SC; chart catalog vs viewport catalog not proven | NOT_PROVEN |
| DC-DEC-DEP-LOW | LINE DEPARE; d1<=SC and d2<SC | safe=false → DC-OUT selected by QUAPOS and safe | DRVAL1=2, DRVAL2=2, chart_next=2 → LS(SOLD,2,DEPSC); expected LS(SOLD,1,DEPCN) | FAIL |
| DC-DEC-DEP-NEXT | LINE DEPARE; d1>SC | safe=(abs(d1-chart.next)<1e-4) → DC-OUT selected by QUAPOS and safe | Python DEPARE fallback may mark safe despite d1<=SC,d2<SC; chart catalog vs viewport catalog not proven | NOT_PROVEN |
| DC-DEC-CNT-EXACT | otherwise; VALDCO==SC | safe=true → DC-OUT selected by QUAPOS and safe | Python DEPARE fallback may mark safe despite d1<=SC,d2<SC; chart catalog vs viewport catalog not proven | NOT_PROVEN |
| DC-DEC-CNT-NEXT | otherwise; VALDCO!=SC | safe=(abs(VALDCO-chart.next)<1e-4) → DC-OUT selected by QUAPOS and safe | Python DEPARE fallback may mark safe despite d1<=SC,d2<SC; chart catalog vs viewport catalog not proven | NOT_PROVEN |
| DC-OUT-LOW-SAFE | QUAPOS∈[2,9] and safe | SAFECD Plain lookup INST; fallback LS(DASH,2,DEPSC) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| DC-OUT-LOW-NORMAL | QUAPOS∈[2,9] and !safe | LS(DASH,1,DEPCN) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| DC-OUT-ZERO-SAFE | QUAPOS absent/0 and safe | SAFECN Plain lookup INST; fallback LS(SOLD,2,DEPSC) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| DC-OUT-ZERO-NORMAL | QUAPOS absent/0 and !safe | LS(SOLD,1,DEPCN) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| DC-OUT-OTHER | QUAPOS nonzero outside [2,9] | — | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
### QUAPOS01/QUAPNT01/QUALIN01
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| QP-4 | QUAPOS=4 | SY(QUAPOS01) | local Python output matches; complete pipeline placement and source QUAPOS mapping not proven | NOT_PROVEN |
| QP-5 | QUAPOS=5 | SY(QUAPOS02) | local Python output matches; complete pipeline placement and source QUAPOS mapping not proven | NOT_PROVEN |
| QP-78 | QUAPOS∈{7,8} | SY(QUAPOS03) | local Python output matches; complete pipeline placement and source QUAPOS mapping not proven | NOT_PROVEN |
| QP-LOW | QUAPOS∈{2,3,6,9} | SY(LOWACC03) | LOWACC03 absent from CM95 resources; fixed XML not supplied | NOT_PROVEN |
| QP-ACCURATE | QUAPOS absent or outside [2,9] | — | local Python output matches; complete pipeline placement and source QUAPOS mapping not proven | NOT_PROVEN |
| QL-LOW | QUAPOS present in [2,9] | LC(LOWACC21) | local Python matches, consumer geometric fidelity unproven | NOT_PROVEN |
| QL-OTHER | QUAPOS present outside [2,9] | — | local Python matches, consumer geometric fidelity unproven | NOT_PROVEN |
| QL-RADAR | QUAPOS absent; class COALNE; CONRAD=1 | LS(SOLD,3,CHMGF) → LS(SOLD,1,CSTLN) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| QL-NORMAL | QUAPOS absent; other class or COALNE CONRAD absent/not1 | LS(SOLD,1,CSTLN) | local Python matches, consumer geometric fidelity unproven | NOT_PROVEN |
| QP-DISPATCH | QUAPOS01: GEO_LINE vs else | CSQUALIN01 for LINE else CSQUAPNT01 | direct QUALIN01/QUAPNT01 are registered upstream but absent resolve_csp_hints dispatch; internal Python helpers exist | NOT_PROVEN |
### SLCONS03
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| SL-P-LOW | QUAPOS present∈[2,9] | SY(LOWACC01) | AREA prefix remains even if cmdw empty; QUAPOS presence itself suppresses normal styling upstream | NOT_PROVEN |
| SL-P-OTHER | QUAPOS absent/outside [2,9] | — | AREA prefix remains even if cmdw empty; QUAPOS presence itself suppresses normal styling upstream | NOT_PROVEN |
| SL-LOW | QUAPOS present∈[2,9] | AP(CROSSX01) iff AREA → LC(LOWACC01) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SL-PRESENT-GOOD | QUAPOS present outside [2,9] | AP(CROSSX01) iff AREA | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| SL-CONDTN | QUAPOS absent; CONDTN∈{1,2} | AP(CROSSX01) iff AREA → LS(DASH,1,CSTLN) | AREA prefix remains even if cmdw empty; QUAPOS presence itself suppresses normal styling upstream | NOT_PROVEN |
| SL-WHARF | QUAPOS absent; previous false; CATSLC∈{6,15,16} | AP(CROSSX01) iff AREA → LS(SOLD,4,CSTLN) | AREA prefix remains even if cmdw empty; QUAPOS presence itself suppresses normal styling upstream | NOT_PROVEN |
| SL-DRY | QUAPOS absent; previous false; WATLEV=2 | AP(CROSSX01) iff AREA → LS(SOLD,2,CSTLN) | AREA prefix remains even if cmdw empty; QUAPOS presence itself suppresses normal styling upstream | NOT_PROVEN |
| SL-WET | QUAPOS absent; previous false; WATLEV∈{3,4} | AP(CROSSX01) iff AREA → LS(DASH,2,CSTLN) | AREA prefix remains even if cmdw empty; QUAPOS presence itself suppresses normal styling upstream | NOT_PROVEN |
| SL-OTHER | QUAPOS absent; remaining | AP(CROSSX01) iff AREA → LS(SOLD,2,CSTLN) | AREA prefix remains even if cmdw empty; QUAPOS presence itself suppresses normal styling upstream | NOT_PROVEN |
### RESTRN01
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| RE-ABSENT | RESTRN absent/empty | — | source uses octal 011..015 = decimal9..13; R={14} expected ENTRES51, Python ENTRES71; R={15} expected RSRDEF51, Python INFARE51 | NOT_PROVEN |
| RE-ENTRY-MIX | R∩{7,8,14}; R∩{1..6} | SY(ENTRES61) | source uses octal 011..015 = decimal9..13; R={14} expected ENTRES51, Python ENTRES71; R={15} expected RSRDEF51, Python INFARE51 | NOT_PROVEN |
| RE-ENTRY-INFO | R∩{7,8,14}; no {1..6}; R∩{9..13} | SY(ENTRES71) | source uses octal 011..015 = decimal9..13; R={14} expected ENTRES51, Python ENTRES71; R={15} expected RSRDEF51, Python INFARE51 | NOT_PROVEN |
| RE-ENTRY-ONLY | R∩{7,8,14}; no {1..6,9..13} | SY(ENTRES51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RE-ANCHOR-MIX | no entry; R∩{1,2}; R∩{3..6} | SY(ACHRES61) | source uses octal 011..015 = decimal9..13; R={14} expected ENTRES51, Python ENTRES71; R={15} expected RSRDEF51, Python INFARE51 | NOT_PROVEN |
| RE-ANCHOR-INFO | no entry; R∩{1,2}; no {3..6}; R∩{9..13} | SY(ACHRES71) | source uses octal 011..015 = decimal9..13; R={14} expected ENTRES51, Python ENTRES71; R={15} expected RSRDEF51, Python INFARE51 | NOT_PROVEN |
| RE-ANCHOR-ONLY | no entry; R∩{1,2}; no {3..6,9..13} | SY(ACHRES51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RE-FISH-INFO | no entry/anchor; R∩{3..6}; R∩{9..13} | SY(FSHRES71) | source uses octal 011..015 = decimal9..13; R={14} expected ENTRES51, Python ENTRES71; R={15} expected RSRDEF51, Python INFARE51 | NOT_PROVEN |
| RE-FISH-ONLY | no entry/anchor; R∩{3..6}; no {9..13} | SY(FSHRES51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RE-INFO | no {1..8,14}; R∩{9..13} | SY(INFARE51) | source uses octal 011..015 = decimal9..13; R={14} expected ENTRES51, Python ENTRES71; R={15} expected RSRDEF51, Python INFARE51 | NOT_PROVEN |
| RE-DEFAULT | nonempty R without prior match | SY(RSRDEF51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
### RESARE02
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| RA-ENTRY-MIX-PLAIN | R contains entry; R intersects1..6 or CATREA A; symbolized_boundaries=False | OP(6---) → LS(DASH,2,CHMGD) → SY(ENTRES61) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ENTRY-MIX-SYMB | R contains entry; R intersects1..6 or CATREA A; symbolized_boundaries=True | OP(6---) → LC(RESARE51) → SY(ENTRES61) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ENTRY-INFO-PLAIN | entry; previous false; R intersects9..13 or CATREA B; symbolized_boundaries=False | OP(6---) → LS(DASH,2,CHMGD) → SY(ENTRES71) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ENTRY-INFO-SYMB | entry; previous false; R intersects9..13 or CATREA B; symbolized_boundaries=True | OP(6---) → LC(RESARE51) → SY(ENTRES71) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ENTRY-ONLY-PLAIN | entry; previous false; symbolized_boundaries=False | OP(6---) → LS(DASH,2,CHMGD) → SY(ENTRES51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ENTRY-ONLY-SYMB | entry; previous false; symbolized_boundaries=True | OP(6---) → LC(RESARE51) → SY(ENTRES51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ANCHOR-MIX-PLAIN | no entry; anchor; fishing or CATREA A; symbolized_boundaries=False | OP(6---) → LS(DASH,2,CHMGD) → SY(ACHRES61) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ANCHOR-MIX-SYMB | no entry; anchor; fishing or CATREA A; symbolized_boundaries=True | OP(6---) → LC(RESARE51) → SY(ACHRES61) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ANCHOR-INFO-PLAIN | no entry; anchor; previous false; R info or CATREA B; symbolized_boundaries=False | OP(6---) → LS(DASH,2,CHMGD) → SY(ACHRES71) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ANCHOR-INFO-SYMB | no entry; anchor; previous false; R info or CATREA B; symbolized_boundaries=True | OP(6---) → LC(RESARE51) → SY(ACHRES71) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ANCHOR-ONLY-PLAIN | no entry; anchor; previous false; symbolized_boundaries=False | OP(6---) → LS(DASH,2,CHMGD) → SY(RESTRN51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-ANCHOR-ONLY-SYMB | no entry; anchor; previous false; symbolized_boundaries=True | OP(6---) → LC(RESARE51) → SY(RESTRN51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-FISH-A-PLAIN | no entry/anchor; fishing; CATREA A; symbolized_boundaries=False | OP(6---) → LS(DASH,2,CHMGD) → SY(FSHRES51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-FISH-A-SYMB | no entry/anchor; fishing; CATREA A; symbolized_boundaries=True | OP(6---) → LC(FSHRES51) → SY(FSHRES51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-FISH-INFO-PLAIN | no entry/anchor; fishing; no A; R info or CATREA B; symbolized_boundaries=False | OP(6---) → LS(DASH,2,CHMGD) → SY(FSHRES71) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-FISH-INFO-SYMB | no entry/anchor; fishing; no A; R info or CATREA B; symbolized_boundaries=True | OP(6---) → LC(FSHRES51) → SY(FSHRES71) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-FISH-ONLY-PLAIN | no entry/anchor; fishing; previous false; symbolized_boundaries=False | OP(6---) → LS(DASH,2,CHMGD) → SY(FSHRES51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-FISH-ONLY-SYMB | no entry/anchor; fishing; previous false; symbolized_boundaries=True | OP(6---) → LC(FSHRES51) → SY(FSHRES51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-R-INFO-PLAIN | R present; no entry/anchor/fishing; R info; symbolized_boundaries=False | LS(DASH,2,CHMGD) → SY(INFARE51) | A={1,8,9,12,14,19,21,25}; B={4,5,6,7,10,18,20,22,23,24}; info={9,10,11,12,13}. Static boundary choice frozen; no runtime reselection. | NOT_PROVEN |
| RA-R-INFO-SYMB | R present; no entry/anchor/fishing; R info; symbolized_boundaries=True | LC(CTYARE51) → SY(INFARE51) | A={1,8,9,12,14,19,21,25}; B={4,5,6,7,10,18,20,22,23,24}; info={9,10,11,12,13}. Static boundary choice frozen; no runtime reselection. | NOT_PROVEN |
| RA-R-DEFAULT-PLAIN | R present (even empty); no prior match; symbolized_boundaries=False | LS(DASH,2,CHMGD) → SY(RSRDEF51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-R-DEFAULT-SYMB | R present (even empty); no prior match; symbolized_boundaries=True | LC(CTYARE51) → SY(RSRDEF51) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| RA-NOR-AB-PLAIN | R absent; CATREA A and B; symbolized_boundaries=False | LS(DASH,2,CHMGD) → SY(CTYARE71) | A={1,8,9,12,14,19,21,25}; B={4,5,6,7,10,18,20,22,23,24}; info={9,10,11,12,13}. Static boundary choice frozen; no runtime reselection. | NOT_PROVEN |
| RA-NOR-AB-SYMB | R absent; CATREA A and B; symbolized_boundaries=True | LC(CTYARE51) → SY(CTYARE71) | A={1,8,9,12,14,19,21,25}; B={4,5,6,7,10,18,20,22,23,24}; info={9,10,11,12,13}. Static boundary choice frozen; no runtime reselection. | NOT_PROVEN |
| RA-NOR-A-PLAIN | R absent; A only; symbolized_boundaries=False | LS(DASH,2,CHMGD) → SY(CTYARE51) | A={1,8,9,12,14,19,21,25}; B={4,5,6,7,10,18,20,22,23,24}; info={9,10,11,12,13}. Static boundary choice frozen; no runtime reselection. | NOT_PROVEN |
| RA-NOR-A-SYMB | R absent; A only; symbolized_boundaries=True | LC(CTYARE51) → SY(CTYARE51) | A={1,8,9,12,14,19,21,25}; B={4,5,6,7,10,18,20,22,23,24}; info={9,10,11,12,13}. Static boundary choice frozen; no runtime reselection. | NOT_PROVEN |
| RA-NOR-B-PLAIN | R absent; B only; symbolized_boundaries=False | LS(DASH,2,CHMGD) → SY(INFARE51) | A={1,8,9,12,14,19,21,25}; B={4,5,6,7,10,18,20,22,23,24}; info={9,10,11,12,13}. Static boundary choice frozen; no runtime reselection. | NOT_PROVEN |
| RA-NOR-B-SYMB | R absent; B only; symbolized_boundaries=True | LC(CTYARE51) → SY(INFARE51) | A={1,8,9,12,14,19,21,25}; B={4,5,6,7,10,18,20,22,23,24}; info={9,10,11,12,13}. Static boundary choice frozen; no runtime reselection. | NOT_PROVEN |
| RA-NOR-NONE-PLAIN | R absent; neither A nor B; symbolized_boundaries=False | LS(DASH,2,CHMGD) → SY(RSRDEF51) | A={1,8,9,12,14,19,21,25}; B={4,5,6,7,10,18,20,22,23,24}; info={9,10,11,12,13}. Static boundary choice frozen; no runtime reselection. | NOT_PROVEN |
| RA-NOR-NONE-SYMB | R absent; neither A nor B; symbolized_boundaries=True | LC(CTYARE51) → SY(RSRDEF51) | A={1,8,9,12,14,19,21,25}; B={4,5,6,7,10,18,20,22,23,24}; info={9,10,11,12,13}. Static boundary choice frozen; no runtime reselection. | NOT_PROVEN |
### LIGHTS05/LIGHTS06
| branch_id | condition | expected | current / evidence | v3 status |
|---|---|---|---|---|
| LI-DISPATCH | CS(LIGHTS05) | LIGHTS06(param) immediately | legacy LIGHTS05 body after return unreachable; LIGHTS06 not registered as separate CS entry | NOT_PROVEN |
| LI-FLOOD | CATLIT contains8 or11 | SY(LIGHTS82) → LI-TEXT selected by _LITDSN01 + prior lat/lon/description | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-STRIP | no8/11; CATLIT contains9 | SY(LIGHTS81) → LI-TEXT selected by _LITDSN01 + prior lat/lon/description | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-DIRECTION | other; sector value missing/-9; CATLIT1 or14 | SY(QUESMRK1) → LI-TEXT selected by _LITDSN01 + prior lat/lon/description | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-FLARE | other; no sector; no CATLIT1/14; VALNMR(default9)<10 | SY(flareColor,135) → LI-TEXT selected by _LITDSN01 + prior lat/lon/description | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-ROUND | other; no sector; no CATLIT1/14; VALNMR>=10 | CA(OUTLW,4,roundColor,2,0,360,radius+colorDelta,0) → LI-TEXT selected by _LITDSN01 + prior lat/lon/description | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-ZERO-SWEEP | sector values not -9; sweep<1 or =360 | CA(OUTLW,4,roundColor,2,0,360,radius+colorDelta,0) → LI-TEXT selected by _LITDSN01 + prior lat/lon/description | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-SECTOR | sector; sweep>=1 !=360; not obscured | CA(OUTLW,4,sectorColor,2,start,end,sectorRadius,25) → LI-TEXT selected by _LITDSN01 + prior lat/lon/description | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-OBSCURED | sector; sweep>=1 !=360; LITVIS3/7/8 | CA(CHBLK,4,CHBRN,1,start,end,sectorRadius,25) → LI-TEXT selected by _LITDSN01 + prior lat/lon/description | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-SEL-RED | single3 or pair1+3 | LI terminal with flare LIGHTS11; round LITRD delta1 → LI-TEXT | CA equivalent angle modulo alone does not prove renderer scale/layout; exact source parameters remain recorded | NOT_PROVEN |
| LI-SEL-GREEN | single4 or pair1+4 | LI terminal with flare LIGHTS12; round LITGN delta0 → LI-TEXT | CA equivalent angle modulo alone does not prove renderer scale/layout; exact source parameters remain recorded | NOT_PROVEN |
| LI-SEL-YELLOW | single1/6/9 (octal011) | LI terminal with flare LIGHTS13; round LITYW delta2 → LI-TEXT | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-SEL-MAGENTA | single12 / absent color default12 | LI terminal with flare LITDEF11; round CHMGD delta3 → LI-TEXT | CA equivalent angle modulo alone does not prove renderer scale/layout; exact source parameters remain recorded | NOT_PROVEN |
| LI-SEL-OTHER | other single/multi color | LI terminal with flare LITDEF11; round CHMGD delta5 → LI-TEXT | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-SECTOR-COLOR | single3→red;4→green;1/6/11→yellow; pair1+3/red,1+4/green;else magenta | LI terminal with sectorColor from this table → LI-TEXT | CA equivalent angle modulo alone does not prove renderer scale/layout; exact source parameters remain recorded | NOT_PROVEN |
| LI-ROUND-RADIUS | V>0: <7→3;<15→10;<30→15;else20; V<=0→3 | LI terminal with round radius before colorDelta → LI-TEXT | CA equivalent angle modulo alone does not prove renderer scale/layout; exact source parameters remain recorded | NOT_PROVEN |
| LI-SECTOR-RADIUS | V>0: <15→10;<30→15;else20; V<=0→20 | LI terminal with sector radius → LI-TEXT | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-ANGLE | sectr2<=sectr1→+360; each >180 subtract180 else add180 | LI terminal with start,end after seaward conversion → LI-TEXT | CA equivalent angle modulo alone does not prove renderer scale/layout; exact source parameters remain recorded | NOT_PROVEN |
| LI-SENTINEL | either SECTR value=-9 | LI terminal with non-sector branch → LI-TEXT | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-TEXT-FIRST | different lastLat/lastLon; description nonempty | LI mode prefix → TX(desc,3,2,3,'15110',2,0,CHBLK,23) | flare_at_45 false in reachable LIGHTS06; text visibility handled later by RenderT_All | NOT_PROVEN |
| LI-TEXT-DUPLICATE | same previous lat/lon; same description | LI mode prefix | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-TEXT-CHANGED | same previous lat/lon; different description | LI mode prefix → TX(desc,3,2,3,'15110',2,1,CHBLK,23) | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-TEXT-EMPTY-FIRST | different lat/lon; empty description | LI mode prefix | flare_at_45 false in reachable LIGHTS06; text visibility handled later by RenderT_All | NOT_PROVEN |
| LI-DESC-CHAR | LITCHR1..29 or absent/unknown | LI mode prefix → TX using description rule: description abbreviation per _LITDSN01 switch; 21/23 vert;22/24 horz | full Object→Lookup→consumer equivalence and rendering parameters not proven | NOT_PROVEN |
| LI-DESC-TWO-GROUP | LITCHR13/14/15/16/25/26/27/29 | LI mode prefix → TX using description rule: insert (?) even without SIGGRP; replace ? with first character of first group; append second if !=1 | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-DESC-SINGLE-GROUP | other LITCHR; SIGGRP present !=(1) | LI mode prefix → TX using description rule: append literal SIGGRP | full Object→Lookup→consumer equivalence and rendering parameters not proven | NOT_PROVEN |
| LI-DESC-SECTOR-PRESENCE | SECTR1 attribute exists (SECTR2 irrelevant) | LI mode prefix → TX using description rule: omit COLOUR and VALNMR text | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-DESC-PERIOD | SIGPER present | LI mode prefix → TX using description rule: 1 decimal iff abs(round-value)>.01 else integer; append s | full Object→Lookup→consumer equivalence and rendering parameters not proven | NOT_PROVEN |
| LI-DESC-HEIGHT-M | HEIGHT present; height unit metres | LI mode prefix → TX using description rule: rounded HEIGHT + m | full Object→Lookup→consumer equivalence and rendering parameters not proven | NOT_PROVEN |
| LI-DESC-HEIGHT-FT | HEIGHT present; height unit feet | LI mode prefix → TX using description rule: rounded HEIGHT/0.3048 + ft | Current ordered Rule IR and runtime executor satisfy this v2 failing branch; phase-family witness PASS. | PASS |
| LI-DESC-RANGE | VALNMR present and SECTR1 absent | LI mode prefix → TX using description rule: rounded range + Nm | full Object→Lookup→consumer equivalence and rendering parameters not proven | NOT_PROVEN |
## 6. 剩余 FAIL
`DC-DEC-DEP-LOW`：OpenCPN DEPCNT 的 DEPARE interval 在判定前等价采用规范化后的 depth range；当前 `resolve_depcnt02_instruction` 对 `DRVAL2<=DRVAL1` 未共享 DEPARE01 的 `+0.01` 规范化，因此把 witness 错判为 safe contour。证据包：`build/audits/cm95_s52_remaining_26_residual_fail_evidence_v1.json`。

107
docs/报告/CM95_S52_剩余26个根因统一修复报告_v1.md Normal file
View File

@@ -0,0 +1,107 @@
# CM95 S-52 剩余 26 个根因统一修复报告 v1
日期：2026-09-21。
## 1. 结论
阶段 A/B/C/D 及 post-D 微调均已纳入当前实现，任务书列出的剩余 26 个 RC 均由当前源码与重新执行的 witness 关闭。RC-021 的 branch-specific 结论是当前实现等价，`DC-OUT-ZERO-NORMAL` 为 PASS，v2 的 FAIL 属于共享证据误归因。
完整 206 条重新审计得到 **PASS 120 / FAIL 1 / NOT_PROVEN 85**。审计同时暴露一条不属于 RC-021 的相邻残留机制 `RC-039 / DC-DEC-DEP-LOW`，因此 Target Portrayal 保持 FAIL，本轮没有扩大为新一轮代码修复。
## 2. Production / release
- plan：`build/production/cm95_s52_kyushu_production_plan_v5_ordered_rule_ir.json`
- plan id：`d6627c77efec38d1fcd9f398870cd19519e9e948ba4515e7357829aa10087f2b`
- release：`cm95-d1-62a85bd40d3a-d6627c77efec`
- jobs：5065/5065 PASS
- PBF：5064
- features：476120
- 本轮 build/release generation：未执行；复用外部 shell 已完成产物并只读校验 summary。
- PBF contract：已由阶段 A 引入 ordered Rule IR，v5 plan 使用 `cm95pbf-builder/0.4.13-s52-ordered-rule-ir`。
- 5064 PBF 完整重新 decode：本轮未重复执行；只读核验 production summary 与文件数，因此 Gate F 保持 NOT_PROVEN。
## 3. 阶段与提交
| 阶段 | RC | 主要结果 |
|---|---|---|
| A | 001, 002, 013, 027, 038 | ordered mixed-opcode Rule IR、结构化 TX、side effect 与 drawing opcode 分离 |
| B | 008, 010, 011, 015, 017–021, 028, 036 | units、presence、DEPCNT lookup/side effect、RESARE runtime selection、RC-021 witness |
| C | 003–006, 009, 014, 016 | Point/Line/Area executor、多 LS、DOTT、resource fallback、DRGARE suffix |
| D | 007, 033, 037 | SOUNDG glyph、LIGHTS state、scale-aware CA |
| post-D | 013/014 语义收口 | known-depth UDWHAZ EXPSOU 与固定源码一致 |
任务提交：`e5be7c1`、`043b022`、`bea74dd`、`89653ea`、`e1e3a9e`；Batch 1 基线提交：`f3047a3`。
- 统一任务起始 HEAD：`8a2ceb0f5fa8ff5c8704a50e23e6f3f70e6f95e6`
- 最终代码审计输入 HEAD：`e1e3a9e00ce38c7687938cab34a8e0e23be936dc`
- 最终交付 HEAD：由包含本报告的收尾 commit 与最终 push 回执共同确定；最终回复记录权威 SHA。
### 3.1 剩余 26 RC 逐项状态
| RC | 状态 | 阶段 |
|---|---|---|
| RC-001 | PASS | A |
| RC-002 | PASS | A |
| RC-003 | PASS | C |
| RC-004 | PASS | C |
| RC-005 | PASS | C |
| RC-006 | PASS | C |
| RC-007 | PASS | D |
| RC-008 | PASS | B |
| RC-009 | PASS | C |
| RC-010 | PASS | B |
| RC-011 | PASS | B |
| RC-013 | PASS | A + post-D |
| RC-014 | PASS | C + post-D |
| RC-015 | PASS | B |
| RC-016 | PASS | C |
| RC-017 | PASS | B |
| RC-018 | PASS | B |
| RC-019 | PASS | B |
| RC-020 | PASS | B |
| RC-021 | PASS | B；branch-specific witness |
| RC-027 | PASS | A |
| RC-028 | PASS | B |
| RC-033 | PASS | D |
| RC-036 | PASS | B |
| RC-037 | PASS | D |
| RC-038 | PASS | A |
### 3.2 Witness
| Witness | 状态 | SHA-256 |
|---|---|---|
| phase A | PASS | `a15a7255729110a77ab809788f10277412e7181624cadf2bc85e4815b19ab3f2` |
| phase B | PASS | `1dcd8ae7cb2974b011573d2c3008fa895597e306d866e90851d1cdebf8f1c7ba` |
| phase C | PASS | `8860118ebb1919f641e567332b97a4be39f7040d7413689e52d3e7b617e54651` |
| phase D | PASS | `a104b2edf9a6897ca73ad60936fa98cb61526d8cd2338bed3276f4ba7988babf` |
| current branch probes | PASS（执行完成；包含 1 个确认 residual） | `32b08a41221ec24ab5b70b367781bcb95fcebe763bc1e9a82c95fb189c7d43a3` |
## 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 | FAIL | All 206 rows were re-adjudicated; DC-DEC-DEP-LOW is now a branch-specific confirmed mismatch. |
| 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 | FAIL | The DEPCNT DEPARE interval path does not normalize DRVAL2<=DRVAL1 before safe-contour selection. |
| 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. 残留项
唯一 branch FAIL：`DC-DEC-DEP-LOW`。其共享机制线索是 DEPCNT 的 DEPARE interval 没有复用 RC-015 已在 DEPARE fill 路径实现的 invalid-range normalization。紧凑证据包：`build/audits/cm95_s52_remaining_26_residual_fail_evidence_v1.json`。
流程级 Gate A 仍有 `$AREAS/$SCODE` 与 lookup parser 语义差异；它们不是本轮新修代码范围。Gate F/G/I 继续保守为 NOT_PROVEN。
## 6. 交付物
- `docs/报告/CM95_S52_OpenCPN渲染流程对照审计报告_v3.md`
- `build/audits/cm95_s52_opencpn_code_first_equivalence_v3.json`
- `build/audits/cm95_s52_remaining_26_root_cause_fix_v1.json`
- `build/audits/cm95_s52_remaining_26_residual_fail_evidence_v1.json`
本任务代码修改范围：`src/cm95pbf/{csp,presentation,s52,mapping}.py`、`tools/cm95_s52_style_compiler.py`、`web/{kyushu_compare.html,kyushu_compare_server.py,s52_runtime_executor.js}`、runtime capability registry。收尾新增文件为本节四项产物及 `tools/cm95_s52_code_first_reaudit_v3.py`。既有 importer/Linux/README 等无关 dirty/untracked 文件均按 SHA-256 保护，未纳入提交。