theory CSpace_I

lemma valid_mdb_ctes_init:
  "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte;
     caps_no_overlap' m (capRange cap); s \<turnstile>' cap;
     valid_objs' s; m = ctes_of s; cap \<noteq> NullCap;
     fresh_virt_cap_class (capClass cap) (ctes_of s);
     cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s) \<rbrakk> \<Longrightarrow>
  valid_mdb_ctes (m (p \<mapsto> CTE cap initMDBNode))" apply (simp add: valid_mdb_ctes_def) apply (rule conjI, rule valid_dlist_init, simp+) apply (subgoal_tac "p \<noteq> 0") prefer 2 apply (erule no_0_neq, clarsimp) apply (clarsimp simp: no_0_update) apply (rule conjI, rule mdb_chain_0_update_0, simp+) apply (rule conjI, rule valid_badges_0_update, simp+) apply (rule conjI, erule (1) caps_contained_no_overlap) apply (rule conjI, rule mdb_chunked_init, simp+) apply (rule conjI) apply (rule untyped_mdb_init, (simp add: valid_mdb_ctes_def)+) apply (rule conjI) apply (rule untyped_inc_init, (simp add: valid_mdb_ctes_def)+) apply (rule conjI) apply (erule(1) valid_nullcaps_init) apply (rule conjI, simp add: ut_revocable'_def initMDBNode_def) apply (rule conjI, erule(4) class_links_init) apply (rule conjI) apply (erule distinct_zombies_init, simp+) apply (erule valid_capAligned) apply clarsimp apply (case_tac ctea, clarsimp) apply (rule valid_capAligned, erule(1) ctes_of_valid_cap') apply (rule conjI) apply (erule (1) irq_control_init) apply (simp add: ran_def reply_masters_rvk_fb_def) apply (auto simp: initMDBNode_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_mdb_ctes m; m p = Some cte; no_mdb cte; caps_no_overlap' m (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s)\<rbrakk> \<Longrightarrow> valid_mdb_ctes (m(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s)\<rbrakk> \<Longrightarrow> valid_dlist ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> no_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chain_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_badges ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> caps_contained' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chunked ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s)\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chain_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_badges ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> caps_contained' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chunked ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chain_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_badges ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> caps_contained' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chunked ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s)\<rbrakk> \<Longrightarrow> p \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s)\<rbrakk> \<Longrightarrow> p \<noteq> 0
 2. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chain_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_badges ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> caps_contained' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chunked ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_dlist (ctes_of s) \<and> no_0 (ctes_of s) \<and> mdb_chain_0 (ctes_of s) \<and> valid_badges (ctes_of s) \<and> caps_contained' (ctes_of s) \<and> mdb_chunked (ctes_of s) \<and> untyped_mdb' (ctes_of s) \<and> untyped_inc' (ctes_of s) \<and> valid_nullcaps (ctes_of s) \<and> ut_revocable' (ctes_of s) \<and> class_links (ctes_of s) \<and> distinct_zombies (ctes_of s) \<and> irq_control (ctes_of s) \<and> reply_masters_rvk_fb (ctes_of s); ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0\<rbrakk> \<Longrightarrow> no_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chain_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_badges ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> caps_contained' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chunked ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> mdb_chain_0 ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_badges ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> caps_contained' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chunked ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> valid_badges ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> caps_contained' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chunked ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> caps_contained' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> mdb_chunked ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> mdb_chunked ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> untyped_mdb' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> untyped_inc' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> valid_nullcaps ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> ut_revocable' ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> class_links ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> distinct_zombies ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> capAligned cap
 2. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> \<forall>x cte. ctes_of s x = Some cte \<longrightarrow> capAligned (cteCap cte)
 3. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> \<forall>x cte. ctes_of s x = Some cte \<longrightarrow> capAligned (cteCap cte)
 2. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (2 subgoals):
 1. \<And>x ctea. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some ctea\<rbrakk> \<Longrightarrow> capAligned (cteCap ctea)
 2. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (2 subgoals):
 1. \<And>x x1 x2. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s); ctes_of s x = Some (CTE x1 x2)\<rbrakk> \<Longrightarrow> capAligned x1
 2. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) \<and> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> irq_control ((ctes_of s)(p \<mapsto> CTE cap initMDBNode))
 2. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); reply_masters_rvk_fb (ctes_of s)\<rbrakk> \<Longrightarrow> reply_masters_rvk_fb ((ctes_of s)(p \<mapsto> CTE cap initMDBNode)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ctes_of s p = Some cte; no_mdb cte; caps_no_overlap' (ctes_of s) (capRange cap); valid_cap' cap s; valid_objs' s; m = ctes_of s; cap \<noteq> capability.NullCap; fresh_virt_cap_class (capClass cap) (ctes_of s); cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s); p \<noteq> 0; valid_dlist (ctes_of s); no_0 (ctes_of s); mdb_chain_0 (ctes_of s); valid_badges (ctes_of s); caps_contained' (ctes_of s); mdb_chunked (ctes_of s); untyped_mdb' (ctes_of s); untyped_inc' (ctes_of s); valid_nullcaps (ctes_of s); ut_revocable' (ctes_of s); class_links (ctes_of s); distinct_zombies (ctes_of s); irq_control (ctes_of s); \<forall>cte. (\<exists>a. ctes_of s a = Some cte) \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte)\<rbrakk> \<Longrightarrow> \<forall>cte. (\<exists>a. (a = p \<longrightarrow> CTE cap initMDBNode = cte) \<and> (a \<noteq> p \<longrightarrow> ctes_of s a = Some cte)) \<longrightarrow> isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte) proof (prove)
goal:
No subgoals!