kings-crown/FVELER_Isabelle huggingface dataset:
theory ADT_C

lemma cthread_state_rel_imp_eq:
  "cthread_state_relation x z \<Longrightarrow> cthread_state_relation y z \<Longrightarrow> x=y" apply (simp add: cthread_state_relation_def split_def) apply (cases x) apply (cases y, simp_all add: ThreadState_BlockedOnReceive_def
    ThreadState_BlockedOnReply_def ThreadState_BlockedOnNotification_def
    ThreadState_Running_def ThreadState_Inactive_def
    ThreadState_IdleThreadState_def ThreadState_BlockedOnSend_def
    ThreadState_Restart_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cthread_state_relation x z; cthread_state_relation y z\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cthread_state_relation_lifted x (thread_state_lift (fst z), seL4_Fault_lift (snd z)); cthread_state_relation_lifted y (thread_state_lift (fst z), seL4_Fault_lift (snd z))\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal (8 subgoals):
 1. \<And>x11 x12. \<lbrakk>cthread_state_relation_lifted x (thread_state_lift (fst z), seL4_Fault_lift (snd z)); cthread_state_relation_lifted y (thread_state_lift (fst z), seL4_Fault_lift (snd z)); x = Structures_H.thread_state.BlockedOnReceive x11 x12\<rbrakk> \<Longrightarrow> x = y
 2. \<lbrakk>cthread_state_relation_lifted x (thread_state_lift (fst z), seL4_Fault_lift (snd z)); cthread_state_relation_lifted y (thread_state_lift (fst z), seL4_Fault_lift (snd z)); awaiting_reply' x\<rbrakk> \<Longrightarrow> x = y
 3. \<And>x3. \<lbrakk>cthread_state_relation_lifted x (thread_state_lift (fst z), seL4_Fault_lift (snd z)); cthread_state_relation_lifted y (thread_state_lift (fst z), seL4_Fault_lift (snd z)); x = Structures_H.thread_state.BlockedOnNotification x3\<rbrakk> \<Longrightarrow> x = y
 4. \<lbrakk>cthread_state_relation_lifted x (thread_state_lift (fst z), seL4_Fault_lift (snd z)); cthread_state_relation_lifted y (thread_state_lift (fst z), seL4_Fault_lift (snd z)); x = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> x = y
 5. \<lbrakk>cthread_state_relation_lifted x (thread_state_lift (fst z), seL4_Fault_lift (snd z)); cthread_state_relation_lifted y (thread_state_lift (fst z), seL4_Fault_lift (snd z)); x = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> x = y
 6. \<lbrakk>cthread_state_relation_lifted x (thread_state_lift (fst z), seL4_Fault_lift (snd z)); cthread_state_relation_lifted y (thread_state_lift (fst z), seL4_Fault_lift (snd z)); idle' x\<rbrakk> \<Longrightarrow> x = y
 7. \<And>x71 x72 x73 x74 x75. \<lbrakk>cthread_state_relation_lifted x (thread_state_lift (fst z), seL4_Fault_lift (snd z)); cthread_state_relation_lifted y (thread_state_lift (fst z), seL4_Fault_lift (snd z)); x = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> x = y
 8. \<lbrakk>cthread_state_relation_lifted x (thread_state_lift (fst z), seL4_Fault_lift (snd z)); cthread_state_relation_lifted y (thread_state_lift (fst z), seL4_Fault_lift (snd z)); x = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!
theory ADT_C

lemma ksPSpace_valid_objs_tcbBoundNotification_nonzero:
  "\<exists>s. ksPSpace s = ah \<and> no_0_obj' s \<and> valid_objs' s
     \<Longrightarrow> map_to_tcbs ah p = Some tcb \<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0" apply (clarsimp simp: map_comp_def split: option.splits) apply (erule(1) valid_objsE') apply (clarsimp simp: projectKOs valid_obj'_def valid_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>s. ksPSpace s = ah \<and> no_0_obj' s \<and> valid_objs' s; map_to_tcbs ah p = Some tcb\<rbrakk> \<Longrightarrow> tcbBoundNotification tcb \<noteq> Some 0 proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>ksPSpace s p = Some x2; no_0_obj' s; valid_objs' s; projectKO_opt x2 = Some tcb; ah = ksPSpace s; tcbBoundNotification tcb = Some 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>ksPSpace s p = Some x2; no_0_obj' s; projectKO_opt x2 = Some tcb; ah = ksPSpace s; tcbBoundNotification tcb = Some 0; valid_obj' x2 s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ADT_C

lemma tcb_queue_rel_clift_unique:
  "tcb_queue_relation gn gp (clift s) as pp cp \<Longrightarrow>
   tcb_queue_relation gn gp (clift s) as' pp cp \<Longrightarrow> as' = as" by (rule tcb_queue_rel_unique, rule lift_t_NULL)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation gn gp (clift s) as pp cp; tcb_queue_relation gn gp (clift s) as' pp cp\<rbrakk> \<Longrightarrow> as' = as
theory ADT_C

lemma tcb_queue_rel'_clift_unique:
  "tcb_queue_relation' gn gp (clift s) as pp cp \<Longrightarrow>
   tcb_queue_relation' gn gp (clift s) as' pp cp \<Longrightarrow> as' = as" by (clarsimp simp add: tcb_queue_relation'_def)
     (rule tcb_queue_rel_clift_unique)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>tcb_queue_relation' gn gp (clift s) as pp cp; tcb_queue_relation' gn gp (clift s) as' pp cp\<rbrakk> \<Longrightarrow> as' = as
theory ADT_C

lemma cpspace_ep_relation_unique:
  assumes "cpspace_ep_relation ah ch" "cpspace_ep_relation ah' ch"
  shows   "map_to_eps ah' = map_to_eps ah" apply (rule cmap_relation_unique[OF inj_Ptr _ assms]) apply (clarsimp simp: EPState_Idle_def EPState_Recv_def EPState_Send_def
             cendpoint_relation_def Let_def tcb_queue_rel'_clift_unique
           split: endpoint.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_eps ah' = map_to_eps ah proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>cendpoint_relation (clift ch) x z; cendpoint_relation (clift ch) y z\<rbrakk> \<Longrightarrow> x = y proof (prove)
goal:
No subgoals!
theory ADT_C

lemma ksPSpace_valid_pspace_ntfnBoundTCB_nonzero:
  "\<exists>s. ksPSpace s = ah \<and> valid_pspace' s
     \<Longrightarrow> map_to_ntfns ah p = Some ntfn \<Longrightarrow> ntfnBoundTCB ntfn \<noteq> Some 0" apply (clarsimp simp: map_comp_def valid_pspace'_def split: option.splits) apply (erule(1) valid_objsE') apply (clarsimp simp: projectKOs valid_obj'_def valid_ntfn'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>s. ksPSpace s = ah \<and> valid_pspace' s; map_to_ntfns ah p = Some ntfn\<rbrakk> \<Longrightarrow> ntfnBoundTCB ntfn \<noteq> Some 0 proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>ksPSpace s p = Some x2; valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; projectKO_opt x2 = Some ntfn; ah = ksPSpace s; ntfnBoundTCB ntfn = Some 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>ksPSpace s p = Some x2; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; projectKO_opt x2 = Some ntfn; ah = ksPSpace s; ntfnBoundTCB ntfn = Some 0; valid_obj' x2 s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory ADT_C

lemma tcb_ptr_to_ctcb_ptr_inj:
  "tcb_ptr_to_ctcb_ptr x = tcb_ptr_to_ctcb_ptr y \<Longrightarrow> x = y" by (auto simp: tcb_ptr_to_ctcb_ptr_def ctcb_offset_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcb_ptr_to_ctcb_ptr x = tcb_ptr_to_ctcb_ptr y \<Longrightarrow> x = y
theory ADT_C

lemma cpspace_pde_relation_unique:
  assumes "cpspace_pde_relation ah ch" "cpspace_pde_relation ah' ch"
  shows   "map_to_pdes ah' = map_to_pdes ah" apply (rule cmap_relation_unique[OF inj_Ptr _ assms]) by (simp add: cpde_relation_def s_from_cacheable_def Let_def split: pde.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_pdes ah' = map_to_pdes ah proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>cpde_relation x z; cpde_relation y z\<rbrakk> \<Longrightarrow> x = y
theory ADT_C

lemma cpspace_pte_relation_unique:
  assumes "cpspace_pte_relation ah ch" "cpspace_pte_relation ah' ch"
  shows   "map_to_ptes ah' = map_to_ptes ah" apply (rule cmap_relation_unique[OF inj_Ptr _ assms]) by (simp add: cpte_relation_def s_from_cacheable_def Let_def split: pte.splits bool.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_ptes ah' = map_to_ptes ah proof (prove)
goal (1 subgoal):
 1. \<And>x y z. \<lbrakk>cpte_relation x z; cpte_relation y z\<rbrakk> \<Longrightarrow> x = y
theory ADT_C

lemma valid_objs'_imp_wf_asid_pool':
  "valid_objs' s \<Longrightarrow> \<forall>x\<in>ran (map_to_asidpools (ksPSpace s)). wf_asid_pool' x" apply (clarsimp simp: valid_objs'_def ran_def) apply (case_tac "ksPSpace s a", simp+) apply (rename_tac y, drule_tac x=y in spec) apply (case_tac y, simp_all add: projectKO_opt_asidpool) apply (clarsimp simp: valid_obj'_def
                 split: arch_kernel_object.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_objs' s \<Longrightarrow> \<forall>x\<in>ran (map_to_asidpools (ksPSpace s)). wf_asid_pool' x proof (prove)
goal (1 subgoal):
 1. \<And>x a. \<lbrakk>\<forall>obj. (\<exists>a. ksPSpace s a = Some obj) \<longrightarrow> valid_obj' obj s; map_to_asidpools (ksPSpace s) a = Some x\<rbrakk> \<Longrightarrow> wf_asid_pool' x proof (prove)
goal (1 subgoal):
 1. \<And>x a aa. \<lbrakk>\<forall>obj. (\<exists>a. ksPSpace s a = Some obj) \<longrightarrow> valid_obj' obj s; projectKO_opt aa = Some x; ksPSpace s a = Some aa\<rbrakk> \<Longrightarrow> wf_asid_pool' x proof (prove)
goal (1 subgoal):
 1. \<And>x a y. \<lbrakk>projectKO_opt y = Some x; ksPSpace s a = Some y; (\<exists>a. ksPSpace s a = Some y) \<longrightarrow> valid_obj' y s\<rbrakk> \<Longrightarrow> wf_asid_pool' x proof (prove)
goal (1 subgoal):
 1. \<And>x a y x8. \<lbrakk>(case x8 of KOASIDPool x \<Rightarrow> Some x | _ \<Rightarrow> None) = Some x; ksPSpace s a = Some (KOArch x8); (\<exists>a. ksPSpace s a = Some (KOArch x8)) \<longrightarrow> valid_obj' (KOArch x8) s; y = KOArch x8\<rbrakk> \<Longrightarrow> wf_asid_pool' x proof (prove)
goal:
No subgoals!
theory ADT_C

lemma ksPSpace_eq_imp_ko_wp_at'_eq:
  "ksPSpace s' = ksPSpace s \<Longrightarrow> ko_wp_at' P a s' = ko_wp_at' P a s" by (clarsimp simp: ko_wp_at'_def ps_clear_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksPSpace s' = ksPSpace s \<Longrightarrow> ko_wp_at' P a s' = ko_wp_at' P a s
theory ADT_C

lemma ksPSpace_eq_imp_obj_at'_eq:
  assumes ksPSpace: "ksPSpace s' = ksPSpace s"
  shows "obj_at' P a s' = obj_at' P a s" by (clarsimp simp: obj_at'_real_def ksPSpace_eq_imp_ko_wp_at'_eq[OF ksPSpace])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P a s' = obj_at' P a s
theory ADT_C

lemma ksPSpace_eq_imp_valid_tcb'_eq:
  assumes ksPSpace: "ksPSpace s' = ksPSpace s"
  shows "valid_tcb' tcb s' = valid_tcb' tcb s" by (auto simp: ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace]
                 ksPSpace_eq_imp_valid_cap'_eq[OF ksPSpace]
                 valid_tcb'_def valid_tcb_state'_def valid_bound_ntfn'_def
          split: thread_state.splits option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_tcb' tcb s' = valid_tcb' tcb s
theory ADT_C

lemma ksPSpace_eq_imp_valid_pspace'_eq:
  assumes ksPSpace: "ksPSpace s' = ksPSpace s"
  shows "valid_pspace' s = valid_pspace' s'" using assms by (clarsimp simp: valid_pspace'_def pspace_aligned'_def
        pspace_distinct'_def ps_clear_def no_0_obj'_def valid_mdb'_def
        ksPSpace_eq_imp_valid_objs'_eq[OF ksPSpace])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_pspace' s = valid_pspace' s' proof (prove)
using this:
ksPSpace s' = ksPSpace s

goal (1 subgoal):
 1. valid_pspace' s = valid_pspace' s'
theory ADT_C

lemma cstate_to_pspace_H_correct:
  "valid_pspace' a \<Longrightarrow>
   cpspace_relation (ksPSpace a)
     (underlying_memory (cstate_to_machine_H c)) (t_hrs_' c) \<Longrightarrow>
   cstate_to_pspace_H c = ksPSpace a" apply (simp add: cstate_to_pspace_H_def) apply (rule the_equality, simp) apply (rule_tac s1=a in ksPSpace_eq_imp_valid_pspace'_eq[THEN iffD1],
          clarsimp+) apply (drule (2) cpspace_relation_unique, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' a; cpspace_relation (ksPSpace a) (underlying_memory (cstate_to_machine_H c)) (t_hrs_' c)\<rbrakk> \<Longrightarrow> cstate_to_pspace_H c = ksPSpace a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_pspace' a; cpspace_relation (ksPSpace a) (underlying_memory (cstate_to_machine_H c)) (t_hrs_' c)\<rbrakk> \<Longrightarrow> (THE h. valid_pspace' (undefined\<lparr>ksPSpace := h\<rparr>) \<and> cpspace_relation h (underlying_memory (cstate_to_machine_H c)) (t_hrs_' c)) = ksPSpace a proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_pspace' a; cpspace_relation (ksPSpace a) (underlying_memory (cstate_to_machine_H c)) (t_hrs_' c)\<rbrakk> \<Longrightarrow> valid_pspace' (undefined\<lparr>ksPSpace := ksPSpace a\<rparr>)
 2. \<And>h. \<lbrakk>valid_pspace' a; cpspace_relation (ksPSpace a) (underlying_memory (cstate_to_machine_H c)) (t_hrs_' c); valid_pspace' (undefined\<lparr>ksPSpace := h\<rparr>) \<and> cpspace_relation h (underlying_memory (cstate_to_machine_H c)) (t_hrs_' c)\<rbrakk> \<Longrightarrow> h = ksPSpace a proof (prove)
goal (1 subgoal):
 1. \<And>h. \<lbrakk>valid_pspace' a; cpspace_relation (ksPSpace a) (underlying_memory (cstate_to_machine_H c)) (t_hrs_' c); valid_pspace' (undefined\<lparr>ksPSpace := h\<rparr>); cpspace_relation h (underlying_memory (cstate_to_machine_H c)) (t_hrs_' c)\<rbrakk> \<Longrightarrow> h = ksPSpace a proof (prove)
goal:
No subgoals!
theory ADT_C

lemma (in kernel_m) cDomScheduleIdx_to_H_correct:
  assumes valid: "valid_state' as"
  assumes cstate_rel: "cstate_relation as cs"
  assumes ms: "cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)"
  shows "unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as" using assms by (clarsimp simp: cstate_relation_def Let_def observable_memory_def valid_state'_def
                     newKernelState_def unat_of_nat_eq cdom_schedule_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as proof (prove)
using this:
valid_state' as
cstate_relation as cs
cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)

goal (1 subgoal):
 1. unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as
theory ADT_C

lemma cbitmap_L1_to_H_correct:
  "cbitmap_L1_relation cs as \<Longrightarrow>
   cbitmap_L1_to_H cs = as" unfolding cbitmap_L1_to_H_def cbitmap_L1_relation_def apply (rule ext) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cbitmap_L1_relation cs as \<Longrightarrow> cbitmap_L1_to_H cs = as proof (prove)
goal (1 subgoal):
 1. \<forall>d. (d \<le> maxDomain \<longrightarrow> cs.[unat d] = as d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> as d = 0) \<Longrightarrow> (\<lambda>d. if d \<le> maxDomain then cs.[unat d] else 0) = as proof (prove)
goal (1 subgoal):
 1. \<And>d. \<forall>d. (d \<le> maxDomain \<longrightarrow> cs.[unat d] = as d) \<and> (\<not> d \<le> maxDomain \<longrightarrow> as d = 0) \<Longrightarrow> (if d \<le> maxDomain then cs.[unat d] else 0) = as d proof (prove)
goal:
No subgoals!
theory ADT_C

lemma cpspace_device_data_relation_user_mem'[simp]:
  "cpspace_device_data_relation (ksPSpace as) (option_to_0 \<circ> user_mem' as) (t_hrs_' cs)
  = cpspace_device_data_relation (ksPSpace as)  (underlying_memory (ksMachineState as)) (t_hrs_' cs)" apply (clarsimp simp: cmap_relation_def cuser_user_data_device_relation_def heap_to_device_data_def) apply (rule_tac arg_cong[where  f = "%x. x = y" for y]) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cpspace_device_data_relation (ksPSpace as) (option_to_0 \<circ> user_mem' as) (t_hrs_' cs) = cpspace_device_data_relation (ksPSpace as) (underlying_memory (ksMachineState as)) (t_hrs_' cs) proof (prove)
goal (1 subgoal):
 1. (PTR(user_data_device_C) ` dom (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (option_to_0 \<circ> user_mem' as) p) (map_to_user_data_device (ksPSpace as) p)) = dom (clift (t_hrs_' cs))) = (PTR(user_data_device_C) ` dom (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState as)) p) (map_to_user_data_device (ksPSpace as) p)) = dom (clift (t_hrs_' cs))) proof (prove)
goal (1 subgoal):
 1. PTR(user_data_device_C) ` dom (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (option_to_0 \<circ> user_mem' as) p) (map_to_user_data_device (ksPSpace as) p)) = PTR(user_data_device_C) ` dom (\<lambda>p. map_option (\<lambda>_. byte_to_word_heap (underlying_memory (ksMachineState as)) p) (map_to_user_data_device (ksPSpace as) p))
theory Fastpath_Equiv

lemma setCTE_obj_at'_queued:
  "\<lbrace>obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace>" unfolding setCTE_def by (rule setObject_cte_obj_at_tcb', simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace> setCTE p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace> setObject p v \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (tcbQueued tcb)) t\<rbrace>
theory Fastpath_Equiv

lemma getEndpoint_obj_at':
  "\<lbrace>obj_at' P ptr\<rbrace> getEndpoint ptr \<lbrace>\<lambda>rv s. P rv\<rbrace>" apply (wp getEndpoint_wp) apply (clarsimp simp: obj_at'_def projectKOs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P ptr\<rbrace> getEndpoint ptr \<lbrace>\<lambda>rv s. P rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. obj_at' P ptr s \<Longrightarrow> \<forall>ep. ko_at' ep ptr s \<longrightarrow> P ep proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma tcbSchedEnqueue_tcbContext[wp]:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
     tcbSchedEnqueue t'
   \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>" apply (rule tcbSchedEnqueue_obj_at_unchangedT[OF all_tcbI]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> tcbSchedEnqueue t' \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>f a b c d e fa g h i j k l m n p q. P ((atcbContextGet \<circ> tcbArch) (tcbQueued_update f (Thread a b c d e fa g h i j k l m n p q))) = P ((atcbContextGet \<circ> tcbArch) (Thread a b c d e fa g h i j k l m n p q)) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma setCTE_tcbContext:
  "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
   setCTE slot cte
   \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>" apply (simp add: setCTE_def) apply (rule setObject_cte_obj_at_tcb', simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> setCTE slot cte \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) t\<rbrace> setObject slot cte \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. P (atcbContextGet (tcbArch tcb))) t\<rbrace> proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma seThreadState_tcbContext:
 "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
    setThreadState a b
  \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>" apply (rule setThreadState_obj_at_unchanged) apply (clarsimp simp: atcbContext_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> setThreadState a b \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>f a b c d e fa g h i j k l m n p q. P ((atcbContextGet \<circ> tcbArch) (tcbState_update f (Thread a b c d e fa g h i j k l m n p q))) = P ((atcbContextGet \<circ> tcbArch) (Thread a b c d e fa g h i j k l m n p q))
 2. \<And>f a b c d e fa g h i j k l m n p q. P ((atcbContextGet \<circ> tcbArch) (tcbQueued_update f (Thread a b c d e fa g h i j k l m n p q))) = P ((atcbContextGet \<circ> tcbArch) (Thread a b c d e fa g h i j k l m n p q)) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma setBoundNotification_tcbContext:
 "\<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>
    setBoundNotification a b
  \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet o tcbArch) tcb)) t\<rbrace>" apply (rule setBoundNotification_obj_at_unchanged) apply (clarsimp simp: atcbContext_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> setBoundNotification a b \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P ((atcbContextGet \<circ> tcbArch) tcb)) t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>f a b c d e fa g h i j k l m n p q. P ((atcbContextGet \<circ> tcbArch) (tcbBoundNotification_update f (Thread a b c d e fa g h i j k l m n p q))) = P ((atcbContextGet \<circ> tcbArch) (Thread a b c d e fa g h i j k l m n p q)) proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma obj_at_tcbs_of:
  "obj_at' P t s = (EX tcb. tcbs_of s t = Some tcb & P tcb)" apply (simp add: tcbs_of_def split: if_split) apply (intro conjI impI) apply (clarsimp simp: obj_at'_def projectKOs) apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. obj_at' P t s = (\<exists>tcb. tcbs_of s t = Some tcb \<and> P tcb) proof (prove)
goal (1 subgoal):
 1. (tcb_at' t s \<longrightarrow> obj_at' P t s = (\<exists>tcb. projectKO_opt (the (ksPSpace s t)) = Some tcb \<and> P tcb)) \<and> (\<not> tcb_at' t s \<longrightarrow> \<not> obj_at' P t s) proof (prove)
goal (2 subgoals):
 1. tcb_at' t s \<Longrightarrow> obj_at' P t s = (\<exists>tcb. projectKO_opt (the (ksPSpace s t)) = Some tcb \<and> P tcb)
 2. \<not> tcb_at' t s \<Longrightarrow> \<not> obj_at' P t s proof (prove)
goal (1 subgoal):
 1. \<not> tcb_at' t s \<Longrightarrow> \<not> obj_at' P t s proof (prove)
goal:
No subgoals!
theory Fastpath_Equiv

lemma st_tcb_at_tcbs_of:
  "st_tcb_at' P t s = (EX tcb. tcbs_of s t = Some tcb & P (tcbState tcb))" by (simp add: st_tcb_at'_def obj_at_tcbs_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. st_tcb_at' P t s = (\<exists>tcb. tcbs_of s t = Some tcb \<and> P (tcbState tcb))
theory Fastpath_Equiv

lemma tcbs_of_ko_at':
  "\<lbrakk> tcbs_of s p = Some tcb \<rbrakk> \<Longrightarrow> ko_at' tcb p s" by (simp add: obj_at_tcbs_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tcbs_of s p = Some tcb \<Longrightarrow> ko_at' tcb p s
theory Fastpath_Equiv

lemma acc_CNodeCap_repr:
  "isCNodeCap cap
     \<Longrightarrow> cap = CNodeCap (capCNodePtr cap) (capCNodeBits cap)
                        (capCNodeGuard cap) (capCNodeGuardSize cap)" by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isCNodeCap cap \<Longrightarrow> cap = capability.CNodeCap (capCNodePtr cap) (capCNodeBits cap) (capCNodeGuard cap) (capCNodeGuardSize cap)