kings-crown/FVELER_Isabelle huggingface dataset:
theory DetSchedInvs_AI

lemma valid_queues_def2:
  "valid_queues_2 queues ekh kh =
     (\<forall>d p. (\<forall>t \<in> set (queues d p).
              is_etcb_at' t ekh \<and>
              (case ekh t of None \<Rightarrow> False | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and>
              st_tcb_at_kh runnable t kh) \<and>
              distinct (queues d p))" by (clarsimp simp: valid_queues_def
                     conj_assoc[where P="is_etcb_at' t ekh \<and> (case ekh t of
                                           None \<Rightarrow> False |
                                           Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d)"]
                     etcb_at_conj_is_etcb_at[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_queues_2 queues ekh kh = (\<forall>d p. (\<forall>t\<in>set (queues d p). is_etcb_at' t ekh \<and> (case ekh t of None \<Rightarrow> False | Some x \<Rightarrow> tcb_priority x = p \<and> tcb_domain x = d) \<and> st_tcb_at_kh runnable t kh) \<and> distinct (queues d p))
theory DetSchedInvs_AI

lemma schact_is_rct[elim!]: "schact_is_rct s \<Longrightarrow> scheduler_action s = resume_cur_thread" apply (simp add: schact_is_rct_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. schact_is_rct s \<Longrightarrow> scheduler_action s = resume_cur_thread proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma valid_etcbs_lift:
  assumes a: "\<And>P T t. \<lbrace>\<lambda>s. P (typ_at T t s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T t s)\<rbrace>"
      and b: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
    shows "\<lbrace>valid_etcbs\<rbrace> f \<lbrace>\<lambda>rv. valid_etcbs\<rbrace>" apply (rule hoare_lift_Pf[where f="\<lambda>s. ekheap s", OF _ b]) apply (simp add: valid_etcbs_def) apply (simp add: tcb_at_st_tcb_at[symmetric] tcb_at_typ) apply (wp hoare_vcg_all_lift a) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> f \<lbrace>\<lambda>rv. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. valid_etcbs_2 x (kheap s)\<rbrace> f \<lbrace>\<lambda>_ a. valid_etcbs_2 x (kheap a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>ptr. st_tcb_at (\<lambda>_. True) ptr s = is_etcb_at' ptr x\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>ptr. st_tcb_at (\<lambda>_. True) ptr a = is_etcb_at' ptr x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>ptr. typ_at ATCB ptr s = is_etcb_at' ptr x\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>ptr. typ_at ATCB ptr a = is_etcb_at' ptr x\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma valid_queues_lift:
  assumes a: "\<And>Q t. \<lbrace>\<lambda>s. st_tcb_at Q t s\<rbrace> f \<lbrace>\<lambda>rv s. st_tcb_at Q t s\<rbrace>"
      and c: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
      and d: "\<And>P. \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>"
    shows "\<lbrace>valid_queues\<rbrace> f \<lbrace>\<lambda>rv. valid_queues\<rbrace>" apply (rule hoare_lift_Pf[where f="\<lambda>s. ekheap s", OF _ c]) apply (rule hoare_lift_Pf[where f="\<lambda>s. ready_queues s", OF _ d]) apply (simp add: valid_queues_def) apply (wp hoare_vcg_ball_lift hoare_vcg_all_lift hoare_vcg_conj_lift a) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues\<rbrace> f \<lbrace>\<lambda>rv. valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. valid_queues_2 (ready_queues s) x (kheap s)\<rbrace> f \<lbrace>\<lambda>_ a. valid_queues_2 (ready_queues a) x (kheap a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>s. valid_queues_2 xa x (kheap s)\<rbrace> f \<lbrace>\<lambda>_ a. valid_queues_2 xa x (kheap a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>s. \<forall>d p. (\<forall>t\<in>set (xa d p). is_etcb_at' t x \<and> etcb_at' (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t x \<and> st_tcb_at runnable t s) \<and> distinct (xa d p)\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>d p. (\<forall>t\<in>set (xa d p). is_etcb_at' t x \<and> etcb_at' (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t x \<and> st_tcb_at runnable t a) \<and> distinct (xa d p)\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma ct_not_in_q_lift:
  assumes a: "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
      and b: "\<And>P. \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>"
      and c: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>"
    shows "\<lbrace>ct_not_in_q\<rbrace> f \<lbrace>\<lambda>rv. ct_not_in_q\<rbrace>" apply (rule hoare_lift_Pf[where f="\<lambda>s. scheduler_action s", OF _ a]) apply (rule hoare_lift_Pf[where f="\<lambda>s. ready_queues s", OF _ b]) apply (rule hoare_lift_Pf[where f="\<lambda>s. cur_thread s", OF _ c]) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_not_in_q\<rbrace> f \<lbrace>\<lambda>rv. ct_not_in_q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. ct_not_in_q_2 (ready_queues s) x (cur_thread s)\<rbrace> f \<lbrace>\<lambda>_ a. ct_not_in_q_2 (ready_queues a) x (cur_thread a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>s. ct_not_in_q_2 xa x (cur_thread s)\<rbrace> f \<lbrace>\<lambda>_ a. ct_not_in_q_2 xa x (cur_thread a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrace>\<lambda>s. ct_not_in_q_2 xa x xb\<rbrace> f \<lbrace>\<lambda>_ a. ct_not_in_q_2 xa x xb\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma ct_in_cur_domain_lift:
  assumes a: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
      and b: "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
      and c: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>"
      and d: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>"
      and e: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>"
    shows "\<lbrace>ct_in_cur_domain\<rbrace> f \<lbrace>\<lambda>rv. ct_in_cur_domain\<rbrace>" apply (rule hoare_lift_Pf[where f="\<lambda>s. ekheap s", OF _ a]) apply (rule hoare_lift_Pf[where f="\<lambda>s. scheduler_action s", OF _ b]) apply (rule hoare_lift_Pf[where f="\<lambda>s. cur_domain s", OF _ c]) apply (rule hoare_lift_Pf[where f="\<lambda>s. cur_thread s", OF _ d]) apply (rule hoare_lift_Pf[where f="\<lambda>s. idle_thread s", OF _ e]) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_cur_domain\<rbrace> f \<lbrace>\<lambda>rv. ct_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. ct_in_cur_domain_2 (cur_thread s) (idle_thread s) (scheduler_action s) (cur_domain s) x\<rbrace> f \<lbrace>\<lambda>_ a. ct_in_cur_domain_2 (cur_thread a) (idle_thread a) (scheduler_action a) (cur_domain a) x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>s. ct_in_cur_domain_2 (cur_thread s) (idle_thread s) xa (cur_domain s) x\<rbrace> f \<lbrace>\<lambda>_ a. ct_in_cur_domain_2 (cur_thread a) (idle_thread a) xa (cur_domain a) x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. \<lbrace>\<lambda>s. ct_in_cur_domain_2 (cur_thread s) (idle_thread s) xa xb x\<rbrace> f \<lbrace>\<lambda>_ a. ct_in_cur_domain_2 (cur_thread a) (idle_thread a) xa xb x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc. \<lbrace>\<lambda>s. ct_in_cur_domain_2 xc (idle_thread s) xa xb x\<rbrace> f \<lbrace>\<lambda>_ a. ct_in_cur_domain_2 xc (idle_thread a) xa xb x\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb xc xd. \<lbrace>\<lambda>s. ct_in_cur_domain_2 xc xd xa xb x\<rbrace> f \<lbrace>\<lambda>_ a. ct_in_cur_domain_2 xc xd xa xb x\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma weak_valid_sched_action_lift:
  assumes a: "\<And>Q t. \<lbrace>\<lambda>s. st_tcb_at Q t s\<rbrace> f \<lbrace>\<lambda>rv s. st_tcb_at Q t s\<rbrace>"
  assumes c: "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
    shows "\<lbrace>weak_valid_sched_action\<rbrace> f \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace>" apply (rule hoare_lift_Pf[where f="\<lambda>s. scheduler_action s", OF _ c]) apply (simp add: weak_valid_sched_action_def) apply (wp hoare_vcg_all_lift hoare_weak_lift_imp a) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>weak_valid_sched_action\<rbrace> f \<lbrace>\<lambda>rv. weak_valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. weak_valid_sched_action_2 x (ekheap s) (kheap s)\<rbrace> f \<lbrace>\<lambda>_ a. weak_valid_sched_action_2 x (ekheap a) (kheap a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. \<forall>t. x = switch_thread t \<longrightarrow> st_tcb_at runnable t s\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>t. x = switch_thread t \<longrightarrow> st_tcb_at runnable t a\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma switch_in_cur_domain_lift:
  assumes a: "\<And>Q t. \<lbrace>\<lambda>s. etcb_at Q t s\<rbrace> f \<lbrace>\<lambda>rv s. etcb_at Q t s\<rbrace>"
  assumes b: "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
  assumes c: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>"
    shows "\<lbrace>switch_in_cur_domain\<rbrace> f \<lbrace>\<lambda>rv. switch_in_cur_domain\<rbrace>" apply (rule hoare_lift_Pf[where f="\<lambda>s. scheduler_action s", OF _ b]) apply (rule hoare_lift_Pf[where f="\<lambda>s. cur_domain s", OF _ c]) apply (simp add: switch_in_cur_domain_def in_cur_domain_def) apply (wp hoare_vcg_all_lift hoare_weak_lift_imp a c) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>switch_in_cur_domain\<rbrace> f \<lbrace>\<lambda>rv. switch_in_cur_domain\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. switch_in_cur_domain_2 x (ekheap s) (cur_domain s)\<rbrace> f \<lbrace>\<lambda>_ a. switch_in_cur_domain_2 x (ekheap a) (cur_domain a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>s. switch_in_cur_domain_2 x (ekheap s) xa\<rbrace> f \<lbrace>\<lambda>_ a. switch_in_cur_domain_2 x (ekheap a) xa\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xa. \<lbrace>\<lambda>s. \<forall>t. x = switch_thread t \<longrightarrow> etcb_at (\<lambda>t. tcb_domain t = xa) t s\<rbrace> f \<lbrace>\<lambda>_ a. \<forall>t. x = switch_thread t \<longrightarrow> etcb_at (\<lambda>t. tcb_domain t = xa) t a\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma valid_sched_action_lift:
  assumes a: "\<And>Q t. \<lbrace>\<lambda>s. st_tcb_at Q t s\<rbrace> f \<lbrace>\<lambda>rv s. st_tcb_at Q t s\<rbrace>"
  assumes b: "\<And>Q t. \<lbrace>\<lambda>s. etcb_at Q t s\<rbrace> f \<lbrace>\<lambda>rv s. etcb_at Q t s\<rbrace>"
  assumes c: "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
  assumes d: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>"
  assumes e: "\<And>Q t. \<lbrace>\<lambda>s. Q (cur_domain s)\<rbrace> f \<lbrace>\<lambda>rv s. Q (cur_domain s)\<rbrace>"
    shows "\<lbrace>valid_sched_action\<rbrace> f \<lbrace>\<lambda>rv. valid_sched_action\<rbrace>" apply (rule hoare_lift_Pf[where f="\<lambda>s. cur_thread s", OF _ d]) apply (simp add: valid_sched_action_def) apply (rule hoare_vcg_conj_lift) apply (rule hoare_lift_Pf[where f="\<lambda>s. scheduler_action s", OF _ c]) apply (simp add: is_activatable_def) apply (wp weak_valid_sched_action_lift switch_in_cur_domain_lift hoare_weak_lift_imp a b c d e)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched_action\<rbrace> f \<lbrace>\<lambda>rv. valid_sched_action\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. valid_sched_action_2 (scheduler_action s) (ekheap s) (kheap s) x (cur_domain s)\<rbrace> f \<lbrace>\<lambda>_ a. valid_sched_action_2 (scheduler_action a) (ekheap a) (kheap a) x (cur_domain a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. is_activatable x s \<and> weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> f \<lbrace>\<lambda>_ a. is_activatable x a \<and> weak_valid_sched_action a \<and> switch_in_cur_domain a\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>is_activatable x\<rbrace> f \<lbrace>\<lambda>rv. is_activatable x\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>s. weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> f \<lbrace>\<lambda>rv s. weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrace>\<lambda>s. is_activatable_2 x xa (kheap s)\<rbrace> f \<lbrace>\<lambda>_ a. is_activatable_2 x xa (kheap a)\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>s. weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> f \<lbrace>\<lambda>rv s. weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x xa. \<lbrace>\<lambda>s. xa = resume_cur_thread \<longrightarrow> st_tcb_at activatable x s\<rbrace> f \<lbrace>\<lambda>_ a. xa = resume_cur_thread \<longrightarrow> st_tcb_at activatable x a\<rbrace>
 2. \<And>x. \<lbrace>\<lambda>s. weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> f \<lbrace>\<lambda>rv s. weak_valid_sched_action s \<and> switch_in_cur_domain s\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma valid_sched_lift:
  assumes a: "\<And>Q t. \<lbrace>\<lambda>s. st_tcb_at Q t s\<rbrace> f \<lbrace>\<lambda>rv s. st_tcb_at Q t s\<rbrace>"
  assumes b: "\<And>Q t. \<lbrace>\<lambda>s. etcb_at Q t s\<rbrace> f \<lbrace>\<lambda>rv s. etcb_at Q t s\<rbrace>"
  assumes c: "\<And>P T t. \<lbrace>\<lambda>s. P (typ_at T t s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T t s)\<rbrace>"
  assumes d: "\<And>P. \<lbrace>\<lambda>s. P (ekheap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ekheap s)\<rbrace>"
  assumes e: "\<And>P. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> f \<lbrace>\<lambda>rv s. P (scheduler_action s)\<rbrace>"
  assumes f: "\<And>P. \<lbrace>\<lambda>s. P (ready_queues s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ready_queues s)\<rbrace>"
  assumes g: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_domain s)\<rbrace>"
  assumes h: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>"
  assumes i: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>rv s. P (idle_thread s)\<rbrace>"
    shows "\<lbrace>valid_sched\<rbrace> f \<lbrace>\<lambda>rv. valid_sched\<rbrace>" apply (simp add: valid_sched_def) apply (wp valid_etcbs_lift valid_queues_lift ct_not_in_q_lift ct_in_cur_domain_lift
            valid_sched_action_lift valid_blocked_lift a b c d e f g h i hoare_vcg_conj_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> f \<lbrace>\<lambda>rv. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s\<rbrace> f \<lbrace>\<lambda>rv s. valid_etcbs s \<and> valid_queues s \<and> ct_not_in_q s \<and> valid_sched_action s \<and> ct_in_cur_domain s \<and> valid_blocked s \<and> valid_idle_etcb s\<rbrace> proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma valid_etcbs_tcb_etcb:
  "\<lbrakk> valid_etcbs s; kheap s ptr = Some (TCB tcb) \<rbrakk> \<Longrightarrow> \<exists>etcb. ekheap s ptr = Some etcb" by (force simp: valid_etcbs_def is_etcb_at_def st_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_etcbs s; kheap s ptr = Some (TCB tcb)\<rbrakk> \<Longrightarrow> \<exists>etcb. ekheap s ptr = Some etcb
theory DetSchedInvs_AI

lemma valid_etcbs_get_tcb_get_etcb:
  "\<lbrakk> valid_etcbs s; get_tcb ptr s = Some tcb \<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb ptr s = Some etcb" apply (clarsimp simp: valid_etcbs_def st_tcb_at_def obj_at_def is_etcb_at_def get_etcb_def get_tcb_def
                  split: option.splits if_split) apply (erule_tac x=ptr in allE) apply (clarsimp simp: get_etcb_def split: option.splits kernel_object.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_etcbs s; get_tcb ptr s = Some tcb\<rbrakk> \<Longrightarrow> \<exists>etcb. get_etcb ptr s = Some etcb proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>\<forall>ptr. (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y); kheap s ptr = Some x2; (case x2 of TCB tcb \<Rightarrow> Some tcb | _ \<Rightarrow> None) = Some tcb\<rbrakk> \<Longrightarrow> \<exists>etcb. ekheap s ptr = Some etcb proof (prove)
goal (1 subgoal):
 1. \<And>x2. \<lbrakk>kheap s ptr = Some x2; (case x2 of TCB tcb \<Rightarrow> Some tcb | _ \<Rightarrow> None) = Some tcb; (\<exists>ko. kheap s ptr = Some ko \<and> (\<exists>tcb. ko = TCB tcb)) = (\<exists>y. ekheap s ptr = Some y)\<rbrakk> \<Longrightarrow> \<exists>etcb. ekheap s ptr = Some etcb proof (prove)
goal:
No subgoals!
theory DetSchedInvs_AI

lemma ekheap_tcb_at:
  "\<lbrakk>ekheap s x = Some y; valid_etcbs s\<rbrakk> \<Longrightarrow> tcb_at x s" by (fastforce simp: valid_etcbs_def is_etcb_at_def st_tcb_at_def obj_at_def is_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ekheap s x = Some y; valid_etcbs s\<rbrakk> \<Longrightarrow> tcb_at x s
theory DetSchedInvs_AI

lemma tcb_at_is_etcb_at:
  "\<lbrakk>tcb_at t s; valid_etcbs s\<rbrakk> \<Longrightarrow> is_etcb_at t s" by (simp add: valid_etcbs_def tcb_at_st_tcb_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at t s; valid_etcbs s\<rbrakk> \<Longrightarrow> is_etcb_at t s
theory DetSchedInvs_AI

lemma tcb_at_ekheap_dom:
  "\<lbrakk>tcb_at x s; valid_etcbs s\<rbrakk> \<Longrightarrow> (\<exists>etcb. ekheap s x = Some etcb)" by (auto simp: is_etcb_at_def dest: tcb_at_is_etcb_at)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_at x s; valid_etcbs s\<rbrakk> \<Longrightarrow> \<exists>etcb. ekheap s x = Some etcb
theory DetSchedInvs_AI

lemma ekheap_kheap_dom:
  "\<lbrakk>ekheap s x = Some etcb; valid_etcbs s\<rbrakk>
    \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb)" by (fastforce simp: valid_etcbs_def st_tcb_at_def obj_at_def is_etcb_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ekheap s x = Some etcb; valid_etcbs s\<rbrakk> \<Longrightarrow> \<exists>tcb. kheap s x = Some (TCB tcb)
theory DetSchedAux_AI

lemma create_cap_ct[wp]: "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> create_cap a b c d e \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>" apply (simp add: create_cap_def) apply (rule hoare_pre) apply (wp dxo_wp_weak | wpc | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> create_cap a b c d e \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> case e of (dest, oref) \<Rightarrow> do dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
y <- set_cdt (cdt(dest \<mapsto> c));
y <- do_extended_op (create_cap_ext c dest dest_p);
y <- set_original dest True;
set_cap (default_cap a oref b d) dest
od \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case e of (dest, oref) \<Rightarrow> do dest_p <- gets (\<lambda>s. cdt s dest);
cdt <- gets cdt;
y <- set_cdt (cdt(dest \<mapsto> c));
y <- do_extended_op (create_cap_ext c dest dest_p);
y <- set_original dest True;
set_cap (default_cap a oref b d) dest
od \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>
 2. \<And>s. P (cur_thread s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory DetSchedAux_AI

lemma retype_region_valid_etcbs[wp]:"\<lbrace>valid_etcbs\<rbrace> retype_region a b c d dev \<lbrace>\<lambda>_. valid_etcbs\<rbrace>" apply (simp add: retype_region_def) apply (simp add: retype_region_ext_def bind_assoc) apply wp apply (clarsimp simp del: fun_upd_apply) apply (blast intro: valid_etcb_fold_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> retype_region a b c d dev \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> do y <- when (d \<noteq> Untyped) (do kh <- gets kheap;
y <- retype_region_ext (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) d;
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) kh))
od);
return (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b])
od \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_etcbs\<rbrace> do y <- when (d \<noteq> Untyped) (do kh <- gets kheap;
x <- gets ekheap;
xa <- gets cur_domain;
y <- modify (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext d xa)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) x));
modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) kh))
od);
return (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b])
od \<lbrace>\<lambda>_. valid_etcbs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_etcbs s \<Longrightarrow> (if d \<noteq> Untyped then \<lambda>s. valid_etcbs (s\<lparr>ekheap := foldr (\<lambda>p ekh. ekh(p := default_ext d (cur_domain s))) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (ekheap s), kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (kheap s)\<rparr>) else valid_etcbs) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_etcbs s; d \<noteq> Untyped\<rbrakk> \<Longrightarrow> valid_etcbs_2 (foldr (\<lambda>p ekh. ekh(p := default_ext d (cur_domain s))) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (ekheap s)) (foldr (\<lambda>p kh. kh(p \<mapsto> default_object d dev c)) (map (\<lambda>p. ptr_add a (p * 2 ^ obj_bits_api d c)) [0..<b]) (kheap s)) proof (prove)
goal:
No subgoals!
theory DetSchedAux_AI

lemma create_cap_no_pred_tcb_at: "\<lbrace>\<lambda>s. \<not> pred_tcb_at proj P t s\<rbrace>
          create_cap apiobject_type nat' prod'' dev x
          \<lbrace>\<lambda>r s. \<not> pred_tcb_at proj P t s\<rbrace>" by (rule typ_at_pred_tcb_at_lift; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<not> pred_tcb_at proj P t s\<rbrace> create_cap apiobject_type nat' prod'' dev x \<lbrace>\<lambda>r s. \<not> pred_tcb_at proj P t s\<rbrace>