theory ArchArch_AI

lemma invoke_arch_tcb:
  "\<lbrace>invs and valid_arch_inv ai and st_tcb_at active tptr\<rbrace>
  arch_perform_invocation ai
  \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>" apply (simp add: arch_perform_invocation_def) apply (cases ai, simp_all) apply (wp, clarsimp simp: st_tcb_at_tcb_at)+ defer apply (wp, clarsimp simp: st_tcb_at_tcb_at) apply (wp perform_asid_control_invocation_tcb_at) apply (clarsimp simp add: valid_arch_inv_def) apply (clarsimp simp: valid_aci_def) apply (frule st_tcb_ex_cap) apply fastforce apply (clarsimp split: Structures_A.thread_state.splits) apply auto[1] apply (clarsimp simp: ex_nonz_cap_to_def) apply (frule invs_untyped_children) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (erule_tac ptr="(aa,ba)" in untyped_children_in_mdbE[where P="\<lambda>c. t \<in> zobj_refs c" for t]) apply (simp add: cte_wp_at_caps_of_state)+ apply fastforce apply (clarsimp simp: zobj_refs_to_obj_refs cte_wp_at_caps_of_state) apply (drule_tac p="(aa,ba)" in caps_of_state_valid_cap, fastforce) apply (clarsimp simp: valid_cap_def cap_aligned_def) apply (drule_tac x=tptr in base_member_set, simp) apply (simp add: pageBits_def field_simps del: atLeastAtMost_iff) apply (metis (no_types) orthD1 x_power_minus_1) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_arch_inv ai and st_tcb_at active tptr\<rbrace> arch_perform_invocation ai \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_arch_inv ai and st_tcb_at active tptr\<rbrace> liftE (case ai of InvokePageTable oper \<Rightarrow> do perform_page_table_invocation oper;
return []
od | InvokePageDirectory oper \<Rightarrow> do perform_page_directory_invocation oper;
return []
od | InvokePage x \<Rightarrow> perform_page_invocation x | InvokeASIDControl oper \<Rightarrow> do perform_asid_control_invocation oper;
return []
od | InvokeASIDPool oper \<Rightarrow> do perform_asid_pool_invocation oper;
return []
od) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. ai = InvokePageTable x1 \<Longrightarrow> \<lbrace>invs and valid_arch_inv (InvokePageTable x1) and st_tcb_at active tptr\<rbrace> liftE (do y <- perform_page_table_invocation x1;
return []
od) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>
 2. \<And>x2. ai = InvokePageDirectory x2 \<Longrightarrow> \<lbrace>invs and valid_arch_inv (InvokePageDirectory x2) and st_tcb_at active tptr\<rbrace> liftE (do y <- perform_page_directory_invocation x2;
return []
od) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>
 3. \<And>x3. ai = InvokePage x3 \<Longrightarrow> \<lbrace>invs and valid_arch_inv (InvokePage x3) and st_tcb_at active tptr\<rbrace> liftE (perform_page_invocation x3) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>
 4. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs and valid_arch_inv (InvokeASIDControl x4) and st_tcb_at active tptr\<rbrace> liftE (do y <- perform_asid_control_invocation x4;
return []
od) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>
 5. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs and valid_arch_inv (InvokeASIDPool x5) and st_tcb_at active tptr\<rbrace> liftE (do y <- perform_asid_pool_invocation x5;
return []
od) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs and valid_arch_inv (InvokeASIDControl x4) and st_tcb_at active tptr\<rbrace> liftE (do y <- perform_asid_control_invocation x4;
return []
od) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>
 2. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs and valid_arch_inv (InvokeASIDPool x5) and st_tcb_at active tptr\<rbrace> liftE (do y <- perform_asid_pool_invocation x5;
return []
od) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>invs and valid_arch_inv (InvokeASIDPool x5) and st_tcb_at active tptr\<rbrace> liftE (do y <- perform_asid_pool_invocation x5;
return []
od) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>
 2. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs and valid_arch_inv (InvokeASIDControl x4) and st_tcb_at active tptr\<rbrace> liftE (do y <- perform_asid_control_invocation x4;
return []
od) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>invs and valid_arch_inv (InvokeASIDControl x4) and st_tcb_at active tptr\<rbrace> liftE (do y <- perform_asid_control_invocation x4;
return []
od) \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x4 s. \<lbrakk>ai = InvokeASIDControl x4; (invs and valid_arch_inv (InvokeASIDControl x4) and st_tcb_at active tptr) s\<rbrakk> \<Longrightarrow> (invs and valid_aci x4 and st_tcb_at active tptr and K (\<forall>w a b c. x4 = MakePool w a b c \<longrightarrow> w \<noteq> tptr)) s proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba c. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; valid_aci (MakePool tptr (a, b) (aa, ba) c) s; st_tcb_at active tptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba c. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba c. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap s
 2. \<And>s a b aa ba c st. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; active st\<rbrakk> \<Longrightarrow> \<not> halted st
 3. \<And>s a b aa ba c. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; ex_nonz_cap_to tptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba c st. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; active st\<rbrakk> \<Longrightarrow> \<not> halted st
 2. \<And>s a b aa ba c. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; ex_nonz_cap_to tptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba c st. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; active st\<rbrakk> \<Longrightarrow> st \<noteq> Inactive \<and> st \<noteq> IdleThreadState
 2. \<And>s a b aa ba c. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; ex_nonz_cap_to tptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba c. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; ex_nonz_cap_to tptr s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba c ab bb. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; cte_wp_at (\<lambda>c. tptr \<in> zobj_refs c) (ab, bb) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba c ab bb. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; cte_wp_at (\<lambda>c. c = NullCap) (a, b) s; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False tptr pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; cte_wp_at (\<lambda>c. tptr \<in> zobj_refs c) (ab, bb) s; untyped_children_in_mdb s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; untyped_children_in_mdb s; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap125 s a b aa ba c ab bb capa idx)) (aa, ba) s
 2. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> is_untyped_cap (?cap125 s a b aa ba c ab bb capa idx)
 3. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>ca. ?t128 s a b aa ba c ab bb capa idx \<in> zobj_refs ca) (?ptr'125 s a b aa ba c ab bb capa idx) s
 4. \<And>s a b aa ba c ab bb capa idx cap'. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; cte_wp_at ((=) cap') (?ptr'125 s a b aa ba c ab bb capa idx) s; ?t128 s a b aa ba c ab bb capa idx \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (?cap125 s a b aa ba c ab bb capa idx) \<noteq> {}
 5. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; ?ptr'125 s a b aa ba c ab bb capa idx \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (?ptr'125 s a b aa ba c ab bb capa idx) = Some cap \<and> ?t128 s a b aa ba c ab bb capa idx \<in> zobj_refs cap
 2. \<And>s a b aa ba c ab bb capa idx cap'. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; cte_wp_at ((=) cap') (?ptr'125 s a b aa ba c ab bb capa idx) s; ?t128 s a b aa ba c ab bb capa idx \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap False tptr pageBits idx) \<noteq> {}
 3. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; ?ptr'125 s a b aa ba c ab bb capa idx \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba c ab bb capa idx cap'. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; cte_wp_at ((=) cap') (ab, bb) s; tptr \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap False tptr pageBits idx) \<noteq> {}
 2. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> obj_refs capa; \<not> is_zombie capa; obj_refs capa \<inter> {tptr..tptr + 2 ^ pageBits - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (ab, bb) = Some capa; tptr \<in> obj_refs capa; \<not> is_zombie capa; obj_refs capa \<inter> {tptr..tptr + 2 ^ pageBits - 1} = {}; s \<turnstile> UntypedCap False tptr pageBits idx\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (ab, bb) = Some capa; tptr \<in> obj_refs capa; \<not> is_zombie capa; obj_refs capa \<inter> {tptr..tptr + 2 ^ pageBits - 1} = {}; is_aligned tptr pageBits; valid_untyped (UntypedCap False tptr pageBits idx) s; untyped_min_bits \<le> pageBits; idx \<le> 2 ^ pageBits; tptr \<noteq> 0\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (ab, bb) = Some capa; tptr \<in> obj_refs capa; \<not> is_zombie capa; obj_refs capa \<inter> {tptr..tptr + 2 ^ pageBits - 1} = {}; valid_untyped (UntypedCap False tptr pageBits idx) s; untyped_min_bits \<le> pageBits; idx \<le> 2 ^ pageBits; tptr \<noteq> 0\<rbrakk> \<Longrightarrow> pageBits < 32
 2. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (ab, bb) = Some capa; tptr \<in> obj_refs capa; \<not> is_zombie capa; obj_refs capa \<inter> {tptr..tptr + 2 ^ pageBits - 1} = {}; valid_untyped (UntypedCap False tptr pageBits idx) s; untyped_min_bits \<le> pageBits; idx \<le> 2 ^ pageBits; tptr \<noteq> 0; tptr \<in> {tptr..tptr + (2 ^ pageBits - 1)}\<rbrakk> \<Longrightarrow> False
 3. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (ab, bb) = Some capa; tptr \<in> obj_refs capa; \<not> is_zombie capa; obj_refs capa \<inter> {tptr..tptr + 2 ^ pageBits - 1} = {}; valid_untyped (UntypedCap False tptr pageBits idx) s; untyped_min_bits \<le> pageBits; idx \<le> 2 ^ pageBits; tptr \<noteq> 0; tptr \<in> {tptr..tptr + (2 ^ pageBits - 1)}\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba c ab bb capa idx. \<lbrakk>ai = InvokeASIDControl (MakePool tptr (a, b) (aa, ba) c); invs s; st_tcb_at active tptr s; caps_of_state s (a, b) = Some NullCap; cap_table_at (length b) a s; ex_cte_cap_wp_to is_cnode_cap (a, b) s; a = aa \<longrightarrow> b \<noteq> ba; descendants_of (aa, ba) (cdt s) = {}; is_aligned c local.asid_low_bits; c < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of c) = None; caps_of_state s (aa, ba) = Some (UntypedCap False tptr pageBits idx); caps_of_state s (ab, bb) = Some capa; tptr \<in> zobj_refs capa; (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!