theory CSpace_R

lemma setCTE_irq_states' [wp]:
  "\<lbrace>valid_irq_states'\<rbrace> setCTE x y \<lbrace>\<lambda>_. valid_irq_states'\<rbrace>" apply (rule valid_irq_states_lift') apply wp apply (simp add: setCTE_def) apply (wp setObject_ksMachine) apply (simp add: updateObject_cte) apply (rule hoare_pre) apply (wp unless_wp|wpc|simp)+ apply fastforce apply assumption done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_irq_states'\<rbrace> setCTE x y \<lbrace>\<lambda>_. valid_irq_states'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. P (intStateIRQTable (ksInterruptState s))\<rbrace> setCTE x y \<lbrace>\<lambda>_ s. P (intStateIRQTable (ksInterruptState s))\<rbrace>
 2. \<And>P. \<lbrace>\<lambda>s. P (irq_masks (ksMachineState s))\<rbrace> setCTE x y \<lbrace>\<lambda>_ s. P (irq_masks (ksMachineState s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_masks (ksMachineState s))\<rbrace> setCTE x y \<lbrace>\<lambda>_ s. P (irq_masks (ksMachineState s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>s. P (irq_masks (ksMachineState s))\<rbrace> setObject x y \<lbrace>\<lambda>_ s. P (irq_masks (ksMachineState s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P p q n ko. \<lbrace>\<lambda>s. P (irq_masks (ksMachineState s))\<rbrace> updateObject y p q n ko \<lbrace>\<lambda>_ s. P (irq_masks (ksMachineState s))\<rbrace>
 2. \<And>P s. P (irq_masks (ksMachineState s)) \<Longrightarrow> P (irq_masks (ksMachineState s)) proof (prove)
goal (2 subgoals):
 1. \<And>P p q n ko. \<lbrace>\<lambda>s. P (irq_masks (ksMachineState s))\<rbrace> case p of KOTCB tcb \<Rightarrow> do alignCheck n (objBits tcb);
magnitudeCheck n ko (objBits tcb);
if q - n = tcbVTableSlot << objBits undefined then return (KOTCB (tcbVTable_update (\<lambda>_. y) tcb)) else if q - n = tcbCTableSlot << objBits undefined then return (KOTCB (tcbCTable_update (\<lambda>_. y) tcb)) else if q - n = tcbReplySlot << objBits undefined then return (KOTCB (tcbReply_update (\<lambda>_. y) tcb)) else if q - n = tcbCallerSlot << objBits undefined then return (KOTCB (tcbCaller_update (\<lambda>_. y) tcb)) else if q - n = tcbIPCBufferSlot << objBits undefined then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. y) tcb)) else fail
od | KOCTE v3 \<Rightarrow> do unless (q = n) $ haskell_fail [];
alignCheck q (objBits y);
magnitudeCheck q ko (objBits y);
return (KOCTE y)
od | _ \<Rightarrow> typeError [] p \<lbrace>\<lambda>_ s. P (irq_masks (ksMachineState s))\<rbrace>
 2. \<And>P s. P (irq_masks (ksMachineState s)) \<Longrightarrow> P (irq_masks (ksMachineState s)) proof (prove)
goal (3 subgoals):
 1. \<And>P p q n ko. \<lbrace>?Q15 P p q n ko\<rbrace> case p of KOTCB tcb \<Rightarrow> do alignCheck n (objBits tcb);
magnitudeCheck n ko (objBits tcb);
if q - n = tcbVTableSlot << objBits undefined then return (KOTCB (tcbVTable_update (\<lambda>_. y) tcb)) else if q - n = tcbCTableSlot << objBits undefined then return (KOTCB (tcbCTable_update (\<lambda>_. y) tcb)) else if q - n = tcbReplySlot << objBits undefined then return (KOTCB (tcbReply_update (\<lambda>_. y) tcb)) else if q - n = tcbCallerSlot << objBits undefined then return (KOTCB (tcbCaller_update (\<lambda>_. y) tcb)) else if q - n = tcbIPCBufferSlot << objBits undefined then return (KOTCB (tcbIPCBufferFrame_update (\<lambda>_. y) tcb)) else fail
od | KOCTE v3 \<Rightarrow> do unless (q = n) $ haskell_fail [];
alignCheck q (objBits y);
magnitudeCheck q ko (objBits y);
return (KOCTE y)
od | _ \<Rightarrow> typeError [] p \<lbrace>\<lambda>_ s. P (irq_masks (ksMachineState s))\<rbrace>
 2. \<And>P p q n ko s. P (irq_masks (ksMachineState s)) \<Longrightarrow> ?Q15 P p q n ko s
 3. \<And>P s. P (irq_masks (ksMachineState s)) \<Longrightarrow> P (irq_masks (ksMachineState s)) proof (prove)
goal (2 subgoals):
 1. \<And>P p q n ko s. P (irq_masks (ksMachineState s)) \<Longrightarrow> q \<noteq> n \<longrightarrow> (\<forall>x. p = KOCTE x \<longrightarrow> ?Q102 P (KOCTE x) q n ko x s)
 2. \<And>P s. P (irq_masks (ksMachineState s)) \<Longrightarrow> P (irq_masks (ksMachineState s)) proof (prove)
goal (1 subgoal):
 1. \<And>P s. P (irq_masks (ksMachineState s)) \<Longrightarrow> P (irq_masks (ksMachineState s)) proof (prove)
goal:
No subgoals!