kings-crown/FVELER_Isabelle huggingface dataset:
theory CSpace_R

lemma updateMDB_cteCaps_of:
  "\<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> updateMDB ptr f \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" apply (simp add: cteCaps_of_def) apply (wp updateMDB_ctes_of_wp) apply (safe elim!: rsubst [where P=P] intro!: ext) apply (case_tac "ctes_of s x") apply (clarsimp simp: modify_map_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> updateMDB ptr f \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (map_option cteCap \<circ> ctes_of s)\<rbrace> updateMDB ptr f \<lbrace>\<lambda>rv s. P (map_option cteCap \<circ> ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. P (map_option cteCap \<circ> ctes_of s) \<Longrightarrow> (ptr \<noteq> 0 \<longrightarrow> P (map_option cteCap \<circ> modify_map (ctes_of s) ptr (cteMDBNode_update f))) \<and> (ptr = 0 \<longrightarrow> P (map_option cteCap \<circ> ctes_of s)) proof (prove)
goal (1 subgoal):
 1. \<And>s x. ptr \<noteq> 0 \<Longrightarrow> (map_option cteCap \<circ> ctes_of s) x = (map_option cteCap \<circ> modify_map (ctes_of s) ptr (cteMDBNode_update f)) x proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>ptr \<noteq> 0; ctes_of s x = None\<rbrakk> \<Longrightarrow> (map_option cteCap \<circ> ctes_of s) x = (map_option cteCap \<circ> modify_map (ctes_of s) ptr (cteMDBNode_update f)) x
 2. \<And>s x a. \<lbrakk>ptr \<noteq> 0; ctes_of s x = Some a\<rbrakk> \<Longrightarrow> (map_option cteCap \<circ> ctes_of s) x = (map_option cteCap \<circ> modify_map (ctes_of s) ptr (cteMDBNode_update f)) x proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_ksInterruptState[wp]:
  "\<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> setCTE param_a param_b \<lbrace>\<lambda>_ s. P (ksInterruptState s)\<rbrace>" by (wp setObject_ksInterrupt updateObject_cte_inv | simp add: setCTE_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksInterruptState s)\<rbrace> setCTE param_a param_b \<lbrace>\<lambda>_ s. P (ksInterruptState s)\<rbrace>
theory CSpace_R

lemma getCTE_cteCap_wp:
  "\<lbrace>\<lambda>s. case (cteCaps_of s ptr) of None \<Rightarrow> True | Some cap \<Rightarrow> Q cap s\<rbrace> getCTE ptr \<lbrace>\<lambda>rv. Q (cteCap rv)\<rbrace>" apply (wp getCTE_wp) apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. case cteCaps_of s ptr of None \<Rightarrow> True | Some cap \<Rightarrow> Q cap s\<rbrace> getCTE ptr \<lbrace>\<lambda>rv. Q (cteCap rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. case cteCaps_of s ptr of None \<Rightarrow> True | Some cap \<Rightarrow> Q cap s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) ptr s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) ptr s \<and> Q (cteCap cte) s) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma capFreeIndex_update_cte_refs'[simp]:
  "isUntypedCap a \<Longrightarrow> cte_refs' (capFreeIndex_update f a) = cte_refs' a " apply (rule ext) apply (clarsimp simp:isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isUntypedCap a \<Longrightarrow> cte_refs' (capFreeIndex_update f a) = cte_refs' a proof (prove)
goal (1 subgoal):
 1. \<And>x. isUntypedCap a \<Longrightarrow> cte_refs' (capFreeIndex_update f a) x = cte_refs' a x proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_inQ[wp]:
  "\<lbrace>\<lambda>s. P (obj_at' (inQ d p) t s)\<rbrace> setCTE ptr v \<lbrace>\<lambda>rv s. P (obj_at' (inQ d p) t s)\<rbrace>" apply (simp add: setCTE_def) apply (rule setObject_cte_obj_at_tcb') apply (simp_all add: inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' (inQ d p) t s)\<rbrace> setCTE ptr v \<lbrace>\<lambda>rv s. P (obj_at' (inQ d p) t s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (obj_at' (inQ d p) t s)\<rbrace> setObject ptr v \<lbrace>\<lambda>rv s. P (obj_at' (inQ d p) t s)\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>tcb f. inQ d p (tcbCTable_update f tcb) = inQ d p tcb
 2. \<And>tcb f. inQ d p (tcbVTable_update f tcb) = inQ d p tcb
 3. \<And>tcb f. inQ d p (tcbReply_update f tcb) = inQ d p tcb
 4. \<And>tcb f. inQ d p (tcbCaller_update f tcb) = inQ d p tcb
 5. \<And>tcb f. inQ d p (tcbIPCBufferFrame_update f tcb) = inQ d p tcb proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_valid_queues'[wp]:
  "\<lbrace>valid_queues'\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (simp only: valid_queues'_def imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<forall>d p t. \<not> obj_at' (inQ d p) t s \<or> t \<in> set (ksReadyQueues s (d, p))\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. \<forall>d p t. \<not> obj_at' (inQ d p) t s \<or> t \<in> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_it'[wp]:
  "\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setCTE c p \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>" apply (simp add: setCTE_def setObject_def split_def updateObject_cte) apply (wp|wpc|simp del: hoare_fail_any)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setCTE c p \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 c ps));
obj' <- case snd pa of KOTCB tcb \<Rightarrow> do alignCheck (fst pa) (objBits tcb);
magnitudeCheck (fst pa) (snd (lookupAround2 c ps)) (objBits tcb);
if c - fst pa = tcbVTableSlot << objBits undefined then return (KOTCB (tcbVTable_update (\<lambda>_. p) tcb)) else if c - fst pa = tcbCTableSlot << objBits undefined then return (KOTCB (tcbCTable_update (\<lambda>_. p) tcb)) else if c - fst pa = tcbReplySlot << objBits undefined then return (KOTCB (tcbReply_update (\<lambda>_. p) tcb)) else if c - fst pa = tcbCallerSlot << objBits undefined then return (KOTCB (tcbCaller_update (\<lambda>_. p) tcb)) else if c - fst pa = tcbIPCBufferSlot << objBits undefined then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. p) tcb)) else fail
od | KOCTE v3 \<Rightarrow> do unless (c = fst pa) $ haskell_fail [];
alignCheck c (objBits p);
magnitudeCheck c (snd (lookupAround2 c ps)) (objBits p);
return (KOCTE p)
od | _ \<Rightarrow> typeError [] (snd pa);
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_idle [wp]:
  "\<lbrace>valid_idle'\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (simp add: valid_idle'_def) apply (rule hoare_lift_Pf [where f="ksIdleThread"]) apply (intro hoare_vcg_conj_lift; (solves \<open>wpsimp\<close>)?) apply (clarsimp simp: setCTE_def) apply (rule setObject_cte_obj_at_tcb'[where P="idle_tcb'", simplified]) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>\<lambda>s. obj_at' idle_tcb' x s \<and> idle_thread_ptr = x\<rbrace> setCTE p cte \<lbrace>\<lambda>_ a. obj_at' idle_tcb' x a \<and> idle_thread_ptr = x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setCTE p cte \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' idle_tcb' x\<rbrace> setCTE p cte \<lbrace>\<lambda>rv. obj_at' idle_tcb' x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setCTE p cte \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>obj_at' idle_tcb' x\<rbrace> setObject p cte \<lbrace>\<lambda>rv. obj_at' idle_tcb' x\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setCTE p cte \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> setCTE p cte \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma updateMDB_idle'[wp]:
 "\<lbrace>valid_idle'\<rbrace> updateMDB p m \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (clarsimp simp add: updateMDB_def) apply (rule hoare_pre) apply (wp | simp add: valid_idle'_def)+ by fastforce

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> updateMDB p m \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> \<lbrace>valid_idle'\<rbrace> do cte <- getCTE p;
setCTE p (cteMDBNode_update (\<lambda>_. m (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (2 subgoals):
 1. p \<noteq> 0 \<Longrightarrow> \<lbrace>?Q9\<rbrace> do cte <- getCTE p;
setCTE p (cteMDBNode_update (\<lambda>_. m (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>rv. valid_idle'\<rbrace>
 2. \<And>s. \<lbrakk>p \<noteq> 0; valid_idle' s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> 0; obj_at' idle_tcb' (ksIdleThread s) s \<and> idle_thread_ptr = ksIdleThread s\<rbrakk> \<Longrightarrow> obj_at' idle_tcb' idle_thread_ptr s
theory CSpace_R

lemma updateCap_idle':
 "\<lbrace>valid_idle'\<rbrace> updateCap p c \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (simp add: updateCap_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> updateCap p c \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> do cte <- getCTE p;
setCTE p (cteCap_update (\<lambda>_. c) cte)
od \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma cteInsert_idle'[wp]:
 "\<lbrace>valid_idle'\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. valid_idle'\<rbrace>" apply (simp add: cteInsert_def) apply (wp updateMDB_idle' updateCap_idle' | rule hoare_drop_imp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_idle'\<rbrace> do srcCTE <- getCTE src;
oldCTE <- getCTE dest;
y <- assert (cteCap oldCTE = capability.NullCap);
y <- assert (mdbPrev (cteMDBNode oldCTE) = nullPointer \<and> mdbNext (cteMDBNode oldCTE) = nullPointer);
y <- setUntypedCapAsFull (cteCap srcCTE) cap src;
y <- updateCap dest cap;
y <- updateMDB dest (const (mdbFirstBadged_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbRevocable_update (\<lambda>_. revokable' (cteCap srcCTE) cap) (mdbPrev_update (\<lambda>_. src) (cteMDBNode srcCTE)))));
y <- updateMDB src (mdbNext_update (\<lambda>_. dest));
updateMDB (mdbNext (cteMDBNode srcCTE)) (mdbPrev_update (\<lambda>_. dest))
od \<lbrace>\<lambda>rv. valid_idle'\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_arch [wp]:
  "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setCTE p c \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>" apply (simp add: setCTE_def setObject_def split_def updateObject_cte) apply (wp|wpc|simp del: hoare_fail_any)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setCTE p c \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- case snd pa of KOTCB tcb \<Rightarrow> do alignCheck (fst pa) (objBits tcb);
magnitudeCheck (fst pa) (snd (lookupAround2 p ps)) (objBits tcb);
if p - fst pa = tcbVTableSlot << objBits undefined then return (KOTCB (tcbVTable_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbCTableSlot << objBits undefined then return (KOTCB (tcbCTable_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbReplySlot << objBits undefined then return (KOTCB (tcbReply_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbCallerSlot << objBits undefined then return (KOTCB (tcbCaller_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbIPCBufferSlot << objBits undefined then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. c) tcb)) else fail
od | KOCTE v3 \<Rightarrow> do unless (p = fst pa) $ haskell_fail [];
alignCheck p (objBits c);
magnitudeCheck p (snd (lookupAround2 p ps)) (objBits c);
return (KOCTE c)
od | _ \<Rightarrow> typeError [] (snd pa);
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_valid_arch[wp]:
  "\<lbrace>valid_arch_state'\<rbrace> setCTE p c \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" by (wp valid_arch_state_lift' setCTE_typ_at')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> setCTE p c \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>
theory CSpace_R

lemma setCTE_global_refs[wp]:
  "\<lbrace>\<lambda>s. P (global_refs' s)\<rbrace> setCTE p c \<lbrace>\<lambda>_ s. P (global_refs' s)\<rbrace>" apply (simp add: setCTE_def setObject_def split_def updateObject_cte global_refs'_def) apply (wp|wpc|simp del: hoare_fail_any)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (global_refs' s)\<rbrace> setCTE p c \<lbrace>\<lambda>_ s. P (global_refs' s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (insert (ksIdleThread s) (page_directory_refs' (armKSGlobalPD (ksArchState s)) \<union> \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<union> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits))))\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- case snd pa of KOTCB tcb \<Rightarrow> do alignCheck (fst pa) (objBits tcb);
magnitudeCheck (fst pa) (snd (lookupAround2 p ps)) (objBits tcb);
if p - fst pa = tcbVTableSlot << objBits undefined then return (KOTCB (tcbVTable_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbCTableSlot << objBits undefined then return (KOTCB (tcbCTable_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbReplySlot << objBits undefined then return (KOTCB (tcbReply_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbCallerSlot << objBits undefined then return (KOTCB (tcbCaller_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbIPCBufferSlot << objBits undefined then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. c) tcb)) else fail
od | KOCTE v3 \<Rightarrow> do unless (p = fst pa) $ haskell_fail [];
alignCheck p (objBits c);
magnitudeCheck p (snd (lookupAround2 p ps)) (objBits c);
return (KOCTE c)
od | _ \<Rightarrow> typeError [] (snd pa);
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (insert (ksIdleThread s) (page_directory_refs' (armKSGlobalPD (ksArchState s)) \<union> \<Union> (page_table_refs' ` set (armKSGlobalPTs (ksArchState s))) \<union> range (\<lambda>irq. irq_node' s + (UCAST(10 \<rightarrow> 32) irq << cteSizeBits))))\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma setCTE_gsMaxObjectSize[wp]:
  "\<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> setCTE p c \<lbrace>\<lambda>_ s. P (gsMaxObjectSize s)\<rbrace>" apply (simp add: setCTE_def setObject_def split_def updateObject_cte) apply (wp|wpc|simp del: hoare_fail_any)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> setCTE p c \<lbrace>\<lambda>_ s. P (gsMaxObjectSize s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (gsMaxObjectSize s)\<rbrace> do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- case snd pa of KOTCB tcb \<Rightarrow> do alignCheck (fst pa) (objBits tcb);
magnitudeCheck (fst pa) (snd (lookupAround2 p ps)) (objBits tcb);
if p - fst pa = tcbVTableSlot << objBits undefined then return (KOTCB (tcbVTable_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbCTableSlot << objBits undefined then return (KOTCB (tcbCTable_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbReplySlot << objBits undefined then return (KOTCB (tcbReply_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbCallerSlot << objBits undefined then return (KOTCB (tcbCaller_update (\<lambda>_. c) tcb)) else if p - fst pa = tcbIPCBufferSlot << objBits undefined then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. c) tcb)) else fail
od | KOCTE v3 \<Rightarrow> do unless (p = fst pa) $ haskell_fail [];
alignCheck p (objBits c);
magnitudeCheck p (snd (lookupAround2 p ps)) (objBits c);
return (KOCTE c)
od | _ \<Rightarrow> typeError [] (snd pa);
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od \<lbrace>\<lambda>_ s. P (gsMaxObjectSize s)\<rbrace> proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma updateMDB_global_refs [wp]:
 "\<lbrace>valid_global_refs'\<rbrace> updateMDB p m \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" apply (clarsimp simp add: updateMDB_def) apply (rule hoare_pre) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of valid_global_refs'_def valid_refs'_def valid_cap_sizes'_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs'\<rbrace> updateMDB p m \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. p \<noteq> 0 \<Longrightarrow> \<lbrace>valid_global_refs'\<rbrace> do cte <- getCTE p;
setCTE p (cteMDBNode_update (\<lambda>_. m (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. p \<noteq> 0 \<Longrightarrow> \<lbrace>?Q9\<rbrace> do cte <- getCTE p;
setCTE p (cteMDBNode_update (\<lambda>_. m (cteMDBNode cte)) cte)
od \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>
 2. \<And>s. \<lbrakk>p \<noteq> 0; valid_global_refs' s\<rbrakk> \<Longrightarrow> ?Q9 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>p \<noteq> 0; valid_global_refs' s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (cteCap (cteMDBNode_update (\<lambda>_. m (cteMDBNode cte)) cte)) = {}) and (\<lambda>s. 2 ^ capBits (cteCap (cteMDBNode_update (\<lambda>_. m (cteMDBNode cte)) cte)) \<le> gsMaxObjectSize s)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>p \<noteq> 0; \<forall>c\<in>ran (ctes_of s). kernel_data_refs \<inter> capRange (cteCap c) = {}; global_refs' s \<subseteq> kernel_data_refs; \<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s; ctes_of s p = Some cte\<rbrakk> \<Longrightarrow> kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> 2 ^ capBits (cteCap cte) \<le> gsMaxObjectSize s proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma updateCap_global_refs [wp]:
 "\<lbrace>valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange cap = {})
     and (\<lambda>s. 2 ^ capBits cap \<le> gsMaxObjectSize s)\<rbrace>
  updateCap p cap
  \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" apply (clarsimp simp add: updateCap_def) apply (rule hoare_pre) apply (wp getCTE_wp) apply (clarsimp simp: cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange cap = {}) and (\<lambda>s. 2 ^ capBits cap \<le> gsMaxObjectSize s)\<rbrace> updateCap p cap \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange cap = {}) and (\<lambda>s. 2 ^ capBits cap \<le> gsMaxObjectSize s)\<rbrace> do cte <- getCTE p;
setCTE p (cteCap_update (\<lambda>_. cap) cte)
od \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do cte <- getCTE p;
setCTE p (cteCap_update (\<lambda>_. cap) cte)
od \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>
 2. \<And>s. (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange cap = {}) and (\<lambda>s. 2 ^ capBits cap \<le> gsMaxObjectSize s)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange cap = {}) and (\<lambda>s. 2 ^ capBits cap \<le> gsMaxObjectSize s)) s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) p s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> (valid_global_refs' and (\<lambda>s. kernel_data_refs \<inter> capRange (cteCap (cteCap_update (\<lambda>_. cap) cte)) = {}) and (\<lambda>s. 2 ^ capBits (cteCap (cteCap_update (\<lambda>_. cap) cte)) \<le> gsMaxObjectSize s)) s) proof (prove)
goal:
No subgoals!
theory CSpace_R

lemma cteInsert_valid_arch [wp]:
 "\<lbrace>valid_arch_state'\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>" by (rule valid_arch_state_lift'; wp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state'\<rbrace> cteInsert cap src dest \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>
theory CSpace_R

lemma setCTE_valid_mappings'[wp]:
  "\<lbrace>valid_pde_mappings'\<rbrace> setCTE x y \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" apply (wp valid_pde_mappings_lift' setCTE_typ_at') apply (simp add: setCTE_def) apply (rule obj_at_setObject2) apply (clarsimp simp: updateObject_cte typeError_def in_monad
                  split: Structures_H.kernel_object.split_asm if_split_asm) apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_pde_mappings'\<rbrace> setCTE x y \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrace>obj_at' (valid_pde_mapping' (xa && mask pdBits)) xa\<rbrace> setCTE x y \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (xa && mask pdBits)) xa\<rbrace>
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>xa. \<lbrace>obj_at' (valid_pde_mapping' (xa && mask pdBits)) xa\<rbrace> setObject x y \<lbrace>\<lambda>rv. obj_at' (valid_pde_mapping' (xa && mask pdBits)) xa\<rbrace>
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (2 subgoals):
 1. \<And>x ko s' v oko xa y n s. (ko, s') \<in> fst (updateObject v oko xa y n s) \<Longrightarrow> koTypeOf ko \<noteq> koType TYPE(ARM_H.pde)
 2. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pde_mappings' s \<Longrightarrow> valid_pde_mappings' s proof (prove)
goal:
No subgoals!