From 7d15511ad911b4748399159647757fb3c772c8df Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Aug 2022 22:17:46 +0200
Subject: [PATCH] Bump Iris.
---
coq-reloc.opam | 2 +-
theories/examples/folly_queue/refinement.v | 20 ++++++++---------
theories/examples/folly_queue/turnSequencer.v | 6 ++---
theories/examples/red_blue_flag.v | 22 +++++++++----------
4 files changed, 25 insertions(+), 25 deletions(-)
diff --git a/coq-reloc.opam b/coq-reloc.opam
index 2556bbf..a2f54de 100644
--- a/coq-reloc.opam
+++ b/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" }
]
diff --git a/theories/examples/folly_queue/refinement.v b/theories/examples/folly_queue/refinement.v
index 1be8f9f..16e5107 100644
--- a/theories/examples/folly_queue/refinement.v
+++ b/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 "#∗". }
diff --git a/theories/examples/folly_queue/turnSequencer.v b/theories/examples/folly_queue/turnSequencer.v
index 7a4c87d..060ad28 100644
--- a/theories/examples/folly_queue/turnSequencer.v
+++ b/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']".
diff --git a/theories/examples/red_blue_flag.v b/theories/examples/red_blue_flag.v
index 076ff67..6828260 100644
--- a/theories/examples/red_blue_flag.v
+++ b/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. }
--
GitLab