theory Finalise_R

lemma emptySlot_valid_global_refs[wp]:
  "\<lbrace>valid_global_refs' and cte_at' sl\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" apply (simp add: valid_global_refs'_def global_refs'_def) apply (rule hoare_pre) apply (rule hoare_use_eq_irq_node' [OF emptySlot_irq_node']) apply (rule hoare_use_eq [where f=ksArchState, OF emptySlot_ksArch]) apply (rule hoare_use_eq [where f=ksIdleThread, OF emptySlot_ksIdle]) apply (rule hoare_use_eq [where f=gsMaxObjectSize], wp) apply (simp add: valid_refs'_cteCaps valid_cap_sizes_cteCaps) apply (rule emptySlot_cteCaps_of) apply (clarsimp simp: cte_wp_at_ctes_of) apply (frule(1) cte_at_valid_cap_sizes_0) apply (clarsimp simp: valid_refs'_cteCaps valid_cap_sizes_cteCaps ball_ran_eq) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs' and cte_wp_at' (\<lambda>_. True) sl\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)) and cte_wp_at' (\<lambda>_. True) sl\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)\<rbrace>
 2. \<And>s. ((\<lambda>s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)) and cte_wp_at' (\<lambda>_. True) sl) s \<Longrightarrow> ?Q4 s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P7 f\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. f + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)\<rbrace>
 2. \<And>s. ((\<lambda>s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)) and cte_wp_at' (\<lambda>_. True) sl) s \<Longrightarrow> ?P7 (irq_node' s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa. \<lbrace>?P17 f fa\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD fa) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs fa)) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. f + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)\<rbrace>
 2. \<And>s. ((\<lambda>s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)) and cte_wp_at' (\<lambda>_. True) sl) s \<Longrightarrow> ?P17 (irq_node' s) (ksArchState s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa fb. \<lbrace>?P28 f fa fb\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> fb \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD fa) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs fa)) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. f + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)\<rbrace>
 2. \<And>s. ((\<lambda>s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)) and cte_wp_at' (\<lambda>_. True) sl) s \<Longrightarrow> ?P28 (irq_node' s) (ksArchState s) (ksIdleThread s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa fb fc. \<lbrace>?P39 f fa fb fc\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> fb \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD fa) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs fa)) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. f + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' fc (ctes_of s)\<rbrace>
 2. \<And>s. ((\<lambda>s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)) and cte_wp_at' (\<lambda>_. True) sl) s \<Longrightarrow> ?P39 (irq_node' s) (ksArchState s) (ksIdleThread s) (gsMaxObjectSize s) s proof (prove)
goal (2 subgoals):
 1. \<And>f fa fb fc. \<lbrace>?P39 f fa fb fc\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. (\<forall>c\<in>ran (cteCaps_of s). ARM.kernel_data_refs \<inter> capRange c = {}) \<and> fb \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD fa) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs fa)) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. f + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> (\<forall>c\<in>ran (cteCaps_of s). 2 ^ capBits c \<le> fc)\<rbrace>
 2. \<And>s. ((\<lambda>s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)) and cte_wp_at' (\<lambda>_. True) sl) s \<Longrightarrow> ?P39 (irq_node' s) (ksArchState s) (ksIdleThread s) (gsMaxObjectSize s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. valid_refs' ARM.kernel_data_refs (ctes_of s) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)) and cte_wp_at' (\<lambda>_. True) sl) s \<Longrightarrow> (\<forall>c\<in>ran ((cteCaps_of s)(sl \<mapsto> capability.NullCap)). ARM.kernel_data_refs \<inter> capRange c = {}) \<and> ksIdleThread s \<in> ARM.kernel_data_refs \<and> page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs \<and> \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs \<and> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs \<and> (\<forall>c\<in>ran ((cteCaps_of s)(sl \<mapsto> capability.NullCap)). 2 ^ capBits c \<le> gsMaxObjectSize s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_refs' ARM.kernel_data_refs (ctes_of s); ksIdleThread s \<in> ARM.kernel_data_refs; page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs; \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); ctes_of s sl = Some cte\<rbrakk> \<Longrightarrow> (\<forall>c\<in>ran (\<lambda>a. if a = sl then Some capability.NullCap else cteCaps_of s a). ARM.kernel_data_refs \<inter> capRange c = {}) \<and> (\<forall>c\<in>ran (\<lambda>a. if a = sl then Some capability.NullCap else cteCaps_of s a). 2 ^ capBits c \<le> gsMaxObjectSize s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_refs' ARM.kernel_data_refs (ctes_of s); ksIdleThread s \<in> ARM.kernel_data_refs; page_directory_refs' (ARM_H.armKSGlobalPD (ksArchState s)) \<subseteq> ARM.kernel_data_refs; \<Union> (page_table_refs' ` set (ARM_H.armKSGlobalPTs (ksArchState s))) \<subseteq> ARM.kernel_data_refs; range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits)) \<subseteq> ARM.kernel_data_refs; valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s); ctes_of s sl = Some cte; 0 < gsMaxObjectSize s\<rbrakk> \<Longrightarrow> (\<forall>c\<in>ran (\<lambda>a. if a = sl then Some capability.NullCap else cteCaps_of s a). ARM.kernel_data_refs \<inter> capRange c = {}) \<and> (\<forall>c\<in>ran (\<lambda>a. if a = sl then Some capability.NullCap else cteCaps_of s a). 2 ^ capBits c \<le> gsMaxObjectSize s) proof (prove)
goal:
No subgoals!