theory Finalise_R

lemma class_links_n: "class_links n" using valid slot apply (clarsimp simp: valid_mdb_ctes_def class_links_def) apply (case_tac cte, case_tac cte') apply (drule n_nextD) apply (clarsimp simp: split: if_split_asm) apply (simp add: no_0_n) apply (drule n_cap)+ apply clarsimp apply (frule spec[where x=slot],
          drule spec[where x="mdbNext s_node"],
          simp, simp add: m_slot_next) apply (drule spec[where x="mdbPrev s_node"],
          drule spec[where x=slot], simp) apply (drule n_cap)+ apply clarsimp apply (fastforce split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. class_links n proof (prove)
using this:
valid_mdb_ctes m
m slot = Some (CTE s_cap s_node)

goal (1 subgoal):
 1. class_links n proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte'. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some cte; n p' = Some cte'; n \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte' x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some cte; n p' = Some cte'; n \<turnstile> p \<leadsto> p'; cte = CTE x1 x2; cte' = CTE x1a x2a\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (1 subgoal):
 1. \<And>p p' cte cte' x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some cte; n p' = Some cte'; cte = CTE x1 x2; cte' = CTE x1a x2a; if p = slot then p' = 0 else if p = mdbPrev s_node then m \<turnstile> p \<leadsto> slot \<and> p' = mdbNext s_node else m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass (cteCap cte) = capClass (cteCap cte') proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n slot = Some (CTE x1 x2); n 0 = Some (CTE x1a x2a)\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a
 2. \<And>x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n (mdbPrev s_node) = Some (CTE x1 x2); n (mdbNext s_node) = Some (CTE x1a x2a); mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a
 3. \<And>p p' x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some (CTE x1 x2); n p' = Some (CTE x1a x2a); p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n (mdbPrev s_node) = Some (CTE x1 x2); n (mdbNext s_node) = Some (CTE x1a x2a); mdbPrev s_node \<noteq> 0\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a
 2. \<And>p p' x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some (CTE x1 x2); n p' = Some (CTE x1a x2a); p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; mdbPrev s_node \<noteq> 0; \<exists>cap' node'. m (mdbPrev s_node) = Some (CTE cap' node') \<and> (if mdbPrev s_node = slot then x1 = capability.NullCap else cap' = x1); \<exists>cap' node'. m (mdbNext s_node) = Some (CTE cap' node') \<and> (if mdbNext s_node = slot then x1a = capability.NullCap else cap' = x1a)\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a
 2. \<And>p p' x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some (CTE x1 x2); n p' = Some (CTE x1a x2a); p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (2 subgoals):
 1. \<And>x1 x1a node' node'a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; mdbPrev s_node \<noteq> 0; m (mdbPrev s_node) = Some (CTE x1 node'); m (mdbNext s_node) = Some (CTE x1a node'a)\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a
 2. \<And>p p' x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some (CTE x1 x2); n p' = Some (CTE x1a x2a); p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (2 subgoals):
 1. \<And>x1 x1a node' node'a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; mdbPrev s_node \<noteq> 0; m (mdbPrev s_node) = Some (CTE x1 node'); m (mdbNext s_node) = Some (CTE x1a node'a); capClass s_cap = capClass x1a\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a
 2. \<And>p p' x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some (CTE x1 x2); n p' = Some (CTE x1a x2a); p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some (CTE x1 x2); n p' = Some (CTE x1a x2a); p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> p'\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x2 x1a x2a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> p'; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then x1 = capability.NullCap else cap' = x1); \<exists>cap' node'. m p' = Some (CTE cap' node') \<and> (if p' = slot then x1a = capability.NullCap else cap' = x1a)\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal (1 subgoal):
 1. \<And>p p' x1 x1a node' cap' node'a. \<lbrakk>m slot = Some (CTE s_cap s_node); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; \<forall>p p' cte. m p = Some cte \<longrightarrow> (\<forall>cte'. m p' = Some cte' \<longrightarrow> m \<turnstile> p \<leadsto> p' \<longrightarrow> capClass (cteCap cte) = capClass (cteCap cte')); distinct_zombies m; irq_control m; reply_masters_rvk_fb m; p \<noteq> slot; p \<noteq> mdbPrev s_node; m \<turnstile> p \<leadsto> p'; m p = Some (CTE x1 node'); if p' = slot then x1a = capability.NullCap else cap' = x1a; m p' = Some (CTE cap' node'a)\<rbrakk> \<Longrightarrow> capClass x1 = capClass x1a proof (prove)
goal:
No subgoals!