theory Tcb_R

lemma decodeUnbindNotification_corres:
  "corres (ser \<oplus> tcbinv_relation)
      (tcb_at t)
      (tcb_at' t)
     (decode_unbind_notification (cap.ThreadCap t))
     (decodeUnbindNotification (capability.ThreadCap t))" apply (simp add: decode_unbind_notification_def decodeUnbindNotification_def) apply (rule corres_guard_imp) apply (rule corres_split_eqrE) apply simp apply (rule getBoundNotification_corres) apply (rule corres_trivial) apply (simp split: option.splits) apply (simp add: returnOk_def) apply wp+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t) (decode_unbind_notification (cap.ThreadCap t)) (decodeUnbindNotification (capability.ThreadCap t)) proof (prove)
goal (1 subgoal):
 1. corres (ser \<oplus> tcbinv_relation) (tcb_at t) (tcb_at' t) (doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (tcb_invocation.NotificationControl t None)
odE) (doE ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl t None)
odE) proof (prove)
goal (3 subgoals):
 1. corres (ser \<oplus> tcbinv_relation) ?Q4 ?Q'4 (doE nTFN <- liftE (get_bound_notification t);
y <- case nTFN of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (tcb_invocation.NotificationControl t None)
odE) (doE ntfn <- liftE (getBoundNotification t);
y <- case ntfn of None \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl t None)
odE)
 2. \<And>s. tcb_at t s \<Longrightarrow> ?Q4 s
 3. \<And>s. tcb_at' t s \<Longrightarrow> ?Q'4 s proof (prove)
goal (6 subgoals):
 1. corres (ser \<oplus> (=)) ?P8 ?P'8 (liftE (get_bound_notification t)) (liftE (getBoundNotification t))
 2. \<And>nTFN. corres (ser \<oplus> tcbinv_relation) (?R8 nTFN) (?R'8 nTFN) (doE y <- case nTFN of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (tcb_invocation.NotificationControl t None)
odE) (doE y <- case nTFN of None \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl t None)
odE)
 3. \<lbrace>?Q8\<rbrace> liftE (get_bound_notification t) \<lbrace>?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> liftE (getBoundNotification t) \<lbrace>?R'8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. tcb_at t s \<Longrightarrow> (?P8 and ?Q8) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (6 subgoals):
 1. corres (=) ?P8 ?P'8 (get_bound_notification t) (getBoundNotification t)
 2. \<And>nTFN. corres (ser \<oplus> tcbinv_relation) (?R8 nTFN) (?R'8 nTFN) (doE y <- case nTFN of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (tcb_invocation.NotificationControl t None)
odE) (doE y <- case nTFN of None \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl t None)
odE)
 3. \<lbrace>?Q8\<rbrace> liftE (get_bound_notification t) \<lbrace>?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Q'8\<rbrace> liftE (getBoundNotification t) \<lbrace>?R'8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. tcb_at t s \<Longrightarrow> (?P8 and ?Q8) s
 6. \<And>s. tcb_at' t s \<Longrightarrow> (?P'8 and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>nTFN. corres (ser \<oplus> tcbinv_relation) (?R8 nTFN) (?R'8 nTFN) (doE y <- case nTFN of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (tcb_invocation.NotificationControl t None)
odE) (doE y <- case nTFN of None \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl t None)
odE)
 2. \<lbrace>?Q8\<rbrace> liftE (get_bound_notification t) \<lbrace>?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> liftE (getBoundNotification t) \<lbrace>?R'8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q8) s
 5. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>nTFN. corres (ser \<oplus> tcbinv_relation) (\<lambda>_. True) (\<lambda>_. True) (doE y <- case nTFN of None \<Rightarrow> throwError ExceptionTypes_A.syscall_error.IllegalOperation | Some x \<Rightarrow> returnOk ();
returnOk (tcb_invocation.NotificationControl t None)
odE) (doE y <- case nTFN of None \<Rightarrow> throwError Fault_H.syscall_error.IllegalOperation | Some v15 \<Rightarrow> returnOk ();
returnOk (tcbinvocation.NotificationControl t None)
odE)
 2. \<lbrace>?Q8\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q8) s
 5. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>nTFN. (\<exists>x2. nTFN = Some x2) \<longrightarrow> corres (ser \<oplus> tcbinv_relation) (\<lambda>_. True) (\<lambda>_. True) (returnOk (tcb_invocation.NotificationControl t None)) (returnOk (tcbinvocation.NotificationControl t None))
 2. \<lbrace>?Q8\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q8) s
 5. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'8) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q8\<rbrace> liftE (get_bound_notification t) \<lbrace>\<lambda>nTFN _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrace>?Q'8\<rbrace> liftE (getBoundNotification t) \<lbrace>\<lambda>nTFN _. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and ?Q8) s
 4. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and ?Q'8) s proof (prove)
goal (2 subgoals):
 1. \<And>s. tcb_at t s \<Longrightarrow> (tcb_at t and (\<lambda>s. True \<and> True)) s
 2. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and (\<lambda>s. True \<and> True)) s proof (prove)
goal:
No subgoals!