theory Finalise_AI

lemma cancel_ipc_caps_of_state:
  "\<lbrace>\<lambda>s. (\<forall>p. cte_wp_at can_fast_finalise p s
           \<longrightarrow> P ((caps_of_state s) (p \<mapsto> cap.NullCap)))
           \<and> P (caps_of_state s)\<rbrace>
     cancel_ipc t
   \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" apply (simp add: cancel_ipc_def reply_cancel_ipc_def
             cong: Structures_A.thread_state.case_cong) apply (wpsimp wp: cap_delete_one_caps_of_state) apply (rule_tac Q="\<lambda>_ s. (\<forall>p. cte_wp_at can_fast_finalise p s
                                \<longrightarrow> P ((caps_of_state s) (p \<mapsto> cap.NullCap)))
                                \<and> P (caps_of_state s)"
                  in hoare_post_imp) apply (clarsimp simp: fun_upd_def[symmetric] split_paired_Ball) apply (simp add: cte_wp_at_caps_of_state) apply (wpsimp wp: hoare_vcg_all_lift hoare_convert_imp thread_set_caps_of_state_trivial
                 simp: ran_tcb_cap_cases)+ prefer 2 apply assumption apply (rule hoare_strengthen_post [OF gts_sp]) apply (clarsimp simp: fun_upd_def[symmetric] cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>p. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) \<and> P (caps_of_state s)\<rbrace> cancel_ipc t \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>a b. cte_wp_at can_fast_finalise (a, b) s \<longrightarrow> P ((caps_of_state s)((a, b) \<mapsto> NullCap))) \<and> P (caps_of_state s)\<rbrace> do state <- get_thread_state t;
case state of BlockedOnReceive x y \<Rightarrow> blocked_cancel_ipc (BlockedOnReceive x y) t | BlockedOnSend x y \<Rightarrow> blocked_cancel_ipc (BlockedOnSend x y) t | BlockedOnReply \<Rightarrow> do y <- thread_set (tcb_fault_update (\<lambda>_. None)) t;
cap <- get_cap (t, tcb_cnode_index 2);
descs <- gets (descendants_of (t, tcb_cnode_index 2) \<circ> cdt);
when (descs \<noteq> {}) (do y <- assert (\<exists>a b. descs = {(a, b)});
select descs >>= cap_delete_one
od)
od | BlockedOnNotification event \<Rightarrow> cancel_signal t event | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<lbrace>?R26 (ds_id BlockedOnReply)\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>y s. (descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> (\<forall>x\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). cte_wp_at can_fast_finalise x s \<longrightarrow> P ((caps_of_state s)(x \<mapsto> NullCap)))) \<and> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> P (caps_of_state s))\<rbrace>
 2. \<And>state x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>?R25 state x7\<rbrace> cancel_signal t x7 \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 3. \<And>state. idle state \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 4. \<lbrace>?Q11\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> P (caps_of_state s)) \<and> (inactive state \<longrightarrow> P (caps_of_state s)) \<and> (state = Restart \<longrightarrow> P (caps_of_state s)) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> P (caps_of_state s)) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> P (caps_of_state s)) \<and> (awaiting_reply state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (idle state \<longrightarrow> ?R23 state s)\<rbrace>
 5. \<And>s. (\<forall>a b. cte_wp_at can_fast_finalise (a, b) s \<longrightarrow> P ((caps_of_state s)((a, b) \<mapsto> NullCap))) \<and> P (caps_of_state s) \<Longrightarrow> ?Q11 s proof (prove)
goal (6 subgoals):
 1. \<And>rv s. (\<forall>p. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) \<and> P (caps_of_state s) \<Longrightarrow> (descendants_of (t, tcb_cnode_index 2) (cdt s) \<noteq> {} \<longrightarrow> (\<exists>a b. descendants_of (t, tcb_cnode_index 2) (cdt s) = {(a, b)}) \<longrightarrow> (\<forall>x\<in>descendants_of (t, tcb_cnode_index 2) (cdt s). cte_wp_at can_fast_finalise x s \<longrightarrow> P ((caps_of_state s)(x \<mapsto> NullCap)))) \<and> (descendants_of (t, tcb_cnode_index 2) (cdt s) = {} \<longrightarrow> P (caps_of_state s))
 2. \<lbrace>?R26 (ds_id BlockedOnReply)\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_ s. (\<forall>p. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) \<and> P (caps_of_state s)\<rbrace>
 3. \<And>state x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>?R25 state x7\<rbrace> cancel_signal t x7 \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 4. \<And>state. idle state \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 5. \<lbrace>?Q11\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> P (caps_of_state s)) \<and> (inactive state \<longrightarrow> P (caps_of_state s)) \<and> (state = Restart \<longrightarrow> P (caps_of_state s)) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> P (caps_of_state s)) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> P (caps_of_state s)) \<and> (awaiting_reply state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (idle state \<longrightarrow> ?R23 state s)\<rbrace>
 6. \<And>s. (\<forall>a b. cte_wp_at can_fast_finalise (a, b) s \<longrightarrow> P ((caps_of_state s)((a, b) \<mapsto> NullCap))) \<and> P (caps_of_state s) \<Longrightarrow> ?Q11 s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?R26 (ds_id BlockedOnReply)\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_ s. (\<forall>p. cte_wp_at can_fast_finalise p s \<longrightarrow> P ((caps_of_state s)(p \<mapsto> NullCap))) \<and> P (caps_of_state s)\<rbrace>
 2. \<And>state x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>?R25 state x7\<rbrace> cancel_signal t x7 \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 3. \<And>state. idle state \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 4. \<lbrace>?Q11\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> P (caps_of_state s)) \<and> (inactive state \<longrightarrow> P (caps_of_state s)) \<and> (state = Restart \<longrightarrow> P (caps_of_state s)) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> P (caps_of_state s)) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> P (caps_of_state s)) \<and> (awaiting_reply state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (idle state \<longrightarrow> ?R23 state s)\<rbrace>
 5. \<And>s. (\<forall>a b. cte_wp_at can_fast_finalise (a, b) s \<longrightarrow> P ((caps_of_state s)((a, b) \<mapsto> NullCap))) \<and> P (caps_of_state s) \<Longrightarrow> ?Q11 s proof (prove)
goal (5 subgoals):
 1. \<lbrace>?R26 (ds_id BlockedOnReply)\<rbrace> thread_set (tcb_fault_update (\<lambda>_. None)) t \<lbrace>\<lambda>_ s. (\<forall>a b. (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> can_fast_finalise cap) \<longrightarrow> P ((caps_of_state s)((a, b) \<mapsto> NullCap))) \<and> P (caps_of_state s)\<rbrace>
 2. \<And>state x7. state = BlockedOnNotification x7 \<Longrightarrow> \<lbrace>?R25 state x7\<rbrace> cancel_signal t x7 \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 3. \<And>state. idle state \<Longrightarrow> \<lbrace>?R23 state\<rbrace> return () \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>
 4. \<lbrace>?Q11\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> P (caps_of_state s)) \<and> (inactive state \<longrightarrow> P (caps_of_state s)) \<and> (state = Restart \<longrightarrow> P (caps_of_state s)) \<and> (\<forall>x xa. state = BlockedOnReceive x xa \<longrightarrow> P (caps_of_state s)) \<and> (\<forall>x xa. state = BlockedOnSend x xa \<longrightarrow> P (caps_of_state s)) \<and> (awaiting_reply state \<longrightarrow> ?R26 state s) \<and> (\<forall>x. state = BlockedOnNotification x \<longrightarrow> ?R25 state x s) \<and> (idle state \<longrightarrow> ?R23 state s)\<rbrace>
 5. \<And>s. (\<forall>a b. cte_wp_at can_fast_finalise (a, b) s \<longrightarrow> P ((caps_of_state s)((a, b) \<mapsto> NullCap))) \<and> P (caps_of_state s) \<Longrightarrow> ?Q11 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q11\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> P (caps_of_state s)) \<and> (inactive state \<longrightarrow> P (caps_of_state s)) \<and> (state = Restart \<longrightarrow> P (caps_of_state s)) \<and> ((\<exists>x xa. state = BlockedOnReceive x xa) \<longrightarrow> P (caps_of_state s)) \<and> ((\<exists>x xa. state = BlockedOnSend x xa) \<longrightarrow> P (caps_of_state s)) \<and> (awaiting_reply state \<longrightarrow> (\<forall>x xa. (\<exists>cap. caps_of_state s (x, xa) = Some cap \<and> can_fast_finalise cap) \<longrightarrow> P (\<lambda>a. if a = (x, xa) then Some NullCap else caps_of_state s a)) \<and> P (caps_of_state s)) \<and> ((\<exists>x. state = BlockedOnNotification x) \<longrightarrow> P (caps_of_state s)) \<and> (idle state \<longrightarrow> P (caps_of_state s))\<rbrace>
 2. \<And>s. (\<forall>a b. cte_wp_at can_fast_finalise (a, b) s \<longrightarrow> P ((caps_of_state s)((a, b) \<mapsto> NullCap))) \<and> P (caps_of_state s) \<Longrightarrow> ?Q11 s proof (prove)
goal (2 subgoals):
 1. \<And>s. (\<forall>a b. cte_wp_at can_fast_finalise (a, b) s \<longrightarrow> P ((caps_of_state s)((a, b) \<mapsto> NullCap))) \<and> P (caps_of_state s) \<Longrightarrow> ?Q11 s
 2. \<lbrace>?Q11\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> P (caps_of_state s)) \<and> (inactive state \<longrightarrow> P (caps_of_state s)) \<and> (state = Restart \<longrightarrow> P (caps_of_state s)) \<and> ((\<exists>x xa. state = BlockedOnReceive x xa) \<longrightarrow> P (caps_of_state s)) \<and> ((\<exists>x xa. state = BlockedOnSend x xa) \<longrightarrow> P (caps_of_state s)) \<and> (awaiting_reply state \<longrightarrow> (\<forall>x xa. (\<exists>cap. caps_of_state s (x, xa) = Some cap \<and> can_fast_finalise cap) \<longrightarrow> P (\<lambda>a. if a = (x, xa) then Some NullCap else caps_of_state s a)) \<and> P (caps_of_state s)) \<and> ((\<exists>x. state = BlockedOnNotification x) \<longrightarrow> P (caps_of_state s)) \<and> (idle state \<longrightarrow> P (caps_of_state s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>a b. cte_wp_at can_fast_finalise (a, b) s \<longrightarrow> P ((caps_of_state s)((a, b) \<mapsto> NullCap))) \<and> P (caps_of_state s)\<rbrace> get_thread_state t \<lbrace>\<lambda>state s. (state = Running \<longrightarrow> P (caps_of_state s)) \<and> (inactive state \<longrightarrow> P (caps_of_state s)) \<and> (state = Restart \<longrightarrow> P (caps_of_state s)) \<and> ((\<exists>x xa. state = BlockedOnReceive x xa) \<longrightarrow> P (caps_of_state s)) \<and> ((\<exists>x xa. state = BlockedOnSend x xa) \<longrightarrow> P (caps_of_state s)) \<and> (awaiting_reply state \<longrightarrow> (\<forall>x xa. (\<exists>cap. caps_of_state s (x, xa) = Some cap \<and> can_fast_finalise cap) \<longrightarrow> P (\<lambda>a. if a = (x, xa) then Some NullCap else caps_of_state s a)) \<and> P (caps_of_state s)) \<and> ((\<exists>x. state = BlockedOnNotification x) \<longrightarrow> P (caps_of_state s)) \<and> (idle state \<longrightarrow> P (caps_of_state s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (st_tcb_at ((=) rv) t and (\<lambda>s. (\<forall>a b. cte_wp_at can_fast_finalise (a, b) s \<longrightarrow> P ((caps_of_state s)((a, b) \<mapsto> NullCap))) \<and> P (caps_of_state s))) s \<Longrightarrow> (rv = Running \<longrightarrow> P (caps_of_state s)) \<and> (inactive rv \<longrightarrow> P (caps_of_state s)) \<and> (rv = Restart \<longrightarrow> P (caps_of_state s)) \<and> ((\<exists>x xa. rv = BlockedOnReceive x xa) \<longrightarrow> P (caps_of_state s)) \<and> ((\<exists>x xa. rv = BlockedOnSend x xa) \<longrightarrow> P (caps_of_state s)) \<and> (awaiting_reply rv \<longrightarrow> (\<forall>x xa. (\<exists>cap. caps_of_state s (x, xa) = Some cap \<and> can_fast_finalise cap) \<longrightarrow> P (\<lambda>a. if a = (x, xa) then Some NullCap else caps_of_state s a)) \<and> P (caps_of_state s)) \<and> ((\<exists>x. rv = BlockedOnNotification x) \<longrightarrow> P (caps_of_state s)) \<and> (idle rv \<longrightarrow> P (caps_of_state s)) proof (prove)
goal:
No subgoals!