10.2 不变量清单

step card dmg eng blk hp goal turn hand note
   0 T T T T T T T T 开局
   1 T T T T T T T T
   4 T T T T T T T T 第4步欠费空转
   8 T T T T T T T T
  16 T T T T T T T T 第16步取胜
  25 T T T T T T T T 终态

// file: core/test/gd_mech_10_checklist.test.ts
// tier: P
// verify: node --test 'core/test/gd_mech_10_checklist.test.ts'
//
// 10.2 不变量清单：把 ch1（资源与目标）/ ch3（守恒）/ ch4（状态封闭与断言）
// 散落的不变量汇总成**一张可执行清单**。每条检查是一个 (snapshot) -> boolean
// 的纯函数；清单在真实轨迹上必须全 true，且**每条都配一个故意造违反的负例**，
// 检查器必须返回 false——否则这条检查只是摆设（4.2 已说过：没有反面的断言等于没说）。

import { test } from "node:test";
import assert from "node:assert/strict";
import { readFileSync } from "node:fs";
import { fileURLToPath } from "node:url";
import { dirname, join } from "node:path";

import { runSpec, invariantsHold } from "../src/ashdeck/combat.ts";
import type { Snapshot, Spec } from "../src/ashdeck/types.ts";

const HERE = dirname(fileURLToPath(import.meta.url));
const SPEC: Spec = JSON.parse(
  readFileSync(join(HERE, "..", "..", "config", "play_spec.json"), "utf8"),
);
const P = SPEC.params;
const DECK = SPEC.cards.reduce((a, c) => a + c.count, 0);
const POOL = new Set(SPEC.cards.map((c) => c.id));

/** 清单一条：名字 + 来源节号 + 判据（整数比较，无浮点）。 */
type Check = { name: string; from: string; ok: (s: Snapshot) => boolean };

const CHECKS: Check[] = [
  { name: "cardCount==deckSize", from: "3.2", ok: (s) => s.cardCount === DECK },
  { name: "damageConserved", from: "3.2", ok: (s) => s.dealt === P.enemyHp - s.enemyHp },
  { name: "energyInRange", from: "3.2", ok: (s) => s.energy >= 0 && s.energy <= P.energyMax },
  { name: "blockNonNegative", from: "3.2", ok: (s) => s.block >= 0 },
  { name: "hpNotExceed", from: "1.2", ok: (s) => s.playerHp <= P.playerHp && s.enemyHp <= P.enemyHp },
  { name: "goalConsistency", from: "1.2", ok: (s) => !s.won || s.enemyHp <= 0 },
  { name: "turnBound", from: "1.2", ok: (s) => s.over || s.turn <= P.turnLimit },
  { name: "handClosed", from: "4.1", ok: (s) => s.hand.every((id) => POOL.has(id)) },
];

/** 逐步轨迹：第 k 项 = 处理完前 k 个命令后的状态。 */
function trace(spec: Spec, seq: string[]): Snapshot[] {
  const out: Snapshot[] = [];
  for (let k = 0; k <= seq.length; k += 1) out.push(runSpec(spec, seq.slice(0, k)));
  return out;
}
const TRACE = trace(SPEC, SPEC.strategy);

test("清单结构：8 条，来源恰好覆盖 1.2 / 3.2 / 4.1", () => {
  assert.equal(CHECKS.length, 8);
  assert.deepEqual([...new Set(CHECKS.map((c) => c.from))].sort(), ["1.2", "3.2", "4.1"]);
});

test("清单在真实轨迹（26 个状态）上逐条成立", () => {
  assert.equal(TRACE.length, 26);
  for (const c of CHECKS) {
    for (const s of TRACE) assert.equal(c.ok(s), true, `${c.name} 在真实状态上破了`);
  }
});

test("负例自证：8 条各有反例，检查器必须判 false", () => {
  const base = TRACE[TRACE.length - 1];
  const bad: Array<[string, Snapshot]> = [
    ["cardCount==deckSize", { ...base, cardCount: DECK - 1 }],
    ["damageConserved", { ...base, dealt: base.dealt + 1 }],
    ["energyInRange", { ...base, energy: P.energyMax + 1 }],
    ["blockNonNegative", { ...base, block: -1 }],
    ["hpNotExceed", { ...base, enemyHp: P.enemyHp + 1 }],
    ["goalConsistency", { ...base, won: true, enemyHp: 10 }],
    ["turnBound", { ...base, over: false, turn: P.turnLimit + 1 }],
    ["handClosed", { ...base, hand: ["heal"] }],
  ];
  assert.equal(bad.length, CHECKS.length);
  for (const [name, snap] of bad) {
    const c = CHECKS.find((x) => x.name === name);
    assert.ok(c, `清单里没有 ${name}`);
    assert.equal(c.ok(snap), false, `${name} 的反例没被抓住`);
  }
  // 恒真检查器必然漏掉全部反例——这就是「每条必须配反例」的理由
  const alwaysTrue = (_s: Snapshot) => true;
  assert.equal(bad.filter(([, s]) => alwaysTrue(s)).length, bad.length);
});

test("与 4.2 的 invariantsHold 对齐：真实轨迹全 true", () => {
  for (const s of TRACE) assert.equal(invariantsHold(SPEC, s), true);
});

✔ 清单结构：8 条，来源恰好覆盖 1.2 / 3.2 / 4.1 (0.824167ms)
✔ 清单在真实轨迹（26 个状态）上逐条成立 (0.171584ms)
✔ 负例自证：8 条各有反例，检查器必须判 false (0.15975ms)
✔ 与 4.2 的 invariantsHold 对齐：真实轨迹全 true (0.091125ms)
ℹ tests 4
ℹ suites 0
ℹ pass 4
ℹ fail 0
ℹ cancelled 0
ℹ skipped 0
ℹ todo 0
ℹ duration_ms 197.773792