lifting.v 3.44 KB
Newer Older
1
From iris.program_logic Require Export weakestpre.
2
From iris.program_logic Require Import ownership.
3
From iris.algebra Require Export upred_big_op.
4
From iris.proofmode Require Import tactics.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
6

Section lifting.
7
Context `{irisG Λ Σ}.
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
15
16
Lemma wp_lift_step E Φ e1 :
  to_val e1 = None 
  (|={E,}=>  σ1,  reducible e1 σ1   ownP σ1 
17
      e2 σ2 efs,  prim_step e1 σ1 e2 σ2 efs  ownP σ2
18
          ={,E}= WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
19
   WP e1 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
20
Proof.
21
  iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
  iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
23
  iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
24
  iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
25
26
  iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
  iApply "H"; eauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
27
Qed.
28

29
Lemma wp_lift_pure_step E Φ e1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  to_val e1 = None 
31
  ( σ1, reducible e1 σ1) 
32
  ( σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs  σ1 = σ2) 
33
34
  (  e2 efs σ,  prim_step e1 σ e2 σ efs 
    WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
35
   WP e1 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
36
Proof.
37
38
  iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
  iIntros (σ1) "Hσ". iApply pvs_intro'; [set_solver|iIntros "Hclose"].
39
40
  iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
  destruct (Hstep σ1 e2 σ2 efs); auto; subst.
41
  iVs "Hclose"; iVsIntro. iFrame "Hσ". iApply "H"; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
42
Qed.
43
44

(** Derived lifting lemmas. *)
45
Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
46
  atomic e1 
47
  reducible e1 σ1 
48
49
   ownP σ1   ( v2 σ2 efs,  prim_step e1 σ1 (of_val v2) σ2 efs  ownP σ2 -
    (|={E}=> Φ v2)  [ list] ef  efs, WP ef {{ _, True }})
50
   WP e1 @ E {{ Φ }}.
51
Proof.
52
53
54
55
  iIntros (Hatomic ?) "[Hσ H]".
  iApply (wp_lift_step E _ e1); eauto using reducible_not_val.
  iApply pvs_intro'; [set_solver|iIntros "Hclose"].
  iExists σ1. iFrame "Hσ"; iSplit; eauto.
56
57
58
  iNext; iIntros (e2 σ2 efs) "[% Hσ]".
  edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
  iDestruct ("H" $! v2 σ2 efs with "[Hσ]") as "[HΦ $]"; first by eauto.
59
  iVs "Hclose". iVs "HΦ". iApply wp_value; auto using to_of_val.
60
61
Qed.

62
Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 efs :
63
  atomic e1 
64
  reducible e1 σ1 
65
66
  ( e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' 
                   σ2 = σ2'  to_val e2' = Some v2  efs = efs') 
67
68
69
   ownP σ1   (ownP σ2 -
    (|={E}=> Φ v2)  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
70
Proof.
71
  iIntros (?? Hdet) "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ σ1); try done.
72
  iFrame. iNext. iIntros (v2' σ2' efs') "[% Hσ2']".
73
  edestruct Hdet as (->&->%of_to_val%(inj of_val)&->). done. by iApply "Hσ2".
74
75
Qed.

76
Lemma wp_lift_pure_det_step {E Φ} e1 e2 efs :
77
78
  to_val e1 = None 
  ( σ1, reducible e1 σ1) 
79
  ( σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs'  σ1 = σ2  e2 = e2'  efs = efs')
80
81
   (WP e2 @ E {{ Φ }}  [ list] ef  efs, WP ef {{ _, True }})
   WP e1 @ E {{ Φ }}.
82
Proof.
83
  iIntros (?? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
84
  by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
85
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
86
End lifting.