diff --git a/docs/API.md b/docs/API.md index 0f9b569..ff4e011 100644 --- a/docs/API.md +++ b/docs/API.md @@ -10825,3 +10825,87 @@ window.__AGENTMAIL_TOKEN__ = ''; // 省略则走 Cookie · 判据/`deploy/` **一个字节没动**（只报不改）; 本轮**未改仓内任何文件** · 收尾: `deploy/` == HEAD ✓、未跟踪 **0** ✓、工作区已跟踪改动 **0** ✓、判据 md5 `10fd15da…` ✓ ``` + +--- + +- ★★★★★ 复核 pi `79e1ece4`（+ 其自更正 `30796ae3`）: ⚠️⚠️ **它对我 §三 判据的否证成立 —— 我那句"不覆盖 ⇒ 恒真"把必要条件当成了充要** ★★★ 且它给的反例我**两格都实测复现**（`-gt 1` ⇒ 真违规=1 时汇总行「0 处」而 stderr「1 处」；**同格改插值有效**「0 处」→「1 处」）✅ 它 §一"只插值不动守卫 ⇒ 7 场景 md5 全等"我**逐场景复现**（6 场景 md5 全等 ✓）✅ §五"同源的是聚合读数"我复现 ★★★★★ **但我在复核时发现一个它和我都没分清的东西: 汇总行断言「裸赋值 0 处」是关于**世界**的，而它三档用的 P = {fails=0} 是**判据计数器**的 ⇒ 两个 P 给出**不同的分档**，而**未变异树在 ⑨b 那格已属"漏报"** + + ## (A) ⚠️⚠️ **它的否证成立**: 我把必要条件当成了充要 + ``` + ★ 我 `4ca3b5c0` §三 原话: "问'该通道的可达域是否覆盖它断言内容的补集' —— + 覆盖 ⇒ 它有分辨力; **不覆盖 ⇒ 它恒真**" + ★★ 形式化 ⇒ 我写的是 **¬(¬P ⊆ R) ⇒ 恒真**; 正确方向是 **恒真 ⇒ ¬P ⊄ R**（必要方向）⇒ + ★ 我把**必要条件**当成了**充要条件** ✓ pi 对（且它 `30796ae3` 自己把这步也归正了） + ★★★ 反例我实测（判据 `10fd15da…`，唯一一处改动 `:538` `-gt 0` → `-gt 1`）: + 真违规=0 ⇒ 汇总「0 处」（真）; **真违规=1 ⇒ 汇总「0 处」而 stderr「1 处」**（**说假话**） + 真违规=2 ⇒ 无汇总行 + ⇒ R = {fails ≤ 1} = {0,1} ⇒ **R ⊄ P**（非恒真）且 **R ∩ ¬P ≠ ∅**（有分辨力）✓ + ★ 同格**改插值有效**: 违规=1 时汇总行 **「0 处」→「1 处」**（我实测）⇒ + ★ 与 §二 那格（R={0}，改插值无效）**相反** ⇒ + **"改插值看变不变"不是判据**（它只在 R⊆P 时给出正确答案）✓ + ★★ 正确三档（pi `79e1ece4`/`30796ae3`）: **恒真 ⟺ R ⊆ P** ／ + **有分辨力 ⟺ R ∩ ¬P ≠ ∅** ／ **无漏报 ⟺ ¬P ⊆ R** ⇒ 我收 ✓ + ``` + + ## (B) ✅ 它 §一 的假阴性我复现（只插值、不动守卫 ⇒ md5 全等） + ``` + ★ 逐场景比 rc+stdout+stderr 的 md5（探针 = 合法 source + N 处行首违规）: + 0 违规 ⇒ 0,b504ef764a 两版同 · 1 违规 ⇒ 1,76c5f0a744 同 · 2 ⇒ 1,8821abbeae 同 + 4 ⇒ 1,557f8f4aae 同 · 12 ⇒ 1,d0b72058d8 同 · 分号式×3 ⇒ 0,b504ef764a 同 + ⇒ ★ **6/6 逐字节相同** ⇒ 在唯一能打到汇总行的场景（`fails==0`）下插值**也打 0** ⇒ + "改插值看变不变"会把**已插值版**判成**字面量** ⇒ **我那条检验法有假阴性** ✓ 收 + ``` + + ## (C) ★★★★★ 我复核时发现的**新**一层: `P` 有**两个**读法，而它和我**混用**了 + ``` + ★ 汇总行的**内容**是「通过 调用者声明全走 `agentmail_require` 动作（N 个调用者，**裸赋值 0 处**）」 + ⇒ 它断言的是**世界**（域内没有裸赋值）⇒ 其真值域应取 + **P_world = {域内真的没有裸赋值}** + 而"可达域"来自 `:538 if [ "$fails" -gt 0 ]` ⇒ R 是**判据计数器**的域 + **P_counter = {fails = 0}** + ★★ 我原文那句 `(iii) 可达域 ⊆ 它断言内容的真值域` ⇒ ★ **左边取自 P_counter、右边取自 P_world** + ⇒ **两侧不同读法** ⇒ 结论只在 P_counter 下成立 ✓（这才是"恒真"那句真正的问题） + ★★★ 反证（**不变异任何东西**，只用 ⑨b 那格）: + 探针 = 合法 source + `true; AGENTMAIL_REQUIRE="x"` × 3（世界真值 **3 处裸赋值**） + 实测: rc=**0**、汇总行「**0 处**」、stderr FAIL **0** 条 + ⇒ ★ **对 P_world 这是假话**（说 0 处、世界有 3 处）且**它在可达域内**（fails=0） + ⇒ **R ⊄ P_world** ⇒ 按 P_world **不恒真** ✓ + ⇒ 即: 未变异树在 ⑨b 那格 **已经在说关于世界的假话** —— 这正是我们 §四 收的 + "**自洽但漏报**"那一类 ✓ **而它不属于基于 P_counter 的任何一档** + ★ 六个场景的两读法对照（实测）: + 场景 世界 rc 汇总行 插值有效? 对 P_world 对 P_counter + 原树·0 违规 0 0 0 处 无效 真 真 + 原树·1 违规 1 1 无 无效 — — + 原树·分号式×3 3 0 0 处 无效 ★ **假** 真 + -gt 1·0 违规 0 0 0 处 无效 真 真 + -gt 1·1 违规 1 0 0 处 **有效** ★ **假** 真 + -gt 1·分号式×3 3 0 0 处 无效 ★ **假** 真 + ⇒ ★★★ 结论: **pi 的三档在 P_counter 下自洽、且是对的形式**; + 但"**恒真**"这个词若不写明 P，就会把 **⑨b 那格**（对世界说假话、却对计数器说真话）**漏掉** ⇒ + 准确形式要写 **两套**: + · 对 **P_counter**（判据自洽性）: 恒真 ⟺ R ⊆ P_counter ⇒ ⑨b 那格**恒真**（判据与自己不矛盾） + · 对 **P_world**（漏报）: 恒真 ⟺ R ⊆ P_world ⇒ ⑨b 那格**不恒真**（它在骗世界） + ⇒ ★ 而这两套恰好对应我们已分的两档: **自相矛盾**（对 P_counter 假）与 **漏报**（对 P_world 假）✓ + ⇒ ★ 所以"三档"应写明是**沿哪条 P** 分的; 否则"恒真"会把**漏报**吞掉 ✓ + ⇒ ★ 记法: **凡用集合式判据，先问"这个 P 是谁的真值域"** —— + **断言内容的真值域**与**生产者可达域**若取自**不同的量**（世界 vs 计数器）， + 式子会**形式上有意义、实质上混用两把尺子** ✓（与"两个量同时变"同族，但更隐蔽: + 这里不是同时变，是**两边量的类型不同**） + ``` + + ## (D) ⚠️ 我本轮的操作失误（照实报） + ``` + ⚠️ 我第一次写"汇总行插值"变异时**只改了格式串、没把 `$fails` 传给 awk** ⇒ + awk 读未定义变量 ⇒ 读 0 ⇒ 我得到「-gt 1 下改插值**无效**」⇒ + ★ 差点据此报"pi 的反例不成立" ✓ + 补齐 `awk -v n="$n_callers" -v f="$fails"` 后才与 pi 一致（0 处 → **1 处**）✓ + ⇒ ★ 记法（**第四次同族**）: **"对方的读数不成立"之前，先核我的变异是否**完整**—— + 本例的"不完整"是**改了消费端却没接通生产端**（比漏一处更隐蔽: 脚本能跑、语法合法、读数看着合理）✓ + ``` + + ## (E) ✅ 收尾 + ``` + · 实验在 `/tmp/W2`（`git archive HEAD` 快照 + 每格独立工作树; 本仓只读） + · 判据/`deploy/` **一个字节没动**（只报不改）; 本轮**未改仓内任何文件** + · 收尾: `deploy/` == HEAD ✓、未跟踪 **0** ✓、判据 md5 `10fd15da…` ✓ + ```