Commit 9a3439f5 authored by Robbert Krebbers's avatar Robbert Krebbers

Make use of `excl_auth` camera.

parent 38f75bf3
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl auth gmap agree.
From iris.algebra Require Import excl_auth gmap agree.
From iris.base_logic.lib Require Export invariants.
Set Default Proof Using "Type".
Import uPred.
......@@ -7,10 +7,10 @@ Import uPred.
(** The CMRAs we need. *)
Class boxG Σ :=
boxG_inG :> inG Σ (prodR
(authR (optionUR (exclR boolO)))
(excl_authR boolO)
(optionR (agreeR (laterO (iPrePropO Σ))))).
Definition boxΣ : gFunctors := #[ GFunctor (authR (optionUR (exclR boolO)) *
Definition boxΣ : gFunctors := #[ GFunctor (excl_authR boolO *
optionRF (agreeRF ( )) ) ].
Instance subG_boxΣ Σ : subG boxΣ Σ boxG Σ.
......@@ -21,14 +21,14 @@ Section box_defs.
Definition slice_name := gname.
Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool))) : iProp Σ :=
Definition box_own_auth (γ : slice_name) (a : excl_authR boolO) : iProp Σ :=
own γ (a, None).
Definition box_own_prop (γ : slice_name) (P : iProp Σ) : iProp Σ :=
own γ (ε, Some (to_agree (Next (iProp_unfold P)))).
Definition slice_inv (γ : slice_name) (P : iProp Σ) : iProp Σ :=
( b, box_own_auth γ ( Excl' b) if b then P else True)%I.
( b, box_own_auth γ (E b) if b then P else True)%I.
Definition slice (γ : slice_name) (P : iProp Σ) : iProp Σ :=
(box_own_prop γ P inv N (slice_inv γ P))%I.
......@@ -36,7 +36,7 @@ Section box_defs.
Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
( Φ : slice_name iProp Σ,
(P [ map] γ _ f, Φ γ)
[ map] γ b f, box_own_auth γ ( Excl' b) box_own_prop γ (Φ γ)
[ map] γ b f, box_own_auth γ (E b) box_own_prop γ (Φ γ)
inv N (slice_inv γ (Φ γ)))%I.
End box_defs.
......@@ -75,18 +75,18 @@ Global Instance box_proper f : Proper ((≡) ==> (≡)) (box N f).
Proof. apply ne_proper, _. Qed.
Lemma box_own_auth_agree γ b1 b2 :
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2) b1 = b2.
box_own_auth γ (E b1) box_own_auth γ (E b2) b1 = b2.
Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_both_valid.
by iDestruct 1 as %?%excl_auth_agreeL.
Qed.
Lemma box_own_auth_update γ b1 b2 b3 :
box_own_auth γ ( Excl' b1) box_own_auth γ ( Excl' b2)
== box_own_auth γ ( Excl' b3) box_own_auth γ ( Excl' b3).
box_own_auth γ (E b1) box_own_auth γ (E b2)
== box_own_auth γ (E b3) box_own_auth γ (E b3).
Proof.
rewrite /box_own_auth -!own_op. apply own_update, prod_update; last done.
by apply auth_update, option_local_update, exclusive_local_update.
apply excl_auth_update.
Qed.
Lemma box_own_agree γ Q1 Q2 :
......@@ -108,7 +108,7 @@ Lemma slice_insert_empty E q f Q P :
slice N γ Q ?q box N (<[γ:=false]> f) (Q P).
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iMod (own_alloc_cofinite ( Excl' false Excl' false,
iMod (own_alloc_cofinite (E false E false,
Some (to_agree (Next (iProp_unfold Q)))) (dom _ f))
as (γ) "[Hdom Hγ]"; first by (split; [apply auth_both_valid|]).
rewrite pair_split. iDestruct "Hγ" as "[[Hγ Hγ'] #HγQ]".
......@@ -225,7 +225,7 @@ Lemma box_empty E f P :
Proof.
iDestruct 1 as (Φ) "[#HeqP Hf]".
iAssert (([ map] γ↦b f, Φ γ)
[ map] γ↦b f, box_own_auth γ ( Excl' false) box_own_prop γ (Φ γ)
[ map] γ↦b f, box_own_auth γ (E false) box_own_prop γ (Φ γ)
inv N (slice_inv γ (Φ γ)))%I with "[> Hf]" as "[HΦ ?]".
{ rewrite -big_sepM_sep -big_sepM_fupd. iApply (@big_sepM_impl with "[$Hf]").
iIntros "!#" (γ b ?) "(Hγ' & #HγΦ & #Hinv)".
......
From iris.proofmode Require Import tactics classes.
From iris.algebra Require Import excl auth.
From iris.algebra Require Import excl_auth.
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import lifting adequacy.
From iris.program_logic Require ectx_language.
......@@ -16,24 +16,24 @@ union.
Class ownPG (Λ : language) (Σ : gFunctors) := OwnPG {
ownP_invG : invG Σ;
ownP_inG :> inG Σ (authR (optionUR (exclR (stateO Λ))));
ownP_inG :> inG Σ (excl_authR (stateO Λ));
ownP_name : gname;
}.
Instance ownPG_irisG `{!ownPG Λ Σ} : irisG Λ Σ := {
iris_invG := ownP_invG;
state_interp σ κs _ := own ownP_name ( (Excl' σ))%I;
state_interp σ κs _ := own ownP_name (E σ)%I;
fork_post _ := True%I;
}.
Global Opaque iris_invG.
Definition ownPΣ (Λ : language) : gFunctors :=
#[invΣ;
GFunctor (authR (optionUR (exclR (stateO Λ))))].
GFunctor (excl_authR (stateO Λ))].
Class ownPPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
ownPPre_invG :> invPreG Σ;
ownPPre_state_inG :> inG Σ (authR (optionUR (exclR (stateO Λ))))
ownPPre_state_inG :> inG Σ (excl_authR (stateO Λ))
}.
Instance subG_ownPΣ {Λ Σ} : subG (ownPΣ Λ) Σ ownPPreG Λ Σ.
......@@ -41,8 +41,7 @@ Proof. solve_inG. Qed.
(** Ownership *)
Definition ownP `{!ownPG Λ Σ} (σ : state Λ) : iProp Σ :=
own ownP_name ( (Excl' σ)).
own ownP_name (E σ).
Typeclasses Opaque ownP.
Instance: Params (@ownP) 3 := {}.
......@@ -53,9 +52,9 @@ Theorem ownP_adequacy Σ `{!ownPPreG Λ Σ} s e σ φ :
Proof.
intros Hwp. apply (wp_adequacy Σ _).
iIntros (? κs).
iMod (own_alloc ( (Excl' σ) (Excl' σ))) as (γσ) "[Hσ Hσf]";
first by apply auth_both_valid.
iModIntro. iExists (λ σ κs, own γσ ( (Excl' σ)))%I, (λ _, True%I).
iMod (own_alloc (E σ E σ)) as (γσ) "[Hσ Hσf]";
first by apply excl_auth_valid.
iModIntro. iExists (λ σ κs, own γσ (E σ))%I, (λ _, True%I).
iFrame "Hσ".
iApply (Hwp (OwnPG _ _ _ _ γσ)). rewrite /ownP. iFrame.
Qed.
......@@ -69,9 +68,9 @@ Theorem ownP_invariance Σ `{!ownPPreG Λ Σ} s e σ1 t2 σ2 φ :
Proof.
intros Hwp Hsteps. eapply (wp_invariance Σ Λ s e σ1 t2 σ2 _)=> //.
iIntros (? κs).
iMod (own_alloc ( (Excl' σ1) (Excl' σ1))) as (γσ) "[Hσ Hσf]";
iMod (own_alloc (E σ1 E σ1)) as (γσ) "[Hσ Hσf]";
first by apply auth_both_valid.
iExists (λ σ κs' _, own γσ ( (Excl' σ)))%I, (λ _, True%I).
iExists (λ σ κs' _, own γσ (E σ))%I, (λ _, True%I).
iFrame "Hσ".
iMod (Hwp (OwnPG _ _ _ _ γσ) with "[Hσf]") as "[$ H]";
first by rewrite /ownP; iFrame.
......@@ -118,8 +117,7 @@ Section lifting.
iModIntro; iSplit; [by destruct s|]; iNext; iIntros (e2 σ2 efs Hstep).
iDestruct "Hσκs" as "Hσ". rewrite /ownP.
iMod (own_update_2 with "Hσ Hσf") as "[Hσ Hσf]".
{ apply auth_update. apply option_local_update.
by apply (exclusive_local_update _ (Excl σ2)). }
{ apply excl_auth_update. }
iFrame "Hσ". iApply ("H" with "[]"); eauto with iFrame.
Qed.
......
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