kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_AI

lemma invs_valid_arch_caps[elim!]:
  "invs s \<Longrightarrow> valid_arch_caps s" by (clarsimp simp: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs s \<Longrightarrow> valid_arch_caps s
theory Syscall_AI

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

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>x s. s \<turnstile> fst x\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> doE (slot, cr) <- lookup_slot_for_thread t xs;
cap <- liftE $ get_cap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x s. s \<turnstile> fst x\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE (slot, cr) <- lookup_slot_for_thread t xs;
cap <- liftE $ get_cap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x s. s \<turnstile> fst x\<rbrace>, -
 2. \<And>s. invs s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma lec_valid_cap [wp]:
  "\<lbrace>invs\<rbrace> lookup_extra_caps t xa mi \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. s \<turnstile> fst x)\<rbrace>, -" unfolding lookup_extra_caps_def by (wpsimp wp: mapME_set)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_extra_caps t xa mi \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. s \<turnstile> fst x\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> (liftE $ get_extra_cptrs xa mi) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot t cptr) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. s \<turnstile> fst x\<rbrace>, -
theory Syscall_AI

lemma lcs_ex_cap_to [wp]:
  "\<lbrace>invs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>x s. \<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_to r s\<rbrace>, -" unfolding lookup_cap_and_slot_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>x s. \<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> doE (slot, cr) <- lookup_slot_for_thread t xs;
cap <- liftE $ get_cap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x s. \<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<rbrace>, -
theory Syscall_AI

lemma lcs_ex_nonz_cap_to [wp]:
  "\<lbrace>invs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>x s. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s\<rbrace>, -" unfolding lookup_cap_and_slot_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_cap_and_slot 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, cr) <- lookup_slot_for_thread t xs;
cap <- liftE $ get_cap slot;
returnOk (cap, slot)
odE \<lbrace>\<lambda>x s. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s\<rbrace>, -
theory Syscall_AI

lemma lcs_cte_at[wp]:
  "\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>rv. cte_at (snd rv)\<rbrace>,-" apply (simp add: lookup_cap_and_slot_def split_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) (snd rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> doE p <- lookup_slot_for_thread t xs;
cap <- liftE (get_cap (fst p));
returnOk (cap, fst p)
odE \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>_. True) (snd rv)\<rbrace>, - proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma lcs_real_cte_at[wp]:
  "\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>rv. real_cte_at (snd rv)\<rbrace>,-" by (wpsimp simp: lookup_cap_and_slot_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_cap_and_slot t xs \<lbrace>\<lambda>rv. real_cte_at (snd rv)\<rbrace>, -
theory Syscall_AI

lemma lec_ex_cap_to [wp]:
  "\<lbrace>invs\<rbrace>
  lookup_extra_caps t xa mi
  \<lbrace>\<lambda>rv s. (\<forall>cap \<in> set rv. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_to r s)\<rbrace>, -" unfolding lookup_extra_caps_def by (wp mapME_set | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_extra_caps t xa mi \<lbrace>\<lambda>rv s. \<forall>cap\<in>set rv. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> (liftE $ get_extra_cptrs xa mi) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot t cptr) \<lbrace>\<lambda>rv s. \<forall>cap\<in>set rv. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_wp_to (\<lambda>_. True) r s\<rbrace>, -
theory Syscall_AI

lemma lec_ex_nonz_cap_to [wp]:
  "\<lbrace>invs\<rbrace>
  lookup_extra_caps t xa mi
  \<lbrace>\<lambda>rv s. (\<forall>cap \<in> set rv. \<forall>r\<in>zobj_refs (fst cap). ex_nonz_cap_to r s)\<rbrace>, -" unfolding lookup_extra_caps_def by (wp mapME_set | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_extra_caps t xa mi \<lbrace>\<lambda>rv s. \<forall>cap\<in>set rv. \<forall>r\<in>zobj_refs (fst cap). ex_nonz_cap_to r s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> (liftE $ get_extra_cptrs xa mi) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False $ lookup_cap_and_slot t cptr) \<lbrace>\<lambda>rv s. \<forall>cap\<in>set rv. \<forall>r\<in>zobj_refs (fst cap). ex_nonz_cap_to r s\<rbrace>, -
theory Syscall_AI

lemma lookup_extras_real_ctes[wp]:
  "\<lbrace>valid_objs\<rbrace> lookup_extra_caps t xs info \<lbrace>\<lambda>rv s. \<forall>x \<in> set rv. real_cte_at (snd x) s\<rbrace>,-" apply (simp add: lookup_extra_caps_def
              split del: if_split) apply (rule hoare_pre) apply (wp mapME_set) apply (simp add: lookup_cap_and_slot_def split_def) apply (wp case_options_weak_wp mapM_wp'
                 | simp add: load_word_offs_word_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_extra_caps 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 (get_extra_cptrs xs info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot 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 (get_extra_cptrs xs info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot 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 (4 subgoals):
 1. \<And>cptrs x y. \<lbrace>valid_objs and real_cte_at (snd x)\<rbrace> lookup_cap_and_slot t y \<lbrace>\<lambda>_. real_cte_at (snd x)\<rbrace>, -
 2. \<And>cptrs x. \<lbrace>valid_objs\<rbrace> cap_fault_on_failure (of_bl x) False (lookup_cap_and_slot t x) \<lbrace>\<lambda>_. valid_objs\<rbrace>, -
 3. \<lbrace>?P'\<rbrace> liftE (get_extra_cptrs xs info) \<lbrace>\<lambda>cptrs. valid_objs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrace>valid_objs and real_cte_at (snd x)\<rbrace> doE p <- lookup_slot_for_thread t y;
cap <- liftE (get_cap (fst p));
returnOk (cap, fst p)
odE \<lbrace>\<lambda>_. real_cte_at (snd x)\<rbrace>, -
 2. \<And>cptrs x. \<lbrace>valid_objs\<rbrace> cap_fault_on_failure (of_bl x) False (lookup_cap_and_slot t x) \<lbrace>\<lambda>_. valid_objs\<rbrace>, -
 3. \<lbrace>?P'\<rbrace> liftE (get_extra_cptrs xs info) \<lbrace>\<lambda>cptrs. valid_objs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. valid_objs s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma mapME_wp:
  assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> f x \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>"
  shows      "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>" apply (induct xs) apply (simp add: mapME_def sequenceE_def) apply wp apply (simp add: mapME_Cons) apply (wpsimp wp: x|assumption)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. set [] \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f [] \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>P\<rbrace> returnOk [] \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>
 2. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>; set (a # xs) \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> mapME f (a # xs) \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a xs. \<lbrakk>\<lbrace>P\<rbrace> mapME f xs \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace>; a \<in> S \<and> set xs \<subseteq> S\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> doE y <- f a;
ys <- mapME f xs;
returnOk (y # ys)
odE \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>E\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma resolve_address_bits_valid_fault2:
  "\<lbrace>invs and valid_cap (fst param)\<rbrace>
   resolve_address_bits param
   -,\<lbrace>\<lambda>f s. valid_fault (ExceptionTypes_A.fault.CapFault x y f)\<rbrace>" apply (cut_tac resolve_address_bits_valid_fault[of param x y]) apply (clarsimp simp add: validE_E_def validE_def valid_def
                  split: sum.splits) apply (drule invs_valid_objs) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap (fst param)\<rbrace> resolve_address_bits param -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap (fst param)\<rbrace> resolve_address_bits param \<lbrace>\<lambda>_. valid_objs\<rbrace>, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace> \<Longrightarrow> \<lbrace>invs and valid_cap (fst param)\<rbrace> resolve_address_bits param -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b x1. \<lbrakk>\<forall>s. valid_objs s \<and> s \<turnstile> fst param \<longrightarrow> (\<forall>xa\<in>fst (resolve_address_bits param s). case xa of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> valid_fault (CapFault x y x1)) \<and> ((\<forall>a b ba. r \<noteq> Inr ((a, b), ba)) \<or> valid_objs s')); (Inl x1, b) \<in> fst (resolve_address_bits param s); invs s; s \<turnstile> fst param\<rbrakk> \<Longrightarrow> valid_fault (CapFault x y x1) proof (prove)
goal (1 subgoal):
 1. \<And>s b x1. \<lbrakk>\<forall>s. valid_objs s \<and> s \<turnstile> fst param \<longrightarrow> (\<forall>xa\<in>fst (resolve_address_bits param s). case xa of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> valid_fault (CapFault x y x1)) \<and> ((\<forall>a b ba. r \<noteq> Inr ((a, b), ba)) \<or> valid_objs s')); (Inl x1, b) \<in> fst (resolve_address_bits param s); s \<turnstile> fst param; valid_objs s\<rbrakk> \<Longrightarrow> valid_fault (CapFault x y x1) proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma lookup_cap_and_slot_valid_fault:
  "\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread cptr
   \<lbrace>\<lambda>_. valid_objs\<rbrace>,
   \<lbrace>\<lambda>ft s. valid_fault (ExceptionTypes_A.CapFault (of_bl cptr) rp ft)\<rbrace>" apply (simp add: lookup_cap_and_slot_def split_def lookup_slot_for_thread_def
         | wp resolve_address_bits_valid_fault)+ apply (clarsimp simp: objs_valid_tcb_ctable) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread cptr \<lbrace>\<lambda>_. valid_objs\<rbrace>, \<lbrace>\<lambda>ft s. valid_fault (CapFault (of_bl cptr) rp ft)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> (\<exists>y. get_tcb thread s = Some y) \<longrightarrow> s \<turnstile> tcb_ctable (the (get_tcb thread s)) proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma lookup_cap_and_slot_valid_fault2[wp]:
  "\<lbrace>invs\<rbrace> lookup_cap_and_slot thread (to_bl p)
   -,\<lbrace>\<lambda>ft s. valid_fault (ExceptionTypes_A.CapFault p rp ft)\<rbrace>" using lookup_cap_and_slot_valid_fault[of thread "to_bl p"] apply (clarsimp simp add: validE_E_def validE_def valid_def
                  split: sum.splits) apply (drule invs_valid_objs) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_cap_and_slot thread (to_bl p) -, \<lbrace>\<lambda>ft s. valid_fault (CapFault p rp ft)\<rbrace> proof (prove)
using this:
\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread (to_bl p) \<lbrace>\<lambda>_. valid_objs\<rbrace>, \<lbrace>\<lambda>ft s. valid_fault (CapFault (of_bl (to_bl p)) ?rp ft)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_cap_and_slot thread (to_bl p) -, \<lbrace>\<lambda>ft s. valid_fault (CapFault p rp ft)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b x1. \<lbrakk>\<And>rp. \<forall>s. valid_objs s \<longrightarrow> (\<forall>x\<in>fst (lookup_cap_and_slot thread (to_bl p) s). case x of (Inl e, s') \<Rightarrow> valid_fault (CapFault p rp e) | (Inr ra, s') \<Rightarrow> valid_objs s'); invs s; (Inl x1, b) \<in> fst (lookup_cap_and_slot thread (to_bl p) s)\<rbrakk> \<Longrightarrow> valid_fault (CapFault p rp x1) proof (prove)
goal (1 subgoal):
 1. \<And>s b x1. \<lbrakk>\<And>rp. \<forall>s. valid_objs s \<longrightarrow> (\<forall>x\<in>fst (lookup_cap_and_slot thread (to_bl p) s). case x of (Inl e, s') \<Rightarrow> valid_fault (CapFault p rp e) | (Inr ra, s') \<Rightarrow> valid_objs s'); (Inl x1, b) \<in> fst (lookup_cap_and_slot thread (to_bl p) s); valid_objs s\<rbrakk> \<Longrightarrow> valid_fault (CapFault p rp x1) proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma lec_valid_fault2[wp]:
  "\<lbrace>invs\<rbrace> lookup_extra_caps thread buffer info -,\<lbrace>\<lambda>rv s. valid_fault rv\<rbrace>" apply (cut_tac lec_valid_fault[of thread buffer info]) apply (clarsimp simp add: validE_E_def validE_def valid_def
                  split: sum.splits ) apply (drule invs_valid_objs) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_extra_caps thread buffer info -, \<lbrace>\<lambda>rv s. valid_fault rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_extra_caps thread buffer info \<lbrace>\<lambda>_. valid_objs\<rbrace>, \<lbrace>\<lambda>rv s. valid_fault rv\<rbrace> \<Longrightarrow> \<lbrace>invs\<rbrace> lookup_extra_caps thread buffer info -, \<lbrace>\<lambda>rv s. valid_fault rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s b x1. \<lbrakk>\<forall>s. valid_objs s \<longrightarrow> (\<forall>x\<in>fst (lookup_extra_caps thread buffer info s). case x of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> valid_fault x1) \<and> ((\<exists>x2. r = Inl x2) \<or> valid_objs s')); invs s; (Inl x1, b) \<in> fst (lookup_extra_caps thread buffer info s)\<rbrakk> \<Longrightarrow> valid_fault x1 proof (prove)
goal (1 subgoal):
 1. \<And>s b x1. \<lbrakk>\<forall>s. valid_objs s \<longrightarrow> (\<forall>x\<in>fst (lookup_extra_caps thread buffer info s). case x of (r, s') \<Rightarrow> (\<forall>x1. r = Inl x1 \<longrightarrow> valid_fault x1) \<and> ((\<exists>x2. r = Inl x2) \<or> valid_objs s')); (Inl x1, b) \<in> fst (lookup_extra_caps thread buffer info s); valid_objs s\<rbrakk> \<Longrightarrow> valid_fault x1 proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma lec_caps_to[wp]:
  "\<lbrace>invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> lookup_extra_caps 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: lookup_extra_caps_def split del: if_split) apply (rule hoare_pre) apply (wp mapME_set) apply (simp add: lookup_cap_and_slot_def split_def) apply (wp lsft_ex_cte_cap_to mapM_wp'
                    | simp add: load_word_offs_word_def | wpc)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (\<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> lookup_extra_caps 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. is_cnode_cap cap \<longrightarrow> P cap)\<rbrace> liftE (get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot 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 (get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot 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. is_cnode_cap cap \<longrightarrow> P cap)) s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> lookup_cap_and_slot 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> cap_fault_on_failure (of_bl y) False (lookup_cap_and_slot t y) \<lbrace>\<lambda>_. ex_cte_cap_wp_to P (snd x)\<rbrace>, -
 3. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> cap_fault_on_failure (of_bl x) False (lookup_cap_and_slot t x) \<lbrace>\<lambda>_. ?B4 cptrs\<rbrace>, -
 4. \<lbrace>?P'\<rbrace> liftE (get_extra_cptrs buffer info) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. (invs and (\<lambda>y. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)) s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> doE p <- lookup_slot_for_thread t x;
cap <- liftE (get_cap (fst p));
returnOk (cap, fst p)
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> cap_fault_on_failure (of_bl y) False (lookup_cap_and_slot t y) \<lbrace>\<lambda>_. ex_cte_cap_wp_to P (snd x)\<rbrace>, -
 3. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> cap_fault_on_failure (of_bl x) False (lookup_cap_and_slot t x) \<lbrace>\<lambda>_. ?B4 cptrs\<rbrace>, -
 4. \<lbrace>?P'\<rbrace> liftE (get_extra_cptrs buffer info) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. (invs and (\<lambda>y. \<forall>cap. is_cnode_cap cap \<longrightarrow> P cap)) s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma get_cap_int_derived[wp]:
  "\<lbrace>\<top>\<rbrace> get_cap slot \<lbrace>\<lambda>rv. cte_wp_at (interrupt_derived rv) slot\<rbrace>" apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state interrupt_derived_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_cap slot \<lbrace>\<lambda>rv. cte_wp_at (interrupt_derived rv) slot\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cte_wp_at (interrupt_derived cap) slot s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma lec_derived[wp]:
  "\<lbrace>invs\<rbrace>
     lookup_extra_caps t buffer info
   \<lbrace>\<lambda>rv s. (\<forall>x\<in>set rv. cte_wp_at (interrupt_derived (fst x)) (snd x) s)\<rbrace>,-" apply (simp add: lookup_extra_caps_def split del: if_split) apply (rule hoare_pre) apply (wp mapME_set) apply (simp add: lookup_cap_and_slot_def split_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> lookup_extra_caps t buffer info \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (interrupt_derived (fst x)) (snd x) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> liftE (get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot t cptr)) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (interrupt_derived (fst x)) (snd x) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> liftE (get_extra_cptrs buffer info) >>=E mapME (\<lambda>cptr. cap_fault_on_failure (of_bl cptr) False (lookup_cap_and_slot t cptr)) \<lbrace>\<lambda>rv s. \<forall>x\<in>set rv. cte_wp_at (interrupt_derived (fst x)) (snd x) s\<rbrace>, -
 2. \<And>s. invs s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> lookup_cap_and_slot t x \<lbrace>\<lambda>x. cte_wp_at (interrupt_derived (fst x)) (snd x)\<rbrace>, -
 2. \<And>cptrs x y. \<lbrace>?B4 cptrs and cte_wp_at (interrupt_derived (fst x)) (snd x)\<rbrace> cap_fault_on_failure (of_bl y) False (lookup_cap_and_slot t y) \<lbrace>\<lambda>_. cte_wp_at (interrupt_derived (fst x)) (snd x)\<rbrace>, -
 3. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> cap_fault_on_failure (of_bl x) False (lookup_cap_and_slot t x) \<lbrace>\<lambda>_. ?B4 cptrs\<rbrace>, -
 4. \<lbrace>?P'\<rbrace> liftE (get_extra_cptrs buffer info) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. invs s \<Longrightarrow> ?P' s proof (prove)
goal (5 subgoals):
 1. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> doE p <- lookup_slot_for_thread t x;
cap <- liftE (get_cap (fst p));
returnOk (cap, fst p)
odE \<lbrace>\<lambda>x. cte_wp_at (interrupt_derived (fst x)) (snd x)\<rbrace>, -
 2. \<And>cptrs x y. \<lbrace>?B4 cptrs and cte_wp_at (interrupt_derived (fst x)) (snd x)\<rbrace> cap_fault_on_failure (of_bl y) False (lookup_cap_and_slot t y) \<lbrace>\<lambda>_. cte_wp_at (interrupt_derived (fst x)) (snd x)\<rbrace>, -
 3. \<And>cptrs x. \<lbrace>?B4 cptrs\<rbrace> cap_fault_on_failure (of_bl x) False (lookup_cap_and_slot t x) \<lbrace>\<lambda>_. ?B4 cptrs\<rbrace>, -
 4. \<lbrace>?P'\<rbrace> liftE (get_extra_cptrs buffer info) \<lbrace>?B4\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. invs s \<Longrightarrow> ?P' s proof (prove)
goal:
No subgoals!
theory Syscall_AI

lemma lookup_cap_and_slot_dimished [wp]:
  "\<lbrace>valid_objs\<rbrace>
    lookup_cap_and_slot thread cptr
   \<lbrace>\<lambda>x. cte_wp_at ((=) (fst x)) (snd x)\<rbrace>, -" by (wpsimp wp: get_cap_wp simp: lookup_cap_and_slot_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread cptr \<lbrace>\<lambda>x. cte_wp_at ((=) (fst x)) (snd x)\<rbrace>, -