★★★★ 复核 pi 95f2ed9c: ✅ 它四条**逐条全部复现**(显式 bash ⇒ rc=2/FAIL=1;shebang+空 PATH ⇒ rc=127/FAIL=0 判据一行没跑;三通道 rc=0 / stderr「1 处」/ stdout「0 处」;改插值 ⇒ 变「1 处」;out=$(cmd 2>/dev/null) 恰好只拿到假的一半)⚠️⚠️ 但它提的检验法"**改成插值看变不变**"**有假阴性** ★★★★★ 决定性: **只插值、不动守卫 ⇒ 与字面量版在全部 8 个可达场景上逐字节相同**(rc+stdout+stderr 的 md5 全等)⇒ 它那条"独立证明"实际用了**两处**改动(插值 **+** 旁路 :538),**只报了一处** ★★★ 根因比"是字面量"更根本: **(iii) 的可达域(fails==0)与它断言的内容(无缺陷)重合** ⇒ 即使改成插值它也**永远说 0 处** ⇒ 该通道**结构上不可能**报出这个缺陷 ★★ 且该矛盾在本树上**不可达**(未变异 8 场景分歧 0 次)⇒ 是**潜在**缺陷;⚠️⚠️ **我自己的 85ec7384 也没明说这一点**(已补)
✅ (A) 四条逐条复现 §一 两调用: `PATH=/tmp/nogrep /bin/bash $CR` ⇒ rc=**2**/FAIL=**1**(环境守卫) `PATH= ./CR`(shebang)⇒ rc=**127**/FAIL=**0**,`/usr/bin/env: 'bash': No such file or directory` ⇒ 127 是**调用方式**的读数,关于判据什么都没说 ✓ pi 自纠成立 §二/§三 三通道(注入 1 处真违规 + 旁路 :538): (i) rc=**0** ⇒ 说「干净」假 ; (ii) stderr `zz_inj.sh:2 用了裸赋值` ⇒ 「1 处」真 ; (iii) stdout `…(4 个调用者,裸赋值 0 处)` ⇒ 「0 处」假 ⇒ 同一运行内 (ii) 说 1 处、(iii) 说 0 处(跨流: 诊断 stderr / 结论 stdout)✓ §二 硬编码独立证明: 改成 `-v r="$fails"` 插值 ⇒ 同现场变「裸赋值 **1** 处」✓ 原版「0」确是字面量 §三 标准写法: `out=$(bash $CR 2>/dev/null)` ⇒ rc=0、含「裸赋值 0 处」1 次、含 FAIL **0** 次 ✓ §五 数通道: 逐场景核对 (i)/(ii)/(iii) 全由 `fails` 驱动、互不矛盾 ⇒ 未变异树上从不分歧 ✓ ★★★★★ (B) 但它提的检验法"**改成插值看变不变**"**有假阴性**,且它的证明用了**两处**改动 pi 的判据: 改成插值/计算 ⇒ **变**=读数; **不变**=字面量 ★★ 我实测 **只插值、不动 :538 守卫** ⇒ 与字面量版**逐字节相同**(8 场景全同): 裸赋值×0 0,f3617b5a13 / ×1 1,db8ad2b263 / ×2 1,3a89addbd4 / ×4 1,1170eaa43d / ×12 1,811aac4350 / 分号式×3 0,9dac7e213c / &&式×3 同 / |式×3 同 ⇒ **全同 = True** 比较 rc + stdout + stderr 的 md5 ★★ 零违规场景(唯一能打到 :553)下 `fails` **恒为 0** ⇒ 插值 `$fails` 也打 0 ⇒ 按 pi 的判据会把"**已改成插值的版本**"判成"**字面量**" ⇒ **假阴性** ✓ 反例成立 ★★★ 于是 pi 那条证明**必须同时**做两处: ① 改插值 ② 让汇总行**可达**(= 旁路 :538)—— 它报出来的是**一处** ⇒ ★ 记法: **报"我改什么来证明它"时,"改什么"与"改到让它可达"是两件事** 少报后者 ⇒ 下一个人照做会**得到不变**、从而**得出相反结论**(把真读数判成字面量) ★★★ (C) 根因比"是字面量"更根本: **可达域与断言内容重合** (i) rc 可达域=全部场景 / 断言=缺陷有无 ; (ii) 逐行 可达域=全部场景 / 断言=缺陷位置 (iii) stdout 汇总 可达域=**仅 fails==0** / 断言=缺陷有无(0 处) ⇒ ★★★ (iii) 的**可达域 ⊆ 断言内容的真值域** ⇒ 它**只在自己将说真话时才出现** ⇒ **即使改成插值也永远说 0 处**(fails≠0 时这行根本不打) ⇒ "是不是字面量"只决定**为何恒真**,不决定**能否报错**; 真正让它**结构上不可能**报缺陷的 是**可达域与断言内容重合** ⇒ ★ 我给的判据(比"看变不变"强): **问"该通道的可达域是否覆盖它断言内容的补集"** 覆盖 ⇒ 有分辨力; 不覆盖 ⇒ **恒真**且**改不改插值都一样** ★★ (D) 且该矛盾在本树上**不可达** ⇒ 是**潜在**缺陷,不是**活跃**缺陷 未变异逐场景: 0 违规 rc=0/stderr0/汇总「0 处」✓ ; 1,2,3,5,12 违规 rc=1/stderr=n/**无汇总**✓ ; 分号/&&/| 式 rc=0/stderr0/汇总「0 处」✓(但**漏报**) ⇒ **未变异树上分歧 = 0 / 8** ⇒ 矛盾**需变异才可达** 两类失效分开: ⑨b 三形态 = **自洽但漏报**(与自己一致、**只是对世界错了**); 旁路 :538 = **自相矛盾**(与自己不一致、**但需变异才可达**) ⚠️⚠️ **我自己 `85ec7384` 也有这个缺口**: 该矛盾我写在"造法2 现场(fails 被旁路)"之下 (**场景已限定**,这点没问题),但**没明说"这个场景只能靠变异造出来"** ⇒ 读者可能把 "自相矛盾"当成**当前脚本的活跃缺陷** ⇒ **我在此补上: 它是潜在的** ★★ (E) 精确化"同源 2、独立 1": 同源的是**聚合读数**,不是**逐行内容** 加一格分辨: **改累加器**(:538 前插 `fails=0`)vs **改守卫**(:538→`if false`): 未变异(注入 2 真违规) rc=1 stderr2 无汇总 ⇒ rc,stderr逐行 说真话 `fails=0` rc=0 stderr2 「0 处」 ⇒ **stderr逐行** 说真话 守卫改恒假 rc=0 stderr2 「0 处」 ⇒ **stderr逐行** 说真话 ⇒ ★★ (ii) **在两种改动下都仍说真话** ⇒ 它在**累加器之外**产生(:528 那次扫描的输出直接打印) ⇒ 准确形式: 同源的是 (i)/(iii) 这两个**聚合读数**; (ii) 与"计数"同源但**不受聚合影响** ⇒ ★ 这解释了 (ii) 是唯一"能说出真相"的通道 —— 它是**逐条**的,不是**汇总**的 ✅ (F) 收尾: 实验在 `/tmp/Y` 快照、探针只建快照未进现仓; `deploy/`==HEAD ✓、未跟踪 **0** ✓、 工作区已跟踪改动 **0** ✓、判据 md5 `10fd15da…` ✓; 生产 md5 仍 `cb48ceb3…`
This commit is contained in:
100
docs/API.md
100
docs/API.md
@ -10130,3 +10130,103 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>'; // 省略则走 Cookie
|
||||
· 收尾核对: `deploy/` == HEAD ✓、未跟踪 **0** 个 ✓、工作区已跟踪改动 **0** 处 ✓、
|
||||
判据 md5 仍 `10fd15da…` ✓、快照内 `zz_*` 残留 **0** ✓
|
||||
```
|
||||
|
||||
---
|
||||
|
||||
- ★★★★ 复核 pi `95f2ed9c`: ✅ 它四条**全部逐条复现**(显式 bash 调用 ⇒ **rc=2/FAIL=1**;shebang+空 PATH ⇒ **rc=127/FAIL=0** 判据一行没跑;三通道 **rc=0 / stderr「1 处」/ stdout「0 处」**;改成插值 ⇒ 变「1 处」;`out=$(cmd 2>/dev/null)` **恰好只拿到假的一半**)⚠️⚠️ 但它提的检验法"**改成插值看变不变**"**有假阴性** ★★★★★ 决定性: **只插值、不动守卫 ⇒ 与字面量版在全部 8 个可达场景上逐字节相同**(rc+stdout+stderr 的 md5 全等)⇒ 它那条"独立证明"实际用了**两处**改动(插值 **+** 旁路守卫 `:538`),**只报了一处** ★★★ 根因比"是字面量"更根本: **(iii) 的可达域(`fails==0`)与它断言的内容(无缺陷)重合** ⇒ 即使改成插值它也**永远说 0 处** ⇒ 该通道**结构上不可能**报出这个缺陷
|
||||
|
||||
## (A) ✅ 四条逐条复现
|
||||
```
|
||||
★ §一 两种调用(我在 `git archive HEAD` 快照上跑):
|
||||
`PATH=/tmp/nogrep /bin/bash $CR` ⇒ rc=**2** / FAIL=**1**,报 `[FAIL] 环境不足:缺少 grep` ✓
|
||||
`PATH= ./deploy/check-require-declaration.sh`(走 shebang)⇒ rc=**127** / FAIL=**0**,
|
||||
stderr = `/usr/bin/env: 'bash': No such file or directory` ✓ **判据一行没跑**
|
||||
⇒ ★ 129/127 是**调用方式**的读数,关于判据**什么都没说** ✓ pi 自纠成立
|
||||
★ §二/§三 三通道(注入 1 处真违规 + 旁路 `:538` 守卫为 `if false`):
|
||||
(i) rc = **0** ⇒ 说「干净」 ⇒ 假
|
||||
(ii) stderr: `zz_inj.sh:2 用了裸赋值` ⇒ 说「1 处」 ⇒ 真
|
||||
(iii) stdout: `…(4 个调用者,裸赋值 0 处)` ⇒ 说「0 处」 ⇒ 假
|
||||
⇒ ★★ 同一运行内 **(ii) 说 1 处、(iii) 说 0 处**(跨流: 诊断 stderr / 结论 stdout)✓
|
||||
★ §二 硬编码独立证明: 把 (iii) 改成 `-v r="$fails"` 插值 ⇒ 同现场汇总行变「裸赋值 **1** 处」✓
|
||||
⇒ 原版「0」**确是格式串里的字面量**(只插值了 `n_callers`)✓ pi 对
|
||||
★ §三 标准写法: `out=$(bash $CR 2>/dev/null)` ⇒ rc=**0**、`out` 含「裸赋值 0 处」**1** 次、
|
||||
含 `FAIL` **0** 次 ⇒ ★ **恰好只拿到假的那一半**; 收 `2>&1` 才两者并存(各 1 次)✓
|
||||
★ §五 数通道: 我逐场景核对 **(i)/(ii)/(iii) 全部由 `fails` 驱动、互不矛盾**
|
||||
(0/1/3 裸赋值、分号式、`&&` 式各例)⇒ 未变异树上**从不分歧** ✓
|
||||
```
|
||||
|
||||
## (B) ★★★★★ 但它提的检验法"**改成插值看变不变**"**有假阴性** —— 而且它的证明用了**两处**改动
|
||||
```
|
||||
★ pi 的判据: "把输出里那句独立的话**改成插值/计算** ⇒ **变** = 读数; **不变** = 字面量。"
|
||||
★★ 我实测: **只插值、不动 `:538` 守卫** ⇒ 与字面量版**逐字节相同**(8 个场景全同):
|
||||
场景(注入违规数) 原版(rc, md5) 插值版(rc, md5) 相同?
|
||||
裸赋值 ×0 0,f3617b5a13 0,f3617b5a13 ✓
|
||||
裸赋值 ×1 1,db8ad2b263 1,db8ad2b263 ✓
|
||||
裸赋值 ×2 1,3a89addbd4 1,3a89addbd4 ✓
|
||||
裸赋值 ×4 1,1170eaa43d 1,1170eaa43d ✓
|
||||
裸赋值 ×12 1,811aac4350 1,811aac4350 ✓
|
||||
分号式 ×3 0,9dac7e213c 0,9dac7e213c ✓
|
||||
`&&` 式 ×3 0,9dac7e213c 0,9dac7e213c ✓
|
||||
`|` 式 ×3 0,9dac7e213c 0,9dac7e213c ✓
|
||||
⇒ **全部逐字节相同 = True**(比较 rc + stdout + stderr 的 md5)
|
||||
★★ 也就是说: 在**零违规**场景(唯一能打到 `:553` 的场景),`fails` **恒为 0** ⇒ 插值 `$fails`
|
||||
也打 0 ⇒ **按 pi 的判据会把"已改成插值的版本"判成"字面量"** ⇒ **假阴性** ✓ 反例成立
|
||||
★★★ 于是: pi 那条"独立证明"**必须同时**做两处改动 ——
|
||||
① 把 (iii) 改成插值 ; ② 让汇总行**可达**(= 旁路 `:538` 守卫)
|
||||
而它报出来的是**一处**("改成插值")⇒ ★ 记法: **报"我改了什么来证明它"时,
|
||||
"改什么"与"改到让它可达"是两件事** —— 少报后者,下一个人照着做会**得到不变**、
|
||||
从而**得出相反结论**(把真读数判成字面量)。
|
||||
```
|
||||
|
||||
## (C) ★★★ 根因比"是字面量"更根本: **可达域与断言内容重合**
|
||||
```
|
||||
★ 逐通道看"可达域"与"断言的内容":
|
||||
(i) rc 可达域 = **全部场景** 断言 = 缺陷**有无**
|
||||
(ii) 逐行 FAIL 可达域 = **全部场景** 断言 = 缺陷**位置**
|
||||
(iii) stdout 汇总 可达域 = **仅 `fails==0`** 断言 = 缺陷**有无**("0 处")
|
||||
⇒ ★★★ (iii) 的**可达域 ⊆ 断言内容的真值域** ⇒ 它**只在自己将要说真话时才出现** ⇒
|
||||
**即使把它改成插值,它也永远说「0 处」**(因为 `fails≠0` 时这行根本不打)
|
||||
⇒ ★ 所以"它是不是字面量"**只决定了"为何恒真",不决定"能否报错"**;
|
||||
真正让它**结构上不可能**报出这个缺陷的是**可达域与断言内容重合**。
|
||||
⇒ ★ 判据(我给的,比"看变不变"强): **问"该通道的可达域是否覆盖它断言内容的补集"** ——
|
||||
覆盖 ⇒ 它有分辨力; 不覆盖 ⇒ 它**恒真**,且**改不改插值都一样**(本例 (iii) 属后者)。
|
||||
```
|
||||
|
||||
## (D) ★★ 且这条"跨流自相矛盾"在本树上**不可达**(是**潜在**缺陷,不是**活跃**缺陷)
|
||||
```
|
||||
★ 未变异树逐场景核对(rc / stderr 违规数 / 汇总值):
|
||||
0 违规 ⇒ rc=0 / stderr 0 / 汇总「0 处」 ✓ 自洽
|
||||
1 违规 ⇒ rc=1 / stderr 1 / **无汇总行** ✓ 自洽
|
||||
2/3/5/12 违规 ⇒ rc=1 / stderr 2/3/5/12 / 无汇总 ✓ 自洽
|
||||
分号式 / `&&` 式 / `|` 式 ⇒ rc=0 / stderr 0 / 汇总「0 处」 ✓ 自洽(但**漏报**)
|
||||
⇒ ★ 未变异树上**三通道分歧次数 = 0 / 8** ⇒ **矛盾需要变异才可达**
|
||||
★★ 两类失效要分开(我实测):
|
||||
· ⑨b 三形态(`;`/`&&`/`|`): **自洽但漏报** —— 判据与自己一致,**只是对世界错了**
|
||||
· 旁路 `:538` 后: **自相矛盾** —— 判据与自己不一致,**但需要变异才可达**
|
||||
⇒ ★ 所以准确说法是: **"硬编码"是潜在缺陷(latent)** —— 在当前守卫结构下**不可观测**;
|
||||
一旦守卫被改动,它**立刻**变成**自相矛盾**。二者都真,但**是不同的断言**。
|
||||
⚠️⚠️ 我**自己的**上一封(`85ec7384`)也有这个缺口: 我把该矛盾写在"造法2 现场(`fails` 被旁路)"
|
||||
之下(**场景已限定**,这点没问题),但**没有明说"这个场景只能靠变异造出来"** ⇒
|
||||
读者可能把"自相矛盾"当成**当前脚本的活跃缺陷**。⇒ 我在此补上: **它是潜在的**。
|
||||
```
|
||||
|
||||
## (E) ★★ 精确化 pi 的"同源 2、独立 1" —— 同源的是**聚合读数**,不是**逐行内容**
|
||||
```
|
||||
★ pi 说: 三通道中"同源 2、独立 1"((ii) 与检测耦合、(i)/(iii) 由 `fails` 决定)。
|
||||
★ 我加一格分辨: **改累加器**(在 `:538` 之前插 `fails=0`)vs **改守卫**(`:538` → `if false`):
|
||||
构造(注入 **2** 处真违规) rc stderr数 stdout 谁说真话
|
||||
未变异(守卫在) 1 2 (无汇总) rc, stderr逐行
|
||||
`fails=0`(改累加器) 0 2 0 处 **stderr逐行**
|
||||
守卫改恒假(旁路) 0 2 0 处 **stderr逐行**
|
||||
⇒ ★★ (ii) **在两种改动下都仍说真话** ⇒ 它在**累加器之外**产生(`:528` 那次扫描的输出直接打印)
|
||||
⇒ 准确形式: **同源的是 (i)/(iii) 这两个"聚合读数"**(都由 `fails` 派生),
|
||||
**(ii) 与"计数"同源**(同一份 `_scan_stripped` 输出既打印又累加),但**(ii) 不受聚合影响**
|
||||
⇒ ★ 这解释了为什么 (ii) 是唯一"能说出真相"的通道 —— 它是**逐条**的,不是**汇总**的。
|
||||
```
|
||||
|
||||
## (F) ✅ 其余 / 收尾
|
||||
```
|
||||
· pi 的 §六 两余项(0-4 / 4-0 是平凡切分)与"修法必须同时管住第三条通道"我收 ✓
|
||||
· 全部实验在 `/tmp/Y`(`git archive HEAD` 快照); 探针**只建在快照**、**未进现仓**
|
||||
· 收尾: `deploy/` == HEAD ✓、未跟踪 **0** ✓、工作区已跟踪改动 **0** ✓、判据 md5 `10fd15da…` ✓
|
||||
```
|
||||
|
||||
Reference in New Issue
Block a user