theory Intent_DR

lemma set_mrs_corres_no_recv_buffer:
  "dcorres dc \<top> (valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (set_mrs y None msg)" apply (clarsimp simp:set_mrs_def get_thread_def arch_tcb_update_aux3 arch_tcb_set_registers_def) apply (rule dcorres_absorb_gets_the, clarsimp) apply (drule(1) valid_etcbs_get_tcb_get_etcb) apply (rule corres_dummy_return_l) apply (rule corres_split_forwards' [where Q'="%x. \<top>" and Q="%x. \<top>"]) apply (rule set_cxt_none_det_intent_corres) apply (simp add:get_tcb_def get_etcb_def
                  split:option.splits Structures_A.kernel_object.splits
               | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (set_mrs y None msg) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_idle and not_idle_thread y and valid_etcbs) (corrupt_tcb_intent y) (do tcb <- gets_the (get_tcb y);
y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length msg) msg_registers) then msg ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch tcb) reg)) tcb));
return (word_of_nat (min (length msg_registers) (length msg)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent y) (do y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length msg) msg_registers) then msg ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj'));
return (word_of_nat (min (length msg_registers) (length msg)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent y) (do y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length msg) msg_registers) then msg ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj'));
return (word_of_nat (min (length msg_registers) (length msg)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent y >>= return) (do y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length msg) msg_registers) then msg ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj'));
return (word_of_nat (min (length msg_registers) (length msg)))
od) proof (prove)
goal (4 subgoals):
 1. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> dcorres (?r'9 s' obj') ((=) (transform s')) ((=) s') (corrupt_tcb_intent y) (KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length msg) msg_registers) then msg ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')))
 2. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>x _. True\<rbrace>
 3. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length msg) msg_registers) then msg ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>\<lambda>x _. True\<rbrace>
 4. \<And>s' obj' x ya. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb; ?r'9 s' obj' x ya\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (return (word_of_nat (min (length msg_registers) (length msg)))) proof (prove)
goal (7 subgoals):
 1. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> kheap s' y = Some (TCB obj')
 2. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> ekheap s' y \<noteq> None
 3. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> valid_idle s'
 4. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> not_idle_thread y s'
 5. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>x _. True\<rbrace>
 6. \<And>s' obj'. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set (\<lambda>reg. if reg \<in> set (take (length msg) msg_registers) then msg ! the_index msg_registers reg else arch_tcb_get_registers (tcb_arch obj') reg)) obj')) \<lbrace>\<lambda>x _. True\<rbrace>
 7. \<And>s' obj' x ya. \<lbrakk>get_tcb y s' = Some obj'; valid_idle s'; not_idle_thread y s'; \<exists>etcb. get_etcb y s' = Some etcb; dc x ya\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return x) (return (word_of_nat (min (length msg_registers) (length msg)))) proof (prove)
goal:
No subgoals!