kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchVSpace_AI

lemma vs_lookup_trans:
  "(vs_lookup1 s')^* = (vs_lookup1 s)^* \<union> (vs_lookup1 s)^* O new_lookups^*" using pd pde apply (simp add: vs_lookup1) apply (rule union_trans) apply (subst (asm) new_lookups_def) apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def
                        empty_table_def pde_ref_def
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (vs_lookup1 s')\<^sup>* = (vs_lookup1 s)\<^sup>* \<union> (vs_lookup1 s)\<^sup>* O new_lookups\<^sup>* proof (prove)
using this:
kheap s pdp = Some (ArchObj (PageDirectory pd))
empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))

goal (1 subgoal):
 1. (vs_lookup1 s')\<^sup>* = (vs_lookup1 s)\<^sup>* \<union> (vs_lookup1 s)\<^sup>* O new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s pdp = Some (ArchObj (PageDirectory pd)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (vs_lookup1 s \<union> new_lookups)\<^sup>* = (vs_lookup1 s)\<^sup>* \<union> (vs_lookup1 s)\<^sup>* O new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>kheap s pdp = Some (ArchObj (PageDirectory pd)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); (x, y) \<in> new_lookups; (y, z) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (x, z) \<in> new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>kheap s pdp = Some (ArchObj (PageDirectory pd)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); (x, y) \<in> {((rs, p), rs', p'). rs' = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rs \<and> p = ap \<and> p' = pdp}; (y, z) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> (x, z) \<in> new_lookups\<^sup>* proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vs_lookup:
  "vs_lookup s' = vs_lookup s \<union> new_lookups^* `` vs_lookup s" unfolding vs_lookup_def by (simp add: vs_lookup_trans relcomp_Image Un_Image)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup s' = vs_lookup s \<union> new_lookups\<^sup>* `` vs_lookup s proof (prove)
goal (1 subgoal):
 1. (vs_lookup1 s')\<^sup>* `` vs_asid_refs (asid_table s') = (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<union> new_lookups\<^sup>* `` (vs_lookup1 s)\<^sup>* `` vs_asid_refs (asid_table s)
theory ArchVSpace_AI

lemma vs_lookup2:
  "vs_lookup s' = vs_lookup s \<union> (new_lookups `` vs_lookup s)" by (auto simp add: vs_lookup new_lookups_rtrancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup s' = vs_lookup s \<union> new_lookups `` vs_lookup s
theory ArchVSpace_AI

lemma vs_lookup_pages_trans:
  "(vs_lookup_pages1 s')^* =
   (vs_lookup_pages1 s)^* \<union> (vs_lookup_pages1 s)^* O new_lookups^*" using pd pde apply (simp add: vs_lookup_pages1) apply (rule union_trans) apply (subst (asm) new_lookups_def) apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def
                        graph_of_def empty_table_def pde_ref_pages_def
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (vs_lookup_pages1 s')\<^sup>* = (vs_lookup_pages1 s)\<^sup>* \<union> (vs_lookup_pages1 s)\<^sup>* O new_lookups\<^sup>* proof (prove)
using this:
kheap s pdp = Some (ArchObj (PageDirectory pd))
empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))

goal (1 subgoal):
 1. (vs_lookup_pages1 s')\<^sup>* = (vs_lookup_pages1 s)\<^sup>* \<union> (vs_lookup_pages1 s)\<^sup>* O new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<lbrakk>kheap s pdp = Some (ArchObj (PageDirectory pd)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd))\<rbrakk> \<Longrightarrow> (vs_lookup_pages1 s \<union> new_lookups)\<^sup>* = (vs_lookup_pages1 s)\<^sup>* \<union> (vs_lookup_pages1 s)\<^sup>* O new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>kheap s pdp = Some (ArchObj (PageDirectory pd)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); (x, y) \<in> new_lookups; (y, z) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> (x, z) \<in> new_lookups\<^sup>* proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>kheap s pdp = Some (ArchObj (PageDirectory pd)); empty_table (set (second_level_tables (arch_state s))) (ArchObj (PageDirectory pd)); (x, y) \<in> {((rs, p), rs', p'). rs' = VSRef (UCAST(10 \<rightarrow> 32) asid) (Some AASIDPool) # rs \<and> p = ap \<and> p' = pdp}; (y, z) \<in> vs_lookup_pages1 s\<rbrakk> \<Longrightarrow> (x, z) \<in> new_lookups\<^sup>* proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma vs_lookup_pages:
  "vs_lookup_pages s' =
   vs_lookup_pages s \<union> new_lookups^* `` vs_lookup_pages s" unfolding vs_lookup_pages_def by (simp add: vs_lookup_pages_trans relcomp_Image Un_Image)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages s' = vs_lookup_pages s \<union> new_lookups\<^sup>* `` vs_lookup_pages s proof (prove)
goal (1 subgoal):
 1. (vs_lookup_pages1 s')\<^sup>* `` vs_asid_refs (asid_table s') = (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s) \<union> new_lookups\<^sup>* `` (vs_lookup_pages1 s)\<^sup>* `` vs_asid_refs (asid_table s)
theory ArchVSpace_AI

lemma vs_lookup_pages2:
  "vs_lookup_pages s' = vs_lookup_pages s \<union> (new_lookups `` vs_lookup_pages s)" by (auto simp add: vs_lookup_pages new_lookups_rtrancl)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_lookup_pages s' = vs_lookup_pages s \<union> new_lookups `` vs_lookup_pages s
theory ArchVSpace_AI

lemma not_kernel_slot_not_global_pt:
  "\<lbrakk>pde_ref (pd x) = Some p; x \<notin> kernel_mapping_slots;
    kheap s p' = Some (ArchObj (PageDirectory pd)); valid_kernel_mappings s\<rbrakk>
   \<Longrightarrow> p \<notin> set (second_level_tables (arch_state s))" apply (clarsimp simp: valid_kernel_mappings_def valid_kernel_mappings_if_pd_def) apply (drule_tac x="ArchObj (PageDirectory pd)" in bspec) apply ((fastforce simp: ran_def)+)[1] apply (simp add: second_level_tables_def split: arch_kernel_obj.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref (pd x) = Some p; x \<notin> kernel_mapping_slots; kheap s p' = Some (ArchObj (PageDirectory pd)); valid_kernel_mappings s\<rbrakk> \<Longrightarrow> p \<notin> set (second_level_tables (arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref (pd x) = Some p; x \<notin> kernel_mapping_slots; kheap s p' = Some (ArchObj (PageDirectory pd)); \<forall>x\<in>ran (kheap s). case x of ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) | ArchObj _ \<Rightarrow> True | _ \<Rightarrow> True; p \<in> set (second_level_tables (arch_state s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pde_ref (pd x) = Some p; x \<notin> kernel_mapping_slots; kheap s p' = Some (ArchObj (PageDirectory pd)); p \<in> set (second_level_tables (arch_state s))\<rbrakk> \<Longrightarrow> ArchObj (PageDirectory pd) \<in> ran (kheap s)
 2. \<lbrakk>pde_ref (pd x) = Some p; x \<notin> kernel_mapping_slots; kheap s p' = Some (ArchObj (PageDirectory pd)); p \<in> set (second_level_tables (arch_state s)); case ArchObj (PageDirectory pd) of ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) | ArchObj _ \<Rightarrow> True | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pde_ref (pd x) = Some p; x \<notin> kernel_mapping_slots; kheap s p' = Some (ArchObj (PageDirectory pd)); p \<in> set (second_level_tables (arch_state s)); case ArchObj (PageDirectory pd) of ArchObj (PageDirectory pd) \<Rightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> (r \<in> set (arm_global_pts (arch_state s))) = (x \<in> kernel_mapping_slots) | ArchObj _ \<Rightarrow> True | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma obj_at_not_pt_not_in_global_pts:
  "\<lbrakk> obj_at P p s; valid_arch_state s; valid_global_objs s; \<And>pt. \<not> P (ArchObj (PageTable pt)) \<rbrakk>
          \<Longrightarrow> p \<notin> set (second_level_tables (arch_state s))" unfolding second_level_tables_def apply (rule notI, drule(1) valid_global_ptsD) apply (clarsimp simp: obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P p s; valid_arch_state s; valid_global_objs s; \<And>pt. \<not> P (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> p \<notin> set (second_level_tables (arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P p s; valid_arch_state s; valid_global_objs s; \<And>pt. \<not> P (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> p \<notin> set (arm_global_pts (arch_state s)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>obj_at P p s; valid_arch_state s; valid_global_objs s; \<And>pt. \<not> P (ArchObj (PageTable pt)); \<exists>pt. ako_at (PageTable pt) p s \<and> (\<forall>x. aligned_pte (pt x))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ArchVSpace_AI

lemma valid_vspace_obj_default:
  assumes tyunt: "ty \<noteq> Structures_A.apiobject_type.Untyped"
  shows "ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s'" apply (cases ty, simp_all add: default_object_def tyunt) apply (simp add: valid_vspace_obj_default') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ArchObj ao = default_object ty dev us \<Longrightarrow> valid_vspace_obj ao s' proof (prove)
goal (1 subgoal):
 1. \<And>x6. \<lbrakk>ao = default_arch_object x6 dev us; ty = ArchObject x6\<rbrakk> \<Longrightarrow> valid_vspace_obj (default_arch_object x6 dev us) s' proof (prove)
goal:
No subgoals!
theory Schedule_AI

lemma findM_inv:
  assumes x: "\<And>x. \<lbrace>P\<rbrace> m x \<lbrace>\<lambda>rv. P\<rbrace>"
  shows      "\<lbrace>P\<rbrace> findM m xs \<lbrace>\<lambda>rv. P\<rbrace>" by (rule findM_inv', simp_all add: x)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> findM m xs \<lbrace>\<lambda>rv. P\<rbrace>
theory Schedule_AI

lemma allActiveTCBs_gets:
  "allActiveTCBs = gets (\<lambda>state. {x. getActiveTCB x state \<noteq> None})" by (simp add: allActiveTCBs_def gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. allActiveTCBs = gets (\<lambda>state. {x. getActiveTCB x state \<noteq> None})
theory Schedule_AI

lemma sct_invs:
  "\<lbrace>invs and tcb_at t\<rbrace> modify (cur_thread_update (%_. t)) \<lbrace>\<lambda>rv. invs\<rbrace>" by wp (clarsimp simp add: invs_def cur_tcb_def valid_state_def valid_idle_def
                            valid_irq_node_def valid_machine_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and tcb_at t\<rbrace> modify (cur_thread_update (\<lambda>_. t)) \<lbrace>\<lambda>rv. invs\<rbrace>
theory Schedule_AI

lemma dmo_storeWord_valid_irq_states[wp]:
  "\<lbrace>valid_irq_states\<rbrace> do_machine_op (storeWord x y) \<lbrace>\<lambda>_. valid_irq_states\<rbrace>" apply (simp add: do_machine_op_def |  wp | wpc)+ apply clarsimp apply(erule use_valid[OF _ storeWord_valid_irq_states]) by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states\<rbrace> do_machine_op (storeWord x y) \<lbrace>\<lambda>_. valid_irq_states\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_irq_states s \<Longrightarrow> \<forall>x\<in>fst (storeWord x y (machine_state s)). \<forall>xa. x = ((), xa) \<longrightarrow> valid_irq_states (s\<lparr>machine_state := xa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s xa. \<lbrakk>valid_irq_states s; ((), xa) \<in> fst (storeWord x y (machine_state s))\<rbrakk> \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := xa\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s x. valid_irq_states s \<Longrightarrow> valid_irq_states (s\<lparr>machine_state := machine_state s\<rparr>)
theory Schedule_AI

lemma dmo_kheap_arch_state[wp]:
  "\<lbrace>\<lambda>s. P (kheap s) (arch_state s)\<rbrace>
   do_machine_op a
   \<lbrace>\<lambda>_ s. P (kheap s) (arch_state s)\<rbrace>" by (clarsimp simp: do_machine_op_def simpler_gets_def select_f_def
          simpler_modify_def return_def bind_def valid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (kheap s) (arch_state s)\<rbrace> do_machine_op a \<lbrace>\<lambda>_ s. P (kheap s) (arch_state s)\<rbrace>
theory Schedule_AI

lemma (in Schedule_AI) stt_tcb [wp]:
  "\<lbrace>tcb_at t\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. (tcb_at t :: 'a state \<Rightarrow> bool)\<rbrace>" apply (simp add: switch_to_thread_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> switch_to_thread t \<lbrace>\<lambda>_. tcb_at t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- do_extended_op (tcb_sched_action tcb_sched_dequeue t);
modify (cur_thread_update (\<lambda>_. t))
od \<lbrace>\<lambda>_. tcb_at t\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_AI

lemma invs_exst [iff]:
  "invs (trans_state f s) = invs s" by (simp add: invs_def valid_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs (trans_state f s) = invs s
theory Schedule_AI

lemma (in Schedule_AI) stt_activatable:
  "\<lbrace>st_tcb_at runnable t\<rbrace> switch_to_thread t \<lbrace>\<lambda>rv . (ct_in_state activatable :: 'a state \<Rightarrow> bool) \<rbrace>" apply (simp add: switch_to_thread_def) apply (wp | simp add: ct_in_state_def)+ apply (rule hoare_post_imp [OF _ arch_stt_runnable]) apply (clarsimp elim!: pred_tcb_weakenE) apply (rule assert_inv) apply wp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable t\<rbrace> switch_to_thread t \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable t\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- do_extended_op (tcb_sched_action tcb_sched_dequeue t);
modify (cur_thread_update (\<lambda>_. t))
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>state. \<lbrace>?B2 state ()\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>ya. st_tcb_at activatable t\<rbrace>
 2. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb t state = Some y) \<lbrace>?B2 state\<rbrace>
 3. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 4. \<And>s. st_tcb_at runnable t s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>state rv s. st_tcb_at runnable t s \<Longrightarrow> st_tcb_at activatable t s
 2. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb t state = Some y) \<lbrace>\<lambda>a. st_tcb_at runnable t\<rbrace>
 3. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 4. \<And>s. st_tcb_at runnable t s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>state. \<lbrace>?B1 state\<rbrace> assert (\<exists>y. get_tcb t state = Some y) \<lbrace>\<lambda>a. st_tcb_at runnable t\<rbrace>
 2. \<lbrace>?Q\<rbrace> get \<lbrace>?B1\<rbrace>
 3. \<And>s. st_tcb_at runnable t s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> get \<lbrace>\<lambda>state. st_tcb_at runnable t\<rbrace>
 2. \<And>s. st_tcb_at runnable t s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at runnable t s \<Longrightarrow> st_tcb_at runnable t s proof (prove)
goal:
No subgoals!
theory Schedule_AI

lemma invs_upd_cur_valid:
  "\<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. invs\<rbrace>; \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv. tcb_at thread\<rbrace>\<rbrakk>
    \<Longrightarrow> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. invs (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>" by (fastforce simp: valid_def invs_def valid_state_def cur_tcb_def valid_machine_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. invs\<rbrace>; \<lbrace>Q\<rbrace> f \<lbrace>\<lambda>rv. tcb_at thread\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P and Q\<rbrace> f \<lbrace>\<lambda>rv s. invs (s\<lparr>cur_thread := thread\<rparr>)\<rbrace>
theory Schedule_AI

lemma pred_tcb_weaken_strongerE:
  "\<lbrakk> pred_tcb_at proj P t s; \<And>tcb . P (proj tcb) \<Longrightarrow> P' (proj' tcb) \<rbrakk> \<Longrightarrow> pred_tcb_at proj' P' t s" by (auto simp: pred_tcb_at_def elim: obj_at_weakenE)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pred_tcb_at proj P t s; \<And>tcb. P (proj tcb) \<Longrightarrow> P' (proj' tcb)\<rbrakk> \<Longrightarrow> pred_tcb_at proj' P' t s
theory Schedule_AI

lemma OR_choice_weak_wp:
  "\<lbrace>P\<rbrace> f \<sqinter> g \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> OR_choice b f g \<lbrace>Q\<rbrace>" apply (fastforce simp add: OR_choice_def alternative_def valid_def bind_def
                    select_f_def gets_def return_def get_def
          split: option.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> f \<sqinter> g \<lbrace>Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> OR_choice b f g \<lbrace>Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_AI

lemma (in Schedule_AI_U) schedule_invs[wp]:
  "\<lbrace>invs\<rbrace> (Schedule_A.schedule :: (unit,unit) s_monad) \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: Schedule_A.schedule_def allActiveTCBs_def) apply (wp OR_choice_weak_wp dmo_invs thread_get_inv
            do_machine_op_tcb select_ext_weak_wp when_def
          | clarsimp simp: getActiveTCB_def get_tcb_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> schedule \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do cur <- gets cur_thread;
state <- get;
thread <- select {x. \<exists>y. getActiveTCB x state = Some y};
if thread = cur then return () \<sqinter> switch_to_thread thread else switch_to_thread thread
od \<sqinter> do cur <- gets cur_thread;
idl <- gets idle_thread;
if idl = cur then return () \<sqinter> switch_to_idle_thread else switch_to_idle_thread
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory Schedule_AI

lemma get_tcb_exst_update:
  "get_tcb p (trans_state f s) = get_tcb p s" by (simp add: get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. get_tcb p (trans_state f s) = get_tcb p s
theory Schedule_AI

lemma ct_in_state_trans_update[simp]: "ct_in_state st (trans_state f s) = ct_in_state st s" apply (simp add: ct_in_state_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_in_state st (trans_state f s) = ct_in_state st s proof (prove)
goal:
No subgoals!
theory ArchSchedule_AI

lemma clearExMonitor_invs [wp]:
  "\<lbrace>invs\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_. invs\<rbrace>" apply (wp dmo_invs) apply (clarsimp simp: clearExMonitor_def machine_op_lift_def
                        machine_rest_lift_def in_monad select_f_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>m. \<forall>(r, m')\<in>fst (clearExMonitor m). (\<forall>p. in_user_frame p s \<or> underlying_memory m' p = underlying_memory m p) \<and> (\<forall>irq. m = machine_state s \<longrightarrow> (interrupt_states s irq = IRQInactive \<longrightarrow> irq_masks m' irq) \<or> irq_masks m' irq = irq_masks m irq) \<and> invs s proof (prove)
goal:
No subgoals!
theory ArchSchedule_AI

lemma arch_stt_invs [wp,Schedule_AI_asms]:
  "\<lbrace>invs\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: arch_switch_to_thread_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> arch_switch_to_thread t' \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do y <- set_vm_root t';
do_machine_op clearExMonitor
od \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSchedule_AI

lemma arch_stt_runnable[Schedule_AI_asms]:
  "\<lbrace>st_tcb_at runnable t\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>r . st_tcb_at runnable t\<rbrace>" apply (simp add: arch_switch_to_thread_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable t\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>r. st_tcb_at runnable t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at runnable t\<rbrace> do y <- set_vm_root t;
do_machine_op clearExMonitor
od \<lbrace>\<lambda>r. st_tcb_at runnable t\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSchedule_AI

lemma arch_stit_invs[wp, Schedule_AI_asms]:
  "\<lbrace>invs\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. invs\<rbrace>" by (wpsimp wp: svr_invs simp: arch_switch_to_idle_thread_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. invs\<rbrace>
theory ArchSchedule_AI

lemma arch_stit_tcb_at[wp]:
  "\<lbrace>tcb_at t\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. tcb_at t\<rbrace>" apply (simp add: arch_switch_to_idle_thread_def ) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>r. tcb_at t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at t\<rbrace> gets idle_thread >>= set_vm_root \<lbrace>\<lambda>r. tcb_at t\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSchedule_AI

lemma arch_stit_activatable[wp, Schedule_AI_asms]:
  "\<lbrace>ct_in_state activatable\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rv . ct_in_state activatable\<rbrace>" apply (clarsimp simp: arch_switch_to_idle_thread_def) apply (wpsimp simp: ct_in_state_def wp: ct_in_state_thread_state_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state activatable\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_in_state activatable\<rbrace> gets idle_thread >>= set_vm_root \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchSchedule_AI

lemma stit_invs [wp,Schedule_AI_asms]:
  "\<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: switch_to_idle_thread_def) apply (wp sct_invs) by (clarsimp simp: invs_def valid_state_def valid_idle_def cur_tcb_def
                     pred_tcb_at_def valid_machine_state_def obj_at_def is_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> invs s \<and> tcb_at (idle_thread s) s