theory Detype_R

lemma createNewCaps_ret_len:
  "\<lbrace>K (n < 2 ^ word_bits \<and> n \<noteq> 0)\<rbrace>
   createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv s. n = length rv\<rbrace>" including no_pre apply (rule hoare_name_pre_state) apply clarsimp apply (case_tac ty) apply (simp_all add:createNewCaps_def ARM_H.toAPIType_def) apply (rule hoare_pre) apply wpc apply ((wp+)|simp add:Arch_createNewCaps_def ARM_H.toAPIType_def
           unat_of_nat_minus_1
           [where 'a=32, folded word_bits_def] |
          erule hoare_strengthen_post[OF createObjects_ret],clarsimp+ | intro conjI impI)+ apply (rule hoare_pre,
          ((wp+)
              | simp add: Arch_createNewCaps_def toAPIType_def
                          ARM_H.toAPIType_def unat_of_nat_minus_1
              | erule hoare_strengthen_post[OF createObjects_ret],clarsimp+
              | intro conjI impI)+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (n < 2 ^ word_bits \<and> n \<noteq> 0)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (n < 2 ^ word_bits \<and> n \<noteq> 0)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. K (n < 2 ^ word_bits \<and> n \<noteq> 0) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s x1. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = APIObjectType x1\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 2. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 3. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 4. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 5. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 6. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 7. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. n = length rv\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>s x1. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = APIObjectType x1\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 2. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 3. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 4. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 5. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 6. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 7. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>s x1. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = APIObjectType x1\<rbrakk> \<Longrightarrow> \<lbrace>?Q5 s x1\<rbrace> case x1 of ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] | ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od | ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od | ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od | ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 2. \<And>s x1 sa. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = APIObjectType x1; s = sa\<rbrakk> \<Longrightarrow> ?Q5 s x1 sa
 3. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 4. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 5. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 6. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 7. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 8. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace> proof (prove)
goal (12 subgoals):
 1. \<And>s x1. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>?R19 s x1\<rbrace> return $ map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ fromIntegral us) us 0) [0 .e. fromIntegral n - 1] \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 2. \<And>s x1. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>?R18 s x1\<rbrace> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
curdom <- curDomain;
mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return $ map capability.ThreadCap addrs
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 3. \<And>s x1. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>?R17 s x1\<rbrace> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 4. \<And>s x1. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>?R16 s x1\<rbrace> do addrs <- createObjects ptr n (injectKOS makeObject) 0;
return $ map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 5. \<And>s x1. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = APIObjectType x1; x1 = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>?R15 s x1\<rbrace> do addrs <- createObjects ptr n (injectKOS makeObject) us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr `~elem~` map fromPPtr addrs then Just us else gsCNodes ks addr\<rparr>);
return $ map (\<lambda>addr. capability.CNodeCap addr us 0 0) addrs
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 6. \<And>s x1 sa. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = APIObjectType x1; s = sa\<rbrakk> \<Longrightarrow> (x1 = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> ?R19 s x1 sa) \<and> (x1 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> ?R18 s x1 sa) \<and> (x1 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> ?R17 s x1 sa) \<and> (x1 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> ?R16 s x1 sa) \<and> (x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> ?R15 s x1 sa)
 7. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SmallPageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SmallPageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 8. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 9. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 10. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
A total of 12 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SmallPageObject; d\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> createObjects ptr n KOUserDataDevice 0 \<lbrace>\<lambda>addrs s. n = length addrs\<rbrace>
 2. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SmallPageObject; \<not> d\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do addrs <- createObjects ptr n KOUserData 0;
y <- modify (\<lambda>ks. ks\<lparr>gsUserPages := \<lambda>addr. if addr \<in> set addrs then Just ARMSmallPage else gsUserPages ks addr\<rparr>);
return (map (\<lambda>n. arch_capability.PageCap False n VMReadWrite ARMSmallPage None) addrs)
od \<lbrace>\<lambda>archCaps a. n = length archCaps\<rbrace>
 3. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = LargePageObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps LargePageObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 4. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 5. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = SuperSectionObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps SuperSectionObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 6. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = PageTableObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageTableObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace>
 7. \<And>s. \<lbrakk>n < 2 ^ word_bits; 0 < n; ty = PageDirectoryObject\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> do archCaps <- Arch_createNewCaps PageDirectoryObject ptr n us d;
return (map capability.ArchObjectCap archCaps)
od \<lbrace>\<lambda>rv s. n = length rv\<rbrace> proof (prove)
goal:
No subgoals!