theory ArchFinalise_AI

lemma delete_asid_empty_table_pd:
  "\<lbrace>\<lambda>s. page_directory_at word s
      \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
    delete_asid a word
   \<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>" apply (simp add: delete_asid_def) apply (wp | wpc)+ apply wps apply wp+ apply (simp add: set_asid_pool_def) apply (case_tac "x2 = word") defer apply wps apply (rule set_object_at_obj) apply (wp get_object_ret | wps)+ apply (clarsimp simp: obj_at_def empty_table_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> delete_asid a word \<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> do asid_table <- gets (arm_asid_table \<circ> arch_state);
case asid_table (asid_high_bits_of a) of None \<Rightarrow> return () | Some pool_ptr \<Rightarrow> do pool <- get_asid_pool pool_ptr;
when (pool (UCAST(32 \<rightarrow> 10) a) = Some word) $ do flush_space a;
invalidate_asid_entry a;
pool' <- return (pool(UCAST(32 \<rightarrow> 10) a := None));
set_asid_pool pool_ptr pool';
gets cur_thread >>= set_vm_root
od
od
od \<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>asid_table x2 pool x xa pool' xb tcb. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B27 asid_table x2 pool x xa pool' xb tcb\<rbrace> set_vm_root tcb \<lbrace>\<lambda>_ s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
 2. \<And>asid_table x2 pool x xa pool' xb. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B25 asid_table x2 pool x xa pool' xb\<rbrace> gets cur_thread \<lbrace>?B27 asid_table x2 pool x xa pool' xb\<rbrace>
 3. \<And>asid_table x2 pool x xa pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B24 asid_table x2 pool x xa pool'\<rbrace> set_asid_pool x2 pool' \<lbrace>?B25 asid_table x2 pool x xa pool'\<rbrace>
 4. \<And>asid_table x2 pool x xa. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B22 asid_table x2 pool x xa\<rbrace> return (pool(UCAST(32 \<rightarrow> 10) a := None)) \<lbrace>?B24 asid_table x2 pool x xa\<rbrace>
 5. \<And>asid_table x2 pool x. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B20 asid_table x2 pool x\<rbrace> invalidate_asid_entry a \<lbrace>?B22 asid_table x2 pool x\<rbrace>
 6. \<And>asid_table x2 pool. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 asid_table x2 pool\<rbrace> flush_space a \<lbrace>?B20 asid_table x2 pool\<rbrace>
 7. \<And>asid_table x2. asid_table (asid_high_bits_of a) = Some x2 \<Longrightarrow> \<lbrace>?R11 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) a) = Some word then ?Q19 asid_table x2 pool else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 8. \<lbrace>?Q\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of a) = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s) \<and> (\<forall>x. asid_table (asid_high_bits_of a) = Some x \<longrightarrow> ?R11 asid_table x s)\<rbrace>
 9. \<And>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>asid_table x2 pool x xa pool' xb tcb prev_s. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?P29 asid_table x2 pool x xa pool' xb tcb prev_s\<rbrace> set_vm_root tcb \<lbrace>\<lambda>rv s'. obj_at (empty_table (set (arm_global_pts (arch_state prev_s)))) word prev_s\<rbrace>
 2. \<And>asid_table x2 pool x xa pool' xb. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B25 asid_table x2 pool x xa pool' xb\<rbrace> gets cur_thread \<lbrace>\<lambda>tcb s. ?P29 asid_table x2 pool x xa pool' xb tcb s s\<rbrace>
 3. \<And>asid_table x2 pool x xa pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B24 asid_table x2 pool x xa pool'\<rbrace> set_asid_pool x2 pool' \<lbrace>?B25 asid_table x2 pool x xa pool'\<rbrace>
 4. \<And>asid_table x2 pool x xa. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B22 asid_table x2 pool x xa\<rbrace> return (pool(UCAST(32 \<rightarrow> 10) a := None)) \<lbrace>?B24 asid_table x2 pool x xa\<rbrace>
 5. \<And>asid_table x2 pool x. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B20 asid_table x2 pool x\<rbrace> invalidate_asid_entry a \<lbrace>?B22 asid_table x2 pool x\<rbrace>
 6. \<And>asid_table x2 pool. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 asid_table x2 pool\<rbrace> flush_space a \<lbrace>?B20 asid_table x2 pool\<rbrace>
 7. \<And>asid_table x2. asid_table (asid_high_bits_of a) = Some x2 \<Longrightarrow> \<lbrace>?R11 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) a) = Some word then ?Q19 asid_table x2 pool else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 8. \<lbrace>?Q\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of a) = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s) \<and> (\<forall>x. asid_table (asid_high_bits_of a) = Some x \<longrightarrow> ?R11 asid_table x s)\<rbrace>
 9. \<And>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>asid_table x2 pool x xa pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B24 asid_table x2 pool x xa pool'\<rbrace> set_asid_pool x2 pool' \<lbrace>\<lambda>xb s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
 2. \<And>asid_table x2 pool x xa. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B22 asid_table x2 pool x xa\<rbrace> return (pool(UCAST(32 \<rightarrow> 10) a := None)) \<lbrace>?B24 asid_table x2 pool x xa\<rbrace>
 3. \<And>asid_table x2 pool x. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B20 asid_table x2 pool x\<rbrace> invalidate_asid_entry a \<lbrace>?B22 asid_table x2 pool x\<rbrace>
 4. \<And>asid_table x2 pool. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 asid_table x2 pool\<rbrace> flush_space a \<lbrace>?B20 asid_table x2 pool\<rbrace>
 5. \<And>asid_table x2. asid_table (asid_high_bits_of a) = Some x2 \<Longrightarrow> \<lbrace>?R11 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) a) = Some word then ?Q19 asid_table x2 pool else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of a) = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s) \<and> (\<forall>x. asid_table (asid_high_bits_of a) = Some x \<longrightarrow> ?R11 asid_table x s)\<rbrace>
 7. \<And>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>asid_table x2 pool pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B24 asid_table x2 pool () () pool'\<rbrace> set_object x2 (ArchObj (ASIDPool pool')) \<lbrace>\<lambda>xb s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
 2. \<And>asid_table x2 pool x xa. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B22 asid_table x2 pool x xa\<rbrace> return (pool(UCAST(32 \<rightarrow> 10) a := None)) \<lbrace>?B24 asid_table x2 pool x xa\<rbrace>
 3. \<And>asid_table x2 pool x. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B20 asid_table x2 pool x\<rbrace> invalidate_asid_entry a \<lbrace>?B22 asid_table x2 pool x\<rbrace>
 4. \<And>asid_table x2 pool. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 asid_table x2 pool\<rbrace> flush_space a \<lbrace>?B20 asid_table x2 pool\<rbrace>
 5. \<And>asid_table x2. asid_table (asid_high_bits_of a) = Some x2 \<Longrightarrow> \<lbrace>?R11 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) a) = Some word then ?Q19 asid_table x2 pool else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of a) = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s) \<and> (\<forall>x. asid_table (asid_high_bits_of a) = Some x \<longrightarrow> ?R11 asid_table x s)\<rbrace>
 7. \<And>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>asid_table x2 pool pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word; x2 = word\<rbrakk> \<Longrightarrow> \<lbrace>?B24 asid_table x2 pool () () pool'\<rbrace> set_object x2 (ArchObj (ASIDPool pool')) \<lbrace>\<lambda>xb s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
 2. \<And>asid_table x2 pool pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word; x2 \<noteq> word\<rbrakk> \<Longrightarrow> \<lbrace>?B24 asid_table x2 pool () () pool'\<rbrace> set_object x2 (ArchObj (ASIDPool pool')) \<lbrace>\<lambda>xb s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
 3. \<And>asid_table x2 pool x xa. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B22 asid_table x2 pool x xa\<rbrace> return (pool(UCAST(32 \<rightarrow> 10) a := None)) \<lbrace>?B24 asid_table x2 pool x xa\<rbrace>
 4. \<And>asid_table x2 pool x. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B20 asid_table x2 pool x\<rbrace> invalidate_asid_entry a \<lbrace>?B22 asid_table x2 pool x\<rbrace>
 5. \<And>asid_table x2 pool. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 asid_table x2 pool\<rbrace> flush_space a \<lbrace>?B20 asid_table x2 pool\<rbrace>
 6. \<And>asid_table x2. asid_table (asid_high_bits_of a) = Some x2 \<Longrightarrow> \<lbrace>?R11 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) a) = Some word then ?Q19 asid_table x2 pool else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 7. \<lbrace>?Q\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of a) = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s) \<and> (\<forall>x. asid_table (asid_high_bits_of a) = Some x \<longrightarrow> ?R11 asid_table x s)\<rbrace>
 8. \<And>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>asid_table x2 pool pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word; x2 \<noteq> word\<rbrakk> \<Longrightarrow> \<lbrace>?B24 asid_table x2 pool () () pool'\<rbrace> set_object x2 (ArchObj (ASIDPool pool')) \<lbrace>\<lambda>xb s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
 2. \<And>asid_table x2 pool x xa. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B22 asid_table x2 pool x xa\<rbrace> return (pool(UCAST(32 \<rightarrow> 10) a := None)) \<lbrace>?B24 asid_table x2 pool x xa\<rbrace>
 3. \<And>asid_table x2 pool x. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B20 asid_table x2 pool x\<rbrace> invalidate_asid_entry a \<lbrace>?B22 asid_table x2 pool x\<rbrace>
 4. \<And>asid_table x2 pool. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 asid_table x2 pool\<rbrace> flush_space a \<lbrace>?B20 asid_table x2 pool\<rbrace>
 5. \<And>asid_table x2. asid_table (asid_high_bits_of a) = Some x2 \<Longrightarrow> \<lbrace>?R11 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) a) = Some word then ?Q19 asid_table x2 pool else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of a) = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s) \<and> (\<forall>x. asid_table (asid_high_bits_of a) = Some x \<longrightarrow> ?R11 asid_table x s)\<rbrace>
 7. \<And>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q s
 8. \<And>asid_table x2 pool pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word; x2 = word\<rbrakk> \<Longrightarrow> \<lbrace>?B24 asid_table x2 pool () () pool'\<rbrace> set_object x2 (ArchObj (ASIDPool pool')) \<lbrace>\<lambda>xb s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>asid_table x2 pool pool' prev_s. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word; x2 \<noteq> word\<rbrakk> \<Longrightarrow> \<lbrace>?P42 asid_table x2 pool pool' prev_s\<rbrace> set_object x2 (ArchObj (ASIDPool pool')) \<lbrace>\<lambda>rv. obj_at (empty_table (set (arm_global_pts (arch_state prev_s)))) word\<rbrace>
 2. \<And>asid_table x2 pool x xa. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B22 asid_table x2 pool x xa\<rbrace> return (pool(UCAST(32 \<rightarrow> 10) a := None)) \<lbrace>?B24 asid_table x2 pool x xa\<rbrace>
 3. \<And>asid_table x2 pool x. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B20 asid_table x2 pool x\<rbrace> invalidate_asid_entry a \<lbrace>?B22 asid_table x2 pool x\<rbrace>
 4. \<And>asid_table x2 pool. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 asid_table x2 pool\<rbrace> flush_space a \<lbrace>?B20 asid_table x2 pool\<rbrace>
 5. \<And>asid_table x2. asid_table (asid_high_bits_of a) = Some x2 \<Longrightarrow> \<lbrace>?R11 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) a) = Some word then ?Q19 asid_table x2 pool else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 6. \<lbrace>?Q\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of a) = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s) \<and> (\<forall>x. asid_table (asid_high_bits_of a) = Some x \<longrightarrow> ?R11 asid_table x s)\<rbrace>
 7. \<And>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q s
 8. \<And>asid_table x2 pool pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word; x2 = word\<rbrakk> \<Longrightarrow> \<lbrace>?B24 asid_table x2 pool () () pool'\<rbrace> set_object x2 (ArchObj (ASIDPool pool')) \<lbrace>\<lambda>xb s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace>
flex-flex pairs:
\<lambda>asid_table x2 pool pool' s. ?P42 asid_table x2 pool pool' s s \<equiv>\<^sup>? \<lambda>asid_table x2 pool. ?B24 asid_table x2 pool () () proof (prove)
goal (7 subgoals):
 1. \<And>asid_table x2 pool x xa. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B22 asid_table x2 pool x xa\<rbrace> return (pool(UCAST(32 \<rightarrow> 10) a := None)) \<lbrace>\<lambda>a b. obj_at (empty_table (set (arm_global_pts (arch_state b)))) word b \<and> (word = x2 \<longrightarrow> empty_table (set (arm_global_pts (arch_state b))) (ArchObj (ASIDPool a)))\<rbrace>
 2. \<And>asid_table x2 pool x. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?B20 asid_table x2 pool x\<rbrace> invalidate_asid_entry a \<lbrace>?B22 asid_table x2 pool x\<rbrace>
 3. \<And>asid_table x2 pool. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word\<rbrakk> \<Longrightarrow> \<lbrace>?Q19 asid_table x2 pool\<rbrace> flush_space a \<lbrace>?B20 asid_table x2 pool\<rbrace>
 4. \<And>asid_table x2. asid_table (asid_high_bits_of a) = Some x2 \<Longrightarrow> \<lbrace>?R11 asid_table x2\<rbrace> get_asid_pool x2 \<lbrace>\<lambda>pool. if pool (UCAST(32 \<rightarrow> 10) a) = Some word then ?Q19 asid_table x2 pool else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)\<rbrace>
 5. \<lbrace>?Q\<rbrace> gets (arm_asid_table \<circ> arch_state) \<lbrace>\<lambda>asid_table s. (asid_table (asid_high_bits_of a) = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s) \<and> (\<forall>x. asid_table (asid_high_bits_of a) = Some x \<longrightarrow> ?R11 asid_table x s)\<rbrace>
 6. \<And>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ?Q s
 7. \<And>asid_table x2 pool pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word; x2 = word\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. obj_at (empty_table (set (arm_global_pts (arch_state a)))) word a \<and> (word = x2 \<longrightarrow> empty_table (set (arm_global_pts (arch_state a))) (ArchObj (ASIDPool pool')))\<rbrace> set_object x2 (ArchObj (ASIDPool pool')) \<lbrace>\<lambda>xb s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. typ_at (AArch APageDirectory) word s \<and> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<Longrightarrow> ((arm_asid_table \<circ> arch_state) s (asid_high_bits_of a) = None \<longrightarrow> obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s) \<and> (\<forall>x. (arm_asid_table \<circ> arch_state) s (asid_high_bits_of a) = Some x \<longrightarrow> (\<forall>pool. ako_at (ASIDPool pool) x s \<longrightarrow> (if pool (UCAST(32 \<rightarrow> 10) a) = Some word then \<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s \<and> (word = x \<longrightarrow> empty_table (set (arm_global_pts (arch_state s))) (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) a := None))))) else (\<lambda>s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s)) s))
 2. \<And>asid_table x2 pool pool'. \<lbrakk>asid_table (asid_high_bits_of a) = Some x2; pool (UCAST(32 \<rightarrow> 10) a) = Some word; x2 = word\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. obj_at (empty_table (set (arm_global_pts (arch_state a)))) word a \<and> (word = x2 \<longrightarrow> empty_table (set (arm_global_pts (arch_state a))) (ArchObj (ASIDPool pool')))\<rbrace> set_object x2 (ArchObj (ASIDPool pool')) \<lbrace>\<lambda>xb s. obj_at (empty_table (set (arm_global_pts (arch_state s)))) word s\<rbrace> proof (prove)
goal:
No subgoals!