Browse Source

fix(ac15): 形态统计唯一化 —— 12+2+1+2=17 那个数是错的,真值 2+2+1+10=15

起因:3a 报出的形态分布「12 + 2 + 1 + 2 = 17」与批内 15 条对不上。
根因不是加法算错,是**分类不唯一**:activityChainVerdict 把命中的标签用 " + "
拼起来,于是 SA-2 / SC-2 同时是 intentional-strict 与零写入守卫,各被数两次。

改动:
- ActivityChainShape 唯一分类 + Case.ActivityShape() 按优先级取第一个命中
  (legacy-defect > intentional-strict > zero-write > equality)。
  零值取 Unclassified 而不是 equality —— 漏赋值的形态不许静默冒充「两侧应一致」。
- ActivityShapeTally:Σ 各形态条数 == len(cases) 由构造保证。
- 报告新增一行「活动域形态」(Summarize → activityShapeLine),数由程序加,不再手算。
- 单测 4 条:优先级表 / 标签互不为子串 / 判定文案恰好命中 1 个标签 / 真实注册表 Σ 闭合。
- README §18.3 自伤清单加第 6 条(只让「报出来的数字」变错的那一类),
  并补 §18.5 真实分布:15 条 = legacy-defect 2 + strict 2 + zero-write 1 + equality 10。
- spdump README 坑清单加第 6 条:SELECT var = expr 不是赋值。

真值口径(-v 输出,注册表现算):
  活动域形态分布:15 条 = legacy-defect 2 + intentional-strict 2 + zero-write 1 + equality 10

读法:15 条里只有 10 条在验「两侧一致」,另 5 条证明的是别的事 ——
所以「15 条全绿」不能翻译成「15 条都证明了实现正确」。
Q 3 giờ trước cách đây
mục cha
commit
9e2b0b7dc5

+ 7 - 1
cmd/spdump/README.md

@@ -34,7 +34,7 @@ AC-15 阶段 2 用三次实测证明:**「照抄 SP」是不可行的策略**
 
 ⇒ **证据强度:SQL 语句 > 参数签名 > COMMENT > 表名/函数名。**
 
-## 读 SP 正文的五个坑(每一条都真的让我们算错过)
+## 读 SP 正文的六个坑(每一条都真的让我们算错过)
 
 | # | 坑 | 错在哪 | 怎么防 |
 |---|---|---|---|
@@ -43,6 +43,12 @@ AC-15 阶段 2 用三次实测证明:**「照抄 SP」是不可行的策略**
 | 3 | **`SELECT … INTO` 无行可赋时不改变量** | 变量停在 `DEFAULT 0`,于是"账户行不存在"与"余额真的是 0"在 SP 里**不可区分** —— `custom_refund` 会因此静默 `success=0`,调用方看到的是"成功"。 | 断言"账户行是否存在"要单独读,不能从变量值反推。 |
 | 4 | **`OR` 的短路能把 NULL 变成"走另一条分支"** | `IF(ISNULL(_balance) OR _balance<=0)`:NULL 时**左边**就成立、右边根本不求值 ⇒ 结果是"拒绝",不是"NULL 参与比较"。 | 遇到 `ISNULL(x) OR y` 一定要想"x 为 NULL 时 y 会不会被求值"。 |
 | 5 | **同名逻辑出现在多处,执行位置可能不同** | `tmp_user_activity` 那段在 `cleared_balance` 里跑在**写流水之前**、在 `custom_refund` 里跑在**写流水之后**。SQL 逐字相同,事务内顺序不同 ⇒ 失败终态组合不同。 | 同一段 SQL 出现在 N 处就测 N 次;并且各自记下"它在流水之前还是之后"(见 C2-10)。 |
+| 6 | **`SELECT var = expr` 不是赋值,`SET var = expr` 才是** | `user_discount_refund_user_activity` 里写的是 `IF (inputAmount>logDiscountAmountUsed) THEN SELECT inputAmount = logDiscountAmountUsed; END IF;` —— 这句**只产生一个布尔结果列**(比较的返回值),`inputAmount` **一位都不变**。所以"退超就压到流水额"这道钳制**从未生效**:type=3 代金券把入参覆盖成面额后,SP 直接按**面额**退,池行 `discount_amount_used` 退成**负数**。照"这是钳制"去读,期望值会算错一整笔面额。 | 见到 `SELECT` 后面跟 `x = …` 的形式,**先判断 `=` 左边是不是变量名**:是 ⇒ 这是 T-SQL 赋值语法被硬搬过来的死代码,不产生任何效果。`spdump` 的全文里对 `SELECT .* = ` 单独 grep 一遍,逐处确认。锁在 `TestActivityChainVerdictIsSingleLabel` 的同批 case DRA-2(`Case.LegacyRefundTakesFullFace`)。 |
+
+第 6 条特别值得记一笔:它**没有任何症状**。SP 不报错、不警告、`SELECT` 还正常返回一个结果集,
+调用方拿到的 `success=1` 也完全正常 —— 唯一的痕迹是"池行用量变成了负数",
+而这只有在写期望值时才看得出来。所以读 SP 不能只读"控制流像什么",
+还要读"**每一行到底改了哪个变量**"。
 
 ## 安全约束(硬性,不是约定)
 

+ 20 - 1
internal/academic/dualrun/stage2/README.md

@@ -1225,7 +1225,7 @@ $sql = "SELECT SUM(t1.discount_amount-t1.discount_amount_used) as amount FROM ..
 反过来,三处**故意选严**的:`toleranceCents = 0`(容差永不放宽)、
 哨兵的 `nonzeroSamples > 0`(非空自检)、`未分类断言数 == 0`。
 
-### 18.3 「自伤清单」:新基建最容易把旧判据悄悄弄坏的六种方式
+### 18.3 「自伤清单」:新基建最容易把旧判据悄悄弄坏的七种方式
 
 每一条都**不产生明显症状**,只让断言变松或整块消失。加基建/加 case 时逐条对照。
 
@@ -1237,6 +1237,25 @@ $sql = "SELECT SUM(t1.discount_amount-t1.discount_amount_used) as amount FROM ..
 | 3 | **两个不同口径的列共用一个读函数** | 比对变松,永不报错(例:`float(10,2)` 与 `float(10,3)` 同表) | 读函数按口径**分成两个**(`readRound2` / `readRound3`),并加单测断言两者字符串不同 |
 | 4 | **行集"靠键配对"** | 少写一条 + 多写一条落在同一键上 ⇒ 互相抵消,绿 | 多重集(`map[tuple]int`),并把自增 id / 时间戳排除在 tuple 外 |
 | 5 | **闸门只数"非 Skipped 断言"** | 基建断言(残留 / 基线)永远为真 ⇒ 闸恒过 | 断言分 `Business` / `Infrastructure`,闸门只认业务;`Kind == 0` 算非业务(§18.2) |
+| **6** | **一个对象挂多个分类标签,然后"按标签计数"**(批 3a 真踩:`activityChainVerdict` 把命中的标签用 `" + "` 拼起来 ⇒ SA-2 / SC-2 同时是 `intentional-strict` 与 `零写入守卫`) | **两份数各自都对,加起来不等于总数** —— 报出 `12 + 2 + 1 + 2 = 17`,而该批只有 **15** 条。没有任何一条断言会红,因为它错在**记账**不在**判定** | 分类**唯一化**:`Case.ActivityShape()` 按优先级(`legacy-defect > strict > 零写入 > equality`)取**第一个**命中;统计只走 `ActivityShapeTally`,并把 `Σ N == len(cases)` 与"判定文案恰好命中 1 个标签"写成单测 |
+
+第 6 条和前面五条不是一类:前面五条让**断言变松**,第 6 条只让**报出来的数字变错**。
+但后果一样严重 —— 数字是决策输入。`12 + 2 + 1 + 2 = 17` 那份统计如果被拿去写周报,
+"12 条在验一致性"会让人以为覆盖够了,而真实值是 **10**(见 §18.5)。
+**能自己加一遍的账,一定要让程序加。**
+
+### 18.5 活动域形态的真实分布(`ActivityShapeTally` 输出)
+
+```
+活动域形态分布:15 条 = legacy-defect 2 + intentional-strict 2 + zero-write 1 + equality 10
+```
+
+读法:**15 条里只有 10 条在验"两侧一致"**,另有 4 条(`legacy-defect` 2 + `strict` 2)
+本来就是"两侧该不同"的登记,1 条是零写入守卫。所以"15 条全绿"这句
+**不能翻译成"15 条都证明了实现正确"** —— 有 5 条证明的是别的事。
+这跟 §16 的 `Skipped` 分解是同一个道理:绿的总数不等于检出力。
+
+这一行现在由报告自动打印(`Summarize` → `activityShapeLine`),**不要手算**。
 
 ### 18.4 代价必须可读:SQL 执行次数 + 耗时
 

+ 113 - 13
internal/academic/dualrun/stage2/activity_compare.go

@@ -2,7 +2,6 @@ package stage2
 
 import (
 	"fmt"
-	"strings"
 )
 
 // 本文件是活动链 7 支的比对与断言(批 3a)。
@@ -420,20 +419,121 @@ func isActivityChainOp(op Op) bool {
 	return false
 }
 
-// activityChainVerdict 生成"这批里多少条在验一致性 / 多少条在登记分歧"的登记文案。
-// 由 case 声明 `IntentionalStrict` 或 `ExpectActivityZeroWrite` 决定,不靠猜。
-func activityChainVerdict(c Case) string {
-	parts := []string{}
-	if c.IntentionalStrict {
-		parts = append(parts, "intentional-strict(legacy 静默 / target 显式拒绝)")
-	}
-	if c.ExpectActivityZeroWrite {
-		parts = append(parts, "零写入守卫(两侧都不写库)")
+// ActivityChainShape 是一条活动域 case 的**唯一**形态分类。
+//
+// # 为什么必须"唯一",不能是"命中的标签 join"
+//
+// 第一版把命中的标签用 `" + "` 拼起来,于是一条 case 可以同时是
+// 「intentional-strict」和「零写入守卫」。看着信息更全,但它让**按标签数行数**这件事失去意义:
+// 一条 case 落在两行里,两份数各自都对,加起来不等于批内条数。
+//
+// 3a 实测就踩了:报出的形态分布是 12 + 2 + 1 + 2 = 17,而该批只有 **15** 条 ——
+// SA-2 / SC-2 因为同时置了 `IntentionalStrict` 与 `ExpectActivityZeroWrite`,各被数两次。
+//
+// 唯一分类之后,`Σ 各形态条数 == 批内 case 数` 变成恒等式(`ActivityShapeTally`),
+// 不需要任何人再做一次加法校验 —— 加法校验本来就是"人会忘"的那类事。
+type ActivityChainShape int
+
+const (
+	// ActivityShapeUnclassified 是零值,**不该出现**。
+	// 按 §18.2「默认值永远选严的那一侧」:零值不做成 equality,
+	// 否则将来加一种形态忘了赋值,它会静默冒充"两侧应一致"。
+	ActivityShapeUnclassified ActivityChainShape = iota
+	// ActivityShapeLegacyDefect 两侧本就该不同(只登记实际值,不做相等判定)。
+	// **优先级最高**:它才是这条 case 存在的理由,其它标签只是顺带的守卫。
+	ActivityShapeLegacyDefect
+	// ActivityShapeIntentionalStrict legacy 静默 / target 显式拒绝。
+	ActivityShapeIntentionalStrict
+	// ActivityShapeZeroWrite 两侧都不写库(守卫类)。
+	ActivityShapeZeroWrite
+	// ActivityShapeEquality 两侧应一致(默认)。
+	ActivityShapeEquality
+)
+
+// Label 是形态的短标签:只用于统计与 grep,**互不为子串**(脚本按它计数才安全)。
+func (s ActivityChainShape) Label() string {
+	switch s {
+	case ActivityShapeLegacyDefect:
+		return "legacy-defect"
+	case ActivityShapeIntentionalStrict:
+		return "intentional-strict"
+	case ActivityShapeZeroWrite:
+		return "zero-write"
+	case ActivityShapeEquality:
+		return "equality"
+	}
+	return "unclassified"
+}
+
+// Text 是报告里的说明文案(标签 + 一句为什么)。
+func (s ActivityChainShape) Text() string {
+	switch s {
+	case ActivityShapeLegacyDefect:
+		return "legacy-defect(两侧本就该不同:旧 SP 少退 / 超退 ⇒ 只登记实际值)"
+	case ActivityShapeIntentionalStrict:
+		return "intentional-strict(legacy 静默 / target 显式拒绝)"
+	case ActivityShapeZeroWrite:
+		return "zero-write(两侧都不写库,守卫类)"
+	case ActivityShapeEquality:
+		return "equality(两侧应一致)"
+	}
+	return "unclassified(未分类 —— 这是缺陷,不该出现)"
+}
+
+// ActivityShape 返回这条 case 的**唯一**形态,按优先级取第一个命中。
+//
+// 优先级 LEGACY-DEFECT > strict > 零写入 > equality:越靠前越"这条 case 想证明什么",
+// 越靠后越"没人声明所以按默认处理"。一条 case 若既登记分歧又带守卫,
+// 它该被计成"登记分歧"——因为那是它唯一不可被别条替代的那件事。
+func (c Case) ActivityShape() ActivityChainShape {
+	switch {
+	case c.LegacyDrainsCursorAfterFirst || c.LegacyRefundTakesFullFace:
+		return ActivityShapeLegacyDefect
+	case c.IntentionalStrict:
+		return ActivityShapeIntentionalStrict
+	case c.ExpectActivityZeroWrite:
+		return ActivityShapeZeroWrite
+	default:
+		return ActivityShapeEquality
 	}
-	if len(parts) == 0 {
-		parts = append(parts, "equality(两侧应一致)")
+}
+
+// activityChainVerdict 是活动域 case 的形态登记文案(唯一形态,不并列)。
+func activityChainVerdict(c Case) string {
+	return c.ActivityShape().Text()
+}
+
+// ActivityShapeCount 是形态计数的单项(Tally 的返回元素)。
+type ActivityShapeCount struct {
+	Shape ActivityChainShape
+	N     int
+}
+
+// ActivityShapeTally 按**唯一形态**统计一批 case,并按固定顺序返回。
+//
+// 两个性质由构造保证(单测锁住):
+//
+//	① Σ N == len(cases) —— 这就是唯一分类的全部意义,3a 那次 12+2+1+2=17 的防法;
+//	② 未分类条数恒为 0    —— 非 0 = 有人加了形态却没接进 `ActivityShape()`。
+func ActivityShapeTally(cases []Case) []ActivityShapeCount {
+	order := []ActivityChainShape{
+		ActivityShapeLegacyDefect,
+		ActivityShapeIntentionalStrict,
+		ActivityShapeZeroWrite,
+		ActivityShapeEquality,
+		ActivityShapeUnclassified,
+	}
+	counts := make(map[ActivityChainShape]int, len(order))
+	for _, c := range cases {
+		counts[c.ActivityShape()]++
+	}
+	out := make([]ActivityShapeCount, 0, len(order))
+	for _, s := range order {
+		if n := counts[s]; n > 0 {
+			out = append(out, ActivityShapeCount{Shape: s, N: n})
+		}
 	}
-	return strings.Join(parts, " + ")
+	return out
 }
 
 // wantDiscountUsed 是"退回类 Op 之后池行 `discount_amount_used` 的期望值"。

+ 133 - 0
internal/academic/dualrun/stage2/activity_shape_test.go

@@ -0,0 +1,133 @@
+package stage2
+
+import (
+	"strconv"
+	"strings"
+	"testing"
+)
+
+// 本文件锁住「一条活动域 case 只能有一个形态」这件事。
+//
+// 起因是一次真实报数错误:形态分布报成 12 + 2 + 1 + 2 = 17,而该批只有 15 条 ——
+// SA-2 / SC-2 同时置了 `IntentionalStrict` 与 `ExpectActivityZeroWrite`,
+// 旧的 `activityChainVerdict` 把两个标签 `" + "` 拼起来,于是两条 case 各被数两次。
+//
+// 结论:**只要形态不是唯一的,"按形态计数"就永远需要一个加法校验,而人一定会忘。**
+
+// TestActivityShapePriority 锁住优先级:LEGACY-DEFECT > strict > 零写入 > equality。
+//
+// 每个组合都写成表,改优先级必须改这张表 —— 否则"哪条 case 被计成什么"会静默漂移。
+func TestActivityShapePriority(t *testing.T) {
+	tt := []struct {
+		name string
+		c    Case
+		want ActivityChainShape
+	}{
+		{"什么都没声明 → equality", Case{}, ActivityShapeEquality},
+		{"只 零写入", Case{ExpectActivityZeroWrite: true}, ActivityShapeZeroWrite},
+		{"只 strict", Case{IntentionalStrict: true}, ActivityShapeIntentionalStrict},
+		{"strict + 零写入 → strict 优先", Case{IntentionalStrict: true, ExpectActivityZeroWrite: true},
+			ActivityShapeIntentionalStrict},
+		{"只 游标抽干 → legacy-defect",
+			Case{LegacyDrainsCursorAfterFirst: true}, ActivityShapeLegacyDefect},
+		{"只 按面额退 → legacy-defect",
+			Case{LegacyRefundTakesFullFace: true}, ActivityShapeLegacyDefect},
+		{"游标抽干 + strict → legacy-defect 压过 strict",
+			Case{LegacyDrainsCursorAfterFirst: true, IntentionalStrict: true}, ActivityShapeLegacyDefect},
+		{"按面额退 + 零写入 → legacy-defect 压过零写入",
+			Case{LegacyRefundTakesFullFace: true, ExpectActivityZeroWrite: true}, ActivityShapeLegacyDefect},
+		{"三者全置 → 只算 legacy-defect",
+			Case{LegacyDrainsCursorAfterFirst: true, LegacyRefundTakesFullFace: true,
+				IntentionalStrict: true, ExpectActivityZeroWrite: true}, ActivityShapeLegacyDefect},
+	}
+	for _, tc := range tt {
+		if got := tc.c.ActivityShape(); got != tc.want {
+			t.Errorf("%s:期望 %s,得到 %s", tc.name, tc.want.Label(), got.Label())
+		}
+	}
+}
+
+// TestActivityShapeLabelsAreDistinct 锁住标签互不为子串。
+//
+// 报告是纯文本,统计脚本只能靠 grep 标签。若 A 的标签是 B 的子串,
+// `grep -c A` 会把 B 那些行也算进去 —— 又是一次"数出来的数对不上"。
+func TestActivityShapeLabelsAreDistinct(t *testing.T) {
+	all := []ActivityChainShape{
+		ActivityShapeLegacyDefect, ActivityShapeIntentionalStrict,
+		ActivityShapeZeroWrite, ActivityShapeEquality,
+	}
+	for i, a := range all {
+		for j, b := range all {
+			if i == j {
+				continue
+			}
+			if strings.Contains(b.Label(), a.Label()) {
+				t.Errorf("标签 %q 是 %q 的子串 —— grep 计数会串行", a.Label(), b.Label())
+			}
+		}
+	}
+}
+
+// TestActivityChainVerdictIsSingleLabel 是这次修复的**核心断言**:
+// 任意一条 case 的判定文案里,**恰好命中一个**形态标签。
+//
+// 旧实现下这条测试会在 SA-2 / SC-2 上失败(命中 2 个),而那正是报数错的根因。
+// 顺带锁住:文案里的标签必须就是 `ActivityShape()` 的结果,不允许"文案写 A、分类是 B"。
+func TestActivityChainVerdictIsSingleLabel(t *testing.T) {
+	all := []ActivityChainShape{
+		ActivityShapeLegacyDefect, ActivityShapeIntentionalStrict,
+		ActivityShapeZeroWrite, ActivityShapeEquality,
+	}
+	// 用真实注册表跑一遍:新加的 case 若同时置多个 flag,这里立刻红。
+	for _, c := range DefaultCases("") {
+		if !isActivityChainOp(c.Op) {
+			continue
+		}
+		text := activityChainVerdict(c)
+		hits, hit := 0, ActivityShapeUnclassified
+		for _, s := range all {
+			if strings.Contains(text, s.Label()) {
+				hits++
+				hit = s
+			}
+		}
+		if hits != 1 {
+			t.Errorf("case %q 的判定文案命中 %d 个形态标签(必须恰好 1 个):%s", c.Name, hits, text)
+			continue
+		}
+		if hit != c.ActivityShape() {
+			t.Errorf("case %q:文案写的是 %s,但 ActivityShape() 是 %s", c.Name, hit.Label(), c.ActivityShape().Label())
+		}
+	}
+}
+
+// TestActivityShapeTallyAddsUp 锁住恒等式 Σ N == len(cases),并且未分类恒为 0。
+//
+// 断言对象是**真实注册表**而不是编造的样例:编造样例只能证明函数会加法,
+// 证明不了"这一批 case 现在记的账是对的"。
+func TestActivityShapeTallyAddsUp(t *testing.T) {
+	act := make([]Case, 0)
+	for _, c := range DefaultCases("") {
+		if isActivityChainOp(c.Op) {
+			act = append(act, c)
+		}
+	}
+	if len(act) == 0 {
+		t.Fatal("活动域 case 为 0 条 —— 注册表接线断了,后面每个数都不可信")
+	}
+	tally := ActivityShapeTally(act)
+	sum := 0
+	parts := make([]string, 0, len(tally))
+	for _, tc := range tally {
+		if tc.Shape == ActivityShapeUnclassified {
+			t.Errorf("出现未分类形态 %d 条 —— 有人加了 flag 却没接进 ActivityShape()", tc.N)
+		}
+		sum += tc.N
+		parts = append(parts, tc.Shape.Label()+" "+strconv.Itoa(tc.N))
+	}
+	// 打出来:这是**当前注册表**的真实分布,报告里那一行就是从这来的。
+	t.Logf("活动域形态分布:%d 条 = %s", len(act), strings.Join(parts, " + "))
+	if sum != len(act) {
+		t.Errorf("形态计数之和 %d ≠ 活动域 case 数 %d —— 分类不唯一(这正是 3a 报数错的成因)", sum, len(act))
+	}
+}

+ 28 - 0
internal/academic/dualrun/stage2/run.go

@@ -1799,6 +1799,12 @@ func Summarize(w io.Writer, results []*CaseResult) bool {
 	} else {
 		fmt.Fprintf(w, "未分类断言(Kind==0):0 条\n")
 	}
+	// 活动域形态分布:**按唯一形态统计**,所以 Σ 必须等于该批条数。
+	// 这一行存在的理由就是 3a 那次人工加法算错(12+2+1+2=17,实际 15)——
+	// 报告自己给一个恒等式,比任何人再算一遍都可靠。
+	if line, ok := activityShapeLine(results); ok {
+		fmt.Fprintf(w, "活动域形态:%s\n", line)
+	}
 	for _, r := range results {
 		st := "PASS"
 		if !r.OK() {
@@ -1819,3 +1825,25 @@ func sumBusiness(results []*CaseResult) int {
 	}
 	return n
 }
+
+// activityShapeLine 生成活动域形态分布那一行;非活动域 case 为 0 条时返回 ok=false(不打印)。
+//
+// 输出形如:`15 条:legacy-defect 4 | intentional-strict 2 | zero-write 6 | equality 3`
+// **尾部再打一次总数**,让人不必自己加:两侧对不上就是记账错了,不是"少打印了一类"。
+func activityShapeLine(results []*CaseResult) (string, bool) {
+	act := make([]Case, 0, len(results))
+	for _, r := range results {
+		if isActivityChainOp(r.Case.Op) {
+			act = append(act, r.Case)
+		}
+	}
+	if len(act) == 0 {
+		return "", false
+	}
+	tally := ActivityShapeTally(act)
+	parts := make([]string, 0, len(tally))
+	for _, t := range tally {
+		parts = append(parts, fmt.Sprintf("%s %d", t.Shape.Label(), t.N))
+	}
+	return fmt.Sprintf("%d 条:%s", len(act), strings.Join(parts, " | ")), true
+}