bump iris

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" }
 ]

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).

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).

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) Σ;
 }.
 

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".

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. *)