diff --git a/opam b/opam
index fc8a5b8361693fc08e0b697b0bf7663985dffa52..e09ae8787b6bb4dd85da880b67a36e7839f5ce0e 100644
--- a/opam
+++ b/opam
@@ -10,5 +10,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/lrust'" ]
depends: [
- "coq-iris" { (= "dev.2017-09-20.3") | (= "dev") }
+ "coq-iris" { (= "dev.2017-09-25.0") | (= "dev") }
]
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 166130461bcf6fb15192e93f21872af20dcb247d..10ec7bbe63547e04116f929cda07c5c16e195299 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -452,20 +452,20 @@ Section arc.
+ iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
iExists _. iMod (own_update_2 with "Hâ— Hown") as "$".
{ apply auth_update_dealloc, prod_local_update_2,
- (cancel_local_update_empty 1%nat), _. }
+ (cancel_local_update_unit 1%nat), _. }
iExists _. iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
+ iFrame. iApply "Hclose1". iExists _. auto with iFrame.
- iDestruct "H" as "[? >$]". iIntros "!>"; iSplit; iIntros "Hl1".
+ iMod ("Hclose1" with "[>-]") as "_"; last iLeft; auto with lia.
iExists _. iMod (own_update_2 with "Hâ— Hown") as "$".
{ apply auth_update_dealloc, prod_local_update_2,
- (cancel_local_update_empty 1%nat), _. }
+ (cancel_local_update_unit 1%nat), _. }
iFrame. by replace (S (S weak) - 1) with (S weak:Z) by lia.
+ iFrame. iApply "Hclose1". iExists _. auto with iFrame.
- iDestruct "H" as "(>? & >$ & HP2)". iIntros "!>"; iSplit; iIntros "Hl1".
+ iMod (own_update_2 with "Hâ— Hown") as "Hâ—".
{ apply auth_update_dealloc, prod_local_update_2,
- (cancel_local_update_empty 1%nat), _. }
+ (cancel_local_update_unit 1%nat), _. }
destruct weak as [|weak].
* iMod ("Hclose1" with "[Hâ—]") as "_"; last by auto with iFrame.
iExists _. iFrame.
@@ -519,7 +519,7 @@ Section arc.
+ destruct Hqq' as [<- ->].
iMod (own_update_2 with "Hâ— Hown") as "[Hâ— Hâ—¯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
- etrans; first apply cancel_local_update_empty, _.
+ etrans; first apply cancel_local_update_unit, _.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[Hâ— Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
iModIntro. wp_case. iApply wp_fupd. wp_op=>[_|//].
@@ -528,7 +528,7 @@ Section arc.
rewrite -[in (_, _)](Pos.succ_pred s) // -[wl in Cinl (_, wl)]left_id
-Pos.add_1_l -2!pair_op -Cinl_op Some_op.
iMod (own_update_2 _ _ _ _ with "Hâ— Hown") as "Hâ—".
- { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_empty, _. }
+ { apply auth_update_dealloc, prod_local_update_1, @cancel_local_update_unit, _. }
iMod ("Hclose" with "[- HΦ]") as "_".
{ iExists _. iFrame. iExists (q + q'')%Qp. iFrame. iSplit; last by destruct s.
iIntros "!> !%". rewrite assoc -Hq''. f_equal. apply comm, _. }
@@ -552,7 +552,7 @@ Section arc.
- wp_apply (wp_cas_int_suc with "Hs"); first done. iIntros "Hs".
destruct Hqq' as [<- ->]. iMod (own_update_2 with "Hâ— Hown") as "[Hâ— Hâ—¯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
- etrans; first apply cancel_local_update_empty, _.
+ etrans; first apply cancel_local_update_unit, _.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iMod ("Hclose" with "[Hâ— Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
iApply ("HΦ" $! true). rewrite -{1}Hq''. iFrame. by iApply close_last_strong.
@@ -615,7 +615,7 @@ Section arc.
+ setoid_subst. iDestruct "H" as (?) "(Hq & ? & ? & >? & >%)". subst. wp_read.
iMod (own_update_2 with "Hâ— Hâ—¯") as "Hâ—".
{ apply auth_update_dealloc. rewrite -{1}[(_, 0%nat)]right_id.
- apply cancel_local_update_empty, _. }
+ apply cancel_local_update_unit, _. }
iMod ("Hclose" with "[Hâ—]") as "_"; first by iExists _; iFrame.
iModIntro. wp_seq. wp_op=>[_|//]. wp_let. wp_op. wp_write. iApply "HΦ".
iDestruct "Hq" as %<-. iFrame.
@@ -643,7 +643,7 @@ Section arc.
- wp_apply (wp_cas_int_suc with "Hs")=>//. iIntros "Hs".
destruct Hqq' as [<- ->]. iMod (own_update_2 with "Hâ— Hown") as "[Hâ— Hâ—¯]".
{ apply auth_update, prod_local_update_1. rewrite -[x in (x, _)]right_id.
- etrans; first apply cancel_local_update_empty, _.
+ etrans; first apply cancel_local_update_unit, _.
by apply (op_local_update _ _ (Some (Cinr (Excl ())))). }
iCombine "HP1" "HP1'" as "HP1". rewrite Hq''. clear Hq'' q''.
iMod ("Hclose" with "[Hâ— Hs Hw]") as "_"; first by iExists _; do 2 iFrame.
@@ -668,4 +668,4 @@ Section arc.
Qed.
End arc.
-Typeclasses Opaque is_arc arc_tok weak_tok.
\ No newline at end of file
+Typeclasses Opaque is_arc arc_tok weak_tok.
diff --git a/theories/lifetime/model/faking.v b/theories/lifetime/model/faking.v
index 0714e38e31110531884a34cccb37dd9dbe958245..dfb8359c6aaa9c19a39ef298fe59f4caf736877a 100644
--- a/theories/lifetime/model/faking.v
+++ b/theories/lifetime/model/faking.v
@@ -21,7 +21,7 @@ Proof.
iMod (own_alloc ((◠∅ ⋅ ◯ ∅) :auth (gmap slice_name
(frac * agree bor_stateC)))) as (γbor) "[Hbor Hbor']";
first by apply auth_valid_discrete_2.
- iMod (own_alloc ((◠∅) :auth (gset_disj slice_name)))
+ iMod (own_alloc ((◠ε) :auth (gset_disj slice_name)))
as (γinh) "Hinh"; first by done.
set (γs := LftNames γbor γcnt γinh).
iMod (own_update with "HI") as "[HI Hγs]".
diff --git a/theories/lifetime/model/primitive.v b/theories/lifetime/model/primitive.v
index 54daebe3797c2d929dab3e1c3bc355d7e1066126..a4c995fc218d1baad5adbc8133dc846621f0360d 100644
--- a/theories/lifetime/model/primitive.v
+++ b/theories/lifetime/model/primitive.v
@@ -452,7 +452,7 @@ Proof.
iModIntro. iSplitL "Hbox HE".
{ iNext. rewrite /lft_inh. iExists ({[γE]} ∪ PE).
rewrite to_gmap_union_singleton. iFrame. }
- clear dependent PE. rewrite -(left_id_L ∅ op (◯ GSet {[γE]})).
+ clear dependent PE. rewrite -(left_id_L ε op (◯ GSet {[γE]})).
iDestruct "HEâ—¯" as "[HEâ—¯' HEâ—¯]". iSplitL "HEâ—¯'".
{ iIntros (I) "HI". iApply (own_inh_auth with "HI HEâ—¯'"). }
iIntros (Q'). rewrite {1}/lft_inh. iDestruct 1 as (PE) "[>HE Hbox]".
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index 123029972f8c15f41b31ecf44f6ad81cf3400138..4835e61ec5f6037e1bc4b8abf51fe5ea2efa1c82 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -290,7 +290,7 @@ Section code.
-- iLeft. iSplit; first done. rewrite Hincls. iFrame "Hl†".
iMod (own_update_2 with "Hst Htok") as "Hst".
{ apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
- apply cancel_local_update_empty, _. }
+ apply cancel_local_update_unit, _. }
rewrite -[in (1).[ν]%I]Hqq' -[(|={∅,⊤}=>_)%I]fupd_trans.
iApply step_fupd_mask_mono;
last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
@@ -309,7 +309,7 @@ Section code.
iModIntro. iNext. iMod "H†". iMod ("Hν†" with "H†") as "Hty". iModIntro.
iMod (own_update_2 with "Hst Htok") as "Hst".
{ apply auth_update_dealloc, prod_local_update_1,
- (cancel_local_update_empty (Some _) None). }
+ (cancel_local_update_unit (Some _) None). }
iSplitL "Hty".
{ iDestruct "Hty" as (vy) "[H Hty]". iExists vy. iFrame.
by iApply "Hinclo". }
@@ -319,7 +319,7 @@ Section code.
* iIntros "Hl1".
iMod (own_update_2 with "Hst Htok") as "[Hst Htok]".
{ apply auth_update. etrans.
- - rewrite [(Some _, weak)]pair_split. apply cancel_local_update_empty, _.
+ - rewrite [(Some _, weak)]pair_split. apply cancel_local_update_unit, _.
- apply (op_local_update _ _ (Some (Cinr (Excl tt)), 0%nat)). auto. }
rewrite -[(|={∅,⊤}=>_)%I]fupd_trans -[in (1).[ν]%I]Hqq'.
iApply step_fupd_mask_mono;
@@ -343,14 +343,14 @@ Section code.
iApply ("Hclose" with "[>- $Hna]"). iExists (None, 0%nat).
iMod (own_update_2 with "Hst Htok") as "$"; last done.
apply auth_update_dealloc. rewrite -{1}(right_id (None, 0%nat) _ (_, _)).
- apply cancel_local_update_empty, _.
+ apply cancel_local_update_unit, _.
-- iRight. iSplitR; first by auto with lia. iIntros "!> Hl†Hl2 Hvl".
iApply ("Hclose" with "[>- $Hna]"). iExists (None, S weak).
rewrite Hincls. iFrame. iSplitR "Hl2"; last first.
{ simpl. destruct Pos.of_succ_nat; rewrite /= ?Pos.pred_double_succ //. }
iMod (own_update_2 with "Hst Htok") as "$"; last done.
apply auth_update_dealloc, prod_local_update', reflexivity.
- rewrite -{1}(right_id None _ (Some _)). apply cancel_local_update_empty, _.
+ rewrite -{1}(right_id None _ (Some _)). apply cancel_local_update_unit, _.
+ apply csum_included in Hincl.
destruct Hincl as [->|[(?&(?,?)&[=<-]&->&(q',strong)&[]%(inj2 pair))|
(?&?&[=]&?)]]; first done. setoid_subst.
@@ -362,7 +362,7 @@ Section code.
* iMod (own_update_2 with "Hst Htok") as "Hst".
{ apply auth_update_dealloc.
rewrite -pair_op -Cinl_op Some_op -{1}(left_id 0%nat _ weak) -pair_op.
- apply (cancel_local_update_empty _ (_, _)). }
+ apply (cancel_local_update_unit _ (_, _)). }
iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
iSplitL; first last.
{ rewrite [(_+_)%Qp]assoc [(q'+_)%Qp]comm. auto. }
diff --git a/theories/typing/lib/rc/weak.v b/theories/typing/lib/rc/weak.v
index 4e50af06d3d9102ed2c852ca1cfcbfc93ae9d2c5..992f8b234d9172dbeb80055298c31557be1e1771 100644
--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -404,7 +404,7 @@ Section code.
destruct weakc; first by simpl in *; lia.
iMod (own_update_2 with "Hrcâ— Hwtok") as "Hrcâ—".
{ apply auth_update_dealloc, prod_local_update_2,
- (cancel_local_update_empty 1%nat), _. }
+ (cancel_local_update_unit 1%nat), _. }
destruct st as [[[q'' strong]| |]|]; try done.
- iExists _. iDestruct "Hrcst" as (q0) "(Hlw & >$ & Hrcst)". iRight.
iSplitR; first by auto with lia. iIntros "!>?". iApply "Hclose". iFrame.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 87012a873bb7fa74f639dc196f6e91b4d0766d1f..ca36f8eab0d6cc56facec2e26310d295347f41d1 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -177,7 +177,7 @@ Section ref_functions.
- destruct Heq as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
iExists None. iFrame. iMod (own_update with "Hâ—â—¯") as "$".
{ apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
- apply cancel_local_update_empty, _. }
+ apply cancel_local_update_unit, _. }
iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
- destruct Hincl as [ [=] |[ (?&?&[=]&?) | (?&?&[=<-]&[=<-]&[[q0 n']EQ]) ]].
destruct EQ as [?%leibniz_equiv ?%leibniz_equiv]. simpl in *. subst.
@@ -186,7 +186,7 @@ Section ref_functions.
iExists (Some (_, Cinr (q0, n'))). iFrame. iMod (own_update with "Hâ—â—¯") as "$".
{ apply auth_update_dealloc.
rewrite -(agree_idemp (to_agree _)) -pair_op -Cinr_op -pair_op Some_op.
- apply (cancel_local_update_empty (reading_st q ν)), _. }
+ apply (cancel_local_update_unit (reading_st q ν)), _. }
iExists ν. iFrame. iApply step_fupd_intro; first set_solver. iIntros "!>".
iSplitR; first done. iExists (q+q'')%Qp. iFrame.
by rewrite assoc (comm _ q0 q). }
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index acc5cc5b6b0ab94d273889a6b75b1ecccb36c787..396713e73cbecbd762d25fea91f0dd33defd48b6 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -138,7 +138,7 @@ Section refmut_functions.
iMod ("Hcloseβ" with "[> H↦lrc H◠H◯ Hb] Hna") as "[Hβ Hna]".
{ iExists None. iFrame. iMod (own_update_2 with "Hâ— Hâ—¯") as "$"; last done.
apply auth_update_dealloc. rewrite -(right_id None _ (Some _)).
- apply cancel_local_update_empty, _. }
+ apply cancel_local_update_unit, _. }
iMod ("Hcloseα" with "Hβ") as "Hα". iMod ("Hclose" with "Hα HL") as "HL". wp_seq.
iApply (type_type _ _ _ [ #lx â— box (uninit 2)]
with "[] LFT HE Hna HL Hk"); last first.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index 5e3905c02b1e40ffe984b2579285943403b53631..9a6f357382380c9595adce8710acb92bd77be449 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -100,7 +100,7 @@ Section rwlockreadguard_functions.
iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
iMod ("Hh" with "H†") as "Hb". iIntros "!> Hlx". iExists None. iFrame.
iApply (own_update_2 with "Hâ— Hâ—¯"). apply auth_update_dealloc.
- rewrite -(right_id None op (Some _)). apply cancel_local_update_empty, _.
+ rewrite -(right_id None op (Some _)). apply cancel_local_update_unit, _.
- iApply step_fupd_intro. set_solver. iNext. iIntros "Hlx".
apply csum_included in Hle.
destruct Hle as [|[(?&?&[=]&?)|(?&[[agν q']n]&[=<-]&->&Hle%prod_included)]];
@@ -118,7 +118,7 @@ Section rwlockreadguard_functions.
assert (n = 1%positive â‹… Pos.pred n) as EQn.
{ rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
rewrite {1}EQn -{1}(agree_idemp (to_agree _)) -2!pair_op -Cinr_op Some_op.
- apply (cancel_local_update_empty (reading_st q ν)) , _. }
+ apply (cancel_local_update_unit (reading_st q ν)) , _. }
iApply (wp_step_fupd with "INV"). done. set_solver.
iApply (wp_cas_int_suc with "Hlx"); try done. iNext. iIntros "Hlx INV !>".
iMod ("INV" with "Hlx") as "INV". iMod ("Hcloseβ" with "[$INV]") as "Hβ".
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard_code.v b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
index 548fe054bf5a19e9073dcf9fdbbc0ea22c17f6ca..bc97a8042f3cc0efa6cee6937b2152b0e7672184 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard_code.v
@@ -131,7 +131,7 @@ Section rwlockwriteguard_functions.
destruct st0 as [[[]|]| |]; try by inversion Heq.
iExists None. iFrame. iMod (own_update_2 with "Hâ— Hâ—¯") as "$"; last done.
apply auth_update_dealloc. rewrite -(right_id None op (Some _)).
- apply cancel_local_update_empty, _. }
+ apply cancel_local_update_unit, _. }
iModIntro. wp_seq. iMod ("Hcloseα" with "Hβ") as "Hα".
iMod ("Hclose" with "Hα HL") as "HL".
iApply (type_type _ _ _ [ x â— box (uninit 1)]