theory Finalise_R

lemma caps_contained_n:
  "caps_contained' n" using valid apply (clarsimp simp: valid_mdb_ctes_def caps_contained'_def) apply (drule n_cap)+ apply (clarsimp split: if_split_asm) apply (erule disjE, clarsimp) apply clarsimp apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. caps_contained' n proof (prove)
using this:
valid_mdb_ctes m

goal (1 subgoal):
 1. caps_contained' n proof (prove)
goal (1 subgoal):
 1. \<And>p p' c na c' n' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; n p = Some (CTE c na); n p' = Some (CTE c' n'); \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c n c' n' x. \<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; \<exists>cap' node'. m p = Some (CTE cap' node') \<and> (if p = slot then c = capability.NullCap else cap' = c); \<exists>cap' node'. m p' = Some (CTE cap' node') \<and> (if p' = slot then c' = capability.NullCap else cap' = c')\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c' x cap' node'. \<lbrakk>m p' = Some (CTE c' node'); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p' \<noteq> slot; p = slot \<longrightarrow> (\<exists>node'. m slot = Some (CTE cap' node')) \<and> c = capability.NullCap; p = slot \<or> (\<exists>node'. m p = Some (CTE cap' node')) \<and> cap' = c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c' x cap' node'. \<lbrakk>m p' = Some (CTE c' node'); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p' \<noteq> slot; p = slot \<longrightarrow> (\<exists>node'. m slot = Some (CTE cap' node')) \<and> c = capability.NullCap; (\<exists>node'. m p = Some (CTE cap' node')) \<and> cap' = c\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal (1 subgoal):
 1. \<And>p p' c c' x node' node'a. \<lbrakk>m p' = Some (CTE c' node'); valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; \<forall>p p' c. (\<exists>n. m p = Some (CTE c n)) \<longrightarrow> (\<forall>c'. (\<exists>n'. m p' = Some (CTE c' n')) \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> capRange c' \<subseteq> untypedRange c); mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; reply_masters_rvk_fb m; \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; x \<in> capRange c'; p' \<noteq> slot; p = slot \<longrightarrow> (\<exists>node'. m slot = Some (CTE c node')) \<and> c = capability.NullCap; m p = Some (CTE c node'a)\<rbrakk> \<Longrightarrow> x \<in> untypedRange c proof (prove)
goal:
No subgoals!