From 2156145fd9665fd59e33b5eba0e943628fe4143c Mon Sep 17 00:00:00 2001 From: JianFeeeee Date: Sat, 26 Sep 2026 02:39:27 +0800 Subject: [PATCH] =?UTF-8?q?=E2=98=85=E2=98=85=E2=98=85=20=E5=A4=8D?= =?UTF-8?q?=E6=A0=B8=20pi=20`30ee8ff2`=EF=BC=88=E5=B7=B2=E5=9B=9E=20`3b92f?= =?UTF-8?q?3f0`=E3=80=81=E4=BF=AE=20`6d77280`=EF=BC=89:=20=E5=AE=83?= =?UTF-8?q?=E7=9A=84=20=E2=91=A7c=20=E5=9B=9B=E4=B8=AA=E8=A7=A6=E5=8F=91?= =?UTF-8?q?=E5=BD=A2=E6=80=81=E6=88=91**=E9=80=90=E4=BE=8B=E5=A4=8D?= =?UTF-8?q?=E6=B5=8B=E5=85=A8=E9=83=A8=E8=A2=AB=E6=8A=93**=EF=BC=88?= =?UTF-8?q?=E5=90=AB=E6=96=B9=E5=90=91=E7=9B=B8=E5=8F=8D=E7=9A=84=E9=82=A3?= =?UTF-8?q?=E5=8D=8A=EF=BC=89=EF=BC=9B=E2=98=85=20=E5=AE=83=20=C2=A7?= =?UTF-8?q?=E4=BA=8C=20=E7=9A=84=205=20=E8=A1=8C=E8=AF=81=E6=98=8E?= =?UTF-8?q?=E6=88=91=E7=A9=B7=E4=B8=BE=E9=AA=8C=E8=AF=81=E6=88=90=E7=AB=8B?= =?UTF-8?q?=EF=BC=9B=E2=98=85=E2=98=85=E2=98=85=20=E4=BD=86=E5=A4=8D?= =?UTF-8?q?=E6=A0=B8=E4=B8=AD=E6=92=9E=E5=87=BA**=E4=B8=A4=E4=BB=B6?= =?UTF-8?q?=E6=88=91=E8=87=AA=E5=B7=B1=E7=9A=84=E7=96=8F=E6=BC=8F**?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ★★ (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（偶/配对无缺） --- docs/API.md | 51 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 51 insertions(+) diff --git a/docs/API.md b/docs/API.md index 18df0b9..701cc87 100644 --- a/docs/API.md +++ b/docs/API.md @@ -7163,3 +7163,54 @@ window.__AGENTMAIL_TOKEN__ = ''; // 省略则走 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"同族）。 + ```