kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_R

lemma getSlotCap_cap_to'[wp]:
  "\<lbrace>\<top>\<rbrace> getSlotCap cp \<lbrace>\<lambda>rv s. \<forall>r\<in>cte_refs' rv (irq_node' s). ex_cte_cap_to' r s\<rbrace>" apply (simp add: getSlotCap_def) apply (wp getCTE_wp) apply (fastforce simp: cte_wp_at_ctes_of ex_cte_cap_to'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> getSlotCap cp \<lbrace>\<lambda>rv s. \<forall>r\<in>cte_refs' rv (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do cte <- getCTE cp;
return (cteCap cte)
od \<lbrace>\<lambda>rv s. \<forall>r\<in>cte_refs' rv (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> cte_wp_at' (\<lambda>_. True) cp s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) cp s \<and> (\<forall>r\<in>cte_refs' (cteCap cte) (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s)) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma getSlotCap_cap_to2:
  "\<lbrace>\<top> and K (\<forall>cap. P cap \<longrightarrow> Q cap)\<rbrace>
     getSlotCap slot
   \<lbrace>\<lambda>rv s. P rv \<longrightarrow> (\<forall>x \<in> cte_refs' rv (irq_node' s). ex_cte_cap_wp_to' Q x s)\<rbrace>" apply (simp add: getSlotCap_def) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of ex_cte_cap_wp_to'_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>_. True) and K (\<forall>cap. P cap \<longrightarrow> Q cap)\<rbrace> getSlotCap slot \<lbrace>\<lambda>rv s. P rv \<longrightarrow> (\<forall>x\<in>cte_refs' rv (irq_node' s). ex_cte_cap_wp_to' Q x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. \<forall>cap. P cap \<longrightarrow> Q cap\<rbrace> do cte <- getCTE slot;
return (cteCap cte)
od \<lbrace>\<lambda>rv s. P rv \<longrightarrow> (\<forall>x\<in>cte_refs' rv (irq_node' s). ex_cte_cap_wp_to' Q x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>cap. P cap \<longrightarrow> Q cap \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) slot s \<and> (P (cteCap cte) \<longrightarrow> (\<forall>x\<in>cte_refs' (cteCap cte) (irq_node' s). ex_cte_cap_wp_to' Q x s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x. \<lbrakk>\<forall>cap. P cap \<longrightarrow> Q cap; ctes_of s slot = Some cte; P (cteCap cte); x \<in> cte_refs' (cteCap cte) (irq_node' s)\<rbrakk> \<Longrightarrow> \<exists>cref cte. ctes_of s cref = Some cte \<and> Q (cteCap cte) \<and> x \<in> cte_refs' (cteCap cte) (irq_node' s) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma rab_cap_to'[wp]:
  "\<lbrace>(\<lambda>s. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s))
              and K (\<forall>cap. isCNodeCap cap \<longrightarrow> P cap)\<rbrace>
     resolveAddressBits cap cref depth
   \<lbrace>\<lambda>rv s. ex_cte_cap_wp_to' P (fst rv) s\<rbrace>,-" apply (rule hoare_gen_asmE) apply (unfold validE_R_def) apply (rule use_spec, rule rab_cap_to'') apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)) and K (\<forall>cap. isCNodeCap cap \<longrightarrow> P cap)\<rbrace> CSpace_H.resolveAddressBits cap cref depth \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<forall>cap. isCNodeCap cap \<longrightarrow> P cap \<Longrightarrow> \<lbrace>\<lambda>s. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> CSpace_H.resolveAddressBits cap cref depth \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<forall>cap. isCNodeCap cap \<longrightarrow> P cap \<Longrightarrow> \<lbrace>\<lambda>s. isCNodeCap cap \<longrightarrow> (\<forall>r\<in>cte_refs' cap (irq_node' s). ex_cte_cap_wp_to' P r s)\<rbrace> CSpace_H.resolveAddressBits cap cref depth \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P (fst rv)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<forall>cap. isCNodeCap cap \<longrightarrow> P cap \<Longrightarrow> isCNodeCap cap \<longrightarrow> P cap proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma lookupCNode_cap_to'[wp]:
  "\<lbrace>\<lambda>s. \<forall>r\<in>cte_refs' rootCap (irq_node' s). ex_cte_cap_to' r s\<rbrace>
     lookupSlotForCNodeOp isSrc rootCap cref depth
   \<lbrace>\<lambda>p. ex_cte_cap_to' p\<rbrace>,-" apply (simp add: lookupSlotForCNodeOp_def Let_def split_def unlessE_def
             split del: if_split cong: if_cong) apply (rule hoare_pre) apply (wp hoare_drop_imps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r\<in>cte_refs' rootCap (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s\<rbrace> lookupSlotForCNodeOp isSrc rootCap cref depth \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>r\<in>cte_refs' rootCap (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s\<rbrace> if isCNodeCap rootCap then doE y <- rangeCheck depth (Suc 0) (size cref);
lookupErrorOnFailure isSrc (doE result <- CSpace_H.resolveAddressBits rootCap cref depth;
if snd result = 0 then returnOk (fst result) else throwError (Fault_H.lookup_failure.DepthMismatch (snd result) 0)
odE)
odE else throwError (Fault_H.syscall_error.FailedLookup isSrc Fault_H.lookup_failure.InvalidRoot) \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True)\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'7\<rbrace> if isCNodeCap rootCap then doE y <- rangeCheck depth (Suc 0) (size cref);
lookupErrorOnFailure isSrc (doE result <- CSpace_H.resolveAddressBits rootCap cref depth;
if snd result = 0 then returnOk (fst result) else throwError (Fault_H.lookup_failure.DepthMismatch (snd result) 0)
odE)
odE else throwError (Fault_H.syscall_error.FailedLookup isSrc Fault_H.lookup_failure.InvalidRoot) \<lbrace>ex_cte_cap_wp_to' (\<lambda>_. True)\<rbrace>, -
 2. \<And>s. \<forall>r\<in>cte_refs' rootCap (irq_node' s). ex_cte_cap_wp_to' (\<lambda>_. True) r s \<Longrightarrow> ?P'7 s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma badge_derived'_refl[simp]: "badge_derived' c c" by (simp add: badge_derived'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. badge_derived' c c
theory CSpace_R

lemma getSlotCap_wp:
  "\<lbrace>\<lambda>s.  (\<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<and> Q cap s)\<rbrace>
   getSlotCap p \<lbrace>Q\<rbrace>" apply (simp add: getSlotCap_def) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<and> Q cap s\<rbrace> getSlotCap p \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<and> Q cap s\<rbrace> do cte <- getCTE p;
return (cteCap cte)
od \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<exists>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<and> Q cap s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> Q (cteCap cte) s) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma storeWordUser_typ_at' :
  "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> storeWordUser v w \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>" unfolding storeWordUser_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> storeWordUser v w \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> do stateAssert (pointerInUserData v) [];
doMachineOp $ storeWord v w
od \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>
theory CSpace_R

lemma usableUntypedRange_mono2:
  "isUntypedCap cap
    \<Longrightarrow> isUntypedCap cap'
    \<Longrightarrow> capAligned cap \<Longrightarrow> capFreeIndex cap \<le> 2 ^ capBlockSize cap
    \<Longrightarrow> capFreeIndex cap' \<le> 2 ^ capBlockSize cap'
    \<Longrightarrow> capFreeIndex cap \<ge> capFreeIndex cap'
    \<Longrightarrow> capPtr cap' = capPtr cap
    \<Longrightarrow> capBlockSize cap' = capBlockSize cap
    \<Longrightarrow> usableUntypedRange cap \<le> usableUntypedRange cap'" apply (clarsimp simp only: isCap_simps capability.sel del: subsetI) apply (rule usableUntypedRange_mono1, auto simp: capAligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isUntypedCap cap; isUntypedCap cap'; capAligned cap; capFreeIndex cap \<le> 2 ^ capBlockSize cap; capFreeIndex cap' \<le> 2 ^ capBlockSize cap'; capFreeIndex cap' \<le> capFreeIndex cap; capPtr cap' = capPtr cap; capBlockSize cap' = capBlockSize cap\<rbrakk> \<Longrightarrow> usableUntypedRange cap \<subseteq> usableUntypedRange cap' proof (prove)
goal (1 subgoal):
 1. \<And>d da v0 v0a v1 v1a f fa. \<lbrakk>capAligned (capability.UntypedCap d v0 v1 f); f \<le> 2 ^ v1; fa \<le> 2 ^ v1; fa \<le> f; cap = capability.UntypedCap d v0 v1 f; cap' = capability.UntypedCap da v0 v1 fa\<rbrakk> \<Longrightarrow> usableUntypedRange (capability.UntypedCap d v0 v1 f) \<subseteq> usableUntypedRange (capability.UntypedCap da v0 v1 fa) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma ctes_of_cte_wpD:
  "ctes_of s p = Some cte \<Longrightarrow> cte_wp_at' ((=) cte) p s" by (simp add: cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctes_of s p = Some cte \<Longrightarrow> cte_wp_at' ((=) cte) p s
theory CSpace_R

lemma no_fail_getSlotCap:
  "no_fail (cte_at' p) (getSlotCap p)" apply (rule no_fail_pre) apply (simp add: getSlotCap_def | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (cte_wp_at' (\<lambda>_. True) p) (getSlotCap p) proof (prove)
goal (2 subgoals):
 1. no_fail ?P (getSlotCap p)
 2. \<And>s. cte_wp_at' (\<lambda>_. True) p s \<Longrightarrow> ?P s proof (prove)
goal:
No subgoals!
theory Move_R

lemma zip_map_rel:
  assumes "(x,y) \<in> set (zip xs ys)" "map f xs = map g ys"
  shows "f x = g y" using assms by (induct xs arbitrary: x y ys; cases ys) auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. f x = g y proof (prove)
using this:
(x, y) \<in> set (zip xs ys)
map f xs = map g ys

goal (1 subgoal):
 1. f x = g y
theory Move_R

lemma fold_K:
  "(P and (\<lambda> s. Q)) = (P and K Q)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (P and (\<lambda>s. Q)) = (P and K Q)
theory Move_R

lemma no_other_bits_set:
  "\<lbrakk> (w::'a::len word) && ~~ (2 ^ n) = 0 ; n' \<noteq> n ; n < size w ; n' < size w \<rbrakk>
   \<Longrightarrow>  \<not> w !! n'" by (fastforce dest!: word_eqD simp: word_ops_nth_size word_size nth_w2p)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>w && ~~ 2 ^ n = 0; n' \<noteq> n; n < size w; n' < size w\<rbrakk> \<Longrightarrow> \<not> w !! n'
theory Move_R

lemma mask_out_first_mask_some_eq:
  "\<lbrakk> x && ~~ mask n = y && ~~ mask n; n \<le> m \<rbrakk> \<Longrightarrow> x && ~~ mask m = y && ~~ mask m" apply (rule word_eqI, rename_tac n') apply (drule_tac x=n' in word_eqD) apply (auto simp: word_ops_nth_size word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>x && ~~ mask n = y && ~~ mask n; n \<le> m\<rbrakk> \<Longrightarrow> x && ~~ mask m = y && ~~ mask m proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>x && ~~ mask n = y && ~~ mask n; n \<le> m\<rbrakk> \<Longrightarrow> n' < size (x && ~~ mask m) \<longrightarrow> (x && ~~ mask m) !! n' = (y && ~~ mask m) !! n' proof (prove)
goal (1 subgoal):
 1. \<And>n'. \<lbrakk>n \<le> m; (x && ~~ mask n) !! n' = (y && ~~ mask n) !! n'\<rbrakk> \<Longrightarrow> n' < size (x && ~~ mask m) \<longrightarrow> (x && ~~ mask m) !! n' = (y && ~~ mask m) !! n' proof (prove)
goal:
No subgoals!
theory Move_R

lemma unaligned_helper:
  "\<lbrakk>is_aligned x n; y\<noteq>0; y < 2 ^ n\<rbrakk> \<Longrightarrow> \<not> is_aligned (x + y) n" apply (simp (no_asm_simp) add: is_aligned_mask) apply (simp add: mask_add_aligned) apply (cut_tac mask_eq_iff_w2p[of n y], simp_all add: word_size) apply (rule ccontr) apply (simp add: not_less power_overflow word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y \<noteq> 0; y < 2 ^ n\<rbrakk> \<Longrightarrow> \<not> is_aligned (x + y) n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y \<noteq> 0; y < 2 ^ n\<rbrakk> \<Longrightarrow> x + y && mask n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y \<noteq> 0; y < 2 ^ n\<rbrakk> \<Longrightarrow> y && mask n \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y \<noteq> 0; y < 2 ^ n\<rbrakk> \<Longrightarrow> n < LENGTH('a) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x n; y \<noteq> 0; y < 2 ^ n; \<not> n < LENGTH('a)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Move_R

lemma hoare_vcg_if_lift3:
  "\<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow>
  \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (if P rv s then X rv else Y rv) s\<rbrace>" by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (P rv s \<longrightarrow> X rv s) \<and> (\<not> P rv s \<longrightarrow> Y rv s)\<rbrace> \<Longrightarrow> \<lbrace>R\<rbrace> f \<lbrace>\<lambda>rv s. (if P rv s then X rv else Y rv) s\<rbrace>
theory Move_R

lemma corres_if_r':
  "\<lbrakk> G' \<Longrightarrow> corres_underlying sr nf nf' r P P' a c; \<not>G' \<Longrightarrow> corres_underlying sr nf nf' r P Q' a d \<rbrakk>
   \<Longrightarrow> corres_underlying sr nf nf' r (P) (if G' then P' else Q')
                                     (a) (if G' then c  else d)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>G' \<Longrightarrow> corres_underlying sr nf nf' r P P' a c; \<not> G' \<Longrightarrow> corres_underlying sr nf nf' r P Q' a d\<rbrakk> \<Longrightarrow> corres_underlying sr nf nf' r P (if G' then P' else Q') a (if G' then c else d)
theory Move_R

lemma valid_corres_combined:
  assumes "valid P f Q"
  assumes "corres_underlying sr False nf' rr P P' f f'"
  assumes "valid (\<lambda>s'. \<exists>s. (s,s')\<in>sr \<and> P s \<and> P' s') f' Q'" (is "valid ?P _ _")
  shows "valid ?P f' (\<lambda>r' s'. \<exists>r s. (s,s') \<in> sr \<and> Q r s \<and> Q' r' s' \<and> rr r r')" using assms by (fastforce simp: valid_def corres_underlying_def split_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> sr \<and> P s \<and> P' s'\<rbrace> f' \<lbrace>\<lambda>r' s'. \<exists>r s. (s, s') \<in> sr \<and> Q r s \<and> Q' r' s' \<and> rr r r'\<rbrace> proof (prove)
using this:
\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>
corres_underlying sr False nf' rr P P' f f'
\<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> sr \<and> P s \<and> P' s'\<rbrace> f' \<lbrace>Q'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s'. \<exists>s. (s, s') \<in> sr \<and> P s \<and> P' s'\<rbrace> f' \<lbrace>\<lambda>r' s'. \<exists>r s. (s, s') \<in> sr \<and> Q r s \<and> Q' r' s' \<and> rr r r'\<rbrace>
theory Move_R

lemma next_child_child_set:
  "\<lbrakk>next_child slot (cdt_list s) = Some child; valid_list s\<rbrakk>
    \<Longrightarrow> child \<in> (case next_child slot (cdt_list s) of None \<Rightarrow> {} | Some n \<Rightarrow> {n})" by (simp add: next_child_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>next_child slot (cdt_list s) = Some child; valid_list s\<rbrakk> \<Longrightarrow> child \<in> (case next_child slot (cdt_list s) of None \<Rightarrow> {} | Some n \<Rightarrow> {n})
theory Move_R

lemma cap_delete_one_cur_tcb[wp]:
  "\<lbrace>\<lambda>s. cur_tcb s\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s. cur_tcb s\<rbrace>" apply (simp add: cur_tcb_def) apply (rule hoare_pre) apply wps apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cur_tcb\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_. cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. tcb_at (cur_thread s) s\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s. tcb_at (cur_thread s) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> cap_delete_one slot \<lbrace>\<lambda>_ s. tcb_at (cur_thread s) s\<rbrace>
 2. \<And>s. tcb_at (cur_thread s) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P3 prev_s\<rbrace> cap_delete_one slot \<lbrace>\<lambda>rv s'. tcb_at (cur_thread prev_s) prev_s\<rbrace>
 2. \<And>s. tcb_at (cur_thread s) s \<Longrightarrow> ?P3 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. tcb_at (cur_thread s) s \<Longrightarrow> tcb_at (cur_thread s) s proof (prove)
goal:
No subgoals!
theory Move_R

lemma check_active_irq_invs:
  "\<lbrace>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 \<rbrace>
   check_active_irq
   \<lbrace>\<lambda>_. invs and (ct_running or ct_idle) and valid_list and valid_sched
        and (\<lambda>s. scheduler_action s = resume_cur_thread)
        and (\<lambda>s. 0 < domain_time s) and valid_domain_list \<rbrace>" by (wpsimp simp: check_active_irq_def ct_in_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>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\<rbrace> check_active_irq \<lbrace>\<lambda>_. invs and (ct_running or ct_idle) and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list\<rbrace>
theory Move_R

lemma check_active_irq_invs_just_idle:
  "\<lbrace>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 \<rbrace>
   check_active_irq
   \<lbrace>\<lambda>_. invs and ct_idle and valid_list and valid_sched
        and (\<lambda>s. scheduler_action s = resume_cur_thread)
        and (\<lambda>s. 0 < domain_time s) and valid_domain_list \<rbrace>" by (wpsimp simp: check_active_irq_def ct_in_state_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>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\<rbrace> check_active_irq \<lbrace>\<lambda>_. invs and ct_idle and valid_list and valid_sched and (\<lambda>s. scheduler_action s = resume_cur_thread) and (\<lambda>s. 0 < domain_time s) and valid_domain_list\<rbrace>
theory Move_R

lemma caps_of_state_kheap_ekheap[simp]:
  "caps_of_state (kheap_update f (ekheap_update ef s))
     = caps_of_state (kheap_update f s)" apply (simp add: trans_state_update[symmetric] del: trans_state_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_of_state (kheap_update f (ekheap_update ef s)) = caps_of_state (kheap_update f s) proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma countLeadingZeros_word_clz[simp]:
  "countLeadingZeros w = word_clz w" unfolding countLeadingZeros_def word_clz_def by (simp add: to_bl_upt)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. countLeadingZeros w = word_clz w proof (prove)
goal (1 subgoal):
 1. (length \<circ> takeWhile Not \<circ> reverse \<circ> map ((!!) w) $ [0 .e. finiteBitSize w - 1]) = length (takeWhile Not (to_bl w))
theory TcbAcc_R

lemma wordLog2_word_log2[simp]:
  "wordLog2 = word_log2" apply (rule ext) unfolding wordLog2_def word_log2_def by (simp add: word_size wordBits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. wordLog2 = word_log2 proof (prove)
goal (1 subgoal):
 1. \<And>x. wordLog2 x = word_log2 x proof (prove)
goal (1 subgoal):
 1. \<And>x. finiteBitSize x - 1 - countLeadingZeros x = size x - 1 - word_clz x
theory TcbAcc_R

lemma getHighestPrio_def'[simp]:
  "getHighestPrio d = gets (lookupBitmapPriority d)" unfolding getHighestPrio_def gets_def by (fastforce simp: gets_def get_bind_apply lookupBitmapPriority_def bitmap_fun_defs)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. getHighestPrio d = gets (lookupBitmapPriority d) proof (prove)
goal (1 subgoal):
 1. do l1 <- getReadyQueuesL1Bitmap d;
l1index <- return (wordLog2 l1);
l1indexInverted <- return (invertL1Index l1index);
l2 <- getReadyQueuesL2Bitmap d l1indexInverted;
l2index <- return (wordLog2 l2);
return $ l1IndexToPrio l1index || fromIntegral l2index
od = do s <- get;
return (lookupBitmapPriority d s)
od
theory TcbAcc_R

lemma isHighestPrio_def':
  "isHighestPrio d p = gets (\<lambda>s. ksReadyQueuesL1Bitmap s d = 0 \<or> lookupBitmapPriority d s \<le> p)" unfolding isHighestPrio_def bitmap_fun_defs getHighestPrio_def' apply (rule ext) apply (clarsimp simp: gets_def bind_assoc return_def Nondet_Monad.bind_def get_def
                  split: if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isHighestPrio d p = gets (\<lambda>s. ksReadyQueuesL1Bitmap s d = 0 \<or> lookupBitmapPriority d s \<le> p) proof (prove)
goal (1 subgoal):
 1. do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
if l1 = 0 then return True else do hprio <- gets (lookupBitmapPriority d);
return (hprio \<le> p)
od
od = gets (\<lambda>s. ksReadyQueuesL1Bitmap s d = 0 \<or> lookupBitmapPriority d s \<le> p) proof (prove)
goal (1 subgoal):
 1. \<And>x. (do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
if l1 = 0 then return True else do hprio <- gets (lookupBitmapPriority d);
return (hprio \<le> p)
od
od) x = gets (\<lambda>s. ksReadyQueuesL1Bitmap s d = 0 \<or> lookupBitmapPriority d s \<le> p) x proof (prove)
goal:
No subgoals!
theory TcbAcc_R

lemma getHighestPrio_inv[wp]:
  "\<lbrace> P \<rbrace> getHighestPrio d \<lbrace>\<lambda>_. P \<rbrace>" unfolding bitmap_fun_defs by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getHighestPrio d \<lbrace>\<lambda>_. P\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> getHighestPrio d \<lbrace>\<lambda>_. P\<rbrace>
theory TcbAcc_R

lemma valid_bitmapQ_bitmapQ_simp:
  "\<lbrakk> valid_bitmapQ s \<rbrakk> \<Longrightarrow>
   bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> [])" unfolding valid_bitmapQ_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_bitmapQ s \<Longrightarrow> bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> []) proof (prove)
goal (1 subgoal):
 1. \<forall>d p. bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> []) \<Longrightarrow> bitmapQ d p s = (ksReadyQueues s (d, p) \<noteq> [])