Forked from
Iris / Iris
6349 commits behind the upstream repository.
-
Robbert Krebbers authored
This way, it won't pick arbitrary (and possibly wrong!) inG instances when multiple ones are available. We achieve this by declaring: Hint Mode inG - - + So that type class inference only succeeds when the type of the ghost variable does not include any evars. This required me to make some minor changes throughout the whole development making some types explicit.
Robbert Krebbers authoredThis way, it won't pick arbitrary (and possibly wrong!) inG instances when multiple ones are available. We achieve this by declaring: Hint Mode inG - - + So that type class inference only succeeds when the type of the ghost variable does not include any evars. This required me to make some minor changes throughout the whole development making some types explicit.
boxes.v 8.17 KiB
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import auth saved_prop.
From iris.proofmode Require Import tactics invariants ghost_ownership.
Import uPred.
(** The CMRAs we need. *)
Class boxG Λ Σ :=
boxG_inG :> inG Λ Σ (prodR
(authR (optionUR (exclR boolC)))
(optionR (agreeR (laterC (iPrePropG Λ Σ))))).
Section box_defs.
Context `{boxG Λ Σ} (N : namespace).
Notation iProp := (iPropG Λ Σ).
Definition slice_name := gname.
Definition box_own_auth (γ : slice_name) (a : auth (option (excl bool)))
:= own γ (a, (∅:option (agree (later (iPrePropG Λ Σ))))).
Definition box_own_prop (γ : slice_name) (P : iProp) : iProp :=
own γ (∅:auth (option (excl bool)), Some (to_agree (Next (iProp_unfold P)))).
Definition slice_inv (γ : slice_name) (P : iProp) : iProp :=
(∃ b, box_own_auth γ (● Excl' b) ★ box_own_prop γ P ★ if b then P else True)%I.
Definition slice (γ : slice_name) (P : iProp) : iProp :=
inv N (slice_inv γ P).
Definition box (f : gmap slice_name bool) (P : iProp) : iProp :=
(∃ Φ : slice_name → iProp,
▷ (P ≡ [★ map] γ ↦ b ∈ f, Φ γ) ★
[★ map] γ ↦ b ∈ f, box_own_auth γ (◯ Excl' b) ★ box_own_prop γ (Φ γ) ★
inv N (slice_inv γ (Φ γ)))%I.
End box_defs.
Instance: Params (@box_own_auth) 4.
Instance: Params (@box_own_prop) 4.
Instance: Params (@slice_inv) 4.
Instance: Params (@slice) 5.
Instance: Params (@box) 5.
Section box.
Context `{boxG Λ Σ} (N : namespace).
Notation iProp := (iPropG Λ Σ).
Implicit Types P Q : iProp.
Global Instance box_own_prop_ne n γ : Proper (dist n ==> dist n) (box_own_prop γ).
Proof. solve_proper. Qed.
Global Instance box_inv_ne n γ : Proper (dist n ==> dist n) (slice_inv γ).
Proof. solve_proper. Qed.
Global Instance slice_ne n γ : Proper (dist n ==> dist n) (slice N γ).
Proof. solve_proper. Qed.
Global Instance box_ne n f : Proper (dist n ==> dist n) (box N f).
Proof. solve_proper. Qed.
Global Instance slice_persistent γ P : PersistentP (slice N γ P).
Proof. apply _. Qed.
Lemma box_own_auth_agree γ b1 b2 :
box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2) ⊢ b1 = b2.
Proof.
rewrite /box_own_prop -own_op own_valid prod_validI /= and_elim_l.
by iDestruct 1 as % [[[] [=]%leibniz_equiv] ?]%auth_valid_discrete.
Qed.
Lemma box_own_auth_update E γ b1 b2 b3 :
box_own_auth γ (● Excl' b1) ★ box_own_auth γ (◯ Excl' b2)
={E}=> box_own_auth γ (● Excl' b3) ★ box_own_auth γ (◯ Excl' b3).
Proof.
rewrite /box_own_prop -!own_op own_valid_l prod_validI; iIntros "[[Hb _] Hγ]".