311 lines
37 KiB
Markdown
311 lines
37 KiB
Markdown
# A1 扫雷棋盘生成 设计推演
|
||
|
||
> 状态：concluded（除文末开放问题） · 本文只装"为什么"——`design/gdd/a1-board-generation.md` 只收本文的结论。
|
||
> 修订时新增问题节，不删旧节（历史即依据）。
|
||
> 来源：本文吸收原 lean 版（v1.1-lean）全部推导、论证、裁决记录与验收设施详表；公式结论与表达式在 design 件，推导与论证在此。
|
||
|
||
## 问题：可推理率该怎么度量（F1 的口径是怎么钉死的）？
|
||
|
||
### 广度分析
|
||
|
||
- 候选 A：字面窄读"确定性推导格数"（仅数字推导入分子）——收益是口径最严；代价是任意好图都远低于常规门槛，度量与立法本意脱节，被裁掉。
|
||
- 候选 B：免赌确定揭示格数（初始展开 ∪ 连锁揭示 ∪ 推导开据三通道全计入分子，初始展开格同时计入分母）——与 P1 承诺语句"从初始安全区出发，逻辑可推导的挖掘占比不低于门槛"对齐，定为现行口径。
|
||
- 候选 C：单判据 inferability——被"雾区无雷"常识单独撑线的度量空心风险否掉；裁定加第二判据 inferability_core（分子分母都剔除雾格），与 F2 雾占比绝对上限 0.25 合围该风险。
|
||
|
||
### 深度分析
|
||
|
||
雾格入分子有两条通道：链可达雾格经算子①（0 格级联）入分子；与 R∞ 邻接的链不可达雾格经信息源（b）雾元知识入分子；恒无 R 邻格的雾格计入终局残余。雾格挖掘是零雷险行为（玩家可见知识），故计入"免赌"口径；其 AP 全价代价不在此度量、由 F3 单独承载——这是"风险轴与成本轴必须分开"的直接理由：雾板可推理率高而预算负担仍在，恰为两轴不可互相折算的例证。雾格入分子通道与挖掘相邻性（A3 限 8 向相邻）口径对齐，公式本身不变。
|
||
|
||
求解器初始可见态取 0 格 flood 闭包内芯而非保守可达域全体——"外扩 1 格"环非自动展开的必然产物，计入会高估玩家信息。由此派生度量保真对偶义务：既有"A2 实际展开域 ⊆ A1 排除域"之外，新增"A1 求解器初始态 ⊆ A2 实际初始展开域"（登记 A2 GDD）；若 A2 定稿展开更小，A1 回退口径 = 出生 3×3 最小态。
|
||
|
||
次序无关性是度量不变式：两算子对 R 单调 ⇒ 最小不动点唯一、与开据次序无关——实现可任意定序而度量不变，兼防一类实现方差 bug；最小不动点可经单调 worklist 传播实现，不强制全板重扫描。每图指标输出携带 metric_version（当前 1）防推理器实现漂移静默改定义（联动 F4 基线）；未来改 R∞/信息源域则 version=2 + 向量重制，仅增判据与指标集不动 R∞ 定义时 version 不跳变。
|
||
|
||
clearable 与 inferability 分两闸的理由：inferability 门槛不蕴含可清图——终局对赌残余（拉低可推理率）与矿壳包围的不可达安全格（使 cleared 永不可达）是正交缺陷（1 个不可达格在 126 安全格的板上仅拉低 0.008、0.95 门槛照过，而该板功能性残废）；故清图可达性是合法性谓词（违规 = 该次尝试判废重试，非"接受最优"候选），与质量度量分属两闸（验收算子见 F5）。
|
||
|
||
### 综合判断
|
||
|
||
现行口径 = 免赌占比双判据 + 合法性闸分立 + 信息源穷尽枚举冻结 + metric_version 防漂移。改 R∞ 定义、信息源域或规则域 = GDD 修订，非调参。
|
||
|
||
### F1 完整验算例（design 件只留摘要）
|
||
|
||
12×12 图（144 格），mine_density=0.15 → N = round(0.15×135) = 20（设环内移除 0，\|M\|=20）、S=124；雾 2 区共 9 格。R₀=21，全图 0 级联闭包 58（含 5 个链可达雾格）；数字推导开据 51 + 雾元知识开据 4（链不可达雾格）+ 推导触发级联 8 = 63 → R∞=121；残余 3 格 = 一处终局非确定对 + 1 孤立残余格。inferability = 121/124 ≈ 0.976 ≥ target 0.95；inferability_core = (121−9)/(124−9) = 112/115 ≈ 0.974 ≥ 0.95 → 两项判据达标，attempts_used=1。
|
||
|
||
## 问题：参数域与可行性谓词怎么定（F2/F2b/F2c 的边界从哪来）？
|
||
|
||
### 广度分析
|
||
|
||
- 雾占比上界候选：纯 f≤8d 推导界（必要上界，边计数）——不足：堵不住"极雾行以雾元知识撑满可推理率"的度量空心；故叠加 0.25 绝对上限（MVP 量级护栏，非推导界）。
|
||
- 成本闸候选：运行期墙钟时间逃生——被否：耗时依赖输出即破同种子同图（文本级契约），确定性死线必须加载期可判定，故取 attempts×W×H ≤ C 的静态谓词形式，C = 16384 为 provisional 量级护栏，正式值归 OQ2 ADR。
|
||
- 联合校验候选：给 inferability_target × 雾/密度参数加第三条静态跨字段校验——被裁决拒绝（见下裁决表）。
|
||
|
||
### 深度分析
|
||
|
||
必要上界推导（边计数）：每雾格 ≥1 条到非雾雷的邻接边 ⇒ 邻接边数 ≥ \|F\|；每雷 ≤ 8 邻 ⇒ \|F\| ≤ 8\|M\| ⇒ f ≤ 8d。必要 ≠ 充分：连通性缺口（雷膨胀皮肤碎裂，A4 EC2）不由本式判定，由静默降级 + F4 兜底。极端行为：d=0.5 时 8d=4，f<1 成为绑定约束；d→0 时几乎任何正 f 均被拒（小雾量在稀雷图结构性不可布，属正确拒绝）；f > 0.25 恒拒（与 d 无关）；attempts×W×H > 16384 恒拒。
|
||
|
||
F2b sound 性论证：N = round(d×(W×H−9)) 先定数、先布后删只减不增 ⇒ \|M\| ≤ N ⇒ \|S\| = W×H − \|M\| ≥ W×H − round(d×(W×H−9))——round 取整钉死后恒成立（其他取整为非法实现）；计数可行 ≠ 连通可行——clearable 生成期闸不可互替。F2b 为 Schema 校验行 delta：min_safe_count 原仅产物侧不变式（Rule 8），参数侧联合不可行域（小图×高密×高下限）经 F2b 于加载期拦截。
|
||
|
||
布雷数下限 round(d×(W×H−9)) ≥ 1 的动机：零雷板 = 初始展开即 cleared 的 A3 EC5 钓鱼活体 + 标中旗经济恒空 + F4 全断言隐形穿越。
|
||
|
||
与 Schema 校验的关系：F2 是 Tuning Knobs 跨字段谓词的规范化合取形，二者等价——Schema 校验行采本规范形消除分歧；(count=0, f>0) 角点已入 AC-2 违例集。
|
||
|
||
### 综合判断
|
||
|
||
三谓词加载期可判定、违规即致命；0.25 / 16384 / 布雷数下限与 F4 严格零阈值同属结构冻结（调整走 GDD 修订非调参）。
|
||
|
||
### 联合可行域裁决（不加第三条跨字段校验——裁决记录）
|
||
|
||
| # | 裁决要点 |
|
||
|---|---|
|
||
| 1 | 无可判定静态界——inferability 由 0 格拓扑、雾形、出生位置主导，聚合参数不决定它，任何 sound 加载期联合谓词要么空洞要么误杀 |
|
||
| 2 | 架构既定——暴露机制就是"运行期接受最优不死锁 + 强告警埋点 + 调参期批量断言"，第三闸重复且更弱 |
|
||
| 3 | 补偿保证（与 F4 绑定生效）——F4 红线 + 降级率埋点使联合不可行域在首次批量生成时必然现形 |
|
||
| 4 | 裁决边界——拒绝的是 inferability 可行性静态联合谓词（无可判定静态界）；雾占比绝对上限 0.25（度量语义护栏）与 F2c 成本谓词（确定性成本死线）均有可判定形式且不声称预测 inferability，不在该裁决覆盖内 |
|
||
| 5 | 回写义务（advisory 非校验）——target、fog_target_ratio、mine_density 同向调高时降级率结构性上行，属参数域边界而非实现缺陷 |
|
||
|
||
### F2/F2b/F2c 验算表
|
||
|
||
| 输入 | 判定 | 依据 |
|
||
|---|---|---|
|
||
| (d=0.15, f*=0.12, count=2) | ✓ 放行 | 域内 |
|
||
| (d=0.06, f*=0.50) | ✗ 致命 | 0.50 > 8d = 0.48 |
|
||
| (count=3, f*=0) | ✗ 致命 | 一致性腿（count ≥ 1 ⇒ f > 0） |
|
||
| (count=0, f*=0) | ✓ | level 1 无雾行标准形 |
|
||
| (count=0, f*=0.05) | ✗ 致命 | count=0 ⇒ f=0 腿（角点） |
|
||
| (d=0.15, f*=0.85, count=32) | ✗ 致命 | 0.85 > 0.25 雾占比绝对上限——极雾行加载期判死 |
|
||
| F2b：10×10、d=0.10、min_safe=50 | ✓ | 100 − round(0.10×91) = 91 ≥ 50 |
|
||
| F2c：10×10×16 = 1600；12×12×16 = 2304 | ✓ | ≤ 16384 |
|
||
| F2c：64×64×32 = 131072 | ✗ 致命 | 该组合换图相位同步卡顿秒级至百秒级 |
|
||
|
||
## 问题：雾的成本怎么记（F3 的口径为什么是这样）？
|
||
|
||
### 广度分析
|
||
|
||
- 分母候选 A：雾内部分母 \|U\|/\|F\|——被裁：不单列输出，可由指标集（实际雾占比 + Chain₀/U 重算）按需还原，不作对账输入。
|
||
- 分母候选 B：付费格分母 \|U\| ÷ max(1, \|S ∖ Chain₀\|)——定为 B1 条款 5 对账精确口径（雾在最小清图 AP 负担中的权重）。
|
||
|
||
### 深度分析
|
||
|
||
分母 = \|S ∖ Chain₀\| = 最小清图付费挖掘格数（初始展开与连锁免费、其余每格 dig_ap_cost——A3 价目只读引用），分母下限 1 防全连锁退化板除零。链可达性取决于未开 0 格隐藏拓扑，玩家决策时点不可求值——本式是生成期事后度量；A4"玩家侧按全价做预算"的保守启发式不与本式冲突，两口径服务不同主体。聚合义务（A4 ⑤ 公式化）：逐板计算入指标集；调参期按行批量聚合出核算报告供 C3 修正行参数；无运行期强制——A1 只拥有量的计算与输出，不拥有"够不够"的判（归 A1/A3 契约与 C3）。
|
||
|
||
边界形态的观测意义：U=F（雾区全部链不可达）→ 雾板退化为纯 AP 税——A4 反向护栏与 B4 定价约束的观测对象；U=∅（雾全链免开）→ 雾零成本——B4"糖果区"病理在此指标上直接现形。验算例：F1 例板 F=9、链可达雾 5 → U=4；dig_ap_cost=1 → Δbudget_fog = 4 AP；付费格 = 124 − 58 = 66 → fog_burden_ratio ≈ 0.061。
|
||
|
||
### 综合判断
|
||
|
||
Δbudget_fog 与 fog_burden_ratio 随图输出、生成期算账、调参期批量核对；运行期不强制，账对不上改的是难度参数行。
|
||
|
||
## 问题：调参期红线怎么守（F4 的阈值与样本量怎么定的）？
|
||
|
||
### 广度分析
|
||
|
||
- 红线阈值候选：小容差（如允许 1% 失败）——被否：A1 反向护栏已定"跌破门槛 = 阻塞缺陷"，任何一例失败即触发参数修正会话，迫使决策显式化；裁定严格零（用户定稿）。
|
||
- 雾出现下限候选：1.0——被否：EC2 连通性降级是合法运气事件；裁定 0.95（收紧为达成区占比后，同时容纳完全降级与部分达成两类合法运气事件）。
|
||
|
||
### 深度分析
|
||
|
||
阈值裁定理由（五条）：
|
||
|
||
| # | 理由 |
|
||
|---|---|
|
||
| ① | 红线严格零（用户定稿）：任何一例失败即触发参数修正会话，迫使决策显式化；运行期"接受最优/最不坏"是安全网，批量红线是调参期纪律 |
|
||
| ② | N=256：95% 下限的稳定通过要求真实出现率 ≥ 0.98（3σ 余量 ≈ 99.97%） |
|
||
| ③ | 雾出现下限 0.95 而非 1.0：5% 容差容纳自然方差；系统性病理（level 2 小图低密关雾成片失败）呈现 ~0% 出现率，与 0.95 相距悬殊，检出无歧义 |
|
||
| ④ | 断言 B′ 零成本反向杠杆：门控 bug（如 level 1 出雾）一例即现形 |
|
||
| ⑤ | 成本：行数 × 256 板 × ≤32 attempts 的生成+求解模拟，离线分钟级（成立域 = worklist 级求解实现 ∧ 大面积行稀少；naive 全板扫描实现 + 数行 48×64 板即小时级——分片续跑义务见 OQ2） |
|
||
|
||
σ 基址打包论证：σ(L,D) = 10^9 + 2^20·L + 2^12·D——位打包使行区间 [σ, σ+255] 两两不交、远离运行期取号域；朴素 1000·L+D 打包在 D≥1000 时精确碰撞〔(1,1001) ≡ (2,1)〕且同 L 相邻深度行批量区间 255/256 种子重叠。登记种子按失效协议全部重搜——夹具 σ 为登记时值。derive_at 纯函数、不推运行期计数器；σ 基址清单入版本库，批量跨迭代可复现。target行 期望由表值推导，不写死。
|
||
|
||
### 综合判断
|
||
|
||
断言 A/A″/A′/B/B′/E + 报告 C + 诊断 D 现行口径冻结；严格零阈值与 0.85/0.25/16384 同属结构冻结。验算行：行 (2,0)（fog unlock 关）N=256 → 两项判据达标 256/256 → A 通过；达成区数 = count 的板 251/256 = 0.980 ≥ 0.95 → B 通过；重试率 3.1% → 诊断记录。行 (3,2)：达成区数 = count 的板 220/256 = 0.859 < 0.95 → B 失败 → 修正行参数（区域数/尺寸/密度侧保证，禁放宽 A4 Rule 3）。极端行为：target 1.0 的行在断言 A 下大概率开火（合法、预期信号）；断言 B′ 失败即实现缺陷而非参数问题。
|
||
|
||
## 问题：生成-验证循环与验收算子怎么取舍（F5 为什么是三分支）？
|
||
|
||
### 广度分析
|
||
|
||
- 候选 A：一次性生成不重试——被否：雾布完才测可推理率，单次失败即废图过于浪费，且没有参数问题的暴露通道。
|
||
- 候选 B：全局 argmax（跑满 attempts 取最高分）——被否：达标即出（最早达标尝试 k*）是重试语义的自然形式化，argmax 徒增耗时无品质收益。
|
||
- 候选 C：attempts 用尽直接报错/卡死——被否：玩家永不卡死是硬承诺；裁定降级链 = 接受最优（k**，tie 取最早、零额外取数）+ 强告警 → 零合法时接受最不坏（k***，确定性劣度字典序）+ 最高级告警 + 非法产物标记（均为用户定稿）。
|
||
|
||
### 深度分析
|
||
|
||
合法性闸（clearable/min_safe）在质量评分之前的理由：不可清图产物若进入"接受最优"候选，质量分会掩盖功能残废——1 个不可达安全格只拉低 inferability 0.008，板却已功能性残废。三分支共用同一 board_gen 流实例（Rule 3/6），k*/k**/k*** 与 B_out 同为流取数的确定函数——回放语义闭合；scope 事件边界操作定义 = 生成函数完整返回（重试不产生新取号），D3 快照切点天然落在边界外（D2"消费侧遵守"条款的 A1 具体化）。生成期表值单次读取（行参数在生成开始时快照，生成期内不重读——防热重载撕裂 attempt 语义，A4 EC8 同族）。"接受最不坏"分支的确定性劣度 = (不可达安全格数, min_safe 缺口, 序号) 字典序——零额外取数、可重放。B1 编排不得把 attempt 边界当 scope 事件（登记 B1 接线注记）。
|
||
|
||
EC5 玩家侧语义登记：非法产物标记属遥测域、玩家不可见——零合法板在玩家侧表现为"看似可玩"的功能残废（不可清图板挖光可达域后 cleared 永不触发、清图奖励永不可得、无任何提示），GDD 如实登记该体验债；玩家侧诚实呈现（提示/补偿/回退）登记为 B1/D1 域承接项；运行期熔断候选（同 (L,D) 连续降级/非法 ≥ 阈值 → 确定性回退该行已知好种子重生成）不破"玩家永不卡死"与回放契约，方案裁决归实现期 ADR（OQ2 关联）。
|
||
|
||
### 综合判断
|
||
|
||
三分支 + 合法性闸前置 + 强告警分级是现行契约；降级率是参数问题的暴露通道，批量红线由 F4 断言 A′ 守。
|
||
|
||
## 问题：体验锚点为什么这样定（P1/P4/P3 的生成侧承诺）？
|
||
|
||
### 广度分析
|
||
|
||
- P1 生成端对偶：D2 保"同种子同结果"的可复现，A1 保"同参数同品质"的可推理——可推理率生成参数 = 出题人义务；玩家输给的是自己选的赌（雾区/终局盲猜），不是不可解的局。
|
||
- P4 难度物质：雷密、尺寸、雾占比随 (level_index, node_depth) 爬升——难度由 BoardGenTable 行参数直接雕刻，非文案。
|
||
- P3 空间面：生成期布置约束兑现"雾区无雷、雾贴雷簇"（A4 Rule 3 结构推论）——洞口前的权衡是真实的信息权衡而非装饰。
|
||
|
||
### 深度分析
|
||
|
||
情绪目标："这局能算"的底气——A1 不制造情绪，它制造情绪的前提条件（玩家永不看见生成器，但每轮都在体验它的产物）。参考感受：扫雷原版"每局必有解"的玩家信念（原版实际不保证——本作把这份信念变成生成端契约）；Into the Breach 每张谜题可解的设计诚实。反向护栏（裁剪判据）："纯猜局"是 P1 的死亡体验——生成端若让玩家频繁坠入不可推理局面，结算端再华丽也救不回掌控感；红线 = 生成参数使可推理率跌破门槛即为阻塞缺陷（验收红线，非调参建议）。
|
||
|
||
### 综合判断
|
||
|
||
三条支柱承诺全部以生成端可判定契约承载（双判据、行参数雕刻、布置约束），无一依赖文案或呈现。
|
||
|
||
## 问题：核心结构决策的取舍记录（布雷、取整、密度形态、推理域）？
|
||
|
||
### 广度分析
|
||
|
||
- 布雷语义候选：落选重投（落进环内就重取位置）vs 先布后删（落完再删、只减不增、不重投、无迭代）——裁定先布后删：确定性终止、无迭代、漂移量可观测（|M| ≤ N 入指标集）。
|
||
- 雷数取整候选：round 钉死（其他取整为非法实现——F2b sound 性论证依赖此钉死）。
|
||
- 雷量参数形态候选：定数 vs 密度浮点——裁定密度浮点（尺寸解耦；f≤8d 分母对齐），用户拍板四结构决策之一。
|
||
- 推理域候选：开放信息源 vs 封闭枚举 single_subset——裁定冻结（用户拍板）；改域 = 改可推理率定义 = GDD 修订非调参。
|
||
|
||
### 深度分析
|
||
|
||
四结构决策（生成-验证循环 / 接受最优 + 零合法接受最不坏 / 推理域 single_subset 冻结 / 密度浮点）与 F4 严格零红线为用户拍板——全部经 2026-09-09 full /design-review 8 条 blocking 修订后放行（日志：design/gdd/reviews/a1-board-generation-review-log.md）。雾边双向净效应建模（A4④）：可推理率测量在布雾完成后进行，雾边寂静减项与雾锚增项（雾元知识开据格）同时内生于测量，禁单向补偿；AC-8 板ⅲ 为此的度量侧证据。
|
||
|
||
### 综合判断
|
||
|
||
结构决策全部冻结；任何一项的改动都走 GDD 修订。
|
||
|
||
## 问题：措辞与口径防漂移登记（为什么是 registry 级）？
|
||
|
||
### 广度分析
|
||
|
||
inferability 与 P(安全) 是两个系统的两个量，混用即口径漂移。
|
||
|
||
### 深度分析
|
||
|
||
inferability 是盘面级免赌占比（生成侧）；P(安全) 是单格认知概率（决策侧、经济口径）——免赌集内 P(安全) 恒 = 1（含雾格），风险讨论收缩到残余集（其安全格占比 ≤ 1 − inferability）。inferability 是 P(安全) 的生成端结构性上界代理之占比形式，不是 P(安全) 本身。B1 条款 3 对账输入 = actuals 分布 p10（F4 报告 C）而非 target 参数——防"拿参数当事实"。
|
||
|
||
### 综合判断
|
||
|
||
措辞登记为 registry 级事实（board_gen_table.inferability_vs_p_safe），B1 消费回执已登记。
|
||
|
||
## 问题：验收设施怎么设计（测试口径各条款的理由）？
|
||
|
||
### 广度分析
|
||
|
||
- 冒烟载体：A1 是生成函数系统，`godot --headless --script`（承 D2 冒烟框架；脚本 extends SceneTree、autoload 显式实例化）。
|
||
- 度量独立入口（qa-lead 裁决、分解面声明）：推理器（R∞/inferability/metric_version）、F3 度量（Chain₀/U/Δbudget_fog/fog_burden_ratio）、合法性谓词（legality/clearable）以独立纯函数入口暴露——生成函数内嵌调用与独立入口同一实现，独立入口不引入新逻辑、仅暴露 F1/F3/F5 已定义的函数；独立入口的行为断言即内嵌调用的行为（次序无关性、防作弊等白盒性质测试以此为载体）；若实现期 ADR 裁决推理器不可独立调用，AC-7/8/9/12 的单元腿须降级重议——登记缺口 G1，门禁评审列为 A1 实现契约条款。
|
||
- 测试种子取号：经 `derive_at("board_gen", σ)` 纯函数（D2 R2 预览语义的测试侧合法用途，不推运行期计数器）；测试脚本以该种子构造流实例属测试通道合法动作（AC-18 扫描豁免域）；运行期 replay 语义（open_stream 全真路径）另测（AC-5）。
|
||
|
||
### 深度分析
|
||
|
||
夹具策略：默认根 = MVP 参考行 L1·D0 / L2·D0（干净检出）——参考行是 GDD 定稿的 schema 自洽性证明行，期望全部由表读值推导、对 C3 调参免疫；行为变体经 `--data-root` 夹具根注入（禁拷入 data/tables/）；黄金图板与病态板经 Board class_name 直引程序构造（不经生成器、不经 load()/preload()——A4 AC-5 先例）。登记种子（σ 值）依赖管线确定性：一经验证恒成立，实现或定义变更致失效 → 按失效协议重搜并登记（与黄金向量失效协议同源）。
|
||
|
||
黄金图回归向量协议：五类手工核验小板，每板 = 显式坐标规格（尺寸/雷集/雾区格集/出生 3×3，程序构造不经生成器）+ 登记常数（(\|R∞\|,\|S\|) 整数对、含雾板另登记 (\|R∞∖F\|, \|S∖F\|) core 整数对——由既有坐标规格派生、向量不重制、关键格 R∞ 成员表、clearable、Chain₀/U 格集、Δbudget_fog、fog_burden_ratio 比对形 = 整数对 (\|U\|, max(1,\|S∖Chain₀\|))、metric_version=1——整数对比对，禁浮点容差）+ 逐格手工推导记录（每格声明信息源 ∈ {数字约束（a)、雾元知识（b)、0 格级联①}，入版本库随向量文件——手工常数的登记依据）；比对内容 = 度量独立入口 + 合法性谓词输出与登记常数逐位相等；失效处置协议 = 失配先按冻结定义复核手工推导，推导无误即实现缺陷（修实现）；solver_rules/合法信息源域/metric_version 变更 = 换 solver_rules 即失效，走 GDD 修订 + 向量重制（推理域冻结的非调参性质的行为侧兑现）。
|
||
|
||
期望值推导纪律：行为类 AC 期望 = ConfigDB/表读值推导（inferability_target/min_safe_count/max_gen_attempts/fog_region_count/unlock_level/dig_ap_cost/σ 公式全读值），不写死玩法数值；唯一例外 = 黄金图向量手工常数（依据 = 手工推导记录）；参考行 GDD 自注期望（\|S\|≈91 等）为说明非断言，任何 AC 不采用。致命类独立进程协议：承 D2 AC-2b / A4 AC-4b——runner manifest 逐条登记"夹具根 → 期望退出码"（AC-3 三行，均 ≠0）；单进程内只做测试通道收集断言；每用例先 `reset_diagnostics()`（承 D2 冒烟协议；warning/error 断言一律经诊断收集器）。
|
||
|
||
MVP 参考行自洽性验证：F2/F2b/F2c 全过（10×10×16 = 1600、12×12×16 = 2304 ≤ 16384）；期望 \|S\| ≈ 91、R₀ ≈ 12–20 → inferability 期望 ≥ 0.95（L1 无雾 ⇒ core ≡ inferability；L2 雾 ~14/144 格、core 判据轻度收窄仍期望 ≥ 0.92——两项判据同时达标；attempts_used ≈ 1，F4 全绿理论位形）。参考行明细：L1·D0（10×10 / d=0.10 / target=0.95 / single_subset / min_safe=50 / attempts=16 / fog 0·0——level 1 候选池空标准形 / biome={"dungeon"} 占位）；L2·D0（12×12 / d=0.12 / target=0.92 / 同冻结 / min_safe=60 / attempts=16 / fog 1 区·0.10〔≤8×0.12 ✓——F4 断言 B 首个真实考验行〕 / biome 同占位）。全部 provisional——仅 schema 自洽性证明，曲线数值归 C3 调参所有权。
|
||
|
||
### 综合判断
|
||
|
||
测试口径全部条款现行有效；缺口 G1/G2/G4 如实登记（见开放问题区）。
|
||
|
||
## 附录 A：夹具规格（qa-lead 交付，逐根原样保留）
|
||
|
||
| 夹具根 | 内容（F2/F2b 均过，除违例根外） | 用途 |
|
||
|---|---|---|
|
||
| `a1_fog_domain` | f>8d 违例行 | AC-2/3（致命） |
|
||
| `a1_min_safe` | 10×10/d=0.10/min_safe=92（F2b 违例：100−round(0.10×91)=91<92） | AC-2/3（致命） |
|
||
| `a1_biome_empty` | board_biome=∅ 行（A4⑮） | AC-2/3（致命） |
|
||
| `a1_pool_empty` | VariationTable 测试行（biome_tag=[ice]、unlock_level=1，承 A4 variation_biome_tag 同型）+ BoardGenTable 两行：(1,0) board_biome={dungeon}（pool=∅）/ (1,1) board_biome={dungeon,ice}（pool 非空） | AC-13 |
|
||
| `a1_high_target@k` | 12×12/d=0.12/target=1.0/fog=1 区 0.05/min_safe=60/attempts=k∈{1,2} | AC-5/11 |
|
||
| `a1_ec5@k` | 10×10/d=0.45/min_safe=1/target=0.85（域内合法档）/fog=0/attempts=k∈{1,2,8,16}；σ* 登记（@1 零合法验证种子） | AC-12 |
|
||
| `a1_two_regions` | 10×10/d=0.15/count=2/f=0.12/target=0.85/attempts=16；σ 登记 | AC-14 |
|
||
| `a1_ec2_press` | f := 8×d 计算值恰界行（程序内动态赋值）；σ*′ 登记（shortfall>0 搜索种子） | AC-15 |
|
||
|
||
黄金板设计要求：ⅰ 纯数字推理板（无雾；须含仅 single_subset 规则可开的推导格）· ⅱ 链密集板（0 格级联闭包主导）· ⅲ 含雾板（须同时含：链可达雾、链不可达雾、邻接出生 3×3 的雾区、寂静减项证据格、雾锚增项证据格【雾元知识开据格】）· ⅳ 终局对赌残余板（inferability 严格 ∈ (0,1) 的非确定残余）· ⅴ 不可达安全格板（clearable 违例形态）。
|
||
|
||
只读观测量清单：产物格状态（雷布/数字/0 格/雾区标记/出生区）+ 八项指标（实际 inferability【含 metric_version】/ inferability_core / 实际雾占比【= \|F\| ÷ (W×H)】/ 实际雷数与实际 \|S\| / fog_burden_ratio / Δbudget_fog / attempts_used / 降级标记【含非法产物标记与 shortfall】）。
|
||
|
||
## 附录 B：out-of-scope deferral 表（以对侧登记为生效条件）
|
||
|
||
| 编号 | deferral 内容 | 对侧 / 生效条件 |
|
||
|---|---|---|
|
||
| O1 | B1 接线——attempt 边界非 scope 事件的编排侧断言、指标对账消费（actuals p10 非 target）归 B1 GDD AC（A1 侧生成半边已由 AC-5 计数器断言覆盖） | B1 GDD 登记 |
|
||
| O2 | F4 全量——N=256/行 × 全行的断言 A 严格零/B 0.95/报告 C/诊断 D = 调参期离线批量工具域（工具本体为 A1 交付物，登记 OQ；σ 基址清单入版本库），冒烟仅载缩样（AC-10） | 批量工具交付登记 |
|
||
| O3 | A2 集成——双包含回验（A2 实际展开域 ⊆ A1 排除域；A1 求解器初始态 ⊆ A2 实际初始展开域）登记 A2 GDD（A1 半边由 AC-6(a) 测试 BFS 对照承载） | A2 GDD 登记 |
|
||
| O4 | fault-injection 缺载体——EC7 生成中热重载（同步单调用无重入点，构造性成立且注入不可）、EC10 内部异常 fatal、EC4 tie-取最早（需精确同分尝试）deferral 至实现期注入设施或可选种子搜索会话 | 实现期登记 |
|
||
| O5 | 性能预算——生成耗时/换图相位无定稿预算值（Tuning Knobs OQ），perf-profile 期承载 | perf-profile 期 |
|
||
| O6 | 呈现域——EC6 雾区视觉合并归 D1、biome 色板换皮归 D1/art-bible | D1/art-bible 登记 |
|
||
| O7 | C3 全行审计——曲线导出工具全行矩阵 diff 为 C3 期交付物（D2 OQ5 既有排期） | C3 期 |
|
||
|
||
## 附录 C：Knob 调参方向表（调过高/调过低的后果记录）
|
||
|
||
| Knob | 参考（L1/L2） | 调过高 | 调过低 |
|
||
|---|---|---|---|
|
||
| board_width/height [8,64] | 10×10 / 12×12 | 决策带宽膨胀、清图时长拉长 | 逼近 min_safe 联合域（F2b 拦截线） |
|
||
| mine_density (0,0.5] | 0.10 / 0.12 | 推理窗收窄、可推理率难达标（F4 断言 A 开火）；f≤8d 分母水涨船高 | 图面空旷、奖励密度稀 |
|
||
| inferability_target [0.85,1] | 0.95 / 0.92 | 重试率升、深行联合不可行（F2 裁决：无静态闸，F4 必然现形） | 域下限 0.85 = P1 绝对锚（加载期拒绝 + F4 断言 A″ 兜底）——"纯猜局混入"红线自此有可判定载体；0.85 本身的调整走 GDD 修订非调参 |
|
||
| min_safe_count | 50 / 60 | 小图联合无解（F2b 加载期拦截） | 退化板钓鱼复现（A3 EC5 对冲失效） |
|
||
| max_gen_attempts [1,32] | 16 | 生成耗时随 attempts×面积×传播深度超线性涨（对边长最高三次方量级；F2c 成本闸拦病理组合，OQ2） | 降级率上行、质量下行 |
|
||
| fog_region_count | 0 / 1 | 信息剥夺过重（P1 落差）；F4 断言 B 压力 | 低于雾出现率下限 → A4"解锁新变异"推进感哑火（A4⑭ 义务） |
|
||
| fog_target_ratio [0,1) | 0 / 0.10 | 逼近 8d 上界 → 布置降级率升（连通性，EC12 两闸注记）；> 0.25 加载期拒绝（F2 雾占比绝对上限腿） | 雾存在感弱、P4 推进感哑火 |
|
||
| board_biome | {"dungeon"} | ——（词表 owner 未定稿，暂只校验非空） | —— |
|
||
|
||
## 附录 D：覆盖矩阵（qa-lead 交付，验收评审用）
|
||
|
||
| 类别 | 映射 |
|
||
|---|---|
|
||
| Core Rules | 1→AC-4/5/6(c)/16（布雷语义）· 2→AC-8/9/10(a)/16（两项判据）· 3→AC-10/11/12 · 4→AC-6(a)(b)/7（芯/环口径）· 5→AC-6(c)(d)(e)/13/14/15 · 6→AC-4/5/14/18 · 7→AC-16 · 8→AC-2/3/6(f) · 9→AC-1/2/3/13 · 10→AC-6(g)/17/18/19 |
|
||
| Formulas | F1→AC-8/9/7/16 · F2/F2b/F2c→AC-2/3（角点/上限/布雷数下限/成本上限）· F3→AC-16 · F4→AC-10（全量 O2；断言 A″/E 属 O2）· F5→AC-10(e)/11/12/7 |
|
||
| EC | EC1→13 · EC2→15 · EC3→7/8 · EC4→11（tie O4）· EC5→12（玩家侧语义登记 B1/D1 域）· EC6→14（合并 O6）· EC7→O4 · EC8→10(c) · EC9→2/11 · EC10→O4 · EC11(F2b)→2/3 · EC12→2/15 · EC13→2 · EC14→5 |
|
||
| A4 义务 | ①→13 · ②→6(c) · ③→6(a)(b) · ④→8/16（core 常数补强）· ⑤→16 · ⑥→13 · ⑦→15 · ⑧→4/14 · ⑨→7/8 · ⑩→2/3 · ⑪→14（间接承载——共置+确定性，无取号耦合差分）· ⑫→6(d)(e)/2 · ⑬→15（部分覆盖：面积判据实现同样通过 a1_ec2_press——取号耦合差分夹具登记待核销）· ⑭→10/O2（断言 B 收紧达成区占比）· ⑮→2/3 |
|
||
| 规模 | 19 条 AC + A4×15 全落位 + 黄金五板；⑪ 差分承载与 ⑬ 差分夹具登记待核销（间接承载已注明），5 处标注问题的修正明细见评审日志 |
|
||
|
||
## 开放问题
|
||
|
||
| # | 悬案 | owner | 时机 |
|
||
|---|---|---|---|
|
||
| OQ1 | F4 全量批量工具的 owner 排期：调参期红线工具（断言 A/A′/B/B′ + 报告 C + 诊断 D，N=256/行）——与 D2 OQ5 曲线导出工具同批登记排期（排期倒挂：A1 定稿→首行数值回填→即需抽查；临时载体 = 冒烟缩样 AC-6/10，统计意义有限，如实登记） | A1 交付物 / C3 消费 | C3 调参期前 |
|
||
| OQ2 | 生成性能预算与异步化选项：① 预算数值定稿——F2c 谓词形式已冻结（max_gen_attempts × W×H ≤ C），C = 16384 为 provisional 占位，ADR 裁定正式 C 与 headless debug 基准（如"64×64 单次求解 ≤ X ms"）；② 解空间圈定——死路二：attempts 并行化（毁 board_gen 流序即毁回放）、分帧/协程化（跨帧在飞 open_stream 实例与 D2 快照切点契约冲突，需 D3 扩容修订）；活路四：同步 + 加载幕（B1 换图相位）、主线程分帧 + D3 快照扩容修订、WorkerThread + D2 EC13 单线程假设接口漂移修订（join 先于任何快照切出）、B1 预测性预生成（线性图结构的死时间生成——scope 计数器推进时点须入回放语义）；③ 实现姿态约束——最小不动点可经单调 worklist 传播实现（次序无关性不强制全板重扫描——F1 注记⑤），禁全对全子集比较（ADR 验收底线）；④ F4 全量工具须支持分片续跑（"分钟级"成立域 = worklist 实现 ∧ 大面积行稀少，见 F4 阈值⑤） | 实现期 ADR / perf-profile | Technical Setup |
|
||
| OQ3 | 度量独立入口分解面确认：推理器/F3 度量/合法性谓词三入口暴露（AC-7/8/9/12 单元腿前提——缺口 G1）；若 ADR 裁决不暴露，四条 AC 单元腿降级重议 | 实现期 ADR | 实现期 |
|
||
| OQ4 | biome 词表 owner 定稿：board_biome 值域现只校验非空（EC13）；词表定稿后补域校验 + 参考行占位值替换（接口漂移） | B4/C1 域 + AD 门禁 | 垂直切片前 |
|
||
| OQ5 | 黄金向量手工推导第二人复核：五板逐格推导记录入版本库后安排复核（qa-lead 缺口登记——推导错误即假失配） | A1 定稿评审 | A1 /design-review |
|
||
| OQ6 | 精英/Boss 第三轴落点重审：节点形态定稿后强制重审——① Dmax 行约定是否覆盖全部 Boss 场景 ② 精英节点是否需第三键维 / elite_、boss_ 字段激活（分支地图同深度并存精英与普通节点时）；激活即走 D2 Rule 4 改键通道 + 本表 schema 修订（接口漂移迁移，退路已登记） | C1/C3 GDD | C1 定稿时 |
|
||
|
||
待拍板（格式迁移中发现的原文与 registry 落差，不自行裁决）：
|
||
|
||
| # | 事项 | 来源 |
|
||
|---|---|---|
|
||
| T1 | registry `a2_initial_expansion.degenerate_gap` 与 systems-index 登记了一条 A1 修订义务（反例 B / N=1 行 100% 退化）：F5 legality 增 `R₀ ≠ S`（违例 = 尝试作废重试）+ F4 断言 A′ 族严格零覆盖 + Rule 4 排除域基准措辞钉死"以最终产物板计"。该义务未落入原 A1 GDD 任何版本（F5 legality 现形 = clearable ∧ \|S\| ≥ min_safe ∧ 结构不变式，R₀=S 的退化板 clearable 照过）。本次为格式迁移、禁止加规则，原样保留现形并在此登记——待用户/修订流程裁决是否按既有登记走接口漂移修订 | design/registry/entities.yaml + systems-index 门禁记录 |
|
||
|
||
缺口登记（原测试口径/AC 内的 G 编号，保留）：
|
||
|
||
| # | 缺口 | 处置 |
|
||
|---|---|---|
|
||
| G1 | 度量独立入口分解面未确认（AC-7/8/9/12 单元腿前提） | 归 OQ3，实现期 ADR 裁决；不暴露则四条 AC 单元腿降级重议 |
|
||
| G2 | AC-9 输入表示序不变量不覆盖完全开据定序自由度的穷尽验证 | out-of-scope，如实登记 |
|
||
| G4 | a1_ec2_press 的 shortfall>0 搜索种子 σ*′ 若搜索无解，后备语义未定 | 登记待核销，协议同 AC-12 种子搜索 |
|
||
|
||
## 去向映射（零丢失审计证据）
|
||
|
||
| 原章节 | 落点 |
|
||
|---|---|
|
||
| 头部（状态/版本/支柱/层级/一句话/复核注记） | design 头部（状态/版本/一句话/推演件指针）；承载支柱与层级定位并入 design 设计目的定位段；复核注记（CD/AD 未经咨询、生产前人工复核）→ 本文件开放问题区关联 OQ5 + 版本历史沿革 |
|
||
| 速览表 | 定位/拥有/不拥有 → design 系统范围；上游输入/下游输出 → design 依赖与输出；硬约束 → design 生成管线与随机流纪律规则 3 + schema 节；缺位后果 → design 设计目的 |
|
||
| 体验锚点（P1/P4/P3 表、情绪目标、参考感受、反向护栏） | 结论（五条体验承诺）→ design 设计目的；全部论证 → 本文件「体验锚点」问题节 |
|
||
| 全局流程（五阶段字符画 + 出口分发表） | design 核心循环（原样保留） |
|
||
| 核心规则 1–10（人话 + 举证） | 人话 → design 各领域章节编号规则（规则 1/6 → 生成管线与随机流纪律；规则 4 → 出生区与可达域；规则 5/9 → 变异布置与雾形边界；规则 2/3 → 可推理率度量与验收算子；规则 7 → 清图预算增量；规则 8/10 → 参数表节）；举证中的计算指向保留为 F 编号引用 |
|
||
| 枚举（八项指标集 / solver_rules） | solver_rules → design 可推理率节规则 5 + schema 表；八项指标集 → design 依赖与输出产物行 + AC-16（逐字段枚举保留）；指标逐项语义 → 本附录 A 只读观测量清单 + design 各 F 节 |
|
||
| F1 结论 + 推导 + 口径注记 + Variables + 验算 | 结论与公式本体 + 口径钉死表 + 变量表 + 值域边界 → design F1 小节；推导论证（两通道、初始态、次序无关、clearable 两闸理由、完整验算例）→ 本文件「可推理率」问题节 |
|
||
| F2/F2b/F2c 结论 + 推导 + 联合可行域裁决 + 验算 | 结论与判定式 → design 加载期校验表；边计数推导、sound 性论证、禁墙钟论证、裁决表、验算表、极端行为 → 本文件「参数域」问题节 |
|
||
| F3 结论 + 推导 + 口径注记 + Variables + 验算 | 结论与公式 + 口径表 + 变量表 → design 清图预算增量节；分母取舍、两主体口径、边界形态观测意义、验算例 → 本文件「雾的成本」问题节 |
|
||
| F4 结论 + 推导 + 阈值理由 + Variables + 验算 | 结论与断言表 → design F4 小节；阈值裁定理由五条、σ 打包论证、成本论证、验算行 → 本文件「调参期红线」问题节 |
|
||
| F5 结论 + 推导 + 注记 | 结论与公式 + 注记表 + EC4/EC5 出口表 → design F5 小节；三分支取舍、合法性闸前置理由、EC5 玩家侧语义论证 → 本文件「验收算子」问题节 |
|
||
| 显式排除声明（归属表） | design 系统范围不负责清单（括注归属）+ 依赖与输出 |
|
||
| 措辞登记 | design 依赖与输出节前注记；论证 → 本文件「措辞」问题节 |
|
||
| MVP 参考行 | design 调参表默认列（provisional 标注）；参考行明细与自洽性验证 → 本文件「验收设施」问题节 |
|
||
| 状态（五阶段失败语义 + 不变式） | design 生成管线节失败语义表 + 不变式行 |
|
||
| 边界情况 EC1–EC14 | EC1/EC2/EC3/EC6/EC12/EC13 → design 变异布置节与出生区节编号规则；EC4/EC5/EC8/EC9 → design F5 小节出口表；EC7/EC10/EC14 → design 生成管线节规则；EC11 → design 加载期校验节规则；判据与依据编号全部保留 |
|
||
| 依赖（上游/下游/A4×15 落位表/跨系统对账登记/双向一致性核对） | design 依赖与输出（原样保留） |
|
||
| 呈现与 UI 契约（5 行数据面义务） | design 依赖与输出末表（原样保留） |
|
||
| Tuning Knobs（schema + 加载期校验 + 第三轴登记 + Knob 表 + 非 knob + 工具参数 + Knob 交互） | schema + 校验 + 第三轴 → design 参数表节；调参表（字段|域|默认|owner）→ design 调参表；调过高/调过低后果 → 本文件附录 C；非 knob 结构冻结清单与 Knob 交互 → design 调参表脚注 |
|
||
| 验收标准（测试口径 8 行 / 夹具规格 / out-of-scope deferral / AC-1–19 / 覆盖矩阵） | AC 19 条 GWT（编号不动、判定口径保留）→ design 验收标准；测试口径详表 + 夹具规格 + deferral 表 + 覆盖矩阵 → 本文件「验收设施」问题节 + 附录 A/B/D |
|
||
| 开放悬案 OQ1–6 | 本文件开放问题区（原编号保留） |
|
||
| 版本历史（3 行） | design 版本历史（原 3 行保留 + 追加 v2 迁移行） |
|