theory KHeap_AI

lemma valid_cap_same_type:
  "\<lbrakk> s \<turnstile> cap; a_type k = a_type ko; kheap s p = Some ko \<rbrakk>
  \<Longrightarrow> s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr> \<turnstile> cap" apply (simp add: valid_cap_def split: cap.split) apply (auto elim!: typ_at_same_type untyped_same_type
               simp: ntfn_at_typ ep_at_typ tcb_at_typ cap_table_at_typ
              split: option.split sum.split) by (intro hoare_to_pure_kheap_upd[OF valid_arch_cap_typ, simplified obj_at_def],
      assumption, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> cap; a_type k = a_type ko; kheap s p = Some ko\<rbrakk> \<Longrightarrow> s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr> \<turnstile> cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap ac \<Rightarrow> valid_arch_cap ac s | _ \<Rightarrow> True); a_type k = a_type ko; kheap s p = Some ko\<rbrakk> \<Longrightarrow> (\<forall>x21 x22 x23 x24. cap = UntypedCap x21 x22 x23 x24 \<longrightarrow> valid_untyped (UntypedCap x21 x22 x23 x24) (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) \<and> untyped_min_bits \<le> x23 \<and> x24 \<le> 2 ^ x23 \<and> x22 \<noteq> 0) \<and> (\<forall>x31. (\<exists>x32 x33. cap = EndpointCap x31 x32 x33) \<longrightarrow> ep_at x31 (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)) \<and> (\<forall>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<longrightarrow> ntfn_at x41 (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) \<and> AllowGrant \<notin> x43 \<and> AllowGrantReply \<notin> x43) \<and> (\<forall>x51 x52 x53. cap = ReplyCap x51 x52 x53 \<longrightarrow> tcb_at x51 (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) \<and> AllowWrite \<in> x53 \<and> AllowRead \<notin> x53 \<and> AllowGrantReply \<notin> x53) \<and> (\<forall>x61 x62 x63. cap = CNodeCap x61 x62 x63 \<longrightarrow> cap_table_at x62 x61 (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) \<and> 0 < x62 \<and> length x63 \<le> word_bits) \<and> (\<forall>x7. cap = ThreadCap x7 \<longrightarrow> tcb_at x7 (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)) \<and> (\<forall>x10. cap = IRQHandlerCap x10 \<longrightarrow> x10 \<le> maxIRQ) \<and> (\<forall>x111 x112 x113. cap = Zombie x111 x112 x113 \<longrightarrow> (case x112 of None \<Rightarrow> tcb_at x111 (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) \<and> x113 \<le> 5 | Some b \<Rightarrow> cap_table_at b x111 (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>) \<and> x113 \<le> 2 ^ b \<and> b \<noteq> 0)) \<and> (\<forall>x12. cap = ArchObjectCap x12 \<longrightarrow> valid_arch_cap x12 (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>x12. \<lbrakk>a_type k = a_type ko; kheap s p = Some ko; cap_aligned (ArchObjectCap x12); valid_arch_cap x12 s; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> valid_arch_cap x12 (s\<lparr>kheap := (kheap s)(p \<mapsto> k)\<rparr>)