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

(* the fields of the cell structure *)

Definition data := 0%Z.
Definition next := 1%Z.

(* a tactic unfolding fields name to their offset *)
Ltac Unfolds_fields :=
  unfold data; unfold next.

(* the reverse list algorithm *)
Definition reverse_list (i j k:var.v):=
    (j <- (nat_e 0));
    while ((var_e i) =/= (nat_e 0)) (
       
       (k <-* (i -.> next));
       ((i -.> next) *<- (var_e j));
       (j <- (var_e i));
       (i <- (var_e k))

    ).

(* this assertion represents the fact that a list begin at an adress *)
Inductive list_assert : list Z -> nat -> nat ->  store.s -> heap.h -> Prop :=
     list_end : forall i j l s h,
                      sep.emp s h ->
                      i = j ->
                      l = nil ->
                      list_assert l i j s h
    | list_suiv: forall l l' d i j k s h h1 h2,
                      h1 # h2 ->
                      h === h1 +++ h2 ->
                      i <> k ->
                      i <> j ->
                      l = d::l' ->
                      ((nat_e i) |--> ((int_e d)::(nat_e j)::nil)) s h1 ->
                      (list_assert l' j k) s h2 ->
                      list_assert l i k s h.

Definition list_empty : list Z := nil.

(* A list reversion of coq list *)
Fixpoint list_reverse_coq (l : list Z) : list Z :=
   match l with
     nil => nil
     | a :: l' => (list_reverse_coq l') ++ a::nil 
   end.

Eval compute in (list_reverse_coq (3%Z::6%Z::8%Z::1%Z::8%Z::9%Z::13%Z::nil)).

Lemma list_reverse_coq_lemma1: forall l a,
                   list_reverse_coq (l ++ a::nil) = a:: (list_reverse_coq l).
induction l.
simpl.
auto.
intros.
simpl.
rewrite IHl.
simpl.
auto.
Qed.

Lemma list_reverse_coq_lemma2: forall l,
                   list_reverse_coq (list_reverse_coq l) = l.
induction l.
simpl; auto.
simpl.
rewrite list_reverse_coq_lemma1.
rewrite IHl.
auto.
Qed.

Lemma list_assert_inde_store: forall l i j s1 s2 h,
   list_assert l i j s1 h -> list_assert l i j s2 h.
intros.
induction H.
eapply list_end.
auto.
auto.
auto.
eapply list_suiv with (h1 := h1) (h2 := h2) (d := d) (j := j).
auto.
auto.
auto.
intuition.
apply H3.
auto.
auto.
Qed.


(* precondition and postcondition of reverse_list *)
Definition reverse_precondition (l: list Z) (hd: var.v) : assert := 
( fun s => fun h => exists v, (eval (var_e hd) s = Z_of_nat v) /\ (list_assert l v  0) s h).

Definition reverse_postcondition (l: list Z) (hd: var.v) : assert := 
( fun s => fun h => exists v, (eval (var_e hd) s = Z_of_nat v) /\ (list_assert (list_reverse_coq l) v 0) s h).


(* reverse_list specification *)
Definition reverse_list_specif: Prop := forall l i j k,
                  var.set (i::j::k::nil) ->
                  {{reverse_precondition l i}}
                  reverse_list i j k
                  {{reverse_postcondition l j}}.


Lemma list_assert_hd_uneq: forall l1 l2 hd1 hd2 s h,
   ((list_assert l1 hd1 0) ** (list_assert l2 hd2 0)) s h ->
   hd1 <> 0 ->
   hd1 <> hd2.
intros.
Decompose_sepcon H h1 h2.
inversion_clear H1.
intuition.
inversion_clear H4.
intuition.
simpl in H9.
Decompose_sepcon H9 h31 h32.
simpl in H15.
Decompose_sepcon H15 h51 h52.
red in H18.
red in H9.
inversion_clear H9.
inversion_clear H21.
inversion_clear H18.
inversion_clear H21.
simpl in H9.
rewrite Z_of_nat2loc in H9.
simpl in H18.
rewrite Z_of_nat2loc in H18.
injection H9; injection H18; intros.
subst x0 x.
simpl in H24; simpl in H23.
eapply heap.disjoint_singleton' with (z := d) (z' := d0).
eapply heap.disjoint_equal with h51.
eapply heap.disjoint_com.
eapply heap.disjoint_equal with h31.
Disjoint_heap.
Equal_heap.
Equal_heap.
intuition.
intuition.
Qed.

Lemma list_assert_heap_equal: forall l startl s h1 h2, h1 === h2 ->
    list_assert l startl 0 s h1 -> list_assert l startl 0 s h2.
induction l.
intros.
inversion_clear H0.
eapply list_end.
red in H1.
red.
Equal_heap.
auto.
auto.
inversion H5.
intros.
inversion_clear H0.
inversion H3.
injection H5; intros; subst d l'.
clear H5.
simpl in H6.
Decompose_sepcon H6 h01 h02.
Decompose_sepcon H9 h021 h022.
red in H12.
eapply list_suiv with (h1 := h01 +++ h021) (h2 := h3).
Disjoint_heap.
apply heap.equal_trans with h1.
Equal_heap.
Equal_heap.
auto.
apply H4.
intuition.
simpl.
Compose_sepcon h01 h021.
Mapsto_equiv.
Compose_sepcon h021 heap.emp.
Mapsto_equiv.
red; apply heap.equal_refl.
eapply IHl.
apply heap.equal_refl.
auto.
Qed.


(* reverse_list verification *)
Lemma reverse_list_verif: reverse_list_specif.
unfold reverse_list_specif.
intros.
unfold reverse_list.
unfold reverse_precondition.
unfold reverse_postcondition.

eapply semax_assign_var_e'' with ( fun s => fun h => 
exists v, 
   (eval (var_e i) s = Z_of_nat v) /\ 
   (list_assert l v 0) s h /\
   (eval (var_e j) s = Z_of_nat 0)
).

simpl; red; intros.
inversion_clear H0.
inversion_clear H1.
exists x.
split.
Resolve_simpl_store_update.
split.
eapply list_assert_inde_store; apply H2.
Resolve_simpl_store_update.

apply semax_while' with (fun s => fun h =>
exists l1, exists l2,
    l = l1 ++ l2 /\
    (exists v_i, exists v_j,
        eval (var_e i) s = Z_of_nat v_i /\
        eval (var_e j) s = Z_of_nat v_j /\
        ((list_assert l2 v_i  0) ** (list_assert (list_reverse_coq l1) v_j 0)) s h
    )
).

simpl; red; intros.
inversion_clear H0.
decompose [and] H1; clear H1.
exists list_empty; unfold list_empty.
exists l.
simpl; split; auto.
exists x; exists 0.
split; auto.
split; auto.
Compose_sepcon h heap.emp.
auto.
eapply list_end.
red; apply heap.equal_refl.
auto.
auto.

apply semax_strengthen_pre with (fun s => fun h =>
exists l1, exists l2, exists elt,
    l = l1 ++ (elt::l2) /\
    (exists v_i, exists v_j,
        eval (var_e i) s = Z_of_nat v_i /\
        eval (var_e j) s = Z_of_nat v_j /\
        v_i <> 0 /\ 
        v_i <> v_j /\
        ((list_assert (elt::l2) v_i 0) ** (list_assert (list_reverse_coq l1) v_j 0)) s h
    )
).

simpl; red; intros.
inversion_clear H0.
inversion_clear H1 as [l1].
inversion_clear H0 as [l2].
inversion_clear H1.
inversion_clear H3 as [v_i].
inversion_clear H1 as [v_j].
decompose [and] H3; clear H3.
generalize (negb_true_is_false _ H2); clear H2; intros.
generalize (Zeq_bool_false (store.lookup i s) 0); intro X; inversion_clear X.
generalize (H3 H2); clear H3 H4 H2; intros.
assert (A1: v_i <> 0).
rewrite H1 in H2.
intuition.
generalize (list_assert_hd_uneq _ _ _ _ s h H6 A1); clear A1; intro A1.
Decompose_sepcon H6 h1 h2.
inversion_clear H4.
subst v_i.
rewrite H1 in H2.
intuition.
clear H2.
subst l2.
exists l1; exists l'; exists d.
split; auto.
exists v_i; exists v_j.
split; auto.
split; auto.
split; auto.
split.
auto.
Compose_sepcon h1 h2.
eapply list_suiv.
apply H7.
auto.
auto.
apply H11.
intuition.
apply H13.
auto.
auto.

apply semax_assign_var_lookup_backwards'' with (fun s => fun h =>
exists l1, exists l2, exists elt,
    l = l1 ++ (elt::l2) /\
    (exists v_i, exists v_j, exists v_k,
        eval (var_e i) s = Z_of_nat v_i /\
        eval (var_e j) s = Z_of_nat v_j /\
        eval (var_e k) s = Z_of_nat v_k /\
        v_i <> 0 /\ 
        v_i <> v_j /\ 
        ((list_assert (elt::nil) v_i  v_k) ** (list_assert (l2) v_k  0) ** (list_assert (list_reverse_coq l1) v_j 0)) s h
    )
).
simpl; red; intros.
inversion_clear H0 as [l1].
inversion_clear H1 as [l2].
inversion_clear H0 as [elt].
inversion_clear H1.
inversion_clear H2 as [v_i].
inversion_clear H1 as [v_j].
decompose [and] H2; clear H2.
Decompose_sepcon H7 h1 h2.
inversion_clear H6.
contradiction.
injection H13; intros; clear H13; subst d l'.
simpl in H14.
Decompose_sepcon H14 h31 h32.
Decompose_sepcon H17 h321 h322.
red in H20.
exists (nat_e j0).
Compose_sepcon h321 (h31 +++ h4 +++ h2).
unfold next.
Mapsto_equiv.
Intro_sepimp h321' h'.
red.
exists l1; exists l2; exists elt.
split; auto.
exists v_i; exists v_j; exists j0.
split.
Resolve_simpl_store_update.
split.
Resolve_simpl_store_update.
split.
Resolve_simpl_store_update.
split; auto.
split; auto.
Compose_sepcon (h321' +++ h31 +++ h4) h2.
Compose_sepcon (h321' +++ h31) h4.
apply list_assert_inde_store with s.
eapply list_suiv with (h1 := (h321' +++ h31)) (h2 := heap.emp).
Disjoint_heap.
Equal_heap.
auto.
apply H12.
intuition.
simpl.
Compose_sepcon h31 h321'.
Mapsto_equiv.
Compose_sepcon h321' heap.emp.
Mapsto_equiv.
rewrite H1; unfold next; auto.
red; eapply heap.equal_refl.
eapply list_end.
red; eapply heap.equal_refl.
auto.
auto.
apply list_assert_inde_store with s.
auto.
apply list_assert_inde_store with s.
auto.

apply semax_assign_lookup_expr_backwards'' with (fun s => fun h =>
exists l1, exists l2, exists elt,
    l = l1 ++ (elt::l2) /\
    (exists v_i, exists v_k,
        eval (var_e i) s = Z_of_nat v_i /\
        eval (var_e k) s = Z_of_nat v_k /\
        v_i <> 0 /\ 
        ((list_assert (list_reverse_coq (l1 ++ elt ::nil)) v_i  0) ** (list_assert (l2) v_k  0)) s h
    )
).
simpl; red; intros.
inversion_clear H0 as [l1].
inversion_clear H1 as [l2].
inversion_clear H0 as [elt].
inversion_clear H1.
inversion_clear H2 as [v_i].
inversion_clear H1 as [v_j].
inversion_clear H2 as [v_k].
decompose [and] H1; clear H1.
Decompose_sepcon H8 h1 h2.
Decompose_sepcon H7 h11 h12.
inversion_clear H9.
inversion H15.
injection H17; intros; subst d l'; clear H17.
inversion_clear H19.
clear H20; subst j0; red in H9.
simpl in H18.
Decompose_sepcon H18 h31 h32.
Decompose_sepcon H21 h321 h322.
red in H24.
unfold next.
exists (nat_e v_k).
Compose_sepcon h321 (h31 +++ h4 +++ h12 +++ h2).
Mapsto_equiv.
Intro_sepimp h321' h'.
exists l1; exists l2; exists elt.
split; auto.
exists v_i; exists v_k.
split; auto.
split; auto.
split; auto.
rewrite list_reverse_coq_lemma1.
Compose_sepcon (h31 +++ h321' +++ h2) h12.
eapply list_suiv with (h1 := h31 +++ h321') (h2 := h2).
Disjoint_heap.
Equal_heap.
auto.
apply H6.
intuition.
simpl.
Compose_sepcon h31 h321'.
Mapsto_equiv.
Compose_sepcon h321' heap.emp.
Mapsto_equiv.
red; eapply heap.equal_refl.
auto.
auto.
inversion H22.

apply semax_assign_var_e'' with (fun s => fun h =>
exists l1, exists l2, exists elt,
    l = l1 ++ (elt::l2) /\
    (exists v_j, exists v_k,
        eval (var_e j) s = Z_of_nat v_j /\
        eval (var_e k) s = Z_of_nat v_k /\
        ((list_assert (list_reverse_coq (l1 ++ elt ::nil)) v_j  0) ** (list_assert (l2) v_k  0)) s h
    )
).
simpl; red; intros.
inversion_clear H0 as [l1].
inversion_clear H1 as [l2].
inversion_clear H0 as [elt].
inversion_clear H1.
inversion_clear H2 as [v_i].
inversion_clear H1 as [v_k].
decompose [and] H2; clear H2.
red.
exists l1; exists l2; exists elt.
split; auto.
exists v_i; exists v_k.
split.
Resolve_simpl_store_update.
split.
Resolve_simpl_store_update.
Resolve_simpl_store_update.
apply list_assert_inde_store with s0.
auto.
apply list_assert_inde_store with s0.
auto.


apply semax_assign_var_e'.
red; simpl.
intros.
inversion_clear H0 as [l1].
inversion_clear H1 as [l2].
inversion_clear H0 as [elt].
inversion_clear H1.
inversion_clear H2 as [v_j].
inversion_clear H1 as [v_k].
decompose [and] H2; clear H2.
exists (l1 ++ elt::nil); exists l2. 
split.
rewrite app_ass; simpl; auto.
exists v_k; exists v_j.
split.
Resolve_simpl_store_update.
split.
Resolve_simpl_store_update.
Decompose_sepcon H5 h1 h2.
Compose_sepcon h2 h1.
apply list_assert_inde_store with s.
auto.
apply list_assert_inde_store with s.
auto.

simpl; red; intros.
inversion_clear H0.
inversion_clear H1 as [l1].
inversion_clear H0 as [l2].
inversion_clear H1.
inversion_clear H3 as [v_i].
inversion_clear H1 as [v_j].
decompose [and] H3; clear H3.
exists v_j.
generalize (negb_false_is_true _ H2); clear H2; intros.
rewrite (Zeq_bool_true _ _ H2) in H1.
split.
auto.
Decompose_sepcon H6 h1 h2.
assert (0%Z = Z_of_nat 0).
auto.
rewrite H7 in H1.
rewrite <- (Z_of_nat_inj _ _ H1) in H4.
inversion_clear H4.
red in H9.
subst l2.
rewrite <- app_nil_end in H0; subst l1.
eapply list_assert_heap_equal with h2.
Equal_heap.
auto.
intuition.
Qed.