kings-crown/FVELER_Isabelle huggingface dataset:
theory ArchKernelInit_AI

lemma cap_refs_respects_device_region_init[simp]:
  "cap_refs_respects_device_region init_A_st" apply (clarsimp simp: cap_refs_respects_device_region_def) apply (frule cte_wp_at_caps_of_state[THEN iffD1]) apply clarsimp apply (subst(asm) caps_of_state_init_A_st_Null) apply (clarsimp simp: cte_wp_at_caps_of_state cap_range_respects_device_region_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap_refs_respects_device_region init_A_st proof (prove)
goal (1 subgoal):
 1. \<And>a b. cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c init_A_st) (a, b) init_A_st \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c init_A_st) (a, b) init_A_st; \<exists>cap. caps_of_state init_A_st (a, b) = Some cap \<and> \<not> cap_range_respects_device_region cap init_A_st\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c init_A_st) (a, b) init_A_st; caps_of_state init_A_st (a, b) = Some cap; \<not> cap_range_respects_device_region cap init_A_st\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>cte_wp_at (\<lambda>c. \<not> cap_range_respects_device_region c init_A_st) (a, b) init_A_st; (if cte_wp_at (\<lambda>_. True) (a, b) init_A_st then Some NullCap else None) = Some cap; \<not> cap_range_respects_device_region cap init_A_st\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma doMachineOp_ksPSpace_inv[wp]:
  "\<lbrace>\<lambda>s. P (ksPSpace s)\<rbrace> doMachineOp f \<lbrace>\<lambda>ya s. P (ksPSpace s)\<rbrace>" by (simp add:doMachineOp_def split_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksPSpace s)\<rbrace> doMachineOp f \<lbrace>\<lambda>ya s. P (ksPSpace s)\<rbrace>
theory PageTableDuplicates

lemma transferCapsToSlots_duplicates'[wp]:
 "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
  transferCapsToSlots ep buffer n caps slots mi
  \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" by (rule transferCapsToSlots_pres1; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> transferCapsToSlots ep buffer n caps slots mi \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
theory PageTableDuplicates

lemma koTypeOf_pte:
  "koTypeOf ko = ArchT PTET \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte)"
  "archTypeOf ako = PTET \<Longrightarrow> \<exists>pte. ako = KOPTE pte" apply (case_tac ko; simp) apply (rename_tac arch_kernel_object) apply (case_tac arch_kernel_object; simp) apply (case_tac ako; simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (koTypeOf ko = ArchT PTET \<Longrightarrow> \<exists>pte. ko = KOArch (KOPTE pte)) &&& (archTypeOf ako = PTET \<Longrightarrow> \<exists>pte. ako = KOPTE pte) proof (prove)
goal (2 subgoals):
 1. \<And>x8. \<lbrakk>archTypeOf x8 = PTET; ko = KOArch x8\<rbrakk> \<Longrightarrow> \<exists>pte. x8 = KOPTE pte
 2. archTypeOf ako = PTET \<Longrightarrow> \<exists>pte. ako = KOPTE pte proof (prove)
goal (2 subgoals):
 1. \<And>arch_kernel_object. \<lbrakk>archTypeOf arch_kernel_object = PTET; ko = KOArch arch_kernel_object\<rbrakk> \<Longrightarrow> \<exists>pte. arch_kernel_object = KOPTE pte
 2. archTypeOf ako = PTET \<Longrightarrow> \<exists>pte. ako = KOPTE pte proof (prove)
goal (1 subgoal):
 1. archTypeOf ako = PTET \<Longrightarrow> \<exists>pte. ako = KOPTE pte proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma is_aligned_plus_bound:
  assumes al: "is_aligned p sz"
  assumes cmp: "sz \<le> lz"
  assumes b:  "b \<le> (2::word32) ^ sz - 1"
  assumes bound : "p < 2 ^ lz"
  assumes sz: "sz < word_bits"
  shows "p + b < 2 ^ lz" proof - have lower:"p + b \<le> p + (2 ^ sz - 1)" apply (rule word_plus_mono_right[OF b]) apply (rule is_aligned_no_overflow'[OF al]) done show ?thesis using bound sz apply - apply (rule le_less_trans[OF lower]) apply (rule ccontr) apply (simp add:not_less) apply (drule neg_mask_mono_le[where n = sz]) apply (subst (asm) is_aligned_neg_mask_eq) apply (rule is_aligned_weaken[OF is_aligned_triv cmp]) apply (subst (asm) is_aligned_add_helper[THEN conjunct2,OF al]) apply (simp add:word_bits_def) apply simp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. p + b < 2 ^ lz proof (state)
goal (1 subgoal):
 1. p + b < 2 ^ lz proof (prove)
goal (1 subgoal):
 1. p + b \<le> p + (2 ^ sz - 1) proof (prove)
goal (1 subgoal):
 1. p \<le> p + (2 ^ sz - 1) proof (prove)
goal:
No subgoals! proof (state)
this:
p + b \<le> p + (2 ^ sz - 1)

goal (1 subgoal):
 1. p + b < 2 ^ lz proof (prove)
goal (1 subgoal):
 1. p + b < 2 ^ lz proof (prove)
using this:
p < 2 ^ lz
sz < word_bits

goal (1 subgoal):
 1. p + b < 2 ^ lz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < 2 ^ lz; sz < word_bits\<rbrakk> \<Longrightarrow> p + b < 2 ^ lz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < 2 ^ lz; sz < word_bits\<rbrakk> \<Longrightarrow> p + (2 ^ sz - 1) < 2 ^ lz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < 2 ^ lz; sz < word_bits; \<not> p + (2 ^ sz - 1) < 2 ^ lz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < 2 ^ lz; sz < word_bits; 2 ^ lz \<le> p + (2 ^ sz - 1)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < 2 ^ lz; sz < word_bits; 2 ^ lz && ~~ mask sz \<le> p + (2 ^ sz - 1) && ~~ mask sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p < 2 ^ lz; sz < word_bits\<rbrakk> \<Longrightarrow> is_aligned (2 ^ lz) sz
 2. \<lbrakk>p < 2 ^ lz; sz < word_bits; 2 ^ lz \<le> p + (2 ^ sz - 1) && ~~ mask sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < 2 ^ lz; sz < word_bits; 2 ^ lz \<le> p + (2 ^ sz - 1) && ~~ mask sz\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>p < 2 ^ lz; sz < word_bits\<rbrakk> \<Longrightarrow> 2 ^ sz - 1 < 2 ^ sz
 2. \<lbrakk>p < 2 ^ lz; sz < word_bits; 2 ^ lz \<le> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p < 2 ^ lz; sz < word_bits; 2 ^ lz \<le> p\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
p + b < 2 ^ lz

goal:
No subgoals!
theory PageTableDuplicates

lemma vs_ptr_align_upbound:
  "vs_ptr_align a \<le> 6" by (simp add:vs_ptr_align_def
      split:Structures_H.kernel_object.splits
      arch_kernel_object.splits
      ARM_H.pde.splits ARM_H.pte.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. vs_ptr_align a \<le> 6
theory PageTableDuplicates

lemma foldr_data_map_insert[simp]:
 "foldr (\<lambda>addr map a. if a = addr then Some b else map a)
 = foldr (\<lambda>addr. data_map_insert addr b)" apply (rule ext)+ apply (simp add:data_map_insert_def[abs_def] fun_upd_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. foldr (\<lambda>addr map a. if a = addr then Some b else map a) = foldr (\<lambda>addr. data_map_insert addr b) proof (prove)
goal (1 subgoal):
 1. \<And>x xa xb. foldr (\<lambda>addr map a. if a = addr then Some b else map a) x xa xb = foldr (\<lambda>addr. data_map_insert addr b) x xa xb proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma none_in_new_cap_addrs:
  "\<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits;
  pspace_no_overlap' ptr (objBitsKO obj + us) s;
  pspace_aligned' s\<rbrakk>
  \<Longrightarrow> \<forall>x\<in>set (new_cap_addrs (2^us) ptr obj). ksPSpace s x = None" apply (rule ccontr,clarsimp) apply (drule not_in_new_cap_addrs[rotated - 1]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (new_cap_addrs (2 ^ us) ptr obj). ksPSpace s x = None proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; pspace_aligned' s; x \<in> set (new_cap_addrs (2 ^ us) ptr obj); ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>x y. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; x \<in> set (new_cap_addrs (2 ^ us) ptr obj); ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> is_aligned (?ptr8 x y) (objBitsKO (?obj8 x y) + ?us8 x y)
 2. \<And>x y. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; x \<in> set (new_cap_addrs (2 ^ us) ptr obj); ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> objBitsKO (?obj8 x y) + ?us8 x y < word_bits
 3. \<And>x y. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; x \<in> set (new_cap_addrs (2 ^ us) ptr obj); ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> pspace_no_overlap' (?ptr8 x y) (objBitsKO (?obj8 x y) + ?us8 x y) s
 4. \<And>x y. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; x \<in> set (new_cap_addrs (2 ^ us) ptr obj); ksPSpace s x = Some y\<rbrakk> \<Longrightarrow> ksPSpace s (?dest8 x y) = Some (?ko8 x y)
 5. \<And>x y. \<lbrakk>is_aligned ptr (objBitsKO obj + us); objBitsKO obj + us < word_bits; pspace_no_overlap' ptr (objBitsKO obj + us) s; x \<in> set (new_cap_addrs (2 ^ us) ptr obj); ksPSpace s x = Some y; ?dest8 x y \<notin> set (new_cap_addrs (2 ^ ?us8 x y) (?ptr8 x y) (?obj8 x y))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma is_aligned_armKSGlobalPD:
  "valid_arch_state' s
    \<Longrightarrow> is_aligned (armKSGlobalPD (ksArchState s)) pdBits" by (clarsimp simp: valid_arch_state'_def page_directory_at'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_arch_state' s \<Longrightarrow> is_aligned (armKSGlobalPD (ksArchState s)) pdBits
theory PageTableDuplicates

lemma new_CapTable_bound:
  "range_cover (ptr :: obj_ref) sz (APIType_capBits tp us) n
    \<Longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28" apply (frule range_cover.sz) apply (drule range_cover.sz(2)) apply (clarsimp simp: APIType_capBits_def objBits_simps' word_bits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (APIType_capBits tp us) n \<Longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz < LENGTH(32); APIType_capBits tp us \<le> sz\<rbrakk> \<Longrightarrow> tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> us < 28 proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma get_asid_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
  getObject param_b \<lbrace>\<lambda>(pool::asidpool) s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add:getObject_def split_def| wp)+ apply (simp add:loadObject_default_def|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> getObject param_b \<lbrace>\<lambda>pool s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>map x. \<lbrace>?B2 map x\<rbrace> loadObject_default param_b (fst x) (snd (lookupAround2 param_b map)) (snd x) \<lbrace>\<lambda>pool s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
 2. \<And>map. \<lbrace>?B1 map\<rbrace> assert_opt (fst (lookupAround2 param_b map)) \<lbrace>?B2 map\<rbrace>
 3. \<lbrace>?Q\<rbrace> gets ksPSpace \<lbrace>?B1\<rbrace>
 4. \<And>s. vs_valid_duplicates' (ksPSpace s) \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma set_asid_pool_valid_duplicates'[wp]:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
  setObject a (pool::asidpool)
  \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (clarsimp simp: setObject_def split_def valid_def in_monad
                        projectKOs pspace_aligned'_def ps_clear_upd
                        objBits_def[symmetric] lookupAround2_char1
                 split: if_split_asm) apply (frule pspace_storable_class.updateObject_type[where v = pool,simplified]) apply (clarsimp simp:updateObject_default_def assert_def bind_def
    alignCheck_def in_monad when_def alignError_def magnitudeCheck_def
    assert_opt_def return_def fail_def typeError_def
    split:if_splits option.splits Structures_H.kernel_object.splits) apply (erule valid_duplicates'_non_pd_pt_I[rotated 3],clarsimp+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> setObject a pool \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba s''a obj'. \<lbrakk>vs_valid_duplicates' (ksPSpace s); aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default pool ba a aa (snd (lookupAround2 a (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(aa \<mapsto> obj')) proof (prove)
goal (1 subgoal):
 1. \<And>s aa ba s''a obj'. \<lbrakk>vs_valid_duplicates' (ksPSpace s); aa \<le> a; ksPSpace s aa = Some ba; \<forall>z. aa < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default pool ba a aa (snd (lookupAround2 a (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(aa \<mapsto> obj')) proof (prove)
goal (2 subgoals):
 1. \<And>s ba s''a aa. \<lbrakk>ArchT ASIDPoolT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 a (ksPSpace s)) = None; (aa, s''a) \<in> fst (projectKO ba s); a && mask (objBits pool) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOArch (KOASIDPool pool)))
 2. \<And>s ba s''a x2 aa. \<lbrakk>ArchT ASIDPoolT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> a \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 a (ksPSpace s)) = Some x2; \<not> x2 - a < 2 ^ objBits pool; (aa, s''a) \<in> fst (projectKO ba s); a && mask (objBits pool) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOArch (KOASIDPool pool))) proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma checkMappingPPtr_SmallPage:
  "\<lbrace>\<top>\<rbrace> checkMappingPPtr word ARMSmallPage (Inl p)
           \<lbrace>\<lambda>x s. ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s\<rbrace>,-" apply (simp add:checkMappingPPtr_def) apply (wp unlessE_wp getPTE_wp |wpc|simp add:)+ apply (clarsimp simp:ko_wp_at'_def obj_at'_def) apply (clarsimp simp:projectKO_def projectKO_opt_pte
    return_def fail_def vs_entry_align_def
    split:kernel_object.splits
    arch_kernel_object.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> checkMappingPPtr word ARMSmallPage (Inl p) \<lbrace>\<lambda>x. ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE pte <- liftE (getObject p);
case pte of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case ARMSmallPage of ARMLargePage \<Rightarrow> unlessE (base = addrFromPPtr word) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.SmallPagePTE base x xa xb xc \<Rightarrow> case ARMSmallPage of ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr word) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot
odE \<lbrace>\<lambda>x. ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>ko. ko_at' ko p s \<longrightarrow> (\<exists>x xa xb xc. ko = ARM_H.SmallPagePTE (addrFromPPtr word) x xa xb xc) \<longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s proof (prove)
goal (1 subgoal):
 1. \<And>s koa x xa xb xc. \<lbrakk>ksPSpace s p = Some koa; is_aligned p (objBitsKO koa); fst (projectKO koa s) = {(ARM_H.SmallPagePTE (addrFromPPtr word) x xa xb xc, s)}; ps_clear p (objBitsKO koa) s\<rbrakk> \<Longrightarrow> vs_entry_align koa = 0 proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma checkMappingPPtr_Section:
  "\<lbrace>\<top>\<rbrace> checkMappingPPtr word ARMSection (Inr p)
           \<lbrace>\<lambda>x s. ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s\<rbrace>,-" apply (simp add:checkMappingPPtr_def) apply (wp unlessE_wp getPDE_wp |wpc|simp add:)+ apply (clarsimp simp:ko_wp_at'_def obj_at'_def) apply (clarsimp simp:projectKO_def projectKO_opt_pde
    return_def fail_def vs_entry_align_def
    split:kernel_object.splits
    arch_kernel_object.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> checkMappingPPtr word ARMSection (Inr p) \<lbrace>\<lambda>x. ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> doE pde <- liftE (getObject p);
case pde of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case ARMSection of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr word) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.SuperSectionPDE base x xa xb xc xd \<Rightarrow> case ARMSection of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr word) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot
odE \<lbrace>\<lambda>x. ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<forall>ko. ko_at' ko p s \<longrightarrow> (\<exists>x xa xb xc xd xe. ko = ARM_H.SectionPDE (addrFromPPtr word) x xa xb xc xd xe) \<longrightarrow> ko_wp_at' (\<lambda>ko. vs_entry_align ko = 0) p s proof (prove)
goal (1 subgoal):
 1. \<And>s koa x xa xb xc xd xe. \<lbrakk>ksPSpace s p = Some koa; is_aligned p (objBitsKO koa); fst (projectKO koa s) = {(ARM_H.SectionPDE (addrFromPPtr word) x xa xb xc xd xe, s)}; ps_clear p (objBitsKO koa) s\<rbrakk> \<Longrightarrow> vs_entry_align koa = 0 proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma mapM_x_mapM_valid:
  "\<lbrace> P \<rbrace> mapM_x f xs \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace>mapM f xs \<lbrace>\<lambda>r. Q\<rbrace>" apply (simp add: mapM_x_mapM) apply (clarsimp simp:valid_def return_def bind_def) apply (drule spec) apply (erule impE) apply simp apply (drule(1) bspec) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> mapM_x f xs \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do x <- mapM f xs;
return ()
od \<lbrace>\<lambda>r. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> mapM f xs \<lbrace>\<lambda>r. Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>\<forall>s. P s \<longrightarrow> (\<forall>y\<in>fst (mapM f xs s). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((), s)}, False)). case x of (r, x) \<Rightarrow> Q x); P s; (a, b) \<in> fst (mapM f xs s)\<rbrakk> \<Longrightarrow> Q b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (mapM f xs s); P (?s18 s a b) \<longrightarrow> (\<forall>y\<in>fst (mapM f xs (?s18 s a b)). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((), s)}, False)). case x of (r, x) \<Rightarrow> Q x)\<rbrakk> \<Longrightarrow> Q b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (mapM f xs s)\<rbrakk> \<Longrightarrow> P (?s18 s a b)
 2. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (mapM f xs s); \<forall>y\<in>fst (mapM f xs (?s18 s a b)). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((), s)}, False)). case x of (r, x) \<Rightarrow> Q x\<rbrakk> \<Longrightarrow> Q b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (mapM f xs s); \<forall>y\<in>fst (mapM f xs s). \<forall>x\<in>fst (case y of (x, s) \<Rightarrow> ({((), s)}, False)). case x of (r, x) \<Rightarrow> Q x\<rbrakk> \<Longrightarrow> Q b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>P s; (a, b) \<in> fst (mapM f xs s); \<forall>x\<in>fst (case (a, b) of (x, s) \<Rightarrow> ({((), s)}, False)). case x of (r, x) \<Rightarrow> Q x\<rbrakk> \<Longrightarrow> Q b proof (prove)
goal:
No subgoals!
theory PageTableDuplicates

lemma valid_duplicates_finalise_prop_stuff:
  "no_cte_prop (vs_valid_duplicates' \<circ> ksPSpace) = vs_valid_duplicates' \<circ> ksPSpace"
  "finalise_prop_stuff (vs_valid_duplicates' \<circ> ksPSpace)" by (simp_all add: no_cte_prop_def finalise_prop_stuff_def
                    setCTE_valid_duplicates' o_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_cte_prop (vs_valid_duplicates' \<circ> ksPSpace) = vs_valid_duplicates' \<circ> ksPSpace &&& finalise_prop_stuff (vs_valid_duplicates' \<circ> ksPSpace)