theory PageTableDuplicates

lemma set_ntfn_valid_duplicate' [wp]:
  "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace>
  setNotification ep v  \<lbrace>\<lambda>rv s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" apply (simp add:setNotification_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 = v,simplified]) apply (clarsimp simp:updateObject_default_def assert_def bind_def
    alignCheck_def in_monad when_def alignError_def magnitudeCheck_def
    assert_opt_def return_def fail_def split:if_splits option.splits) apply (rule_tac ko = ba in valid_duplicates'_non_pd_pt_I) apply simp+ apply (rule_tac ko = ba in valid_duplicates'_non_pd_pt_I) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> setNotification ep v \<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 ep v \<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> ep; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default v ba ep a (snd (lookupAround2 ep (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> ep; ksPSpace s a = Some ba; \<forall>z. a < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; (obj', s''a) \<in> fst (updateObject_default v ba ep a (snd (lookupAround2 ep (ksPSpace s))) s); koTypeOf obj' = koTypeOf ba\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(a \<mapsto> obj')) proof (prove)
goal (2 subgoals):
 1. \<And>s ba s''a a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = None; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(ep \<mapsto> KONotification v))
 2. \<And>s ba s''a x2 a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = Some x2; \<not> x2 - ep < 2 ^ objBits v; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(ep \<mapsto> KONotification v)) proof (prove)
goal (6 subgoals):
 1. \<And>s ba s''a a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = None; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> koTypeOf ba \<noteq> ArchT PDET
 2. \<And>s ba s''a a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = None; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> koTypeOf ba \<noteq> ArchT PTET
 3. \<And>s ba s''a a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = None; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 4. \<And>s ba s''a a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = None; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> ksPSpace s ep = Some ba
 5. \<And>s ba s''a a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = None; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> koTypeOf ba = koTypeOf (KONotification v)
 6. \<And>s ba s''a x2 a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = Some x2; \<not> x2 - ep < 2 ^ objBits v; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(ep \<mapsto> KONotification v)) proof (prove)
goal (1 subgoal):
 1. \<And>s ba s''a x2 a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = Some x2; \<not> x2 - ep < 2 ^ objBits v; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' ((ksPSpace s)(ep \<mapsto> KONotification v)) proof (prove)
goal (5 subgoals):
 1. \<And>s ba s''a x2 a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = Some x2; \<not> x2 - ep < 2 ^ objBits v; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> koTypeOf ba \<noteq> ArchT PDET
 2. \<And>s ba s''a x2 a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = Some x2; \<not> x2 - ep < 2 ^ objBits v; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> koTypeOf ba \<noteq> ArchT PTET
 3. \<And>s ba s''a x2 a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = Some x2; \<not> x2 - ep < 2 ^ objBits v; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> vs_valid_duplicates' (ksPSpace s)
 4. \<And>s ba s''a x2 a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = Some x2; \<not> x2 - ep < 2 ^ objBits v; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> ksPSpace s ep = Some ba
 5. \<And>s ba s''a x2 a. \<lbrakk>NotificationT = koTypeOf ba; vs_valid_duplicates' (ksPSpace s); ksPSpace s ep = Some ba; \<forall>z. ep < z \<and> z \<le> ep \<longrightarrow> ksPSpace s z = None; snd (lookupAround2 ep (ksPSpace s)) = Some x2; \<not> x2 - ep < 2 ^ objBits v; (a, s''a) \<in> fst (projectKO ba s); ep && mask (objBits v) = 0\<rbrakk> \<Longrightarrow> koTypeOf ba = koTypeOf (KONotification v) proof (prove)
goal:
No subgoals!