theory Retype_R

lemma createNewCaps_valid_arch_state:
  "\<lbrace>(\<lambda>s. valid_arch_state' s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s
        \<and> (tp = APIObjectType ArchTypes_H.CapTableObject \<longrightarrow> us > 0))
       and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)\<rbrace>
     createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace>" apply (simp add: valid_arch_state'_def
                   valid_asid_table'_def
                   valid_global_pts'_def
                   page_table_at'_def
                   page_directory_at'_def
                   typ_at_to_obj_at_arches) apply (rule hoare_pre) apply (rule hoare_use_eq [where f=ksArchState, OF createNewCaps_ksArch]) apply (wp hoare_vcg_const_Ball_lift
             hoare_vcg_prop
             createNewCaps_obj_at''
             createNewCaps_ko_wp_at'
             hoare_vcg_all_lift
             hoare_vcg_const_imp_lift) apply (clarsimp simp: valid_pspace'_def o_def) apply (intro conjI) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. valid_arch_state' s \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and K (range_cover ptr sz (APIType_capBits ty us) n \<and> n \<noteq> 0)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv. valid_arch_state'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q8\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s))\<rbrace>
 2. \<And>s. ((\<lambda>s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> ?Q8 s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P11 f\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. dom (armKSASIDTable f) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable f) \<and> is_aligned (armKSGlobalPD f) pdBits \<and> (\<forall>y<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD f + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs f). is_aligned p ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable f) (map_option fst \<circ> armKSASIDMap f) \<and> valid_asid_map' (armKSASIDMap f)\<rbrace>
 2. \<And>s. ((\<lambda>s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> ?P11 (ksArchState s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>y<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD (ksArchState s) + (y << 2)) s) \<and> (\<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (p + (y << 2)) s)) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) \<and> valid_pspace' s \<and> pspace_no_overlap' ptr sz s \<and> (tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us)) and (\<lambda>y. range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)) s \<Longrightarrow> dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1} \<and> 0 \<notin> ran (armKSASIDTable (ksArchState s)) \<and> is_aligned (armKSGlobalPD (ksArchState s)) pdBits \<and> (\<forall>x<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD (ksArchState s) + (x << 2)) s \<and> range_cover ptr (?sz44 (ksArchState s) x) (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz44 (ksArchState s) x) s \<and> (koType TYPE(ARM_H.pde) = koType TYPE(ARM_H.pde) \<longrightarrow> (\<forall>x. True) \<and> (\<forall>pde. \<exists>x. injectKOS x = injectKOS pde)) \<and> (\<forall>tcb d. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> True) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> True))) \<and> (\<forall>x\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned x ptBits \<and> (\<forall>xa<0x100. obj_at' (\<lambda>_. True) (x + (xa << 2)) s \<and> range_cover ptr (?sz52 (ksArchState s) x xa) (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz52 (ksArchState s) x xa) s \<and> (koType TYPE(ARM_H.pte) = koType TYPE(ARM_H.pde) \<longrightarrow> (\<forall>x. True) \<and> (\<forall>pde. \<exists>x. injectKOS x = injectKOS pde)) \<and> (\<forall>tcb d. \<not> tcbQueued tcb \<and> tcbState tcb = Structures_H.thread_state.Inactive \<longrightarrow> (\<exists>obj. injectKOS obj = KOTCB (tcbDomain_update (\<lambda>_. d) tcb) \<and> True) = (\<exists>obj. injectKOS obj = KOTCB tcb \<and> True)))) \<and> is_inv (armKSHWASIDTable (ksArchState s)) (map_option fst \<circ> armKSASIDMap (ksArchState s)) \<and> valid_asid_map' (armKSASIDMap (ksArchState s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; 0 \<notin> ran (armKSASIDTable (ksArchState s)); is_aligned (armKSGlobalPD (ksArchState s)) pdBits; \<forall>y<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD (ksArchState s) + (y << 2)) s; \<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (p + (y << 2)) s); is_inv (armKSHWASIDTable (ksArchState s)) (\<lambda>x. map_option fst (armKSASIDMap (ksArchState s) x)); valid_asid_map' (armKSASIDMap (ksArchState s)); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; pspace_no_overlap' ptr sz s; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (APIType_capBits ty us) n; 0 < n\<rbrakk> \<Longrightarrow> (\<forall>x<0x1000. range_cover ptr (?sz44 (ksArchState s) x) (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr (?sz44 (ksArchState s) x) s) \<and> (\<forall>x\<in>set (armKSGlobalPTs (ksArchState s)). \<forall>xa<0x100. range_cover ptr (?sz52 (ksArchState s) x xa) (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr (?sz52 (ksArchState s) x xa) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; 0 \<notin> ran (armKSASIDTable (ksArchState s)); is_aligned (armKSGlobalPD (ksArchState s)) pdBits; \<forall>y<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD (ksArchState s) + (y << 2)) s; \<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (p + (y << 2)) s); is_inv (armKSHWASIDTable (ksArchState s)) (\<lambda>x. map_option fst (armKSASIDMap (ksArchState s) x)); valid_asid_map' (armKSASIDMap (ksArchState s)); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; pspace_no_overlap' ptr sz s; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (APIType_capBits ty us) n; 0 < n\<rbrakk> \<Longrightarrow> \<forall>x<0x1000. range_cover ptr (?sz44 (ksArchState s) x) (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr (?sz44 (ksArchState s) x) s
 2. \<And>s. \<lbrakk>dom (armKSASIDTable (ksArchState s)) \<subseteq> {0..2 ^ local.asid_high_bits - 1}; 0 \<notin> ran (armKSASIDTable (ksArchState s)); is_aligned (armKSGlobalPD (ksArchState s)) pdBits; \<forall>y<0x1000. obj_at' (\<lambda>_. True) (armKSGlobalPD (ksArchState s) + (y << 2)) s; \<forall>p\<in>set (armKSGlobalPTs (ksArchState s)). is_aligned p ptBits \<and> (\<forall>y<0x100. obj_at' (\<lambda>_. True) (p + (y << 2)) s); is_inv (armKSHWASIDTable (ksArchState s)) (\<lambda>x. map_option fst (armKSASIDMap (ksArchState s) x)); valid_asid_map' (armKSASIDMap (ksArchState s)); valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; pspace_no_overlap' ptr sz s; tp = APIObjectType ArchTypes_H.apiobject_type.CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (APIType_capBits ty us) n; 0 < n\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (armKSGlobalPTs (ksArchState s)). \<forall>xa<0x100. range_cover ptr (?sz52 (ksArchState s) x xa) (APIType_capBits ty us) n \<and> pspace_no_overlap' ptr (?sz52 (ksArchState s) x xa) s proof (prove)
goal:
No subgoals!