theory ArchArch_AC

lemma perform_page_invocation_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and K (authorised_page_inv aag pgi)
                       and valid_page_inv pgi and valid_vspace_objs
                       and pspace_aligned and is_subject aag  \<circ> cur_thread\<rbrace>
   perform_page_invocation pgi
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" proof - 
  (* does not work as elim rule with clarsimp, which hammers Ball in concl. *)
   have set_tl_subset_mp: "\<And>xs a. a \<in> set (tl xs) \<Longrightarrow> a \<in> set xs" by (case_tac xs; clarsimp) have hd_valid_slots:
    "\<And>a xs s. valid_slots (Inl (a, xs)) s \<Longrightarrow> hd xs \<in> set xs"
    "\<And>a xs s. valid_slots (Inr (a, xs)) s \<Longrightarrow> hd xs \<in> set xs" by (simp_all add: valid_slots_def) show ?thesis apply (simp add: perform_page_invocation_def mapM_discarded swp_def
                   valid_page_inv_def valid_unmap_def
                   authorised_page_inv_def authorised_slots_def
            split: page_invocation.split sum.split
                   arch_cap.split option.split,
         safe) apply (wp set_cap_integrity_autarch unmap_page_respects
                  mapM_x_and_const_wp[OF store_pte_respects] store_pte_respects
                  mapM_x_and_const_wp[OF store_pde_respects] store_pde_respects
               | elim conjE hd_valid_slots[THEN bspec[rotated]]
               | clarsimp dest!: set_tl_subset_mp
               | wpc )+ apply (clarsimp simp: cte_wp_at_caps_of_state cap_rights_update_def
                         acap_rights_update_def update_map_data_def is_pg_cap_def
                         valid_page_inv_def valid_cap_simps
                  dest!: cap_master_cap_eqDs) apply (drule (1) clas_caps_of_state) apply (simp add: cap_links_asid_slot_def label_owns_asid_slot_def) apply (auto dest: pas_refined_Control)[1] apply (wpsimp wp: set_mrs_integrity_autarch set_message_info_integrity_autarch
                 simp: ipc_buffer_has_auth_def)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>xs a. a \<in> set (tl xs) \<Longrightarrow> a \<in> set xs proof (state)
this:
?a \<in> set (tl ?xs) \<Longrightarrow> ?a \<in> set ?xs

goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>a xs s. valid_slots (Inl (a, xs)) s \<Longrightarrow> hd xs \<in> set xs) &&& (\<And>a xs s. valid_slots (Inr (a, xs)) s \<Longrightarrow> hd xs \<in> set xs) proof (state)
this:
valid_slots (Inl (?a1, ?xs1)) ?s1 \<Longrightarrow> hd ?xs1 \<in> set ?xs1
valid_slots (Inr (?a1, ?xs1)) ?s1 \<Longrightarrow> hd ?xs1 \<in> set ?xs1

goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x11 x12 a b x14 aa ba. pgi = PageMap x11 x12 (a, b) (Inl (aa, ba)) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>y. pas_cap_cur_auth aag x12 \<and> is_subject aag a \<and> (\<forall>a ab b. pte_ref aa = Some (a, ab, b) \<longrightarrow> (\<forall>aa\<in>b. \<forall>p\<in>ptr_range a ab. (pasSubject aag, aa, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set ba. is_subject aag (x && ~~ mask pt_bits))) and (cte_wp_at (is_arch_update x12) (a, b) and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) (a, b) or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs (Inl (aa, ba)) c s) (a, b) s)) and cte_wp_at is_pg_cap (a, b) and same_refs (Inl (aa, ba)) x12 and valid_slots (Inl (aa, ba)) and valid_cap x12 and (\<lambda>y. is_pg_cap x12 \<and> empty_refs (Inl (aa, ba)) \<and> x11 \<le> mask local.asid_bits \<and> x11 \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs (Inl (aa, ba))) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid x11 pd s)) and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> do y <- set_cap x12 (a, b);
y <- do flush <- pte_check_if_mapped (hd ba);
y <- store_pte (hd ba) aa;
_ <- mapM_x (\<lambda>y. store_pte y InvalidPTE) (tl ba);
y <- do_machine_op (cleanCacheRange_PoU (hd ba) (last_byte_pte (last ba)) (addrFromPPtr (hd ba)));
if flush then invalidate_tlb_by_asid x11 else return ()
od;
return []
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x11 x12 a b x14 aa ba. pgi = PageMap x11 x12 (a, b) (Inr (aa, ba)) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>y. pas_cap_cur_auth aag x12 \<and> is_subject aag a \<and> (\<forall>a ab b. pde_ref2 aa = Some (a, ab, b) \<longrightarrow> (\<forall>aa\<in>b. \<forall>p\<in>ptr_range a ab. (pasSubject aag, aa, pasObjectAbs aag p) \<in> pasPolicy aag)) \<and> (\<forall>x\<in>set ba. is_subject aag (x && ~~ mask pd_bits))) and (cte_wp_at (is_arch_update x12) (a, b) and (cte_wp_at (\<lambda>c. vs_cap_ref c = None) (a, b) or (\<lambda>s. cte_wp_at (\<lambda>c. same_refs (Inr (aa, ba)) c s) (a, b) s)) and cte_wp_at is_pg_cap (a, b) and same_refs (Inr (aa, ba)) x12 and valid_slots (Inr (aa, ba)) and valid_cap x12 and (\<lambda>y. is_pg_cap x12 \<and> empty_refs (Inr (aa, ba)) \<and> x11 \<le> mask local.asid_bits \<and> x11 \<noteq> 0) and (\<lambda>s. \<exists>a b. cte_wp_at (parent_for_refs (Inr (aa, ba))) (a, b) s) and (\<lambda>s. \<exists>pd. vspace_at_asid x11 pd s)) and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> do y <- set_cap x12 (a, b);
y <- do flush <- pde_check_if_mapped (hd ba);
y <- store_pde (hd ba) aa;
_ <- mapM_x (\<lambda>y. store_pde y InvalidPDE) (tl ba);
y <- do_machine_op (cleanCacheRange_PoU (hd ba) (last_byte_pde (last ba)) (addrFromPPtr (hd ba)));
if flush then invalidate_tlb_by_asid x11 else return ()
od;
return []
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>a b x31 x32 x33 x34 x35. pgi = PageUnmap (PageCap x31 x32 x33 x34 None) (a, b) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>y. pas_cap_cur_auth aag (ArchObjectCap (PageCap x31 x32 x33 x34 None)) \<and> is_subject aag a) and (\<lambda>s. cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 None))) (a, b) s \<and> s \<turnstile> ArchObjectCap (PageCap x31 x32 x33 x34 None)) and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> do cap <- liftM the_arch_cap (get_cap (a, b));
y <- set_cap (ArchObjectCap (update_map_data cap None)) (a, b);
return []
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>a b x31 x32 x33 x34 x35 aa ba. pgi = PageUnmap (PageCap x31 x32 x33 x34 (Some (aa, ba))) (a, b) \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (\<lambda>y. pas_cap_cur_auth aag (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba)))) \<and> is_subject aag a) and (\<lambda>s. 0 < aa \<and> is_aligned ba pageBits \<and> (x34 = ARMSuperSection \<longrightarrow> is_aligned ba 24) \<and> (x34 = ARMLargePage \<longrightarrow> is_aligned ba 16) \<and> (x34 = ARMSection \<longrightarrow> is_aligned ba 20) \<and> cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba))))) (a, b) s \<and> s \<turnstile> ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba)))) and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> do y <- unmap_page x34 aa ba x32;
cap <- liftM the_arch_cap (get_cap (a, b));
y <- set_cap (ArchObjectCap (update_map_data cap None)) (a, b);
return []
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 5. \<And>x31 x32 x33 x34 x35 x36. pgi = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (vspace_at_asid x36 x35 and (\<lambda>y. x36 \<le> mask local.asid_bits \<and> x36 \<noteq> 0)) and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> do y <- when (x32 < x33) (do root_switched <- set_vm_root_for_flush x35 x36;
y <- do_machine_op (do_flush x31 x32 x33 x34);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 6. \<And>x4. pgi = PageGetAddr x4 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> return [addrFromPPtr x4] \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a b x31 x32 x33 x34 aa ba s. \<lbrakk>pgi = PageUnmap (PageCap x31 x32 x33 x34 (Some (aa, ba))) (a, b); integrity aag X st s; pas_refined aag s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba)))); is_subject aag a; 0 < aa; is_aligned ba pageBits; x34 = ARMSuperSection \<longrightarrow> is_aligned ba 24; x34 = ARMLargePage \<longrightarrow> is_aligned ba 16; x34 = ARMSection \<longrightarrow> is_aligned ba 20; cte_wp_at ((=) (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba))))) (a, b) s; s \<turnstile> ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba))); valid_vspace_objs s; pspace_aligned s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> is_subject_asid aag aa \<and> vmsz_aligned ba x34 \<and> ba < kernel_base
 2. \<And>x31 x32 x33 x34 x35 x36. pgi = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (vspace_at_asid x36 x35 and (\<lambda>y. x36 \<le> mask local.asid_bits \<and> x36 \<noteq> 0)) and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> do y <- when (x32 < x33) (do root_switched <- set_vm_root_for_flush x35 x36;
y <- do_machine_op (do_flush x31 x32 x33 x34);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>x4. pgi = PageGetAddr x4 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> return [addrFromPPtr x4] \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a b x31 x32 x33 x34 aa ba s. \<lbrakk>pgi = PageUnmap (PageCap x31 x32 x33 x34 (Some (aa, ba))) (a, b); integrity aag X st s; pas_refined aag s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba)))); is_subject aag a; 0 < aa; is_aligned ba pageBits; x34 = ARMSuperSection \<longrightarrow> is_aligned ba 24; x34 = ARMLargePage \<longrightarrow> is_aligned ba 16; x34 = ARMSection \<longrightarrow> is_aligned ba 20; caps_of_state s (a, b) = Some (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba)))); valid_vspace_objs s; pspace_aligned s; is_subject aag (cur_thread s); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba)))); if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s; x33 \<in> valid_vm_rights; aa < 2 ^ local.asid_bits; vmsz_aligned ba x34; ba < kernel_base\<rbrakk> \<Longrightarrow> is_subject_asid aag aa
 2. \<And>x31 x32 x33 x34 x35 x36. pgi = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (vspace_at_asid x36 x35 and (\<lambda>y. x36 \<le> mask local.asid_bits \<and> x36 \<noteq> 0)) and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> do y <- when (x32 < x33) (do root_switched <- set_vm_root_for_flush x35 x36;
y <- do_machine_op (do_flush x31 x32 x33 x34);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>x4. pgi = PageGetAddr x4 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> return [addrFromPPtr x4] \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a b x31 x32 x33 x34 aa ba s. \<lbrakk>pgi = PageUnmap (PageCap x31 x32 x33 x34 (Some (aa, ba))) (a, b); integrity aag X st s; pas_refined aag s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba)))); is_subject aag a; 0 < aa; is_aligned ba pageBits; x34 = ARMSuperSection \<longrightarrow> is_aligned ba 24; x34 = ARMLargePage \<longrightarrow> is_aligned ba 16; x34 = ARMSection \<longrightarrow> is_aligned ba 20; valid_vspace_objs s; pspace_aligned s; is_subject aag (cur_thread s); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba)))); if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s; x33 \<in> valid_vm_rights; aa < 2 ^ local.asid_bits; vmsz_aligned ba x34; ba < kernel_base; cap_links_asid_slot aag (pasObjectAbs aag (fst (a, b))) (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba))))\<rbrakk> \<Longrightarrow> is_subject_asid aag aa
 2. \<And>x31 x32 x33 x34 x35 x36. pgi = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (vspace_at_asid x36 x35 and (\<lambda>y. x36 \<le> mask local.asid_bits \<and> x36 \<noteq> 0)) and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> do y <- when (x32 < x33) (do root_switched <- set_vm_root_for_flush x35 x36;
y <- do_machine_op (do_flush x31 x32 x33 x34);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>x4. pgi = PageGetAddr x4 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> return [addrFromPPtr x4] \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>a b x31 x32 x33 x34 aa ba s. \<lbrakk>pgi = PageUnmap (PageCap x31 x32 x33 x34 (Some (aa, ba))) (a, b); integrity aag X st s; pas_refined aag s; pas_cap_cur_auth aag (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba)))); is_subject aag a; 0 < aa; is_aligned ba pageBits; x34 = ARMSuperSection \<longrightarrow> is_aligned ba 24; x34 = ARMLargePage \<longrightarrow> is_aligned ba 16; x34 = ARMSection \<longrightarrow> is_aligned ba 20; valid_vspace_objs s; pspace_aligned s; is_subject aag (cur_thread s); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 (Some (aa, ba)))); if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s; x33 \<in> valid_vm_rights; aa < 2 ^ local.asid_bits; vmsz_aligned ba x34; ba < kernel_base; (pasSubject aag, Control, pasASIDAbs aag aa) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> is_subject_asid aag aa
 2. \<And>x31 x32 x33 x34 x35 x36. pgi = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (vspace_at_asid x36 x35 and (\<lambda>y. x36 \<le> mask local.asid_bits \<and> x36 \<noteq> 0)) and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> do y <- when (x32 < x33) (do root_switched <- set_vm_root_for_flush x35 x36;
y <- do_machine_op (do_flush x31 x32 x33 x34);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>x4. pgi = PageGetAddr x4 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> return [addrFromPPtr x4] \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33 x34 x35 x36. pgi = PageFlush x31 x32 x33 x34 x35 x36 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and (vspace_at_asid x36 x35 and (\<lambda>y. x36 \<le> mask local.asid_bits \<and> x36 \<noteq> 0)) and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> do y <- when (x32 < x33) (do root_switched <- set_vm_root_for_flush x35 x36;
y <- do_machine_op (do_flush x31 x32 x33 x34);
when root_switched (gets cur_thread >>= set_vm_root)
od);
return []
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>x4. pgi = PageGetAddr x4 \<Longrightarrow> \<lbrace>integrity aag X st and pas_refined aag and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> return [addrFromPPtr x4] \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>integrity aag X st and pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> perform_page_invocation pgi \<lbrace>\<lambda>_. integrity aag X st\<rbrace>

goal:
No subgoals!