theory CNode_DR

lemma opt_cap_pt_Some:
  "\<lbrakk>valid_idle s';kheap s' (y && ~~ mask pt_bits)= Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk>
         \<Longrightarrow>  (opt_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) (transform s'))
    = Some (transform_pte (fun (of_nat (unat (y && mask pt_bits >> 2)))))" apply (clarsimp simp: opt_cap_def transform_def slots_of_def object_slots_def
                        transform_objects_def map_add_def restrict_map_def not_idle_thread_def) apply (frule arch_obj_not_idle, simp) apply (clarsimp simp:transform_page_table_contents_def unat_map_def not_idle_thread_def) apply (rule unat_less_helper) apply clarsimp apply (subst shiftr_div_2n_w) apply (simp add:word_size)+ apply (rule word_div_mult,simp+) apply (rule eq_mask_less[where n = 10,simplified]) apply (simp add: mask_twice pt_bits_def pageBits_def word_size)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk> \<Longrightarrow> opt_cap (y && ~~ mask pt_bits, unat (y && mask pt_bits >> 2)) (transform s') = Some (transform_pte (fun (word_of_nat (unat (y && mask pt_bits >> 2))))) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk> \<Longrightarrow> (y && ~~ mask pt_bits \<noteq> idle_thread s' \<longrightarrow> transform_page_table_contents fun (unat (y && mask pt_bits >> 2)) = Some (transform_pte (fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))))) \<and> y && ~~ mask pt_bits \<noteq> idle_thread s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); not_idle_thread (y && ~~ mask pt_bits) s'\<rbrakk> \<Longrightarrow> (y && ~~ mask pt_bits \<noteq> idle_thread s' \<longrightarrow> transform_page_table_contents fun (unat (y && mask pt_bits >> 2)) = Some (transform_pte (fun (UCAST(32 \<rightarrow> 8) (y && mask pt_bits >> 2))))) \<and> y && ~~ mask pt_bits \<noteq> idle_thread s' proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); y && ~~ mask pt_bits \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> unat (y && mask pt_bits >> 2) < 256 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); y && ~~ mask pt_bits \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> y && mask pt_bits >> 2 < word_of_nat 256 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); y && ~~ mask pt_bits \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> y && mask pt_bits >> 2 < 0x100 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); y && ~~ mask pt_bits \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> (y && mask pt_bits) div 2\<^sup>2 < 0x100 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); y && ~~ mask pt_bits \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> (y && mask pt_bits) div 4 < 0x100 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); y && ~~ mask pt_bits \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> y && mask pt_bits < 0x400 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); y && ~~ mask pt_bits \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> y && mask pt_bits = (y && mask pt_bits) && mask 10
 2. \<lbrakk>valid_idle s'; kheap s' (y && ~~ mask pt_bits) = Some (ArchObj (arch_kernel_obj.PageTable fun)); y && ~~ mask pt_bits \<noteq> idle_thread s'\<rbrakk> \<Longrightarrow> 10 < LENGTH(32) proof (prove)
goal:
No subgoals!