theory KHeap_R

lemma updateObject_cte_is_tcb_or_cte:
  fixes cte :: cte and ptr :: word32
  shows "\<lbrakk> fst (lookupAround2 p (ksPSpace s)) = Some (q, ko);
           snd (lookupAround2 p (ksPSpace s)) = n;
           (ko', s') \<in> fst (updateObject cte ko p q n s) \<rbrakk> \<Longrightarrow>
  (\<exists>tcb getF setF. ko = KOTCB tcb \<and> s' = s \<and> tcb_cte_cases (p - q) = Some (getF, setF)
    \<and> ko' = KOTCB (setF (\<lambda>x. cte) tcb) \<and> is_aligned q tcbBlockSizeBits \<and> ps_clear q tcbBlockSizeBits s) \<or>
  (\<exists>cte'. ko = KOCTE cte' \<and> ko' = KOCTE cte \<and> s' = s
        \<and> p = q \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits s)" apply (clarsimp simp: updateObject_cte typeError_def alignError_def
               tcbVTableSlot_def tcbCTableSlot_def to_bl_1 rev_take objBits_simps'
               in_monad map_bits_to_bl cte_level_bits_def in_magnitude_check
               lookupAround2_char1
         split: kernel_object.splits) apply (subst(asm) in_magnitude_check3, simp+) apply (simp add: in_monad tcbCTableSlot_def tcbVTableSlot_def
                    tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def
             split: if_split_asm) apply (simp add: in_monad tcbCTableSlot_def tcbVTableSlot_def
                   tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def
            split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>fst (lookupAround2 p (ksPSpace s)) = Some (q, ko); snd (lookupAround2 p (ksPSpace s)) = n; (ko', s') \<in> fst (updateObject cte ko p q n s)\<rbrakk> \<Longrightarrow> (\<exists>tcb getF setF. ko = KOTCB tcb \<and> s' = s \<and> tcb_cte_cases (p - q) = Some (getF, setF) \<and> ko' = KOTCB (setF (\<lambda>x. cte) tcb) \<and> is_aligned q tcbBlockSizeBits \<and> ps_clear q tcbBlockSizeBits s) \<or> (\<exists>cte'. ko = KOCTE cte' \<and> ko' = KOCTE cte \<and> s' = s \<and> p = q \<and> is_aligned p cte_level_bits \<and> ps_clear p cte_level_bits s) proof (prove)
goal (1 subgoal):
 1. \<And>x6 s''. \<lbrakk>q \<le> p; ksPSpace s q = Some (KOTCB x6); \<forall>z. q < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ko = KOTCB x6; n = snd (lookupAround2 p (ksPSpace s)); is_aligned q 9; ((), s'') \<in> fst (magnitudeCheck q (snd (lookupAround2 p (ksPSpace s))) 9 s); (ko', s') \<in> fst ((if p - q = 0x10 then return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6)) else if p = q then return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6)) else if p - q = tcbReplySlot << 4 then return (KOTCB (tcbReply_update (\<lambda>_. cte) x6)) else if p - q = tcbCallerSlot << 4 then return (KOTCB (tcbCaller_update (\<lambda>_. cte) x6)) else if p - q = tcbIPCBufferSlot << 4 then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) x6)) else fail) s'')\<rbrakk> \<Longrightarrow> s' = s \<and> (\<exists>getF setF. tcb_cte_cases (p - q) = Some (getF, setF) \<and> ko' = KOTCB (setF (\<lambda>x. cte) x6) \<and> ps_clear q 9 s) proof (prove)
goal (2 subgoals):
 1. \<And>x6 s''. \<lbrakk>(ko', s') \<in> fst ((if p - q = 0x10 then return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6)) else if p = q then return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6)) else if p - q = tcbReplySlot << 4 then return (KOTCB (tcbReply_update (\<lambda>_. cte) x6)) else if p - q = tcbCallerSlot << 4 then return (KOTCB (tcbCaller_update (\<lambda>_. cte) x6)) else if p - q = tcbIPCBufferSlot << 4 then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) x6)) else fail) s''); q \<le> p; ksPSpace s q = Some (KOTCB x6); \<forall>z. q < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ko = KOTCB x6; n = snd (lookupAround2 p (ksPSpace s)); is_aligned q 9\<rbrakk> \<Longrightarrow> p - q < 0x200
 2. \<And>x6 s''. \<lbrakk>q \<le> p; ksPSpace s q = Some (KOTCB x6); \<forall>z. q < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ko = KOTCB x6; n = snd (lookupAround2 p (ksPSpace s)); is_aligned q 9; ((), s'') \<in> (if ps_clear q 9 s then {((), s)} else {}); (ko', s') \<in> fst ((if p - q = 0x10 then return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6)) else if p = q then return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6)) else if p - q = tcbReplySlot << 4 then return (KOTCB (tcbReply_update (\<lambda>_. cte) x6)) else if p - q = tcbCallerSlot << 4 then return (KOTCB (tcbCaller_update (\<lambda>_. cte) x6)) else if p - q = tcbIPCBufferSlot << 4 then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) x6)) else fail) s'')\<rbrakk> \<Longrightarrow> s' = s \<and> (\<exists>getF setF. tcb_cte_cases (p - q) = Some (getF, setF) \<and> ko' = KOTCB (setF (\<lambda>x. cte) x6) \<and> ps_clear q 9 s) proof (prove)
goal (1 subgoal):
 1. \<And>x6 s''. \<lbrakk>q \<le> p; ksPSpace s q = Some (KOTCB x6); \<forall>z. q < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; ko = KOTCB x6; n = snd (lookupAround2 p (ksPSpace s)); is_aligned q 9; ((), s'') \<in> (if ps_clear q 9 s then {((), s)} else {}); (ko', s') \<in> fst ((if p - q = 0x10 then return (KOTCB (tcbVTable_update (\<lambda>_. cte) x6)) else if p = q then return (KOTCB (tcbCTable_update (\<lambda>_. cte) x6)) else if p - q = tcbReplySlot << 4 then return (KOTCB (tcbReply_update (\<lambda>_. cte) x6)) else if p - q = tcbCallerSlot << 4 then return (KOTCB (tcbCaller_update (\<lambda>_. cte) x6)) else if p - q = tcbIPCBufferSlot << 4 then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) x6)) else fail) s'')\<rbrakk> \<Longrightarrow> s' = s \<and> (\<exists>getF setF. tcb_cte_cases (p - q) = Some (getF, setF) \<and> ko' = KOTCB (setF (\<lambda>x. cte) x6) \<and> ps_clear q 9 s) proof (prove)
goal:
No subgoals!