Commit f88fbb3f authored by charguer's avatar charguer

functor for RO

parent 20aa3390
......@@ -13,7 +13,8 @@ SRC :=\
ModelLambda \
ModelSepFunctor \
ModelSepBasic \
ModelSepCredits
ModelSepCredits \
ModelSepRO
OTHER :=\
ModelSepRO \
......
......@@ -9,6 +9,10 @@ This file contains:
- a definition of triples,
- statement and proofs of SL reasoning rules.
It also contains triples with heap predicates and post-conditions
lifted so as to specify logical values, which are related to
deeply-embedded values using encoding functions (called encoders).
It also contains an alternative, low-level definition of triples,
and an alternative soundness proof that goes along with it.
......@@ -168,8 +172,8 @@ Qed.
Lemma hprop_star_pure : forall (P:Prop) H h,
(\[P] \* H) h = (P /\ H h).
Proof using.
intros. applys prop_ext. iff (?&?&N&?&?&?) (N1&N2).
{ destruct N. subst. rewrite~ heap_union_empty_l. }
intros. applys prop_ext. iff (h1&h2&P1&P2&D&E) (N1&N2).
{ lets (R&HP): hprop_pure_inv (rm P1). subst. rewrite~ heap_union_empty_l. }
{ exists~ heap_empty h. }
Qed.
......@@ -450,6 +454,174 @@ End TripleWithGC.
(********************************************************************)
(********************************************************************)
(********************************************************************)
(* * Triples with lifting *)
Module TripleWithGCAndLifting.
Import TripleWithGC.
Generalizable Variables A B.
(*------------------------------------------------------------------*)
(* ** Func type *)
Definition func := val.
(*------------------------------------------------------------------*)
(* ** Encoders *)
Class Enc (A:Type) :=
make_Enc { enc : A -> val }.
Instance Enc_loc : Enc loc.
Proof using. constructor. applys val_loc. Defined.
Instance Enc_unit : Enc unit.
Proof using. constructor. applys (fun x:unit => val_unit). Defined.
Instance Enc_int : Enc int.
Proof using. constructor. applys val_int. Defined.
Instance Enc_func : Enc func.
Proof using. constructor. applys (fun x:func => x). Defined.
(*------------------------------------------------------------------*)
(* ** Lifting of operations and predicates *)
Definition hprop_single_enc `{EA:Enc A} r V :=
hprop_single r (enc V).
Notation "r '~~~>' V" := (hprop_single_enc r V)
(at level 32, no associativity) : heap_scope.
Definition PostEnc `{Enc A} (Q:A->hprop) : val->hprop :=
fun v => Hexists V, \[v = enc V] \* Q V.
Definition Triple (t:trm) (H:hprop) `{EA:Enc A} (Q:A->hprop) :=
triple t H (PostEnc Q).
Definition Subst_trm (x:var) `{Enc A} (X:A) (t:trm) : trm :=
subst_trm x (enc X) t.
(*------------------------------------------------------------------*)
(* ** Lifting of rules *)
Lemma Rule_val : forall A `{EA:Enc A} (V:A) v H (Q:A->hprop),
v = enc V ->
H ==> Q V ->
Triple (trm_val v) H Q.
Proof using.
introv E M. applys rule_val.
unfold PostEnc. subst.
applys himpl_inst_exists V.
applys~ himpl_inst_prop.
Qed.
Lemma Rule_if : forall (V:int) v t1 t2 H A `{EA:Enc A} (Q:A->hprop),
v = enc V ->
Triple (If V = 0 then t2 else t1) H Q ->
Triple (trm_if v t1 t2) H Q.
Proof using.
introv E M. applys rule_if. subst.
applys_eq (rm M) 3. tests: (V = 0); simpl; case_if~.
Qed.
Lemma Rule_let : forall x t1 t2 H,
forall A `{EA:Enc A} (Q:A->hprop) A1 `{EA1:Enc A1} (Q1:A1->hprop),
Triple t1 H Q1 ->
(forall (X:A1), Triple (Subst_trm x X t2) (Q1 X) Q) ->
Triple (trm_let x t1 t2) H Q.
Proof using.
introv M1 M2. applys rule_let M1.
intros v. unfold PostEnc.
applys rule_extract_exists. intros V.
applys rule_extract_prop.
introv E. subst. applys M2.
(* TODO: why notation for hprop_exists shows hexists? *)
Qed.
Lemma Rule_let_val_enc : forall A1 `{Enc A1} (V1:A1) x v1 t2 H A `{EA: Enc A} (Q:A->hprop),
v1 = enc V1 ->
(forall X, X = V1 -> Triple (Subst_trm x X t2) H Q) ->
Triple (trm_let x (trm_val v1) t2) H Q.
Proof using.
introv E M. applys rule_let_val. intros X EX. subst. applys~ M.
Qed.
(* Remark:
Lemma Rule_let_val : forall x v1 t2 H A `{EA: Enc A} (Q:A->hprop),
(forall `{Enc A1} (X:A1), v1 = enc X -> Triple (Subst_trm x X t2) H Q) ->
Triple (trm_let x (trm_val v1) t2) H Q.
=> could be proved by exploiting the fact that every value is the encoding of another.
*)
Lemma Rule_app : forall f x (F:func) V t1 H A `{EA:Enc A} (Q:A->hprop),
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. applys* rule_app.
Qed.
Lemma enc_val_fix_eq : forall F f x t1,
F = val_fix f x t1 ->
enc F = F.
Proof using. intros. subst~. Qed.
Lemma Rule_let_fix : forall f x t1 t2 H A `{EA:Enc A} (Q:A->hprop),
(forall (F:func),
(forall `{EA1:Enc A1} `{EA2:Enc A2} (X:A1) H' (Q':A2->hprop),
Triple (Subst_trm f F (Subst_trm x X t1)) H' Q' ->
Triple (trm_app F (enc 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_enc _ _ (val_fix f x t1)).
{ symmetry. applys* enc_val_fix_eq. }
intros F EF. applys (rm M). clears H Q.
intros A2 EA2 A3 EA3 X H Q M.
applys~ Rule_app EF.
Qed.
Lemma Rule_new : forall A `{EA:Enc A} (V:A) v,
v = enc V ->
Triple (prim_new v) \[] (fun l => l ~~~> V).
Proof using.
introv E. applys_eq rule_new 1. subst~.
Qed.
Lemma Rule_get : forall A `{EA:Enc A} (V:A) l,
Triple (prim_get (val_loc l)) (l ~~~> V) (fun x => \[x = V] \* (l ~~~> V)).
Proof using.
introv. applys rule_consequence. { auto. } { applys rule_get. }
{ intros v. unfold PostEnc.
applys himpl_extract_prop. intro_subst.
applys himpl_inst_exists V.
applys~ himpl_inst_prop.
applys~ himpl_inst_prop. }
Qed.
Lemma Rule_set : forall A1 A2 `{EA1:Enc A1} (V1:A1) `{EA2:Enc A2} (V2:A2) l v2,
v2 = enc V2 ->
Triple (prim_set (val_pair (val_loc l) v2)) (l ~~~> V1) (fun (r:unit) => l ~~~> V2).
Proof using.
introv E. applys rule_consequence. { auto. } { applys rule_set. }
{ subst. intros v. unfold PostEnc.
applys himpl_extract_prop. intro_subst.
applys himpl_inst_exists tt.
applys~ himpl_inst_prop. }
Qed.
End TripleWithGCAndLifting.
(********************************************************************)
(********************************************************************)
(********************************************************************)
......@@ -458,6 +630,7 @@ End TripleWithGC.
Module TripleWithoutGC.
Implicit Types H : hprop.
(*------------------------------------------------------------------*)
(* ** Definition of triples *)
......
(* **
(**
This file formalizes "Separation Logic with Time Credits",
following the presentation by Arthur Charguéraud and
......@@ -392,8 +392,8 @@ Qed.
Lemma hprop_star_pure : forall (P:Prop) H h,
(\[P] \* H) h = (P /\ H h).
Proof using.
intros. applys prop_ext. iff (?&?&N&?&?&?) (N1&N2).
{ destruct N. subst. rewrite~ heap_union_empty_l. }
intros. applys prop_ext. iff (h1&h2&P1&P2&D&E) (N1&N2).
{ lets (R&HP): hprop_pure_inv (rm P1). subst. rewrite~ heap_union_empty_l. }
{ exists~ heap_empty h. }
Qed.
......@@ -513,17 +513,6 @@ Qed.
End Credits.
(*------------------------------------------------------------------*)
(* ** Notation for compatibility *)
Notation "'heap_empty'" := state_empty : heap_scope.
Notation "h1 \u h2" := (state_union h1 h2)
(at level 51, right associativity) : heap_scope.
Definition heap_union_empty_r := state_union_empty_r.
(*------------------------------------------------------------------*)
(* ** Tactics for reductions *)
......@@ -538,6 +527,7 @@ Ltac state_red_base tt ::=
Implicit Types h : heap.
Implicit Types H : hprop.
Implicit Types Q : val -> hprop.
(*------------------------------------------------------------------*)
......@@ -553,7 +543,7 @@ Definition triple t H Q :=
(*------------------------------------------------------------------*)
(* ** Auxiliary definitions *)
(* ** Definitions of [pay] *)
Definition pay_one H H' :=
H ==> (\$ 1%nat) \* H'.
......
......@@ -104,6 +104,13 @@ Definition hprop_exists A (J : A -> hprop) : hprop :=
Definition hprop_gc :=
hprop_exists (fun (H:hprop) => H).
(* Remark: [hprop_or] is not needed in practice.
Definition hprop_or (H1 H2 : hprop) : hprop :=
fun h => H1 h \/ H2 h.
*)
(** Notation *)
Notation "\[]" := (hprop_empty)
......
This diff is collapsed.
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