Require Import VST.floyd.proofauto.
Require Import VST.progs.fib.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Fixpoint fib_of_nat (n: nat): Z :=
  match n with
  | O => 0
  | S n' =>
    match n' with
    | O => 1
    | S n'' => fib_of_nat n'' + fib_of_nat n'
    end
  end.

Definition fib_of_Z (n: Z): Z := fib_of_nat (nat_of_Z n).

Theorem fib_0: fib_of_Z 0 = 0.
(* Goal: @eq Z (fib_of_nat (Nat.add (nat_of_Z (Zpos (xO xH))) (nat_of_Z n))) (Z.add (fib_of_nat (nat_of_Z n)) (fib_of_nat (Nat.add (nat_of_Z (Zpos xH)) (nat_of_Z n)))) *)
Proof. reflexivity. Qed.

Theorem fib_1: fib_of_Z 1 = 1.
(* Goal: @eq Z (fib_of_nat (Nat.add (nat_of_Z (Zpos (xO xH))) (nat_of_Z n))) (Z.add (fib_of_nat (nat_of_Z n)) (fib_of_nat (Nat.add (nat_of_Z (Zpos xH)) (nat_of_Z n)))) *)
Proof. reflexivity. Qed.

Theorem fib_rec: forall n, n >= 0 -> fib_of_Z (n + 2) = fib_of_Z n + fib_of_Z (n + 1).
Proof.
(* Goal: forall (n : Z) (_ : Z.le Z0 n), Z.le (fib_of_Z n) (fib_of_Z (Z.add n (Zpos xH))) *)
  intros.
(* Goal: Z.le Z0 (fib_of_Z n) *)
  unfold fib_of_Z.
(* Goal: @eq Z (fib_of_nat (nat_of_Z (Z.add n (Zpos (xO xH))))) (Z.add (fib_of_nat (nat_of_Z n)) (fib_of_nat (nat_of_Z (Z.add n (Zpos xH))))) *)
  rewrite !nat_of_Z_plus, !(plus_comm (nat_of_Z n)) by omega.
(* Goal: @eq Z (fib_of_nat (Nat.add (nat_of_Z (Zpos (xO xH))) (nat_of_Z n))) (Z.add (fib_of_nat (nat_of_Z n)) (fib_of_nat (Nat.add (nat_of_Z (Zpos xH)) (nat_of_Z n)))) *)
  reflexivity.
Qed.

Lemma fib_nonneg: forall n, 0 <= fib_of_Z n.
Proof.
(* Goal: forall (n : Z) (_ : Z.le Z0 n), Z.le (fib_of_Z n) (fib_of_Z (Z.add n (Zpos xH))) *)
  intros.
(* Goal: Z.le Z0 (fib_of_Z n) *)
  unfold fib_of_Z.
(* Goal: Z.le Z0 (fib_of_nat (nat_of_Z n)) *)
  forget (nat_of_Z n) as m; clear.
(* Goal: Z.le Z0 (fib_of_nat m) *)
  assert (0 <= fib_of_nat m /\ 0 <= fib_of_nat (S m)); [| tauto].
(* Goal: and (Z.le Z0 (fib_of_nat m)) (Z.le Z0 (fib_of_nat (S m))) *)
  induction m; [simpl; try omega |].
  
(* Goal: and (Z.le Z0 (fib_of_nat (S m))) (Z.le Z0 (fib_of_nat (S (S m)))) *)
  destruct IHm.
(* Goal: and (Z.le Z0 (fib_of_nat (S m))) (Z.le Z0 (fib_of_nat (S (S m)))) *)
  split; [auto |].
(* Goal: Z.le Z0 (fib_of_nat (S (S m))) *)
  change (fib_of_nat (S (S m))) with (fib_of_nat m + fib_of_nat (S m)).
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
  omega.
Qed.

Lemma fib_ordered: forall n, 0 <= n -> fib_of_Z n <= fib_of_Z (n + 1).
Proof.
(* Goal: forall (n : Z) (_ : Z.le Z0 n), Z.le (fib_of_Z n) (fib_of_Z (Z.add n (Zpos xH))) *)
  intros.
(* Goal: Z.le (fib_of_Z n) (fib_of_Z (Z.add n (Zpos xH))) *)
  destruct (zeq n 0); [subst; simpl; rewrite fib_0, fib_1; omega |].
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
  replace (n + 1) with (n - 1 + 2) by omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
  rewrite fib_rec by omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
  replace (n - 1 + 1) with n by omega.
(* Goal: Z.le (fib_of_Z n) (Z.add (fib_of_Z (Z.sub n (Zpos xH))) (fib_of_Z n)) *)
  pose proof fib_nonneg (n -1).
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
  omega.
Qed.

Lemma fib_bound: forall n, 0 <= n < 46 -> 0 <= fib_of_Z n < Int.max_signed.
Proof.
  assert (fib_of_Z 0 = 0 -> fib_of_Z (0 + 1) = 1 -> forall n, 0 <= n < 46 -> 0 <= fib_of_Z n < Int.max_signed);
    [| intros; apply H; auto].
  do 46
  match goal with
  | |- fib_of_Z ?z = ?f0  -> fib_of_Z (?z + 1) = ?f1 -> forall n, ?z <= n < 46 -> _ =>
         let f2 := eval compute in (f0 + f1) in
         assert (fib_of_Z (z + 1) = f1 -> fib_of_Z (z + 2) = f2 -> forall n, z + 1 <= n < 46 ->0 <= fib_of_Z n < Int.max_signed); [
           replace (z + 2) with (z + 1 + 1) by omega |
           intros HH0 HH1; specialize (H HH1 ltac:(rewrite fib_rec by (simpl; omega); rewrite HH0, HH1; reflexivity));
           intros; destruct (zeq z n); [subst n; rewrite HH0; rep_omega | apply H; omega] (*;
           split; [apply fib_nonneg | specialize (H (n + 1) ltac:(omega)); pose proof fib_ordered n; omega]*)
           ]
  end.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
  intros; simpl in *. omega.
Qed.

Definition fib_spec fun_id :=
 DECLARE fun_id
  WITH n : Z
  PRE  [ _n OF tint ]
     PROP (0 <= n < 45) (* 50th term is too large to be a 32bit int *)
     LOCAL (temp _n (Vint (Int.repr n)))
     SEP ()
  POST [ tint ]
     PROP () LOCAL (temp ret_temp (Vint (Int.repr (fib_of_Z n))))
     SEP ().

Definition Gprog : funspecs :=
         ltac:(with_library prog [ fib_spec _fib_loop; fib_spec _fib_loop_save_var; fib_spec _fib_rec ]).

Lemma body_fib_loop: semax_body Vprog Gprog f_fib_loop (fib_spec _fib_loop).
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_fib_rec (fib_spec _fib_rec) *)
  start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  forward.  (* a0 = 0; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  forward.  (* a1 = 1; *)
  forward_for_simple_bound n
    (EX i: Z,
    (PROP ()
     LOCAL (temp _a1 (Vint (Int.repr (fib_of_Z (i + 1)))); temp _a0 (Vint (Int.repr (fib_of_Z i))); temp _n (Vint (Int.repr n)))
     SEP ()))%assert.
(* Goal: and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos (xO xH))))) (Z.lt (fib_of_Z (Z.sub n (Zpos (xO xH)))) Int.max_signed)) (and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos xH)))) (Z.lt (fib_of_Z (Z.sub n (Zpos xH))) Int.max_signed)) (and (Z.le Z0 (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH))))) (Z.lt (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))) Int.max_signed))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  { (* Prove that loop invariant implies typechecking of loop condition *)
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric (@eq val (Vint (Int.repr (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))))) (Vint (Int.repr (fib_of_Z n))))) *)
    entailer!.
  }
(* Goal: and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos (xO xH))))) (Z.lt (fib_of_Z (Z.sub n (Zpos (xO xH)))) Int.max_signed)) (and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos xH)))) (Z.lt (fib_of_Z (Z.sub n (Zpos xH))) Int.max_signed)) (and (Z.le Z0 (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH))))) (Z.lt (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))) Int.max_signed))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  { (* Prove that loop body preserves invariant *)
    assert (0 <= fib_of_Z i < Int.max_signed /\
            0 <= fib_of_Z (i + 1) < Int.max_signed /\
            0 <= fib_of_Z i + fib_of_Z (i + 1) < Int.max_signed) as [R0 [R1 R2]].
(* Goal: and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos (xO xH))))) (Z.lt (fib_of_Z (Z.sub n (Zpos (xO xH)))) Int.max_signed)) (and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos xH)))) (Z.lt (fib_of_Z (Z.sub n (Zpos xH))) Int.max_signed)) (and (Z.le Z0 (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH))))) (Z.lt (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))) Int.max_signed))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
    {
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
      rewrite <- fib_rec by omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
      split; [| split]; apply fib_bound; omega.
    }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
    forward. (* a2 = a0 + a1; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
    forward. (* a0 = a1; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
    forward. (* a1 = a2; *)
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric (@eq val (Vint (Int.repr (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))))) (Vint (Int.repr (fib_of_Z n))))) *)
    entailer!.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
    rewrite <- fib_rec by omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
    do 3 f_equal; omega.
  }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  forward. (* return a0; *)
Qed.

Lemma body_fib_rec: semax_body Vprog Gprog f_fib_rec (fib_spec _fib_rec).
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_fib_rec (fib_spec _fib_rec) *)
  start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _n tint) (Econst_int (Int.repr (Zpos xH)) tint) tint) (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) Sskip) MORE_COMMANDS) POSTCONDITION *)
  forward_if.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  { forward. }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _n tint) (Econst_int (Int.repr (Zpos xH)) tint) tint) (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) Sskip) MORE_COMMANDS) POSTCONDITION *)
  forward_if.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  { forward. }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _fib_rec (Tfunction (Tcons tint Tnil) tint cc_default)) (@cons expr (Ebinop Osub (Etempvar _n tint) (Econst_int (Int.repr (Zpos (xO xH))) tint) tint) (@nil expr))) (Scall (@Some ident _t'2) (Evar _fib_rec (Tfunction (Tcons tint Tnil) tint cc_default)) (@cons expr (Ebinop Osub (Etempvar _n tint) (Econst_int (Int.repr (Zpos xH)) tint) tint) (@nil expr)))) MORE_COMMANDS) POSTCONDITION *)
  forward_call (n - 2).
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
    1: omega.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef))) (SEPx (@nil mpred)))) (Ssequence (Scall (@Some ident _t'2) (Evar _fib_rec (Tfunction (Tcons tint Tnil) tint cc_default)) (@cons expr (Ebinop Osub (Etempvar _n tint) (Econst_int (Int.repr (Zpos xH)) tint) tint) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
  forward_call (n - 1).
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
    1: omega.
  assert (0 <= fib_of_Z (n - 2) < Int.max_signed /\
          0 <= fib_of_Z (n - 1) < Int.max_signed /\
          0 <= fib_of_Z (n - 2) + fib_of_Z (n - 1) < Int.max_signed) as [R0 [R1 R2]].
(* Goal: and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos (xO xH))))) (Z.lt (fib_of_Z (Z.sub n (Zpos (xO xH)))) Int.max_signed)) (and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos xH)))) (Z.lt (fib_of_Z (Z.sub n (Zpos xH))) Int.max_signed)) (and (Z.le Z0 (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH))))) (Z.lt (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))) Int.max_signed))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  {
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
    replace (n - 1) with (n - 2 + 1) at 3 4 by omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
    rewrite <- fib_rec by omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
    split; [| split]; apply fib_bound; omega.
  }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  forward.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric (@eq val (Vint (Int.repr (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))))) (Vint (Int.repr (fib_of_Z n))))) *)
  entailer!.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
  replace (n - 1) with (n - 2 + 1) by omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
  rewrite <- fib_rec by omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
  do 3 f_equal; omega.
Qed.

Lemma body_fib_loop_save_var: semax_body Vprog Gprog f_fib_loop_save_var (fib_spec _fib_loop_save_var).
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_fib_rec (fib_spec _fib_rec) *)
  start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  forward.  (* a0 = 0; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  forward.  (* a1 = 1; *)
  forward_loop
    (EX i: Z,
    (PROP (0 <= i <= n)
     LOCAL (temp _a1 (Vint (Int.repr (fib_of_Z (i + 1))));
            temp _a0 (Vint (Int.repr (fib_of_Z i)));
            temp _n (Vint (Int.repr (n - i))))
     SEP ()))%assert
  break:
    (PROP ()
     LOCAL (temp _a0 (Vint (Int.repr (fib_of_Z n))))
     SEP ())%assert.
(* Goal: and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos (xO xH))))) (Z.lt (fib_of_Z (Z.sub n (Zpos (xO xH)))) Int.max_signed)) (and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos xH)))) (Z.lt (fib_of_Z (Z.sub n (Zpos xH))) Int.max_signed)) (and (Z.le Z0 (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH))))) (Z.lt (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))) Int.max_signed))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  { (* Prove that the precon implies the loop invariant *)
    Exists 0.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric (@eq val (Vint (Int.repr (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))))) (Vint (Int.repr (fib_of_Z n))))) *)
    entailer!.
  }
(* Goal: and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos (xO xH))))) (Z.lt (fib_of_Z (Z.sub n (Zpos (xO xH)))) Int.max_signed)) (and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos xH)))) (Z.lt (fib_of_Z (Z.sub n (Zpos xH))) Int.max_signed)) (and (Z.le Z0 (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH))))) (Z.lt (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))) Int.max_signed))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  { (* Prove that loop body preserves invariant *)
    Intros i.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _n tint) (Econst_int (Int.repr (Zpos xH)) tint) tint) (Sreturn (@Some expr (Econst_int (Int.repr (Zpos xH)) tint))) Sskip) MORE_COMMANDS) POSTCONDITION *)
    forward_if.
(* Goal: and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos (xO xH))))) (Z.lt (fib_of_Z (Z.sub n (Zpos (xO xH)))) Int.max_signed)) (and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos xH)))) (Z.lt (fib_of_Z (Z.sub n (Zpos xH))) Int.max_signed)) (and (Z.le Z0 (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH))))) (Z.lt (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))) Int.max_signed))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
    2:{ (* Else branch *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
      forward. (* break; *)
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
      assert (i = n) by omega.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric (@eq val (Vint (Int.repr (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))))) (Vint (Int.repr (fib_of_Z n))))) *)
      entailer!.
    }
    (* Then branch and other loop body *)
    assert (0 <= fib_of_Z i < Int.max_signed /\
            0 <= fib_of_Z (i + 1) < Int.max_signed /\
            0 <= fib_of_Z i + fib_of_Z (i + 1) < Int.max_signed) as [R0 [R1 R2]].
(* Goal: and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos (xO xH))))) (Z.lt (fib_of_Z (Z.sub n (Zpos (xO xH)))) Int.max_signed)) (and (and (Z.le Z0 (fib_of_Z (Z.sub n (Zpos xH)))) (Z.lt (fib_of_Z (Z.sub n (Zpos xH))) Int.max_signed)) (and (Z.le Z0 (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH))))) (Z.lt (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))) Int.max_signed))) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
    {
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
      rewrite <- fib_rec by omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
      split; [| split]; apply fib_bound; omega.
    }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
    forward. (* a1 = a0 + a1; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
    forward. (* a0 = a1 - a0; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
    forward. (* -- n *)
    Exists (i + 1).
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric (@eq val (Vint (Int.repr (Z.add (fib_of_Z (Z.sub n (Zpos (xO xH)))) (fib_of_Z (Z.sub n (Zpos xH)))))) (Vint (Int.repr (fib_of_Z n))))) *)
    entailer!.
    split3.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
    + rewrite <- fib_rec by omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
      do 3 f_equal; omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
    + do 2 f_equal; omega.
(* Goal: and (Z.le Z0 (fib_of_Z n)) (Z.lt (fib_of_Z n) Int.max_signed) *)
    + do 2 f_equal; omega.
  }
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'2 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos xH)))))) (@cons localdef (temp _t'1 (Vint (Int.repr (fib_of_Z (Z.sub n (Zpos (xO xH))))))) (@cons localdef (temp _n (Vint (Int.repr n))) (@nil localdef)))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Ebinop Oadd (Etempvar _t'1 tint) (Etempvar _t'2 tint) tint))) POSTCONDITION *)
  forward. (* return a0; *)
Qed.
