kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_R

lemma arch_deriveCap_untyped_derived[wp]:
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. untyped_derived_eq c' (cteCap cte)) slot s\<rbrace>
     ARM_H.deriveCap slot (capCap c')
   \<lbrace>\<lambda>rv s. cte_wp_at' (untyped_derived_eq rv o cteCap) slot s\<rbrace>, -" apply (wpsimp simp: ARM_H.deriveCap_def Let_def untyped_derived_eq_ArchObjectCap split_del: if_split
                  wp: undefined_validE_R) apply(clarsimp simp: cte_wp_at_ctes_of isCap_simps untyped_derived_eq_def) by (case_tac "capCap c'"; fastforce)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. untyped_derived_eq c' (cteCap cte)) slot\<rbrace> Arch.deriveCap slot (capCap c') \<lbrace>\<lambda>rv. cte_wp_at' (untyped_derived_eq rv \<circ> cteCap) slot\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>cte. untyped_derived_eq c' (cteCap cte)) slot s \<Longrightarrow> (isPageTableCap (capCap c') \<and> (\<exists>a b. capPTMappedAddress (capCap c') = Some (a, b)) \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot s) \<and> ((isPageTableCap (capCap c') \<longrightarrow> capPTMappedAddress (capCap c') = None) \<longrightarrow> \<not> isPageTableCap (capCap c') \<longrightarrow> (isPageDirectoryCap (capCap c') \<and> (\<exists>y. capPDMappedASID (capCap c') = Some y) \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot s) \<and> ((isPageDirectoryCap (capCap c') \<longrightarrow> capPDMappedASID (capCap c') = None) \<longrightarrow> \<not> isPageDirectoryCap (capCap c') \<longrightarrow> (isPageCap (capCap c') \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot s) \<and> (\<not> isPageCap (capCap c') \<longrightarrow> (isASIDControlCap (capCap c') \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot s) \<and> (\<not> isASIDControlCap (capCap c') \<longrightarrow> (isASIDPoolCap (capCap c') \<longrightarrow> cte_wp_at' (\<lambda>_. True) slot s) \<and> isASIDPoolCap (capCap c'))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>ctes_of s slot = Some cte; (\<exists>d v0 v1 f. c' = capability.UntypedCap d v0 v1 f) \<longrightarrow> c' = cteCap cte; \<forall>v0 v1. capCap c' \<noteq> arch_capability.PageTableCap v0 v1; \<forall>v0 v1. capCap c' \<noteq> arch_capability.PageDirectoryCap v0 v1; \<forall>d v0 v1 v2 v3. capCap c' \<noteq> arch_capability.PageCap d v0 v1 v2 v3; capCap c' \<noteq> arch_capability.ASIDControlCap\<rbrakk> \<Longrightarrow> \<exists>v0 v1. capCap c' = arch_capability.ASIDPoolCap v0 v1
theory CSpace_R

lemma deriveCap_untyped_derived:
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. untyped_derived_eq c' (cteCap cte)) slot s\<rbrace>
  deriveCap slot c'
  \<lbrace>\<lambda>rv s. cte_wp_at' (untyped_derived_eq rv o cteCap) slot s\<rbrace>, -" apply (simp add: deriveCap_def split del: if_split) apply (rule hoare_pre) apply (wp arch_deriveCap_inv | simp add: o_def untyped_derived_eq_ArchObjectCap)+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps untyped_derived_eq_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. untyped_derived_eq c' (cteCap cte)) slot\<rbrace> global.deriveCap slot c' \<lbrace>\<lambda>rv. cte_wp_at' (untyped_derived_eq rv \<circ> cteCap) slot\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. untyped_derived_eq c' (cteCap cte)) slot\<rbrace> if isZombie c' then returnOk capability.NullCap else if isIRQControlCap c' then returnOk capability.NullCap else if isUntypedCap c' then doE y <- ensureNoChildren slot;
returnOk c'
odE else if isReplyCap c' then returnOk capability.NullCap else if isArchObjectCap c' then Arch.deriveCap slot (capCap c') else returnOk c' \<lbrace>\<lambda>rv. cte_wp_at' (untyped_derived_eq rv \<circ> cteCap) slot\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'12\<rbrace> if isZombie c' then returnOk capability.NullCap else if isIRQControlCap c' then returnOk capability.NullCap else if isUntypedCap c' then doE y <- ensureNoChildren slot;
returnOk c'
odE else if isReplyCap c' then returnOk capability.NullCap else if isArchObjectCap c' then Arch.deriveCap slot (capCap c') else returnOk c' \<lbrace>\<lambda>rv. cte_wp_at' (untyped_derived_eq rv \<circ> cteCap) slot\<rbrace>, -
 2. \<And>s. cte_wp_at' (\<lambda>cte. untyped_derived_eq c' (cteCap cte)) slot s \<Longrightarrow> ?P'12 s proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>cte. untyped_derived_eq c' (cteCap cte)) slot s \<Longrightarrow> (isZombie c' \<longrightarrow> cte_wp_at' (\<lambda>x. untyped_derived_eq capability.NullCap (cteCap x)) slot s) \<and> (\<not> isZombie c' \<longrightarrow> (isIRQControlCap c' \<longrightarrow> cte_wp_at' (\<lambda>x. untyped_derived_eq capability.NullCap (cteCap x)) slot s) \<and> (\<not> isIRQControlCap c' \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> isReplyCap c' \<longrightarrow> cte_wp_at' (\<lambda>x. untyped_derived_eq capability.NullCap (cteCap x)) slot s)) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma getCTE_symb_exec_r:
  "corres_underlying sr False nf' dc \<top> (cte_at' p) (return ()) (getCTE p)" apply (rule corres_no_failI, wp) apply (clarsimp simp: return_def
                 elim!: use_valid [OF _ getCTE_inv]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying sr False nf' dc (\<lambda>_. True) (cte_wp_at' (\<lambda>_. True) p) (return ()) (getCTE p) proof (prove)
goal (1 subgoal):
 1. \<forall>(s, s')\<in>sr. True \<and> cte_wp_at' (\<lambda>_. True) p s' \<longrightarrow> (\<forall>(r', t')\<in>fst (getCTE p s'). \<exists>(r, t)\<in>fst (return () s). (t, t') \<in> sr \<and> dc r r') proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma updateMDB_symb_exec_r:
  "corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False nf' dc
        \<top> (pspace_aligned' and pspace_distinct' and (no_0 \<circ> ctes_of) and (\<lambda>s. p \<noteq> 0 \<longrightarrow> cte_at' p s))
        (return ()) (updateMDB p m)" using no_fail_updateMDB [of p m] apply (clarsimp simp: corres_underlying_def return_def no_fail_def) apply (drule(1) updateMDB_the_lot, simp, assumption+) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False nf' dc (\<lambda>_. True) (pspace_aligned' and pspace_distinct' and no_0 \<circ> ctes_of and (\<lambda>s. p \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) p s)) (return ()) (updateMDB p m) proof (prove)
using this:
no_fail (\<lambda>s. p \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) p s) (updateMDB p m)

goal (1 subgoal):
 1. corres_underlying {(s, s'). pspace_relations (ekheap s) (kheap s) (ksPSpace s')} False nf' dc (\<lambda>_. True) (pspace_aligned' and pspace_distinct' and no_0 \<circ> ctes_of and (\<lambda>s. p \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) p s)) (return ()) (updateMDB p m) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>\<forall>s. (p \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) p s) \<longrightarrow> \<not> snd (updateMDB p m s); pspace_relations (ekheap a) (kheap a) (ksPSpace b); ((), ba) \<in> fst (updateMDB p m b); pspace_aligned' b; pspace_distinct' b; no_0 (ctes_of b); p \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) p b\<rbrakk> \<Longrightarrow> pspace_relations (ekheap a) (kheap a) (ksPSpace ba) proof (prove)
goal (1 subgoal):
 1. \<And>a b ba. \<lbrakk>\<forall>s. (p \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) p s) \<longrightarrow> \<not> snd (updateMDB p m s); pspace_relations (ekheap a) (kheap a) (ksPSpace b); pspace_aligned' b; pspace_distinct' b; no_0 (ctes_of b); p \<noteq> 0 \<longrightarrow> cte_wp_at' (\<lambda>_. True) p b; ctes_of ba = modify_map (ctes_of b) p (cteMDBNode_update m) \<and> ksMachineState ba = ksMachineState b \<and> ksWorkUnitsCompleted ba = ksWorkUnitsCompleted b \<and> ksCurThread ba = ksCurThread b \<and> ksIdleThread ba = ksIdleThread b \<and> ksReadyQueues ba = ksReadyQueues b \<and> ksSchedulerAction ba = ksSchedulerAction b \<and> ksInterruptState ba = ksInterruptState b \<and> ksArchState ba = ksArchState b \<and> gsUserPages ba = gsUserPages b \<and> gsCNodes ba = gsCNodes b \<and> pspace_relations (ekheap a) (kheap a) (ksPSpace ba) \<and> pspace_aligned' ba \<and> pspace_distinct' ba \<and> no_0 (ctes_of ba) \<and> ksDomScheduleIdx ba = ksDomScheduleIdx b \<and> ksDomSchedule ba = ksDomSchedule b \<and> ksCurDomain ba = ksCurDomain b \<and> ksDomainTime ba = ksDomainTime b\<rbrakk> \<Longrightarrow> pspace_relations (ekheap a) (kheap a) (ksPSpace ba) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma updateMDB_ctes_of_cases:
  "\<lbrace>\<lambda>s. P (modify_map (ctes_of s) p (if p = 0 then id else cteMDBNode_update f))\<rbrace>
     updateMDB p f \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" apply (simp add: updateMDB_def split del: if_split) apply (rule hoare_pre, wp getCTE_ctes_of) apply (clarsimp simp: modify_map_def map_option_case
                 split: option.split
          | rule conjI ext | erule rsubst[where P=P])+ apply (case_tac y, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (modify_map (ctes_of s) p (if p = 0 then id else cteMDBNode_update f))\<rbrace> updateMDB p f \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (modify_map (ctes_of s) p (if p = 0 then id else cteMDBNode_update f))\<rbrace> if p = 0 then return () else do cte <- getCTE p;
setCTE p (cteMDBNode_update (\<lambda>_. f (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (modify_map (ctes_of s) p (if p = 0 then id else cteMDBNode_update f)) \<Longrightarrow> (p = 0 \<longrightarrow> P (ctes_of s)) \<and> (p \<noteq> 0 \<longrightarrow> ctes_of s p \<noteq> None \<longrightarrow> P ((ctes_of s)(p \<mapsto> cteMDBNode_update (\<lambda>_. f (cteMDBNode (the (ctes_of s p)))) (the (ctes_of s p))))) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>p \<noteq> 0; ctes_of s p = Some y\<rbrakk> \<Longrightarrow> cteMDBNode_update f y = cteMDBNode_update (\<lambda>_. f (cteMDBNode y)) y proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_state_bits[wp]:
  "\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>"
  "\<lbrace>\<lambda>s. Q (ksIdleThread s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. Q (ksIdleThread s)\<rbrace>"
  "\<lbrace>\<lambda>s. R (ksArchState s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. R (ksArchState s)\<rbrace>"
  "\<lbrace>\<lambda>s. S (ksInterruptState s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. S (ksInterruptState s)\<rbrace>" apply (simp_all add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace> &&& \<lbrace>\<lambda>s. Q (ksIdleThread s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. Q (ksIdleThread s)\<rbrace>) &&& \<lbrace>\<lambda>s. R (ksArchState s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. R (ksArchState s)\<rbrace> &&& \<lbrace>\<lambda>s. S (ksInterruptState s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. S (ksInterruptState s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<lbrace>\<lambda>s. P (ksMachineState s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksMachineState s)\<rbrace>
 2. \<lbrace>\<lambda>s. Q (ksIdleThread s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. Q (ksIdleThread s)\<rbrace>
 3. \<lbrace>\<lambda>s. R (ksArchState s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. R (ksArchState s)\<rbrace>
 4. \<lbrace>\<lambda>s. S (ksInterruptState s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. S (ksInterruptState s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma cte_map_eq_subst:
  "\<lbrakk> cte_at p s; cte_at p' s; valid_objs s; pspace_aligned s; pspace_distinct s \<rbrakk>
     \<Longrightarrow> (cte_map p = cte_map p') = (p = p')" by (fastforce elim!: cte_map_inj_eq)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cte_wp_at (\<lambda>_. True) p s; cte_wp_at (\<lambda>_. True) p' s; valid_objs s; pspace_aligned s; pspace_distinct s\<rbrakk> \<Longrightarrow> (cte_map p = cte_map p') = (p = p')
theory CSpace_R

lemma revokable_relation_simp:
  "\<lbrakk> (s, s') \<in> state_relation; null_filter (caps_of_state s) p = Some c; ctes_of s' (cte_map p) = Some (CTE cap node) \<rbrakk>
      \<Longrightarrow> mdbRevocable node = is_original_cap s p" by (cases p, clarsimp simp: state_relation_def revokable_relation_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(s, s') \<in> state_relation; null_filter (caps_of_state s) p = Some c; ctes_of s' (cte_map p) = Some (CTE cap node)\<rbrakk> \<Longrightarrow> mdbRevocable node = is_original_cap s p
theory CSpace_R

lemma setCTE_gsUserPages[wp]:
  "\<lbrace>\<lambda>s. P (gsUserPages s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (gsUserPages s)\<rbrace>" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (gsUserPages s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (gsUserPages s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (gsUserPages s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (gsUserPages s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma set_original_symb_exec_l':
  "corres_underlying {(s, s'). f (ekheap s) (kheap s) s'} False nf' dc P P' (set_original p b) (return x)" by (simp add: corres_underlying_def return_def set_original_def in_monad Bex_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres_underlying {(s, s'). f (ekheap s) (kheap s) s'} False nf' dc P P' (set_original p b) (return x)
theory CSpace_R

lemma setCTE_schedule_index[wp]:
  "\<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksDomScheduleIdx s)\<rbrace>" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksDomScheduleIdx s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomScheduleIdx s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksDomScheduleIdx s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_schedule[wp]:
  "\<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace>" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomSchedule s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksDomSchedule s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_domain_time[wp]:
  "\<lbrace>\<lambda>s. P (ksDomainTime s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksDomainTime s)\<rbrace>" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomainTime s)\<rbrace> setCTE p v \<lbrace>\<lambda>rv s. P (ksDomainTime s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksDomainTime s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>rv s. P (ksDomainTime s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_work_units_completed[wp]:
  "\<lbrace>\<lambda>s. P (ksWorkUnitsCompleted s)\<rbrace> setCTE p v \<lbrace>\<lambda>_ s. P (ksWorkUnitsCompleted s)\<rbrace>" apply (simp add: setCTE_def setObject_def split_def) apply (wp updateObject_cte_inv crunch_wps | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksWorkUnitsCompleted s)\<rbrace> setCTE p v \<lbrace>\<lambda>_ s. P (ksWorkUnitsCompleted s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksWorkUnitsCompleted s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- updateObject v (snd pa) p (fst pa) (snd (lookupAround2 p ps));
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksWorkUnitsCompleted s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma cte_map_nat_to_cref:
  "\<lbrakk> n < 2 ^ b; b < word_bits \<rbrakk> \<Longrightarrow>
   cte_map (p, nat_to_cref b n) = p + (of_nat n * 2^cte_level_bits)" apply (clarsimp simp: cte_map_def nat_to_cref_def
                 dest!: less_is_drop_replicate) apply (rule arg_cong [where f="\<lambda>x. x * 2^cte_level_bits"]) apply (subst of_drop_to_bl) apply (simp add: word_bits_def) apply (subst mask_eq_iff_w2p) apply (simp add: word_size) apply (simp add: word_less_nat_alt word_size word_bits_def) apply (rule order_le_less_trans) defer apply assumption apply (subst unat_of_nat) apply (rule mod_less_eq_dividend) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ b; b < word_bits\<rbrakk> \<Longrightarrow> cte_map (p, nat_to_cref b n) = p + word_of_nat n * 2 ^ cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ b; b < word_bits\<rbrakk> \<Longrightarrow> of_bl (drop (word_bits - b) (to_bl (word_of_nat n))) * 2 ^ cte_level_bits = word_of_nat n * 2 ^ cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ b; b < word_bits\<rbrakk> \<Longrightarrow> of_bl (drop (word_bits - b) (to_bl (word_of_nat n))) = word_of_nat n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ b; b < word_bits\<rbrakk> \<Longrightarrow> word_of_nat n && mask (size (word_of_nat n) - (word_bits - b)) = word_of_nat n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> word_of_nat n && mask (size (word_of_nat n) + b - 32) = word_of_nat n proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> size (word_of_nat n) + b - 32 < size (word_of_nat n)
 2. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> word_of_nat n < 2 ^ (size (word_of_nat n) + b - 32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> word_of_nat n < 2 ^ (size (word_of_nat n) + b - 32) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) < 2 ^ b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) \<le> ?y7
 2. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> ?y7 < 2 ^ b proof (prove)
goal (2 subgoals):
 1. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> ?y7 < 2 ^ b
 2. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) \<le> ?y7 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> unat (word_of_nat n) \<le> n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n < 2 ^ b; b < 32\<rbrakk> \<Longrightarrow> n mod 2 ^ LENGTH(32) \<le> n proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma valid_nullcapsE:
  "\<lbrakk> valid_nullcaps m; m p = Some (CTE NullCap n);
    \<lbrakk> mdbPrev n = 0; mdbNext n = 0 \<rbrakk> \<Longrightarrow> P \<rbrakk>
  \<Longrightarrow> P" by (fastforce simp: valid_nullcaps_def nullMDBNode_def nullPointer_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_nullcaps m; m p = Some (CTE capability.NullCap n); \<lbrakk>mdbPrev n = 0; mdbNext n = 0\<rbrakk> \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P
theory CSpace_R

lemma valid_nullcaps_prev:
  "\<lbrakk> m (mdbPrev n) = Some (CTE NullCap n'); m p = Some (CTE c n);
    no_0 m; valid_dlist m; valid_nullcaps m \<rbrakk> \<Longrightarrow> False" apply (erule (1) valid_nullcapsE) apply (erule_tac p=p in valid_dlistEp, assumption) apply clarsimp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m (mdbPrev n) = Some (CTE capability.NullCap n'); m p = Some (CTE c n); no_0 m; valid_dlist m; valid_nullcaps m\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>m (mdbPrev n) = Some (CTE capability.NullCap n'); m p = Some (CTE c n); no_0 m; valid_dlist m; mdbPrev n' = 0; mdbNext n' = 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<lbrakk>m (mdbPrev n) = Some (CTE capability.NullCap n'); m p = Some (CTE c n); no_0 m; mdbPrev n' = 0; mdbNext n' = 0\<rbrakk> \<Longrightarrow> mdbPrev (cteMDBNode (CTE c n)) \<noteq> 0
 2. \<And>cte'. \<lbrakk>m (mdbPrev n) = Some (CTE capability.NullCap n'); m p = Some (CTE c n); no_0 m; mdbPrev n' = 0; mdbNext n' = 0; m (mdbPrev (cteMDBNode (CTE c n))) = Some cte'; mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte'. \<lbrakk>m (mdbPrev n) = Some (CTE capability.NullCap n'); m p = Some (CTE c n); no_0 m; mdbPrev n' = 0; mdbNext n' = 0; m (mdbPrev (cteMDBNode (CTE c n))) = Some cte'; mdbNext (cteMDBNode cte') = p\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!