#moonbit_static_analysis

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

#安装 / 快速上手

moon add riantr/moonbit_static_analysis@0.3.4

// 用途一：修订一段 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                # 75/75 全绿（四个 target 各 75）
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.3.4 可被任何 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

#DeepSeek Harness 插件