theory Arch_DP

lemma invoke_asid_pool_wp:
  "off < 2 ^ asid_low_bits \<Longrightarrow>
  \<lbrace> <(cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap
    \<and>* (\<And>* off\<in>{off. off < 2 ^ asid_low_bits}. (p, off) \<mapsto>c -)
    \<and>* pd_ref \<mapsto>c (PageDirectoryCap pd Real asid')
    \<and>* R > \<rbrace>
  invoke_asid_pool (Assign asid pd_ref (p,off))
  \<lbrace>\<lambda>rv s. <(cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap
    \<and>* pd_ref \<mapsto>c  (PageDirectoryCap pd Real (Some asid))
    \<and>* (\<And>* off\<in>{off. off < 2 ^ asid_low_bits}. (p, off) \<mapsto>c -)
    \<and>* R > s\<rbrace>" apply (clarsimp simp:invoke_asid_pool_def | wp| wpc)+ apply (rename_tac word cdl_frame_cap_type option) apply (rule_tac P = "word = pd" in hoare_gen_asm) apply simp apply (rule hoare_strengthen_post[OF set_cap_wp]) apply (subst set_split_single[where A = "(Collect (\<lambda>off. off < 2 ^ asid_low_bits))"]) apply simp apply (subst sep.prod.union_disjoint) apply simp+ apply (clarsimp simp: sep_conj_assoc) apply (sep_erule_concl sep_any_imp, sep_solve) apply (rename_tac word cdl_frame_cap_type option) apply (wp hoare_vcg_conj_lift) apply (rule_tac P = "word = pd" in hoare_gen_asm) apply simp apply (rule hoare_strengthen_post[OF set_cap_wp]) apply (sep_solve) apply wp+ apply clarsimp apply (safe; fastforce?) apply (subst (asm) set_split_single[where A = "(Collect (\<lambda>off. off < 2 ^ asid_low_bits))"]) apply simp apply (subst (asm) sep.prod.union_disjoint) apply simp+ apply (simp add:sep_conj_assoc) apply sep_solve apply (sep_select_asm 3) apply (drule opt_cap_sep_imp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R)\<rbrace> invoke_asid_pool (Assign asid pd_ref (p, off)) \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?B164 x191 x192 x193 ()\<rbrace> set_cap (p, off) (PageDirectoryCap x191 Fake None) \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 2. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>?B164 x191 x192 x193\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word cdl_frame_cap_type option. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?B164 word cdl_frame_cap_type option ()\<rbrace> set_cap (p, off) (PageDirectoryCap word Fake None) \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 2. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>?B164 x191 x192 x193\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word cdl_frame_cap_type option. \<lbrakk>off < 2 ^ asid_low_bits; word = pd\<rbrakk> \<Longrightarrow> \<lbrace>?P'170 word cdl_frame_cap_type option ()\<rbrace> set_cap (p, off) (PageDirectoryCap word Fake None) \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 2. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>\<lambda>a. ?P'170 x191 x192 x193 a and K (x191 = pd)\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word cdl_frame_cap_type option. \<lbrakk>off < 2 ^ asid_low_bits; word = pd\<rbrakk> \<Longrightarrow> \<lbrace>?P'170 pd cdl_frame_cap_type option ()\<rbrace> set_cap (p, off) (PageDirectoryCap pd Fake None) \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 2. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>\<lambda>a. ?P'170 x191 x192 x193 a and K (x191 = pd)\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word cdl_frame_cap_type option rv s. \<lbrakk>off < 2 ^ asid_low_bits; word = pd; cdl.lift ((p, off) \<mapsto>c PageDirectoryCap pd Fake None \<and>* ?R174 pd cdl_frame_cap_type option ()) s\<rbrakk> \<Longrightarrow> cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s
 2. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>\<lambda>a. cdl.lift ((p, off) \<mapsto>c - \<and>* ?R174 x191 x192 x193 a) and K (x191 = pd)\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>word cdl_frame_cap_type option rv s. \<lbrakk>off < 2 ^ asid_low_bits; word = pd; cdl.lift ((p, off) \<mapsto>c PageDirectoryCap pd Fake None \<and>* ?R174 pd cdl_frame_cap_type option ()) s\<rbrakk> \<Longrightarrow> ?a178 word cdl_frame_cap_type option rv s \<in> {off. off < 2 ^ asid_low_bits}
 2. \<And>word cdl_frame_cap_type option rv s. \<lbrakk>off < 2 ^ asid_low_bits; word = pd; cdl.lift ((p, off) \<mapsto>c PageDirectoryCap pd Fake None \<and>* ?R174 pd cdl_frame_cap_type option ()) s\<rbrakk> \<Longrightarrow> cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {?a178 word cdl_frame_cap_type option rv s} \<union> {?a178 word cdl_frame_cap_type option rv s}. (p, off) \<mapsto>c -) \<and>* R) s
 3. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>\<lambda>a. cdl.lift ((p, off) \<mapsto>c - \<and>* ?R174 x191 x192 x193 a) and K (x191 = pd)\<rbrace>
 4. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word cdl_frame_cap_type option rv s. \<lbrakk>off < 2 ^ asid_low_bits; word = pd; cdl.lift ((p, off) \<mapsto>c PageDirectoryCap pd Fake None \<and>* ?R174 pd cdl_frame_cap_type option ()) s\<rbrakk> \<Longrightarrow> cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off} \<union> {off}. (p, off) \<mapsto>c -) \<and>* R) s
 2. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>\<lambda>a. cdl.lift ((p, off) \<mapsto>c - \<and>* ?R174 x191 x192 x193 a) and K (x191 = pd)\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>word cdl_frame_cap_type option rv s. \<lbrakk>off < 2 ^ asid_low_bits; word = pd; cdl.lift ((p, off) \<mapsto>c PageDirectoryCap pd Fake None \<and>* ?R174 pd cdl_frame_cap_type option ()) s\<rbrakk> \<Longrightarrow> finite ({off. off < 2 ^ asid_low_bits} - {off})
 2. \<And>word cdl_frame_cap_type option rv s. \<lbrakk>off < 2 ^ asid_low_bits; word = pd; cdl.lift ((p, off) \<mapsto>c PageDirectoryCap pd Fake None \<and>* ?R174 pd cdl_frame_cap_type option ()) s\<rbrakk> \<Longrightarrow> finite {off}
 3. \<And>word cdl_frame_cap_type option rv s. \<lbrakk>off < 2 ^ asid_low_bits; word = pd; cdl.lift ((p, off) \<mapsto>c PageDirectoryCap pd Fake None \<and>* ?R174 pd cdl_frame_cap_type option ()) s\<rbrakk> \<Longrightarrow> ({off. off < 2 ^ asid_low_bits} - {off}) \<inter> {off} = {}
 4. \<And>word cdl_frame_cap_type option rv s. \<lbrakk>off < 2 ^ asid_low_bits; word = pd; cdl.lift ((p, off) \<mapsto>c PageDirectoryCap pd Fake None \<and>* ?R174 pd cdl_frame_cap_type option ()) s\<rbrakk> \<Longrightarrow> cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* ((SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* (SETSEPCONJ off:{off}. (p, off) \<mapsto>c -)) \<and>* R) s
 5. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>\<lambda>a. cdl.lift ((p, off) \<mapsto>c - \<and>* ?R174 x191 x192 x193 a) and K (x191 = pd)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 15 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word cdl_frame_cap_type option s. \<lbrakk>off < 2 ^ asid_low_bits; word = pd; cdl.lift ((p, off) \<mapsto>c PageDirectoryCap pd Fake None \<and>* ?R174 pd cdl_frame_cap_type option ()) s\<rbrakk> \<Longrightarrow> cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* ((SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* (p, off) \<mapsto>c -) \<and>* R) s
 2. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>\<lambda>a. cdl.lift ((p, off) \<mapsto>c - \<and>* ?R174 x191 x192 x193 a) and K (x191 = pd)\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>cdl_frame_cap_type option s. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((p, off) \<mapsto>c PageDirectoryCap pd Fake None \<and>* ?R174 pd cdl_frame_cap_type option ()) s\<rbrakk> \<Longrightarrow> cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* (p, off) \<mapsto>c - \<and>* R) s
 2. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>\<lambda>a. cdl.lift ((p, off) \<mapsto>c - \<and>* ?R174 x191 x192 x193 a) and K (x191 = pd)\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>x191 x192 x193. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap x191 x192 x193) x191 x192 x193\<rbrace> set_cap pd_ref (PageDirectoryCap x191 Real (Some asid)) \<lbrace>\<lambda>a. cdl.lift ((p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap x191 Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R) and K (x191 = pd)\<rbrace>
 2. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 3. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> get_cap pd_ref \<lbrace>\<lambda>x s. (x = NullCap \<longrightarrow> ?R107 x s) \<and> (\<forall>xa xb xc. x = UntypedCap xa xb xc \<longrightarrow> ?R108 x xa xb xc s) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> ?R109 x xa xb xc s) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> ?R110 x xa xb xc s) \<and> (\<forall>xa xb. x = ReplyCap xa xb \<longrightarrow> ?R111 x xa xb s) \<and> (\<forall>xa. x = MasterReplyCap xa \<longrightarrow> ?R112 x xa s) \<and> (\<forall>xa xb xc xd. x = CNodeCap xa xb xc xd \<longrightarrow> ?R113 x xa xb xc xd s) \<and> (\<forall>xa. x = TcbCap xa \<longrightarrow> ?R114 x xa s) \<and> (x = DomainCap \<longrightarrow> ?R115 x s) \<and> (\<forall>xa xb xc xd xe xf. x = PendingSyncSendCap xa xb xc xd xe xf \<longrightarrow> ?R116 x xa xb xc xd xe xf s) \<and> (\<forall>xa xb xc. x = PendingSyncRecvCap xa xb xc \<longrightarrow> ?R117 x xa xb xc s) \<and> (\<forall>xa. x = PendingNtfnRecvCap xa \<longrightarrow> ?R118 x xa s) \<and> (x = RestartCap \<longrightarrow> ?R119 x s) \<and> (x = RunningCap \<longrightarrow> ?R120 x s) \<and> (x = IrqControlCap \<longrightarrow> ?R121 x s) \<and> (\<forall>xa. x = IrqHandlerCap xa \<longrightarrow> ?R122 x xa s) \<and> (\<forall>xa xb xc xd xe xf. x = FrameCap xa xb xc xd xe xf \<longrightarrow> ?R123 x xa xb xc xd xe xf s) \<and> (\<forall>xa xb xc. x = PageTableCap xa xb xc \<longrightarrow> ?R124 x xa xb xc s) \<and> (\<forall>xa xb xc. x = PageDirectoryCap xa xb xc \<longrightarrow> ?R125 x xa xb xc s) \<and> (x = AsidControlCap \<longrightarrow> ?R126 x s) \<and> (\<forall>xa xb. x = AsidPoolCap xa xb \<longrightarrow> ?R127 x xa xb s) \<and> (\<forall>xa xb. x = IOPortsCap xa xb \<longrightarrow> ?R128 x xa xb s) \<and> (x = IOSpaceMasterCap \<longrightarrow> ?R129 x s) \<and> (\<forall>xa. x = IOSpaceCap xa \<longrightarrow> ?R130 x xa s) \<and> (\<forall>xa. x = IOPageTableCap xa \<longrightarrow> ?R131 x xa s) \<and> (\<forall>xa. x = ZombieCap xa \<longrightarrow> ?R132 x xa s) \<and> (\<forall>xa. x = BoundNotificationCap xa \<longrightarrow> ?R133 x xa s)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>word cdl_frame_cap_type option. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?R125 (PageDirectoryCap word cdl_frame_cap_type option) word cdl_frame_cap_type option\<rbrace> set_cap pd_ref (PageDirectoryCap word Real (Some asid)) \<lbrace>\<lambda>a. cdl.lift ((p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap word Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R) and K (word = pd)\<rbrace>
 2. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 3. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> get_cap pd_ref \<lbrace>\<lambda>x s. (x = NullCap \<longrightarrow> ?R107 x s) \<and> (\<forall>xa xb xc. x = UntypedCap xa xb xc \<longrightarrow> ?R108 x xa xb xc s) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> ?R109 x xa xb xc s) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> ?R110 x xa xb xc s) \<and> (\<forall>xa xb. x = ReplyCap xa xb \<longrightarrow> ?R111 x xa xb s) \<and> (\<forall>xa. x = MasterReplyCap xa \<longrightarrow> ?R112 x xa s) \<and> (\<forall>xa xb xc xd. x = CNodeCap xa xb xc xd \<longrightarrow> ?R113 x xa xb xc xd s) \<and> (\<forall>xa. x = TcbCap xa \<longrightarrow> ?R114 x xa s) \<and> (x = DomainCap \<longrightarrow> ?R115 x s) \<and> (\<forall>xa xb xc xd xe xf. x = PendingSyncSendCap xa xb xc xd xe xf \<longrightarrow> ?R116 x xa xb xc xd xe xf s) \<and> (\<forall>xa xb xc. x = PendingSyncRecvCap xa xb xc \<longrightarrow> ?R117 x xa xb xc s) \<and> (\<forall>xa. x = PendingNtfnRecvCap xa \<longrightarrow> ?R118 x xa s) \<and> (x = RestartCap \<longrightarrow> ?R119 x s) \<and> (x = RunningCap \<longrightarrow> ?R120 x s) \<and> (x = IrqControlCap \<longrightarrow> ?R121 x s) \<and> (\<forall>xa. x = IrqHandlerCap xa \<longrightarrow> ?R122 x xa s) \<and> (\<forall>xa xb xc xd xe xf. x = FrameCap xa xb xc xd xe xf \<longrightarrow> ?R123 x xa xb xc xd xe xf s) \<and> (\<forall>xa xb xc. x = PageTableCap xa xb xc \<longrightarrow> ?R124 x xa xb xc s) \<and> (\<forall>xa xb xc. x = PageDirectoryCap xa xb xc \<longrightarrow> ?R125 x xa xb xc s) \<and> (x = AsidControlCap \<longrightarrow> ?R126 x s) \<and> (\<forall>xa xb. x = AsidPoolCap xa xb \<longrightarrow> ?R127 x xa xb s) \<and> (\<forall>xa xb. x = IOPortsCap xa xb \<longrightarrow> ?R128 x xa xb s) \<and> (x = IOSpaceMasterCap \<longrightarrow> ?R129 x s) \<and> (\<forall>xa. x = IOSpaceCap xa \<longrightarrow> ?R130 x xa s) \<and> (\<forall>xa. x = IOPageTableCap xa \<longrightarrow> ?R131 x xa s) \<and> (\<forall>xa. x = ZombieCap xa \<longrightarrow> ?R132 x xa s) \<and> (\<forall>xa. x = BoundNotificationCap xa \<longrightarrow> ?R133 x xa s)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word cdl_frame_cap_type option. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?P203 (PageDirectoryCap word cdl_frame_cap_type option) word cdl_frame_cap_type option\<rbrace> set_cap pd_ref (PageDirectoryCap word Real (Some asid)) \<lbrace>\<lambda>rv. cdl.lift ((p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap word Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 2. \<And>word cdl_frame_cap_type option. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?P'202 (PageDirectoryCap word cdl_frame_cap_type option) word cdl_frame_cap_type option\<rbrace> set_cap pd_ref (PageDirectoryCap word Real (Some asid)) \<lbrace>\<lambda>rv. K (word = pd)\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word cdl_frame_cap_type option. \<lbrakk>off < 2 ^ asid_low_bits; word = pd\<rbrakk> \<Longrightarrow> \<lbrace>?P'207 (PageDirectoryCap word cdl_frame_cap_type option) word cdl_frame_cap_type option\<rbrace> set_cap pd_ref (PageDirectoryCap word Real (Some asid)) \<lbrace>\<lambda>rv. cdl.lift ((p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap word Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 2. \<And>word cdl_frame_cap_type option. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?P'202 (PageDirectoryCap word cdl_frame_cap_type option) word cdl_frame_cap_type option\<rbrace> set_cap pd_ref (PageDirectoryCap word Real (Some asid)) \<lbrace>\<lambda>rv. K (word = pd)\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word cdl_frame_cap_type option. \<lbrakk>off < 2 ^ asid_low_bits; word = pd\<rbrakk> \<Longrightarrow> \<lbrace>?P'207 (PageDirectoryCap pd cdl_frame_cap_type option) pd cdl_frame_cap_type option\<rbrace> set_cap pd_ref (PageDirectoryCap pd Real (Some asid)) \<lbrace>\<lambda>rv. cdl.lift ((p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 2. \<And>word cdl_frame_cap_type option. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?P'202 (PageDirectoryCap word cdl_frame_cap_type option) word cdl_frame_cap_type option\<rbrace> set_cap pd_ref (PageDirectoryCap word Real (Some asid)) \<lbrace>\<lambda>rv. K (word = pd)\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word cdl_frame_cap_type option rv s. \<lbrakk>off < 2 ^ asid_low_bits; word = pd; cdl.lift (pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* ?R217 (PageDirectoryCap pd cdl_frame_cap_type option) pd cdl_frame_cap_type option) s\<rbrakk> \<Longrightarrow> cdl.lift ((p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R) s
 2. \<And>word cdl_frame_cap_type option. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?P'202 (PageDirectoryCap word cdl_frame_cap_type option) word cdl_frame_cap_type option\<rbrace> set_cap pd_ref (PageDirectoryCap word Real (Some asid)) \<lbrace>\<lambda>rv. K (word = pd)\<rbrace>
 3. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>word cdl_frame_cap_type option. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?P'202 (PageDirectoryCap word cdl_frame_cap_type option) word cdl_frame_cap_type option\<rbrace> set_cap pd_ref (PageDirectoryCap word Real (Some asid)) \<lbrace>\<lambda>rv. K (word = pd)\<rbrace>
 2. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidControlCap\<rbrakk> \<Longrightarrow> \<lbrace>?R126 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 3. \<And>x x211 x212. \<lbrakk>off < 2 ^ asid_low_bits; x = AsidPoolCap x211 x212\<rbrakk> \<Longrightarrow> \<lbrace>?R127 x x211 x212\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 4. \<And>x x221 x222. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPortsCap x221 x222\<rbrakk> \<Longrightarrow> \<lbrace>?R128 x x221 x222\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 5. \<And>x. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceMasterCap\<rbrakk> \<Longrightarrow> \<lbrace>?R129 x\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 6. \<And>x x24. \<lbrakk>off < 2 ^ asid_low_bits; x = IOSpaceCap x24\<rbrakk> \<Longrightarrow> \<lbrace>?R130 x x24\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 7. \<And>x x25. \<lbrakk>off < 2 ^ asid_low_bits; x = IOPageTableCap x25\<rbrakk> \<Longrightarrow> \<lbrace>?R131 x x25\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 8. \<And>x x26. \<lbrakk>off < 2 ^ asid_low_bits; x = ZombieCap x26\<rbrakk> \<Longrightarrow> \<lbrace>?R132 x x26\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 9. \<And>x x27. \<lbrakk>off < 2 ^ asid_low_bits; x = BoundNotificationCap x27\<rbrakk> \<Longrightarrow> \<lbrace>?R133 x x27\<rbrace> fail \<lbrace>\<lambda>rv. cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real (Some asid) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R)\<rbrace>
 10. off < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?Q\<rbrace> get_cap pd_ref \<lbrace>\<lambda>x s. (x = NullCap \<longrightarrow> ?R107 x s) \<and> (\<forall>xa xb xc. x = UntypedCap xa xb xc \<longrightarrow> ?R108 x xa xb xc s) \<and> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> ?R109 x xa xb xc s) \<and> (\<forall>xa xb xc. x = NotificationCap xa xb xc \<longrightarrow> ?R110 x xa xb xc s) \<and> (\<forall>xa xb. x = ReplyCap xa xb \<longrightarrow> ?R111 x xa xb s) \<and> (\<forall>xa. x = MasterReplyCap xa \<longrightarrow> ?R112 x xa s) \<and> (\<forall>xa xb xc xd. x = CNodeCap xa xb xc xd \<longrightarrow> ?R113 x xa xb xc xd s) \<and> (\<forall>xa. x = TcbCap xa \<longrightarrow> ?R114 x xa s) \<and> (x = DomainCap \<longrightarrow> ?R115 x s) \<and> (\<forall>xa xb xc xd xe xf. x = PendingSyncSendCap xa xb xc xd xe xf \<longrightarrow> ?R116 x xa xb xc xd xe xf s) \<and> (\<forall>xa xb xc. x = PendingSyncRecvCap xa xb xc \<longrightarrow> ?R117 x xa xb xc s) \<and> (\<forall>xa. x = PendingNtfnRecvCap xa \<longrightarrow> ?R118 x xa s) \<and> (x = RestartCap \<longrightarrow> ?R119 x s) \<and> (x = RunningCap \<longrightarrow> ?R120 x s) \<and> (x = IrqControlCap \<longrightarrow> ?R121 x s) \<and> (\<forall>xa. x = IrqHandlerCap xa \<longrightarrow> ?R122 x xa s) \<and> (\<forall>xa xb xc xd xe xf. x = FrameCap xa xb xc xd xe xf \<longrightarrow> ?R123 x xa xb xc xd xe xf s) \<and> (\<forall>xa xb xc. x = PageTableCap xa xb xc \<longrightarrow> ?R124 x xa xb xc s) \<and> (\<forall>xa xb xc. x = PageDirectoryCap xa xb xc \<longrightarrow> (cdl.lift (pd_ref \<mapsto>c - \<and>* (pd_ref \<mapsto>c PageDirectoryCap xa Real (Some asid) \<longrightarrow>* (p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap xa Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)) and K (xa = pd)) s \<and> ?P'202 x xa xb xc s) \<and> (x = AsidControlCap \<longrightarrow> ?R126 x s) \<and> (\<forall>xa xb. x = AsidPoolCap xa xb \<longrightarrow> ?R127 x xa xb s) \<and> (\<forall>xa xb. x = IOPortsCap xa xb \<longrightarrow> ?R128 x xa xb s) \<and> (x = IOSpaceMasterCap \<longrightarrow> ?R129 x s) \<and> (\<forall>xa. x = IOSpaceCap xa \<longrightarrow> ?R130 x xa s) \<and> (\<forall>xa. x = IOPageTableCap xa \<longrightarrow> ?R131 x xa s) \<and> (\<forall>xa. x = ZombieCap xa \<longrightarrow> ?R132 x xa s) \<and> (\<forall>xa. x = BoundNotificationCap xa \<longrightarrow> ?R133 x xa s)\<rbrace>
A total of 11 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s\<rbrakk> \<Longrightarrow> opt_cap pd_ref s \<noteq> None \<longrightarrow> (the (opt_cap pd_ref s) = NullCap \<longrightarrow> ?R107 (the (opt_cap pd_ref s)) s) \<and> (\<forall>x xa xb. the (opt_cap pd_ref s) = UntypedCap x xa xb \<longrightarrow> ?R108 (the (opt_cap pd_ref s)) x xa xb s) \<and> (\<forall>x xa xb. the (opt_cap pd_ref s) = EndpointCap x xa xb \<longrightarrow> ?R109 (the (opt_cap pd_ref s)) x xa xb s) \<and> (\<forall>x xa xb. the (opt_cap pd_ref s) = NotificationCap x xa xb \<longrightarrow> ?R110 (the (opt_cap pd_ref s)) x xa xb s) \<and> (\<forall>x xa. the (opt_cap pd_ref s) = ReplyCap x xa \<longrightarrow> ?R111 (the (opt_cap pd_ref s)) x xa s) \<and> (\<forall>x. the (opt_cap pd_ref s) = MasterReplyCap x \<longrightarrow> ?R112 (the (opt_cap pd_ref s)) x s) \<and> (\<forall>x xa xb xc. the (opt_cap pd_ref s) = CNodeCap x xa xb xc \<longrightarrow> ?R113 (the (opt_cap pd_ref s)) x xa xb xc s) \<and> (\<forall>x. the (opt_cap pd_ref s) = TcbCap x \<longrightarrow> ?R114 (the (opt_cap pd_ref s)) x s) \<and> (the (opt_cap pd_ref s) = DomainCap \<longrightarrow> ?R115 (the (opt_cap pd_ref s)) s) \<and> (\<forall>x xa xb xc xd xe. the (opt_cap pd_ref s) = PendingSyncSendCap x xa xb xc xd xe \<longrightarrow> ?R116 (the (opt_cap pd_ref s)) x xa xb xc xd xe s) \<and> (\<forall>x xa xb. the (opt_cap pd_ref s) = PendingSyncRecvCap x xa xb \<longrightarrow> ?R117 (the (opt_cap pd_ref s)) x xa xb s) \<and> (\<forall>x. the (opt_cap pd_ref s) = PendingNtfnRecvCap x \<longrightarrow> ?R118 (the (opt_cap pd_ref s)) x s) \<and> (the (opt_cap pd_ref s) = RestartCap \<longrightarrow> ?R119 (the (opt_cap pd_ref s)) s) \<and> (the (opt_cap pd_ref s) = RunningCap \<longrightarrow> ?R120 (the (opt_cap pd_ref s)) s) \<and> (the (opt_cap pd_ref s) = IrqControlCap \<longrightarrow> ?R121 (the (opt_cap pd_ref s)) s) \<and> (\<forall>x. the (opt_cap pd_ref s) = IrqHandlerCap x \<longrightarrow> ?R122 (the (opt_cap pd_ref s)) x s) \<and> (\<forall>x xa xb xc xd xe. the (opt_cap pd_ref s) = FrameCap x xa xb xc xd xe \<longrightarrow> ?R123 (the (opt_cap pd_ref s)) x xa xb xc xd xe s) \<and> (\<forall>x xa xb. the (opt_cap pd_ref s) = PageTableCap x xa xb \<longrightarrow> ?R124 (the (opt_cap pd_ref s)) x xa xb s) \<and> (\<forall>x xa xb. the (opt_cap pd_ref s) = PageDirectoryCap x xa xb \<longrightarrow> (cdl.lift (pd_ref \<mapsto>c - \<and>* (pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<longrightarrow>* (p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)) and K (x = pd)) s \<and> K (x = pd) s) \<and> (the (opt_cap pd_ref s) = AsidControlCap \<longrightarrow> True) \<and> (\<forall>x xa. the (opt_cap pd_ref s) = AsidPoolCap x xa \<longrightarrow> True) \<and> (\<forall>x xa. the (opt_cap pd_ref s) = IOPortsCap x xa \<longrightarrow> True) \<and> (the (opt_cap pd_ref s) = IOSpaceMasterCap \<longrightarrow> True) \<and> (\<forall>x. the (opt_cap pd_ref s) = IOSpaceCap x \<longrightarrow> True) \<and> (\<forall>x. the (opt_cap pd_ref s) = IOPageTableCap x \<longrightarrow> True) \<and> (\<forall>x. the (opt_cap pd_ref s) = ZombieCap x \<longrightarrow> True) \<and> (\<forall>x. the (opt_cap pd_ref s) = BoundNotificationCap x \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some y\<rbrakk> \<Longrightarrow> (y = NullCap \<longrightarrow> ?R107 NullCap s) \<and> (\<forall>x xa xb. y = UntypedCap x xa xb \<longrightarrow> ?R108 (UntypedCap x xa xb) x xa xb s) \<and> (\<forall>x xa xb. y = EndpointCap x xa xb \<longrightarrow> ?R109 (EndpointCap x xa xb) x xa xb s) \<and> (\<forall>x xa xb. y = NotificationCap x xa xb \<longrightarrow> ?R110 (NotificationCap x xa xb) x xa xb s) \<and> (\<forall>x xa. y = ReplyCap x xa \<longrightarrow> ?R111 (ReplyCap x xa) x xa s) \<and> (\<forall>x. y = MasterReplyCap x \<longrightarrow> ?R112 (MasterReplyCap x) x s) \<and> (\<forall>x xa xb xc. y = CNodeCap x xa xb xc \<longrightarrow> ?R113 (CNodeCap x xa xb xc) x xa xb xc s) \<and> (\<forall>x. y = TcbCap x \<longrightarrow> ?R114 (TcbCap x) x s) \<and> (y = DomainCap \<longrightarrow> ?R115 DomainCap s) \<and> (\<forall>x xa xb xc xd xe. y = PendingSyncSendCap x xa xb xc xd xe \<longrightarrow> ?R116 (PendingSyncSendCap x xa xb xc xd xe) x xa xb xc xd xe s) \<and> (\<forall>x xa xb. y = PendingSyncRecvCap x xa xb \<longrightarrow> ?R117 (PendingSyncRecvCap x xa xb) x xa xb s) \<and> (\<forall>x. y = PendingNtfnRecvCap x \<longrightarrow> ?R118 (PendingNtfnRecvCap x) x s) \<and> (y = RestartCap \<longrightarrow> ?R119 RestartCap s) \<and> (y = RunningCap \<longrightarrow> ?R120 RunningCap s) \<and> (y = IrqControlCap \<longrightarrow> ?R121 IrqControlCap s) \<and> (\<forall>x. y = IrqHandlerCap x \<longrightarrow> ?R122 (IrqHandlerCap x) x s) \<and> (\<forall>x xa xb xc xd xe. y = FrameCap x xa xb xc xd xe \<longrightarrow> ?R123 (FrameCap x xa xb xc xd xe) x xa xb xc xd xe s) \<and> (\<forall>x xa xb. y = PageTableCap x xa xb \<longrightarrow> ?R124 (PageTableCap x xa xb) x xa xb s) \<and> (\<forall>x. (\<exists>xa xb. y = PageDirectoryCap x xa xb) \<longrightarrow> cdl.lift (pd_ref \<mapsto>c - \<and>* (pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<longrightarrow>* (p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)) s \<and> x = pd) proof (prove)
goal (2 subgoals):
 1. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> cdl.lift (pd_ref \<mapsto>c - \<and>* (pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<longrightarrow>* (p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)) s
 2. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> x = pd proof (prove)
goal (3 subgoals):
 1. \<And>s y x xa xb. \<lbrakk>opt_cap pd_ref s = Some (PageDirectoryCap x xa xb); off < 2 ^ asid_low_bits\<rbrakk> \<Longrightarrow> ?a445 s y x xa xb \<in> {off. off < 2 ^ asid_low_bits}
 2. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {?a445 s y x xa xb} \<union> {?a445 s y x xa xb}. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> cdl.lift (pd_ref \<mapsto>c - \<and>* (pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<longrightarrow>* (p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)) s
 3. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> x = pd proof (prove)
goal (2 subgoals):
 1. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off} \<union> {off}. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> cdl.lift (pd_ref \<mapsto>c - \<and>* (pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<longrightarrow>* (p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)) s
 2. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> x = pd proof (prove)
goal (5 subgoals):
 1. \<And>s y x xa xb. \<lbrakk>opt_cap pd_ref s = Some (PageDirectoryCap x xa xb); off < 2 ^ asid_low_bits\<rbrakk> \<Longrightarrow> finite ({off. off < 2 ^ asid_low_bits} - {off})
 2. \<And>s y x xa xb. \<lbrakk>opt_cap pd_ref s = Some (PageDirectoryCap x xa xb); off < 2 ^ asid_low_bits\<rbrakk> \<Longrightarrow> finite {off}
 3. \<And>s y x xa xb. \<lbrakk>opt_cap pd_ref s = Some (PageDirectoryCap x xa xb); off < 2 ^ asid_low_bits\<rbrakk> \<Longrightarrow> ({off. off < 2 ^ asid_low_bits} - {off}) \<inter> {off} = {}
 4. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* ((SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* (SETSEPCONJ off:{off}. (p, off) \<mapsto>c -)) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> cdl.lift (pd_ref \<mapsto>c - \<and>* (pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<longrightarrow>* (p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)) s
 5. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> x = pd proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* ((SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> cdl.lift (pd_ref \<mapsto>c - \<and>* (pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<longrightarrow>* (p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)) s
 2. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> x = pd proof (prove)
goal (2 subgoals):
 1. \<And>s x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* (p, off) \<mapsto>c - \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> cdl.lift (pd_ref \<mapsto>c - \<and>* (pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<longrightarrow>* (p, off) \<mapsto>c - \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* pd_ref \<mapsto>c PageDirectoryCap x Real (Some asid) \<and>* (SETSEPCONJ off:{off. off < 2 ^ asid_low_bits} - {off}. (p, off) \<mapsto>c -) \<and>* R)) s
 2. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> x = pd proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; cdl.lift ((cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* R) s; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb)\<rbrakk> \<Longrightarrow> x = pd proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb); cdl.lift (pd_ref \<mapsto>c PageDirectoryCap pd Real asid' \<and>* (cur_thread, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s\<rbrakk> \<Longrightarrow> x = pd proof (prove)
goal (1 subgoal):
 1. \<And>s y x xa xb. \<lbrakk>off < 2 ^ asid_low_bits; opt_cap pd_ref s = Some (PageDirectoryCap x xa xb); \<exists>cap'. opt_cap pd_ref s = Some cap' \<and> reset_cap_asid cap' = reset_cap_asid (PageDirectoryCap pd Real asid')\<rbrakk> \<Longrightarrow> x = pd proof (prove)
goal:
No subgoals!