theory Retype_C

lemma Arch_createObject_preserves_bytes:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call Arch_createObject_'proc
      {t. \<forall>nt. t_' s = object_type_from_H nt
         \<longrightarrow> (\<forall>x \<in> - {ptr_val (regionBase_' s) ..+ 2 ^ getObjectSize nt (unat (userSize_' s))}.
             hrs_htd (t_hrs_' (globals t)) x = hrs_htd (t_hrs_' (globals s)) x)
         \<and> byte_regions_unmodified' t s}" apply (hoare_rule HoarePartial.ProcNoRec1) apply clarsimp apply (rule conseqPre, vcg exspec=cap_small_frame_cap_new_modifies
                             exspec=cap_frame_cap_new_modifies
                             exspec=cap_page_table_cap_new_modifies
                             exspec=copyGlobalMappings_preserves_bytes
                             exspec=addrFromPPtr_modifies
                             exspec=cleanCacheRange_PoU_preserves_bytes
                             exspec=cap_page_directory_cap_new_modifies) apply (safe intro!: byte_regions_unmodified_hrs_mem_update,
         (simp_all add: h_t_valid_field hrs_htd_update)+) apply (safe intro!: ptr_retyp_d ptr_retyps_out) apply (simp_all add: object_type_from_H_def Kernel_C_defs APIType_capBits_def
                            split: object_type.split_asm apiobject_type.split_asm) apply (rule byte_regions_unmodified_flip, simp) apply (rule byte_regions_unmodified_trans[rotated],
         assumption, simp_all add: hrs_htd_update_canon hrs_htd_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call Arch_createObject_'proc \<lbrace>\<forall>nt. \<^bsup>s\<^esup>t = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val \<^bsup>s\<^esup>regionBase..+2 ^ getObjectSize nt (unat \<^bsup>s\<^esup>userSize)}. hrs_htd \<acute>t_hrs x = hrs_htd \<^bsup>s\<^esup>t_hrs x) \<and> byte_regions_unmodified \<acute>t_hrs \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} TRY
   SWITCH \<acute>t {SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject}\<Rightarrow> IF \<acute>deviceMemory \<noteq> 0 THEN
  Guard MemorySafety \<lbrace>fst (True, ptr_retyps 1 (PTR(user_data_device_C) (ptr_val \<acute>regionBase)))\<rbrace> (Guard MemorySafety {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (globals_update (t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(user_data_device_C) (ptr_val \<acute>regionBase)))))));;
Guard GhostStateError \<lbrace>fst (True, gs_new_frames Wellformed_C.ARMSmallPage (ptr_val \<acute>regionBase) (unat ARMSmallPageBits))\<rbrace> (\<acute>globals :== ghost'state_'_update (snd (True, gs_new_frames Wellformed_C.ARMSmallPage (ptr_val \<acute>regionBase) (unat ARMSmallPageBits))))
ELSE
  Guard MemorySafety \<lbrace>fst (True, ptr_retyps 1 (PTR(user_data_C) (ptr_val \<acute>regionBase)))\<rbrace> (Guard MemorySafety {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (globals_update (t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(user_data_C) (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(user_data_C) (ptr_val \<acute>regionBase)))))));;
Guard GhostStateError \<lbrace>fst (True, gs_new_frames Wellformed_C.ARMSmallPage (ptr_val \<acute>regionBase) (unat ARMSmallPageBits))\<rbrace> (\<acute>globals :== ghost'state_'_update (snd (True, gs_new_frames Wellformed_C.ARMSmallPage (ptr_val \<acute>regionBase) (unat ARMSmallPageBits))))
FI;;
Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidHighBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidHighBits <s 0x20\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s asidInvalid\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (\<acute>ret__struct_cap_C :== CALL cap_small_frame_cap_new_'proc(UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1),SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) (if \<not> \<not> \<acute>deviceMemory \<noteq> 0 then 1 else 0),UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1),UCAST(32 \<rightarrow> 32) (ptr_val \<acute>regionBase)))))))));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_' | {SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject}\<Rightarrow> IF \<acute>deviceMemory \<noteq> 0 THEN
  Guard MemorySafety \<lbrace>fst (True, ptr_retyps 16 (PTR(user_data_device_C) (ptr_val \<acute>regionBase)))\<rbrace> (Guard MemorySafety {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (globals_update (t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 16 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 16 (PTR(user_data_device_C) (ptr_val \<acute>regionBase)))))));;
Guard GhostStateError \<lbrace>fst (True, gs_new_frames Wellformed_C.ARMLargePage (ptr_val \<acute>regionBase) (unat ARMLargePageBits))\<rbrace> (\<acute>globals :== ghost'state_'_update (snd (True, gs_new_frames Wellformed_C.ARMLargePage (ptr_val \<acute>regionBase) (unat ARMLargePageBits))))
ELSE
  Guard MemorySafety \<lbrace>fst (True, ptr_retyps 16 (PTR(user_data_C) (ptr_val \<acute>regionBase)))\<rbrace> (Guard MemorySafety {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (globals_update (t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 16 (PTR(user_data_C) (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 16 (PTR(user_data_C) (ptr_val \<acute>regionBase)))))));;
Guard GhostStateError \<lbrace>fst (True, gs_new_frames Wellformed_C.ARMLargePage (ptr_val \<acute>regionBase) (unat ARMLargePageBits))\<rbrace> (\<acute>globals :== ghost'state_'_update (snd (True, gs_new_frames Wellformed_C.ARMLargePage (ptr_val \<acute>regionBase) (unat ARMLargePageBits))))
FI;;
Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidHighBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidHighBits <s 0x20\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s asidInvalid\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (\<acute>ret__struct_cap_C :== CALL cap_frame_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage,UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1),SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) (if \<not> \<not> \<acute>deviceMemory \<noteq> 0 then 1 else 0),UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1),UCAST(32 \<rightarrow> 32) (ptr_val \<acute>regionBase)))))))));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_' | {SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject}\<Rightarrow> IF \<acute>deviceMemory \<noteq> 0 THEN
  Guard MemorySafety \<lbrace>fst (True, ptr_retyps 256 (PTR(user_data_device_C) (ptr_val \<acute>regionBase)))\<rbrace> (Guard MemorySafety {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (globals_update (t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 256 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 256 (PTR(user_data_device_C) (ptr_val \<acute>regionBase)))))));;
Guard GhostStateError \<lbrace>fst (True, gs_new_frames Wellformed_C.ARMSection (ptr_val \<acute>regionBase) (unat ARMSectionBits))\<rbrace> (\<acute>globals :== ghost'state_'_update (snd (True, gs_new_frames Wellformed_C.ARMSection (ptr_val \<acute>regionBase) (unat ARMSectionBits))))
ELSE
  Guard MemorySafety \<lbrace>fst (True, ptr_retyps 256 (PTR(user_data_C) (ptr_val \<acute>regionBase)))\<rbrace> (Guard MemorySafety {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (globals_update (t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 256 (PTR(user_data_C) (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 256 (PTR(user_data_C) (ptr_val \<acute>regionBase)))))));;
Guard GhostStateError \<lbrace>fst (True, gs_new_frames Wellformed_C.ARMSection (ptr_val \<acute>regionBase) (unat ARMSectionBits))\<rbrace> (\<acute>globals :== ghost'state_'_update (snd (True, gs_new_frames Wellformed_C.ARMSection (ptr_val \<acute>regionBase) (unat ARMSectionBits))))
FI;;
Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidHighBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidHighBits <s 0x20\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s asidInvalid\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (\<acute>ret__struct_cap_C :== CALL cap_frame_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection,UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1),SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) (if \<not> \<not> \<acute>deviceMemory \<noteq> 0 then 1 else 0),UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1),UCAST(32 \<rightarrow> 32) (ptr_val \<acute>regionBase)))))))));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_' | {SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject}\<Rightarrow> IF \<acute>deviceMemory \<noteq> 0 THEN
  Guard MemorySafety \<lbrace>fst (True, ptr_retyps 4096 (PTR(user_data_device_C) (ptr_val \<acute>regionBase)))\<rbrace> (Guard MemorySafety {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (globals_update (t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 4096 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 4096 (PTR(user_data_device_C) (ptr_val \<acute>regionBase)))))));;
Guard GhostStateError \<lbrace>fst (True, gs_new_frames Wellformed_C.ARMSuperSection (ptr_val \<acute>regionBase) (unat ARMSuperSectionBits))\<rbrace> (\<acute>globals :== ghost'state_'_update (snd (True, gs_new_frames Wellformed_C.ARMSuperSection (ptr_val \<acute>regionBase) (unat ARMSuperSectionBits))))
ELSE
  Guard MemorySafety \<lbrace>fst (True, ptr_retyps 4096 (PTR(user_data_C) (ptr_val \<acute>regionBase)))\<rbrace> (Guard MemorySafety {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (globals_update (t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 4096 (PTR(user_data_C) (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 4096 (PTR(user_data_C) (ptr_val \<acute>regionBase)))))));;
Guard GhostStateError \<lbrace>fst (True, gs_new_frames Wellformed_C.ARMSuperSection (ptr_val \<acute>regionBase) (unat ARMSuperSectionBits))\<rbrace> (\<acute>globals :== ghost'state_'_update (snd (True, gs_new_frames Wellformed_C.ARMSuperSection (ptr_val \<acute>regionBase) (unat ARMSuperSectionBits))))
FI;;
Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidHighBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidHighBits <s 0x20\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s asidInvalid\<rbrace> (Guard ShiftError \<lbrace>0 \<le>s Kernel_C.asidLowBits\<rbrace> (Guard ShiftError \<lbrace>Kernel_C.asidLowBits <s 0x20\<rbrace> (\<acute>ret__struct_cap_C :== CALL cap_frame_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection,UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1),SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite,SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) (if \<not> \<not> \<acute>deviceMemory \<noteq> 0 then 1 else 0),UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1),UCAST(32 \<rightarrow> 32) (ptr_val \<acute>regionBase)))))))));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_' | {SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject}\<Rightarrow> Guard MemorySafety \<lbrace>fst (True, ptr_retyps 1 (pt_Ptr (ptr_val \<acute>regionBase)))\<rbrace> (Guard MemorySafety {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (globals_update (t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 1 (pt_Ptr (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 1 (pt_Ptr (ptr_val \<acute>regionBase)))))));;
\<acute>ret__struct_cap_C :== CALL cap_page_table_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) asidInvalid,SCAST(32 signed \<rightarrow> 32) 0,UCAST(32 \<rightarrow> 32) (ptr_val \<acute>regionBase));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_' | {SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject}\<Rightarrow> Guard MemorySafety \<lbrace>fst (True, ptr_retyps 1 (pd_Ptr (ptr_val \<acute>regionBase)))\<rbrace> (Guard MemorySafety {s. htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (t_hrs_' (globals (globals_update (t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 1 (pd_Ptr (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 1 (pd_Ptr (ptr_val \<acute>regionBase)))))));;
CALL copyGlobalMappings_'proc(PTR_COERCE(unit \<rightarrow> pde_C) \<acute>regionBase);;
\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(\<acute>regionBase);;
Guard ShiftError \<lbrace>0 \<le>s 0xC + 2\<rbrace> (Guard ShiftError \<lbrace>unat 1 * 2 ^ unat (0xC + 2) < 2 ^ 31 \<and> 0 \<le>s 1\<rbrace> (Guard SignedArithmetic \<lbrace>- 2147483648 \<le> sint 0xC + sint 2 \<and> sint 0xC + sint 2 \<le> 2147483647\<rbrace> (CALL cleanCacheRange_PoU_'proc(ptr_val \<acute>regionBase,ptr_val \<acute>regionBase + SCAST(32 signed \<rightarrow> 32) (1 << unat (0xC + 2)) - SCAST(32 signed \<rightarrow> 32) 1,\<acute>ret__unsigned_long))));;
\<acute>ret__struct_cap_C :== CALL cap_page_directory_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) asidInvalid,UCAST(32 \<rightarrow> 32) (ptr_val \<acute>regionBase));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_' | UNIV\<Rightarrow> Guard DontReach {} (CALL halt_'proc();;
Guard DontReach {} SKIP) END;;
Guard DontReach {} SKIP
CATCH SKIP
END \<lbrace>\<forall>nt. \<^bsup>s\<^esup>t = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val \<^bsup>s\<^esup>regionBase..+2 ^ getObjectSize nt (unat \<^bsup>s\<^esup>userSize)}. hrs_htd \<acute>t_hrs x = hrs_htd \<^bsup>s\<^esup>t_hrs x) \<and> byte_regions_unmodified \<acute>t_hrs \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} TRY
  IF \<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject THEN
  IF \<acute>deviceMemory \<noteq> 0 THEN
  Guard MemorySafety UNIV (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) \<acute>regionBase)))));;
Guard GhostStateError UNIV (\<acute>globals :== ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val \<acute>regionBase) (unat ARMSmallPageBits)))
ELSE
  Guard MemorySafety UNIV (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) \<acute>regionBase)))));;
Guard GhostStateError UNIV (\<acute>globals :== ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val \<acute>regionBase) (unat ARMSmallPageBits)))
FI;;
Guard ShiftError (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) (Guard ShiftError (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) (Guard ShiftError (if 0 \<le>s asidInvalid then UNIV else {}) (Guard ShiftError (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) (\<acute>ret__struct_cap_C :== CALL cap_small_frame_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) asidInvalid && 2 ^ local.asid_low_bits - 1,SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite,0,if \<acute>deviceMemory \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) (asidInvalid >> local.asid_low_bits) && 2 ^ unat Kernel_C.asidHighBits - 1,ptr_val \<acute>regionBase))))))));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_'
ELSE
  IF \<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject THEN
  IF \<acute>deviceMemory \<noteq> 0 THEN
  Guard MemorySafety UNIV (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) \<acute>regionBase)))));;
Guard GhostStateError UNIV (\<acute>globals :== ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val \<acute>regionBase) (unat ARMLargePageBits)))
ELSE
  Guard MemorySafety UNIV (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) \<acute>regionBase)))));;
Guard GhostStateError UNIV (\<acute>globals :== ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val \<acute>regionBase) (unat ARMLargePageBits)))
FI;;
Guard ShiftError (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) (Guard ShiftError (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) (Guard ShiftError (if 0 \<le>s asidInvalid then UNIV else {}) (Guard ShiftError (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) (\<acute>ret__struct_cap_C :== CALL cap_frame_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage,SCAST(32 signed \<rightarrow> 32) asidInvalid && 2 ^ local.asid_low_bits - 1,SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite,0,if \<acute>deviceMemory \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) (asidInvalid >> local.asid_low_bits) && 2 ^ unat Kernel_C.asidHighBits - 1,ptr_val \<acute>regionBase))))))));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_'
ELSE
  IF \<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject THEN
  IF \<acute>deviceMemory \<noteq> 0 THEN
  Guard MemorySafety UNIV (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) \<acute>regionBase)))));;
Guard GhostStateError UNIV (\<acute>globals :== ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val \<acute>regionBase) (unat ARMSectionBits)))
ELSE
  Guard MemorySafety UNIV (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) \<acute>regionBase)))));;
Guard GhostStateError UNIV (\<acute>globals :== ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val \<acute>regionBase) (unat ARMSectionBits)))
FI;;
Guard ShiftError (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) (Guard ShiftError (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) (Guard ShiftError (if 0 \<le>s asidInvalid then UNIV else {}) (Guard ShiftError (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) (\<acute>ret__struct_cap_C :== CALL cap_frame_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection,SCAST(32 signed \<rightarrow> 32) asidInvalid && 2 ^ local.asid_low_bits - 1,SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite,0,if \<acute>deviceMemory \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) (asidInvalid >> local.asid_low_bits) && 2 ^ unat Kernel_C.asidHighBits - 1,ptr_val \<acute>regionBase))))))));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_'
ELSE
  IF \<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject THEN
  IF \<acute>deviceMemory \<noteq> 0 THEN
  Guard MemorySafety UNIV (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) \<acute>regionBase)))));;
Guard GhostStateError UNIV (\<acute>globals :== ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val \<acute>regionBase) (unat ARMSuperSectionBits)))
ELSE
  Guard MemorySafety UNIV (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) \<acute>regionBase)))));;
Guard GhostStateError UNIV (\<acute>globals :== ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val \<acute>regionBase) (unat ARMSuperSectionBits)))
FI;;
Guard ShiftError (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) (Guard ShiftError (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) (Guard ShiftError (if 0 \<le>s asidInvalid then UNIV else {}) (Guard ShiftError (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) (Guard ShiftError (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) (\<acute>ret__struct_cap_C :== CALL cap_frame_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection,SCAST(32 signed \<rightarrow> 32) asidInvalid && 2 ^ local.asid_low_bits - 1,SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite,0,if \<acute>deviceMemory \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) (asidInvalid >> local.asid_low_bits) && 2 ^ unat Kernel_C.asidHighBits - 1,ptr_val \<acute>regionBase))))))));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_'
ELSE
  IF \<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject THEN
  Guard MemorySafety UNIV (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pte_C[256]) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pte_C[256]) \<acute>regionBase)))));;
\<acute>ret__struct_cap_C :== CALL cap_page_table_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) asidInvalid,0,ptr_val \<acute>regionBase);;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_'
ELSE
  IF \<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject THEN
  Guard MemorySafety UNIV (Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) \<acute>regionBase)))));;
CALL copyGlobalMappings_'proc(PTR_COERCE(unit \<rightarrow> pde_C) \<acute>regionBase);;
\<acute>ret__unsigned_long :== CALL addrFromPPtr_'proc(\<acute>regionBase);;
Guard ShiftError UNIV (Guard ShiftError UNIV (Guard SignedArithmetic UNIV (CALL cleanCacheRange_PoU_'proc(ptr_val \<acute>regionBase,0x3FFF + ptr_val \<acute>regionBase,\<acute>ret__unsigned_long))));;
\<acute>ret__struct_cap_C :== CALL cap_page_directory_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) false,SCAST(32 signed \<rightarrow> 32) asidInvalid,ptr_val \<acute>regionBase);;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_'
ELSE
  Cond UNIV (Guard DontReach {} (CALL halt_'proc();;
Guard DontReach {} SKIP)) SKIP
FI
FI
FI
FI
FI
FI;;
Guard DontReach {} SKIP
CATCH SKIP
END \<lbrace>\<forall>nt. \<^bsup>s\<^esup>t = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val \<^bsup>s\<^esup>regionBase..+2 ^ APIType_capBits nt (unat \<^bsup>s\<^esup>userSize)}. hrs_htd \<acute>t_hrs x = hrs_htd \<^bsup>s\<^esup>t_hrs x) \<and> byte_regions_unmodified \<acute>t_hrs \<^bsup>s\<^esup>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> {sa. (t_' sa = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<longrightarrow> (deviceMemory_' sa \<noteq> 0 \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals sa))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa)))) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' sa)) (unat ARMSmallPageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' sa)) (unat ARMSmallPageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' sa)) (unat ARMSmallPageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' sa)) (unat ARMSmallPageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' sa)) (unat ARMSmallPageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s asidInvalid then UNIV else {}) \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa))) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa))) (t_hrs_' (globals s)))) \<and> (\<not> deviceMemory_' sa \<noteq> 0 \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals sa))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa)))) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' sa)) (unat ARMSmallPageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' sa)) (unat ARMSmallPageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' sa)) (unat ARMSmallPageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' sa)) (unat ARMSmallPageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' sa)) (unat ARMSmallPageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s asidInvalid then UNIV else {}) \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa))) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa))) (t_hrs_' (globals s))))) \<and> (t_' sa \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<longrightarrow> (t_' sa = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<longrightarrow> (deviceMemory_' sa \<noteq> 0 \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals sa))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa)))) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' sa)) (unat ARMLargePageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' sa)) (unat ARMLargePageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' sa)) (unat ARMLargePageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' sa)) (unat ARMLargePageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' sa)) (unat ARMLargePageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s asidInvalid then UNIV else {}) \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa))) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa))) (t_hrs_' (globals s)))) \<and> (\<not> deviceMemory_' sa \<noteq> 0 \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals sa))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa)))) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' sa)) (unat ARMLargePageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' sa)) (unat ARMLargePageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' sa)) (unat ARMLargePageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' sa)) (unat ARMLargePageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' sa)) (unat ARMLargePageBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s asidInvalid then UNIV else {}) \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa))) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa))) (t_hrs_' (globals s))))) \<and> (t_' sa \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<longrightarrow> (t_' sa = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<longrightarrow> (deviceMemory_' sa \<noteq> 0 \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals sa))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa)))) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' sa)) (unat ARMSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' sa)) (unat ARMSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' sa)) (unat ARMSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' sa)) (unat ARMSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' sa)) (unat ARMSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s asidInvalid then UNIV else {}) \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa))) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa))) (t_hrs_' (globals s)))) \<and> (\<not> deviceMemory_' sa \<noteq> 0 \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals sa))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa)))) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' sa)) (unat ARMSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' sa)) (unat ARMSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' sa)) (unat ARMSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' sa)) (unat ARMSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' sa)) (unat ARMSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s asidInvalid then UNIV else {}) \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa))) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa))) (t_hrs_' (globals s))))) \<and> (t_' sa \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<longrightarrow> (t_' sa = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<longrightarrow> (deviceMemory_' sa \<noteq> 0 \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals sa))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa)))) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' sa)) (unat ARMSuperSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' sa)) (unat ARMSuperSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' sa)) (unat ARMSuperSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' sa)) (unat ARMSuperSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' sa)) (unat ARMSuperSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s asidInvalid then UNIV else {}) \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa))) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' sa))) (t_hrs_' (globals sa))) (t_hrs_' (globals s)))) \<and> (\<not> deviceMemory_' sa \<noteq> 0 \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals sa))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa)))) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' sa)) (unat ARMSuperSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidLowBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' sa)) (unat ARMSuperSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidLowBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' sa)) (unat ARMSuperSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s Kernel_C.asidHighBits then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' sa)) (unat ARMSuperSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if Kernel_C.asidHighBits <s 0x20 then UNIV else {}) \<longrightarrow> globals_update (\<lambda>x. ghost'state_'_update (gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' sa)) (unat ARMSuperSectionBits)) (t_hrs_'_update (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa)))) x)) sa \<in> (if 0 \<le>s asidInvalid then UNIV else {}) \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa))) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' sa))) (t_hrs_' (globals sa))) (t_hrs_' (globals s))))) \<and> (t_' sa \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<longrightarrow> (t_' sa = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals sa))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pte_C[256]) (regionBase_' sa))) (t_hrs_' (globals sa)))) \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pte_C[256]) (regionBase_' sa))) (t_hrs_' (globals sa))) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pte_C[256]) (regionBase_' sa))) (t_hrs_' (globals sa))) (t_hrs_' (globals s)))) \<and> (t_' sa \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject \<longrightarrow> (t_' sa = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals sa))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' sa))) (t_hrs_' (globals sa)))) \<longrightarrow> (\<forall>t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' sa))) (t_hrs_' (globals sa))) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' sa))) (t_hrs_' (globals sa))) (t_hrs_' (globals t)) \<longrightarrow> (\<forall>ta. hrs_htd (t_hrs_' (globals ta)) = hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' sa))) (t_hrs_' (globals sa))) \<and> byte_regions_unmodified (t_hrs_' (globals t)) (t_hrs_' (globals ta)) \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' sa))) (t_hrs_' (globals sa))) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (t_hrs_' (globals ta)) (t_hrs_' (globals s)))))) \<and> (t_' sa \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject \<longrightarrow> (True \<longrightarrow> \<not> False) \<and> (\<not> True \<longrightarrow> False \<longrightarrow> (\<forall>nt. t_' s = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}. hrs_htd (t_hrs_' (globals sa)) x = hrs_htd (t_hrs_' (globals s)) x) \<and> byte_regions_unmodified (t_hrs_' (globals sa)) (t_hrs_' (globals s))))))))))} proof (prove)
goal (11 subgoals):
 1. \<And>s nt xa. \<lbrakk>object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject; deviceMemory_' s \<noteq> 0; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 2. \<And>s nt xa. \<lbrakk>object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject; deviceMemory_' s = 0; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 3. \<And>s nt xa. \<lbrakk>seL4_ARM_LargePageObject \<noteq> seL4_ARM_SmallPageObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject; deviceMemory_' s \<noteq> 0; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 4. \<And>s nt xa. \<lbrakk>seL4_ARM_LargePageObject \<noteq> seL4_ARM_SmallPageObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject; deviceMemory_' s = 0; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 5. \<And>s nt xa. \<lbrakk>seL4_ARM_SectionObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_SectionObject \<noteq> seL4_ARM_LargePageObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject; deviceMemory_' s \<noteq> 0; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 6. \<And>s nt xa. \<lbrakk>seL4_ARM_SectionObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_SectionObject \<noteq> seL4_ARM_LargePageObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject; deviceMemory_' s = 0; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 7. \<And>s nt xa. \<lbrakk>seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_LargePageObject; seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_SectionObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject; deviceMemory_' s \<noteq> 0; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 8. \<And>s nt xa. \<lbrakk>seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_LargePageObject; seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_SectionObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject; deviceMemory_' s = 0; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 9. \<And>s nt xa. \<lbrakk>seL4_ARM_PageTableObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_PageTableObject \<noteq> seL4_ARM_LargePageObject; seL4_ARM_PageTableObject \<noteq> seL4_ARM_SectionObject; seL4_ARM_PageTableObject \<noteq> seL4_ARM_SuperSectionObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> pte_C[256]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyp (PTR_COERCE(unit \<rightarrow> pte_C[256]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 10. \<And>s t ta nt xa. \<lbrakk>seL4_ARM_PageDirectoryObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_PageDirectoryObject \<noteq> seL4_ARM_LargePageObject; seL4_ARM_PageDirectoryObject \<noteq> seL4_ARM_SectionObject; seL4_ARM_PageDirectoryObject \<noteq> seL4_ARM_SuperSectionObject; seL4_ARM_PageDirectoryObject \<noteq> seL4_ARM_PageTableObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); hrs_htd (t_hrs_' (globals t)) = ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))); byte_regions_unmodified (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s))) (t_hrs_' (globals s))) (t_hrs_' (globals t)); hrs_htd (t_hrs_' (globals ta)) = ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))); byte_regions_unmodified (t_hrs_' (globals t)) (t_hrs_' (globals ta)); t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s nt xa. \<lbrakk>object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject; deviceMemory_' s \<noteq> 0; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> ptr_span (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s))\<rbrakk> \<Longrightarrow> False
 2. \<And>s nt xa. \<lbrakk>object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject; deviceMemory_' s = 0; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> ptr_span (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s))\<rbrakk> \<Longrightarrow> False
 3. \<And>s nt xa. \<lbrakk>seL4_ARM_LargePageObject \<noteq> seL4_ARM_SmallPageObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject; deviceMemory_' s \<noteq> 0; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> {ptr_val (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s))..+16 * size_of TYPE(user_data_device_C)}\<rbrakk> \<Longrightarrow> False
 4. \<And>s nt xa. \<lbrakk>seL4_ARM_LargePageObject \<noteq> seL4_ARM_SmallPageObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 16 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject; deviceMemory_' s = 0; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> {ptr_val (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s))..+16 * size_of TYPE(user_data_C)}\<rbrakk> \<Longrightarrow> False
 5. \<And>s nt xa. \<lbrakk>seL4_ARM_SectionObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_SectionObject \<noteq> seL4_ARM_LargePageObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject; deviceMemory_' s \<noteq> 0; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> {ptr_val (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s))..+256 * size_of TYPE(user_data_device_C)}\<rbrakk> \<Longrightarrow> False
 6. \<And>s nt xa. \<lbrakk>seL4_ARM_SectionObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_SectionObject \<noteq> seL4_ARM_LargePageObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 256 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject; deviceMemory_' s = 0; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> {ptr_val (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s))..+256 * size_of TYPE(user_data_C)}\<rbrakk> \<Longrightarrow> False
 7. \<And>s nt xa. \<lbrakk>seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_LargePageObject; seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_SectionObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject; deviceMemory_' s \<noteq> 0; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> {ptr_val (PTR_COERCE(unit \<rightarrow> user_data_device_C) (regionBase_' s))..+4096 * size_of TYPE(user_data_device_C)}\<rbrakk> \<Longrightarrow> False
 8. \<And>s nt xa. \<lbrakk>seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_LargePageObject; seL4_ARM_SuperSectionObject \<noteq> seL4_ARM_SectionObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyps 4096 (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); 0 \<le>s Kernel_C.asidLowBits; Kernel_C.asidLowBits <s 0x20; 0 \<le>s Kernel_C.asidHighBits; Kernel_C.asidHighBits <s 0x20; 0 \<le>s asidInvalid; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject; deviceMemory_' s = 0; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> {ptr_val (PTR_COERCE(unit \<rightarrow> user_data_C) (regionBase_' s))..+4096 * size_of TYPE(user_data_C)}\<rbrakk> \<Longrightarrow> False
 9. \<And>s nt xa. \<lbrakk>seL4_ARM_PageTableObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_PageTableObject \<noteq> seL4_ARM_LargePageObject; seL4_ARM_PageTableObject \<noteq> seL4_ARM_SectionObject; seL4_ARM_PageTableObject \<noteq> seL4_ARM_SuperSectionObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> pte_C[256]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> ptr_span (PTR_COERCE(unit \<rightarrow> pte_C[256]) (regionBase_' s))\<rbrakk> \<Longrightarrow> False
 10. \<And>s t ta nt xa. \<lbrakk>seL4_ARM_PageDirectoryObject \<noteq> seL4_ARM_SmallPageObject; seL4_ARM_PageDirectoryObject \<noteq> seL4_ARM_LargePageObject; seL4_ARM_PageDirectoryObject \<noteq> seL4_ARM_SectionObject; seL4_ARM_PageDirectoryObject \<noteq> seL4_ARM_SuperSectionObject; seL4_ARM_PageDirectoryObject \<noteq> seL4_ARM_PageTableObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); hrs_htd (t_hrs_' (globals t)) = ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))); byte_regions_unmodified (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s))) (t_hrs_' (globals s))) (t_hrs_' (globals t)); hrs_htd (t_hrs_' (globals ta)) = ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))); byte_regions_unmodified (t_hrs_' (globals t)) (t_hrs_' (globals ta)); t_' s = SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> ptr_span (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s))\<rbrakk> \<Longrightarrow> False
A total of 11 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s t ta nt. \<lbrakk>htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); hrs_htd (t_hrs_' (globals t)) = ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))); byte_regions_unmodified (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s))) (t_hrs_' (globals s))) (t_hrs_' (globals t)); hrs_htd (t_hrs_' (globals ta)) = ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))); byte_regions_unmodified (t_hrs_' (globals t)) (t_hrs_' (globals ta)); t_' s = 5; nt = object_type.PageDirectoryObject\<rbrakk> \<Longrightarrow> byte_regions_unmodified (t_hrs_' (globals ta)) (t_hrs_' (globals s)) proof (prove)
goal (1 subgoal):
 1. \<And>s t ta nt. \<lbrakk>htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); hrs_htd (t_hrs_' (globals t)) = ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))); byte_regions_unmodified (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s))) (t_hrs_' (globals s))) (t_hrs_' (globals t)); hrs_htd (t_hrs_' (globals ta)) = ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))); byte_regions_unmodified (t_hrs_' (globals t)) (t_hrs_' (globals ta)); t_' s = 5; nt = object_type.PageDirectoryObject\<rbrakk> \<Longrightarrow> byte_regions_unmodified (hrs_htd_update (\<lambda>_. ptr_retyp (PTR_COERCE(unit \<rightarrow> pde_C[4096]) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))) (t_hrs_' (globals s))) (t_hrs_' (globals ta)) proof (prove)
goal:
No subgoals!