theory Arch_DP

lemma seL4_ASIDPool_Assign_wp:
  assumes misc:
  "cap_object cnode_cap = cnode_id" "is_cnode_cap cnode_cap"
  "offset sel4_page_directory root_size = pd_offset"
  "offset sel4_asid root_size = asid_offset"
  and sz: "one_lvl_lookup cnode_cap word_bits root_size"
          "guard_equal cnode_cap sel4_page_directory word_bits"
          "guard_equal cnode_cap sel4_asid word_bits"
  shows
  "\<lbrace>
  \<guillemotleft> (root_tcb_id,tcb_pending_op_slot) \<mapsto>c RunningCap
  \<and>* root_tcb_id \<mapsto>f Tcb tcb
  \<and>* (cnode_id,asid_offset) \<mapsto>c AsidPoolCap p base
  \<and>* (cnode_id,pd_offset) \<mapsto>c PageDirectoryCap pd Real None
  \<and>*  (\<And>* off\<in>{off. off < 2 ^ asid_low_bits}. (p, off) \<mapsto>c -)
  \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size)
  \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap
  \<and>* R \<guillemotright>\<rbrace>
  seL4_ASIDPool_Assign sel4_asid sel4_page_directory
  \<lbrace>\<lambda>_. \<guillemotleft> (root_tcb_id,tcb_pending_op_slot) \<mapsto>c RunningCap
  \<and>* root_tcb_id \<mapsto>f Tcb tcb
  \<and>* (cnode_id,asid_offset) \<mapsto>c AsidPoolCap p base
  \<and>* (cnode_id,pd_offset) \<mapsto>c PageDirectoryCap pd Real None
  \<and>* (\<And>* off\<in>{off. off < 2 ^ asid_low_bits}. (p, off) \<mapsto>c -)
  \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size)
  \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap
  \<and>* R\<guillemotright> \<rbrace>" apply (simp add:seL4_ASIDPool_Assign_def sep_state_projection2_def
    | wp do_kernel_op_wp)+ apply (rule call_kernel_with_intent_allow_error_helper[where check = True and Perror = \<top>,simplified]) apply fastforce apply (rule set_cap_wp) apply (wp+)[4] apply (rule_tac P = "\<exists>x. x < 2 ^ asid_low_bits
              \<and> iv =  (InvokeAsidPool (Assign (base, x) (cnode_id,pd_offset) (p, x)))"
              in hoare_gen_asmEx) apply clarsimp apply wp apply (rule hoare_strengthen_post[OF invoke_asid_pool_wp[where pd = pd
              and cur_thread = root_tcb_id
              and R="(cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>*
                      root_tcb_id \<mapsto>f Tcb tcb \<and>*
                      cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>*
                      (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R"]]) apply simp apply (rule conjI,sep_solve) apply (subst (asm) sep_map_c_asid_simp) apply sep_solve apply (wp hoare_vcg_conj_lift) apply (rule hoare_strengthen_post[OF set_cap_wp]) apply assumption apply wp apply (subst sep_map_c_asid_simp) apply (wp hoare_vcg_conj_lift) apply simp apply (rule_tac P = "\<exists>asid. cs = [(PageDirectoryCap pd Real asid,(cnode_id,pd_offset))]" in hoare_gen_asmE) apply clarsimp apply (rule decode_invocation_asid_pool_assign) apply (clarsimp simp:conj_comms lookup_extra_caps_def mapME_singleton) apply (rule wp_no_exception_seq) apply wp apply (rule lookup_cap_and_slot_rvu[where r = root_size
           and cap' = "PageDirectoryCap pd Real None"]) apply (rule hoare_pre) apply (rule lookup_cap_and_slot_rvu[where r = root_size
           and cap' = "AsidPoolCap p base"]) apply (erule_tac Q="cdl_current_domain s = minBound" in conjE, assumption) apply clarsimp apply (wp update_thread_intent_update hoare_vcg_all_lift
      hoare_vcg_imp_lift) apply clarsimp defer apply clarsimp using misc sz apply (intro conjI impI allI, simp_all add: reset_cap_asid_simps2) apply sep_solve apply sep_solve apply (clarsimp simp:user_pointer_at_def Let_def word_bits_def sep_conj_assoc) apply (sep_solve) apply (clarsimp dest!:reset_cap_asid_simps2 simp: ep_related_cap_def) apply (clarsimp simp:user_pointer_at_def Let_def word_bits_def sep_conj_assoc) apply (sep_solve) apply (sep_solve) apply clarsimp apply (drule_tac x = "AsidPoolCap p base" in spec) apply clarsimp apply (erule impE) apply (rule_tac x = "PageDirectoryCap pd Real None" in exI) apply simp apply clarsimp apply (drule  use_sep_true_for_sep_map_c) apply simp apply sep_solve done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Separation_SD.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)\<rbrace> seL4_ASIDPool_Assign sel4_asid sel4_page_directory \<lbrace>\<lambda>_. Separation_SD.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P1\<rbrace> call_kernel_with_intent \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> True \<lbrace>\<lambda>_. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)\<rbrace>
 2. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> (?P1 \<circ> kernel_state) s proof (prove)
goal (14 subgoals):
 1. cdl_intent_op \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> = Some ?intent_op8 \<and> cdl_intent_cap \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> = ?intent_cptr8 \<and> cdl_intent_extras \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> = ?intent_extra8
 2. \<lbrace>?R8\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>_. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)\<rbrace>
 3. \<lbrace>?Ra8\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>_. ?R8\<rbrace>
 4. \<lbrace>\<lambda>_. True\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrace>?Rb8\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>_. ?Ra8\<rbrace>
 6. \<lbrace>\<lambda>_. True\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>_ _. True\<rbrace>
 7. \<And>iv. \<lbrace>?PIV8 iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> ?Rb8 s\<rbrace>, \<lbrace>\<lambda>_ s. tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some ?intent_op8 \<and> cdl_intent_cap (cdl_tcb_intent tcb) = cdl_intent_cap \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> cdl_intent_extras (cdl_tcb_intent tcb) = cdl_intent_extras \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> no_pending s \<and> ?Pd2.8 s\<rbrace>
 8. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. ?PIV8 iv\<rbrace>
 9. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs ?intent_op8 \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 10. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id ?intent_extra8 \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<lbrace>?R8\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>_. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)\<rbrace>
 2. \<lbrace>?Ra8\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>_. ?R8\<rbrace>
 3. \<lbrace>\<lambda>_. True\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Rb8\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>_. ?Ra8\<rbrace>
 5. \<lbrace>\<lambda>_. True\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>iv. \<lbrace>?PIV8 iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> ?Rb8 s\<rbrace>, \<lbrace>\<lambda>_ s. tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some (AsidPoolIntent AsidPoolAssignIntent) \<and> cdl_intent_cap (cdl_tcb_intent tcb) = cdl_intent_cap \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> cdl_intent_extras (cdl_tcb_intent tcb) = cdl_intent_extras \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> no_pending s \<and> ?Pd2.8 s\<rbrace>
 7. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. ?PIV8 iv\<rbrace>
 8. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 9. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 10. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<lbrace>?Ra8\<rbrace> mark_tcb_intent_error root_tcb_id False \<lbrace>\<lambda>_. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)\<rbrace>
 2. \<lbrace>\<lambda>_. True\<rbrace> mark_tcb_intent_error root_tcb_id True \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Rb8\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>_. ?Ra8\<rbrace>
 4. \<lbrace>\<lambda>_. True\<rbrace> corrupt_ipc_buffer root_tcb_id True \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>iv. \<lbrace>?PIV8 iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> ?Rb8 s\<rbrace>, \<lbrace>\<lambda>_ s. tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some (AsidPoolIntent AsidPoolAssignIntent) \<and> cdl_intent_cap (cdl_tcb_intent tcb) = cdl_intent_cap \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> cdl_intent_extras (cdl_tcb_intent tcb) = cdl_intent_extras \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> no_pending s \<and> ?Pd2.8 s\<rbrace>
 6. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. ?PIV8 iv\<rbrace>
 7. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 8. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 9. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 10. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
A total of 12 subgoals... proof (prove)
goal (8 subgoals):
 1. \<And>iv. \<lbrace>?PIV8 iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrace>, \<lbrace>\<lambda>_ s. tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some (AsidPoolIntent AsidPoolAssignIntent) \<and> cdl_intent_cap (cdl_tcb_intent tcb) = cdl_intent_cap \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> cdl_intent_extras (cdl_tcb_intent tcb) = cdl_intent_extras \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> no_pending s \<and> ?Pd2.8 s\<rbrace>
 2. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. ?PIV8 iv\<rbrace>
 3. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 5. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 7. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 8. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (8 subgoals):
 1. \<And>iv. \<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)) \<Longrightarrow> \<lbrace>?P'51 iv\<rbrace> perform_invocation True True iv \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrace>, \<lbrace>\<lambda>_ s. tcb_at' (\<lambda>tcb. cdl_intent_op (cdl_tcb_intent tcb) = Some (AsidPoolIntent AsidPoolAssignIntent) \<and> cdl_intent_cap (cdl_tcb_intent tcb) = cdl_intent_cap \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> cdl_intent_extras (cdl_tcb_intent tcb) = cdl_intent_extras \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> \<not> cdl_intent_error (cdl_tcb_intent tcb)) root_tcb_id s \<and> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> no_pending s \<and> ?Pd2.8 s\<rbrace>
 2. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. ?P'51 iv and K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 3. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 5. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 7. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 8. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (8 subgoals):
 1. \<And>x. x < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?P'51 (InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace> invoke_asid_pool (Assign (base, x) (cnode_id, pd_offset) (p, x)) \<lbrace>\<lambda>rv s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrace>
 2. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. ?P'51 iv and K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 3. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 5. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 7. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 8. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (8 subgoals):
 1. \<And>x. x < 2 ^ asid_low_bits \<Longrightarrow> \<lbrace>?P'69 (InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace> invoke_asid_pool (Assign (base, x) (cnode_id, pd_offset) (p, x)) \<lbrace>\<lambda>rv s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrace>
 2. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. (\<lambda>a. cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> ?P'69 iv a) and K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 3. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 5. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 7. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 8. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (9 subgoals):
 1. \<And>x. x < 2 ^ asid_low_bits \<Longrightarrow> x < 2 ^ asid_low_bits
 2. \<And>x rv s. \<lbrakk>x < 2 ^ asid_low_bits; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (Some (base, x)) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s
 3. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. (\<lambda>a. cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (?asid'78 iv) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) a) and K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 4. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 5. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 6. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 7. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 8. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 9. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (8 subgoals):
 1. \<And>x rv s. \<lbrakk>x < 2 ^ asid_low_bits; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (Some (base, x)) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s
 2. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. (\<lambda>a. cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (?asid'78 iv) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) a) and K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 3. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 5. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 7. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 8. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (8 subgoals):
 1. \<And>x rv s. \<lbrakk>x < 2 ^ asid_low_bits; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (Some (base, x)) \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s
 2. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. (\<lambda>a. cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (?asid'78 iv) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) a) and K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 3. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 5. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 7. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 8. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (8 subgoals):
 1. \<And>x rv s. \<lbrakk>x < 2 ^ asid_low_bits; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s
 2. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. (\<lambda>a. cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (?asid'78 iv) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) a) and K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 3. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 5. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 7. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 8. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (7 subgoals):
 1. \<And>iv. \<lbrace>?Ps8 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>_. (\<lambda>a. cdl_current_thread a = Some root_tcb_id \<and> cdl_current_domain a = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (?asid'78 iv) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) a) and K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 2. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>?Ps8\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 3. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 4. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 6. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 7. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (8 subgoals):
 1. \<And>iv. \<lbrace>?P'146 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (?asid'78 iv) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)\<rbrace>
 2. \<And>iv. \<lbrace>?P'143 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 3. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>iv s. (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> ?P'146 iv s) \<and> ?P'143 iv s\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 5. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 7. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 8. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (8 subgoals):
 1. \<And>iv rv s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* ?R150 iv) s \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RestartCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (?asid'78 iv) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s
 2. \<And>iv. \<lbrace>?P'143 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 3. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>iv s. (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* ?R150 iv) s) \<and> ?P'143 iv s\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 4. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 5. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 6. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 7. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 8. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (7 subgoals):
 1. \<And>iv. \<lbrace>?P'143 iv\<rbrace> set_cap (root_tcb_id, tcb_pending_op_slot) RestartCap \<lbrace>\<lambda>rv. K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>
 2. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>iv s. (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (?asid'152 iv) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> ?P'143 iv s\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 3. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 4. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 5. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 6. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 7. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (6 subgoals):
 1. \<And>c ref cs. \<lbrace>?Pd8 cs c ref\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>iv s. (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real (?asid'152 iv) \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x))) s\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 2. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd8 xa (fst uu_) (snd uu_)\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 3. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 5. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 6. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (6 subgoals):
 1. \<And>c ref cs. \<lbrace>?Pd158 c c ref ref cs cs\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>iv s. (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> K (\<exists>x<2 ^ asid_low_bits. iv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x))) s\<rbrace>, \<lbrace>\<lambda>_ s. cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s\<rbrace>
 2. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa. ?Pd158 (fst uu_) (fst uu_) (snd uu_) (snd uu_) xa xa\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 3. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 5. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 6. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (6 subgoals):
 1. \<And>c ref cs. \<lbrace>?P'181 c c ref ref cs cs\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>rv. K (\<exists>x<2 ^ asid_low_bits. rv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x)))\<rbrace>, -
 2. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa s. (((\<lambda>a. cdl_current_thread a = Some root_tcb_id) and (\<lambda>a. cdl_current_thread a = Some root_tcb_id)) s \<and> ((\<lambda>a. cdl_current_domain a = minBound) and (\<lambda>a. cdl_current_domain a = minBound)) s \<and> (cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) and cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True))) s) \<and> (((\<lambda>a. cdl_current_thread a = Some root_tcb_id) and (\<lambda>a. cdl_current_thread a = Some root_tcb_id)) s \<and> ((\<lambda>a. cdl_current_domain a = minBound) and (\<lambda>a. cdl_current_domain a = minBound)) s \<and> (cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) and cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)) s) \<and> ?P'181 (fst uu_) (fst uu_) (snd uu_) (snd uu_) xa xa s\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 3. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 5. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 6. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (6 subgoals):
 1. \<And>c ref cs. \<lbrace>?P'181 c c ref ref cs cs\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>rv s. \<exists>x<2 ^ asid_low_bits. rv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x))\<rbrace>, -
 2. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa s. (((\<lambda>a. cdl_current_thread a = Some root_tcb_id) and (\<lambda>a. cdl_current_thread a = Some root_tcb_id)) s \<and> ((\<lambda>a. cdl_current_domain a = minBound) and (\<lambda>a. cdl_current_domain a = minBound)) s \<and> (cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) and cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True))) s) \<and> (((\<lambda>a. cdl_current_thread a = Some root_tcb_id) and (\<lambda>a. cdl_current_thread a = Some root_tcb_id)) s \<and> ((\<lambda>a. cdl_current_domain a = minBound) and (\<lambda>a. cdl_current_domain a = minBound)) s \<and> (cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) and cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)) s) \<and> ?P'181 (fst uu_) (fst uu_) (snd uu_) (snd uu_) xa xa s\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 3. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 5. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 6. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (6 subgoals):
 1. \<And>c ref cs. \<exists>asid. cs = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)] \<Longrightarrow> \<lbrace>?P'208 c c ref ref cs cs\<rbrace> decode_invocation c ref cs (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>rv s. \<exists>x<2 ^ asid_low_bits. rv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x))\<rbrace>, -
 2. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa s. (((\<lambda>a. cdl_current_thread a = Some root_tcb_id) and (\<lambda>a. cdl_current_thread a = Some root_tcb_id)) s \<and> ((\<lambda>a. cdl_current_domain a = minBound) and (\<lambda>a. cdl_current_domain a = minBound)) s \<and> (cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) and cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True))) s) \<and> (((\<lambda>a. cdl_current_thread a = Some root_tcb_id) and (\<lambda>a. cdl_current_thread a = Some root_tcb_id)) s \<and> ((\<lambda>a. cdl_current_domain a = minBound) and (\<lambda>a. cdl_current_domain a = minBound)) s \<and> (cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) and cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)) s) \<and> (?P'208 (fst uu_) (fst uu_) (snd uu_) (snd uu_) xa xa and K (\<exists>asid. xa = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)])) s\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 3. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 5. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 6. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (6 subgoals):
 1. \<And>c a b asid. \<lbrace>?P'208 c c (a, b) (a, b) [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)] [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]\<rbrace> decode_invocation c (a, b) [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)] (AsidPoolIntent AsidPoolAssignIntent) \<lbrace>\<lambda>rv s. \<exists>x<2 ^ asid_low_bits. rv = InvokeAsidPool (Assign (base, x) (cnode_id, pd_offset) (p, x))\<rbrace>, -
 2. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa s. (((\<lambda>a. cdl_current_thread a = Some root_tcb_id) and (\<lambda>a. cdl_current_thread a = Some root_tcb_id)) s \<and> ((\<lambda>a. cdl_current_domain a = minBound) and (\<lambda>a. cdl_current_domain a = minBound)) s \<and> (cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) and cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True))) s) \<and> (((\<lambda>a. cdl_current_thread a = Some root_tcb_id) and (\<lambda>a. cdl_current_thread a = Some root_tcb_id)) s \<and> ((\<lambda>a. cdl_current_domain a = minBound) and (\<lambda>a. cdl_current_domain a = minBound)) s \<and> (cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) and cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)) s) \<and> (?P'208 (fst uu_) (fst uu_) (snd uu_) (snd uu_) xa xa and K (\<exists>asid. xa = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)])) s\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 3. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 5. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 6. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (5 subgoals):
 1. \<And>uu_. \<lbrace>?Pd1.8 (fst uu_) (snd uu_)\<rbrace> lookup_extra_caps root_tcb_id [sel4_page_directory] \<lbrace>\<lambda>xa s. (((\<lambda>a. cdl_current_thread a = Some root_tcb_id) and (\<lambda>a. cdl_current_thread a = Some root_tcb_id)) s \<and> ((\<lambda>a. cdl_current_domain a = minBound) and (\<lambda>a. cdl_current_domain a = minBound)) s \<and> (cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) and cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True))) s) \<and> (((\<lambda>a. cdl_current_thread a = Some root_tcb_id) and (\<lambda>a. cdl_current_thread a = Some root_tcb_id)) s \<and> ((\<lambda>a. cdl_current_domain a = minBound) and (\<lambda>a. cdl_current_domain a = minBound)) s \<and> (cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) and cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R)) s) \<and> ((\<lambda>a. fst uu_ = AsidPoolCap p base) and K (\<exists>asid. xa = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)])) s\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 2. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 4. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 5. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (5 subgoals):
 1. \<And>a aa b. \<lbrace>?Pd1.8 a (aa, b)\<rbrace> doE x <- lookup_cap_and_slot root_tcb_id sel4_page_directory;
returnOk [x]
odE \<lbrace>\<lambda>xa s. cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> a = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. xa = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 2. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 4. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 5. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (6 subgoals):
 1. \<And>a aa b uu_. \<lbrace>?P'216 a aa b uu_\<rbrace> returnOk [uu_] \<lbrace>\<lambda>xa s. cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> a = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. xa = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 2. \<And>a aa b. \<lbrace>?Pd1.8 a (aa, b)\<rbrace> lookup_cap_and_slot root_tcb_id sel4_page_directory \<lbrace>?P'216 a aa b\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 3. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 4. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 5. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 6. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (5 subgoals):
 1. \<And>a aa b. \<lbrace>?Pd1.8 a (aa, b)\<rbrace> lookup_cap_and_slot root_tcb_id sel4_page_directory \<lbrace>\<lambda>uu_ b. cdl_current_domain b = minBound \<and> cdl_current_thread b = Some root_tcb_id \<and> a = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) b \<and> (\<exists>asid. [uu_] = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) b\<rbrace>, \<lbrace>\<lambda>_ s. False\<rbrace>
 2. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ?Pd1.8 (fst uu_) (snd uu_) s \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 3. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 4. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 5. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Pd2.8\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ((\<forall>c. reset_cap_asid c = reset_cap_asid (PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> fst uu_ = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. [(c, cap_object (?cap232 (fst uu_) (snd uu_)), offset sel4_page_directory root_size)] = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 (fst uu_) (snd uu_) \<and>* \<box> (root_size, word_bits) : ?cap230 (fst uu_) (snd uu_) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 (fst uu_) (snd uu_)) s) \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 3. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 4. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s
flex-flex pairs:
\<lambda>a aa b. ?cap230 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap232 a (aa, b)
\<lambda>a aa b. ?cap230 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap231 a (aa, b) proof (prove)
goal (5 subgoals):
 1. \<lbrace>?Q233\<rbrace> lookup_cap_and_slot root_tcb_id sel4_asid \<lbrace>\<lambda>uu_ s. ((\<forall>c. reset_cap_asid c = reset_cap_asid (PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> fst uu_ = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. [(c, cap_object (?cap232 (fst uu_) (snd uu_)), offset sel4_page_directory root_size)] = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 (fst uu_) (snd uu_) \<and>* \<box> (root_size, word_bits) : ?cap230 (fst uu_) (snd uu_) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 (fst uu_) (snd uu_)) s) \<and> \<not> ep_related_cap (fst uu_)\<rbrace>, \<lbrace>\<lambda>y s. False\<rbrace>
 2. \<And>s. ?Pd2.8 s \<Longrightarrow> ?Q233 s
 3. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 4. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 5. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s
flex-flex pairs:
\<lambda>a aa b. ?cap232 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b)
\<lambda>a aa b. ?cap231 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b) proof (prove)
goal (4 subgoals):
 1. \<And>s. ?Pd2.8 s \<Longrightarrow> (\<forall>c. reset_cap_asid c = reset_cap_asid (AsidPoolCap p base) \<longrightarrow> ((\<forall>ca. reset_cap_asid ca = reset_cap_asid (PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> fst (c, cap_object ?cap236, offset sel4_asid root_size) = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. [(ca, cap_object (?cap232 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size))), offset sel4_page_directory root_size)] = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size)) \<and>* \<box> (root_size, word_bits) : ?cap230 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size)) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size))) s) \<and> \<not> ep_related_cap (fst (c, cap_object ?cap236, offset sel4_asid root_size))) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s
 2. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv. ?Pd2.8\<rbrace>
 3. \<And>s. ?Pd2.8 s \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 4. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s
flex-flex pairs:
\<lambda>a aa b. ?cap232 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b)
\<lambda>a aa b. ?cap231 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b) proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv s. ((\<forall>c. reset_cap_asid c = reset_cap_asid (AsidPoolCap p base) \<longrightarrow> ((\<forall>ca. reset_cap_asid ca = reset_cap_asid (PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> fst (c, cap_object ?cap236, offset sel4_asid root_size) = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. [(ca, cap_object (?cap232 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size))), offset sel4_page_directory root_size)] = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size)) \<and>* \<box> (root_size, word_bits) : ?cap230 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size)) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size))) s) \<and> \<not> ep_related_cap (fst (c, cap_object ?cap236, offset sel4_asid root_size))) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s) \<and> cdl_current_domain s = minBound\<rbrace>
 2. \<And>s. ((\<forall>c. reset_cap_asid c = reset_cap_asid (AsidPoolCap p base) \<longrightarrow> ((\<forall>ca. reset_cap_asid ca = reset_cap_asid (PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> fst (c, cap_object ?cap236, offset sel4_asid root_size) = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. [(ca, cap_object (?cap232 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size))), offset sel4_page_directory root_size)] = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size)) \<and>* \<box> (root_size, word_bits) : ?cap230 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size)) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size))) s) \<and> \<not> ep_related_cap (fst (c, cap_object ?cap236, offset sel4_asid root_size))) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s) \<and> cdl_current_domain s = minBound \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 3. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s
flex-flex pairs:
\<lambda>a aa b. ?cap232 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b)
\<lambda>a aa b. ?cap231 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b) proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P8\<rbrace> update_thread root_tcb_id (cdl_tcb_intent_update (\<lambda>x. \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr>)) \<lbrace>\<lambda>rv s. (\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> (\<forall>ca. reset_cap_asid ca = PageDirectoryCap pd Real None \<longrightarrow> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> c = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. ca = PageDirectoryCap pd Real asid) \<and> cap_object (?cap232 c (cap_object ?cap236, offset sel4_asid root_size)) = cnode_id \<and> offset sel4_page_directory root_size = pd_offset \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 c (cap_object ?cap236, offset sel4_asid root_size) \<and>* \<box> (root_size, word_bits) : ?cap230 c (cap_object ?cap236, offset sel4_asid root_size) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 c (cap_object ?cap236, offset sel4_asid root_size)) s \<and> \<not> ep_related_cap c) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s \<and> cdl_current_domain s = minBound\<rbrace>
 2. \<And>s. ((\<forall>c. reset_cap_asid c = reset_cap_asid (AsidPoolCap p base) \<longrightarrow> ((\<forall>ca. reset_cap_asid ca = reset_cap_asid (PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> fst (c, cap_object ?cap236, offset sel4_asid root_size) = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. [(ca, cap_object (?cap232 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size))), offset sel4_page_directory root_size)] = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size)) \<and>* \<box> (root_size, word_bits) : ?cap230 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size)) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size))) s) \<and> \<not> ep_related_cap (fst (c, cap_object ?cap236, offset sel4_asid root_size))) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s) \<and> cdl_current_domain s = minBound \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 3. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> ?P8 s) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s
flex-flex pairs:
\<lambda>a aa b. ?cap232 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b)
\<lambda>a aa b. ?cap231 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b) proof (prove)
goal (2 subgoals):
 1. \<And>s. ((\<forall>c. reset_cap_asid c = reset_cap_asid (AsidPoolCap p base) \<longrightarrow> ((\<forall>ca. reset_cap_asid ca = reset_cap_asid (PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> fst (c, cap_object ?cap236, offset sel4_asid root_size) = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. [(ca, cap_object (?cap232 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size))), offset sel4_page_directory root_size)] = [(PageDirectoryCap pd Real asid, cnode_id, pd_offset)]) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size)) \<and>* \<box> (root_size, word_bits) : ?cap230 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size)) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 (fst (c, cap_object ?cap236, offset sel4_asid root_size)) (snd (c, cap_object ?cap236, offset sel4_asid root_size))) s) \<and> \<not> ep_related_cap (fst (c, cap_object ?cap236, offset sel4_asid root_size))) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s) \<and> cdl_current_domain s = minBound \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 2. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> (\<forall>x. reset_cap_asid x \<noteq> AsidPoolCap p base \<or> (\<forall>xa. reset_cap_asid xa \<noteq> PageDirectoryCap pd Real None \<or> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> x = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. xa = PageDirectoryCap pd Real asid) \<and> cap_object (?cap232 x (cap_object ?cap236, offset sel4_asid root_size)) = cnode_id \<and> offset sel4_page_directory root_size = pd_offset \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 x (cap_object ?cap236, offset sel4_asid root_size) \<and>* \<box> (root_size, word_bits) : ?cap230 x (cap_object ?cap236, offset sel4_asid root_size) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 x (cap_object ?cap236, offset sel4_asid root_size)) s \<and> \<not> ep_related_cap x) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s \<and> cdl_current_domain s = minBound) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s
flex-flex pairs:
\<lambda>a aa b. ?cap232 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b)
\<lambda>a aa b. ?cap231 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> (\<forall>ca. reset_cap_asid ca = PageDirectoryCap pd Real None \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> c = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. ca = PageDirectoryCap pd Real asid) \<and> cap_object (?cap232 c (cap_object ?cap236, offset sel4_asid root_size)) = cnode_id \<and> offset sel4_page_directory root_size = pd_offset \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 c (cap_object ?cap236, offset sel4_asid root_size) \<and>* \<box> (root_size, word_bits) : ?cap230 c (cap_object ?cap236, offset sel4_asid root_size) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 c (cap_object ?cap236, offset sel4_asid root_size)) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
 2. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> (\<forall>x. reset_cap_asid x \<noteq> AsidPoolCap p base \<or> (\<forall>xa. reset_cap_asid xa \<noteq> PageDirectoryCap pd Real None \<or> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> x = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. xa = PageDirectoryCap pd Real asid) \<and> cap_object (?cap232 x (cap_object ?cap236, offset sel4_asid root_size)) = cnode_id \<and> offset sel4_page_directory root_size = pd_offset \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 x (cap_object ?cap236, offset sel4_asid root_size) \<and>* \<box> (root_size, word_bits) : ?cap230 x (cap_object ?cap236, offset sel4_asid root_size) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 x (cap_object ?cap236, offset sel4_asid root_size)) s \<and> \<not> ep_related_cap x) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s \<and> cdl_current_domain s = minBound) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s
flex-flex pairs:
\<lambda>a aa b. ?cap232 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b)
\<lambda>a aa b. ?cap231 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b) proof (prove)
goal (2 subgoals):
 1. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> ((\<lambda>s. \<not> cdl_intent_error \<lparr>cdl_intent_op = Some (AsidPoolIntent AsidPoolAssignIntent), cdl_intent_error = False, cdl_intent_cap = sel4_asid, cdl_intent_extras = [sel4_page_directory], cdl_intent_recv_slot = None\<rparr> \<and> (cdl_current_thread s = Some root_tcb_id \<and> cdl_current_domain s = minBound \<longrightarrow> (\<forall>x. reset_cap_asid x \<noteq> AsidPoolCap p base \<or> (\<forall>xa. reset_cap_asid xa \<noteq> PageDirectoryCap pd Real None \<or> cdl_current_domain s = minBound \<and> cdl_current_thread s = Some root_tcb_id \<and> x = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. xa = PageDirectoryCap pd Real asid) \<and> cap_object (?cap232 x (cap_object ?cap236, offset sel4_asid root_size)) = cnode_id \<and> offset sel4_page_directory root_size = pd_offset \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 x (cap_object ?cap236, offset sel4_asid root_size) \<and>* \<box> (root_size, word_bits) : ?cap230 x (cap_object ?cap236, offset sel4_asid root_size) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 x (cap_object ?cap236, offset sel4_asid root_size)) s \<and> \<not> ep_related_cap x) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s \<and> cdl_current_domain s = minBound) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s) \<circ> kernel_state) s
 2. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> (\<forall>ca. reset_cap_asid ca = PageDirectoryCap pd Real None \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> c = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. ca = PageDirectoryCap pd Real asid) \<and> cap_object (?cap232 c (cap_object ?cap236, offset sel4_asid root_size)) = cnode_id \<and> offset sel4_page_directory root_size = pd_offset \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 c (cap_object ?cap236, offset sel4_asid root_size) \<and>* \<box> (root_size, word_bits) : ?cap230 c (cap_object ?cap236, offset sel4_asid root_size) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 c (cap_object ?cap236, offset sel4_asid root_size)) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
flex-flex pairs:
\<lambda>a aa b. ?cap232 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b)
\<lambda>a aa b. ?cap231 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b) proof (prove)
goal (2 subgoals):
 1. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> (cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound \<longrightarrow> (\<forall>x. reset_cap_asid x = AsidPoolCap p base \<longrightarrow> (\<forall>xa. reset_cap_asid xa = PageDirectoryCap pd Real None \<longrightarrow> x = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) (kernel_state s) \<and> (\<exists>asid. xa = PageDirectoryCap pd Real asid) \<and> cap_object (?cap232 x (cap_object ?cap236, offset sel4_asid root_size)) = cnode_id \<and> offset sel4_page_directory root_size = pd_offset \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s)) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 x (cap_object ?cap236, offset sel4_asid root_size) \<and>* \<box> (root_size, word_bits) : ?cap230 x (cap_object ?cap236, offset sel4_asid root_size) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 x (cap_object ?cap236, offset sel4_asid root_size)) (kernel_state s) \<and> \<not> ep_related_cap x) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) (kernel_state s)) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) (kernel_state s)
 2. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> (\<forall>ca. reset_cap_asid ca = PageDirectoryCap pd Real None \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> c = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. ca = PageDirectoryCap pd Real asid) \<and> cap_object (?cap232 c (cap_object ?cap236, offset sel4_asid root_size)) = cnode_id \<and> offset sel4_page_directory root_size = pd_offset \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 c (cap_object ?cap236, offset sel4_asid root_size) \<and>* \<box> (root_size, word_bits) : ?cap230 c (cap_object ?cap236, offset sel4_asid root_size) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 c (cap_object ?cap236, offset sel4_asid root_size)) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
flex-flex pairs:
\<lambda>a aa b. ?cap232 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b)
\<lambda>a aa b. ?cap231 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b) proof (prove)
using this:
cap_object cnode_cap = cnode_id
is_cnode_cap cnode_cap
offset sel4_page_directory root_size = pd_offset
offset sel4_asid root_size = asid_offset
one_lvl_lookup cnode_cap word_bits root_size
guard_equal cnode_cap sel4_page_directory word_bits
guard_equal cnode_cap sel4_asid word_bits

goal (2 subgoals):
 1. \<And>s. cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s) \<Longrightarrow> (cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound \<longrightarrow> (\<forall>x. reset_cap_asid x = AsidPoolCap p base \<longrightarrow> (\<forall>xa. reset_cap_asid xa = PageDirectoryCap pd Real None \<longrightarrow> x = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) (kernel_state s) \<and> (\<exists>asid. xa = PageDirectoryCap pd Real asid) \<and> cap_object (?cap232 x (cap_object ?cap236, offset sel4_asid root_size)) = cnode_id \<and> offset sel4_page_directory root_size = pd_offset \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s)) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 x (cap_object ?cap236, offset sel4_asid root_size) \<and>* \<box> (root_size, word_bits) : ?cap230 x (cap_object ?cap236, offset sel4_asid root_size) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 x (cap_object ?cap236, offset sel4_asid root_size)) (kernel_state s) \<and> \<not> ep_related_cap x) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) (kernel_state s)) \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) (kernel_state s)
 2. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> (\<forall>ca. reset_cap_asid ca = PageDirectoryCap pd Real None \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> c = AsidPoolCap p base \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> (\<exists>asid. ca = PageDirectoryCap pd Real asid) \<and> cap_object (?cap232 c (cap_object ?cap236, offset sel4_asid root_size)) = cnode_id \<and> offset sel4_page_directory root_size = pd_offset \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap231 c (cap_object ?cap236, offset sel4_asid root_size) \<and>* \<box> (root_size, word_bits) : ?cap230 c (cap_object ?cap236, offset sel4_asid root_size) sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 c (cap_object ?cap236, offset sel4_asid root_size)) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s
flex-flex pairs:
\<lambda>a aa b. ?cap232 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b)
\<lambda>a aa b. ?cap231 a (aa, b) \<equiv>\<^sup>? \<lambda>a aa b. ?cap230 a (aa, b) proof (prove)
goal (7 subgoals):
 1. \<And>s x xa. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; reset_cap_asid xa = PageDirectoryCap pd Real None; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) (kernel_state s)
 2. \<And>s x xa. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; reset_cap_asid xa = PageDirectoryCap pd Real None; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s)
 3. \<And>s x. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 x (cap_object ?cap236, asid_offset)) (kernel_state s)
 4. \<And>s x. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> \<not> ep_related_cap x
 5. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) (kernel_state s)
 6. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) (kernel_state s)
 7. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cap_object cnode_cap = cnode_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 c (cap_object ?cap236, asid_offset)) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s proof (prove)
goal (6 subgoals):
 1. \<And>s x xa. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; reset_cap_asid xa = PageDirectoryCap pd Real None; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s)
 2. \<And>s x. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 x (cap_object ?cap236, asid_offset)) (kernel_state s)
 3. \<And>s x. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> \<not> ep_related_cap x
 4. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) (kernel_state s)
 5. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) (kernel_state s)
 6. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cap_object cnode_cap = cnode_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 c (cap_object ?cap236, asid_offset)) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s proof (prove)
goal (5 subgoals):
 1. \<And>s x. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 x (cap_object ?cap236, asid_offset)) (kernel_state s)
 2. \<And>s x. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> \<not> ep_related_cap x
 3. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) (kernel_state s)
 4. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) (kernel_state s)
 5. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cap_object cnode_cap = cnode_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 c (cap_object ?cap236, asid_offset)) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s proof (prove)
goal (5 subgoals):
 1. \<And>s x. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); reset_cap_asid x = AsidPoolCap p base; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap 32 root_size; guard_equal cnode_cap sel4_page_directory 32; guard_equal cnode_cap sel4_asid 32; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl_current_thread (kernel_state s) = Some root_tcb_id; cdl_current_domain (kernel_state s) = minBound\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* ?R229 x (cap_object ?cap236, offset sel4_asid root_size)) (kernel_state s)
 2. \<And>s x. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> \<not> ep_related_cap x
 3. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) (kernel_state s)
 4. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) (kernel_state s)
 5. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cap_object cnode_cap = cnode_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* ?R229 c (cap_object ?cap236, asid_offset)) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c ?cap236 \<and>* \<box> (root_size, word_bits) : ?cap236 sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; reset_cap_asid x = AsidPoolCap p base; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> \<not> ep_related_cap x
 2. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) (kernel_state s)
 3. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) (kernel_state s)
 4. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cap_object cnode_cap = cnode_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cdl_current_thread (kernel_state s) = Some root_tcb_id \<and> cdl_current_domain (kernel_state s) = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) (kernel_state s)
 2. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) (kernel_state s)
 3. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cap_object cnode_cap = cnode_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap 32 root_size; guard_equal cnode_cap sel4_page_directory 32; guard_equal cnode_cap sel4_asid 32; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl_current_thread (kernel_state s) = Some root_tcb_id; cdl_current_domain (kernel_state s) = minBound\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* ?R236) (kernel_state s)
 2. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) (kernel_state s)
 3. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cap_object cnode_cap = cnode_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* ?R236) s; cdl_current_domain s = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) (kernel_state s); cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) (kernel_state s)
 2. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cap_object cnode_cap = cnode_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb ?tcb8 \<and>* (\<lambda>s. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cap_object cnode_cap = cnode_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cnode_id, pd_offset) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cnode_id, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cnode_id \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, asid_offset) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; cap_object cnode_cap = cnode_id; is_cnode_cap cnode_cap; offset sel4_page_directory root_size = pd_offset; offset sel4_asid root_size = asid_offset; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>c. reset_cap_asid c = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s \<and> \<not> ep_related_cap c; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; reset_cap_asid (AsidPoolCap p base) = AsidPoolCap p base \<longrightarrow> ((\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s) \<and> cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s \<and> \<not> ep_related_cap (AsidPoolCap p base)\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; (\<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None) \<longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; \<not> ep_related_cap (AsidPoolCap p base)\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; \<not> ep_related_cap (AsidPoolCap p base)\<rbrakk> \<Longrightarrow> \<exists>c. reset_cap_asid c = PageDirectoryCap pd Real None
 2. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; \<not> ep_related_cap (AsidPoolCap p base); cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; \<not> ep_related_cap (AsidPoolCap p base)\<rbrakk> \<Longrightarrow> reset_cap_asid (PageDirectoryCap pd Real None) = PageDirectoryCap pd Real None
 2. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; \<not> ep_related_cap (AsidPoolCap p base); cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; \<not> ep_related_cap (AsidPoolCap p base); cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl_current_thread s = Some root_tcb_id \<and> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; \<not> ep_related_cap (AsidPoolCap p base); cdl_current_thread s = Some root_tcb_id; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (\<lambda>s. True)) s; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; \<not> ep_related_cap (AsidPoolCap p base); cdl_current_thread s = Some root_tcb_id; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* ?R648 s) s
 2. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; \<not> ep_related_cap (AsidPoolCap p base); cdl_current_thread s = Some root_tcb_id; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* ?R648 s) s\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_asid \<mapsto>u AsidPoolCap p base \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; cdl_current_domain s = minBound; is_cnode_cap cnode_cap; one_lvl_lookup cnode_cap word_bits root_size; guard_equal cnode_cap sel4_page_directory word_bits; guard_equal cnode_cap sel4_asid word_bits; cnode_id = cap_object cnode_cap; pd_offset = offset sel4_page_directory root_size; asid_offset = offset sel4_asid root_size; cdl.lift ((root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* \<box> (root_size, word_bits) : cnode_cap sel4_page_directory \<mapsto>u PageDirectoryCap pd Real None \<and>* (root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* R) s; \<not> ep_related_cap (AsidPoolCap p base); cdl_current_thread s = Some root_tcb_id; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c - \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s; cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* (SETSEPCONJ off | off < 2 ^ asid_low_bits. (p, off) \<mapsto>c -) \<and>* (cap_object cnode_cap, offset sel4_page_directory root_size) \<mapsto>c PageDirectoryCap pd Real None \<and>* (cap_object cnode_cap, offset sel4_asid root_size) \<mapsto>c AsidPoolCap p base \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* cap_object cnode_cap \<mapsto>f CNode (empty_cnode root_size) \<and>* (root_tcb_id, tcb_cspace_slot) \<mapsto>c cnode_cap \<and>* R) s\<rbrakk> \<Longrightarrow> cdl.lift ((root_tcb_id, tcb_pending_op_slot) \<mapsto>c RunningCap \<and>* root_tcb_id \<mapsto>f Tcb tcb \<and>* (\<lambda>s. True)) s proof (prove)
goal:
No subgoals!