theory IpcCancel_R

lemma reply_no_descendants_mdbNext_null:
  assumes descs: "descendants_of (t, tcb_cnode_index 2) (cdt s) = {}"
  and        sr: "(s, s') \<in> state_relation"
  and      invs: "valid_reply_caps s" "valid_reply_masters s"
                 "valid_objs s" "valid_mdb s" "valid_mdb' s'" "pspace_aligned' s'"
                 "pspace_distinct' s'"
  and       tcb: "st_tcb_at (Not \<circ> halted) t s"
  and       cte: "ctes_of s' (t + 2*2^cte_level_bits) = Some cte"
  shows          "mdbNext (cteMDBNode cte) = nullPointer" proof - from invs st_tcb_at_reply_cap_valid[OF tcb] have "cte_wp_at (is_master_reply_cap_to t) (t, tcb_cnode_index 2) s" by (fastforce simp: cte_wp_at_caps_of_state is_cap_simps is_master_reply_cap_to_def) hence "\<exists>r. cteCap cte = capability.ReplyCap t True r" using invs sr by (fastforce simp: cte_wp_at_master_reply_cap_to_ex_rights
                        cte_wp_at_ctes_of cte cte_map_def tcb_cnode_index_def
                  dest: pspace_relation_cte_wp_at state_relation_pspace_relation) hence class_link:
    "\<forall>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte' \<longrightarrow>
            capClass (cteCap cte') = ReplyClass t" using invs apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def) apply (drule class_linksD[where m="ctes_of s'", OF cte]) apply (simp add: mdb_next_unfold cte) apply assumption apply simp done from invs tcb descs have "\<forall>ptr m g.
      cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s \<longrightarrow> ptr = (t, tcb_cnode_index 2)" apply (intro allI impI) apply (case_tac m) apply (fastforce simp: invs_def valid_state_def valid_reply_masters_def
                            cte_wp_at_master_reply_cap_to_ex_rights) apply (fastforce simp: has_reply_cap_def cte_wp_at_reply_cap_to_ex_rights
                     dest: reply_master_no_descendants_no_reply elim: st_tcb_at_tcb_at) done hence "\<forall>ptr m mdb r.
      ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb) \<longrightarrow> ptr = t + 2*2^cte_level_bits" using sr invs apply (intro allI impI) apply (drule(2) pspace_relation_cte_wp_atI
                    [OF state_relation_pspace_relation]) apply (elim exE, case_tac c, simp_all del: split_paired_All) apply (elim allE, erule impE, fastforce) apply (clarsimp simp: cte_map_def tcb_cnode_index_def) done hence class_unique:
    "\<forall>ptr cte'. ctes_of s' ptr = Some cte' \<longrightarrow>
                capClass (cteCap cte') = ReplyClass t \<longrightarrow>
                ptr = t + 2*2^cte_level_bits" apply (intro allI impI) apply (case_tac cte', rename_tac cap node, case_tac cap, simp_all) apply (rename_tac arch_capability) apply (case_tac arch_capability, simp_all) done from invs have no_null: "ctes_of s' nullPointer = None" by (clarsimp simp: no_0_def nullPointer_def valid_mdb'_def valid_mdb_ctes_def) from invs cte have no_loop: "mdbNext (cteMDBNode cte) \<noteq> t + 2*2^cte_level_bits" by (fastforce simp: mdb_next_rel_def mdb_next_def
                       valid_mdb'_def
                 dest: valid_mdb_no_loops no_loops_direct_simp) from invs cte have
    "mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow>
     (\<exists>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte')" by (fastforce simp: valid_mdb'_def valid_mdb_ctes_def nullPointer_def
                 elim: valid_dlistEn) hence
    "mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow>
     mdbNext (cteMDBNode cte) = t + 2*2^cte_level_bits" using class_link class_unique by clarsimp thus ?thesis by (simp add: no_loop) qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (state)
goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (chain)
picking this:
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'
\<lbrakk>valid_objs s; True; \<not> (Not \<circ> halted) Structures_A.thread_state.Inactive \<and> \<not> (Not \<circ> halted) Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. is_master_reply_cap cap \<and> obj_ref_of cap = t) (t, tcb_cnode_index 2) s proof (prove)
using this:
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'
\<lbrakk>valid_objs s; True; \<not> (Not \<circ> halted) Structures_A.thread_state.Inactive \<and> \<not> (Not \<circ> halted) Structures_A.thread_state.IdleThreadState\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. is_master_reply_cap cap \<and> obj_ref_of cap = t) (t, tcb_cnode_index 2) s

goal (1 subgoal):
 1. cte_wp_at (is_master_reply_cap_to t) (t, tcb_cnode_index 2) s proof (state)
this:
cte_wp_at (is_master_reply_cap_to t) (t, tcb_cnode_index 2) s

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (prove)
using this:
cte_wp_at (is_master_reply_cap_to t) (t, tcb_cnode_index 2) s

goal (1 subgoal):
 1. \<exists>r. cteCap cte = capability.ReplyCap t True r proof (prove)
using this:
cte_wp_at (is_master_reply_cap_to t) (t, tcb_cnode_index 2) s
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'
(s, s') \<in> state_relation

goal (1 subgoal):
 1. \<exists>r. cteCap cte = capability.ReplyCap t True r proof (state)
this:
\<exists>r. cteCap cte = capability.ReplyCap t True r

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (prove)
using this:
\<exists>r. cteCap cte = capability.ReplyCap t True r

goal (1 subgoal):
 1. \<forall>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte' \<longrightarrow> capClass (cteCap cte') = ReplyClass t proof (prove)
using this:
\<exists>r. cteCap cte = capability.ReplyCap t True r
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'

goal (1 subgoal):
 1. \<forall>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte' \<longrightarrow> capClass (cteCap cte') = ReplyClass t proof (prove)
goal (1 subgoal):
 1. \<And>r cte'. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; pspace_aligned' s'; pspace_distinct' s'; cteCap cte = capability.ReplyCap t True r; 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'); ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte'\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = ReplyClass t proof (prove)
goal (3 subgoals):
 1. \<And>r cte'. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; pspace_aligned' s'; pspace_distinct' s'; cteCap cte = capability.ReplyCap t True r; 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> ctes_of s' \<turnstile> t + 2 * 2 ^ cte_level_bits \<leadsto> mdbNext (cteMDBNode cte)
 2. \<And>r cte'. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; pspace_aligned' s'; pspace_distinct' s'; cteCap cte = capability.ReplyCap t True r; 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')
 3. \<And>r cte'. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; pspace_aligned' s'; pspace_distinct' s'; cteCap cte = capability.ReplyCap t True r; 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'); capClass (cteCap cte) = capClass (cteCap cte')\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = ReplyClass t proof (prove)
goal (2 subgoals):
 1. \<And>r cte'. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; pspace_aligned' s'; pspace_distinct' s'; cteCap cte = capability.ReplyCap t True r; 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')
 2. \<And>r cte'. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; pspace_aligned' s'; pspace_distinct' s'; cteCap cte = capability.ReplyCap t True r; 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'); capClass (cteCap cte) = capClass (cteCap cte')\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = ReplyClass t proof (prove)
goal (1 subgoal):
 1. \<And>r cte'. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; pspace_aligned' s'; pspace_distinct' s'; cteCap cte = capability.ReplyCap t True r; 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'); capClass (cteCap cte) = capClass (cteCap cte')\<rbrakk> \<Longrightarrow> capClass (cteCap cte') = ReplyClass t proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte' \<longrightarrow> capClass (cteCap cte') = ReplyClass t

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (chain)
picking this:
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'
st_tcb_at (Not \<circ> halted) t s
descendants_of (t, tcb_cnode_index 2) (cdt s) = {} proof (prove)
using this:
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'
st_tcb_at (Not \<circ> halted) t s
descendants_of (t, tcb_cnode_index 2) (cdt s) = {}

goal (1 subgoal):
 1. \<forall>ptr m g. cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s \<longrightarrow> ptr = (t, tcb_cnode_index 2) proof (prove)
goal (1 subgoal):
 1. \<And>ptr m g. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; st_tcb_at (Not \<circ> halted) t s; descendants_of (t, tcb_cnode_index 2) (cdt s) = {}; cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s\<rbrakk> \<Longrightarrow> ptr = (t, tcb_cnode_index 2) proof (prove)
goal (2 subgoals):
 1. \<And>ptr m g. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; st_tcb_at (Not \<circ> halted) t s; descendants_of (t, tcb_cnode_index 2) (cdt s) = {}; cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s; m\<rbrakk> \<Longrightarrow> ptr = (t, tcb_cnode_index 2)
 2. \<And>ptr m g. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; st_tcb_at (Not \<circ> halted) t s; descendants_of (t, tcb_cnode_index 2) (cdt s) = {}; cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s; \<not> m\<rbrakk> \<Longrightarrow> ptr = (t, tcb_cnode_index 2) proof (prove)
goal (1 subgoal):
 1. \<And>ptr m g. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; st_tcb_at (Not \<circ> halted) t s; descendants_of (t, tcb_cnode_index 2) (cdt s) = {}; cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s; \<not> m\<rbrakk> \<Longrightarrow> ptr = (t, tcb_cnode_index 2) proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>ptr m g. cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s \<longrightarrow> ptr = (t, tcb_cnode_index 2)

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (prove)
using this:
\<forall>ptr m g. cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s \<longrightarrow> ptr = (t, tcb_cnode_index 2)

goal (1 subgoal):
 1. \<forall>ptr m mdb r. ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb) \<longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits proof (prove)
using this:
\<forall>ptr m g. cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s \<longrightarrow> ptr = (t, tcb_cnode_index 2)
(s, s') \<in> state_relation
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'

goal (1 subgoal):
 1. \<forall>ptr m mdb r. ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb) \<longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>ptr m mdb r. \<lbrakk>\<forall>ptr m g. cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s \<longrightarrow> ptr = (t, tcb_cnode_index 2); (s, s') \<in> state_relation; valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb)\<rbrakk> \<Longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>ptr m mdb r. \<lbrakk>\<forall>ptr m g. cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s \<longrightarrow> ptr = (t, tcb_cnode_index 2); valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb); \<exists>c slot. cte_wp_at ((=) c) slot s \<and> cap_relation c (cteCap (CTE (capability.ReplyCap t m r) mdb)) \<and> ptr = cte_map slot\<rbrakk> \<Longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>m mdb c slot x53. \<lbrakk>\<forall>ptr. (\<exists>m g. cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s) \<longrightarrow> ptr = (t, tcb_cnode_index 2); valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; ctes_of s' (cte_map slot) = Some (CTE (capability.ReplyCap t m (AllowGrant \<in> x53)) mdb); cte_wp_at ((=) (cap.ReplyCap t m x53)) slot s; c = cap.ReplyCap t m x53\<rbrakk> \<Longrightarrow> cte_map slot = t + 2 * 2 ^ cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>m mdb c slot x53. \<lbrakk>valid_reply_caps s; valid_reply_masters s; valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; pspace_distinct' s'; ctes_of s' (cte_map slot) = Some (CTE (capability.ReplyCap t m (AllowGrant \<in> x53)) mdb); cte_wp_at ((=) (cap.ReplyCap t m x53)) slot s; c = cap.ReplyCap t m x53; slot = (t, tcb_cnode_index 2)\<rbrakk> \<Longrightarrow> cte_map slot = t + 2 * 2 ^ cte_level_bits proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>ptr m mdb r. ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb) \<longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (prove)
using this:
\<forall>ptr m mdb r. ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb) \<longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits

goal (1 subgoal):
 1. \<forall>ptr cte'. ctes_of s' ptr = Some cte' \<longrightarrow> capClass (cteCap cte') = ReplyClass t \<longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>ptr cte'. \<lbrakk>\<forall>ptr m mdb r. ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb) \<longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits; ctes_of s' ptr = Some cte'; capClass (cteCap cte') = ReplyClass t\<rbrakk> \<Longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>ptr cte' cap node x8. \<lbrakk>\<forall>ptr. (\<exists>m mdb r. ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb)) \<longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits; ctes_of s' ptr = Some (CTE (capability.ArchObjectCap x8) node); acapClass x8 = ReplyClass t; cte' = CTE (capability.ArchObjectCap x8) node; cap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits proof (prove)
goal (1 subgoal):
 1. \<And>ptr cte' cap node arch_capability. \<lbrakk>\<forall>ptr. (\<exists>m mdb r. ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb)) \<longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits; ctes_of s' ptr = Some (CTE (capability.ArchObjectCap arch_capability) node); acapClass arch_capability = ReplyClass t; cte' = CTE (capability.ArchObjectCap arch_capability) node; cap = capability.ArchObjectCap arch_capability\<rbrakk> \<Longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits proof (prove)
goal:
No subgoals! proof (state)
this:
\<forall>ptr cte'. ctes_of s' ptr = Some cte' \<longrightarrow> capClass (cteCap cte') = ReplyClass t \<longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (chain)
picking this:
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s' proof (prove)
using this:
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'

goal (1 subgoal):
 1. ctes_of s' nullPointer = None proof (state)
this:
ctes_of s' nullPointer = None

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (chain)
picking this:
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'
ctes_of s' (t + 2 * 2 ^ cte_level_bits) = Some cte proof (prove)
using this:
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'
ctes_of s' (t + 2 * 2 ^ cte_level_bits) = Some cte

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> t + 2 * 2 ^ cte_level_bits proof (state)
this:
mdbNext (cteMDBNode cte) \<noteq> t + 2 * 2 ^ cte_level_bits

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (chain)
picking this:
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'
ctes_of s' (t + 2 * 2 ^ cte_level_bits) = Some cte proof (prove)
using this:
valid_reply_caps s
valid_reply_masters s
valid_objs s
valid_mdb s
valid_mdb' s'
pspace_aligned' s'
pspace_distinct' s'
ctes_of s' (t + 2 * 2 ^ cte_level_bits) = Some cte

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> (\<exists>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte') proof (state)
this:
mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> (\<exists>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte')

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (prove)
using this:
mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> (\<exists>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte')

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> mdbNext (cteMDBNode cte) = t + 2 * 2 ^ cte_level_bits proof (prove)
using this:
mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> (\<exists>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte')
\<forall>cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte' \<longrightarrow> capClass (cteCap cte') = ReplyClass t
\<forall>ptr cte'. ctes_of s' ptr = Some cte' \<longrightarrow> capClass (cteCap cte') = ReplyClass t \<longrightarrow> ptr = t + 2 * 2 ^ cte_level_bits

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> mdbNext (cteMDBNode cte) = t + 2 * 2 ^ cte_level_bits proof (state)
this:
mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> mdbNext (cteMDBNode cte) = t + 2 * 2 ^ cte_level_bits

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (prove)
using this:
mdbNext (cteMDBNode cte) \<noteq> nullPointer \<longrightarrow> mdbNext (cteMDBNode cte) = t + 2 * 2 ^ cte_level_bits

goal (1 subgoal):
 1. mdbNext (cteMDBNode cte) = nullPointer proof (state)
this:
mdbNext (cteMDBNode cte) = nullPointer

goal:
No subgoals!