Require Import VST.floyd.proofauto.
Require Import VST.progs.odd.
Require Import VST.progs.verif_evenodd_spec.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.

Definition Gprog : funspecs :=
     ltac:(with_library prog [odd_spec; even_spec]).

Lemma body_odd : semax_body Vprog Gprog f_odd odd_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_odd odd_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp even._n (Vint (Int.repr z))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _n tuint) (Econst_int (Int.repr Z0) tint) tint) (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))) Sskip) MORE_COMMANDS) POSTCONDITION *)
change even._n with _n.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr z))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Sifthenelse (Ebinop Oeq (Etempvar _n tuint) (Econst_int (Int.repr Z0) tint) tint) (Sreturn (@Some expr (Econst_int (Int.repr Z0) tint))) Sskip) MORE_COMMANDS) POSTCONDITION *)
forward_if.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (if Z.even (Z.sub z (Zpos xH)) then Int.one else Int.zero))) (@cons localdef (temp _n (Vint (Int.repr z))) (@nil localdef))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _t'1 tint))) POSTCONDITION *)
 forward.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _n (Vint (Int.repr z))) (@nil localdef)) (SEPx (@nil mpred)))) (Ssequence (Scall (@Some ident _t'1) (Evar _even (Tfunction (Tcons tuint Tnil) tint cc_default)) (@cons expr (Ebinop Osub (Etempvar _n tuint) (Econst_int (Int.repr (Zpos xH)) tint) tuint) (@nil expr))) MORE_COMMANDS) POSTCONDITION *)
  forward_call (z-1).
(* Goal: and (Z.le Z0 (Z.sub z (Zpos xH))) (Z.le (Z.sub z (Zpos xH)) Int.max_signed) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (if Z.even (Z.sub z (Zpos xH)) then Int.one else Int.zero))) (@cons localdef (temp _n (Vint (Int.repr z))) (@nil localdef))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _t'1 tint))) POSTCONDITION *)
  omega.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t'1 (Vint (if Z.even (Z.sub z (Zpos xH)) then Int.one else Int.zero))) (@cons localdef (temp _n (Vint (Int.repr z))) (@nil localdef))) (SEPx (@nil mpred)))) (Sreturn (@Some expr (Etempvar _t'1 tint))) POSTCONDITION *)
  forward.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric (@eq val (Vint (if Z.even (Z.sub z (Zpos xH)) then Int.one else Int.zero)) (Vint (if Z.odd z then Int.one else Int.zero)))) *)
  entailer!.
(* Goal: @eq val (Vint (if Z.even (Z.sub z (Zpos xH)) then Int.one else Int.zero)) (Vint (if Z.odd z then Int.one else Int.zero)) *)
  rewrite Z.even_sub; simpl.
  case_eq (Z.odd z); rewrite Zodd_even_bool;
  destruct (Z.even z); simpl; try (intros; congruence).
Qed.

(* The Espec for odd is different from the Espec for even;
  the former has only "even" as an external function, and vice versa. *)
Definition Espec := add_funspecs NullExtension.Espec (ext_link_prog odd.prog) Gprog.
Existing Instance Espec.

(* Can't prove   prog_correct: semax_prog prog Vprog Gprog
  because there is no _main function, so prove all_funcs_correct instead. *)
Lemma all_funcs_correct:
  semax_func Vprog Gprog (prog_funct prog) Gprog.
Proof.
(* Goal: semax_func Espec Vprog Gprog CompSpecs (prog_funct prog) Gprog *)
repeat (apply semax_func_cons_ext_vacuous; [reflexivity | reflexivity | ]).
(* Goal: semax_func Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _even (@External function (EF_external (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false true true false true true true false) (String (Ascii.Ascii true false true false false true true false) (String (Ascii.Ascii false true true true false true true false) EmptyString)))) (mksignature (@cons typ AST.Tint (@nil typ)) (@Some typ AST.Tint) cc_default)) (Tcons tuint Tnil) tint cc_default)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _odd (@Internal function f_odd)) (@nil (prod ident (fundef function))))) (@cons (prod ident funspec) (@pair ident funspec _even (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type even._n tuint) (@nil (prod ident type))) tint) cc_default Z (fun z : Z => PROPx (@cons Prop (and (Z.le Z0 z) (Z.le z Int.max_signed)) (@nil Prop)) (LOCALx (@cons localdef (temp even._n (Vint (Int.repr z))) (@nil localdef)) (SEPx (@nil mpred)))) (fun z : Z => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (if Z.even z then Int.one else Int.zero))) (@nil localdef)) (SEPx (@nil mpred)))))) (@cons (prod ident funspec) (@pair ident funspec _odd (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type even._n tuint) (@nil (prod ident type))) tint) cc_default (prod Z unit) (fun x : prod Z unit => let (z, _) := x in PROPx (@cons Prop (and (Z.le Z0 z) (Z.le z Int.max_signed)) (@nil Prop)) (LOCALx (@cons localdef (temp even._n (Vint (Int.repr z))) (@nil localdef)) (SEPx (@nil mpred)))) (fun x : prod Z unit => let (z, _) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (if Z.odd z then Int.one else Int.zero))) (@nil localdef)) (SEPx (@nil mpred)))))) (@nil (prod ident funspec)))) *)
semax_func_cons_ext.
(* Goal: semax_func Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _odd (@Internal function f_odd)) (@nil (prod ident (fundef function)))) (@cons (prod ident funspec) (@pair ident funspec _odd (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type even._n tuint) (@nil (prod ident type))) tint) cc_default (prod Z unit) (fun x : prod Z unit => let (z, _) := x in PROPx (@cons Prop (and (Z.le Z0 z) (Z.le z Int.max_signed)) (@nil Prop)) (LOCALx (@cons localdef (temp even._n (Vint (Int.repr z))) (@nil localdef)) (SEPx (@nil mpred)))) (fun x : prod Z unit => let (z, _) := x in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (if Z.odd z then Int.one else Int.zero))) (@nil localdef)) (SEPx (@nil mpred)))))) (@nil (prod ident funspec))) *)
semax_func_cons body_odd.
Qed.
