如何确定hamming重量不变量

Question

我正在学习达夫尼，试图为汉明重量问题编写一个规范，也就是一个数字中的1位数。我相信我的规格是正确的，但仍然不能证实。为了提高验证速度，我将其限制为8位数；问题定义：https://leetcode.com/problems/number-of-1-bits/

function method twoPow(x: bv16): bv16
  requires 0 <= x <= 16
{
  1 << x
}

function method oneMask(n: bv16): bv16
    requires 0 <= n <= 16
    ensures oneMask(n) == twoPow(n)-1
{
   twoPow(n)-1
}

function countOneBits(n:bv8): bv8 {
    if n == 0 then 0 else (n & 1) + countOneBits(n >> 1)
}

method hammingWeight(n: bv8) returns (count: bv8 )
    ensures count == countOneBits(n)
{
    count := 0;
    var i := 0;
    var n' := n;
    assert oneMask(8) as bv8 == 255; //passes
    while i < 8
        invariant 0 <= i <= 8
        invariant n' == n >> i
        invariant count == countOneBits(n & oneMask(i) as bv8);
    {
        count := count + n' & 1;
        n' := n' >> 1;
        i := i + 1;
    }
}

我在javascript中编写了相同的代码来测试循环前后的行为和不变量值。我没看到任何问题。

function twoPow(x) {
    return 1 << x;
}

function oneMask(n) {
    return twoPow(n)-1;
}

function countOneBits(n) {
    return n === 0 ? 0 : (n & 1) + countOneBits(n >> 1)
}

function hammingWeight(n) {
    if(n < 0 || n > 256) throw new Error("out of range")
    console.log(`n: ${n} also ${n.toString(2)}`)
    let count = 0;
    let i = 0;
    let nprime = n;
    console.log("beforeloop",`i: ${i}`, `n' = ${nprime}`, `count: ${count}`, `oneMask: ${oneMask(i)}`, `cb: ${countOneBits(n & oneMask(i))}`)
    console.log("invariants", i >= 0 && i <= 8, nprime == n >> i, count == countOneBits(n & oneMask(i)));
    while (i < 8) {
        console.log("");
        console.log('before',`i: ${i}`, `n' = ${nprime}`, `count: ${count}`, `oneMask: ${oneMask(i)}`, `cb: ${countOneBits(n & oneMask(i))}`)
        console.log("invariants", i >= 0 && i <= 8, nprime == n >> i, count == countOneBits(n & oneMask(i)));
        count += nprime & 1;
        nprime = nprime >> 1;
        i++;
        console.log('Afterloop',`i: ${i}`, `n' = ${nprime}`, `count: ${count}`, `oneMask: ${oneMask(i)}`, `cb: ${countOneBits(n & oneMask(i))}`)
        console.log("invariants", i >= 0 && i <= 8, nprime == n >> i, count == countOneBits(n & oneMask(i)));
    }
    return count;
};

hammingWeight(128);

所有不变量计算为真。我一定是漏掉了什么。它说invariant count == countOneBits(n & oneMask(i) as bv8);可能不是由循环来维护的。运行javascript显示它们都是真的。这是由于oneMask对bv8的影响吗？

编辑:我用一个不需要转换，但仍然不能解决问题的函数替换了掩码函数。

function method oneMaskOr(n: bv8): bv8 
    requires 0 <= n <= 8
    ensures oneMaskOr(n) as bv16 == oneMask(n as bv16)
{
    if n == 0 then 0 else (1 << (n-1)) | oneMaskOr(n-1)
}

我发现的一件有趣的事情是，它向我展示了一个反例，它已经到达循环的末尾，并且设置了输入变量n的最后一个位，因此值为128或更高。但是，当我在循环的上方添加一个断言，其值等于循环末尾的计数时，它就会向我显示另一个值n。

assert 1 == countOneBits(128 & OneMaskOr(8)); //counterexample -> 192
assert 2 == countOneBits(192 & OneMaskOr(8)); //counterexample -> 160

所以它似乎不是在计算循环结束后的循环不变量吗？我认为不变量的全部要点是在循环结束后进行评估。

编辑2:我搞清楚了，很明显，在while循环中添加了一个显式的减额子句来修复它。不过我不明白。我以为达芙妮会想出办法的。

    while i < 8
        invariant 0 <= i <= 8
        invariant n' == n >> i
        invariant count == countOneBits(n & oneMask(i) as bv8);
        decreases 8 - i
    {

我看到文档中有一行用于循环终止：

如果循环的减额子句指定*，则不执行终止检查。此功能的使用只对部分正确性而言是合理的。

因此，如果缺少减额子句，它默认为*吗？

Answer 1

在反复试用之后，我确实找到了一个版本，尽管它需要重新工作countOneBits()，因此它的递归遵循迭代的顺序：

function countOneBits(n:bv8, i: int, j:int): bv8
  requires i ≥ 0 ∧ i ≤ j ∧ j ≤ 8
  decreases 8-i {
  if i == j then 0
  else (n&1) + countOneBits(n >> 1, i+1, j)
}

method hammingWeight(n: bv8) returns (count: bv8 )
ensures count == countOneBits(n,0,8)
{
    count ≔  0;
    var i ≔  0;
    var n' ≔ n;
    //
    assert count == countOneBits(n,0,i);
    //
    while i < 8
        invariant 0 ≤ i ≤ 8;
        invariant n' == n >> i;
        invariant count == countOneBits(n,0,i);
    {
        count ≔  (n' & 1) + count;
        n' ≔  n' >> 1;
        i ≔  i + 1;
    }
}

这里的直觉是，countOneBits(n,i,j)返回i (包括)和j (独占)之间的1位数。然后，这反映了循环在增加i时所做的事情。