theory KHeap_R

lemma no_fail_loadObject_default [wp]:
  "no_fail (\<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 no_fail_pre) apply (wp case_option_wp) apply (clarsimp simp: is_aligned_mask) apply (clarsimp split: option.split_asm) apply (clarsimp simp: is_aligned_mask[symmetric]) apply simp done

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