kings-crown/FVELER_Isabelle huggingface dataset:
theory Detype_R

lemma placeNewObject_valid_arch_state:
  "\<lbrace>valid_arch_state' and
    pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and
    pspace_aligned' and pspace_distinct' and
    K (is_aligned ptr (objBitsKO (injectKOS val) + us)) and
    K ( (objBitsKO (injectKOS val)+ us)< word_bits)\<rbrace>
   placeNewObject ptr val us
   \<lbrace>\<lambda>rv s. valid_arch_state' s\<rbrace>" apply (simp add:placeNewObject_def2 split_def) apply (rule createObjects'_wp_subst) apply (wp createObjects_valid_arch) apply clarsimp apply (intro conjI,simp) apply (erule(1) range_cover_full) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and pspace_distinct' and K (is_aligned ptr (objBitsKO (injectKOS val) + us)) and K (objBitsKO (injectKOS val) + us < word_bits)\<rbrace> placeNewObject ptr val us \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and pspace_distinct' and (\<lambda>y. is_aligned ptr (objBitsKO (injectKOS val) + us)) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits)\<rbrace> createObjects' ptr (Suc 0) (injectKOS val) us \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and pspace_distinct' and (\<lambda>y. is_aligned ptr (objBitsKO (injectKOS val) + us)) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits)\<rbrace> createObjects ptr (Suc 0) (injectKOS val) us \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_arch_state' and pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) and pspace_aligned' and pspace_distinct' and (\<lambda>y. is_aligned ptr (objBitsKO (injectKOS val) + us)) and (\<lambda>y. objBitsKO (injectKOS val) + us < word_bits)) s \<Longrightarrow> valid_arch_state' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr ?sz4 s \<and> range_cover ptr ?sz4 (objBitsKO (injectKOS val) + us) (Suc 0) \<and> Suc 0 \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_arch_state' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits\<rbrakk> \<Longrightarrow> pspace_no_overlap' ptr ?sz4 s \<and> range_cover ptr ?sz4 (objBitsKO (injectKOS val) + us) (Suc 0) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_arch_state' s; pspace_no_overlap' ptr (objBitsKO (injectKOS val) + us) s; pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO (injectKOS val) + us); objBitsKO (injectKOS val) + us < word_bits\<rbrakk> \<Longrightarrow> range_cover ptr (objBitsKO (injectKOS val) + us) (objBitsKO (injectKOS val) + us) (Suc 0) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma setCTE_modify_gsCNode_commute:
  "monad_commute P (setCTE src (cte::cte))
                   (modify (%ks. ks\<lparr>gsCNodes := f (gsCNodes ks)\<rparr>))" by (auto simp: monad_commute_def setCTE_def setObject_def split_def bind_def
                 return_def simpler_modify_def simpler_gets_def assert_opt_def
                 fail_def simpler_updateObject_def
           split: option.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute P (setCTE src cte) (modify (\<lambda>ks. ks\<lparr>gsCNodes := f (gsCNodes ks)\<rparr>))
theory Detype_R

lemma setCTE_modify_gsUserPages_commute:
  "monad_commute P (setCTE src (cte::cte))
                   (modify (%ks. ks\<lparr>gsUserPages := f (gsUserPages ks)\<rparr>))" by (auto simp: monad_commute_def setCTE_def setObject_def split_def bind_def
                 return_def simpler_modify_def simpler_gets_def assert_opt_def
                 fail_def simpler_updateObject_def
           split: option.splits if_split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute P (setCTE src cte) (modify (\<lambda>ks. ks\<lparr>gsUserPages := f (gsUserPages ks)\<rparr>))
theory Detype_R

lemma placeNewObject_tcb_at':
  notes [simp del] = atLeastatMost_subset_iff atLeastLessThan_iff
                     Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex atLeastAtMost_iff
  shows "\<lbrace> pspace_aligned' and pspace_distinct'
             and pspace_no_overlap' ptr (objBits (makeObject::tcb))
             and  K(is_aligned ptr  (objBits (makeObject::tcb))) \<rbrace>
         placeNewObject ptr (makeObject::tcb) 0
         \<lbrace>\<lambda>_ s. tcb_at' ptr s \<rbrace>" apply (simp add: placeNewObject_def placeNewObject'_def split_def) apply (wp unless_wp |wpc | simp add:alignError_def)+ by (auto simp: obj_at'_def is_aligned_mask lookupAround2_None1
                    lookupAround2_char1 field_simps objBits_simps
                    projectKO_opt_tcb projectKO_def return_def ps_clear_def
           split: if_splits
           dest!: pspace_no_overlap_disjoint')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBits makeObject) and K (is_aligned ptr (objBits makeObject))\<rbrace> placeNewObject ptr makeObject 0 \<lbrace>\<lambda>_. tcb_at' ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBits makeObject) and (\<lambda>y. is_aligned ptr (objBits makeObject))\<rbrace> do y <- unless (ptr && mask (objBitsKO (KOTCB makeObject)) = 0) (alignError (objBitsKO (KOTCB makeObject)));
ps <- gets ksPSpace;
y <- case fst (lookupAround2 (ptr + (2 ^ objBitsKO (KOTCB makeObject) - 1)) ps) of None \<Rightarrow> return () | Some a \<Rightarrow> assert (fst a < ptr);
modify (ksPSpace_update (\<lambda>_. ps(ptr \<mapsto> KOTCB makeObject)))
od \<lbrace>\<lambda>_. tcb_at' ptr\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (objBits makeObject) s \<and> is_aligned ptr (objBits makeObject) \<Longrightarrow> (ptr && mask (objBitsKO (KOTCB makeObject)) = 0 \<longrightarrow> (fst (lookupAround2 (ptr + (2 ^ objBitsKO (KOTCB makeObject) - 1)) (ksPSpace s)) = None \<longrightarrow> tcb_at' ptr (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some (KOTCB makeObject) else ksPSpace s a\<rparr>)) \<and> (\<forall>a. (\<exists>b. fst (lookupAround2 (ptr + (2 ^ objBitsKO (KOTCB makeObject) - 1)) (ksPSpace s)) = Some (a, b)) \<longrightarrow> a < ptr \<longrightarrow> tcb_at' ptr (s\<lparr>ksPSpace := \<lambda>a. if a = ptr then Some (KOTCB makeObject) else ksPSpace s a\<rparr>))) \<and> (ptr && mask (objBitsKO (KOTCB makeObject)) \<noteq> 0 \<longrightarrow> ?Q31 s)
theory Detype_R

lemma monad_commute_if_weak_r:
"\<lbrakk>monad_commute P1 f h1; monad_commute P2 f h2\<rbrakk> \<Longrightarrow>
  monad_commute (P1 and P2) f (if d then h1 else h2)" apply (clarsimp) apply (intro conjI impI) apply (erule monad_commute_guard_imp,simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monad_commute P1 f h1; monad_commute P2 f h2\<rbrakk> \<Longrightarrow> monad_commute (P1 and P2) f (if d then h1 else h2) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monad_commute P1 f h1; monad_commute P2 f h2\<rbrakk> \<Longrightarrow> (d \<longrightarrow> monad_commute (P1 and P2) f h1) \<and> (\<not> d \<longrightarrow> monad_commute (P1 and P2) f h2) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>monad_commute P1 f h1; monad_commute P2 f h2; d\<rbrakk> \<Longrightarrow> monad_commute (P1 and P2) f h1
 2. \<lbrakk>monad_commute P1 f h1; monad_commute P2 f h2; \<not> d\<rbrakk> \<Longrightarrow> monad_commute (P1 and P2) f h2 proof (prove)
goal:
No subgoals!
theory Detype_R

lemma updateMDB_pspace_no_overlap':
  "\<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace>
   updateMDB slot f
   \<lbrace>\<lambda>rv s. pspace_no_overlap' ptr sz s\<rbrace>" apply (rule hoare_pre) apply (clarsimp simp: updateMDB_def split del: if_split) apply (wp setCTE_pspace_no_overlap') apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace> updateMDB slot f \<lbrace>\<lambda>rv. pspace_no_overlap' ptr sz\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> updateMDB slot f \<lbrace>\<lambda>rv. pspace_no_overlap' ptr sz\<rbrace>
 2. \<And>s. (pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if slot = 0 then return () else do cte <- getCTE slot;
mdb <- return (cteMDBNode cte);
mdb' <- return (f mdb);
return (cteMDBNode_update (\<lambda>_. mdb') cte) >>= setCTE slot
od \<lbrace>\<lambda>rv. pspace_no_overlap' ptr sz\<rbrace>
 2. \<And>s. (pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz) s \<Longrightarrow> (slot = 0 \<longrightarrow> pspace_no_overlap' ptr sz s) \<and> (slot \<noteq> 0 \<longrightarrow> (pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz) s) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma pspace_no_overlapD2':
  "\<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s;sz < word_bits;
    ctes_of s slot = Some cte\<rbrakk>
   \<Longrightarrow> slot \<noteq> ptr" apply (drule ctes_of_ko_at) apply clarsimp apply (drule(1) pspace_no_overlapD') apply (erule in_empty_interE) apply (simp add:obj_range'_def) apply clarsimp apply (subst is_aligned_neg_mask_eq[symmetric]) apply simp apply (simp add: is_aligned_neg_mask is_aligned_no_overflow) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; ctes_of s slot = Some cte\<rbrakk> \<Longrightarrow> slot \<noteq> ptr proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; \<exists>ptr ko. ksPSpace s ptr = Some ko \<and> slot \<in> obj_range' ptr ko\<rbrakk> \<Longrightarrow> slot \<noteq> ptr proof (prove)
goal (1 subgoal):
 1. \<And>ptra ko. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; ksPSpace s ptra = Some ko; ptr \<in> obj_range' ptra ko; slot = ptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>ptra ko. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; ptr \<in> obj_range' ptra ko; slot = ptr; {ptra..ptra + 2 ^ objBitsKO ko - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>ptra ko. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; ptr \<in> obj_range' ptra ko; slot = ptr\<rbrakk> \<Longrightarrow> ?x11 ptra ko \<in> {ptra..ptra + 2 ^ objBitsKO ko - 1}
 2. \<And>ptra ko. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; ptr \<in> obj_range' ptra ko; slot = ptr\<rbrakk> \<Longrightarrow> ?x11 ptra ko \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>ptra ko. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; ptr \<in> obj_range' ptra ko; slot = ptr\<rbrakk> \<Longrightarrow> ptr \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>ptra ko. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; ptr \<in> obj_range' ptra ko; slot = ptr\<rbrakk> \<Longrightarrow> ptr \<le> ptr + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>ptra ko. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; ptr \<in> obj_range' ptra ko; slot = ptr\<rbrakk> \<Longrightarrow> is_aligned ptr (?n14 ptra ko)
 2. \<And>ptra ko. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; ptr \<in> obj_range' ptra ko; slot = ptr\<rbrakk> \<Longrightarrow> ptr && ~~ mask (?n14 ptra ko) \<le> ptr + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>ptra ko. \<lbrakk>is_aligned ptr sz; pspace_no_overlap' ptr sz s; sz < word_bits; ptr \<in> obj_range' ptra ko; slot = ptr\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> ptr + 2 ^ sz - 1 proof (prove)
goal:
No subgoals!
theory Detype_R

lemma caps_overlap_reserved'_subseteq:
  "\<lbrakk>caps_overlap_reserved' B s; A\<subseteq> B\<rbrakk> \<Longrightarrow> caps_overlap_reserved' A s" apply (clarsimp simp:caps_overlap_reserved'_def) apply (drule(1) bspec) apply (erule disjoint_subset2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_overlap_reserved' B s; A \<subseteq> B\<rbrakk> \<Longrightarrow> caps_overlap_reserved' A s proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>\<forall>cte\<in>ran (ctes_of s). isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> B = {}; A \<subseteq> B; cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> A = {} proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>A \<subseteq> B; cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> B = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> A = {} proof (prove)
goal (1 subgoal):
 1. \<And>cte. \<lbrakk>cte \<in> ran (ctes_of s); isUntypedCap (cteCap cte); isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> B = {}\<rbrakk> \<Longrightarrow> usableUntypedRange (cteCap cte) \<inter> B = {} proof (prove)
goal:
No subgoals!
theory Detype_R

lemma valid_arch_state'_updateMDB:
  "\<lbrace>valid_arch_state' \<rbrace> updateMDB a b \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>" by (clarsimp simp:updateMDB_def valid_arch_state_def,wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> updateMDB a b \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>
theory Detype_R

lemma fail_commute:
  "monad_commute \<top> fail f = empty_fail f" apply (simp add: monad_commute_def empty_fail_def) apply (simp add: fail_def bind_def del: split_paired_Ex) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) fail f = empty_fail f proof (prove)
goal (1 subgoal):
 1. (\<forall>s. fail s = (do y <- f;
fail
od) s) = (\<forall>s. fst (f s) = {} \<longrightarrow> snd (f s)) proof (prove)
goal (1 subgoal):
 1. (\<forall>s. (\<exists>x. x \<in> fst (f s)) \<or> snd (f s)) = (\<forall>s. fst (f s) = {} \<longrightarrow> snd (f s)) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma modify_commute:
  "monad_commute P (modify f) (modify g)
    = (\<forall>s. P s \<longrightarrow> f (g s) = g (f s))" apply (simp add: monad_commute_def exec_modify) apply (simp add: return_def eq_commute) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute P (modify f) (modify g) = (\<forall>s. P s \<longrightarrow> f (g s) = g (f s)) proof (prove)
goal (1 subgoal):
 1. (\<forall>s. P s \<longrightarrow> return ((), ()) (g (f s)) = return ((), ()) (f (g s))) = (\<forall>s. P s \<longrightarrow> f (g s) = g (f s)) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma assert_commute2: "empty_fail f
    \<Longrightarrow> monad_commute \<top> (assert G) f" apply (clarsimp simp:assert_def monad_commute_def) apply (simp add: fail_def bind_def empty_fail_def del: split_paired_Ex) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. empty_fail f \<Longrightarrow> monad_commute (\<lambda>_. True) (assert G) f proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>empty_fail f; \<not> G\<rbrakk> \<Longrightarrow> fail s = (do y <- f;
fail
od) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. fst (f s) = {} \<longrightarrow> snd (f s); \<not> G\<rbrakk> \<Longrightarrow> (\<exists>x. x \<in> fst (f s)) \<or> snd (f s) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma threadSet_gsUntypedZeroRanges_commute':
  "monad_commute \<top>
     (threadSet fn ptr)
     (modify (\<lambda>s. s \<lparr> gsUntypedZeroRanges := f (gsUntypedZeroRanges s) \<rparr> ))" apply (simp add: threadSet_def getObject_def setObject_def) apply (rule commute_commute) apply (strengthen monad_commute_guard_imp[OF monad_commute_split[where P="\<top>" and Q="\<top>\<top>"], OF _ _ hoare_vcg_prop]
     | simp add: modify_commute updateObject_default_def alignCheck_assert
                 magnitudeCheck_assert return_commute return_commute[THEN commute_commute]
                 projectKO_def2 assert_commute2 assert_commute2[THEN commute_commute]
                 assert_opt_def2 loadObject_default_def
          split: option.split prod.split)+ apply (simp add: monad_commute_def exec_gets exec_modify) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (threadSet fn ptr) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (do tcb <- do map <- gets ksPSpace;
case lookupAround2 ptr map of (before, after) \<Rightarrow> do (ptr', y) <- assert_opt before;
loadObject_default ptr ptr' after y
od
od;
ps <- gets ksPSpace;
case lookupAround2 ptr ps of (before, after) \<Rightarrow> do (ptr', obj) <- assert_opt before;
obj' <- updateObject_default (fn tcb) obj ptr ptr' after;
modify (ksPSpace_update (\<lambda>_. ps(ptr' \<mapsto> obj')))
od
od) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (do tcb <- do map <- gets ksPSpace;
case lookupAround2 ptr map of (before, after) \<Rightarrow> do (ptr', y) <- assert_opt before;
loadObject_default ptr ptr' after y
od
od;
ps <- gets ksPSpace;
case lookupAround2 ptr ps of (before, after) \<Rightarrow> do (ptr', obj) <- assert_opt before;
obj' <- updateObject_default (fn tcb) obj ptr ptr' after;
modify (ksPSpace_update (\<lambda>_. ps(ptr' \<mapsto> obj')))
od
od) proof (prove)
goal (1 subgoal):
 1. monad_commute (\<lambda>_. True) (modify (\<lambda>s. s\<lparr>gsUntypedZeroRanges := f (gsUntypedZeroRanges s)\<rparr>)) (gets ksPSpace) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma doMachineOp_modify_commute:
  "\<lbrakk> \<forall>s. P s \<longrightarrow> ksMachineState (f s) = ksMachineState s;
      \<forall>s. P s \<longrightarrow> (\<forall>(rv, ms') \<in> fst (oper (ksMachineState s)).
          f (ksMachineState_update (\<lambda>_. ms') s) = ksMachineState_update (\<lambda>_. ms') (f s)) \<rbrakk>
    \<Longrightarrow> monad_commute P (doMachineOp oper) (modify (f))" apply (clarsimp simp: monad_commute_def doMachineOp_def
                        exec_gets bind_assoc exec_modify) apply (simp add: bind_def[where f="select_f v" for v],
    simp add: select_f_def split_def exec_modify cart_singleton_image) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>s. P s \<longrightarrow> ksMachineState (f s) = ksMachineState s; \<forall>s. P s \<longrightarrow> (\<forall>(rv, ms')\<in>fst (oper (ksMachineState s)). f (s\<lparr>ksMachineState := ms'\<rparr>) = f s\<lparr>ksMachineState := ms'\<rparr>)\<rbrakk> \<Longrightarrow> monad_commute P (doMachineOp oper) (modify f) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s. P s \<longrightarrow> ksMachineState (f s) = ksMachineState s; \<forall>s. P s \<longrightarrow> (\<forall>x\<in>fst (oper (ksMachineState s)). case x of (rv, ms') \<Rightarrow> f (s\<lparr>ksMachineState := ms'\<rparr>) = f s\<lparr>ksMachineState := ms'\<rparr>); P s\<rbrakk> \<Longrightarrow> (do x <- select_f (oper (ksMachineState s));
x <- case x of (r, ms') \<Rightarrow> do y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od;
y <- modify f;
return (x, ())
od) s = (do x <- select_f (oper (ksMachineState s));
x <- case x of (r, ms') \<Rightarrow> do y <- modify (ksMachineState_update (\<lambda>_. ms'));
return r
od;
return (x, ())
od) (f s) proof (prove)
goal:
No subgoals!
theory Detype_R

lemma monad_commute_If_rhs:
  "monad_commute P a b \<Longrightarrow> monad_commute Q a c
    \<Longrightarrow> monad_commute (\<lambda>s. (R \<longrightarrow> P s) \<and> (\<not> R \<longrightarrow> Q s)) a (if R then b else c)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>monad_commute P a b; monad_commute Q a c\<rbrakk> \<Longrightarrow> monad_commute (\<lambda>s. (R \<longrightarrow> P s) \<and> (\<not> R \<longrightarrow> Q s)) a (if R then b else c)
theory Detype_R

lemma case_eq_if_isUntypedCap:
  "(case c of UntypedCap _ _ _ _ \<Rightarrow> x | _ \<Rightarrow> y)
    = (if isUntypedCap c then x else y)" by (cases c, simp_all add: isCap_simps)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (case c of capability.UntypedCap xa xb xc xd \<Rightarrow> x | _ \<Rightarrow> y) = (if isUntypedCap c then x else y)
theory Detype_R

lemma updateNewFreeIndex_cte_wp_at[wp]:
  "\<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> updateNewFreeIndex slot \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>" by (simp add: cte_wp_at_ctes_of, wp)

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

lemma doMachineOp_psp_no_overlap:
  "\<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s \<rbrace>
   doMachineOp f
   \<lbrace>\<lambda>y s. pspace_no_overlap' ptr sz s\<rbrace>" by (wp pspace_no_overlap'_lift,simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. pspace_no_overlap' ptr sz s \<and> pspace_aligned' s \<and> pspace_distinct' s\<rbrace> doMachineOp f \<lbrace>\<lambda>y. pspace_no_overlap' ptr sz\<rbrace>
theory Detype_R

lemma copyGlobalMappings_pspace_no_overlap':
  "\<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace>
   copyGlobalMappings xa
   \<lbrace>\<lambda>ya. pspace_no_overlap' ptr sz\<rbrace>" apply (rule hoare_pre) apply (clarsimp simp:copyGlobalMappings_def) apply (wp mapM_x_wp_inv pspace_no_overlap'_lift) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz\<rbrace> copyGlobalMappings xa \<lbrace>\<lambda>ya. pspace_no_overlap' ptr sz\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> copyGlobalMappings xa \<lbrace>\<lambda>ya. pspace_no_overlap' ptr sz\<rbrace>
 2. \<And>s. (pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do globalPD <- gets (armKSGlobalPD \<circ> ksArchState);
mapM_x (\<lambda>index. getObject (globalPD + (index << pdeBits)) >>= storePDE (xa + (index << pdeBits))) [pptrBase >> 20 .e. 2 ^ (pdBits - pdeBits) - 1]
od \<lbrace>\<lambda>ya. pspace_no_overlap' ptr sz\<rbrace>
 2. \<And>s. (pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr sz) s \<Longrightarrow> ((\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s) and pspace_no_overlap' ptr sz) s proof (prove)
goal:
No subgoals!