theory Detype_R

lemma deleteObjects_cte_wp_at':
  "\<lbrace>\<lambda>s. cte_wp_at' P p s \<and> p \<notin> {ptr .. ptr + 2 ^ bits - 1}
         \<and> s \<turnstile>' (UntypedCap d ptr bits idx) \<and> valid_pspace' s\<rbrace>
     deleteObjects ptr bits
   \<lbrace>\<lambda>rv s. cte_wp_at' P p s\<rbrace>" apply (simp add: deleteObjects_def3 doMachineOp_def split_def) apply wp apply (clarsimp simp: valid_pspace'_def cong:if_cong) apply (subgoal_tac
     "s\<lparr>ksMachineState := b,
        ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None
                        else ksPSpace s x\<rparr> =
      ksMachineState_update (\<lambda>_. b)
      (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None
                         else ksPSpace s x\<rparr>)", erule ssubst) apply (simp add: cte_wp_at_delete' x_power_minus_1) apply (case_tac s, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' P p s \<and> p \<notin> {ptr..ptr + 2 ^ bits - 1} \<and> valid_cap' (capability.UntypedCap d ptr bits idx) s \<and> valid_pspace' s\<rbrace> deleteObjects ptr bits \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' P p s \<and> (ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1) \<and> valid_cap' (capability.UntypedCap d ptr bits idx) s \<and> valid_pspace' s\<rbrace> do y <- assert (is_aligned ptr bits);
y <- stateAssert (deletionIsSafe ptr bits) [];
y <- do ms <- gets ksMachineState;
p <- select_f (freeMemory ptr bits ms);
modify (ksMachineState_update (\<lambda>_. snd p))
od;
y <- stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1)) [];
y <- modify (\<lambda>s. s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>);
stateAssert ksASIDMapSafe []
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' P p s \<and> (ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1) \<and> valid_cap' (capability.UntypedCap d ptr bits idx) s \<and> valid_pspace' s \<Longrightarrow> is_aligned ptr bits \<longrightarrow> deletionIsSafe ptr bits s \<longrightarrow> (\<forall>x\<in>fst (freeMemory ptr bits (ksMachineState s)). \<not> cNodePartialOverlap (gsCNodes (s\<lparr>ksMachineState := snd x\<rparr>)) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1) \<longrightarrow> ksASIDMapSafe (s\<lparr>ksMachineState := snd x, ksPSpace := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsUserPages := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsCNodes := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd x\<rparr>) xa\<rparr>) \<longrightarrow> cte_wp_at' P p (s\<lparr>ksMachineState := snd x, ksPSpace := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else ksPSpace (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsUserPages := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsUserPages (s\<lparr>ksMachineState := snd x\<rparr>) xa, gsCNodes := \<lambda>xa. if ptr \<le> xa \<and> xa \<le> ptr + 2 ^ bits - 1 then None else gsCNodes (s\<lparr>ksMachineState := snd x\<rparr>) xa\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>cte_wp_at' P p s; ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1; valid_cap' (capability.UntypedCap d ptr bits idx) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>)\<rbrakk> \<Longrightarrow> cte_wp_at' P p (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>cte_wp_at' P p s; ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1; valid_cap' (capability.UntypedCap d ptr bits idx) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>)\<rbrakk> \<Longrightarrow> cte_wp_at' P p (s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, ksMachineState := b\<rparr>)
 2. \<And>s b. \<lbrakk>cte_wp_at' P p s; ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1; valid_cap' (capability.UntypedCap d ptr bits idx) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>)\<rbrakk> \<Longrightarrow> s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr> = s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, ksMachineState := b\<rparr> proof (prove)
goal (1 subgoal):
 1. \<And>s b. \<lbrakk>cte_wp_at' P p s; ptr \<le> p \<longrightarrow> \<not> p \<le> ptr + 2 ^ bits - 1; valid_cap' (capability.UntypedCap d ptr bits idx) s; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; is_aligned ptr bits; deletionIsSafe ptr bits s; \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1); ((), b) \<in> fst (freeMemory ptr bits (ksMachineState s)); ksASIDMapSafe (s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, gsUserPages := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsUserPages s x, gsCNodes := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else gsCNodes s x\<rparr>)\<rbrakk> \<Longrightarrow> s\<lparr>ksMachineState := b, ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x\<rparr> = s\<lparr>ksPSpace := \<lambda>x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else ksPSpace s x, ksMachineState := b\<rparr> proof (prove)
goal:
No subgoals!