theory VSpace_R

lemma performPageDirectoryInvocation_corres:
  "page_directory_invocation_map pdi pdi' \<Longrightarrow>
   corres dc (invs and valid_pdi pdi)
             (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj'
               and cur_tcb' and valid_arch_state')
             (perform_page_directory_invocation pdi) (performPageDirectoryInvocation pdi')" apply (simp add: perform_page_directory_invocation_def performPageDirectoryInvocation_def) apply (corres_cases_both simp: page_directory_invocation_map_def) apply (clarsimp simp: page_directory_invocation_map_def) apply (rule corres_when, simp) apply (rule corres_split[OF setVMRootForFlush_corres]) apply (rule corres_split[OF corres_machine_op]) apply (rule doFlush_corres) apply (rule corres_when, simp) apply (rule corres_split[OF getCurThread_corres]) apply clarsimp apply (rule setVMRoot_corres) apply wp+ apply (simp flip: cur_tcb_def) apply (wp hoare_drop_imps) apply (simp flip: cur_tcb'_def) apply (wp hoare_drop_imps)+ apply (auto simp: valid_pdi_def invs_vspace_objs[simplified] page_directory_invocation_map_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. page_directory_invocation_map pdi pdi' \<Longrightarrow> corres dc (invs and valid_pdi pdi) (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') (perform_page_directory_invocation pdi) (performPageDirectoryInvocation pdi') proof (prove)
goal (1 subgoal):
 1. page_directory_invocation_map pdi pdi' \<Longrightarrow> corres dc (invs and valid_pdi pdi) (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') (case pdi of ARM_A.PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- set_vm_root_for_flush pd asid;
do_machine_op $ do_flush typ start end pstart;
when root_switched $ gets cur_thread >>= set_vm_root
od | ARM_A.PageDirectoryNothing \<Rightarrow> return ()) (case pdi' of ARM_H.PageDirectoryNothing \<Rightarrow> return () | ARM_H.PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> when (start < end) $ do root_switched <- setVMRootForFlush pd asid;
doMachineOp $ doFlush typ start end pstart;
when root_switched $ getCurThread >>= setVMRoot
od) proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 x21 x22 x23 x24 x25 x26. \<lbrakk>page_directory_invocation_map pdi pdi'; pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush x21 x22 x23 x24 x25 x26\<rbrakk> \<Longrightarrow> corres dc (?Q'224 x11 x12 x13 x14 x15 x16 x21 x22 x23 x24 x25 x26) (?Q226 x11 x12 x13 x14 x15 x16 x21 x22 x23 x24 x25 x26) (when (x12 < x13) $ do root_switched <- set_vm_root_for_flush x15 x16;
do_machine_op $ do_flush x11 x12 x13 x14;
when root_switched $ gets cur_thread >>= set_vm_root
od) (when (x22 < x23) $ do root_switched <- setVMRootForFlush x25 x26;
doMachineOp $ doFlush x21 x22 x23 x24;
when root_switched $ getCurThread >>= setVMRoot
od)
 2. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> ?Q'224 x xa xb xc xd xe xf xg xh xi xj xk s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 3. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> ?Q226 x xa xb xc xd xe xf xg xh xi xj xk s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> corres dc (?Q'224 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16) (?Q226 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16) (when (x12 < x13) (do root_switched <- set_vm_root_for_flush x15 x16;
y <- do_machine_op (do_flush x11 x12 x13 x14);
when root_switched (gets cur_thread >>= set_vm_root)
od)) (when (x12 < x13) (do root_switched <- setVMRootForFlush x15 x16;
y <- doMachineOp (doFlush (flush_type_map x11) x12 x13 x14);
when root_switched (getCurThread >>= setVMRoot)
od))
 2. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> ?Q'224 x xa xb xc xd xe xf xg xh xi xj xk s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 3. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> ?Q226 x xa xb xc xd xe xf xg xh xi xj xk s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (3 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> corres dc (?P258 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16) (?P'257 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16) (do root_switched <- set_vm_root_for_flush x15 x16;
y <- do_machine_op (do_flush x11 x12 x13 x14);
when root_switched (gets cur_thread >>= set_vm_root)
od) (do root_switched <- setVMRootForFlush x15 x16;
y <- doMachineOp (doFlush (flush_type_map x11) x12 x13 x14);
when root_switched (getCurThread >>= setVMRoot)
od)
 2. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> ?P258 x xa xb xc xd xe xf xg xh xi xj xk s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 3. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> ?P'257 x xa xb xc xd xe xf xg xh xi xj xk s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> corres dc (?R261 x11 x12 x13 x14 x15 x16 rv) (?R'261 x11 x12 x13 x14 x15 x16 rv') (do y <- do_machine_op (do_flush x11 x12 x13 x14);
when rv (gets cur_thread >>= set_vm_root)
od) (do y <- doMachineOp (doFlush (flush_type_map x11) x12 x13 x14);
when rv' (getCurThread >>= setVMRoot)
od)
 2. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>?R261 x11 x12 x13 x14 x15 x16\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>?R'261 x11 x12 x13 x14 x15 x16\<rbrace>
 4. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 5. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> corres_underlying Id False True (?r'271 x11 x12 x13 x14 x15 x16 rv rv') (\<lambda>_. True) (\<lambda>_. True) (do_flush x11 x12 x13 x14) (doFlush (flush_type_map x11) x12 x13 x14)
 2. \<And>x11 x12 x13 x14 x15 x16 rv rv' rva rv'a. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'; ?r'271 x11 x12 x13 x14 x15 x16 rv rv' rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?R271 x11 x12 x13 x14 x15 x16 rv rv' rva) (?R'271 x11 x12 x13 x14 x15 x16 rv rv' rv'a) (when rv (gets cur_thread >>= set_vm_root)) (when rv' (getCurThread >>= setVMRoot))
 3. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>?R271 x11 x12 x13 x14 x15 x16 rv rv'\<rbrace>
 4. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace> doMachineOp (doFlush (flush_type_map x11) x12 x13 x14) \<lbrace>?R'271 x11 x12 x13 x14 x15 x16 rv rv'\<rbrace>
 5. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace>
 6. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace>
 7. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 8. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv rv' rva rv'a. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?R271 x11 x12 x13 x14 x15 x16 rv rv' rva) (?R'271 x11 x12 x13 x14 x15 x16 rv rv' rv'a) (when rv (gets cur_thread >>= set_vm_root)) (when rv' (getCurThread >>= setVMRoot))
 2. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>?R271 x11 x12 x13 x14 x15 x16 rv rv'\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace> doMachineOp (doFlush (flush_type_map x11) x12 x13 x14) \<lbrace>?R'271 x11 x12 x13 x14 x15 x16 rv rv'\<rbrace>
 4. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace>
 5. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace>
 6. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 7. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (7 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv rv' rva rv'a. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> corres dc (?P282 x11 x12 x13 x14 x15 x16 rv rv' rva) (?P'284 x11 x12 x13 x14 x15 x16 rv rv' rv'a) (gets cur_thread >>= set_vm_root) (getCurThread >>= setVMRoot)
 2. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>\<lambda>rva x. rv \<longrightarrow> ?P282 x11 x12 x13 x14 x15 x16 rv rv' rva x\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace> doMachineOp (doFlush (flush_type_map x11) x12 x13 x14) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ?P'284 x11 x12 x13 x14 x15 x16 rv rv' rv'a x\<rbrace>
 4. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace>
 5. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace>
 6. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 7. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (9 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv rv' rva rv'a rvb rv'b. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'; dc rva rv'a; rvb = rv'b\<rbrakk> \<Longrightarrow> corres dc (?R287 x11 x12 x13 x14 x15 x16 rv rv' rva rv'a rvb) (?R'287 x11 x12 x13 x14 x15 x16 rv rv' rva rv'a rv'b) (set_vm_root rvb) (setVMRoot rv'b)
 2. \<And>x11 x12 x13 x14 x15 x16 rv rv' rva rv'a. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q288 x11 x12 x13 x14 x15 x16 rv rv' rva\<rbrace> gets cur_thread \<lbrace>?R287 x11 x12 x13 x14 x15 x16 rv rv' rva rv'a\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16 rv rv' rva rv'a. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'289 x11 x12 x13 x14 x15 x16 rv rv' rv'a\<rbrace> getCurThread \<lbrace>?R'287 x11 x12 x13 x14 x15 x16 rv rv' rva rv'a\<rbrace>
 4. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>\<lambda>rva x. rv \<longrightarrow> ((\<lambda>_. True) and ?Q288 x11 x12 x13 x14 x15 x16 rv rv' rva) x\<rbrace>
 5. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace> doMachineOp (doFlush (flush_type_map x11) x12 x13 x14) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q'289 x11 x12 x13 x14 x15 x16 rv rv' rv'a) x\<rbrace>
 6. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace>
 7. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace>
 8. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 9. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (9 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv' rv'b. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> corres dc (?R287 x11 x12 x13 x14 x15 x16 rv' rv' () () rv'b) (?R'287 x11 x12 x13 x14 x15 x16 rv' rv' () () rv'b) (set_vm_root rv'b) (setVMRoot rv'b)
 2. \<And>x11 x12 x13 x14 x15 x16 rv rv' rva rv'a. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q288 x11 x12 x13 x14 x15 x16 rv rv' rva\<rbrace> gets cur_thread \<lbrace>?R287 x11 x12 x13 x14 x15 x16 rv rv' rva rv'a\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16 rv rv' rva rv'a. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'289 x11 x12 x13 x14 x15 x16 rv rv' rv'a\<rbrace> getCurThread \<lbrace>?R'287 x11 x12 x13 x14 x15 x16 rv rv' rva rv'a\<rbrace>
 4. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>\<lambda>rva x. rv \<longrightarrow> ((\<lambda>_. True) and ?Q288 x11 x12 x13 x14 x15 x16 rv rv' rva) x\<rbrace>
 5. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace> doMachineOp (doFlush (flush_type_map x11) x12 x13 x14) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q'289 x11 x12 x13 x14 x15 x16 rv rv' rv'a) x\<rbrace>
 6. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace>
 7. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace>
 8. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 9. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv rv' rva rv'a. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q288 x11 x12 x13 x14 x15 x16 rv rv' rva\<rbrace> gets cur_thread \<lbrace>\<lambda>a. tcb_at a and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs\<rbrace>
 2. \<And>x11 x12 x13 x14 x15 x16 rv rv' rva rv'a. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'289 x11 x12 x13 x14 x15 x16 rv rv' rv'a\<rbrace> getCurThread \<lbrace>\<lambda>a. pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' a and no_0_obj'\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>\<lambda>rva x. rv \<longrightarrow> ((\<lambda>_. True) and ?Q288 x11 x12 x13 x14 x15 x16 rv rv' rva) x\<rbrace>
 4. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace> doMachineOp (doFlush (flush_type_map x11) x12 x13 x14) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and ?Q'289 x11 x12 x13 x14 x15 x16 rv rv' rv'a) x\<rbrace>
 5. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace>
 6. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace>
 7. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 8. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>\<lambda>rva x. rv \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. (tcb_at (cur_thread a) and valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs) a)) x\<rbrace>
 2. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace> doMachineOp (doFlush (flush_type_map x11) x12 x13 x14) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' (ksCurThread a) and no_0_obj') a)) x\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace>
 4. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace>
 5. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 6. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q273 x11 x12 x13 x14 x15 x16 rv'\<rbrace> do_machine_op (do_flush x11 x12 x13 x14) \<lbrace>\<lambda>rva x. rv' \<longrightarrow> cur_tcb x \<and> valid_arch_state x \<and> valid_objs x \<and> valid_asid_map x \<and> unique_table_refs (caps_of_state x) \<and> valid_vs_lookup x \<and> valid_global_objs x \<and> pspace_aligned x \<and> pspace_distinct x \<and> valid_vspace_objs x\<rbrace>
 2. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace> doMachineOp (doFlush (flush_type_map x11) x12 x13 x14) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' (ksCurThread a) and no_0_obj') a)) x\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q273 x11 x12 x13 x14 x15 x16 rv\<rbrace>
 4. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace>
 5. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 6. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace> doMachineOp (doFlush (flush_type_map x11) x12 x13 x14) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> ((\<lambda>_. True) and (\<lambda>a. (pspace_aligned' and pspace_distinct' and valid_arch_state' and tcb_at' (ksCurThread a) and no_0_obj') a)) x\<rbrace>
 2. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. cur_tcb s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_asid_map s \<and> unique_table_refs (caps_of_state s) \<and> valid_vs_lookup s \<and> valid_global_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_vspace_objs s)\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace>
 4. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 5. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12 x13 x14 x15 x16 rv rv'. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16; rv = rv'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace> doMachineOp (doFlush (flush_type_map x11) x12 x13 x14) \<lbrace>\<lambda>rv'a x. rv' \<longrightarrow> pspace_aligned' x \<and> pspace_distinct' x \<and> valid_arch_state' x \<and> cur_tcb' x \<and> no_0_obj' x\<rbrace>
 2. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q267 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> set_vm_root_for_flush x15 x16 \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. cur_tcb s \<and> valid_arch_state s \<and> valid_objs s \<and> valid_asid_map s \<and> unique_table_refs (caps_of_state s) \<and> valid_vs_lookup s \<and> valid_global_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_vspace_objs s)\<rbrace>
 3. \<And>x11 x12 x13 x14 x15 x16. \<lbrakk>pdi = ARM_A.PageDirectoryFlush x11 x12 x13 x14 x15 x16; pdi' = ARM_H.PageDirectoryFlush (flush_type_map x11) x12 x13 x14 x15 x16\<rbrakk> \<Longrightarrow> \<lbrace>?Q'266 x11 x12 x13 x14 x15 x16 (flush_type_map x11) x12 x13 x14 x15 x16\<rbrace> setVMRootForFlush x15 x16 \<lbrace>\<lambda>rv'. (\<lambda>_. True) and ?Q'274 x11 x12 x13 x14 x15 x16 rv'\<rbrace>
 4. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (cur_tcb and vspace_at_asid xk xj and K (xk \<noteq> 0 \<and> xk \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and ?Q267 x xa xb xc xd xe xf xg xh xi xj xk) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 5. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>xf xg xh xi xj xk. pdi' = ARM_H.PageDirectoryFlush xf xg xh xi xj xk \<longrightarrow> xg < xh \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'266 x xa xb xc xd xe xf xg xh xi xj xk) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> xa < xb \<longrightarrow> (cur_tcb and vspace_at_asid xe xd and K (xe \<noteq> 0 \<and> xe \<le> mask local.asid_bits) and valid_asid_map and valid_vs_lookup and valid_vspace_objs and valid_global_objs and unique_table_refs \<circ> caps_of_state and valid_arch_state and pspace_aligned and pspace_distinct and (\<lambda>a. True \<and> cur_tcb a \<and> valid_arch_state a \<and> valid_objs a \<and> (valid_asid_map and K (xe \<le> mask local.asid_bits)) a \<and> unique_table_refs (caps_of_state a) \<and> valid_vs_lookup a \<and> valid_global_objs a \<and> pspace_aligned a \<and> pspace_distinct a \<and> valid_vspace_objs a)) s)) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True))
 2. \<And>s s'. \<lbrakk>page_directory_invocation_map pdi pdi'; (invs and valid_pdi pdi) s; (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_arch_state') s'; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (\<forall>x xa xb xc xd xe. pdi = ARM_A.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> xa < xb \<longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>a. True \<and> pspace_aligned' a \<and> pspace_distinct' a \<and> valid_arch_state' a \<and> cur_tcb' a \<and> no_0_obj' a)) s')) \<and> (pdi = ARM_A.PageDirectoryNothing \<longrightarrow> (pdi' = ARM_H.PageDirectoryNothing \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. pdi' = ARM_H.PageDirectoryFlush x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal:
No subgoals!