Bump Iris.

coq-lambda-rust.opam

@@ -13,7 +13,7 @@ the type system, and safety proof for some Rust libraries.
 """
 
 depends: [
-  "coq-iris" { (= "dev.2022-08-03.0.949ab7bc") | (= "dev") }
+  "coq-iris" { (= "dev.2022-08-11.1.c9223a52") | (= "dev") }
 ]
 
 build: [make "-j%{jobs}%"]

theories/typing/function.v

@@ -95,7 +95,7 @@ Section fn.
       { intros Hprop. apply Hprop, list_fmap_ne; last first.
         - symmetry. eapply Forall2_impl; first apply Hfp. intros.
           apply dist_later_dist, type_dist2_dist_later. done.
-        - apply _. }
+        - solve_proper. }
       clear. intros n tid p i x y. rewrite list_dist_lookup=>/(_ i).
       case _ : (x !! i)=>[tyx|]; case  _ : (y !! i)=>[tyy|];
         inversion_clear 1; [solve_proper|done].

theories/typing/lib/rc/rc.v

@@ -368,7 +368,7 @@ Section code.
                                (?&?&[=]&?)]]; first done. setoid_subst.
         iDestruct "Hproto" as (q'') "(Hl1 & Hl2 & Hl† & >Hqq' & Hν & Hν†)".
         iDestruct "Hqq'" as %Hqq'. wp_read. iApply "HΦ". iFrame "Hl1". iRight.
-        iSplit; first by rewrite !pos_op_plus; auto with lia. iSplit; iIntros "H↦".
+        iSplit; first by rewrite !pos_op_add; auto with lia. iSplit; iIntros "H↦".
         * iMod ("Hclose" with "[- Htok Hν1]") as "$"; last by auto 10 with iFrame.
           iFrame. iExists _. iFrame. auto with iFrame.
         * iMod (own_update_2 with "Hst Htok") as "Hst".
@@ -378,7 +378,7 @@ Section code.
           iApply "Hclose". iFrame. iExists _. iFrame. iExists (q+q'')%Qp. iFrame.
           iSplitL; first last.
           { rewrite [(_+_)%Qp]assoc [(q'+_)%Qp]comm. auto. }
-          rewrite pos_op_plus Z.sub_1_r -Pos2Z.inj_pred; last lia.
+          rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
           by rewrite Pos.add_1_l Pos.pred_succ.
   Qed.
 

theories/typing/lib/refcell/ref_code.v

@@ -173,7 +173,7 @@ Section ref_functions.
         iApply "H†". replace 1%Qp with (q'+q'')%Qp by naive_solver. iFrame.
       - simpl in *. setoid_subst. iExists (Some (ν, false, q0, n')). iFrame.
         iAssert (lrc ↦ #(Z.pos n'))%I with "[H↦lrc]" as "$".
-        { rewrite pos_op_plus Z.sub_1_r -Pos2Z.inj_pred; last lia.
+        { rewrite pos_op_add Z.sub_1_r -Pos2Z.inj_pred; last lia.
           by rewrite Pos.add_1_l Pos.pred_succ. }
         iMod (own_update with "H●◯") as "$".
         { apply auth_update_dealloc.

theories/typing/lib/refcell/refmut_code.v

@@ -148,7 +148,7 @@ Section refmut_functions.
           apply (cancel_local_update_unit (writing_stR q _)), _. }
         iDestruct "INV" as "(H† & Hq & _)".
         rewrite /= (_:Z.neg (1%positive ⋅ n') + 1 = Z.neg n');
-          last (rewrite pos_op_plus; lia). iFrame.
+          last (rewrite pos_op_add; lia). iFrame.
         iApply step_fupd_intro; [set_solver+|]. iSplitL; [|done].
         iDestruct "Hq" as (q' ?) "?". iExists (q+q')%Qp. iFrame.
         rewrite assoc (comm _ q'' q) //. }

theories/typing/lib/rwlock/rwlockreadguard_code.v

@@ -117,7 +117,7 @@ Section rwlockreadguard_functions.
           iSplitL "H● H◯"; last by eauto with iFrame.
           iApply (own_update_2 with "H● H◯"). apply auth_update_dealloc.
           assert (n = 1%positive ⋅ Pos.pred n) as EQn.
-          { rewrite pos_op_plus -Pplus_one_succ_l Pos.succ_pred // =>?. by subst. }
+          { rewrite pos_op_add -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_unit (reading_st q ν)) , _. }
       iApply (wp_step_fupd with "INV"); first set_solver.

[Ralf Jung]

A similar patch will be needed on the weak-mem branch.