Require Import VST.floyd.proofauto.
Require Import VST.progs.reverse_client.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.
Definition t_struct_list := Tstruct _list noattr.

Fixpoint listrep (sigma: list int) (x: val) : mpred :=
 match sigma with
 | h::hs => 
    EX y:val, 
      data_at Tsh t_struct_list (Vint h,y) x  *  listrep hs y
 | nil => 
    !! (x = nullval) && emp
 end.

Arguments listrep sigma x : simpl never.

Lemma listrep_local_facts:
  forall sigma p,
   listrep sigma p |--
   !! (is_pointer_or_null p /\ (p=nullval <-> sigma=nil)).
Proof.
(* Goal: forall (sigma : list Int.int) (p : val), @derives mpred Nveric (listrep sigma p) (@prop mpred Nveric (and (is_pointer_or_null p) (iff (@eq val p nullval) (@eq (list Int.int) sigma (@nil Int.int))))) *)
intros.
revert p; induction sigma; 
  unfold listrep; fold listrep; intros; normalize.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@prop mpred Nveric (and (is_pointer_or_null nullval) (iff (@eq val nullval nullval) (@eq (list Int.int) (@nil Int.int) (@nil Int.int))))) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val (Vint a) y) p) (listrep sigma y)) (@prop mpred Nveric (and (is_pointer_or_null p) (iff (@eq val p nullval) (@eq (list Int.int) (@cons Int.int a sigma) (@nil Int.int))))) *)
apply prop_right; split; simpl; auto. intuition.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val (Vint a) y) p) (listrep sigma y)) (@prop mpred Nveric (and (is_pointer_or_null p) (iff (@eq val p nullval) (@eq (list Int.int) (@cons Int.int a sigma) (@nil Int.int))))) *)
entailer!.
(* Goal: iff (@eq val p nullval) (@eq (list Int.int) (@cons Int.int a sigma) (@nil Int.int)) *)
split; intro. subst p. destruct H; contradiction. inv H2.
Qed.

Hint Resolve listrep_local_facts : saturate_local.

Lemma listrep_valid_pointer:
  forall sigma p,
   listrep sigma p |-- valid_pointer p.
Proof.
 destruct sigma; unfold listrep; fold listrep;
 intros; normalize.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (valid_pointer nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val (Vint i) y) p) (listrep sigma y)) (valid_pointer p) *)
 auto with valid_pointer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val (Vint i) y) p) (listrep sigma y)) (valid_pointer p) *)
 apply sepcon_valid_pointer1.
(* Goal: @derives mpred Nveric (@data_at CompSpecs Tsh t_struct_list (@pair val val (Vint i) y) p) (valid_pointer p) *)
 apply data_at_valid_ptr; auto.
 simpl;  computable.
Qed.

Hint Resolve listrep_valid_pointer : valid_pointer.

Definition reverse_spec :=
 DECLARE _reverse
  WITH sigma : list int, p: val
  PRE  [ _p OF (tptr t_struct_list) ]
     PROP ()
     LOCAL (temp _p p)
     SEP (listrep sigma p)
  POST [ (tptr t_struct_list) ]
    EX q:val,
     PROP () LOCAL (temp ret_temp q)
     SEP (listrep (rev sigma) q).

Definition last_foo_spec :=
 DECLARE _last_foo
  WITH sigma : list int, p: val, sigma': list int, x: int
  PRE  [ _p OF (tptr t_struct_list) ]
     PROP (sigma = sigma' ++ x :: nil)
     LOCAL (temp _p p)
     SEP (listrep sigma p)
  POST [ tuint ]
     PROP () LOCAL (temp ret_temp (Vint x))
     SEP (TT).

Definition Gprog : funspecs :=
         ltac:(with_library prog [ reverse_spec; last_foo_spec ]).

Lemma body_last_foo: semax_body Vprog Gprog
                                    f_last_foo last_foo_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_last_foo last_foo_spec *)
  start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@nil localdef)) (SEPx (@cons mpred (listrep sigma p) (@nil mpred))))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _reverse (Tfunction (Tcons (tptr (Tstruct _list noattr)) Tnil) (tptr (Tstruct _list noattr)) cc_default)) (@cons expr (Etempvar _p (tptr (Tstruct _list noattr))) (@nil expr))) (Sset _p (Etempvar _t'1 (tptr (Tstruct _list noattr))))) MORE_COMMANDS) POSTCONDITION *)
  subst sigma.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p) (@nil localdef)) (SEPx (@cons mpred (listrep (@app Int.int sigma' (@cons Int.int x (@nil Int.int))) p) (@nil mpred))))) (Ssequence (Ssequence (Scall (@Some ident _t'1) (Evar _reverse (Tfunction (Tcons (tptr (Tstruct _list noattr)) Tnil) (tptr (Tstruct _list noattr)) cc_default)) (@cons expr (Etempvar _p (tptr (Tstruct _list noattr))) (@nil expr))) (Sset _p (Etempvar _t'1 (tptr (Tstruct _list noattr))))) MORE_COMMANDS) POSTCONDITION *)
  forward_call (sigma' ++ [x], p). (* p = reverse (p); *)
(* Goal: semax CompSpecs Espec Delta (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun vret : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p vret) (@nil localdef)) (SEPx (@cons mpred (listrep (@rev Int.int (@app Int.int sigma' (@cons Int.int x (@nil Int.int)))) vret) (@nil mpred)))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _head tuint)) MORE_COMMANDS) POSTCONDITION *)
  Intros p'.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p') (@nil localdef)) (SEPx (@cons mpred (listrep (@rev Int.int (@app Int.int sigma' (@cons Int.int x (@nil Int.int)))) p') (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _head tuint)) MORE_COMMANDS) POSTCONDITION *)
  rewrite rev_app_distr; simpl.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p') (@nil localdef)) (SEPx (@cons mpred (listrep (@cons Int.int x (@rev Int.int sigma')) p') (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _head tuint)) MORE_COMMANDS) POSTCONDITION *)
  unfold listrep; fold listrep.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _p p') (@nil localdef)) (SEPx (@cons mpred (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs Tsh t_struct_list (@pair val val (Vint x) y) p') (listrep (@rev Int.int sigma') y))) (@nil mpred))))) (Ssequence (Sset _res (Efield (Ederef (Etempvar _p (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _head tuint)) MORE_COMMANDS) POSTCONDITION *)
  Intros q.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x)) (@cons localdef (temp _p p') (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Tsh t_struct_list (@pair val val (Vint x) q) p') (@cons mpred (listrep (@rev Int.int sigma') q) (@nil mpred)))))) (Sreturn (@Some expr (Etempvar _res tuint))) POSTCONDITION *)
  forward. (* res = p -> head; *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _res (Vint x)) (@cons localdef (temp _p p') (@nil localdef))) (SEPx (@cons mpred (@data_at CompSpecs Tsh t_struct_list (@pair val val (Vint x) q) p') (@cons mpred (listrep (@rev Int.int sigma') q) (@nil mpred)))))) (Sreturn (@Some expr (Etempvar _res tuint))) POSTCONDITION *)
  forward. (* return res; *)
Qed.
