Commit 86460eea authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 392a0d4a
...@@ -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-06-11.8.a51fa3cf") | (= "dev") } "coq-iris" { (= "dev.2019-06-12.4.ae1dd418") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
...@@ -9,7 +9,7 @@ Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' : ...@@ -9,7 +9,7 @@ Theorem soundness Σ `{invPreG Σ} e τ e' thp σ σ' :
Proof. Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto). intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto).
eapply (wp_adequacy Σ); eauto. eapply (wp_adequacy Σ); eauto.
iIntros (Hinv ?). iModIntro. iExists (λ _ _, 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.
set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I). set (HΣ := IrisG _ _ Hinv (λ _ _ _, True)%I (λ _, True)%I).
iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto. iApply (wp_wand with "[]"). iApply Hlog; eauto. by iApply interp_env_nil. auto.
......
...@@ -17,7 +17,7 @@ Proof. ...@@ -17,7 +17,7 @@ Proof.
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".
iModIntro. iExists (λ σ _, gen_heap_ctx σ); iFrame. iModIntro. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
set (HeapΣ := (HeapG Σ Hinv Hheap)). set (HeapΣ := (HeapG Σ Hinv Hheap)).
iApply (wp_wand with "[]"). iApply (wp_wand with "[]").
- replace e with e.[env_subst[]] by by asimpl. - replace e with e.[env_subst[]] by by asimpl.
......
...@@ -25,7 +25,7 @@ Proof. ...@@ -25,7 +25,7 @@ Proof.
rewrite /to_gen_heap fin_maps.map_fmap_empty. rewrite /to_gen_heap fin_maps.map_fmap_empty.
iFrame. } iFrame. }
set (HeapΣ := HeapG Σ Hinv Hheap). set (HeapΣ := HeapG Σ Hinv Hheap).
iExists (λ σ _, gen_heap_ctx σ); iFrame. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
iApply wp_fupd. iApply (wp_wand with "[-]"). iApply wp_fupd. iApply (wp_wand with "[-]").
- iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel". - iPoseProof (Hlog _ _ with "[$Hcfg]") as "Hrel".
{ iApply (@logrel_binary.interp_env_nil Σ HeapΣ). } { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
......
...@@ -22,7 +22,7 @@ Proof. ...@@ -22,7 +22,7 @@ Proof.
iMod (inv_alloc specN _ (spec_inv ([e'], )) with "[Hcfg1]") as "#Hcfg". iMod (inv_alloc specN _ (spec_inv ([e'], )) with "[Hcfg1]") as "#Hcfg".
{ iNext. iExists [e'], . rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. } { iNext. iExists [e'], . rewrite /to_gen_heap fin_maps.map_fmap_empty. auto. }
set (HeapΣ := (HeapIG Σ Hinv Hheap)). set (HeapΣ := (HeapIG Σ Hinv Hheap)).
iExists (λ σ _, gen_heap_ctx σ); iFrame. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
iApply wp_fupd. iApply wp_wand_r. iApply wp_fupd. iApply wp_wand_r.
iSplitL. iSplitL.
iPoseProof ((Hlog _ _ [] []) with "[]") as "Hrel". iPoseProof ((Hlog _ _ [] []) with "[]") as "Hrel".
......
...@@ -16,7 +16,7 @@ Proof. ...@@ -16,7 +16,7 @@ Proof.
intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; eauto). intros Hlog ??. cut (adequate NotStuck e σ (λ _ _, True)); first (intros [_ ?]; 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 σ); iFrame. iModIntro. iExists (λ σ _, gen_heap_ctx σ), (λ _, True%I); iFrame.
set (HeapΣ := (HeapIG Σ Hinv Hheap)). set (HeapΣ := (HeapIG Σ Hinv Hheap)).
iApply (wp_wand with "[]"). iApply (wp_wand with "[]").
- replace e with e.[env_subst[]] by by asimpl. - replace e with e.[env_subst[]] by by asimpl.
......
...@@ -16,7 +16,7 @@ Proof. ...@@ -16,7 +16,7 @@ Proof.
set (Σ := invΣ). intros. set (Σ := invΣ). intros.
cut (adequate NotStuck e () (λ _ _, True)); first (intros [_ Hsafe]; eauto). cut (adequate NotStuck e () (λ _ _, True)); first (intros [_ Hsafe]; eauto).
eapply (wp_adequacy Σ _). iIntros (Hinv ?). eapply (wp_adequacy Σ _). iIntros (Hinv ?).
iModIntro. iExists (λ _ _, 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).
iApply (wp_wand with "[]"). by iApply wp_soundness. eauto. iApply (wp_wand with "[]"). by iApply wp_soundness. eauto.
Qed. Qed.
......
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