From 2b18ebd35fc13c0110a8e3e0a0c7ca3f82b12e4e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <gaeher@mpi-sws.org>
Date: Sat, 18 Mar 2023 14:12:47 +0100
Subject: [PATCH] bump Iris
---
semantics.opam | 2 +-
theories/program_logics/heap_lang/derived_laws.v | 10 +++++-----
theories/program_logics/heap_lang/primitive_laws.v | 8 ++++----
theories/program_logics/reloc/src_rules.v | 2 +-
4 files changed, 11 insertions(+), 11 deletions(-)
diff --git a/semantics.opam b/semantics.opam
index 8a1bf0b..6f91b8e 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -10,7 +10,7 @@ version: "dev"
depends: [
"coq" { (>= "8.13" & < "8.17~") | (= "dev") }
- "coq-iris-heap-lang" { (= "dev.2023-03-07.1.7e127436") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2023-03-18.3.1b3e86bb") | (= "dev") }
"coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15") | (= "1.3+8.16") }
"coq-autosubst" { (= "1.7") | (= "dev") }
]
diff --git a/theories/program_logics/heap_lang/derived_laws.v b/theories/program_logics/heap_lang/derived_laws.v
index f703761..e43905d 100644
--- a/theories/program_logics/heap_lang/derived_laws.v
+++ b/theories/program_logics/heap_lang/derived_laws.v
@@ -53,20 +53,20 @@ Lemma array_nil l dq : l ↦∗{dq} [] ⊣⊢ emp.
Proof. by rewrite /array. Qed.
Lemma array_singleton l dq v : l ↦∗{dq} [v] ⊣⊢ l ↦{dq} v.
-Proof. by rewrite /array /= right_id loc_add_0. Qed.
+Proof. by rewrite /array /= right_id Loc.add_0. Qed.
Lemma array_app l dq vs ws :
l ↦∗{dq} (vs ++ ws) ⊣⊢ l ↦∗{dq} vs ∗ (l +ₗ length vs) ↦∗{dq} ws.
Proof.
rewrite /array big_sepL_app.
setoid_rewrite Nat2Z.inj_add.
- by setoid_rewrite loc_add_assoc.
+ by setoid_rewrite Loc.add_assoc.
Qed.
Lemma array_cons l dq v vs : l ↦∗{dq} (v :: vs) ⊣⊢ l ↦{dq} v ∗ (l +ₗ 1) ↦∗{dq} vs.
Proof.
- rewrite /array big_sepL_cons loc_add_0.
- setoid_rewrite loc_add_assoc.
+ rewrite /array big_sepL_cons Loc.add_0.
+ setoid_rewrite Loc.add_assoc.
setoid_rewrite Nat2Z.inj_succ.
by setoid_rewrite Z.add_1_l.
Qed.
@@ -104,7 +104,7 @@ Proof.
{ done. }
iIntros "[$ Hl]". rewrite -fmap_S_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
- setoid_rewrite <-loc_add_assoc. iApply "IH". done.
+ setoid_rewrite <-Loc.add_assoc. iApply "IH". done.
Qed.
Lemma wp_allocN s E v n Φ :
diff --git a/theories/program_logics/heap_lang/primitive_laws.v b/theories/program_logics/heap_lang/primitive_laws.v
index 79557df..e749f58 100644
--- a/theories/program_logics/heap_lang/primitive_laws.v
+++ b/theories/program_logics/heap_lang/primitive_laws.v
@@ -97,10 +97,10 @@ Proof.
rewrite big_opM_union; last first.
{ apply map_disjoint_spec=> l' v1 v2 /lookup_singleton_Some [-> _].
intros (j&w&?&Hjl&_)%heap_array_lookup.
- rewrite loc_add_assoc -{1}[l']loc_add_0 in Hjl. simplify_eq; lia. }
- rewrite loc_add_0 -fmap_S_seq big_sepL_fmap.
+ rewrite Loc.add_assoc -{1}[l']Loc.add_0 in Hjl. simplify_eq; lia. }
+ rewrite Loc.add_0 -fmap_S_seq big_sepL_fmap.
setoid_rewrite Nat2Z.inj_succ. setoid_rewrite <-Z.add_1_l.
- setoid_rewrite <-loc_add_assoc.
+ setoid_rewrite <-Loc.add_assoc.
rewrite big_opM_singleton; iDestruct "Hvs" as "[$ Hvs]". by iApply "IH".
Qed.
@@ -128,7 +128,7 @@ Lemma wp_alloc s E v Φ :
WP Alloc (Val v) @ s; E; E {{ Φ }}.
Proof.
iIntros "HΦ". iApply wp_allocN_seq; [auto with lia..|].
- iIntros "!>" (l) "/= (? & _)". rewrite loc_add_0. iApply "HΦ"; iFrame.
+ iIntros "!>" (l) "/= (? & _)". rewrite Loc.add_0. iApply "HΦ"; iFrame.
Qed.
Lemma wp_free s E l v Φ :
diff --git a/theories/program_logics/reloc/src_rules.v b/theories/program_logics/reloc/src_rules.v
index 8d4698b..abada63 100644
--- a/theories/program_logics/reloc/src_rules.v
+++ b/theories/program_logics/reloc/src_rules.v
@@ -224,7 +224,7 @@ Section rules.
You will find the following lemmas relating to memory allocation helpful:
- alloc_fresh
- state_init_heap_singleton
- - fresh_locs_fresh
+ - Loc.fresh_fresh
- not_elem_of_dom
- loc_add_0_l
*)
--
GitLab