#moonbit_static_analysis

1. 程序代码修订：分析快速进化中的 MoonBit 语言的程序（未定义名、未用绑定、类型错配、死分支、不可达代码）；
2. 静态状态修订：为多层状态机提供通用机器表审计（src/statecheck）——被测对象调用本模块，把机器表作为纯数据喂进来。参考消费方是 riantr/pyroduct（主体／群体／社会／进化层状态机族），其 audit 包用真实机器表调用本模块做黑盒测试。

#0.4.7 要点

#安装 / 快速上手

moon add riantr/moonbit_static_analysis@0.4.7

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

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

#三鉴（结构/类型/行为）（流水线核心）

#用途一：程序代码修订（快速进化中的 MoonBit 语言）

moon run src/cli          # demo：6 个样例 × 三鉴

=== 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)

#用途二：静态状态修订（机器表 → 三鉴）

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

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

已知设计（4 条，出处层：设计使然——0.2.0 审计已验证）：
- state '无忆' is never entered: it appears only as a transition source
- state '无筹' is never entered: it appears only as a transition source
- state '无忆' is unreachable from the initial position '立位'
- state '无筹' is unreachable from the initial position '立位'

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

moon run src/cli 末尾那台 pyroduct 形状示例机器 是本模块内嵌的 8 状态玩具机 （statecheck.pyroduct_flavored()），不是 pyroduct 的真表；它带 182:12 这类 行:列，那是 state_span() 按状态名哈希出来的稳定伪 span（同一名字永远同一坐标）， 不是任何源文件的位置——别拿它去 pyroduct 里对行号。

#把扫描结果渲染成状态图（public API）

let root = /* 已解析到的源码根目录 */
let prov = @sa.provenance_for("my/module@1.2.3", root)
let text = @sa.mermaid_states(verdicts, @sa.aggregate(verdicts), prov, 8, 25)
println(scan_artifact_name(prov, root))

• 迁移标签是第一个 : 之后的全部内容，所以标签里不能再有 :——行号和消息因此放在 带引号的 state 标签里，绝不放箭头上
• MoonBit 没有运算符续行，源码里以 + 开头的行是语法错误——所以文档是一段一段 write_string 拼出来的，原因就是这个

#给产物命名：版本与扫描时间写进文件名

moonbit_static_analysis_0.4.7_0.1.20260920_20261009T155222Z.mmd
moonbitlang-core_0.1.20260920+7d59c7ec9_0.1.20260920_20261009T051925Z.mmd
tree_unknown_0.1.20260920_20261009T051511Z.mmd     # 版本没找到

moon 0.1.20260920 (914d7da 2026-09-20)

本轮更正。 上一版这一节写着「CLI 根本没法打时间戳，因为唯一的时钟在 internal 包后面」。那是错的：moonbitlang/async 把它公开重导出了 （pub using @event_loop {now}），而且 provenance_for 从 0.4.5 起就在调 @async.now()。CLI 之所以写 unknown，只是因为它被塞了一个手写的空时间戳，而没有去调 那个本来就能用的函数。

• 不省略它没能确定的东西。 版本、工具链或时钟缺失时写字面量 unknown。省掉那一段会 得到一个"看起来完整"的名字，而且四个字段时更糟：会错位——读 core_0.1.2_20261009 的人会把时间戳当成工具链版本。
• 不产出 dotfile。 以 . 开头的名字在 Linux/macOS 上 ls 根本列不出来，而没人 列得出来的产物等于没人找得回来。
• 不把文件名当记录。 同样的三个字段会以 %% 注释重复写在文档正文里，因为文件 是会被改名的，改完名之后它的名字就不再是证据了。

#从 CLI 直接写出一张图：--mmd / --mmd-auto

moonx riantr/moonbit_static_analysis@latest <target> --mmd out/scan.mmd
moonx riantr/moonbit_static_analysis@latest <target> --mmd-auto

• 要显式开，永远不是默认。 这张图天生有损：mermaid_states 按 actionable 数排序、 到自己的上限就停，并在正文里写明 %% THIS DRAWING IS A SUBSET。把图当唯一输出等于把 这句话藏起来，而且会悄悄弄坏所有 grep SUMMARY 的脚本。
• --mmd 必须带路径，自动命名另给一个 --mmd-auto。 可选值在这里是歧义的： <target> --mmd <path> 里 --mmd 后面那个裸词同样可能是第二个目标，两种读法无法区分。 与其猜、然后以 "unexpected extra argument" 失败，不如让这个值必填。
• 产物绝不落进被扫描的树里。 本模块写明的约束是只读目标的文件；往别人的源码仓库 里丢文件既违背这个承诺，也会弄脏一棵用户未必拥有的树。

MMD  _mbcore_0.1.20260920+7d59c7ec9_0.1.20260920_20261009T132547Z.mmd

#包结构

src/core      Span/Severity/Lens/Family(merge_group 契约)/Frame + Family::advice
src/report    Report 结构与渲染（lens 并集标签、vst 框架）
src/sa        扫描入口 + aggregate() + mermaid_states()（对外 library）
src/lexer     MoonBit 词法前端
src/parser    MoonBit 语法 → ast（含 .mbtx 脚本的 import 块）
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 + 示例机器审计）

#文件种类（MoonBit 工具链的其它后缀）

#验证

moon check --target all --deny-warn   # 0 错 0 警（js / native / wasm / wasm-gc）
moon test --deny-warn                # wasm 192/192；js 与 wasm-gc 139/139
moon run src/cli                     # 程序 demo + 文件种类 demo + pyroduct 形状示例机器审计

CI 只跑 --target js；上面「四个 target」是本地跑的结论，CI 不覆盖 native/wasm。

#形式验证（moon prove）

moon prove src/core --why3-config .why3.conf   # 生成 19 个 VC 并交 cvc5/alt-ergo

• 21/21 目标全部 VALID（unsat）：19 条引理 + span_at/zero_span 两个自动安全 VC。
• 已知工具链限制（均为上游问题，非本项目代码）：
  1. #proof_pure 函数体为结构体字面量时（pos/span_at/zero_span）降级为不透明逻辑符号 —— 函数体被丢弃，span 形状律在逻辑侧不可证（已由测试钉住，见 core_proof.mbtp 注释）。
  2. 捆绑 why3server（Windows 构建）丢失求解器 stdout —— why3 报 "High failure"、输出仅 .；裸 why3 ... prove CLI 同样复现。逐目标机检绕过： why3 -o <dir> -P cvc5 <mlw> 导出 SMT 后对每个文件跑 cvc5。

#发布

• mooncakes.io：moon publish（发布后 riantr/moonbit_static_analysis@0.4.7 可被任何 MoonBit 模块以 import 依赖；src/cli 附带 SKILL.md，上架 skills.mooncakes.io）。
• Gitee / GitHub：git push 双推；tag 与 moon.mod 版本号保持一致。

#分析其他项目（不引入本项目）

moonx riantr/moonbit_static_analysis@latest riantr/moonbit_doubleML@latest

#输出说的是「我读懂了什么」，不是「我数出多少条」

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

• PARSED 是头号指标。 工具链的前端只覆盖 MoonBit 的一个子集，读不懂的部分 报出来的「发现」量的是工具的盲区，不是你的代码。
• 半读懂的文件仍然值得读。 解析器记录它真正读不下去的第一行；那之前的 发现照常报（PARTIAL），之后的计入 unreliable 且从不展示——它们来自一棵 已经错了的树，摆出来等于把这个工具最初的毛病又犯一遍。
• 跳过声明不算读不懂。 「不分析 test 块」不会移动这条边界，因为块之后的 代码照样读得通。
• actionable 不含告知。 「这种声明不分析」不是你的代码有缺陷——不然自检 会报「发现 92 个问题」而真实缺陷是 0。
• 未解析文件按原因分组而不是一行一个，带示例路径。
• actionable + notices + unreliable = total，这一行打印里直接断言成立。withheld 也印在旁边，但是 unreliable 的子集（无前置发现的 PARTIAL 文件的尾部发现），不计入等式。

与 moon check 的关系要说清楚：在 .mbt 上，本工具不与工具链的编译器 竞争——moon check 有真正的解析器和约 90 条内建告警，覆盖率恒为 100%， 实测 2.3 秒 / 128 条，且每条都带 file:line:col、源码片段与修复建议。本工具的 .mbt 前端只读一个子集：在 moonbitlang/core 上，882 个 .mbt 解析了 173 个（19.6%），而 .mbti 与 .mbt.md 是 100%。原先最大的单一原因 方法调用在 AST 里根本没有位置——ECall 的被调名是 String，所以 m.set(k, v) 无处安放，解析就停在那里——本轮已修（新增 EMethodCall 节点， 三个 lens 都接上），该阻塞从 34 降到 0。这才是诚实的头条数字，也是 PARSED 要印在第一行的原因。本工具能说「编译器做不到」的地方是 .mbti / .mbt.md / .mbtp 三类文件与跨包语义。

早先版本在同一份 ML/CI 代码上报过 529 条「未使用局部」，而编译器报 8 条。 那不是两种意见，而是没解析的 struct 函数体里那些字段被当成了没被读的绑定。 现在它报不出来了——被前端截断的函数会整函数退出未使用局部 / 未使用参数 / 参数被改写这三族审计，因为「从未被读」是关于整个函数的结论，半个函数 支撑不了这个结论。仅此一项修复就把 moonbitlang/core 从 270 条 actionable 降到 147 条，把本仓库从 11 条降到 0 条。

再往下读，同一条原则还适用于模块帧，也适用于一类解析器从没学过怎么解析的 名字：前端没读完的文件，模块帧是可证不完整的，所以那里「找不到可见绑定」 什么也不能证明；而 Type::member 路径（@debug.Repr::opaque_(v)）是成员引用 不是绑定，跟字段名、方法名本来的处理一致。再把 extern "c" fn 当成声明建模 （原先整条跳过，名字就丢了，于是每个 extern 函数的调用点都报未绑定），补上数值 字面量与 enum 构造器，moonbitlang/core 从 270 条降到 49 条，undefined name 从 64 条降到 17 条（发布 0.4.6 时误记为 0，与该版扫描产物不符，后按实测勘正）， 本仓库仍是 0；0.4.7 再把 .mbti 审计的未知类型检查接到模块级接口符号表上， 其余 13 条误报清零，降到 36。

moonbitlang/core	文件	解析	actionable	未定义名
0.4.5	1029	305	270	64
0.4.6	1029	320	49	17
0.4.7	1029	320	36	17

#DeepSeek Harness 插件