Require Import VST.floyd.proofauto. (* Import the Verifiable C system *)
Require Import VST.progs.sumarray. (* 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.


(* Functional spec of this 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 a b : list Z, @eq Z (sum_Z (@app Z a b)) (Z.add (sum_Z a) (sum_Z b)) *)
  intros. induction a; simpl; omega.
Qed.

(* Beginning of the API spec for the sumarray.c program *)
Definition sumarray_spec : ident * funspec :=
 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;
          Forall (fun x => 0 <= x <= Int.max_unsigned) contents)
          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).

(* Note: It would also be reasonable to let [contents] have type [list int].
  Then the [Forall] would not be needed in the PROP part of PRE.
*)

(* 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 (1+2+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_main main_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 _s (Vint (Int.repr (sum_Z four_contents)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr four_contents)) (gv _four)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* i = 0; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vint (Int.repr (sum_Z four_contents)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr four_contents)) (gv _four)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint))) MORE_COMMANDS) POSTCONDITION *)
forward.  (* s = 0; *)
(* To do symbolic execution through a [while] loop, we must
 * provide a loop invariant, so we use [forward_while] with
 * the invariant as an argument .*)
forward_while
 (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)).
(* forward_while leaves four subgoals; here we label them
   with the * bullet. *)
* (* Prove that current precondition implies loop invariant *)
Exists 0.   (* Instantiate the existential on the right-side of |--   *)
entailer!.  (* Simplify this entailment as much as possible; in this
      case, it solves entirely; in other cases, entailer! leaves subgoals *)
* (* Prove that loop invariant implies typechecking condition *)
entailer!.  (* Typechecking conditions usually solve quite easily *)
* (* Prove postcondition of loop body implies loop invariant *)
(* In order to get to the postcondition of the loop body, of course,
   we must forward-symbolic-execute through the loop body;
   so we start that here. *)
(* "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 _a a) (@cons localdef (temp _i (Vint (Int.repr i))) (@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 (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 *)
assert_PROP (Zlength contents = size). {
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength (@reptype CompSpecs tuint) (@map Int.int val Vint (@map Z Int.int Int.repr 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 i 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 _s (Vint (Int.repr (sum_Z four_contents)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr four_contents)) (gv _four)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint))) MORE_COMMANDS) POSTCONDITION *)
forward. (* x = a[i] *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vint (Int.repr (sum_Z four_contents)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr four_contents)) (gv _four)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint))) MORE_COMMANDS) POSTCONDITION *)
forward. (* s += x; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vint (Int.repr (sum_Z four_contents)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr four_contents)) (gv _four)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint))) MORE_COMMANDS) POSTCONDITION *)
forward. (* i++; *) 
 (* 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 (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.add (Int.repr i) (Int.repr (Zpos xH))))) (@cons localdef (temp _s (Vint (Int.add (Int.repr (sum_Z (@sublist Z Z0 i contents))) (Int.repr (@Znth Z Inhabitant_Z i contents))))) (@cons localdef (temp _t'1 (Vint (Int.repr (@Znth Z Inhabitant_Z i contents)))) (@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)))))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) Z (fun a0 : Z => PROPx (@cons Prop (and (Z.le Z0 a0) (Z.le a0 size)) (@nil Prop)) (LOCALx (@cons localdef (temp _a a) (@cons localdef (temp _i (Vint (Int.repr a0))) (@cons localdef (temp _n (Vint (Int.repr size))) (@cons localdef (temp _s (Vint (Int.repr (sum_Z (@sublist Z Z0 a0 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)))))) *)
 Exists (i+1).
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh (tarray tuint (@Zlength (@reptype CompSpecs tuint) (@map Int.int val Vint (@map Z Int.int Int.repr 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 i contents)))) (Vint (Int.repr (sum_Z contents))))) *)
 entailer!. simpl.
(* Goal: @eq val (Vint (Int.repr (sum_Z (@sublist Z Z0 (Z.add i (Zpos xH)) contents)))) (Vint (Int.repr (Z.add (sum_Z (@sublist Z Z0 i contents)) (@Znth Z Inhabitant_Z i contents)))) *)
 f_equal.
(* 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))) *)
 rewrite (sublist_split 0 i (i+1)) by omega.
(* Goal: @eq Int.int (Int.repr (sum_Z (@app Z (@sublist Z Z0 i contents) (@sublist Z i (Z.add i (Zpos xH)) contents)))) (Int.repr (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 val (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents)))) (Vint (Int.repr (sum_Z contents))) *)
 autorewrite with sublist. normalize.
(* Goal: @eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))) *)
 simpl. rewrite Z.add_0_r. reflexivity.
* (* After the loop *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vint (Int.repr (sum_Z four_contents)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr four_contents)) (gv _four)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint))) MORE_COMMANDS) 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 (@reptype CompSpecs tuint) (@map Int.int val Vint (@map Z Int.int Int.repr 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 i contents)))) (Vint (Int.repr (sum_Z contents))))) *)
entailer!.
autorewrite with sublist in *.
(* Goal: @eq val (Vint (Int.repr (sum_Z (@sublist Z Z0 i contents)))) (Vint (Int.repr (sum_Z contents))) *)
autorewrite with sublist.
(* Goal: @eq val (Vint (Int.repr (sum_Z contents))) (Vint (Int.repr (sum_Z contents))) *)
reflexivity.
Qed.

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

Lemma body_main:  semax_body Vprog Gprog f_main main_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_main main_spec *)
start_function.
forward_call (*  s = sumarray(four,4); *)
  (gv _four, Ews,four_contents,4).
(* Goal: and (readable_share Ews) (and (and (Z.le Z0 (Zpos (xO (xO xH)))) (Z.le (Zpos (xO (xO xH))) Int.max_signed)) (@Forall Z (fun x : Z => and (Z.le Z0 x) (Z.le x Int.max_unsigned)) four_contents)) *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vint (Int.repr (sum_Z four_contents)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr four_contents)) (gv _four)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint))) MORE_COMMANDS) POSTCONDITION *)
 split3. auto. computable. repeat constructor; computable.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _s (Vint (Int.repr (sum_Z four_contents)))) (@cons localdef (gvars gv) (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Ews (tarray tuint (Zpos (xO (xO xH)))) (@map Int.int val Vint (@map Z Int.int Int.repr four_contents)) (gv _four)) (@nil mpred))))) (Ssequence (Sreturn (@Some expr (Ecast (Etempvar _s tuint) tint))) MORE_COMMANDS) POSTCONDITION *)
forward. (* return s; *)
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)) (@cons Prop (@Forall Z (fun x0 : Z => and (Z.le Z0 x0) (Z.le x0 Int.max_unsigned)) contents) (@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 (Z.add (Z.add (Zpos xH) (Zpos (xO xH))) (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 (Z.add (Z.add (Zpos xH) (Zpos (xO xH))) (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.

