theory ArchArch_AC

lemma perform_asid_control_invocation_respects:
  "\<lbrace>integrity aag X st and K (authorised_asid_control_inv aag aci)\<rbrace>
   perform_asid_control_invocation aci
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: perform_asid_control_invocation_def) apply (rule hoare_pre) apply (wpc, simp) apply (wpsimp wp: set_cap_integrity_autarch cap_insert_integrity_autarch
                     retype_region_integrity[where sz=12] hoare_weak_lift_imp) apply (clarsimp simp: authorised_asid_control_inv_def
                        ptr_range_def page_bits_def add.commute
                        range_cover_def obj_bits_api_def default_arch_object_def
                        pageBits_def word_bits_def) apply (subst is_aligned_neg_mask_eq[THEN sym], assumption) apply (simp add: and_mask_eq_iff_shiftr_0 mask_zero word_size_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (authorised_asid_control_inv aag aci)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and (\<lambda>y. authorised_asid_control_inv aag aci)\<rbrace> case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case aci of MakePool frame slot parent base \<Rightarrow> do delete_objects frame page_bits;
pcap <- get_cap parent;
set_cap (max_free_index_update pcap) parent;
retype_region frame 1 0 (ArchObject ASIDPoolObj) False;
cap_insert (ArchObjectCap $ ASIDPoolCap frame base) parent slot;
assert (base && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
asid_table' <- return (asid_table(asid_high_bits_of base \<mapsto> frame));
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table'\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. (integrity aag X st and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x3 x4. aci = MakePool x1 x2 x3 x4 \<Longrightarrow> \<lbrace>?R12 x1 x2 x3 x4\<rbrace> do y <- delete_objects x1 page_bits;
pcap <- get_cap x3;
y <- set_cap (max_free_index_update pcap) x3;
y <- retype_region x1 (Suc 0) 0 (ArchObject ASIDPoolObj) False;
y <- cap_insert (ArchObjectCap (ASIDPoolCap x1 x4)) x3 x2;
y <- assert (x4 && mask local.asid_low_bits = 0);
asid_table <- gets (arm_asid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := asid_table(asid_high_bits_of x4 \<mapsto> x1)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>s. (integrity aag X st and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> ?R12 x xa xb xc s proof (prove)
goal (1 subgoal):
 1. \<And>s. (integrity aag X st and (\<lambda>y. authorised_asid_control_inv aag aci)) s \<Longrightarrow> \<forall>x xa xb xc. aci = MakePool x xa xb xc \<longrightarrow> xc && mask local.asid_low_bits = 0 \<longrightarrow> (integrity aag X st s \<and> is_aligned x page_bits \<and> page_bits < word_bits \<and> word_size_bits \<le> page_bits \<and> (\<forall>p\<in>ptr_range x page_bits. is_subject aag p)) \<and> K (is_subject aag (fst xb)) s \<and> K (range_cover x 12 (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> (\<forall>x\<in>up_aligned_area x 12. is_subject aag x)) s \<and> K (is_subject aag (fst xb) \<and> is_subject aag (fst xa)) s \<and> (\<forall>asid'. asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of xc \<longrightarrow> is_subject_asid aag asid') proof (prove)
goal (1 subgoal):
 1. \<And>s x a b aa ba xa. \<lbrakk>integrity aag X st s; aci = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; is_aligned x 12; \<forall>asid. is_subject_asid aag asid; is_subject aag aa; \<forall>x\<in>{x..x + 0xFFF}. is_subject aag x\<rbrakk> \<Longrightarrow> word_size_bits \<le> 12 \<and> unat (x && mask 12 >> 12) = 0 proof (prove)
goal (1 subgoal):
 1. \<And>s x a b aa ba xa. \<lbrakk>integrity aag X st s; aci = MakePool x (a, b) (aa, ba) xa; xa && mask local.asid_low_bits = 0; is_subject aag a; is_aligned x 12; \<forall>asid. is_subject_asid aag asid; is_subject aag aa; \<forall>x\<in>{x..x + 0xFFF}. is_subject aag x\<rbrakk> \<Longrightarrow> word_size_bits \<le> 12 \<and> unat ((x && ~~ mask 12) && mask 12 >> 12) = 0 proof (prove)
goal:
No subgoals!