theory Dpolicy

lemma state_irqs_transform_rev:
  "\<lbrakk> einvs s; (x, a, y) \<in> cdl_state_irqs_to_policy aag (transform s) \<rbrakk> \<Longrightarrow>
   (x, a, y) \<in> state_irqs_to_policy aag s" apply (erule cdl_state_irqs_to_policy_aux.induct) apply (rule_tac P="is_thread_state_cap cap" in case_split) apply (clarsimp simp:is_thread_state_cap_def split:cdl_cap.splits) apply (rule_tac P="is_bound_ntfn_cap cap" in case_split) apply (clarsimp simp:is_bound_ntfn_cap_def split:cdl_cap.splits) apply (rule_tac P="\<not> is_real_cap cap" in case_split) apply (clarsimp simp:is_real_cap_def split:cdl_cap.splits) apply (rule_tac P="is_null_cap cap" in case_split) apply (clarsimp simp:is_null_cap_def split:cdl_cap.splits) apply (frule caps_of_state_transform_opt_cap_rev, simp+) apply clarsimp apply (subst fst_transform_cslot_ptr[symmetric]) apply (rule_tac cap=cap' in sita_controlled) apply simp apply (simp add:cap_irqs_controlled_transform) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>einvs s; (x, a, y) \<in> cdl_state_irqs_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (x, a, y) \<in> state_irqs_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (2 subgoals):
 1. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s
 2. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (2 subgoals):
 1. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap; is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s
 2. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (2 subgoals):
 1. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> is_real_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s
 2. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> \<not> is_real_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> \<not> is_real_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (2 subgoals):
 1. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> \<not> is_real_cap cap; is_null_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s
 2. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> \<not> is_real_cap cap; \<not> is_null_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>ref cap irq. \<lbrakk>einvs s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; \<not> \<not> is_real_cap cap; \<not> is_null_cap cap\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>ref cap irq. \<lbrakk>invs s \<and> valid_list s \<and> valid_sched s; opt_cap ref (transform s) = Some cap; irq \<in> cdl_cap_irqs_controlled cap; \<not> is_thread_state_cap cap; \<not> is_bound_ntfn_cap cap; is_real_cap cap; \<not> is_null_cap cap; \<exists>cap'. cap = transform_cap cap' \<and> (\<exists>a b. ref = transform_cslot_ptr (a, b) \<and> caps_of_state s (a, b) = Some cap')\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>a b irq cap' aa ba. \<lbrakk>opt_cap (transform_cslot_ptr (aa, ba)) (transform s) = Some (transform_cap cap'); irq \<in> cdl_cap_irqs_controlled (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s (aa, ba) = Some cap'\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst (transform_cslot_ptr (aa, ba))), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (1 subgoal):
 1. \<And>a b irq cap' aa ba. \<lbrakk>opt_cap (transform_cslot_ptr (aa, ba)) (transform s) = Some (transform_cap cap'); irq \<in> cdl_cap_irqs_controlled (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s (aa, ba) = Some cap'\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (fst (aa, ba)), Control, pasIRQAbs aag irq) \<in> state_irqs_to_policy aag s proof (prove)
goal (2 subgoals):
 1. \<And>a b irq cap' aa ba. \<lbrakk>opt_cap (transform_cslot_ptr (aa, ba)) (transform s) = Some (transform_cap cap'); irq \<in> cdl_cap_irqs_controlled (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s (aa, ba) = Some cap'\<rbrakk> \<Longrightarrow> caps_of_state s (aa, ba) = Some cap'
 2. \<And>a b irq cap' aa ba. \<lbrakk>opt_cap (transform_cslot_ptr (aa, ba)) (transform s) = Some (transform_cap cap'); irq \<in> cdl_cap_irqs_controlled (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s (aa, ba) = Some cap'\<rbrakk> \<Longrightarrow> irq \<in> cap_irqs_controlled cap' proof (prove)
goal (1 subgoal):
 1. \<And>a b irq cap' aa ba. \<lbrakk>opt_cap (transform_cslot_ptr (aa, ba)) (transform s) = Some (transform_cap cap'); irq \<in> cdl_cap_irqs_controlled (transform_cap cap'); \<not> is_thread_state_cap (transform_cap cap'); is_real_cap (transform_cap cap'); \<not> is_null_cap (transform_cap cap'); invs s; valid_list s; valid_sched s; (a, b) = transform_cslot_ptr (aa, ba); caps_of_state s (aa, ba) = Some cap'\<rbrakk> \<Longrightarrow> irq \<in> cap_irqs_controlled cap' proof (prove)
goal:
No subgoals!