theory DetWP

lemma det_wp_loadObject_default [wp]:
  "det_wp (\<lambda>s. \<exists>obj. projectKO_opt ko = Some (obj::'a) \<and>
                      is_aligned p (objBits obj) \<and> q = p
                      \<and> case_option True (\<lambda>x. 2 ^ (objBits obj) \<le> x - p) n)
           (loadObject_default p q n ko :: ('a::pre_storable) kernel)" apply (simp add: loadObject_default_def split_def projectKO_def
                   alignCheck_def alignError_def magnitudeCheck_def
                   unless_def) apply (rule det_wp_pre) apply (wp case_option_wp) apply (clarsimp simp: is_aligned_mask[symmetric]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>s. \<exists>obj. projectKO_opt ko = Some obj \<and> is_aligned p (objBits obj) \<and> q = p \<and> (case n of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits obj \<le> x - p)) (loadObject_default p q n ko) proof (prove)
goal (1 subgoal):
 1. det_wp (\<lambda>s. \<exists>obj. projectKO_opt ko = Some obj \<and> is_aligned p (objBits obj) \<and> q = p \<and> (case n of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits obj \<le> x - p)) (do y <- assert (p = q);
val <- case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
y <- when (p && mask (objBits val) \<noteq> 0) fail;
y <- case n of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - p < 1 << objBits val) fail;
return val
od) proof (prove)
goal (2 subgoals):
 1. det_wp ?P' (do y <- assert (p = q);
val <- case projectKO_opt ko of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
y <- when (p && mask (objBits val) \<noteq> 0) fail;
y <- case n of None \<Rightarrow> return () | Some z \<Rightarrow> when (z - p < 1 << objBits val) fail;
return val
od)
 2. \<And>s. \<exists>obj. projectKO_opt ko = Some obj \<and> is_aligned p (objBits obj) \<and> q = p \<and> (case n of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits obj \<le> x - p) \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>obj. projectKO_opt ko = Some obj \<and> is_aligned p (objBits obj) \<and> q = p \<and> (case n of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits obj \<le> x - p) \<Longrightarrow> ((\<lambda>_. p = q) and (\<lambda>s. p = q \<longrightarrow> ((\<lambda>s. (projectKO_opt ko = None \<longrightarrow> False) \<and> (\<forall>y. projectKO_opt ko = Some y \<longrightarrow> True)) and (\<lambda>s. (projectKO_opt ko = None \<longrightarrow> True) \<and> (projectKO_opt ko \<noteq> None \<longrightarrow> ((\<lambda>s. p && mask (objBits (the (projectKO_opt ko))) \<noteq> 0 \<longrightarrow> False) and (\<lambda>s. ((n = None \<longrightarrow> True) \<and> (\<forall>y. n = Some y \<longrightarrow> y - p < 1 << objBits (the (projectKO_opt ko)) \<longrightarrow> False)) \<and> (n = None \<longrightarrow> True) \<and> (n \<noteq> None \<longrightarrow> True))) s))) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>obj y. \<lbrakk>projectKO_opt ko = Some obj; is_aligned p (objBits obj); 2 ^ objBits obj \<le> y - p; q = p; n = Some y; y - p < 2 ^ objBits obj\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!