theory Retype_R

lemma createObjects_untyped_ranges_zero':
  assumes moKO: "makeObjectKO dev ty = Some val"
  shows
  "\<lbrace>ct_active' and valid_pspace' and pspace_no_overlap' ptr sz
       and untyped_ranges_zero'
       and K (range_cover ptr sz (objBitsKO val + gSize) n \<and> n \<noteq> 0)\<rbrace>
     createObjects ptr n val gSize
   \<lbrace>\<lambda>_. untyped_ranges_zero'\<rbrace>" apply (rule hoare_gen_asm) apply (simp add: untyped_zero_ranges_cte_def iff_conv_conj_imp
                   createObjects_def) apply (simp only: imp_conv_disj not_all not_ex) apply (rule hoare_pre) apply (wp hoare_vcg_all_lift hoare_vcg_ex_lift hoare_vcg_conj_lift
             hoare_vcg_disj_lift createObjects_orig_cte_wp_at2'[where sz=sz]) apply (clarsimp simp: valid_pspace'_def) apply (cut_tac moKO[symmetric]) apply (simp add: makeObjectKO_def projectKO_opt_tcb projectKO_opt_cte
                   split: sum.split_asm kernel_object.split_asm
                          arch_kernel_object.split_asm
                          object_type.split_asm apiobject_type.split_asm) apply (simp add: makeObject_tcb tcb_cte_cases_def makeObject_cte
                    untypedZeroRange_def) apply (simp add: makeObject_cte untypedZeroRange_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active' and valid_pspace' and pspace_no_overlap' ptr sz and untyped_ranges_zero' and K (range_cover ptr sz (objBitsKO val + gSize) n \<and> n \<noteq> 0)\<rbrace> createObjects ptr n val gSize \<lbrace>\<lambda>_. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val + gSize) n \<and> n \<noteq> 0 \<Longrightarrow> \<lbrace>ct_active' and valid_pspace' and pspace_no_overlap' ptr sz and untyped_ranges_zero'\<rbrace> createObjects ptr n val gSize \<lbrace>\<lambda>_. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val + gSize) n \<and> 0 < n \<Longrightarrow> \<lbrace>ct_active' and valid_pspace' and pspace_no_overlap' ptr sz and (\<lambda>s. \<forall>a b. ((\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<longrightarrow> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<in> gsUntypedZeroRanges s \<longrightarrow> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s)))\<rbrace> do y <- createObjects' ptr n val gSize;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gSize)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>_ s. \<forall>a b. ((\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<longrightarrow> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<in> gsUntypedZeroRanges s \<longrightarrow> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (objBitsKO val + gSize) n \<and> 0 < n \<Longrightarrow> \<lbrace>ct_active' and valid_pspace' and pspace_no_overlap' ptr sz and (\<lambda>s. \<forall>a b. ((\<forall>p. \<not> cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<or> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<notin> gsUntypedZeroRanges s \<or> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s)))\<rbrace> do y <- createObjects' ptr n val gSize;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gSize)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>_ s. \<forall>a b. ((\<forall>p. \<not> cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<or> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<notin> gsUntypedZeroRanges s \<or> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (objBitsKO val + gSize) n \<and> 0 < n \<Longrightarrow> \<lbrace>?Q2\<rbrace> do y <- createObjects' ptr n val gSize;
return (map (\<lambda>n. ptr + (n << objBitsKO val + gSize)) [0 .e. word_of_nat n - 1])
od \<lbrace>\<lambda>_ s. \<forall>a b. ((\<forall>p. \<not> cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<or> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<notin> gsUntypedZeroRanges s \<or> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s))\<rbrace>
 2. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gSize) n \<and> 0 < n; (ct_active' and valid_pspace' and pspace_no_overlap' ptr sz and (\<lambda>s. \<forall>a b. ((\<forall>p. \<not> cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<or> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<notin> gsUntypedZeroRanges s \<or> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s)))) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>range_cover ptr sz (objBitsKO val + gSize) n \<and> 0 < n; (ct_active' and valid_pspace' and pspace_no_overlap' ptr sz and (\<lambda>s. \<forall>a b. ((\<forall>p. \<not> cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<or> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<notin> gsUntypedZeroRanges s \<or> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s)))) s\<rbrakk> \<Longrightarrow> \<forall>x xa. ((\<forall>xb. \<not> cte_wp_at' (\<lambda>a. untypedZeroRange (cteCap a) = Some (x, xa)) xb s \<and> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gSize) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> untypedZeroRange (cteCap a) = Some (x, xa)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some xb \<Rightarrow> ((\<lambda>a. untypedZeroRange (cteCap a) = Some (x, xa)) \<circ> getF) xb)) \<and> pspace_no_overlap' ptr sz s) \<or> (x, xa) \<in> gsUntypedZeroRanges s) \<and> ((x, xa) \<notin> gsUntypedZeroRanges s \<or> (\<exists>xb. cte_wp_at' (\<lambda>a. untypedZeroRange (cteCap a) = Some (x, xa)) xb s \<and> n \<noteq> 0 \<and> range_cover ptr sz (objBitsKO val + gSize) n \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> untypedZeroRange (cteCap a) = Some (x, xa)) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. \<not> (case projectKO_opt val of None \<Rightarrow> False | Some xb \<Rightarrow> ((\<lambda>a. untypedZeroRange (cteCap a) = Some (x, xa)) \<circ> getF) xb)) \<and> pspace_no_overlap' ptr sz s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>range_cover ptr sz (objBitsKO val + gSize) n; 0 < n; ct_active' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; pspace_no_overlap' ptr sz s; \<forall>a b. ((\<forall>p. \<not> cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<or> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<in> gsUntypedZeroRanges s \<longrightarrow> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s))\<rbrakk> \<Longrightarrow> ((\<forall>xb. \<not> cte_wp_at' (\<lambda>a. untypedZeroRange (cteCap a) = Some (x, xa)) xb s) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> untypedZeroRange (cteCap a) = Some (x, xa)) \<and> (\<forall>xb\<in>ran tcb_cte_cases. case xb of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> untypedZeroRange (cteCap (getF x2)) = Some (x, xa))) \<or> (x, xa) \<in> gsUntypedZeroRanges s) \<and> ((x, xa) \<in> gsUntypedZeroRanges s \<longrightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> untypedZeroRange (cteCap a) = Some (x, xa)) \<and> (\<forall>xb\<in>ran tcb_cte_cases. case xb of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> untypedZeroRange (cteCap (getF x2)) = Some (x, xa)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa. \<lbrakk>range_cover ptr sz (objBitsKO val + gSize) n; 0 < n; ct_active' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; pspace_no_overlap' ptr sz s; \<forall>a b. ((\<forall>p. \<not> cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<or> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<in> gsUntypedZeroRanges s \<longrightarrow> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s)); Some val = makeObjectKO dev ty\<rbrakk> \<Longrightarrow> ((\<forall>xb. \<not> cte_wp_at' (\<lambda>a. untypedZeroRange (cteCap a) = Some (x, xa)) xb s) \<and> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> untypedZeroRange (cteCap a) = Some (x, xa)) \<and> (\<forall>xb\<in>ran tcb_cte_cases. case xb of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> untypedZeroRange (cteCap (getF x2)) = Some (x, xa))) \<or> (x, xa) \<in> gsUntypedZeroRanges s) \<and> ((x, xa) \<in> gsUntypedZeroRanges s \<longrightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some a \<Rightarrow> untypedZeroRange (cteCap a) = Some (x, xa)) \<and> (\<forall>xb\<in>ran tcb_cte_cases. case xb of (getF, setF) \<Rightarrow> \<not> (case projectKO_opt val of None \<Rightarrow> False | Some x2 \<Rightarrow> untypedZeroRange (cteCap (getF x2)) = Some (x, xa)))) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa x2 x1. \<lbrakk>range_cover ptr sz (objBitsKO (KOTCB makeObject) + gSize) n; 0 < n; ct_active' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; pspace_no_overlap' ptr sz s; \<forall>a b. ((\<forall>p. \<not> cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<or> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<in> gsUntypedZeroRanges s \<longrightarrow> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s)); ty = Inr (APIObjectType ArchTypes_H.apiobject_type.TCBObject); x2 = APIObjectType ArchTypes_H.apiobject_type.TCBObject; x1 = ArchTypes_H.apiobject_type.TCBObject; val = KOTCB makeObject\<rbrakk> \<Longrightarrow> ((\<forall>xb. \<not> cte_wp_at' (\<lambda>a. untypedZeroRange (cteCap a) = Some (x, xa)) xb s) \<and> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. untypedZeroRange (cteCap (getF makeObject)) \<noteq> Some (x, xa)) \<or> (x, xa) \<in> gsUntypedZeroRanges s) \<and> ((x, xa) \<in> gsUntypedZeroRanges s \<longrightarrow> (\<forall>(getF, setF)\<in>ran tcb_cte_cases. untypedZeroRange (cteCap (getF makeObject)) \<noteq> Some (x, xa)))
 2. \<And>s x xa x2 x1. \<lbrakk>range_cover ptr sz (objBitsKO (KOCTE makeObject) + gSize) n; 0 < n; ct_active' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; pspace_no_overlap' ptr sz s; \<forall>a b. ((\<forall>p. \<not> cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<or> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<in> gsUntypedZeroRanges s \<longrightarrow> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s)); ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); x2 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; val = KOCTE makeObject\<rbrakk> \<Longrightarrow> ((\<forall>xb. \<not> cte_wp_at' (\<lambda>a. untypedZeroRange (cteCap a) = Some (x, xa)) xb s) \<and> untypedZeroRange (cteCap makeObject) \<noteq> Some (x, xa) \<or> (x, xa) \<in> gsUntypedZeroRanges s) \<and> ((x, xa) \<in> gsUntypedZeroRanges s \<longrightarrow> untypedZeroRange (cteCap makeObject) \<noteq> Some (x, xa)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa x2 x1. \<lbrakk>range_cover ptr sz (objBitsKO (KOCTE makeObject) + gSize) n; 0 < n; ct_active' s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; pspace_no_overlap' ptr sz s; \<forall>a b. ((\<forall>p. \<not> cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s) \<or> (a, b) \<in> gsUntypedZeroRanges s) \<and> ((a, b) \<in> gsUntypedZeroRanges s \<longrightarrow> (\<exists>p. cte_wp_at' (\<lambda>cte. untypedZeroRange (cteCap cte) = Some (a, b)) p s)); ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject); x2 = APIObjectType ArchTypes_H.apiobject_type.CapTableObject; x1 = ArchTypes_H.apiobject_type.CapTableObject; val = KOCTE makeObject\<rbrakk> \<Longrightarrow> ((\<forall>xb. \<not> cte_wp_at' (\<lambda>a. untypedZeroRange (cteCap a) = Some (x, xa)) xb s) \<and> untypedZeroRange (cteCap makeObject) \<noteq> Some (x, xa) \<or> (x, xa) \<in> gsUntypedZeroRanges s) \<and> ((x, xa) \<in> gsUntypedZeroRanges s \<longrightarrow> untypedZeroRange (cteCap makeObject) \<noteq> Some (x, xa)) proof (prove)
goal:
No subgoals!