Commit dcbf7d4c authored by Robbert Krebbers's avatar Robbert Krebbers

Improve class inference and imlicit arguments for FrameShiftAssertion.

parent 036278e5
......@@ -73,8 +73,7 @@ Section heap.
P wp E (Load (Loc l)) Q.
Proof.
rewrite /heap_ctx /heap_own. intros HN Hl Hctx HP.
eapply (auth_fsa (heap_inv HeapI) (wp_fsa _ _) id).
{ eassumption. } { eassumption. }
eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) id); simpl; eauto.
rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
rewrite -assoc. apply const_elim_sep_l=>Hv /=.
......@@ -84,9 +83,6 @@ Section heap.
case _:(hf !! l)=>[[?||]|]; by auto. }
apply later_mono, wand_intro_l. rewrite left_id const_equiv // left_id.
by rewrite -later_intro.
Unshelve.
(* TODO Make it so that this becomes a goal, not shelved. *)
{ eexists; eauto. }
Qed.
Lemma wp_load N E γ l v P Q :
......@@ -107,8 +103,7 @@ Section heap.
P wp E (Store (Loc l) e) Q.
Proof.
rewrite /heap_ctx /heap_own. intros HN Hval Hl Hctx HP.
eapply (auth_fsa (heap_inv HeapI) (wp_fsa _ _) (alter (λ _, Excl v) l)).
{ eassumption. } { eassumption. }
eapply (auth_fsa (heap_inv HeapI) (wp_fsa _) (alter (λ _, Excl v) l)); simpl; eauto.
rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
rewrite -assoc. apply const_elim_sep_l=>Hv /=.
......@@ -136,9 +131,6 @@ Section heap.
case (hf !! l')=>[[?||]|]; auto; contradiction.
- rewrite /from_heap /to_heap lookup_insert_ne // !lookup_omap !lookup_op !lookup_fmap.
rewrite lookup_insert_ne //.
Unshelve.
(* TODO Make it so that this becomes a goal, not shelved. *)
{ eexists; eauto. }
Qed.
Lemma wp_store N E γ l e v v' P Q :
......
......@@ -83,24 +83,28 @@ Section auth.
(* Notice how the user has to prove that `b⋅a'` is valid at all
step-indices. However, since A is timeless, that should not be
a restriction. *)
Lemma auth_fsa {X : Type} {FSA} (FSAs : FrameShiftAssertion (A:=X) FSA)
L `{!LocalUpdate Lv L} N E P (Q : X iPropG Λ Σ) γ a :
Lemma auth_fsa {B} (fsa : FSA Λ (globalF Σ) B) `{!FrameShiftAssertion fsaV fsa}
L `{!LocalUpdate Lv L} N E P (Q : B iPropG Λ Σ) γ a :
fsaV
nclose N E
P auth_ctx AuthI γ N φ
P (auth_own AuthI γ a ( a', ■✓(a a') ▷φ (a a') -
FSA (E nclose N) (λ x, (Lv a (L aa')) ▷φ (L a a') (auth_own AuthI γ (L a) - Q x))))
P FSA E Q.
P (auth_own AuthI γ a ( a',
(a a') φ (a a') -
fsa (E nclose N) (λ x,
(Lv a (L aa')) φ (L a a')
(auth_own AuthI γ (L a) - Q x))))
P fsa E Q.
Proof.
rewrite /auth_ctx=>HN Hinv Hinner.
eapply inv_fsa; [eassumption..|]. rewrite Hinner=>{Hinner Hinv P}.
rewrite /auth_ctx=>? HN Hinv Hinner.
eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P}.
apply wand_intro_l.
rewrite assoc auth_opened !pvs_frame_r !sep_exist_r.
apply fsa_strip_pvs; first done. apply exist_elim=>a'.
apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
rewrite (forall_elim a'). rewrite [(_ _)%I]comm.
(* Getting this wand eliminated is really annoying. *)
rewrite [(_ _)%I]comm -!assoc [(▷φ _ _ _)%I]assoc [(▷φ _ _)%I]comm.
rewrite wand_elim_r fsa_frame_l.
apply fsa_mono_pvs; first done. intros x. rewrite comm -!assoc.
apply (fsa_mono_pvs fsa)=> x. rewrite comm -!assoc.
apply const_elim_sep_l=>-[HL Hv].
rewrite assoc [(_ (_ - _))%I]comm -assoc.
rewrite auth_closing //; []. erewrite pvs_frame_l. apply pvs_mono.
......
......@@ -66,22 +66,24 @@ Lemma always_inv N P : (□ inv N P)%I ≡ inv N P.
Proof. by rewrite always_always. Qed.
(** Invariants can be opened around any frame-shifting assertion. *)
Lemma inv_fsa {A : Type} {FSA} (FSAs : FrameShiftAssertion (A:=A) FSA)
E N P (Q : A iProp Λ Σ) R :
Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}
E N P (Q : A iProp Λ Σ) R :
fsaV
nclose N E
R inv N P
R (P - FSA (E nclose N) (λ a, P Q a))
R FSA E Q.
R ( P - fsa (E nclose N) (λ a, P Q a))
R fsa E Q.
Proof.
move=>HN Hinv Hinner. rewrite -[R](idemp ()%I) {1}Hinv Hinner =>{Hinv Hinner R}.
intros ? HN Hinv Hinner.
rewrite -[R](idemp ()%I) {1}Hinv Hinner =>{Hinv Hinner R}.
rewrite always_and_sep_l /inv sep_exist_r. apply exist_elim=>i.
rewrite always_and_sep_l -assoc. apply const_elim_sep_l=>HiN.
rewrite -(fsa_trans3 E (E {[encode i]})) //; last by solve_elem_of+.
rewrite -(fsa_open_close E (E {[encode i]})) //; last by solve_elem_of+.
(* Add this to the local context, so that solve_elem_of finds it. *)
assert ({[encode i]} nclose N) by eauto.
rewrite (always_sep_dup (ownI _ _)).
rewrite {1}pvs_openI !pvs_frame_r.
apply pvs_mask_frame_mono ; [solve_elem_of..|].
apply pvs_mask_frame_mono; [solve_elem_of..|].
rewrite (comm _ (_)%I) -assoc wand_elim_r fsa_frame_l.
apply fsa_mask_frame_mono; [solve_elem_of..|]. intros a.
rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
......@@ -95,15 +97,14 @@ Lemma pvs_open_close E N P Q R :
R inv N P
R (P - pvs (E nclose N) (E nclose N) (P Q))
R pvs E E Q.
Proof. move=>HN ? ?. apply: (inv_fsa pvs_fsa); eassumption. Qed.
Proof. intros. by apply: (inv_fsa pvs_fsa); try eassumption. Qed.
Lemma wp_open_close E e N P (Q : val Λ iProp Λ Σ) R :
atomic e nclose N E
R inv N P
R (P - wp (E nclose N) e (λ v, P Q v))
R wp E e Q.
Proof.
move=>He HN ? ?. apply: (inv_fsa (wp_fsa e _)); eassumption. Qed.
Proof. intros. apply: (inv_fsa (wp_fsa e)); eassumption. Qed.
Lemma inv_alloc N P : P pvs N N (inv N P).
Proof. by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite. Qed.
......
......@@ -181,59 +181,42 @@ Qed.
End pvs.
(** * Frame Shift Assertions. *)
Section fsa.
Context {Λ : language} {Σ : iFunctor} {A : Type}.
Implicit Types P : iProp Λ Σ.
Implicit Types Q : A iProp Λ Σ.
(* Yes, the name is horrible...
Frame Shift Assertions take a mask and a predicate over some type (that's
their "postcondition"). They support weakening the mask, framing resources
into the postcondition, and composition witn mask-changing view shifts. *)
Class FrameShiftAssertion (FSA : coPset (A iProp Λ Σ) iProp Λ Σ) := {
fsa_mask_frame_mono E1 E2 Q Q' :> E1 E2
( a, Q a Q' a) FSA E1 Q FSA E2 Q';
fsa_trans3 E1 E2 Q : E2 E1
pvs E1 E2 (FSA E2 (λ a, pvs E2 E1 (Q a))) FSA E1 Q;
fsa_frame_r E P Q : (FSA E Q P) FSA E (λ a, Q a P)
Notation FSA Λ Σ A := (coPset (A iProp Λ Σ) iProp Λ Σ).
Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := {
fsa_mask_frame_mono E1 E2 Q Q' :
E1 E2 ( a, Q a Q' a) fsa E1 Q fsa E2 Q';
fsa_trans3 E Q : pvs E E (fsa E (λ a, pvs E E (Q a))) fsa E Q;
fsa_open_close E1 E2 Q :
fsaV E2 E1 pvs E1 E2 (fsa E2 (λ a, pvs E2 E1 (Q a))) fsa E1 Q;
fsa_frame_r E P Q : (fsa E Q P) fsa E (λ a, Q a P)
}.
Context FSA `{FrameShiftAssertion FSA}.
Lemma fsa_mono E Q Q' : ( a, Q a Q' a) FSA E Q FSA E Q'.
Section fsa.
Context {Λ Σ A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa}.
Implicit Types Q : A iProp Λ Σ.
Lemma fsa_mono E Q Q' : ( a, Q a Q' a) fsa E Q fsa E Q'.
Proof. apply fsa_mask_frame_mono; auto. Qed.
Lemma fsa_mask_weaken E1 E2 Q : E1 E2 FSA E1 Q FSA E2 Q.
Lemma fsa_mask_weaken E1 E2 Q : E1 E2 fsa E1 Q fsa E2 Q.
Proof. intros. apply fsa_mask_frame_mono; auto. Qed.
Lemma fsa_frame_l E P Q :
(P FSA E Q) FSA E (λ a, P Q a).
Proof.
rewrite comm fsa_frame_r. apply fsa_mono=>a.
by rewrite comm.
Qed.
Lemma fsa_strip_pvs E P Q : P FSA E Q pvs E E P FSA E Q.
Proof.
move=>->. rewrite -{2}fsa_trans3; last reflexivity.
apply pvs_mono, fsa_mono=>a. apply pvs_intro.
Qed.
Lemma fsa_mono_pvs E Q Q' : ( a, Q a pvs E E (Q' a)) FSA E Q FSA E Q'.
Lemma fsa_frame_l E P Q : (P fsa E Q) fsa E (λ a, P Q a).
Proof. rewrite comm fsa_frame_r. apply fsa_mono=>a. by rewrite comm. Qed.
Lemma fsa_strip_pvs E P Q : P fsa E Q pvs E E P fsa E Q.
Proof.
move=>HQ. rewrite -[FSA E Q']fsa_trans3; last reflexivity.
rewrite -pvs_intro. by apply fsa_mono.
move=>->. rewrite -{2}fsa_trans3.
apply pvs_mono, fsa_mono=>a; apply pvs_intro.
Qed.
Lemma fsa_mono_pvs E Q Q' : ( a, Q a pvs E E (Q' a)) fsa E Q fsa E Q'.
Proof. intros. rewrite -[fsa E Q']fsa_trans3 -pvs_intro. by apply fsa_mono. Qed.
End fsa.
(** View shifts are a FSA. *)
Section pvs_fsa.
Context {Λ : language} {Σ : iFunctor}.
Implicit Types P : iProp Λ Σ.
Implicit Types Q : () iProp Λ Σ.
Global Instance pvs_fsa : FrameShiftAssertion (λ E Q, pvs E E (Q ())).
Definition pvs_fsa {Λ Σ} : FSA Λ Σ () := λ E Q, pvs E E (Q ()).
Instance pvs_fsa_prf {Λ Σ} : FrameShiftAssertion True (@pvs_fsa Λ Σ).
Proof.
split; intros.
- apply pvs_mask_frame_mono; auto.
- apply pvs_trans3; auto.
- apply pvs_frame_r; auto.
rewrite /pvs_fsa.
split; auto using pvs_mask_frame_mono, pvs_trans3, pvs_frame_r.
Qed.
End pvs_fsa.
......@@ -231,12 +231,10 @@ Lemma wp_mask_weaken E1 E2 e Q : E1 ⊆ E2 → wp E1 e Q ⊑ wp E2 e Q.
Proof. auto using wp_mask_frame_mono. Qed.
(** * Weakest-pre is a FSA. *)
Global Instance wp_fsa e : atomic e FrameShiftAssertion (λ E Q, wp E e Q).
Definition wp_fsa (e : expr Λ) : FSA Λ Σ (val Λ) := λ E, wp E e.
Global Instance wp_fsa_prf : FrameShiftAssertion (atomic e) (wp_fsa e).
Proof.
split; intros.
- apply wp_mask_frame_mono; auto.
- apply wp_atomic; auto.
- apply wp_frame_r; auto.
rewrite /wp_fsa; split; auto using wp_mask_frame_mono, wp_atomic, wp_frame_r.
intros E Q. by rewrite -(pvs_wp E e Q) -(wp_pvs E e Q).
Qed.
End wp.
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