theory Retype_C

lemma c_guard_tcb:
  assumes al: "is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits"
  and   ptr0: "ctcb_ptr_to_tcb_ptr p \<noteq> 0"
  shows "c_guard p" unfolding c_guard_def proof (rule conjI) show "ptr_aligned p" using al apply - apply (rule is_aligned_ptr_aligned [where n = word_size_bits]) apply (rule is_aligned_weaken) apply (erule ctcb_ptr_to_tcb_ptr_aligned) by (auto simp: align_of_def word_size_bits_def ctcb_size_bits_def) show "c_null_guard p" using ptr0 al unfolding c_null_guard_def apply - apply (rule intvl_nowrap [where x = 0, simplified]) apply (clarsimp simp: ctcb_ptr_to_tcb_ptr_def ctcb_offset_defs is_aligned_def objBits_defs) apply (drule ctcb_ptr_to_tcb_ptr_aligned) apply (erule is_aligned_no_wrap_le) by (auto simp add: word_bits_conv ctcb_size_bits_def) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c_guard p proof (prove)
goal (1 subgoal):
 1. ptr_aligned p \<and> c_null_guard p proof (state)
goal (2 subgoals):
 1. ptr_aligned p
 2. c_null_guard p proof (prove)
goal (1 subgoal):
 1. ptr_aligned p proof (prove)
using this:
is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits

goal (1 subgoal):
 1. ptr_aligned p proof (prove)
goal (1 subgoal):
 1. is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits \<Longrightarrow> ptr_aligned p proof (prove)
goal (2 subgoals):
 1. is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits \<Longrightarrow> is_aligned (ptr_val p) word_size_bits
 2. is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits \<Longrightarrow> align_of TYPE(tcb_C) = 2 ^ word_size_bits proof (prove)
goal (3 subgoals):
 1. is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits \<Longrightarrow> is_aligned (ptr_val p) ?x4
 2. is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits \<Longrightarrow> word_size_bits \<le> ?x4
 3. is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits \<Longrightarrow> align_of TYPE(tcb_C) = 2 ^ word_size_bits proof (prove)
goal (2 subgoals):
 1. is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits \<Longrightarrow> word_size_bits \<le> ctcb_size_bits
 2. is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits \<Longrightarrow> align_of TYPE(tcb_C) = 2 ^ word_size_bits proof (state)
this:
ptr_aligned p

goal (1 subgoal):
 1. c_null_guard p proof (prove)
goal (1 subgoal):
 1. c_null_guard p proof (prove)
using this:
ctcb_ptr_to_tcb_ptr p \<noteq> 0
is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits

goal (1 subgoal):
 1. c_null_guard p proof (prove)
using this:
ctcb_ptr_to_tcb_ptr p \<noteq> 0
is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits

goal (1 subgoal):
 1. 0 \<notin> ptr_span p proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctcb_ptr_to_tcb_ptr p \<noteq> 0; is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 0 \<notin> ptr_span p proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctcb_ptr_to_tcb_ptr p \<noteq> 0; is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits\<rbrakk> \<Longrightarrow> ptr_val p \<noteq> 0
 2. \<lbrakk>ctcb_ptr_to_tcb_ptr p \<noteq> 0; is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits\<rbrakk> \<Longrightarrow> unat (ptr_val p) + size_of TYPE(tcb_C) \<le> 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctcb_ptr_to_tcb_ptr p \<noteq> 0; is_aligned (ctcb_ptr_to_tcb_ptr p) tcbBlockSizeBits\<rbrakk> \<Longrightarrow> unat (ptr_val p) + size_of TYPE(tcb_C) \<le> 2 ^ LENGTH(32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctcb_ptr_to_tcb_ptr p \<noteq> 0; is_aligned (ptr_val p) ctcb_size_bits\<rbrakk> \<Longrightarrow> unat (ptr_val p) + size_of TYPE(tcb_C) \<le> 2 ^ LENGTH(32) proof (prove)
goal (2 subgoals):
 1. ctcb_ptr_to_tcb_ptr p \<noteq> 0 \<Longrightarrow> ctcb_size_bits < LENGTH(32)
 2. ctcb_ptr_to_tcb_ptr p \<noteq> 0 \<Longrightarrow> size_of TYPE(tcb_C) \<le> 2 ^ ctcb_size_bits proof (state)
this:
c_null_guard p

goal:
No subgoals!