loop invariants always fail

[lvtao-sec]

Hi,

I'm writing a function to reverse bits of a 64-bit vector in dafny, as shown in the function ReverseNBits.

It works in a loop, each iteration of which gets one bit of num from low to high, left shift result one bit, and then or the retrieved one bit at the lowest bit of result.

I add two loop invariants (in the form of forall) to ensure the result is correct, which checks at iteration i, if the lowest i bits of result and num is in the reversed order, and if the highest(64-i) bits are zeros.

But the two invariants always fail, can anyone give me some hints on how to solve this issue?
Thank you in advance!

function reversed(result: bv64, num: bv64, curbit: int, width: int): bool
    requires curbit < width
    requires 0 < width <= 64
    requires 0 <= curbit < 64
    {
        ((result >> curbit) & 1) == ((num >> (width-curbit-1)) & 1)
    }

function zero(result: bv64, shiftbit: int): bool
    requires 0 <= shiftbit < 64
    {
        ((result >> shiftbit) & 1) == 0
    }

method ReverseNBits(num: bv64, N: int) returns (y: bv64)
    requires N == 16 || N == 32 || N == 64
    // ensures bitReversed2(num, y, N-1, N-1) == true
    {
        var result: bv64 := 0;
        var i: int := 0;

        var sum: int := 0;

        // n = 64, num=0x4000000000000000, result=0, i = 63
        // n = 16, num=0x80, result = 0, i = 8
        while i < N
            invariant 0 <= i <= N
            invariant i == 0 ==> result == 0
            invariant 0 < i < N ==> forall j,m :: 0 <= j < i && i <= m < 64 ==> reversed(result, num, j, i) && zero(result, m)
            invariant i == 64 ==> forall j :: 0 <= j < i ==> reversed(result, num, j, i)
            //
            decreases N - i
        {
            result := ((result << 1) | ((num >> i) & 1));
            i := i + 1;
        }

        var maskN: bv64 := if N == 64 then 0xffffffffffffffff else ((0x0000000000000001 << N) - 1);
        y := ((result & maskN) | (num & !maskN));
    }