Commit dd32b1ff authored by Ralf Jung's avatar Ralf Jung

Merge branch 'ci/amin/fix-logrell-soundness' into 'master'

Fix logrel soundness proofs

See merge request iris/examples!27
parents a83f57e6 b95a80e0
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [ depends: [
"coq-iris" { (= "dev.2019-11-02.1.9d4613fc") | (= "dev") } "coq-iris" { (= "dev.2019-11-07.3.eb2dfc72") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
...@@ -4,10 +4,11 @@ From iris.program_logic Require Import adequacy. ...@@ -4,10 +4,11 @@ From iris.program_logic Require Import adequacy.
Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' : Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
( `{irisG F_mu_lang Σ}, [] e : τ) ( `{irisG F_mu_lang Σ}, [] e : τ)
rtc erased_step ([e], σ) (thp, σ') e' thp rtc erased_step ([e], σ) (thp, σ') e' thp not_stuck e' σ'.
is_Some (to_val e') reducible e' σ'.
Proof. Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto). intros Hlog ??.
cut (adequate NotStuck e σ (λ _ _, True));
first by intros [_ Hsafe]; eapply Hsafe; eauto.
eapply (wp_adequacy Σ); eauto. eapply (wp_adequacy Σ); eauto.
iIntros (Hinv ?). iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=> //. iIntros (Hinv ?). iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=> //.
replace e with e.[env_subst[]] by by asimpl. replace e with e.[env_subst[]] by by asimpl.
...@@ -17,8 +18,7 @@ Qed. ...@@ -17,8 +18,7 @@ Qed.
Corollary type_soundness e τ e' thp σ σ' : Corollary type_soundness e τ e' thp σ σ' :
[] e : τ [] e : τ
rtc erased_step ([e], σ) (thp, σ') e' thp rtc erased_step ([e], σ) (thp, σ') e' thp not_stuck e' σ'.
is_Some (to_val e') reducible e' σ'.
Proof. Proof.
intros ??. set (Σ := invΣ). intros ??. set (Σ := invΣ).
eapply (soundness Σ); eauto using fundamental. eapply (soundness Σ); eauto using fundamental.
......
...@@ -10,10 +10,11 @@ Class heapPreG Σ := HeapPreG { ...@@ -10,10 +10,11 @@ Class heapPreG Σ := HeapPreG {
Theorem soundness Σ `{heapPreG Σ} e τ e' thp σ σ' : Theorem soundness Σ `{heapPreG Σ} e τ e' thp σ σ' :
( `{heapG Σ}, [] e : τ) ( `{heapG Σ}, [] e : τ)
rtc erased_step ([e], σ) (thp, σ') e' thp rtc erased_step ([e], σ) (thp, σ') e' thp not_stuck e' σ'.
is_Some (to_val e') reducible e' σ'.
Proof. Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto). intros Hlog ??.
cut (adequate NotStuck e σ (λ _ _, True));
first by intros [_ Hsafe]; eapply Hsafe; eauto.
eapply (wp_adequacy Σ _); eauto. eapply (wp_adequacy Σ _); eauto.
iIntros (Hinv ?). iIntros (Hinv ?).
iMod (gen_heap_init σ) as (Hheap) "Hh". iMod (gen_heap_init σ) as (Hheap) "Hh".
...@@ -27,8 +28,7 @@ Qed. ...@@ -27,8 +28,7 @@ Qed.
Corollary type_soundness e τ e' thp σ σ' : Corollary type_soundness e τ e' thp σ σ' :
[] e : τ [] e : τ
rtc erased_step ([e], σ) (thp, σ') e' thp rtc erased_step ([e], σ) (thp, σ') e' thp not_stuck e' σ'.
is_Some (to_val e') reducible e' σ'.
Proof. Proof.
intros ??. set (Σ := #[invΣ ; gen_heapΣ loc val]). intros ??. set (Σ := #[invΣ ; gen_heapΣ loc val]).
set (HG := HeapPreG Σ _ _). set (HG := HeapPreG Σ _ _).
......
...@@ -11,9 +11,11 @@ Class heapPreIG Σ := HeapPreIG { ...@@ -11,9 +11,11 @@ Class heapPreIG Σ := HeapPreIG {
Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' : Theorem soundness Σ `{heapPreIG Σ} e τ e' thp σ σ' :
( `{heapIG Σ}, [] e : τ) ( `{heapIG Σ}, [] e : τ)
rtc erased_step ([e], σ) (thp, σ') e' thp rtc erased_step ([e], σ) (thp, σ') e' thp
is_Some (to_val e') reducible e' σ'. not_stuck e' σ'.
Proof. Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto). intros Hlog ??.
cut (adequate NotStuck e σ (λ _ _, True));
first by intros [_ Hsafe]; eapply Hsafe; eauto.
eapply (wp_adequacy Σ _). iIntros (Hinv ?). eapply (wp_adequacy Σ _). iIntros (Hinv ?).
iMod (gen_heap_init σ) as (Hheap) "Hh". iMod (gen_heap_init σ) as (Hheap) "Hh".
iModIntro. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame. iModIntro. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
...@@ -26,8 +28,7 @@ Qed. ...@@ -26,8 +28,7 @@ Qed.
Corollary type_soundness e τ e' thp σ σ' : Corollary type_soundness e τ e' thp σ σ' :
[] e : τ [] e : τ
rtc erased_step ([e], σ) (thp, σ') e' thp rtc erased_step ([e], σ) (thp, σ') e' thp not_stuck e' σ'.
is_Some (to_val e') reducible e' σ'.
Proof. Proof.
intros ??. set (Σ := #[invΣ ; gen_heapΣ loc F_mu_ref_conc.val]). intros ??. set (Σ := #[invΣ ; gen_heapΣ loc F_mu_ref_conc.val]).
set (HG := HeapPreIG Σ _ _). set (HG := HeapPreIG Σ _ _).
......
...@@ -10,11 +10,11 @@ Proof. ...@@ -10,11 +10,11 @@ Proof.
Qed. Qed.
Theorem soundness e τ e' thp : Theorem soundness e τ e' thp :
[] e : τ rtc erased_step ([e], ()) (thp, ()) e' thp [] e : τ rtc erased_step ([e], ()) (thp, ()) e' thp not_stuck e' ().
is_Some (to_val e') reducible e' ().
Proof. Proof.
set (Σ := invΣ). intros. set (Σ := invΣ). intros.
cut (adequate NotStuck e () (λ _ _, True)); first (intros [_ Hsafe]; eauto). cut (adequate NotStuck e () (λ _ _, True));
first by intros [_ Hsafe]; eapply Hsafe; eauto.
eapply (wp_adequacy Σ _). iIntros (Hinv ?). eapply (wp_adequacy Σ _). iIntros (Hinv ?).
iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=>//. iModIntro. iExists (λ _ _, True%I), (λ _, True%I). iSplit=>//.
set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I). set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment