kings-crown/FVELER_Isabelle huggingface dataset:
theory TcbAcc_R

lemma setThreadState_ksCurDomain[wp]:
  "\<lbrace> \<lambda>s. P (ksCurDomain s) \<rbrace> setThreadState st tptr \<lbrace>\<lambda>_ s. P (ksCurDomain s) \<rbrace>" apply (simp add: setThreadState_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setThreadState st tptr \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) tptr;
runnable <- isRunnable tptr;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = tptr \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setBoundNotification_ct_idle_or_in_cur_domain'[wp]:
  "\<lbrace>ct_idle_or_in_cur_domain'\<rbrace> setBoundNotification t a \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace>" apply (simp add: setBoundNotification_def) apply (wp threadSet_ct_idle_or_in_cur_domain' hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> setBoundNotification t a \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_idle_or_in_cur_domain'\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. t)) a \<lbrace>\<lambda>rv. ct_idle_or_in_cur_domain'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setBoundNotification_ksCurDomain[wp]:
  "\<lbrace> \<lambda>s. P (ksCurDomain s) \<rbrace> setBoundNotification st tptr \<lbrace>\<lambda>_ s. P (ksCurDomain s) \<rbrace>" apply (simp add: setBoundNotification_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> setBoundNotification st tptr \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksCurDomain s)\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. st)) tptr \<lbrace>\<lambda>_ s. P (ksCurDomain s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setBoundNotification_ksDomSchedule[wp]:
  "\<lbrace> \<lambda>s. P (ksDomSchedule s) \<rbrace> setBoundNotification st tptr \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>" apply (simp add: setBoundNotification_def) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setBoundNotification st tptr \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> threadSet (tcbBoundNotification_update (\<lambda>_. st)) tptr \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_utr[wp]:
  "\<lbrace>untyped_ranges_zero'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. untyped_ranges_zero'\<rbrace>" apply (simp add: cteCaps_of_def) apply (wp untyped_ranges_zero_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>untyped_ranges_zero'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. untyped_ranges_zero'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s)\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. untyped_ranges_zero_inv (map_option cteCap \<circ> ctes_of s) (gsUntypedZeroRanges s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_cap_to'[wp]:
  "\<lbrace>ex_nonz_cap_to' p\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" by (wp ex_nonz_cap_to_pres')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>
theory TcbAcc_R

lemma sts_pred_tcb_neq':
  "\<lbrace>pred_tcb_at' proj P t and K (t \<noteq> t')\<rbrace>
  setThreadState st t'
  \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace>" apply (simp add: setThreadState_def) apply (wp threadSet_pred_tcb_at_state | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t and K (t \<noteq> t')\<rbrace> setThreadState st t' \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pred_tcb_at' proj P t and (\<lambda>y. t \<noteq> t')\<rbrace> do y <- threadSet (tcbState_update (\<lambda>_. st)) t';
runnable <- isRunnable t';
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = t' \<and> action = ResumeCurrentThread) rescheduleRequired
od \<lbrace>\<lambda>_. pred_tcb_at' proj P t\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sts_st_tcb_at'_cases:
  "\<lbrace>\<lambda>s. ((t = t') \<longrightarrow> (P ts \<and> tcb_at' t' s)) \<and> ((t \<noteq> t') \<longrightarrow> st_tcb_at' P t' s)\<rbrace>
     setThreadState ts t
   \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace>" apply (wp sts_st_tcb') apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (t = t' \<longrightarrow> P ts \<and> tcb_at' t' s) \<and> (t \<noteq> t' \<longrightarrow> st_tcb_at' P t' s)\<rbrace> setThreadState ts t \<lbrace>\<lambda>rv. st_tcb_at' P t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (t = t' \<longrightarrow> P ts \<and> tcb_at' t' s) \<and> (t \<noteq> t' \<longrightarrow> st_tcb_at' P t' s) \<Longrightarrow> (if t' = t then K (P ts) else st_tcb_at' P t') s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma threadSet_ct_running':
  "(\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow>
  \<lbrace>ct_running'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. ct_running'\<rbrace>" apply (simp add: ct_in_state'_def) apply (rule hoare_lift_Pf [where f=ksCurThread]) apply (wp threadSet_pred_tcb_no_state; simp) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>ct_running'\<rbrace> threadSet f t \<lbrace>\<lambda>rv. ct_running'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>\<lambda>s. st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s\<rbrace> threadSet f t \<lbrace>\<lambda>rv s. st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) x\<rbrace> threadSet f t \<lbrace>\<lambda>_. st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) x\<rbrace>
 2. \<And>P. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. (\<And>tcb. tcbState (f tcb) = tcbState tcb) \<Longrightarrow> \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> threadSet f t \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma setThreadState_tcb_in_cur_domain'[wp]:
  "\<lbrace>tcb_in_cur_domain' t'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace>" apply (simp add: tcb_in_cur_domain'_def) apply (rule hoare_pre) apply wps apply (wp setThreadState_not_st | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_in_cur_domain' t'\<rbrace> setThreadState st t \<lbrace>\<lambda>_. tcb_in_cur_domain' t'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> setThreadState st t \<lbrace>\<lambda>_ s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. obj_at' (\<lambda>tcb. ksCurDomain prev_s = tcbDomain tcb) t'\<rbrace>
 2. \<And>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t' s \<Longrightarrow> ?P3 s s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_global_refs':   "\<lbrace>valid_global_refs'\<rbrace> asUser t f \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" apply (simp add: asUser_def split_def) apply (wpsimp wp: threadSet_global_refs select_f_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> asUser t f \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma sch_act_sane_lift:
  assumes "\<And>P. \<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
  assumes "\<And>P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ksCurThread s)\<rbrace>"
  shows "\<lbrace>sch_act_sane\<rbrace> f \<lbrace>\<lambda>rv. sch_act_sane\<rbrace>" apply (simp add: sch_act_sane_def) apply (rule hoare_vcg_all_lift) apply (rule hoare_lift_Pf [where f=ksCurThread]) apply (wp assms)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_sane\<rbrace> f \<lbrace>\<lambda>rv. sch_act_sane\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<noteq> ksCurThread s\<rbrace> f \<lbrace>\<lambda>rv s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<noteq> ksCurThread s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrace>\<lambda>s. ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<noteq> ksCurThread s\<rbrace> f \<lbrace>\<lambda>rv s. ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<noteq> ksCurThread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>t x. \<lbrace>\<lambda>s. ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<noteq> x\<rbrace> f \<lbrace>\<lambda>_ a. ksSchedulerAction a = SwitchToThread t \<longrightarrow> t \<noteq> x\<rbrace>
 2. \<And>t P. \<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma storeWordUser_invs[wp]:
  "\<lbrace>invs'\<rbrace> storeWordUser p w \<lbrace>\<lambda>rv. invs'\<rbrace>" by (simp add: storeWordUser_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> storeWordUser p w \<lbrace>\<lambda>rv. invs'\<rbrace>
theory TcbAcc_R

lemma hoare_valid_ipc_buffer_ptr_typ_at':
  "(\<And>q. \<lbrace>typ_at' UserDataT q\<rbrace> a \<lbrace>\<lambda>_. typ_at' UserDataT q\<rbrace>)
   \<Longrightarrow> \<lbrace>valid_ipc_buffer_ptr' p\<rbrace> a \<lbrace>\<lambda>_. valid_ipc_buffer_ptr' p\<rbrace>" unfolding valid_ipc_buffer_ptr'_def2 including no_pre apply wp apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrace>typ_at' UserDataT q\<rbrace> a \<lbrace>\<lambda>_. typ_at' UserDataT q\<rbrace>) \<Longrightarrow> \<lbrace>valid_ipc_buffer_ptr' p\<rbrace> a \<lbrace>\<lambda>_. valid_ipc_buffer_ptr' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrace>typ_at' UserDataT q\<rbrace> a \<lbrace>\<lambda>_. typ_at' UserDataT q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned p msg_align_bits \<and> typ_at' UserDataT (p && ~~ mask pageBits) s\<rbrace> a \<lbrace>\<lambda>_ s. is_aligned p msg_align_bits \<and> typ_at' UserDataT (p && ~~ mask pageBits) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrace>typ_at' UserDataT q\<rbrace> a \<lbrace>\<lambda>_. typ_at' UserDataT q\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. is_aligned p msg_align_bits \<and> typ_at' UserDataT (p && ~~ mask pageBits) s\<rbrace> a \<lbrace>\<lambda>_ s. is_aligned p msg_align_bits \<and> typ_at' UserDataT (p && ~~ mask pageBits) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>q. \<lbrace>typ_at' UserDataT q\<rbrace> a \<lbrace>\<lambda>_. typ_at' UserDataT q\<rbrace>) \<Longrightarrow> \<lbrace>typ_at' UserDataT (p && ~~ mask pageBits)\<rbrace> a \<lbrace>\<lambda>rv. typ_at' UserDataT (p && ~~ mask pageBits)\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma gts_wp':
  "\<lbrace>\<lambda>s. \<forall>st. st_tcb_at' ((=) st) t s \<longrightarrow> P st s\<rbrace> getThreadState t \<lbrace>P\<rbrace>" apply (rule hoare_post_imp) prefer 2 apply (rule gts_sp') apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>st. st_tcb_at' ((=) st) t s \<longrightarrow> P st s\<rbrace> getThreadState t \<lbrace>P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q rv s \<Longrightarrow> P rv s
 2. \<lbrace>\<lambda>s. \<forall>st. st_tcb_at' ((=) st) t s \<longrightarrow> P st s\<rbrace> getThreadState t \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>st. st_tcb_at' ((=) st) t s \<longrightarrow> P st s\<rbrace> getThreadState t \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> P rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (st_tcb_at' (\<lambda>st. st = rv) t and (\<lambda>s. \<forall>st. st_tcb_at' ((=) st) t s \<longrightarrow> P st s)) s \<Longrightarrow> P rv s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma gbn_wp':
  "\<lbrace>\<lambda>s. \<forall>ntfn. bound_tcb_at' ((=) ntfn) t s \<longrightarrow> P ntfn s\<rbrace> getBoundNotification t \<lbrace>P\<rbrace>" apply (rule hoare_post_imp) prefer 2 apply (rule gbn_sp') apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>ntfn. bound_tcb_at' ((=) ntfn) t s \<longrightarrow> P ntfn s\<rbrace> getBoundNotification t \<lbrace>P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. ?Q rv s \<Longrightarrow> P rv s
 2. \<lbrace>\<lambda>s. \<forall>ntfn. bound_tcb_at' ((=) ntfn) t s \<longrightarrow> P ntfn s\<rbrace> getBoundNotification t \<lbrace>?Q\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>\<lambda>s. \<forall>ntfn. bound_tcb_at' ((=) ntfn) t s \<longrightarrow> P ntfn s\<rbrace> getBoundNotification t \<lbrace>?Q\<rbrace>
 2. \<And>rv s. ?Q rv s \<Longrightarrow> P rv s proof (prove)
goal (1 subgoal):
 1. \<And>rv s. (bound_tcb_at' (\<lambda>st. st = rv) t and (\<lambda>s. \<forall>ntfn. bound_tcb_at' ((=) ntfn) t s \<longrightarrow> P ntfn s)) s \<Longrightarrow> P rv s proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma asUser_irq_handlers':
  "\<lbrace>valid_irq_handlers'\<rbrace> asUser t f \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" apply (simp add: asUser_def split_def) apply (wpsimp wp: threadSet_irq_handlers' [OF all_tcbI, OF ball_tcb_cte_casesI] select_f_inv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers'\<rbrace> asUser t f \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_handlers'\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace> proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma non_exst_same_prio_upd[simp]:
  "non_exst_same tcb (tcbPriority_update f tcb)" by (cases tcb, simp add: non_exst_same_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. non_exst_same tcb (tcbPriority_update f tcb)
theory TcbAcc_R

lemma non_exst_same_timeSlice_upd[simp]:
  "non_exst_same tcb (tcbTimeSlice_update f tcb)" by (cases tcb, simp add: non_exst_same_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. non_exst_same tcb (tcbTimeSlice_update f tcb)
theory TcbAcc_R

lemma non_exst_same_domain_upd[simp]:
  "non_exst_same tcb (tcbDomain_update f tcb)" by (cases tcb, simp add: non_exst_same_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. non_exst_same tcb (tcbDomain_update f tcb)
theory TcbAcc_R

lemma archTcbUpdate_aux2: "(\<lambda>tcb. tcb\<lparr> tcbArch := f (tcbArch tcb)\<rparr>) = tcbArch_update f" by (rule ext, case_tac tcb, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lambda>tcb. tcbArch_update (\<lambda>_. f (tcbArch tcb)) tcb) = tcbArch_update f
theory VSpace_R

lemma asidBits_asid_bits[simp]:
  "asidBits = asid_bits" by (simp add: asid_bits_def asidBits_def
                asidHighBits_def asid_low_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. asidBits = local.asid_bits
theory VSpace_R

lemma invalidate_asid_ext_corres:
  "corres dc
          (\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s
               \<and> pspace_aligned s \<and> pspace_distinct s
               \<and> vspace_at_asid a pd s \<and> pd_at_uniq a pd s
               \<and> a \<noteq> 0 \<and> a \<le> mask asid_bits)
          (pspace_aligned' and pspace_distinct' and no_0_obj')
     (invalidate_asid a) (invalidateASID a)" apply (insert invalidateASID_corres) apply (clarsimp simp: corres_underlying_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid a pd s \<and> pd_at_uniq a pd s \<and> a \<noteq> 0 \<and> a \<le> mask local.asid_bits) (pspace_aligned' and pspace_distinct' and no_0_obj') (invalidate_asid a) (invalidateASID a) proof (prove)
goal (1 subgoal):
 1. (\<And>a pd. corres dc (valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and vspace_at_asid a pd and pd_at_uniq a pd and K (a \<noteq> 0 \<and> a \<le> mask local.asid_bits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (invalidate_asid a) (invalidateASID a)) \<Longrightarrow> corres dc (\<lambda>s. \<exists>pd. valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid a pd s \<and> pd_at_uniq a pd s \<and> a \<noteq> 0 \<and> a \<le> mask local.asid_bits) (pspace_aligned' and pspace_distinct' and no_0_obj') (invalidate_asid a) (invalidateASID a) proof (prove)
goal (1 subgoal):
 1. \<And>aa b pd. \<lbrakk>\<And>a pd. \<forall>x\<in>state_relation. case x of (s, s') \<Rightarrow> valid_asid_map s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> vspace_at_asid a pd s \<and> pd_at_uniq a pd s \<and> a \<noteq> 0 \<and> a \<le> mask local.asid_bits \<and> pspace_aligned' s' \<and> pspace_distinct' s' \<and> no_0_obj' s' \<longrightarrow> (\<forall>x\<in>fst (invalidateASID a s'). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (invalidate_asid a s). case x of (r, t) \<Rightarrow> (t, t') \<in> state_relation) \<and> \<not> snd (invalidateASID a s'); (aa, b) \<in> state_relation; valid_asid_map aa; valid_vspace_objs aa; pspace_aligned aa; pspace_distinct aa; pspace_aligned' b; vspace_at_asid a pd aa; pspace_distinct' b; no_0_obj' b; pd_at_uniq a pd aa; a \<noteq> 0; a \<le> mask local.asid_bits\<rbrakk> \<Longrightarrow> (\<forall>x\<in>fst (invalidateASID a b). case x of (r', t') \<Rightarrow> \<exists>x\<in>fst (invalidate_asid a aa). case x of (r, t) \<Rightarrow> (t, t') \<in> state_relation) \<and> \<not> snd (invalidateASID a b) proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma setCurrentPD_to_abs:
  "setCurrentPD = set_current_pd" by (rule ext)
     (clarsimp simp: set_current_pd_def setCurrentPD_def writeTTBR0Ptr_def fromPAddr_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. setCurrentPD = set_current_pd
theory VSpace_R

lemma state_relation_asid_map:
  "(s, s') \<in> state_relation \<Longrightarrow> armKSASIDMap (ksArchState s') = arm_asid_map (arch_state s)" by (simp add: state_relation_def arch_state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> state_relation \<Longrightarrow> armKSASIDMap (ksArchState s') = arm_asid_map (arch_state s)
theory VSpace_R

lemma invalidateTLBByASID_invs'[wp]:
  "\<lbrace>invs'\<rbrace> invalidateTLBByASID param_a \<lbrace>\<lambda>_. invs'\<rbrace>" apply (clarsimp simp: invalidateTLBByASID_def loadHWASID_def
         | wp dmo_invs' no_irq_invalidateLocalTLB_ASID no_irq | wpc)+ apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p"
         in use_valid) apply (clarsimp simp: invalidateLocalTLB_ASID_def machine_op_lift_def
                          machine_rest_lift_def split_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> invalidateTLBByASID param_a \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s x m b p. \<lbrakk>invs' s; (case armKSASIDMap (ksArchState s) param_a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid) = Some x; ((), b) \<in> fst (invalidateLocalTLB_ASID x m); \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal (3 subgoals):
 1. \<And>s x m b p. \<lbrakk>invs' s; (case armKSASIDMap (ksArchState s) param_a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid) = Some x; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> \<lbrace>?P53 s x m b p\<rbrace> invalidateLocalTLB_ASID x \<lbrace>\<lambda>_ m'. underlying_memory m' p = underlying_memory m p\<rbrace>
 2. \<And>s x m b p. \<lbrakk>invs' s; (case armKSASIDMap (ksArchState s) param_a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid) = Some x; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p\<rbrakk> \<Longrightarrow> ?P53 s x m b p m
 3. \<And>s x m b p. \<lbrakk>invs' s; (case armKSASIDMap (ksArchState s) param_a of None \<Rightarrow> None | Some (hw_asid, x) \<Rightarrow> Some hw_asid) = Some x; \<not> pointerInUserData p s; underlying_memory b p \<noteq> underlying_memory m p; underlying_memory b p = underlying_memory m p\<rbrakk> \<Longrightarrow> pointerInDeviceData p s proof (prove)
goal:
No subgoals!
theory VSpace_R

lemma get_asid_pool_corres_inv':
  "corres (\<lambda>p. (\<lambda>p'. p = p' o ucast) \<circ> inv ASIDPool)
          (asid_pool_at p) (pspace_aligned' and pspace_distinct')
          (get_asid_pool p) (getObject p)" apply (rule corres_rel_imp) apply (rule getObject_ASIDPool_corres') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (\<lambda>p. (\<lambda>p'. p = p' \<circ> UCAST(10 \<rightarrow> 32)) \<circ> inv asidpool.ASIDPool) (typ_at (AArch AASIDPool) p) (pspace_aligned' and pspace_distinct') (get_asid_pool p) (getObject p) proof (prove)
goal (2 subgoals):
 1. corres ?r' (typ_at (AArch AASIDPool) p) (pspace_aligned' and pspace_distinct') (get_asid_pool p) (getObject p)
 2. \<And>x y. ?r' x y \<Longrightarrow> ((\<lambda>p'. x = p' \<circ> UCAST(10 \<rightarrow> 32)) \<circ> inv asidpool.ASIDPool) y proof (prove)
goal (1 subgoal):
 1. \<And>x y. x = inv asidpool.ASIDPool y \<circ> UCAST(10 \<rightarrow> 32) \<Longrightarrow> ((\<lambda>p'. x = p' \<circ> UCAST(10 \<rightarrow> 32)) \<circ> inv asidpool.ASIDPool) y proof (prove)
goal:
No subgoals!