1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7(*
8Hoare reasoning and WP (weakest-precondition) generator rules for the option monad.
9
10This list is almost certainly incomplete; add rules here as they are needed.
11*)
12
13theory OptionMonadWP
14imports
15  OptionMonadND
16  WP
17begin
18
19declare K_def [simp]
20
21(* Hoare triples.
22   TODO: design a sensible syntax for them. *)
23
24(* Partial correctness. *)
25definition ovalid :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" where
26  "ovalid P f Q \<equiv> \<forall>s r. P s \<and> f s = Some r \<longrightarrow> Q r s"
27(* Total correctness. *)
28definition ovalidNF :: "('s \<Rightarrow> bool) \<Rightarrow> ('s \<Rightarrow> 'a option) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> bool" where
29  "ovalidNF P f Q \<equiv> \<forall>s. P s \<longrightarrow> (f s \<noteq> None \<and> (\<forall>r. f s = Some r \<longrightarrow> Q r s))"
30(* Termination. *)
31definition no_ofail where "no_ofail P f \<equiv> \<forall>s. P s \<longrightarrow> f s \<noteq> None"
32
33(*
34This rule lets us apply ovalidNF machinery for proving no_ofail.
35However, we ought to eventually write working wp rules for no_ofail (see below).
36*)
37lemma no_ofail_is_ovalidNF: "no_ofail P f \<equiv> ovalidNF P f (\<lambda>_ _. True)"
38  by (simp add: no_ofail_def ovalidNF_def)
39lemma ovalidNF_combine: "\<lbrakk> ovalid P f Q; no_ofail P f \<rbrakk> \<Longrightarrow> ovalidNF P f Q"
40  by (auto simp: ovalidNF_def ovalid_def no_ofail_def)
41
42
43(* Annotating programs with loop invariant and measure. *)
44definition owhile_inv ::
45  "('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> 'a option) \<Rightarrow> 'a
46   \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 's \<Rightarrow> nat) \<Rightarrow> 's \<Rightarrow> 'a option"
47  where "owhile_inv C B x I M = owhile C B x"
48
49lemmas owhile_add_inv = owhile_inv_def[symmetric]
50
51
52(* WP rules for ovalid. *)
53lemma obind_wp [wp]:
54  "\<lbrakk> \<And>r. ovalid (R r) (g r) Q; ovalid P f R \<rbrakk> \<Longrightarrow> ovalid P (obind f g) Q"
55  by (simp add: ovalid_def obind_def split: option.splits, fast)
56
57lemma oreturn_wp [wp]:
58  "ovalid (P x) (oreturn x) P"
59  by (simp add: ovalid_def)
60
61lemma ocondition_wp [wp]:
62  "\<lbrakk> ovalid L l Q; ovalid R r Q \<rbrakk>
63   \<Longrightarrow> ovalid (\<lambda>s. if C s then L s else R s) (ocondition C l r) Q"
64  by (auto simp: ovalid_def ocondition_def)
65
66lemma ofail_wp [wp]:
67  "ovalid (\<lambda>_. True) ofail Q"
68  by (simp add: ovalid_def ofail_def)
69
70lemma ovalid_K_bind_wp [wp]:
71  "ovalid P f Q \<Longrightarrow> ovalid P (K_bind f x) Q"
72  by simp
73
74lemma ogets_wp [wp]: "ovalid (\<lambda>s. P (f s) s) (ogets f) P"
75  by (simp add: ovalid_def ogets_def)
76
77lemma oguard_wp [wp]: "ovalid (\<lambda>s. f s \<longrightarrow> P () s) (oguard f) P"
78  by (simp add: ovalid_def oguard_def)
79
80lemma oskip_wp [wp]:
81  "ovalid (\<lambda>s. P () s) oskip P"
82  by (simp add: ovalid_def oskip_def)
83
84lemma ovalid_case_prod [wp]:
85  assumes "(\<And>x y. ovalid (P x y) (B x y) Q)"
86  shows "ovalid (case v of (x, y) \<Rightarrow> P x y) (case v of (x, y) \<Rightarrow> B x y) Q"
87  using assms unfolding ovalid_def by auto
88
89lemma owhile_ovalid [wp]:
90"\<lbrakk>\<And>a. ovalid (\<lambda>s. I a s \<and> C a s) (B a) I;
91   \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s\<rbrakk>
92  \<Longrightarrow> ovalid (I a) (owhile_inv C B a I M) Q"
93  unfolding owhile_inv_def owhile_def ovalid_def
94  apply clarify
95  apply (frule_tac I = "\<lambda>a. I a s" in option_while_rule)
96  apply auto
97  done
98
99definition ovalid_property where "ovalid_property P x = (\<lambda>s f. (\<forall>r. Some r = x s f \<longrightarrow> P r s))"
100lemma ovalid_is_triple [wp_trip]:
101  "ovalid P f Q = triple_judgement P f (ovalid_property Q (\<lambda>s f. f s))"
102  by (auto simp: triple_judgement_def ovalid_def ovalid_property_def)
103
104
105lemma ovalid_wp_comb1 [wp_comb]:
106  "\<lbrakk> ovalid P' f Q; ovalid P f Q'; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> ovalid P f (\<lambda>r s. Q r s \<and> Q' r s)"
107  by (simp add: ovalid_def)
108
109lemma ovalid_wp_comb2 [wp_comb]:
110  "\<lbrakk> ovalid P f Q; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> ovalid P' f Q"
111  by (auto simp: ovalid_def)
112
113lemma ovalid_wp_comb3 [wp_comb]:
114  "\<lbrakk> ovalid P f Q; ovalid P' f Q' \<rbrakk> \<Longrightarrow> ovalid (\<lambda>s. P s \<and> P' s) f (\<lambda>r s. Q r s \<and> Q' r s)"
115  by (auto simp: ovalid_def)
116
117
118
119(* WP rules for ovalidNF. *)
120lemma obind_NF_wp [wp]:
121  "\<lbrakk> \<And>r. ovalidNF (R r) (g r) Q; ovalidNF P f R \<rbrakk> \<Longrightarrow> ovalidNF P (obind f g) Q"
122  by (auto simp: ovalidNF_def obind_def split: option.splits)
123
124lemma oreturn_NF_wp [wp]:
125  "ovalidNF (P x) (oreturn x) P"
126  by (simp add: ovalidNF_def oreturn_def)
127
128lemma ocondition_NF_wp [wp]:
129  "\<lbrakk> ovalidNF L l Q; ovalidNF R r Q \<rbrakk>
130   \<Longrightarrow> ovalidNF (\<lambda>s. if C s then L s else R s) (ocondition C l r) Q"
131  by (simp add: ovalidNF_def ocondition_def)
132
133lemma ofail_NF_wp [wp]:
134  "ovalidNF (\<lambda>_. False) ofail Q"
135  by (simp add: ovalidNF_def ofail_def)
136
137lemma ovalidNF_K_bind_wp [wp]:
138  "ovalidNF P f Q \<Longrightarrow> ovalidNF P (K_bind f x) Q"
139  by simp
140
141lemma ogets_NF_wp [wp]:
142  "ovalidNF (\<lambda>s. P (f s) s) (ogets f) P"
143  by (simp add: ovalidNF_def ogets_def)
144
145lemma oguard_NF_wp [wp]:
146  "ovalidNF (\<lambda>s. f s \<and> P () s) (oguard f) P"
147  by (simp add: ovalidNF_def oguard_def)
148
149lemma oskip_NF_wp [wp]:
150  "ovalidNF (\<lambda>s. P () s) oskip P"
151  by (simp add: ovalidNF_def oskip_def)
152
153lemma ovalid_NF_case_prod [wp]:
154  assumes "(\<And>x y. ovalidNF (P x y) (B x y) Q)"
155  shows "ovalidNF (case v of (x, y) \<Rightarrow> P x y) (case v of (x, y) \<Rightarrow> B x y) Q"
156  using assms unfolding ovalidNF_def by auto
157
158lemma owhile_NF [wp]:
159"\<lbrakk>\<And>a. ovalidNF (\<lambda>s. I a s \<and> C a s) (B a) I;
160   \<And>a m. ovalid (\<lambda>s. I a s \<and> C a s \<and> M a s = m) (B a) (\<lambda>r s. M r s < m);
161   \<And>a s. \<lbrakk>I a s; \<not> C a s\<rbrakk> \<Longrightarrow> Q a s\<rbrakk>
162  \<Longrightarrow> ovalidNF (I a) (owhile_inv C B a I M) Q"
163  unfolding owhile_inv_def ovalidNF_def ovalid_def
164  apply clarify
165  apply (rule_tac I = I and M = "measure (\<lambda>r. M r s)" in owhile_rule)
166       apply fastforce
167      apply fastforce
168     apply fastforce
169    apply blast+
170  done
171
172definition ovalidNF_property where "ovalidNF_property P x = (\<lambda>s f. (x s f \<noteq> None \<and> (\<forall>r. Some r = x s f \<longrightarrow> P r s)))"
173lemma ovalidNF_is_triple [wp_trip]:
174  "ovalidNF P f Q = triple_judgement P f (ovalidNF_property Q (\<lambda>s f. f s))"
175  by (auto simp: triple_judgement_def ovalidNF_def ovalidNF_property_def)
176
177
178lemma ovalidNF_wp_comb1 [wp_comb]:
179  "\<lbrakk> ovalidNF P' f Q; ovalidNF P f Q'; \<And>s. P s \<Longrightarrow> P' s \<rbrakk> \<Longrightarrow> ovalidNF P f (\<lambda>r s. Q r s \<and> Q' r s)"
180  by (simp add: ovalidNF_def)
181
182lemma ovalidNF_wp_comb2 [wp_comb]:
183  "\<lbrakk> ovalidNF P f Q; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> ovalidNF P' f Q"
184  by (simp add: ovalidNF_def)
185
186lemma ovalidNF_wp_comb3 [wp_comb]:
187  "\<lbrakk> ovalidNF P f Q; ovalidNF P' f Q' \<rbrakk> \<Longrightarrow> ovalidNF (\<lambda>s. P s \<and> P' s) f (\<lambda>r s. Q r s \<and> Q' r s)"
188  by (simp add: ovalidNF_def)
189
190
191
192(* FIXME: WP rules for no_ofail, which might not be correct. *)
193lemma no_ofail_ofail [wp]: "no_ofail (\<lambda>_. False) ofail"
194  by (simp add: no_ofail_def ofail_def)
195
196lemma no_ofail_ogets [wp]: "no_ofail (\<lambda>_. True) (ogets f)"
197  by (simp add: no_ofail_def ogets_def)
198
199lemma no_ofail_obind [wp]:
200  "\<lbrakk> \<And>r. no_ofail (P r) (g r); no_ofail Q f; ovalid Q f P \<rbrakk> \<Longrightarrow> no_ofail Q (obind f g)"
201  by (auto simp: no_ofail_def obind_def ovalid_def)
202
203lemma no_ofail_K_bind [wp]:
204  "no_ofail P f \<Longrightarrow> no_ofail P (K_bind f x)"
205  by simp
206
207lemma no_ofail_oguard [wp]:
208  "no_ofail (\<lambda>s. f s) (oguard f)"
209  by (auto simp: no_ofail_def oguard_def)
210
211lemma no_ofail_ocondition [wp]:
212  "\<lbrakk> no_ofail L l; no_ofail R r \<rbrakk>
213     \<Longrightarrow> no_ofail (\<lambda>s. if C s then L s else R s) (ocondition C l r)"
214  by (simp add: no_ofail_def ocondition_def)
215
216lemma no_ofail_oreturn [wp]:
217  "no_ofail (\<lambda>_. True) (oreturn x)"
218  by (simp add: no_ofail_def oreturn_def)
219
220lemma no_ofail_oskip [wp]:
221  "no_ofail (\<lambda>_. True) oskip"
222  by (simp add: no_ofail_def oskip_def)
223
224lemma no_ofail_is_triple [wp_trip]:
225  "no_ofail P f = triple_judgement P f (\<lambda>s f. f s \<noteq> None)"
226  by (auto simp: triple_judgement_def no_ofail_def)
227
228lemma no_ofail_wp_comb1 [wp_comb]:
229  "\<lbrakk> no_ofail P f; \<And>s. P' s \<Longrightarrow> P s \<rbrakk> \<Longrightarrow> no_ofail P' f"
230  by (simp add: no_ofail_def)
231
232lemma no_ofail_wp_comb2 [wp_comb]:
233  "\<lbrakk> no_ofail P f; no_ofail P' f \<rbrakk> \<Longrightarrow> no_ofail (\<lambda>s. P s \<and> P' s) f"
234  by (simp add: no_ofail_def)
235
236
237
238(* Some extra lemmas for our predicates. *)
239lemma ovalid_grab_asm:
240  "(G \<Longrightarrow> ovalid P f Q) \<Longrightarrow> ovalid (\<lambda>s. G \<and> P s) f Q"
241  by (simp add: ovalid_def)
242lemma ovalidNF_grab_asm:
243  "(G \<Longrightarrow> ovalidNF P f Q) \<Longrightarrow> ovalidNF (\<lambda>s. G \<and> P s) f Q"
244  by (simp add: ovalidNF_def)
245lemma no_ofail_grab_asm:
246  "(G \<Longrightarrow> no_ofail P f) \<Longrightarrow> no_ofail (\<lambda>s. G \<and> P s) f"
247  by (simp add: no_ofail_def)
248
249lemma ovalid_assume_pre:
250  "(\<And>s. P s \<Longrightarrow> ovalid P f Q) \<Longrightarrow> ovalid P f Q"
251  by (auto simp: ovalid_def)
252lemma ovalidNF_assume_pre:
253  "(\<And>s. P s \<Longrightarrow> ovalidNF P f Q) \<Longrightarrow> ovalidNF P f Q"
254  by (simp add: ovalidNF_def)
255lemma no_ofail_assume_pre:
256  "(\<And>s. P s \<Longrightarrow> no_ofail P f) \<Longrightarrow> no_ofail P f"
257  by (simp add: no_ofail_def)
258
259lemma ovalid_pre_imp:
260  "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; ovalid P f Q \<rbrakk> \<Longrightarrow> ovalid P' f Q"
261  by (simp add: ovalid_def)
262lemma ovalidNF_pre_imp:
263  "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P' f Q"
264  by (simp add: ovalidNF_def)
265lemma no_ofail_pre_imp:
266  "\<lbrakk> \<And>s. P' s \<Longrightarrow> P s; no_ofail P f \<rbrakk> \<Longrightarrow> no_ofail P' f"
267  by (simp add: no_ofail_def)
268
269lemma ovalid_post_imp:
270  "\<lbrakk> \<And>r s. Q r s \<Longrightarrow> Q' r s; ovalid P f Q \<rbrakk> \<Longrightarrow> ovalid P f Q'"
271  by (simp add: ovalid_def)
272lemma ovalidNF_post_imp:
273  "\<lbrakk> \<And>r s. Q r s \<Longrightarrow> Q' r s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P f Q'"
274  by (simp add: ovalidNF_def)
275
276lemma ovalid_post_imp_assuming_pre:
277  "\<lbrakk> \<And>r s. \<lbrakk> P s; Q r s \<rbrakk> \<Longrightarrow> Q' r s; ovalid P f Q \<rbrakk> \<Longrightarrow> ovalid P f Q'"
278  by (simp add: ovalid_def)
279lemma ovalidNF_post_imp_assuming_pre:
280  "\<lbrakk> \<And>r s. \<lbrakk> P s; Q r s \<rbrakk> \<Longrightarrow> Q' r s; ovalidNF P f Q \<rbrakk> \<Longrightarrow> ovalidNF P f Q'"
281  by (simp add: ovalidNF_def)
282
283end
284