theory Retype_C

lemma createObject_untypedRange:
  assumes split:
    "\<lbrace>P\<rbrace> createObject ty ptr us dev
     \<lbrace>\<lambda>m s. (toAPIType ty = Some apiobject_type.Untyped \<longrightarrow>
                            Q {ptr..ptr + 2 ^ us - 1} s) \<and>
            (toAPIType ty \<noteq> Some apiobject_type.Untyped \<longrightarrow> Q {} s)\<rbrace>"
  shows "\<lbrace>P\<rbrace> createObject ty ptr us dev\<lbrace>\<lambda>m s. Q (untypedRange m) s\<rbrace>" including no_pre using split apply (simp add: createObject_def) apply (case_tac "toAPIType ty") apply (simp add: split | wp)+ apply (simp add: valid_def return_def bind_def split_def) apply (case_tac a, simp_all) apply (simp add: valid_def return_def simpler_gets_def simpler_modify_def
                       bind_def split_def curDomain_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace> proof (prove)
using this:
\<lbrace>P\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>m s. (toAPIType ty = Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {ptr..ptr + 2 ^ us - 1} s) \<and> (toAPIType ty \<noteq> Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {} s)\<rbrace>

goal (1 subgoal):
 1. \<lbrace>P\<rbrace> global.createObject ty ptr us dev \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>m s. (toAPIType ty = Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {ptr..ptr + 2 ^ us - 1} s) \<and> (toAPIType ty \<noteq> Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {} s)\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>m s. (toAPIType ty = Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {ptr..ptr + 2 ^ us - 1} s) \<and> (toAPIType ty \<noteq> Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {} s)\<rbrace>; toAPIType ty = None\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace>
 2. \<And>a. \<lbrakk>\<lbrace>P\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>m s. (toAPIType ty = Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {ptr..ptr + 2 ^ us - 1} s) \<and> (toAPIType ty \<noteq> Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {} s)\<rbrace>; toAPIType ty = Some a\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>\<lbrace>P\<rbrace> do archCap <- Arch.createObject ty ptr us dev;
return (capability.ArchObjectCap archCap)
od \<lbrace>\<lambda>m. Q {}\<rbrace>; toAPIType ty = None\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> Arch.createObject ty ptr us dev \<lbrace>\<lambda>archCap. Q {}\<rbrace>
 2. \<And>a. \<lbrakk>\<lbrace>P\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>m s. (toAPIType ty = Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {ptr..ptr + 2 ^ us - 1} s) \<and> (toAPIType ty \<noteq> Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {} s)\<rbrace>; toAPIType ty = Some a\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a. \<lbrakk>\<lbrace>P\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>m s. (toAPIType ty = Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {ptr..ptr + 2 ^ us - 1} s) \<and> (toAPIType ty \<noteq> Some ArchTypes_H.apiobject_type.Untyped \<longrightarrow> Q {} s)\<rbrace>; toAPIType ty = Some a\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> case toAPIType ty of None \<Rightarrow> do archCap <- Arch.createObject ty ptr us dev;
return $ capability.ArchObjectCap archCap
od | Some ArchTypes_H.apiobject_type.Untyped \<Rightarrow> return $ capability.UntypedCap dev (PPtr $ fromPPtr ptr) us 0 | Some ArchTypes_H.apiobject_type.TCBObject \<Rightarrow> do placeNewObject ptr makeObject 0;
curdom <- curDomain;
threadSet (tcbDomain_update (\<lambda>_. curdom)) (PPtr $ fromPPtr ptr);
return $ capability.ThreadCap (PPtr $ fromPPtr ptr)
od | Some ArchTypes_H.apiobject_type.EndpointObject \<Rightarrow> do placeNewObject ptr makeObject 0;
return $ capability.EndpointCap (PPtr $ fromPPtr ptr) 0 True True True True
od | Some ArchTypes_H.apiobject_type.NotificationObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject 0;
return $ capability.NotificationCap (PPtr $ fromPPtr ptr) 0 True True
od | Some ArchTypes_H.apiobject_type.CapTableObject \<Rightarrow> do placeNewObject (PPtr $ fromPPtr ptr) makeObject us;
modify (\<lambda>ks. ks\<lparr>gsCNodes := \<lambda>y. if y = fromPPtr ptr then Just us else gsCNodes ks y\<rparr>);
return $ capability.CNodeCap (PPtr $ fromPPtr ptr) us 0 0
od \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>\<lbrace>P\<rbrace> return (capability.UntypedCap dev ptr us 0) \<lbrace>\<lambda>m. Q {ptr..ptr + 2 ^ us - 1}\<rbrace>; toAPIType ty = Some ArchTypes_H.apiobject_type.Untyped; a = ArchTypes_H.apiobject_type.Untyped\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> return (capability.UntypedCap dev ptr us 0) \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace>
 2. \<And>a. \<lbrakk>\<lbrace>P\<rbrace> do y <- placeNewObject ptr makeObject 0;
curdom <- curDomain;
y <- threadSet (tcbDomain_update (\<lambda>_. curdom)) ptr;
return (capability.ThreadCap ptr)
od \<lbrace>\<lambda>m. Q {}\<rbrace>; toAPIType ty = Some ArchTypes_H.apiobject_type.TCBObject; a = ArchTypes_H.apiobject_type.TCBObject\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do y <- placeNewObject ptr makeObject 0;
curdom <- curDomain;
y <- threadSet (tcbDomain_update (\<lambda>_. curdom)) ptr;
return (capability.ThreadCap ptr)
od \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace>
 3. \<And>a. \<lbrakk>\<lbrace>P\<rbrace> do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od \<lbrace>\<lambda>m. Q {}\<rbrace>; toAPIType ty = Some ArchTypes_H.apiobject_type.EndpointObject; a = ArchTypes_H.apiobject_type.EndpointObject\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do y <- placeNewObject ptr makeObject 0;
return (capability.EndpointCap ptr 0 True True True True)
od \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace>
 4. \<And>a. \<lbrakk>\<lbrace>P\<rbrace> do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od \<lbrace>\<lambda>m. Q {}\<rbrace>; toAPIType ty = Some ArchTypes_H.apiobject_type.NotificationObject; a = ArchTypes_H.apiobject_type.NotificationObject\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do y <- placeNewObject ptr makeObject 0;
return (capability.NotificationCap ptr 0 True True)
od \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace>
 5. \<And>a. \<lbrakk>\<lbrace>P\<rbrace> do y <- placeNewObject ptr 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 \<lbrace>\<lambda>m. Q {}\<rbrace>; toAPIType ty = Some ArchTypes_H.apiobject_type.CapTableObject; a = ArchTypes_H.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> do y <- placeNewObject ptr 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 \<lbrace>\<lambda>m. Q (untypedRange m)\<rbrace> proof (prove)
goal:
No subgoals!