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

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

15
Lemma wp_lift_step s E Φ e1 :
16 17
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E,}=
Ralf Jung's avatar
Ralf Jung committed
18
    if s is NotStuck then reducible e1 σ1 else True 
19
      e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={,E}=
20 21 22 23 24 25 26 27 28
      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.
Qed.

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

37
(** Derived lifting lemmas. *)
38
Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
Ralf Jung's avatar
Ralf Jung committed
39
  ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
40
  ( σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
41
  (|={E,E'}=>  e2 efs σ, prim_step e1 σ e2 σ efs 
42 43
    WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Proof.
45 46 47
  iIntros (Hsafe Hstep) "H". iApply wp_lift_step.
  { specialize (Hsafe inhabitant). destruct s; last done.
      by eapply reducible_not_val. }
Ralf Jung's avatar
Ralf Jung committed
48
  iIntros (σ1) "Hσ". iMod "H".
49 50 51
  iMod fupd_intro_mask' as "Hclose"; last iModIntro; first by set_solver. iSplit.
  { iPureIntro. destruct s; done. }
  iNext. iIntros (e2 σ2 efs ?).
52
  destruct (Hstep σ1 e2 σ2 efs); auto; subst.
Ralf Jung's avatar
Ralf Jung committed
53
  iMod "Hclose" as "_". iFrame "Hσ". iMod "H". iApply "H"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
54
Qed.
55

56
Lemma wp_lift_pure_stuck `{Inhabited (state Λ)} E Φ e :
57
  ( σ, stuck e σ) 
58 59 60 61
  True  WP e @ E ?{{ Φ }}.
Proof.
  iIntros (Hstuck) "_". iApply wp_lift_stuck.
  - destruct(to_val e) as [v|] eqn:He; last done.
62
    rewrite -He. by case: (Hstuck inhabitant).
63 64 65 66
  - iIntros (σ) "_". iMod (fupd_intro_mask' E ) as "_".
    by set_solver. by auto.
Qed.

67 68
(* Atomic steps don't need any mask-changing business here, one can
   use the generic lemmas here. *)
69
Lemma wp_lift_atomic_step {s E Φ} e1 :
70 71
  to_val e1 = None 
  ( σ1, state_interp σ1 ={E}=
Ralf Jung's avatar
Ralf Jung committed
72
    if s is NotStuck then reducible e1 σ1 else True 
73 74
      e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs ={E}=
      state_interp σ2 
75 76
      default False (to_val e2) Φ  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
77
Proof.
78
  iIntros (?) "H". iApply (wp_lift_step s E _ e1)=>//; iIntros (σ1) "Hσ1".
79 80 81 82
  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.
83
  destruct (to_val e2) eqn:?; last by iExFalso.
84
  by iApply wp_value.
85 86
Qed.

87
Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
Ralf Jung's avatar
Ralf Jung committed
88
  ( σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) 
89
  ( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs')
90 91
  (|={E,E'}=> WP e2 @ s; E {{ Φ }}  [ list] ef  efs, WP ef @ s;  {{ _, True }})
   WP e1 @ s; E {{ Φ }}.
92
Proof.
93
  iIntros (? Hpuredet) "H". iApply (wp_lift_pure_step s E E'); try done.
94
  { by intros; eapply Hpuredet. }
95
  iApply (step_fupd_wand with "H"); iIntros "H".
96
  by iIntros (e' efs' σ (_&->&->)%Hpuredet).
97
Qed.
Dan Frumin's avatar
Dan Frumin committed
98

99
Lemma wp_pure_step_fupd `{Inhabited (state Λ)} s E E' e1 e2 φ Φ :
Dan Frumin's avatar
Dan Frumin committed
100 101
  PureExec φ e1 e2 
  φ 
102
  (|={E,E'}=> WP e2 @ s; E {{ Φ }})  WP e1 @ s; E {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
103 104
Proof.
  iIntros ([??] Hφ) "HWP".
105
  iApply (wp_lift_pure_det_step with "[HWP]").
106
  - intros σ. specialize (pure_exec_safe σ). destruct s; eauto using reducible_not_val.
107 108
  - destruct s; naive_solver.
  - by rewrite big_sepL_nil right_id.
Dan Frumin's avatar
Dan Frumin committed
109 110
Qed.

111
Lemma wp_pure_step_later `{Inhabited (state Λ)} s E e1 e2 φ Φ :
Dan Frumin's avatar
Dan Frumin committed
112 113
  PureExec φ e1 e2 
  φ 
114
   WP e2 @ s; E {{ Φ }}  WP e1 @ s; E {{ Φ }}.
Dan Frumin's avatar
Dan Frumin committed
115 116 117
Proof.
  intros ??. rewrite -wp_pure_step_fupd //. rewrite -step_fupd_intro //.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
End lifting.