kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchVSpace_AI

lemma dmb_underlying_memory[wp]:
  "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace>
   dmb
   \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" by (clarsimp simp: dmb_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> dmb \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>
theory ArchVSpace_AI

lemma invalidateLocalTLB_underlying_memory:
  "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace>
   invalidateLocalTLB
   \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" by (clarsimp simp: invalidateLocalTLB_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> invalidateLocalTLB \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>
theory ArchVSpace_AI

lemma dmo_invalidateLocalTLB_ASID_invs[wp]:
  "\<lbrace>invs\<rbrace> do_machine_op (invalidateLocalTLB_ASID asid) \<lbrace>\<lambda>_. invs\<rbrace>" apply (wp dmo_invs) apply safe apply (drule use_valid) apply (rule invalidateLocalTLB_ASID_underlying_memory) apply fastforce+ apply(erule (1) use_valid[OF _ invalidateLocalTLB_ASID_irq_masks]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op (invalidateLocalTLB_ASID asid) \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (invalidateLocalTLB_ASID asid m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s proof (prove)
goal (2 subgoals):
 1. \<And>s m b p. \<lbrakk>invs s; ((), b) \<in> fst (invalidateLocalTLB_ASID asid m); underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (invalidateLocalTLB_ASID asid (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (4 subgoals):
 1. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P19 s m b p\<rbrace> invalidateLocalTLB_ASID asid \<lbrace>?Q19 s m b p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P19 s m b p m
 3. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p; ?Q19 s m b p () b\<rbrakk> \<Longrightarrow> in_user_frame p s
 4. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (invalidateLocalTLB_ASID asid (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> underlying_memory m (?p23 s m b p) = ?um23 s m b p
 2. \<And>s m b p. \<lbrakk>invs s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b (?p23 s m b p) = ?um23 s m b p\<rbrakk> \<Longrightarrow> in_user_frame p s
 3. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (invalidateLocalTLB_ASID asid (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (1 subgoal):
 1. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (invalidateLocalTLB_ASID asid (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma load_hw_asid_invs[wp]: "\<lbrace>invs\<rbrace> load_hw_asid asid \<lbrace>\<lambda>y. invs\<rbrace>" by (simp add: load_hw_asid_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> load_hw_asid asid \<lbrace>\<lambda>y. invs\<rbrace>
theory ArchVSpace_AI

lemma invalidate_tlb_by_asid_invs[wp]:
  "\<lbrace>invs\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>_. invs\<rbrace>" apply (clarsimp simp: invalidate_tlb_by_asid_def | wp | wpc)+ apply (rule_tac Q="K invs" in hoare_post_imp) apply (clarsimp|wp load_hw_asid_invs)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> load_hw_asid asid \<lbrace>\<lambda>maybe_hw_asid s. (maybe_hw_asid = None \<longrightarrow> invs s) \<and> ((\<exists>x. maybe_hw_asid = Some x) \<longrightarrow> invs s)\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. K invs rv s \<Longrightarrow> (rv = None \<longrightarrow> invs s) \<and> ((\<exists>x. rv = Some x) \<longrightarrow> invs s)
 2. \<lbrace>?Q\<rbrace> load_hw_asid asid \<lbrace>K invs\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma invalidate_hw_asid_entry_pd_still_uniq[wp]:
  "\<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s\<rbrace>
     invalidate_hw_asid_entry y
   \<lbrace>\<lambda>rv s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s\<rbrace>" 
   (* this could be generalised to other functions on pd_at_* *)
   apply (simp add: vspace_at_asid_def pd_at_uniq_def
                   invalidate_hw_asid_entry_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s\<rbrace> invalidate_hw_asid_entry y \<lbrace>\<lambda>rv s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s\<rbrace> invalidate_hw_asid_entry y \<lbrace>\<lambda>rv s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<longrightarrow> pd \<notin> ran (map_option snd \<circ> arm_asid_map (arch_state s) |` (- {asid}))\<rbrace> do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(y := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>rv s. \<forall>pd. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<longrightarrow> pd \<notin> ran (map_option snd \<circ> arm_asid_map (arch_state s) |` (- {asid}))\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma invalidate_asid_entry_arch_state [wp]:
  "\<lbrace>valid_arch_state\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" apply (simp add: invalidate_asid_entry_def invalidate_asid_def invalidate_hw_asid_entry_def) apply (wp load_hw_asid_wp) apply (clarsimp simp: valid_arch_state_def is_inv_None_upd comp_upd_simp simp del: fun_upd_apply) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
y <- when (\<exists>y. maybe_hw_asid = Some y) (do hw_asid_map <- gets (arm_hwasid_table \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := hw_asid_map(the maybe_hw_asid := None)\<rparr>\<rparr>)
od);
asid_map <- gets (arm_asid_map \<circ> arch_state);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(asid := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_arch_state s \<Longrightarrow> (if \<exists>y. map_option fst (arm_asid_map (arch_state s) asid) = Some y then \<lambda>sa. valid_arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>, arch_state := arch_state (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>)\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) (sa\<lparr>arch_state := arch_state sa\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) sa)(the (map_option fst (arm_asid_map (arch_state s) asid)) := None)\<rparr>\<rparr>))(asid := None)\<rparr>\<rparr>) else (\<lambda>s. valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid := None)\<rparr>\<rparr>))) s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma flush_space_asid_map[wp]:
  "\<lbrace>valid_asid_map\<rbrace> flush_space space \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>" apply (simp add: flush_space_def) apply (wp load_hw_asid_wp | wpc | simp | rule_tac Q="\<lambda>_. valid_asid_map" in hoare_strengthen_post)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> flush_space space \<lbrace>\<lambda>rv. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map\<rbrace> do maybe_hw_asid <- load_hw_asid space;
y <- do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op $ invalidateLocalTLB_ASID hw_asid
od \<lbrace>\<lambda>rv. valid_asid_map\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma flush_space_arch_objs[wp]:
  "\<lbrace>valid_vspace_objs\<rbrace> flush_space space \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" apply (simp add: flush_space_def) apply (wp load_hw_asid_wp | wpc | simp | rule_tac Q="\<lambda>_. valid_vspace_objs" in hoare_strengthen_post)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs\<rbrace> flush_space space \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs\<rbrace> do maybe_hw_asid <- load_hw_asid space;
y <- do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op $ invalidateLocalTLB_ASID hw_asid
od \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma flush_space_pd_at_asid [wp]:
  "\<lbrace>vspace_at_asid a pd\<rbrace> flush_space asid \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace>" apply (simp add: flush_space_def) apply (wp load_hw_asid_wp|wpc|rule_tac Q="\<lambda>_. vspace_at_asid a pd" in hoare_strengthen_post|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid a pd\<rbrace> flush_space asid \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid a pd\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
y <- do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op $ invalidateLocalTLB_ASID hw_asid
od \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma flush_space_arch [wp]:
  "\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (arch_state s)\<rbrace>" apply (simp add: flush_space_def) apply (wp load_hw_asid_wp|wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (arch_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> do maybe_hw_asid <- load_hw_asid asid;
y <- do_machine_op cleanCaches_PoU;
case maybe_hw_asid of None \<Rightarrow> return () | Some hw_asid \<Rightarrow> do_machine_op $ invalidateLocalTLB_ASID hw_asid
od \<lbrace>\<lambda>rv s. P (arch_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (arch_state s) \<Longrightarrow> (map_option fst (arm_asid_map (arch_state s) asid) = None \<longrightarrow> P (arch_state s)) \<and> (\<forall>x. map_option fst (arm_asid_map (arch_state s) asid) = Some x \<longrightarrow> P (arch_state s)) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma pd_at_asid_arch_up':
  "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s)
    \<Longrightarrow> vspace_at_asid asid pd (arch_state_update f s) = vspace_at_asid asid pd s" by (clarsimp simp add: vspace_at_asid_def vs_lookup_def vs_lookup1_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_asid_table (f (arch_state s)) = asid_table s \<Longrightarrow> vspace_at_asid asid pd (arch_state_update f s) = vspace_at_asid asid pd s
theory ArchVSpace_AI

lemma pd_at_asid_arch_up:
  "vspace_at_asid asid pd (s\<lparr>arch_state := arch_state s \<lparr>arm_asid_map := a, arm_hwasid_table := b\<rparr>\<rparr>) =
  vspace_at_asid asid pd s" by (simp add: pd_at_asid_arch_up')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vspace_at_asid asid pd (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := a, arm_hwasid_table := b\<rparr>\<rparr>) = vspace_at_asid asid pd s
theory ArchVSpace_AI

lemma invalidate_I_PoU_underlying_memory[wp]:
  "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace>
   invalidate_I_PoU
   \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" by (clarsimp simp: invalidate_I_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> invalidate_I_PoU \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>
theory ArchVSpace_AI

lemma clean_D_PoU_underlying_memory[wp]:
  "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace>
   clean_D_PoU
   \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" by (clarsimp simp: clean_D_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> clean_D_PoU \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>
theory ArchVSpace_AI

lemma dmo_cleanCaches_PoU_invs[wp]: "\<lbrace>invs\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y. invs\<rbrace>" apply (wp dmo_invs) apply clarsimp apply safe apply (simp add: use_valid[OF _ cleanCaches_PoU_underlying_memory_inv[where P="\<lambda>x. x = v" for v]]) apply(erule(1) use_valid[OF _ cleanCaches_PoU_irq_masks]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (cleanCaches_PoU m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s proof (prove)
goal (1 subgoal):
 1. \<And>s m b. \<lbrakk>invs s; ((), b) \<in> fst (cleanCaches_PoU m)\<rbrakk> \<Longrightarrow> (\<forall>p. in_user_frame p s \<or> underlying_memory b p = underlying_memory m p) \<and> (m = machine_state s \<longrightarrow> (\<forall>irq. interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks b irq \<or> irq_masks b irq = irq_masks (machine_state s) irq)) proof (prove)
goal (2 subgoals):
 1. \<And>s m b p. \<lbrakk>invs s; ((), b) \<in> fst (cleanCaches_PoU m); underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> in_user_frame p s
 2. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (cleanCaches_PoU (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal (1 subgoal):
 1. \<And>s m b irq. \<lbrakk>invs s; ((), b) \<in> fst (cleanCaches_PoU (machine_state s)); interrupt_states s irq = IRQInactive; \<not> irq_masks b irq; irq_masks (machine_state s) irq\<rbrakk> \<Longrightarrow> irq_masks b irq proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma flush_space_invs[wp]: "\<lbrace>invs\<rbrace> flush_space asid \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: flush_space_def | wp | wpc)+ apply (rule_tac Q="K invs" in hoare_post_imp, (simp|wp)+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> flush_space asid \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>maybe_hw_asid. \<lbrace>?B1 maybe_hw_asid\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>a b. (maybe_hw_asid = None \<longrightarrow> invs b) \<and> ((\<exists>x. maybe_hw_asid = Some x) \<longrightarrow> invs b)\<rbrace>
 2. \<lbrace>?Q\<rbrace> load_hw_asid asid \<lbrace>?B1\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma asid_high_bits_of_or:
 "x \<le> 2^asid_low_bits - 1 \<Longrightarrow> asid_high_bits_of (base || x) = asid_high_bits_of base" apply (rule word_eqI) apply (drule le_2p_upper_bits) apply (simp add: asid_low_bits_def word_bits_def) apply (simp add: asid_high_bits_of_def word_size nth_ucast nth_shiftr asid_low_bits_def word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> asid_high_bits_of (base || x) = asid_high_bits_of base proof (prove)
goal (1 subgoal):
 1. \<And>n. x \<le> 2 ^ local.asid_low_bits - 1 \<Longrightarrow> n < size (asid_high_bits_of (base || x)) \<longrightarrow> asid_high_bits_of (base || x) !! n = asid_high_bits_of base !! n proof (prove)
goal (2 subgoals):
 1. \<And>n. local.asid_low_bits < LENGTH(32)
 2. \<And>n. \<forall>n'\<ge>local.asid_low_bits. n' < LENGTH(32) \<longrightarrow> \<not> x !! n' \<Longrightarrow> n < size (asid_high_bits_of (base || x)) \<longrightarrow> asid_high_bits_of (base || x) !! n = asid_high_bits_of base !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<forall>n'\<ge>local.asid_low_bits. n' < LENGTH(32) \<longrightarrow> \<not> x !! n' \<Longrightarrow> n < size (asid_high_bits_of (base || x)) \<longrightarrow> asid_high_bits_of (base || x) !! n = asid_high_bits_of base !! n proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vs_lookup_clear_asid_table:
  "(rf \<rhd> p) (s\<lparr>arch_state := arch_state s
                \<lparr>arm_asid_table := (arm_asid_table (arch_state s))
                   (pptr := None)\<rparr>\<rparr>)
        \<longrightarrow> (rf \<rhd> p) s" apply (simp add: vs_lookup_def vs_lookup1_def) apply (rule impI, erule subsetD[rotated]) apply (rule Image_mono[OF order_refl]) apply (simp add: vs_asid_refs_def graph_of_def) apply (rule image_mono) apply (clarsimp split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rf \<rhd> p) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(pptr := None)\<rparr>\<rparr>) \<longrightarrow> (rf \<rhd> p) s proof (prove)
goal (1 subgoal):
 1. (rf, p) \<in> {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko)}\<^sup>* `` vs_asid_refs ((asid_table s)(pptr := None)) \<longrightarrow> (rf, p) \<in> {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko)}\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko)}\<^sup>* `` vs_asid_refs ((asid_table s)(pptr := None)) \<subseteq> {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs ko)}\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. vs_asid_refs ((asid_table s)(pptr := None)) \<subseteq> vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` {(x, y). (if x = pptr then None else asid_table s x) = Some y} \<subseteq> (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` {(x, y). asid_table s x = Some y} proof (prove)
goal (1 subgoal):
 1. {(x, y). (if x = pptr then None else asid_table s x) = Some y} \<subseteq> {(x, y). asid_table s x = Some y} proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vs_lookup_pages_clear_asid_table:
  "(rf \<unrhd> p) (s\<lparr>arch_state := arch_state s
                \<lparr>arm_asid_table := (arm_asid_table (arch_state s))
                   (pptr := None)\<rparr>\<rparr>)
   \<Longrightarrow> (rf \<unrhd> p) s" apply (simp add: vs_lookup_pages_def vs_lookup_pages1_def) apply (erule subsetD[rotated]) apply (rule Image_mono[OF order_refl]) apply (simp add: vs_asid_refs_def graph_of_def) apply (rule image_mono) apply (clarsimp split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (rf \<unrhd> p) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(pptr := None)\<rparr>\<rparr>) \<Longrightarrow> (rf \<unrhd> p) s proof (prove)
goal (1 subgoal):
 1. (rf, p) \<in> {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs_pages ko)}\<^sup>* `` vs_asid_refs ((asid_table s)(pptr := None)) \<Longrightarrow> (rf, p) \<in> {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs_pages ko)}\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs_pages ko)}\<^sup>* `` vs_asid_refs ((asid_table s)(pptr := None)) \<subseteq> {((rs, p), rs', p'). \<exists>ko. ko_at ko p s \<and> (\<exists>r. rs' = r # rs \<and> (r, p') \<in> vs_refs_pages ko)}\<^sup>* `` vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. vs_asid_refs ((asid_table s)(pptr := None)) \<subseteq> vs_asid_refs (asid_table s) proof (prove)
goal (1 subgoal):
 1. (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` {(x, y). (if x = pptr then None else asid_table s x) = Some y} \<subseteq> (\<lambda>x. case x of (r, p) \<Rightarrow> ([VSRef (UCAST(7 \<rightarrow> 32) r) None], p)) ` {(x, y). asid_table s x = Some y} proof (prove)
goal (1 subgoal):
 1. {(x, y). (if x = pptr then None else asid_table s x) = Some y} \<subseteq> {(x, y). asid_table s x = Some y} proof (prove)
goal:
No subgoals!