theory Detype_R

lemma createObject_gsUntypedZeroRanges_commute:
  "monad_commute
     \<top>
     (RetypeDecls_H.createObject ty ptr us dev)
     (modify (\<lambda>s. s \<lparr> gsUntypedZeroRanges := f (gsUntypedZeroRanges s) \<rparr> ))" apply (simp add: createObject_def ARM_H.createObject_def
                   placeNewDataObject_def
                   placeNewObject_def2 bind_assoc fail_commute
                   return_commute toAPIType_def
    split: option.split apiobject_type.split object_type.split) apply (strengthen monad_commute_guard_imp[OF monad_commute_split[where P="\<top>" and Q="\<top>\<top>"],
          OF _ _ hoare_vcg_prop, THEN commute_commute]
      monad_commute_guard_imp[OF monad_commute_split[where P="\<top>" and Q="\<top>\<top>"],
          OF _ _ hoare_vcg_prop]
     | simp add: modify_commute createObjects_gsUntypedZeroRanges_commute'
                 createObjects_gsUntypedZeroRanges_commute'[THEN commute_commute]
                 return_commute return_commute[THEN commute_commute]
                 threadSet_gsUntypedZeroRanges_commute'[THEN commute_commute]
                 doMachineOp_modify_commute[THEN commute_commute]
                 copyGlobalMappings_gsUntypedZeroRanges_commute'[THEN commute_commute]
          split: option.split prod.split cong: if_cong)+ apply (simp add: curDomain_def monad_commute_def exec_modify exec_gets) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (global.createObject ty ptr us dev) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. (dev \<longrightarrow> (\<forall>x1. ty = APIObjectType x1 \<longrightarrow> (\<forall>x2. (x2 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> x1 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> monad_commute (\<lambda>_. True) (do y <- createObjects' ptr (Suc 0) (KOTCB makeObject) 0;
curdom <- curDomain;
y <- threadSet (tcbDomain_update (\<lambda>_. curdom)) ptr;
return (capability.ThreadCap ptr)
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (x2 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> x1 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> monad_commute (\<lambda>_. True) (do y <- createObjects' ptr (Suc 0) (KOEndpoint makeObject) 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (x2 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> x1 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> monad_commute (\<lambda>_. True) (do y <- createObjects' ptr (Suc 0) (KONotification makeObject) 0;
return (capability.NotificationCap ptr 0 True True)
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (x2 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> monad_commute (\<lambda>_. True) (do y <- createObjects' ptr (Suc 0) (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))))) \<and> (ty = SmallPageObject \<longrightarrow> monad_commute (\<lambda>_. True) (do x <- createObjects' ptr (Suc 0) KOUserDataDevice 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>y. if y = ptr then Just ARMSmallPage else gsUserPages ks y\<rparr>);
return (capability.ArchObjectCap (arch_capability.PageCap True ptr VMReadWrite ARMSmallPage None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (ty = LargePageObject \<longrightarrow> monad_commute (\<lambda>_. True) (do x <- createObjects' ptr (Suc 0) KOUserDataDevice 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>y. if y = ptr then Just ARMLargePage else gsUserPages ks y\<rparr>);
return (capability.ArchObjectCap (arch_capability.PageCap True ptr VMReadWrite ARMLargePage None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (ty = SectionObject \<longrightarrow> monad_commute (\<lambda>_. True) (do x <- createObjects' ptr (Suc 0) KOUserDataDevice 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>y. if y = ptr then Just ARMSection else gsUserPages ks y\<rparr>);
return (capability.ArchObjectCap (arch_capability.PageCap True ptr VMReadWrite ARMSection None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (ty = SuperSectionObject \<longrightarrow> monad_commute (\<lambda>_. True) (do x <- createObjects' ptr (Suc 0) KOUserDataDevice 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>y. if y = ptr then Just ARMSuperSection else gsUserPages ks y\<rparr>);
return (capability.ArchObjectCap (arch_capability.PageCap True ptr VMReadWrite ARMSuperSection None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (ty = PageTableObject \<longrightarrow> monad_commute (\<lambda>_. True) (do y <- createObjects' ptr (Suc 0) (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (capability.ArchObjectCap (arch_capability.PageTableCap ptr None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (ty = PageDirectoryObject \<longrightarrow> monad_commute (\<lambda>_. True) (do x <- createObjects' ptr (Suc 0) (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
x <- copyGlobalMappings ptr;
y <- doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ pdBits - 1) (addrFromPPtr ptr));
return (capability.ArchObjectCap (arch_capability.PageDirectoryCap ptr None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)))) \<and> (\<not> dev \<longrightarrow> (\<forall>x1. ty = APIObjectType x1 \<longrightarrow> (\<forall>x2. (x2 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> x1 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> monad_commute (\<lambda>_. True) (do y <- createObjects' ptr (Suc 0) (KOTCB makeObject) 0;
curdom <- curDomain;
y <- threadSet (tcbDomain_update (\<lambda>_. curdom)) ptr;
return (capability.ThreadCap ptr)
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (x2 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> x1 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> monad_commute (\<lambda>_. True) (do y <- createObjects' ptr (Suc 0) (KOEndpoint makeObject) 0;
return (capability.EndpointCap ptr 0 True True True True)
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (x2 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> x1 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> monad_commute (\<lambda>_. True) (do y <- createObjects' ptr (Suc 0) (KONotification makeObject) 0;
return (capability.NotificationCap ptr 0 True True)
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (x2 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> monad_commute (\<lambda>_. True) (do y <- createObjects' ptr (Suc 0) (KOCTE makeObject) us;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = ptr then Just us else gsCNodes ks y\<rparr>);
return (capability.CNodeCap ptr us 0 0)
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))))) \<and> (ty = SmallPageObject \<longrightarrow> monad_commute (\<lambda>_. True) (do x <- createObjects' ptr (Suc 0) KOUserData 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>y. if y = ptr then Just ARMSmallPage else gsUserPages ks y\<rparr>);
return (capability.ArchObjectCap (arch_capability.PageCap False ptr VMReadWrite ARMSmallPage None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (ty = LargePageObject \<longrightarrow> monad_commute (\<lambda>_. True) (do x <- createObjects' ptr (Suc 0) KOUserData 4;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>y. if y = ptr then Just ARMLargePage else gsUserPages ks y\<rparr>);
return (capability.ArchObjectCap (arch_capability.PageCap False ptr VMReadWrite ARMLargePage None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (ty = SectionObject \<longrightarrow> monad_commute (\<lambda>_. True) (do x <- createObjects' ptr (Suc 0) KOUserData 8;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>y. if y = ptr then Just ARMSection else gsUserPages ks y\<rparr>);
return (capability.ArchObjectCap (arch_capability.PageCap False ptr VMReadWrite ARMSection None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (ty = SuperSectionObject \<longrightarrow> monad_commute (\<lambda>_. True) (do x <- createObjects' ptr (Suc 0) KOUserData 12;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>y. if y = ptr then Just ARMSuperSection else gsUserPages ks y\<rparr>);
return (capability.ArchObjectCap (arch_capability.PageCap False ptr VMReadWrite ARMSuperSection None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (ty = PageTableObject \<longrightarrow> monad_commute (\<lambda>_. True) (do y <- createObjects' ptr (Suc 0) (KOArch (KOPTE makeObject)) (ptBits - objBits makeObject);
return (capability.ArchObjectCap (arch_capability.PageTableCap ptr None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>))) \<and> (ty = PageDirectoryObject \<longrightarrow> monad_commute (\<lambda>_. True) (do x <- createObjects' ptr (Suc 0) (KOArch (KOPDE makeObject)) (pdBits - objBits makeObject);
x <- copyGlobalMappings ptr;
y <- doMachineOp (cleanCacheRange_PoU ptr (ptr + 2 ^ pdBits - 1) (addrFromPPtr ptr));
return (capability.ArchObjectCap (arch_capability.PageDirectoryCap ptr None))
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)))) proof (prove)
goal (1 subgoal):
 1. ty = APIObjectType ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) curDomain proof (prove)
goal:
No subgoals!