theory KHeap_R

lemma no_fail_getNotification [wp]:
  "no_fail (ntfn_at' ptr) (getNotification ptr)" apply (simp add: getNotification_def getObject_def
                   split_def) apply (rule no_fail_pre) apply wp apply (clarsimp simp add: obj_at'_def projectKOs objBits_simps'
                            lookupAround2_known1) apply (erule(1) ps_clear_lookupAround2) apply simp apply (simp add: field_simps) apply (erule is_aligned_no_wrap') apply (simp add: word_bits_conv) apply (clarsimp split: option.split_asm simp: objBits_simps' archObjSize_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (ntfn_at' ptr) (getNotification ptr) proof (prove)
goal (1 subgoal):
 1. no_fail (ntfn_at' ptr) (do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 ptr map));
loadObject_default ptr (fst p) (snd (lookupAround2 ptr map)) (snd p)
od) proof (prove)
goal (2 subgoals):
 1. no_fail ?P (do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 ptr map));
loadObject_default ptr (fst p) (snd (lookupAround2 ptr map)) (snd p)
od)
 2. \<And>s. ntfn_at' ptr s \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. ntfn_at' 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> (\<exists>obj. projectKO_opt (snd (the (fst (lookupAround2 ptr (ksPSpace s))))) = Some obj \<and> is_aligned ptr (objBits obj) \<and> fst (the (fst (lookupAround2 ptr (ksPSpace s)))) = ptr \<and> (case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits obj \<le> x - ptr)))) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (KONotification obj); is_aligned ptr 4; ps_clear ptr 4 s\<rbrakk> \<Longrightarrow> case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x10 \<le> x - ptr proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (KONotification obj); is_aligned ptr 4\<rbrakk> \<Longrightarrow> ptr \<le> ptr
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (KONotification obj); is_aligned ptr 4\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ 4 - 1
 3. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (KONotification obj); is_aligned ptr 4; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, KONotification obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - ptr\<rbrakk> \<Longrightarrow> case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x10 \<le> x - ptr proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (KONotification obj); is_aligned ptr 4\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ 4 - 1
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (KONotification obj); is_aligned ptr 4; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, KONotification obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - ptr\<rbrakk> \<Longrightarrow> case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x10 \<le> x - ptr proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (KONotification obj); is_aligned ptr 4\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 0xF
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (KONotification obj); is_aligned ptr 4; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, KONotification obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - ptr\<rbrakk> \<Longrightarrow> case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x10 \<le> x - ptr proof (prove)
goal (2 subgoals):
 1. \<And>s obj. ksPSpace s ptr = Some (KONotification obj) \<Longrightarrow> 0xF < 2 ^ 4
 2. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (KONotification obj); is_aligned ptr 4; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, KONotification obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - ptr\<rbrakk> \<Longrightarrow> case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x10 \<le> x - ptr proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>ksPSpace s ptr = Some (KONotification obj); is_aligned ptr 4; fst (lookupAround2 ptr (ksPSpace s)) = Some (ptr, KONotification obj); case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 4 \<le> x - ptr\<rbrakk> \<Longrightarrow> case snd (lookupAround2 ptr (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x10 \<le> x - ptr proof (prove)
goal:
No subgoals!