theory Dpolicy

lemma pas_refined_transform:
  "einvs s \<Longrightarrow> pas_refined aag s = pcs_refined aag (transform s)" apply (clarsimp simp:pcs_refined_def pas_refined_def irq_map_wellformed_transform tcb_domain_map_wellformed_transform) apply safe apply (rule subsetD, simp) apply (clarsimp simp:auth_graph_map_mem) apply (rule_tac x="x'" in exI, clarsimp, rule_tac x="y'" in exI, clarsimp) apply (clarsimp simp:state_objs_transform_rev) apply (rule_tac A="state_asids_to_policy aag s" in subsetD, simp) apply (clarsimp simp:state_asids_transform_rev[simplified]) apply (rule_tac A="state_irqs_to_policy aag s" in subsetD, simp) apply (clarsimp simp:state_irqs_transform_rev) apply (rule subsetD, simp) apply (clarsimp simp:auth_graph_map_mem) apply (rule_tac x="x'" in exI, clarsimp, rule_tac x="y'" in exI, clarsimp) apply (clarsimp simp:state_objs_transform) apply (rule_tac A="cdl_state_asids_to_policy aag (transform s)" in subsetD, simp) apply (clarsimp simp:state_asids_transform) apply (rule_tac A="cdl_state_irqs_to_policy aag (transform s)" in subsetD, simp) apply (clarsimp simp:state_irqs_transform) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. einvs s \<Longrightarrow> pas_refined aag s = pcs_refined aag (transform s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; valid_list s; valid_sched s\<rbrakk> \<Longrightarrow> (pas_wellformed aag \<and> cdl_irq_map_wellformed aag (transform s) \<and> cdl_tcb_domain_map_wellformed aag (transform s) \<and> state_objs_in_policy aag s \<and> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag \<and> state_irqs_to_policy aag s \<subseteq> pasPolicy aag) = (pas_wellformed aag \<and> cdl_irq_map_wellformed aag (transform s) \<and> cdl_tcb_domain_map_wellformed aag (transform s) \<and> auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag \<and> cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag \<and> cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag) proof (prove)
goal (6 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s))\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_asids_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_irqs_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 4. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 5. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 6. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (6 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s))\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_asids_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_irqs_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 4. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 5. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 6. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (6 subgoals):
 1. \<And>aa x' y'. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (x', aa, y') \<in> cdl_state_objs_to_policy (transform s)\<rbrakk> \<Longrightarrow> \<exists>x'a. pasObjectAbs aag x' = pasObjectAbs aag x'a \<and> (\<exists>y'a. pasObjectAbs aag y' = pasObjectAbs aag y'a \<and> (x'a, aa, y'a) \<in> state_objs_to_policy s)
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_asids_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_irqs_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 4. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 5. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 6. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (6 subgoals):
 1. \<And>aa x' y'. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (x', aa, y') \<in> cdl_state_objs_to_policy (transform s)\<rbrakk> \<Longrightarrow> (x', aa, y') \<in> state_objs_to_policy s
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_asids_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_irqs_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 4. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 5. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 6. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (5 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_asids_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_irqs_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 4. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 5. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (5 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_asids_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_asids_to_policy aag s
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_irqs_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 4. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 5. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (4 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_irqs_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 4. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (4 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); state_objs_in_policy aag s; state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s) \<subseteq> pasPolicy aag; state_irqs_to_policy aag s \<subseteq> pasPolicy aag; (a, aa, b) \<in> cdl_state_irqs_to_policy aag (transform s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> state_irqs_to_policy aag s
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 4. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (state_objs_to_policy s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s))
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>aa x' y'. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (x', aa, y') \<in> state_objs_to_policy s\<rbrakk> \<Longrightarrow> \<exists>x'a. pasObjectAbs aag x' = pasObjectAbs aag x'a \<and> (\<exists>y'a. pasObjectAbs aag y' = pasObjectAbs aag y'a \<and> (x'a, aa, y'a) \<in> cdl_state_objs_to_policy (transform s))
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>aa x' y'. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (x', aa, y') \<in> state_objs_to_policy s\<rbrakk> \<Longrightarrow> (x', aa, y') \<in> cdl_state_objs_to_policy (transform s)
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 3. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_asids_to_policy_aux aag (caps_of_state s) (asid_table s) (state_vrefs s)\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> cdl_state_asids_to_policy aag (transform s)
 2. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>a aa b. \<lbrakk>invs s; valid_list s; valid_sched s; pas_wellformed aag; cdl_irq_map_wellformed aag (transform s); cdl_tcb_domain_map_wellformed aag (transform s); auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy (transform s)) \<subseteq> pasPolicy aag; cdl_state_asids_to_policy aag (transform s) \<subseteq> pasPolicy aag; cdl_state_irqs_to_policy aag (transform s) \<subseteq> pasPolicy aag; (a, aa, b) \<in> state_irqs_to_policy aag s\<rbrakk> \<Longrightarrow> (a, aa, b) \<in> cdl_state_irqs_to_policy aag (transform s) proof (prove)
goal:
No subgoals!