theory KHeap_AI

lemma set_object_valid_ioc_caps:
  "\<lbrace>\<lambda>s. valid_ioc s \<and> typ_at (a_type obj) ptr s \<and>
    (\<forall>b. is_original_cap s (ptr,b) \<longrightarrow> null_filter (cap_of obj) b \<noteq> None)\<rbrace>
   set_object ptr obj
   \<lbrace>\<lambda>_ s. valid_ioc s\<rbrace>" apply (wpsimp wp: set_object_wp_strong) apply (clarsimp simp add: valid_ioc_def) apply (drule spec, drule spec, erule impE, assumption) apply (case_tac "a=ptr", simp_all add: cte_wp_at_cases) apply (drule spec, erule impE, assumption) apply (erule disjE) apply (rule disjI1) apply (clarsimp simp add: obj_at_def a_type_simps) apply (fastforce simp: a_type_def cap_of_def
                         null_filter_def
                  split: Structures_A.kernel_object.splits if_split_asm) apply (rule disjI2) apply (clarsimp simp add: obj_at_def a_type_simps) apply (fastforce simp: a_type_def cap_of_def tcb_cnode_map_def null_filter_def
                 split: Structures_A.kernel_object.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_ioc s \<and> typ_at (a_type obj) ptr s \<and> (\<forall>b. is_original_cap s (ptr, b) \<longrightarrow> null_filter (cap_of obj) b \<noteq> None)\<rbrace> set_object ptr obj \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>valid_ioc s; typ_at (a_type ko) ptr s; \<forall>b. is_original_cap s (ptr, b) \<longrightarrow> (\<exists>y. null_filter (cap_of obj) b = Some y); ko_at ko ptr s; a_type obj = a_type ko\<rbrakk> \<Longrightarrow> valid_ioc (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a b. \<lbrakk>\<forall>a b. is_original_cap s (a, b) \<longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s; typ_at (a_type ko) ptr s; \<forall>b. is_original_cap s (ptr, b) \<longrightarrow> (\<exists>y. null_filter (cap_of obj) b = Some y); ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (a, b)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a b. \<lbrakk>typ_at (a_type ko) ptr s; \<forall>b. is_original_cap s (ptr, b) \<longrightarrow> (\<exists>y. null_filter (cap_of obj) b = Some y); ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (a, b); cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>x. x \<noteq> NullCap) (a, b) (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a b. \<lbrakk>typ_at (a_type ko) ptr s; \<forall>b. is_original_cap s (ptr, b) \<longrightarrow> (\<exists>y. null_filter (cap_of obj) b = Some y); ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (ptr, b); (\<exists>sz fun. kheap s ptr = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s ptr = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); a = ptr\<rbrakk> \<Longrightarrow> (\<exists>sz fun. obj = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. obj = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a b. \<lbrakk>typ_at (a_type ko) ptr s; ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (ptr, b); (\<exists>sz fun. kheap s ptr = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. kheap s ptr = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); a = ptr; \<exists>y. null_filter (cap_of obj) b = Some y\<rbrakk> \<Longrightarrow> (\<exists>sz fun. obj = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. obj = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko a b. \<lbrakk>typ_at (a_type ko) ptr s; ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (ptr, b); a = ptr; \<exists>y. null_filter (cap_of obj) b = Some y; \<exists>sz fun. kheap s ptr = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)\<rbrakk> \<Longrightarrow> (\<exists>sz fun. obj = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. obj = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap))
 2. \<And>s ko a b. \<lbrakk>typ_at (a_type ko) ptr s; ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (ptr, b); a = ptr; \<exists>y. null_filter (cap_of obj) b = Some y; \<exists>tcb. kheap s ptr = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)\<rbrakk> \<Longrightarrow> (\<exists>sz fun. obj = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. obj = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)) proof (prove)
goal (2 subgoals):
 1. \<And>s ko a b. \<lbrakk>typ_at (a_type ko) ptr s; ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (ptr, b); a = ptr; \<exists>y. null_filter (cap_of obj) b = Some y; \<exists>sz fun. kheap s ptr = Some (CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)\<rbrakk> \<Longrightarrow> \<exists>sz fun. obj = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)
 2. \<And>s ko a b. \<lbrakk>typ_at (a_type ko) ptr s; ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (ptr, b); a = ptr; \<exists>y. null_filter (cap_of obj) b = Some y; \<exists>tcb. kheap s ptr = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)\<rbrakk> \<Longrightarrow> (\<exists>sz fun. obj = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. obj = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)) proof (prove)
goal (2 subgoals):
 1. \<And>s b y sz fun cap cs. \<lbrakk>kheap s ptr = Some (CNode sz fun); is_original_cap s (ptr, b); null_filter (cap_of (CNode sz cs)) b = Some y; well_formed_cnode_n sz fun; fun b = Some cap; cap \<noteq> NullCap; well_formed_cnode_n sz cs; obj = CNode sz cs\<rbrakk> \<Longrightarrow> \<exists>cap. cs b = Some cap \<and> cap \<noteq> NullCap
 2. \<And>s ko a b. \<lbrakk>typ_at (a_type ko) ptr s; ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (ptr, b); a = ptr; \<exists>y. null_filter (cap_of obj) b = Some y; \<exists>tcb. kheap s ptr = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)\<rbrakk> \<Longrightarrow> (\<exists>sz fun. obj = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. obj = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a b. \<lbrakk>typ_at (a_type ko) ptr s; ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (ptr, b); a = ptr; \<exists>y. null_filter (cap_of obj) b = Some y; \<exists>tcb. kheap s ptr = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)\<rbrakk> \<Longrightarrow> (\<exists>sz fun. obj = CNode sz fun \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> cap \<noteq> NullCap)) \<or> (\<exists>tcb. obj = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko a b. \<lbrakk>typ_at (a_type ko) ptr s; ko_at ko ptr s; a_type obj = a_type ko; is_original_cap s (ptr, b); a = ptr; \<exists>y. null_filter (cap_of obj) b = Some y; \<exists>tcb. kheap s ptr = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)\<rbrakk> \<Longrightarrow> \<exists>tcb. obj = TCB tcb \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap) proof (prove)
goal (1 subgoal):
 1. \<And>s b y tcb get set restr tcba. \<lbrakk>kheap s ptr = Some (TCB tcb); is_original_cap s (ptr, b); null_filter (cap_of (TCB tcba)) b = Some y; get tcb \<noteq> NullCap; tcb_cap_cases b = Some (get, set, restr); obj = TCB tcba; get tcba = NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!