theory PageTableDuplicates

lemma setCTE_valid_duplicates'[wp]:
 "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
  setCTE p cte \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add:setCTE_def) apply (clarsimp simp: setObject_def split_def valid_def in_monad
                        projectKOs pspace_aligned'_def ps_clear_upd
                        objBits_def[symmetric] lookupAround2_char1
                 split: if_split_asm) apply (frule pspace_storable_class.updateObject_type[where v = cte,simplified]) apply (clarsimp simp:ObjectInstances_H.updateObject_cte assert_def bind_def
    alignCheck_def in_monad when_def alignError_def magnitudeCheck_def
    assert_opt_def return_def fail_def typeError_def
    split:if_splits option.splits Structures_H.kernel_object.splits) apply (erule valid_duplicates'_non_pd_pt_I[rotated 3],simp+)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> setObject p cte \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s''a obj'. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject cte ba p a (snd (lookupAround2 p (ksPSpace s))) s)\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (1 subgoal):
 1. \<And>s a ba s''a obj'. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject cte ba p a (snd (lookupAround2 p (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (12 subgoals):
 1. \<And>s a x6. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; p - a = tcbVTableSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = None; a && mask (objBits x6) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB (tcbVTable_update (\<lambda>_. cte) x6)))
 2. \<And>s a x6 x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; p - a = tcbVTableSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = Some x2; \<not> x2 - a < 2 ^ objBits x6; a && mask (objBits x6) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB (tcbVTable_update (\<lambda>_. cte) x6)))
 3. \<And>s a x6. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; p - a = tcbCTableSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = None; a && mask (objBits x6) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB (tcbCTable_update (\<lambda>_. cte) x6)))
 4. \<And>s a x6 x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; tcbCTableSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; p - a = tcbCTableSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = Some x2; \<not> x2 - a < 2 ^ objBits x6; a && mask (objBits x6) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB (tcbCTable_update (\<lambda>_. cte) x6)))
 5. \<And>s a x6. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; p - a = tcbReplySlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = None; a && mask (objBits x6) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB (tcbReply_update (\<lambda>_. cte) x6)))
 6. \<And>s a x6 x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; tcbReplySlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbReplySlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; p - a = tcbReplySlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = Some x2; \<not> x2 - a < 2 ^ objBits x6; a && mask (objBits x6) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB (tcbReply_update (\<lambda>_. cte) x6)))
 7. \<And>s a x6. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined; p - a = tcbCallerSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = None; a && mask (objBits x6) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB (tcbCaller_update (\<lambda>_. cte) x6)))
 8. \<And>s a x6 x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; tcbCallerSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbCallerSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; tcbCallerSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined; p - a = tcbCallerSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = Some x2; \<not> x2 - a < 2 ^ objBits x6; a && mask (objBits x6) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB (tcbCaller_update (\<lambda>_. cte) x6)))
 9. \<And>s a x6. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; tcbIPCBufferSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbCallerSlot << objBits undefined; p - a = tcbIPCBufferSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = None; a && mask (objBits x6) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) x6)))
 10. \<And>s a x6 x2. \<lbrakk>vs_valid_duplicates' (ksPSpace s); a \<le> p; ksPSpace s a = Some (KOTCB x6); \<forall>z. a < z \<and> z \<le> p \<longrightarrow> ksPSpace s z = None; tcbIPCBufferSlot << objBits undefined \<noteq> tcbVTableSlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbCTableSlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbReplySlot << objBits undefined; tcbIPCBufferSlot << objBits undefined \<noteq> tcbCallerSlot << objBits undefined; p - a = tcbIPCBufferSlot << objBits undefined; snd (lookupAround2 p (ksPSpace s)) = Some x2; \<not> x2 - a < 2 ^ objBits x6; a && mask (objBits x6) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> KOTCB (tcbIPCBufferFrame_update (\<lambda>_. cte) x6)))
A total of 12 subgoals... proof (prove)
goal:
No subgoals!