theory Untyped_R

lemma createNewCaps_not_isZombie[wp]:
  "\<lbrace>\<top>\<rbrace> createNewCaps ty ptr bits sz d \<lbrace>\<lambda>rv s. (\<forall>cap \<in> set rv. \<not> isZombie cap)\<rbrace>" apply (simp add: createNewCaps_def toAPIType_def ARM_H.toAPIType_def
                   createNewCaps_def
              split del: if_split cong: option.case_cong if_cong
                                        apiobject_type.case_cong
                                        ARM_H.object_type.case_cong) apply (rule hoare_pre) apply (wp undefined_valid | wpc
            | simp add: isCap_simps)+ apply auto? done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> createNewCaps ty ptr bits sz d \<lbrace>\<lambda>rv s. \<forall>cap\<in>set rv. \<not> isZombie cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> case case ty of APIObjectType a \<Rightarrow> Some a | _ \<Rightarrow> None of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr bits sz d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return (map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ sz) sz 0) [0 .e. word_of_nat bits - 1]) | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr bits (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr bits (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr bits (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr bits (KOCTE makeObject) sz;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Some sz else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr sz 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<forall>cap\<in>set rv. \<not> isZombie cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q13\<rbrace> case case ty of APIObjectType a \<Rightarrow> Some a | _ \<Rightarrow> None of None \<Rightarrow> do archCaps <- Arch_createNewCaps ty ptr bits sz d;
return (map capability.ArchObjectCap archCaps)
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return (map (\<lambda>n. capability.UntypedCap d (ptr + n * 2 ^ sz) sz 0) [0 .e. word_of_nat bits - 1]) | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do addrs <- createObjects ptr bits (KOTCB makeObject) 0;
curdom <- curDomain;
y <- mapM_x (threadSet (tcbDomain_update (\<lambda>_. curdom))) addrs;
return (map capability.ThreadCap addrs)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do addrs <- createObjects ptr bits (KOEndpoint makeObject) 0;
return (map (\<lambda>addr. capability.EndpointCap addr 0 True True True True) addrs)
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do addrs <- createObjects ptr bits (KONotification makeObject) 0;
return (map (\<lambda>addr. capability.NotificationCap addr 0 True True) addrs)
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do addrs <- createObjects ptr bits (KOCTE makeObject) sz;
y <- modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>addr. if addr \<in> set addrs then Some sz else gsCNodes ks addr\<rparr>);
return (map (\<lambda>addr. capability.CNodeCap addr sz 0 0) addrs)
od \<lbrace>\<lambda>rv s. \<forall>cap\<in>set rv. \<not> isZombie cap\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q13 s proof (prove)
goal:
No subgoals! proof (prove)
goal:
No subgoals!