kings-crown/FVELER_Isabelle huggingface dataset:
theory Refine

lemma checkActiveIRQ_valid_duplicates':
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
   checkActiveIRQ
   \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add: checkActiveIRQ_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> checkActiveIRQ \<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 irq <- doMachineOp (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal:
No subgoals!
theory Refine

lemma check_active_irq_corres':
  "corres (=) \<top> \<top> (check_active_irq) (checkActiveIRQ)" apply (simp add: check_active_irq_def checkActiveIRQ_def) apply (rule corres_guard_imp) apply (rule corres_split[OF corres_machine_op[OF corres_underlying_trivial], where R="\<lambda>_. \<top>" and R'="\<lambda>_. \<top>"]) apply simp apply (rule no_fail_getActiveIRQ) apply (wp | simp )+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) check_active_irq checkActiveIRQ proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>_. True) (\<lambda>_. True) (do irq <- do_machine_op (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od) (do irq <- doMachineOp (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (do irq <- do_machine_op (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od) (do irq <- doMachineOp (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od)
 2. \<And>s. True \<Longrightarrow> ?Q s
 3. \<And>s. True \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. True \<Longrightarrow> no_fail ?Q5 (getActiveIRQ False)
 2. \<And>irq irqa. irq = irqa \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>_. True) (return (\<exists>y. irq = Some y)) (return (\<exists>y. irqa = Some y))
 3. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q4) s
 6. \<And>s. True \<Longrightarrow> (?Q5 \<circ> ksMachineState and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. no_fail ?Q5 (getActiveIRQ False)
 2. \<And>irq irqa. irq = irqa \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>_. True) (return (\<exists>y. irq = Some y)) (return (\<exists>y. irqa = Some y))
 3. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q4) s
 6. \<And>s. True \<Longrightarrow> (?Q5 \<circ> ksMachineState and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>irq irqa. irq = irqa \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>_. True) (return (\<exists>y. irq = Some y)) (return (\<exists>y. irqa = Some y))
 2. \<lbrace>?Q4\<rbrace> do_machine_op (getActiveIRQ False) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> doMachineOp (getActiveIRQ False) \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) \<circ> machine_state and ?Q4) s
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) \<circ> ksMachineState and ?Q'4) s proof (prove)
goal:
No subgoals!
theory Refine

lemma check_active_irq_corres:
  "corres (=)
    (invs and (ct_running or ct_idle) and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)
     and (\<lambda>s. 0 < domain_time s) and valid_domain_list)
    (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
      and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle')
      and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
    (check_active_irq) (checkActiveIRQ)" apply (rule corres_guard_imp) apply (rule check_active_irq_corres', auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (invs and (ct_running or ct_idle) and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) check_active_irq checkActiveIRQ proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' check_active_irq checkActiveIRQ
 2. \<And>s. (invs and (ct_running or ct_idle) and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (ct_running' or ct_idle') and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) s \<Longrightarrow> ?Q' s proof (prove)
goal:
No subgoals!
theory Refine

lemma checkActiveIRQ_just_running_corres:
  "corres (=)
    (invs and ct_running and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)
      and (\<lambda>s. 0 < domain_time s) and valid_domain_list)
    (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))
      and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'
      and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
    (check_active_irq) (checkActiveIRQ)" apply (rule corres_guard_imp) apply (rule check_active_irq_corres', auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (invs and ct_running and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) check_active_irq checkActiveIRQ proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' check_active_irq checkActiveIRQ
 2. \<And>s. (invs and ct_running and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and ct_running' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q' s proof (prove)
goal:
No subgoals!
theory Refine

lemma checkActiveIRQ_just_idle_corres:
  "corres (=)
    (invs and ct_idle and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread)
      and (\<lambda>s. 0 < domain_time s)  and valid_domain_list)
    (invs' and ct_idle' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))
      and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'
      and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
    (check_active_irq) (checkActiveIRQ)" apply (rule corres_guard_imp) apply (rule check_active_irq_corres', auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (invs and ct_idle and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) (invs' and ct_idle' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) check_active_irq checkActiveIRQ proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' check_active_irq checkActiveIRQ
 2. \<And>s. (invs and ct_idle and einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and ct_idle' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q' s proof (prove)
goal:
No subgoals!
theory Refine

lemma checkActiveIRQ_invs':
  "\<lbrace>invs' and ex_abs invs and (ct_running' or ct_idle')
    and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>
   checkActiveIRQ
   \<lbrace>\<lambda>_. invs' and (ct_running' or ct_idle')
    and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>" apply (simp add: checkActiveIRQ_def ex_abs_def) apply (wp dmo_invs' | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_abs invs and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> checkActiveIRQ \<lbrace>\<lambda>_. invs' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and (\<lambda>s'. \<exists>s. (s, s') \<in> state_relation \<and> invs s) and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> do irq <- doMachineOp (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od \<lbrace>\<lambda>_. invs' and (ct_running' or ct_idle') and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> proof (prove)
goal:
No subgoals!
theory Refine

lemma checkActiveIRQ_invs'_just_running:
  "\<lbrace>invs' and ex_abs invs and ct_running'
    and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>
   checkActiveIRQ
   \<lbrace>\<lambda>_. invs' and ct_running'
    and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>" apply (simp add: checkActiveIRQ_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_abs invs and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> checkActiveIRQ \<lbrace>\<lambda>_. invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_abs invs and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> do irq <- doMachineOp (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od \<lbrace>\<lambda>_. invs' and ct_running' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> proof (prove)
goal:
No subgoals!
theory Refine

lemma checkActiveIRQ_invs'_just_idle:
  "\<lbrace>invs' and ex_abs invs and ct_idle'
    and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>
   checkActiveIRQ
   \<lbrace>\<lambda>_. invs' and ct_idle'
    and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>" apply (simp add: checkActiveIRQ_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_abs invs and ct_idle' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> checkActiveIRQ \<lbrace>\<lambda>_. invs' and ct_idle' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ex_abs invs and ct_idle' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> do irq <- doMachineOp (getActiveIRQ False);
return (\<exists>y. irq = Some y)
od \<lbrace>\<lambda>_. invs' and ct_idle' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> proof (prove)
goal:
No subgoals!
theory Refine

lemma sched_act_rct_related:
  "\<lbrakk> (a, c) \<in> state_relation; ksSchedulerAction c = ResumeCurrentThread\<rbrakk>
     \<Longrightarrow> scheduler_action a = resume_cur_thread" by (case_tac "scheduler_action a", simp_all add: state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(a, c) \<in> state_relation; ksSchedulerAction c = ResumeCurrentThread\<rbrakk> \<Longrightarrow> scheduler_action a = resume_cur_thread
theory Refine

lemma domain_time_rel_eq:
  "(a, c) \<in> state_relation \<Longrightarrow> P (ksDomainTime c) = P (domain_time a)" by (clarsimp simp: state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, c) \<in> state_relation \<Longrightarrow> P (ksDomainTime c) = P (domain_time a)
theory Refine

lemma domain_list_rel_eq:
  "(a, c) \<in> state_relation \<Longrightarrow> P (ksDomSchedule c) = P (domain_list a)" by (clarsimp simp: state_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (a, c) \<in> state_relation \<Longrightarrow> P (ksDomSchedule c) = P (domain_list a)
theory Refine

theorem refinement:
  "ADT_H uop \<sqsubseteq> ADT_A uop" apply (rule sim_imp_refines) apply (rule L_invariantI) apply (rule akernel_invariant) apply (rule ckernel_invariant) apply (rule fw_sim_A_H) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ADT_H uop \<sqsubseteq> ADT_A uop proof (prove)
goal (1 subgoal):
 1. ADT_H uop \<sqsubseteq>\<^sub>F ADT_A uop proof (prove)
goal (3 subgoals):
 1. ADT_A uop \<Turnstile> ?I\<^sub>a2
 2. ADT_H uop \<Turnstile> ?I\<^sub>c2
 3. LI (ADT_A uop) (ADT_H uop) ?r2 (?I\<^sub>a2 \<times> ?I\<^sub>c2) proof (prove)
goal (2 subgoals):
 1. ADT_H uop \<Turnstile> ?I\<^sub>c2
 2. LI (ADT_A uop) (ADT_H uop) ?r2 (full_invs \<times> ?I\<^sub>c2) proof (prove)
goal (1 subgoal):
 1. LI (ADT_A uop) (ADT_H uop) ?r2 (full_invs \<times> full_invs') proof (prove)
goal:
No subgoals!
theory RAB_FN

lemma isCNodeCap_capUntypedPtr_capCNodePtr:
  "isCNodeCap c \<Longrightarrow> capUntypedPtr c = capCNodePtr c" by (clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isCNodeCap c \<Longrightarrow> global.capUntypedPtr c = capCNodePtr c
theory EmptyFail_H

lemma withoutPreemption_empty_fail[intro!, wp, simp]:
  "empty_fail m \<Longrightarrow> empty_fail (withoutPreemption m)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (withoutPreemption m)
theory EmptyFail_H

lemma withoutFailure_empty_fail[intro!, wp, simp]:
  "empty_fail m \<Longrightarrow> empty_fail (withoutFailure m)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (withoutFailure m)
theory EmptyFail_H

lemma catchFailure_empty_fail[intro!, wp, simp]:
  "\<lbrakk> empty_fail f; \<And>x. empty_fail (g x) \<rbrakk> \<Longrightarrow> empty_fail (catchFailure f g)" by (simp add: empty_fail_catch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>empty_fail f; \<And>x. empty_fail (g x)\<rbrakk> \<Longrightarrow> empty_fail (catchFailure f g)
theory EmptyFail_H

lemma emptyOnFailure_empty_fail[intro!, wp, simp]:
  "empty_fail m \<Longrightarrow> empty_fail (emptyOnFailure m)" by (simp add: emptyOnFailure_def empty_fail_catch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (emptyOnFailure m)
theory EmptyFail_H

lemma rethrowFailure_empty_fail [intro!, wp, simp]:
  "empty_fail m \<Longrightarrow> empty_fail (rethrowFailure f m)" apply (simp add:rethrowFailure_def o_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (rethrowFailure f m) proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (m <handle2> (\<lambda>x. throwError (f x))) proof (prove)
goal:
No subgoals!
theory EmptyFail_H

lemma unifyFailure_empty_fail [intro!, wp, simp]:
  "empty_fail f \<Longrightarrow> empty_fail (unifyFailure f)" by (simp add: unifyFailure_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (unifyFailure f)
theory EmptyFail_H

lemma lookupErrorOnFailure_empty_fail [intro!, wp, simp]:
  "empty_fail f \<Longrightarrow> empty_fail (lookupErrorOnFailure isSource f)" by (simp add: lookupErrorOnFailure_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (lookupErrorOnFailure isSource f)
theory EmptyFail_H

lemma setObject_empty_fail [intro!, wp, simp]:
  assumes x: "(\<And>a b c. empty_fail (updateObject v a x b c))"
  shows "empty_fail (setObject x v)" apply (simp add: setObject_def split_def) apply (wp x | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (setObject x v) proof (prove)
goal (1 subgoal):
 1. empty_fail (do ps <- gets ksPSpace;
p <- assert_opt (fst (lookupAround2 x ps));
obj' <- updateObject v (snd p) x (fst p) (snd (lookupAround2 x ps));
modify (ksPSpace_update (\<lambda>_. ps(fst p \<mapsto> obj')))
od) proof (prove)
goal:
No subgoals!
theory EmptyFail_H

lemma asUser_empty_fail [intro!, wp, simp]:
  "empty_fail f \<Longrightarrow> empty_fail (asUser t f)" apply (simp add:asUser_def) apply (wp | wpc | simp | simp add: empty_fail_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (asUser t f) proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
(a, uc') <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet uc' (tcbArch tcb)) tcb) t;
return a
od) proof (prove)
goal:
No subgoals!
theory EmptyFail_H

lemma capFaultOnFailure_empty_fail [intro!, wp, simp]:
  "empty_fail m \<Longrightarrow> empty_fail (capFaultOnFailure cptr rp m)" apply (simp add: capFaultOnFailure_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (capFaultOnFailure cptr rp m) proof (prove)
goal:
No subgoals!
theory EmptyFail_H

lemma empty_fail_getObject_ep [intro!, wp, simp]:
  "empty_fail (getObject p :: endpoint kernel)" by (simp add: empty_fail_getObject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getObject p)
theory EmptyFail_H

lemma getEndpoint_empty_fail [intro!, wp, simp]:
  "empty_fail (getEndpoint ep)" by (simp add: getEndpoint_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getEndpoint ep)
theory EmptyFail_H

lemma constOnFailure_empty_fail[intro!, wp, simp]:
  "empty_fail m \<Longrightarrow> empty_fail (constOnFailure x m)" by (simp add: constOnFailure_def const_def empty_fail_catch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail m \<Longrightarrow> empty_fail (constOnFailure x m)
theory EmptyFail_H

lemma ArchRetypeDecls_H_deriveCap_empty_fail[intro!, wp, simp]:
  "isPageTableCap y \<or> isPageDirectoryCap y \<or> isPageCap y
   \<or> isASIDControlCap y \<or> isASIDPoolCap y
   \<Longrightarrow> empty_fail (Arch.deriveCap x y)" apply (simp add: ARM_H.deriveCap_def) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isPageTableCap y \<or> isPageDirectoryCap y \<or> isPageCap y \<or> isASIDControlCap y \<or> isASIDPoolCap y \<Longrightarrow> empty_fail (Arch.deriveCap x y) proof (prove)
goal (1 subgoal):
 1. isPageTableCap y \<or> isPageDirectoryCap y \<or> isPageCap y \<or> isASIDControlCap y \<or> isASIDPoolCap y \<Longrightarrow> \<not> isASIDPoolCap y \<longrightarrow> \<not> isASIDControlCap y \<longrightarrow> \<not> isPageCap y \<longrightarrow> (isPageDirectoryCap y \<longrightarrow> (\<exists>ya. capPDMappedASID y = Some ya)) \<longrightarrow> (isPageDirectoryCap y \<longrightarrow> capPDMappedASID y = None) \<longrightarrow> (isPageTableCap y \<longrightarrow> (\<exists>a b. capPTMappedAddress y = Some (a, b))) \<longrightarrow> (isPageTableCap y \<longrightarrow> capPTMappedAddress y = None) \<longrightarrow> empty_fail undefined
theory EmptyFail_H

lemma transferCapsToSlots_empty_fail[intro!, wp, simp]:
  "empty_fail (transferCapsToSlots ep buffer n caps slots mi)" apply (induct caps arbitrary: slots n mi) apply simp apply (simp add: Let_def split_def
             split del: if_split) apply (simp | wp | wpc | safe)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (transferCapsToSlots ep buffer n caps slots mi) proof (prove)
goal (2 subgoals):
 1. \<And>slots n mi. empty_fail (transferCapsToSlots ep buffer n [] slots mi)
 2. \<And>a caps slots n mi. (\<And>slots n mi. empty_fail (transferCapsToSlots ep buffer n caps slots mi)) \<Longrightarrow> empty_fail (transferCapsToSlots ep buffer n (a # caps) slots mi) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. empty_fail (transferCapsToSlots ep buffer n caps slots mi)) \<Longrightarrow> empty_fail (transferCapsToSlots ep buffer n (a # caps) slots mi) proof (prove)
goal (1 subgoal):
 1. \<And>a caps slots n mi. (\<And>slots n mi. empty_fail (transferCapsToSlots ep buffer n caps slots mi)) \<Longrightarrow> empty_fail (constOnFailure (msgExtraCaps_update (\<lambda>_. word_of_nat n) mi) (if isEndpointCap (fst a) \<and> (\<exists>y. ep = Some y) \<and> capEPPtr (fst a) = the ep then doE y <- liftE (setExtraBadge buffer (capEPBadge (fst a)) n);
liftE (transferCapsToSlots ep buffer (Suc n) caps slots (msgCapsUnwrapped_update (\<lambda>_. msgCapsUnwrapped mi || 2 ^ n) mi))
odE else case slots of [] \<Rightarrow> returnOk $ msgExtraCaps_update (\<lambda>_. fromIntegral n) mi | destSlot # slots' \<Rightarrow> doE cap' <- unifyFailure $ global.deriveCap (snd a) $ fst a;
whenE (isNullCap cap') $ throw undefined;
withoutFailure $ cteInsert cap' (snd a) destSlot;
withoutFailure $ transferCapsToSlots ep buffer (Suc n) caps slots' mi
odE)) proof (prove)
goal:
No subgoals!
theory EmptyFail_H

lemma empty_fail_getObject_ap [intro!, wp, simp]:
  "empty_fail (getObject p :: asidpool kernel)" by (simp add: empty_fail_getObject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getObject p)
theory EmptyFail_H

lemma empty_fail_getObject_pde [intro!, wp, simp]:
  "empty_fail (getObject p :: pde kernel)" by (simp add: empty_fail_getObject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getObject p)
theory EmptyFail_H

lemma empty_fail_getObject_pte [intro!, wp, simp]:
  "empty_fail (getObject p :: pte kernel)" by (simp add: empty_fail_getObject)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (getObject p)
theory EmptyFail_H

lemma ignoreFailure_empty_fail[intro!, wp, simp]:
  "empty_fail x \<Longrightarrow> empty_fail (ignoreFailure x)" by (simp add: ignoreFailure_def empty_fail_catch)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail x \<Longrightarrow> empty_fail (ignoreFailure x)
theory EmptyFail_H

lemma ThreadDecls_H_restart_empty_fail[intro!, wp, simp]:
  "empty_fail (ThreadDecls_H.restart target)" by (fastforce simp: restart_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail (ThreadDecls_H.restart target)
theory EmptyFail_H

lemma spec_empty_fail_If:
  "\<lbrakk> P \<Longrightarrow> spec_empty_fail f s; \<not> P \<Longrightarrow> spec_empty_fail g s \<rbrakk>
   \<Longrightarrow> spec_empty_fail (if P then f else g) s" by (simp split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>P \<Longrightarrow> spec_empty_fail f s; \<not> P \<Longrightarrow> spec_empty_fail g s\<rbrakk> \<Longrightarrow> spec_empty_fail (if P then f else g) s
theory EmptyFail_H

lemma spec_empty_whenE':
  "\<lbrakk> P \<Longrightarrow> spec_empty_fail f s \<rbrakk> \<Longrightarrow> spec_empty_fail (whenE P f) s" by (simp add: whenE_def spec_empty_returnOk)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P \<Longrightarrow> spec_empty_fail f s) \<Longrightarrow> spec_empty_fail (whenE P f) s
theory EmptyFail_H

lemma checkCapAt_empty_fail[intro!, wp, simp]:
  "empty_fail action \<Longrightarrow> empty_fail (checkCapAt cap ptr action)" by (fastforce simp: checkCapAt_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail action \<Longrightarrow> empty_fail (checkCapAt cap ptr action)
theory EmptyFail_H

lemma assertDerived_empty_fail[intro!, wp, simp]:
  "empty_fail f \<Longrightarrow> empty_fail (assertDerived src cap f)" by (fastforce simp: assertDerived_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (assertDerived src cap f)