theory CSpace_C

lemma clearUntypedFreeIndex_noop_ccorres:
  "ccorres dc xfdc (valid_objs' and untyped_ranges_zero') UNIV hs
      (clearUntypedFreeIndex p) Skip" apply (simp add: clearUntypedFreeIndex_def getSlotCap_def) apply (rule ccorres_guard_imp) apply (rule ccorres_pre_getCTE[where P="\<lambda>rv. cte_wp_at' ((=) rv) p
        and valid_objs' and untyped_ranges_zero'" and P'="K UNIV"]) apply (case_tac "cteCap cte", simp_all add: ccorres_guard_imp[OF ccorres_return_Skip])[1] apply (rule ccorres_guard_imp, rule updateTrackedFreeIndex_forward_noop_ccorres) apply (clarsimp simp: cte_wp_at_ctes_of max_free_index_def) apply (frule(1) Finalise_R.ctes_of_valid') apply (clarsimp simp: valid_cap_simps') apply simp apply (clarsimp simp: cte_wp_at_ctes_of) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_objs' and untyped_ranges_zero') UNIV hs (clearUntypedFreeIndex p) SKIP proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_objs' and untyped_ranges_zero') UNIV hs (do cte <- getCTE p;
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex p (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()
od) SKIP proof (prove)
goal (3 subgoals):
 1. ccorres dc xfdc ?Q6 ?Q'6 hs (do cte <- getCTE p;
case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex p (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()
od) SKIP
 2. \<And>s. (valid_objs' and untyped_ranges_zero') s \<Longrightarrow> ?Q6 s
 3. \<And>s. s \<in> UNIV \<Longrightarrow> s \<in> ?Q'6 proof (prove)
goal (3 subgoals):
 1. \<And>cte. ccorres dc xfdc (cte_wp_at' ((=) cte) p and valid_objs' and untyped_ranges_zero') (K UNIV cte) hs (case cteCap cte of capability.UntypedCap x xa xb xc \<Rightarrow> updateTrackedFreeIndex p (maxFreeIndex (capBlockSize (cteCap cte))) | _ \<Rightarrow> return ()) SKIP
 2. \<And>s. (valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s p = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) p and valid_objs' and untyped_ranges_zero') s
 3. \<And>s. s \<in> UNIV \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K UNIV (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104. cteCap cte = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> ccorres dc xfdc (cte_wp_at' ((=) cte) p and valid_objs' and untyped_ranges_zero') UNIV hs (updateTrackedFreeIndex p (max_free_index x103)) SKIP
 2. \<And>s. (valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s p = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) p and valid_objs' and untyped_ranges_zero') s
 3. \<And>s. s \<in> UNIV \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K UNIV (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; (cte_wp_at' ((=) cte) p and valid_objs' and untyped_ranges_zero') s\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> max_free_index x103 \<and> max_free_index x103 \<le> 2 ^ capBlockSize cap) \<circ> cteCap) p and valid_objs' and untyped_ranges_zero') s
 2. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV
 3. \<And>s. (valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s p = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) p and valid_objs' and untyped_ranges_zero') s
 4. \<And>s. s \<in> UNIV \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K UNIV (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; ctes_of s p = Some cte; valid_objs' s; untyped_ranges_zero' s\<rbrakk> \<Longrightarrow> x104 \<le> 2 ^ x103
 2. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV
 3. \<And>s. (valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s p = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) p and valid_objs' and untyped_ranges_zero') s
 4. \<And>s. s \<in> UNIV \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K UNIV (cte_to_H cte')} proof (prove)
goal (4 subgoals):
 1. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; ctes_of s p = Some cte; valid_objs' s; untyped_ranges_zero' s; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> x104 \<le> 2 ^ x103
 2. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV
 3. \<And>s. (valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s p = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) p and valid_objs' and untyped_ranges_zero') s
 4. \<And>s. s \<in> UNIV \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K UNIV (cte_to_H cte')} proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104 s. \<lbrakk>cteCap cte = capability.UntypedCap x101 x102 x103 x104; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV
 2. \<And>s. (valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s p = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) p and valid_objs' and untyped_ranges_zero') s
 3. \<And>s. s \<in> UNIV \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K UNIV (cte_to_H cte')} proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_objs' and untyped_ranges_zero') s \<Longrightarrow> \<forall>cte. ctes_of s p = Some cte \<longrightarrow> (cte_wp_at' ((=) cte) p and valid_objs' and untyped_ranges_zero') s
 2. \<And>s. s \<in> UNIV \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K UNIV (cte_to_H cte')} proof (prove)
goal (1 subgoal):
 1. \<And>s. s \<in> UNIV \<Longrightarrow> s \<in> {s. \<forall>cte'. (cte_lift \<circ>\<^sub>m cslift s) (cte_Ptr p) = Some cte' \<and> cl_valid_cte cte' \<longrightarrow> s \<in> K UNIV (cte_to_H cte')} proof (prove)
goal:
No subgoals!