theory KHeap_AI

lemma get_simple_ko_valid [wp]:
  "\<lbrace>valid_objs\<rbrace> get_simple_ko f oref \<lbrace> \<lambda>r s. valid_simple_obj (f r) s\<rbrace>" apply (simp add: get_simple_ko_def) apply (wpsimp) apply (drule valid_objs_imp_valid_simple_objs) apply (clarsimp simp: valid_simple_objs_def partial_inv_def obj_at_def the_equality split: if_splits) apply (drule_tac x=oref in bspec) apply (clarsimp simp: the_equality  split: kernel_object.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> get_simple_ko f oref \<lbrace>\<lambda>r. valid_simple_obj (f r)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs\<rbrace> do kobj <- get_object oref;
y <- assert (a_type kobj = AEndpoint \<or> a_type kobj = ANTFN);
case partial_inv f kobj of None \<Rightarrow> fail | Some x \<Rightarrow> return x
od \<lbrace>\<lambda>r s. case f r of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_objs s; ko_at ko oref s\<rbrakk> \<Longrightarrow> (a_type ko = AEndpoint \<longrightarrow> (\<forall>x. partial_inv f ko = Some x \<longrightarrow> (case f x of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True))) \<and> (a_type ko = ANTFN \<longrightarrow> (\<forall>x. partial_inv f ko = Some x \<longrightarrow> (case f x of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True))) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>ko_at ko oref s; valid_simple_objs s\<rbrakk> \<Longrightarrow> (a_type ko = AEndpoint \<longrightarrow> (\<forall>x. partial_inv f ko = Some x \<longrightarrow> (case f x of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True))) \<and> (a_type ko = ANTFN \<longrightarrow> (\<forall>x. partial_inv f ko = Some x \<longrightarrow> (case f x of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True))) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>kheap s oref = Some (f y); \<forall>ptr\<in>dom (kheap s). \<exists>obj. kheap s ptr = Some obj \<and> (case obj of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True); \<forall>ya y'. f ya = f y \<and> f y' = f y \<longrightarrow> ya = y'\<rbrakk> \<Longrightarrow> (a_type (f y) = AEndpoint \<longrightarrow> (case f y of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True)) \<and> (a_type (f y) = ANTFN \<longrightarrow> (case f y of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True)) proof (prove)
goal (2 subgoals):
 1. \<And>s y. \<lbrakk>kheap s oref = Some (f y); \<forall>ya y'. f ya = f y \<and> f y' = f y \<longrightarrow> ya = y'\<rbrakk> \<Longrightarrow> oref \<in> dom (kheap s)
 2. \<And>s y. \<lbrakk>kheap s oref = Some (f y); \<forall>ya y'. f ya = f y \<and> f y' = f y \<longrightarrow> ya = y'; \<exists>obj. kheap s oref = Some obj \<and> (case obj of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True)\<rbrakk> \<Longrightarrow> (a_type (f y) = AEndpoint \<longrightarrow> (case f y of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True)) \<and> (a_type (f y) = ANTFN \<longrightarrow> (case f y of Endpoint p \<Rightarrow> valid_ep p s | Notification p \<Rightarrow> valid_ntfn p s | ArchObj ao \<Rightarrow> arch_valid_obj ao s | _ \<Rightarrow> True)) proof (prove)
goal:
No subgoals!