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