theory ArchFinalise_AI

lemma suspend_unlive':
  "\<lbrace>bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t \<rbrace>
      suspend t
   \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) t\<rbrace>" apply (simp add: suspend_def set_thread_state_def set_object_def get_object_def) supply hoare_vcg_if_split[wp_split del] if_split[split del] apply (wp | simp only: obj_at_exst_update)+ apply (simp add: obj_at_def live_def hyp_live_def) apply (rule_tac Q="\<lambda>_. bound_tcb_at ((=) None) t" in hoare_strengthen_post) supply hoare_vcg_if_split[wp_split] apply wp apply (auto simp: pred_tcb_def2)[1] apply (simp flip: if_split) apply wp apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t\<rbrace> suspend t \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t\<rbrace> do y <- cancel_ipc t;
state <- get_thread_state t;
y <- if state = Running then update_restart_pc t else return ();
y <- do tcb <- gets_the (get_tcb t);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := Inactive\<rparr>))\<rparr>)
od;
do_extended_op (set_thread_state_ext t)
od;
do_extended_op (tcb_sched_action tcb_sched_dequeue t)
od \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t\<rbrace> do y <- cancel_ipc t;
state <- get_thread_state t;
y <- if state = Running then update_restart_pc t else return ();
y <- do tcb <- gets_the (get_tcb t);
y <- do kobj <- do kh <- gets kheap;
y <- assert (\<exists>y. kh t = Some y);
return (the (kh t))
od;
y <- assert (a_type kobj = ATCB);
s <- get;
put (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := Inactive\<rparr>))\<rparr>)
od;
do_extended_op (set_thread_state_ext t)
od;
do_extended_op (tcb_sched_action tcb_sched_dequeue t)
od \<lbrace>\<lambda>rv. obj_at (Not \<circ> live) t\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y state. \<lbrace>?B2 y state\<rbrace> if state = Running then update_restart_pc t else return () \<lbrace>\<lambda>ya s. get_tcb t s \<noteq> None \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> obj_at (Not \<circ> live) t (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (the (get_tcb t s)\<lparr>tcb_state := Inactive\<rparr>))\<rparr>)\<rbrace>
 2. \<And>y. \<lbrace>?B1 y\<rbrace> get_thread_state t \<lbrace>?B2 y\<rbrace>
 3. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 4. \<And>s. (bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>state. \<lbrace>?B2 () state\<rbrace> if state = Running then update_restart_pc t else return () \<lbrace>\<lambda>ya s. (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> tcb_bound_notification (the (get_tcb t s)) = None\<rbrace>
 2. \<And>y. \<lbrace>?B1 y\<rbrace> get_thread_state t \<lbrace>?B2 y\<rbrace>
 3. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 4. \<And>s. (bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>state. \<lbrace>?B2 () state\<rbrace> if state = Running then update_restart_pc t else return () \<lbrace>\<lambda>_. bound_tcb_at ((=) None) t\<rbrace>
 2. \<And>state rv s. bound_tcb_at ((=) None) t s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> tcb_bound_notification (the (get_tcb t s)) = None
 3. \<And>y. \<lbrace>?B1 y\<rbrace> get_thread_state t \<lbrace>?B2 y\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 5. \<And>s. (bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>state. \<lbrace>?B2 () state\<rbrace> if state = Running then update_restart_pc t else return () \<lbrace>\<lambda>_. bound_tcb_at ((=) None) t\<rbrace>
 2. \<And>state rv s. bound_tcb_at ((=) None) t s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> tcb_bound_notification (the (get_tcb t s)) = None
 3. \<And>y. \<lbrace>?B1 y\<rbrace> get_thread_state t \<lbrace>?B2 y\<rbrace>
 4. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 5. \<And>s. (bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>state rv s. bound_tcb_at ((=) None) t s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> (\<exists>y. kheap s t = Some y) \<longrightarrow> a_type (the (kheap s t)) = ATCB \<longrightarrow> tcb_bound_notification (the (get_tcb t s)) = None
 2. \<And>y. \<lbrace>?B1 y\<rbrace> get_thread_state t \<lbrace>\<lambda>a b. (a = Running \<longrightarrow> bound_tcb_at ((=) None) t b) \<and> (a \<noteq> Running \<longrightarrow> bound_tcb_at ((=) None) t b)\<rbrace>
 3. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 4. \<And>s. (bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>y. \<lbrace>?B1 y\<rbrace> get_thread_state t \<lbrace>\<lambda>a b. (a = Running \<longrightarrow> bound_tcb_at ((=) None) t b) \<and> (a \<noteq> Running \<longrightarrow> bound_tcb_at ((=) None) t b)\<rbrace>
 2. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 3. \<And>s. (bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B1 ()\<rbrace> get_thread_state t \<lbrace>\<lambda>a. bound_tcb_at ((=) None) t\<rbrace>
 2. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>?B1\<rbrace>
 3. \<And>s. (bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cancel_ipc t \<lbrace>\<lambda>a. bound_tcb_at ((=) None) t\<rbrace>
 2. \<And>s. (bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (bound_tcb_at ((=) None) t and valid_mdb and valid_objs and tcb_at t) s \<Longrightarrow> (bound_tcb_at ((=) None) t and (valid_mdb and valid_objs and tcb_at t)) s proof (prove)
goal:
No subgoals!