kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_AI

lemma cap_swap_valid_objs:
  "\<lbrace>valid_objs and valid_cap c and valid_cap c'
        and tcb_cap_valid c' x
        and tcb_cap_valid c y\<rbrace>
  cap_swap c x c' y
  \<lbrace>\<lambda>_. valid_objs\<rbrace>" apply (simp add: cap_swap_def) apply (wp set_cdt_valid_objs set_cap_valid_objs set_cap_valid_cap
         |simp split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap c and valid_cap c' and tcb_cap_valid c' x and tcb_cap_valid c y\<rbrace> cap_swap c x c' y \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and valid_cap c and valid_cap c' and tcb_cap_valid c' x and tcb_cap_valid c y\<rbrace> do ya <- set_cap c' x;
ya <- set_cap c y;
slot1_p <- gets (\<lambda>s. cdt s x);
slot2_p <- gets (\<lambda>s. cdt s y);
cdt <- gets cdt;
ya <- set_cdt ((\<lambda>n. if cdt n = Some x then Some y else if cdt n = Some y then Some x else cdt n)(x := if cdt y = Some x then Some y else if cdt y = Some y then Some x else cdt y, y := if cdt x = Some x then Some y else if cdt x = Some y then Some x else cdt x));
ya <- do_extended_op (cap_swap_ext x y slot1_p slot2_p);
is_original <- gets is_original_cap;
ya <- set_original x (is_original y);
set_original y (is_original x)
od \<lbrace>\<lambda>_. valid_objs\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma lookup_cap_valid:
  "\<lbrace>valid_objs\<rbrace> lookup_cap t c \<lbrace>\<lambda>rv. valid_cap rv\<rbrace>,-" by (simp add: lookup_cap_def split_def) wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> lookup_cap t c \<lbrace>valid_cap\<rbrace>, -
theory CSpace_AI

lemma mask_cap_is_zombie[simp]:
  "is_zombie (mask_cap rs cap) = is_zombie cap" by (cases cap, simp_all add: mask_cap_def cap_rights_update_def is_zombie_def split:bool.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_zombie (mask_cap rs cap) = is_zombie cap
theory CSpace_AI

lemma get_cap_exists[wp]:
  "\<lbrace>\<top>\<rbrace> get_cap sl \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs rv. ex_nonz_cap_to r s\<rbrace>" apply (wp get_cap_wp) apply (cases sl) apply (fastforce simp: ex_nonz_cap_to_def elim!: cte_wp_at_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> get_cap sl \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs rv. ex_nonz_cap_to r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) sl s \<longrightarrow> (\<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s) proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>True; sl = (a, b)\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) sl s \<longrightarrow> (\<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma lookup_cap_ex_cap[wp]:
  "\<lbrace>\<top>\<rbrace> lookup_cap t ref \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs rv. ex_nonz_cap_to r s\<rbrace>,-" apply (simp add: lookup_cap_def split_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> lookup_cap t ref \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs rv. ex_nonz_cap_to r s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE p <- lookup_slot_for_thread t ref;
liftE (get_cap (fst p))
odE \<lbrace>\<lambda>rv s. \<forall>r\<in>zobj_refs rv. ex_nonz_cap_to r s\<rbrace>, - proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma guarded_lookup_valid_cap:
  "\<lbrace>valid_objs\<rbrace> null_cap_on_failure (lookup_cap t c) \<lbrace>\<lambda>rv. valid_cap rv \<rbrace>" apply (simp add: null_cap_on_failure_def) apply wp apply (rule hoare_strengthen_post) apply (rule lookup_cap_valid [unfolded validE_R_def validE_def]) apply (simp split: sum.splits) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> null_cap_on_failure (lookup_cap t c) \<lbrace>valid_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> liftM (case_sum (\<lambda>x. NullCap) id) (lookup_cap t c) \<lbrace>valid_cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> lookup_cap t c \<lbrace>valid_cap \<circ> case_sum (\<lambda>x. NullCap) id\<rbrace>
 2. \<And>s. valid_objs s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?Q\<rbrace> lookup_cap t c \<lbrace>?Q2\<rbrace>
 2. \<And>rv s. ?Q2 rv s \<Longrightarrow> (valid_cap \<circ> case_sum (\<lambda>x. NullCap) id) rv s
 3. \<And>s. valid_objs s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>rv s. case rv of Inl e \<Rightarrow> True | Inr r \<Rightarrow> s \<turnstile> r \<Longrightarrow> (valid_cap \<circ> case_sum (\<lambda>x. NullCap) id) rv s
 2. \<And>s. valid_objs s \<Longrightarrow> valid_objs s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs s \<Longrightarrow> valid_objs s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma lsfco_cte_at[wp]:
  "\<lbrace>invs and valid_cap cap\<rbrace>
     lookup_slot_for_cnode_op bl cap ref depth
   \<lbrace>\<lambda>rv. cte_at rv\<rbrace>,-" apply (simp add: lookup_slot_for_cnode_op_def split_def unlessE_def whenE_def
        split del: if_split cong: if_cong) apply (wp | wpc | simp)+ apply (wp hoare_drop_imps resolve_address_bits_cte_at)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap cap\<rbrace> lookup_slot_for_cnode_op bl cap ref depth \<lbrace>cte_wp_at (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and valid_cap cap\<rbrace> if is_cnode_cap cap then doE y <- if depth = 0 \<or> word_bits < depth then throwError (RangeError 1 (word_of_nat word_bits)) else returnOk ();
lookup_error_on_failure bl (doE p <- resolve_address_bits (cap, drop (length ref - depth) ref);
case snd p of [] \<Rightarrow> returnOk (fst p) | a # list \<Rightarrow> throwError $ DepthMismatch (length (snd p)) 0
odE)
odE else throwError (FailedLookup bl InvalidRoot) \<lbrace>cte_wp_at (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. is_cnode_cap cap \<Longrightarrow> \<lbrace>?P'31 ()\<rbrace> resolve_address_bits (cap, drop (length ref - depth) ref) \<lbrace>\<lambda>p s. snd p = [] \<longrightarrow> cte_wp_at (\<lambda>_. True) (fst p) s\<rbrace>, -
 2. is_cnode_cap cap \<Longrightarrow> \<lbrace>?Qa5\<rbrace> if depth = 0 \<or> word_bits < depth then throwError (RangeError 1 (word_of_nat word_bits)) else returnOk () \<lbrace>\<lambda>y s. True \<and> ?P'31 y s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<not> is_cnode_cap cap \<Longrightarrow> \<lbrace>?R5\<rbrace> throwError (FailedLookup bl InvalidRoot) \<lbrace>cte_wp_at (\<lambda>_. True)\<rbrace>, -
 4. \<And>s. (invs and valid_cap cap) s \<Longrightarrow> (is_cnode_cap cap \<longrightarrow> ?Qa5 s) \<and> (\<not> is_cnode_cap cap \<longrightarrow> ?R5 s) proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and valid_cap cap) s \<Longrightarrow> (is_cnode_cap cap \<longrightarrow> True \<and> True \<and> (depth = 0 \<or> word_bits < depth \<longrightarrow> True) \<and> (\<not> (depth = 0 \<or> word_bits < depth) \<longrightarrow> valid_objs s \<and> s \<turnstile> fst (cap, drop (length ref - depth) ref))) \<and> (\<not> is_cnode_cap cap \<longrightarrow> True) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma ct_from_words_inv [wp]:
  "\<lbrace>P\<rbrace> captransfer_from_words ws \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: captransfer_from_words_def | wp dmo_inv loadWord_inv)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> captransfer_from_words ws \<lbrace>\<lambda>rv. P\<rbrace>
theory CSpace_AI

lemma not_Null_valid_imp [simp]:
  "(cap \<noteq> cap.NullCap \<longrightarrow> s \<turnstile> cap) = (s \<turnstile> cap)" by (auto simp: valid_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cap \<noteq> NullCap \<longrightarrow> s \<turnstile> cap) = s \<turnstile> cap
theory CSpace_AI

lemma enc_inv [wp]:
  "\<lbrace>P\<rbrace> ensure_no_children slot \<lbrace>\<lambda>rv. P\<rbrace>" unfolding ensure_no_children_def whenE_def apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> ensure_no_children slot \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> doE cdt <- liftE $ gets cdt;
if \<exists>c. cdt c = Some slot then throwError RevokeFirst else returnOk ()
odE \<lbrace>\<lambda>rv. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> ((\<exists>c. cdt s c = Some slot) \<longrightarrow> P s \<and> True) \<and> ((\<nexists>c. cdt s c = Some slot) \<longrightarrow> P s) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma badge_update_valid [iff]:
  "valid_cap (badge_update d cap) = valid_cap cap" by (rule ext, cases cap)
     (auto simp: badge_update_def valid_cap_def cap_aligned_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_cap (badge_update d cap) = valid_cap cap
theory CSpace_AI

lemma ensure_empty_inv[wp]:
  "\<lbrace>P\<rbrace> ensure_empty p \<lbrace>\<lambda>rv. P\<rbrace>" by (simp add: ensure_empty_def whenE_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> ensure_empty p \<lbrace>\<lambda>rv. P\<rbrace>
theory CSpace_AI

lemma ensure_empty_stronger:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. c = cap.NullCap) p s \<longrightarrow> P s\<rbrace> ensure_empty p \<lbrace>\<lambda>rv. P\<rbrace>,-" apply (simp add: ensure_empty_def whenE_def) apply wp apply simp apply (simp only: imp_conv_disj) apply (rule hoare_vcg_disj_lift) apply (wp get_cap_cte_wp_at3)+ apply (simp add: pred_neg_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. c = NullCap) p s \<longrightarrow> P s\<rbrace> ensure_empty p \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>c. c = NullCap) p s \<longrightarrow> P s\<rbrace> doE cap <- liftE (get_cap p);
if cap \<noteq> NullCap then throwError DeleteFirst else returnOk ()
odE \<lbrace>\<lambda>rv. P\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> get_cap p \<lbrace>\<lambda>cap s. (cap \<noteq> NullCap \<longrightarrow> True) \<and> (\<not> cap \<noteq> NullCap \<longrightarrow> P s)\<rbrace>
 2. \<And>s. cte_wp_at (\<lambda>c. c = NullCap) p s \<longrightarrow> P s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> get_cap p \<lbrace>\<lambda>cap s. cap = NullCap \<longrightarrow> P s\<rbrace>
 2. \<And>s. cte_wp_at (\<lambda>c. c = NullCap) p s \<longrightarrow> P s \<Longrightarrow> ?P' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> get_cap p \<lbrace>\<lambda>cap s. cap \<noteq> NullCap \<or> P s\<rbrace>
 2. \<And>s. cte_wp_at (\<lambda>c. c = NullCap) p s \<longrightarrow> P s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P8\<rbrace> get_cap p \<lbrace>\<lambda>rv s. rv \<noteq> NullCap\<rbrace>
 2. \<lbrace>?P'8\<rbrace> get_cap p \<lbrace>\<lambda>rv. P\<rbrace>
 3. \<And>s. cte_wp_at (\<lambda>c. c = NullCap) p s \<longrightarrow> P s \<Longrightarrow> ?P8 s \<or> ?P'8 s proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (\<lambda>c. c = NullCap) p s \<longrightarrow> P s \<Longrightarrow> (not cte_wp_at (not (\<lambda>rv. rv \<noteq> NullCap)) p) s \<or> P s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_cdt_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap\<rbrace> set_cdt m \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace>" apply (simp add: set_cdt_def) apply wp apply (clarsimp elim!: ifunsafe_pspaceI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> set_cdt m \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap\<rbrace> do s <- get;
put (s\<lparr>cdt := m\<rparr>)
od \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_unsafe_then_cap s \<Longrightarrow> if_unsafe_then_cap (s\<lparr>cdt := m\<rparr>) proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma set_cdt_ex_cap[wp]:
  "\<lbrace>ex_cte_cap_to p\<rbrace> set_cdt m \<lbrace>\<lambda>rv. ex_cte_cap_to p\<rbrace>" by (wp ex_cte_cap_to_pres set_cdt_cte_wp_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to (\<lambda>_. True) p\<rbrace> set_cdt m \<lbrace>\<lambda>rv. ex_cte_cap_wp_to (\<lambda>_. True) p\<rbrace>
theory CSpace_AI

lemma ex_cte_wp_revokable[simp]:
  "ex_cte_cap_wp_to P p (is_original_cap_update f s)
      = ex_cte_cap_wp_to P p s" by (simp add: ex_cte_cap_wp_to_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to P p (is_original_cap_update f s) = ex_cte_cap_wp_to P p s
theory CSpace_AI

lemma cns_of_heap_typ_at:
  "cns_of_heap (kheap s) p = Some n \<longleftrightarrow> typ_at (ACapTable n) p s" by (auto simp: typ_at_eq_kheap_obj(4) cns_of_heap_def
                 wf_unique wf_cs_n_unique
           split: option.splits Structures_A.kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (cns_of_heap (kheap s) p = Some n) = typ_at (ACapTable n) p s
theory CSpace_AI

lemma ups_of_heap_TCB_upd[simp]:
  "h x = Some (TCB tcb) \<Longrightarrow> ups_of_heap (h(x \<mapsto> TCB y)) = ups_of_heap h" by (erule ups_of_heap_non_arch_upd) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h x = Some (TCB tcb) \<Longrightarrow> ups_of_heap (h(x \<mapsto> TCB y)) = ups_of_heap h
theory CSpace_AI

lemma ups_of_heap_CNode_upd[simp]:
  "h x = Some (CNode sz cs) \<Longrightarrow> ups_of_heap (h(x \<mapsto> CNode sz y)) = ups_of_heap h" by (erule ups_of_heap_non_arch_upd) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h x = Some (CNode sz cs) \<Longrightarrow> ups_of_heap (h(x \<mapsto> CNode sz y)) = ups_of_heap h
theory CSpace_AI

lemma cns_of_heap_TCB_upd[simp]:
  "h x = Some (TCB tcb) \<Longrightarrow> cns_of_heap (h(x \<mapsto> TCB y)) = cns_of_heap h" by (rule ext) (simp add: cns_of_heap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. h x = Some (TCB tcb) \<Longrightarrow> cns_of_heap (h(x \<mapsto> TCB y)) = cns_of_heap h
theory CSpace_AI

lemma cns_of_heap_CNode_upd[simp]:
  "\<lbrakk>h a = Some (CNode sz cs); cs bl = Some cap; well_formed_cnode_n sz cs\<rbrakk>
   \<Longrightarrow> cns_of_heap (h(a \<mapsto> CNode sz (cs(bl \<mapsto> cap')))) = cns_of_heap h" apply (rule ext) apply (auto simp add: cns_of_heap_def wf_unique) apply (clarsimp simp add: well_formed_cnode_n_def dom_def Collect_eq) apply (frule_tac x=bl in spec) apply (erule_tac x=aa in allE) apply (clarsimp split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h a = Some (CNode sz cs); cs bl = Some cap; well_formed_cnode_n sz cs\<rbrakk> \<Longrightarrow> cns_of_heap (h(a \<mapsto> CNode sz (cs(bl \<mapsto> cap')))) = cns_of_heap h proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>h a = Some (CNode sz cs); cs bl = Some cap; well_formed_cnode_n sz cs\<rbrakk> \<Longrightarrow> cns_of_heap (h(a \<mapsto> CNode sz (cs(bl \<mapsto> cap')))) x = cns_of_heap h x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h a = Some (CNode sz cs); cs bl = Some cap; well_formed_cnode_n sz cs; \<not> well_formed_cnode_n sz (cs(bl \<mapsto> cap'))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>h a = Some (CNode sz cs); cs bl = Some cap; \<forall>a. (\<exists>y. cs a = Some y) = (length a = sz); (\<exists>y. (if aa = bl then Some cap' else cs aa) = Some y) = (length aa \<noteq> sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>h a = Some (CNode sz cs); cs bl = Some cap; \<forall>a. (\<exists>y. cs a = Some y) = (length a = sz); (\<exists>y. (if aa = bl then Some cap' else cs aa) = Some y) = (length aa \<noteq> sz); (\<exists>y. cs bl = Some y) = (length bl = sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa. \<lbrakk>h a = Some (CNode sz cs); cs bl = Some cap; (\<exists>y. (if aa = bl then Some cap' else cs aa) = Some y) = (length aa \<noteq> sz); (\<exists>y. cs bl = Some y) = (length bl = sz); (\<exists>y. cs aa = Some y) = (length aa = sz)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma no_reply_caps_for_thread:
  "\<lbrakk> invs s; tcb_at t s; cte_wp_at (\<lambda>c. c = cap.NullCap) (t, tcb_cnode_index 2) s \<rbrakk>
   \<Longrightarrow> \<forall>sl m R. \<not> cte_wp_at (\<lambda>c. c = cap.ReplyCap t m R) sl s" apply clarsimp apply (case_tac m, simp_all) apply (fastforce simp: invs_def valid_state_def valid_reply_masters_def
                          cte_wp_at_caps_of_state is_master_reply_cap_to_def) apply (subgoal_tac "st_tcb_at halted t s") apply (fastforce simp: invs_def valid_state_def valid_reply_caps_def
                          has_reply_cap_def cte_wp_at_caps_of_state st_tcb_def2
                          is_reply_cap_to_def) apply (thin_tac "cte_wp_at _ (a, b) s") apply (fastforce simp: pred_tcb_at_def obj_at_def is_tcb valid_obj_def
                         valid_tcb_def cte_wp_at_cases tcb_cap_cases_def
                   dest: invs_valid_objs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> \<forall>sl m R. \<not> cte_wp_at (\<lambda>c. c = ReplyCap t m R) sl s proof (prove)
goal (1 subgoal):
 1. \<And>a b m R. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 2) s; cte_wp_at (\<lambda>c. c = ReplyCap t m R) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b m R. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 2) s; cte_wp_at (\<lambda>c. c = ReplyCap t True R) (a, b) s; m\<rbrakk> \<Longrightarrow> False
 2. \<And>a b m R. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 2) s; cte_wp_at (\<lambda>c. c = ReplyCap t False R) (a, b) s; \<not> m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b m R. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 2) s; cte_wp_at (\<lambda>c. c = ReplyCap t False R) (a, b) s; \<not> m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b m R. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 2) s; cte_wp_at (\<lambda>c. c = ReplyCap t False R) (a, b) s; \<not> m; st_tcb_at halted t s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b m R. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 2) s; cte_wp_at (\<lambda>c. c = ReplyCap t False R) (a, b) s; \<not> m\<rbrakk> \<Longrightarrow> st_tcb_at halted t s proof (prove)
goal (1 subgoal):
 1. \<And>a b m R. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 2) s; cte_wp_at (\<lambda>c. c = ReplyCap t False R) (a, b) s; \<not> m\<rbrakk> \<Longrightarrow> st_tcb_at halted t s proof (prove)
goal (1 subgoal):
 1. \<And>a b m R. \<lbrakk>invs s; tcb_at t s; cte_wp_at (\<lambda>c. c = NullCap) (t, tcb_cnode_index 2) s; \<not> m\<rbrakk> \<Longrightarrow> st_tcb_at halted t s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma appropriate_cte_cap_def2:
  "appropriate_cte_cap cap cte_cap =
    (cap = NullCap
      \<or> (\<exists> ref badge rights. cap = NotificationCap ref badge rights)
      \<or> (\<forall> irq. cte_cap \<noteq> IRQHandlerCap irq))" by (clarsimp simp: appropriate_cte_cap_def cap_irqs_def cap_irq_opt_def split: cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. appropriate_cte_cap cap cte_cap = (cap = NullCap \<or> (\<exists>ref badge rights. cap = NotificationCap ref badge rights) \<or> (\<forall>irq. cte_cap \<noteq> IRQHandlerCap irq))
theory CSpace_AI

lemma setup_reply_master_ifunsafe[wp]:
  "\<And>t.
    \<lbrace>if_unsafe_then_cap and tcb_at t and ex_nonz_cap_to t and valid_objs\<rbrace>
      setup_reply_master t
    \<lbrace>\<lambda>rv. if_unsafe_then_cap :: 'state_ext state \<Rightarrow> bool\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp new_cap_ifunsafe get_cap_wp) apply (fastforce elim: ex_nonz_tcb_cte_caps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrace>if_unsafe_then_cap and tcb_at t and ex_nonz_cap_to t and valid_objs\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrace>if_unsafe_then_cap and tcb_at t and ex_nonz_cap_to t and valid_objs\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>rv. if_unsafe_then_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t s. (if_unsafe_then_cap and tcb_at t and ex_nonz_cap_to t and valid_objs) s \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) (t, tcb_cnode_index 2) s \<longrightarrow> (if cap = NullCap then \<lambda>s. (cte_wp_at ((=) NullCap) (t, tcb_cnode_index 2) and if_unsafe_then_cap and ex_cte_cap_wp_to (appropriate_cte_cap (ReplyCap t True {AllowGrant, AllowWrite})) (t, tcb_cnode_index 2)) (s\<lparr>is_original_cap := (is_original_cap s)((t, tcb_cnode_index 2) := True)\<rparr>) else if_unsafe_then_cap) s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma setup_reply_master_reply[wp]:
  "\<lbrace>valid_reply_caps and tcb_at t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp hoare_drop_imps | simp add: if_fun_split)+ apply (fastforce elim: tcb_at_cte_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps and tcb_at t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_caps and tcb_at t\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>rv. valid_reply_caps\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_reply_caps s \<and> tcb_at t s \<Longrightarrow> cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s proof (prove)
goal:
No subgoals!
theory CSpace_AI

lemma setup_reply_master_reply_masters[wp]:
  "\<lbrace>valid_reply_masters and tcb_at t\<rbrace>
    setup_reply_master t \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace>" apply (simp add: setup_reply_master_def) apply (wp hoare_drop_imps | simp add: if_fun_split)+ apply (fastforce elim: tcb_at_cte_at) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and tcb_at t\<rbrace> setup_reply_master t \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_reply_masters and tcb_at t\<rbrace> do old_cap <- get_cap (t, tcb_cnode_index 2);
when (old_cap = NullCap) (do y <- set_original (t, tcb_cnode_index 2) True;
set_cap (ReplyCap t True {AllowGrant, AllowWrite}) (t, tcb_cnode_index 2)
od)
od \<lbrace>\<lambda>rv. valid_reply_masters\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_reply_masters s \<and> tcb_at t s \<Longrightarrow> cte_wp_at (\<lambda>_. True) (t, tcb_cnode_index 2) s proof (prove)
goal:
No subgoals!