lifting.v 6.01 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, state_interp σ1 (cons_obs κ κs) ={E,}=
Ralf Jung's avatar
Ralf Jung committed
19
    if s is NotStuck then reducible e1 σ1 else True 
20 21
     e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs ={,,E}=
      state_interp σ2 κs  WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
22 23
   WP e1 @ s; E {{ Φ }}.
Proof.
24
  rewrite wp_unfold /wp_pre=>->. iIntros "H" (σ1 κ κs) "Hσ".
25
  iMod ("H" with "Hσ") as "(%&H)". iModIntro. iSplit. by destruct s.
26
  iIntros (????). iApply "H". eauto.
27 28 29 30
Qed.

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

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

52
Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
Ralf Jung's avatar
Ralf Jung committed
53
  ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
54
  ( κ σ1 e2 σ2 efs, prim_step e1 σ1 κ e2 σ2 efs  κ = None  σ1 = σ2) 
55
  (|={E,E'}=>  κ e2 efs σ, prim_step e1 σ κ e2 σ efs 
56 57
    WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
Proof.
59
  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
60 61
  { specialize (Hsafe inhabitant). destruct s; last done.
      by eapply reducible_not_val. }
62
  iIntros (σ1 κ κs) "Hσ". iMod "H".
63 64
  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
  { iPureIntro. destruct s; done. }
65
  iNext. iIntros (e2 σ2 efs Hstep').
66
  destruct (Hstep κ σ1 e2 σ2 efs); auto; subst; clear Hstep.
Ralf Jung's avatar
Ralf Jung committed
67
  iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Qed.
69

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

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

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

118
Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
Ralf Jung's avatar
Ralf Jung committed
119
  ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
120
  ( σ1 κ e2' σ2 efs', prim_step e1 σ1 κ e2' σ2 efs'  κ = None  σ1 = σ2  e2 = e2'  efs = efs')
121 122
  (|={E,E'}=> WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
123
Proof.
124
  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step s E E'); try done.
125
  { by naive_solver. }
126
  iApply (step_fupd_wand with "H"); iIntros "H".
127
  by iIntros (κ e' efs' σ (->&_&->&->)%Hpuredet).
128
Qed.
Dan Frumin's avatar
Dan Frumin committed
129

130
Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ Φ :
Dan Frumin's avatar
Dan Frumin committed
131 132
  PureExec φ e1 e2 
  φ 
133
  (|={E,E'}=> WP e2 @ s; E {{ Φ }})  WP e1 @ s; E {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
134 135
Proof.
  iIntros ([??] Hφ) "HWP".
136
  iApply (wp_lift_pure_det_step with "[HWP]").
137
  - intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val.
138
  - destruct s; naive_solver.
139
  - by rewrite big_sepL_nil right_id.
Dan Frumin's avatar
Dan Frumin committed
140 141
Qed.

142
Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ :
Dan Frumin's avatar
Dan Frumin committed
143 144
  PureExec φ e1 e2 
  φ 
145
   WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
146 147 148
Proof.
  intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
149
End lifting.