theory Ipc_DR

lemma dcorres_dummy_corrupt_ipc_buffer:
  "dcorres dc (\<top>) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_ipc_buffer y b) (return x)" apply (clarsimp simp:corrupt_ipc_buffer_def get_ipc_buffer_def) apply (rule dcorres_expand_pfx) apply (clarsimp simp:gets_the_def gets_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (clarsimp simp:tcb_at_def) apply (frule(1) valid_etcbs_get_tcb_get_etcb) apply (subst opt_cap_tcb) apply (simp add:not_idle_thread_def assert_opt_def)+ apply (case_tac "tcb_ipcframe tcb") apply simp_all apply (rule corres_guard_imp[OF dummy_corrupt_tcb_intent_corres]
        ,(clarsimp simp:not_idle_thread_def tcb_at_def)+)+ apply (rename_tac arch_cap etcb) apply (case_tac "arch_cap") apply simp_all apply (rule corres_guard_imp[OF dummy_corrupt_tcb_intent_corres]
        ,(clarsimp simp:not_idle_thread_def tcb_at_def)+)+ apply (clarsimp simp: | rule conjI)+ apply (rule corres_guard_imp[OF dcorres_dummy_corrupt_frame],clarsimp+) apply (clarsimp | rule conjI)+ apply (rule corres_guard_imp[OF dcorres_dummy_corrupt_frame],clarsimp+) apply (rule corres_guard_imp[OF dummy_corrupt_tcb_intent_corres]
    ,(clarsimp simp:not_idle_thread_def tcb_at_def)+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (corrupt_ipc_buffer y b) (return x) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) (do buffer <- do frame_cap <- KHeap_D.get_cap (y, tcb_ipcbuffer_slot);
case frame_cap of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None
od;
case buffer of None \<Rightarrow> corrupt_tcb_intent y | Some a \<Rightarrow> corrupt_frame a
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; (tcb_at y and valid_idle and not_idle_thread y and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (do buffer <- do frame_cap <- KHeap_D.get_cap (y, tcb_ipcbuffer_slot);
case frame_cap of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None
od;
case buffer of None \<Rightarrow> corrupt_tcb_intent y | Some a \<Rightarrow> corrupt_frame a
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>tcb_at y s'; valid_idle s'; not_idle_thread y s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do x <- get;
x <- assert_opt (opt_cap (y, tcb_ipcbuffer_slot) x);
(case x of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>tcb_at y s'; valid_idle s'; not_idle_thread y s'; valid_etcbs s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do x <- assert_opt (opt_cap (y, tcb_ipcbuffer_slot) (transform s'a));
(case x of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s'a tcb. \<lbrakk>valid_idle s'a; not_idle_thread y s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do x <- assert_opt (opt_cap (y, tcb_ipcbuffer_slot) (transform s'a));
(case x of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s'a tcb. \<lbrakk>valid_idle s'a; not_idle_thread y s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do x <- assert_opt (opt_cap (y, tcb_ipcbuffer_slot) (transform s'a));
(case x of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame
od) (return x) proof (prove)
goal (4 subgoals):
 1. \<And>s'a tcb. \<lbrakk>valid_idle s'a; not_idle_thread y s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> get_tcb y s'a = Some (?tcb13 s'a tcb)
 2. \<And>s'a tcb. \<lbrakk>valid_idle s'a; not_idle_thread y s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb y s'a = Some etcb
 3. \<And>s'a tcb. \<lbrakk>valid_idle s'a; not_idle_thread y s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s'a
 4. \<And>s'a tcb. \<lbrakk>valid_idle s'a; not_idle_thread y s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (do x <- assert_opt (if tcb_ipcbuffer_slot \<in> tcb_abstract_slots then map_option (\<lambda>(getF, uu_, uu_). transform_cap (getF (?tcb13 s'a tcb))) (tcb_cap_cases (tcb_cnode_index tcb_ipcbuffer_slot)) else if tcb_ipcbuffer_slot = tcb_pending_op_slot then Some (infer_tcb_pending_op y (tcb_state (?tcb13 s'a tcb))) else if tcb_ipcbuffer_slot = tcb_boundntfn_slot then Some (infer_tcb_bound_notification (tcb_bound_notification (?tcb13 s'a tcb))) else None);
(case x of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame
od) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s'a tcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x) proof (prove)
goal (12 subgoals):
 1. \<And>s'a tcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 2. \<And>s'a tcb x21 x22 x23 x24. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 3. \<And>s'a tcb x31 x32 x33. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 4. \<And>s'a tcb x41 x42 x43. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 5. \<And>s'a tcb x51 x52 x53. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 6. \<And>s'a tcb x61 x62 x63. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 7. \<And>s'a tcb x7. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 8. \<And>s'a tcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 9. \<And>s'a tcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 10. \<And>s'a tcb x10. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (tcb_ipcframe tcb) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>s'a tcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 2. \<And>s'a tcb x21 x22 x23 x24. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 3. \<And>s'a tcb x31 x32 x33. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 4. \<And>s'a tcb x41 x42 x43. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 5. \<And>s'a tcb x51 x52 x53. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 6. \<And>s'a tcb x61 x62 x63. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 7. \<And>s'a tcb x7. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = ThreadCap x7\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 8. \<And>s'a tcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = cap.DomainCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 9. \<And>s'a tcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = IRQControlCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 10. \<And>s'a tcb x10. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; \<exists>etcb. get_etcb y s'a = Some etcb; tcb_ipcframe tcb = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s'a tcb x12 etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap x12; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (ArchObjectCap x12) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x) proof (prove)
goal (1 subgoal):
 1. \<And>s'a tcb arch_cap etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap arch_cap; get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (ArchObjectCap arch_cap) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x) proof (prove)
goal (5 subgoals):
 1. \<And>s'a tcb arch_cap etcb x11 x12. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap arch_cap; get_etcb y s'a = Some etcb; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (ArchObjectCap arch_cap) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 2. \<And>s'a tcb arch_cap etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap arch_cap; get_etcb y s'a = Some etcb; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (ArchObjectCap arch_cap) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 3. \<And>s'a tcb arch_cap etcb x31 x32 x33 x34 x35. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap arch_cap; get_etcb y s'a = Some etcb; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (ArchObjectCap arch_cap) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 4. \<And>s'a tcb arch_cap etcb x41 x42. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap arch_cap; get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (ArchObjectCap arch_cap) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x)
 5. \<And>s'a tcb arch_cap etcb x51 x52. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap arch_cap; get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) ((case transform_cap (ArchObjectCap arch_cap) of FrameCap x a rights xa xb xc \<Rightarrow> if AllowWrite \<in> rights \<and> AllowRead \<in> rights \<or> AllowRead \<in> rights \<and> \<not> b then return (Some a) else return None | _ \<Rightarrow> return None) >>= case_option (corrupt_tcb_intent y) corrupt_frame) (return x) proof (prove)
goal (5 subgoals):
 1. \<And>s'a tcb arch_cap etcb x11 x12. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (ASIDPoolCap x11 x12); get_etcb y s'a = Some etcb; arch_cap = ASIDPoolCap x11 x12\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 2. \<And>s'a tcb arch_cap etcb. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap ASIDControlCap; get_etcb y s'a = Some etcb; arch_cap = ASIDControlCap\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 3. \<And>s'a tcb arch_cap etcb x31 x32 x33 x34 x35. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 x32 x33 x34 x35); get_etcb y s'a = Some etcb; arch_cap = PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33 \<and> AllowRead \<in> x33 \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_frame x32) (return x)) \<and> (AllowRead \<in> x33 \<and> \<not> b \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_frame x32) (return x)) \<and> ((AllowWrite \<in> x33 \<longrightarrow> AllowRead \<notin> x33) \<and> (AllowRead \<in> x33 \<longrightarrow> b) \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x))
 4. \<And>s'a tcb arch_cap etcb x41 x42. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageTableCap x41 x42); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 5. \<And>s'a tcb arch_cap etcb x51 x52. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x) proof (prove)
goal (3 subgoals):
 1. \<And>s'a tcb etcb x31 x32 x33 x34 x35. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 x32 x33 x34 x35); get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33 \<and> AllowRead \<in> x33 \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_frame x32) (return x)) \<and> (AllowRead \<in> x33 \<and> \<not> b \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_frame x32) (return x)) \<and> ((AllowWrite \<in> x33 \<longrightarrow> AllowRead \<notin> x33) \<and> (AllowRead \<in> x33 \<longrightarrow> b) \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x))
 2. \<And>s'a tcb arch_cap etcb x41 x42. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageTableCap x41 x42); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 3. \<And>s'a tcb arch_cap etcb x51 x52. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x) proof (prove)
goal (4 subgoals):
 1. \<And>s'a tcb etcb x31 x32 x33 x34 x35. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 x32 x33 x34 x35); get_etcb y s'a = Some etcb; AllowWrite \<in> x33; AllowRead \<in> x33\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_frame x32) (return x)
 2. \<And>s'a tcb etcb x31 x32 x33 x34 x35. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 x32 x33 x34 x35); get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> (AllowRead \<in> x33 \<and> \<not> b \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_frame x32) (return x)) \<and> ((AllowWrite \<in> x33 \<longrightarrow> AllowRead \<notin> x33) \<and> (AllowRead \<in> x33 \<longrightarrow> b) \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x))
 3. \<And>s'a tcb arch_cap etcb x41 x42. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageTableCap x41 x42); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 4. \<And>s'a tcb arch_cap etcb x51 x52. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x) proof (prove)
goal (3 subgoals):
 1. \<And>s'a tcb etcb x31 x32 x33 x34 x35. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 x32 x33 x34 x35); get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> (AllowRead \<in> x33 \<and> \<not> b \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_frame x32) (return x)) \<and> ((AllowWrite \<in> x33 \<longrightarrow> AllowRead \<notin> x33) \<and> (AllowRead \<in> x33 \<longrightarrow> b) \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x))
 2. \<And>s'a tcb arch_cap etcb x41 x42. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageTableCap x41 x42); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 3. \<And>s'a tcb arch_cap etcb x51 x52. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x) proof (prove)
goal (4 subgoals):
 1. \<And>s'a tcb etcb x31 x32 x33 x34 x35. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 x32 x33 x34 x35); get_etcb y s'a = Some etcb; AllowRead \<in> x33; \<not> b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_frame x32) (return x)
 2. \<And>s'a tcb etcb x31 x32 x33 x34 x35. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 x32 x33 x34 x35); get_etcb y s'a = Some etcb\<rbrakk> \<Longrightarrow> (AllowWrite \<in> x33 \<longrightarrow> AllowRead \<notin> x33) \<and> (AllowRead \<in> x33 \<longrightarrow> b) \<longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 3. \<And>s'a tcb arch_cap etcb x41 x42. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageTableCap x41 x42); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 4. \<And>s'a tcb arch_cap etcb x51 x52. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x) proof (prove)
goal (3 subgoals):
 1. \<And>s'a tcb etcb x31 x32 x33 x34 x35. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (PageCap x31 x32 x33 x34 x35); get_etcb y s'a = Some etcb; AllowWrite \<in> x33 \<longrightarrow> AllowRead \<notin> x33; AllowRead \<in> x33 \<longrightarrow> b\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 2. \<And>s'a tcb arch_cap etcb x41 x42. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageTableCap x41 x42); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x)
 3. \<And>s'a tcb arch_cap etcb x51 x52. \<lbrakk>valid_idle s'a; y \<noteq> idle_thread s'a; valid_etcbs s'a; get_tcb y s'a = Some tcb; tcb_ipcframe tcb = ArchObjectCap (arch_cap.PageDirectoryCap x51 x52); get_etcb y s'a = Some etcb; arch_cap = arch_cap.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s'a)) ((=) s'a) (corrupt_tcb_intent y) (return x) proof (prove)
goal:
No subgoals!