From 9c3c76d3efc732ac51c1153b90f25f72c46bcd7c Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 2 May 2023 22:09:49 +0200
Subject: [PATCH] Bump Iris; bump minimal Coq version to 8.17.

---
 .gitlab-ci.yml                        |  6 +++---
 README.md                             |  2 +-
 coq-lambda-rust.opam                  |  2 +-
 theories/lang/adequacy.v              |  6 +++---
 theories/lang/heap.v                  |  6 +++---
 theories/lang/lang.v                  |  2 +-
 theories/lang/lib/arc.v               |  2 +-
 theories/lang/lib/spawn.v             |  2 +-
 theories/lang/lifting.v               |  2 +-
 theories/lang/races.v                 |  2 +-
 theories/lifetime/frac_borrow.v       |  2 +-
 theories/lifetime/meta.v              |  2 +-
 theories/lifetime/model/definitions.v | 24 ++++++++++++------------
 theories/typing/lib/brandedvec.v      |  4 ++--
 theories/typing/lib/ghostcell.v       |  4 ++--
 theories/typing/lib/rc/rc.v           |  2 +-
 theories/typing/lib/refcell/refcell.v |  2 +-
 theories/typing/lib/rwlock/rwlock.v   |  2 +-
 theories/typing/soundness.v           |  8 ++++----
 theories/typing/type.v                |  8 ++++----
 20 files changed, 45 insertions(+), 45 deletions(-)

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 20000068..e82d49df 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -28,10 +28,10 @@ variables:
 
 ## Build jobs
 
-build-coq.8.15.1:
+build-coq.8.17.0:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.15.1"
+    OPAM_PINS: "coq version 8.17.0"
     DENY_WARNINGS: "1"
     MANGLE_NAMES: "1"
   tags:
@@ -40,7 +40,7 @@ build-coq.8.15.1:
 trigger-iris.timing:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.15.1   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
+    OPAM_PINS: "coq version 8.17.0   git+https://gitlab.mpi-sws.org/$IRIS_REPO#$IRIS_REV"
   tags:
   - fp-timing
   only:
diff --git a/README.md b/README.md
index e51dd406..d7439865 100644
--- a/README.md
+++ b/README.md
@@ -6,7 +6,7 @@ This is the Coq development accompanying lambda-Rust.
 
 This version is known to compile with:
 
- - Coq 8.15.1
+ - Coq 8.17.0
  - A development version of [Iris](https://gitlab.mpi-sws.org/iris/iris)
 
 ## Building from source
diff --git a/coq-lambda-rust.opam b/coq-lambda-rust.opam
index 862ba524..a1facd94 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.2023-03-09.0.f91e8eab") | (= "dev") }
+  "coq-iris" { (= "dev.2023-05-02.4.943e9b74") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]
diff --git a/theories/lang/adequacy.v b/theories/lang/adequacy.v
index ec4b64cd..5fdf7378 100644
--- a/theories/lang/adequacy.v
+++ b/theories/lang/adequacy.v
@@ -5,9 +5,9 @@ From lrust.lang Require Import proofmode notation.
 From iris.prelude Require Import options.
 
 Class lrustGpreS Σ := HeapGpreS {
-  lrustGpreS_irig :> invGpreS Σ;
-  lrustGpreS_heap :> inG Σ (authR heapUR);
-  lrustGpreS_heap_freeable :> inG Σ (authR heap_freeableUR)
+  lrustGpreS_irig :: invGpreS Σ;
+  lrustGpreS_heap :: inG Σ (authR heapUR);
+  lrustGpreS_heap_freeable :: inG Σ (authR heap_freeableUR)
 }.
 
 Definition lrustΣ : gFunctors :=
diff --git a/theories/lang/heap.v b/theories/lang/heap.v
index 4836e47f..e3f918db 100644
--- a/theories/lang/heap.v
+++ b/theories/lang/heap.v
@@ -19,8 +19,8 @@ Definition heap_freeableUR : ucmra :=
   gmapUR block (prodR fracR (gmapR Z (exclR unitO))).
 
 Class heapGS Σ := HeapGS {
-  heap_inG :> inG Σ (authR heapUR);
-  heap_freeable_inG :> inG Σ (authR heap_freeableUR);
+  heap_inG :: inG Σ (authR heapUR);
+  heap_freeable_inG :: inG Σ (authR heap_freeableUR);
   heap_name : gname;
   heap_freeable_name : gname
 }.
@@ -274,7 +274,7 @@ Section heap.
   Proof. revert i. induction n as [|n IH]=>i; first done. by apply insert_valid. Qed.
 
   Lemma heap_freeable_op_eq l q1 q2 n n' :
-    †{q1}l…n ∗ †{q2}l+ₗn … n' ⊣⊢ †{q1+q2}l…(n+n').
+    †{q1}l…n ∗ †{q2}l +ₗ n … n' ⊣⊢ †{q1+q2}l…(n+n').
   Proof.
     by rewrite heap_freeable_eq /heap_freeable_def -own_op -auth_frag_op
       singleton_op -pair_op inter_op.
diff --git a/theories/lang/lang.v b/theories/lang/lang.v
index 47f69d9b..16a15295 100644
--- a/theories/lang/lang.v
+++ b/theories/lang/lang.v
@@ -402,7 +402,7 @@ Lemma shift_loc_0_nat l : l +â‚— 0%nat = l.
 Proof. destruct l as [b o]. rewrite /shift_loc /=. f_equal. lia. Qed.
 
 Global Instance shift_loc_inj l : Inj (=) (=) (shift_loc l).
-Proof. destruct l as [b o]; intros n n' [=?]; lia. Qed.
+Proof. destruct l as [b o]; intros n n' [= ?]; lia. Qed.
 
 Lemma shift_loc_block l n : (l +â‚— n).1 = l.1.
 Proof. done. Qed.
diff --git a/theories/lang/lib/arc.v b/theories/lang/lib/arc.v
index 305e4000..5b4e7d9d 100644
--- a/theories/lang/lib/arc.v
+++ b/theories/lang/lib/arc.v
@@ -108,7 +108,7 @@ Definition arc_stR :=
   prodUR (optionUR (csumR (prodR (prodR fracR positiveR) (optionR (exclR unitO)))
                           (exclR unitO))) natUR.
 Class arcG Σ :=
-  RcG :> inG Σ (authR arc_stR).
+  RcG :: inG Σ (authR arc_stR).
 Definition arcΣ : gFunctors := #[GFunctor (authR arc_stR)].
 Global Instance subG_arcΣ {Σ} : subG arcΣ Σ → arcG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/lang/lib/spawn.v b/theories/lang/lib/spawn.v
index b176e3f3..07a32237 100644
--- a/theories/lang/lib/spawn.v
+++ b/theories/lang/lib/spawn.v
@@ -28,7 +28,7 @@ Definition join : val :=
       "join" ["c"].
 
 (** The CMRA & functor we need. *)
-Class spawnG Σ := SpawnG { spawn_tokG :> inG Σ (exclR unitO) }.
+Class spawnG Σ := SpawnG { spawn_tokG :: inG Σ (exclR unitO) }.
 Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
 
 Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
diff --git a/theories/lang/lifting.v b/theories/lang/lifting.v
index 76a60e18..ae3b1cb4 100644
--- a/theories/lang/lifting.v
+++ b/theories/lang/lifting.v
@@ -8,7 +8,7 @@ Import uPred.
 
 Class lrustGS Σ := LRustGS {
   lrustGS_invGS : invGS Σ;
-  lrustGS_heapGS :> heapGS Σ
+  lrustGS_heapGS :: heapGS Σ
 }.
 
 Global Instance lrustGS_irisGS `{!lrustGS Σ} : irisGS lrust_lang Σ := {
diff --git a/theories/lang/races.v b/theories/lang/races.v
index 0c0f6ca7..501581fd 100644
--- a/theories/lang/races.v
+++ b/theories/lang/races.v
@@ -144,7 +144,7 @@ Proof.
     - subst. by rewrite /shift_loc Z.add_0_r -surjective_pairing lookup_delete.
     - replace i with (1+(i-1)) by lia.
       rewrite lookup_delete_ne -shift_loc_assoc ?IH //; first lia.
-      destruct l; intros [=?]. lia. }
+      destruct l; intros [= ?]. lia. }
   assert (FREE' : σ' !! l = None).
   { inversion Ha1; clear Ha1; inv_head_step. auto. }
   destruct Hred2 as (κ'&e2'&σ''&ef&?).
diff --git a/theories/lifetime/frac_borrow.v b/theories/lifetime/frac_borrow.v
index f73a58ed..6d1d6468 100644
--- a/theories/lifetime/frac_borrow.v
+++ b/theories/lifetime/frac_borrow.v
@@ -4,7 +4,7 @@ From iris.algebra Require Import frac.
 From lrust.lifetime Require Export at_borrow.
 From iris.prelude Require Import options.
 
-Class frac_borG Σ := frac_borG_inG :> inG Σ fracR.
+Class frac_borG Σ := frac_borG_inG :: inG Σ fracR.
 
 Local Definition frac_bor_inv `{!invGS Σ, !lftGS Σ userE, !frac_borG Σ}
                               (φ : Qp → iProp Σ) γ κ' :=
diff --git a/theories/lifetime/meta.v b/theories/lifetime/meta.v
index b9e4f8af..4fe35cf4 100644
--- a/theories/lifetime/meta.v
+++ b/theories/lifetime/meta.v
@@ -7,7 +7,7 @@ From iris.prelude Require Import options.
 [gname]) to a lifetime (as is required for types using branding). *)
 
 Class lft_metaG Σ := LftMetaG {
-  lft_meta_inG :> inG Σ (dyn_reservation_mapR (agreeR gnameO));
+  lft_meta_inG :: inG Σ (dyn_reservation_mapR (agreeR gnameO));
 }.
 Definition lft_metaΣ : gFunctors :=
   #[GFunctor (dyn_reservation_mapR (agreeR gnameO))].
diff --git a/theories/lifetime/model/definitions.v b/theories/lifetime/model/definitions.v
index e887cdca..026e51ef 100644
--- a/theories/lifetime/model/definitions.v
+++ b/theories/lifetime/model/definitions.v
@@ -41,25 +41,25 @@ Definition borUR := gmapUR slice_name (prodR fracR (agreeR bor_stateO)).
 Definition inhUR := gset_disjUR slice_name.
 
 Class lftGS Σ (userE : coPset) := LftG {
-  lft_box :> boxG Σ;
-  alft_inG :> inG Σ (authR alftUR);
+  lft_box :: boxG Σ;
+  alft_inG :: inG Σ (authR alftUR);
   alft_name : gname;
-  ilft_inG :> inG Σ (authR ilftUR);
+  ilft_inG :: inG Σ (authR ilftUR);
   ilft_name : gname;
-  lft_bor_inG :> inG Σ (authR borUR);
-  lft_cnt_inG :> inG Σ (authR natUR);
-  lft_inh_inG :> inG Σ (authR inhUR);
+  lft_bor_inG :: inG Σ (authR borUR);
+  lft_cnt_inG :: inG Σ (authR natUR);
+  lft_inh_inG :: inG Σ (authR inhUR);
   userE_lftN_disj : ↑lftN ## userE;
 }.
 Definition lftGS' := lftGS.
 
 Class lftGpreS Σ := LftGPreS {
-  lft_preG_box :> boxG Σ;
-  alft_preG_inG :> inG Σ (authR alftUR);
-  ilft_preG_inG :> inG Σ (authR ilftUR);
-  lft_preG_bor_inG :> inG Σ (authR borUR);
-  lft_preG_cnt_inG :> inG Σ (authR natUR);
-  lft_preG_inh_inG :> inG Σ (authR inhUR);
+  lft_preG_box :: boxG Σ;
+  alft_preG_inG :: inG Σ (authR alftUR);
+  ilft_preG_inG :: inG Σ (authR ilftUR);
+  lft_preG_bor_inG :: inG Σ (authR borUR);
+  lft_preG_cnt_inG :: inG Σ (authR natUR);
+  lft_preG_inh_inG :: inG Σ (authR inhUR);
 }.
 Definition lftGpreS' := lftGpreS.
 
diff --git a/theories/typing/lib/brandedvec.v b/theories/typing/lib/brandedvec.v
index 94e4ad98..29577ea8 100644
--- a/theories/typing/lib/brandedvec.v
+++ b/theories/typing/lib/brandedvec.v
@@ -8,8 +8,8 @@ From iris.prelude Require Import options.
 
 Definition brandidx_stR := max_natUR.
 Class brandidxG Σ := BrandedIdxG {
-  brandidx_inG :> inG Σ (authR brandidx_stR);
-  brandidx_gsingletonG :> lft_metaG Σ;
+  brandidx_inG :: inG Σ (authR brandidx_stR);
+  brandidx_gsingletonG :: lft_metaG Σ;
 }.
 
 Definition brandidxΣ : gFunctors
diff --git a/theories/typing/lib/ghostcell.v b/theories/typing/lib/ghostcell.v
index bb868034..1cd696e9 100644
--- a/theories/typing/lib/ghostcell.v
+++ b/theories/typing/lib/ghostcell.v
@@ -69,8 +69,8 @@ Definition ghosttoken_stR :=
   (csumR (exclR unitO) ((prodR (agreeR lftO) fracR))).
 
 Class ghostcellG Σ := GhostcellG {
-  ghostcell_inG :> inG Σ (ghosttoken_stR);
-  ghostcell_gsingletonG :> lft_metaG Σ;
+  ghostcell_inG :: inG Σ (ghosttoken_stR);
+  ghostcell_gsingletonG :: lft_metaG Σ;
 }.
 
 Definition ghostcellΣ : gFunctors
diff --git a/theories/typing/lib/rc/rc.v b/theories/typing/lib/rc/rc.v
index bf265d14..9e3f2ad0 100644
--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -9,7 +9,7 @@ From iris.prelude Require Import options.
 Definition rc_stR :=
   prodUR (optionUR (csumR (prodR fracR positiveR) (exclR unitO))) natUR.
 Class rcG Σ :=
-  RcG :> inG Σ (authR rc_stR).
+  RcG :: inG Σ (authR rc_stR).
 Definition rcΣ : gFunctors := #[GFunctor (authR rc_stR)].
 Global Instance subG_rcΣ {Σ} : subG rcΣ Σ → rcG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/typing/lib/refcell/refcell.v b/theories/typing/lib/refcell/refcell.v
index da4ced23..f136a89b 100644
--- a/theories/typing/lib/refcell/refcell.v
+++ b/theories/typing/lib/refcell/refcell.v
@@ -11,7 +11,7 @@ Definition refcell_stR :=
              fracR)
              positiveR).
 Class refcellG Σ :=
-  RefCellG :> inG Σ (authR refcell_stR).
+  RefCellG :: inG Σ (authR refcell_stR).
 Definition refcellΣ : gFunctors := #[GFunctor (authR refcell_stR)].
 Global Instance subG_refcellΣ {Σ} : subG refcellΣ Σ → refcellG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index ec3810b1..a34db311 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -8,7 +8,7 @@ From iris.prelude Require Import options.
 Definition rwlock_stR :=
   optionUR (csumR (exclR unitO) (prodR (prodR (agreeR lftO) fracR) positiveR)).
 Class rwlockG Σ :=
-  RwLockG :> inG Σ (authR rwlock_stR).
+  RwLockG :: inG Σ (authR rwlock_stR).
 Definition rwlockΣ : gFunctors := #[GFunctor (authR rwlock_stR)].
 Global Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
 Proof. solve_inG. Qed.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
index a2623b75..11c4e698 100644
--- a/theories/typing/soundness.v
+++ b/theories/typing/soundness.v
@@ -8,10 +8,10 @@ From iris.prelude Require Import options.
 
 
 Class typeGpreS Σ := PreTypeG {
-  type_preG_lrustGS :> lrustGpreS Σ;
-  type_preG_lftGS :> lftGpreS Σ;
-  type_preG_na_invG :> na_invG Σ;
-  type_preG_frac_borG :> frac_borG Σ
+  type_preG_lrustGS :: lrustGpreS Σ;
+  type_preG_lftGS :: lftGpreS Σ;
+  type_preG_na_invG :: na_invG Σ;
+  type_preG_frac_borG :: frac_borG Σ
 }.
 
 Definition typeΣ : gFunctors :=
diff --git a/theories/typing/type.v b/theories/typing/type.v
index e577ecff..29154f26 100644
--- a/theories/typing/type.v
+++ b/theories/typing/type.v
@@ -7,10 +7,10 @@ From lrust.typing Require Import lft_contexts.
 From iris.prelude Require Import options.
 
 Class typeGS Σ := TypeG {
-  type_lrustGS :> lrustGS Σ;
-  type_lftGS :> lftGS Σ lft_userE;
-  type_na_invG :> na_invG Σ;
-  type_frac_borrowG :> frac_borG Σ
+  type_lrustGS :: lrustGS Σ;
+  type_lftGS :: lftGS Σ lft_userE;
+  type_na_invG :: na_invG Σ;
+  type_frac_borrowG :: frac_borG Σ
 }.
 
 Definition lrustN := nroot .@ "lrust".
-- 
GitLab