(*
 *  Seplog is an implementation of separation logic (an extension of Hoare
 *  logic by John C. Reynolds, Peter W. O'Hearn, and colleagues) in the
 *  Coq proof assistant (version 8, http://coq.inria.fr) together with a
 *  sample verification of the heap manager of the Topsy operating system
 *  (version 2, http://www.topsy.net). More information is available at
 *  http://web.yl.is.s.u-tokyo.ac.jp/~affeldt/seplog.
 *
 *  Copyright (c) 2005 Reynald Affeldt and Nicolas Marti
 *
 *  This program is free software; you can redistribute it and/or modify
 *  it under the terms of the GNU General Public License as published by
 *  the Free Software Foundation; either version 2 of the License, or
 *  (at your option) any later version.
 *
 *  This program is distributed in the hope that it will be useful,
 *  but WITHOUT ANY WARRANTY; without even the implied warranty of
 *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 *  GNU General Public License for more details.
 *
 *  You should have received a copy of the GNU General Public License
 *  along with this program; if not, write to the Free Software
 *  Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301  USA
 *)

Require Import List.
Require Import ZArith.
Require Import List.
Require Import EqNat.
Require Import Classical.

Require Import util.
Require Import heap.
Require Import bipl.

Import valandloc.

(* commands of the langage *)

Inductive cmd : Set :=
 skip : cmd
| assign_var_e : var.v -> expr -> cmd
| assign_var_lookup : var.v -> expr -> cmd
| assign_lookup_expr : expr -> expr -> cmd
| malloc : var.v -> expr -> cmd
| free : expr -> cmd
| while : expr_b -> cmd -> cmd
| seq : cmd -> cmd -> cmd
| ifte : expr_b -> cmd -> cmd -> cmd.

Notation "x <- e" := (assign_var_e x e) (at level 80) : sep_scope.
Notation "x '<-*' e" := (assign_var_lookup x e) (at level 80) : sep_scope.
Notation "e '*<-' f" := (assign_lookup_expr e f) (at level 80) : sep_scope.
Notation "x '<-malloc' e" := (malloc x e) (at level 80) : sep_scope.
Notation "c ; d" := (seq c d) (at level 81, right associativity) : sep_scope.
Notation "'ifte' a 'thendo' x 'elsedo' y" := (ifte a x y)(at level 80) : sep_scope.

Open Local Scope sep_scope.
Open Local Scope heap_scope.

(* states *)

Definition state := prod store.s heap.h.

(******************************************************************************)

(** operational semantics *)

Inductive exec : (option state) -> cmd -> (option state) -> Prop :=
  exec_none : forall c, exec None c None

  | exec_skip:  forall s h,  exec (Some (s, h)) skip (Some (s, h))
    
  | exec_assign_var_e : forall s h x e,
    exec (Some (s, h)) (x <- e) (Some (store.update x (eval e s) s, h))
    
  | exec_assign_var_lookup : forall s h x e l z,
    Zgt (eval e s) Z0 -> (* the address looked up at is strictly greater than 0 *)
    val2loc (eval e s) = Some l -> (* and can be cast to a location *)
    heap.lookup l h = Some z -> (* we extract the corresponding cell contents if any *)
    exec (Some (s, h)) (x <-* e) (Some (store.update x z s, h))

  | exec_assign_var_lookup_err : forall s h x e,
    (Zle (eval e s) Z0) (* the address looked up at is negative *)
    \/
    ((Zgt (eval e s) Z0) /\ (* the address looked up at is positive but... *)
      (forall l, val2loc (eval e s) = Some l -> (* the corresponding location *)
	heap.lookup l h = None) (* is not allocated *)
    ) ->
    exec (Some (s, h)) (x <-* e) None

  | exec_assign_lookup_expr : forall s h e e' l z,
    ((Zgt (eval e s) Z0)) ->
    val2loc (eval e s) = Some l -> (* compute the (strictly positive) address *)
    heap.lookup l h = Some z -> (* extract the value (if ever present) *)
    (exec (Some (s, h)) (e *<- e') (Some (s, (heap.update l (eval e' s) h))))
    
  | exec_assign_lookup_expr_err : forall s h e e',
    (Zle (eval e s) Z0) (* fail if the address to be lookuperenced is not valid *)
    \/((Zgt (eval e s) Z0) /\
      (forall l, val2loc (eval e s) = Some l -> (* compute the (strictly positive) address *)
	heap.lookup l h = None) (* if the address is not allocated *)
    ) ->
    (exec (Some (s, h)) (e *<- e') None)

  | exec_malloc : forall s h x e n,
    n > 0 /\
    heap.disjoint h (heap.singleton n (eval e s)) ->
    exec (Some (s, h)) (x <-malloc e) (Some ((store.update x (Z_of_nat n) s), h +++ (heap.singleton n (eval e s))))

  | exec_free : forall s h e v l,
    val2loc (eval e s) = Some l ->
    heap.lookup l h = Some v->
    exec (Some (s, h)) (free e) (Some (s, (heap.dif h l)))

  | exec_free_err : forall s h e ,
    (Zle (eval e s) Z0) (* fail if the address to be lookuperenced is not valid *)
    \/((Zgt (eval e s) Z0) /\
      (forall l, val2loc (eval e s) = Some l -> (* compute the (strictly positive) address *)
	heap.lookup l h = None) (* if the address is not allocated *)
    ) ->
    (exec (Some (s, h)) (free e) None)
	
  | exec_seq : forall s s' s'' c d,
    exec s c s' -> exec s' d s'' ->
    exec s (c ; d) s''
    
  | exec_while_true : forall s h s' s'' b c,
    eval_b b s = true ->
    exec (Some (s, h)) c s' ->
    exec s' (while b c) s'' ->
    exec (Some (s, h)) (while b c) s''
    
  | exec_while_false : forall s h b c,
    eval_b b s = false ->
    exec (Some (s, h)) (while b c) (Some (s, h))
    
  | exec_ifte_true : forall b c d s h s',
    eval_b b s = true ->
    exec (Some (s, h)) c s' ->
    exec (Some (s, h)) (ifte b thendo c elsedo d) s'
    
  | exec_ifte_false : forall b c d s h s',
    eval_b b s = false ->
    exec (Some (s, h)) d s' ->
    exec (Some (s, h)) (ifte b thendo c elsedo d) s'.

Notation "s -- c --> t" := (exec s c t) (at level 82) : sep_scope.

Lemma from_none' : forall s0 c s, (s0 -- c --> s) -> s0 = None -> s = None.
do 4 intro.
induction H.
auto.
intro X; discriminate X.
intro X; discriminate X.
intro X; discriminate X.
intro X; discriminate X.
intro X; discriminate X.
intro X; discriminate X.
intro X; discriminate X.
intro X; discriminate X.
intro X; discriminate X.
auto.
intro X; discriminate X.
intro X; discriminate X.
intro X; discriminate X.
intro X; discriminate X.
Qed.

Lemma from_none : forall c s, (None -- c --> s) -> s = None.
intros; eapply from_none'.
apply H.
auto.
Qed.

(* Axiomatic Semantics *)

(* update the store used in an assertion using the value of an expr *)
Definition update_store2 (x:var.v) (e:expr) (P:assert) : assert :=
  fun s h => P (store.update x (eval e s) s) h.

(* update the store used in an assertion using the value held in a heap *)
Definition lookup2 (x:var.v) (e:expr) (P:assert) : assert :=
  fun s h =>
    exists p, val2loc (eval e s) = Some p /\
      exists z, heap.lookup p h = Some z /\
	P (store.update x z s) h.

(* update the heap used in an assertion *)
Definition update_heap2 (e:expr) (e':expr) (P:assert) : assert :=
fun s => fun h =>
  exists p, val2loc (eval e s) = Some p /\
    exists z, heap.lookup p h = Some z /\
      P s (heap.update p (eval e' s) h).

Inductive semax : assert -> cmd -> assert -> Prop :=
  semax_skip: forall P, semax P skip P
| semax_assign_var_e : forall P x e, 
  semax (update_store2 x e P) (x <- e) P
| semax_assign_var_lookup : forall P x e,
  (semax (lookup2 x e P) (x <-* e) P)
| semax_assign_lookup_expr : forall P e e',
  (semax (update_heap2 e e' P) (e *<- e') P)
| semax_malloc : forall P x e,
  (semax (fun s h => forall n, ((n |-> e) -* (update_store2 x n P)) s h)
    (x <-malloc e) P)
| semax_free : forall P e,
  (semax 
    (fun s h => 
      exists l, val2loc (eval e s) = Some l /\
	exists v, heap.lookup l h = Some v /\
	  P s (heap.dif h l))
    (free e)
    P)
| semax_seq : forall P Q R c d, 
  semax P c Q -> semax Q d R -> semax P (c ; d) R
| semax_while : forall P b c, 
  (semax (fun s h => ((P s h) /\ (eval_b b s)=true)) c P) -> 
  (semax P (while b c) (fun s => fun h => ((P s h) /\ (eval_b b s)=false)))
| semax_conseq : forall (P P' Q Q':assert) c,
  (Q' ==> Q) -> (P ==> P') -> 
  semax P' c Q' -> semax P c Q
| semax_ifte : forall P Q b c d,
  (semax (fun s h => (P s h) /\ (eval_b b s)=true) c Q) ->
  (semax (fun s h => (P s h) /\ (eval_b b s)=false) d Q) ->
  semax P (ifte b thendo c elsedo d) Q.

Notation "{{ P }} c {{ Q }}" := (semax P c Q) (at level 82) : sep_scope.

(** axiomatic semantic lemmas *)

Lemma semax_weaken_post : forall P (Q Q':assert) c,
  (Q' ==> Q) -> {{ P }} c {{ Q' }} -> {{ P }} c {{ Q }}.
intros.
apply semax_conseq with (P':=P) (Q':=Q').
auto.
red; auto.
auto.
Qed.

Lemma semax_strengthen_pre : forall (P:assert) (P':assert) Q c,
  (P ==> P') -> {{ P' }} c {{ Q }} -> {{ P }} c {{ Q }}.
intros.
apply semax_conseq with (P':=P') (Q':=Q).
red; auto.
auto.
auto.
Qed.

(* Definition of axiomatic semantic linked to the operationnal semantic *)

Definition semax' (P:assert) (c:cmd) (Q:assert) : Prop :=
    forall s h, (P s h -> ~(Some (s, h) -- c --> None)) /\
      (forall s' h', P s h -> (Some (s, h) -- c --> Some (s', h')) -> Q s' h').

Lemma semax_sound : forall P Q c,
  {{ P }} c {{ Q }} -> semax' P c Q.
intros.
induction H.
(****
 **** case skip
 ****)
red.
intros.
split.
intros.
red.
intro.
inversion H0.
intros.
inversion H0.
subst s' h'.
auto.
(****
 **** case semax_assign_var_e
 ****)
red.
intros.
split.
intro.
intro.
inversion_clear H0.
intros.
inversion H0.
subst h' s' e0 x0 h0 s0.
unfold update_store2 in H.
auto.
(****
 **** case semax_assign_var_lookup
 ****)
red.
intros.
split.
intro.
intro.
inversion_clear H0.
inversion_clear H1.
red in H.
inversion_clear H.
inversion_clear H1.
generalize (val2loc_neg _ H0); intros.
rewrite H in H1; discriminate H1.
inversion_clear H0.
red in H.
inversion_clear H.
inversion_clear H0.
generalize (H2 _ H); intro.
inversion_clear H3.
inversion_clear H4.
rewrite H0 in H3; discriminate H3.
intros.
inversion H0.
subst h' s' s0 h0 x0 e0.
unfold lookup2 in H.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
inversion_clear H1.
rewrite H in H8; injection H8; clear H8; intro; subst x0.
generalize (heap.heap_is_function _ _ _ H9 _ H2); intro; subst x1.
auto.
(***
 *** case semax_assign_lookup_expr
 ***)
red.
intros.
split.
intro.
intro.
inversion_clear H0.
inversion_clear H1.
red in H.
inversion_clear H.
inversion_clear H1.
generalize (val2loc_neg _ H0); intro.
rewrite H in H1; discriminate H1.
inversion_clear H0.
inversion_clear H.
inversion_clear H0.
generalize (H2 _ H); intro.
inversion_clear H3.
inversion_clear H4.
rewrite H0 in H3; discriminate H3.
intros.
inversion H0.
subst s' h' s0 h0 e0 e'0.
unfold update_heap2 in H.
inversion_clear H.
inversion_clear H1.
rewrite H8 in H; injection H; clear H; intro; subst x.
inversion_clear H2.
inversion_clear H.
auto.
(***
 *** case semax_malloc
 ***)
red.
intros.
split.
intro.
intro.
inversion H0.
intros.
inversion H0.
subst s0 h0 x0 e0 s' h'.
generalize (H (int_e (Z_of_nat n))); clear H; intro.
unfold update_store2 in H.
simpl in H.
unfold sep.imp in H.
apply H with (h':=(heap.singleton n (eval e s))); auto.
split; auto.
inversion_clear H2.
auto.
exists n.
simpl.
split; auto.
apply Z_of_nat2loc.
intuition.
apply heap.equal_refl.
apply heap.equal_refl.
(***
 *** case semax_free
 ***)
red.
intros.
split.
intro.
intro.
inversion H0.
subst s0 h0 e0.
inversion_clear H.
inversion_clear H1.
inversion_clear H3.
inversion_clear H1.
inversion_clear H2.
generalize (val2loc_neg _ H1); intro.
rewrite H in H2; discriminate H2.
inversion_clear H1.
generalize (H5 _ H); intros.
rewrite H3 in H1; discriminate H1.
intros.
inversion_clear H.
inversion_clear H1.
inversion_clear H2.
inversion_clear H1.
inversion H0.
subst s0 h0 e0 s' h'.
rewrite H in H7.
injection H7; intro; subst x.
auto.
(****
 **** case semax_seq
 ****)
red.
intros.
split.
intro.
intro.
inversion_clear H2.
red in IHsemax1.
generalize (IHsemax1 s h); intro.
inversion_clear H2.
destruct s'.
destruct s0.
generalize (H6 _ _ H1 H3); intro.
generalize (IHsemax2 s0 h0); intro.
inversion_clear H7.
tauto.
tauto.
intros.
inversion_clear H2.
red in IHsemax1.
red in IHsemax2.
destruct s'0.
destruct s0 as [s'' h''].
generalize (IHsemax1 s h); intro.
inversion_clear H2.
generalize (H6 _ _ H1 H3); intro.
generalize (IHsemax2 s'' h''); intro.
inversion_clear H7.
apply (H9 _ _ H2 H4).
generalize (from_none _ _ H4); intro.
discriminate H2.
(****
 **** case semax_while
 ****)
red.
intros.
split.
intro.
intro.
assert (exists d, d = while b c).
exists (while b c); auto.
inversion_clear H2.
rewrite <-H3 in H1.
assert (exists S, S=(Some (s, h))).
exists (Some (s, h)); auto.
inversion_clear H2.
rewrite <-H4 in H1.
generalize P b c H IHsemax s h H0 H3 H4;
clear P b c H IHsemax s h H0 H3 H4.
rename x into C.
rename x0 into st0.
assert (exists S, S=(@None state)).
exists (@None state); auto.
inversion_clear H.
rewrite <-H0 in H1.
generalize H0; clear H0.
rename x into st'.
induction H1.
intros.
discriminate H4.
intros.
discriminate H3.
intros.
discriminate H3.
intros.
discriminate H5.
intros.
discriminate H3.
intros.
discriminate H5.
intros.
discriminate H3.
intros.
discriminate H3.
intros.
discriminate H4.
intros.
discriminate H3.
intros.
discriminate H3.
intros.
injection H4; clear H4; intros; subst s0 h0.
injection H3; clear H3; intros; subst b0 c0.
red in IHsemax.
generalize (IHsemax s h); intro.
inversion_clear H3.
generalize (H4 (conj H2 H)); clear H4; intro.
destruct s'.
destruct s0.
generalize (H5 s0 h0 (conj H2 H) H1_); clear H5; intro.
generalize (IHexec2 H0 _ _ _ H1 IHsemax _ _ H4).
auto.
tauto.
intros.
discriminate H0.
intros.
discriminate H4.
intros.
discriminate H4.
intros.
assert (exists d, d = while b c).
exists (while b c); auto.
inversion_clear H2 as [C].
rewrite <-H3 in H1.
assert (exists S, S=(Some (s, h))).
exists (Some (s, h)); auto.
inversion_clear H2 as [sigma].
rewrite <-H4 in H1.
assert (exists S, S=(Some (s', h'))).
exists (Some (s', h')); auto.
inversion_clear H2 as [sigma'].
rewrite <-H5 in H1.
generalize P b c H IHsemax s h s' h' H0 H3 H4 H5;
clear P b c H IHsemax s h s' h' H0 H3 H4 H5.
induction H1.
intros.
discriminate H4.
intros.
discriminate H3.
intros.
discriminate H3.
intros.
discriminate H4.
intros.
discriminate H5.
intros.
discriminate H4.
intros.
discriminate H3.
intros.
discriminate H3.
intros.
discriminate H3.
intros.
discriminate H3.
intros.
discriminate H3.
(****
 **** case exec_while true
 ****)
intros.
injection H3; clear H3; intros; subst c0 b0.
injection H4; clear H4; intros; subst h0 s0.
clear IHexec1.
rename s'' into sigma'.
rename s' into sigma''.
rename s'0 into s'.
(* we know s,h |= P /\ b, by the inductive hypothesis IHsemax we have sigma'' |= P *)
induction sigma''.
induction a.
rename a into s''.
rename b0 into h''.
assert (P s'' h'').
red in IHsemax.
generalize (IHsemax s h); intro.
inversion_clear H2.
apply H4; auto.
(* since sigma'' --while b c--> sigma' and {P}while b c{P /\ ~b}, then we have sigma' |= P /\ ~b *)
generalize (IHexec2 _ _ _ H0 IHsemax _ _ s' h' H2 (refl_equal (while b c)) (refl_equal (Some (s'', h'')))); intro.
auto.
generalize (from_none _ _ H1_0); intro X; rewrite H5 in X; discriminate X.
(****
 **** case exec_while false 
 ****)
intros.
injection H5; clear H5; intros; subst s' h'.
injection H4; clear H4; intros; subst s0 h0.
injection H3; clear H3; intros; subst b0 c0.
auto.
intros.
discriminate H3.
intros.
discriminate H3.
(****
 **** 
 ****)
red.
intros.
split.
intro.
intro.
red in IHsemax.
generalize (IHsemax s h); intros.
inversion_clear H4.
apply H5.
apply H0.
auto.
auto.
intros.
red in IHsemax.
generalize (IHsemax s h);intro.
inversion_clear H4.
apply H.
apply H6.
apply H0.
auto.
auto.
(****
 **** ifte
 ****)
red.
intros.
cut (((eval_b b s)=true)\/((eval_b b s)=false)).
intro.
split.
intro.
intro.
inversion_clear H3.
red in IHsemax1.
generalize (IHsemax1 s h); intro.
inversion_clear H3.
apply H6.
auto.
auto.
generalize (IHsemax2 s h); intro.
inversion_clear H3.
apply H6.
auto.
auto.
intros.
inversion_clear H3.
red in IHsemax1.
generalize (IHsemax1 s h); intro.
inversion_clear H3.
apply H7.
auto.
auto.
(* on doit prouver que "s,h -- c --> s',h'" est vrai, il suffit 
d'inverser la derivation H3 et d'utilise le fait que (eval_b b s)=true *)
inversion_clear H1.
rewrite H4 in H3; discriminate H3.
(* cas ou eval_b b s <> true, pareil que ci-dessus *)
red in IHsemax2.
generalize (IHsemax2 s h); intro.
inversion_clear H1.
apply H7.
auto.
auto.
case (eval_b b s); auto.
Qed.

Definition semax_alternative (P:assert) (c:cmd) (Q:assert) : Prop :=
  forall s h, P s h ->
    (forall s' h', ((Some (s, h)) -- c --> (Some (s', h'))) -> (Q s' h')).

Lemma semax_sound_alternative : forall P Q c,
  {{ P }} c {{ Q }} -> semax_alternative P c Q.
intros.
generalize (semax_sound _ _ _ H); intro.
red in H0.
red.
intros.
generalize (H0 s h); intro.
inversion_clear H3.
auto.
Qed.

(*
 * derived Reynolds' axioms
 *)

Lemma semax_assign_var_lookup_backwards : forall x e P,
  {{ fun s h => exists e0, ((e |-> e0) ** ((e |-> e0) -* (update_store2 x e0 P))) s h }} x <-* e {{ P }}.
intros.
apply semax_strengthen_pre with (lookup2 x e P).
do 3 intro.
inversion_clear H.
generalize (sep.mp _ _ _ _ H0); intro.
red in H.
red.
inversion_clear H0.
inversion_clear H1.
inversion_clear H0.
inversion_clear H2.
inversion_clear H3.
inversion_clear H2.
inversion_clear H3.
exists x3.
split; auto.
exists (eval x0 s).
split; auto.
apply heap.lookup_equal with (x1 +++ x2).
apply heap.equal_sym; auto.
apply heap.lookup_union; auto.
eapply heap.lookup_equal with (heap.singleton x3 (eval x0 s)).
Equal_heap.
rewrite heap.lookup_singleton; auto.
apply semax_assign_var_lookup.
Qed.

Lemma semax_assign_var_lookup_backwards_alternative : forall x e P e0,
  {{ (e |-> e0) ** ((e |-> e0) -* (update_store2 x e0 P)) }} x <-* e {{ P }}.
intros.
apply semax_strengthen_pre with 
(fun s => fun h =>
    exists e0, ((e |-> e0) ** ((e |-> e0) -* (update_store2 x e0 P))) s h).
intros.
exists e0.
auto.
apply semax_assign_var_lookup_backwards.
Qed.

Lemma semax_assign_lookup_expr_local: forall x v v',
    {{ x |-> v }} x *<- v' {{ x |-> v' }}.
intros.
apply semax_conseq with (P':=(update_heap2 x v' (x|->v')))
(Q':=(x|->v')) (c:=(assign_lookup_expr x  v')).
red; intros.
intuition.
red; intros.
inversion_clear H.
inversion_clear H0.
red.
exists x0; auto.
split; auto.
exists (eval v s).
split.
eapply heap.lookup_equal with (heap.singleton x0 (eval v s)).
Equal_heap.
apply heap.lookup_singleton.
exists x0.
split; auto.
apply heap.equal_trans with (heap.update x0 (eval v' s) (heap.singleton x0 (eval v s))).
apply heap.equal_update.
apply H1.
eapply heap.update_singleton.
apply semax_assign_lookup_expr.
Qed.

(*
 * frame rule
 *)

Fixpoint modified_cmd_var (c:cmd) {struct c} : list var.v :=
  match c with 
    skip => nil
    | x <- e => x::nil
    | x <-* e => x::nil
    | e *<- f => nil
    | x <-malloc e => x::nil
    | free e => nil
    | c1 ; c2 => (modified_cmd_var c1) ++ (modified_cmd_var c2)
    | ifte a thendo c1 elsedo c2 => (modified_cmd_var c1) ++ (modified_cmd_var c2)
    | while a c1 => (modified_cmd_var c1)
   end.

Fixpoint modified_loc_expr (c:cmd) {struct c} : list expr :=
  match c with 
    skip => nil
    | x <- e => nil
    | x <-* e => nil
    | e *<- f => e::nil
    | x <-malloc e => nil
    | free e => e::nil
    | c1 ; c2 => (modified_loc_expr c1) ++ (modified_loc_expr c2)
    | ifte a thendo c1 elsedo c2 => (modified_loc_expr c1) ++ (modified_loc_expr c2)
    | while a c1 => (modified_loc_expr c1)
  end.

Lemma inde_seq : forall R c d,
  inde (modified_cmd_var (c; d)) R ->
  (inde (modified_cmd_var c) R)/\(inde (modified_cmd_var d) R).
intros.
split.
red.
intros.  
split; intro.
red in H.
generalize (H s h x v); intro.
assert (In x (modified_cmd_var (c; d))).
simpl.
apply in_or_app.
auto.
tauto.
red in H.
generalize (H s h x v); intros.
assert (In x (modified_cmd_var (c; d))).
simpl.
apply in_or_app.
auto.
tauto.
red.
intros.  
split; intro.
red in H.
generalize (H s h x v); intro.
assert (In x (modified_cmd_var (c; d))).
simpl.
apply in_or_app.
auto.
tauto.
red in H.
generalize (H s h x v); intros.
assert (In x (modified_cmd_var (c; d))).
simpl.
apply in_or_app.
auto.
tauto.
Qed.

Lemma inde_ifte : forall R b c d,
  inde (modified_cmd_var (ifte b thendo c elsedo d)) R ->
  (inde (modified_cmd_var c) R)/\(inde (modified_cmd_var d) R).
intros.
split.
red.
intros.
red in H.
generalize (H s h x v); intro.
apply H1.
simpl.
apply in_or_app.
auto.
red.
intros.
red in H.
generalize (H s h x v); intro.
apply H1.
simpl.
apply in_or_app.
auto.
Qed.

Lemma frame_rule : forall P c Q,
  {{P}} c {{Q}} -> 
  forall R , 
    (inde (modified_cmd_var c) R -> 
      {{ P ** R }} c {{ Q ** R }}).
do 4 intro.
induction H.
(* skip *)
intros.
apply semax_skip.
(* x <- e *)
intros.
apply semax_strengthen_pre with (update_store2 x e (P**R)).
red; intros.
red in H0.
inversion_clear H0 as [h1].
inversion_clear H1 as [h2].
decompose [and] H0; clear H0.
red.
exists h1; exists h2.
split; auto.
split; auto.
split; auto.
red in H.
apply inde_update_store.
simpl in H.
auto.
auto.
apply semax_assign_var_e.
(* x <-* e *)
intros.
apply semax_strengthen_pre with (lookup2 x e (P**R)).
red; intros.
red in H0.
red.
inversion_clear H0 as [h1].
inversion_clear H1 as [h2].
decompose [and] H0; clear H0.
unfold lookup2 in H2.
inversion_clear H2 as [p].
inversion_clear H0.
inversion_clear H4 as [z].
inversion_clear H0.
exists p; split; auto; exists z; split.
apply heap.lookup_equal with (h1 +++ h2).
apply heap.equal_sym; auto.
apply heap.lookup_union; auto.
exists h1; exists h2.
split; auto.
split; auto.
split; auto.
apply inde_update_store.
auto.
auto.
apply semax_assign_var_lookup.
(* e *<- e' *)
intros.
apply semax_strengthen_pre with (update_heap2 e e' (P**R)).
red; intros.
red.
red in H0.
inversion_clear H0 as [h1].
inversion_clear H1 as [h2].
decompose [and] H0; clear H0.
red in H2.
inversion_clear H2 as [p].
inversion_clear H0.
inversion_clear H4 as [z].
inversion_clear H0.
exists p; split; auto; exists z; split.
apply heap.lookup_equal with (h1 +++ h2).
apply heap.equal_sym; auto.
apply heap.lookup_union; auto.
exists (heap.update p (eval e' s) h1); exists h2.
split.
apply heap.disjoint_update.
auto.
split.
apply heap.equal_update_L.
auto.
auto.
eapply heap.lookup_In.
apply H4.
auto.
apply semax_assign_lookup_expr.
(* x <-malloc e *)
intros.
apply semax_strengthen_pre with (fun s h =>
  forall n , ((n |-> e) -* update_store2 x n (P ** R)) s h).
red; intros.
red; intros.
red in H0.
inversion_clear H0 as [h1].
inversion_clear H3 as [h2].
decompose [and] H0; clear H0.
generalize (H4 n); clear H4; intro.
red in H0.
generalize (H0 h'); clear H0; intro.
assert (h1 # h').
apply heap.equal_union_disjoint with h2 h.
split; auto.
intuition.
generalize (H0 (conj H4 (proj2 H1))); clear H0; intro.
generalize (H0 (h1 +++ h')); clear H0; intro.
generalize (H0 (heap.equal_refl (h1 +++ h'))); clear H0; intro.
red in H0.
red.
exists (h1+++h'); exists h2.
split.
apply heap.disjoint_com.
apply heap.disjoint_union.
split.
apply heap.disjoint_com; auto.
apply heap.equal_union_disjoint with h1 h.
split.
apply heap.equal_trans with (h1+++h2); auto.
apply heap.union_com.
auto.
intuition.
split.
apply heap.equal_trans with (h2 +++ (h1 +++ h')).
apply heap.equal_trans with ((h2 +++ h1) +++ h').
apply heap.equal_trans with (h +++ h'); auto.
apply heap.equal_union.
apply heap.equal_trans with (h1 +++ h2); auto.
apply heap.union_com; auto.
apply heap.disjoint_com; intuition.
apply heap.equal_sym.
apply heap.union_assoc.
apply heap.union_com.
apply heap.disjoint_union.
split.
apply heap.disjoint_com; auto.
apply heap.equal_union_disjoint with h1 h.
split.
apply heap.equal_trans with (h1+++h2); auto.
apply heap.union_com.
auto.
intuition.
split; auto.
red in H.
generalize (H s h2 x (eval n s)); clear H; intro.
simpl in H.
tauto.
apply semax_malloc.
(* free *)
intros.
apply semax_strengthen_pre with (fun (s : store.s) (h : heap.h) =>
      exists l : loc,
        val2loc (eval e s) = Some l /\
        (exists v0 : heap.v, heap.lookup l h = Some v0 /\ (P ** R) s (heap.dif h l))).
red; intros.
inversion_clear H0.
inversion_clear H1.
decompose [and] H0; clear H0.
inversion_clear H2.
decompose [and] H0; clear H0.
inversion_clear H4.
inversion_clear H0.
exists x1.
split; auto.
exists x2.
split.
apply heap.lookup_equal with (x+++x0).
apply heap.equal_sym; auto.
apply heap.lookup_union.
auto.
auto.
exists (heap.dif x x1).
exists x0. 
assert (x0 === (heap.dif x0 x1)).
apply heap.equal_sym.
apply heap.dif_disjoint with x2.

generalize (heap.lookup_exists_partition x x1 x2 H4); intros.
inversion_clear H0.
inversion_clear H7.
Disjoint_heap.

split.

apply heap.disjoint_equal with (heap.dif x0 x1).
apply heap.dif_disjoint'.
auto.
apply heap.equal_sym; auto.
split; auto.

apply heap.equal_trans with (heap.dif (x +++ x0) x1).
apply heap.dif_equal.
auto.
apply heap.equal_trans with (heap.dif x x1 +++ heap.dif x0 x1).
apply heap.dif_union.
apply heap.equal_trans with (heap.dif x0 x1 +++ heap.dif x x1).
apply heap.union_com.
apply heap.dif_disjoint'.
auto.
apply heap.equal_trans with ( x0 +++ heap.dif x x1).
apply heap.equal_union.
Equal_heap.
apply heap.dif_disjoint'.
auto.
apply heap.union_com.
apply heap.disjoint_com.
apply heap.disjoint_equal with (heap.dif x0 x1).
apply heap.dif_disjoint'.
auto.
Equal_heap.
apply semax_free.
(* sequence *)
intros.
apply semax_seq with (Q ** R0).
apply semax_strengthen_pre with (P ** R0).
red; auto.
generalize (IHsemax1 R0); intro.
apply IHsemax1.
exact (proj1 (inde_seq _ _ _ H1)).
apply (IHsemax2 R0).
apply (proj2 (inde_seq _ _ _ H1)).
(* while true *)
intros.
apply semax_weaken_post with (
  fun s h =>
    ((P ** R) s h /\ eval_b b s = false)
).
red; intros.
red.
inversion_clear H1.
red in H2.
inversion_clear H2 as [h1].
inversion_clear H1 as [h2].
decompose [and] H2; clear H2.
exists h1; exists h2; auto.
apply semax_strengthen_pre with (
  fun s h => (P ** R) s h
).
red; intros.
auto.
apply semax_while with (P:=P**R).
assert (inde (modified_cmd_var c) R).
auto.
generalize (IHsemax _ H1); intro.
apply semax_strengthen_pre with (
fun s h => ((fun s0 h0 => P s0 h0 /\ eval_b b s0 = true) ** R) s h
).
red; intros.
red.
inversion_clear H3.
red in H4.
inversion_clear H4 as [h1].
inversion_clear H3 as [h2].
decompose [and] H4; clear H4.
exists h1; exists h2; auto.
auto.
(* semax_conseq *)
intros.
generalize (IHsemax _ H2); intros.
apply semax_strengthen_pre with (P' ** R).
red; intros.
red in H4.
inversion_clear H4 as [h1].
inversion_clear H5 as [h2].
decompose [and] H4; clear H4.
exists h1; exists h2; auto.
apply semax_weaken_post with (Q' ** R).
red; intros.
inversion_clear H4 as [h1].
inversion_clear H5 as [h2].
decompose [and] H4; clear H4.
exists h1; exists h2; auto.
auto.
(* semax_ifte *)
intros.
apply semax_ifte.
assert (inde (modified_cmd_var c) R).
exact (proj1 (inde_ifte _ _ _ _ H1)).
generalize (IHsemax1 _ H2); intro.
apply semax_strengthen_pre with (
fun s h => ((fun s0 h0 => P s0 h0 /\ eval_b b s0 = true) ** R) s h 
); auto.
red; intros.
inversion_clear H4.
red in H5.
inversion_clear H5 as [h1].
inversion_clear H4 as [h2].
decompose [and] H5; clear H5.
red.
exists h1; exists h2; auto.
assert (inde (modified_cmd_var d) R).
exact (proj2 (inde_ifte _ _ _ _ H1)).
generalize (IHsemax2 _ H2); intro.
apply semax_strengthen_pre with (
fun s h => ((fun s0 h0 => P s0 h0 /\ eval_b b s0 = false) ** R) s h
); auto.
red; intros.
inversion_clear H4.
red in H5.
inversion_clear H5 as [h1].
inversion_clear H4 as [h2].
decompose [and] H5; clear H5.
red.
exists h1; exists h2; auto.
Qed.

Ltac Frame_rule_pre A :=
      match goal with
             | |- {{?a1 **  A }} ?c {{?Q}} => idtac
             | |- {{ A ** ?a1}} ?c {{?Q}} => rewrite (sep.con_com_equiv A a1)
             | |- {{ (?a1 ** ?a2) ** ?a3}} ?c {{?Q}} => rewrite (sep.con_assoc_equiv a2 a1 a3); Frame_rule_pre A
             | |- {{ ?a1 ** ?a2}} ?c {{?Q}} => rewrite (sep.con_com_equiv a1 a2); Frame_rule_pre A
      end.

Ltac Frame_rule_post A :=
      match goal with
             | |- {{?P}} ?c {{?a1 **  A }} => idtac
             | |- {{?P}} ?c {{ A ** ?a1}} => rewrite (sep.con_com_equiv A a1)
             | |- {{?P}} ?c {{ (?a1 ** ?a2) ** ?a3}} => rewrite (sep.con_assoc_equiv a2 a1 a3); Frame_rule_post A
             | |- {{?P}} ?c {{ ?a1 ** ?a2}} => rewrite (sep.con_com_equiv a1 a2); Frame_rule_post A
      end.

Ltac Frame_rule A := 
                match goal with
                    | |- {{?P}} ?c {{?Q}} => 
                        (Frame_rule_pre  A); (Frame_rule_post A); 
                        eapply frame_rule
                end.

Lemma semax_free_global_backwards : forall e v P, 
  {{ (e |-> v) ** P }} free e {{ sep.emp ** P }}.
intros.
apply frame_rule.
apply semax_strengthen_pre with 
(fun s h =>
         exists l : loc,
           val2loc (eval e s) = Some l /\
           (exists v0 : heap.v,
              heap.lookup l h = Some v0 /\ sep.emp s (heap.dif h l))).
red; intros.
inversion_clear H.
inversion_clear H0.
exists x.
split; auto.
exists (eval v s).
split.
eapply heap.lookup_equal with (heap.singleton x (eval v s)).
Equal_heap.
apply heap.lookup_singleton.
red.
eapply heap.equal_trans with ((heap.singleton x (eval v s)) --- x).
eapply heap.dif_equal.
auto.
apply heap.dif_singleton_emp.
apply semax_free.
simpl.
red.
intros.
simpl in H.
tauto.
Qed.

(*
 * more Reynolds' axioms
 *)

Lemma semax_assign_lookup_expr_global : forall P e e',
  {{ (fun s' h' => exists e'', ((e |-> e'') s' h')) ** P }} e *<- e' {{ (e |-> e') ** P }}.
intros.
apply frame_rule.
apply semax_strengthen_pre with (update_heap2 e e' (e |-> e')).
red; intros.
inversion_clear H.
red in H0.
inversion_clear H0.
red.
exists x0; split; intuition.
exists (eval x s); split; auto.
eapply heap.lookup_equal with (heap.singleton x0 (eval x s)).
Equal_heap.
apply heap.lookup_singleton.
red.
exists x0; split; auto.
eapply heap.equal_trans with (heap.update x0 (eval e' s) (heap.singleton x0 (eval x s))).
eapply heap.equal_update.
auto.
apply heap.update_singleton.
apply semax_assign_lookup_expr.
simpl.
red; intros.
simpl in H; contradiction.
Qed.

Lemma semax_assign_lookup_expr_global_alternative : forall P e e' e'',
  {{ (e |-> e'') ** P }} e *<- e' {{ (e |-> e') ** P }}.
intros.
apply semax_strengthen_pre with ((fun s' => fun h' => exists e'', (e |-> e'') s' h') ** P).
red; intros.
red in H.
inversion_clear H.
inversion_clear H0.
decompose [and] H; clear H.
exists x; exists x0.
split; auto.
split; auto.
split; auto.
exists e''.
auto.
apply semax_assign_lookup_expr_global.
Qed.

Lemma semax_assign_lookup_expr_backwards : forall P e e',
  {{ fun s h => exists e'', ((e |-> e'') ** ((e |-> e') -* P)) s h }} e *<- e' {{ P }}.
intros.
generalize (semax_assign_lookup_expr_global ((e |-> e') -* P) e e'); intro.
apply semax_weaken_post with ((e |-> e') ** ((e |-> e') -* P)).
apply sep.mp.
apply semax_strengthen_pre with
((fun s' h' => exists e'' : expr, (e |-> e'') s' h' ) ** ((e |-> e') -* P)).
red; intros.
inversion_clear H0.
red.
inversion_clear H1.
exists x0.
inversion_clear H0.
exists x1.
decompose [and] H1; clear H1.
split; auto.
split; auto.
split; auto.
exists x; auto.
auto.
Qed.

Lemma semax_assign_lookup_expr_backwards_alternative : forall P e e' e'',
  {{ (e |-> e'') ** ((e |-> e') -* P) }} e *<- e' {{ P }}.
intros.
generalize (semax_assign_lookup_expr_global_alternative ((e |-> e') -* P) e e' e''); intro.
apply semax_weaken_post with ((e |-> e') ** ((e |-> e') -* P)).
apply sep.mp.
auto.
Qed.