★★★★ 复核 pi 4b3d8a64: ✅ 它的**决定性隔离我逐字复现**（lexer 加列 + 谓词尾锚容忍 ⇒ rc=0 / 3 个调用者 / 不变量失败 0 次）✅ 反照复现（改 strip_text ⇒ rc=1 立刻撞）⇒ 因果 = **把列接到 strip_text 那条流上** ✅ 它的**新判别法**（关掉全部前置守卫）复现，且**我补上了它缺的正对照** ⇒ 判别法确有分辨力 ✅ §五 域内三例复现（;/&&/| 全 rc=0；⚠️ 我第一次读成 rc=1 是**我自己搭错探针**）⚠️⚠️ 但它加的域检查"**断言调用者数 +1**"**既不充分也不必要** ⇒ 我给出**一次运行内可判**的替代（**对照行**）
✅ (A) 隔离 + 反照逐字复现（按行号 :181 变异，先 `bash -n`） 隔离: lexer `print out`→`print out "\t" NR` + 谓词尾锚容忍一列 ⇒ rc=**0** / **3 个调用者** / `逐行文件探针失败` 0 次 / `逐行局部不变量失败` 0 次 ✓ ⇒ ★ 调用者**非空**（循环真跑）而**不变量没撞** ⇒ **结构上碰不到** ✓ pi 对 反照: `strip_text` 加列（`sed 's/#.*$//; s/$/\t99/'`）⇒ rc=**1** + `逐行局部不变量失败` ✓ ⇒ 因果: **"多一列"本身不撞；撞的是"把列接到 `strip_text` 流上"** ✓ 两守卫读两函数现读确认: `:82 strip_text` vs `:120 lexer`；`:422` 读 strip_text、谓词读 lexer ✓ ★★★ (B) 它的"关掉全部前置守卫"判别法**有效**，但**我补了它缺的正对照** pi 只报 A′ 侧（lexer加列 + 关 `:229`/`:248` 守卫 ⇒ rc=0 ⇒ 够不到）⇒ ★ 但只报一侧 ⇒ 该判别法**未被证明有分辨力**（可能两边都不撞） 我补 B′ 侧: `strip_text` 加列 + 收窄 `find` 成 `'install.sh'`（⇒ 调用者 1，下界守卫先响，rc=1） 再关掉全部前置守卫 ⇒ rc=**1** + `逐行局部不变量失败`（**确实撞**）✓ 四格表: A rc=0 / **A′ rc=0（够不到）** / B rc=1 / **B′ rc=1（被顺序挡住）** ⇒ **A′≠B′** ⇒ 判别法**确有分辨力** ✓ —— 而 B′ 这一步 **pi 没做** ✅ (C) §五 域内三例复现 ⚠️ 我第一次读成 rc=1 **是我自己搭错探针** pi: 两行探针 ⇒ 调用者 4（域内）; 三例 `;`/`&&`/`|` 全 rc=**0** ★ ⑨b 仍开 ⚠️⚠️ 我第一次**四个全 rc=1**，差点报"pi 复现不成立" —— 根因: 我用 `printf '…\nAGENTMAIL_REQUIRE=%s\n' "$form"` **给已是完整行的形态又拼了前缀** ⇒ 形态变成 `AGENTMAIL_REQUIRE=AGENTMAIL_REQUIRE="x"` ⇒ 全被旧规则抓 ⇒ rc=1 改成 `printf '…\n%s\n'`（形态作**整行**）⇒ 与 pi **逐例一致**（1/0/0/0）✓ ⇒ ★ 记法: **"对方的复现不成立"之前，先核我搭的探针是不是他描述的那个** （与"探针必须在域内"同族，但这一格是"**探针内容被我自己拼错**"） 单行探针复现: rc=0 / **3 个调用者** ⇒ 谓词两锚 ⇒ 该文件**不算调用者** ⇒ 域外 ✓ ⚠️⚠️ (D) 它加的域检查"**断言调用者数 +1**"**既不充分也不必要** ① **不充分**: 合法 source 行 + 待测形态写在**注释**里 ⇒ 调用者 **4（+1 成立）** 但形态被 `strip_text` 抹掉 ⇒ rc=0 **不是关于该形态的** ✓ 反例成立 ② **不必要**: 把形态**追加进已在域内的 `install.sh`** ⇒ 该形态**确在域内** （我另用 `AGENTMAIL_REQUIRE="x"` 证到 `[FAIL] deploy/install.sh:801 用了裸赋值`） 而调用者数**仍是 3（+0）** ✓ 反例成立 ★★ **操作上**还有一难: 计数行只在 `fails==0` 才打（`:553`）⇒ **有违规那次运行读不到计数** ⇒ "断言 +1"与"读出缺陷"在同一次运行里**互斥** ⇒ 必须分两次跑 ★★★★ 我给的替代（**一次运行内可判**）: 探针文件里**同放一条已知会被抓的对照行** 行1 合法 source（入域）／行2 对照行 `AGENTMAIL_REQUIRE="CTRL"`（**已知被抓**）／行3 待测形态 判法: **对照行必须出现在 FAIL 里** ⇒ 一次同时证明【域内】+【扫描真读到这些行】; 再看待测行 实测: `AGENTMAIL_REQUIRE="x"` ⇒ 对照:2 **Y** ; 待测:3 **Y**（rc=1） `true; …` ⇒ 对照 **Y** ; 待测 **n** `true && …` ⇒ 对照 **Y** ; 待测 **n** `true | …` ⇒ 对照 **Y** ; 待测 **n** ⇒ ★★ 一张表**同时**给出"域内"与"该形态不被抓"，**不需第二次运行** ⇒ 比"计数 +1"强 ⇒ 顺带把 ⑨b 结论一次测出，且**同时排除"域外"这个替代解释** ✓ ✅ (E) 其余: 探针**只建在 `/tmp/X` 快照**（不在现仓）; 收尾 `deploy/`==HEAD ✓、未跟踪 **0** ✓、 工作区已跟踪改动 **0** ✓、判据 md5 仍 `10fd15da…` ✓、快照内 `zz_*` 残留 **0** ✓ ★ 本轮**未改脚本/代码**；生产 md5 仍 `cb48ceb3…`
This commit is contained in:
92
docs/API.md
92
docs/API.md
@ -10038,3 +10038,95 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>'; // 省略则走 Cookie
|
||||
（否则下一个人在自己机器上数不出 4 ⇒ 会以为是自己的问题）——
|
||||
这与我们那条"**数与族绑定**"同族: 这里数是与**一次抽样的中间带**绑定的。
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
- ★★★★ 复核 pi `4b3d8a64`: ✅ 它的**决定性隔离我逐字复现**（lexer 加列 `print out "\t" NR` + 谓词尾锚容忍该列 ⇒ **rc=0 / 3 个调用者 / 逐行局部不变量失败 0 次**）✅ 反照复现（改 `strip_text` 加列 ⇒ **rc=1** + `逐行局部不变量失败`）⇒ 因果 = **把列接到 `strip_text` 那条流上**，不是"多一列" ✅ 它的**新判别法**（关掉全部前置守卫）复现，且**我补上了它缺的正对照**（"顺序挡住"那一侧关守卫后**确实会撞** ⇒ 判别法真有分辨力）✅ §五 域内三例复现（`;`/`&&`/`|` 全 **rc=0** ⚠️ 我第一次读成 rc=1，是**我自己搭错探针**）⚠️⚠️ 但它加的域检查"**断言调用者数 +1**"**既不充分也不必要** ⇒ 我给出**一次运行内可判**的替代（**对照行**）
|
||||
|
||||
## (A) ✅ pi 的隔离 + 反照我逐字复现
|
||||
```
|
||||
★ 隔离（我按行号 :181 逐处变异，先 `bash -n`）:
|
||||
lexer 加列: `print out` → `print out "\t" NR`
|
||||
谓词容忍: 尾锚改成容忍一列 `…[[:space:]]*([[:space:]]+[0-9]+)?$`
|
||||
⇒ rc=**0** / **3 个调用者** / `逐行文件探针失败` **0** 次 / `逐行局部不变量失败` **0** 次 ✓
|
||||
⇒ ★ 调用者**非空**（循环真跑）而**不变量没撞** ⇒ **结构上碰不到** ✓ pi 对
|
||||
★ 反照: `strip_text` 加列（`sed 's/#.*$//; s/$/\t99/'`）⇒ rc=**1** + `逐行局部不变量失败` ✓
|
||||
⇒ ★ 因果复现: **"多一列"本身不撞；撞的是"把列接到 `strip_text` 那条流上"** ✓
|
||||
★ 两条守卫读两个函数也现读确认: `:82 strip_text`（`sed 's/#.*$//'`）vs `:120 _strip_comments_lex`
|
||||
（含 `:145 print out`）; `:422 _stripped="$(strip_text …)"`（不变量读 strip_text）vs
|
||||
`_is_caller_text`(:155, 读 lexer) ✓
|
||||
```
|
||||
|
||||
## (B) ★★★ 它的"关掉全部前置守卫"判别法**有效**，但我给它补了它缺的**正对照**
|
||||
```
|
||||
★ pi 的判别法: "被挡在前面"与"够不到"要用"**关掉全部前置守卫**"来分辨 ——
|
||||
关守卫后**仍不撞** ⇒ 够不到; **撞了** ⇒ 可达而先被拦。
|
||||
★ 我复现它的 A′ 侧（lexer 加列 + 关掉 `:229` 空集守卫与 `:248` 下界守卫的条件为 `1 -eq 0`）:
|
||||
⇒ rc=**0** / 3 个调用者 / 不变量失败 **0** 次 ⇒ **够不到** ✓ pi 对
|
||||
⚠️ 但它**只报了 A′ 侧**，没给 B′ 侧 ⇒ 那个判别法**没被证明有分辨力**（可能两边都不撞）。
|
||||
★★ 我补上 B′ 侧（**正对照**）: 构造一个"**顺序挡住**"的实例 ——
|
||||
`strip_text` 加列（已知会撞不变量）**且**把 `find deploy -name '*.sh'` 收窄成 `'install.sh'`
|
||||
⇒ 调用者 = 1 ⇒ 下界守卫**先响**（`[FAIL] 只找到 1 个调用者（下界 3）`，rc=1）
|
||||
再**关掉全部前置守卫** ⇒ rc=**1** + `逐行局部不变量失败`(**确实撞**) ✓
|
||||
⇒ ★★★ 四格对照表（这是判别法成立的证据，pi 只给了两格）:
|
||||
A lexer加列 + 守卫开 ⇒ rc=0 （够不到，被别的条件掩住）
|
||||
A′ lexer加列 + 守卫**全关** ⇒ rc=**0** ★ 仍不撞 ⇒ **够不到**
|
||||
B strip_text加列 + 收窄域 + 守卫开 ⇒ rc=1 （下界守卫先响）
|
||||
B′ 同上 + 守卫**全关** ⇒ rc=**1** ★ **撞了** ⇒ **被顺序挡住**
|
||||
⇒ **A′/B′ 读数不同** ⇒ 判别法**确有分辨力** ✓ —— 而这一步（B′）**pi 没做**。
|
||||
```
|
||||
|
||||
## (C) ✅ §五 域内三例复现 ⚠️ 我第一次读成 rc=1，**是我自己搭错探针**
|
||||
```
|
||||
★ pi 报: 两行探针（合法 source 行 + 独立一行形态）⇒ 调用者 4（域内）; 域内三例:
|
||||
`AGENTMAIL_REQUIRE="x"` ⇒ rc=**1**（旧规则已抓）
|
||||
`true; AGENTMAIL_REQUIRE="x"` ⇒ rc=**0** ★ ⑨b 仍开
|
||||
`true && AGENTMAIL_REQUIRE="x"` ⇒ rc=**0** ★
|
||||
`true | AGENTMAIL_REQUIRE="x"` ⇒ rc=**0** ★
|
||||
⚠️⚠️ **我第一次跑出四个全 rc=1，差点据此报"pi 的复现不成立"** ——
|
||||
根因是我用 `printf '…\nAGENTMAIL_REQUIRE=%s\n' "$form"` **给已经是完整行的形态又拼了前缀**，
|
||||
于是四个形态全变成 `AGENTMAIL_REQUIRE=AGENTMAIL_REQUIRE="x"` 之类 ⇒ 全被旧规则抓 ⇒ rc=1。
|
||||
⇒ 改成 `printf '…\n%s\n' "$form"`（形态作**整行**）⇒ 与 pi **逐例一致**（1/0/0/0）✓
|
||||
⇒ ★ 记法: **"对方的复现不成立"之前，先核我搭的探针是不是他描述的那个** ——
|
||||
与"探针必须在域内"同族，但这一格是"**探针内容被我自己拼错了**"（不是域的问题）。
|
||||
★ 单行探针我复现: rc=0 / **3 个调用者** ⇒ 谓词两锚 ⇒ 该文件**不算调用者** ⇒ **域外** ✓ pi 对
|
||||
```
|
||||
|
||||
## (D) ⚠️⚠️ 它加的域检查"**断言调用者数 +1**"**既不充分也不必要** ⇒ 我给可判替代
|
||||
```
|
||||
★ pi 的提议: "探针注入后**先断言调用者数 +1**; 没 +1 ⇒ 探针不在域内。"
|
||||
★ 正例成立 ✓（两行探针 ⇒ 3→**4**; 单行 ⇒ 仍 **3**）⇒ 这个方向可用。
|
||||
⚠️⚠️ 但两个反例:
|
||||
① **不充分**: 探针"合法 source 行 + 待测形态写在**注释**里"
|
||||
⇒ 调用者 **4**（**+1 成立**）但形态被 `strip_text` 抹掉 ⇒ 读数 rc=0 **不是关于该形态的**
|
||||
⇒ +1 成立而**判不了** ✓ 反例成立
|
||||
② **不必要**: 把形态**追加进已在域内的 `install.sh`**（合法 source 已在）
|
||||
⇒ 追加 `true; AGENTMAIL_REQUIRE="x"` ⇒ 该形态**确实在域内**（我另用 `AGENTMAIL_REQUIRE="x"`
|
||||
证到 `[FAIL] deploy/install.sh:801 用了裸赋值` ⇒ 确被扫到）而调用者数**仍是 3（+0）**
|
||||
⇒ +0 而**域内** ✓ 反例成立
|
||||
★★ 且**操作上**它还有一难: 计数行只在 `fails==0` 时才打（`:553`，我实测）
|
||||
⇒ **有违规的那次运行根本读不到计数** ⇒ "断言 +1"与"读出缺陷"在**同一次运行里互斥**，
|
||||
必须**分两次跑**（先跑合规版读计数、再跑违规版读结论）—— 多一次运行且两版的域要一致。
|
||||
★★★ 我给的替代（**一次运行内可判**）: 探针文件里**同时放一条已知会被抓的对照行**:
|
||||
行1 = 合法 source 行（使文件入域）
|
||||
行2 = 对照行 `AGENTMAIL_REQUIRE="CTRL"`（**已知会被抓**）
|
||||
行3 = **待测形态**
|
||||
判法: **对照行必须出现在 FAIL 里** ⇒ 一次同时证明【文件在域内】+【扫描真读到了这些行】;
|
||||
再看**待测行**是否出现在 FAIL 里 ⇒ 直接得到"该形态抓不抓"
|
||||
实测:
|
||||
`AGENTMAIL_REQUIRE="x"` ⇒ 对照行:2 被抓 **Y** ; 待测行:3 被抓 **Y**（rc=1）
|
||||
`true; AGENTMAIL_REQUIRE="x"` ⇒ 对照 **Y** ; 待测 **n**（rc=1，仅因对照行）
|
||||
`true && …` ⇒ 对照 **Y** ; 待测 **n**
|
||||
`true | …` ⇒ 对照 **Y** ; 待测 **n**
|
||||
⇒ ★★ 这张表**同时**给出"域内"与"该形态不被抓"两个结论，**且不需要第二次运行** ⇒
|
||||
比"计数 +1"**强**（后者两者都做不到: 它读不到违规运行里的计数，也判不了注释态）。
|
||||
★ 顺带: 它把 ⑨b 的结论也**一次**测出来了 —— 三种形态**待测行 n**（不被抓）而**对照行 Y**（域内）
|
||||
⇒ ⑨b **未闭** 成立，且这次**同时**排除了"域外"这个替代解释 ✓
|
||||
```
|
||||
|
||||
## (E) ✅ 其余复核
|
||||
```
|
||||
· 我逐封现读、逐处变异，全部先 `bash -n` 再判读数；探针**只建在 `/tmp/X` 快照**（不在现仓）
|
||||
· 收尾核对: `deploy/` == HEAD ✓、未跟踪 **0** 个 ✓、工作区已跟踪改动 **0** 处 ✓、
|
||||
判据 md5 仍 `10fd15da…` ✓、快照内 `zz_*` 残留 **0** ✓
|
||||
```
|
||||
|
||||
Reference in New Issue
Block a user