theory Ipc_C

lemma loadCapTransfer_ctReceiveDepth:
  "\<lbrace>\<top>\<rbrace> loadCapTransfer buffer \<lbrace>\<lambda>rv s. ctReceiveDepth rv < 2 ^ word_bits\<rbrace>" apply (simp add: loadCapTransfer_def capTransferFromWords_def) apply wp apply (rule_tac Q'="\<lambda>_ _. True" in hoare_post_eq) apply simp apply (simp only: word_bits_len_of[symmetric]) apply (subst unat_lt2p, simp) apply wpsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> loadCapTransfer buffer \<lbrace>\<lambda>rv s. ctReceiveDepth rv < 2 ^ word_bits\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> do w0 <- loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize);
w1 <- loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + word_of_nat wordSize);
w2 <- loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + 2 * word_of_nat wordSize);
return (CT w0 w1 (unat w2))
od \<lbrace>\<lambda>rv s. ctReceiveDepth rv < 2 ^ word_bits\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x w1. \<lbrace>?B2 x w1\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + 2 * word_of_nat wordSize) \<lbrace>\<lambda>w2 a. ctReceiveDepth (CT x w1 (unat w2)) < 2 ^ word_bits\<rbrace>
 2. \<And>x. \<lbrace>?B1 x\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + word_of_nat wordSize) \<lbrace>?B2 x\<rbrace>
 3. \<lbrace>?Q\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) \<lbrace>?B1\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>x w1. (\<lambda>w2 a. ctReceiveDepth (CT x w1 (unat w2)) < 2 ^ word_bits) = (\<lambda>_ _. True)
 2. \<And>x w1. \<lbrace>?B2 x w1\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + 2 * word_of_nat wordSize) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + word_of_nat wordSize) \<lbrace>?B2 x\<rbrace>
 4. \<lbrace>?Q\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) \<lbrace>?B1\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. (\<lambda>w2 a. unat w2 < 2 ^ word_bits) = (\<lambda>_ _. True)
 2. \<And>x w1. \<lbrace>?B2 x w1\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + 2 * word_of_nat wordSize) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + word_of_nat wordSize) \<lbrace>?B2 x\<rbrace>
 4. \<lbrace>?Q\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) \<lbrace>?B1\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. (\<lambda>w2 a. unat w2 < 2 ^ LENGTH(32)) = (\<lambda>_ _. True)
 2. \<And>x w1. \<lbrace>?B2 x w1\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + 2 * word_of_nat wordSize) \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>x. \<lbrace>?B1 x\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + word_of_nat wordSize) \<lbrace>?B2 x\<rbrace>
 4. \<lbrace>?Q\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) \<lbrace>?B1\<rbrace>
 5. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>x w1. \<lbrace>?B2 x w1\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + 2 * word_of_nat wordSize) \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>x. \<lbrace>?B1 x\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize + word_of_nat wordSize) \<lbrace>?B2 x\<rbrace>
 3. \<lbrace>?Q\<rbrace> loadWordUser (buffer + (msgMaxLength + msgMaxExtraCaps + 2) * word_of_nat wordSize) \<lbrace>?B1\<rbrace>
 4. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!