theory Syscall_S

lemma lsft_sep:
  "\<lbrace>separate_state and valid_objs\<rbrace> lookup_slot_for_thread tcb cptr \<lbrace>\<lambda>rv s. \<forall>cap. caps_of_state s (fst rv) = Some cap \<longrightarrow> separate_cap cap\<rbrace>, -" unfolding lookup_slot_for_thread_def apply wp apply (rule bisim_validE_R) apply (rule bisim_rab) apply (wpc | wp whenE_throwError_wp)+ apply (fastforce elim: separate_cnode_capE dest: separate_state_get_tcbD objs_valid_tcb_ctable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state and valid_objs\<rbrace> lookup_slot_for_thread tcb cptr \<lbrace>\<lambda>rv s. \<forall>cap. caps_of_state s (fst rv) = Some cap \<longrightarrow> separate_cap cap\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>separate_state and valid_objs\<rbrace> doE tcb <- liftE $ gets_the $ get_tcb tcb;
resolve_address_bits (tcb_ctable tcb, cptr)
odE \<lbrace>\<lambda>rv s. \<forall>cap. caps_of_state s (fst rv) = Some cap \<longrightarrow> separate_cap cap\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> resolve_address_bits (tcb_ctable tcb, cptr) \<lbrace>\<lambda>rv s. \<forall>cap. caps_of_state s (fst rv) = Some cap \<longrightarrow> separate_cap cap\<rbrace>, -
 2. \<lbrace>?P'\<rbrace> liftE $ gets_the $ get_tcb tcb \<lbrace>?B1\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (separate_state and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>tcb. bisim (dc \<oplus> (=)) (?P2 tcb) (?P'2 tcb) (?a2 tcb) (resolve_address_bits (tcb_ctable tcb, cptr))
 2. \<And>tcb. \<lbrace>?Q2 tcb\<rbrace> ?a2 tcb \<lbrace>\<lambda>rv s. \<forall>cap. caps_of_state s (fst rv) = Some cap \<longrightarrow> separate_cap cap\<rbrace>, -
 3. \<lbrace>?P'\<rbrace> liftE $ gets_the $ get_tcb tcb \<lbrace>\<lambda>tcb. ?P2 tcb and ?P'2 tcb and ?Q2 tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. (separate_state and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?Q2 tcb\<rbrace> doE _ <- whenE (length cptr < word_bits) (throwError undefined);
case tcb_ctable tcb of CNodeCap p bits guard \<Rightarrow> if guard \<le> cptr then returnOk ((p, take bits (drop (length guard) cptr)), drop (bits + length guard) cptr) else throwError undefined | _ \<Rightarrow> throwError undefined
odE \<lbrace>\<lambda>rv s. \<forall>cap. caps_of_state s (fst rv) = Some cap \<longrightarrow> separate_cap cap\<rbrace>, -
 2. \<lbrace>?P'\<rbrace> liftE $ gets_the $ get_tcb tcb \<lbrace>\<lambda>tcb. (\<lambda>_. True) and (\<lambda>s. separate_cnode_cap (caps_of_state s) (tcb_ctable tcb) \<and> s \<turnstile> tcb_ctable tcb) and ?Q2 tcb\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. (separate_state and valid_objs) s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. (separate_state and valid_objs) s \<Longrightarrow> True \<and> (get_tcb tcb s \<noteq> None \<longrightarrow> ((\<lambda>_. True) and (\<lambda>sa. separate_cnode_cap (caps_of_state sa) (tcb_ctable (the (get_tcb tcb s))) \<and> sa \<turnstile> tcb_ctable (the (get_tcb tcb s))) and (\<lambda>sa. \<not> length cptr < word_bits \<longrightarrow> (tcb_ctable (the (get_tcb tcb s)) = NullCap \<longrightarrow> True) \<and> (\<forall>x xa xb xc. tcb_ctable (the (get_tcb tcb s)) = UntypedCap x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. tcb_ctable (the (get_tcb tcb s)) = EndpointCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. tcb_ctable (the (get_tcb tcb s)) = NotificationCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. tcb_ctable (the (get_tcb tcb s)) = ReplyCap x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb. tcb_ctable (the (get_tcb tcb s)) = CNodeCap x xa xb \<longrightarrow> (xb \<le> cptr \<longrightarrow> (\<forall>cap. caps_of_state sa (fst ((x, take xa (drop (length xb) cptr)), drop (xa + length xb) cptr)) = Some cap \<longrightarrow> separate_cap cap)) \<and> (\<not> xb \<le> cptr \<longrightarrow> True)) \<and> (\<forall>x. tcb_ctable (the (get_tcb tcb s)) = ThreadCap x \<longrightarrow> True) \<and> (tcb_ctable (the (get_tcb tcb s)) = DomainCap \<longrightarrow> True) \<and> (tcb_ctable (the (get_tcb tcb s)) = IRQControlCap \<longrightarrow> True) \<and> (\<forall>x. tcb_ctable (the (get_tcb tcb s)) = IRQHandlerCap x \<longrightarrow> True) \<and> (\<forall>x xa xb. tcb_ctable (the (get_tcb tcb s)) = Zombie x xa xb \<longrightarrow> True) \<and> (\<forall>x. tcb_ctable (the (get_tcb tcb s)) = ArchObjectCap x \<longrightarrow> True))) s) proof (prove)
goal:
No subgoals!