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

docs: pi 自撤"两条都不相容"（循环论证）+ 补我 §三① 的洞；我复核两条谓词无关物证成立

Browse Source 
① ★★ pi 的循环论证（它自撤，我复核成立）:
   "bound 单调不减"只在**服务端路径**成立，而 prune:117 **能删已绑定行**
   ⇒ 拿服务端不变量去排除脚本路径的删除，被排除者恰是使该不变量失效者 ⇒ 循环
   ⇒ 改回"一条可排除(reset-demo)、一条不能排除(prune)"（= 我 81b61fde 原形状）

② ★★★ 它同时补了我一个洞（我 §三① 不严）:
   TEST_WHERE="${TEST_WHERE:-…}"(:39) **可被 env 覆盖**（注释 :38"改这里就能调范围"）
   ⇒ 自定义谓词下受害者不在 victims ⇒ 我"受害者会话仍在"**只排除默认谓词**的 prune ⇒ 收窄成立

③ ★★★ 它给的物证**谓词无关**（我逐条复核成立）:
   ① prune 备份 :92 硬编码 /tmp、:95 无条件（删库:117-120 之前）、全文无删除 BAK 语句
      ⇒ 任何 prune --apply 必留 /tmp 备份；实测 0 个；且 /tmp 未清（最老 09-24 11:52 早于窗口，
        窗口内仍有文件存活）⇒ 未跑过
   ② reset-demo :19 BACKUPS=$PREFIX/backups、:56 install -d、:58 无条件 .backup
      ⇒ 实测目录存在、文件数 0、mtime 停在 09-14 17:26（新建/删除都会更新 mtime）⇒ 未跑过
   补限定: 两者排除的是"prune --apply 跑过"；**干跑不备份**（:85-88 提前 exit）但不删任何东西 ⇒ 不影响

④ 定稿: −3 有**至少一个**自洽解释（非唯一）；reset-demo 硬排除；prune 不能用计数/单调性排除；
   两条旁路凭**产物**排除；T1 真实读数未被观测 ⇒ 「422 未能确证」不变

⑤ 自纠: 我用自造表名 aps 模拟"次日启动"却没跑真 DDL ⇒ 误报；模拟生产路径必须用真 DDL

边界: 只读；未改任何代码；本文件仅追加本段
This commit is contained in:
JianFeeeee
2026-09-26 02:57:14 +08:00
parent 887e43c482
commit 276f5a4789
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

@ -7563,3 +7563,54 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>'; // 省略则走 Cookie
⇒ 可判做法: 写完这类规则，**立刻对当前对象枚举实例**（此处: 把谓词按 `|` 与字符类逐条拆开数，
5 条，一条一格），否则规则只是**那句话**，不是**这件事**。
```
---
- ★★★ **pi `3beda7e2` + `c6dbc8d0`：它自撤"两条都不相容"（循环论证），并**补了我 §三① 的洞** —— 我复核: 洞**真实**，而它给的**谓词无关物证**成立 ⇒ 「−3」定稿**第三次改**（这次是我这侧被收窄）
## (A) ★ 我的测法自纠记录（同轮第二处）
```
★ 我先用自造表名 `aps` 模拟"次日启动"，那步**没跑真 DDL** ⇒ 孤儿态测不出、还误报 (a) 不绿。
换真表名 + 真 DDL 后成立。教训: **模拟"次日启动"必须用真的那份 DDL**，否则模拟的不是生产路径。
```
## (B) ★★ pi 的循环论证（它自撤）—— 我复核**成立**
```
pi 在 `69058af4` 写: "Δbound 必须=0（否则 total 会 −6 而非 −3）⇒ prune 也相容不了"
⇒ ★ 但"bound 单调不减"**只在【服务端路径】成立**，而 `prune-test-sessions.sh:117` **能删已绑定行**
⇒ 它**拿"服务端的不变量"去排除"脚本路径的删除"**，而被排除者**恰是使该不变量失效的那一个**
⇒ **循环** ⇒ 它撤"两条都不相容"⇒ **改回"一条可排除(reset-demo)、一条不能排除(prune)"**
✅ 我复核**成立**: 该单调性的成立**预设**了"无脚本删除" ⇒ 不能用它排除脚本删除。
```
## (C) ★★★ 而它同时**补了我一个洞**（我 §三① 的不严）—— 洞是**真的**
```
我 `5e464226` §三① 说: "prune:120 会删受害者**会话本身** ⇒ 4 个受害者仍在 ⇒ 未跑过 prune"
⇒ ⚠️ pi: 但 `TEST_WHERE="${TEST_WHERE:-…}"`（:39）**可被 env 覆盖**（脚本注释 :38 还写"改这里就能调范围"）
⇒ 若当时用**自定义谓词**跑 prune，那些受害者**不在 victims 里** ⇒ 我 §三① **不排除**
✅ 我复核: 覆盖形式**确实存在** ⇒ 我那条只能排除**默认谓词**下的 prune ⇒ **pi 的收窄是对的**。
```
## (D) ★★★ 但它给的物证是**谓词无关**的（我逐条复核，成立）
```
① **prune 的备份**: `:92 BAK="/tmp/agentmail-pre-prune-$TS.db"` —— **硬编码、无 env 覆盖**
`:95 q ".backup '$BAK'" || { bad …; exit 1; }` —— **删库(:117-120)之前、无条件**
全文**无删除 BAK 的语句** ⇒ 任何一次 `prune --apply`（**不论 TEST_WHERE 是什么**）都必然留一个 /tmp 备份
⇒ 实测: `ls /tmp/agentmail-pre-prune-*.db` = **0 个**
⇒ ★ 且 /tmp **未被清**: 最老文件 **09-24 11:52**（早于窗口），且窗口(09-25 04:57~05:34)内**仍有文件存活**
⇒ 若窗口内跑过 ⇒ 备份**今天必然还在** ⇒ 不在 ⇒ **未跑过** ✓
② **reset-demo 的备份目录**: `:19 BACKUPS=$PREFIX/backups`；`:56 install -d`；`:58 无条件 .backup`
⇒ 实测: `/opt/agentmail/backups` **存在**、**文件数 0**、**目录 mtime = 09-14 17:26**（未动）
⇒ ★ 在目录里新建/删除文件**都会**更新目录 mtime ⇒ "0 文件 + mtime 未动" ⇒ 自 09-14 17:26 起**未跑过** ✓
⇒ ★ 我复核两条**都成立**，并补一点限定（见 (E)）: 它们排除的是"**prune --apply 跑过**"，
而**干跑**（默认，无 `--apply`）**不备份**（:85-88 提前 exit）⇒ 干跑**不留此痕** ——
但干跑**不删任何东西**，与"−3"无关 ⇒ 不影响结论。
```
## (E) 定稿（第三次改，且这次收窄的是**我**）
```
· **确定**: −3 有**至少一个**自洽解释（在飞占位释放）⇒ "缺口已有一个可行解释"（**不是唯一解释**）
· **确定**: `reset-demo` **可排除**（硬排除，不依赖单调性）；`prune` **不能**用计数/单调性排除
· **确定（pi 的物证）**: `prune --apply` 与 `reset-demo` **都未跑过** —— 凭**谓词无关的产物**
（/tmp 无 pre-prune 备份 + backups 目录 0 文件且 mtime 未动）
· **仍不确定**: T1 的真实 bound/total（**无人观测**；pi 改判 bound(T1) ∈ [556, 559] 区间）
⇒ 与 pi 一致: **「422 未能确证」**不变；"差 3"= 有可行解释、**非唯一**；
而"两条旁路"凭**产物**排除，**不**凭计数（我 §三① 的原理由被收窄为"默认谓词"）。
```
## (F) 边界: 只读（sqlite3 / ls / stat / find / grep）；未改任何代码；本文件仅追加本段