# FlipSpec 设计说明

## 设计目标

FlipSpec 面向有限、可解释的业务策略。设计优先级依次是：语义确定、解释可复现、边界可见、跨目标可运行，最后才是搜索速度。它不把布尔规则包装成另一层黑盒。

## 数据流

```mermaid
flowchart LR
  A["FlipSpec 源文本"] --> B["Lexer：Token + Span"]
  B --> C["Parser：Policy + Expr"]
  C --> D["模型校验"]
  D --> E["三值求值 + Trace"]
  E --> F["反事实搜索"]
  E --> G["阻断条件 / Probe / 决策表"]
  F --> H["最小性证书"]
  F --> I["预算曲线 / 修复组合分析"]
  C --> J["模型画像"]
  F --> K["Markdown / JSON"]
  E --> L["文本 / Mermaid"]
```

## 三值逻辑

缺失特征或类型不可比较时产生 `Unknown`。合取中 `No` 吸收未知值，析取中 `Yes` 吸收未知值：

| A | B | A and B | A or B |
| --- | --- | --- | --- |
| true | unknown | unknown | true |
| false | unknown | false | unknown |
| unknown | unknown | unknown | unknown |

这样既不会把缺失值当成 `false`，也能在一个明确失败的合取中保持最终结果为 `false`。

## 反事实搜索

规划器对未锁定特征的声明域执行深度优先枚举：

1. 从当前环境开始；
2. 每个特征选择域中的一个候选值；
3. 到达叶节点后求值；
4. 只保留达到目标真值且至少发生一次修改的环境；
5. 按总代价、修改数、稳定文本键排序；
6. 删除被更便宜且修改集合更小的方案支配的结果；
7. 返回前 `max_results` 个方案。

规划器始终记录实际求值次数。达到 `max_evaluations` 后停止并设置 `truncated`，调用者因此可以区分“没有解”和“有限预算内没有找到解”。锁定特征只使用当前值，不进入搜索分支。

时间复杂度上界为各未锁定特征域大小的乘积，空间复杂度与特征数量和保留的修复数量相关。项目明确不声称解决大规模组合优化。

## 最小性证书

`Plan::certify(model)` 根据模型声明域重新计算搜索空间大小，并把计划中的求值次数、截断标记、最佳代价和策略匹配关系整理为 `PlanCertificate`。当证书状态为 `minimum-certified` 时，含义是：在这份规格声明的有限域内，搜索已经覆盖所有可行赋值，且没有更低代价的赋值能够翻转结果。

证书不声称现实世界中的修改一定可执行，也不替代调用者对特征域和成本模型的判断。它解决的是可复核性问题：评审者或 CI 可以检查“这个最低代价修复方案是否来自完整搜索”，而不是只相信一段自然语言解释。

## 分析层

除直接给出修复方案外，FlipSpec 还提供三类面向维护和复核的摘要：

- `Policy::budget_report` 枚举不同预算上限内的可达赋值，显示目标结果第一次出现在哪个预算；
- `Policy::profile` 汇总模型搜索空间、目标表达式复杂度、锁定特征、零成本特征和未引用特征；
- `Plan::portfolio` 对候选修复集合做组合分析，区分所有方案都必须修改的共识特征和只在部分方案中出现的替代特征。

这些 API 的共同目标是让调用者能解释“为什么是这个修复前沿”，而不只是拿到一组修改建议。

## 确定性

- 环境使用有序 `Array[Binding]`，避免不同后端的哈希遍历顺序差异；
- 解析器不依赖地区或系统时间；
- 修复方案具有完整稳定排序键；
- JSON 和 Markdown 字段顺序固定；
- CLI 示例不访问本地文件系统。

这些约束让 Wasm、Wasm GC、JavaScript 与 Native 后端能生成一致的可复核结果。

## 错误模型

解析接口返回 `Result[Policy, Diagnostic]`，不因用户输入直接终止程序。诊断包含稳定错误码、消息和一基行列号。程序化构造的模型可调用 `Policy::validate` 一次获取全部结构错误。

## 安全边界

DSL 不是脚本语言：没有循环、动态函数、系统调用或导入。字符串只作为数据参与比较。搜索严格受声明域和求值次数限制，因此接收不可信文本时的主要风险是输入体积和组合空间；宿主应同时限制输入长度与 `max_evaluations`。

## 后续维护方向

- 允许为修复声明条件可行性约束；
- 增加按特征分组的多目标代价；
- 提供增量求值以复用相邻候选环境的子表达式；
- 在不改变核心语义的前提下增加浏览器编辑器；
- 建立 DSL 版本声明与兼容迁移器。