显示两个位向量的等价性答案

【问题标题】：Showing equivalence of two bitvectors显示两个位向量的等价性
【发布时间】：2022-08-03 23:33:36
【问题描述】：

我一直试图证明当两个位向量的所有单个位都等效时，它是等效的。换句话说，下面的语句a和b是bv64和BitIsSet是从位向量中提取ith位的函数，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 基本上掩盖了ith 位置的位并将其与 0 进行比较。

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

同样的事情通过使用布尔序列似乎很简单，我怀疑使用了某种公理？

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 显示位向量等价的一些可能限制那里？

我尝试使用 while 循环，但还没有成功。但是，它使我能够找到我提出的一个健全性问题。 github.com/dafny-lang/dafny/issues/2511
哦，这很有趣。我很高兴我的问题有助于揭示一个错误。

标签： dafny

【解决方案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(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
    }

【讨论】：

很好的解决方案。你如何定义Bitmask？