kings-crown/FVELER_Isabelle huggingface dataset:
theory Delete_C

lemma ccorres_drop_cutMon:
  "ccorres_underlying sr Gamm r xf arrel axf P P' hs f g
    \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' hs (cutMon Q f) g" apply (clarsimp simp: ccorres_underlying_def
                        cutMon_def fail_def
                 split: if_split_asm) apply (subst if_P, simp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying sr Gamm r xf arrel axf P P' hs f g \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' hs (cutMon Q f) g proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (f s) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (f s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False)); (a, b) \<in> sr; P a; b \<in> P'; Q a; \<not> snd (f a)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (if Q a then f a else fail a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b n t. \<lbrakk>Gamm\<turnstile>\<^sub>h \<langle>g # hs,b\<rangle> \<Rightarrow> (n, t); \<forall>x\<in>sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (f s) \<longrightarrow> (\<forall>n t. Gamm\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (f s). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False)); (a, b) \<in> sr; P a; b \<in> P'; Q a; \<not> snd (f a)\<rbrakk> \<Longrightarrow> case t of Normal s'' \<Rightarrow> \<exists>(ra, t)\<in>fst (f a). (t, s'') \<in> sr \<and> unif_rrel (n = length hs) r xf arrel axf ra s'' | _ \<Rightarrow> False proof (prove)
goal:
No subgoals!
theory Delete_C

lemma ccap_zombie_radix_less1:
  "\<lbrakk> ccap_relation cap ccap; isZombie cap; capAligned cap \<rbrakk>
      \<Longrightarrow> \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift ccap))
            \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift ccap) < 28" apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap[THEN iffD2]) apply (clarsimp simp: Let_def capAligned_def
                        objBits_simps' word_bits_conv word_less_nat_alt
                        word_le_nat_alt less_mask_eq
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap ccap; isZombie cap; capAligned cap\<rbrakk> \<Longrightarrow> \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift ccap)) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift ccap) < 0x1C proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap ccap; isZombie cap; capAligned cap; cap = (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift ccap)) then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift ccap) && ~~ mask 5) ZombieTCB (unat (capZombieID_CL (cap_zombie_cap_lift ccap) && mask 5)) else let radix = unat (capZombieType_CL (cap_zombie_cap_lift ccap)) in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift ccap) && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL (cap_zombie_cap_lift ccap) && mask (radix + 1))))\<rbrakk> \<Longrightarrow> \<not> isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift ccap)) \<longrightarrow> capZombieType_CL (cap_zombie_cap_lift ccap) < 0x1C proof (prove)
goal:
No subgoals!
theory Delete_C

lemma ccap_zombie_radix_less3:
  "\<lbrakk> ccap_relation cap ccap; isZombie cap; capAligned cap \<rbrakk>
      \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift ccap) < 28" by (clarsimp simp: get_capZombieBits_CL_def Let_def
                     less_mask_eq ccap_zombie_radix_less2
              split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation cap ccap; isZombie cap; capAligned cap\<rbrakk> \<Longrightarrow> get_capZombieBits_CL (cap_zombie_cap_lift ccap) < 0x1C
theory Delete_C

lemma case_assertE_to_assert:
  "(case cap of
           Zombie ptr2 x xa \<Rightarrow>
                  haskell_assertE (P ptr2 x xa) []
                | _ \<Rightarrow> returnOk ())
       = liftE (assert (case cap of Zombie ptr2 x xa \<Rightarrow> P ptr2 x xa | _ \<Rightarrow> True))" apply (simp add: assertE_def returnOk_liftE assert_def
            split: capability.split if_split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case cap of capability.Zombie ptr2 x xa \<Rightarrow> haskell_assertE (P ptr2 x xa) [] | _ \<Rightarrow> returnOk ()) = liftE (assert (case cap of capability.Zombie ptr2 x xa \<Rightarrow> P ptr2 x xa | _ \<Rightarrow> True)) proof (prove)
goal:
No subgoals!
theory Delete_C

lemma of_nat_ZombieTCB_C:
  "n < 28 \<Longrightarrow> of_nat n \<noteq> (ZombieTCB_C :: word32)" apply (drule of_nat_mono_maybe[rotated, where 'a=32]) apply simp apply (clarsimp simp: ZombieTCB_C_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 28 \<Longrightarrow> word_of_nat n \<noteq> ZombieTCB_C proof (prove)
goal (2 subgoals):
 1. 28 < 2 ^ LENGTH(32)
 2. word_of_nat n < word_of_nat 28 \<Longrightarrow> word_of_nat n \<noteq> ZombieTCB_C proof (prove)
goal (1 subgoal):
 1. word_of_nat n < word_of_nat 28 \<Longrightarrow> word_of_nat n \<noteq> ZombieTCB_C proof (prove)
goal:
No subgoals!
theory Delete_C

lemma case_zombie_type_map_inj:
  "case_zombie_type (ZombieTCB_C :: word32) of_nat (capZombieType cap)
     = case_zombie_type (ZombieTCB_C :: word32) of_nat (capZombieType cap')
    \<Longrightarrow> capAligned cap \<Longrightarrow> capAligned cap'
    \<Longrightarrow> isZombie cap \<Longrightarrow> isZombie cap' \<Longrightarrow>
       capZombieType cap = capZombieType cap'" apply (clarsimp simp: capAligned_def word_bits_conv
                        objBits_simps' isCap_simps
                        of_nat_ZombieTCB_C
                        not_sym [OF of_nat_ZombieTCB_C]
                 split: zombie_type.split_asm) apply (subst(asm) word_unat.Abs_inject) apply (simp add: unats_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(case capZombieType cap of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x) = (case capZombieType cap' of ZombieTCB \<Rightarrow> ZombieTCB_C | ZombieCNode x \<Rightarrow> word_of_nat x); capAligned cap; capAligned cap'; isZombie cap; isZombie cap'\<rbrakk> \<Longrightarrow> capZombieType cap = capZombieType cap' proof (prove)
goal (1 subgoal):
 1. \<And>x2 v0 v0a v2 v2a x2a. \<lbrakk>is_aligned v0 (4 + x2a); x2a < 28; is_aligned v0a (4 + x2); x2 < 28; cap = capability.Zombie v0 (ZombieCNode x2a) v2; cap' = capability.Zombie v0a (ZombieCNode x2) v2a; word_of_nat x2a = word_of_nat x2\<rbrakk> \<Longrightarrow> x2a = x2 proof (prove)
goal (3 subgoals):
 1. \<And>x2 v0 v0a v2 v2a x2a. \<lbrakk>is_aligned v0 (4 + x2a); x2a < 28; is_aligned v0a (4 + x2); x2 < 28; cap = capability.Zombie v0 (ZombieCNode x2a) v2; cap' = capability.Zombie v0a (ZombieCNode x2) v2a\<rbrakk> \<Longrightarrow> x2a \<in> unats LENGTH(32)
 2. \<And>x2 v0 v0a v2 v2a x2a. \<lbrakk>is_aligned v0 (4 + x2a); x2a < 28; is_aligned v0a (4 + x2); x2 < 28; cap = capability.Zombie v0 (ZombieCNode x2a) v2; cap' = capability.Zombie v0a (ZombieCNode x2) v2a\<rbrakk> \<Longrightarrow> x2 \<in> unats LENGTH(32)
 3. \<And>x2 v0 v0a v2 v2a x2a. \<lbrakk>is_aligned v0 (4 + x2a); x2a < 28; is_aligned v0a (4 + x2); x2 < 28; cap = capability.Zombie v0 (ZombieCNode x2a) v2; cap' = capability.Zombie v0a (ZombieCNode x2) v2a; x2a = x2\<rbrakk> \<Longrightarrow> x2a = x2 proof (prove)
goal:
No subgoals!
theory Delete_C

lemma valid_Zombie_number_word_bits:
  "valid_cap' cap s \<Longrightarrow> isZombie cap
    \<Longrightarrow> capZombieNumber cap < 2 ^ word_bits" apply (clarsimp simp: valid_cap'_def isCap_simps) apply (erule order_le_less_trans) apply (rule order_le_less_trans[OF zombieCTEs_le]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_cap' cap s; isZombie cap\<rbrakk> \<Longrightarrow> capZombieNumber cap < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2. \<lbrakk>cap = capability.Zombie v0 v1 v2; capAligned (capability.Zombie v0 v1 v2); v2 \<le> zombieCTEs v1; zBits v1 < word_bits; case v1 of ZombieTCB \<Rightarrow> tcb_at' v0 s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> v2 < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2. \<lbrakk>cap = capability.Zombie v0 v1 v2; capAligned (capability.Zombie v0 v1 v2); zBits v1 < word_bits; case v1 of ZombieTCB \<Rightarrow> tcb_at' v0 s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> zombieCTEs v1 < 2 ^ word_bits proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2. \<lbrakk>cap = capability.Zombie v0 v1 v2; capAligned (capability.Zombie v0 v1 v2); zBits v1 < word_bits; case v1 of ZombieTCB \<Rightarrow> tcb_at' v0 s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (v0 + 2 ^ cteSizeBits * (addr && mask n)) s)\<rbrakk> \<Longrightarrow> 2 ^ zBits v1 < 2 ^ word_bits proof (prove)
goal:
No subgoals!
theory Delete_C

lemma ccorres_use_cutMon:
  "(\<And>s. ccorres rvr xf P P' hs (cutMon ((=) s) f) g)
       \<Longrightarrow> ccorres rvr xf P P' hs f g" apply (simp add: ccorres_underlying_def
                   snd_cutMon) apply (simp add: cutMon_def cong: xstate.case_cong) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>s. ccorres rvr xf P P' hs (cutMon ((=) s) f) g) \<Longrightarrow> ccorres rvr xf P P' hs f g proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<forall>x\<in>rf_sr. case x of (sa, s') \<Rightarrow> P sa \<and> s' \<in> P' \<and> s = sa \<and> \<not> snd (f sa) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (cutMon ((=) s) f sa). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False))) \<Longrightarrow> \<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (f s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>(r, t)\<in>fst (f s). (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False)) proof (prove)
goal (1 subgoal):
 1. (\<And>s. \<forall>x\<in>rf_sr. case x of (sa, s') \<Rightarrow> P sa \<and> s' \<in> P' \<and> s = sa \<and> \<not> snd (f sa) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>x\<in>fst (f sa). case x of (r, t) \<Rightarrow> (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False))) \<Longrightarrow> \<forall>x\<in>rf_sr. case x of (s, s') \<Rightarrow> P s \<and> s' \<in> P' \<and> \<not> snd (f s) \<longrightarrow> (\<forall>n t. \<Gamma>\<turnstile>\<^sub>h \<langle>g # hs,s'\<rangle> \<Rightarrow> (n, t) \<longrightarrow> (case t of Normal s'' \<Rightarrow> \<exists>x\<in>fst (f s). case x of (r, t) \<Rightarrow> (t, s'') \<in> rf_sr \<and> unif_rrel (n = length hs) rvr xf rvr xf r s'' | _ \<Rightarrow> False)) proof (prove)
goal:
No subgoals!
theory Detype_C

lemma typ_clear_region_out:
  "x \<notin> {p..+2 ^ bits} \<Longrightarrow> typ_clear_region p bits d x = d x" unfolding typ_clear_region_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> {p..+2 ^ bits} \<Longrightarrow> typ_clear_region p bits d x = d x proof (prove)
goal (1 subgoal):
 1. x \<notin> {p..+2 ^ bits} \<Longrightarrow> (fst (d x), if x \<in> {p..+2 ^ bits} then \<lambda>x. None else snd (d x)) = d x
theory Detype_C

lemma typ_bytes_region_out:
  "x \<notin> {p..+2 ^ bits} \<Longrightarrow> typ_region_bytes p bits d x = d x" unfolding typ_region_bytes_def by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. x \<notin> {p..+2 ^ bits} \<Longrightarrow> typ_region_bytes p bits d x = d x proof (prove)
goal (1 subgoal):
 1. x \<notin> {p..+2 ^ bits} \<Longrightarrow> (if x \<in> {p..+2 ^ bits} then (True, [0::'b \<mapsto> (typ_uinfo_t TYPE(8 word), True)]) else d x) = d x
theory Detype_C

lemma list_map_le_singleton:
  "map_le (list_map xs) [n \<mapsto> x]
    = (xs = [] \<or> n = 0 \<and> xs = [x])" apply (simp add: list_map_def) apply (rule iffI) apply (drule map_of_le) apply simp apply (cases xs, simp_all add: list_map_def upt_conv_Cons
                       split: if_split_asm del: upt.simps) apply (case_tac list, simp_all add: upt_conv_Cons del: upt.simps) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (list_map xs \<subseteq>\<^sub>m [n \<mapsto> x]) = (xs = [] \<or> n = 0 \<and> xs = [x]) proof (prove)
goal (1 subgoal):
 1. (map_of (zip [0..<length xs] xs) \<subseteq>\<^sub>m [n \<mapsto> x]) = (xs = [] \<or> n = 0 \<and> xs = [x]) proof (prove)
goal (2 subgoals):
 1. map_of (zip [0..<length xs] xs) \<subseteq>\<^sub>m [n \<mapsto> x] \<Longrightarrow> xs = [] \<or> n = 0 \<and> xs = [x]
 2. xs = [] \<or> n = 0 \<and> xs = [x] \<Longrightarrow> map_of (zip [0..<length xs] xs) \<subseteq>\<^sub>m [n \<mapsto> x] proof (prove)
goal (3 subgoals):
 1. distinct (map fst (zip [0..<length xs] xs))
 2. \<forall>(xa, v)\<in>set (zip [0..<length xs] xs). [n \<mapsto> x] xa = Some v \<Longrightarrow> xs = [] \<or> n = 0 \<and> xs = [x]
 3. xs = [] \<or> n = 0 \<and> xs = [x] \<Longrightarrow> map_of (zip [0..<length xs] xs) \<subseteq>\<^sub>m [n \<mapsto> x] proof (prove)
goal (2 subgoals):
 1. \<forall>(xa, v)\<in>set (zip [0..<length xs] xs). [n \<mapsto> x] xa = Some v \<Longrightarrow> xs = [] \<or> n = 0 \<and> xs = [x]
 2. xs = [] \<or> n = 0 \<and> xs = [x] \<Longrightarrow> map_of (zip [0..<length xs] xs) \<subseteq>\<^sub>m [n \<mapsto> x] proof (prove)
goal (2 subgoals):
 1. \<And>list. \<lbrakk>xs = x # list; n = 0; \<forall>xa\<in>set (zip [Suc 0..<Suc (length list)] list). case xa of (xa, v) \<Rightarrow> (if xa = 0 then Some x else None) = Some v\<rbrakk> \<Longrightarrow> list = []
 2. xs = [] \<or> n = 0 \<and> xs = [x] \<Longrightarrow> map_of (zip [0..<length xs] xs) \<subseteq>\<^sub>m [n \<mapsto> x] proof (prove)
goal (1 subgoal):
 1. xs = [] \<or> n = 0 \<and> xs = [x] \<Longrightarrow> map_of (zip [0..<length xs] xs) \<subseteq>\<^sub>m [n \<mapsto> x] proof (prove)
goal:
No subgoals!
theory Detype_C

lemma neq_types_not_typ_slice_eq:
  "\<lbrakk> s \<noteq> t \<rbrakk> \<Longrightarrow> typ_slice_t s k \<noteq> [(t, v)]" using ladder_set_self[where s=s and n=k] by clarsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s \<noteq> t \<Longrightarrow> typ_slice_t s k \<noteq> [(t, v)] proof (prove)
using this:
s \<in> fst ` set (typ_slice_t s k)

goal (1 subgoal):
 1. s \<noteq> t \<Longrightarrow> typ_slice_t s k \<noteq> [(t, v)]
theory Detype_C

lemma h_t_valid_typ_region_bytes:
  fixes p :: "'a :: c_type ptr"
  assumes neq_byte: "typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE (word8)"
  shows "typ_region_bytes ptr bits hp,g \<Turnstile>\<^sub>t p =
   ({ptr_val p ..+ size_of (TYPE ('a))} \<inter> {ptr ..+ 2 ^ bits} = {} \<and> hp,g \<Turnstile>\<^sub>t p)" unfolding h_t_valid_def by (simp add: valid_footprint_typ_region_bytes[OF neq_byte]
                size_of_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. typ_region_bytes ptr bits hp,g \<Turnstile>\<^sub>t p = ({ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> hp,g \<Turnstile>\<^sub>t p) proof (prove)
goal (1 subgoal):
 1. (valid_footprint (typ_region_bytes ptr bits hp) (ptr_val p) (typ_uinfo_t TYPE('a)) \<and> g p) = ({ptr_val p..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> valid_footprint hp (ptr_val p) (typ_uinfo_t TYPE('a)) \<and> g p)
theory Detype_C

lemma heap_list_s_heap_list':
  fixes p :: "'a :: c_type ptr"
  shows "hrs_htd hp,\<top> \<Turnstile>\<^sub>t p \<Longrightarrow>
  heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val p) =
  heap_list (hrs_mem hp) (size_of TYPE('a)) (ptr_val p)" apply (cases hp) apply (simp add: hrs_htd_def hrs_mem_def heap_list_s_heap_list) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. hrs_htd hp,\<lambda>_. True \<Turnstile>\<^sub>t p \<Longrightarrow> heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val p) = heap_list (hrs_mem hp) (size_of TYPE('a)) (ptr_val p) proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>hrs_htd hp,\<lambda>_. True \<Turnstile>\<^sub>t p; hp = (a, b)\<rbrakk> \<Longrightarrow> heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val p) = heap_list (hrs_mem hp) (size_of TYPE('a)) (ptr_val p) proof (prove)
goal:
No subgoals!
theory Detype_C

lemma image_Ptr:
  "Ptr ` S = {x. ptr_val x \<in> S}" apply (safe, simp_all) apply (case_tac x, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. PTR('a) ` S = {x. ptr_val x \<in> S} proof (prove)
goal (1 subgoal):
 1. \<And>x. ptr_val x \<in> S \<Longrightarrow> x \<in> PTR('a) ` S proof (prove)
goal:
No subgoals!
theory Detype_C

lemma cmap_relation_h_t_valid:
  fixes p :: "'a :: c_type ptr"
  shows "\<lbrakk>cmap_relation am (cslift s' :: 'a typ_heap) f rel; s' \<Turnstile>\<^sub>c p;
  \<And>v v' x. \<lbrakk>f x = p; am x = Some v; cslift s' p = Some v'; rel v v'\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" unfolding cmap_relation_def apply (clarsimp simp: h_t_valid_clift_Some_iff) apply (drule equalityD2) apply (drule (1) subsetD [OF _ domI]) apply clarsimp apply (drule (1) bspec [OF _ domI]) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cmap_relation am (cslift s') f rel; s' \<Turnstile>\<^sub>c p; \<And>v v' x. \<lbrakk>f x = p; am x = Some v; cslift s' p = Some v'; rel v v'\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<lbrakk>f ` dom am = dom (cslift s') \<and> (\<forall>x\<in>dom am. rel (the (am x)) (the (cslift s' (f x)))); s' \<Turnstile>\<^sub>c p; \<And>v v' x. \<lbrakk>f x = p; am x = Some v; cslift s' p = Some v'; rel v v'\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>\<And>va v' x. \<lbrakk>f x = p; am x = Some va; v = v'; rel va v'\<rbrakk> \<Longrightarrow> R; cslift s' p = Some v; f ` dom am = dom (cslift s'); \<forall>x\<in>dom am. rel (the (am x)) (the (cslift s' (f x)))\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>\<And>va v' x. \<lbrakk>f x = p; am x = Some va; v = v'; rel va v'\<rbrakk> \<Longrightarrow> R; cslift s' p = Some v; \<forall>x\<in>dom am. rel (the (am x)) (the (cslift s' (f x))); dom (cslift s') \<subseteq> f ` dom am\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>\<And>va v' x. \<lbrakk>f x = p; am x = Some va; v = v'; rel va v'\<rbrakk> \<Longrightarrow> R; cslift s' p = Some v; \<forall>x\<in>dom am. rel (the (am x)) (the (cslift s' (f x))); p \<in> f ` dom am\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<And>v x y. \<lbrakk>\<And>va v' xa. \<lbrakk>f xa = f x; am xa = Some va; v = v'; rel va v'\<rbrakk> \<Longrightarrow> R; cslift s' (f x) = Some v; \<forall>x\<in>dom am. rel (the (am x)) (the (cslift s' (f x))); p = f x; am x = Some y\<rbrakk> \<Longrightarrow> R proof (prove)
goal (1 subgoal):
 1. \<And>v x y. \<lbrakk>\<And>va v' xa. \<lbrakk>f xa = f x; am xa = Some va; v = v'; rel va v'\<rbrakk> \<Longrightarrow> R; cslift s' (f x) = Some v; p = f x; am x = Some y; rel (the (am x)) (the (cslift s' (f x)))\<rbrakk> \<Longrightarrow> R proof (prove)
goal:
No subgoals!
theory Detype_C

lemma aligned_ranges_subset_or_disjointE [consumes 2, case_names disjoint subset1 subset2]:
  "\<lbrakk>is_aligned p n; is_aligned p' n';
   {p..p + 2 ^ n - 1} \<inter> {p'..p' + 2 ^ n' - 1} = {}  \<Longrightarrow> P;
   {p..p + 2 ^ n - 1} \<subseteq> {p'..p' + 2 ^ n' - 1} \<Longrightarrow> P;
   {p'..p' + 2 ^ n' - 1} \<subseteq> {p..p + 2 ^ n - 1} \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" apply (drule (1) aligned_ranges_subset_or_disjoint) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p n; is_aligned p' n'; {p..p + 2 ^ n - 1} \<inter> {p'..p' + 2 ^ n' - 1} = {} \<Longrightarrow> P; {p..p + 2 ^ n - 1} \<subseteq> {p'..p' + 2 ^ n' - 1} \<Longrightarrow> P; {p'..p' + 2 ^ n' - 1} \<subseteq> {p..p + 2 ^ n - 1} \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned p' n'; {p..p + 2 ^ n - 1} \<inter> {p'..p' + 2 ^ n' - 1} = {} \<Longrightarrow> P; {p..p + 2 ^ n - 1} \<subseteq> {p'..p' + 2 ^ n' - 1} \<Longrightarrow> P; {p'..p' + 2 ^ n' - 1} \<subseteq> {p..p + 2 ^ n - 1} \<Longrightarrow> P; {p..p + 2 ^ n - 1} \<inter> {p'..p' + 2 ^ n' - 1} = {} \<or> {p..p + 2 ^ n - 1} \<subseteq> {p'..p' + 2 ^ n' - 1} \<or> {p'..p' + 2 ^ n' - 1} \<subseteq> {p..p + 2 ^ n - 1}\<rbrakk> \<Longrightarrow> P proof (prove)
goal:
No subgoals!
theory Detype_C

lemma tcb_ptr_to_ctcb_ptr_in_range:
  fixes tcb :: tcb
  assumes tat: "ko_at' tcb x s"
  shows "ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}" proof - from tat have al: "is_aligned x tcbBlockSizeBits" by (clarsimp elim!: obj_atE' simp: projectKOs objBits_simps) hence "x \<le> x + 2 ^ tcbBlockSizeBits - 1" by (rule is_aligned_no_overflow) moreover from al have "x \<le> x + 2 ^ ctcb_size_bits" by (rule is_aligned_no_wrap') (simp add: ctcb_size_bits_def objBits_defs) ultimately show ?thesis unfolding tcb_ptr_to_ctcb_ptr_def by (simp add: ctcb_offset_defs objBits_simps' add.commute)
       (subst word_plus_mono_right; simp) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1} proof (state)
goal (1 subgoal):
 1. ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1} proof (chain)
picking this:
ko_at' tcb x s proof (prove)
using this:
ko_at' tcb x s

goal (1 subgoal):
 1. is_aligned x tcbBlockSizeBits proof (state)
this:
is_aligned x tcbBlockSizeBits

goal (1 subgoal):
 1. ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1} proof (prove)
using this:
is_aligned x tcbBlockSizeBits

goal (1 subgoal):
 1. x \<le> x + 2 ^ tcbBlockSizeBits - 1 proof (state)
this:
x \<le> x + 2 ^ tcbBlockSizeBits - 1

goal (1 subgoal):
 1. ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1} proof (state)
this:
x \<le> x + 2 ^ tcbBlockSizeBits - 1

goal (1 subgoal):
 1. ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1} proof (chain)
picking this:
is_aligned x tcbBlockSizeBits proof (prove)
using this:
is_aligned x tcbBlockSizeBits

goal (1 subgoal):
 1. x \<le> x + 2 ^ ctcb_size_bits proof (state)
this:
x \<le> x + 2 ^ ctcb_size_bits

goal (1 subgoal):
 1. ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1} proof (chain)
picking this:
x \<le> x + 2 ^ tcbBlockSizeBits - 1
x \<le> x + 2 ^ ctcb_size_bits proof (prove)
using this:
x \<le> x + 2 ^ tcbBlockSizeBits - 1
x \<le> x + 2 ^ ctcb_size_bits

goal (1 subgoal):
 1. ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1} proof (prove)
using this:
x \<le> x + 2 ^ tcbBlockSizeBits - 1
x \<le> x + 2 ^ ctcb_size_bits

goal (1 subgoal):
 1. ptr_val (tcb_Ptr (x + ctcb_offset)) \<in> {x..x + 2 ^ objBits tcb - 1} proof (state)
this:
ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}

goal:
No subgoals!