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


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

Arguments listrep sh contents x : simpl never.

Lemma listrep_local_facts:
  forall sh contents p,
     listrep sh contents p |--
     !! (is_pointer_or_null p /\ (p=nullval <-> contents=nil)).
Proof.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
intros.
(* Goal: @derives mpred Nveric (listrep sh contents p) (@prop mpred Nveric (and (is_pointer_or_null p) (iff (@eq val p nullval) (@eq (list val) contents (@nil val))))) *)
revert p; induction contents; 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 val) (@nil val) (@nil val))))) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a y) p) (listrep sh contents y)) (@prop mpred Nveric (and (is_pointer_or_null p) (iff (@eq val p nullval) (@eq (list val) (@cons val a contents) (@nil val))))) *)
apply prop_right; split; simpl; auto. intuition.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
entailer!.
(* Goal: iff (@eq val p nullval) (@eq (list val) (@cons val a contents) (@nil val)) *)
split; intro. subst p. destruct H; contradiction. inv H2.
Qed.

Hint Resolve listrep_local_facts : saturate_local.

Lemma listrep_valid_pointer:
  forall sh contents p,
   sepalg.nonidentity sh ->
   listrep sh contents p |-- valid_pointer p.
Proof.
(* Goal: forall (sh : share) (contents : list val) (p : val) (_ : @sepalg.nonidentity share Share.Join_ba pa_share sh), @derives mpred Nveric (listrep sh contents p) (valid_pointer p) *)
 destruct contents; 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 sh t_struct_list (@pair val val v y) p) (listrep sh contents y)) (valid_pointer p) *)
 auto with valid_pointer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) p) (listrep sh contents y)) (valid_pointer p) *)
 apply sepcon_valid_pointer1.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) p) (valid_pointer p) *)
 apply data_at_valid_ptr; auto. simpl;  computable.
Qed.

Hint Resolve listrep_valid_pointer : valid_pointer.

Lemma listrep_null: forall sh contents,
    listrep sh contents nullval = !! (contents=nil) && emp.
Proof.
(* Goal: forall (sh : share) (contents : list val), @eq mpred (listrep sh contents nullval) (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@nil val))) (@emp mpred Nveric Sveric)) *)
destruct contents; unfold listrep; fold listrep.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (lseg sh contents y x)))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) *)
normalize.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) contents (@nil val)) (is_pointer_or_null nullval))) (@emp mpred Nveric Sveric)) (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@nil val))) (@emp mpred Nveric Sveric)) *)
apply pred_ext.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) nullval) (listrep sh contents y)) (@emp mpred Nveric Sveric) *)
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) (@cons val v contents) (@nil val))) (@emp mpred Nveric Sveric)) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) nullval) (listrep sh contents y))) *)
Intros y. entailer. destruct H; contradiction.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) *)
Intros.
Qed.

Lemma is_pointer_or_null_not_null:
 forall x, is_pointer_or_null x -> x <> nullval -> isptr x.
Proof.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
intros.
(* Goal: isptr x *)
 destruct x; try contradiction. hnf in H; subst i. contradiction H0; reflexivity.
(* Goal: isptr (Vptr b i) *)
 apply I.
Qed.

Definition append_spec :=
 DECLARE _append
  WITH sh : share, x: val, y: val, s1: list val, s2: list val
  PRE [ _x OF (tptr t_struct_list) , _y OF (tptr t_struct_list)]
     PROP(writable_share sh)
     LOCAL (temp _x x; temp _y y)
     SEP (listrep sh s1 x; listrep sh s2 y)
  POST [ tptr t_struct_list ]
    EX r: val,
     PROP()
     LOCAL(temp ret_temp r)
     SEP (listrep sh (s1++s2) r).

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

Module Proof1.

Definition lseg (sh: share) (contents: list val) (x z: val) : mpred :=
  ALL cts2:list val, listrep sh cts2 z -* listrep sh (contents++cts2) x.

Lemma body_append: semax_body Vprog Gprog f_append append_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_append append_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef))) (SEPx (@cons mpred (listrep sh s1 x) (@cons mpred (listrep sh s2 y) (@nil mpred)))))) (Sifthenelse (Ebinop Oeq (Etempvar _x (tptr (Tstruct _list noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid)) tint) (Sreturn (@Some expr (Etempvar _y (tptr (Tstruct _list noattr))))) (Ssequence (Sset _t (Etempvar _x (tptr (Tstruct _list noattr)))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) (Ssequence (Swhile (Ebinop One (Etempvar _u (tptr (Tstruct _list noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid)) tint) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr))) (Etempvar _y (tptr (Tstruct _list noattr)))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr)))))))))) POSTCONDITION *)
forward_if.
*
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (lseg sh contents y x)))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) *)
 subst x. rewrite listrep_null. normalize.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
(* Goal: @derives mpred Nveric (listrep sh s2 y) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val y a)) (listrep sh (@app val (@nil val) s2) a))) *)
 Exists y.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
 entailer!.
(* Goal: @derives mpred Nveric (listrep sh s2 y) (listrep sh (@app val (@nil val) s2) y) *)
 simpl; auto.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef)))) (SEPx (@cons mpred (listrep sh s1 x) (@cons mpred (listrep sh s2 y) (@nil mpred)))))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
 destruct s1 as [ | v s1']; unfold listrep at 1; fold listrep.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (lseg sh contents y x)))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) *)
 normalize.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef)))) (SEPx (@cons mpred (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (listrep sh s1' y))) (@cons mpred (listrep sh s2 y) (@nil mpred)))))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
 Intros u.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@cons mpred (listrep sh s1' u) (@cons mpred (listrep sh s2 y) (@nil mpred))))))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
 remember (v::s1') as s1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
 forward_while
      ( EX a: val, EX s1b: list val, EX t: val, EX u: val,
            PROP ()
            LOCAL (temp _x x; temp _t t; temp _u u; temp _y y)
            SEP (listrep sh (a::s1b++s2) t -* listrep sh (s1++s2) x;
                   data_at sh t_struct_list (a,u) t;
                   listrep sh s1b u;
                   listrep sh s2 y))%assert.
+ (* current assertion implies 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 _u u) (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@cons mpred (listrep sh s1' u) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun a : val => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (list val) (fun s1b : list val => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun t : val => @exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) val (fun u : val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u) t) (@cons mpred (listrep sh s1b u) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))))))) *)
   Exists v s1' x u.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
   subst s1. entailer!. simpl. cancel_wand.
+ (* loop test is safe to execute *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
   entailer!.
+ (* loop body preserves invariant *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   clear v Heqs1.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) *)
   destruct s1b; unfold listrep at 3; fold listrep. Intros. contradiction.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@cons val v s1b) s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) u0) (listrep sh s1b y))) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   Intros z.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward.
(* 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 _u z) (@cons localdef (temp _t u0) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@cons val v s1b) s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val v z) u0) (@cons mpred (listrep sh s1b z) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))))) (@exp (forall _ : environ, mpred) (@LiftNatDed' mpred Nveric) (prod (prod (prod val (list val)) val) val) (fun a : prod (prod (prod val (list val)) val) val => PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t (@snd (prod val (list val)) val (@fst (prod (prod val (list val)) val) val a))) (@cons localdef (temp _u (@snd (prod (prod val (list val)) val) val a)) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val (@fst val (list val) (@fst (prod val (list val)) val (@fst (prod (prod val (list val)) val) val a))) (@app val (@snd val (list val) (@fst (prod val (list val)) val (@fst (prod (prod val (list val)) val) val a))) s2)) (@snd (prod val (list val)) val (@fst (prod (prod val (list val)) val) val a))) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val (@fst val (list val) (@fst (prod val (list val)) val (@fst (prod (prod val (list val)) val) val a))) (@snd (prod (prod val (list val)) val) val a)) (@snd (prod val (list val)) val (@fst (prod (prod val (list val)) val) val a))) (@cons mpred (listrep sh (@snd val (list val) (@fst (prod val (list val)) val (@fst (prod (prod val (list val)) val) val a))) (@snd (prod (prod val (list val)) val) val a)) (@cons mpred (listrep sh s2 y) (@nil mpred))))))))) *)
   Exists (v,s1b,u0,z). unfold fst, snd.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@nil val) s2)) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a y) t)) (listrep sh (@nil val) nullval)) (listrep sh s2 y)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (listrep sh (@app val s1 s2) x)) *)
   simpl app.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
   entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a (@cons val v (@app val s1b s2))) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t)) (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1b s2)) u0) (listrep sh (@app val s1 s2) x)) *)
   rewrite sepcon_comm.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@wand mpred Nveric Sveric (listrep sh (@cons val a (@cons val v (@app val s1b s2))) t) (listrep sh (@app val s1 s2) x))) (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1b s2)) u0) (listrep sh (@app val s1 s2) x)) *)
   apply RAMIF_PLAIN.trans''.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1b s2)) u0) (listrep sh (@cons val a (@cons val v (@app val s1b s2))) t)) *)
   apply wand_sepcon_adjoint.
   forget (v::s1b++s2) as s3.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (listrep sh s3 u0)) (listrep sh (@cons val a s3) t) *)
   unfold listrep; fold listrep; Exists u0; auto.
+ (* after the loop *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr))) (Etempvar _y (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   clear v s1' Heqs1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a y) t)) (listrep sh s1b nullval)) (listrep sh s2 y)) (@exp mpred Nveric val (fun a0 : val => @andp mpred Nveric (@prop mpred Nveric (@eq val x a0)) (listrep sh (@app val s1 s2) a0))) *)
   rewrite (proj1 H2 (eq_refl _)).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@nil val) s2)) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a y) t)) (listrep sh (@nil val) nullval)) (listrep sh s2 y)) (@exp mpred Nveric val (fun a0 : val => @andp mpred Nveric (@prop mpred Nveric (@eq val x a0)) (listrep sh (@app val s1 s2) a0))) *)
   Exists x.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@nil val) s2)) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a y) t)) (listrep sh (@nil val) nullval)) (listrep sh s2 y)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (listrep sh (@app val s1 s2) x)) *)
   simpl app.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a s2) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a y) t)) (listrep sh (@nil val) nullval)) (listrep sh s2 y)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (listrep sh (@app val s1 s2) x)) *)
   clear.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
   entailer!.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (lseg sh contents y x)))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) *)
   unfold listrep at 3; fold listrep. normalize.
   pull_right (listrep sh (a :: s2) t -* listrep sh (s1 ++ s2) x).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (listrep sh s2 y)) (@wand mpred Nveric Sveric (listrep sh (@cons val a s2) t) (listrep sh (@app val s1 s2) x))) (listrep sh (@app val s1 s2) x) *)
   apply modus_ponens_wand'.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (listrep sh s2 y)) (listrep sh (@cons val a s2) t) *)
   unfold listrep at 2; fold listrep. Exists y; auto.
Qed.

End Proof1.

Module Proof2.

Definition lseg (sh: share) (contents: list val) (x z: val) : mpred :=
  ALL cts2:list val, listrep sh cts2 z -* listrep sh (contents++cts2) x.

Lemma body_append: semax_body Vprog Gprog f_append append_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_append append_spec *)
start_function.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef))) (SEPx (@cons mpred (listrep sh s1 x) (@cons mpred (listrep sh s2 y) (@nil mpred)))))) (Sifthenelse (Ebinop Oeq (Etempvar _x (tptr (Tstruct _list noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid)) tint) (Sreturn (@Some expr (Etempvar _y (tptr (Tstruct _list noattr))))) (Ssequence (Sset _t (Etempvar _x (tptr (Tstruct _list noattr)))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) (Ssequence (Swhile (Ebinop One (Etempvar _u (tptr (Tstruct _list noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid)) tint) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr))) (Etempvar _y (tptr (Tstruct _list noattr)))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr)))))))))) POSTCONDITION *)
forward_if.
*
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (lseg sh contents y x)))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) *)
 subst x. rewrite listrep_null. normalize.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
(* Goal: @derives mpred Nveric (listrep sh s2 y) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val y a)) (listrep sh (@app val (@nil val) s2) a))) *)
 Exists y.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
 entailer!.
(* Goal: @derives mpred Nveric (listrep sh s2 y) (listrep sh (@app val (@nil val) s2) y) *)
 simpl; auto.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@nil val) s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@cons val v s1b) s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) u0) (listrep sh s1b y))) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
 destruct s1 as [ | v s1']; unfold listrep; fold listrep. Intros; contradiction.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef)))) (SEPx (@cons mpred (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (listrep sh s1' y))) (@cons mpred (listrep sh s2 y) (@nil mpred)))))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
 Intros u.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@cons mpred (listrep sh s1' u) (@cons mpred (listrep sh s2 y) (@nil mpred))))))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
 remember (v::s1') as s1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
 forward_while
      (EX s1a: list val,  EX a: val, EX s1b: list val, EX t: val, EX u: val,
            PROP (s1 = s1a ++ a :: s1b)
            LOCAL (temp _x x; temp _t t; temp _u u; temp _y y)
            SEP (lseg sh s1a x t;
                   data_at sh t_struct_list (a,u) t;
                   listrep sh s1b u;
                   listrep sh s2 y))%assert.
+ (* current assertion implies loop invariant *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
   Exists (@nil val) v s1' x u.  entailer!.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1' s2)) x) (listrep sh (@app val (@cons val v s1') s2) x)) *)
   unfold lseg. apply allp_right; intro. simpl. cancel_wand.
+ (* loop test is safe to execute *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
   entailer!.
+ (* loop body preserves 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 _u u) (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@cons mpred (listrep sh s1' u) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t x) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1' s2)) x) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@cons mpred (listrep sh s1' u) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) *)
   clear v Heqs1. subst s1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@nil val) s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (@emp mpred Nveric Sveric) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@cons val v s1b) s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) u0) (listrep sh s1b y))) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   destruct s1b; unfold listrep; fold listrep. Intros; contradiction.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@cons val v s1b) s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) u0) (listrep sh s1b y))) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
   Intros z.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward.
   Exists (s1a++[a],v,s1b,u0,z). unfold fst, snd.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@nil val) s2)) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a y) t)) (listrep sh (@nil val) nullval)) (listrep sh s2 y)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (listrep sh (@app val s1 s2) x)) *)
   rewrite !app_ass. simpl app.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
   entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@data_at CompSpecs sh t_struct_list (@pair val val a b) u)) (@sepcon mpred Nveric Sveric (lseg sh (@cons val v (@nil val)) x u) (@data_at CompSpecs sh t_struct_list (@pair val val a b) u)) *)
   unfold lseg.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a (@cons val v (@app val s1b s2))) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t)) (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1b s2)) u0) (listrep sh (@app val s1 s2) x)) *)
   rewrite sepcon_comm.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a s2) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a y) t)) (listrep sh (@nil val) nullval)) (listrep sh s2 y)) (@andp mpred Nveric (@prop mpred Nveric (@eq val x x)) (listrep sh (@app val s1 s2) x)) *)
   clear.
   apply RAMIF_Q.trans'' with (cons a).
   extensionality cts; simpl; rewrite app_ass; reflexivity.
(* Goal: @derives mpred Nveric (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1b s2)) u0) (listrep sh (@cons val a (@cons val v (@app val s1b s2))) t)) *)
   apply allp_right; intro. apply wand_sepcon_adjoint.
   unfold listrep at 2; fold listrep; Exists u0.  apply derives_refl.
 + (* after the loop *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
   forward. forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
   Exists x. entailer!.
   destruct H3 as [? _]. specialize (H3 (eq_refl _)). subst s1b.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (lseg sh contents y x)))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) *)
   unfold listrep at 1. normalize. rewrite H0. rewrite app_ass. simpl app.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@data_at CompSpecs sh t_struct_list (@pair val val a b) u)) (@sepcon mpred Nveric Sveric (lseg sh (@cons val v (@nil val)) x u) (@data_at CompSpecs sh t_struct_list (@pair val val a b) u)) *)
   unfold lseg.
   rewrite sepcon_assoc.
   eapply derives_trans; [apply allp_sepcon1 | ]. apply allp_left with (a::s2).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a (@cons val v (@app val s1b s2))) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t)) (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1b s2)) u0) (listrep sh (@app val s1 s2) x)) *)
   rewrite sepcon_comm.
   eapply derives_trans; [ | apply modus_ponens_wand].
   apply sepcon_derives; [ | apply derives_refl].
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (listrep sh s2 y)) (listrep sh (@cons val a s2) t) *)
   unfold listrep at 2; fold listrep. Exists y; auto.
Qed.

End Proof2.

Module Proof3.  (*************** inductive lseg *******************)

Fixpoint lseg (sh: share)
            (contents: list val) (x z: val) : mpred :=
 match contents with
 | h::hs => !! (x<>z) && 
              EX y:val,
                data_at sh t_struct_list (h,y) x * lseg sh hs y z
 | nil => !! (x = z /\ is_pointer_or_null x) && emp
 end.

Arguments lseg sh contents x z : simpl never.

Lemma lseg_local_facts:
  forall sh contents p q,
     lseg sh contents p q |--
     !! (is_pointer_or_null p /\ is_pointer_or_null q /\ (p=q <-> contents=nil)).
Proof.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
intros.
apply derives_trans with (lseg sh contents p q && !! (is_pointer_or_null p /\
        is_pointer_or_null q /\ (p = q <-> contents = []))).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
2: entailer!.
revert p; induction contents; intros; simpl; unfold lseg; fold lseg.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
entailer!.
(* Goal: iff (@eq val nullval nullval) (@eq (list val) (@nil val) (@nil val)) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a y) p) (listrep sh contents y)) (@prop mpred Nveric (and (is_pointer_or_null p) (iff (@eq val p nullval) (@eq (list val) (@cons val a contents) (@nil val))))) *)
intuition.
(* Goal: @derives mpred Nveric (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) *)
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) *)
Intros y. Exists y.
eapply derives_trans.
apply sepcon_derives.
apply derives_refl.
apply IHcontents.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
entailer!.
intuition congruence.
Qed.

Hint Resolve lseg_local_facts : saturate_local.

Lemma lseg_valid_pointer:
  forall sh contents p ,
   sepalg.nonidentity sh ->
   lseg sh contents p nullval |-- valid_pointer p.
Proof.
 destruct contents; unfold lseg; fold lseg; intros; normalize;
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (valid_pointer nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) p) (listrep sh contents y)) (valid_pointer p) *)
 auto with valid_pointer.
Qed.

Hint Resolve lseg_valid_pointer : valid_pointer.

Lemma lseg_eq: forall sh contents x,
    lseg sh contents x x = !! (contents=nil /\ is_pointer_or_null x) && emp.
Proof.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
intros.
(* Goal: @eq mpred (lseg sh contents x x) (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) contents (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) *)
destruct contents; unfold lseg; fold lseg.
(* Goal: iff (@eq val nullval nullval) (@eq (list val) (@nil val) (@nil val)) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a y) p) (listrep sh contents y)) (@prop mpred Nveric (and (is_pointer_or_null p) (iff (@eq val p nullval) (@eq (list val) (@cons val a contents) (@nil val))))) *)
f_equal. f_equal. f_equal. apply prop_ext; intuition.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (lseg sh contents y x)))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) *)
normalize.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) contents (@nil val)) (is_pointer_or_null nullval))) (@emp mpred Nveric Sveric)) (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@nil val))) (@emp mpred Nveric Sveric)) *)
apply pred_ext.
(* Goal: @derives mpred Nveric (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) *)
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) *)
Intros y. entailer.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) *)
Intros.
Qed.

Lemma lseg_null: forall sh contents,
    lseg sh contents nullval nullval = !! (contents=nil) && emp.
Proof.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
intros.
(* Goal: @eq mpred (lseg sh contents nullval nullval) (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@nil val))) (@emp mpred Nveric Sveric)) *)
 rewrite lseg_eq.
(* Goal: @eq mpred (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) contents (@nil val)) (is_pointer_or_null nullval))) (@emp mpred Nveric Sveric)) (@andp mpred Nveric (@prop mpred Nveric (@eq (list val) contents (@nil val))) (@emp mpred Nveric Sveric)) *)
 apply pred_ext.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
 entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
 entailer!.
Qed.

Lemma lseg_cons: forall sh (v u x: val) s,
   readable_share sh ->
 data_at sh t_struct_list (v, u) x * lseg sh s u nullval
 |-- lseg sh [v] x u * lseg sh s u nullval.
Proof.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (lseg sh s u nullval)) (@sepcon mpred Nveric Sveric (lseg sh (@cons val v (@nil val)) x u) (lseg sh s u nullval)) *)
     unfold lseg at 2. Exists u. 
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh s1 j x)) (lseg sh s2 x nullval)) (@andp mpred Nveric (@prop mpred Nveric (not (@eq val w nullval))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh (@app val s1 s2) j nullval))) *)
     entailer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh s1 j x)) (lseg sh s2 x nullval)) (@andp mpred Nveric (@prop mpred Nveric (not (@eq val w nullval))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh (@app val s1 s2) j nullval))) *)
     destruct s; unfold lseg at 1; fold lseg; entailer.
Qed.

Lemma lseg_cons': forall sh (v u x a b: val) ,
   readable_share sh ->
 data_at sh t_struct_list (v, u) x * data_at sh t_struct_list (a,b) u
 |-- lseg sh [v] x u * data_at sh t_struct_list (a,b) u.
Proof.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@data_at CompSpecs sh t_struct_list (@pair val val a b) u)) (@sepcon mpred Nveric Sveric (lseg sh (@cons val v (@nil val)) x u) (@data_at CompSpecs sh t_struct_list (@pair val val a b) u)) *)
     unfold lseg. Exists u. 
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh s1 j x)) (lseg sh s2 x nullval)) (@andp mpred Nveric (@prop mpred Nveric (not (@eq val w nullval))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh (@app val s1 s2) j nullval))) *)
     entailer.
Qed.

Lemma lseg_app': forall sh s1 s2 (a w x y z: val),
   readable_share sh ->
   lseg sh s1 w x * lseg sh s2 x y * data_at sh t_struct_list (a,z) y |--
   lseg sh (s1++s2) w y * data_at sh t_struct_list (a,z) y.
Proof.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
 intros.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1' s2)) x) (listrep sh (@app val (@cons val v s1') s2) x)) *)
 revert w; induction s1; intro; simpl.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
 unfold lseg at 1. entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
 unfold lseg at 1 3; fold lseg. Intros j; Exists j.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh s1 j x)) (lseg sh s2 x nullval)) (@andp mpred Nveric (@prop mpred Nveric (not (@eq val w nullval))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh (@app val s1 s2) j nullval))) *)
 entailer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh s1 j x)) (lseg sh s2 x nullval)) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh (@app val s1 s2) j nullval)) *)
 sep_apply (IHs1 j).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (@data_at CompSpecs sh t_struct_list (@pair val val a u) y)) (lseg sh s3 u z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a u) y) (lseg sh s3 u z))) *)
 cancel. 
Qed.

Lemma lseg_app_null: forall sh s1 s2 (w x: val),
   readable_share sh ->
   lseg sh s1 w x * lseg sh s2 x nullval |--
   lseg sh (s1++s2) w nullval.
Proof.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
 intros.
(* Goal: @derives mpred Nveric (@emp mpred Nveric Sveric) (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1' s2)) x) (listrep sh (@app val (@cons val v s1') s2) x)) *)
 revert w; induction s1; intro; simpl.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
 unfold lseg at 1. entailer!.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
 unfold lseg at 1 3; fold lseg. Intros j; Exists j.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh s1 j x)) (lseg sh s2 x nullval)) (@andp mpred Nveric (@prop mpred Nveric (not (@eq val w nullval))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh (@app val s1 s2) j nullval))) *)
 entailer.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh s1 j x)) (lseg sh s2 x nullval)) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh (@app val s1 s2) j nullval)) *)
 sep_apply (IHs1 j).
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (@data_at CompSpecs sh t_struct_list (@pair val val a u) y)) (lseg sh s3 u z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a u) y) (lseg sh s3 u z))) *)
 cancel.
Qed.

Lemma lseg_app: forall sh s1 s2 a s3 (w x y z: val),
   readable_share sh ->
   lseg sh s1 w x * lseg sh s2 x y * lseg sh (a::s3) y z |--
   lseg sh (s1++s2) w y * lseg sh (a::s3) y z.
Proof.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
 intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
 unfold lseg at 3 5; fold lseg.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@data_at CompSpecs sh t_struct_list (@pair val val a b) u)) (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (not (@eq val x u))) (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (@andp mpred Nveric (@prop mpred Nveric (and (@eq val y u) (is_pointer_or_null y))) (@emp mpred Nveric Sveric))))) (@data_at CompSpecs sh t_struct_list (@pair val val a b) u)) *)
 Intros u; Exists u. rewrite prop_true_andp by auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a u) y) (lseg sh s3 u z))) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a u) y) (lseg sh s3 u z))) *)
 sep_apply (lseg_app' sh s1 s2 a w x y u); auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (@data_at CompSpecs sh t_struct_list (@pair val val a u) y)) (lseg sh s3 u z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a u) y) (lseg sh s3 u z))) *)
 cancel.
Qed.

Lemma listrep_lseg_null :
 listrep = fun sh s p => lseg sh s p nullval.
Proof.
(* Goal: @eq (forall (_ : share) (_ : list val) (_ : val), mpred) listrep (fun (sh : share) (s : list val) (p : val) => lseg sh s p nullval) *)
extensionality sh s p.
(* Goal: @eq mpred (listrep sh s p) (lseg sh s p nullval) *)
revert p.
(* Goal: forall (sh : share) (s1 s2 : list val) (a : val) (s3 : list val) (w x y z : val) (_ : readable_share sh), @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh s1 w x) (lseg sh s2 x y)) (lseg sh (@cons val a s3) y z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (lseg sh (@cons val a s3) y z)) *)
induction s; intros.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
unfold lseg, listrep; apply pred_ext; entailer!.
(* Goal: @eq mpred (listrep sh (@cons val a s) p) (lseg sh (@cons val a s) p nullval) *)
unfold lseg, listrep; fold lseg; fold listrep.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
apply pred_ext; Intros y; Exists y; rewrite IHs; entailer!.
Qed.

Lemma body_append: semax_body Vprog Gprog f_append append_spec.
Proof.
(* Goal: semax_body Vprog Gprog CompSpecs f_append append_spec *)
start_function.
revert POSTCONDITION; rewrite listrep_lseg_null; intro.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef))) (SEPx (@cons mpred (listrep sh s1 x) (@cons mpred (listrep sh s2 y) (@nil mpred)))))) (Sifthenelse (Ebinop Oeq (Etempvar _x (tptr (Tstruct _list noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid)) tint) (Sreturn (@Some expr (Etempvar _y (tptr (Tstruct _list noattr))))) (Ssequence (Sset _t (Etempvar _x (tptr (Tstruct _list noattr)))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) (Ssequence (Swhile (Ebinop One (Etempvar _u (tptr (Tstruct _list noattr))) (Ecast (Econst_int (Int.repr Z0) tint) (tptr tvoid)) tint) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr))) (Etempvar _y (tptr (Tstruct _list noattr)))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr)))))))))) POSTCONDITION *)
forward_if.
*
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) *)
 subst x. rewrite lseg_null. Intros. subst.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
(* Goal: @derives mpred Nveric (listrep sh s2 y) (@exp mpred Nveric val (fun a : val => @andp mpred Nveric (@prop mpred Nveric (@eq val y a)) (listrep sh (@app val (@nil val) s2) a))) *)
 Exists y.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
 entailer!.
(* Goal: @derives mpred Nveric (listrep sh s2 y) (listrep sh (@app val (@nil val) s2) y) *)
 simpl; auto.
*
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
 destruct s1 as [ | v s1']; unfold lseg at 1; fold lseg.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) *)
 Intros. contradiction H.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef)))) (SEPx (@cons mpred (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) x) (listrep sh s1' y))) (@cons mpred (listrep sh s2 y) (@nil mpred)))))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
 Intros u.
 clear - SH.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef)))) (SEPx (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@cons mpred (listrep sh s1' u) (@cons mpred (listrep sh s2 y) (@nil mpred))))))) (Ssequence (Sset _u (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
 remember (v::s1') as s1.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
 forward.
 forward_while
      (EX s1a: list val, EX a: val, EX s1b: list val, EX t: val, EX u: val,
            PROP (s1 = s1a ++ a :: s1b)
            LOCAL (temp _x x; temp _t t; temp _u u; temp _y y)
            SEP (lseg sh s1a x t; 
                   data_at sh t_struct_list (a,u) t;
                   lseg sh s1b u nullval; 
                   lseg sh s2 y nullval))%assert.
 + (* current assertion implies loop invariant *)
     Exists (@nil val) v s1' x u.
(* 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 _u u) (@cons localdef (temp _t x) (@cons localdef (temp _x x) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@cons mpred (listrep sh s1' u) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t x) (@cons localdef (temp _u u) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val v (@app val s1' s2)) x) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val v u) x) (@cons mpred (listrep sh s1' u) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) *)
     subst s1. rewrite lseg_eq.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh s1 j x)) (lseg sh s2 x nullval)) (@andp mpred Nveric (@prop mpred Nveric (not (@eq val w nullval))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh (@app val s1 s2) j nullval))) *)
     entailer.
(*     sep_apply (lseg_cons sh v u x s1'); auto. *)
 + (* loop test is safe to execute *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
     entailer!.
 + (* loop body preserves invariant *)
    destruct s1b; unfold lseg at 2; fold lseg.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) *)
    Intros. contradiction.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@cons val v s1b) s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (@exp mpred Nveric val (fun y : val => @sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v y) u0) (listrep sh s1b y))) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Ssequence (Sset _t (Etempvar _u (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
    Intros z.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
    forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
    forward.
    Exists (s1a++a::nil, v0, s1b,u0,z). unfold fst, snd.
    simpl app; rewrite app_ass.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh s1 j x)) (lseg sh s2 x nullval)) (@andp mpred Nveric (@prop mpred Nveric (not (@eq val w nullval))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a j) w) (lseg sh (@app val s1 s2) j nullval))) *)
    entailer.
    sep_apply (lseg_cons' sh a u0 t v0 z); auto.
    sep_apply (lseg_app' sh s1a [a] v0 x t u0 z); auto.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (@data_at CompSpecs sh t_struct_list (@pair val val a u) y)) (lseg sh s3 u z)) (@sepcon mpred Nveric Sveric (lseg sh (@app val s1 s2) w y) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val a u) y) (lseg sh s3 u z))) *)
    cancel.
 + (* after the loop *)
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a u0) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Ssequence (Sassign (Efield (Ederef (Etempvar _t (tptr (Tstruct _list noattr))) (Tstruct _list noattr)) _tail (tptr (Tstruct _list noattr))) (Etempvar _y (tptr (Tstruct _list noattr)))) MORE_COMMANDS) POSTCONDITION *)
    clear v s1' Heqs1.
(* Goal: @derives mpred Nveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq (list val) (@cons val v contents) (@nil val)) (is_pointer_or_null x))) (@emp mpred Nveric Sveric)) (@exp mpred Nveric val (fun x0 : val => @andp mpred Nveric (@prop mpred Nveric (not (@eq val x x))) (@sepcon mpred Nveric Sveric (@data_at CompSpecs sh t_struct_list (@pair val val v x0) x) (lseg sh contents x0 x)))) *)
    subst. rewrite lseg_eq. Intros. subst. 
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
    forward.
(* Goal: semax CompSpecs Espec Delta (PROPx (@nil Prop) (LOCALx (@cons localdef (temp _x x) (@cons localdef (temp _t t) (@cons localdef (temp _u u0) (@cons localdef (temp _y y) (@nil localdef))))) (SEPx (@cons mpred (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val s1b s2)) t) (listrep sh (@app val s1 s2) x)) (@cons mpred (@data_at CompSpecs sh t_struct_list (@pair val val a y) t) (@cons mpred (listrep sh s1b u0) (@cons mpred (listrep sh s2 y) (@nil mpred)))))))) (Sreturn (@Some expr (Etempvar _x (tptr (Tstruct _list noattr))))) POSTCONDITION *)
    forward.
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@sepcon mpred Nveric Sveric (@wand mpred Nveric Sveric (listrep sh (@cons val a (@app val (@nil val) s2)) t) (listrep sh (@app val s1 s2) x)) (@data_at CompSpecs sh t_struct_list (@pair val val a y) t)) (listrep sh (@nil val) nullval)) (listrep sh s2 y)) (@exp mpred Nveric val (fun a0 : val => @andp mpred Nveric (@prop mpred Nveric (@eq val x a0)) (listrep sh (@app val s1 s2) a0))) *)
    Exists x. 
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (@andp mpred Nveric (@prop mpred Nveric (and (@eq val w x) (is_pointer_or_null w))) (@emp mpred Nveric Sveric)) (lseg sh s2 x nullval)) (lseg sh s2 w nullval) *)
(* Goal: @derives mpred Nveric (@sepcon mpred Nveric Sveric (lseg sh (@cons val a s1) w x) (lseg sh s2 x nullval)) (lseg sh (@cons val a (@app val s1 s2)) w nullval) *)
    entailer!.
    sep_apply (lseg_cons sh a y t s2); auto.
    sep_apply (lseg_app_null sh [a] s2 t y); auto.
    rewrite app_ass.
    sep_apply (lseg_app_null sh s1a ([a]++s2) x t); auto.
Qed.

End Proof3.

