kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_C

lemma range_cover_bound3:
  "\<lbrakk>range_cover ptr sz us n; x < of_nat n\<rbrakk>
  \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> ptr + (of_nat n) * 2 ^ us - 1" apply (frule range_cover_subset[where p = "unat x"]) apply (simp add:unat_less_helper) apply (rule ccontr,simp) apply (drule(1) range_cover_subset_not_empty) apply (clarsimp simp: field_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> ptr + word_of_nat n * 2 ^ us - 1 proof (prove)
goal (3 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n\<rbrakk> \<Longrightarrow> unat x < n
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; {ptr + word_of_nat (unat x) * 2 ^ us..ptr + word_of_nat (unat x) * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> ptr + word_of_nat n * 2 ^ us - 1 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; {ptr + word_of_nat (unat x) * 2 ^ us..ptr + word_of_nat (unat x) * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> ptr + word_of_nat n * 2 ^ us - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; x < word_of_nat n; {ptr + word_of_nat (unat x) * 2 ^ us..ptr + word_of_nat (unat x) * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> ptr + word_of_nat n * 2 ^ us - 1 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us n; {ptr + word_of_nat (unat x) * 2 ^ us..ptr + word_of_nat (unat x) * 2 ^ us + 2 ^ us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ us - 1}; {ptr + x * 2 ^ us..ptr + x * 2 ^ us + 2 ^ us - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> ptr + x * 2 ^ us + 2 ^ us - 1 \<le> ptr + word_of_nat n * 2 ^ us - 1 proof (prove)
goal:
No subgoals!
theory Retype_C

lemma APIType_capBits_min:
  "(tp = APIObjectType apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> userSize)
    \<Longrightarrow> 4 \<le> APIType_capBits tp userSize" by (simp add: APIType_capBits_def objBits_simps' untypedBits_defs
         split: object_type.split ArchTypes_H.apiobject_type.split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. tp = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> minUntypedSizeBits \<le> userSize \<Longrightarrow> 4 \<le> APIType_capBits tp userSize
theory Retype_C

lemma byte_regions_unmodified_flip_eq:
  "byte_regions_unmodified hrs' hrs
    \<Longrightarrow> hrs_htd hrs' = hrs_htd hrs
    \<Longrightarrow> byte_regions_unmodified hrs hrs'" by (simp add: byte_regions_unmodified_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>byte_regions_unmodified hrs' hrs; hrs_htd hrs' = hrs_htd hrs\<rbrakk> \<Longrightarrow> byte_regions_unmodified hrs hrs'
theory Retype_C

lemma insertNewCap_preserves_bytes_flip:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call insertNewCap_'proc
      {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
         \<and> byte_regions_unmodified' t s}" by (rule allI, rule conseqPost, rule insertNewCap_preserves_bytes[rule_format])
     (auto elim: byte_regions_unmodified_flip_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call insertNewCap_'proc \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<acute>t_hrs \<^bsup>s\<^esup>t_hrs\<rbrace>
theory Retype_C

lemma cleanByVA_PoU_preserves_bytes:
  "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanByVA_PoU_'proc
      {t. hrs_htd (t_hrs_' (globals t)) = hrs_htd (t_hrs_' (globals s))
         \<and> byte_regions_unmodified' s t}" apply (rule allI, rule conseqPost, rule cleanByVA_PoU_preserves_kernel_bytes[rule_format]; simp) apply (clarsimp simp: byte_regions_unmodified_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} Call cleanByVA_PoU_'proc \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> (\<forall>x. (\<exists>a b. snd (hrs_htd \<^bsup>s\<^esup>t_hrs x) 0 = Some (a, b)) \<longrightarrow> hrs_mem \<acute>t_hrs x = hrs_mem \<^bsup>s\<^esup>t_hrs x)\<rbrace> \<subseteq> \<lbrace>hrs_htd \<acute>t_hrs = hrs_htd \<^bsup>s\<^esup>t_hrs \<and> byte_regions_unmodified \<^bsup>s\<^esup>t_hrs \<acute>t_hrs\<rbrace> proof (prove)
goal:
No subgoals!
theory Retype_C

lemma hrs_htd_update_canon:
  "hrs_htd_update (\<lambda>_. f (hrs_htd hrs)) hrs = hrs_htd_update f hrs" by (cases hrs, simp add: hrs_htd_update_def hrs_htd_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hrs_htd_update (\<lambda>_. f (hrs_htd hrs)) hrs = hrs_htd_update f hrs
theory Retype_C

lemma ptr_arr_retyps_eq_outside_dom:
  "x \<notin> {ptr_val (p :: 'a ptr) ..+ n * size_of TYPE ('a :: wf_type)}
    \<Longrightarrow> ptr_arr_retyps n p htd x = htd x" by (simp add: ptr_arr_retyps_def htd_update_list_same2)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> {ptr_val p..+n * size_of TYPE('a)} \<Longrightarrow> ptr_arr_retyps n p htd x = htd x
theory Recycle_C

lemma collapse_foldl_replicate:
  "replicate (length xs) v = xs \<Longrightarrow>
   foldl (@) [] (map (\<lambda>_. xs) ys)
        = replicateHider (length xs * length ys) v" apply (induct ys rule: rev_induct) apply (simp add: replicateHider_def) apply (simp add: replicateHider_def) apply (subst add.commute, simp add: replicate_add) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. replicate (length xs) v = xs \<Longrightarrow> foldl (@) [] (map (\<lambda>_. xs) ys) = replicateHider (length xs * length ys) v proof (prove)
goal (2 subgoals):
 1. replicate (length xs) v = xs \<Longrightarrow> foldl (@) [] (map (\<lambda>_. xs) []) = replicateHider (length xs * length []) v
 2. \<And>x xsa. \<lbrakk>replicate (length xs) v = xs \<Longrightarrow> foldl (@) [] (map (\<lambda>_. xs) xsa) = replicateHider (length xs * length xsa) v; replicate (length xs) v = xs\<rbrakk> \<Longrightarrow> foldl (@) [] (map (\<lambda>_. xs) (xsa @ [x])) = replicateHider (length xs * length (xsa @ [x])) v proof (prove)
goal (1 subgoal):
 1. \<And>x xsa. \<lbrakk>replicate (length xs) v = xs \<Longrightarrow> foldl (@) [] (map (\<lambda>_. xs) xsa) = replicateHider (length xs * length xsa) v; replicate (length xs) v = xs\<rbrakk> \<Longrightarrow> foldl (@) [] (map (\<lambda>_. xs) (xsa @ [x])) = replicateHider (length xs * length (xsa @ [x])) v proof (prove)
goal (1 subgoal):
 1. \<And>xsa. \<lbrakk>foldl (@) [] (map (\<lambda>_. xs) xsa) = replicate (length xs * length xsa) v; replicate (length xs) v = xs\<rbrakk> \<Longrightarrow> replicate (length xs * length xsa) v @ xs = replicate (length xs + length xs * length xsa) v proof (prove)
goal:
No subgoals!
theory Recycle_C

lemma help_force_intvl_range_conv:
  "\<lbrakk> is_aligned (p::word32) n; v = 2 ^ n; n < word_bits \<rbrakk>
    \<Longrightarrow> {p ..+ v} = {p .. p + 2 ^ n - 1}" by (simp add: intvl_range_conv word_bits_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; v = 2 ^ n; n < word_bits\<rbrakk> \<Longrightarrow> {p..+v} = {p..p + 2 ^ n - 1}
theory Recycle_C

lemma flex_user_data_at_rf_sr_dom_s:
  "\<lbrakk> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits).
         typ_at' UserDataT (x + p * 2 ^ pageBits) s); (s, s') \<in> rf_sr \<rbrakk>
    \<Longrightarrow> {x ..+ 2 ^ pageBitsForSize sz} \<times> {SIndexVal, SIndexTyp 0}
    \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))" apply (rule_tac m=pageBits in intvl_2_power_times_decomp,
         simp_all add: pbfs_atleast_pageBits pbfs_less_wb') apply (erule allEI, clarsimp) apply (drule(1) user_data_at_rf_sr_dom_s) apply (erule subsetD) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' UserDataT (x + p * 2 ^ pageBits) s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> {x..+2 ^ pageBitsForSize sz} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' UserDataT (x + p * 2 ^ pageBits) s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<forall>y<2 ^ (pageBitsForSize sz - pageBits). {x + y * 2 ^ pageBits..+2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y a b. \<lbrakk>(s, s') \<in> rf_sr; y < 2 ^ (pageBitsForSize sz - pageBits); a \<in> {x + y * 2 ^ pageBits..+2 ^ pageBits}; b = SIndexVal \<or> b = SIndexTyp 0; typ_at' UserDataT (x + y * 2 ^ pageBits) s\<rbrakk> \<Longrightarrow> (a, b) \<in> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y a b. \<lbrakk>(s, s') \<in> rf_sr; y < 2 ^ (pageBitsForSize sz - pageBits); a \<in> {x + y * 2 ^ pageBits..+2 ^ pageBits}; b = SIndexVal \<or> b = SIndexTyp 0; {x + y * 2 ^ pageBits..+2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} \<subseteq> dom_s (hrs_htd (t_hrs_' (globals s')))\<rbrakk> \<Longrightarrow> (a, b) \<in> dom_s (hrs_htd (t_hrs_' (globals s'))) proof (prove)
goal (1 subgoal):
 1. \<And>y a b. \<lbrakk>(s, s') \<in> rf_sr; y < 2 ^ (pageBitsForSize sz - pageBits); a \<in> {x + y * 2 ^ pageBits..+2 ^ pageBits}; b = SIndexVal \<or> b = SIndexTyp 0\<rbrakk> \<Longrightarrow> (a, b) \<in> {x + y * 2 ^ pageBits..+2 ^ pageBits} \<times> {SIndexVal, SIndexTyp 0} proof (prove)
goal:
No subgoals!
theory Recycle_C

lemma hrs_mem_update_fold_eq:
  "hrs_mem_update (fold f xs)
    = fold (hrs_mem_update o f) xs" apply (rule sym, induct xs) apply (simp add: hrs_mem_update_def) apply (simp add: hrs_mem_update_def fun_eq_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hrs_mem_update (fold f xs) = fold (hrs_mem_update \<circ> f) xs proof (prove)
goal (2 subgoals):
 1. fold (hrs_mem_update \<circ> f) [] = hrs_mem_update (fold f [])
 2. \<And>x1 xs. fold (hrs_mem_update \<circ> f) xs = hrs_mem_update (fold f xs) \<Longrightarrow> fold (hrs_mem_update \<circ> f) (x1 # xs) = hrs_mem_update (fold f (x1 # xs)) proof (prove)
goal (1 subgoal):
 1. \<And>x1 xs. fold (hrs_mem_update \<circ> f) xs = hrs_mem_update (fold f xs) \<Longrightarrow> fold (hrs_mem_update \<circ> f) (x1 # xs) = hrs_mem_update (fold f (x1 # xs)) proof (prove)
goal:
No subgoals!
theory Recycle_C

lemma coerce_memset_to_heap_update_pte:
  "heap_update_list x (replicateHider 4 0)
      = heap_update (Ptr x :: pte_C ptr)
             (pte_C.pte_C (FCP (\<lambda>x. 0)))" apply (intro ext, simp add: heap_update_def) apply (rule_tac f="\<lambda>xs. heap_update_list x xs a b" for a b in arg_cong) apply (simp add: to_bytes_def size_of_def typ_info_simps pte_C_tag_def) apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def
                   final_pad_def size_td_lt_ti_typ_pad_combine Let_def size_of_def) apply (simp add: typ_info_simps align_td_array' size_td_array) apply (simp add: typ_info_array' typ_info_word word_rsplit_0) apply (simp add: replicateHider_def word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update_list x (replicateHider 4 0) = heap_update (pte_Ptr x) (pte_C.pte_C (ARRAY x. 0)) proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. heap_update_list x (replicateHider 4 0) xa xaa = heap_update_list x (to_bytes (pte_C.pte_C (ARRAY x. 0)) (heap_list xa 4 x)) xa xaa proof (prove)
goal (1 subgoal):
 1. \<And>xa xaa. replicateHider 4 0 = to_bytes (pte_C.pte_C (ARRAY x. 0)) (heap_list xa 4 x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. replicateHider 4 0 = access_ti (final_pad (ti_typ_pad_combine TYPE(32 word[1]) pte_C.words_C (pte_C.words_C_update \<circ> (\<lambda>x _. x)) ''words_C'' (empty_typ_info ''pte_C''))) (pte_C.pte_C (ARRAY x. 0)) (heap_list xa 4 x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. replicateHider 4 0 = access_ti (if 0 < (2 ^ align_td (typ_info_t TYPE(32 word[1])) - size_td (typ_info_t TYPE(32 word[1])) mod 2 ^ align_td (typ_info_t TYPE(32 word[1]))) mod 2 ^ align_td (typ_info_t TYPE(32 word[1])) then ti_pad_combine ((2 ^ align_td (typ_info_t TYPE(32 word[1])) - size_td (typ_info_t TYPE(32 word[1])) mod 2 ^ align_td (typ_info_t TYPE(32 word[1]))) mod 2 ^ align_td (typ_info_t TYPE(32 word[1]))) (TypDesc (TypAggregate [DTPair (adjust_ti (typ_info_t TYPE(32 word[1])) pte_C.words_C (pte_C.words_C_update \<circ> (\<lambda>x _. x))) ''words_C'']) ''pte_C'') else TypDesc (TypAggregate [DTPair (adjust_ti (typ_info_t TYPE(32 word[1])) pte_C.words_C (pte_C.words_C_update \<circ> (\<lambda>x _. x))) ''words_C'']) ''pte_C'') (pte_C.pte_C (ARRAY x. 0)) (heap_list xa 4 x) proof (prove)
goal (1 subgoal):
 1. \<And>xa. replicateHider 4 0 = access_ti (typ_info_t TYPE(32 word[1])) (ARRAY x. 0) (heap_list xa 4 x) proof (prove)
goal (1 subgoal):
 1. replicateHider 4 0 = [0, 0, 0, 0] proof (prove)
goal:
No subgoals!
theory Recycle_C

lemma objBits_eq_by_type:
  fixes x :: "'a :: pspace_storable" and y :: 'a
  shows "objBits x = objBits y" apply (simp add: objBits_def) apply (rule objBits_type) apply (simp add: koTypeOf_injectKO) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. objBits x = objBits y proof (prove)
goal (1 subgoal):
 1. objBitsKO (injectKOS x) = objBitsKO (injectKOS y) proof (prove)
goal (1 subgoal):
 1. koTypeOf (injectKOS x) = koTypeOf (injectKOS y) proof (prove)
goal:
No subgoals!
theory Recycle_C

lemma option_to_0_user_mem':
  "option_to_0 \<circ> user_mem' as =(\<lambda>x. if x \<in> {y. \<not> pointerInUserData y as} then 0
  else underlying_memory (ksMachineState as) x) " apply (rule ext) apply (simp add:user_mem'_def option_to_0_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. option_to_0 \<circ> user_mem' as = (\<lambda>x. if x \<in> {y. \<not> pointerInUserData y as} then 0 else underlying_memory (ksMachineState as) x) proof (prove)
goal (1 subgoal):
 1. \<And>x. (option_to_0 \<circ> user_mem' as) x = (if x \<in> {y. \<not> pointerInUserData y as} then 0 else underlying_memory (ksMachineState as) x) proof (prove)
goal:
No subgoals!
theory Recycle_C

lemma modify_gets_helper:
  "do y \<leftarrow> modify (ksPSpace_update (\<lambda>_. ps)); ps' \<leftarrow> gets ksPSpace; f ps' od
      = do y \<leftarrow> modify (ksPSpace_update (\<lambda>_. ps)); f ps od" by (simp add: bind_def simpler_modify_def simpler_gets_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do y <- modify (ksPSpace_update (\<lambda>_. ps));
gets ksPSpace >>= f
od = do y <- modify (ksPSpace_update (\<lambda>_. ps));
f ps
od
theory Recycle_C

lemma snd_lookupAround2_update:
  "ps y \<noteq> None \<Longrightarrow>
    snd (lookupAround2 x (ps (y \<mapsto> v'))) = snd (lookupAround2 x ps)" apply (clarsimp simp: lookupAround2_def lookupAround_def Let_def
                        dom_fun_upd2
              simp del: dom_fun_upd cong: if_cong option.case_cong) apply (clarsimp split: option.split if_split  cong: if_cong) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ps y \<noteq> None \<Longrightarrow> snd (lookupAround2 x (ps(y \<mapsto> v'))) = snd (lookupAround2 x ps) proof (prove)
goal (1 subgoal):
 1. \<And>ya. ps y = Some ya \<Longrightarrow> snd (case if x = y then Some v' else ps x of None \<Rightarrow> (if \<forall>xa. xa \<in> dom ps \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom ps. k < x}, the (if Max {k \<in> dom ps. k < x} = y then Some v' else ps (Max {k \<in> dom ps. k < x}))), case if \<forall>xa. xa \<in> dom ps \<longrightarrow> \<not> x < xa then None else Some (Min {k \<in> dom ps. x < k}, the (if Min {k \<in> dom ps. k < x} = y then Some v' else ps (Min {k \<in> dom ps. k < x}))) of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2)) | Some v \<Rightarrow> (Some (x, v), case if \<forall>xa. xa \<in> dom ps \<longrightarrow> \<not> x < xa then None else Some (Min {k \<in> dom ps. x < k}, the (if Min {k \<in> dom ps. k < x} = y then Some v' else ps (Min {k \<in> dom ps. k < x}))) of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2))) = snd (case ps x of None \<Rightarrow> (if \<forall>xa. xa \<in> dom ps \<longrightarrow> \<not> xa < x then None else Some (Max {k \<in> dom ps. k < x}, the (ps (Max {k \<in> dom ps. k < x}))), case if \<forall>xa. xa \<in> dom ps \<longrightarrow> \<not> x < xa then None else Some (Min {k \<in> dom ps. x < k}, the (ps (Min {k \<in> dom ps. k < x}))) of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2)) | Some v \<Rightarrow> (Some (x, v), case if \<forall>xa. xa \<in> dom ps \<longrightarrow> \<not> x < xa then None else Some (Min {k \<in> dom ps. x < k}, the (ps (Min {k \<in> dom ps. k < x}))) of None \<Rightarrow> None | Some x2 \<Rightarrow> Some (fst x2))) proof (prove)
goal (1 subgoal):
 1. \<And>ya. ps y = Some ya \<Longrightarrow> ((\<forall>xa. xa \<in> dom ps \<longrightarrow> \<not> x < xa) \<longrightarrow> (\<exists>xa. xa \<in> dom ps \<and> x < xa) \<longrightarrow> (\<exists>y. ps x = Some y) \<and> ps x = None) \<and> ((\<exists>xa. xa \<in> dom ps \<and> x < xa) \<longrightarrow> (\<forall>xa. xa \<in> dom ps \<longrightarrow> \<not> x < xa) \<longrightarrow> (\<exists>y. ps x = Some y) \<and> ps x = None) proof (prove)
goal:
No subgoals!
theory Recycle_C

lemma ccorres_inst_voodoo:
  "\<forall>x. ccorres r xf (P x) (P' x) hs (h x) (c x)
     \<Longrightarrow> \<forall>x. ccorres r xf (P x) (P' x) hs (h x) (c x)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>x. ccorres r xf (P x) (P' x) hs (h x) (c x) \<Longrightarrow> \<forall>x. ccorres r xf (P x) (P' x) hs (h x) (c x)
theory Recycle_C

lemma cnotification_relation_q_cong:
  "\<lbrakk>\<And>t rf. (t, rf) \<in> ntfn_q_refs_of' (ntfnObj ntfn) \<Longrightarrow>  hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t)\<rbrakk>
      \<Longrightarrow>  cnotification_relation hp ntfn ntfn' = cnotification_relation hp' ntfn ntfn'" apply (cases "ntfnObj ntfn", simp_all add: cnotification_relation_def Let_def) apply (auto intro: iffD1[OF tcb_queue_relation'_cong[OF refl refl refl]]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>t rf. (t, rf) \<in> ntfn_q_refs_of' (ntfnObj ntfn) \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t)) \<Longrightarrow> cnotification_relation hp ntfn ntfn' = cnotification_relation hp' ntfn ntfn' proof (prove)
goal (1 subgoal):
 1. \<And>x3. \<lbrakk>\<And>t. t \<in> set x3 \<Longrightarrow> hp (tcb_ptr_to_ctcb_ptr t) = hp' (tcb_ptr_to_ctcb_ptr t); ntfnObj ntfn = Structures_H.ntfn.WaitingNtfn x3\<rbrakk> \<Longrightarrow> (notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' hp x3 (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift ntfn'))) = (notification_CL.state_CL (notification_lift ntfn') = SCAST(32 signed \<rightarrow> 32) NtfnState_Waiting \<and> ep_queue_relation' hp' x3 (tcb_Ptr (ntfnQueue_head_CL (notification_lift ntfn'))) (tcb_Ptr (ntfnQueue_tail_CL (notification_lift ntfn'))) \<and> option_to_ctcb_ptr (ntfnBoundTCB ntfn) = tcb_Ptr (ntfnBoundTCB_CL (notification_lift ntfn'))) proof (prove)
goal:
No subgoals!
theory Recycle_C

lemma tcbSchedEnqueue_ep_at:
  "\<lbrace>obj_at' (P :: endpoint \<Rightarrow> bool) ep\<rbrace>
      tcbSchedEnqueue t
   \<lbrace>\<lambda>rv. obj_at' P ep\<rbrace>" including no_pre apply (simp add: tcbSchedEnqueue_def unless_def null_def) apply (wp threadGet_wp, clarsimp, wp+) apply (clarsimp split: if_split, wp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P ep\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>rv. obj_at' P ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P ep\<rbrace> tcbSchedEnqueue t \<lbrace>\<lambda>rv. obj_at' P ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P ep\<rbrace> do queued <- threadGet tcbQueued t;
when (\<not> queued) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (t # queue);
y <- when (queue = []) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
od \<lbrace>\<lambda>rv. obj_at' P ep\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>obj_at' P ep\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then obj_at' P ep else obj_at' P ep\<rbrace> proof (prove)
goal:
No subgoals!
theory Recycle_C

lemma ccorres_duplicate_guard:
  "ccorres r xf (P and P) Q hs f f' \<Longrightarrow> ccorres r xf P Q hs f f'" by (erule ccorres_guard_imp, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (P and P) Q hs f f' \<Longrightarrow> ccorres r xf P Q hs f f'
theory Recycle_C

lemma ep_q_refs'_no_NTFNBound[simp]:
  "(x, NTFNBound) \<notin> ep_q_refs_of' ep" by (auto simp: ep_q_refs_of'_def split: endpoint.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, NTFNBound) \<notin> ep_q_refs_of' ep
theory Recycle_C

lemma ntfn_q_refs'_no_NTFNBound[simp]:
  "(x, NTFNBound) \<notin> ntfn_q_refs_of' ntfn" by (auto simp: ntfn_q_refs_of'_def split: ntfn.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (x, NTFNBound) \<notin> ntfn_q_refs_of' ntfn
theory Recycle_C

lemma cte_lift_ccte_relation:
  "cte_lift cte' = Some ctel'
    \<Longrightarrow> c_valid_cte cte'
    \<Longrightarrow> ccte_relation (cte_to_H ctel') cte'" by (simp add: ccte_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_lift cte' = Some ctel'; c_valid_cte cte'\<rbrakk> \<Longrightarrow> ccte_relation (cte_to_H ctel') cte'
theory Recycle_C

lemma ccap_relation_isDeviceCap2:
 "\<lbrakk>ccap_relation cp cap; isUntypedCap cp
  \<rbrakk> \<Longrightarrow> (capIsDevice_CL (cap_untyped_cap_lift cap) = 0) = (\<not> (capIsDevice cp))" apply (frule cap_get_tag_UntypedCap) apply (simp add:cap_get_tag_isCap to_bool_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cp cap; isUntypedCap cp\<rbrakk> \<Longrightarrow> (capIsDevice_CL (cap_untyped_cap_lift cap) = 0) = (\<not> capIsDevice cp) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cp cap; isUntypedCap cp; (cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_untyped_cap) = (cp = capability.UntypedCap (to_bool (capIsDevice_CL (cap_untyped_cap_lift cap))) (capPtr_CL (cap_untyped_cap_lift cap)) (unat (capBlockSize_CL (cap_untyped_cap_lift cap))) (unat (capFreeIndex_CL (cap_untyped_cap_lift cap) << 4)))\<rbrakk> \<Longrightarrow> (capIsDevice_CL (cap_untyped_cap_lift cap) = 0) = (\<not> capIsDevice cp) proof (prove)
goal:
No subgoals!