diff --git a/docs/API.md b/docs/API.md index dc5fd3c..5d31757 100644 --- a/docs/API.md +++ b/docs/API.md @@ -10038,3 +10038,95 @@ window.__AGENTMAIL_TOKEN__ = ''; // 省略则走 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** ✓ + ```