Commit 497cb7fa authored by Robbert Krebbers's avatar Robbert Krebbers

Convert more stuff to the proofmode.

parent 4811ea4f
Pipeline #841 passed with stage
......@@ -144,10 +144,8 @@ Section heap.
Proof.
iIntros {??} "[#Hinv HΦ]". rewrite /heap_ctx.
iPvs (auth_empty heap_name) as "Hheap".
(* TODO: change [auth_fsa] to single turnstile and use [iApply] *)
apply (auth_fsa heap_inv (wp_fsa (Alloc e)))
with N heap_name ; simpl; eauto with I.
iFrame "Hheap". iIntros {h}. rewrite [ h]left_id.
iApply (auth_fsa heap_inv (wp_fsa (Alloc e)) _ N); simpl; eauto.
iFrame "Hinv Hheap". iIntros {h}. rewrite [ h]left_id.
iIntros "[% Hheap]". rewrite /heap_inv.
iApply wp_alloc_pst; first done. iFrame "Hheap". iNext.
iIntros {l} "[% Hheap]". iExists (op {[ l := Frac 1 (DecAgree v) ]}), _, _.
......@@ -164,9 +162,9 @@ Section heap.
WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
iIntros {?} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Frac q (DecAgree v) ]}; simpl; eauto.
iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
heap_name {[ l := Frac q (DecAgree v) ]}); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
iIntros "$". by iSplit.
......@@ -178,9 +176,9 @@ Section heap.
WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
iIntros {??} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l))
with N heap_name {[ l := Frac 1 (DecAgree v') ]}; simpl; eauto with I.
iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v)) l) _
N _ heap_name {[ l := Frac 1 (DecAgree v') ]}); simpl; eauto.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_store_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
......@@ -192,9 +190,9 @@ Section heap.
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
iIntros {????} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Frac q (DecAgree v') ]}; simpl; eauto 10.
iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (auth_fsa' heap_inv (wp_fsa _) id _ N _
heap_name {[ l := Frac q (DecAgree v') ]}); simpl; eauto 10.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_fail_pst _ (<[l:=v']>(of_heap h))); rewrite ?lookup_insert //.
rewrite of_heap_singleton_op //. iFrame "Hl". iNext.
iIntros "$". by iSplit.
......@@ -206,9 +204,9 @@ Section heap.
WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
iIntros {???} "[#Hh [Hl HΦ]]". rewrite /heap_ctx /heap_mapsto.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l))
with N heap_name {[ l := Frac 1 (DecAgree v1) ]}; simpl; eauto 10.
iFrame "Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Frac 1 (DecAgree v2)) l)
_ N _ heap_name {[ l := Frac 1 (DecAgree v1) ]}); simpl; eauto 10.
iFrame "Hh Hl". iIntros {h} "[% Hl]". rewrite /heap_inv.
iApply (wp_cas_suc_pst _ (<[l:=v1]>(of_heap h))); rewrite ?lookup_insert //.
rewrite alter_singleton insert_insert !of_heap_singleton_op; eauto.
iFrame "Hl". iNext. iIntros "$". iFrame "HΦ". iPureIntro; naive_solver.
......
From iris.algebra Require Export auth upred_tactics.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.proofmode Require Import invariants ghost_ownership.
Import uPred.
(* The CMRA we need. *)
......@@ -57,100 +58,56 @@ Section auth.
a nclose N E
φ a (|={E}=> γ, auth_ctx γ N φ auth_own γ a).
Proof.
intros Ha HN. eapply sep_elim_True_r.
{ by eapply (own_alloc (Auth (Excl a) a) E). }
rewrite pvs_frame_l. apply pvs_strip_pvs.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
trans ( auth_inv γ φ auth_own γ a)%I.
{ rewrite /auth_inv -(exist_intro a) later_sep.
ecancel [ φ _]%I.
by rewrite -later_intro -own_op auth_both_op. }
rewrite (inv_alloc N E) // /auth_ctx pvs_frame_r. apply pvs_mono.
by rewrite always_and_sep_l.
iIntros {??} "Hφ". rewrite /auth_own /auth_ctx.
iPvs (own_alloc (Auth (Excl a) a)) as {γ} "Hγ"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iPvs (inv_alloc N _ (auth_inv γ φ) with "-[Hγ']"); first done.
{ iNext. iExists a. by iFrame "Hφ". }
iPvsIntro; iExists γ; by iFrame "Hγ'".
Qed.
Lemma auth_empty γ E : True |={E}=> auth_own γ .
Proof. by rewrite -own_empty. Qed.
Lemma auth_opened E γ a :
( auth_inv γ φ auth_own γ a)
(|={E}=> a', (a a') φ (a a') own γ ( (a a') a)).
Proof.
rewrite /auth_inv. rewrite later_exist sep_exist_r. apply exist_elim=>b.
rewrite later_sep [( own _ _)%I]pvs_timeless !pvs_frame_r. apply pvs_mono.
rewrite own_valid_l discrete_valid -!assoc. apply const_elim_sep_l=>Hv.
rewrite [(▷φ _ _)%I]comm assoc -own_op.
rewrite own_valid_r auth_validI /= and_elim_l sep_exist_l sep_exist_r /=.
apply exist_elim=>a'.
rewrite left_id -(exist_intro a').
apply (eq_rewrite b (a a') (λ x, x φ x own γ ( x a))%I).
{ by move=>n x y /timeless_iff ->. }
{ by eauto with I. }
rewrite -valid_intro; last by apply Hv.
rewrite left_id comm. auto with I.
Qed.
Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' :
Lv a (L a a')
( φ (L a a') own γ ( (a a') a))
(|={E}=> auth_inv γ φ auth_own γ (L a)).
Proof.
intros HL Hv. rewrite /auth_inv -(exist_intro (L a a')).
(* TODO it would be really nice to use cancel here *)
rewrite later_sep [(_ ▷φ _)%I]comm -assoc.
rewrite -pvs_frame_l. apply sep_mono_r.
rewrite -later_intro -own_op.
by apply own_update, (auth_local_update_l L).
Qed.
Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
Lemma auth_fsa E N P (Ψ : V iPropG Λ Σ) γ a :
fsaV
nclose N E
P auth_ctx γ N φ
P ( auth_own γ a a',
(a a') φ (a a') -
fsa (E nclose N) (λ x, L Lv (Hup : LocalUpdate Lv L),
(Lv a (L a a')) φ (L a a')
(auth_own γ (L a) - Ψ x)))
P fsa E Ψ.
Lemma auth_fsa E N (Ψ : V iPropG Λ Σ) γ a :
fsaV nclose N E
(auth_ctx γ N φ auth_own γ a a',
(a a') φ (a a') -
fsa (E nclose N) (λ x, L Lv (Hup : LocalUpdate Lv L),
(Lv a (L a a')) φ (L a a')
(auth_own γ (L a) - Ψ x)))
fsa E Ψ.
Proof.
rewrite /auth_ctx=>? HN Hinv Hinner.
eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
apply wand_intro_l. rewrite assoc.
rewrite (pvs_timeless (E N)) pvs_frame_l pvs_frame_r.
apply (fsa_strip_pvs fsa).
rewrite (auth_opened (E N)) !pvs_frame_r !sep_exist_r.
apply (fsa_strip_pvs fsa). apply exist_elim=>a'.
rewrite (forall_elim a'). rewrite [(_ _)%I]comm.
eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
{ rewrite assoc [(_ own _ _)%I]comm -assoc discrete_valid. done. }
rewrite fsa_frame_l.
apply (fsa_mono_pvs fsa)=> x.
rewrite sep_exist_l; apply exist_elim=> L.
rewrite sep_exist_l; apply exist_elim=> Lv.
rewrite sep_exist_l; apply exist_elim=> ?.
rewrite comm -!assoc. apply const_elim_sep_l=>-[HL Hv].
rewrite assoc [(_ (_ - _))%I]comm -assoc.
rewrite (auth_closing (E N)) //; [].
rewrite pvs_frame_l. apply pvs_mono.
by rewrite assoc [(_ _)%I]comm -assoc wand_elim_l.
iIntros {??} "(#? & Hγf & HΨ)". rewrite /auth_ctx /auth_own.
iInv N as {a'} "[Hγ Hφ]".
iTimeless "Hγ"; iTimeless "Hγf"; iCombine "Hγ" "Hγf" as "Hγ".
iDestruct (own_valid _ with "Hγ !") as "Hvalid".
iDestruct (auth_validI _ with "Hvalid") as "[Ha' %]"; simpl; iClear "Hvalid".
iDestruct "Ha'" as {b} "Ha'"; iDestruct "Ha'" as %Ha'.
rewrite ->(left_id _ _) in Ha'; setoid_subst.
iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ"; by iSplit. }
iIntros {v} "HL". iDestruct "HL" as {L Lv ?} "(% & Hφ & HΨ)".
iPvs (own_update _ with "Hγ") as "[Hγ Hγf]".
{ apply (auth_local_update_l L); tauto. }
iPvsIntro. iSplitL "Hφ Hγ"; last by iApply "HΨ".
iNext. iExists (L a b). by iFrame "Hφ".
Qed.
Lemma auth_fsa' L `{!LocalUpdate Lv L} E N P (Ψ : V iPropG Λ Σ) γ a :
fsaV
nclose N E
P auth_ctx γ N φ
P ( auth_own γ a ( a',
(a a') φ (a a') -
fsa (E nclose N) (λ x,
(Lv a (L a a')) φ (L a a')
(auth_own γ (L a) - Ψ x))))
P fsa E Ψ.
Lemma auth_fsa' L `{!LocalUpdate Lv L} E N (Ψ : V iPropG Λ Σ) γ a :
fsaV nclose N E
(auth_ctx γ N φ auth_own γ a ( a',
(a a') φ (a a') -
fsa (E nclose N) (λ x,
(Lv a (L a a')) φ (L a a')
(auth_own γ (L a) - Ψ x))))
fsa E Ψ.
Proof.
intros ??? HP. eapply auth_fsa with N γ a; eauto.
rewrite HP; apply sep_mono_r, forall_mono=> a'.
apply wand_mono; first done. apply (fsa_mono fsa)=> b.
rewrite -(exist_intro L). by repeat erewrite <-exist_intro by apply _.
iIntros {??} "(#Ha & Hγf & HΨ)"; iApply (auth_fsa E N Ψ γ a); auto.
iFrame "Ha Hγf". iIntros {a'} "H".
iApply fsa_wand_r; iSplitL; first by iApply "HΨ".
iIntros {v} "?"; by iExists L, Lv, _.
Qed.
End auth.
From iris.program_logic Require Export weakestpre viewshifts.
From iris.proofmode Require Import weakestpre.
From iris.proofmode Require Import weakestpre invariants.
Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
(e : expr Λ) (Φ : val Λ iProp Λ Σ) : iProp Λ Σ :=
......@@ -145,7 +145,6 @@ Lemma ht_inv N E P Φ R e :
(inv N R {{ R P }} e @ E nclose N {{ v, R Φ v }})
{{ P }} e @ E {{ Φ }}.
Proof.
iIntros {??} "[#? #Hwp] ! HP". eapply wp_inv; eauto.
iIntros "HR". iApply "Hwp". by iSplitL "HR".
iIntros {??} "[#? #Hwp] ! HP". iInv N as "HR". iApply "Hwp". by iSplitL "HR".
Qed.
End hoare.
From iris.algebra Require Export base.
From iris.program_logic Require Import ownership.
From iris.program_logic Require Export namespaces pviewshifts weakestpre.
From iris.program_logic Require Export namespaces.
From iris.proofmode Require Import pviewshifts.
Import uPred.
Local Hint Extern 100 (@eq coPset _ _) => set_solver.
Local Hint Extern 100 (@subseteq coPset _ _) => set_solver.
Local Hint Extern 100 (_ _) => set_solver.
Local Hint Extern 99 ({[ _ ]} _) => apply elem_of_subseteq_singleton.
(** Derived forms and lemmas about them. *)
Definition inv {Λ Σ} (N : namespace) (P : iProp Λ Σ) : iProp Λ Σ :=
......@@ -29,72 +25,22 @@ Proof. rewrite /inv; apply _. Qed.
Lemma always_inv N P : inv N P ⊣⊢ inv N P.
Proof. by rewrite always_always. Qed.
(** Invariants can be opened around any frame-shifting assertion. *)
Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ R :
fsaV nclose N E
R inv N P
R ( P - fsa (E nclose N) (λ a, P Ψ a))
R fsa E Ψ.
Proof.
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_open_close E (E {[encode i]})) //; last by set_solver+.
(* Add this to the local context, so that set_solver 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; [set_solver..|].
rewrite (comm _ (_)%I) -assoc wand_elim_r fsa_frame_l.
apply fsa_mask_frame_mono; [set_solver..|]. intros a.
rewrite assoc -always_and_sep_l pvs_closeI pvs_frame_r left_id.
apply pvs_mask_frame'; set_solver.
Qed.
Lemma inv_fsa_timeless {A} (fsa : FSA Λ Σ A)
`{!FrameShiftAssertion fsaV fsa} E N P `{!TimelessP P} Ψ R :
fsaV nclose N E
R inv N P
R (P - fsa (E nclose N) (λ a, P Ψ a))
R fsa E Ψ.
Proof.
intros ??? HR. eapply inv_fsa, wand_intro_l; eauto.
trans (|={E N}=> P R)%I; first by rewrite pvs_timeless pvs_frame_r.
apply (fsa_strip_pvs _). rewrite HR wand_elim_r.
apply: fsa_mono=> v. by rewrite -later_intro.
Qed.
(* Derive the concrete forms for pvs and wp, because they are useful. *)
Lemma pvs_inv E N P Q R :
nclose N E
R inv N P
R ( P - |={E nclose N}=> ( P Q))
R (|={E}=> Q).
Proof. intros. by apply: (inv_fsa pvs_fsa). Qed.
Lemma pvs_inv_timeless E N P `{!TimelessP P} Q R :
nclose N E
R inv N P
R (P - |={E nclose N}=> (P Q))
R (|={E}=> Q).
Proof. intros. by apply: (inv_fsa_timeless pvs_fsa). Qed.
Lemma wp_inv E e N P Φ R :
atomic e nclose N E
R inv N P
R ( P - WP e @ E nclose N {{ v, P Φ v }})
R WP e @ E {{ Φ }}.
Proof. intros. by apply: (inv_fsa (wp_fsa e)). Qed.
Lemma wp_inv_timeless E e N P `{!TimelessP P} Φ R :
atomic e nclose N E
R inv N P
R (P - WP e @ E nclose N {{ v, P Φ v }})
R WP e @ E {{ Φ }}.
Proof. intros. by apply: (inv_fsa_timeless (wp_fsa e)). Qed.
Lemma inv_alloc N E P : nclose N E P |={E}=> inv N P.
Proof.
intros. rewrite -(pvs_mask_weaken N) //.
by rewrite /inv (pvs_allocI N); last apply coPset_suffixes_infinite.
Qed.
(** Invariants can be opened around any frame-shifting assertion. *)
Lemma inv_fsa {A} (fsa : FSA Λ Σ A) `{!FrameShiftAssertion fsaV fsa} E N P Ψ :
fsaV nclose N E
(inv N P ( P - fsa (E nclose N) (λ a, P Ψ a))) fsa E Ψ.
Proof.
iIntros {??} "[#Hinv HΨ]"; rewrite /inv; iDestruct "Hinv" as {i} "[% Hi]".
iApply (fsa_open_close E (E {[encode i]})); auto; first by set_solver.
iPvs (pvs_openI' _ _ with "Hi") as "HP"; [set_solver..|iPvsIntro].
iApply (fsa_mask_weaken _ (E N)); first set_solver.
iApply fsa_wand_r; iSplitL; [by iApply "HΨ"|iIntros {v} "[HP HΨ]"].
iPvs (pvs_closeI' _ _ P with "[HP]"); [auto|by iSplit|set_solver|done].
Qed.
End inv.
From iris.algebra Require Export sts upred_tactics.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.proofmode Require Import invariants ghost_ownership.
Import uPred.
(** The CMRA we need. *)
......@@ -64,7 +65,7 @@ Section sts.
Lemma sts_ownS_weaken E γ S1 S2 T1 T2 :
T2 T1 S1 S2 sts.closed S2 T2
sts_ownS γ S1 T1 (|={E}=> sts_ownS γ S2 T2).
Proof. intros ? ? ?. by apply own_update, sts_update_frag. Qed.
Proof. intros ???. by apply own_update, sts_update_frag. Qed.
Lemma sts_own_weaken E γ s S T1 T2 :
T2 T1 s S sts.closed S T2
......@@ -80,86 +81,46 @@ Section sts.
nclose N E
φ s (|={E}=> γ, sts_ctx γ N φ sts_own γ s ( sts.tok s)).
Proof.
intros HN. eapply sep_elim_True_r.
{ apply (own_alloc (sts_auth s ( sts.tok s)) E).
apply sts_auth_valid; set_solver. }
rewrite pvs_frame_l. apply pvs_strip_pvs.
rewrite sep_exist_l. apply exist_elim=>γ. rewrite -(exist_intro γ).
trans ( sts_inv γ φ sts_own γ s ( sts.tok s))%I.
{ rewrite /sts_inv -(exist_intro s) later_sep.
ecancel [ φ _]%I.
by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
rewrite (inv_alloc N E) // /sts_ctx pvs_frame_r.
by rewrite always_and_sep_l.
Qed.
Lemma sts_opened E γ S T :
( sts_inv γ φ sts_ownS γ S T)
(|={E}=> s, (s S) φ s own γ (sts_auth s T)).
Proof.
rewrite /sts_inv later_exist sep_exist_r. apply exist_elim=>s.
rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono.
rewrite -(exist_intro s). ecancel [ φ _]%I.
rewrite -own_op own_valid_l discrete_valid.
apply const_elim_sep_l=> Hvalid.
assert (s S) by eauto using sts_auth_frag_valid_inv.
rewrite const_equiv // left_id sts_op_auth_frag //.
by assert ( sts_frag S T) as [??] by eauto using cmra_valid_op_r.
Qed.
Lemma sts_closing E γ s T s' T' :
sts.steps (s, T) (s', T')
( φ s' own γ (sts_auth s T)) (|={E}=> sts_inv γ φ sts_own γ s' T').
Proof.
intros Hstep. rewrite /sts_inv -(exist_intro s') later_sep.
(* TODO it would be really nice to use cancel here *)
rewrite [(_ φ _)%I]comm -assoc.
rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro.
rewrite own_valid_l discrete_valid. apply const_elim_sep_l=>Hval.
trans (|={E}=> own γ (sts_auth s' T'))%I.
{ by apply own_update, sts_update_auth. }
by rewrite -own_op sts_op_auth_frag_up.
iIntros {?} "Hφ". rewrite /sts_ctx /sts_own.
iPvs (own_alloc (sts_auth s ( sts.tok s))) as {γ} "Hγ".
{ apply sts_auth_valid; set_solver. }
iExists γ; iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ $]".
iPvs (inv_alloc N _ (sts_inv γ φ) with "[Hφ Hγ]") as "#?"; auto.
iNext. iExists s. by iFrame "Hφ".
Qed.
Context {V} (fsa : FSA Λ (globalF Σ) V) `{!FrameShiftAssertion fsaV fsa}.
Lemma sts_fsaS E N P (Ψ : V iPropG Λ Σ) γ S T :
Lemma sts_fsaS E N (Ψ : V iPropG Λ Σ) γ S T :
fsaV nclose N E
P sts_ctx γ N φ
P (sts_ownS γ S T s,
(s S) φ s -
fsa (E nclose N) (λ x, s' T',
sts.steps (s, T) (s', T') φ s'
(sts_own γ s' T' - Ψ x)))
P fsa E Ψ.
(sts_ctx γ N φ sts_ownS γ S T s,
(s S) φ s -
fsa (E nclose N) (λ x, s' T',
sts.steps (s, T) (s', T') φ s' (sts_own γ s' T' - Ψ x)))
fsa E Ψ.
Proof.
rewrite /sts_ctx=>? HN Hinv Hinner.
eapply (inv_fsa fsa); eauto. rewrite Hinner=>{Hinner Hinv P HN}.
apply wand_intro_l. rewrite assoc.
rewrite (sts_opened (E N)) !pvs_frame_r !sep_exist_r.
apply (fsa_strip_pvs fsa). apply exist_elim=>s.
rewrite (forall_elim s). rewrite [(_ _)%I]comm.
eapply wand_apply_r; first (by eapply (wand_frame_l (own γ _))); last first.
{ rewrite assoc [(_ own _ _)%I]comm -assoc. done. }
rewrite fsa_frame_l.
apply (fsa_mono_pvs fsa)=> x.
rewrite sep_exist_l; apply exist_elim=> s'.
rewrite sep_exist_l; apply exist_elim=>T'.
rewrite comm -!assoc. apply const_elim_sep_l=>-Hstep.
rewrite assoc [(_ (_ - _))%I]comm -assoc.
rewrite (sts_closing (E N)) //; [].
rewrite pvs_frame_l. apply pvs_mono.
by rewrite assoc [(_ _)%I]comm -assoc wand_elim_l.
iIntros {??} "(#? & Hγf & HΨ)". rewrite /sts_ctx /sts_ownS /sts_inv /sts_own.
iInv N as {s} "[Hγ Hφ]"; iTimeless "Hγ".
iCombine "Hγ" "Hγf" as "Hγ"; iDestruct (own_valid with "Hγ !") as %Hvalid.
assert (s S) by eauto using sts_auth_frag_valid_inv.
assert ( sts_frag S T) as [??] by eauto using cmra_valid_op_r.
iRevert "Hγ"; rewrite sts_op_auth_frag //; iIntros "Hγ".
iApply pvs_fsa_fsa; iApply fsa_wand_r; iSplitL "HΨ Hφ".
{ iApply "HΨ"; by iSplit. }
iIntros {a} "H"; iDestruct "H" as {s' T'} "(% & Hφ & HΨ)".
iPvs (own_update with "Hγ") as "Hγ"; first eauto using sts_update_auth.
iRevert "Hγ"; rewrite -sts_op_auth_frag_up; iIntros "[Hγ Hγf]".
iPvsIntro; iSplitL "Hφ Hγ"; last by iApply "HΨ".
iNext; iExists s'; by iFrame "Hφ".
Qed.
Lemma sts_fsa E N P (Ψ : V iPropG Λ Σ) γ s0 T :
Lemma sts_fsa E N (Ψ : V iPropG Λ Σ) γ s0 T :
fsaV nclose N E
P sts_ctx γ N φ
P (sts_own γ s0 T s,
(s sts.up s0 T) φ s -
fsa (E nclose N) (λ x, s' T',
(sts.steps (s, T) (s', T')) φ s'
(sts_own γ s' T' - Ψ x)))
P fsa E Ψ.
(sts_ctx γ N φ sts_own γ s0 T s,
(s sts.up s0 T) φ s -
fsa (E nclose N) (λ x, s' T',
(sts.steps (s, T) (s', T')) φ s'
(sts_own γ s' T' - Ψ x)))
fsa E Ψ.
Proof. by apply sts_fsaS. Qed.
End sts.
From iris.program_logic Require Import ownership.
From iris.program_logic Require Export pviewshifts invariants ghost_ownership.
From iris.proofmode Require Import pviewshifts.
From iris.proofmode Require Import pviewshifts invariants.
Import uPred.
Definition vs {Λ Σ} (E1 E2 : coPset) (P Q : iProp Λ Σ) : iProp Λ Σ :=
......@@ -94,8 +94,8 @@ Proof. intros; apply vs_mask_frame; set_solver. Qed.
Lemma vs_inv N E P Q R :
nclose N E (inv N R ( R P ={E nclose N}=> R Q)) (P ={E}=> Q).
Proof.
iIntros {?} "#[? Hvs] ! HP". eapply pvs_inv; eauto.
iIntros "HR". iApply ("Hvs" with "!"). by iSplitL "HR".
iIntros {?} "#[? Hvs] ! HP". iInv N as "HR".
iApply ("Hvs" with "!"). by iSplitL "HR".
Qed.
Lemma vs_alloc N P : P ={N}=> inv N P.
......
......@@ -14,7 +14,8 @@ Lemma tac_inv_fsa {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
envs_app false (Esnoc Enil i ( P)) Δ = Some Δ'
Δ' fsa (E nclose N) (λ a, P Φ a) Δ Q.
Proof.
intros ????? HΔ'. rewrite -(fsa_split Q). eapply (inv_fsa fsa); eauto.
intros ????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
rewrite // -always_and_sep_l. apply and_intro; first done.
rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
Qed.
......@@ -24,9 +25,12 @@ Lemma tac_inv_fsa_timeless {A} (fsa : FSA Λ Σ A) fsaV Δ Δ' E N i P Q Φ :
envs_app false (Esnoc Enil i P) Δ = Some Δ'
Δ' fsa (E nclose N) (λ a, P Φ a) Δ Q.
Proof.
intros ?????? HΔ'. rewrite -(fsa_split Q).
eapply (inv_fsa_timeless fsa); eauto.
rewrite envs_app_sound //; simpl. by rewrite right_id HΔ'.
intros ?????? HΔ'. rewrite -(fsa_split Q) -(inv_fsa fsa _ _ P) //.
rewrite // -always_and_sep_l. apply and_intro, wand_intro_l; first done.
trans (|={E N}=> P Δ)%I; first by rewrite pvs_timeless pvs_frame_r.
apply (fsa_strip_pvs _).
rewrite envs_app_sound //; simpl. rewrite right_id HΔ' wand_elim_r.
apply: fsa_mono=> v. by rewrite -later_intro.
Qed.
End invariants.
......
......@@ -18,7 +18,8 @@ Lemma tac_sts_fsa {A} (fsa : FSA Λ _ A) fsaV Δ E N i γ S T Q Φ :
sts.steps (s, T) (s', T') φ s' (sts_own γ s' T' - Φ a)))
Δ Q.
Proof.
intros ????? HΔ'. rewrite -(fsa_split Q); eapply (sts_fsaS φ fsa); eauto.
intros ????? HΔ'. rewrite -(fsa_split Q) -(sts_fsaS φ fsa) //.
rewrite // -always_and_sep_l. apply and_intro; first done.
rewrite envs_lookup_sound //; simpl; apply sep_mono_r.
apply forall_intro=>s; apply wand_intro_l.
rewrite -assoc; apply const_elim_sep_l=> Hs.
......
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