theory Invoke_C

lemma resetUntypedCap_gsCNodes_at_pt:
  "\<lbrace>(\<lambda>s. P (gsCNodes s ptr))
      and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> ptr \<notin> untypedRange (cteCap cte)) slot
      and valid_objs'\<rbrace>
    resetUntypedCap slot
   \<lbrace>\<lambda>rv s. P (gsCNodes s ptr)\<rbrace>, -" apply (simp add: resetUntypedCap_def unlessE_def) apply (rule hoare_pre) apply (wp mapME_x_wp' | simp add: unless_def)+ apply (wp hoare_vcg_const_imp_lift
              deleteObjects_gsCNodes_at_pt
              getSlotCap_wp)+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps) apply (frule(1) ctes_of_valid') apply (clarsimp simp: valid_cap_simps' capAligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (gsCNodes s ptr)) and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> ptr \<notin> untypedRange (cteCap cte)) slot and valid_objs'\<rbrace> resetUntypedCap slot \<lbrace>\<lambda>rv s. P (gsCNodes s ptr)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. P (gsCNodes s ptr)) and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> ptr \<notin> untypedRange (cteCap cte)) slot and valid_objs'\<rbrace> doE cap <- liftE (getSlotCap slot);
if capFreeIndex cap = 0 then returnOk () else 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>rv s. P (gsCNodes s ptr)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'\<rbrace> doE cap <- liftE (getSlotCap slot);
if capFreeIndex cap = 0 then returnOk () else 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>rv s. P (gsCNodes s ptr)\<rbrace>, -
 2. \<And>s. ((\<lambda>s. P (gsCNodes s ptr)) and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> ptr \<notin> untypedRange (cteCap cte)) slot and valid_objs') s \<Longrightarrow> ?P' s proof (prove)
goal (3 subgoals):
 1. \<And>cap. 0 < capFreeIndex cap \<Longrightarrow> \<lbrace>?P'46 cap\<rbrace> deleteObjects (capPtr cap) (capBlockSize cap) \<lbrace>\<lambda>y s. (capIsDevice cap \<longrightarrow> P (gsCNodes s ptr)) \<and> (capBlockSize cap < resetChunkBits \<longrightarrow> P (gsCNodes s ptr)) \<and> (\<not> capIsDevice cap \<and> \<not> capBlockSize cap < resetChunkBits \<longrightarrow> P (gsCNodes s ptr))\<rbrace>
 2. \<lbrace>?P'\<rbrace> liftE (getSlotCap slot) \<lbrace>\<lambda>cap s. (capFreeIndex cap = 0 \<longrightarrow> P (gsCNodes s ptr)) \<and> (capFreeIndex cap \<noteq> 0 \<longrightarrow> True \<and> ?P'46 cap s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. ((\<lambda>s. P (gsCNodes s ptr)) and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> ptr \<notin> untypedRange (cteCap cte)) slot and valid_objs') s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. P (gsCNodes s ptr)) and cte_wp_at' (\<lambda>cte. isUntypedCap (cteCap cte) \<and> ptr \<notin> untypedRange (cteCap cte)) slot and valid_objs') s \<Longrightarrow> True \<and> (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> (capFreeIndex cap = 0 \<longrightarrow> P (gsCNodes s ptr)) \<and> (capFreeIndex cap \<noteq> 0 \<longrightarrow> True \<and> (capIsDevice cap \<longrightarrow> ((\<lambda>s. P (gsCNodes s ptr)) and K (ptr \<notin> {capPtr cap..capPtr cap + 2 ^ capBlockSize cap - 1} \<and> is_aligned (capPtr cap) (capBlockSize cap))) s) \<and> (capBlockSize cap < resetChunkBits \<longrightarrow> ((\<lambda>s. P (gsCNodes s ptr)) and K (ptr \<notin> {capPtr cap..capPtr cap + 2 ^ capBlockSize cap - 1} \<and> is_aligned (capPtr cap) (capBlockSize cap))) s) \<and> (\<not> capIsDevice cap \<and> \<not> capBlockSize cap < resetChunkBits \<longrightarrow> ((\<lambda>s. P (gsCNodes s ptr)) and K (ptr \<notin> {capPtr cap..capPtr cap + 2 ^ capBlockSize cap - 1} \<and> is_aligned (capPtr cap) (capBlockSize cap))) s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>P (gsCNodes s ptr); valid_objs' s; ctes_of s slot = Some cte; v0 \<le> ptr \<longrightarrow> \<not> ptr \<le> v0 + 2 ^ v1 - 1; cteCap cte = capability.UntypedCap d v0 v1 f; 0 < f\<rbrakk> \<Longrightarrow> (d \<longrightarrow> is_aligned v0 v1) \<and> (v1 < resetChunkBits \<longrightarrow> is_aligned v0 v1) \<and> (\<not> d \<and> \<not> v1 < resetChunkBits \<longrightarrow> is_aligned v0 v1) proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>P (gsCNodes s ptr); valid_objs' s; ctes_of s slot = Some cte; v0 \<le> ptr \<longrightarrow> \<not> ptr \<le> v0 + 2 ^ v1 - 1; cteCap cte = capability.UntypedCap d v0 v1 f; 0 < f; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> (d \<longrightarrow> is_aligned v0 v1) \<and> (v1 < resetChunkBits \<longrightarrow> is_aligned v0 v1) \<and> (\<not> d \<and> \<not> v1 < resetChunkBits \<longrightarrow> is_aligned v0 v1) proof (prove)
goal:
No subgoals!