kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_AI

lemma cap_swap_valid_ioc[wp]:
  "\<lbrace>\<lambda>s. valid_ioc s \<and>
    cte_wp_at (weak_derived c) p s \<and>
    cte_wp_at (weak_derived c') p' s\<rbrace>
    cap_swap c p c' p'
   \<lbrace>\<lambda>_ s. valid_ioc s\<rbrace>" apply (simp add: cap_swap_def valid_ioc_def cte_wp_at_caps_of_state) apply (wp set_cdt_cos_ioc set_cap_caps_of_state2 | simp split del: if_split)+ apply (cases p, cases p') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_ioc s \<and> cte_wp_at (weak_derived c) p s \<and> cte_wp_at (weak_derived c') p' s\<rbrace> cap_swap c p c' p' \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap \<noteq> NullCap)) \<and> (\<exists>cap. caps_of_state s p = Some cap \<and> weak_derived c cap) \<and> (\<exists>cap. caps_of_state s p' = Some cap \<and> weak_derived c' cap)\<rbrace> do y <- set_cap c' p;
y <- set_cap c p';
slot1_p <- gets (\<lambda>s. cdt s p);
slot2_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some p then Some p' else if cdt n = Some p' then Some p else cdt n)(p := if cdt p' = Some p then Some p' else if cdt p' = Some p' then Some p else cdt p', p' := if cdt p = Some p then Some p' else if cdt p = Some p' then Some p else cdt p));
y <- do_extended_op (cap_swap_ext p p' slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original p (is_original p');
set_original p' (is_original p)
od \<lbrace>\<lambda>_ s. \<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap \<noteq> NullCap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap \<noteq> NullCap)) \<and> (\<exists>cap. caps_of_state s p = Some cap \<and> weak_derived c cap) \<and> (\<exists>cap. caps_of_state s p' = Some cap \<and> weak_derived c' cap) \<Longrightarrow> \<forall>a b. (if (a, b) = p' then is_original_cap s p else if (a, b) = p then is_original_cap s p' else is_original_cap s (a, b)) \<longrightarrow> (\<exists>cap. (if (a, b) = p' then Some c else if (a, b) = p then Some c' else caps_of_state s (a, b)) = Some cap \<and> cap \<noteq> NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba. \<lbrakk>(\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap \<noteq> NullCap)) \<and> (\<exists>cap. caps_of_state s p = Some cap \<and> weak_derived c cap) \<and> (\<exists>cap. caps_of_state s p' = Some cap \<and> weak_derived c' cap); p = (a, b); p' = (aa, ba)\<rbrakk> \<Longrightarrow> \<forall>a b. (if (a, b) = p' then is_original_cap s p else if (a, b) = p then is_original_cap s p' else is_original_cap s (a, b)) \<longrightarrow> (\<exists>cap. (if (a, b) = p' then Some c else if (a, b) = p then Some c' else caps_of_state s (a, b)) = Some cap \<and> cap \<noteq> NullCap) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_refs_respects_device_region_original_cap[wp]:
  "cap_refs_respects_device_region
                (s\<lparr>is_original_cap := ocp\<rparr>) = cap_refs_respects_device_region s" by (simp add:cap_refs_respects_device_region_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_refs_respects_device_region (s\<lparr>is_original_cap := ocp\<rparr>) = cap_refs_respects_device_region s
theory CNodeInv_AI

lemma final_cap_unchanged:
  assumes x: "\<And>P p. \<lbrace>cte_wp_at P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace>"
  assumes y: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>"
  shows      "\<lbrace>is_final_cap' cap\<rbrace> f \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace>" apply (simp only: is_final_cap'_def3 imp_conv_disj de_Morgan_conj) apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift x hoare_vcg_disj_lift
            valid_cte_at_neg_typ [OF y]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>is_final_cap' cap\<rbrace> f \<lbrace>\<lambda>rv. is_final_cap' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>cref. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref s \<and> (\<forall>cref'. (\<not> cte_wp_at (\<lambda>_. True) cref' s \<or> \<not> cref' \<noteq> cref) \<or> cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c = {}) cref' s)\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c \<noteq> {}) cref s \<and> (\<forall>cref'. (\<not> cte_wp_at (\<lambda>_. True) cref' s \<or> \<not> cref' \<noteq> cref) \<or> cte_wp_at (\<lambda>c. gen_obj_refs cap \<inter> gen_obj_refs c = {}) cref' s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cyclic_zombieD[dest!]:
  "cap_cyclic_zombie cap sl
    \<Longrightarrow> \<exists>p zb n. cap = cap.Zombie p zb n
        \<and> sl = (p, replicate (zombie_cte_bits zb) False)" by (cases cap, simp_all add: cap_cyclic_zombie_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_cyclic_zombie cap sl \<Longrightarrow> \<exists>p zb n. cap = Zombie p zb n \<and> sl = (p, replicate (zombie_cte_bits zb) False)
theory CNodeInv_AI

lemma cap_delete_deletes:
  notes hoare_pre [wp_pre del]
  shows
  "\<And>p.
    \<lbrace>\<top> :: 'state_ext state \<Rightarrow> bool\<rbrace>
      cap_delete p
    \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = cap.NullCap) p\<rbrace>,-" subgoal for p unfolding cap_delete_def using rec_del_delete_cases[where sl=p and ex=True] apply (simp add: validE_R_def) apply wp apply simp done done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p. \<lbrace>\<lambda>_. True\<rbrace> cap_delete p \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) p\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> cap_delete p \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) p\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE rec_del (CTEDeleteCall p True);
returnOk ()
odE \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) p\<rbrace>, - proof (prove)
using this:
\<lbrace>\<lambda>_. True\<rbrace> rec_del (CTEDeleteCall p True) \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap \<or> \<not> True \<and> is_zombie c \<and> p \<in> fst_cte_ptrs c) p\<rbrace>, -

goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE rec_del (CTEDeleteCall p True);
returnOk ()
odE \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) p\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> rec_del (CTEDeleteCall p True) \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> doE y <- rec_del (CTEDeleteCall p True);
returnOk ()
odE \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> rec_del (CTEDeleteCall p True) \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>c. c = NullCap) p\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> rec_del (CTEDeleteCall p True) \<lbrace>\<lambda>y s. True \<and> cte_wp_at (\<lambda>c. c = NullCap) p s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cte_wp_at_weakenE_customised:
  "\<lbrakk>cte_wp_at P t s; \<And>c. \<lbrakk> P c; cte_wp_at ((=) c) t s \<rbrakk> \<Longrightarrow> P' c\<rbrakk> \<Longrightarrow> cte_wp_at P' t s" by (clarsimp simp: cte_wp_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at P t s; \<And>c. \<lbrakk>P c; cte_wp_at ((=) c) t s\<rbrakk> \<Longrightarrow> P' c\<rbrakk> \<Longrightarrow> cte_wp_at P' t s
theory CNodeInv_AI

lemma cap_swap_fd_cte_wp_at_one_case:
  "\<lbrace>\<lambda>s. p \<noteq> p'' \<and> ((p = p') \<longrightarrow> cte_wp_at P p'' s) \<and> ((p \<noteq> p') \<longrightarrow> cte_wp_at P p s)\<rbrace>
     cap_swap_for_delete p' p''
   \<lbrace>\<lambda>rv s. cte_wp_at P p s\<rbrace>" apply (simp add: cte_wp_at_caps_of_state) apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. p \<noteq> p'' \<and> (p = p' \<longrightarrow> cte_wp_at P p'' s) \<and> (p \<noteq> p' \<longrightarrow> cte_wp_at P p s)\<rbrace> cap_swap_for_delete p' p'' \<lbrace>\<lambda>rv. cte_wp_at P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. p \<noteq> p'' \<and> (p = p' \<longrightarrow> (\<exists>cap. caps_of_state s p'' = Some cap \<and> P cap)) \<and> (p \<noteq> p' \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap))\<rbrace> cap_swap_for_delete p' p'' \<lbrace>\<lambda>rv s. \<exists>cap. caps_of_state s p = Some cap \<and> P cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. p \<noteq> p'' \<and> (p = p' \<longrightarrow> (\<exists>cap. caps_of_state s p'' = Some cap \<and> P cap)) \<and> (p \<noteq> p' \<longrightarrow> (\<exists>cap. caps_of_state s p = Some cap \<and> P cap)) \<Longrightarrow> \<exists>cap. (caps_of_state s \<circ> id(p' := p'', p'' := p')) p = Some cap \<and> P cap proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma zombie_has_objrefs:
  "is_zombie c \<Longrightarrow> obj_refs c \<noteq> {}" by (case_tac c, simp_all add: is_zombie_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_zombie c \<Longrightarrow> obj_refs c \<noteq> {}
theory CNodeInv_AI

lemma word_same_bl_memo_unify_word_type:
  "\<lbrakk> of_bl xs = (of_bl ys :: ('a :: len) word); length xs = length ys;
     length xs \<le> len_of TYPE('a) \<rbrakk> \<Longrightarrow> xs = ys" apply (subst same_append_eq[symmetric]) apply (rule word_bl.Abs_eqD) apply (subst of_bl_rep_False)+ apply simp apply simp apply (erule le_add_diff_inverse2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> xs = ys proof (prove)
goal (1 subgoal):
 1. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> ?xs @ xs = ?xs @ ys proof (prove)
goal (3 subgoals):
 1. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> of_bl (?xs @ xs) = of_bl (?xs @ ys)
 2. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> ?xs @ xs \<in> {bl. length bl = LENGTH(?'a1)}
 3. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> ?xs @ ys \<in> {bl. length bl = LENGTH(?'a1)} proof (prove)
goal (3 subgoals):
 1. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> of_bl xs = of_bl ys
 2. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> replicate ?n6 False @ xs \<in> {bl. length bl = LENGTH(?'a1)}
 3. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> replicate ?n6 False @ ys \<in> {bl. length bl = LENGTH(?'a1)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> replicate ?n6 False @ xs \<in> {bl. length bl = LENGTH('a)}
 2. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> replicate ?n6 False @ ys \<in> {bl. length bl = LENGTH('a)} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length ys \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> ?n6 + length ys = LENGTH('a)
 2. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> replicate ?n6 False @ ys \<in> {bl. length bl = LENGTH('a)} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>of_bl xs = of_bl ys; length xs = length ys; length xs \<le> LENGTH('a)\<rbrakk> \<Longrightarrow> replicate (LENGTH('a) - length ys) False @ ys \<in> {bl. length bl = LENGTH('a)} proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma suspend_ex_cte_cap[wp]:
  "\<lbrace>ex_cte_cap_wp_to P p\<rbrace> IpcCancel_A.suspend t \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>" apply (simp add: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state
              del: split_paired_Ex) apply (wp hoare_use_eq_irq_node [OF suspend_irq_node suspend_caps_of_state]) apply (simp del: split_paired_Ex split_paired_All) apply (intro allI impI, erule exEI) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (clarsimp simp: can_fast_finalise_def
                 split: cap.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P p\<rbrace> suspend t \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)\<rbrace> suspend t \<lbrace>\<lambda>rv s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s) \<Longrightarrow> (\<forall>pa. cte_wp_at can_fast_finalise pa s \<longrightarrow> (\<exists>cref cap. ((caps_of_state s)(pa \<mapsto> NullCap)) cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s))) \<and> (\<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>cref cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s) \<Longrightarrow> \<forall>pa. cte_wp_at can_fast_finalise pa s \<longrightarrow> (\<exists>cref. cref \<noteq> pa \<and> (cref \<noteq> pa \<longrightarrow> (\<exists>cap. caps_of_state s cref = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s pa x. \<lbrakk>cte_wp_at can_fast_finalise pa s; \<exists>cap. caps_of_state s x = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> x \<noteq> pa \<and> (x \<noteq> pa \<longrightarrow> (\<exists>cap. caps_of_state s x = Some cap \<and> P cap \<and> p \<in> cte_refs cap (interrupt_irq_node s))) proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap. \<lbrakk>can_fast_finalise cap; caps_of_state s (a, b) = Some cap; P cap; p \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma zombie_is_cap_toE:
  "\<And>ptr zbits n p (s::'state_ext state) m P.
    \<lbrakk> cte_wp_at ((=) (Zombie ptr zbits n)) p s; invs s; m < n; P (Zombie ptr zbits n) \<rbrakk>
      \<Longrightarrow> ex_cte_cap_wp_to P (ptr, nat_to_cref (zombie_cte_bits zbits) m) s" unfolding ex_cte_cap_wp_to_def apply (frule cte_wp_at_valid_objs_valid_cap, clarsimp) apply (intro exI, erule cte_wp_at_weakenE) apply clarsimp apply (drule(2) zombie_is_cap_toE_pre, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ptr zbits n p s m P. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) p s; invs s; m < n; P (Zombie ptr zbits n)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to P (ptr, nat_to_cref (zombie_cte_bits zbits) m) s proof (prove)
goal (1 subgoal):
 1. \<And>ptr zbits n p s m P. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) p s; invs s; m < n; P (Zombie ptr zbits n)\<rbrakk> \<Longrightarrow> \<exists>cref. cte_wp_at (\<lambda>c. P c \<and> (ptr, nat_to_cref (zombie_cte_bits zbits) m) \<in> cte_refs c (interrupt_irq_node s)) cref s proof (prove)
goal (1 subgoal):
 1. \<And>ptr zbits n p s m P. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) p s; invs s; m < n; P (Zombie ptr zbits n); \<exists>cap. Zombie ptr zbits n = cap \<and> s \<turnstile> cap\<rbrakk> \<Longrightarrow> \<exists>cref. cte_wp_at (\<lambda>c. P c \<and> (ptr, nat_to_cref (zombie_cte_bits zbits) m) \<in> cte_refs c (interrupt_irq_node s)) cref s proof (prove)
goal (1 subgoal):
 1. \<And>ptr zbits n p s m P c. \<lbrakk>invs s; m < n; P (Zombie ptr zbits n); \<exists>cap. Zombie ptr zbits n = cap \<and> s \<turnstile> cap; Zombie ptr zbits n = c\<rbrakk> \<Longrightarrow> P c \<and> (ptr, nat_to_cref (zombie_cte_bits zbits) m) \<in> cte_refs c (interrupt_irq_node s) proof (prove)
goal (1 subgoal):
 1. \<And>ptr zbits n s m P. \<lbrakk>invs s; m < n; P (Zombie ptr zbits n); s \<turnstile> Zombie ptr zbits n\<rbrakk> \<Longrightarrow> length (nat_to_cref (zombie_cte_bits zbits) m) = zombie_cte_bits zbits \<and> unat (of_bl (nat_to_cref (zombie_cte_bits zbits) m)) < n proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma zombie_is_cap_toE2:
  "\<lbrakk> cte_wp_at ((=) (cap.Zombie ptr zbits n)) p s; 0 < n;
             P (cap.Zombie ptr zbits n) \<rbrakk>
     \<Longrightarrow> ex_cte_cap_wp_to P (ptr, replicate (zombie_cte_bits zbits) False) s" unfolding ex_cte_cap_wp_to_def apply (rule exI, erule cte_wp_at_weakenE) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) p s; 0 < n; P (Zombie ptr zbits n)\<rbrakk> \<Longrightarrow> ex_cte_cap_wp_to P (ptr, replicate (zombie_cte_bits zbits) False) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at ((=) (Zombie ptr zbits n)) p s; 0 < n; P (Zombie ptr zbits n)\<rbrakk> \<Longrightarrow> \<exists>cref. cte_wp_at (\<lambda>c. P c \<and> (ptr, replicate (zombie_cte_bits zbits) False) \<in> cte_refs c (interrupt_irq_node s)) cref s proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>0 < n; P (Zombie ptr zbits n); Zombie ptr zbits n = c\<rbrakk> \<Longrightarrow> P c \<and> (ptr, replicate (zombie_cte_bits zbits) False) \<in> cte_refs c (interrupt_irq_node s) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma set_cap_emptyable[wp]:
  "\<not> is_master_reply_cap cap \<Longrightarrow>
   \<lbrace>emptyable sl and cte_at p\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. emptyable sl\<rbrace>" apply (simp add: emptyable_def) apply (subst imp_conv_disj)+ apply (wp hoare_vcg_disj_lift set_cap_typ_at set_cap_cte_wp_at
       | simp add: tcb_at_typ)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_master_reply_cap cap \<Longrightarrow> \<lbrace>emptyable sl and cte_wp_at (\<lambda>_. True) p\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. emptyable sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> is_master_reply_cap cap \<Longrightarrow> \<lbrace>(\<lambda>s. tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s) and cte_wp_at (\<lambda>_. True) p\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted (fst sl) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<not> is_master_reply_cap cap \<Longrightarrow> \<lbrace>(\<lambda>s. \<not> (tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2) \<or> st_tcb_at halted (fst sl) s) and cte_wp_at (\<lambda>_. True) p\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<not> (tcb_at (fst sl) s \<and> snd sl = tcb_cnode_index 2) \<or> st_tcb_at halted (fst sl) s\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma set_cap_halted_if_tcb[wp]:
  "\<lbrace>halted_if_tcb t\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. halted_if_tcb t\<rbrace>" apply (simp add: halted_if_tcb_def) apply (subst imp_conv_disj)+ apply (wp hoare_vcg_disj_lift set_cap_typ_at | simp add: tcb_at_typ)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>halted_if_tcb t\<rbrace> set_cap cap p \<lbrace>\<lambda>rv. halted_if_tcb t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at t s \<longrightarrow> st_tcb_at halted t s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. tcb_at t s \<longrightarrow> st_tcb_at halted t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> tcb_at t s \<or> st_tcb_at halted t s\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. \<not> tcb_at t s \<or> st_tcb_at halted t s\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma valid_Zombie_n_less_cte_bits:
  "s \<turnstile> cap.Zombie p zb n \<Longrightarrow> n \<le> 2 ^ zombie_cte_bits zb" by (clarsimp simp: valid_cap_def split: option.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> Zombie p zb n \<Longrightarrow> n \<le> 2 ^ zombie_cte_bits zb
theory CNodeInv_AI

lemma zombie_cte_bits_less:
  "s \<turnstile> cap.Zombie p zb m \<Longrightarrow> zombie_cte_bits zb < word_bits" by (clarsimp simp: valid_cap_def cap_aligned_def
              split: option.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> Zombie p zb m \<Longrightarrow> zombie_cte_bits zb < word_bits
theory CNodeInv_AI

lemma replicate_False_tcb_valid[simp]:
  "tcb_cap_valid cap (p, replicate n False) s" apply (clarsimp simp: tcb_cap_valid_def st_tcb_def2 tcb_at_def) apply (rule conjI) apply (clarsimp split: option.split) apply (frule tcb_cap_cases_length[OF domI]) apply (clarsimp simp add: tcb_cap_cases_def tcb_cnode_index_def to_bl_1) apply (cases n, simp_all add: tcb_cnode_index_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_cap_valid cap (p, replicate n False) s proof (prove)
goal (1 subgoal):
 1. \<And>tcb. get_tcb p s = Some tcb \<Longrightarrow> (case tcb_cap_cases (replicate n False) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst (p, replicate n False)) (tcb_state tcb) cap) \<and> (replicate n False = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) p s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb))) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. get_tcb p s = Some tcb \<Longrightarrow> case tcb_cap_cases (replicate n False) of None \<Rightarrow> True | Some (getF, setF, restr) \<Rightarrow> restr (fst (p, replicate n False)) (tcb_state tcb) cap
 2. \<And>tcb. get_tcb p s = Some tcb \<Longrightarrow> replicate n False = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) p s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>get_tcb p s = Some tcb; tcb_cap_cases (replicate n False) = Some (a, aa, b)\<rbrakk> \<Longrightarrow> b p (tcb_state tcb) cap
 2. \<And>tcb. get_tcb p s = Some tcb \<Longrightarrow> replicate n False = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) p s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)) proof (prove)
goal (2 subgoals):
 1. \<And>tcb a aa b. \<lbrakk>get_tcb p s = Some tcb; tcb_cap_cases (replicate n False) = Some (a, aa, b); length (replicate n False) = 3\<rbrakk> \<Longrightarrow> b p (tcb_state tcb) cap
 2. \<And>tcb. get_tcb p s = Some tcb \<Longrightarrow> replicate n False = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) p s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>tcb. get_tcb p s = Some tcb \<Longrightarrow> replicate n False = tcb_cnode_index 4 \<longrightarrow> (\<forall>tcb. ko_at (TCB tcb) p s \<longrightarrow> valid_ipc_buffer_cap cap (tcb_ipc_buffer tcb)) proof (prove)
goal:
No subgoals!