theory KHeap_R

lemma no_fail_setObject_other [wp]:
  fixes ob :: "'a :: pspace_storable"
  assumes x: "updateObject ob = updateObject_default ob"
  shows "no_fail (obj_at' (\<lambda>k::'a. objBits k = objBits ob) ptr)
                  (setObject ptr ob)" apply (simp add: setObject_def x split_def updateObject_default_def
                   projectKO_def2 alignCheck_def alignError_def) apply (rule no_fail_pre) apply (wp ) apply (clarsimp simp: is_aligned_mask[symmetric] obj_at'_def
                        objBits_def[symmetric] projectKOs
                        project_inject lookupAround2_known1) apply (erule(1) ps_clear_lookupAround2) apply simp apply (erule is_aligned_get_word_bits) apply (subst add_diff_eq[symmetric]) apply (erule is_aligned_no_wrap') apply simp apply simp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (obj_at' (\<lambda>k. objBits k = objBits ob) ptr) (setObject ptr ob) proof (prove)
goal (1 subgoal):
 1. no_fail (obj_at' (\<lambda>k. objBits k = objBits ob) ptr) (do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 ptr ps));
obj' <- do y <- assert (ptr = fst p);
_ <- assert_opt (projectKO_opt (snd p));
y <- unless (ptr && mask (objBits ob) = 0) fail;
y <- magnitudeCheck ptr (snd (lookupAround2 ptr ps)) (objBits ob);
return (injectKO ob)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od) proof (prove)
goal (2 subgoals):
 1. no_fail ?P1 (do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 ptr ps));
obj' <- do y <- assert (ptr = fst p);
_ <- assert_opt (projectKO_opt (snd p));
y <- unless (ptr && mask (objBits ob) = 0) fail;
y <- magnitudeCheck ptr (snd (lookupAround2 ptr ps)) (objBits ob);
return (injectKO ob)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od)
 2. \<And>s. obj_at' (\<lambda>k. objBits k = objBits ob) ptr s \<Longrightarrow> ?P1 s proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' (\<lambda>k. objBits k = objBits ob) ptr s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. fst (lookupAround2 ptr (ksPSpace s)) \<noteq> None) and (\<lambda>sa. fst (lookupAround2 ptr (ksPSpace s)) \<noteq> None \<longrightarrow> ((\<lambda>_. ptr = fst (the (fst (lookupAround2 ptr (ksPSpace s))))) and (\<lambda>sa. ptr = fst (the (fst (lookupAround2 ptr (ksPSpace s)))) \<longrightarrow> ((\<lambda>_. projectKO_opt (snd (the (fst (lookupAround2 ptr (ksPSpace s))))) \<noteq> None) and (\<lambda>sa. projectKO_opt (snd (the (fst (lookupAround2 ptr (ksPSpace s))))) \<noteq> None \<longrightarrow> ((if ptr && mask (objBits ob) = 0 then \<lambda>_. True else (\<lambda>_. False)) and (\<lambda>sa. (case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits ob \<le> z - ptr) \<and> True)) sa)) sa) and (\<lambda>sa. ptr = fst (the (fst (lookupAround2 ptr (ksPSpace s)))) \<longrightarrow> projectKO_opt (snd (the (fst (lookupAround2 ptr (ksPSpace s))))) \<noteq> None \<longrightarrow> True)) sa)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; ps_clear ptr (objBits ob) s\<rbrakk> \<Longrightarrow> (\<exists>y. injectKO y = injectKO obj) \<and> ((\<exists>y. injectKO y = injectKO obj) \<longrightarrow> (case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits ob \<le> z - ptr)) proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob\<rbrakk> \<Longrightarrow> ptr \<le> ptr
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ objBits ob - 1
 3. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKO obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKO y = injectKO obj) \<and> ((\<exists>y. injectKO y = injectKO obj) \<longrightarrow> (case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits ob \<le> z - ptr)) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ objBits ob - 1
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKO obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKO y = injectKO obj) \<and> ((\<exists>y. injectKO y = injectKO obj) \<longrightarrow> (case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits ob \<le> z - ptr)) proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); objBits obj = objBits ob; is_aligned ptr (objBits ob); objBits ob < LENGTH(32)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ objBits ob - 1
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); objBits obj = objBits ob; ptr = 0; LENGTH(32) \<le> objBits ob\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ objBits ob - 1
 3. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKO obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKO y = injectKO obj) \<and> ((\<exists>y. injectKO y = injectKO obj) \<longrightarrow> (case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits ob \<le> z - ptr)) proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); objBits obj = objBits ob; is_aligned ptr (objBits ob); objBits ob < LENGTH(32)\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (2 ^ objBits ob - 1)
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); objBits obj = objBits ob; ptr = 0; LENGTH(32) \<le> objBits ob\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ objBits ob - 1
 3. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKO obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKO y = injectKO obj) \<and> ((\<exists>y. injectKO y = injectKO obj) \<longrightarrow> (case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits ob \<le> z - ptr)) proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); objBits obj = objBits ob; objBits ob < LENGTH(32)\<rbrakk> \<Longrightarrow> 2 ^ objBits ob - 1 < 2 ^ objBits ob
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); objBits obj = objBits ob; ptr = 0; LENGTH(32) \<le> objBits ob\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ objBits ob - 1
 3. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKO obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKO y = injectKO obj) \<and> ((\<exists>y. injectKO y = injectKO obj) \<longrightarrow> (case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits ob \<le> z - ptr)) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); objBits obj = objBits ob; ptr = 0; LENGTH(32) \<le> objBits ob\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ objBits ob - 1
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKO obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKO y = injectKO obj) \<and> ((\<exists>y. injectKO y = injectKO obj) \<longrightarrow> (case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits ob \<le> z - ptr)) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKO obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKO obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKO y = injectKO obj) \<and> ((\<exists>y. injectKO y = injectKO obj) \<longrightarrow> (case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits ob \<le> z - ptr)) proof (prove)
goal:
No subgoals!