Dafny: rotated region of an array method verification

Question

this proof gives an infinite loop in Dafnys' verifier:

// Status: verifier infinite loop
// rotates a region of the array by one place forward
method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>)
  requires arr != null
  requires start + len <= arr.Length
  // returned array is the same size as input arr
  ensures r != null && r.Length == arr.Length
  // elements before the start of the region are unchanged
  ensures arr[..start] == r[..start]
  // elements after the end of the rhe region are unchanged
  ensures arr[(start + len)..] == r[(start + len)..]
  // elements in the region are skewed by one in a positive direction and wrap
  // around
  ensures forall k :: 0 <= k < len
                 ==> r[start + ((k + 1) % len)] == arr[start + k]
{
    var i: nat := 0;
    r := new int[arr.Length];
    // just make a copy of the array
    while i < arr.Length
      invariant i <= arr.Length
      invariant forall k: nat :: k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }

    i := 0;
    // rotate the region
    while i < len
      invariant 0 <= i <= len
      invariant arr[..start] == r[..start]
      invariant arr[(start + len)..] == r[(start + len)..]
      invariant forall k :: 0 <= k < i 
                ==> r[start + ((k + 1) % len)] == arr[start + k]
    {
        r[start + ((i + 1) % len)] := arr[start + i];
        i := i + 1;
    }
}

which points to some sort of undecidability issue or is it? Is there a better way to present this problem to avoid the infinite loop?

previous version:

method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>)
  requires arr != null
  requires start + len <= arr.Length
  // returned array is the same size as input arr
  ensures r != null && r.Length == arr.Length
  // elements before the start of the region are unchanged
  ensures arr[..start] == r[..start]
  // elements after the end of the rhe region are unchanged
  ensures arr[(start + len)..] == r[(start + len)..]
  // elements in the region are skewed by one in a positive direction and wrap around
  ensures forall k :: start <= k < (start + len)
                 ==> r[start + (((k + 1) - start) % len)] == arr[k]
{
    var i: nat := 0;
    r := new int[arr.Length];

    while i < arr.Length
      invariant i <= arr.Length
      invariant forall k: nat :: k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }

    i := start;

    while i < (start + len)
      invariant start <= i <= (start + len)
      invariant arr[..start] == r[..start]
      invariant arr[(start + len)..] == r[(start + len)..]
      invariant forall k :: start <= k < i
                ==> r[start + (((k + 1) - start) % len)] == arr[k]
    {
        r[start + (((i + 1) - start) % len)] := arr[i];
        i := i + 1;
    }
}

Answer 1

Non-linear arithmetic is not decidable. So I suspect that using the % operator to define rotation is the root cause of your problem. Below is a version, that does verify, that defines rotation using only linear integer arithmetic.

See also How does Z3 handle non-linear integer arithmetic?

predicate rotated(o:seq<int>, r:seq<int>) 
  requires |o| == |r|
{
  (forall i :: 1 <= i < |o| ==> r[i] == o[i-1]) &&
  (|o| > 0 ==> r[0] == o[|o|-1])  
}

// Status: verifier infinite loop
// rotates a region of the array by one place forward
method displace(arr: array<int>, start: nat, len: nat) returns (r: array<int>)
  requires arr != null
  requires start + len <= arr.Length
  ensures r != null && r.Length == arr.Length
  ensures arr[..start] == r[..start]
  ensures arr[(start + len)..] == r[(start + len)..]
  ensures rotated(arr[start .. start+len], r[start .. start+len])
{
    var i: nat := 0;
    r := new int[arr.Length];
    while i < start
      invariant i <= start
      invariant forall k: nat :: k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }

    assert arr[..start] == r[..start];

    if len > 0 {
      r[start] := arr[start+len-1];

      assert r[start] == arr[start+len-1];

      i := start+1;
      while i < start+len
        invariant start < i <= start+len
        invariant arr[..start] == r[..start]
        invariant r[start] == arr[start+len-1]
        invariant forall k: nat :: start < k < i ==> r[k] == arr[k-1]
      {
          r[i] := arr[i-1];
          i := i + 1;
      }
    }

    assert rotated(arr[start .. start+len], r[start .. start+len]);

    i := start+len;
    while i < arr.Length
      invariant start+len <= i <= arr.Length
      invariant arr[..start] == r[..start]
      invariant rotated(arr[start .. start+len], r[start .. start+len])
      invariant forall k: nat :: start+len <= k < i ==> r[k] == arr[k]
    {
        r[i] := arr[i];
        i := i + 1;
    }
}

http://rise4fun.com/Dafny/aysI