theory Retype_C

lemma createObject_untyped_region_is_zero_bytes:
  "\<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s. let tp = (object_type_to_H (t_' s));
          sz = APIType_capBits tp (unat (userSize_' s))
      in (\<not> to_bool (deviceMemory_' s)
              \<longrightarrow> region_actually_is_zero_bytes (ptr_val (regionBase_' s)) (2 ^ sz) s)
          \<and> is_aligned (ptr_val (regionBase_' s)) sz
          \<and> sz < 32 \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> sz \<ge> minUntypedSizeBits)}
      Call createObject_'proc
   {t. cap_get_tag (ret__struct_cap_C_' t) = scast cap_untyped_cap
         \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True
          | Some (a, b) \<Rightarrow> region_actually_is_zero_bytes a (unat ((b + 1) - a)) t)}" apply (rule allI, rule conseqPre, vcg exspec=copyGlobalMappings_modifies
      exspec=Arch_initContext_modifies
      exspec=cleanCacheRange_PoU_modifies) apply (clarsimp simp: cap_tag_defs) apply (simp add: cap_lift_untyped_cap cap_tag_defs cap_to_H_simps
                   cap_untyped_cap_lift_def object_type_from_H_def) apply (simp add: untypedZeroRange_def split: if_split) apply (clarsimp simp: getFreeRef_def Let_def object_type_to_H_def untypedBits_defs) apply (simp add:  APIType_capBits_def
                   less_mask_eq word_less_nat_alt) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s. let tp = object_type_to_H (t_' s); sz = APIType_capBits tp (unat (userSize_' s)) in (\<not> to_bool (deviceMemory_' s) \<longrightarrow> region_actually_is_bytes (ptr_val (regionBase_' s)) (2 ^ sz) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ sz) (ptr_val (regionBase_' s)) = replicate (2 ^ sz) 0) \<and> is_aligned (ptr_val (regionBase_' s)) sz \<and> sz < 32 \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> sz)} Call createObject_'proc {t. cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) t \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. let tp = object_type_to_H (t_' s); sz = APIType_capBits tp (unat (userSize_' s)) in (\<not> to_bool (deviceMemory_' s) \<longrightarrow> region_actually_is_bytes (ptr_val (regionBase_' s)) (2 ^ sz) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (2 ^ sz) (ptr_val (regionBase_' s)) = replicate (2 ^ sz) 0) \<and> is_aligned (ptr_val (regionBase_' s)) sz \<and> sz < 32 \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> sz)} \<subseteq> {s. (SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject = t_' s \<longrightarrow> (deviceMemory_' s \<noteq> 0 \<longrightarrow> fst (True, ptr_retyps 1 (PTR(user_data_device_C) (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> fst (True, gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' s)) (unat ARMSmallPageBits)) \<longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<longrightarrow> Kernel_C.asidLowBits <s 0x20 \<longrightarrow> 0 \<le>s Kernel_C.asidHighBits \<longrightarrow> Kernel_C.asidHighBits <s 0x20 \<longrightarrow> 0 \<le>s asidInvalid \<longrightarrow> (\<forall>t. cap_small_frame_cap_lift (ret__struct_cap_C_' t) = \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10, capFVMRights_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2, capFMappedAddress_CL = SCAST(32 signed \<rightarrow> 32) 0 && ~~ mask 12, capFIsDevice_CL = SCAST(32 signed \<rightarrow> 32) (if deviceMemory_' s \<noteq> 0 then 1 else 0) && mask 1, capFMappedASIDHigh_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1) && mask 7, capFBasePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 12\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))) \<and> (\<not> deviceMemory_' s \<noteq> 0 \<longrightarrow> fst (True, ptr_retyps 1 (PTR(user_data_C) (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> fst (True, gs_new_frames Wellformed_C.ARMSmallPage (ptr_val (regionBase_' s)) (unat ARMSmallPageBits)) \<longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<longrightarrow> Kernel_C.asidLowBits <s 0x20 \<longrightarrow> 0 \<le>s Kernel_C.asidHighBits \<longrightarrow> Kernel_C.asidHighBits <s 0x20 \<longrightarrow> 0 \<le>s asidInvalid \<longrightarrow> (\<forall>t. cap_small_frame_cap_lift (ret__struct_cap_C_' t) = \<lparr>cap_small_frame_cap_CL.capFMappedASIDLow_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10, capFVMRights_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2, capFMappedAddress_CL = SCAST(32 signed \<rightarrow> 32) 0 && ~~ mask 12, capFIsDevice_CL = SCAST(32 signed \<rightarrow> 32) (if deviceMemory_' s \<noteq> 0 then 1 else 0) && mask 1, capFMappedASIDHigh_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1) && mask 7, capFBasePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 12\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SmallPageObject \<noteq> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject = t_' s \<longrightarrow> (deviceMemory_' s \<noteq> 0 \<longrightarrow> fst (True, ptr_retyps 16 (PTR(user_data_device_C) (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 16 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> fst (True, gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' s)) (unat ARMLargePageBits)) \<longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<longrightarrow> Kernel_C.asidLowBits <s 0x20 \<longrightarrow> 0 \<le>s Kernel_C.asidHighBits \<longrightarrow> Kernel_C.asidHighBits <s 0x20 \<longrightarrow> 0 \<le>s asidInvalid \<longrightarrow> (\<forall>t. cap_frame_cap_lift (ret__struct_cap_C_' t) = \<lparr>capFSize_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage && mask 2, capFMappedASIDLow_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10, capFVMRights_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2, capFMappedAddress_CL = SCAST(32 signed \<rightarrow> 32) 0 && ~~ mask 14, capFIsDevice_CL = SCAST(32 signed \<rightarrow> 32) (if deviceMemory_' s \<noteq> 0 then 1 else 0) && mask 1, capFMappedASIDHigh_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1) && mask 7, capFBasePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 14\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_frame_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 16 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyps 16 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))) \<and> (\<not> deviceMemory_' s \<noteq> 0 \<longrightarrow> fst (True, ptr_retyps 16 (PTR(user_data_C) (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 16 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> fst (True, gs_new_frames Wellformed_C.ARMLargePage (ptr_val (regionBase_' s)) (unat ARMLargePageBits)) \<longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<longrightarrow> Kernel_C.asidLowBits <s 0x20 \<longrightarrow> 0 \<le>s Kernel_C.asidHighBits \<longrightarrow> Kernel_C.asidHighBits <s 0x20 \<longrightarrow> 0 \<le>s asidInvalid \<longrightarrow> (\<forall>t. cap_frame_cap_lift (ret__struct_cap_C_' t) = \<lparr>capFSize_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage && mask 2, capFMappedASIDLow_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10, capFVMRights_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2, capFMappedAddress_CL = SCAST(32 signed \<rightarrow> 32) 0 && ~~ mask 14, capFIsDevice_CL = SCAST(32 signed \<rightarrow> 32) (if deviceMemory_' s \<noteq> 0 then 1 else 0) && mask 1, capFMappedASIDHigh_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1) && mask 7, capFBasePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 14\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_frame_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 16 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyps 16 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_LargePageObject \<noteq> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject = t_' s \<longrightarrow> (deviceMemory_' s \<noteq> 0 \<longrightarrow> fst (True, ptr_retyps 256 (PTR(user_data_device_C) (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 256 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> fst (True, gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' s)) (unat ARMSectionBits)) \<longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<longrightarrow> Kernel_C.asidLowBits <s 0x20 \<longrightarrow> 0 \<le>s Kernel_C.asidHighBits \<longrightarrow> Kernel_C.asidHighBits <s 0x20 \<longrightarrow> 0 \<le>s asidInvalid \<longrightarrow> (\<forall>t. cap_frame_cap_lift (ret__struct_cap_C_' t) = \<lparr>capFSize_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection && mask 2, capFMappedASIDLow_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10, capFVMRights_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2, capFMappedAddress_CL = SCAST(32 signed \<rightarrow> 32) 0 && ~~ mask 14, capFIsDevice_CL = SCAST(32 signed \<rightarrow> 32) (if deviceMemory_' s \<noteq> 0 then 1 else 0) && mask 1, capFMappedASIDHigh_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1) && mask 7, capFBasePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 14\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_frame_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 256 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyps 256 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))) \<and> (\<not> deviceMemory_' s \<noteq> 0 \<longrightarrow> fst (True, ptr_retyps 256 (PTR(user_data_C) (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 256 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> fst (True, gs_new_frames Wellformed_C.ARMSection (ptr_val (regionBase_' s)) (unat ARMSectionBits)) \<longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<longrightarrow> Kernel_C.asidLowBits <s 0x20 \<longrightarrow> 0 \<le>s Kernel_C.asidHighBits \<longrightarrow> Kernel_C.asidHighBits <s 0x20 \<longrightarrow> 0 \<le>s asidInvalid \<longrightarrow> (\<forall>t. cap_frame_cap_lift (ret__struct_cap_C_' t) = \<lparr>capFSize_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection && mask 2, capFMappedASIDLow_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10, capFVMRights_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2, capFMappedAddress_CL = SCAST(32 signed \<rightarrow> 32) 0 && ~~ mask 14, capFIsDevice_CL = SCAST(32 signed \<rightarrow> 32) (if deviceMemory_' s \<noteq> 0 then 1 else 0) && mask 1, capFMappedASIDHigh_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1) && mask 7, capFBasePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 14\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_frame_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 256 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyps 256 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SectionObject \<noteq> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject = t_' s \<longrightarrow> (deviceMemory_' s \<noteq> 0 \<longrightarrow> fst (True, ptr_retyps 4096 (PTR(user_data_device_C) (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 4096 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> fst (True, gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' s)) (unat ARMSuperSectionBits)) \<longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<longrightarrow> Kernel_C.asidLowBits <s 0x20 \<longrightarrow> 0 \<le>s Kernel_C.asidHighBits \<longrightarrow> Kernel_C.asidHighBits <s 0x20 \<longrightarrow> 0 \<le>s asidInvalid \<longrightarrow> (\<forall>t. cap_frame_cap_lift (ret__struct_cap_C_' t) = \<lparr>capFSize_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection && mask 2, capFMappedASIDLow_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10, capFVMRights_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2, capFMappedAddress_CL = SCAST(32 signed \<rightarrow> 32) 0 && ~~ mask 14, capFIsDevice_CL = SCAST(32 signed \<rightarrow> 32) (if deviceMemory_' s \<noteq> 0 then 1 else 0) && mask 1, capFMappedASIDHigh_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1) && mask 7, capFBasePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 14\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_frame_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 4096 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyps 4096 (PTR(user_data_device_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))) \<and> (\<not> deviceMemory_' s \<noteq> 0 \<longrightarrow> fst (True, ptr_retyps 4096 (PTR(user_data_C) (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 4096 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> fst (True, gs_new_frames Wellformed_C.ARMSuperSection (ptr_val (regionBase_' s)) (unat ARMSuperSectionBits)) \<longrightarrow> 0 \<le>s Kernel_C.asidLowBits \<longrightarrow> Kernel_C.asidLowBits <s 0x20 \<longrightarrow> 0 \<le>s Kernel_C.asidHighBits \<longrightarrow> Kernel_C.asidHighBits <s 0x20 \<longrightarrow> 0 \<le>s asidInvalid \<longrightarrow> (\<forall>t. cap_frame_cap_lift (ret__struct_cap_C_' t) = \<lparr>capFSize_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection && mask 2, capFMappedASIDLow_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) asidInvalid && (1 << unat Kernel_C.asidLowBits) - 1) && mask 10, capFVMRights_CL = SCAST(32 signed \<rightarrow> 32) Kernel_C.VMReadWrite && mask 2, capFMappedAddress_CL = SCAST(32 signed \<rightarrow> 32) 0 && ~~ mask 14, capFIsDevice_CL = SCAST(32 signed \<rightarrow> 32) (if deviceMemory_' s \<noteq> 0 then 1 else 0) && mask 1, capFMappedASIDHigh_CL = UCAST(32 \<rightarrow> 32) (SCAST(32 signed \<rightarrow> 32) (asidInvalid >> unat Kernel_C.asidLowBits) && (1 << unat Kernel_C.asidHighBits) - 1) && mask 7, capFBasePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 14\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_frame_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 4096 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyps 4096 (PTR(user_data_C) (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_SuperSectionObject \<noteq> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject = t_' s \<longrightarrow> fst (True, ptr_retyps 1 (pt_Ptr (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 1 (pt_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> (\<forall>t. cap_page_table_cap_lift (ret__struct_cap_C_' t) = \<lparr>capPTIsMapped_CL = SCAST(32 signed \<rightarrow> 32) false && mask 1, capPTMappedASID_CL = SCAST(32 signed \<rightarrow> 32) asidInvalid && mask 17, capPTMappedAddress_CL = SCAST(32 signed \<rightarrow> 32) 0 && ~~ mask 20, capPTBasePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 10\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_page_table_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_page_table_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 1 (pt_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyps 1 (pt_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageTableObject \<noteq> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject = t_' s \<longrightarrow> fst (True, ptr_retyps 1 (pd_Ptr (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyps 1 (pd_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> (\<forall>t. ret__unsigned_long_' t = addrFromPPtr (ptr_val (regionBase_' s)) \<longrightarrow> 0 \<le>s 0xC + 2 \<longrightarrow> unat 1 * 2 ^ unat (0xC + 2) < 2 ^ 31 \<and> 0 \<le>s 1 \<longrightarrow> - 2147483648 \<le> sint 0xC + sint 2 \<and> sint 0xC + sint 2 \<le> 2147483647 \<longrightarrow> (\<forall>t ta. cap_page_directory_cap_lift (ret__struct_cap_C_' ta) = \<lparr>capPDMappedASID_CL = SCAST(32 signed \<rightarrow> 32) false && mask 17, capPDIsMapped_CL = SCAST(32 signed \<rightarrow> 32) asidInvalid && mask 1, capPDBasePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 14\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' ta) = SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_page_directory_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' ta)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) t \<and> heap_list (hrs_mem (t_hrs_' (globals t))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0)))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_ARM_PageDirectoryObject \<noteq> t_' s \<longrightarrow> (True \<longrightarrow> \<not> False) \<and> (\<not> True \<longrightarrow> False \<longrightarrow> cap_get_tag (ret__struct_cap_C_' s) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' s)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))))))))) \<and> (\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_TCBObject = t_' s \<longrightarrow> (\<forall>v. 0 \<le>s 9 - 1 \<longrightarrow> 9 - 1 <s 0x20 \<longrightarrow> - 2147483648 \<le> sint 9 - sint 1 \<and> sint 9 - sint 1 \<le> 2147483647 \<longrightarrow> fst (True, \<lambda>x. ptr_retyps 1 (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))) x)) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, \<lambda>x. ptr_retyps 1 (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))) x))) (t_hrs_' (globals s)))) \<longrightarrow> hrs_htd (hrs_htd_update (snd (True, \<lambda>x. ptr_retyps 1 (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))) x))) (t_hrs_' (globals s))) \<Turnstile>\<^sub>t tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1))) \<longrightarrow> (\<forall>t. t \<Turnstile>\<^sub>c tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1))) \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(32 word) &(tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))\<rightarrow>[''tcbTimeSlice_C''])) (SCAST(32 signed \<rightarrow> 32) 5)) (t_hrs_' (globals t))) \<Turnstile>\<^sub>t tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1))) \<longrightarrow> (\<forall>ta. cap_thread_cap_lift (ret__struct_cap_C_' ta) = \<lparr>cap_thread_cap_CL.capTCBPtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1))))) && ~~ mask 4\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' ta) = SCAST(32 signed \<rightarrow> 32) cap_thread_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_thread_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' ta)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_mem_update (heap_update (PTR(32 word) &(tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))\<rightarrow>[''tcbDomain_C''])) (ksCurDomain_' (globals s))) (hrs_mem_update (heap_update (PTR(32 word) &(tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))\<rightarrow>[''tcbTimeSlice_C''])) (SCAST(32 signed \<rightarrow> 32) 5)) (t_hrs_' (globals t))))) \<and> heap_list (hrs_mem (hrs_mem_update (heap_update (PTR(32 word) &(tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))\<rightarrow>[''tcbDomain_C''])) (ksCurDomain_' (globals s))) (hrs_mem_update (heap_update (PTR(32 word) &(tcb_Ptr (ptr_val (regionBase_' s) + (1 << unat (9 - 1)))\<rightarrow>[''tcbTimeSlice_C''])) (SCAST(32 signed \<rightarrow> 32) 5)) (t_hrs_' (globals t))))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_TCBObject \<noteq> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject = t_' s \<longrightarrow> fst (True, ptr_retyp (ep_Ptr (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyp (ep_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> (\<forall>t. cap_endpoint_cap_lift (ret__struct_cap_C_' t) = \<lparr>capEPBadge_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 28, capCanGrantReply_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, capCanGrant_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, capCanSend_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, capCanReceive_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, capEPPtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 4\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyp (ep_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyp (ep_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject \<noteq> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject = t_' s \<longrightarrow> fst (True, ptr_retyp (ntfn_Ptr (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_retyp (ntfn_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> (\<forall>t. cap_notification_cap_lift (ret__struct_cap_C_' t) = \<lparr>capNtfnBadge_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 28, capNtfnCanReceive_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, capNtfnCanSend_CL = SCAST(32 signed \<rightarrow> 32) true && mask 1, capNtfnPtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 4\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_notification_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_notification_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_retyp (ntfn_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_retyp (ntfn_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject \<noteq> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject = t_' s \<longrightarrow> fst (True, ptr_arr_retyps (2 ^ unat (userSize_' s)) (cte_Ptr (ptr_val (regionBase_' s)))) \<longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s))) \<and> htd_safe domain (hrs_htd (hrs_htd_update (snd (True, ptr_arr_retyps (2 ^ unat (userSize_' s)) (cte_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<longrightarrow> fst (True, gs_new_cnodes (unat (userSize_' s)) (ptr_val (regionBase_' s)) (4 + unat (userSize_' s))) \<longrightarrow> (\<forall>t. cap_cnode_cap_lift (ret__struct_cap_C_' t) = \<lparr>capCNodeRadix_CL = UCAST(32 \<rightarrow> 32) (userSize_' s) && mask 5, capCNodeGuardSize_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 5, capCNodeGuard_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 18, capCNodePtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 5\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_cnode_cap \<longrightarrow> SCAST(32 signed \<rightarrow> 32) cap_cnode_cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd (hrs_htd_update (snd (True, ptr_arr_retyps (2 ^ unat (userSize_' s)) (cte_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) \<and> heap_list (hrs_mem (hrs_htd_update (snd (True, ptr_arr_retyps (2 ^ unat (userSize_' s)) (cte_Ptr (ptr_val (regionBase_' s))))) (t_hrs_' (globals s)))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject \<noteq> t_' s \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject = t_' s \<longrightarrow> (\<forall>t. cap_untyped_cap_lift (ret__struct_cap_C_' t) = \<lparr>capFreeIndex_CL = SCAST(32 signed \<rightarrow> 32) 0 && mask 26, capIsDevice_CL = SCAST(32 signed \<rightarrow> 32) (if deviceMemory_' s \<noteq> 0 then 1 else 0) && mask 1, capBlockSize_CL = UCAST(32 \<rightarrow> 32) (userSize_' s) && mask 5, capPtr_CL = UCAST(32 \<rightarrow> 32) (ptr_val (regionBase_' s)) && ~~ mask 4\<rparr> \<and> cap_get_tag (ret__struct_cap_C_' t) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))) \<and> (SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject \<noteq> t_' s \<longrightarrow> (True \<longrightarrow> \<not> False) \<and> (\<not> True \<longrightarrow> False \<longrightarrow> cap_get_tag (ret__struct_cap_C_' s) = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap \<longrightarrow> (case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' s)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) s \<and> heap_list (hrs_mem (t_hrs_' (globals s))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0))))))))} proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>let tp = object_type_to_H (t_' x); sz = APIType_capBits tp (unat (userSize_' x)) in (\<not> to_bool (deviceMemory_' x) \<longrightarrow> region_actually_is_bytes (ptr_val (regionBase_' x)) (2 ^ sz) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ sz) (ptr_val (regionBase_' x)) = replicate (2 ^ sz) 0) \<and> is_aligned (ptr_val (regionBase_' x)) sz \<and> sz < 32 \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) (unat (userSize_' x))); \<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_TCBObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject = t_' x; cap_untyped_cap_lift (ret__struct_cap_C_' t) = \<lparr>capFreeIndex_CL = 0, capIsDevice_CL = (if deviceMemory_' x \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) && 1, capBlockSize_CL = userSize_' x && mask 5, capPtr_CL = ptr_val (regionBase_' x) && ~~ mask 4\<rparr>; cap_get_tag (ret__struct_cap_C_' t) = 2\<rbrakk> \<Longrightarrow> case untypedZeroRange (cap_to_H (the (cap_lift (ret__struct_cap_C_' t)))) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>let tp = object_type_to_H (t_' x); sz = APIType_capBits tp (unat (userSize_' x)) in (\<not> to_bool (deviceMemory_' x) \<longrightarrow> region_actually_is_bytes (ptr_val (regionBase_' x)) (2 ^ sz) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ sz) (ptr_val (regionBase_' x)) = replicate (2 ^ sz) 0) \<and> is_aligned (ptr_val (regionBase_' x)) sz \<and> sz < 32 \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) (unat (userSize_' x))); \<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_TCBObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject = t_' x; (cap_C.words_C (ret__struct_cap_C_' t).[Suc 0] >> 6) && mask 26 = 0 \<and> (cap_C.words_C (ret__struct_cap_C_' t).[Suc 0] >> 5) && 1 = (if deviceMemory_' x \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) && 1 \<and> cap_C.words_C (ret__struct_cap_C_' t).[Suc 0] && mask 5 = userSize_' x && mask 5 \<and> cap_C.words_C (ret__struct_cap_C_' t).[0] && ~~ mask 4 = ptr_val (regionBase_' x) && ~~ mask 4; cap_get_tag (ret__struct_cap_C_' t) = 2\<rbrakk> \<Longrightarrow> case untypedZeroRange (capability.UntypedCap (to_bool ((if deviceMemory_' x \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) && 1)) (ptr_val (regionBase_' x) && ~~ mask 4) (unat (userSize_' x && mask 5)) 0) of None \<Rightarrow> True | Some (a, b) \<Rightarrow> region_actually_is_bytes a (unat (b + 1 - a)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>let tp = object_type_to_H (t_' x); sz = APIType_capBits tp (unat (userSize_' x)) in (\<not> to_bool (deviceMemory_' x) \<longrightarrow> region_actually_is_bytes (ptr_val (regionBase_' x)) (2 ^ sz) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ sz) (ptr_val (regionBase_' x)) = replicate (2 ^ sz) 0) \<and> is_aligned (ptr_val (regionBase_' x)) sz \<and> sz < 32 \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) (unat (userSize_' x))); \<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_TCBObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject = t_' x; (cap_C.words_C (ret__struct_cap_C_' t).[Suc 0] >> 6) && mask 26 = 0 \<and> (cap_C.words_C (ret__struct_cap_C_' t).[Suc 0] >> 5) && 1 = (if deviceMemory_' x \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0) && 1 \<and> cap_C.words_C (ret__struct_cap_C_' t).[Suc 0] && mask 5 = userSize_' x && mask 5 \<and> cap_C.words_C (ret__struct_cap_C_' t).[0] && ~~ mask 4 = ptr_val (regionBase_' x) && ~~ mask 4; cap_get_tag (ret__struct_cap_C_' t) = 2\<rbrakk> \<Longrightarrow> deviceMemory_' x = 0 \<longrightarrow> 0 < max_free_index (unat (userSize_' x && mask 5)) \<longrightarrow> region_actually_is_bytes (getFreeRef (ptr_val (regionBase_' x) && ~~ mask 4) 0) (unat ((ptr_val (regionBase_' x) && ~~ mask 4) + 2 ^ unat (userSize_' x && mask 5) - getFreeRef (ptr_val (regionBase_' x) && ~~ mask 4) 0)) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat ((ptr_val (regionBase_' x) && ~~ mask 4) + 2 ^ unat (userSize_' x && mask 5) - getFreeRef (ptr_val (regionBase_' x) && ~~ mask 4) 0)) (getFreeRef (ptr_val (regionBase_' x) && ~~ mask 4) 0) = replicate (unat ((ptr_val (regionBase_' x) && ~~ mask 4) + 2 ^ unat (userSize_' x && mask 5) - getFreeRef (ptr_val (regionBase_' x) && ~~ mask 4) 0)) 0 proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_TCBObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject \<noteq> t_' x; SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject = t_' x; cap_get_tag (ret__struct_cap_C_' t) = 2; (cap_C.words_C (ret__struct_cap_C_' t).[Suc 0] >> 6) && mask 26 = 0; is_aligned (ptr_val (regionBase_' x)) (APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) (unat (userSize_' x))); (cap_C.words_C (ret__struct_cap_C_' t).[Suc 0] >> 5) && 1 = 0; APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) (unat (userSize_' x)) < 32; 4 \<le> APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) (unat (userSize_' x)); cap_C.words_C (ret__struct_cap_C_' t).[Suc 0] && mask 5 = userSize_' x && mask 5; cap_C.words_C (ret__struct_cap_C_' t).[0] && ~~ mask 4 = ptr_val (regionBase_' x); deviceMemory_' x = 0; 0 < max_free_index (unat (userSize_' x && mask 5)); region_actually_is_bytes (ptr_val (regionBase_' x)) (2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) (unat (userSize_' x))) x; heap_list (hrs_mem (t_hrs_' (globals x))) (2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) (unat (userSize_' x))) (ptr_val (regionBase_' x)) = replicate (2 ^ APIType_capBits (APIObjectType ArchTypes_H.apiobject_type.Untyped) (unat (userSize_' x))) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes (ptr_val (regionBase_' x)) (unat (2 ^ unat (userSize_' x && mask 5))) x \<and> heap_list (hrs_mem (t_hrs_' (globals x))) (unat (2 ^ unat (userSize_' x && mask 5))) (ptr_val (regionBase_' x)) = replicate (unat (2 ^ unat (userSize_' x && mask 5))) 0 proof (prove)
goal:
No subgoals!