// ---- Square of Fibonacci ----

function Fib(n: nat): nat {
  if n < 2 then n else Fib(n-2) + Fib(n-1)
}

method FibSquared(n: nat) returns (x: nat)
  ensures x == Fib(n) * Fib(n)
{
  x := 0;
  var i, y, k := 0, 1, 0;
  assert k < y;
  while i != n
    invariant 0 <= i <= n
    invariant x == Fib(i) * Fib(i)
    invariant y == Fib(i+1) * Fib(i+1)
    invariant k == 2*Fib(i+1)*Fib(i)
  {
    x, y, k := y, y + k + x, y + y + k;
    i := i + 1;
  }
}

// ---- Canyon Search ----

function method Dist(x: int, y: int): int {
  if x < y then y - x else x - y
}

function method Min(x: int, y: int): int {
  if x < y then x else y
}

method CanyonSearch(a: array<int>, b: array<int>) returns (d: int)
  requires a.Length != 0 && b.Length != 0
  requires forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j]
  requires forall i,j :: 0 <= i < j < b.Length ==> b[i] <= b[j]
  ensures exists i,j :: 0 <= i < a.Length && 0 <= j < b.Length && d == Dist(a[i], b[j])
  ensures forall i,j :: 0 <= i < a.Length && 0 <= j < b.Length ==> d <= Dist(a[i], b[j])
{
  d := Dist(a[0], b[0]);
  var m, n := 0, 0;
  while m != a.Length && n != b.Length
    invariant 0 <= m <= a.Length && 0 <= n <= b.Length
    invariant exists i,j :: 0 <= i < a.Length && 0 <= j < b.Length && d == Dist(a[i], b[j])
    invariant forall i,j :: 0 <= i < a.Length && 0 <= j < b.Length ==>
      d <= Dist(a[i], b[j]) || (m <= i && n <= j)
    decreases a.Length - m + b.Length - n
  {
    d := Min(d, Dist(a[m]));
    if
    case a[m] <= b[n] =>
      m := m + 1;
    case b[n] <= a[m] =>
      n := n + 1;
  }
}