lifting.v 6.17 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2
From iris.proofmode Require Import tactics.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5

Section lifting.
6
Context `{irisG Λ Σ}.
7
Implicit Types s : stuckness.
8 9 10
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
11 12
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ  iProp Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
13

Ralf Jung's avatar
fix TWP  
Ralf Jung committed
14 15
Hint Resolve reducible_no_obs_reducible.

16
Lemma wp_lift_step_fupd s E Φ e1 :
17
  to_val e1 = None 
18
  ( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,}=
Ralf Jung's avatar
Ralf Jung committed
19
    if s is NotStuck then reducible e1 σ1 else True 
20
     e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs ={,,E}=
21 22
      state_interp σ2 κs (length efs + n) 
      WP e2 @ s; E {{ Φ }} 
23
      [ list] ef  efs, WP ef @ s;  {{ fork_post }})
24 25
   WP e1 @ s; E {{ Φ }}.
Proof.
26
  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs n) "Hσ".
27
  iMod ("H" with "Hσ") as "(%&H)". iModIntro. iSplit. by destruct s.
28
  iIntros (????). iApply "H". eauto.
29 30 31 32
Qed.

Lemma wp_lift_stuck E Φ e :
  to_val e = None 
33
  ( σ κs n, state_interp σ κs n ={E,}= stuck e σ⌝)
34 35
   WP e @ E ?{{ Φ }}.
Proof.
36
  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs n) "Hσ".
37
  iMod ("H" with "Hσ") as %[? Hirr]. iModIntro. iSplit; first done.
38
  iIntros (e2 σ2 efs ?). by case: (Hirr κ e2 σ2 efs).
39
Qed.
40

41
(** Derived lifting lemmas. *)
42 43
Lemma wp_lift_step s E Φ e1 :
  to_val e1 = None 
44
  ( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,}=
45
    if s is NotStuck then reducible e1 σ1 else True 
46
      e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs ={,E}=
47 48
      state_interp σ2 κs (length efs + n) 
      WP e2 @ s; E {{ Φ }} 
49
      [ list] ef  efs, WP ef @ s;  {{ fork_post }})
50 51
   WP e1 @ s; E {{ Φ }}.
Proof.
52 53
  iIntros (?) "H". iApply wp_lift_step_fupd; [done|]. iIntros (????) "Hσ".
  iMod ("H" with "Hσ") as "[$ H]". iIntros "!> * % !> !>". by iApply "H".
54 55
Qed.

56 57
Lemma wp_lift_pure_step_no_fork `{Inhabited (state Λ)} s E E' Φ e1 :
  ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
58
  ( κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs  κ = []  σ2 = σ1  efs = []) 
59 60 61 62 63 64 65 66 67 68 69 70
  (|={E,E'}=>  κ e2 efs σ, prim_step e1 σ κ e2 σ efs  WP e2 @ s; E {{ Φ }})
   WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
  { specialize (Hsafe inhabitant). destruct s; eauto using reducible_not_val. }
  iIntros (σ1 κ κs n) "Hσ". iMod "H".
  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
  { iPureIntro. destruct s; done. }
  iNext. iIntros (e2 σ2 efs ?).
  destruct (Hstep κ σ1 e2 σ2 efs) as (-> & <- & ->); auto.
  iMod "Hclose" as "_". iMod "H". iModIntro.
  iDestruct ("H" with "[//]") as "H". simpl. iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
71
Qed.
72

73
Lemma wp_lift_pure_stuck `{Inhabited (state Λ)} E Φ e :
74
  ( σ, stuck e σ) 
75 76 77 78
  True  WP e @ E ?{{ Φ }}.
Proof.
  iIntros (Hstuck) "_". iApply wp_lift_stuck.
  - destruct(to_val e) as [v|] eqn:He; last done.
79
    rewrite -He. by case: (Hstuck inhabitant).
80
  - iIntros (σ κs n) "_". by iMod (fupd_intro_mask' E ) as "_"; first set_solver.
81 82
Qed.

83 84
(* Atomic steps don't need any mask-changing business here, one can
   use the generic lemmas here. *)
85 86
Lemma wp_lift_atomic_step_fupd {s E1 E2 Φ} e1 :
  to_val e1 = None 
87
  ( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=
88
    if s is NotStuck then reducible e1 σ1 else True 
89
     e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs ={E1,E2}=
90 91
      state_interp σ2 κs (length efs + n) 
      from_option Φ False (to_val e2) 
92
      [ list] ef  efs, WP ef @ s;  {{ fork_post }})
93 94
   WP e1 @ s; E1 {{ Φ }}.
Proof.
95 96
  iIntros (?) "H".
  iApply (wp_lift_step_fupd s E1 _ e1)=>//; iIntros (σ1 κ κs n) "Hσ1".
97 98
  iMod ("H" $! σ1 with "Hσ1") as "[$ H]".
  iMod (fupd_intro_mask' E1 ) as "Hclose"; first set_solver.
99 100
  iIntros "!>" (e2 σ2 efs ?). iMod "Hclose" as "_".
  iMod ("H" $! e2 σ2 efs with "[#]") as "H"; [done|].
101
  iMod (fupd_intro_mask' E2 ) as "Hclose"; [set_solver|]. iIntros "!> !>".
102
  iMod "Hclose" as "_". iMod "H" as "($ & HQ & $)".
103
  destruct (to_val e2) eqn:?; last by iExFalso.
104
  iApply wp_value; last done. by apply of_to_val.
105 106
Qed.

107
Lemma wp_lift_atomic_step {s E Φ} e1 :
108
  to_val e1 = None 
109
  ( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=
Ralf Jung's avatar
Ralf Jung committed
110
    if s is NotStuck then reducible e1 σ1 else True 
111
      e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs ={E}=
112 113
      state_interp σ2 κs (length efs + n) 
      from_option Φ False (to_val e2) 
114
      [ list] ef  efs, WP ef @ s;  {{ fork_post }})
115
   WP e1 @ s; E {{ Φ }}.
116
Proof.
117
  iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
118
  iIntros (????) "?". iMod ("H" with "[$]") as "[$ H]".
119
  iIntros "!> *". iIntros (Hstep) "!> !>".
120
  by iApply "H".
121 122
Qed.

123 124 125
Lemma wp_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E E' Φ} e1 e2 :
  ( σ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' 
126
    κ = []  σ2 = σ1  e2' = e2  efs' = []) 
127 128 129 130 131 132 133 134
  (|={E,E'}=> WP e2 @ s; E {{ Φ }})  WP e1 @ s; E {{ Φ }}.
Proof.
  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step_no_fork s E E'); try done.
  { naive_solver. }
  iApply (step_fupd_wand with "H"); iIntros "H".
  iIntros (κ e' efs' σ (_&?&->&?)%Hpuredet); auto.
Qed.

135 136
Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ n Φ :
  PureExec φ n e1 e2 
Dan Frumin's avatar
Dan Frumin committed
137
  φ 
138
  (|={E,E'}=>^n WP e2 @ s; E {{ Φ }})  WP e1 @ s; E {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
139
Proof.
140 141
  iIntros (Hexec Hφ) "Hwp". specialize (Hexec Hφ).
  iInduction Hexec as [e|n e1 e2 e3 [Hsafe ?]] "IH"; simpl; first done.
142
  iApply wp_lift_pure_det_step_no_fork.
143
  - intros σ. specialize (Hsafe σ). destruct s; eauto using reducible_not_val.
144 145
  - done.
  - by iApply (step_fupd_wand with "Hwp").
Dan Frumin's avatar
Dan Frumin committed
146 147
Qed.

148 149
Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ n Φ :
  PureExec φ n e1 e2 
Dan Frumin's avatar
Dan Frumin committed
150
  φ 
151
  ^n WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
152
Proof.
153 154
  intros Hexec ?. rewrite -wp_pure_step_fupd //. clear Hexec.
  induction n as [|n IH]; by rewrite //= -step_fupd_intro // IH.
Dan Frumin's avatar
Dan Frumin committed
155
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
156
End lifting.