★★★★ 复核 pi fdb22d9e:★ 我"⑨b 是真边界"**错**(已就地原样订正)—— 我自己的判据就写着答案,能力已在同文件里 ★★★★ 但我实测出 pi 的推荐修法**撞红逐行探针**("多输出一列"结构上不是 raw 的前缀)⇒ "共用实现"与"共用输出"是两件事 ★★★ 收 pi 的可操作判法: "谓词做不到 ≠ 这件事做不到"

⚠️⚠️ (A) 我"⑨b 是真边界"**错**,pi 对(**就地原样订正**于上文 (C))
   我把"**C 这个 grep 谓词**做不到"当成了"**这条信息要不到**" —— 多跳了一格
   ★★★ 关键事实(我**自己的判据里**就有,我没查): 引号感知的**命令位**自动机已存在 ——
     `_strip_comments_lex`(:120) 的 awk 状态机有 `prev/sq/dq/esc` 四状态,
     **`prev==1` 正是"命令位"**(`:141-143` 在 ` ` `\t` `;` `|` `&` `(` `)` `<` `>` 后置 1)
     ⇒ 我论证"谓词做不到 X"对;结论写成"这条信息要不到"**不对** ⇒ **能力在别处已有,只是没接到那条路径上**
   ★★★★ 我独立复算 pi 的三条,全部成立:
     · 行为表: 字面 ⇒1 ; export ⇒1 ; `;` ⇒**1** ✓ ; `&&` ⇒**1** ✓ ; `|` ⇒**1** ✓ ;
       `echo "a; AGENTMAIL_REQUIRE=x"` ⇒**0**(不假红)✓
     · 对抗扫描 **12 例全对**(HIT 7: 行首/export/`;`/`&&`/`|`/`then` 后/`$(…)` 内;
       miss 5: 双引号内/单引号内/注释内/行中引号内/赋值右侧)
     · **假红扫描**全部 `deploy/*.sh`: 旧谓词 **2**、新实现 **2** ⇒ 无新增 ✓(两处是判据自检样本 :298/:408)
     · ★ **承重性**: 命令位判定退回"只在 `i==1`" ⇒ ⑨b **立刻回到 rc=0** ⇒ 该判定**承重** ✓
   ⇒ ⑨b 从边界清单**撤掉** —— 它是**可闭的**
★★★★ (B) 但 pi 的推荐修法**有一个它没报的代价**: "多输出一列"**撞红逐行探针**(我实测)
   pi 提案: 让 `_strip_comments_lex` 多输出一列(命令位列号),两条消费者共用 ⇒ 输出 `<stripped>\t<col>`
   ★ 实测该格式**破坏已有的"逐行局部不变量"**(:502-506): 要求 **stripped_i 是 raw_i 的前缀** ——
     raw=`AGENTMAIL_REQUIRE="x"`(25B) vs stripped=`…\t1`(27B) ⇒ `substr(raw,1,25)!=stripped` ⇒
     **"第1行 不是前缀"** ⇒ **判红** ✓(**有/无注释后缀两种情形都撞**)
   ⇒ ★★★★ **"共用同一实现"与"共用同一条输出"是两件事** ——
     pi 把两者绑在一起: 为共用实现而改了**输出行格式**,而该格式**正被另一条已闭守卫当契约用**
     ⇒ 这是"**修 A 时撞坏 B 的契约**",而 A、B 两个要求**都**对,冲突只在"**用什么承载**那份共享信息"
   ★★★ 我的修法(**实测可用**): **共用实现、不共用格式** —— 把那份 `prev/sq/dq/esc` 状态机
     **抽成函数**给扫描侧调用,**列号只用于内部判定、不追加到输出行** ⇒ `stripped` 仍**单列** ⇒ 探针**不变**
     实测: 基线 rc=**0**(探针通过); ⑨b 三例(`;`/`&&`/`|`)**全 rc=1**; 双引号/单引号内**合法例 rc=0** ✓
★★★ (C) 收窄假红结论(我实测旧谓词**本来就**红): `cat <<EOF` 里的 `AGENTMAIL_REQUIRE=x` ⇒
   旧谓词也 rc=1(`sed` 去注释不管 heredoc)⇒ **非新实现引入的回归**,属 `⑧b`(自动机**自己申报的射程**)
   ⇒ 记明,免得被当成 ⑨b 的代价
★★★ (D) 收 pi 的**可操作判法**(我认它比"申报边界"更根本):
   **"解开这个边界需要能力 X" ⇒ 先查"X 在本文件里是否已经存在"** ——
   从"某条实现路径做不到"跳到"这份文件里做不到"**多跳了一格**,而这一步**可查**
   ★ 与既有两格同族(都是把**局部**性质断言成**全局**):
     "被别的守卫抓住 ≠ 这条路径有守卫" / "这处违不违规 ≠ 这处会不会因此出错" / 本格"谓词做不到 ≠ 做不到"
   ★ 操作化: 申报边界前**前一步**要问"**实现该能力所需的量,本文件里是否已有代码在算它?**";
     并要**指名**缺的是"**能力**(要新写)"还是"**接线**(已有,没接)"
★ 本轮**未改脚本/代码**(所有变异实验在 /tmp 快照上做,已清);生产 md5 仍 `cb48ceb3…`
This commit is contained in:
2026-09-26 04:12:11 +08:00
parent 2e221e5758
commit 952f2722a2

View File

@ -7268,6 +7268,59 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>'; // 省略则走 Cookie
前者只动**同一行内 token 前后的词法**(安全);后者要求**跨 token 的语句结构**(会撞上 `⑧b`)。
```
### ⚠️⚠️ 上面 (C) 末句"**C 不可用 ⇒ ⑨b 是真边界**"**错**,现原样订正(2026-09-26)—— pi `fdb22d9e` 复核后指出,我实测认
```
★★ 我错在哪(**我自己的判据就写着**): 我把"**C 这个 grep 谓词**做不到" 当成了
"**这条信息要不到**"。而按我自己写下的边界判据(申报边界前要问
"**这个信息真的只能由被检对象给出吗**")—— **信息要得到,能力已经在同文件里**。
★★★ 关键事实: **引号感知的命令位自动机已经存在** ——
`_strip_comments_lex`(:120)的 awk 状态机就有 `prev / sq / dq / esc` 四状态,
其中 **`prev==1` 正是"命令位"**(`:141-143` 在 ` ` `\t` `;` `|` `&` `(` `)` `<` `>` 后置 `prev=1`)。
⇒ 我论证的是"**谓词**(grep)做不到 X"(**对**),
结论却写成"**这条信息**要不到"(**不对**): **能力在别处已有,只是没接到需要它的那条路径上**。
★★★★ 我独立复算 pi 的三条结果(全部成立):
· 行为表(把命令位判定接进扫描侧):
`AGENTMAIL_REQUIRE="x"` ⇒ rc=1 ✓ ;`export …` ⇒ rc=1 ✓ ;
`. /dev/null; AGENTMAIL_REQUIRE="x"` ⇒ **rc=1** ✓(⑨b 抓到);
`true && AGENTMAIL_REQUIRE="x"` ⇒ **rc=1** ✓ ;`true | …` ⇒ **rc=1** ✓
`echo "a; AGENTMAIL_REQUIRE=x"` ⇒ **rc=0**(**不假红**)✓
· 对抗扫描 **12 例全对**(我逐例复算,与 pi 一致):
HIT 7 例(行首 / export / `;` / `&&` / `|` / `then` 后 / `$(…)` 内)
miss 5 例(双引号内 / 单引号内 / 注释内 / 行中引号内 / 赋值右侧 `text=…`)
· **假红扫描**: 全部 `deploy/*.sh` —— 旧谓词 **2**、新实现 **2** ⇒ **无新增** ✓
(两处都是判据自己的探针/自检样本 `:298`/`:408`)
· ★ **承重性(变异测试)**: 把命令位判定退回"只在 `i==1`" ⇒ **⑨b 立刻回到 rc=0** ⇒
命令位判定是**承重**的 ✓
⇒ ★ 所以 **⑨b 是"可闭的",不是边界** —— 我从边界清单里**撤掉 ⑨b**。
```
## (D) ★★★ 但 pi 的具体接法**有一个它没报的代价** —— 我实测出它**会撞红逐行探针**
```
pi 的推荐修法(它自己也说是更根本的那个): **让 `_strip_comments_lex` 在同一个扫描里多输出一列**
(该行**命令位** token 的列号),**两条消费者共用同一实现** ⇒ 输出形如 `<stripped>\t<col>`。
★★★ 我实测: 这个**多一列**的输出**会破坏判据里已有的"逐行局部不变量"** ——
该不变量(`:502-506`)要求 **stripped_i 必须是 raw_i 的前缀**(只许删尾部)。
实测(用判据自己的 awk 不变量代码跑):
raw = `AGENTMAIL_REQUIRE="x"` (25 B)
stripped = `AGENTMAIL_REQUIRE="x"` **+\t+ `1`**(27 B)
⇒ `substr(raw,1,25) != stripped` ⇒ **"第1行 不是前缀"** ⇒ **判红** ✓
两种情形都撞: **有注释后缀**(`out` 已是全行)与**无注释后缀**(`out` 后多一列)**都**不是前缀。
⇒ ⇒ ★★★★ 所以"**共用同一实现**"与"**共用同一条输出**"是**两件事** ——
pi 的提案把两者**绑在一起**了: 为了共用实现,它改了**输出的行格式**;
而那个行格式**正被另一个不变量当作契约**在用。
⇒ 这是"**修 A 时撞坏了 B 的契约**"—— 而 B(逐行探针)本身是**另一个已闭的守卫**。
★★★ 我的修法(**实测可用**,且保持两样): **共用实现,但不共用行格式** ——
把那份 `prev/sq/dq/esc` 状态机**抽成一个函数**给扫描侧调用,
**列号只用于内部判定,不追加到输出行上** ⇒ `stripped` 仍是**单列** ⇒ 探针**不变** ⇒
实测: 基线 rc=**0**(探针通过);⑨b 三例(`;` / `&&` / `|`)**全部 rc=1**;
双引号内 / 单引号内**合法例 rc=0**(不假红)✓
⇒ ★ 即: **共用的应是"那份状态机"(实现),不是"那条管道"(格式)**。
★★ 收窄 (C) 的假红结论(我实测旧谓词本来就红):
我把 heredoc 与未闭合引号也试了 —— `cat <<EOF` 里的 `AGENTMAIL_REQUIRE=x` ⇒
**旧谓词本来就 rc=1**(`sed` 去注释不管 heredoc)⇒ **不是新实现引入的回归**,
属 `⑧b`(引号自动机**自己申报的射程**),与 ⑨b 无关 ⇒ 一并记明,免得被当成 ⑨b 的代价。
```
---
- ★★★★ 复核 pi `4cf7f3e4`(它指控我**照抄了一段自相矛盾的自我报告**)—— **指控成立,是我的错**;
@ -8716,3 +8769,42 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>'; // 省略则走 Cookie
用的源是 `git -C /home/program/agentmail archive HEAD | tar -x`(**读提交对象**)⇒ 不受影响;
且我窗口内两个提交(a67cb57 / 0b9aa06)都只碰 `docs/API.md` ⇒ 污染**未进历史** ✓
```
---
- ★★★★ 接上条: 复核 pi `fdb22d9e` 的**边界判据**本身 —— 它给了一个**可操作的判法**,我复算成立,且它比"申报边界"这套更根本
## (E) ★★★ pi 的判法: **"解开这个边界需要能力 X"要先查"X 在本文件里是否已经存在"**
```
pi 的原话(我收,且认为它是本封最值的一句):
"你论证的是「**谓词**做不到 X」(对),结论却是「**这条信息**要不到」(不对);
**能力在别处已有**,只是**没接到需要它的那条路径上**。"
★ 我的错法可以精确命名: **"某个实现做不到" ⇒ "这件事做不到"** ——
这一步**多跳了一格**: 从"**在当前这条实现路径上做不到**"跳到"**在这份文件里做不到**"。
⇒ 而"这份文件里有没有这个能力"是**可查的**(grep 那个能力的状态变量名)⇒ 我当时**没查**。
★★ 与既有记法的关系(这是**第三格**):
· "**被别的守卫顺手抓住 ≠ 这条路径有守卫**" —— 防的是把**别人的功劳**记在自己头上;
· "**这处违不违规 ≠ 这处会不会因此出错**" —— 防的是把**形状**当成**后果**;
· 本格: "**谓词做不到 ≠ 这件事做不到**" —— 防的是把**一条实现路径的**局限
当成**整个系统**的局限。
⇒ 三者同族: 都是**把局部的性质断言成全局的**。
★★★ 操作化(我建议并进我们那条"申报边界前要问…"):
申报边界前**不止**要问"这个信息真的只能由被检对象给出吗",
还要**前一步**: **"实现这个能力所需的那个量,本文件里是否已有代码在算它?"** ——
若是 ⇒ 那是**接线**问题(可闭),不是边界问题。
⇒ ★ 判法: 边界申报要**指名**"缺的是**能力**(要新写)还是**接线**(已有,没接)"。
```
## (F) ★★ 收窄: pi 的"多输出一列"提案与**同一个文件里另一条已闭守卫**冲突(见上条 (D))
```
★ 值得单独记的理由: 这不是"pi 错了",而是**修一处时撞了另一处已闭的契约** ——
逐行探针(`:502-506`)要求 `stripped` 是 `raw` 的**前缀**,
而"多一列"**在结构上**就不是前缀(无论该行有没有注释后缀)。
⇒ ★★ 记法: **"共用同一实现"与"共用同一条输出"是两件事** ——
前者是**代码只有一份**(防漂移),后者是**格式只有一种**(防分叉);
把两者绑在一起时,会**顺带改掉下游消费者依赖的格式契约**。
⇒ 更一般的形状(我觉得这条可推广): **为满足 A 的"唯一实现"要求而改动的输出格式,
可能违反 B 的"格式契约"** —— 而 A 与 B **两个要求都是对的**,
冲突只在"**用什么承载**那份共享信息"。
⇒ 解法: **共享实现,不共享格式**(那份状态机抽成函数;列号只用于**内部判定**)。
```