theory CSpaceAcc_C

lemma pageBitsForSize_spec:
  "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. \<acute>pagesize && mask 2 = \<acute>pagesize\<rbrace> Call pageBitsForSize_'proc
   \<lbrace> \<acute>ret__unsigned_long = of_nat (pageBitsForSize (gen_framesize_to_H \<^bsup>s\<^esup>pagesize)) \<rbrace>" apply vcg apply clarsimp apply (clarsimp simp: pageBitsForSize_def gen_framesize_to_H_def
                        ARMSmallPageBits_def ARMLargePageBits_def ARMSectionBits_def
                        ARMSuperSectionBits_def Kernel_C.ARMSmallPage_def
                        Kernel_C.ARMLargePage_def Kernel_C.ARMSection_def
                        Kernel_C.ARMSuperSection_def) apply (subst (asm) mask_eq_iff_w2p, simp add: word_size) apply simp apply (drule word_less_cases [where y=4]) apply (erule disjE, simp, simp) apply (drule word_less_cases [where y=3]) apply (erule disjE, simp, simp) apply (drule word_less_cases [where y=2]) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s. \<Gamma>\<turnstile> \<lbrace>s. \<acute>pagesize && mask 2 = \<acute>pagesize\<rbrace> Call pageBitsForSize_'proc \<lbrace>\<acute>ret__unsigned_long = word_of_nat (pageBitsForSize (gen_framesize_to_H \<^bsup>s\<^esup>pagesize))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>pagesize. pagesize && mask 2 = pagesize \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = pagesize \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMSmallPageBits = word_of_nat (pageBitsForSize (gen_framesize_to_H pagesize))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> pagesize \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = pagesize \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMLargePageBits = word_of_nat (pageBitsForSize (gen_framesize_to_H pagesize))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage \<noteq> pagesize \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = pagesize \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMSectionBits = word_of_nat (pageBitsForSize (gen_framesize_to_H pagesize))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> pagesize \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = pagesize \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMSuperSectionBits = word_of_nat (pageBitsForSize (gen_framesize_to_H pagesize))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection \<noteq> pagesize \<longrightarrow> (True \<longrightarrow> False) \<and> (\<not> True \<longrightarrow> False))))) proof (prove)
goal (1 subgoal):
 1. \<And>pagesize. pagesize && mask 2 = pagesize \<Longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage = pagesize \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMSmallPageBits = word_of_nat (pageBitsForSize (gen_framesize_to_H pagesize))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSmallPage \<noteq> pagesize \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage = pagesize \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMLargePageBits = word_of_nat (pageBitsForSize (gen_framesize_to_H pagesize))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMLargePage \<noteq> pagesize \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection = pagesize \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMSectionBits = word_of_nat (pageBitsForSize (gen_framesize_to_H pagesize))) \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSection \<noteq> pagesize \<longrightarrow> (SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = pagesize \<longrightarrow> SCAST(32 signed \<rightarrow> 32) ARMSuperSectionBits = word_of_nat (pageBitsForSize (gen_framesize_to_H pagesize))) \<and> SCAST(32 signed \<rightarrow> 32) Kernel_C.ARMSuperSection = pagesize))) proof (prove)
goal (1 subgoal):
 1. \<And>pagesize. \<lbrakk>pagesize && mask 2 = pagesize; 0 < pagesize; pagesize \<noteq> 1; pagesize \<noteq> 2\<rbrakk> \<Longrightarrow> pagesize = 3 proof (prove)
goal (1 subgoal):
 1. \<And>pagesize. \<lbrakk>pagesize < 2\<^sup>2; 0 < pagesize; pagesize \<noteq> 1; pagesize \<noteq> 2\<rbrakk> \<Longrightarrow> pagesize = 3 proof (prove)
goal (1 subgoal):
 1. \<And>pagesize. \<lbrakk>pagesize < 4; 0 < pagesize; pagesize \<noteq> 1; pagesize \<noteq> 2\<rbrakk> \<Longrightarrow> pagesize = 3 proof (prove)
goal (1 subgoal):
 1. \<And>pagesize. \<lbrakk>0 < pagesize; pagesize \<noteq> 1; pagesize \<noteq> 2; pagesize = 4 - 1 \<or> pagesize < 4 - 1\<rbrakk> \<Longrightarrow> pagesize = 3 proof (prove)
goal (1 subgoal):
 1. \<And>pagesize. \<lbrakk>0 < pagesize; pagesize \<noteq> 1; pagesize \<noteq> 2; pagesize < 3\<rbrakk> \<Longrightarrow> pagesize = 3 proof (prove)
goal (1 subgoal):
 1. \<And>pagesize. \<lbrakk>0 < pagesize; pagesize \<noteq> 1; pagesize \<noteq> 2; pagesize = 3 - 1 \<or> pagesize < 3 - 1\<rbrakk> \<Longrightarrow> pagesize = 3 proof (prove)
goal (1 subgoal):
 1. \<And>pagesize. \<lbrakk>0 < pagesize; pagesize \<noteq> 1; pagesize \<noteq> 2; pagesize < 2\<rbrakk> \<Longrightarrow> pagesize = 3 proof (prove)
goal (1 subgoal):
 1. \<And>pagesize. \<lbrakk>0 < pagesize; pagesize \<noteq> 1; pagesize \<noteq> 2; pagesize = 2 - 1 \<or> pagesize < 2 - 1\<rbrakk> \<Longrightarrow> pagesize = 3 proof (prove)
goal:
No subgoals!