theory ArchDetSchedAux_AI

lemma perform_asid_control_invocation_valid_sched:
  "\<lbrace>ct_active and invs and valid_aci aci and valid_sched and valid_idle\<rbrace>
     perform_asid_control_invocation aci
   \<lbrace>\<lambda>_. valid_sched\<rbrace>" apply (rule hoare_pre) apply (rule_tac I="invs and ct_active and valid_aci aci" in valid_sched_tcb_state_preservation) apply (wp perform_asid_control_invocation_st_tcb_at) apply simp apply (wp perform_asid_control_etcb_at)+ apply (rule hoare_strengthen_post, rule aci_invs) apply (simp add: invs_def valid_state_def) apply (rule hoare_lift_Pf[where f="\<lambda>s. scheduler_action s"]) apply (rule hoare_lift_Pf[where f="\<lambda>s. cur_domain s"]) apply (rule hoare_lift_Pf[where f="\<lambda>s. idle_thread s"]) apply wp+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active and invs and valid_aci aci and valid_sched and valid_idle\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_sched\<rbrace>
 2. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>P t. \<lbrace>invs and ct_active and valid_aci aci and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. st_tcb_at P t\<rbrace>
 2. \<And>P t. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 5. \<lbrace>valid_etcbs\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_etcbs\<rbrace>
 6. \<lbrace>valid_blocked\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_blocked\<rbrace>
 7. \<lbrace>invs and ct_active and valid_aci aci\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_idle\<rbrace>
 8. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 9. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> (invs and ct_active and valid_aci aci and ct_active and valid_sched and valid_idle) s proof (prove)
goal (9 subgoals):
 1. \<And>P t s. (invs and ct_active and valid_aci aci and ct_active and st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t) s \<Longrightarrow> (st_tcb_at (P and Not \<circ> inactive and Not \<circ> idle) t and ct_active and invs and valid_aci aci) s
 2. \<And>P t. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 4. \<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 5. \<lbrace>valid_etcbs\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_etcbs\<rbrace>
 6. \<lbrace>valid_blocked\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_blocked\<rbrace>
 7. \<lbrace>invs and ct_active and valid_aci aci\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_idle\<rbrace>
 8. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 9. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> (invs and ct_active and valid_aci aci and ct_active and valid_sched and valid_idle) s proof (prove)
goal (8 subgoals):
 1. \<And>P t. \<lbrace>etcb_at P t and valid_etcbs\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. st_tcb_at (Not \<circ> inactive) t s \<longrightarrow> etcb_at P t s\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>
 4. \<lbrace>valid_etcbs\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_etcbs\<rbrace>
 5. \<lbrace>valid_blocked\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_blocked\<rbrace>
 6. \<lbrace>invs and ct_active and valid_aci aci\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_idle\<rbrace>
 7. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 8. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> (invs and ct_active and valid_aci aci and ct_active and valid_sched and valid_idle) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>invs and ct_active and valid_aci aci\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_. valid_idle\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 3. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> (invs and ct_active and valid_aci aci and ct_active and valid_sched and valid_idle) s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. invs s \<Longrightarrow> valid_idle s
 2. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 3. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> (invs and ct_active and valid_aci aci and ct_active and valid_sched and valid_idle) s proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>r s. P (scheduler_action s) (ready_queues s) (cur_domain s)\<rbrace>
 2. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> (invs and ct_active and valid_aci aci and ct_active and valid_sched and valid_idle) s proof (prove)
goal (3 subgoals):
 1. \<And>P x. \<lbrace>\<lambda>s. P x (ready_queues s) (cur_domain s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_ a. P x (ready_queues a) (cur_domain a)\<rbrace>
 2. \<And>P Pa. \<lbrace>\<lambda>s. Pa (scheduler_action s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_ s. Pa (scheduler_action s)\<rbrace>
 3. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> (invs and ct_active and valid_aci aci and ct_active and valid_sched and valid_idle) s proof (prove)
goal (4 subgoals):
 1. \<And>P x xa. \<lbrace>\<lambda>s. P x (ready_queues s) xa\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_ a. P x (ready_queues a) xa\<rbrace>
 2. \<And>P x Pa. \<lbrace>\<lambda>s. Pa (cur_domain s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_ s. Pa (cur_domain s)\<rbrace>
 3. \<And>P Pa. \<lbrace>\<lambda>s. Pa (scheduler_action s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_ s. Pa (scheduler_action s)\<rbrace>
 4. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> (invs and ct_active and valid_aci aci and ct_active and valid_sched and valid_idle) s proof (prove)
goal (5 subgoals):
 1. \<And>P x xa xb. \<lbrace>\<lambda>s. P x (ready_queues s) xa\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_ a. P x (ready_queues a) xa\<rbrace>
 2. \<And>P x xa Pa. \<lbrace>\<lambda>s. Pa (idle_thread s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_ s. Pa (idle_thread s)\<rbrace>
 3. \<And>P x Pa. \<lbrace>\<lambda>s. Pa (cur_domain s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_ s. Pa (cur_domain s)\<rbrace>
 4. \<And>P Pa. \<lbrace>\<lambda>s. Pa (scheduler_action s)\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>_ s. Pa (scheduler_action s)\<rbrace>
 5. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> (invs and ct_active and valid_aci aci and ct_active and valid_sched and valid_idle) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (ct_active and invs and valid_aci aci and valid_sched and valid_idle) s \<Longrightarrow> (invs and ct_active and valid_aci aci and ct_active and valid_sched and valid_idle) s proof (prove)
goal:
No subgoals!