moonspace

thy1016/moonspace 是一个用 MoonBit 编写的 Agent 解空间基础设施库： 以合同先行、门校验强制为核心——空间合同（TOML）既可以由人编写， 也可以由 LLM 起草；无论来源如何，必须通过解析、阳集闭合与可达性 三类门校验之后才会被构造成可执行的状态机。库本身端口中立：不绑定 任何具体的 LLM 供方、存储引擎或执行环境。

仓库另附两份架构文档：spec.md（项目级决策锚点）与 const.md（红线裁定簿）。

特性

• 三沙箱架构：解空间（合法状态/事件/effect 的 Mealy 纯转移）、 运行空间（副作用执行边界：Port 权限/资源/超时/审计）与验证环境 （纯函数模型 + 属性 + 不变量）三面分离，依赖单向不回穿。
• 合同驱动生成：gen/ 读取 domain/*.toml 合同对，生成表驱动 状态机、CPS 单层 dispatch、可达性剪枝、属性测试骨架与 handler stub 模板；生成器零业务词——semantics 封闭词表是唯一可硬编码面。
• 组合代数：parallel（张量积，自动做可达性剪枝）/ series（串联 桥接）/ feedback（显式 LoopBack 事件回送，守卫必填）三算子。
• typed 产物面：cmd/ 再生入口从合同生成 typed 枚举与 step 函数， 入库产物受逐字节回归比对（golden）与双实现等价校验（parity）双门 约束，漂移即红。
• 双后端可用：库面（space/ gen/ 主面、runtime/ verify/ out/ 主面）后端中立，wasm-gc 与 native 双双通过编译检查；浏览器 嵌入形态为库面编 wasm 产物、宿主以 JS 实现 EffectHandler。

架构

包	沙箱	职责	依赖
space/	EffectSpace Sandbox（解空间）	合法状态/事件/effect 词表与机器件	无
runtime/	Runtime Sandbox（运行空间）	副作用执行边界：Port 权限/资源/超时/审计	space
verify/	Verification Sandbox（验证环境）	纯函数模型 + 属性 + 不变量，零真实 Port	space
gen/	解空间生成器	读合同产表驱动状态机 + dispatch + 测试骨架	toml + space

外圈三件：out/ 为 typed 产物面（纯生成禁手写 + stubs.mbt 手写 填空区，两区永不拼接）；cmd/ 为合同再生入口；examples/ 为示例 loop 全栈自证。

安装

确保环境中已安装 MoonBit 工具链。模块发布至 mooncakes 后可通过 moon add thy1016/moonspace 引入；当前亦可以源码依赖方式（workspace 成员或 git 依赖）使用。

快速上手

在仓库根目录：

moon run examples --target native                                # 示例 loop：合同 → 门 → 大 loop，零 LLM
moon test gen runtime space out verify --target native           # 本模块全部门件
moon run cmd --target native                                     # 合同再生（修改 domain/*.toml 后）

示例 loop 输出：

合同 hello_loop_space 过门：态 3 / 事件 3 / 效应 1 / 转移 3
终局: Done / Completed / rounds=2
  r1: DoIt → WorkDone (completed)
槽位 result_summary = did it

空间合同（domain/）

• retrieval_base.toml / retrieval_domain.toml —— 演示空间一
• reasoning_base.toml / reasoning_domain.toml —— 演示空间二
• composition.toml —— 组合合同：parallel / series / feedback 三算子

合同采用骨架/行为分离的文件对组织：*_base.toml 为词表骨架 （声明态/事件/效应/槽位，只选用不发明）；*_domain.toml 为转移行为 （from/on/to/effect/args 转移表，含 assign_from 糖——效应回执 字段落入 ctx 槽位）。文件对按 meta.name 配对。

宿主装配词表（如 agent 工作流、任务相位机等）住宿主自己的仓库 domain/，不入本仓产物面——新消费者的接入路径 = 自带合同对 + stub 填空，零生成器代码改动。

持久合同规则

• 新键可选：解析器提供缺省，不因键缺席报错；
• 未知键忽略：旧合同文件对新版生成器保持可读；
• 删键/改义：与手写合同文件的迁移同笔完成；
• 字段契约的可执行镜像为 gen/contract.mbt；typed 产物与手写合同 的漂移由回归门拦停。

设计不变量

• 转移为纯函数；effect 仅产出、由 handler 解释执行；持久化/权限/ 审计留在 Port 层；
• CPS 单层 continuation；handler 幂等或可重试；回调带超时与取消；
• feedback 回送为显式 LoopBack 事件，禁止任意 continuation 捕获；
• 守卫谓词只判解空间数据条件；工具许可等外部语义留 handler 域内 哨兵面，判否以哨兵事件回灌续轮；
• 生成器零业务词：semantics 封闭词表 （query/command/commit/rollback/stop）是唯一可硬编码面。

构建说明

• moon run / moon test 缺省使用 wasm 构建计划；本仓的文件 系统吃用面（对照门测试件、cmd/ 再生入口）以 native 为门件目标， 因此 native 跑法必须显式携带 --target native，否则相应门件会被 静默跳过。
• 库面后端中立：moon check --target wasm-gc 全绿；浏览器嵌入形态 依赖 moonbitlang/async 的 wasm 入口补齐，当前可执行面暂以 native 为准。
• 作为多模块 workspace 成员使用时，在成员目录内直接运行 moon test 会构建整个 workspace；建议按包过滤，或以独立 clone 形式开发。

宿主嵌入（引擎形态）

moonspace 是被嵌入的确定性内核，宿主集合开放——不是宿主跑在 moonspace 里，而是 moonspace 作为引擎库跑在宿主里（同一二进制静态 链接：loop 骨架在 moonspace，效应回调由宿主 handler 实现）：

• agent 宿主：LLM 调用纯函数化、多级校验门与完整 agent loop （已落地；装配词表住宿主仓）；
• 数据管线宿主：domain/ 的 retrieval/reasoning 合同对 （BM25Search / VectorSearch / LLMCall 词表）即检索管线速写， handler 真身与预算面待接；
• 浏览器宿主（规划中）：库面编 wasm 产物 + 宿主 JS 实现 EffectHandler，真效应留在宿主侧。

嵌入身份为编排面而非存储面——数据访问始终走宿主自己的 port， moonspace 不承担数据访问层职责。

许可证

本项目以 木兰宽松许可证第 2 版（Mulan PSL v2） 授权，详见 LICENSE。

仓库

• 本仓：https://gitlink.org.cn/thy7/mbt.space