theory Finalise_DR

lemma dcorres_get_pde_helper:
  "ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
  \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_pde r') \<top> valid_idle
  (cdl_get_pde (transform_pd_slot_ref ptr)) (get_pde ptr)" apply (simp add:cdl_get_pde_def
    get_pde_def gets_def gets_the_def
    get_pd_def get_object_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (rule dcorres_absorb_get_r) apply (clarsimp simp:assert_def assert_opt_def
    corres_free_fail
    split:Structures_A.kernel_object.splits
    arch_kernel_obj.splits) apply (drule(2) pd_at_cdl_pd_at) apply (simp add:ucast_nat_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_pde r') (\<lambda>_. True) valid_idle (cdl_get_pde (transform_pd_slot_ref ptr)) (get_pde ptr) proof (prove)
goal (1 subgoal):
 1. UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_pde r') (\<lambda>_. True) valid_idle (do s <- get;
assert_opt (opt_cap (transform_pd_slot_ref ptr) s)
od) (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;
return (pd (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True; valid_idle s'\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_pde r') ((=) (transform s')) ((=) s') (assert_opt (opt_cap (transform_pd_slot_ref ptr) (transform s'))) (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;
return (pd (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s' s'a. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; True; valid_idle s'; transform s' = transform s'a; s' = s'a\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_pde r') ((=) (transform s'a)) ((=) s'a) (assert_opt (opt_cap (transform_pd_slot_ref ptr) (transform s'))) (do x <- assert (\<exists>y. kheap s'a (ptr && ~~ mask pd_bits) = Some y);
pd <- case the (kheap s'a (ptr && ~~ mask pd_bits)) of ArchObj (arch_kernel_obj.PageDirectory xa) \<Rightarrow> return xa | ArchObj _ \<Rightarrow> fail | _ \<Rightarrow> fail;
return (pd (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2)))
od) proof (prove)
goal (1 subgoal):
 1. \<And>s'a x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_idle s'a; kheap s'a (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3))\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_pde r') ((=) (transform s'a)) ((=) s'a) (case opt_cap (transform_pd_slot_ref ptr) (transform s'a) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (x3 (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2)))) proof (prove)
goal (1 subgoal):
 1. \<And>s'a x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s'a (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory x3)); opt_cap (transform_pd_slot_ref ptr) (transform s'a) = Some (transform_pde (x3 (word_of_nat (unat (ptr && mask pd_bits >> 2)))))\<rbrakk> \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_pde r') ((=) (transform s'a)) ((=) s'a) (case opt_cap (transform_pd_slot_ref ptr) (transform s'a) of None \<Rightarrow> fail | Some x \<Rightarrow> return x) (return (x3 (UCAST(32 \<rightarrow> 12) (ptr && mask pd_bits >> 2)))) proof (prove)
goal:
No subgoals!