theory Syscall_C

lemma real_cte_tcbCallerSlot:
  "tcb_at' t s \<Longrightarrow> \<not> real_cte_at' (t + 2 ^ cte_level_bits * tcbCallerSlot) s" apply (clarsimp simp: obj_at'_def projectKOs objBits_simps'
                        cte_level_bits_def tcbCallerSlot_def) apply (drule_tac x=t and y="t + a" for a in ps_clearD, assumption) apply (rule le_neq_trans, simp_all)[1] apply (erule is_aligned_no_wrap') apply simp apply (subst field_simps[symmetric], rule is_aligned_no_overflow3, assumption, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_at' t s \<Longrightarrow> \<not> real_cte_at' (t + 2 ^ cte_level_bits * tcbCallerSlot) s proof (prove)
goal (1 subgoal):
 1. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; ps_clear t 9 s; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s\<rbrakk> \<Longrightarrow> t < t + 0x30
 2. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s\<rbrakk> \<Longrightarrow> t + 0x30 \<le> t + 2 ^ 9 - 1
 3. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s; False\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s\<rbrakk> \<Longrightarrow> t \<le> t + 0x30
 2. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s\<rbrakk> \<Longrightarrow> t + 0x30 \<le> t + 2 ^ 9 - 1
 3. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s; False\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s\<rbrakk> \<Longrightarrow> 0x30 < 2 ^ 9
 2. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s\<rbrakk> \<Longrightarrow> t + 0x30 \<le> t + 2 ^ 9 - 1
 3. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s; False\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s\<rbrakk> \<Longrightarrow> t + 0x30 \<le> t + 2 ^ 9 - 1
 2. \<And>obj obja. \<lbrakk>ksPSpace s t = Some (KOTCB obj); is_aligned t 9; is_aligned (t + 0x30) 4; ksPSpace s (t + 0x30) = Some (KOCTE obja); ps_clear (t + 0x30) 4 s; False\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!