theory CSpace_AI

lemma set_untyped_cap_as_full_cap_zombies_final:
  "\<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s.  zombies_final s\<rbrace>" apply (clarsimp simp:set_untyped_cap_as_full_def
    split:if_split_asm | rule conjI | wp set_cap_zombies )+ apply (clarsimp simp:cte_wp_at_caps_of_state) apply (rule zombies_finalD2) apply (simp add:get_cap_caps_of_state) apply (rule sym,simp) apply (simp add:get_cap_caps_of_state) apply (rule sym,simp) apply simp+ apply (clarsimp simp:is_cap_simps free_index_update_def)+ apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; cte_wp_at ((=) src_cap) src s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap'. \<forall>r\<in>ex_zombie_refs (max_free_index_update src_cap, cap'). \<forall>a b. src \<noteq> (a, b) \<and> cte_wp_at (\<lambda>cap''. r \<in> obj_refs cap'') (a, b) s \<longrightarrow> cte_wp_at (Not \<circ> is_zombie) (a, b) s \<and> \<not> is_zombie src_cap) src s
 2. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> \<not> is_zombie capa \<and> \<not> is_zombie src_cap
 2. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> fst (get_cap (?p33 s r a b capa) (?s33 s r a b capa)) = {(capa, ?s33 s r a b capa)}
 2. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> fst (get_cap (?p'33 s r a b capa) (?s33 s r a b capa)) = {(src_cap, ?s33 s r a b capa)}
 3. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> ?p33 s r a b capa \<noteq> ?p'33 s r a b capa
 4. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> zombies_final (?s33 s r a b capa)
 5. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> obj_refs capa \<inter> obj_refs src_cap \<noteq> {}
 6. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> Some capa = caps_of_state (?s33 s r a b capa) (?p33 s r a b capa)
 2. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> fst (get_cap (?p'33 s r a b capa) (?s33 s r a b capa)) = {(src_cap, ?s33 s r a b capa)}
 3. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> ?p33 s r a b capa \<noteq> ?p'33 s r a b capa
 4. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> zombies_final (?s33 s r a b capa)
 5. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> obj_refs capa \<inter> obj_refs src_cap \<noteq> {}
 6. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> fst (get_cap (?p'33 s r a b capa) s) = {(src_cap, s)}
 2. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> (a, b) \<noteq> ?p'33 s r a b capa
 3. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> zombies_final s
 4. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> obj_refs capa \<inter> obj_refs src_cap \<noteq> {}
 5. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> Some src_cap = caps_of_state s (?p'33 s r a b capa)
 2. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> (a, b) \<noteq> ?p'33 s r a b capa
 3. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> zombies_final s
 4. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> obj_refs capa \<inter> obj_refs src_cap \<noteq> {}
 5. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> (a, b) \<noteq> src
 2. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> zombies_final s
 3. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> obj_refs capa \<inter> obj_refs src_cap \<noteq> {}
 4. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s r a b capa. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; zombies_final s; caps_of_state s src = Some src_cap; r \<in> ex_zombie_refs (max_free_index_update src_cap, src_cap); src \<noteq> (a, b); caps_of_state s (a, b) = Some capa; r \<in> obj_refs capa\<rbrakk> \<Longrightarrow> obj_refs capa \<inter> obj_refs src_cap \<noteq> {}
 2. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<longrightarrow> (\<exists>dev r bits f. src_cap = UntypedCap dev r bits f) \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap \<Longrightarrow> \<lbrace>zombies_final and cte_wp_at ((=) src_cap) src\<rbrace> return () \<lbrace>\<lambda>rv. zombies_final\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> (\<exists>dev r bits f. cap = UntypedCap dev r bits f) \<longrightarrow> (\<exists>dev r bits f. src_cap = UntypedCap dev r bits f) \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; (zombies_final and cte_wp_at ((=) src_cap) src) s\<rbrakk> \<Longrightarrow> zombies_final s proof (prove)
goal:
No subgoals!