Toccata

(* Euler Project, problem 2

Each new term in the Fibonacci sequence is generated by adding the
previous two terms. By starting with 1 and 2, the first 10 terms will
be:

1, 2, 3, 5, 8, 13, 21, 34, 55, 89, ...

By considering the terms in the Fibonacci sequence whose values do not
exceed four million, find the sum of the even-valued terms. *)

Sum of even-valued Fibonacci numbers

theory FibSumEven

  use int.Int
  use int.Fibonacci
  use int.ComputerDivision

  (* [fib_sum_even m n] is the sum of even-valued terms of the
      Fibonacci sequence from index 0 to n-1, that do not exceed m *)
  function fib_sum_even int int : int

  axiom SumZero: forall m:int. fib_sum_even m 0 = 0

  axiom SumEvenLe: forall n m:int.
     n >= 0 -> fib n <= m -> mod (fib n) 2 = 0 ->
       fib_sum_even m (n+1) = fib_sum_even m n + fib n

  axiom SumEvenGt: forall n m:int.
     n >= 0 -> fib n > m -> mod (fib n) 2 = 0 ->
       fib_sum_even m (n+1) = fib_sum_even m n

  axiom SumOdd: forall n m:int.
     n >= 0 -> mod (fib n) 2 <> 0 ->
       fib_sum_even m (n+1) = fib_sum_even m n

  predicate is_fib_sum_even (m:int) (sum:int) =
    exists n:int.
      sum = fib_sum_even m n /\ fib n > m
   (* Note: we take for granted that [fib] is an
        increasing sequence *)

end

module FibOnlyEven

  use int.Int
  use int.ComputerDivision
  use int.Fibonacci

  let rec lemma fib_even_3n (n:int)
    requires { n >= 0 }
    variant { n }
    ensures { mod (fib n) 2 = 0 <-> mod n 3 = 0 }
  = if n > 2 then fib_even_3n (n-3)

  function fib_even (n: int) : int = fib (3 * n)

  lemma fib_even0: fib_even 0 = 0
  lemma fib_even1: fib_even 1 = 2

  lemma fib_evenn: forall n:int [fib_even n].
     n >= 2 -> fib_even n = 4 * fib_even (n-1) + fib_even (n-2)

end

module Solve

  use int.Int
  use ref.Ref
  use int.Fibonacci
  use FibSumEven
  use FibOnlyEven

  let f m : int
    requires { m >= 0 }
    ensures  { exists n:int. result = fib_sum_even m n /\ fib n > m }
  = let x = ref 0 in
    let y = ref 2 in
    let sum = ref 0 in
    let ghost n = ref 0 in
    let ghost k = ref 0 in
    while !x <= m do
      invariant { !n >= 0 }
      invariant { !k >= 0 }
      invariant { !x = fib_even !n }
      invariant { !x = fib !k }
      invariant { !y = fib_even (!n+1) }
      invariant { !y = fib (!k+3) }
      invariant { !sum = fib_sum_even m !k }
      invariant { 0 <= !x < !y }
      variant { m - !x }
      let tmp = !x in
      x := !y;
      y := 4 * !y + tmp;
      sum := !sum + tmp;
      n := !n + 1;
      k := !k + 3
    done;
    !sum

  let run () = f 4_000_000 (* should be 4613732 *)

  exception BenchFailure

  let bench () raises { BenchFailure -> true } =
    let x = run () in
    if x <> 4613732 then raise BenchFailure;
    x

end