Merge branch 'bump-iris' into 'master'

Bump Iris version to match LambdaRust-Coq.

See merge request !4

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 01d12014855abe6adaea20bbb35b1e9beadff14e
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 398bae9d092b6568cf8d504ca98d8810979eea33

theories/atomic.v

@@ -2,7 +2,6 @@
 
 From iris.base_logic Require Export fancy_updates.
 From iris.program_logic Require Export hoare weakestpre.
-From iris.prelude Require Export coPset.
 Import uPred.
 
 Section atomic.

theories/atomic_incr.v

@@ -2,7 +2,6 @@ From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris_atomic Require Import atomic.
 From iris.proofmode Require Import tactics.
-From iris.prelude Require Import coPset.
 From iris.heap_lang.lib Require Import par.
 
 Section incr.

theories/flat.v

@@ -166,7 +166,7 @@ Section proof.
         subst. rewrite Qp_div_2. iMod ("Hclose" with "[-HR Hor HΦ]").
         { iNext. iDestruct "Hp" as "[Hp1 Hp2]". iRight. iRight.
           iRight. iExists x5, v. iFrame. iExists Q. iFrame. }
-        iApply "HΦ". iFrame.
+        iApply "HΦ". iFrame. done.
       * iDestruct "Hp" as (? ?) "[? Hs]". iDestruct "Hs" as (?) "(_ & _ & _ & >Ho1' & _)".
         iApply excl_falso. iFrame.
     - destruct ts as [[[[γx γ1] γ3] γ4] γq]. iDestruct "Hp" as (? x) "(_ & _ & >Ho2' & _)".
@@ -207,7 +207,7 @@ Section proof.
       { iFrame. iFrame "#". }
       iNext. iIntros "HRf".
       wp_seq. wp_proj. iApply (IHxs with "[-HΦ]")=>//.
-      iFrame "#"; first by iFrame. eauto.
+      iFrame "#"; first by iFrame.
   Qed.
 
   Lemma try_srv_spec R (s: loc) (lk: val) (γr γm γlk: gname) Φ :
@@ -282,7 +282,7 @@ Section proof.
     iIntros (P Q x) "#Hf".
     iIntros "!# Hp". wp_let. wp_bind (install _ _ _).
     iApply (install_spec R P Q f x γm γr s with "[-]")=>//.
-    { iFrame. iFrame "#". eauto. }
+    { iFrame. iFrame "#". }
     iNext. iIntros (p [[[[γx γ1] γ3] γ4] γq]) "[(Ho3 & Hx & HoQ) #?]".
     wp_let. wp_bind (loop _ _ _).
     iApply (loop_spec with "[-Hx HoQ]")=>//.
@@ -290,13 +290,13 @@ Section proof.
     iNext. iIntros (? ?) "Hs".
     iDestruct "Hs" as (Q') "(Hx' & HoQ' & HQ')".
     destruct (decide (x = a)) as [->|Hneq].
-    - iDestruct (saved_prop_agree with "[HoQ HoQ']") as "Heq"; first by iFrame.
+    - iDestruct (saved_prop_agree with "[$HoQ] [HoQ']") as "Heq"; first by iFrame.
       wp_let. iDestruct (uPred.cofe_funC_equivI with "Heq") as "Heq".
-      iSpecialize ("Heq" $! a0). by iRewrite "Heq" in "HQ'".
+      iSpecialize ("Heq" $! a0). by iRewrite -"Heq" in "HQ'".
     - iExFalso. iCombine "Hx" "Hx'" as "Hx".
       iDestruct (own_valid with "Hx") as %[_ H1].
-      rewrite pair_op //=  in H1=>//. apply to_agree_comp_valid in H1.
-      fold_leibniz. done.
+      rewrite //= in H1.
+      by apply agree_op_inv' in H1.
   Qed.
 
 End proof.

theories/misc.v

@@ -3,7 +3,6 @@
 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang proofmode notation.
 From iris.algebra Require Import auth frac gmap agree.
-From iris.prelude Require Import countable.
 From iris.base_logic Require Import big_op auth fractional.
 
 Import uPred.
@@ -36,8 +35,9 @@ Section heap_extra.
     ~((q1 + q2)%Qp ≤ 1%Qp)%Qc →
     p ↦{q1} a ∗ p ↦{q2} b ⊢ False.
   Proof.
-    iIntros (?) "Hp". 
-    iDestruct (@mapsto_valid_2 with "Hp") as %H'. done.
+    iIntros (?) "Hp".
+    iDestruct "Hp" as "[Hl Hr]".
+    iDestruct (@mapsto_valid_2 with "Hl Hr") as %H'. done.
   Qed.
 
 End heap_extra.
@@ -81,6 +81,6 @@ Section pair.
     iIntros "[Ho Ho']".
     iDestruct (m_frag_agree with "[Ho Ho']") as %Heq; first iFrame.
     subst. iCombine "Ho" "Ho'" as "Ho".
-    rewrite pair_op frac_op' agree_idemp. by iFrame.
+    by iFrame.
   Qed.
 End pair.

theories/peritem.v

@@ -54,7 +54,7 @@ Section proofs.
     { iFrame. iExists [], l.
       iFrame. simpl. eauto. }
     iMod (inv_alloc N _ (∃ xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
-    iApply "HΦ". iFrame "#".
+    iApply "HΦ". iFrame "#". done.
   Qed.
   
   Lemma push_spec (s: loc) (x: val):

theories/simple_sync.v

@@ -33,7 +33,7 @@ Section syncer.
     iSpecialize ("Hf" with "[R HP]"); first by iFrame.
     iApply wp_wand_r.  iSplitL "Hf"; first done.
     iIntros (v') "[HR HQv]". wp_let. wp_bind (release _).
-    iApply (release_spec with "[$HR $Hl $Hlocked]").
+    iApply (release_spec with "[$Hl $HR $Hlocked]").
     iNext. iIntros "_". by wp_seq.
   Qed.
 End syncer.

theories/treiber.v

@@ -64,17 +64,17 @@ Section proof.
         simpl. iDestruct "Hys" as (hd' ?) "(Hhd & Hys')".
         iExFalso. iDestruct "Hxs" as (?) "Hhd'".
         (* FIXME: If I dont use the @ here and below through this file, it loops. *)
-        by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
+        by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
     - induction ys as [|y ys' IHys'].
       + iIntros (hd) "(Hxs & Hys)".
         simpl.
         iExFalso. iDestruct "Hxs" as (? ?) "(Hhd & _)".
         iDestruct "Hys" as (?) "Hhd'".
-        by iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %?.
+        by iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %?.
       + iIntros (hd) "(Hxs & Hys)".
         simpl. iDestruct "Hxs" as (? ?) "(Hhd & Hxs')".
         iDestruct "Hys" as (? ?) "(Hhd' & Hys')".
-        iDestruct (@mapsto_agree with "[$Hhd $Hhd']") as %[= Heq].
+        iDestruct (@mapsto_agree with "[$Hhd] [$Hhd']") as %[= Heq].
         subst. iDestruct (IHxs' with "[Hxs' Hys']") as "%"; first by iFrame.
         by subst.
   Qed.
@@ -173,9 +173,9 @@ Section proof.
         { iRight. iExists y', (q / 2 / 2)%Qp, hd', xs'.
           destruct xs as [|x' xs''].
           - simpl. iDestruct "Hhd''" as (?) "H".
-            iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1 $H]") as %?.
+            iExFalso. by iDestruct (@mapsto_agree with "[$Hhd1] [$H]") as %?.
           - simpl. iDestruct "Hhd''" as (hd''' ?) "(Hhd'' & Hxs'')".
-            iDestruct (@mapsto_agree with "[$Hhd1 $Hhd'']") as %[=].
+            iDestruct (@mapsto_agree with "[$Hhd1] [$Hhd'']") as %[=].
             subst.
             iDestruct (uniq_is_list with "[Hxs1 Hxs'']") as "%"; first by iFrame. subst.
             repeat (iSplitR "Hxs1 Hs"; first done).