Commit 1bcc45db authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (make use of `excl_auth`).

parent ba740097
Pipeline #21446 passed with stage
in 22 minutes and 5 seconds
-Q theories actris
-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/compare.v
theories/utils/contribution.v
......
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/actris" ]
depends: [
"coq-iris" { (= "dev.2019-10-25.0.bbd38120") | (= "dev") }
"coq-iris" { (= "dev.2019-11-21.4.d1787db2") | (= "dev") }
]
......@@ -27,8 +27,8 @@ protocols. *)
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.heap_lang Require Import lifting.
From iris.algebra Require Import excl auth list.
From actris.utils Require Import auth_excl llist.
From iris.algebra Require Import excl_auth list.
From actris.utils Require Import llist.
Set Default Proof Using "Type".
Inductive side := Left | Right.
......@@ -70,10 +70,10 @@ Definition recv : val :=
(** * Setup of Iris's cameras *)
Class chanG Σ := {
chanG_lockG :> lockG Σ;
chanG_authG :> auth_exclG (listO valO) Σ;
chanG_authG :> inG Σ (excl_authR (listO valO));
}.
Definition chanΣ : gFunctors :=
#[ lockΣ; auth_exclΣ (constOF (listO valO)) ].
#[ lockΣ; GFunctor (excl_authR (listO valO)) ].
Instance subG_chanΣ {Σ} : subG chanΣ Σ chanG Σ.
Proof. solve_inG. Qed.
......@@ -89,8 +89,8 @@ Section channel.
(** * The logical connectives *)
Definition chan_inv (γ : chan_name) (l r : loc) : iProp Σ :=
( ls rs,
llist sbi_internal_eq l ls own (chan_l_name γ) ( to_auth_excl ls)
llist sbi_internal_eq r rs own (chan_r_name γ) ( to_auth_excl rs))%I.
llist sbi_internal_eq l ls own (chan_l_name γ) (E ls)
llist sbi_internal_eq r rs own (chan_r_name γ) (E rs))%I.
Typeclasses Opaque chan_inv.
Definition is_chan (γ : chan_name) (c1 c2 : val) : iProp Σ :=
......@@ -104,16 +104,16 @@ Section channel.
Lemma chan_inv_alt s γ l r :
chan_inv γ l r ls rs,
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
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.
destruct s; rewrite /chan_inv //=.
iSplit; iDestruct 1 as (ls rs) "(?&?&?&?)"; iExists rs, ls; iFrame.
Qed.
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 *)
Global Instance chan_own_timeless γ s vs : Timeless (chan_own γ s vs).
......@@ -128,13 +128,13 @@ Section channel.
wp_lam.
wp_apply (lnil_spec with "[//]"); iIntros (l) "Hl".
wp_apply (lnil_spec with "[//]"); iIntros (r) "Hr".
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (lsγ) "[Hls Hls']".
{ by apply auth_both_valid. }
iMod (own_alloc ( (to_auth_excl []) (to_auth_excl []))) as (rsγ) "[Hrs Hrs']".
{ by apply auth_both_valid. }
iMod (own_alloc (E [] E [])) as (lsγ) "[Hls Hls']".
{ by apply excl_auth_valid. }
iMod (own_alloc (E [] E [])) as (rsγ) "[Hrs Hrs']".
{ by apply excl_auth_valid. }
wp_apply (newlock_spec N ( ls rs,
llist sbi_internal_eq l ls own lsγ ( to_auth_excl ls)
llist sbi_internal_eq r rs own rsγ ( to_auth_excl rs))%I with "[Hl Hr Hls Hrs]").
llist sbi_internal_eq l ls own lsγ (E ls)
llist sbi_internal_eq r rs own rsγ (E rs))%I with "[Hl Hr Hls Hrs]").
{ eauto 10 with iFrame. }
iIntros (lk γlk) "#Hlk". wp_pures.
iApply ("HΦ" $! _ _ (Chan_name γlk lsγ rsγ)); simpl.
......@@ -157,8 +157,9 @@ Section channel.
(vs ws) "(Hll & Hvs & Href' & Hws)".
wp_seq. wp_bind (Fst (_,_)%V)%E.
iMod "HΦ" as (vs') "[Hchan HΦ]".
iDestruct (excl_eq with "Hvs Hchan") as %<-%leibniz_equiv.
iMod (excl_update _ _ _ (vs ++ [v]) with "Hvs Hchan") as "[Hvs Hchan]".
iDestruct (own_valid_2 with "Hvs Hchan") as %<-%excl_auth_agreeL.
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_apply (lsnoc_spec with "[$Hll //]"); iIntros "Hll".
wp_apply (release_spec with "[-HΦ $Hlock $Hlocked]"); last eauto.
......@@ -190,8 +191,9 @@ Section channel.
rewrite /llist. eauto 10 with iFrame. }
iIntros (_). by wp_pures.
- iDestruct "HΦ" as "[_ >HΦ]". iDestruct "HΦ" as (vs') "[Hvs' HΦ]".
iDestruct (excl_eq with "Hvs Hvs'") as %<-%leibniz_equiv.
iMod (excl_update _ _ _ vs with "Hvs Hvs'") as "[Hvs Hvs']".
iDestruct (own_valid_2 with "Hvs Hvs'") as %<-%excl_auth_agreeL.
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_apply (lisnil_spec with "Hll"); iIntros "Hll". iMod "HΦ".
wp_apply (lpop_spec with "Hll"); iIntros (v') "[% Hll]"; simplify_eq/=.
......
......@@ -42,8 +42,7 @@ From actris.channel Require Export channel.
From actris.channel Require Import proto_model.
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth excl.
From actris.utils Require Import auth_excl.
From iris.algebra Require Import excl_auth.
Export action.
Definition start_chan : val := λ: "f",
......@@ -53,15 +52,15 @@ Definition start_chan : val := λ: "f",
(** * Setup of Iris's cameras *)
Class proto_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Σ := #[
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 Σ.
Proof. intros [??%subG_auth_exclG]%subG_inv. constructor; apply _. Qed.
Proof. intros [??%subG_inG]%subG_inv. constructor; apply _. Qed.
(** * Types *)
Definition iProto Σ := proto val (iPropO Σ) (iPropO Σ).
......@@ -230,16 +229,17 @@ Record proto_name := ProtName {
proto_r_name : gname
}.
Definition to_proto_auth_excl {Σ} (p : iProto Σ) :=
to_auth_excl (Next (proto_map id iProp_fold iProp_unfold p)).
Definition to_pre_proto {Σ} (p : iProto Σ) :
proto val (iPrePropO Σ) (iPrePropO Σ) :=
proto_map id iProp_fold iProp_unfold p.
Definition proto_own_frag `{!proto_chanG Σ} (γ : proto_name) (s : side)
(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)
(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 Σ :=
( l r pl pr,
......@@ -537,7 +537,7 @@ Section proto.
Proper (() ==> () ==> ()) (proto_interp (Σ:=Σ) vs).
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.
Global Instance proto_own_ne γ s : NonExpansive (proto_own_frag γ s).
Proof. solve_proper. Qed.
......@@ -551,9 +551,9 @@ Section proto.
Proof.
iIntros "Hauth Hfrag".
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.
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.
{ intros p''. rewrite -proto_map_compose -{2}(proto_map_id p'').
apply proto_map_ext=> // pc /=; by rewrite iProp_fold_unfold. }
......@@ -566,8 +566,7 @@ Section proto.
Proof.
iIntros "Hauth Hfrag".
iDestruct (own_update_2 with "Hauth Hfrag") as "H".
{ eapply (auth_update _ _ (to_proto_auth_excl p'') (to_proto_auth_excl p'')).
apply option_local_update. by apply exclusive_local_update. }
{ eapply (excl_auth_update _ _ (Next (to_pre_proto p''))). }
by rewrite own_op.
Qed.
......@@ -626,12 +625,12 @@ Section proto.
c1 p c2 iProto_dual p.
Proof.
iIntros "#Hcctx Hcol Hcor".
iMod (own_alloc ( (to_proto_auth_excl p)
(to_proto_auth_excl p))) as (lγ) "[Hlsta Hlstf]".
{ by apply auth_both_valid_2. }
iMod (own_alloc ( (to_proto_auth_excl (iProto_dual p))
(to_proto_auth_excl (iProto_dual p)))) as (rγ) "[Hrsta Hrstf]".
{ by apply auth_both_valid_2. }
iMod (own_alloc (E (Next (to_pre_proto p))
E (Next (to_pre_proto p)))) as (lγ) "[Hlsta Hlstf]".
{ by apply excl_auth_valid. }
iMod (own_alloc (E (Next (to_pre_proto (iProto_dual p)))
E (Next (to_pre_proto (iProto_dual p))))) as (rγ) "[Hrsta Hrstf]".
{ by apply excl_auth_valid. }
pose (ProtName cγ lγ rγ) as pγ.
iMod (inv_alloc protoN _ (proto_inv pγ) with "[-Hlstf Hrstf Hcctx]") as "#Hinv".
{ 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.
......@@ -17,7 +17,7 @@ To model this ghost theory construction, we use the camera
[auth (option (csum (positive * A) (excl unit)))]. *)
From iris.base_logic Require Export base_logic lib.iprop lib.own.
From iris.proofmode Require Export tactics.
From iris.algebra Require Import excl auth csum gmultiset frac_auth.
From iris.algebra Require Import excl auth csum gmultiset.
From iris.algebra Require Export local_updates.
Class contributionG Σ (A : ucmraT) `{!CmraDiscrete A} := {
......
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