theory PageTableDuplicates

lemma copyGlobalMappings_ksPSpace_same:
  notes blah[simp del] =  atLeastatMost_subset_iff atLeastLessThan_iff
          Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex
          atLeastAtMost_iff
  shows
  "\<lbrakk>is_aligned ptr pdBits\<rbrakk> \<Longrightarrow>
   \<lbrace>\<lambda>s. ksPSpace s x = ko \<and> pspace_distinct' s \<and> pspace_aligned' s \<and>
    is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ptr = armKSGlobalPD (ksArchState s)\<rbrace>
   copyGlobalMappings ptr
   \<lbrace>\<lambda>_ s. ksPSpace s x = ko\<rbrace>" apply (simp add:copyGlobalMappings_def) apply (rule hoare_name_pre_state) apply clarsimp apply (rule hoare_pre) apply wp apply (rule_tac Q = "\<lambda>r s'. ksPSpace s' x = ksPSpace s x \<and> globalPD = armKSGlobalPD (ksArchState s)"
      in hoare_post_imp) apply simp apply (wp hoare_vcg_all_lift getPDE_wp mapM_x_wp'
    | simp add: storePDE_def setObject_def split_def
    updateObject_default_def
    split: option.splits)+ apply (clarsimp simp:objBits_simps archObjSize_def) apply (clarsimp simp:obj_at'_def objBits_simps
      projectKO_def projectKO_opt_pde fail_def return_def
      split: Structures_H.kernel_object.splits
      arch_kernel_object.splits) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned ptr pdBits \<Longrightarrow> \<lbrace>\<lambda>s. ksPSpace s x = ko \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ptr = armKSGlobalPD (ksArchState s)\<rbrace> copyGlobalMappings ptr \<lbrace>\<lambda>_ s. ksPSpace s x = ko\<rbrace> proof (prove)
goal (1 subgoal):
 1. is_aligned ptr pdBits \<Longrightarrow> \<lbrace>\<lambda>s. ksPSpace s x = ko \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ptr = armKSGlobalPD (ksArchState s)\<rbrace> do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (ptr + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]
od \<lbrace>\<lambda>_ s. ksPSpace s x = ko\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>is_aligned ptr pdBits; ksPSpace s x = ko \<and> pspace_distinct' s \<and> pspace_aligned' s \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (ptr + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]
od \<lbrace>\<lambda>_ s. ksPSpace s x = ko\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (armKSGlobalPD (ksArchState s) + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]
od \<lbrace>\<lambda>_ sa. ksPSpace sa x = ksPSpace s x\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s\<rbrace> do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (armKSGlobalPD (ksArchState s) + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]
od \<lbrace>\<lambda>_ sa. ksPSpace sa x = ksPSpace s x\<rbrace>
 2. \<And>s sa. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); s = sa\<rbrakk> \<Longrightarrow> ?Q12 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s globalPD. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>?B16 s globalPD\<rbrace> mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (armKSGlobalPD (ksArchState s) + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<lbrace>\<lambda>_ sa. ksPSpace sa x = ksPSpace s x\<rbrace>
 2. \<And>s. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?B16 s\<rbrace>
 3. \<And>s sa. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); s = sa\<rbrakk> \<Longrightarrow> ?Q12 s sa proof (prove)
goal (4 subgoals):
 1. \<And>s globalPD rv sa. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); ksPSpace sa x = ksPSpace s x \<and> globalPD = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> ksPSpace sa x = ksPSpace s x
 2. \<And>s globalPD. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>?B16 s globalPD\<rbrace> mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (armKSGlobalPD (ksArchState s) + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<lbrace>\<lambda>r s'. ksPSpace s' x = ksPSpace s x \<and> globalPD = armKSGlobalPD (ksArchState s)\<rbrace>
 3. \<And>s. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?B16 s\<rbrace>
 4. \<And>s sa. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); s = sa\<rbrakk> \<Longrightarrow> ?Q12 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s globalPD. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>?B16 s globalPD\<rbrace> mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (armKSGlobalPD (ksArchState s) + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1] \<lbrace>\<lambda>r s'. ksPSpace s' x = ksPSpace s x \<and> globalPD = armKSGlobalPD (ksArchState s)\<rbrace>
 2. \<And>s. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?B16 s\<rbrace>
 3. \<And>s sa. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); s = sa\<rbrakk> \<Longrightarrow> ?Q12 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s xa sa. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); pptrBase >> 20 \<le> xa \<and> xa \<le> 2 ^ (pdBits - pdeBits) - 1; ksPSpace sa x = ksPSpace s x\<rbrakk> \<Longrightarrow> x = armKSGlobalPD (ksArchState s) + (xa << pdeBits) \<longrightarrow> (\<forall>ko. ko_at' ko (armKSGlobalPD (ksArchState s) + (xa << pdeBits)) sa \<longrightarrow> (\<exists>y. fst (lookupAround2 (armKSGlobalPD (ksArchState s) + (xa << pdeBits)) (ksPSpace sa)) = Some y) \<longrightarrow> armKSGlobalPD (ksArchState s) + (xa << pdeBits) = fst (the (fst (lookupAround2 (armKSGlobalPD (ksArchState s) + (xa << pdeBits)) (ksPSpace sa)))) \<longrightarrow> Some (KOArch (KOPDE ko)) = ksPSpace s (armKSGlobalPD (ksArchState s) + (xa << pdeBits)))
 2. \<And>s. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD s'. ksPSpace s' x = ksPSpace s x \<and> globalPD = armKSGlobalPD (ksArchState s)\<rbrace>
 3. \<And>s sa. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); s = sa\<rbrakk> \<Longrightarrow> ?Q12 s sa proof (prove)
goal (3 subgoals):
 1. \<And>s xa sa koa b. \<lbrakk>ko = Some b; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); ksPSpace sa (armKSGlobalPD (ksArchState s) + (xa << pdeBits)) = Some b; pptrBase >> 20 \<le> xa; xa \<le> 2 ^ (pdBits - pdeBits) - 1; ko_at' koa (armKSGlobalPD (ksArchState s) + (xa << pdeBits)) sa; ksPSpace s (armKSGlobalPD (ksArchState s) + (xa << pdeBits)) = Some b; x = armKSGlobalPD (ksArchState s) + (xa << pdeBits)\<rbrakk> \<Longrightarrow> KOArch (KOPDE koa) = b
 2. \<And>s. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD s'. ksPSpace s' x = ksPSpace s x \<and> globalPD = armKSGlobalPD (ksArchState s)\<rbrace>
 3. \<And>s sa. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); s = sa\<rbrakk> \<Longrightarrow> ?Q12 s sa proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s)\<rbrakk> \<Longrightarrow> \<lbrace>?Q12 s\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>globalPD s'. ksPSpace s' x = ksPSpace s x \<and> globalPD = armKSGlobalPD (ksArchState s)\<rbrace>
 2. \<And>s sa. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); s = sa\<rbrakk> \<Longrightarrow> ?Q12 s sa proof (prove)
goal (1 subgoal):
 1. \<And>s sa. \<lbrakk>ko = ksPSpace s x; pspace_distinct' s; pspace_aligned' s; is_aligned (armKSGlobalPD (ksArchState s)) pdBits; ptr = armKSGlobalPD (ksArchState s); s = sa\<rbrakk> \<Longrightarrow> ksPSpace sa x = ksPSpace s x \<and> (armKSGlobalPD \<circ> ksArchState) sa = armKSGlobalPD (ksArchState s) proof (prove)
goal:
No subgoals!