theory Syscall_AI

lemma do_reply_transfer_nonz_cap:
  "\<lbrace>\<lambda>s :: 'state_ext state. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s
            \<and> tcb_at receiver s\<rbrace>
     do_reply_transfer sender receiver slot grant
   \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>" apply (simp add: do_reply_transfer_def) apply (rule hoare_seq_ext [OF _ gts_sp]) apply (rule hoare_pre) apply (wp cap_delete_one_cte_wp_at_preserved hoare_vcg_ex_lift | simp split del: if_split
          | wpc | strengthen ex_nonz_cap_to_tcb_strg)+ apply (clarsimp simp add: tcb_cap_cases_def is_cap_simps can_fast_finalise_def) apply (strengthen ex_tcb_cap_to_tcb_at_strg) apply (wp drop_when_dxo_wp hoare_vcg_ex_lift
             thread_set_no_change_tcb_state thread_set_cte_wp_at_trivial
             ex_nonz_cap_to_pres [OF thread_set_cte_wp_at_trivial]
             | simp add: tcb_cap_cases_def)+ apply (wp hoare_vcg_ex_lift cap_delete_one_cte_wp_at_preserved
            | strengthen ex_nonz_cap_to_tcb_strg)+ apply (clarsimp simp add: tcb_cap_cases_def is_cap_simps can_fast_finalise_def) apply (strengthen ex_tcb_cap_to_tcb_at_strg) apply (wp hoare_drop_imp hoare_allI)+ apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s\<rbrace> do_reply_transfer sender receiver slot grant \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s\<rbrace> do state <- get_thread_state receiver;
y <- assert (awaiting_reply state);
thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od)
od \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at ((=) state) receiver and (\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s)\<rbrace> do y <- assert (awaiting_reply state);
thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od)
od \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>state. \<lbrace>?Q8 state\<rbrace> do y <- assert (awaiting_reply state);
thread_get tcb_fault receiver >>= case_option (do y <- do_ipc_transfer sender None 0 grant receiver;
y <- cap_delete_one slot;
y <- set_thread_state receiver Running;
do_extended_op (possible_switch_to receiver)
od) (\<lambda>f. do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply f receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od)
od \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>
 2. \<And>state s. (st_tcb_at ((=) state) receiver and (\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s)) s \<Longrightarrow> ?Q8 state s proof (prove)
goal (6 subgoals):
 1. \<And>cap. is_thread_cap cap \<and> p \<in> zobj_refs cap \<Longrightarrow> \<not> can_fast_finalise cap
 2. \<And>state x. x = None \<Longrightarrow> \<lbrace>?R24 state () x\<rbrace> do_ipc_transfer sender None 0 grant receiver \<lbrace>\<lambda>a b. \<exists>x. cte_wp_at (\<lambda>a. is_thread_cap a \<and> p \<in> zobj_refs a) x b\<rbrace>
 3. \<And>state x x2. x = Some x2 \<Longrightarrow> \<lbrace>\<lambda>a. ?R23 state () x a x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>
 4. \<And>state y. \<lbrace>?B12 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R24 state y a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R23 state y a b x)\<rbrace>
 5. \<And>state. \<lbrace>?Q8 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B12 state\<rbrace>
 6. \<And>state s. (st_tcb_at ((=) state) receiver and (\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s)) s \<Longrightarrow> ?Q8 state s proof (prove)
goal (5 subgoals):
 1. \<And>state x. x = None \<Longrightarrow> \<lbrace>?R24 state () x\<rbrace> do_ipc_transfer sender None 0 grant receiver \<lbrace>\<lambda>a b. \<exists>x. cte_wp_at (\<lambda>a. is_thread_cap a \<and> p \<in> zobj_refs a) x b\<rbrace>
 2. \<And>state x x2. x = Some x2 \<Longrightarrow> \<lbrace>\<lambda>a. ?R23 state () x a x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>
 3. \<And>state y. \<lbrace>?B12 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R24 state y a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R23 state y a b x)\<rbrace>
 4. \<And>state. \<lbrace>?Q8 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B12 state\<rbrace>
 5. \<And>state s. (st_tcb_at ((=) state) receiver and (\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s)) s \<Longrightarrow> ?Q8 state s proof (prove)
goal (5 subgoals):
 1. \<And>state x. x = None \<Longrightarrow> \<lbrace>?R24 state () x\<rbrace> do_ipc_transfer sender None 0 grant receiver \<lbrace>\<lambda>r s. ex_nonz_cap_to p s \<and> tcb_at p s \<and> valid_objs s\<rbrace>
 2. \<And>state x x2. x = Some x2 \<Longrightarrow> \<lbrace>\<lambda>a. ?R23 state () x a x2\<rbrace> do y <- cap_delete_one slot;
mi <- get_message_info sender;
buf <- lookup_ipc_buffer False sender;
mrs <- get_mrs sender buf mi;
restart <- handle_fault_reply x2 receiver (mi_label mi) mrs;
y <- thread_set (tcb_fault_update (\<lambda>_. None)) receiver;
y <- set_thread_state receiver (if restart then Restart else Inactive);
when restart (do_extended_op (possible_switch_to receiver))
od \<lbrace>\<lambda>rv. ex_nonz_cap_to p\<rbrace>
 3. \<And>state y. \<lbrace>?B12 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ?R24 state y a b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R23 state y a b x)\<rbrace>
 4. \<And>state. \<lbrace>?Q8 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B12 state\<rbrace>
 5. \<And>state s. (st_tcb_at ((=) state) receiver and (\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s)) s \<Longrightarrow> ?Q8 state s proof (prove)
goal (4 subgoals):
 1. \<And>state x x2. x = Some x2 \<Longrightarrow> \<lbrace>?R70 state () (Some x2) x2\<rbrace> cap_delete_one slot \<lbrace>\<lambda>xa. ex_nonz_cap_to p\<rbrace>
 2. \<And>state y. \<lbrace>?B12 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ex_nonz_cap_to p b \<and> tcb_at p b \<and> (valid_objs and valid_mdb) b) \<and> (\<forall>x. a = Some x \<longrightarrow> ?R70 state y a x b)\<rbrace>
 3. \<And>state. \<lbrace>?Q8 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B12 state\<rbrace>
 4. \<And>state s. (st_tcb_at ((=) state) receiver and (\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s)) s \<Longrightarrow> ?Q8 state s proof (prove)
goal (4 subgoals):
 1. \<And>state x x2 cref cap. \<lbrakk>x = Some x2; is_thread_cap cap \<and> p \<in> zobj_refs cap\<rbrakk> \<Longrightarrow> \<not> can_fast_finalise cap
 2. \<And>state y. \<lbrace>?B12 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ex_nonz_cap_to p b \<and> tcb_at p b \<and> (valid_objs and valid_mdb) b) \<and> (\<forall>x. a = Some x \<longrightarrow> (\<exists>x. cte_wp_at (\<lambda>a. is_thread_cap a \<and> p \<in> zobj_refs a) x b))\<rbrace>
 3. \<And>state. \<lbrace>?Q8 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B12 state\<rbrace>
 4. \<And>state s. (st_tcb_at ((=) state) receiver and (\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s)) s \<Longrightarrow> ?Q8 state s proof (prove)
goal (3 subgoals):
 1. \<And>state y. \<lbrace>?B12 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>a b. (a = None \<longrightarrow> ex_nonz_cap_to p b \<and> tcb_at p b \<and> (valid_objs and valid_mdb) b) \<and> (\<forall>x. a = Some x \<longrightarrow> (\<exists>x. cte_wp_at (\<lambda>a. is_thread_cap a \<and> p \<in> zobj_refs a) x b))\<rbrace>
 2. \<And>state. \<lbrace>?Q8 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B12 state\<rbrace>
 3. \<And>state s. (st_tcb_at ((=) state) receiver and (\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s)) s \<Longrightarrow> ?Q8 state s proof (prove)
goal (3 subgoals):
 1. \<And>state y. \<lbrace>?B12 state y\<rbrace> thread_get tcb_fault receiver \<lbrace>\<lambda>r s. (r = None \<longrightarrow> ex_nonz_cap_to p s \<and> tcb_at p s \<and> (valid_objs and valid_mdb) s) \<and> (\<forall>x. r = Some x \<longrightarrow> ex_nonz_cap_to p s \<and> tcb_at p s \<and> valid_objs s)\<rbrace>
 2. \<And>state. \<lbrace>?Q8 state\<rbrace> assert (awaiting_reply state) \<lbrace>?B12 state\<rbrace>
 3. \<And>state s. (st_tcb_at ((=) state) receiver and (\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s)) s \<Longrightarrow> ?Q8 state s proof (prove)
goal (1 subgoal):
 1. \<And>state s. (st_tcb_at ((=) state) receiver and (\<lambda>s. ex_nonz_cap_to p s \<and> valid_objs s \<and> tcb_at p s \<and> valid_mdb s \<and> tcb_at receiver s)) s \<Longrightarrow> awaiting_reply state \<longrightarrow> (ex_nonz_cap_to p s \<and> tcb_at p s \<and> (valid_objs and valid_mdb) s) \<and> ex_nonz_cap_to p s \<and> tcb_at p s \<and> valid_objs s proof (prove)
goal:
No subgoals!