Commit 1f013d6c authored by charguer's avatar charguer

cf_credits_ok

parent 2a519c61
......@@ -437,3 +437,167 @@ the type of arguments and return type as well.
*)
(*------------------------------------------------------------------*)
(* ** Lemmas for introduction and elimination of [is_local] *)
(** Weaken and frame and gc property [local] *)
Lemma local_frame_gc : forall (F:formula) H H1 H2 Q1 Q,
is_local F ->
F H1 Q1 ->
H ==> H1 \* H2 ->
Q1 \*+ H2 ===> Q \*+ \GC ->
F H Q.
Proof using.
introv L M WH WQ. rewrite L. introv Ph.
exists H1 H2 Q1. splits~.
Qed.
(** Weakening on pre and post from [local] *)
Lemma local_weaken : forall H' Q' (F:formula) H Q,
is_local F ->
F H' Q' ->
H ==> H' ->
Q' ===> Q ->
F H Q.
Proof using.
intros. eapply local_frame_gc with (H2 := \[]); eauto.
rewrite~ hprop_star_empty_r.
apply* qimpl_gc_instantiate.
Qed.
(** Weakening on pre from [local] *)
Lemma local_weaken_pre : forall H' (F:formula) H Q,
is_local F ->
F H' Q ->
H ==> H' ->
F H Q.
Proof using. intros. apply* local_weaken. Qed.
(** Weakening on post from [local] *)
Lemma local_weaken_post : forall Q' (F:formula) H Q,
is_local F ->
F H Q' ->
Q' ===> Q ->
F H Q.
Proof using. intros. apply* local_weaken. Qed.
(** Garbage collection on precondition from [local] *)
Lemma local_gc_pre : forall H' (F:formula) H Q,
is_local F ->
H ==> H' \* \GC ->
F H' Q ->
F H Q.
Proof using.
introv LF H1 H2. applys~ local_frame_gc H2.
Qed.
(** Variant of the above, useful for tactics to specify
the garbage collected part *)
Lemma local_gc_pre_on : forall HG H' (F:formula) H Q,
is_local F ->
H ==> HG \* H' ->
F H' Q ->
F H Q.
Proof using.
introv L M W. rewrite L. introv Ph.
exists H' HG Q. splits.
{ rewrite hprop_star_comm. apply~ M. }
{ auto. }
{ apply* qimpl_gc_instantiate. }
Qed.
(** Garbage collection on post-condition from [local] *)
Lemma local_gc_post : forall Q' (F:formula) H Q,
is_local F ->
F H Q' ->
Q' ===> Q \*+ \GC ->
F H Q.
Proof using.
introv L M W. rewrite L. introv Ph.
exists H \[] Q'. splits~.
{ rewrite~ hprop_star_empty_r. }
{ intros x. rewrite~ hprop_star_empty_r. }
Qed.
(** Extraction of pure facts from [local] *)
Lemma local_extract_prop : forall (F:formula) H (P:Prop) Q,
is_local F ->
(P -> F H Q) ->
F (\[P] \* H) Q.
Proof using.
introv L M. rewrite L. introv (h1&h2&(PH1&HP)&PH2&H1&H2).
lets: hprop_empty_inv HP. subst h1. rew_state. subst h2.
exists H \[] Q. splits~.
{ rewrite~ hprop_star_empty_r. }
{ apply* qimpl_gc_instantiate. }
Qed.
(** Extraction of existentials from [local] *)
Lemma local_extract_exists : forall (F:formula) A (J:A->hprop) Q,
is_local F ->
(forall x, F (J x) Q) ->
F (hprop_exists J) Q.
Proof using.
introv L M. rewrite L. introv (x&Hx).
exists (J x) \[] Q. splits~.
{ rewrite~ hprop_star_empty_r. }
{ apply* qimpl_gc_instantiate. }
Qed.
Lemma qimpl_gc_instantiate : forall (Q Q':val->hprop) (H:hprop),
Q ===> Q' ->
Q \*+ H ===> Q' \*+ \GC.
Proof using.
introv IQ. intros x h (ha&hb&Ha&Hb&Dab&Eab).
exists ha hb. splits~.
{ applys~ IQ. }
{ applys hprop_gc_prove. }
Qed.
Lemma rule_consequence_frame : forall H2 H1 Q1 t H Q,
H ==> H1 \* H2 ->
triple t H1 Q1 ->
Q1 \*+ H2 ===> Q ->
triple t H Q.
Proof using.
introv HH Ht HQ. applys rule_consequence HH HQ. applys* rule_frame Ht.
Qed.
(********************************************************************)
(* ** Preliminaries *)
(*------------------------------------------------------------------*)
(** Derived lemmas for heap entailment and structural rules. *)
Lemma himpl_trans_star : forall (H1' H1 H2 H3:hprop),
H1 ==> H1' ->
H1' \* H2 ==> H3 ->
H1 \* H2 ==> H3.
Proof using.
introv M N. intros h (ha&hb&Ha&Hb&Dab&Eab).
applys N. lets Ha': M Ha. exists ha hb. splits~.
Qed.
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* ** * Rules without GC, low-level proof *)
Implicit Types H : hprop.
(*------------------------------------------------------------------*)
(* ** Definition of triples *)
Definition triple t H Q :=
forall h1 h2,
\# h1 h2 ->
H h1 ->
exists h1' v,
\# h1' h2
/\ red (h1 \u h2) t (h1' \u h2) v
/\ Q v h1'.
(*------------------------------------------------------------------*)
(* ** Structural rules *)
Lemma rule_extract_exists : forall t A (J:A->hprop) Q,
(forall x, triple t (J x) Q) ->
triple t (hprop_exists J) Q.
Proof using. introv M D (x&Jx). applys* M. Qed.
Lemma rule_extract_prop : forall t (P:Prop) H Q,
(P -> triple t H Q) ->
triple t (\[P] \* H) Q.
Proof using.
intros t. applys (rule_extract_prop_from_extract_exists (triple t)).
applys rule_extract_exists.
Qed.
Lemma rule_consequence : forall t H' Q' H Q,
H ==> H' ->
triple t H' Q' ->
Q' ===> Q ->
triple t H Q.
Proof using.
introv MH M MQ. intros h1 h2 D P1.
lets P1': (rm MH) (rm P1).
forwards~ (h1'&v&(N1&N2&N3)): (rm M) h2 (rm P1').
exists h1' v. splits~. applys~ MQ.
Qed.
Lemma rule_frame : forall t H Q H',
triple t H Q ->
triple t (H \* H') (Q \*+ H').
Proof using.
introv M. intros h1 h2 D1 (h1a&h1b&H1a&H1b&D12a&E12).
lets~ (h1'a&v&Da&Ra&Qa): M h1a (h1b \u h2).
subst h1. exists (h1'a \u h1b) v. splits~.
{ state_red. }
{ exists~ h1'a h1b. }
Qed.
(*------------------------------------------------------------------*)
(* ** Term rules *)
Lemma rule_val : forall v H Q,
H ==> Q v ->
triple (trm_val v) H Q.
Proof using.
introv M D H1. exists h1 v. splits~.
{ applys red_val. }
Qed.
Lemma rule_if : forall v t1 t2 H Q,
triple (If v = val_int 0 then t2 else t1) H Q ->
triple (trm_if v t1 t2) H Q.
Proof using.
introv M D H1. forwards (h1'&v'&Da&Ra&Qa): M D H1.
exists h1' v'. splits~.
{ applys~ red_if. }
Qed.
Lemma rule_let : forall x t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple (subst_trm x X t2) (Q1 X) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using.
introv M1 M2. intros h1 h2 D1 H1.
lets (h1'&v1&Da&Ra&Qa): M1 D1 H1.
forwards~ (h1''&v2&Db&Rb&Qb): M2 v1 h1' h2.
exists h1'' v2. splits~.
{ applys red_let Ra. state_red. }
Qed.
Lemma rule_let_val : forall x v1 t2 H Q,
(forall (X:val), X = v1 -> triple (subst_trm x X t2) H Q) ->
triple (trm_let x (trm_val v1) t2) H Q.
Proof using.
introv M. forwards~ M': M.
applys_eq~ (>> rule_let H (fun x => \[x = v1] \* H)) 2.
{ applys rule_val. applys~ himpl_inst_prop. }
{ intros X. applys rule_extract_prop. applys M. }
Qed.
Lemma rule_app : forall f x F V t1 H Q,
F = (val_fix f x t1) ->
triple (subst_trm f F (subst_trm x V t1)) H Q ->
triple (trm_app F V) H Q.
Proof using.
introv EF M. subst F. intros h1 h2 D1 H1.
lets (h1'a&ra&Da&Ra&Qa): M D1 H1.
exists h1'a ra. splits~.
{ applys~ red_app. }
Qed.
Lemma rule_let_fix : forall f x t1 t2 H Q,
(forall (F:val),
(forall X H' Q',
triple (subst_trm f F (subst_trm x X t1)) H' Q' ->
triple (trm_app F X) H' Q') ->
triple (subst_trm f F t2) H Q) ->
triple (trm_let f (trm_val (val_fix f x t1)) t2) H Q.
Proof using.
introv M. applys rule_let_val. intros F EF.
applys (rm M). clears H Q. intros X H Q. applys~ rule_app.
Qed.
Section RulesPrimitiveOps.
Transparent hprop_single.
Lemma rule_ref : forall v,
triple (prim_ref v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using.
intros. intros h1 h2 _ P1.
lets E: hprop_empty_inv P1. subst h1.
forwards~ (l&Dl&Nl): (state_disjoint_new null h2 v).
sets h1': (state_single l v).
exists h1' (val_loc l). splits~.
{ rew_state. applys~ red_ref. }
{ exists l. applys~ himpl_inst_prop (l ~~> v). split~. }
Qed.
Lemma rule_get : forall v l,
triple (prim_get (val_loc l)) (l ~~> v) (fun x => \[x = v] \* (l ~~> v)).
Proof using.
intros. intros h1 h2 D P1. exists h1 v. splits~.
{ applys red_get. destruct P1 as (P1a&P1b). applys~ state_union_single_read. }
{ rewrite hprop_star_pure. split~. }
Qed.
Lemma rule_set : forall w l v,
triple (prim_set (val_pair (val_loc l) w)) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
Proof using.
intros. intros h1 h2 D (P1a&P1b).
sets h1': (state_single l w).
exists h1' val_unit. splits~.
{ applys state_disjoint_single_set v. rewrite~ <- P1a. }
{ rew_state. applys~ red_set. applys~ state_union_single_write v w. }
{ applys~ himpl_inst_prop (l ~~> w). split~. }
Qed.
End RulesPrimitiveOps.
......@@ -6,3 +6,5 @@ ModelSepFunctor
ModelSepBasic
ModelSepCredits
ModelSepRO
ModelCF
ModelCFCredits
\ No newline at end of file
##############################################################################
# CFML setup.
......@@ -11,7 +12,9 @@ include $(CFML)/Makefile.common
# The official list of files that should be compiled by [make]
# and included in the archive by [make export].
SRC := $(shell grep -v -e "^ *#" FILES)
# SRC := $(shell grep -v -e "^ *#" FILES)
SRC := ModelState ModelLambda ModelSepFunctor ModelSepBasic ModelSepCredits ModelSepRO ModelCF ModelCFCredits
PWD := $(shell pwd)
......
This diff is collapsed.
(********************************************************************)
(* ** Completeness proof *)
(* TO BE COMPLETED *)
(*
Section Completeness.
Ltac simpl_Trm :=
match goal with E: _ = trm_of_Trm ?T |- _ => destruct T; inverts E end.
Hint Resolve cf_local.
Lemma local_name : forall F (H:hprop) (Q:val->hprop),
is_local F ->
(forall m, H m -> F (= m) Q) ->
F H Q.
Proof.
introv L M. rewrite L. intros m Hm.
exists (= m) \[] Q. splits~.
{ exists~ m state_empty. }
{ intros h. applys himpl_cancel_r. intros h' Hh'. applys~ hprop_gc_prove. }
Qed.
Lemma cf_name : forall T (H:hprop) (Q:val->hprop),
(forall m, H m -> cf T (= m) Q) ->
cf T H Q.
Proof. intros. apply~ local_name. Qed.
Definition spost (m:state) (v:val) :=
fun x => \[x = v] \* (= m).
Fixpoint Trm_of_trm (t : trm) : Trm :=
let aux := Trm_of_trm in
match t with
| trm_val v => Trm_val v
| trm_if v t1 t2 => Trm_if v (aux t1) (aux t2)
| trm_let x t1 t2 => Trm_let x (aux t1) (aux t2)
| trm_app v1 v2 => Trm_app v1 v2
end.
Axiom trm_of_Trm_on_Trm_of_trm : forall t,
trm_of_Trm (Trm_of_trm t) = t.
Axiom trm_of_Trm_on_subst_Trm : forall f v T,
trm_of_Trm (subst_Trm f v T) = subst_trm f v (trm_of_Trm T).
Hint Rewrite trm_of_Trm_on_Trm_of_trm trm_of_Trm_on_subst_Trm : simpl_tr.
Tactic Notation "simpl_tr" := autorewrite with simpl_tr.
Tactic Notation "simpl_tr" "~" := simpl_tr; auto_tilde.
Lemma rule_conseq_frame : forall H'' t H' Q' H Q,
H ==> H' \* H'' ->
triple t H' Q' ->
Q' \*+ H'' ===> Q ->
triple t H Q.
Proof using. intros. applys* rule_consequence. applys* rule_frame. Qed.
Theorem cf_complete_wrt_semantics : forall (T:Trm) m m' v',
red m T m' v' -> (cf T) (= m) (spost m' v').
Proof using.
introv H. gen_eq t: (trm_of_Trm T); gen T; induction H; intros T E.
{ simpl_Trm. simpl_cf. applys local_erase. hnf.
intros m' E. subst. exists~ (state_empty:state) m. }
{ simpl_Trm. simpl_cf. applys local_erase. hnf.
case_if; applys~ IHred. }
{ simpl_Trm.
{ simpl_cf. applys local_erase. hnf.
exists (spost m2 v1). split.
{ applys~ IHred1. }
{ intros X. unfold spost. applys~ local_extract_prop.
intros E. subst. applys~ IHred2. rewrite~ subst_trm_of_Trm. } }
{ simpl_cf. applys local_erase. hnf.
intros F HF. inverts H. clear IHred1.
rename v into f, v0 into x.
specializes IHred2
(subst_Trm f (val_fix f x (trm_of_Trm T1)) T2) __. { simpl_tr~. }
(* specializes HF (val_fix f x (trm_of_Trm T1)). *)
skip E: (F = (val_fix f x (trm_of_Trm T1))). (* from CF extended *)
rewrite <- E in *. applys IHred2.
} }
{ simpl_Trm. simpl_cf. applys local_erase. unfold cf_app, app.
sets U: (subst_Trm f (val_fix f x t) (subst_Trm x v0 (Trm_of_trm t))).
applys* rule_app. applys_eq (>> cf_sound U) 3.
{ applys IHred. unfold U. simpl_tr~. }
{ unfold U. subst v. simpl_tr~. } }
{ simpl_Trm. simpl_cf. apply local_erase. unfolds. unfolds.
lets: rule_new. applys rule_conseq_frame (= ma) \[].
{ admit. }
{ applys rule_new. }
{ intros r. unfold spost. subst mb.
Transparent hprop_single. unfold hprop_single. admit. }
{ admit. }
{ admit. }
Qed.
End Completeness.
*)
This diff is collapsed.
This diff is collapsed.
......@@ -24,7 +24,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import ModelLambda ModelSepFunctor.
Require Export ModelLambda ModelSepFunctor.
Open Scope state_scope.
......@@ -401,7 +401,7 @@ End SepCreditsCore.
(********************************************************************)
(* * Properties of the logic *)
Module Import SepCreditsSetup := SepLogicSetup SepCreditsCore.
Module Export SepCreditsSetup := SepLogicSetup SepCreditsCore.
(*------------------------------------------------------------------*)
......@@ -701,8 +701,57 @@ Qed.
End RulesPrimitiveOps.
(********************************************************************)
(* * Bonus *)
(*------------------------------------------------------------------*)
(* ** Alternative, higher-level definition of triples *)
Definition triple'' t H Q :=
forall H' h,
(H \* H') h ->
exists n h' v,
red n (h^s) t (h'^s) v
/\ (Q v \* \GC \* H') h'
/\ (h^c = n + h'^c)%nat.
Lemma triple_eq_triple'' : triple = triple''.
Proof using.
applys prop_ext_3. intros t H Q.
unfold triple, triple''. iff M.
{ introv P1. forwards (n&m'&c'&v&R1&R2&R3): M H' (h^s) (h^c).
{ applys_eq P1 1. applys~ heap_eq. }
exists n (m',c') v. splits~. }
{ introv P1. forwards~ (n&h'&v&R1&R2&R3): M H' (m,c).
exists n (h'^s) (h'^c) v. splits~.
applys_eq R2 1. applys~ heap_eq. }
Qed.
(*------------------------------------------------------------------*)
(* ** Triples satisfy the [local] predicate *)
Lemma is_local_triple : forall t,
is_local (triple t).
Proof using.
intros. rewrite triple_eq_triple''.
applys prop_ext_2. intros H Q. iff M.
{ intros h Hh. forwards (h'&v&N1&N2): M \[] h.
{ hhsimpl. }
exists H \[] Q. splits~. { hhsimpl. } { hsimpl. } }
{ intros H' h Hh. lets (h1&h2&N1&N2&N3&N4): Hh. hnf in M.
lets (H1&H2&Q1&R1&R2&R3): M N1.
forwards (n&h'&v&S1&S2&S3): R2 (H2\*H') h.
{ subst h. rewrite <- hprop_star_assoc. exists~ h1 h2. }
exists n h' v. splits~. rewrite <- hprop_gc_merge.
applys himpl_forward S2.
hchange (R3 v). rew_heap.
rewrite (hprop_star_comm_assoc \GC H'). hsimpl. }
Qed.
(*------------------------------------------------------------------*)
(* ** Alternative, low-level definition of triples *)
(* ** Alternative, lower-level definition of triples *)
Definition triple' t H Q :=
forall m1 c1 m2,
......
......@@ -8,7 +8,6 @@ as described in Arthur Charguéraud's lecture notes.
Set Implicit Arguments.
Require Import LibCore ModelLambda ModelSepFunctor ModelSepBasic.
Import SepBasicSetup.
Import TripleWithGCAndLifting.
Open Scope heap_scope.
Ltac auto_star ::= jauto.
......
......@@ -1596,11 +1596,12 @@ Qed.
(** Weakening under a [local] modifier *)
Lemma local_weaken_body : forall (B:Type) (F F':~~B),
(forall H Q, F H Q -> F' H Q) ->
F ===> F' ->
local F ===> local F'.
Proof using.
introv M. intros H Q N. introv Hh.
destruct (N _ Hh) as (H1&H2&Q1&P1&P2&P3). exists___*.
introv M. intros H Q N. introv Hh.
destruct (N _ Hh) as (H1&H2&Q1&P1&P2&P3).
specializes M H1 Q1. exists___*.
Qed.
......
This diff is collapsed.
......@@ -16,7 +16,7 @@ License: MIT.
*)
Set Implicit Arguments.
Require Import ModelLambda ModelSepFunctor.
Require Export ModelLambda ModelSepFunctor.
Open Scope state_scope.
Implicit Arguments exist [A P].
......@@ -562,7 +562,7 @@ End SepROCore.
(********************************************************************)
(* * Properties of the logic *)
Module Import SepROSetup := SepLogicSetup SepROCore.
Module Export SepROSetup := SepLogicSetup SepROCore.
(*------------------------------------------------------------------*)
......
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