数值函数的形式化验证与参考实现：想法、评估与约束
综合自
idea/中的多份讨论：[[PureLibm-rs.md]] 的项目设计、[[项目诊断.md]] 的项目 B 评估与手工艺候选分析、[[Rust科学计算生态调研.md]] 的 LLVM/浮点约束章节、[[项目选择判据-双视角.md]] 的判据框架、[[个人项目选择规则.md]] 的数学库规则。整理日期：2026年6月
〇、更新后的目标定位（基于 PureLibm-rs 设计）
参考 [[PureLibm-rs.md]] 的设计方案。
PureLibm-rs 是一个以可读性和正确性为首要目标的正确舍入（correctly rounded）数学库，使用 Rust 编写。
四项核心原则
| # | 原则 | 含义 |
|---|---|---|
| 1 | 参考实现 | 代码贴近算法的数学表达形式。不做混淆性的位优化。优先使用语义化操作和具名 helper 而非魔法常量。目标读者是"想理解算法的人"，不只是"想跑结果的人" |
| 2 | 详细文档 | 每个函数带完整的算法描述（特殊值处理 → range reduction → 多项式逼近 → reconstruction）、交叉引用（论文、CORE-MATH 源码行、标准文档）、系数来源标注 |
| 3 | 魔术参数均有出处 | 每个魔法常数标注生成脚本（Sollya/Gappa）、生成命令、脚本路径。脚本放在 coeff/ 目录下，有 Sollya 环境即可复现 |
| 4 | 完备的测试 | 五级验证体系：L0 类型系统 + lint → L1 穷举/随机/边界测试 + 高精度 oracle → L2 Kani bounded model checking → L3 Sollya/Gappa 证明 → L4 Coq/Flocq 完整证明 |
与之前"形式化验证数学库"想法的关系
之前的想法聚焦在验证（证明一个已有实现的正确性）。PureLibm-rs 的设计将范围扩展为先做参考实现，再做验证：
- 实现本身是可读的、像论文公式的代码（手工艺的"手表匠"体验）
- 验证嵌入实现的全流程——每个阶段的保证强度递进
- 文档和系数追溯本身就是"领域知识结构化"的产出
这对"形式化验证作为项目"的评估产生了关键影响： 之前认为这个项目在手工艺维度上不好（证明搜索反心流），但 PureLibm-rs 的模式将**"实现 + 文档 + 测试工程"作为手艺活的主体**，形式化验证作为渐进的增强层——实现和工程测试在你可预测推进的那一侧，形式化证明在"偶尔突破"那一侧。
一、核心问题
目标： 构建一个可读、可验证、正确舍入的数学库参考实现——代码本身是审美对象，文档让魔术参数可追溯，验证体系是渐进的分层保证。
动机：
- AI 让代码生成趋近免费 → 验证需求随之爆发。"可读的参考实现"本身就是 AI 时代的高价值资产（规格优于代码）
- 数值计算正确性验证是 PSE/科学计算的核心痛点
- 形式化验证是 AI 最不擅长的硬骨头之一（≥ 5 年窗口期）
- 已有经验基础：C/F77 数学库维护经验、PureLibm.jl 的可读化中文文档实践
关键前提： 在动手之前，需要理解两件事：
- PureLibm-rs 模式如何改变了"形式化验证数学库"的项目体验——实现 + 文档 + 工程测试作为手艺主体，形式化证明作为增强
- 目标语言（Rust/LLVM）对浮点运算的底层约束——这决定了"能证明什么"和"在什么假设下证明"
二、项目评估：AI 辅助形式化验证数学库
2.1 战略价值视角
以下来自项目诊断初评（AI 时代竞争力角度）。
| 判据 | 结果 |
|---|---|
| 产出属性 | 形式化规格 + 证明 + 验证方法论 → 纯判断型资产 |
| AI 替代期限 | ≥ 5 年，形式化验证的 proof engineering 是 AI 最不擅长的硬骨头 → 通过 |
| 裁员测试 | 代码可擦除重写，但证明、规格、方法论不会消失 → 通过 |
| AI 时代需求趋势 | 显著增强 —— AI 生成的数值代码越多，验证需求越大 |
潜在可积累资产：
| 资产类型 | 不可替代性 |
|---|---|
| 形式化规格（函数的正确性定义） | ✅ 核心护城河 |
| 证明库（已完成的证明可被引用） | ✅ 判断型资产 |
| AI 辅助验证的方法论/工作流 | ✅ 知识型资产（"最后一公里"经验模式化） |
| 测试集/反例库 | ✅ 边界 case 积累 |
个人匹配度：
- ✅ 数学库实现经验（维护过 C/F77 数学库），理解数值计算陷阱
- ✅ ChemE 领域数值计算需求是独特应用视角
- ✅ 即使验证不成，方法论笔记本身就有价值
- ⚠️ 与毕业/研究主线无直接关联 → P2（允许启动，但非最高优先级）
关键风险： 形式化验证 + 数学库，两个都是深坑，必须设边界防无限考古。
2.2 手工艺（Craft）视角重评
以下来自后续的手工艺视角重评。
手工艺项目的评估标准：
| 维度 | 好 | 差 |
|---|---|---|
| 心流潜力 | 重复但有技巧，能进入心流 | 高风险阻塞（卡一个问题一整天） |
| 工作单元 | 自包含，做完一个是一个 | 互相依赖，必须整体推进 |
| 进度可见 | 做一点就能看到结果 | 长期看不到进展 |
| 深度 | 可以深挖，但不强制 | 浅尝辄止或必须深挖 |
| 审美回报 | 结果本身就是审美对象 | 只有跑通/没跑通两种状态 |
| 维护负担 | 产出静止，不需要持续维护 | 依赖上游，版本漂移 |
| AI 关系 | AI 可辅助也可不用，不影响体验 | AI 替代了核心乐趣 |
形式化验证数学库按上述标准重评：
| 维度 | 评价 | 说明 |
|---|---|---|
| 心流潜力 | ⚠️ 中偏低 | 证明搜索经常卡死——一个 lemma 卡几小时是常态。不是"重复有技巧"，是"困在迷宫里"。心流需要的是可预测的挑战，证明不是 |
| 工作单元 | ✅ 好 | 每个函数自包含 |
| 进度可见 | ❌ 差 | 典型困境：3 小时看起来什么都没产出。要么证明通过了（瞬间），要么卡着（很久） |
| 深度 | ✅ 好 | 无限深 |
| 审美回报 | ⚠️ 中 | 证明通过的瞬间有满足感，但证明本身不是审美对象（除非你是逻辑学家） |
| 维护负担 | ✅ 低 | 证明不需要维护 |
| AI 关系 | ⚠️ 微妙 | AI 削弱了这个项目的核心乐趣。前 AI 时代手工实现数学库 + 形式化验证是完整的手工艺体验；现在 AI 能生成代码，只剩下证明部分，而证明恰好是卡住/阻塞风险最高的部分 |
重评结论：作为手工艺项目，形式化验证数学库有结构性缺陷。
核心问题不是做不做得好，而是证明搜索的随机阻塞特性天然反心流。它更像"解谜"（puzzle）而非"手艺"（craft）。解谜的乐趣在于偶尔的突破，手艺的乐趣在于持续的打磨。
前 AI 时代它是好选择，因为"写代码"这层手艺活填充了证明搜索之间的等待。现在这层被 AI 剥离了，剩下的证明部分太硬、太脆，不适合放松。
2.3 PureLibm-rs 模式如何修复这个问题
PureLibm-rs 的设计将工作主体从"纯证明"切换到"实现 + 文档 + 工程测试 + 渐进验证"：
之前的模式：
实现（AI 已替代）→ 证明（反心流，阻塞频繁）→ 结束
手艺体验总量：低
PureLibm-rs 模式：
实现（古法手写，审美对象）→ 文档（叙事产出）→ 工程测试（立即可见，心流好）
→ 系数追溯（考古乐趣）→ L0-L2 验证（可预测推进）→ L3-L4 证明（偶尔的深度）
手艺体验总量：高
对手工艺重评的修正：
| 维度 | 之前（纯验证） | PureLibm-rs 模式下 |
|---|---|---|
| 心流潜力 | ⚠️ 中偏低 | ✅ 实现+测试是可预测挑战，证明是可选的深度 |
| 进度可见 | ❌ 差 | ✅ 每完成一个函数的实现+测试+文档就是可见进度 |
| 审美回报 | ⚠️ 中 | ✅ 代码本身（数学公式的翻译）是审美对象；测试通过的绿色是审美回报；系数来源的考古故事是审美产出 |
| AI 关系 | ⚠️ AI 替代了代码层的乐趣 | ✅ 古法手写实现 + AI 辅助验证 = 各取所需 |
修正结论：PureLibm-rs 模式将一个"解谜型"项目转化为"手艺 + 解谜"混合项目。 实现和工程测试层提供可预测的心流（手艺满足），形式化验证层提供偶尔的深度突破（解谜满足）。两者加起来，总体验质量显著优于纯验证。
这恰好对应"特殊函数手表匠"的方向——每个函数是一个自包含的机芯，实现它、测试它、记录它的系数来源，本身就是手艺活。形式化验证是"加上去的保险"，不是"唯一的产出"。
两个评价的分层：
- 在"AI 时代战略项目"框架下 → 仍然高价值 ✅
- 在"手工艺放松项目"框架下 → PureLibm-rs 模式下修复了之前的缺陷，变成了可行的选择 ✅
2.4 建议的启动方式（更新：基于 PureLibm-rs Pilot 阶段）
对应 [[PureLibm-rs.md]] 的 M1–M2 里程碑。
第一步：搭建基础设施（M1），而非直接写证明。
选择 2-3 个 pilot 函数完成全链路验证：
| 函数 | 复杂度 | 验证价值 |
|---|---|---|
cr_sqrtf | 低 — 分支少，range reduction 简单 | 验证基础设施：FFI 对接、测试编排、coverage 工具链 |
cr_sinf | 高 — 复杂 range reduction（Payne-Hanek）、多项式逼近、多条件分支 | 验证核心翻译流程 + L2 Kani 验证方案 |
cr_expf | 中高 — 特殊值路径多（overflow/denormal） | 补充异常路径覆盖 |
交付物：
- 实现代码 + 函数文档（含系数来源标注）
- f32 穷举测试通过（对比高精度 oracle）
- CORE-MATH 一致性测试通过
- Kani 验证对
cr_sinf的 range reduction 代码无 panic 和溢出 - 系数脚本在
coeff/下可独立运行
Pilot 阶段通过后，可以复用基础设施推进 M3（全部 ~40 个 binary32 函数）。pilot 不代表其余函数可以机械填充——每个函数仍需要独立确认特殊值策略、hard-to-round cases、系数来源、range reduction 边界和 oracle 差异。
三、参考实现的设计要求
对应 [[PureLibm-rs.md]] 第 1、5 章。
3.1 代码可读性
代码贴近算法的数学表达形式。每个函数遵循统一的结构模板：
/// 函数名 + 简短描述
///
/// # 正确性保证
/// - 正确性 oracle: MPFR / 高精度参考，f32 穷举测试已通过
/// - 翻译一致性参考: CORE-MATH (commit hash)
///
/// # 算法描述
/// 1. 特殊值处理（NaN, Inf, subnormal）
/// 2. Range reduction 步骤
/// 3. 多项式逼近
/// 4. Reconstruction
///
/// # 系数来源
/// Sollya 脚本: `coeff/sinf.sollya`
///
/// # 验证
/// - Kani: `verification/sinf_range_reduction.rs` 验证 range reduction
/// - f32 穷举测试: `cargo test --features exhaustive --test exhaust sinf`
pub fn cr_sinf(x: f32) -> f32 { ... }
3.2 位操作策略
| 不鼓励 | 推荐 |
|---|---|
为普通数值操作内联 bits & 0x7fffffff 取绝对值 | 优先使用 f32::abs(x)；需要保留 NaN payload 时用具名 helper |
为普通数值操作内联 bits ^ 0x80000000 翻转符号 | 优先使用 -x 或 copysign(x, y) |
memcpy / 类型双关转换 | f32::to_bits() / f32::from_bits() |
对于 IEEE 754 编码层面的提取操作，应封装为具名函数：
// 不鼓励：每次使用时都需要理解位运算含义
let bits = x.to_bits();
let exp = ((bits >> 23) & 0xff) as i32;
// 鼓励：抽象为具名函数
fn extract_exponent(x: f32) -> i32 { ... }
3.3 架构决策
| 问题 | 决策 |
|---|---|
no_std | 起步阶段以 std 为默认，核心算法与 I/O/FFI 分离以保留未来提取路径 |
| C FFI 绑定 | 暂不考虑。后续如有需要以独立包形式提供 |
| fenv/errno | API 合同只保证返回值。在不影响可读性的前提下尽可能保持与 C libm 的返回值语义一致（signed zero、NaN、Inf、subnormal） |
| FMA 使用 | 使用 f32::mul_add / f64::mul_add 表达 FMA 语义；不要求硬件 FMA 指令 |
| 命名前缀 | 公开 API 使用 cr_ 前缀（如 cr_sinf）；常量使用 CR_ 前缀 |
| MSRV | Rust 1.85（Edition 2024） |
四、魔术参数的出处追溯
对应 [[PureLibm-rs.md]] 第 5 章可读性要求。
这是 PureLibm-rs 区别于普通 libm 实现的核心特征：每个魔法常数都能回答"这个数字是怎么来的"。
4.1 系数标注格式
源码中每个魔法常数必须标注来源：
// Generated by: Sollya
// Script: coeff/sinf.sollya
// Command: remez(..., [-2^-12, 2^-12], ...)
const CR_SINF_A: f64 = 0x1.921fb54442d17p-3;
4.2 系数脚本目录
coeff/ 目录下提供可独立运行的 .sollya 脚本：
# 有 Sollya 环境即可复现
sollya coeff/sinf.sollya
脚本注释中标注使用的 Sollya/Gappa/MPFR 版本。在函数集完全实现后，再考虑多版本交叉验证。
4.3 引用文献
函数文档应交叉引用相关论文和 CORE-MATH 源码行：
//! # References
//! - [CORE-MATH sinf.c (commit a1b2c3d)](https://github.com/...)
//! - J.-M. Muller, "Elementary Functions: Algorithms and Implementation", 3rd ed.
//! - Payne & Hanek, "Radian Reduction for Trigonometric Functions", 1983
4.4 为什么这很重要
在 AI 时代，规格就是护城河。一个包含完整系数来源、算法描述和引用链的参考实现，其价值远超一个"能跑但不知道为什么"的实现。系数追溯文档本身是"领域知识结构化"的产出——把论文和脚本里的隐式知识变成可复现的公共品。
五、完备的测试体系（五级验证）
对应 [[PureLibm-rs.md]] 第 2 章。
验证分为五个级别，每一级提供不同强度的保证：
| 级别 | 手段 | 保证内容 | CI 频率 |
|---|---|---|---|
| L0 | Rust 类型系统 + #[deny(unsafe_op_in_unsafe_fn)] + clippy lint + 单元/集成测试 | 降低 UB、panic 风险；禁止新增未审查的 panic!、unwrap、越界索引 | 每次提交 |
| L1 | float32 穷举测试 + float64 随机/边界测试。正确性 oracle 使用高精度参考（MPFR）；翻译一致性 oracle 使用 CORE-MATH FFI | f32 在穷举输入上符合正确舍入目标；f64 在采样范围内与参考一致 | 穷举为 nightly/cron，其余每次提交 |
| L2 | Kani bounded model checking | 对 range reduction、整数/位操作、表索引等逻辑验证无 panic、无越界、无未声明溢出 | 每次提交 |
| L3 | Sollya + Gappa 脚本 | 生成多项式逼近的误差边界证明；计算公式常数 | 记录在 coeff/，手工检查 |
| L4 | Coq / Flocq | 完整机器可检查的正确舍入证明 | CORE-MATH 已有部分函数完成，本项逐步对接 |
项目起步瞄准 L0–L2。L3–L4 作为文档和演进目标。
Oracle 分层
- 正确性 oracle：用于证明正确舍入目标。对比 MPFR 或其他高精度参考，按目标舍入模式生成期望结果。
- 翻译一致性 oracle：用于证明 Rust 移植没有偏离指定 CORE-MATH commit。CORE-MATH 以 git submodule 形式纳入，
build.rs通过cccrate 编译为静态库，测试中 FFI 调用。
CORE-MATH 一致性测试不能单独证明正确舍入；它只证明与指定参考实现返回值一致。若 CORE-MATH 和高精度 oracle 结果冲突，以正确性 oracle 为准。
测试组织
src/ ← 库代码
tests/ ← cargo test: 随机 + 边界值测试（每次 CI）
tests/exhaust.rs ← #[cfg(feature = "exhaustive")] gate（nightly cron）
tests/exhaust/ ← 穷举测试子模块
kani.toml ← cargo kani harness 注册
verification/ ← Kani 验证代码，只通过 #[cfg(kani)] 编译
六、相关手艺项目方向
PureLibm-rs 的模式（实现 + 文档 + 工程测试 + 渐进验证）恰好将"特殊函数手表匠"的手艺体验和"形式化验证"战略价值结合为一个统一的工作流。以下是形成互补的三个相关方向。
6.1 特殊函数手表匠（Numerical Function Gallery）
每次选一个数学函数（erf, log1p, hypot, tgamma, j0...），深入研究它、实现它、测试它、记录它。
手工艺优势：
- 每个函数自包含：读原始论文 → 选算法 → 实现 → 跑误差测试 → 画误差曲面图 → 写笔记
- AI 拿不走手艺乐趣：AI 可以生成实现，但不能替你欣赏 1969 年 Cody 的方法和 1993 年 Tang 的近似哪种更优雅
- 维护负担 ≈ 零
- 长期性：C99 有 100+ 个数学函数，加上 IEEE 754-2019 新增的，够做好几年
与 PureLibm-rs 的关系： 这是 PureLibm-rs 的"手艺核心"——你可直接在这个项目中实践：选一个 CORE-MATH 未覆盖的函数 → 古法手写实现 → 写文档 → 跑穷举测试 → 标注系数来源。PureLibm-rs 的工程结构可以复用。
6.2 浮点陷阱图鉴（FP Trap Encyclopedia）
系统地收集、复现、解释、可视化浮点数陷阱——那些让数值程序悄然出错的情况。
手工艺优势：
- "田野调查"模式：发现案例 → 最小化复现 → 理解机制 → 画图解释 → 归档
- 审美产出很好：精心设计的浮点陷阱可视化本身就是作品
- AI 只能生成"已知的"陷阱，不能真正跑代码发现新案例
- 长期性：无限
与形式化验证的关系： 浮点陷阱图鉴收集的反例，可以作为形式化验证的测试集——两者互补。一个做"正面证明"，一个做"反面探测"。
6.3 FORTRAN 遗产修复（Legacy FORTRAN Restoration）
选取 netlib、SLATEC 等经典 FORTRAN 数值库中的子程序，做"考古修复"——理解、翻译到现代语言（Julia）、补测试、写历史注释。
手工艺优势：
- 像修复古籍——每段代码背后有作者的经验、时代假设、未写出的推导
- AI 可以翻译代码，但 AI 不能做"考古"——理解为什么 1979 年的作者用了这个奇怪的常数
- 审美对象是翻译的优雅程度
关键约束： 这是一次性的翻译+注释产出，不是持续维护原库。只做前者。
6.4 方向间的互补关系
特殊函数手表匠 ←→ 浮点陷阱图鉴 ←→ PureLibm-rs 验证体系
正向建造 反向探测 分层正确性保证
"造表" "田野调查" "证明 + 保险"
PureLibm-rs 把这些方向整合为统一工作流：
手表匠 = 实现层（手写 + 文档 + 系数标注）
陷阱图鉴 = 测试输入源（反例纳入 CI 测试集）
验证体系 = L0-L4 分层保证（工程测试 → 形式化证明）
三者共享底层的数学函数知识。PureLibm-rs 提供了将它们统一在一起的工程框架。
七、LLVM 对浮点运算的弱约束
以下来自 Rust 科学计算生态调研第八章。
在考虑用 Rust 做形式化验证或高精度数值函数实现时，必须理解 Rust/LLVM 浮点运算的底层约束——这决定了"能证明什么"和"在什么假设下证明"。Rust 通过 LLVM 生成机器码，LLVM 的浮点 IR 指令并非严格 IEEE 754，在多个维度上提供了弱于 C 编译环境的保证。
7.1 舍入模式：LLVM 评级 F（完全未实现）
| 能力 | C (gcc/clang + glibc/musl) | Rust (via LLVM) |
|---|---|---|
| 动态舍入模式 | fesetround(FE_UPWARD) via fenv.h | 不可用。修改 MXCSR/FPCR 是 UB |
| 静态舍入操作 | #pragma STDC FENV_ROUND (C23) | LLVM 评级 F — 完全未实现 |
| 约束 intrinsic | — | 存在 llvm.experimental.constrained.*，但 Rust 不暴露 |
实际后果： 如果你想实现一个需要非默认舍入的数值函数（如 interval arithmetic 需要向上/向下舍入），Rust/LLVM 原生不支持。唯一的 workaround 是：
- 用
unsafe+ inline asm 操作 MXCSR（跨平台不兼容且是 UB） - 依赖
fesetround的 FFI 绑定（不可移植，优化器可能破坏） - 使用整数位操作模拟不同舍入方向的运算
7.2 NaN 传播：故意非确定性
Rust RFC 3514（2024 稳定化）明确规定：
- NaN 的符号和 payload 不是确定性的 — 相同的操作、相同的输入，在不同架构、优化级别甚至不同运行之间，可能产生不同的 NaN 位模式
const fn和运行时求值可能产生不同的 NaN — 这在 Rust 1.82 中被正式稳定化- sNaN 可以传播为 sNaN — 违反 IEEE 754 的"操作从不输出 sNaN"规则（LLVM 优化如
x * 1.0 → x需要这个行为来保持语义）
这意味着：你不能在 Rust 中验证 NaN 传播的精确行为，因为规范本身不承诺。如果需要"当输入是 NaN 时输出特定的 NaN payload"（某些嵌入式或安全关键场景），Rust 不是正确的工具。
7.3 浮点环境：没有暴露
| C 能力 | Rust 状态 |
|---|---|
fetestexcept(FE_OVERFLOW) | 不可用 |
feclearexcept(FE_ALL_EXCEPT) | 不可用 |
fegetenv / fesetenv | 不可用 |
#pragma STDC FENV_ACCESS ON | 不存在 |
实际后果： 如果你的数值函数需要"检测是否发生了溢出/下溢/不精确"作为算法分支条件（某些自适应精度算法中常见），Rust 不直接支持。
7.4 精度收缩
| 行为 | C（fp-contract） | Rust |
|---|---|---|
| FMA 自动收缩 | 实现定义，#pragma STDC FP_CONTRACT 控制 | * 和 + 相邻时默认允许收缩。设置 -C target-feature=-fma 可禁用 |
a * b + c 在 Rust 中可能被优化为 fma(a, b, c)（一次舍入）或保留两次舍入——不承诺具体行为。需要严格 bitwise 可复现的场景需要用 mul_add 显式控制。
7.5 已知不兼容 IEEE 的平台
| 平台 | 问题 |
|---|---|
32-bit x86 无 SSE2 (i586) | x87 80-bit 内部精度，无法提供 IEEE 兼容结果 |
| 32-bit x86 有 SSE2 | x87 返回寄存器可能修改 NaN payload |
| 旧 MIPS | quiet/signaling bit 反了 |
| 32-bit ARM NEON | SIMD 操作总是 flush-to-zero |
八、Rust libm vs C libm
8.1 Rust libm 的优势
Rust 的 libm crate（从 musl 移植）有比 C 生态更现代的测试基础设施：
| 特征 | 说明 |
|---|---|
| ULP 精度框架 | 每个函数有明确的 ULP 误差阈值（标准数学函数 0-4 ULPs） |
| MPFR 参考验证 | CI 中以高精度 MPFR 库为 golden reference |
| 边界 case 框架 | 显式的 EdgeCases 生成器，覆盖 ±0、±∞、NaN、渐近线、临界点 |
| 跨架构测试 | 自动检测跨平台一致性 |
| 可覆盖容忍度 | MaybeOverride trait 允许标记已知问题的断言失败/ULP 放宽/跳过 |
一篇 2025 年的研究（Gladman et al.）直接比较了双精度 cosh 的最大 ULP 误差：
| 库 | 最大 ULP 误差 |
|---|---|
| musl | 1.04 |
| OpenLibm / FreeBSD | 1.47 |
| GNU glibc | 1.93 |
| Newlib | 2.67 |
musl（和继承它的 Rust libm）在精度上可以超过 glibc。
8.2 Rust libm 的弱项
| 弱项 | 说明 |
|---|---|
| NaN 行为取决于编译目标 | 非确定性来源于 LLVM 后端，不是 libm 代码的问题，但结果一样 |
| 交叉架构一致性弱于严格 C | C 有 #pragma STDC FENV_ACCESS 来约束优化器；Rust/LLVM 没有等价机制 |
| sNaN 处理分歧 | Rust libm 继承了 musl 的 C 标准立场（pow(sNaN,0)=1），glibc 的立场是返回 NaN。这种分歧在不同标准的解读之间无法消除 |
| Rust 版本升级可能改变浮点行为 | const fn 浮点运算的行为在 1.82 改变过；未来 LLVM 升级可能改变 runtime 路径上的优化 |
九、形式化验证工具现状
| 工具 | 方法 | 浮点能力 | 状态 |
|---|---|---|---|
| Kani | 模型检查（CBMC 后端） | v0.59-0.61 增强了浮点支持，可以验证固定输入范围的精度断言。不支持舍入模式/NaN propagation 的验证 | 对数学函数验证仍然有限 |
| Creusot | 演绎验证（Why3 后端） | 专注于 Rust 的类型安全和借用语义。浮点专用 support 较弱 | 不适合纯数值验证 |
| Verus | 演绎验证（SMT via Z3） | 通过 Rust 的 assert! 和 proof 函数验证。浮点公式在 SMT 中是理论难点 | 可用于辅助证明算法逻辑，而非精度 |
| grug | 基于 MIR 的符号执行 | 研究级，可以探索浮点路径 | 早期 |
现状：没有一个 Rust 工具可以端到端验证"这个函数对所有 f64 输入的误差 ≤ 1 ULP"。 这是一个开放的研究问题——部分因为 LLVM 的非确定性 NaN 语义使得验证的 precondition 本身就很难写。
十、对项目的实际含义
10.1 在 Rust 中，你能可靠验证什么？
| 可验证 | 方法 | 局限 |
|---|---|---|
| ✅ 固定输入输出的 bitwise 等价 | Kani + property test | 需要固定编译目标 |
| ✅ 给定输入的 ULP 误差界限 | proptest + MPFR 对照 | 非形式化证明 |
| ✅ 不 panic、不溢出、不除零 | Kani + #[kani::proof] | 不含浮点域约束 |
| ⚠️ 单调性 | proptest + 采样 | 全输入域的单调性是开放问题 |
| ❌ NaN propagation 行为 | — | Rust 不承诺确定性 |
| ❌ 跨所有浮点输入的 ≤ 1 ULP 保证 | — | 无现成工具，需手动证明 |
10.2 证明声明中必须包含的假设
如果你要做"形式化验证"（即使是部分验证），文档开头必须声明：
- 目标硬件平台（如 x86_64-unknown-linux-gnu，禁止 i586）
- 接受的 NaN 行为（接受非确定性，仅验证非 NaN 输入路径）
- 舍入模式假设（默认 round-to-nearest-even，不验证其他模式）
- 验收标准（对
f64所有非 NaN 输入，误差 ≤ 2 ULPs）
10.3 核心结论
在 Rust 中做数值函数的形式化验证，其理论完备性弱于 C +
#pragma STDC FENV_ACCESS组合。但 Rust libm 的测试基础设施比大多数 C libm 的实际测试更系统。
换句话说：C 的标准环境理论上提供更强的浮点确定性（你可以用 fenv.h 告诉编译器不要越界），但实践中大多数 C libm 实现并没有 Rust libm 那种 ULP 精度框架和跨架构 CI。理论完整性和工程验证强度之间存在一个值得注意的 trade-off。
十一、替代方案
如果有追求最高浮点确定性的需求：
| 方案 | 说明 | 代价 |
|---|---|---|
C + #pragma STDC FENV_ACCESS ON | 编译器不得跨浮点操作优化 | C 语言本身的内存安全风险 |
| Julia | 可以调用 llvmcall 加 constrained intrinsic，且 Base.Math 已是黄金参考 | 仍然依赖 LLVM 后端 |
| 直接在 Julia 中验证算法，在 Rust 中做工程实现 | 形式化规格用 Julia 标注，Rust 实现用 proptest + MPFR 对抗 | 两个语言的验证结果需要对齐 |
| Ada (SPARK) | SPARK 的浮点合约是工业级最强的，有静态精度证明 | 生态窄，不实用 |
| Rust + 软件浮点库 | 用 soft-float crate 做 bit-exact 跨平台计算 | 极慢，不适合日常使用 |
十二、C libm vs Rust libm：综合评价矩阵
| 维度 | C libm 生态 | Rust libm 生态 | 对验证工作的影响 |
|---|---|---|---|
| 标准环境浮点确定性 | ⭐⭐⭐⭐ (有 fenv) | ⭐⭐ (LLVM 约束弱) | C 更强 |
| 工程测试基础设施 | ⭐⭐½ (ad-hoc) | ⭐⭐⭐⭐ (ULP 框架 + MPFR CI) | Rust 更强 |
| NaN 确定性 | ⭐⭐⭐½ | ⭐ (故意非确定) | C 大幅领先 |
| 舍入模式控制 | ⭐⭐⭐⭐ | ⭐ (基本没有) | C 大幅领先 |
| 跨架构一致性 | ⭐⭐½ (取决于编译器) | ⭐⭐½ (同样取决于 LLVM) | 持平 |
| 形式化验证工具 | ⭐⭐⭐ (Frama-C, VST) | ⭐⭐ (Kani, Creusot) | C 更成熟 |
| AI 辅助验证友好度 | ⭐⭐ (UB 多) | ⭐⭐⭐⭐ (类型安全) | Rust 更好 |
十三、项目选择判据框架的交叉应用
13.1 形式化验证在判据框架中的位置
价值判据（"判断"还是"代码"？）：
- 形式化规格 + 证明 → 纯判断型资产 ✅
- AI 替代期限 → ≥ 5 年 ✅
- 裁员测试 → 去掉代码，证明和规格仍有价值 ✅
需求判据（在 AI 时代是增强还是减弱？）：
- 形式化验证需求随 AI 代码量增长而爆发 → 增强 ✅
资产判据（不可替代型资产占比）：
- 规格 ✅ | 证明 ✅ | 测试集 ✅ | 方法论 ✅
- 代码实现 ❌（可被 AI 替代）
- 比例：高 ✅
在"高价值领域速查"中的位置：
- 基准与评测 ✅
- 验证工具链 ✅
- 领域知识结构化 ✅
13.2 两级过滤器快速判断
| 过滤器 | 形式化验证数学库 |
|---|---|
| 1. AI 做不好，且短期内做不好？ | ✅ 是（≥ 5 年） |
| 2. 去掉代码后 3 年后还有用？ | ✅ 是（证明、规格是长期资产） |
| 3. 积累的资产是"判断"还是"代码"？ | ✅ 判断型 |
| 4. 我有别人没有的东西吗？ | ✅ 数学库实现经验 + ChemE 视角 |
战略角度：通过。手工艺角度：不通过。 关键取决于你要什么。
十四、关于数学库的个人规则
来自 [[个人项目选择规则.md]] 的相关内容。
数学库函数重写
读别人代码并重写的实际成本很高，因为数学库代码通常压缩了：
- 数值分析、误差控制、table generation
- 历史 bug fix、特定平台假设
- 作者经验和未写出的推导
如果没有作者交流、原始推导、测试集和实际使用场景，单纯重写很容易变成无限考古。
以后只有在以下情况下继续：
- 服务某个具体函数的验证
- 服务某篇技术文章
- 服务自己的参考库
- 服务一个真实 bug 修复
- 服务简历/研究展示
- 有明确 benchmark 和完成定义
否则不作为独立长期项目。
特殊函数库 / F77 数学库维护
如果自己实际上不用，默认降级为有限维护：
- 保持项目可构建
- 修复明确问题
- 接受高质量 PR
- 不主动扩展
- 不为"它有意义"承担无限责任
数学知识补充既是奖励也是负担，必须和明确需求绑定。
十五、综合行动建议
-
PureLibm-rs pilot 作为手艺项目主线 → 搭建 M1 基础设施 + 完成 2-3 个 pilot 函数（
cr_sqrtf,cr_sinf,cr_expf）。这是"特殊函数手表匠"的实际载体——实现、写文档、标注系数来源、跑穷举测试、跑 Kani。手艺体验好，战略价值高。 -
形式化验证作为渐进增强，不是起点 → L0-L2（类型系统 + 穷举测试 + Kani）作为 CI 常驻；L3-L4（Sollya/Coq）作为文档和演进目标，不急。
-
浮点陷阱图鉴作为并行项目 → 与 PureLibm-rs 互补。发现的反例可以纳入 PureLibm-rs 的测试集。
-
如果追求最高浮点确定性 → 最终的 bit-exact 验证可能需要 C +
#pragma STDC FENV_ACCESS环境。但在那之前，Rust 的测试基础设施完全够做方法论级的工作。 -
长期方向 → PureLibm-rs 的系数和文档本身就是"领域知识结构化"的产出。ℜeos/FeOs 的测试贡献是另一个直接的社区出口。
-
与 ChemE 的联系 → 面向科学计算的验证工具链，是"个人发展 × 社区贡献"的交集方向之一。PureLibm-rs 在这个方向上的积累——系数追溯、测试体系、形式化方法——都可以迁移到 ChemE 数值模型的验证中。