kings-crown/FVELER_Isabelle huggingface dataset:
theory VSpace_C

lemma APFromVMRights_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. \<acute>vm_rights < 4\<rbrace> Call APFromVMRights_'proc
  \<lbrace> \<acute>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) \<rbrace>" apply vcg apply (simp add: vmrights_to_H_def ap_from_vm_rights_def
                   Kernel_C.VMNoAccess_def Kernel_C.VMKernelOnly_def
                   Kernel_C.VMReadOnly_def Kernel_C.VMReadWrite_def) apply clarsimp apply (drule word_less_cases, auto)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. \<acute>vm_rights < 4\<rbrace> Call APFromVMRights_'proc \<lbrace>\<acute>ret__unsigned_long = ap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>vm_rights. vm_rights < 4 \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess = vm_rights \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 0 = ap_from_vm_rights (vmrights_to_H vm_rights)) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess \<noteq> vm_rights \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly = vm_rights \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 1 = ap_from_vm_rights (vmrights_to_H vm_rights)) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMKernelOnly \<noteq> vm_rights \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly = vm_rights \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 2 = ap_from_vm_rights (vmrights_to_H vm_rights)) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadOnly \<noteq> vm_rights \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite = vm_rights \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 3 = ap_from_vm_rights (vmrights_to_H vm_rights)) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite \<noteq> vm_rights \<longrightarrow> (True \<longrightarrow> False) \<and> (\<not> True \<longrightarrow> False))))) proof (prove)
goal (1 subgoal):
 1. \<And>vm_rights. vm_rights < 4 \<Longrightarrow> vm_rights \<noteq> 0 \<longrightarrow> vm_rights \<noteq> 1 \<longrightarrow> vm_rights \<noteq> 2 \<longrightarrow> vm_rights = 3 proof (prove)
goal (1 subgoal):
 1. \<And>vm_rights. \<lbrakk>vm_rights < 4; vm_rights \<noteq> 0; vm_rights \<noteq> 1; vm_rights \<noteq> 2\<rbrakk> \<Longrightarrow> vm_rights = 3 proof (prove)
goal:
No subgoals!
theory VSpace_C

lemma ap_from_vm_rights_mask:
  "ap_from_vm_rights R && 3 = (ap_from_vm_rights R :: word32)" by (simp add: ap_from_vm_rights_def split: vmrights.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ap_from_vm_rights R && 3 = ap_from_vm_rights R
theory VSpace_C

lemma vmAttributesFromWord_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. True\<rbrace> Call vmAttributesFromWord_'proc
  \<lbrace> vm_attributes_lift \<acute>ret__struct_vm_attributes_C =
      \<lparr>  armExecuteNever_CL =  (\<^bsup>s\<^esup>w >> 2) && 1,
        armParityEnabled_CL = (\<^bsup>s\<^esup>w >> 1) && 1,
        armPageCacheable_CL = \<^bsup>s\<^esup>w && 1 \<rparr>  \<rbrace>" by (vcg, simp add: vm_attributes_lift_def word_sless_def word_sle_def mask_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. True\<rbrace> Call vmAttributesFromWord_'proc \<lbrace>vm_attributes_lift \<acute>ret__struct_vm_attributes_C = \<lparr>armExecuteNever_CL = (\<^bsup>s\<^esup>w >> 2) && 1, armParityEnabled_CL = (\<^bsup>s\<^esup>w >> 1) && 1, armPageCacheable_CL = \<^bsup>s\<^esup>w && 1\<rparr>\<rbrace>
theory VSpace_C

lemma cap_to_H_PDCap:
  "cap_to_H cap = ArchObjectCap (PageDirectoryCap p asid) \<Longrightarrow>
  \<exists>cap_CL. cap = Cap_page_directory_cap cap_CL \<and>
           to_bool (capPDIsMapped_CL cap_CL) = (asid \<noteq> None) \<and>
           (asid \<noteq> None \<longrightarrow> capPDMappedASID_CL cap_CL = the asid) \<and>
           capPDBasePtr_CL cap_CL = p" by (auto simp add: cap_to_H_def Let_def split: cap_CL.splits if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_to_H cap = capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid) \<Longrightarrow> \<exists>cap_CL. cap = Cap_page_directory_cap cap_CL \<and> to_bool (capPDIsMapped_CL cap_CL) = (asid \<noteq> None) \<and> (asid \<noteq> None \<longrightarrow> capPDMappedASID_CL cap_CL = the asid) \<and> capPDBasePtr_CL cap_CL = p
theory VSpace_C

lemma cap_lift_PDCap_Base:
  "\<lbrakk> cap_to_H cap_cl = ArchObjectCap (PageDirectoryCap p asid);
     cap_lift cap_c = Some cap_cl \<rbrakk>
  \<Longrightarrow> p = capPDBasePtr_CL (cap_page_directory_cap_lift cap_c)" apply (simp add: cap_page_directory_cap_lift_def) apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_to_H cap_cl = capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid); cap_lift cap_c = Some cap_cl\<rbrakk> \<Longrightarrow> p = capPDBasePtr_CL (cap_page_directory_cap_lift cap_c) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_to_H cap_cl = capability.ArchObjectCap (arch_capability.PageDirectoryCap p asid); cap_lift cap_c = Some cap_cl\<rbrakk> \<Longrightarrow> p = capPDBasePtr_CL (case cap_cl of Cap_page_directory_cap rec \<Rightarrow> rec) proof (prove)
goal:
No subgoals!
theory StoreWord_C

lemma in_doMachineOp:
  "(a, s) \<in> fst (doMachineOp f s') = (\<exists>b. (a, b) \<in> fst (f (ksMachineState s')) \<and> s = s'\<lparr>ksMachineState := b\<rparr>)" unfolding doMachineOp_def by (simp add: in_monad select_f_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((a, s) \<in> fst (doMachineOp f s')) = (\<exists>b. (a, b) \<in> fst (f (ksMachineState s')) \<and> s = s'\<lparr>ksMachineState := b\<rparr>) proof (prove)
goal (1 subgoal):
 1. ((a, s) \<in> fst ((do ms <- gets ksMachineState;
(r, ms') <- select_f (f ms);
modify (ksMachineState_update (\<lambda>_. ms'));
return r
od) s')) = (\<exists>b. (a, b) \<in> fst (f (ksMachineState s')) \<and> s = s'\<lparr>ksMachineState := b\<rparr>)
theory StoreWord_C

lemma dom_heap_to_user_data:
  "dom (heap_to_user_data hp uhp) = dom (map_to_user_data hp)" unfolding heap_to_user_data_def by (simp add: Let_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (heap_to_user_data hp uhp) = dom (map_to_user_data hp) proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>p. let uhpa = map_to_user_data hp in map_option (\<lambda>_. byte_to_word_heap uhp p) (uhpa p)) = dom (map_to_user_data hp)
theory StoreWord_C

lemma byte_to_word_heap_upd_outside_range:
  "p \<notin> {(base + ucast off * 4)..+4} \<Longrightarrow>
   byte_to_word_heap (m (p := v')) base off = byte_to_word_heap m base off" apply (simp add: byte_to_word_heap_def Let_def) apply (erule contrapos_np) apply (clarsimp intro!: intvl_inter_le [where k=0 and ka=3, simplified, OF refl]
                          intvl_inter_le [where k=0 and ka=2, simplified, OF refl]
                          intvl_inter_le [where k=0 and ka=1, simplified, OF refl]
                          intvl_inter_le [where k=0 and ka=0, simplified, OF refl]
                   split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p \<notin> {base + UCAST(10 \<rightarrow> 32) off * 4..+4} \<Longrightarrow> byte_to_word_heap (m(p := v')) base off = byte_to_word_heap m base off proof (prove)
goal (1 subgoal):
 1. p \<notin> {base + UCAST(10 \<rightarrow> 32) off * 4..+4} \<Longrightarrow> word_rcat [if base + UCAST(10 \<rightarrow> 32) off * 4 + 3 = p then v' else m (base + UCAST(10 \<rightarrow> 32) off * 4 + 3), if base + UCAST(10 \<rightarrow> 32) off * 4 + 2 = p then v' else m (base + UCAST(10 \<rightarrow> 32) off * 4 + 2), if base + UCAST(10 \<rightarrow> 32) off * 4 + 1 = p then v' else m (base + UCAST(10 \<rightarrow> 32) off * 4 + 1), if base + UCAST(10 \<rightarrow> 32) off * 4 = p then v' else m (base + UCAST(10 \<rightarrow> 32) off * 4)] = word_rcat [m (base + UCAST(10 \<rightarrow> 32) off * 4 + 3), m (base + UCAST(10 \<rightarrow> 32) off * 4 + 2), m (base + UCAST(10 \<rightarrow> 32) off * 4 + 1), m (base + UCAST(10 \<rightarrow> 32) off * 4)] proof (prove)
goal (1 subgoal):
 1. word_rcat [if base + UCAST(10 \<rightarrow> 32) off * 4 + 3 = p then v' else m (base + UCAST(10 \<rightarrow> 32) off * 4 + 3), if base + UCAST(10 \<rightarrow> 32) off * 4 + 2 = p then v' else m (base + UCAST(10 \<rightarrow> 32) off * 4 + 2), if base + UCAST(10 \<rightarrow> 32) off * 4 + 1 = p then v' else m (base + UCAST(10 \<rightarrow> 32) off * 4 + 1), if base + UCAST(10 \<rightarrow> 32) off * 4 = p then v' else m (base + UCAST(10 \<rightarrow> 32) off * 4)] \<noteq> word_rcat [m (base + UCAST(10 \<rightarrow> 32) off * 4 + 3), m (base + UCAST(10 \<rightarrow> 32) off * 4 + 2), m (base + UCAST(10 \<rightarrow> 32) off * 4 + 1), m (base + UCAST(10 \<rightarrow> 32) off * 4)] \<Longrightarrow> p \<in> {base + UCAST(10 \<rightarrow> 32) off * 4..+4} proof (prove)
goal:
No subgoals!
theory StoreWord_C

lemma intvl_range_conv:
  "\<lbrakk> is_aligned (ptr :: 'a :: len word) bits; bits < len_of TYPE('a) \<rbrakk> \<Longrightarrow>
   {ptr ..+ 2 ^ bits} = {ptr .. ptr + 2 ^ bits - 1}" by (rule upto_intvl_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr bits; bits < LENGTH('a)\<rbrakk> \<Longrightarrow> {ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}
theory StoreWord_C

lemma nat_less_4_cases:
  "i < (4::nat) ==> i = 0 | i = 1 | i = 2 | i = 3" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. i < 4 \<Longrightarrow> i = 0 \<or> i = 1 \<or> i = 2 \<or> i = 3
theory StoreWord_C

lemma user_data_device_relation_upd:
  assumes al: "is_aligned ptr 2"
  shows "cuser_user_data_device_relation
            (byte_to_word_heap
              (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits))
            (the (cslift s (Ptr (ptr && ~~ mask pageBits)))) \<Longrightarrow>
     cuser_user_data_device_relation
            (byte_to_word_heap
              ((underlying_memory (ksMachineState \<sigma>))
               (ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2,
                ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0))
              (ptr && ~~ mask pageBits))
            (user_data_device_C.words_C_update
              (\<lambda>ws. Arrays.update ws (unat (ucast ((ptr && mask pageBits) >> 2):: 10 word)) w)
              (the (cslift s (Ptr (ptr && ~~ mask pageBits)))))" by (simp add:cuser_user_data_device_relation_def )

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cuser_user_data_device_relation (byte_to_word_heap (underlying_memory (ksMachineState \<sigma>)) (ptr && ~~ mask pageBits)) (the (cslift s (PTR(user_data_device_C) (ptr && ~~ mask pageBits)))) \<Longrightarrow> cuser_user_data_device_relation (byte_to_word_heap ((underlying_memory (ksMachineState \<sigma>))(ptr := word_rsplit w ! 3, ptr + 1 := word_rsplit w ! 2, ptr + 2 := word_rsplit w ! Suc 0, ptr + 3 := word_rsplit w ! 0)) (ptr && ~~ mask pageBits)) (user_data_device_C.words_C_update (\<lambda>ws. Arrays.update ws (unat (UCAST(32 \<rightarrow> 10) (ptr && mask pageBits >> 2))) w) (the (cslift s (PTR(user_data_device_C) (ptr && ~~ mask pageBits)))))
theory StoreWord_C

lemma deviceDataSeperate:
  "\<lbrakk>\<not> pointerInDeviceData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserDataDevice\<rbrakk>
  \<Longrightarrow> ptr \<noteq> x" apply (rule ccontr,clarsimp) apply (frule(1) pspace_alignedD') apply (clarsimp simp: pointerInDeviceData_def objBits_simps typ_at'_def ko_wp_at'_def) apply (frule(1) pspace_distinctD') apply (clarsimp simp: objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInDeviceData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserDataDevice\<rbrakk> \<Longrightarrow> ptr \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInDeviceData x \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserDataDevice; ptr = x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInDeviceData x \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserDataDevice; ptr = x; is_aligned x (objBitsKO KOUserDataDevice)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> ps_clear x pageBits \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserDataDevice; ptr = x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> ps_clear x pageBits \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserDataDevice; ptr = x; is_aligned x pageBits; ps_clear x (objBitsKO KOUserDataDevice) \<sigma>\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory StoreWord_C

lemma userDataSeperate:
  "\<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData\<rbrakk>
  \<Longrightarrow> ptr \<noteq> x" apply (rule ccontr,clarsimp) apply (frule(1) pspace_alignedD') apply (clarsimp simp: pointerInUserData_def objBits_simps typ_at'_def ko_wp_at'_def) apply (frule(1) pspace_distinctD') apply (clarsimp simp: objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInUserData ptr \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData\<rbrakk> \<Longrightarrow> ptr \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInUserData x \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr = x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> pointerInUserData x \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr = x; is_aligned x (objBitsKO KOUserData)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> ps_clear x pageBits \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr = x; is_aligned x pageBits\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> ps_clear x pageBits \<sigma>; pspace_distinct' \<sigma>; pspace_aligned' \<sigma>; ksPSpace \<sigma> x = Some KOUserData; ptr = x; is_aligned x pageBits; ps_clear x (objBitsKO KOUserData) \<sigma>\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory StoreWord_C

lemma pointerInUserData_whole_word[simp]:
  "\<lbrakk>is_aligned ptr 2;  n < 4\<rbrakk> \<Longrightarrow> pointerInUserData (ptr + n) \<sigma> = pointerInUserData ptr \<sigma>" apply (simp add:pointerInUserData_def pageBits_def) apply (subst and_not_mask_twice[symmetric,where m = 12 and n =2,simplified]) apply (simp add: neg_mask_add_aligned[where n=2,simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; n < 4\<rbrakk> \<Longrightarrow> pointerInUserData (ptr + n) \<sigma> = pointerInUserData ptr \<sigma> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; n < 4\<rbrakk> \<Longrightarrow> typ_at' UserDataT (ptr + n && ~~ mask 12) \<sigma> = typ_at' UserDataT (ptr && ~~ mask 12) \<sigma> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; n < 4\<rbrakk> \<Longrightarrow> typ_at' UserDataT ((ptr + n && ~~ mask 2) && ~~ mask 12) \<sigma> = typ_at' UserDataT (ptr && ~~ mask 12) \<sigma> proof (prove)
goal:
No subgoals!
theory StoreWord_C

lemma pointerInDeviceData_whole_word[simp]:
  "\<lbrakk>is_aligned ptr 2;  n < 4\<rbrakk> \<Longrightarrow> pointerInDeviceData (ptr + n) \<sigma> = pointerInDeviceData ptr \<sigma>" apply (simp add:pointerInDeviceData_def pageBits_def) apply (subst and_not_mask_twice[symmetric,where m = 12 and n =2,simplified]) apply (simp add: neg_mask_add_aligned[where n=2,simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; n < 4\<rbrakk> \<Longrightarrow> pointerInDeviceData (ptr + n) \<sigma> = pointerInDeviceData ptr \<sigma> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; n < 4\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT (ptr + n && ~~ mask 12) \<sigma> = typ_at' UserDataDeviceT (ptr && ~~ mask 12) \<sigma> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr 2; n < 4\<rbrakk> \<Longrightarrow> typ_at' UserDataDeviceT ((ptr + n && ~~ mask 2) && ~~ mask 12) \<sigma> = typ_at' UserDataDeviceT (ptr && ~~ mask 12) \<sigma> proof (prove)
goal:
No subgoals!
theory StoreWord_C

lemma du_ptr_disjoint:
 "pointerInDeviceData ptr \<sigma> \<Longrightarrow> \<not> pointerInUserData ptr \<sigma>"
 "pointerInUserData ptr \<sigma> \<Longrightarrow> \<not> pointerInDeviceData ptr \<sigma>" by (auto simp: pointerInDeviceData_def pointerInUserData_def typ_at'_def ko_wp_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pointerInDeviceData ptr \<sigma> \<Longrightarrow> \<not> pointerInUserData ptr \<sigma>) &&& (pointerInUserData ptr \<sigma> \<Longrightarrow> \<not> pointerInDeviceData ptr \<sigma>)
theory StoreWord_C

lemma storeWord_ccorres:
  "ccorres dc xfdc
     (valid_pspace' and K (is_aligned ptr 2) and pointerInUserData ptr)
     (UNIV \<inter> {s. ptr' s = Ptr ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val}) hs
     (doMachineOp $ storeWord ptr val)
     (Basic (\<lambda>s. globals_update (t_hrs_'_update
           (hrs_mem_update (heap_update (ptr' s) (val' s)))) s))" apply (rule ccorres_guard_imp2, rule storeWord_ccorres') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_pspace' and K (is_aligned ptr 2) and pointerInUserData ptr) (UNIV \<inter> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val}) hs (doMachineOp $ storeWord ptr val) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update \<acute>ptr' \<acute>val'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_pspace' and K (is_aligned ptr 2) and pointerInUserData ptr) s; s' \<in> UNIV \<inter> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val}\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and K (is_aligned ptr 2) and (\<lambda>s. pointerInUserData ptr s \<or> pointerInDeviceData ptr s)) s \<and> s' \<in> UNIV \<inter> {s. ptr' s = PTR(32 word) ptr} \<inter> {s. c_guard (ptr' s)} \<inter> {s. val' s = val} proof (prove)
goal:
No subgoals!
theory StoreWord_C

lemma pointerInUserData_h_t_valid:
  "\<lbrakk> valid_pspace' s; pointerInUserData ptr s ;
       is_aligned ptr 2; (s, s') \<in> rf_sr \<rbrakk>
      \<Longrightarrow> hrs_htd (t_hrs_' (globals s')) \<Turnstile>\<^sub>t (Ptr ptr :: word32 ptr)" apply (frule_tac p=ptr in
     user_word_at_cross_over[rotated, OF _ refl]) apply (simp add: user_word_at_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; pointerInUserData ptr s; is_aligned ptr 2; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c PTR(32 word) ptr proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_pspace' s; pointerInUserData ptr s; is_aligned ptr 2; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> user_word_at ?x ptr s
 2. \<lbrakk>valid_pspace' s; pointerInUserData ptr s; is_aligned ptr 2; (s, s') \<in> rf_sr; c_guard (PTR(32 word) ptr) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) ptr \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) ptr) = ?x\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c PTR(32 word) ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' s; pointerInUserData ptr s; is_aligned ptr 2; (s, s') \<in> rf_sr; c_guard (PTR(32 word) ptr) \<and> s' \<Turnstile>\<^sub>c PTR(32 word) ptr \<and> h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(32 word) ptr) = word_rcat [underlying_memory (ksMachineState s) (ptr + 3), underlying_memory (ksMachineState s) (ptr + 2), underlying_memory (ksMachineState s) (ptr + 1), underlying_memory (ksMachineState s) ptr]\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c PTR(32 word) ptr proof (prove)
goal:
No subgoals!
theory DetWP

lemma det_wp_doMachineOp [wp]:
  "det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (\<lambda>_. P) (doMachineOp f)" apply (simp add: doMachineOp_def split_def) apply (rule det_wp_pre, wp) apply (erule det_wp_select_f) apply wp+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (\<lambda>_. P) (doMachineOp f) proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (\<lambda>_. P) (do ms <- gets ksMachineState;
p <- select_f (f ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od) proof (prove)
goal (5 subgoals):
 1. \<And>ms. det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (?P6 ms) (select_f (f ms))
 2. \<And>ms p. det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (?Q6 ms p) (do y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od)
 3. \<And>ms. det_wp (\<lambda>_. P) f \<Longrightarrow> \<lbrace>?P'6 ms\<rbrace> select_f (f ms) \<lbrace>?Q6 ms\<rbrace>
 4. det_wp (\<lambda>_. P) f \<Longrightarrow> \<lbrace>?P'4\<rbrace> gets ksMachineState \<lbrace>\<lambda>ms. ?P6 ms and ?P'6 ms\<rbrace>
 5. \<And>s. \<lbrakk>det_wp (\<lambda>_. P) f; P\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?P'4) s proof (prove)
goal (4 subgoals):
 1. \<And>ms p. det_wp (\<lambda>_. P) f \<Longrightarrow> det_wp (?Q6 ms p) (do y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od)
 2. \<And>ms. det_wp (\<lambda>_. P) f \<Longrightarrow> \<lbrace>?P'6 ms\<rbrace> select_f (f ms) \<lbrace>?Q6 ms\<rbrace>
 3. det_wp (\<lambda>_. P) f \<Longrightarrow> \<lbrace>?P'4\<rbrace> gets ksMachineState \<lbrace>\<lambda>ms. (\<lambda>_. P) and ?P'6 ms\<rbrace>
 4. \<And>s. \<lbrakk>det_wp (\<lambda>_. P) f; P\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?P'4) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>det_wp (\<lambda>_. P) f; P\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. P) and (\<lambda>sa. \<forall>x\<in>fst (f (ksMachineState s)). ((\<lambda>_. True) and (\<lambda>s. True)) sa)) s)) s proof (prove)
goal:
No subgoals!