Require Import VST.floyd.proofauto.
Require Import VST.progs.loop_minus1.

Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs.  mk_varspecs prog. Defined.

Definition sum_Z : list Z -> Z := fold_right Z.add 0.

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).

Definition Gprog : funspecs := ltac:(with_library prog [sumarray_spec]).

Lemma sum_Z_app:
  forall a b, sum_Z (a++b) =  sum_Z a + sum_Z b.
(* Goal: forall a b : list Z, @eq Z (sum_Z (@app Z a b)) (Z.add (sum_Z a) (sum_Z b)) *)
Proof. intros. induction a; simpl; omega. Qed.

Lemma body_sumarray: semax_body Vprog Gprog f_sumarray sumarray_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 (temp _i (Vint (Int.repr (Z.sub size (Zpos xH))))) (@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 (Z.add (Z.sub size (Zpos xH)) (Zpos xH)) 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.
  forward_for_simple_bound
    (size - 1)
    (EX i: Z,
     PROP  ()
     LOCAL (temp _a a;
            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)).
  - entailer!.
  - assert_PROP (Zlength contents = size) by
        (entailer!; do 2 rewrite Zlength_map; reflexivity).
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr (Z.sub size (Zpos xH))))) (@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 (Z.add (Z.sub size (Zpos xH)) (Zpos xH)) 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. forward. entailer!. f_equal. f_equal.
(* Goal: @eq Z (sum_Z (@sublist Z Z0 (Z.add (Z.add i (Zpos xH)) (Zpos xH)) contents)) (Z.add (sum_Z (@sublist Z Z0 (Z.add i (Zpos xH)) contents)) (@Znth Z Inhabitant_Z (Z.add i (Zpos xH)) contents)) *)
    rewrite (sublist_split 0 (i + 1) (i + 1 + 1)) by omega.
(* Goal: @eq Z (sum_Z (@app Z (@sublist Z Z0 (Z.add i (Zpos xH)) contents) (@sublist Z (Z.add i (Zpos xH)) (Z.add (Z.add i (Zpos xH)) (Zpos xH)) contents))) (Z.add (sum_Z (@sublist Z Z0 (Z.add i (Zpos xH)) contents)) (@Znth Z Inhabitant_Z (Z.add i (Zpos xH)) contents)) *)
    rewrite sum_Z_app. rewrite (sublist_one (i + 1)) by omega.
(* Goal: @eq Z (Z.add (sum_Z (@sublist Z Z0 (Z.add i (Zpos xH)) contents)) (sum_Z (@cons Z (@Znth Z Inhabitant_Z (Z.add i (Zpos xH)) contents) (@nil Z)))) (Z.add (sum_Z (@sublist Z Z0 (Z.add i (Zpos xH)) contents)) (@Znth Z Inhabitant_Z (Z.add i (Zpos xH)) contents)) *)
    simpl. autorewrite with sublist. reflexivity.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _i (Vint (Int.repr (Z.sub size (Zpos xH))))) (@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 (Z.add (Z.sub size (Zpos xH)) (Zpos xH)) 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. entailer!.  autorewrite with sublist in *. reflexivity.
Qed.
