kings-crown/FVELER_Isabelle huggingface dataset:
theory CNodeInv_AI

lemma cap_delete_rvk_prog:
  "\<And>m ptr.
    \<lbrace>\<lambda>s::'state_ext state. revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s)\<rbrace>
      cap_delete ptr
    \<lbrace>\<lambda>rv s. revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s)\<rbrace>,-" unfolding cap_delete_def validE_R_def apply wpsimp apply (unfold validE_R_def) apply (rule use_spec) apply (rule rec_del_rvk_prog rec_del_rvk_prog[unfolded o_def]) apply (simp add: o_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>m ptr. \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> cap_delete ptr \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>m ptr. \<lbrace>\<lambda>s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace> doE rec_del (CTEDeleteCall ptr True);
returnOk ()
odE \<lbrace>\<lambda>rv s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>m a b. \<lbrace>?P'22 a b m (a, b)\<rbrace> rec_del (CTEDeleteCall (a, b) True) \<lbrace>\<lambda>x3 x4. revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state x4 a))\<rbrace>, -
 2. \<And>m ptr s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> True \<and> True \<and> ?P'22 (fst ptr) (snd ptr) m ptr s proof (prove)
goal (2 subgoals):
 1. \<And>m a b. \<lbrace>?P'22 a b m (a, b)\<rbrace> rec_del (CTEDeleteCall (a, b) True) \<lbrace>\<lambda>x3 x4. revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state x4 a))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>m ptr s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> True \<and> True \<and> ?P'22 (fst ptr) (snd ptr) m ptr s proof (prove)
goal (2 subgoals):
 1. \<And>m a b s. s \<turnstile> \<lbrace>?P'25 m a b (a, b)\<rbrace> rec_del (CTEDeleteCall (a, b) True) \<lbrace>\<lambda>x3 x4. revoke_progress_ord m (\<lambda>a. map_option cap_to_rpo (caps_of_state x4 a))\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>m ptr s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> True \<and> True \<and> ?P'25 m (fst ptr) (snd ptr) ptr s proof (prove)
goal (1 subgoal):
 1. \<And>m ptr s. revoke_progress_ord m (map_option cap_to_rpo \<circ> caps_of_state s) \<Longrightarrow> True \<and> True \<and> revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x)) \<and> (case CTEDeleteCall ptr True of ReduceZombieCall cap sl ex \<Rightarrow> cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s | _ \<Rightarrow> True) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma get_object_some: "kheap s ptr = Some ko \<Longrightarrow> get_object ptr s = ({(ko, s)}, False)" by (clarsimp simp: get_object_def gets_def get_def bind_def assert_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s ptr = Some ko \<Longrightarrow> get_object ptr s = ({(ko, s)}, False)
theory CNodeInv_AI

lemma get_cap_fail_or_not:
  "fst (get_cap slot s) \<noteq> {} \<Longrightarrow> snd (get_cap slot s) = False" by (clarsimp elim!: nonemptyE dest!: get_cap_det)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (get_cap slot s) \<noteq> {} \<Longrightarrow> snd (get_cap slot s) = False
theory CNodeInv_AI

lemma set_cap_cap_somewhere:
  "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cp. P (fst slot) (snd slot) cp \<longrightarrow> P (fst slot) (snd slot) cap) slot s
         \<and> (\<exists>oref cref. cte_wp_at (P oref cref) (oref, cref) s)\<rbrace>
     set_cap cap slot
   \<lbrace>\<lambda>rv s. \<exists>oref cref. cte_wp_at (P oref cref) (oref, cref) s\<rbrace>" apply (simp add: cte_wp_at_caps_of_state) apply wp apply clarsimp apply (rule_tac x=oref in exI) apply (rule_tac x=cref in exI) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at (\<lambda>cp. P (fst slot) (snd slot) cp \<longrightarrow> P (fst slot) (snd slot) cap) slot s \<and> (\<exists>oref cref. cte_wp_at (P oref cref) (oref, cref) s)\<rbrace> set_cap cap slot \<lbrace>\<lambda>rv s. \<exists>oref cref. cte_wp_at (P oref cref) (oref, cref) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>capa. caps_of_state s slot = Some capa \<and> (P (fst slot) (snd slot) capa \<longrightarrow> P (fst slot) (snd slot) cap)) \<and> (\<exists>oref cref cap. caps_of_state s (oref, cref) = Some cap \<and> P oref cref cap)\<rbrace> set_cap cap slot \<lbrace>\<lambda>rv s. \<exists>oref cref cap. caps_of_state s (oref, cref) = Some cap \<and> P oref cref cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>capa. caps_of_state s slot = Some capa \<and> (P (fst slot) (snd slot) capa \<longrightarrow> P (fst slot) (snd slot) cap)) \<and> (\<exists>oref cref cap. caps_of_state s (oref, cref) = Some cap \<and> P oref cref cap) \<Longrightarrow> \<exists>oref cref capa. ((caps_of_state s)(slot \<mapsto> cap)) (oref, cref) = Some capa \<and> P oref cref capa proof (prove)
goal (1 subgoal):
 1. \<And>s capa oref cref capaa. \<lbrakk>caps_of_state s slot = Some capa; P (fst slot) (snd slot) capa \<longrightarrow> P (fst slot) (snd slot) cap; caps_of_state s (oref, cref) = Some capaa; P oref cref capaa\<rbrakk> \<Longrightarrow> \<exists>oref cref. ((oref, cref) = slot \<longrightarrow> P oref cref cap) \<and> ((oref, cref) \<noteq> slot \<longrightarrow> (\<exists>cap. caps_of_state s (oref, cref) = Some cap \<and> P oref cref cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa oref cref capaa. \<lbrakk>caps_of_state s slot = Some capa; P (fst slot) (snd slot) capa \<longrightarrow> P (fst slot) (snd slot) cap; caps_of_state s (oref, cref) = Some capaa; P oref cref capaa\<rbrakk> \<Longrightarrow> \<exists>cref. ((oref, cref) = slot \<longrightarrow> P oref cref cap) \<and> ((oref, cref) \<noteq> slot \<longrightarrow> (\<exists>cap. caps_of_state s (oref, cref) = Some cap \<and> P oref cref cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s capa oref cref capaa. \<lbrakk>caps_of_state s slot = Some capa; P (fst slot) (snd slot) capa \<longrightarrow> P (fst slot) (snd slot) cap; caps_of_state s (oref, cref) = Some capaa; P oref cref capaa\<rbrakk> \<Longrightarrow> ((oref, cref) = slot \<longrightarrow> P oref cref cap) \<and> ((oref, cref) \<noteq> slot \<longrightarrow> (\<exists>cap. caps_of_state s (oref, cref) = Some cap \<and> P oref cref cap)) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma rec_del_ReduceZombie_emptyable:
  "\<And>cap slot ex.
    \<lbrace>invs and (cte_wp_at ((=) cap) slot and is_final_cap' cap
          and (\<lambda>y. is_zombie cap))
          and (\<lambda>s. \<not> ex \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s)
          and emptyable slot
          and (\<lambda>s. \<not> cap_removeable cap slot \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s))\<rbrace>
      rec_del (ReduceZombieCall cap slot ex)
    \<lbrace>\<lambda>rv. emptyable slot :: 'state_ext state \<Rightarrow> bool\<rbrace>, -" subgoal for cap slot ex by (rule rec_del_emptyable [where args="ReduceZombieCall cap slot ex", simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>cap slot ex. \<lbrace>invs and (cte_wp_at ((=) cap) slot and is_final_cap' cap and (\<lambda>y. is_zombie cap)) and (\<lambda>s. \<not> ex \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and emptyable slot and (\<lambda>s. \<not> cap_removeable cap slot \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s))\<rbrace> rec_del (ReduceZombieCall cap slot ex) \<lbrace>\<lambda>rv. emptyable slot\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (cte_wp_at ((=) cap) slot and is_final_cap' cap and (\<lambda>y. is_zombie cap)) and (\<lambda>s. \<not> ex \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) slot s) and emptyable slot and (\<lambda>s. \<not> cap_removeable cap slot \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s))\<rbrace> rec_del (ReduceZombieCall cap slot ex) \<lbrace>\<lambda>rv. emptyable slot\<rbrace>, - proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma wf_cap_revoke_recset:
  "wf cap_revoke_recset" by (simp add: cap_revoke_recset_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wf cap_revoke_recset
theory CNodeInv_AI

lemma in_select_ext_weak: "(a,b) \<in> fst (select_ext f S s)  \<Longrightarrow>
       (a,b) \<in> fst (select S s)" apply (drule_tac Q="\<lambda>r s'. r \<in> S \<and> s' =s" in  use_valid[OF _ select_ext_weak_wp]) apply (simp add: select_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, b) \<in> fst (select_ext f S s) \<Longrightarrow> (a, b) \<in> fst (select S s) proof (prove)
goal (2 subgoals):
 1. \<forall>x\<in>S. x \<in> S \<and> s = s
 2. a \<in> S \<and> b = s \<Longrightarrow> (a, b) \<in> fst (select S s) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_revoke_dom: "\<And> (p :: (machine_word \<times> bool list) \<times> 'state_ext state). cap_revoke_dom p" using cap_revoke_termination by blast

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

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

lemma ball_subset: "\<forall>x\<in>A. Q x \<Longrightarrow> B \<subseteq> A \<Longrightarrow> \<forall>x\<in>B. Q x" apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>A. Q x; B \<subseteq> A\<rbrakk> \<Longrightarrow> \<forall>x\<in>B. Q x proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_revoke_invs:
  "\<And>ptr. \<lbrace>\<lambda>s::'state_ext state. invs s\<rbrace> cap_revoke ptr \<lbrace>\<lambda>rv. invs\<rbrace>" apply (wp cap_revoke_preservation_desc_of) apply (fastforce simp: emptyable_def dest: reply_slot_not_descendant) apply (wp preemption_point_inv) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>ptr. \<lbrace>invs\<rbrace> cap_revoke ptr \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ptr s sl sa. invs sa \<Longrightarrow> \<forall>sl'\<in>descendants_of sl (cdt sa). emptyable sl' sa
 2. \<And>ptr s. \<lbrace>invs\<rbrace> preemption_point \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ptr s. invs s \<Longrightarrow> invs s proof (prove)
goal (2 subgoals):
 1. \<And>ptr s. \<lbrace>invs\<rbrace> preemption_point \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ptr s. invs s \<Longrightarrow> invs s proof (prove)
goal (4 subgoals):
 1. \<And>ptr s. irq_state_independent_A invs
 2. \<And>ptr s f sa. invs (trans_state f sa) = invs sa
 3. \<And>ptr s sa. invs sa \<Longrightarrow> invs sa
 4. \<And>ptr s. invs s \<Longrightarrow> invs s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma descendants_of_cdt_parent:
  "\<lbrakk> p' \<in> descendants_of p (cdt s) \<rbrakk> \<Longrightarrow> \<exists>p''. cdt s \<Turnstile> p'' \<leadsto> p'" apply (simp add: descendants_of_def del: split_paired_Ex) apply (erule tranclE) apply (erule exI) apply (erule exI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p' \<in> descendants_of p (cdt s) \<Longrightarrow> \<exists>p''. cdt s \<Turnstile> p'' \<leadsto> p' proof (prove)
goal (1 subgoal):
 1. cdt s \<Turnstile> p \<rightarrow> p' \<Longrightarrow> \<exists>p''. cdt s \<Turnstile> p'' \<leadsto> p' proof (prove)
goal (2 subgoals):
 1. cdt s \<Turnstile> p \<leadsto> p' \<Longrightarrow> \<exists>p''. cdt s \<Turnstile> p'' \<leadsto> p'
 2. \<And>c. \<lbrakk>cdt s \<Turnstile> p \<rightarrow> c; cdt s \<Turnstile> c \<leadsto> p'\<rbrakk> \<Longrightarrow> \<exists>p''. cdt s \<Turnstile> p'' \<leadsto> p' proof (prove)
goal (1 subgoal):
 1. \<And>c. \<lbrakk>cdt s \<Turnstile> p \<rightarrow> c; cdt s \<Turnstile> c \<leadsto> p'\<rbrakk> \<Longrightarrow> \<exists>p''. cdt s \<Turnstile> p'' \<leadsto> p' proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_revoke_mdb_stuff3:
  "\<lbrakk> p' \<in> descendants_of p (cdt s); valid_mdb s \<rbrakk>
     \<Longrightarrow> cte_wp_at ((\<noteq>) cap.NullCap) p' s" apply (clarsimp simp add: valid_mdb_def
                     dest!: descendants_of_cdt_parent) apply (simp add: cdt_parent_of_def) apply (drule(1) mdb_cte_atD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p' \<in> descendants_of p (cdt s); valid_mdb s\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) p' s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cdt s \<Turnstile> (a, b) \<leadsto> p'; mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) p' s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cdt s p' = Some (a, b); mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) p' s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>mdb_cte_at (swp (cte_wp_at ((\<noteq>) NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_master_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); valid_arch_mdb (is_original_cap s) (caps_of_state s); swp (cte_wp_at ((\<noteq>) NullCap)) s (a, b) \<and> swp (cte_wp_at ((\<noteq>) NullCap)) s p'\<rbrakk> \<Longrightarrow> cte_wp_at ((\<noteq>) NullCap) p' s proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma inv_cnode_typ_at:
  "\<And>P T p ci. \<lbrace>\<lambda>s::'state_ext state. P (typ_at T p s)\<rbrace> invoke_cnode ci \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" apply (case_tac ci, simp_all add: invoke_cnode_def split del: if_split) apply (wp cap_insert_typ_at cap_move_typ_at cap_swap_typ_at hoare_drop_imps
                  cap_delete_typ_at cap_revoke_typ_at hoare_vcg_all_lift | wpc |
               simp | rule conjI impI | rule hoare_pre)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P T p ci. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> invoke_cnode ci \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>P T p ci x11 x12 x13. ci = InsertCall x11 x12 x13 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> liftE (cap_insert x11 x12 x13) \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
 2. \<And>P T p ci x21 x22 x23. ci = MoveCall x21 x22 x23 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> liftE (cap_move x21 x22 x23) \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
 3. \<And>P T p ci x3. ci = RevokeCall x3 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> cap_revoke x3 \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
 4. \<And>P T p ci x4. ci = DeleteCall x4 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> cap_delete x4 \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
 5. \<And>P T p ci x51 x52 x53 x54 x55. ci = RotateCall x51 x52 x53 x54 x55 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> liftE (if x53 = x55 then cap_swap x51 x55 x52 x54 else do y <- cap_move x52 x54 x55;
cap_move x51 x53 x54
od) \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
 6. \<And>P T p ci x6. ci = SaveCall x6 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> liftE (do thread <- gets cur_thread;
cap <- get_cap (thread, tcb_cnode_index 3);
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap (thread, tcb_cnode_index 3) x6 | _ \<Rightarrow> fail
od) \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>
 7. \<And>P T p ci x7. ci = CancelBadgedSendsCall x7 \<Longrightarrow> \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> case x7 of EndpointCap ep b R \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | _ \<Rightarrow> fail \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma invoke_cnode_tcb[wp]:
  "\<And>tptr ci. \<lbrace>tcb_at tptr::'state_ext state \<Rightarrow> bool\<rbrace> invoke_cnode ci \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>" by (simp add: tcb_at_typ, wp inv_cnode_typ_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>tptr ci. \<lbrace>tcb_at tptr\<rbrace> invoke_cnode ci \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>
theory CNodeInv_AI

lemma zombies_final_caps_of_state:
  "zombies_final = zombies_final_caps \<circ> caps_of_state" by (rule ext,
      simp add: zombies_final_def2 zombies_final_caps_def
                cte_wp_at_caps_of_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zombies_final = zombies_final_caps \<circ> caps_of_state
theory CNodeInv_AI

lemma set_cdt_caps_of_state[wp]:
  "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_cdt p \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (simp add: set_cdt_def) apply wp apply (simp add: caps_of_state_cte_wp_at) done

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

lemma cap_move_caps_of_state:
  notes fun_upd_apply [simp del]
  shows "\<lbrace>\<lambda>s. P ((caps_of_state s) (ptr' \<mapsto> cap, ptr \<mapsto> cap.NullCap ))\<rbrace>
           cap_move cap ptr ptr'
         \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" by (wpsimp simp: cap_move_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P ((caps_of_state s)(ptr' \<mapsto> cap, ptr \<mapsto> NullCap))\<rbrace> cap_move cap ptr ptr' \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
theory CNodeInv_AI

lemma state_refs_of_rvk[simp]:
  "state_refs_of (is_original_cap_update f s) = state_refs_of s" by (simp add: state_refs_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. state_refs_of (is_original_cap_update f s) = state_refs_of s
theory CNodeInv_AI

lemma weak_derived_is_zombie:
  "weak_derived cap cap' \<Longrightarrow> is_zombie cap = is_zombie cap'" by (auto simp: weak_derived_def copy_of_def is_cap_simps same_object_as_def
           split: if_split_asm cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived cap cap' \<Longrightarrow> is_zombie cap = is_zombie cap'
theory CNodeInv_AI

lemma weak_derived_cte_refs':
  "weak_derived cap cap' \<Longrightarrow> cte_refs cap = cte_refs cap'" by (fastforce simp: copy_of_cte_refs weak_derived_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_derived cap cap' \<Longrightarrow> cte_refs cap = cte_refs cap'
theory CNodeInv_AI

lemma appropriate_cte_master:
  "appropriate_cte_cap (cap_master_cap cap) = appropriate_cte_cap cap" apply (rule ext) apply (simp add: cap_master_cap_def appropriate_cte_cap_def
            split: cap.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. appropriate_cte_cap (cap_master_cap cap) = appropriate_cte_cap cap proof (prove)
goal (1 subgoal):
 1. \<And>x. appropriate_cte_cap (cap_master_cap cap) x = appropriate_cte_cap cap x proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cap_range_NullCap:
  "cap_range cap.NullCap = {}" by (simp add: cap_range_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_range NullCap = {}
theory CNodeInv_AI

lemma copy_of_reply_master:
  "copy_of cap cap' \<Longrightarrow> is_master_reply_cap cap = is_master_reply_cap cap'" apply (clarsimp simp: copy_of_def is_cap_simps) apply (clarsimp simp: same_object_as_def split: cap.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. copy_of cap cap' \<Longrightarrow> is_master_reply_cap cap = is_master_reply_cap cap' proof (prove)
goal (1 subgoal):
 1. if \<exists>dev r bits f. cap' = UntypedCap dev r bits f then cap' = cap else same_object_as cap' cap \<and> (\<exists>x R. cap' = ReplyCap x False R) = (\<exists>x R. cap = ReplyCap x False R) \<and> (\<exists>x R. cap' = ReplyCap x True R) = (\<exists>x R. cap = ReplyCap x True R) \<Longrightarrow> (\<exists>x R. cap = ReplyCap x True R) = (\<exists>x R. cap' = ReplyCap x True R) proof (prove)
goal:
No subgoals!
theory CNodeInv_AI

lemma cte_wp_at_use2:
  "\<lbrakk>cte_wp_at P p s; cte_wp_at P' p s; \<And>c. \<lbrakk>cte_wp_at ((=) c) p s; P c; P' c\<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" by (auto simp: cte_wp_at_caps_of_state)

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

lemma cte_wp_at_use3:
  "\<lbrakk>cte_wp_at P p s; cte_wp_at P' p s; cte_wp_at P'' p s; \<And>c. \<lbrakk>cte_wp_at ((=) c) p s; P c; P' c; P'' c\<rbrakk> \<Longrightarrow> Q \<rbrakk> \<Longrightarrow> Q" by (auto simp: cte_wp_at_caps_of_state)

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

lemma cap_move_valid_cap[wp]:
  "\<lbrace>\<lambda>s. s \<turnstile> cap'\<rbrace> cap_move cap p p' \<lbrace>\<lambda>_ s. s \<turnstile> cap'\<rbrace>" unfolding cap_move_def by (wp set_cdt_valid_cap | simp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s \<turnstile> cap'\<rbrace> cap_move cap p p' \<lbrace>\<lambda>_ s. s \<turnstile> cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. s \<turnstile> cap'\<rbrace> do set_cap cap p';
set_cap NullCap p;
src_p <- gets (\<lambda>s. cdt s p);
dest_p <- gets (\<lambda>s. cdt s p');
cdt <- gets cdt;
parent <- return $ cdt p;
cdt' <- return $ cdt(p' := parent, p := None);
set_cdt (\<lambda>r. if cdt' r = Some p then Some p' else cdt' r);
do_extended_op (cap_move_ext p p' src_p dest_p);
is_original <- gets is_original_cap;
set_original p' (is_original p);
set_original p False
od \<lbrace>\<lambda>_ s. s \<turnstile> cap'\<rbrace>