Require Import VST.floyd.proofauto. (* Import the Verifiable C system *)
Require Import VST.progs.sumarray2. (* Import the AST of this C program *)
(* The next line is "boilerplate", always required after importing an AST. *)
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.


(* Some definitions relating to the functional spec of this particular program.  *)
Definition sum_Z : list Z -> Z := fold_right Z.add 0.

Lemma sum_Z_app:
  forall a b, sum_Z (a++b) =  sum_Z a + sum_Z b.
Proof.
(* Goal: forall (x : A) (_ : @In A x (@sublist A lo hi al)), P x *)
  intros. induction a; simpl; omega.
Qed.

(* Beginning of the API spec for the sumarray.c program *)
Definition sumarray_spec :=
 DECLARE _sumarray
  WITH a: val, sh : share, contents : list Z, size: Z
  PRE [ _a OF (tptr tuint), _n OF tint ]
          PROP  (readable_share sh; 0 <= size <= Int.max_signed)
          LOCAL (temp _a a; temp _n (Vint (Int.repr size)))
          SEP   (data_at sh (tarray tuint size) (map Vint (map Int.repr contents)) a)
  POST [ tuint ]
        PROP () LOCAL(temp ret_temp  (Vint (Int.repr (sum_Z contents))))
           SEP (data_at sh (tarray tuint size) (map Vint (map Int.repr contents)) a).

(* The precondition of "int main(void){}" always looks like this. *)
Definition main_spec :=
 DECLARE _main
  WITH gv: globals
  PRE  [] main_pre prog nil gv
  POST [ tint ]  
     PROP() 
     LOCAL (temp ret_temp (Vint (Int.repr (3+4)))) 
     SEP(TT).

(* Packaging the API spec all together. *)
Definition Gprog : funspecs :=
        ltac:(with_library prog [sumarray_spec; main_spec]).

(** Proof that f_sumarray, the body of the sumarray() function,
 ** satisfies sumarray_spec, in the global context (Vprog,Gprog).
 **)
Lemma body_sumarray: semax_body Vprog Gprog f_sumarray sumarray_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_sumarray sumarray_spec *)
start_function.  (* Always do this at the beginning of a semax_body proof *)
(* The next two lines do forward symbolic execution through
   the first two executable statements of the function body *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
forward.  (* s = 0; *)
forward_for_simple_bound size
  (EX i: Z,
   PROP  ((*0 <= i <= size*))
   LOCAL (temp _a a;
          (*temp _i (Vint (Int.repr i)); *)
          temp _n (Vint (Int.repr size));
          temp _s (Vint (Int.repr (sum_Z (sublist 0 i contents)))))
   SEP   (data_at sh (tarray tuint size) (map Vint (map Int.repr contents)) a)).

* (* Prove that current precondition implies loop invariant *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))))) *)
entailer!.
* (* Prove postcondition of loop body implies loop invariant *)
(* "forward" fails and tells us to first make (0 <= i < Zlength contents)
   provable by auto, so we assert the following: *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _a (tptr tuint)) (Etempvar _i tint) (tptr tuint)) tuint)) MORE_COMMANDS) POSTCONDITION *)
assert_PROP (Zlength contents = size). {
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))))) *)
  entailer!. do 2 rewrite Zlength_map. reflexivity.
}
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
forward. (* x = a[i] *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
forward. (* s += x; *)
 (* Now we have reached the end of the loop body, and it's
   time to prove that the _current precondition_  (which is the
   postcondition of the loop body) entails the loop invariant. *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))))) *)
entailer!.
(* Goal: @eq Int.int (Int.repr (sum_Z (@sublist Z Z0 (Z.add i (Zpos xH)) contents))) (Int.repr (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents))) *)
 f_equal. f_equal.
(* Goal: @eq Z (sum_Z (@sublist Z Z0 (Z.add i (Zpos xH)) contents)) (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) *)
 rewrite (sublist_split 0 i (i+1)) by omega.
(* Goal: @eq Z (sum_Z (@app Z (@sublist Z Z0 i contents) (@sublist Z i (Z.add i (Zpos xH)) contents))) (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) *)
 rewrite sum_Z_app. rewrite (sublist_one i) by omega.
(* Goal: @eq Z (Z.add (sum_Z (@sublist Z Z0 i contents)) (sum_Z (@cons Z (@Znth Z Inhabitant_Z i contents) (@nil Z)))) (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) *)
 simpl. autorewrite with sublist. normalize.
* (* After the loop *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
forward.  (* return s; *)
 (* Here we prove that the postcondition of the function body
    entails the postcondition demanded by the function specification. *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))))) *)
entailer!.
autorewrite with sublist in *.
(* Goal: @eq Z (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) *)
reflexivity.
Qed.

(* Contents of the extern global initialized array "_four" *)
Definition four_contents := [1; 2; 3; 4].

(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq Z (@Zlength Z contents) size)) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _a (tptr tuint)) (Etempvar _i tint) (tptr tuint)) tuint)) MORE_COMMANDS) POSTCONDITION *)
Lemma Forall_sublist: forall {A} (P: A->Prop) lo hi (al: list A),
  Forall P al -> Forall P (sublist lo hi al).
Proof.
(* Goal: forall (x : A) (_ : @In A x (@sublist A lo hi al)), P x *)
intros.
(* Goal: @Forall A P (@sublist A lo hi al) *)
apply Forall_forall. rewrite -> Forall_forall in H.
(* Goal: forall (x : A) (_ : @In A x (@sublist A lo hi al)), P x *)
intros.
(* Goal: P x *)
apply H; auto.
(* Goal: @In A x al *)
apply sublist_In in H0. auto.
Qed.

Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_sumarray sumarray_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@cons Int.int (Int.repr (Zpos xH)) (@cons Int.int (Int.repr (Zpos (xO xH))) (@cons Int.int (Int.repr (Zpos (xI xH))) (@cons Int.int (Int.repr (Zpos (xO (xO xH)))) (@nil Int.int)))))) (gv _four)) (@nil mpred))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _sumarray (Tfunction (Tcons (tptr tuint) (Tcons tint Tnil)) tuint cc_default)) (@cons expr (Ebinop Oadd (Evar _four (tarray tuint (Zpos (xO (xO xH))))) (Econst_int (Int.repr (Zpos (xO xH))) tint) (tptr tuint)) (@cons expr (Econst_int (Int.repr (Zpos (xO xH))) tint) (@nil expr)))) (Sset _s (Etempvar _t'1 tuint))) (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint)))) MORE_COMMANDS) POSTCONDITION *)
set (four := gv _four).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@cons Int.int (Int.repr (Zpos xH)) (@cons Int.int (Int.repr (Zpos (xO xH))) (@cons Int.int (Int.repr (Zpos (xI xH))) (@cons Int.int (Int.repr (Zpos (xO (xO xH)))) (@nil Int.int)))))) four) (@nil mpred))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _sumarray (Tfunction (Tcons (tptr tuint) (Tcons tint Tnil)) tuint cc_default)) (@cons expr (Ebinop Oadd (Evar _four (tarray tuint (Zpos (xO (xO xH))))) (Econst_int (Int.repr (Zpos (xO xH))) tint) (tptr tuint)) (@cons expr (Econst_int (Int.repr (Zpos (xO xH))) tint) (@nil expr)))) (Sset _s (Etempvar _t'1 tuint))) (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint)))) MORE_COMMANDS) POSTCONDITION *)
change [Int.repr 1; Int.repr 2; Int.repr 3; Int.repr 4] with (map Int.repr four_contents).
set (contents :=  map Vint (map Int.repr four_contents)).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) contents four) (@nil mpred))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _sumarray (Tfunction (Tcons (tptr tuint) (Tcons tint Tnil)) tuint cc_default)) (@cons expr (Ebinop Oadd (Evar _four (tarray tuint (Zpos (xO (xO xH))))) (Econst_int (Int.repr (Zpos (xO xH))) tint) (tptr tuint)) (@cons expr (Econst_int (Int.repr (Zpos (xO xH))) tint) (@nil expr)))) (Sset _s (Etempvar _t'1 tuint))) (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint)))) MORE_COMMANDS) POSTCONDITION *)
assert (Zlength contents = 4) by (subst contents; reflexivity).
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))))) *)
assert_PROP (field_compatible (tarray tuint 4) [] four) by entailer!.
assert (Forall (fun x : Z => Int.min_signed <= x <= Int.max_signed) four_contents)
  by (repeat constructor; computable).
 rewrite <- (sublist_same 0 4 contents), (sublist_split 0 2 4)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents)))) (Vint (Int.repr (sum_Z contents))))) *)
    by now autorewrite with sublist.
(* Goal: @eq Z (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) *)
erewrite (split2_data_at_Tarray_app 2 4); try apply JMeq_refl; auto; try omega; try reflexivity.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (gvars gv) (@nil localdef)) (SEPx (@cons mpred (@sepcon mpred Nveric Sveric (@data_at CompSpecs Ews (tarray tuint (Zpos (xO xH))) (@sublist val Z0 (Zpos (xO xH)) contents) four) (@data_at CompSpecs Ews (tarray tuint (Z.sub (Zpos (xO (xO xH))) (Zpos (xO xH)))) (@sublist val (Zpos (xO xH)) (Zpos (xO (xO xH))) contents) (@field_address0 CompSpecs (tarray tuint (Zpos (xO (xO xH)))) (@cons gfield (ArraySubsc (Zpos (xO xH))) (@nil gfield)) four))) (@nil mpred))))) (Ssequence (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _sumarray (Tfunction (Tcons (tptr tuint) (Tcons tint Tnil)) tuint cc_default)) (@cons expr (Ebinop Oadd (Evar _four (tarray tuint (Zpos (xO (xO xH))))) (Econst_int (Int.repr (Zpos (xO xH))) tint) (tptr tuint)) (@cons expr (Econst_int (Int.repr (Zpos (xO xH))) tint) (@nil expr)))) (Sset _s (Etempvar _t'1 tuint))) (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint)))) MORE_COMMANDS) POSTCONDITION *)
Intros.
forward_call (*  s = sumarray(four+2,2); *)
  (field_address0 (tarray tuint 4) [ArraySubsc 2] four, Ews,
    sublist 2 4 four_contents,2).
+
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))))) *)
 entailer!.
(* Goal: @eq (option val) (@Some val (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) tuint) (Zpos (xO xH))) (gv _four))) (@Some val (@field_address0 CompSpecs (tarray tuint (Zpos (xO (xO xH)))) (@cons gfield (ArraySubsc (Zpos (xO xH))) (@nil gfield)) four)) *)
 rewrite field_address0_offset by auto with field_compatible.
(* Goal: @eq (option val) (@Some val (offset_val (Z.mul (@sizeof (@cenv_cs CompSpecs) tuint) (Zpos (xO xH))) (gv _four))) (@Some val (offset_val (@nested_field_offset CompSpecs (tarray tuint (Zpos (xO (xO xH)))) (@cons gfield (ArraySubsc (Zpos (xO xH))) (@nil gfield))) four)) *)
 normalize.
(* Goal: readable_share Ews *)
(* Goal: and (Z.le Z0 (Zpos (xO xH))) (Z.le (Zpos (xO xH)) Int.max_signed) *)
+ split. auto. computable.
+
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z (Zpos (xO xH)) (Zpos (xO (xO xH))) four_contents))))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO xH))) (@map Int.int val Vint (@map Z Int.int Int.repr (@sublist Z (Zpos (xO xH)) (Zpos (xO (xO xH))) four_contents))) (@field_address0 CompSpecs (tarray tuint (Zpos (xO (xO xH)))) (@cons gfield (ArraySubsc (Zpos (xO xH))) (@nil gfield)) four)) (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO xH))) (@sublist val Z0 (Zpos (xO xH)) contents) four) (@nil mpred)))))) (Ssequence (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint))) MORE_COMMANDS) POSTCONDITION *)
  gather_SEP 1 2.
(* Goal: @eq Z (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) *)
  erewrite <- (split2_data_at_Tarray_app 2 4); try apply JMeq_refl; auto; try omega; try reflexivity.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents)))) (Vint (Int.repr (sum_Z contents))))) *)
  rewrite <- !sublist_map. fold contents. autorewrite with sublist.
(* Goal: readable_share Ews *)
(* Goal: and (Z.le Z0 (Zpos (xO xH))) (Z.le (Zpos (xO xH)) Int.max_signed) *)
  rewrite (sublist_same 0 4) by auto.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
  forward. (* return *)
Qed.

Existing Instance NullExtension.Espec.

Lemma prog_correct:
  semax_prog prog Vprog Gprog.
Proof.
(* Goal: semax_prog NullExtension.Espec CompSpecs prog Vprog Gprog *)
prove_semax_prog.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _sumarray (@Internal function f_sumarray)) (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function))))) (@cons (prod ident funspec) (@pair ident funspec _sumarray (NDmk_funspec (@pair (list (prod ident type)) type (@cons (prod ident type) (@pair ident type _a (tptr tuint)) (@cons (prod ident type) (@pair ident type _n tint) (@nil (prod ident type)))) tuint) cc_default (prod (prod (prod val share) (list Z)) Z) (fun x : prod (prod (prod val share) (list Z)) Z => let (p, size) := x in let (p0, contents) := p in let (a, sh) := p0 in PROPx (@cons Prop (readable_share sh) (@cons Prop (and (Z.le Z0 size) (Z.le size Int.max_signed)) (@nil Prop))) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (fun x : prod (prod (prod val share) (list Z)) Z => let (p, size) := x in let (p0, contents) := p in let (a, sh) := p0 in PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (sum_Z contents)))) (@nil localdef)) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO (xO xH))))))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec)))) *)
semax_func_cons body_sumarray.
(* Goal: semax_func NullExtension.Espec Vprog Gprog CompSpecs (@cons (prod ident (fundef function)) (@pair ident (fundef function) _main (@Internal function f_main)) (@nil (prod ident (fundef function)))) (@cons (prod ident funspec) (@pair ident funspec _main (NDmk_funspec (@pair (list (prod ident type)) type (@nil (prod ident type)) tint) cc_default globals (fun gv : globals => main_pre prog (@nil Type) gv) (fun _ : globals => PROPx (@nil Prop) (LOCALx (@cons localdef (temp ret_temp (Vint (Int.repr (Z.add (Zpos (xI xH)) (Zpos (xO (xO xH))))))) (@nil localdef)) (SEPx (@cons mpred (@TT mpred Nveric) (@nil mpred))))))) (@nil (prod ident funspec))) *)
semax_func_cons body_main.
Qed.

(**  Here begins an alternate proof of the "for" loop.
  Instead of using forward_for_simple_bound, we use the 
  general-case loop tactic, forward_for.

To understand this verification, let's take the program,

(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq Z (@Zlength Z contents) size)) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _a (tptr tuint)) (Etempvar _i tint) (tptr tuint)) tuint)) MORE_COMMANDS) POSTCONDITION *)
  int sumarray(int a[], int n) {
     int i,s,x;
     s=0;
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq Z (@Zlength Z contents) size)) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _a (tptr tuint)) (Etempvar _i tint) (tptr tuint)) tuint)) MORE_COMMANDS) POSTCONDITION *)
     for (i=0; i<n; i++) {
       x = a[i];
       s += x;
     }
     return s;
  }

and annotate with assertions:


(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq Z (@Zlength Z contents) size)) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _a (tptr tuint)) (Etempvar _i tint) (tptr tuint)) tuint)) MORE_COMMANDS) POSTCONDITION *)
  int sumarray(int a[], int n) {
     int i,s,x;
     s=0;
(* Goal: @derives (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@andp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (local (tc_environ Delta)) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred)))))) (@prop (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (@eq Z (@Zlength Z contents) size)) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr i))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _a (tptr tuint)) (Etempvar _i tint) (tptr tuint)) tuint)) MORE_COMMANDS) POSTCONDITION *)
     for (i=0; i<n; i++) {
       assert (sumarray_Inv(i));
       x = a[i];
       s += x;
       assert (sumarray_PostBody(i));
     }
     return s;
  }

The assertions are defined in these definitions:
*)
Definition sumarray_Inv a sh contents size i :=
   PROP  (0 <= i <= size)
   LOCAL (temp _a a;
          temp _i (Vint (Int.repr i));
          temp _n (Vint (Int.repr size));
          temp _s (Vint (Int.repr (sum_Z (sublist 0 i contents)))))
   SEP   (data_at sh (tarray tuint size) (map Vint (map Int.repr contents)) a).

Definition sumarray_PostBody a sh contents size i :=
   PROP  (0 <= i < size)
   LOCAL (temp _a a;
          temp _i (Vint (Int.repr i));
          temp _n (Vint (Int.repr size));
          temp _s (Vint (Int.repr (sum_Z (sublist 0 (i+1) contents)))))
   SEP   (data_at sh (tarray tuint size) (map Vint (map Int.repr contents)) a).

(* . . . and now you can see how these assertions are used
   in the proof, using the semax_loop rule. *)

Lemma body_sumarray_alt: semax_body Vprog Gprog f_sumarray sumarray_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_sumarray sumarray_spec *)
start_function.  (* Always do this at the beginning of a semax_body proof *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
forward.  (* s = 0; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vint (Int.repr Z0))) (@cons localdef (temp _a a) (@cons localdef (temp _n (Vint (Int.repr size))) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Sfor (Sset _i (Econst_int (Int.repr Z0) tint)) (Ebinop Olt (Etempvar _i tint) (Etempvar _n tint) tint) (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _a (tptr tuint)) (Etempvar _i tint) (tptr tuint)) tuint)) (Sset _s (Ebinop Oadd (Etempvar _s tuint) (Etempvar _t'1 tuint) tuint))) (Sset _i (Ebinop Oadd (Etempvar _i tint) (Econst_int (Int.repr (Zpos xH)) tint) tint))) MORE_COMMANDS) POSTCONDITION *)
forward_for (sumarray_Inv a sh contents size).
* (* initializer establishes precondition *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
forward. (* i=0; *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))))) *)
unfold sumarray_Inv. Exists 0. entailer!.
* (* loop-test expression typechecks *)
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))))) *)
entailer!.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Ssequence (Ssequence (Sset _t'1 (Ederef (Ebinop Oadd (Etempvar _a (tptr tuint)) (Etempvar _i tint) (tptr tuint)) tuint)) (Sset _s (Ebinop Oadd (Etempvar _s tuint) (Etempvar _t'1 tuint) tuint))) MORE_COMMANDS) POSTCONDITION *)
rename x into i.
assert_PROP (size=Zlength contents)
  by (entailer!; autorewrite with sublist; auto).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
forward. (* x = a[i]; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
forward. (* s += x; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
forward.  (* i++; *)
Exists (i+1).
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))))) *)
entailer!.
(* Goal: @eq Int.int (Int.repr (sum_Z (@sublist Z Z0 (Z.add i (Zpos xH)) contents))) (Int.repr (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents))) *)
     f_equal. f_equal.
(* Goal: @eq Z (sum_Z (@sublist Z Z0 (Z.add i (Zpos xH)) contents)) (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) *)
     rewrite (sublist_split 0 i (i+1)) by omega.
(* Goal: @eq Z (sum_Z (@app Z (@sublist Z Z0 i contents) (@sublist Z i (Z.add i (Zpos xH)) contents))) (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) *)
     rewrite sum_Z_app. rewrite (sublist_one i) by omega.
(* Goal: @eq Z (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)) *)
     simpl. autorewrite with sublist norm. reflexivity.
* (* after the loop *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr x))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents))))) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh (tarray tuint size) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@nil mpred))))) (Sreturn (@Some expr (Etempvar _s tuint))) POSTCONDITION *)
forward. (* return s; *)
autorewrite with sublist in *.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z (@sublist Z Z0 x contents)))) (Vint (Int.repr (sum_Z contents))))) *)
autorewrite with sublist.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength Z contents)) (@map Int.int val Vint (@map Z Int.int Int.repr contents)) a) (@prop mpred Nveric (@eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))))) *)
entailer!.
Qed.
