theory Example_Valid_StateH

lemma step_restrict_s0:
  "1 \<le> maxDomain \<Longrightarrow> step_restrict s0" supply option.case_cong[cong] if_cong[cong] apply (clarsimp simp: step_restrict_def has_srel_state_def) apply (rule_tac x="fst (fst s0H)" in exI) apply (rule_tac x="snd (fst s0H)" in exI) apply (rule_tac x="snd s0H" in exI) apply (simp add: s0H_def lift_fst_rel_def lift_snd_rel_def s0_srel s0_def split del: if_split) apply (rule conjI) apply (clarsimp split: if_split_asm) apply (rule conjI) apply clarsimp apply (frule ct_idle'_related[OF s0_srel s0H_invs]; solves simp) apply clarsimp apply (drule ct_idle_related[OF s0_srel]; simp) apply (clarsimp simp: full_invs_if'_def s0H_invs) apply (rule conjI) apply (simp only: ex_abs_def) apply (rule_tac x="s0_internal" in exI) apply (simp only: einvs_s0 s0_srel) apply (simp add: s0H_internal_def valid_domain_list'_def) apply (rule conjI) apply (clarsimp simp: vs_valid_duplicates'_def split: option.splits) apply (frule kh0H_SomeD) apply (elim disjE, simp_all add: vs_ptr_align_def kh0H_all_obj_def')[1] apply (clarsimp simp: the_nat_to_bl_simps split: if_split_asm) apply (clarsimp simp: the_nat_to_bl_simps split: if_split_asm) apply (clarsimp simp: the_nat_to_bl_simps split: if_split_asm) apply (clarsimp split: if_split_asm) apply (clarsimp simp: High_pd'H_def split: if_split_asm) apply (clarsimp simp: Low_pd'H_def split: if_split_asm) apply (clarsimp simp: High_pt'H_def split: if_split_asm) apply (clarsimp simp: Low_pt'H_def split: if_split_asm) apply (clarsimp simp: ct_in_state'_def st_tcb_at'_def obj_at'_def projectKO_eq project_inject
                        s0H_internal_def objBits_simps' s0_ptrs_aligned Low_tcbH_def) apply (rule pspace_distinctD''[OF _ s0H_pspace_distinct', simplified s0H_internal_def]) apply (simp add: objBits_simps') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> step_restrict s0 proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> step_restrict s0 proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> \<exists>a b ba. (s0, (a, b), ba) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> ((a, b), ba) \<in> full_invs_if' proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> \<exists>b ba. (s0, (fst (fst s0H), b), ba) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> ((fst (fst s0H), b), ba) \<in> full_invs_if' proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> \<exists>b. (s0, (fst (fst s0H), internal_state_if s0H), b) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> ((fst (fst s0H), internal_state_if s0H), b) \<in> full_invs_if' proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> (s0, (fst (fst s0H), internal_state_if s0H), snd s0H) \<in> lift_fst_rel (lift_snd_rel state_relation) \<and> ((fst (fst s0H), internal_state_if s0H), snd s0H) \<in> full_invs_if' proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> (if ct_idle s0_internal then idle_context s0_internal else s0_context) = (if ct_idle' s0H_internal then idle_context s0_internal else s0_context) \<and> ((if ct_idle' s0H_internal then idle_context s0_internal else s0_context, s0H_internal), KernelExit) \<in> full_invs_if' proof (prove)
goal (2 subgoals):
 1. 1 \<le> maxDomain \<Longrightarrow> (if ct_idle s0_internal then idle_context s0_internal else s0_context) = (if ct_idle' s0H_internal then idle_context s0_internal else s0_context)
 2. 1 \<le> maxDomain \<Longrightarrow> ((if ct_idle' s0H_internal then idle_context s0_internal else s0_context, s0H_internal), KernelExit) \<in> full_invs_if' proof (prove)
goal (2 subgoals):
 1. 1 \<le> maxDomain \<Longrightarrow> (ct_idle s0_internal \<longrightarrow> \<not> ct_idle' s0H_internal \<longrightarrow> idle_context s0_internal = s0_context) \<and> (\<not> ct_idle s0_internal \<longrightarrow> ct_idle' s0H_internal \<longrightarrow> s0_context = idle_context s0_internal)
 2. 1 \<le> maxDomain \<Longrightarrow> ((if ct_idle' s0H_internal then idle_context s0_internal else s0_context, s0H_internal), KernelExit) \<in> full_invs_if' proof (prove)
goal (3 subgoals):
 1. 1 \<le> maxDomain \<Longrightarrow> ct_idle s0_internal \<longrightarrow> \<not> ct_idle' s0H_internal \<longrightarrow> idle_context s0_internal = s0_context
 2. 1 \<le> maxDomain \<Longrightarrow> \<not> ct_idle s0_internal \<longrightarrow> ct_idle' s0H_internal \<longrightarrow> s0_context = idle_context s0_internal
 3. 1 \<le> maxDomain \<Longrightarrow> ((if ct_idle' s0H_internal then idle_context s0_internal else s0_context, s0H_internal), KernelExit) \<in> full_invs_if' proof (prove)
goal (3 subgoals):
 1. \<lbrakk>1 \<le> maxDomain; ct_idle s0_internal; \<not> ct_idle' s0H_internal\<rbrakk> \<Longrightarrow> idle_context s0_internal = s0_context
 2. 1 \<le> maxDomain \<Longrightarrow> \<not> ct_idle s0_internal \<longrightarrow> ct_idle' s0H_internal \<longrightarrow> s0_context = idle_context s0_internal
 3. 1 \<le> maxDomain \<Longrightarrow> ((if ct_idle' s0H_internal then idle_context s0_internal else s0_context, s0H_internal), KernelExit) \<in> full_invs_if' proof (prove)
goal (2 subgoals):
 1. 1 \<le> maxDomain \<Longrightarrow> \<not> ct_idle s0_internal \<longrightarrow> ct_idle' s0H_internal \<longrightarrow> s0_context = idle_context s0_internal
 2. 1 \<le> maxDomain \<Longrightarrow> ((if ct_idle' s0H_internal then idle_context s0_internal else s0_context, s0H_internal), KernelExit) \<in> full_invs_if' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>1 \<le> maxDomain; \<not> ct_idle s0_internal; ct_idle' s0H_internal\<rbrakk> \<Longrightarrow> s0_context = idle_context s0_internal
 2. 1 \<le> maxDomain \<Longrightarrow> ((if ct_idle' s0H_internal then idle_context s0_internal else s0_context, s0H_internal), KernelExit) \<in> full_invs_if' proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> ((if ct_idle' s0H_internal then idle_context s0_internal else s0_context, s0H_internal), KernelExit) \<in> full_invs_if' proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> ex_abs einvs s0H_internal \<and> vs_valid_duplicates' kh0H \<and> 0 < ksDomainTime s0H_internal \<and> (ksDomainTime s0H_internal = 0 \<longrightarrow> ksSchedulerAction s0H_internal = ChooseNewThread) \<and> valid_domain_list' s0H_internal \<and> (ct_running' s0H_internal \<or> ct_idle' s0H_internal) \<and> ksSchedulerAction s0H_internal = ResumeCurrentThread \<and> ksDomainTime s0H_internal \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. 1 \<le> maxDomain \<Longrightarrow> ex_abs einvs s0H_internal
 2. 1 \<le> maxDomain \<Longrightarrow> vs_valid_duplicates' kh0H \<and> 0 < ksDomainTime s0H_internal \<and> (ksDomainTime s0H_internal = 0 \<longrightarrow> ksSchedulerAction s0H_internal = ChooseNewThread) \<and> valid_domain_list' s0H_internal \<and> (ct_running' s0H_internal \<or> ct_idle' s0H_internal) \<and> ksSchedulerAction s0H_internal = ResumeCurrentThread \<and> ksDomainTime s0H_internal \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. 1 \<le> maxDomain \<Longrightarrow> \<exists>s. (s, s0H_internal) \<in> state_relation \<and> einvs s
 2. 1 \<le> maxDomain \<Longrightarrow> vs_valid_duplicates' kh0H \<and> 0 < ksDomainTime s0H_internal \<and> (ksDomainTime s0H_internal = 0 \<longrightarrow> ksSchedulerAction s0H_internal = ChooseNewThread) \<and> valid_domain_list' s0H_internal \<and> (ct_running' s0H_internal \<or> ct_idle' s0H_internal) \<and> ksSchedulerAction s0H_internal = ResumeCurrentThread \<and> ksDomainTime s0H_internal \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. 1 \<le> maxDomain \<Longrightarrow> (s0_internal, s0H_internal) \<in> state_relation \<and> einvs s0_internal
 2. 1 \<le> maxDomain \<Longrightarrow> vs_valid_duplicates' kh0H \<and> 0 < ksDomainTime s0H_internal \<and> (ksDomainTime s0H_internal = 0 \<longrightarrow> ksSchedulerAction s0H_internal = ChooseNewThread) \<and> valid_domain_list' s0H_internal \<and> (ct_running' s0H_internal \<or> ct_idle' s0H_internal) \<and> ksSchedulerAction s0H_internal = ResumeCurrentThread \<and> ksDomainTime s0H_internal \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> vs_valid_duplicates' kh0H \<and> 0 < ksDomainTime s0H_internal \<and> (ksDomainTime s0H_internal = 0 \<longrightarrow> ksSchedulerAction s0H_internal = ChooseNewThread) \<and> valid_domain_list' s0H_internal \<and> (ct_running' s0H_internal \<or> ct_idle' s0H_internal) \<and> ksSchedulerAction s0H_internal = ResumeCurrentThread \<and> ksDomainTime s0H_internal \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> vs_valid_duplicates' kh0H \<and> (ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr>) proof (prove)
goal (2 subgoals):
 1. 1 \<le> maxDomain \<Longrightarrow> vs_valid_duplicates' kh0H
 2. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>1 \<le> maxDomain; kh0H x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2)\<rbrakk> \<Longrightarrow> Some x2 = kh0H y
 2. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>x y x2. \<lbrakk>1 \<le> maxDomain; kh0H x = Some x2; is_aligned y 2; x && ~~ mask (vs_ptr_align x2) = y && ~~ mask (vs_ptr_align x2); x = init_globals_frame \<and> x2 = KOUserData \<or> x = idle_tcb_ptr \<and> x2 = KOTCB idle_tcbH \<or> x = High_tcb_ptr \<and> x2 = KOTCB High_tcbH \<or> x = Low_tcb_ptr \<and> x2 = KOTCB Low_tcbH \<or> x = ntfn_ptr \<and> x2 = KONotification ntfnH \<or> x = irq_cnode_ptr \<and> x2 = KOCTE irq_cte \<or> x \<in> irq_node_offs_range \<and> x2 = KOCTE (CTE capability.NullCap (MDB 0 0 False False)) \<or> x \<in> cnode_offs_range Low_cnode_ptr \<and> Low_cte Low_cnode_ptr x \<noteq> None \<and> x2 = the (Low_cte Low_cnode_ptr x) \<or> x \<in> cnode_offs_range High_cnode_ptr \<and> High_cte High_cnode_ptr x \<noteq> None \<and> x2 = the (High_cte High_cnode_ptr x) \<or> x \<in> cnode_offs_range Silc_cnode_ptr \<and> Silc_cte Silc_cnode_ptr x \<noteq> None \<and> x2 = the (Silc_cte Silc_cnode_ptr x) \<or> x \<in> pd_offs_range init_global_pd \<and> global_pdH' init_global_pd x \<noteq> None \<and> x2 = the (global_pdH' init_global_pd x) \<or> x \<in> pd_offs_range High_pd_ptr \<and> High_pdH High_pd_ptr x \<noteq> None \<and> x2 = the (High_pdH High_pd_ptr x) \<or> x \<in> pd_offs_range Low_pd_ptr \<and> Low_pdH Low_pd_ptr x \<noteq> None \<and> x2 = the (Low_pdH Low_pd_ptr x) \<or> x \<in> pt_offs_range High_pt_ptr \<and> High_ptH High_pt_ptr x \<noteq> None \<and> x2 = the (High_ptH High_pt_ptr x) \<or> x \<in> pt_offs_range Low_pt_ptr \<and> Low_ptH Low_pt_ptr x \<noteq> None \<and> x2 = the (Low_ptH Low_pt_ptr x)\<rbrakk> \<Longrightarrow> Some x2 = kh0H y
 2. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (9 subgoals):
 1. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = (if is_aligned x cte_level_bits \<and> Low_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Low_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (Silc_cnode_ptr + 0x13E0) 0 False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB 0 (Low_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB 0 Low_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap Low_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None); is_aligned y 2; x && ~~ mask (case the (if is_aligned x cte_level_bits \<and> Low_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Low_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (Silc_cnode_ptr + 0x13E0) 0 False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB 0 (Low_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB 0 Low_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap Low_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (if is_aligned x cte_level_bits \<and> Low_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Low_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (Silc_cnode_ptr + 0x13E0) 0 False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB 0 (Low_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB 0 Low_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap Low_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> cnode_offs_range Low_cnode_ptr \<and> (\<exists>y. (if is_aligned x cte_level_bits \<and> Low_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Low_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (Silc_cnode_ptr + 0x13E0) 0 False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB 0 (Low_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB 0 Low_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap Low_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) = Some y)\<rbrakk> \<Longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) \<longrightarrow> (is_aligned x cte_level_bits \<and> Low_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Low_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.ThreadCap Low_tcb_ptr) (MDB 0 0 False False))) = kh0H y) \<and> ((Low_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Low_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 (Suc 0) \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 \<longrightarrow> (is_aligned x cte_level_bits \<and> Low_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Low_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.CNodeCap Low_cnode_ptr 10 2 10) (MDB 0 Low_tcb_ptr False False))) = kh0H y) \<and> ((Low_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Low_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 2 \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 \<longrightarrow> (is_aligned x cte_level_bits \<and> Low_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Low_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap Low_pd_ptr (Some Low_asid))) (MDB 0 (Low_tcb_ptr + 0x10) False False))) = kh0H y) \<and> ((Low_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Low_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 3 \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> Low_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Low_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (Silc_cnode_ptr + 0x13E0) 0 False False))) = kh0H y) \<and> ((Low_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Low_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - Low_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> Low_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Low_cnode_ptr \<longrightarrow> Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) = kh0H y) \<and> ((Low_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Low_cnode_ptr) \<longrightarrow> None = kh0H y)))))
 2. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = (if is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None); is_aligned y 2; x && ~~ mask (case the (if is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (if is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> cnode_offs_range High_cnode_ptr \<and> (\<exists>y. (if is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) = Some y)\<rbrakk> \<Longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) \<longrightarrow> (is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False))) = kh0H y) \<and> ((High_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + High_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 (Suc 0) \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 \<longrightarrow> (is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False))) = kh0H y) \<and> ((High_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + High_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 2 \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 \<longrightarrow> (is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False))) = kh0H y) \<and> ((High_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + High_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 3 \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False))) = kh0H y) \<and> ((High_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + High_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr \<longrightarrow> Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) = kh0H y) \<and> ((High_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + High_cnode_ptr) \<longrightarrow> None = kh0H y)))))
 3. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None); is_aligned y 2; x && ~~ mask (case the (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> cnode_offs_range Silc_cnode_ptr \<and> (\<exists>y. (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) = Some y)\<rbrakk> \<Longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 \<longrightarrow> (is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False))) = kh0H y) \<and> ((Silc_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Silc_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 2 \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))) = kh0H y) \<and> ((Silc_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Silc_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr \<longrightarrow> Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) = kh0H y) \<and> ((Silc_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Silc_cnode_ptr) \<longrightarrow> None = kh0H y)))
 4. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range init_global_pd \<and> (\<exists>y. (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2) = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd \<longrightarrow> Some (KOArch (KOPDE (ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {})))) = kh0H y) \<and> ((init_global_pd \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + init_global_pd) \<longrightarrow> None = kh0H y)) \<and> (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2) \<noteq> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd \<longrightarrow> Some (KOArch (KOPDE ARM_H.InvalidPDE)) = kh0H y) \<and> ((init_global_pd \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + init_global_pd) \<longrightarrow> None = kh0H y))
 5. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range High_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (High_pd'H (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2))))) = kh0H y) \<and> ((High_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + High_pd_ptr) \<longrightarrow> None = kh0H y)
 6. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range Low_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (Low_pd'H (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2))))) = kh0H y) \<and> ((Low_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + Low_pd_ptr) \<longrightarrow> None = kh0H y)
 7. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range High_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (High_pt'H (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2))))) = kh0H y) \<and> ((High_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + High_pt_ptr) \<longrightarrow> None = kh0H y)
 8. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range Low_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (Low_pt'H (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2))))) = kh0H y) \<and> ((Low_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + Low_pt_ptr) \<longrightarrow> None = kh0H y)
 9. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (8 subgoals):
 1. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = (if is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None); is_aligned y 2; x && ~~ mask (case the (if is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (if is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> cnode_offs_range High_cnode_ptr \<and> (\<exists>y. (if is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 then Some (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) then Some (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) = Some y)\<rbrakk> \<Longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 (Suc 0) \<longrightarrow> (is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.ThreadCap High_tcb_ptr) (MDB 0 0 False False))) = kh0H y) \<and> ((High_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + High_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 (Suc 0) \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 \<longrightarrow> (is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.CNodeCap High_cnode_ptr 10 2 10) (MDB 0 High_tcb_ptr False False))) = kh0H y) \<and> ((High_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + High_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 2 \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 3 \<longrightarrow> (is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.ArchObjectCap (arch_capability.PageDirectoryCap High_pd_ptr (Some High_asid))) (MDB 0 (High_tcb_ptr + 0x10) False False))) = kh0H y) \<and> ((High_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + High_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 3 \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.NotificationCap ntfn_ptr 0 False True) (MDB 0 (Silc_cnode_ptr + 0x13E0) False False))) = kh0H y) \<and> ((High_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + High_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - High_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> High_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + High_cnode_ptr \<longrightarrow> Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) = kh0H y) \<and> ((High_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + High_cnode_ptr) \<longrightarrow> None = kh0H y)))))
 2. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None); is_aligned y 2; x && ~~ mask (case the (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> cnode_offs_range Silc_cnode_ptr \<and> (\<exists>y. (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) = Some y)\<rbrakk> \<Longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 \<longrightarrow> (is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False))) = kh0H y) \<and> ((Silc_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Silc_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 2 \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))) = kh0H y) \<and> ((Silc_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Silc_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr \<longrightarrow> Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) = kh0H y) \<and> ((Silc_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Silc_cnode_ptr) \<longrightarrow> None = kh0H y)))
 3. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range init_global_pd \<and> (\<exists>y. (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2) = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd \<longrightarrow> Some (KOArch (KOPDE (ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {})))) = kh0H y) \<and> ((init_global_pd \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + init_global_pd) \<longrightarrow> None = kh0H y)) \<and> (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2) \<noteq> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd \<longrightarrow> Some (KOArch (KOPDE ARM_H.InvalidPDE)) = kh0H y) \<and> ((init_global_pd \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + init_global_pd) \<longrightarrow> None = kh0H y))
 4. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range High_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (High_pd'H (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2))))) = kh0H y) \<and> ((High_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + High_pd_ptr) \<longrightarrow> None = kh0H y)
 5. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range Low_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (Low_pd'H (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2))))) = kh0H y) \<and> ((Low_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + Low_pd_ptr) \<longrightarrow> None = kh0H y)
 6. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range High_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (High_pt'H (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2))))) = kh0H y) \<and> ((High_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + High_pt_ptr) \<longrightarrow> None = kh0H y)
 7. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range Low_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (Low_pt'H (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2))))) = kh0H y) \<and> ((Low_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + Low_pt_ptr) \<longrightarrow> None = kh0H y)
 8. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None); is_aligned y 2; x && ~~ mask (case the (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> cnode_offs_range Silc_cnode_ptr \<and> (\<exists>y. (if is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr then map_option KOCTE (if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 then Some (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False)) else if to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 then Some (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False)) else Some (CTE capability.NullCap (MDB 0 0 False False))) else None) = Some y)\<rbrakk> \<Longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 2 \<longrightarrow> (is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.CNodeCap Silc_cnode_ptr 10 2 10) (MDB 0 0 False False))) = kh0H y) \<and> ((Silc_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Silc_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 2 \<longrightarrow> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) = the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr \<longrightarrow> Some (KOCTE (CTE (capability.NotificationCap ntfn_ptr 0 True False) (MDB (High_cnode_ptr + 0x13E0) (Low_cnode_ptr + 0x13E0) False False))) = kh0H y) \<and> ((Silc_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Silc_cnode_ptr) \<longrightarrow> None = kh0H y)) \<and> (to_bl (UCAST(32 \<rightarrow> 10) (x - Silc_cnode_ptr >> cte_level_bits)) \<noteq> the_nat_to_bl 10 318 \<longrightarrow> (is_aligned x cte_level_bits \<and> Silc_cnode_ptr \<le> x \<and> x \<le> 0x3FFF + Silc_cnode_ptr \<longrightarrow> Some (KOCTE (CTE capability.NullCap (MDB 0 0 False False))) = kh0H y) \<and> ((Silc_cnode_ptr \<le> x \<longrightarrow> is_aligned x cte_level_bits \<longrightarrow> \<not> x \<le> 0x3FFF + Silc_cnode_ptr) \<longrightarrow> None = kh0H y)))
 2. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range init_global_pd \<and> (\<exists>y. (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2) = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd \<longrightarrow> Some (KOArch (KOPDE (ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {})))) = kh0H y) \<and> ((init_global_pd \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + init_global_pd) \<longrightarrow> None = kh0H y)) \<and> (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2) \<noteq> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd \<longrightarrow> Some (KOArch (KOPDE ARM_H.InvalidPDE)) = kh0H y) \<and> ((init_global_pd \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + init_global_pd) \<longrightarrow> None = kh0H y))
 3. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range High_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (High_pd'H (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2))))) = kh0H y) \<and> ((High_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + High_pd_ptr) \<longrightarrow> None = kh0H y)
 4. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range Low_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (Low_pd'H (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2))))) = kh0H y) \<and> ((Low_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + Low_pd_ptr) \<longrightarrow> None = kh0H y)
 5. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range High_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (High_pt'H (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2))))) = kh0H y) \<and> ((High_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + High_pt_ptr) \<longrightarrow> None = kh0H y)
 6. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range Low_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (Low_pt'H (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2))))) = kh0H y) \<and> ((Low_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + Low_pt_ptr) \<longrightarrow> None = kh0H y)
 7. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (6 subgoals):
 1. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (if x = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) then ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {}) else ARM_H.InvalidPDE))) (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range init_global_pd \<and> (\<exists>y. (if is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd then Some (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2) = UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd \<longrightarrow> Some (KOArch (KOPDE (ARM_H.SectionPDE (addrFromPPtr kernel_base) False 0 False False False (vmrights_map {})))) = kh0H y) \<and> ((init_global_pd \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + init_global_pd) \<longrightarrow> None = kh0H y)) \<and> (UCAST(32 \<rightarrow> 12) (x - init_global_pd >> 2) \<noteq> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<longrightarrow> (is_aligned x 2 \<and> init_global_pd \<le> x \<and> x \<le> 0x3FFF + init_global_pd \<longrightarrow> Some (KOArch (KOPDE ARM_H.InvalidPDE)) = kh0H y) \<and> ((init_global_pd \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + init_global_pd) \<longrightarrow> None = kh0H y))
 2. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range High_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (High_pd'H (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2))))) = kh0H y) \<and> ((High_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + High_pd_ptr) \<longrightarrow> None = kh0H y)
 3. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range Low_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (Low_pd'H (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2))))) = kh0H y) \<and> ((Low_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + Low_pd_ptr) \<longrightarrow> None = kh0H y)
 4. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range High_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (High_pt'H (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2))))) = kh0H y) \<and> ((High_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + High_pt_ptr) \<longrightarrow> None = kh0H y)
 5. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range Low_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (Low_pt'H (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2))))) = kh0H y) \<and> ((Low_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + Low_pt_ptr) \<longrightarrow> None = kh0H y)
 6. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (High_pd'H x))) (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range High_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pd_ptr \<le> x \<and> x \<le> 0x3FFF + High_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (High_pd'H (UCAST(32 \<rightarrow> 12) (x - High_pd_ptr >> 2))))) = kh0H y) \<and> ((High_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + High_pd_ptr) \<longrightarrow> None = kh0H y)
 2. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range Low_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (Low_pd'H (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2))))) = kh0H y) \<and> ((Low_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + Low_pd_ptr) \<longrightarrow> None = kh0H y)
 3. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range High_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (High_pt'H (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2))))) = kh0H y) \<and> ((High_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + High_pt_ptr) \<longrightarrow> None = kh0H y)
 4. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range Low_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (Low_pt'H (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2))))) = kh0H y) \<and> ((Low_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + Low_pt_ptr) \<longrightarrow> None = kh0H y)
 5. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPDE (Low_pd'H x))) (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pd_offs_range Low_pd_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr then Some (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pd_ptr \<le> x \<and> x \<le> 0x3FFF + Low_pd_ptr \<longrightarrow> Some (KOArch (KOPDE (Low_pd'H (UCAST(32 \<rightarrow> 12) (x - Low_pd_ptr >> 2))))) = kh0H y) \<and> ((Low_pd_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FFF + Low_pd_ptr) \<longrightarrow> None = kh0H y)
 2. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range High_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (High_pt'H (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2))))) = kh0H y) \<and> ((High_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + High_pt_ptr) \<longrightarrow> None = kh0H y)
 3. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range Low_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (Low_pt'H (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2))))) = kh0H y) \<and> ((Low_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + Low_pt_ptr) \<longrightarrow> None = kh0H y)
 4. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (High_pt'H x))) (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range High_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> High_pt_ptr \<le> x \<and> x \<le> 0x3FF + High_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (High_pt'H (UCAST(32 \<rightarrow> 8) (x - High_pt_ptr >> 2))))) = kh0H y) \<and> ((High_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + High_pt_ptr) \<longrightarrow> None = kh0H y)
 2. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range Low_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (Low_pt'H (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2))))) = kh0H y) \<and> ((Low_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + Low_pt_ptr) \<longrightarrow> None = kh0H y)
 3. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>1 \<le> maxDomain; kh0H x = map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None); is_aligned y 2; x && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0) = y && ~~ mask (case the (map_option (\<lambda>x. KOArch (KOPTE (Low_pt'H x))) (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None)) of KOArch (KOASIDPool asidpool) \<Rightarrow> 0 | KOArch (KOPTE (ARM_H.LargePagePTE x xaa xb xc xd)) \<Rightarrow> 6 | KOArch (KOPTE _) \<Rightarrow> 0 | KOArch (KOPDE (ARM_H.SuperSectionPDE x xaa xb xc xd xe)) \<Rightarrow> 6 | KOArch (KOPDE _) \<Rightarrow> 0 | _ \<Rightarrow> 0); x \<in> pt_offs_range Low_pt_ptr \<and> (\<exists>y. (if is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr then Some (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2)) else None) = Some y)\<rbrakk> \<Longrightarrow> (is_aligned x 2 \<and> Low_pt_ptr \<le> x \<and> x \<le> 0x3FF + Low_pt_ptr \<longrightarrow> Some (KOArch (KOPTE (Low_pt'H (UCAST(32 \<rightarrow> 8) (x - Low_pt_ptr >> 2))))) = kh0H y) \<and> ((Low_pt_ptr \<le> x \<longrightarrow> is_aligned x 2 \<longrightarrow> \<not> x \<le> 0x3FF + Low_pt_ptr) \<longrightarrow> None = kh0H y)
 2. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> ct_running' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> \<or> ct_idle' \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> ps_clear Low_tcb_ptr 9 \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> proof (prove)
goal (1 subgoal):
 1. 1 \<le> maxDomain \<Longrightarrow> \<exists>v. ksPSpace \<lparr>ksPSpace = kh0H, gsUserPages = \<lambda>x. if x = init_globals_frame then Some ARMSmallPage else None, gsCNodes = (\<lambda>x. if \<exists>irq. init_irq_node_ptr + (UCAST(10 \<rightarrow> 32) irq << cte_level_bits) = x then Some 0 else None)(Low_cnode_ptr \<mapsto> 10, High_cnode_ptr \<mapsto> 10, Silc_cnode_ptr \<mapsto> 10, irq_cnode_ptr \<mapsto> 0), gsUntypedZeroRanges = ran (untypedZeroRange \<circ>\<^sub>m (map_option cteCap \<circ> map_to_ctes kh0H)), gsMaxObjectSize = CARD(32 word), ksDomScheduleIdx = 0, ksDomSchedule = [(0, 0xA), (1, 0xA)], ksCurDomain = 0, ksDomainTime = 5, ksReadyQueues = const [], ksReadyQueuesL1Bitmap = const 0, ksReadyQueuesL2Bitmap = const 0, ksCurThread = Low_tcb_ptr, ksIdleThread = idle_tcb_ptr, ksSchedulerAction = ResumeCurrentThread, ksInterruptState = InterruptState init_irq_node_ptr ((\<lambda>_. irqstate.IRQInactive)(timer_irq := irqstate.IRQTimer)), ksWorkUnitsCompleted = undefined, ksArchState = arch_state0H, ksMachineState = machine_state0\<rparr> Low_tcb_ptr = Some v \<and> objBitsKO v = 9 proof (prove)
goal:
No subgoals!