ectx_lifting.v 5.82 KB
Newer Older
1
(** Some derived lemmas for ectx-based languages *)
2
From iris.program_logic Require Export ectx_language weakestpre lifting.
3
From iris.proofmode Require Import tactics.
4
Set Default Proof Using "Type".
5 6

Section wp.
7
Context {Λ : ectxLanguage} `{irisG Λ Σ} {Hinh : Inhabited (state Λ)}.
8
Implicit Types s : stuckness.
9
Implicit Types P : iProp Σ.
10 11 12
Implicit Types Φ : val Λ  iProp Σ.
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
Hint Resolve head_prim_reducible head_reducible_prim_step.
14
Hint Resolve (reducible_not_val _ inhabitant).
15
Hint Resolve head_stuck_stuck.
16

17
Lemma wp_lift_head_step_fupd {s E Φ} e1 :
18
  to_val e1 = None 
19
  ( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,}=
20
    head_reducible e1 σ1 
21
     e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={,,E}=
22 23
      state_interp σ2 κs (length efs + n) 
      WP e2 @ s; E {{ Φ }} 
24
      [ list] ef  efs, WP ef @ s;  {{ fork_post }})
25
   WP e1 @ s; E {{ Φ }}.
26
Proof.
27
  iIntros (?) "H". iApply wp_lift_step_fupd=>//. iIntros (σ1 κ κs Qs) "Hσ".
28
  iMod ("H" with "Hσ") as "[% H]"; iModIntro.
29
  iSplit; first by destruct s; eauto. iIntros (e2 σ2 efs ?).
30
  iApply "H"; eauto.
31 32
Qed.

33 34
Lemma wp_lift_head_step {s E Φ} e1 :
  to_val e1 = None 
35
  ( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E,}=
36
    head_reducible e1 σ1 
37
      e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={,E}=
38 39
      state_interp σ2 κs (length efs + n) 
      WP e2 @ s; E {{ Φ }} 
40
      [ list] ef  efs, WP ef @ s;  {{ fork_post }})
41 42
   WP e1 @ s; E {{ Φ }}.
Proof.
43
  iIntros (?) "H". iApply wp_lift_head_step_fupd; [done|]. iIntros (????) "?".
44
  iMod ("H" with "[$]") as "[$ H]". iIntros "!>" (e2 σ2 efs ?) "!> !>". by iApply "H".
45 46
Qed.

47 48
Lemma wp_lift_head_stuck E Φ e :
  to_val e = None 
49
  sub_redexes_are_values e 
50
  ( σ κs n, state_interp σ κs n ={E,}= head_stuck e σ⌝)
51 52
   WP e @ E ?{{ Φ }}.
Proof.
53
  iIntros (??) "H". iApply wp_lift_stuck; first done.
54
  iIntros (σ κs n) "Hσ". iMod ("H" with "Hσ") as "%". by auto.
55 56 57 58
Qed.

Lemma wp_lift_pure_head_stuck E Φ e :
  to_val e = None 
59 60
  sub_redexes_are_values e 
  ( σ, head_stuck e σ) 
61 62
  WP e @ E ?{{ Φ }}%I.
Proof using Hinh.
63
  iIntros (?? Hstuck). iApply wp_lift_head_stuck; [done|done|].
64
  iIntros (σ κs n) "_". iMod (fupd_intro_mask' E ) as "_"; first set_solver.
65
  by auto.
66 67
Qed.

68 69
Lemma wp_lift_atomic_head_step_fupd {s E1 E2 Φ} e1 :
  to_val e1 = None 
70
  ( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=
71
    head_reducible e1 σ1 
72
     e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E1,E2}=
73 74
      state_interp σ2 κs (length efs + n) 
      from_option Φ False (to_val e2) 
75
      [ list] ef  efs, WP ef @ s;  {{ fork_post }})
76 77 78
   WP e1 @ s; E1 {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step_fupd; [done|].
79
  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
80
  iSplit; first by destruct s; auto. iIntros (e2 σ2 efs Hstep).
81
  iApply "H"; eauto.
82 83
Qed.

84
Lemma wp_lift_atomic_head_step {s E Φ} e1 :
85
  to_val e1 = None 
86
  ( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=
87
    head_reducible e1 σ1 
88
      e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E}=
89 90
      state_interp σ2 κs (length efs + n) 
      from_option Φ False (to_val e2) 
91
      [ list] ef  efs, WP ef @ s;  {{ fork_post }})
92
   WP e1 @ s; E {{ Φ }}.
93 94
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_step; eauto.
95
  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" with "Hσ1") as "[% H]"; iModIntro.
96
  iSplit; first by destruct s; auto. iNext. iIntros (e2 σ2 efs Hstep).
97
  iApply "H"; eauto.
98 99
Qed.

100
Lemma wp_lift_atomic_head_step_no_fork_fupd {s E1 E2 Φ} e1 :
101
  to_val e1 = None 
102
  ( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E1}=
103
    head_reducible e1 σ1 
104
     e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E1,E2}=
105
      efs = []  state_interp σ2 κs n  from_option Φ False (to_val e2))
106 107 108
   WP e1 @ s; E1 {{ Φ }}.
Proof.
  iIntros (?) "H". iApply wp_lift_atomic_head_step_fupd; [done|].
109
  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
110 111
  iIntros (v2 σ2 efs Hstep).
  iMod ("H" $! v2 σ2 efs with "[# //]") as "H".
112
  iIntros "!> !>". iMod "H" as "(-> & ? & ?) /=". by iFrame.
113 114
Qed.

115
Lemma wp_lift_atomic_head_step_no_fork {s E Φ} e1 :
116
  to_val e1 = None 
117
  ( σ1 κ κs n, state_interp σ1 (κ ++ κs) n ={E}=
118
    head_reducible e1 σ1 
119
      e2 σ2 efs, head_step e1 σ1 κ e2 σ2 efs ={E}=
120
      efs = []  state_interp σ2 κs n  from_option Φ False (to_val e2))
121
   WP e1 @ s; E {{ Φ }}.
122
Proof.
123
  iIntros (?) "H". iApply wp_lift_atomic_head_step; eauto.
124
  iIntros (σ1 κ κs Qs) "Hσ1". iMod ("H" $! σ1 with "Hσ1") as "[$ H]"; iModIntro.
125
  iNext; iIntros (v2 σ2 efs Hstep).
126
  iMod ("H" $! v2 σ2 efs with "[//]") as "(-> & ? & ?) /=". by iFrame.
127 128
Qed.

129
Lemma wp_lift_pure_det_head_step_no_fork {s E E' Φ} e1 e2 :
130 131
  to_val e1 = None 
  ( σ1, head_reducible e1 σ1) 
132
  ( σ1 κ e2' σ2 efs',
133
    head_step e1 σ1 κ e2' σ2 efs'  κ = []  σ2 = σ1  e2' = e2  efs' = []) 
134
  (|={E,E'}=> WP e2 @ s; E {{ Φ }})  WP e1 @ s; E {{ Φ }}.
135
Proof using Hinh.
136
  intros. rewrite -(wp_lift_pure_det_step_no_fork e1 e2); eauto.
137
  destruct s; by auto.
138
Qed.
139

140
Lemma wp_lift_pure_det_head_step_no_fork' {s E Φ} e1 e2 :
141 142
  to_val e1 = None 
  ( σ1, head_reducible e1 σ1) 
143
  ( σ1 κ e2' σ2 efs',
144
    head_step e1 σ1 κ e2' σ2 efs'  κ = []  σ2 = σ1  e2' = e2  efs' = []) 
145
   WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
146
Proof using Hinh.
147
  intros. rewrite -[(WP e1 @ s; _ {{ _ }})%I]wp_lift_pure_det_head_step_no_fork //.
148 149
  rewrite -step_fupd_intro //.
Qed.
150
End wp.