theory Ctac

lemma ccorres_lift_rhs_Basic:
  assumes cc: "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (d' v)"
  and  xfxfu: "\<And>v s. xf' (xfu' (\<lambda>_. v) s) = v"
  and   ceqv: "\<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' d (d' rv')"
  and     gg: "\<And>x f s. globals (xfu' f s) = globals s"
  (* WARNING: the tactic csymbr relies on the outermost variable being of the same type as the return type of xf' *)
  (*  and    Pig: "\<And>x (s :: cstate) v'. P' x (i s) \<Longrightarrow> P' x (i (xfu' (\<lambda>_. x) s))" *)
  (* The concrete guard here is stronger than required --- we really need xf'' t not v *)
  shows   "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G {s. xfu' (\<lambda>_. v) s \<in> G'}  hs a (Basic (xfu' (\<lambda>_. v)) ;; d)"
  (is "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G ?G' hs a (?c ;; d)") proof (subst return_bind [where x = "()" and f = "\<lambda>_. a", symmetric],
    rule ccorres_guard_imp [OF ccorres_split_nothrow, OF _ ceqv]) show "ccorres dc xf' \<top> UNIV hs (return ()) ?c" apply (rule ccorres_noop) apply (vcg spec=modifies) done next fix rv' show "ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' \<inter> {s. rv' = v}) hs a (d' rv')" apply (rule ccorres_gen_asm2) apply (erule ssubst) apply (rule cc) done next show "\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>" by wp next show "\<Gamma>\<turnstile> ?G' ?c {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' \<inter> {_. xf' s = v}}" apply vcg apply (clarsimp simp add: xfxfu) done qed simp_all

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G {s. xfu' (\<lambda>_. v) s \<in> G'} hs a (Basic (xfu' (\<lambda>_. v));;
d) proof (state)
goal (6 subgoals):
 1. ccorres ?r'1 xf' ?P1 ?P'1 hs (return ()) (Basic (xfu' (\<lambda>_. v)))
 2. \<And>uu_ rv'. ?r'1 uu_ rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q1 uu_) (?Q'1 uu_ rv') hs a (d' rv')
 3. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 4. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. v)) {s. \<forall>uu_. ?r'1 uu_ (xf' s) \<longrightarrow> s \<in> ?Q'1 uu_ (xf' s)}
 5. \<And>s. G s \<Longrightarrow> (?P1 and ?R1) s
 6. \<And>s. s \<in> {s. xfu' (\<lambda>_. v) s \<in> G'} \<Longrightarrow> s \<in> ?P'1 \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. ccorres dc xf' (\<lambda>_. True) UNIV hs (return ()) (Basic (xfu' (\<lambda>_. v))) proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Basic (xfu' (\<lambda>_. v)) {t. t may_not_modify_globals s} proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres dc xf' (\<lambda>_. True) UNIV hs (return ()) (Basic (xfu' (\<lambda>_. v)))

goal (5 subgoals):
 1. \<And>uu_ rv'. dc uu_ rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q1 uu_) (?Q'1 uu_ rv') hs a (d' rv')
 2. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. v)) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> ?Q'1 uu_ (xf' s)}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. xfu' (\<lambda>_. v) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (state)
goal (5 subgoals):
 1. \<And>uu_ rv'. dc uu_ rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q1 uu_) (?Q'1 uu_ rv') hs a (d' rv')
 2. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. v)) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> ?Q'1 uu_ (xf' s)}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. xfu' (\<lambda>_. v) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (state)
goal (5 subgoals):
 1. \<And>uu_ rv'. dc uu_ rv' \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf (?Q1 uu_) (?Q'1 uu_ rv') hs a (d' rv')
 2. \<lbrace>?R1\<rbrace> return () \<lbrace>?Q1\<rbrace>
 3. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. v)) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> ?Q'1 uu_ (xf' s)}
 4. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 5. \<And>s. s \<in> {s. xfu' (\<lambda>_. v) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' \<inter> \<lbrace>rv' = v\<rbrace>) hs a (d' rv') proof (prove)
goal (1 subgoal):
 1. rv' = v \<Longrightarrow> ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (d' rv') proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> r xf arrel axf G G' hs a (d' v) proof (prove)
goal:
No subgoals! proof (state)
this:
ccorres_underlying rf_sr \<Gamma> r xf arrel axf G (G' \<inter> \<lbrace>rv' = v\<rbrace>) hs a (d' rv')

goal (4 subgoals):
 1. \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. v)) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>xf' s = v\<rbrace>}
 3. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 4. \<And>s. s \<in> {s. xfu' (\<lambda>_. v) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (state)
goal (4 subgoals):
 1. \<lbrace>?R1\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>
 2. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. v)) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>xf' s = v\<rbrace>}
 3. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and ?R1) s
 4. \<And>s. s \<in> {s. xfu' (\<lambda>_. v) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. \<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace> proof (state)
this:
\<lbrace>G\<rbrace> return () \<lbrace>\<lambda>_. G\<rbrace>

goal (3 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. v)) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>xf' s = v\<rbrace>}
 2. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and G) s
 3. \<And>s. s \<in> {s. xfu' (\<lambda>_. v) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (state)
goal (3 subgoals):
 1. \<Gamma>\<turnstile>\<^bsub>/?F1\<^esub> ?R'1 Basic (xfu' (\<lambda>_. v)) {s. \<forall>uu_. dc uu_ (xf' s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>xf' s = v\<rbrace>}
 2. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and G) s
 3. \<And>s. s \<in> {s. xfu' (\<lambda>_. v) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> ?R'1 proof (prove)
goal (1 subgoal):
 1. \<Gamma>\<turnstile> {s. xfu' (\<lambda>_. v) s \<in> G'} Basic (xfu' (\<lambda>_. v)) {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>xf' s = v\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>t_hrs phantom_machine_state ghost'state avail_reg ksNumCPUs ndks_boot active_irq rootserver ksCurDomain ksCurThread ksDomainTime ksIdleThread tlbLockCount armKSNextASID current_fault ksReadyQueues armKSASIDTable rootserver_mem armKSHWASIDTable intStateIRQTable ksDomScheduleIdx ksSchedulerAction current_extra_caps isFPUEnabledCached current_lookup_fault ksWorkUnitsCompleted current_syscall_error ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap more global_exn_var ret__struct_create_frames_of_region_ret_C ret__struct_create_mappings_pte_return_C ret__struct_create_mappings_pde_return_C ret__struct_resolveAddressBits_ret_C ret__struct_lookupCapAndSlot_ret_C ret__struct_lookupSlot_raw_ret_C ret__struct_findPDForASID_ret_C ret__struct_seL4_MessageInfo_C ret__struct_lookupPTSlot_ret_C ret__struct_finaliseSlot_ret_C ret__struct_seL4_SlotRegion_C ret__struct_finaliseCap_ret_C ret__struct_seL4_CapRights_C ret__struct_lookupSlot_ret_C ret__struct_vm_attributes_C ret__struct_lookupCap_ret_C ret__struct_deriveCap_ret_C ret__struct_lookup_fault_C ret__struct_cap_transfer_C ret__struct_resolve_ret_C ret__ptr_to_unsigned_long ret__struct_seL4_Fault_C ret__ptr_to_struct_tcb_C ret__ptr_to_struct_pte_C ret__ptr_to_struct_pde_C ret__ptr_to_struct_cte_C ret__struct_tcb_queue_C ret__struct_p_region_C ret__struct_mdb_node_C original_lookup_fault unsigned_long_eret_4 unsigned_long_eret_3 unsigned_long_eret_2 ret__struct_region_C struct_cap_C_eret_3 struct_cap_C_eret_2 extra_bi_frame_vptr seL4_CNode_CapData ret__unsigned_long ret__unsigned_char ptr_to_void_eret_2 first_untyped_slot extra_bi_size_bits capPTMappedAddress capFMappedASIDHigh boot_mem_reuse_reg tlbflush_required stored_asid_valid ret__struct_pte_C ret__struct_pde_C ret__struct_cap_C receiverIPCBuffer newCapIsRevocable create_frames_ret capNtfnCanReceive capFMappedAddress capFMappedASIDLow capCNodeGuardSize untypedFreeBytes thread_state_ptr size_unique_name seL4_MessageInfo scheduler_action ret__ptr_to_void receiveIPCBuffer prevIsSameObject notification_ptr l1index_inverted instructionFault capReplyCanGrant capReplyCanGrant___unsigned_long capCanGrantReply armParityEnabled armPageCacheable unsigned_eret_6 unsigned_eret_5 unsigned_eret_4 unsigned_eret_3 unsigned_eret_2 unaligned_start transferInteger totalObjectSize slot_pos_before extra_bi_region extra_bi_offset cnode_size_bits cap_rights_mask capPTMappedASID capPDMappedASID armExecuteNever ui_p_reg_start stored_hw_asid stored_hw_asid___struct_pde_C slot_pos_after seL4_CapRights root_cnode_cap msgTransferred mdbFirstBadged mdbFirstBadged___unsigned_long inReceivePhase hw_asid_offset currentPDEType cptr_bufferPtr capReplyMaster capReplyMaster___unsigned_long capNtfnCanSend alignedFreeRef vm_attributes vRoot_srcSlot transferFrame syscallNumber suspendSource stack_address root_switched ret__unsigned ret__longlong replyCanGrant receiveBuffer___ptr_to_void receiveBuffer nonexecutable mva_plus_asid fpsid_subarch extra_bi_size dtb_phys_addr device_memory cmp_size_bits capsUnwrapped capZombieType capPTIsMapped capPDIsMapped capCanReceive capCNodeRadix capCNodeGuard canGrantReply cRoot_srcSlot bufferSrcSlot bi_frame_vptr was_runnable w_rightsMask vm_faultType vRoot_newCap ui_p_reg_end transferArch thread_state resumeTarget processor_id pivotNewData nextFreeArea mdb_node_ptr mdbRevocable mdbRevocable___unsigned_long lookup_fault extra_bi_ret epQueue_tail epQueue_head endpoint_ptr endpointTail dtb_phys_end deviceMemory cap_type_tag capPTBasePtr capPDBasePtr capNtfnBadge capFreeIndex capFVMRights capFIsDevice capBlockSize cRoot_newCap w_bufferPtr userObjSize updateFlags resolve_ret pte_entries pde_entries new_hw_asid newPivotCap n_available ipcbuf_vptr instruction handlerSlot handlerCPtr empty_index controlSlot cleanupInfo capZombieID capVMRights capIsDevice capFBasePtr capFBasePtr___unsigned_long capCanGrant capCNodePtr capASIDPool capASIDBase ui_v_entry threadRoot targetSlot targetSlot___ptr_to_struct_pde_C srcNewData source_cap sendBuffer___ptr_to_void sendBuffer seL4_Fault retypeBase regionBase pivotIndex pivotDepth parentSlot objectSize ntfn_queue nodeWindow nodeOffset n_reserved isReceiver isBlocking ipcbuf_cap ipc_buffer int_eret_3 int_eret_2 handlerCap guardFound fault_type extra_size executable dtb_addr_p destOffset destLength derivedCap cur_thread csselr_old cap_rights capNtfnPtr capEPBadge capCanSend callerSlot bufferSlot bufferAddr block_size attributes assoc_bits align_bits StrictC'_v vm_rights vbase_ptr vRootSlot vRootData use_large threadPtr stack_top size_bits size_bits___unsigned ret__long replySlot radixBits pv_offset pivotSlot pivotRoot pdCapSlot page_size page_base num_nodes nodeIndex nodeDepth newVTable newSrcCap masterCap levelBits it_pd_cap it_ap_cap ipcBuffer immediate haveHWFPU guardSize guardBits global_pd freeIndex frame_cap frameSize faultType extraCaps dtb_p_reg destCNode capTCBPtr capTCBPtr___unsigned_long candidate callerCap callerCap___ptr_to_struct_cte_C cacheable cRootSlot cRootData bufferPtr bufferCap bitsFound base_addr baseValue available asid_base allocated alignment vmRights vRootCap userSize ui_v_reg ui_p_reg transfer tls_base tcb_dest srcIndex srcDepth slot_ptr rootSlot ret__int reserved reserved___ptr_to_struct_region_C receiver priority prev_ptr prev_cap preserve prefetch pagesize pageBits ntfn_cap node_ptr nodeSize next_ptr mdb_node it_v_reg isSource irqState inverted invLabel invLabel___int find_ret fastfail endpoint dtb_size___unsigned_long dtb_size destSlot data_ram cnodeCap clzl_ret cap_type capIndex capGuard capFSize capEPPtr canGrant cRootCap boundTCB blocking bitsLeft asidPool archInfo v_entry untyped trigger tcb_src tag_ram syscall srcSlot srcRoot sendBuf rootCap restart res_ret recvBuf ptr_src ptr_dst pte_ptr pt_vptr ptIndex poolPtr pde_ptr pdIndex pdIndex___unsigned_long ntfnPtr ntfnCap node_id nodeCap nextPtr new_cap newType newPrio newData msgInfo msgInfo___struct_seL4_MessageInfo_C mdbPrev mdbPrev___unsigned_long mdbNode mdbNext mdbNext___unsigned_long map_ret map_ret___struct_create_mappings_pde_return_C lus_ret lufType luc_ret l2index l1index irqSlot initial hw_asid freeRef faultep faultEP exposed endSlot do_call disable destCap cte_ptr context cap_ptr capData basePtr authTCB authCap address z_slot w_bits ut_cap ui_reg ts_ptr tsType thread tcbptr target___unsigned target___unsigned_char target status srcTCB srcMDB srcCap sender result pt_cap ptSlot pstart pd_val pd_cap pdSlot parity parent offset offset___unsigned_long offset___int number number___unsigned_long newMcp newMDB newCap n_bits maxlen lu_ret lu_ret___struct_lookupCap_ret_C lu_ret___struct_lookupPTSlot_ret_C lu_ret___struct_lookupSlot_ret_C lu_ret___struct_lookupSlot_raw_ret_C length length___unsigned_long isMove isCall htpidr header fs_ret fc_ret ep_ref ep_ptr ep_cap epCPtr domain do_map dc_ret ctSlot capptr cap_pd capPtr capIRQ caller buffer badge2 ap_cap Domain vaddr v_reg state state___ptr_to_struct_thread_state_C start slot3 slot2 slot1 size2 reset radix queue pdCap paddr p_reg nsets nirqs newPD level lbits label label___unsigned_long irq_w index index___int guard grant frame frame___ptr_to_struct_kernel_frame_C fpsid fpexc flags final fault fault___unsigned_long epptr depth cte_b cte_a cptr2 cpacr count cnode chunk cap_b cap_a block badge bBase assoc aifsr adfsr actlr aBase AIFSR ADFSR ACTLR wptr word vtop vptr type tptr topB topA tcap tCap slot size size___unsigned_long sent root ptr2 prrr prio prev pptr pptr___unsigned_long pool phys ntfn nmrr next next___ptr_to_struct_tcb_C mdb2 mdb1 mask mask___unsigned mask___unsigned_longlong line info ifsr ifar idx2 diff dfsr dfar dest dest___ptr_to_char data ctag cptr code clid cidr cap2 cap1 call cPtr botB botA bits bits___unsigned base base___unsigned bTop auth attr asid arch addr addr___unsigned aTop PRRR NMRR IFSR IFAR DFSR DFAR CLID CIDR wsl w_b w_a val val___long v32 tex tcb tag str src src___ptr_to_char scr ret ret___unsigned_long ret___struct_findPDForASID_ret_C ret___struct_lookupPTSlot_ret_C ret___struct_resolve_ret_C ret___struct_create_mappings_pte_return_C ret___struct_create_mappings_pde_return_C ret___struct_deriveCap_ret_C ret___struct_lookupCap_ret_C ret___struct_lookupCapAndSlot_ret_C ret___struct_lookupSlot_raw_ret_C ret___struct_lookupSlot_ret_C ret___struct_resolveAddressBits_ret_C ret___struct_finaliseSlot_ret_C res reg reg___struct_region_C reg___struct_p_region_C ptr ptr___ptr_to_unsigned_long ptr___ptr_to_struct_cte_C pte pte___ptr_to_struct_pte_C pde pde___ptr_to_struct_pde_C msb mdb mcp max luf lou loc len irq idx ex1 end dom cte cpu cap bit aux acr TEX FSR FAR APX ts sz s2 s1 pt pd pd___struct_cap_C pd___struct_findPDForASID_ret_C pc pa nG mi id id___anonymous_enum ep ct bi ap ap___unsigned_long XN AP y y___int x x___unsigned_longlong x___unsigned_long x___int w w___int w___struct_seL4_CNode_CapData_C va v___int v___unsigned t s___unsigned_long s___ptr_to_char s r r___ptr_to_struct_p_region_C r___ptr_to_struct_region_C q p p___ptr_to_unsigned_char n n___int m l j i i___unsigned i___int f e c c___char b a S P C B morea. xfu' (\<lambda>_. v) \<lparr>globals = \<lparr>t_hrs_' = t_hrs, phantom_machine_state_' = phantom_machine_state, ghost'state_' = ghost'state, avail_reg_' = avail_reg, ksNumCPUs_' = ksNumCPUs, ndks_boot_' = ndks_boot, active_irq_' = active_irq, rootserver_' = rootserver, ksCurDomain_' = ksCurDomain, ksCurThread_' = ksCurThread, ksDomainTime_' = ksDomainTime, ksIdleThread_' = ksIdleThread, tlbLockCount_' = tlbLockCount, armKSNextASID_' = armKSNextASID, current_fault_' = current_fault, ksReadyQueues_' = ksReadyQueues, armKSASIDTable_' = armKSASIDTable, rootserver_mem_' = rootserver_mem, armKSHWASIDTable_' = armKSHWASIDTable, intStateIRQTable_' = intStateIRQTable, ksDomScheduleIdx_' = ksDomScheduleIdx, ksSchedulerAction_' = ksSchedulerAction, current_extra_caps_' = current_extra_caps, isFPUEnabledCached_' = isFPUEnabledCached, current_lookup_fault_' = current_lookup_fault, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted, current_syscall_error_' = current_syscall_error, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap, \<dots> = more\<rparr>, global_exn_var_' = global_exn_var, ret__struct_create_frames_of_region_ret_C_' = ret__struct_create_frames_of_region_ret_C, ret__struct_create_mappings_pte_return_C_' = ret__struct_create_mappings_pte_return_C, ret__struct_create_mappings_pde_return_C_' = ret__struct_create_mappings_pde_return_C, ret__struct_resolveAddressBits_ret_C_' = ret__struct_resolveAddressBits_ret_C, ret__struct_lookupCapAndSlot_ret_C_' = ret__struct_lookupCapAndSlot_ret_C, ret__struct_lookupSlot_raw_ret_C_' = ret__struct_lookupSlot_raw_ret_C, ret__struct_findPDForASID_ret_C_' = ret__struct_findPDForASID_ret_C, ret__struct_seL4_MessageInfo_C_' = ret__struct_seL4_MessageInfo_C, ret__struct_lookupPTSlot_ret_C_' = ret__struct_lookupPTSlot_ret_C, ret__struct_finaliseSlot_ret_C_' = ret__struct_finaliseSlot_ret_C, ret__struct_seL4_SlotRegion_C_' = ret__struct_seL4_SlotRegion_C, ret__struct_finaliseCap_ret_C_' = ret__struct_finaliseCap_ret_C, ret__struct_seL4_CapRights_C_' = ret__struct_seL4_CapRights_C, ret__struct_lookupSlot_ret_C_' = ret__struct_lookupSlot_ret_C, ret__struct_vm_attributes_C_' = ret__struct_vm_attributes_C, ret__struct_lookupCap_ret_C_' = ret__struct_lookupCap_ret_C, ret__struct_deriveCap_ret_C_' = ret__struct_deriveCap_ret_C, ret__struct_lookup_fault_C_' = ret__struct_lookup_fault_C, ret__struct_cap_transfer_C_' = ret__struct_cap_transfer_C, ret__struct_resolve_ret_C_' = ret__struct_resolve_ret_C, ret__ptr_to_unsigned_long_' = ret__ptr_to_unsigned_long, ret__struct_seL4_Fault_C_' = ret__struct_seL4_Fault_C, ret__ptr_to_struct_tcb_C_' = ret__ptr_to_struct_tcb_C, ret__ptr_to_struct_pte_C_' = ret__ptr_to_struct_pte_C, ret__ptr_to_struct_pde_C_' = ret__ptr_to_struct_pde_C, ret__ptr_to_struct_cte_C_' = ret__ptr_to_struct_cte_C, ret__struct_tcb_queue_C_' = ret__struct_tcb_queue_C, ret__struct_p_region_C_' = ret__struct_p_region_C, ret__struct_mdb_node_C_' = ret__struct_mdb_node_C, original_lookup_fault___struct_lookup_fault_C_' = original_lookup_fault, unsigned_long_eret_4_' = unsigned_long_eret_4, unsigned_long_eret_3_' = unsigned_long_eret_3, unsigned_long_eret_2_' = unsigned_long_eret_2, ret__struct_region_C_' = ret__struct_region_C, struct_cap_C_eret_3_' = struct_cap_C_eret_3, struct_cap_C_eret_2_' = struct_cap_C_eret_2, extra_bi_frame_vptr___unsigned_long_' = extra_bi_frame_vptr, seL4_CNode_CapData___struct_seL4_CNode_CapData_C_' = seL4_CNode_CapData, ret__unsigned_long_' = ret__unsigned_long, ret__unsigned_char_' = ret__unsigned_char, ptr_to_void_eret_2_' = ptr_to_void_eret_2, first_untyped_slot___unsigned_long_' = first_untyped_slot, extra_bi_size_bits___unsigned_long_' = extra_bi_size_bits, capPTMappedAddress___unsigned_' = capPTMappedAddress, capFMappedASIDHigh___unsigned_' = capFMappedASIDHigh, boot_mem_reuse_reg___struct_region_C_' = boot_mem_reuse_reg, tlbflush_required___unsigned_long_' = tlbflush_required, stored_asid_valid___unsigned_' = stored_asid_valid, ret__struct_pte_C_' = ret__struct_pte_C, ret__struct_pde_C_' = ret__struct_pde_C, ret__struct_cap_C_' = ret__struct_cap_C, receiverIPCBuffer___ptr_to_unsigned_long_' = receiverIPCBuffer, newCapIsRevocable___unsigned_long_' = newCapIsRevocable, create_frames_ret___struct_create_frames_of_region_ret_C_' = create_frames_ret, capNtfnCanReceive___unsigned_' = capNtfnCanReceive, capFMappedAddress___unsigned_' = capFMappedAddress, capFMappedASIDLow___unsigned_' = capFMappedASIDLow, capCNodeGuardSize___unsigned_' = capCNodeGuardSize, untypedFreeBytes___unsigned_long_' = untypedFreeBytes, thread_state_ptr___ptr_to_struct_thread_state_C_' = thread_state_ptr, size_unique_name___unsigned_long_' = size_unique_name, seL4_MessageInfo___struct_seL4_MessageInfo_C_' = seL4_MessageInfo, scheduler_action___ptr_to_struct_tcb_C_' = scheduler_action, ret__ptr_to_void_' = ret__ptr_to_void, receiveIPCBuffer___ptr_to_unsigned_long_' = receiveIPCBuffer, prevIsSameObject___unsigned_long_' = prevIsSameObject, notification_ptr___ptr_to_struct_notification_C_' = notification_ptr, l1index_inverted___unsigned_long_' = l1index_inverted, instructionFault___unsigned_' = instructionFault, capReplyCanGrant___unsigned_' = capReplyCanGrant, capReplyCanGrant___unsigned_long_' = capReplyCanGrant___unsigned_long, capCanGrantReply___unsigned_' = capCanGrantReply, armParityEnabled___unsigned_' = armParityEnabled, armPageCacheable___unsigned_' = armPageCacheable, unsigned_eret_6_' = unsigned_eret_6, unsigned_eret_5_' = unsigned_eret_5, unsigned_eret_4_' = unsigned_eret_4, unsigned_eret_3_' = unsigned_eret_3, unsigned_eret_2_' = unsigned_eret_2, unaligned_start___unsigned_long_' = unaligned_start, transferInteger___unsigned_long_' = transferInteger, totalObjectSize___unsigned_long_' = totalObjectSize, slot_pos_before___unsigned_long_' = slot_pos_before, extra_bi_region___struct_region_C_' = extra_bi_region, extra_bi_offset___unsigned_long_' = extra_bi_offset, cnode_size_bits___unsigned_long_' = cnode_size_bits, cap_rights_mask___struct_seL4_CapRights_C_' = cap_rights_mask, capPTMappedASID___unsigned_' = capPTMappedASID, capPDMappedASID___unsigned_' = capPDMappedASID, armExecuteNever___unsigned_' = armExecuteNever, ui_p_reg_start___unsigned_long_' = ui_p_reg_start, stored_hw_asid___unsigned_' = stored_hw_asid, stored_hw_asid___struct_pde_C_' = stored_hw_asid___struct_pde_C, slot_pos_after___unsigned_long_' = slot_pos_after, seL4_CapRights___struct_seL4_CapRights_C_' = seL4_CapRights, root_cnode_cap___struct_cap_C_' = root_cnode_cap, msgTransferred___unsigned_long_' = msgTransferred, mdbFirstBadged___unsigned_' = mdbFirstBadged, mdbFirstBadged___unsigned_long_' = mdbFirstBadged___unsigned_long, inReceivePhase___unsigned_' = inReceivePhase, hw_asid_offset___unsigned_long_' = hw_asid_offset, currentPDEType___enum_pde_tag_' = currentPDEType, cptr_bufferPtr___unsigned_long_' = cptr_bufferPtr, capReplyMaster___unsigned_' = capReplyMaster, capReplyMaster___unsigned_long_' = capReplyMaster___unsigned_long, capNtfnCanSend___unsigned_' = capNtfnCanSend, alignedFreeRef___unsigned_long_' = alignedFreeRef, vm_attributes___struct_vm_attributes_C_' = vm_attributes, vRoot_srcSlot___ptr_to_struct_cte_C_' = vRoot_srcSlot, transferFrame___unsigned_long_' = transferFrame, syscallNumber___unsigned_' = syscallNumber, suspendSource___unsigned_long_' = suspendSource, stack_address___unsigned_long_' = stack_address, root_switched___unsigned_long_' = root_switched, ret__unsigned_' = ret__unsigned, ret__longlong_' = ret__longlong, replyCanGrant___unsigned_long_' = replyCanGrant, receiveBuffer___ptr_to_void_' = receiveBuffer___ptr_to_void, receiveBuffer___ptr_to_unsigned_long_' = receiveBuffer, nonexecutable___unsigned_long_' = nonexecutable, mva_plus_asid___unsigned_long_' = mva_plus_asid, fpsid_subarch___unsigned_long_' = fpsid_subarch, extra_bi_size___unsigned_long_' = extra_bi_size, dtb_phys_addr___unsigned_long_' = dtb_phys_addr, device_memory___unsigned_long_' = device_memory, cmp_size_bits___unsigned_long_' = cmp_size_bits, capsUnwrapped___unsigned_' = capsUnwrapped, capZombieType___unsigned_' = capZombieType, capPTIsMapped___unsigned_' = capPTIsMapped, capPDIsMapped___unsigned_' = capPDIsMapped, capCanReceive___unsigned_' = capCanReceive, capCNodeRadix___unsigned_' = capCNodeRadix, capCNodeGuard___unsigned_' = capCNodeGuard, canGrantReply___unsigned_long_' = canGrantReply, cRoot_srcSlot___ptr_to_struct_cte_C_' = cRoot_srcSlot, bufferSrcSlot___ptr_to_struct_cte_C_' = bufferSrcSlot, bi_frame_vptr___unsigned_long_' = bi_frame_vptr, was_runnable___unsigned_long_' = was_runnable, w_rightsMask___unsigned_long_' = w_rightsMask, vm_faultType___unsigned_long_' = vm_faultType, vRoot_newCap___struct_cap_C_' = vRoot_newCap, ui_p_reg_end___unsigned_long_' = ui_p_reg_end, transferArch___unsigned_long_' = transferArch, thread_state___struct_thread_state_C_' = thread_state, resumeTarget___unsigned_long_' = resumeTarget, processor_id___unsigned_long_' = processor_id, pivotNewData___unsigned_long_' = pivotNewData, nextFreeArea___ptr_to_void_' = nextFreeArea, mdb_node_ptr___ptr_to_struct_mdb_node_C_' = mdb_node_ptr, mdbRevocable___unsigned_' = mdbRevocable, mdbRevocable___unsigned_long_' = mdbRevocable___unsigned_long, lookup_fault___struct_lookup_fault_C_' = lookup_fault, extra_bi_ret___struct_create_frames_of_region_ret_C_' = extra_bi_ret, epQueue_tail___unsigned_long_' = epQueue_tail, epQueue_head___unsigned_long_' = epQueue_head, endpoint_ptr___ptr_to_struct_endpoint_C_' = endpoint_ptr, endpointTail___ptr_to_struct_tcb_C_' = endpointTail, dtb_phys_end___unsigned_long_' = dtb_phys_end, deviceMemory___unsigned_long_' = deviceMemory, cap_type_tag___unsigned_' = cap_type_tag, capPTBasePtr___unsigned_' = capPTBasePtr, capPDBasePtr___unsigned_' = capPDBasePtr, capNtfnBadge___unsigned_' = capNtfnBadge, capFreeIndex___unsigned_' = capFreeIndex, capFVMRights___unsigned_' = capFVMRights, capFIsDevice___unsigned_' = capFIsDevice, capBlockSize___unsigned_' = capBlockSize, cRoot_newCap___struct_cap_C_' = cRoot_newCap, w_bufferPtr___unsigned_long_' = w_bufferPtr, userObjSize___unsigned_long_' = userObjSize, updateFlags___unsigned_long_' = updateFlags, resolve_ret___struct_resolve_ret_C_' = resolve_ret, pte_entries___struct_pte_range_C_' = pte_entries, pde_entries___struct_pde_range_C_' = pde_entries, new_hw_asid___unsigned_char_' = new_hw_asid, newPivotCap___struct_cap_C_' = newPivotCap, n_available___unsigned_long_' = n_available, ipcbuf_vptr___unsigned_long_' = ipcbuf_vptr, instruction___unsigned_long_' = instruction, handlerSlot___ptr_to_struct_cte_C_' = handlerSlot, handlerCPtr___unsigned_long_' = handlerCPtr, empty_index___int_' = empty_index, controlSlot___ptr_to_struct_cte_C_' = controlSlot, cleanupInfo___struct_cap_C_' = cleanupInfo, capZombieID___unsigned_' = capZombieID, capVMRights___unsigned_long_' = capVMRights, capIsDevice___unsigned_' = capIsDevice, capFBasePtr___unsigned_' = capFBasePtr, capFBasePtr___unsigned_long_' = capFBasePtr___unsigned_long, capCanGrant___unsigned_' = capCanGrant, capCNodePtr___unsigned_' = capCNodePtr, capASIDPool___unsigned_' = capASIDPool, capASIDBase___unsigned_' = capASIDBase, ui_v_entry___unsigned_long_' = ui_v_entry, threadRoot___struct_cap_C_' = threadRoot, targetSlot___ptr_to_struct_pte_C_' = targetSlot, targetSlot___ptr_to_struct_pde_C_' = targetSlot___ptr_to_struct_pde_C, srcNewData___unsigned_long_' = srcNewData, source_cap___struct_cap_C_' = source_cap, sendBuffer___ptr_to_void_' = sendBuffer___ptr_to_void, sendBuffer___ptr_to_unsigned_long_' = sendBuffer, seL4_Fault___struct_seL4_Fault_C_' = seL4_Fault, retypeBase___ptr_to_void_' = retypeBase, regionBase___ptr_to_void_' = regionBase, pivotIndex___unsigned_long_' = pivotIndex, pivotDepth___unsigned_long_' = pivotDepth, parentSlot___ptr_to_struct_cte_C_' = parentSlot, objectSize___unsigned_long_' = objectSize, ntfn_queue___struct_tcb_queue_C_' = ntfn_queue, nodeWindow___unsigned_long_' = nodeWindow, nodeOffset___unsigned_long_' = nodeOffset, n_reserved___unsigned_long_' = n_reserved, isReceiver___unsigned_long_' = isReceiver, isBlocking___unsigned_long_' = isBlocking, ipcbuf_cap___struct_cap_C_' = ipcbuf_cap, ipc_buffer___ptr_to_unsigned_long_' = ipc_buffer, int_eret_3_' = int_eret_3, int_eret_2_' = int_eret_2, handlerCap___struct_cap_C_' = handlerCap, guardFound___unsigned_' = guardFound, fault_type___unsigned_long_' = fault_type, extra_size___unsigned_long_' = extra_size, executable___unsigned_long_' = executable, dtb_addr_p___unsigned_long_' = dtb_addr_p, destOffset___unsigned_long_' = destOffset, destLength___unsigned_long_' = destLength, derivedCap___struct_cap_C_' = derivedCap, cur_thread___ptr_to_struct_tcb_C_' = cur_thread, csselr_old___unsigned_long_' = csselr_old, cap_rights___struct_seL4_CapRights_C_' = cap_rights, capNtfnPtr___unsigned_' = capNtfnPtr, capEPBadge___unsigned_' = capEPBadge, capCanSend___unsigned_' = capCanSend, callerSlot___ptr_to_struct_cte_C_' = callerSlot, bufferSlot___ptr_to_struct_cte_C_' = bufferSlot, bufferAddr___unsigned_long_' = bufferAddr, block_size___unsigned_long_' = block_size, attributes___struct_vm_attributes_C_' = attributes, assoc_bits___int_' = assoc_bits, align_bits___unsigned_' = align_bits, StrictC'_v___unsigned_long_' = StrictC'_v, vm_rights___unsigned_long_' = vm_rights, vbase_ptr___ptr_to_void_' = vbase_ptr, vRootSlot___ptr_to_struct_cte_C_' = vRootSlot, vRootData___unsigned_long_' = vRootData, use_large___unsigned_long_' = use_large, threadPtr___ptr_to_struct_tcb_C_' = threadPtr, stack_top___unsigned_long_' = stack_top, size_bits___unsigned_long_' = size_bits, size_bits___unsigned_' = size_bits___unsigned, ret__long_' = ret__long, replySlot___ptr_to_struct_cte_C_' = replySlot, radixBits___unsigned_long_' = radixBits, pv_offset___long_' = pv_offset, pivotSlot___ptr_to_struct_cte_C_' = pivotSlot, pivotRoot___struct_cap_C_' = pivotRoot, pdCapSlot___ptr_to_struct_cte_C_' = pdCapSlot, page_size___unsigned_long_' = page_size, page_base___unsigned_long_' = page_base, num_nodes___unsigned_long_' = num_nodes, nodeIndex___unsigned_long_' = nodeIndex, nodeDepth___unsigned_long_' = nodeDepth, newVTable___struct_cap_C_' = newVTable, newSrcCap___struct_cap_C_' = newSrcCap, masterCap___struct_cap_C_' = masterCap, levelBits___unsigned_long_' = levelBits, it_pd_cap___struct_cap_C_' = it_pd_cap, it_ap_cap___struct_cap_C_' = it_ap_cap, ipcBuffer___ptr_to_unsigned_long_' = ipcBuffer, immediate___unsigned_long_' = immediate, haveHWFPU___unsigned_long_' = haveHWFPU, guardSize___unsigned_long_' = guardSize, guardBits___unsigned_long_' = guardBits, global_pd___ptr_to_struct_pde_C_' = global_pd, freeIndex___unsigned_long_' = freeIndex, frame_cap___struct_cap_C_' = frame_cap, frameSize___unsigned_long_' = frameSize, faultType___unsigned_long_' = faultType, extraCaps___unsigned_' = extraCaps, dtb_p_reg___struct_p_region_C_' = dtb_p_reg, destCNode___ptr_to_struct_cte_C_' = destCNode, capTCBPtr___unsigned_' = capTCBPtr, capTCBPtr___unsigned_long_' = capTCBPtr___unsigned_long, candidate___ptr_to_struct_tcb_C_' = candidate, callerCap___struct_cap_C_' = callerCap, callerCap___ptr_to_struct_cte_C_' = callerCap___ptr_to_struct_cte_C, cacheable___unsigned_long_' = cacheable, cRootSlot___ptr_to_struct_cte_C_' = cRootSlot, cRootData___unsigned_long_' = cRootData, bufferPtr___ptr_to_unsigned_long_' = bufferPtr, bufferCap___struct_cap_C_' = bufferCap, bitsFound___unsigned_' = bitsFound, base_addr___unsigned_long_' = base_addr, baseValue___unsigned_long_' = baseValue, available___ptr_to_struct_p_region_C_' = available, asid_base___unsigned_long_' = asid_base, allocated___unsigned_long_' = allocated, alignment___unsigned_long_' = alignment, vmRights___unsigned_long_' = vmRights, vRootCap___struct_cap_C_' = vRootCap, userSize___unsigned_long_' = userSize, ui_v_reg___struct_v_region_C_' = ui_v_reg, ui_p_reg___struct_p_region_C_' = ui_p_reg, transfer___struct_cap_transfer_C_' = transfer, tls_base___unsigned_long_' = tls_base, tcb_dest___ptr_to_struct_tcb_C_' = tcb_dest, srcIndex___unsigned_long_' = srcIndex, srcDepth___unsigned_long_' = srcDepth, slot_ptr___ptr_to_struct_cte_C_' = slot_ptr, rootSlot___ptr_to_struct_cte_C_' = rootSlot, ret__int_' = ret__int, reserved___unsigned_' = reserved, reserved___ptr_to_struct_region_C_' = reserved___ptr_to_struct_region_C, receiver___ptr_to_struct_tcb_C_' = receiver, priority___unsigned_long_' = priority, prev_ptr___unsigned_long_' = prev_ptr, prev_cap___struct_cap_C_' = prev_cap, preserve___unsigned_long_' = preserve, prefetch___unsigned_' = prefetch, pagesize___unsigned_long_' = pagesize, pageBits___unsigned_' = pageBits, ntfn_cap___struct_cap_C_' = ntfn_cap, node_ptr___ptr_to_struct_mdb_node_C_' = node_ptr, nodeSize___unsigned_long_' = nodeSize, next_ptr___unsigned_long_' = next_ptr, mdb_node___struct_mdb_node_C_' = mdb_node, it_v_reg___struct_v_region_C_' = it_v_reg, isSource___unsigned_long_' = isSource, irqState___unsigned_long_' = irqState, inverted___unsigned_long_' = inverted, invLabel___unsigned_long_' = invLabel, invLabel___int_' = invLabel___int, find_ret___struct_findPDForASID_ret_C_' = find_ret, fastfail___unsigned_long_' = fastfail, endpoint___ptr_to_struct_endpoint_C_' = endpoint, dtb_size___unsigned_long_' = dtb_size___unsigned_long, dtb_size___unsigned_' = dtb_size, destSlot___ptr_to_struct_cte_C_' = destSlot, data_ram___unsigned_' = data_ram, cnodeCap___struct_cap_C_' = cnodeCap, clzl_ret___unsigned_long_' = clzl_ret, cap_type___unsigned_long_' = cap_type, capIndex___unsigned_long_' = capIndex, capGuard___unsigned_long_' = capGuard, capFSize___unsigned_' = capFSize, capEPPtr___unsigned_' = capEPPtr, canGrant___unsigned_long_' = canGrant, cRootCap___struct_cap_C_' = cRootCap, boundTCB___ptr_to_struct_tcb_C_' = boundTCB, blocking___unsigned_long_' = blocking, bitsLeft___unsigned_' = bitsLeft, asidPool___ptr_to_struct_asid_pool_C_' = asidPool, archInfo___unsigned_long_' = archInfo, v_entry___unsigned_long_' = v_entry, untyped___struct_cap_C_' = untyped, trigger___unsigned_long_' = trigger, tcb_src___ptr_to_struct_tcb_C_' = tcb_src, tag_ram___unsigned_' = tag_ram, syscall___unsigned_long_' = syscall, srcSlot___ptr_to_struct_cte_C_' = srcSlot, srcRoot___struct_cap_C_' = srcRoot, sendBuf___ptr_to_unsigned_long_' = sendBuf, rootCap___struct_cap_C_' = rootCap, restart___unsigned_long_' = restart, res_ret___struct_resolveAddressBits_ret_C_' = res_ret, recvBuf___ptr_to_unsigned_long_' = recvBuf, ptr_src___ptr_to_void_' = ptr_src, ptr_dst___ptr_to_void_' = ptr_dst, pte_ptr___ptr_to_struct_pte_C_' = pte_ptr, pt_vptr___unsigned_long_' = pt_vptr, ptIndex___unsigned_' = ptIndex, poolPtr___ptr_to_struct_asid_pool_C_' = poolPtr, pde_ptr___ptr_to_struct_pde_C_' = pde_ptr, pdIndex___unsigned_' = pdIndex, pdIndex___unsigned_long_' = pdIndex___unsigned_long, ntfnPtr___ptr_to_struct_notification_C_' = ntfnPtr, ntfnCap___struct_cap_C_' = ntfnCap, node_id___unsigned_long_' = node_id, nodeCap___struct_cap_C_' = nodeCap, nextPtr___ptr_to_struct_cte_C_' = nextPtr, new_cap___struct_cap_C_' = new_cap, newType___unsigned_long_' = newType, newPrio___unsigned_long_' = newPrio, newData___unsigned_long_' = newData, msgInfo___unsigned_long_' = msgInfo, msgInfo___struct_seL4_MessageInfo_C_' = msgInfo___struct_seL4_MessageInfo_C, mdbPrev___unsigned_' = mdbPrev, mdbPrev___unsigned_long_' = mdbPrev___unsigned_long, mdbNode___struct_mdb_node_C_' = mdbNode, mdbNext___unsigned_' = mdbNext, mdbNext___unsigned_long_' = mdbNext___unsigned_long, map_ret___struct_create_mappings_pte_return_C_' = map_ret, map_ret___struct_create_mappings_pde_return_C_' = map_ret___struct_create_mappings_pde_return_C, lus_ret___struct_lookupSlot_ret_C_' = lus_ret, lufType___unsigned_long_' = lufType, luc_ret___struct_lookupCap_ret_C_' = luc_ret, l2index___unsigned_long_' = l2index, l1index___unsigned_long_' = l1index, irqSlot___ptr_to_struct_cte_C_' = irqSlot, initial___ptr_to_struct_tcb_C_' = initial, hw_asid___unsigned_char_' = hw_asid, freeRef___unsigned_long_' = freeRef, faultep___unsigned_long_' = faultep, faultEP___unsigned_long_' = faultEP, exposed___unsigned_long_' = exposed, endSlot___ptr_to_struct_cte_C_' = endSlot, do_call___unsigned_long_' = do_call, disable___unsigned_long_' = disable, destCap___struct_cap_C_' = destCap, cte_ptr___ptr_to_struct_cte_C_' = cte_ptr, context___ptr_to_struct_user_context_C_' = context, cap_ptr___ptr_to_struct_cap_C_' = cap_ptr, capData___unsigned_long_' = capData, basePtr___unsigned_long_' = basePtr, authTCB___ptr_to_struct_tcb_C_' = authTCB, authCap___struct_cap_C_' = authCap, address___unsigned_' = address, z_slot___ptr_to_struct_cte_C_' = z_slot, w_bits___unsigned_long_' = w_bits, ut_cap___struct_cap_C_' = ut_cap, ui_reg___struct_region_C_' = ui_reg, ts_ptr___ptr_to_struct_thread_state_C_' = ts_ptr, tsType___unsigned_long_' = tsType, thread___ptr_to_struct_tcb_C_' = thread, tcbptr___ptr_to_struct_tcb_C_' = tcbptr, target___unsigned_' = target___unsigned, target___unsigned_char_' = target___unsigned_char, target___ptr_to_struct_tcb_C_' = target, status___unsigned_long_' = status, srcTCB___ptr_to_struct_tcb_C_' = srcTCB, srcMDB___struct_mdb_node_C_' = srcMDB, srcCap___struct_cap_C_' = srcCap, sender___ptr_to_struct_tcb_C_' = sender, result___unsigned_long_' = result, pt_cap___struct_cap_C_' = pt_cap, ptSlot___ptr_to_struct_pte_C_' = ptSlot, pstart___unsigned_long_' = pstart, pd_val___unsigned_long_' = pd_val, pd_cap___struct_cap_C_' = pd_cap, pdSlot___ptr_to_struct_pde_C_' = pdSlot, parity___unsigned_long_' = parity, parent___ptr_to_struct_cte_C_' = parent, offset___unsigned_' = offset, offset___unsigned_long_' = offset___unsigned_long, offset___int_' = offset___int, number___unsigned_' = number, number___unsigned_long_' = number___unsigned_long, newMcp___unsigned_long_' = newMcp, newMDB___struct_mdb_node_C_' = newMDB, newCap___struct_cap_C_' = newCap, n_bits___unsigned_long_' = n_bits, maxlen___unsigned_long_' = maxlen, lu_ret___struct_lookupCapAndSlot_ret_C_' = lu_ret, lu_ret___struct_lookupCap_ret_C_' = lu_ret___struct_lookupCap_ret_C, lu_ret___struct_lookupPTSlot_ret_C_' = lu_ret___struct_lookupPTSlot_ret_C, lu_ret___struct_lookupSlot_ret_C_' = lu_ret___struct_lookupSlot_ret_C, lu_ret___struct_lookupSlot_raw_ret_C_' = lu_ret___struct_lookupSlot_raw_ret_C, length___unsigned_' = length, length___unsigned_long_' = length___unsigned_long, isMove___unsigned_long_' = isMove, isCall___unsigned_long_' = isCall, htpidr___unsigned_long_' = htpidr, header___struct_seL4_BootInfoHeader_C_' = header, fs_ret___struct_finaliseSlot_ret_C_' = fs_ret, fc_ret___struct_finaliseCap_ret_C_' = fc_ret, ep_ref___unsigned_long_' = ep_ref, ep_ptr___ptr_to_struct_endpoint_C_' = ep_ptr, ep_cap___struct_cap_C_' = ep_cap, epCPtr___unsigned_long_' = epCPtr, domain___unsigned_long_' = domain, do_map___unsigned_long_' = do_map, dc_ret___struct_deriveCap_ret_C_' = dc_ret, ctSlot___ptr_to_struct_cte_C_' = ctSlot, capptr___unsigned_long_' = capptr, cap_pd___ptr_to_struct_pde_C_' = cap_pd, capPtr___unsigned_' = capPtr, capIRQ___unsigned_' = capIRQ, caller___ptr_to_struct_tcb_C_' = caller, buffer___ptr_to_unsigned_long_' = buffer, badge2___unsigned_long_' = badge2, ap_cap___struct_cap_C_' = ap_cap, Domain___unsigned_' = Domain, vaddr___unsigned_long_' = vaddr, v_reg___struct_v_region_C_' = v_reg, state___unsigned_long_' = state, state___ptr_to_struct_thread_state_C_' = state___ptr_to_struct_thread_state_C, start___unsigned_long_' = start, slot3___ptr_to_struct_cte_C_' = slot3, slot2___ptr_to_struct_cte_C_' = slot2, slot1___ptr_to_struct_cte_C_' = slot1, size2___unsigned_long_' = size2, reset___unsigned_long_' = reset, radix___unsigned_long_' = radix, queue___struct_tcb_queue_C_' = queue, pdCap___struct_cap_C_' = pdCap, paddr___unsigned_long_' = paddr, p_reg___struct_p_region_C_' = p_reg, nsets___int_' = nsets, nirqs___int_' = nirqs, newPD___ptr_to_struct_pde_C_' = newPD, level___int_' = level, lbits___int_' = lbits, label___unsigned_' = label, label___unsigned_long_' = label___unsigned_long, irq_w___unsigned_long_' = irq_w, index___unsigned_long_' = index, index___int_' = index___int, guard___unsigned_long_' = guard, grant___unsigned_long_' = grant, frame___ptr_to_void_' = frame, frame___ptr_to_struct_kernel_frame_C_' = frame___ptr_to_struct_kernel_frame_C, fpsid___unsigned_long_' = fpsid, fpexc___unsigned_long_' = fpexc, flags___unsigned_long_' = flags, final___unsigned_long_' = final, fault___struct_seL4_Fault_C_' = fault, fault___unsigned_long_' = fault___unsigned_long, epptr___ptr_to_struct_endpoint_C_' = epptr, depth___unsigned_long_' = depth, cte_b___ptr_to_struct_cte_C_' = cte_b, cte_a___ptr_to_struct_cte_C_' = cte_a, cptr2___unsigned_long_' = cptr2, cpacr___unsigned_long_' = cpacr, count___unsigned_' = count, cnode___struct_cap_C_' = cnode, chunk___int_' = chunk, cap_b___struct_cap_C_' = cap_b, cap_a___struct_cap_C_' = cap_a, block___unsigned_long_' = block, badge___unsigned_long_' = badge, bBase___unsigned_long_' = bBase, assoc___int_' = assoc, aifsr___unsigned_long_' = aifsr, adfsr___unsigned_long_' = adfsr, actlr___unsigned_long_' = actlr, aBase___unsigned_long_' = aBase, AIFSR___unsigned_long_' = AIFSR, ADFSR___unsigned_long_' = ADFSR, ACTLR___unsigned_long_' = ACTLR, wptr___ptr_to_unsigned_long_' = wptr, word___int_' = word, vtop___unsigned_long_' = vtop, vptr___unsigned_long_' = vptr, type___unsigned_long_' = type, tptr___ptr_to_struct_tcb_C_' = tptr, topB___unsigned_long_' = topB, topA___unsigned_long_' = topA, tcap___struct_cap_C_' = tcap, tCap___struct_cap_C_' = tCap, slot___ptr_to_struct_cte_C_' = slot, size___unsigned_' = size, size___unsigned_long_' = size___unsigned_long, sent___unsigned_long_' = sent, root___struct_cap_C_' = root, ptr2___ptr_to_struct_cte_C_' = ptr2, prrr___unsigned_long_' = prrr, prio___unsigned_long_' = prio, prev___ptr_to_struct_cte_C_' = prev, pptr___ptr_to_void_' = pptr, pptr___unsigned_long_' = pptr___unsigned_long, pool___ptr_to_struct_asid_pool_C_' = pool, phys___unsigned_long_' = phys, ntfn___ptr_to_struct_notification_C_' = ntfn, nmrr___unsigned_long_' = nmrr, next___ptr_to_struct_cte_C_' = next, next___ptr_to_struct_tcb_C_' = next___ptr_to_struct_tcb_C, mdb2___struct_mdb_node_C_' = mdb2, mdb1___struct_mdb_node_C_' = mdb1, mask___unsigned_long_' = mask, mask___unsigned_' = mask___unsigned, mask___unsigned_longlong_' = mask___unsigned_longlong, line___unsigned_long_' = line, info___struct_seL4_MessageInfo_C_' = info, ifsr___unsigned_long_' = ifsr, ifar___unsigned_long_' = ifar, idx2___unsigned_long_' = idx2, diff___int_' = diff, dfsr___unsigned_long_' = dfsr, dfar___unsigned_long_' = dfar, dest___ptr_to_struct_tcb_C_' = dest, dest___ptr_to_char_' = dest___ptr_to_char, data___unsigned_long_' = data, ctag___enum_cap_tag_' = ctag, cptr___unsigned_long_' = cptr, code___unsigned_' = code, clid___int_' = clid, cidr___unsigned_long_' = cidr, cap2___struct_cap_C_' = cap2, cap1___struct_cap_C_' = cap1, call___unsigned_long_' = call, cPtr___unsigned_long_' = cPtr, botB___unsigned_long_' = botB, botA___unsigned_long_' = botA, bits___unsigned_long_' = bits, bits___unsigned_' = bits___unsigned, base___unsigned_long_' = base, base___unsigned_' = base___unsigned, bTop___unsigned_long_' = bTop, auth___ptr_to_struct_tcb_C_' = auth, attr___struct_vm_attributes_C_' = attr, asid___unsigned_long_' = asid, arch___unsigned_long_' = arch, addr___unsigned_long_' = addr, addr___unsigned_' = addr___unsigned, aTop___unsigned_long_' = aTop, PRRR___unsigned_long_' = PRRR, NMRR___unsigned_long_' = NMRR, IFSR___unsigned_long_' = IFSR, IFAR___unsigned_long_' = IFAR, DFSR___unsigned_long_' = DFSR, DFAR___unsigned_long_' = DFAR, CLID___unsigned_long_' = CLID, CIDR___unsigned_long_' = CIDR, wsl___unsigned_long_' = wsl, w_b___unsigned_long_' = w_b, w_a___unsigned_long_' = w_a, val___unsigned_long_' = val, val___long_' = val___long, v32___unsigned_' = v32, tex___unsigned_long_' = tex, tcb___ptr_to_struct_tcb_C_' = tcb, tag___struct_seL4_MessageInfo_C_' = tag, str___ptr_to_char_' = str, src___ptr_to_struct_tcb_C_' = src, src___ptr_to_char_' = src___ptr_to_char, scr___unsigned_long_' = scr, ret___unsigned_' = ret, ret___unsigned_long_' = ret___unsigned_long, ret___struct_findPDForASID_ret_C_' = ret___struct_findPDForASID_ret_C, ret___struct_lookupPTSlot_ret_C_' = ret___struct_lookupPTSlot_ret_C, ret___struct_resolve_ret_C_' = ret___struct_resolve_ret_C, ret___struct_create_mappings_pte_return_C_' = ret___struct_create_mappings_pte_return_C, ret___struct_create_mappings_pde_return_C_' = ret___struct_create_mappings_pde_return_C, ret___struct_deriveCap_ret_C_' = ret___struct_deriveCap_ret_C, ret___struct_lookupCap_ret_C_' = ret___struct_lookupCap_ret_C, ret___struct_lookupCapAndSlot_ret_C_' = ret___struct_lookupCapAndSlot_ret_C, ret___struct_lookupSlot_raw_ret_C_' = ret___struct_lookupSlot_raw_ret_C, ret___struct_lookupSlot_ret_C_' = ret___struct_lookupSlot_ret_C, ret___struct_resolveAddressBits_ret_C_' = ret___struct_resolveAddressBits_ret_C, ret___struct_finaliseSlot_ret_C_' = ret___struct_finaliseSlot_ret_C, res___long_' = res, reg___unsigned_long_' = reg, reg___struct_region_C_' = reg___struct_region_C, reg___struct_p_region_C_' = reg___struct_p_region_C, ptr___unsigned_long_' = ptr, ptr___ptr_to_unsigned_long_' = ptr___ptr_to_unsigned_long, ptr___ptr_to_struct_cte_C_' = ptr___ptr_to_struct_cte_C, pte___struct_pte_C_' = pte, pte___ptr_to_struct_pte_C_' = pte___ptr_to_struct_pte_C, pde___struct_pde_C_' = pde, pde___ptr_to_struct_pde_C_' = pde___ptr_to_struct_pde_C, msb___unsigned_long_' = msb, mdb___struct_mdb_node_C_' = mdb, mcp___unsigned_long_' = mcp, max___unsigned_long_' = max, luf___struct_lookup_fault_C_' = luf, lou___int_' = lou, loc___int_' = loc, len___unsigned_long_' = len, irq___unsigned_long_' = irq, idx___unsigned_long_' = idx, ex1___struct_seL4_Fault_C_' = ex1, end___unsigned_long_' = end, dom___unsigned_long_' = dom, cte___ptr_to_struct_cte_C_' = cte, cpu___unsigned_long_' = cpu, cap___struct_cap_C_' = cap, bit___int_' = bit, aux___unsigned_' = aux, acr___unsigned_long_' = acr, TEX___unsigned_' = TEX, FSR___unsigned_' = FSR, FAR___unsigned_long_' = FAR, APX___unsigned_' = APX, ts___unsigned_long_' = ts, sz___unsigned_long_' = sz, s2___ptr_to_char_' = s2, s1___ptr_to_char_' = s1, pt___ptr_to_struct_pte_C_' = pt, pd___ptr_to_struct_pde_C_' = pd, pd___struct_cap_C_' = pd___struct_cap_C, pd___struct_findPDForASID_ret_C_' = pd___struct_findPDForASID_ret_C, pc___unsigned_long_' = pc, pa___unsigned_long_' = pa, nG___unsigned_' = nG, mi___struct_seL4_MessageInfo_C_' = mi, id___unsigned_long_' = id, id___anonymous_enum_' = id___anonymous_enum, ep___ptr_to_struct_endpoint_C_' = ep, ct___struct_cap_transfer_C_' = ct, bi___ptr_to_struct_seL4_BootInfo_C_' = bi, ap___ptr_to_struct_asid_pool_C_' = ap, ap___unsigned_long_' = ap___unsigned_long, XN___unsigned_' = XN, AP___unsigned_' = AP, y___unsigned_' = y, y___int_' = y___int, x___unsigned_' = x, x___unsigned_longlong_' = x___unsigned_longlong, x___unsigned_long_' = x___unsigned_long, x___int_' = x___int, w___unsigned_long_' = w, w___int_' = w___int, w___struct_seL4_CNode_CapData_C_' = w___struct_seL4_CNode_CapData_C, v___unsigned_long_' = va, v___int_' = v___int, v___unsigned_' = v___unsigned, t___unsigned_long_' = t, s___unsigned_long_' = s___unsigned_long, s___ptr_to_char_' = s___ptr_to_char, s___ptr_to_void_' = s, r___unsigned_long_' = r, r___ptr_to_struct_p_region_C_' = r___ptr_to_struct_p_region_C, r___ptr_to_struct_region_C_' = r___ptr_to_struct_region_C, q___ptr_to_unsigned_char_' = q, p___unsigned_long_' = p, p___ptr_to_unsigned_char_' = p___ptr_to_unsigned_char, n___unsigned_long_' = n, n___int_' = n___int, m___struct_region_C_' = m, l___int_' = l, j___unsigned_long_' = j, i___unsigned_long_' = i, i___unsigned_' = i___unsigned, i___int_' = i___int, f___unsigned_long_' = f, e___unsigned_long_' = e, c___unsigned_long_' = c, c___char_' = c___char, b___unsigned_long_' = b, a___unsigned_long_' = a, S___unsigned_' = S, P___unsigned_' = P, C___unsigned_' = C, B___unsigned_' = B, \<dots> = morea\<rparr> \<in> G' \<Longrightarrow> \<forall>uu. dc uu (xf' (xfu' (\<lambda>_. v) \<lparr>globals = \<lparr>t_hrs_' = t_hrs, phantom_machine_state_' = phantom_machine_state, ghost'state_' = ghost'state, avail_reg_' = avail_reg, ksNumCPUs_' = ksNumCPUs, ndks_boot_' = ndks_boot, active_irq_' = active_irq, rootserver_' = rootserver, ksCurDomain_' = ksCurDomain, ksCurThread_' = ksCurThread, ksDomainTime_' = ksDomainTime, ksIdleThread_' = ksIdleThread, tlbLockCount_' = tlbLockCount, armKSNextASID_' = armKSNextASID, current_fault_' = current_fault, ksReadyQueues_' = ksReadyQueues, armKSASIDTable_' = armKSASIDTable, rootserver_mem_' = rootserver_mem, armKSHWASIDTable_' = armKSHWASIDTable, intStateIRQTable_' = intStateIRQTable, ksDomScheduleIdx_' = ksDomScheduleIdx, ksSchedulerAction_' = ksSchedulerAction, current_extra_caps_' = current_extra_caps, isFPUEnabledCached_' = isFPUEnabledCached, current_lookup_fault_' = current_lookup_fault, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted, current_syscall_error_' = current_syscall_error, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap, \<dots> = more\<rparr>, global_exn_var_' = global_exn_var, ret__struct_create_frames_of_region_ret_C_' = ret__struct_create_frames_of_region_ret_C, ret__struct_create_mappings_pte_return_C_' = ret__struct_create_mappings_pte_return_C, ret__struct_create_mappings_pde_return_C_' = ret__struct_create_mappings_pde_return_C, ret__struct_resolveAddressBits_ret_C_' = ret__struct_resolveAddressBits_ret_C, ret__struct_lookupCapAndSlot_ret_C_' = ret__struct_lookupCapAndSlot_ret_C, ret__struct_lookupSlot_raw_ret_C_' = ret__struct_lookupSlot_raw_ret_C, ret__struct_findPDForASID_ret_C_' = ret__struct_findPDForASID_ret_C, ret__struct_seL4_MessageInfo_C_' = ret__struct_seL4_MessageInfo_C, ret__struct_lookupPTSlot_ret_C_' = ret__struct_lookupPTSlot_ret_C, ret__struct_finaliseSlot_ret_C_' = ret__struct_finaliseSlot_ret_C, ret__struct_seL4_SlotRegion_C_' = ret__struct_seL4_SlotRegion_C, ret__struct_finaliseCap_ret_C_' = ret__struct_finaliseCap_ret_C, ret__struct_seL4_CapRights_C_' = ret__struct_seL4_CapRights_C, ret__struct_lookupSlot_ret_C_' = ret__struct_lookupSlot_ret_C, ret__struct_vm_attributes_C_' = ret__struct_vm_attributes_C, ret__struct_lookupCap_ret_C_' = ret__struct_lookupCap_ret_C, ret__struct_deriveCap_ret_C_' = ret__struct_deriveCap_ret_C, ret__struct_lookup_fault_C_' = ret__struct_lookup_fault_C, ret__struct_cap_transfer_C_' = ret__struct_cap_transfer_C, ret__struct_resolve_ret_C_' = ret__struct_resolve_ret_C, ret__ptr_to_unsigned_long_' = ret__ptr_to_unsigned_long, ret__struct_seL4_Fault_C_' = ret__struct_seL4_Fault_C, ret__ptr_to_struct_tcb_C_' = ret__ptr_to_struct_tcb_C, ret__ptr_to_struct_pte_C_' = ret__ptr_to_struct_pte_C, ret__ptr_to_struct_pde_C_' = ret__ptr_to_struct_pde_C, ret__ptr_to_struct_cte_C_' = ret__ptr_to_struct_cte_C, ret__struct_tcb_queue_C_' = ret__struct_tcb_queue_C, ret__struct_p_region_C_' = ret__struct_p_region_C, ret__struct_mdb_node_C_' = ret__struct_mdb_node_C, original_lookup_fault___struct_lookup_fault_C_' = original_lookup_fault, unsigned_long_eret_4_' = unsigned_long_eret_4, unsigned_long_eret_3_' = unsigned_long_eret_3, unsigned_long_eret_2_' = unsigned_long_eret_2, ret__struct_region_C_' = ret__struct_region_C, struct_cap_C_eret_3_' = struct_cap_C_eret_3, struct_cap_C_eret_2_' = struct_cap_C_eret_2, extra_bi_frame_vptr___unsigned_long_' = extra_bi_frame_vptr, seL4_CNode_CapData___struct_seL4_CNode_CapData_C_' = seL4_CNode_CapData, ret__unsigned_long_' = ret__unsigned_long, ret__unsigned_char_' = ret__unsigned_char, ptr_to_void_eret_2_' = ptr_to_void_eret_2, first_untyped_slot___unsigned_long_' = first_untyped_slot, extra_bi_size_bits___unsigned_long_' = extra_bi_size_bits, capPTMappedAddress___unsigned_' = capPTMappedAddress, capFMappedASIDHigh___unsigned_' = capFMappedASIDHigh, boot_mem_reuse_reg___struct_region_C_' = boot_mem_reuse_reg, tlbflush_required___unsigned_long_' = tlbflush_required, stored_asid_valid___unsigned_' = stored_asid_valid, ret__struct_pte_C_' = ret__struct_pte_C, ret__struct_pde_C_' = ret__struct_pde_C, ret__struct_cap_C_' = ret__struct_cap_C, receiverIPCBuffer___ptr_to_unsigned_long_' = receiverIPCBuffer, newCapIsRevocable___unsigned_long_' = newCapIsRevocable, create_frames_ret___struct_create_frames_of_region_ret_C_' = create_frames_ret, capNtfnCanReceive___unsigned_' = capNtfnCanReceive, capFMappedAddress___unsigned_' = capFMappedAddress, capFMappedASIDLow___unsigned_' = capFMappedASIDLow, capCNodeGuardSize___unsigned_' = capCNodeGuardSize, untypedFreeBytes___unsigned_long_' = untypedFreeBytes, thread_state_ptr___ptr_to_struct_thread_state_C_' = thread_state_ptr, size_unique_name___unsigned_long_' = size_unique_name, seL4_MessageInfo___struct_seL4_MessageInfo_C_' = seL4_MessageInfo, scheduler_action___ptr_to_struct_tcb_C_' = scheduler_action, ret__ptr_to_void_' = ret__ptr_to_void, receiveIPCBuffer___ptr_to_unsigned_long_' = receiveIPCBuffer, prevIsSameObject___unsigned_long_' = prevIsSameObject, notification_ptr___ptr_to_struct_notification_C_' = notification_ptr, l1index_inverted___unsigned_long_' = l1index_inverted, instructionFault___unsigned_' = instructionFault, capReplyCanGrant___unsigned_' = capReplyCanGrant, capReplyCanGrant___unsigned_long_' = capReplyCanGrant___unsigned_long, capCanGrantReply___unsigned_' = capCanGrantReply, armParityEnabled___unsigned_' = armParityEnabled, armPageCacheable___unsigned_' = armPageCacheable, unsigned_eret_6_' = unsigned_eret_6, unsigned_eret_5_' = unsigned_eret_5, unsigned_eret_4_' = unsigned_eret_4, unsigned_eret_3_' = unsigned_eret_3, unsigned_eret_2_' = unsigned_eret_2, unaligned_start___unsigned_long_' = unaligned_start, transferInteger___unsigned_long_' = transferInteger, totalObjectSize___unsigned_long_' = totalObjectSize, slot_pos_before___unsigned_long_' = slot_pos_before, extra_bi_region___struct_region_C_' = extra_bi_region, extra_bi_offset___unsigned_long_' = extra_bi_offset, cnode_size_bits___unsigned_long_' = cnode_size_bits, cap_rights_mask___struct_seL4_CapRights_C_' = cap_rights_mask, capPTMappedASID___unsigned_' = capPTMappedASID, capPDMappedASID___unsigned_' = capPDMappedASID, armExecuteNever___unsigned_' = armExecuteNever, ui_p_reg_start___unsigned_long_' = ui_p_reg_start, stored_hw_asid___unsigned_' = stored_hw_asid, stored_hw_asid___struct_pde_C_' = stored_hw_asid___struct_pde_C, slot_pos_after___unsigned_long_' = slot_pos_after, seL4_CapRights___struct_seL4_CapRights_C_' = seL4_CapRights, root_cnode_cap___struct_cap_C_' = root_cnode_cap, msgTransferred___unsigned_long_' = msgTransferred, mdbFirstBadged___unsigned_' = mdbFirstBadged, mdbFirstBadged___unsigned_long_' = mdbFirstBadged___unsigned_long, inReceivePhase___unsigned_' = inReceivePhase, hw_asid_offset___unsigned_long_' = hw_asid_offset, currentPDEType___enum_pde_tag_' = currentPDEType, cptr_bufferPtr___unsigned_long_' = cptr_bufferPtr, capReplyMaster___unsigned_' = capReplyMaster, capReplyMaster___unsigned_long_' = capReplyMaster___unsigned_long, capNtfnCanSend___unsigned_' = capNtfnCanSend, alignedFreeRef___unsigned_long_' = alignedFreeRef, vm_attributes___struct_vm_attributes_C_' = vm_attributes, vRoot_srcSlot___ptr_to_struct_cte_C_' = vRoot_srcSlot, transferFrame___unsigned_long_' = transferFrame, syscallNumber___unsigned_' = syscallNumber, suspendSource___unsigned_long_' = suspendSource, stack_address___unsigned_long_' = stack_address, root_switched___unsigned_long_' = root_switched, ret__unsigned_' = ret__unsigned, ret__longlong_' = ret__longlong, replyCanGrant___unsigned_long_' = replyCanGrant, receiveBuffer___ptr_to_void_' = receiveBuffer___ptr_to_void, receiveBuffer___ptr_to_unsigned_long_' = receiveBuffer, nonexecutable___unsigned_long_' = nonexecutable, mva_plus_asid___unsigned_long_' = mva_plus_asid, fpsid_subarch___unsigned_long_' = fpsid_subarch, extra_bi_size___unsigned_long_' = extra_bi_size, dtb_phys_addr___unsigned_long_' = dtb_phys_addr, device_memory___unsigned_long_' = device_memory, cmp_size_bits___unsigned_long_' = cmp_size_bits, capsUnwrapped___unsigned_' = capsUnwrapped, capZombieType___unsigned_' = capZombieType, capPTIsMapped___unsigned_' = capPTIsMapped, capPDIsMapped___unsigned_' = capPDIsMapped, capCanReceive___unsigned_' = capCanReceive, capCNodeRadix___unsigned_' = capCNodeRadix, capCNodeGuard___unsigned_' = capCNodeGuard, canGrantReply___unsigned_long_' = canGrantReply, cRoot_srcSlot___ptr_to_struct_cte_C_' = cRoot_srcSlot, bufferSrcSlot___ptr_to_struct_cte_C_' = bufferSrcSlot, bi_frame_vptr___unsigned_long_' = bi_frame_vptr, was_runnable___unsigned_long_' = was_runnable, w_rightsMask___unsigned_long_' = w_rightsMask, vm_faultType___unsigned_long_' = vm_faultType, vRoot_newCap___struct_cap_C_' = vRoot_newCap, ui_p_reg_end___unsigned_long_' = ui_p_reg_end, transferArch___unsigned_long_' = transferArch, thread_state___struct_thread_state_C_' = thread_state, resumeTarget___unsigned_long_' = resumeTarget, processor_id___unsigned_long_' = processor_id, pivotNewData___unsigned_long_' = pivotNewData, nextFreeArea___ptr_to_void_' = nextFreeArea, mdb_node_ptr___ptr_to_struct_mdb_node_C_' = mdb_node_ptr, mdbRevocable___unsigned_' = mdbRevocable, mdbRevocable___unsigned_long_' = mdbRevocable___unsigned_long, lookup_fault___struct_lookup_fault_C_' = lookup_fault, extra_bi_ret___struct_create_frames_of_region_ret_C_' = extra_bi_ret, epQueue_tail___unsigned_long_' = epQueue_tail, epQueue_head___unsigned_long_' = epQueue_head, endpoint_ptr___ptr_to_struct_endpoint_C_' = endpoint_ptr, endpointTail___ptr_to_struct_tcb_C_' = endpointTail, dtb_phys_end___unsigned_long_' = dtb_phys_end, deviceMemory___unsigned_long_' = deviceMemory, cap_type_tag___unsigned_' = cap_type_tag, capPTBasePtr___unsigned_' = capPTBasePtr, capPDBasePtr___unsigned_' = capPDBasePtr, capNtfnBadge___unsigned_' = capNtfnBadge, capFreeIndex___unsigned_' = capFreeIndex, capFVMRights___unsigned_' = capFVMRights, capFIsDevice___unsigned_' = capFIsDevice, capBlockSize___unsigned_' = capBlockSize, cRoot_newCap___struct_cap_C_' = cRoot_newCap, w_bufferPtr___unsigned_long_' = w_bufferPtr, userObjSize___unsigned_long_' = userObjSize, updateFlags___unsigned_long_' = updateFlags, resolve_ret___struct_resolve_ret_C_' = resolve_ret, pte_entries___struct_pte_range_C_' = pte_entries, pde_entries___struct_pde_range_C_' = pde_entries, new_hw_asid___unsigned_char_' = new_hw_asid, newPivotCap___struct_cap_C_' = newPivotCap, n_available___unsigned_long_' = n_available, ipcbuf_vptr___unsigned_long_' = ipcbuf_vptr, instruction___unsigned_long_' = instruction, handlerSlot___ptr_to_struct_cte_C_' = handlerSlot, handlerCPtr___unsigned_long_' = handlerCPtr, empty_index___int_' = empty_index, controlSlot___ptr_to_struct_cte_C_' = controlSlot, cleanupInfo___struct_cap_C_' = cleanupInfo, capZombieID___unsigned_' = capZombieID, capVMRights___unsigned_long_' = capVMRights, capIsDevice___unsigned_' = capIsDevice, capFBasePtr___unsigned_' = capFBasePtr, capFBasePtr___unsigned_long_' = capFBasePtr___unsigned_long, capCanGrant___unsigned_' = capCanGrant, capCNodePtr___unsigned_' = capCNodePtr, capASIDPool___unsigned_' = capASIDPool, capASIDBase___unsigned_' = capASIDBase, ui_v_entry___unsigned_long_' = ui_v_entry, threadRoot___struct_cap_C_' = threadRoot, targetSlot___ptr_to_struct_pte_C_' = targetSlot, targetSlot___ptr_to_struct_pde_C_' = targetSlot___ptr_to_struct_pde_C, srcNewData___unsigned_long_' = srcNewData, source_cap___struct_cap_C_' = source_cap, sendBuffer___ptr_to_void_' = sendBuffer___ptr_to_void, sendBuffer___ptr_to_unsigned_long_' = sendBuffer, seL4_Fault___struct_seL4_Fault_C_' = seL4_Fault, retypeBase___ptr_to_void_' = retypeBase, regionBase___ptr_to_void_' = regionBase, pivotIndex___unsigned_long_' = pivotIndex, pivotDepth___unsigned_long_' = pivotDepth, parentSlot___ptr_to_struct_cte_C_' = parentSlot, objectSize___unsigned_long_' = objectSize, ntfn_queue___struct_tcb_queue_C_' = ntfn_queue, nodeWindow___unsigned_long_' = nodeWindow, nodeOffset___unsigned_long_' = nodeOffset, n_reserved___unsigned_long_' = n_reserved, isReceiver___unsigned_long_' = isReceiver, isBlocking___unsigned_long_' = isBlocking, ipcbuf_cap___struct_cap_C_' = ipcbuf_cap, ipc_buffer___ptr_to_unsigned_long_' = ipc_buffer, int_eret_3_' = int_eret_3, int_eret_2_' = int_eret_2, handlerCap___struct_cap_C_' = handlerCap, guardFound___unsigned_' = guardFound, fault_type___unsigned_long_' = fault_type, extra_size___unsigned_long_' = extra_size, executable___unsigned_long_' = executable, dtb_addr_p___unsigned_long_' = dtb_addr_p, destOffset___unsigned_long_' = destOffset, destLength___unsigned_long_' = destLength, derivedCap___struct_cap_C_' = derivedCap, cur_thread___ptr_to_struct_tcb_C_' = cur_thread, csselr_old___unsigned_long_' = csselr_old, cap_rights___struct_seL4_CapRights_C_' = cap_rights, capNtfnPtr___unsigned_' = capNtfnPtr, capEPBadge___unsigned_' = capEPBadge, capCanSend___unsigned_' = capCanSend, callerSlot___ptr_to_struct_cte_C_' = callerSlot, bufferSlot___ptr_to_struct_cte_C_' = bufferSlot, bufferAddr___unsigned_long_' = bufferAddr, block_size___unsigned_long_' = block_size, attributes___struct_vm_attributes_C_' = attributes, assoc_bits___int_' = assoc_bits, align_bits___unsigned_' = align_bits, StrictC'_v___unsigned_long_' = StrictC'_v, vm_rights___unsigned_long_' = vm_rights, vbase_ptr___ptr_to_void_' = vbase_ptr, vRootSlot___ptr_to_struct_cte_C_' = vRootSlot, vRootData___unsigned_long_' = vRootData, use_large___unsigned_long_' = use_large, threadPtr___ptr_to_struct_tcb_C_' = threadPtr, stack_top___unsigned_long_' = stack_top, size_bits___unsigned_long_' = size_bits, size_bits___unsigned_' = size_bits___unsigned, ret__long_' = ret__long, replySlot___ptr_to_struct_cte_C_' = replySlot, radixBits___unsigned_long_' = radixBits, pv_offset___long_' = pv_offset, pivotSlot___ptr_to_struct_cte_C_' = pivotSlot, pivotRoot___struct_cap_C_' = pivotRoot, pdCapSlot___ptr_to_struct_cte_C_' = pdCapSlot, page_size___unsigned_long_' = page_size, page_base___unsigned_long_' = page_base, num_nodes___unsigned_long_' = num_nodes, nodeIndex___unsigned_long_' = nodeIndex, nodeDepth___unsigned_long_' = nodeDepth, newVTable___struct_cap_C_' = newVTable, newSrcCap___struct_cap_C_' = newSrcCap, masterCap___struct_cap_C_' = masterCap, levelBits___unsigned_long_' = levelBits, it_pd_cap___struct_cap_C_' = it_pd_cap, it_ap_cap___struct_cap_C_' = it_ap_cap, ipcBuffer___ptr_to_unsigned_long_' = ipcBuffer, immediate___unsigned_long_' = immediate, haveHWFPU___unsigned_long_' = haveHWFPU, guardSize___unsigned_long_' = guardSize, guardBits___unsigned_long_' = guardBits, global_pd___ptr_to_struct_pde_C_' = global_pd, freeIndex___unsigned_long_' = freeIndex, frame_cap___struct_cap_C_' = frame_cap, frameSize___unsigned_long_' = frameSize, faultType___unsigned_long_' = faultType, extraCaps___unsigned_' = extraCaps, dtb_p_reg___struct_p_region_C_' = dtb_p_reg, destCNode___ptr_to_struct_cte_C_' = destCNode, capTCBPtr___unsigned_' = capTCBPtr, capTCBPtr___unsigned_long_' = capTCBPtr___unsigned_long, candidate___ptr_to_struct_tcb_C_' = candidate, callerCap___struct_cap_C_' = callerCap, callerCap___ptr_to_struct_cte_C_' = callerCap___ptr_to_struct_cte_C, cacheable___unsigned_long_' = cacheable, cRootSlot___ptr_to_struct_cte_C_' = cRootSlot, cRootData___unsigned_long_' = cRootData, bufferPtr___ptr_to_unsigned_long_' = bufferPtr, bufferCap___struct_cap_C_' = bufferCap, bitsFound___unsigned_' = bitsFound, base_addr___unsigned_long_' = base_addr, baseValue___unsigned_long_' = baseValue, available___ptr_to_struct_p_region_C_' = available, asid_base___unsigned_long_' = asid_base, allocated___unsigned_long_' = allocated, alignment___unsigned_long_' = alignment, vmRights___unsigned_long_' = vmRights, vRootCap___struct_cap_C_' = vRootCap, userSize___unsigned_long_' = userSize, ui_v_reg___struct_v_region_C_' = ui_v_reg, ui_p_reg___struct_p_region_C_' = ui_p_reg, transfer___struct_cap_transfer_C_' = transfer, tls_base___unsigned_long_' = tls_base, tcb_dest___ptr_to_struct_tcb_C_' = tcb_dest, srcIndex___unsigned_long_' = srcIndex, srcDepth___unsigned_long_' = srcDepth, slot_ptr___ptr_to_struct_cte_C_' = slot_ptr, rootSlot___ptr_to_struct_cte_C_' = rootSlot, ret__int_' = ret__int, reserved___unsigned_' = reserved, reserved___ptr_to_struct_region_C_' = reserved___ptr_to_struct_region_C, receiver___ptr_to_struct_tcb_C_' = receiver, priority___unsigned_long_' = priority, prev_ptr___unsigned_long_' = prev_ptr, prev_cap___struct_cap_C_' = prev_cap, preserve___unsigned_long_' = preserve, prefetch___unsigned_' = prefetch, pagesize___unsigned_long_' = pagesize, pageBits___unsigned_' = pageBits, ntfn_cap___struct_cap_C_' = ntfn_cap, node_ptr___ptr_to_struct_mdb_node_C_' = node_ptr, nodeSize___unsigned_long_' = nodeSize, next_ptr___unsigned_long_' = next_ptr, mdb_node___struct_mdb_node_C_' = mdb_node, it_v_reg___struct_v_region_C_' = it_v_reg, isSource___unsigned_long_' = isSource, irqState___unsigned_long_' = irqState, inverted___unsigned_long_' = inverted, invLabel___unsigned_long_' = invLabel, invLabel___int_' = invLabel___int, find_ret___struct_findPDForASID_ret_C_' = find_ret, fastfail___unsigned_long_' = fastfail, endpoint___ptr_to_struct_endpoint_C_' = endpoint, dtb_size___unsigned_long_' = dtb_size___unsigned_long, dtb_size___unsigned_' = dtb_size, destSlot___ptr_to_struct_cte_C_' = destSlot, data_ram___unsigned_' = data_ram, cnodeCap___struct_cap_C_' = cnodeCap, clzl_ret___unsigned_long_' = clzl_ret, cap_type___unsigned_long_' = cap_type, capIndex___unsigned_long_' = capIndex, capGuard___unsigned_long_' = capGuard, capFSize___unsigned_' = capFSize, capEPPtr___unsigned_' = capEPPtr, canGrant___unsigned_long_' = canGrant, cRootCap___struct_cap_C_' = cRootCap, boundTCB___ptr_to_struct_tcb_C_' = boundTCB, blocking___unsigned_long_' = blocking, bitsLeft___unsigned_' = bitsLeft, asidPool___ptr_to_struct_asid_pool_C_' = asidPool, archInfo___unsigned_long_' = archInfo, v_entry___unsigned_long_' = v_entry, untyped___struct_cap_C_' = untyped, trigger___unsigned_long_' = trigger, tcb_src___ptr_to_struct_tcb_C_' = tcb_src, tag_ram___unsigned_' = tag_ram, syscall___unsigned_long_' = syscall, srcSlot___ptr_to_struct_cte_C_' = srcSlot, srcRoot___struct_cap_C_' = srcRoot, sendBuf___ptr_to_unsigned_long_' = sendBuf, rootCap___struct_cap_C_' = rootCap, restart___unsigned_long_' = restart, res_ret___struct_resolveAddressBits_ret_C_' = res_ret, recvBuf___ptr_to_unsigned_long_' = recvBuf, ptr_src___ptr_to_void_' = ptr_src, ptr_dst___ptr_to_void_' = ptr_dst, pte_ptr___ptr_to_struct_pte_C_' = pte_ptr, pt_vptr___unsigned_long_' = pt_vptr, ptIndex___unsigned_' = ptIndex, poolPtr___ptr_to_struct_asid_pool_C_' = poolPtr, pde_ptr___ptr_to_struct_pde_C_' = pde_ptr, pdIndex___unsigned_' = pdIndex, pdIndex___unsigned_long_' = pdIndex___unsigned_long, ntfnPtr___ptr_to_struct_notification_C_' = ntfnPtr, ntfnCap___struct_cap_C_' = ntfnCap, node_id___unsigned_long_' = node_id, nodeCap___struct_cap_C_' = nodeCap, nextPtr___ptr_to_struct_cte_C_' = nextPtr, new_cap___struct_cap_C_' = new_cap, newType___unsigned_long_' = newType, newPrio___unsigned_long_' = newPrio, newData___unsigned_long_' = newData, msgInfo___unsigned_long_' = msgInfo, msgInfo___struct_seL4_MessageInfo_C_' = msgInfo___struct_seL4_MessageInfo_C, mdbPrev___unsigned_' = mdbPrev, mdbPrev___unsigned_long_' = mdbPrev___unsigned_long, mdbNode___struct_mdb_node_C_' = mdbNode, mdbNext___unsigned_' = mdbNext, mdbNext___unsigned_long_' = mdbNext___unsigned_long, map_ret___struct_create_mappings_pte_return_C_' = map_ret, map_ret___struct_create_mappings_pde_return_C_' = map_ret___struct_create_mappings_pde_return_C, lus_ret___struct_lookupSlot_ret_C_' = lus_ret, lufType___unsigned_long_' = lufType, luc_ret___struct_lookupCap_ret_C_' = luc_ret, l2index___unsigned_long_' = l2index, l1index___unsigned_long_' = l1index, irqSlot___ptr_to_struct_cte_C_' = irqSlot, initial___ptr_to_struct_tcb_C_' = initial, hw_asid___unsigned_char_' = hw_asid, freeRef___unsigned_long_' = freeRef, faultep___unsigned_long_' = faultep, faultEP___unsigned_long_' = faultEP, exposed___unsigned_long_' = exposed, endSlot___ptr_to_struct_cte_C_' = endSlot, do_call___unsigned_long_' = do_call, disable___unsigned_long_' = disable, destCap___struct_cap_C_' = destCap, cte_ptr___ptr_to_struct_cte_C_' = cte_ptr, context___ptr_to_struct_user_context_C_' = context, cap_ptr___ptr_to_struct_cap_C_' = cap_ptr, capData___unsigned_long_' = capData, basePtr___unsigned_long_' = basePtr, authTCB___ptr_to_struct_tcb_C_' = authTCB, authCap___struct_cap_C_' = authCap, address___unsigned_' = address, z_slot___ptr_to_struct_cte_C_' = z_slot, w_bits___unsigned_long_' = w_bits, ut_cap___struct_cap_C_' = ut_cap, ui_reg___struct_region_C_' = ui_reg, ts_ptr___ptr_to_struct_thread_state_C_' = ts_ptr, tsType___unsigned_long_' = tsType, thread___ptr_to_struct_tcb_C_' = thread, tcbptr___ptr_to_struct_tcb_C_' = tcbptr, target___unsigned_' = target___unsigned, target___unsigned_char_' = target___unsigned_char, target___ptr_to_struct_tcb_C_' = target, status___unsigned_long_' = status, srcTCB___ptr_to_struct_tcb_C_' = srcTCB, srcMDB___struct_mdb_node_C_' = srcMDB, srcCap___struct_cap_C_' = srcCap, sender___ptr_to_struct_tcb_C_' = sender, result___unsigned_long_' = result, pt_cap___struct_cap_C_' = pt_cap, ptSlot___ptr_to_struct_pte_C_' = ptSlot, pstart___unsigned_long_' = pstart, pd_val___unsigned_long_' = pd_val, pd_cap___struct_cap_C_' = pd_cap, pdSlot___ptr_to_struct_pde_C_' = pdSlot, parity___unsigned_long_' = parity, parent___ptr_to_struct_cte_C_' = parent, offset___unsigned_' = offset, offset___unsigned_long_' = offset___unsigned_long, offset___int_' = offset___int, number___unsigned_' = number, number___unsigned_long_' = number___unsigned_long, newMcp___unsigned_long_' = newMcp, newMDB___struct_mdb_node_C_' = newMDB, newCap___struct_cap_C_' = newCap, n_bits___unsigned_long_' = n_bits, maxlen___unsigned_long_' = maxlen, lu_ret___struct_lookupCapAndSlot_ret_C_' = lu_ret, lu_ret___struct_lookupCap_ret_C_' = lu_ret___struct_lookupCap_ret_C, lu_ret___struct_lookupPTSlot_ret_C_' = lu_ret___struct_lookupPTSlot_ret_C, lu_ret___struct_lookupSlot_ret_C_' = lu_ret___struct_lookupSlot_ret_C, lu_ret___struct_lookupSlot_raw_ret_C_' = lu_ret___struct_lookupSlot_raw_ret_C, length___unsigned_' = length, length___unsigned_long_' = length___unsigned_long, isMove___unsigned_long_' = isMove, isCall___unsigned_long_' = isCall, htpidr___unsigned_long_' = htpidr, header___struct_seL4_BootInfoHeader_C_' = header, fs_ret___struct_finaliseSlot_ret_C_' = fs_ret, fc_ret___struct_finaliseCap_ret_C_' = fc_ret, ep_ref___unsigned_long_' = ep_ref, ep_ptr___ptr_to_struct_endpoint_C_' = ep_ptr, ep_cap___struct_cap_C_' = ep_cap, epCPtr___unsigned_long_' = epCPtr, domain___unsigned_long_' = domain, do_map___unsigned_long_' = do_map, dc_ret___struct_deriveCap_ret_C_' = dc_ret, ctSlot___ptr_to_struct_cte_C_' = ctSlot, capptr___unsigned_long_' = capptr, cap_pd___ptr_to_struct_pde_C_' = cap_pd, capPtr___unsigned_' = capPtr, capIRQ___unsigned_' = capIRQ, caller___ptr_to_struct_tcb_C_' = caller, buffer___ptr_to_unsigned_long_' = buffer, badge2___unsigned_long_' = badge2, ap_cap___struct_cap_C_' = ap_cap, Domain___unsigned_' = Domain, vaddr___unsigned_long_' = vaddr, v_reg___struct_v_region_C_' = v_reg, state___unsigned_long_' = state, state___ptr_to_struct_thread_state_C_' = state___ptr_to_struct_thread_state_C, start___unsigned_long_' = start, slot3___ptr_to_struct_cte_C_' = slot3, slot2___ptr_to_struct_cte_C_' = slot2, slot1___ptr_to_struct_cte_C_' = slot1, size2___unsigned_long_' = size2, reset___unsigned_long_' = reset, radix___unsigned_long_' = radix, queue___struct_tcb_queue_C_' = queue, pdCap___struct_cap_C_' = pdCap, paddr___unsigned_long_' = paddr, p_reg___struct_p_region_C_' = p_reg, nsets___int_' = nsets, nirqs___int_' = nirqs, newPD___ptr_to_struct_pde_C_' = newPD, level___int_' = level, lbits___int_' = lbits, label___unsigned_' = label, label___unsigned_long_' = label___unsigned_long, irq_w___unsigned_long_' = irq_w, index___unsigned_long_' = index, index___int_' = index___int, guard___unsigned_long_' = guard, grant___unsigned_long_' = grant, frame___ptr_to_void_' = frame, frame___ptr_to_struct_kernel_frame_C_' = frame___ptr_to_struct_kernel_frame_C, fpsid___unsigned_long_' = fpsid, fpexc___unsigned_long_' = fpexc, flags___unsigned_long_' = flags, final___unsigned_long_' = final, fault___struct_seL4_Fault_C_' = fault, fault___unsigned_long_' = fault___unsigned_long, epptr___ptr_to_struct_endpoint_C_' = epptr, depth___unsigned_long_' = depth, cte_b___ptr_to_struct_cte_C_' = cte_b, cte_a___ptr_to_struct_cte_C_' = cte_a, cptr2___unsigned_long_' = cptr2, cpacr___unsigned_long_' = cpacr, count___unsigned_' = count, cnode___struct_cap_C_' = cnode, chunk___int_' = chunk, cap_b___struct_cap_C_' = cap_b, cap_a___struct_cap_C_' = cap_a, block___unsigned_long_' = block, badge___unsigned_long_' = badge, bBase___unsigned_long_' = bBase, assoc___int_' = assoc, aifsr___unsigned_long_' = aifsr, adfsr___unsigned_long_' = adfsr, actlr___unsigned_long_' = actlr, aBase___unsigned_long_' = aBase, AIFSR___unsigned_long_' = AIFSR, ADFSR___unsigned_long_' = ADFSR, ACTLR___unsigned_long_' = ACTLR, wptr___ptr_to_unsigned_long_' = wptr, word___int_' = word, vtop___unsigned_long_' = vtop, vptr___unsigned_long_' = vptr, type___unsigned_long_' = type, tptr___ptr_to_struct_tcb_C_' = tptr, topB___unsigned_long_' = topB, topA___unsigned_long_' = topA, tcap___struct_cap_C_' = tcap, tCap___struct_cap_C_' = tCap, slot___ptr_to_struct_cte_C_' = slot, size___unsigned_' = size, size___unsigned_long_' = size___unsigned_long, sent___unsigned_long_' = sent, root___struct_cap_C_' = root, ptr2___ptr_to_struct_cte_C_' = ptr2, prrr___unsigned_long_' = prrr, prio___unsigned_long_' = prio, prev___ptr_to_struct_cte_C_' = prev, pptr___ptr_to_void_' = pptr, pptr___unsigned_long_' = pptr___unsigned_long, pool___ptr_to_struct_asid_pool_C_' = pool, phys___unsigned_long_' = phys, ntfn___ptr_to_struct_notification_C_' = ntfn, nmrr___unsigned_long_' = nmrr, next___ptr_to_struct_cte_C_' = next, next___ptr_to_struct_tcb_C_' = next___ptr_to_struct_tcb_C, mdb2___struct_mdb_node_C_' = mdb2, mdb1___struct_mdb_node_C_' = mdb1, mask___unsigned_long_' = mask, mask___unsigned_' = mask___unsigned, mask___unsigned_longlong_' = mask___unsigned_longlong, line___unsigned_long_' = line, info___struct_seL4_MessageInfo_C_' = info, ifsr___unsigned_long_' = ifsr, ifar___unsigned_long_' = ifar, idx2___unsigned_long_' = idx2, diff___int_' = diff, dfsr___unsigned_long_' = dfsr, dfar___unsigned_long_' = dfar, dest___ptr_to_struct_tcb_C_' = dest, dest___ptr_to_char_' = dest___ptr_to_char, data___unsigned_long_' = data, ctag___enum_cap_tag_' = ctag, cptr___unsigned_long_' = cptr, code___unsigned_' = code, clid___int_' = clid, cidr___unsigned_long_' = cidr, cap2___struct_cap_C_' = cap2, cap1___struct_cap_C_' = cap1, call___unsigned_long_' = call, cPtr___unsigned_long_' = cPtr, botB___unsigned_long_' = botB, botA___unsigned_long_' = botA, bits___unsigned_long_' = bits, bits___unsigned_' = bits___unsigned, base___unsigned_long_' = base, base___unsigned_' = base___unsigned, bTop___unsigned_long_' = bTop, auth___ptr_to_struct_tcb_C_' = auth, attr___struct_vm_attributes_C_' = attr, asid___unsigned_long_' = asid, arch___unsigned_long_' = arch, addr___unsigned_long_' = addr, addr___unsigned_' = addr___unsigned, aTop___unsigned_long_' = aTop, PRRR___unsigned_long_' = PRRR, NMRR___unsigned_long_' = NMRR, IFSR___unsigned_long_' = IFSR, IFAR___unsigned_long_' = IFAR, DFSR___unsigned_long_' = DFSR, DFAR___unsigned_long_' = DFAR, CLID___unsigned_long_' = CLID, CIDR___unsigned_long_' = CIDR, wsl___unsigned_long_' = wsl, w_b___unsigned_long_' = w_b, w_a___unsigned_long_' = w_a, val___unsigned_long_' = val, val___long_' = val___long, v32___unsigned_' = v32, tex___unsigned_long_' = tex, tcb___ptr_to_struct_tcb_C_' = tcb, tag___struct_seL4_MessageInfo_C_' = tag, str___ptr_to_char_' = str, src___ptr_to_struct_tcb_C_' = src, src___ptr_to_char_' = src___ptr_to_char, scr___unsigned_long_' = scr, ret___unsigned_' = ret, ret___unsigned_long_' = ret___unsigned_long, ret___struct_findPDForASID_ret_C_' = ret___struct_findPDForASID_ret_C, ret___struct_lookupPTSlot_ret_C_' = ret___struct_lookupPTSlot_ret_C, ret___struct_resolve_ret_C_' = ret___struct_resolve_ret_C, ret___struct_create_mappings_pte_return_C_' = ret___struct_create_mappings_pte_return_C, ret___struct_create_mappings_pde_return_C_' = ret___struct_create_mappings_pde_return_C, ret___struct_deriveCap_ret_C_' = ret___struct_deriveCap_ret_C, ret___struct_lookupCap_ret_C_' = ret___struct_lookupCap_ret_C, ret___struct_lookupCapAndSlot_ret_C_' = ret___struct_lookupCapAndSlot_ret_C, ret___struct_lookupSlot_raw_ret_C_' = ret___struct_lookupSlot_raw_ret_C, ret___struct_lookupSlot_ret_C_' = ret___struct_lookupSlot_ret_C, ret___struct_resolveAddressBits_ret_C_' = ret___struct_resolveAddressBits_ret_C, ret___struct_finaliseSlot_ret_C_' = ret___struct_finaliseSlot_ret_C, res___long_' = res, reg___unsigned_long_' = reg, reg___struct_region_C_' = reg___struct_region_C, reg___struct_p_region_C_' = reg___struct_p_region_C, ptr___unsigned_long_' = ptr, ptr___ptr_to_unsigned_long_' = ptr___ptr_to_unsigned_long, ptr___ptr_to_struct_cte_C_' = ptr___ptr_to_struct_cte_C, pte___struct_pte_C_' = pte, pte___ptr_to_struct_pte_C_' = pte___ptr_to_struct_pte_C, pde___struct_pde_C_' = pde, pde___ptr_to_struct_pde_C_' = pde___ptr_to_struct_pde_C, msb___unsigned_long_' = msb, mdb___struct_mdb_node_C_' = mdb, mcp___unsigned_long_' = mcp, max___unsigned_long_' = max, luf___struct_lookup_fault_C_' = luf, lou___int_' = lou, loc___int_' = loc, len___unsigned_long_' = len, irq___unsigned_long_' = irq, idx___unsigned_long_' = idx, ex1___struct_seL4_Fault_C_' = ex1, end___unsigned_long_' = end, dom___unsigned_long_' = dom, cte___ptr_to_struct_cte_C_' = cte, cpu___unsigned_long_' = cpu, cap___struct_cap_C_' = cap, bit___int_' = bit, aux___unsigned_' = aux, acr___unsigned_long_' = acr, TEX___unsigned_' = TEX, FSR___unsigned_' = FSR, FAR___unsigned_long_' = FAR, APX___unsigned_' = APX, ts___unsigned_long_' = ts, sz___unsigned_long_' = sz, s2___ptr_to_char_' = s2, s1___ptr_to_char_' = s1, pt___ptr_to_struct_pte_C_' = pt, pd___ptr_to_struct_pde_C_' = pd, pd___struct_cap_C_' = pd___struct_cap_C, pd___struct_findPDForASID_ret_C_' = pd___struct_findPDForASID_ret_C, pc___unsigned_long_' = pc, pa___unsigned_long_' = pa, nG___unsigned_' = nG, mi___struct_seL4_MessageInfo_C_' = mi, id___unsigned_long_' = id, id___anonymous_enum_' = id___anonymous_enum, ep___ptr_to_struct_endpoint_C_' = ep, ct___struct_cap_transfer_C_' = ct, bi___ptr_to_struct_seL4_BootInfo_C_' = bi, ap___ptr_to_struct_asid_pool_C_' = ap, ap___unsigned_long_' = ap___unsigned_long, XN___unsigned_' = XN, AP___unsigned_' = AP, y___unsigned_' = y, y___int_' = y___int, x___unsigned_' = x, x___unsigned_longlong_' = x___unsigned_longlong, x___unsigned_long_' = x___unsigned_long, x___int_' = x___int, w___unsigned_long_' = w, w___int_' = w___int, w___struct_seL4_CNode_CapData_C_' = w___struct_seL4_CNode_CapData_C, v___unsigned_long_' = va, v___int_' = v___int, v___unsigned_' = v___unsigned, t___unsigned_long_' = t, s___unsigned_long_' = s___unsigned_long, s___ptr_to_char_' = s___ptr_to_char, s___ptr_to_void_' = s, r___unsigned_long_' = r, r___ptr_to_struct_p_region_C_' = r___ptr_to_struct_p_region_C, r___ptr_to_struct_region_C_' = r___ptr_to_struct_region_C, q___ptr_to_unsigned_char_' = q, p___unsigned_long_' = p, p___ptr_to_unsigned_char_' = p___ptr_to_unsigned_char, n___unsigned_long_' = n, n___int_' = n___int, m___struct_region_C_' = m, l___int_' = l, j___unsigned_long_' = j, i___unsigned_long_' = i, i___unsigned_' = i___unsigned, i___int_' = i___int, f___unsigned_long_' = f, e___unsigned_long_' = e, c___unsigned_long_' = c, c___char_' = c___char, b___unsigned_long_' = b, a___unsigned_long_' = a, S___unsigned_' = S, P___unsigned_' = P, C___unsigned_' = C, B___unsigned_' = B, \<dots> = morea\<rparr>)) \<longrightarrow> xfu' (\<lambda>_. v) \<lparr>globals = \<lparr>t_hrs_' = t_hrs, phantom_machine_state_' = phantom_machine_state, ghost'state_' = ghost'state, avail_reg_' = avail_reg, ksNumCPUs_' = ksNumCPUs, ndks_boot_' = ndks_boot, active_irq_' = active_irq, rootserver_' = rootserver, ksCurDomain_' = ksCurDomain, ksCurThread_' = ksCurThread, ksDomainTime_' = ksDomainTime, ksIdleThread_' = ksIdleThread, tlbLockCount_' = tlbLockCount, armKSNextASID_' = armKSNextASID, current_fault_' = current_fault, ksReadyQueues_' = ksReadyQueues, armKSASIDTable_' = armKSASIDTable, rootserver_mem_' = rootserver_mem, armKSHWASIDTable_' = armKSHWASIDTable, intStateIRQTable_' = intStateIRQTable, ksDomScheduleIdx_' = ksDomScheduleIdx, ksSchedulerAction_' = ksSchedulerAction, current_extra_caps_' = current_extra_caps, isFPUEnabledCached_' = isFPUEnabledCached, current_lookup_fault_' = current_lookup_fault, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted, current_syscall_error_' = current_syscall_error, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap, \<dots> = more\<rparr>, global_exn_var_' = global_exn_var, ret__struct_create_frames_of_region_ret_C_' = ret__struct_create_frames_of_region_ret_C, ret__struct_create_mappings_pte_return_C_' = ret__struct_create_mappings_pte_return_C, ret__struct_create_mappings_pde_return_C_' = ret__struct_create_mappings_pde_return_C, ret__struct_resolveAddressBits_ret_C_' = ret__struct_resolveAddressBits_ret_C, ret__struct_lookupCapAndSlot_ret_C_' = ret__struct_lookupCapAndSlot_ret_C, ret__struct_lookupSlot_raw_ret_C_' = ret__struct_lookupSlot_raw_ret_C, ret__struct_findPDForASID_ret_C_' = ret__struct_findPDForASID_ret_C, ret__struct_seL4_MessageInfo_C_' = ret__struct_seL4_MessageInfo_C, ret__struct_lookupPTSlot_ret_C_' = ret__struct_lookupPTSlot_ret_C, ret__struct_finaliseSlot_ret_C_' = ret__struct_finaliseSlot_ret_C, ret__struct_seL4_SlotRegion_C_' = ret__struct_seL4_SlotRegion_C, ret__struct_finaliseCap_ret_C_' = ret__struct_finaliseCap_ret_C, ret__struct_seL4_CapRights_C_' = ret__struct_seL4_CapRights_C, ret__struct_lookupSlot_ret_C_' = ret__struct_lookupSlot_ret_C, ret__struct_vm_attributes_C_' = ret__struct_vm_attributes_C, ret__struct_lookupCap_ret_C_' = ret__struct_lookupCap_ret_C, ret__struct_deriveCap_ret_C_' = ret__struct_deriveCap_ret_C, ret__struct_lookup_fault_C_' = ret__struct_lookup_fault_C, ret__struct_cap_transfer_C_' = ret__struct_cap_transfer_C, ret__struct_resolve_ret_C_' = ret__struct_resolve_ret_C, ret__ptr_to_unsigned_long_' = ret__ptr_to_unsigned_long, ret__struct_seL4_Fault_C_' = ret__struct_seL4_Fault_C, ret__ptr_to_struct_tcb_C_' = ret__ptr_to_struct_tcb_C, ret__ptr_to_struct_pte_C_' = ret__ptr_to_struct_pte_C, ret__ptr_to_struct_pde_C_' = ret__ptr_to_struct_pde_C, ret__ptr_to_struct_cte_C_' = ret__ptr_to_struct_cte_C, ret__struct_tcb_queue_C_' = ret__struct_tcb_queue_C, ret__struct_p_region_C_' = ret__struct_p_region_C, ret__struct_mdb_node_C_' = ret__struct_mdb_node_C, original_lookup_fault___struct_lookup_fault_C_' = original_lookup_fault, unsigned_long_eret_4_' = unsigned_long_eret_4, unsigned_long_eret_3_' = unsigned_long_eret_3, unsigned_long_eret_2_' = unsigned_long_eret_2, ret__struct_region_C_' = ret__struct_region_C, struct_cap_C_eret_3_' = struct_cap_C_eret_3, struct_cap_C_eret_2_' = struct_cap_C_eret_2, extra_bi_frame_vptr___unsigned_long_' = extra_bi_frame_vptr, seL4_CNode_CapData___struct_seL4_CNode_CapData_C_' = seL4_CNode_CapData, ret__unsigned_long_' = ret__unsigned_long, ret__unsigned_char_' = ret__unsigned_char, ptr_to_void_eret_2_' = ptr_to_void_eret_2, first_untyped_slot___unsigned_long_' = first_untyped_slot, extra_bi_size_bits___unsigned_long_' = extra_bi_size_bits, capPTMappedAddress___unsigned_' = capPTMappedAddress, capFMappedASIDHigh___unsigned_' = capFMappedASIDHigh, boot_mem_reuse_reg___struct_region_C_' = boot_mem_reuse_reg, tlbflush_required___unsigned_long_' = tlbflush_required, stored_asid_valid___unsigned_' = stored_asid_valid, ret__struct_pte_C_' = ret__struct_pte_C, ret__struct_pde_C_' = ret__struct_pde_C, ret__struct_cap_C_' = ret__struct_cap_C, receiverIPCBuffer___ptr_to_unsigned_long_' = receiverIPCBuffer, newCapIsRevocable___unsigned_long_' = newCapIsRevocable, create_frames_ret___struct_create_frames_of_region_ret_C_' = create_frames_ret, capNtfnCanReceive___unsigned_' = capNtfnCanReceive, capFMappedAddress___unsigned_' = capFMappedAddress, capFMappedASIDLow___unsigned_' = capFMappedASIDLow, capCNodeGuardSize___unsigned_' = capCNodeGuardSize, untypedFreeBytes___unsigned_long_' = untypedFreeBytes, thread_state_ptr___ptr_to_struct_thread_state_C_' = thread_state_ptr, size_unique_name___unsigned_long_' = size_unique_name, seL4_MessageInfo___struct_seL4_MessageInfo_C_' = seL4_MessageInfo, scheduler_action___ptr_to_struct_tcb_C_' = scheduler_action, ret__ptr_to_void_' = ret__ptr_to_void, receiveIPCBuffer___ptr_to_unsigned_long_' = receiveIPCBuffer, prevIsSameObject___unsigned_long_' = prevIsSameObject, notification_ptr___ptr_to_struct_notification_C_' = notification_ptr, l1index_inverted___unsigned_long_' = l1index_inverted, instructionFault___unsigned_' = instructionFault, capReplyCanGrant___unsigned_' = capReplyCanGrant, capReplyCanGrant___unsigned_long_' = capReplyCanGrant___unsigned_long, capCanGrantReply___unsigned_' = capCanGrantReply, armParityEnabled___unsigned_' = armParityEnabled, armPageCacheable___unsigned_' = armPageCacheable, unsigned_eret_6_' = unsigned_eret_6, unsigned_eret_5_' = unsigned_eret_5, unsigned_eret_4_' = unsigned_eret_4, unsigned_eret_3_' = unsigned_eret_3, unsigned_eret_2_' = unsigned_eret_2, unaligned_start___unsigned_long_' = unaligned_start, transferInteger___unsigned_long_' = transferInteger, totalObjectSize___unsigned_long_' = totalObjectSize, slot_pos_before___unsigned_long_' = slot_pos_before, extra_bi_region___struct_region_C_' = extra_bi_region, extra_bi_offset___unsigned_long_' = extra_bi_offset, cnode_size_bits___unsigned_long_' = cnode_size_bits, cap_rights_mask___struct_seL4_CapRights_C_' = cap_rights_mask, capPTMappedASID___unsigned_' = capPTMappedASID, capPDMappedASID___unsigned_' = capPDMappedASID, armExecuteNever___unsigned_' = armExecuteNever, ui_p_reg_start___unsigned_long_' = ui_p_reg_start, stored_hw_asid___unsigned_' = stored_hw_asid, stored_hw_asid___struct_pde_C_' = stored_hw_asid___struct_pde_C, slot_pos_after___unsigned_long_' = slot_pos_after, seL4_CapRights___struct_seL4_CapRights_C_' = seL4_CapRights, root_cnode_cap___struct_cap_C_' = root_cnode_cap, msgTransferred___unsigned_long_' = msgTransferred, mdbFirstBadged___unsigned_' = mdbFirstBadged, mdbFirstBadged___unsigned_long_' = mdbFirstBadged___unsigned_long, inReceivePhase___unsigned_' = inReceivePhase, hw_asid_offset___unsigned_long_' = hw_asid_offset, currentPDEType___enum_pde_tag_' = currentPDEType, cptr_bufferPtr___unsigned_long_' = cptr_bufferPtr, capReplyMaster___unsigned_' = capReplyMaster, capReplyMaster___unsigned_long_' = capReplyMaster___unsigned_long, capNtfnCanSend___unsigned_' = capNtfnCanSend, alignedFreeRef___unsigned_long_' = alignedFreeRef, vm_attributes___struct_vm_attributes_C_' = vm_attributes, vRoot_srcSlot___ptr_to_struct_cte_C_' = vRoot_srcSlot, transferFrame___unsigned_long_' = transferFrame, syscallNumber___unsigned_' = syscallNumber, suspendSource___unsigned_long_' = suspendSource, stack_address___unsigned_long_' = stack_address, root_switched___unsigned_long_' = root_switched, ret__unsigned_' = ret__unsigned, ret__longlong_' = ret__longlong, replyCanGrant___unsigned_long_' = replyCanGrant, receiveBuffer___ptr_to_void_' = receiveBuffer___ptr_to_void, receiveBuffer___ptr_to_unsigned_long_' = receiveBuffer, nonexecutable___unsigned_long_' = nonexecutable, mva_plus_asid___unsigned_long_' = mva_plus_asid, fpsid_subarch___unsigned_long_' = fpsid_subarch, extra_bi_size___unsigned_long_' = extra_bi_size, dtb_phys_addr___unsigned_long_' = dtb_phys_addr, device_memory___unsigned_long_' = device_memory, cmp_size_bits___unsigned_long_' = cmp_size_bits, capsUnwrapped___unsigned_' = capsUnwrapped, capZombieType___unsigned_' = capZombieType, capPTIsMapped___unsigned_' = capPTIsMapped, capPDIsMapped___unsigned_' = capPDIsMapped, capCanReceive___unsigned_' = capCanReceive, capCNodeRadix___unsigned_' = capCNodeRadix, capCNodeGuard___unsigned_' = capCNodeGuard, canGrantReply___unsigned_long_' = canGrantReply, cRoot_srcSlot___ptr_to_struct_cte_C_' = cRoot_srcSlot, bufferSrcSlot___ptr_to_struct_cte_C_' = bufferSrcSlot, bi_frame_vptr___unsigned_long_' = bi_frame_vptr, was_runnable___unsigned_long_' = was_runnable, w_rightsMask___unsigned_long_' = w_rightsMask, vm_faultType___unsigned_long_' = vm_faultType, vRoot_newCap___struct_cap_C_' = vRoot_newCap, ui_p_reg_end___unsigned_long_' = ui_p_reg_end, transferArch___unsigned_long_' = transferArch, thread_state___struct_thread_state_C_' = thread_state, resumeTarget___unsigned_long_' = resumeTarget, processor_id___unsigned_long_' = processor_id, pivotNewData___unsigned_long_' = pivotNewData, nextFreeArea___ptr_to_void_' = nextFreeArea, mdb_node_ptr___ptr_to_struct_mdb_node_C_' = mdb_node_ptr, mdbRevocable___unsigned_' = mdbRevocable, mdbRevocable___unsigned_long_' = mdbRevocable___unsigned_long, lookup_fault___struct_lookup_fault_C_' = lookup_fault, extra_bi_ret___struct_create_frames_of_region_ret_C_' = extra_bi_ret, epQueue_tail___unsigned_long_' = epQueue_tail, epQueue_head___unsigned_long_' = epQueue_head, endpoint_ptr___ptr_to_struct_endpoint_C_' = endpoint_ptr, endpointTail___ptr_to_struct_tcb_C_' = endpointTail, dtb_phys_end___unsigned_long_' = dtb_phys_end, deviceMemory___unsigned_long_' = deviceMemory, cap_type_tag___unsigned_' = cap_type_tag, capPTBasePtr___unsigned_' = capPTBasePtr, capPDBasePtr___unsigned_' = capPDBasePtr, capNtfnBadge___unsigned_' = capNtfnBadge, capFreeIndex___unsigned_' = capFreeIndex, capFVMRights___unsigned_' = capFVMRights, capFIsDevice___unsigned_' = capFIsDevice, capBlockSize___unsigned_' = capBlockSize, cRoot_newCap___struct_cap_C_' = cRoot_newCap, w_bufferPtr___unsigned_long_' = w_bufferPtr, userObjSize___unsigned_long_' = userObjSize, updateFlags___unsigned_long_' = updateFlags, resolve_ret___struct_resolve_ret_C_' = resolve_ret, pte_entries___struct_pte_range_C_' = pte_entries, pde_entries___struct_pde_range_C_' = pde_entries, new_hw_asid___unsigned_char_' = new_hw_asid, newPivotCap___struct_cap_C_' = newPivotCap, n_available___unsigned_long_' = n_available, ipcbuf_vptr___unsigned_long_' = ipcbuf_vptr, instruction___unsigned_long_' = instruction, handlerSlot___ptr_to_struct_cte_C_' = handlerSlot, handlerCPtr___unsigned_long_' = handlerCPtr, empty_index___int_' = empty_index, controlSlot___ptr_to_struct_cte_C_' = controlSlot, cleanupInfo___struct_cap_C_' = cleanupInfo, capZombieID___unsigned_' = capZombieID, capVMRights___unsigned_long_' = capVMRights, capIsDevice___unsigned_' = capIsDevice, capFBasePtr___unsigned_' = capFBasePtr, capFBasePtr___unsigned_long_' = capFBasePtr___unsigned_long, capCanGrant___unsigned_' = capCanGrant, capCNodePtr___unsigned_' = capCNodePtr, capASIDPool___unsigned_' = capASIDPool, capASIDBase___unsigned_' = capASIDBase, ui_v_entry___unsigned_long_' = ui_v_entry, threadRoot___struct_cap_C_' = threadRoot, targetSlot___ptr_to_struct_pte_C_' = targetSlot, targetSlot___ptr_to_struct_pde_C_' = targetSlot___ptr_to_struct_pde_C, srcNewData___unsigned_long_' = srcNewData, source_cap___struct_cap_C_' = source_cap, sendBuffer___ptr_to_void_' = sendBuffer___ptr_to_void, sendBuffer___ptr_to_unsigned_long_' = sendBuffer, seL4_Fault___struct_seL4_Fault_C_' = seL4_Fault, retypeBase___ptr_to_void_' = retypeBase, regionBase___ptr_to_void_' = regionBase, pivotIndex___unsigned_long_' = pivotIndex, pivotDepth___unsigned_long_' = pivotDepth, parentSlot___ptr_to_struct_cte_C_' = parentSlot, objectSize___unsigned_long_' = objectSize, ntfn_queue___struct_tcb_queue_C_' = ntfn_queue, nodeWindow___unsigned_long_' = nodeWindow, nodeOffset___unsigned_long_' = nodeOffset, n_reserved___unsigned_long_' = n_reserved, isReceiver___unsigned_long_' = isReceiver, isBlocking___unsigned_long_' = isBlocking, ipcbuf_cap___struct_cap_C_' = ipcbuf_cap, ipc_buffer___ptr_to_unsigned_long_' = ipc_buffer, int_eret_3_' = int_eret_3, int_eret_2_' = int_eret_2, handlerCap___struct_cap_C_' = handlerCap, guardFound___unsigned_' = guardFound, fault_type___unsigned_long_' = fault_type, extra_size___unsigned_long_' = extra_size, executable___unsigned_long_' = executable, dtb_addr_p___unsigned_long_' = dtb_addr_p, destOffset___unsigned_long_' = destOffset, destLength___unsigned_long_' = destLength, derivedCap___struct_cap_C_' = derivedCap, cur_thread___ptr_to_struct_tcb_C_' = cur_thread, csselr_old___unsigned_long_' = csselr_old, cap_rights___struct_seL4_CapRights_C_' = cap_rights, capNtfnPtr___unsigned_' = capNtfnPtr, capEPBadge___unsigned_' = capEPBadge, capCanSend___unsigned_' = capCanSend, callerSlot___ptr_to_struct_cte_C_' = callerSlot, bufferSlot___ptr_to_struct_cte_C_' = bufferSlot, bufferAddr___unsigned_long_' = bufferAddr, block_size___unsigned_long_' = block_size, attributes___struct_vm_attributes_C_' = attributes, assoc_bits___int_' = assoc_bits, align_bits___unsigned_' = align_bits, StrictC'_v___unsigned_long_' = StrictC'_v, vm_rights___unsigned_long_' = vm_rights, vbase_ptr___ptr_to_void_' = vbase_ptr, vRootSlot___ptr_to_struct_cte_C_' = vRootSlot, vRootData___unsigned_long_' = vRootData, use_large___unsigned_long_' = use_large, threadPtr___ptr_to_struct_tcb_C_' = threadPtr, stack_top___unsigned_long_' = stack_top, size_bits___unsigned_long_' = size_bits, size_bits___unsigned_' = size_bits___unsigned, ret__long_' = ret__long, replySlot___ptr_to_struct_cte_C_' = replySlot, radixBits___unsigned_long_' = radixBits, pv_offset___long_' = pv_offset, pivotSlot___ptr_to_struct_cte_C_' = pivotSlot, pivotRoot___struct_cap_C_' = pivotRoot, pdCapSlot___ptr_to_struct_cte_C_' = pdCapSlot, page_size___unsigned_long_' = page_size, page_base___unsigned_long_' = page_base, num_nodes___unsigned_long_' = num_nodes, nodeIndex___unsigned_long_' = nodeIndex, nodeDepth___unsigned_long_' = nodeDepth, newVTable___struct_cap_C_' = newVTable, newSrcCap___struct_cap_C_' = newSrcCap, masterCap___struct_cap_C_' = masterCap, levelBits___unsigned_long_' = levelBits, it_pd_cap___struct_cap_C_' = it_pd_cap, it_ap_cap___struct_cap_C_' = it_ap_cap, ipcBuffer___ptr_to_unsigned_long_' = ipcBuffer, immediate___unsigned_long_' = immediate, haveHWFPU___unsigned_long_' = haveHWFPU, guardSize___unsigned_long_' = guardSize, guardBits___unsigned_long_' = guardBits, global_pd___ptr_to_struct_pde_C_' = global_pd, freeIndex___unsigned_long_' = freeIndex, frame_cap___struct_cap_C_' = frame_cap, frameSize___unsigned_long_' = frameSize, faultType___unsigned_long_' = faultType, extraCaps___unsigned_' = extraCaps, dtb_p_reg___struct_p_region_C_' = dtb_p_reg, destCNode___ptr_to_struct_cte_C_' = destCNode, capTCBPtr___unsigned_' = capTCBPtr, capTCBPtr___unsigned_long_' = capTCBPtr___unsigned_long, candidate___ptr_to_struct_tcb_C_' = candidate, callerCap___struct_cap_C_' = callerCap, callerCap___ptr_to_struct_cte_C_' = callerCap___ptr_to_struct_cte_C, cacheable___unsigned_long_' = cacheable, cRootSlot___ptr_to_struct_cte_C_' = cRootSlot, cRootData___unsigned_long_' = cRootData, bufferPtr___ptr_to_unsigned_long_' = bufferPtr, bufferCap___struct_cap_C_' = bufferCap, bitsFound___unsigned_' = bitsFound, base_addr___unsigned_long_' = base_addr, baseValue___unsigned_long_' = baseValue, available___ptr_to_struct_p_region_C_' = available, asid_base___unsigned_long_' = asid_base, allocated___unsigned_long_' = allocated, alignment___unsigned_long_' = alignment, vmRights___unsigned_long_' = vmRights, vRootCap___struct_cap_C_' = vRootCap, userSize___unsigned_long_' = userSize, ui_v_reg___struct_v_region_C_' = ui_v_reg, ui_p_reg___struct_p_region_C_' = ui_p_reg, transfer___struct_cap_transfer_C_' = transfer, tls_base___unsigned_long_' = tls_base, tcb_dest___ptr_to_struct_tcb_C_' = tcb_dest, srcIndex___unsigned_long_' = srcIndex, srcDepth___unsigned_long_' = srcDepth, slot_ptr___ptr_to_struct_cte_C_' = slot_ptr, rootSlot___ptr_to_struct_cte_C_' = rootSlot, ret__int_' = ret__int, reserved___unsigned_' = reserved, reserved___ptr_to_struct_region_C_' = reserved___ptr_to_struct_region_C, receiver___ptr_to_struct_tcb_C_' = receiver, priority___unsigned_long_' = priority, prev_ptr___unsigned_long_' = prev_ptr, prev_cap___struct_cap_C_' = prev_cap, preserve___unsigned_long_' = preserve, prefetch___unsigned_' = prefetch, pagesize___unsigned_long_' = pagesize, pageBits___unsigned_' = pageBits, ntfn_cap___struct_cap_C_' = ntfn_cap, node_ptr___ptr_to_struct_mdb_node_C_' = node_ptr, nodeSize___unsigned_long_' = nodeSize, next_ptr___unsigned_long_' = next_ptr, mdb_node___struct_mdb_node_C_' = mdb_node, it_v_reg___struct_v_region_C_' = it_v_reg, isSource___unsigned_long_' = isSource, irqState___unsigned_long_' = irqState, inverted___unsigned_long_' = inverted, invLabel___unsigned_long_' = invLabel, invLabel___int_' = invLabel___int, find_ret___struct_findPDForASID_ret_C_' = find_ret, fastfail___unsigned_long_' = fastfail, endpoint___ptr_to_struct_endpoint_C_' = endpoint, dtb_size___unsigned_long_' = dtb_size___unsigned_long, dtb_size___unsigned_' = dtb_size, destSlot___ptr_to_struct_cte_C_' = destSlot, data_ram___unsigned_' = data_ram, cnodeCap___struct_cap_C_' = cnodeCap, clzl_ret___unsigned_long_' = clzl_ret, cap_type___unsigned_long_' = cap_type, capIndex___unsigned_long_' = capIndex, capGuard___unsigned_long_' = capGuard, capFSize___unsigned_' = capFSize, capEPPtr___unsigned_' = capEPPtr, canGrant___unsigned_long_' = canGrant, cRootCap___struct_cap_C_' = cRootCap, boundTCB___ptr_to_struct_tcb_C_' = boundTCB, blocking___unsigned_long_' = blocking, bitsLeft___unsigned_' = bitsLeft, asidPool___ptr_to_struct_asid_pool_C_' = asidPool, archInfo___unsigned_long_' = archInfo, v_entry___unsigned_long_' = v_entry, untyped___struct_cap_C_' = untyped, trigger___unsigned_long_' = trigger, tcb_src___ptr_to_struct_tcb_C_' = tcb_src, tag_ram___unsigned_' = tag_ram, syscall___unsigned_long_' = syscall, srcSlot___ptr_to_struct_cte_C_' = srcSlot, srcRoot___struct_cap_C_' = srcRoot, sendBuf___ptr_to_unsigned_long_' = sendBuf, rootCap___struct_cap_C_' = rootCap, restart___unsigned_long_' = restart, res_ret___struct_resolveAddressBits_ret_C_' = res_ret, recvBuf___ptr_to_unsigned_long_' = recvBuf, ptr_src___ptr_to_void_' = ptr_src, ptr_dst___ptr_to_void_' = ptr_dst, pte_ptr___ptr_to_struct_pte_C_' = pte_ptr, pt_vptr___unsigned_long_' = pt_vptr, ptIndex___unsigned_' = ptIndex, poolPtr___ptr_to_struct_asid_pool_C_' = poolPtr, pde_ptr___ptr_to_struct_pde_C_' = pde_ptr, pdIndex___unsigned_' = pdIndex, pdIndex___unsigned_long_' = pdIndex___unsigned_long, ntfnPtr___ptr_to_struct_notification_C_' = ntfnPtr, ntfnCap___struct_cap_C_' = ntfnCap, node_id___unsigned_long_' = node_id, nodeCap___struct_cap_C_' = nodeCap, nextPtr___ptr_to_struct_cte_C_' = nextPtr, new_cap___struct_cap_C_' = new_cap, newType___unsigned_long_' = newType, newPrio___unsigned_long_' = newPrio, newData___unsigned_long_' = newData, msgInfo___unsigned_long_' = msgInfo, msgInfo___struct_seL4_MessageInfo_C_' = msgInfo___struct_seL4_MessageInfo_C, mdbPrev___unsigned_' = mdbPrev, mdbPrev___unsigned_long_' = mdbPrev___unsigned_long, mdbNode___struct_mdb_node_C_' = mdbNode, mdbNext___unsigned_' = mdbNext, mdbNext___unsigned_long_' = mdbNext___unsigned_long, map_ret___struct_create_mappings_pte_return_C_' = map_ret, map_ret___struct_create_mappings_pde_return_C_' = map_ret___struct_create_mappings_pde_return_C, lus_ret___struct_lookupSlot_ret_C_' = lus_ret, lufType___unsigned_long_' = lufType, luc_ret___struct_lookupCap_ret_C_' = luc_ret, l2index___unsigned_long_' = l2index, l1index___unsigned_long_' = l1index, irqSlot___ptr_to_struct_cte_C_' = irqSlot, initial___ptr_to_struct_tcb_C_' = initial, hw_asid___unsigned_char_' = hw_asid, freeRef___unsigned_long_' = freeRef, faultep___unsigned_long_' = faultep, faultEP___unsigned_long_' = faultEP, exposed___unsigned_long_' = exposed, endSlot___ptr_to_struct_cte_C_' = endSlot, do_call___unsigned_long_' = do_call, disable___unsigned_long_' = disable, destCap___struct_cap_C_' = destCap, cte_ptr___ptr_to_struct_cte_C_' = cte_ptr, context___ptr_to_struct_user_context_C_' = context, cap_ptr___ptr_to_struct_cap_C_' = cap_ptr, capData___unsigned_long_' = capData, basePtr___unsigned_long_' = basePtr, authTCB___ptr_to_struct_tcb_C_' = authTCB, authCap___struct_cap_C_' = authCap, address___unsigned_' = address, z_slot___ptr_to_struct_cte_C_' = z_slot, w_bits___unsigned_long_' = w_bits, ut_cap___struct_cap_C_' = ut_cap, ui_reg___struct_region_C_' = ui_reg, ts_ptr___ptr_to_struct_thread_state_C_' = ts_ptr, tsType___unsigned_long_' = tsType, thread___ptr_to_struct_tcb_C_' = thread, tcbptr___ptr_to_struct_tcb_C_' = tcbptr, target___unsigned_' = target___unsigned, target___unsigned_char_' = target___unsigned_char, target___ptr_to_struct_tcb_C_' = target, status___unsigned_long_' = status, srcTCB___ptr_to_struct_tcb_C_' = srcTCB, srcMDB___struct_mdb_node_C_' = srcMDB, srcCap___struct_cap_C_' = srcCap, sender___ptr_to_struct_tcb_C_' = sender, result___unsigned_long_' = result, pt_cap___struct_cap_C_' = pt_cap, ptSlot___ptr_to_struct_pte_C_' = ptSlot, pstart___unsigned_long_' = pstart, pd_val___unsigned_long_' = pd_val, pd_cap___struct_cap_C_' = pd_cap, pdSlot___ptr_to_struct_pde_C_' = pdSlot, parity___unsigned_long_' = parity, parent___ptr_to_struct_cte_C_' = parent, offset___unsigned_' = offset, offset___unsigned_long_' = offset___unsigned_long, offset___int_' = offset___int, number___unsigned_' = number, number___unsigned_long_' = number___unsigned_long, newMcp___unsigned_long_' = newMcp, newMDB___struct_mdb_node_C_' = newMDB, newCap___struct_cap_C_' = newCap, n_bits___unsigned_long_' = n_bits, maxlen___unsigned_long_' = maxlen, lu_ret___struct_lookupCapAndSlot_ret_C_' = lu_ret, lu_ret___struct_lookupCap_ret_C_' = lu_ret___struct_lookupCap_ret_C, lu_ret___struct_lookupPTSlot_ret_C_' = lu_ret___struct_lookupPTSlot_ret_C, lu_ret___struct_lookupSlot_ret_C_' = lu_ret___struct_lookupSlot_ret_C, lu_ret___struct_lookupSlot_raw_ret_C_' = lu_ret___struct_lookupSlot_raw_ret_C, length___unsigned_' = length, length___unsigned_long_' = length___unsigned_long, isMove___unsigned_long_' = isMove, isCall___unsigned_long_' = isCall, htpidr___unsigned_long_' = htpidr, header___struct_seL4_BootInfoHeader_C_' = header, fs_ret___struct_finaliseSlot_ret_C_' = fs_ret, fc_ret___struct_finaliseCap_ret_C_' = fc_ret, ep_ref___unsigned_long_' = ep_ref, ep_ptr___ptr_to_struct_endpoint_C_' = ep_ptr, ep_cap___struct_cap_C_' = ep_cap, epCPtr___unsigned_long_' = epCPtr, domain___unsigned_long_' = domain, do_map___unsigned_long_' = do_map, dc_ret___struct_deriveCap_ret_C_' = dc_ret, ctSlot___ptr_to_struct_cte_C_' = ctSlot, capptr___unsigned_long_' = capptr, cap_pd___ptr_to_struct_pde_C_' = cap_pd, capPtr___unsigned_' = capPtr, capIRQ___unsigned_' = capIRQ, caller___ptr_to_struct_tcb_C_' = caller, buffer___ptr_to_unsigned_long_' = buffer, badge2___unsigned_long_' = badge2, ap_cap___struct_cap_C_' = ap_cap, Domain___unsigned_' = Domain, vaddr___unsigned_long_' = vaddr, v_reg___struct_v_region_C_' = v_reg, state___unsigned_long_' = state, state___ptr_to_struct_thread_state_C_' = state___ptr_to_struct_thread_state_C, start___unsigned_long_' = start, slot3___ptr_to_struct_cte_C_' = slot3, slot2___ptr_to_struct_cte_C_' = slot2, slot1___ptr_to_struct_cte_C_' = slot1, size2___unsigned_long_' = size2, reset___unsigned_long_' = reset, radix___unsigned_long_' = radix, queue___struct_tcb_queue_C_' = queue, pdCap___struct_cap_C_' = pdCap, paddr___unsigned_long_' = paddr, p_reg___struct_p_region_C_' = p_reg, nsets___int_' = nsets, nirqs___int_' = nirqs, newPD___ptr_to_struct_pde_C_' = newPD, level___int_' = level, lbits___int_' = lbits, label___unsigned_' = label, label___unsigned_long_' = label___unsigned_long, irq_w___unsigned_long_' = irq_w, index___unsigned_long_' = index, index___int_' = index___int, guard___unsigned_long_' = guard, grant___unsigned_long_' = grant, frame___ptr_to_void_' = frame, frame___ptr_to_struct_kernel_frame_C_' = frame___ptr_to_struct_kernel_frame_C, fpsid___unsigned_long_' = fpsid, fpexc___unsigned_long_' = fpexc, flags___unsigned_long_' = flags, final___unsigned_long_' = final, fault___struct_seL4_Fault_C_' = fault, fault___unsigned_long_' = fault___unsigned_long, epptr___ptr_to_struct_endpoint_C_' = epptr, depth___unsigned_long_' = depth, cte_b___ptr_to_struct_cte_C_' = cte_b, cte_a___ptr_to_struct_cte_C_' = cte_a, cptr2___unsigned_long_' = cptr2, cpacr___unsigned_long_' = cpacr, count___unsigned_' = count, cnode___struct_cap_C_' = cnode, chunk___int_' = chunk, cap_b___struct_cap_C_' = cap_b, cap_a___struct_cap_C_' = cap_a, block___unsigned_long_' = block, badge___unsigned_long_' = badge, bBase___unsigned_long_' = bBase, assoc___int_' = assoc, aifsr___unsigned_long_' = aifsr, adfsr___unsigned_long_' = adfsr, actlr___unsigned_long_' = actlr, aBase___unsigned_long_' = aBase, AIFSR___unsigned_long_' = AIFSR, ADFSR___unsigned_long_' = ADFSR, ACTLR___unsigned_long_' = ACTLR, wptr___ptr_to_unsigned_long_' = wptr, word___int_' = word, vtop___unsigned_long_' = vtop, vptr___unsigned_long_' = vptr, type___unsigned_long_' = type, tptr___ptr_to_struct_tcb_C_' = tptr, topB___unsigned_long_' = topB, topA___unsigned_long_' = topA, tcap___struct_cap_C_' = tcap, tCap___struct_cap_C_' = tCap, slot___ptr_to_struct_cte_C_' = slot, size___unsigned_' = size, size___unsigned_long_' = size___unsigned_long, sent___unsigned_long_' = sent, root___struct_cap_C_' = root, ptr2___ptr_to_struct_cte_C_' = ptr2, prrr___unsigned_long_' = prrr, prio___unsigned_long_' = prio, prev___ptr_to_struct_cte_C_' = prev, pptr___ptr_to_void_' = pptr, pptr___unsigned_long_' = pptr___unsigned_long, pool___ptr_to_struct_asid_pool_C_' = pool, phys___unsigned_long_' = phys, ntfn___ptr_to_struct_notification_C_' = ntfn, nmrr___unsigned_long_' = nmrr, next___ptr_to_struct_cte_C_' = next, next___ptr_to_struct_tcb_C_' = next___ptr_to_struct_tcb_C, mdb2___struct_mdb_node_C_' = mdb2, mdb1___struct_mdb_node_C_' = mdb1, mask___unsigned_long_' = mask, mask___unsigned_' = mask___unsigned, mask___unsigned_longlong_' = mask___unsigned_longlong, line___unsigned_long_' = line, info___struct_seL4_MessageInfo_C_' = info, ifsr___unsigned_long_' = ifsr, ifar___unsigned_long_' = ifar, idx2___unsigned_long_' = idx2, diff___int_' = diff, dfsr___unsigned_long_' = dfsr, dfar___unsigned_long_' = dfar, dest___ptr_to_struct_tcb_C_' = dest, dest___ptr_to_char_' = dest___ptr_to_char, data___unsigned_long_' = data, ctag___enum_cap_tag_' = ctag, cptr___unsigned_long_' = cptr, code___unsigned_' = code, clid___int_' = clid, cidr___unsigned_long_' = cidr, cap2___struct_cap_C_' = cap2, cap1___struct_cap_C_' = cap1, call___unsigned_long_' = call, cPtr___unsigned_long_' = cPtr, botB___unsigned_long_' = botB, botA___unsigned_long_' = botA, bits___unsigned_long_' = bits, bits___unsigned_' = bits___unsigned, base___unsigned_long_' = base, base___unsigned_' = base___unsigned, bTop___unsigned_long_' = bTop, auth___ptr_to_struct_tcb_C_' = auth, attr___struct_vm_attributes_C_' = attr, asid___unsigned_long_' = asid, arch___unsigned_long_' = arch, addr___unsigned_long_' = addr, addr___unsigned_' = addr___unsigned, aTop___unsigned_long_' = aTop, PRRR___unsigned_long_' = PRRR, NMRR___unsigned_long_' = NMRR, IFSR___unsigned_long_' = IFSR, IFAR___unsigned_long_' = IFAR, DFSR___unsigned_long_' = DFSR, DFAR___unsigned_long_' = DFAR, CLID___unsigned_long_' = CLID, CIDR___unsigned_long_' = CIDR, wsl___unsigned_long_' = wsl, w_b___unsigned_long_' = w_b, w_a___unsigned_long_' = w_a, val___unsigned_long_' = val, val___long_' = val___long, v32___unsigned_' = v32, tex___unsigned_long_' = tex, tcb___ptr_to_struct_tcb_C_' = tcb, tag___struct_seL4_MessageInfo_C_' = tag, str___ptr_to_char_' = str, src___ptr_to_struct_tcb_C_' = src, src___ptr_to_char_' = src___ptr_to_char, scr___unsigned_long_' = scr, ret___unsigned_' = ret, ret___unsigned_long_' = ret___unsigned_long, ret___struct_findPDForASID_ret_C_' = ret___struct_findPDForASID_ret_C, ret___struct_lookupPTSlot_ret_C_' = ret___struct_lookupPTSlot_ret_C, ret___struct_resolve_ret_C_' = ret___struct_resolve_ret_C, ret___struct_create_mappings_pte_return_C_' = ret___struct_create_mappings_pte_return_C, ret___struct_create_mappings_pde_return_C_' = ret___struct_create_mappings_pde_return_C, ret___struct_deriveCap_ret_C_' = ret___struct_deriveCap_ret_C, ret___struct_lookupCap_ret_C_' = ret___struct_lookupCap_ret_C, ret___struct_lookupCapAndSlot_ret_C_' = ret___struct_lookupCapAndSlot_ret_C, ret___struct_lookupSlot_raw_ret_C_' = ret___struct_lookupSlot_raw_ret_C, ret___struct_lookupSlot_ret_C_' = ret___struct_lookupSlot_ret_C, ret___struct_resolveAddressBits_ret_C_' = ret___struct_resolveAddressBits_ret_C, ret___struct_finaliseSlot_ret_C_' = ret___struct_finaliseSlot_ret_C, res___long_' = res, reg___unsigned_long_' = reg, reg___struct_region_C_' = reg___struct_region_C, reg___struct_p_region_C_' = reg___struct_p_region_C, ptr___unsigned_long_' = ptr, ptr___ptr_to_unsigned_long_' = ptr___ptr_to_unsigned_long, ptr___ptr_to_struct_cte_C_' = ptr___ptr_to_struct_cte_C, pte___struct_pte_C_' = pte, pte___ptr_to_struct_pte_C_' = pte___ptr_to_struct_pte_C, pde___struct_pde_C_' = pde, pde___ptr_to_struct_pde_C_' = pde___ptr_to_struct_pde_C, msb___unsigned_long_' = msb, mdb___struct_mdb_node_C_' = mdb, mcp___unsigned_long_' = mcp, max___unsigned_long_' = max, luf___struct_lookup_fault_C_' = luf, lou___int_' = lou, loc___int_' = loc, len___unsigned_long_' = len, irq___unsigned_long_' = irq, idx___unsigned_long_' = idx, ex1___struct_seL4_Fault_C_' = ex1, end___unsigned_long_' = end, dom___unsigned_long_' = dom, cte___ptr_to_struct_cte_C_' = cte, cpu___unsigned_long_' = cpu, cap___struct_cap_C_' = cap, bit___int_' = bit, aux___unsigned_' = aux, acr___unsigned_long_' = acr, TEX___unsigned_' = TEX, FSR___unsigned_' = FSR, FAR___unsigned_long_' = FAR, APX___unsigned_' = APX, ts___unsigned_long_' = ts, sz___unsigned_long_' = sz, s2___ptr_to_char_' = s2, s1___ptr_to_char_' = s1, pt___ptr_to_struct_pte_C_' = pt, pd___ptr_to_struct_pde_C_' = pd, pd___struct_cap_C_' = pd___struct_cap_C, pd___struct_findPDForASID_ret_C_' = pd___struct_findPDForASID_ret_C, pc___unsigned_long_' = pc, pa___unsigned_long_' = pa, nG___unsigned_' = nG, mi___struct_seL4_MessageInfo_C_' = mi, id___unsigned_long_' = id, id___anonymous_enum_' = id___anonymous_enum, ep___ptr_to_struct_endpoint_C_' = ep, ct___struct_cap_transfer_C_' = ct, bi___ptr_to_struct_seL4_BootInfo_C_' = bi, ap___ptr_to_struct_asid_pool_C_' = ap, ap___unsigned_long_' = ap___unsigned_long, XN___unsigned_' = XN, AP___unsigned_' = AP, y___unsigned_' = y, y___int_' = y___int, x___unsigned_' = x, x___unsigned_longlong_' = x___unsigned_longlong, x___unsigned_long_' = x___unsigned_long, x___int_' = x___int, w___unsigned_long_' = w, w___int_' = w___int, w___struct_seL4_CNode_CapData_C_' = w___struct_seL4_CNode_CapData_C, v___unsigned_long_' = va, v___int_' = v___int, v___unsigned_' = v___unsigned, t___unsigned_long_' = t, s___unsigned_long_' = s___unsigned_long, s___ptr_to_char_' = s___ptr_to_char, s___ptr_to_void_' = s, r___unsigned_long_' = r, r___ptr_to_struct_p_region_C_' = r___ptr_to_struct_p_region_C, r___ptr_to_struct_region_C_' = r___ptr_to_struct_region_C, q___ptr_to_unsigned_char_' = q, p___unsigned_long_' = p, p___ptr_to_unsigned_char_' = p___ptr_to_unsigned_char, n___unsigned_long_' = n, n___int_' = n___int, m___struct_region_C_' = m, l___int_' = l, j___unsigned_long_' = j, i___unsigned_long_' = i, i___unsigned_' = i___unsigned, i___int_' = i___int, f___unsigned_long_' = f, e___unsigned_long_' = e, c___unsigned_long_' = c, c___char_' = c___char, b___unsigned_long_' = b, a___unsigned_long_' = a, S___unsigned_' = S, P___unsigned_' = P, C___unsigned_' = C, B___unsigned_' = B, \<dots> = morea\<rparr> \<in> G' \<and> xf' (xfu' (\<lambda>_. v) \<lparr>globals = \<lparr>t_hrs_' = t_hrs, phantom_machine_state_' = phantom_machine_state, ghost'state_' = ghost'state, avail_reg_' = avail_reg, ksNumCPUs_' = ksNumCPUs, ndks_boot_' = ndks_boot, active_irq_' = active_irq, rootserver_' = rootserver, ksCurDomain_' = ksCurDomain, ksCurThread_' = ksCurThread, ksDomainTime_' = ksDomainTime, ksIdleThread_' = ksIdleThread, tlbLockCount_' = tlbLockCount, armKSNextASID_' = armKSNextASID, current_fault_' = current_fault, ksReadyQueues_' = ksReadyQueues, armKSASIDTable_' = armKSASIDTable, rootserver_mem_' = rootserver_mem, armKSHWASIDTable_' = armKSHWASIDTable, intStateIRQTable_' = intStateIRQTable, ksDomScheduleIdx_' = ksDomScheduleIdx, ksSchedulerAction_' = ksSchedulerAction, current_extra_caps_' = current_extra_caps, isFPUEnabledCached_' = isFPUEnabledCached, current_lookup_fault_' = current_lookup_fault, ksWorkUnitsCompleted_' = ksWorkUnitsCompleted, current_syscall_error_' = current_syscall_error, ksReadyQueuesL1Bitmap_' = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap_' = ksReadyQueuesL2Bitmap, \<dots> = more\<rparr>, global_exn_var_' = global_exn_var, ret__struct_create_frames_of_region_ret_C_' = ret__struct_create_frames_of_region_ret_C, ret__struct_create_mappings_pte_return_C_' = ret__struct_create_mappings_pte_return_C, ret__struct_create_mappings_pde_return_C_' = ret__struct_create_mappings_pde_return_C, ret__struct_resolveAddressBits_ret_C_' = ret__struct_resolveAddressBits_ret_C, ret__struct_lookupCapAndSlot_ret_C_' = ret__struct_lookupCapAndSlot_ret_C, ret__struct_lookupSlot_raw_ret_C_' = ret__struct_lookupSlot_raw_ret_C, ret__struct_findPDForASID_ret_C_' = ret__struct_findPDForASID_ret_C, ret__struct_seL4_MessageInfo_C_' = ret__struct_seL4_MessageInfo_C, ret__struct_lookupPTSlot_ret_C_' = ret__struct_lookupPTSlot_ret_C, ret__struct_finaliseSlot_ret_C_' = ret__struct_finaliseSlot_ret_C, ret__struct_seL4_SlotRegion_C_' = ret__struct_seL4_SlotRegion_C, ret__struct_finaliseCap_ret_C_' = ret__struct_finaliseCap_ret_C, ret__struct_seL4_CapRights_C_' = ret__struct_seL4_CapRights_C, ret__struct_lookupSlot_ret_C_' = ret__struct_lookupSlot_ret_C, ret__struct_vm_attributes_C_' = ret__struct_vm_attributes_C, ret__struct_lookupCap_ret_C_' = ret__struct_lookupCap_ret_C, ret__struct_deriveCap_ret_C_' = ret__struct_deriveCap_ret_C, ret__struct_lookup_fault_C_' = ret__struct_lookup_fault_C, ret__struct_cap_transfer_C_' = ret__struct_cap_transfer_C, ret__struct_resolve_ret_C_' = ret__struct_resolve_ret_C, ret__ptr_to_unsigned_long_' = ret__ptr_to_unsigned_long, ret__struct_seL4_Fault_C_' = ret__struct_seL4_Fault_C, ret__ptr_to_struct_tcb_C_' = ret__ptr_to_struct_tcb_C, ret__ptr_to_struct_pte_C_' = ret__ptr_to_struct_pte_C, ret__ptr_to_struct_pde_C_' = ret__ptr_to_struct_pde_C, ret__ptr_to_struct_cte_C_' = ret__ptr_to_struct_cte_C, ret__struct_tcb_queue_C_' = ret__struct_tcb_queue_C, ret__struct_p_region_C_' = ret__struct_p_region_C, ret__struct_mdb_node_C_' = ret__struct_mdb_node_C, original_lookup_fault___struct_lookup_fault_C_' = original_lookup_fault, unsigned_long_eret_4_' = unsigned_long_eret_4, unsigned_long_eret_3_' = unsigned_long_eret_3, unsigned_long_eret_2_' = unsigned_long_eret_2, ret__struct_region_C_' = ret__struct_region_C, struct_cap_C_eret_3_' = struct_cap_C_eret_3, struct_cap_C_eret_2_' = struct_cap_C_eret_2, extra_bi_frame_vptr___unsigned_long_' = extra_bi_frame_vptr, seL4_CNode_CapData___struct_seL4_CNode_CapData_C_' = seL4_CNode_CapData, ret__unsigned_long_' = ret__unsigned_long, ret__unsigned_char_' = ret__unsigned_char, ptr_to_void_eret_2_' = ptr_to_void_eret_2, first_untyped_slot___unsigned_long_' = first_untyped_slot, extra_bi_size_bits___unsigned_long_' = extra_bi_size_bits, capPTMappedAddress___unsigned_' = capPTMappedAddress, capFMappedASIDHigh___unsigned_' = capFMappedASIDHigh, boot_mem_reuse_reg___struct_region_C_' = boot_mem_reuse_reg, tlbflush_required___unsigned_long_' = tlbflush_required, stored_asid_valid___unsigned_' = stored_asid_valid, ret__struct_pte_C_' = ret__struct_pte_C, ret__struct_pde_C_' = ret__struct_pde_C, ret__struct_cap_C_' = ret__struct_cap_C, receiverIPCBuffer___ptr_to_unsigned_long_' = receiverIPCBuffer, newCapIsRevocable___unsigned_long_' = newCapIsRevocable, create_frames_ret___struct_create_frames_of_region_ret_C_' = create_frames_ret, capNtfnCanReceive___unsigned_' = capNtfnCanReceive, capFMappedAddress___unsigned_' = capFMappedAddress, capFMappedASIDLow___unsigned_' = capFMappedASIDLow, capCNodeGuardSize___unsigned_' = capCNodeGuardSize, untypedFreeBytes___unsigned_long_' = untypedFreeBytes, thread_state_ptr___ptr_to_struct_thread_state_C_' = thread_state_ptr, size_unique_name___unsigned_long_' = size_unique_name, seL4_MessageInfo___struct_seL4_MessageInfo_C_' = seL4_MessageInfo, scheduler_action___ptr_to_struct_tcb_C_' = scheduler_action, ret__ptr_to_void_' = ret__ptr_to_void, receiveIPCBuffer___ptr_to_unsigned_long_' = receiveIPCBuffer, prevIsSameObject___unsigned_long_' = prevIsSameObject, notification_ptr___ptr_to_struct_notification_C_' = notification_ptr, l1index_inverted___unsigned_long_' = l1index_inverted, instructionFault___unsigned_' = instructionFault, capReplyCanGrant___unsigned_' = capReplyCanGrant, capReplyCanGrant___unsigned_long_' = capReplyCanGrant___unsigned_long, capCanGrantReply___unsigned_' = capCanGrantReply, armParityEnabled___unsigned_' = armParityEnabled, armPageCacheable___unsigned_' = armPageCacheable, unsigned_eret_6_' = unsigned_eret_6, unsigned_eret_5_' = unsigned_eret_5, unsigned_eret_4_' = unsigned_eret_4, unsigned_eret_3_' = unsigned_eret_3, unsigned_eret_2_' = unsigned_eret_2, unaligned_start___unsigned_long_' = unaligned_start, transferInteger___unsigned_long_' = transferInteger, totalObjectSize___unsigned_long_' = totalObjectSize, slot_pos_before___unsigned_long_' = slot_pos_before, extra_bi_region___struct_region_C_' = extra_bi_region, extra_bi_offset___unsigned_long_' = extra_bi_offset, cnode_size_bits___unsigned_long_' = cnode_size_bits, cap_rights_mask___struct_seL4_CapRights_C_' = cap_rights_mask, capPTMappedASID___unsigned_' = capPTMappedASID, capPDMappedASID___unsigned_' = capPDMappedASID, armExecuteNever___unsigned_' = armExecuteNever, ui_p_reg_start___unsigned_long_' = ui_p_reg_start, stored_hw_asid___unsigned_' = stored_hw_asid, stored_hw_asid___struct_pde_C_' = stored_hw_asid___struct_pde_C, slot_pos_after___unsigned_long_' = slot_pos_after, seL4_CapRights___struct_seL4_CapRights_C_' = seL4_CapRights, root_cnode_cap___struct_cap_C_' = root_cnode_cap, msgTransferred___unsigned_long_' = msgTransferred, mdbFirstBadged___unsigned_' = mdbFirstBadged, mdbFirstBadged___unsigned_long_' = mdbFirstBadged___unsigned_long, inReceivePhase___unsigned_' = inReceivePhase, hw_asid_offset___unsigned_long_' = hw_asid_offset, currentPDEType___enum_pde_tag_' = currentPDEType, cptr_bufferPtr___unsigned_long_' = cptr_bufferPtr, capReplyMaster___unsigned_' = capReplyMaster, capReplyMaster___unsigned_long_' = capReplyMaster___unsigned_long, capNtfnCanSend___unsigned_' = capNtfnCanSend, alignedFreeRef___unsigned_long_' = alignedFreeRef, vm_attributes___struct_vm_attributes_C_' = vm_attributes, vRoot_srcSlot___ptr_to_struct_cte_C_' = vRoot_srcSlot, transferFrame___unsigned_long_' = transferFrame, syscallNumber___unsigned_' = syscallNumber, suspendSource___unsigned_long_' = suspendSource, stack_address___unsigned_long_' = stack_address, root_switched___unsigned_long_' = root_switched, ret__unsigned_' = ret__unsigned, ret__longlong_' = ret__longlong, replyCanGrant___unsigned_long_' = replyCanGrant, receiveBuffer___ptr_to_void_' = receiveBuffer___ptr_to_void, receiveBuffer___ptr_to_unsigned_long_' = receiveBuffer, nonexecutable___unsigned_long_' = nonexecutable, mva_plus_asid___unsigned_long_' = mva_plus_asid, fpsid_subarch___unsigned_long_' = fpsid_subarch, extra_bi_size___unsigned_long_' = extra_bi_size, dtb_phys_addr___unsigned_long_' = dtb_phys_addr, device_memory___unsigned_long_' = device_memory, cmp_size_bits___unsigned_long_' = cmp_size_bits, capsUnwrapped___unsigned_' = capsUnwrapped, capZombieType___unsigned_' = capZombieType, capPTIsMapped___unsigned_' = capPTIsMapped, capPDIsMapped___unsigned_' = capPDIsMapped, capCanReceive___unsigned_' = capCanReceive, capCNodeRadix___unsigned_' = capCNodeRadix, capCNodeGuard___unsigned_' = capCNodeGuard, canGrantReply___unsigned_long_' = canGrantReply, cRoot_srcSlot___ptr_to_struct_cte_C_' = cRoot_srcSlot, bufferSrcSlot___ptr_to_struct_cte_C_' = bufferSrcSlot, bi_frame_vptr___unsigned_long_' = bi_frame_vptr, was_runnable___unsigned_long_' = was_runnable, w_rightsMask___unsigned_long_' = w_rightsMask, vm_faultType___unsigned_long_' = vm_faultType, vRoot_newCap___struct_cap_C_' = vRoot_newCap, ui_p_reg_end___unsigned_long_' = ui_p_reg_end, transferArch___unsigned_long_' = transferArch, thread_state___struct_thread_state_C_' = thread_state, resumeTarget___unsigned_long_' = resumeTarget, processor_id___unsigned_long_' = processor_id, pivotNewData___unsigned_long_' = pivotNewData, nextFreeArea___ptr_to_void_' = nextFreeArea, mdb_node_ptr___ptr_to_struct_mdb_node_C_' = mdb_node_ptr, mdbRevocable___unsigned_' = mdbRevocable, mdbRevocable___unsigned_long_' = mdbRevocable___unsigned_long, lookup_fault___struct_lookup_fault_C_' = lookup_fault, extra_bi_ret___struct_create_frames_of_region_ret_C_' = extra_bi_ret, epQueue_tail___unsigned_long_' = epQueue_tail, epQueue_head___unsigned_long_' = epQueue_head, endpoint_ptr___ptr_to_struct_endpoint_C_' = endpoint_ptr, endpointTail___ptr_to_struct_tcb_C_' = endpointTail, dtb_phys_end___unsigned_long_' = dtb_phys_end, deviceMemory___unsigned_long_' = deviceMemory, cap_type_tag___unsigned_' = cap_type_tag, capPTBasePtr___unsigned_' = capPTBasePtr, capPDBasePtr___unsigned_' = capPDBasePtr, capNtfnBadge___unsigned_' = capNtfnBadge, capFreeIndex___unsigned_' = capFreeIndex, capFVMRights___unsigned_' = capFVMRights, capFIsDevice___unsigned_' = capFIsDevice, capBlockSize___unsigned_' = capBlockSize, cRoot_newCap___struct_cap_C_' = cRoot_newCap, w_bufferPtr___unsigned_long_' = w_bufferPtr, userObjSize___unsigned_long_' = userObjSize, updateFlags___unsigned_long_' = updateFlags, resolve_ret___struct_resolve_ret_C_' = resolve_ret, pte_entries___struct_pte_range_C_' = pte_entries, pde_entries___struct_pde_range_C_' = pde_entries, new_hw_asid___unsigned_char_' = new_hw_asid, newPivotCap___struct_cap_C_' = newPivotCap, n_available___unsigned_long_' = n_available, ipcbuf_vptr___unsigned_long_' = ipcbuf_vptr, instruction___unsigned_long_' = instruction, handlerSlot___ptr_to_struct_cte_C_' = handlerSlot, handlerCPtr___unsigned_long_' = handlerCPtr, empty_index___int_' = empty_index, controlSlot___ptr_to_struct_cte_C_' = controlSlot, cleanupInfo___struct_cap_C_' = cleanupInfo, capZombieID___unsigned_' = capZombieID, capVMRights___unsigned_long_' = capVMRights, capIsDevice___unsigned_' = capIsDevice, capFBasePtr___unsigned_' = capFBasePtr, capFBasePtr___unsigned_long_' = capFBasePtr___unsigned_long, capCanGrant___unsigned_' = capCanGrant, capCNodePtr___unsigned_' = capCNodePtr, capASIDPool___unsigned_' = capASIDPool, capASIDBase___unsigned_' = capASIDBase, ui_v_entry___unsigned_long_' = ui_v_entry, threadRoot___struct_cap_C_' = threadRoot, targetSlot___ptr_to_struct_pte_C_' = targetSlot, targetSlot___ptr_to_struct_pde_C_' = targetSlot___ptr_to_struct_pde_C, srcNewData___unsigned_long_' = srcNewData, source_cap___struct_cap_C_' = source_cap, sendBuffer___ptr_to_void_' = sendBuffer___ptr_to_void, sendBuffer___ptr_to_unsigned_long_' = sendBuffer, seL4_Fault___struct_seL4_Fault_C_' = seL4_Fault, retypeBase___ptr_to_void_' = retypeBase, regionBase___ptr_to_void_' = regionBase, pivotIndex___unsigned_long_' = pivotIndex, pivotDepth___unsigned_long_' = pivotDepth, parentSlot___ptr_to_struct_cte_C_' = parentSlot, objectSize___unsigned_long_' = objectSize, ntfn_queue___struct_tcb_queue_C_' = ntfn_queue, nodeWindow___unsigned_long_' = nodeWindow, nodeOffset___unsigned_long_' = nodeOffset, n_reserved___unsigned_long_' = n_reserved, isReceiver___unsigned_long_' = isReceiver, isBlocking___unsigned_long_' = isBlocking, ipcbuf_cap___struct_cap_C_' = ipcbuf_cap, ipc_buffer___ptr_to_unsigned_long_' = ipc_buffer, int_eret_3_' = int_eret_3, int_eret_2_' = int_eret_2, handlerCap___struct_cap_C_' = handlerCap, guardFound___unsigned_' = guardFound, fault_type___unsigned_long_' = fault_type, extra_size___unsigned_long_' = extra_size, executable___unsigned_long_' = executable, dtb_addr_p___unsigned_long_' = dtb_addr_p, destOffset___unsigned_long_' = destOffset, destLength___unsigned_long_' = destLength, derivedCap___struct_cap_C_' = derivedCap, cur_thread___ptr_to_struct_tcb_C_' = cur_thread, csselr_old___unsigned_long_' = csselr_old, cap_rights___struct_seL4_CapRights_C_' = cap_rights, capNtfnPtr___unsigned_' = capNtfnPtr, capEPBadge___unsigned_' = capEPBadge, capCanSend___unsigned_' = capCanSend, callerSlot___ptr_to_struct_cte_C_' = callerSlot, bufferSlot___ptr_to_struct_cte_C_' = bufferSlot, bufferAddr___unsigned_long_' = bufferAddr, block_size___unsigned_long_' = block_size, attributes___struct_vm_attributes_C_' = attributes, assoc_bits___int_' = assoc_bits, align_bits___unsigned_' = align_bits, StrictC'_v___unsigned_long_' = StrictC'_v, vm_rights___unsigned_long_' = vm_rights, vbase_ptr___ptr_to_void_' = vbase_ptr, vRootSlot___ptr_to_struct_cte_C_' = vRootSlot, vRootData___unsigned_long_' = vRootData, use_large___unsigned_long_' = use_large, threadPtr___ptr_to_struct_tcb_C_' = threadPtr, stack_top___unsigned_long_' = stack_top, size_bits___unsigned_long_' = size_bits, size_bits___unsigned_' = size_bits___unsigned, ret__long_' = ret__long, replySlot___ptr_to_struct_cte_C_' = replySlot, radixBits___unsigned_long_' = radixBits, pv_offset___long_' = pv_offset, pivotSlot___ptr_to_struct_cte_C_' = pivotSlot, pivotRoot___struct_cap_C_' = pivotRoot, pdCapSlot___ptr_to_struct_cte_C_' = pdCapSlot, page_size___unsigned_long_' = page_size, page_base___unsigned_long_' = page_base, num_nodes___unsigned_long_' = num_nodes, nodeIndex___unsigned_long_' = nodeIndex, nodeDepth___unsigned_long_' = nodeDepth, newVTable___struct_cap_C_' = newVTable, newSrcCap___struct_cap_C_' = newSrcCap, masterCap___struct_cap_C_' = masterCap, levelBits___unsigned_long_' = levelBits, it_pd_cap___struct_cap_C_' = it_pd_cap, it_ap_cap___struct_cap_C_' = it_ap_cap, ipcBuffer___ptr_to_unsigned_long_' = ipcBuffer, immediate___unsigned_long_' = immediate, haveHWFPU___unsigned_long_' = haveHWFPU, guardSize___unsigned_long_' = guardSize, guardBits___unsigned_long_' = guardBits, global_pd___ptr_to_struct_pde_C_' = global_pd, freeIndex___unsigned_long_' = freeIndex, frame_cap___struct_cap_C_' = frame_cap, frameSize___unsigned_long_' = frameSize, faultType___unsigned_long_' = faultType, extraCaps___unsigned_' = extraCaps, dtb_p_reg___struct_p_region_C_' = dtb_p_reg, destCNode___ptr_to_struct_cte_C_' = destCNode, capTCBPtr___unsigned_' = capTCBPtr, capTCBPtr___unsigned_long_' = capTCBPtr___unsigned_long, candidate___ptr_to_struct_tcb_C_' = candidate, callerCap___struct_cap_C_' = callerCap, callerCap___ptr_to_struct_cte_C_' = callerCap___ptr_to_struct_cte_C, cacheable___unsigned_long_' = cacheable, cRootSlot___ptr_to_struct_cte_C_' = cRootSlot, cRootData___unsigned_long_' = cRootData, bufferPtr___ptr_to_unsigned_long_' = bufferPtr, bufferCap___struct_cap_C_' = bufferCap, bitsFound___unsigned_' = bitsFound, base_addr___unsigned_long_' = base_addr, baseValue___unsigned_long_' = baseValue, available___ptr_to_struct_p_region_C_' = available, asid_base___unsigned_long_' = asid_base, allocated___unsigned_long_' = allocated, alignment___unsigned_long_' = alignment, vmRights___unsigned_long_' = vmRights, vRootCap___struct_cap_C_' = vRootCap, userSize___unsigned_long_' = userSize, ui_v_reg___struct_v_region_C_' = ui_v_reg, ui_p_reg___struct_p_region_C_' = ui_p_reg, transfer___struct_cap_transfer_C_' = transfer, tls_base___unsigned_long_' = tls_base, tcb_dest___ptr_to_struct_tcb_C_' = tcb_dest, srcIndex___unsigned_long_' = srcIndex, srcDepth___unsigned_long_' = srcDepth, slot_ptr___ptr_to_struct_cte_C_' = slot_ptr, rootSlot___ptr_to_struct_cte_C_' = rootSlot, ret__int_' = ret__int, reserved___unsigned_' = reserved, reserved___ptr_to_struct_region_C_' = reserved___ptr_to_struct_region_C, receiver___ptr_to_struct_tcb_C_' = receiver, priority___unsigned_long_' = priority, prev_ptr___unsigned_long_' = prev_ptr, prev_cap___struct_cap_C_' = prev_cap, preserve___unsigned_long_' = preserve, prefetch___unsigned_' = prefetch, pagesize___unsigned_long_' = pagesize, pageBits___unsigned_' = pageBits, ntfn_cap___struct_cap_C_' = ntfn_cap, node_ptr___ptr_to_struct_mdb_node_C_' = node_ptr, nodeSize___unsigned_long_' = nodeSize, next_ptr___unsigned_long_' = next_ptr, mdb_node___struct_mdb_node_C_' = mdb_node, it_v_reg___struct_v_region_C_' = it_v_reg, isSource___unsigned_long_' = isSource, irqState___unsigned_long_' = irqState, inverted___unsigned_long_' = inverted, invLabel___unsigned_long_' = invLabel, invLabel___int_' = invLabel___int, find_ret___struct_findPDForASID_ret_C_' = find_ret, fastfail___unsigned_long_' = fastfail, endpoint___ptr_to_struct_endpoint_C_' = endpoint, dtb_size___unsigned_long_' = dtb_size___unsigned_long, dtb_size___unsigned_' = dtb_size, destSlot___ptr_to_struct_cte_C_' = destSlot, data_ram___unsigned_' = data_ram, cnodeCap___struct_cap_C_' = cnodeCap, clzl_ret___unsigned_long_' = clzl_ret, cap_type___unsigned_long_' = cap_type, capIndex___unsigned_long_' = capIndex, capGuard___unsigned_long_' = capGuard, capFSize___unsigned_' = capFSize, capEPPtr___unsigned_' = capEPPtr, canGrant___unsigned_long_' = canGrant, cRootCap___struct_cap_C_' = cRootCap, boundTCB___ptr_to_struct_tcb_C_' = boundTCB, blocking___unsigned_long_' = blocking, bitsLeft___unsigned_' = bitsLeft, asidPool___ptr_to_struct_asid_pool_C_' = asidPool, archInfo___unsigned_long_' = archInfo, v_entry___unsigned_long_' = v_entry, untyped___struct_cap_C_' = untyped, trigger___unsigned_long_' = trigger, tcb_src___ptr_to_struct_tcb_C_' = tcb_src, tag_ram___unsigned_' = tag_ram, syscall___unsigned_long_' = syscall, srcSlot___ptr_to_struct_cte_C_' = srcSlot, srcRoot___struct_cap_C_' = srcRoot, sendBuf___ptr_to_unsigned_long_' = sendBuf, rootCap___struct_cap_C_' = rootCap, restart___unsigned_long_' = restart, res_ret___struct_resolveAddressBits_ret_C_' = res_ret, recvBuf___ptr_to_unsigned_long_' = recvBuf, ptr_src___ptr_to_void_' = ptr_src, ptr_dst___ptr_to_void_' = ptr_dst, pte_ptr___ptr_to_struct_pte_C_' = pte_ptr, pt_vptr___unsigned_long_' = pt_vptr, ptIndex___unsigned_' = ptIndex, poolPtr___ptr_to_struct_asid_pool_C_' = poolPtr, pde_ptr___ptr_to_struct_pde_C_' = pde_ptr, pdIndex___unsigned_' = pdIndex, pdIndex___unsigned_long_' = pdIndex___unsigned_long, ntfnPtr___ptr_to_struct_notification_C_' = ntfnPtr, ntfnCap___struct_cap_C_' = ntfnCap, node_id___unsigned_long_' = node_id, nodeCap___struct_cap_C_' = nodeCap, nextPtr___ptr_to_struct_cte_C_' = nextPtr, new_cap___struct_cap_C_' = new_cap, newType___unsigned_long_' = newType, newPrio___unsigned_long_' = newPrio, newData___unsigned_long_' = newData, msgInfo___unsigned_long_' = msgInfo, msgInfo___struct_seL4_MessageInfo_C_' = msgInfo___struct_seL4_MessageInfo_C, mdbPrev___unsigned_' = mdbPrev, mdbPrev___unsigned_long_' = mdbPrev___unsigned_long, mdbNode___struct_mdb_node_C_' = mdbNode, mdbNext___unsigned_' = mdbNext, mdbNext___unsigned_long_' = mdbNext___unsigned_long, map_ret___struct_create_mappings_pte_return_C_' = map_ret, map_ret___struct_create_mappings_pde_return_C_' = map_ret___struct_create_mappings_pde_return_C, lus_ret___struct_lookupSlot_ret_C_' = lus_ret, lufType___unsigned_long_' = lufType, luc_ret___struct_lookupCap_ret_C_' = luc_ret, l2index___unsigned_long_' = l2index, l1index___unsigned_long_' = l1index, irqSlot___ptr_to_struct_cte_C_' = irqSlot, initial___ptr_to_struct_tcb_C_' = initial, hw_asid___unsigned_char_' = hw_asid, freeRef___unsigned_long_' = freeRef, faultep___unsigned_long_' = faultep, faultEP___unsigned_long_' = faultEP, exposed___unsigned_long_' = exposed, endSlot___ptr_to_struct_cte_C_' = endSlot, do_call___unsigned_long_' = do_call, disable___unsigned_long_' = disable, destCap___struct_cap_C_' = destCap, cte_ptr___ptr_to_struct_cte_C_' = cte_ptr, context___ptr_to_struct_user_context_C_' = context, cap_ptr___ptr_to_struct_cap_C_' = cap_ptr, capData___unsigned_long_' = capData, basePtr___unsigned_long_' = basePtr, authTCB___ptr_to_struct_tcb_C_' = authTCB, authCap___struct_cap_C_' = authCap, address___unsigned_' = address, z_slot___ptr_to_struct_cte_C_' = z_slot, w_bits___unsigned_long_' = w_bits, ut_cap___struct_cap_C_' = ut_cap, ui_reg___struct_region_C_' = ui_reg, ts_ptr___ptr_to_struct_thread_state_C_' = ts_ptr, tsType___unsigned_long_' = tsType, thread___ptr_to_struct_tcb_C_' = thread, tcbptr___ptr_to_struct_tcb_C_' = tcbptr, target___unsigned_' = target___unsigned, target___unsigned_char_' = target___unsigned_char, target___ptr_to_struct_tcb_C_' = target, status___unsigned_long_' = status, srcTCB___ptr_to_struct_tcb_C_' = srcTCB, srcMDB___struct_mdb_node_C_' = srcMDB, srcCap___struct_cap_C_' = srcCap, sender___ptr_to_struct_tcb_C_' = sender, result___unsigned_long_' = result, pt_cap___struct_cap_C_' = pt_cap, ptSlot___ptr_to_struct_pte_C_' = ptSlot, pstart___unsigned_long_' = pstart, pd_val___unsigned_long_' = pd_val, pd_cap___struct_cap_C_' = pd_cap, pdSlot___ptr_to_struct_pde_C_' = pdSlot, parity___unsigned_long_' = parity, parent___ptr_to_struct_cte_C_' = parent, offset___unsigned_' = offset, offset___unsigned_long_' = offset___unsigned_long, offset___int_' = offset___int, number___unsigned_' = number, number___unsigned_long_' = number___unsigned_long, newMcp___unsigned_long_' = newMcp, newMDB___struct_mdb_node_C_' = newMDB, newCap___struct_cap_C_' = newCap, n_bits___unsigned_long_' = n_bits, maxlen___unsigned_long_' = maxlen, lu_ret___struct_lookupCapAndSlot_ret_C_' = lu_ret, lu_ret___struct_lookupCap_ret_C_' = lu_ret___struct_lookupCap_ret_C, lu_ret___struct_lookupPTSlot_ret_C_' = lu_ret___struct_lookupPTSlot_ret_C, lu_ret___struct_lookupSlot_ret_C_' = lu_ret___struct_lookupSlot_ret_C, lu_ret___struct_lookupSlot_raw_ret_C_' = lu_ret___struct_lookupSlot_raw_ret_C, length___unsigned_' = length, length___unsigned_long_' = length___unsigned_long, isMove___unsigned_long_' = isMove, isCall___unsigned_long_' = isCall, htpidr___unsigned_long_' = htpidr, header___struct_seL4_BootInfoHeader_C_' = header, fs_ret___struct_finaliseSlot_ret_C_' = fs_ret, fc_ret___struct_finaliseCap_ret_C_' = fc_ret, ep_ref___unsigned_long_' = ep_ref, ep_ptr___ptr_to_struct_endpoint_C_' = ep_ptr, ep_cap___struct_cap_C_' = ep_cap, epCPtr___unsigned_long_' = epCPtr, domain___unsigned_long_' = domain, do_map___unsigned_long_' = do_map, dc_ret___struct_deriveCap_ret_C_' = dc_ret, ctSlot___ptr_to_struct_cte_C_' = ctSlot, capptr___unsigned_long_' = capptr, cap_pd___ptr_to_struct_pde_C_' = cap_pd, capPtr___unsigned_' = capPtr, capIRQ___unsigned_' = capIRQ, caller___ptr_to_struct_tcb_C_' = caller, buffer___ptr_to_unsigned_long_' = buffer, badge2___unsigned_long_' = badge2, ap_cap___struct_cap_C_' = ap_cap, Domain___unsigned_' = Domain, vaddr___unsigned_long_' = vaddr, v_reg___struct_v_region_C_' = v_reg, state___unsigned_long_' = state, state___ptr_to_struct_thread_state_C_' = state___ptr_to_struct_thread_state_C, start___unsigned_long_' = start, slot3___ptr_to_struct_cte_C_' = slot3, slot2___ptr_to_struct_cte_C_' = slot2, slot1___ptr_to_struct_cte_C_' = slot1, size2___unsigned_long_' = size2, reset___unsigned_long_' = reset, radix___unsigned_long_' = radix, queue___struct_tcb_queue_C_' = queue, pdCap___struct_cap_C_' = pdCap, paddr___unsigned_long_' = paddr, p_reg___struct_p_region_C_' = p_reg, nsets___int_' = nsets, nirqs___int_' = nirqs, newPD___ptr_to_struct_pde_C_' = newPD, level___int_' = level, lbits___int_' = lbits, label___unsigned_' = label, label___unsigned_long_' = label___unsigned_long, irq_w___unsigned_long_' = irq_w, index___unsigned_long_' = index, index___int_' = index___int, guard___unsigned_long_' = guard, grant___unsigned_long_' = grant, frame___ptr_to_void_' = frame, frame___ptr_to_struct_kernel_frame_C_' = frame___ptr_to_struct_kernel_frame_C, fpsid___unsigned_long_' = fpsid, fpexc___unsigned_long_' = fpexc, flags___unsigned_long_' = flags, final___unsigned_long_' = final, fault___struct_seL4_Fault_C_' = fault, fault___unsigned_long_' = fault___unsigned_long, epptr___ptr_to_struct_endpoint_C_' = epptr, depth___unsigned_long_' = depth, cte_b___ptr_to_struct_cte_C_' = cte_b, cte_a___ptr_to_struct_cte_C_' = cte_a, cptr2___unsigned_long_' = cptr2, cpacr___unsigned_long_' = cpacr, count___unsigned_' = count, cnode___struct_cap_C_' = cnode, chunk___int_' = chunk, cap_b___struct_cap_C_' = cap_b, cap_a___struct_cap_C_' = cap_a, block___unsigned_long_' = block, badge___unsigned_long_' = badge, bBase___unsigned_long_' = bBase, assoc___int_' = assoc, aifsr___unsigned_long_' = aifsr, adfsr___unsigned_long_' = adfsr, actlr___unsigned_long_' = actlr, aBase___unsigned_long_' = aBase, AIFSR___unsigned_long_' = AIFSR, ADFSR___unsigned_long_' = ADFSR, ACTLR___unsigned_long_' = ACTLR, wptr___ptr_to_unsigned_long_' = wptr, word___int_' = word, vtop___unsigned_long_' = vtop, vptr___unsigned_long_' = vptr, type___unsigned_long_' = type, tptr___ptr_to_struct_tcb_C_' = tptr, topB___unsigned_long_' = topB, topA___unsigned_long_' = topA, tcap___struct_cap_C_' = tcap, tCap___struct_cap_C_' = tCap, slot___ptr_to_struct_cte_C_' = slot, size___unsigned_' = size, size___unsigned_long_' = size___unsigned_long, sent___unsigned_long_' = sent, root___struct_cap_C_' = root, ptr2___ptr_to_struct_cte_C_' = ptr2, prrr___unsigned_long_' = prrr, prio___unsigned_long_' = prio, prev___ptr_to_struct_cte_C_' = prev, pptr___ptr_to_void_' = pptr, pptr___unsigned_long_' = pptr___unsigned_long, pool___ptr_to_struct_asid_pool_C_' = pool, phys___unsigned_long_' = phys, ntfn___ptr_to_struct_notification_C_' = ntfn, nmrr___unsigned_long_' = nmrr, next___ptr_to_struct_cte_C_' = next, next___ptr_to_struct_tcb_C_' = next___ptr_to_struct_tcb_C, mdb2___struct_mdb_node_C_' = mdb2, mdb1___struct_mdb_node_C_' = mdb1, mask___unsigned_long_' = mask, mask___unsigned_' = mask___unsigned, mask___unsigned_longlong_' = mask___unsigned_longlong, line___unsigned_long_' = line, info___struct_seL4_MessageInfo_C_' = info, ifsr___unsigned_long_' = ifsr, ifar___unsigned_long_' = ifar, idx2___unsigned_long_' = idx2, diff___int_' = diff, dfsr___unsigned_long_' = dfsr, dfar___unsigned_long_' = dfar, dest___ptr_to_struct_tcb_C_' = dest, dest___ptr_to_char_' = dest___ptr_to_char, data___unsigned_long_' = data, ctag___enum_cap_tag_' = ctag, cptr___unsigned_long_' = cptr, code___unsigned_' = code, clid___int_' = clid, cidr___unsigned_long_' = cidr, cap2___struct_cap_C_' = cap2, cap1___struct_cap_C_' = cap1, call___unsigned_long_' = call, cPtr___unsigned_long_' = cPtr, botB___unsigned_long_' = botB, botA___unsigned_long_' = botA, bits___unsigned_long_' = bits, bits___unsigned_' = bits___unsigned, base___unsigned_long_' = base, base___unsigned_' = base___unsigned, bTop___unsigned_long_' = bTop, auth___ptr_to_struct_tcb_C_' = auth, attr___struct_vm_attributes_C_' = attr, asid___unsigned_long_' = asid, arch___unsigned_long_' = arch, addr___unsigned_long_' = addr, addr___unsigned_' = addr___unsigned, aTop___unsigned_long_' = aTop, PRRR___unsigned_long_' = PRRR, NMRR___unsigned_long_' = NMRR, IFSR___unsigned_long_' = IFSR, IFAR___unsigned_long_' = IFAR, DFSR___unsigned_long_' = DFSR, DFAR___unsigned_long_' = DFAR, CLID___unsigned_long_' = CLID, CIDR___unsigned_long_' = CIDR, wsl___unsigned_long_' = wsl, w_b___unsigned_long_' = w_b, w_a___unsigned_long_' = w_a, val___unsigned_long_' = val, val___long_' = val___long, v32___unsigned_' = v32, tex___unsigned_long_' = tex, tcb___ptr_to_struct_tcb_C_' = tcb, tag___struct_seL4_MessageInfo_C_' = tag, str___ptr_to_char_' = str, src___ptr_to_struct_tcb_C_' = src, src___ptr_to_char_' = src___ptr_to_char, scr___unsigned_long_' = scr, ret___unsigned_' = ret, ret___unsigned_long_' = ret___unsigned_long, ret___struct_findPDForASID_ret_C_' = ret___struct_findPDForASID_ret_C, ret___struct_lookupPTSlot_ret_C_' = ret___struct_lookupPTSlot_ret_C, ret___struct_resolve_ret_C_' = ret___struct_resolve_ret_C, ret___struct_create_mappings_pte_return_C_' = ret___struct_create_mappings_pte_return_C, ret___struct_create_mappings_pde_return_C_' = ret___struct_create_mappings_pde_return_C, ret___struct_deriveCap_ret_C_' = ret___struct_deriveCap_ret_C, ret___struct_lookupCap_ret_C_' = ret___struct_lookupCap_ret_C, ret___struct_lookupCapAndSlot_ret_C_' = ret___struct_lookupCapAndSlot_ret_C, ret___struct_lookupSlot_raw_ret_C_' = ret___struct_lookupSlot_raw_ret_C, ret___struct_lookupSlot_ret_C_' = ret___struct_lookupSlot_ret_C, ret___struct_resolveAddressBits_ret_C_' = ret___struct_resolveAddressBits_ret_C, ret___struct_finaliseSlot_ret_C_' = ret___struct_finaliseSlot_ret_C, res___long_' = res, reg___unsigned_long_' = reg, reg___struct_region_C_' = reg___struct_region_C, reg___struct_p_region_C_' = reg___struct_p_region_C, ptr___unsigned_long_' = ptr, ptr___ptr_to_unsigned_long_' = ptr___ptr_to_unsigned_long, ptr___ptr_to_struct_cte_C_' = ptr___ptr_to_struct_cte_C, pte___struct_pte_C_' = pte, pte___ptr_to_struct_pte_C_' = pte___ptr_to_struct_pte_C, pde___struct_pde_C_' = pde, pde___ptr_to_struct_pde_C_' = pde___ptr_to_struct_pde_C, msb___unsigned_long_' = msb, mdb___struct_mdb_node_C_' = mdb, mcp___unsigned_long_' = mcp, max___unsigned_long_' = max, luf___struct_lookup_fault_C_' = luf, lou___int_' = lou, loc___int_' = loc, len___unsigned_long_' = len, irq___unsigned_long_' = irq, idx___unsigned_long_' = idx, ex1___struct_seL4_Fault_C_' = ex1, end___unsigned_long_' = end, dom___unsigned_long_' = dom, cte___ptr_to_struct_cte_C_' = cte, cpu___unsigned_long_' = cpu, cap___struct_cap_C_' = cap, bit___int_' = bit, aux___unsigned_' = aux, acr___unsigned_long_' = acr, TEX___unsigned_' = TEX, FSR___unsigned_' = FSR, FAR___unsigned_long_' = FAR, APX___unsigned_' = APX, ts___unsigned_long_' = ts, sz___unsigned_long_' = sz, s2___ptr_to_char_' = s2, s1___ptr_to_char_' = s1, pt___ptr_to_struct_pte_C_' = pt, pd___ptr_to_struct_pde_C_' = pd, pd___struct_cap_C_' = pd___struct_cap_C, pd___struct_findPDForASID_ret_C_' = pd___struct_findPDForASID_ret_C, pc___unsigned_long_' = pc, pa___unsigned_long_' = pa, nG___unsigned_' = nG, mi___struct_seL4_MessageInfo_C_' = mi, id___unsigned_long_' = id, id___anonymous_enum_' = id___anonymous_enum, ep___ptr_to_struct_endpoint_C_' = ep, ct___struct_cap_transfer_C_' = ct, bi___ptr_to_struct_seL4_BootInfo_C_' = bi, ap___ptr_to_struct_asid_pool_C_' = ap, ap___unsigned_long_' = ap___unsigned_long, XN___unsigned_' = XN, AP___unsigned_' = AP, y___unsigned_' = y, y___int_' = y___int, x___unsigned_' = x, x___unsigned_longlong_' = x___unsigned_longlong, x___unsigned_long_' = x___unsigned_long, x___int_' = x___int, w___unsigned_long_' = w, w___int_' = w___int, w___struct_seL4_CNode_CapData_C_' = w___struct_seL4_CNode_CapData_C, v___unsigned_long_' = va, v___int_' = v___int, v___unsigned_' = v___unsigned, t___unsigned_long_' = t, s___unsigned_long_' = s___unsigned_long, s___ptr_to_char_' = s___ptr_to_char, s___ptr_to_void_' = s, r___unsigned_long_' = r, r___ptr_to_struct_p_region_C_' = r___ptr_to_struct_p_region_C, r___ptr_to_struct_region_C_' = r___ptr_to_struct_region_C, q___ptr_to_unsigned_char_' = q, p___unsigned_long_' = p, p___ptr_to_unsigned_char_' = p___ptr_to_unsigned_char, n___unsigned_long_' = n, n___int_' = n___int, m___struct_region_C_' = m, l___int_' = l, j___unsigned_long_' = j, i___unsigned_long_' = i, i___unsigned_' = i___unsigned, i___int_' = i___int, f___unsigned_long_' = f, e___unsigned_long_' = e, c___unsigned_long_' = c, c___char_' = c___char, b___unsigned_long_' = b, a___unsigned_long_' = a, S___unsigned_' = S, P___unsigned_' = P, C___unsigned_' = C, B___unsigned_' = B, \<dots> = morea\<rparr>) = v proof (prove)
goal:
No subgoals! proof (state)
this:
\<Gamma>\<turnstile> {s. xfu' (\<lambda>_. v) s \<in> G'} Basic (xfu' (\<lambda>_. v)) {s. \<forall>uu. dc uu (xf' s) \<longrightarrow> s \<in> G' \<inter> \<lbrace>xf' s = v\<rbrace>}

goal (2 subgoals):
 1. \<And>s. G s \<Longrightarrow> ((\<lambda>_. True) and G) s
 2. \<And>s. s \<in> {s. xfu' (\<lambda>_. v) s \<in> G'} \<Longrightarrow> s \<in> UNIV \<inter> {s. xfu' (\<lambda>_. v) s \<in> G'}