hoare.v 5.76 KB
Newer Older
1
From iris.program_logic Require Export weakestpre viewshifts.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
From iris.proofmode Require Import weakestpre.
Robbert Krebbers's avatar
Robbert Krebbers committed
3

4
Definition ht {Λ Σ} (E : coPset) (P : iProp Λ Σ)
5
    (e : expr Λ) (Φ : val Λ  iProp Λ Σ) : iProp Λ Σ :=
6
  ( (P  WP e @ E {{ Φ }}))%I.
7
Instance: Params (@ht) 3.
Robbert Krebbers's avatar
Robbert Krebbers committed
8

9
Notation "{{ P } } e @ E {{ Φ } }" := (ht E P e Φ)
10 11 12 13 14
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  {{  Φ  } }") : uPred_scope.
Notation "{{ P } } e {{ Φ } }" := (ht  P e Φ)
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  {{  Φ  } }") : uPred_scope.
15
Notation "{{ P } } e @ E {{ Φ } }" := (True  ht E P e Φ)
16 17
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  @  E  {{  Φ  } }") : C_scope.
18
Notation "{{ P } } e {{ Φ } }" := (True  ht  P e Φ)
19 20
  (at level 20, P, e, Φ at level 200,
   format "{{  P  } }  e  {{  Φ  } }") : C_scope.
Robbert Krebbers's avatar
Robbert Krebbers committed
21

22 23 24 25 26 27 28 29 30 31 32 33 34
Notation "{{ P } } e @ E {{ v , Q } }" := (ht E P e (λ v, Q))
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : uPred_scope.
Notation "{{ P } } e {{ v , Q } }" := (ht  P e (λ v, Q))
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  {{  v ,  Q  } }") : uPred_scope.
Notation "{{ P } } e @ E {{ v , Q } }" := (True  ht E P e (λ v, Q))
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : C_scope.
Notation "{{ P } } e {{ v , Q } }" := (True  ht  P e (λ v, Q))
  (at level 20, P, e, Q at level 200,
   format "{{  P  } }  e  {{  v ,  Q  } }") : C_scope.

Robbert Krebbers's avatar
Robbert Krebbers committed
35
Section hoare.
36
Context {Λ : language} {Σ : iFunctor}.
37 38
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ Ψ : val Λ  iProp Λ Σ.
39
Implicit Types v : val Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
40 41 42
Import uPred.

Global Instance ht_ne E n :
43
  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
Ralf Jung's avatar
Ralf Jung committed
44
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
Global Instance ht_proper E :
46
  Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
Robbert Krebbers's avatar
Robbert Krebbers committed
47
Proof. solve_proper. Qed.
48
Lemma ht_mono E P P' Φ Φ' e :
49
  P  P'  ( v, Φ' v  Φ v)  {{ P' }} e @ E {{ Φ' }}  {{ P }} e @ E {{ Φ }}.
50
Proof. by intros; apply always_mono, impl_mono, wp_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
51
Global Instance ht_mono' E :
52
  Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
Robbert Krebbers's avatar
Robbert Krebbers committed
53
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
54

55
Lemma ht_alt E P Φ e : (P  WP e @ E {{ Φ }})  {{ P }} e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
Proof. iIntros {Hwp} "! HP". by iApply Hwp. Qed.
57

58
Lemma ht_val E v : {{ True : iProp Λ Σ }} of_val v @ E {{ v', v = v' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Proof. iIntros "! _". by iApply wp_value'. Qed.
60

61 62
Lemma ht_vs E P P' Φ Φ' e :
  ((P ={E}=> P')  {{ P' }} e @ E {{ Φ' }}   v, Φ' v ={E}=> Φ v)
63
   {{ P }} e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
65 66 67
  iIntros "(#Hvs&#Hwp&#HΦ) ! HP". iPvs "Hvs" "HP" as "HP".
  iApply wp_pvs; iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
  iIntros {v} "Hv". by iApply "HΦ" "!".
Robbert Krebbers's avatar
Robbert Krebbers committed
68
Qed.
69

70
Lemma ht_atomic E1 E2 P P' Φ Φ' e :
Robbert Krebbers's avatar
Robbert Krebbers committed
71
  E2  E1  atomic e 
72
  ((P ={E1,E2}=> P')  {{ P' }} e @ E2 {{ Φ' }}   v, Φ' v ={E2,E1}=> Φ v)
73
   {{ P }} e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
74
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
75 76 77 78
  iIntros {??} "(#Hvs&#Hwp&#HΦ) ! HP". iApply (wp_atomic _ E2); auto.
  iPvs "Hvs" "HP" as "HP"; first set_solver. iPvsIntro.
  iApply wp_wand_r; iSplitL; [by iApply "Hwp"|].
  iIntros {v} "Hv". by iApply "HΦ" "!".
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Qed.
80

81 82
Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
  ({{ P }} e @ E {{ Φ }}   v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
83
   {{ P }} K e @ E {{ Φ' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
85 86 87
  iIntros "(#Hwpe&#HwpK) ! HP". iApply wp_bind.
  iApply wp_wand_r; iSplitL; [by iApply "Hwpe"|].
  iIntros {v} "Hv". by iApply "HwpK" "!".
Robbert Krebbers's avatar
Robbert Krebbers committed
88
Qed.
89

90
Lemma ht_mask_weaken E1 E2 P Φ e :
91
  E1  E2  {{ P }} e @ E1 {{ Φ }}  {{ P }} e @ E2 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
92 93 94 95
Proof.
  iIntros {?} "#Hwp ! HP". iApply (wp_mask_frame_mono E1 E2); try done.
  by iApply "Hwp".
Qed.
96

97
Lemma ht_frame_l E P Φ R e :
98
  {{ P }} e @ E {{ Φ }}  {{ R  P }} e @ E {{ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
100
  iIntros "#Hwp ! [HR HP]". iApply wp_frame_l; iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
101
Qed.
102

103
Lemma ht_frame_r E P Φ R e :
104
  {{ P }} e @ E {{ Φ }}  {{ P  R }} e @ E {{ v, Φ v  R }}.
105
Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
106

107 108 109 110 111 112 113 114
Lemma ht_frame_step_l E E1 E2 P R1 R2 R3 e Φ :
  to_val e = None  E  E1  E2  E1 
  ((R1 ={E1,E2}=>  R2)  (R2 ={E2,E1}=> R3)  {{ P }} e @ E {{ Φ }})
     {{ R1  P }} e @ (E  E1) {{ λ v, R3  Φ v }}.
Proof.
  iIntros {???} "[#Hvs1 [#Hvs2 #Hwp]] ! [HR HP]".
  iApply (wp_frame_step_l E E1 E2); try done.
  iSplitL "HR".
Ralf Jung's avatar
Ralf Jung committed
115 116 117
  - iPvs "Hvs1" "HR" as "HR"; first by set_solver.
    iPvsIntro. iNext. iPvs "Hvs2" "HR" as "HR"; first by set_solver.
    iPvsIntro. iApply "HR".
118 119 120 121 122 123 124 125
  - iApply "Hwp". done.
Qed.

Lemma ht_frame_step_r E E1 E2 P R1 R2 R3 e Φ :
  to_val e = None  E  E1  E2  E1 
  ((R1 ={E1,E2}=>  R2)  (R2 ={E2,E1}=> R3)  {{ P }} e @ E {{ Φ }})
     {{ R1  P }} e @ (E  E1) {{ λ v, Φ v  R3 }}.
Proof.
Ralf Jung's avatar
Ralf Jung committed
126
  iIntros {???} "[Hvs1 [Hvs2 Hwp]]".
127
  setoid_rewrite (comm _ _ R3).
Ralf Jung's avatar
Ralf Jung committed
128 129
  iApply ht_frame_step_l; try eassumption.
  iSplit; last iSplit; done.
130 131
Qed.

Ralf Jung's avatar
Ralf Jung committed
132
Lemma ht_frame_step_l' E P R e Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
133
  to_val e = None 
134
  {{ P }} e @ E {{ Φ }}  {{  R  P }} e @ E {{ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
  iIntros {?} "#Hwp ! [HR HP]".
Ralf Jung's avatar
Ralf Jung committed
137
  iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
138
Qed.
139

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

Lemma ht_inv N E P Φ R e :
  atomic e  nclose N  E 
150
  (inv N R  {{  R  P }} e @ E  nclose N {{ v,  R  Φ v }})
151 152
     {{ P }} e @ E {{ Φ }}.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
153 154
  iIntros {??} "[#? #Hwp] ! HP". eapply wp_inv; eauto.
  iIntros "HR". iApply "Hwp". by iSplitL "HR".
155
Qed.
156
End hoare.