kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpacePre_AI

lemma masked_as_full_simps[simp]:
  "masked_as_full (cap.EndpointCap r badge a) cap = (cap.EndpointCap r badge a)"
  "masked_as_full (cap.Zombie r bits n) cap = (cap.Zombie r bits n)"
  "masked_as_full (cap.ArchObjectCap x) cap = (cap.ArchObjectCap x)"
  "masked_as_full (cap.CNodeCap r n g) cap = (cap.CNodeCap r n g)"
  "masked_as_full (cap.ReplyCap r m a) cap = (cap.ReplyCap r m a)"
  "masked_as_full cap.NullCap cap = cap.NullCap"
  "masked_as_full cap.DomainCap cap = cap.DomainCap"
  "masked_as_full (cap.ThreadCap r) cap = cap.ThreadCap r"
  "masked_as_full cap (cap.EndpointCap r badge a) = cap"
  "masked_as_full cap (cap.Zombie r bits n) = cap"
  "masked_as_full cap (cap.ArchObjectCap x) = cap"
  "masked_as_full cap (cap.CNodeCap r n g) = cap"
  "masked_as_full cap (cap.ReplyCap r m a) = cap"
  "masked_as_full cap cap.NullCap = cap"
  "masked_as_full cap cap.DomainCap = cap"
  "masked_as_full cap (cap.ThreadCap r) = cap" by (simp add:masked_as_full_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (((masked_as_full (EndpointCap r badge a) cap = EndpointCap r badge a &&& masked_as_full (Zombie r bits n) cap = Zombie r bits n) &&& masked_as_full (ArchObjectCap x) cap = ArchObjectCap x &&& masked_as_full (CNodeCap r n g) cap = CNodeCap r n g) &&& (masked_as_full (ReplyCap r m a) cap = ReplyCap r m a &&& masked_as_full NullCap cap = NullCap) &&& masked_as_full DomainCap cap = DomainCap &&& masked_as_full (ThreadCap r) cap = ThreadCap r) &&& ((masked_as_full cap (EndpointCap r badge a) = cap &&& masked_as_full cap (Zombie r bits n) = cap) &&& masked_as_full cap (ArchObjectCap x) = cap &&& masked_as_full cap (CNodeCap r n g) = cap) &&& (masked_as_full cap (ReplyCap r m a) = cap &&& masked_as_full cap NullCap = cap) &&& masked_as_full cap DomainCap = cap &&& masked_as_full cap (ThreadCap r) = cap
theory CSpacePre_AI

lemma maksed_as_full_test_function_stuff[simp]:
  "gen_obj_refs (masked_as_full a cap) = gen_obj_refs a"
  "cap_asid (masked_as_full a cap ) = cap_asid a"
  "obj_refs (masked_as_full a cap ) = obj_refs a"
  "is_zombie (masked_as_full a cap ) = is_zombie a"
  "is_cnode_cap (masked_as_full a cap ) = is_cnode_cap a"
  "is_thread_cap (masked_as_full a cap ) = is_thread_cap a"
  "is_domain_cap (masked_as_full a cap ) = is_domain_cap a"
  "is_ep_cap (masked_as_full a cap ) = is_ep_cap a"
  "is_untyped_cap (masked_as_full a cap ) = is_untyped_cap a"
  "is_arch_cap (masked_as_full a cap ) = is_arch_cap a"
  "is_zombie (masked_as_full a cap ) = is_zombie a"
  "is_ntfn_cap (masked_as_full a cap ) = is_ntfn_cap a"
  "is_reply_cap (masked_as_full a cap ) = is_reply_cap a"
  "is_master_reply_cap (masked_as_full a cap ) = is_master_reply_cap a" by (auto simp:masked_as_full_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((gen_obj_refs (masked_as_full a cap) = gen_obj_refs a &&& cap_asid (masked_as_full a cap) = cap_asid a &&& obj_refs (masked_as_full a cap) = obj_refs a) &&& (is_zombie (masked_as_full a cap) = is_zombie a &&& is_cnode_cap (masked_as_full a cap) = is_cnode_cap a) &&& is_thread_cap (masked_as_full a cap) = is_thread_cap a &&& is_domain_cap (masked_as_full a cap) = is_domain_cap a) &&& (is_ep_cap (masked_as_full a cap) = is_ep_cap a &&& is_untyped_cap (masked_as_full a cap) = is_untyped_cap a &&& is_arch_cap (masked_as_full a cap) = is_arch_cap a) &&& (is_zombie (masked_as_full a cap) = is_zombie a &&& is_ntfn_cap (masked_as_full a cap) = is_ntfn_cap a) &&& is_reply_cap (masked_as_full a cap) = is_reply_cap a &&& is_master_reply_cap (masked_as_full a cap) = is_master_reply_cap a
theory ArchCSpacePre_AI

lemma pageBitsForSize_eq[simp]:
  "(pageBitsForSize sz = pageBitsForSize sz') = (sz = sz')" by (case_tac sz) (case_tac sz', simp+)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (pageBitsForSize sz = pageBitsForSize sz') = (sz = sz')
theory ArchCSpacePre_AI

lemma aobj_ref_cases':
  "aobj_ref acap = (case acap of arch_cap.ASIDControlCap \<Rightarrow> aobj_ref acap
                                | _ \<Rightarrow> aobj_ref acap)" by (simp split: arch_cap.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. aobj_ref acap = (case acap of ASIDPoolCap word1 word2 \<Rightarrow> aobj_ref acap | _ \<Rightarrow> aobj_ref acap)
theory ArchCSpacePre_AI

lemma aobj_ref_cases:
  "aobj_ref acap =
  (case acap of
    arch_cap.ASIDPoolCap w1 w2 \<Rightarrow> Some w1
  | arch_cap.ASIDControlCap \<Rightarrow> None
  | arch_cap.PageCap _ w s sz opt \<Rightarrow> Some w
  | arch_cap.PageTableCap w opt \<Rightarrow> Some w
  | arch_cap.PageDirectoryCap w opt \<Rightarrow> Some w)" apply (subst aobj_ref_cases') apply (clarsimp cong: arch_cap.case_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. aobj_ref acap = (case acap of ASIDPoolCap w1 w2 \<Rightarrow> Some w1 | ASIDControlCap \<Rightarrow> None | PageCap x w s sz opt \<Rightarrow> Some w | PageTableCap w opt \<Rightarrow> Some w | PageDirectoryCap w opt \<Rightarrow> Some w) proof (prove)
goal (1 subgoal):
 1. (case acap of ASIDPoolCap word1 word2 \<Rightarrow> aobj_ref acap | _ \<Rightarrow> aobj_ref acap) = (case acap of ASIDPoolCap w1 w2 \<Rightarrow> Some w1 | ASIDControlCap \<Rightarrow> None | PageCap x w s sz opt \<Rightarrow> Some w | PageTableCap w opt \<Rightarrow> Some w | PageDirectoryCap w opt \<Rightarrow> Some w) proof (prove)
goal:
No subgoals!
theory ArchCSpacePre_AI

lemma ups_of_heap_typ_at:
  "ups_of_heap (kheap s) p = Some sz \<longleftrightarrow> data_at sz p s" apply (simp add: typ_at_eq_kheap_obj ups_of_heap_def data_at_def
      split: option.splits Structures_A.kernel_object.splits
             arch_kernel_obj.splits) by force

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (ups_of_heap (kheap s) p = Some sz) = data_at sz p s proof (prove)
goal (1 subgoal):
 1. \<forall>x41 x42. kheap s p = Some (ArchObj (DataPage x41 x42)) \<longrightarrow> (x42 = sz) = (\<not> x41 \<and> x42 = sz \<or> x41 \<and> x42 = sz)
theory ArchCSpacePre_AI

lemma ups_of_heap_typ_at_def:
  "ups_of_heap (kheap s) \<equiv> \<lambda>p.
   if \<exists>!sz. data_at sz p s
     then Some (THE sz. data_at sz p s)
   else None" apply (rule eq_reflection) apply (rule ext) apply (clarsimp simp: ups_of_heap_typ_at) apply (intro conjI impI) apply (frule (1) theI') apply safe apply (fastforce simp: ups_of_heap_typ_at) apply (clarsimp simp add: obj_at_def data_at_def) apply force done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ups_of_heap (kheap s) \<equiv> \<lambda>p. if \<exists>!sz. data_at sz p s then Some (THE sz. data_at sz p s) else None proof (prove)
goal (1 subgoal):
 1. ups_of_heap (kheap s) = (\<lambda>p. if \<exists>!sz. data_at sz p s then Some (THE sz. data_at sz p s) else None) proof (prove)
goal (1 subgoal):
 1. \<And>p. ups_of_heap (kheap s) p = (if \<exists>!sz. data_at sz p s then Some (THE sz. data_at sz p s) else None) proof (prove)
goal (1 subgoal):
 1. \<And>p. ((\<exists>!sz. data_at sz p s) \<longrightarrow> data_at (THE sz. data_at sz p s) p s) \<and> ((\<nexists>!sz. data_at sz p s) \<longrightarrow> ups_of_heap (kheap s) p = None) proof (prove)
goal (2 subgoals):
 1. \<And>p. \<exists>!sz. data_at sz p s \<Longrightarrow> data_at (THE sz. data_at sz p s) p s
 2. \<And>p. \<nexists>!sz. data_at sz p s \<Longrightarrow> ups_of_heap (kheap s) p = None proof (prove)
goal (1 subgoal):
 1. \<And>p. \<nexists>!sz. data_at sz p s \<Longrightarrow> ups_of_heap (kheap s) p = None proof (prove)
goal (2 subgoals):
 1. \<And>p y. ups_of_heap (kheap s) p = Some y \<Longrightarrow> \<exists>sz. data_at sz p s
 2. \<And>p sz y ya. \<lbrakk>data_at sz p s; data_at y p s; ups_of_heap (kheap s) p = Some ya\<rbrakk> \<Longrightarrow> sz = y proof (prove)
goal (1 subgoal):
 1. \<And>p sz y ya. \<lbrakk>data_at sz p s; data_at y p s; ups_of_heap (kheap s) p = Some ya\<rbrakk> \<Longrightarrow> sz = y proof (prove)
goal (1 subgoal):
 1. \<And>p sz y ya. \<lbrakk>(\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch (AUserData sz)) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch (ADeviceData sz)); (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch (AUserData y)) \<or> (\<exists>ko. kheap s p = Some ko \<and> a_type ko = AArch (ADeviceData y)); ups_of_heap (kheap s) p = Some ya\<rbrakk> \<Longrightarrow> sz = y proof (prove)
goal:
No subgoals!
theory ArchCSpacePre_AI

lemma ups_of_heap_non_arch_upd:
  "h x = Some ko \<Longrightarrow> non_arch_obj ko \<Longrightarrow> non_arch_obj ko' \<Longrightarrow> ups_of_heap (h(x \<mapsto> ko')) = ups_of_heap h" by (rule ext) (auto simp add: ups_of_heap_def non_arch_obj_def split: kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>h x = Some ko; non_arch_obj ko; non_arch_obj ko'\<rbrakk> \<Longrightarrow> ups_of_heap (h(x \<mapsto> ko')) = ups_of_heap h
theory ArchCSpacePre_AI

lemma vs_cap_ref_to_table_cap_ref:
  "\<not> is_pg_cap cap \<Longrightarrow> vs_cap_ref cap = table_cap_ref cap" by (simp add: is_pg_cap_def table_cap_ref_def vs_cap_ref_simps
         split: cap.splits arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_pg_cap cap \<Longrightarrow> vs_cap_ref cap = table_cap_ref cap
theory ArchCSpacePre_AI

lemma cap_master_cap_pg_cap:
 "\<lbrakk>cap_master_cap cap = cap_master_cap capa\<rbrakk>
  \<Longrightarrow> is_pg_cap cap = is_pg_cap capa" by (clarsimp simp:cap_master_cap_def is_cap_simps
    split:cap.splits arch_cap.splits dest!:cap_master_cap_eqDs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_cap cap = cap_master_cap capa \<Longrightarrow> is_pg_cap cap = is_pg_cap capa
theory ArchCSpacePre_AI

lemma master_arch_cap_obj_refs:
  "cap_master_arch_cap c = cap_master_arch_cap c' \<Longrightarrow> aobj_ref c = aobj_ref c'" by (simp add: cap_master_arch_cap_def split: arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_arch_cap c = cap_master_arch_cap c' \<Longrightarrow> aobj_ref c = aobj_ref c'
theory ArchCSpacePre_AI

lemma master_arch_cap_cap_class:
  "cap_master_arch_cap c = cap_master_arch_cap c' \<Longrightarrow> acap_class c = acap_class c'" by (simp add: cap_master_arch_cap_def split: arch_cap.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_master_arch_cap c = cap_master_arch_cap c' \<Longrightarrow> acap_class c = acap_class c'
theory ArchCSpacePre_AI

lemma is_cap_free_index_update[simp]:
  "is_pd_cap (src_cap\<lparr>free_index := a\<rparr>) = is_pd_cap src_cap"
  "is_pt_cap (src_cap\<lparr>free_index := a\<rparr>) = is_pt_cap src_cap" by (simp add:is_cap_simps free_index_update_def split:cap.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_pd_cap (free_index_update (\<lambda>_. a) src_cap) = is_pd_cap src_cap &&& is_pt_cap (free_index_update (\<lambda>_. a) src_cap) = is_pt_cap src_cap
theory ArchCSpacePre_AI

lemma masked_as_full_test_function_stuff[simp]:
  "is_pd_cap (masked_as_full a cap ) = is_pd_cap a"
  "is_pt_cap (masked_as_full a cap ) = is_pt_cap a"
  "vs_cap_ref (masked_as_full a cap ) = vs_cap_ref a" by (auto simp:masked_as_full_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_pd_cap (masked_as_full a cap) = is_pd_cap a &&& is_pt_cap (masked_as_full a cap) = is_pt_cap a &&& vs_cap_ref (masked_as_full a cap) = vs_cap_ref a
theory ArchCSpacePre_AI

lemma same_aobject_as_commute:
  "same_aobject_as x y \<Longrightarrow> same_aobject_as y x" by (cases x; cases y; clarsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. same_aobject_as x y \<Longrightarrow> same_aobject_as y x
theory ArchCSpacePre_AI

lemma is_pt_pd_Null[simp]:
  "\<not> is_pt_cap cap.NullCap \<and> \<not> is_pd_cap cap.NullCap" by (simp add: is_pt_cap_def is_pd_cap_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_pt_cap NullCap \<and> \<not> is_pd_cap NullCap
theory ArchCSpacePre_AI

lemma arch_derived_is_device:
  "\<lbrakk>cap_master_arch_cap c = cap_master_arch_cap c';
        is_derived_arch (ArchObjectCap c) (ArchObjectCap c')\<rbrakk>
       \<Longrightarrow> arch_cap_is_device c' = arch_cap_is_device c" apply (case_tac c) apply (clarsimp simp: is_derived_arch_def
    cap_range_def is_cap_simps cap_master_cap_def cap_master_arch_cap_def
              split: if_split_asm cap.splits arch_cap.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_master_arch_cap c = cap_master_arch_cap c'; is_derived_arch (ArchObjectCap c) (ArchObjectCap c')\<rbrakk> \<Longrightarrow> arch_cap_is_device c' = arch_cap_is_device c proof (prove)
goal (5 subgoals):
 1. \<And>x11 x12. \<lbrakk>cap_master_arch_cap c = cap_master_arch_cap c'; is_derived_arch (ArchObjectCap c) (ArchObjectCap c'); c = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> arch_cap_is_device c' = arch_cap_is_device c
 2. \<lbrakk>cap_master_arch_cap c = cap_master_arch_cap c'; is_derived_arch (ArchObjectCap c) (ArchObjectCap c'); c = ASIDControlCap\<rbrakk> \<Longrightarrow> arch_cap_is_device c' = arch_cap_is_device c
 3. \<And>x31 x32 x33 x34 x35. \<lbrakk>cap_master_arch_cap c = cap_master_arch_cap c'; is_derived_arch (ArchObjectCap c) (ArchObjectCap c'); c = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> arch_cap_is_device c' = arch_cap_is_device c
 4. \<And>x41 x42. \<lbrakk>cap_master_arch_cap c = cap_master_arch_cap c'; is_derived_arch (ArchObjectCap c) (ArchObjectCap c'); c = PageTableCap x41 x42\<rbrakk> \<Longrightarrow> arch_cap_is_device c' = arch_cap_is_device c
 5. \<And>x51 x52. \<lbrakk>cap_master_arch_cap c = cap_master_arch_cap c'; is_derived_arch (ArchObjectCap c) (ArchObjectCap c'); c = PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> arch_cap_is_device c' = arch_cap_is_device c proof (prove)
goal:
No subgoals!
theory ArchCSpacePre_AI

lemma valid_arch_mdb_simple:
  "\<And>s capa. \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s);
              is_simple_cap cap; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow>
         valid_arch_mdb ((is_original_cap s) (dest := is_cap_revocable cap capa))
                       ((caps_of_state s)(dest \<mapsto> cap))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s); is_simple_cap cap; caps_of_state s src = Some capa\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
theory ArchCSpacePre_AI

lemma valid_arch_mdb_free_index_update:
  "\<lbrakk>m src = Some capa;m' = m (src\<mapsto> capa\<lparr>free_index :=x\<rparr>) \<rbrakk> \<Longrightarrow>
   valid_arch_mdb c (m') = valid_arch_mdb c (m)" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m src = Some capa; m' = m(src \<mapsto> free_index_update (\<lambda>_. x) capa)\<rbrakk> \<Longrightarrow> valid_arch_mdb c m' = valid_arch_mdb c m
theory ArchCSpacePre_AI

lemma set_cap_update_free_index_valid_arch_mdb:
  "\<lbrace>\<lambda>s. valid_arch_mdb (is_original_cap s) (caps_of_state s) \<and> is_untyped_cap src_cap\<rbrace>
         set_cap (free_index_update f src_cap) src
   \<lbrace>\<lambda>rv s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>" by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_arch_mdb (is_original_cap s) (caps_of_state s) \<and> is_untyped_cap src_cap\<rbrace> set_cap (free_index_update f src_cap) src \<lbrace>\<lambda>rv s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>
theory ArchCSpacePre_AI

lemma set_untyped_cap_as_full_valid_arch_mdb:
  "\<lbrace>\<lambda>s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>
            set_untyped_cap_as_full src_cap c src
   \<lbrace>\<lambda>rv s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>" by (wpsimp wp: set_cap_update_free_index_valid_arch_mdb
           simp: set_untyped_cap_as_full_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> set_untyped_cap_as_full src_cap c src \<lbrace>\<lambda>rv s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>
theory ArchCSpacePre_AI

lemma valid_arch_mdb_not_arch_cap_update:
     "\<And>s cap capa. \<lbrakk>\<not>is_arch_cap cap; valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk>
       \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := True))
            ((caps_of_state s)(src \<mapsto> cap, dest\<mapsto>capa))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s cap capa. \<lbrakk>\<not> is_arch_cap cap; valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := True)) ((caps_of_state s)(src \<mapsto> cap, dest \<mapsto> capa))
theory ArchCSpacePre_AI

lemma valid_arch_mdb_derived_cap_update:
  "\<And>s capa. \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s);
             is_derived (cdt s) src cap capa\<rbrakk> \<Longrightarrow>
           valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa))
                           ((caps_of_state s)(dest \<mapsto> cap))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s); is_derived (cdt s) src cap capa\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap))
theory ArchCSpacePre_AI

lemma valid_arch_mdb_free_index_update':
  "\<And>s capa. \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some capa;
                   is_untyped_cap cap\<rbrakk> \<Longrightarrow>
           valid_arch_mdb ((is_original_cap s) (dest := is_cap_revocable cap capa))
            ((caps_of_state s)(dest \<mapsto> cap, src \<mapsto> max_free_index_update capa))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some capa; is_untyped_cap cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_cap_revocable cap capa)) ((caps_of_state s)(dest \<mapsto> cap, src \<mapsto> max_free_index_update capa))
theory ArchCSpacePre_AI

lemma valid_arch_mdb_weak_derived_update:
  "\<And>s capa. \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s);
                      caps_of_state s src = Some capa; weak_derived cap capa\<rbrakk> \<Longrightarrow>
        valid_arch_mdb ((is_original_cap s) (dest := is_original_cap s src, src := False))
            ((caps_of_state s)(dest \<mapsto> cap, src \<mapsto> NullCap))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s capa. \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s); caps_of_state s src = Some capa; weak_derived cap capa\<rbrakk> \<Longrightarrow> valid_arch_mdb ((is_original_cap s)(dest := is_original_cap s src, src := False)) ((caps_of_state s)(dest \<mapsto> cap, src \<mapsto> NullCap))
theory ArchCSpacePre_AI

lemma valid_arch_mdb_tcb_cnode_update:
  "valid_arch_mdb (is_original_cap s) (caps_of_state s) \<Longrightarrow>
           valid_arch_mdb ((is_original_cap s) ((t, tcb_cnode_index 2) := True))
              ((caps_of_state s)((t, tcb_cnode_index 2) \<mapsto> ReplyCap t True r))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_mdb (is_original_cap s) (caps_of_state s) \<Longrightarrow> valid_arch_mdb ((is_original_cap s)((t, tcb_cnode_index 2) := True)) ((caps_of_state s)((t, tcb_cnode_index 2) \<mapsto> ReplyCap t True r))
theory ArchCSpacePre_AI

lemma safe_parent_for_arch_not_arch':
  "\<not>is_arch_cap cap \<Longrightarrow> \<not>safe_parent_for_arch c cap" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> is_arch_cap cap \<Longrightarrow> \<not> safe_parent_for_arch c cap
theory ArchCSpacePre_AI

lemma safe_parent_arch_is_parent:
  "\<lbrakk>safe_parent_for_arch cap pcap; caps_of_state s p = Some pcap;
      valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow>
    should_be_parent_of pcap (is_original_cap s p) cap f" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>safe_parent_for_arch cap pcap; caps_of_state s p = Some pcap; valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrakk> \<Longrightarrow> should_be_parent_of pcap (is_original_cap s p) cap f
theory ArchCSpacePre_AI

lemma safe_parent_for_arch_no_obj_refs:
  "safe_parent_for_arch cap c \<Longrightarrow> obj_refs cap = {}" by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. safe_parent_for_arch cap c \<Longrightarrow> obj_refs cap = {}
theory ArchCSpacePre_AI

lemma valid_arch_mdb_same_master_cap:
  "\<lbrakk>valid_arch_mdb ioc cs; cs sl = Some cap; cap_master_cap cap' = cap_master_cap cap\<rbrakk> \<Longrightarrow>
  valid_arch_mdb ioc (cs(sl\<mapsto>cap'))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_mdb ioc cs; cs sl = Some cap; cap_master_cap cap' = cap_master_cap cap\<rbrakk> \<Longrightarrow> valid_arch_mdb ioc (cs(sl \<mapsto> cap'))
theory ArchCSpacePre_AI

lemma valid_arch_mdb_null_filter:
  "valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)) = valid_arch_mdb (is_original_cap s) (caps_of_state s)" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_mdb (is_original_cap s) (null_filter (caps_of_state s)) = valid_arch_mdb (is_original_cap s) (caps_of_state s)
theory ArchCSpacePre_AI

lemma valid_arch_mdb_untypeds:
  "\<And>s. valid_arch_mdb (is_original_cap s) (caps_of_state s)
       \<Longrightarrow> valid_arch_mdb (\<lambda>x. x \<noteq> cref \<longrightarrow> is_original_cap s x)
            ((caps_of_state s)(cref \<mapsto> default_cap tp oref sz dev))"
  "\<And>s. valid_arch_mdb (is_original_cap s) (caps_of_state s)
       \<Longrightarrow> valid_arch_mdb (is_original_cap s)
            ((caps_of_state s)(cref \<mapsto> UntypedCap dev ptr sz idx))" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. valid_arch_mdb (is_original_cap s) (caps_of_state s) \<Longrightarrow> valid_arch_mdb (\<lambda>x. x \<noteq> cref \<longrightarrow> is_original_cap s x) ((caps_of_state s)(cref \<mapsto> default_cap tp oref sz dev))) &&& (\<And>s. valid_arch_mdb (is_original_cap s) (caps_of_state s) \<Longrightarrow> valid_arch_mdb (is_original_cap s) ((caps_of_state s)(cref \<mapsto> UntypedCap dev ptr sz idx)))
theory CSpace_AI

lemma capBadge_ordefield_simps[simp]:
  "(None, y) \<in> capBadge_ordering fb"
  "((y, None) \<in> capBadge_ordering fb) = (y = None)"
  "((y, y) \<in> capBadge_ordering fb) = (fb \<longrightarrow> (y = None \<or> y = Some 0))"
  "((Some x, Some z) \<in> capBadge_ordering fb) = (x = 0 \<or> (\<not> fb \<and> x = z))"
  "(y, Some 0) \<in> capBadge_ordering fb = (y = None \<or> y = Some 0)" by (simp add: capBadge_ordering_def disj.commute
           | simp add: eq_commute image_def
           | fastforce)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ((None, y) \<in> capBadge_ordering fb &&& ((y, None) \<in> capBadge_ordering fb) = (y = None)) &&& ((y, y) \<in> capBadge_ordering fb) = (fb \<longrightarrow> y = None \<or> y = Some 0) &&& ((Some x, Some z) \<in> capBadge_ordering fb) = (x = 0 \<or> \<not> fb \<and> x = z) &&& ((y, Some 0) \<in> capBadge_ordering fb) = (y = None \<or> y = Some 0)
theory CSpace_AI

lemma capBadge_ordering_trans:
  "\<lbrakk> (x, y) \<in> capBadge_ordering v; (y, z) \<in> capBadge_ordering v2 \<rbrakk>
       \<Longrightarrow> (x, z) \<in> capBadge_ordering v2" by (auto simp: capBadge_ordering_def split: if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(x, y) \<in> capBadge_ordering v; (y, z) \<in> capBadge_ordering v2\<rbrakk> \<Longrightarrow> (x, z) \<in> capBadge_ordering v2