theory Arch_DR

lemma store_pde_set_cap_corres:
  "\<lbrakk> slot = transform_pd_slot_ref ptr; cap = transform_pde pde ; ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow>
   dcorres dc \<top> valid_idle (KHeap_D.set_cap slot cap)
      (store_pde ptr pde)" apply (clarsimp simp:store_pde_def get_pd_def set_pd_def get_object_def gets_def bind_assoc) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:corres_free_fail assert_def split:Structures_A.kernel_object.splits arch_kernel_obj.splits) apply (clarsimp simp:transform_pd_slot_ref_def) apply (rule corres_guard_imp[OF dcorres_set_pde_cap]) apply (simp add: obj_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot = transform_pd_slot_ref ptr; cap = transform_pde pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) valid_idle (KHeap_D.set_cap slot cap) (store_pde ptr pde) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot = transform_pd_slot_ref ptr; cap = transform_pde pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) valid_idle (KHeap_D.set_cap (transform_pd_slot_ref ptr) (transform_pde pde)) (do x <- get;
xa <- assert (\<exists>y. kheap x (ptr && ~~ mask pd_bits) = Some y);
pd <- case the (kheap x (ptr && ~~ mask pd_bits)) of ArchObj (arch_kernel_obj.PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>slot = transform_pd_slot_ref ptr; cap = transform_pde pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True; valid_idle s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (transform_pd_slot_ref ptr) (transform_pde pde)) (do x <- assert (\<exists>y. kheap s' (ptr && ~~ mask pd_bits) = Some y);
pd <- case the (kheap s' (ptr && ~~ mask pd_bits)) of ArchObj (arch_kernel_obj.PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (pd(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>slot = transform_pd_slot_ref ptr; cap = transform_pde pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (transform_pd_slot_ref ptr) (transform_pde pde)) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) proof (prove)
goal (1 subgoal):
 1. \<And>s' x3. \<lbrakk>slot = (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)); cap = transform_pde pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)) (transform_pde pde)) (KHeap_A.set_object (ptr && ~~ mask pd_bits) (ArchObj (arch_kernel_obj.PageDirectory (x3(UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) := pde))))) proof (prove)
goal (5 subgoals):
 1. \<And>s' x3. \<lbrakk>slot = (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)); cap = transform_pde pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> ptr && mask pd_bits >> 2 = ?ptr25 s' x3 && mask pd_bits >> 2
 2. \<And>s' x3. \<lbrakk>slot = (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)); cap = transform_pde pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> transform_pde pde = transform_pde pde
 3. \<And>s' x3. \<lbrakk>slot = (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)); cap = transform_pde pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (?ptr25 s' x3 && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 4. \<And>s' x3 s. \<lbrakk>slot = (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)); cap = transform_pde pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); transform s' = s\<rbrakk> \<Longrightarrow> True
 5. \<And>s' x3 s. \<lbrakk>slot = (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2)); cap = transform_pde pde; UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'; kheap s' (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); s' = s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (arch_kernel_obj.PageDirectory x3) (ptr && ~~ mask pd_bits)) s proof (prove)
goal:
No subgoals!