kings-crown/FVELER_Isabelle huggingface dataset:
theory Refine

lemma do_user_op_valid_sched:"\<lbrace>valid_sched\<rbrace> do_user_op f tc \<lbrace>\<lambda>_. valid_sched\<rbrace>" unfolding do_user_op_def apply (wp | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do_user_op f tc \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_sched\<rbrace> do t <- gets cur_thread;
conv <- gets (ptable_lift t);
rights <- gets (ptable_rights t);
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
(e, tc', um', ds') <- select (fst (f t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va})));
do_machine_op (user_memory_update ((um' |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)));
do_machine_op (device_memory_update ((ds' |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds));
return (e, tc')
od \<lbrace>\<lambda>_. valid_sched\<rbrace> proof (prove)
goal:
No subgoals!
theory Refine

lemma do_user_op_sched_act:
  "\<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do_user_op f tc \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace>" unfolding do_user_op_def apply (wp | simp add: split_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do_user_op f tc \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace> do t <- gets cur_thread;
conv <- gets (ptable_lift t);
rights <- gets (ptable_rights t);
um <- gets (\<lambda>s. user_mem s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> machine_state);
(e, tc', um', ds') <- select (fst (f t (conv |` {pa. rights pa \<noteq> {}}) rights (tc, um |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. conv va = Some pa \<and> AllowRead \<in> rights va})));
do_machine_op (user_memory_update ((um' |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` (- dom ds)));
do_machine_op (device_memory_update ((ds' |` {pa. \<exists>va. conv va = Some pa \<and> AllowWrite \<in> rights va} \<circ> addrFromPPtr) |` dom ds));
return (e, tc')
od \<lbrace>\<lambda>_ s. P (scheduler_action s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Refine

lemma do_user_op_invs2:
  "\<lbrace>einvs  and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread)
    and (\<lambda>s. 0 < domain_time s) and valid_domain_list \<rbrace>
  do_user_op f tc
   \<lbrace>\<lambda>_. (einvs  and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread))
        and (\<lambda>s. 0 < domain_time s) and valid_domain_list \<rbrace>" apply (rule_tac Q="\<lambda>_. valid_list and valid_sched and
   (\<lambda>s. scheduler_action s = resume_cur_thread) and (invs and ct_running) and
   (\<lambda>s. 0 < domain_time s) and valid_domain_list"
   in hoare_strengthen_post) apply (wp do_user_op_valid_list do_user_op_valid_sched do_user_op_sched_act
    do_user_op_invs | simp | force)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list\<rbrace> do_user_op f tc \<lbrace>\<lambda>_. einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list\<rbrace> do_user_op f tc \<lbrace>\<lambda>_. valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (invs and ct_running) and (\<lambda>s. 0 < domain_time s) and valid_domain_list\<rbrace>
 2. \<And>rv s. (valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (invs and ct_running) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> (einvs and ct_running and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s proof (prove)
goal:
No subgoals!
theory Refine

lemma valid_list_init[simp]:
  "valid_list init_A_st" by (simp add: valid_list_2_def init_A_st_def ext_init_def init_cdt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_list init_A_st
theory Refine

lemma valid_sched_init[simp]:
  "valid_sched init_A_st" apply (simp add: valid_sched_def init_A_st_def ext_init_def) apply (clarsimp simp: valid_etcbs_def init_kheap_def st_tcb_at_kh_def obj_at_kh_def
                    obj_at_def is_etcb_at_def idle_thread_ptr_def init_globals_frame_def
                    init_global_pd_def valid_queues_2_def ct_not_in_q_def not_queued_def
                    valid_sched_action_def is_activatable_def
                    ct_in_cur_domain_2_def valid_blocked_2_def valid_idle_etcb_def etcb_at'_def default_etcb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_sched init_A_st proof (prove)
goal (1 subgoal):
 1. valid_etcbs_2 [idle_thread_ptr \<mapsto> default_etcb] init_kheap \<and> valid_queues_2 (const (const [])) [idle_thread_ptr \<mapsto> default_etcb] init_kheap \<and> ct_not_in_q_2 (const (const [])) resume_cur_thread idle_thread_ptr \<and> valid_sched_action_2 resume_cur_thread [idle_thread_ptr \<mapsto> default_etcb] init_kheap idle_thread_ptr 0 \<and> ct_in_cur_domain_2 idle_thread_ptr idle_thread_ptr resume_cur_thread 0 [idle_thread_ptr \<mapsto> default_etcb] \<and> valid_blocked_2 (const (const [])) init_kheap resume_cur_thread idle_thread_ptr \<and> valid_idle_etcb_2 [idle_thread_ptr \<mapsto> default_etcb] proof (prove)
goal:
No subgoals!
theory Refine

lemma valid_domain_list_init[simp]:
  "valid_domain_list init_A_st" by (simp add: init_A_st_def ext_init_def valid_domain_list_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_domain_list init_A_st
theory Refine

lemma ckernel_invs:
  "\<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
               (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and
               (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>
  callKernel e
  \<lbrace>\<lambda>rs. (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
    and (invs' and (ct_running' or ct_idle'))\<rbrace>" apply (simp add: callKernel_def) apply (rule hoare_pre) apply (wp activate_invs' activate_sch_act schedule_sch
             schedule_sch_act_simple he_invs' schedule_invs'
             hoare_drop_imp[where R="\<lambda>_. kernelExitAssertions"]
          | simp add: no_irq_getActiveIRQ)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> callKernel e \<lbrace>\<lambda>rs. (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle'))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> do y <- stateAssert fastpathKernelAssertions [];
y <- handleEvent e <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od));
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od \<lbrace>\<lambda>rs. (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle'))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- stateAssert fastpathKernelAssertions [];
y <- handleEvent e <handle> (\<lambda>_. liftE (do irq <- doMachineOp (getActiveIRQ True);
when (\<exists>y. irq = Some y) (handleInterrupt (the irq))
od));
y <- ThreadDecls_H.schedule;
y <- activateThread;
stateAssert kernelExitAssertions []
od \<lbrace>\<lambda>rs. (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle'))\<rbrace>
 2. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Refine

lemma fastpathKernelAssertions_cross:
  "\<lbrakk> (s,s') \<in> state_relation; invs s; valid_arch_state' s'\<rbrakk> \<Longrightarrow> fastpathKernelAssertions s'" unfolding fastpathKernelAssertions_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; invs s; valid_arch_state' s'\<rbrakk> \<Longrightarrow> fastpathKernelAssertions s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; invs s; valid_arch_state' s'\<rbrakk> \<Longrightarrow> True
theory Refine

lemma corres_cross_over_fastpathKernelAssertions:
  "\<lbrakk> \<And>s. P s \<Longrightarrow> invs s; \<And>s'. Q s' \<Longrightarrow> invs' s';
     corres r P (Q and fastpathKernelAssertions) f g \<rbrakk> \<Longrightarrow>
   corres r P Q f g" by (rule corres_cross_over_guard[where Q="Q and fastpathKernelAssertions"])
     (fastforce elim: fastpathKernelAssertions_cross)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s. P s \<Longrightarrow> invs s; \<And>s'. Q s' \<Longrightarrow> invs' s'; corres r P (Q and fastpathKernelAssertions) f g\<rbrakk> \<Longrightarrow> corres r P Q f g
theory Refine

lemma callKernel_domain_time_left:
  "\<lbrace> \<top> \<rbrace> callKernel e \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s \<rbrace>" unfolding callKernel_def kernelExitAssertions_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> callKernel e \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do stateAssert fastpathKernelAssertions [];
runExceptT $ handleEvent e `~catchError~` (\<lambda>_. withoutPreemption $ do irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
ThreadDecls_H.schedule;
activateThread;
stateAssert (\<lambda>s. 0 < ksDomainTime s \<and> valid_domain_list' s) []
od \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s\<rbrace>
theory Refine

lemma kernelEntry_invs':
  "\<lbrace> invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and
           (ct_running' or ct_idle') and
           (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
           (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
           (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' \<rbrace>
  kernelEntry e tc
  \<lbrace>\<lambda>rs. (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
         (invs' and (ct_running' or ct_idle')) and
         (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
         (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' \<rbrace>" apply (simp add: kernelEntry_def) apply (wp ckernel_invs callKernel_valid_duplicates' callKernel_domain_time_left
            threadSet_invs_trivial threadSet_ct_running'
            TcbAcc_R.dmo_invs' hoare_weak_lift_imp
            callKernel_domain_time_left
         | clarsimp simp: user_memory_update_def no_irq_def tcb_at_invs'
                          valid_domain_list'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace> kernelEntry e tc \<lbrace>\<lambda>rs. (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle')) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace> do t <- getCurThread;
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet tc (tcbArch tcb)) tcb) t;
y <- callKernel e;
getCurThread >>= threadGet (atcbContextGet \<circ> tcbArch)
od \<lbrace>\<lambda>rs. (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (invs' and (ct_running' or ct_idle')) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace> proof (prove)
goal:
No subgoals!
theory Refine

lemma ptable_lift_abs_state[simp]:
  "ptable_lift t (abs_state s) = ptable_lift t s" by (simp add: ptable_lift_def abs_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptable_lift t (abs_state s) = ptable_lift t s
theory Refine

lemma ptable_rights_abs_state[simp]:
  "ptable_rights t (abs_state s) = ptable_rights t s" by (simp add: ptable_rights_def abs_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptable_rights t (abs_state s) = ptable_rights t s
theory Refine

lemma ptable_rights_imp_UserData:
  assumes invs: "einvs s" and invs': "invs' s'"
  assumes rel: "(s,s') : state_relation"
  assumes rights: "ptable_rights t (absKState s') x \<noteq> {}"
  assumes trans:
    "ptable_lift t (absKState s') x = Some (ARM.addrFromPPtr y)"
  shows "pointerInUserData y s' \<or> pointerInDeviceData y s'" proof - from invs invs' rel have [simp]: "absKState s' = abs_state s" by - (rule absKState_correct', simp_all) from invs have valid: "valid_state s" by auto from invs' have valid': "valid_state' s'" by auto have "in_user_frame y s \<or> in_device_frame y s " by (rule ptable_rights_imp_frame[OF valid rights[simplified]
                                             trans[simplified]]) thus ?thesis by (auto simp add: pointerInUserData_relation[OF rel valid' valid]
     pointerInDeviceData_relation[OF rel valid' valid]) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pointerInUserData y s' \<or> pointerInDeviceData y s' proof (state)
goal (1 subgoal):
 1. pointerInUserData y s' \<or> pointerInDeviceData y s' proof (chain)
picking this:
einvs s
invs' s'
(s, s') \<in> state_relation proof (prove)
using this:
einvs s
invs' s'
(s, s') \<in> state_relation

goal (1 subgoal):
 1. absKState s' = abs_state s proof (state)
this:
absKState s' = abs_state s

goal (1 subgoal):
 1. pointerInUserData y s' \<or> pointerInDeviceData y s' proof (chain)
picking this:
einvs s proof (prove)
using this:
einvs s

goal (1 subgoal):
 1. valid_state s proof (state)
this:
valid_state s

goal (1 subgoal):
 1. pointerInUserData y s' \<or> pointerInDeviceData y s' proof (chain)
picking this:
invs' s' proof (prove)
using this:
invs' s'

goal (1 subgoal):
 1. valid_state' s' proof (state)
this:
valid_state' s'

goal (1 subgoal):
 1. pointerInUserData y s' \<or> pointerInDeviceData y s' proof (prove)
goal (1 subgoal):
 1. in_user_frame y s \<or> in_device_frame y s proof (state)
this:
in_user_frame y s \<or> in_device_frame y s

goal (1 subgoal):
 1. pointerInUserData y s' \<or> pointerInDeviceData y s' proof (prove)
using this:
in_user_frame y s \<or> in_device_frame y s

goal (1 subgoal):
 1. pointerInUserData y s' \<or> pointerInDeviceData y s' proof (state)
this:
pointerInUserData y s' \<or> pointerInDeviceData y s'

goal:
No subgoals!
theory Refine

lemma device_update_invs':
  "\<lbrace>invs'\<rbrace>doMachineOp (device_memory_update ds)
   \<lbrace>\<lambda>_. invs'\<rbrace>" apply (simp add: doMachineOp_def device_memory_update_def simpler_modify_def select_f_def
                    gets_def get_def bind_def valid_def return_def) by (clarsimp simp: invs'_def valid_state'_def valid_irq_states'_def valid_machine_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp (device_memory_update ds) \<lbrace>\<lambda>_. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. invs' s \<longrightarrow> invs' (s\<lparr>ksMachineState := ksMachineState s\<lparr>device_state := device_state (ksMachineState s) ++ ds\<rparr>\<rparr>)
theory Refine

lemma doUserOp_valid_duplicates':
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
   doUserOp f tc
   \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add: doUserOp_def split_def) apply (wp dmo_invs') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> doUserOp f tc \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> do t <- getCurThread;
trans <- gets (ptable_lift t \<circ> absKState);
perms <- gets (ptable_rights t \<circ> absKState);
um <- gets (\<lambda>s. user_mem' s \<circ> ptrFromPAddr);
dm <- gets (\<lambda>s. device_mem' s \<circ> ptrFromPAddr);
ds <- gets (device_state \<circ> ksMachineState);
y <- assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds);
y <- assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds);
p <- select (fst (f t (trans |` {pa. perms pa \<noteq> {}}) perms (tc, um |` {pa. \<exists>va. trans va = Some pa \<and> AllowRead \<in> perms va}, (ds \<circ> ptrFromPAddr) |` {pa. \<exists>va. trans va = Some pa \<and> AllowRead \<in> perms va})));
y <- doMachineOp (user_memory_update ((fst (snd (snd p)) |` {pa. \<exists>va. trans va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` (- dom ds)));
y <- doMachineOp (device_memory_update ((snd (snd (snd p)) |` {pa. \<exists>va. trans va = Some pa \<and> AllowWrite \<in> perms va} \<circ> addrFromPPtr) |` dom ds));
return (fst p, fst (snd p))
od \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> dom (user_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> - dom ((device_state \<circ> ksMachineState) s) \<longrightarrow> dom (device_mem' s \<circ> ptrFromPAddr \<circ> addrFromPPtr) \<subseteq> dom ((device_state \<circ> ksMachineState) s) \<longrightarrow> (\<forall>x\<in>fst (f (ksCurThread s) ((ptable_lift (ksCurThread s) \<circ> absKState) s |` {pa. (ptable_rights (ksCurThread s) \<circ> absKState) s pa \<noteq> {}}) ((ptable_rights (ksCurThread s) \<circ> absKState) s) (tc, (user_mem' s \<circ> ptrFromPAddr) |` {pa. \<exists>va. (ptable_lift (ksCurThread s) \<circ> absKState) s va = Some pa \<and> AllowRead \<in> (ptable_rights (ksCurThread s) \<circ> absKState) s va}, ((device_state \<circ> ksMachineState) s \<circ> ptrFromPAddr) |` {pa. \<exists>va. (ptable_lift (ksCurThread s) \<circ> absKState) s va = Some pa \<and> AllowRead \<in> (ptable_rights (ksCurThread s) \<circ> absKState) s va})). vs_valid_duplicates' (ksPSpace s)) proof (prove)
goal:
No subgoals!
theory Refine

lemma user_mem_corres:
  "corres (=) invs invs' (gets (\<lambda>x. g (user_mem x))) (gets (\<lambda>x. g (user_mem' x)))" by (clarsimp simp add: gets_def get_def return_def bind_def
                         invs_def invs'_def
                         corres_underlying_def user_mem_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) invs invs' (gets (\<lambda>x. g (user_mem x))) (gets (\<lambda>x. g (user_mem' x)))
theory Refine

lemma device_mem_corres:
  "corres (=) invs invs' (gets (\<lambda>x. g (device_mem x))) (gets (\<lambda>x. g (device_mem' x)))" by (clarsimp simp add: gets_def get_def return_def bind_def
                         invs_def invs'_def
                         corres_underlying_def device_mem_relation)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) invs invs' (gets (\<lambda>x. g (device_mem x))) (gets (\<lambda>x. g (device_mem' x)))
theory Refine

lemma corres_gets_machine_state:
  "corres (=) \<top> \<top> (gets (f \<circ> machine_state)) (gets (f \<circ> ksMachineState))" by (clarsimp simp: gets_def corres_underlying_def
                     in_monad bind_def get_def return_def state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (gets (f \<circ> machine_state)) (gets (f \<circ> ksMachineState))
theory Refine

lemma ct_running_related:
  "\<lbrakk> (a, c) \<in> state_relation; ct_running' c \<rbrakk>
     \<Longrightarrow> ct_running a" apply (clarsimp simp: ct_in_state_def ct_in_state'_def
                        curthread_relation) apply (frule(1) st_tcb_at_coerce_abstract) apply (erule st_tcb_weakenE) apply (case_tac st, simp_all)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; ct_running' c\<rbrakk> \<Longrightarrow> ct_running a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (cur_thread a) c\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. st = Structures_A.thread_state.Running) (cur_thread a) a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (cur_thread a) c; st_tcb_at (\<lambda>st. \<exists>st'. thread_state_relation st st' \<and> st' = Structures_H.thread_state.Running) (cur_thread a) a\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>st. st = Structures_A.thread_state.Running) (cur_thread a) a proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>(a, c) \<in> state_relation; st_tcb_at' (\<lambda>st. st = Structures_H.thread_state.Running) (cur_thread a) c; \<exists>st'. thread_state_relation st st' \<and> st' = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> st = Structures_A.thread_state.Running proof (prove)
goal:
No subgoals!
theory Refine

lemma ct_idle_related:
  "\<lbrakk> (a, c) \<in> state_relation; ct_idle' c \<rbrakk>
     \<Longrightarrow> ct_idle a" apply (clarsimp simp: ct_in_state_def ct_in_state'_def
                        curthread_relation) apply (frule(1) st_tcb_at_coerce_abstract) apply (erule st_tcb_weakenE) apply (case_tac st, simp_all)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; ct_idle' c\<rbrakk> \<Longrightarrow> ct_idle a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; st_tcb_at' idle' (cur_thread a) c\<rbrakk> \<Longrightarrow> st_tcb_at idle (cur_thread a) a proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; st_tcb_at' idle' (cur_thread a) c; st_tcb_at (\<lambda>st. \<exists>st'. thread_state_relation st st' \<and> idle' st') (cur_thread a) a\<rbrakk> \<Longrightarrow> st_tcb_at idle (cur_thread a) a proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>(a, c) \<in> state_relation; st_tcb_at' idle' (cur_thread a) c; \<exists>st'. thread_state_relation st st' \<and> idle' st'\<rbrakk> \<Longrightarrow> idle st proof (prove)
goal:
No subgoals!