Commit e23aa096 authored by Robbert Krebbers's avatar Robbert Krebbers

Make file layout heap_lang consistent with auth.

parent 4e43a270
From heap_lang Require Export derived.
From program_logic Require Import ownership auth.
Import uPred.
(* TODO: The entire construction could be generalized to arbitrary languages that have
a finmap as their state. Or maybe even beyond "as their state", i.e. arbitrary
predicates over finmaps instead of just ownP. *)
Section heap.
Definition heapRA := mapRA loc (exclRA (leibnizC val)).
Context {Σ : iFunctorG} (HeapI : gid) `{!InG heap_lang Σ HeapI (authRA heapRA)}.
Context (N : namespace).
Implicit Types P : iPropG heap_lang Σ.
Implicit Types σ : state.
Implicit Types h g : heapRA.
Implicit Types γ : gname.
Definition heapRA := mapRA loc (exclRA (leibnizC val)).
Local Instance heap_auth : AuthInG heap_lang Σ HeapI heapRA.
Proof. split; intros; apply _. Qed.
Class HeapInG Σ (i : gid) := heap_inG :> InG heap_lang Σ i (authRA heapRA).
Instance heap_inG_auth `{HeapInG Σ i} : AuthInG heap_lang Σ i heapRA.
Proof. split; apply _. Qed.
Notation to_heap σ := (Excl <$> σ).
Definition from_heap : heapRA state :=
omap (λ e, if e is Excl v then Some v else None).
Definition to_heap : state heapRA := fmap Excl.
Definition from_heap : heapRA state := omap (maybe Excl).
Lemma from_to_heap σ : from_heap (to_heap σ) = σ.
Proof.
apply map_eq=>l. rewrite lookup_omap lookup_fmap.
(* FIXME RJ: To do case-analysis on σ !! l, I need to do this weird
"case _: ...". Neither destruct nor plain case work, I need the
one that generates an equality - but I do not need the equality.
This also happened in algebra/fin_maps.v. *)
by case _:(σ !! l)=>[v|] /=.
Qed.
Lemma from_to_heap σ : from_heap (to_heap σ) = σ.
Proof. apply map_eq=> l. rewrite lookup_omap lookup_fmap. by case (σ !! l). Qed.
(* TODO: Do we want to expose heap ownership based on the state, or the heapRA?
The former does not expose the annoying "Excl", so for now I am going for
that. We should be able to derive the lemmas we want for this, too. *)
Definition heap_own {Σ} (i : gid) `{HeapInG Σ i}
(γ : gname) (σ : state) : iPropG heap_lang Σ := auth_own i γ (to_heap σ).
Definition heap_mapsto {Σ} (i : gid) `{HeapInG Σ i}
(γ : gname) (l : loc) (v : val) : iPropG heap_lang Σ := heap_own i γ {[ l v ]}.
Definition heap_inv {Σ} (i : gid) `{HeapInG Σ i}
(h : heapRA) : iPropG heap_lang Σ := ownP (from_heap h).
Definition heap_ctx {Σ} (i : gid) `{HeapInG Σ i}
(γ : gname) (N : namespace) : iPropG heap_lang Σ := auth_ctx i γ N (heap_inv i).
(* TODO: Do we want to expose heap ownership based on the state, or the heapRA?
The former does not expose the annoying "Excl", so for now I am going for
that. We should be able to derive the lemmas we want for this, too. *)
Definition heap_own (γ : gname) (σ : state) : iPropG heap_lang Σ :=
auth_own HeapI γ (to_heap σ).
Definition heap_mapsto (γ : gname) (l : loc) (v : val) : iPropG heap_lang Σ :=
heap_own γ {[ l v ]}.
Definition heap_inv (h : heapRA) : iPropG heap_lang Σ :=
ownP (from_heap h).
Definition heap_ctx (γ : gname) : iPropG heap_lang Σ :=
auth_ctx HeapI γ N heap_inv.
Section heap.
Context {Σ : iFunctorG} (HeapI : gid) `{!HeapInG Σ HeapI}.
Implicit Types N : namespace.
Implicit Types P : iPropG heap_lang Σ.
Implicit Types σ : state.
Implicit Types h g : heapRA.
Implicit Types γ : gname.
Global Instance heap_inv_proper : Proper (() ==> ()) heap_inv.
Global Instance heap_inv_proper : Proper (() ==> ()) (heap_inv HeapI).
Proof.
move=>? ? EQ. rewrite /heap_inv /from_heap.
(* TODO I guess we need some lemma about omap? *)
Admitted. (* FIXME... I can't make progress otherwise... *)
Lemma heap_own_op γ σ1 σ2 :
(heap_own γ σ1 heap_own γ σ2)%I ((σ1 σ2) heap_own γ (σ1 σ2))%I.
(heap_own HeapI γ σ1 heap_own HeapI γ σ2)%I
( (σ1 σ2) heap_own HeapI γ (σ1 σ2))%I.
Proof. (* TODO. *)
Abort.
Lemma heap_own_mapsto γ σ l v :
(* TODO: Is this the best way to express "l ∉ dom σ"? *)
(heap_own γ σ heap_mapsto γ l v)%I ((σ !! l = None) heap_own γ (<[l:=v]>σ))%I.
(heap_own HeapI γ σ heap_mapsto HeapI γ l v)%I
( (σ !! l = None) heap_own HeapI γ (<[l:=v]>σ))%I.
Proof. (* TODO. *)
Abort.
(* TODO: Prove equivalence to a big sum. *)
Lemma heap_alloc σ :
ownP σ pvs N N ( γ, heap_ctx γ heap_own γ σ).
Lemma heap_alloc N σ :
ownP σ pvs N N ( γ, heap_ctx HeapI γ N heap_own HeapI γ σ).
Proof.
rewrite -{1}[σ]from_to_heap.
rewrite -(auth_alloc heap_inv N); first done.
rewrite -(auth_alloc _ N); first done.
move=>n l. rewrite lookup_fmap. by case _:(σ !! l)=>[v|] /=.
Qed.
Lemma wp_load_heap E γ σ l v P Q :
Lemma wp_load_heap N E γ σ l v P Q :
nclose N E
σ !! l = Some v
P heap_ctx γ
P (heap_own γ σ (heap_own γ σ - Q v))
P heap_ctx HeapI γ N
P (heap_own HeapI γ σ (heap_own HeapI γ σ - Q v))
P wp E (Load (Loc l)) Q.
Proof.
rewrite /heap_ctx /heap_own. intros HN Hl Hctx HP.
eapply (auth_fsa heap_inv (wp_fsa (Load _) _) (λ _, True) id).
eapply (auth_fsa (heap_inv HeapI) (wp_fsa (Load _) _) (λ _, True) id).
{ eassumption. } { eassumption. }
rewrite HP=>{HP Hctx HN}. apply sep_mono; first done.
apply forall_intro=>hf. apply wand_intro_l. rewrite /heap_inv.
......@@ -95,10 +90,10 @@ Section heap.
{ eexists. eauto. }
Qed.
Lemma wp_load E γ l v P Q :
Lemma wp_load N E γ l v P Q :
nclose N E
P heap_ctx γ
P (heap_mapsto γ l v (heap_mapsto γ l v - Q v))
P heap_ctx HeapI γ N
P (heap_mapsto HeapI γ l v (heap_mapsto HeapI γ l v - Q v))
P wp E (Load (Loc l)) Q.
Proof.
intros HN. rewrite /heap_mapsto. apply wp_load_heap; first done.
......
......@@ -10,7 +10,7 @@ Definition saved_prop_own {Λ Σ} (i : gid) `{SavedPropInG Λ Σ i}
own i γ (to_agree (Next (iProp_unfold P))).
Instance: Params (@saved_prop_own) 5.
Section stored_prop.
Section saved_prop.
Context `{SavedPropInG Λ Σ SPI}.
Implicit Types P Q : iPropG Λ Σ.
Implicit Types γ : gname.
......@@ -28,4 +28,4 @@ Section stored_prop.
apply (eq_rewrite (iProp_unfold P) (iProp_unfold Q) (λ Q' : iPreProp Λ _,
iProp_fold (iProp_unfold P) iProp_fold Q')%I); solve_ne || auto with I.
Qed.
End stored_prop.
End saved_prop.
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