4.2 不变量断言：守恒、不可达、单调

// snippet: core/src/ashdeck/combat.ts 的 invariantsHold（四条声明的落地）
export function invariantsHold(spec: Spec, s: Snapshot): boolean {
  return (
    s.cardCount === spec.cards.reduce((a, c) => a + c.count, 0) &&
    s.damageConserved === true &&
    s.energy >= 0 &&
    s.energy <= spec.params.energyMax &&
    s.block >= 0
  );
}

// file: core/test/gd_mech_04_invariants.test.ts
// tier: P
// verify: node --test 'core/test/gd_mech_04_invariants.test.ts'
//
// 4.2 三类不变量：守恒 / 不可达 / 单调。每一类都配一个**负例断言为 false**，
// 否则「不变量成立」只是一句没有反面的空话。
//
// 手法：状态机是纯函数，故 runSpec(spec, seq.slice(0, k)) 得到的就是回放第 k 步
// 的状态——于是可以在**每一步**上查不变量，而不是只看终态。

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 { digestSnap } from "../src/ashdeck/digest.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 DECK = SPEC.cards.reduce((a, c) => a + c.count, 0);

/** 逐步轨迹：第 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;
}

/** 单调不增判据。 */
function nonIncreasing(xs: number[]): boolean {
  for (let i = 1; i < xs.length; i += 1) if (xs[i] > xs[i - 1]) return false;
  return true;
}

/** 单调不减判据。 */
function nonDecreasing(xs: number[]): boolean {
  for (let i = 1; i < xs.length; i += 1) if (xs[i] < xs[i - 1]) return false;
  return true;
}

const TRACE = trace(SPEC, SPEC.strategy);
const LAST = TRACE[TRACE.length - 1];

test("守恒①：牌数恒为 12、伤害恒等于已扣敌方血量，逐步成立", () => {
  assert.equal(DECK, 12);
  assert.equal(TRACE.length, 26);
  for (const s of TRACE) {
    assert.equal(s.cardCount, DECK);
    assert.equal(s.damageConserved, true);
    assert.equal(s.dealt, SPEC.params.enemyHp - s.enemyHp);
  }
  assert.equal(LAST.won, true);
});

test("守恒②：逐步满足 invariantsHold（能量与格挡不越界）", () => {
  for (const s of TRACE) assert.equal(invariantsHold(SPEC, s), true);
});

test("负例：守恒被破坏时 invariantsHold 必须为 false", () => {
  assert.equal(invariantsHold(SPEC, { ...LAST, cardCount: DECK - 1 }), false);
  assert.equal(invariantsHold(SPEC, { ...LAST, damageConserved: false }), false);
  assert.equal(invariantsHold(SPEC, { ...LAST, energy: SPEC.params.energyMax + 1 }), false);
  assert.equal(invariantsHold(SPEC, { ...LAST, energy: -1 }), false);
  assert.equal(invariantsHold(SPEC, { ...LAST, block: -1 }), false);
});

test("不可达①：非法动作 p99 执行后状态与不执行逐字相同", () => {
  const noop = runSpec(SPEC, ["p99"]);
  const base = runSpec(SPEC, []);
  assert.equal(digestSnap(noop), digestSnap(base));
  assert.equal(noop.played, 0);
  assert.equal(noop.enemyHp, SPEC.params.enemyHp);
});

test("不可达②：欠费动作被 continue 跳过，状态完全不变", () => {
  const before = runSpec(SPEC, ["p1", "p1"]); // 能量 3 -> 1 -> 0
  assert.equal(before.energy, 0);
  assert.equal(before.hand[1], "guard"); // guard 费用 1 > 能量 0
  const after = runSpec(SPEC, ["p1", "p1", "p1"]);
  assert.equal(digestSnap(after), digestSnap(before));
  assert.equal(after.played, before.played);
});

test("不可达③：规格自带的策略里有 13 个空转步（4 个欠费 + 9 个终局后）", () => {
  const noop: number[] = [];
  for (let k = 1; k <= SPEC.strategy.length; k += 1) {
    if (digestSnap(TRACE[k]) === digestSnap(TRACE[k - 1])) noop.push(k);
  }
  assert.equal(SPEC.strategy.length, 25);
  assert.equal(noop.length, 13);
  assert.deepEqual(noop, [4, 9, 13, 14, 17, 18, 19, 20, 21, 22, 23, 24, 25]);
  assert.equal(TRACE[4].energy, 0);
  assert.equal(TRACE[4].hand[0], "guard"); // 费用 1 > 能量 0
  assert.equal(TRACE[9].hand[0], "strike"); // 费用 1 > 能量 0
  assert.equal(TRACE[13].energy, 1);
  assert.equal(TRACE[13].hand[0], "heavy"); // 费用 2 > 能量 1
  assert.equal(TRACE[16].won, true); // 第 16 步取胜，其后 9 步被 over 短路
  for (let k = 17; k <= 25; k += 1) assert.equal(TRACE[k].over, true);
});

test("负例：可负担的动作必须真的改变状态（否则「不可达」判据自身失效）", () => {
  const before = runSpec(SPEC, ["p1", "p1"]);
  const after = runSpec(SPEC, ["p1", "p1", "p0"]); // jab 费用 0，永远可负担
  assert.notEqual(digestSnap(after), digestSnap(before));
  assert.equal(after.played, before.played + 1);
});

test("单调①：enemyHp 与 playerHp 逐步不增，turn 与 played 逐步不减", () => {
  assert.equal(nonIncreasing(TRACE.map((s) => s.enemyHp)), true);
  assert.equal(nonIncreasing(TRACE.map((s) => s.playerHp)), true);
  assert.equal(nonDecreasing(TRACE.map((s) => s.turn)), true);
  assert.equal(nonDecreasing(TRACE.map((s) => s.played)), true);
  assert.equal(TRACE[0].enemyHp, 50);
  assert.equal(LAST.enemyHp, 0);
});

test("负例：单调判据必须能判 false", () => {
  assert.equal(nonIncreasing([50, 45, 51]), false);
  assert.equal(nonIncreasing([50, 50, 49]), true);
  assert.equal(nonDecreasing([1, 2, 1]), false);
  const broken = TRACE.map((s) => s.enemyHp);
  broken[1] = broken[0] + 1; // 人为造一次回弹
  assert.equal(nonIncreasing(broken), false);
});

test("三类不变量合起来：基线终态同时满足守恒、无越界、单调三面", () => {
  assert.equal(invariantsHold(SPEC, LAST), true);
  assert.equal(nonIncreasing(TRACE.map((s) => s.enemyHp)), true);
  assert.equal(LAST.over, true);
  assert.equal(LAST.turn, 4);
  assert.equal(LAST.played, 9);
});

✔ 守恒①：牌数恒为 12、伤害恒等于已扣敌方血量，逐步成立 (0.514542ms)
✔ 守恒②：逐步满足 invariantsHold（能量与格挡不越界） (0.096125ms)
✔ 负例：守恒被破坏时 invariantsHold 必须为 false (0.073583ms)
✔ 不可达①：非法动作 p99 执行后状态与不执行逐字相同 (0.102458ms)
✔ 不可达②：欠费动作被 continue 跳过，状态完全不变 (0.076291ms)
✔ 不可达③：规格自带的策略里有 13 个空转步（4 个欠费 + 9 个终局后） (0.430958ms)
✔ 负例：可负担的动作必须真的改变状态（否则「不可达」判据自身失效） (0.080417ms)
✔ 单调①：enemyHp 与 playerHp 逐步不增，turn 与 played 逐步不减 (0.094333ms)
✔ 负例：单调判据必须能判 false (0.079541ms)
✔ 三类不变量合起来：基线终态同时满足守恒、无越界、单调三面 (0.110708ms)
ℹ tests 10
ℹ suites 0
ℹ pass 10
ℹ fail 0
ℹ cancelled 0
ℹ skipped 0
ℹ todo 0
ℹ duration_ms 200.77125