kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchVSpace_AI

lemma pde_update_valid_vspace_objs:
  "[|valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))|]
   ==> valid_vspace_objs
         (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(ucast (p && mask pd_bits >> 2) := pde))))\<rparr>)" apply (cut_tac pde=pde and p=p in store_pde_vspace_objs_unmap) apply (clarsimp simp: valid_def) apply (erule allE[where x=s]) apply (clarsimp simp: split_def simpler_store_pde_def obj_at_def a_type_def
                  split: if_split_asm option.splits Structures_A.kernel_object.splits
                         arch_kernel_obj.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); \<lbrace>valid_vspace_objs and valid_pde pde and K (pde_ref pde = None)\<rbrace> store_pde p pde \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); \<forall>s. valid_vspace_objs s \<and> valid_pde pde s \<longrightarrow> (\<forall>x\<in>fst (store_pde p pde s). case x of (r, s') \<Rightarrow> valid_vspace_objs s')\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); valid_vspace_objs s \<and> valid_pde pde s \<longrightarrow> (\<forall>x\<in>fst (store_pde p pde s). case x of (r, s') \<Rightarrow> valid_vspace_objs s')\<rbrakk> \<Longrightarrow> valid_vspace_objs (s\<lparr>kheap := (kheap s)(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) := pde))))\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma mapM_x_swp_store_pte_invs [wp]:
  "\<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. (\<exists>\<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow>
                  valid_pte pte s) and
    (\<lambda>s. wellformed_pte pte) and
    (\<lambda>s. \<exists>slot. cte_wp_at
           (\<lambda>c. image (\<lambda>x. x && ~~ mask pt_bits) (set slots) \<subseteq> obj_refs c \<and>
                is_pt_cap c \<and> (pte = InvalidPTE \<or>
                               cap_asid c \<noteq> None)) slot s) and
   (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow>
              (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow>
                   (\<exists>p' cap.
                       caps_of_state s p' = Some cap \<and>
                       q \<in> obj_refs cap \<and>
                       vs_cap_ref cap =
                       Some
                        (VSRef (p && mask pt_bits >> 2) (Some APageTable) #
                         ref))))\<rbrace>
     mapM_x (swp store_pte pte) slots \<lbrace>\<lambda>_. invs\<rbrace>" by (simp add: mapM_x_mapM | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> valid_pte pte s) and (\<lambda>s. wellformed_pte pte) and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs c \<and> is_pt_cap c \<and> (pte = InvalidPTE \<or> cap_asid c \<noteq> None)) slot s) and (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> (\<exists>p' cap. caps_of_state s p' = Some cap \<and> q \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))))\<rbrace> mapM_x (swp store_pte pte) slots \<lbrace>\<lambda>_. invs\<rbrace>
theory ArchVSpace_AI

lemma mapM_x_swp_store_pde_invs_unmap:
  "\<lbrace>invs and K (\<forall>sl\<in>set slots.
                   ucast (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and
    (\<lambda>s. \<forall>sl \<in> set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and
    K (pde = InvalidPDE)\<rbrace>
  mapM_x (swp store_pde pde) slots \<lbrace>\<lambda>_. invs\<rbrace>" by (simp add: mapM_x_mapM | wp mapM_swp_store_pde_invs_unmap)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (\<forall>sl\<in>set slots. UCAST(32 \<rightarrow> 12) (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and K (pde = InvalidPDE)\<rbrace> mapM_x (swp store_pde pde) slots \<lbrace>\<lambda>_. invs\<rbrace>
theory ArchVSpace_AI

lemma vs_cap_ref_table_cap_ref_None:
  "vs_cap_ref x = None \<Longrightarrow> table_cap_ref x = None" by (simp add: vs_cap_ref_def table_cap_ref_simps
         split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_cap_ref x = None \<Longrightarrow> table_cap_ref x = None
theory ArchVSpace_AI

lemma master_cap_eq_is_pg_cap_eq:
  "cap_master_cap c = cap_master_cap d \<Longrightarrow> is_pg_cap c = is_pg_cap d" by (simp add: cap_master_cap_def is_pg_cap_def
         split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap c = cap_master_cap d \<Longrightarrow> is_pg_cap c = is_pg_cap d
theory ArchVSpace_AI

lemma master_cap_eq_is_device_cap_eq:
  "cap_master_cap c = cap_master_cap d \<Longrightarrow> cap_is_device c = cap_is_device d" by (simp add: cap_master_cap_def
         split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap c = cap_master_cap d \<Longrightarrow> cap_is_device c = cap_is_device d
theory ArchVSpace_AI

lemma set_vm_root_for_flush_invs:
  "\<lbrace>invs and K (asid \<le> mask asid_bits)\<rbrace>
  set_vm_root_for_flush pd asid \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: set_vm_root_for_flush_def) apply (wp hoare_drop_imps hoare_vcg_all_lift |wpc|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (asid \<le> mask local.asid_bits)\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>y. asid \<le> mask local.asid_bits)\<rbrace> do tcb <- gets cur_thread;
thread_root <- get_cap (tcb, tcb_cnode_index (Suc 0));
not_is_pd <- case thread_root of ArchObjectCap (PageDirectoryCap cur_pd None) \<Rightarrow> return True | ArchObjectCap (PageDirectoryCap cur_pd (Some x)) \<Rightarrow> return (cur_pd \<noteq> pd) | ArchObjectCap _ \<Rightarrow> return True | _ \<Rightarrow> return True;
if not_is_pd then do arm_context_switch pd asid;
return True
od else return False
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma flush_table_invs[wp]:
  "\<lbrace>invs and K (asid \<le> mask asid_bits)\<rbrace>
  flush_table pd asid vptr pt \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: flush_table_def) apply (wp dmo_invalidateLocalTLB_ASID_invs | simp)+ apply (simp only: if_cancel
            | clarsimp simp: machine_op_lift_def
                             machine_rest_lift_def split_def
            | wp set_vm_root_for_flush_invs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (asid \<le> mask local.asid_bits)\<rbrace> flush_table pd asid vptr pt \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>y. asid \<le> mask local.asid_bits)\<rbrace> do y <- assert (vptr && mask 20 = 0);
root_switched <- set_vm_root_for_flush pd asid;
maybe_hw_asid <- load_hw_asid asid;
when (\<exists>y. maybe_hw_asid = Some y) (do y <- do_machine_op (invalidateLocalTLB_ASID (the maybe_hw_asid));
when root_switched (gets cur_thread >>= set_vm_root)
od)
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B5 ()\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>a. invs\<rbrace>
 2. \<lbrace>?Q4\<rbrace> assert (vptr && mask 20 = 0) \<lbrace>?B5\<rbrace>
 3. \<And>s. (invs and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q4 s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma global_refs_arch_update_eq:
  "\<lbrakk> arm_globals_frame (f (arch_state s)) = arm_globals_frame (arch_state s);
     arm_global_pd (f (arch_state s)) = arm_global_pd (arch_state s);
     arm_global_pts (f (arch_state s)) = arm_global_pts (arch_state s) \<rbrakk>
       \<Longrightarrow> global_refs (arch_state_update f s) = global_refs s" by (simp add: global_refs_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arm_globals_frame (f (arch_state s)) = arm_globals_frame (arch_state s); arm_global_pd (f (arch_state s)) = arm_global_pd (arch_state s); arm_global_pts (f (arch_state s)) = arm_global_pts (arch_state s)\<rbrakk> \<Longrightarrow> global_refs (arch_state_update f s) = global_refs s
theory ArchVSpace_AI

lemma lookup_pd_slot_kernel_mappings_strg:
  "is_aligned pd pd_bits \<and> vptr < kernel_base
     \<and> vmsz_aligned vptr ARMSection
     \<longrightarrow> ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots" by (simp add: less_kernel_base_mapping_slots)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<and> vptr < kernel_base \<and> vmsz_aligned vptr ARMSection \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
theory ArchVSpace_AI

lemma cleanByVA_PoU_underlying_memory[wp]:
  "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> cleanByVA_PoU w q \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" by (clarsimp simp: cleanByVA_PoU_def machine_op_lift_def machine_rest_lift_def split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> cleanByVA_PoU w q \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>
theory ArchVSpace_AI

lemma final_cap_lift:
  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P (is_final_cap' cap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (is_final_cap' cap s)\<rbrace>" by (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state, rule x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (is_final_cap' cap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (is_final_cap' cap s)\<rbrace>
theory ArchVSpace_AI

lemma pd_shifting_again:
  "\<lbrakk> is_aligned pd pd_bits \<rbrakk>
    \<Longrightarrow> pd + (ucast (ae :: 12 word) << 2) && ~~ mask pd_bits = pd" apply (erule add_mask_lower_bits) apply (clarsimp simp add: nth_shiftl nth_ucast word_size
                            pd_bits_def pageBits_def
                     dest!: test_bit_size) apply arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned pd pd_bits \<Longrightarrow> pd + (UCAST(12 \<rightarrow> 'a) ae << 2) && ~~ mask pd_bits = pd proof (prove)
goal (1 subgoal):
 1. \<forall>n'\<ge>pd_bits. n' < LENGTH('a) \<longrightarrow> \<not> (UCAST(12 \<rightarrow> 'a) ae << 2) !! n' proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>14 \<le> n'; n' < LENGTH('a); n' - 2 < 12\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vs_lookup_pages_2ConsD:
  "((v # v' # vs) \<unrhd> p) s \<Longrightarrow>
   \<exists>p'. ((v' # vs) \<unrhd> p') s \<and> ((v' # vs, p') \<unrhd>1 (v # v' # vs, p)) s" apply (clarsimp simp: vs_lookup_pages_def) apply (erule rtranclE) apply (clarsimp simp: vs_asid_refs_def) apply (fastforce simp: vs_lookup_pages1_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((v # v' # vs) \<unrhd> p) s \<Longrightarrow> \<exists>p'. ((v' # vs) \<unrhd> p') s \<and> ((v' # vs, p'), v # v' # vs, p) \<in> vs_lookup_pages1 s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>((a, b), v # v' # vs, p) \<in> (vs_lookup_pages1 s)\<^sup>*; (a, b) \<in> vs_asid_refs (asid_table s)\<rbrakk> \<Longrightarrow> \<exists>p'. (v' # vs, p') \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<and> ((v' # vs, p'), v # v' # vs, p) \<in> vs_lookup_pages1 s proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); (a, b) = (v # v' # vs, p)\<rbrakk> \<Longrightarrow> \<exists>p'. (v' # vs, p') \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<and> ((v' # vs, p'), v # v' # vs, p) \<in> vs_lookup_pages1 s
 2. \<And>a b y. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); ((a, b), y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, v # v' # vs, p) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> \<exists>p'. (v' # vs, p') \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<and> ((v' # vs, p'), v # v' # vs, p) \<in> vs_lookup_pages1 s proof (prove)
goal (1 subgoal):
 1. \<And>a b y. \<lbrakk>(a, b) \<in> vs_asid_refs (asid_table s); ((a, b), y) \<in> (vs_lookup_pages1 s)\<^sup>*; (y, v # v' # vs, p) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> \<exists>p'. (v' # vs, p') \<in> (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<and> ((v' # vs, p'), v # v' # vs, p) \<in> vs_lookup_pages1 s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma flush_table_vs_lookup_pages[wp]:
  "\<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace>
   flush_table a b c d
   \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>" by (simp add: flush_table_def | wp mapM_UNIV_wp hoare_drop_imps | wpc
     | intro conjI impI)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> flush_table a b c d \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>
theory ArchVSpace_AI

lemma unmap_page_table_unmapped2:
  "\<lbrace>pspace_aligned and valid_vspace_objs and
      K (ref = [VSRef (vaddr >> 20) (Some APageDirectory),
               VSRef (asid && mask asid_low_bits) (Some AASIDPool),
               VSRef (ucast (asid_high_bits_of asid)) None]
           \<and> p = pt)\<rbrace>
     unmap_page_table asid vaddr pt
   \<lbrace>\<lambda>rv s. \<not> (ref \<rhd> p) s\<rbrace>" apply (rule hoare_gen_asm) apply simp apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_vspace_objs and K (ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt)\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>rv s. (ref, p) \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt \<Longrightarrow> \<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>rv s. (ref, p) \<notin> vs_lookup s\<rbrace> proof (prove)
goal (1 subgoal):
 1. ref = [VSRef (vaddr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<and> p = pt \<Longrightarrow> \<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> unmap_page_table asid vaddr pt \<lbrace>\<lambda>rv s. ([VSRef (vaddr >> 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\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma cacheRangeOp_lift[wp]:
  assumes o: "\<And>a b. \<lbrace>P\<rbrace> oper a b \<lbrace>\<lambda>_. P\<rbrace>"
  shows "\<lbrace>P\<rbrace> cacheRangeOp oper x y z \<lbrace>\<lambda>_. P\<rbrace>" apply (clarsimp simp: cacheRangeOp_def lineStart_def cacheLineBits_def cacheLine_def) apply (rule hoare_pre) apply (wp mapM_x_wp_inv o) apply (case_tac x, simp, wp o, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> cacheRangeOp oper x y z \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapM_x (\<lambda>(x, y). oper x y) (zip [x >> 5 << 5 , (x >> 5 << 5) + 0x20 .e. y >> 5 << 5] [z >> 5 << 5 , (z >> 5 << 5) + 0x20 .e. z + (y - x) >> 5 << 5]) \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q1\<rbrace> mapM_x (\<lambda>(x, y). oper x y) (zip [x >> 5 << 5 , (x >> 5 << 5) + 0x20 .e. y >> 5 << 5] [z >> 5 << 5 , (z >> 5 << 5) + 0x20 .e. z + (y - x) >> 5 << 5]) \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q1 s proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>P\<rbrace> case x of (x, xa) \<Rightarrow> oper x xa \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> P s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma cleanCacheRange_PoU_underlying_memory[wp]:
  "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> cleanCacheRange_PoU a b c \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" by (clarsimp simp: cleanCacheRange_PoU_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> cleanCacheRange_PoU a b c \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>
theory ArchVSpace_AI

lemma empty_table_pt_capI:
  "\<lbrakk>caps_of_state s p =
    Some (cap.ArchObjectCap (arch_cap.PageTableCap pt None));
    valid_table_caps s\<rbrakk>
   \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pt s" apply (case_tac p) apply (clarsimp simp: valid_table_caps_def simp del: imp_disjL) apply (drule spec)+ apply (erule impE, simp add: is_cap_simps)+ by assumption

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageTableCap pt None)); valid_table_caps s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pt s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s p = Some (ArchObjectCap (PageTableCap pt None)); valid_table_caps s; p = (a, b)\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pt s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap pt None)); \<forall>r a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_pd_cap cap \<or> is_pt_cap cap \<longrightarrow> cap_asid cap = None \<longrightarrow> r \<in> obj_refs cap \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) r s; p = (a, b)\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pt s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap pt None)); p = (a, b); caps_of_state s (?a3 a b, ?b5 a b) = Some (?cap7 a b) \<longrightarrow> is_pd_cap (?cap7 a b) \<or> is_pt_cap (?cap7 a b) \<longrightarrow> cap_asid (?cap7 a b) = None \<longrightarrow> ?r1 a b \<in> obj_refs (?cap7 a b) \<longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) (?r1 a b) s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pt s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>caps_of_state s (a, b) = Some (ArchObjectCap (PageTableCap pt None)); p = (a, b); obj_at (empty_table (set (second_level_tables (arch_state s)))) pt s\<rbrakk> \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pt s
theory ArchVSpace_AI

lemma no_irq_do_flush:
  "no_irq (do_flush a b c d)" apply (simp add: do_flush_def) apply (case_tac a) apply (wp no_irq_dsb no_irq_invalidateCacheRange_I no_irq_branchFlushRange no_irq_isb | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (do_flush a b c d) proof (prove)
goal (1 subgoal):
 1. no_irq (case a of Clean \<Rightarrow> cleanCacheRange_RAM b c d | Invalidate \<Rightarrow> invalidateCacheRange_RAM b c d | CleanInvalidate \<Rightarrow> cleanInvalidateCacheRange_RAM b c d | Unify \<Rightarrow> do cleanCacheRange_PoU b c d;
dsb;
invalidateCacheRange_I b c d;
branchFlushRange b c d;
isb
od) proof (prove)
goal (4 subgoals):
 1. a = Clean \<Longrightarrow> no_irq (case a of Clean \<Rightarrow> cleanCacheRange_RAM b c d | Invalidate \<Rightarrow> invalidateCacheRange_RAM b c d | CleanInvalidate \<Rightarrow> cleanInvalidateCacheRange_RAM b c d | Unify \<Rightarrow> do cleanCacheRange_PoU b c d;
dsb;
invalidateCacheRange_I b c d;
branchFlushRange b c d;
isb
od)
 2. a = Invalidate \<Longrightarrow> no_irq (case a of Clean \<Rightarrow> cleanCacheRange_RAM b c d | Invalidate \<Rightarrow> invalidateCacheRange_RAM b c d | CleanInvalidate \<Rightarrow> cleanInvalidateCacheRange_RAM b c d | Unify \<Rightarrow> do cleanCacheRange_PoU b c d;
dsb;
invalidateCacheRange_I b c d;
branchFlushRange b c d;
isb
od)
 3. a = CleanInvalidate \<Longrightarrow> no_irq (case a of Clean \<Rightarrow> cleanCacheRange_RAM b c d | Invalidate \<Rightarrow> invalidateCacheRange_RAM b c d | CleanInvalidate \<Rightarrow> cleanInvalidateCacheRange_RAM b c d | Unify \<Rightarrow> do cleanCacheRange_PoU b c d;
dsb;
invalidateCacheRange_I b c d;
branchFlushRange b c d;
isb
od)
 4. a = Unify \<Longrightarrow> no_irq (case a of Clean \<Rightarrow> cleanCacheRange_RAM b c d | Invalidate \<Rightarrow> invalidateCacheRange_RAM b c d | CleanInvalidate \<Rightarrow> cleanInvalidateCacheRange_RAM b c d | Unify \<Rightarrow> do cleanCacheRange_PoU b c d;
dsb;
invalidateCacheRange_I b c d;
branchFlushRange b c d;
isb
od) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma cleanCacheRange_PoU_respects_device_region[wp]:
  "\<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> cleanCacheRange_PoU a b c \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>" apply (clarsimp simp: cleanCacheRange_PoU_def cacheRangeOp_def) apply (wp mapM_x_wp |  wpc | clarsimp | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> cleanCacheRange_PoU a b c \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> mapM_x (\<lambda>(x, y). cleanByVA_PoU x y) (zip [lineStart a , lineStart a + word_of_nat cacheLine .e. lineStart b] [lineStart c , lineStart c + word_of_nat cacheLine .e. lineStart (c + (b - a))]) \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace> proof (prove)
goal:
No subgoals!