theory Syscall_IF

lemma handle_invocation_globals_equiv:
  "\<lbrace>invs and ct_active and globals_equiv st\<rbrace>
   handle_invocation calling blocking
   \<lbrace>\<lambda>_. globals_equiv (st :: det_state)\<rbrace>" apply (simp add: handle_invocation_def ts_Restart_case_helper
                   liftE_liftM_liftME liftME_def bindE_assoc) apply (wp syscall_valid handle_fault_globals_equiv reply_from_kernel_globals_equiv
            set_thread_state_globals_equiv hoare_vcg_all_lift
         | simp split del: if_split
         | wp (once) hoare_drop_imps)+ apply (rule_tac Q="\<lambda>r. invs and globals_equiv st and (\<lambda>s. thread \<noteq> idle_thread s)"
                     and E="\<lambda>_. globals_equiv st" in hoare_post_impErr) apply (wp pinv_invs perform_invocation_globals_equiv
                     requiv_get_tcb_eq' set_thread_state_globals_equiv
                     sts_authorised_for_globals_inv
                     decode_invocation_authorised_globals_inv
                  | simp add: crunch_simps invs_imps)+ apply (auto intro: st_tcb_ex_cap simp: ct_active_not_idle ct_in_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active and globals_equiv st\<rbrace> handle_invocation calling blocking \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and ct_active and globals_equiv st\<rbrace> doE thread <- liftE (gets cur_thread);
info <- liftE (get_message_info thread);
x <- liftE (as_user thread (getRegister cap_register));
syscall (doE (cap, slot) <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE) (\<lambda>fault. when blocking (handle_fault thread fault)) (\<lambda>(slot, cap, extracaps, buffer). doE args <- liftE (get_mrs thread buffer info);
decode_invocation (mi_label info) args (to_bl x) slot cap extracaps
odE) (\<lambda>err. when calling (reply_from_kernel thread (msg_from_syscall_error err))) (\<lambda>oper. doE y <- liftE (set_thread_state thread Restart);
reply <- perform_invocation blocking calling oper;
liftE (do state <- get_thread_state thread;
if state = Restart then do when calling $ reply_from_kernel thread (0, reply);
set_thread_state thread Running
od else return ()
od)
odE)
odE \<lbrace>\<lambda>_. globals_equiv st\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>thread info x rv. \<lbrace>?B10 thread info x rv ()\<rbrace> perform_invocation blocking calling rv \<lbrace>\<lambda>a b. (if calling then \<lambda>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s)) s \<and> valid_arch_state s else (\<lambda>s. globals_equiv st s \<and> valid_arch_state s)) b \<and> globals_equiv st b\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>thread info x rv. \<lbrace>?P_no_err5 thread info x rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B10 thread info x rv\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 3. \<And>thread info x rv. \<lbrace>?P_no_flt5 thread info x rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- liftE (get_mrs thread buffer info);
decode_invocation (mi_label info) args (to_bl x) slot cap extracaps
odE \<lbrace>?P_no_err5 thread info x\<rbrace>, \<lbrace>\<lambda>err. if calling then globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s) else globals_equiv st\<rbrace>
 4. \<And>thread info x. \<lbrace>?B4 thread info x\<rbrace> doE (cap, slot) <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt5 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault ft) else globals_equiv st\<rbrace>
 5. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 6. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 7. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 8. \<And>s. (invs and ct_active and globals_equiv st) s \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>thread info x rv. \<lbrace>?B10 thread info x rv ()\<rbrace> perform_invocation blocking calling rv \<lbrace>\<lambda>r. invs and globals_equiv st and (\<lambda>s. thread \<noteq> idle_thread s)\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>thread info x rv rva s. (invs and globals_equiv st and (\<lambda>s. thread \<noteq> idle_thread s)) s \<Longrightarrow> (if calling then \<lambda>s. (globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s)) s \<and> valid_arch_state s else (\<lambda>s. globals_equiv st s \<and> valid_arch_state s)) s \<and> globals_equiv st s
 3. \<And>thread info x rv e s. globals_equiv st s \<Longrightarrow> globals_equiv st s
 4. \<And>thread info x rv. \<lbrace>?P_no_err5 thread info x rv\<rbrace> liftE (set_thread_state thread Restart) \<lbrace>?B10 thread info x rv\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 5. \<And>thread info x rv. \<lbrace>?P_no_flt5 thread info x rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- liftE (get_mrs thread buffer info);
decode_invocation (mi_label info) args (to_bl x) slot cap extracaps
odE \<lbrace>?P_no_err5 thread info x\<rbrace>, \<lbrace>\<lambda>err. if calling then globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and (\<lambda>s. thread \<noteq> idle_thread s) else globals_equiv st\<rbrace>
 6. \<And>thread info x. \<lbrace>?B4 thread info x\<rbrace> doE (cap, slot) <- cap_fault_on_failure x False (lookup_cap_and_slot thread (to_bl x));
buffer <- liftE (lookup_ipc_buffer False thread);
extracaps <- lookup_extra_caps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt5 thread info x\<rbrace>, \<lbrace>\<lambda>ft. if blocking then globals_equiv st and valid_objs and valid_arch_state and valid_global_refs and pspace_distinct and pspace_aligned and valid_global_objs and valid_idle and (\<lambda>s. sym_refs (state_refs_of s)) and K (valid_fault ft) else globals_equiv st\<rbrace>
 7. \<And>thread info. \<lbrace>?B3 thread info\<rbrace> liftE (as_user thread (getRegister cap_register)) \<lbrace>?B4 thread info\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 8. \<And>thread. \<lbrace>?B2 thread\<rbrace> liftE (get_message_info thread) \<lbrace>?B3 thread\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 9. \<lbrace>?Q\<rbrace> liftE (gets cur_thread) \<lbrace>?B2\<rbrace>, \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 10. \<And>s. (invs and ct_active and globals_equiv st) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> ct_active s \<and> globals_equiv st s \<Longrightarrow> (blocking \<longrightarrow> valid_idle s) \<and> (calling \<longrightarrow> cur_thread s \<noteq> idle_thread s) \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> st_tcb_at active (cur_thread s) s \<and> ex_nonz_cap_to (cur_thread s) s \<and> cur_thread s \<noteq> idle_thread s proof (prove)
goal:
No subgoals!