theory ArchArch_AC

lemma perform_page_table_invocation_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and invs and valid_pti page_table_invocation
                       and K (authorised_page_table_inv aag page_table_invocation)\<rbrace>
   perform_page_table_invocation page_table_invocation
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: perform_page_table_invocation_def
             cong: page_table_invocation.case_cong option.case_cong prod.case_cong
                   cap.case_cong arch_cap.case_cong) apply (wpsimp wp: store_pde_respects set_cap_integrity_autarch
                    store_pte_respects unmap_page_table_respects mapM_wp'
              simp: mapM_x_mapM authorised_page_table_inv_def cleanByVA_PoU_def) apply (auto simp: valid_pti_def valid_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and invs and valid_pti page_table_invocation and K (authorised_page_table_inv aag page_table_invocation)\<rbrace> perform_page_table_invocation page_table_invocation \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_page_table_inv aag page_table_invocation \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and invs and valid_pti page_table_invocation\<rbrace> perform_page_table_invocation page_table_invocation \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. authorised_page_table_inv aag page_table_invocation \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and invs and valid_pti page_table_invocation\<rbrace> case page_table_invocation of PageTableMap cap ct_slot pde pd_slot \<Rightarrow> do y <- set_cap cap ct_slot;
y <- store_pde pd_slot pde;
do_machine_op (cleanByVA_PoU pd_slot (addrFromPPtr pd_slot))
od | PageTableUnmap (ArchObjectCap (PageTableCap p mapped_address)) ct_slot \<Rightarrow> do y <- case mapped_address of None \<Rightarrow> return () | Some (asid, vaddr) \<Rightarrow> do y <- unmap_page_table asid vaddr p;
y <- mapM_x (swp store_pte InvalidPTE) [p , p + 4 .e. p + 2 ^ pt_bits - 1];
do_machine_op (cleanCacheRange_PoU p (p + 2 ^ pt_bits - 1) (addrFromPPtr p))
od;
cap <- liftM the_arch_cap (get_cap ct_slot);
set_cap (ArchObjectCap (update_map_data cap None)) ct_slot
od | PageTableUnmap (ArchObjectCap _) ct_slot \<Rightarrow> fail | PageTableUnmap _ ct_slot \<Rightarrow> fail \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>case page_table_invocation of PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) \<and> (case pde_ref2 pde of None \<Rightarrow> True | Some x \<Rightarrow> (is_subject aag \<circ> fst) x) \<and> pas_cap_cur_auth aag cap | PageTableUnmap cap cslot_ptr \<Rightarrow> is_subject aag (fst cslot_ptr) \<and> pas_cap_cur_auth aag cap \<and> (\<forall>p asid vspace_ref. cap = ArchObjectCap (PageTableCap p (Some (asid, vspace_ref))) \<longrightarrow> is_subject_asid aag asid \<and> (\<forall>x\<in>set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits))); integrity aag X st s; pas_refined aag s; invs s; valid_pti page_table_invocation s\<rbrakk> \<Longrightarrow> (\<forall>x a b xa xb. page_table_invocation = PageTableMap x (a, b) xa xb \<longrightarrow> is_subject aag a \<and> is_subject aag (xb && ~~ mask pd_bits)) \<and> (\<forall>x. (\<exists>a b. page_table_invocation = PageTableUnmap x (a, b)) \<longrightarrow> (\<forall>xa. x = ArchObjectCap xa \<longrightarrow> (\<forall>x xb. xa = PageTableCap x xb \<longrightarrow> (\<forall>a b. xb = Some (a, b) \<longrightarrow> is_subject_asid aag a \<and> b < kernel_base)))) proof (prove)
goal:
No subgoals!