kings-crown/FVELER_Isabelle huggingface dataset:
theory Dpolicy

lemma opt_cap_pd_Some':
  "\<lbrakk> valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun));
     slot < ucast (kernel_base >> 20) \<rbrakk> \<Longrightarrow>
     (opt_cap (a, unat slot) (transform s)) = Some (transform_pde (fun slot))" apply (clarsimp simp:opt_cap_def transform_def slots_of_def object_slots_def
                       transform_objects_def restrict_map_def map_add_def not_idle_thread_def) apply (frule arch_obj_not_idle,simp) apply (clarsimp simp:transform_page_directory_contents_def unat_map_def not_idle_thread_def
                       kernel_pde_mask_def word_not_le[symmetric]) apply (rule unat_lt2p[where 'a="12", simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); slot < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> opt_cap (a, unat slot) (transform s) = Some (transform_pde (fun slot)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); slot < UCAST(32 \<rightarrow> 12) (kernel_base >> 20)\<rbrakk> \<Longrightarrow> (a \<noteq> idle_thread s \<longrightarrow> transform_page_directory_contents fun (unat slot) = Some (transform_pde (fun slot))) \<and> a \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); slot < UCAST(32 \<rightarrow> 12) (kernel_base >> 20); not_idle_thread a s\<rbrakk> \<Longrightarrow> (a \<noteq> idle_thread s \<longrightarrow> transform_page_directory_contents fun (unat slot) = Some (transform_pde (fun slot))) \<and> a \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); \<not> UCAST(32 \<rightarrow> 12) (kernel_base >> 20) \<le> slot; a \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> unat slot < 4096 proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma pde_cdl_obj_refs:
  "\<lbrakk> pde_ref2 pde = Some (a, b, c); ptr \<in> ptr_range a b \<rbrakk> \<Longrightarrow>
     ptr \<in> cdl_obj_refs (transform_pde pde)" apply (case_tac pde; simp add: pde_ref2_def transform_pde_def ptr_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref2 pde = Some (a, b, c); ptr \<in> ptr_range a b\<rbrakk> \<Longrightarrow> ptr \<in> cdl_obj_refs (transform_pde pde) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma pde_cdl_cap_auth_conferred:
  "\<lbrakk> pde_ref2 pde = Some (a, b, c); auth \<in> c \<rbrakk> \<Longrightarrow>
     auth \<in> cdl_cap_auth_conferred (transform_pde pde)" apply (case_tac pde; simp add: pde_ref2_def transform_pde_def cdl_cap_auth_conferred_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref2 pde = Some (a, b, c); auth \<in> c\<rbrakk> \<Longrightarrow> auth \<in> cdl_cap_auth_conferred (transform_pde pde) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma pte_ref_transform_rev:
  "ptr' \<in> cdl_obj_refs (transform_pte pte) \<Longrightarrow>
       pte_ref pte = Some (cap_object (transform_pte pte), get_size (transform_pte pte),
                           cdl_cap_auth_conferred (transform_pte pte)) \<and>
       ptr' \<in> ptr_range (cap_object (transform_pte pte)) (get_size (transform_pte pte))" apply (case_tac pte) apply (simp_all add:pte_ref_def transform_pte_def
                        vspace_cap_rights_to_auth_def cdl_cap_auth_conferred_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr' \<in> cdl_obj_refs (transform_pte pte) \<Longrightarrow> pte_ref pte = Some (cap_object (transform_pte pte), get_size (transform_pte pte), cdl_cap_auth_conferred (transform_pte pte)) \<and> ptr' \<in> ptr_range (cap_object (transform_pte pte)) (get_size (transform_pte pte)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pte pte); pte = InvalidPTE\<rbrakk> \<Longrightarrow> pte_ref pte = Some (cap_object (transform_pte pte), get_size (transform_pte pte), cdl_cap_auth_conferred (transform_pte pte)) \<and> ptr' \<in> ptr_range (cap_object (transform_pte pte)) (get_size (transform_pte pte))
 2. \<And>x21 x22 x23. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pte pte); pte = LargePagePTE x21 x22 x23\<rbrakk> \<Longrightarrow> pte_ref pte = Some (cap_object (transform_pte pte), get_size (transform_pte pte), cdl_cap_auth_conferred (transform_pte pte)) \<and> ptr' \<in> ptr_range (cap_object (transform_pte pte)) (get_size (transform_pte pte))
 3. \<And>x31 x32 x33. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pte pte); pte = SmallPagePTE x31 x32 x33\<rbrakk> \<Longrightarrow> pte_ref pte = Some (cap_object (transform_pte pte), get_size (transform_pte pte), cdl_cap_auth_conferred (transform_pte pte)) \<and> ptr' \<in> ptr_range (cap_object (transform_pte pte)) (get_size (transform_pte pte)) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma pde_ref_transform_rev:
  "ptr' \<in> cdl_obj_refs (transform_pde pde) \<Longrightarrow>
       pde_ref2 pde = Some (cap_object (transform_pde pde), get_size (transform_pde pde),
                           cdl_cap_auth_conferred (transform_pde pde)) \<and>
       ptr' \<in> ptr_range (cap_object (transform_pde pde)) (get_size (transform_pde pde))" apply (case_tac pde) apply (simp_all add:pde_ref2_def transform_pde_def ptr_range_def
                         vspace_cap_rights_to_auth_def cdl_cap_auth_conferred_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr' \<in> cdl_obj_refs (transform_pde pde) \<Longrightarrow> pde_ref2 pde = Some (cap_object (transform_pde pde), get_size (transform_pde pde), cdl_cap_auth_conferred (transform_pde pde)) \<and> ptr' \<in> ptr_range (cap_object (transform_pde pde)) (get_size (transform_pde pde)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde pde); pde = InvalidPDE\<rbrakk> \<Longrightarrow> pde_ref2 pde = Some (cap_object (transform_pde pde), get_size (transform_pde pde), cdl_cap_auth_conferred (transform_pde pde)) \<and> ptr' \<in> ptr_range (cap_object (transform_pde pde)) (get_size (transform_pde pde))
 2. \<And>x21 x22 x23. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde pde); pde = PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> pde_ref2 pde = Some (cap_object (transform_pde pde), get_size (transform_pde pde), cdl_cap_auth_conferred (transform_pde pde)) \<and> ptr' \<in> ptr_range (cap_object (transform_pde pde)) (get_size (transform_pde pde))
 3. \<And>x31 x32 x33 x34. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde pde); pde = SectionPDE x31 x32 x33 x34\<rbrakk> \<Longrightarrow> pde_ref2 pde = Some (cap_object (transform_pde pde), get_size (transform_pde pde), cdl_cap_auth_conferred (transform_pde pde)) \<and> ptr' \<in> ptr_range (cap_object (transform_pde pde)) (get_size (transform_pde pde))
 4. \<And>x41 x42 x43. \<lbrakk>ptr' \<in> cdl_obj_refs (transform_pde pde); pde = SuperSectionPDE x41 x42 x43\<rbrakk> \<Longrightarrow> pde_ref2 pde = Some (cap_object (transform_pde pde), get_size (transform_pde pde), cdl_cap_auth_conferred (transform_pde pde)) \<and> ptr' \<in> ptr_range (cap_object (transform_pde pde)) (get_size (transform_pde pde)) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma cdl_transform_null_cap:
  "\<lbrakk> einvs s; caps_of_state s (ptr, slot) = Some cap;
     opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap \<rbrakk> \<Longrightarrow>
   cap = cap.NullCap" apply (case_tac "ptr = idle_thread s") apply (clarsimp simp: opt_cap_def slots_of_def
                         transform_def transform_cslot_ptr_def transform_objects_def
                         map_add_def) apply (subst (asm) caps_of_state_transform_opt_cap, assumption) apply fastforce apply fastforce apply (clarsimp simp: transform_cap_def split: cap.splits arch_cap.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> cap = cap.NullCap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap; ptr = idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.NullCap
 2. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap; ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap; ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.NullCap proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ptr \<noteq> idle_thread s; einvs s; caps_of_state s (ptr, slot) = Some cap\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<lbrakk>ptr \<noteq> idle_thread s; einvs s; caps_of_state s (ptr, slot) = Some cap\<rbrakk> \<Longrightarrow> fst (ptr, slot) \<noteq> idle_thread s
 3. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; Some (transform_cap cap) = Some cdl_cap.NullCap; ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.NullCap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<noteq> idle_thread s; einvs s; caps_of_state s (ptr, slot) = Some cap\<rbrakk> \<Longrightarrow> fst (ptr, slot) \<noteq> idle_thread s
 2. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; Some (transform_cap cap) = Some cdl_cap.NullCap; ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; Some (transform_cap cap) = Some cdl_cap.NullCap; ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.NullCap proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma cdl_transform_reply_cap:
  "\<lbrakk> einvs s; caps_of_state s (ptr, slot) = Some cap;
     opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R) \<rbrakk> \<Longrightarrow>
   cap = cap.ReplyCap t False R" apply (case_tac "ptr = idle_thread s") apply (clarsimp simp: opt_cap_def slots_of_def
                         transform_def transform_cslot_ptr_def transform_objects_def
                         map_add_def) apply (subst (asm) caps_of_state_transform_opt_cap, assumption) apply fastforce apply fastforce apply (clarsimp simp: transform_cap_def split: cap.splits arch_cap.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R)\<rbrakk> \<Longrightarrow> cap = cap.ReplyCap t False R proof (prove)
goal (2 subgoals):
 1. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R); ptr = idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.ReplyCap t False R
 2. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R); ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.ReplyCap t False R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R); ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.ReplyCap t False R proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ptr \<noteq> idle_thread s; einvs s; caps_of_state s (ptr, slot) = Some cap\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<lbrakk>ptr \<noteq> idle_thread s; einvs s; caps_of_state s (ptr, slot) = Some cap\<rbrakk> \<Longrightarrow> fst (ptr, slot) \<noteq> idle_thread s
 3. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; Some (transform_cap cap) = Some (cdl_cap.ReplyCap t R); ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.ReplyCap t False R proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptr \<noteq> idle_thread s; einvs s; caps_of_state s (ptr, slot) = Some cap\<rbrakk> \<Longrightarrow> fst (ptr, slot) \<noteq> idle_thread s
 2. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; Some (transform_cap cap) = Some (cdl_cap.ReplyCap t R); ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.ReplyCap t False R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; caps_of_state s (ptr, slot) = Some cap; Some (transform_cap cap) = Some (cdl_cap.ReplyCap t R); ptr \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> cap = cap.ReplyCap t False R proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma asid_table_entry_transform:
  "arm_asid_table (arch_state s) (asid_high_bits_of asid) = poolptr \<Longrightarrow>
   cdl_asid_table (transform s) (fst (transform_asid asid)) =
                        Some (transform_asid_table_entry poolptr)" apply (clarsimp simp:transform_def transform_asid_table_def unat_map_def
                       transform_asid_table_entry_def transform_asid_def) apply (simp add:transform_asid_def asid_high_bits_of_def asid_low_bits_def) apply (rule unat_lt2p[where 'a=7, simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asid_table s (asid_high_bits_of asid) = poolptr \<Longrightarrow> cdl_asid_table (transform s) (fst (transform_asid asid)) = Some (transform_asid_table_entry poolptr) proof (prove)
goal (1 subgoal):
 1. poolptr = asid_table s (asid_high_bits_of asid) \<Longrightarrow> unat (asid_high_bits_of asid) < 128 proof (prove)
goal (1 subgoal):
 1. poolptr = asid_table s (UCAST(32 \<rightarrow> 7) (asid >> 10)) \<Longrightarrow> unat (UCAST(32 \<rightarrow> 7) (asid >> 10)) < 128 proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma transform_asid_high_bits_of:
  "of_nat (fst (transform_asid asid)) = asid_high_bits_of asid" apply (clarsimp simp:transform_asid_def asid_high_bits_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_nat (fst (transform_asid asid)) = asid_high_bits_of asid proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma transform_asid_high_bits_of':
  "fst (transform_asid asid) = unat (asid_high_bits_of asid)" apply (clarsimp simp:transform_asid_def asid_high_bits_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. fst (transform_asid asid) = unat (asid_high_bits_of asid) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma transform_asid_low_bits_of:
  "of_nat (snd (transform_asid asid)) = (ucast asid :: 10 word)" apply (clarsimp simp:transform_asid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. word_of_nat (snd (transform_asid asid)) = UCAST(32 \<rightarrow> 10) asid proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma cap_asid'_transform:
  "\<lbrakk> invs s; caps_of_state s ptr = Some cap \<rbrakk> \<Longrightarrow> cap_asid' cap = cdl_cap_asid' (transform_cap cap)" supply image_cong_simp [cong del] apply (case_tac cap; simp) apply (drule caps_of_state_valid, simp) apply (rename_tac arch_cap) apply (case_tac arch_cap; simp) apply (clarsimp simp:transform_asid_high_bits_of' valid_cap_def split:option.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s ptr = Some cap\<rbrakk> \<Longrightarrow> cap_asid' cap = cdl_cap_asid' (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s ptr = Some cap\<rbrakk> \<Longrightarrow> cap_asid' cap = cdl_cap_asid' (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>invs s; caps_of_state s ptr = Some (ArchObjectCap x12); cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> acap_asid' x12 = cdl_cap_asid' (transform_cap (ArchObjectCap x12)) proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>caps_of_state s ptr = Some (ArchObjectCap x12); cap = ArchObjectCap x12; s \<turnstile> ArchObjectCap x12\<rbrakk> \<Longrightarrow> acap_asid' x12 = cdl_cap_asid' (transform_cap (ArchObjectCap x12)) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. \<lbrakk>caps_of_state s ptr = Some (ArchObjectCap arch_cap); cap = ArchObjectCap arch_cap; s \<turnstile> ArchObjectCap arch_cap\<rbrakk> \<Longrightarrow> acap_asid' arch_cap = cdl_cap_asid' (transform_cap (ArchObjectCap arch_cap)) proof (prove)
goal (4 subgoals):
 1. \<And>arch_cap x11 x12. \<lbrakk>caps_of_state s ptr = Some (ArchObjectCap (ASIDPoolCap x11 x12)); cap = ArchObjectCap (ASIDPoolCap x11 x12); s \<turnstile> ArchObjectCap (ASIDPoolCap x11 x12); arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> {x. asid_high_bits_of x = asid_high_bits_of x12 \<and> x \<noteq> 0} = {x. fst (transform_asid x) = fst (transform_asid x12) \<and> x \<noteq> 0}
 2. \<And>arch_cap x31 x32 x33 x34 x35. \<lbrakk>caps_of_state s ptr = Some (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); s \<turnstile> ArchObjectCap (PageCap x31 x32 x33 x34 x35); arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> fst ` set_option x35 = (transform_asid_rev \<circ> fst) ` set_option (transform_mapping x35)
 3. \<And>arch_cap x41 x42. \<lbrakk>caps_of_state s ptr = Some (ArchObjectCap (arch_cap.PageTableCap x41 x42)); cap = ArchObjectCap (arch_cap.PageTableCap x41 x42); s \<turnstile> ArchObjectCap (arch_cap.PageTableCap x41 x42); arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> fst ` set_option x42 = (transform_asid_rev \<circ> fst) ` set_option (transform_mapping x42)
 4. \<And>arch_cap x51 x52. \<lbrakk>caps_of_state s ptr = Some (ArchObjectCap (arch_cap.PageDirectoryCap x51 x52)); cap = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); s \<turnstile> ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> set_option x52 = transform_asid_rev ` set_option (map_option transform_asid x52) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma idle_thread_no_irqs:
  "\<lbrakk> invs s; caps_of_state s ptr = Some cap;
     irq \<in> cap_irqs_controlled cap \<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s" apply (rule notI) apply (drule idle_thread_null_cap, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; caps_of_state s ptr = Some cap; irq \<in> cap_irqs_controlled cap; fst ptr = idle_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma cap_irqs_controlled_transform:
  "cap_irqs_controlled cap = cdl_cap_irqs_controlled (transform_cap cap)" apply (case_tac cap; simp) apply (rename_tac arch_cap) apply (case_tac arch_cap; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_irqs_controlled cap = cdl_cap_irqs_controlled (transform_cap cap) proof (prove)
goal (1 subgoal):
 1. \<And>x12. cap = ArchObjectCap x12 \<Longrightarrow> {} = cdl_cap_irqs_controlled (transform_cap (ArchObjectCap x12)) proof (prove)
goal (1 subgoal):
 1. \<And>arch_cap. cap = ArchObjectCap arch_cap \<Longrightarrow> {} = cdl_cap_irqs_controlled (transform_cap (ArchObjectCap arch_cap)) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma irq_map_wellformed_transform:
  "irq_map_wellformed aag s = cdl_irq_map_wellformed aag (transform s)" apply (clarsimp simp:irq_map_wellformed_aux_def cdl_irq_map_wellformed_aux_def
                       transform_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_map_wellformed aag s = cdl_irq_map_wellformed aag (transform s) proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma einvs_idle_domain:
  "einvs s \<Longrightarrow> \<exists>etcb. ekheap s idle_thread_ptr = Some etcb \<and> tcb_domain etcb = default_domain" apply (clarsimp simp: valid_sched_def valid_idle_etcb_def etcb_at_def
                        valid_etcbs_def invs_def valid_state_def valid_idle_def pred_tcb_at_def obj_at_def is_etcb_at_def
                       split: option.splits) apply (erule_tac x="idle_thread s" in allE) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. einvs s \<Longrightarrow> \<exists>etcb. ekheap s idle_thread_ptr = Some etcb \<and> tcb_domain etcb = default_domain proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ekheap s idle_thread_ptr = None; valid_pspace s; valid_mdb s; valid_ioc s; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); only_idle s; if_unsafe_then_cap s; idle (tcb_state tcb); valid_reply_caps s; tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; \<forall>ptr. (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y); valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain_2 (cur_thread s) idle_thread_ptr (scheduler_action s) (cur_domain s) (ekheap s); valid_blocked s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>tcb. \<lbrakk>ekheap s idle_thread_ptr = None; valid_pspace s; valid_mdb s; valid_ioc s; idle_thread s = idle_thread_ptr; kheap s idle_thread_ptr = Some (TCB tcb); only_idle s; if_unsafe_then_cap s; idle (tcb_state tcb); valid_reply_caps s; tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb); valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; valid_list s; valid_queues s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain_2 (cur_thread s) idle_thread_ptr (scheduler_action s) (cur_domain s) (ekheap s); valid_blocked s; (\<exists>ko. kheap s (idle_thread s) = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s (idle_thread s) = Some y)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Dpolicy

lemma tcb_domain_map_wellformed_transform:
  "einvs s \<Longrightarrow>
  tcb_domain_map_wellformed aag s = cdl_tcb_domain_map_wellformed aag (transform s)" by (clarsimp simp: tcb_domain_map_wellformed_aux_def cdl_tcb_domain_map_wellformed_aux_def
                     cdl_domains_of_state_transform)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. einvs s \<Longrightarrow> tcb_domain_map_wellformed aag s = cdl_tcb_domain_map_wellformed aag (transform s)
theory CNode_AC

lemma tcb_domain_map_wellformed_ekheap[intro!, simp]:
  "ekheap (P s) = ekheap s \<Longrightarrow> tcb_domain_map_wellformed aag (P s) = tcb_domain_map_wellformed aag s" by (simp add: tcb_domain_map_wellformed_aux_def get_etcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ekheap (P s) = ekheap s \<Longrightarrow> tcb_domain_map_wellformed aag (P s) = tcb_domain_map_wellformed aag s
theory CNode_AC

lemma set_cap_integrity_autarch:
  "\<lbrace>integrity aag X st and K (is_subject aag (fst slot))\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" by (wpsimp simp: set_cap_def wp: set_object_integrity_autarch get_object_wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and K (is_subject aag (fst slot))\<rbrace> set_cap cap slot \<lbrace>\<lambda>_. integrity aag X st\<rbrace>