theory KHeap_AI

lemma set_object_valid_ioc_no_caps:
  "\<lbrace>\<lambda>s. valid_ioc s \<and> typ_at (a_type obj) ptr s \<and> \<not> is_tcb obj \<and>
        (\<forall>n. \<not> is_cap_table n obj) \<rbrace>
   set_object ptr obj
   \<lbrace>\<lambda>_ s. valid_ioc s\<rbrace>" apply (wpsimp wp: set_object_wp_strong simp: obj_at_def) apply (clarsimp simp add: valid_ioc_def cte_wp_at_cases is_tcb) apply (drule spec, drule spec, erule impE, assumption) apply (elim disjE) prefer 2 apply (fastforce simp: obj_at_def a_type_def
                   split: Structures_A.kernel_object.splits if_split_asm) apply (fastforce simp: obj_at_def a_type_def is_cap_table_def well_formed_cnode_n_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> \<not> is_tcb obj \<and> (\<forall>n. \<not> is_cap_table n obj)\<rbrace> set_object ptr obj \<lbrace>\<lambda>_. valid_ioc\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s koa. \<lbrakk>valid_ioc s; \<not> is_tcb obj; \<forall>n. \<not> is_cap_table n obj; kheap s ptr = Some koa; a_type obj = a_type koa\<rbrakk> \<Longrightarrow> valid_ioc (s\<lparr>kheap := (kheap s)(ptr \<mapsto> obj)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s koa b. \<lbrakk>\<forall>a b. is_original_cap s (a, b) \<longrightarrow> (\<exists>sz fun. kheap s a = 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 a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> get tcb \<noteq> NullCap)); \<forall>tcb. obj \<noteq> TCB tcb; \<forall>n. \<not> is_cap_table n obj; kheap s ptr = Some koa; a_type obj = a_type koa; is_original_cap s (ptr, b)\<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) proof (prove)
goal (1 subgoal):
 1. \<And>s koa b. \<lbrakk>\<forall>tcb. obj \<noteq> TCB tcb; \<forall>n. \<not> is_cap_table n obj; kheap s ptr = Some koa; a_type obj = a_type koa; 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))\<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) proof (prove)
goal (2 subgoals):
 1. \<And>s koa b. \<lbrakk>\<forall>tcb. obj \<noteq> TCB tcb; \<forall>n. \<not> is_cap_table n obj; kheap s ptr = Some koa; a_type obj = a_type koa; 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)\<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 koa b. \<lbrakk>\<forall>tcb. obj \<noteq> TCB tcb; \<forall>n. \<not> is_cap_table n obj; kheap s ptr = Some koa; a_type obj = a_type koa; is_original_cap s (ptr, b); \<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) proof (prove)
goal (2 subgoals):
 1. \<And>s koa b. \<lbrakk>\<forall>tcb. obj \<noteq> TCB tcb; \<forall>n. \<not> is_cap_table n obj; kheap s ptr = Some koa; a_type obj = a_type koa; is_original_cap s (ptr, b); \<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)
 2. \<And>s koa b. \<lbrakk>\<forall>tcb. obj \<noteq> TCB tcb; \<forall>n. \<not> is_cap_table n obj; kheap s ptr = Some koa; a_type obj = a_type koa; 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)\<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) proof (prove)
goal (1 subgoal):
 1. \<And>s koa b. \<lbrakk>\<forall>tcb. obj \<noteq> TCB tcb; \<forall>n. \<not> is_cap_table n obj; kheap s ptr = Some koa; a_type obj = a_type koa; 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)\<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) proof (prove)
goal:
No subgoals!