theory ArchArch_AI

lemma perform_asid_control_invocation_tcb_at:
  "\<lbrace>invs and valid_aci aci and st_tcb_at active p and
    K (\<forall>w a b c. aci = asid_control_invocation.MakePool w a b c \<longrightarrow> w \<noteq> p)\<rbrace>
  perform_asid_control_invocation aci
  \<lbrace>\<lambda>rv. tcb_at p\<rbrace>" apply (simp add: perform_asid_control_invocation_def) apply (cases aci) apply clarsimp apply (wp |simp)+ apply (wp obj_at_delete_objects retype_region_obj_at_other2  hoare_vcg_const_imp_lift|assumption)+ apply (intro impI conjI) apply (clarsimp simp: retype_addrs_def obj_bits_api_def default_arch_object_def image_def ptr_add_def) apply (clarsimp simp: st_tcb_at_tcb_at)+ 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 valid_aci_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 simp apply (simp add:cte_wp_at_caps_of_state) apply fastforce apply (clarsimp simp: zobj_refs_to_obj_refs) apply (erule(1) in_empty_interE) apply (clarsimp simp:page_bits_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_aci aci and st_tcb_at active p and K (\<forall>w a b c. aci = MakePool w a b c \<longrightarrow> w \<noteq> p)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>rv. tcb_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_aci aci and st_tcb_at active p and (\<lambda>y. \<forall>w. (\<exists>a b aa ba c. aci = MakePool w (a, b) (aa, ba) c) \<longrightarrow> w \<noteq> p)\<rbrace> case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>rv. tcb_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>invs and valid_aci aci and st_tcb_at active p and (\<lambda>y. \<forall>w. (\<exists>a b aa ba c. aci = MakePool w (a, b) (aa, ba) c) \<longrightarrow> w \<noteq> p)\<rbrace> case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>rv. tcb_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4. aci = MakePool x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>invs and valid_aci (MakePool x1 (a, b) (aa, ba) x4) and st_tcb_at active p and (\<lambda>y. x1 \<noteq> p)\<rbrace> do y <- delete_objects x1 page_bits;
pcap <- get_cap (aa, ba);
y <- set_cap (max_free_index_update pcap) (aa, ba);
y <- retype_region x1 (Suc 0) 0 (ArchObject ASIDPoolObj) False;
y <- cap_insert (ArchObjectCap (ASIDPoolCap x1 x4)) (aa, ba) (a, b);
y <- assert (x4 && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of x4 \<mapsto> x1)\<rparr>\<rparr>)
od \<lbrace>\<lambda>rv. tcb_at p\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x1 a b aa ba x4 pcap yb. aci = MakePool x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>?B12 x1 a b aa ba x4 () pcap () yb\<rbrace> cap_insert (ArchObjectCap (ASIDPoolCap x1 x4)) (aa, ba) (a, b) \<lbrace>\<lambda>yc s. x4 && mask local.asid_low_bits = 0 \<longrightarrow> tcb_at p s\<rbrace>
 2. \<And>x1 a b aa ba x4 y pcap ya. aci = MakePool x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>?B11 x1 a b aa ba x4 y pcap ya\<rbrace> retype_region x1 (Suc 0) 0 (ArchObject ASIDPoolObj) False \<lbrace>?B12 x1 a b aa ba x4 y pcap ya\<rbrace>
 3. \<And>x1 a b aa ba x4 y pcap. aci = MakePool x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>?B10 x1 a b aa ba x4 y pcap\<rbrace> set_cap (max_free_index_update pcap) (aa, ba) \<lbrace>?B11 x1 a b aa ba x4 y pcap\<rbrace>
 4. \<And>x1 a b aa ba x4 y. aci = MakePool x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>?B9 x1 a b aa ba x4 y\<rbrace> get_cap (aa, ba) \<lbrace>?B10 x1 a b aa ba x4 y\<rbrace>
 5. \<And>x1 a b aa ba x4. aci = MakePool x1 (a, b) (aa, ba) x4 \<Longrightarrow> \<lbrace>?Q8 x1 a b aa ba x4\<rbrace> delete_objects x1 page_bits \<lbrace>?B9 x1 a b aa ba x4\<rbrace>
 6. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; (invs and valid_aci (MakePool x1 (a, b) (aa, ba) x4) and st_tcb_at active p and (\<lambda>y. x1 \<noteq> p)) s\<rbrakk> \<Longrightarrow> ?Q8 x1 a b aa ba x4 s proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; (invs and valid_aci (MakePool x1 (a, b) (aa, ba) x4) and st_tcb_at active p and (\<lambda>y. x1 \<noteq> p)) s\<rbrakk> \<Longrightarrow> (x4 && mask local.asid_low_bits = 0 \<longrightarrow> p \<notin> set (retype_addrs x1 (ArchObject ASIDPoolObj) (Suc 0) 0) \<and> tcb_at p s) \<and> p \<notin> {x1..x1 + 2 ^ page_bits - 1} proof (prove)
goal (3 subgoals):
 1. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; (invs and valid_aci (MakePool x1 (a, b) (aa, ba) x4) and st_tcb_at active p and (\<lambda>y. x1 \<noteq> p)) s; x4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> p \<notin> set (retype_addrs x1 (ArchObject ASIDPoolObj) (Suc 0) 0)
 2. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; (invs and valid_aci (MakePool x1 (a, b) (aa, ba) x4) and st_tcb_at active p and (\<lambda>y. x1 \<noteq> p)) s; x4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> tcb_at p s
 3. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; (invs and valid_aci (MakePool x1 (a, b) (aa, ba) x4) and st_tcb_at active p and (\<lambda>y. x1 \<noteq> p)) s\<rbrakk> \<Longrightarrow> p \<notin> {x1..x1 + 2 ^ page_bits - 1} proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; (invs and valid_aci (MakePool x1 (a, b) (aa, ba) x4) and st_tcb_at active p and (\<lambda>y. x1 \<noteq> p)) s; x4 && mask local.asid_low_bits = 0\<rbrakk> \<Longrightarrow> tcb_at p s
 2. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; (invs and valid_aci (MakePool x1 (a, b) (aa, ba) x4) and st_tcb_at active p and (\<lambda>y. x1 \<noteq> p)) s\<rbrakk> \<Longrightarrow> p \<notin> {x1..x1 + 2 ^ page_bits - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; valid_aci (MakePool x1 (a, b) (aa, ba) x4) s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; valid_aci (MakePool x1 (a, b) (aa, ba) x4) s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1\<rbrakk> \<Longrightarrow> if_live_then_nonz_cap s
 2. \<And>x1 a b aa ba x4 s st. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; valid_aci (MakePool x1 (a, b) (aa, ba) x4) s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; active st\<rbrakk> \<Longrightarrow> \<not> halted st
 3. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; valid_aci (MakePool x1 (a, b) (aa, ba) x4) s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; ex_nonz_cap_to p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4 s st. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; valid_aci (MakePool x1 (a, b) (aa, ba) x4) s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; active st\<rbrakk> \<Longrightarrow> \<not> halted st
 2. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; valid_aci (MakePool x1 (a, b) (aa, ba) x4) s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; ex_nonz_cap_to p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4 s st. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; valid_aci (MakePool x1 (a, b) (aa, ba) x4) s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; active st\<rbrakk> \<Longrightarrow> st \<noteq> Inactive \<and> st \<noteq> IdleThreadState
 2. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; valid_aci (MakePool x1 (a, b) (aa, ba) x4) s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; ex_nonz_cap_to p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; valid_aci (MakePool x1 (a, b) (aa, ba) x4) s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; ex_nonz_cap_to p s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s ab bb. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; cte_wp_at (\<lambda>c. p \<in> zobj_refs c) (ab, bb) 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 x1 pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s ab bb. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; cte_wp_at (\<lambda>c. p \<in> zobj_refs c) (ab, bb) 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 x1 pageBits idx) (aa, ba) s; descendants_of (aa, ba) (cdt s) = {}; is_aligned x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; untyped_children_in_mdb s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; untyped_children_in_mdb s; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx)\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap110 x1 a b aa ba x4 s ab bb cap idx)) (aa, ba) s
 2. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx)\<rbrakk> \<Longrightarrow> is_untyped_cap (?cap110 x1 a b aa ba x4 s ab bb cap idx)
 3. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. ?t113 x1 a b aa ba x4 s ab bb cap idx \<in> zobj_refs c) (?ptr'110 x1 a b aa ba x4 s ab bb cap idx) s
 4. \<And>x1 a b aa ba x4 s ab bb cap idx cap'. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); cte_wp_at ((=) cap') (?ptr'110 x1 a b aa ba x4 s ab bb cap idx) s; ?t113 x1 a b aa ba x4 s ab bb cap idx \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (?cap110 x1 a b aa ba x4 s ab bb cap idx) \<noteq> {}
 5. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); ?ptr'110 x1 a b aa ba x4 s ab bb cap idx \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx)\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap False x1 pageBits idx)
 2. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. ?t113 x1 a b aa ba x4 s ab bb cap idx \<in> zobj_refs c) (?ptr'110 x1 a b aa ba x4 s ab bb cap idx) s
 3. \<And>x1 a b aa ba x4 s ab bb cap idx cap'. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); cte_wp_at ((=) cap') (?ptr'110 x1 a b aa ba x4 s ab bb cap idx) s; ?t113 x1 a b aa ba x4 s ab bb cap idx \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap False x1 pageBits idx) \<noteq> {}
 4. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); ?ptr'110 x1 a b aa ba x4 s ab bb cap idx \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. ?t113 x1 a b aa ba x4 s ab bb cap idx \<in> zobj_refs c) (?ptr'110 x1 a b aa ba x4 s ab bb cap idx) s
 2. \<And>x1 a b aa ba x4 s ab bb cap idx cap'. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); cte_wp_at ((=) cap') (?ptr'110 x1 a b aa ba x4 s ab bb cap idx) s; ?t113 x1 a b aa ba x4 s ab bb cap idx \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap False x1 pageBits idx) \<noteq> {}
 3. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); ?ptr'110 x1 a b aa ba x4 s ab bb cap idx \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx)\<rbrakk> \<Longrightarrow> \<exists>capa. caps_of_state s (?ptr'110 x1 a b aa ba x4 s ab bb cap idx) = Some capa \<and> ?t113 x1 a b aa ba x4 s ab bb cap idx \<in> zobj_refs capa
 2. \<And>x1 a b aa ba x4 s ab bb cap idx cap'. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); cte_wp_at ((=) cap') (?ptr'110 x1 a b aa ba x4 s ab bb cap idx) s; ?t113 x1 a b aa ba x4 s ab bb cap idx \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap False x1 pageBits idx) \<noteq> {}
 3. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); ?ptr'110 x1 a b aa ba x4 s ab bb cap idx \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4 s ab bb cap idx cap'. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); cte_wp_at ((=) cap') (ab, bb) s; p \<in> zobj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap False x1 pageBits idx) \<noteq> {}
 2. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4 s ab bb cap idx cap'. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); cte_wp_at ((=) cap') (ab, bb) s; p \<in> obj_refs cap; \<not> is_zombie cap; p \<in> obj_refs cap'; \<not> is_zombie cap'; obj_refs cap' \<inter> {x1..x1 + 2 ^ pageBits - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4 s ab bb cap idx cap'. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); cte_wp_at ((=) cap') (ab, bb) s; p \<in> obj_refs cap; \<not> is_zombie cap; p \<in> obj_refs cap'; \<not> is_zombie cap'\<rbrakk> \<Longrightarrow> p \<in> {x1..x1 + 2 ^ pageBits - 1}
 2. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x1 a b aa ba x4 s ab bb cap idx. \<lbrakk>aci = MakePool x1 (a, b) (aa, ba) x4; invs s; st_tcb_at active p s; x1 \<noteq> p; x1 \<le> p; p \<le> x1 + 2 ^ page_bits - 1; 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 x4 local.asid_low_bits; x4 < 2 ^ local.asid_bits; asid_table s (asid_high_bits_of x4) = None; caps_of_state s (ab, bb) = Some cap; p \<in> zobj_refs cap; caps_of_state s (aa, ba) = Some (UntypedCap False x1 pageBits idx); (ab, bb) \<in> descendants_of (aa, ba) (cdt s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!