theory Detype_C

lemma tcb_cte_cases_in_range3:
  assumes tc: "tcb_cte_cases (y - x) = Some v"
  and     al: "is_aligned x tcbBlockSizeBits"
  shows   "y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1" proof - note [simp] = objBits_defs ctcb_size_bits_def from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ ctcb_size_bits - 1" unfolding tcb_cte_cases_def by (simp add: diff_eq_eq split: if_split_asm) have "q + (2 ^ cteSizeBits - 1) \<le> (2 ^ ctcb_size_bits - 1) + (2 ^ cteSizeBits - 1)" using qv by (rule word_plus_mcs_3) simp also have "\<dots> \<le> 2 ^ tcbBlockSizeBits - 1" by simp finally have "x + (q + (2 ^ cteSizeBits - 1)) \<le> x + (2 ^ tcbBlockSizeBits - 1)" apply (rule word_plus_mono_right) apply (rule is_aligned_no_overflow' [OF al]) done thus ?thesis using yq by (simp add: field_simps) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (state)
goal (1 subgoal):
 1. y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (state)
this:
tcbBlockSizeBits \<equiv> 9
epSizeBits \<equiv> 4
ntfnSizeBits \<equiv> State_H.wordSizeCase 4 5
cteSizeBits \<equiv> State_H.wordSizeCase 4 5
ctcb_size_bits \<equiv> 8

goal (1 subgoal):
 1. y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (chain)
picking this:
tcb_cte_cases (y - x) = Some v proof (prove)
using this:
tcb_cte_cases (y - x) = Some v

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>y = x + q; q \<le> 2 ^ ctcb_size_bits - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (prove)
using this:
[0 \<mapsto> (tcb.tcbCTable, tcbCTable_update), 0x10 \<mapsto> (tcb.tcbVTable, tcbVTable_update), 0x20 \<mapsto> (tcb.tcbReply, tcbReply_update), 0x30 \<mapsto> (tcb.tcbCaller, tcbCaller_update), 0x40 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update)] (y - x) = Some v

goal (1 subgoal):
 1. (\<And>q. \<lbrakk>y = x + q; q \<le> 2 ^ ctcb_size_bits - 1\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
y = x + q
q \<le> 2 ^ ctcb_size_bits - 1

goal (1 subgoal):
 1. y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (1 subgoal):
 1. q + (2 ^ cteSizeBits - 1) \<le> 2 ^ ctcb_size_bits - 1 + (2 ^ cteSizeBits - 1) proof (prove)
using this:
q \<le> 2 ^ ctcb_size_bits - 1

goal (1 subgoal):
 1. q + (2 ^ cteSizeBits - 1) \<le> 2 ^ ctcb_size_bits - 1 + (2 ^ cteSizeBits - 1) proof (state)
this:
q + (2 ^ cteSizeBits - 1) \<le> 2 ^ ctcb_size_bits - 1 + (2 ^ cteSizeBits - 1)

goal (1 subgoal):
 1. y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (state)
this:
q + (2 ^ cteSizeBits - 1) \<le> 2 ^ ctcb_size_bits - 1 + (2 ^ cteSizeBits - 1)

goal (1 subgoal):
 1. y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (prove)
goal (1 subgoal):
 1. 2 ^ ctcb_size_bits - 1 + (2 ^ cteSizeBits - 1) \<le> 2 ^ tcbBlockSizeBits - 1 proof (state)
this:
2 ^ ctcb_size_bits - 1 + (2 ^ cteSizeBits - 1) \<le> 2 ^ tcbBlockSizeBits - 1

goal (1 subgoal):
 1. y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (chain)
picking this:
q + (2 ^ cteSizeBits - 1) \<le> 2 ^ tcbBlockSizeBits - 1 proof (prove)
using this:
q + (2 ^ cteSizeBits - 1) \<le> 2 ^ tcbBlockSizeBits - 1

goal (1 subgoal):
 1. x + (q + (2 ^ cteSizeBits - 1)) \<le> x + (2 ^ tcbBlockSizeBits - 1) proof (prove)
goal (1 subgoal):
 1. x \<le> x + (2 ^ tcbBlockSizeBits - 1) proof (prove)
goal:
No subgoals! proof (state)
this:
x + (q + (2 ^ cteSizeBits - 1)) \<le> x + (2 ^ tcbBlockSizeBits - 1)

goal (1 subgoal):
 1. y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (prove)
using this:
x + (q + (2 ^ cteSizeBits - 1)) \<le> x + (2 ^ tcbBlockSizeBits - 1)

goal (1 subgoal):
 1. y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (prove)
using this:
x + (q + (2 ^ cteSizeBits - 1)) \<le> x + (2 ^ tcbBlockSizeBits - 1)
y = x + q

goal (1 subgoal):
 1. y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (state)
this:
y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1

goal:
No subgoals!