lifting.v 4.41 KB
Newer Older
1
2
From iris.program_logic Require Export weakestpre.
From iris.program_logic Require Import wsat ownership.
3
From iris.proofmode Require Import pviewshifts.
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Local Hint Extern 10 (_  _) => omega.
Robbert Krebbers's avatar
Robbert Krebbers committed
5
Local Hint Extern 100 (_  _) => set_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
6
Local Hint Extern 10 ({_} _) =>
7
8
9
  repeat match goal with
  | H : wsat _ _ _ _ |- _ => apply wsat_valid in H; last omega
  end; solve_validN.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
11

Section lifting.
12
Context {Λ : language} {Σ : iFunctor}.
13
14
15
Implicit Types v : val Λ.
Implicit Types e : expr Λ.
Implicit Types σ : state Λ.
16
17
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ : val Λ  iProp Λ Σ.
Robbert Krebbers's avatar
Robbert Krebbers committed
18

19
Notation wp_fork ef := (default True ef (flip (wp ) (λ _, True)))%I.
20

Robbert Krebbers's avatar
Robbert Krebbers committed
21
Lemma wp_lift_step E1 E2
22
    (φ : expr Λ  state Λ  option (expr Λ)  Prop) Φ e1 :
Ralf Jung's avatar
Ralf Jung committed
23
  E2  E1  to_val e1 = None 
24
25
26
27
28
  (|={E1,E2}=>  σ1,
       reducible e1 σ1 
       ( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  φ e2 σ2 ef) 
       ownP σ1    e2 σ2 ef,
        ( φ e2 σ2 ef  ownP σ2) ={E2,E1}= WP e2 @ E1 {{ Φ }}  wp_fork ef)
29
   WP e1 @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Proof.
31
32
33
34
  intros ? He. rewrite pvs_eq wp_eq.
  uPred.unseal; split=> n r ? Hvs; constructor; auto. intros k Ef σ1' rf ???.
  destruct (Hvs (S k) Ef σ1' rf) as (r'&(σ1&Hsafe&Hstep&r1&r2&?&?&Hwp)&Hws);
    auto; clear Hvs; cofe_subst r'.
Ralf Jung's avatar
Ralf Jung committed
35
  destruct (wsat_update_pst k (E2  Ef) σ1 σ1' r1 (r2  rf)) as [-> Hws'].
36
  { apply equiv_dist. rewrite -(ownP_spec k); auto. }
37
  { by rewrite assoc. }
Robbert Krebbers's avatar
Robbert Krebbers committed
38
  constructor; [done|intros e2 σ2 ef ?; specialize (Hws' σ2)].
39
  destruct (λ H1 H2 H3, Hwp e2 σ2 ef k (update_pst σ2 r1) H1 H2 H3 k Ef σ2 rf)
Robbert Krebbers's avatar
Robbert Krebbers committed
40
    as (r'&(r1'&r2'&?&?&?)&?); auto; cofe_subst r'.
41
  { split. by eapply Hstep. apply ownP_spec; auto. }
42
  { rewrite (comm _ r2) -assoc; eauto using wsat_le. }
43
  exists r1', r2'; split_and?; try done. by uPred.unseal; intros ? ->.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
Qed.
45

46
Lemma wp_lift_pure_step E (φ : expr Λ  option (expr Λ)  Prop) Φ e1 :
Robbert Krebbers's avatar
Robbert Krebbers committed
47
  to_val e1 = None 
48
  ( σ1, reducible e1 σ1) 
Robbert Krebbers's avatar
Robbert Krebbers committed
49
  ( σ1 e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  σ1 = σ2  φ e2 ef) 
50
  (  e2 ef,  φ e2 ef  WP e2 @ E {{ Φ }}  wp_fork ef)  WP e1 @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Proof.
Ralf Jung's avatar
Ralf Jung committed
52
53
  intros He Hsafe Hstep; rewrite wp_eq; uPred.unseal.
  split=> n r ? Hwp; constructor; auto.
54
  intros k Ef σ1 rf ???; split; [done|]. destruct n as [|n]; first lia.
Robbert Krebbers's avatar
Robbert Krebbers committed
55
  intros e2 σ2 ef ?; destruct (Hstep σ1 e2 σ2 ef); auto; subst.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  destruct (Hwp e2 ef k r) as (r1&r2&Hr&?&?); auto.
57
58
59
  exists r1,r2; split_and?; try done.
  - rewrite -Hr; eauto using wsat_le.
  - uPred.unseal; by intros ? ->.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
Qed.
61
62

(** Derived lifting lemmas. *)
63
Import uPred.
64

65
Lemma wp_lift_atomic_step {E Φ} e1
66
67
    (φ : expr Λ  state Λ  option (expr Λ)  Prop) σ1 :
  atomic e1 
68
  reducible e1 σ1 
69
  ( e2 σ2 ef, prim_step e1 σ1 e2 σ2 ef  φ e2 σ2 ef) 
70
71
   ownP σ1   ( v2 σ2 ef,
     φ (of_val v2) σ2 ef  ownP σ2 - (|={E}=> Φ v2)  wp_fork ef)
72
   WP e1 @ E {{ Φ }}.
73
Proof.
74
75
76
77
78
79
80
  iIntros {???} "[Hσ1 Hwp]". iApply (wp_lift_step E E (λ e2 σ2 ef,
    is_Some (to_val e2)  φ e2 σ2 ef) _ e1); auto using atomic_not_val.
  iApply pvs_intro. iExists σ1. repeat iSplit; eauto using atomic_step.
  iFrame. iNext. iIntros {e2 σ2 ef} "[#He2 Hσ2]".
  iDestruct "He2" as %[[v2 Hv%of_to_val]?]. subst e2.
  iDestruct ("Hwp" $! v2 σ2 ef with "[Hσ2]") as "[HΦ ?]". by eauto.
  iFrame. iPvs "HΦ". iPvsIntro. iApply wp_value; auto using to_of_val.
81
82
Qed.

83
Lemma wp_lift_atomic_det_step {E Φ e1} σ1 v2 σ2 ef :
84
  atomic e1 
85
  reducible e1 σ1 
86
87
  ( e2' σ2' ef', prim_step e1 σ1 e2' σ2' ef' 
    σ2 = σ2'  to_val e2' = Some v2  ef = ef') 
88
   ownP σ1   (ownP σ2 - (|={E}=> Φ v2)  wp_fork ef)  WP e1 @ E {{ Φ }}.
89
Proof.
90
91
92
93
  iIntros {???} "[Hσ1 Hσ2]". iApply (wp_lift_atomic_step _ (λ e2' σ2' ef',
    σ2 = σ2'  to_val e2' = Some v2  ef = ef') σ1); try done. iFrame. iNext.
  iIntros {v2' σ2' ef'} "[#Hφ Hσ2']". rewrite to_of_val.
  iDestruct "Hφ" as %(->&[= ->]&->). by iApply "Hσ2".
94
95
Qed.

96
Lemma wp_lift_pure_det_step {E Φ} e1 e2 ef :
97
98
  to_val e1 = None 
  ( σ1, reducible e1 σ1) 
99
  ( σ1 e2' σ2 ef', prim_step e1 σ1 e2' σ2 ef'  σ1 = σ2  e2 = e2'  ef = ef')
100
   (WP e2 @ E {{ Φ }}  wp_fork ef)  WP e1 @ E {{ Φ }}.
101
Proof.
102
103
104
  iIntros {???} "?".
  iApply (wp_lift_pure_step E (λ e2' ef', e2 = e2'  ef = ef')); try done.
  iNext. by iIntros {e' ef' [-> ->] }.
105
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
End lifting.