theory DetWP

lemma det_wp_setObject_other [wp]:
  fixes ob :: "'a :: pspace_storable"
  assumes x: "updateObject ob = updateObject_default ob"
  shows "det_wp (obj_at' (\<lambda>k::'a. objBits k = objBits ob) ptr)
                  (setObject ptr ob)" apply (simp add: setObject_def x split_def updateObject_default_def
                   magnitudeCheck_def
                   projectKO_def2 alignCheck_def alignError_def) apply (rule det_wp_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. det_wp (obj_at' (\<lambda>k. objBits k = objBits ob) ptr) (setObject ptr ob) proof (prove)
goal (1 subgoal):
 1. det_wp (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 <- case snd (lookupAround2 ptr ps) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - ptr < 1 << objBits ob) fail;
return (injectKOS ob)
od;
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od) proof (prove)
goal (2 subgoals):
 1. det_wp ?P'1 (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 <- case snd (lookupAround2 ptr ps) of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - ptr < 1 << objBits ob) fail;
return (injectKOS 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> ?P'1 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> ((\<lambda>s. ptr && mask (objBits ob) \<noteq> 0 \<longrightarrow> False) and (\<lambda>sa. ((snd (lookupAround2 ptr (ksPSpace s)) = None \<longrightarrow> True) \<and> (\<forall>y. snd (lookupAround2 ptr (ksPSpace s)) = Some y \<longrightarrow> y - ptr < 1 << objBits ob \<longrightarrow> False)) \<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 (injectKOS obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; ps_clear ptr (objBits ob) s\<rbrakk> \<Longrightarrow> (\<exists>y. injectKOS y = injectKOS obj) \<and> ((\<exists>y. injectKOS y = injectKOS obj) \<longrightarrow> (\<forall>y. snd (lookupAround2 ptr (ksPSpace s)) = Some y \<longrightarrow> \<not> y - ptr < 2 ^ objBits ob)) proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKOS obj); is_aligned ptr (objBits ob); objBits obj = objBits ob\<rbrakk> \<Longrightarrow> ptr \<le> ptr
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKOS 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 (injectKOS obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKOS obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKOS y = injectKOS obj) \<and> ((\<exists>y. injectKOS y = injectKOS obj) \<longrightarrow> (\<forall>y. snd (lookupAround2 ptr (ksPSpace s)) = Some y \<longrightarrow> \<not> y - ptr < 2 ^ objBits ob)) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKOS 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 (injectKOS obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKOS obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKOS y = injectKOS obj) \<and> ((\<exists>y. injectKOS y = injectKOS obj) \<longrightarrow> (\<forall>y. snd (lookupAround2 ptr (ksPSpace s)) = Some y \<longrightarrow> \<not> y - ptr < 2 ^ objBits ob)) proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKOS 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 (injectKOS 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 (injectKOS obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKOS obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKOS y = injectKOS obj) \<and> ((\<exists>y. injectKOS y = injectKOS obj) \<longrightarrow> (\<forall>y. snd (lookupAround2 ptr (ksPSpace s)) = Some y \<longrightarrow> \<not> y - ptr < 2 ^ objBits ob)) proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKOS 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 (injectKOS 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 (injectKOS obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKOS obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKOS y = injectKOS obj) \<and> ((\<exists>y. injectKOS y = injectKOS obj) \<longrightarrow> (\<forall>y. snd (lookupAround2 ptr (ksPSpace s)) = Some y \<longrightarrow> \<not> y - ptr < 2 ^ objBits ob)) proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKOS 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 (injectKOS 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 (injectKOS obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKOS obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKOS y = injectKOS obj) \<and> ((\<exists>y. injectKOS y = injectKOS obj) \<longrightarrow> (\<forall>y. snd (lookupAround2 ptr (ksPSpace s)) = Some y \<longrightarrow> \<not> y - ptr < 2 ^ objBits ob)) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKOS 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 (injectKOS obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKOS obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKOS y = injectKOS obj) \<and> ((\<exists>y. injectKOS y = injectKOS obj) \<longrightarrow> (\<forall>y. snd (lookupAround2 ptr (ksPSpace s)) = Some y \<longrightarrow> \<not> y - ptr < 2 ^ objBits ob)) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (injectKOS obj); is_aligned ptr (objBits ob); objBits obj = objBits ob; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, injectKOS obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits ob \<le> x - ptr\<rbrakk> \<Longrightarrow> (\<exists>y. injectKOS y = injectKOS obj) \<and> ((\<exists>y. injectKOS y = injectKOS obj) \<longrightarrow> (\<forall>y. snd (lookupAround2 ptr (ksPSpace s)) = Some y \<longrightarrow> \<not> y - ptr < 2 ^ objBits ob)) proof (prove)
goal:
No subgoals!