Bump Iris.

coq-reloc.opam

@@ -6,7 +6,7 @@ bug-reports: "https://gitlab.mpi-sws.org/dfrumin/reloc/issues"
 dev-repo: "git+https://gitlab.mpi-sws.org/dfrumin/reloc.git"
 
 depends: [
-  "coq-iris-heap-lang" { (= "dev.2022-08-03.0.949ab7bc") | (= "dev") }
+  "coq-iris-heap-lang" { (= "dev.2022-08-12.4.9245c4c0") | (= "dev") }
   "coq-autosubst" { = "dev" }
 ]
 

theories/examples/folly_queue/refinement.v

@@ -29,11 +29,11 @@ Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
 Require Import Arith ZArith ZifyClasses ZifyInst Lia.
 
 Global Program Instance Op_Nat_mod : BinOp Nat.modulo :=
-  {| TBOp := Z.modulo ; TBOpInj := Nat2Z_inj_mod |}.
+  {| TBOp := Z.modulo ; TBOpInj := Nat2Z.inj_mod |}.
 Add Zify BinOp Op_Nat_mod.
 
 Global Program Instance Op_Nat_div : BinOp Nat.div :=
-  {| TBOp := Z.div ; TBOpInj := Nat2Z_inj_div |}.
+  {| TBOp := Z.div ; TBOpInj := Nat2Z.inj_div |}.
 Add Zify BinOp Op_Nat_div.
 
 (* lia now works with Nat.modulo nad Nat.div. *)
@@ -737,12 +737,12 @@ Section queue_refinement.
       rel_bind_l (! _)%E.
       rel_apply_l refines_wp_l.
       assert ((Z.of_nat pushTicket `rem` Z.of_nat q)%Z = Z.of_nat (pushTicket `mod` q)) as ->.
-      { rewrite Nat2Z_inj_mod. apply Z.rem_mod_nonneg; lia. }
+      { rewrite Nat2Z.inj_mod. apply Z.rem_mod_nonneg; lia. }
       wp_apply (wp_load_offset with "arrPts").
       { rewrite list_lookup_fmap. rewrite Hattss. reflexivity. }
       iIntros "arrPts".
       rewrite Z.quot_div_nonneg; [|lia|lia].
-      rewrite -Nat2Z_inj_div.
+      rewrite -Nat2Z.inj_div.
       rel_apply_l refines_wp_l.
       wp_apply (enqueueWithTicket_spec' _ (R _ q (pushTicket `mod` q)) with "[-]").
       2: { iIntros. rel_values. }
@@ -790,12 +790,12 @@ Section queue_refinement.
       rel_bind_l (! _)%E.
       rel_apply_l refines_wp_l.
       assert ((Z.of_nat pushTicket `rem` Z.of_nat q)%Z = Z.of_nat (pushTicket `mod` q)) as ->.
-      { rewrite Nat2Z_inj_mod. apply Z.rem_mod_nonneg; lia. }
+      { rewrite Nat2Z.inj_mod. apply Z.rem_mod_nonneg; lia. }
       wp_apply (wp_load_offset with "arrPts").
       { rewrite list_lookup_fmap. rewrite Hattss. reflexivity. }
       iIntros "arrPts".
       rewrite Z.quot_div_nonneg; [|lia|lia].
-      rewrite -Nat2Z_inj_div.
+      rewrite -Nat2Z.inj_div.
       rel_apply_l refines_wp_l.
       wp_apply (enqueueWithTicket_spec' _ (R _ q (pushTicket `mod` q)) with "[-]").
       2: { iIntros. rel_values. }
@@ -866,14 +866,14 @@ Section queue_refinement.
       rel_pures_l.
 
       assert ((Z.of_nat popTicket `rem` Z.of_nat q)%Z = Z.of_nat (popTicket `mod` q)) as ->.
-      { rewrite Nat2Z_inj_mod. apply Z.rem_mod_nonneg; lia. }
+      { rewrite Nat2Z.inj_mod. apply Z.rem_mod_nonneg; lia. }
       rel_apply_l refines_wp_l.
       wp_apply (wp_load_offset with "arrPts").
       { rewrite list_lookup_fmap. rewrite Hattss. reflexivity. }
       iIntros "arrPts".
 
       rewrite Z.quot_div_nonneg; [|lia|lia].
-      rewrite -Nat2Z_inj_div.
+      rewrite -Nat2Z.inj_div.
       iApply wp_fupd.
       simpl.
       wp_apply (dequeueWithTicket_spec2 _ (R _ q (popTicket `mod` q)) with "[-Htok]").
@@ -953,13 +953,13 @@ Section queue_refinement.
       rel_bind_l (! _)%E.
       rel_apply_l refines_wp_l.
       assert ((Z.of_nat popTicket `rem` Z.of_nat q)%Z = Z.of_nat (popTicket `mod` q)) as ->.
-      { rewrite Nat2Z_inj_mod. apply Z.rem_mod_nonneg; lia. }
+      { rewrite Nat2Z.inj_mod. apply Z.rem_mod_nonneg; lia. }
       wp_apply (wp_load_offset with "arrPts").
       { rewrite list_lookup_fmap. rewrite Hattss. reflexivity. }
       iIntros "arrPts".
 
       rewrite Z.quot_div_nonneg; [|lia|lia].
-      rewrite -Nat2Z_inj_div.
+      rewrite -Nat2Z.inj_div.
       rel_apply_l refines_wp_l.
       wp_apply (dequeueWithTicket_spec' _ (R _ q (popTicket `mod` q)) with "[-]").
       { iFrame "#∗". }

theories/examples/folly_queue/turnSequencer.v

@@ -122,7 +122,7 @@ Section spec.
       iDestruct "Hc'" as (ℓ1' ?) "Hc'".
       simplify_eq/=.
       iCombine "ℓPts Hc'" as "ℓPts".
-      iDestruct (mapsto_valid_2 with "ℓPts Hc") as %[?%Qp_not_add_le_l _].
+      iDestruct (mapsto_valid_2 with "ℓPts Hc") as %[?%Qp.not_add_le_l _].
       done. }
     wp_load.
     iDestruct (mapsto_agree with "ℓPts Hc") as %[= Heq].
@@ -136,11 +136,11 @@ Section spec.
       iDestruct "Hc'" as (ℓ1' ?) "Hc'".
       simplify_eq/=.
       iCombine "ℓPts Hc'" as "ℓPts".
-      iDestruct (mapsto_valid_2 with "ℓPts Hc") as %[?%Qp_not_add_le_l _].
+      iDestruct (mapsto_valid_2 with "ℓPts Hc") as %[?%Qp.not_add_le_l _].
       done. }
     iDestruct (mapsto_combine with "ℓPts Hc") as "[ℓPts %Heq]".
     simplify_eq/=.
-    rewrite dfrac_op_own Qp_half_half.
+    rewrite dfrac_op_own Qp.half_half.
     wp_store.
     assert ((n + 1)%Z = (n + 1)%nat) as ->. { lia. }
     iDestruct "ℓPts" as "[ℓPts ℓPts']".

theories/examples/red_blue_flag.v

@@ -141,7 +141,7 @@ Section offer_theory.
     iIntros "O P".
     iDestruct (offer_agree with "O P") as %<-.
     iMod (own_update_2 _ _ _  (Cinl (Excl ())) with "O P") as "O".
-    { rewrite -Cinr_op -pair_op frac_op Qp_half_half.
+    { rewrite -Cinr_op -pair_op frac_op Qp.half_half.
       apply cmra_update_exclusive. done. }
     iModIntro. iFrame. done.
   Qed.
@@ -150,7 +150,7 @@ Section offer_theory.
   Proof.
     iIntros "O".
     iMod (no_offer_to_offer with "O") as "O".
-    rewrite -{1}Qp_three_quarter_quarter.
+    rewrite -{1}Qp.three_quarter_quarter.
     iDestruct (offer_split with "O") as "[Hhalf Hhalf']".
     iModIntro. iFrame.
   Qed.
@@ -163,7 +163,7 @@ Section proofs.
   Definition offer_token γ q := own γ (q : frac).
 
   Lemma offer_token_split γ : own γ 1%Qp ⊣⊢ own γ (1/2)%Qp ∗ own γ (1/2)%Qp.
-  Proof. rewrite -{1}Qp_half_half. rewrite -own_op. done. Qed.
+  Proof. rewrite -{1}Qp.half_half. rewrite -own_op. done. Qed.
 
   (* The specification thread `k` is about to run a flip. *)
   Definition tp_flip k bf lk := (refines_right k (blueFlip #bf lk))%I.
@@ -369,7 +369,7 @@ Section proofs.
       iDestruct "Hdisj" as "[(_ & Htok & Hoff) | Hdisj]".
       2: { iDestruct "Hdisj" as (?) "[[% _]|[% _]]"; by subst. }
       iMod (no_offer_to_offer _ k  with "Hoff") as "Hoff".
-      iEval (rewrite -Qp_half_half) in "Hoff".
+      iEval (rewrite -Qp.half_half) in "Hoff".
       iDestruct (offer_split with "Hoff") as "[Hoff Hoff']".
       iMod ("Hclose" with "[-IH Hoff Htok]") as "_".
       { iNext. iExists _. iFrame. iExists 1. iFrame. iRight. iExists k. iLeft. by iFrame. }
@@ -385,7 +385,7 @@ Section proofs.
         iDestruct "Hdisj" as "[[% _] | Hdisj]"; first by subst.
         iDestruct "Hdisj" as (?) "[(% & Hoff' & Hj) | [% _]]"; last by subst.
         iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
-        rewrite Qp_half_half.
+        rewrite Qp.half_half.
         iMod (offer_to_no_offer with "Hoff") as "Hoff".
         iMod ("Hclose" with "[-IH Hj]") as "_".
         { iNext. iExists _. iFrame. iExists 0. iFrame. iLeft. by iFrame. }
@@ -400,7 +400,7 @@ Section proofs.
       iDestruct "Hdisj" as "[[Hoff' Hj] | Hoff']".
       2: {
         iDestruct (own_valid_2 with "Htok Hoff'") as %Hv.
-        by apply Qp_not_add_le_l in Hv. }
+        by apply Qp.not_add_le_l in Hv. }
       iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
       iDestruct (offer_token_split with "Htok") as "[Htok Htok']".
       iMod ("Hclose" with "[-IH Hj Hoff Htok]") as "_".
@@ -418,16 +418,16 @@ Section proofs.
       { iDestruct (no_offer_exclusive with "Hoff' Hoff") as %?. done. }
       iDestruct "Hdisj" as (?) "[(_ & Hoff' & _) | (% & Hdisj)]".
       { iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
-        rewrite Qp_half_half.
+        rewrite Qp.half_half.
         iDestruct (own_offer_valid with "Hoff") as %Hle.
-        by apply Qp_not_add_le_l in Hle. }
+        by apply Qp.not_add_le_l in Hle. }
       iDestruct "Hdisj" as "[[Hoff' _] | Htok']".
       { iDestruct (offer_combine with "Hoff Hoff'") as "(<- & Hoff)".
-        rewrite Qp_half_half.
+        rewrite Qp.half_half.
         iDestruct (own_offer_valid with "Hoff") as %Hle.
-        by apply Qp_not_add_le_l in Hle. }
+        by apply Qp.not_add_le_l in Hle. }
       iCombine "Htok Htok'" as "Htok".
-      iEval (rewrite Qp_half_half) in "Hoff".
+      iEval (rewrite Qp.half_half) in "Hoff".
       iMod (offer_to_no_offer with "Hoff") as "Hoff".
       iMod ("Hclose" with "[-IH Hj]") as "_".
       { iNext. iExists _. iFrame. iExists 0. iFrame. iLeft. iFrame. done. }