kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_AI

lemma unbind_notification_not_recursive:
  "\<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace>
     unbind_notification tcb
   \<lbrace>\<lambda>rv s. P (not_recursive_cspaces s)\<rbrace>" apply (simp add: not_recursive_cspaces_def cte_wp_at_caps_of_state) apply (wp unbind_notification_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace> unbind_notification tcb \<lbrace>\<lambda>rv s. P (not_recursive_cspaces s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap}\<rbrace> unbind_notification tcb \<lbrace>\<lambda>rv s. P {ptr. \<exists>cap. caps_of_state s ptr = Some cap \<and> ptr \<notin> fst_cte_ptrs cap}\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma get_cap_det2:
  "(r, s') \<in> fst (get_cap p s) \<Longrightarrow> get_cap p s = ({(r, s)}, False) \<and> s' = s" apply (rule conjI) apply (erule get_cap_det) apply (erule use_valid [OF _ get_cap_inv]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (r, s') \<in> fst (get_cap p s) \<Longrightarrow> get_cap p s = ({(r, s)}, False) \<and> s' = s proof (prove)
goal (2 subgoals):
 1. (r, s') \<in> fst (get_cap p s) \<Longrightarrow> get_cap p s = ({(r, s)}, False)
 2. (r, s') \<in> fst (get_cap p s) \<Longrightarrow> s' = s proof (prove)
goal (1 subgoal):
 1. (r, s') \<in> fst (get_cap p s) \<Longrightarrow> s' = s proof (prove)
goal (1 subgoal):
 1. s = s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma wf_rdcall_finalise_ord_lift:
  "wf S \<Longrightarrow> wf (rdcall_finalise_ord_lift S)" unfolding rdcall_finalise_ord_lift_def by (auto intro!: wf_mlex wf_Un wf_map_prod_image inj_onI)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf S \<Longrightarrow> wf (rdcall_finalise_ord_lift S) proof (prove)
goal (1 subgoal):
 1. wf S \<Longrightarrow> wf ((\<lambda>(x, s). case x of CTEDeleteCall a b \<Rightarrow> 3 | FinaliseSlotCall a b \<Rightarrow> 2 | ReduceZombieCall cap a b \<Rightarrow> 1) <*mlex*> (map_prod (\<lambda>(x, s). (FinaliseSlotCall x True, s)) (\<lambda>(x, s). (FinaliseSlotCall x True, s)) ` S \<union> map_prod (\<lambda>(x, s). (FinaliseSlotCall x False, s)) (\<lambda>(x, s). (FinaliseSlotCall x False, s)) ` S))
theory CNodeInv_AI

lemma rec_del_recset_wf: "wf rec_del_recset" unfolding rec_del_recset_def by (intro wf_sum_wf wf_rdcall_finalise_ord_lift wf_measure
            wf_inv_image wf_lex_prod wf_less_than)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf rec_del_recset proof (prove)
goal (1 subgoal):
 1. wf (wf_sum (exposed_rdcall \<circ> fst) (rdcall_finalise_ord_lift (inv_image (less_than <*lex*> less_than) (\<lambda>(x, s). case caps_of_state s x of None \<Rightarrow> (3, 0) | Some NullCap \<Rightarrow> (0, 0) | Some (Zombie p zb n) \<Rightarrow> (if fst_cte_ptrs (Zombie p zb n) = {x} then 1 else 2, n) | Some _ \<Rightarrow> (3, 0)))) (rdcall_finalise_ord_lift (measure (\<lambda>(x, s). card (not_recursive_cspaces s)))))
theory CNodeInv_AI

lemma in_get_cap_cte_wp_at:
  "(rv, s') \<in> fst (get_cap p s) = (s = s' \<and> cte_wp_at ((=) rv) p s)" apply (rule iffI) apply (clarsimp dest!: get_cap_det2 simp: cte_wp_at_def) apply (clarsimp simp: cte_wp_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((rv, s') \<in> fst (get_cap p s)) = (s = s' \<and> cte_wp_at ((=) rv) p s) proof (prove)
goal (2 subgoals):
 1. (rv, s') \<in> fst (get_cap p s) \<Longrightarrow> s = s' \<and> cte_wp_at ((=) rv) p s
 2. s = s' \<and> cte_wp_at ((=) rv) p s \<Longrightarrow> (rv, s') \<in> fst (get_cap p s) proof (prove)
goal (1 subgoal):
 1. s = s' \<and> cte_wp_at ((=) rv) p s \<Longrightarrow> (rv, s') \<in> fst (get_cap p s) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma fst_cte_ptrs_first_cte_of:
  "fst_cte_ptrs (cap.Zombie ptr zb n) = {first_cslot_of (cap.Zombie ptr zb n)}" by (simp add: fst_cte_ptrs_def tcb_cnode_index_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst_cte_ptrs (Zombie ptr zb n) = {first_cslot_of (Zombie ptr zb n)}
theory CNodeInv_AI

lemma emptyable_irq_state_independent[intro!, simp]:
  "emptyable x (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>)
   = emptyable x s" by (auto simp: emptyable_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. emptyable x (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = emptyable x s
theory CNodeInv_AI

lemma not_recursive_cspaces_irq_state_independent[intro!, simp]:
  "not_recursive_cspaces (s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr>)
   = not_recursive_cspaces s" by (simp add: not_recursive_cspaces_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. not_recursive_cspaces (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) = not_recursive_cspaces s
theory CNodeInv_AI

lemma preemption_point_not_recursive_cspaces[wp]:
  "preemption_point \<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace>" unfolding preemption_point_def by (wpsimp wp: OR_choiceE_weak_wp hoare_drop_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace> preemption_point \<lbrace>\<lambda>_ s. P (not_recursive_cspaces s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (not_recursive_cspaces s)\<rbrace> doE liftE $ do_extended_op update_work_units;
OR_choiceE work_units_limit_reached (doE liftE $ do_extended_op reset_work_units;
irq_opt <- liftE $ do_machine_op (getActiveIRQ True);
case irq_opt of None \<Rightarrow> returnOk () | Some x \<Rightarrow> K (throwError $ ()) x
odE) (returnOk ())
odE \<lbrace>\<lambda>_ s. P (not_recursive_cspaces s)\<rbrace>
theory CNodeInv_AI

lemma preemption_point_caps_of_state[wp]:
  "preemption_point \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>" unfolding preemption_point_def by (wpsimp wp: OR_choiceE_weak_wp hoare_drop_imp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> preemption_point \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> doE liftE $ do_extended_op update_work_units;
OR_choiceE work_units_limit_reached (doE liftE $ do_extended_op reset_work_units;
irq_opt <- liftE $ do_machine_op (getActiveIRQ True);
case irq_opt of None \<Rightarrow> returnOk () | Some x \<Rightarrow> K (throwError $ ()) x
odE) (returnOk ())
odE \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>
theory CNodeInv_AI

lemma rec_del_dom: "\<And> (p :: rec_del_call \<times> 'state_ext state). rec_del_dom p" using rec_del_termination by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p. rec_del_dom p proof (prove)
using this:
All rec_del_dom

goal (1 subgoal):
 1. \<And>p. rec_del_dom p
theory CNodeInv_AI

lemma without_preemption_wp [wp_split]:
  "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> without_preemption f \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> without_preemption f \<lbrace>Q\<rbrace>, \<lbrace>E\<rbrace>
theory CNodeInv_AI

lemma cap_swap_valid_cap:
  "\<lbrace>valid_cap c\<rbrace> cap_swap_for_delete x y \<lbrace>\<lambda>_. valid_cap c\<rbrace>" apply(simp add: cap_swap_for_delete_def) apply(wp cap_swap_valid_cap) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> cap_swap_for_delete x y \<lbrace>\<lambda>_. valid_cap c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> when (x \<noteq> y) (do cap1 <- get_cap x;
cap2 <- get_cap y;
cap_swap cap1 x cap2 y
od) \<lbrace>\<lambda>_. valid_cap c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<turnstile> c \<Longrightarrow> (if x \<noteq> y then valid_cap c else valid_cap c) s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_swap_cte_at:
  "\<lbrace>cte_at p\<rbrace> cap_swap_for_delete x y \<lbrace>\<lambda>_. cte_at p\<rbrace>" apply(simp add: cap_swap_for_delete_def) apply(wp cap_swap_cte_at) apply(simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> cap_swap_for_delete x y \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) p\<rbrace> when (x \<noteq> y) (do cap1 <- get_cap x;
cap2 <- get_cap y;
cap_swap cap1 x cap2 y
od) \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (\<lambda>_. True) p s \<Longrightarrow> (if x \<noteq> y then cte_wp_at (\<lambda>_. True) p else cte_wp_at (\<lambda>_. True) p) s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma rec_del_cte_at:
  "\<And>c call. \<lbrace>cte_at c :: 'state_ext state \<Rightarrow> bool\<rbrace> rec_del call \<lbrace>\<lambda>_. cte_at c\<rbrace>" by (wp valid_cte_at_typ rec_del_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>c call. \<lbrace>cte_wp_at (\<lambda>_. True) c\<rbrace> rec_del call \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) c\<rbrace>
theory CNodeInv_AI

lemma dom_valid_cap[wp]:
  "\<lbrace>valid_cap c\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_cap c\<rbrace>" apply (simp add: do_machine_op_def split_def) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> do_machine_op f \<lbrace>\<lambda>_. valid_cap c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap c\<rbrace> do ms <- gets machine_state;
p <- select_f (f ms);
y <- modify (machine_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_. valid_cap c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<turnstile> c \<Longrightarrow> \<forall>x\<in>fst (f (machine_state s)). s\<lparr>machine_state := snd x\<rparr> \<turnstile> c proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma dom_cte_at:
  "\<lbrace>cte_at c\<rbrace> do_machine_op f \<lbrace>\<lambda>_. cte_at c\<rbrace>" apply (simp add: do_machine_op_def split_def) apply wp apply (simp add: cte_at_cases) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) c\<rbrace> do_machine_op f \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>_. True) c\<rbrace> do ms <- gets machine_state;
p <- select_f (f ms);
y <- modify (machine_state_update (\<lambda>_. snd p));
return (fst p)
od \<lbrace>\<lambda>_. cte_wp_at (\<lambda>_. True) c\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at (\<lambda>_. True) c s \<Longrightarrow> \<forall>x\<in>fst (f (machine_state s)). cte_wp_at (\<lambda>_. True) c (s\<lparr>machine_state := snd x\<rparr>) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cnode_to_zombie_valid:
  "\<lbrakk> s \<turnstile> cap.CNodeCap oref bits guard \<rbrakk>
    \<Longrightarrow> s \<turnstile> cap.Zombie oref (Some bits) (2 ^ bits)" by (clarsimp simp: valid_cap_def cap_table_at_cte_at
                     word_unat_power cap_aligned_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> CNodeCap oref bits guard \<Longrightarrow> s \<turnstile> Zombie oref (Some bits) (2 ^ bits)
theory CNodeInv_AI

lemma tcb_to_zombie_valid:
  "\<lbrakk> s \<turnstile> cap.ThreadCap t \<rbrakk>
    \<Longrightarrow> s \<turnstile> cap.Zombie t None 5" apply (simp add: valid_cap_def) apply (simp add: cap_aligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<turnstile> ThreadCap t \<Longrightarrow> s \<turnstile> Zombie t None 5 proof (prove)
goal (1 subgoal):
 1. cap_aligned (ThreadCap t) \<and> tcb_at t s \<Longrightarrow> cap_aligned (Zombie t None 5) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma set_original_valid_pspace:
  "\<lbrace>valid_pspace\<rbrace> set_original p v \<lbrace>\<lambda>rv. valid_pspace\<rbrace>" apply wp apply (erule valid_pspace_eqI) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pspace\<rbrace> set_original p v \<lbrace>\<lambda>rv. valid_pspace\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pspace s \<Longrightarrow> valid_pspace (s\<lparr>is_original_cap := (is_original_cap s)(p := v)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. kheap s = kheap (s\<lparr>is_original_cap := (is_original_cap s)(p := v)\<rparr>) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma obj_ref_untyped_empty [simp]:
  "obj_refs c \<inter> untyped_range c = {}" by (cases c, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_refs c \<inter> untyped_range c = {}
theory CNodeInv_AI

lemma weak_derived_Reply_eq:
  "\<lbrakk> weak_derived c c'; c = ReplyCap t m R \<rbrakk> \<Longrightarrow> (\<exists> R'. (c' = cap.ReplyCap t m R'))"
  "\<lbrakk> weak_derived c c'; c' = ReplyCap t m R\<rbrakk> \<Longrightarrow> (\<exists> R'. (c = cap.ReplyCap t m R' ))" by (auto simp: weak_derived_def copy_of_def
                 same_object_as_def is_cap_simps
          split: if_split_asm cap.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>weak_derived c c'; c = ReplyCap t m R\<rbrakk> \<Longrightarrow> \<exists>R'. c' = ReplyCap t m R') &&& (\<lbrakk>weak_derived c c'; c' = ReplyCap t m R\<rbrakk> \<Longrightarrow> \<exists>R'. c = ReplyCap t m R')
theory CNodeInv_AI

lemma no_mloop_n:
  "no_mloop n" by (simp add: no_mloop_def parency)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_mloop n
theory CNodeInv_AI

lemma descendants_no_loop [simp]:
  "x \<notin> descendants_of x m" by (simp add: descendants_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> descendants_of x m
theory CNodeInv_AI

lemma untyped_mdb_n:
  "untyped_mdb n cs'" proof - from valid_mdb have "untyped_mdb m cs" by (simp add: cs_def m valid_mdb_def2) thus ?thesis using cap cap' by (simp add: untyped_mdb_def cs'_def descendants_of_def parency
                  s_d_swap_def
             del: split_paired_All) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untyped_mdb n cs' proof (state)
goal (1 subgoal):
 1. untyped_mdb n cs' proof (chain)
picking this:
valid_mdb s proof (prove)
using this:
valid_mdb s

goal (1 subgoal):
 1. untyped_mdb m cs proof (state)
this:
untyped_mdb m cs

goal (1 subgoal):
 1. untyped_mdb n cs' proof (prove)
using this:
untyped_mdb m cs

goal (1 subgoal):
 1. untyped_mdb n cs' proof (prove)
using this:
untyped_mdb m cs
cs src = Some cap
cs dest = Some cap'

goal (1 subgoal):
 1. untyped_mdb n cs' proof (state)
this:
untyped_mdb n cs'

goal:
No subgoals!
theory CNodeInv_AI

lemma reply_mdb_n:
  "reply_mdb n cs'" by (simp add: reply_mdb_def reply_masters_mdb_n reply_caps_mdb_n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reply_mdb n cs'
theory CNodeInv_AI

lemma set_cdt_valid_objs[wp]:
  "\<lbrace>valid_objs\<rbrace> set_cdt m \<lbrace>\<lambda>rv. valid_objs\<rbrace>" by (simp add: set_cdt_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> set_cdt m \<lbrace>\<lambda>rv. valid_objs\<rbrace>
theory CNodeInv_AI

lemma cap_swap_fd_iflive[wp]:
  "\<lbrace>if_live_then_nonz_cap\<rbrace>
     cap_swap_for_delete a b
   \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace>" apply (simp add: cap_swap_for_delete_def) apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_live_then_nonz_cap\<rbrace> when (a \<noteq> b) (do cap1 <- get_cap a;
cap2 <- get_cap b;
cap_swap cap1 a cap2 b
od) \<lbrace>\<lambda>rv. if_live_then_nonz_cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. if_live_then_nonz_cap s \<Longrightarrow> (if a \<noteq> b then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) a s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) b s \<longrightarrow> (if_live_then_nonz_cap and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs cap) a and cte_wp_at (\<lambda>x. zobj_refs x = zobj_refs capa) b) s) else if_live_then_nonz_cap) s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma set_cdt_caps_of[wp]:
  "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" by wp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_cdt m \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
theory CNodeInv_AI

lemma cap_swap_fd_ex_cte_cap[wp]:
  "\<lbrace>ex_cte_cap_wp_to P p\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>" apply (simp add: cap_swap_for_delete_def) apply (wp get_cap_wp) apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P p\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to P p\<rbrace> when (a \<noteq> b) (do cap1 <- get_cap a;
cap2 <- get_cap b;
cap_swap cap1 a cap2 b
od) \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ex_cte_cap_wp_to P p s \<Longrightarrow> (if a \<noteq> b then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) a s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) b s \<longrightarrow> (ex_cte_cap_wp_to P p and cte_wp_at (\<lambda>x. cte_refs x = cte_refs cap \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P cap)) a and cte_wp_at (\<lambda>x. cte_refs x = cte_refs capa \<and> ((\<exists>y. cte_refs x y \<noteq> {}) \<longrightarrow> P x = P capa)) b) s) else ex_cte_cap_wp_to P p) s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_swap_caps_of_state[wp]:
  "\<lbrace>\<lambda>s. P ((caps_of_state s) ( a := Some c', b := Some c ))\<rbrace>
     cap_swap c a c' b
   \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (simp add: cap_swap_def) apply (wp get_cap_wp | simp del: fun_upd_apply split del: if_split)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c))\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((caps_of_state s)(a \<mapsto> c', b \<mapsto> c))\<rbrace> do y <- set_cap c' a;
y <- set_cap c b;
slot1_p <- gets (\<lambda>s. cdt s a);
slot2_p <- gets (\<lambda>s. cdt s b);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>n. if cdt n = Some a then Some b else if cdt n = Some b then Some a else cdt n)(a := if cdt b = Some a then Some b else if cdt b = Some b then Some a else cdt b, b := if cdt a = Some a then Some b else if cdt a = Some b then Some a else cdt a));
y <- do_extended_op (cap_swap_ext a b slot1_p slot2_p);
is_original <- gets is_original_cap;
y <- set_original a (is_original b);
set_original b (is_original a)
od \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_swap_fd_caps_of_state[wp]:
  "\<lbrace>\<lambda>s. P ((caps_of_state s) \<circ> (id ( a := b, b := a )))\<rbrace>
     cap_swap_for_delete a b
   \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (simp add: cap_swap_for_delete_def) apply (wp get_cap_wp) apply (cases "a = b") apply (simp add: fun_upd_def id_def[symmetric] cong: if_cong) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (erule rsubst[where P=P]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s \<circ> id(a := b, b := a))\<rbrace> cap_swap_for_delete a b \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_of_state s \<circ> id(a := b, b := a))\<rbrace> when (a \<noteq> b) (do cap1 <- get_cap a;
cap2 <- get_cap b;
cap_swap cap1 a cap2 b
od) \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (caps_of_state s \<circ> id(a := b, b := a)) \<Longrightarrow> (if a \<noteq> b then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) a s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) b s \<longrightarrow> P ((caps_of_state s)(a \<mapsto> capa, b \<mapsto> cap))) else (\<lambda>s. P (caps_of_state s))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>P (caps_of_state s \<circ> id(a := b, b := a)); a = b\<rbrakk> \<Longrightarrow> (if a \<noteq> b then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) a s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) b s \<longrightarrow> P ((caps_of_state s)(a \<mapsto> capa, b \<mapsto> cap))) else (\<lambda>s. P (caps_of_state s))) s
 2. \<And>s. \<lbrakk>P (caps_of_state s \<circ> id(a := b, b := a)); a \<noteq> b\<rbrakk> \<Longrightarrow> (if a \<noteq> b then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) a s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) b s \<longrightarrow> P ((caps_of_state s)(a \<mapsto> capa, b \<mapsto> cap))) else (\<lambda>s. P (caps_of_state s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P (caps_of_state s \<circ> id(a := b, b := a)); a \<noteq> b\<rbrakk> \<Longrightarrow> (if a \<noteq> b then \<lambda>s. \<forall>cap. cte_wp_at ((=) cap) a s \<longrightarrow> (\<forall>capa. cte_wp_at ((=) capa) b s \<longrightarrow> P ((caps_of_state s)(a \<mapsto> capa, b \<mapsto> cap))) else (\<lambda>s. P (caps_of_state s))) s proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>P (caps_of_state s \<circ> id(a := b, b := a)); a \<noteq> b; caps_of_state s a = Some cap; caps_of_state s b = Some capa\<rbrakk> \<Longrightarrow> P (\<lambda>c. if c = b then Some cap else if c = a then Some capa else caps_of_state s c) proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>a \<noteq> b; caps_of_state s a = Some cap; caps_of_state s b = Some capa\<rbrakk> \<Longrightarrow> caps_of_state s \<circ> id(a := b, b := a) = (\<lambda>c. if c = b then Some cap else if c = a then Some capa else caps_of_state s c) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_irqs_appropriate_strengthen:
  "ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) x s
     \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) x s" by (auto simp: appropriate_cte_cap_def
          elim!: ex_cte_cap_wp_to_weakenE
          split: cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) x s \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) x s