Commit 5c59c27d authored by Robbert Krebbers's avatar Robbert Krebbers

Prepare for iris!328

parent f5481a10
-Q theories actris -Q theories actris
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-convert_concl_no_check,-undeclared-scope,-ambiguous-paths -arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files,-convert_concl_no_check,-undeclared-scope,-ambiguous-paths
theories/utils/auth_excl.v
theories/utils/llist.v theories/utils/llist.v
theories/utils/compare.v theories/utils/compare.v
theories/utils/contribution.v theories/utils/contribution.v
......
...@@ -27,8 +27,8 @@ protocols. *) ...@@ -27,8 +27,8 @@ protocols. *)
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.heap_lang Require Import lifting. From iris.heap_lang Require Import lifting.
From iris.algebra Require Import excl auth list. From iris.algebra Require Import excl_auth list.
From actris.utils Require Import auth_excl llist. From actris.utils Require Import llist.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Inductive side := Left | Right. Inductive side := Left | Right.
...@@ -70,10 +70,10 @@ Definition recv : val := ...@@ -70,10 +70,10 @@ Definition recv : val :=
(** * Setup of Iris's cameras *) (** * Setup of Iris's cameras *)
Class chanG Σ := { Class chanG Σ := {
chanG_lockG :> lockG Σ; chanG_lockG :> lockG Σ;
chanG_authG :> auth_exclG (listO valO) Σ; chanG_authG :> inG Σ (excl_authR (listO valO));
}. }.
Definition chanΣ : gFunctors := Definition chanΣ : gFunctors :=
#[ lockΣ; auth_exclΣ (constOF (listO valO)) ]. #[ lockΣ; GFunctor (excl_authR (listO valO)) ].
Instance subG_chanΣ {Σ} : subG chanΣ Σ chanG Σ. Instance subG_chanΣ {Σ} : subG chanΣ Σ chanG Σ.
Proof. solve_inG. Qed. Proof. solve_inG. Qed.
...@@ -89,8 +89,8 @@ Section channel. ...@@ -89,8 +89,8 @@ Section channel.
(** * The logical connectives *) (** * The logical connectives *)
Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ := Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
( ls rs, ( ls rs,
llist sbi_internal_eq l ls own (chan_l_name γ) ( to_auth_excl ls) llist sbi_internal_eq l ls own (chan_l_name γ) (E ls)
llist sbi_internal_eq r rs own (chan_r_name γ) ( to_auth_excl rs))%I. llist sbi_internal_eq r rs own (chan_r_name γ) (E rs))%I.
Typeclasses Opaque chan_inv. Typeclasses Opaque chan_inv.
Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ := Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
...@@ -104,16 +104,16 @@ Section channel. ...@@ -104,16 +104,16 @@ Section channel.
Lemma chan_inv_alt s γ l r : Lemma chan_inv_alt s γ l r :
chan_inv γ l r ls rs, chan_inv γ l r ls rs,
llist sbi_internal_eq (side_elim s l r) ls llist sbi_internal_eq (side_elim s l r) ls
own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl ls) own (side_elim s chan_l_name chan_r_name γ) (E ls)
llist sbi_internal_eq (side_elim s r l) rs llist sbi_internal_eq (side_elim s r l) rs
own (side_elim s chan_r_name chan_l_name γ) ( to_auth_excl rs). own (side_elim s chan_r_name chan_l_name γ) (E rs).
Proof. Proof.
destruct s; rewrite /chan_inv //=. destruct s; rewrite /chan_inv //=.
iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame. iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
Qed. Qed.
Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ := Definition chan_own (γ : chan_name) (s : side) (vs : list val) : iProp Σ :=
own (side_elim s chan_l_name chan_r_name γ) ( to_auth_excl vs)%I. own (side_elim s chan_l_name chan_r_name γ) (E vs)%I.
(** * The proof rules *) (** * The proof rules *)
Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs). Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
...@@ -128,13 +128,13 @@ Section channel. ...@@ -128,13 +128,13 @@ Section channel.
wp_lam. wp_lam.
wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl". wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr". wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (lsγ) "[Hls Hls']". iMod (own_alloc (E [] E [])) as (lsγ) "[Hls Hls']".
{ by apply auth_both_valid. } { by apply excl_auth_valid. }
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (rsγ) "[Hrs Hrs']". iMod (own_alloc (E [] E [])) as (rsγ) "[Hrs Hrs']".
{ by apply auth_both_valid. } { by apply excl_auth_valid. }
wp_apply (newlock_spec N ( ls rs, wp_apply (newlock_spec N ( ls rs,
llist sbi_internal_eq l ls own lsγ ( to_auth_excl ls) llist sbi_internal_eq l ls own lsγ (E ls)
llist sbi_internal_eq r rs own rsγ ( to_auth_excl rs))%I with "[Hl Hr Hls Hrs]"). llist sbi_internal_eq r rs own rsγ (E rs))%I with "[Hl Hr Hls Hrs]").
{ eauto 10 with iFrame. } { eauto 10 with iFrame. }
iIntros (lk γlk) "#Hlk". wp_pures. iIntros (lk γlk) "#Hlk". wp_pures.
iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl. iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl.
...@@ -157,8 +157,9 @@ Section channel. ...@@ -157,8 +157,9 @@ Section channel.
(vs ws) "(Hll & Hvs & Href' & Hws)". (vs ws) "(Hll & Hvs & Href' & Hws)".
wp_seq. wp_bind (Fst (_,_)%V)%E. wp_seq. wp_bind (Fst (_,_)%V)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]". iMod "HΦ" as (vs') "[Hchan HΦ]".
iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv. iDestruct (own_valid_2 with "Hvs Hchan") as %<-%excl_auth_agreeL.
iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]". iMod (own_update_2 _ _ _ (E (vs ++ [v]) _) with "Hvs Hchan") as "[Hvs Hchan]".
{ apply excl_auth_update. }
wp_pures. iMod ("HΦ" with "Hchan") as "HΦ"; iModIntro. wp_pures. iMod ("HΦ" with "Hchan") as "HΦ"; iModIntro.
wp_apply (lsnoc_spec with "[$Hll //]"); iIntros "Hll". wp_apply (lsnoc_spec with "[$Hll //]"); iIntros "Hll".
wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto. wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
...@@ -190,8 +191,9 @@ Section channel. ...@@ -190,8 +191,9 @@ Section channel.
rewrite /llist. eauto 10 with iFrame. } rewrite /llist. eauto 10 with iFrame. }
iIntros (_). by wp_pures. iIntros (_). by wp_pures.
- iDestruct "HΦ" as "[_ >HΦ]". iDestruct "HΦ" as (vs') "[Hvs' HΦ]". - iDestruct "HΦ" as "[_ >HΦ]". iDestruct "HΦ" as (vs') "[Hvs' HΦ]".
iDestruct (excl_eq with "Hvs Hvs'") as %<-%leibniz_equiv. iDestruct (own_valid_2 with "Hvs Hvs'") as %<-%excl_auth_agreeL.
iMod (excl_update _ _ _ vs with "Hvs Hvs'") as "[Hvs Hvs']". iMod (own_update_2 _ _ _ (E vs _) with "Hvs Hvs'") as "[Hvs Hvs']".
{ apply excl_auth_update. }
wp_pures. iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro. wp_pures. iMod ("HΦ" with "[//] Hvs'") as "HΦ"; iModIntro.
wp_apply (lisnil_spec with "Hll"); iIntros "Hll". wp_apply (lisnil_spec with "Hll"); iIntros "Hll".
wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=. wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=.
......
...@@ -42,8 +42,7 @@ From actris.channel Require Export channel. ...@@ -42,8 +42,7 @@ From actris.channel Require Export channel.
From actris.channel Require Import proto_model. From actris.channel Require Import proto_model.
From iris.base_logic.lib Require Import invariants. From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth excl. From iris.algebra Require Import excl_auth.
From actris.utils Require Import auth_excl.
Export action. Export action.
Definition start_chan : val := λ: "f", Definition start_chan : val := λ: "f",
...@@ -53,15 +52,15 @@ Definition start_chan : val := λ: "f", ...@@ -53,15 +52,15 @@ Definition start_chan : val := λ: "f",
(** * Setup of Iris's cameras *) (** * Setup of Iris's cameras *)
Class proto_chanG Σ := { Class proto_chanG Σ := {
proto_chanG_chanG :> chanG Σ; proto_chanG_chanG :> chanG Σ;
proto_chanG_authG :> auth_exclG (laterO (proto val (iPrePropO Σ) (iPrePropO Σ))) Σ; proto_chanG_authG :> inG Σ (excl_authR (laterO (proto val (iPrePropO Σ) (iPrePropO Σ))));
}. }.
Definition proto_chanΣ := #[ Definition proto_chanΣ := #[
chanΣ; chanΣ;
GFunctor (authRF(optionURF (exclRF (laterOF (protoOF val idOF idOF))))) GFunctor (authRF (optionURF (exclRF (laterOF (protoOF val idOF idOF)))))
]. ].
Instance subG_chanΣ {Σ} : subG proto_chanΣ Σ proto_chanG Σ. Instance subG_chanΣ {Σ} : subG proto_chanΣ Σ proto_chanG Σ.
Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed. Proof. intros [??%subG_inG]%subG_inv. constructor; apply _. Qed.
(** * Types *) (** * Types *)
Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ). Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ).
...@@ -212,16 +211,17 @@ Record proto_name := ProtName { ...@@ -212,16 +211,17 @@ Record proto_name := ProtName {
proto_r_name : gname proto_r_name : gname
}. }.
Definition to_proto_auth_excl `{!proto_chanG Σ} (p : iProto Σ) := Definition to_pre_proto `{!proto_chanG Σ} (p : iProto Σ) :
to_auth_excl (Next (proto_map id iProp_fold iProp_unfold p)). proto val (iPrePropO Σ) (iPrePropO Σ) :=
proto_map id iProp_fold iProp_unfold p.
Definition proto_own_frag `{!proto_chanG Σ} (γ : proto_name) (s : side) Definition proto_own_frag `{!proto_chanG Σ} (γ : proto_name) (s : side)
(p : iProto Σ) : iProp Σ := (p : iProto Σ) : iProp Σ :=
own (side_elim s proto_l_name proto_r_name γ) ( to_proto_auth_excl p)%I. own (side_elim s proto_l_name proto_r_name γ) (E (Next (to_pre_proto p))).
Definition proto_own_auth `{!proto_chanG Σ} (γ : proto_name) (s : side) Definition proto_own_auth `{!proto_chanG Σ} (γ : proto_name) (s : side)
(p : iProto Σ) : iProp Σ := (p : iProto Σ) : iProp Σ :=
own (side_elim s proto_l_name proto_r_name γ) ( to_proto_auth_excl p)%I. own (side_elim s proto_l_name proto_r_name γ) (E (Next (to_pre_proto p))).
Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ := Definition proto_inv `{!proto_chanG Σ} (γ : proto_name) : iProp Σ :=
( l r pl pr, ( l r pl pr,
...@@ -385,7 +385,7 @@ Section proto. ...@@ -385,7 +385,7 @@ Section proto.
Global Instance proto_interp_proper vs : Proper (() ==> () ==> ()) (proto_interp vs). Global Instance proto_interp_proper vs : Proper (() ==> () ==> ()) (proto_interp vs).
Proof. apply (ne_proper_2 _). Qed. Proof. apply (ne_proper_2 _). Qed.
Global Instance to_proto_auth_excl_ne : NonExpansive to_proto_auth_excl. Global Instance to_pre_proto_ne : NonExpansive to_pre_proto.
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s). Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s).
Proof. solve_proper. Qed. Proof. solve_proper. Qed.
...@@ -399,9 +399,9 @@ Section proto. ...@@ -399,9 +399,9 @@ Section proto.
Proof. Proof.
iIntros "Hauth Hfrag". iIntros "Hauth Hfrag".
iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid". iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
iDestruct (to_auth_excl_valid with "Hvalid") as "Hvalid". iDestruct (excl_auth_agreeI with "Hvalid") as "Hvalid".
iDestruct (bi.later_eq_1 with "Hvalid") as "Hvalid"; iNext. iDestruct (bi.later_eq_1 with "Hvalid") as "Hvalid"; iNext.
assert ( p, rewrite /to_pre_proto. assert ( p,
proto_map id iProp_unfold iProp_fold (proto_map id iProp_fold iProp_unfold p) p) as help. proto_map id iProp_unfold iProp_fold (proto_map id iProp_fold iProp_unfold p) p) as help.
{ intros p''. rewrite -proto_map_compose -{2}(proto_map_id p''). { intros p''. rewrite -proto_map_compose -{2}(proto_map_id p'').
apply proto_map_ext=> // pc /=; by rewrite iProp_fold_unfold. } apply proto_map_ext=> // pc /=; by rewrite iProp_fold_unfold. }
...@@ -414,8 +414,7 @@ Section proto. ...@@ -414,8 +414,7 @@ Section proto.
Proof. Proof.
iIntros "Hauth Hfrag". iIntros "Hauth Hfrag".
iDestruct (own_update_2 with "Hauth Hfrag") as "H". iDestruct (own_update_2 with "Hauth Hfrag") as "H".
{ eapply (auth_update _ _ (to_proto_auth_excl p'') (to_proto_auth_excl p'')). { eapply (excl_auth_update _ _ (Next (to_pre_proto p''))). }
apply option_local_update. by apply exclusive_local_update. }
by rewrite own_op. by rewrite own_op.
Qed. Qed.
...@@ -474,12 +473,12 @@ Section proto. ...@@ -474,12 +473,12 @@ Section proto.
c1 p c2 iProto_dual p. c1 p c2 iProto_dual p.
Proof. Proof.
iIntros "#Hcctx Hcol Hcor". iIntros "#Hcctx Hcol Hcor".
iMod (own_alloc ( (to_proto_auth_excl p) iMod (own_alloc (E (Next (to_pre_proto p))
(to_proto_auth_excl p))) as (lγ) "[Hlsta Hlstf]". E (Next (to_pre_proto p)))) as (lγ) "[Hlsta Hlstf]".
{ by apply auth_both_valid_2. } { by apply excl_auth_valid. }
iMod (own_alloc ( (to_proto_auth_excl (iProto_dual p)) iMod (own_alloc (E (Next (to_pre_proto (iProto_dual p)))
(to_proto_auth_excl (iProto_dual p)))) as (rγ) "[Hrsta Hrstf]". E (Next (to_pre_proto (iProto_dual p))))) as (rγ) "[Hrsta Hrstf]".
{ by apply auth_both_valid_2. } { by apply excl_auth_valid. }
pose (ProtName cγ lγ rγ) as pγ. pose (ProtName cγ lγ rγ) as pγ.
iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv". iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
{ iNext. rewrite /proto_inv. eauto 10 with iFrame. } { iNext. rewrite /proto_inv. eauto 10 with iFrame. }
......
(** This file provides some utilities for the commonly used camera of
authoritative exclusive ownership, [auth (option (excl A))]. *)
From iris.proofmode Require Import tactics.
From iris.algebra Require Import excl auth.
From iris.base_logic.lib Require Import own.
Set Default Proof Using "Type".
Class auth_exclG (A : ofeT) (Σ : gFunctors) := AuthExclG {
exclG_authG :> inG Σ (authR (optionUR (exclR A)));
}.
Definition auth_exclΣ (F : oFunctor) `{!oFunctorContractive F} : gFunctors :=
#[GFunctor (authRF (optionURF (exclRF F)))].
Instance subG_auth_exclG (F : oFunctor) `{!oFunctorContractive F} {Σ} :
subG (auth_exclΣ F) Σ auth_exclG (F (iPrePropO Σ) _) Σ.
Proof. solve_inG. Qed.
Definition to_auth_excl {A : ofeT} (a : A) : option (excl A) :=
Excl' a.
Instance: Params (@to_auth_excl) 1 := {}.
Section auth_excl_ofe.
Context {A : ofeT}.
Global Instance to_auth_excl_ne : NonExpansive (@to_auth_excl A).
Proof. solve_proper. Qed.
Global Instance to_auth_excl_proper :
Proper (() ==> ()) (@to_auth_excl A).
Proof. solve_proper. Qed.
End auth_excl_ofe.
Section auth_excl.
Context `{!auth_exclG A Σ}.
Implicit Types x y : A.
Lemma to_auth_excl_valid x y :
( to_auth_excl x to_auth_excl y) - (x y : iProp Σ).
Proof.
iIntros "Hvalid".
iDestruct (auth_both_validI with "Hvalid") as "[_ [Hle Hvalid]]"; simpl.
iDestruct "Hle" as ([z|]) "Hy"; last first.
- by rewrite bi.option_equivI /= excl_equivI.
- iRewrite "Hy" in "Hvalid".
by rewrite uPred.option_validI /= excl_validI /=.
Qed.
Lemma excl_eq γ x y :
own γ ( to_auth_excl x) - own γ ( to_auth_excl y) - x y.
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_valid_2 with "Hauth Hfrag") as "Hvalid".
iDestruct (to_auth_excl_valid with "Hvalid") as "$".
Qed.
Lemma excl_update γ x y z :
own γ ( to_auth_excl y) - own γ ( to_auth_excl x) ==
own γ ( to_auth_excl z) own γ ( to_auth_excl z).
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_update_2 with "Hauth Hfrag") as "H".
{ eapply (auth_update _ _ (to_auth_excl z) (to_auth_excl z)).
eapply option_local_update.
eapply exclusive_local_update. done. }
by rewrite own_op.
Qed.
End auth_excl.
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