kings-crown/FVELER_Isabelle huggingface dataset:
theory Retype_C

lemma memzero_modifies:
  "\<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call memzero_'proc {t. t may_only_modify_globals \<sigma> in [t_hrs]}" apply (rule allI, rule conseqPre) apply (hoare_rule HoarePartial.ProcNoRec1) apply (tactic \<open>HoarePackage.vcg_tac "_modifies" "false" [] @{context} 1\<close>) apply (clarsimp simp: mex_def meq_def simp del: split_paired_Ex) apply (intro exI globals.equality, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {\<sigma>} Call memzero_'proc {t. t may_only_modify_globals \<sigma> in [t_hrs]} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P'2 \<sigma>) Call memzero_'proc {t. t may_only_modify_globals \<sigma> in [t_hrs]}
 2. \<And>\<sigma>. {\<sigma>} \<subseteq> ?P'2 \<sigma> proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?P5 \<sigma> ()) TRY
  \<acute>p___ptr_to_unsigned_char :== PTR_COERCE(unit \<rightarrow> 8 word) \<acute>s;;
SKIP;;
SKIP;;
Guard GhostStateError \<lbrace>fst (gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> \<acute>n \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state, id)\<rbrace> (\<acute>globals :== ghost'state_'_update (snd (gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state = 0 \<or> \<acute>n \<le> gs_get_assn cap_get_capSizeBits_'proc \<acute>ghost'state, id)));;
WHILE \<acute>n \<noteq> SCAST(32 signed \<rightarrow> 32) 0 DO
  Guard C_Guard \<lbrace>ptr_safe (PTR_COERCE(8 word \<rightarrow> 32 word) \<acute>p___ptr_to_unsigned_char) (hrs_htd \<acute>t_hrs) \<and> c_guard (PTR_COERCE(8 word \<rightarrow> 32 word) \<acute>p___ptr_to_unsigned_char)\<rbrace> (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR_COERCE(8 word \<rightarrow> 32 word) \<acute>p___ptr_to_unsigned_char) (SCAST(32 signed \<rightarrow> 32) 0))));;
Guard MemorySafety \<lbrace>ptr_add_assertion' \<acute>p___ptr_to_unsigned_char (uint (word_of_int (int (size_of TYPE(32 word))))) False (hrs_htd \<acute>t_hrs)\<rbrace> (\<acute>p___ptr_to_unsigned_char :== \<acute>p___ptr_to_unsigned_char +\<^sub>p uint (word_of_int (int (size_of TYPE(32 word)))));;
\<acute>n :== \<acute>n - UCAST(32 \<rightarrow> 32) (word_of_int (int (size_of TYPE(32 word))))
OD
CATCH SKIP
END {t. t may_only_modify_globals \<sigma> in [t_hrs]}
 2. \<And>\<sigma>. {\<sigma>} \<subseteq> ?P5 \<sigma> () proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {\<sigma>} \<subseteq> {s. globals s may_only_modify_globals \<sigma> in [t_hrs]} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. \<exists>t_hrs_'. ghost'state_'_update (\<lambda>a. a) (globals \<sigma>) = globals \<sigma>\<lparr>t_hrs_' := t_hrs_'\<rparr> proof (prove)
goal:
No subgoals!
theory Retype_C

lemma ghost_assertion_size_logic_no_unat:
  "sz \<le> gsMaxObjectSize s
    \<Longrightarrow> (s, \<sigma>) \<in> rf_sr
    \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>)) = 0 \<or>
            of_nat sz \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>))" apply (rule ghost_assertion_size_logic'[rotated]) apply (simp add: rf_sr_def) apply (simp add: unat_of_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz \<le> gsMaxObjectSize s; (s, \<sigma>) \<in> rf_sr\<rbrakk> \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>)) = 0 \<or> word_of_nat sz \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>sz \<le> gsMaxObjectSize s; (s, \<sigma>) \<in> rf_sr\<rbrakk> \<Longrightarrow> cstate_relation ?s (globals \<sigma>)
 2. \<lbrakk>sz \<le> gsMaxObjectSize s; (s, \<sigma>) \<in> rf_sr\<rbrakk> \<Longrightarrow> unat (word_of_nat sz) \<le> gsMaxObjectSize ?s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz \<le> gsMaxObjectSize s; (s, \<sigma>) \<in> rf_sr\<rbrakk> \<Longrightarrow> unat (word_of_nat sz) \<le> gsMaxObjectSize s proof (prove)
goal:
No subgoals!
theory Retype_C

lemma ptr_array_retyps_htd_safe_neg:
  "\<lbrakk> htd_safe D htd; {ptr_val ptr ..+ n * size_of TYPE('a :: mem_type)} \<inter> D' = {}; -D \<subseteq> D' \<rbrakk>
   \<Longrightarrow> htd_safe D (ptr_arr_retyps n (ptr :: 'a ptr) htd)" apply (simp add: htd_safe_def ptr_arr_retyps_def htd_update_list_dom_better) apply (auto simp: dom_tll_def intvl_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>htd_safe D htd; {ptr_val ptr..+n * size_of TYPE('a)} \<inter> D' = {}; - D \<subseteq> D'\<rbrakk> \<Longrightarrow> htd_safe D (ptr_arr_retyps n ptr htd) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dom_s htd \<subseteq> D \<times> UNIV; {ptr_val ptr..+n * size_of TYPE('a)} \<inter> D' = {}; - D \<subseteq> D'\<rbrakk> \<Longrightarrow> dom_tll (ptr_val ptr) (map (\<lambda>i. list_map (typ_slice_t (uinfo_array_tag_n_m TYPE('a) n n) i)) [0..<n * size_of TYPE('a)]) \<subseteq> D \<times> UNIV proof (prove)
goal:
No subgoals!
theory Retype_C

lemma dom_disj_union:
  "dom (\<lambda>x. if P x \<or> Q x then Some (G x) else None) = dom (\<lambda>x. if P x then Some (G x) else None)
  \<union> dom (\<lambda>x. if Q x then Some (G x) else None)" by (auto split:if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dom (\<lambda>x. if P x \<or> Q x then Some (G x) else None) = dom (\<lambda>x. if P x then Some (G x) else None) \<union> dom (\<lambda>x. if Q x then Some (G x) else None)
theory Retype_C

lemma ccorres_apiType_split:
  "\<lbrakk> apiType = apiobject_type.Untyped \<Longrightarrow> ccorres rr xf P1 P1' hs X Y;
     apiType = apiobject_type.TCBObject \<Longrightarrow> ccorres rr xf P2 P2' hs X Y;
     apiType = apiobject_type.EndpointObject \<Longrightarrow> ccorres rr xf P3 P3' hs X Y;
     apiType = apiobject_type.NotificationObject \<Longrightarrow> ccorres rr xf P4 P4' hs X Y;
     apiType = apiobject_type.CapTableObject \<Longrightarrow> ccorres rr xf P5 P5' hs X Y
   \<rbrakk> \<Longrightarrow> ccorres rr xf
         ((\<lambda>s. apiType = apiobject_type.Untyped \<longrightarrow> P1 s)
         and (\<lambda>s. apiType = apiobject_type.TCBObject \<longrightarrow> P2 s)
         and (\<lambda>s. apiType = apiobject_type.EndpointObject \<longrightarrow> P3 s)
         and (\<lambda>s. apiType = apiobject_type.NotificationObject \<longrightarrow> P4 s)
         and (\<lambda>s. apiType = apiobject_type.CapTableObject \<longrightarrow> P5 s))
         ({s. apiType = apiobject_type.Untyped \<longrightarrow> s \<in> P1'}
         \<inter> {s. apiType = apiobject_type.TCBObject \<longrightarrow> s \<in> P2'}
         \<inter> {s. apiType = apiobject_type.EndpointObject \<longrightarrow> s \<in> P3'}
         \<inter> {s. apiType = apiobject_type.NotificationObject \<longrightarrow> s \<in> P4'}
         \<inter> {s. apiType = apiobject_type.CapTableObject \<longrightarrow> s \<in> P5'})
         hs X Y" apply (case_tac apiType, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>apiType = ArchTypes_H.apiobject_type.Untyped \<Longrightarrow> ccorres rr xf P1 P1' hs X Y; apiType = ArchTypes_H.apiobject_type.TCBObject \<Longrightarrow> ccorres rr xf P2 P2' hs X Y; apiType = ArchTypes_H.apiobject_type.EndpointObject \<Longrightarrow> ccorres rr xf P3 P3' hs X Y; apiType = ArchTypes_H.apiobject_type.NotificationObject \<Longrightarrow> ccorres rr xf P4 P4' hs X Y; apiType = ArchTypes_H.apiobject_type.CapTableObject \<Longrightarrow> ccorres rr xf P5 P5' hs X Y\<rbrakk> \<Longrightarrow> ccorres rr xf ((\<lambda>s. apiType = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> P1 s) and (\<lambda>s. apiType = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> P2 s) and (\<lambda>s. apiType = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> P3 s) and (\<lambda>s. apiType = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> P4 s) and (\<lambda>s. apiType = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> P5 s)) ({s. apiType = ArchTypes_H.apiobject_type.Untyped \<longrightarrow> s \<in> P1'} \<inter> {s. apiType = ArchTypes_H.apiobject_type.TCBObject \<longrightarrow> s \<in> P2'} \<inter> {s. apiType = ArchTypes_H.apiobject_type.EndpointObject \<longrightarrow> s \<in> P3'} \<inter> {s. apiType = ArchTypes_H.apiobject_type.NotificationObject \<longrightarrow> s \<in> P4'} \<inter> {s. apiType = ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> s \<in> P5'}) hs X Y proof (prove)
goal:
No subgoals!
theory Retype_C

lemma gsUserPages_update_ccorres:
  "ccorresG rf_sr G dc xf (\<lambda>_. sz = pageBitsForSize pgsz) UNIV hs
     (modify (gsUserPages_update (\<lambda>m a. if a = ptr then Some pgsz else m a)))
     (Basic (globals_update (ghost'state_'_update
                  (gs_new_frames pgsz ptr sz))))" apply (rule ccorres_from_vcg) apply vcg_step apply (clarsimp simp: split_def simpler_modify_def gs_new_frames_def) apply (case_tac "ghost'state_' (globals x)") apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def fun_upd_def
                        carch_state_relation_def cmachine_state_relation_def
                        ghost_size_rel_def ghost_assertion_data_get_def
                  cong: if_cong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorresG rf_sr G dc xf (\<lambda>_. sz = pageBitsForSize pgsz) UNIV hs (modify (gsUserPages_update (\<lambda>m a. if a = ptr then Some pgsz else m a))) (\<acute>globals :== ghost'state_'_update (gs_new_frames pgsz ptr sz)) proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. G\<turnstile> {s. sz = pageBitsForSize pgsz \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>globals :== ghost'state_'_update (gs_new_frames pgsz ptr sz) {s. \<exists>(rv, \<sigma>')\<in>fst (modify (gsUserPages_update (\<lambda>m a. if a = ptr then Some pgsz else m a)) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xf s)} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. sz = pageBitsForSize pgsz \<and> True \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (modify (gsUserPages_update (\<lambda>m a. if a = ptr then Some pgsz else m a)) \<sigma>). (\<sigma>', globals_update (ghost'state_'_update (gs_new_frames pgsz ptr sz)) s) \<in> rf_sr \<and> dc rv (xf (globals_update (ghost'state_'_update (gs_new_frames pgsz ptr sz)) s))} proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x. \<lbrakk>(\<sigma>, x) \<in> rf_sr; sz = pageBitsForSize pgsz\<rbrakk> \<Longrightarrow> (gsUserPages_update (\<lambda>m a. if a = ptr then Some pgsz else m a) \<sigma>, globals_update (ghost'state_'_update (\<lambda>gs. (\<lambda>x. if x = ptr then Some pgsz else fst gs x, snd gs))) x) \<in> rf_sr proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma> x a b c. \<lbrakk>(\<sigma>, x) \<in> rf_sr; sz = pageBitsForSize pgsz; ghost'state_' (globals x) = (a, b, c)\<rbrakk> \<Longrightarrow> (gsUserPages_update (\<lambda>m a. if a = ptr then Some pgsz else m a) \<sigma>, globals_update (ghost'state_'_update (\<lambda>gs. (\<lambda>x. if x = ptr then Some pgsz else fst gs x, snd gs))) x) \<in> rf_sr proof (prove)
goal:
No subgoals!
theory Retype_C

lemma gsUserPages_update:
    "\<And>f. (\<lambda>s. s\<lparr>gsUserPages := f(gsUserPages s)\<rparr>) = gsUserPages_update f" by (rule ext) simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>f. (\<lambda>s. s\<lparr>gsUserPages := f (gsUserPages s)\<rparr>) = gsUserPages_update f
theory Retype_C

lemma modify_gsUserPages_update:
  "modify (\<lambda>s. s\<lparr>gsUserPages := f(gsUserPages s)\<rparr>) = modify (gsUserPages_update f)" by (simp only: gsUserPages_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify (\<lambda>s. s\<lparr>gsUserPages := f (gsUserPages s)\<rparr>) = modify (gsUserPages_update f)
theory Retype_C

lemma cond_second_eq_seq_ccorres:
  "ccorres_underlying sr Gamm r xf arrel axf G G' hs m
        (Cond P (a ;; c) (b ;; c) ;; d)
    = ccorres_underlying sr Gamm r xf arrel axf G G' hs m
        (Cond P a b ;; c ;; d)" apply (rule ccorres_semantic_equiv) apply (rule semantic_equivI) apply (auto elim!: exec_Normal_elim_cases intro: exec.Seq exec.CondTrue exec.CondFalse) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamm r xf arrel axf G G' hs m (Cond P (a;;
c) (b;;
c);;
d) = ccorres_underlying sr Gamm r xf arrel axf G G' hs m (Cond P a b;;
c;;
d) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> semantic_equiv Gamm s s' (Cond P (a;;
c) (b;;
c);;
d) (Cond P a b;;
c;;
d) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. s \<in> G' \<Longrightarrow> Gamm\<turnstile> \<langle>Cond P (a;;
c) (b;;
c);;
d,Normal s\<rangle> \<Rightarrow> s' = Gamm\<turnstile> \<langle>Cond P a b;;
c;;
d,Normal s\<rangle> \<Rightarrow> s' proof (prove)
goal:
No subgoals!
theory Retype_C

lemma map_to_tcbs_upd:
  "map_to_tcbs ((ksPSpace s)(t \<mapsto> KOTCB tcb')) = (map_to_tcbs (ksPSpace s))(t \<mapsto> tcb')" apply (rule ext) apply (clarsimp simp: map_comp_def projectKOs split: option.splits if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. map_to_tcbs ((ksPSpace s)(t \<mapsto> KOTCB tcb')) = (map_to_tcbs (ksPSpace s))(t \<mapsto> tcb') proof (prove)
goal (1 subgoal):
 1. \<And>x. map_to_tcbs ((ksPSpace s)(t \<mapsto> KOTCB tcb')) x = ((map_to_tcbs (ksPSpace s))(t \<mapsto> tcb')) x proof (prove)
goal:
No subgoals!
theory Retype_C

lemma cep_relations_drop_fun_upd:
  "\<lbrakk> f x = Some v; tcbEPNext_C v' = tcbEPNext_C v; tcbEPPrev_C v' = tcbEPPrev_C v \<rbrakk>
      \<Longrightarrow> cendpoint_relation (f (x \<mapsto> v')) = cendpoint_relation f"
  "\<lbrakk> f x = Some v; tcbEPNext_C v' = tcbEPNext_C v; tcbEPPrev_C v' = tcbEPPrev_C v \<rbrakk>
      \<Longrightarrow> cnotification_relation (f (x \<mapsto> v')) = cnotification_relation f" by (intro ext cendpoint_relation_upd_tcb_no_queues[where thread=x]
                cnotification_relation_upd_tcb_no_queues[where thread=x]
          | simp split: if_split)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>f x = Some v; tcbEPNext_C v' = tcbEPNext_C v; tcbEPPrev_C v' = tcbEPPrev_C v\<rbrakk> \<Longrightarrow> cendpoint_relation (f(x \<mapsto> v')) = cendpoint_relation f) &&& (\<lbrakk>f x = Some v; tcbEPNext_C v' = tcbEPNext_C v; tcbEPPrev_C v' = tcbEPPrev_C v\<rbrakk> \<Longrightarrow> cnotification_relation (f(x \<mapsto> v')) = cnotification_relation f)
theory Retype_C

lemma ccorres_guard_impR:
  "\<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf W Q' hs f g; (\<And>s s'. \<lbrakk>(s, s') \<in> sr; s' \<in> A'\<rbrakk> \<Longrightarrow> s' \<in> Q')\<rbrakk>
  \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf W A' hs f g" by (rule ccorres_guard_imp2,simp+)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccorres_underlying sr \<Gamma> r xf arrel axf W Q' hs f g; \<And>s s'. \<lbrakk>(s, s') \<in> sr; s' \<in> A'\<rbrakk> \<Longrightarrow> s' \<in> Q'\<rbrakk> \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf W A' hs f g
theory Retype_C

lemma tcb_range_subseteq:
  "is_aligned x (objBitsKO (KOTCB ko))
   \<Longrightarrow> {ptr_val (tcb_ptr_to_ctcb_ptr x)..+size_of TYPE(tcb_C)} \<subseteq> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1}" apply (simp add: tcb_ptr_to_ctcb_ptr_def) apply (rule subset_trans) apply (rule intvl_sub_offset[where z = "2^objBitsKO (KOTCB ko)"]) apply (simp add: ctcb_offset_defs size_of_def objBits_simps') apply (subst intvl_range_conv) apply simp apply (simp add: objBits_simps' word_bits_conv) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> ptr_span (tcb_ptr_to_ctcb_ptr x) \<subseteq> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} proof (prove)
goal (1 subgoal):
 1. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> {x + ctcb_offset..+152} \<subseteq> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} proof (prove)
goal (2 subgoals):
 1. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> {x + ctcb_offset..+152} \<subseteq> ?B1
 2. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> ?B1 \<subseteq> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} proof (prove)
goal (2 subgoals):
 1. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> unat ctcb_offset + 152 \<le> 2 ^ objBitsKO (KOTCB ko)
 2. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> {x..+2 ^ objBitsKO (KOTCB ko)} \<subseteq> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} proof (prove)
goal (1 subgoal):
 1. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> {x..+2 ^ objBitsKO (KOTCB ko)} \<subseteq> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} proof (prove)
goal (3 subgoals):
 1. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> is_aligned x (objBitsKO (KOTCB ko))
 2. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> objBitsKO (KOTCB ko) < LENGTH(32)
 3. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} \<subseteq> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} proof (prove)
goal (2 subgoals):
 1. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> objBitsKO (KOTCB ko) < LENGTH(32)
 2. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} \<subseteq> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} proof (prove)
goal (1 subgoal):
 1. is_aligned x (objBitsKO (KOTCB ko)) \<Longrightarrow> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} \<subseteq> {x..x + 2 ^ objBitsKO (KOTCB ko) - 1} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma typ_bytes_cpspace_relation_clift_userdata:
assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::kernel_state))) hp"
  and "is_aligned ptr bits" "bits < word_bits"
  and "pspace_aligned' s"
  and "pspace_no_overlap' ptr bits s"
shows "clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = ((clift hp) :: (user_data_C ptr \<rightharpoonup> user_data_C))"
  (is "?lhs = ?rhs") using assms apply - apply (rule lift_t_typ_region_bytes_none, simp_all) apply (rule pspace_no_overlap_induce_user_data[simplified], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
using this:
cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp
is_aligned ptr bits
bits < word_bits
pspace_aligned' s
pspace_no_overlap' ptr bits s

goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s; clift hp x = Some v\<rbrakk> \<Longrightarrow> {ptr_val x..+4096} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma typ_bytes_cpspace_relation_clift_devicedata:
assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::kernel_state))) hp"
  and "is_aligned ptr bits" "bits < word_bits"
  and "pspace_aligned' s"
  and "pspace_no_overlap' ptr bits s"
 shows "clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = ((clift hp) :: (user_data_device_C ptr \<rightharpoonup> user_data_device_C))"
  (is "?lhs = ?rhs") using assms apply - apply (rule lift_t_typ_region_bytes_none, simp_all) apply (rule pspace_no_overlap_induce_device_data[simplified], auto) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
using this:
cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp
is_aligned ptr bits
bits < word_bits
pspace_aligned' s
pspace_no_overlap' ptr bits s

goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s; clift hp x = Some v\<rbrakk> \<Longrightarrow> {ptr_val x..+4096} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma typ_bytes_cpspace_relation_clift_tcb:
assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::kernel_state))) hp"
  and "is_aligned ptr bits" "bits < word_bits"
  and "pspace_aligned' s"
  and "pspace_no_overlap' ptr bits s"
 shows "clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = ((clift hp) :: (tcb_C ptr \<rightharpoonup> tcb_C))"
  (is "?lhs = ?rhs") using assms apply - apply (rule lift_t_typ_region_bytes_none, simp_all) apply (erule(5) pspace_no_overlap_induce_tcb[simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
using this:
cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp
is_aligned ptr bits
bits < word_bits
pspace_aligned' s
pspace_no_overlap' ptr bits s

goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s; clift hp x = Some v\<rbrakk> \<Longrightarrow> {ptr_val x..+152} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal:
No subgoals!
theory Retype_C

lemma typ_bytes_cpspace_relation_clift_pde:
assumes "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState (s::kernel_state))) hp"
  and "is_aligned ptr bits" "bits < word_bits"
  and "pspace_aligned' s"
  and "pspace_no_overlap' ptr bits s"
 shows "clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = ((clift hp) :: (pde_C ptr \<rightharpoonup> pde_C))"
  (is "?lhs = ?rhs") using assms apply - apply (rule lift_t_typ_region_bytes_none, simp_all) apply (erule(5) pspace_no_overlap_induce_pde[unfolded size_of_def,simplified]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
using this:
cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp
is_aligned ptr bits
bits < word_bits
pspace_aligned' s
pspace_no_overlap' ptr bits s

goal (1 subgoal):
 1. clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s\<rbrakk> \<Longrightarrow> clift (hrs_htd_update (typ_region_bytes ptr bits) hp) = clift hp proof (prove)
goal (1 subgoal):
 1. \<And>x v. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) hp; is_aligned ptr bits; bits < word_bits; pspace_aligned' s; pspace_no_overlap' ptr bits s; clift hp x = Some v\<rbrakk> \<Longrightarrow> {ptr_val x..+4} \<inter> {ptr..+2 ^ bits} = {} proof (prove)
goal:
No subgoals!