Dafny项目中的BigNumber减法运算问题分析与解决方案

背景介绍

Dafny是一种支持形式化验证的编程语言，它能够同时进行程序验证和代码生成。在Dafny 3.0.0版本中，当使用C++后端编译包含原生类型(nat/int)减法运算的代码时，会遇到"Subtraction of non-native type is not yet supported"的错误。

问题本质

Dafny的C++后端将原生整数类型(nat/int)映射为BigNumber类型，但目前实现中BigNumber并未完整支持减法运算操作。这与Dafny文档中的说明一致：C++编译器不支持BigInteger，因此不应直接使用int类型或数组长度等原生操作。

技术分析

在Dafny验证阶段，减法运算能够正常通过验证，因为验证器使用的是Dafny自己的数学逻辑。问题出现在代码生成阶段，当尝试将Dafny代码编译为C++时，减法运算无法找到对应的BigNumber实现。

解决方案比较

方案一：使用固定宽度整数类型

最直接的解决方案是将代码中的nat/int替换为固定宽度的整数类型，如uint64或int64：

newtype{:nativeType "long"} nat64 = i:int | 0 <= i < 0x8000000000000000

优点：

• 实现简单直接
• 性能较好

缺点：

• 需要修改现有已验证代码
• 需要添加额外的范围检查来处理可能的溢出
• 可能破坏原有的验证逻辑

方案二：实现完整的BigNumber支持

理论上可以开发一个完整的BigNumber C++实现，包括加减乘除等基本运算。这需要：

1. 实现BigNumber类
2. 支持所有必要的运算符重载
3. 处理与C++标准库的兼容性问题(如作为哈希键等)

优点：

• 保持Dafny数学语义的完整性
• 不需要修改已验证代码

缺点：

• 实现复杂度高
• 性能开销大
• 需要修改Dafny编译器代码

方案三：混合解决方案(临时方案)

作为临时解决方案，可以采用以下步骤：

1. 在Dafny代码中将nat临时转换为int64进行运算
2. 在生成的C++代码中将BigNumber简单映射为原生整数类型

using BigNumber = int;

注意：这仅适用于不严格要求验证正确性的场景，如性能基准测试等。

最佳实践建议

对于生产环境，建议采用以下策略：

1. 在新项目中预先设计使用固定宽度整数类型
2. 对于已有项目，逐步重构将关键路径上的运算迁移到固定宽度类型
3. 保留BigNumber仅用于确实需要任意精度计算的场景
4. 考虑为Dafny贡献完整的BigNumber C++实现

总结

Dafny的C++后端目前对BigNumber的支持有限，开发者在涉及数值运算时需要特别注意类型选择。根据项目需求，可以选择使用固定宽度类型、等待官方支持或自行扩展实现。理解这一限制有助于更好地规划Dafny项目的技术路线。