x64+riscv proofs: adjust for init_arch_objects changes

init_arch_objects now takes one more parameter.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

proof/access-control/RISCV64/ArchRetype_AC.thy

@@ -250,7 +250,7 @@ crunch delete_objects
   (ignore: do_machine_op freeMemory)
 
 lemma init_arch_objects_pas_cur_domain[Retype_AC_assms, wp]:
-  "init_arch_objects tp ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>"
+  "init_arch_objects tp dev ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>"
   by wp
 
 lemma retype_region_pas_cur_domain[Retype_AC_assms, wp]:

proof/infoflow/RISCV64/ArchIRQMasks_IF.thy

@@ -152,7 +152,7 @@ lemma invoke_tcb_irq_masks[IRQMasks_IF_assms]:
   by fastforce+
 
 lemma init_arch_objects_irq_masks:
-  "init_arch_objects new_type ptr num_objects obj_sz refs \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>"
+  "init_arch_objects new_type dev ptr num_objects obj_sz refs \<lbrace>\<lambda>s. P (irq_masks_of_state s)\<rbrace>"
   by (rule init_arch_objects_inv)
 
 end

proof/infoflow/RISCV64/ArchRetype_IF.thy

@@ -227,7 +227,7 @@ lemma dmo_freeMemory_globals_equiv[Retype_IF_assms]:
   done
 
 lemma init_arch_objects_reads_respects_g:
-  "reads_respects_g aag l \<top> (init_arch_objects new_type ptr num_objects obj_sz refs)"
+  "reads_respects_g aag l \<top> (init_arch_objects new_type dev ptr num_objects obj_sz refs)"
   unfolding init_arch_objects_def by wp
 
 lemma copy_global_mappings_globals_equiv:

proof/invariant-abstract/RISCV64/ArchRetype_AI.thy

@@ -211,7 +211,7 @@ lemma init_arch_objects_invs_from_restricted:
   "\<lbrace>post_retype_invs new_type refs
          and (\<lambda>s. global_refs s \<inter> set refs = {})
          and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace>
-     init_arch_objects new_type ptr bits obj_sz refs
+     init_arch_objects new_type dev ptr bits obj_sz refs
    \<lbrace>\<lambda>_. invs\<rbrace>"
   apply (simp add: init_arch_objects_def split del: if_split)
   apply (rule hoare_pre)
@@ -1047,7 +1047,7 @@ crunch init_arch_objects
 
 lemma init_arch_objects_excap:
   "\<lbrace>ex_cte_cap_wp_to P p\<rbrace>
-      init_arch_objects tp ptr bits us refs
+      init_arch_objects tp dev ptr bits us refs
    \<lbrace>\<lambda>rv s. ex_cte_cap_wp_to P p s\<rbrace>"
   by (wp ex_cte_cap_to_pres)
 

proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy

@@ -191,13 +191,13 @@ lemma cap_refs_in_kernel_windowD2:
 
 lemma init_arch_objects_descendants_range[wp,Untyped_AI_assms]:
   "\<lbrace>\<lambda>(s::'state_ext::state_ext state). descendants_range x cref s \<rbrace>
-   init_arch_objects ty ptr n us y
+   init_arch_objects ty dev ptr n us y
    \<lbrace>\<lambda>rv s. descendants_range x cref s\<rbrace>"
   unfolding init_arch_objects_def by wp
 
 lemma init_arch_objects_caps_overlap_reserved[wp,Untyped_AI_assms]:
   "\<lbrace>\<lambda>(s::'state_ext::state_ext state). caps_overlap_reserved S s\<rbrace>
-   init_arch_objects ty ptr n us y
+   init_arch_objects ty dev ptr n us y
    \<lbrace>\<lambda>rv s. caps_overlap_reserved S s\<rbrace>"
   unfolding init_arch_objects_def by wp
 
@@ -327,7 +327,7 @@ lemma init_arch_objects_nonempty_table[Untyped_AI_assms, wp]:
   "\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
          \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and
     K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us))\<rbrace>
-        init_arch_objects tp ptr bits us refs
+        init_arch_objects tp dev ptr bits us refs
    \<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>"
   unfolding init_arch_objects_def by wpsimp
 

proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy

@@ -202,7 +202,7 @@ lemma init_arch_objects_valid_vspace:
   "\<lbrace>valid_vspace_objs' and pspace_aligned and valid_arch_state
            and K (orefs = retype_addrs ptr type n us)
            and K (range_cover ptr sz (obj_bits_api type us) n)\<rbrace>
-     init_arch_objects type ptr n obj_sz orefs
+     init_arch_objects type dev ptr n obj_sz orefs
    \<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
   unfolding init_arch_objects_def by wpsimp
 

proof/invariant-abstract/X64/ArchRetype_AI.thy

@@ -538,7 +538,7 @@ lemma init_arch_objects_invs_from_restricted:
   "\<lbrace>post_retype_invs new_type refs
          and (\<lambda>s. global_refs s \<inter> set refs = {})
          and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace>
-     init_arch_objects new_type ptr bits obj_sz refs
+     init_arch_objects new_type dev ptr bits obj_sz refs
    \<lbrace>\<lambda>_. invs\<rbrace>"
   apply (simp add: init_arch_objects_def)
   apply (rule hoare_pre)
@@ -1287,7 +1287,7 @@ crunch init_arch_objects
   (wp: crunch_wps)
 
 lemma init_arch_objects_excap[wp]:
-  "\<lbrace>ex_cte_cap_wp_to P p\<rbrace> init_arch_objects tp ptr bits us refs \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>"
+  "\<lbrace>ex_cte_cap_wp_to P p\<rbrace> init_arch_objects tp dev ptr bits us refs \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>"
   by (wp ex_cte_cap_to_pres )
 
 crunch init_arch_objects

proof/invariant-abstract/X64/ArchUntyped_AI.thy

@@ -190,7 +190,7 @@ lemma copy_global_mappings_hoare_lift:(*FIXME: arch-split  \<rightarrow> these d
 
 lemma init_arch_objects_hoare_lift:
   assumes wp:  "\<And>ptr val. \<lbrace>P\<rbrace> store_pml4e ptr val \<lbrace>\<lambda>rv. P\<rbrace>"
-  shows       "\<lbrace>P\<rbrace> init_arch_objects tp ptr sz us adds \<lbrace>\<lambda>rv. P\<rbrace>"
+  shows       "\<lbrace>P\<rbrace> init_arch_objects tp dev ptr sz us adds \<lbrace>\<lambda>rv. P\<rbrace>"
 proof -
   have pres: "\<lbrace>P\<rbrace> return () \<lbrace>\<lambda>rv. P\<rbrace>"
     by (wp wp | simp)+
@@ -215,7 +215,7 @@ lemma cap_refs_in_kernel_windowD2:
   done
 
 lemma init_arch_objects_descendants_range[wp,Untyped_AI_assms]:
-  "\<lbrace>\<lambda>(s::'state_ext::state_ext state). descendants_range x cref s \<rbrace> init_arch_objects ty ptr n us y
+  "\<lbrace>\<lambda>(s::'state_ext::state_ext state). descendants_range x cref s \<rbrace> init_arch_objects ty dev ptr n us y
           \<lbrace>\<lambda>rv s. descendants_range x cref s\<rbrace>"
   apply (simp add:descendants_range_def)
   apply (rule hoare_pre)
@@ -230,7 +230,7 @@ lemma init_arch_objects_descendants_range[wp,Untyped_AI_assms]:
 
 lemma init_arch_objects_caps_overlap_reserved[wp,Untyped_AI_assms]:
   "\<lbrace>\<lambda>(s::'state_ext::state_ext state). caps_overlap_reserved S s\<rbrace>
-   init_arch_objects ty ptr n us y
+   init_arch_objects ty dev ptr n us y
    \<lbrace>\<lambda>rv s. caps_overlap_reserved S s\<rbrace>"
   apply (simp add:caps_overlap_reserved_def)
   apply (rule hoare_pre)
@@ -533,7 +533,7 @@ lemma init_arch_objects_nonempty_table[Untyped_AI_assms, wp]:
   "\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)
          \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and
     K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us))\<rbrace>
-        init_arch_objects tp ptr bits us refs
+        init_arch_objects tp dev ptr bits us refs
    \<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>"
   apply (rule hoare_gen_asm)
   apply (simp add: init_arch_objects_def split del: if_split)

proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy

@@ -528,7 +528,7 @@ lemma init_arch_objects_valid_vspace:
   "\<lbrace>valid_vspace_objs' and pspace_aligned and valid_arch_state
            and K (orefs = retype_addrs ptr type n us)
            and K (range_cover ptr sz (obj_bits_api type us) n)\<rbrace>
-     init_arch_objects type ptr n obj_sz orefs
+     init_arch_objects type dev ptr n obj_sz orefs
    \<lbrace>\<lambda>rv. valid_vspace_objs'\<rbrace>"
   apply (rule hoare_gen_asm)+
   apply (simp add: init_arch_objects_def)

proof/refine/RISCV64/Retype_R.thy

@@ -2615,9 +2615,9 @@ lemma corres_retype:
   done
 
 lemma init_arch_objects_APIType_map2:
-  "init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs =
+  "init_arch_objects (APIType_map2 (Inr ty)) dev ptr bits sz refs =
      (case ty of APIObjectType _ \<Rightarrow> return ()
-   | _ \<Rightarrow> init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs)"
+   | _ \<Rightarrow> init_arch_objects (APIType_map2 (Inr ty)) dev ptr bits sz refs)"
   apply (clarsimp split: RISCV64_H.object_type.split)
   apply (simp add: init_arch_objects_def APIType_map2_def
             split: apiobject_type.split)
@@ -5335,7 +5335,7 @@ lemma createObjects_Not_tcbQueued:
   done
 
 lemma init_arch_objects_APIType_map2_noop:
-  "init_arch_objects (APIType_map2 tp) ptr n m addrs = return ()"
+  "init_arch_objects (APIType_map2 tp) dev ptr n m addrs = return ()"
   apply (simp add: init_arch_objects_def APIType_map2_def)
   done
 
@@ -5359,7 +5359,7 @@ lemma corres_retype_region_createNewCaps:
                   \<and> valid_pspace' s \<and> valid_arch_state' s
                   \<and> range_cover y sz (obj_bits_api (APIType_map2 (Inr ty)) us) n \<and> n\<noteq> 0)
             (do x \<leftarrow> retype_region y n us (APIType_map2 (Inr ty)) dev :: obj_ref list det_ext_monad;
-                init_arch_objects (APIType_map2 (Inr ty)) y n us x;
+                init_arch_objects (APIType_map2 (Inr ty)) dev y n us x;
                 return x od)
             (createNewCaps ty y n us dev)"
   apply (rule_tac F="range_cover y sz (obj_bits_api (APIType_map2 (Inr ty)) us) n

proof/refine/X64/Retype_R.thy

@@ -2721,9 +2721,9 @@ lemma corres_retype:
   done
 
 lemma init_arch_objects_APIType_map2:
-  "init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs =
+  "init_arch_objects (APIType_map2 (Inr ty)) dev ptr bits sz refs =
      (case ty of APIObjectType _ \<Rightarrow> return ()
-   | _ \<Rightarrow> init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs)"
+   | _ \<Rightarrow> init_arch_objects (APIType_map2 (Inr ty)) dev ptr bits sz refs)"
   apply (clarsimp split: X64_H.object_type.split)
   apply (simp add: init_arch_objects_def APIType_map2_def
             split: apiobject_type.split)
@@ -5579,7 +5579,7 @@ lemma createObjects_Not_tcbQueued:
 
 lemma init_arch_objects_APIType_map2_noop:
   "tp \<noteq> Inr PML4Object
-   \<longrightarrow> init_arch_objects (APIType_map2 tp) ptr n m addrs
+   \<longrightarrow> init_arch_objects (APIType_map2 tp) dev ptr n m addrs
     = return ()"
   apply (simp add: init_arch_objects_def APIType_map2_def)
   apply (cases tp, simp_all split: kernel_object.split arch_kernel_object.split
@@ -5645,7 +5645,7 @@ lemma corres_retype_region_createNewCaps:
                   \<and> valid_pspace' s \<and> valid_arch_state' s
                   \<and> range_cover y sz (obj_bits_api (APIType_map2 (Inr ty)) us) n \<and> n\<noteq> 0)
             (do x \<leftarrow> retype_region y n us (APIType_map2 (Inr ty)) dev :: obj_ref list det_ext_monad;
-                init_arch_objects (APIType_map2 (Inr ty)) y n us x;
+                init_arch_objects (APIType_map2 (Inr ty)) dev y n us x;
                 return x od)
             (createNewCaps ty y n us dev)"
   apply (rule_tac F="range_cover y sz (obj_bits_api (APIType_map2 (Inr ty)) us) n