theory CNode_DR

lemma dcorres_set_asid_pool_none_trivial:
  "dcorres dc (\<lambda>s. opt_cap (a, snd (transform_asid asid)) s = Some cdl_cap.NullCap)
              (valid_idle and ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) a)
   (return ()) (set_asid_pool a (pool(ucast asid := None)))" apply (simp add:set_asid_pool_def get_object_def gets_def bind_assoc) apply (clarsimp simp:KHeap_D.set_object_def simpler_modify_def put_def bind_def obj_at_def
                       corres_underlying_def update_slots_def return_def object_slots_def) apply (clarsimp simp:KHeap_A.set_object_def get_object_def in_monad get_def put_def bind_def return_def) apply (clarsimp simp:transform_def transform_current_thread_def
                       opt_cap_def slots_of_def) apply (drule(1) arch_obj_not_idle) apply (rule ext) apply (clarsimp simp:not_idle_thread_def transform_objects_def restrict_map_def map_add_def) apply (case_tac "kheap b x") apply (subgoal_tac "x \<noteq> a") apply (clarsimp simp:fun_upd_other) apply clarsimp apply simp apply (rule_tac P="x \<noteq> a" in case_split) apply (clarsimp simp:fun_upd_other) apply (clarsimp simp:fun_upd_same object_slots_def) apply (rule ext) apply (clarsimp simp:transform_asid_pool_contents_def transform_asid_def) apply (clarsimp simp:unat_map_def) apply (rule_tac P="of_nat x \<noteq> (ucast asid :: 10 word)" in case_split) apply (clarsimp simp:fun_upd_other) apply (clarsimp simp:fun_upd_same transform_asid_pool_entry_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>s. opt_cap (a, snd (transform_asid asid)) s = Some cdl_cap.NullCap) (valid_idle and ako_at (ASIDPool pool) a) (return ()) (set_asid_pool a (pool(UCAST(32 \<rightarrow> 10) asid := None))) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>s. opt_cap (a, snd (transform_asid asid)) s = Some cdl_cap.NullCap) (valid_idle and ako_at (ASIDPool pool) a) (return ()) (KHeap_A.set_object a (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) proof (prove)
goal (1 subgoal):
 1. \<And>b ba. \<lbrakk>((), ba) \<in> fst (KHeap_A.set_object a (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))) b); opt_cap (a, snd (transform_asid asid)) (transform b) = Some cdl_cap.NullCap; valid_idle b; kheap b a = Some (ArchObj (ASIDPool pool))\<rbrakk> \<Longrightarrow> transform ba = transform b proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>opt_cap (a, snd (transform_asid asid)) (transform b) = Some cdl_cap.NullCap; valid_idle b; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))\<rbrakk> \<Longrightarrow> transform (update_kheap ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) b) = transform b proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>(case transform_objects b a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (snd (transform_asid asid)) = Some cdl_cap.NullCap; valid_idle b; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) b) = transform_objects b proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>(case transform_objects b a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); not_idle_thread a b\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) b) = transform_objects b proof (prove)
goal (1 subgoal):
 1. \<And>b x. \<lbrakk>(case transform_objects b a of None \<Rightarrow> \<lambda>x. None | Some x \<Rightarrow> object_slots x) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); not_idle_thread a b\<rbrakk> \<Longrightarrow> transform_objects (update_kheap ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) b) x = transform_objects b x proof (prove)
goal (1 subgoal):
 1. \<And>b x. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = (case kheap b x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) proof (prove)
goal (2 subgoals):
 1. \<And>b x. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = None\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = (case kheap b x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa)
 2. \<And>b x aa. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = Some aa\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = (case kheap b x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) proof (prove)
goal (3 subgoals):
 1. \<And>b x. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = None; x \<noteq> a\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = (case kheap b x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa)
 2. \<And>b x. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = None\<rbrakk> \<Longrightarrow> x \<noteq> a
 3. \<And>b x aa. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = Some aa\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = (case kheap b x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) proof (prove)
goal (2 subgoals):
 1. \<And>b x. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = None\<rbrakk> \<Longrightarrow> x \<noteq> a
 2. \<And>b x aa. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = Some aa\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = (case kheap b x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) proof (prove)
goal (1 subgoal):
 1. \<And>b x aa. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = Some aa\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = (case kheap b x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) proof (prove)
goal (1 subgoal):
 1. \<And>b x aa. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = Some aa\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = Some (transform_object (machine_state b) x (ekheap b x) aa) proof (prove)
goal (2 subgoals):
 1. \<And>b x aa. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = Some aa; x \<noteq> a\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = Some (transform_object (machine_state b) x (ekheap b x) aa)
 2. \<And>b x aa. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = Some aa; \<not> x \<noteq> a\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = Some (transform_object (machine_state b) x (ekheap b x) aa) proof (prove)
goal (1 subgoal):
 1. \<And>b x aa. \<lbrakk>object_slots (AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents pool\<rparr>) (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x \<noteq> idle_thread b; kheap b x = Some aa; \<not> x \<noteq> a\<rbrakk> \<Longrightarrow> (case ((kheap b)(a \<mapsto> ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None))))) x of None \<Rightarrow> Some cdl_object.Untyped | Some xa \<Rightarrow> (Some \<circ> transform_object (machine_state b) x (ekheap b x)) xa) = Some (transform_object (machine_state b) x (ekheap b x) aa) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>transform_asid_pool_contents pool (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> transform_asid_pool_contents (pool(UCAST(32 \<rightarrow> 10) asid := None)) = transform_asid_pool_contents pool proof (prove)
goal (1 subgoal):
 1. \<And>b x. \<lbrakk>transform_asid_pool_contents pool (snd (transform_asid asid)) = Some cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> transform_asid_pool_contents (pool(UCAST(32 \<rightarrow> 10) asid := None)) x = transform_asid_pool_contents pool x proof (prove)
goal (1 subgoal):
 1. \<And>b x. \<lbrakk>transform_asid_pool_entry (pool (UCAST(32 \<rightarrow> 10) asid)) = cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b\<rbrakk> \<Longrightarrow> unat_map (Some \<circ> transform_asid_pool_entry \<circ> pool(UCAST(32 \<rightarrow> 10) asid := None)) x = unat_map (Some \<circ> transform_asid_pool_entry \<circ> pool) x proof (prove)
goal (1 subgoal):
 1. \<And>b x. \<lbrakk>transform_asid_pool_entry (pool (UCAST(32 \<rightarrow> 10) asid)) = cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x < 1024\<rbrakk> \<Longrightarrow> transform_asid_pool_entry ((pool(UCAST(32 \<rightarrow> 10) asid := None)) (word_of_nat x)) = transform_asid_pool_entry (pool (word_of_nat x)) proof (prove)
goal (2 subgoals):
 1. \<And>b x. \<lbrakk>transform_asid_pool_entry (pool (UCAST(32 \<rightarrow> 10) asid)) = cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x < 1024; word_of_nat x \<noteq> UCAST(32 \<rightarrow> 10) asid\<rbrakk> \<Longrightarrow> transform_asid_pool_entry ((pool(UCAST(32 \<rightarrow> 10) asid := None)) (word_of_nat x)) = transform_asid_pool_entry (pool (word_of_nat x))
 2. \<And>b x. \<lbrakk>transform_asid_pool_entry (pool (UCAST(32 \<rightarrow> 10) asid)) = cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x < 1024; \<not> word_of_nat x \<noteq> UCAST(32 \<rightarrow> 10) asid\<rbrakk> \<Longrightarrow> transform_asid_pool_entry ((pool(UCAST(32 \<rightarrow> 10) asid := None)) (word_of_nat x)) = transform_asid_pool_entry (pool (word_of_nat x)) proof (prove)
goal (1 subgoal):
 1. \<And>b x. \<lbrakk>transform_asid_pool_entry (pool (UCAST(32 \<rightarrow> 10) asid)) = cdl_cap.NullCap; kheap b a = Some (ArchObj (ASIDPool pool)); a_type (ArchObj (ASIDPool pool)) = a_type (ArchObj (ASIDPool (pool(UCAST(32 \<rightarrow> 10) asid := None)))); a \<noteq> idle_thread b; x < 1024; \<not> word_of_nat x \<noteq> UCAST(32 \<rightarrow> 10) asid\<rbrakk> \<Longrightarrow> transform_asid_pool_entry ((pool(UCAST(32 \<rightarrow> 10) asid := None)) (word_of_nat x)) = transform_asid_pool_entry (pool (word_of_nat x)) proof (prove)
goal:
No subgoals!