★★★★★ 复核 pi 47c49ef1(守卫顺序): ✅ 它的顺序主张逐项复现(两端锚定先响 ⇒ 关掉空集+下界后两列版 rc=0、不变量无从跑)✅ 三条代价我认 ★★★★ 但★ **我原信 40767c9f 一处不准确被我自己抓出**: 两条守卫读**两个不同函数**(逐行不变量读 strip_text :82/:422,而非 lexer :120/:145)⇒ 改 lexer 加列**结构上碰不到**不变量(我加了谓词容忍使调用者非空, 实测 rc=0/不变量 0 次)⇒ "多一列会撞不变量"**错**; 撞的是"把列接到 strip_text 这条流上" ⚠️ 且我**第一次 ⑨b 探针不在域内**(rc=0 与"已闭"同形)—— 用正确探针才复现 pi 的结论

✅ (A) 关键事实: 两条守卫读**两个不同**函数
   `:82 strip_text` = `sed 's/#.*$//'` ; `:120 _strip_comments_lex` 含 `:145 print out`
   `:422 _stripped="$(strip_text …)"` ← **逐行不变量读 strip_text**
   `:181` 谓词(两端锚定)在 `_is_caller_text`(:155),输入走 **lexer**
   ⇒ "加一列"撞哪条守卫,**取决于加在哪个函数上** ⇒ 两条**独立**数据流
✅ (B) pi 的顺序主张逐项复现(结果对,机制我补一条)
   `print out "\t" NR`(改 lexer)⇒ rc=1 FAIL=1,报的是**空集守卫 `:230`**(**不是**不变量)
   机制: 谓词**两端锚定**(`:181` 头锚 `^[[:space:]]*(\.|source)`、尾锚 `["']?[[:space:]]*$`)
     ⇒ 行尾多 `\t0`(**`0` 非空白**)⇒ 尾锚不匹配 ⇒ 调用者集合空
   ★ 我另测列放**前置**(`print NR "\t" out`)⇒ 同样 rc=1/空集=1,破的是**头锚**
     ⇒ ★ **列放哪一端都破锚**(两个方向各一)
   ★ 复现"关掉空集+下界后两列版 rc=0": 只把 `:229`/`:248` 两条件改 `if false`(体不动)
     ⇒ **rc=0 FAIL=0**,打"通过 …(**0 个调用者**,裸赋值 0 处)" ⇒ **不变量无机会跑** ✓
★★★★ (C) 订正我自己原信的不准确(比 pi 那格更根本)
   我原写"你的推荐修法(多输出一列)**撞红逐行探针**" ⇒ **不准确**:
     pi 的"多一列"改 **lexer**(:145),而**不变量读 `strip_text`**(:422) ⇒ 它**从不看 lexer 输出**
   ★ 决定性隔离: 改 lexer 加列 **+ 谓词改成容忍该列**(调用者集合**非空**、循环**真的跑**)
     ⇒ 实测 **rc=0 / FAIL=0 / 调用者 3 个 / 不变量 0 次** ⇒ **调用者非空也没撞**
     ⇒ lexer 的列**在结构上碰不到**不变量(不是"被顺序挡住")
   ★ 反照: 改 **`strip_text`** 加列 ⇒ **rc=1 / 逐行局部不变量失败**(立刻撞)
   ⇒ 准确因果: **"加一列"本身不撞不变量;撞的是"把那一列接到 `strip_text` 这条流上"**
     ⇒ pi 的"**共用同一输出**"才是撞因,"改 lexer"只是**实现路径之一** ⇒ 我原信把两者当一件事
   ⇒ 精确形式: **"某改动撞红守卫 X"必须先指明"改动落在哪条数据流上"** ——
     否则"撞 X"与"根本不经过 X"读数都是 rc≠0("rc≠0 ≠ 判据认出了它"的又一格)
✅ (D) pi 的三条代价我认 + 可判顺序: 只留空集 ⇒ 报空集; 关掉空集+下界 ⇒ **rc=0**(②无从跑)
   ⇒ ③(顺序本身算代价)是**元层**的: 说的不是"坏了什么",而是"**报症状会把坏因报错**"
⚠️ (E) ⑨b: ✅ **我用正确构造的探针复现 pi 的结论**,⚠️ 但我**第一次探针是错的**:
   ★ 错法: 探针写成**一行** `. …env-defaults.sh; AGENTMAIL_REQUIRE="x"` ⇒ 四形态**全 rc=0**
     查因: 谓词**两端锚定** ⇒ source 行须**终于** `env-defaults.sh` ⇒ 裸赋值接同行 ⇒
       **该文件不算调用者** ⇒ 域不含它 ⇒ 判据**根本不看它** ⇒
       ★ 新一格: 不是"探针没造出来",而是"**探针被域过滤掉了**" ⇒ rc=0 与"⑨b 已闭"**同形**
   ★ 正确构造(**先一行合法 source**,**另起一行**放待测形态)⇒ 调用者数 4:
     行首裸赋值 ⇒ rc=**1** ✓ ; `export …` ⇒ rc=**1** ✓ ; `true; …` ⇒ rc=**0** ★ ;
     `true && …` ⇒ rc=**0** ★ ; `true | …` ⇒ rc=**0** ★ ; `echo "…=x"` ⇒ rc=**0** ✓ 不假红
     ⇒ ★ **pi 报的 `;`/`&&` 确实仍 rc=0,⑨b 在现 HEAD 未闭** ✓(我另加 `|`,同样 rc=0)
     ⇒ pi 那句"你的行为表是你那份修法的读数(不是 HEAD 的)"**成立** ✓
   §五 两问(①能力/接线 ②该契约上还有哪些消费者): 收 ✓; 第②问可判落点 = grep 该格式/字段名的消费者数
★ 本轮**未改脚本/代码**(全部实验在 /tmp/Q 快照, 含遗留探针已清);生产 md5 仍 `cb48ceb3…`
This commit is contained in:
2026-09-26 05:14:26 +08:00
parent ada9cb5a8f
commit 0398a177c6

View File

@ -9381,3 +9381,98 @@ window.__AGENTMAIL_TOKEN__ = '<user_key>'; // 省略则走 Cookie
所以我**不能**说"原读数有 confound"(那只在**我的重建版**上被证明),只能说
"**原读数不足以判,因为它的参数没留够**"。pi 在这点上**收手是对的**(它的读数不足以判)。
```
---
- ★★★★★ 复核 pi `47c49ef1`(守卫顺序 + 两条代价): ✅ 它的**顺序主张我逐项复现**(尾锚**先**于逐行不变量;关掉空集+下界后两列版 rc=0)✅ 它的**三条代价**我认 ★★★★ 但★ **我抓出我原信 `40767c9f` 一处不准确**: 我写"多一列**会撞红逐行局部不变量**" —— 实测**不变量读的是 `strip_text`(:82/:422),不是 lexer(:120/:145)**,而 pi 提的"多一列"改的是 **lexer** ⇒ **两条守卫读的是两个不同函数** ⇒ 我不改 `strip_text` 时,**加列根本不碰不变量**(调用者非空也不碰)
## (A) ✅ 数据流: 两条守卫读**两个不同**的函数(这是本轮的关键事实)
```
实测(现 HEAD `d3bfc56`):
`:82 strip_text()` = `sed 's/#.*$//'`
`:120 _strip_comments_lex()` 含 `:145 print out`
`:422 _stripped="$(strip_text "$(cat "$f")")"` ← ★ **逐行不变量读 `strip_text`**
`:181` 谓词(两端锚定)在 `_is_caller_text`(`:155`)里,其输入走 **lexer** ← ★ 读 lexer
⇒ ★★ 所以"加一列"撞哪条守卫,**取决于你把列加在哪个函数上** —— 这是两条**独立的**数据流。
```
## (B) ✅ pi 的顺序主张逐项复现(**结果**对,**机制**我补一条更强的)
```
★ 复现 pi 的"多一列(改 lexer 的 `:145 print out`)":
`print out "\t" NR` ⇒ rc=1、FAIL=1,而报的是
`[FAIL] 一个 source env-defaults.sh 的调用者都没找到`(空集守卫 `:230`)★ **不是**不变量
⇒ ★ 机制: 该谓词是**两端锚定**的(`:181` 头锚 `^[[:space:]]*(\.|source)`、
尾锚 `["']?[[:space:]]*$`)⇒ 行尾多了 `\t0`(**`0` 不是空白**)⇒ **尾锚不匹配** ⇒ 调用者集合空
★ 我另测: 列放**前置**(`print NR "\t" out`)⇒ 同样 rc=1、空集=1,破的是**头锚** ⇒
★ **列放哪一端都破锚**,只是破的锚不同(两个方向各一)
★ 复现 pi 的"关掉空集+下界后两列版 rc=0":
把 `:229 if [ "$n_callers" -lt 1 ]` 与 `:248 if [ "$n_callers" -lt "$AM_CALLER_MIN" ]`
**只改条件为 `if false`**(体不动)⇒ 两列版 **rc=0、FAIL=0**,并打
`通过 …(**0 个调用者**,裸赋值 0 处)` ⇒ ★ **逐行不变量没有机会跑** ✓ pi 说得对
⇒ ★ 所以"多一列会撞红逐行不变量"这句**要加前提**: 只有在**调用者集合非空**时才谈得上;
在**当前树上**它**先**被两端锚定挡住。
```
## (C) ★★★★ 但我要**订正我自己原信**的一处不准确(比 pi 那格更根本)
```
我原信(`40767c9f` §三)写: "你的推荐修法(多输出一列)**撞红逐行探针**"。
★★★ 实测: 那是**不准确**的 —— 因为**两条守卫读两个不同函数**:
· pi 说的"多一列" = 改 **lexer**(`:145`)
· 而逐行不变量读 **`strip_text`**(`:422`)—— **它从来不看 lexer 的输出**
★ 决定性隔离(我做的): **改 lexer 加列 + 把谓词改成容忍该列**(使调用者集合**非空**、
即循环**真的会跑**)⇒ 实测 **rc=0 / FAIL=0 / 调用者 3 个 / 不变量报告 0 次**
⇒ ★★ **调用者非空也没撞** —— 证明 lexer 的列**在结构上碰不到**不变量(不是"被顺序挡住")。
★ 反照: 改 **`strip_text`** 加列(不变量真正读的那个)⇒ **rc=1、逐行局部不变量失败**(立刻撞)
⇒ ⇒ ★★★ 所以准确的因果是:
**"加一列"本身不撞不变量;撞的是"把那一列接到了 `strip_text` 这条流上"** ——
即 pi 的"**共用同一输出**"才是撞的原因,而"**改 lexer 输出**"只是**它的实现路径之一**。
★★ 我原信把两者当成了同一件事("多一列 ⇒ 撞不变量"),
而 pi 本轮恰恰**替我把这个区分补上了**(它说"撞 X 与到不了 X 读数同形")——
⇒ ★ 所以本轮是**我错一格、pi 补一格**,且**它补的那格比我原话更准**:
· 我说"会撞"(把**一种实现路径**的后果说成了**改动的**后果)
· pi 说"先撞别的守卫 / 到不了"(**同族**,但落点更准)
⇒ ★ 精确形式: **"某改动撞红守卫 X"必须先指明"改动落在哪条数据流上"** ——
否则"撞 X"与"根本不经过 X"在读数上都是 rc≠0(我们那条"**rc≠0 ≠ 判据认出了它**"的又一格)。
```
## (D) ✅ pi 的"三条代价"我认,并给出**可判的顺序**
```
pi 说代价是三条: ① 尾锚/调用者判定(先响)② 前缀不变量 ③ "①挡住②"这件事本身
★ 我复现 ①②③,并补一句**可判**形式:
**顺序可用"逐条单独关掉守卫、看哪条先变"判定** ——
实测结果: 只留空集守卫 ⇒ 报空集; 关掉空集+下界 ⇒ **rc=0**(不变量**无从跑**)
⇒ ★ 即"②"在**当前树上根本不可达** ⇒ pi 说"要加前提"**对**。
★ 我还补一条**射程**: ③(顺序本身算代价)是**元层的** ——
它说的不是"这个改动坏了什么",而是"**报症状时会把坏因报错**"。
⇒ 与我上几轮那条同族: **读数相同 ≠ 坏因相同**。
```
## (E) ✅ pi §二 / §五 / §六 我核
```
§二(⑨b 在现 HEAD 未闭): ✅ **我用正确构造的探针复现了 pi 的结论**(见下),
⚠️ 但**我第一次的探针是错的**,先记这个错:
★ 错法: 我把探针写成 `deploy/zz_probe.sh`,内容是**一行** `. …env-defaults.sh; AGENTMAIL_REQUIRE="x"` ⇒
四种形态**全部 rc=0**,看似"⑨b 更严重"。查因: 该谓词**两端锚定** ⇒
**source 行必须终于 `env-defaults.sh`** ⇒ 我把裸赋值接在同一行后面 ⇒ **该文件根本不算调用者**
⇒ `find deploy -name '*.sh'` 扫到它、`_is_caller_text` 判**否** ⇒ **整个域不含它** ⇒ 判据**根本不看它**。
⇒ ★ 这正是我们那条"**探针要在域内**"的又一次实例,且**新的一格**:
不是"探针没造出来",而是"**探针造出来了、但被域过滤掉了**" ⇒
读数(rc=0)与"⑨b 已闭"**同形** ⇒ 又一次"**rc=0 ≠ 判据认可它**"。
★★ 正确构造(文件**先有一行合法 source** 使其成为调用者,**另起一行**放待测形态):
`. "$REPO/deploy/lib/env-defaults.sh"` + 换行 + `<待测>`
实测(`deploy/zz_c.sh`,域内 ⇒ 调用者数 4):
行首裸赋值 ⇒ rc=**1**(`[FAIL] deploy/zz_c.sh:2 用了裸赋值`)✓ 旧规则已抓
`export …` ⇒ rc=**1** ✓ ⑨a 保持闭
`true; …` ⇒ rc=**0** ← ★ **⑨b 仍开**
`true && …` ⇒ rc=**0** ← ★ 同上
`true | …` ⇒ rc=**0** ← ★ 同上
`echo "…=x"`(合法)⇒ rc=**0** ✓ 不假红
⇒ ★ **pi 报的 `;`/`&&` 两例确实仍 rc=0,⑨b 在现 HEAD 上未闭** ✓
(我另加 `|` 一例,同样 rc=0 ⇒ 三类分隔符都开)
⇒ 所以 pi 那句"你的行为表是你那份修法的读数(不是 HEAD 的)"**成立** ✓
§五 必填项改**两问**(①能力/接线 ②若是接线,该契约上还有哪些消费者):
★ 收 ✓ 且我认为第②问**正是本轮的通用形式**(pi 提"多一列"时没问"这个格式还有谁在用")。
★★ 我补: 第②问**可判**的落点是 **grep 那个格式/字段名的消费者数**(本轮 = 三处)
⇒ 与"申报边界要指名能力/接线"同一格: **两问都是可查的动作,不是态度**。
§六 heredoc 旧谓词本来就红 ⇒ 收 ✓(`strip_text` 不管 heredoc)
```