Skip to content
GitLab
Commit ac20161b authored by Ralf Jung's avatar Ralf Jung
Browse files

unseal the ownerships, now that ecancel respects Typeclasses Opaque

parent f50cfd4e
Hide whitespace changes
Inline Side-by-side
heap_lang/heap.v
View file @ ac20161b
......@@ -22,13 +22,9 @@ Definition of_heap : heapRA → state := omap (maybe Excl).
(* heap_mapsto is defined strongly opaquely, to prevent unification from
matching it against other forms of ownership. *)
Definition heap_mapsto_def `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
Definition heap_mapsto `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ :=
auth_own heap_name {[ l := Excl v ]}.
(* Perform sealing *)
Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
Definition heap_mapsto {Σ h} := proj1_sig heap_mapsto_aux Σ h.
Definition heap_mapsto_eq :
@heap_mapsto = @heap_mapsto_def := proj2_sig heap_mapsto_aux.
Typeclasses Opaque heap_mapsto.
Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
ownP (of_heap h).
......@@ -76,20 +72,20 @@ Section heap.
authG heap_lang Σ heapRA → nclose N ⊆ E →
ownP σ ⊑ (|={E}=> ∃ _ : heapG Σ, heap_ctx N ∧ Π★{map σ} heap_mapsto).
Proof.
intros. rewrite heap_mapsto_eq -{1}(from_to_heap σ). etrans.
intros. rewrite -{1}(from_to_heap σ). etrans.
{ rewrite [ownP _]later_intro.
apply (auth_alloc (ownP ∘ of_heap) E N (to_heap σ)); last done.
apply to_heap_valid. }
apply pvs_mono, exist_elim=> γ.
rewrite -(exist_intro (HeapG _ _ γ)); apply and_mono_r.
rewrite /heap_mapsto_def /heap_name.
rewrite /heap_mapsto /heap_name.
induction σ as [|l v σ Hl IH] using map_ind.
{ rewrite big_sepM_empty; apply True_intro. }
rewrite to_heap_insert big_sepM_insert //.
rewrite (map_insert_singleton_op (to_heap σ));
last rewrite lookup_fmap Hl; auto.
(* FIXME: investigate why we have to unfold auth_own here. *)
by rewrite auth_own_op IH auth_own_eq.
by rewrite auth_own_op IH.
Qed.
Context `{heapG Σ}.
......@@ -101,7 +97,7 @@ Section heap.
(** General properties of mapsto *)
Lemma heap_mapsto_disjoint l v1 v2 : (l ↦ v1 ★ l ↦ v2)%I ⊑ False.
Proof.
rewrite heap_mapsto_eq -auth_own_op auth_own_valid map_op_singleton.
rewrite -auth_own_op auth_own_valid map_op_singleton.
rewrite map_validI (forall_elim l) lookup_singleton.
by rewrite option_validI excl_validI.
Qed.
......@@ -113,7 +109,7 @@ Section heap.
P ⊑ (▷ ∀ l, l ↦ v -★ Φ (LocV l)) →
P ⊑ || Alloc e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ??? HP.
rewrite /heap_ctx /heap_inv=> ??? HP.
trans (|={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)))
......@@ -127,7 +123,7 @@ Section heap.
rewrite -(exist_intro (op {[ l := Excl v ]})).
repeat erewrite <-exist_intro by apply _; simpl.
rewrite -of_heap_insert left_id right_id.
ecancel [_ -★ Φ _]%I.
rewrite /heap_mapsto. ecancel [_ -★ Φ _]%I.
rewrite -(map_insert_singleton_op h); last by apply of_heap_None.
rewrite const_equiv ?left_id; last by apply (map_insert_valid h).
apply later_intro.
......@@ -138,7 +134,7 @@ Section heap.
P ⊑ (▷ l ↦ v ★ ▷ (l ↦ v -★ Φ v)) →
P ⊑ || Load (Loc l) @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ?? HPΦ.
rewrite /heap_ctx /heap_inv=> ?? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Excl v ]}; simpl; eauto with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
......@@ -156,7 +152,7 @@ Section heap.
P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v -★ Φ (LitV LitUnit))) →
P ⊑ || Store (Loc l) e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ??? HPΦ.
rewrite /heap_ctx /heap_inv=> ??? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v) l))
with N heap_name {[ l := Excl v' ]}; simpl; eauto with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
......@@ -175,7 +171,7 @@ Section heap.
P ⊑ (▷ l ↦ v' ★ ▷ (l ↦ v' -★ Φ (LitV (LitBool false)))) →
P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=>????? HPΦ.
rewrite /heap_ctx /heap_inv=>????? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) id)
with N heap_name {[ l := Excl v' ]}; simpl; eauto 10 with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
......@@ -193,7 +189,7 @@ Section heap.
P ⊑ (▷ l ↦ v1 ★ ▷ (l ↦ v2 -★ Φ (LitV (LitBool true)))) →
P ⊑ || Cas (Loc l) e1 e2 @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ???? HPΦ.
rewrite /heap_ctx /heap_inv=> ???? HPΦ.
apply (auth_fsa' heap_inv (wp_fsa _) (alter (λ _, Excl v2) l))
with N heap_name {[ l := Excl v1 ]}; simpl; eauto 10 with I.
rewrite HPΦ{HPΦ}; apply sep_mono_r, forall_intro=> h; apply wand_intro_l.
......
program_logic/auth.v
View file @ ac20161b
......@@ -13,12 +13,9 @@ Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
`{CMRAIdentity A, CMRADiscrete A} : authG Λ Σ A.
Proof. split; try apply _. apply: inGF_inG. Qed.
Definition auth_own_def `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
Definition auth_own `{authG Λ Σ A} (γ : gname) (a : A) : iPropG Λ Σ :=
own γ (◯ a).
(* Perform sealing *)
Definition auth_own_aux : { x | x = @auth_own_def }. by eexists. Qed.
Definition auth_own {Λ Σ A Ae a} := proj1_sig auth_own_aux Λ Σ A Ae a.
Definition auth_own_eq : @auth_own = @auth_own_def := proj2_sig auth_own_aux.
Typeclasses Opaque auth_own.
Definition auth_inv `{authG Λ Σ A}
(γ : gname) (φ : A → iPropG Λ Σ) : iPropG Λ Σ :=
......@@ -40,17 +37,17 @@ Section auth.
Implicit Types γ : gname.
Global Instance auth_own_ne n γ : Proper (dist n ==> dist n) (auth_own γ).
Proof. rewrite auth_own_eq; solve_proper. Qed.
Proof. solve_proper. Qed.
Global Instance auth_own_proper γ : Proper ((≡) ==> (≡)) (auth_own γ).
Proof. by rewrite auth_own_eq; solve_proper. Qed.
Proof. solve_proper. Qed.
Global Instance auth_own_timeless γ a : TimelessP (auth_own γ a).
Proof. rewrite auth_own_eq. apply _. Qed.
Proof. rewrite /auth_own. apply _. Qed.
Lemma auth_own_op γ a b :
auth_own γ (a ⋅ b) ≡ (auth_own γ a ★ auth_own γ b)%I.
Proof. by rewrite auth_own_eq /auth_own_def -own_op auth_frag_op. Qed.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Lemma auth_own_valid γ a : auth_own γ a ⊑ ✓ a.
Proof. by rewrite auth_own_eq /auth_own_def own_valid auth_validI. Qed.
Proof. by rewrite /auth_own own_valid auth_validI. Qed.
Lemma auth_alloc E N a :
✓ a → nclose N ⊆ E →
......@@ -63,13 +60,13 @@ Section auth.
trans (▷ auth_inv γ φ ★ auth_own γ a)%I.
{ rewrite /auth_inv -(exist_intro a) later_sep.
ecancel [▷ φ _]%I.
by rewrite -later_intro auth_own_eq -own_op auth_both_op. }
by rewrite -later_intro -own_op auth_both_op. }
rewrite (inv_alloc N) /auth_ctx pvs_frame_r. apply pvs_mono.
by rewrite always_and_sep_l.
Qed.
Lemma auth_empty γ E : True ⊑ (|={E}=> auth_own γ ∅).
Proof. by rewrite auth_own_eq -own_update_empty. Qed.
Proof. by rewrite -own_update_empty. Qed.
Lemma auth_opened E γ a :
(▷ auth_inv γ φ ★ auth_own γ a)
......@@ -78,7 +75,7 @@ Section auth.
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 auth_own_eq [(▷φ _ ★ _)%I]comm assoc -own_op.
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').
......@@ -94,7 +91,7 @@ Section auth.
(▷ φ (L a ⋅ a') ★ own γ (● (a ⋅ a') ⋅ ◯ a))
⊑ (|={E}=> ▷ auth_inv γ φ ★ auth_own γ (L a)).
Proof.
intros HL Hv. rewrite /auth_inv auth_own_eq -(exist_intro (L a ⋅ a')).
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.
......
program_logic/saved_prop.v
View file @ ac20161b
......@@ -8,15 +8,10 @@ Notation savedPropG Λ Σ :=
Instance inGF_savedPropG `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
Proof. apply: inGF_inG. Qed.
Definition saved_prop_own_def `{savedPropG Λ Σ}
Definition saved_prop_own `{savedPropG Λ Σ}
(γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
own γ (to_agree (Next (iProp_unfold P))).
(* Perform sealing *)
Definition saved_prop_own_aux : { x | x = @saved_prop_own_def }. by eexists. Qed.
Definition saved_prop_own {Λ Σ s} := proj1_sig saved_prop_own_aux Λ Σ s.
Definition saved_prop_own_eq :
@saved_prop_own = @saved_prop_own_def := proj2_sig saved_prop_own_aux.
Typeclasses Opaque saved_prop_own.
Instance: Params (@saved_prop_own) 4.
Section saved_prop.
......@@ -26,20 +21,20 @@ Section saved_prop.
Global Instance saved_prop_always_stable γ P :
AlwaysStable (saved_prop_own γ P).
Proof. by rewrite /AlwaysStable saved_prop_own_eq always_own. Qed.
Proof. by rewrite /AlwaysStable always_own. Qed.
Lemma saved_prop_alloc_strong N P (G : gset gname) :
True ⊑ pvs N N (∃ γ, ■ (γ ∉ G) ∧ saved_prop_own γ P).
Proof. by rewrite saved_prop_own_eq; apply own_alloc_strong. Qed.
Proof. by apply own_alloc_strong. Qed.
Lemma saved_prop_alloc N P :
True ⊑ pvs N N (∃ γ, saved_prop_own γ P).
Proof. by rewrite saved_prop_own_eq; apply own_alloc. Qed.
Proof. by apply own_alloc. Qed.
Lemma saved_prop_agree γ P Q :
(saved_prop_own γ P ★ saved_prop_own γ Q) ⊑ ▷ (P ≡ Q).
Proof.
rewrite saved_prop_own_eq -own_op own_valid agree_validI.
rewrite -own_op own_valid agree_validI.
rewrite agree_equivI later_equivI /=; apply later_mono.
rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
apply (eq_rewrite (iProp_unfold P) (iProp_unfold Q) (λ Q' : iPreProp Λ _,
......
program_logic/sts.v
View file @ ac20161b
......@@ -13,21 +13,13 @@ Instance inGF_stsG sts `{inGF Λ Σ (stsGF sts)}
`{Inhabited (sts.state sts)} : stsG Λ Σ sts.
Proof. split; try apply _. apply: inGF_inG. Qed.
Definition sts_ownS_def `{i : stsG Λ Σ sts} (γ : gname)
Definition sts_ownS `{i : stsG Λ Σ sts} (γ : gname)
(S : sts.states sts) (T : sts.tokens sts) : iPropG Λ Σ:=
own γ (sts_frag S T).
(* Perform sealing. *)
Definition sts_ownS_aux : { x | x = @sts_ownS_def }. by eexists. Qed.
Definition sts_ownS {Λ Σ sts i} := proj1_sig sts_ownS_aux Λ Σ sts i.
Definition sts_ownS_eq : @sts_ownS = @sts_ownS_def := proj2_sig sts_ownS_aux.
Definition sts_own_def `{i : stsG Λ Σ sts} (γ : gname)
Definition sts_own `{i : stsG Λ Σ sts} (γ : gname)
(s : sts.state sts) (T : sts.tokens sts) : iPropG Λ Σ :=
own γ (sts_frag_up s T).
(* Perform sealing. *)
Definition sts_own_aux : { x | x = @sts_own_def }. by eexists. Qed.
Definition sts_own {Λ Σ sts i} := proj1_sig sts_own_aux Λ Σ sts i.
Definition sts_own_eq : @sts_own = @sts_own_def := proj2_sig sts_own_aux.
Typeclasses Opaque sts_own sts_ownS.
Definition sts_inv `{i : stsG Λ Σ sts} (γ : gname)
(φ : sts.state sts → iPropG Λ Σ) : iPropG Λ Σ :=
......@@ -57,9 +49,9 @@ Section sts.
Proper (pointwise_relation _ (≡) ==> (≡)) (sts_inv γ).
Proof. solve_proper. Qed.
Global Instance sts_ownS_proper γ : Proper ((≡) ==> (≡) ==> (≡)) (sts_ownS γ).
Proof. rewrite sts_ownS_eq. solve_proper. Qed.
Proof. solve_proper. Qed.
Global Instance sts_own_proper γ s : Proper ((≡) ==> (≡)) (sts_own γ s).
Proof. rewrite sts_own_eq. solve_proper. Qed.
Proof. solve_proper. Qed.
Global Instance sts_ctx_ne n γ N :
Proper (pointwise_relation _ (dist n) ==> dist n) (sts_ctx γ N).
Proof. solve_proper. Qed.
......@@ -72,22 +64,17 @@ 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 ? ? ?. rewrite sts_ownS_eq. 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 →
sts_own γ s T1 ⊑ (|={E}=> sts_ownS γ S T2).
Proof.
intros ???. rewrite sts_ownS_eq sts_own_eq.
by apply own_update, sts_update_frag_up.
Qed.
Proof. intros ???. by apply own_update, sts_update_frag_up. Qed.
Lemma sts_ownS_op γ S1 S2 T1 T2 :
T1 ∩ T2 ⊆ ∅ → sts.closed S1 T1 → sts.closed S2 T2 →
sts_ownS γ (S1 ∩ S2) (T1 ∪ T2) ≡ (sts_ownS γ S1 T1 ★ sts_ownS γ S2 T2)%I.
Proof. intros. by rewrite sts_ownS_eq /sts_ownS_def -own_op sts_op_frag. Qed.
Proof. intros. by rewrite /sts_ownS -own_op sts_op_frag. Qed.
Lemma sts_alloc E N s :
nclose N ⊆ E →
......@@ -101,7 +88,7 @@ Section sts.
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. rewrite sts_own_eq.
ecancel [▷ φ _]%I.
by rewrite -later_intro -own_op sts_op_auth_frag_up; last set_solver. }
rewrite (inv_alloc N) /sts_ctx pvs_frame_r.
by rewrite always_and_sep_l.
......@@ -111,7 +98,7 @@ Section sts.
(▷ sts_inv γ φ ★ sts_ownS γ S T)
⊑ (|={E}=> ∃ s, ■ (s ∈ S) ★ ▷ φ s ★ own γ (sts_auth s T)).
Proof.
rewrite /sts_inv sts_ownS_eq later_exist sep_exist_r. apply exist_elim=>s.
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).
rewrite [(_ ★ ▷φ _)%I]comm -!assoc -own_op -[(▷φ _ ★ _)%I]comm.
......@@ -126,7 +113,7 @@ Section sts.
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 sts_own_eq -(exist_intro s') later_sep.
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.
......@@ -176,8 +163,5 @@ Section sts.
■ (sts.steps (s, T) (s', T')) ★ ▷ φ s' ★
(sts_own γ s' T' -★ Ψ x))) →
P ⊑ fsa E Ψ.
Proof.
rewrite sts_own_eq. intros. eapply sts_fsaS; try done; [].
by rewrite sts_ownS_eq sts_own_eq.
Qed.
Proof. by apply sts_fsaS. Qed.
End sts.
Supports Markdown
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