theory DetWP

lemma det_wp_getTCB [wp]:
  "det_wp (tcb_at' t) (getObject t :: tcb kernel)" apply (simp add: getObject_def split_def) apply (rule det_wp_pre) apply (wp|wpc)+ apply (clarsimp simp add: obj_at'_def projectKOs objBits_simps
                      cong: conj_cong option.case_cong) apply (simp add: lookupAround2_known1) apply (rule ps_clear_lookupAround2, assumption+) apply simp apply (erule is_aligned_no_overflow) apply (simp add: word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (tcb_at' t) (getObject t) proof (prove)
goal (1 subgoal):
 1. det_wp (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. det_wp ?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 tcbBlockSizeBits; ps_clear t tcbBlockSizeBits 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> 2 ^ tcbBlockSizeBits \<le> x - t) proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - t proof (prove)
goal (3 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> t \<le> t
 2. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> t \<le> t + 2 ^ tcbBlockSizeBits - 1
 3. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; fst (lookupAround2 t (ksPSpace s)) = Some (t, KOTCB obj); case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - t\<rbrakk> \<Longrightarrow> case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - t proof (prove)
goal (2 subgoals):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> t \<le> t + 2 ^ tcbBlockSizeBits - 1
 2. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; fst (lookupAround2 t (ksPSpace s)) = Some (t, KOTCB obj); case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - t\<rbrakk> \<Longrightarrow> case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - t proof (prove)
goal (1 subgoal):
 1. \<And>s obj. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; fst (lookupAround2 t (ksPSpace s)) = Some (t, KOTCB obj); case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - t\<rbrakk> \<Longrightarrow> case snd (lookupAround2 t (ksPSpace s)) of None \<Rightarrow> True | Some x \<Rightarrow> 2 ^ tcbBlockSizeBits \<le> x - t proof (prove)
goal:
No subgoals!