theory Detype_R

lemma createTCBs_tcb_at':
  "\<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and>
   pspace_no_overlap' ptr sz s \<and>
   range_cover ptr sz
  (objBitsKO (KOTCB makeObject)) (Suc n) \<rbrace>
  createObjects' ptr (Suc n) (KOTCB makeObject) 0
  \<lbrace>\<lambda>rv s.
  (\<forall>x\<in>set [0.e.of_nat n]. tcb_at' (ptr + x * 2^tcbBlockSizeBits) s)\<rbrace>" apply (simp add:createObjects'_def split_def alignError_def) apply (wp unless_wp |wpc)+ apply (subst data_map_insert_def[symmetric])+ apply clarsimp apply (subgoal_tac "(\<forall>x\<le>of_nat n.
    tcb_at' (ptr + x * 2^tcbBlockSizeBits) (s\<lparr>ksPSpace :=
    foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject))
    (new_cap_addrs (Suc n) ptr (KOTCB makeObject))
    (ksPSpace s)\<rparr>))") apply (subst (asm) new_cap_addrs_def2) apply (drule range_cover.weak) apply simp apply simp apply (clarsimp simp: retype_obj_at_disj') apply (clarsimp simp: projectKO_opt_tcb) apply (clarsimp simp: new_cap_addrs_def image_def) apply (drule_tac x = "unat x" in bspec) apply (simp add:objBits_simps' shiftl_t2n) apply (rule unat_less_helper) apply (rule ccontr) apply simp apply (simp add: objBits_simps shiftl_t2n) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n)\<rbrace> createObjects' ptr (Suc n) (KOTCB makeObject) 0 \<lbrace>\<lambda>rv s. \<forall>x\<in>set [0 .e. word_of_nat n]. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n)\<rbrace> do y <- unless (ptr && mask (objBitsKO (KOTCB makeObject)) = 0) fail;
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. foldr (\<lambda>addr map. map(addr \<mapsto> KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) ps))
od \<lbrace>\<lambda>rv s. \<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n) \<Longrightarrow> (if ptr && mask (objBitsKO (KOTCB makeObject)) = 0 then \<lambda>s. (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>))) \<and> (\<forall>x. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = Some x \<longrightarrow> fst x < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr map. map(addr \<mapsto> KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>))) else (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n) \<Longrightarrow> (if ptr && mask (objBitsKO (KOTCB makeObject)) = 0 then \<lambda>s. (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>))) \<and> (\<forall>x. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = Some x \<longrightarrow> fst x < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>))) else (\<lambda>_. True)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>))) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; \<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (new_cap_addrs (Suc n) ptr (KOTCB makeObject)) (ksPSpace s)\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>)))
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0\<rbrakk> \<Longrightarrow> \<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (new_cap_addrs (Suc n) ptr (KOTCB makeObject)) (ksPSpace s)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0\<rbrakk> \<Longrightarrow> n < 2 ^ 32
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; \<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>)))
 3. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0\<rbrakk> \<Longrightarrow> \<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (new_cap_addrs (Suc n) ptr (KOTCB makeObject)) (ksPSpace s)\<rparr>) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr && mask (objBitsKO (KOTCB makeObject)) = 0; Suc n < 2 ^ LENGTH(32)\<rbrakk> \<Longrightarrow> n < 2 ^ 32
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; \<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>)))
 3. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0\<rbrakk> \<Longrightarrow> \<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (new_cap_addrs (Suc n) ptr (KOTCB makeObject)) (ksPSpace s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; \<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>)\<rbrakk> \<Longrightarrow> (fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = None \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>))) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + word_of_nat (shiftL (Suc n) (objBitsKO (KOTCB makeObject)) - Suc 0)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> (\<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (map (\<lambda>n. ptr + (n << objBitsKO (KOTCB makeObject))) [0 .e. word_of_nat n]) (ksPSpace s)\<rparr>)))
 2. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0\<rbrakk> \<Longrightarrow> \<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (new_cap_addrs (Suc n) ptr (KOTCB makeObject)) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0\<rbrakk> \<Longrightarrow> \<forall>x\<le>word_of_nat n. tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr (KOTCB makeObject)) (new_cap_addrs (Suc n) ptr (KOTCB makeObject)) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; x \<le> word_of_nat n; ptr + x * 2 ^ tcbBlockSizeBits \<in> set (new_cap_addrs (Suc n) ptr (KOTCB makeObject)) \<longrightarrow> projectKO_opt (KOTCB makeObject) = None\<rbrakk> \<Longrightarrow> tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; x \<le> word_of_nat n; ptr + x * 2 ^ tcbBlockSizeBits \<notin> set (new_cap_addrs (Suc n) ptr (KOTCB makeObject))\<rbrakk> \<Longrightarrow> tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; x \<le> word_of_nat n; x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat n << objBitsKO (KOTCB makeObject); \<forall>xa\<in>{0..<n}. x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat xa << objBitsKO (KOTCB makeObject)\<rbrakk> \<Longrightarrow> tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; x \<le> word_of_nat n; x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat n << objBitsKO (KOTCB makeObject)\<rbrakk> \<Longrightarrow> unat x \<in> {0..<n}
 2. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; x \<le> word_of_nat n; x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat n << objBitsKO (KOTCB makeObject); x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat (unat x) << objBitsKO (KOTCB makeObject)\<rbrakk> \<Longrightarrow> tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz 9 (Suc n); ptr && mask 9 = 0; x \<le> word_of_nat n; x * 0x200 \<noteq> 0x200 * word_of_nat n\<rbrakk> \<Longrightarrow> unat x < n
 2. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; x \<le> word_of_nat n; x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat n << objBitsKO (KOTCB makeObject); x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat (unat x) << objBitsKO (KOTCB makeObject)\<rbrakk> \<Longrightarrow> tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz 9 (Suc n); ptr && mask 9 = 0; x \<le> word_of_nat n; x * 0x200 \<noteq> 0x200 * word_of_nat n\<rbrakk> \<Longrightarrow> x < word_of_nat n
 2. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; x \<le> word_of_nat n; x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat n << objBitsKO (KOTCB makeObject); x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat (unat x) << objBitsKO (KOTCB makeObject)\<rbrakk> \<Longrightarrow> tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) s proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz 9 (Suc n); ptr && mask 9 = 0; x \<le> word_of_nat n; x * 0x200 \<noteq> 0x200 * word_of_nat n; \<not> x < word_of_nat n\<rbrakk> \<Longrightarrow> False
 2. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; x \<le> word_of_nat n; x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat n << objBitsKO (KOTCB makeObject); x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat (unat x) << objBitsKO (KOTCB makeObject)\<rbrakk> \<Longrightarrow> tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) s proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO (KOTCB makeObject)) (Suc n); ptr && mask (objBitsKO (KOTCB makeObject)) = 0; x \<le> word_of_nat n; x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat n << objBitsKO (KOTCB makeObject); x * 2 ^ tcbBlockSizeBits \<noteq> word_of_nat (unat x) << objBitsKO (KOTCB makeObject)\<rbrakk> \<Longrightarrow> tcb_at' (ptr + x * 2 ^ tcbBlockSizeBits) s proof (prove)
goal:
No subgoals!