hoare.v 4.23 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

Section hoare.
23
Context {Λ : language} {Σ : iFunctor}.
24 25
Implicit Types P Q : iProp Λ Σ.
Implicit Types Φ Ψ : val Λ  iProp Λ Σ.
26
Implicit Types v : val Λ.
Robbert Krebbers's avatar
Robbert Krebbers committed
27 28 29
Import uPred.

Global Instance ht_ne E n :
30
  Proper (dist n ==> eq==>pointwise_relation _ (dist n) ==> dist n) (@ht Λ Σ E).
Ralf Jung's avatar
Ralf Jung committed
31
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Global Instance ht_proper E :
33
  Proper (() ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
Robbert Krebbers's avatar
Robbert Krebbers committed
34
Proof. solve_proper. Qed.
35
Lemma ht_mono E P P' Φ Φ' e :
36
  P  P'  ( v, Φ' v  Φ v)  {{ P' }} e @ E {{ Φ' }}  {{ P }} e @ E {{ Φ }}.
37
Proof. by intros; apply always_mono, impl_mono, wp_mono. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
38
Global Instance ht_mono' E :
39
  Proper (flip () ==> eq ==> pointwise_relation _ () ==> ()) (@ht Λ Σ E).
Robbert Krebbers's avatar
Robbert Krebbers committed
40
Proof. solve_proper. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
41

42
Lemma ht_alt E P Φ e : (P  WP e @ E {{ Φ }})  {{ P }} e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
43
Proof. iIntros {Hwp} "! HP". by iApply Hwp. Qed.
44 45 46

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

49 50
Lemma ht_vs E P P' Φ Φ' e :
  ((P ={E}=> P')  {{ P' }} e @ E {{ Φ' }}   v, Φ' v ={E}=> Φ v)
51
   {{ P }} e @ E {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
53 54 55
  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
56
Qed.
57

58
Lemma ht_atomic E1 E2 P P' Φ Φ' e :
Robbert Krebbers's avatar
Robbert Krebbers committed
59
  E2  E1  atomic e 
60
  ((P ={E1,E2}=> P')  {{ P' }} e @ E2 {{ Φ' }}   v, Φ' v ={E2,E1}=> Φ v)
61
   {{ P }} e @ E1 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
63 64 65 66
  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
67
Qed.
68

69 70
Lemma ht_bind `{LanguageCtx Λ K} E P Φ Φ' e :
  ({{ P }} e @ E {{ Φ }}   v, {{ Φ v }} K (of_val v) @ E {{ Φ' }})
71
   {{ P }} K e @ E {{ Φ' }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
73 74 75
  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
76
Qed.
77

78
Lemma ht_mask_weaken E1 E2 P Φ e :
79
  E1  E2  {{ P }} e @ E1 {{ Φ }}  {{ P }} e @ E2 {{ Φ }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
80 81 82 83
Proof.
  iIntros {?} "#Hwp ! HP". iApply (wp_mask_frame_mono E1 E2); try done.
  by iApply "Hwp".
Qed.
84

85
Lemma ht_frame_l E P Φ R e :
86
  {{ P }} e @ E {{ Φ }}  {{ R  P }} e @ E {{ λ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
88
  iIntros "#Hwp ! [HR HP]". iApply wp_frame_l; iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
89
Qed.
90

91
Lemma ht_frame_r E P Φ R e :
92
  {{ P }} e @ E {{ Φ }}  {{ P  R }} e @ E {{ λ v, Φ v  R }}.
93
Proof. setoid_rewrite (comm _ _ R); apply ht_frame_l. Qed.
94

Ralf Jung's avatar
Ralf Jung committed
95
Lemma ht_frame_step_l' E P R e Φ :
Robbert Krebbers's avatar
Robbert Krebbers committed
96
  to_val e = None 
97
  {{ P }} e @ E {{ Φ }}  {{  R  P }} e @ E {{ λ v, R  Φ v }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
  iIntros {?} "#Hwp ! [HR HP]".
Ralf Jung's avatar
Ralf Jung committed
100
  iApply wp_frame_step_l'; try done. iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
101
Qed.
102

Ralf Jung's avatar
Ralf Jung committed
103
Lemma ht_frame_step_r' E P Φ R e :
Robbert Krebbers's avatar
Robbert Krebbers committed
104
  to_val e = None 
105
  {{ P }} e @ E {{ Φ }}  {{ P   R }} e @ E {{ λ v, Φ v  R }}.
Robbert Krebbers's avatar
Robbert Krebbers committed
106
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
  iIntros {?} "#Hwp ! [HP HR]".
Ralf Jung's avatar
Ralf Jung committed
108
  iApply wp_frame_step_r'; try done. iFrame "HR". by iApply "Hwp".
Robbert Krebbers's avatar
Robbert Krebbers committed
109
Qed.
110 111 112 113 114 115

Lemma ht_inv N E P Φ R e :
  atomic e  nclose N  E 
  (inv N R  {{  R  P }} e @ E  nclose N {{ λ v,  R  Φ v }})
     {{ P }} e @ E {{ Φ }}.
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
116 117
  iIntros {??} "[#? #Hwp] ! HP". eapply wp_inv; eauto.
  iIntros "HR". iApply "Hwp". by iSplitL "HR".
118
Qed.
119
End hoare.