theory CSpace1_R

lemma no_fail_setCTE [wp]:
  "no_fail (cte_at' p) (setCTE p c)" apply (clarsimp simp: setCTE_def setObject_def split_def unless_def
                        updateObject_cte alignCheck_def alignError_def
                        typeError_def is_aligned_mask[symmetric]
                  cong: kernel_object.case_cong) apply (wp|wpc)+ apply (clarsimp simp: cte_wp_at'_def getObject_def split_def
                        in_monad loadObject_cte
                 dest!: in_singleton
             split del: if_split) apply (clarsimp simp: typeError_def alignCheck_def alignError_def
                        in_monad is_aligned_mask[symmetric] objBits_simps
                        magnitudeCheck_def
                 split: kernel_object.split_asm if_split_asm option.splits
             split del: if_split) apply simp_all done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. no_fail (cte_wp_at' (\<lambda>_. True) p) (setCTE p c) proof (prove)
goal (1 subgoal):
 1. no_fail (cte_wp_at' (\<lambda>_. True) p) (do ps <- gets ksPSpace;
pa <- assert_opt (fst (lookupAround2 p ps));
obj' <- case snd pa of KOTCB tcb \<Rightarrow> do y <- when (\<not> is_aligned (fst pa) (objBits tcb)) fail;
y <- 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 y <- when (p \<noteq> fst pa) fail;
y <- when (\<not> is_aligned p (objBits c)) fail;
y <- magnitudeCheck p (snd (lookupAround2 p ps)) (objBits c);
return (KOCTE c)
od | _ \<Rightarrow> fail;
modify (ksPSpace_update (\<lambda>_. ps(fst pa \<mapsto> obj')))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>_. True) p s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. fst (lookupAround2 p (ksPSpace s)) \<noteq> None) and (\<lambda>sa. fst (lookupAround2 p (ksPSpace s)) \<noteq> None \<longrightarrow> ((\<lambda>sa. (\<forall>x. snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOEndpoint x \<longrightarrow> False) \<and> (\<forall>x. snd (the (fst (lookupAround2 p (ksPSpace s)))) = KONotification x \<longrightarrow> False) \<and> (snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOKernelData \<longrightarrow> False) \<and> (snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOUserData \<longrightarrow> False) \<and> (snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOUserDataDevice \<longrightarrow> False) \<and> (\<forall>x. snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOTCB x \<longrightarrow> ((if \<not> is_aligned (fst (the (fst (lookupAround2 p (ksPSpace s))))) (objBits x) then \<lambda>_. False else (\<lambda>_. True)) and (\<lambda>sa. (case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x \<le> z - fst (the (fst (lookupAround2 p (ksPSpace s))))) \<and> (if \<not> is_aligned (fst (the (fst (lookupAround2 p (ksPSpace s))))) (objBits x) then \<lambda>_. True else if p - fst (the (fst (lookupAround2 p (ksPSpace s)))) = tcbVTableSlot << objBits undefined then \<lambda>_. True else if p - fst (the (fst (lookupAround2 p (ksPSpace s)))) = tcbCTableSlot << objBits undefined then \<lambda>_. True else if p - fst (the (fst (lookupAround2 p (ksPSpace s)))) = tcbReplySlot << objBits undefined then \<lambda>_. True else if p - fst (the (fst (lookupAround2 p (ksPSpace s)))) = tcbCallerSlot << objBits undefined then \<lambda>_. True else if p - fst (the (fst (lookupAround2 p (ksPSpace s)))) = tcbIPCBufferSlot << objBits undefined then \<lambda>_. True else (\<lambda>_. False)) sa)) sa) \<and> (\<forall>x. snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOCTE x \<longrightarrow> ((if p \<noteq> fst (the (fst (lookupAround2 p (ksPSpace s)))) then \<lambda>_. False else (\<lambda>_. True)) and (if p \<noteq> fst (the (fst (lookupAround2 p (ksPSpace s)))) then \<lambda>_. True else (\<lambda>sa. (if \<not> is_aligned p (objBits c) then \<lambda>_. False else (\<lambda>_. True)) sa \<and> (case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits c \<le> z - p) \<and> True))) sa) \<and> (\<forall>x. snd (the (fst (lookupAround2 p (ksPSpace s)))) = KOArch x \<longrightarrow> False)) and (\<lambda>_. True)) sa)) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte a b. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, b); (cte, s) \<in> fst ((case b of KOTCB tcb \<Rightarrow> do alignCheck (fst (a, b)) (objBits tcb);
magnitudeCheck (fst (a, b)) (snd (lookupAround2 p (ksPSpace s))) (objBits tcb);
if p - fst (a, b) = tcbVTableSlot << objBits undefined then return (tcbVTable tcb) else if p - fst (a, b) = tcbCTableSlot << objBits undefined then return (tcbCTable tcb) else if p - fst (a, b) = tcbReplySlot << objBits undefined then return (tcbReply tcb) else if p - fst (a, b) = tcbCallerSlot << objBits undefined then return (tcbCaller tcb) else if p - fst (a, b) = tcbIPCBufferSlot << objBits undefined then return (tcbIPCBufferFrame tcb) else fail
od | KOCTE cte \<Rightarrow> do unless (p = fst (a, b)) $ haskell_fail [];
alignCheck p (objBits cte);
magnitudeCheck p (snd (lookupAround2 p (ksPSpace s))) (objBits cte);
return cte
od | _ \<Rightarrow> typeError [] (snd (a, b))) s)\<rbrakk> \<Longrightarrow> (\<forall>x. b \<noteq> KOEndpoint x) \<and> (\<forall>x. b \<noteq> KONotification x) \<and> b \<noteq> KOKernelData \<and> b \<noteq> KOUserData \<and> b \<noteq> KOUserDataDevice \<and> (\<forall>x. b = KOTCB x \<longrightarrow> (if \<not> is_aligned a (objBits x) then \<lambda>_. False else (\<lambda>_. True)) s \<and> (case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits x \<le> z - a) \<and> (if \<not> is_aligned a (objBits x) then \<lambda>_. True else if p - a = tcbVTableSlot << objBits undefined then \<lambda>_. True else if p - a = tcbCTableSlot << objBits undefined then \<lambda>_. True else if p - a = tcbReplySlot << objBits undefined then \<lambda>_. True else if p - a = tcbCallerSlot << objBits undefined then \<lambda>_. True else if p - a = tcbIPCBufferSlot << objBits undefined then \<lambda>_. True else (\<lambda>_. False)) s) \<and> ((\<exists>x. b = KOCTE x) \<longrightarrow> (if p \<noteq> a then \<lambda>_. False else (\<lambda>_. True)) s \<and> (if p \<noteq> a then \<lambda>_. True else (\<lambda>sa. (if \<not> is_aligned p (objBits c) then \<lambda>_. False else (\<lambda>_. True)) sa \<and> (case snd (lookupAround2 p (ksPSpace s)) of None \<Rightarrow> True | Some z \<Rightarrow> 2 ^ objBits c \<le> z - p))) s) \<and> (\<forall>x. b \<noteq> KOArch x) proof (prove)
goal (6 subgoals):
 1. \<And>s a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); p - a = tcbVTableSlot << cteSizeBits; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a tcbBlockSizeBits; \<not> x2 - a < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a
 2. \<And>s a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbCTableSlot << cteSizeBits \<noteq> tcbVTableSlot << cteSizeBits; p - a = tcbCTableSlot << cteSizeBits; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a tcbBlockSizeBits; \<not> x2 - a < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a
 3. \<And>s a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbReplySlot << cteSizeBits \<noteq> tcbVTableSlot << cteSizeBits; tcbReplySlot << cteSizeBits \<noteq> tcbCTableSlot << cteSizeBits; p - a = tcbReplySlot << cteSizeBits; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a tcbBlockSizeBits; \<not> x2 - a < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a
 4. \<And>s a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbCallerSlot << cteSizeBits \<noteq> tcbVTableSlot << cteSizeBits; tcbCallerSlot << cteSizeBits \<noteq> tcbCTableSlot << cteSizeBits; tcbCallerSlot << cteSizeBits \<noteq> tcbReplySlot << cteSizeBits; p - a = tcbCallerSlot << cteSizeBits; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a tcbBlockSizeBits; \<not> x2 - a < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a
 5. \<And>s a x6 x2. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (a, KOTCB x6); tcbIPCBufferSlot << cteSizeBits \<noteq> tcbVTableSlot << cteSizeBits; tcbIPCBufferSlot << cteSizeBits \<noteq> tcbCTableSlot << cteSizeBits; tcbIPCBufferSlot << cteSizeBits \<noteq> tcbReplySlot << cteSizeBits; tcbIPCBufferSlot << cteSizeBits \<noteq> tcbCallerSlot << cteSizeBits; p - a = tcbIPCBufferSlot << cteSizeBits; snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned a tcbBlockSizeBits; \<not> x2 - a < 2 ^ tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2 ^ tcbBlockSizeBits \<le> x2 - a
 6. \<And>s x7 x2. \<lbrakk>ksPSpace s p = Some (KOCTE x7); snd (lookupAround2 p (ksPSpace s)) = Some x2; is_aligned p cteSizeBits; \<not> x2 - p < 2 ^ cteSizeBits\<rbrakk> \<Longrightarrow> 2 ^ cteSizeBits \<le> x2 - p proof (prove)
goal:
No subgoals!