kings-crown/FVELER_Isabelle huggingface dataset:
theory VSpace_R

lemma storePDE_tcb_obj_at'[wp]:
  "\<lbrace>obj_at' (P::tcb \<Rightarrow> bool) t\<rbrace> storePDE p pde \<lbrace>\<lambda>_. obj_at' P t\<rbrace>" apply (simp add: storePDE_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>obj_at' P t\<rbrace> storePDE p pde \<lbrace>\<lambda>_. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setObject p pde \<lbrace>\<lambda>_. obj_at' P 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 storePDE_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t\<rbrace> storePDE p pde \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>" by (wp tcb_in_cur_domain'_lift)

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

lemma storePDE_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace>ct_idle_or_in_cur_domain'\<rbrace> storePDE p pde \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" by (wp ct_idle_or_in_cur_domain'_lift hoare_vcg_disj_lift)

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

lemma setObject_pte_ksDomScheduleIdx [wp]:
  "\<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setObject p (pte::pte) \<lbrace>\<lambda>_. \<lambda>s. P (ksDomScheduleIdx s)\<rbrace>" by (wp updateObject_default_inv|simp add:setObject_def | wpc)+

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

lemma storePTE_valid_mdb [wp]:
  "\<lbrace>valid_mdb'\<rbrace> storePTE p pte \<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> storePTE p pte \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
theory VSpace_R

lemma storePTE_inQ[wp]:
  "\<lbrace>\<lambda>s. P (obj_at' (inQ d p) t s)\<rbrace> storePTE ptr pde \<lbrace>\<lambda>rv s. P (obj_at' (inQ d p) t s)\<rbrace>" apply (simp add: obj_at'_real_def storePTE_def) apply (wp setObject_ko_wp_at | simp add: objBits_simps archObjSize_def pteBits_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> storePTE 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 (KOPTE pde)) = Some obj \<and> inQ d p obj) t s) proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePTE_valid_queues [wp]:
  "\<lbrace>Invariants_H.valid_queues\<rbrace> storePTE 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> storePTE p pde \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>
theory VSpace_R

lemma storePTE_valid_queues' [wp]:
  "\<lbrace>valid_queues'\<rbrace> storePTE 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> storePTE p pde \<lbrace>\<lambda>_. valid_queues'\<rbrace>
theory VSpace_R

lemma storePTE_state_refs' [wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> storePTE p pte \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" apply (clarsimp simp: storePTE_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> storePTE p pte \<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 pte \<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 (KOPTE uu_)); is_aligned p (archObjSize (KOPTE pte)); ((), s'') \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOPTE pte)) 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 (KOPTE pte)) 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 storePTE_iflive [wp]:
  "\<lbrace>if_live_then_nonz_cap'\<rbrace> storePTE p pte \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" apply (simp add: storePTE_def) apply (rule hoare_pre) apply (rule setObject_iflive' [where P=\<top>], simp) apply (simp add: objBits_simps archObjSize_def) apply (auto simp: updateObject_default_def in_monad projectKOs pteBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> storePTE p pte \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> setObject p pte \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject p pte \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>
 2. \<And>s. if_live_then_nonz_cap' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x. objBits x = ?n3
 2. 1 < 2 ^ ?n3
 3. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject pte (KOTCB tcb) p x n s); True; lookupAround2 p (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 4. \<And>x n cte s. fst (updateObject pte (KOCTE cte) p x n s) = {}
 5. \<And>s. if_live_then_nonz_cap' s \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO pte) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (4 subgoals):
 1. 1 < 2 ^ pteBits
 2. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject pte (KOTCB tcb) p x n s); True; lookupAround2 p (ksPSpace s) = (Some (x, KOTCB tcb), n)\<rbrakk> \<Longrightarrow> \<exists>tcb'. t = (KOTCB tcb', s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. getF tcb' = getF tcb)
 3. \<And>x n cte s. fst (updateObject pte (KOCTE cte) p x n s) = {}
 4. \<And>s. if_live_then_nonz_cap' s \<Longrightarrow> if_live_then_nonz_cap' s \<and> (live' (injectKO pte) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setObject_pte_ksInt [wp]:
  "\<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> setObject p (pte::pte) \<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 pte \<lbrace>\<lambda>_ s. P (ksInterruptState s)\<rbrace>
theory VSpace_R

lemma storePTE_idle [wp]:
  "\<lbrace>valid_idle'\<rbrace> storePTE p pte \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" by (valid_idle'_setObject simp: storePTE_def)

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

lemma storePTE_irq_states' [wp]:
  "\<lbrace>valid_irq_states'\<rbrace> storePTE pte p \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>" apply (simp add: storePTE_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> storePTE pte p \<lbrace>\<lambda>_. valid_irq_states'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> setObject pte p \<lbrace>\<lambda>_. valid_irq_states'\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePTE_valid_objs [wp]:
  "\<lbrace>valid_objs' and valid_pte' pte\<rbrace> storePTE p pte \<lbrace>\<lambda>_. valid_objs'\<rbrace>" apply (simp add: storePTE_def doMachineOp_def split_def) apply (rule hoare_pre) apply (wp hoare_drop_imps|wpc|simp)+ apply (rule setObject_valid_objs') prefer 2 apply assumption apply (clarsimp simp: updateObject_default_def in_monad) apply (clarsimp simp: valid_obj'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_pte' pte\<rbrace> storePTE p pte \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_pte' pte\<rbrace> do y <- setObject p pte;
ms <- gets ksMachineState;
p <- select_f (storeWordVM p (wordFromPTE pte) ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- setObject p pte;
ms <- gets ksMachineState;
p <- select_f (storeWordVM p (wordFromPTE pte) ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od \<lbrace>\<lambda>_. valid_objs'\<rbrace>
 2. \<And>s. (valid_objs' and valid_pte' pte) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject p pte \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<And>s. (valid_objs' and valid_pte' pte) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>x n ko s ko' s'. \<lbrakk>(ko', s') \<in> fst (updateObject pte ko p x n s); ?P14 s; valid_obj' ko s; lookupAround2 p (ksPSpace s) = (Some (x, ko), n)\<rbrakk> \<Longrightarrow> valid_obj' ko' s
 2. \<And>s. (valid_objs' and valid_pte' pte) s \<Longrightarrow> (valid_objs' and ?P14) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_objs' and valid_pte' pte) s \<Longrightarrow> (valid_objs' and ?P14) s
 2. \<And>x n ko s ko' s'. \<lbrakk>(ko', s') \<in> fst (updateObject pte ko p x n s); ?P14 s; valid_obj' ko s; lookupAround2 p (ksPSpace s) = (Some (x, ko), n)\<rbrakk> \<Longrightarrow> valid_obj' ko' s proof (prove)
goal (1 subgoal):
 1. \<And>x n ko s ko' s'. \<lbrakk>(ko', s') \<in> fst (updateObject pte ko p x n s); valid_pte' pte s; valid_obj' ko s; lookupAround2 p (ksPSpace s) = (Some (x, ko), n)\<rbrakk> \<Longrightarrow> valid_obj' ko' s proof (prove)
goal (1 subgoal):
 1. \<And>n ko s s' s'' uu_. \<lbrakk>valid_pte' pte s; valid_obj' ko s; lookupAround2 p (ksPSpace s) = (Some (p, ko), n); (uu_, s'') \<in> fst (projectKO ko s); is_aligned p (objBits pte); ((), s') \<in> fst (magnitudeCheck p n (objBits pte) s'')\<rbrakk> \<Longrightarrow> valid_obj' (KOArch (KOPTE pte)) s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePTE_pde_mappings'[wp]:
  "\<lbrace>valid_pde_mappings'\<rbrace> storePTE p pte \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (wp valid_pde_mappings_lift') apply (simp add: storePTE_def) apply (rule obj_at_setObject2) apply (clarsimp dest!: updateObject_default_result) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings'\<rbrace> storePTE p pte \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> storePTE p pte \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace>
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> setObject p pte \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace>
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>x ko s' v oko xa y n s. (ko, s') \<in> fst (updateObject v oko xa y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(ARM_H.pde)
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma storePTE_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> storePTE p pde \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" apply (simp add: storePTE_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> storePTE 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 storePTE_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> storePTE p pte \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (rule ct_not_inQ_lift [OF storePTE_nosch]) apply (simp add: storePTE_def) apply (rule hoare_weaken_pre) apply (wps setObject_pte_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> storePTE p pte \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> storePTE p pte \<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 pte \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q10\<rbrace> setObject p pte \<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 pte \<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_pte_cur_domain[wp]:
  "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject t (v::pte) \<lbrace>\<lambda>rv s. P (ksCurDomain 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 (ksCurDomain s)\<rbrace> setObject t v \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain 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 (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setObject_pte_ksDomSchedule[wp]:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setObject t (v::pte) \<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 storePTE_cur_domain[wp]:
  "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> storePTE p pde \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace>" by (simp add: storePTE_def) wp

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

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

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

lemma storePTE_tcb_obj_at'[wp]:
  "\<lbrace>obj_at' (P::tcb \<Rightarrow> bool) t\<rbrace> storePTE p pte \<lbrace>\<lambda>_. obj_at' P t\<rbrace>" apply (simp add: storePTE_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>obj_at' P t\<rbrace> storePTE p pte \<lbrace>\<lambda>_. obj_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P t\<rbrace> setObject p pte \<lbrace>\<lambda>_. obj_at' P 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_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t\<rbrace> storePTE p pte \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>" by (wp tcb_in_cur_domain'_lift)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t\<rbrace> storePTE p pte \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>
theory VSpace_R

lemma storePTE_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace>ct_idle_or_in_cur_domain'\<rbrace> storePTE p pte \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" by (wp ct_idle_or_in_cur_domain'_lift hoare_vcg_disj_lift)

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

lemma setASIDPool_valid_objs [wp]:
  "\<lbrace>valid_objs' and valid_asid_pool' ap\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. valid_objs'\<rbrace>" apply (rule hoare_pre) apply (rule setObject_valid_objs') prefer 2 apply assumption apply (clarsimp simp: updateObject_default_def in_monad) apply (clarsimp simp: valid_obj'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_asid_pool' ap\<rbrace> setObject p ap \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject p ap \<lbrace>\<lambda>_. valid_objs'\<rbrace>
 2. \<And>s. (valid_objs' and valid_asid_pool' ap) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>x n ko s ko' s'. \<lbrakk>(ko', s') \<in> fst (updateObject ap ko p x n s); ?P3 s; valid_obj' ko s; lookupAround2 p (ksPSpace s) = (Some (x, ko), n)\<rbrakk> \<Longrightarrow> valid_obj' ko' s
 2. \<And>s. (valid_objs' and valid_asid_pool' ap) s \<Longrightarrow> (valid_objs' and ?P3) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_objs' and valid_asid_pool' ap) s \<Longrightarrow> (valid_objs' and ?P3) s
 2. \<And>x n ko s ko' s'. \<lbrakk>(ko', s') \<in> fst (updateObject ap ko p x n s); ?P3 s; valid_obj' ko s; lookupAround2 p (ksPSpace s) = (Some (x, ko), n)\<rbrakk> \<Longrightarrow> valid_obj' ko' s proof (prove)
goal (1 subgoal):
 1. \<And>x n ko s ko' s'. \<lbrakk>(ko', s') \<in> fst (updateObject ap ko p x n s); valid_asid_pool' ap s; valid_obj' ko s; lookupAround2 p (ksPSpace s) = (Some (x, ko), n)\<rbrakk> \<Longrightarrow> valid_obj' ko' s proof (prove)
goal (1 subgoal):
 1. \<And>n ko s s' s'' uu_. \<lbrakk>valid_asid_pool' ap s; valid_obj' ko s; lookupAround2 p (ksPSpace s) = (Some (p, ko), n); (uu_, s'') \<in> fst (projectKO ko s); is_aligned p (objBits ap); ((), s') \<in> fst (magnitudeCheck p n (objBits ap) s'')\<rbrakk> \<Longrightarrow> valid_obj' (KOArch (KOASIDPool ap)) s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setASIDPool_valid_mdb [wp]:
  "\<lbrace>valid_mdb'\<rbrace> setObject p (ap::asidpool) \<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> setObject p ap \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
theory VSpace_R

lemma setASIDPool_ksQ [wp]:
  "\<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>" by (wp setObject_qs updateObject_default_inv|simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setObject p ap \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>