theory Finalise_IF

lemma suspend_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and tcb_at thread
                                                 and K (is_subject aag thread))
                          (suspend thread)" unfolding suspend_def apply (wp reads_respects_f[OF set_thread_state_owned_reads_respects, where st=st and Q="\<top>"]
            reads_respects_f[OF tcb_sched_action_reads_respects, where st=st and Q=\<top>]
            reads_respects_f[OF get_thread_state_rev, where st=st and Q="\<top>"]
            reads_respects_f[OF update_restart_pc_reads_respects, where st=st and Q="\<top>"]
            gts_wp set_thread_state_pas_refined | simp)+ apply (wp cancel_ipc_reads_respects_f[where st=st] cancel_ipc_silc_inv)+ apply clarsimp apply (wp hoare_allI hoare_drop_imps) apply clarsimp apply (wp cancel_ipc_silc_inv)+ apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) (suspend thread) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) (do cancel_ipc thread;
state <- get_thread_state thread;
if state = Running then update_restart_pc thread else return ();
set_thread_state thread Inactive;
do_extended_op (tcb_sched_action tcb_sched_dequeue thread)
od) proof (prove)
goal (3 subgoals):
 1. reads_respects_f aag l ?P' (cancel_ipc thread)
 2. \<lbrace>?P''\<rbrace> cancel_ipc thread \<lbrace>\<lambda>rv s. (silc_inv aag st and K (aag_can_read aag thread) and (\<lambda>_. True)) s \<and> (\<forall>sta. st_tcb_at ((=) sta) thread s \<longrightarrow> ((sta = Running \<longrightarrow> (silc_inv aag st and (silc_inv aag (?s31 rv sta) and K (is_subject aag thread)) and (\<lambda>_. True)) s) \<and> (sta \<noteq> Running \<longrightarrow> True)) \<and> (sta = Running \<longrightarrow> silc_inv aag st s \<and> aag_can_read aag thread \<and> True \<and> silc_inv aag st s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> K (\<forall>r\<in>tcb_st_to_auth Inactive. (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag) s \<and> True) \<and> (sta \<noteq> Running \<longrightarrow> silc_inv aag st s \<and> aag_can_read aag thread \<and> True \<and> silc_inv aag st s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth Inactive. (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> True))\<rbrace>
 3. \<And>s. (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<Longrightarrow> ?P' s \<and> ?P'' s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'86\<rbrace> cancel_ipc thread \<lbrace>\<lambda>rv s. \<forall>sta. st_tcb_at ((=) sta) thread s \<longrightarrow> ((sta = Running \<longrightarrow> (silc_inv aag st and (silc_inv aag (?s31 rv sta) and K (is_subject aag thread)) and (\<lambda>_. True)) s) \<and> (sta \<noteq> Running \<longrightarrow> True)) \<and> (sta = Running \<longrightarrow> silc_inv aag st s \<and> aag_can_read aag thread \<and> True \<and> silc_inv aag st s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state)) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> K (\<forall>r\<in>tcb_st_to_auth Inactive. (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag) s \<and> True) \<and> (sta \<noteq> Running \<longrightarrow> silc_inv aag st s \<and> aag_can_read aag thread \<and> True \<and> silc_inv aag st s \<and> (pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and K (\<forall>r\<in>tcb_st_to_auth Inactive. (pasObjectAbs aag thread, snd r, pasObjectAbs aag (fst r)) \<in> pasPolicy aag)) s \<and> True)\<rbrace>
 2. \<And>s. (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<Longrightarrow> (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<and> (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag thread)) s \<and> K (aag_can_read aag thread) s \<and> True \<and> ?P'86 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'86\<rbrace> cancel_ipc thread \<lbrace>\<lambda>rv s. \<forall>sta. st_tcb_at ((=) sta) thread s \<longrightarrow> (sta = Running \<longrightarrow> silc_inv aag st s \<and> silc_inv aag (?s31 () Running) s \<and> is_subject aag thread) \<and> silc_inv aag st s \<and> aag_can_read aag thread \<and> silc_inv aag st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 2. \<And>s. (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<Longrightarrow> (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<and> (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag thread)) s \<and> K (aag_can_read aag thread) s \<and> True \<and> ?P'86 s proof (prove)
goal (3 subgoals):
 1. \<And>sta. \<lbrace>?P105\<rbrace> cancel_ipc thread \<lbrace>\<lambda>rv s. silc_inv aag st s \<and> silc_inv aag (?s31 () (ds_id Running)) s \<and> is_subject aag thread\<rbrace>
 2. \<And>sta. \<lbrace>?P'106\<rbrace> cancel_ipc thread \<lbrace>\<lambda>rv s. silc_inv aag st s \<and> aag_can_read aag thread \<and> silc_inv aag st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 3. \<And>s. (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<Longrightarrow> (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<and> (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag thread)) s \<and> K (aag_can_read aag thread) s \<and> True \<and> ?P105 s \<and> ?P'106 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P105\<rbrace> cancel_ipc thread \<lbrace>\<lambda>rv s. silc_inv aag st s \<and> silc_inv aag (?s31 () (ds_id Running)) s \<and> is_subject aag thread\<rbrace>
 2. \<And>sta. \<lbrace>?P'106\<rbrace> cancel_ipc thread \<lbrace>\<lambda>rv s. silc_inv aag st s \<and> aag_can_read aag thread \<and> silc_inv aag st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s\<rbrace>
 3. \<And>s. (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<Longrightarrow> (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<and> (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag thread)) s \<and> K (aag_can_read aag thread) s \<and> True \<and> ?P105 s \<and> ?P'106 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<Longrightarrow> (silc_inv aag st and pas_refined aag and invs and tcb_at thread and K (is_subject aag thread)) s \<and> (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag thread)) s \<and> K (aag_can_read aag thread) s \<and> True \<and> ((silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag thread)) s \<and> (silc_inv aag (?s31 () (ds_id Running)) and valid_mdb and pas_refined aag and K (is_subject aag thread)) s \<and> is_subject aag thread) \<and> (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag thread)) s \<and> aag_can_read aag thread \<and> (silc_inv aag st and valid_mdb and pas_refined aag and K (is_subject aag thread)) s \<and> (pas_refined aag and (pspace_aligned and valid_vspace_objs and valid_arch_state) and (invs and tcb_at thread and K (is_subject aag thread))) s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s proof (prove)
goal:
No subgoals!