theory Retype_C

lemma createObject_preserves_bytes:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call 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=Arch_createObject_preserves_bytes
                             exspec=cap_thread_cap_new_modifies
                             exspec=cap_endpoint_cap_new_modifies
                             exspec=cap_notification_cap_new_modifies
                             exspec=cap_cnode_cap_new_modifies
                             exspec=cap_untyped_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 trans[OF ptr_retyp_d ptr_retyp_d]
                         ptr_arr_retyps_eq_outside_dom) apply (simp_all add: object_type_from_H_def Kernel_C_defs APIType_capBits_def
                           objBits_simps' cte_C_size power_add ctcb_offset_defs
                      split: object_type.split_asm apiobject_type.split_asm) apply (erule notE, erule subsetD[rotated], rule intvl_start_le intvl_sub_offset, simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call 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
  IF SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> \<acute>t THEN
  \<acute>ret__struct_cap_C :== CALL Arch_createObject_'proc(\<acute>t,\<acute>regionBase,\<acute>userSize,\<acute>deviceMemory);;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_'
FI;;
 SWITCH \<acute>t {SCAST(32 signed \<rightarrow> 32) seL4_TCBObject}\<Rightarrow> lvar_nondet_init tcb_' tcb_'_update;;
Guard ShiftError \<lbrace>0 \<le>s 9 - 1\<rbrace> (Guard ShiftError \<lbrace>9 - 1 <s 0x20\<rbrace> (Guard SignedArithmetic \<lbrace>- 2147483648 \<le> sint 9 - sint 1 \<and> sint 9 - sint 1 \<le> 2147483647\<rbrace> (\<acute>tcb :== tcb_Ptr (ptr_val \<acute>regionBase + (1 << unat (9 - 1))))));;
Guard MemorySafety \<lbrace>fst (True, ptr_retyps 1 (PTR(cte_C[5]) (ptr_val \<acute>tcb - ctcb_offset)) \<circ> ptr_retyp \<acute>tcb)\<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(cte_C[5]) (ptr_val (tcb_' s) - ctcb_offset)) \<circ> ptr_retyp (tcb_' s))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyps 1 (PTR(cte_C[5]) (ptr_val \<acute>tcb - ctcb_offset)) \<circ> ptr_retyp \<acute>tcb)))));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (CALL Arch_initContext_'proc(PTR(user_context_C) &(PTR(arch_tcb_C) &(\<acute>tcb\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(\<acute>tcb\<rightarrow>[''tcbTimeSlice_C''])) (SCAST(32 signed \<rightarrow> 32) 5))));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(\<acute>tcb\<rightarrow>[''tcbDomain_C''])) \<acute>ksCurDomain)));;
SKIP;;
\<acute>ret__struct_cap_C :== CALL cap_thread_cap_new_'proc(UCAST(32 \<rightarrow> 32) (ptr_val \<acute>tcb));;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_' | {SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject}\<Rightarrow> Guard MemorySafety \<lbrace>fst (True, ptr_retyp (ep_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_retyp (ep_Ptr (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyp (ep_Ptr (ptr_val \<acute>regionBase)))))));;
\<acute>ret__struct_cap_C :== CALL cap_endpoint_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,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_NotificationObject}\<Rightarrow> Guard MemorySafety \<lbrace>fst (True, ptr_retyp (ntfn_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_retyp (ntfn_Ptr (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_retyp (ntfn_Ptr (ptr_val \<acute>regionBase)))))));;
\<acute>ret__struct_cap_C :== CALL cap_notification_cap_new_'proc(SCAST(32 signed \<rightarrow> 32) 0,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,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_CapTableObject}\<Rightarrow> Guard MemorySafety \<lbrace>fst (True, ptr_arr_retyps (2 ^ unat \<acute>userSize) (cte_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_arr_retyps (2 ^ unat (userSize_' s)) (cte_Ptr (ptr_val (regionBase_' s))))))) s))))} (\<acute>globals :== t_hrs_'_update (hrs_htd_update (snd (True, ptr_arr_retyps (2 ^ unat \<acute>userSize) (cte_Ptr (ptr_val \<acute>regionBase)))))));;
Guard GhostStateError \<lbrace>fst (True, gs_new_cnodes (unat \<acute>userSize) (ptr_val \<acute>regionBase) (4 + unat \<acute>userSize))\<rbrace> (\<acute>globals :== ghost'state_'_update (snd (True, gs_new_cnodes (unat \<acute>userSize) (ptr_val \<acute>regionBase) (4 + unat \<acute>userSize))));;
\<acute>ret__struct_cap_C :== CALL cap_cnode_cap_new_'proc(UCAST(32 \<rightarrow> 32) \<acute>userSize,SCAST(32 signed \<rightarrow> 32) 0,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_UntypedObject}\<Rightarrow> \<acute>ret__struct_cap_C :== CALL cap_untyped_cap_new_'proc(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) \<acute>userSize,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 SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> \<acute>t THEN
  \<acute>ret__struct_cap_C :== CALL Arch_createObject_'proc();;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_'
FI;;
IF \<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_TCBObject THEN
  lvar_nondet_init tcb_' tcb_'_update;;
Guard ShiftError UNIV (Guard ShiftError UNIV (Guard SignedArithmetic UNIV (\<acute>tcb :== tcb_Ptr (ptr_val \<acute>regionBase + 0x100))));;
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(cte_C[5]) (ptr_val \<acute>tcb - ctcb_offset)) \<circ> ptr_retyp \<acute>tcb) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR(cte_C[5]) (ptr_val \<acute>tcb - ctcb_offset)) \<circ> ptr_retyp \<acute>tcb))));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (CALL Arch_initContext_'proc(PTR(user_context_C) &(PTR(arch_tcb_C) &(\<acute>tcb\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(\<acute>tcb\<rightarrow>[''tcbTimeSlice_C''])) 5)));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_' s} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(\<acute>tcb\<rightarrow>[''tcbDomain_C''])) \<acute>ksCurDomain)));;
SKIP;;
\<acute>ret__struct_cap_C :== CALL cap_thread_cap_new_'proc(ptr_val \<acute>tcb);;
return_C ret__struct_cap_C_'_update ret__struct_cap_C_'
ELSE
  IF \<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject 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> endpoint_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> endpoint_C) \<acute>regionBase)))));;
\<acute>ret__struct_cap_C :== CALL cap_endpoint_cap_new_'proc(0,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,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_NotificationObject 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> notification_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> notification_C) \<acute>regionBase)))));;
\<acute>ret__struct_cap_C :== CALL cap_notification_cap_new_'proc(0,SCAST(32 signed \<rightarrow> 32) true,SCAST(32 signed \<rightarrow> 32) true,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_CapTableObject 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_arr_retyps (2 ^ unat \<acute>userSize) (PTR_COERCE(unit \<rightarrow> cte_C) \<acute>regionBase)) \<acute>t_hrs))\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_htd_update (ptr_arr_retyps (2 ^ unat \<acute>userSize) (PTR_COERCE(unit \<rightarrow> cte_C) \<acute>regionBase)))));;
Guard GhostStateError UNIV (\<acute>globals :== ghost'state_'_update (gs_new_cnodes (unat \<acute>userSize) (ptr_val \<acute>regionBase) (4 + unat \<acute>userSize)));;
\<acute>ret__struct_cap_C :== CALL cap_cnode_cap_new_'proc(\<acute>userSize,0,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_UntypedObject THEN
  \<acute>ret__struct_cap_C :== CALL cap_untyped_cap_new_'proc(0,if \<acute>deviceMemory \<noteq> 0 then SCAST(32 signed \<rightarrow> 32) 1 else SCAST(32 signed \<rightarrow> 32) 0,\<acute>userSize,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;;
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> \<lbrace>(SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> \<acute>t \<longrightarrow> (\<forall>ta. (\<forall>nt. \<acute>t = object_type_from_H nt \<longrightarrow> (\<forall>x\<in>- {ptr_val \<acute>regionBase..+2 ^ getObjectSize nt (unat \<acute>userSize)}. hrs_htd \<^bsup>ta\<^esup>t_hrs x = hrs_htd \<acute>t_hrs x) \<and> byte_regions_unmodified \<^bsup>ta\<^esup>t_hrs \<acute>t_hrs) \<longrightarrow> (\<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 \<^bsup>ta\<^esup>t_hrs x = hrs_htd \<^bsup>s\<^esup>t_hrs x) \<and> byte_regions_unmodified \<^bsup>ta\<^esup>t_hrs \<^bsup>s\<^esup>t_hrs))) \<and> (\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> \<acute>t \<longrightarrow> (\<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_TCBObject \<longrightarrow> (\<forall>v. True \<longrightarrow> htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs)) \<longrightarrow> hrs_htd (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs) \<Turnstile>\<^sub>t tcb_Ptr (ptr_val \<acute>regionBase + 0x100) \<longrightarrow> Kernel_C.CPSR <s 0x14 \<longrightarrow> 0 \<le>s Kernel_C.CPSR \<longrightarrow> hrs_htd (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs) \<Turnstile>\<^sub>t PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C'']) \<longrightarrow> 0 \<le>s 8 \<longrightarrow> unat 1 * 2 ^ unat 8 < 2 ^ 31 \<and> 0 \<le>s 1 \<longrightarrow> 0 \<le>s 6 \<longrightarrow> unat 1 * 2 ^ unat 6 < 2 ^ 31 \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])) (Arrays.update (h_val (hrs_mem (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs)) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C'']))) (unat Kernel_C.CPSR) (SCAST(32 signed \<rightarrow> 32) (((1 << unat 6) || 0x10) || (1 << unat 8))))) (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs)) \<Turnstile>\<^sub>t tcb_Ptr (ptr_val \<acute>regionBase + 0x100) \<longrightarrow> hrs_htd (hrs_mem_update (heap_update (PTR(32 word) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbTimeSlice_C''])) 5) (hrs_mem_update (heap_update (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])) (Arrays.update (h_val (hrs_mem (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs)) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C'']))) (unat Kernel_C.CPSR) (SCAST(32 signed \<rightarrow> 32) (((1 << unat 6) || 0x10) || (1 << unat 8))))) (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs))) \<Turnstile>\<^sub>t tcb_Ptr (ptr_val \<acute>regionBase + 0x100) \<longrightarrow> (\<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 (hrs_mem_update (heap_update (PTR(32 word) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbDomain_C''])) \<acute>ksCurDomain) (hrs_mem_update (heap_update (PTR(32 word) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbTimeSlice_C''])) 5) (hrs_mem_update (heap_update (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])) (Arrays.update (h_val (hrs_mem (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs)) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C'']))) (unat Kernel_C.CPSR) (SCAST(32 signed \<rightarrow> 32) (((1 << unat 6) || 0x10) || (1 << unat 8))))) (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs)))) x = hrs_htd \<^bsup>s\<^esup>t_hrs x) \<and> byte_regions_unmodified (hrs_mem_update (heap_update (PTR(32 word) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbDomain_C''])) \<acute>ksCurDomain) (hrs_mem_update (heap_update (PTR(32 word) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbTimeSlice_C''])) 5) (hrs_mem_update (heap_update (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C''])) (Arrays.update (h_val (hrs_mem (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs)) (PTR(32 word[20]) &(PTR(user_context_C) &(PTR(arch_tcb_C) &(tcb_Ptr (ptr_val \<acute>regionBase + 0x100)\<rightarrow>[''tcbArch_C''])\<rightarrow>[''tcbContext_C''])\<rightarrow>[''registers_C'']))) (unat Kernel_C.CPSR) (SCAST(32 signed \<rightarrow> 32) (((1 << unat 6) || 0x10) || (1 << unat 8))))) (hrs_htd_update (\<lambda>x. ptr_retyp (PTR(cte_C[5]) (ptr_val (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val \<acute>regionBase + 0x100)) x)) \<acute>t_hrs)))) \<^bsup>s\<^esup>t_hrs))) \<and> (\<acute>t \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject \<longrightarrow> (\<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> endpoint_C) \<acute>regionBase)) \<acute>t_hrs)) \<longrightarrow> (\<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 (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> endpoint_C) \<acute>regionBase)) \<acute>t_hrs) x = hrs_htd \<^bsup>s\<^esup>t_hrs x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> endpoint_C) \<acute>regionBase)) \<acute>t_hrs) \<^bsup>s\<^esup>t_hrs)) \<and> (\<acute>t \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject \<longrightarrow> (\<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> notification_C) \<acute>regionBase)) \<acute>t_hrs)) \<longrightarrow> (\<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 (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> notification_C) \<acute>regionBase)) \<acute>t_hrs) x = hrs_htd \<^bsup>s\<^esup>t_hrs x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_retyp (PTR_COERCE(unit \<rightarrow> notification_C) \<acute>regionBase)) \<acute>t_hrs) \<^bsup>s\<^esup>t_hrs)) \<and> (\<acute>t \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject \<longrightarrow> (\<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject \<longrightarrow> True \<longrightarrow> htd_safe domain (hrs_htd \<acute>t_hrs) \<and> htd_safe domain (hrs_htd (hrs_htd_update (ptr_arr_retyps (2 ^ unat \<acute>userSize) (PTR_COERCE(unit \<rightarrow> cte_C) \<acute>regionBase)) \<acute>t_hrs)) \<longrightarrow> (\<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 (hrs_htd_update (ptr_arr_retyps (2 ^ unat \<acute>userSize) (PTR_COERCE(unit \<rightarrow> cte_C) \<acute>regionBase)) \<acute>t_hrs) x = hrs_htd \<^bsup>s\<^esup>t_hrs x) \<and> byte_regions_unmodified (hrs_htd_update (ptr_arr_retyps (2 ^ unat \<acute>userSize) (PTR_COERCE(unit \<rightarrow> cte_C) \<acute>regionBase)) \<acute>t_hrs) \<^bsup>s\<^esup>t_hrs)) \<and> (\<acute>t \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject \<longrightarrow> (\<acute>t = SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject \<longrightarrow> (\<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)) \<and> (\<acute>t \<noteq> SCAST(32 signed \<rightarrow> 32) seL4_UntypedObject \<longrightarrow> (True \<longrightarrow> \<not> False) \<and> (\<not> True \<longrightarrow> False \<longrightarrow> (\<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 (4 subgoals):
 1. \<And>s nt xa. \<lbrakk>\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR(cte_C[5]) (ptr_val (regionBase_' s) + 0x100 - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s))))); ptr_retyp (PTR(cte_C[5]) (ptr_val (regionBase_' s) + 0x100 - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s)))) \<Turnstile>\<^sub>t tcb_Ptr (ptr_val (regionBase_' s) + 0x100); Kernel_C.CPSR <s 0x14; 0 \<le>s Kernel_C.CPSR; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyp (PTR(cte_C[5]) (ptr_val (regionBase_' s) + 0x100 - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s)))) xa = hrs_htd (t_hrs_' (globals s)) xa
 2. \<And>s nt xa. \<lbrakk>\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject; seL4_EndpointObject \<noteq> seL4_TCBObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> endpoint_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); t_' s = SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyp (PTR_COERCE(unit \<rightarrow> endpoint_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 3. \<And>s nt xa. \<lbrakk>\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject; seL4_NotificationObject \<noteq> seL4_TCBObject; seL4_NotificationObject \<noteq> seL4_EndpointObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> notification_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); t_' s = SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_retyp (PTR_COERCE(unit \<rightarrow> notification_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa
 4. \<And>s nt xa. \<lbrakk>\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject; seL4_CapTableObject \<noteq> seL4_TCBObject; seL4_CapTableObject \<noteq> seL4_EndpointObject; seL4_CapTableObject \<noteq> seL4_NotificationObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_arr_retyps (2 ^ unat (userSize_' s)) (PTR_COERCE(unit \<rightarrow> cte_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); t_' s = SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}\<rbrakk> \<Longrightarrow> ptr_arr_retyps (2 ^ unat (userSize_' s)) (PTR_COERCE(unit \<rightarrow> cte_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s))) xa = hrs_htd (t_hrs_' (globals s)) xa proof (prove)
goal (5 subgoals):
 1. \<And>s nt xa. \<lbrakk>\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR(cte_C[5]) (ptr_val (regionBase_' s) + 0x100 - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s))))); ptr_retyp (PTR(cte_C[5]) (ptr_val (regionBase_' s) + 0x100 - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s)))) \<Turnstile>\<^sub>t tcb_Ptr (ptr_val (regionBase_' s) + 0x100); Kernel_C.CPSR <s 0x14; 0 \<le>s Kernel_C.CPSR; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> ptr_span (PTR(cte_C[5]) (ptr_val (regionBase_' s) + 0x100 - ctcb_offset))\<rbrakk> \<Longrightarrow> False
 2. \<And>s nt xa. \<lbrakk>\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR(cte_C[5]) (ptr_val (regionBase_' s) + 0x100 - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s))))); ptr_retyp (PTR(cte_C[5]) (ptr_val (regionBase_' s) + 0x100 - ctcb_offset)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s)))) \<Turnstile>\<^sub>t tcb_Ptr (ptr_val (regionBase_' s) + 0x100); Kernel_C.CPSR <s 0x14; 0 \<le>s Kernel_C.CPSR; t_' s = SCAST(32 signed \<rightarrow> 32) seL4_TCBObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> ptr_span (tcb_Ptr (ptr_val (regionBase_' s) + 0x100))\<rbrakk> \<Longrightarrow> False
 3. \<And>s nt xa. \<lbrakk>\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject; seL4_EndpointObject \<noteq> seL4_TCBObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> endpoint_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); t_' s = SCAST(32 signed \<rightarrow> 32) seL4_EndpointObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> ptr_span (PTR_COERCE(unit \<rightarrow> endpoint_C) (regionBase_' s))\<rbrakk> \<Longrightarrow> False
 4. \<And>s nt xa. \<lbrakk>\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject; seL4_NotificationObject \<noteq> seL4_TCBObject; seL4_NotificationObject \<noteq> seL4_EndpointObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> notification_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); t_' s = SCAST(32 signed \<rightarrow> 32) seL4_NotificationObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> ptr_span (PTR_COERCE(unit \<rightarrow> notification_C) (regionBase_' s))\<rbrakk> \<Longrightarrow> False
 5. \<And>s nt xa. \<lbrakk>\<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject; seL4_CapTableObject \<noteq> seL4_TCBObject; seL4_CapTableObject \<noteq> seL4_EndpointObject; seL4_CapTableObject \<noteq> seL4_NotificationObject; object_type_from_H nt = SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_arr_retyps (2 ^ unat (userSize_' s)) (PTR_COERCE(unit \<rightarrow> cte_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); t_' s = SCAST(32 signed \<rightarrow> 32) seL4_CapTableObject; xa \<notin> {ptr_val (regionBase_' s)..+2 ^ APIType_capBits nt (unat (userSize_' s))}; xa \<in> {ptr_val (PTR_COERCE(unit \<rightarrow> cte_C) (regionBase_' s))..+2 ^ unat (userSize_' s) * size_of TYPE(cte_C)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s nt xa x1. \<lbrakk>xa \<in> {ptr_val (regionBase_' s)..+80}; \<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> 1; nt = APIObjectType ArchTypes_H.apiobject_type.TCBObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> cte_C[5]) (regionBase_' s)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s))))); ptr_retyp (PTR_COERCE(unit \<rightarrow> cte_C[5]) (regionBase_' s)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s)))) \<Turnstile>\<^sub>t tcb_Ptr (ptr_val (regionBase_' s) + 0x100); Kernel_C.CPSR <s 0x14; 0 \<le>s Kernel_C.CPSR; t_' s = 1; x1 = ArchTypes_H.apiobject_type.TCBObject; xa \<notin> {ptr_val (regionBase_' s)..+512}\<rbrakk> \<Longrightarrow> False
 2. \<And>s nt xa x1. \<lbrakk>xa \<in> {ptr_val (regionBase_' s) + 0x100..+152}; \<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> 1; nt = APIObjectType ArchTypes_H.apiobject_type.TCBObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_retyp (PTR_COERCE(unit \<rightarrow> cte_C[5]) (regionBase_' s)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s))))); ptr_retyp (PTR_COERCE(unit \<rightarrow> cte_C[5]) (regionBase_' s)) (ptr_retyp (tcb_Ptr (ptr_val (regionBase_' s) + 0x100)) (hrs_htd (t_hrs_' (globals s)))) \<Turnstile>\<^sub>t tcb_Ptr (ptr_val (regionBase_' s) + 0x100); Kernel_C.CPSR <s 0x14; 0 \<le>s Kernel_C.CPSR; t_' s = 1; x1 = ArchTypes_H.apiobject_type.TCBObject; xa \<notin> {ptr_val (regionBase_' s)..+512}\<rbrakk> \<Longrightarrow> False
 3. \<And>s nt xa x1. \<lbrakk>xa \<in> {ptr_val (regionBase_' s)..+2 ^ unat (userSize_' s) * 16}; \<not> SCAST(32 signed \<rightarrow> 32) seL4_NonArchObjectTypeCount \<le> 4; nt = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; htd_safe domain (hrs_htd (t_hrs_' (globals s))); htd_safe domain (ptr_arr_retyps (2 ^ unat (userSize_' s)) (PTR_COERCE(unit \<rightarrow> cte_C) (regionBase_' s)) (hrs_htd (t_hrs_' (globals s)))); t_' s = 4; x1 = ArchTypes_H.apiobject_type.CapTableObject; xa \<notin> {ptr_val (regionBase_' s)..+16 * 2 ^ unat (userSize_' s)}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!