dafny - 显示两个位向量的等价性

Question

我一直在尝试证明当两个位向量的所有单独位都相等时它们是等价的。换句话说，下面的语句中a和b是bv64，BitIsSet是提取的函数>来自位向量的第 位，WORD_SIZE 为 64。

(a == b) == (forall i | 0 <= i < WORD_SIZE :: (BitIsSet(a, i) == BitIsSet(b, i)))

第一种情况，其中 a == b 对 Dafny 来说似乎微不足道。所以我要展示的是

if a != b {
    assert !(forall i | 0 <= i < WORD_SIZE :: (BitIsSet(a, i) == BitIsSet(b, i)));
}

这基本上表明存在一个 i 使得两个位不同:

    assert exists i | 0 <= i < WORD_SIZE :: (BitIsSet(a, i) != BitIsSet(b, i)) 

关于如何最好地解决这个问题有什么提示吗？

为了完整性，BitIsSet 基本上屏蔽了 第 位置的位并将其与 0 进行比较。

predicate method {:opaque} BitIsSet(x:bv64, i: nat)
    requires i < WORD_SIZE
{
   (x & ((1 as bv64) << (i as bv7))) != 0
}

通过使用 bool 值序列来完成同样的事情似乎非常简单，我怀疑使用了某种公理？

lemma SeqBoolEquiv(a: seq<bool>, b: seq<bool>)
    requires |a| == WORD_SIZE && |b| == WORD_SIZE
    ensures (a == b) <==> (forall i | 0 <= i < WORD_SIZE :: a[i] == b[i])
{
}

编辑:试图了解这里发生了什么:无法显示位向量(与序列相对)的等价性可能是由于 Dafny 级别缺少公理，或者 Boogie 或 Z3 显示位向量等价性的一些可能限制在那里？

Answer 1

我已经成功地完成了证明，大致遵循了一位使用不同语言的同事的证明。所以，Dafny 很乐意证明这一点

(a & 0xffff_ffff_ffff_ffff) == (b & 0xffff_ffff_ffff_ffff) <==> a == b

我们可以使用它并对位掩码进行归纳，将我们的初始证明转换为:

((a & Bitmask(N)) == (b & Bitmask(N)) == (forall i | 0 <= i < N :: (BitIsSet(a, i) == BitIsSet(b, i)))

然后对 N 进行归纳带底座 N == 0其中 Bitmask(0) == 0 , 并展示关于附加位的步骤案例推理。

最后，我们可以使用归纳证明来得到 N == WORD_SIZE 的结果这给了我们原始引理 (a & Bitmask(WORD_SIZE)) == a .

编辑:BitMask 定义。是否靠溢出得到BitMask(64)工作，即它改变了 1来自 bv64 , 然后 0 - 1 == 0xff..ff . Dafny 似乎对此很满意，我可以证明 BitMask(WORD_SIZE) == 0xff..ff

    function method {:opaque} BitMask(i: uint64) : bv64
        requires i <= WORD_SIZE
    {
        ((1 as bv64) << (i as bv7)) - 1
    }