kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_C

lemma ccorres_cases:
  assumes P:    " P \<Longrightarrow> ccorres r xf G G' hs a b"
  assumes notP: "\<not>P \<Longrightarrow> ccorres r xf H H' hs a b"
  shows "ccorres r xf (\<lambda>s. (P \<longrightarrow> G s) \<and> (\<not>P \<longrightarrow> H s))
                      ({s. P \<longrightarrow> s \<in> G'} \<inter> {s. \<not>P \<longrightarrow> s \<in> H'})
                      hs a b" apply (cases P, auto simp: P notP) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres r xf (\<lambda>s. (P \<longrightarrow> G s) \<and> (\<not> P \<longrightarrow> H s)) ({s. P \<longrightarrow> s \<in> G'} \<inter> {s. \<not> P \<longrightarrow> s \<in> H'}) hs a b proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma cmdb_node_relation_mdbNext:
  "cmdbnode_relation n n'
         \<Longrightarrow> mdbNext_CL (mdb_node_lift n') = mdbNext n" by (simp add:cmdbnode_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmdbnode_relation n n' \<Longrightarrow> mdbNext_CL (mdb_node_lift n') = mdbNext n
theory CSpace_C

lemma cslift_ptr_safe:
  "cslift x ptr = Some a
  \<Longrightarrow> ptr_safe ptr (hrs_htd (t_hrs_' (globals x)))" apply (rule_tac h = "fst (t_hrs_' (globals x))"
        in lift_t_ptr_safe[where g = c_guard]) apply (fastforce simp add:typ_heap_simps hrs_htd_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cslift x ptr = Some a \<Longrightarrow> ptr_safe ptr (hrs_htd (t_hrs_' (globals x))) proof (prove)
goal (1 subgoal):
 1. cslift x ptr = Some a \<Longrightarrow> clift (fst (t_hrs_' (globals x)), hrs_htd (t_hrs_' (globals x))) ptr = Some ?x proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma is_aligned_3_prev:
  "\<lbrakk> valid_mdb' s; pspace_aligned' s; ctes_of s p = Some cte \<rbrakk>
  \<Longrightarrow> is_aligned (mdbPrev (cteMDBNode cte)) 3" apply (cases "mdbPrev (cteMDBNode cte) = 0", simp) apply (drule (2) valid_mdb_ctes_of_prev) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb' s; pspace_aligned' s; ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> is_aligned (mdbPrev (cteMDBNode cte)) 3 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb' s; pspace_aligned' s; ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (mdbPrev (cteMDBNode cte)) 3 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; cte_wp_at' (\<lambda>_. True) (mdbPrev (cteMDBNode cte)) s\<rbrakk> \<Longrightarrow> is_aligned (mdbPrev (cteMDBNode cte)) 3 proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma is_aligned_3_next:
  "\<lbrakk> valid_mdb' s; pspace_aligned' s; ctes_of s p = Some cte \<rbrakk>
  \<Longrightarrow> is_aligned (mdbNext (cteMDBNode cte)) 3" apply (cases "mdbNext (cteMDBNode cte) = 0", simp) apply (drule (2) valid_mdb_ctes_of_next) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb' s; pspace_aligned' s; ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> is_aligned (mdbNext (cteMDBNode cte)) 3 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb' s; pspace_aligned' s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0\<rbrakk> \<Longrightarrow> is_aligned (mdbNext (cteMDBNode cte)) 3 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; cte_wp_at' (\<lambda>_. True) (mdbNext (cteMDBNode cte)) s\<rbrakk> \<Longrightarrow> is_aligned (mdbNext (cteMDBNode cte)) 3 proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma mdbPrev_CL_mdb_node_lift_mask [simp]:
 "mdbPrev_CL (mdb_node_lift mdbNode) && ~~ mask 3
 = mdbPrev_CL (mdb_node_lift mdbNode)" apply (simp add: mdb_node_lift_def mask_def  word_bw_assocs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbPrev_CL (mdb_node_lift mdbNode) && ~~ mask 3 = mdbPrev_CL (mdb_node_lift mdbNode) proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma mdbPrev_CL_mdb_node_lift_eq_mdbPrev:
  "cmdbnode_relation n n' \<Longrightarrow>  (mdbPrev_CL (mdb_node_lift n')) =(mdbPrev n)" by (erule cmdbnode_relationE, fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmdbnode_relation n n' \<Longrightarrow> mdbPrev_CL (mdb_node_lift n') = mdbPrev n
theory CSpace_C

lemma mdbNext_not_zero_eq_simpler:
  "cmdbnode_relation n n' \<Longrightarrow> (mdbNext n \<noteq> 0) = (mdbNext_CL (mdb_node_lift n') \<noteq> 0)" apply clarsimp apply (erule cmdbnode_relationE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmdbnode_relation n n' \<Longrightarrow> (mdbNext n \<noteq> 0) = (mdbNext_CL (mdb_node_lift n') \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. cmdbnode_relation n n' \<Longrightarrow> (mdbNext n = 0) = (mdbNext_CL (mdb_node_lift n') = 0) proof (prove)
goal (1 subgoal):
 1. n = mdb_node_to_H (mdb_node_lift n') \<Longrightarrow> (mdbNext n = 0) = (mdbNext_CL (mdb_node_lift n') = 0) proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma mdbPrev_not_zero_eq_simpler:
  "cmdbnode_relation n n' \<Longrightarrow> (mdbPrev n \<noteq> 0) = (mdbPrev_CL (mdb_node_lift n') \<noteq> 0)" apply clarsimp apply (erule cmdbnode_relationE) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cmdbnode_relation n n' \<Longrightarrow> (mdbPrev n \<noteq> 0) = (mdbPrev_CL (mdb_node_lift n') \<noteq> 0) proof (prove)
goal (1 subgoal):
 1. cmdbnode_relation n n' \<Longrightarrow> (mdbPrev n = 0) = (mdbPrev_CL (mdb_node_lift n') = 0) proof (prove)
goal (1 subgoal):
 1. n = mdb_node_to_H (mdb_node_lift n') \<Longrightarrow> (mdbPrev n = 0) = (mdbPrev_CL (mdb_node_lift n') = 0) proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma deletedIRQHandler_ccorres:
  "ccorres dc xfdc
         (\<lambda>s. ucast irq \<le> (ucast Kernel_C.maxIRQ :: machine_word))
         (UNIV \<inter> {s. irq_' s = ucast irq}) []
         (deletedIRQHandler irq)
         (Call deletedIRQHandler_'proc )" apply (cinit simp del: return_bind) apply (ctac add: setIRQState_ccorres) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ) (UNIV \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>) [] (deletedIRQHandler irq) (Call deletedIRQHandler_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q9 ?Q'9 [SKIP] (setIRQState irqstate.IRQInactive irq) (CALL setIRQState_'proc(SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive,\<acute>irq))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; s' \<in> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ; s' \<in> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. UCAST(10 \<rightarrow> 32) irq \<le> UCAST(32 signed \<rightarrow> 32) Kernel_C.maxIRQ)) s \<and> s' \<in> {s. irq_'_update (\<lambda>_. irq_' s) (irqState_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) Kernel_C.IRQInactive) s) \<in> UNIV \<inter> \<lbrace>\<acute>irqState = irqstate_to_C irqstate.IRQInactive\<rbrace> \<inter> \<lbrace>\<acute>irq = UCAST(10 \<rightarrow> 32) irq\<rbrace>} proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma region_actually_is_bytes_subset:
  "region_actually_is_bytes' ptr sz htd
    \<Longrightarrow> {ptr' ..+ sz'} \<subseteq> {ptr ..+ sz}
    \<Longrightarrow> region_actually_is_bytes' ptr' sz' htd" by (auto simp: region_actually_is_bytes'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>region_actually_is_bytes' ptr sz htd; {ptr'..+sz'} \<subseteq> {ptr..+sz}\<rbrakk> \<Longrightarrow> region_actually_is_bytes' ptr' sz' htd
theory CSpace_C

lemma intvl_both_le:
  "\<lbrakk> a \<le> x; unat x + y \<le> unat a + b \<rbrakk>
    \<Longrightarrow>  {x ..+ y} \<le> {a ..+ b}" apply (rule order_trans[OF _ intvl_sub_offset[where x="x - a"]]) apply (simp, rule order_refl) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> x; unat x + y \<le> unat a + b\<rbrakk> \<Longrightarrow> {x..+y} \<subseteq> {a..+b} proof (prove)
goal (2 subgoals):
 1. \<lbrakk>a \<le> x; unat x + y \<le> unat a + b\<rbrakk> \<Longrightarrow> {x..+y} \<subseteq> {a + (x - a)..+?y1}
 2. \<lbrakk>a \<le> x; unat x + y \<le> unat a + b\<rbrakk> \<Longrightarrow> unat (x - a) + ?y1 \<le> b proof (prove)
goal (1 subgoal):
 1. \<lbrakk>a \<le> x; unat x + y \<le> unat a + b\<rbrakk> \<Longrightarrow> unat (x - a) + y \<le> b proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma intvl_close_Un:
  "y = x + of_nat n
    \<Longrightarrow> ({x ..+ n} \<union> {y ..+ m}) = {x ..+ n + m}" apply ((simp add: intvl_def, safe, simp_all,
    simp_all only: of_nat_add[symmetric]); (rule exI, strengthen refl)) apply simp_all apply (rule ccontr) apply (drule_tac x="k - n" in spec) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. y = x + word_of_nat n \<Longrightarrow> {x..+n} \<union> {y..+m} = {x..+n + m} proof (prove)
goal (3 subgoals):
 1. \<And>k. \<lbrakk>y = x + word_of_nat n; k < n\<rbrakk> \<Longrightarrow> True \<and> k < n + m
 2. \<And>k. \<lbrakk>y = x + word_of_nat n; k < m\<rbrakk> \<Longrightarrow> True \<and> n + k < n + m
 3. \<And>k. \<lbrakk>y = x + word_of_nat n; \<forall>ka. word_of_nat k = word_of_nat (n + ka) \<longrightarrow> \<not> ka < m; k < n + m\<rbrakk> \<Longrightarrow> True \<and> k < n proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>y = x + word_of_nat n; \<forall>ka. word_of_nat k = word_of_nat n + word_of_nat ka \<longrightarrow> \<not> ka < m; k < n + m\<rbrakk> \<Longrightarrow> k < n proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>y = x + word_of_nat n; \<forall>ka. word_of_nat k = word_of_nat n + word_of_nat ka \<longrightarrow> \<not> ka < m; k < n + m; \<not> k < n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>k. \<lbrakk>y = x + word_of_nat n; k < n + m; \<not> k < n; word_of_nat k = word_of_nat n + word_of_nat (k - n) \<longrightarrow> \<not> k - n < m\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma ctes_of_untyped_zero_rf_sr_case:
  "\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr;
      untyped_ranges_zero' s \<rbrakk>
    \<Longrightarrow> case untypedZeroRange (cteCap cte)
               of None \<Rightarrow> True
    | Some (start, end) \<Rightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'" by (simp split: option.split add: ctes_of_untyped_zero_rf_sr)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; (s, s') \<in> rf_sr; untyped_ranges_zero' s\<rbrakk> \<Longrightarrow> case untypedZeroRange (cteCap cte) of None \<Rightarrow> True | Some (start, end) \<Rightarrow> region_actually_is_bytes start (unat (end + 1 - start)) s' \<and> heap_list (hrs_mem (t_hrs_' (globals s'))) (unat (end + 1 - start)) start = replicate (unat (end + 1 - start)) 0
theory CSpace_C

lemma gsUntypedZeroRanges_update_helper:
  "(\<sigma>, s) \<in> rf_sr
    \<Longrightarrow> (zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s))
            \<longrightarrow> zero_ranges_are_zero (f (gsUntypedZeroRanges \<sigma>)) (t_hrs_' (globals s)))
    \<Longrightarrow> (gsUntypedZeroRanges_update f \<sigma>, s) \<in> rf_sr" by (clarsimp simp: rf_sr_def cstate_relation_def Let_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<sigma>, s) \<in> rf_sr; zero_ranges_are_zero (gsUntypedZeroRanges \<sigma>) (t_hrs_' (globals s)) \<longrightarrow> zero_ranges_are_zero (f (gsUntypedZeroRanges \<sigma>)) (t_hrs_' (globals s))\<rbrakk> \<Longrightarrow> (gsUntypedZeroRanges_update f \<sigma>, s) \<in> rf_sr
theory CSpace_C

lemma heap_list_zero_Ball_intvl:
  "heap_list_is_zero hmem ptr n = (\<forall>x \<in> {ptr ..+ n}. hmem x = 0)" apply safe apply (erule heap_list_h_eq_better) apply (simp add: heap_list_rpbs) apply (rule trans[OF heap_list_h_eq2 heap_list_rpbs]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (heap_list hmem n ptr = replicate n 0) = (\<forall>x\<in>{ptr..+n}. hmem x = 0) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>heap_list hmem n ptr = replicate n 0; x \<in> {ptr..+n}\<rbrakk> \<Longrightarrow> hmem x = 0
 2. \<forall>x\<in>{ptr..+n}. hmem x = 0 \<Longrightarrow> heap_list hmem n ptr = replicate n 0 proof (prove)
goal (2 subgoals):
 1. \<And>x. heap_list hmem n ptr = replicate n 0 \<Longrightarrow> heap_list hmem n ptr = heap_list (\<lambda>a. 0) n ptr
 2. \<forall>x\<in>{ptr..+n}. hmem x = 0 \<Longrightarrow> heap_list hmem n ptr = replicate n 0 proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>{ptr..+n}. hmem x = 0 \<Longrightarrow> heap_list hmem n ptr = replicate n 0 proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>\<forall>x\<in>{ptr..+n}. hmem x = 0; x \<in> {ptr..+n}\<rbrakk> \<Longrightarrow> hmem x = 0 proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma untypedZeroRange_not_device:
  "untypedZeroRange cap = Some r
    \<Longrightarrow> \<not> capIsDevice cap" by (clarsimp simp: untypedZeroRange_def cong: if_cong)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. untypedZeroRange cap = Some r \<Longrightarrow> \<not> capIsDevice cap
theory CSpace_C

lemma updateTrackedFreeIndex_forward_noop_ccorres:
  "ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap
              \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) o cteCap) slot
          and valid_objs' and untyped_ranges_zero') UNIV hs
      (updateTrackedFreeIndex slot idx) Skip"
  (is "ccorres dc xfdc ?P UNIV _ _ _") apply (rule ccorres_name_pre) apply (rule ccorres_guard_imp2,
     rule_tac cap'="cteCap (the (ctes_of s slot))" in updateTrackedFreeIndex_noop_ccorres) apply (clarsimp simp: cte_wp_at_ctes_of region_actually_is_bytes'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') UNIV hs (updateTrackedFreeIndex slot idx) SKIP proof (prove)
goal (1 subgoal):
 1. \<And>s. (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s \<Longrightarrow> ccorres dc xfdc (\<lambda>s'. s' = s) UNIV hs (updateTrackedFreeIndex slot idx) SKIP proof (prove)
goal (1 subgoal):
 1. \<And>s sa s'. \<lbrakk>(cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') s; (sa, s') \<in> rf_sr; sa = s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> idx \<le> 2 ^ capBlockSize cap \<and> (capFreeIndex cap \<le> idx \<or> cteCap (the (ctes_of s slot)) = cap)) \<circ> cteCap) slot and valid_objs' and untyped_ranges_zero') sa \<and> s' \<in> {sa. \<not> capIsDevice (cteCap (the (ctes_of s slot))) \<longrightarrow> region_actually_is_bytes (capPtr (cteCap (the (ctes_of s slot))) + word_of_nat idx) (capFreeIndex (cteCap (the (ctes_of s slot))) - idx) sa \<and> heap_list (hrs_mem (t_hrs_' (globals sa))) (capFreeIndex (cteCap (the (ctes_of s slot))) - idx) (capPtr (cteCap (the (ctes_of s slot))) + word_of_nat idx) = replicate (capFreeIndex (cteCap (the (ctes_of s slot))) - idx) 0} proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma not_irq_or_arch_cap_case:
  "\<lbrakk>\<not>isIRQHandlerCap cap; \<not> isArchCap \<top> cap\<rbrakk> \<Longrightarrow>
   (case cap of IRQHandlerCap irq \<Rightarrow> f irq | ArchObjectCap acap \<Rightarrow> g acap | _ \<Rightarrow> h) = h" by (case_tac cap; clarsimp simp: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> isIRQHandlerCap cap; \<not> isArchCap (\<lambda>_. True) cap\<rbrakk> \<Longrightarrow> (case cap of capability.IRQHandlerCap irq \<Rightarrow> f irq | capability.ArchObjectCap acap \<Rightarrow> g acap | _ \<Rightarrow> h) = h
theory CSpace_C

lemma ccorres_return_void_C:
  "ccorres dc xfdc \<top> UNIV (SKIP # hs) (return rv) (return_void_C)" apply (rule ccorres_from_vcg_throws) apply (simp add: return_def) apply (rule allI, rule conseqPre) apply vcg apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>_. True) UNIV (SKIP # hs) (return rv) return_void_C proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_void_C {},{s. \<exists>(rv, \<sigma>')\<in>fst (return rv \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)} proof (prove)
goal (1 subgoal):
 1. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr} return_void_C {},{s. (\<sigma>, s) \<in> rf_sr} proof (prove)
goal (2 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> (?P'8 \<sigma>) return_void_C {},{s. (\<sigma>, s) \<in> rf_sr}
 2. \<And>\<sigma>. {s. (\<sigma>, s) \<in> rf_sr} \<subseteq> ?P'8 \<sigma> proof (prove)
goal (1 subgoal):
 1. \<And>\<sigma>. {s. (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. (\<sigma>, s\<lparr>global_exn_var_' := Return\<rparr>) \<in> rf_sr} proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma gen_framesize_to_H_is_framesize_to_H_if_not_ARMSmallPage:
  " c\<noteq>scast Kernel_C.ARMSmallPage \<Longrightarrow>gen_framesize_to_H c =  framesize_to_H c" by (simp add: gen_framesize_to_H_def framesize_to_H_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. c \<noteq> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<Longrightarrow> gen_framesize_to_H c = framesize_to_H c
theory CSpace_C

lemma generic_frame_cap_get_capFVMRights_spec:
  "\<forall>s. \<Gamma> \<turnstile> {s} Call generic_frame_cap_get_capFVMRights_'proc
     {t. ret__unsigned_long_' t = generic_frame_cap_get_capFVMRights_CL (cap_lift (cap_' s))}" apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: generic_frame_cap_get_capFVMRights_CL_def
                        cap_lift_small_frame_cap cap_lift_frame_cap
                        cap_small_frame_cap_lift_def cap_frame_cap_lift_def) by (simp add: cap_lift_def Let_def Kernel_C.VMNoAccess_def split: if_split)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> {s} Call generic_frame_cap_get_capFVMRights_'proc \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFVMRights_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. {s} \<subseteq> \<lbrace>\<forall>v t. \<^bsup>t\<^esup>ret__unsigned = cap_get_tag \<acute>cap \<longrightarrow> (cap_small_frame_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag \<acute>cap) \<longrightarrow> cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift \<acute>cap) \<longrightarrow> UCAST(32 \<rightarrow> 32) (cap_small_frame_cap_CL.capFVMRights_CL (cap_small_frame_cap_lift \<acute>cap)) = generic_frame_cap_get_capFVMRights_CL (cap_lift \<^bsup>s\<^esup>cap))) \<and> (cap_small_frame_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag \<acute>cap) \<longrightarrow> (cap_frame_cap = UCAST(32 \<rightarrow> 32 signed) (cap_get_tag \<acute>cap) \<longrightarrow> cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_frame_cap \<and> (\<forall>t. \<^bsup>t\<^esup>ret__unsigned = cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift \<acute>cap) \<longrightarrow> UCAST(32 \<rightarrow> 32) (cap_frame_cap_CL.capFVMRights_CL (cap_frame_cap_lift \<acute>cap)) = generic_frame_cap_get_capFVMRights_CL (cap_lift \<^bsup>s\<^esup>cap))) \<and> (cap_frame_cap \<noteq> UCAST(32 \<rightarrow> 32 signed) (cap_get_tag \<acute>cap) \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess = generic_frame_cap_get_capFVMRights_CL (cap_lift \<^bsup>s\<^esup>cap)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>ret__unsigned_' t = cap_get_tag (cap_' s); cap_get_tag (cap_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_small_frame_cap; cap_get_tag (cap_' s) \<noteq> SCAST(32 signed \<rightarrow> 32) cap_frame_cap\<rbrakk> \<Longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.VMNoAccess = (case cap_lift (cap_' s) of None \<Rightarrow> 0 | Some (Cap_small_frame_cap xa) \<Rightarrow> cap_small_frame_cap_CL.capFVMRights_CL xa | Some (Cap_frame_cap xa) \<Rightarrow> cap_frame_cap_CL.capFVMRights_CL xa | Some _ \<Rightarrow> 0)
theory CSpace_C

lemma cap_zombie_cap_get_capZombieBits_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_zombie_cap \<rbrace>
       \<acute>ret__unsigned_long :== PROC cap_zombie_cap_get_capZombieBits(\<acute>cap)
       \<lbrace>\<acute>ret__unsigned_long = get_capZombieBits_CL (cap_zombie_cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" apply vcg apply (clarsimp simp: get_capZombieBits_CL_def word_sle_def mask_def
                        isZombieTCB_C_def ZombieTCB_C_def Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap\<rbrace> Call cap_zombie_cap_get_capZombieBits_'proc \<lbrace>\<acute>ret__unsigned_long = get_capZombieBits_CL (cap_zombie_cap_lift \<^bsup>s\<^esup>cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>cap. cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<Longrightarrow> cap_get_tag cap = SCAST(32 signed \<rightarrow> 32) cap_zombie_cap \<and> (\<forall>ret__unsigned. ret__unsigned = capZombieType_CL (cap_zombie_cap_lift cap) \<longrightarrow> 0 \<le>s 5 \<and> 5 <s 0x20 \<and> (UCAST(32 \<rightarrow> 32) (capZombieType_CL (cap_zombie_cap_lift cap)) = 1 << unat 5 \<longrightarrow> SCAST(32 signed \<rightarrow> 32) 4 = get_capZombieBits_CL (cap_zombie_cap_lift cap)) \<and> (UCAST(32 \<rightarrow> 32) (capZombieType_CL (cap_zombie_cap_lift cap)) \<noteq> 1 << unat 5 \<longrightarrow> 0 \<le>s 5 \<and> 5 <s 0x20 \<and> UCAST(32 \<rightarrow> 32) (capZombieType_CL (cap_zombie_cap_lift cap)) && (1 << unat 5) - 1 = get_capZombieBits_CL (cap_zombie_cap_lift cap))) proof (prove)
goal:
No subgoals!
theory CSpace_C

lemma ctcb_ptr_to_tcb_ptr_mask':
  "is_aligned (ctcb_ptr_to_tcb_ptr (tcb_Ptr x)) (objBits (undefined :: tcb)) \<Longrightarrow>
     ctcb_ptr_to_tcb_ptr (tcb_Ptr x) = x && ~~ mask (objBits (undefined :: tcb))" apply (simp add: ctcb_ptr_to_tcb_ptr_def) apply (drule_tac d=ctcb_offset in is_aligned_add_helper) apply (simp add: objBits_simps' ctcb_offset_defs) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_aligned (ctcb_ptr_to_tcb_ptr (tcb_Ptr x)) (objBits undefined) \<Longrightarrow> ctcb_ptr_to_tcb_ptr (tcb_Ptr x) = x && ~~ mask (objBits undefined) proof (prove)
goal (1 subgoal):
 1. is_aligned (x - ctcb_offset) (objBits undefined) \<Longrightarrow> x - ctcb_offset = x && ~~ mask (objBits undefined) proof (prove)
goal (2 subgoals):
 1. ctcb_offset < 2 ^ objBits undefined
 2. x - ctcb_offset + ctcb_offset && mask (objBits undefined) = ctcb_offset \<and> x - ctcb_offset + ctcb_offset && ~~ mask (objBits undefined) = x - ctcb_offset \<Longrightarrow> x - ctcb_offset = x && ~~ mask (objBits undefined) proof (prove)
goal (1 subgoal):
 1. x - ctcb_offset + ctcb_offset && mask (objBits undefined) = ctcb_offset \<and> x - ctcb_offset + ctcb_offset && ~~ mask (objBits undefined) = x - ctcb_offset \<Longrightarrow> x - ctcb_offset = x && ~~ mask (objBits undefined) proof (prove)
goal:
No subgoals!