theory Noninterference

lemma schedule_cur_domain:
  "\<lbrace>\<lambda>s. P (cur_domain s) \<and> domain_time s \<noteq> 0\<rbrace>
   schedule
   \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>"
   (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>") supply hoare_pre_cont[where f=next_domain, wp add]
         ethread_get_wp[wp del] if_split[split del] if_cong[cong] apply (simp add: schedule_def schedule_choose_new_thread_def | wp | wpc)+ apply (rule_tac Q="\<lambda>_. ?PRE" in hoare_strengthen_post) apply (simp | wp gts_wp | wp (once) hoare_drop_imps)+ apply (rule_tac Q="\<lambda>_. ?PRE" in hoare_strengthen_post) apply (simp | wp gts_wp | wp (once) hoare_drop_imps)+ apply (rule_tac Q="\<lambda>_. ?PRE" in hoare_strengthen_post) apply (simp | wp gts_wp | wp (once) hoare_drop_imps)+ apply (clarsimp split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_domain s) \<and> domain_time s \<noteq> 0\<rbrace> schedule \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_domain s) \<and> domain_time s \<noteq> 0\<rbrace> schedule \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace> proof (prove)
goal (14 subgoals):
 1. \<And>ct ct_st x x2 xa xb xc xd xe xf. \<lbrakk>x = switch_thread x2; xd \<and> \<not> xf\<rbrakk> \<Longrightarrow> \<lbrace>?Q36 ct ct_st (switch_thread x2) x2 () xa xb xc True xe False\<rbrace> tcb_sched_action tcb_sched_enqueue x2 \<lbrace>\<lambda>a b. (if domain_time b = 0 then \<lambda>a. False else (\<lambda>a. P (cur_domain a))) (scheduler_action_update (\<lambda>_. choose_new_thread) b)\<rbrace>
 2. \<And>ct ct_st x x2 y xa xb xc xd xe xf. \<lbrakk>x = switch_thread x2; \<not> (xd \<and> \<not> xf)\<rbrakk> \<Longrightarrow> \<lbrace>?R36 ct ct_st x x2 y xa xb xc xd xe xf\<rbrace> if runnable ct_st \<and> xc = xb then do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
dom_time <- gets domain_time;
y <- when (dom_time = 0) next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od else do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 3. \<And>ct ct_st x x2 y xa xb xc xd xe. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B34 ct ct_st x x2 y xa xb xc xd xe\<rbrace> gets (is_highest_prio xe xb) \<lbrace>\<lambda>xf s. (xd \<and> \<not> xf \<longrightarrow> ?Q36 ct ct_st x x2 y xa xb xc xd xe xf s) \<and> (\<not> (xd \<and> \<not> xf) \<longrightarrow> ?R36 ct ct_st x x2 y xa xb xc xd xe xf s)\<rbrace>
 4. \<And>ct ct_st x x2 y xa xb xc xd. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B33 ct ct_st x x2 y xa xb xc xd\<rbrace> gets cur_domain \<lbrace>?B34 ct ct_st x x2 y xa xb xc xd\<rbrace>
 5. \<And>ct ct_st x x2 y xa xb xc. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B32 ct ct_st x x2 y xa xb xc\<rbrace> schedule_switch_thread_fastfail ct xa xc xb \<lbrace>?B33 ct ct_st x x2 y xa xb xc\<rbrace>
 6. \<And>ct ct_st x x2 y xa xb. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B31 ct ct_st x x2 y xa xb\<rbrace> ethread_get_when (ct \<noteq> xa) tcb_priority ct \<lbrace>?B32 ct ct_st x x2 y xa xb\<rbrace>
 7. \<And>ct ct_st x x2 y xa. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B30 ct ct_st x x2 y xa\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B31 ct ct_st x x2 y xa\<rbrace>
 8. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B28 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B30 ct ct_st x x2 y\<rbrace>
 9. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st (switch_thread x2) x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B28 ct ct_st x x2\<rbrace>
 10. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R15 ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
dom_time <- gets domain_time;
y <- when (dom_time = 0) next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>ct ct_st x x2 xa xb xc xd xe xf. \<lbrakk>x = switch_thread x2; xd \<and> \<not> xf\<rbrakk> \<Longrightarrow> \<lbrace>?Q36 ct ct_st (switch_thread x2) x2 () xa xb xc True xe False\<rbrace> tcb_sched_action tcb_sched_enqueue x2 \<lbrace>\<lambda>_ s. P (cur_domain s) \<and> domain_time s \<noteq> 0\<rbrace>
 2. \<And>ct ct_st x x2 xa xb xc xd xe xf rv s. \<lbrakk>x = switch_thread x2; xd \<and> \<not> xf; P (cur_domain s) \<and> domain_time s \<noteq> 0\<rbrakk> \<Longrightarrow> (if domain_time s = 0 then \<lambda>a. False else (\<lambda>a. P (cur_domain a))) (scheduler_action_update (\<lambda>_. choose_new_thread) s)
 3. \<And>ct ct_st x x2 y xa xb xc xd xe xf. \<lbrakk>x = switch_thread x2; \<not> (xd \<and> \<not> xf)\<rbrakk> \<Longrightarrow> \<lbrace>?R36 ct ct_st x x2 y xa xb xc xd xe xf\<rbrace> if runnable ct_st \<and> xc = xb then do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
dom_time <- gets domain_time;
y <- when (dom_time = 0) next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od else do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 4. \<And>ct ct_st x x2 y xa xb xc xd xe. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B34 ct ct_st x x2 y xa xb xc xd xe\<rbrace> gets (is_highest_prio xe xb) \<lbrace>\<lambda>xf s. (xd \<and> \<not> xf \<longrightarrow> ?Q36 ct ct_st x x2 y xa xb xc xd xe xf s) \<and> (\<not> (xd \<and> \<not> xf) \<longrightarrow> ?R36 ct ct_st x x2 y xa xb xc xd xe xf s)\<rbrace>
 5. \<And>ct ct_st x x2 y xa xb xc xd. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B33 ct ct_st x x2 y xa xb xc xd\<rbrace> gets cur_domain \<lbrace>?B34 ct ct_st x x2 y xa xb xc xd\<rbrace>
 6. \<And>ct ct_st x x2 y xa xb xc. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B32 ct ct_st x x2 y xa xb xc\<rbrace> schedule_switch_thread_fastfail ct xa xc xb \<lbrace>?B33 ct ct_st x x2 y xa xb xc\<rbrace>
 7. \<And>ct ct_st x x2 y xa xb. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B31 ct ct_st x x2 y xa xb\<rbrace> ethread_get_when (ct \<noteq> xa) tcb_priority ct \<lbrace>?B32 ct ct_st x x2 y xa xb\<rbrace>
 8. \<And>ct ct_st x x2 y xa. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B30 ct ct_st x x2 y xa\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B31 ct ct_st x x2 y xa\<rbrace>
 9. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B28 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B30 ct ct_st x x2 y\<rbrace>
 10. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st (switch_thread x2) x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B28 ct ct_st x x2\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>ct ct_st x x2 xa xb xd xe xf. \<lbrakk>x = switch_thread x2; xd \<longrightarrow> xf; runnable ct_st\<rbrakk> \<Longrightarrow> \<lbrace>?Q75 ct ct_st (switch_thread x2) x2 () xa xb xb xd xe xf\<rbrace> tcb_sched_action tcb_sched_append x2 \<lbrace>\<lambda>a b. (if domain_time b = 0 then \<lambda>a. False else (\<lambda>a. P (cur_domain a))) (scheduler_action_update (\<lambda>_. choose_new_thread) b)\<rbrace>
 2. \<And>ct ct_st x x2 xa xb xc xd xe xf. \<lbrakk>x = switch_thread x2; xd \<longrightarrow> xf; \<not> (runnable ct_st \<and> xc = xb)\<rbrakk> \<Longrightarrow> \<lbrace>?R74 ct ct_st (switch_thread x2) x2 () xa xb xc xd xe xf\<rbrace> do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 3. \<And>ct ct_st x x2 y xa xb xc xd xe. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B34 ct ct_st x x2 y xa xb xc xd xe\<rbrace> gets (is_highest_prio xe xb) \<lbrace>\<lambda>xf s. (xd \<and> \<not> xf \<longrightarrow> P (cur_domain s) \<and> domain_time s \<noteq> 0) \<and> (\<not> (xd \<and> \<not> xf) \<longrightarrow> (runnable ct_st \<and> xc = xb \<longrightarrow> ?Q75 ct ct_st x x2 y xa xb xc xd xe xf s) \<and> (\<not> (runnable ct_st \<and> xc = xb) \<longrightarrow> ?R74 ct ct_st x x2 y xa xb xc xd xe xf s))\<rbrace>
 4. \<And>ct ct_st x x2 y xa xb xc xd. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B33 ct ct_st x x2 y xa xb xc xd\<rbrace> gets cur_domain \<lbrace>?B34 ct ct_st x x2 y xa xb xc xd\<rbrace>
 5. \<And>ct ct_st x x2 y xa xb xc. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B32 ct ct_st x x2 y xa xb xc\<rbrace> schedule_switch_thread_fastfail ct xa xc xb \<lbrace>?B33 ct ct_st x x2 y xa xb xc\<rbrace>
 6. \<And>ct ct_st x x2 y xa xb. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B31 ct ct_st x x2 y xa xb\<rbrace> ethread_get_when (ct \<noteq> xa) tcb_priority ct \<lbrace>?B32 ct ct_st x x2 y xa xb\<rbrace>
 7. \<And>ct ct_st x x2 y xa. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B30 ct ct_st x x2 y xa\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B31 ct ct_st x x2 y xa\<rbrace>
 8. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B28 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B30 ct ct_st x x2 y\<rbrace>
 9. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st (switch_thread x2) x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B28 ct ct_st x x2\<rbrace>
 10. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R15 ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
dom_time <- gets domain_time;
y <- when (dom_time = 0) next_domain;
y <- choose_thread;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>ct ct_st x x2 xa xb xd xe xf. \<lbrakk>x = switch_thread x2; xd \<longrightarrow> xf; runnable ct_st\<rbrakk> \<Longrightarrow> \<lbrace>?Q75 ct ct_st (switch_thread x2) x2 () xa xb xb xd xe xf\<rbrace> tcb_sched_action tcb_sched_append x2 \<lbrace>\<lambda>_ s. P (cur_domain s) \<and> domain_time s \<noteq> 0\<rbrace>
 2. \<And>ct ct_st x x2 xa xb xd xe xf rv s. \<lbrakk>x = switch_thread x2; xd \<longrightarrow> xf; runnable ct_st; P (cur_domain s) \<and> domain_time s \<noteq> 0\<rbrakk> \<Longrightarrow> (if domain_time s = 0 then \<lambda>a. False else (\<lambda>a. P (cur_domain a))) (scheduler_action_update (\<lambda>_. choose_new_thread) s)
 3. \<And>ct ct_st x x2 xa xb xc xd xe xf. \<lbrakk>x = switch_thread x2; xd \<longrightarrow> xf; \<not> (runnable ct_st \<and> xc = xb)\<rbrakk> \<Longrightarrow> \<lbrace>?R74 ct ct_st (switch_thread x2) x2 () xa xb xc xd xe xf\<rbrace> do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od \<lbrace>\<lambda>_ s. P (cur_domain s)\<rbrace>
 4. \<And>ct ct_st x x2 y xa xb xc xd xe. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B34 ct ct_st x x2 y xa xb xc xd xe\<rbrace> gets (is_highest_prio xe xb) \<lbrace>\<lambda>xf s. (xd \<and> \<not> xf \<longrightarrow> P (cur_domain s) \<and> domain_time s \<noteq> 0) \<and> (\<not> (xd \<and> \<not> xf) \<longrightarrow> (runnable ct_st \<and> xc = xb \<longrightarrow> ?Q75 ct ct_st x x2 y xa xb xc xd xe xf s) \<and> (\<not> (runnable ct_st \<and> xc = xb) \<longrightarrow> ?R74 ct ct_st x x2 y xa xb xc xd xe xf s))\<rbrace>
 5. \<And>ct ct_st x x2 y xa xb xc xd. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B33 ct ct_st x x2 y xa xb xc xd\<rbrace> gets cur_domain \<lbrace>?B34 ct ct_st x x2 y xa xb xc xd\<rbrace>
 6. \<And>ct ct_st x x2 y xa xb xc. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B32 ct ct_st x x2 y xa xb xc\<rbrace> schedule_switch_thread_fastfail ct xa xc xb \<lbrace>?B33 ct ct_st x x2 y xa xb xc\<rbrace>
 7. \<And>ct ct_st x x2 y xa xb. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B31 ct ct_st x x2 y xa xb\<rbrace> ethread_get_when (ct \<noteq> xa) tcb_priority ct \<lbrace>?B32 ct ct_st x x2 y xa xb\<rbrace>
 8. \<And>ct ct_st x x2 y xa. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B30 ct ct_st x x2 y xa\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B31 ct ct_st x x2 y xa\<rbrace>
 9. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B28 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B30 ct ct_st x x2 y\<rbrace>
 10. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st (switch_thread x2) x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B28 ct ct_st x x2\<rbrace>
A total of 15 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>ct ct_st. runnable ct_st \<Longrightarrow> \<lbrace>?Q239 ct ct_st (ds_id choose_new_thread)\<rbrace> tcb_sched_action tcb_sched_enqueue ct \<lbrace>\<lambda>a b. (if domain_time b = 0 then \<lambda>a. False else (\<lambda>a. P (cur_domain a))) b\<rbrace>
 2. \<And>ct ct_st. \<lbrace>?B8 ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> P (cur_domain s)) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> (if runnable ct_st then \<lambda>a. P (cur_domain a) \<and> domain_time a \<noteq> 0 \<and> P (cur_domain a) \<and> domain_time a \<noteq> 0 \<and> P (cur_domain a) else (\<lambda>a. P (cur_domain a) \<and> domain_time a \<noteq> 0 \<and> P (cur_domain a) \<and> domain_time a \<noteq> 0 \<and> P (cur_domain a))) s) \<and> (x = choose_new_thread \<longrightarrow> (if runnable ct_st then ?Q239 ct ct_st x else (\<lambda>a. (if domain_time a = 0 then \<lambda>a. False else (\<lambda>a. P (cur_domain a))) a)) s)\<rbrace>
 3. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 4. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 5. \<And>s. P (cur_domain s) \<and> domain_time s \<noteq> 0 \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>ct ct_st. runnable ct_st \<Longrightarrow> \<lbrace>?Q239 ct ct_st (ds_id choose_new_thread)\<rbrace> tcb_sched_action tcb_sched_enqueue ct \<lbrace>\<lambda>_ s. P (cur_domain s) \<and> domain_time s \<noteq> 0\<rbrace>
 2. \<And>ct ct_st rv s. \<lbrakk>runnable ct_st; P (cur_domain s) \<and> domain_time s \<noteq> 0\<rbrakk> \<Longrightarrow> (if domain_time s = 0 then \<lambda>a. False else (\<lambda>a. P (cur_domain a))) s
 3. \<And>ct ct_st. \<lbrace>?B8 ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> P (cur_domain s)) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> (if runnable ct_st then \<lambda>a. P (cur_domain a) \<and> domain_time a \<noteq> 0 \<and> P (cur_domain a) \<and> domain_time a \<noteq> 0 \<and> P (cur_domain a) else (\<lambda>a. P (cur_domain a) \<and> domain_time a \<noteq> 0 \<and> P (cur_domain a) \<and> domain_time a \<noteq> 0 \<and> P (cur_domain a))) s) \<and> (x = choose_new_thread \<longrightarrow> (if runnable ct_st then ?Q239 ct ct_st x else (\<lambda>a. (if domain_time a = 0 then \<lambda>a. False else (\<lambda>a. P (cur_domain a))) a)) s)\<rbrace>
 4. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 5. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 6. \<And>s. P (cur_domain s) \<and> domain_time s \<noteq> 0 \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P (cur_domain s) \<and> domain_time s \<noteq> 0 \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> scheduler_action s = choose_new_thread \<longrightarrow> (if runnable st then \<lambda>a. P (cur_domain a) \<and> domain_time a \<noteq> 0 else (\<lambda>a. (if domain_time a = 0 then \<lambda>a. False else (\<lambda>a. P (cur_domain a))) a)) s proof (prove)
goal:
No subgoals!