theory Detype_C

lemma tcb_ptr_to_ctcb_ptr_in_range':
  fixes tcb :: tcb
  assumes al: "is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits"
  shows "{ptr_val x ..+ size_of TYPE (tcb_C)}
          \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb}" proof - from al have "ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ tcbBlockSizeBits - 1" by (rule is_aligned_no_overflow) moreover from al have "ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ ctcb_size_bits" by (rule is_aligned_no_wrap') (simp add: ctcb_size_bits_def objBits_defs) moreover from al have "is_aligned (ptr_val x) ctcb_size_bits" by (rule ctcb_ptr_to_tcb_ptr_aligned) moreover from al have "{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} = {ctcb_ptr_to_tcb_ptr x.. ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}" apply - apply (rule upto_intvl_eq) apply (simp add: objBits_simps') done ultimately show ?thesis unfolding ctcb_ptr_to_tcb_ptr_def ctcb_offset_defs apply - apply (clarsimp simp: field_simps objBits_simps' size_of_def) apply (drule intvlD) apply clarsimp apply (rule conjI) apply (erule order_trans, erule is_aligned_no_wrap') apply (rule of_nat_power) apply simp apply simp apply (rule word_plus_mono_right) apply (simp add: word_le_nat_alt unat_of_nat) apply (erule is_aligned_no_wrap') apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (state)
goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (chain)
picking this:
is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits proof (prove)
using this:
is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits

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

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (state)
this:
ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ tcbBlockSizeBits - 1

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (chain)
picking this:
is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits proof (prove)
using this:
is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits

goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ ctcb_size_bits proof (state)
this:
ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ ctcb_size_bits

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (state)
this:
ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ ctcb_size_bits

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (chain)
picking this:
is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits proof (prove)
using this:
is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits

goal (1 subgoal):
 1. is_aligned (ptr_val x) ctcb_size_bits proof (state)
this:
is_aligned (ptr_val x) ctcb_size_bits

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (state)
this:
is_aligned (ptr_val x) ctcb_size_bits

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (chain)
picking this:
is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits proof (prove)
using this:
is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits

goal (1 subgoal):
 1. {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} = {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} proof (prove)
goal (1 subgoal):
 1. is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits \<Longrightarrow> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} = {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} proof (prove)
goal (1 subgoal):
 1. is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits \<Longrightarrow> is_aligned (ctcb_ptr_to_tcb_ptr x) (objBits tcb) proof (prove)
goal:
No subgoals! proof (state)
this:
{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} = {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (chain)
picking this:
ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ tcbBlockSizeBits - 1
ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ ctcb_size_bits
is_aligned (ptr_val x) ctcb_size_bits
{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} = {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1} proof (prove)
using this:
ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ tcbBlockSizeBits - 1
ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ ctcb_size_bits
is_aligned (ptr_val x) ctcb_size_bits
{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} = {ctcb_ptr_to_tcb_ptr x..ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} proof (prove)
using this:
ptr_val x - 2 ^ 8 \<le> ptr_val x - 2 ^ 8 + 2 ^ tcbBlockSizeBits - 1
ptr_val x - 2 ^ 8 \<le> ptr_val x - 2 ^ 8 + 2 ^ 8
is_aligned (ptr_val x) 8
{ptr_val x - 2 ^ 8..+2 ^ objBits tcb} = {ptr_val x - 2 ^ 8..ptr_val x - 2 ^ 8 + 2 ^ objBits tcb - 1}

goal (1 subgoal):
 1. ptr_span x \<subseteq> {ptr_val x - 2 ^ 8..+2 ^ objBits tcb} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr_val x - 2 ^ 8 \<le> ptr_val x - 2 ^ 8 + 2 ^ tcbBlockSizeBits - 1; ptr_val x - 2 ^ 8 \<le> ptr_val x - 2 ^ 8 + 2 ^ 8; is_aligned (ptr_val x) 8; {ptr_val x - 2 ^ 8..+2 ^ objBits tcb} = {ptr_val x - 2 ^ 8..ptr_val x - 2 ^ 8 + 2 ^ objBits tcb - 1}\<rbrakk> \<Longrightarrow> ptr_span x \<subseteq> {ptr_val x - 2 ^ 8..+2 ^ objBits tcb} proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; xa \<in> {ptr_val x..+152}\<rbrakk> \<Longrightarrow> ptr_val x - 0x100 \<le> xa \<and> xa \<le> ptr_val x + 0xFF proof (prove)
goal (1 subgoal):
 1. \<And>xa. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; \<exists>k. xa = ptr_val x + word_of_nat k \<and> k < 152\<rbrakk> \<Longrightarrow> ptr_val x - 0x100 \<le> xa \<and> xa \<le> ptr_val x + 0xFF proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> ptr_val x - 0x100 \<le> ptr_val x + word_of_nat k \<and> ptr_val x + word_of_nat k \<le> ptr_val x + 0xFF proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> ptr_val x - 0x100 \<le> ptr_val x + word_of_nat k
 2. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> ptr_val x + word_of_nat k \<le> ptr_val x + 0xFF proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> word_of_nat k < 2 ^ 8
 2. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> ptr_val x + word_of_nat k \<le> ptr_val x + 0xFF proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> k < 2 ^ 8
 2. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> 8 < LENGTH(32)
 3. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> ptr_val x + word_of_nat k \<le> ptr_val x + 0xFF proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> 8 < LENGTH(32)
 2. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> ptr_val x + word_of_nat k \<le> ptr_val x + 0xFF proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> ptr_val x + word_of_nat k \<le> ptr_val x + 0xFF proof (prove)
goal (2 subgoals):
 1. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> word_of_nat k \<le> 0xFF
 2. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> ptr_val x \<le> ptr_val x + 0xFF proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; is_aligned (ptr_val x) 8; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> ptr_val x \<le> ptr_val x + 0xFF proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>ptr_val x - 0x100 \<le> ptr_val x + 0xFF; ptr_val x - 0x100 \<le> ptr_val x; {ptr_val x - 0x100..+512} = {ptr_val x - 0x100..ptr_val x + 0xFF}; k < 152\<rbrakk> \<Longrightarrow> 0xFF < 2 ^ 8 proof (prove)
goal:
No subgoals! proof (state)
this:
ptr_span x \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb}

goal:
No subgoals!