kings-crown/FVELER_Isabelle huggingface dataset:
theory Syscall_R

lemma hy_invs':
  "\<lbrace>invs' and ct_active'\<rbrace> handleYield \<lbrace>\<lambda>r. invs' and ct_active'\<rbrace>" apply (simp add: handleYield_def) apply (wp ct_in_state_thread_state_lift'
            rescheduleRequired_all_invs_but_ct_not_inQ
            tcbSchedAppend_invs_but_ct_not_inQ' | simp)+ apply (clarsimp simp add: invs'_def valid_state'_def ct_in_state'_def sch_act_wf_weak cur_tcb'_def
                   valid_pspace_valid_objs' valid_objs'_maxDomain tcb_in_cur_domain'_def
                   ) apply (simp add:ct_active_runnable'[unfolded ct_in_state'_def]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active'\<rbrace> handleYield \<lbrace>\<lambda>r. invs' and ct_active'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active'\<rbrace> do thread <- getCurThread;
y <- tcbSchedDequeue thread;
y <- tcbSchedAppend thread;
rescheduleRequired
od \<lbrace>\<lambda>r. invs' and ct_active'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> ct_active' s \<Longrightarrow> tcb_at' (ksCurThread s) s \<and> st_tcb_at' runnable' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; tcb_at' (ksCurThread s) s; st_tcb_at' active' (ksCurThread s) s\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma getDFSR_invs'[wp]:
  "valid invs' (doMachineOp getDFSR) (\<lambda>_. invs')" by (simp add: getDFSR_def doMachineOp_def split_def select_f_returns | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp getDFSR \<lbrace>\<lambda>_. invs'\<rbrace>
theory Syscall_R

lemma getFAR_invs'[wp]:
  "valid invs' (doMachineOp getFAR) (\<lambda>_. invs')" by (simp add: getFAR_def doMachineOp_def split_def select_f_returns | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp getFAR \<lbrace>\<lambda>_. invs'\<rbrace>
theory Syscall_R

lemma getIFSR_invs'[wp]:
  "valid invs' (doMachineOp getIFSR) (\<lambda>_. invs')" by (simp add: getIFSR_def doMachineOp_def split_def select_f_returns | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> doMachineOp getIFSR \<lbrace>\<lambda>_. invs'\<rbrace>
theory Syscall_R

lemma hv_invs'[wp]: "\<lbrace>invs' and tcb_at' t'\<rbrace> handleVMFault t' vptr \<lbrace>\<lambda>r. invs'\<rbrace>" apply (simp add: ARM_H.handleVMFault_def
             cong: vmfault_type.case_cong) apply (rule hoare_pre) apply (wp | wpcw | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t'\<rbrace> handleVMFault t' vptr \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and tcb_at' t'\<rbrace> case vptr of ARMDataAbort \<Rightarrow> doE addr <- liftE (doMachineOp getFAR);
fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault && mask 14]))
odE | ARMPrefetchAbort \<Rightarrow> doE pc <- liftE (asUser t' getRestartPC);
fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pc [1, fault && mask 14]))
odE \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> case vptr of ARMDataAbort \<Rightarrow> doE addr <- liftE (doMachineOp getFAR);
fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault && mask 14]))
odE | ARMPrefetchAbort \<Rightarrow> doE pc <- liftE (asUser t' getRestartPC);
fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pc [1, fault && mask 14]))
odE \<lbrace>\<lambda>r. invs'\<rbrace>
 2. \<And>s. (invs' and tcb_at' t') s \<Longrightarrow> ?Q4 s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma hv_inv_ex':
  "\<lbrace>P\<rbrace> handleVMFault t vp \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: ARM_H.handleVMFault_def
             cong: vmfault_type.case_cong) apply (rule hoare_pre) apply (wp dmo_inv' getDFSR_inv getFAR_inv getIFSR_inv getRestartPC_inv
             det_getRestartPC asUser_inv
          | wpcw)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> handleVMFault t vp \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case vp of ARMDataAbort \<Rightarrow> doE addr <- liftE (doMachineOp getFAR);
fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault && mask 14]))
odE | ARMPrefetchAbort \<Rightarrow> doE pc <- liftE (asUser t getRestartPC);
fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pc [1, fault && mask 14]))
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4\<rbrace> case vp of ARMDataAbort \<Rightarrow> doE addr <- liftE (doMachineOp getFAR);
fault <- liftE (doMachineOp getDFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault addr [0, fault && mask 14]))
odE | ARMPrefetchAbort \<Rightarrow> doE pc <- liftE (asUser t getRestartPC);
fault <- liftE (doMachineOp getIFSR);
throwError (Fault_H.fault.ArchFault (ARM_H.VMFault pc [1, fault && mask 14]))
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. P s \<Longrightarrow> (P s \<and> True) \<and> P s \<and> True proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma active_from_running':
  "ct_running' s' \<Longrightarrow> ct_active' s'" by (clarsimp elim!: pred_tcb'_weakenE
               simp: ct_in_state'_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_running' s' \<Longrightarrow> ct_active' s'
theory Syscall_R

lemma simple_from_running':
  "ct_running' s' \<Longrightarrow> ct_in_state' simple' s'" by (clarsimp elim!: pred_tcb'_weakenE
               simp: ct_in_state'_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ct_running' s' \<Longrightarrow> ct_in_state' simple' s'
theory Syscall_R

lemma hr_invs'[wp]:
  "\<lbrace>invs' and sch_act_simple\<rbrace> handleReply \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: handleReply_def getSlotCap_def
                   getThreadCallerSlot_map getCurThread_def) apply (wp getCTE_wp | wpc | simp)+ apply (clarsimp simp: cte_wp_at_ctes_of) apply (drule ctes_of_valid', clarsimp+) apply (simp add: valid_cap'_def) apply (simp add: invs'_def cur_tcb'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple\<rbrace> handleReply \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple\<rbrace> do thread <- gets ksCurThread;
cte <- getCTE (cte_map (thread, tcb_cnode_index 3));
case cteCap cte of capability.NullCap \<Rightarrow> return () | capability.ReplyCap caller True canGrant \<Rightarrow> haskell_fail [] | capability.ReplyCap caller False canGrant \<Rightarrow> do haskell_assert (caller \<noteq> thread) [];
doReplyTransfer thread caller (cte_map (thread, tcb_cnode_index 3)) canGrant
od | _ \<Rightarrow> haskell_fail []
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> sch_act_simple s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) (cte_map (ksCurThread s, tcb_cnode_index 3)) s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) (cte_map (ksCurThread s, tcb_cnode_index 3)) s \<and> (\<forall>x xa. (\<exists>xb. cteCap cte = capability.ReplyCap x xa xb) \<longrightarrow> \<not> xa \<longrightarrow> tcb_at' x s \<and> tcb_at' (ksCurThread s) s \<and> cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap x False grant) (cte_map (ksCurThread s, tcb_cnode_index 3)) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x xa xb. \<lbrakk>invs' s; sch_act_simple s; ctes_of s (cte_map (ksCurThread s, tcb_cnode_index 3)) = Some cte; cteCap cte = capability.ReplyCap x False xb; \<not> xa\<rbrakk> \<Longrightarrow> tcb_at' x s \<and> tcb_at' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte x xa xb. \<lbrakk>invs' s; sch_act_simple s; cteCap cte = capability.ReplyCap x False xb; \<not> xa; valid_cap' (capability.ReplyCap x False xb) s\<rbrakk> \<Longrightarrow> tcb_at' x s \<and> tcb_at' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte x xa xb. \<lbrakk>invs' s; sch_act_simple s; cteCap cte = capability.ReplyCap x False xb; \<not> xa; capAligned (capability.ReplyCap x False xb) \<and> tcb_at' x s\<rbrakk> \<Longrightarrow> tcb_at' (ksCurThread s) s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma doReplyTransfer_st_tcb_at_active:
  "\<lbrace>st_tcb_at' active' t and tcb_at' t' and K (t \<noteq> t') and
    cte_wp_at' (\<lambda>cte. cteCap cte = (capability.ReplyCap t' False g)) sl\<rbrace>
    doReplyTransfer t t' sl g
   \<lbrace>\<lambda>rv. st_tcb_at' active' t\<rbrace>" apply (simp add: doReplyTransfer_def liftM_def) apply (wp setThreadState_st_tcb sts_pred_tcb_neq' cteDeleteOne_reply_pred_tcb_at
            hoare_drop_imps threadSet_pred_tcb_no_state hoare_exI
            doIPCTransfer_non_null_cte_wp_at2' | wpc | clarsimp simp:isCap_simps)+ apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' active' t and tcb_at' t' and K (t \<noteq> t') and cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False g) sl\<rbrace> doReplyTransfer t t' sl g \<lbrace>\<lambda>rv. st_tcb_at' active' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at' active' t and tcb_at' t' and (\<lambda>y. t \<noteq> t') and cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False g) sl\<rbrace> do state <- getThreadState t';
y <- assert (isReply state);
x <- getCTE sl;
y <- assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer);
parentCap <- getSlotCap (mdbPrev (cteMDBNode x));
y <- assert (isReplyCap parentCap \<and> capReplyMaster parentCap);
threadGet tcbFault t' >>= case_option (do y <- doIPCTransfer t None 0 g t';
y <- cteDeleteOne sl;
y <- setThreadState Structures_H.thread_state.Running t';
possibleSwitchTo t'
od) (\<lambda>f. do y <- cteDeleteOne sl;
tag <- getMessageInfo t;
sendBuffer <- lookupIPCBuffer False t;
mrs <- getMRs t sendBuffer tag;
restart <- handleFaultReply f t' (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t';
if restart then do y <- setThreadState Structures_H.thread_state.Restart t';
possibleSwitchTo t'
od else setThreadState Structures_H.thread_state.Inactive t'
od)
od \<lbrace>\<lambda>rv. st_tcb_at' active' t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at' active' t s; tcb_at' t' s; t \<noteq> t'; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False g) sl s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap (?t'174 () () ()) False (?r172 () () ())) sl s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) sl s) proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma handleCall_corres:
  "corres (dc \<oplus> dc) (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
              (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
                (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
                ct_active')
         handle_call handleCall" by (simp add: handle_call_def handleCall_def liftE_bindE handleInvocation_corres)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active) (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') handle_call handleCall
theory Syscall_R

lemma hc_invs'[wp]:
  "\<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
      (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
      ct_active'\<rbrace>
     handleCall
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: handleCall_def) apply (wp) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active'\<rbrace> handleCall \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active'\<rbrace> handleInvocation True True \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active') s \<Longrightarrow> (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma cteInsert_sane[wp]:
  "\<lbrace>sch_act_sane\<rbrace> cteInsert newCap srcSlot destSlot \<lbrace>\<lambda>_. sch_act_sane\<rbrace>" apply (simp add: sch_act_sane_def) apply (wp hoare_vcg_all_lift
            hoare_convert_imp [OF cteInsert_nosch cteInsert_ct]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>sch_act_sane\<rbrace> cteInsert newCap srcSlot destSlot \<lbrace>\<lambda>_. 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> cteInsert newCap srcSlot destSlot \<lbrace>\<lambda>_ s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<noteq> ksCurThread s\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma possibleSwitchTo_sane:
  "\<lbrace>\<lambda>s. sch_act_sane s \<and> t \<noteq> ksCurThread s\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>_. sch_act_sane\<rbrace>" apply (simp add: possibleSwitchTo_def setSchedulerAction_def curDomain_def
              cong: if_cong) apply (wp hoare_drop_imps | wpc)+ apply (simp add: sch_act_sane_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_sane s \<and> t \<noteq> ksCurThread s\<rbrace> possibleSwitchTo t \<lbrace>\<lambda>_. sch_act_sane\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_sane s \<and> t \<noteq> ksCurThread s\<rbrace> do curDom <- gets ksCurDomain;
targetDom <- threadGet tcbDomain t;
action <- getSchedulerAction;
if targetDom \<noteq> curDom then tcbSchedEnqueue t else if action \<noteq> ResumeCurrentThread then do y <- rescheduleRequired;
tcbSchedEnqueue t
od else modify (ksSchedulerAction_update (\<lambda>_. SwitchToThread t))
od \<lbrace>\<lambda>_. sch_act_sane\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. sch_act_sane s \<and> t \<noteq> ksCurThread s \<Longrightarrow> sch_act_sane s \<and> True \<and> sch_act_sane (s\<lparr>ksSchedulerAction := SwitchToThread t\<rparr>) proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma doReplyTransfer_sane:
  "\<lbrace>\<lambda>s. sch_act_sane s \<and> t' \<noteq> ksCurThread s\<rbrace>
  doReplyTransfer t t' callerSlot g \<lbrace>\<lambda>rv. sch_act_sane\<rbrace>" apply (simp add: doReplyTransfer_def liftM_def) apply (wp possibleSwitchTo_sane hoare_drop_imps hoare_vcg_all_lift|wpc)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_sane s \<and> t' \<noteq> ksCurThread s\<rbrace> doReplyTransfer t t' callerSlot g \<lbrace>\<lambda>rv. sch_act_sane\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. sch_act_sane s \<and> t' \<noteq> ksCurThread s\<rbrace> do state <- getThreadState t';
y <- assert (isReply state);
x <- getCTE callerSlot;
y <- assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer);
parentCap <- getSlotCap (mdbPrev (cteMDBNode x));
y <- assert (isReplyCap parentCap \<and> capReplyMaster parentCap);
threadGet tcbFault t' >>= case_option (do y <- doIPCTransfer t None 0 g t';
y <- cteDeleteOne callerSlot;
y <- setThreadState Structures_H.thread_state.Running t';
possibleSwitchTo t'
od) (\<lambda>f. do y <- cteDeleteOne callerSlot;
tag <- getMessageInfo t;
sendBuffer <- lookupIPCBuffer False t;
mrs <- getMRs t sendBuffer tag;
restart <- handleFaultReply f t' (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t';
if restart then do y <- setThreadState Structures_H.thread_state.Restart t';
possibleSwitchTo t'
od else setThreadState Structures_H.thread_state.Inactive t'
od)
od \<lbrace>\<lambda>rv. sch_act_sane\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. sch_act_sane s \<and> t' \<noteq> ksCurThread s \<Longrightarrow> (sch_act_sane s \<and> t' \<noteq> ksCurThread s) \<and> (\<forall>x. sch_act_sane s \<and> t' \<noteq> ksCurThread s \<and> sch_act_sane s) proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma handleReply_nonz_cap_to_ct:
  "\<lbrace>ct_active' and invs' and sch_act_simple\<rbrace>
     handleReply
   \<lbrace>\<lambda>rv s. ex_nonz_cap_to' (ksCurThread s) s\<rbrace>" apply (rule_tac Q="\<lambda>rv. ct_active' and invs'"
               in hoare_post_imp) apply (auto simp: ct_in_state'_def elim: st_tcb_ex_cap'')[1] apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active' and invs' and sch_act_simple\<rbrace> handleReply \<lbrace>\<lambda>rv s. ex_nonz_cap_to' (ksCurThread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (ct_active' and invs') s \<Longrightarrow> ex_nonz_cap_to' (ksCurThread s) s
 2. \<lbrace>ct_active' and invs' and sch_act_simple\<rbrace> handleReply \<lbrace>\<lambda>rv. ct_active' and invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ct_active' and invs' and sch_act_simple\<rbrace> handleReply \<lbrace>\<lambda>rv. ct_active' and invs'\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma handleHypervisorFault_corres:
  "corres dc (einvs and  st_tcb_at active thread and ex_nonz_cap_to thread
                   and (%_. valid_fault f))
             (invs' and sch_act_not thread
                    and (\<lambda>s. \<forall>p. thread \<notin> set(ksReadyQueues s p))
                    and st_tcb_at' simple' thread and ex_nonz_cap_to' thread)
          (handle_hypervisor_fault w fault)
          (handleHypervisorFault w fault)" apply (cases fault; clarsimp simp add: handleHypervisorFault_def returnOk_def2) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (einvs and st_tcb_at active thread and ex_nonz_cap_to thread and (\<lambda>_. valid_fault f)) (invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread) (handle_hypervisor_fault w fault) (handleHypervisorFault w fault) proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma hv_inv':
  "\<lbrace>P\<rbrace> handleVMFault p t \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: ARM_H.handleVMFault_def) apply (rule hoare_pre) apply (wp dmo_inv' getDFSR_inv getFAR_inv getIFSR_inv getRestartPC_inv
             det_getRestartPC asUser_inv
          |wpc|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> handleVMFault p t \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case t of ARMDataAbort \<Rightarrow> doE addr <- withoutFailure $ doMachineOp getFAR;
fault <- withoutFailure $ doMachineOp getDFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault addr [0, fault && mask 14]
odE | ARMPrefetchAbort \<Rightarrow> doE pc <- withoutFailure $ asUser p $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> case t of ARMDataAbort \<Rightarrow> doE addr <- withoutFailure $ doMachineOp getFAR;
fault <- withoutFailure $ doMachineOp getDFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault addr [0, fault && mask 14]
odE | ARMPrefetchAbort \<Rightarrow> doE pc <- withoutFailure $ asUser p $ getRestartPC;
fault <- withoutFailure $ doMachineOp getIFSR;
throw $ Fault_H.fault.ArchFault $ ARM_H.VMFault (VPtr pc) [1, fault && mask 14]
odE \<lbrace>\<lambda>_. P\<rbrace>
 2. \<And>s. P s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma hh_inv':
  "\<lbrace>P\<rbrace> handleHypervisorFault p t \<lbrace>\<lambda>_. P\<rbrace>" apply (simp add: ARM_H.handleHypervisorFault_def) apply (cases t; clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> handleHypervisorFault p t \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> case t of ARMNoHypFaults \<Rightarrow> return () \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal:
No subgoals!
theory Syscall_R

lemma ct_not_idle':
  fixes s
  assumes vi:  "valid_idle' s"
      and cts: "ct_in_state' (\<lambda>tcb. \<not>idle' tcb) s"
  shows "ksCurThread s \<noteq> ksIdleThread s" proof assume "ksCurThread s = ksIdleThread s" with vi have "ct_in_state' idle' s" unfolding ct_in_state'_def valid_idle'_def by (clarsimp simp: pred_tcb_at'_def obj_at'_def idle_tcb'_def) with cts show False unfolding ct_in_state'_def by (fastforce dest: pred_tcb_at_conj') qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ksCurThread s \<noteq> ksIdleThread s proof (state)
goal (1 subgoal):
 1. ksCurThread s = ksIdleThread s \<Longrightarrow> False proof (state)
this:
ksCurThread s = ksIdleThread s

goal (1 subgoal):
 1. ksCurThread s = ksIdleThread s \<Longrightarrow> False proof (chain)
picking this:
valid_idle' s
ksCurThread s = ksIdleThread s proof (prove)
using this:
valid_idle' s
ksCurThread s = ksIdleThread s

goal (1 subgoal):
 1. ct_idle' s proof (prove)
using this:
obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s
ksCurThread s = ksIdleThread s

goal (1 subgoal):
 1. st_tcb_at' idle' (ksCurThread s) s proof (state)
this:
ct_idle' s

goal (1 subgoal):
 1. ksCurThread s = ksIdleThread s \<Longrightarrow> False proof (chain)
picking this:
ct_in_state' (\<lambda>tcb. tcb \<noteq> Structures_H.thread_state.IdleThreadState) s
ct_idle' s proof (prove)
using this:
ct_in_state' (\<lambda>tcb. tcb \<noteq> Structures_H.thread_state.IdleThreadState) s
ct_idle' s

goal (1 subgoal):
 1. False proof (prove)
using this:
st_tcb_at' (\<lambda>tcb. tcb \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s
st_tcb_at' idle' (ksCurThread s) s

goal (1 subgoal):
 1. False proof (state)
this:
False

goal:
No subgoals!