theory IsolatedThreadAction

lemma lookupIPCBuffer_isolatable:
  "thread_actions_isolatable idx (lookupIPCBuffer w t)" supply if_split[split del] if_cong[cong] apply (simp add: lookupIPCBuffer_def) apply (rule thread_actions_isolatable_bind) apply (clarsimp simp: put_tcb_state_regs_tcb_def threadGet_isolatable
                        getThreadBufferSlot_def locateSlot_conv getSlotCap_def
                  split: tcb_state_regs.split)+ apply (rule thread_actions_isolatable_bind) apply (clarsimp simp: thread_actions_isolatable_return
                          getCTE_isolatable
                          assert_isolatable
                   split: capability.split arch_capability.split bool.split)+ apply (rule thread_actions_isolatable_if) apply (rule thread_actions_isolatable_bind) apply (simp add: assert_isolatable thread_actions_isolatable_return | wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (lookupIPCBuffer w t) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (lookupIPCBuffer w t) proof (prove)
goal (1 subgoal):
 1. thread_actions_isolatable idx (do bufferPtr <- threadGet tcbIPCBuffer t;
bufferFrameSlot <- getThreadBufferSlot t;
bufferCap <- getSlotCap bufferFrameSlot;
case bufferCap of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz x) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz x) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr bufferPtr && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return Nothing | _ \<Rightarrow> return Nothing
od) proof (prove)
goal (3 subgoals):
 1. thread_actions_isolatable idx (threadGet tcbIPCBuffer t)
 2. \<And>x. thread_actions_isolatable idx (do bufferFrameSlot <- getThreadBufferSlot t;
bufferCap <- getSlotCap bufferFrameSlot;
case bufferCap of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xa) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xa) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr x && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return Nothing | _ \<Rightarrow> return Nothing
od)
 3. \<And>ta. \<lbrace>tcb_at' ta\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. thread_actions_isolatable idx (do cte <- getCTE (t + 2 ^ cte_level_bits * tcbIPCBufferSlot);
case cteCap cte of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xb) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xb) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr x && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return Nothing | _ \<Rightarrow> return Nothing
od)
 2. \<And>ta. \<lbrace>tcb_at' ta\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. thread_actions_isolatable idx (getCTE (t + 2 ^ cte_level_bits * tcbIPCBufferSlot))
 2. \<And>x xa. thread_actions_isolatable idx (case cteCap xa of capability.ArchObjectCap (arch_capability.PageCap True baseptr rights sz xb) \<Rightarrow> return Nothing | capability.ArchObjectCap (arch_capability.PageCap False baseptr rights sz xb) \<Rightarrow> do pBits <- return (pageBitsForSize sz);
if rights = VMReadWrite \<or> \<not> w \<and> rights = VMReadOnly then do ptr <- return (baseptr + PPtr (fromVPtr x && mask pBits));
haskell_assert (ptr \<noteq> 0) [];
return $ Just ptr
od else return Nothing
od | capability.ArchObjectCap _ \<Rightarrow> return Nothing | _ \<Rightarrow> return Nothing)
 3. \<And>x ta. \<lbrace>tcb_at' ta\<rbrace> getCTE (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace>
 4. \<And>ta. \<lbrace>tcb_at' ta\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x xa x32 x33 x34 x35. cteCap xa = capability.ArchObjectCap (arch_capability.PageCap False x32 x33 x34 x35) \<Longrightarrow> thread_actions_isolatable idx (if x33 = VMReadWrite \<or> \<not> w \<and> x33 = VMReadOnly then do y <- assert (x32 + (x && mask (pageBitsForSize x34)) \<noteq> 0);
return (Some (x32 + (x && mask (pageBitsForSize x34))))
od else return None)
 2. \<And>x ta. \<lbrace>tcb_at' ta\<rbrace> getCTE (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace>
 3. \<And>ta. \<lbrace>tcb_at' ta\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x xa x32 x33 x34 x35. \<lbrakk>cteCap xa = capability.ArchObjectCap (arch_capability.PageCap False x32 x33 x34 x35); x33 = VMReadWrite \<or> \<not> w \<and> x33 = VMReadOnly\<rbrakk> \<Longrightarrow> thread_actions_isolatable idx (do y <- assert (x32 + (x && mask (pageBitsForSize x34)) \<noteq> 0);
return (Some (x32 + (x && mask (pageBitsForSize x34))))
od)
 2. \<And>x xa x32 x33 x34 x35. \<lbrakk>cteCap xa = capability.ArchObjectCap (arch_capability.PageCap False x32 x33 x34 x35); \<not> (x33 = VMReadWrite \<or> \<not> w \<and> x33 = VMReadOnly)\<rbrakk> \<Longrightarrow> thread_actions_isolatable idx (return None)
 3. \<And>x ta. \<lbrace>tcb_at' ta\<rbrace> getCTE (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace>
 4. \<And>ta. \<lbrace>tcb_at' ta\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>x xa x32 x33 x34 x35. \<lbrakk>cteCap xa = capability.ArchObjectCap (arch_capability.PageCap False x32 x33 x34 x35); x33 = VMReadWrite \<or> \<not> w \<and> x33 = VMReadOnly\<rbrakk> \<Longrightarrow> thread_actions_isolatable idx (assert (x32 + (x && mask (pageBitsForSize x34)) \<noteq> 0))
 2. \<And>x xa x32 x33 x34 x35 xb. \<lbrakk>cteCap xa = capability.ArchObjectCap (arch_capability.PageCap False x32 x33 x34 x35); x33 = VMReadWrite \<or> \<not> w \<and> x33 = VMReadOnly\<rbrakk> \<Longrightarrow> thread_actions_isolatable idx (return (Some (x32 + (x && mask (pageBitsForSize x34)))))
 3. \<And>x xa x32 x33 x34 x35 t. \<lbrakk>cteCap xa = capability.ArchObjectCap (arch_capability.PageCap False x32 x33 x34 x35); x33 = VMReadWrite \<or> \<not> w \<and> x33 = VMReadOnly\<rbrakk> \<Longrightarrow> \<lbrace>tcb_at' t\<rbrace> assert (x32 + (x && mask (pageBitsForSize x34)) \<noteq> 0) \<lbrace>\<lambda>rv. tcb_at' t\<rbrace>
 4. \<And>x xa x32 x33 x34 x35. \<lbrakk>cteCap xa = capability.ArchObjectCap (arch_capability.PageCap False x32 x33 x34 x35); \<not> (x33 = VMReadWrite \<or> \<not> w \<and> x33 = VMReadOnly)\<rbrakk> \<Longrightarrow> thread_actions_isolatable idx (return None)
 5. \<And>x ta. \<lbrace>tcb_at' ta\<rbrace> getCTE (t + 2 ^ cte_level_bits * tcbIPCBufferSlot) \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace>
 6. \<And>ta. \<lbrace>tcb_at' ta\<rbrace> threadGet tcbIPCBuffer t \<lbrace>\<lambda>rv. tcb_at' ta\<rbrace> proof (prove)
goal:
No subgoals!