theory Detype_C

lemma tcb_queue_relation_live_restrict:
  assumes vuc: "s \<turnstile>' capability.UntypedCap d ptr bits idx"
  and     rel: "\<forall>t \<in> set q. tcb_at' t s"
  and    live: "\<forall>t \<in> set q. ko_wp_at' live' t s"
  and      rl: "\<forall>(p :: word32) P. ko_wp_at' P p s \<and> (\<forall>ko. P ko \<longrightarrow> live' ko) \<longrightarrow> p \<notin> {ptr..ptr + 2 ^ bits - 1}"
  shows "tcb_queue_relation' getNext getPrev (cm |` (- Ptr ` {ptr..+2 ^ bits})) q cend chead =
  tcb_queue_relation' getNext getPrev cm q cend chead" proof (rule tcb_queue_relation'_cong [OF refl refl refl]) fix p assume "p \<in> tcb_ptr_to_ctcb_ptr ` set q" hence pin: "ctcb_ptr_to_tcb_ptr p \<in> set q" by (rule tcb_ptr_to_ctcb_ptr_imageD) with rel have "tcb_at' (ctcb_ptr_to_tcb_ptr p) s" .. then obtain tcb :: tcb where koat: "ko_at' tcb (ctcb_ptr_to_tcb_ptr p) s" by (clarsimp simp: obj_at'_real_def ko_wp_at'_def) from live pin have "ko_wp_at' live' (ctcb_ptr_to_tcb_ptr p) s" .. hence notin: "(ctcb_ptr_to_tcb_ptr p) \<notin> {ptr..ptr + 2 ^ bits - 1}" by (fastforce intro!: rl [rule_format]) from vuc have al: "is_aligned ptr bits" and wb: "bits < word_bits" by (auto elim!: valid_untyped_capE) hence ran': " {ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}" by (simp add: upto_intvl_eq) hence "p \<in> - Ptr ` {ptr..+2 ^ bits}" using vuc koat notin apply - apply (erule contrapos_np) apply (erule (1) valid_untyped_cap_ctcb_member) apply (clarsimp elim!: imageE simp: ran') done thus "(cm |` (- Ptr ` {ptr..+2 ^ bits})) p = cm p" by simp qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_queue_relation' getNext getPrev (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) q cend chead = tcb_queue_relation' getNext getPrev cm q cend chead proof (state)
goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (state)
goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (state)
this:
p \<in> tcb_ptr_to_ctcb_ptr ` set q

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (prove)
using this:
p \<in> tcb_ptr_to_ctcb_ptr ` set q

goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr p \<in> set q proof (state)
this:
ctcb_ptr_to_tcb_ptr p \<in> set q

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (chain)
picking this:
\<forall>t\<in>set q. tcb_at' t s
ctcb_ptr_to_tcb_ptr p \<in> set q proof (prove)
using this:
\<forall>t\<in>set q. tcb_at' t s
ctcb_ptr_to_tcb_ptr p \<in> set q

goal (1 subgoal):
 1. tcb_at' (ctcb_ptr_to_tcb_ptr p) s proof (state)
this:
tcb_at' (ctcb_ptr_to_tcb_ptr p) s

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (chain)
picking this:
tcb_at' (ctcb_ptr_to_tcb_ptr p) s proof (prove)
using this:
tcb_at' (ctcb_ptr_to_tcb_ptr p) s

goal (1 subgoal):
 1. (\<And>tcb. ko_at' tcb (ctcb_ptr_to_tcb_ptr p) s \<Longrightarrow> thesis) \<Longrightarrow> thesis proof (state)
this:
ko_at' tcb (ctcb_ptr_to_tcb_ptr p) s

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (chain)
picking this:
\<forall>t\<in>set q. ko_wp_at' live' t s
ctcb_ptr_to_tcb_ptr p \<in> set q proof (prove)
using this:
\<forall>t\<in>set q. ko_wp_at' live' t s
ctcb_ptr_to_tcb_ptr p \<in> set q

goal (1 subgoal):
 1. ko_wp_at' live' (ctcb_ptr_to_tcb_ptr p) s proof (state)
this:
ko_wp_at' live' (ctcb_ptr_to_tcb_ptr p) s

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (prove)
using this:
ko_wp_at' live' (ctcb_ptr_to_tcb_ptr p) s

goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr p \<notin> {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
ctcb_ptr_to_tcb_ptr p \<notin> {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (chain)
picking this:
valid_cap' (capability.UntypedCap d ptr bits idx) s proof (prove)
using this:
valid_cap' (capability.UntypedCap d ptr bits idx) s

goal (1 subgoal):
 1. is_aligned ptr bits &&& bits < word_bits proof (state)
this:
is_aligned ptr bits
bits < word_bits

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (prove)
using this:
is_aligned ptr bits
bits < word_bits

goal (1 subgoal):
 1. {ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1} proof (state)
this:
{ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (prove)
using this:
{ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. p \<in> - tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
using this:
{ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}
valid_cap' (capability.UntypedCap d ptr bits idx) s
ko_at' tcb (ctcb_ptr_to_tcb_ptr p) s
ctcb_ptr_to_tcb_ptr p \<notin> {ptr..ptr + 2 ^ bits - 1}

goal (1 subgoal):
 1. p \<in> - tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}; valid_cap' (capability.UntypedCap d ptr bits idx) s; ko_at' tcb (ctcb_ptr_to_tcb_ptr p) s; ctcb_ptr_to_tcb_ptr p \<notin> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> p \<in> - tcb_Ptr ` {ptr..+2 ^ bits} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}; valid_cap' (capability.UntypedCap d ptr bits idx) s; ko_at' tcb (ctcb_ptr_to_tcb_ptr p) s; p \<notin> - tcb_Ptr ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> ctcb_ptr_to_tcb_ptr p \<in> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>{ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}; ko_at' tcb (ctcb_ptr_to_tcb_ptr p) s; p \<notin> - tcb_Ptr ` {ptr..+2 ^ bits}\<rbrakk> \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr p)) \<in> {ptr..ptr + 2 ^ bits - 1} proof (prove)
goal:
No subgoals! proof (state)
this:
p \<in> - tcb_Ptr ` {ptr..+2 ^ bits}

goal (1 subgoal):
 1. \<And>p. p \<in> tcb_ptr_to_ctcb_ptr ` set q \<Longrightarrow> (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (prove)
using this:
p \<in> - tcb_Ptr ` {ptr..+2 ^ bits}

goal (1 subgoal):
 1. (cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p proof (state)
this:
(cm|\<^bsub>(- tcb_Ptr ` {ptr..+2 ^ bits})\<^esub>) p = cm p

goal:
No subgoals!