kings-crown/FVELER_Isabelle huggingface dataset:
theory VSpace_R

lemma armv_contextSwitch_invs [wp]:
  "\<lbrace>invs'\<rbrace> armv_contextSwitch pd asid \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: armv_contextSwitch_def) apply (wp dmo_invs' no_irq_armv_contextSwitch_HWASID no_irq
      hoare_vcg_all_lift) apply (rule hoare_post_imp[rotated], rule hoare_vcg_prop[where P=True]) apply clarsimp apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
         in use_valid) apply (simp add: machine_op_lift_def machine_rest_lift_def split_def armv_ctxt_sw_defs
                     writeTTBR0Ptr_def
              | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> armv_contextSwitch pd asid \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do hwasid <- getHWASID asid;
doMachineOp (armv_contextSwitch_HWASID pd hwasid)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>m. \<lbrace>?P9 m\<rbrace> getHWASID asid \<lbrace>\<lambda>rv s. \<forall>(r, m')\<in>fst (armv_contextSwitch_HWASID pd rv m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<lbrace>?P'8\<rbrace> getHWASID asid \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>s. invs' s \<Longrightarrow> (\<forall>x. ?P9 x s) \<and> ?P'8 s proof (prove)
goal (3 subgoals):
 1. \<And>m rv s. True \<Longrightarrow> \<forall>(r, m')\<in>fst (armv_contextSwitch_HWASID pd rv m). \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory m' p = underlying_memory m p
 2. \<lbrace>?P'8\<rbrace> getHWASID asid \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>s. invs' s \<Longrightarrow> (\<forall>x. True) \<and> ?P'8 s proof (prove)
goal (3 subgoals):
 1. \<And>m rv s b p. \<lbrakk>((), b) \<in> fst (armv_contextSwitch_HWASID pd rv m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s
 2. \<lbrace>?P'8\<rbrace> getHWASID asid \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>s. invs' s \<Longrightarrow> (\<forall>x. True) \<and> ?P'8 s proof (prove)
goal (5 subgoals):
 1. \<And>m rv s b p. \<lbrakk>\<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P21 m rv s b p\<rbrace> armv_contextSwitch_HWASID pd rv \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>m rv s b p. \<lbrakk>\<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P21 m rv s b p m
 3. \<And>m rv s b p. \<lbrakk>\<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s
 4. \<lbrace>?P'8\<rbrace> getHWASID asid \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>s. invs' s \<Longrightarrow> (\<forall>x. True) \<and> ?P'8 s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma dmo_setCurrentPD_invs'[wp]:
  "\<lbrace>invs'\<rbrace> doMachineOp (setCurrentPD addr) \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (wpsimp wp: dmo_invs' no_irq_set_current_pd no_irq simp: setCurrentPD_to_abs) apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
         in use_valid) apply (clarsimp simp: set_current_pd_def machine_op_lift_def writeTTBR0_def dsb_def isb_def
                          machine_rest_lift_def split_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp (setCurrentPD addr) \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s m b p. \<lbrakk>invs' s; ((), b) \<in> fst (set_current_pd addr m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P18 s m b p\<rbrace> set_current_pd addr \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P18 s m b p m
 3. \<And>s m b p. \<lbrakk>invs' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma dmo_setCurrentPD_invs_no_cicd':
  "\<lbrace>invs_no_cicd'\<rbrace> doMachineOp (setCurrentPD addr) \<lbrace>\<lambda>rv. invs_no_cicd'\<rbrace>" apply (wpsimp wp: dmo_invs_no_cicd' no_irq_set_current_pd no_irq  simp: setCurrentPD_to_abs) apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
         in use_valid) apply (clarsimp simp: set_current_pd_def machine_op_lift_def writeTTBR0_def dsb_def isb_def
                        machine_rest_lift_def split_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> doMachineOp (setCurrentPD addr) \<lbrace>\<lambda>rv. all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s m b p. \<lbrakk>all_invs_but_ct_idle_or_in_cur_domain' s; ((), b) \<in> fst (set_current_pd addr m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s m b p. \<lbrakk>all_invs_but_ct_idle_or_in_cur_domain' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P18 s m b p\<rbrace> set_current_pd addr \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>s m b p. \<lbrakk>all_invs_but_ct_idle_or_in_cur_domain' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P18 s m b p m
 3. \<And>s m b p. \<lbrakk>all_invs_but_ct_idle_or_in_cur_domain' s; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma valid_slots_lift':
  assumes t: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>"
  shows "\<lbrace>valid_slots' x\<rbrace> f \<lbrace>\<lambda>rv. valid_slots' x\<rbrace>" apply (clarsimp simp: valid_slots'_def split: sum.splits prod.splits) apply safe apply (rule hoare_pre, wp hoare_vcg_const_Ball_lift t valid_pde_lift' valid_pte_lift', simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_slots' x\<rbrace> f \<lbrace>\<lambda>rv. valid_slots' x\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<forall>a. (\<exists>b. x = Inl (a, b)) \<longrightarrow> \<lbrace>valid_pte' a\<rbrace> f \<lbrace>\<lambda>rv. valid_pte' a\<rbrace>) \<and> (\<forall>a. (\<exists>b. x = Inr (a, b)) \<longrightarrow> \<lbrace>valid_pde' a\<rbrace> f \<lbrace>\<lambda>rv. valid_pde' a\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>a b. x = Inl (a, b) \<Longrightarrow> \<lbrace>valid_pte' a\<rbrace> f \<lbrace>\<lambda>rv. valid_pte' a\<rbrace>
 2. \<And>a b. x = Inr (a, b) \<Longrightarrow> \<lbrace>valid_pde' a\<rbrace> f \<lbrace>\<lambda>rv. valid_pde' a\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePDE_pred_tcb_at' [wp]:
  "\<lbrace>pred_tcb_at' proj P t\<rbrace> storePDE p pde \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace>" apply (simp add: storePDE_def pred_tcb_at'_def) apply (rule obj_at_setObject2) apply (clarsimp simp add: updateObject_default_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t\<rbrace> storePDE p pde \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> setObject p pde \<lbrace>\<lambda>_. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb) proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePTE_pred_tcb_at' [wp]:
  "\<lbrace>pred_tcb_at' proj P t\<rbrace> storePTE p pte \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace>" apply (simp add: storePTE_def pred_tcb_at'_def) apply (rule obj_at_setObject2) apply (clarsimp simp add: updateObject_default_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t\<rbrace> storePTE p pte \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> setObject p pte \<lbrace>\<lambda>_. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb) proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setASID_pred_tcb_at' [wp]:
  "\<lbrace>pred_tcb_at' proj P t\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace>" apply (simp add: pred_tcb_at'_def) apply (rule obj_at_setObject2) apply (clarsimp simp add: updateObject_default_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t\<rbrace> setObject p ap \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> setObject p ap \<lbrace>\<lambda>_. obj_at' (\<lambda>ko. P (proj (tcb_to_itcb' ko))) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb) proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma dmo_ct[wp]:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> doMachineOp m \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>" apply (simp add: doMachineOp_def split_def) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> doMachineOp m \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do ms <- gets ksMachineState;
p <- select_f (m ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ksCurThread s) \<Longrightarrow> \<forall>x\<in>fst (m (ksMachineState s)). P (ksCurThread (s\<lparr>ksMachineState := snd x\<rparr>)) proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePDE_valid_mdb [wp]:
  "\<lbrace>valid_mdb'\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>" by (simp add: valid_mdb'_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb'\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
theory VSpace_R

lemma storePDE_inQ[wp]:
  "\<lbrace>\<lambda>s. P (obj_at' (inQ d p) t s)\<rbrace> storePDE ptr pde \<lbrace>\<lambda>rv s. P (obj_at' (inQ d p) t s)\<rbrace>" apply (simp add: obj_at'_real_def storePDE_def) apply (wp setObject_ko_wp_at | simp add: objBits_simps archObjSize_def pdeBits_def)+ apply (clarsimp simp: projectKOs obj_at'_def ko_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' (inQ d p) t s)\<rbrace> storePDE ptr pde \<lbrace>\<lambda>rv s. P (obj_at' (inQ d p) t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s)\<rbrace> setObject ptr pde \<lbrace>\<lambda>rv s. P (ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s) \<Longrightarrow> ptr = t \<longrightarrow> obj_at' (\<lambda>x. True) t s \<longrightarrow> P (ko_wp_at' (\<lambda>y. \<exists>obj. projectKO_opt (KOArch (KOPDE pde)) = Some obj \<and> inQ d p obj) t s) proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePDE_valid_queues [wp]:
  "\<lbrace>Invariants_H.valid_queues\<rbrace> storePDE p pde \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" by (wp valid_queues_lift | simp add: pred_tcb_at'_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues\<rbrace> storePDE p pde \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>
theory VSpace_R

lemma storePDE_valid_queues' [wp]:
  "\<lbrace>valid_queues'\<rbrace> storePDE p pde \<lbrace>\<lambda>_. valid_queues'\<rbrace>" by (wp valid_queues_lift')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> storePDE p pde \<lbrace>\<lambda>_. valid_queues'\<rbrace>
theory VSpace_R

lemma storePDE_state_refs' [wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> storePDE p pde \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" apply (clarsimp simp: storePDE_def) apply (clarsimp simp: setObject_def valid_def in_monad split_def
                        updateObject_default_def projectKOs objBits_simps
                        in_magnitude_check state_refs_of'_def ps_clear_upd
                 elim!: rsubst[where P=P] intro!: ext
             split del: if_split cong: option.case_cong if_cong) apply (simp split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> storePDE p pde \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> setObject p pde \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x uu_ s''. \<lbrakk>ksPSpace s p = Some (KOArch (KOPDE uu_)); is_aligned p (archObjSize (KOPDE pde)); ((), s'') \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPDE pde)) s)\<rbrakk> \<Longrightarrow> (case ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> ps_clear x (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s then refs_of' ko else {}) = (case if x = p then Some (KOArch (KOPDE pde)) else ksPSpace s x of None \<Rightarrow> {} | Some ko \<Rightarrow> if is_aligned x (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> ps_clear x (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s then refs_of' ko else {}) proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setObject_pde_ksInt [wp]:
  "\<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> setObject p (pde::pde) \<lbrace>\<lambda>_. \<lambda>s. P (ksInterruptState s)\<rbrace>" by (wp setObject_ksInterrupt updateObject_default_inv|simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> setObject p pde \<lbrace>\<lambda>_ s. P (ksInterruptState s)\<rbrace>
theory VSpace_R

lemma storePDE_ifunsafe [wp]:
  "\<lbrace>if_unsafe_then_cap'\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" apply (simp add: storePDE_def) apply (rule hoare_pre) apply (rule setObject_ifunsafe' [where P=\<top>], simp) apply (auto simp: updateObject_default_def in_monad projectKOs)[2] apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap'\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap'\<rbrace> setObject p pde \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject p pde \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>
 2. \<And>s. if_unsafe_then_cap' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject_default pde (KOTCB tcb) p x n s); lookupAround2 p (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF tcb' = getF tcb)
 2. \<And>x n cte s. fst (updateObject pde (KOCTE cte) p x n s) = {}
 3. \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setObject p pde \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>
 4. \<And>s. if_unsafe_then_cap' s \<Longrightarrow> if_unsafe_then_cap' s \<and> True proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setObject p pde \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace>
 2. \<And>s. if_unsafe_then_cap' s \<Longrightarrow> if_unsafe_then_cap' s \<and> True proof (prove)
goal (1 subgoal):
 1. \<And>s. if_unsafe_then_cap' s \<Longrightarrow> if_unsafe_then_cap' s \<and> True proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePDE_idle [wp]:
  "\<lbrace>valid_idle'\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" by (valid_idle'_setObject simp: storePDE_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> storePDE p pde \<lbrace>\<lambda>rv. valid_idle'\<rbrace>
theory VSpace_R

lemma storePDE_irq_states' [wp]:
  "\<lbrace>valid_irq_states'\<rbrace> storePDE pde p \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>" apply (simp add: storePDE_def) apply (wpsimp wp: valid_irq_states_lift' dmo_lift' no_irq_storeWord setObject_ksMachine
                    updateObject_default_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> storePDE pde p \<lbrace>\<lambda>_. valid_irq_states'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> setObject pde p \<lbrace>\<lambda>_. valid_irq_states'\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePDE_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> storePDE p pde \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" apply (simp add: storePDE_def valid_machine_state'_def pointerInUserData_def
                   pointerInDeviceData_def) apply (wp setObject_typ_at_inv setObject_ksMachine updateObject_default_inv
            hoare_vcg_all_lift hoare_vcg_disj_lift | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state'\<rbrace> storePDE p pde \<lbrace>\<lambda>_. valid_machine_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> setObject p pde \<lbrace>\<lambda>_ s. \<forall>p. typ_at' UserDataT (p && ~~ mask pageBits) s \<or> typ_at' UserDataDeviceT (p && ~~ mask pageBits) s \<or> underlying_memory (ksMachineState s) p = 0\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePDE_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> storePDE p pde \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (rule ct_not_inQ_lift [OF storePDE_nosch]) apply (simp add: storePDE_def) apply (rule hoare_weaken_pre) apply (wps setObject_PDE_ct) apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_default_def in_monad)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_inQ\<rbrace> storePDE p pde \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> storePDE p pde \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> setObject p pde \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q10\<rbrace> setObject p pde \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q10 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P13 prev_s\<rbrace> setObject p pde \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?P13 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s ko s' v oko x y n s. (ko, s') \<in> fst (updateObject v oko x y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(Structures_H.tcb)
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setObject_pde_ksDomSchedule[wp]:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setObject t (v::pde) \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t ps));
obj' <- updateObject_default v (snd p) t (fst p) (snd (lookupAround2 t ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePDE_cur_domain[wp]:
  "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> storePDE p pde \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace>" by (simp add: storePDE_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> storePDE p pde \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace>
theory VSpace_R

lemma storePDE_ksDomSchedule[wp]:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> storePDE p pde \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>" by (simp add: storePDE_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> storePDE p pde \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>