架构

floating 由若干显式数值域组成，外围是轻量的组合层、解析层和验证层。核心原则是：数值语义保持纯粹且显式，而文件、进程、语料和基准测试都留在仓库边缘。本指南将各个包对应到这些层，追踪一次运算穿过数值核心的全过程，并列出每一层都遵守的不变量。

分层图

层	包	职责
共享词汇	`def`	`Sign`、`PartialOrder`、`Floating` trait、谓词，以及重新导出的 `arithmetic` 类型
标量域	`bin_float`, `decimal`, `decimal_gda`	二进制、IEEE 十进制和 GDA 十进制值，及其上下文与状态
区间域	`ball_float`	裸区间与带装饰的外向舍入实数包络
Checked 组合	`bin_float_checked`, `decimal_checked`, `decimal_gda_checked`, `ball_float_checked`	保留各数值域错误、标志或陷阱状态的流水线
语义投影	`semantic`	精确的、与表示无关的观察
语法	`numeric_expr`	source span、literal、primitive call、callback evaluation
格式前端	`frontend/gda_expr`, `frontend/itl_expr`, `frontend/mpfr_expr`, `frontend/testfloat_expr`	解析一种外部语料语法并执行带类型的用例
运行适配	`internal`、`internal/conformance`、`internal/runner_cli`、`cli` 和 `cli/*`	共享辅助函数、汇总、分片、文件、JSON 与文本输出、退出状态
证据	`consistency`、`doc_examples`、`bench` 和 `bench/*`、`tools/`、`testdata/`	跨包定律、文档示例、基准测试、符合性测试编排

包边界由 moon.pkg 决定；包内的文件只用于组织实现，不会创建命名空间。依赖关系自上而下：每个数值包都依赖 def 和 internal，ball_float 构建在 bin_float 之上，decimal 和 decimal_gda 借助 bin_float 与 ball_float 实现其经认证的初等函数，checked 包封装各自的数值域，而任何数值部分都不依赖前端、CLI 或基准测试。

标准边界

不存在通用的“浮点值”。每个标准都保有自己的可观察状态：

数值域	规范模型	操作结果
`bin_float`	任意精度的 IEEE 754-2019 二进制算术，binary16/32/64/128 交换格式	值 + `BinaryFlags`
`decimal`	IEEE 754-2019 十进制算术，decimal32/64/128 DPD 与 BID 交换格式	值 + `DecimalFlags`
`decimal_gda`	General Decimal Arithmetic Specification 1.70，标量运算	含 raised flags、sticky next context、可选 trap 的 `GdaOutcome`
`ball_float`	IEEE 1788-2015 裸区间与带装饰区间，限于声明的运算集合	包络、装饰（decoration）或 NaI，可选的 `BallFlags`

这种分离避免了有损转换，例如把 GDA 陷阱当作 IEEE 标志，把 IEEE 无穷大当作通用错误，或把 Empty、Entire 与 NaI 当作可互换的区间失败。数值语义定义了上述每一种状态。

数值核心流水线

所有标量核心都采用同一种分解方式，尽管它们的表示和标准各不相同：

immutable operand value(s) + explicit context
  -> special-value and domain classification
  -> exact coefficient computation, or a certified enclosure
  -> one domain-owned finalization (rounding, exponent range, status)
  -> public value + explicit status

BinFloat 存储类别、符号、不含末尾零比特的非负二进制系数、指数、精度以及 NaN 状态（signaling 位与 payload）。Decimal 与 GDA Decimal 各自存储符号、由包自身管理的以 $10^9$ 为基数的系数、作为量子（quantum）的指数、精度以及特殊状态。BallFloat 存储两个 BinFloat 端点、精度以及 Empty 标记；BallFloatDecorated 在此基础上增加装饰，但不改变裸区间的表示。

最终化（finalization）是语义防火墙。计算内核可以计算精确的和、积、商、根或保护位与粘滞位，但只有最终化器决定舍入后的值、同值类（cohort）、标志、陷阱、装饰以及区间端点的方向。它还对首位比特强制实施二进制实现的指数范围 $[1 - 2^{30},\ 2^{30} - 1]$ ：超出该范围的结果会按舍入方向被归类为上溢或下溢，而不是以饱和指数存储。

精确值极其庞大的运算从不将其实际展开。相距很远的加数会折叠为一个粘滞位；IEEE 余数运算通过对 $2^k$ 平方再相乘，将巨大的被除数对 $2y$ 取模来约化；舍入到整数时通过移位拆分系数；区间端点求和时，若某个加数比另一个低超过 $\max(65536, p)$ 比特，则将其舍弃为一个定向粘滞项。每种捷径都恰好向最终化器提供与完整计算相同的舍入位和粘滞信息。

算法选择

大整数内核使用分阶段选择器，而非单一算法：

size + shape + target + proof preconditions
  -> inline / schoolbook / Comba
  -> Karatsuba
  -> Toom-3
  -> NTT + exact CRT reconstruction
  -> exact fallback if an advanced precondition fails

除法同样会在目标测量结果支持的情况下，从字除法和 Knuth 算法 D 过渡到 Burnikel–Ziegler 算法与倒数 Newton 迭代。稀疏和不平衡的操作数有各自的路径，因为仅按较长长度选择的算法，在填充上的浪费可能超过其渐近意义上的节省。

切换点是私有的、特定于目标平台的策略。它们通过 Maremark 基准测试层次（bench/*）在稠密、稀疏、平方、平衡和不平衡数据上测量，边界测试则在每个阈值之下、之上以及恰好处比较精确结果。因此 Native、LLVM、Wasm、Wasm-GC 和 JavaScript 可以选择不同的算法，但必须返回相同的公开结果。

经认证的初等函数

初等函数（指数、对数、幂、根、三角函数、双曲函数及其反函数）在二进制、十进制和区间三套实现中遵循同一份证明契约，采用 Ziv 策略的风格：¹1 A. Ziv，“Fast evaluation of elementary mathematical functions with correctly rounded last bit”，ACM TOMS 17(3)，1991。Muller 等，Handbook of Floating-Point Arithmetic，第 2 版，2018，第 10 章讨论了这一循环所解决的制表者困境（table-maker’s dilemma）。

在任何细化之前，先根据结果 $\log_2$ 的认证界判定那些必然超出上下文范围的结果（上溢、下溢）。
在工作精度 $w = p + 64$ 下，计算精确值的定向下包络与上包络 $[\ell, h]$ 。
将两个端点舍入到目标精度。由于舍入是单调的，若 $\operatorname{rnd}(\ell) = \operatorname{rnd}(h)$ 且标志相同，则 $[\ell, h]$ 中的每个值（包括精确值）都会舍入到该结果。
否则将 $w$ 增加 $\max(32, \lfloor w/2 \rfloor)$ 并重复，至多 12 次。
如果所有尝试都无法达成一致，try_* 函数返回一个 CertificationFailure，其中包含阶段、原因、精度、工作精度和尝试次数；非 try 函数则返回一个有定义的无效结果（在二进制中为带 invalid operation 的静默 NaN），且从不中止。

bin_float 负责标量二进数（dyadic）证书。ball_float 将其提升到端点、临界点、极点和定义域边界上。decimal 和 decimal_gda 将精确的十进制输入转换为定向的二进数界，运行二进制证书，再通过精确整数算术把认证后的端点转换回来；远超十进制范围的端点会被替换为舍入结果相同的代表值，因此不会展开任何巨大的十进制数。全函数形式的区间函数可以放宽到 $[-1, 1]$ 或 Entire 之类的安全集合，而其 checked 形式会暴露失败。任何路径都不会用宿主的 Double 近似值来替代。

十进制文本转换

BinFloat::from_string_ctx 和 to_decimal_string_ctx 对任意精度和指数都是正确舍入的，且在 $k$ 极大时不会展开 $10^{k}$ 。解析时先根据对数估计判定必然的上溢或下溢；对较小的指数，直接舍入精确有理数 $D \cdot 10^{k}$ ；对较大的指数，则用定向的十的幂包络 $D \cdot 10^{k}$ ，并不断增大工作精度直到两端舍入结果一致——由于此处不可能出现平局，该过程必然终止。格式化时先由二进制估计求出首位十进制指数，再用定向的十的幂加以修正；to_shortest_string_ctx 对数字位数做二分搜索，这是成立的，因为回读结果关于位数是单调的。

上下文与状态的流动

任何数值包都不依赖环境中的舍入模式。

二进制和 IEEE 十进制上下文是不可变的输入；标志是显式输出，由调用者自行 combine。
decimal_gda 返回一个新的上下文，其状态包含已触发的标志，然后按固定优先级至多选择一个陷阱。
BallContext 确定端点精度和指数界，并返回 BallFlags。
BinFloat、Decimal 和 GDA Decimal 实现了 Luna-Flow/arithmetic 的 contextual trait（AddContextual、…、ExpContextual），因此泛型代码可以在同一个 ArithmeticContext 下运行这三者；BinaryContext::from_arithmetic_context 及其十进制对应函数会携带该上下文的精度、舍入方式、指数界和 clamp。
BinFloatResult 和 BallFloatResult 保留第一个 ArithmeticError。
DecimalChecked 保留有定义的 IEEE 结果，累积标志，并单独保存认证错误。
GdaDecimalChecked 串联传递单一结果，在遇到 Trapped 时停止，且只能通过显式的 resume_defined 转换恢复。

这些包装器只是组合已有语义；它们自身不添加任何算术，也从不合并互不兼容的状态通道。

公开接口与 trait 方法

每个包生成的 pkg.generated.mbti 是判断哪些内容公开的权威依据。自 MoonBit 0.10 起，trait 实现中的方法不再自动提升为该类型的方法：像 BinFloat::to_string、Decimal::add_contextual 或 BinFloat::sqrt_checked 这样的方法之所以能用点语法调用，只是因为包用 pub extend 声明了它，随后 .mbti 会将其列为 pub fn Type::name。未以这种方式列出的 trait 方法仍可通过 trait 访问（例如基于 Floating 的 @def.is_finite(x)），但不能写作 x.method()。

解析与执行

numeric_expr 保存语法数据并提供后序回调求值。它不执行任何 IO，也不选择数值后端。

每个 frontend/* 包负责一种外部语法：

gda_expr 解析 .decTest 指令与用例，并执行 GDA 结果；
testfloat_expr 解析 Berkeley TestFloat 向量，并绑定格式、运算、舍入、微小性（tininess）和精确性；
mpfr_expr 解析固定版本的 MPFR 平方根、整数幂和初等函数见证数据；
itl_expr 解析 ITF1788 区间测试行，并对声明的支持集合进行分类。

前端返回带类型的汇总。cli 包在 internal/conformance（分片、用例处置、汇总）和 internal/runner_cli（选项、文件、JSON）之上，负责文件、过滤、分片、渲染和退出码。tools/ 下的 Python 工具负责获取经校验和固定的数据、规划任务、运行隔离的目标平台与进程并汇总结果；它们从不替代 MoonBit 实现。

稳定性边界

应用接口包括 def、四个数值包和四个 checked 包装器。semantic 和 numeric_expr 是暂定的集成接口。前端之所以公开，是为了让仓库中的运行器能够组合它们，但其兼容性承诺仅限于声明的语料。

internal 与 internal/*、cli 与 cli/*、bench 与 bench/*、consistency 以及 doc_examples 属于实现与验证基础设施。某个符号出现在 pkg.generated.mbti 中，并不意味着它成为长期的应用契约；依赖它之前请先阅读该包的设计页面。

不变量

值的符号独立于其非负系数。
有限二进制值的规范化只移除因子 2。
十进制解析会保留量子（quantum），直到显式调用规范化或约简运算。
上下文最终化是唯一对有界结果进行舍入并决定状态的地方。
区间下端点向 $-\infty$ 舍入，上端点向 $+\infty$ 舍入。
Empty、Entire、NaI、NaN、带符号零和无穷大都保持为显式状态。
有限结果的指数绝不会超出实现范围。
快速路径与回退路径不能改变公开的值或状态。
符合性汇总对所选用例构成划分，且分片是确定性的。
IO、下载、进程状态和并行调度都留在工具链中。

扩展规则

把行为添加到拥有其语义的包中。在创建总括性的 trait 之前，先复用 Luna-Flow/arithmetic 和 Luna-Flow/luna-generic 的能力 trait。保持内核私有、上下文与状态显式；除非外部格式本身是稳定的交换契约，否则其解析应放在数值类型之外。当新的 trait 方法属于该类型的公开接口时，用 pub extend 将其提升为点语法可调用的方法。

扩展符合性测试范围需要协同修改解析器、执行器、支持分类、CLI 模式、语料清单、测试、生成的接口以及文档。能解析一个新运算并不等于支持它，除非严格执行具有明确定义的比较方式和可复现的证据；参见验证。

A. Ziv，“Fast evaluation of elementary mathematical functions with correctly rounded last bit”，ACM TOMS 17(3)，1991。Muller 等，Handbook of Floating-Point Arithmetic，第 2 版，2018，第 10 章讨论了这一循环所解决的制表者困境（table-maker’s dilemma）。 ↩

架构

分层图