theory Arch_C

lemma resolveVAddr_ret:
  "\<lbrace>valid_objs' and P \<rbrace> resolveVAddr p start
  \<lbrace>\<lambda>r s. P s \<and> (r \<noteq> None \<longrightarrow> is_aligned (snd (the r)) (pageBitsForSize (fst (the r))))
  \<rbrace>" apply (simp add:resolveVAddr_def) apply (wp getPDE_wp getPTE_wp|wpc|simp)+ apply (intro conjI impI allI) apply clarsimp apply (drule obj_at_valid_objs', clarsimp)+ apply (clarsimp simp: projectKOs valid_obj'_def valid_mapping'_def) apply (drule obj_at_valid_objs', clarsimp)+ apply (clarsimp simp: projectKOs valid_obj'_def valid_mapping'_def) apply (drule obj_at_valid_objs', clarsimp)+ apply (clarsimp simp: projectKOs valid_obj'_def valid_mapping'_def) apply (drule obj_at_valid_objs', clarsimp)+ apply (clarsimp simp: projectKOs valid_obj'_def valid_mapping'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and P\<rbrace> resolveVAddr p start \<lbrace>\<lambda>r s. P s \<and> (r \<noteq> None \<longrightarrow> is_aligned (snd (the r)) (pageBitsForSize (fst (the r))))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs' and P\<rbrace> getObject (lookup_pd_slot p start) >>= ARM_H.case_pde (return None) (\<lambda>table v61 v62. do y <- stateAssert (page_table_at' (ptrFromPAddr table)) [];
getObject (lookup_pt_slot_no_fail (ptrFromPAddr table) start) >>= ARM_H.case_pte (return None) (\<lambda>frame v42 v43 v44 v45. return (Some (Wellformed_C.ARMLargePage, frame))) (\<lambda>frame v46 v47 v48 v49. return (Some (Wellformed_C.ARMSmallPage, frame)))
od) (\<lambda>frame v50 v51 v52 v53 v54 v55. return (Some (Wellformed_C.ARMSection, frame))) (\<lambda>frame v56 v57 v58 v59 v60. return (Some (Wellformed_C.ARMSuperSection, frame))) \<lbrace>\<lambda>r s. P s \<and> ((\<exists>a b. r = Some (a, b)) \<longrightarrow> is_aligned (snd (the r)) (pageBitsForSize (fst (the r))))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> P s \<Longrightarrow> \<forall>ko. ko_at' ko (lookup_pd_slot p start) s \<longrightarrow> (\<forall>x. (\<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb) \<longrightarrow> page_table_at' (ptrFromPAddr x) s \<longrightarrow> (\<forall>ko. ko_at' ko (lookup_pt_slot_no_fail (ptrFromPAddr x) start) s \<longrightarrow> (\<forall>x. (\<exists>xa xb xc xd. ko = ARM_H.LargePagePTE x xa xb xc xd) \<longrightarrow> is_aligned x 16) \<and> (\<forall>x. (\<exists>xa xb xc xd. ko = ARM_H.SmallPagePTE x xa xb xc xd) \<longrightarrow> is_aligned x 12))) \<and> (\<forall>x. (\<exists>xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf) \<longrightarrow> is_aligned x 20) \<and> (\<forall>x. (\<exists>xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe) \<longrightarrow> is_aligned x 24) proof (prove)
goal (4 subgoals):
 1. \<And>s ko x koa xa. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb; page_table_at' (ptrFromPAddr x) s; ko_at' koa (lookup_pt_slot_no_fail (ptrFromPAddr x) start) s; \<exists>x xb xc xd. koa = ARM_H.LargePagePTE xa x xb xc xd\<rbrakk> \<Longrightarrow> is_aligned xa 16
 2. \<And>s ko x koa xa. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb; page_table_at' (ptrFromPAddr x) s; ko_at' koa (lookup_pt_slot_no_fail (ptrFromPAddr x) start) s; \<exists>x xb xc xd. koa = ARM_H.SmallPagePTE xa x xb xc xd\<rbrakk> \<Longrightarrow> is_aligned xa 12
 3. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf\<rbrakk> \<Longrightarrow> is_aligned x 20
 4. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe\<rbrakk> \<Longrightarrow> is_aligned x 24 proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb xc xd xe xf xg. \<lbrakk>ko_at' (ARM_H.PageTablePDE x xb xd) (lookup_pd_slot p start) s; page_table_at' (ptrFromPAddr x) s; ko_at' (ARM_H.LargePagePTE xa xc xe xf xg) (lookup_pt_slot_no_fail (ptrFromPAddr x) start) s; valid_objs' s; P s\<rbrakk> \<Longrightarrow> is_aligned xa 16
 2. \<And>s ko x koa xa. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb; page_table_at' (ptrFromPAddr x) s; ko_at' koa (lookup_pt_slot_no_fail (ptrFromPAddr x) start) s; \<exists>x xb xc xd. koa = ARM_H.SmallPagePTE xa x xb xc xd\<rbrakk> \<Longrightarrow> is_aligned xa 12
 3. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf\<rbrakk> \<Longrightarrow> is_aligned x 20
 4. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe\<rbrakk> \<Longrightarrow> is_aligned x 24 proof (prove)
goal (4 subgoals):
 1. \<And>s x xa xb xc xd xe xf xg. \<lbrakk>page_table_at' (ptrFromPAddr x) s; valid_objs' s; P s; \<exists>k. k = ARM_H.PageTablePDE x xb xd \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s); \<exists>k. k = ARM_H.LargePagePTE xa xc xe xf xg \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s)\<rbrakk> \<Longrightarrow> is_aligned xa 16
 2. \<And>s ko x koa xa. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb; page_table_at' (ptrFromPAddr x) s; ko_at' koa (lookup_pt_slot_no_fail (ptrFromPAddr x) start) s; \<exists>x xb xc xd. koa = ARM_H.SmallPagePTE xa x xb xc xd\<rbrakk> \<Longrightarrow> is_aligned xa 12
 3. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf\<rbrakk> \<Longrightarrow> is_aligned x 20
 4. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe\<rbrakk> \<Longrightarrow> is_aligned x 24 proof (prove)
goal (3 subgoals):
 1. \<And>s ko x koa xa. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb; page_table_at' (ptrFromPAddr x) s; ko_at' koa (lookup_pt_slot_no_fail (ptrFromPAddr x) start) s; \<exists>x xb xc xd. koa = ARM_H.SmallPagePTE xa x xb xc xd\<rbrakk> \<Longrightarrow> is_aligned xa 12
 2. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf\<rbrakk> \<Longrightarrow> is_aligned x 20
 3. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe\<rbrakk> \<Longrightarrow> is_aligned x 24 proof (prove)
goal (3 subgoals):
 1. \<And>s ko x koa xa. \<lbrakk>valid_objs' s \<and> P s; \<exists>xa xb. ko = ARM_H.PageTablePDE x xa xb; page_table_at' (ptrFromPAddr x) s; \<exists>x xb xc xd. koa = ARM_H.SmallPagePTE xa x xb xc xd; \<exists>k. k = ko \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s); \<exists>k. k = koa \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s)\<rbrakk> \<Longrightarrow> is_aligned xa 12
 2. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf\<rbrakk> \<Longrightarrow> is_aligned x 20
 3. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe\<rbrakk> \<Longrightarrow> is_aligned x 24 proof (prove)
goal (2 subgoals):
 1. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf\<rbrakk> \<Longrightarrow> is_aligned x 20
 2. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe\<rbrakk> \<Longrightarrow> is_aligned x 24 proof (prove)
goal (2 subgoals):
 1. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; \<exists>xa xb xc xd xe xf. ko = ARM_H.SectionPDE x xa xb xc xd xe xf; \<exists>k. k = ko \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s)\<rbrakk> \<Longrightarrow> is_aligned x 20
 2. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe\<rbrakk> \<Longrightarrow> is_aligned x 24 proof (prove)
goal (1 subgoal):
 1. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; ko_at' ko (lookup_pd_slot p start) s; \<exists>xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe\<rbrakk> \<Longrightarrow> is_aligned x 24 proof (prove)
goal (1 subgoal):
 1. \<And>s ko x. \<lbrakk>valid_objs' s \<and> P s; \<exists>xa xb xc xd xe. ko = ARM_H.SuperSectionPDE x xa xb xc xd xe; \<exists>k. k = ko \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKOS k = ko) \<longrightarrow> valid_obj' (injectKOS k) s)\<rbrakk> \<Longrightarrow> is_aligned x 24 proof (prove)
goal:
No subgoals!