theory CSpaceInv_AI

lemma set_cap_cap_refs_respects_device_region_NullCap:
  "\<lbrace>cap_refs_respects_device_region\<rbrace>
     set_cap NullCap p
   \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" apply (simp add: cap_refs_respects_device_region_def cap_range_respects_device_region_def) apply (rule hoare_pre) apply wps apply (simp add: cte_wp_at_caps_of_state ) apply (wp hoare_vcg_all_lift) apply (clarsimp simp: cap_range_def) apply (drule_tac x = x in spec) apply (drule_tac x = xa in spec) apply (clarsimp simp: cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cap_refs_respects_device_region\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>a b. \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> - dom (device_state (machine_state s)))) (a, b) s\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv s. \<forall>a b. \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> - dom (device_state (machine_state s)))) (a, b) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q35\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv s. \<forall>a b. \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> - dom (device_state (machine_state s)))) (a, b) s\<rbrace>
 2. \<And>s. \<forall>a b. \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> - dom (device_state (machine_state s)))) (a, b) s \<Longrightarrow> ?Q35 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P38 prev_s\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv s'. \<forall>a b. \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> dom (device_state (machine_state prev_s))) \<and> (\<not> cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> - dom (device_state (machine_state prev_s)))) (a, b) s'\<rbrace>
 2. \<And>s. \<forall>a b. \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> - dom (device_state (machine_state s)))) (a, b) s \<Longrightarrow> ?P38 s s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P38 prev_s\<rbrace> set_cap NullCap p \<lbrace>\<lambda>rv s'. \<forall>a b cap. caps_of_state s' (a, b) = Some cap \<longrightarrow> cap_is_device cap \<and> cap_range cap \<subseteq> dom (device_state (machine_state prev_s)) \<or> \<not> cap_is_device cap \<and> cap_range cap \<subseteq> - dom (device_state (machine_state prev_s))\<rbrace>
 2. \<And>s. \<forall>a b. \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> - dom (device_state (machine_state s)))) (a, b) s \<Longrightarrow> ?P38 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>a b. \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device c \<longrightarrow> \<not> cap_range c \<subseteq> - dom (device_state (machine_state s)))) (a, b) s \<Longrightarrow> \<forall>x xa xb. ((caps_of_state s)(p \<mapsto> NullCap)) (x, xa) = Some xb \<longrightarrow> cap_is_device xb \<and> cap_range xb \<subseteq> dom (device_state (machine_state s)) \<or> \<not> cap_is_device xb \<and> cap_range xb \<subseteq> - dom (device_state (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>\<forall>a b. \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> untyped_range c \<subseteq> dom (device_state (machine_state s)) \<longrightarrow> \<not> obj_refs c \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device c \<longrightarrow> untyped_range c \<subseteq> - dom (device_state (machine_state s)) \<longrightarrow> \<not> obj_refs c \<subseteq> - dom (device_state (machine_state s)))) (a, b) s; (x, xa) \<noteq> p; caps_of_state s (x, xa) = Some xb; untyped_range xb \<subseteq> - dom (device_state (machine_state s)) \<longrightarrow> cap_is_device xb \<or> \<not> obj_refs xb \<subseteq> - dom (device_state (machine_state s))\<rbrakk> \<Longrightarrow> cap_is_device xb \<and> untyped_range xb \<subseteq> dom (device_state (machine_state s)) \<and> obj_refs xb \<subseteq> dom (device_state (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>(x, xa) \<noteq> p; caps_of_state s (x, xa) = Some xb; untyped_range xb \<subseteq> - dom (device_state (machine_state s)) \<longrightarrow> cap_is_device xb \<or> \<not> obj_refs xb \<subseteq> - dom (device_state (machine_state s)); \<forall>b. \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> untyped_range c \<subseteq> dom (device_state (machine_state s)) \<longrightarrow> \<not> obj_refs c \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device c \<longrightarrow> untyped_range c \<subseteq> - dom (device_state (machine_state s)) \<longrightarrow> \<not> obj_refs c \<subseteq> - dom (device_state (machine_state s)))) (x, b) s\<rbrakk> \<Longrightarrow> cap_is_device xb \<and> untyped_range xb \<subseteq> dom (device_state (machine_state s)) \<and> obj_refs xb \<subseteq> dom (device_state (machine_state s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>(x, xa) \<noteq> p; caps_of_state s (x, xa) = Some xb; untyped_range xb \<subseteq> - dom (device_state (machine_state s)) \<longrightarrow> cap_is_device xb \<or> \<not> obj_refs xb \<subseteq> - dom (device_state (machine_state s)); \<not> cte_wp_at (\<lambda>c. (cap_is_device c \<longrightarrow> untyped_range c \<subseteq> dom (device_state (machine_state s)) \<longrightarrow> \<not> obj_refs c \<subseteq> dom (device_state (machine_state s))) \<and> (\<not> cap_is_device c \<longrightarrow> untyped_range c \<subseteq> - dom (device_state (machine_state s)) \<longrightarrow> \<not> obj_refs c \<subseteq> - dom (device_state (machine_state s)))) (x, xa) s\<rbrakk> \<Longrightarrow> cap_is_device xb \<and> untyped_range xb \<subseteq> dom (device_state (machine_state s)) \<and> obj_refs xb \<subseteq> dom (device_state (machine_state s)) proof (prove)
goal:
No subgoals!