how to fix hamming weight invariants

I am learning Dafny, attempting to write a specification for the hamming weight problem, aka the number of 1 bits in a number. I believe I have gotten the specification correct, but it still doesn't verify. For speed of verification I limited it to 8 bit numbers; problem definition: 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;
    }
}

I have written the same code in javascript to test the behavior and example the invariant values before and after the loop. I don't seen any problems.


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);

All invariants evaluate as true. I must be missing something. it says invariant count == countOneBits(n & oneMask(i) as bv8); might not be maintained by the loop. Running the javascript shows that they are all true. Is it due to the cast of oneMask to bv8?

edit: I replaced the mask function with one that didn't require casting and that still not resolve the problem.


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)
}

One interesting thing I found is that it shows me a counter example where it has reached the end of the loop and the final bit of the input variable n is set, so values 128 or greater. But when I add an assertion above the loop that value equals the count at the end of the loop it then shows me the another value of n.

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

So it seems like it isn't evaluating the loop invariant after the end of loop? I thought the whole point of the invariants was to evaluate after the end of loop.

Edit 2: I figured it out, apparently adding the explicit decreases clause to the while loop fixed it. I don't get it though. I thought Dafny could figure this out.

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

I see one line in the docs for loop termination saying

If the decreases clause of a loop specifies *, then no termination check will be performed. Use of this feature is sound only with respect to partial correctness.

So is if the decreases clause is missing does it default to *?

Solution

After playing around, I did find a version which passes though it required reworking countOneBits() so that its recursion followed the order of iteration:

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;
    }
}

The intuition here is that countOneBits(n,i,j) returns the number of 1 bits between i (inclusive) and j (exclusive). This then reflects what the loop is doing as we increase i.