kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchKHeap_AI

lemma equal_kernel_mappings_lift:
  assumes aobj_at:
    "\<And>P P' pd. vspace_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>"
  shows "\<lbrace>equal_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>" apply (simp add: equal_kernel_mappings_def) apply (rule hoare_vcg_all_lift)+ apply (rule hoare_convert_imp) apply simp apply (rule hoare_convert_imp) apply (wp aobj_at[OF vspace_obj_pred_arch_obj_l])+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equal_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>x y pd pd'. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>x y pd pd'. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x y pd pd'. \<lbrace>\<lambda>s. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrace> f \<lbrace>\<lambda>rv s. ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x y pd pd'. \<lbrace>\<lambda>s. \<not> (ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s)\<rbrace> f \<lbrace>\<lambda>rv s. \<not> (ako_at (PageDirectory pd) x s \<and> ako_at (PageDirectory pd') y s)\<rbrace>
 2. \<And>x y pd pd'. \<lbrace>\<lambda>s. \<forall>w\<in>kernel_mapping_slots. pd w = pd' w\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>w\<in>kernel_mapping_slots. pd w = pd' w\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x y pd pd'. \<lbrace>\<lambda>s. ako_at (PageDirectory pd) x s \<longrightarrow> \<not> ako_at (PageDirectory pd') y s\<rbrace> f \<lbrace>\<lambda>rv s. ako_at (PageDirectory pd) x s \<longrightarrow> \<not> ako_at (PageDirectory pd') y s\<rbrace>
 2. \<And>x y pd pd'. \<lbrace>\<lambda>s. \<forall>w\<in>kernel_mapping_slots. pd w = pd' w\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>w\<in>kernel_mapping_slots. pd w = pd' w\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x y pd pd'. \<lbrace>\<lambda>s. \<not> ako_at (PageDirectory pd) x s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> ako_at (PageDirectory pd) x s\<rbrace>
 2. \<And>x y pd pd'. \<lbrace>\<lambda>s. \<not> ako_at (PageDirectory pd') y s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> ako_at (PageDirectory pd') y s\<rbrace>
 3. \<And>x y pd pd'. \<lbrace>\<lambda>s. \<forall>w\<in>kernel_mapping_slots. pd w = pd' w\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>w\<in>kernel_mapping_slots. pd w = pd' w\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_machine_state_lift:
  assumes memory: "\<And>P. \<lbrace>\<lambda>s. P (underlying_memory (machine_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (underlying_memory (machine_state s))\<rbrace>"
  assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
  shows "\<lbrace>valid_machine_state\<rbrace> f \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" unfolding valid_machine_state_def apply (rule hoare_lift_Pf[where f="\<lambda>s. underlying_memory (machine_state s)", OF _ memory]) apply (rule hoare_vcg_all_lift) apply (rule hoare_vcg_disj_lift[OF _ hoare_vcg_prop]) apply (rule in_user_frame_lift) apply (wp aobj_at; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_machine_state\<rbrace> f \<lbrace>\<lambda>_. valid_machine_state\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0\<rbrace> f \<lbrace>\<lambda>_ s. \<forall>p. in_user_frame p s \<or> underlying_memory (machine_state s) p = 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>p. in_user_frame p s \<or> x p = 0\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>p. in_user_frame p a \<or> x p = 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x p. \<lbrace>\<lambda>s. in_user_frame p s \<or> x p = 0\<rbrace> f \<lbrace>\<lambda>rv s. in_user_frame p s \<or> x p = 0\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x p. \<lbrace>in_user_frame p\<rbrace> f \<lbrace>\<lambda>rv. in_user_frame p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x p T pa. \<lbrace>typ_at (AArch T) pa\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) pa\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_ao_at_lift:
  assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
      and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>"
  shows      "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>" unfolding valid_ao_at_def by (wp hoare_vcg_ex_lift y valid_vspace_obj_typ z)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace>
theory ArchKHeap_AI

lemma valid_ao_at_lift_aobj_at:
  assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
  shows      "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>" unfolding valid_ao_at_def by (wp hoare_vcg_ex_lift valid_vspace_obj_typ aobj_at | clarsimp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace>
theory ArchKHeap_AI

lemma valid_vso_at_lift:
  assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>"
      and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>"
  shows      "\<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>" unfolding valid_vso_at_def by (wpsimp wp: hoare_vcg_ex_lift y valid_vspace_obj_typ z)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace>
theory ArchKHeap_AI

lemma valid_vso_at_lift_aobj_at:
  assumes aobj_at: "\<And>P' pd. vspace_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>"
  shows      "\<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>" unfolding valid_vso_at_def apply (rule hoare_vcg_ex_lift) apply (rule hoare_vcg_conj_lift aobj_at)+ apply (clarsimp simp: vspace_obj_pred_def) apply (rule iffI) apply ((case_tac ao; clarsimp)+)[2] apply (wpsimp wp: valid_vspace_obj_typ) apply (wpsimp wp: aobj_at) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. \<exists>ao. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ao. \<lbrace>\<lambda>s. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace> f \<lbrace>\<lambda>rv s. ako_at ao p s \<and> valid_vspace_obj ao s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ao. vspace_obj_pred ((=) (ArchObj ao))
 2. \<And>ao. \<lbrace>valid_vspace_obj ao\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_obj ao\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ao ko ko'. \<lbrakk>non_vspace_obj ko; non_vspace_obj ko'\<rbrakk> \<Longrightarrow> (ArchObj ao = ko) = (ArchObj ao = ko')
 2. \<And>ao. \<lbrace>valid_vspace_obj ao\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_obj ao\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ao ko ko'. \<lbrakk>non_vspace_obj ko; non_vspace_obj ko'; ArchObj ao = ko\<rbrakk> \<Longrightarrow> ArchObj ao = ko'
 2. \<And>ao ko ko'. \<lbrakk>non_vspace_obj ko; non_vspace_obj ko'; ArchObj ao = ko'\<rbrakk> \<Longrightarrow> ArchObj ao = ko
 3. \<And>ao. \<lbrace>valid_vspace_obj ao\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_obj ao\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ao. \<lbrace>valid_vspace_obj ao\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_obj ao\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>p T. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>
 2. \<And>ao s. valid_vspace_obj ao s \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal (1 subgoal):
 1. \<And>ao s. valid_vspace_obj ao s \<Longrightarrow> valid_vspace_obj ao s proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma set_object_equal_mappings:
  "\<lbrace>\<lambda>s. equal_kernel_mappings s
          \<and> (\<forall>pd. ko = ArchObj (PageDirectory pd)
                \<longrightarrow> (\<forall>x pd'. ko_at (ArchObj (PageDirectory pd')) x s
                         \<longrightarrow> (\<forall>w \<in> kernel_mapping_slots. pd w = pd' w)))\<rbrace>
     set_object p ko
   \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>" apply (wpsimp wp: set_object_wp) apply (clarsimp simp: equal_kernel_mappings_def obj_at_def
             split del: if_split) apply (simp split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. equal_kernel_mappings s \<and> (\<forall>pd. ko = ArchObj (PageDirectory pd) \<longrightarrow> (\<forall>x pd'. ako_at (PageDirectory pd') x s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)))\<rbrace> set_object p ko \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>equal_kernel_mappings s; \<forall>pd. ko = ArchObj (PageDirectory pd) \<longrightarrow> (\<forall>x pd'. ako_at (PageDirectory pd') x s \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w))\<rbrakk> \<Longrightarrow> equal_kernel_mappings (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x y pd pd' w. \<lbrakk>\<forall>x y pd pd'. kheap s x = Some (ArchObj (PageDirectory pd)) \<and> kheap s y = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w); \<forall>pd. ko = ArchObj (PageDirectory pd) \<longrightarrow> (\<forall>x pd'. kheap s x = Some (ArchObj (PageDirectory pd')) \<longrightarrow> (\<forall>w\<in>kernel_mapping_slots. pd w = pd' w)); w \<in> kernel_mapping_slots; (if x = p then Some ko else kheap s x) = Some (ArchObj (PageDirectory pd)); (if y = p then Some ko else kheap s y) = Some (ArchObj (PageDirectory pd'))\<rbrakk> \<Longrightarrow> pd w = pd' w proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma valid_global_vspace_mappings_arch_update[simp]:
  "arm_global_pd (f (arch_state s)) = arm_global_pd (arch_state s)
   \<and> arm_kernel_vspace (f (arch_state s)) = arm_kernel_vspace (arch_state s)
     \<Longrightarrow> valid_global_vspace_mappings (arch_state_update f s) = valid_global_vspace_mappings s" by (simp add: valid_global_vspace_mappings_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arm_global_pd (f (arch_state s)) = arm_global_pd (arch_state s) \<and> arm_kernel_vspace (f (arch_state s)) = arm_kernel_vspace (arch_state s) \<Longrightarrow> valid_global_vspace_mappings (arch_state_update f s) = valid_global_vspace_mappings s
theory ArchKHeap_AI

lemma set_object_global_vspace_mappings:
  "\<lbrace>valid_global_vspace_mappings
            and (\<lambda>s. (page_directory_at p s \<or> page_table_at p s)
                       \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s)\<rbrace>
     set_object p ko
   \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" apply (wpsimp wp: set_object_wp) apply (erule valid_global_vspace_mappings_pres) apply (clarsimp simp: obj_at_def a_type_def global_refs_def second_level_tables_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_vspace_mappings and (\<lambda>s. typ_at (AArch APageDirectory) p s \<or> typ_at (AArch APageTable) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s)\<rbrace> set_object p ko \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_global_vspace_mappings s; typ_at (AArch APageDirectory) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s; typ_at (AArch APageTable) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s\<rbrakk> \<Longrightarrow> valid_global_vspace_mappings (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) proof (prove)
goal (4 subgoals):
 1. \<And>s pd. \<lbrakk>typ_at (AArch APageDirectory) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s; typ_at (AArch APageTable) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s; ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) s\<rbrakk> \<Longrightarrow> ako_at (PageDirectory pd) (arm_global_pd (arch_state s)) (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
 2. \<And>s pt pa. \<lbrakk>typ_at (AArch APageDirectory) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s; typ_at (AArch APageTable) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s; ako_at (PageTable pt) pa s; valid_global_objs s \<Longrightarrow> pa \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> ako_at (PageTable pt) pa (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)
 3. \<And>s. \<lbrakk>typ_at (AArch APageDirectory) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s; typ_at (AArch APageTable) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s\<rbrakk> \<Longrightarrow> arm_global_pd (arch_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)) = arm_global_pd (arch_state s)
 4. \<And>s. \<lbrakk>typ_at (AArch APageDirectory) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s; typ_at (AArch APageTable) p s \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s\<rbrakk> \<Longrightarrow> arm_kernel_vspace (arch_state (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>)) = arm_kernel_vspace (arch_state s) proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma store_pde_pred_tcb_at:
  "\<lbrace>pred_tcb_at proj P t\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>" apply (simp add: store_pde_def set_pd_def get_pd_def) apply (wpsimp wp: set_object_wp get_object_wp simp: a_type_def) apply (clarsimp simp: pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at proj P t\<rbrace> do pd <- get_object (ptr && ~~ mask pd_bits) >>= case_kernel_object (\<lambda>nat fun. fail) (\<lambda>tcb_ext. fail) (\<lambda>endpoint. fail) (\<lambda>notification_ext. fail) (case_arch_kernel_obj (\<lambda>fun. fail) (\<lambda>fun. fail) return (\<lambda>bool vmpage_size. fail));
set_object (ptr && ~~ mask pd_bits) (ArchObj (PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := val))))
od \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>pred_tcb_at proj P t s; ako_at (PageDirectory xa) (ptr && ~~ mask pd_bits) s\<rbrakk> \<Longrightarrow> pred_tcb_at proj P t (s\<lparr>kheap := (kheap s)(ptr && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (\<lambda>a. if a = UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) then val else xa a)))\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma empty_table_lift:
  assumes S: "\<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>_ s. P (S s)\<rbrace>"
  assumes o: "\<And>P. \<lbrace>obj_at P p and Q\<rbrace> f \<lbrace>\<lambda>_. obj_at P p\<rbrace>"
  shows "\<lbrace>\<lambda>s. obj_at (empty_table (S s)) p s \<and> Q s\<rbrace>
         f \<lbrace>\<lambda>_ s. obj_at (empty_table (S s)) p s\<rbrace>" apply (rule hoare_lift_Pf2 [where f="S"]) apply (wp o S|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at (empty_table (S s)) p s \<and> Q s\<rbrace> f \<lbrace>\<lambda>_ s. obj_at (empty_table (S s)) p s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. obj_at (empty_table x) p s \<and> Q s\<rbrace> f \<lbrace>\<lambda>_. obj_at (empty_table x) p\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>_ s. P (S s)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma user_mem_obj_upd_dom:
  "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow>
   dom (user_mem (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>))
   = dom (user_mem s)" by (clarsimp simp: user_mem_def in_user_frame_obj_upd dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> dom (user_mem (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>)) = dom (user_mem s)
theory ArchKHeap_AI

lemma device_mem_obj_upd_dom:
  "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow>
   dom (device_mem (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>))
   = dom (device_mem s)" by (clarsimp simp: device_mem_def in_device_frame_obj_upd dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> dom (device_mem (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>)) = dom (device_mem s)
theory ArchKHeap_AI

lemma pspace_respects_region_cong[cong]:
  "\<lbrakk>kheap a  = kheap b; device_state (machine_state a) = device_state (machine_state b)\<rbrakk>
  \<Longrightarrow> pspace_respects_device_region a = pspace_respects_device_region b" by (simp add: pspace_respects_device_region_def device_mem_def user_mem_def in_device_frame_def
    in_user_frame_def obj_at_def dom_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap a = kheap b; device_state (machine_state a) = device_state (machine_state b)\<rbrakk> \<Longrightarrow> pspace_respects_device_region a = pspace_respects_device_region b
theory ArchKHeap_AI

lemma cap_is_device_obj_is_device[simp]:
  "cap_is_device (default_cap tp a sz dev) = obj_is_device tp dev" by (simp add: default_cap_def arch_default_cap_def obj_is_device_def
                default_object_def  default_arch_object_def
         split: apiobject_type.splits aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_is_device (default_cap tp a sz dev) = obj_is_device tp dev
theory ArchKHeap_AI

lemma state_hyp_refs_of_ep_update: "\<And>s ep val. typ_at AEndpoint ep s \<Longrightarrow>
       state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint val)\<rparr>) = state_hyp_refs_of s" apply (rule all_ext) apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s ep val. typ_at AEndpoint ep s \<Longrightarrow> state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint val)\<rparr>) = state_hyp_refs_of s proof (prove)
goal (1 subgoal):
 1. \<And>s ep val. typ_at AEndpoint ep s \<Longrightarrow> \<forall>x. state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint val)\<rparr>) x = state_hyp_refs_of s x proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma state_hyp_refs_of_ntfn_update: "\<And>s ep val. typ_at ANTFN ep s \<Longrightarrow>
       state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification val)\<rparr>) = state_hyp_refs_of s" apply (rule all_ext) apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>s ep val. typ_at ANTFN ep s \<Longrightarrow> state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification val)\<rparr>) = state_hyp_refs_of s proof (prove)
goal (1 subgoal):
 1. \<And>s ep val. typ_at ANTFN ep s \<Longrightarrow> \<forall>x. state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification val)\<rparr>) x = state_hyp_refs_of s x proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma state_hyp_refs_of_tcb_state_update:
       "kheap s t = Some (TCB tcb) \<Longrightarrow>
          state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
            = state_hyp_refs_of s" apply (rule all_ext) apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. kheap s t = Some (TCB tcb) \<Longrightarrow> state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>) = state_hyp_refs_of s proof (prove)
goal (1 subgoal):
 1. kheap s t = Some (TCB tcb) \<Longrightarrow> \<forall>x. state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>) x = state_hyp_refs_of s x proof (prove)
goal:
No subgoals!
theory ArchKHeap_AI

lemma arch_valid_obj_same_type:
  "\<lbrakk> arch_valid_obj ao s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
   \<Longrightarrow> arch_valid_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)" by (induction ao rule: arch_kernel_obj.induct;
         clarsimp simp: typ_at_same_type)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_valid_obj ao s; kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> arch_valid_obj ao (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)
theory ArchKHeap_AI

lemma default_arch_object_not_live: "\<not> live (ArchObj (default_arch_object aty dev us))" by (clarsimp simp: default_arch_object_def live_def hyp_live_def arch_live_def
               split: aobject_type.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> live (ArchObj (default_arch_object aty dev us))
theory ArchKHeap_AI

lemma default_tcb_not_live: "\<not> live (TCB default_tcb)" by (clarsimp simp: default_tcb_def default_arch_tcb_def live_def hyp_live_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<not> live (TCB default_tcb)
theory ArchKHeap_AI

lemma valid_arch_tcb_same_type:
  "\<lbrakk> valid_arch_tcb t s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk>
   \<Longrightarrow> valid_arch_tcb t (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)" by (auto simp: valid_arch_tcb_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_arch_tcb t s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> valid_arch_tcb t (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)