theory Intent_DR

lemma store_word_corres:
  "within_page buf ptr sz \<Longrightarrow>
  dcorres dc \<top>
  (pspace_aligned and pspace_distinct and valid_objs and
  (ipc_frame_ptr_at buf s_id) and (ipc_frame_sz_at sz s_id) and valid_etcbs)
  (corrupt_frame buf) (do_machine_op (storeWord ptr b))" apply (case_tac "is_aligned ptr 2") apply (simp add: corrupt_frame_def) apply (simp add: do_machine_op_def gets_def) apply (rule dcorres_absorb_get_r) apply clarsimp apply (drule store_word_corres_helper[where s_id = s_id],simp+) apply (simp add:ipc_frame_wp_at_def obj_at_def)+ apply clarsimp apply (rule corres_guard_imp) apply (rule_tac Q="(=) s'" and P =\<top> in select_pick_corres) apply (simp add: select_f_store_word bind_assoc) apply (clarsimp simp:assert_def corres_free_fail) apply (rule corres_modify, simp) apply (rule sym) apply simp+ apply (clarsimp simp: do_machine_op_def gets_def) apply (rule dcorres_absorb_get_r) apply (rule corres_guard_imp) apply (clarsimp simp:select_f_def fail_def storeWord_def
                         is_aligned_mask assert_def
          |rule conjI)+ apply (simp add:bind_def simpler_modify_def corres_free_fail[unfolded fail_def])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. within_page buf ptr sz \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b))
 2. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (do f <- select UNIV;
modify (corrupt_intents f buf)
od) (do_machine_op (storeWord ptr b))
 2. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (do f <- select UNIV;
modify (corrupt_intents f buf)
od) (do s <- get;
(r, ms') <- select_f (storeWord ptr b (machine_state s));
modify (update_machine ms')
od)
 2. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; True; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do f <- select UNIV;
modify (corrupt_intents f buf)
od) (do (r, ms') <- select_f (storeWord ptr b (machine_state s'));
modify (update_machine ms')
od)
 2. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_aligned s'; pspace_distinct s'; valid_objs s'; ipc_frame_ptr_at buf s_id s'; ipc_frame_sz_at sz s_id s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do f <- select UNIV;
modify (corrupt_intents f buf)
od) (do (r, ms') <- select_f (storeWord ptr b (machine_state s'));
modify (update_machine ms')
od)
 2. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; ipc_frame_ptr_at buf s_id s'; ipc_frame_sz_at sz s_id s'; valid_etcbs s'; \<exists>f. corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do f <- select UNIV;
modify (corrupt_intents f buf)
od) (do (r, ms') <- select_f (storeWord ptr b (machine_state s'));
modify (update_machine ms')
od)
 2. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; \<exists>ko. kheap s' s_id = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> (case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False)); \<exists>ko. kheap s' s_id = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> (case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False)); valid_etcbs s'; \<exists>f. corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do f <- select UNIV;
modify (corrupt_intents f buf)
od) (do (r, ms') <- select_f (storeWord ptr b (machine_state s'));
modify (update_machine ms')
od)
 2. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (2 subgoals):
 1. \<And>s' f tcb. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do f <- select UNIV;
modify (corrupt_intents f buf)
od) (do (r, ms') <- select_f (storeWord ptr b (machine_state s'));
modify (update_machine ms')
od)
 2. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (4 subgoals):
 1. \<And>s' f tcb. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> dcorres dc (?Q33 s' f tcb) (?Q'33 s' f tcb) (do f <- select UNIV;
modify (corrupt_intents f buf)
od) (do (r, ms') <- select_f (storeWord ptr b (machine_state s'));
modify (update_machine ms')
od)
 2. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform s' = s\<rbrakk> \<Longrightarrow> ?Q33 s' f tcb s
 3. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; s' = s\<rbrakk> \<Longrightarrow> ?Q'33 s' f tcb s
 4. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (4 subgoals):
 1. \<And>s' f tcb. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (modify (corrupt_intents (?x37 s' f tcb) buf)) (do (r, ms') <- select_f (storeWord ptr b (machine_state s'));
modify (update_machine ms')
od)
 2. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ?x37 s' f tcb \<in> UNIV)) s
 3. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; s' = s\<rbrakk> \<Longrightarrow> s' = s
 4. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (4 subgoals):
 1. \<And>s' f tcb. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (modify (corrupt_intents (?x37 s' f tcb) buf)) (do y <- assert (ptr && mask 2 = 0);
modify (update_machine (storeWord_ms ptr b (machine_state s')))
od)
 2. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ?x37 s' f tcb \<in> UNIV)) s
 3. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; s' = s\<rbrakk> \<Longrightarrow> s' = s
 4. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (4 subgoals):
 1. \<And>s' f tcb. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; ptr && mask 2 = 0\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (modify (corrupt_intents (?x37 s' f tcb) buf)) (modify (update_machine (storeWord_ms ptr b (machine_state s'))))
 2. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ?x37 s' f tcb \<in> UNIV)) s
 3. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; s' = s\<rbrakk> \<Longrightarrow> s' = s
 4. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (4 subgoals):
 1. \<And>s' f tcb s s'a. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'a; valid_objs s'a; valid_etcbs s'a; corrupt_intents f buf s = transform (update_machine (storeWord_ms ptr (?b10 s'a) (machine_state s'a)) s'a); kheap s'a s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; ptr && mask 2 = 0; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> transform (update_machine (storeWord_ms ptr b (machine_state s'a)) s'a) = corrupt_intents (?x37 s'a f tcb) buf s
 2. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ?x37 s' f tcb \<in> UNIV)) s
 3. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; s' = s\<rbrakk> \<Longrightarrow> s' = s
 4. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (4 subgoals):
 1. \<And>s' f tcb s s'a. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'a; valid_objs s'a; valid_etcbs s'a; corrupt_intents f buf s = transform (update_machine (storeWord_ms ptr (?b10 s'a) (machine_state s'a)) s'a); kheap s'a s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; ptr && mask 2 = 0; s' = s'a; transform s'a = s\<rbrakk> \<Longrightarrow> corrupt_intents (?x37 s'a f tcb) buf s = transform (update_machine (storeWord_ms ptr b (machine_state s'a)) s'a)
 2. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ?x37 s' f tcb \<in> UNIV)) s
 3. \<And>s' f tcb s. \<lbrakk>within_page buf ptr sz; is_aligned ptr 2; pspace_distinct s'; valid_objs s'; valid_etcbs s'; corrupt_intents f buf (transform s') = transform (update_machine (storeWord_ms ptr (?b10 s') (machine_state s')) s'); kheap s' s_id = Some (TCB tcb); case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sz mapdata) \<Rightarrow> buf = ptr | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; case tcb_ipcframe tcb of ArchObjectCap (PageCap dev ptr rights sza mapdata) \<Rightarrow> sz = sza | ArchObjectCap _ \<Rightarrow> False | _ \<Rightarrow> False; s' = s\<rbrakk> \<Longrightarrow> s' = s
 4. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do_machine_op (storeWord ptr b)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) (corrupt_frame buf) (do s <- get;
(r, ms') <- select_f (storeWord ptr b (machine_state s));
modify (update_machine ms')
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2; True; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_frame buf) (do (r, ms') <- select_f (storeWord ptr b (machine_state s'));
modify (update_machine ms')
od) proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2; True; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q52 s') (?Q'52 s') (corrupt_frame buf) (do (r, ms') <- select_f (storeWord ptr b (machine_state s'));
modify (update_machine ms')
od)
 2. \<And>s' s. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2; True; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q52 s' s
 3. \<And>s' s. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2; True; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'52 s' s proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>within_page buf ptr sz; ptr && mask 2 \<noteq> 0; pspace_aligned s'; pspace_distinct s'; valid_objs s'; ipc_frame_ptr_at buf s_id s'; ipc_frame_sz_at sz s_id s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q52 s') (?Q'52 s') (corrupt_frame buf) (do (r, ms') <- \<lambda>s. (fst ((do y <- \<lambda>s. ({}, True);
modify (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit b ! 3, ptr + 1 := word_rsplit b ! 2, ptr + 2 := word_rsplit b ! Suc 0, ptr + 3 := word_rsplit b ! 0)))
od) (machine_state s')) \<times> {s}, snd ((do y <- \<lambda>s. ({}, True);
modify (underlying_memory_update (\<lambda>m. m(ptr := word_rsplit b ! 3, ptr + 1 := word_rsplit b ! 2, ptr + 2 := word_rsplit b ! Suc 0, ptr + 3 := word_rsplit b ! 0)))
od) (machine_state s')));
modify (update_machine ms')
od)
 2. \<And>s' s. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2; True; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q52 s' s
 3. \<And>s' s. \<lbrakk>within_page buf ptr sz; \<not> is_aligned ptr 2; True; (pspace_aligned and pspace_distinct and valid_objs and ipc_frame_ptr_at buf s_id and ipc_frame_sz_at sz s_id and valid_etcbs) s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'52 s' s proof (prove)
goal:
No subgoals!