kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_R

lemma get_ep_sp':
  "\<lbrace>P\<rbrace> getEndpoint r \<lbrace>\<lambda>t. P and ko_at' t r\<rbrace>" by (clarsimp simp: getEndpoint_def getObject_def loadObject_default_def
                     projectKOs in_monad valid_def obj_at'_def objBits_simps'
                     in_magnitude_check split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getEndpoint r \<lbrace>\<lambda>t. P and ko_at' t r\<rbrace>
theory KHeap_R

lemma setEndpoint_cur_tcb'[wp]:
  "\<lbrace>cur_tcb'\<rbrace> setEndpoint p v \<lbrace>\<lambda>rv. cur_tcb'\<rbrace>" apply (wp cur_tcb_lift) apply (simp add: setEndpoint_def setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb'\<rbrace> setEndpoint p v \<lbrace>\<lambda>rv. cur_tcb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setEndpoint p v \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 2. \<And>s. cur_tcb' s \<Longrightarrow> cur_tcb' s proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject_default v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>
 2. \<And>s. cur_tcb' s \<Longrightarrow> cur_tcb' s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma ex_nonz_cap_to_pres':
  assumes y: "\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>"
  shows      "\<lbrace>ex_nonz_cap_to' p\<rbrace> f \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" apply (simp only: ex_nonz_cap_to'_def) apply (intro hoare_vcg_disj_lift hoare_vcg_ex_lift
               y hoare_vcg_all_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> f \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setEndpoint_cap_to'[wp]:
  "\<lbrace>ex_nonz_cap_to' p\<rbrace> setEndpoint p' v \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" by (wp ex_nonz_cap_to_pres')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> setEndpoint p' v \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>
theory KHeap_R

lemma setEndpoint_idle'[wp]:
  "\<lbrace>\<lambda>s. valid_idle' s\<rbrace>
   setEndpoint p v
   \<lbrace>\<lambda>_. valid_idle'\<rbrace>" unfolding setEndpoint_def apply (wp setObject_idle') apply (simp add: objBits_simps' updateObject_default_inv)+ apply (clarsimp simp: projectKOs idle_tcb_ps_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> setEndpoint p v \<lbrace>\<lambda>_. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> setObject p v \<lbrace>\<lambda>_. valid_idle'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ko s x y n. updateObject v ko p y n s = updateObject_default v ko p y n s
 2. \<And>x. objBits x = ?n1
 3. 1 < 2 ^ ?n1
 4. \<And>P p q n ko. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> updateObject v p q n ko \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>
 5. \<And>s. valid_idle' s \<Longrightarrow> valid_idle' s \<and> (p = ksIdleThread s \<longrightarrow> (\<exists>val. idle_tcb_ps val) \<longrightarrow> idle_tcb_ps v) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_idle' s \<Longrightarrow> p = ksIdleThread s \<longrightarrow> Ex idle_tcb_ps \<longrightarrow> idle_tcb_ps v proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_ksPSpace_only:
  "\<lbrakk> \<And>p q n ko. \<lbrace>P\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv. P \<rbrace>;
        \<And>f s. P (ksPSpace_update f s) = P s \<rbrakk>
     \<Longrightarrow> \<lbrace>P\<rbrace> setObject ptr val \<lbrace>\<lambda>rv. P\<rbrace>" apply (simp add: setObject_def split_def) apply (wp | simp | assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p q n ko. \<lbrace>P\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv. P\<rbrace>; \<And>f s. P (ksPSpace_update f s) = P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> setObject ptr val \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>p q n ko. \<lbrace>P\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv. P\<rbrace>; \<And>f s. P (ksPSpace_update f s) = P s\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 ptr ps));
obj' <- updateObject val (snd p) ptr (fst p) (snd (lookupAround2 ptr ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_ksMachine:
  "\<lbrakk> \<And>p q n ko. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace> \<rbrakk>
     \<Longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setObject ptr val \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>" by (simp add: setObject_ksPSpace_only)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>p q n ko. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setObject ptr val \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>
theory KHeap_R

lemma setObject_ksInterrupt:
  "\<lbrakk> \<And>p q n ko. \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv s. P (ksInterruptState s)\<rbrace> \<rbrakk>
     \<Longrightarrow> \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> setObject ptr val \<lbrace>\<lambda>rv s. P (ksInterruptState s)\<rbrace>" by (simp add: setObject_ksPSpace_only)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>p q n ko. \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv s. P (ksInterruptState s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> setObject ptr val \<lbrace>\<lambda>rv s. P (ksInterruptState s)\<rbrace>
theory KHeap_R

lemma valid_irq_handlers_lift':
  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>"
  assumes y: "\<And>P. \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ksInterruptState s)\<rbrace>"
  shows      "\<lbrace>valid_irq_handlers'\<rbrace> f \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" apply (simp add: valid_irq_handlers'_def irq_issued'_def) apply (rule hoare_use_eq [where f=cteCaps_of, OF x y]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers'\<rbrace> f \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>cap\<in>ran (cteCaps_of s). \<forall>irq. cap = capability.IRQHandlerCap irq \<longrightarrow> intStateIRQTable (ksInterruptState s) irq = irqstate.IRQSignal\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ep_maxObj [wp]:
  "\<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv s. P (gsMaxObjectSize s)\<rbrace>" by (simp add: setEndpoint_def | wp setObject_ksPSpace_only updateObject_default_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> setEndpoint ptr val \<lbrace>\<lambda>rv s. P (gsMaxObjectSize s)\<rbrace>
theory KHeap_R

lemma setObject_ep_ct:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p (e::endpoint) \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>" apply (simp add: setObject_def updateObject_ep_eta split_def) apply (wp updateObject_default_inv | simp)+ done

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

lemma setObject_ntfn_ct:
  "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p (e::Structures_H.notification)
   \<lbrace>\<lambda>_ s. P (ksCurThread 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 (ksCurThread s)\<rbrace> setObject p e \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject_default e (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma get_ntfn_sp':
  "\<lbrace>P\<rbrace> getNotification r \<lbrace>\<lambda>t. P and ko_at' t r\<rbrace>" by (clarsimp simp: getNotification_def getObject_def loadObject_default_def
                     projectKOs in_monad valid_def obj_at'_def objBits_simps'
                     in_magnitude_check split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getNotification r \<lbrace>\<lambda>t. P and ko_at' t r\<rbrace>
theory KHeap_R

lemma set_ntfn_pred_tcb_at' [wp]:
  "\<lbrace> pred_tcb_at' proj P t \<rbrace>
   setNotification ep v
   \<lbrace> \<lambda>rv. pred_tcb_at' proj P t \<rbrace>" apply (simp add: setNotification_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> setNotification ep v \<lbrace>\<lambda>rv. 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 ep v \<lbrace>\<lambda>rv. 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 KHeap_R

lemma set_ntfn_cap_to'[wp]:
  "\<lbrace>ex_nonz_cap_to' p\<rbrace> setNotification p' v \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" by (wp ex_nonz_cap_to_pres')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> setNotification p' v \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>
theory KHeap_R

lemma setNotification_ifunsafe'[wp]:
  "\<lbrace>if_unsafe_then_cap'\<rbrace> setNotification p v \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" unfolding setNotification_def apply (rule setObject_ifunsafe'[where P="\<top>", simplified]) apply (clarsimp simp: updateObject_default_def in_monad projectKOs
                  intro!: equals0I)+ apply (simp add: setObject_def split_def) apply (wp updateObject_default_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap'\<rbrace> setNotification p v \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap'\<rbrace> setObject p v \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject v (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 v (KOCTE cte) p x n s) = {}
 3. \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setObject p v \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setObject p v \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject_default v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setNotification_idle'[wp]:
  "\<lbrace>\<lambda>s. valid_idle' s\<rbrace> setNotification p v \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" unfolding setNotification_def apply (wp setObject_idle') apply (simp add: objBits_simps' updateObject_default_inv)+ apply (clarsimp simp: projectKOs idle_tcb_ps_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> setNotification p v \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> setObject p v \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ko s x y n. updateObject v ko p y n s = updateObject_default v ko p y n s
 2. \<And>x. objBits x = ?n1
 3. 1 < 2 ^ ?n1
 4. \<And>P p q n ko. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> updateObject v p q n ko \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>
 5. \<And>s. valid_idle' s \<Longrightarrow> valid_idle' s \<and> (p = ksIdleThread s \<longrightarrow> (\<exists>val. idle_tcb_ps val) \<longrightarrow> idle_tcb_ps v) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_idle' s \<Longrightarrow> p = ksIdleThread s \<longrightarrow> Ex idle_tcb_ps \<longrightarrow> idle_tcb_ps v proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_arch' [wp]:
  "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setNotification ntfn p \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>" apply (simp add: setNotification_def setObject_def split_def) apply (wp updateObject_default_inv|simp)+ done

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

lemma set_ntfn_ksInterrupt[wp]:
  "\<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv s. P (ksInterruptState s)\<rbrace>" by (simp add: setNotification_def | wp setObject_ksInterrupt updateObject_default_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv s. P (ksInterruptState s)\<rbrace>
theory KHeap_R

lemma set_ntfn_ksMachine[wp]:
  "\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>" by (simp add: setNotification_def | wp setObject_ksMachine updateObject_default_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>
theory KHeap_R

lemma set_ntfn_maxObj [wp]:
  "\<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv s. P (gsMaxObjectSize s)\<rbrace>" by (simp add: setNotification_def | wp setObject_ksPSpace_only updateObject_default_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv s. P (gsMaxObjectSize s)\<rbrace>
theory KHeap_R

lemma set_ntfn_global_refs' [wp]:
  "\<lbrace>valid_global_refs'\<rbrace> setNotification ptr val \<lbrace>\<lambda>_. valid_global_refs'\<rbrace>" by (rule valid_global_refs_lift'; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> setNotification ptr val \<lbrace>\<lambda>_. valid_global_refs'\<rbrace>
theory KHeap_R

lemma set_ntfn_valid_arch' [wp]:
  "\<lbrace>valid_arch_state'\<rbrace> setNotification ptr val \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" by (rule valid_arch_state_lift'; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> setNotification ptr val \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>
theory KHeap_R

lemma valid_irq_states_lift':
  assumes x: "\<And>P. \<lbrace>\<lambda>s. P (intStateIRQTable (ksInterruptState s))\<rbrace> f \<lbrace>\<lambda>rv s. P (intStateIRQTable (ksInterruptState s))\<rbrace>"
  assumes y: "\<And>P. \<lbrace>\<lambda>s. P (irq_masks (ksMachineState s))\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_masks (ksMachineState s))\<rbrace>"
  shows      "\<lbrace>valid_irq_states'\<rbrace> f \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace>" apply (rule hoare_use_eq [where f="\<lambda>s. irq_masks (ksMachineState s)"], rule y) apply (rule hoare_use_eq [where f="\<lambda>s. intStateIRQTable (ksInterruptState s)"], rule x) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> f \<lbrace>\<lambda>rv. valid_irq_states'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>fa. \<lbrace>\<lambda>s. valid_irq_masks' (intStateIRQTable (ksInterruptState s)) fa\<rbrace> f \<lbrace>\<lambda>rv s. valid_irq_masks' (intStateIRQTable (ksInterruptState s)) fa\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>fa faa. \<lbrace>\<lambda>s. valid_irq_masks' faa fa\<rbrace> f \<lbrace>\<lambda>rv s. valid_irq_masks' faa fa\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma valid_pde_mappings'_def2:
  "valid_pde_mappings' =
     (\<lambda>s. \<forall>x. pde_at' x s \<longrightarrow> obj_at' (valid_pde_mapping' (x && mask pdBits)) x s)" apply (clarsimp simp: valid_pde_mappings'_def typ_at_to_obj_at_arches) apply (rule ext, rule iff_allI) apply (clarsimp simp: obj_at'_def projectKOs) apply (auto simp add: objBits_simps archObjSize_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pde_mappings' = (\<lambda>s. \<forall>x. pde_at' x s \<longrightarrow> obj_at' (valid_pde_mapping' (x && mask pdBits)) x s) proof (prove)
goal (1 subgoal):
 1. (\<lambda>s. \<forall>x pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) = (\<lambda>s. \<forall>x. obj_at' (\<lambda>_. True) x s \<longrightarrow> obj_at' (valid_pde_mapping' (x && mask pdBits)) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. (\<forall>pde. ko_at' pde x s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) = (obj_at' (\<lambda>_. True) x s \<longrightarrow> obj_at' (valid_pde_mapping' (x && mask pdBits)) x s) proof (prove)
goal (1 subgoal):
 1. \<And>s x. (\<forall>pde. ksPSpace s x = Some (KOArch (KOPDE pde)) \<and> is_aligned x (objBitsKO (KOArch (KOPDE pde))) \<and> ps_clear x (objBitsKO (KOArch (KOPDE pde))) s \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde) = ((\<exists>ko. ksPSpace s x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (\<exists>obj. ko = KOArch (KOPDE obj)) \<and> ps_clear x (objBitsKO ko) s) \<longrightarrow> (\<exists>ko. ksPSpace s x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (\<exists>obj. ko = KOArch (KOPDE obj) \<and> valid_pde_mapping' (x && mask pdBits) obj \<and> ps_clear x (objBitsKO ko) s))) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma valid_pde_mappings_lift':
  assumes x: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>"
  assumes y: "\<And>x. \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace>
                    f \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace>"
  shows      "\<lbrace>valid_pde_mappings'\<rbrace> f \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (simp only: valid_pde_mappings'_def2 imp_conv_disj) apply (rule hoare_vcg_all_lift hoare_vcg_disj_lift x y)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings'\<rbrace> f \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. \<not> pde_at' x s \<or> obj_at' (valid_pde_mapping' (x && mask pdBits)) x s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x. \<not> pde_at' x s \<or> obj_at' (valid_pde_mapping' (x && mask pdBits)) x s\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ntfn_valid_pde_mappings'[wp]:
  "\<lbrace>valid_pde_mappings'\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (rule valid_pde_mappings_lift') apply wp apply (simp add: setNotification_def) apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_default_def in_monad) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings'\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>
 2. \<And>x. \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> setNotification ptr val \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> setObject ptr val \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (x && mask pdBits)) x\<rbrace> proof (prove)
goal (1 subgoal):
 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) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma irqs_masked_lift:
  assumes "\<And>P. \<lbrace>\<lambda>s. P (intStateIRQTable (ksInterruptState s))\<rbrace> f
               \<lbrace>\<lambda>rv s. P (intStateIRQTable (ksInterruptState s))\<rbrace>"
  shows "\<lbrace>irqs_masked'\<rbrace> f \<lbrace>\<lambda>_. irqs_masked'\<rbrace>" apply (simp add: irqs_masked'_def) apply (wp assms) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>irqs_masked'\<rbrace> f \<lbrace>\<lambda>_. irqs_masked'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>irq>maxIRQ. intStateIRQTable (ksInterruptState s) irq = irqstate.IRQInactive\<rbrace> proof (prove)
goal:
No subgoals!