kings-crown/FVELER_Isabelle huggingface dataset:
theory VSpace_R

lemma storeHWASID_obj_at [wp]:
  "\<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> storeHWASID x y \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace>" apply (simp add: storeHWASID_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> storeHWASID x y \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> do pd <- findPDForASIDAssert x;
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
ya <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(x \<mapsto> (y, pd))) (ksArchState s)\<rparr>);
hwASIDMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. hwASIDMap(y \<mapsto> x)) (ksArchState s)\<rparr>)
od \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma findFreeHWASID_obj_at [wp]:
  "\<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace>" apply (simp add: findFreeHWASID_def invalidateASID_def
                   invalidateHWASIDEntry_def bind_assoc
              cong: option.case_cong) apply (wp doMachineOp_obj_at|wpc|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> do hwASIDTable <- gets (armKSHWASIDTable \<circ> ksArchState);
nextASID <- gets (armKSNextASID \<circ> ksArchState);
case find (\<lambda>a. hwASIDTable a = None) ([nextASID .e. maxBound] @ init [minBound .e. nextASID]) of None \<Rightarrow> do x <- findPDForASIDAssert (the (hwASIDTable nextASID));
x <- gets (armKSASIDMap \<circ> ksArchState);
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. x(the (hwASIDTable nextASID) := None)) (ksArchState s)\<rparr>);
y <- doMachineOp (invalidateLocalTLB_ASID nextASID);
x <- gets (armKSHWASIDTable \<circ> ksArchState);
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. x(nextASID := None)) (ksArchState s)\<rparr>);
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if nextASID = maxBound then minBound else nextASID + 1) (ksArchState s)\<rparr>);
return nextASID
od | Some x2 \<Rightarrow> return x2
od \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma findFreeHWASID_None_HWTable [wp]:
  "\<lbrace>\<top>\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. armKSHWASIDTable (ksArchState s) rv = None\<rbrace>" apply (simp add: findFreeHWASID_def invalidateHWASIDEntry_def invalidateASID_def
                   doMachineOp_def
              cong: option.case_cong) apply (wp|wpc|simp)+ apply (auto dest!: findSomeD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> findFreeHWASID \<lbrace>\<lambda>rv s. armKSHWASIDTable (ksArchState s) rv = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do hwASIDTable <- gets (armKSHWASIDTable \<circ> ksArchState);
nextASID <- gets (armKSNextASID \<circ> ksArchState);
case find (\<lambda>a. hwASIDTable a = None) ([nextASID .e. maxBound] @ init [minBound .e. nextASID]) of None \<Rightarrow> do y <- do y <- findPDForASIDAssert (the (hwASIDTable nextASID));
asidMap <- gets (armKSASIDMap \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSASIDMap_update (\<lambda>_. asidMap(the (hwASIDTable nextASID) := None)) (ksArchState s)\<rparr>)
od;
y <- do ms <- gets ksMachineState;
(r, ms') <- select_f (invalidateLocalTLB_ASID nextASID ms);
modify (ksMachineState_update (\<lambda>_. ms'))
od;
y <- do asidMap <- gets (armKSHWASIDTable \<circ> ksArchState);
modify (\<lambda>s. s\<lparr>ksArchState := armKSHWASIDTable_update (\<lambda>_. asidMap(nextASID := None)) (ksArchState s)\<rparr>)
od;
y <- modify (\<lambda>s. s\<lparr>ksArchState := armKSNextASID_update (\<lambda>_. if nextASID = maxBound then minBound else nextASID + 1) (ksArchState s)\<rparr>);
return nextASID
od | Some x2 \<Rightarrow> return x2
od \<lbrace>\<lambda>rv s. armKSHWASIDTable (ksArchState s) rv = None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x. find (\<lambda>a. armKSHWASIDTable (ksArchState s) a = None) ([armKSNextASID (ksArchState s) .e. maxBound] @ init [minBound .e. armKSNextASID (ksArchState s)]) = Some x \<longrightarrow> armKSHWASIDTable (ksArchState s) x = None proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma getHWASID_valid_arch':
  "\<lbrace>valid_arch_state'\<rbrace>
      getHWASID asid \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" apply (simp add: getHWASID_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> getHWASID asid \<lbrace>\<lambda>_. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> do maybe_hw_asid <- loadHWASID asid;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
y <- storeHWASID 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:
No subgoals!
theory VSpace_R

lemma store_pte_pd_at_asid[wp]:
  "\<lbrace>vspace_at_asid asid pd\<rbrace>
  store_pte p pte \<lbrace>\<lambda>_. vspace_at_asid asid pd\<rbrace>" apply (simp add: store_pte_def set_pd_def set_object_def vspace_at_asid_def) apply (wp get_object_wp) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid asid pd\<rbrace> store_pte p pte \<lbrace>\<lambda>_. vspace_at_asid asid pd\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>[VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd\<rbrace> do pt <- get_pt (p && ~~ mask pt_bits);
set_pt (p && ~~ mask pt_bits) (pt(UCAST(32 \<rightarrow> 8) (p && mask pt_bits >> 2) := pte))
od \<lbrace>\<lambda>_. [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s \<Longrightarrow> \<forall>pt. ako_at (PageTable pt) (p && ~~ mask pt_bits) s \<longrightarrow> ([VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd) s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma updateCap_vs_entry_align[wp]:
 "\<lbrace>ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p \<rbrace> updateCap ptr cap
  \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace>" apply (simp add:updateCap_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> updateCap ptr cap \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> do cte <- getCTE ptr;
setCTE ptr (cteCap_update (\<lambda>_. cap) cte)
od \<lbrace>\<lambda>rv. ko_wp_at' (\<lambda>ko. P (vs_entry_align ko)) p\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma updateCap_valid_slots'[wp]:
  "\<lbrace>valid_slots' x2\<rbrace> updateCap cte cte' \<lbrace>\<lambda>_ s. valid_slots' x2 s \<rbrace>" apply (case_tac x2) apply (clarsimp simp:valid_slots'_def) apply (wp hoare_vcg_ball_lift) apply (clarsimp simp:valid_slots'_def) apply (wp hoare_vcg_ball_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_slots' x2\<rbrace> updateCap cte cte' \<lbrace>\<lambda>_. valid_slots' x2\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a. x2 = Inl a \<Longrightarrow> \<lbrace>valid_slots' x2\<rbrace> updateCap cte cte' \<lbrace>\<lambda>_. valid_slots' x2\<rbrace>
 2. \<And>b. x2 = Inr b \<Longrightarrow> \<lbrace>valid_slots' x2\<rbrace> updateCap cte cte' \<lbrace>\<lambda>_. valid_slots' x2\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b. x2 = Inl (a, b) \<Longrightarrow> \<lbrace>valid_pte' a\<rbrace> updateCap cte cte' \<lbrace>\<lambda>_. valid_pte' a\<rbrace>
 2. \<And>b. x2 = Inr b \<Longrightarrow> \<lbrace>valid_slots' x2\<rbrace> updateCap cte cte' \<lbrace>\<lambda>_. valid_slots' x2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>b. x2 = Inr b \<Longrightarrow> \<lbrace>valid_slots' x2\<rbrace> updateCap cte cte' \<lbrace>\<lambda>_. valid_slots' x2\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a b. x2 = Inr (a, b) \<Longrightarrow> \<lbrace>valid_pde' a\<rbrace> updateCap cte cte' \<lbrace>\<lambda>_. valid_pde' a\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma set_cap_pd_at_asid [wp]:
  "\<lbrace>vspace_at_asid asid pd\<rbrace> set_cap t st \<lbrace>\<lambda>rv. vspace_at_asid asid pd\<rbrace>" apply (simp add: vspace_at_asid_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>vspace_at_asid asid pd\<rbrace> set_cap t st \<lbrace>\<lambda>rv. vspace_at_asid asid pd\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>[VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd\<rbrace> set_cap t st \<lbrace>\<lambda>rv. [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] \<rhd> pd\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma set_cap_valid_slots_inv[wp]:
  "\<lbrace>valid_slots m\<rbrace> set_cap t st \<lbrace>\<lambda>rv. valid_slots m\<rbrace>" by (cases m, (clarsimp simp: valid_slots_def, wp hoare_vcg_ball_lift set_cap.vs_lookup set_cap_typ_ats)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_slots m\<rbrace> set_cap t st \<lbrace>\<lambda>rv. valid_slots m\<rbrace>
theory VSpace_R

lemma set_cap_same_refs_inv[wp]:
  "\<lbrace>\<lambda>s. same_refs m cap s\<rbrace> set_cap t st \<lbrace>\<lambda>rv s. same_refs m cap s\<rbrace>" by (cases m, (clarsimp simp: same_refs_def, wp)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>same_refs m cap\<rbrace> set_cap t st \<lbrace>\<lambda>rv. same_refs m cap\<rbrace>
theory VSpace_R

lemma duplicate_address_set_simp:
  "\<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET \<rbrakk>
  \<Longrightarrow> p && ~~ mask (vs_ptr_align m) = p" by (auto simp:vs_ptr_align_def koTypeOf_def
    split:kernel_object.splits arch_kernel_object.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>koTypeOf m \<noteq> ArchT PDET; koTypeOf m \<noteq> ArchT PTET\<rbrakk> \<Longrightarrow> p && ~~ mask (vs_ptr_align m) = p
theory VSpace_R

lemma message_info_to_data_eqv:
  "wordFromMessageInfo (message_info_map mi) = message_info_to_data mi" apply (cases mi) apply (simp add: wordFromMessageInfo_def
    msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def
    shiftL_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wordFromMessageInfo (message_info_map mi) = message_info_to_data mi proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2 x3 x4. mi = Structures_A.message_info.MI x1 x2 x3 x4 \<Longrightarrow> wordFromMessageInfo (message_info_map mi) = message_info_to_data mi proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma message_info_from_data_eqv:
  "message_info_map (data_to_message_info rv) = messageInfoFromWord rv" by (auto simp: data_to_message_info_def messageInfoFromWord_def Let_def not_less
                 msgLengthBits_def msgExtraCapBits_def msgMaxExtraCaps_def mask_def
                 shiftL_nat msgMaxLength_def msgLabelBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. message_info_map (data_to_message_info rv) = messageInfoFromWord rv
theory VSpace_R

lemma setMessageInfo_corres:
 "mi' = message_info_map mi \<Longrightarrow>
  corres dc (tcb_at t) (tcb_at' t)
         (set_message_info t mi) (setMessageInfo t mi')" apply (simp add: setMessageInfo_def set_message_info_def) apply (subgoal_tac "wordFromMessageInfo (message_info_map mi) =
                      message_info_to_data mi") apply (simp add: asUser_setRegister_corres msg_info_register_def
                    msgInfoRegister_def) apply (simp add: message_info_to_data_eqv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mi' = message_info_map mi \<Longrightarrow> corres dc (tcb_at t) (tcb_at' t) (set_message_info t mi) (setMessageInfo t mi') proof (prove)
goal (1 subgoal):
 1. mi' = message_info_map mi \<Longrightarrow> corres dc (tcb_at t) (tcb_at' t) (as_user t (setRegister msg_info_register (message_info_to_data mi))) (asUser t (setRegister TCB_H.msgInfoRegister (wordFromMessageInfo (message_info_map mi)))) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>mi' = message_info_map mi; wordFromMessageInfo (message_info_map mi) = message_info_to_data mi\<rbrakk> \<Longrightarrow> corres dc (tcb_at t) (tcb_at' t) (as_user t (setRegister msg_info_register (message_info_to_data mi))) (asUser t (setRegister TCB_H.msgInfoRegister (wordFromMessageInfo (message_info_map mi))))
 2. mi' = message_info_map mi \<Longrightarrow> wordFromMessageInfo (message_info_map mi) = message_info_to_data mi proof (prove)
goal (1 subgoal):
 1. mi' = message_info_map mi \<Longrightarrow> wordFromMessageInfo (message_info_map mi) = message_info_to_data mi proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma set_mi_invs'[wp]: "\<lbrace>invs' and tcb_at' t\<rbrace> setMessageInfo t a \<lbrace>\<lambda>x. invs'\<rbrace>" by (simp add: setMessageInfo_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t\<rbrace> setMessageInfo t a \<lbrace>\<lambda>x. invs'\<rbrace>
theory VSpace_R

lemma set_mi_tcb' [wp]:
  "\<lbrace> tcb_at' t \<rbrace> setMessageInfo receiver msg \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>" by (simp add: setMessageInfo_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t\<rbrace> setMessageInfo receiver msg \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
theory VSpace_R

lemma set_mrs_invs'[wp]:
  "\<lbrace> invs' and tcb_at' receiver \<rbrace> setMRs receiver recv_buf mrs \<lbrace>\<lambda>rv. invs' \<rbrace>" apply (simp add: setMRs_def) apply (wp dmo_invs' no_irq_mapM no_irq_storeWord crunch_wps|
         simp add: zipWithM_x_mapM split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' receiver\<rbrace> setMRs receiver recv_buf mrs \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' receiver\<rbrace> do y <- asUser receiver (zipWithM_x setRegister TCB_H.msgRegisters (take (min (length mrs) (length TCB_H.msgRegisters + length (case recv_buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
y <- zipWithM_x storeWordUser (case recv_buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]) (drop (length TCB_H.msgRegisters) (take (min (length mrs) (length TCB_H.msgRegisters + length (case recv_buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))) mrs));
return (word_of_nat (min (length mrs) (length TCB_H.msgRegisters + length (case recv_buf of None \<Rightarrow> [] | Some bufferPtr \<Rightarrow> map (\<lambda>x. bufferPtr + x * word_of_nat wordSize) [1 + word_of_nat (length TCB_H.msgRegisters) .e. msgMaxLength]))))
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma same_refs_vs_cap_ref_eq:
  assumes "valid_slots entries s"
  assumes "same_refs entries cap s"
  assumes "same_refs entries cap' s"
  shows "vs_cap_ref cap = vs_cap_ref cap'" using assms apply (cases entries; clarsimp simp: same_refs_def valid_slots_def) apply (all \<open>rename_tac pte slots p; case_tac slots; clarsimp\<close>) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_cap_ref cap = vs_cap_ref cap' proof (prove)
using this:
valid_slots entries s
same_refs entries cap s
same_refs entries cap' s

goal (1 subgoal):
 1. vs_cap_ref cap = vs_cap_ref cap' proof (prove)
goal (2 subgoals):
 1. \<And>a b p. \<lbrakk>entries = Inl (a, b); b \<noteq> []; case b of [] \<Rightarrow> True | x # xs \<Rightarrow> \<forall>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s \<longrightarrow> vs_cap_ref cap = Some (VSRef (x && mask pt_bits >> 2) (Some APageTable) # ref); case b of [] \<Rightarrow> True | x # xs \<Rightarrow> \<forall>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s \<longrightarrow> vs_cap_ref cap' = Some (VSRef (x && mask pt_bits >> 2) (Some APageTable) # ref); \<forall>p\<in>set b. (\<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) \<and> pte_at p s; p \<in> obj_refs cap; pte_ref_pages a = Some p; p \<in> obj_refs cap'; wellformed_pte a; valid_pte a s\<rbrakk> \<Longrightarrow> vs_cap_ref cap = vs_cap_ref cap'
 2. \<And>a b p. \<lbrakk>entries = Inr (a, b); b \<noteq> []; case b of [] \<Rightarrow> True | x # xs \<Rightarrow> \<forall>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s \<longrightarrow> vs_cap_ref cap = Some (VSRef (x && mask pd_bits >> 2) (Some APageDirectory) # ref); case b of [] \<Rightarrow> True | x # xs \<Rightarrow> \<forall>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s \<longrightarrow> vs_cap_ref cap' = Some (VSRef (x && mask pd_bits >> 2) (Some APageDirectory) # ref); \<forall>p\<in>set b. (\<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) \<and> pde_at p s \<and> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots; p \<in> obj_refs cap; pde_ref_pages a = Some p; p \<in> obj_refs cap'; wellformed_pde a; valid_pde a s\<rbrakk> \<Longrightarrow> vs_cap_ref cap = vs_cap_ref cap' proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma armv_contextSwitch_obj_at [wp]:
  "\<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> armv_contextSwitch pd a \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace>" apply (simp add: armv_contextSwitch_def armv_contextSwitch_HWASID_def getHWASID_def) apply (wp doMachineOp_obj_at|wpc|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> armv_contextSwitch pd a \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' P' t s)\<rbrace> do hwasid <- do maybe_hw_asid <- loadHWASID a;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
y <- storeHWASID a new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od;
doMachineOp (do y <- setCurrentPD (addrFromPPtr pd);
setHardwareASID hwasid
od)
od \<lbrace>\<lambda>rv s. P (obj_at' P' t s)\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma getHWASID_invs [wp]:
  "\<lbrace>invs'\<rbrace> getHWASID asid \<lbrace>\<lambda>hw_asid. invs'\<rbrace>" apply (simp add: getHWASID_def) apply (wp storeHWASID_invs findFreeHWASID_invs|wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> getHWASID asid \<lbrace>\<lambda>hw_asid. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do maybe_hw_asid <- loadHWASID asid;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
y <- storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od \<lbrace>\<lambda>hw_asid. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<Longrightarrow> (map_option fst (armKSASIDMap (ksArchState s) asid) = None \<longrightarrow> invs' s \<and> armKSASIDMap (ksArchState s) asid = None \<and> True) \<and> (\<forall>x. map_option fst (armKSASIDMap (ksArchState s) asid) = Some x \<longrightarrow> invs' s) proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma getHWASID_invs_no_cicd':
  "\<lbrace>invs_no_cicd'\<rbrace> getHWASID asid \<lbrace>\<lambda>hw_asid. invs_no_cicd'\<rbrace>" apply (simp add: getHWASID_def) apply (wp storeHWASID_invs_no_cicd' findFreeHWASID_invs_no_cicd'|wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> getHWASID asid \<lbrace>\<lambda>hw_asid. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> do maybe_hw_asid <- loadHWASID asid;
case maybe_hw_asid of None \<Rightarrow> do new_hw_asid <- findFreeHWASID;
y <- storeHWASID asid new_hw_asid;
return new_hw_asid
od | Some hw_asid \<Rightarrow> return hw_asid
od \<lbrace>\<lambda>hw_asid. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> (map_option fst (armKSASIDMap (ksArchState s) asid) = None \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s \<and> armKSASIDMap (ksArchState s) asid = None \<and> True) \<and> (\<forall>x. map_option fst (armKSASIDMap (ksArchState s) asid) = Some x \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma no_irq_armv_contextSwitch_HWASID:
  "no_irq (armv_contextSwitch_HWASID pd hwasid)" apply (simp add: armv_contextSwitch_HWASID_def setCurrentPD_to_abs) apply (wp no_irq_set_current_pd no_irq_setHardwareASID) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_irq (armv_contextSwitch_HWASID pd hwasid) proof (prove)
goal (1 subgoal):
 1. no_irq (do y <- set_current_pd (addrFromPPtr pd);
setHardwareASID hwasid
od) proof (prove)
goal:
No subgoals!