kings-crown/FVELER_Isabelle huggingface dataset:
theory Detype_R

lemma pspace_no_overlap'_tail:
  "\<lbrakk>range_cover ptr sz us (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s;
    pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk>
   \<Longrightarrow> pspace_no_overlap' (ptr + (1 + of_nat n << us)) sz s" apply (erule pspace_no_overlap'_le2) apply (erule(1) range_cover_ptr_le) apply (erule(1) range_cover_tail_mask) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_no_overlap' (ptr + (1 + word_of_nat n << us)) sz s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr \<le> ptr + (1 + word_of_nat n << us)
 2. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>range_cover ptr sz us (Suc (Suc n)); pspace_aligned' s; pspace_distinct' s; ptr \<noteq> 0\<rbrakk> \<Longrightarrow> ptr + (1 + word_of_nat n << us) && ~~ mask sz = ptr && ~~ mask sz proof (prove)
goal:
No subgoals!
theory Detype_R

lemma objSize_eq_capBits:
  "Types_H.getObjectSize ty us = APIType_capBits ty us" apply (case_tac ty) apply (clarsimp simp:ARM_H.getObjectSize_def objBits_simps
    APIType_capBits_def apiGetObjectSize_def ptBits_def
    tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def cteSizeBits_def
    pageBits_def pdBits_def pteBits_def pdeBits_def
    split : apiobject_type.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. getObjectSize ty us = APIType_capBits ty us proof (prove)
goal (7 subgoals):
 1. \<And>x1. ty = APIObjectType x1 \<Longrightarrow> getObjectSize ty us = APIType_capBits ty us
 2. ty = SmallPageObject \<Longrightarrow> getObjectSize ty us = APIType_capBits ty us
 3. ty = LargePageObject \<Longrightarrow> getObjectSize ty us = APIType_capBits ty us
 4. ty = SectionObject \<Longrightarrow> getObjectSize ty us = APIType_capBits ty us
 5. ty = SuperSectionObject \<Longrightarrow> getObjectSize ty us = APIType_capBits ty us
 6. ty = PageTableObject \<Longrightarrow> getObjectSize ty us = APIType_capBits ty us
 7. ty = PageDirectoryObject \<Longrightarrow> getObjectSize ty us = APIType_capBits ty us proof (prove)
goal:
No subgoals!
theory Detype_R

lemma modify_comp:
  "modify (ksPSpace_update (\<lambda>a. f (g a))) =
  (do modify (ksPSpace_update (\<lambda>a. (g a)));
      modify (ksPSpace_update (\<lambda>a. f a))
   od)" by (clarsimp simp:simpler_modify_def bind_def Fun.comp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. modify (ksPSpace_update (\<lambda>a. f (g a))) = do modify (ksPSpace_update g);
modify (ksPSpace_update f)
od
theory Detype_R

lemma gsCNodes_upd_createObjects'_comm:
  "do _ \<leftarrow> modify (gsCNodes_update f);
      x \<leftarrow> createObjects' ptr n obj us;
      m x
   od =
   do x \<leftarrow> createObjects' ptr n obj us;
      _ \<leftarrow> modify (gsCNodes_update f);
      m x
   od" apply (rule ext) apply (case_tac x) by (auto simp: createObjects'_def split_def bind_assoc return_def unless_def
          when_def simpler_gets_def alignError_def fail_def assert_def
          simpler_modify_def bind_def
        split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- modify (gsCNodes_update f);
createObjects' ptr n obj us >>= m
od = do x <- createObjects' ptr n obj us;
_ <- modify (gsCNodes_update f);
m x
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do _ <- modify (gsCNodes_update f);
createObjects' ptr n obj us >>= m
od) x = (do x <- createObjects' ptr n obj us;
_ <- modify (gsCNodes_update f);
m x
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. x = \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr> \<Longrightarrow> (do _ <- modify (gsCNodes_update f);
createObjects' ptr n obj us >>= m
od) x = (do x <- createObjects' ptr n obj us;
_ <- modify (gsCNodes_update f);
m x
od) x
theory Detype_R

lemma gsUserPages_upd_createObjects'_comm:
  "do _ \<leftarrow> modify (gsUserPages_update f);
      x \<leftarrow> createObjects' ptr n obj us;
      m x
   od =
   do x \<leftarrow> createObjects' ptr n obj us;
      _ \<leftarrow> modify (gsUserPages_update f);
      m x
   od" apply (rule ext) apply (case_tac x) by (auto simp: createObjects'_def split_def bind_assoc return_def unless_def
          when_def simpler_gets_def alignError_def fail_def assert_def
          simpler_modify_def bind_def
        split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do _ <- modify (gsUserPages_update f);
createObjects' ptr n obj us >>= m
od = do x <- createObjects' ptr n obj us;
_ <- modify (gsUserPages_update f);
m x
od proof (prove)
goal (1 subgoal):
 1. \<And>x. (do _ <- modify (gsUserPages_update f);
createObjects' ptr n obj us >>= m
od) x = (do x <- createObjects' ptr n obj us;
_ <- modify (gsUserPages_update f);
m x
od) x proof (prove)
goal (1 subgoal):
 1. \<And>x ksPSpace gsUserPages gsCNodes gsUntypedZeroRanges gsMaxObjectSize ksDomScheduleIdx ksDomSchedule ksCurDomain ksDomainTime ksReadyQueues ksReadyQueuesL1Bitmap ksReadyQueuesL2Bitmap ksCurThread ksIdleThread ksSchedulerAction ksInterruptState ksWorkUnitsCompleted ksArchState ksMachineState. x = \<lparr>ksPSpace = ksPSpace, gsUserPages = gsUserPages, gsCNodes = gsCNodes, gsUntypedZeroRanges = gsUntypedZeroRanges, gsMaxObjectSize = gsMaxObjectSize, ksDomScheduleIdx = ksDomScheduleIdx, ksDomSchedule = ksDomSchedule, ksCurDomain = ksCurDomain, ksDomainTime = ksDomainTime, ksReadyQueues = ksReadyQueues, ksReadyQueuesL1Bitmap = ksReadyQueuesL1Bitmap, ksReadyQueuesL2Bitmap = ksReadyQueuesL2Bitmap, ksCurThread = ksCurThread, ksIdleThread = ksIdleThread, ksSchedulerAction = ksSchedulerAction, ksInterruptState = ksInterruptState, ksWorkUnitsCompleted = ksWorkUnitsCompleted, ksArchState = ksArchState, ksMachineState = ksMachineState\<rparr> \<Longrightarrow> (do _ <- modify (gsUserPages_update f);
createObjects' ptr n obj us >>= m
od) x = (do x <- createObjects' ptr n obj us;
_ <- modify (gsUserPages_update f);
m x
od) x
theory Detype_R

lemma ef_dmo':
  "empty_fail f \<Longrightarrow> empty_fail (doMachineOp f)" by (auto simp: empty_fail_def doMachineOp_def split_def select_f_def
           simpler_modify_def simpler_gets_def return_def bind_def image_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> empty_fail (doMachineOp f)
theory Detype_R

lemma rewrite_step:
  assumes rewrite: "\<And>s. P s \<Longrightarrow> f s = f' s"
  shows "P s \<Longrightarrow> ( f >>= g ) s = (f' >>= g ) s" by (simp add:bind_def rewrite)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. P s \<Longrightarrow> (f >>= g) s = (f' >>= g) s
theory Detype_R

lemma rewrite_through_step:
  assumes rewrite: "\<And>s r. P s \<Longrightarrow> f r s = f' r s"
  assumes hoare: "\<lbrace>Q\<rbrace> g \<lbrace>\<lambda>r. P\<rbrace>"
  shows "Q s \<Longrightarrow>
    (do x \<leftarrow> g;
       y \<leftarrow> f x;
       h x y od) s =
    (do x \<leftarrow> g;
       y \<leftarrow> f' x;
       h x y od) s" apply (rule monad_eq_split[where Q = "\<lambda>r. P"]) apply (simp add:bind_def rewrite) apply (rule hoare) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Q s \<Longrightarrow> (do x <- g;
f x >>= h x
od) s = (do x <- g;
f' x >>= h x
od) s proof (prove)
goal (3 subgoals):
 1. \<And>r sa. \<lbrakk>Q s; P sa\<rbrakk> \<Longrightarrow> (f r >>= h r) sa = (f' r >>= h r) sa
 2. Q s \<Longrightarrow> \<lbrace>?P\<rbrace> g \<lbrace>\<lambda>r. P\<rbrace>
 3. Q s \<Longrightarrow> ?P s proof (prove)
goal (2 subgoals):
 1. Q s \<Longrightarrow> \<lbrace>?P\<rbrace> g \<lbrace>\<lambda>r. P\<rbrace>
 2. Q s \<Longrightarrow> ?P s proof (prove)
goal (1 subgoal):
 1. Q s \<Longrightarrow> Q s proof (prove)
goal:
No subgoals!
theory Detype_R

lemma new_cap_addrs_def2:
  "n < 2 ^ 32
   \<Longrightarrow> new_cap_addrs (Suc n) ptr obj
   = map (\<lambda>n. ptr + (n << objBitsKO obj)) [0.e.of_nat n]" by (simp add:new_cap_addrs_def upto_enum_word unat_of_nat Fun.comp_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. n < 2 ^ 32 \<Longrightarrow> new_cap_addrs (Suc n) ptr obj = map (\<lambda>n. ptr + (n << objBitsKO obj)) [0 .e. word_of_nat n]
theory Detype_R

lemma createObject_def3:
  "createObject =
   (\<lambda>ty ptr us d. createNewCaps ty ptr (Suc 0) us d >>= (\<lambda>m. return (hd m)))" apply (rule ext)+ apply (simp add:createObject_def2[symmetric]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. global.createObject = (\<lambda>ty ptr us d. do m <- createNewCaps ty ptr (Suc 0) us d;
return (hd m)
od) proof (prove)
goal (1 subgoal):
 1. \<And>ty ptr us d x. global.createObject ty ptr us d x = (do m <- createNewCaps ty ptr (Suc 0) us d;
return (hd m)
od) x proof (prove)
goal:
No subgoals!
theory Detype_R

lemma to_from_apiTypeD: "toAPIType ty = Some x \<Longrightarrow> ty = fromAPIType x" by (cases ty) (auto simp add: fromAPIType_def
    toAPIType_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. toAPIType ty = Some x \<Longrightarrow> ty = fromAPIType x
theory Detype_R

lemma updateNewFreeIndex_cteCaps_of[wp]:
  "\<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> updateNewFreeIndex slot \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" by (simp add: cteCaps_of_def, wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> updateNewFreeIndex slot \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>
theory Detype_R

lemma insertNewCap_wps[wp]:
  "\<lbrace>pspace_aligned'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>"
  "\<lbrace>pspace_distinct'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>"
  "\<lbrace>\<lambda>s. P ((cteCaps_of s)(slot \<mapsto> cap))\<rbrace>
      insertNewCap parent slot cap
   \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" apply (simp_all add: insertNewCap_def) apply (wp hoare_drop_imps
            | simp add: o_def)+ apply (fastforce elim!: rsubst[where P=P]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace> &&& \<lbrace>pspace_distinct'\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace> &&& \<lbrace>\<lambda>s. P ((cteCaps_of s)(slot \<mapsto> cap))\<rbrace> insertNewCap parent slot cap \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>pspace_aligned'\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv. pspace_aligned'\<rbrace>
 2. \<lbrace>pspace_distinct'\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv. pspace_distinct'\<rbrace>
 3. \<lbrace>\<lambda>s. P ((cteCaps_of s)(slot \<mapsto> cap))\<rbrace> do next <- liftM (mdbNext \<circ> cteMDBNode) (getCTE parent);
oldCTE <- getCTE slot;
y <- assert (cteCap oldCTE = capability.NullCap \<and> mdbNext (cteMDBNode oldCTE) = nullPointer \<and> mdbPrev (cteMDBNode oldCTE) = nullPointer);
y <- setCTE slot (CTE cap (MDB next parent True True));
y <- updateMDB next (mdbPrev_update (\<lambda>_. slot));
y <- updateMDB parent (mdbNext_update (\<lambda>_. slot));
updateNewFreeIndex slot
od \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P ((cteCaps_of s)(slot \<mapsto> cap)) \<Longrightarrow> P (\<lambda>a. if a = slot then Some cap else cteCaps_of s a) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma valid_untyped_inv_wcap':
  "valid_untyped_inv' ui
    = (\<lambda>s. \<exists>sz idx. valid_untyped_inv_wcap' ui
        (Some (case ui of Invocations_H.Retype slot reset ptr_base ptr ty us slots d
            \<Rightarrow> UntypedCap d (ptr && ~~ mask sz) sz idx)) s)" by (cases ui, auto simp: fun_eq_iff cte_wp_at_ctes_of)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. valid_untyped_inv' ui = (\<lambda>s. \<exists>sz idx. valid_untyped_inv_wcap' ui (Some (case ui of Invocations_H.untyped_invocation.Retype slot reset ptr_base ptr ty us slots d \<Rightarrow> capability.UntypedCap d (ptr && ~~ mask sz) sz idx)) s)
theory Untyped_R

lemma whenE_rangeCheck_eq:
  "(rangeCheck (x :: 'a :: {linorder, integral}) y z) =
    (whenE (x < fromIntegral y \<or> fromIntegral z < x)
      (throwError (RangeError (fromIntegral y) (fromIntegral z))))" by (simp add: rangeCheck_def unlessE_whenE linorder_not_le[symmetric])

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. rangeCheck x y z = whenE (x < fromIntegral y \<or> fromIntegral z < x) (throwError (Fault_H.syscall_error.RangeError (fromIntegral y) (fromIntegral z)))
theory Untyped_R

lemma APIType_map2_CapTable[simp]:
  "(APIType_map2 ty = Structures_A.CapTableObject)
    = (ty = Inr (APIObjectType ArchTypes_H.CapTableObject))" by (simp add: APIType_map2_def
         split: sum.split ARM_H.object_type.split
                apiobject_type.split
                kernel_object.split arch_kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (APIType_map2 ty = Structures_A.apiobject_type.CapTableObject) = (ty = Inr (APIObjectType ArchTypes_H.apiobject_type.CapTableObject))
theory Untyped_R

lemma alignUp_H[simp]:
  "Untyped_H.alignUp = More_Word_Operations.alignUp" apply (rule ext)+ apply (clarsimp simp:Untyped_H.alignUp_def More_Word_Operations.alignUp_def mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. Untyped_H.alignUp = More_Word_Operations.alignUp proof (prove)
goal (1 subgoal):
 1. \<And>x xa. Untyped_H.alignUp x xa = More_Word_Operations.alignUp x xa proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma mapM_x_stateAssert:
  "mapM_x (\<lambda>x. stateAssert (f x) (ss x)) xs
    = stateAssert (\<lambda>s. \<forall>x \<in> set xs. f x s) []" apply (induct xs) apply (simp add: mapM_x_Nil) apply (simp add: mapM_x_Cons) apply (simp add: fun_eq_iff stateAssert_def bind_assoc exec_get assert_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mapM_x (\<lambda>x. stateAssert (f x) (ss x)) xs = stateAssert (\<lambda>s. \<forall>x\<in>set xs. f x s) [] proof (prove)
goal (2 subgoals):
 1. mapM_x (\<lambda>x. stateAssert (f x) (ss x)) [] = stateAssert (\<lambda>s. \<forall>x\<in>set []. f x s) []
 2. \<And>a xs. mapM_x (\<lambda>x. stateAssert (f x) (ss x)) xs = stateAssert (\<lambda>s. \<forall>x\<in>set xs. f x s) [] \<Longrightarrow> mapM_x (\<lambda>x. stateAssert (f x) (ss x)) (a # xs) = stateAssert (\<lambda>s. \<forall>x\<in>set (a # xs). f x s) [] proof (prove)
goal (1 subgoal):
 1. \<And>a xs. mapM_x (\<lambda>x. stateAssert (f x) (ss x)) xs = stateAssert (\<lambda>s. \<forall>x\<in>set xs. f x s) [] \<Longrightarrow> mapM_x (\<lambda>x. stateAssert (f x) (ss x)) (a # xs) = stateAssert (\<lambda>s. \<forall>x\<in>set (a # xs). f x s) [] proof (prove)
goal (1 subgoal):
 1. \<And>a xs. mapM_x (\<lambda>x. stateAssert (f x) (ss x)) xs = stateAssert (\<lambda>s. \<forall>x\<in>set xs. f x s) [] \<Longrightarrow> do y <- stateAssert (f a) (ss a);
stateAssert (\<lambda>s. \<forall>x\<in>set xs. f x s) []
od = stateAssert (\<lambda>s. f a s \<and> (\<forall>x\<in>set xs. f x s)) [] proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma mapM_locate_eq:
    "isCNodeCap cap
    \<Longrightarrow> mapM (\<lambda>x. locateSlotCap cap x) xs
        = (do stateAssert (\<lambda>s. case gsCNodes s (capUntypedPtr cap) of None \<Rightarrow> xs = [] | Some n
                \<Rightarrow> \<forall>x \<in> set xs. n = capCNodeBits cap \<and> x < 2 ^ n) [];
            return (map (\<lambda>x. (capCNodePtr cap) + 2 ^ cte_level_bits * x) xs) od)" apply (clarsimp simp: isCap_simps) apply (simp add: locateSlot_conv objBits_simps cte_level_bits_def
                   liftM_def[symmetric] mapM_liftM_const isCap_simps) apply (simp add: liftM_def mapM_discarded mapM_x_stateAssert) apply (intro bind_cong refl arg_cong2[where f=stateAssert] ext) apply (simp add: isCap_simps split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isCNodeCap cap \<Longrightarrow> mapM (locateSlotCap cap) xs = do stateAssert (\<lambda>s. case gsCNodes s (global.capUntypedPtr cap) of None \<Rightarrow> xs = [] | Some n \<Rightarrow> \<forall>x\<in>set xs. n = capCNodeBits cap \<and> x < 2 ^ n) [];
return (map (\<lambda>x. capCNodePtr cap + 2 ^ cte_level_bits * x) xs)
od proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 v3. cap = capability.CNodeCap v0 v1 v2 v3 \<Longrightarrow> mapM (locateSlotCap (capability.CNodeCap v0 v1 v2 v3)) xs = do y <- stateAssert (\<lambda>s. case gsCNodes s v0 of None \<Rightarrow> xs = [] | Some n \<Rightarrow> \<forall>x\<in>set xs. n = v1 \<and> x < 2 ^ n) [];
return (map (\<lambda>x. v0 + 2 ^ cte_level_bits * x) xs)
od proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 v3. cap = capability.CNodeCap v0 v1 v2 v3 \<Longrightarrow> liftM (\<lambda>ys. map (\<lambda>x. v0 + 0x10 * x) xs) (mapM (\<lambda>x. stateAssert (\<lambda>s. case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> x < 2 ^ n) []) xs) = liftM (\<lambda>y. map (\<lambda>x. v0 + 0x10 * x) xs) (stateAssert (\<lambda>s. case gsCNodes s v0 of None \<Rightarrow> xs = [] | Some n \<Rightarrow> \<forall>x\<in>set xs. n = v1 \<and> x < 2 ^ n) []) proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 v3. cap = capability.CNodeCap v0 v1 v2 v3 \<Longrightarrow> do _ <- stateAssert (\<lambda>s. \<forall>x\<in>set xs. case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> x < 2 ^ n) [];
return (map (\<lambda>x. v0 + 0x10 * x) xs)
od = do x <- stateAssert (\<lambda>s. case gsCNodes s v0 of None \<Rightarrow> xs = [] | Some n \<Rightarrow> \<forall>x\<in>set xs. n = v1 \<and> x < 2 ^ n) [];
return (map (\<lambda>x. v0 + 0x10 * x) xs)
od proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 v3 s. cap = capability.CNodeCap v0 v1 v2 v3 \<Longrightarrow> (\<forall>x\<in>set xs. case gsCNodes s v0 of None \<Rightarrow> False | Some n \<Rightarrow> n = v1 \<and> x < 2 ^ n) = (case gsCNodes s v0 of None \<Rightarrow> xs = [] | Some n \<Rightarrow> \<forall>x\<in>set xs. n = v1 \<and> x < 2 ^ n) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma is_frame_type_isFrameType_eq[simp]:
  "(is_frame_type (APIType_map2 (Inr (toEnum (unat arg0))))) =
   (Types_H.isFrameType (toEnum (unat arg0)))" by (simp add: APIType_map2_def is_frame_type_defs split: apiobject_type.splits object_type.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_frame_type (APIType_map2 (Inr (toEnum (unat arg0)))) = isFrameType (toEnum (unat arg0))
theory Untyped_R

lemma corres_whenE_throw_merge:
  "corres r P P' f (doE _ \<leftarrow> whenE (A \<or> B) (throwError e); h odE)
  \<Longrightarrow> corres r P P' f (doE _ \<leftarrow> whenE A (throwError e); _ \<leftarrow>  whenE B (throwError e); h odE)" by (auto simp: whenE_def split: if_splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres r P P' f (doE _ <- whenE (A \<or> B) (throwError e);
h
odE) \<Longrightarrow> corres r P P' f (doE _ <- whenE A (throwError e);
_ <- whenE B (throwError e);
h
odE)
theory Untyped_R

lemma descendants_of_cte_at':
  "\<lbrakk>p \<in> descendants_of' x (ctes_of s); valid_mdb' s\<rbrakk>
   \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s" by (clarsimp simp:descendants_of'_def cte_wp_at_ctes_of
    dest!:subtree_target_Some)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>p \<in> descendants_of' x (ctes_of s); valid_mdb' s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s
theory Untyped_R

lemma checkFreeIndex_wp:
  "\<lbrace>\<lambda>s. if descendants_of' slot (ctes_of s) = {} then Q y s else Q x s\<rbrace>
   constOnFailure x (doE z \<leftarrow> ensureNoChildren slot; returnOk y odE)
   \<lbrace>Q\<rbrace>" apply (clarsimp simp:constOnFailure_def const_def) apply (wp ensureNoChildren_wp) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if descendants_of' slot (ctes_of s) = {} then Q y s else Q x s\<rbrace> constOnFailure x (doE z <- ensureNoChildren slot;
returnOk y
odE) \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (descendants_of' slot (ctes_of s) = {} \<longrightarrow> Q y s) \<and> (descendants_of' slot (ctes_of s) \<noteq> {} \<longrightarrow> Q x s)\<rbrace> doE z <- ensureNoChildren slot;
returnOk y
odE <catch> (\<lambda>y. return x) \<lbrace>Q\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (descendants_of' slot (ctes_of s) = {} \<longrightarrow> Q y s) \<and> (descendants_of' slot (ctes_of s) \<noteq> {} \<longrightarrow> Q x s) \<Longrightarrow> (descendants_of' slot (ctes_of s) \<noteq> {} \<longrightarrow> Q x s) \<and> (descendants_of' slot (ctes_of s) = {} \<longrightarrow> Q y s) proof (prove)
goal:
No subgoals!
theory Untyped_R

lemma ensureNoChildren_sp:
  "\<lbrace>P\<rbrace> ensureNoChildren sl \<lbrace>\<lambda>rv s. P s \<and> descendants_of' sl (ctes_of s) = {}\<rbrace>,-" by (wp ensureNoChildren_wp, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> ensureNoChildren sl \<lbrace>\<lambda>rv s. P s \<and> descendants_of' sl (ctes_of s) = {}\<rbrace>, -
theory Untyped_R

lemma irq_nodes_global:
  "irq_node' s + (ucast (irq :: 10 word)) * 16 \<in> global_refs' s" by (simp add: global_refs'_def mult.commute mult.left_commute cteSizeBits_def shiftl_t2n)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. irq_node' s + UCAST(10 \<rightarrow> 32) irq * 0x10 \<in> global_refs' s
theory Untyped_R

lemma valid_global_refsD2':
  "\<lbrakk>ctes_of s p = Some cte; valid_global_refs' s\<rbrakk> \<Longrightarrow>
  global_refs' s \<inter> capRange (cteCap cte) = {}" by (blast dest: valid_global_refsD')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; valid_global_refs' s\<rbrakk> \<Longrightarrow> global_refs' s \<inter> capRange (cteCap cte) = {}