kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_C

lemma size_td_map_list:
  "size_td_list (map (\<lambda>n. DTPair
                                 (adjust_ti (typ_info_t TYPE('a :: c_type))
                                   (\<lambda>x. index x n)
                                   (\<lambda>x f. Arrays.update f n x))
                                 (replicate n CHR ''1''))
                        [0..<n]) = (size_td (typ_info_t TYPE('a :: c_type)) * n)" apply (induct n) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. size_td_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<n]) = size_td (typ_info_t TYPE('a)) * n proof (prove)
goal (2 subgoals):
 1. size_td_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<0]) = size_td (typ_info_t TYPE('a)) * 0
 2. \<And>n. size_td_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<n]) = size_td (typ_info_t TYPE('a)) * n \<Longrightarrow> size_td_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<Suc n]) = size_td (typ_info_t TYPE('a)) * Suc n proof (prove)
goal (1 subgoal):
 1. \<And>n. size_td_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<n]) = size_td (typ_info_t TYPE('a)) * n \<Longrightarrow> size_td_list (map (\<lambda>n. DTPair (adjust_ti (typ_info_t TYPE('a)) (\<lambda>x. x.[n]) (\<lambda>x f. Arrays.update f n x)) (replicate n CHR ''1'')) [0..<Suc n]) = size_td (typ_info_t TYPE('a)) * Suc n proof (prove)
goal:
No subgoals!
theory Retype_C

lemma update_ti_t_array_rep:
  "bs = replicate ((card (UNIV :: 'b :: finite set)) * size_td (typ_info_t TYPE('a))) v \<Longrightarrow>
  update_ti_t (typ_info_t TYPE('a :: c_type['b :: finite])) bs x =
  foldr (\<lambda>n arr. Arrays.update arr n
        (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (index arr n)))
        [0..<(card (UNIV :: 'b :: finite set))] x" unfolding typ_info_array array_tag_def apply (rule update_ti_t_array_tag_n_rep) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bs = replicate (CARD('b) * size_td (typ_info_t TYPE('a))) v \<Longrightarrow> update_ti_t (typ_info_t TYPE('a['b])) bs x = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<CARD('b)] x proof (prove)
goal (1 subgoal):
 1. bs = replicate (CARD('b) * size_td (typ_info_t TYPE('a))) v \<Longrightarrow> update_ti_t (array_tag_n CARD('b)) bs x = foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE('a)) (replicate (size_td (typ_info_t TYPE('a))) v) (arr.[n]))) [0..<CARD('b)] x proof (prove)
goal (2 subgoals):
 1. bs = replicate (CARD('b) * size_td (typ_info_t TYPE('a))) v \<Longrightarrow> bs = replicate (CARD('b) * size_td (typ_info_t TYPE('a))) v
 2. bs = replicate (CARD('b) * size_td (typ_info_t TYPE('a))) v \<Longrightarrow> CARD('b) \<le> CARD('b) proof (prove)
goal (1 subgoal):
 1. bs = replicate (CARD('b) * size_td (typ_info_t TYPE('a))) v \<Longrightarrow> CARD('b) \<le> CARD('b) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma update_ti_t_array_rep_word0:
  "bs = replicate ((card (UNIV :: 'b :: finite set)) * 4) 0 \<Longrightarrow>
  update_ti_t (typ_info_t TYPE(word32['b :: finite])) bs x =
  foldr (\<lambda>n arr. Arrays.update arr n 0)
        [0..<(card (UNIV :: 'b :: finite set))] x" apply (subst update_ti_t_array_rep) apply simp apply (simp add: update_ti_t_word32_0s) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. bs = replicate (CARD('b) * 4) 0 \<Longrightarrow> update_ti_t (typ_info_t TYPE(32 word['b])) bs x = foldr (\<lambda>n arr. Arrays.update arr n 0) [0..<CARD('b)] x proof (prove)
goal (2 subgoals):
 1. bs = replicate (CARD('b) * 4) 0 \<Longrightarrow> bs = replicate (CARD('b) * size_td (typ_info_t TYPE(32 word))) ?v
 2. bs = replicate (CARD('b) * 4) 0 \<Longrightarrow> foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE(32 word)) (replicate (size_td (typ_info_t TYPE(32 word))) ?v) (arr.[n]))) [0..<CARD('b)] x = foldr (\<lambda>n arr. Arrays.update arr n 0) [0..<CARD('b)] x proof (prove)
goal (1 subgoal):
 1. bs = replicate (CARD('b) * 4) 0 \<Longrightarrow> foldr (\<lambda>n arr. Arrays.update arr n (update_ti_t (typ_info_t TYPE(32 word)) (replicate (size_td (typ_info_t TYPE(32 word))) 0) (arr.[n]))) [0..<CARD('b)] x = foldr (\<lambda>n arr. Arrays.update arr n 0) [0..<CARD('b)] x proof (prove)
goal:
No subgoals!
theory Retype_C

lemma tcb_queue_update_other':
  "\<lbrakk> ctcb_ptr_to_tcb_ptr p \<notin> set tcbs \<rbrakk> \<Longrightarrow>
  tcb_queue_relation' next prev (mp(p \<mapsto> v)) tcbs qe qh =
  tcb_queue_relation' next prev mp tcbs qe qh" unfolding tcb_queue_relation'_def by (simp add: tcb_queue_update_other)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr p \<notin> set tcbs \<Longrightarrow> tcb_queue_relation' next prev (mp(p \<mapsto> v)) tcbs qe qh = tcb_queue_relation' next prev mp tcbs qe qh proof (prove)
goal (1 subgoal):
 1. ctcb_ptr_to_tcb_ptr p \<notin> set tcbs \<Longrightarrow> (qh = (if tcbs = [] then NULL else tcb_ptr_to_ctcb_ptr (last tcbs)) \<and> tcb_queue_relation next prev (mp(p \<mapsto> v)) tcbs NULL qe) = (qh = (if tcbs = [] then NULL else tcb_ptr_to_ctcb_ptr (last tcbs)) \<and> tcb_queue_relation next prev mp tcbs NULL qe)
theory Retype_C

lemma tcb_ptr_orth_cte_ptrs':
  "ptr_span (tcb_Ptr (regionBase + 0x100)) \<inter> ptr_span (Ptr regionBase :: (cte_C[5]) ptr) = {}" apply (rule disjointI) apply (clarsimp simp: ctcb_ptr_to_tcb_ptr_def size_td_array
                        intvl_def field_simps size_of_def ctcb_offset_def) apply (simp add: unat_arith_simps unat_of_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_span (tcb_Ptr (regionBase + 0x100)) \<inter> ptr_span (PTR(cte_C[5]) regionBase) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>x \<in> ptr_span (tcb_Ptr (regionBase + 0x100)); y \<in> ptr_span (PTR(cte_C[5]) regionBase)\<rbrakk> \<Longrightarrow> x \<noteq> y proof (prove)
goal (1 subgoal):
 1. \<And>k ka. \<lbrakk>k < 152; ka < 80; word_of_nat k + 0x100 = word_of_nat ka\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory Retype_C

lemma ps_clear_subset:
  assumes pd: "ps_clear x (objBitsKO ko) (s' \<lparr>ksPSpace := (\<lambda>x. if x \<in> as then Some (f x) else ksPSpace s' x) \<rparr>)"
  and    sub: "as' \<subseteq> as"
  and     al: "is_aligned x (objBitsKO ko)"
  shows  "ps_clear x (objBitsKO ko) (s' \<lparr>ksPSpace := (\<lambda>x. if x \<in> as' then Some (f x) else ksPSpace s' x) \<rparr>)" using al pd sub apply - apply (simp add: ps_clear_def3 [OF al objBitsKO_gt_0] dom_if_Some) apply (erule disjoint_subset2 [rotated]) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> as' then Some (f x) else ksPSpace s' x\<rparr>) proof (prove)
using this:
is_aligned x (objBitsKO ko)
ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> as then Some (f x) else ksPSpace s' x\<rparr>)
as' \<subseteq> as

goal (1 subgoal):
 1. ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> as' then Some (f x) else ksPSpace s' x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x (objBitsKO ko); ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> as then Some (f x) else ksPSpace s' x\<rparr>); as' \<subseteq> as\<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO ko) (s'\<lparr>ksPSpace := \<lambda>x. if x \<in> as' then Some (f x) else ksPSpace s' x\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x (objBitsKO ko); {x + 1..x + 2 ^ objBitsKO ko - 1} \<inter> (as \<union> dom (ksPSpace s')) = {}; as' \<subseteq> as\<rbrakk> \<Longrightarrow> {x + 1..x + 2 ^ objBitsKO ko - 1} \<inter> (as' \<union> dom (ksPSpace s')) = {} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned x (objBitsKO ko); as' \<subseteq> as\<rbrakk> \<Longrightarrow> as' \<union> dom (ksPSpace s') \<subseteq> as \<union> dom (ksPSpace s') proof (prove)
goal:
No subgoals!
theory Retype_C

lemma heap_list_eq_replicate_eq_eq:
  "(heap_list hp n ptr = replicate n v)
    = (\<forall>p \<in> {ptr ..+ n}. hp p = v)" by (induct n arbitrary: ptr, simp_all add: intvl_Suc_right)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (heap_list hp n ptr = replicate n v) = (\<forall>p\<in>{ptr..+n}. hp p = v)
theory Retype_C

lemma heap_update_list_replicate_eq:
  "(heap_update_list x (replicate n v) hp y)
    = (if y \<in> {x ..+ n} then v else hp y)" apply (induct n arbitrary: x hp, simp_all add: intvl_Suc_right) apply (simp split: if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. heap_update_list x (replicate n v) hp y = (if y \<in> {x..+n} then v else hp y) proof (prove)
goal (1 subgoal):
 1. \<And>n x hp. (\<And>x hp. heap_update_list x (replicate n v) hp y = (if y \<in> {x..+n} then v else hp y)) \<Longrightarrow> (if y \<in> {x + 1..+n} then v else (hp(x := v)) y) = (if y = x \<or> y \<in> {x + 1..+n} then v else hp y) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma zero_ranges_are_zero_update_zero[simp]:
  "zero_ranges_are_zero rs hrs
    \<Longrightarrow> zero_ranges_are_zero rs (hrs_mem_update (heap_update_list ptr (replicate n 0)) hrs)" apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update) apply (drule(1) bspec) apply (clarsimp simp: heap_list_eq_replicate_eq_eq heap_update_list_replicate_eq cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. zero_ranges_are_zero rs hrs \<Longrightarrow> zero_ranges_are_zero rs (hrs_mem_update (heap_update_list ptr (replicate n 0)) hrs) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>rs. case x of (start, end) \<Rightarrow> region_actually_is_bytes' start (unat (end + 1 - start)) (hrs_htd hrs) \<and> heap_list (hrs_mem hrs) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0; (a, b) \<in> rs\<rbrakk> \<Longrightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd hrs) \<and> heap_list (heap_update_list ptr (replicate n 0) (hrs_mem hrs)) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>(a, b) \<in> rs; case (a, b) of (start, end) \<Rightarrow> region_actually_is_bytes' start (unat (end + 1 - start)) (hrs_htd hrs) \<and> heap_list (hrs_mem hrs) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0\<rbrakk> \<Longrightarrow> region_actually_is_bytes' a (unat (b + 1 - a)) (hrs_htd hrs) \<and> heap_list (heap_update_list ptr (replicate n 0) (hrs_mem hrs)) (unat (b + 1 - a)) a = replicate (unat (b + 1 - a)) 0 proof (prove)
goal:
No subgoals!
theory Retype_C

lemma rf_sr_rep0:
  assumes sr: "(\<sigma>, x) \<in> rf_sr"
  assumes empty: "region_is_bytes ptr sz x"
  shows "(\<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list ptr (replicate sz 0)))) x) \<in> rf_sr" using sr by (clarsimp simp add: rf_sr_def cstate_relation_def Let_def cpspace_relation_def
        carch_state_relation_def cmachine_state_relation_def
        cslift_bytes_mem_update[OF empty, simplified] cte_C_size)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list ptr (replicate sz 0)))) x) \<in> rf_sr proof (prove)
using this:
(\<sigma>, x) \<in> rf_sr

goal (1 subgoal):
 1. (\<sigma>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update_list ptr (replicate sz 0)))) x) \<in> rf_sr
theory Retype_C

lemma range_cover_bound_weak:
  "\<lbrakk> n \<noteq> 0; range_cover ptr sz us n \<rbrakk> \<Longrightarrow>
    ptr + (of_nat n * 2 ^ us - 1) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1" apply (frule range_cover_cell_subset[where x = "of_nat (n - 1)"]) apply (simp add:range_cover_not_zero) apply (frule range_cover_subset_not_empty[rotated,where x = "of_nat (n - 1)"]) apply (simp add:range_cover_not_zero) apply (clarsimp simp: field_simps) done

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

lemma pageBitsForSize_mess_multi:
  "4 * (2::nat) ^ (pageBitsForSize sz - 2) = 2^(pageBitsForSize sz)" apply (subgoal_tac "(4 :: nat) = 2 ^ 2") apply (erule ssubst) apply (subst power_add [symmetric]) apply (rule arg_cong [where f = "\<lambda>n. 2 ^ n"]) apply (case_tac sz,simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. 4 * 2 ^ (pageBitsForSize sz - 2) = 2 ^ pageBitsForSize sz proof (prove)
goal (2 subgoals):
 1. 4 = 2\<^sup>2 \<Longrightarrow> 4 * 2 ^ (pageBitsForSize sz - 2) = 2 ^ pageBitsForSize sz
 2. 4 = 2\<^sup>2 proof (prove)
goal (2 subgoals):
 1. 2\<^sup>2 * 2 ^ (pageBitsForSize sz - 2) = 2 ^ pageBitsForSize sz
 2. 4 = 2\<^sup>2 proof (prove)
goal (2 subgoals):
 1. 2 ^ (2 + (pageBitsForSize sz - 2)) = 2 ^ pageBitsForSize sz
 2. 4 = 2\<^sup>2 proof (prove)
goal (2 subgoals):
 1. 2 + (pageBitsForSize sz - 2) = pageBitsForSize sz
 2. 4 = 2\<^sup>2 proof (prove)
goal:
No subgoals!
theory Retype_C

lemma valid_pde_mappings_ko_atD':
  "\<lbrakk> ko_at' ko p s; valid_pde_mappings' s \<rbrakk>
       \<Longrightarrow> ko_at' ko p s \<and> valid_pde_mapping' (p && mask pdBits) ko" by (simp add: valid_pde_mappings'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ko p s; valid_pde_mappings' s\<rbrakk> \<Longrightarrow> ko_at' ko p s \<and> valid_pde_mapping' (p && mask pdBits) ko
theory Retype_C

lemma ccorres_only_change_locals:
  "\<lbrakk> \<And>s. \<Gamma> \<turnstile> {s} C {t. globals s = globals t} \<rbrakk> \<Longrightarrow> ccorresG rf_sr \<Gamma> dc xfdc \<top> UNIV hs (return x) C" apply (rule ccorres_from_vcg) apply (clarsimp simp: return_def) apply (clarsimp simp: rf_sr_def) apply (rule hoare_complete) apply (clarsimp simp: HoarePartialDef.valid_def) apply (erule_tac x=x in meta_allE) apply (drule hoare_sound) apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<Gamma>\<turnstile> {s} C {t. globals s = globals t}) \<Longrightarrow> ccorres dc xfdc (\<lambda>_. True) UNIV hs (return x) C proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<Gamma>\<turnstile> {s} C {t. globals s = globals t}) \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} C {s. \<exists>(rv, \<sigma>')\<in>fst (return x \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. (\<And>s. \<Gamma>\<turnstile> {s} C {t. globals s = globals t}) \<Longrightarrow> \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr} C {s. (\<sigma>, s) \<in> rf_sr} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. (\<And>s. \<Gamma>\<turnstile> {s} C {t. globals s = globals t}) \<Longrightarrow> \<Gamma>\<turnstile> {s. cstate_relation \<sigma> (globals s)} C {s. cstate_relation \<sigma> (globals s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. (\<And>s. \<Gamma>\<turnstile> {s} C {t. globals s = globals t}) \<Longrightarrow> \<Gamma>\<Turnstile>\<^bsub>/{}\<^esub> {s. cstate_relation \<sigma> (globals s)} C {s. cstate_relation \<sigma> (globals s)},{} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x. \<lbrakk>\<And>s. \<Gamma>\<turnstile> {s} C {t. globals s = globals t}; \<Gamma>\<turnstile> \<langle>C,Normal x\<rangle> \<Rightarrow> t; cstate_relation \<sigma> (globals x)\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. cstate_relation \<sigma> (globals s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x. \<lbrakk>\<Gamma>\<turnstile> \<langle>C,Normal x\<rangle> \<Rightarrow> t; cstate_relation \<sigma> (globals x); \<Gamma>\<turnstile> {x} C {t. globals x = globals t}\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. cstate_relation \<sigma> (globals s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x. \<lbrakk>\<Gamma>\<turnstile> \<langle>C,Normal x\<rangle> \<Rightarrow> t; cstate_relation \<sigma> (globals x); \<Gamma>,{}\<Turnstile>\<^bsub>/{}\<^esub> {x} C {t. globals x = globals t},{}\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. cstate_relation \<sigma> (globals s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> t x. \<lbrakk>\<Gamma>\<turnstile> \<langle>C,Normal x\<rangle> \<Rightarrow> t; cstate_relation \<sigma> (globals x); \<forall>t. \<Gamma>\<turnstile> \<langle>C,Normal x\<rangle> \<Rightarrow> t \<longrightarrow> t \<in> Normal ` {t. globals x = globals t}\<rbrakk> \<Longrightarrow> t \<in> Normal ` {s. cstate_relation \<sigma> (globals s)} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma getObjectSize_max_size:
  "\<lbrakk> newType =  APIObjectType apiobject_type.Untyped \<longrightarrow> x < 32;
         newType =  APIObjectType apiobject_type.CapTableObject \<longrightarrow> x < 28 \<rbrakk> \<Longrightarrow> getObjectSize newType x < word_bits" apply (clarsimp simp only: getObjectSize_def apiGetObjectSize_def word_bits_def
                  split: ARM_H.object_type.splits apiobject_type.splits) apply (clarsimp simp: tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def cteSizeBits_def
                        pdBits_def pageBits_def ptBits_def pteBits_def pdeBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> x < 32; newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x < 28\<rbrakk> \<Longrightarrow> getObjectSize newType x < word_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>newType = APIObjectType ArchTypes_H.apiobject_type.Untyped \<longrightarrow> x < 32; newType = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> x < 28\<rbrakk> \<Longrightarrow> (\<forall>x1. (x1 = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> newType = APIObjectType x1 \<longrightarrow> x < LENGTH(32)) \<and> (x1 = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> newType = APIObjectType x1 \<longrightarrow> tcbBlockSizeBits < LENGTH(32)) \<and> (x1 = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> newType = APIObjectType x1 \<longrightarrow> epSizeBits < LENGTH(32)) \<and> (x1 = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> newType = APIObjectType x1 \<longrightarrow> ntfnSizeBits < LENGTH(32)) \<and> (x1 = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> newType = APIObjectType x1 \<longrightarrow> cteSizeBits + x < LENGTH(32))) \<and> (newType = object_type.SmallPageObject \<longrightarrow> pageBitsForSize Wellformed_C.ARMSmallPage < LENGTH(32)) \<and> (newType = object_type.LargePageObject \<longrightarrow> pageBitsForSize Wellformed_C.ARMLargePage < LENGTH(32)) \<and> (newType = object_type.SectionObject \<longrightarrow> pageBitsForSize Wellformed_C.ARMSection < LENGTH(32)) \<and> (newType = object_type.SuperSectionObject \<longrightarrow> pageBitsForSize Wellformed_C.ARMSuperSection < LENGTH(32)) \<and> (newType = object_type.PageTableObject \<longrightarrow> ptBits < LENGTH(32)) \<and> (newType = object_type.PageDirectoryObject \<longrightarrow> pdBits < LENGTH(32)) proof (prove)
goal:
No subgoals!
theory Retype_C

lemma rf_sr_htd_safe:
  "(s, s') \<in> rf_sr \<Longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s')))" by (simp add: rf_sr_def cstate_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (s, s') \<in> rf_sr \<Longrightarrow> htd_safe domain (hrs_htd (t_hrs_' (globals s')))
theory Retype_C

lemma typ_region_bytes_actually_is_bytes:
  "htd = typ_region_bytes ptr bits htd'
    \<Longrightarrow> region_actually_is_bytes' ptr (2 ^ bits) htd" by (clarsimp simp: region_actually_is_bytes'_def typ_region_bytes_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. htd = typ_region_bytes ptr bits htd' \<Longrightarrow> region_actually_is_bytes' ptr (2 ^ bits) htd