验证

本仓库将快速的开发检查与有限、可复现的符合性结论区分开来。通过某个语料只能证明所声明的格式、运算、舍入模式、目标和 fixture 版本。本指南列出各个关卡、每项已发布结论的覆盖范围，以及如何复现和排查结果。

验证层级

层	命令	用途
文档	just docs	tools/doc_quality.py（页面覆盖、API 快照、链接与锚点、版本与 GDA 相关声明、各包的 README.mbt.md 文件），然后运行 src/doc_examples 测试
格式	just fmt	MoonBit 格式化工具
PR	just pr [jobs]	格式检查、文档、带 --deny-warn 的原生检查与测试、Python 工具测试，以及四套已提交的冒烟语料
IEEE 十进制	just gate decimal [jobs]	已提交的 decimal32/64/128 DPD 与 BID 向量，在 native、Wasm、Wasm-GC 和 JavaScript 上运行
GDA 十进制	just gate decimal_gda [jobs]	包测试与前端测试，然后是固定版本的 official 与 official0 .decTest 语料
二进制	just gate binary [jobs]	固定版本的 TestFloat level-1 矩阵与 MPFR 见证数据
区间	just gate interval [jobs]	所有严格 ITF1788 阶段
完整	just ci [jobs]	在全部四个目标上进行格式检查、文档、--deny-warn 检查与测试，生成接口，并运行所有符合性关卡

先运行范围最窄的相关检查，发布前再逐步扩大范围。翻译目录由 lunadoc check 单独检查，doc/ 下的每次改动都会触发 Docs 工作流运行该检查。

持续集成

• ci.yml 对每个拉取请求以及每次推送到 main 运行 just pr。
• nightly.yml 每晚以及按需将 quick、decimal、decimal_gda、binary 与 interval 的 just gate 作为并行任务运行。它按清单哈希缓存以 SHA-256 固定的上游语料（下载后仍会校验哈希），并将每个 summary.json 作为产物上传，从而在维护者的机器之外复现已发布的结果。
• docs.yml 运行组织的 lunadoc check 工作流。
• publish.yml 执行构建，运行文档关卡、格式检查、全目标 --deny-warn 检查和测试，然后发布到 mooncakes。

共享的符合性运行器

所有 suite 使用同一个 dispatcher：

just conformance <build|run|smoke|plan|fetch> \
  <decimal|decimal_gda|binary|interval> [options]

decimal 是独立的 IEEE 十进制语料；decimal_gda 是 GDA .decTest 语料；binary 组合了 TestFloat 与 MPFR 数据源；interval 使用 ITF1788。

smoke 运行已提交的 fixture，不下载任何内容。plan 打印确定性的任务列表。fetch 先校验固定的来源，再将被忽略的数据安装到 .tmp/ 之下。run 执行所选的测试套件。各后端特有的过滤器、阶段、目标、严格模式、分片以及 JSON 输出见 testdata/bin_float/README.md、testdata/decimal/README.md 与 testdata/interval/README.md。

已发布的结论

• GDA。 144 个文件的 official 语料中全部 64,986 条合法可执行标量行均通过，official0 的全部 16,124 条合法行也均通过。141 条 # 占位行或非标量行属于诊断性排除，而非未支持的合法行为。
• 二进制。 TestFloat level-1 矩阵（种子 1）在 binary16/32/64/128 上共有 468 个任务、254,227,872 个向量：其中加、减、乘、除和平方根占 7,461,360 个，其余 246,766,512 个用于 IEEE 运算 mulAdd（占其中 245,329,920 个）、rem、roundToInt、到 32 位与 64 位有符号及无符号整数的转换，以及比较运算 eq、le、lt、eq_signaling、le_quiet 和 lt_quiet。对于使用舍入方向的运算，测试覆盖五种舍入方向；算术运算和 mulAdd 覆盖两种微小性模式；roundToInt 和各转换覆盖精确与不精确两种变体。无效的整数转换只比较标志，因为在 API 返回 None 的地方，SoftFloat 返回的是平台相关的哨兵值。MPFR 部分另外加入了固定版本平方根数据中的 1,055 条可执行行，以及 2,088 个以哈希固定的见证数据，覆盖 29 种初等运算，精度为 binary32/64/128，涵盖全部六种 BinaryRoundingMode 值。
• IEEE 十进制。 已提交的 decimal32/64/128 DPD 与 BID fixture 覆盖编码、特殊值、标志、核心算术以及全部 1,024 个 DPD declet，在 native、Wasm、Wasm-GC 和 JavaScript 上运行；LLVM 不在此关卡范围内。一份已提交的初等函数判定数据另外加入了 2,784 行，由 768 位 MPFR 包络在全部八种十进制舍入模式下计算得到。
• 区间。 严格 ITF1788 阶段通过了全部 4,656/4,656 个选定用例：集合、关系、数值观测、消去、算术、初等核心、指数与对数、一般幂、三角函数、双曲函数、反三角函数、atan2、FMA、整数幂和极值。逆运算仍不受支持。

just pr 运行的已提交冒烟 fixture 是上述语料的子集：例如二进制冒烟测试有 2,451 行（240 个 TestFloat 向量、3 个平方根见证、120 个整数幂见证以及 2,088 个初等函数见证）。

这些都是有限的结论。它们并不意味着覆盖 IEEE 754 或 IEEE 1788 的每一个运算、任意的资源规模、每一种 NaN 载荷策略，或将来的语料版本。各包的二进制、IEEE 十进制、GDA和区间符合性页面给出了确切的矩阵及其排除项。

可复现性

外部产物在各语料清单（testdata/*/corpora.json）中按版本和 SHA-256 固定。构建使用以后端命名的输出和隔离的目标目录，使并行任务不会相互覆盖。分片选取确定性的用例索引，合并后的汇总保留精确的总数和失败 ID。大型生成 fixture 被拆分到多个文件中（IEEE 十进制公开 API fixture 每个文件写入 400 个测试），以便每种工具链都能编译。

MoonBit 前端负责解析并执行数值行。Python 负责编排下载、任务规划、子进程、目标选择和结果汇总。可选的判定实现（oracle）绝不会被悄悄替换为更弱的实现；缺失的前提条件会被明确报告。

性能证据与语义符合性相互独立。基准测试清单固定了基线源码、依赖、工具链、目标、调度、样本数和离散度上限，且性能阈值从不改变正确性。参见性能审计以及各包的性能页面。

失败排查

1. 用能复现问题的最小用例、ID 过滤器、阶段或分片重新运行失败的后端。
2. 区分解析诊断、不受支持的用例、旧有分类、可执行结果不匹配以及基础设施故障。
3. 记录期望值、实际值、标志、上下文、目标、语料版本和命令。
4. 运行对应的白盒包测试，以判断缺陷位于解析、算术、交换格式还是汇总环节。
5. 修复后，依次运行针对性用例、已提交的冒烟 fixture、后端关卡，最后运行 just pr 或 just ci。

不得通过降低 strict support、丢弃 flags 或改写分母让失败 gate 变绿。

发布关卡

发布前：

1. 使 moon.mod、README.md、手册与 CHANGELOG.md 保持一致；
2. 运行 just docs、lunadoc check，并检查生成接口的差异；
3. 迭代期间运行 just pr；
4. 对候选发布版本运行 just ci；
5. 通过仓库的 publish.yml GitHub Actions 工作流发布。

本地 moon publish 不是 Luna-Flow 的发布途径，因为组织的凭据由工作流提供。