theory Syscall_AC

lemma set_thread_state_authorised[wp]:
  "\<lbrace>authorised_invocation aag i and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace>
   set_thread_state thread Restart
   \<lbrace>\<lambda>_. authorised_invocation aag i\<rbrace>" apply (cases i; simp add: authorised_invocation_def) apply (wpsimp wp: sts_valid_untyped_inv ct_in_state_set
                            hoare_vcg_ex_lift sts_obj_at_impossible)+ apply (rename_tac cnode_invocation) apply (case_tac cnode_invocation;
            simp add: cnode_inv_auth_derivations_def authorised_cnode_inv_def)[1] apply (wp set_thread_state_cte_wp_at | simp)+ apply (rename_tac arch_invocation) apply (wpsimp wp: sts_valid_arch_inv ct_in_state_set) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>authorised_invocation aag i and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_. authorised_invocation aag i\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>x1. i = InvokeUntyped x1 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_untyped_inv x1 s \<and> authorised_untyped_inv aag x1 \<and> ct_active s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. valid_untyped_inv x1 s \<and> authorised_untyped_inv aag x1 \<and> ct_active s\<rbrace>
 2. \<And>x21 x22 x23 x24. i = InvokeEndpoint x21 x22 x23 x24 \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ep. ko_at (Endpoint ep) x21 s \<and> (x23 \<longrightarrow> (\<forall>r\<in>ep_q_refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)) \<and> (pasSubject aag, Grant, pasObjectAbs aag x21) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x21) \<in> pasPolicy aag) \<and> (x24 \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag x21) \<in> pasPolicy aag) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x21) \<in> pasPolicy aag) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. \<exists>ep. ko_at (Endpoint ep) x21 s \<and> (x23 \<longrightarrow> (\<forall>r\<in>ep_q_refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)) \<and> (pasSubject aag, Grant, pasObjectAbs aag x21) \<in> pasPolicy aag \<and> (pasSubject aag, Call, pasObjectAbs aag x21) \<in> pasPolicy aag) \<and> (x24 \<longrightarrow> (pasSubject aag, Call, pasObjectAbs aag x21) \<in> pasPolicy aag) \<and> (pasSubject aag, SyncSend, pasObjectAbs aag x21) \<in> pasPolicy aag\<rbrace>
 3. \<And>x31 x32. i = InvokeNotification x31 x32 \<Longrightarrow> \<lbrace>(\<lambda>s. (pasSubject aag, Notify, pasObjectAbs aag x31) \<in> pasPolicy aag) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. (pasSubject aag, Notify, pasObjectAbs aag x31) \<in> pasPolicy aag\<rbrace>
 4. \<And>x41 x42 x43. i = InvokeReply x41 x42 x43 \<Longrightarrow> \<lbrace>(\<lambda>s. (x43 \<longrightarrow> is_subject aag x41) \<and> is_subject aag (fst x42) \<and> (pasSubject aag, Reply, pasObjectAbs aag x41) \<in> pasPolicy aag) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. (x43 \<longrightarrow> is_subject aag x41) \<and> is_subject aag (fst x42) \<and> (pasSubject aag, Reply, pasObjectAbs aag x41) \<in> pasPolicy aag\<rbrace>
 5. \<And>x5. i = InvokeTCB x5 \<Longrightarrow> \<lbrace>(\<lambda>s. tcb_inv_wf x5 s \<and> authorised_tcb_inv aag x5) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. tcb_inv_wf x5 s \<and> authorised_tcb_inv aag x5\<rbrace>
 6. \<And>x7. i = InvokeCNode x7 \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_cnode_inv aag x7 s \<and> is_subject aag (cur_thread s) \<and> cnode_inv_auth_derivations x7 s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_cnode_inv aag x7 s \<and> is_subject aag (cur_thread s) \<and> cnode_inv_auth_derivations x7 s\<rbrace>
 7. \<And>x8. i = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_irq_ctl_inv aag x8) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_irq_ctl_inv aag x8\<rbrace>
 8. \<And>x9. i = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_irq_hdl_inv aag x9) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_irq_hdl_inv aag x9\<rbrace>
 9. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_arch_inv x10 s \<and> authorised_arch_inv aag x10 s \<and> ct_active s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. valid_arch_inv x10 s \<and> authorised_arch_inv aag x10 s \<and> ct_active s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x7. i = InvokeCNode x7 \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_cnode_inv aag x7 s \<and> is_subject aag (cur_thread s) \<and> cnode_inv_auth_derivations x7 s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_cnode_inv aag x7 s \<and> is_subject aag (cur_thread s) \<and> cnode_inv_auth_derivations x7 s\<rbrace>
 2. \<And>x8. i = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_irq_ctl_inv aag x8) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_irq_ctl_inv aag x8\<rbrace>
 3. \<And>x9. i = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_irq_hdl_inv aag x9) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_irq_hdl_inv aag x9\<rbrace>
 4. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_arch_inv x10 s \<and> authorised_arch_inv aag x10 s \<and> ct_active s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. valid_arch_inv x10 s \<and> authorised_arch_inv aag x10 s \<and> ct_active s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>cnode_invocation. i = InvokeCNode cnode_invocation \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_cnode_inv aag cnode_invocation s \<and> is_subject aag (cur_thread s) \<and> cnode_inv_auth_derivations cnode_invocation s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_cnode_inv aag cnode_invocation s \<and> is_subject aag (cur_thread s) \<and> cnode_inv_auth_derivations cnode_invocation s\<rbrace>
 2. \<And>x8. i = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_irq_ctl_inv aag x8) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_irq_ctl_inv aag x8\<rbrace>
 3. \<And>x9. i = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_irq_hdl_inv aag x9) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_irq_hdl_inv aag x9\<rbrace>
 4. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_arch_inv x10 s \<and> authorised_arch_inv aag x10 s \<and> ct_active s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. valid_arch_inv x10 s \<and> authorised_arch_inv aag x10 s \<and> ct_active s\<rbrace> proof (prove)
goal (10 subgoals):
 1. \<And>cnode_invocation x11 x12 x13. \<lbrakk>i = InvokeCNode (InsertCall x11 x12 x13); cnode_invocation = InsertCall x11 x12 x13\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. is_subject aag (fst x12) \<and> is_subject aag (fst x13) \<and> is_subject aag (cur_thread s) \<and> cte_wp_at (auth_derived x11) x12 s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. is_subject aag (fst x12) \<and> is_subject aag (fst x13) \<and> is_subject aag (cur_thread s) \<and> cte_wp_at (auth_derived x11) x12 s\<rbrace>
 2. \<And>cnode_invocation x21 x22 x23. \<lbrakk>i = InvokeCNode (MoveCall x21 x22 x23); cnode_invocation = MoveCall x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. is_subject aag (fst x22) \<and> is_subject aag (fst x23) \<and> is_subject aag (cur_thread s) \<and> cte_wp_at (auth_derived x21) x22 s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. is_subject aag (fst x22) \<and> is_subject aag (fst x23) \<and> is_subject aag (cur_thread s) \<and> cte_wp_at (auth_derived x21) x22 s\<rbrace>
 3. \<And>cnode_invocation x3. \<lbrakk>i = InvokeCNode (RevokeCall x3); cnode_invocation = RevokeCall x3\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. is_subject aag (fst x3) \<and> is_subject aag (cur_thread s)) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. is_subject aag (fst x3) \<and> is_subject aag (cur_thread s)\<rbrace>
 4. \<And>cnode_invocation x4. \<lbrakk>i = InvokeCNode (DeleteCall x4); cnode_invocation = DeleteCall x4\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. is_subject aag (fst x4) \<and> is_subject aag (cur_thread s)) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. is_subject aag (fst x4) \<and> is_subject aag (cur_thread s)\<rbrace>
 5. \<And>cnode_invocation x51 x52 x53 x54 x55. \<lbrakk>i = InvokeCNode (RotateCall x51 x52 x53 x54 x55); cnode_invocation = RotateCall x51 x52 x53 x54 x55\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. is_subject aag (fst x53) \<and> is_subject aag (fst x54) \<and> is_subject aag (fst x55) \<and> is_subject aag (cur_thread s) \<and> cte_wp_at (auth_derived x51) x53 s \<and> cte_wp_at (auth_derived x52) x54 s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. is_subject aag (fst x53) \<and> is_subject aag (fst x54) \<and> is_subject aag (fst x55) \<and> is_subject aag (cur_thread s) \<and> cte_wp_at (auth_derived x51) x53 s \<and> cte_wp_at (auth_derived x52) x54 s\<rbrace>
 6. \<And>cnode_invocation x6. \<lbrakk>i = InvokeCNode (SaveCall x6); cnode_invocation = SaveCall x6\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. is_subject aag (fst x6) \<and> is_subject aag (cur_thread s)) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. is_subject aag (fst x6) \<and> is_subject aag (cur_thread s)\<rbrace>
 7. \<And>cnode_invocation x7. \<lbrakk>i = InvokeCNode (CancelBadgedSendsCall x7); cnode_invocation = CancelBadgedSendsCall x7\<rbrakk> \<Longrightarrow> \<lbrace>(\<lambda>s. pas_cap_cur_auth aag x7 \<and> is_subject aag (cur_thread s)) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. pas_cap_cur_auth aag x7 \<and> is_subject aag (cur_thread s)\<rbrace>
 8. \<And>x8. i = InvokeIRQControl x8 \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_irq_ctl_inv aag x8) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_irq_ctl_inv aag x8\<rbrace>
 9. \<And>x9. i = InvokeIRQHandler x9 \<Longrightarrow> \<lbrace>(\<lambda>s. authorised_irq_hdl_inv aag x9) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. authorised_irq_hdl_inv aag x9\<rbrace>
 10. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_arch_inv x10 s \<and> authorised_arch_inv aag x10 s \<and> ct_active s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. valid_arch_inv x10 s \<and> authorised_arch_inv aag x10 s \<and> ct_active s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x10. i = InvokeArchObject x10 \<Longrightarrow> \<lbrace>(\<lambda>s. valid_arch_inv x10 s \<and> authorised_arch_inv aag x10 s \<and> ct_active s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. valid_arch_inv x10 s \<and> authorised_arch_inv aag x10 s \<and> ct_active s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>arch_invocation. i = InvokeArchObject arch_invocation \<Longrightarrow> \<lbrace>(\<lambda>s. valid_arch_inv arch_invocation s \<and> authorised_arch_inv aag arch_invocation s \<and> ct_active s) and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> set_thread_state thread Restart \<lbrace>\<lambda>_ s. valid_arch_inv arch_invocation s \<and> authorised_arch_inv aag arch_invocation s \<and> ct_active s\<rbrace> proof (prove)
goal:
No subgoals!