theory Detype_R

lemma copyGlobalMappings_gsUntypedZeroRanges_commute':
  "monad_commute \<top>
     (copyGlobalMappings ptr)
     (modify (\<lambda>s. s \<lparr> gsUntypedZeroRanges := f (gsUntypedZeroRanges s) \<rparr> ))" apply (simp add: copyGlobalMappings_def) apply (rule monad_commute_guard_imp) apply (rule commute_commute[OF monad_commute_split[where P="\<top>"]]) apply (rule mapM_x_commute[where f = id and P="\<top>\<top>"]) apply (simp add: storePDE_def getObject_def setObject_def cong: bind_cong) apply (strengthen monad_commute_guard_imp[OF monad_commute_split[where P="\<top>" and Q="\<top>\<top>"], OF _ _ hoare_vcg_prop]
         | simp add: modify_commute updateObject_default_def alignCheck_assert
                     magnitudeCheck_assert return_commute return_commute[THEN commute_commute]
                     projectKO_def2 assert_commute2 assert_commute2[THEN commute_commute]
                     assert_opt_def2 loadObject_default_def
              split: option.split prod.split)+ apply (simp add: monad_commute_def exec_gets exec_modify) apply wp apply (simp add: monad_commute_def exec_gets exec_modify) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (copyGlobalMappings ptr) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (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) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) proof (prove)
goal (2 subgoals):
 1. monad_commute ?P (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) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))
 2. \<And>s. True \<Longrightarrow> ?P s proof (prove)
goal (4 subgoals):
 1. \<And>r. monad_commute (?Q4 r) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (mapM_x (\<lambda>index. getObject (r + (index << pdeBits)) >>= storePDE (ptr + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1])
 2. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (gets (armKSGlobalPD \<circ> ksArchState))
 3. \<lbrace>?P'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>?Q4\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?P'4) s proof (prove)
goal (5 subgoals):
 1. \<And>r ra. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (getObject (r + (ra << pdeBits)) >>= storePDE (ptr + (ra << pdeBits)))
 2. \<And>r ra x. \<lbrace>(\<lambda>_. True) and K (id ra \<noteq> id x) and (\<lambda>_. True)\<rbrace> getObject (r + (x << pdeBits)) >>= storePDE (ptr + (x << pdeBits)) \<lbrace>\<lambda>v _. True\<rbrace>
 3. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (gets (armKSGlobalPD \<circ> ksArchState))
 4. \<lbrace>?P'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>r s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>r\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. True)\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?P'4) s proof (prove)
goal (5 subgoals):
 1. \<And>r ra. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (do v <- do v <- gets ksPSpace;
case lookupAround2 (r + (ra << pdeBits)) v of (before, after) \<Rightarrow> do (ptr', y) <- assert_opt before;
loadObject_default (r + (ra << pdeBits)) ptr' after y
od
od;
va <- gets ksPSpace;
case lookupAround2 (ptr + (ra << pdeBits)) va of (before, after) \<Rightarrow> do (ptr', obj) <- assert_opt before;
v <- updateObject_default v obj (ptr + (ra << pdeBits)) ptr' after;
modify (ksPSpace_update (\<lambda>_. va(ptr' \<mapsto> v)))
od
od)
 2. \<And>r ra x. \<lbrace>(\<lambda>_. True) and K (id ra \<noteq> id x) and (\<lambda>_. True)\<rbrace> getObject (r + (x << pdeBits)) >>= storePDE (ptr + (x << pdeBits)) \<lbrace>\<lambda>v _. True\<rbrace>
 3. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (gets (armKSGlobalPD \<circ> ksArchState))
 4. \<lbrace>?P'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>r s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>r\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. True)\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?P'4) s proof (prove)
goal (5 subgoals):
 1. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (gets ksPSpace)
 2. \<And>r ra x. \<lbrace>(\<lambda>_. True) and K (id ra \<noteq> id x) and (\<lambda>_. True)\<rbrace> getObject (r + (x << pdeBits)) >>= storePDE (ptr + (x << pdeBits)) \<lbrace>\<lambda>v _. True\<rbrace>
 3. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (gets (armKSGlobalPD \<circ> ksArchState))
 4. \<lbrace>?P'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>r s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>r\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. True)\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?P'4) s proof (prove)
goal (4 subgoals):
 1. \<And>r ra x. \<lbrace>(\<lambda>_. True) and K (id ra \<noteq> id x) and (\<lambda>_. True)\<rbrace> getObject (r + (x << pdeBits)) >>= storePDE (ptr + (x << pdeBits)) \<lbrace>\<lambda>v _. True\<rbrace>
 2. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (gets (armKSGlobalPD \<circ> ksArchState))
 3. \<lbrace>?P'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>r s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>r\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. True)\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?P'4) s proof (prove)
goal (3 subgoals):
 1. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (gets (armKSGlobalPD \<circ> ksArchState))
 2. \<lbrace>?P'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>r s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>r\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. True)\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?P'4) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'4\<rbrace> gets (armKSGlobalPD \<circ> ksArchState) \<lbrace>\<lambda>r s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>r\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. True)\<rbrace>
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?P'4) s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. distinct (map id [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]) \<and> (\<forall>r\<in>set [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]. True))) s proof (prove)
goal:
No subgoals!