theory Detype_C

lemma valid_untyped_cap_ctcb_member:
  fixes tcb :: tcb
  assumes vu: "s \<turnstile>' UntypedCap d ptr bits idx"
  and   koat: "ko_at' tcb x s"
  and     pv: "ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr .. ptr + 2 ^ bits - 1}"
  shows   "x \<in> {ptr .. ptr + 2 ^ bits - 1}" using vu proof - from vu koat have "{x..x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}" proof (rule valid_untyped_cap_ko_at_disjoint) from koat have "ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}" by (rule tcb_ptr_to_ctcb_ptr_in_range) thus "{x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}" using pv apply - apply rule apply (drule (1) orthD1) apply simp done qed thus ?thesis proof (rule set_mp) from koat have "is_aligned x (objBits tcb)" by (clarsimp elim!: obj_atE' simp: objBits_simps projectKOs) thus "x \<in> {x..x + 2 ^ objBits tcb - 1}" apply (rule base_member_set [simplified field_simps]) apply (simp add: objBits_simps' word_bits_conv) done qed qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<in> {ptr..ptr + 2 ^ bits - 1} proof (prove)
using this:
valid_cap' (capability.UntypedCap d ptr bits idx) s

goal (1 subgoal):
 1. x \<in> {ptr..ptr + 2 ^ bits - 1} proof (state)
goal (1 subgoal):
 1. valid_cap' (capability.UntypedCap d ptr bits idx) s \<Longrightarrow> x \<in> {ptr..ptr + 2 ^ bits - 1} proof (chain)
picking this:
valid_cap' (capability.UntypedCap d ptr bits idx) s
ko_at' tcb x s proof (prove)
using this:
valid_cap' (capability.UntypedCap d ptr bits idx) s
ko_at' tcb x s

goal (1 subgoal):
 1. {x..x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1} proof (state)
goal (1 subgoal):
 1. {x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} proof (chain)
picking this:
ko_at' tcb x s proof (prove)
using this:
ko_at' tcb x s

goal (1 subgoal):
 1. ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1} proof (state)
this:
ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}

goal (1 subgoal):
 1. {x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} proof (prove)
using this:
ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}

goal (1 subgoal):
 1. {x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} proof (prove)
using this:
ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}
ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. {x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}; ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> {x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}; ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr..ptr + 2 ^ bits - 1}; {x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}; ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr..ptr + 2 ^ bits - 1}; ptr_val (tcb_ptr_to_ctcb_ptr x) \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
{x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}

goal:
No subgoals! proof (state)
this:
{x..x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. valid_cap' (capability.UntypedCap d ptr bits idx) s \<Longrightarrow> x \<in> {ptr..ptr + 2 ^ bits - 1} proof (prove)
using this:
{x..x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. x \<in> {ptr..ptr + 2 ^ bits - 1} proof (state)
goal (1 subgoal):
 1. x \<in> {x..x + 2 ^ objBits tcb - 1} proof (chain)
picking this:
ko_at' tcb x s proof (prove)
using this:
ko_at' tcb x s

goal (1 subgoal):
 1. is_aligned x (objBits tcb) proof (state)
this:
is_aligned x (objBits tcb)

goal (1 subgoal):
 1. x \<in> {x..x + 2 ^ objBits tcb - 1} proof (prove)
using this:
is_aligned x (objBits tcb)

goal (1 subgoal):
 1. x \<in> {x..x + 2 ^ objBits tcb - 1} proof (prove)
goal (1 subgoal):
 1. objBits tcb < LENGTH(32) proof (prove)
goal:
No subgoals! proof (state)
this:
x \<in> {x..x + 2 ^ objBits tcb - 1}

goal:
No subgoals! proof (state)
this:
x \<in> {ptr..ptr + 2 ^ bits - 1}

goal:
No subgoals!