theory Ipc_DR

lemma dcorres_dat:
  "dcorres dc \<top> (valid_etcbs and not_idle_thread a and valid_idle)
           (do_notification_transfer a)
           (do y \<leftarrow> set_thread_state a Structures_A.thread_state.Running;
               y \<leftarrow> as_user a (set_register badge_register badge);
               possible_switch_to a
            od)" apply (simp add: Endpoint_D.do_notification_transfer_def) apply (rule dcorres_expand_pfx) apply clarsimp apply (rule corres_guard_imp) apply (rule dcorres_dc_rhs_noop_below_2_True[OF allI[OF possible_switch_to_dcorres]]) apply (rule corres_split[OF set_thread_state_corres]) apply (rule set_register_corres) apply (wp)+ apply simp apply (clarsimp simp: not_idle_thread_def valid_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_etcbs and not_idle_thread a and valid_idle) (do_notification_transfer a) (do y <- set_thread_state a Running;
y <- as_user a (set_register badge_register badge);
possible_switch_to a
od) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (valid_etcbs and not_idle_thread a and valid_idle) (do y <- KHeap_D.set_cap (a, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent a
od) (do y <- set_thread_state a Running;
y <- as_user a (set_register badge_register badge);
possible_switch_to a
od) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>s = transform s'; True; (valid_etcbs and not_idle_thread a and valid_idle) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (do y <- KHeap_D.set_cap (a, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent a
od) (do y <- set_thread_state a Running;
y <- as_user a (set_register badge_register badge);
possible_switch_to a
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (do y <- KHeap_D.set_cap (a, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent a
od) (do y <- set_thread_state a Running;
y <- as_user a (set_register badge_register badge);
possible_switch_to a
od) proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q5 s') (?Q'5 s') (do y <- KHeap_D.set_cap (a, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent a
od) (do y <- set_thread_state a Running;
y <- as_user a (set_register badge_register badge);
possible_switch_to a
od)
 2. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q5 s' s
 3. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'5 s' s proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q5 s') (?Q'5 s') (do y <- KHeap_D.set_cap (a, tcb_pending_op_slot) RunningCap;
corrupt_tcb_intent a
od) (do x <- set_thread_state a Running;
as_user a (set_register badge_register badge)
od)
 2. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q5 s' s
 3. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'5 s' s proof (prove)
goal (5 subgoals):
 1. \<And>s' y x. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; dc y x\<rbrakk> \<Longrightarrow> dcorres dc (?R14 s' y) (?R'14 s' x) (corrupt_tcb_intent a) (as_user a (set_register badge_register badge))
 2. \<And>s'. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 s'\<rbrace> KHeap_D.set_cap (a, tcb_pending_op_slot) RunningCap \<lbrace>?R14 s'\<rbrace>
 3. \<And>s'. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 s'\<rbrace> set_thread_state a Running \<lbrace>?R'14 s'\<rbrace>
 4. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q14 s') s
 5. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread a and K (RunningCap = infer_tcb_pending_op a Running) and valid_etcbs and ?Q'14 s') s proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 s'\<rbrace> KHeap_D.set_cap (a, tcb_pending_op_slot) RunningCap \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>s'. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 s'\<rbrace> set_thread_state a Running \<lbrace>\<lambda>x. valid_idle and not_idle_thread a and valid_etcbs\<rbrace>
 3. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q14 s') s
 4. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread a and K (RunningCap = infer_tcb_pending_op a Running) and valid_etcbs and ?Q'14 s') s proof (prove)
goal (2 subgoals):
 1. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True)) s
 2. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread a and K (RunningCap = infer_tcb_pending_op a Running) and valid_etcbs and (\<lambda>s. (valid_idle and (\<lambda>s. a = idle_thread s \<longrightarrow> idle Running)) s \<and> not_idle_thread a s \<and> valid_etcbs s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s' s. \<lbrakk>valid_etcbs s'; not_idle_thread a s'; valid_idle s'; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread a and K (RunningCap = infer_tcb_pending_op a Running) and valid_etcbs and (\<lambda>s. (valid_idle and (\<lambda>s. a = idle_thread s \<longrightarrow> idle Running)) s \<and> not_idle_thread a s \<and> valid_etcbs s)) s proof (prove)
goal:
No subgoals!