diff --git a/semantics.opam b/semantics.opam index 32fd42f75210842878bee06d079a4bb4a86eba8d..c292cf8097f9cf4260daa62eb997f3b37c5ed795 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 f366ba73be48524cbaf26e856bc8dcf793cc0560..d82a85e90644f43fe1035043bf5f10fbca78eb1a 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 ed45a848f7efed590f36f4916ad1a1bf5d3c6ca2..64b9ed1a4d0fef072947c334567af8720c86b73a 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 892c2d4a09b84789ed6cda58d8ba0742b5f00da6..79557df40e587d0bd33e7cfc6a587a28c2e10e0c 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 7a47f65c7399aa8e2adc81ae7e3c98116ca86c3c..07c035e698d46ca5e7a8664dd2284d65618dfdd3 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 35f1b6d3959ca2d50d52dbf2eae467b93323e125..97f6d91898f09b03cefa390be68836a8802a7402 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. *)