Dafny处理位向量

问题描述

• 我正在尝试将Dafny与（无符号）位向量一起使用（在this post之后）。
• 以下简化示例（permalink）可以正常工作，但是当我更改为bv32时，我得到：
  • Unexpected prover response: timeout
• 这是一个错误吗？或两者之间的预期性能差距？
• 以下是使该帖子自包含的代码：

method bitvectors()
{
    var a : bv16 := 0;
    // var a : bv32 := 0;
    ghost var atag := a;
    while (a<0xFFFF)
    // while (a<0xFFFFFFFF)
        invariant atag < 0xFFFF
        //invariant atag < 0xFFFFFFFF
    {
        atag := a;
        a := a+1;
    }
}

解决方法

我希望其他人有更好的答案...但是基本上这就是为什么我远离位向量的原因：）

我做了一些挖掘工作，在这个特定示例上，Dafny似乎陷入了循环终止检查中。在Boogie级别，比较位向量涉及将它们转换为数学整数，然后转换为实数，然后进行比较。对于求解器来说，使用这些转换函数很麻烦，因为它们跨越了不同的理论。

对不起，我帮不上忙。