kings-crown/FVELER_Isabelle huggingface dataset:
theory SyscallArgs_C

lemma asUser_const_rv:
  assumes f: "\<lbrace>\<lambda>s. P\<rbrace> f \<lbrace>\<lambda>rv s. Q rv\<rbrace>"
  shows "\<lbrace>\<lambda>s. P\<rbrace> asUser t f \<lbrace>\<lambda>rv s. Q rv\<rbrace>" apply (simp add: asUser_def split_def) apply (wp) apply (clarsimp simp: threadGet_def) apply (wp getObject_tcb_wp) apply clarsimp apply (drule obj_at_ko_at') apply clarsimp apply (rename_tac tcb) apply (rule_tac x=tcb in exI) apply clarsimp apply (drule use_valid, rule f, assumption) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P\<rbrace> asUser t f \<lbrace>\<lambda>rv s. Q rv\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P\<rbrace> do uc <- threadGet (atcbContextGet \<circ> tcbArch) t;
p <- select_f (f uc);
y <- threadSet (\<lambda>tcb. tcbArch_update (\<lambda>_. atcbContextSet (snd p) (tcbArch tcb)) tcb) t;
return (fst p)
od \<lbrace>\<lambda>rv s. Q rv\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadGet (atcbContextGet \<circ> tcbArch) t \<lbrace>\<lambda>uc s. \<forall>x\<in>fst (f uc). Q (fst x)\<rbrace>
 2. \<And>s. P \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> liftM (atcbContextGet \<circ> tcbArch) (getObject t) \<lbrace>\<lambda>uc s. \<forall>x\<in>fst (f uc). Q (fst x)\<rbrace>
 2. \<And>s. P \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. P \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> ((\<lambda>uc s. \<forall>x\<in>fst (f uc). Q (fst x)) \<circ> (atcbContextGet \<circ> tcbArch)) ta s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P; tcb_at' t s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> (\<forall>x\<in>fst (f (atcbContextGet (tcbArch ta))). Q (fst x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>P; \<exists>ko. ko_at' ko t s \<and> True\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> (\<forall>x\<in>fst (f (atcbContextGet (tcbArch ta))). Q (fst x)) proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>P; ko_at' ko t s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> (\<forall>x\<in>fst (f (atcbContextGet (tcbArch ta))). Q (fst x)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>P; ko_at' tcb t s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> (\<forall>x\<in>fst (f (atcbContextGet (tcbArch ta))). Q (fst x)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>P; ko_at' tcb t s\<rbrakk> \<Longrightarrow> ko_at' tcb t s \<and> (\<forall>x\<in>fst (f (atcbContextGet (tcbArch tcb))). Q (fst x)) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb a b. \<lbrakk>P; ko_at' tcb t s; (a, b) \<in> fst (f (atcbContextGet (tcbArch tcb)))\<rbrakk> \<Longrightarrow> Q a proof (prove)
goal (1 subgoal):
 1. \<And>s tcb a b. \<lbrakk>P; ko_at' tcb t s; Q a\<rbrakk> \<Longrightarrow> Q a proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma ccorres_case_bools:
  assumes P: "ccorres r xf P P' hs (a True) (c True)"
  assumes Q: "ccorres r xf Q Q' hs (a False) (c False)"
  shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s))
                      ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'})
                      hs (a b) (c b)" apply (cases b) apply (auto simp: P Q) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not> b \<longrightarrow> s \<in> Q'}) hs (a b) (c b) proof (prove)
goal (2 subgoals):
 1. b \<Longrightarrow> ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not> b \<longrightarrow> s \<in> Q'}) hs (a b) (c b)
 2. \<not> b \<Longrightarrow> ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not> b \<longrightarrow> s \<in> Q'}) hs (a b) (c b) proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma pageBitsForSize_32 [simp]:
  "pageBitsForSize sz < 32" by (cases sz, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. pageBitsForSize sz < 32
theory SyscallArgs_C

lemma ccap_relation_frame_tags:
  "ccap_relation (ArchObjectCap (PageCap dev v0 v1 v2 v3)) cap \<Longrightarrow>
  cap_get_tag cap = scast cap_frame_cap \<or> cap_get_tag cap = scast cap_small_frame_cap" apply (case_tac "v2 = ARMSmallPage") apply (auto simp: cap_get_tag_isCap_unfolded_H_cap) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation (capability.ArchObjectCap (arch_capability.PageCap dev v0 v1 v2 v3)) cap \<Longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap dev v0 v1 v2 v3)) cap; v2 = Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap
 2. \<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capability.PageCap dev v0 v1 v2 v3)) cap; v2 \<noteq> Wellformed_C.ARMSmallPage\<rbrakk> \<Longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<or> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma ccorres_case_bools':
  assumes P: "b \<Longrightarrow> ccorres r xf P P' hs (a True) (c True)"
  assumes Q: "\<not> b \<Longrightarrow> ccorres r xf Q Q' hs (a False) (c False)"
  shows "ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not>b \<longrightarrow> Q s))
                      ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not>b \<longrightarrow> s \<in> Q'})
                      hs (a b) (c b)" apply (cases b) apply (auto simp: P Q) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not> b \<longrightarrow> s \<in> Q'}) hs (a b) (c b) proof (prove)
goal (2 subgoals):
 1. b \<Longrightarrow> ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not> b \<longrightarrow> s \<in> Q'}) hs (a b) (c b)
 2. \<not> b \<Longrightarrow> ccorres r xf (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) ({s. b \<longrightarrow> s \<in> P'} \<inter> {s. \<not> b \<longrightarrow> s \<in> Q'}) hs (a b) (c b) proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma capFVMRights_range:
  "\<And>cap. cap_get_tag cap = scast cap_frame_cap \<Longrightarrow>
   cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) \<le> 3"
  "\<And>cap. cap_get_tag cap = scast cap_small_frame_cap \<Longrightarrow>
   cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap) \<le> 3" by (simp add: cap_frame_cap_lift_def cap_small_frame_cap_lift_def
                cap_lift_def cap_tag_defs word_and_le1 mask_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<Longrightarrow> cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift cap) \<le> 3) &&& (\<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<Longrightarrow> cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift cap) \<le> 3)
theory SyscallArgs_C

lemma loadWordUser_wp:
  "\<lbrace>\<lambda>s. is_aligned p 2 \<and> (\<forall>v. user_word_at v p s \<longrightarrow> P v s)\<rbrace>
    loadWordUser p
   \<lbrace>P\<rbrace>" apply (simp add: loadWordUser_def loadWord_def stateAssert_def
                   user_word_at_def valid_def) apply (clarsimp simp: in_monad in_doMachineOp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. is_aligned p 2 \<and> (\<forall>v. user_word_at v p s \<longrightarrow> P v s)\<rbrace> loadWordUser p \<lbrace>P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<forall>s. is_aligned p 2 \<and> (is_aligned p 2 \<and> pointerInUserData p s \<longrightarrow> P (word_rcat [underlying_memory (ksMachineState s) (p + 3), underlying_memory (ksMachineState s) (p + 2), underlying_memory (ksMachineState s) (p + 1), underlying_memory (ksMachineState s) p]) s) \<longrightarrow> (\<forall>x\<in>fst ((do y <- do s <- get;
assert (pointerInUserData p s)
od;
doMachineOp (do m <- gets underlying_memory;
y <- assert (p && mask 2 = 0);
return (word_rcat [m (p + 3), m (p + 2), m (p + 1), m p])
od)
od) s). case x of (r, s') \<Rightarrow> P r s') proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma sysargs_rel_to_n:
  "sysargs_rel args buffer s \<Longrightarrow> sysargs_rel_n args buffer n s = (n < length args)" by (auto simp add: sysargs_rel_def sysargs_rel_n_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. sysargs_rel args buffer s \<Longrightarrow> sysargs_rel_n args buffer n s = (n < length args)
theory SyscallArgs_C

lemma length_msgRegisters:
  "length ARM_H.msgRegisters = unat (scast n_msgRegisters :: word32)" by (simp add: msgRegisters_unfold n_msgRegisters_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. length TCB_H.msgRegisters = unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters)
theory SyscallArgs_C

lemma getMRs_len[simplified]:
  "\<lbrace>\<top>\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. length args > unat (scast n_msgRegisters :: word32) \<longrightarrow> buffer \<noteq> None\<rbrace>" apply (simp add: getMRs_def) apply (cases buffer, simp_all add:hoare_TrueI) apply (wp asUser_const_rv | simp)+ apply (simp add: length_msgRegisters) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args s. unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args \<longrightarrow> buffer \<noteq> None\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do hardwareMRValues <- asUser thread (mapM getRegister TCB_H.msgRegisters);
bufferMRValues <- case buffer of None \<Rightarrow> return [] | Some bufferPtr \<Rightarrow> return (map (\<lambda>x. bufferPtr + PPtr (x * word_of_nat wordSize)) [fromIntegral $ length TCB_H.msgRegisters + 1 .e. msgMaxLength]) >>= mapM loadWordUser;
return (take (unat (msgLength mi)) hardwareMRValues @ take (unat (msgLength mi) - length hardwareMRValues) bufferMRValues)
od \<lbrace>\<lambda>args s. unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args \<longrightarrow> (\<exists>y. buffer = Some y)\<rbrace> proof (prove)
goal (1 subgoal):
 1. buffer = None \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> do hardwareMRValues <- asUser thread (mapM getRegister TCB_H.msgRegisters);
return (take (unat (msgLength mi)) hardwareMRValues)
od \<lbrace>\<lambda>args s. \<not> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args\<rbrace> proof (prove)
goal (1 subgoal):
 1. buffer = None \<Longrightarrow> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length TCB_H.msgRegisters \<longrightarrow> \<not> unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < unat (msgLength mi) proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma getMRs_sysargs_rel:
  "\<lbrace>(\<lambda>s. thread = ksCurThread s) and cur_tcb' and case_option \<top> valid_ipc_buffer_ptr' buffer and K (msgLength mi \<le> msgMaxLength)\<rbrace>
  getMRs thread buffer mi \<lbrace>\<lambda>args. sysargs_rel args buffer\<rbrace>" apply (simp add: sysargs_rel_def) apply (wp getMRs_rel getMRs_len|simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. thread = ksCurThread s) and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and K (msgLength mi \<le> msgMaxLength)\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args. sysargs_rel args buffer\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. thread = ksCurThread s) and cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and (\<lambda>y. msgLength mi \<le> msgMaxLength)\<rbrace> getMRs thread buffer mi \<lbrace>\<lambda>args. cur_tcb' and (case buffer of None \<Rightarrow> \<lambda>_. True | Some x \<Rightarrow> valid_ipc_buffer_ptr' x) and getMRs_rel args buffer and (\<lambda>_. unat (SCAST(32 signed \<rightarrow> 32) n_msgRegisters) < length args \<longrightarrow> (\<exists>y. buffer = Some y))\<rbrace> proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma ccorres_assume_pre:
  assumes "\<And>s. P s \<Longrightarrow> ccorres r xf (P and (\<lambda>s'. s' = s)) P' hs H C"
  shows "ccorres r xf P P' hs H C" apply (clarsimp simp: ccorres_underlying_def) apply (frule assms) apply (simp add: ccorres_underlying_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf P P' hs H C proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (H a); \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (H a); \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t); ccorres r xf (P and (\<lambda>s'. s' = a)) P' hs H C\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>(a, b) \<in> rf_sr; P a; b \<in> P'; \<not> snd (H a); \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,b\<rangle> \<Rightarrow> (n, t); \<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> s = a \<and> s' \<in> P' \<and> \<not> snd (H s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>C # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (H s). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False))\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (H a). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) r xf r xf ra s'' | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma index_msgRegisters_less':
  "n < 4 \<Longrightarrow> index msgRegistersC n < 0x14" by (simp add: msgRegistersC_def fupdate_def Arrays.update_def
                fcp_beta "StrictC'_register_defs")

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 4 \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[n] < 0x14
theory SyscallArgs_C

lemma index_msgRegisters_less:
  "n < 4 \<Longrightarrow> index msgRegistersC n <s 0x14"
  "n < 4 \<Longrightarrow> index msgRegistersC n < 0x14" using index_msgRegisters_less' by (simp_all add: word_sless_msb_less)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (n < 4 \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[n] <s 0x14) &&& (n < 4 \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[n] < 0x14) proof (prove)
using this:
?n < 4 \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[?n] < 0x14

goal (1 subgoal):
 1. (n < 4 \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[n] <s 0x14) &&& (n < 4 \<Longrightarrow> kernel_all_global_addresses.msgRegisters.[n] < 0x14)
theory SyscallArgs_C

lemma array_assertion_valid_ipc_buffer_ptr_abs:
  "\<forall>s s'. (s, s') \<in> rf_sr \<and> (valid_ipc_buffer_ptr' (ptr_val (p s)) s)
        \<and> (n s' \<le> 2 ^ (msg_align_bits - 2) \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0))
    \<longrightarrow> (x s' = 0 \<or> array_assertion (p s :: word32 ptr) (n s') (hrs_htd (t_hrs_' (globals s'))))" apply (intro allI impI disjCI2, clarsimp) apply (erule(1) valid_ipc_buffer_ptr_array, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s s'. (s, s') \<in> rf_sr \<and> valid_ipc_buffer_ptr' (ptr_val (p s)) s \<and> n s' \<le> 2 ^ (msg_align_bits - 2) \<and> (x s' \<noteq> (0::'a) \<longrightarrow> n s' \<noteq> 0) \<longrightarrow> x s' = (0::'a) \<or> array_assertion (p s) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>x s' \<noteq> (0::'a); (s, s') \<in> rf_sr; valid_ipc_buffer_ptr' (ptr_val (p s)) s; n s' \<le> 2 ^ (msg_align_bits - 2); 0 < n s'\<rbrakk> \<Longrightarrow> array_assertion (p s) (n s') (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal:
No subgoals!
theory SyscallArgs_C

lemma ccorres_equals_throwError:
  "\<lbrakk> f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c \<rbrakk>
     \<Longrightarrow> ccorres_underlying sr Gamm rr xf arr axf P P' hs f c" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f = throwError v; ccorres_underlying sr Gamm rr xf arr axf P P' hs (throwError v) c\<rbrakk> \<Longrightarrow> ccorres_underlying sr Gamm rr xf arr axf P P' hs f c
theory IpcCancel_C

lemma cready_queues_index_to_C_in_range':
  assumes prems: "qdom \<le> ucast maxDom" "prio \<le> ucast maxPrio"
  shows "cready_queues_index_to_C qdom prio < num_tcb_queues" proof - have P: "unat prio < numPriorities" using prems by (simp add: numPriorities_def seL4_MaxPrio_def Suc_le_lessD unat_le_helper) have Q: "unat qdom < numDomains" using prems by (simp add: maxDom_to_H le_maxDomain_eq_less_numDomains word_le_nat_alt) show ?thesis using mod_lemma[OF _ P, where q="unat qdom" and c=numDomains] Q by (clarsimp simp: num_tcb_queues_calculation cready_queues_index_to_C_def field_simps) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cready_queues_index_to_C qdom prio < num_tcb_queues proof (state)
goal (1 subgoal):
 1. cready_queues_index_to_C qdom prio < num_tcb_queues proof (prove)
goal (1 subgoal):
 1. unat prio < Config_H.numPriorities proof (prove)
using this:
qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom
prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio

goal (1 subgoal):
 1. unat prio < Config_H.numPriorities proof (state)
this:
unat prio < Config_H.numPriorities

goal (1 subgoal):
 1. cready_queues_index_to_C qdom prio < num_tcb_queues proof (prove)
goal (1 subgoal):
 1. unat qdom < numDomains proof (prove)
using this:
qdom \<le> UCAST(32 signed \<rightarrow> 8) maxDom
prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio

goal (1 subgoal):
 1. unat qdom < numDomains proof (state)
this:
unat qdom < numDomains

goal (1 subgoal):
 1. cready_queues_index_to_C qdom prio < num_tcb_queues proof (prove)
goal (1 subgoal):
 1. cready_queues_index_to_C qdom prio < num_tcb_queues proof (prove)
using this:
0 < numDomains \<Longrightarrow> Config_H.numPriorities * (unat qdom mod numDomains) + unat prio < Config_H.numPriorities * numDomains
unat qdom < numDomains

goal (1 subgoal):
 1. cready_queues_index_to_C qdom prio < num_tcb_queues proof (state)
this:
cready_queues_index_to_C qdom prio < num_tcb_queues

goal:
No subgoals!
theory IpcCancel_C

lemma cready_queues_index_to_C_inj:
  "\<lbrakk> cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio';
     prio \<le> ucast maxPrio; prio' \<le> ucast maxPrio \<rbrakk> \<Longrightarrow> prio = prio' \<and> qdom = qdom'" apply (rule context_conjI) apply (auto simp: cready_queues_index_to_C_def numPriorities_def
                    seL4_MaxPrio_def word_le_nat_alt dest: arg_cong[where f="\<lambda>x. x mod 256"]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; prio' \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> prio = prio' \<and> qdom = qdom' proof (prove)
goal (2 subgoals):
 1. \<lbrakk>cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; prio' \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> prio = prio'
 2. \<lbrakk>cready_queues_index_to_C qdom prio = cready_queues_index_to_C qdom' prio'; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; prio' \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; prio = prio'\<rbrakk> \<Longrightarrow> qdom = qdom' proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma cready_queues_index_to_C_distinct:
  "\<lbrakk> qdom = qdom' \<longrightarrow> prio \<noteq> prio'; prio \<le> ucast maxPrio; prio' \<le> ucast maxPrio \<rbrakk>
   \<Longrightarrow> cready_queues_index_to_C qdom prio \<noteq> cready_queues_index_to_C qdom' prio'" apply (auto simp: cready_queues_index_to_C_inj) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>qdom = qdom' \<longrightarrow> prio \<noteq> prio'; prio \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio; prio' \<le> UCAST(32 signed \<rightarrow> 8) seL4_MaxPrio\<rbrakk> \<Longrightarrow> cready_queues_index_to_C qdom prio \<noteq> cready_queues_index_to_C qdom' prio' proof (prove)
goal:
No subgoals!
theory IpcCancel_C

lemma invs_valid_queues'[elim!]:
  "invs' s \<Longrightarrow> valid_queues' s" by (simp add: invs'_def valid_state'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. invs' s \<Longrightarrow> valid_queues' s