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

6
Definition ht `{irisG Λ Σ} (s : stuckness) (E : coPset) (P : iProp Σ)
7
    (e : expr Λ) (Φ : val Λ  iProp Σ) : iProp Σ :=
8 9
  ( (P - WP e @ s; E {{ Φ }}))%I.
Instance: Params (@ht) 5.
Robbert Krebbers's avatar
Robbert Krebbers committed
10

11 12
Notation "{{ P } } e @ s ; E {{ Φ } }" := (ht s E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
13
   format "{{  P  } }  e  @  s ;  E  {{  Φ  } }") : stdpp_scope.
14
Notation "{{ P } } e @ E {{ Φ } }" := (ht not_stuck E P%I e%E Φ%I)
15
  (at level 20, P, e, Φ at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
16
   format "{{  P  } }  e  @  E  {{  Φ  } }") : stdpp_scope.
17 18
Notation "{{ P } } e @ E ? {{ Φ } }" := (ht maybe_stuck E P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
19
   format "{{  P  } }  e  @  E  ? {{  Φ  } }") : stdpp_scope.
20
Notation "{{ P } } e {{ Φ } }" := (ht not_stuck  P%I e%E Φ%I)
21
  (at level 20, P, e, Φ at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
22
   format "{{  P  } }  e  {{  Φ  } }") : stdpp_scope.
23 24
Notation "{{ P } } e ? {{ Φ } }" := (ht maybe_stuck  P%I e%E Φ%I)
  (at level 20, P, e, Φ at level 200,
25
   format "{{  P  } }  e  ? {{  Φ  } }") : stdpp_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
26

27 28
Notation "{{ P } } e @ s ; E {{ v , Q } }" := (ht s E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
29
   format "{{  P  } }  e  @  s ;  E  {{  v ,  Q  } }") : stdpp_scope.
30
Notation "{{ P } } e @ E {{ v , Q } }" := (ht not_stuck E P%I e%E (λ v, Q)%I)
31
  (at level 20, P, e, Q at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
32
   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : stdpp_scope.
33 34
Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht maybe_stuck E P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
35
   format "{{  P  } }  e  @  E  ? {{  v ,  Q  } }") : stdpp_scope.
36
Notation "{{ P } } e {{ v , Q } }" := (ht not_stuck  P%I e%E (λ v, Q)%I)
37
  (at level 20, P, e, Q at level 200,
Robbert Krebbers's avatar
Robbert Krebbers committed
38
   format "{{  P  } }  e  {{  v ,  Q  } }") : stdpp_scope.
39 40
Notation "{{ P } } e ? {{ v , Q } }" := (ht maybe_stuck  P%I e%E (λ v, Q)%I)
  (at level 20, P, e, Q at level 200,
41
   format "{{  P  } }  e  ? {{  v ,  Q  } }") : stdpp_scope.
42

Robbert Krebbers's avatar
Robbert Krebbers committed
43
Section hoare.
44
Context `{irisG Λ Σ}.
45
Implicit Types s : stuckness.
46 47
Implicit Types P Q : iProp Σ.
Implicit Types Φ Ψ : val Λ  iProp Σ.
48
Implicit Types v : val Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
49 50
Import uPred.

51 52
Global Instance ht_ne s E n :
  Proper (dist n ==> eq ==> pointwise_relation _ (dist n) ==> dist n) (ht s E).
Ralf Jung's avatar
Ralf Jung committed
53
Proof. solve_proper. Qed.
54 55
Global Instance ht_proper s E :
  Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (ht s E).
Robbert Krebbers's avatar
Robbert Krebbers committed
56
Proof. solve_proper. Qed.
57 58
Lemma ht_mono s E P P' Φ Φ' e :
  (P  P')  ( v, Φ' v  Φ v)  {{ P' }} e @ s; E {{ Φ' }}  {{ P }} e @ s; E {{ Φ }}.
59
Proof. by intros; apply persistently_mono, wand_mono, wp_mono. Qed.
David Swasey's avatar
David Swasey committed
60
Lemma ht_stuck_mono s1 s2 E P Φ e :
61
  s1  s2  {{ P }} e @ s1; E {{ Φ }}  {{ P }} e @ s2; E {{ Φ }}.
David Swasey's avatar
David Swasey committed
62
Proof. by intros; apply persistently_mono, wand_mono, wp_stuck_mono. Qed.
63 64
Global Instance ht_mono' s E :
  Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (ht s E).
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
66

67
Lemma ht_alt s E P Φ e : (P  WP e @ s; E {{ Φ }})  {{ P }} e @ s; E {{ Φ }}.
68
Proof. iIntros (Hwp) "!# HP". by iApply Hwp. Qed.
69

70
Lemma ht_val s E v : {{ True }} of_val v @ s; E {{ v', v = v' }}.
71
Proof. iIntros "!# _". by iApply wp_value'. Qed.
72

73 74 75
Lemma ht_vs s E P P' Φ Φ' e :
  (P ={E}=> P')  {{ P' }} e @ s; E {{ Φ' }}  ( v, Φ' v ={E}=> Φ v)
   {{ P }} e @ s; E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
Proof.
77
  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iMod ("Hvs" with "HP") as "HP".
78
  iApply wp_fupd. iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
79
  iIntros (v) "Hv". by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
80
Qed.
81

Ralf Jung's avatar
Ralf Jung committed
82
Lemma ht_atomic s E1 E2 P P' Φ Φ' e `{!Atomic (stuckness_to_atomicity s) e} :
83 84
  (P ={E1,E2}=> P')  {{ P' }} e @ s; E2 {{ Φ' }}  ( v, Φ' v ={E2,E1}=> Φ v)
   {{ P }} e @ s; E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
85
Proof.
86
  iIntros "(#Hvs & #Hwp & #HΦ) !# HP". iApply (wp_atomic _ _ E2); auto.
87
  iMod ("Hvs" with "HP") as "HP". iModIntro.
88
  iApply (wp_wand with "[HP]"); [by iApply "Hwp"|].
89
  iIntros (v) "Hv". by iApply "HΦ".
Robbert Krebbers's avatar
Robbert Krebbers committed
90
Qed.
91

92 93 94
Lemma ht_bind `{LanguageCtx Λ K} s E P Φ Φ' e :
  {{ P }} e @ s; E {{ Φ }}  ( v, {{ Φ v }} K (of_val v) @ s; E {{ Φ' }})
   {{ P }} K e @ s; E {{ Φ' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
95
Proof.
96
  iIntros "[#Hwpe #HwpK] !# HP". iApply wp_bind.
97
  iApply (wp_wand with "[HP]"); [by iApply "Hwpe"|].
98
  iIntros (v) "Hv". by iApply "HwpK".
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Qed.
100

David Swasey's avatar
David Swasey committed
101
Lemma ht_stuck_weaken s E P Φ e :
102 103
  {{ P }} e @ s; E {{ Φ }}  {{ P }} e @ E ?{{ Φ }}.
Proof.
David Swasey's avatar
David Swasey committed
104
  by iIntros "#Hwp !# ?"; iApply wp_stuck_weaken; iApply "Hwp".
105 106 107 108
Qed.

Lemma ht_mask_weaken s E1 E2 P Φ e :
  E1  E2  {{ P }} e @ s; E1 {{ Φ }}  {{ P }} e @ s; E2 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Proof.
110
  iIntros (?) "#Hwp !# HP". iApply (wp_mask_mono _ E1 E2); try done.
Robbert Krebbers's avatar
Robbert Krebbers committed
111 112
  by iApply "Hwp".
Qed.
113

114 115
Lemma ht_frame_l s E P Φ R e :
  {{ P }} e @ s; E {{ Φ }}  {{ R  P }} e @ s; E {{ v, R  Φ v }}.
116
Proof. iIntros "#Hwp !# [$ HP]". by iApply "Hwp". Qed.
117

118 119
Lemma ht_frame_r s E P Φ R e :
  {{ P }} e @ s; E {{ Φ }}  {{ P  R }} e @ s; E {{ v, Φ v  R }}.
120
Proof. iIntros "#Hwp !# [HP $]". by iApply "Hwp". Qed.
121

122
Lemma ht_frame_step_l s E1 E2 P R1 R2 e Φ :
123
  to_val e = None  E2  E1 
124 125
  (R1 ={E1,E2}=>  |={E2,E1}=> R2)  {{ P }} e @ s; E2 {{ Φ }}
   {{ R1  P }} e @ s; E1 {{ λ v, R2  Φ v }}.
126
Proof.
127
  iIntros (??) "[#Hvs #Hwp] !# [HR HP]".
128
  iApply (wp_frame_step_l _ E1 E2); try done.
129
  iSplitL "HR"; [by iApply "Hvs"|by iApply "Hwp"].
130 131
Qed.

132
Lemma ht_frame_step_r s E1 E2 P R1 R2 e Φ :
133
  to_val e = None  E2  E1 
134 135
  (R1 ={E1,E2}=>  |={E2,E1}=> R2)  {{ P }} e @ s; E2 {{ Φ }}
   {{ P  R1 }} e @ s; E1 {{ λ v, Φ v  R2 }}.
136
Proof.
137
  iIntros (??) "[#Hvs #Hwp] !# [HP HR]".
138
  iApply (wp_frame_step_r _ E1 E2); try done.
139
  iSplitR "HR"; [by iApply "Hwp"|by iApply "Hvs"].
140 141
Qed.

142
Lemma ht_frame_step_l' s E P R e Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
143
  to_val e = None 
144
  {{ P }} e @ s; E {{ Φ }}  {{  R  P }} e @ s; E {{ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
145
Proof.
146
  iIntros (?) "#Hwp !# [HR HP]".
Ralf Jung's avatar
Ralf Jung committed
147
  iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
148
Qed.
149

150
Lemma ht_frame_step_r' s E P Φ R e :
Robbert Krebbers's avatar
Robbert Krebbers committed
151
  to_val e = None 
152
  {{ P }} e @ s; E {{ Φ }}  {{ P   R }} e @ s; E {{ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
153
Proof.
154
  iIntros (?) "#Hwp !# [HP HR]".
Ralf Jung's avatar
Ralf Jung committed
155
  iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
156
Qed.
157
End hoare.