kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchVSpace_AI

lemma valid_vspace_objs_unmap_strg:
  "valid_vspace_objs s \<longrightarrow>
   valid_vspace_objs(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(ptr := None)\<rparr>\<rparr>)" apply (clarsimp simp: valid_vspace_objs_def) apply (drule vs_lookup_clear_asid_table [rule_format]) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vspace_objs s \<longrightarrow> valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(ptr := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (rs \<rhd> p) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(ptr := None)\<rparr>\<rparr>); ako_at ao p s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>p rs ao. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); ako_at ao p s; (rs \<rhd> p) s\<rbrakk> \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma valid_vs_lookup_unmap_strg:
  "valid_vs_lookup s \<longrightarrow>
   valid_vs_lookup(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(ptr := None)\<rparr>\<rparr>)" apply (clarsimp simp: valid_vs_lookup_def) apply (drule vs_lookup_pages_clear_asid_table) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_vs_lookup s \<longrightarrow> valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(ptr := None)\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>p ref. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); (ref \<unrhd> p) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(ptr := None)\<rparr>\<rparr>)\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal (1 subgoal):
 1. \<And>p ref. \<lbrakk>\<forall>p ref. (ref \<unrhd> p) s \<longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref); (ref \<unrhd> p) s\<rbrakk> \<Longrightarrow> ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma invalidate_asid_entry_asid_map_None_inv:
  "\<lbrace>\<lambda>s. arm_asid_map (arch_state s) y = None\<rbrace>
  invalidate_asid_entry (base + x)
  \<lbrace>\<lambda>_ s. arm_asid_map (arch_state s) y = None\<rbrace>" apply (simp add: invalidate_asid_entry_def invalidate_asid_def
                   invalidate_hw_asid_entry_def) apply (wp load_hw_asid_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. arm_asid_map (arch_state s) y = None\<rbrace> invalidate_asid_entry (base + x) \<lbrace>\<lambda>_ s. arm_asid_map (arch_state s) y = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. arm_asid_map (arch_state s) y = None\<rbrace> do maybe_hw_asid <- load_hw_asid (base + x);
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(base + x := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_ s. arm_asid_map (arch_state s) y = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. arm_asid_map (arch_state s) y = None \<Longrightarrow> (if \<exists>y. map_option fst (arm_asid_map (arch_state s) (base + x)) = Some y then \<lambda>sa. arm_asid_map (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) (base + x))) := 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) (base + x))) := 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) (base + x))) := None)\<rparr>\<rparr>))(base + x := None)\<rparr>\<rparr>)) y = None else (\<lambda>s. arm_asid_map (arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(base + x := None)\<rparr>\<rparr>)) y = None)) s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma asid_low_bits_word_bits:
  "asid_low_bits < word_bits" by (simp add: asid_low_bits_def word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. local.asid_low_bits < word_bits
theory ArchVSpace_AI

lemma valid_global_objs_arch_update:
  "arm_global_pd (f (arch_state s)) = arm_global_pd (arch_state s)
    \<and> arm_global_pts (f (arch_state s)) = arm_global_pts (arch_state s)
     \<Longrightarrow> valid_global_objs (arch_state_update f s) = valid_global_objs s" by (simp add: valid_global_objs_def second_level_tables_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_global_pd (f (arch_state s)) = arm_global_pd (arch_state s) \<and> arm_global_pts (f (arch_state s)) = arm_global_pts (arch_state s) \<Longrightarrow> valid_global_objs (arch_state_update f s) = valid_global_objs s
theory ArchVSpace_AI

lemma hw_asid_Some [wp]:
  "\<lbrace>valid_asid asid\<rbrace>
  load_hw_asid asid
  \<lbrace>\<lambda>rv s. \<exists>y. rv = Some y\<rbrace>" by (simp add: load_hw_asid_def, wp) (simp add: valid_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid asid\<rbrace> load_hw_asid asid \<lbrace>\<lambda>rv s. \<exists>y. rv = Some y\<rbrace>
theory ArchVSpace_AI

lemma invalidate_hw_asid_None [wp]:
  "\<lbrace>\<top>\<rbrace> invalidate_hw_asid_entry hw_asid \<lbrace>\<lambda>_ s. arm_hwasid_table (arch_state s) hw_asid = None\<rbrace>" apply (simp add: invalidate_hw_asid_entry_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> invalidate_hw_asid_entry hw_asid \<lbrace>\<lambda>_ s. arm_hwasid_table (arch_state s) hw_asid = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<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(hw_asid := None)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_ s. arm_hwasid_table (arch_state s) hw_asid = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> arm_hwasid_table (arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) s)(hw_asid := None)\<rparr>\<rparr>)) hw_asid = None proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma find_free_hw_asid_None_hw [wp]:
  "\<lbrace>\<top>\<rbrace> find_free_hw_asid \<lbrace>\<lambda>rv s. arm_hwasid_table (arch_state s) rv = None\<rbrace>" apply (simp add: find_free_hw_asid_def) apply (wp|wpc|simp)+ apply (clarsimp dest!: findSomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> find_free_hw_asid \<lbrace>\<lambda>rv s. arm_hwasid_table (arch_state s) rv = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do hw_asid_table <- gets (arm_hwasid_table \<circ> arch_state);
next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do invalidate_asid $ the $ hw_asid_table next_asid;
do_machine_op $ invalidateLocalTLB_ASID next_asid;
invalidate_hw_asid_entry next_asid;
new_next_asid <- return (next_asid + 1);
modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := new_next_asid\<rparr>\<rparr>);
return next_asid
od | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>rv s. arm_hwasid_table (arch_state s) rv = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x. find (\<lambda>a. arm_hwasid_table (arch_state s) a = None) (take (Suc (unat maxBound) - unat minBound) [arm_next_asid (arch_state s) .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat (arm_next_asid (arch_state s))))) [minBound .e. arm_next_asid (arch_state s)]) = Some x \<longrightarrow> arm_hwasid_table (arch_state s) x = None proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma find_free_hw_asid_None_asid_map [wp]:
  "\<lbrace>\<lambda>s. arm_asid_map (arch_state s) asid = None\<rbrace>
  find_free_hw_asid
  \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) asid = None\<rbrace>" apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def
              cong: option.case_cong) apply (wp|wpc|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. arm_asid_map (arch_state s) asid = None\<rbrace> find_free_hw_asid \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) asid = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. arm_asid_map (arch_state s) asid = None\<rbrace> do hw_asid_table <- gets (arm_hwasid_table \<circ> arch_state);
next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- do 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(the (hw_asid_table next_asid) := None)\<rparr>\<rparr>)
od;
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
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(next_asid := None)\<rparr>\<rparr>)
od;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2
od \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) asid = None\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma get_hw_asid_valid_arch:
  "\<lbrace>valid_arch_state\<rbrace> get_hw_asid asid \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" apply (simp add: get_hw_asid_def) apply (wp load_hw_asid_wp store_hw_asid_valid_arch|wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state\<rbrace> get_hw_asid 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;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- find_free_hw_asid;
store_hw_asid asid new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od \<lbrace>\<lambda>_. valid_arch_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_arch_state s \<Longrightarrow> (map_option fst (arm_asid_map (arch_state s) asid) = None \<longrightarrow> valid_arch_state s \<and> arm_asid_map (arch_state s) asid = None \<and> True) \<and> (\<forall>x. map_option fst (arm_asid_map (arch_state s) asid) = Some x \<longrightarrow> valid_arch_state s) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma svmrff_asid_mapped [wp]:
  "\<lbrace>valid_asid asid\<rbrace>
  set_vm_root_for_flush pd asid
  \<lbrace>\<lambda>rv. valid_asid asid\<rbrace>" apply (simp add: set_vm_root_for_flush_def arm_context_switch_def
                   get_hw_asid_def store_hw_asid_def find_free_hw_asid_def
                   load_hw_asid_def
              cong: if_cong option.case_cong) apply (wp|wpc|simp add: valid_asid_def|wp hoare_vcg_all_lift hoare_drop_imps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid asid\<rbrace> set_vm_root_for_flush pd asid \<lbrace>\<lambda>rv. valid_asid asid\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid asid\<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 y <- do hwasid <- do asid_map <- gets (arm_asid_map \<circ> arch_state);
case asid_map asid of None \<Rightarrow> do new_hw_asid <- do hw_asid_table <- gets (arm_hwasid_table \<circ> arch_state);
next_asid <- gets (arm_next_asid \<circ> arch_state);
case find (\<lambda>a. hw_asid_table a = None) (take (Suc (unat maxBound) - unat minBound) [next_asid .e. maxBound] @ take (Suc (unat maxBound) - (unat minBound + (Suc (unat maxBound) - unat next_asid))) [minBound .e. next_asid]) of None \<Rightarrow> do y <- invalidate_asid (the (hw_asid_table next_asid));
y <- do_machine_op (invalidateLocalTLB_ASID next_asid);
y <- invalidate_hw_asid_entry next_asid;
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_next_asid := next_asid + 1\<rparr>\<rparr>);
return next_asid
od | Some x2 \<Rightarrow> return x2
od;
y <- do pd <- find_pd_for_asid_assert asid;
asid_map <- gets (arm_asid_map \<circ> arch_state);
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(asid \<mapsto> (new_hw_asid, pd))\<rparr>\<rparr>);
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(new_hw_asid \<mapsto> asid)\<rparr>\<rparr>)
od;
return new_hw_asid
od | Some x2 \<Rightarrow> return (fst x2)
od;
do_machine_op (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)
od;
return True
od else return False
od \<lbrace>\<lambda>rv. valid_asid asid\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma store_hw_asid_asid_map [wp]:
  "\<lbrace>valid_asid_map and K (asid \<le> mask asid_bits)\<rbrace>
  store_hw_asid asid hw_asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: store_hw_asid_def) apply (wp find_pd_for_asid_assert_wp) apply (clarsimp simp: valid_asid_map_def fun_upd_def[symmetric]
                        pd_at_asid_arch_up) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and K (asid \<le> mask local.asid_bits)\<rbrace> store_hw_asid asid hw_asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits)\<rbrace> do pd <- find_pd_for_asid_assert asid;
asid_map <- gets (arm_asid_map \<circ> arch_state);
y <- modify (\<lambda>s. s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := asid_map(asid \<mapsto> (hw_asid, pd))\<rparr>\<rparr>);
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(hw_asid \<mapsto> asid)\<rparr>\<rparr>)
od \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits)) s \<Longrightarrow> \<forall>pd. vspace_at_asid asid pd s \<and> asid \<noteq> 0 \<longrightarrow> valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid \<mapsto> (hw_asid, pd))\<rparr>, arch_state := arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid \<mapsto> (hw_asid, pd))\<rparr>\<rparr>)\<lparr>arm_hwasid_table := ((arm_hwasid_table \<circ> arch_state) (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_map := ((arm_asid_map \<circ> arch_state) s)(asid \<mapsto> (hw_asid, pd))\<rparr>\<rparr>))(hw_asid \<mapsto> asid)\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma arm_context_switch_asid_map [wp]:
  "\<lbrace>valid_asid_map and K (asid \<le> mask asid_bits)\<rbrace>
  arm_context_switch pd asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" apply (simp add: arm_context_switch_def get_hw_asid_def) apply (wp load_hw_asid_wp|wpc|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and K (asid \<le> mask local.asid_bits)\<rbrace> arm_context_switch pd asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_asid_map and (\<lambda>y. asid \<le> mask local.asid_bits)\<rbrace> do hwasid <- do maybe_hw_asid <- load_hw_asid asid;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- find_free_hw_asid;
store_hw_asid asid new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od;
do_machine_op (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od)
od \<lbrace>\<lambda>_. valid_asid_map\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma valid_vs_lookup_arch_update:
  "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s)
     \<Longrightarrow> valid_vs_lookup (arch_state_update f s) = valid_vs_lookup s" by (simp add: valid_vs_lookup_def vs_lookup_pages_arch_update)

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

lemma find_pd_for_asid_page_directory [wp]:
  "\<lbrace>valid_vspace_objs\<rbrace>
  find_pd_for_asid asid
  \<lbrace>\<lambda>pd. page_directory_at pd\<rbrace>, -" apply (simp add: find_pd_for_asid_def assertE_def whenE_def split del: if_split) apply (wp|wpc|clarsimp|rule conjI)+ apply (drule vs_lookup_atI) apply (drule (2) valid_vspace_objsD) apply clarsimp apply (drule bspec, blast) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs\<rbrace> find_pd_for_asid asid \<lbrace>typ_at (AArch APageDirectory)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs\<rbrace> doE y <- if 0 < asid then returnOk () else fail;
asid_table <- liftE (gets (arm_asid_table \<circ> arch_state));
pool <- case asid_table (asid_high_bits_of asid) of None \<Rightarrow> throwError InvalidRoot | Some ptr \<Rightarrow> liftE $ get_asid_pool ptr;
case pool (UCAST(32 \<rightarrow> 10) asid) of None \<Rightarrow> throwError InvalidRoot | Some x \<Rightarrow> returnOk x
odE \<lbrace>typ_at (AArch APageDirectory)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>valid_vspace_objs s; 0 < asid; asid_table s (asid_high_bits_of asid) = Some x; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) xa s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>valid_vspace_objs s; 0 < asid; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; ([VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> x) s\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) xa s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>valid_vspace_objs s; 0 < asid; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; valid_vspace_obj (ASIDPool pool) s\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) xa s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>valid_vspace_objs s; 0 < asid; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; \<forall>x\<in>ran pool. typ_at (AArch APageDirectory) x s\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) xa s proof (prove)
goal (1 subgoal):
 1. \<And>s x pool xa. \<lbrakk>valid_vspace_objs s; 0 < asid; ako_at (ASIDPool pool) x s; pool (UCAST(32 \<rightarrow> 10) asid) = Some xa; typ_at (AArch APageDirectory) xa s\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) xa s proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma find_pd_for_asid_lookup[wp]:
  "\<lbrace>\<top>\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. \<exists>\<rhd> pd\<rbrace>,-" apply (rule hoare_post_imp_R, rule find_pd_for_asid_lookup_ref) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd s. \<exists>ref. (ref \<rhd> pd) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>rv s. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> rv) s \<Longrightarrow> \<exists>ref. (ref \<rhd> rv) s proof (prove)
goal:
No subgoals!