theory IsolatedThreadAction

lemma clearUntypedFreeIndex_isolatable:
  "thread_actions_isolatable idx (clearUntypedFreeIndex slot)" supply option.case_cong[cong] apply (simp add: clearUntypedFreeIndex_def getSlotCap_def) apply (rule thread_actions_isolatable_bind) apply (rule getCTE_isolatable) apply (simp split: capability.split, safe intro!: thread_actions_isolatable_return) apply (simp add: updateTrackedFreeIndex_def getSlotCap_def) apply (intro thread_actions_isolatable_bind getCTE_isolatable
                modify_isolatable) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (clearUntypedFreeIndex slot) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (clearUntypedFreeIndex slot) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do cte <- getCTE slot;
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex slot (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()
od) proof (prove)
goal (3 subgoals):
 1. thread_actions_isolatable idx (getCTE slot)
 2. \<And>x. thread_actions_isolatable idx (case cteCap x of capability.UntypedCap xa xaa xb xc \<Rightarrow> updateTrackedFreeIndex slot (maxFreeIndex (capBlockSize (cteCap x))) | _ \<Rightarrow> return ())
 3. \<And>t. \<lbrace>tcb_at' t\<rbrace> getCTE slot \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. thread_actions_isolatable idx (case cteCap x of capability.UntypedCap xa xaa xb xc \<Rightarrow> updateTrackedFreeIndex slot (maxFreeIndex (capBlockSize (cteCap x))) | _ \<Rightarrow> return ())
 2. \<And>t. \<lbrace>tcb_at' t\<rbrace> getCTE slot \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x x101 x102 x103 x104. cteCap x = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> thread_actions_isolatable idx (updateTrackedFreeIndex slot (max_free_index x103))
 2. \<And>t. \<lbrace>tcb_at' t\<rbrace> getCTE slot \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x x101 x102 x103 x104. cteCap x = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> thread_actions_isolatable idx (do cte <- getCTE slot;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. max_free_index x103) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od)
 2. \<And>t. \<lbrace>tcb_at' t\<rbrace> getCTE slot \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>x x101 x102 x103 x104 xa tsrs act s. \<lbrakk>cteCap x = capability.UntypedCap x101 x102 x103 x104; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap xa) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, ksSchedulerAction := act\<rparr>) = ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>ksSchedulerAction := act\<rparr>)\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap xa) of None \<Rightarrow> gsUntypedZeroRanges (ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>ksSchedulerAction := act\<rparr>)) | Some r \<Rightarrow> gsUntypedZeroRanges (ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>ksSchedulerAction := act\<rparr>)) - {r}\<rparr>
 2. \<And>x x101 x102 x103 x104 xa xb tsrs act s. \<lbrakk>cteCap x = capability.UntypedCap x101 x102 x103 x104; \<forall>x. tcb_at' (idx x) s\<rbrakk> \<Longrightarrow> ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. max_free_index x103) (cteCap xa)) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> insert r (gsUntypedZeroRanges s), ksSchedulerAction := act\<rparr>) = ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>ksSchedulerAction := act\<rparr>)\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. max_free_index x103) (cteCap xa)) of None \<Rightarrow> gsUntypedZeroRanges (ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>ksSchedulerAction := act\<rparr>)) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (ksPSpace_update (partial_overwrite idx tsrs) (s\<lparr>ksSchedulerAction := act\<rparr>)))\<rparr>
 3. \<And>x x101 x102 x103 x104 xa t. cteCap x = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>tcb_at' t\<rbrace> modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap xa) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 4. \<And>x x101 x102 x103 x104 t. cteCap x = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>tcb_at' t\<rbrace> getCTE slot \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 5. \<And>t. \<lbrace>tcb_at' t\<rbrace> getCTE slot \<lbrace>\<lambda>rv. tcb_at' t\<rbrace> proof (prove)
goal:
No subgoals!