theory Dpolicy

lemma cdl_transferable_implies_transferable:
  "\<lbrakk> einvs s; cdt s (ptr, slot) = Some (pptr, pslot);
     cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ptr, slot)) (transform s)) \<rbrakk>
       \<Longrightarrow> is_transferable_in (ptr, slot) s" apply clarsimp apply (frule invs_mdb_cte, drule mdb_cte_at_rewrite, clarsimp simp: mdb_cte_at_def) apply ((drule spec)+, erule(1) impE, clarsimp) apply (erule cdl_cap_is_transferable.cases) apply (erule contrapos_pp[where Q="opt_cap _ _ = _"], clarsimp) apply (rule exI) apply (rule caps_of_state_transform_opt_cap) apply assumption apply fastforce apply (blast dest: idle_thread_null_cap) apply (fastforce dest: cdl_transform_null_cap[rotated]) apply (fastforce simp: is_transferable.simps dest: cdl_transform_reply_cap[rotated]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; cdt s (ptr, slot) = Some (pptr, pslot); cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ptr, slot)) (transform s))\<rbrakk> \<Longrightarrow> is_transferable_in (ptr, slot) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ptr, slot)) (transform s)); invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> is_transferable_in (ptr, slot) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ptr, slot)) (transform s)); invs s; valid_list s; valid_sched s; \<forall>a b aa ba. cdt s (aa, ba) = Some (a, b) \<longrightarrow> (\<exists>c. caps_of_state s (a, b) = Some c \<and> cap.NullCap \<noteq> c) \<and> (\<exists>c. caps_of_state s (aa, ba) = Some c \<and> cap.NullCap \<noteq> c)\<rbrakk> \<Longrightarrow> is_transferable_in (ptr, slot) s proof (prove)
goal (1 subgoal):
 1. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); cdl_cap_is_transferable (opt_cap (transform_cslot_ptr (ptr, slot)) (transform s)); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca\<rbrakk> \<Longrightarrow> is_transferable_cap ca proof (prove)
goal (3 subgoals):
 1. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = None\<rbrakk> \<Longrightarrow> is_transferable_cap ca
 2. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> is_transferable_cap ca
 3. \<And>c ca t R. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R)\<rbrakk> \<Longrightarrow> is_transferable_cap ca proof (prove)
goal (3 subgoals):
 1. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; \<not> is_transferable_cap ca\<rbrakk> \<Longrightarrow> \<exists>y. opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some y
 2. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> is_transferable_cap ca
 3. \<And>c ca t R. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R)\<rbrakk> \<Longrightarrow> is_transferable_cap ca proof (prove)
goal (3 subgoals):
 1. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; \<not> is_transferable_cap ca\<rbrakk> \<Longrightarrow> opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (?y34 c ca)
 2. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> is_transferable_cap ca
 3. \<And>c ca t R. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R)\<rbrakk> \<Longrightarrow> is_transferable_cap ca proof (prove)
goal (5 subgoals):
 1. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; \<not> is_transferable_cap ca\<rbrakk> \<Longrightarrow> caps_of_state s (ptr, slot) = Some (?cap36 c ca)
 2. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; \<not> is_transferable_cap ca\<rbrakk> \<Longrightarrow> valid_etcbs s
 3. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; \<not> is_transferable_cap ca\<rbrakk> \<Longrightarrow> fst (ptr, slot) \<noteq> idle_thread s
 4. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> is_transferable_cap ca
 5. \<And>c ca t R. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R)\<rbrakk> \<Longrightarrow> is_transferable_cap ca proof (prove)
goal (4 subgoals):
 1. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; \<not> is_transferable_cap ca\<rbrakk> \<Longrightarrow> valid_etcbs s
 2. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; \<not> is_transferable_cap ca\<rbrakk> \<Longrightarrow> fst (ptr, slot) \<noteq> idle_thread s
 3. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> is_transferable_cap ca
 4. \<And>c ca t R. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R)\<rbrakk> \<Longrightarrow> is_transferable_cap ca proof (prove)
goal (3 subgoals):
 1. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; \<not> is_transferable_cap ca\<rbrakk> \<Longrightarrow> fst (ptr, slot) \<noteq> idle_thread s
 2. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> is_transferable_cap ca
 3. \<And>c ca t R. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R)\<rbrakk> \<Longrightarrow> is_transferable_cap ca proof (prove)
goal (2 subgoals):
 1. \<And>c ca. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> is_transferable_cap ca
 2. \<And>c ca t R. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R)\<rbrakk> \<Longrightarrow> is_transferable_cap ca proof (prove)
goal (1 subgoal):
 1. \<And>c ca t R. \<lbrakk>cdt s (ptr, slot) = Some (pptr, pslot); invs s; valid_list s; valid_sched s; caps_of_state s (pptr, pslot) = Some c; cap.NullCap \<noteq> c; caps_of_state s (ptr, slot) = Some ca; cap.NullCap \<noteq> ca; opt_cap (transform_cslot_ptr (ptr, slot)) (transform s) = Some (cdl_cap.ReplyCap t R)\<rbrakk> \<Longrightarrow> is_transferable_cap ca proof (prove)
goal:
No subgoals!