theory ArchArch_AI

lemma vs_lookup_and_unique_refs:
  "\<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref';
    p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s)\<rbrakk>
   \<Longrightarrow> ref = ref'" apply (frule_tac ref=ref in valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], assumption) apply clarsimp apply (frule_tac cap'=capa in unique_table_refsD) apply simp+ apply (case_tac capa, simp_all) apply ((case_tac cap, simp_all)+)[6] apply (clarsimp simp add: table_cap_ref_def vs_cap_ref_def split: cap.splits arch_cap.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s)\<rbrakk> \<Longrightarrow> ref = ref' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); \<exists>slot cap. caps_of_state s slot = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> ref = ref' proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref\<rbrakk> \<Longrightarrow> ref = ref' proof (prove)
goal (4 subgoals):
 1. \<And>a b capa. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref\<rbrakk> \<Longrightarrow> caps_of_state s (?p8 a b capa) = Some (?cap8 a b capa)
 2. \<And>a b capa. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref\<rbrakk> \<Longrightarrow> caps_of_state s (?p'8 a b capa) = Some capa
 3. \<And>a b capa. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref\<rbrakk> \<Longrightarrow> obj_refs (?cap8 a b capa) = obj_refs capa
 4. \<And>a b capa. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; table_cap_ref (?cap8 a b capa) = table_cap_ref capa\<rbrakk> \<Longrightarrow> ref = ref' proof (prove)
goal (2 subgoals):
 1. \<And>a b capa. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref\<rbrakk> \<Longrightarrow> obj_refs cap = obj_refs capa
 2. \<And>a b capa. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; table_cap_ref cap = table_cap_ref capa\<rbrakk> \<Longrightarrow> ref = ref' proof (prove)
goal (7 subgoals):
 1. \<And>a b capa x31 x32 x33. \<lbrakk>(ref \<rhd> x31) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; x31 \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some (EndpointCap x31 x32 x33); p = x31; vs_cap_ref (EndpointCap x31 x32 x33) = Some ref; capa = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> obj_refs cap = {x31}
 2. \<And>a b capa x41 x42 x43. \<lbrakk>(ref \<rhd> x41) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; x41 \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some (NotificationCap x41 x42 x43); p = x41; vs_cap_ref (NotificationCap x41 x42 x43) = Some ref; capa = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> obj_refs cap = {x41}
 3. \<And>a b capa x61 x62 x63. \<lbrakk>(ref \<rhd> x61) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; x61 \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some (CNodeCap x61 x62 x63); p = x61; vs_cap_ref (CNodeCap x61 x62 x63) = Some ref; capa = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> obj_refs cap = {x61}
 4. \<And>a b capa x7. \<lbrakk>(ref \<rhd> x7) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; x7 \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some (ThreadCap x7); p = x7; vs_cap_ref (ThreadCap x7) = Some ref; capa = ThreadCap x7\<rbrakk> \<Longrightarrow> obj_refs cap = {x7}
 5. \<And>a b capa x111 x112 x113. \<lbrakk>(ref \<rhd> x111) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; x111 \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some (Zombie x111 x112 x113); p = x111; vs_cap_ref (Zombie x111 x112 x113) = Some ref; capa = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> obj_refs cap = {x111}
 6. \<And>a b capa x12. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some (ArchObjectCap x12); aobj_ref x12 = Some p; vs_cap_ref (ArchObjectCap x12) = Some ref; capa = ArchObjectCap x12\<rbrakk> \<Longrightarrow> obj_refs cap = {p}
 7. \<And>a b capa. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref capa = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; table_cap_ref cap = Some ref'\<rbrakk> \<Longrightarrow> ref = ref' proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref capa = Some ref'; p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s); caps_of_state s (a, b) = Some capa; p \<in> obj_refs capa; vs_cap_ref capa = Some ref; table_cap_ref cap = Some ref'\<rbrakk> \<Longrightarrow> ref = ref' proof (prove)
goal:
No subgoals!