/*

class Cell {
  var data: int
  constructor (x: int)
    ensures data == x
  {
    data := x;
  }
}

newtype int32 = x | -0x8000_0000 <= x < 0x8000_0000

type even = x: int | x % 2 == 0

type small = x | 0 <= x < 100

method Example(arr: array<real>, s: small, e: even)
  requires s < arr.Length

trait CountingThings {

}

class Counter extends CountingThings {
  ghost var N: nat
  ghost var Repr: set<object>
  var incs: Cell
  var decs: Cell

  predicate Valid()
    reads this, Repr
  {
    this in Repr && this.incs in Repr && this.decs in Repr &&
    incs != decs &&
    N == incs.data - decs.data
  }

  constructor ()
    ensures Valid()
    ensures N == 0
  {
    incs := new Cell(0);
    decs := new Cell(0);
    N := 0;
    Repr := {this, incs, decs};
  }

  method Inc()
    requires Valid()
    modifies Repr
    ensures Valid()
    ensures N == old(N) + 1
  {
    N, incs.data := N + 1, incs.data + 1;
  }
}

method TestHarness() {
  var d := new Counter();
  var c := new Counter();
  assert c.N == 0;
  c.Inc();
  assert d.N == 0;
  c.Inc();
  assert c.N == 2;
}

*/

















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

method FibSquare(n: nat) returns (x: nat)
  ensures x == Fib(n) * Fib(n)
{
  x := 0;
  var y, z := 1, 0;
  for i := 0 to n
    invariant 0 <= i <= n
    invariant x == Fib(i) * Fib(i)
    invariant y == Fib(i + 1) * Fib(i + 1)
    invariant z == 2 * Fib(i) * Fib(i + 1)
  {
    x, y, z := y, x + z + y, z + y + y;
  }
}

method Main() {
  var x := FibSquare(5);
  assert x == 25;
  print x, "\n";
}