Skip to content

GitLab

Commit 98b48609 authored by Ralf Jung's avatar Ralf Jung
Browse files

make proofs of physical lifting much shorter

parent 4fae25bb
Hide whitespace changes
Inline Side-by-side
barrier/heap_lang.v
View file @ 98b48609
......@@ -105,7 +105,9 @@ Inductive ectx_item :=
| CasLCtx (e1 : expr) (e2 : expr)
| CasMCtx (v0 : val) (e2 : expr)
| CasRCtx (v0 : val) (v1 : val).
Notation ectx := (list ectx_item).
Implicit Types Ki : ectx_item.
Implicit Types K : ectx.
......@@ -132,6 +134,7 @@ Definition ectx_item_fill (Ki : ectx_item) (e : expr) : expr :=
| CasMCtx v0 e2 => Cas (of_val v0) e e2
| CasRCtx v0 v1 => Cas (of_val v0) (of_val v1) e
end.
Instance ectx_fill : Fill ectx expr :=
fix go K e := let _ : Fill _ _ := @go in
match K with [] => e | Ki :: K => ectx_item_fill Ki (fill K e) end.
......@@ -181,6 +184,9 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
σ !! l = Some v1 →
head_step (Cas (Loc l) e1 e2) σ LitTrue (<[l:=v2]>σ) None.
Definition head_reducible e σ : Prop :=
∃ e' σ' ef, head_step e σ e' σ' ef.
(** Atomic expressions *)
Definition atomic (e: expr) :=
match e with
......@@ -202,40 +208,53 @@ Inductive prim_step
(** Basic properties about the language *)
Lemma to_of_val v : to_val (of_val v) = Some v.
Proof. by induction v; simplify_option_equality. Qed.
Lemma of_to_val e v : to_val e = Some v → of_val v = e.
Proof.
revert v; induction e; intros; simplify_option_equality; auto with f_equal.
Qed.
Instance: Injective (=) (=) of_val.
Proof. by intros ?? Hv; apply (injective Some); rewrite -!to_of_val Hv. Qed.
Instance ectx_item_fill_inj Ki : Injective (=) (=) (ectx_item_fill Ki).
Proof. destruct Ki; intros ???; simplify_equality'; auto with f_equal. Qed.
Instance ectx_fill_inj K : Injective (=) (=) (fill K).
Proof. red; induction K as [|Ki K IH]; naive_solver. Qed.
Lemma fill_app K1 K2 e : fill (K1 ++ K2) e = fill K1 (fill K2 e).
Proof. revert e; induction K1; simpl; auto with f_equal. Qed.
Lemma fill_val K e : is_Some (to_val (fill K e)) → is_Some (to_val e).
Proof.
intros [v' Hv']; revert v' Hv'.
induction K as [|[]]; intros; simplify_option_equality; eauto.
Qed.
Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
Proof. rewrite !eq_None_not_Some; eauto using fill_val. Qed.
Lemma values_head_stuck e1 σ1 e2 σ2 ef :
head_step e1 σ1 e2 σ2 ef → to_val e1 = None.
Proof. destruct 1; naive_solver. Qed.
Lemma values_stuck e1 σ1 e2 σ2 ef : prim_step e1 σ1 e2 σ2 ef → to_val e1 = None.
Proof. intros [??? -> -> ?]; eauto using fill_not_val, values_head_stuck. Qed.
Lemma atomic_not_val e : atomic e → to_val e = None.
Proof. destruct e; naive_solver. Qed.
Lemma atomic_fill K e : atomic (fill K e) → to_val e = None → K = [].
Proof.
rewrite eq_None_not_Some.
destruct K as [|[]]; naive_solver eauto using fill_val.
Qed.
Lemma atomic_head_step e1 σ1 e2 σ2 ef :
atomic e1 → head_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
Proof. destruct 2; simpl; rewrite ?to_of_val; naive_solver. Qed.
Lemma atomic_step e1 σ1 e2 σ2 ef :
atomic e1 → prim_step e1 σ1 e2 σ2 ef → is_Some (to_val e2).
Proof.
......@@ -243,9 +262,11 @@ Proof.
assert (K = []) as -> by eauto 10 using atomic_fill, values_head_stuck.
naive_solver eauto using atomic_head_step.
Qed.
Lemma head_ctx_step_val Ki e σ1 e2 σ2 ef :
head_step (ectx_item_fill Ki e) σ1 e2 σ2 ef → is_Some (to_val e).
Proof. destruct Ki; inversion_clear 1; simplify_option_equality; eauto. Qed.
Lemma fill_item_inj Ki1 Ki2 e1 e2 :
to_val e1 = None → to_val e2 = None →
ectx_item_fill Ki1 e1 = ectx_item_fill Ki2 e2 → Ki1 = Ki2.
......@@ -255,6 +276,7 @@ Proof.
| H : to_val (of_val _) = None |- _ => by rewrite to_of_val in H
end; auto.
Qed.
(* When something does a step, and another decomposition of the same expression
has a non-val [e] in the hole, then [K] is a left sub-context of [K'] - in
other words, [e] also contains the reducible expression *)
......@@ -270,12 +292,29 @@ Proof.
cut (Ki = Ki'); [naive_solver eauto using prefix_of_cons|].
eauto using fill_item_inj, values_head_stuck, fill_not_val.
Qed.
Lemma prim_head_step e1 σ1 e2 σ2 ef :
head_reducible e1 σ1 →
prim_step e1 σ1 e2 σ2 ef →
head_step e1 σ1 e2 σ2 ef.
Proof.
intros (e2'' & σ2'' & ef'' & Hstep'') [K' e1' e2' Heq1 Heq2 Hstep].
assert (K' `prefix_of` []) as Hemp.
{ eapply step_by_val; last first.
- eexact Hstep''.
- eapply values_head_stuck. eexact Hstep.
- done. }
destruct K'; last by (exfalso; eapply prefix_of_nil_not; eassumption).
by subst e1 e2.
Qed.
Lemma alloc_fresh e v σ :
let l := fresh (dom _ σ) in
to_val e = Some v → head_step (Alloc e) σ (Loc l) (<[l:=v]>σ) None.
Proof.
by intros; apply AllocS, (not_elem_of_dom (D:=gset positive)), is_fresh.
Qed.
End heap_lang.
(** Language *)
......@@ -284,6 +323,7 @@ Program Canonical Structure heap_lang : language := {|
of_val := heap_lang.of_val; to_val := heap_lang.to_val;
atomic := heap_lang.atomic; prim_step := heap_lang.prim_step;
|}.
Solve Obligations with eauto using heap_lang.to_of_val, heap_lang.of_to_val,
heap_lang.values_stuck, heap_lang.atomic_not_val, heap_lang.atomic_step.
Global Instance heap_lang_ctx : CtxLanguage heap_lang heap_lang.ectx.
......@@ -299,3 +339,11 @@ Proof.
exists (fill K' e2''); rewrite heap_lang.fill_app; split; auto.
econstructor; eauto.
Qed.
Lemma head_reducible_reducible e σ :
heap_lang.head_reducible e σ → reducible e σ.
Proof.
intros H. destruct H; destruct_conjs.
do 3 eexists.
eapply heap_lang.Ectx_step with (K:=[]); last eassumption; done.
Qed.
barrier/heap_lang_tactics.v
View file @ 98b48609
......@@ -61,7 +61,8 @@ Ltac reshape_expr e tac :=
end in go (@nil ectx_item) e.
Ltac do_step tac :=
try match goal with |- reducible _ _ => eexists _, _, _ end;
try match goal with |- language.reducible _ _ => eexists _, _, _ end;
try match goal with |- head_reducible _ _ => eexists _, _, _ end;
simpl;
match goal with
| |- prim_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
......@@ -69,4 +70,7 @@ Ltac do_step tac :=
eapply Ectx_step with K e1' _); [reflexivity|reflexivity|];
first [apply alloc_fresh|econstructor];
rewrite ?to_of_val; tac; fail
| |- head_step ?e1 ?σ1 ?e2 ?σ2 ?ef =>
first [apply alloc_fresh|econstructor];
rewrite ?to_of_val; tac; fail
end.
barrier/lifting.v
View file @ 98b48609
......@@ -2,7 +2,8 @@ Require Import prelude.gmap iris.lifting.
Require Export iris.weakestpre barrier.heap_lang_tactics.
Import uPred.
Import heap_lang.
Local Hint Extern 0 (reducible _ _) => do_step ltac:(eauto 2).
Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
Local Hint Extern 0 (head_reducible _ _) => do_step ltac:(eauto 2).
Section lifting.
Context {Σ : iFunctor}.
......@@ -16,84 +17,75 @@ Lemma wp_bind {E e} K Q :
Proof. apply wp_bind. Qed.
(** Base axioms for core primitives of the language: Stateful reductions. *)
Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 :
E1 ⊆ E2 → to_val e1 = None →
reducible e1 σ1 →
(∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → ef = None ∧ φ e2 σ2) →
pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2, (■ φ e2 σ2 ∧ ownP σ2) -★
pvs E1 E2 (wp E2 e2 Q))
⊑ wp E2 e1 Q.
Proof.
intros ? He Hsafe Hstep.
rewrite -(wp_lift_step E1 E2 (λ e' σ' ef, ef = None ∧ φ e' σ') _ _ σ1) //.
apply pvs_mono, sep_mono, later_mono; first done.
apply forall_mono=>e2; apply forall_mono=>σ2.
apply forall_intro=>ef; apply wand_intro_l.
rewrite always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[-> ?] /=.
by rewrite const_equiv // left_id wand_elim_r right_id.
Qed.
(* TODO RJ: Figure out some better way to make the
postcondition a predicate over a *location* *)
Lemma wp_alloc_pst E σ e v Q :
to_val e = Some v →
(ownP σ ★ ▷ (∀ l, ■(σ !! l = None) ∧ ownP (<[l:=v]>σ) -★ Q (LocV l)))
⊑ wp E (Alloc e) Q.
Proof.
intros; set (φ e' σ' := ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None).
rewrite -(wp_lift_step E E φ _ _ σ) // /φ; last by intros; inv_step; eauto.
intros; set (φ e' σ' ef := ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None
∧ ef = (None : option expr)).
rewrite -(wp_lift_step E E φ _ _ σ) // /φ; last (by intros; inv_step; eauto); [].
rewrite -pvs_intro. apply sep_mono, later_mono; first done.
apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
apply forall_intro=>e2; apply forall_intro=>σ2; apply forall_intro=>ef.
apply wand_intro_l.
rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[l [-> [-> ?]]].
by rewrite (forall_elim l) const_equiv // left_id wand_elim_r -wp_value'.
apply const_elim_l=>-[l [-> [-> [? ->]]]].
rewrite right_id (forall_elim l) const_equiv //.
by rewrite left_id wand_elim_r -wp_value'.
Qed.
Lemma wp_lift_atomic_det_step {E Q e1} σ1 v2 σ2 :
to_val e1 = None →
head_reducible e1 σ1 →
(∀ e' σ' ef, head_step e1 σ1 e' σ' ef → ef = None ∧ e' = of_val v2 ∧ σ' = σ2) →
(ownP σ1 ★ ▷ (ownP σ2 -★ Q v2)) ⊑ wp E e1 Q.
Proof.
intros He Hsafe Hstep.
rewrite -(wp_lift_step E E (λ e' σ' ef, ef = None ∧ e' = of_val v2 ∧ σ' = σ2) _ e1 σ1) //; last first.
{ intros. by apply Hstep, prim_head_step. }
{ by apply head_reducible_reducible. }
rewrite -pvs_intro. apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2'.
apply forall_intro=>ef; apply wand_intro_l.
rewrite always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[-> [-> ->]] /=.
rewrite -pvs_intro right_id -wp_value.
by rewrite wand_elim_r.
Qed.
Lemma wp_load_pst E σ l v Q :
σ !! l = Some v →
(ownP σ ★ ▷ (ownP σ -★ Q v)) ⊑ wp E (Load (Loc l)) Q.
Proof.
intros; rewrite -(wp_lift_step E E (λ e' σ', e' = of_val v ∧ σ' = σ)) //;
last by intros; inv_step; eauto.
rewrite -pvs_intro; apply sep_mono, later_mono; first done.
apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value.
intros; rewrite -(wp_lift_atomic_det_step σ v σ) //;
last (by intros; inv_step; eauto).
Qed.
Lemma wp_store_pst E σ l e v v' Q :
to_val e = Some v → σ !! l = Some v' →
(ownP σ ★ ▷ (ownP (<[l:=v]>σ) -★ Q LitUnitV)) ⊑ wp E (Store (Loc l) e) Q.
Proof.
intros.
rewrite -(wp_lift_step E E (λ e' σ', e' = LitUnit ∧ σ' = <[l:=v]>σ)) //;
rewrite -(wp_lift_atomic_det_step σ LitUnitV (<[l:=v]>σ)) //;
last by intros; inv_step; eauto.
rewrite -pvs_intro; apply sep_mono, later_mono; first done.
apply forall_intro=>e2; apply forall_intro=>σ2; apply wand_intro_l.
rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
Qed.
Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Q :
to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
(ownP σ ★ ▷ (ownP σ -★ Q LitFalseV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
Proof.
intros; rewrite -(wp_lift_step E E (λ e' σ', e' = LitFalse ∧ σ' = σ)) //;
intros; rewrite -(wp_lift_atomic_det_step σ LitFalseV σ) //;
last by intros; inv_step; eauto.
rewrite -pvs_intro; apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2; apply wand_intro_l.
rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
Qed.
Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Q :
to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
(ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Q LitTrueV)) ⊑ wp E (Cas (Loc l) e1 e2) Q.
Proof.
intros.
rewrite -(wp_lift_step E E (λ e' σ', e' = LitTrue ∧ σ' = <[l:=v2]>σ)) //;
rewrite -(wp_lift_atomic_det_step σ LitTrueV (<[l:=v2]>σ)) //;
last by intros; inv_step; eauto.
rewrite -pvs_intro; apply sep_mono, later_mono; first done.
apply forall_intro=>e2'; apply forall_intro=>σ2; apply wand_intro_l.
rewrite -pvs_intro always_and_sep_l' -associative -always_and_sep_l'.
apply const_elim_l=>-[-> ->]; by rewrite wand_elim_r -wp_value'.
Qed.
(** Base axioms for core primitives of the language: Stateless reductions *)
......@@ -107,6 +99,7 @@ Proof.
apply sep_intro_True_l; last done.
by rewrite -wp_value' //; apply const_intro.
Qed.
Lemma wp_lift_pure_step E (φ : expr → Prop) Q e1 :
to_val e1 = None →
(∀ σ1, reducible e1 σ1) →
......@@ -118,6 +111,7 @@ Proof.
apply impl_intro_l, const_elim_l=>-[-> ?] /=.
by rewrite const_equiv // left_id right_id.
Qed.
Lemma wp_rec E ef e v Q :
to_val e = Some v →
▷ wp E ef.[Rec ef, e /] Q ⊑ wp E (App (Rec ef) e) Q.
......@@ -126,6 +120,7 @@ Proof.
Q (App (Rec ef) e)) //=; last by intros; inv_step; eauto.
by apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
Qed.
Lemma wp_plus E n1 n2 Q :
▷ Q (LitNatV (n1 + n2)) ⊑ wp E (Plus (LitNat n1) (LitNat n2)) Q.
Proof.
......@@ -134,6 +129,7 @@ Proof.
apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
by rewrite -wp_value'.
Qed.
Lemma wp_le_true E n1 n2 Q :
n1 ≤ n2 →
▷ Q LitTrueV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
......@@ -143,6 +139,7 @@ Proof.
apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
by rewrite -wp_value'.
Qed.
Lemma wp_le_false E n1 n2 Q :
n1 > n2 →
▷ Q LitFalseV ⊑ wp E (Le (LitNat n1) (LitNat n2)) Q.
......@@ -152,6 +149,7 @@ Proof.
apply later_mono, forall_intro=>e2; apply impl_intro_l, const_elim_l=>->.
by rewrite -wp_value'.
Qed.
Lemma wp_fst E e1 v1 e2 v2 Q :
to_val e1 = Some v1 → to_val e2 = Some v2 →
▷Q v1 ⊑ wp E (Fst (Pair e1 e2)) Q.
......@@ -161,6 +159,7 @@ Proof.
apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
by rewrite -wp_value'.
Qed.
Lemma wp_snd E e1 v1 e2 v2 Q :
to_val e1 = Some v1 → to_val e2 = Some v2 →
▷ Q v2 ⊑ wp E (Snd (Pair e1 e2)) Q.
......@@ -170,6 +169,7 @@ Proof.
apply later_mono, forall_intro=>e2'; apply impl_intro_l, const_elim_l=>->.
by rewrite -wp_value'.
Qed.
Lemma wp_case_inl E e0 v0 e1 e2 Q :
to_val e0 = Some v0 →
▷ wp E e1.[e0/] Q ⊑ wp E (Case (InjL e0) e1 e2) Q.
......@@ -178,6 +178,7 @@ Proof.
(Case (InjL e0) e1 e2)) //=; last by intros; inv_step; eauto.
by apply later_mono, forall_intro=>e1'; apply impl_intro_l, const_elim_l=>->.
Qed.
Lemma wp_case_inr E e0 v0 e1 e2 Q :
to_val e0 = Some v0 →
▷ wp E e2.[e0/] Q ⊑ wp E (Case (InjR e0) e1 e2) Q.
......@@ -197,4 +198,5 @@ Proof.
* rewrite -wp_le_true; auto.
* rewrite -wp_le_false; auto with lia.
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