#moonbit_static_analysis

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

#0.4.7 要点

#0.4.11 —— 第一次扫外部代码：四个修复，全部来自实测

moonx riantr/moonbit_static_analysis@latest riantr/pyroduct@latest

#0.4.12 —— 包私有跨文件解析：剩余最大的一类被关掉

• 26 条涉及的 11 个名字（sieve、ridge_fit、ridge_predict、ols_core、 normal_cdf、fmt、claim_code、claim_of、phase_code、contains_state、 has_state）全部是同目录兄弟文件里的包私有顶层 fn——26/26，没有例外；
• 工具链确认语言确实允许：两文件包里一个文件调用另一个文件的私有 fn， moon check 与 moon test 都通过，跨 _test.mbt 也一样（has_state 正是这一种）。所以这 26 条全是对分析器的误报。

1. 只取深度 0。 函数体、test、extend、impl 里的绑定都在至少一层花括号 之下，永远不会被收进来。否则一个局部 let 就能让自己全包可见。
2. 名字必须是关键字后紧邻的那个 token。 let (a, b) = ... 后面跟的是 (， 什么都收不到。
3. fn Foo::new 按整体收成 Foo::new，不是 Foo——Foo 未必存在。

#0.4.17 —— 11 → 9：一条的根因是「上一版把探针写坏了」，另一条是「读到了却丢掉」

#Array::make：探针从来没调用过那个函数

#为什么是表，不是规则

#顺带证伪了 0.4.16 的一条结论

#Select：同包兄弟文件里的枚举变体

fn every_mode() -> Array[Mode] {
  [Select, Rect, Polygon, Keypoint, EditBinding]
}

#差分：933 个文件里只有 2 个文件的判定变了

#0.4.16 —— 19 → 8，其中 6 条是真阳性：先承认「对」，再修剩下的错

#跨包 const：3.0F * hz 被报成 'float' 和 'fn hz'

// snn_mbt/istdp.mbt
r: 3.0F * hz,   // hz 是 @snn_kw 的 const hz : Float

#带花括号的 suberror

#一个反向的发现：这个分析器漏报

限定名一度被过度报告（Layer::ReLU、fn hz），修完之后它们变成了 报告不足。

#改完又撤回：Byte::default / Array::make

let pixels : Array[Byte] = Array::make(total, Byte::default())

#结果

#0.4.15 —— 剩下 30 条里的 12 条：三个成因，其中一个差点把整条规则静音

#单元变体：同一文件里，带载荷的能读、不能带载荷的读不到

enum Layer {
  Conv2d(Conv2dParam)   // 能读
  ReLU                 // 报 undefined name
}

#「函数体是空的」不能当 extern 的代理

#结果

#突变脚本自己踩的第三个坑

#0.4.14 —— pyroduct 的 0 不是「对」：换四个语料，一次挖出三个真缺陷 + 一个静默错误

#还有一个不产生任何发现的缺陷

1.5 -> 1 | 0.25 -> 0 | 3.14159 -> 3

#实测过的修法，以及一条实测后撤回的修法

• 五道突变里，这三道全部存活（改回去套件照样全绿）；
• 在 933 个文件上做差分扫描，两次的报告流逐字节相同。

#结果

#顺带修掉的两个自伤

1. Get-Content -Raw 在中文 Windows 上按 GBK 解码 UTF-8，把注释里的 — 写成 鈥?，并且吞掉了后面的换行，把两行注释并成一行。现已改为按字节读、并用 SHA256 证明 restore 与运行前逐字节一致。
2. 差分脚本里 "$v_" 被 PowerShell 解析成名为 v_ 的变量（空），两次扫描 写进同一个文件、后者覆盖前者，于是「变体 A 和变体 B」变成了自己和自己比， 报出「完全一致」。现在用 ${v_}，并在比较前断言文件存在——两次读取都失败 曾经被当成「相同」。

#0.4.13 —— 最后 5 条：三种成因，其中一种是「把检查调窄」的陷阱

#第一条差点被我用一个更糟的 bug 换掉

#_ 前缀：分析器和编译器规则相反

#self 是约定参数名，不是关键字

#被突变验证挖出来的两件事

1. 突变脚本自己的过滤器匹配了 0 个测试。 两个 guard 报成 GREEN，其实 --filter 的 glob 根本没选中任何用例——一次「全绿」什么也没证明。脚本现在 断言 ran > 0，ran = 0 直接判 INVALID。
2. 一个修复没有任何测试能杀死它。 我一度让空列表字面量「采纳注解类型」， 把它静音后两个语料的发现流逐字节相同（496 / 528 条），也没有测试能杀它。 真正起作用的是 ty_assignability 那一条。测不出差别的分支不是保险，是没被测过 却长得像决策的代码——已删，并在两处注释里写明为什么删。

#0.4.10 —— 发布 0.4.9 才暴露出自检一直在遮蔽的两件事

no visible binding for 'is_coordinate'
no visible binding for 'split_coord'

let stem = if is_coordinate(p.target) {   // 226 行——if 表达式
  ...
if is_coordinate(target) {                // 411 行——if 语句

#0.4.9 —— @latest 扫描把自己的产物命名成 unknown

moonx riantr/moonbit_static_analysis@latest riantr/moonbit_static_analysis@latest --mmd-auto

MMD	riantr-moonbit_static_analysis_0.4.8_0.1.20260920_20261010T235302Z.mmd
  %% version=0.4.8

#0.4.8 —— 以 mermaid 工件为证据的三轮自检

• 第三轮的起点就是错的。 那 8 条本来准备当死代码清理。它们不是死代码——照着清理 就是删掉能跑的代码去迎合一条误报。那一轮找到的是分析器自己的缺陷。
• 插值那个修复立刻又造出两条误报：no visible binding for '1' 和 '10'， 出在 \{i + 1} 与 \{pct / 10}——标识符被允许以数字开头。只有拿真实代码再扫一遍 才会浮出来。修误报和制造误报是同一类动作，区别只在于有没有再跑一次扫描。

#安装 / 快速上手

moon add riantr/moonbit_static_analysis@0.4.17

// 用途一：修订一段 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.17 可被任何 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 插件