theory VSpace_R

lemma unmapPageTable_corres:
  "corres dc
          (invs and valid_etcbs and page_table_at pt and
           K (0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask asid_bits))
          (valid_arch_state' and pspace_aligned' and pspace_distinct'
            and no_0_obj' and cur_tcb' and valid_objs')
          (unmap_page_table asid vptr pt)
          (unmapPageTable asid vptr pt)" apply (clarsimp simp: unmapPageTable_def unmap_page_table_def ignoreFailure_def const_def cong: option.case_cong) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF pageTableMapped_corres]) apply (simp add: case_option_If2 split del: if_split) apply (rule corres_if2[OF refl]) apply (rule corres_split) apply (rule storePDE_corres') apply (simp add:pde_relation_aligned_def) apply (rule corres_split[OF corres_machine_op]) apply (rule corres_Id, rule refl, simp) apply (wp no_fail_cleanByVA_PoU) apply (rule flushTable_corres) apply (wpsimp wp: store_pde_pd_at_asid store_pde_vspace_objs_invalid)+ apply (rule hoare_vcg_conj_lift) apply (simp add: store_pde_def) apply (wp set_pd_vs_lookup_unmap)+ apply (rule corres_trivial, simp) apply (wp page_table_mapped_wp) apply (wp hoare_drop_imps)[1] apply (clarsimp simp: invs_def valid_state_def valid_pspace_def
                         valid_arch_caps_def word_gt_0) apply (frule (1) page_directory_pde_at_lookupI) apply (auto elim: simp: empty_table_def valid_pde_mappings_def pde_ref_def obj_at_def
                     vs_refs_pages_def graph_of_def split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_etcbs and typ_at (AArch APageTable) pt and K (0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') (unmap_page_table asid vptr pt) (unmapPageTable asid vptr pt) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') (do pdOpt <- page_table_mapped asid vptr pt;
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- store_pde (lookup_pd_slot pd vptr) ARM_A.InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot pd vptr) (addrFromPPtr (lookup_pd_slot pd vptr)));
flush_table pd asid vptr pt
od
od) (do maybePD <- pageTableMapped asid vptr pt;
case maybePD of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- storePDE (lookup_pd_slot pd vptr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot pd vptr) (addrFromPPtr (lookup_pd_slot pd vptr)));
flushTable pd asid vptr
od
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q4 ?Q'4 (do pdOpt <- page_table_mapped asid vptr pt;
case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- store_pde (lookup_pd_slot pd vptr) ARM_A.InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot pd vptr) (addrFromPPtr (lookup_pd_slot pd vptr)));
flush_table pd asid vptr pt
od
od) (do maybePD <- pageTableMapped asid vptr pt;
case maybePD of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- storePDE (lookup_pd_slot pd vptr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot pd vptr) (addrFromPPtr (lookup_pd_slot pd vptr)));
flushTable pd asid vptr
od
od)
 2. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q4 s
 3. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> ?Q'4 s proof (prove)
goal (5 subgoals):
 1. \<And>pdOpt. corres dc (?R8 pdOpt) (?R'8 pdOpt) (case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- store_pde (lookup_pd_slot pd vptr) ARM_A.InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot pd vptr) (addrFromPPtr (lookup_pd_slot pd vptr)));
flush_table pd asid vptr pt
od) (case pdOpt of None \<Rightarrow> return () | Some pd \<Rightarrow> do y <- storePDE (lookup_pd_slot pd vptr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot pd vptr) (addrFromPPtr (lookup_pd_slot pd vptr)));
flushTable pd asid vptr
od)
 2. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>?R8\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>?R'8\<rbrace>
 4. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 5. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>pdOpt. corres dc (?R8 pdOpt) (?R'8 pdOpt) (if \<exists>y. pdOpt = Some y then do y <- store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)));
flush_table (the pdOpt) asid vptr pt
od else return ()) (if \<exists>y. pdOpt = Some y then do y <- storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)));
flushTable (the pdOpt) asid vptr
od else return ())
 2. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>?R8\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>?R'8\<rbrace>
 4. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 5. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. \<And>pdOpt. corres dc (?P13 pdOpt) (?P'13 pdOpt) (do y <- store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE;
y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)));
flush_table (the pdOpt) asid vptr pt
od) (do y <- storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE;
y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)));
flushTable (the pdOpt) asid vptr
od)
 2. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 3. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> ?P13 pdOpt x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> ?P'13 pdOpt x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 5. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 6. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (9 subgoals):
 1. \<And>pdOpt. corres (?r'17 pdOpt) (?P17 pdOpt) (?P'17 pdOpt) (store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE) (storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE)
 2. \<And>pdOpt y ya. ?r'17 pdOpt y ya \<Longrightarrow> corres dc (?R17 pdOpt y) (?R'17 pdOpt ya) (do y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)));
flush_table (the pdOpt) asid vptr pt
od) (do y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)));
flushTable (the pdOpt) asid vptr
od)
 3. \<And>pdOpt. \<lbrace>?Q17 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>?R17 pdOpt\<rbrace>
 4. \<And>pdOpt. \<lbrace>?Q'17 pdOpt\<rbrace> storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE \<lbrace>?R'17 pdOpt\<rbrace>
 5. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 6. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (?P17 pdOpt and ?Q17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 7. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (?P'17 pdOpt and ?Q'17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 8. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 9. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (9 subgoals):
 1. \<And>pdOpt. pde_relation_aligned (lookup_pd_slot (the pdOpt) vptr >> 2) ARM_A.InvalidPDE ARM_H.InvalidPDE
 2. \<And>pdOpt y ya. dc y ya \<Longrightarrow> corres dc (?R17 pdOpt y) (?R'17 pdOpt ya) (do y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)));
flush_table (the pdOpt) asid vptr pt
od) (do y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)));
flushTable (the pdOpt) asid vptr
od)
 3. \<And>pdOpt. \<lbrace>?Q17 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>?R17 pdOpt\<rbrace>
 4. \<And>pdOpt. \<lbrace>?Q'17 pdOpt\<rbrace> storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE \<lbrace>?R'17 pdOpt\<rbrace>
 5. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 6. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and ?Q17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 7. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 8. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 9. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>pdOpt y ya. dc y ya \<Longrightarrow> corres dc (?R17 pdOpt y) (?R'17 pdOpt ya) (do y <- do_machine_op (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)));
flush_table (the pdOpt) asid vptr pt
od) (do y <- doMachineOp (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)));
flushTable (the pdOpt) asid vptr
od)
 2. \<And>pdOpt. \<lbrace>?Q17 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>?R17 pdOpt\<rbrace>
 3. \<And>pdOpt. \<lbrace>?Q'17 pdOpt\<rbrace> storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE \<lbrace>?R'17 pdOpt\<rbrace>
 4. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 5. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and ?Q17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 7. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 8. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (11 subgoals):
 1. \<And>pdOpt y ya. dc y ya \<Longrightarrow> corres_underlying Id False True (?r'24 pdOpt y ya) (\<lambda>_. True) (\<lambda>_. True) (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr))) (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)))
 2. \<And>pdOpt y ya yb yc. \<lbrakk>dc y ya; ?r'24 pdOpt y ya yb yc\<rbrakk> \<Longrightarrow> corres dc (?R24 pdOpt y ya yb) (?R'24 pdOpt y ya yc) (flush_table (the pdOpt) asid vptr pt) (flushTable (the pdOpt) asid vptr)
 3. \<And>pdOpt y ya. dc y ya \<Longrightarrow> \<lbrace>?Q26 pdOpt y\<rbrace> do_machine_op (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr))) \<lbrace>?R24 pdOpt y ya\<rbrace>
 4. \<And>pdOpt y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'27 pdOpt ya\<rbrace> doMachineOp (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr))) \<lbrace>?R'24 pdOpt y ya\<rbrace>
 5. \<And>pdOpt. \<lbrace>?Q17 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q26 pdOpt y\<rbrace>
 6. \<And>pdOpt. \<lbrace>?Q'17 pdOpt\<rbrace> storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'27 pdOpt ya\<rbrace>
 7. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 8. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and ?Q17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 10. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>pdOpt y ya. \<lbrakk>dc y ya; True\<rbrakk> \<Longrightarrow> no_fail (\<lambda>_. True) (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr)))
 2. \<And>pdOpt y ya yb yc. \<lbrakk>dc y ya; True\<rbrakk> \<Longrightarrow> corres dc (?R24 pdOpt y ya yb) (?R'24 pdOpt y ya yc) (flush_table (the pdOpt) asid vptr pt) (flushTable (the pdOpt) asid vptr)
 3. \<And>pdOpt y ya. dc y ya \<Longrightarrow> \<lbrace>?Q26 pdOpt y\<rbrace> do_machine_op (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr))) \<lbrace>?R24 pdOpt y ya\<rbrace>
 4. \<And>pdOpt y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'27 pdOpt ya\<rbrace> doMachineOp (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr))) \<lbrace>?R'24 pdOpt y ya\<rbrace>
 5. \<And>pdOpt. \<lbrace>?Q17 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q26 pdOpt y\<rbrace>
 6. \<And>pdOpt. \<lbrace>?Q'17 pdOpt\<rbrace> storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'27 pdOpt ya\<rbrace>
 7. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 8. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and ?Q17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 9. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 10. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>pdOpt y ya yb yc. \<lbrakk>dc y ya; True\<rbrakk> \<Longrightarrow> corres dc (?R24 pdOpt y ya yb) (?R'24 pdOpt y ya yc) (flush_table (the pdOpt) asid vptr pt) (flushTable (the pdOpt) asid vptr)
 2. \<And>pdOpt y ya. dc y ya \<Longrightarrow> \<lbrace>?Q26 pdOpt y\<rbrace> do_machine_op (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr))) \<lbrace>?R24 pdOpt y ya\<rbrace>
 3. \<And>pdOpt y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'27 pdOpt ya\<rbrace> doMachineOp (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr))) \<lbrace>?R'24 pdOpt y ya\<rbrace>
 4. \<And>pdOpt. \<lbrace>?Q17 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q26 pdOpt y\<rbrace>
 5. \<And>pdOpt. \<lbrace>?Q'17 pdOpt\<rbrace> storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'27 pdOpt ya\<rbrace>
 6. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 7. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and ?Q17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 8. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 9. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 10. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (9 subgoals):
 1. \<And>pdOpt y ya. dc y ya \<Longrightarrow> \<lbrace>?Q26 pdOpt y\<rbrace> do_machine_op (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr))) \<lbrace>\<lambda>yb. pspace_aligned and valid_objs and valid_arch_state and cur_tcb and vspace_at_asid asid (the pdOpt) and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and K (is_aligned vptr (pageBitsForSize ARMSection) \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)\<rbrace>
 2. \<And>pdOpt y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'27 pdOpt ya\<rbrace> doMachineOp (cleanByVA_PoU (lookup_pd_slot (the pdOpt) vptr) (addrFromPPtr (lookup_pd_slot (the pdOpt) vptr))) \<lbrace>\<lambda>yc. pspace_aligned' and pspace_distinct' and no_0_obj' and valid_arch_state' and cur_tcb'\<rbrace>
 3. \<And>pdOpt. \<lbrace>?Q17 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>\<lambda>y. (\<lambda>_. True) and ?Q26 pdOpt y\<rbrace>
 4. \<And>pdOpt. \<lbrace>?Q'17 pdOpt\<rbrace> storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE \<lbrace>\<lambda>ya. (\<lambda>_. True) and ?Q'27 pdOpt ya\<rbrace>
 5. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 6. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and ?Q17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 7. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 8. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 9. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (7 subgoals):
 1. \<And>pdOpt. \<lbrace>?P'153 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>\<lambda>rv s. valid_vs_lookup s \<and> valid_global_objs s \<and> unique_table_refs (caps_of_state s) \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0\<rbrace>
 2. \<And>pdOpt. \<lbrace>?Q'17 pdOpt\<rbrace> storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE \<lbrace>\<lambda>ya. (\<lambda>_. True) and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_arch_state' s \<and> cur_tcb' s)\<rbrace>
 3. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 4. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and (\<lambda>s. True \<and> pspace_aligned s \<and> ((\<lambda>s. wellformed_pde ARM_A.InvalidPDE) and valid_objs) s \<and> valid_arch_state s \<and> cur_tcb s \<and> vspace_at_asid asid (the pdOpt) s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> ?P'153 pdOpt s)) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 5. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 6. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 7. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>pdOpt. \<lbrace>?P156 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>\<lambda>rv. valid_vs_lookup\<rbrace>
 2. \<And>pdOpt. \<lbrace>?P'156 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>\<lambda>rv s. valid_global_objs s \<and> unique_table_refs (caps_of_state s) \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0\<rbrace>
 3. \<And>pdOpt. \<lbrace>?Q'17 pdOpt\<rbrace> storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE \<lbrace>\<lambda>ya. (\<lambda>_. True) and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_arch_state' s \<and> cur_tcb' s)\<rbrace>
 4. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 5. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and (\<lambda>s. True \<and> pspace_aligned s \<and> ((\<lambda>s. wellformed_pde ARM_A.InvalidPDE) and valid_objs) s \<and> valid_arch_state s \<and> cur_tcb s \<and> vspace_at_asid asid (the pdOpt) s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> ?P156 pdOpt s \<and> ?P'156 pdOpt s)) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 7. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 8. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (8 subgoals):
 1. \<And>pdOpt. \<lbrace>?P156 pdOpt\<rbrace> do pd <- get_pd (lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits);
set_pd (lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits) (pd(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the pdOpt) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE))
od \<lbrace>\<lambda>rv. valid_vs_lookup\<rbrace>
 2. \<And>pdOpt. \<lbrace>?P'156 pdOpt\<rbrace> store_pde (lookup_pd_slot (the pdOpt) vptr) ARM_A.InvalidPDE \<lbrace>\<lambda>rv s. valid_global_objs s \<and> unique_table_refs (caps_of_state s) \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0\<rbrace>
 3. \<And>pdOpt. \<lbrace>?Q'17 pdOpt\<rbrace> storePDE (lookup_pd_slot (the pdOpt) vptr) ARM_H.InvalidPDE \<lbrace>\<lambda>ya. (\<lambda>_. True) and (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_arch_state' s \<and> cur_tcb' s)\<rbrace>
 4. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 5. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and (\<lambda>s. True \<and> pspace_aligned s \<and> ((\<lambda>s. wellformed_pde ARM_A.InvalidPDE) and valid_objs) s \<and> valid_arch_state s \<and> cur_tcb s \<and> vspace_at_asid asid (the pdOpt) s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> ?P156 pdOpt s \<and> ?P'156 pdOpt s)) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 6. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'17 pdOpt) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 7. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 8. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>pdOpt. corres dc (?Q13 pdOpt) (?Q'13 pdOpt) (return ()) (return ())
 2. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and (\<lambda>s. True \<and> pspace_aligned s \<and> ((\<lambda>s. wellformed_pde ARM_A.InvalidPDE) and valid_objs) s \<and> valid_arch_state s \<and> cur_tcb s \<and> vspace_at_asid asid (the pdOpt) s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>pd. ako_at (PageDirectory pd) (lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits) s \<longrightarrow> (valid_vs_lookup and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the pdOpt) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE)))) \<subseteq> vs_refs_pages ko) (lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits)) s) \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pd. obj_at (empty_table (set (second_level_tables (arch_state s)))) (lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pd) (lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the pdOpt) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s \<and> unique_table_refs (caps_of_state s) \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q13 pdOpt x)\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_arch_state' s \<and> cur_tcb' s)) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> ?Q'13 pdOpt x)\<rbrace>
 4. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 5. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q8\<rbrace> page_table_mapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the pdOpt) vptr) and pspace_aligned and valid_etcbs and (\<lambda>s. True \<and> pspace_aligned s \<and> ((\<lambda>s. wellformed_pde ARM_A.InvalidPDE) and valid_objs) s \<and> valid_arch_state s \<and> cur_tcb s \<and> vspace_at_asid asid (the pdOpt) s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>pd. ako_at (PageDirectory pd) (lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits) s \<longrightarrow> (valid_vs_lookup and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the pdOpt) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE)))) \<subseteq> vs_refs_pages ko) (lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits)) s) \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pd. obj_at (empty_table (set (second_level_tables (arch_state s)))) (lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pd) (lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the pdOpt) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. lookup_pd_slot (the pdOpt) vptr && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s \<and> unique_table_refs (caps_of_state s) \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> True)\<rbrace>
 2. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_arch_state' s \<and> cur_tcb' s)) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> True)\<rbrace>
 3. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and ?Q8) s
 4. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q'8\<rbrace> pageTableMapped asid vptr pt \<lbrace>\<lambda>pdOpt x. ((\<exists>y. pdOpt = Some y) \<longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>s. True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_arch_state' s \<and> cur_tcb' s)) x) \<and> ((\<nexists>y. pdOpt = Some y) \<longrightarrow> True)\<rbrace>
 2. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and (\<lambda>s. valid_vspace_objs s \<and> pspace_aligned s \<and> (([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> ((\<exists>y. None = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the None) vptr) and pspace_aligned and valid_etcbs and (\<lambda>s. True \<and> pspace_aligned s \<and> ((\<lambda>s. wellformed_pde ARM_A.InvalidPDE) and valid_objs) s \<and> valid_arch_state s \<and> cur_tcb s \<and> vspace_at_asid asid (the None) s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>pd. ako_at (PageDirectory pd) (lookup_pd_slot (the None) vptr && ~~ mask pd_bits) s \<longrightarrow> (valid_vs_lookup and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the None) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE)))) \<subseteq> vs_refs_pages ko) (lookup_pd_slot (the None) vptr && ~~ mask pd_bits)) s) \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pd. obj_at (empty_table (set (second_level_tables (arch_state s)))) (lookup_pd_slot (the None) vptr && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pd) (lookup_pd_slot (the None) vptr && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the None) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. lookup_pd_slot (the None) vptr && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s \<and> unique_table_refs (caps_of_state s) \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s) \<and> ((\<nexists>y. None = Some y) \<longrightarrow> True)) \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> ((\<exists>y. Some pd = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the (Some pd)) vptr) and pspace_aligned and valid_etcbs and (\<lambda>s. True \<and> pspace_aligned s \<and> ((\<lambda>s. wellformed_pde ARM_A.InvalidPDE) and valid_objs) s \<and> valid_arch_state s \<and> cur_tcb s \<and> vspace_at_asid asid (the (Some pd)) s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot (the (Some pd)) vptr && ~~ mask pd_bits) s \<longrightarrow> (valid_vs_lookup and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the (Some pd)) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE)))) \<subseteq> vs_refs_pages ko) (lookup_pd_slot (the (Some pd)) vptr && ~~ mask pd_bits)) s) \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pda. obj_at (empty_table (set (second_level_tables (arch_state s)))) (lookup_pd_slot (the (Some pd)) vptr && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pda) (lookup_pd_slot (the (Some pd)) vptr && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the (Some pd)) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. lookup_pd_slot (the (Some pd)) vptr && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s \<and> unique_table_refs (caps_of_state s) \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s) \<and> ((\<nexists>y. Some pd = Some y) \<longrightarrow> True)))) s
 3. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and valid_etcbs and typ_at (AArch APageTable) pt and (\<lambda>y. 0 < asid \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits) and (\<lambda>s. valid_vspace_objs s \<and> pspace_aligned s \<and> (([VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None], pt) \<notin> vs_lookup s \<longrightarrow> ((\<exists>y. None = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the None) vptr) and pspace_aligned and valid_etcbs and (\<lambda>s. True \<and> pspace_aligned s \<and> ((\<lambda>s. wellformed_pde ARM_A.InvalidPDE) and valid_objs) s \<and> valid_arch_state s \<and> cur_tcb s \<and> vspace_at_asid asid (the None) s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>pd. ako_at (PageDirectory pd) (lookup_pd_slot (the None) vptr && ~~ mask pd_bits) s \<longrightarrow> (valid_vs_lookup and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the None) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE)))) \<subseteq> vs_refs_pages ko) (lookup_pd_slot (the None) vptr && ~~ mask pd_bits)) s) \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pd. obj_at (empty_table (set (second_level_tables (arch_state s)))) (lookup_pd_slot (the None) vptr && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pd) (lookup_pd_slot (the None) vptr && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the None) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. lookup_pd_slot (the None) vptr && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s \<and> unique_table_refs (caps_of_state s) \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s) \<and> ((\<nexists>y. None = Some y) \<longrightarrow> True)) \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned pd pd_bits \<longrightarrow> ((\<exists>y. Some pd = Some y) \<longrightarrow> (pde_at (lookup_pd_slot (the (Some pd)) vptr) and pspace_aligned and valid_etcbs and (\<lambda>s. True \<and> pspace_aligned s \<and> ((\<lambda>s. wellformed_pde ARM_A.InvalidPDE) and valid_objs) s \<and> valid_arch_state s \<and> cur_tcb s \<and> vspace_at_asid asid (the (Some pd)) s \<and> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (\<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot (the (Some pd)) vptr && ~~ mask pd_bits) s \<longrightarrow> (valid_vs_lookup and obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the (Some pd)) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE)))) \<subseteq> vs_refs_pages ko) (lookup_pd_slot (the (Some pd)) vptr && ~~ mask pd_bits)) s) \<and> (valid_global_objs and valid_global_refs and valid_arch_state and (\<lambda>s. (\<forall>pda. obj_at (empty_table (set (second_level_tables (arch_state s)))) (lookup_pd_slot (the (Some pd)) vptr && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pda) (lookup_pd_slot (the (Some pd)) vptr && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (lookup_pd_slot (the (Some pd)) vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE))))) \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. lookup_pd_slot (the (Some pd)) vptr && ~~ mask pd_bits \<in> obj_refs cap) slot s))) s \<and> unique_table_refs (caps_of_state s) \<and> is_aligned vptr 20 \<and> asid \<le> mask local.asid_bits \<and> asid \<noteq> 0)) s) \<and> ((\<nexists>y. Some pd = Some y) \<longrightarrow> True)))) s
 2. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (pspace_aligned' and pspace_distinct' and (\<lambda>s. True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_arch_state' s \<and> cur_tcb' s)) s \<and> True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_etcbs s; typ_at (AArch APageTable) pt s; asid \<noteq> 0; is_aligned vptr 20; asid \<le> mask local.asid_bits; vspace_at_asid asid pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pd_bits\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vptr) s \<and> (\<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE)))) \<subseteq> vs_refs_pages ko) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s) \<and> ((\<forall>pda. obj_at (empty_table (set (second_level_tables (arch_state s)))) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. lookup_pd_slot pd vptr && ~~ mask pd_bits \<in> obj_refs cap) (a, b) s))
 2. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (pspace_aligned' and pspace_distinct' and (\<lambda>s. True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_arch_state' s \<and> cur_tcb' s)) s \<and> True)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pd. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_vs_lookup s; valid_table_caps s; unique_table_caps (caps_of_state s); unique_table_refs (caps_of_state s); valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_etcbs s; typ_at (AArch APageTable) pt s; asid \<noteq> 0; is_aligned vptr 20; asid \<le> mask local.asid_bits; vspace_at_asid asid pd s; typ_at (AArch APageDirectory) pd s; is_aligned pd pd_bits; pde_at (lookup_pd_slot pd (?vptr241 s pd)) s\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vptr) s \<and> (\<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE)))) \<subseteq> vs_refs_pages ko) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s) \<and> ((\<forall>pda. obj_at (empty_table (set (second_level_tables (arch_state s)))) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<and> ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory (pda(UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) := ARM_A.InvalidPDE))))) \<or> (\<exists>a b. cte_wp_at (\<lambda>cap. lookup_pd_slot pd vptr && ~~ mask pd_bits \<in> obj_refs cap) (a, b) s))
 2. \<And>s. (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and cur_tcb' and valid_objs') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and (\<lambda>s. (pspace_aligned' and pspace_distinct' and (\<lambda>s. True \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_arch_state' s \<and> cur_tcb' s)) s \<and> True)) s proof (prove)
goal:
No subgoals!