theory Untyped_R

lemma resetUntypedCap_st_tcb_at':
  "\<lbrace>invs' and st_tcb_at' (P and ((\<noteq>) Inactive) and ((\<noteq>) IdleThreadState)) t
      and cte_wp_at' (\<lambda>cp. isUntypedCap (cteCap cp)) slot
      and ct_active' and sch_act_simple and (\<lambda>s. descendants_of' slot (ctes_of s) = {})\<rbrace>
    resetUntypedCap slot
  \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps) apply (simp add: resetUntypedCap_def) apply (rule hoare_pre) apply (wp mapME_x_inv_wp preemptionPoint_inv
             deleteObjects_st_tcb_at'[where p=slot] getSlotCap_wp
           | simp add: unless_def
           | wp (once) hoare_drop_imps)+ apply (clarsimp simp: cte_wp_at_ctes_of) apply (strengthen refl) apply (rule exI, strengthen refl) apply (frule cte_wp_at_valid_objs_valid_cap'[OF ctes_of_cte_wpD], clarsimp+) apply (clarsimp simp: valid_cap_simps' capAligned_def empty_descendants_range_in'
                        descendants_range'_def2
                 elim!: pred_tcb'_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t and cte_wp_at' (\<lambda>cp. isUntypedCap (cteCap cp)) slot and ct_active' and sch_act_simple and (\<lambda>s. descendants_of' slot (ctes_of s) = {})\<rbrace> resetUntypedCap slot \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t and cte_wp_at' (\<lambda>cp. isUntypedCap (cteCap cp)) slot and ct_active' and sch_act_simple and (\<lambda>s. descendants_of' slot (ctes_of s) = {})) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> resetUntypedCap slot \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>invs' s; st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t s; ct_active' s; ctes_of s slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; sch_act_simple s; descendants_of' slot (ctes_of s) = {}\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> resetUntypedCap slot \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>invs' s; st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t s; ct_active' s; ctes_of s slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; sch_act_simple s; descendants_of' slot (ctes_of s) = {}\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> doE cap <- liftE (getSlotCap slot);
unlessE (capFreeIndex cap = 0) (doE y <- liftE (deleteObjects (capPtr cap) (capBlockSize cap));
if capIsDevice cap \<or> capBlockSize cap < resetChunkBits then withoutPreemption $ do unless (capIsDevice cap) $ doMachineOp $ clearMemory (PPtr (fromPPtr (capPtr cap))) (1 `~shiftL~` capBlockSize cap);
updateFreeIndex slot 0
od else forME_x (reverse [capPtr cap , capPtr cap + 1 `~shiftL~` resetChunkBits .e. getFreeRef (capPtr cap) (capFreeIndex cap) - 1]) (\<lambda>addr. doE withoutPreemption $ doMachineOp $ clearMemory (PPtr (fromPPtr addr)) (1 `~shiftL~` resetChunkBits);
withoutPreemption $ updateFreeIndex slot (getFreeIndex (capPtr cap) addr);
preemptionPoint
odE)
odE)
odE \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s cte d v0 v1 f. \<lbrakk>invs' s; st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t s; ct_active' s; ctes_of s slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; sch_act_simple s; descendants_of' slot (ctes_of s) = {}\<rbrakk> \<Longrightarrow> \<lbrace>?Q13 s cte d v0 v1 f\<rbrace> doE cap <- liftE (getSlotCap slot);
unlessE (capFreeIndex cap = 0) (doE y <- liftE (deleteObjects (capPtr cap) (capBlockSize cap));
if capIsDevice cap \<or> capBlockSize cap < resetChunkBits then withoutPreemption $ do unless (capIsDevice cap) $ doMachineOp $ clearMemory (PPtr (fromPPtr (capPtr cap))) (1 `~shiftL~` capBlockSize cap);
updateFreeIndex slot 0
od else forME_x (reverse [capPtr cap , capPtr cap + 1 `~shiftL~` resetChunkBits .e. getFreeRef (capPtr cap) (capFreeIndex cap) - 1]) (\<lambda>addr. doE withoutPreemption $ doMachineOp $ clearMemory (PPtr (fromPPtr addr)) (1 `~shiftL~` resetChunkBits);
withoutPreemption $ updateFreeIndex slot (getFreeIndex (capPtr cap) addr);
preemptionPoint
odE)
odE)
odE \<lbrace>\<lambda>_. st_tcb_at' P t\<rbrace>
 2. \<And>s cte d v0 v1 f sa. \<lbrakk>invs' s; st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t s; ct_active' s; ctes_of s slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; sch_act_simple s; descendants_of' slot (ctes_of s) = {}; s = sa\<rbrakk> \<Longrightarrow> ?Q13 s cte d v0 v1 f sa proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f sa. \<lbrakk>invs' sa; st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t sa; ct_active' sa; ctes_of sa slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; sch_act_simple sa; descendants_of' slot (ctes_of sa) = {}; s = sa\<rbrakk> \<Longrightarrow> \<exists>cap. (capFreeIndex cap = 0 \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = cap) slot sa \<and> st_tcb_at' P t sa) \<and> (0 < capFreeIndex cap \<longrightarrow> cte_wp_at' (\<lambda>c. cteCap c = cap) slot sa \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d80 sa cte d v0 v1 f cap) (capPtr cap) (capBlockSize cap) (?idx80 sa cte d v0 v1 f cap)) slot sa \<and> descendants_range' (capability.UntypedCap (?d80 sa cte d v0 v1 f cap) (capPtr cap) (capBlockSize cap) (?idx80 sa cte d v0 v1 f cap)) slot (ctes_of sa) \<and> capBlockSize cap < word_bits \<and> is_aligned (capPtr cap) (capBlockSize cap) \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d87 sa cte d v0 v1 f cap) (capPtr cap) (capBlockSize cap) (?idx87 sa cte d v0 v1 f cap)) slot sa \<and> descendants_range' (capability.UntypedCap (?d87 sa cte d v0 v1 f cap) (capPtr cap) (capBlockSize cap) (?idx87 sa cte d v0 v1 f cap)) slot (ctes_of sa) \<and> capBlockSize cap < word_bits \<and> is_aligned (capPtr cap) (capBlockSize cap) \<and> cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap (?d93 sa cte d v0 v1 f cap) (capPtr cap) (capBlockSize cap) (?idx93 sa cte d v0 v1 f cap)) slot sa \<and> descendants_range' (capability.UntypedCap (?d93 sa cte d v0 v1 f cap) (capPtr cap) (capBlockSize cap) (?idx93 sa cte d v0 v1 f cap)) slot (ctes_of sa) \<and> capBlockSize cap < word_bits \<and> is_aligned (capPtr cap) (capBlockSize cap)) proof (prove)
goal (1 subgoal):
 1. \<And>cte d v0 v1 f sa. \<lbrakk>invs' sa; st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t sa; ct_active' sa; ctes_of sa slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; sch_act_simple sa; descendants_of' slot (ctes_of sa) = {}\<rbrakk> \<Longrightarrow> \<exists>cap. (capFreeIndex cap = 0 \<longrightarrow> capability.UntypedCap d v0 v1 f = cap \<and> st_tcb_at' P t sa) \<and> (0 < capFreeIndex cap \<longrightarrow> capability.UntypedCap d v0 v1 f = cap \<and> d = ?d80 sa cte d v0 v1 f cap \<and> v0 = capPtr cap \<and> v1 = capBlockSize cap \<and> f = ?idx80 sa cte d v0 v1 f cap \<and> descendants_range' (capability.UntypedCap (?d80 sa cte d v0 v1 f cap) (capPtr cap) (capBlockSize cap) (?idx80 sa cte d v0 v1 f cap)) slot (ctes_of sa) \<and> capBlockSize cap < word_bits \<and> is_aligned (capPtr cap) (capBlockSize cap) \<and> d = ?d87 sa cte d v0 v1 f cap \<and> v0 = capPtr cap \<and> v1 = capBlockSize cap \<and> f = ?idx87 sa cte d v0 v1 f cap \<and> descendants_range' (capability.UntypedCap (?d87 sa cte d v0 v1 f cap) (capPtr cap) (capBlockSize cap) (?idx87 sa cte d v0 v1 f cap)) slot (ctes_of sa) \<and> capBlockSize cap < word_bits \<and> is_aligned (capPtr cap) (capBlockSize cap) \<and> d = ?d93 sa cte d v0 v1 f cap \<and> v0 = capPtr cap \<and> v1 = capBlockSize cap \<and> f = ?idx93 sa cte d v0 v1 f cap \<and> descendants_range' (capability.UntypedCap (?d93 sa cte d v0 v1 f cap) (capPtr cap) (capBlockSize cap) (?idx93 sa cte d v0 v1 f cap)) slot (ctes_of sa) \<and> capBlockSize cap < word_bits \<and> is_aligned (capPtr cap) (capBlockSize cap)) proof (prove)
goal (1 subgoal):
 1. \<And>cte d v0 v1 f sa. \<lbrakk>invs' sa; st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t sa; ct_active' sa; ctes_of sa slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; sch_act_simple sa; descendants_of' slot (ctes_of sa) = {}\<rbrakk> \<Longrightarrow> \<exists>x. (capFreeIndex x = 0 \<longrightarrow> capability.UntypedCap d v0 v1 f = x \<and> st_tcb_at' P t sa) \<and> (0 < capFreeIndex x \<longrightarrow> capability.UntypedCap d v0 v1 f = x \<and> True \<and> v0 = capPtr x \<and> v1 = capBlockSize x \<and> True \<and> descendants_range' (capability.UntypedCap d (capPtr x) (capBlockSize x) f) slot (ctes_of sa) \<and> capBlockSize x < word_bits \<and> is_aligned (capPtr x) (capBlockSize x) \<and> True \<and> v0 = capPtr x \<and> v1 = capBlockSize x \<and> True \<and> descendants_range' (capability.UntypedCap d (capPtr x) (capBlockSize x) f) slot (ctes_of sa) \<and> capBlockSize x < word_bits \<and> is_aligned (capPtr x) (capBlockSize x) \<and> True \<and> v0 = capPtr x \<and> v1 = capBlockSize x \<and> True \<and> descendants_range' (capability.UntypedCap d (capPtr x) (capBlockSize x) f) slot (ctes_of sa) \<and> capBlockSize x < word_bits \<and> is_aligned (capPtr x) (capBlockSize x)) proof (prove)
goal (1 subgoal):
 1. \<And>cte d v0 v1 f sa. \<lbrakk>invs' sa; st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t sa; ct_active' sa; ctes_of sa slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; sch_act_simple sa; descendants_of' slot (ctes_of sa) = {}\<rbrakk> \<Longrightarrow> (capFreeIndex (capability.UntypedCap d v0 v1 f) = 0 \<longrightarrow> True \<and> st_tcb_at' P t sa) \<and> (0 < capFreeIndex (capability.UntypedCap d v0 v1 f) \<longrightarrow> True \<and> True \<and> v0 = capPtr (capability.UntypedCap d v0 v1 f) \<and> v1 = capBlockSize (capability.UntypedCap d v0 v1 f) \<and> True \<and> descendants_range' (capability.UntypedCap d (capPtr (capability.UntypedCap d v0 v1 f)) (capBlockSize (capability.UntypedCap d v0 v1 f)) f) slot (ctes_of sa) \<and> capBlockSize (capability.UntypedCap d v0 v1 f) < word_bits \<and> is_aligned (capPtr (capability.UntypedCap d v0 v1 f)) (capBlockSize (capability.UntypedCap d v0 v1 f)) \<and> True \<and> v0 = capPtr (capability.UntypedCap d v0 v1 f) \<and> v1 = capBlockSize (capability.UntypedCap d v0 v1 f) \<and> True \<and> descendants_range' (capability.UntypedCap d (capPtr (capability.UntypedCap d v0 v1 f)) (capBlockSize (capability.UntypedCap d v0 v1 f)) f) slot (ctes_of sa) \<and> capBlockSize (capability.UntypedCap d v0 v1 f) < word_bits \<and> is_aligned (capPtr (capability.UntypedCap d v0 v1 f)) (capBlockSize (capability.UntypedCap d v0 v1 f)) \<and> True \<and> v0 = capPtr (capability.UntypedCap d v0 v1 f) \<and> v1 = capBlockSize (capability.UntypedCap d v0 v1 f) \<and> True \<and> descendants_range' (capability.UntypedCap d (capPtr (capability.UntypedCap d v0 v1 f)) (capBlockSize (capability.UntypedCap d v0 v1 f)) f) slot (ctes_of sa) \<and> capBlockSize (capability.UntypedCap d v0 v1 f) < word_bits \<and> is_aligned (capPtr (capability.UntypedCap d v0 v1 f)) (capBlockSize (capability.UntypedCap d v0 v1 f))) proof (prove)
goal (1 subgoal):
 1. \<And>cte d v0 v1 f sa. \<lbrakk>invs' sa; st_tcb_at' (P and (\<noteq>) Structures_H.thread_state.Inactive and (\<noteq>) Structures_H.thread_state.IdleThreadState) t sa; ct_active' sa; ctes_of sa slot = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; sch_act_simple sa; descendants_of' slot (ctes_of sa) = {}; valid_cap' (capability.UntypedCap d v0 v1 f) sa\<rbrakk> \<Longrightarrow> (f = 0 \<longrightarrow> st_tcb_at' P t sa) \<and> (0 < f \<longrightarrow> descendants_range' (capability.UntypedCap d v0 v1 f) slot (ctes_of sa) \<and> v1 < word_bits \<and> is_aligned v0 v1 \<and> descendants_range' (capability.UntypedCap d v0 v1 f) slot (ctes_of sa) \<and> v1 < word_bits \<and> is_aligned v0 v1 \<and> descendants_range' (capability.UntypedCap d v0 v1 f) slot (ctes_of sa) \<and> v1 < word_bits \<and> is_aligned v0 v1) proof (prove)
goal:
No subgoals!