theory Arch_C

lemma lookupPTSlot_le_0x3C:
  "\<lbrace>valid_objs' and K (vmsz_aligned' vptr ARMLargePage)\<rbrace>
      lookupPTSlot pd vptr \<lbrace>\<lambda>rv s. rv \<le> rv + 0x3C\<rbrace>,-" apply (rule hoare_gen_asmE) apply (simp add: lookupPTSlot_def cong: pde.case_cong) apply (rule hoare_pre) apply (wp getPDE_wp | wpc)+ apply clarsimp apply (drule(1) obj_at_valid_objs') apply (clarsimp simp: projectKOs) apply (clarsimp simp: valid_obj'_def ptBits_def pageBits_def vmsz_aligned'_def
                        lookup_pt_slot_no_fail_def) apply (subgoal_tac "is_aligned (ptrFromPAddr x) 10") apply (rule is_aligned_no_wrap' [where sz=6]) apply (erule aligned_add_aligned) apply clarsimp apply (rule is_aligned_andI1) apply clarsimp apply (simp add: word_bits_def) apply simp apply (rule is_aligned_ptrFromPAddr_n[rotated], simp) apply (erule is_aligned_weaken) apply (simp add: pteBits_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and K (vmsz_aligned' vptr Wellformed_C.ARMLargePage)\<rbrace> lookupPTSlot pd vptr \<lbrace>\<lambda>rv s. rv \<le> rv + 0x3C\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. vmsz_aligned' vptr Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>valid_objs'\<rbrace> lookupPTSlot pd vptr \<lbrace>\<lambda>rv s. rv \<le> rv + 0x3C\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. vmsz_aligned' vptr Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>valid_objs'\<rbrace> liftE (getObject (lookup_pd_slot pd vptr)) >>=E ARM_H.case_pde (throwError (Fault_H.lookup_failure.MissingCapability 20)) (\<lambda>x xa xb. liftE (do y <- stateAssert (page_table_at' (ptrFromPAddr x)) [];
return (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr)
od)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. throwError (Fault_H.lookup_failure.MissingCapability 20)) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. throwError (Fault_H.lookup_failure.MissingCapability 20)) \<lbrace>\<lambda>rv s. rv \<le> rv + 0x3C\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. vmsz_aligned' vptr Wellformed_C.ARMLargePage \<Longrightarrow> \<lbrace>?P'6\<rbrace> liftE (getObject (lookup_pd_slot pd vptr)) >>=E ARM_H.case_pde (throwError (Fault_H.lookup_failure.MissingCapability 20)) (\<lambda>x xa xb. liftE (do y <- stateAssert (page_table_at' (ptrFromPAddr x)) [];
return (lookup_pt_slot_no_fail (ptrFromPAddr x) vptr)
od)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. throwError (Fault_H.lookup_failure.MissingCapability 20)) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. throwError (Fault_H.lookup_failure.MissingCapability 20)) \<lbrace>\<lambda>rv s. rv \<le> rv + 0x3C\<rbrace>, -
 2. \<And>s. \<lbrakk>vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s\<rbrakk> \<Longrightarrow> ?P'6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s\<rbrakk> \<Longrightarrow> True \<and> (\<forall>ko. ko_at' ko (lookup_pd_slot pd vptr) s \<longrightarrow> (ko = ARM_H.InvalidPDE \<longrightarrow> True) \<and> (\<forall>x xa xb. ko = ARM_H.PageTablePDE x xa xb \<longrightarrow> page_table_at' (ptrFromPAddr x) s \<longrightarrow> lookup_pt_slot_no_fail (ptrFromPAddr x) vptr \<le> lookup_pt_slot_no_fail (ptrFromPAddr x) vptr + 0x3C) \<and> (\<forall>x xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe \<longrightarrow> True)) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; ko_at' (ARM_H.PageTablePDE x xa xb) (lookup_pd_slot pd vptr) s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> lookup_pt_slot_no_fail (ptrFromPAddr x) vptr \<le> lookup_pt_slot_no_fail (ptrFromPAddr x) vptr + 0x3C proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; page_table_at' (ptrFromPAddr x) s; \<exists>k. k = ARM_H.PageTablePDE x xa xb \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s)\<rbrakk> \<Longrightarrow> lookup_pt_slot_no_fail (ptrFromPAddr x) vptr \<le> lookup_pt_slot_no_fail (ptrFromPAddr x) vptr + 0x3C proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb. \<lbrakk>vmsz_aligned' vptr Wellformed_C.ARMLargePage; valid_objs' s; page_table_at' (ptrFromPAddr x) s; valid_obj' (KOArch (KOPDE (ARM_H.PageTablePDE x xa xb))) s\<rbrakk> \<Longrightarrow> lookup_pt_slot_no_fail (ptrFromPAddr x) vptr \<le> lookup_pt_slot_no_fail (ptrFromPAddr x) vptr + 0x3C proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) \<le> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) \<le> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C
 2. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10 proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 2. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 3. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10 proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 2. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> 6 \<le> 10
 3. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 4. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10 proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF) 4
 2. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> 6 \<le> 10
 3. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 4. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10 proof (prove)
goal (4 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 12) 4
 2. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> 6 \<le> 10
 3. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 4. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10 proof (prove)
goal (3 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> 6 \<le> 10
 2. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 3. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10 proof (prove)
goal (2 subgoals):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits); is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 2. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s; is_aligned x (8 + pteBits)\<rbrakk> \<Longrightarrow> is_aligned x 10 proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>is_aligned vptr 16; valid_objs' s; page_table_at' (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 10 \<le> 8 + pteBits proof (prove)
goal:
No subgoals!