theory Arch_DR

lemma store_pte_set_cap_corres:
  "\<lbrakk> slot = transform_pt_slot_ref ptr; cap = transform_pte pte\<rbrakk> \<Longrightarrow>
   dcorres dc \<top> valid_idle (KHeap_D.set_cap slot cap)
      (store_pte ptr pte)" apply (clarsimp simp:store_pte_def get_pt_def set_pt_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_pt_slot_ref_def) apply (rule corres_guard_imp[OF dcorres_set_pte_cap]) apply (simp add: obj_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot = transform_pt_slot_ref ptr; cap = transform_pte pte\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) valid_idle (KHeap_D.set_cap slot cap) (store_pte ptr pte) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>slot = transform_pt_slot_ref ptr; cap = transform_pte pte\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) valid_idle (KHeap_D.set_cap (transform_pt_slot_ref ptr) (transform_pte pte)) (do x <- get;
xa <- assert (\<exists>y. kheap x (ptr && ~~ mask pt_bits) = Some y);
pt <- case the (kheap x (ptr && ~~ mask pt_bits)) of ArchObj (arch_kernel_obj.PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := pte))))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>slot = transform_pt_slot_ref ptr; cap = transform_pte pte; True; valid_idle s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (transform_pt_slot_ref ptr) (transform_pte pte)) (do x <- assert (\<exists>y. kheap s' (ptr && ~~ mask pt_bits) = Some y);
pt <- case the (kheap s' (ptr && ~~ mask pt_bits)) of ArchObj (arch_kernel_obj.PageTable xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (pt(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := pte))))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2. \<lbrakk>slot = transform_pt_slot_ref ptr; cap = transform_pte pte; valid_idle s'; kheap s' (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (transform_pt_slot_ref ptr) (transform_pte pte)) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := pte))))) proof (prove)
goal (1 subgoal):
 1. \<And>s' x2. \<lbrakk>slot = (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)); cap = transform_pte pte; valid_idle s'; kheap s' (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (KHeap_D.set_cap (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)) (transform_pte pte)) (KHeap_A.set_object (ptr && ~~ mask pt_bits) (ArchObj (arch_kernel_obj.PageTable (x2(UCAST(32 \<rightarrow> 8) (ptr && mask pt_bits >> 2) := pte))))) proof (prove)
goal (4 subgoals):
 1. \<And>s' x2. \<lbrakk>slot = (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)); cap = transform_pte pte; valid_idle s'; kheap s' (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> ?x25 s' x2 = ptr && mask pt_bits >> 2
 2. \<And>s' x2. \<lbrakk>slot = (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)); cap = transform_pte pte; valid_idle s'; kheap s' (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2))\<rbrakk> \<Longrightarrow> transform_pte pte = transform_pte pte
 3. \<And>s' x2 s. \<lbrakk>slot = (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)); cap = transform_pte pte; valid_idle s'; kheap s' (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); transform s' = s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' x2 s. \<lbrakk>slot = (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2)); cap = transform_pte pte; valid_idle s'; kheap s' (ptr && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable x2)); s' = s\<rbrakk> \<Longrightarrow> (valid_idle and ako_at (arch_kernel_obj.PageTable x2) (ptr && ~~ mask pt_bits)) s proof (prove)
goal:
No subgoals!