Commit 358b3e1d by Robbert Krebbers

### Use pvs notation everywhere.

parent 611ad992
 ... ... @@ -65,7 +65,7 @@ Section heap. (** Allocation *) Lemma heap_alloc E N σ : authG heap_lang Σ heapRA → nclose N ⊆ E → ownP σ ⊑ pvs E E (∃ (_ : heapG Σ), heap_ctx N ∧ Π★{map σ} heap_mapsto). ownP σ ⊑ (|={E}=> ∃ (_ : heapG Σ), heap_ctx N ∧ Π★{map σ} heap_mapsto). Proof. intros. rewrite -{1}(from_to_heap σ). etransitivity. { rewrite [ownP _]later_intro. ... ... @@ -103,7 +103,7 @@ Section heap. P ⊑ wp E (Alloc e) Φ. Proof. rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP. transitivity (pvs E E (auth_own heap_name ∅ ★ P))%I. transitivity (|={E}=> auth_own heap_name ∅ ★ P)%I. { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. } apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e))) with N heap_name ∅; simpl; eauto with I. ... ...
 ... ... @@ -43,7 +43,7 @@ Section auth. Lemma auth_alloc E N a : ✓ a → nclose N ⊆ E → ▷ φ a ⊑ pvs E E (∃ γ, auth_ctx γ N φ ∧ auth_own γ a). ▷ φ 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) N). } ... ... @@ -58,12 +58,12 @@ Section auth. by rewrite always_and_sep_l. Qed. Lemma auth_empty γ E : True ⊑ pvs E E (auth_own γ ∅). Lemma auth_empty γ E : True ⊑ (|={E}=> auth_own γ ∅). Proof. by rewrite /auth_own -own_update_empty. Qed. Lemma auth_opened E γ a : (▷ auth_inv γ φ ★ auth_own γ a) ⊑ pvs E E (∃ a', ■ ✓ (a ⋅ a') ★ ▷ φ (a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ 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 [(▷(_ ∧ _))%I]pvs_timeless !pvs_frame_r. apply pvs_mono. ... ... @@ -83,7 +83,7 @@ Section auth. Lemma auth_closing `{!LocalUpdate Lv L} E γ a a' : Lv a → ✓ (L a ⋅ a') → (▷ φ (L a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a)) ⊑ pvs E E (▷ auth_inv γ φ ★ auth_own γ (L a)). ⊑ (|={E}=> ▷ auth_inv γ φ ★ auth_own γ (L a)). Proof. intros HL Hv. rewrite /auth_inv /auth_own -(exist_intro (L a ⋅ a')). rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc. ... ...
 ... ... @@ -91,7 +91,7 @@ Proof. by rewrite /AlwaysStable always_own_unit. Qed. (* TODO: This also holds if we just have ✓ a at the current step-idx, as Iris assertion. However, the map_updateP_alloc does not suffice to show this. *) Lemma own_alloc_strong a E (G : gset gname) : ✓ a → True ⊑ pvs E E (∃ γ, ■(γ ∉ G) ∧ own γ a). ✓ a → True ⊑ (|={E}=> ∃ γ, ■(γ ∉ G) ∧ own γ a). Proof. intros Ha. rewrite -(pvs_mono _ _ (∃ m, ■ (∃ γ, γ ∉ G ∧ m = to_globalF γ a) ∧ ownG m)%I). ... ... @@ -101,14 +101,14 @@ Proof. - apply exist_elim=>m; apply const_elim_l=>-[γ [Hfresh ->]]. by rewrite -(exist_intro γ) const_equiv. Qed. Lemma own_alloc a E : ✓ a → True ⊑ pvs E E (∃ γ, own γ a). Lemma own_alloc a E : ✓ a → True ⊑ (|={E}=> ∃ γ, own γ a). Proof. intros Ha. rewrite (own_alloc_strong a E ∅) //; []. apply pvs_mono. apply exist_mono=>?. eauto with I. Qed. Lemma own_updateP P γ a E : a ~~>: P → own γ a ⊑ pvs E E (∃ a', ■ P a' ∧ own γ a'). a ~~>: P → own γ a ⊑ (|={E}=> ∃ a', ■ P a' ∧ own γ a'). Proof. intros Ha. rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I). ... ... @@ -120,7 +120,7 @@ Proof. Qed. Lemma own_updateP_empty `{Empty A, !CMRAIdentity A} P γ E : ∅ ~~>: P → True ⊑ pvs E E (∃ a, ■ P a ∧ own γ a). ∅ ~~>: P → True ⊑ (|={E}=> ∃ a, ■ P a ∧ own γ a). Proof. intros Hemp. rewrite -(pvs_mono _ _ (∃ m, ■ (∃ a', m = to_globalF γ a' ∧ P a') ∧ ownG m)%I). ... ... @@ -131,14 +131,14 @@ Proof. rewrite -(exist_intro a'). by apply and_intro; [apply const_intro|]. Qed. Lemma own_update γ a a' E : a ~~> a' → own γ a ⊑ pvs E E (own γ a'). Lemma own_update γ a a' E : a ~~> a' → own γ a ⊑ (|={E}=> own γ a'). Proof. intros; rewrite (own_updateP (a' =)); last by apply cmra_update_updateP. by apply pvs_mono, exist_elim=> a''; apply const_elim_l=> ->. Qed. Lemma own_update_empty `{Empty A, !CMRAIdentity A} γ E : True ⊑ pvs E E (own γ ∅). True ⊑ (|={E}=> own γ ∅). Proof. rewrite (own_updateP_empty (∅ =)); last by apply cmra_updateP_id. apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->. ... ...
 ... ... @@ -58,7 +58,7 @@ Lemma pvs_open_close E N P Q R : nclose N ⊆ E → R ⊑ inv N P → R ⊑ (▷ P -★ pvs (E ∖ nclose N) (E ∖ nclose N) (▷ P ★ Q)) → R ⊑ pvs E E Q. R ⊑ (|={E}=> Q). Proof. intros. by apply: (inv_fsa pvs_fsa). Qed. Lemma wp_open_close E e N P Φ R : ... ...
 ... ... @@ -23,8 +23,8 @@ Lemma wp_lift_step E1 E2 E1 ⊆ E2 → to_val e1 = None → reducible e1 σ1 → (∀ e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef → φ e2 σ2 ef) → pvs E2 E1 (ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ∧ ownP σ2) -★ pvs E1 E2 (wp E2 e2 Φ ★ wp_fork ef)) (|={E2,E1}=> ownP σ1 ★ ▷ ∀ e2 σ2 ef, (■ φ e2 σ2 ef ∧ ownP σ2) -★ |={E1,E2}=> wp E2 e2 Φ ★ wp_fork ef) ⊑ wp E2 e1 Φ. Proof. intros ? He Hsafe Hstep n r ? Hvs; constructor; auto. ... ...
 ... ... @@ -203,7 +203,7 @@ Notation FSA Λ Σ A := (coPset → (A → iProp Λ Σ) → iProp Λ Σ). Class FrameShiftAssertion {Λ Σ A} (fsaV : Prop) (fsa : FSA Λ Σ A) := { fsa_mask_frame_mono E1 E2 Φ Ψ : E1 ⊆ E2 → (∀ a, Φ a ⊑ Ψ a) → fsa E1 Φ ⊑ fsa E2 Ψ; fsa_trans3 E Φ : pvs E E (fsa E (λ a, |={E}=> Φ a)) ⊑ fsa E Φ; fsa_trans3 E Φ : (|={E}=> fsa E (λ a, |={E}=> Φ a)) ⊑ fsa E Φ; fsa_open_close E1 E2 Φ : fsaV → E2 ⊆ E1 → (|={E1,E2}=> fsa E2 (λ a, |={E2,E1}=> Φ a)) ⊑ fsa E1 Φ; fsa_frame_r E P Φ : (fsa E Φ ★ P) ⊑ fsa E (λ a, Φ a ★ P) ... ...
 ... ... @@ -55,12 +55,12 @@ Section sts. sts_frag_included. *) Lemma sts_ownS_weaken E γ S1 S2 T1 T2 : T1 ≡ T2 → S1 ⊆ S2 → sts.closed S2 T2 → sts_ownS γ S1 T1 ⊑ pvs E E (sts_ownS γ S2 T2). sts_ownS γ S1 T1 ⊑ (|={E}=> sts_ownS γ S2 T2). Proof. intros -> ? ?. by apply own_update, sts_update_frag. Qed. Lemma sts_own_weaken E γ s S T1 T2 : T1 ≡ T2 → s ∈ S → sts.closed S T2 → sts_own γ s T1 ⊑ pvs E E (sts_ownS γ S T2). sts_own γ s T1 ⊑ (|={E}=> sts_ownS γ S T2). Proof. intros -> ??. by apply own_update, sts_update_frag_up. Qed. Lemma sts_ownS_op γ S1 S2 T1 T2 : ... ... @@ -70,7 +70,7 @@ Section sts. Lemma sts_alloc E N s : nclose N ⊆ E → ▷ φ s ⊑ pvs E E (∃ γ, sts_ctx γ N φ ∧ sts_own γ s (⊤ ∖ sts.tok s)). ▷ φ 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)) N). ... ... @@ -88,7 +88,7 @@ Section sts. Lemma sts_opened E γ S T : (▷ sts_inv γ φ ★ sts_ownS γ S T) ⊑ pvs E E (∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)). ⊑ (|={E}=> ∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)). Proof. rewrite /sts_inv /sts_ownS later_exist sep_exist_r. apply exist_elim=>s. rewrite later_sep pvs_timeless !pvs_frame_r. apply pvs_mono. ... ... @@ -104,13 +104,13 @@ Section sts. Lemma sts_closing E γ s T s' T' : sts.step (s, T) (s', T') → (▷ φ s' ★ own γ (sts_auth s T)) ⊑ pvs E E (▷ sts_inv γ φ ★ sts_own γ s' T'). (▷ φ s' ★ own γ (sts_auth s T)) ⊑ (|={E}=> ▷ sts_inv γ φ ★ sts_own γ s' T'). Proof. intros Hstep. rewrite /sts_inv /sts_own -(exist_intro s'). rewrite later_sep [(_ ★ ▷φ _)%I]comm -assoc. rewrite -pvs_frame_l. apply sep_mono_r. rewrite -later_intro. rewrite own_valid_l discrete_validI. apply const_elim_sep_l=>Hval. transitivity (pvs E E (own γ (sts_auth s' T'))). transitivity (|={E}=> own γ (sts_auth s' T'))%I. { by apply own_update, sts_update_auth. } by rewrite -own_op sts_op_auth_frag_up; last by inversion_clear Hstep. Qed. ... ...
 ... ... @@ -21,7 +21,7 @@ Record wp_go {Λ Σ} (E : coPset) (Φ Φfork : expr Λ → nat → iRes Λ Σ }. CoInductive wp_pre {Λ Σ} (E : coPset) (Φ : val Λ → iProp Λ Σ) : expr Λ → nat → iRes Λ Σ → Prop := | wp_pre_value n r v : pvs E E (Φ v) n r → wp_pre E Φ (of_val v) n r | wp_pre_value n r v : (|={E}=> Φ v)%I n r → wp_pre E Φ (of_val v) n r | wp_pre_step n r1 e1 : to_val e1 = None → (∀ rf k Ef σ1, ... ... @@ -95,7 +95,7 @@ Proof. exists r2, r2'; split_ands; [rewrite HE'|eapply IH|]; eauto. Qed. Lemma wp_value_inv E Φ v n r : wp E (of_val v) Φ n r → pvs E E (Φ v) n r. Lemma wp_value_inv E Φ v n r : wp E (of_val v) Φ n r → (|={E}=> Φ v)%I n r. Proof. by inversion 1 as [|??? He]; [|rewrite ?to_of_val in He]; simplify_eq. Qed. ... ... @@ -107,7 +107,7 @@ Proof. intros He; destruct 3; [by rewrite ?to_of_val in He|eauto]. Qed. Lemma wp_value' E Φ v : Φ v ⊑ wp E (of_val v) Φ. Proof. by constructor; apply pvs_intro. Qed. Lemma pvs_wp E e Φ : pvs E E (wp E e Φ) ⊑ wp E e Φ. Lemma pvs_wp E e Φ : (|={E}=> wp E e Φ) ⊑ wp E e Φ. Proof. intros n r ? Hvs. destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|]. ... ... @@ -117,7 +117,7 @@ Proof. destruct (Hvs rf (S k) Ef σ1) as (r'&Hwp&?); auto. eapply wp_step_inv with (S k) r'; eauto. Qed. Lemma wp_pvs E e Φ : wp E e (λ v, pvs E E (Φ v)) ⊑ wp E e Φ. Lemma wp_pvs E e Φ : wp E e (λ v, |={E}=> Φ v) ⊑ wp E e Φ. Proof. intros n r; revert e r; induction n as [n IH] using lt_wf_ind=> e r Hr HΦ. destruct (to_val e) as [v|] eqn:He; [apply of_to_val in He; subst|]. ... ... @@ -129,7 +129,7 @@ Proof. exists r2, r2'; split_ands; [|apply (IH k)|]; auto. Qed. Lemma wp_atomic E1 E2 e Φ : E2 ⊆ E1 → atomic e → pvs E1 E2 (wp E2 e (λ v, pvs E2 E1 (Φ v))) ⊑ wp E1 e Φ. E2 ⊆ E1 → atomic e → (|={E1,E2}=> wp E2 e (λ v, |={E2,E1}=> Φ v)) ⊑ wp E1 e Φ. Proof. intros ? He n r ? Hvs; constructor; eauto using atomic_not_val. intros rf k Ef σ1 ???. ... ... @@ -201,11 +201,11 @@ Proof. by apply wp_mask_frame_mono. Qed. Global Instance wp_mono' E e : Proper (pointwise_relation _ (⊑) ==> (⊑)) (@wp Λ Σ E e). Proof. by intros Φ Φ' ?; apply wp_mono. Qed. Lemma wp_strip_pvs E e P Φ : P ⊑ wp E e Φ → pvs E E P ⊑ wp E e Φ. Lemma wp_strip_pvs E e P Φ : P ⊑ wp E e Φ → (|={E}=> P) ⊑ wp E e Φ. Proof. move=>->. by rewrite pvs_wp. Qed. Lemma wp_value E Φ e v : to_val e = Some v → Φ v ⊑ wp E e Φ. Proof. intros; rewrite -(of_to_val e v) //; by apply wp_value'. Qed. Lemma wp_value_pvs E Φ e v : to_val e = Some v → pvs E E (Φ v) ⊑ wp E e Φ. Lemma wp_value_pvs E Φ e v : to_val e = Some v → (|={E}=> Φ v) ⊑ wp E e Φ. Proof. intros. rewrite -wp_pvs. rewrite -wp_value //. Qed. Lemma wp_frame_l E e Φ R : (R ★ wp E e Φ) ⊑ wp E e (λ v, R ★ Φ v). Proof. setoid_rewrite (comm _ R); apply wp_frame_r. Qed. ... ...
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