theory Syscall_IF

lemma invoke_cnode_reads_respects_f:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_f aag l
           (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs
                            and simple_sched_action and valid_cnode_inv ci
                            and (\<lambda>s. is_subject aag (cur_thread s))
                            and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci)
           (invoke_cnode ci)" unfolding invoke_cnode_def apply (rule equiv_valid_guard_imp) apply (wpc | wp reads_respects_f[OF cap_insert_reads_respects] cap_insert_silc_inv
                  reads_respects_f[OF cap_move_reads_respects] cap_move_silc_inv get_cap_auth_wp
                  cap_revoke_reads_respects_f cap_delete_reads_respects_f cap_swap_silc_inv
                  reads_respects_f[OF cap_swap_reads_respects] cap_move_cte_wp_at_other
                  reads_respects_f[OF get_cap_rev]  cancel_badged_sends_reads_respects_f
             | simp add: when_def split del: if_split
             | elim conjE, assumption)+ apply (clarsimp simp: cnode_inv_auth_derivations_def authorised_cnode_inv_def) apply (auto intro: real_cte_emptyable_strg[rule_format]
               simp: silc_inv_def reads_equiv_f_def requiv_cur_thread_eq caps_of_state_cteD
                     aag_cap_auth_recycle_EndpointCap cte_wp_at_weak_derived_ReplyCap ) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci) (invoke_cnode ci) proof (prove)
goal (1 subgoal):
 1. reads_respects_f aag l (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci) (case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail) proof (prove)
goal (2 subgoals):
 1. reads_respects_f aag l ?Q (case ci of InsertCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_insert cap src_slot dest_slot | MoveCall cap src_slot dest_slot \<Rightarrow> without_preemption $ cap_move cap src_slot dest_slot | RevokeCall dest_slot \<Rightarrow> cap_revoke dest_slot | DeleteCall dest_slot \<Rightarrow> cap_delete dest_slot | RotateCall cap1 cap2 slot1 slot2 slot3 \<Rightarrow> without_preemption $ if slot1 = slot3 then cap_swap cap1 slot1 cap2 slot2 else do cap_move cap2 slot2 slot3;
cap_move cap1 slot1 slot2
od | SaveCall slot \<Rightarrow> without_preemption $ do thread <- gets cur_thread;
src_slot <- return (thread, tcb_cnode_index 3);
cap <- get_cap src_slot;
case cap of NullCap \<Rightarrow> return () | ReplyCap x True xa \<Rightarrow> fail | ReplyCap x False xa \<Rightarrow> cap_move cap src_slot slot | _ \<Rightarrow> fail
od | CancelBadgedSendsCall (EndpointCap ep b R) \<Rightarrow> without_preemption $ when (b \<noteq> 0) $ cancel_badged_sends ep b | CancelBadgedSendsCall _ \<Rightarrow> fail)
 2. \<And>s. (silc_inv aag st and only_timer_irq_inv irq st' and pas_refined aag and einvs and simple_sched_action and valid_cnode_inv ci and (\<lambda>s. is_subject aag (cur_thread s)) and cnode_inv_auth_derivations ci and authorised_cnode_inv aag ci) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. silc_inv aag st s \<and> only_timer_irq_inv irq st' s \<and> pas_refined aag s \<and> invs s \<and> valid_list s \<and> valid_sched s \<and> simple_sched_action s \<and> valid_cnode_inv ci s \<and> is_subject aag (cur_thread s) \<and> cnode_inv_auth_derivations ci s \<and> authorised_cnode_inv aag ci s \<Longrightarrow> (\<forall>x a b aa ba. ci = InsertCall x (a, b) (aa, ba) \<longrightarrow> silc_inv aag (?st50 x (a, b) (aa, ba)) s \<and> aag_can_read aag a \<and> aag_can_read aag aa \<and> cte_wp_at (is_derived (cdt s) (a, b) x) (a, b) s \<and> pasObjectAbs aag a = pasObjectAbs aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel) \<and> (\<forall>x a b aa ba. ci = MoveCall x (a, b) (aa, ba) \<longrightarrow> silc_inv aag (?st57 x (a, b) (aa, ba)) s \<and> is_subject aag a \<and> is_subject aag aa \<and> cte_wp_at (weak_derived x) (a, b) s \<and> pasObjectAbs aag a = pasObjectAbs aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel) \<and> (\<forall>a b. ci = RevokeCall (a, b) \<longrightarrow> silc_inv aag (?st63 (a, b)) s \<and> only_timer_irq_inv (?irq63 (a, b)) (?st'63 (a, b)) s \<and> is_subject aag a) \<and> (\<forall>a b. ci = DeleteCall (a, b) \<longrightarrow> silc_inv aag (?st66 (a, b)) s \<and> only_timer_irq_inv (?irq66 (a, b)) (?st'66 (a, b)) s \<and> emptyable (a, b) s \<and> cdt_change_allowed' aag (a, b) s) \<and> (\<forall>x xa a b aa ba ab bb. ci = RotateCall x xa (a, b) (aa, ba) (ab, bb) \<longrightarrow> (a = ab \<and> b = bb \<longrightarrow> silc_inv aag (?st71 x xa (ab, bb) (aa, ba) (ab, bb)) s \<and> is_subject aag ab \<and> is_subject aag aa \<and> cte_wp_at (weak_derived x) (ab, bb) s \<and> cte_wp_at (weak_derived xa) (aa, ba) s \<and> pasObjectAbs aag ab = pasObjectAbs aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> silc_inv aag (?st85 x xa (a, b) (aa, ba) (ab, bb)) s \<and> is_subject aag aa \<and> is_subject aag ab \<and> cte_wp_at (weak_derived xa) (aa, ba) s \<and> pasObjectAbs aag aa = pasObjectAbs aag ab \<and> pasObjectAbs aag ab \<noteq> SilcLabel \<and> silc_inv aag (?st96 x xa (a, b) (aa, ba) (ab, bb)) s \<and> cte_wp_at (weak_derived xa) (aa, ba) s \<and> pasObjectAbs aag aa = pasObjectAbs aag ab \<and> pasObjectAbs aag ab \<noteq> SilcLabel \<and> is_subject aag a \<and> is_subject aag aa \<and> cte_wp_at (weak_derived x) (a, b) s \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<and> pasObjectAbs aag a = pasObjectAbs aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel)) \<and> (\<forall>a b. ci = SaveCall (a, b) \<longrightarrow> silc_inv aag (?st243 (a, b)) s \<and> silc_inv aag (?st231 (a, b) (cur_thread s)) s \<and> pas_refined (?aag234 (a, b) (cur_thread s)) s \<and> is_subject (?aag234 (a, b) (cur_thread s)) (cur_thread s) \<and> ((\<exists>cap. caps_of_state s (cur_thread s, tcb_cnode_index 3) = Some cap \<and> pas_cap_cur_auth (?aag234 (a, b) (cur_thread s)) cap) \<longrightarrow> silc_inv aag (?st231 (a, b) (cur_thread s)) s) \<and> pas_refined (?aag240 (a, b) (cur_thread s)) s \<and> is_subject (?aag240 (a, b) (cur_thread s)) (cur_thread s) \<and> (\<forall>cap. caps_of_state s (cur_thread s, tcb_cnode_index 3) = Some cap \<and> pas_cap_cur_auth (?aag240 (a, b) (cur_thread s)) cap \<longrightarrow> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> silc_inv aag (?st204 (a, b) (cur_thread s) (ReplyCap x False xb) x False xb) s \<and> is_subject aag a \<and> cte_wp_at (weak_derived (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s \<and> pasSubject aag = pasObjectAbs aag a \<and> pasObjectAbs aag a \<noteq> SilcLabel))) \<and> (\<forall>x. ci = CancelBadgedSendsCall x \<longrightarrow> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> xb \<noteq> 0 \<longrightarrow> silc_inv aag (?st342 (EndpointCap xa xb xc) xa xb xc) s \<and> is_subject aag xa)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>silc_inv aag st s; only_timer_irq_inv irq st' s; pas_refined aag s; invs s; valid_list s; valid_sched s; simple_sched_action s; valid_cnode_inv ci s; is_subject aag (cur_thread s); (case ci of InsertCall cap ptr ptr' \<Rightarrow> cte_wp_at (auth_derived cap) ptr | MoveCall cap ptr ptr' \<Rightarrow> cte_wp_at (auth_derived cap) ptr | RotateCall s_cap p_cap src pivot dest \<Rightarrow> cte_wp_at (auth_derived s_cap) src and cte_wp_at (auth_derived p_cap) pivot | _ \<Rightarrow> \<lambda>_. True) s; case ci of InsertCall cap ptr ptr' \<Rightarrow> pasObjectAbs aag ` {fst ptr, fst ptr'} \<subseteq> {pasSubject aag} | MoveCall cap ptr ptr' \<Rightarrow> pasObjectAbs aag ` {fst ptr, fst ptr'} \<subseteq> {pasSubject aag} | RevokeCall ptr \<Rightarrow> is_subject aag (fst ptr) | DeleteCall ptr \<Rightarrow> is_subject aag (fst ptr) | RotateCall s_cap p_cap src pivot dest \<Rightarrow> pasObjectAbs aag ` {fst src, fst pivot, fst dest} \<subseteq> {pasSubject aag} | SaveCall ptr \<Rightarrow> is_subject aag (fst ptr) | CancelBadgedSendsCall x \<Rightarrow> pas_cap_cur_auth aag x\<rbrakk> \<Longrightarrow> (\<forall>x a b aa ba. ci = InsertCall x (a, b) (aa, ba) \<longrightarrow> silc_inv aag (?st50 x (a, b) (aa, ba)) s \<and> aag_can_read aag a \<and> aag_can_read aag aa \<and> cte_wp_at (is_derived (cdt s) (a, b) x) (a, b) s \<and> pasObjectAbs aag a = pasObjectAbs aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel) \<and> (\<forall>x a b aa ba. ci = MoveCall x (a, b) (aa, ba) \<longrightarrow> silc_inv aag (?st57 x (a, b) (aa, ba)) s \<and> is_subject aag a \<and> is_subject aag aa \<and> cte_wp_at (weak_derived x) (a, b) s \<and> pasObjectAbs aag a = pasObjectAbs aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel) \<and> (\<forall>a b. ci = RevokeCall (a, b) \<longrightarrow> silc_inv aag (?st63 (a, b)) s \<and> only_timer_irq_inv (?irq63 (a, b)) (?st'63 (a, b)) s \<and> is_subject aag a) \<and> (\<forall>a b. ci = DeleteCall (a, b) \<longrightarrow> silc_inv aag (?st66 (a, b)) s \<and> only_timer_irq_inv (?irq66 (a, b)) (?st'66 (a, b)) s \<and> emptyable (a, b) s \<and> cdt_change_allowed' aag (a, b) s) \<and> (\<forall>x xa a b aa ba ab bb. ci = RotateCall x xa (a, b) (aa, ba) (ab, bb) \<longrightarrow> (a = ab \<and> b = bb \<longrightarrow> silc_inv aag (?st71 x xa (ab, bb) (aa, ba) (ab, bb)) s \<and> is_subject aag ab \<and> is_subject aag aa \<and> cte_wp_at (weak_derived x) (ab, bb) s \<and> cte_wp_at (weak_derived xa) (aa, ba) s \<and> pasObjectAbs aag ab = pasObjectAbs aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel) \<and> ((a = ab \<longrightarrow> b \<noteq> bb) \<longrightarrow> silc_inv aag (?st85 x xa (a, b) (aa, ba) (ab, bb)) s \<and> is_subject aag aa \<and> is_subject aag ab \<and> cte_wp_at (weak_derived xa) (aa, ba) s \<and> pasObjectAbs aag aa = pasObjectAbs aag ab \<and> pasObjectAbs aag ab \<noteq> SilcLabel \<and> silc_inv aag (?st96 x xa (a, b) (aa, ba) (ab, bb)) s \<and> cte_wp_at (weak_derived xa) (aa, ba) s \<and> pasObjectAbs aag aa = pasObjectAbs aag ab \<and> pasObjectAbs aag ab \<noteq> SilcLabel \<and> is_subject aag a \<and> is_subject aag aa \<and> cte_wp_at (weak_derived x) (a, b) s \<and> (a = aa \<longrightarrow> b \<noteq> ba) \<and> pasObjectAbs aag a = pasObjectAbs aag aa \<and> pasObjectAbs aag aa \<noteq> SilcLabel)) \<and> (\<forall>a b. ci = SaveCall (a, b) \<longrightarrow> silc_inv aag (?st243 (a, b)) s \<and> silc_inv aag (?st231 (a, b) (cur_thread s)) s \<and> pas_refined (?aag234 (a, b) (cur_thread s)) s \<and> is_subject (?aag234 (a, b) (cur_thread s)) (cur_thread s) \<and> ((\<exists>cap. caps_of_state s (cur_thread s, tcb_cnode_index 3) = Some cap \<and> pas_cap_cur_auth (?aag234 (a, b) (cur_thread s)) cap) \<longrightarrow> silc_inv aag (?st231 (a, b) (cur_thread s)) s) \<and> pas_refined (?aag240 (a, b) (cur_thread s)) s \<and> is_subject (?aag240 (a, b) (cur_thread s)) (cur_thread s) \<and> (\<forall>cap. caps_of_state s (cur_thread s, tcb_cnode_index 3) = Some cap \<and> pas_cap_cur_auth (?aag240 (a, b) (cur_thread s)) cap \<longrightarrow> (\<forall>x xa xb. cap = ReplyCap x xa xb \<longrightarrow> \<not> xa \<longrightarrow> silc_inv aag (?st204 (a, b) (cur_thread s) (ReplyCap x False xb) x False xb) s \<and> is_subject aag a \<and> cte_wp_at (weak_derived (ReplyCap x False xb)) (cur_thread s, tcb_cnode_index 3) s \<and> pasSubject aag = pasObjectAbs aag a \<and> pasObjectAbs aag a \<noteq> SilcLabel))) \<and> (\<forall>x. ci = CancelBadgedSendsCall x \<longrightarrow> (\<forall>xa xb xc. x = EndpointCap xa xb xc \<longrightarrow> xb \<noteq> 0 \<longrightarrow> silc_inv aag (?st342 (EndpointCap xa xb xc) xa xb xc) s \<and> is_subject aag xa)) proof (prove)
goal:
No subgoals!