kings-crown/FVELER_Isabelle huggingface dataset:
theory VSpace_R

lemma setASIDPool_inQ[wp]:
  "\<lbrace>\<lambda>s. P (obj_at' (inQ d p) t s)\<rbrace>
     setObject ptr (ap::asidpool)
   \<lbrace>\<lambda>rv s. P (obj_at' (inQ d p) t s)\<rbrace>" apply (simp add: obj_at'_real_def) apply (wp setObject_ko_wp_at
            | simp add: objBits_simps archObjSize_def)+ apply (simp add: pageBits_def) apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' (inQ d p) t s)\<rbrace> setObject ptr ap \<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 ap \<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 (2 subgoals):
 1. 1 < 2 ^ pageBits
 2. \<And>s. P (ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s) \<Longrightarrow> obj_at' (\<lambda>x. True) ptr s \<longrightarrow> P (ko_wp_at' (if ptr = t then K (\<exists>obj. projectKO_opt (injectKO ap) = Some obj \<and> inQ d p obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ d p obj)) t s) 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> obj_at' (\<lambda>x. True) ptr s \<longrightarrow> P (ko_wp_at' (if ptr = t then K (\<exists>obj. projectKO_opt (injectKO ap) = Some obj \<and> inQ d p obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ d p obj)) t s) proof (prove)
goal:
No subgoals!
theory VSpace_R

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

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

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

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

lemma setASIDPool_valid_queues [wp]:
  "\<lbrace>Invariants_H.valid_queues\<rbrace> setObject p (ap::asidpool) \<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> setObject p ap \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>
theory VSpace_R

lemma setASIDPool_valid_queues' [wp]:
  "\<lbrace>valid_queues'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. valid_queues'\<rbrace>" by (wp valid_queues_lift')

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

lemma setASIDPool_state_refs' [wp]:
  "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" 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> setObject p ap \<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 (KOASIDPool uu_)); is_aligned p (archObjSize (KOASIDPool ap)); ((), s'') \<in> fst (magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (archObjSize (KOASIDPool ap)) 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 (KOASIDPool ap)) 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 setASIDPool_iflive [wp]:
  "\<lbrace>if_live_then_nonz_cap'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" 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 pageBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap'\<rbrace> setObject p ap \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject p ap \<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 ap (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 ap (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 ap) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal (4 subgoals):
 1. 1 < 2 ^ pageBits
 2. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject ap (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 ap (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 ap) \<longrightarrow> ex_nonz_cap_to' p s) \<and> True proof (prove)
goal:
No subgoals!
theory VSpace_R

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

lemma setASIDPool_ifunsafe [wp]:
  "\<lbrace>if_unsafe_then_cap'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" 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> setObject p ap \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject p ap \<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 ap (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 ap (KOCTE cte) p x n s) = {}
 3. \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setObject p ap \<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 ap \<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 setASIDPool_it' [wp]:
  "\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. \<lambda>s. P (ksIdleThread s)\<rbrace>" by (wp setObject_it updateObject_default_inv|simp)+

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

lemma setASIDPool_idle [wp]:
  "\<lbrace>valid_idle'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" by valid_idle'_setObject

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

lemma setASIDPool_irq_states' [wp]:
  "\<lbrace>valid_irq_states'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>" apply (rule hoare_pre) apply (rule hoare_use_eq [where f=ksInterruptState, OF setObject_ksInterrupt]) apply (simp, rule updateObject_default_inv) apply (rule hoare_use_eq [where f=ksMachineState, OF setObject_ksMachine]) apply (simp, rule updateObject_default_inv) apply wp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> setObject p ap \<lbrace>\<lambda>_. valid_irq_states'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setObject p ap \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>P p q n ko. \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> updateObject ap p q n ko \<lbrace>\<lambda>_ s. P (ksInterruptState s)\<rbrace>
 2. \<And>f. \<lbrace>?P3 f\<rbrace> setObject p ap \<lbrace>\<lambda>_ s. valid_irq_masks' (intStateIRQTable f) (irq_masks (ksMachineState s))\<rbrace>
 3. \<And>s. valid_irq_states' s \<Longrightarrow> ?P3 (ksInterruptState s) s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> setObject p ap \<lbrace>\<lambda>_ s. valid_irq_masks' (intStateIRQTable f) (irq_masks (ksMachineState s))\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?P3 (ksInterruptState s) s proof (prove)
goal (3 subgoals):
 1. \<And>f P p q n ko. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> updateObject ap p q n ko \<lbrace>\<lambda>_ s. P (ksMachineState s)\<rbrace>
 2. \<And>f fa. \<lbrace>?P16 f fa\<rbrace> setObject p ap \<lbrace>\<lambda>_ s. valid_irq_masks' (intStateIRQTable f) (irq_masks fa)\<rbrace>
 3. \<And>s. valid_irq_states' s \<Longrightarrow> ?P16 (ksInterruptState s) (ksMachineState s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa. \<lbrace>?P16 f fa\<rbrace> setObject p ap \<lbrace>\<lambda>_ s. valid_irq_masks' (intStateIRQTable f) (irq_masks fa)\<rbrace>
 2. \<And>s. valid_irq_states' s \<Longrightarrow> ?P16 (ksInterruptState s) (ksMachineState s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states' s \<Longrightarrow> valid_irq_states' s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setObject_asidpool_mappings'[wp]:
  "\<lbrace>valid_pde_mappings'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (wp valid_pde_mappings_lift') 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> setObject p ap \<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> setObject p ap \<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 setASIDPool_vms'[wp]:
  "\<lbrace>valid_machine_state'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" apply (simp add: 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> setObject p ap \<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 ap \<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 setASIDPool_ct_not_inQ[wp]:
  "\<lbrace>ct_not_inQ\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" apply (rule ct_not_inQ_lift [OF setObject_nosch]) apply (simp add: updateObject_default_def | wp)+ apply (rule hoare_weaken_pre) apply (wps setObject_ASID_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> setObject p ap \<lbrace>\<lambda>_. ct_not_inQ\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P p q n ko. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> updateObject ap p q n ko \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 2. \<lbrace>\<lambda>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> setObject p ap \<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 ap \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q23\<rbrace> setObject p ap \<lbrace>\<lambda>_ s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?Q23 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P26 prev_s\<rbrace> setObject p ap \<lbrace>\<lambda>rv. obj_at' (Not \<circ> tcbQueued) (ksCurThread prev_s)\<rbrace>
 2. \<And>s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<Longrightarrow> ?P26 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_asidpool_cur'[wp]:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>" apply (simp add: setObject_def) apply (wp | wpc | simp add: updateObject_default_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p ap \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do ps <- gets ksPSpace;
case lookupAround2 p ps of (before, after) \<Rightarrow> do (ptr', obj) <- assert_opt before;
obj' <- updateObject_default ap obj p ptr' after;
modify (ksPSpace_update (\<lambda>_. ps(ptr' \<mapsto> obj')))
od
od \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setObject_asidpool_cur_domain[wp]:
  "\<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject p (ap::asidpool) \<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 p ap \<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;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject_default ap (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setObject_asidpool_ksDomSchedule[wp]:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setObject p (ap::asidpool) \<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 p ap \<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;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject_default ap (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setObject_tcb_obj_at'[wp]:
  "\<lbrace>obj_at' (P::tcb \<Rightarrow> bool) t\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. obj_at' P t\<rbrace>" 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> setObject p ap \<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 setObject_asidpool_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t\<rbrace> setObject p (ap::asidpool) \<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> setObject p ap \<lbrace>\<lambda>_. tcb_in_cur_domain' t\<rbrace>
theory VSpace_R

lemma setObject_asidpool_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace>ct_idle_or_in_cur_domain'\<rbrace> setObject p (ap::asidpool) \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" apply (rule ct_idle_or_in_cur_domain'_lift) apply (wp hoare_vcg_disj_lift)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> setObject p ap \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setObject p ap \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setObject p ap \<lbrace>\<lambda>_ s. P (ksSchedulerAction s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setObject p ap \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p ap \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 5. \<And>d a t t'. \<lbrace>\<lambda>s. t = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s\<rbrace> setObject p ap \<lbrace>\<lambda>_ s. t = t' \<or> obj_at' (\<lambda>tcb. d = tcbDomain tcb) t s\<rbrace> proof (prove)
goal:
No subgoals!
theory VSpace_R

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

lemma setVMRootForFlush_invs'[wp]: "\<lbrace>invs'\<rbrace> setVMRootForFlush a b \<lbrace>\<lambda>_. invs'\<rbrace>" apply (simp add: setVMRootForFlush_def) apply (wp storePDE_Invalid_invs mapM_wp' crunch_wps | simp add: crunch_simps)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> setVMRootForFlush a b \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do tcb <- getCurThread;
threadRootSlot <- getThreadVSpaceRoot tcb;
threadRoot <- getSlotCap threadRootSlot;
if isArchObjectCap threadRoot \<and> isPageDirectoryCap (capCap threadRoot) \<and> (\<exists>y. capPDMappedASID (capCap threadRoot) = Some y) \<and> capPDBasePtr (capCap threadRoot) = a then let cur_pd = a in return False else do armv_contextSwitch a b;
return True
od
od \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal:
No subgoals!