# moonbit_static_analysis

[English](README.md) | **中文**

`riantr/moonbit_static_analysis` —— 一个 **三鉴（结构 / 类型 / 行为）静态分析流水线**，
面向 MoonBit。一套基础设施，两种用途：

1. **程序代码修订** —— 分析 **快速进化中的 MoonBit 语言** 写的程序（未定义名、未用绑定、
   类型不匹配、死分支、不可达代码）；
2. **静态状态修订** —— 面向多层状态机的通用机器表审计（`src/statecheck`）：**被审计的主体
   调用本模块**，把它的机器表当纯数据喂进来。

它能读 MoonBit 工具链的每一种文件后缀 —— `.mbt` / `.mbtx` / `.mbti` / `.mbt.md` /
`.mbtp` —— 而且 **绝不修改被扫描的目标**：被分析的仓库既不依赖本模块，也不会被本模块改动。

在 `moonbitlang/core`（1679 个文件）上的实测：**解析 1621 个，actionable 30 条**——其中 10 条
是本前端读不到的构造或算不出来的运算符，另外 20 条是 `MSA-015` 声明上的死存储：一个在任何
读取之前就被覆盖掉的 `let`。那是**被分析代码里的死重量**，不是阅读器的盲区，而且这 20 条每
一条都对着它指名的源码核过。0.4.38 降级的那 14 条——分析器解不出来的名字——算作 notice，
不在这 30 条里。同一棵树上 `moon check --target all` **一条**诊断也不报。

## 目录

- [特性](#特性)
- [安装](#安装)
- [快速上手](#快速上手)
- [用途一：程序代码修订](#用途一程序代码修订)
- [用途二：静态状态修订](#用途二静态状态修订)
- [API 参考](#api-参考)
- [命令行参考](#命令行参考)
- [输出怎么读](#输出怎么读)
- [覆盖范围与边界](#覆盖范围与边界)
- [文件种类](#文件种类)
- [包结构](#包结构)
- [验证](#验证)
- [发布历史](#发布历史)
- [参与开发](#参与开发)
- [许可证](#许可证)
- [参考](#参考)

## 特性

- ✅ **三鉴，一份报告** —— 结构遍历 → 类型/符号 → 抽象解释，合并之后一个缺陷就是 **一条**
  发现，它的透镜标签是所有看见它的透镜的并集。合并是无损的：合并前后的计数都保留。
- ✅ **MoonBit 的每一种文件后缀** —— `.mbt` / `.mbtx` / `.mbti` / `.mbt.md` / `.mbtp`，
  其中包括编译器**根本不审**的三种。
- ✅ **只读，不写** —— 被分析的仓库既不依赖本模块，也不会被本模块改动。本工具只在扫描时
  **读取**目标的文件。
- ✅ **跨文件符号解析** —— `--extern-iface-dir` 索引 `.mbti` 里的声明，于是从别的包用来的
  类型不会被报成未定义。
- ✅ **诚实的覆盖率** —— 前端读不完的文件被标成 `PARTIAL`，它边界之后的发现**被计数、
  但不展示**。
- ✅ **只有可能要紧的 notice 才占一行** —— 只有可能藏住发现的 notice 才逐行打印，其余按形状
  汇总成一张表。`--show-notices` 把完整列表带回来。
- ✅ **状态机审计** —— 同一套三鉴跑在纯数据的机器表上：状态即绑定、驱动槽即类型契约、
  历程即抽象执行。
- ✅ **Mermaid 图输出** —— `--mmd` / `--mmd-auto`，可选开启；被截断的图会在自己的头部
  里写明这一点。
- ✅ **文件名里带出处** —— 包、版本、**工具链**和时间戳，好让一次扫描可以和后来的扫描
  互相比较。
- ⚠️ **`--per-function`** —— 行为透镜的第二个入口。用它的数字之前，请先读
  [覆盖范围与边界](#覆盖范围与边界)。

## 安装

```bash
moon add riantr/moonbit_static_analysis@0.4.47
```

然后在 `moon.mod` 里引入：

```moonbit
import {
  "riantr/moonbit_static_analysis@0.4.47",
}
```

### 宿主要满足什么

发布出去的 wasm **不是自包含的**。它从 `moonbitlang/async` 导入了 **93 个符号**——文件 IO、
进程调用、事件循环——实例化模块时**宿主**必须把这些符号全都提供出来。`moonx` 提供的是
**你的** MoonBit 工具链自带的那个异步运行时。

所以这个产物有一条**下限**，而下限是发布出去的**字节**的属性：

| 是什么 | 在哪里 |
|---|---|
| 产物允许向宿主要的符号 | `_verify/host_requirements.txt` |
| 把产物按这份清单卡住的门 | `_verify/check_host_requirements.ps1` |
| 对**发布出去的字节**做同一件事 | `_verify/selfscan_published.ps1` |

**从 0.4.45 起，运行时来自 `moonbitlang/core/async`——你的工具链自带的那一份——而这个包
本身一个依赖都没有了。** `moon.mod` 里没有 import 块，没有版本需要和用户的工具链对齐。
这正是要点：正是「这个包钉的版本」和「用户的工具链自带的版本」之间的分歧，让 0.4.38
坏掉了。

**宿主 ABI 的模块名没变，变的是符号集合，而且变大了。** wasm 导入的模块名来自源码里的
FFI 声明，而 `moonbitlang/core/async` 仍然用 `moonbitlang/async` 这个名字声明它的宿主
extern——所以宿主提供的还是同一个模块。变的是集合：**90 → 93**。

| | 符号 |
|---|---|
| **新增** | `stdio/get_stdio_handle`、`thread_pool/get_read_console_result`、`thread_pool/make_read_console_job`、`thread_pool/make_write_console_job`、`thread_pool/run_job` |
| **消失** | `io/errno_is_read_EOF/windows`、`thread_pool/errno_is_cancelled` |

**而下限也跟着抬高了，这一条值得读两遍。** 实测：独立的 `moonbitlang/async` 0.22.5 只能覆盖
93 个里的 **89** 个——它有 `stdio/get_stdio_handle`，但四个 `thread_pool` 新增的一个都没有。
工具链自带的 `moonbitlang/core` **0.10.20+65efd5b93** 声明了 215 个 extern，93 个全覆盖。所以：

> **0.4.45 及以后需要自带 `moonbitlang/core` 0.10.20+65efd5b93（或更新）的 MoonBit 工具链**——
> 也就是 moon 0.1.20261104 或更新。还在自带独立 `moonbitlang/async` 的工具链无法实例化
> 这个产物，而只升级这个包本身改变不了这一点：导入面是发布出去的字节的属性。

错误在分析器一行都还没跑的时候就到了：

```
LinkError: WebAssembly.Instance(): Import #5 "moonbitlang/async" "thread_pool/make_write_console_job": function import requires a callable
```

**0.4.38 是按比多数人更新的宿主构建的，然后被一个用户撞出来了。** 它的 `moonbitlang/async`
被升到了 0.22.6，而 0.22.6 多声明了三个必须由宿主提供的符号——同样那三个 console job。
自带 0.22.5 的工具链提供不出它们。0.4.45 又要了那三个，外加两个新的，因为它用的运行时
就是随工具链一起发的那一个。如果你是在 0.4.38 上撞到了这个错误：先用 **0.4.37**，或者升级
你的 MoonBit 工具链，或者换到 **0.4.47**。

升级前还有一件事要知道：`moonbitlang/core/async` 目前仍被 core 团队标为 **experimental**，
所以用到它的那些包在自己的 `moon.pkg` 里明确写了出来。随工具链一起发、但还没稳定——这
两件事同时成立，这个包就是两件事都占。

## 快速上手

### 扫描另一个项目 —— 不引入依赖，也不改动它

```bash
moonx riantr/moonbit_static_analysis@latest riantr/moonbit_doubleML@latest
```

`moonx` 下载 mooncakes 为该发布版本构建好的 **预编译 wasm**，缓存后用 `moonrun` 跑起来
——不用 clone，也不用本地构建。

目标可以是注册表坐标（`author/module`，可带 `@version` 或 `@latest`），也可以是本地路径；
省略则扫描当前目录。坐标会先由 `moon fetch` 落到 `.repos/`，然后再遍历。

### 当作库来用

```moonbit
// 用途一：修订一段 MoonBit（当前子集）程序
let result : @pipeline.PipelineResult =
  @pipeline.run(source, "main.mbt", @core.IfaceSymTab::empty())
println(@pipeline.render_result(result))

// 用途二：审计一台状态机（机器表以纯数据进来）
let spec : @statecheck.MachineSpec = { name: "主体", states: [...], ... }
println(@statecheck.render(spec))
```

### 跑一遍 demo

```bash
moon run src/cli          # 6 个样例 × 三鉴、文件种类 demo、样例机器
```

## 用途一：程序代码修订

三鉴是这样装配的：**后面每一鉴都消费前面那一鉴的表**。

| 透镜 | 包 | 职责 | 产出 |
|---|---|---|---|
| 结构 | `src/walk` | 以赋值论绑定、未用/未定义/形参被改、常量折叠剪枝 | 绑定表 `fn_bindings` |
| 类型 | `src/types` | 以标注论契约、推导、赋值/实参/条件检查（**声明来自绑定表**） | 签名表 `sigs` |
| 行为 | `src/interp` | 在格上做抽象解释、按签名分派方法、虚拟栈（**方法表来自签名表**） | 行为发现 |
| 合并 | `src/pipeline` | 一个缺陷在多鉴里的回声 → 一条报告，透镜取并集 | `render_result` |

```
=== undefined.mbt ===
2:10 - error: undefined variable 'missing' (UndefinedName) [structural+type+behavior]
  in main() at undefined.mbt:4
  in g at undefined.mbt:1
Summary: 1 finding(s) (before merge: structural 1, type 2, behavior 1)
```

三鉴都看见的同一个缺陷 → **一条**报告，标签取并集。死分支会被剪两次（结构侧的 `const_eval`
加上行为侧的 `ABool` 格值），而调用一个不存在的 `typo_fn` 产生零条发现。

## 用途二：静态状态修订

`src/statecheck` 接受 **任意状态机的纯数据规格** —— 一个 `MachineSpec`（状态 / 初始 /
终止 / 迁移 / 触发槽落位 / Block 理由 / 历程）。三鉴读机器表的方式，和读程序一模一样：

| 透镜 | 机器侧语义 | 它检查什么 |
|---|---|---|
| 结构 | **状态即绑定**（「以赋值论绑定」抬升到机器表） | 每个状态至少被一条迁移绑定（入或出）；只出不进 → `never entered`；从初始位出发的可达闭包；终止位必须可达——这台机器得能走到头 |
| 类型 | **驱动槽契约**（「以标注论契约」） | 每个触发必须落进已知槽，不许有空槽；一个 `Block` 必须带理由——**无路的一步必须出声说，不能沉默** |
| 行为 | **历程即抽象执行**（虚拟栈） | 每个历程步骤都必须被某条迁移承载；一个搁浅的步骤会带着虚拟栈从入口帧走到错误帧 |

```moonbit
let spec : @statecheck.MachineSpec = { name: "主体", states: [...], ... }
let findings : Array[@report.Report] = @statecheck.audit(spec)
let text : String = @statecheck.render(spec)   // 合并后的文本报告
```

**pyroduct 是被审计的主体，不是依赖**：本模块不依赖 pyroduct；方向是 pyroduct（它的
`audit` 包）拿自己的真实机器表拼出 `MachineSpec` 来调用本模块。单向：机器 → 分析器。

pyroduct 的真实自审（`moon run cmd/main -- audit`）打印：

```
规格 | 计数
---|---
状态 | 034
迁移 | 053
触发→槽 | 049 → 8
无路组合（带理由） | 228
修习历程 | 031 站

未预期发现：**0 条**
```

「未预期发现 0 条」这一行是绊线：真实表上一旦出现新的结构/类型/行为发现，就会让
pyroduct 的测试挂掉，强制一次复审。同一次运行还会列出它**每次都报**的四条**已知设计**
发现（两个只出不进的状态）——上面把它们略去了，因为那是模型本身、不是缺陷，而且要紧的
是最后那一行。

> `moon run src/cli` 末尾打印的 `pyroduct-shaped sample machine` 是本模块自己的
> **8 状态玩具**（`statecheck.pyroduct_flavored()`），不是 pyroduct 的真实表。它带的
> `182:12` 这样的坐标是**由状态名散列出来的稳定伪位置**，不是任何源文件里的行号。

## API 参考

### 程序分析 —— `src/pipeline`

| 函数 | 签名 |
|---|---|
| `run` | `(src : String, file : String, extern_iface : @core.IfaceSymTab) -> PipelineResult` |
| `run_functions` | `(src : String, file : String, extern_iface : @core.IfaceSymTab) -> PipelineResult` |
| `render_result` | `(r : PipelineResult) -> String` |
| `merge_findings` | `(all : Array[@report.Report]) -> Array[@report.Report]` |
| `merge_group` | `(g : Array[@report.Report]) -> @report.Report` |

`run` 让行为透镜在 **模块** 上入口，`run_functions` 让它在每个 **函数** 上入口（见
[覆盖范围与边界](#覆盖范围与边界)）。两个视图是**分开的，不是相加的**。

### 机器表 —— `src/statecheck`

| 函数 | 签名 |
|---|---|
| `audit` | `(spec : MachineSpec) -> Array[@report.Report]` |
| `render` | `(spec : MachineSpec) -> String` |
| `pyroduct_flavored` | `() -> MachineSpec` —— 那个 8 状态样例机器 |

### 图与出处 —— `src/sa`

| 函数 | 签名 |
|---|---|
| `mermaid_states` | `(verdicts : Array[Verdict], summary : Summary, prov : ScanProvenance, per_file : Int32, max_files : Int32) -> String` |
| `provenance_for` | `async (target : String, root : String) -> ScanProvenance` |
| `scan_artifact_name` | `(p : ScanProvenance, root : String) -> String` |
| `aggregate` | `(verdicts : Array[Verdict]) -> Summary` |
| `stamp_utc` | `(ms : Int64) -> String` |
| `moon_mod_version` | `(src : String) -> String` |

`mermaid_states` 返回合法的 mermaid `stateDiagram-v2`。它绕开的两条约束都是实测的，不是
假设的：转移标签是**第一个** `:` 之后的全部内容，所以里面不能再有 `:`——于是位置和消息
都放进带引号的状态标签里；而 MoonBit 没有运算符续行，所以以 `+` 开头的源码行是解析错误，
这就是文档一行一行 `write_string` 写出来的原因。

`per_file` 和 `max_files` 给绘图封顶，`0` 表示不封。**被封顶砍掉的部分会在图里写明**，
写在头部和文件上的一条注里，所以被截断的图不会被读成干净的图。文件按 **actionable**
条数降序排，而不是按原始发现数：在 `moonbitlang/core` 上，原始发现最多的文件是
`v128/simd_float.mbt`，**51** 条发现——全是 notice、零缺陷；按原始数排会把它放在一张
「该把注意力放在哪」为职责的图的第一位。

### 出处 —— 产物的文件名

一次扫描结果是对**某棵特定的树**、被**某个特定的工具链**、在**某个特定的时刻**读出来的
主张。这三样都进文件名 —— `<package>_<version>_<moonbit>_<stamp>.mmd`：

```
moonbit_static_analysis_0.4.47_0.1.20261023_20261024T060000Z.mmd
moonbitlang-core_0.1.20261105+65efd5b93_0.1.20261104_20261114T060000Z.mmd
tree_unknown_unknown_0.1.20261104_20261114T055946Z.mmd     # 版本没定下来
```

| 字段 | 回答什么问题 | 来源 |
|---|---|---|
| `package` | 读的是谁 | 坐标，或**解析后**的目录名 |
| `version` | 它的哪一版 | 目标的 `moon.mod`（`moon.mod.json` 也认） |
| `moonbit` | **是哪个工具链读的** | `moon version`，作为子进程跑 |
| `stamp` | 什么时候 | `@async.now()`，UTC |

`moonbit` 是从树里**恢复不出来**的那一格，也正是它决定一次扫描能不能和后来的扫描比较。
如果 `moon version` 子进程失败，这一格读作 `unknown`，而不是写错。

它刻意**不**做三件事：不省略它定不下来的东西（缺失的版本、工具链或时钟写成字面量
`unknown`——四个字段里省掉一段会让**其余几段错位**）；不产出点开头的文件名（以 `.` 开头的
名字在 `ls` 里看不见，而一个没人能列出来的产物，谁也不会再找到它）；不把文件名本身当成
记录——同样的三件事会以 `%%` 头注释在文档**里面**再写一遍，因为文件会被改名，而一旦改了名，
名字就不再是任何证据。

### 报告 —— `src/report`

| 函数 | 签名 |
|---|---|
| `Report::render` | `(self : Report) -> String` |
| `render_reports` | `(reports : Array[Report]) -> String` |

每条发现都带一条注，含 `WHY:`（哪条规则触发的、依据什么触发的）和 `HOW:`（该改什么），
取自 `@core.Family::advice`。

## 命令行参考

```
moonx riantr/moonbit_static_analysis@latest <target> [旗标]
```

| 旗标 | 含义 |
|---|---|
| `<target>` | 注册表坐标（`author/module[@version]`）或路径。省略则扫描当前目录。 |
| `--exclude <dir>` | 要跳过的目录名。可重复。它存在是因为点目录规则抓不全：项目可能把 vendored 的注册表快照放在一个普通名字下。 |
| `--extern-iface-dir <dir>` | 在这个目录里找 `.mbti`，把里面声明的类型/值当成被分析的所有 `.mbt` 文件里的合法名字。可重复。最自然的目标是 `moon fetch` 过依赖之后的 `.repos/`。目标自己的树永远被索引。 |
| `--no-auto-fetch-deps` | 默认会读目标的 `moon.mod` 并 `moon fetch` 每个直接依赖。加上它就跳过自动 fetch。 |
| `--mmd <path>` | **同时**把这次扫描写成 mermaid `stateDiagram-v2` 落到 `<path>`，并在最后一行打印 `MMD<TAB><path>`。刻意做成可选：stdout 始终是权威的文本报告。 |
| `--mmd-auto` | 同上，但自己取名，写到**工作目录**——绝不写进被分析的树里。 |
| `--per-function` | 让行为透镜在每个 **函数** 上入口，而不是在模块上。 |
| `--findings-shown-per-file N` | 每个文件**打印**多少条发现（默认 40）。这是打印上限，不是分析上限：SUMMARY 的计数来自全部发现，所以调大它只是把本来已经计数的发现显示出来，不会改动 SUMMARY 里的任何数字。 |
| `--show-notices` | **每一条** notice 都逐行打印，而不只是那些可能藏住一条发现的。默认只有当 notice 所在的区域落在某个函数体的范围内——也就是某个结论可能因为它而被压下——才逐行打印；其余的 notice 按形状汇总进扫描末尾的一张 `NOTICES` 表。这个开关把完整的逐行列表恢复回来，也就是 0.4.36 之前的样子，而且它不改动任何计数：两种模式下 SUMMARY 的数字完全一样。 |
| `--families MSA-007,MSA-002` | 只报这些家族，按它们的**稳定 id**。id 就是每条渲染出的发现、每条 JSON 记录都带的 `MSA-NNN` 码；完整名单见[置信度、id、profile 与 `nosec`](#置信度idprofile-与-nosec)。这个版本不认识的 id 只是一条 `WARNING`，扫描照跑——后来版本才加的家族不该让老分析器的 profile 用不了，而打错字该吵出来而不是直接崩掉。 |
| `--exclude-families MSA-007` | 除了这些家族，其余全报。同一套 id 词汇、同一套规则。一个 id **既**被包含**又**被排除是 `ERROR`，扫描根本不跑：这两条规则互相矛盾，谁赢要由扫描器里两个 `if` 的先后决定。 |
| `--honor-nosec` | 认被分析源码里的 `// nosec` 注释：`// nosec` 压掉那一行上的全部发现，`// nosec MSA-007` 只压掉那一行上的那一个家族。**默认关闭**，而这个默认是一个决定而不是遗漏：一个工具会因为被分析源码里的一句注释就不再报某条发现，那它的输出就得先读一遍源码才敢信。一条**什么都没压掉**的 `// nosec` 会被当成一条自己的发现报出来——过期的抑制是源码的事实，而源码正是这工具分析的东西。 |
| `--ssa-cost` | 量一量**静态单赋值**在目标树上要花多少，打印一行 `SSA-COST`：程序定义了多少变量、SSA 会给它们多少个版本、多少个 φ 函数、以及去掉它们需要多少条拷贝。它是一次**查询**而不是扫描——打印完这一行就停，不报任何发现。它量的是讲义自己的那条说法——南京大学 2026 秋季《Intermediate Representation》那一讲的 p.37：「SSA 可能引入太多变量和 φ 函数」——一条不带数字的说法。这一行把**覆盖率**和数字印在一起，因为没有覆盖率的数字只是一半个数字。 || `--contexts` | 在 `SUMMARY` **之后**打印一行 `CONTEXTS`：行为透镜**执行**了多少个函数体（`executions`）、跨多少个不同签名（函数 + 抽象实参）、从多少条调用串到达、有多少签名被多于一条调用串到达、有多少次到达是递归截断、最深调用栈几层。属于 opt-in，理由与 `--metrics` 相同，但它回答的是**另一个**问题：不是"检查了多少"，而是"分析器把它的执行花在哪里"——本代码在每个调用点**重新执行**被调函数体，而不是把它摘要掉（书里 §8.4 的 functional 方法），因此 §8.3 的调用串上界从未被施加，递归截断是唯一的一处上下文合并。 |

`--mmd` 必须带路径，`--mmd-auto` 是另一个写法，这是刻意的：一个可选的值在这里是有歧义的，
因为在 `<target> --mmd <path>` 里，`--mmd` 后面那个词既可能是路径，也可能是第二个没预期的
目标，没法分辨。

> **命令行无法以非零码退出。** MoonBit 在这里可用的包里没有暴露进程退出的入口，所以一个
> 定位不到的目标会打印 `ERROR` 然后仍然退出 0——**调用方必须读输出，而不是读退出码**。

## 输出怎么读

```
SCANNED	107 files under ...\ML\CI
CLEAN	.mbti	unchecked=0	...\CI/pof/pkg.generated.mbti
PARTIAL	.mbt	defects=1	notices=2	unchecked=17	read up to line 36, 57 after it not shown	...\CI/pof/aggregator.mbt
12:3 - notice: ... (UndefinedName) [behavior, MSA-002, low]
PARSED	32/107 files understood (29.9%); 75 more read only up to their first parse error
SUMMARY	files=107	parsed=32	actionable=56	notices=212	unreliable=15759	withheld=6769	unchecked=2841	total=16027	(actionable+notices+unreliable = total; withheld ⊆ unreliable; unchecked calls are not findings)
```

- **`PARSED` 才是头条。** 前端覆盖的是 MoonBit 的一个**子集**，所以它读不懂的部分量的是
  这工具的盲区，不是你的代码。
- **读了一半的文件仍然值得读。** 解析器记下它**真正**失败的那一行；之前的发现照报
  （`PARTIAL`），之后的计入 `unreliable` 且永不展示——那来自一棵已经不对的树，把它当结果
  端上来，就是这个工具当初要根治的那个毛病。
- **被跳过的声明不会挪动这条边界。** 「这个 `test` 块没被分析」不影响后面的代码仍被读到，
  所以这样的文件是 `FOUND`。
- **`actionable` 不含 notice。** 我们选择不分析的声明形式不是你代码的缺陷——而且它也不装成缺陷：
  一条范围限制渲染成 **`notice:`**，不是 `error:`。
- 读不懂的文件**按原因分组**，而不是一行一个。
- **只有可能藏住发现的 notice 才值得占一行。** 0.4.36 起，扫描只在 notice 所在的区域落在某个
  函数体的范围内——也就是某个结论可能因为它而被压下——时才逐行打印它，其余的 notice 按形状
  汇总进扫描末尾的一张 `NOTICES` 表：

```
NOTICES	TOTAL	notices=13520	printed=1705	aggregated=11815	1705 of them are printed per line: the ones that can hide a finding, and the low-confidence ones, which name a place. The other 11815 are counted by shape below
NOTICES	count=7947	test declaration is outside the analyzed subset; its body was not analyzed
```

  表里的 `notices` 就是 SUMMARY 的 `notices`，`printed` 加 `aggregated` 又等于它，而每一行
  加起来等于 `aggregated`：三个数来自三次不同的计算，读者可以据此核对有没有东西在半路上丢掉。
  上面摘出来的是 TOTAL 行和最大的一行；整张表每种形状一行，从大到小排。
  `printed` 这个数说的是**归类**，不是保证这些行都上了屏——每文件 40 条的打印上限对它们照样
  有效，被藏起来的条数写在 `... N more in this file` 那一行里。`--show-notices` 把完整的
  逐行列表恢复回来。
- `actionable + notices + unreliable` = `total`，这一行自己断言。`withheld` 另行报出，但它是
  `unreliable` 的子集，所以故意不参与这个和式。

**跨文件类型符号解析** —— 一个 `.mbt` 用了别的包里声明的类型（比如 `@argparse` 的
`Command`），单文件分析器只看得见自己那个文件，于是会报 `undefined name 'Command'`。
`--extern-iface-dir <dir>`（可重复）在指定目录里找 `.mbti`，把它们声明的类型和值签名
装进一张**跨文件符号表**；结构遍历和类型透镜在报 `FUndefinedName` 之前会先查这张表。

这张表只**抑制**，从不发明合法绑定：表里没有的名字照报。类型命中返回 `TUnknown`；值命中
返回 `TUnknownFn`——一个已知是值、但签名没读的值——于是 `Command(...)` 既不会触发
`FOpMismatch`，也不会拿一个凭空发明的参数个数去检查。查表前会先剥掉 `@pkg.` 前缀：
`.mbti` 里写的是裸名（`pub fn T::m`），使用处必须写 `@pkg.T::m`，所以精确匹配下这两种
拼法永远碰不上，而命名另一个包最常见的写法也就永远打不中。

### 置信度、id、profile 与 `nosec`

0.4.37 起，每条发现都带着**严重度之外的两个事实**，都在原本放透镜标签的那个方括号里：

```
12:3 - notice: no visible binding for 'cmd' (UndefinedName) [structural, MSA-002, low]
```

**置信度说的是透镜检查了多少。** 严重度说的是这条发现**如果是真的**有多糟；置信度说的是分析器
有多确定它是真的——两者互相独立：一条发现可以又严重又不确定，也可以无关紧要却非常确定。一共
三个值，正好是透镜可能处的三种境地：

| 置信度 | 透镜…… | 家族 | 渲染成 |
|---|---|---|---|
| `high` | 手边就有声明、签名或类型 | 其余全部 | 它自己的严重度 |
| `low` | 只在**名字**上推理 | `UndefinedName`（MSA-002）——它没找到的那个绑定，可能在它根本没拿到的某个文件、某个包里 | `notice:` |
| `undecided` | 根本没法判断 | 一条声明出来的范围限制——分析器自己的盲区 | `notice:` |

**0.4.38 起，这条轴开始决定事情。** 分析器站不住脚的发现被**降级**：渲染成 `notice:`，计入
`notices` 而不是 `actionable`。它**没有被藏起来**——家族、稳定 id、置信度、还有读者屏幕上
属于它自己的那一行都还在；变的是标签和桶。一条 `low` 的发现说的是*它没找到的那个绑定可能在
它根本没拿到的某个文件、某个包里*，而 `actionable` 是你应该去看的那张单子。

一条发现**不会**因为不确定就被丢掉。它只是被以更低的置信度报出来——而这正是「沉默读起来像
『没什么可报』」和「一句关于检查了多少的陈述」之间的全部差别。

**id 才是稳定的那个名字。** 家族的公开名字是第二套要手工维护的词汇：原先十一个名字里有五个
不是标签去掉 `F`（`FParse` → `ParseError`、`FAssignType` → `AssignTypeMismatch`、`FArgType`
→ `ArgTypeMismatch`、`FOpMismatch` → `OperatorMismatch`、`FCondBool` → `NonBooleanCond`）。
一个把 `"family": "ArgTypeMismatch"` 写进抑制或 CI 过滤器的消费方，在名字被改的时候**收不到
任何提醒**——因为名字不是契约。而 **id** 只分配一次、**永不重编号**，所以它能活过一次改名：

| id | 家族 | id | 家族 |
|---|---|---|---|
| `MSA-001` | `ParseError` | `MSA-007` | `ArgTypeMismatch` |
| `MSA-002` | `UndefinedName` | `MSA-008` | `OperatorMismatch` |
| `MSA-003` | `UnusedLocal` | `MSA-009` | `MethodError` |
| `MSA-004` | `UnusedParam` | `MSA-010` | `NonBooleanCond` |
| `MSA-005` | `ParamChanged` | `MSA-011` | `Unreachable` |
| `MSA-006` | `AssignTypeMismatch` | `MSA-012` | `StaleNosec` |
| `MSA-013` | `InfeasibleBranch` | `MSA-014` | `RedundantGuard` |
| `MSA-015` | `DeadStore` | `MSA-016` | `DivisionByZero` |
| `MSA-017` | `NegativeIndex` | | |

这些 id 是**手工**分配的——从枚举的位置推导一个 id，会在每次插入之后把后面所有家族重新编号，
而那正是 id 唯一不能做的事——并且 `_verify/check_family_roster.ps1` 会**检查**这张表：每个家族
一个 id、没有 id 被用两次、id 是从 `MSA-001` 起连着的一段，以及反向表（id → 家族）与正向表
严格互逆。写了两遍的数迟早会自己跟自己不一致，而两张表之间的不一致读者是看不见的，所以要用
一道门去比对它们。

**而且这张表现在也和代码对拍**：`MSA-015`（`DeadStore`，死存储家族）整整一个
版本都漏在这张表外面，却没有任何一道门吭声——因为每道门都是把代码里的花名册跟它自己比对，
而这张表只是散文。`_verify/check_readme_links.ps1` 现在会把**两份** README 里的 id 和名字读
出来，断言每张表点名的家族集合就是 `all_families()` 返回的那个集合——于是「代码里有、表里没有」
的家族变成一道**门禁失败**，而不是读者自己要去发现的惊喜。

**`MSA-015` 也管声明。** `let` 就是一次写入，而一个在任何读取之前就被覆盖掉的 `let`，和一个
被覆盖掉的重赋值一样死：`let mut x = 0` 后面接 `x = 1`（中间没有对 `x` 的读），报在**声明那一行**上。
两者靠各自的措辞区分——*the value bound to 'x'* 和 *the value stored in 'x'*——而且声明只有在
这个名字在别处被读过时才报，所以它绝不会和 `MSA-003`（`UnusedLocal`，说法正相反）重复。

**`MSA-016` 和 `MSA-017` 是讲义自己的两个应用，而工具链这两种形状都抓不到。** 这棵树的符号
分析出自的那一页幻灯片标题是 *Static Analysis — An Example*，它点名了一个分析的两个应用：
*「判定给定程序里所有变量的符号（+、− 或 0）」*——*「检查除以零的错误」*、*「检查数组的负下标」*。
这个分析是一个**符号**定义域（`+`、`−`、`0`、`unknown`），而且它回答的方向是**必然**：符号未知的
除数**不报**——工具只在能证明的时候说「这次除法**就是**除以零」，而一句「可能」的崩溃断言就是
一个等着出现的假阳性。

对着编译器实测：`moon check` 跑一份同时装着 `1 / 0`、`10 / y`、`arr[-1]`、`arr[0 - 1]` 和
`arr[0]` 的探针，退出码 0，对这两种形状一个字都不说。所以这里的一条发现**不是**编译器已经说过
的重复项——它是工具链里唯一会说这件事的东西。

两条断言是两个家族，因为它们是关于**不同操作数**的两条断言：`MSA-016` 关于**除数**（`/` 与 `%`——
取余在运行时同样失败；而浮点被除数不是崩溃，所以不报），`MSA-017` 关于**下标**。一行可以同时
带上两者（`a / b[0]`），而只给一个家族的读者就得猜这条发现说的是哪个操作数。

**profile 按 id 选家族**，而且在扫描开始前就被检查过：这个版本不认识的 id 只是一条 `WARNING`，
扫描照跑；一个既被包含又被排除的 id 是 `ERROR`，扫描根本不跑。这个过滤作用在整份发现列表上、
在可信区间切分**之前**，所以 `total`、`unreliable` 和 `notices` 说的都是同一批发现。

**`nosec` 是按行、按家族**的，而且**默认关闭**：

```moonbit
let x = cmd()          // nosec              -- 压掉这一行上的全部发现
let y = cmd()          // nosec MSA-002      -- 只压掉这一行上的那一个家族
```

一条**什么都没压掉**的 `// nosec` 会被当成一条自己的发现报出来——`StaleNosec`，`MSA-012`——
因为过期的抑制是源码里的死重量，也是它当初指的那段代码已经变了的信号。那条过期发现在抑制
**之后**才生成，所以一条空白的 `// nosec` 压不掉关于自己过期的那条警告。

**而且它只够到发现自己所在的那一行，不够到整条语句。** `bandit` 把问题所在行和**上下文**的
行范围并在一起，所以在它那儿，写在多行调用第一行上的 `// nosec` 能压掉三行之后的那个名字。
这里行就是行：写在语句第一行上的 `// nosec` **够不到**下面的名字，而那个名字会在它自己的位置
被报出来。两种写法都实测过——注释放语句第一行时发现仍然被报出来（渲染成 `notice:`，因为
那是分析器解不出来的名字），注释放名字自己那一行时文件是干净的。把这条规则放宽会移动固定的
语料基线，所以它写在这里，而不是悄悄塞进去。

**而且一次**成功**的抑制，在计数里不留任何痕迹。** `bandit` 留着**两个**计数器——空白的算
`nosec`，点名 id 的算 `skipped_tests`——所以读者能看出有多少发现是被源码自己的注释从报告里
拿走的。这里被 `// nosec` 拿掉的发现就是不在了：SUMMARY 数的是剩下的那些，而没有任何地方说
拿走了多少。实测：开着 `--honor-nosec`、两次抑制都生效时，整个输出里没有一处提到抑制。分析器
在**反方向**上是有披露的——它**查不了**的调用会记成 `unchecked`，而不是被悄悄抹平——所以这两半
今天并不对称，这个不对称写在这里，而不是留给读者自己去发现。

**分析器没能检查的调用，也被披露出来。** 类型透镜只有在读到了被调用方的签名时才检查实参个数
和类型；`.mbti` 给的是名字，从来不给参数表，方法的签名根本不在源码里，而 `..` 链式调用就是
换了写法的方法调用。0.4.37 之前，这三种情况工具一声不吭，于是「我没法检查这个」和「这里没
东西可报」是同一份输出——一个既没有发现、又有四百次没检查的调用的文件，打印出来和一个干净
文件一模一样。现在这个数出现在文件自己的判定行（`unchecked=N`）和 `SUMMARY` 上，并且**故意
不参与**那个和式。在七个固定语料上实测：**29,887** 次没检查的调用，对应 **31** 条 actionable 发现。

## 覆盖范围与边界

### 这个工具不跟谁竞争

在 `.mbt` 上，本工具 **不与工具链的编译器竞争**：`moon check` 有真正的解析器，读的是**整个**
语言。在同一棵 `moonbitlang/core` 上它**一条**诊断也不报；本工具的 `.mbt`
前端读的是一个 **子集**，解析 **1679 个文件里的 1621 个**（96.5%）；`.mbti` 和 `.mbt.md` 是 100%。

本工具能做而编译器不能做的：编译器**根本不审**的那三种文件——`.mbti`、`.mbt.md`、
`.mbtp`——以及跨包语义。

### 一条 finding 值多少：sound、complete、useful

没有哪个静态分析是精确的。**Rice 定理**说，程序行为的非平凡性质在一般情况下不可判定，
所以任何分析器都必须放弃点什么，唯一的区别是**放弃哪一头**。标准词汇是这样的：

- **sound** —— 不报漏报（false negative）：报出来的都真的存在；
- **complete** —— 不报错报（false positive）：真的存在的都报出来了；
- **useful** —— sound 或 complete 之一，但不可能两者兼得。

**这个工具是有用的，不是完美的，而且它说清了自己站在哪一边。** 它不声称完备：一条 finding
可能是误报，而它读不懂的语言构造会报成 notice，而不是报成缺陷。它也不声称 sound：死代码
那几个家族是对程序控制流与取值的近似做出的判断，而
[`--per-function`](#--per-function让行为透镜在每个函数上入口) 视图自己就写着它「还没有
sound」。它承诺的东西更窄，而且是逐条 finding 承诺的：**分析器自己站不住脚的 finding 会被
渲染成 notice**（见[置信度、id、profile 与 `nosec`](#置信度idprofile-与-nosec)），每条
notice 都写明工具没读懂什么。

本工具的分析所依据的讲义系列是南京大学《静态程序分析》（李樾，2026 秋季）；完整对照——本
仓库实现了课程自己的哪些分析、框架与本仓库在哪里不一致——见 `_verify/NARRATIVE.md` §0564。

### 前端读过去、但没有分析的构造

每一个它读过去**却没有分析**的声明或表达式形式都会报成一条 notice，而那条 notice 说的是
**工具**，不是你的代码——所以它渲染成 **`notice:`**，一个自己的标签，而不是借来的 `error:`。
在本项目自己的源码上实测（236 个文件，把每个文件 40 条的打印上限放开，所以数的是全部
发现而不是每份文件的前 40 条）：

| notice | 条数 | | notice | 条数 | |
|---|---:|---|---|---:|---|
| `test` 声明 | 1600 | | `const` 声明 | 7 |
| `if` 表达式 | 100 | | 短 lambda | 8 |
| `struct` 声明 | 85 | | `type` 声明 | 7 |
| 匿名函数字面量 | 48 | | `try` 表达式 | 1 |
| `enum` 声明 | 25 | | | |

去掉其中任何一行，都需要为那个形式做一个 AST 节点，所以它们是**功能**，不是措辞问题。
真正要紧的区别不在措辞，而在**位置**：**157** 条落在某个函数体的范围内，会把那个函数体的
审计整个关掉，所以它们逐行打印；其余 **1724** 条在所有函数体之外，什么也藏不住，于是在
扫描结束时按形状汇总成一张表。

**这个划分来自分析器自己的几何，而不是来自措辞。** 落在函数体范围内的区域在那个函数的洞
列表里，所以帧审计没法判定它可能读到过的绑定；落在所有函数体之外的区域不在任何函数的洞
列表里，所以它什么也藏不住。同一条 `if expression is outside the analyzed subset`，落在函数
体内就打印，落在模块顶层就汇总——所以一条按消息措辞来分的规则，对其中一半一定是错的。

**`match` 表达式那一行没有了**：0.4.34 开始读 `match` 的 arm，arm 是普通代码，它不再是一块
「读过去但没分析」的区域。

### `ParseError`：一个家族，两种含义

`ParseError` 不是一件事。它既覆盖**声明过的范围限制**——分析器读到了某个构造但没有分析
它——也覆盖文件里的**真缺陷**：没闭合的字符串字面量、坏掉的接口行、重复的签名。两者来自
不同的产出方，由一个判定 `Report::is_notice` 分开：渲染器、计数、mermaid 图和 JSON 桥都走
它。**有一个消费方故意不走**：决定哪些 notice 要在读者屏幕上单独占一行的那个切分，问的
是 `Report::is_declared_scope_limit`——所以一条被降级的发现仍然保留自己那一行。

| 它是什么 | 渲染成 | 计入 |
|---|---|---|
| 一条声明过的范围限制 | `notice:` | notice——不进 `actionable` |
| 一条低置信度的发现（0.4.38 起） | `notice:` | notice——不进 `actionable` |
| 文件里的一个真缺陷 | `error:` | actionable |

在七个固定语料和本项目自己的源码上实测（把每个文件 40 条的打印上限放开，所以数的是全部
发现而不是每份文件的前 40 条）：**23,226** 条 notice——每一条声明过的范围限制，加上 0.4.38
降级的那些低置信度发现。扫描自己也这么说：它的 `NOTICES` 表把其中 **3,971** 条算作逐行打印、
**19,255** 条算作汇总，3,971 + 19,255 = 23,226，正好等于渲染出来的 notice 行数——范围限制
和降级的发现加在一起。这个家族的真缺陷会渲染成 `error:`，发布门禁单独数这一类并要求它为零，
而一个都没有。

### 一个区域只让它「可能读到过」的绑定闭嘴

当前端**故意**不分析某个构造时——一个 `match`、一个表达式位置的 `if`、一个 lambda——
文件里就留下一块**区域**。那块区域从来没被读过，所以它可能包含对周围任何在作用域内的
东西的一次读取。分析器以前把这当成整个函数的**一个**结论：函数里任何地方有一块区域，
这个函数框架能下的**所有**结论就全部关掉——于是函数末尾的一个 `match`，会把函数顶部
声明的绑定的「未被使用」结论一起带走。

现在这个结论是**按绑定**下的。一块区域只能触及在区域开始时就已经在作用域内的绑定，
所以声明在该区域范围**之后**的绑定会被判定，而声明在之前的不会。只在区域**内部**被读取
的绑定仍然不会被报出来：那块区域可能读到过它，硬说它没被读过就是在正确代码上造假阳性。

这是实测的，数字值得一读。把「区域关掉」那个开关拿掉之后（`Walker::holes_in` 里的一行，
再和发布版对拍），在七个固定语料和本项目自己的源码上，工具会产出 **694** 条 `UnusedLocal`
和 **1,343** 条 `UnusedParam`（这里的「自己的源码」就是上面那张通知表数的同一个 236 个文件；
`_verify/` 里没有任何被跟踪的源码，所以被排除在外，这一对数字在干净检出上可复现）；
开着的时候，也就是发布版，它只产出其中**一条**：
`moonbit_labeler` 里一个赋值之后从未被读取的局部变量。所以被区域抑制藏起来的是
**693** 条局部变量和 **1,343** 条参数。这次收窄在今天的语料上**一条**也没找回：
那些绑定全都声明在各自区域的**之前**，那块区域仍然可能读到它们。它买到的是：
区域现在是一个绑定一个绑定地判，所以当某块区域被**读懂**时（也就是去分析 `match`
这件事本身），它恢复的是「其他区域够不着的那些绑定」的结论，而不是什么都恢复不了。

这件事没有编译器可以对照：MoonBit 的 `moon check` 根本没有「未使用的局部变量」这条告警
（本项目 `moon.mod` 里关掉的 `0079` 是 *unused derive*），而每一个固定语料都设了
`warn_list: ""`。这条规则由 `_verify/check_frame_audit.ps1` 和
`_verify/mutate_0501.ps1` 守着。

### `UndefinedName` 的两个盲点

两个都是已知的，而且都写在发现自己的注里：

- `#doc(hidden)` 的 API 在任何 `.mbti` 里都不出现，所以无法从依赖的**源码**索引；
- 写成 `@pkg.fn(1, 2)` 的顶层跨包引用，解析器不会把它折成一个可调用的名字，所以即使那个
  包**已经**被索引，它照样会被报出来。

### `--per-function`：让行为透镜在每个函数上入口

`--per-function` 把每个函数都当作程序的入口来分析，形参绑定到按**声明类型**新造的抽象值。
对入口点来说声明类型是唯一站得住的选择：形参的运行期值未知，透镜只能假定声明类型，
不能更多。

两个视图是**分开的，不是相加的**，所以可以互相比较而不会互相遮蔽。默认（模块）视图
不变：同一批语料加不加这个旗标，数字逐字节一致。

> **这个视图还不算可靠，旗标是可选的就是因为这个。** 它由
> `_verify/census_perfunction.ps1` 在**全部七个**固定语料上量，发版门禁**把数字钉住**。
> 现在它报 **47** 条 `actionable`——46 条在 `moonbitlang/core` 上，1 条在
> `moonbit_labeler` 上——而模块视图报 30 条和 1 条。census 自己的分类是：**26** 条是本前端
> 读不到的构造或算不出来的运算符；**20** 条是死存储——一个没人读的值，也是透镜自己对代码的
> 主张；剩下 1 条是真缺陷——`moonbit_labeler` 里一个赋了值却没被读的局部变量，也是本工具在任何
> 一个语料上报出的第一条真缺陷。
> **它们每一条都归进了有名家族。** census 为"归不了类"的发现留了一个桶，那个桶在 0.4.45
> 之前一直装着 9 条 `MSA-015` 死存储——一个家族在读还在某个"前端声明为子集之外"的区域里时，
> 报出了"这个值没人读"。修掉它们的规则，正是帧审计早就在用的那条：一个身上有洞的函数，
> 就不审它。
>
> | 家族 | 条数 | 透镜当时主张什么 |
> |---|---:|---|
> | C | 6 | 两个数组之间的 `==` |
> | D | 4 | `Int + Char` 与 `List + List` |
> | E | 3 | 结构体上的 `*` |
> | G | 8 | unreachable code——透镜自己对代码的主张 |
> | H | 1 | 赋了值却没被读的局部变量——透镜自己对代码的主张，也是这次普查里唯一一条真缺陷 |
> | I | 1 | `Double` 上的 `abs` |
> | J | 1 | 两个函数值上的 `*` |
> | K | 3 | 带具名实参的本地调用 |
> | M | 20 | 死存储——一个没人读的值——透镜自己对代码的主张 |
>
> **还有 17 条被降级了。** 0.4.38 起，分析器站不住脚的发现渲染成 `notice:`、算作 notice 而
> 不是 actionable，而普查把降级的那一组单列一张表、单列一个总数——一组离开普查的发现，就是
> 一组可能悄悄消失的发现。这 17 条全都带着 `low` 置信度，而且全都是分析器解不出来的名字。
>
> **模块视图数到的是 14 条，而且不是同样的那 14 条。** 两个视图是两次分析——这个视图把每个
> 函数都当成入口，模块视图拿的是整个模块——所以它们找到的不是同一批名字：在 `moonbit_core`
> 里这个视图报 17 条、模块视图报 14 条，其中只有 **8** 条是同一个位置。这和上面 46 对 30 的
> 差别是同一回事，两个视图始终是分开的，不能相加。
>
> | 降级家族 | 条数 | 透镜当时主张什么 |
> |---|---:|---|
> | B | 8 | BigInt 字面量的 `N` 后缀（`0N`）没被读出来 |
> | F | 1 | 分析器看不见的名字——同包兄弟文件里的辅助函数、类型参数的方法、`.mbti` 索引里没有的内部 API |
> | L | 8 | 已记录的 `#doc(hidden)` 边界 |
>
> **A 家族没了，而且它没了是因为它被修掉了。** 它是十六进制浮点：词法器把 `0x1.0p1023` 读成
> 整数 `0x1` 加一个名字 `p1023`，于是每一个它读不出来的指数部分都成了未定义名。现在词法器把
> 十六进制浮点读成**一个**字面量，取的值与工具链算出来的一致，所以这个家族一个成员都不剩了——
> 而这一行留在普查表里、是空的，好让一个又漏出名字来的十六进制浮点被当成**回归**抓住，而不是
> 报成一条普查归不了类的发现。
>
> **「能过」是量出来的，不是假设的。** `moon check --target all` 在 `moonbitlang/core` 上
> **一条**诊断也不报：锁定的 core 是自举的，而工具链会检查接口文件，这一版 core 干净地过了
> 这一关。这只是一半：没有诊断的文件和没人打开过的文件长得一模一样，所以
> `_verify/control_perfunction_census.ps1` 往带发现的**十七个**文件里（**副本上**）各追加一个
> 故意的类型错误，并要求错误原样回来——要求是 **17 / 17**，而今天这个对照读到的是 **17 / 17**。
>
> （这一行从 **0.4.43 到 0.4.46 一直是红的**，原因在语料而不在分析器：旧的锁定语料自带一条诊断
> ——`abort/pkg.mbti:4`，`fn[T] abort(String) -> T` 里的那个 `String` 不在作用域里——而检查器在
> 它上面**直接退出**，还没开始类型检查别的包，于是每一次探针都带着那一条错误回来，探针自己那条
> 错误从来没出现过。重新锁定到 `0.1.20261105+65efd5b93` 换来了一棵本工具链能从头查到尾的语料，
> 这一行也跟着变绿了。）
>
> **L 家族那八条是「已记录的边界」而不是缺陷**：跨包的 `#doc(hidden)` 函数没法从依赖的
> **源码**索引——只能从它的 `.mbti`——所以 `io` 的 `new_uninitialized` 构造器仍然报未定义函数：
> `@io.Utf8TextView::new_uninitialized` 四处、`@io.Utf8Writer::new_uninitialized` 两处、
> `@io.Utf8Reader::new_uninitialized` 两处。要回答它们，就得把这个分析器长成源码索引器，那是
> 另一个项目。**拿它来看透镜，不要拿它卡构建。**
>
> （这条注记原本写的是 **116 → 2**，而那个「2」是**六个**语料的普查——`moonbit_core`
> 不在其中，而它的发现数比其余六个加起来还多。那个数字对**量过的**语料是真的，对
> **没量过的**语料是假的。发布史见 [CHANGELOG.zh.md](CHANGELOG.zh.md)。）

## 文件种类

| 后缀 | 本工具做什么 |
|---|---|
| `.mbt` | 三鉴程序分析 |
| `.mbtx` | 三鉴程序分析 + import 块审计 |
| `.mbti` | 接口审计：畸形行 / 重复签名 / 未知的类型引用。行文法与 `moon info` 真正吐出的一致，所以生成的接口文件不会报*畸形行*。未知类型检查会查全模块的接口表，在 `moonbitlang/core` 上实测 **0**。残留的发现仍可能指向扫描范围之外声明的类型——请当作未经验证，而不是缺陷。 |
| `.mbt.md` |  literate：只认工具链真正**会编译**的围栏——`mbt check` / `mbt test` 以及 `moonbit` 写法。裸 `mbt`、裸 `moonbit` 和 `nocheck` 是展示块，跳过。 |
| `.mbtp` | 逻辑侧证明 lint（函数体里的字符串常量、被禁的 `!`/`↔` 形式、跨包调用、没有 `proof_ensure` 的引理）——**不能替代 `moon prove`** |
| `moon.mod` / `moon.pkg` / 工作区 | 只记录，不做静态分析——配置不是代码 |

完整分类见 [EXTENSIONS.md](EXTENSIONS.md)。

## 包结构

```
src/core      Span/Severity/Lens/Family(merge_group 契约)/Frame + Family::advice
src/report    Report 结构与渲染（透镜标签取并集、vst 帧）
src/flow      数据流框架：CFG + 四个求解器（轮转、带边传递的那一版，以及节点前与前向两种工作表，测试里互相对拍）、基本块及其上的控制流图、活跃变量（may，后向）、带 widening 的区间域、可用表达式（must，前向——同一个求解器的对偶读法）、常量传播（同一个格，读在 CFG 上）、调用图（整程序的那张图，解在 trait 层次上）、
以及指针分析的另外三种读法：带上下文（调用点 / 对象）、带范围（按需）、以及完全不要堆
（访问路径，也就是 storeless 模型）
src/sa        扫描入口 + aggregate() + mermaid_states()（public，库）
src/lexer     MoonBit 词法前端
src/parser    MoonBit 语法 → ast
src/ast       MoonBit 抽象语法
src/walk      结构透镜：绑定表 + 结构发现
src/types     类型透镜：Ty/Ty?/Sig 推导
src/interp    行为透镜：AbsVal 格 + 分派 + 虚拟栈
src/pipeline  装配：跑三鉴 + merge_group 合并
src/moonfiles 其它文件种类：.mbt.md 逐块三鉴 / .mbti 接口审计 / .mbtp 证明 lint
src/statecheck 用途二：通用机器表审计（纯数据 MachineSpec 桥）
src/samples   demo 样例（内嵌 MoonBit 源码）
src/cli       可执行入口（程序 demo + 文件种类 demo + 样例机器审计）
src/jsoncli   DeepSeek Harness 的 JSON 桥
```

根包是个薄转发层；实现是 `src/sa`，一个**库**。`src/sa` 和根包都声明
`supported_targets = "+wasm+native"`，因为文件 IO 和子进程来自 `moonbitlang/core/async`，
而只有部分后端有可用的 async 运行时；其余后端**跳过**这两个包而不是失败。

### 数据流框架同时承载两个方向

`src/flow` 里有一个 bot/join/eq 的 Lattice 和四个不动点求解器；三个增量里，
建立在它上面的每个分析都是 **may** 分析：活跃变量是 may 且后向，区间域沿上升链做 widening。
可用表达式是另一个方向——IN[B] = ∩ over P OUT[P]，一个**必须**分析，它的安全答案是
下近似——而它**不需要第二个求解器**：在 (⊤, ∩) 上的必须分析，就是把同一个载体按相反
次序读的 may 分析，所以它给现成求解器传一个 bot 为 ⊤、join 为 ∩ 的格。入口
节点特判为 ∅（程序开始前什么也不可用）；它三种会静默出错的方式——⊥ 播种、漏掉入口特判、
以及 meet 的累加身份元误取 ∅——各自都被 src/flow/avail_test.mbt 里的一行测试钉住。

**还有第四类分析：会「拿掉」一个事实的那种。** 指针分析（`src/flow/pta.mbt`）问的是
一个指针可能指向哪些对象，而框架把这道题承载了两次。流不敏感的那一版——整份程序一张
points-to 关系表——就是源码里写的那一版；流敏感的那一版在**每个程序位置**各留一张表，
并且在写一个指针时**替换**掉它的对象集合，而不是往里并。这是本包里第一个不是 join 的
传递函数，而它仍然是单调的，所以仍然跑在同一个求解器上。它的可靠性建立在指针定义域上：
一个变量旧的绑定是它私有的，而字段指针是按它的**对象**命名的（`o1.f`），所以每个
（对象，字段）对恰好只有一个指针，不可能有别的东西对那个字段持不同意见。
`src/flow/pta_flow_test.mbt` 把来源讲义为一份程序印出来的两张表都钉住（两种读法各一张），
并且检查两个求解器在它上面给出同一个答案。

**还有第五类：一个三元定义域，读在 CFG 上。** 常量传播（`src/flow/cprop.mbt`）问的是每个
程序点上变量的值是多少，它的定义域是三值的：`Undef`（还没有值）、`C(n)`（常量 `n`）和
`Nac`（不是常量）。定义域和规则本来就在这棵树里，**过程间**的那种读法也在——但那一种读法
没有框架：没有可跑的 CFG、没有可求交的汇合点、没有要到达的不动点。
`src/flow/cprop_intra.mbt` 补上的正是讲义说的那个框架（南京大学《Data Flow Analysis --
Foundations》）：一个 CFG、每个汇合点上的 meet、以及那个不动点。**没有一行是重写的。**
讲义的四条 meet 规则——`NAC ⊓ v = NAC`、`UNDEF ⊓ v = v`、`c ⊓ c = c`、`c₁ ⊓ c₂ = NAC`——
正是这个定义域早就有的 join；而三条传递规则——`x = c`、`x = y`、`x = y op z`——正是这个模块
早就有的规则，现在由一个函数（`cprop_assign`）供两种读法共用。两种读法只在**一种节点**
上不同：在调用处，过程间的规则给恒等，过程内的规则给 `Nac`。新的是框架，以及跑它的第三个
求解器。

**第三个求解器是另一种形状，不是新算法。** `src/flow/worklist.mbt` 里的 `solve_worklist`
就是讲义 §11 印的那个前向工作表：状态是 `OUT[B]`，每个节点的输入从它的前驱读回来，
而后继只有在它前驱的 OUT 变了时才被重新入队。这个包里本来就有轮转求解器（同一套方程、
不同的访问次序）和一个把状态放在节点**之前**的工作表；这是第三种形状。讲义把工作表称作
「Iterative Algorithm 的一个优化」（p.256），这句话是一个断言——两者算的是**同一个**
不动点——所以有一行测试把常量传播分别跑过新求解器和轮转求解器，要求它们**逐节点**相同；
另有一行测试要求工作表对两个前驱做 **join** 而不是覆盖，因为那正是 meet，也正是工作表
唯一会悄悄做错的事。

**这个分析不是分配的，而树里就是这么写的。** 讲义自己印了反例（p.249-252）：在图
`Entry → X(a=1,b=9) / Y(a=9,b=1) → Z(c=a+b)` 上，先 join 再传递给出 `c = NAC`，先传递再
join 给出 `c = 10`——两种次序里和都是 10，但 meet 已经把常量丢掉了。本树的分析先 join，
所以它给 `NAC`，也就是安全的那一边；而测试把**两种次序都钉住**，于是它们的差别是树里的
一个事实，而不是某页幻灯片上的旁注。定义域的序（`cpv_leq`）是公开的而不是私有的，
因为讲义最后一道题——*「证明我们的常量传播分析是单调的」*（p.254）——是一个关于某个函数
的断言，而那个函数必须够得着才能被测试；单调性也正是不动点定理会用到的前提。

**而它不开新的发现族。** 这道分析本可以报出的那一类——结果在程序跑起来之前就已经定下的
分支——已经由 `MSA-013`（`InfeasibleBranch`）和 `MSA-014`（`RedundantGuard`）说了。所以
`cprop_const_branches` 是一次**测量**，不是一次报告：它点名这道分析能定下哪些分支，而且
它不开新的族，因为本来就能承载那些发现的族已经存在。

**还有第六类：在它之上的整程序那张图。** 调用图（`src/flow/callgraph.mbt`）是讲义的第二
节——南京大学《Interprocedural Analysis》（谭添），p.33-39 与 p.52-56——也是方法调用不再是
一个洞的地方。讲义的 `Resolve(call)` 有三种情形，而 MoonBit 三种都答得上：一次**静态**
调用 `f(x)` 点名了自己的目标；一次**特殊**调用 `Type::m(x)` 在调用里就点了自己的类型；
一次**虚拟**调用 `recv.m(x)` 则由接收者的**声明类型**决定——若那是 trait，目标就是
trait 自己的方法，加上每一个实现了它的类型，也就是讲义那句「c 的子类或 c 自己」；若那是
一个具体类型，目标就是那个类型自己的方法。

MoonBit 没有类，所以讲义的**类层次**就是 **trait 层次**——`impl Trait for Type` 与
`derive(Trait)`——而它是从源码文本里读出来的，因为这棵树的 AST 不带它：parser 把 `trait`
与 `impl` 声明整块读过，于是「哪个类型实现了哪个 trait」在这棵树里曾经是谁也答不出的
问题。接收者的**声明类型**是注解（`SLet` 的第二个字段、`Param.tyann`），因为类型透镜
只公开模块帧，函数内部的局部类型因此根本没有被公开。

两条边界是被**数出来**的，不是被藏起来的。**方法体不在这棵树里**，所以图上的边只是
**点名**那些实现，然后停在那里——一个实现内部的调用是看不见的。而接收者**没有声明
类型**的调用解析不出任何目标，于是被记成未解析，而不是被连到一个猜测上。

**还有第七类：同一个指针问题，换一个上下文、换一个范围来问。** 上面的指针分析回答的是
「这个指针可能指向哪些对象」，而且是在整程序上回答、把所有调用上下文都并成一个答案。
定义这道分析的讲义把这个「并」写成一道**选择题**，而不是事实：《Pointer Analysis》
（南京大学 谭添，2021）p.34 印着 **Key Factors** 表，四个因子里有一行是 *Context
sensitivity ——「如何给调用上下文建模？」—— Context-sensitive | Context-insensitive*；
p.49-53 展开两种读法，p.53 用 *「We start with this」* 标出被合并的那一种。第四行是
*Analysis scope ——「程序的哪些部分该被分析？」—— Whole-program | Demand-driven*，
p.72-77 展开它。所以这棵树留空的那几格是**讲义自己的选项**，其中两格现在建好了。

`src/flow/pta_ctx.mbt` 是上下文敏感的那一版：分析按 **(函数, 上下文)** 对跑，而上下文由
调用点贡献。实现了三种抽象，都是讲义自己的——后续讲义《Pointer Analysis — Context
Sensitivity (I)》（`11-12_PTA-CS.pdf`）p.99-115 印着 `Select` 的几种变体：**不敏感**
（`Select _,_,_ = []`，p.102——每个函数一个状态）、**调用点**（`Select(c,l,_) = [l_1..l_k]`，
p.103——取最后 `k` 个调用点，也就是 k-CFA，Shivers 1991）、以及**对象**（p.100——接收者的
分配点）。**调用点的标号就是行号**，这是讲义自己的标号；一行里有两个调用时用 `line:col`。

**类型敏感没有实现，而原因是测量出来的。** `Select` 的第三种变体是接收者的**类型**。
局部变量的类型在这棵包的任何地方都读不到——类型透镜只公开模块帧，所以 `src/flow`
问不出接收者是什么类型，硬做就得编一个出来。所以它被留下，而不是猜出来。

`src/flow/pta_demand.mbt` 是按需分析的那一版，它复现的是讲义 p.76 的那一**列**：客户是
*call graph construction*，关心点是讲义那份程序的**第 5 行**（`z.bar()`），答案是
`z ➝ {o4}`。四条规则是**倒着**读的——哪些语句写了这个指针、它们读了什么——所以算出来的
只有**被点名的那几个指针**的表。两条边界是被**数出来**的，不是被藏起来的。这一支里
**调用的结果不是一个源**：没被建模的值贡献为零，而不是贡献一个编出来的对象。而被点名的
**参数**确实跨过调用边界，落到调用者的实参上——否则需求就停在被调函数门口了。

**范围改变的是算多少，不是算成什么。** 对于被点名的那个指针，按需分析给出的就是整程序
分析给出的答案；变的是被计算的那批指针。有一行测试要求这个相等式成立，所以第二种读法
不可能悄悄变成另一道分析。

**而它不开新的发现族。** 两种读法都不报任何东西：上下文和范围都是一次**测量**，而这棵树
的指针分析是库级的，不在报告流水线里。发现族清单仍然是十七个。

**还有第八类：同一个指针问题，不要堆地问。** 上面的指针分析问的是「这个指针可能指向哪些
对象」，答案是一组对象，而对象总得被**命名**。storeless 模型不命名它们。讲义自己的
**Heap abstraction** 那一行——*如何给堆内存建模？—— Allocation-site | Storeless*（p.34，
并且在每个因子那节的开头重印：p.48、p.54、p.71，以及 p.78 的「Pointer Analysis in This
Course」）——有第二格，而讲义在 p.42-43 引的就是它的定义：Vini Kanvar 与 Uday P. Khedker，
《Heap Abstractions for Static Analysis》，ACM Computing Surveys 2016（免费全文是
arXiv:1403.4910v5）。讲义点名这格九次、定义它零次；定义在综述里，所以这一格去读综述。

`src/flow/pta_storeless.mbt` 是 storeless 的那一版。堆是一组**访问路径**——一个指针变量后面
跟一串字段名——而综述的定义是精确的：*「storeless 模型不把与这些访问路径对应的内存位置或
对象显式化。设 V 为根变量集合、F 为字段变量名集合，则访问路径集合定义为 V x F*」*（p.7）。
这里的定义域就是那个集合，而规则是 `pta.mbt` 的那四条规则搬到这个定义域上。其中不一样的是
**New**：新的位置由**以变量为根的路径**命名，而不是由分配点命名——因为综述把「分配点」归类为
一种**概括**（p.11），而这一格正是没有概括的那个模型。在这里把新位置写成 `o1` 的树，是分配点
模型穿着 storeless 模型的衣服。

**概括是综述的，而它正是让这个模型有限的东西。** 访问路径集合是 `V x F*`，所以「访问路径的
个数可能是无限的，每条访问路径的长度也无界」（p.7）。综述用 **k-limiting 谓词**来框它——
「堆位置是否距根变量至多 k 次间接？」（p.12）——并配一个自环，它「为超过 k = 2 次间接的访问
路径存下伪别名」（p.9）。这棵树实现了那个谓词，并且**数切点**：比界更深的路径被并进它前缀
的那些位置。切点按**不同的位置**数，而不是按轮数数——不动点每轮把规则应用一遍，所以计数器数到
的是某个切点出现在几轮里，而不是程序里有几个切点。

**而算法是这棵树的，因为综述说了算法不是它的主题。** 它的摘要就是这么说的：*「我们的兴趣
在抽象上，而不在构造这些抽象的算法上」*（p.1）。所以这一格是综述的模型、综述的概括，加上这棵树
自己的那四条规则——而综述的 Figure 6 **没有**被复现，因为复现它的树等于宣称一个综述没有给的
算法。

**两个模型并排，测量。** 同一批程序由两个模型读，别名判定逐对比较。在讲义自己 p.28-29 的
那份程序上，两个模型**一致**——三对、三次一致、零次不一致——因为别名问题在两套词汇里是同一个
问题。而它们对「一个变量可能到达什么」**不一致**，而且这个差别是关于两种**抽象**的事实，不是
关于任一实现的。在 `x = new C(); x = new D(); y = x;` 上，分配点模型说 `x -> {o1,o2}`、
`y -> {o1,o2}`——两个**位置**、两个对象——而 storeless 模型说 `x -> {x}`、`y -> {x}`——一个
**根**、一条路径。这就是综述自己的区分（*「用分配点做概括，会把在同一个程序位置分配出去的堆对象
合并掉」*，p.11），也是两个模型的 points-to 答案不可比、而别名答案可比的原因。

**而这条边界是被数出来的，不是被藏起来的。** 在这套规则里，一个值永远是它所指位置的**根**，
所以最深的值在深度零上，综述里那个伪别名——一个指针到达界以下的路径——根本不会通过指针产生。
它在关系里才看得见：比界更深的路径在那里被并进前缀。两个模型的别名判定由一行测试逐对比较，
而那一行不一致的，就是上面这一行。

**而它仍然不开新的发现族。** 堆抽象是一次**测量**，不是一份报告：发现族清单仍然是十七个，
storeless 模型是库级的分析，和另外两种指针读法并列。

### CFG 底下还有一层：基本块

`src/flow/bb.mbt` 把一个 CFG 拆成**基本块**，再在基本块上建控制流图——也就是 CFG 通常
被画在其上的那一层。它对齐的那份讲义（南京大学 2026 秋季《Intermediate
Representation》）印了一份完整的实例，并把两个问题点名成可执行的问题：*「How to build
basic blocks on top of IR」*和*「How to construct control flow graphs on top of BBs?」*。
它那十二条指令连同 **leaders** 和**基本块**都是印出来的，所以这一层是拿印出来的东西
对拍，而不是拿自己的输出对拍。

讲义里的两条指令在 MoonBit 里没有对应的语句——一条无条件 `goto`，一条离开整个程序的
`return`——所以那份程序是手工搭成图的，而且搭成本仓库自己的构造器产出的形状（节点从后
往前分配，所以源码序是被**验证**的而不是被假定的）。同一个形状随后又用 `cfg_of` 从真正
的 MoonBit 语句再搭一遍，因为只对手工图有效的层，等于没有证明自己有效。

块图的**形状**和节点图一样——一个计数、一个后继关系、一个前驱关系——所以现成的求解器
不用写第二个就能跑在它上面，其中一行测试把同一个可达性分析在两张图上都跑一遍，并要求
两者一致。讲义里的 Entry 和 Exit 不是基本块：它说这两个节点「do not correspond to
executable IR」，所以它们被并排放在块列表旁边而不是混进去。`break` 是跳出**循环**而不是
跳出**函数**，而图分不出这两种 `Stop`，所以构造器没能忠实转换的语句计数被一并带出来，
调用方要先看它——和死存储家族的做法一样。

### 基本块底下还有一层：规则本来就是写在三地址码上的

`src/flow/ir.mbt` 是同一份讲义陈述那些规则时所用的**三地址码**。它不是一堆指令，而是一门
有语法的语言，而讲义把语法印出来了：一条指令的右边最多一个运算符，所以 `c = a + b + 3` 降级成
`t1 = a + b` 再 `c = t1 + 3`；一条指令最多三个地址；地址恰好三种——**名字**、**常量**、
**编译器生成的临时变量**。那六个常见形式是 `x = y`、`x = uop y`、`x = y bop z`、`goto L`、
`if x goto L`、`if x rop y goto L`。

`src/flow/ir_cfg.mbt` 随后把讲义的 **leader 规则**、**边规则**和 **Entry/Exit** 直接作用在
这样一条指令列表上——**完全不做翻译**。上一层是不得不翻译的，因为讲义把规则写在三地址码上，
而本仓库的图是语句图，所以那份翻译只能被相信、无法被检验。现在两条路径在讲义自己的程序上
互相对拍：同样的 leaders、同样的块、同样的边、同样的入口、同样的出口。这和两个求解器互相对拍
是同一个形状。

三地址码路径产出的是语句路径产出的**同一个 `Bb` 类型**——这是故意的：块图是一件事、一个定义，
两个可能对「块是什么」有不同看法的结构，等于对「块」有两个定义。

两个扩展项是明着标出来的，不是偷偷塞进去的：讲义的 IR 根本没有调用形式（这正是它把
`x = input` 写成从名为 `input` 的地址拷贝的原因），而它那「六个常见形式」里也没有 `return`，
尽管它自己的程序最后一条就是 `return`。

讲义自己那十二条指令，严格说**并不是**三地址码：`(9) c = 2a - b` 的右边有两个运算符，而 `2a`
不属于那三种地址之一。夹具原样保留讲义的文本，所以讲义印出来的块就是代码产出的块，并且有一行
测试把这件事写成话——一个「修正」过实例的夹具，检验的就不是讲义印出来的东西了。

`src/flow/laws_test.mbt` 把两个有限格的每一个元素都枚举出来，检查五条格律，以及传递
函数的**单调性**——不动点定理会用到的那个前提，也是一个格的三条闭包本身保证不了的那条
性质。points-to 表的格也是同样检查的。

### 还有讲义页脚上印的那个箭头：3AC -> SSA

`src/flow/ssa.mbt` 是同一份讲义第五节定义的**静态单赋值**形式。讲义用几句话陈述它的规则——「所有 SSA
里的赋值都是给名字互不相同的变量」「给每个定义一个新鲜的名字」「把这个新鲜的名字传播给后面的使用」
「每个变量恰好一个定义」——而页脚印着它讲的那个箭头：`3AC -> SSA`。

讲义自己的那张图就是检验。它把 `if e` 分到 `x₀ = 0` 和 `x₁ = 1`，两者汇到一个节点，那个节点里是
`y = x + 7`——`x` 被**红圈**标出来，因为那一页问的就是这件事：「如果一个变量的使用落在控制流汇合处
怎么办？」答案就是下一页引入的合并算子：`x₂ = ∅(x₀,x₁)`，而且「∅(x₀,x₁) 在控制流经过条件的真分支时取
x₀ 的值，否则取 x₁ 的值」。`src/flow/ssa_test.mbt` 把那张图变成一个程序、降级成三地址码，然后要求结果
与那张图**逐条指令**相同：

```
if e goto L1
goto L2
x₀ = 0
goto L3
x₁ = 1
x₂ = ∅(x₀,x₁)
y = x₂ + 7
```

讲义留白的两件事是**量出来的**，不是凭口味定的。它把汇合节点画成一个有**两条入边**的节点，说 φ 函数
「在汇合节点上选取各个值」——但一个变量的两个定义相遇的地方并不是那个地方，而是**支配边界**，
`src/flow/dom.mbt` 算的就是它。而那张图把 `y` 画成没有下标、`x` 却有三个，所以恰好只有一个定义的变量
保留它的裸名字。

**讲义自己那条代价说法，实测。** 《Intermediate Representation》那一讲的 p.37 说「SSA 可能引入太多变量和 φ 函数」「在翻译成机器码时可能引入效率
问题（因为拷贝操作）」——两条说法都不带数字。在讲义自己那个十二条指令的程序上：**8** 个变量变成 **16**
个版本，出现 **8** 个 φ 函数，去掉它们需要 **16** 条拷贝。在本项目自己的源码上——208 个文件、961 个
函数、7,487 条三地址码指令——同一个测量给出 **837** 个变量变成 **2,087** 个版本、**756** 个 φ 函数、
**1,860** 条拷贝。这条说法不是修辞。

这个测量是扫描器的一个模式，`--ssa-cost`，它打印一行：

```
SSA-COST	files=208	unreadable=0	functions=961	converted=5	partial=956	declined=5080	…
```

它把**覆盖率**和数字印在一起，因为没有覆盖率的数字只是一半个数字：读了哪些文件、量了多少个函数、
以及 lowering 放弃了多少条语句（4,979 条——三地址码那层把它懂的语句转掉，其余的计数）。发布门禁把这一行
钉住，所以下一个动它的增量必须**故意**去动那个钉子。
## 验证

```bash
moon check --target all --deny-warn   # 0 错 0 警（js / native / wasm / wasm-gc）
moon test --deny-warn                # wasm 1600/1600；js 与 wasm-gc 1458/1458
moon run src/cli                     # 程序 demo + 文件种类 demo + 样例机器审计
```

`--deny-warn` 是刻意的：不加它，就没有任何东西强制「0 警」这个说法——一次告警回归会静悄悄
地过掉 CI。CI（`.github/workflows/gate.yml`）跑 `moon update`、`moon check --deny-warn`、
`moon fmt --check`、`moon test --target js --deny-warn` 和 `moon build --target wasm`。

各 target 的测试数量不同是刻意的：`src/sa` 与 `src/jsoncli` 声明
`supported_targets = "+wasm+native"`，所以 js 与 wasm-gc 这两次运行会**跳过**这两个包而不是
失败它们。一个声称所有 target 都是同一个数字的测试计数本身就是错的，而 wasm 那个数字是
唯一同时覆盖渲染器和扫描器的。

### 唯一的发布入口

`moon check` 和 `moon test` 是地板，而本项目不只靠地板。它上面的所有东西都在**一个**脚本里：

```bash
powershell -NoProfile -ExecutionPolicy Bypass -File _verify\release.ps1
```

`_verify/release.ps1` 依次跑：门禁自身的自测；`moon fmt --check`；`moon check --deny-warn`；
三个测试 target；`moon build --target wasm`；**产物的宿主契约——用户的工具链必须提供的那些符号，
发布出去的字节和本地构建都要查**；语法探针自己的判定；自身源码自扫；**这份
README 自己的链接、锚点、版本与计数**；**变异门名册，以及一个证明它会变红的自测**；**注册表
到底会收到什么，以及一道保证碎屑不会混进去的检查**；**通知的标签，以及一道保证范围限制不会被
当成错误的检查**；**帧审计，以及一道保证一个区域只让「它可能读到过」的绑定闭嘴的检查**；已发布包
自扫的自测；与固定基线的语料比对；逐函数普查及其对照；**行为透镜自己的那张表，跟今天分析器
真正产出的数字对账**；然后是**每一个**变异门——**87** 个。

下面是其余各个 stage 的名字，按它们各自打印出来的原样列出——所以一个跑了、却没在这里点名的
stage，就是读者找不到的 stage：

    moon fmt --check
    moon check --deny-warn
    moon test --target js
    moon test --target wasm
    moon test --target wasm-gc
    moon build --target wasm
    moon build --release --target wasm
    the host contract of the artifact (what a user's toolchain must supply)
    grammar probe control (its verdicts can go red)
    self-scan (own source)
    ssa cost (own source)
    README links, anchors, versions and counts
    gate roster: self-test (seven injected defects must be caught)
    gate roster: one harness, one list, and a count that matches
    the shared harness: the INCONCLUSIVE verdict, shown to go red
    proof contracts: no false #proof_pure
    package contents: the junk stays out, the evidence stays in
    notice labels: a scope limit is a notice, a defect is an error
    the family roster: one id each, contiguous, and reversible
    frame audit: a region silences the bindings it could have read, and no others
    match arms: the arms are read, the findings are true ones, and the fallback is exact
    published self-scan self-test
    published package self-scan
    the notice reconciliation can go red (a real defect is seen)
    corpus SUMMARY vs pinned baseline
    per-function census vs pinned baseline
    per-function census control (the files are READ by moon check)
    the behavior lens: measured against its own header
    the region suppression: what it hides, measured and pinned
    the reach of the `raise?` construct, measured and pinned
    the premises of the 0505 porting plan, measured
    the notice flood: which notices deserve a line, measured
    the three bandit transfers: measured, not asserted
    the confidence demotion: measured, not asserted
    the transfer scope: the requirements document, the three rows, and where they landed

这份名单是从 `_verify/release.ps1` **推出来的**，并由 `_verify/check_readme_links.ps1`
检查：所以一个加了门禁、却没在这里点名的 stage，会让那道门禁变红，而不是悄悄地让门禁做的事
变宽。

### 这三项转移是被要求做的什么

置信度轴、稳定的家族 id 和 `nosec` 不是这个项目自己发明的。它们是**一份需求文档里的
三行要求**——那份文档在本仓库的**上一级目录**：`bandit_review.md`，一份对 PyCQA
`bandit` 的评审，读于 **2026-10-27** 的工作树。那份文档在这里**不会被改**：一份被改成
迎合实现的需求文档，就不再是需求了。

| 行 | 它要求什么 | 实现它的文件 |
|---|---|---|
| 1 | 每个发现一条**置信度**轴，与严重度并列 | `src/core/core.mbt`、`src/report/report.mbt`、`src/jsoncli/main.mbt` |
| 2 | **稳定的家族 id**，以及一个被检查的 profile | `src/core/core.mbt`、`src/sa/profile.mbt` |
| 3 | **`nosec`**，包括那条「抑制没压住任何东西」的警告 | `src/sa/profile.mbt`、`src/sa/main.mbt` |

第 3 行落在**别的地方**，和评审预测的不一样。评审把它放在 `parser.mbt` 的 skip
机制里，而 parser 并不参与：一条什么都没压住的抑制，是关于**最终**发现集合的事实，而
parser 层的 skip 跑在产出那个集合的镜头**之前**。推理过程、评审给那一行自己钉的
pin（0507 按 settle 自己的话把它反转了），以及那份有日期的状态栏，都在
`_verify/NARRATIVE.md` §0514。

**这份地图是被检查的，不是被断言的。** `_verify/check_transfer_scope.ps1` 点名那份
文档、逐字引用那三行，并把 §0514 地图里的每个 `file:line` 对着这棵树解析一遍——文件
在，而且那一行还带着那个符号。它的 `-SelfTest` 会往一份副本里为「这道门禁可能不再
守住的每一种方式”注入一种缺陷，并要求每一种都被抓到。**全部被抓到**，而且门禁会打印出
到底有几种。

这份名册是**被检查的，不是被断言的**：一个在磁盘上存在、却不在名册里的变异门**永远不会跑**，
而一个不会跑的变异门和一个跑绿了的变异门长得一模一样。`_verify/check_gate_roster.ps1`
把两份名册**双向**比对；它的 `-SelfTest` 往 `_verify` 的**副本**里注入七种缺陷——名册没
列的变异门、名册列了却不在磁盘上的变异门、脱离共享 harness 的变异门、被删掉的 harness
保证、harness 里的 `--filter`、harness 头部过时的计数、一条没有指明项目根目录的 moon
调用——并要求每一种都被抓到。**七种
全部被抓到。**

**发到注册表的东西也被检查。** 打包哪些文件由 `.moonignore` 决定，而一份没人验证过的
意图清单就是一句注释。`_verify/check_package_contents.ps1` 跑 `moon package --list`
——和 `moon publish` 用的是同一条命令——并断言：碎屑**不在**（提交信息草稿、扫描产物、
凭据、门禁记录、remeasure 转储），证据**在**（87 道变异门及其 harness、settle 脚本、
叙述、名册门，以及读者会被引去的那几份文档），并且每一个被 git 跟踪的文件都发得出去。
**两个方向都已被证明会变红**：把 `COMMIT_*.md` 那条规则注释掉，包里就多出 23 份草稿，
门禁失败；把 `_verify/NARRATIVE.md` 排除掉，叙述就没了，门禁也失败。

**通知不是错误，标签就是这么说的。** 一条声明过的范围限制——「match expression is outside
the analyzed subset; it was read but not analysed」——渲染成 **`notice:`**，绝不是 `error:`：
它说的是分析器读到了什么，不是它读到的代码有什么毛病。`FParse` 是一个家族、两种含义，
两者由一个判定 `Report::is_notice` 分开，而渲染器、SUMMARY 里的 `actionable` 计数、
mermaid 图和 JSON 桥全都走它——所以标签和数字不可能互相打架。
`_verify/check_notice_labels.ps1` 检查渲染出来的输出、用工具自己的消息跑遍四条产出路径，
并在源码里守住标记的约定。**它的两半都已被证明会变红**：把范围限制又标成 `error:` 会失败，
从某条跳过消息里去掉标记也会失败。

两个开关会改变它的行为：`-SkipMutations` 跑除变异门以外的一切；`-SelfTest` 拿一个失败
的、一个抛异常的、一个通过的函数体去考验门禁自己的 stage 函数。**一道从没被证明会变红的
防护不是防护**，而这里就是证明它的地方。

### 形式验证（`moon prove`）

`src/core` 是证明对象：`src/core/moon.pkg` 里 `proof_enabled = true`，用来启用 MoonBit
2026 的实验性形式验证；`src/core/core_proof.mbtp` 是逻辑侧——谓词 + **19 条引理**。
这 19 条引理在 2026-10-03 实测为 **21/21 个目标 VALID**（unsat），每一个都用 cvc5
机器验证过。

> **这条命令今天跑不绿，原因已量过。** `moon prove src/core --why3-config .why3.conf`
> 报 `unbound type symbol 'map'`。`src/core` 在 2026-10-08 多了一个 `IfaceSymTab`——
> 它的字段是 `Map[String, Bool]`——而工具链的证明前导库**没有 `Map` 理论**，于是生成
> 的 Why3 文件里出现 `map int bool`，`moon prove` 和 `why3` 都加载不了它。19 条引理
> 从来没碰过 `IfaceSymTab`：被证明的是**整个包**，而包里有这个类型。修法是把
> `IfaceSymTab` 移出证明范围，而那会改本包的公开 API（`@core.IfaceSymTab` 是导出的），
> 所以这是版本线上的决定，不是一个补丁的事。
>
> 还有两处 `#proof_pure` 标注是**假的**：`path_tail` 和 `unqualified` 的函数体会
> 构造 `StringBuilder`，证明器不认（错误 4207）。一处假标注就让整个文件停止证明，
> 而这两处都是 2026-10-09 加上的。它们已被移除，并且 `_verify/check_prove_contracts.ps1`
> 现在会在发布门禁里拦住任何「证明器不认的 `#proof_pure` 函数体」。

## 发布历史

逐版本的发布史——每一版改了什么、改动的实测依据是什么、以及某个结论被撤回时的更正——
见 **[CHANGELOG.zh.md](CHANGELOG.zh.md)**（[English](CHANGELOG.md)）。

## 参与开发

1. Fork 仓库并建一个特性分支。
2. 给新功能加测试。
3. 把发布门禁跑绿：

   ```bash
   powershell -NoProfile -ExecutionPolicy Bypass -File _verify\release.ps1
   ```

4. 提一个 pull request。

这道门禁不是装饰：它会跑 **87 道变异门**，每一道都改源码、要求一个测试变红、
并证明恢复是逐字节一致的。
**504** 个存活变异里，**461** 个预期被杀；其中 **384 个**还点名了必须变红的是哪个测试，
所以门禁日志说的是**哪个**测试在守着这道防线，而不只是「有东西红了」。
这三个数字都由 README 门禁**从门禁源码自己算出来**——没有被检查过的公开数字，
是会悄悄消失的。

## 许可证

MIT License。详见 [LICENSE](LICENSE)。

## 参考

- [MoonBit 语言指南](https://www.moonbitlang.com/docs/)
- [moonbitlang/core](https://mooncakes.io/docs/moonbitlang/core) —— 固定语料
- [moonbitlang/parser@0.4.3](https://mooncakes.io/docs/moonbitlang/parser@0.4.3) 与
  [moonbitlang/lexer@0.4.2](https://mooncakes.io/docs/moonbitlang/lexer@0.4.2)
  —— 工具链自己的文法，对照用
- [riantr/pyroduct](https://mooncakes.io/docs/riantr/pyroduct) —— 机器表审计的参考消费方
- [skills.mooncakes.io](https://skills.mooncakes.io) —— 已发布的 skill
- 南京大学《静态程序分析》（李樾，2026 秋季）—— 本工具的分析所依据的讲义系列；本仓库实现了
  课程自己的哪些分析，对照见 `_verify/NARRATIVE.md` §0564