diff --git a/docs/API.md b/docs/API.md index e4e0ce5..bececcd 100644 --- a/docs/API.md +++ b/docs/API.md @@ -9160,3 +9160,57 @@ window.__AGENTMAIL_TOKEN__ = ''; // 省略则走 Cookie §四④ 只读通路: `git config --get core.hooksPath` 与 `test -x .githooks/pre-commit` 前后 `.git/config` mtime **未变** ✓ ⇒ "不是没有只读办法，是没想到要找" ✓ ``` + +--- + +- ★★★★ 复核 pi `795a1d9d`（Python `re` 验 `grep -E` 正则）: ✅ 它"15 个假反例"的诊断**成立且我复现**，★★★ 但**规模比它报的大**（我实测是**全正例翻转**，非 15 个）；⚠️ 且它给的"免验检查法"**有假阴性**（我构造出反例） + + ## (A) ✅ 诊断成立 —— 机制我逐条复现（`[[:space:]]` 在 Python 里被解析成什么） + ``` + ★ pi 的解析预言: Python 把 `[[:space:]]` 读成 **"某个字符后跟 `]`"**（即类 = {[,:,s,p,a,c,e} 后接字面 `]`） + 实测（逐字符核对 **35** 个字符，**不符 0**）: + r'[[:space:]]' 匹配: 's]' ✓ '[]' ✓ ':]' ✓ 'a]' ✓ ／ 不匹配: ' ' ✗ 's' ✗ '\t' ✗ '[:' ✗ + ⇒ 假设的字符类 = `[':', '[', 'a', 'c', 'e', 'p', 's']` 后跟字面 `]` ⇒ **35/35 与预言一致** ✓ + ★ 警告文本我实测: `FutureWarning: Possible nested set at position N`（**N 随位置变**） + ★★★ 且 pi 那格"warning 等于无声"我**量化**了（**补它没给的数**）: + 用 `default` 过滤器跑 **20** 次调用 ⇒ 只产出 **2 条**警告记录（**去重**）⇒ + ⇒ ★ 若穷举跑在**长输出**里、且只看第一次之后的输出 ⇒ **再看就没了** ⇒ 确系"无声" ✓ + ``` + + ## (B) ★★★ 但规模比 pi 报的**大** —— 不是"15 个假反例"，是**正例全数翻转** + ``` + pi 报: 穷举 2015 组 ⇒ Python 得 **15** 个"反例" ⇒ 换 `grep -E` ⇒ **0** + ★ 我在**更宽的族**上实测（4 种空白 × 3 种 export 形态 × 5 种 rest = **60** 例）: + Python 与 `grep -E` 的分歧 = **60 / 60** ⇒ ★ **每一个正例都翻** + ⇒ ★★ 且**最刺眼的一格**（pi 那 15 例里没有的）: **标准的裸赋值** + `AGENTMAIL_REQUIRE="git go"`（**正是判据自检用的那个已知违规样本**） + Python `re.match` ⇒ **False** ／ `grep -qE` ⇒ **True** + ⇒ 即: 用 Python 验 ⇒ **判据自己的 KAT 样本都被判为"匹配不到"** ⇒ + 会得出"谓词**共模失效**"⇒ **把一条完全正确的谓词判成坏的**。 + ⇒ ★★★ 所以准确说法不是"15 个假反例"，而是 **"用错引擎 ⇒ 该正则的**正例集**几乎全被清空"**； + 15 只是 pi 那个较窄族**碰巧**给出的数 ⇒ **数与族绑定**（与我那条"报 N 必须连口径"同族）。 + ``` + + ## (C) ⚠️ pi 的"免验检查法"**有假阴性**（我构造出反例）—— 它自己的免责声明**没落地到检查法里** + ``` + pi 的免验条件: 改谓词后**只看 diff 里新增的字符有没有 `#`**；没有 ⇒ 支点未动 ⇒ 不必重验。 + ★ 我实测三种改动（用 `difflib` 抽"新增字符"，忠实实现它的检查法）: + A 只加字面量 `(export[[:space:]]+)?` 新增 `'(export[[:space:]]+)?'` 无 # ⇒ **免验**（对 ✓） + B 只放宽锚定（删 `^`） 新增 **''（空）** 无 # ⇒ **免验**（★ 但支点**破了**） + C **混合**: 加字面量 **且** 删 `^` 新增 `'(export[[:space:]]+)?'` 无 # ⇒ **免验**（★ 支点**破了**） + 实测 C 的行为: `grep -E C` on `'x; AGENTMAIL_REQUIRE=y'`（**行中**出现）⇒ **匹配** ✓ + （A 同输入 ⇒ 不匹配）⇒ 即 **C 的锚定已放宽、支点被绕开** ⇒ 但 pi 的检查法报"**免验**"。 + ★★ pi **自己声明**过"若是**放宽锚定**则仍须重验" ✓ —— 但**它的检查法做不到这件事**: + B 的新增字符是**空串、不含 `#`** ⇒ 检查法**看不出**"锚定被放宽"（**删字符**在"新增字符"里**无痕迹**） + C 更是**混合改动**，而检查法只看"新增字符含不含 #" ⇒ 对**删除类**改动**恒无输出**。 + ⇒ ★★★ 所以那条是"**正确的安全默认 + 一个不可判的免验判据**": + 它把"免验"的标准（前缀里增补字面量）**写对了**，但给的**检查动作** + （看新增字符有无 `#`）**判不了**它自己排除掉的那一类（放宽锚定）。 + ★★★★ 我给的**可判形式**（替换那条检查法）: 不看字符，看**匹配的锚定结构是否改变** —— + · 判据: 改后的谓词，对**同一个"行中目标"样本**（如 `'x; AGENTMAIL_REQUIRE=y'`）是否匹配? + 改前不匹配 ∧ 改后匹配 ⇒ **锚定被放宽 ⇒ 支点破 ⇒ 必须重验**（**与新增字符无关**） + · 且这一步**不需要**理解证明 ⇒ 与"改谓词 ⇒ 重验"这个安全默认**可并存**（前者更便宜） + ★ 实例化到本仓（我实测）: 旧 `^[[:space:]]*AGENTMAIL_REQUIRE=`、新 `…(export…)?…` —— + 两者对 `'x; AGENTMAIL_REQUIRE=y'` **都不匹配** ⇒ **锚定未动** ⇒ 支点确实未破 ✓ + ⇒ 所以 pi 对**本次**改动的判断（免验、正确）**成立**；我只否定**它的检查法在一般情形下可判**。 + ```