theory KHeap_R

lemma no_fail_getObject_tcb [wp]:
  "no_fail (tcb_at' t) (getObject t :: tcb kernel)" apply (simp add: getObject_def split_def) apply (rule no_fail_pre) apply wp apply (clarsimp simp add: obj_at'_def projectKOs objBits_simps'
                      cong: conj_cong) apply (rule ps_clear_lookupAround2, assumption+) apply simp apply (simp add: field_simps) apply (erule is_aligned_no_wrap') apply simp apply (fastforce split: option.split_asm simp: objBits_simps' archObjSize_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at' t) (getObject t) proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at' t) (do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t map));
loadObject_default t (fst p) (snd (lookupAround2 t map)) (snd p)
od) proof (prove)
goal (2 subgoals):
 1. no_fail ?P (do map <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 t map));
loadObject_default t (fst p) (snd (lookupAround2 t map)) (snd p)
od)
 2. \<And>s. tcb_at' t s \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. fst (lookupAround2 t (ksPSpace s)) \<noteq> None) and (\<lambda>sa. fst (lookupAround2 t (ksPSpace s)) \<noteq> None \<longrightarrow> (\<exists>obj. projectKO_opt (snd (the (fst (lookupAround2 t (ksPSpace s))))) = Some obj \<and> is_aligned t (objBits obj) \<and> fst (the (fst (lookupAround2 t (ksPSpace s)))) = t \<and> (case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ objBits obj \<le> x - t)))) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<and> (\<exists>obj. snd (the (fst (lookupAround2 t (ksPSpace s)))) = KOTCB obj) \<and> fst (the (fst (lookupAround2 t (ksPSpace s)))) = t \<and> (case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x200 \<le> x - t) proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s\<rbrakk> \<Longrightarrow> t \<le> t
 2. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s\<rbrakk> \<Longrightarrow> t \<le> t + 2 ^ 9 - 1
 3. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s; fst (lookupAround2 t (ksPSpace s)) = Some (t, KOTCB obj); case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 9 \<le> x - t\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<and> (\<exists>obj. snd (the (fst (lookupAround2 t (ksPSpace s)))) = KOTCB obj) \<and> fst (the (fst (lookupAround2 t (ksPSpace s)))) = t \<and> (case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x200 \<le> x - t) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s\<rbrakk> \<Longrightarrow> t \<le> t + 2 ^ 9 - 1
 2. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s; fst (lookupAround2 t (ksPSpace s)) = Some (t, KOTCB obj); case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 9 \<le> x - t\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<and> (\<exists>obj. snd (the (fst (lookupAround2 t (ksPSpace s)))) = KOTCB obj) \<and> fst (the (fst (lookupAround2 t (ksPSpace s)))) = t \<and> (case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x200 \<le> x - t) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s\<rbrakk> \<Longrightarrow> t \<le> t + 0x1FF
 2. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s; fst (lookupAround2 t (ksPSpace s)) = Some (t, KOTCB obj); case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 9 \<le> x - t\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<and> (\<exists>obj. snd (the (fst (lookupAround2 t (ksPSpace s)))) = KOTCB obj) \<and> fst (the (fst (lookupAround2 t (ksPSpace s)))) = t \<and> (case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x200 \<le> x - t) proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); ps_clear t 9 s\<rbrakk> \<Longrightarrow> 0x1FF < 2 ^ 9
 2. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s; fst (lookupAround2 t (ksPSpace s)) = Some (t, KOTCB obj); case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 9 \<le> x - t\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<and> (\<exists>obj. snd (the (fst (lookupAround2 t (ksPSpace s)))) = KOTCB obj) \<and> fst (the (fst (lookupAround2 t (ksPSpace s)))) = t \<and> (case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x200 \<le> x - t) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s; fst (lookupAround2 t (ksPSpace s)) = Some (t, KOTCB obj); case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ 9 \<le> x - t\<rbrakk> \<Longrightarrow> (\<exists>a b. fst (lookupAround2 t (ksPSpace s)) = Some (a, b)) \<and> (\<exists>obj. snd (the (fst (lookupAround2 t (ksPSpace s)))) = KOTCB obj) \<and> fst (the (fst (lookupAround2 t (ksPSpace s)))) = t \<and> (case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 0x200 \<le> x - t) proof (prove)
goal:
No subgoals!