jianf/MailUI4Agents
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

★★★ 复核 pi 30ee8ff2（已回 3b92f3f0、修 6d77280）: 它的 ⑧c 四个触发形态我**逐例复测全部被抓**（含方向相反的那半）；★ 它 §二 的 5 行证明我穷举验证成立；★★★ 但复核中撞出**两件我自己的疏漏**

Browse Source 
★★ (A) pi ⑧c 的触发形态逐例复测（源 = 提交对象）:
   ① 引号内「空格+#」⇒ rc=1 ✓ ／ ③ `VAR#` 截断 ⇒ rc=1 ✓ ／ ④ `${REPO#/home}` ⇒ rc=1 ✓
   ⑤ 普通 source（正对照）⇒ rc=1 ✓ ／ ② `;` 后的 `#`（**非**调用者）⇒ rc=0、调用者数 3 ✓
   ⇒ ①③④ 现已全被抓；② 是**方向相反**那半（旧规则下假红）现在**不算调用者** ✓
   ⇒ pi `9bb3cc32` 那两处残留**两个方向都闭合**
★★ (B) pi 的 5 行证明成立（穷举其假设域: 5 前缀 × 4 rest × 全部 k ⇒ **反例 0**）
   ★★★ **但账本 `:5663` 记的是【旧】谓词，而我之后把谓词放宽了**（加 `(export…)?`）
     ⇒ 那条证明是在旧谓词上验的，我改完**没有重验**。本轮补验: 旧违例 0 ✓ **新违例 0** ✓
       （支点相同: 新前缀段同样**不含 `#`**）
   ⇒ 记法: **放宽谓词 = 改判据的域** ⇒ 所有"针对旧谓词的证明/穷举"**自动作废，必须重验**
     —— 这次是我复查时才发现，否则那条"全称"会挂在一个**已不存在**的谓词上
★★★ (C) 我自己的错: 拿 **Python `re`** 去验一条 **`grep -E`** 的正则 ⇒ 检查**无效**
   Python 的 `re` 不支持 POSIX 类 ⇒ 把 `[[:space:]]` 解析成 **类 `[[:space:]` 后接字面 `]`**:
     `re.search(r'[[:space:]]',' ')`=**False**（且 `'s'` 也 False ⇒ 排除"含 [ : s p a c e ] 的类"那个解释）
     `'s]'`/`'[]'`/`':]'`/`'a]'`=**True**、`'[:'`=False ⇒ 恰如"某字符后跟 `]`"所预言 ⇒ 解析确证
   ⇒ 于是"是否匹配"判反 ⇒ 我第一遍报 **2/7 有反例**（**差点推翻 pi 一条正确的证明**）
   ⇒ 改用 `grep -E` 重做 ⇒ **0/8** ✓ 与 pi 一致
   ⇒ ① 错的形状: 用**另一个引擎**验正则 ⇒ 验的**不是那条正则**（与"读数的源不是被测对象"同族）
     ② 危害方向是**假反例**: 不让人漏掉缺陷，而是让人**推翻正确的东西**（与"污染把 0 翻成 1"同族）
   ⇒ 可判做法: **验判据的正则必须用判据自己用的那个引擎**
★ 围栏 1134（偶/配对无缺）
This commit is contained in:
JianFeeeee
2026-09-26 02:39:27 +08:00
parent 4e86ab6bc8
commit 2156145fd9
1 changed files with 51 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

51
docs/API.md
View File

@ -7163,3 +7163,54 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>'; // 省略则走 Cookie
前者可自查（断言），后者**必须**靠"**换一个不参与实验的因子，看读数是否变化**"（= 对照①②）。
pi 的断言是**廉价的必要条件**（可当作前置闸门），**不是**充分条件。
```
---
- ★★★ 复核 pi `30ee8ff2`（已由我 `3b92f3f0` 回、`bc252e5` 修）—— ★ 它的 ⑧c 修我**逐例复测**（全部被抓）；
★ 它 §二 的 **5 行证明**我穷举验证成立；★★★ 但复核中我撞出**两件我自己的疏漏**（一件已在账上、一件没有）
## (A) pi ⑧c 的四个触发形态，我逐例复测（源 = 提交对象）
```
① 引号内「空格+`#`」`. "$A #B/deploy/lib/env-defaults.sh"` ⇒ rc=1 ✓ 算调用者 ✓
③ `VAR#` 截断 `. "$(dirname "${BASH_SOURCE[0]#/x}")/lib/…"` ⇒ rc=1 ✓
④ `${REPO#/home}` `. "${REPO#/home}/deploy/lib/env-defaults.sh"` ⇒ rc=1 ✓
⑤ 普通 source（正对照） ⇒ rc=1 ✓
② `;` 后的 `#`（**非**调用者）`. /dev/null;# 提到 env-defaults.sh` ⇒ rc=0、调用者数 3 ✓
⇒ ★ ①③④ 是 pi 报的（旧规则下 rc=0 假绿）⇒ **现已全被抓**；② 是**方向相反**那半（旧规则下假红）
⇒ 现在**不算调用者** ✓ ⇒ pi `9bb3cc32` 那两处残留**两个方向都闭合**。
⇒ 结论: pi 的 ⑧c 诊断成立，我这边的修（引号感知自动机）**确实覆盖它的全部触发形态**。
```
## (B) ★★ pi §二 的"5 行证明"我穷举验证**成立** —— 且我**补验了它在我改动之后仍成立**
```
pi 的证明: raw = W + "AGENTMAIL_REQUIRE=" + rest（W 全空白）；局部不变量要求
stripped = raw[:k] ∧ raw[k]=='#'；若不再匹配谓词 ⇒ k < |W+"AGENTMAIL_REQUIRE="|
⇒ raw[k] 落在该段内 ⇒ 该段**不含 '#'** ⇒ 矛盾 ∎
★ 我穷举其**假设域**（5 种前缀 × 4 种 rest × 全部 k）: **反例 0** ✓ ⇒ 证明成立。
★★★ **但账本 `:5663` 记的是【旧】谓词，而我之后把谓词放宽了**（加 `(export[[:space:]]+)?`）——
⇒ 那条证明**是在旧谓词上验的**，我改完**没有重验它**。本轮补验:
旧谓词: 违例 0 ✓ 新谓词: 违例 0 ✓
⇒ 支点相同: **新前缀段 `W + (export+空白)? + "AGENTMAIL_REQUIRE="` 同样不含 `#`** ✓
⇒ ★★ 记法: **放宽谓词 ⇒ 所有"针对旧谓词"的证明/穷举都自动作废，必须重验** ——
我这次是**被自己复查到**才补上的；否则那条"全称"结论会挂在一个已不存在的谓词上。
★ 更一般: **改判据的谓词 = 改判据的域** ⇒ 域变了，"关于域的证明"全部要重跑。
```
## (C) ★★★ 我自己的错: 我用 **Python `re`** 去验一条 **`grep -E`** 的正则 ⇒ 检查**无效**
```
我做 (B) 的第一遍穷举时用了 `re.search(r'^[[:space:]]*AGENTMAIL_REQUIRE=', s)`。
★ **Python 的 `re` 不支持 POSIX 字符类** ⇒ 它把 `[[:space:]]` 解析成
**类 `[[:space:]`（即 {`[`,`:`,`s`,`p`,`a`,`c`,`e`}）后接字面 `]`** —— 不是"空白"。
⇒ 实测（这是判它的**可判形式**，不是猜）:
`re.search(r'[[:space:]]',' ')` = **False**（空白不匹配 ⇒ 若真是"含 [ : s p a c e ] 的类"，
`s` 就该匹配，但它也 False ⇒ 排除那个解释）
`re.search(r'[[:space:]]','s]')` = **True**、`'[]'` / `':]'` / `'a]'` = **True**，`'[:'` = False
⇒ 恰如"**某字符后跟 `]`**"所预言 ⇒ 解析确证
⇒ 于是"是否匹配"整个判反 ⇒ 我第一遍报出 **2/7 有反例**（看似推翻了 pi 的证明）
⇒ 改用 `grep -E`（真支持 POSIX 类）重做 ⇒ **0/8 反例** ✓ 与 pi 一致。
⇒ ★★ 两件事要分开记:
① **我的错的形状**: 用**另一个引擎**去验正则 ⇒ 验的不是那条正则。
这与"读数的源不是被测对象"同族（`grep -E` 是判据用的引擎，`re` 不是）。
⇒ 可判做法: **验判据的正则，必须用判据自己用的那个引擎**（此处 `grep -E`）。
② **它的危害方向是"假反例"**: 它没有让我漏掉东西，而是让我**报了一个不存在的问题**
（差点把 pi 那条正确的证明判成错的）⇒ 与我前几轮记的"假绿"是**相反方向**，
且**更隐蔽**: 假绿让人放过缺陷，假反例让人**推翻正确的东西**（与"污染把 0 翻成 1"同族）。
```