代码治理

本文档定义 QED 仓库的代码治理规则。它不增加新的语义规范层，只负责把包边界、alias 入口和文档回写义务固定下来，避免代码结构长期漂移。

分层

默认依赖方向固定为：

kernel -> logic/elab -> parser -> tactics -> prover -> cmd

治理要求：

kernel 是唯一 theorem-construction boundary。
logic 只能提供 checked helper、definition/unfold、replay helper 与 theorem catalog 组织，不得新增 primitive authority。
parser 只负责文本语法、normalize、resolution 和 lowering；不得直接依赖 tactics execution object。
tactics 只负责 goal-state transformation 和 replay orchestration；不得回写 parser 语义。
prover 只做 parser/tactics/kernel 的编排与结构化诊断，不得成为新的逻辑权威。
cmd 保持最薄外层，只消费稳定 facade，不新增低层知识。

research_rewrite 位于这条依赖链之外：它是仅用于研究的原型，只依赖 kernel 和 logic，且没有任何已发布的包依赖它。cmd 是可执行包（其 moon.pkg 中为 pkgtype(kind: "executable")），因此其他包无法导入它。

若某次改动需要逆向依赖，默认视为设计问题；应优先引入中立数据结构或显式 bridge，而不是跨层直接引用。

每个包的官方 alias 入口固定为两类：

约束如下：

alias.mbt 只暴露该包生产源码真实需要的稳定符号。
alias_test.mbt 必须先镜像 alias.mbt 的生产导出，再补充 test-only imports。
alias_test.mbt 不是第二套公共 API；不得形成与生产入口不同的导出哲学。
alias 文件头注释必须说明入口适用范围和维护规则。
不得把 alias 当作无边界的下层符号转抄表。
blackbox test 引用本包符号时，须在 alias_test.mbt 中用 using @<本包> {...} 显式导入（MoonBit test_unqualified_package 规则），不得依赖隐式导入。
kernel 不依赖其他 QED 包，因此没有 alias.mbt，只有列出本包测试所用符号的 alias_test.mbt。

单个文件或模块应尽量只承担一种主职责：

以下情况应优先拆分：

本仓库当前的首批治理样式包括：

当代码改动影响以下内容时，必须同步回写文档：

默认维护顺序：

提交与 review 时至少核对：