From 2f0d77a3d0b052a448563532e8d5dd1fc5543479 Mon Sep 17 00:00:00 2001 From: JianFeeeee Date: Fri, 25 Sep 2026 06:10:38 +0800 Subject: [PATCH] =?UTF-8?q?fix(deploy):=20check-relay-counts=20=E4=B8=A4?= =?UTF-8?q?=E6=9D=A1=E6=96=AD=E8=A8=80=E6=98=AF**=E5=81=87=E7=BA=A2**=20?= =?UTF-8?q?=E2=80=94=E2=80=94=20=E6=8A=8A"=E6=81=B0=E5=A5=BD=E5=A6=82?= =?UTF-8?q?=E6=AD=A4"=E5=BD=93=E6=88=90=E4=BA=86=E4=B8=8D=E5=8F=98?= =?UTF-8?q?=E9=87=8F?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 新脚本的立意（把反复对账的查询固定成命令、断言只写不变量、瞬时量只打印）完全正确， 但它自己破了其中两条规则。两条都实测复现，且都把**正确动作**判成失败。 ## 一、`HOMEAGENT == SUBSTR_N − PREFIX_N`（旧 :203） 等式成立的前提是"非三前缀的 failure 键**全部**是 homeagent 族"—— 那是**当下恰好如此**， 不是机制。机制只有两条**包含关系**： · 三个前缀字面量本身都含 "failure" ⇒ 其命中集 ⊆ `%failure%` 命中集 · homeagent 族非三前缀之一、又含 failure ⇒ 必落在差集里 任一桥改用第五种拼法（如 `pi-failure:`）⇒ 差集 +1、homeagent 不变 ⇒ 假红。 实测：插入一行 `pi-failure:` 后 子串=99 三前缀=82 homeagent=16，差=17 ⇒ 旧断言红。 ## 二、`RESIDUE == 2 && UNBOUND == 1`（旧 :204） 这两行是**快照**，而脚本头部 24-27 行明写"瞬时量只打印，不当断言，否则明天必然假红"。 未绑定那行是"claim 后早退没退键"的化石；**清掉它是正确动作**， 旧断言却让清理后变红。实测：清掉该行后 残留=1/未绑定=0 ⇒ 旧断言红。 ⇒ 改为只打印（已在"当下读数"里），另用与清理无关的关系接住： `未绑定 ⊆ 占位`（未绑定必是占位，两者口径一致）。 ## 验证 真库：新旧都绿 /tmp 副本（清化石 + 加第五族）：旧 rc=1（两条 FAIL）、新 rc=0 ⇒ 红→绿可复现，且红的两条正是上面两条 --- deploy/check-relay-counts.sh | 22 +++++++++++++++++----- 1 file changed, 17 insertions(+), 5 deletions(-) diff --git a/deploy/check-relay-counts.sh b/deploy/check-relay-counts.sh index 8aa115f..63d103c 100755 --- a/deploy/check-relay-counts.sh +++ b/deploy/check-relay-counts.sh @@ -198,11 +198,23 @@ chk_true "**空真**: kind<>'failure' 的计数 == 已绑定（对全表恒真 "$([ "$NAIVE" -eq "$BOUND" ] && echo 1 || echo 0)" chk_true "真判据 **严格小于** 空真判据（否则判据没起作用）" \ "$([ "$REAL" -lt "$NAIVE" ] && echo 1 || echo 0)" -chk_true "子串 %failure% **多于** 三前缀（差即 homeagent 族 = 命名巧合）" \ - "$([ "$SUBSTR_N" -gt "$PREFIX_N" ] && echo 1 || echo 0)" -chk_eq "homeagent 族 == 子串 − 三前缀" "$HOMEAGENT" "$((SUBSTR_N - PREFIX_N))" -chk_true "残留集合 = 1 未绑定 + 1 已绑定（**不是同一行**）" \ - "$([ "$RESIDUE" -eq 2 ] && [ "$RESIDUE_UNBOUND" -eq 1 ] && echo 1 || echo 0)" +# ★ 量的是**包含关系**，不是"恰好只有四族"： +# 三个前缀字面量本身都含 "failure" ⇒ 它们匹配的键必然也被 `%failure%` 匹配（子集）。 +# 而 homeagent 族既不以那三者为前缀、又含 failure ⇒ 必落在**差集**里（子集）。 +# 两条都由机制决定。先前写成 `HOMEAGENT == SUBSTR_N - PREFIX_N`，是把 +# "当下只存在这四个族"当成了不变量 —— 任一桥改用第五种拼法（如 `pi-failure:`） +# 会让差集 +1 而 homeagent 不变 ⇒ **假红**（新增命名是正常演进，不是故障）。已实测复现。 +chk_true "三前缀 ⊆ 子串（三前缀字面量都含 failure）" \ + "$([ "$PREFIX_N" -le "$SUBSTR_N" ] && echo 1 || echo 0)" +chk_true "homeagent 族 ⊆ 差集（它非三前缀之一、且含 failure）" \ + "$([ "$HOMEAGENT" -le "$((SUBSTR_N - PREFIX_N))" ] && echo 1 || echo 0)" +# ★ 那两行残留是**快照，不是不变量** —— 与文件头 24-27 行同一条规则。 +# 未绑定那行是"claim 后早退没退键"留下的化石；**清掉它是正确动作**， +# 而 `RESIDUE == 2 && UNBOUND == 1` 会把那个正确动作判成失败 +# （实测：清后 1/0 ⇒ 假红）。⇒ 改为只打印（见上面"当下读数"）， +# 另用一条**与清理无关**的关系接住：未绑定必是占位，口径一致。 +chk_true "残留中未绑定的 ⊆ 占位行（未绑定必是占位，两者口径一致）" \ + "$([ "$RESIDUE_UNBOUND" -le "$PLACE" ] && echo 1 || echo 0)" chk_true "两口径抑制数**不同**（沿链范围不同 ⇒ 量的是不同集合）" \ "$([ "$S_FULL_S" -ne "$S_FAIL_S" ] && echo 1 || echo 0)" chk_true "完整链口径的抑制数 **大于** failure 链口径" \