Commit 168ad45e authored by Dan Frumin's avatar Dan Frumin

Bump the Iris version

parent bcff9394
...@@ -5,8 +5,8 @@ This version is known to compile with: ...@@ -5,8 +5,8 @@ This version is known to compile with:
- Coq 8.6.1 - Coq 8.6.1
- Ssreflect 1.6 - Ssreflect 1.6
- Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel) - Autosubst branch [coq86-devel](https://github.com/uds-psl/autosubst/tree/coq86-devel)
- std++ version [24aef2fea9481e65d1f6658005ddde25ae9a64ee](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/24aef2fea9481e65d1f6658005ddde25ae9a64ee) - std++ version [ca0be4274dd7593c44db46670d078095e9f6c1c7](https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp/tree/ca0be4274dd7593c44db46670d078095e9f6c1c7)
- Iris version [4be0320e9ff9122e90fa5af60e6a02e81eaffa33](https://gitlab.mpi-sws.org/FP/iris-coq/tree/4be0320e9ff9122e90fa5af60e6a02e81eaffa33) - Iris version [bfdd67a736ad91c3838bffde3f57af516dec56d8](https://gitlab.mpi-sws.org/FP/iris-coq/tree/bfdd67a736ad91c3838bffde3f57af516dec56d8)
# Compilation # Compilation
......
...@@ -22,5 +22,5 @@ Proof. ...@@ -22,5 +22,5 @@ Proof.
{ apply: auth_auth_valid. exact: to_gen_heap_valid. } { apply: auth_auth_valid. exact: to_gen_heap_valid. }
iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame. iModIntro. iExists (λ σ, own γ ( to_gen_heap σ)); iFrame.
set (Hheap := GenHeapG loc val Σ _ _ _ γ). set (Hheap := GenHeapG loc val Σ _ _ _ γ).
iApply (Hwp (HeapG _ _ _)). by iApply (Hwp (HeapG _ _ _)).
Qed. Qed.
...@@ -42,7 +42,8 @@ Section lang_rules. ...@@ -42,7 +42,8 @@ Section lang_rules.
to_val e = Some v to_val e = Some v
{{{ True }}} Alloc e @ E {{{ l, RET #l; l ↦ᵢ v }}}. {{{ True }}} Alloc e @ E {{{ l, RET #l; l ↦ᵢ v }}}.
Proof. Proof.
iIntros (<-%of_to_val Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto. iIntros (<-%of_to_val Φ) "_ HΦ".
iApply wp_lift_atomic_head_step_no_fork; auto.
iIntros (σ1) "Hσ !>"; iSplit; first by auto. iIntros (σ1) "Hσ !>"; iSplit; first by auto.
iNext; iIntros (v2 σ2 efs Hstep); inv_head_step. iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done. iMod (@gen_heap_alloc with "Hσ") as "[Hσ Hl]"; first done.
......
...@@ -76,7 +76,8 @@ Section Rules_pre. ...@@ -76,7 +76,8 @@ Section Rules_pre.
Global Instance preStackLink_persistent (Q : D) v `{ vw, PersistentP (Q vw)} : Global Instance preStackLink_persistent (Q : D) v `{ vw, PersistentP (Q vw)} :
PersistentP (preStackLink Q v). PersistentP (preStackLink Q v).
Proof. Proof.
rewrite /PersistentP.
iIntros "H". iLöb as "IH" forall (v). rewrite preStackLink_unfold. iIntros "H". iLöb as "IH" forall (v). rewrite preStackLink_unfold.
iDestruct "H" as (l w) "[% [#Hl [[% %]|Hr]]]"; subst. iDestruct "H" as (l w) "[% [#Hl [[% %]|Hr]]]"; subst.
{ iExists l, _; iAlways; eauto. } { iExists l, _; iAlways; eauto. }
......
...@@ -73,7 +73,7 @@ Section interp_env_facts. ...@@ -73,7 +73,7 @@ Section interp_env_facts.
Lemma interp_env_nil Δ E1 E2 : True interp_env E1 E2 Δ . Lemma interp_env_nil Δ E1 E2 : True interp_env E1 E2 Δ .
Proof. Proof.
iIntros ""; iSplit. iIntros "_". iSplit.
- iPureIntro. unfold_leibniz. by rewrite ?dom_empty. - iPureIntro. unfold_leibniz. by rewrite ?dom_empty.
- rewrite map_zip_with_empty. auto. - rewrite map_zip_with_empty. auto.
Qed. Qed.
...@@ -188,6 +188,7 @@ Section related_facts. ...@@ -188,6 +188,7 @@ Section related_facts.
ElimModal (|={E1,E2}=> P) P ElimModal (|={E1,E2}=> P) P
({E1,E2;Δ;Γ} e log e' : τ) ({E2,E2;Δ;Γ} e log e' : τ) | 10. ({E1,E2;Δ;Γ} e log e' : τ) ({E2,E2;Δ;Γ} e log e' : τ) | 10.
Proof. Proof.
rewrite /ElimModal.
iIntros "[HP HI]". iApply fupd_logrel. iIntros "[HP HI]". iApply fupd_logrel.
iMod "HP". iApply ("HI" with "HP"). iMod "HP". iApply ("HI" with "HP").
Qed. Qed.
...@@ -196,6 +197,7 @@ Section related_facts. ...@@ -196,6 +197,7 @@ Section related_facts.
ElimModal (|={E1}=> P) P ElimModal (|={E1}=> P) P
({E1,E2;Δ;Γ} e log e' : τ) ({E1,E2;Δ;Γ} e log e' : τ) | 0. ({E1,E2;Δ;Γ} e log e' : τ) ({E1,E2;Δ;Γ} e log e' : τ) | 0.
Proof. Proof.
rewrite /ElimModal.
iIntros "[HP HI]". iApply fupd_logrel'. iIntros "[HP HI]". iApply fupd_logrel'.
iMod "HP". iApply ("HI" with "HP"). iMod "HP". iApply ("HI" with "HP").
Qed. Qed.
......
...@@ -20,7 +20,7 @@ Lemma logrel_adequate Σ `{logrelPreG Σ} ...@@ -20,7 +20,7 @@ Lemma logrel_adequate Σ `{logrelPreG Σ}
(ObsType τ v = v')). (ObsType τ v = v')).
Proof. Proof.
intros Hlog. intros Hlog.
eapply (heap_adequacy Σ _); iIntros (Hinv). eapply (heap_adequacy Σ _); iIntros (Hinv) "_".
iMod (own_alloc ( (to_tpool [e'], ) iMod (own_alloc ( (to_tpool [e'], )
((to_tpool [e'] : tpoolUR, ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]". ((to_tpool [e'] : tpoolUR, ) : cfgUR))) as (γc) "[Hcfg1 Hcfg2]".
{ apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. } { apply auth_valid_discrete_2. split=>//. split=>//. apply to_tpool_valid. }
...@@ -32,8 +32,8 @@ Proof. ...@@ -32,8 +32,8 @@ Proof.
iSplitL. iSplitL.
- iPoseProof (Hlog _) as "Hrel". - iPoseProof (Hlog _) as "Hrel".
rewrite bin_log_related_eq /bin_log_related_def. rewrite bin_log_related_eq /bin_log_related_def.
iSpecialize ("Hrel" with "[$Hcfg] []"). iSpecialize ("Hrel" $! with "[$Hcfg] []").
{ iApply logrel_binary.interp_env_nil. } { iAlways. by iApply logrel_binary.interp_env_nil. }
rewrite /env_subst !fmap_empty !subst_p_empty. rewrite /env_subst !fmap_empty !subst_p_empty.
iApply fupd_wp. iApply fupd_wp.
iApply ("Hrel" $! 0 []). simpl. iApply ("Hrel" $! 0 []). simpl.
......
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