Commit 9f8ab0ac authored by Dan Frumin's avatar Dan Frumin

Update to the latest Iris version

parent 62b6b4ff
......@@ -161,10 +161,10 @@ Section a_wp_rules.
iIntros (w) "[HΦ $]". by iApply "Hv".
Qed.
Lemma awp_pure K φ e1 e2 R Φ :
PureExec φ e1 e2
Lemma awp_pure K φ n e1 e2 R Φ :
PureExec φ n e1 e2
φ
AWP (fill K e2) @ R {{ Φ }} -
^n AWP (fill K e2) @ R {{ Φ }} -
AWP (fill K e1) @ R {{ Φ }}.
Proof.
iIntros (? Hφ) "Hawp". iApply wp_awp_bind. wp_pure _.
......@@ -184,8 +184,9 @@ Section a_wp_rules.
AWP e @ R {{ ev, AWP (f ev) @ R {{ Φ }} }} -
AWP (a_bind f e) @ R {{ Φ }}.
Proof.
iIntros ([fv <-]) "Hwp". rewrite /awp /a_bind /=. wp_lam. wp_bind e.
iApply (wp_wand with "Hwp"). iIntros (ev) "Hwp". wp_lam.
iIntros ([fv <-]) "Hwp". rewrite /awp /a_bind /=.
wp_apply (wp_wand with "Hwp"). iIntros (ev) "Hwp".
wp_lam. wp_lam.
iIntros (γ env l I) "#Hflock Hres #Heq". do 2 wp_lam. wp_bind (ev env l).
iApply (wp_wand with "[Hwp Hres]"). iApply ("Hwp" with "Hflock Hres Heq").
iIntros (w) "[Hwp Hres]". wp_let. wp_apply (wp_wand with "Hwp").
......@@ -249,15 +250,15 @@ Section a_wp_rules.
Lemma awp_par (Ψ1 Ψ2 : val iProp Σ) e1 e2 R (Φ : val iProp Σ) :
AWP e1 @ R {{ Ψ1 }} -
AWP e2 @ R {{ Ψ2 }} -
AWP e2 @ R {{ Ψ2 }} -
( w1 w2, Ψ1 w1 - Ψ2 w2 - Φ (w1,w2)%V) -
AWP e1 ||| e2 @ R {{ Φ }}.
Proof.
iIntros "Hwp1 Hwp2 HΦ". rewrite /a_par /awp /=.
wp_bind e1. iApply (wp_wand with "Hwp1").
iIntros (ev1) "Hwp1". wp_lam.
wp_bind e2. iApply (wp_wand with "Hwp2").
iIntros (ev2) "Hwp2". wp_lam.
wp_apply (wp_wand with "Hwp2").
iIntros (ev2) "Hwp2".
wp_apply (wp_wand with "Hwp1").
iIntros (ev1) "Hwp1". do 2 wp_lam.
iIntros (γ env l I) "#Hlock Hres #Heq". do 2 wp_lam.
pose (I' := fmap (λ x, (x.1, (x.2/2)%Qp)) I).
iAssert (flock_resources γ I' flock_resources γ I')%I with "[Hres]" as "[Hres1 Hres2]".
......
......@@ -28,15 +28,16 @@ Tactic Notation "awp_apply" open_constr(lem) :=
| _ => fail "awp_apply: not a 'awp'"
end).
Lemma tac_awp_pure `{amonadG Σ} Δ Δ' K e1 e2 e φ R Φ :
Lemma tac_awp_pure `{amonadG Σ} Δ Δ' K e1 e2 e φ n R Φ :
e = fill K e1
PureExec φ e1 e2
PureExec φ n e1 e2
φ
MaybeIntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs n Δ Δ'
envs_entails Δ' (awp (fill K e2) R Φ)
envs_entails Δ (awp e R Φ).
Proof.
rewrite envs_entails_eq=> -> ??? HΔ'. rewrite into_laterN_env_sound /=.
rewrite envs_entails_eq=> -> ??? HΔ'.
rewrite into_laterN_env_sound /=.
rewrite HΔ' -awp_pure //.
Qed.
......
......@@ -182,8 +182,9 @@ Section proofs.
AWP alloc(e1, e2) @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1".
do 2 awp_lam.
iApply awp_bind. iApply (awp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>". awp_let. do 2 (awp_proj; awp_let).
iDestruct ("HΦ" with "H1 H2") as (n ->) "HΦ".
......@@ -207,8 +208,9 @@ Section proofs.
AWP e1 = e2 @ R {{ Φ }}.
Proof.
iIntros "H1 H2 HΦ".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1". awp_lam.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2". awp_lam.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "H2".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "H1".
do 2 awp_lam.
iApply awp_bind. iApply (awp_par with "H1 H2").
iIntros "!>" (w1 w2) "H1 H2 !>". awp_lam.
iDestruct ("HΦ" with "H1 H2") as (cl w ->) "[Hl HΦ]".
......@@ -305,11 +307,11 @@ Section proofs.
Lemma a_sequence_spec R Φ (f e : expr) :
AsVal f
AWP e @ R {{ v, U (AWP (f v) @ R {{ Φ }}) }} -
AWP e @ R {{ v, U (AWP (f v) @ R {{ Φ }}) }} -
AWP a_seq_bind f e @ R {{ Φ }}.
Proof.
iIntros ([fv <-]) "H". rewrite /a_seq_bind /=. awp_lam.
awp_apply (a_wp_awp with "H"); iIntros (v) "H". awp_lam.
iIntros ([fv <-]) "H". rewrite /a_seq_bind /=.
awp_apply (a_wp_awp with "H"); iIntros (v) "H". do 2 awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). iIntros (w) "H".
awp_lam. iApply awp_bind. iApply a_seq_spec.
iModIntro. by awp_lam.
......@@ -317,12 +319,12 @@ Section proofs.
Lemma a_sequence_spec' R Φ (e e' : expr) :
Closed [] e'
AWP e @ R {{ v, U (AWP e' @ R {{ Φ }}) }} -
AWP e @ R {{ v, U (AWP e' @ R {{ Φ }}) }} -
AWP a_seq_bind (λ: <>, e') e @ R {{ Φ }}.
Proof.
iIntros (?) "He".
iApply a_sequence_spec.
iApply (awp_wand with "He"). iNext.
iApply (awp_wand with "He").
iIntros (?) "He'". iModIntro. by awp_lam.
Qed.
......@@ -335,14 +337,14 @@ Section proofs.
iApply "H".
Qed.
Lemma a_if_spec R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
Lemma a_if_spec R Φ (e e1 e2 : expr) :
AsVal e1
AsVal e2
AWP e @ R {{ v, (v = #true AWP e1 #() @ R {{ Φ }})
(v = #false AWP e2 #() @ R {{ Φ }}) }} -
AWP a_if e e1 e2 @ R {{ Φ }}.
Proof.
iIntros ([v1 <-] [v2 <-]) "H".
iIntros ([v1 <-] [v2 <-]) "H /=".
awp_apply (a_wp_awp with "H"). iIntros (v) "H". do 3 awp_lam.
iApply awp_bind. iApply (awp_wand with "H"). clear v.
iIntros (v) "[[% H] | [% H]]"; simplify_eq; awp_lam; by awp_if.
......@@ -368,7 +370,7 @@ Section proofs.
iApply a_if_spec.
iApply (awp_wand with "H").
iIntros (v) "[[% Hv]|[% Hv]]"; subst; [iLeft|iRight]; iSplit; eauto.
awp_seq. iApply a_sequence_spec'. iNext.
awp_seq. iApply a_sequence_spec'.
awp_seq. done.
Qed.
......@@ -379,15 +381,13 @@ Section proofs.
AWP a_invoke ef ea @ R {{ Φ }}.
Proof.
rewrite /IntoVal. iIntros (<-) "Ha Hfa".
rewrite /a_invoke. awp_lam.
rewrite /a_invoke.
awp_apply (a_wp_awp R with "Ha").
iIntros (a) "Ha". awp_let.
iIntros (a) "Ha". do 2 awp_let.
iApply a_sequence_spec.
iApply (awp_wand with "Ha"). clear a.
iNext. iIntros (a) "HΨ".
iSpecialize ("Hfa" with "HΨ").
iModIntro.
awp_let.
iIntros (a) "HΨ". iSpecialize ("Hfa" with "HΨ").
iModIntro. awp_let.
iApply awp_atomic. iNext. iIntros "HR".
iDestruct ("Hfa" with "HR") as (R') "[HR' Hfa]".
iExists R'. iFrame. by awp_let.
......@@ -422,8 +422,9 @@ Section proofs.
AWP a_ptr_plus e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He2 HΦ". rewrite /a_ptr_plus.
awp_apply (a_wp_awp with "HΦ"); iIntros (a1) "Ha1". awp_lam.
awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2".
awp_apply (a_wp_awp with "HΦ"); iIntros (a1) "Ha1".
do 2 awp_lam.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
iDestruct ("Hv1" with "Hv2") as (cl n -> ->) "HΦ /=".
......@@ -441,8 +442,9 @@ Section proofs.
AWP a_ptr_lt e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He1 HΦ". rewrite /a_ptr_plus.
awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
awp_apply (a_wp_awp with "HΦ"); iIntros (a2) "Ha2". awp_lam.
awp_apply (a_wp_awp with "HΦ"); iIntros (a2) "Ha2".
awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1".
do 2 awp_lam.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
iDestruct ("Hv2" with "Hv1") as ([pl pi] [ql qi] -> ->) "HΦ /=".
......@@ -463,8 +465,9 @@ Section proofs.
Proof.
iIntros "H1 H2 HΦ".
destruct op as [op'| |].
- awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1". awp_lam.
awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2". awp_lam.
- awp_apply (a_wp_awp with "H2"); iIntros (v2) "HΨ2".
awp_apply (a_wp_awp with "H1"); iIntros (v1) "HΨ1".
do 2 awp_lam.
iApply awp_bind.
iApply (awp_par Ψ1 Ψ2 with "HΨ1 HΨ2").
iNext. iIntros (w1 w2) "HΨ1 HΨ2"; subst.
......@@ -501,8 +504,9 @@ Section proofs.
AWP a_pre_bin_op op e1 e2 @ R {{ Φ }}.
Proof.
iIntros "He1 He2 HΦ". rewrite /a_pre_bin_op.
awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1". awp_lam.
awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2". awp_lam.
awp_apply (a_wp_awp with "He2"); iIntros (a2) "Ha2".
awp_apply (a_wp_awp with "He1"); iIntros (a1) "Ha1".
do 2 awp_lam.
iApply awp_bind. iApply (awp_par with "Ha1 Ha2"). iNext.
iIntros (v1 v2) "Hv1 Hv2 !>". awp_let.
iApply awp_atomic. iNext.
......@@ -536,7 +540,7 @@ Section proofs.
iIntros (v) "[(% & H) | (% & H)] //="; subst.
- iRight. iSplit; by eauto; iApply a_seq_spec.
- iLeft. iSplit; first eauto. awp_seq.
iApply a_sequence_spec. iNext. awp_seq.
iApply a_sequence_spec. awp_seq.
iApply (awp_wand with "H").
iIntros (v) "Hi !>". awp_seq.
by iApply ("IH" with "Hi").
......
......@@ -39,7 +39,7 @@ Section factorial_spec.
vcg_solver. rewrite Qp_half_half. iIntros "Hr Hc".
case_bool_decide.
+ iLeft. iSplit; eauto.
iApply a_sequence_spec'; iNext.
iApply a_sequence_spec'.
iApply (incr_spec with "Hc"). iIntros "Hc".
iModIntro. vcg_solver. iIntros "Hc Hr".
iModIntro.
......@@ -79,7 +79,7 @@ Section factorial_spec.
vcg_solver. iIntros "Hr Hc".
case_bool_decide.
+ iRight. iSplit; eauto.
iNext. iApply a_sequence_spec'. iNext. rewrite Qp_half_half.
iNext. iApply a_sequence_spec'. rewrite Qp_half_half.
iApply (incr_spec with "Hc").
iIntros "Hc". iModIntro. vcg_solver.
iIntros "Hc Hr". iModIntro.
......
......@@ -30,7 +30,7 @@ Section gcd_spec.
iIntros (??) "Hl Hr". unfold gcd. do 2 awp_lam.
(* vcg_solver. *)
(* iIntros "Hr Hl". *)
iApply a_sequence_spec'. iNext.
iApply a_sequence_spec'.
iApply (a_while_inv_spec ( x y : Z,
0 x 0 y Z.gcd x y = Z.gcd a b l C #x r C #y)%I with "[Hl Hr]").
- iExists a, b. eauto with iFrame.
......
(** * Reified environments *)
From iris.proofmode Require Import environments coq_tactics.
Import env_notations.
From iris_c.vcgen Require Import dcexpr.
From iris_c.c_translation Require Import monad.
From iris.algebra Require Import frac.
......@@ -759,7 +758,7 @@ Section denv_spec.
- naive_solver.
- apply IHm1. simpl in Hwf.
destruct a as [d|]; last done.
destruct d. naive_solver.
destruct d. by destruct_and!.
Qed.
Lemma denv_wf_mono E E' m :
......
......@@ -562,10 +562,10 @@ Section vcg_spec.
generalize dependent dv. induction de; intros dv Hdv; simplify_eq/=.
- by iApply wp_value.
- simplify_option_eq.
wp_bind (dexpr_interp E de1). iApply wp_wand; first by iApply IHde1.
iIntros (? ->).
wp_bind (dexpr_interp E de2). iApply wp_wand; first by iApply IHde2.
iIntros (? ->).
wp_bind (dexpr_interp E de1). iApply wp_wand; first by iApply IHde1.
iIntros (? ->).
by iApply wp_value.
- destruct (vcg_eval_dexpr de) as [dv'|] eqn:Hde'; simplify_eq/=.
destruct dv'; simplify_eq/=.
......@@ -748,7 +748,7 @@ Section vcg_spec.
iApply (denv_stack_interp_mono with "Hawp"). iIntros "[Hawp1 Hawp2]".
iApply a_sequence_spec'.
{ by apply dcexpr_closed. }
iNext. iApply (awp_wand with "Hawp1").
iApply (awp_wand with "Hawp1").
iIntros (?) "[% HmNew1]". simplify_eq/=. iClear "Hawp".
rewrite (denv_unlock_interp E mNew1).
iModIntro. iDestruct ("Hawp2" with "HmNew1") as "[HmNew' Hawp2]".
......@@ -1180,7 +1180,7 @@ Section vcg_spec.
- simpl in Hwf; apply andb_prop_elim in Hwf as [Hwf1 Hwf2].
rewrite (IH de1) //. iSpecialize ("Hm" with "Hwp"); fold vcg_wp.
iApply (a_sequence_spec' with "[Hm]"); fold dcexpr_interp. by apply dcexpr_closed.
iNext. iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iApply (awp_wand with "Hm"). iIntros (v) "Hex".
iDestruct "Hex" as (Enew dv m' Hpre Hpre' Hm'wf) "(% & Hm & Hwp)". simpl.
rewrite denv_unlock_interp.
iModIntro. rewrite (IH de2) //. iSpecialize ("Hm" with "Hwp").
......
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