theory Intent_DR

lemma corrupt_tcb_intent_as_user_corres:
  "dcorres dc \<top> (valid_idle and not_idle_thread y and valid_etcbs)
     (corrupt_tcb_intent y) (as_user y t)" apply (clarsimp simp:as_user_def) apply (rule dcorres_absorb_gets_the) apply (clarsimp simp:get_tcb_def arch_tcb_update_aux3
                  split:option.splits Structures_A.kernel_object.splits) apply (rule corres_symb_exec_r) apply clarsimp apply (rule corres_dummy_return_l) apply (rule corres_underlying_split) apply (drule(1) valid_etcbs_tcb_etcb) apply (rule set_cxt_none_det_intent_corres; simp) apply (rule corres_return_trivial) apply wpsimp+ 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) (as_user y t) 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);
(a, uc') <- select_f (t (arch_tcb_context_get (tcb_arch tcb)));
y <- KHeap_A.set_object y (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>(valid_idle and not_idle_thread y and valid_etcbs) s'; get_tcb y s' = Some obj'; True\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent y) (do (a, uc') <- select_f (t (arch_tcb_context_get (tcb_arch obj')));
y <- KHeap_A.set_object y (TCB (obj'\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch obj')\<rparr>));
return a
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent y) (do (a, uc') <- select_f (t (arch_tcb_context_get (tcb_arch obj')));
y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set uc') obj'));
return a
od) proof (prove)
goal (4 subgoals):
 1. \<And>s' obj' rv. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'46 s' obj' rv) (corrupt_tcb_intent y) (case rv of (a, uc') \<Rightarrow> do y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set uc') obj'));
return a
od)
 2. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>?Q'46 s' obj'\<rbrace>
 3. \<And>s' obj' s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (select_f (t (arch_tcb_context_get (tcb_arch obj')))) proof (prove)
goal (4 subgoals):
 1. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'46 s' obj' (a, b)) (corrupt_tcb_intent y) (do y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set b) obj'));
return a
od)
 2. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>?Q'46 s' obj'\<rbrace>
 3. \<And>s' obj' s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (select_f (t (arch_tcb_context_get (tcb_arch obj')))) proof (prove)
goal (4 subgoals):
 1. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) (?Q'46 s' obj' (a, b)) (corrupt_tcb_intent y >>= return) (do y <- KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set b) obj'));
return a
od)
 2. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>?Q'46 s' obj'\<rbrace>
 3. \<And>s' obj' s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (select_f (t (arch_tcb_context_get (tcb_arch obj')))) proof (prove)
goal (7 subgoals):
 1. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> dcorres (?r'55 s' obj' a b) ((=) (transform s')) (?Q'46 s' obj' (a, b)) (corrupt_tcb_intent y) (KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set b) obj')))
 2. \<And>s' obj' a b x rv'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); ?r'55 s' obj' a b x rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q55 s' obj' a b x) (?Q'55 s' obj' a b rv') (return x) (return a)
 3. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> corrupt_tcb_intent y \<lbrace>?Q55 s' obj' a b\<rbrace>
 4. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'46 s' obj' (a, b)\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set b) obj')) \<lbrace>?Q'55 s' obj' a b\<rbrace>
 5. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>?Q'46 s' obj'\<rbrace>
 6. \<And>s' obj' s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (select_f (t (arch_tcb_context_get (tcb_arch obj')))) proof (prove)
goal (7 subgoals):
 1. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; kheap s' y = Some (TCB obj'); \<exists>etcb. ekheap s' y = Some etcb\<rbrakk> \<Longrightarrow> dcorres (?r'55 s' obj' a b) ((=) (transform s')) (?Q'46 s' obj' (a, b)) (corrupt_tcb_intent y) (KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set b) obj')))
 2. \<And>s' obj' a b x rv'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); ?r'55 s' obj' a b x rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q55 s' obj' a b x) (?Q'55 s' obj' a b rv') (return x) (return a)
 3. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> corrupt_tcb_intent y \<lbrace>?Q55 s' obj' a b\<rbrace>
 4. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>?Q'46 s' obj' (a, b)\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set b) obj')) \<lbrace>?Q'55 s' obj' a b\<rbrace>
 5. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>?Q'46 s' obj'\<rbrace>
 6. \<And>s' obj' s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (select_f (t (arch_tcb_context_get (tcb_arch obj')))) proof (prove)
goal (6 subgoals):
 1. \<And>s' obj' a b x rv'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); dc x rv'\<rbrakk> \<Longrightarrow> dcorres dc (?Q55 s' obj' a b x) (?Q'55 s' obj' a b rv') (return x) (return a)
 2. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> corrupt_tcb_intent y \<lbrace>?Q55 s' obj' a b\<rbrace>
 3. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set b) obj')) \<lbrace>?Q'55 s' obj' a b\<rbrace>
 4. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>\<lambda>a. (=) s'\<rbrace>
 5. \<And>s' obj' s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (select_f (t (arch_tcb_context_get (tcb_arch obj')))) proof (prove)
goal (5 subgoals):
 1. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) (transform s')\<rbrace> corrupt_tcb_intent y \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>s' obj' a b. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> KHeap_A.set_object y (TCB (tcb_arch_update (arch_tcb_context_set b) obj')) \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj')\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>\<lambda>a. (=) s'\<rbrace>
 4. \<And>s' obj' s. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); s' = s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> select_f (t (arch_tcb_context_get (tcb_arch obj'))) \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>s' obj'. \<lbrakk>valid_idle s'; not_idle_thread y s'; valid_etcbs s'; kheap s' y = Some (TCB obj'); False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (select_f (t (arch_tcb_context_get (tcb_arch obj')))) proof (prove)
goal:
No subgoals!