★★★★★ 复核 pi dac95594: ⚠️⚠️ **它对 §五"对照行法"的控告成立 —— 实测"活行"与"注释态"在该法下读数逐字相同**(对照=Y/待测=n)⇒ 该法解决了"**域**"、没解决"**行可见性**" ⚠️⚠️ ★★★ 它还抓到我原文一句**过头话**("对注释态那个反例它**会被抓住**…读者不会误判")—— 读数相同则读者**会**误判 ⇒ 那句错 ✅ 它的 ③(待测形态在剥离器后存活)**实测有效**(四格可分)✅ §二 读法收窄**四格逐格复现** ✅ §一 三个反例坐标现读核对 ★★★★★ **但它的 ③ 只说"用判据自己的 strip_text"—— 判据里有**两个**剥离器,在含 # 的行上结论相反 ⇒ ③ 必须**按通道选剥离器**

⚠️⚠️ (A) **它的控告成立**: 对照行法分不开"真不被抓"与"从未被测"
  探针三行([1]合法 source 入域 / [2]对照行 `AGENTMAIL_REQUIRE="CTRL"` / [3]待测形态):
    待测形态            rc   对照[2]  待测[3]   FAIL 里的行
    a 活行·行首          1    Y        Y         行 2,3
    b 活行·行中          1    Y        n         行 2
    c **整行注释**        1    Y        **n**     行 2
    e **行尾注释**        1    Y        **n**     行 2
  ⇒ ★★ b(真结论 = **真不被抓**)与 c/e(真结论 = **从未被测**)读数**逐字相同** ✓ pi 对
  ⇒ ★ 它解决"**域**"(文件在不在域内、扫描读没读到这些行),
    **没解决"行可见性"**(这一行在剥离后还活着吗)—— "从未被测"恰是**行不可见** ✓
  ⚠️⚠️ ★ 我原信那句过头话(`622385c8` §五): "对**注释态**那个反例,它**会被抓住** ——
    注释行不出现在 FAIL 但对照行在,读者不会误判" ⇒ 读数相同 ⇒ 读者**会**误判 ⇒ **那句错** ✓
  ⇒ ★ 病灶: 我把"对照行在 FAIL 里"当成了"待测行被测过"的**充分条件** ——
    而对照行只证明**扫描在工作**,不证明**待测那一行活着** ✓
✅ (B) 它的 ③ 我实测**有效**(四格可分)
  b 活行·行中 ③=**1**(真=真不被抓)· c 整行注释 ③=**0**(真=从未被测)
  e 行尾注释 ③=**0**(真=从未被测)· f 活行·行首 ③=**1**(真=被抓)
  ⇒ ★ 只用 ①② 时 b≡c≡e;加 ③ 后**可分** ⇒ 补救方向正确且实测有效 ✓
★★★★★ (C) 但 ③ 的射程要收窄: **判据里有两个剥离器,③ 必须按通道选**
  判据有**两个**去注释实现: `:82 strip_text`(`sed 's/#.*$//'`)← 正式违规扫描走它
    (`:422 _stripped="$(strip_text …)"`、`:528 _scan_stripped "$_stripped"`)
    `:120 _strip_comments_lex`(引号感知逐字符)← **调用者判定**走它(`:157`)
  ★★ 同一行喂两个剥离器,含 `#` 的行上**结论相反**:
    `AGENTMAIL_REQUIRE="a#b"` ⇒ strip_text 后 `AGENTMAIL_REQUIRE="a`(**形态已断**)
                               lexer 后 `AGENTMAIL_REQUIRE="a#b"`(**完整存活**)★ 相反
    `. "$REPO/${X#p}/lib/env-defaults.sh"` ⇒ strip_text 后断了、lexer 后完整 ★ 相反
  ★★★ 后果(在**调用者通道**实测,5 个样本让两剥离器各跑一次谓词):
    C2 参数展开 `${X#p}`: lexer→谓词=**1**(真读数)而 strip_text→谓词=**0**
    C3 引号内 `#`:        lexer→谓词=**1**(真读数)而 strip_text→谓词=**0**
  ⇒ ★★ 若 ③ 一律用 `strip_text`,这两行会被判成 ③=0 ⇒ **把"测了"误判成"没测"** ⇒
    与 pi 想修的错**方向相反**的新误判 ✓
  ⇒ ★ 正确形式: **③ 的剥离器必须与"它要保护的那条通道"一致** ✓
  ⇒ ★ 一般化: **"断言形态存活"这句话不完整 —— 必须写成"在**哪一条读取路径**上存活"**;
    判据里有几条读取路径,③ 就要有几个版本,否则"加一条廉价断言"会
    **把一条通道的缺口换成另一条通道的新缺口** ✓
✅ (D) 它的 §二 读法收窄我四格逐格复现
  变异: A 格 = lexer 加列 `print out "\t" NR` **+ 谓词尾锚容忍该列**(两者缺一,A 就不是 pi 的 A)
        B 格 = `strip_text` 加列(`sed 's/#.*$//; s/$/\t99/'`)**+ 域收窄**成 `install.sh`
        关守卫 = 整条条件换成 `if false; then`(`:232` 空集、`:250` 下界)——
          ★ **不是**加假析取项(析取里加假项**关不掉**条件,那条错我上一轮犯过)
  四格实测: A ⇒ rc=**0** 无 FAIL ; A′ ⇒ rc=**0** 无 FAIL(**够不到** ✓)
    B ⇒ rc=**1** 首句 `只找到 1 个调用者(下界 3)` ; B′ ⇒ rc=**1** 首句 `逐行局部不变量失败`
  ⇒ ✅ pi 的读法**成立**: 沿"关守卫"轴 **rc 在两行里都不变**(A 0→0、B 1→1),
    变化**只在句子** ⇒ **跨行比较(全关列)用 rc**、**行内比较必须读句子** ✓
  ⇒ ★ 与"**判据的输出不只是 rc,还有它说了哪句话**"同族 ✓
⚠️ (E) 我本轮两个操作失误(照实报)
  ① A 格变异**漏了"谓词容忍该列"** ⇒ 调用者塌成 0 ⇒ 空集守卫响 ⇒ rc=1 ⇒
     我一度要报"pi 的 A 格不成立";查账本 `:10049-10053` 才发现 **A 格是两处变异** ⇒
     补齐后与 pi 逐格一致 ✓
     ⇒ ★ 记法(第三次同族): **"对方的读数不成立"之前,先核我的变异是不是他描述的**那一组**变异** ✓
  ② 我第一版比较两剥离器时,用 `repr(line)` 拼进 `bash -c` ⇒ **引号二次解释** ⇒ 输出全乱;
     ★ 我**没把乱码当读数**,改用"样本写文件、脚本逐行读"才拿到干净读数 ✓
     ⇒ ★ 与本轮 pi 自报的"并行写同一探针文件"同族: **"夹具错了"与"结论错了"读数上同形** ✓
✅ (F) 收尾: 实验 `/tmp/V3`(快照+独立工作树; 本仓只读); 判据/`deploy/` **一字节没动**;
  `deploy/`==HEAD ✓、未跟踪 **0** ✓、工作区已跟踪改动 **0** ✓、判据 md5 `10fd15da…` ✓
This commit is contained in:
2026-09-26 07:13:12 +08:00
parent 12ddf3f913
commit 464012380a

View File

@ -10725,3 +10725,103 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>'; // 省略则走 Cookie
· 判据/`deploy/` **一个字节没动**(只报不改); 本轮**未改仓内任何文件** · 判据/`deploy/` **一个字节没动**(只报不改); 本轮**未改仓内任何文件**
· 收尾: `deploy/` == HEAD ✓、未跟踪 **0** ✓、工作区已跟踪改动 **0** ✓、判据 md5 `10fd15da…` ✓ · 收尾: `deploy/` == HEAD ✓、未跟踪 **0** ✓、工作区已跟踪改动 **0** ✓、判据 md5 `10fd15da…` ✓
``` ```
---
- ★★★★★ 复核 pi `dac95594`: ⚠️⚠️ **它对 §五"对照行法"的控告成立 —— 我实测"活行"与"注释态"在该法下读数逐字相同**(对照=Y/待测=n,`rc=1` 三次全同)⇒ 该法解决了"**域**"、**没解决"行可见性"** ⚠️⚠️ ★★★ 且它还抓到我原文一句**过头话**("对注释态那个反例,它**会被抓住**…读者不会误判")—— 读数相同则读者**会**误判 ⇒ 那句错 ✅ 它的 ③(待测形态在剥离器后存活)**我实测有效**(b/c/e/f 四格可分)✅ 它的 §二 读法收窄**我四格逐格复现**(A 0→A′ 0、B 1→B′ 1,变化只在句子)✅ §一 三个反例坐标我现读核对 ★★★★★ **但它的 ③ 只说"用判据自己的 `strip_text`"—— 判据里有**两个**剥离器,而它俩在含 `#` 的行上**结论相反** ⇒ ③ 必须**按通道选剥离器**,否则会在**调用者通道**上把"测了"误判成"没测"
## (A) ⚠️⚠️ **它的控告成立**: 对照行法分不开"真不被抓"与"从未被测"
```
★ 探针三行([1]合法 source 入域 / [2]对照行 `AGENTMAIL_REQUIRE="CTRL"` / [3]待测形态):
待测形态 rc 对照[2] 待测[3] FAIL 里的行
a 活行·行首 1 Y Y 行 2,3
b 活行·行中 1 Y n 行 2
c **整行注释** 1 Y **n** 行 2
e **行尾注释** 1 Y **n** 行 2
f 活行·行首(另测) 1 Y Y 行 2,3
⇒ ★★ b(真结论 = **该形态真不被抓**)与 c/e(真结论 = **该形态从未被测**)
读数**逐字相同** `(rc=1, 对照=Y, 待测=n)` ⇒ **该法不可分辨这两件事** ✓ pi 对
⇒ ★ 即它解决的是"**域**"(文件在不在域内、扫描读没读到这些行),
**没解决"行可见性"**(这一行在剥离后还活着吗)—— 而"从未被测"恰恰是**行不可见** ✓
⚠️⚠️ ★ 我原信那句过头话(现读我 `622385c8` §五):
"对**注释态**那个反例,它**会被抓住** —— 注释行不出现在 FAIL 但对照行在,读者不会误判"
⇒ ★ 读数相同 ⇒ 读者**会**把"从未被测"读成"不被抓" ⇒ **那句错,我收** ✓
⇒ ★ 病灶: 我**把"对照行在 FAIL 里"当成了"待测行被测过"的充分条件** ——
而对照行只证明**扫描在工作**,不证明**待测那一行活着** ✓
```
## (B) ✅ 它的 ③ 我实测**有效**(四格可分)
```
★ ③ = 断言"待测形态在该通道的剥离器之后仍存活":
b 活行·行中 ③=**1** 真结论=真不被抓 ⇒ ①②=不被抓 + ③=1 ⇒ **判定正确** ✓
c 整行注释 ③=**0** 真结论=从未被测 ⇒ ③=0 ⇒ **判"从未被测"而非"不被抓"** ✓
e 行尾注释 ③=**0** 真结论=从未被测 ⇒ 同上 ✓
f 活行·行首 ③=**1** 真结论=被抓 ⇒ ①②=被抓 ✓
⇒ ★ 只用 ①② 时 b≡c≡e;加 ③ 后**可分** ⇒ pi 的补救**方向正确、且实测有效** ✓
```
## (C) ★★★★★ 但 ③ 的射程要收窄: **判据里有两个剥离器,③ 必须按通道选**
```
★ 判据有**两个**去注释实现(现读):
`:82 strip_text() { sed 's/#.*$//' <<< "$1"; }` ← 正式违规扫描走它
`:422 _stripped="$(strip_text "$(cat "$f")")"`、`:528 _scan_stripped "$_stripped"`
`:120 _strip_comments_lex()`(引号感知逐字符) ← **调用者判定**走它
`:157 t="$(printf '%s\n' "$1" | _strip_comments_lex /dev/stdin)"`
★★ 同一行喂给**两个剥离器**,在含 `#` 的行上**结论相反**(现读实测):
行 `true; AGENTMAIL_REQUIRE="x"` ⇒ 两者皆存活 ✓(一致)
行 `AGENTMAIL_REQUIRE="a#b"` ⇒ strip_text 后 `AGENTMAIL_REQUIRE="a`(**形态已断**)
lexer 后 `AGENTMAIL_REQUIRE="a#b"`(**完整存活**)★ 相反
行 `. "$REPO/${X#p}/lib/env-defaults.sh"` ⇒ strip_text 后 `. "$REPO/${X`(**断**)
lexer 后 完整(**存活**)★ 相反
★★★ 后果(我在**调用者通道**上实测,喂 5 个调用者样本让两个剥离器各跑一次谓词):
C2 参数展开 `${X#p}`: lexer→谓词=**1**(真读数) 而 strip_text→谓词=**0**
C3 引号内 `#`: lexer→谓词=**1**(真读数) 而 strip_text→谓词=**0**
⇒ ★★ 若 ③ 一律用 `strip_text` 断言"待测形态存活",这两行会被判成**③=0** ⇒
**把"测了"误判成"没测"** ⇒ 与 pi 想修的错**方向相反**的新误判 ✓
⇒ ★ 正确形式: **③ 的剥离器必须与"它要保护的那条通道"一致** ——
保护裸赋值通道 ⇒ 用 `strip_text`; 保护调用者通道 ⇒ 用 `_strip_comments_lex` ✓
⇒ ★ 一般化(我对 pi 这条补救的补充): **"断言形态存活"这句话是不完整的 ——
必须写成"在**哪一条读取路径**上存活"**; 判据里有几条读取路径,③ 就要有几个版本,
否则"加一条廉价断言"会**把一条通道的缺口换成另一条通道的新缺口** ✓
```
## (D) ✅ 它的 §二 读法收窄我四格逐格复现
```
★ 变异(按行号/整行取原串,先 `bash -n`):
A 格 = lexer 加列 `print out "\t" NR` **+ 谓词尾锚容忍该列**(两者缺一,A 就不是 pi 的 A)
⚠️ 我第一版**漏了谓词容忍** ⇒ 调用者=0 ⇒ 空集守卫响 ⇒ rc=**1** ⇒
差点据此报"pi 的 A 格不成立" —— 而**那是我的变异不完整** ✓(记法见 E)
B 格 = `strip_text` 加列(`sed 's/#.*$//; s/$/\t99/'`)**+ 域收窄**成 `install.sh`
关守卫 = 把整条条件换成 `if false; then`(`:232` 空集、`:250` 下界)——
★ **不是**加假析取项(那条错我上一轮犯过: 析取里加假项**关不掉**条件)
★ 四格实测:
A lexer加列+谓词容忍+守卫开 ⇒ rc=**0** 无 FAIL
A′ 同上 + 守卫全关 ⇒ rc=**0** 无 FAIL ⇒ **够不到** ✓
B strip加列+收窄域+守卫开 ⇒ rc=**1** 首句 `只找到 1 个调用者(下界 3)`
B′ 同上 + 守卫全关 ⇒ rc=**1** 首句 `deploy/install.sh 逐行局部不变量失败`
⇒ ✅ pi 的读法主张**成立**: 沿"关守卫"轴 **rc 在两行里都不变**(A 0→0、B 1→1),
变化**只在句子**(B「下界守卫」→ B′「逐行局部不变量」)⇒
**跨行比较(全关列)用 rc**(A′ 0 vs B′ 1 ⇒ 有分辨力);
**行内比较必须读句子** ⇒ 只读 rc 会把 B 读成"关守卫没影响" ✓
⇒ ★ 这与我们那条"**判据的输出不只是 rc,还有它说了哪句话**"同族 ✓
```
## (E) ⚠️ 我本轮的两个操作失误(照实报)
```
⚠️ ① A 格变异**漏了"谓词容忍该列"** ⇒ 调用者塌成 0 ⇒ 空集守卫响 ⇒ rc=1 ⇒
我一度要报"pi 的 A 格不成立"。★ 停下查账本(`:10049-10053`)才发现
**A 格的定义是两处变异** ⇒ 补齐后与 pi 逐格一致 ✓
⇒ ★ 记法(第三次同族): **"对方的读数不成立"之前,先核我的变异是不是他描述的那**一组**变异** ——
复合变异漏一处,读数就会指向"对方错了"而不是"我漏了" ✓
⚠️ ② 我第一版比较两个剥离器时,用 `repr(line)` 拼进 `bash -c` 的字符串 ⇒
**引号被二次解释** ⇒ 输出全乱(`'AGENTMAIL_REQUIRE=x`)⇒ 我**没把乱码当读数**,
改用"样本写文件、脚本逐行读"的写法才拿到干净读数 ✓
⇒ ★ 与本轮 pi 自报的"并行写同一探针文件"同族: **"夹具错了"与"结论错了"读数上同形** ✓
```
## (F) ✅ 收尾
```
· 实验在 `/tmp/V3`(`git archive HEAD` 快照 + 每格独立工作树; 本仓只读)
· 判据/`deploy/` **一个字节没动**(只报不改); 本轮**未改仓内任何文件**
· 收尾: `deploy/` == HEAD ✓、未跟踪 **0** ✓、工作区已跟踪改动 **0** ✓、判据 md5 `10fd15da…` ✓
```