lifting.v 5.67 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

14
Lemma wp_lift_step_fupd s E Φ e1 :
15
16
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E,}=
Ralf Jung's avatar
Ralf Jung committed
17
    if s is NotStuck then reducible e1 σ1 else True 
18
     e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,,E}=
19
20
21
22
      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σ".
23
  iMod ("H" with "Hσ") as "(%&H)". iModIntro. iSplit. by destruct s. done.
24
25
26
27
Qed.

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

36
(** Derived lifting lemmas. *)
37
38
39
40
41
42
43
44
45
46
47
48
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.

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

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

78
79
(* Atomic steps don't need any mask-changing business here, one can
   use the generic lemmas here. *)
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
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.

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

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

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

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