(*
 *  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
 *)

Load seplog_header.

Open Local Scope Z_scope.

(** Factorial *)

(* Axiomatic definition of the factorial function *)

Axiom facto : Z -> Z.
Axiom facto_neg : forall z, z < 0 -> (facto z)=1.
Axiom facto_zero : (facto 0)=1.
Axiom facto_pos : forall z, z > 0 -> (facto z)=z*(facto (z - 1)).

Lemma factorial : forall n, (0 <= n)->
{{ fun s h => (store.lookup O s)=n /\ (store.lookup 1%nat s)=1 }}
while (var_e O =/= int_e 0%Z)
(
1%nat <- (var_e 1%nat) *e (var_e O) ;
O <- (var_e O) -e (int_e 1%Z)
)
{{ fun s h => (store.lookup 1%nat s) = (facto n) }}. 

intros n n_pos.

apply semax_weaken_post with (fun s => fun _:heap.h =>
  (store.lookup 1%nat s) * (facto (store.lookup O s)) = (facto n) /\ 
  ((store.lookup O s) >= 0) /\ (~(((store.lookup O) s) <> 0))).

red; intros.
decompose [and] H; clear H.
rewrite <-H0.
assert (store.lookup 0%nat s = 0).
apply NNPP.
auto.
rewrite H.
rewrite facto_zero.

ring.

apply semax_strengthen_pre with (fun s => fun _:heap.h =>
(store.lookup 1%nat s) * (facto (store.lookup 0%nat s)) = (facto n) /\
(store.lookup 0%nat s) >= 0).

red; intros.
inversion_clear H.
rewrite H0.
rewrite H1.
split; auto.
ring.
omega.

apply semax_weaken_post with (fun s => fun _:heap.h =>
  ((store.lookup 1%nat s) * (facto (store.lookup 0%nat s)) = (facto n) /\ 
  (store.lookup 0%nat s) >= 0) /\ 
  (eval_b ((var_e 0%nat) =/= (int_e 0)) s)=false).

red; intros.
simpl in H.
decompose [and] H; clear H.
split.
auto.
split.
auto.
assert ((Zeq_bool (store.lookup 0%nat s) 0) = true).
apply negb_false_is_true.
auto.
intro.
apply H0.
generalize (eqb_val0 _ H); intro.
auto.

apply semax_while with (P:=(fun s => fun _:heap.h =>
  (((store.lookup 1%nat s) * (facto (store.lookup 0%nat s))) = (facto n) /\
  ((store.lookup 0%nat s) >= 0)))).

apply semax_seq with (fun s => fun _:heap.h =>
  ((store.lookup 1%nat s) * (facto ((store.lookup 0%nat s) - 1))) = facto n /\
  (store.lookup 0%nat s) - 1 >= 0).

apply semax_strengthen_pre with (update_store2 1%nat ((var_e 1%nat) *e (var_e O)) 
  (fun s => fun _:heap.h =>
    ((store.lookup 1%nat s) * (facto ((store.lookup 0%nat s) - 1))) = facto n /\ 
    (store.lookup 0%nat s) - 1 >= 0)).

red; intros.
red.
simpl.
rewrite store.lookup_update'.
split.
elim store.lookup_update.
decompose [and] H; clear H.
rewrite <-H2.
pattern (facto (store.lookup 0%nat s)).
rewrite facto_pos.
rewrite Zmult_assoc.
auto.
assert ((store.lookup O s)<>0).
generalize (negb_true_is_false _ H1); intro.
generalize (eqb_v0' (store.lookup O s) 0); intro.
apply H0.
auto.

cut (forall z, z >= 0 -> z <> 0 -> z > 0); 
[intro X; apply X; auto | intros; omega].

auto.

elim store.lookup_update.
decompose [and] H; clear H.

simpl in H1.

generalize (bool_5 _ H1); intro.
unfold eqb in H.

cut (forall z, z >= 0 -> z <> 0 -> z - 1 >= 0);
[intro X; apply X; auto | intros; omega].

intro.
apply H.
rewrite H0.
auto.

auto.

apply semax_assign_var_e.

apply semax_strengthen_pre with 
(update_store2 O ((var_e 0%nat) -e (int_e 1))
(fun s => fun _:heap.h =>
     ((store.lookup 1%nat s) * (facto (store.lookup 0%nat s))) = (facto n) /\ 
     (store.lookup O%nat s) >= 0)).

unfold update_store2.
simpl.
red; intros.
elim store.lookup_update.
rewrite store.lookup_update'.
auto.
auto.
apply semax_assign_var_e.
Qed.

Open Local Scope vc_scope.

Lemma vc_factorial : forall n, n >= 0 ->
{{ fun s => fun _:heap.h => (store.lookup O s)=n /\ (store.lookup 1%nat s)=1 }}
(proj_cmd 
  (while' (var_e 0%nat =/= int_e 0)
    (fun s => fun _:heap.h => ((store.lookup 1%nat s) * (facto (store.lookup O%nat s))) = (facto n) /\ ((store.lookup O s) >= 0))
    (1%nat <- (var_e 1%nat) *e (var_e O) ;
      O <- (var_e O) -e (int_e 1))))
{{ fun s => fun _:heap.h =>  (store.lookup 1%nat s) = (facto n) }}. 
intros.
apply wp_vc_util.
intros.
(* vc *)
simpl.
split.
intros.
decompose [and] H0; clear H0.
rewrite <-H3.
assert ((Zeq_bool (store.lookup 0%nat s) 0)=true).
apply negb_false_is_true; auto.
rewrite (eqb_val0 _ H0).
rewrite facto_zero.
ring.
split.
intros.
decompose [and] H0; clear H0.
red.
red.
simpl.
rewrite store.lookup_update'.
elim store.lookup_update.
rewrite store.lookup_update'.
elim store.lookup_update.
rewrite <-H3.
split.
pattern (facto (store.lookup 0%nat s)).
rewrite facto_pos.
rewrite Zmult_assoc.
auto.
assert ((store.lookup 0%nat s) <> 0).
assert ((Zeq_bool (store.lookup 0%nat s) 0)=false).
apply negb_true_is_false; auto.
generalize (eqb_v0' (store.lookup O s) 0); intro.
tauto.

cut (forall z, z >= 0 -> z <> 0 -> z > 0);
[intro X; apply X; auto | intros; omega].

assert ((store.lookup 0%nat s) <> 0).
assert ((Zeq_bool (store.lookup 0%nat s) 0) = false).
apply negb_true_is_false; auto.
apply (eqb_v0' _ _ H0).

cut (forall z, z >= 0 -> z <> 0 -> z - 1 >= 0);
[intro X; apply X; auto | intros; omega].
auto.
auto.
split; red; auto.
(* wp *)
intros.
simpl.
split.
inversion_clear H0.
rewrite H1.
rewrite H2.
ring.
inversion_clear H0.
subst n.
auto.
Qed.

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

(** swap *)

Close Local Scope vc_scope.
Open Local Scope sep_scope.

Lemma swap: forall x y z v a b, (var.set (x::y::z::v::nil)) ->
  {{ ((var_e x) |-> (int_e a)) ** ((var_e y) |-> (int_e b)) }}
  z <-* (var_e x); 
  v <-* (var_e y); 
  (var_e x) *<- (var_e v); 
  (var_e y) *<- (var_e z)
  {{ ((var_e x) |-> (int_e b)) ** ((var_e y) |-> (int_e a)) }}.
intros.

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

(* We split to handle the first instruction *)

apply semax_seq with (
  fun s => fun h =>
    ((var_e x |-> int_e a) ** (var_e y |-> int_e b)) s h /\ 
    eval (var_e z) s = a
).

(* We show that it can be handle by semax_assign_var_deref *)

apply semax_strengthen_pre with (
lookup2 z (var_e x)
(fun s => fun h =>
     ((var_e x |-> int_e a) ** (var_e y |-> int_e b)) s h /\
     eval (var_e z) s = a)
).

red; intros.
red.
inversion_clear H0 as [h1].
inversion_clear H1 as [h2].
decompose [and] H0; clear H0.
inversion_clear H2.
inversion_clear H0.
simpl in H4.
exists x0.
split; auto.
exists a.
split.
apply heap.lookup_equal with (heap.union h1 h2).
apply heap.equal_sym; auto.
apply heap.lookup_union; auto.
eapply heap.lookup_equal.
apply heap.equal_sym.
apply H4.
rewrite heap.lookup_singleton; auto.
split.

apply inde_update_store; auto.
apply inde_sep_con.
apply inde_mapsto.
simpl.
apply inter_weak.
apply inter_nil.
simpl.
red in H; simpl in H; intuition.
simpl.
apply inter_sym.
apply inter_nil.
apply inde_mapsto.
simpl.
apply inter_weak.
apply inter_nil.
simpl.
red in H; simpl in H; intuition.
simpl.
apply inter_sym.
apply inter_nil.

exists h1; exists h2.
split; auto.
split; auto.
split; auto.
exists x0; auto.
simpl.
rewrite store.lookup_update'; auto.

apply semax_assign_var_lookup.

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

(* We split to handle the second instruction *)

apply semax_seq with (
fun s h =>
  ((var_e x |-> int_e a) ** (var_e y |-> int_e b)) s h /\
  eval (var_e z) s = a /\ eval (var_e v) s = b
).

apply semax_strengthen_pre with (
lookup2 v (var_e y)
(fun s h =>
     ((var_e x |-> int_e a) ** (var_e y |-> int_e b)) s h /\
     eval (var_e z) s = a /\ (eval (var_e v) s = b))
).

red; intros.
red.
inversion_clear H0.
inversion_clear H1.
inversion_clear H0.
decompose [and] H1; clear H1.
inversion_clear H6.
inversion_clear H1.
exists x2; split; auto.
exists b.
split.
apply heap.lookup_equal with (heap.union x1 x0).
apply heap.equal_trans with (heap.union x0 x1); auto.
apply heap.union_com; auto.
apply heap.disjoint_com; auto.
apply heap.equal_sym; auto.
apply heap.lookup_union.
apply heap.disjoint_com; auto.
eapply heap.lookup_equal.
apply heap.equal_sym.
apply H6.
rewrite heap.lookup_singleton; auto.
split.

exists x0; exists x1.
split; auto.
split; auto.
split.

apply inde_update_store; auto.
apply inde_mapsto.
simpl.
apply inter_weak.
apply inter_nil.
simpl; red in H; simpl in H; intuition.
simpl.
apply inter_sym.
apply inter_nil.

apply inde_update_store.
apply inde_mapsto.
simpl.
apply inter_weak.
apply inter_nil.
simpl; red in H; simpl in H; intuition.
simpl.
apply inter_sym.
apply inter_nil.

exists x2; auto.
split; simpl.
elim store.lookup_update.
auto.
red in H; simpl in H; intuition.
rewrite store.lookup_update'; auto.

apply semax_assign_var_lookup.

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

apply semax_seq with (
fun s h =>
     ((var_e x |-> int_e b) ** (var_e y |-> int_e b)) s h /\
     eval (var_e z) s = a /\ eval (var_e v) s = b
).

(* We split to handle the third instruction *)

apply semax_strengthen_pre with (
update_heap2 (var_e x) (var_e v)
(fun s h =>
     ((var_e x |-> int_e b) ** (var_e y |-> int_e b)) s h /\
     eval (var_e z) s = a /\ eval (var_e v) s = b)
).

red; intros.
red.
decompose [and] H0; clear H0.
simpl.
inversion_clear H1.
inversion_clear H0.
decompose [and] H1; clear H1.
inversion_clear H2.
inversion_clear H1.
exists x2.
split; auto.
exists a.
split.
apply heap.lookup_equal with (heap.union x0 x1).
apply heap.equal_sym; auto.
apply heap.lookup_union.
auto.
eapply heap.lookup_equal.
apply heap.equal_sym.
apply H6.
rewrite heap.lookup_singleton; auto.
split.
exists (heap.update x2 b x0).
exists x1.
split.
apply heap.disjoint_update.
auto.
split.
simpl in H4.
rewrite H4.
apply heap.equal_update_L.
auto.
auto.
apply heap.lookup_In with a.
eapply heap.lookup_equal.
apply heap.equal_sym.
apply H6.
apply heap.lookup_singleton.
split; auto.
exists x2; split; auto.
simpl.
simpl in H6.
apply heap.equal_trans with (heap.update x2 b (heap.singleton x2 a)).
apply heap.equal_update.
auto.
apply heap.update_singleton.
auto.
apply semax_assign_lookup_expr.

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

(* We handle the last instruction *)

apply semax_strengthen_pre with (
update_heap2 (var_e y) (var_e z)
(fun s h =>
     ((var_e x |-> int_e b) ** (var_e y |-> int_e a)) s h /\
     eval (var_e z) s = a /\ eval (var_e v) s = b)
).

red; intros.
red.
decompose [and] H0; clear H0.
inversion_clear H1.
inversion_clear H0.
decompose [and] H1; clear H1.
inversion_clear H7.
inversion_clear H1.
exists x2; split; auto.
exists b; split.
apply heap.lookup_equal with (heap.union x1 x0).
apply heap.equal_trans with (heap.union x0 x1); auto.
apply heap.union_com.
apply heap.disjoint_com; auto.
apply heap.equal_sym; auto.
apply heap.lookup_union.
apply heap.disjoint_com; auto.
eapply heap.lookup_equal.
apply heap.equal_sym.
apply H7.
simpl.
rewrite heap.lookup_singleton; auto.
split.
simpl.
simpl in H3.
rewrite H3.
exists x0.
exists (heap.update x2 a x1); split; auto.
apply heap.disjoint_com.
apply heap.disjoint_update.
apply heap.disjoint_com; auto.
split.
apply heap.equal_trans with (heap.union (heap.update x2 a x1) x0).
apply heap.equal_update_L.
apply heap.disjoint_com; auto.
apply heap.equal_trans with (heap.union x0 x1); auto.
apply heap.union_com.
auto.
apply heap.lookup_In with b.
eapply heap.lookup_equal.
apply heap.equal_sym.
apply H7.
rewrite heap.lookup_singleton; auto.
apply heap.union_com.
apply heap.disjoint_update.
apply heap.disjoint_com; auto.
split; auto.
exists x2; split; auto.
simpl.
simpl in H7.
apply heap.equal_trans with (heap.update x2 a (heap.singleton x2 b)).
apply heap.equal_update.
auto.
apply heap.update_singleton.
auto.

apply semax_weaken_post with (
(fun s h =>
((var_e x |-> int_e b) ** (var_e y |-> int_e a)) s h /\
eval (var_e z) s = a /\ eval (var_e v) s = b)
).

red; intros.
intuition.

apply semax_assign_lookup_expr.

Qed.

Open Local Scope vc_scope.

Lemma vc_swap: forall x y z v a b, (var.set (x::y::z::v::nil)) ->
  {{ ((var_e x) |-> (int_e a)) ** ((var_e y) |-> (int_e b)) }}
  (proj_cmd
    (z <-*(var_e x) ; 
      v <-* (var_e y) ;
      ((var_e x) *<- (var_e v)) ;
      ((var_e y) *<- (var_e z)))
  )
  {{ ((var_e x) |-> (int_e b)) ** ((var_e y) |-> (int_e a)) }}.
intros.
apply wp_vc_util.
(* vc *)
intros.
simpl.
unfold TT.
intuition.
(* wp *)
intros.
simpl.
exists (int_e a).

generalize H0; clear H0.
apply sep.monotony.
split.
auto.
intros.

generalize H0; clear H0.
apply sep.adjunction.
intros.
red.

exists (int_e b).

simpl.

assert (((var_e y |-> int_e b) ** (var_e x |-> int_e a)) 
  (store.update z (eval (int_e a) s) s) h0).
apply inde_update_store.
apply inde_sep_con.
apply inde_mapsto.
simpl.
apply inter_weak.
apply inter_nil.
simpl.
simpl in H; intuition.
apply inter_weak.
apply inter_nil.
simpl.
simpl in H; intuition.
apply inde_mapsto.
simpl.
apply inter_weak.
apply inter_nil.
simpl.
simpl in H; intuition.
apply inter_weak.
apply inter_nil.
simpl.
simpl in H; intuition.
auto.

generalize H1; clear H1.
apply sep.monotony.
split.
auto.
intros.

generalize H1; clear H1.
apply sep.adjunction.
intros.
red.

simpl.
exists (int_e a).

assert (((var_e x |-> int_e a) ** (var_e y |-> int_e b))  (store.update v b (store.update z a s)) h1).
apply inde_update_store.
apply inde_sep_con.
apply inde_mapsto.
simpl.
apply inter_weak.
apply inter_nil.
simpl.
simpl in H; intuition.
apply inter_weak.
apply inter_nil.
simpl.
simpl in H; intuition.
apply inde_mapsto.
simpl.
apply inter_weak.
apply inter_nil.
simpl.
simpl in H; intuition.
apply inter_weak.
apply inter_nil.
simpl.
simpl in H; intuition.
auto.

generalize H2; clear H2.
apply sep.monotony.
split.
auto.
intros.

generalize H2; clear H2.
apply sep.adjunction.
intros.

exists (int_e b).

generalize H2; clear H2.
apply sep.monotony.
split.
auto.
intros.

generalize H2; clear H2.
apply sep.adjunction.
intros.

inversion_clear H2.
inversion_clear H3.
decompose [and] H2; clear H2.
inversion_clear H4.
inversion_clear H2.
exists x0.
inversion_clear H7.
inversion_clear H2.
exists x1.
split; auto.
split; auto.
split.
exists x2.
split; auto.
simpl.
simpl in H6.
apply heap.equal_trans with (heap.singleton x2
         (store.lookup v (store.update v b (store.update z a s)))).
auto.
rewrite store.lookup_update'.
apply heap.equal_refl.
auto.
exists x3.
split; auto.
simpl.
eapply heap.equal_trans.
apply H8.
simpl.
elim store.lookup_update.
rewrite store.lookup_update'.
apply heap.equal_refl.
red in H; simpl in H; intuition.
Qed.

Close Local Scope vc_scope.