theory ArchArch_AI

lemma sts_valid_arch_inv:
  "\<lbrace>valid_arch_inv ai\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_arch_inv ai\<rbrace>" apply (cases ai, simp_all add: valid_arch_inv_def) apply (rename_tac page_table_invocation) apply (case_tac page_table_invocation, simp_all add: valid_pti_def)[1] apply ((wp valid_pde_lift set_thread_state_valid_cap
                 hoare_vcg_all_lift hoare_vcg_const_imp_lift
                 hoare_vcg_ex_lift set_thread_state_ko
                 sts_typ_ats set_thread_state_cte_wp_at
               | clarsimp simp: is_tcb_def)+)[4] apply (rename_tac asid_control_invocation) apply (case_tac asid_control_invocation) apply (clarsimp simp: valid_aci_def cte_wp_at_caps_of_state) apply (rule hoare_pre, wp hoare_vcg_ex_lift cap_table_at_typ_at) apply clarsimp apply (clarsimp simp: valid_apinv_def split: asid_pool_invocation.splits) apply (rule hoare_pre) apply (wp hoare_vcg_ex_lift set_thread_state_ko) apply (clarsimp simp: is_tcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_inv ai\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_arch_inv ai\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x1. ai = InvokePageTable x1 \<Longrightarrow> \<lbrace>valid_pti x1\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pti x1\<rbrace>
 2. \<And>x2. ai = InvokePageDirectory x2 \<Longrightarrow> \<lbrace>valid_pdi x2\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pdi x2\<rbrace>
 3. \<And>x3. ai = InvokePage x3 \<Longrightarrow> \<lbrace>valid_page_inv x3\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv x3\<rbrace>
 4. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci x4\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_aci x4\<rbrace>
 5. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv x5\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_apinv x5\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>page_table_invocation. ai = InvokePageTable page_table_invocation \<Longrightarrow> \<lbrace>valid_pti page_table_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pti page_table_invocation\<rbrace>
 2. \<And>x2. ai = InvokePageDirectory x2 \<Longrightarrow> \<lbrace>valid_pdi x2\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pdi x2\<rbrace>
 3. \<And>x3. ai = InvokePage x3 \<Longrightarrow> \<lbrace>valid_page_inv x3\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv x3\<rbrace>
 4. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci x4\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_aci x4\<rbrace>
 5. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv x5\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_apinv x5\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>page_table_invocation x11 x12 x13 x14. \<lbrakk>ai = InvokePageTable (PageTableMap x11 x12 x13 x14); page_table_invocation = PageTableMap x11 x12 x13 x14\<rbrakk> \<Longrightarrow> \<lbrace>pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) x12 and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y))\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. pde_at x14 and (\<lambda>s. wellformed_pde x13) and valid_pde x13 and valid_cap x11 and cte_wp_at (\<lambda>c. is_arch_update x11 c \<and> cap_asid c = None) x12 and empty_pde_at x14 and (\<lambda>s. \<exists>p' ref. vs_cap_ref x11 = Some (VSRef (x14 && mask pd_bits >> 2) (Some APageDirectory) # ref) \<and> (ref \<rhd> (x14 && ~~ mask pd_bits)) s \<and> pde_ref x13 = Some p' \<and> p' \<in> obj_refs x11 \<and> (\<exists>ao. ako_at ao p' s \<and> valid_vspace_obj ao s) \<and> hd (the (vs_cap_ref x11)) \<notin> kernel_vsrefs) and (\<lambda>y. is_pt_cap x11 \<and> (\<exists>y. cap_asid x11 = Some y))\<rbrace>
 2. \<And>page_table_invocation x21 x22. \<lbrakk>ai = InvokePageTable (PageTableUnmap x21 x22); page_table_invocation = PageTableUnmap x21 x22\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at ((=) x21) x22 and valid_cap x21 and is_final_cap' x21 and (\<lambda>y. is_pt_cap x21)\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. cte_wp_at ((=) x21) x22 and valid_cap x21 and is_final_cap' x21 and (\<lambda>y. is_pt_cap x21)\<rbrace>
 3. \<And>x2. ai = InvokePageDirectory x2 \<Longrightarrow> \<lbrace>valid_pdi x2\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pdi x2\<rbrace>
 4. \<And>x3. ai = InvokePage x3 \<Longrightarrow> \<lbrace>valid_page_inv x3\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv x3\<rbrace>
 5. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci x4\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_aci x4\<rbrace>
 6. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv x5\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_apinv x5\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x4. ai = InvokeASIDControl x4 \<Longrightarrow> \<lbrace>valid_aci x4\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_aci x4\<rbrace>
 2. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv x5\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_apinv x5\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>asid_control_invocation. ai = InvokeASIDControl asid_control_invocation \<Longrightarrow> \<lbrace>valid_aci asid_control_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_aci asid_control_invocation\<rbrace>
 2. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv x5\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_apinv x5\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>asid_control_invocation x1 x2 x3 x4. \<lbrakk>ai = InvokeASIDControl asid_control_invocation; asid_control_invocation = MakePool x1 x2 x3 x4\<rbrakk> \<Longrightarrow> \<lbrace>valid_aci asid_control_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_aci asid_control_invocation\<rbrace>
 2. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv x5\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_apinv x5\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4. ai = InvokeASIDControl (MakePool x1 (a, b) (aa, ba) x4) \<Longrightarrow> \<lbrace>\<lambda>s. caps_of_state s (a, b) = Some NullCap \<and> cap_table_at (length b) a s \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> (\<exists>idx. cap = UntypedCap False x1 pageBits idx)) \<and> descendants_of (aa, ba) (cdt s) = {} \<and> is_aligned x4 local.asid_low_bits \<and> x4 < 2 ^ local.asid_bits \<and> asid_table s (asid_high_bits_of x4) = None\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. caps_of_state s (a, b) = Some NullCap \<and> cap_table_at (length b) a s \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> (\<exists>idx. cap = UntypedCap False x1 pageBits idx)) \<and> descendants_of (aa, ba) (cdt s) = {} \<and> is_aligned x4 local.asid_low_bits \<and> x4 < 2 ^ local.asid_bits \<and> asid_table s (asid_high_bits_of x4) = None\<rbrace>
 2. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv x5\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_apinv x5\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 a b aa ba x4 s. \<lbrakk>ai = InvokeASIDControl (MakePool x1 (a, b) (aa, ba) x4); caps_of_state s (a, b) = Some NullCap \<and> cap_table_at (length b) a s \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<and> (\<exists>cap. caps_of_state s (aa, ba) = Some cap \<and> (\<exists>idx. cap = UntypedCap False x1 pageBits idx)) \<and> descendants_of (aa, ba) (cdt s) = {} \<and> is_aligned x4 local.asid_low_bits \<and> x4 < 2 ^ local.asid_bits \<and> asid_table s (asid_high_bits_of x4) = None\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) = Some NullCap \<and> cap_table_at (length b) a s \<and> ex_cte_cap_wp_to is_cnode_cap (a, b) s \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<and> (\<exists>x. caps_of_state s (aa, ba) = Some x \<and> (\<exists>idx. x = UntypedCap False x1 pageBits idx)) \<and> descendants_of (aa, ba) (cdt s) = {} \<and> is_aligned x4 local.asid_low_bits \<and> x4 < 2 ^ local.asid_bits \<and> asid_table s (asid_high_bits_of x4) = None
 2. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv x5\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_apinv x5\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x5. ai = InvokeASIDPool x5 \<Longrightarrow> \<lbrace>valid_apinv x5\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_apinv x5\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b. ai = InvokeASIDPool (Assign x1 x2 (a, b)) \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>pool. ako_at (ASIDPool pool) x2 s \<and> pool (UCAST(32 \<rightarrow> 10) x1) = None) and cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) and (\<lambda>y. 0 < x1 \<and> x1 < 2 ^ local.asid_bits) and [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. (\<lambda>s. \<exists>pool. ako_at (ASIDPool pool) x2 s \<and> pool (UCAST(32 \<rightarrow> 10) x1) = None) and cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) and (\<lambda>y. 0 < x1 \<and> x1 < 2 ^ local.asid_bits) and [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 a b. ai = InvokeASIDPool (Assign x1 x2 (a, b)) \<Longrightarrow> \<lbrace>?Q108 x1 x2 a b\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. (\<lambda>s. \<exists>pool. ako_at (ASIDPool pool) x2 s \<and> pool (UCAST(32 \<rightarrow> 10) x1) = None) and cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) and (\<lambda>y. 0 < x1 \<and> x1 < 2 ^ local.asid_bits) and [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2\<rbrace>
 2. \<And>x1 x2 a b s. \<lbrakk>ai = InvokeASIDPool (Assign x1 x2 (a, b)); ((\<lambda>s. \<exists>pool. ako_at (ASIDPool pool) x2 s \<and> pool (UCAST(32 \<rightarrow> 10) x1) = None) and cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) and (\<lambda>y. 0 < x1 \<and> x1 < 2 ^ local.asid_bits) and [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s\<rbrakk> \<Longrightarrow> ?Q108 x1 x2 a b s proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 a b s. \<lbrakk>ai = InvokeASIDPool (Assign x1 x2 (a, b)); ((\<lambda>s. \<exists>pool. ako_at (ASIDPool pool) x2 s \<and> pool (UCAST(32 \<rightarrow> 10) x1) = None) and cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) and (\<lambda>y. 0 < x1 \<and> x1 < 2 ^ local.asid_bits) and [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s\<rbrakk> \<Longrightarrow> (\<exists>x. (ako_at (ASIDPool x) x2 and K (\<not> is_tcb (ArchObj (ASIDPool x)))) s \<and> x (UCAST(32 \<rightarrow> 10) x1) = None) \<and> cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) (a, b) s \<and> (0 < x1 \<and> x1 < 2 ^ local.asid_bits) \<and> ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of x1)) None] \<rhd> x2) s proof (prove)
goal:
No subgoals!