#moonbit_static_analysis

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

#安装 / 快速上手

moon add riantr/moonbit_static_analysis@0.4.1

// 用途一：修订一段 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 里对行号。

#包结构

src/core      Span/Severity/Lens/Family(merge_group 契约)/Frame
src/report    Report 结构与渲染（lens 并集标签、vst 框架）
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                # 86/86 全绿（四个 target 各 86）
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.1 可被任何 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、源码片段与修复建议 （同一份 ML/CI 代码本工具曾报 529 条「未使用局部」，而编译器报 8 条—— 差的那 66 倍是 struct 函数体没解析）。本工具能说「编译器做不到」的地方是 .mbti / .mbt.md / .mbtp 三类文件与跨包语义。

#DeepSeek Harness 插件