1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7theory Memcpy
8imports
9  "CParser.CTranslation"
10  "AutoCorres.AutoCorres"
11begin
12
13abbreviation "ADDR_MAX \<equiv> UWORD_MAX TYPE(addr_bitsize)"
14
15(* Helper for noticing when you accidentally haven't constrained an of_nat *)
16abbreviation "of_nat_addr \<equiv> of_nat::(nat \<Rightarrow> addr)"
17
18lemma byte_ptr_guarded:
19    "ptr_val (x::8 word ptr) \<noteq> 0 \<Longrightarrow> c_guard x"
20  unfolding c_guard_def c_null_guard_def ptr_aligned_def
21  by (clarsimp simp: intvl_Suc)
22
23(* FIXME: MOVE *)
24lemma ptr_add_coerce: "ptr_val (((ptr_coerce x)::('a::{c_type}) ptr) +\<^sub>p a) = (ptr_val x) + (of_int a * of_nat (size_of TYPE('a)))"
25  apply (case_tac x)
26  apply (clarsimp simp: CTypesDefs.ptr_add_def)
27  done
28
29(* FIXME: MOVE *)
30(* Casting a valid pointer to char* and incrementing it by a value less than
31 * the size of the underlying type does not give us NULL.
32 *)
33lemma ptr_contained:"\<lbrakk> c_guard (x::('a::c_type) ptr); size_of TYPE('a) = sz;
34                       0 \<le> i; i < int sz; (y::8 word ptr) = ptr_coerce x\<rbrakk> \<Longrightarrow> c_guard (y +\<^sub>p i)"
35  apply (rule byte_ptr_guarded)
36  unfolding c_guard_def c_null_guard_def ptr_add_def
37  apply simp
38  apply (clarsimp simp: CTypesDefs.ptr_add_def intvl_def)
39  apply (erule allE [where x="nat i"])
40  apply (clarsimp simp: nat_less_iff of_nat_nat)
41  done
42
43external_file "memcpy.c"
44install_C_file "memcpy.c"
45
46(* FIXME: MOVE *)
47lemma squash_auxupd_id[polish]:
48  "modify (t_hrs_'_update (hrs_htd_update id)) = skip"
49  by (monad_eq simp: skip_def id_def hrs_htd_update_def)
50
51autocorres [no_heap_abs=memcpy memcpy_int] "memcpy.c"
52
53(* Dereference a pointer *)
54abbreviation "deref s x \<equiv> h_val (hrs_mem (t_hrs_' s)) x"
55
56(* char* cast *)
57abbreviation "byte_cast x \<equiv> ((ptr_coerce x)::8 word ptr)"
58
59context memcpy begin
60
61lemma memcpy_char:
62  "\<lbrace> \<lambda>s. c_guard (x::8 word ptr) \<and>
63         c_guard (y::8 word ptr) \<and>
64         unat sz = size_of TYPE(8 word) \<and>
65         P (deref s x) \<and>
66         x \<noteq> y\<rbrace>
67      memcpy' (ptr_coerce y) (ptr_coerce x) sz
68   \<lbrace>\<lambda> _ s. P (deref s y) \<rbrace>!"
69  (* Evaluate sz *)
70  apply clarsimp
71
72  unfolding memcpy'_def
73  apply (clarsimp simp:skip_def)
74  apply wp
75
76  (* Unroll the loop twice *)
77  apply (subst whileLoop_unroll, wp)
78     apply (subst whileLoop_unroll, wp)
79
80  (* The remaining loop is never encountered *)
81       apply (rule validNF_false_pre)
82      apply wp+
83
84  (* Finally we're left with the single assignment *)
85  apply (clarsimp simp:hrs_mem_update h_val_heap_update)
86  apply unat_arith
87 done
88
89lemma of_nat_prop_exp: "n < 32 \<Longrightarrow> of_nat (2 ^ n) = 2 ^ (of_nat n)"
90  by clarsimp
91
92lemma memcpy_word:
93  "\<lbrace> \<lambda>s. c_guard (x::32 word ptr) \<and>
94         c_guard (y::32 word ptr) \<and>
95         unat sz = size_of TYPE(32 word) \<and>
96         P (deref s x) \<and>
97         x \<noteq> y \<rbrace>
98      memcpy' (ptr_coerce y) (ptr_coerce x) sz
99   \<lbrace> \<lambda>_ s. P (deref s y) \<rbrace>!"
100  apply clarsimp
101  unfolding memcpy'_def apply (clarsimp simp:skip_def)
102  apply (rule validNF_assume_pre)
103  apply (subgoal_tac "{ptr_val x ..+ unat sz} \<inter> {ptr_val y ..+ unat sz} = {}")
104   apply (subst whileLoop_add_inv [where
105     I="\<lambda>i s.  unat i \<le> unat sz \<and>
106                (\<forall>a < i. deref s (byte_cast x +\<^sub>p uint a) = deref s (byte_cast y +\<^sub>p uint a)) \<and>
107                P (deref s x)" and
108     M="\<lambda>(i, s). unat sz - unat i"])
109   apply (wp validNF_whileLoop_inv_measure_twosteps)
110      apply clarsimp
111      apply (rule conjI, unat_arith)
112      apply (rule conjI, clarsimp)
113       apply (case_tac "a = i")
114        apply (clarsimp)
115        apply (erule_tac x=i in allE)
116        apply (clarsimp simp:hrs_mem_update h_val_heap_update)
117        apply (subst h_val_heap_same)
118            apply (rule ptr_retyp_h_t_valid)
119            apply simp
120           apply (rule ptr_retyp_disjoint)
121            apply (rule ptr_retyp_h_t_valid)
122            apply simp
123           apply (clarsimp simp:ptr_add_def intvl_def CTypesDefs.ptr_add_def)
124          apply simp
125         apply (clarsimp simp: CTypesDefs.ptr_add_def field_of_t_simple)
126         apply (drule field_of_t_simple)
127         apply clarsimp
128        apply simp
129       apply (subgoal_tac "a < i")
130        apply (clarsimp simp:hrs_mem_update)
131        apply (subst h_val_heap_update_disjoint)
132
133         (* The current goal should be obvious to unat_arith, but for some reason isn't *)
134         apply (clarsimp simp:ptr_add_def intvl_def disjoint_iff_not_equal)
135         apply (erule_tac x="ptr_val x + a" in allE, clarsimp)
136         apply (erule impE)
137          apply (rule_tac x="unat a" in exI, clarsimp)
138          apply unat_arith
139
140         apply (erule_tac x="ptr_val y + i" and
141                          P="\<lambda>ya. (\<exists>k. ya = ptr_val y + of_nat k \<and> k < 4) \<longrightarrow> ptr_val y + i \<noteq> ya" in allE, clarsimp)
142         apply (erule_tac x="unat i" in allE, clarsimp)
143          apply unat_arith
144         apply (clarsimp simp:CTypesDefs.ptr_add_def)
145        apply (subst h_val_heap_update_disjoint)
146         (* Similar goal to the previous irritation, but this time Isabelle decides to play ball *)
147         apply (clarsimp simp:ptr_add_def intvl_def ptr_val_def disjoint_iff_not_equal)
148        apply (clarsimp simp:CTypesDefs.ptr_add_def)
149       apply (clarsimp simp:CTypesDefs.ptr_add_def)
150      apply unat_arith
151
152      apply (rule conjI)
153       apply (subst hrs_mem_update)+
154       apply (subst h_val_heap_update_disjoint)
155        apply (clarsimp simp: disjoint_iff_not_equal)
156        apply (clarsimp simp:CTypesDefs.ptr_add_def intvl_def)
157        apply (erule_tac x="ptr_val x + of_nat k" in allE)
158        apply (erule impE)
159         apply (rule_tac x="k" in exI)
160         apply simp
161        apply (erule_tac x="ptr_val y + i" and
162                         P="\<lambda>ya. (\<exists>k. ya = ptr_val y + of_nat k \<and> k < 4) \<longrightarrow> ptr_val x + of_nat k \<noteq> ya" in allE)
163        apply (erule impE)
164         apply (rule_tac x="unat i" in exI)
165         apply simp
166         apply unat_arith
167        apply simp
168       apply simp
169
170      (* Yet more tedium that unat_arith doesn't like *)
171      apply (rule conjI)
172       apply (rule byte_ptr_guarded,
173              clarsimp simp:CTypesDefs.ptr_add_def c_guard_def c_null_guard_def intvl_def,
174              (erule_tac x="unat i" in allE)+,
175              clarsimp,
176              unat_arith)+
177
178     apply wp
179     apply unat_arith
180    apply clarsimp
181    apply (subgoal_tac "deref sa x = deref sa y")
182     apply clarsimp
183    apply (clarsimp simp: h_val_def)[1]
184    apply (rule arg_cong[where f=from_bytes])
185    apply (subst numeral_eqs(3))+
186    apply simp
187    apply (rule_tac x=0 in allE, assumption, erule impE, unat_arith)
188    apply (rule_tac x=1 in allE, assumption, erule impE, unat_arith)
189    apply (rule_tac x=2 in allE, assumption, erule impE, unat_arith)
190    apply (rule_tac x=3 in allE, assumption, erule impE, unat_arith)
191    apply (simp add:CTypesDefs.ptr_add_def)
192    apply (simp add: add.commute from_bytes_eq)
193   apply clarsimp
194  apply (clarsimp simp:intvl_def disjoint_iff_not_equal)
195  apply (drule_tac x=x and y=y and j="of_nat k" and i="of_nat ka" and n=2 in neq_imp_bytes_disjoint)
196        apply assumption
197       apply (case_tac "k = 0", clarsimp) (* insert "k > 0" *)
198       apply (clarsimp simp:unat_of_nat_len)
199      apply (case_tac "ka = 0", clarsimp)
200      apply (clarsimp simp:unat_of_nat_len)
201     apply assumption
202    apply clarsimp+
203  done
204
205text \<open>The bytes at the pointer @{term p} are @{term bs}.\<close>
206definition
207  bytes_at :: "'a globals_scheme \<Rightarrow> 'b::c_type ptr \<Rightarrow> word8 list \<Rightarrow> bool"
208where
209  "bytes_at s p bs \<equiv> length bs = 0 \<or>
210                      (length bs \<le> ADDR_MAX \<and> (\<forall>i \<in> {0..(length bs - 1)}. deref s (byte_cast p +\<^sub>p (of_nat i)) = bs ! i))"
211
212lemma bytes_at_none[simp]: "bytes_at s p []"
213  by (clarsimp simp:bytes_at_def)
214
215text \<open>The bytes of typed pointer @{term p} are @{term bs}.\<close>
216definition
217  bytes_of :: "'a globals_scheme \<Rightarrow> 'b::c_type ptr \<Rightarrow> word8 list \<Rightarrow> bool"
218where
219  "bytes_of s p bs \<equiv> length bs = size_of TYPE('b) \<and> bytes_at s p bs"
220
221text \<open>The bytes at a char pointer are just it dereferenced.\<close>
222lemma bytes_of_char[simp]: "bytes_of s (p::8word ptr) bs = (length bs = 1 \<and> deref s p = hd bs)"
223  apply (clarsimp simp:bytes_of_def bytes_at_def)
224  apply (rule iffI)
225   apply clarsimp
226   apply (erule disjE)
227    apply clarsimp+
228   apply (rule hd_conv_nth[symmetric])
229   apply clarsimp+
230  apply (subgoal_tac "hd bs = bs ! 0")
231   apply simp
232  apply (rule hd_conv_nth)
233  apply clarsimp
234  done
235
236text \<open>A pointer does not wrap around memory.\<close>
237definition
238  no_wrap :: "'a::c_type ptr \<Rightarrow> nat \<Rightarrow> bool"
239where
240  "no_wrap p sz \<equiv> 0 \<notin> {ptr_val p ..+ sz}"
241
242text \<open>Two pointers do not overlap.\<close>
243definition
244  no_overlap :: "'a::c_type ptr \<Rightarrow> 'b::c_type ptr \<Rightarrow> nat \<Rightarrow> bool"
245where
246  "no_overlap p q sz \<equiv> {ptr_val p ..+ sz} \<inter> {ptr_val q ..+ sz} = {}"
247
248lemma no_overlap_sym: "no_overlap x y = no_overlap y x"
249  apply (rule ext)
250  apply (clarsimp simp:no_overlap_def)
251  by blast
252
253(* FIXME: MOVE *)
254lemma h_val_not_id:
255  fixes x :: "'a::mem_type ptr"
256    and y :: "'b::mem_type ptr"
257  shows "{ptr_val x..+size_of TYPE('a)} \<inter> {ptr_val y..+size_of TYPE('b)} = {}
258     \<Longrightarrow> h_val (hrs_mem (hrs_mem_update (heap_update x v) s)) y = h_val (hrs_mem s) y"
259  apply (subst hrs_mem_heap_update[symmetric])
260  apply (subst h_val_heap_update_disjoint)
261   apply blast
262  apply clarsimp
263  done
264
265definition
266  update_bytes :: "'a globals_scheme \<Rightarrow> 'b::mem_type ptr \<Rightarrow> word8 list \<Rightarrow> 'a globals_scheme"
267where
268  "update_bytes s p bs \<equiv> s\<lparr>t_hrs_' := hrs_mem_update (heap_update_list (ptr_val p) bs) (t_hrs_' s)\<rparr>"
269
270lemma the_horse_says_neigh: "(s\<lparr>t_hrs_' := x\<rparr> = s\<lparr>t_hrs_' := y\<rparr>) = (x = y)"
271 by (metis (erased, lifting) globals.cases_scheme globals.select_convs(1) globals.update_convs(1))
272
273lemma upto_singleton[simp]:"[x..x] = [x]"
274  by (simp add: upto_rec1)
275
276lemma update_bytes_ignore_ptr_coerce[simp]: "update_bytes s (ptr_coerce p) = update_bytes s p"
277  by (clarsimp simp:update_bytes_def intro!:ext)
278
279lemma hrs_mem_update_commute:
280  "f \<circ> g = g \<circ> f \<Longrightarrow> hrs_mem_update f (hrs_mem_update g s) = hrs_mem_update g (hrs_mem_update f s)"
281  by (metis (no_types, lifting) comp_eq_elim hrs_htd_def hrs_htd_mem_update hrs_mem_def hrs_mem_f prod.collapse)
282
283lemma hrs_mem_update_collapse:
284  "hrs_mem_update f (hrs_mem_update g s) = hrs_mem_update (f \<circ> g) s"
285  by (metis comp_eq_dest_lhs hrs_htd_def hrs_htd_mem_update hrs_mem_def hrs_mem_f prod.collapse)
286
287lemma update_bytes_reorder:
288  "{ptr_val p..+length cs} \<inter> {ptr_val q..+length bs} = {} \<Longrightarrow>
289      update_bytes (update_bytes s q bs) p cs = update_bytes (update_bytes s p cs) q bs"
290  apply (clarsimp simp:update_bytes_def)
291  apply (subst the_horse_says_neigh)
292  apply (subst hrs_mem_update_commute)
293   apply (clarsimp intro!:ext)
294   apply (subst heap_update_list_commute)
295    apply clarsimp+
296  done
297
298lemma lt_step_down: "\<lbrakk>(x::nat) < y; x = y - 1 \<longrightarrow> P; x < y - 1 \<longrightarrow> P\<rbrakk> \<Longrightarrow> P"
299  by force
300
301(* XXX: This proof makes me sad. *)
302lemma under_uint_imp_no_overflow: "x < ADDR_MAX \<Longrightarrow> ((of_nat x)::addr) + 1 \<noteq> 0"
303  apply (induct x)
304   apply (clarsimp simp:UWORD_MAX_def)+
305  apply unat_arith
306  apply (clarsimp simp:UWORD_MAX_def)
307  apply (cut_tac y=x and z="(of_nat (ADDR_MAX - 1))::addr" in le_unat_uoi)
308   apply (clarsimp simp:UWORD_MAX_def)+
309  done
310
311lemma heap_update_list_append3:
312  "1 + length ys < 2 ^ word_bits \<Longrightarrow>
313    heap_update_list s (y # ys) hp = heap_update_list s [y] (heap_update_list (s + 1) ys hp)"
314  apply clarsimp
315  apply (subst heap_update_list_append2[where xs="[y]", simplified])
316   apply clarsimp+
317  done
318
319lemma hrs_mem_update_cong': "f = g \<Longrightarrow> hrs_mem_update f s = hrs_mem_update g s"
320  by presburger
321
322lemma update_bytes_append: "length bs \<le> ADDR_MAX \<Longrightarrow>
323  update_bytes s p (b # bs) = update_bytes (update_bytes s p [b]) (byte_cast p +\<^sub>p 1) bs"
324  apply (clarsimp simp:update_bytes_def)
325  apply (subst the_horse_says_neigh)
326  apply (subst hrs_mem_update_commute)
327   apply (rule ext)+
328   apply simp
329   apply (case_tac "xa = ptr_val p")
330    apply (clarsimp simp:fun_upd_def)
331    apply (subst heap_update_nmem_same)
332     apply (clarsimp simp:intvl_def ptr_add_def)
333     apply (subgoal_tac "k < ADDR_MAX")
334      prefer 2
335      apply unat_arith
336     apply (drule under_uint_imp_no_overflow)
337     apply unat_arith
338    apply clarsimp
339   apply (subst heap_update_list_update)
340    apply simp
341   apply (clarsimp simp:fun_upd_def)
342  apply (subst hrs_mem_update_collapse)
343  apply (rule hrs_mem_update_cong')
344  apply (clarsimp simp:ptr_add_def)
345  apply (rule ext)
346  apply (cut_tac xs="[b]" and ys=bs and s="ptr_val p" and hp=x in heap_update_list_append)
347  apply (clarsimp simp:fun_upd_def intro!:ext)
348  apply (rule conjI)
349   apply clarsimp
350   apply (subst heap_update_nmem_same)
351    apply (clarsimp simp:ptr_add_def intvl_def)
352    apply (subgoal_tac "k < ADDR_MAX")
353     prefer 2
354     apply unat_arith
355    apply (drule under_uint_imp_no_overflow)
356    apply unat_arith
357   apply clarsimp
358  apply clarsimp
359  apply (case_tac "xa \<in> {ptr_val p + 1..+length bs}")
360  apply (subst heap_update_mem_same_point)
361    apply simp
362   apply (subgoal_tac "addr_card = ADDR_MAX + 1")
363    apply clarsimp
364   apply (clarsimp simp:addr_card UWORD_MAX_def)
365  apply (subst heap_update_mem_same_point)
366    apply simp
367   apply (subgoal_tac "addr_card = ADDR_MAX + 1")
368    apply clarsimp
369   apply (clarsimp simp:addr_card UWORD_MAX_def)
370  apply clarsimp
371  apply (subst heap_update_nmem_same)
372   apply clarsimp
373  apply (subst heap_update_nmem_same)
374   apply clarsimp+
375  done
376
377lemma update_bytes_postpend: "length bs = x + 1 \<Longrightarrow>
378  update_bytes s p bs = update_bytes (update_bytes s p (take x bs)) (byte_cast p +\<^sub>p (of_nat x)) [bs ! x]"
379  apply (clarsimp simp:update_bytes_def)
380  apply (subst the_horse_says_neigh)
381  apply (clarsimp simp:ptr_add_def)
382  apply (subst heap_update_list_concat_fold_hrs_mem)
383   apply clarsimp+
384  by (metis append_eq_conv_conj append_self_conv hd_drop_conv_nth2 lessI take_hd_drop)
385
386lemma h_val_not_id_general:
387  fixes y :: "'a::mem_type ptr"
388  shows "\<forall>i \<in> {0..+size_of TYPE('a)}. \<forall>g. f g (ptr_val y + i) = g (ptr_val y + i)
389     \<Longrightarrow> h_val (hrs_mem (hrs_mem_update f s)) y = h_val (hrs_mem s) y"
390  apply (subst hrs_mem_update)
391  apply (clarsimp simp:h_val_def)
392  apply (subgoal_tac "heap_list (f (hrs_mem s)) (size_of TYPE('a)) (ptr_val y) =
393                      heap_list (hrs_mem s) (size_of TYPE('a)) (ptr_val y)")
394   apply clarsimp
395  apply (cut_tac h="f (hrs_mem s)" and p="ptr_val y" and n="size_of TYPE('a)"
396                 and h'="hrs_mem s" in heap_list_h_eq2)
397   apply (erule_tac x="x - ptr_val y" in  ballE)
398    apply clarsimp
399   apply (clarsimp simp:intvl_def)+
400  done
401
402lemma h_val_not_id_list:
403  fixes y :: "'a::mem_type ptr"
404  shows "{x..+length vs} \<inter> {ptr_val y..+size_of TYPE('a)} = {}
405     \<Longrightarrow> h_val (hrs_mem (hrs_mem_update (heap_update_list x vs) s)) y = h_val (hrs_mem s) y"
406  apply (subst h_val_not_id_general)
407   apply clarsimp
408   apply (metis (erased, hide_lams) disjoint_iff_not_equal heap_update_nmem_same intvlD intvlI
409          monoid_add_class.add.left_neutral)
410  apply clarsimp
411  done
412
413lemma h_val_id_update_bytes:
414  fixes q :: "'a::mem_type ptr"
415  shows "{ptr_val q..+size_of TYPE('a)} \<inter> {ptr_val p..+length bs} = {}
416          \<Longrightarrow> deref (update_bytes s p bs) q = deref s q"
417  apply (clarsimp simp:update_bytes_def)
418  apply (subst h_val_not_id_list)
419   apply blast
420  by simp
421
422lemma bytes_at_len: "bytes_at s p bs \<Longrightarrow> length bs \<le> ADDR_MAX"
423  by (clarsimp simp:bytes_at_def, fastforce)
424
425(* Another sad proof. *)
426lemma le_uint_max_imp_id: "x \<le> ADDR_MAX \<Longrightarrow> unat ((of_nat x)::addr) = x"
427  apply (induct x)
428   apply (clarsimp simp: UWORD_MAX_def)+
429  apply unat_arith
430  apply clarsimp
431  done
432
433lemma update_bytes_id: "update_bytes s p [] = s"
434  apply (clarsimp simp:update_bytes_def)
435  apply (subst heap_update_list_base')
436  by (simp add: hrs_mem_update_id3)
437
438lemma a_horse_by_any_other_name: "t_hrs_'_update f s = s\<lparr>t_hrs_' := f (t_hrs_' s)\<rparr>"
439  by auto
440
441lemma heap_update_list_singleton: "heap_update_list p [x] = heap_update (Ptr p) x"
442  apply (rule ext)
443  by (metis heap_update_def ptr_val.simps to_bytes_word8)
444
445lemma update_bytes_eq: "\<lbrakk>s = s'; p = p'; bs = bs'\<rbrakk> \<Longrightarrow> update_bytes s p bs = update_bytes s' p' bs'"
446  by clarsimp
447
448text \<open>
449  Memcpy does what it says on the box.
450\<close>
451lemma memcpy_wp':
452  fixes src :: "'a::mem_type ptr"
453    and dst :: "'b::mem_type ptr"
454  shows "\<forall>s0 bs.
455  \<lbrace>\<lambda>s. s = s0 \<and> c_guard src \<and> c_guard dst \<and> sz = of_nat (length bs) \<and> bytes_at s src bs \<and>
456       no_wrap src (unat sz) \<and> no_wrap dst (unat sz) \<and> no_overlap src dst (unat sz)\<rbrace>
457    memcpy' (ptr_coerce dst) (ptr_coerce src) sz
458  \<lbrace>\<lambda>r s. r = ptr_coerce dst \<and> bytes_at s dst bs \<and> s = update_bytes s0 dst bs\<rbrace>!"
459  apply (rule allI)+
460  apply (rule validNF_assume_pre)
461  unfolding memcpy'_def
462  apply clarsimp
463  apply (subst whileLoop_add_inv[where
464    I="\<lambda>i s. unat i \<le> unat sz \<and>
465             bytes_at s dst (take (unat i) bs) \<and>
466             bytes_at s src bs \<and>
467             s = update_bytes s0 dst (take (unat i) bs)" and
468    M="\<lambda>(i, s). unat sz - unat i"])
469  apply wp
470    apply clarsimp
471    apply (rule conjI)
472     apply unat_arith
473    apply (rule conjI)
474     apply (simp add:bytes_at_def)
475     apply (case_tac "bs = []")
476      apply (rule disjI1)
477      apply clarsimp
478     apply (rule disjI2)
479     apply clarsimp
480     apply (rule conjI)
481      apply unat_arith
482     apply clarsimp
483     apply (case_tac "unat i = ia")
484      apply clarsimp
485      apply (subgoal_tac "int (unat i) = uint i")
486       prefer 2
487       apply (subst uint_nat)
488       apply simp
489      apply simp
490      apply (subst h_val_id)
491      apply (subst h_val_id_update_bytes)
492       apply (clarsimp simp:no_overlap_def ptr_add_def)
493       apply (subgoal_tac "{ptr_val src + i..+Suc 0} \<subseteq> {ptr_val src..+unat (of_nat_addr (length bs))}")
494        prefer 2
495        apply (clarsimp simp:intvl_def)
496        apply (rule_tac x="unat i" in exI)
497        apply unat_arith
498       apply (subgoal_tac "{ptr_val dst..+unat i} \<subseteq> {ptr_val dst..+unat (of_nat_addr (length bs))}")
499        prefer 2
500        apply (clarsimp simp:intvl_def)
501        apply (rule exI, rule conjI, rule refl)
502        apply (simp add: unat_of_nat)
503       apply blast
504      apply (erule_tac x="unat i" and P="\<lambda>x. deref s0 (byte_cast src +\<^sub>p int x) = bs ! x" in ballE)
505       apply clarsimp
506       apply (subst nth_take)
507        apply unat_arith
508       apply simp
509      apply (erule disjE)
510       apply clarsimp+
511     apply (erule disjE)
512      apply (subgoal_tac "length bs \<noteq> 0")
513       prefer 2
514       apply clarsimp
515      apply (case_tac "unat i = 0")
516       apply unat_arith
517      apply linarith
518     apply (subst h_val_not_id)
519      apply (clarsimp simp:ptr_add_def intvl_def)
520      (* Isabelle, why do you have to make it so hard? *)
521      apply (erule_tac P="unat (of_nat ia) = ia" in notE)
522      apply (cut_tac y=ia and z="(of_nat ADDR_MAX)::addr" in le_unat_uoi)
523       apply (subgoal_tac "unat ((of_nat ADDR_MAX)::addr) = ADDR_MAX")
524        prefer 2
525        apply (simp add: unat_of_nat)
526       apply (simp add: unat_of_nat)
527      apply clarsimp
528     apply clarsimp
529     apply (erule_tac x=ia and A="{0..min (length bs) (unat i) - Suc 0}" in ballE)
530      apply clarsimp
531      apply (subst nth_take, unat_arith)+
532      apply simp
533     apply clarsimp
534     apply unat_arith
535    apply (rule conjI)
536     apply (clarsimp simp:bytes_at_def)
537     apply (subst h_val_not_id)
538      apply (clarsimp simp:no_overlap_def)
539      apply (subgoal_tac "ptr_val (byte_cast dst +\<^sub>p uint i) \<in> {ptr_val dst..+unat (of_nat (length bs))}")
540       prefer 2
541       apply (clarsimp simp:ptr_add_def intvl_def)
542       apply (rule_tac x="unat i" in exI)
543       apply clarsimp
544       apply unat_arith
545      (* More or less symmetric subgoal *)
546      apply (subgoal_tac "ptr_val (byte_cast src +\<^sub>p int ia) \<in> {ptr_val src..+unat ((of_nat (length bs))::addr)}")
547       prefer 2
548       apply (clarsimp simp:ptr_add_def intvl_def)
549       apply (rule_tac x=ia in exI)
550       apply clarsimp
551       apply (subgoal_tac "unat ((of_nat (length bs))::addr) = length bs")
552        apply clarsimp
553        apply arith
554       apply (cut_tac y="length bs" and z="(of_nat ADDR_MAX)::addr" in le_unat_uoi)
555        apply (simp add: unat_of_nat)
556       apply arith
557      apply (clarsimp simp:intvl_def ptr_add_def)
558      apply blast
559     apply clarsimp
560    apply (rule conjI)
561     apply (subst h_val_id_update_bytes)
562      apply (clarsimp simp:no_overlap_def ptr_add_def)
563      apply (subgoal_tac "{ptr_val src + i..+Suc 0} \<subseteq> {ptr_val src..+unat (of_nat_addr (length bs))}")
564       prefer 2
565       apply (clarsimp simp:intvl_def)
566       apply (rule_tac x="unat i" in exI)
567       apply unat_arith
568      apply (subgoal_tac "{ptr_val dst..+min (length bs) (unat i)} \<subseteq> {ptr_val dst..+unat (of_nat_addr (length bs))}")
569       prefer 2
570       apply (clarsimp simp:intvl_def)
571       apply (rule_tac x=ka in exI)
572       apply unat_arith
573      apply blast
574     apply (subgoal_tac "deref s0 (byte_cast src +\<^sub>p uint i) = bs ! (unat i)")
575      apply clarsimp
576      apply (subgoal_tac "update_bytes s0 dst (take (unat (i + 1)) bs) =
577                          update_bytes (update_bytes s0 dst (take (unat i) bs)) (byte_cast dst +\<^sub>p uint i) [bs ! unat i]")
578       apply clarsimp
579       apply (subgoal_tac
580               "\<forall>s'. t_hrs_'_update (hrs_mem_update (heap_update (byte_cast dst +\<^sub>p uint i) (bs ! unat i))) s' =
581                     update_bytes s' (byte_cast dst +\<^sub>p uint i) [bs ! unat i]")
582        apply fast
583       apply (clarsimp simp:update_bytes_def)
584       apply (subst a_horse_by_any_other_name)
585       apply (subst the_horse_says_neigh)
586       apply (clarsimp simp:ptr_add_def)
587       apply (subst heap_update_list_singleton)
588       apply simp
589      apply (cut_tac s=s0 and p=dst and bs="take (unat (i + 1)) bs" and x="unat i"
590                     in update_bytes_postpend)
591       apply (subgoal_tac "unat (i + 1) \<le> length bs")
592        apply clarsimp
593        apply unat_arith
594       apply (subgoal_tac "unat i < length bs")
595        apply unat_arith
596       apply (rule unat_less_helper)
597       apply simp
598      apply clarsimp
599      apply (rule update_bytes_eq)
600        apply (subgoal_tac "min (unat i) (unat (i + 1)) = unat i")
601         apply clarsimp
602        apply clarsimp
603        apply unat_arith
604       apply (clarsimp simp:ptr_add_def)
605      apply clarsimp
606      apply (rule nth_take)
607      apply unat_arith
608     apply (clarsimp simp:bytes_at_def)
609     apply (erule disjE)
610      apply clarsimp
611     apply clarsimp
612     apply (erule_tac x="unat i" in ballE)
613      apply (subst (asm) uint_nat[symmetric])
614      apply simp
615     apply clarsimp
616     apply (subgoal_tac "unat i < length bs")
617      prefer 2
618      apply (rule unat_less_helper)
619      apply simp
620     apply unat_arith
621    apply (rule conjI)
622     apply unat_arith
623    apply (rule conjI)
624     apply (rule byte_ptr_guarded)
625     apply (clarsimp simp:no_wrap_def intvl_def ptr_add_def)
626     apply (erule_tac x="unat i" in allE)
627     apply clarsimp
628    apply (rule byte_ptr_guarded)
629    apply (clarsimp simp:no_wrap_def intvl_def ptr_add_def)
630    apply (erule_tac x="unat i" and
631                     P="\<lambda>x. ptr_val dst + ((of_nat x)::addr) = 0 \<longrightarrow> \<not> x < unat ((of_nat_addr (length bs))::addr)"
632                    in allE)
633    apply clarsimp
634   apply clarsimp
635   apply (rule conjI)
636    apply (subgoal_tac "unat i = length bs")
637     apply clarsimp
638    apply (case_tac "length bs = 0")
639     apply clarsimp
640    apply (subgoal_tac "length bs \<le> ADDR_MAX")
641     prefer 2
642     apply (clarsimp simp:bytes_at_def)
643    (* XXX: We keep introducing this subgoal; we should do it once and for all up top. *)
644    apply (subgoal_tac "unat ((of_nat (length bs))::addr) = length bs")
645     prefer 2
646     apply (cut_tac y="length bs" and z="(of_nat ADDR_MAX)::addr" in le_unat_uoi)
647      apply (clarsimp simp:UWORD_MAX_def)
648     apply clarsimp+
649    apply unat_arith
650   (* insert a bunch a tedium... *)
651   apply (subgoal_tac "unat i = length bs")
652    prefer 2
653    apply (drule bytes_at_len)
654    apply (subgoal_tac "unat (of_nat_addr (length bs)) = length bs")
655     prefer 2
656     apply (rule le_uint_max_imp_id)
657     apply simp
658    apply unat_arith
659   apply clarsimp
660  apply (simp add:update_bytes_id)
661  done
662
663lemma validNF_make_schematic_post':
664  "(\<forall>s0 x. \<lbrace> \<lambda>s. P s0 x s \<rbrace> f \<lbrace> \<lambda>rv s. Q s0 x rv s \<rbrace>!) \<Longrightarrow>
665   \<lbrace> \<lambda>s. \<exists>s0 x. P s0 x s \<and> (\<forall>rv s'. Q s0 x rv s' \<longrightarrow> Q' rv s') \<rbrace> f \<lbrace> Q'\<rbrace>!"
666  by (auto simp add: valid_def validNF_def no_fail_def split: prod.splits)
667
668lemmas memcpy_wp = memcpy_wp'[THEN validNF_make_schematic_post', simplified]
669
670lemma h_val_not_id_update_bytes:
671  fixes q :: "'a::mem_type ptr"
672  shows "\<lbrakk>ptr_val p = ptr_val q; length bs = size_of TYPE('a)\<rbrakk> \<Longrightarrow>
673            deref (update_bytes s p bs) q = from_bytes bs"
674  apply (clarsimp simp:update_bytes_def h_val_def)
675  apply (subst hrs_mem_update)
676  apply (cut_tac p="ptr_val q" and v=bs and h="hrs_mem (t_hrs_' s)" in heap_list_update)
677   apply clarsimp
678   apply (metis less_imp_le max_size)
679  by clarsimp
680
681text \<open>
682  Test that we can use memcpy in a compositional proof. The following proof can be done much more
683  pleasantly, but we're just trying to check that the memcpy WP lemma is usable.
684  TODO: This relies on disabling heap abstraction for the calling function as well. We should be
685  able to phrase an exec_concrete WP lemma over memcpy that lets us prove properties about
686  heap-abstracted callers. This will need AutoCorres support to connect is_valid_* with
687  c_guard/no_overlap/no_wrap.
688\<close>
689
690definition
691  memcpy_int_spec :: "sword32 ptr \<Rightarrow> sword32 ptr \<Rightarrow> bool"
692where
693  "memcpy_int_spec dst src \<equiv>
694    \<forall>x. \<lbrace>\<lambda>s. deref s src = x \<and>
695             {ptr_val src..+4} \<inter> {ptr_val dst..+4} = {} \<and>
696             c_guard src \<and> c_guard dst \<and>
697             no_wrap src 4 \<and> no_wrap dst 4\<rbrace>
698          memcpy_int' dst src
699        \<lbrace>\<lambda>_ s. deref s dst = x\<rbrace>!"
700
701lemma memcpy_int_wp'[unfolded memcpy_int_spec_def]: "memcpy_int_spec dst src"
702  unfolding memcpy_int_spec_def
703  apply (rule allI)
704  unfolding memcpy_int'_def
705  apply (wp memcpy_wp)
706  apply clarsimp
707  apply (rule_tac x="[deref s (byte_cast src),
708                      deref s (byte_cast src +\<^sub>p 1),
709                      deref s (byte_cast src +\<^sub>p 2),
710                      deref s (byte_cast src +\<^sub>p 3)]" in exI)
711  apply (clarsimp simp:bytes_at_def no_overlap_def UINT_MAX_def)
712  apply (rule conjI)
713   apply clarsimp
714   apply (case_tac "i = 0", clarsimp)
715   apply (case_tac "i = 1", clarsimp)
716   apply (case_tac "i = 2", clarsimp)
717   apply (case_tac "i = 3", clarsimp)
718   apply clarsimp
719  apply clarsimp
720  apply (subst h_val_not_id_update_bytes)
721    apply clarsimp+
722  apply (clarsimp simp:h_val_def)
723  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 4 (ptr_val src) =
724                      deref s (byte_cast src) # (heap_list (hrs_mem (t_hrs_' s)) 3 (ptr_val src + 1))")
725   prefer 2
726   apply (clarsimp simp:h_val_def)
727   apply (metis Suc_numeral from_bytes_eq heap_list_rec semiring_norm(2) semiring_norm(8))
728  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 3 (ptr_val src + 1) =
729                      deref s (byte_cast src +\<^sub>p 1) # (heap_list (hrs_mem (t_hrs_' s)) 2 (ptr_val src + 2))")
730   prefer 2
731   apply (clarsimp simp:h_val_def ptr_add_def)
732   apply (cut_tac h="hrs_mem (t_hrs_' s)" and p="ptr_val src + 1" and n=2 in heap_list_rec)
733   apply clarsimp
734   apply (simp add: add.commute from_bytes_eq)
735  apply clarsimp
736  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 2 (ptr_val src + 2) =
737                      deref s (byte_cast src +\<^sub>p 2) # (heap_list (hrs_mem (t_hrs_' s)) 1 (ptr_val src + 3))")
738   prefer 2
739   apply (cut_tac h="hrs_mem (t_hrs_' s)" and p="ptr_val src + 2" and n=3 in heap_list_rec)
740   apply (clarsimp simp:h_val_def ptr_add_def from_bytes_eq)
741   apply (metis (no_types, hide_lams) Suc_eq_plus1 heap_list_base heap_list_rec is_num_normalize(1)
742                monoid_add_class.add.left_neutral one_add_one one_plus_numeral semiring_norm(3))
743  apply (clarsimp simp:h_val_def ptr_add_def from_bytes_eq)
744  done
745
746text \<open>memcpying a typed variable is equivalent to assignment.\<close>
747lemma memcpy_type_wp':
748  fixes dst :: "'a::mem_type ptr"
749    and src :: "'a::mem_type ptr"
750  shows "\<forall>s0 bs.
751   \<lbrace>\<lambda>s. s = s0 \<and> c_guard dst \<and> c_guard src \<and> sz = of_nat (size_of TYPE('a)) \<and>
752        no_overlap dst src (unat sz) \<and> no_wrap dst (unat sz) \<and> no_wrap src (unat sz) \<and>
753        bytes_of s src bs\<rbrace>
754     memcpy' (ptr_coerce dst) (ptr_coerce src) sz
755   \<lbrace>\<lambda>r s. r = ptr_coerce dst \<and> bytes_of s dst bs \<and> s = update_bytes s0 dst bs\<rbrace>!"
756  apply (rule allI)+
757  apply (wp memcpy_wp)
758  apply clarsimp
759  apply (rule_tac x=bs in exI)
760  apply clarsimp
761  apply (subst no_overlap_sym)
762  apply (clarsimp simp:bytes_of_def)
763  done
764
765lemmas memcpy_type_wp = memcpy_type_wp'[THEN validNF_make_schematic_post', simplified]
766
767text \<open>Confirm that we can also prove memcpy_int using the previous generic lemma.\<close>
768lemma memcpy_int_wp''[unfolded memcpy_int_spec_def]: "memcpy_int_spec dst src"
769  unfolding memcpy_int_spec_def memcpy_int'_def
770  apply (rule allI)
771  apply (wp memcpy_type_wp)
772  (* Remainder mostly clagged from the original proof above. *)
773  apply clarsimp
774  apply (rule conjI, clarsimp simp:no_overlap_def, blast)
775  apply (rule_tac x="[deref s (byte_cast src),
776                      deref s (byte_cast src +\<^sub>p 1),
777                      deref s (byte_cast src +\<^sub>p 2),
778                      deref s (byte_cast src +\<^sub>p 3)]" in exI)
779  apply (rule conjI)
780   apply (clarsimp simp:bytes_of_def bytes_at_def UINT_MAX_def)
781   apply (case_tac "i = 0", clarsimp)
782   apply (case_tac "i = 1", clarsimp)
783   apply (case_tac "i = 2", clarsimp)
784   apply (case_tac "i = 3", clarsimp)
785   apply clarsimp
786  apply clarsimp
787  apply (subst h_val_not_id_update_bytes, clarsimp+)
788  apply (clarsimp simp:h_val_def)
789  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 4 (ptr_val src) =
790                      deref s (byte_cast src) # (heap_list (hrs_mem (t_hrs_' s)) 3 (ptr_val src + 1))")
791   prefer 2
792   apply (clarsimp simp:h_val_def from_bytes_eq)
793   apply (subst heap_list_rec[symmetric])
794   apply simp
795  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 3 (ptr_val src + 1) =
796                      deref s (byte_cast src +\<^sub>p 1) # (heap_list (hrs_mem (t_hrs_' s)) 2 (ptr_val src + 2))")
797   prefer 2
798   apply (clarsimp simp:h_val_def ptr_add_def)
799   apply (cut_tac h="hrs_mem (t_hrs_' s)" and p="ptr_val src + 1" and n=2 in heap_list_rec)
800   apply (clarsimp simp: from_bytes_eq)
801   apply (metis add.commute)
802  apply clarsimp
803  apply (subgoal_tac "heap_list (hrs_mem (t_hrs_' s)) 2 (ptr_val src + 2) =
804                      deref s (byte_cast src +\<^sub>p 2) # (heap_list (hrs_mem (t_hrs_' s)) 1 (ptr_val src + 3))")
805   prefer 2
806   apply (cut_tac h="hrs_mem (t_hrs_' s)" and p="ptr_val src + 2" and n=3 in heap_list_rec)
807   apply (clarsimp simp:h_val_def ptr_add_def from_bytes_eq)
808   apply (metis (no_types, hide_lams) Suc_eq_plus1 heap_list_base heap_list_rec is_num_normalize(1)
809                monoid_add_class.add.left_neutral one_add_one one_plus_numeral semiring_norm(3))
810  apply (clarsimp simp:h_val_def ptr_add_def from_bytes_eq)
811  done
812
813lemma bytes_of_imp_at[simp]: "bytes_of s x bs \<Longrightarrow> bytes_at s x bs"
814  by (clarsimp simp:bytes_of_def bytes_at_def)
815
816lemma bytes_at_imp_of:
817  fixes x :: "'a::mem_type ptr"
818  shows "\<lbrakk>bytes_at s x bs; length bs = size_of TYPE('a)\<rbrakk> \<Longrightarrow> bytes_of s x bs"
819  by (clarsimp simp:bytes_of_def bytes_at_def)
820
821text \<open>
822  Memcpying from a source to a destination via an intermediary does what it should. This is close to
823  the desirable property we want for CAmkES systems; i.e. that copying into your IPC buffer on one
824  side and then out on the other gives you back what you put in. Note that the type of the
825  intermediate pointer is irrelevant and we don't need to assume that the source and final
826  destination do not overlap.
827\<close>
828lemma memcpy_seq:
829  fixes x :: "'a::mem_type ptr"
830    and y :: "'b::mem_type ptr"
831    and z :: "'a::mem_type ptr"
832  shows "\<forall>s0 bs.
833   \<lbrace>\<lambda>s. s = s0 \<and> sz = of_nat (size_of TYPE('a)) \<and>
834        c_guard x \<and> c_guard y \<and> c_guard z \<and>
835        no_wrap x (unat sz) \<and> no_wrap y (unat sz) \<and> no_wrap z (unat sz) \<and>
836        no_overlap x y (unat sz) \<and> no_overlap y z (unat sz) \<and>
837        bytes_of s x bs\<rbrace>
838    do memcpy' (ptr_coerce y) (ptr_coerce x) sz;
839       memcpy' (ptr_coerce z) (ptr_coerce y) sz
840    od
841   \<lbrace>\<lambda>r s. r = ptr_coerce z \<and> bytes_of s z bs\<rbrace>!"
842  apply (rule allI)+
843  apply (wp memcpy_wp)
844  apply clarsimp
845  apply (rule_tac x=bs in exI)
846  apply clarsimp
847  apply (rule conjI, clarsimp simp:bytes_of_def)
848  apply clarsimp
849  apply (rule_tac x=bs in exI)
850  apply (rule conjI, clarsimp simp:bytes_of_def)
851  apply clarsimp
852  apply (rule bytes_at_imp_of)
853   apply (clarsimp simp:bytes_of_def)+
854  done
855
856lemma update_ti_eq:
857  fixes x :: "'a::mem_type"
858    and y :: 'a
859  shows "\<lbrakk>length bs = size_of TYPE('a); bs = bs'\<rbrakk>
860          \<Longrightarrow> update_ti_t (typ_info_t TYPE('a)) bs x = update_ti_t (typ_info_t TYPE('a)) bs' y"
861  by (clarsimp simp:upd)
862
863lemma from_bytes_cong: "x = y \<Longrightarrow> from_bytes x = from_bytes y"
864  by simp
865
866declare from_bytes_eq [simp]
867
868text \<open>
869  If you dereference a pointer, the value you get is the same as the underlying bytes backing that
870  memory.
871\<close>
872lemma val_eq_bytes:
873  fixes x :: "'a::mem_type ptr"
874  shows "deref s x = from_bytes (map (\<lambda>off. deref s (byte_cast x +\<^sub>p of_nat off)) [0..<size_of TYPE('a)])"
875  apply (clarsimp simp:h_val_def ptr_add_def)
876  apply (rule from_bytes_cong)
877  apply (rule nth_equalityI)
878   apply clarsimp+
879  apply (subst heap_list_nth)
880   apply clarsimp+
881  done
882
883lemma extract_list_elem: "i < n \<Longrightarrow> f i = (map f [0..<n]) ! i"
884  apply (induct i)
885   apply clarsimp+
886  done
887
888lemma update_deref:
889  fixes x :: "'a::mem_type ptr"
890  shows "size_of TYPE('a) = length bs \<Longrightarrow> deref (update_bytes s x bs) x = from_bytes bs"
891  apply (clarsimp simp:update_bytes_def)
892  apply (subst hrs_mem_update)
893  apply (clarsimp simp:h_val_def)
894  apply (subst heap_list_update)
895   apply (metis less_imp_le max_size)
896  apply clarsimp
897  done
898
899text \<open>
900  The memcpy_int proof can now be completed more elegantly. Note that the body of this proof is more
901  generic than the previous attempts and doesn't involve manually reasoning about each byte.
902\<close>
903lemma memcpy_int_wp'''[unfolded memcpy_int_spec_def]: "memcpy_int_spec dst src"
904  unfolding memcpy_int_spec_def memcpy_int'_def
905  apply (rule allI)
906  apply (wp memcpy_type_wp)
907  apply clarsimp
908  apply (rule conjI, clarsimp simp:no_overlap_def, blast)
909  apply (rule_tac x="map (\<lambda>i. deref s (byte_cast src +\<^sub>p of_nat i)) [0..<size_of TYPE(32sword)]" in exI)
910  apply (rule conjI)
911   apply (clarsimp simp:bytes_of_def bytes_at_def UINT_MAX_def)+
912  apply (subst update_deref)
913   apply clarsimp
914  apply (cut_tac s=s and x=src in val_eq_bytes)
915  apply clarsimp
916  done
917
918lemma bytes_at_heap_list:
919  fixes x :: "'a::mem_type ptr"
920  shows "\<lbrakk>n \<le> ADDR_MAX; no_wrap x n\<rbrakk>
921          \<Longrightarrow> bytes_at s x (heap_list (hrs_mem (t_hrs_' s)) n (ptr_val x))"
922  apply (clarsimp simp:bytes_at_def ptr_add_def h_val_def)
923  apply (subst heap_list_nth)
924   apply unat_arith
925  apply clarsimp
926  done
927
928text \<open>
929  A collection of useful type-generic implications for moving from the abstract heap to the concrete
930  heap.
931\<close>
932definition
933  is_valid_imp_c_guard :: "(lifted_globals \<Rightarrow> 'b::mem_type ptr \<Rightarrow> bool) \<Rightarrow> bool"
934where
935  "is_valid_imp_c_guard is_valid \<equiv> \<forall>s p. is_valid (lift_global_heap s) p \<longrightarrow> c_guard p"
936definition
937  is_valid_imp_no_null :: "(lifted_globals \<Rightarrow> 'b::mem_type ptr \<Rightarrow> bool) \<Rightarrow> bool"
938where
939  "is_valid_imp_no_null is_valid \<equiv>
940     \<forall>s p. is_valid (lift_global_heap s) p \<longrightarrow> 0 \<notin> {ptr_val p..of_nat (size_of TYPE('b))}"
941definition
942  is_valid_imp_no_wrap :: "(lifted_globals \<Rightarrow> 'b::mem_type ptr \<Rightarrow> bool) \<Rightarrow> bool"
943where
944  "is_valid_imp_no_wrap is_valid \<equiv>
945     \<forall>s p. is_valid (lift_global_heap s) p \<longrightarrow> no_wrap p (size_of TYPE('b))"
946definition
947  is_valid_imp_no_overlap :: "(lifted_globals \<Rightarrow> 'b::mem_type ptr \<Rightarrow> bool) \<Rightarrow> bool"
948where
949  "is_valid_imp_no_overlap is_valid \<equiv>
950     \<forall>s p q. is_valid (lift_global_heap s) p \<and> is_valid (lift_global_heap s) q \<and> p \<noteq> q
951               \<longrightarrow> no_overlap p q (size_of TYPE('b))"
952definition
953  is_valid_imp_heap_ptr_valid :: "(lifted_globals \<Rightarrow> 'b::mem_type ptr \<Rightarrow> bool) \<Rightarrow> bool"
954where
955  "is_valid_imp_heap_ptr_valid is_valid \<equiv>
956     \<forall>s p. is_valid (lift_global_heap s) p \<longrightarrow> heap_ptr_valid (hrs_htd (t_hrs_' s)) p"
957
958text \<open>We can easily discharge these for a given type.\<close>
959lemma is_valid_w32_imp_c_guard[unfolded is_valid_imp_c_guard_def, simplified]:
960    "is_valid_imp_c_guard is_valid_w32"
961  unfolding is_valid_imp_c_guard_def
962  apply clarsimp
963  apply (subst (asm) lifted_globals_ext_simps)
964  apply clarsimp
965  apply (rule simple_lift_c_guard, force)
966  done
967
968lemma is_valid_w32_imp_no_null[unfolded is_valid_imp_no_null_def, simplified]:
969    "is_valid_imp_no_null is_valid_w32"
970  unfolding is_valid_imp_no_null_def
971  apply clarsimp
972  apply (subst (asm) lifted_globals_ext_simps)
973  apply clarsimp
974  apply (drule simple_lift_c_guard)
975  apply (clarsimp simp:c_guard_def c_null_guard_def intvl_def)
976  by force
977
978lemma is_valid_w32_imp_no_wrap[unfolded is_valid_imp_no_wrap_def, simplified]:
979    "is_valid_imp_no_wrap is_valid_w32"
980  unfolding is_valid_imp_no_wrap_def no_wrap_def
981  apply clarsimp
982  apply (subst (asm) lifted_globals_ext_simps)
983  apply clarsimp
984  apply (drule simple_lift_c_guard)
985  apply (clarsimp simp:c_guard_def c_null_guard_def intvl_def)
986  done
987
988lemma is_valid_w32_imp_no_overlap[unfolded is_valid_imp_no_overlap_def, simplified]:
989    "is_valid_imp_no_overlap is_valid_w32"
990  unfolding is_valid_imp_no_overlap_def no_wrap_def
991  apply clarsimp
992  apply (subst (asm) lifted_globals_ext_simps)+
993  apply clarsimp
994  apply (drule simple_lift_heap_ptr_valid)+
995  apply (clarsimp simp:no_overlap_def)
996  apply (cut_tac p=p and q=q and d="hrs_htd (t_hrs_' s)" in heap_ptr_valid_neq_disjoint)
997     apply clarsimp+
998  done
999
1000lemma is_valid_w32_imp_heap_ptr_valid[unfolded is_valid_imp_heap_ptr_valid_def, simplified]:
1001    "is_valid_imp_heap_ptr_valid is_valid_w32"
1002  unfolding is_valid_imp_heap_ptr_valid_def
1003  apply clarsimp
1004  apply (subst (asm) lifted_globals_ext_simps)
1005  apply clarsimp
1006  by (rule simple_lift_heap_ptr_valid, force)
1007
1008text \<open>
1009  With that support in place, we can now prove a heap-abstracted call to memcpy of a type in a
1010  reasonably generic way. Note that we leverage the relationship between
1011  is_valid_*/lift_global_heap/simple_lift to transfer assumptions across the boundary between the
1012  abstract and concrete heaps.
1013\<close>
1014lemma
1015  fixes dst :: "32word ptr"
1016    and src :: "32word ptr"
1017  shows "\<forall>s0 x.
1018   \<lbrace>\<lambda>s. s = s0 \<and> is_valid_w32 s dst \<and> is_valid_w32 s src \<and> sz = of_nat (size_of TYPE(32word)) \<and>
1019        heap_w32 s src = x \<and> dst \<noteq> src\<rbrace>
1020     exec_concrete lift_global_heap (memcpy' (ptr_coerce dst) (ptr_coerce src) sz)
1021   \<lbrace>\<lambda>r s. r = ptr_coerce dst \<and> heap_w32 s dst = x\<rbrace>!"
1022  including nf_no_pre
1023  apply (rule allI)+
1024  apply (wp memcpy_wp)
1025  apply (clarsimp simp:is_valid_w32_imp_c_guard
1026                       is_valid_w32_imp_no_wrap
1027                       is_valid_w32_imp_no_overlap)
1028  apply (rule_tac x="map (\<lambda>i. deref s (byte_cast src +\<^sub>p of_nat i)) [0..<size_of TYPE(32word)]" in exI)
1029  apply clarsimp
1030  apply (rule conjI)
1031   apply (clarsimp simp:bytes_at_def UINT_MAX_def)
1032  apply clarsimp
1033  apply (subst lifted_globals_ext_simps(3))+
1034  apply (clarsimp simp:simple_lift_def is_valid_w32_imp_heap_ptr_valid)
1035  apply (rule conjI)
1036   apply clarsimp
1037   apply (subst update_deref)
1038    apply clarsimp+
1039   apply (cut_tac s=s and x=src in val_eq_bytes)
1040   apply clarsimp
1041  apply (clarsimp simp:update_bytes_def is_valid_w32_imp_heap_ptr_valid)
1042  done
1043
1044text \<open>
1045  Let's do the same instantiation for a structure. Note that the proof text for the following lemmas
1046  is identical to the word 32 instantiation above. These could be straightforwardly abstracted into
1047  a locale which could be automatically interpreted with the use of generated proofs.
1048\<close>
1049lemma is_valid_my_structure_imp_c_guard[unfolded is_valid_imp_c_guard_def, simplified]:
1050    "is_valid_imp_c_guard is_valid_my_structure_C"
1051  unfolding is_valid_imp_c_guard_def
1052  apply clarsimp
1053  apply (subst (asm) lifted_globals_ext_simps)
1054  apply clarsimp
1055  apply (rule simple_lift_c_guard, force)
1056  done
1057
1058lemma is_valid_my_structure_imp_no_null[unfolded is_valid_imp_no_null_def, simplified]:
1059    "is_valid_imp_no_null is_valid_my_structure_C"
1060  unfolding is_valid_imp_no_null_def
1061  apply clarsimp
1062  apply (subst (asm) lifted_globals_ext_simps)
1063  apply clarsimp
1064  apply (drule simple_lift_c_guard)
1065  apply (clarsimp simp:c_guard_def c_null_guard_def intvl_def)
1066  by force
1067
1068lemma is_valid_my_structure_imp_no_wrap[unfolded is_valid_imp_no_wrap_def, simplified]:
1069    "is_valid_imp_no_wrap is_valid_my_structure_C"
1070  unfolding is_valid_imp_no_wrap_def no_wrap_def
1071  apply clarsimp
1072  apply (subst (asm) lifted_globals_ext_simps)
1073  apply clarsimp
1074  apply (drule simple_lift_c_guard)
1075  apply (clarsimp simp:c_guard_def c_null_guard_def intvl_def)
1076  done
1077
1078lemma is_valid_my_structure_imp_no_overlap[unfolded is_valid_imp_no_overlap_def, simplified]:
1079    "is_valid_imp_no_overlap is_valid_my_structure_C"
1080  unfolding is_valid_imp_no_overlap_def no_wrap_def
1081  apply clarsimp
1082  apply (subst (asm) lifted_globals_ext_simps)+
1083  apply clarsimp
1084  apply (drule simple_lift_heap_ptr_valid)+
1085  apply (clarsimp simp:no_overlap_def)
1086  apply (cut_tac p=p and q=q and d="hrs_htd (t_hrs_' s)" in heap_ptr_valid_neq_disjoint)
1087     apply clarsimp+
1088  done
1089
1090lemma is_valid_my_structure_imp_heap_ptr_valid[unfolded is_valid_imp_heap_ptr_valid_def, simplified]:
1091    "is_valid_imp_heap_ptr_valid is_valid_my_structure_C"
1092  unfolding is_valid_imp_heap_ptr_valid_def
1093  apply clarsimp
1094  apply (subst (asm) lifted_globals_ext_simps)
1095  apply clarsimp
1096  by (rule simple_lift_heap_ptr_valid, force)
1097
1098text \<open>
1099  Again, we can now trivially transfer Hoare triple properties.
1100\<close>
1101lemma
1102  fixes dst :: "my_structure_C ptr"
1103    and src :: "my_structure_C ptr"
1104  shows "\<forall>s0 x.
1105   \<lbrace>\<lambda>s. s = s0 \<and> is_valid_my_structure_C s dst \<and> is_valid_my_structure_C s src \<and>
1106        heap_my_structure_C s src = x \<and> dst \<noteq> src\<rbrace>
1107     memcpy_struct' dst src
1108   \<lbrace>\<lambda>r s. r = dst \<and> heap_my_structure_C s dst = x\<rbrace>!"
1109  including nf_no_pre
1110  apply (rule allI)+
1111  unfolding memcpy_struct'_def
1112  apply (wp memcpy_wp)
1113  apply (clarsimp simp:is_valid_my_structure_imp_c_guard)
1114  apply (rule_tac x="map (\<lambda>i. deref s (byte_cast src +\<^sub>p of_nat i)) [0..<size_of TYPE(my_structure_C)]" in exI)
1115  apply (clarsimp simp:is_valid_my_structure_imp_no_wrap is_valid_my_structure_imp_no_overlap)
1116  apply (rule conjI)
1117   apply (clarsimp simp:bytes_at_def UINT_MAX_def)
1118  apply clarsimp
1119  apply (subst lifted_globals_ext_simps)+
1120  apply (clarsimp simp:simple_lift_def is_valid_my_structure_imp_heap_ptr_valid)
1121  apply (rule conjI)
1122   apply clarsimp
1123   apply (subst update_deref)
1124    apply clarsimp
1125   apply (cut_tac s=s and x=src in val_eq_bytes)
1126   apply clarsimp
1127  apply (clarsimp simp:update_bytes_def is_valid_my_structure_imp_heap_ptr_valid)
1128  done
1129
1130end
1131
1132end
1133