From c623527141b79324fbdd048f19c631ed9e694ba8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 16 Feb 2021 13:28:14 +0100
Subject: [PATCH] update dependencies

---
 coq-lambda-rust.opam                              |  2 +-
 theories/lang/lifting.v                           |  4 ++--
 theories/lifetime/frac_borrow.v                   |  2 +-
 theories/lifetime/model/accessors.v               |  8 ++++----
 theories/typing/lib/arc.v                         | 14 +++++++-------
 theories/typing/lib/mutex/mutexguard.v            |  2 +-
 theories/typing/lib/rc/rc.v                       |  6 +++---
 theories/typing/lib/refcell/refcell_code.v        |  4 ++--
 theories/typing/lib/rwlock/rwlockreadguard_code.v |  2 +-
 theories/typing/util.v                            |  4 ++--
 10 files changed, 24 insertions(+), 24 deletions(-)

diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index ba62ac1d..9df7c6cf 100644
--- a/coq-lambda-rust.opam
+++ b/coq-lambda-rust.opam
@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2021-02-14.0.842fb394") | (= "dev") }
+  "coq-iris" { (= "dev.2021-02-16.0.8ee71fff") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index b6bff0b0..3620d5d9 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -178,7 +178,7 @@ Lemma wp_read_na E l q v :
 Proof.
   iIntros (Φ) ">Hv HΦ". iApply wp_lift_head_step; auto. iIntros (σ1 κ κs n) "Hσ".
   iMod (heap_read_na with "Hσ Hv") as (m) "(% & Hσ & Hσclose)".
-  iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
+  iMod (fupd_mask_subseteq ∅) as "Hclose"; first set_solver.
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
   iModIntro. iFrame "Hσ". iSplit; last done.
@@ -211,7 +211,7 @@ Proof.
   iIntros (<- Φ) ">Hv HΦ".
   iApply wp_lift_head_step; auto. iIntros (σ1 κ κs n) "Hσ".
   iMod (heap_write_na with "Hσ Hv") as "(% & Hσ & Hσclose)".
-  iMod (fupd_intro_mask' _ ∅) as "Hclose"; first set_solver.
+  iMod (fupd_mask_subseteq ∅) as "Hclose"; first set_solver.
   iModIntro; iSplit; first by eauto.
   iNext; iIntros (e2 σ2 efs Hstep); inv_head_step. iMod "Hclose" as "_".
   iModIntro. iFrame "Hσ". iSplit; last done.
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index b571f34e..d981e6fa 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -64,7 +64,7 @@ Section frac_bor.
     - iLeft. iDestruct "Hφ" as (q) "(Hφ & Hγ & H)". iExists q. iFrame.
       iIntros "!>Hφ". iApply "Hclose". iExists q. iFrame.
     - iRight. iMod "Hclose" as "_". iMod (lft_incl_dead with "Hκκ' H†") as "$". done.
-      iApply fupd_intro_mask. set_solver. done.
+      iApply fupd_mask_intro_subseteq. set_solver. done.
   Qed.
 
   Local Lemma frac_bor_trade1 γ κ' q :
diff --git a/theories/lifetime/model/accessors.v b/theories/lifetime/model/accessors.v
index f23850bc..913c8dd0 100644
--- a/theories/lifetime/model/accessors.v
+++ b/theories/lifetime/model/accessors.v
@@ -128,7 +128,7 @@ Proof.
     iMod (slice_empty _ _ true with "Hs Hbox") as "[HP' Hbox]".
       solve_ndisj. by rewrite lookup_fmap EQB.
     iDestruct ("HPP'" with "HP'") as "$".
-    iMod fupd_intro_mask' as "Hclose"; last iIntros "!>HP'". solve_ndisj.
+    iMod fupd_mask_subseteq as "Hclose"; last iIntros "!>HP'". solve_ndisj.
     iDestruct ("HPP'" with "HP'") as "HP".
     iMod "Hclose" as "_". iMod (slice_fill _ _ true with "Hs HP Hbox") as "Hbox".
       solve_ndisj. by rewrite lookup_insert. iFrame.
@@ -140,7 +140,7 @@ Proof.
     iMod ("Hclose'" with "[-Hbor]") as "_".
     + iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
     + iMod (lft_incl_dead with "Hle H†"). done. iFrame.
-      iApply fupd_intro_mask'. solve_ndisj.
+      iApply fupd_mask_subseteq. solve_ndisj.
 Qed.
 
 (** Basic borrows  *)
@@ -234,7 +234,7 @@ Proof.
       as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
     iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
       solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
-    iMod fupd_intro_mask' as "Hclose"; last iIntros "!>* HvsQ HQ". solve_ndisj.
+    iMod fupd_mask_subseteq as "Hclose"; last iIntros "!>* HvsQ HQ". solve_ndisj.
     iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
     { iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
     iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
@@ -259,6 +259,6 @@ Proof.
     iMod ("Hclose'" with "[-Hbor]") as "_".
     + iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". eauto.
     + iMod (lft_incl_dead with "Hle H†") as "$". done.
-      iApply fupd_intro_mask'. solve_ndisj.
+      iApply fupd_mask_subseteq. solve_ndisj.
 Qed.
 End accessors.
diff --git a/theories/typing/lib/arc.v b/theories/typing/lib/arc.v
index 95ed3014..cb9d8f8e 100644
--- a/theories/typing/lib/arc.v
+++ b/theories/typing/lib/arc.v
@@ -91,7 +91,7 @@ Section arc.
     { apply disjoint_union_l. split; solve_ndisj. }
     iMod ("Hν†" with "Hν") as "H". iModIntro. iNext. iApply fupd_trans.
     iMod "H" as "#Hν".
-    iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hvs" with "Hν") as "$".
+    iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hvs" with "Hν") as "$".
     { set_solver-. }
     iIntros "{$Hν} !>".
     iMod "Hclose2" as "_". iApply "Hclose". auto.
@@ -486,7 +486,7 @@ Section arc.
        with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
     { iIntros "!# Hα".
       iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
-      iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
+      iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
@@ -529,7 +529,7 @@ Section arc.
        with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
     { iIntros "!# Hα".
       iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
-      iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
+      iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros (c) "[Hα _]". iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
@@ -574,7 +574,7 @@ Section arc.
        with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
     { iIntros "!# Hα".
       iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
-      iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
+      iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros (q'') "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
@@ -618,7 +618,7 @@ Section arc.
        with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
     { iIntros "!# Hα".
       iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
-      iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
+      iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
@@ -662,7 +662,7 @@ Section arc.
               with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
     { iIntros "!# Hα".
       iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>Htok Hclose1]"; [solve_ndisj..|].
-      iExists _. iFrame. iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
+      iExists _. iFrame. iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros "[Hα Hown]". wp_seq. iMod ("Hclose1" with "Hα HL") as "HL".
     (* Finish up the proof. *)
@@ -709,7 +709,7 @@ Section arc.
               with "[] [] [$Hα1 $Hα2]"); first by iDestruct "Hpersist" as "[$ _]".
     { iIntros "!# Hα".
       iMod (at_bor_acc_tok with "LFT Hrctokb Hα") as "[>$ Hclose1]"; [solve_ndisj..|].
-      iMod fupd_intro_mask' as "Hclose2"; last iModIntro. set_solver.
+      iMod fupd_mask_subseteq as "Hclose2"; last iModIntro. set_solver.
       iIntros "Htok". iMod "Hclose2" as "_". by iApply "Hclose1". }
     iIntros ([] q') "[Hα Hown]"; wp_if; iMod ("Hclose1" with "Hα HL") as "HL".
     - (* Finish up the proof (sucess). *)
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index a8dca25c..0bb64a00 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -151,7 +151,7 @@ Section code.
     (* FIXME: This should work: iIntros (?? R). *) intros ?? R.
     iIntros "#LFT #Hshr #Hlincl !# Htok".
     iMod (at_bor_acc_tok with "LFT Hshr Htok") as "[Hproto Hclose1]"; [done..|].
-    iMod (fupd_intro_mask') as "Hclose2"; last iModIntro; first solve_ndisj.
+    iMod (fupd_mask_subseteq) as "Hclose2"; last iModIntro; first solve_ndisj.
     iFrame. iIntros "Hproto". iMod "Hclose2" as "_".
     iMod ("Hclose1" with "Hproto") as "$". done.
   Qed.
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index a02cd0c7..863d659c 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -298,7 +298,7 @@ Section code.
              iApply step_fupd_mask_mono;
                last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
              iModIntro. iNext. iMod "H†".
-             iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
+             iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
              { set_solver-. }
              iMod "Hclose2" as "_". iModIntro.
              iMod ("Hclose" with "[Hst $Hna]") as "$"; first by iExists _; iFrame.
@@ -313,7 +313,7 @@ Section code.
                 iApply step_fupd_mask_mono;
                   last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
                 iModIntro. iNext. iMod "H†".
-                iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
+                iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
                 { set_solver-. }
                 iMod "Hclose2" as "_". iModIntro.
                 iMod (own_update_2 with "Hst Htok") as "Hst".
@@ -334,7 +334,7 @@ Section code.
           iApply step_fupd_mask_mono;
             last iMod ("Hνend" with "[$Hν $Hν1]") as "H†"; try done.
           iModIntro. iNext. iMod "H†".
-          iMod fupd_intro_mask' as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
+          iMod fupd_mask_subseteq as "Hclose2"; last iMod ("Hν†" with "H†") as "Hty".
           { set_solver-. }
           iMod "Hclose2" as "_". iModIntro.
           iMod ("Hclose" with "[Hst $Hna Hl1 Hl2]") as "$";
diff --git a/theories/typing/lib/refcell/refcell_code.v b/theories/typing/lib/refcell/refcell_code.v
index 881ba5c6..85f3629e 100644
--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -203,7 +203,7 @@ Section refcell_functions.
           iSplitR "Htok2".
           + iIntros "!> Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro.
             iNext. iMod "Hν".
-            iMod fupd_intro_mask' as "Hclose"; last iMod ("Hh" with "[Hν]") as "$".
+            iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hh" with "[Hν]") as "$".
             { set_solver-. }
             * rewrite -lft_dead_or. auto.
             * done.
@@ -283,7 +283,7 @@ Section refcell_functions.
       iModIntro. iMod ("Hclose''" with "[Hlx Hownst Hbh Htok1] Hna") as "[Hβtok Hna]".
       { iExists _. iFrame. iNext. iSplitL "Hbh".
         - iIntros "Hν". iMod ("Hhν" with "Hν") as "Hν". iModIntro. iNext. iMod "Hν".
-          iMod fupd_intro_mask' as "Hclose"; last iMod ("Hbh" with "[Hν]") as "$".
+          iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hbh" with "[Hν]") as "$".
           { set_solver-. }
           * rewrite -lft_dead_or. auto.
           * done.
diff --git a/theories/typing/lib/rwlock/rwlockreadguard_code.v b/theories/typing/lib/rwlock/rwlockreadguard_code.v
index d4115119..20c1ab6c 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard_code.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard_code.v
@@ -101,7 +101,7 @@ Section rwlockreadguard_functions.
           { (* FIXME [solve_ndisj] fails. *)
             apply: disjoint_difference_r1. done. }
           iMod ("H†" with "Hν") as "H†". iModIntro. iNext. iMod "H†".
-          iMod fupd_intro_mask' as "Hclose"; last iMod ("Hh" with "H†") as "Hb".
+          iMod fupd_mask_subseteq as "Hclose"; last iMod ("Hh" with "H†") as "Hb".
           { set_solver-. }
           iMod "Hclose" as "_". iIntros "!> Hlx". iExists None. iFrame.
           iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
diff --git a/theories/typing/util.v b/theories/typing/util.v
index 7a6344d7..c120c7ba 100644
--- a/theories/typing/util.v
+++ b/theories/typing/util.v
@@ -42,7 +42,7 @@ Section util.
       iModIntro. iNext. iMod "Hdelay" as "[Hb Htok]".
       iMod (ty.(ty_share) with "LFT Hb Htok") as "[#$ $]"; first solve_ndisj.
       iApply "Hclose". auto.
-    - iMod fupd_intro_mask' as "Hclose'"; first solve_ndisj. iModIntro.
+    - iMod fupd_mask_subseteq as "Hclose'"; first solve_ndisj. iModIntro.
       iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
 
@@ -65,7 +65,7 @@ Section util.
       iMod (ty.(ty_share) with "LFT [Hb] Htok") as "[#Hshr $]"; first solve_ndisj.
       { iApply bor_shorten; done. }
       iMod ("Hclose" with "[]") as "_"; auto.
-    - iMod fupd_intro_mask' as "Hclose'"; last iModIntro; first solve_ndisj.
+    - iMod fupd_mask_subseteq as "Hclose'"; last iModIntro; first solve_ndisj.
       iNext. iMod "Hclose'" as "_". iMod ("Hclose" with "[]") as "_"; by eauto.
   Qed.
 End util.
-- 
GitLab