kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_R

lemma doIPCTransfer_non_null_cte_wp_at':
  assumes PUC: "\<And>cap. P cap \<Longrightarrow> \<not> isUntypedCap cap"
  shows
  "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>
   doIPCTransfer sender endpoint badge grant receiver
   \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace>" unfolding doIPCTransfer_def apply (wp doNormalTransfer_non_null_cte_wp_at' hoare_drop_imp hoare_allI | wpc | clarsimp simp:PUC)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> doIPCTransfer sender endpoint badge grant receiver \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> do receiveBuffer <- lookupIPCBuffer True receiver;
fault <- threadGet tcbFault sender;
case fault of None \<Rightarrow> do sendBuffer <- lookupIPCBuffer False sender;
doNormalTransfer sender sendBuffer endpoint badge grant receiver receiveBuffer
od | Some v21 \<Rightarrow> doFaultTransfer badge sender receiver receiveBuffer
od \<lbrace>\<lambda>_. cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) ptr\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma st_tcb_at'_eqD:
  "\<lbrakk> st_tcb_at' (\<lambda>s. s = st) t s; st_tcb_at' (\<lambda>s. s = st') t s \<rbrakk> \<Longrightarrow> st = st'" by (clarsimp simp add: pred_tcb_at'_def obj_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' (\<lambda>s. s = st) t s; st_tcb_at' (\<lambda>s. s = st') t s\<rbrakk> \<Longrightarrow> st = st'
theory Syscall_R

lemma isReply_awaiting_reply':
  "isReply st = awaiting_reply' st" by (case_tac st, (clarsimp simp add: isReply_def)+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isReply st = awaiting_reply' st
theory Syscall_R

lemma ct_active_runnable' [simp]:
  "ct_active' s \<Longrightarrow> ct_in_state' runnable' s" by (fastforce simp: ct_in_state'_def elim!: pred_tcb'_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_active' s \<Longrightarrow> ct_in_state' runnable' s
theory Syscall_R

lemma valid_irq_node_tcbSchedEnqueue[wp]:
  "\<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s \<rbrace> tcbSchedEnqueue ptr
  \<lbrace>\<lambda>rv s'. valid_irq_node' (irq_node' s') s'\<rbrace>" apply (rule hoare_pre) apply (simp add:valid_irq_node'_def ) apply (wp unless_wp hoare_vcg_all_lift | wps)+ apply (simp add:tcbSchedEnqueue_def) apply (wp unless_wp| simp)+ apply (simp add:valid_irq_node'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_irq_node' (irq_node' s) s\<rbrace> tcbSchedEnqueue ptr \<lbrace>\<lambda>rv s'. valid_irq_node' (irq_node' s') s'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> tcbSchedEnqueue ptr \<lbrace>\<lambda>rv s'. valid_irq_node' (irq_node' s') s'\<rbrace>
 2. \<And>s. valid_irq_node' (irq_node' s) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> tcbSchedEnqueue ptr \<lbrace>\<lambda>rv s'. is_aligned (irq_node' s') (size 0 + cteSizeBits) \<and> (\<forall>irq. real_cte_at' (irq_node' s' + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) s')\<rbrace>
 2. \<And>s. valid_irq_node' (irq_node' s) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>irq prev_s. \<lbrace>?P8 irq prev_s\<rbrace> tcbSchedEnqueue ptr \<lbrace>\<lambda>rv. real_cte_at' (irq_node' prev_s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits))\<rbrace>
 2. \<And>s. valid_irq_node' (irq_node' s) s \<Longrightarrow> is_aligned (irq_node' s) (size 0 + cteSizeBits) \<and> (\<forall>x. ?P8 x s s) proof (prove)
goal (2 subgoals):
 1. \<And>irq prev_s. \<lbrace>?P8 irq prev_s\<rbrace> do queued <- threadGet tcbQueued ptr;
unless queued (do tdom <- threadGet tcbDomain ptr;
prio <- threadGet tcbPriority ptr;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (ptr # queue);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) ptr
od)
od \<lbrace>\<lambda>rv. real_cte_at' (irq_node' prev_s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits))\<rbrace>
 2. \<And>s. valid_irq_node' (irq_node' s) s \<Longrightarrow> is_aligned (irq_node' s) (size 0 + cteSizeBits) \<and> (\<forall>x. ?P8 x s s) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_node' (irq_node' s) s \<Longrightarrow> is_aligned (irq_node' s) (size 0 + cteSizeBits) \<and> (\<forall>x. real_cte_at' (irq_node' s + (UCAST(10 \<rightarrow> 32) x << cteSizeBits)) s) proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma rescheduleRequired_valid_queues_but_ct_domain:
  "\<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> valid_objs' s
     \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s) \<rbrace>
    rescheduleRequired
   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> valid_objs' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. Invariants_H.valid_queues s \<and> valid_objs' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma rescheduleRequired_valid_queues'_but_ct_domain:
  "\<lbrace>\<lambda>s. valid_queues' s
     \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)
   \<rbrace>
    rescheduleRequired
   \<lbrace>\<lambda>_. valid_queues'\<rbrace>" apply (simp add: rescheduleRequired_def) apply (wp | wpc | simp | fastforce simp: valid_queues'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)\<rbrace> rescheduleRequired \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_queues' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)\<rbrace> do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma tcbSchedEnqueue_valid_action:
  "\<lbrace>\<lambda>s. \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s\<rbrace>
  tcbSchedEnqueue ptr
  \<lbrace>\<lambda>rv s. \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s\<rbrace>" apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s\<rbrace> tcbSchedEnqueue ptr \<lbrace>\<lambda>rv s. \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s \<Longrightarrow> \<forall>x. sch_act_not x s \<or> st_tcb_at' runnable' x s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma threadSet_not_curthread_ct_domain:
  "\<lbrace>\<lambda>s. ptr \<noteq> ksCurThread s \<and> ct_idle_or_in_cur_domain' s\<rbrace> threadSet f ptr \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace>" apply (simp add:ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) apply (wp hoare_vcg_imp_lift hoare_vcg_disj_lift | wps)+ apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ptr \<noteq> ksCurThread s \<and> ct_idle_or_in_cur_domain' s\<rbrace> threadSet f ptr \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ptr \<noteq> ksCurThread s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s)\<rbrace> threadSet f ptr \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ptr \<noteq> ksCurThread s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) (ksCurThread s) s) \<Longrightarrow> ksSchedulerAction s \<noteq> ResumeCurrentThread \<or> ksCurThread s = ksIdleThread s \<or> obj_at' (\<lambda>obj. if ptr = ksCurThread s then ksCurDomain s = tcbDomain (f obj) else ksCurDomain s = tcbDomain obj) (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma getSlotCap_to_refs[wp]:
  "\<lbrace>\<top>\<rbrace> getSlotCap ref \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs' rv. ex_nonz_cap_to' r s\<rbrace>" by (simp add: getSlotCap_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getSlotCap ref \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs' rv. ex_nonz_cap_to' r s\<rbrace>
theory Syscall_R

lemma lcs_valid' [wp]:
  "\<lbrace>invs'\<rbrace> lookupCapAndSlot t xs \<lbrace>\<lambda>x s. s \<turnstile>' fst x\<rbrace>, -" unfolding lookupCapAndSlot_def apply (rule hoare_pre) apply (wp|clarsimp simp: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> lookupCapAndSlot t xs \<lbrace>\<lambda>x. valid_cap' (fst x)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doE slot <- lookupSlotForThread t xs;
cap <- withoutFailure $ getSlotCap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x. valid_cap' (fst x)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE slot <- lookupSlotForThread t xs;
cap <- withoutFailure $ getSlotCap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x. valid_cap' (fst x)\<rbrace>, -
 2. \<And>s. invs' s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma lcs_ex_cap_to' [wp]:
  "\<lbrace>invs'\<rbrace> lookupCapAndSlot t xs \<lbrace>\<lambda>x s. \<forall>r\<in>cte_refs' (fst x) (irq_node' s). ex_cte_cap_to' r s\<rbrace>, -" unfolding lookupCapAndSlot_def apply (rule hoare_pre) apply (wp | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> lookupCapAndSlot t xs \<lbrace>\<lambda>x s. \<forall>r\<in>cte_refs' (fst x) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doE slot <- lookupSlotForThread t xs;
cap <- withoutFailure $ getSlotCap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x s. \<forall>r\<in>cte_refs' (fst x) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE slot <- lookupSlotForThread t xs;
cap <- withoutFailure $ getSlotCap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x s. \<forall>r\<in>cte_refs' (fst x) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s\<rbrace>, -
 2. \<And>s. invs' s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma lcs_ex_nonz_cap_to' [wp]:
  "\<lbrace>invs'\<rbrace> lookupCapAndSlot t xs \<lbrace>\<lambda>x s. \<forall>r\<in>zobj_refs' (fst x). ex_nonz_cap_to' r s\<rbrace>, -" unfolding lookupCapAndSlot_def apply (rule hoare_pre) apply (wp | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> lookupCapAndSlot t xs \<lbrace>\<lambda>x s. \<forall>r\<in>zobj_refs' (fst x). ex_nonz_cap_to' r s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doE slot <- lookupSlotForThread t xs;
cap <- withoutFailure $ getSlotCap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x s. \<forall>r\<in>zobj_refs' (fst x). ex_nonz_cap_to' r s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE slot <- lookupSlotForThread t xs;
cap <- withoutFailure $ getSlotCap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x s. \<forall>r\<in>zobj_refs' (fst x). ex_nonz_cap_to' r s\<rbrace>, -
 2. \<And>s. invs' s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma lcs_cte_at' [wp]:
  "\<lbrace>valid_objs'\<rbrace> lookupCapAndSlot t xs \<lbrace>\<lambda>rv s. cte_at' (snd rv) s\<rbrace>,-" unfolding lookupCapAndSlot_def apply (rule hoare_pre) apply (wp|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupCapAndSlot t xs \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) (snd rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> doE slot <- lookupSlotForThread t xs;
cap <- withoutFailure $ getSlotCap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) (snd rv)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE slot <- lookupSlotForThread t xs;
cap <- withoutFailure $ getSlotCap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>_. True) (snd rv)\<rbrace>, -
 2. \<And>s. valid_objs' s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma getSlotCap_eq [wp]:
  "\<lbrace>\<top>\<rbrace> getSlotCap slot
  \<lbrace>\<lambda>cap. cte_wp_at' ((=) cap \<circ> cteCap) slot\<rbrace>" by (wpsimp wp: getCTE_wp' simp: getSlotCap_def cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getSlotCap slot \<lbrace>\<lambda>cap. cte_wp_at' ((=) cap \<circ> cteCap) slot\<rbrace>
theory Syscall_R

lemma lcs_eq [wp]:
  "\<lbrace>\<top>\<rbrace> lookupCapAndSlot t cptr \<lbrace>\<lambda>rv. cte_wp_at' ((=) (fst rv) \<circ> cteCap) (snd rv)\<rbrace>,-" by (wpsimp simp: lookupCapAndSlot_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> lookupCapAndSlot t cptr \<lbrace>\<lambda>rv. cte_wp_at' ((=) (fst rv) \<circ> cteCap) (snd rv)\<rbrace>, -
theory Syscall_R

lemma lec_dimished'[wp]:
  "\<lbrace>\<top>\<rbrace> lookupExtraCaps t buffer info
   \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s)\<rbrace>,-" by (wpsimp wp: mapME_set simp: lookupExtraCaps_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> lookupExtraCaps t buffer info \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' ((=) (fst x) \<circ> cteCap) (snd x) s\<rbrace>, -
theory Syscall_R

lemma lookupExtras_real_ctes[wp]:
  "\<lbrace>valid_objs'\<rbrace> lookupExtraCaps t xs info \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. real_cte_at' (snd x) s\<rbrace>,-" apply (simp add: lookupExtraCaps_def Let_def split del: if_split cong: if_cong) apply (rule hoare_pre) apply (wp mapME_set) apply (simp add: lookupCapAndSlot_def split_def) apply (wp case_options_weak_wp mapM_wp' lsft_real_cte | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupExtraCaps t xs info \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. real_cte_at' (snd x) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> liftE (getExtraCPtrs xs info) >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot t cptr)) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. real_cte_at' (snd x) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> liftE (getExtraCPtrs xs info) >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot t cptr)) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. real_cte_at' (snd x) s\<rbrace>, -
 2. \<And>s. valid_objs' s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> lookupCapAndSlot t x \<lbrace>\<lambda>x. real_cte_at' (snd x)\<rbrace>, -
 2. \<And>cptrs x y. \<lbrace>?B4 cptrs and real_cte_at' (snd x)\<rbrace> capFaultOnFailure y False (lookupCapAndSlot t y) \<lbrace>\<lambda>_. real_cte_at' (snd x)\<rbrace>, -
 3. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> capFaultOnFailure x False (lookupCapAndSlot t x) \<lbrace>\<lambda>_. ?B4 cptrs\<rbrace>, -
 4. \<lbrace>?P'\<rbrace> liftE (getExtraCPtrs xs info) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. valid_objs' s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> doE slot <- lookupSlotForThread t x;
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE \<lbrace>\<lambda>x. real_cte_at' (snd x)\<rbrace>, -
 2. \<And>cptrs x y. \<lbrace>?B4 cptrs and real_cte_at' (snd x)\<rbrace> capFaultOnFailure y False (lookupCapAndSlot t y) \<lbrace>\<lambda>_. real_cte_at' (snd x)\<rbrace>, -
 3. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> capFaultOnFailure x False (lookupCapAndSlot t x) \<lbrace>\<lambda>_. ?B4 cptrs\<rbrace>, -
 4. \<lbrace>?P'\<rbrace> liftE (getExtraCPtrs xs info) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. valid_objs' s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma lookupExtras_ctes[wp]:
  "\<lbrace>valid_objs'\<rbrace> lookupExtraCaps t xs info \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. cte_at' (snd x) s\<rbrace>,-" apply (rule hoare_post_imp_R) apply (rule lookupExtras_real_ctes) apply (simp add: real_cte_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> lookupExtraCaps t xs info \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at' (\<lambda>_. True) (snd x) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_objs'\<rbrace> lookupExtraCaps t xs info \<lbrace>?Q'\<rbrace>, -
 2. \<And>rv s. ?Q' rv s \<Longrightarrow> \<forall>x\<in>set rv. cte_wp_at' (\<lambda>_. True) (snd x) s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<forall>x\<in>set rv. real_cte_at' (snd x) s \<Longrightarrow> \<forall>x\<in>set rv. cte_wp_at' (\<lambda>_. True) (snd x) s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma lsft_ex_cte_cap_to':
  "\<lbrace>invs' and K (\<forall>cap. isCNodeCap cap \<longrightarrow> P cap)\<rbrace>
     lookupSlotForThread t cref
   \<lbrace>\<lambda>rv s. ex_cte_cap_wp_to' P rv s\<rbrace>,-" apply (simp add: lookupSlotForThread_def split_def) apply (wp rab_cte_cap_to' getSlotCap_cap_to2 | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and K (\<forall>cap. isCNodeCap cap \<longrightarrow> P cap)\<rbrace> lookupSlotForThread t cref \<lbrace>ex_cte_cap_wp_to' P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>y. \<forall>cap. isCNodeCap cap \<longrightarrow> P cap)\<rbrace> doE threadRootSlot <- liftE (getThreadCSpaceRoot t);
threadRoot <- liftE (getSlotCap threadRootSlot);
p <- CSpace_H.resolveAddressBits threadRoot cref (size cref);
returnOk (fst p)
odE \<lbrace>ex_cte_cap_wp_to' P\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma lec_caps_to'[wp]:
  "\<lbrace>invs' and K (\<forall>cap. isCNodeCap cap \<longrightarrow> P cap)\<rbrace>
     lookupExtraCaps t buffer info
   \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. ex_cte_cap_wp_to' P (snd x) s)\<rbrace>,-" apply (simp add: lookupExtraCaps_def split del: if_split) apply (rule hoare_pre) apply (wp mapME_set) apply (simp add: lookupCapAndSlot_def split_def) apply (wp lsft_ex_cte_cap_to' mapM_wp'
                    | simp | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and K (\<forall>cap. isCNodeCap cap \<longrightarrow> P cap)\<rbrace> lookupExtraCaps t buffer info \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. ex_cte_cap_wp_to' P (snd x) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>y. \<forall>cap. isCNodeCap cap \<longrightarrow> P cap)\<rbrace> liftE (getExtraCPtrs buffer info) >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot t cptr)) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. ex_cte_cap_wp_to' P (snd x) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> liftE (getExtraCPtrs buffer info) >>=E mapME (\<lambda>cptr. capFaultOnFailure cptr False (lookupCapAndSlot t cptr)) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. ex_cte_cap_wp_to' P (snd x) s\<rbrace>, -
 2. \<And>s. (invs' and (\<lambda>y. \<forall>cap. isCNodeCap cap \<longrightarrow> P cap)) s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> lookupCapAndSlot t x \<lbrace>\<lambda>x. ex_cte_cap_wp_to' P (snd x)\<rbrace>, -
 2. \<And>cptrs x y. \<lbrace>?B4 cptrs and ex_cte_cap_wp_to' P (snd x)\<rbrace> capFaultOnFailure y False (lookupCapAndSlot t y) \<lbrace>\<lambda>_. ex_cte_cap_wp_to' P (snd x)\<rbrace>, -
 3. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> capFaultOnFailure x False (lookupCapAndSlot t x) \<lbrace>\<lambda>_. ?B4 cptrs\<rbrace>, -
 4. \<lbrace>?P'\<rbrace> liftE (getExtraCPtrs buffer info) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. (invs' and (\<lambda>y. \<forall>cap. isCNodeCap cap \<longrightarrow> P cap)) s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> doE slot <- lookupSlotForThread t x;
cap <- liftE (getSlotCap slot);
returnOk (cap, slot)
odE \<lbrace>\<lambda>x. ex_cte_cap_wp_to' P (snd x)\<rbrace>, -
 2. \<And>cptrs x y. \<lbrace>?B4 cptrs and ex_cte_cap_wp_to' P (snd x)\<rbrace> capFaultOnFailure y False (lookupCapAndSlot t y) \<lbrace>\<lambda>_. ex_cte_cap_wp_to' P (snd x)\<rbrace>, -
 3. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> capFaultOnFailure x False (lookupCapAndSlot t x) \<lbrace>\<lambda>_. ?B4 cptrs\<rbrace>, -
 4. \<lbrace>?P'\<rbrace> liftE (getExtraCPtrs buffer info) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. (invs' and (\<lambda>y. \<forall>cap. isCNodeCap cap \<longrightarrow> P cap)) s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma getSlotCap_badge_derived[wp]:
  "\<lbrace>\<top>\<rbrace> getSlotCap p \<lbrace>\<lambda>cap. cte_wp_at' (badge_derived' cap \<circ> cteCap) p\<rbrace>" apply (simp add: getSlotCap_def) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getSlotCap p \<lbrace>\<lambda>cap. cte_wp_at' (badge_derived' cap \<circ> cteCap) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do cte <- getCTE p;
return (cteCap cte)
od \<lbrace>\<lambda>cap. cte_wp_at' (badge_derived' cap \<circ> cteCap) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> cte_wp_at' (badge_derived' (cteCap cte) \<circ> cteCap) p s) proof (prove)
goal:
No subgoals!