Commit c91b93ac authored by Ralf Jung's avatar Ralf Jung

Merge remote-tracking branch 'origin/master' into ralf/prophecy

parents 33df52c8 7041c043
......@@ -33,6 +33,11 @@ build-coq.dev:
OPAM_PINS: "coq version dev"
VALIDATE: "1"
build-coq.8.8.2:
<<: *template
variables:
OPAM_PINS: "coq version 8.8.2"
build-coq.8.8.1:
<<: *template
variables:
......
......@@ -29,7 +29,7 @@ Changes in and extensions of the theory:
functions.
* [#] Add atomic updates and logically atomic triples, including tactic support.
See `heap_lang/lib/increment.v` for an example.
* [#] HeapLang now uses right-to-left evaluation order. This makes it
* [#] heap_lang now uses right-to-left evaluation order. This makes it
significantly easier to write specifications of curried functions.
Changes in Coq:
......@@ -84,6 +84,7 @@ Changes in Coq:
* Changed `IntoVal` to be directly usable for rewriting `e` into `of_val v`, and
changed `AsVal` to be usable for rewriting via the `[v <-]` destruct pattern.
* `wp_fork` is now written in curried form.
* `PureExec`/`wp_pure` now supports taking multiple steps at once.
## Iris 3.1.0 (released 2017-12-19)
......
......@@ -14,7 +14,7 @@ document is [available online](http://plv.mpi-sws.org/iris/appendix-3.1.pdf).
This version is known to compile with:
- Coq 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1
- Coq 8.7.1 / 8.7.2 / 8.8.0 / 8.8.1 / 8.8.2
- A development version of [std++](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp)
For a version compatible with Coq 8.6, have a look at the
......
......@@ -962,16 +962,6 @@ Section persistently_affine_bi.
rewrite assoc -persistently_and_sep_r.
by rewrite persistently_elim impl_elim_r.
Qed.
Lemma impl_alt P Q : (P Q) R, R <pers> (P R - Q).
Proof.
apply (anti_symm ()).
- rewrite -(right_id True%I bi_and (P Q)%I) -(exist_intro (P Q)%I).
apply and_mono_r. rewrite -persistently_pure.
apply persistently_intro', wand_intro_l.
by rewrite impl_elim_r persistently_pure right_id.
- apply exist_elim=> R. apply impl_intro_l.
by rewrite assoc persistently_and_sep_r persistently_elim wand_elim_r.
Qed.
End persistently_affine_bi.
(* The intuitionistic modality *)
......@@ -1082,6 +1072,16 @@ Proof.
apply sep_mono; first done. apply and_elim_r.
Qed.
Lemma impl_alt P Q : (P Q) R, R <pers> (P R - Q).
Proof.
apply (anti_symm ()).
- rewrite -(right_id True%I bi_and (P Q)%I) -(exist_intro (P Q)%I).
apply and_mono_r. rewrite impl_elim_r -entails_wand //.
apply persistently_emp_intro.
- apply exist_elim=> R. apply impl_intro_l.
rewrite assoc persistently_and_intuitionistically_sep_r.
by rewrite intuitionistically_elim wand_elim_r.
Qed.
Section bi_affine_intuitionistically.
Context `{BiAffine PROP}.
......
......@@ -10,7 +10,7 @@ Set Default Proof Using "Type".
for this is that it makes curried functions usable: Given a WP for [f a b], we
know that any effects [f] might have to not matter until after *both* [a] and
[b] are evaluated. With left-to-right evaluation, that triple is basically
useless the user let-expands [b].
useless unless the user let-expands [b].
- For prophecy variables, we annotate the reduction steps with an "observation"
and tweak adequacy such that WP knows all future observations. There is
......
......@@ -64,7 +64,8 @@ Local Ltac solve_exec_puredet := simpl; intros; by inv_head_step.
Local Ltac solve_pure_exec :=
unfold IntoVal in *;
repeat match goal with H : AsVal _ |- _ => destruct H as [??] end; subst;
apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
intros ?; apply nsteps_once, pure_head_step_pure_step;
constructor; [solve_exec_safe | solve_exec_puredet].
Class AsRec (e : expr) (f x : binder) (erec : expr) :=
as_rec : e = Rec f x erec.
......@@ -75,37 +76,37 @@ Proof. by unlock. Qed.
Instance pure_rec f x (erec e1 e2 : expr)
`{!AsVal e2, AsRec e1 f x erec, Closed (f :b: x :b: []) erec} :
PureExec True (App e1 e2) (subst' x e2 (subst' f e1 erec)).
PureExec True 1 (App e1 e2) (subst' x e2 (subst' f e1 erec)).
Proof. unfold AsRec in *; solve_pure_exec. Qed.
Instance pure_unop op e v v' `{!IntoVal e v} :
PureExec (un_op_eval op v = Some v') (UnOp op e) (of_val v').
PureExec (un_op_eval op v = Some v') 1 (UnOp op e) (of_val v').
Proof. solve_pure_exec. Qed.
Instance pure_binop op e1 e2 v1 v2 v' `{!IntoVal e1 v1, !IntoVal e2 v2} :
PureExec (bin_op_eval op v1 v2 = Some v') (BinOp op e1 e2) (of_val v').
PureExec (bin_op_eval op v1 v2 = Some v') 1 (BinOp op e1 e2) (of_val v').
Proof. solve_pure_exec. Qed.
Instance pure_if_true e1 e2 : PureExec True (If (Lit (LitBool true)) e1 e2) e1.
Instance pure_if_true e1 e2 : PureExec True 1 (If (Lit (LitBool true)) e1 e2) e1.
Proof. solve_pure_exec. Qed.
Instance pure_if_false e1 e2 : PureExec True (If (Lit (LitBool false)) e1 e2) e2.
Instance pure_if_false e1 e2 : PureExec True 1 (If (Lit (LitBool false)) e1 e2) e2.
Proof. solve_pure_exec. Qed.
Instance pure_fst e1 e2 v1 `{!IntoVal e1 v1, !AsVal e2} :
PureExec True (Fst (Pair e1 e2)) e1.
PureExec True 1 (Fst (Pair e1 e2)) e1.
Proof. solve_pure_exec. Qed.
Instance pure_snd e1 e2 v2 `{!AsVal e1, !IntoVal e2 v2} :
PureExec True (Snd (Pair e1 e2)) e2.
PureExec True 1 (Snd (Pair e1 e2)) e2.
Proof. solve_pure_exec. Qed.
Instance pure_case_inl e0 v e1 e2 `{!IntoVal e0 v} :
PureExec True (Case (InjL e0) e1 e2) (App e1 e0).
PureExec True 1 (Case (InjL e0) e1 e2) (App e1 e0).
Proof. solve_pure_exec. Qed.
Instance pure_case_inr e0 v e1 e2 `{!IntoVal e0 v} :
PureExec True (Case (InjR e0) e1 e2) (App e2 e0).
PureExec True 1 (Case (InjR e0) e1 e2) (App e2 e0).
Proof. solve_pure_exec. Qed.
Section lifting.
......
......@@ -115,18 +115,17 @@ Notation "λ: x y .. z , e" := (Lam x%bind (Lam y%bind .. (Lam z%bind e%E) ..))
(* When parsing lambdas, we want them to be locked (so as to avoid needless
unfolding by tactics and unification). However, unlocked lambda-values sometimes
appear as part of compound expressions, in which case we want them to be pretty
printed too. We achieve that by first defining the non-locked notation, and then
the locked notation. Both will be used for pretty-printing, but only the last
will be used for parsing. *)
printed too. We achieve that by using printing only notations for the non-locked
notation. *)
Notation "λ: x , e" := (LamV x%bind e%E)
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
format "'[' 'λ:' x , '/ ' e ']'", only printing) : val_scope.
Notation "λ: x , e" := (locked (LamV x%bind e%E))
(at level 200, x at level 1, e at level 200,
format "'[' 'λ:' x , '/ ' e ']'") : val_scope.
Notation "λ: x y .. z , e" := (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. ))
(at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope.
format "'[' 'λ:' x y .. z , '/ ' e ']'", only printing) : val_scope.
Notation "λ: x y .. z , e" := (locked (LamV x%bind (Lam y%bind .. (Lam z%bind e%E) .. )))
(at level 200, x, y, z at level 1, e at level 200,
format "'[' 'λ:' x y .. z , '/ ' e ']'") : val_scope.
......
......@@ -30,18 +30,18 @@ Tactic Notation "wp_expr_eval" tactic(t) :=
Ltac wp_expr_simpl := wp_expr_eval simpl.
Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
PureExec φ e1 e2
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
MaybeIntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs n Δ Δ'
envs_entails Δ' (WP e2 @ s; E {{ Φ }})
envs_entails Δ (WP e1 @ s; E {{ Φ }}).
Proof.
rewrite envs_entails_eq=> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite HΔ' -lifting.wp_pure_step_later //.
Qed.
Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ Φ :
PureExec φ e1 e2
Lemma tac_twp_pure `{heapG Σ} Δ s E e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
envs_entails Δ (WP e2 @ s; E [{ Φ }])
envs_entails Δ (WP e1 @ s; E [{ Φ }]).
......
......@@ -214,23 +214,24 @@ Section ectx_language.
econstructor; eauto.
Qed.
Lemma det_head_step_pure_exec (P : Prop) e1 e2 :
( σ, P head_reducible_no_obs e1 σ)
( σ1 κ e2' σ2 efs,
P head_step e1 σ1 κ e2' σ2 efs κ = None σ1 = σ2 e2=e2' efs = [])
PureExec P e1 e2.
Record pure_head_step (e1 e2 : expr Λ) := {
pure_head_step_safe σ1 : head_reducible_no_obs e1 σ1;
pure_head_step_det σ1 κ e2' σ2 efs :
head_step e1 σ1 κ e2' σ2 efs κ = None σ1 = σ2 e2 = e2' efs = []
}.
Lemma pure_head_step_pure_step e1 e2 : pure_head_step e1 e2 pure_step e1 e2.
Proof.
intros Hp1 Hp2. split.
- intros σ ?. destruct (Hp1 σ) as (e2' & σ2 & efs & ?); first done.
intros [Hp1 Hp2]. split.
- intros σ. destruct (Hp1 σ) as (e2' & σ2 & efs & ?).
eexists e2', σ2, efs. by apply head_prim_step.
- intros σ1 κ e2' σ2 efs ? ?%head_reducible_prim_step; eauto using head_reducible_no_obs_reducible.
- intros σ1 κ e2' σ2 efs ?%head_reducible_prim_step; eauto using head_reducible_no_obs_reducible.
Qed.
Global Instance pure_exec_fill K e1 e2 φ :
PureExec φ e1 e2
PureExec φ (fill K e1) (fill K e2).
Global Instance pure_exec_fill K φ n e1 e2 :
PureExec φ n e1 e2
PureExec φ n (fill K e1) (fill K e2).
Proof. apply: pure_exec_ctx. Qed.
End ectx_language.
Arguments ectx_lang : clear implicits.
......
......@@ -177,31 +177,40 @@ Section language.
intros* Heq [? Hs]. pose proof (step_Permutation _ _ _ _ _ _ Heq Hs). firstorder.
Qed.
Class PureExec (P : Prop) (e1 e2 : expr Λ) := {
pure_exec_safe σ :
P reducible_no_obs e1 σ;
pure_exec_puredet σ1 κ e2' σ2 efs :
P prim_step e1 σ1 κ e2' σ2 efs κ = None σ1 = σ2 e2 = e2' efs = [];
Record pure_step (e1 e2 : expr Λ) := {
pure_step_safe σ1 : reducible_no_obs e1 σ1;
pure_step_det σ1 κ e2' σ2 efs :
prim_step e1 σ1 κ e2' σ2 efs κ = None σ1 = σ2 e2 = e2' efs = []
}.
Lemma hoist_pred_pure_exec (P : Prop) (e1 e2 : expr Λ) :
(P PureExec True e1 e2)
PureExec P e1 e2.
Proof. intros HPE. split; intros; eapply HPE; eauto. Qed.
(* TODO: Exclude the case of [n=0], either here, or in [wp_pure] to avoid it
succeeding when it did not actually do anything. *)
Class PureExec (φ : Prop) (n : nat) (e1 e2 : expr Λ) :=
pure_exec : φ relations.nsteps pure_step n e1 e2.
(* We do not make this an instance because it is awfully general. *)
Lemma pure_exec_ctx K `{LanguageCtx Λ K} e1 e2 φ :
PureExec φ e1 e2
PureExec φ (K e1) (K e2).
Lemma pure_step_ctx K `{LanguageCtx Λ K} e1 e2 :
pure_step e1 e2
pure_step (K e1) (K e2).
Proof.
intros [Hred Hstep]. split.
- unfold reducible_no_obs in *. naive_solver eauto using fill_step.
- intros σ1 κ e2' σ2 efs ? Hpstep.
- intros σ1 κ e2' σ2 efs Hpstep.
destruct (fill_step_inv e1 σ1 κ e2' σ2 efs) as (e2'' & -> & ?); [|exact Hpstep|].
+ destruct (Hred σ1) as (? & ? & ? & ?); eauto using val_stuck.
+ edestruct (Hstep σ1 κ e2'' σ2 efs) as (? & -> & -> & ->); auto.
Qed.
Lemma pure_step_nsteps_ctx K `{LanguageCtx Λ K} n e1 e2 :
relations.nsteps pure_step n e1 e2
relations.nsteps pure_step n (K e1) (K e2).
Proof. induction 1; econstructor; eauto using pure_step_ctx. Qed.
(* We do not make this an instance because it is awfully general. *)
Lemma pure_exec_ctx K `{LanguageCtx Λ K} φ n e1 e2 :
PureExec φ n e1 e2
PureExec φ n (K e1) (K e2).
Proof. rewrite /PureExec; eauto using pure_step_nsteps_ctx. Qed.
(* This is a family of frequent assumptions for PureExec *)
Class IntoVal (e : expr Λ) (v : val Λ) :=
into_val : of_val v = e.
......
......@@ -127,23 +127,25 @@ Proof.
by iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
Qed.
Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ Φ :
PureExec φ e1 e2
Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
(|={E,E'}=> WP e2 @ s; E {{ Φ }}) WP e1 @ s; E {{ Φ }}.
Nat.iter n (λ P, |={E,E'}=> P) (WP e2 @ s; E {{ Φ }}) WP e1 @ s; E {{ Φ }}.
Proof.
iIntros ([??] Hφ) "HWP".
iApply (wp_lift_pure_det_step with "[HWP]").
- intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val.
iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
iApply wp_lift_pure_det_step.
- intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
- destruct s; naive_solver.
- by rewrite big_sepL_nil right_id.
- rewrite /= right_id. by iApply (step_fupd_wand with "Hwp").
Qed.
Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ :
PureExec φ e1 e2
Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}.
^n WP e2 @ s; E {{ Φ }} WP e1 @ s; E {{ Φ }}.
Proof.
intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //.
intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec.
induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH.
Qed.
End lifting.
......@@ -70,13 +70,15 @@ Proof.
by iIntros "!>" (κ e' efs' σ (->&_&->&->)%Hpuredet).
Qed.
Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ Φ :
PureExec φ e1 e2
Lemma twp_pure_step `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
PureExec φ n e1 e2
φ
WP e2 @ s; E [{ Φ }] WP e1 @ s; E [{ Φ }].
Proof.
iIntros ([??] Hφ) "HWP".
iApply (twp_lift_pure_det_step with "[HWP]"); [eauto|naive_solver|auto].
iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
iApply twp_lift_pure_det_step; [done|naive_solver|].
iModIntro. rewrite /= right_id. by iApply "IH".
Qed.
End lifting.
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