Commit 9fc544a3 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'fupd_step_wp' into 'gen_proofmode'

Slightly weaker WP (i.e., easier to prove), so that we have an fupd where we did not

See merge request FP/iris-coq!153
parents 618c2767 cfb8421a
Pipeline #9694 passed with stage
in 28 minutes and 39 seconds
......@@ -7,6 +7,10 @@ Coq development, but not every API-breaking change is listed. Changes marked
Changes in and extensions of the theory:
* [#] Change in the definition of WP, so that there is a fancy update between
the quantification over the next states and the later modality. This makes it
possible to prove more powerful lifting lemmas: The new versions feature an
"update that take a step".
* [#] Add weakest preconditions for total program correctness.
* [#] "(Potentially) stuck" weakest preconditions are no longer considered
experimental.
......
......@@ -69,6 +69,12 @@ Reserved Notation "P ={ E }=∗ Q"
(at level 99, E at level 50, Q at level 200,
format "'[' P '/' ={ E }=∗ Q ']'").
Reserved Notation "|={ E1 , E2 , E3 }▷=> Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 , E3 }▷=> Q").
Reserved Notation "P ={ E1 , E2 , E3 }▷=∗ Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "'[' P '/' ={ E1 , E2 , E3 }▷=∗ Q ']'").
Reserved Notation "|={ E1 , E2 }▷=> Q"
(at level 99, E1, E2 at level 50, Q at level 200,
format "|={ E1 , E2 }▷=> Q").
......
......@@ -25,8 +25,10 @@ Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I : bi_scope.
Notation "P ={ E }=∗ Q" := (P - |={E}=> Q) : stdpp_scope.
(** Fancy updates that take a step. *)
Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2}=> ( |={E2,E1}=> Q))%I : bi_scope.
Notation "P ={ E1 , E2 }▷=∗ Q" := (P - |={ E1 , E2 }=> Q)%I : bi_scope.
Notation "|={ E1 , E2 , E3 }▷=> Q" := (|={E1,E2}=> ( |={E2,E3}=> Q))%I : bi_scope.
Notation "P ={ E1 , E2 , E3 }▷=∗ Q" := (P - |={ E1,E2,E3 }=> Q)%I : bi_scope.
Notation "|={ E1 , E2 }▷=> Q" := (|={E1,E2,E1}=> Q)%I : bi_scope.
Notation "P ={ E1 , E2 }▷=∗ Q" := (P - |={ E1 , E2, E1 }=> Q)%I : bi_scope.
Notation "|={ E }▷=> Q" := (|={E,E}=> Q)%I : bi_scope.
Notation "P ={ E }▷=∗ Q" := (P ={E,E}= Q)%I : bi_scope.
......@@ -277,15 +279,15 @@ Section fupd_derived.
Qed.
(** Fancy updates that take a step derived rules. *)
Lemma step_fupd_wand E1 E2 P Q : (|={E1,E2}=> P) - (P - Q) - |={E1,E2}=> Q.
Lemma step_fupd_wand E1 E2 E3 P Q : (|={E1,E2,E3}=> P) - (P - Q) - |={E1,E2,E3}=> Q.
Proof.
apply wand_intro_l.
by rewrite (later_intro (P - Q)%I) fupd_frame_l -later_sep fupd_frame_l
wand_elim_l.
Qed.
Lemma step_fupd_mask_frame_r E1 E2 Ef P :
E1 ## Ef E2 ## Ef (|={E1,E2}=> P) |={E1 Ef,E2 Ef}=> P.
Lemma step_fupd_mask_frame_r E1 E2 E3 Ef P :
E1 ## Ef E2 ## Ef (|={E1,E2,E3}=> P) |={E1 Ef,E2 Ef,E3 Ef}=> P.
Proof.
intros. rewrite -fupd_mask_frame_r //. do 2 f_equiv. by apply fupd_mask_frame_r.
Qed.
......
......@@ -77,8 +77,8 @@ Proof.
rewrite {1}wp_unfold /wp_pre. iIntros (?) "[(Hw & HE & Hσ) H]".
rewrite (val_stuck e1 σ1 e2 σ2 efs) // uPred_fupd_eq.
iMod ("H" $! σ1 with "Hσ [Hw HE]") as ">(Hw & HE & _ & H)"; first by iFrame.
iModIntro; iNext.
iMod ("H" $! e2 σ2 efs with "[%] [$Hw $HE]") as ">($ & $ & $ & $)"; auto.
iMod ("H" $! e2 σ2 efs with "[//] [$Hw $HE]") as ">(Hw & HE & H)".
iIntros "!> !>". by iMod ("H" with "[$Hw $HE]") as ">($ & $ & $)".
Qed.
Lemma wptp_step s e1 t1 t2 σ1 σ2 Φ :
......
......@@ -14,20 +14,32 @@ Hint Resolve head_prim_reducible head_reducible_prim_step.
Hint Resolve (reducible_not_val _ inhabitant).
Hint Resolve head_stuck_stuck.
Lemma wp_lift_head_step {s E Φ} e1 :
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E,}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={,E}=
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={,,E}=
state_interp σ2 WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_step=>//. iIntros (σ1) "Hσ".
iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1) "Hσ".
iMod ("H" with "Hσ") as "[% H]"; iModIntro.
iSplit; first by destruct s; eauto. iNext. iIntros (e2 σ2 efs) "%".
iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs) "%".
iApply "H"; eauto.
Qed.
Lemma wp_lift_head_step {s E Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E,}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={,E}=
state_interp σ2 WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (?) "?".
iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "!> !>". by iApply "H".
Qed.
Lemma wp_lift_head_stuck E Φ e :
to_val e = None
sub_redexes_are_values e
......@@ -45,7 +57,7 @@ Lemma wp_lift_pure_head_step {s E E' Φ} e1 :
WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof using Hinh.
iIntros (??) "H". iApply wp_lift_pure_step; eauto.
iIntros (??) "H". iApply wp_lift_pure_step; [|by eauto|].
{ by destruct s; auto. }
iApply (step_fupd_wand with "H"); iIntros "H".
iIntros (????). iApply "H"; eauto.
......@@ -62,6 +74,21 @@ Proof using Hinh.
by auto.
Qed.
Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E1}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E1,E2}=
state_interp σ2
from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E1 {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
iIntros (σ1) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
iSplit; first by destruct s; auto. iIntros (e2 σ2 efs) "%".
iApply "H"; auto.
Qed.
Lemma wp_lift_atomic_head_step {s E Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E}=
......@@ -77,6 +104,20 @@ Proof.
iApply "H"; auto.
Qed.
Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E1}=
head_reducible e1 σ1
e2 σ2 efs, head_step e1 σ1 e2 σ2 efs ={E1,E2}=
efs = [] state_interp σ2 from_option Φ False (to_val e2))
WP e1 @ s; E1 {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_atomic_head_step_fupd; [done|].
iIntros (σ1) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
iIntros (v2 σ2 efs) "%". iMod ("H" $! v2 σ2 efs with "[# //]") as "H".
iIntros "!> !>". iMod "H" as "(% & $ & $)"; subst; auto.
Qed.
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E}=
......
......@@ -11,16 +11,16 @@ Implicit Types σ : state Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Lemma wp_lift_step s E Φ e1 :
Lemma wp_lift_step_fupd s E Φ e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E,}=
if s is NotStuck then reducible e1 σ1 else True
e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,,E}=
state_interp σ2 WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1) "Hσ".
iMod ("H" with "Hσ") as "(%&?)". iModIntro. iSplit. by destruct s. done.
iMod ("H" with "Hσ") as "(%&H)". iModIntro. iSplit. by destruct s. done.
Qed.
Lemma wp_lift_stuck E Φ e :
......@@ -30,10 +30,22 @@ Lemma wp_lift_stuck E Φ e :
Proof.
rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1) "Hσ".
iMod ("H" with "Hσ") as %[? Hirr]. iModIntro. iSplit; first done.
iIntros "!>" (e2 σ2 efs) "%". by case: (Hirr e2 σ2 efs).
iIntros (e2 σ2 efs) "% !> !>". by case: (Hirr e2 σ2 efs).
Qed.
(** Derived lifting lemmas. *)
Lemma wp_lift_step s E Φ e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E,}=
if s is NotStuck then reducible e1 σ1 else True
e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
state_interp σ2 WP e2 @ s; E {{ Φ }} [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (?) "Hσ".
iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % !>". by iApply "H".
Qed.
Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None)
( σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs σ1 = σ2)
......@@ -65,6 +77,26 @@ Qed.
(* Atomic steps don't need any mask-changing business here, one can
use the generic lemmas here. *)
Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E1}=
if s is NotStuck then reducible e1 σ1 else True
e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={E1,E2}=
state_interp σ2
from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E1 {{ Φ }}.
Proof.
iIntros (?) "H". iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1) "Hσ1".
iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
iMod (fupd_intro_mask' E1 ) as "Hclose"; first set_solver.
iIntros "!>" (e2 σ2 efs ?). iMod "Hclose" as "_".
iMod ("H" $! e2 σ2 efs with "[#]") as "H"; [done|].
iMod (fupd_intro_mask' E2 ) as "Hclose"; [set_solver|]. iIntros "!> !>".
iMod "Hclose" as "_". iMod "H" as "($ & HΦ & $)".
destruct (to_val e2) eqn:?; last by iExFalso.
by iApply wp_value.
Qed.
Lemma wp_lift_atomic_step {s E Φ} e1 :
to_val e1 = None
( σ1, state_interp σ1 ={E}=
......@@ -74,13 +106,9 @@ Lemma wp_lift_atomic_step {s E Φ} e1 :
from_option Φ False (to_val e2) [ list] ef efs, WP ef @ s; {{ _, True }})
WP e1 @ s; E {{ Φ }}.
Proof.
iIntros (?) "H". iApply (wp_lift_step s E _ e1)=>//; iIntros (σ1) "Hσ1".
iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
iMod (fupd_intro_mask' E ) as "Hclose"; first set_solver.
iModIntro; iNext; iIntros (e2 σ2 efs) "%". iMod "Hclose" as "_".
iMod ("H" $! e2 σ2 efs with "[#]") as "($ & HΦ & $)"; first by eauto.
destruct (to_val e2) eqn:?; last by iExFalso.
by iApply wp_value.
iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
iIntros (?) "?". iMod ("H" with "[$]") as "[$ H]". iIntros "!> * % !> !>".
by iApply "H".
Qed.
Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
......
......@@ -315,9 +315,9 @@ Lemma twp_wp s E e Φ : WP e @ s; E [{ Φ }] -∗ WP e @ s; E {{ Φ }}.
Proof.
iIntros "H". iLöb as "IH" forall (E e Φ).
rewrite wp_unfold twp_unfold /wp_pre /twp_pre. destruct (to_val e) as [v|]=>//.
iIntros (σ1) "Hσ". iMod ("H" with "Hσ") as "[$ H]". iModIntro; iNext.
iIntros (e2 σ2 efs) "Hstep".
iMod ("H" with "Hstep") as "($ & H & Hfork)"; iModIntro.
iIntros (σ1) "Hσ". iMod ("H" with "Hσ") as "[$ H]". iIntros "!>".
iIntros (e2 σ2 efs) "Hstep". iMod ("H" with "Hstep") as "($ & H & Hfork)".
iApply step_fupd_intro; [set_solver+|]. iNext.
iSplitL "H". by iApply "IH". iApply (@big_sepL_impl with "[$Hfork]").
iIntros "!#" (k e' _) "H". by iApply "IH".
Qed.
......
......@@ -32,7 +32,7 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
| Some v => |={E}=> Φ v
| None => σ1,
state_interp σ1 ={E,}= if s is NotStuck then reducible e1 σ1 else True
e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,,E}=
state_interp σ2 wp E e2 Φ
[ list] ef efs, wp ef (λ _, True)
end%I.
......@@ -197,7 +197,7 @@ Proof.
(* FIXME: figure out a way to properly automate this proof *)
(* FIXME: reflexivity, as being called many times by f_equiv and f_contractive
is very slow here *)
do 17 (f_contractive || f_equiv). apply IH; first lia.
do 18 (f_contractive || f_equiv). apply IH; first lia.
intros v. eapply dist_le; eauto with omega.
Qed.
Global Instance wp_proper s E e :
......@@ -221,8 +221,8 @@ Proof.
{ iApply ("HΦ" with "[> -]"). by iApply (fupd_mask_mono E1 _). }
iIntros (σ1) "Hσ". iMod (fupd_intro_mask' E2 E1) as "Hclose"; first done.
iMod ("H" with "[$]") as "[% H]".
iModIntro. iSplit; [by destruct s1, s2|]. iNext. iIntros (e2 σ2 efs Hstep).
iMod ("H" with "[//]") as "($ & H & Hefs)".
iModIntro. iSplit; [by destruct s1, s2|]. iIntros (e2 σ2 efs Hstep).
iMod ("H" with "[//]") as "H". iIntros "!> !>". iMod "H" as "($ & H & Hefs)".
iMod "Hclose" as "_". iModIntro. iSplitR "Hefs".
- iApply ("IH" with "[//] H HΦ").
- iApply (big_sepL_impl with "[$Hefs]"); iIntros "!#" (k ef _) "H".
......@@ -245,8 +245,8 @@ Proof.
destruct (to_val e) as [v|] eqn:He.
{ by iDestruct "H" as ">>> $". }
iIntros (σ1) "Hσ". iMod "H". iMod ("H" $! σ1 with "Hσ") as "[$ H]".
iModIntro. iNext. iIntros (e2 σ2 efs Hstep).
iMod ("H" with "[//]") as "(Hphy & H & $)". destruct s.
iModIntro. iIntros (e2 σ2 efs Hstep).
iMod ("H" with "[//]") as "H". iIntros "!>!>". iMod "H" as "(Hphy & H & $)". destruct s.
- rewrite !wp_unfold /wp_pre. destruct (to_val e2) as [v2|] eqn:He2.
+ iDestruct "H" as ">> $". by iFrame.
+ iMod ("H" with "[$]") as "[H _]". iDestruct "H" as %(? & ? & ? & ?).
......@@ -261,8 +261,8 @@ Lemma wp_step_fupd s E1 E2 e P Φ :
Proof.
rewrite !wp_unfold /wp_pre. iIntros (-> ?) "HR H".
iIntros (σ1) "Hσ". iMod "HR". iMod ("H" with "[$]") as "[$ H]".
iModIntro; iNext; iIntros (e2 σ2 efs Hstep).
iMod ("H" $! e2 σ2 efs with "[% //]") as "($ & H & $)".
iIntros "!>" (e2 σ2 efs Hstep). iMod ("H" $! e2 σ2 efs with "[% //]") as "H".
iIntros "!>!>". iMod "H" as "($ & H & $)".
iMod "HR". iModIntro. iApply (wp_strong_mono s s E2 with "H"); [done..|].
iIntros (v) "H". by iApply "H".
Qed.
......@@ -277,10 +277,10 @@ Proof.
iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
{ iPureIntro. destruct s; last done.
unfold reducible in *. naive_solver eauto using fill_step. }
iNext; iIntros (e2 σ2 efs Hstep).
iIntros (e2 σ2 efs Hstep).
destruct (fill_step_inv e σ1 e2 σ2 efs) as (e2'&->&?); auto.
iMod ("H" $! e2' σ2 efs with "[//]") as "($ & H & $)".
by iApply "IH".
iMod ("H" $! e2' σ2 efs with "[//]") as "H". iIntros "!>!>".
iMod "H" as "($ & H & $)". by iApply "IH".
Qed.
Lemma wp_bind_inv K `{!LanguageCtx K} s E e Φ :
......@@ -292,9 +292,9 @@ Proof.
rewrite fill_not_val //.
iIntros (σ1) "Hσ". iMod ("H" with "[$]") as "[% H]". iModIntro; iSplit.
{ destruct s; eauto using reducible_fill. }
iNext; iIntros (e2 σ2 efs Hstep).
iMod ("H" $! (K e2) σ2 efs with "[]") as "($ & H & $)"; eauto using fill_step.
by iApply "IH".
iIntros (e2 σ2 efs Hstep).
iMod ("H" $! (K e2) σ2 efs with "[]") as "H"; [by eauto using fill_step|].
iIntros "!>!>". iMod "H" as "($ & H & $)". by iApply "IH".
Qed.
(** * Derived rules *)
......
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