Commit 43b7c428 authored by Ralf Jung's avatar Ralf Jung

update dependencies

parent a3c28a3c
Pipeline #25331 failed with stage
in 12 minutes and 38 seconds
......@@ -10,7 +10,7 @@ dev-repo: "git+https://gitlab.mpi-sws.org/iris/gpfsl.git"
synopsis: "A combination of GPS and FSL in the promising semantics WITHOUT promises"
depends: [
"coq-iris" { (= "dev.2020-03-13.1.ad82d138") | (= "dev") }
"coq-iris" { (= "dev.2020-03-16.0.62be0a86") | (= "dev") }
"coq-orc11" { (= "dev.2020-03-13.0.3a2bc1bd") | (= "dev") }
]
......
......@@ -26,7 +26,7 @@ Proof. solve_inG. Qed.
Lemma noprol_adequacy Σ `{noprolPreG Σ} e (σ: state) 𝓥 φ:
Wf σ
𝓥 σ.(mem)
( `{noprolG Σ} tid , WP e in tid {{ v, ⌜φ v }}%I)
( `{noprolG Σ} tid, WP e in tid {{ v, ⌜φ v }})
adequate NotStuck (e at 𝓥) σ (λ v _, φ v).
Proof.
intros WFσ H𝓥 Hwp; eapply (wp_adequacy _ _); iIntros (Hinv ?).
......@@ -69,7 +69,7 @@ Proof.
Qed.
Lemma noprol_adequacy' Σ `{noprolPreG Σ} e φ:
( `{noprolG Σ} tid , WP e in tid {{ v, ⌜φ v }}%I)
( `{noprolG Σ} tid, WP e in tid {{ v, ⌜φ v }})
adequate NotStuck (e at init_tview) (mkGB ) (λ v _, φ v).
Proof.
intros. eapply noprol_adequacy=>//. split=>//. split=> l /=.
......
......@@ -165,7 +165,7 @@ Qed.
Lemma cb_escrows_list_alloc Ns γ q (ni: nat):
(ni Ns)
(([ list] i seq (Z.to_nat b) ni, (q >> (i: nat)) #)
={escrowN}= [ list] i seq 0 ni, PE Ns γ q i)%I.
={escrowN}= [ list] i seq 0 ni, PE Ns γ q i).
Proof.
move => Le. iIntros "OL".
iApply big_sepL_fupd.
......
......@@ -205,7 +205,7 @@ Proof.
Qed.
Lemma Tok_is_unique γ :
(Tok γ - Tok γ - False : vProp)%I.
@{vPropI Σ} Tok γ - Tok γ - False.
Proof.
iIntros "t1 t2". iCombine "t1" "t2" as "t".
by iDestruct (own_valid with "t") as %?.
......@@ -213,7 +213,7 @@ Qed.
(* TODO: move *)
Lemma subjectively_sep (P1 P2: vProp) :
(<subj> P1 <subj> P2 <subj> (P1 P2))%I.
(<subj> P1 <subj> P2 <subj> (P1 P2)).
Proof.
iStartProof (iProp _). iIntros (?) "[P1 P2]".
rewrite monPred_subjectively_eq. simpl.
......
......@@ -516,8 +516,8 @@ Proof.
Qed.
Lemma Tkt_ghost_alloc :
(|==> γ,
Perms γ 0 AllTkts γ (firstMap C) [ set] i (setC C), MyTkt γ i None)%I.
|==> γ,
Perms γ 0 AllTkts γ (firstMap C) [ set] i (setC C), MyTkt γ i None.
Proof.
iMod (own_alloc (CoPset $ coPset_from_ex 0, ( (firstMap C) (firstMap C))))
as (γ) "Own".
......
......@@ -518,7 +518,7 @@ Section Properties.
Qed.
Lemma gps_ownA_alloc ζ t V rs:
(|==> γ, gps_ownA γ ζ t V rs Writer γ ζ exwr γ t 1%Qp naWrite γ V rs)%I.
|==> γ, gps_ownA γ ζ t V rs Writer γ ζ exwr γ t 1%Qp naWrite γ V rs.
Proof.
rewrite /gps_ownA /Writer /naWrite /exwr.
do 3 setoid_rewrite <- own_op. rewrite -4!pair_op /= 2!left_id_L -Some_op.
......@@ -606,7 +606,7 @@ Section Properties.
Qed.
Lemma gps_inv_vProp_own_loc_prim IW γ γF bs :
(gps_inv_vProp IP IW l γ γF bs - C, own_loc_prim l 1 C)%I.
gps_inv_vProp IP IW l γ γF bs - C, own_loc_prim l 1 C.
Proof.
iStartProof iProp. iIntros (V).
iDestruct 1 as (μ C tx Va rsa rsn ws) "(Hist & AT & AW & NA & ? & ? & ? & F)".
......
......@@ -57,7 +57,7 @@ Section proofs.
Global Instance na_inv_persistent p N (P : vProp) : Persistent (na_inv p N P).
Proof. rewrite /na_inv; apply _. Qed.
Lemma na_alloc : (|==> p, na_own p )%I.
Lemma na_alloc : |==> p, na_own p .
Proof.
rewrite /na_own. iDestruct (monPred_in_intro True%I with "[//]") as (V) "[HV _]".
iMod (own_alloc (to_ofe_funR (λ _, V))) as (p) "Own".
......
......@@ -43,7 +43,7 @@ Section RelAcqProp.
[by iApply own_unit|done].
Qed.
Lemma rel_True_intro tid : ((|==> {tid} True) : vPropI Σ)%I.
Lemma rel_True_intro tid : @{vPropI Σ} |==> {tid} True.
Proof. iApply rel_objectively_intro. by iIntros "!>". Qed.
Lemma rel_sep_objectively P Q tid :
......
......@@ -23,7 +23,7 @@ Proof.
Qed.
Lemma subj_inv_alloc_open N E P :
N E (|={E, E∖↑N}=> subj_inv N P (P ={E∖↑N, E}= True))%I.
N E |={E, E∖↑N}=> subj_inv N P (P ={E∖↑N, E}= True).
Proof.
intros. iStartProof (iProp _). rewrite subj_inv_eq. iIntros (V).
rewrite monPred_at_embed.
......
......@@ -95,8 +95,8 @@ Proof.
Qed.
Lemma view_inv_alloc_frac N E (q q': frac) (Eq: (q + q' = 1)%Qp):
(|={E}=> γ, view_tok γ q
(P: vProp), P ={E}= view_inv γ N P view_tok γ q')%I.
|={E}=> γ, view_tok γ q
(P: vProp), P ={E}= view_inv γ N P view_tok γ q'.
Proof.
iStartProof (iProp _). iIntros (V).
iMod (own_alloc ( Some (1%Qp, to_latT V) Some (1%Qp, to_latT V)))
......@@ -117,12 +117,12 @@ Proof.
Qed.
Lemma view_inv_alloc_half N E :
(|={E}=> γ, view_tok γ (1/2)
(P: vProp), P ={E}= view_inv γ N P view_tok γ (1/2))%I.
|={E}=> γ, view_tok γ (1/2)
(P: vProp), P ={E}= view_inv γ N P view_tok γ (1/2).
Proof. apply view_inv_alloc_frac. by rewrite Qp_div_2. Qed.
Lemma view_inv_alloc N E :
(|={E}=> γ, (P: vProp), P ={E}= view_inv γ N P view_tok γ 1%Qp)%I.
|={E}=> γ, (P: vProp), P ={E}= view_inv γ N P view_tok γ 1%Qp.
Proof.
iMod view_inv_alloc_half as (γ) "[tok Inv]".
iExists γ. iIntros "!>" (P) "P". iFrame "tok". by iApply ("Inv" with "P").
......@@ -130,7 +130,7 @@ Qed.
Lemma view_inv_alloc_open N E :
N E
(|={E}=> γ, P, |={E,E N}=> view_inv γ N P ( P ={E N,E}= view_tok γ 1%Qp))%I.
|={E}=> γ, P, |={E,E N}=> view_inv γ N P ( P ={E N,E}= view_tok γ 1%Qp).
Proof.
intros. iStartProof (iProp _). iIntros (V).
iMod (own_alloc ( Some (1%Qp, to_latT V) Some (1%Qp, to_latT V)))
......
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