theory KHeap_AI

lemma set_object_cap_refs_respects_device_region:
  "\<lbrace>cap_refs_respects_device_region and obj_at (same_caps ko) p\<rbrace>
  set_object p ko
  \<lbrace>\<lambda>r. cap_refs_respects_device_region\<rbrace>" apply (simp add: set_object_def, wp) apply (clarsimp simp: cap_refs_respects_device_region_def) apply (drule_tac x = a in spec) apply (drule_tac x = b in spec) apply (clarsimp simp: valid_refs_def cte_wp_at_after_update
    cap_range_respects_device_region_def) apply (erule notE) apply (erule cte_wp_at_weakenE) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region and obj_at (same_caps ko) p\<rbrace> set_object p ko \<lbrace>\<lambda>r. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (cap_refs_respects_device_region and obj_at (same_caps ko) p) s \<Longrightarrow> \<forall>koa. ko_at koa p s \<longrightarrow> a_type koa = a_type ko \<longrightarrow> cap_refs_respects_device_region (s\<lparr>kheap := (kheap s)(p \<mapsto> ko)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s koa a b. \<lbrakk>\<forall>a b. \<not> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) (a, b) s; obj_at (same_caps ko) p s; ko_at koa p s; a_type koa = a_type ko; cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)) (a, b) (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s koa a b. \<lbrakk>obj_at (same_caps ko) p s; ko_at koa p s; a_type koa = a_type ko; cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)) (a, b) (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>); \<forall>b. \<not> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s koa a b. \<lbrakk>obj_at (same_caps ko) p s; ko_at koa p s; a_type koa = a_type ko; cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>)) (a, b) (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>); \<not> cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c s) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s koa a b. \<lbrakk>obj_at (same_caps ko) p s; ko_at koa p s; a_type koa = a_type ko; cte_wp_at (\<lambda>c. \<not> (if cap_is_device c then cap_range c \<subseteq> dom (device_state (machine_state (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>))) else cap_range c \<subseteq> - dom (device_state (machine_state (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>))))) (a, b) s; \<not> cte_wp_at (\<lambda>c. \<not> (if cap_is_device c then cap_range c \<subseteq> dom (device_state (machine_state s)) else cap_range c \<subseteq> - dom (device_state (machine_state s)))) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s koa a b. \<lbrakk>obj_at (same_caps ko) p s; ko_at koa p s; a_type koa = a_type ko; cte_wp_at (\<lambda>c. \<not> (if cap_is_device c then cap_range c \<subseteq> dom (device_state (machine_state (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>))) else cap_range c \<subseteq> - dom (device_state (machine_state (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>))))) (a, b) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. \<not> (if cap_is_device c then cap_range c \<subseteq> dom (device_state (machine_state s)) else cap_range c \<subseteq> - dom (device_state (machine_state s)))) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s koa a b c. \<lbrakk>obj_at (same_caps ko) p s; ko_at koa p s; a_type koa = a_type ko; \<not> (if cap_is_device c then cap_range c \<subseteq> dom (device_state (machine_state (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>))) else cap_range c \<subseteq> - dom (device_state (machine_state (s\<lparr>kheap := \<lambda>a. if a = p then Some ko else kheap s a\<rparr>))))\<rbrakk> \<Longrightarrow> \<not> (if cap_is_device c then cap_range c \<subseteq> dom (device_state (machine_state s)) else cap_range c \<subseteq> - dom (device_state (machine_state s))) proof (prove)
goal:
No subgoals!