kings-crown/FVELER_Isabelle huggingface dataset:
theory KHeap_R

lemma setObject_ksDomSchedule_inv:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setObject t (v::tcb) \<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 KHeap_R

lemma projectKO_def2:
  "projectKO ko = assert_opt (projectKO_opt ko)" by (simp add: projectKO_def assert_opt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. projectKO ko = assert_opt (projectKO_opt ko)
theory KHeap_R

lemma setObject_qs[wp]:
  assumes x: "\<And>q n obj. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> updateObject v obj p q n \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setObject p v \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp x | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> setObject p v \<lbrace>\<lambda>rv s. P (ksReadyQueues s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject 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 (ksReadyQueues s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_qsL1[wp]:
  assumes x: "\<And>q n obj. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> updateObject v obj p q n \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> setObject p v \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp x | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> setObject p v \<lbrace>\<lambda>rv s. P (ksReadyQueuesL1Bitmap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL1Bitmap s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject 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 (ksReadyQueuesL1Bitmap s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_qsL2[wp]:
  assumes x: "\<And>q n obj. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> updateObject v obj p q n \<lbrace>\<lambda>rv s. P (ksReadyQueuesL2Bitmap s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> setObject p v \<lbrace>\<lambda>rv s. P (ksReadyQueuesL2Bitmap s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp x | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> setObject p v \<lbrace>\<lambda>rv s. P (ksReadyQueuesL2Bitmap s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksReadyQueuesL2Bitmap s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject 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 (ksReadyQueuesL2Bitmap s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_ifunsafe':
  fixes v :: "'a :: pspace_storable"
  assumes x: "\<And>x n tcb s t. \<lbrakk> t \<in> fst (updateObject v (KOTCB tcb) ptr x n s); P s;
                               lookupAround2 ptr (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)"
  assumes y: "\<And>x n cte s. fst (updateObject v (KOCTE cte) ptr x n s) = {}"
  assumes z: "\<And>P. \<lbrace>\<lambda>s. P (intStateIRQNode (ksInterruptState s))\<rbrace>
                     setObject ptr v \<lbrace>\<lambda>rv s. P (intStateIRQNode (ksInterruptState s))\<rbrace>"
  shows      "\<lbrace>\<lambda>s. if_unsafe_then_cap' s \<and> P s\<rbrace>
                setObject ptr v
              \<lbrace>\<lambda>rv s. if_unsafe_then_cap' s\<rbrace>" apply (simp only: if_unsafe_then_cap'_def ex_cte_cap_to'_def
                    cte_wp_at_ctes_of) apply (rule hoare_use_eq_irq_node' [OF z]) apply (rule setObject_ctes_of [OF x y], assumption+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_unsafe_then_cap' s \<and> P s\<rbrace> setObject ptr v \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>crefa cte. ctes_of s crefa = Some cte \<and> True \<and> cref \<in> cte_refs' (cteCap cte) (irq_node' s))) \<and> P s\<rbrace> setObject ptr v \<lbrace>\<lambda>rv s. \<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>crefa cte. ctes_of s crefa = Some cte \<and> True \<and> cref \<in> cte_refs' (cteCap cte) (irq_node' s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrace>\<lambda>s. (\<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>crefa cte. ctes_of s crefa = Some cte \<and> True \<and> cref \<in> cte_refs' (cteCap cte) f)) \<and> P s\<rbrace> setObject ptr v \<lbrace>\<lambda>rv s. \<forall>cref. (\<exists>cte. ctes_of s cref = Some cte \<and> cteCap cte \<noteq> capability.NullCap) \<longrightarrow> (\<exists>crefa cte. ctes_of s crefa = Some cte \<and> True \<and> cref \<in> cte_refs' (cteCap cte) f)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setObject_it[wp]:
  assumes x: "\<And>p q n ko. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>"
  shows      "\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setObject t val \<lbrace>\<lambda>rv s. P (ksIdleThread s)\<rbrace>" apply (simp add: setObject_def split_def) apply (wp x | simp)+ done

\<comment>\<open>
  `idle_tcb_ps val` asserts that `val` is a pspace_storable value
  which corresponds to an idle TCB.
\<close>

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

lemma setObject_no_0_obj' [wp]:
  "\<lbrace>no_0_obj'\<rbrace> setObject p v \<lbrace>\<lambda>r. no_0_obj'\<rbrace>" apply (clarsimp simp: setObject_def split_def) apply (clarsimp simp: valid_def no_0_obj'_def ko_wp_at'_def in_monad
                        lookupAround2_char1 ps_clear_upd) done

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

lemma no_fail_threadGet [wp]:
  "no_fail (tcb_at' t) (threadGet f t)" by (simp add: threadGet_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at' t) (threadGet f t)
theory KHeap_R

lemma no_fail_getThreadState [wp]:
  "no_fail (tcb_at' t) (getThreadState t)" by (simp add: getThreadState_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at' t) (getThreadState t)
theory KHeap_R

lemma no_fail_setObject_tcb [wp]:
  "no_fail (tcb_at' t) (setObject t (t'::tcb))" apply (rule no_fail_pre, wp) apply (rule ext)+ apply simp apply (simp add: objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at' t) (setObject t t') proof (prove)
goal (2 subgoals):
 1. updateObject t' = updateObject_default t'
 2. \<And>s. tcb_at' t s \<Longrightarrow> obj_at' (\<lambda>k. objBits k = objBits t') t s proof (prove)
goal (2 subgoals):
 1. \<And>x xa xb xc xd. updateObject t' x xa xb xc xd = updateObject_default t' x xa xb xc xd
 2. \<And>s. tcb_at' t s \<Longrightarrow> obj_at' (\<lambda>k. objBits k = objBits t') t s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> obj_at' (\<lambda>k. objBits k = objBits t') t s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma no_fail_threadSet [wp]:
  "no_fail (tcb_at' t) (threadSet f t)" apply (simp add: threadSet_def) apply (rule no_fail_pre, wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at' t) (threadSet f t) proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at' t) (do tcb <- getObject t;
setObject t (f tcb)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and tcb_at' t) s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma dmo_return' [simp]:
  "doMachineOp (return x) = return x" apply (simp add: doMachineOp_def select_f_def return_def gets_def get_def
                   bind_def modify_def put_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doMachineOp (return x) = return x proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma dmo_storeWordVM' [simp]:
  "doMachineOp (storeWordVM x y) = return ()" by (simp add: storeWordVM_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. doMachineOp (storeWordVM x y) = return ()
theory KHeap_R

lemma no_fail_dmo' [wp]:
  "no_fail P f \<Longrightarrow> no_fail (P o ksMachineState) (doMachineOp f)" apply (simp add: doMachineOp_def split_def) apply (rule no_fail_pre, wp) apply simp apply (simp add: no_fail_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail P f \<Longrightarrow> no_fail (P \<circ> ksMachineState) (doMachineOp f) proof (prove)
goal (1 subgoal):
 1. no_fail P f \<Longrightarrow> no_fail (P \<circ> ksMachineState) (do ms <- gets ksMachineState;
p <- select_f (f ms);
y <- modify (ksMachineState_update (\<lambda>_. snd p));
return (fst p)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_fail P f; (P \<circ> ksMachineState) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>sa. \<not> snd (f (ksMachineState s))) and (\<lambda>sa. \<forall>x\<in>fst (f (ksMachineState s)). ((\<lambda>_. True) and (\<lambda>s. True)) sa)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_fail P f; P (ksMachineState s)\<rbrakk> \<Longrightarrow> \<not> snd (f (ksMachineState s)) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setEndpoint_nosch[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
    setEndpoint val ptr
   \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" apply (simp add: setEndpoint_def) apply (rule setObject_nosch) apply (simp add: updateObject_default_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setEndpoint val ptr \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setObject val ptr \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> updateObject ptr p q n ko \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do y <- assert (q = n);
_ <- projectKO p;
y <- alignCheck q (objBits ptr);
y <- magnitudeCheck q ko (objBits ptr);
return (KOEndpoint ptr)
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko s. P (ksSchedulerAction s) \<Longrightarrow> q = n \<longrightarrow> P (ksSchedulerAction s) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma setNotification_nosch[wp]:
  "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
    setNotification val ptr
   \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>" apply (simp add: setNotification_def) apply (rule setObject_nosch) apply (simp add: updateObject_default_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setNotification val ptr \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> setObject val ptr \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> updateObject ptr p q n ko \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> do y <- assert (q = n);
_ <- projectKO p;
y <- alignCheck q (objBits ptr);
y <- magnitudeCheck q ko (objBits ptr);
return (KONotification ptr)
od \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>p q n ko s. P (ksSchedulerAction s) \<Longrightarrow> q = n \<longrightarrow> P (ksSchedulerAction s) proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ep_valid_objs':
  "\<lbrace>valid_objs' and valid_ep' ep\<rbrace>
  setEndpoint epptr ep
  \<lbrace>\<lambda>r s. valid_objs' s\<rbrace>" apply (simp add: setEndpoint_def) apply (rule setObject_valid_objs') apply (clarsimp simp: updateObject_default_def in_monad
                        projectKOs valid_obj'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_ep' ep\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and valid_ep' ep\<rbrace> setObject epptr ep \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x n ko s ko' s'. \<lbrakk>(ko', s') \<in> fst (updateObject ep ko epptr x n s); valid_ep' ep s; valid_obj' ko s; lookupAround2 epptr (ksPSpace s) = (Some (x, ko), n)\<rbrakk> \<Longrightarrow> valid_obj' ko' s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ep_ctes_of[wp]:
  "\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> setEndpoint p val \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" apply (simp add: setEndpoint_def) apply (rule setObject_ctes_of[where Q="\<top>", simplified]) apply (clarsimp simp: updateObject_default_def in_monad
                         projectKOs) apply (clarsimp simp: updateObject_default_def bind_def
                        projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> setEndpoint p val \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> setObject p val \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x n tcb s t. \<lbrakk>t \<in> fst (updateObject val (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 val (KOCTE cte) p x n s) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x n cte s. fst (updateObject val (KOCTE cte) p x n s) = {} proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ep_valid_mdb' [wp]:
  "\<lbrace>valid_mdb'\<rbrace>
     setObject epptr (ep::endpoint)
   \<lbrace>\<lambda>_. valid_mdb'\<rbrace>" apply (simp add: valid_mdb'_def) apply (rule set_ep_ctes_of[simplified setEndpoint_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_mdb'\<rbrace> setObject epptr ep \<lbrace>\<lambda>_. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb_ctes (ctes_of s)\<rbrace> setObject epptr ep \<lbrace>\<lambda>_ s. valid_mdb_ctes (ctes_of s)\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ep_valid_pspace'[wp]:
  "\<lbrace>valid_pspace' and valid_ep' ep\<rbrace>
  setEndpoint epptr ep
  \<lbrace>\<lambda>r. valid_pspace'\<rbrace>" apply (simp add: valid_pspace'_def) apply (wp set_ep_aligned' [simplified] set_ep_valid_objs') apply (wp hoare_vcg_conj_lift) apply (simp add: setEndpoint_def) apply (wp setEndpoint_valid_mdb')+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace' and valid_ep' ep\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and valid_ep' ep\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>r. valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'9\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv s. no_0_obj' s \<and> valid_mdb' s\<rbrace>
 2. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and valid_ep' ep) s \<Longrightarrow> (valid_objs' and valid_ep' ep) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> ?P'9 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P12\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. no_0_obj'\<rbrace>
 2. \<lbrace>?P'12\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
 3. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and valid_ep' ep) s \<Longrightarrow> (valid_objs' and valid_ep' ep) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> ?P12 s \<and> ?P'12 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P12\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv. no_0_obj'\<rbrace>
 2. \<lbrace>?P'12\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
 3. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and valid_ep' ep) s \<Longrightarrow> (valid_objs' and valid_ep' ep) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> ?P12 s \<and> ?P'12 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_objs' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_mdb' and valid_ep' ep) s \<Longrightarrow> (valid_objs' and valid_ep' ep) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ep_valid_bitmapQ[wp]:
  "\<lbrace>Invariants_H.valid_bitmapQ\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. Invariants_H.valid_bitmapQ\<rbrace>" apply (unfold setEndpoint_def) apply (rule setObject_ep_pre) apply (simp add: bitmapQ_defs setObject_def split_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift updateObject_default_inv | simp add: bitmapQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_bitmapQ and ep_at' epptr\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv. valid_bitmapQ\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])) and ep_at' epptr\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 epptr ps));
obj' <- updateObject_default ep (snd p) epptr (fst p) (snd (lookupAround2 epptr ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. \<forall>d p. (ksReadyQueuesL1Bitmap s d !! prioToL1Index p \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) !! unat (p && mask wordRadix)) = (ksReadyQueues s (d, p) \<noteq> [])\<rbrace> proof (prove)
goal:
No subgoals!
theory KHeap_R

lemma set_ep_bitmapQ_no_L1_orphans[wp]:
  "\<lbrace> bitmapQ_no_L1_orphans \<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans \<rbrace>" apply (unfold setEndpoint_def) apply (rule setObject_ep_pre) apply (simp add: bitmapQ_defs setObject_def split_def) apply (wp hoare_Ball_helper hoare_vcg_all_lift updateObject_default_inv | simp add: bitmapQ_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> setEndpoint epptr ep \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bitmapQ_no_L1_orphans and ep_at' epptr\<rbrace> setObject epptr ep \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize) and ep_at' epptr\<rbrace> do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 epptr ps));
obj' <- updateObject_default ep (snd p) epptr (fst p) (snd (lookupAround2 epptr ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> i < l2BitmapSize\<rbrace> proof (prove)
goal:
No subgoals!