From f5867e7877bbbab439fe58e72a502e4de83a8f46 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Lennard=20G=C3=A4her?= <l.gaeher@posteo.de>
Date: Tue, 9 Aug 2022 09:19:59 +0200
Subject: [PATCH] bump iris
---
semantics.opam | 4 ++--
.../program_logics/concurrent_logrel/adequacy.v | 2 +-
theories/program_logics/heap_lang/adequacy.v | 2 +-
theories/program_logics/heap_lang/primitive_laws.v | 2 +-
theories/program_logics/program_logic/adequacy.v | 14 +++++++-------
.../program_logics/program_logic/sequential_wp.v | 2 +-
6 files changed, 13 insertions(+), 13 deletions(-)
diff --git a/semantics.opam b/semantics.opam
index 32fd42f..c292cf8 100644
--- a/semantics.opam
+++ b/semantics.opam
@@ -10,8 +10,8 @@ version: "dev"
depends: [
"coq" { (>= "8.13" & < "8.16~") | (= "dev") }
- "coq-iris" { (= "dev.2022-07-26.0.23bdf6bd") | (= "dev") }
- "coq-iris-heap-lang" { (= "dev.2022-07-26.0.23bdf6bd") | (= "dev") }
+ "coq-iris" { (= "dev.2022-08-09.0.4e9a1ec7") | (= "dev") }
+ "coq-iris-heap-lang" { (= "dev.2022-08-09.0.4e9a1ec7") | (= "dev") }
"coq-equations" { (= "1.2.4+8.13") | (= "1.3+8.14") | (= "1.3+8.15") }
"coq-autosubst" { = "1.7" }
]
diff --git a/theories/program_logics/concurrent_logrel/adequacy.v b/theories/program_logics/concurrent_logrel/adequacy.v
index f366ba7..d82a85e 100644
--- a/theories/program_logics/concurrent_logrel/adequacy.v
+++ b/theories/program_logics/concurrent_logrel/adequacy.v
@@ -16,7 +16,7 @@ Proof.
intros Hlog ??.
cut (adequate NotStuck e σ (λ _ _, True)); first by intros [_ Hsafe]; eapply Hsafe; eauto.
eapply (heap_adequacy Σ _).
- iIntros (??) "_".
+ iIntros (?) "_".
iApply (wp_wand with "[]").
- rewrite -(subst_map_empty e).
iApply (Hlog _ $! trivial_env).
diff --git a/theories/program_logics/heap_lang/adequacy.v b/theories/program_logics/heap_lang/adequacy.v
index ed45a84..64b9ed1 100644
--- a/theories/program_logics/heap_lang/adequacy.v
+++ b/theories/program_logics/heap_lang/adequacy.v
@@ -19,7 +19,7 @@ Definition heap_adequacy Σ `{!heapGpreS Σ} s e σ φ :
(∀ `{!heapGS Σ}, ⊢ WP e @ s; ⊤ {{ v, ⌜φ v⌝ }}) →
adequate s e σ (λ v _, φ v).
Proof.
- intros Hwp; eapply (wp_adequacy _ _); iIntros (??).
+ intros Hwp; eapply (wp_adequacy _ _); iIntros (?).
iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
iModIntro. iExists
(λ σ, (gen_heap_interp σ.(heap))%I).
diff --git a/theories/program_logics/heap_lang/primitive_laws.v b/theories/program_logics/heap_lang/primitive_laws.v
index 892c2d4..79557df 100644
--- a/theories/program_logics/heap_lang/primitive_laws.v
+++ b/theories/program_logics/heap_lang/primitive_laws.v
@@ -12,7 +12,7 @@ From semantics.pl.program_logic Require Export notation.
From iris.prelude Require Import options.
Class heapGS Σ := HeapGS {
- heapGS_invGS : invGS Σ;
+ heapGS_invGS : invGS_gen HasNoLc Σ;
heapGS_gen_heapGS :> gen_heapGS loc (option val) Σ;
}.
diff --git a/theories/program_logics/program_logic/adequacy.v b/theories/program_logics/program_logic/adequacy.v
index 7a47f65..07c035e 100644
--- a/theories/program_logics/program_logic/adequacy.v
+++ b/theories/program_logics/program_logic/adequacy.v
@@ -72,7 +72,7 @@ Proof.
iFrame. iPureIntro. split; first done. lia.
Qed.
-Lemma wp_not_stuck `{!HasNoLc Σ} e σ E Φ :
+Lemma wp_not_stuck e σ E Φ :
state_interp σ -∗ wp' NotStuck E e Φ ={E}=∗ ⌜not_stuck e σ⌝.
Proof.
rewrite wp'_unfold /wp_pre /not_stuck. iIntros "Hσ H".
@@ -81,7 +81,7 @@ Proof.
iMod (fupd_plain_mask with "H") as %?; eauto.
Qed.
-Lemma wptp_strong_adequacy `{!HasNoLc Σ} Φs s n es1 es2 κs σ1 σ2 :
+Lemma wptp_strong_adequacy Φs s n es1 es2 κs σ1 σ2 :
nsteps n (es1, σ1) κs (es2, σ2) →
state_interp σ1 -∗ wptp s es1 Φs
={∅,∅}=∗ |={∅}▷=>^n |={∅,∅}=>
@@ -115,7 +115,7 @@ End adequacy.
(** Iris's generic adequacy result *)
Theorem wp_strong_adequacy Σ Λ `{!invGpreS Σ} e σ1 n κs t2 σ2 φ :
- (∀ `{Hinv : !invGS Σ} `{!HasNoLc Σ},
+ (∀ `{Hinv : !invGS_gen HasNoLc Σ},
⊢ |={⊤}=> ∃
(s: stuckness)
(stateI : state Λ → iProp Σ)
@@ -145,11 +145,11 @@ Theorem wp_strong_adequacy Σ Λ `{!invGpreS Σ} e σ1 n κs t2 σ2 φ :
φ.
Proof.
intros Hwp ?.
- apply (step_fupdN_soundness_no_lc _ n 0)=> Hinv Hlc.
+ apply (step_fupdN_soundness_no_lc _ n 0)=> Hinv.
iIntros "_".
iMod Hwp as (s stateI Φ) "(Hσ & Hwp & Hφ)".
rewrite /wp swp_eq /swp_def. iMod "Hwp".
- iMod (@wptp_strong_adequacy _ _ (IrisG _ _ Hinv stateI) _ [_]
+ iMod (@wptp_strong_adequacy _ _ (IrisG _ _ Hinv stateI) [_]
with "[Hσ] [Hwp]") as "H";[ done | done | | ].
{ by iApply big_sepL2_singleton. }
iAssert (|={∅}▷=>^n |={∅}=> ⌜φ⌝)%I
@@ -203,7 +203,7 @@ Proof.
Qed.
Corollary wp_adequacy Σ Λ `{!invGpreS Σ} s e σ φ :
- (∀ `{Hinv : !invGS Σ} `{!HasNoLc Σ},
+ (∀ `{Hinv : !invGS_gen HasNoLc Σ},
⊢ |={⊤}=> ∃ (stateI : state Λ → iProp Σ),
let _ : irisGS Λ Σ := IrisG _ _ Hinv stateI
in
@@ -211,7 +211,7 @@ Corollary wp_adequacy Σ Λ `{!invGpreS Σ} s e σ φ :
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp. apply adequate_alt; intros t2 σ2 [n [κs ?]]%erased_steps_nsteps.
- eapply (wp_strong_adequacy Σ _); [|done]=> ??.
+ eapply (wp_strong_adequacy Σ _); [|done]=> ?.
iMod Hwp as (stateI) "[Hσ Hwp]".
iExists s, stateI, (λ v, ⌜φ v⌝%I) => /=.
iIntros "{$Hσ $Hwp} !>" (e2 ->) "% H Hv".
diff --git a/theories/program_logics/program_logic/sequential_wp.v b/theories/program_logics/program_logic/sequential_wp.v
index 35f1b6d..97f6d91 100644
--- a/theories/program_logics/program_logic/sequential_wp.v
+++ b/theories/program_logics/program_logic/sequential_wp.v
@@ -6,7 +6,7 @@ From iris.prelude Require Import options.
Import uPred.
Class irisGS (Λ : language) (Σ : gFunctors) := IrisG {
- iris_invGS :> invGS Σ;
+ iris_invGS :> invGS_gen HasNoLc Σ;
(** The state interpretation is an invariant that should hold in
between each step of reduction. Here [state Λ] is the global state. *)
--
GitLab