Commit c84f4f71 authored by charguer's avatar charguer

frame_ro

parent b526fc67
......@@ -2,6 +2,47 @@ Set Implicit Arguments.
Require Import LibCore Shared ModelLambda.
Open Scope state_scope.
(*------------------------------------------------------------------*)
(** Big-step evaluation with counting of the number of beta reductions
(used by the formalization of Separation Logic with time credits) *)
Section Redn.
Local Open Scope nat_scope.
Local Open Scope state_scope.
Inductive redn : nat -> state -> trm -> state -> val -> Prop :=
| redn_val : forall m v,
redn 0 m (trm_val v) m v
| redn_if : forall n m1 m2 v r t1 t2,
redn n m1 (If v = val_int 0 then t2 else t1) m2 r ->
redn n m1 (trm_if v t1 t2) m2 r
| redn_let : forall n1 n2 m1 m2 m3 x t1 t2 v1 r,
redn n1 m1 t1 m2 v1 ->
redn n2 m2 (subst_trm x v1 t2) m3 r ->
redn (n1+n2) m1 (trm_let x t1 t2) m3 r
| redn_app : forall n m1 m2 v1 v2 f x t r,
v1 = val_fix f x t ->
redn n m1 (subst_trm f v1 (subst_trm x v2 t)) m2 r ->
redn (S n) m1 (trm_app v1 v2) m2 r
| redn_new : forall ma mb v l,
mb = (state_single l v) ->
\# ma mb ->
redn 0 ma (trm_new v) (mb \+ ma) (val_loc l)
| redn_get : forall ma mb l v,
ma = (state_single l v) ->
\# ma mb ->
redn 0 (ma \+ mb) (trm_get (val_loc l)) (ma \+ mb) v
| redn_set : forall ma1 ma2 mb l v1 v2,
ma1 = (state_single l v1) ->
ma2 = (state_single l v2) ->
\# ma1 mb ->
redn 0 (ma1 \+ mb) (trm_set (val_loc l) v2) (ma2 \+ mb) val_unit.
End Redn.
(*------------------------------------------------------------------*)
(** Predicate over pairs *)
......
......@@ -169,6 +169,12 @@ Next Obligation.
exists (l::nil). intros. case_if. subst~.
Qed.
(** Update of a state *)
Definition state_update (h:state) (l:loc) (v:val) :=
state_union (state_single l v) h.
(* Note: the union operation first reads in the first argument. *)
End State.
......@@ -214,58 +220,15 @@ Inductive red : state -> trm -> state -> val -> Prop :=
mb = (state_single l v) ->
\# ma mb ->
red ma (trm_new v) (mb \+ ma) (val_loc l)
| red_get : forall ma mb l v,
ma = (state_single l v) ->
\# ma mb ->
red (ma \+ mb) (trm_get (val_loc l)) (ma \+ mb) v
| red_set : forall ma1 ma2 mb l v1 v2,
ma1 = (state_single l v1) ->
ma2 = (state_single l v2) ->
\# ma1 mb ->
red (ma1 \+ mb) (trm_set (val_loc l) v2) (ma2 \+ mb) val_unit.
End Red.
| red_get : forall m l v,
state_data m l = Some v ->
red m (trm_get (val_loc l)) m v
| red_set : forall m m' l v,
m' = state_update m l v ->
red m (trm_set (val_loc l) v) m' val_unit.
(*------------------------------------------------------------------*)
(** Big-step evaluation with counting of the number of beta reductions
(used by the formalization of Separation Logic with time credits) *)
Section Redn.
Local Open Scope nat_scope.
Local Open Scope state_scope.
Inductive redn : nat -> state -> trm -> state -> val -> Prop :=
| redn_val : forall m v,
redn 0 m (trm_val v) m v
| redn_if : forall n m1 m2 v r t1 t2,
redn n m1 (If v = val_int 0 then t2 else t1) m2 r ->
redn n m1 (trm_if v t1 t2) m2 r
| redn_let : forall n1 n2 m1 m2 m3 x t1 t2 v1 r,
redn n1 m1 t1 m2 v1 ->
redn n2 m2 (subst_trm x v1 t2) m3 r ->
redn (n1+n2) m1 (trm_let x t1 t2) m3 r
| redn_app : forall n m1 m2 v1 v2 f x t r,
v1 = val_fix f x t ->
redn n m1 (subst_trm f v1 (subst_trm x v2 t)) m2 r ->
redn (S n) m1 (trm_app v1 v2) m2 r
| redn_new : forall ma mb v l,
mb = (state_single l v) ->
\# ma mb ->
redn 0 ma (trm_new v) (mb \+ ma) (val_loc l)
| redn_get : forall ma mb l v,
ma = (state_single l v) ->
\# ma mb ->
redn 0 (ma \+ mb) (trm_get (val_loc l)) (ma \+ mb) v
| redn_set : forall ma1 ma2 mb l v1 v2,
ma1 = (state_single l v1) ->
ma2 = (state_single l v2) ->
\# ma1 mb ->
redn 0 (ma1 \+ mb) (trm_set (val_loc l) v2) (ma2 \+ mb) val_unit.
End Redn.
End Red.
Local Open Scope state_scope.
......@@ -360,6 +323,23 @@ Lemma state_disjoint_3_unfold : forall h1 h2 h3,
\# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
Proof using. auto. Qed.
Lemma state_disjoint_new : forall (h:state) v,
exists l, \# (state_single l v) h.
Proof using.
intros (m&(L&M)). unfold state_disjoint, pfun_disjoint. simpl.
lets (l&F): (loc_fresh L).
intros v'. exists l. intros l'. case_if~.
{ right. applys not_not_elim. intros H. applys F. applys~ M. }
Qed.
Lemma state_disjoint_single_set : forall (h:state) l v1 v2,
\# (state_single l v1) h ->
\# (state_single l v2) h.
Proof using.
introv M. unfolds state_disjoint, state_single, pfun_disjoint; simpls.
intros l'. specializes M l'. case_if~. destruct M; auto_false.
Qed.
(** Union *)
Lemma state_union_idempotent : forall h,
......
......@@ -211,7 +211,12 @@ Lemma heap_disjoint_components : forall h,
\# (h^f) (h^r).
Proof using. intros ((f,r)&D). simple~. Qed.
Ltac unstate := unfold heap_state; simpl.
Lemma heap_make : forall f r,
state_disjoint f r -> exists (h:heap), h^f = f /\ h^r = r.
Proof using.
introv M. sets h : ((exist (f,r) M : heap)). exists~ h.
(* TODO: exists direct marche pas *)
Qed.
Lemma heap_eq : forall h1 h2,
(h1^f = h2^f /\ h1^r = h2^r) -> h1 = h2.
......@@ -226,6 +231,8 @@ Proof using.
intros ((f1&r1)&D1) ((f2&r2)&D2) M. inverts~ M.
Qed.
Ltac unstate := unfold heap_state; simpl.
(*------------------------------------------------------------------*)
(* ** Auxiliary function [heap_ro] *)
......@@ -970,6 +977,7 @@ Tactic Notation "state_red" "~" :=
state_red; auto_tilde.
Hint Resolve heap_compat_union_l heap_compat_union_r.
Hint Resolve state_agree_empty_l state_agree_empty_r.
(*------------------------------------------------------------------*)
......@@ -1058,34 +1066,57 @@ Proof using.
Qed.
*)
Lemma rule_frame_read_only : forall t H1 Q1 H2,
triple t (H1 \* RO H2) Q1 ->
normal H2 ->
triple t (H1 \* H2) (Q1 \*+ H2).
Proof using.
Admitted.
(*
introv M N. intros h1 (h11&h12&R1&P11&P12&R2).
introv M N. intros h1 (h11&h12&R1&P11&P12&R2) h2 D.
lets R1': heap_compat_ro_r R1.
lets E12: (rm N) P12.
subst h1. lets~ (D1&D2): heap_compat_union_l_inv (rm D).
asserts R12: (heap_state (heap_ro h12) = heap_state h12).
{ skip. }
(*asserts~ D12: (\# (h12^f) state_empty).
sets_eq h12': (exist (h12^f,state_empty) D12 : heap).*)
forwards (v&h1'&K): (rm M) (h11 \u (heap_ro h12)).
{ unstate. rewrite E12. state_eq. }
asserts C: (heap_compat (h11 \u heap_ro h12) h2).
{ apply~ heap_compat_union_l. applys~ heap_compat_ro_l. }
forwards~ (v&h1'&(N1&N2&N3&N4)): (rm M) (h11 \u (heap_ro h12)) h2.
{ exists h11 (heap_ro h12). splits~.
{ applys~ heap_ro_pred. } }
exists v (h1' \u h12). intros h2 D.
subst h1. lets~ (D1&D2): heap_compat_union_l_inv (rm D).
forwards~ (N1&N2&N3&N4): (rm K) h2.
{ skip. }
splits~.
{ apply~ heap_compat_union_l. skip. (* applys~ heap_compat_ro_l. *) }
{ rew_heap~ in N3. skip. (* state_red~. rewrite~ R12. *) }
skip.
skip.
Qed. (* TODO: more automation for assoc/comm rewrite *)
*)
rew_heap~ in N3. rewrite heap_ro_r in N3. rewrite E12 in N3.
lets G: heap_disjoint_components h1'.
forwards (h1''&F1&F2): (heap_make (h1'^f \+ h12^f) (h11^r)).
{ rewrite N3 in G. state_disjoint. }
asserts C': (heap_compat h1'' h2).
{ unfolds. rewrite F1,F2. split.
{ destruct~ D1. }
{ lets G2: heap_disjoint_components h2. rewrite N3 in G.
state_disjoint. } }
exists v h1''. splits.
{ auto. }
{ state_red~.
{ rewrite~ R12. }
{ fequals. unstate. rewrite F1,F2,N3. state_eq. } }
{ rew_heap~. rewrite F2,E12. state_eq~. }
{ destruct N4 as (f1&f2&G1&G2&G3).
asserts D11: (\# f1 (h12^f)).
{ rewrite G2,N3 in G. state_disjoint. }
asserts D12: (\# f2 (h12^f)).
{ rewrite G2,N3 in G. state_disjoint. }
exists (f1 \+ h12) f2. splits.
{ unstate. rewrite E12. state_disjoint. }
{ unstate. rewrite F1,G2,E12.
do 2 rewrite state_union_assoc. fequals.
rewrite state_union_empty_r. apply~ state_union_comm_disjoint. }
{ sets_eq ha: (exist (f1, state_empty) (on_rw_sub_obligation_1 (Q1 v) h1' f1 f2) : heap).
asserts Ca: (heap_compat ha h12).
{ subst ha. split; simpl. auto. rewrite E12. state_disjoint. }
exists ha h12. splits~.
{ applys heap_eq; simpl. rew_heap~. subst ha; simpl.
unstate. rewrite E12. split; state_eq~. } } }
Qed.
(* LATER: automate disjoint_components use by state_disjoint *)
(*------------------------------------------------------------------*)
(** Term rules *)
......@@ -1214,52 +1245,6 @@ Proof using.
applys rule_app. auto.
Qed.
Lemma heap_make : forall f r,
state_disjoint f r -> exists (h:heap), h^f = f /\ h^r = r.
Proof using.
introv M. sets h : ((exist (f,r) M : heap)). exists~ h.
(* TODO: exists direct marche pas *)
Qed.
Hint Resolve state_agree_empty_l state_agree_empty_r.
Axiom loc_fresh : forall (L : list loc),
exists l, ~ Mem l L.
Lemma state_disjoint_new : forall (h:state) v,
exists l, \# (state_single l v) h.
Proof using.
intros (m&(L&M)). unfold state_disjoint, pfun_disjoint. simpl.
lets (l&F): (loc_fresh L).
intros v'. exists l. intros l'. case_if~.
{ right. applys not_not_elim. intros H. applys F. applys~ M. }
Qed.
Axiom red_get' : forall (m:state) l v,
state_data m l = Some v ->
red m (trm_get (val_loc l)) m v.
Definition state_update m l v :=
state_single l v \+ m. (* Because union reads in left branch first *)
Axiom red_set' : forall m m' l v,
m' = state_update m l v ->
red m (trm_set (val_loc l) v) m' val_unit.
Lemma state_disjoint_single_set : forall (h:state) l v1 v2,
\# (state_single l v1) h ->
\# (state_single l v2) h.
Proof using.
introv M. unfolds state_disjoint, state_single, pfun_disjoint; simpls.
intros l'. specializes M l'. case_if~. destruct M; auto_false.
Qed.
Lemma rule_new : forall v,
triple (trm_new v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using.
......
......@@ -5,6 +5,21 @@ Open Scope state_scope.
Ltac auto_star ::= jauto.
-- TODO: need to update proofs using new definition of red.
(* DEPRECATED ==>
| red_get : forall ma mb l v,
ma = (state_single l v) ->
\# ma mb ->
red (ma \+ mb) (trm_get (val_loc l)) (ma \+ mb) v
| red_set : forall ma1 ma2 mb l v1 v2,
ma1 = (state_single l v1) ->
ma2 = (state_single l v2) ->
\# ma1 mb ->
red (ma1 \+ mb) (trm_set (val_loc l) v2) (ma2 \+ mb) val_unit.
*)
(********************************************************************)
(* ** Heaps *)
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment