Commit 82ca2d04 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

Conflicts:
	docs/program-logic.tex
parents 0bd43b95 a0cf8fc5
Pipeline #2825 passed with stage
in 9 minutes and 20 seconds
...@@ -67,7 +67,7 @@ program_logic/model.v ...@@ -67,7 +67,7 @@ program_logic/model.v
program_logic/adequacy.v program_logic/adequacy.v
program_logic/lifting.v program_logic/lifting.v
program_logic/invariants.v program_logic/invariants.v
program_logic/ownership.v program_logic/wsat.v
program_logic/weakestpre.v program_logic/weakestpre.v
program_logic/pviewshifts.v program_logic/pviewshifts.v
program_logic/hoare.v program_logic/hoare.v
...@@ -78,6 +78,7 @@ program_logic/ectxi_language.v ...@@ -78,6 +78,7 @@ program_logic/ectxi_language.v
program_logic/ectx_lifting.v program_logic/ectx_lifting.v
program_logic/ghost_ownership.v program_logic/ghost_ownership.v
program_logic/saved_prop.v program_logic/saved_prop.v
program_logic/auth.v
program_logic/sts.v program_logic/sts.v
program_logic/namespaces.v program_logic/namespaces.v
program_logic/boxes.v program_logic/boxes.v
......
...@@ -96,7 +96,7 @@ The following assertion states that an invariant with name $\iname$ exists and m ...@@ -96,7 +96,7 @@ The following assertion states that an invariant with name $\iname$ exists and m
Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants: Next, we define \emph{view updates}, which are essentially the same as the resource updates of the base logic ($\Sref{sec:base-logic}$), except that they also have access to world satisfaction and can enable and disable invariants:
\[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \] \[ \pvs[\mask_1][\mask_2] \prop \eqdef W * \ownGhost{\gname_{\textmon{En}}}{\mask_1} \wand \upd\diamond (W * \ownGhost{\gname_{\textmon{En}}}{\mask_2} * \prop) \]
Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update. Here, $\mask_1$ and $\mask_2$ are the \emph{masks} of the view update, defining which invariants have to be (at least!) available before and after the update.
We use $\top$ as symbol for the largest possible mask, $\mathbb N$. We use $\top$ as symbol for the largest possible mask, $\mathbb N$, and $\bot$ for the smallest possible mask $\emptyset$.
We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$. We will write $\pvs[\mask] \prop$ for $\pvs[\mask][\mask]\prop$.
% %
View updates satisfy the following basic proof rules: View updates satisfy the following basic proof rules:
......
From iris.program_logic Require Export weakestpre adequacy. From iris.program_logic Require Export weakestpre adequacy.
From iris.heap_lang Require Export heap. From iris.heap_lang Require Export heap.
From iris.algebra Require Import auth. From iris.algebra Require Import auth.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import wsat auth.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Class heapPreG Σ := HeapPreG { Class heapPreG Σ := HeapPreG {
heap_preG_iris :> irisPreG heap_lang Σ; heap_preG_iris :> irisPreG heap_lang Σ;
heap_preG_heap :> inG Σ (authR heapUR) heap_preG_heap :> authG Σ heapUR
}. }.
Definition heapΣ : gFunctors := Definition heapΣ : gFunctors :=
#[irisΣ heap_lang; GFunctor (constRF (authR heapUR))]. #[irisΣ heap_lang; authΣ heapUR].
Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ. Instance subG_heapPreG {Σ} : subG heapΣ Σ heapPreG Σ.
Proof. intros [? ?%subG_inG]%subG_inv. split; apply _. Qed. Proof. intros [? ?]%subG_inv. split; apply _. Qed.
Definition heap_adequacy Σ `{heapPreG Σ} e σ φ : Definition heap_adequacy Σ `{heapPreG Σ} e σ φ :
( `{heapG Σ}, heap_ctx WP e {{ v, φ v }}) ( `{heapG Σ}, heap_ctx WP e {{ v, φ v }})
adequate e σ φ. adequate e σ φ.
Proof. Proof.
intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ". intros Hwp; eapply (wp_adequacy Σ); iIntros (?) "Hσ".
iVs (own_alloc ( to_heap σ)) as (γ) "Hh". iVs (auth_alloc to_heap _ heapN _ σ with "[Hσ]") as (γ) "[Hh _]";[|by iNext|].
{ apply (auth_auth_valid (to_heap _)), to_heap_valid. } { exact: to_heap_valid. }
set (Hheap := HeapG _ _ _ γ). set (Hheap := HeapG _ _ _ γ).
iVs (inv_alloc heapN _ heap_inv with "[-]"); [iNext; iExists σ; by iFrame|].
iApply (Hwp _). by rewrite /heap_ctx. iApply (Hwp _). by rewrite /heap_ctx.
Qed. Qed.
\ No newline at end of file
From iris.heap_lang Require Export lifting. From iris.heap_lang Require Export lifting.
From iris.algebra Require Import auth gmap frac dec_agree. From iris.algebra Require Import auth gmap frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership. From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import wsat auth.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
(* TODO: The entire construction could be generalized to arbitrary languages that have (* TODO: The entire construction could be generalized to arbitrary languages that have
...@@ -14,28 +14,26 @@ Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)). ...@@ -14,28 +14,26 @@ Definition heapUR : ucmraT := gmapUR loc (prodR fracR (dec_agreeR val)).
(** The CMRA we need. *) (** The CMRA we need. *)
Class heapG Σ := HeapG { Class heapG Σ := HeapG {
heapG_iris_inG :> irisG heap_lang Σ; heapG_iris_inG :> irisG heap_lang Σ;
heap_inG :> inG Σ (authR heapUR); heap_inG :> authG Σ heapUR;
heap_name : gname heap_name : gname
}. }.
(** The Functor we need. *)
Definition to_heap : state heapUR := fmap (λ v, (1%Qp, DecAgree v)). Definition to_heap : state heapUR := fmap (λ v, (1%Qp, DecAgree v)).
Section definitions. Section definitions.
Context `{heapG Σ}. Context `{heapG Σ}.
Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ := Definition heap_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
own heap_name ( {[ l := (q, DecAgree v) ]}). auth_own heap_name ({[ l := (q, DecAgree v) ]}).
Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed. Definition heap_mapsto_aux : { x | x = @heap_mapsto_def }. by eexists. Qed.
Definition heap_mapsto := proj1_sig heap_mapsto_aux. Definition heap_mapsto := proj1_sig heap_mapsto_aux.
Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def := Definition heap_mapsto_eq : @heap_mapsto = @heap_mapsto_def :=
proj2_sig heap_mapsto_aux. proj2_sig heap_mapsto_aux.
Definition heap_inv : iProp Σ := ( σ, ownP σ own heap_name ( to_heap σ))%I. Definition heap_ctx : iProp Σ := auth_ctx heap_name heapN to_heap ownP.
Definition heap_ctx : iProp Σ := inv heapN heap_inv.
End definitions. End definitions.
Typeclasses Opaque heap_ctx heap_mapsto. Typeclasses Opaque heap_ctx heap_mapsto.
Instance: Params (@heap_inv) 2.
Notation "l ↦{ q } v" := (heap_mapsto l q v) Notation "l ↦{ q } v" := (heap_mapsto l q v)
(at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope. (at level 20, q at level 50, format "l ↦{ q } v") : uPred_scope.
...@@ -79,8 +77,7 @@ Section heap. ...@@ -79,8 +77,7 @@ Section heap.
Lemma heap_mapsto_op_eq l q1 q2 v : l {q1} v l {q2} v l {q1+q2} v. Lemma heap_mapsto_op_eq l q1 q2 v : l {q1} v l {q2} v l {q1+q2} v.
Proof. Proof.
by rewrite heap_mapsto_eq by rewrite heap_mapsto_eq -auth_own_op op_singleton pair_op dec_agree_idemp.
-own_op -auth_frag_op op_singleton pair_op dec_agree_idemp.
Qed. Qed.
Lemma heap_mapsto_op l q1 q2 v1 v2 : Lemma heap_mapsto_op l q1 q2 v1 v2 :
...@@ -89,8 +86,8 @@ Section heap. ...@@ -89,8 +86,8 @@ Section heap.
destruct (decide (v1 = v2)) as [->|]. destruct (decide (v1 = v2)) as [->|].
{ by rewrite heap_mapsto_op_eq pure_equiv // left_id. } { by rewrite heap_mapsto_op_eq pure_equiv // left_id. }
apply (anti_symm ()); last by apply pure_elim_l. apply (anti_symm ()); last by apply pure_elim_l.
rewrite heap_mapsto_eq -own_op -auth_frag_op own_valid discrete_valid. rewrite heap_mapsto_eq -auth_own_op auth_own_valid discrete_valid.
eapply pure_elim; [done|]=> /auth_own_valid /=. eapply pure_elim; [done|] => /=.
rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros []. rewrite op_singleton pair_op dec_agree_ne // singleton_valid. by intros [].
Qed. Qed.
...@@ -112,14 +109,12 @@ Section heap. ...@@ -112,14 +109,12 @@ Section heap.
heap_ctx ( l, l v ={E}= Φ (LitV (LitLoc l))) WP Alloc e @ E {{ Φ }}. heap_ctx ( l, l v ={E}= Φ (LitV (LitLoc l))) WP Alloc e @ E {{ Φ }}.
Proof. Proof.
iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx. iIntros (<-%of_to_val ?) "[#Hinv HΦ]". rewrite /heap_ctx.
iInv heapN as (σ) ">[Hσ Hh] " "Hclose". iVs (auth_empty heap_name) as "Ha".
iVs (auth_open with "[$Hinv $Ha]") as (σ) "(%&Hσ&Hcl)"; first done.
iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !==>". iApply wp_alloc_pst. iFrame "Hσ". iNext. iIntros (l) "[% Hσ] !==>".
iVs (own_update with "Hh") as "[Hh H]". iVs ("Hcl" with "* [Hσ]") as "Ha".
{ apply auth_update_alloc, { iFrame. iPureIntro. rewrite to_heap_insert.
(alloc_singleton_local_update _ l (1%Qp,DecAgree v)); eapply alloc_singleton_local_update; by auto using lookup_to_heap_None. }
by auto using lookup_to_heap_None. }
iVs ("Hclose" with "[Hσ Hh]") as "_".
{ iNext. iExists (<[l:=v]> σ). rewrite to_heap_insert. by iFrame. }
iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def. iApply "HΦ". by rewrite heap_mapsto_eq /heap_mapsto_def.
Qed. Qed.
...@@ -130,11 +125,9 @@ Section heap. ...@@ -130,11 +125,9 @@ Section heap.
Proof. Proof.
iIntros (?) "[#Hinv [>Hl HΦ]]". iIntros (?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iInv heapN as (σ) ">[Hσ Hh] " "Hclose". iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
iApply (wp_load_pst _ σ); first eauto using heap_singleton_included. iApply (wp_load_pst _ σ); first eauto using heap_singleton_included.
iIntros "{$Hσ} !> Hσ !==>". iVs ("Hclose" with "[Hσ Hh]") as "_". iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
{ iNext. iExists σ. by iFrame. }
by iApply "HΦ". by iApply "HΦ".
Qed. Qed.
...@@ -145,16 +138,12 @@ Section heap. ...@@ -145,16 +138,12 @@ Section heap.
Proof. Proof.
iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]". iIntros (<-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iInv heapN as (σ) ">[Hσ Hh] " "Hclose". iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
iApply (wp_store_pst _ σ); first eauto using heap_singleton_included. iApply (wp_store_pst _ σ); first eauto using heap_singleton_included.
iIntros "{$Hσ} !> Hσ !==>". iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha".
iVs (own_update_2 with "[$Hh $Hl]") as "[Hh Hl]". { iFrame. iPureIntro. rewrite to_heap_insert.
{ eapply auth_update, singleton_local_update, eapply singleton_local_update, exclusive_local_update; last done.
(exclusive_local_update _ (1%Qp, DecAgree v)); last done.
by eapply heap_singleton_included'. } by eapply heap_singleton_included'. }
iVs ("Hclose" with "[Hσ Hh]") as "_".
{ iNext. iExists (<[l:=v]>σ). rewrite to_heap_insert. iFrame. }
by iApply "HΦ". by iApply "HΦ".
Qed. Qed.
...@@ -165,11 +154,9 @@ Section heap. ...@@ -165,11 +154,9 @@ Section heap.
Proof. Proof.
iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]". iIntros (<-%of_to_val <-%of_to_val ??) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iInv heapN as (σ) ">[Hσ Hh] " "Hclose". iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|]. iApply (wp_cas_fail_pst _ σ); [eauto using heap_singleton_included|done|].
iIntros "{$Hσ} !> Hσ !==>". iVs ("Hclose" with "[Hσ Hh]") as "_". iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha"; first eauto.
{ iNext. iExists σ. by iFrame. }
by iApply "HΦ". by iApply "HΦ".
Qed. Qed.
...@@ -180,16 +167,12 @@ Section heap. ...@@ -180,16 +167,12 @@ Section heap.
Proof. Proof.
iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]". iIntros (<-%of_to_val <-%of_to_val ?) "[#Hinv [>Hl HΦ]]".
rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def. rewrite /heap_ctx heap_mapsto_eq /heap_mapsto_def.
iInv heapN as (σ) ">[Hσ Hh] " "Hclose". iVs (auth_open with "[$Hinv $Hl]") as (σ) "(%&Hσ&Hcl)"; first done.
iDestruct (own_valid_2 with "[$Hh $Hl]") as %[??]%auth_valid_discrete_2.
iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included. iApply (wp_cas_suc_pst _ σ); first eauto using heap_singleton_included.
iIntros "{$Hσ} !> Hσ !==>". iIntros "{$Hσ} !> Hσ !==>". iVs ("Hcl" with "* [Hσ]") as "Ha".
iVs (own_update_2 with "[$Hh $Hl]") as "[Hh Hl]". { iFrame. iPureIntro. rewrite to_heap_insert.
{ eapply auth_update, singleton_local_update, eapply singleton_local_update, exclusive_local_update; last done.
(exclusive_local_update _ (1%Qp, DecAgree v2)); last done.
by eapply heap_singleton_included'. } by eapply heap_singleton_included'. }
iVs ("Hclose" with "[Hσ Hh]") as "_".
{ iNext. iExists (<[l:=v2]>σ). rewrite to_heap_insert. iFrame. }
by iApply "HΦ". by iApply "HΦ".
Qed. Qed.
End heap. End heap.
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ownership ectx_lifting. (* for ownP *) From iris.program_logic Require Import wsat ectx_lifting. (* for ownP *)
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import tactics. From iris.heap_lang Require Import tactics.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
......
...@@ -2234,7 +2234,12 @@ Section Forall_Exists. ...@@ -2234,7 +2234,12 @@ Section Forall_Exists.
Lemma not_Forall_Exists l : ¬Forall P l Exists (not P) l. Lemma not_Forall_Exists l : ¬Forall P l Exists (not P) l.
Proof. intro. destruct (Forall_Exists_dec dec l); intuition. Qed. Proof. intro. destruct (Forall_Exists_dec dec l); intuition. Qed.
Lemma not_Exists_Forall l : ¬Exists P l Forall (not P) l. Lemma not_Exists_Forall l : ¬Exists P l Forall (not P) l.
Proof. by destruct (Forall_Exists_dec (λ x, swap_if (decide (P x))) l). Qed. Proof.
(* TODO: Coq 8.6 needs type annotation here, Coq 8.5 did not.
Should we report this? *)
by destruct (@Forall_Exists_dec (not P) _
(λ x : A, swap_if (decide (P x))) l).
Qed.
Global Instance Forall_dec l : Decision (Forall P l) := Global Instance Forall_dec l : Decision (Forall P l) :=
match Forall_Exists_dec dec l with match Forall_Exists_dec dec l with
| left H => left H | left H => left H
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.algebra Require Import gmap auth agree gset coPset upred_big_op. From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import wsat.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Import uPred. Import uPred.
......
From iris.program_logic Require Export invariants.
From iris.algebra Require Export auth.
From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics.
Import uPred.
(* The CMRA we need. *)
Class authG Σ (A : ucmraT) := AuthG {
auth_inG :> inG Σ (authR A);
auth_discrete :> CMRADiscrete A;
}.
Definition authΣ (A : ucmraT) : gFunctors := #[ GFunctor (constRF (authR A)) ].
Instance subG_authΣ Σ A : subG (authΣ A) Σ CMRADiscrete A authG Σ A.
Proof. intros ?%subG_inG ?. by split. Qed.
Section definitions.
Context `{irisG Λ Σ, authG Σ A} {T : Type} (γ : gname).
Definition auth_own (a : A) : iProp Σ :=
own γ ( a).
Definition auth_inv (f : T A) (φ : T iProp Σ) : iProp Σ :=
( t, own γ ( f t) φ t)%I.
Definition auth_ctx (N : namespace) (f : T A) (φ : T iProp Σ) : iProp Σ :=
inv N (auth_inv f φ).
Global Instance auth_own_ne n : Proper (dist n ==> dist n) auth_own.
Proof. solve_proper. Qed.
Global Instance auth_own_proper : Proper (() ==> ()) auth_own.
Proof. solve_proper. Qed.
Global Instance auth_own_timeless a : TimelessP (auth_own a).
Proof. apply _. Qed.
Global Instance auth_own_persistent a : Persistent a PersistentP (auth_own a).
Proof. apply _. Qed.
Global Instance auth_inv_ne n :
Proper (pointwise_relation T (dist n) ==>
pointwise_relation T (dist n) ==> dist n) auth_inv.
Proof. solve_proper. Qed.
Global Instance auth_inv_proper :
Proper (pointwise_relation T () ==>
pointwise_relation T () ==> ()) auth_inv.
Proof. solve_proper. Qed.
Global Instance auth_ctx_ne N n :
Proper (pointwise_relation T (dist n) ==>
pointwise_relation T (dist n) ==> dist n) (auth_ctx N).
Proof. solve_proper. Qed.
Global Instance auth_ctx_proper N :
Proper (pointwise_relation T () ==>
pointwise_relation T () ==> ()) (auth_ctx N).
Proof. solve_proper. Qed.
Global Instance auth_ctx_persistent N f φ : PersistentP (auth_ctx N f φ).
Proof. apply _. Qed.
End definitions.
Typeclasses Opaque auth_own auth_inv auth_ctx.
Instance: Params (@auth_own) 4.
Instance: Params (@auth_inv) 5.
Instance: Params (@auth_ctx) 8.
Section auth.
Context `{irisG Λ Σ, authG Σ A}.
Context {T : Type} `{!Inhabited T}.
Context (f : T A) (φ : T iProp Σ).
Implicit Types N : namespace.
Implicit Types P Q R : iProp Σ.
Implicit Types a b : A.
Implicit Types t u : T.
Implicit Types γ : gname.
Lemma auth_own_op γ a b : auth_own γ (a b) auth_own γ a auth_own γ b.
Proof. by rewrite /auth_own -own_op auth_frag_op. Qed.
Global Instance from_sep_auth_own γ a b1 b2 :
FromOp a b1 b2
FromSep (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
Proof. rewrite /FromOp /FromSep=> <-. by rewrite auth_own_op. Qed.
Global Instance into_and_auth_own p γ a b1 b2 :
IntoOp a b1 b2
IntoAnd p (auth_own γ a) (auth_own γ b1) (auth_own γ b2) | 90.
Proof. intros. apply mk_into_and_sep. by rewrite (into_op a) auth_own_op. Qed.
Lemma auth_own_mono γ a b : a b auth_own γ b auth_own γ a.
Proof. intros [? ->]. by rewrite auth_own_op sep_elim_l. Qed.
Lemma auth_own_valid γ a : auth_own γ a a.
Proof. by rewrite /auth_own own_valid auth_validI. Qed.
Global Instance auth_own_cmra_homomorphism : CMRAHomomorphism (auth_own γ).
Proof. split. apply _. apply auth_own_op. Qed.
Global Instance own_mono' γ : Proper (flip () ==> ()) (auth_own γ).
Proof. intros a1 a2. apply auth_own_mono. Qed.
Lemma auth_alloc_strong N E t (G : gset gname) :
(f t) φ t ={E}=> γ, (γ G) auth_ctx γ N f φ auth_own γ (f t).
Proof.
iIntros (?) "Hφ". rewrite /auth_own /auth_ctx.
iVs (own_alloc_strong (Auth (Excl' (f t)) (f t)) G) as (γ) "[% Hγ]"; first done.
iRevert "Hγ"; rewrite auth_both_op; iIntros "[Hγ Hγ']".
iVs (inv_alloc N _ (auth_inv γ f φ) with "[-Hγ']") as "#?".
{ iNext. rewrite /auth_inv. iExists t. by iFrame. }
eauto.
Qed.
Lemma auth_alloc N E t :
(f t) φ t ={E}=> γ, auth_ctx γ N f φ auth_own γ (f t).
Proof.
iIntros (?) "Hφ".
iVs (auth_alloc_strong N E t with "Hφ") as (γ) "[_ ?]"; eauto.
Qed.
Lemma auth_empty γ : True =r=> auth_own γ .
Proof. by rewrite /auth_own -own_empty. Qed.
Lemma auth_acc E γ a :
auth_inv γ f φ auth_own γ a ={E}=> t,
(a f t) φ t u b,
((f t, a) ~l~> (f u, b)) φ u ={E}= auth_inv γ f φ auth_own γ b.
Proof.
iIntros "(Hinv & Hγf)". rewrite /auth_inv /auth_own.
iDestruct "Hinv" as (t) "[>Hγa Hφ]".
iVsIntro. iExists t.
iDestruct (own_valid_2 with "[$Hγa $Hγf]") as % [? ?]%auth_valid_discrete_2.
iSplit; first done. iFrame. iIntros (u b) "[% Hφ]".
iVs (own_update_2 with "[$Hγa $Hγf]") as "[Hγa Hγf]".
{ eapply auth_update; eassumption. }
iVsIntro. iFrame. iExists u. iFrame.
Qed.
Lemma auth_open E N γ a :
nclose N E
auth_ctx γ N f φ auth_own γ a ={E,EN}=> t,
(a f t) φ t u b,
((f t, a) ~l~> (f u, b)) φ u ={EN,E}= auth_own γ b.
Proof.
iIntros (?) "[#? Hγf]". rewrite /auth_ctx. iInv N as "Hinv" "Hclose".
(* The following is essentially a very trivial composition of the accessors
[auth_acc] and [inv_open] -- but since we don't have any good support
for that currently, this gets more tedious than it should, with us having
to unpack and repack various proofs.
TODO: Make this mostly automatic, by supporting "opening accessors
around accessors". *)
iVs (auth_acc with "[$Hinv $Hγf]") as (t) "(?&?&HclAuth)".
iVsIntro. iExists t. iFrame. iIntros (u b) "H".
iVs ("HclAuth" $! u b with "H") as "(Hinv & ?)". by iVs ("Hclose" with "Hinv").
Qed.
End auth.
Arguments auth_open {_ _ _ _} [_] {_} [_] _ _ _ _ _ _ _.
(** Some derived lemmas for ectx-based languages *) (** Some derived lemmas for ectx-based languages *)
From iris.program_logic Require Export ectx_language weakestpre lifting. From iris.program_logic Require Export ectx_language weakestpre lifting.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import wsat.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
Section wp. Section wp.
......
From iris.program_logic Require Export pviewshifts. From iris.program_logic Require Export pviewshifts.
From iris.program_logic Require Export namespaces. From iris.program_logic Require Export namespaces.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import wsat.
From iris.algebra Require Import gmap. From iris.algebra Require Import gmap.
From iris.proofmode Require Import tactics coq_tactics intro_patterns. From iris.proofmode Require Import tactics coq_tactics intro_patterns.
Import uPred. Import uPred.
......
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import wsat.
From iris.algebra Require Export upred_big_op. From iris.algebra Require Export upred_big_op.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
...@@ -35,8 +35,8 @@ Lemma wp_lift_pure_step E Φ e1 : ...@@ -35,8 +35,8 @@ Lemma wp_lift_pure_step E Φ e1 :
WP e1 @ E {{ Φ }}. WP e1 @ E {{ Φ }}.
Proof. Proof.
iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto. iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
iIntros (σ1) "Hσ". iApply pvs_intro'; [set_solver|iIntros "Hclose"]. iIntros (σ1) "Hσ". iVs (pvs_intro_mask' E ) as "Hclose"; first set_solver.
iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?). iVsIntro. iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
destruct (Hstep σ1 e2 σ2 efs); auto; subst. destruct (Hstep σ1 e2 σ2 efs); auto; subst.
iVs "Hclose"; iVsIntro. iFrame "Hσ". iApply "H"; auto. iVs "Hclose"; iVsIntro. iFrame "Hσ". iApply "H"; auto.
Qed. Qed.
...@@ -51,7 +51,7 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 : ...@@ -51,7 +51,7 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
Proof. Proof.
iIntros (Hatomic ?) "[Hσ H]". iIntros (Hatomic ?) "[Hσ H]".
iApply (wp_lift_step E _ e1); eauto using reducible_not_val. iApply (wp_lift_step E _ e1); eauto using reducible_not_val.
iApply pvs_intro'; [set_solver|iIntros "Hclose"]. iVs (pvs_intro_mask' E ) as "Hclose"; first set_solver. iVsIntro.
iExists σ1. iFrame "Hσ"; iSplit; eauto. iExists σ1. iFrame "Hσ"; iSplit; eauto.
iNext; iIntros (e2 σ2 efs) "[% Hσ]". iNext; iIntros (e2 σ2 efs) "[% Hσ]".
edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto. edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
......
...@@ -52,7 +52,8 @@ Section ndisjoint. ...@@ -52,7 +52,8 @@ Section ndisjoint.
Lemma ndot_ne_disjoint N x y : x y N .@ x N .@ y. Lemma ndot_ne_disjoint N x y : x y N .@ x N .@ y.
Proof. Proof.
intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq. intros Hxy a. rewrite !nclose_eq !elem_coPset_suffixes !ndot_eq.
intros [qx ->] [qy]. by intros [= ?%encode_inj]%list_encode_suffix_eq. intros [qx ->] [qy Hqy].
revert Hqy. by intros [= ?%encode_inj]%list_encode_suffix_eq.
Qed. Qed.
Lemma ndot_preserve_disjoint_l N E x : nclose N E nclose (N .@ x) E. Lemma ndot_preserve_disjoint_l N E x : nclose N E nclose (N .@ x) E.
......
From iris.program_logic Require Export iris. From iris.program_logic Require Export iris.
From iris.program_logic Require Import ownership. From iris.program_logic Require Import wsat.
From iris.algebra Require Import upred_big_op gmap. From iris.algebra Require Import upred_big_op gmap.
From iris.proofmode Require Import tactics classes. From iris.proofmode Require Import tactics classes.
Import uPred. Import uPred.
...@@ -99,6 +99,8 @@ Proof. intros P Q; apply pvs_mono. Qed. ...@@ -99,6 +99,8 @@ Proof. intros P Q; apply pvs_mono. Qed.
Lemma pvs_intro E P : P ={E}=> P. Lemma pvs_intro E P : P ={E}=> P.
Proof. iIntros "HP". by iApply rvs_pvs. Qed. Proof. iIntros "HP". by iApply rvs_pvs. Qed.
Lemma pvs_intro_mask' E1 E2 : E2 E1 True |={E1,E2}=> |={E2,E1}=> True.
Proof. exact: pvs_intro_mask. Qed.
Lemma pvs_except_last E1 E2 P : (|={E1,E2}=> P) ={E1,E2}=> P. Lemma pvs_except_last E1 E2 P : (|={E1,E2}=> P) ={E1,E2}=> P.
Proof. by rewrite {1}(pvs_intro E2 P) except_last_pvs pvs_trans. Qed. Proof. by rewrite {1}(pvs_intro E2 P) except_last_pvs pvs_trans. Qed.
...@@ -109,11 +111,6 @@ Proof. by rewrite pvs_frame_l wand_elim_l. Qed. ...@@ -109,11 +111,6 @@ Proof. by rewrite pvs_frame_l wand_elim_l. Qed.
Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P) (P - Q) ={E1,E2}=> Q. Lemma pvs_wand_r E1 E2 P Q : (|={E1,E2}=> P) (P - Q) ={E1,E2}=> Q.
Proof. by rewrite pvs_frame_r wand_elim_r. Qed.