Commit 20691a2e authored by Ralf Jung's avatar Ralf Jung

Merge remote-tracking branch 'origin/master' into hackgreement

Conflicts:
	coq-ho/iris_ht_rules.v
parents 992d818f 1ebc9a44
Module Type CORE_LANG.
Delimit Scope lang_scope with lang.
Local Open Scope lang_scope.
(******************************************************************)
(** ** Syntax, machine state, and atomic reductions **)
(******************************************************************)
(** Expressions and values **)
Parameter expr : Type. (* PDS: setoid. *)
Parameter expr : Type.
Parameter is_value : expr -> Prop.
Definition value : Type := {e: expr | is_value e}.
......@@ -24,32 +22,51 @@ Module Type CORE_LANG.
fork e1 = fork e2 -> e1 = e2.
(** Evaluation contexts **)
Parameter ectx : Type. (* PDS: setoid. *)
Parameter ectx : Type.
Parameter empty_ctx : ectx.
Parameter comp_ctx : ectx -> ectx -> ectx.
Parameter fill : ectx -> expr -> expr.
Notation "'ε'" := empty_ctx : lang_scope.
Notation "K1 ∘ K2" := (comp_ctx K1 K2) (at level 40, left associativity) : lang_scope.
(* We used to also have notation for filling, but registering any of "[[", "]]", "])" as keyword
is bound to become annoying in Ltac. *)
Axiom fill_empty : forall e, fill ε e = e.
Axiom fill_comp : forall K1 K2 e, fill K1 (fill K2 e) = fill (K1 K2) e.
Axiom fill_inj1 : forall K1 K2 e, (* left-Cancellativity*)
fill K1 e = fill K2 e -> K1 = K2.
Axiom fill_inj2 : forall K e1 e2, (* right-cancellativity *)
fill K e1 = fill K e2 -> e1 = e2.
Axiom fill_noinv: forall K1 K2, (* positivity *)
K1 K2 = ε -> K1 = ε /\ K2 = ε.
Axiom fill_value : forall K e,
is_value (fill K e) ->
K = ε.
Axiom fill_fork : forall K e e',
fork e' = fill K e ->
K = ε.
(*
All of
comp_ctx_assoc
comp_ctx_inj_r
comp_ctx_emp_r
arise only in the proof of
step_same_ctx K K' e e' :
fill K e = fill K' e' ->
reducible e ->
reducible e' ->
K = K'.
Moreover, comp_ctx_positive gets used only in step_same_ctx
and
atomic_fill e K :
atomic (fill K e) ->
~ is_value e ->
K = empty_ctx.
It might be simpler to (prove and) assume these two rather
than those four.
*)
Axiom comp_ctx_emp_r : forall K,
comp_ctx K empty_ctx = K.
Axiom comp_ctx_assoc : forall K0 K1 K2,
comp_ctx K0 (comp_ctx K1 K2) = comp_ctx (comp_ctx K0 K1) K2.
Axiom comp_ctx_inj_r : forall K K1 K2,
comp_ctx K K1 = comp_ctx K K2 -> K1 = K2.
Axiom comp_ctx_positive : forall K1 K2,
comp_ctx K1 K2 = empty_ctx -> K1 = empty_ctx /\ K2 = empty_ctx.
Axiom fill_empty : forall e, fill empty_ctx e = e.
Axiom fill_comp : forall K1 K2 e, fill K1 (fill K2 e) = fill (comp_ctx K1 K2) e.
Axiom fill_inj_r : forall K e1 e2, fill K e1 = fill K e2 -> e1 = e2.
Axiom fill_value : forall K e, is_value (fill K e) -> is_value e.
Axiom fill_fork : forall K e e', fork e' = fill K e -> K = empty_ctx.
(** Shared machine state (e.g., the heap) **)
Parameter state : Type. (* PDS: setoid. *)
Parameter state : Type.
(** Primitive (single thread) machine configurations **)
Definition prim_cfg : Type := (expr * state)%type.
......@@ -80,14 +97,14 @@ Module Type CORE_LANG.
fill K e = fill K' e' ->
reducible e' ->
~ is_value e ->
exists K'', K' = K K''.
exists K'', K' = comp_ctx K K''.
(* Similar to above, buth with a fork instead of a reducible
expression *)
Axiom fork_by_value :
forall K K' e e',
fill K e = fill K' (fork e') ->
~ is_value e ->
exists K'', K' = K K''.
exists K'', K' = comp_ctx K K''.
(** Atomic expressions **)
Parameter atomic : expr -> Prop.
......
......@@ -56,6 +56,17 @@ Module StupidLang : CORE_LANG.
Local Open Scope lang_scope.
Lemma comp_ctx_assoc K0 K1 K2 : (K0 K1) K2 = K0 (K1 K2).
Proof. reflexivity. Qed.
Lemma comp_ctx_emp_r K : K ε = K.
Proof. destruct K. reflexivity. Qed.
Lemma comp_ctx_inj_r K K1 K2 : K K1 = K K2 -> K1 = K2.
Proof.
destruct K1, K2. now tauto.
Qed.
Lemma fill_empty e : ε [[ e ]] = e.
Proof.
reflexivity.
......@@ -65,23 +76,18 @@ Module StupidLang : CORE_LANG.
Proof.
reflexivity.
Qed.
Lemma fill_inj1 K1 K2 e :
K1 [[ e ]] = K2 [[ e ]] -> K1 = K2.
Proof.
intros _. destruct K1, K2. reflexivity.
Qed.
Lemma fill_inj2 K e1 e2 :
Lemma fill_inj_r K e1 e2 :
K [[ e1 ]] = K [[ e2 ]] -> e1 = e2.
Proof.
tauto.
Qed.
Lemma fill_noinv K1 K2:
Lemma comp_ctx_positive K1 K2:
K1 K2 = ε -> K1 = ε /\ K2 = ε.
Proof.
destruct K1, K2. intros _. split; reflexivity.
Qed.
Lemma fill_value K e:
is_value (K [[ e ]]) -> K = ε.
is_value (K [[ e ]]) -> is_value e.
Proof.
destruct K. now auto.
Qed.
......
......@@ -32,9 +32,7 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
simpl; reflexivity.
- contradiction (values_stuck HV HDec).
repeat eexists; eassumption.
- subst e; assert (HT := fill_value HV); subst K.
revert HV; rewrite fill_empty; intros.
contradiction (fork_not_value _ HV).
- subst e; contradiction (fork_not_value (fill_value HV)).
- unfold safeExpr. auto.
Qed.
......@@ -64,17 +62,17 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
change (wp safe m (fill K e) φ w' (S (S k))) in Hφ.
rewrite ->unfold_wp in Hφ. eapply Hφ ; [omega | de_auto_eq | eassumption ].
- intros wf; intros; edestruct He as [_ [HS [HF HS'] ] ]; try eassumption; [].
split; [intros HVal; contradiction HNVal; assert (HT := fill_value HVal);
subst K; rewrite fill_empty in HVal; assumption | split; [| split]; intros].
split; [ | split; [| split]; intros].
+ intros HVal; contradiction (HNVal (fill_value HVal)).
+ clear He HF HE; edestruct step_by_value as [K' EQK];
[eassumption | repeat eexists; eassumption | eassumption |].
subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
subst K0; rewrite <- fill_comp in HDec; apply fill_inj_r in HDec.
edestruct HS as [w' [He HE]]; try eassumption; [].
subst e; clear HStep HS.
eexists. split; last eassumption.
rewrite <- fill_comp. apply IH; assumption.
+ clear He HS HE; edestruct fork_by_value as [K' EQK]; try eassumption; [].
subst K0; rewrite <- fill_comp in HDec; apply fill_inj2 in HDec.
subst K0; rewrite <- fill_comp in HDec; apply fill_inj_r in HDec.
edestruct HF as [wfk [wret [HWR [HWF HE]]]];
try eassumption; []; subst e; clear HF.
do 2 eexists; split; [| split; eassumption].
......@@ -197,8 +195,8 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
+ assumption.
+ omega.
- intros. exfalso. eapply values_stuck; [.. | repeat eexists]; eassumption.
- intros. exfalso. clear - HDec HVal; subst; assert (HT := fill_value HVal); subst.
rewrite ->fill_empty in HVal; now apply fork_not_value in HVal.
- intros. exfalso. clear - HDec HVal. subst.
contradiction (fork_not_value (fill_value HVal)).
- intros; left; assumption.
Qed.
......@@ -309,9 +307,7 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
exists r1'' r2; split; [reflexivity | split; [assumption |] ].
unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; apply HLR.
+ eapply values_stuck; [.. | repeat eexists]; eassumption.
+ subst; clear -HVal.
assert (HT := fill_value HVal); subst K; rewrite ->fill_empty in HVal.
contradiction (fork_not_value e').
+ subst; clear -HVal. contradiction (fork_not_value (fill_value HVal)).
+ unfold safeExpr. now auto.
- subst; eapply fork_not_atomic; eassumption.
- rewrite <- EQr, <- assoc in HE; rewrite ->unfold_wp in Hwp.
......@@ -321,12 +317,13 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
(** Fork **)
Lemma wpFork safe m R e :
wp safe m e (umconst ) * R wp safe m (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).
wp safe m e (umconst ) * R wp safe m (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)). (* PDS: Why sc not and? *)
Proof.
intros w n r [r1 [r2 [EQr [Hwp HLR] ] ] ].
destruct n as [| n]; [apply wpO |].
rewrite ->unfold_wp; intros w'; intros.
split; [intros; contradiction (fork_not_value e) | split; intros; [exfalso | split; intros ] ].
split; [| split; intros; [exfalso | split; intros ] ].
- intros. contradiction (fork_not_value HV).
- assert (HT := fill_fork HDec); subst K; rewrite ->fill_empty in HDec; subst.
eapply fork_stuck with (K := ε); [| repeat eexists; eassumption ]; reflexivity.
- assert (HT := fill_fork HDec); subst K; rewrite ->fill_empty in HDec.
......@@ -342,8 +339,7 @@ Module Type IRIS_HT_RULES (RL : VIRA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP:
simpl; reflexivity.
+ eapply values_stuck; [exact fork_ret_is_value | eassumption | repeat eexists; eassumption].
+ assert (HV := fork_ret_is_value); rewrite ->HDec in HV; clear HDec.
assert (HT := fill_value HV);subst K; rewrite ->fill_empty in HV.
eapply fork_not_value; eassumption.
contradiction (fork_not_value (fill_value HV)).
+ left; apply fork_ret_is_value.
- right; right; exists e empty_ctx; rewrite ->fill_empty; reflexivity.
Qed.
......
......@@ -469,9 +469,8 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
eapply values_stuck; first by eassumption.
* eassumption.
* do 2 eexists. eassumption.
+ move=>? K Hfill. exfalso. eapply fork_not_value. subst e'.
assert(HK := fill_value Hval). subst K.
rewrite fill_empty in Hval. eassumption.
+ move=>e'' K Hfill. clear - Hval Hfill. subst.
contradiction (fork_not_value (fill_value Hval)).
+ move=>_. left. assumption.
Qed.
......
......@@ -13,10 +13,16 @@ Module Lang (C : CORE_LANG).
Export C.
Delimit Scope lang_scope with lang.
Local Open Scope lang_scope.
Notation "'ε'" := empty_ctx : lang_scope.
Notation "K1 ∘ K2" := (comp_ctx K1 K2) (at level 40, left associativity) : lang_scope.
Arguments fork_not_value {_} _.
Arguments comp_ctx_positive {_ _} _.
Arguments fork_inj {_ _} _.
Arguments fill_inj1 {_ _} _ _.
Arguments fill_inj2 _ {_ _} _.
Arguments fill_noinv {_ _} _.
Arguments fill_inj_r _ {_ _} _.
Arguments fill_value {_ _} _.
Arguments fill_fork {_ _ _} _.
Arguments values_stuck {_} _ {_ _} _ _.
......@@ -44,62 +50,13 @@ Module Lang (C : CORE_LANG).
ρ' = (t1 ++ fill K fork_ret :: t2 ++ e :: nil, σ) ->
step ρ ρ'.
(* Some derived facts about contexts *)
Lemma comp_ctx_assoc {K0 K1 K2} :
(K0 K1) K2 = K0 (K1 K2).
Proof.
apply (fill_inj1 fork_ret).
now rewrite <- !fill_comp.
Qed.
Lemma comp_ctx_emp_l {K} :
ε K = K.
Proof.
apply (fill_inj1 fork_ret).
now rewrite <- fill_comp, fill_empty.
Qed.
Lemma comp_ctx_emp_r {K} :
K ε = K.
Proof.
apply (fill_inj1 fork_ret).
now rewrite <- fill_comp, fill_empty.
Qed.
Lemma comp_ctx_inj1 {K1 K2 K} :
K1 K = K2 K ->
K1 = K2.
Proof.
intros HEq.
apply fill_inj1 with (fill K fork_ret).
now rewrite -> !fill_comp, HEq.
Qed.
Lemma comp_ctx_inj2 {K K1 K2} :
K K1 = K K2 ->
K1 = K2.
Proof.
intros HEq.
apply fill_inj1 with fork_ret, fill_inj2 with K.
now rewrite -> !fill_comp, HEq.
Qed.
Lemma comp_ctx_neut_emp_r {K K'} :
K = K K' ->
K' = ε.
Proof.
intros HEq.
rewrite <- comp_ctx_emp_r in HEq at 1.
apply comp_ctx_inj2 in HEq; now symmetry.
Qed.
Lemma comp_ctx_neut_emp_l {K K'} :
K = K' K ->
K' = ε.
Proof.
intros HEq.
rewrite <- comp_ctx_emp_l in HEq at 1.
apply comp_ctx_inj1 in HEq; now symmetry.
apply comp_ctx_inj_r in HEq; now symmetry.
Qed.
(* Lemmas about expressions *)
......@@ -135,9 +92,9 @@ Module Lang (C : CORE_LANG).
+ assumption.
+ now apply reducible_not_value.
+ subst K.
rewrite comp_ctx_assoc in H_K''.
rewrite <- comp_ctx_assoc in H_K''.
assert (H_emp := comp_ctx_neut_emp_r H_K'').
apply fill_noinv in H_emp.
apply comp_ctx_positive in H_emp.
destruct H_emp as[H_K'''_emp H_K''_emp].
subst K'' K'''.
now rewrite comp_ctx_emp_r.
......@@ -177,7 +134,7 @@ Module Lang (C : CORE_LANG).
- now rewrite fill_empty.
- now apply atomic_reducible.
- assumption.
- symmetry in EQK; now apply fill_noinv in EQK.
- symmetry in EQK; now apply comp_ctx_positive in EQK.
Qed.
(* Reflexive, transitive closure of the step relation *)
......
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