Commit d69ec6c4 authored by Ralf Jung's avatar Ralf Jung

make sealing naming consistent

parent e7667215
......@@ -27,11 +27,11 @@ Definition heap_mapsto_def `{heapG Σ} (l : loc) (v: val) : iPropG heap_lang Σ
(* Perform sealing *)
Module Type HeapMapstoSig.
Parameter heap_mapsto : `{heapG Σ} (l : loc) (v: val), iPropG heap_lang Σ.
Axiom heap_mapsto_def : @heap_mapsto = @heap_mapsto_def.
Axiom heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def.
End HeapMapstoSig.
Module Export HeapMapsto : HeapMapstoSig.
Definition heap_mapsto := @heap_mapsto_def.
Definition heap_mapsto_def := Logic.eq_refl (@heap_mapsto).
Definition heap_mapsto_eq := Logic.eq_refl (@heap_mapsto).
End HeapMapsto.
Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
......@@ -80,8 +80,7 @@ Section heap.
authG heap_lang Σ heapRA nclose N E
ownP σ (|={E}=> _ : heapG Σ, heap_ctx N Π★{map σ} heap_mapsto).
Proof.
rewrite heap_mapsto_def.
intros. rewrite -{1}(from_to_heap σ). etrans.
intros. rewrite heap_mapsto_eq -{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. }
......@@ -104,8 +103,7 @@ Section heap.
(** General properties of mapsto *)
Lemma heap_mapsto_disjoint l v1 v2 : (l v1 l v2)%I False.
Proof.
rewrite heap_mapsto_def.
rewrite -auto_own_op auto_own_valid map_op_singleton.
rewrite heap_mapsto_eq -auto_own_op auto_own_valid map_op_singleton.
rewrite map_validI (forall_elim l) lookup_singleton.
by rewrite option_validI excl_validI.
Qed.
......@@ -117,7 +115,7 @@ Section heap.
P ( l, l v - Φ (LocV l))
P || Alloc e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_def=> ?? Hctx HP.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ?? Hctx 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)))
......@@ -143,7 +141,7 @@ Section heap.
P ( l v (l v - Φ v))
P || Load (Loc l) @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_def=>HN ? HPΦ.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=>HN ? 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.
......@@ -161,7 +159,7 @@ Section heap.
P ( l v' (l v - Φ (LitV LitUnit)))
P || Store (Loc l) e @ E {{ Φ }}.
Proof.
rewrite /heap_ctx /heap_inv heap_mapsto_def=>? HN ? HPΦ.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=>? HN ? 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.
......@@ -181,7 +179,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_def=>??? HN ? HPΦ.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=>??? HN ? 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.
......@@ -200,7 +198,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_def=> ?? HN ? HPΦ.
rewrite /heap_ctx /heap_inv heap_mapsto_eq=> ?? HN ? 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.
......
......@@ -15,11 +15,11 @@ Definition saved_prop_own_def `{savedPropG Λ Σ}
Module Type SavedPropOwnSig.
Parameter saved_prop_own : `{savedPropG Λ Σ} (γ : gname) (P : iPropG Λ Σ),
iPropG Λ Σ.
Axiom saved_prop_own_def : @saved_prop_own = @saved_prop_own_def.
Axiom saved_prop_own_eq : @saved_prop_own = @saved_prop_own_def.
End SavedPropOwnSig.
Module Export SavedPropOwn : SavedPropOwnSig.
Definition saved_prop_own := @saved_prop_own_def.
Definition saved_prop_own_def := Logic.eq_refl (@saved_prop_own).
Definition saved_prop_own_eq := Logic.eq_refl (@saved_prop_own).
End SavedPropOwn.
Instance: Params (@saved_prop_own) 4.
......@@ -30,20 +30,20 @@ Section saved_prop.
Global Instance saved_prop_always_stable γ P :
AlwaysStable (saved_prop_own γ P).
Proof. by rewrite /AlwaysStable saved_prop_own_def always_own. Qed.
Proof. by rewrite /AlwaysStable saved_prop_own_eq 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_def; apply own_alloc_strong. Qed.
Proof. by rewrite saved_prop_own_eq; 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_def; apply own_alloc. Qed.
Proof. by rewrite saved_prop_own_eq; 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_def -own_op own_valid agree_validI.
rewrite saved_prop_own_eq -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 Λ _,
......
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