Commit e0d0f8dd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Restraint instance search for global functors.

Also, give all these global functors the suffix GF to avoid shadowing
such as we had with authF.

And add some type annotations for clarity.
parent 32daff99
...@@ -125,7 +125,7 @@ End barrier_proto. ...@@ -125,7 +125,7 @@ End barrier_proto.
Import barrier_proto. Import barrier_proto.
(* The functors we need. *) (* The functors we need. *)
Definition barrierFs := stsF sts `::` agreeF `::` pnil. Definition barrierGFs := stsGF sts `::` agreeF `::` pnil.
(** Now we come to the Iris part of the proof. *) (** Now we come to the Iris part of the proof. *)
Section proof. Section proof.
......
...@@ -26,7 +26,7 @@ Section client. ...@@ -26,7 +26,7 @@ Section client.
End client. End client.
Section ClosedProofs. Section ClosedProofs.
Definition Σ : iFunctorG := heapF .:: barrierFs .++ endF. Definition Σ : iFunctorG := heapGF .:: barrierGFs .++ endGF.
Notation iProp := (iPropG heap_lang Σ). Notation iProp := (iPropG heap_lang Σ).
Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}. Lemma client_safe_closed σ : {{ ownP σ : iProp }} client {{ λ v, True }}.
......
...@@ -7,8 +7,8 @@ Import uPred. ...@@ -7,8 +7,8 @@ Import uPred.
a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
predicates over finmaps instead of just ownP. *) predicates over finmaps instead of just ownP. *)
Definition heapRA := mapRA loc (exclRA (leibnizC val)). Definition heapRA : cmraT := mapRA loc (exclRA (leibnizC val)).
Definition heapF := authF heapRA. Definition heapGF : iFunctor := authGF heapRA.
Class heapG Σ := HeapG { Class heapG Σ := HeapG {
heap_inG : inG heap_lang Σ (authRA heapRA); heap_inG : inG heap_lang Σ (authRA heapRA);
...@@ -21,7 +21,7 @@ Definition to_heap : state → heapRA := fmap Excl. ...@@ -21,7 +21,7 @@ Definition to_heap : state → heapRA := fmap Excl.
Definition of_heap : heapRA state := omap (maybe Excl). Definition of_heap : heapRA state := omap (maybe Excl).
Definition heap_mapsto `{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 ]} : heapRA). auth_own heap_name {[ l := Excl v ]}.
Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ := Definition heap_inv `{i : heapG Σ} (h : heapRA) : iPropG heap_lang Σ :=
ownP (of_heap h). ownP (of_heap h).
Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ := Definition heap_ctx `{i : heapG Σ} (N : namespace) : iPropG heap_lang Σ :=
...@@ -104,7 +104,7 @@ Section heap. ...@@ -104,7 +104,7 @@ Section heap.
P || Alloc e @ E {{ Φ }}. P || Alloc e @ E {{ Φ }}.
Proof. Proof.
rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP. rewrite /heap_ctx /heap_inv /heap_mapsto=> ?? Hctx HP.
trans (|={E}=> auth_own heap_name ( : heapRA) P)%I. trans (|={E}=> auth_own heap_name P)%I.
{ by rewrite -pvs_frame_r -(auth_empty _ E) left_id. } { by rewrite -pvs_frame_r -(auth_empty _ E) left_id. }
apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e))) apply wp_strip_pvs, (auth_fsa heap_inv (wp_fsa (Alloc e)))
with N heap_name ; simpl; eauto with I. with N heap_name ; simpl; eauto with I.
......
...@@ -76,7 +76,7 @@ Section LiftingTests. ...@@ -76,7 +76,7 @@ Section LiftingTests.
End LiftingTests. End LiftingTests.
Section ClosedProofs. Section ClosedProofs.
Definition Σ : iFunctorG := heapF .:: endF. Definition Σ : iFunctorG := heapGF .:: endGF.
Notation iProp := (iPropG heap_lang Σ). Notation iProp := (iPropG heap_lang Σ).
Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}. Lemma heap_e_closed σ : {{ ownP σ : iProp }} heap_e {{ λ v, v = '2 }}.
......
...@@ -9,12 +9,10 @@ Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG { ...@@ -9,12 +9,10 @@ Class authG Λ Σ (A : cmraT) `{Empty A} := AuthG {
auth_timeless (a : A) :> Timeless a; auth_timeless (a : A) :> Timeless a;
}. }.
(* TODO: This shadows algebra.auth.authF. *) Definition authGF (A : cmraT) : iFunctor := constF (authRA A).
Definition authF (A : cmraT) := constF (authRA A). Instance authGF_inGF (A : cmraT) `{inGF Λ Σ (authGF A)}
`{CMRAIdentity A, a : A, Timeless a} : authG Λ Σ A.
Instance authG_inGF (A : cmraT) `{CMRAIdentity A} `{ a : A, Timeless a} Proof. split; try apply _. apply: inGF_inG. Qed.
`{inGF Λ Σ (authF A)} : authG Λ Σ A.
Proof. split; try apply _. move:(@inGF_inG Λ Σ (authF A)). auto. Qed.
Section definitions. Section definitions.
Context `{authG Λ Σ A} (γ : gname). Context `{authG Λ Σ A} (γ : gname).
......
...@@ -28,6 +28,30 @@ Typeclasses Opaque to_globalF own. ...@@ -28,6 +28,30 @@ Typeclasses Opaque to_globalF own.
Notation iPropG Λ Σ := (iProp Λ (globalF Σ)). Notation iPropG Λ Σ := (iProp Λ (globalF Σ)).
Notation iFunctorG := (gid iFunctor). Notation iFunctorG := (gid iFunctor).
(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
the functor breaks badly because Coq is unable to infer the correct
typeclasses, it does not unfold the functor. *)
Class inGF (Λ : language) (Σ : gid iFunctor) (F : iFunctor) := InGF {
inGF_id : gid;
inGF_prf : F = Σ inGF_id;
}.
(* Avoid eager type class search: this line ensures that type class search
is only triggered if the first two arguments of inGF do not contain evars. Since
instance search for [inGF] is restrained, instances should always have [inGF] as
their first argument to avoid loops. For example, the instances [authGF_inGF]
and [auth_identity] otherwise create a cycle that pops up arbitrarily. *)
Hint Mode inGF + + - : typeclass_instances.
Lemma inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
Proof. exists inGF_id. by rewrite -inGF_prf. Qed.
Instance inGF_here {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
Proof. by exists 0. Qed.
Instance inGF_further {Λ Σ} (F F': iFunctor) : inGF Λ Σ F inGF Λ (F' .:: Σ) F.
Proof. intros [i ?]. by exists (S i). Qed.
Definition endGF : iFunctorG := const (constF unitRA).
(** Properties about ghost ownership *)
Section global. Section global.
Context `{i : inG Λ Σ A}. Context `{i : inG Λ Σ A}.
Implicit Types a : A. Implicit Types a : A.
...@@ -145,22 +169,3 @@ Proof. ...@@ -145,22 +169,3 @@ Proof.
apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->. apply pvs_mono, exist_elim=>a. by apply const_elim_l=>->.
Qed. Qed.
End global. End global.
(** We need another typeclass to identify the *functor* in the Σ. Basing inG on
the functor breaks badly because Coq is unable to infer the correct
typeclasses, it does not unfold the functor. *)
Class inGF (Λ : language) (Σ : gid iFunctor) (F : iFunctor) := InGF {
inGF_id : gid;
inGF_prf : F = Σ inGF_id;
}.
Instance inGF_inG `{inGF Λ Σ F} : inG Λ Σ (F (laterC (iPreProp Λ (globalF Σ)))).
Proof. exists inGF_id. f_equal. apply inGF_prf. Qed.
Instance inGF_nil {Λ Σ} (F: iFunctor) : inGF Λ (F .:: Σ) F.
Proof. exists 0. done. Qed.
Instance inGF_cons `{inGF Λ Σ F} (F': iFunctor) : inGF Λ (F' .:: Σ) F.
Proof. exists (S inGF_id). apply inGF_prf. Qed.
Definition endF : gid iFunctor := const (constF unitRA).
...@@ -6,7 +6,7 @@ Notation savedPropG Λ Σ := ...@@ -6,7 +6,7 @@ Notation savedPropG Λ Σ :=
(inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))). (inG Λ Σ (agreeRA (laterC (iPreProp Λ (globalF Σ))))).
Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ. Instance savedPropG_inGF `{inGF Λ Σ agreeF} : savedPropG Λ Σ.
Proof. move:(@inGF_inG Λ Σ agreeF). auto. Qed. Proof. apply: inGF_inG. Qed.
Definition saved_prop_own `{savedPropG Λ Σ} Definition saved_prop_own `{savedPropG Λ Σ}
(γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ := (γ : gname) (P : iPropG Λ Σ) : iPropG Λ Σ :=
...@@ -18,11 +18,9 @@ Section saved_prop. ...@@ -18,11 +18,9 @@ Section saved_prop.
Implicit Types P Q : iPropG Λ Σ. Implicit Types P Q : iPropG Λ Σ.
Implicit Types γ : gname. Implicit Types γ : gname.
Global Instance : P, AlwaysStable (saved_prop_own γ P). Global Instance saved_prop_always_stable γ P :
Proof. AlwaysStable (saved_prop_own γ P).
intros. rewrite /AlwaysStable /saved_prop_own. Proof. by rewrite /AlwaysStable /saved_prop_own always_own. Qed.
rewrite always_own; done.
Qed.
Lemma saved_prop_alloc_strong N P (G : gset gname) : Lemma saved_prop_alloc_strong N P (G : gset gname) :
True pvs N N ( γ, (γ G) saved_prop_own γ P). True pvs N N ( γ, (γ G) saved_prop_own γ P).
......
...@@ -8,11 +8,10 @@ Class stsG Λ Σ (sts : stsT) := StsG { ...@@ -8,11 +8,10 @@ Class stsG Λ Σ (sts : stsT) := StsG {
}. }.
Coercion sts_inG : stsG >-> inG. Coercion sts_inG : stsG >-> inG.
Definition stsF (sts : stsT) := constF (stsRA sts). Definition stsGF (sts : stsT) : iFunctor := constF (stsRA sts).
Instance stsGF_inGF sts `{inGF Λ Σ (stsGF sts)}
Instance stsG_inGF sts `{Inhabited (sts.state sts)} `{Inhabited (sts.state sts)} : stsG Λ Σ sts.
`{inGF Λ Σ (stsF sts)} : stsG Λ Σ sts. Proof. split; try apply _. apply: inGF_inG. Qed.
Proof. split; try apply _. move:(@inGF_inG Λ Σ (stsF sts)). auto. Qed.
Section definitions. Section definitions.
Context `{i : stsG Λ Σ sts} (γ : gname). Context `{i : stsG Λ Σ sts} (γ : gname).
......
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