kings-crown/FVELER_Isabelle huggingface dataset:
theory DetWP

lemma det_wp_loadWordUser [wp]:
  "det_wp (pointerInUserData x and K (is_aligned x 2)) (loadWordUser x)" apply (simp add: loadWordUser_def loadWord_def) apply (rule det_wp_pre, wp) apply (rule det_wp_pre, wp) apply clarsimp apply assumption apply wp apply (clarsimp simp: is_aligned_mask) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (pointerInUserData x and K (is_aligned x 2)) (loadWordUser x) proof (prove)
goal (1 subgoal):
 1. det_wp (pointerInUserData x and (\<lambda>y. is_aligned x 2)) (do y <- stateAssert (pointerInUserData x) [];
doMachineOp (do m <- gets underlying_memory;
y <- assert (x && mask 2 = 0);
return (word_rcat [m (x + 3), m (x + 2), m (x + 1), m x])
od)
od) proof (prove)
goal (3 subgoals):
 1. \<And>y. det_wp (\<lambda>_. ?Q7 y) (do m <- gets underlying_memory;
y <- assert (x && mask 2 = 0);
return (word_rcat [m (x + 3), m (x + 2), m (x + 1), m x])
od)
 2. \<lbrace>?P'4\<rbrace> stateAssert (pointerInUserData x) [] \<lbrace>\<lambda>y _. ?Q7 y\<rbrace>
 3. \<And>s. (pointerInUserData x and (\<lambda>y. is_aligned x 2)) s \<Longrightarrow> (pointerInUserData x and ?P'4) s proof (prove)
goal (3 subgoals):
 1. \<And>y s. ?Q7 y \<Longrightarrow> ((\<lambda>_. True) and ((\<lambda>_. x && mask 2 = 0) and (\<lambda>s. x && mask 2 = 0 \<longrightarrow> True))) s
 2. \<lbrace>?P'4\<rbrace> stateAssert (pointerInUserData x) [] \<lbrace>\<lambda>y _. ?Q7 y\<rbrace>
 3. \<And>s. (pointerInUserData x and (\<lambda>y. is_aligned x 2)) s \<Longrightarrow> (pointerInUserData x and ?P'4) s proof (prove)
goal (3 subgoals):
 1. ?Q7 () \<Longrightarrow> x && mask 2 = 0
 2. \<lbrace>?P'4\<rbrace> stateAssert (pointerInUserData x) [] \<lbrace>\<lambda>y _. ?Q7 y\<rbrace>
 3. \<And>s. (pointerInUserData x and (\<lambda>y. is_aligned x 2)) s \<Longrightarrow> (pointerInUserData x and ?P'4) s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'4\<rbrace> stateAssert (pointerInUserData x) [] \<lbrace>\<lambda>y _. x && mask 2 = 0\<rbrace>
 2. \<And>s. (pointerInUserData x and (\<lambda>y. is_aligned x 2)) s \<Longrightarrow> (pointerInUserData x and ?P'4) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pointerInUserData x and (\<lambda>y. is_aligned x 2)) s \<Longrightarrow> (pointerInUserData x and (\<lambda>s. pointerInUserData x s \<longrightarrow> x && mask 2 = 0)) s proof (prove)
goal:
No subgoals!
theory DetWP

lemma det_wp_setTCB [wp]:
  "det_wp (tcb_at' t) (setObject t (v::tcb))" apply (rule det_wp_pre) apply (wp|wpc|simp)+ apply (clarsimp simp: objBits_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (tcb_at' t) (setObject t v) proof (prove)
goal (2 subgoals):
 1. det_wp ?P' (setObject t v)
 2. \<And>s. tcb_at' t s \<Longrightarrow> ?P' s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> obj_at' (\<lambda>k. objBits k = objBits v) t s proof (prove)
goal:
No subgoals!
theory DetWP

lemma det_wp_threadGet [wp]:
  "det_wp (tcb_at' t) (threadGet f t)" apply (simp add: threadGet_def) apply (rule det_wp_pre, wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (tcb_at' t) (threadGet f t) proof (prove)
goal (1 subgoal):
 1. det_wp (tcb_at' t) (liftM f (getObject t)) proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> tcb_at' t s proof (prove)
goal:
No subgoals!
theory DetWP

lemma det_wp_threadSet [wp]:
  "det_wp (tcb_at' t) (threadSet f t)" apply (simp add: threadSet_def) apply (rule det_wp_pre, wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. det_wp (tcb_at' t) (threadSet f t) proof (prove)
goal (1 subgoal):
 1. det_wp (tcb_at' t) (do tcb <- getObject t;
setObject t (f tcb)
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at' t s \<Longrightarrow> (tcb_at' t and tcb_at' t) s proof (prove)
goal:
No subgoals!
theory DetWP

lemma wordSize_def':
  "wordSize = 4" unfolding wordSize_def wordBits_def by (simp add: word_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wordSize = 4 proof (prove)
goal (1 subgoal):
 1. finiteBitSize undefined div 8 = 4
theory SyscallArgs_C

lemma replyOnRestart_twice[simplified]:
  "do replyOnRestart t reply isCall; replyOnRestart t reply' isCall'; m od
   = do replyOnRestart t reply isCall; m od" apply (rule ext) apply (rule bind_apply_cong[OF refl]) apply simp apply (subst bind_apply_cong [OF _ refl]) apply (erule replyOnRestart_twice') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do replyOnRestart t reply isCall;
replyOnRestart t reply' isCall';
m
od = do replyOnRestart t reply isCall;
m
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do replyOnRestart t reply isCall;
replyOnRestart t reply' isCall';
m
od) x = (do replyOnRestart t reply isCall;
m
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x rv st. (rv, st) \<in> fst (replyOnRestart t reply isCall x) \<Longrightarrow> K_bind (do replyOnRestart t reply' isCall';
m
od) rv st = K_bind m rv st proof (prove)
goal (1 subgoal):
 1. \<And>x st. ((), st) \<in> fst (replyOnRestart t reply isCall x) \<Longrightarrow> (do y <- replyOnRestart t reply' isCall';
m
od) st = m st proof (prove)
goal (2 subgoals):
 1. \<And>x st. ((), st) \<in> fst (replyOnRestart t reply isCall x) \<Longrightarrow> replyOnRestart t reply' isCall' st = ?f'5 x st (?s'5 x st)
 2. \<And>x st. ((), st) \<in> fst (replyOnRestart t reply isCall x) \<Longrightarrow> (do rv <- ?f'5 x st;
m
od) (?s'5 x st) = m st proof (prove)
goal (1 subgoal):
 1. \<And>x st. ((), st) \<in> fst (replyOnRestart t reply isCall x) \<Longrightarrow> (do rv <- return ();
m
od) st = m st proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma intr_and_se_rel_simps[simp]:
  "intr_and_se_rel (Inl se) = syscall_error_rel se"
  "intr_and_se_rel (Inr irq) = cintr irq" by (rule ext | simp add: intr_and_se_rel_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. intr_and_se_rel (Inl se) = syscall_error_rel se &&& intr_and_se_rel (Inr irq) = cintr irq
theory SyscallArgs_C

lemma errstate_globals_overwrite[simp]:
  "errstate (s \<lparr> globals := globals t \<rparr>) = errstate t" by (simp add: errstate_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. errstate (s\<lparr>globals := globals t\<rparr>) = errstate t
theory SyscallArgs_C

lemma slotcap_in_mem_def2:
  "slotcap_in_mem cap slot (ctes_of s)
    = cte_wp_at' (\<lambda>cte. cap = cteCap cte) slot s" by (simp add: slotcap_in_mem_def cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slotcap_in_mem cap slot (ctes_of s) = cte_wp_at' (\<lambda>cte. cap = cteCap cte) slot s
theory SyscallArgs_C

lemma o_xo_injector:
  "((f o f') \<currency> r) = ((f \<currency> r) o case_sum (Inl o f') Inr)" by (intro ext, simp split: sum.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (f \<circ> f') \<currency> r = f \<currency> r \<circ> case_sum (Inl \<circ> f') Inr
theory SyscallArgs_C

lemma getSlotCap_eq:
  "slotcap_in_mem cap slot (ctes_of s)
    \<Longrightarrow> getSlotCap slot s = return cap s" apply (clarsimp simp: slotcap_in_mem_def2 getSlotCap_def) apply (frule cte_wp_at_weakenE'[OF _ TrueI]) apply (drule no_failD[OF no_fail_getCTE]) apply (clarsimp simp: cte_wp_at'_def getCTE_def[symmetric]
                        bind_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. slotcap_in_mem cap slot (ctes_of s) \<Longrightarrow> getSlotCap slot s = return cap s proof (prove)
goal (1 subgoal):
 1. cte_wp_at' (\<lambda>cte. cap = cteCap cte) slot s \<Longrightarrow> (do cte <- getCTE slot;
return (cteCap cte)
od) s = return cap s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cap = cteCap cte) slot s; cte_wp_at' (\<lambda>c. True) slot s\<rbrakk> \<Longrightarrow> (do cte <- getCTE slot;
return (cteCap cte)
od) s = return cap s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at' (\<lambda>cte. cap = cteCap cte) slot s; \<not> snd (getCTE slot s)\<rbrakk> \<Longrightarrow> (do cte <- getCTE slot;
return (cteCap cte)
od) s = return cap s proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma getSlotCap_ccorres_fudge:
  "ccorres_underlying sr Gamm rvr xf ar axf P Q hs (do rv \<leftarrow> getSlotCap slot; _ \<leftarrow> assert (rv = cp); a rv od) c
    \<Longrightarrow> ccorres_underlying sr Gamm rvr xf ar axf
          (P and (slotcap_in_mem cp slot o ctes_of))
          Q hs (a cp) c" apply (simp add: ccorres_underlying_def) apply (erule ballEI, clarsimp del: allI) apply (simp add: bind_apply_cong [OF getSlotCap_eq refl]
             cong: xstate.case_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamm rvr xf ar axf P Q hs (do rv <- getSlotCap slot;
_ <- assert (rv = cp);
a rv
od) c \<Longrightarrow> ccorres_underlying sr Gamm rvr xf ar axf (P and slotcap_in_mem cp slot \<circ> ctes_of) Q hs (a cp) c proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> Q \<and> \<not> snd ((do rv <- getSlotCap slot;
_ <- assert (rv = cp);
a rv
od) s) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((do rv <- getSlotCap slot;
_ <- assert (rv = cp);
a rv
od) s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf ar axf r s'' | _ \<Rightarrow> False)) \<Longrightarrow> \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> slotcap_in_mem cp slot (ctes_of s) \<and> s' \<in> Q \<and> \<not> snd (a cp s) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (a cp s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf ar axf r s'' | _ \<Rightarrow> False)) proof (prove)
goal (1 subgoal):
 1. \<And>aa b. \<lbrakk>(aa, b) \<in> sr; \<not> snd ((do rv <- getSlotCap slot;
_ <- assert (rv = cp);
a rv
od) aa) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst ((do rv <- getSlotCap slot;
_ <- assert (rv = cp);
a rv
od) aa). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf ar axf r s'' | _ \<Rightarrow> False)); P aa; slotcap_in_mem cp slot (ctes_of aa); b \<in> Q; \<not> snd (a cp aa)\<rbrakk> \<Longrightarrow> \<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>c # hs,b\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (a cp aa). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) rvr xf ar axf r s'' | _ \<Rightarrow> False) proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma syscall_error_throwError_ccorres_direct:
  "\<lbrakk> is_syscall_error_code f code;
     \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err \<rbrakk>
   \<Longrightarrow>
   ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_')
      \<top> (UNIV) (SKIP # hs)
      (throwError (Inl err)) code" apply (rule ccorres_from_vcg_throws) apply (rule allI, rule conseqPre) apply (erule iffD1[OF is_syscall_error_code_def, THEN spec]) apply (clarsimp simp: throwError_def return_def) apply (simp add: syscall_error_rel_def exception_defs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> ccorres (intr_and_se_rel \<currency> dc) (liftxf errstate id v' ret__unsigned_long_') (\<lambda>_. True) UNIV (SKIP # hs) (throwError (Inl err)) code proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} code {},{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Inl err) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (intr_and_se_rel \<currency> dc) rv (liftxf errstate id v' ret__unsigned_long_' s)} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?P'4 \<sigma>) code {},{s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Inl err) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (intr_and_se_rel \<currency> dc) rv (liftxf errstate id v' ret__unsigned_long_' s)}
 2. \<And>\<sigma>. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'4 \<sigma> proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. globals_update (current_syscall_error_'_update f) s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR, global_exn_var_' := Return\<rparr> \<in> {s. \<exists>(rv, \<sigma>')\<in>fst (throwError (Inl err) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (intr_and_se_rel \<currency> dc) rv (liftxf errstate id v' ret__unsigned_long_' s)}} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>is_syscall_error_code f code; \<And>err' ft'. syscall_error_to_H (f err') ft' = Some err; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> EXCEPTION_SYSCALL_ERROR \<noteq> EXCEPTION_NONE \<and> syscall_error_rel err (SCAST(32 signed \<rightarrow> 32) EXCEPTION_SYSCALL_ERROR) (errstate (globals_update (current_syscall_error_'_update f) x)) proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma interpret_excaps_test_null2:
  "n < 3 \<Longrightarrow>
   (index (excaprefs_C excps) n = NULL)
      = (length (interpret_excaps excps) \<le> n
            \<and> index (idButNot excaprefs_C excps) n = NULL)" unfolding idButNot_def apply safe apply (rule ccontr, simp only: linorder_not_le) apply (frule(1) interpret_excaps_test_null [OF order_less_imp_le]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 3 \<Longrightarrow> (excaprefs_C excps.[n] = NULL) = (length (interpret_excaps excps) \<le> n \<and> idButNot excaprefs_C excps.[n] = NULL) proof (prove)
goal (1 subgoal):
 1. n < 3 \<Longrightarrow> (excaprefs_C excps.[n] = NULL) = (length (interpret_excaps excps) \<le> n \<and> excaprefs_C excps.[n] = NULL) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 3; excaprefs_C excps.[n] = NULL\<rbrakk> \<Longrightarrow> length (interpret_excaps excps) \<le> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 3; excaprefs_C excps.[n] = NULL; n < length (interpret_excaps excps)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 3; excaprefs_C excps.[n] = NULL; n < length (interpret_excaps excps); (excaprefs_C excps.[n] = NULL) = (length (interpret_excaps excps) = n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma invocationCatch_use_injection_handler:
  "(v >>= invocationCatch thread isBlocking isCall injector)
     = (injection_handler Inl v >>=E
           (invocationCatch thread isBlocking isCall injector o Inr))" apply (simp add: injection_handler_def handleE'_def
                   bind_bindE_assoc) apply (rule ext, rule bind_apply_cong [OF refl]) apply (simp add: invocationCatch_def return_returnOk
            split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. v >>= invocationCatch thread isBlocking isCall injector = injection_handler Inl v >>=E (invocationCatch thread isBlocking isCall injector \<circ> Inr) proof (prove)
goal (1 subgoal):
 1. v >>= invocationCatch thread isBlocking isCall injector = do rv <- v;
(case rv of Inl e \<Rightarrow> throwError (Inl e) | Inr v' \<Rightarrow> return (Inr v')) >>=E (invocationCatch thread isBlocking isCall injector \<circ> Inr)
od proof (prove)
goal (1 subgoal):
 1. \<And>x rv st. (rv, st) \<in> fst (v x) \<Longrightarrow> invocationCatch thread isBlocking isCall injector rv st = ((case rv of Inl e \<Rightarrow> throwError (Inl e) | Inr v' \<Rightarrow> return (Inr v')) >>=E (invocationCatch thread isBlocking isCall injector \<circ> Inr)) st proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma ccorres_injection_handler_csum1:
  "ccorres (f \<currency> r) xf P P' hs a c
    \<Longrightarrow> ccorres
           ((\<lambda>rv a b. \<exists>rv'. rv = injector rv' \<and> f rv' a b) \<currency> r) xf P P' hs
           (injection_handler injector a) c" apply (simp add: injection_handler_liftM) apply (erule ccorres_rel_imp) apply (auto split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (f \<currency> r) xf P P' hs a c \<Longrightarrow> ccorres ((\<lambda>rv a b. \<exists>rv'. rv = injector rv' \<and> f rv' a b) \<currency> r) xf P P' hs (injection_handler injector a) c proof (prove)
goal (1 subgoal):
 1. ccorres (f \<currency> r) xf P P' hs a c \<Longrightarrow> ccorres ((\<lambda>rv a b. \<exists>rv'. rv = injector rv' \<and> f rv' a b) \<currency> r \<circ> case_sum (\<lambda>ex. Inl (injector ex)) Inr) xf P P' hs a c proof (prove)
goal (1 subgoal):
 1. \<And>x y. (f \<currency> r) x (xf y) \<Longrightarrow> ((\<lambda>rv a b. \<exists>rv'. rv = injector rv' \<and> f rv' a b) \<currency> r \<circ> case_sum (\<lambda>ex. Inl (injector ex)) Inr) x (xf y) proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma is_nondet_refinement_refl[simp]:
  "is_nondet_refinement a a" by (simp add: is_nondet_refinement_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_nondet_refinement a a
theory SyscallArgs_C

lemma is_nondet_refinement_bind:
  "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk>
     \<Longrightarrow> is_nondet_refinement (a >>= b) (c >>= d)" apply (clarsimp simp: is_nondet_refinement_def bind_def split_def) apply fast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv)\<rbrakk> \<Longrightarrow> is_nondet_refinement (a >>= b) (c >>= d) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. (snd (a s) \<longrightarrow> snd (c s)) \<and> fst (a s) \<subseteq> fst (c s); \<And>rv. \<forall>s. (snd (b rv s) \<longrightarrow> snd (d rv s)) \<and> fst (b rv s) \<subseteq> fst (d rv s)\<rbrakk> \<Longrightarrow> ((\<exists>x\<in>fst (a s). snd (b (fst x) (snd x))) \<longrightarrow> (\<exists>x\<in>fst (c s). snd (d (fst x) (snd x))) \<or> snd (c s)) \<and> (\<Union>x\<in>fst (a s). fst (b (fst x) (snd x))) \<subseteq> (\<Union>x\<in>fst (c s). fst (d (fst x) (snd x))) proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma is_nondet_refinement_bindE:
  "\<lbrakk> is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv) \<rbrakk>
     \<Longrightarrow> is_nondet_refinement (a >>=E b) (c >>=E d)" apply (simp add: bindE_def) apply (erule is_nondet_refinement_bind) apply (simp add: lift_def split: sum.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv)\<rbrakk> \<Longrightarrow> is_nondet_refinement (a >>=E b) (c >>=E d) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_nondet_refinement a c; \<And>rv. is_nondet_refinement (b rv) (d rv)\<rbrakk> \<Longrightarrow> is_nondet_refinement (a >>= Nondet_Monad.lift b) (c >>= Nondet_Monad.lift d) proof (prove)
goal (1 subgoal):
 1. \<And>rv. (\<And>rv. is_nondet_refinement (b rv) (d rv)) \<Longrightarrow> is_nondet_refinement (Nondet_Monad.lift b rv) (Nondet_Monad.lift d rv) proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma is_nondet_refinement_alternative1:
  "is_nondet_refinement a (a \<sqinter> b)" by (clarsimp simp add: is_nondet_refinement_def alternative_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_nondet_refinement a (a \<sqinter> b)
theory SyscallArgs_C

lemma no_fail_getMRs:
  "no_fail (tcb_at' thread and case_option \<top> valid_ipc_buffer_ptr' buffer)
           (getMRs thread buffer info)" apply (rule det_wp_no_fail) apply (rule det_wp_getMRs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (tcb_at' thread and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (getMRs thread buffer info) proof (prove)
goal (1 subgoal):
 1. det_wp (tcb_at' thread and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x)) (getMRs thread buffer info) proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma msgRegisters_ccorres:
  "n < unat n_msgRegisters \<Longrightarrow>
  register_from_H (ARM_H.msgRegisters ! n) = (index msgRegistersC n)" apply (simp add: msgRegistersC_def msgRegisters_unfold fupdate_def) apply (simp add: Arrays.update_def n_msgRegisters_def fcp_beta nth_Cons' split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < unat n_msgRegisters \<Longrightarrow> register_from_H (TCB_H.msgRegisters ! n) = kernel_all_global_addresses.msgRegisters.[n] proof (prove)
goal (1 subgoal):
 1. n < unat n_msgRegisters \<Longrightarrow> register_from_H ([register.R2, register.R3, register.R4, register.R5] ! n) = Arrays.update (Arrays.update (Arrays.update (Arrays.update (ARRAY _. 0) 0 (SCAST(32 signed \<rightarrow> 32) Kernel_C.R2)) (Suc 0) (SCAST(32 signed \<rightarrow> 32) Kernel_C.R3)) 2 (SCAST(32 signed \<rightarrow> 32) Kernel_C.R4)) 3 (SCAST(32 signed \<rightarrow> 32) Kernel_C.R5).[n] proof (prove)
goal:
No subgoals!