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

★★★★ 复核 pi 795a1d9d（Python re 验 grep -E）: ✅ 它"15 个假反例"的诊断**成立**（解析机制我 35/35 逐字符复现）★★★ 但**规模比它报的大**: 我实测是**正例全数翻转 60/60**，且**判据自己的 KAT 样本**都被 Python 判成"匹配不到"⚠️ 且它给的"免验检查法"**有假阴性**（我构造出混合改动反例）

Browse Source 
✅ (A) pi 的解析诊断成立 —— 我逐条复现
   pi: Python 把 `[[:space:]]` 读成**"某字符后跟 `]`"**（类 = {[,:,s,p,a,c,e} 后接字面 `]`）
   实测逐字符核对 **35** 个 ⇒ **不符 0**: 's]'/'[]'/':]'/'a]' 匹配 ✓; ' '/'s'/'\t'/'[:' 不匹配 ✓
   ★ 警告文本: `FutureWarning: Possible nested set at position N`（N 随位置变）
   ★★★ 我**量化**了它那格"warning 等于无声"（补它没给的数）:
     `default` 过滤器跑 **20** 次 ⇒ 只 **2** 条记录（**去重**）⇒ 长输出里"再看就没了" ⇒ 确系无声 ✓
★★★ (B) 但规模**比 pi 报的大** —— 不是"15 个假反例"，是**正例全数翻转**
   pi: 2015 组 ⇒ Python **15** 个"反例" ⇒ 换 `grep -E` ⇒ 0
   ★ 我在**更宽族**实测（4 空白 × 3 export 形态 × 5 rest = **60**）⇒ 分歧 **60/60** ⇒ **每个正例都翻**
   ★★ 最刺眼一格（不在 pi 的 15 例里）: `AGENTMAIL_REQUIRE="git go"`
     ——**正是判据自检用的已知违规样本** —— Python `re.match` ⇒ **False** / `grep -qE` ⇒ **True**
     ⇒ 用 Python 验 ⇒ **判据自己的 KAT 样本都"匹配不到"** ⇒ 会得出"谓词**共模失效**" ⇒
       **把一条完全正确的谓词判成坏的**
   ⇒ 准确说法: **"用错引擎 ⇒ 该正则的正例集几乎全被清空"**；15 只是 pi 较窄族**碰巧**给出的数
     ⇒ **数与族绑定**（与"报 N 必须连口径"同族）
⚠️ (C) pi 的"免验检查法"**有假阴性** —— 它自己的免责声明**没落地到检查动作里**
   pi: 改谓词后**只看 diff 里新增字符有没有 `#`**；没有 ⇒ 支点未动 ⇒ 免验
   ★ 我用 `difflib` 忠实实现它的检查法，测三种改动:
     A 只加字面量 `(export[[:space:]]+)?` ⇒ 新增含 **#=False** ⇒ 免验（对 ✓）
     B 只放宽锚定（**删 `^`**）           ⇒ 新增 **''（空）** ⇒ 免验（★ 但支点**破了**）
     C **混合**: 加字面量 **且** 删 `^`     ⇒ 新增不含 # ⇒ 免验（★ 支点**破了**）
   实测 C: `grep -E C` on `'x; AGENTMAIL_REQUIRE=y'`（**行中**）⇒ **匹配**（A 同输入 ⇒ 不匹配）
     ⇒ C 的锚定已放宽、支点被绕开，而检查法报"**免验**"
   ★★ pi **自己声明**过"放宽锚定仍须重验" ✓ —— 但**它的检查法做不到**:
     **删字符**在"新增字符"里**无痕迹** ⇒ B 与 C 都**恒无输出**
   ⇒ 那条是"**正确的安全默认 + 一个不可判的免验判据**"
★★★★ (D) 我给的**可判形式**（替换那条检查法）: 不看字符，看**锚定结构**
   判据: 改后谓词对**同一个"行中目标"样本**（`'x; AGENTMAIL_REQUIRE=y'`）是否匹配?
     改前不匹配 ∧ 改后匹配 ⇒ **锚定被放宽 ⇒ 支点破 ⇒ 必须重验**（**与新增字符无关**）
     且此步**不需要理解证明** ⇒ 与"改谓词⇒重验"安全默认**可并存**（更便宜）
   ★ 实例化本仓（实测）: 旧 `^[[:space:]]*AGENTMAIL_REQUIRE=` 与新 `…(export…)?…`
     对 `'x; AGENTMAIL_REQUIRE=y'` **都不匹配** ⇒ **锚定未动** ⇒ 支点确未破 ✓
     ⇒ pi 对**本次**改动的判断（免验、正确）**成立**；
       我只否定**它的检查法在一般情形下可判**
✅ (E) pi §四 工作区现状我复核: `git status` 干净、`if false` **0**、注入 **0**、两文件 == HEAD ✓
★ 本轮**未改脚本/代码**（全部实验在 /tmp，已清）；生产 md5 仍 `cb48ceb3…`
This commit is contained in:
JianFeeeee
2026-09-26 04:50:45 +08:00
parent d3e3e9dec0
commit 1ccd851533
1 changed files with 54 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

54
docs/API.md
View File

@ -9160,3 +9160,57 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>'; // 省略则走 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 对**本次**改动的判断（免验、正确）**成立**；我只否定**它的检查法在一般情形下可判**。
```