theory CNode_DR

lemma transform_pde_NullCap:
  "\<lbrakk>3584 \<le> unat (xa::word32); unat xa < 4096\<rbrakk> \<Longrightarrow>
            transform_pde (kernel_pde_mask ptx (ucast xa)) = cdl_cap.NullCap" apply (clarsimp simp:kernel_pde_mask_def kernel_base_def) apply (subst ucast_le_migrate[symmetric]) apply (simp add:word_size,unat_arith) apply (simp add:word_size)+ apply (drule word_of_nat_le,simp add:transform_pde_def) apply (subst ucast_le_migrate[symmetric]) apply (simp_all add:word_size) apply unat_arith done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3584 \<le> unat xa; unat xa < 4096\<rbrakk> \<Longrightarrow> transform_pde (kernel_pde_mask ptx (UCAST(32 \<rightarrow> 12) xa)) = cdl_cap.NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3584 \<le> unat xa; unat xa < 4096\<rbrakk> \<Longrightarrow> (0xE00 \<le> UCAST(32 \<rightarrow> 12) xa \<longrightarrow> transform_pde InvalidPDE = cdl_cap.NullCap) \<and> (\<not> 0xE00 \<le> UCAST(32 \<rightarrow> 12) xa \<longrightarrow> transform_pde (ptx (UCAST(32 \<rightarrow> 12) xa)) = cdl_cap.NullCap) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>3584 \<le> unat xa; unat xa < 4096\<rbrakk> \<Longrightarrow> xa < 2 ^ size 0xE00
 2. \<lbrakk>3584 \<le> unat xa; unat xa < 4096\<rbrakk> \<Longrightarrow> size 0xE00 < size xa
 3. \<lbrakk>3584 \<le> unat xa; unat xa < 4096\<rbrakk> \<Longrightarrow> (UCAST(12 \<rightarrow> 32) 0xE00 \<le> xa \<longrightarrow> transform_pde InvalidPDE = cdl_cap.NullCap) \<and> (\<not> 0xE00 \<le> UCAST(32 \<rightarrow> 12) xa \<longrightarrow> transform_pde (ptx (UCAST(32 \<rightarrow> 12) xa)) = cdl_cap.NullCap) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>3584 \<le> unat xa; unat xa < 4096\<rbrakk> \<Longrightarrow> size 0xE00 < size xa
 2. \<lbrakk>3584 \<le> unat xa; unat xa < 4096\<rbrakk> \<Longrightarrow> (UCAST(12 \<rightarrow> 32) 0xE00 \<le> xa \<longrightarrow> transform_pde InvalidPDE = cdl_cap.NullCap) \<and> (\<not> 0xE00 \<le> UCAST(32 \<rightarrow> 12) xa \<longrightarrow> transform_pde (ptx (UCAST(32 \<rightarrow> 12) xa)) = cdl_cap.NullCap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>3584 \<le> unat xa; unat xa < 4096\<rbrakk> \<Longrightarrow> (0xE00 \<le> xa \<longrightarrow> transform_pde InvalidPDE = cdl_cap.NullCap) \<and> (\<not> 0xE00 \<le> UCAST(32 \<rightarrow> 12) xa \<longrightarrow> transform_pde (ptx (UCAST(32 \<rightarrow> 12) xa)) = cdl_cap.NullCap) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat xa < 4096; 0xE00 \<le> xa\<rbrakk> \<Longrightarrow> \<not> 0xE00 \<le> UCAST(32 \<rightarrow> 12) xa \<longrightarrow> (case ptx (UCAST(32 \<rightarrow> 12) xa) of InvalidPDE \<Rightarrow> cdl_cap.NullCap | PageTablePDE ref x xa \<Rightarrow> cdl_cap.PageTableCap (transform_paddr ref) Fake None | SectionPDE ref x xa rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSection) Fake None | SuperSectionPDE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSuperSection) Fake None) = cdl_cap.NullCap proof (prove)
goal (3 subgoals):
 1. \<lbrakk>unat xa < 4096; 0xE00 \<le> xa\<rbrakk> \<Longrightarrow> xa < 2 ^ size 0xE00
 2. \<lbrakk>unat xa < 4096; 0xE00 \<le> xa\<rbrakk> \<Longrightarrow> size 0xE00 < size xa
 3. \<lbrakk>unat xa < 4096; 0xE00 \<le> xa\<rbrakk> \<Longrightarrow> \<not> UCAST(12 \<rightarrow> 32) 0xE00 \<le> xa \<longrightarrow> (case ptx (UCAST(32 \<rightarrow> 12) xa) of InvalidPDE \<Rightarrow> cdl_cap.NullCap | PageTablePDE ref x xa \<Rightarrow> cdl_cap.PageTableCap (transform_paddr ref) Fake None | SectionPDE ref x xa rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSection) Fake None | SuperSectionPDE ref x rights_ \<Rightarrow> FrameCap False (transform_paddr ref) rights_ (pageBitsForSize ARMSuperSection) Fake None) = cdl_cap.NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>unat xa < 4096; 0xE00 \<le> xa\<rbrakk> \<Longrightarrow> xa < 0x1000 proof (prove)
goal:
No subgoals!