From f3c0375c9fdcdc4f1ebcb5f9dd45a6904b515787 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 17 Aug 2024 13:35:28 +0200 Subject: [PATCH] x64+riscv proofs: adjust for init_arch_objects changes init_arch_objects now takes one more parameter. Signed-off-by: Gerwin Klein --- proof/access-control/RISCV64/ArchRetype_AC.thy | 2 +- proof/infoflow/RISCV64/ArchIRQMasks_IF.thy | 2 +- proof/infoflow/RISCV64/ArchRetype_IF.thy | 2 +- proof/invariant-abstract/RISCV64/ArchRetype_AI.thy | 4 ++-- proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy | 6 +++--- proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy | 2 +- proof/invariant-abstract/X64/ArchRetype_AI.thy | 4 ++-- proof/invariant-abstract/X64/ArchUntyped_AI.thy | 8 ++++---- proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy | 2 +- proof/refine/RISCV64/Retype_R.thy | 8 ++++---- proof/refine/X64/Retype_R.thy | 8 ++++---- 11 files changed, 24 insertions(+), 24 deletions(-) diff --git a/proof/access-control/RISCV64/ArchRetype_AC.thy b/proof/access-control/RISCV64/ArchRetype_AC.thy index f9b731c133..93b34a9022 100644 --- a/proof/access-control/RISCV64/ArchRetype_AC.thy +++ b/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 \pas_cur_domain aag\" + "init_arch_objects tp dev ptr n us refs \pas_cur_domain aag\" by wp lemma retype_region_pas_cur_domain[Retype_AC_assms, wp]: diff --git a/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy b/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy index 17cd0a26a7..e359be2327 100644 --- a/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy +++ b/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 \\s. P (irq_masks_of_state s)\" + "init_arch_objects new_type dev ptr num_objects obj_sz refs \\s. P (irq_masks_of_state s)\" by (rule init_arch_objects_inv) end diff --git a/proof/infoflow/RISCV64/ArchRetype_IF.thy b/proof/infoflow/RISCV64/ArchRetype_IF.thy index 13f9d1e402..194bdbbf0d 100644 --- a/proof/infoflow/RISCV64/ArchRetype_IF.thy +++ b/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 \ (init_arch_objects new_type ptr num_objects obj_sz refs)" + "reads_respects_g aag l \ (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: diff --git a/proof/invariant-abstract/RISCV64/ArchRetype_AI.thy b/proof/invariant-abstract/RISCV64/ArchRetype_AI.thy index 8fb5f9ae6c..f5592d1578 100644 --- a/proof/invariant-abstract/RISCV64/ArchRetype_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchRetype_AI.thy @@ -211,7 +211,7 @@ lemma init_arch_objects_invs_from_restricted: "\post_retype_invs new_type refs and (\s. global_refs s \ set refs = {}) and K (\ref \ set refs. is_aligned ref (obj_bits_api new_type obj_sz))\ - init_arch_objects new_type ptr bits obj_sz refs + init_arch_objects new_type dev ptr bits obj_sz refs \\_. invs\" 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: "\ex_cte_cap_wp_to P p\ - init_arch_objects tp ptr bits us refs + init_arch_objects tp dev ptr bits us refs \\rv s. ex_cte_cap_wp_to P p s\" by (wp ex_cte_cap_to_pres) diff --git a/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy b/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy index 2d0b6b3d22..db56478145 100644 --- a/proof/invariant-abstract/RISCV64/ArchUntyped_AI.thy +++ b/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]: "\\(s::'state_ext::state_ext state). descendants_range x cref s \ - init_arch_objects ty ptr n us y + init_arch_objects ty dev ptr n us y \\rv s. descendants_range x cref s\" unfolding init_arch_objects_def by wp lemma init_arch_objects_caps_overlap_reserved[wp,Untyped_AI_assms]: "\\(s::'state_ext::state_ext state). caps_overlap_reserved S s\ - init_arch_objects ty ptr n us y + init_arch_objects ty dev ptr n us y \\rv s. caps_overlap_reserved S s\" unfolding init_arch_objects_def by wp @@ -327,7 +327,7 @@ lemma init_arch_objects_nonempty_table[Untyped_AI_assms, wp]: "\(\s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ valid_global_objs s \ valid_arch_state s \ pspace_aligned s) and K (\ref\set refs. is_aligned ref (obj_bits_api tp us))\ - init_arch_objects tp ptr bits us refs + init_arch_objects tp dev ptr bits us refs \\rv s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\" unfolding init_arch_objects_def by wpsimp diff --git a/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy index dc7befa8c9..941ce0c46c 100644 --- a/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy @@ -202,7 +202,7 @@ lemma init_arch_objects_valid_vspace: "\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)\ - init_arch_objects type ptr n obj_sz orefs + init_arch_objects type dev ptr n obj_sz orefs \\rv. valid_vspace_objs'\" unfolding init_arch_objects_def by wpsimp diff --git a/proof/invariant-abstract/X64/ArchRetype_AI.thy b/proof/invariant-abstract/X64/ArchRetype_AI.thy index da95a99243..660b51071e 100644 --- a/proof/invariant-abstract/X64/ArchRetype_AI.thy +++ b/proof/invariant-abstract/X64/ArchRetype_AI.thy @@ -538,7 +538,7 @@ lemma init_arch_objects_invs_from_restricted: "\post_retype_invs new_type refs and (\s. global_refs s \ set refs = {}) and K (\ref \ set refs. is_aligned ref (obj_bits_api new_type obj_sz))\ - init_arch_objects new_type ptr bits obj_sz refs + init_arch_objects new_type dev ptr bits obj_sz refs \\_. invs\" 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]: - "\ex_cte_cap_wp_to P p\ init_arch_objects tp ptr bits us refs \\rv. ex_cte_cap_wp_to P p\" + "\ex_cte_cap_wp_to P p\ init_arch_objects tp dev ptr bits us refs \\rv. ex_cte_cap_wp_to P p\" by (wp ex_cte_cap_to_pres ) crunch init_arch_objects diff --git a/proof/invariant-abstract/X64/ArchUntyped_AI.thy b/proof/invariant-abstract/X64/ArchUntyped_AI.thy index b47869a887..5c165920b1 100644 --- a/proof/invariant-abstract/X64/ArchUntyped_AI.thy +++ b/proof/invariant-abstract/X64/ArchUntyped_AI.thy @@ -190,7 +190,7 @@ lemma copy_global_mappings_hoare_lift:(*FIXME: arch-split \ these d lemma init_arch_objects_hoare_lift: assumes wp: "\ptr val. \P\ store_pml4e ptr val \\rv. P\" - shows "\P\ init_arch_objects tp ptr sz us adds \\rv. P\" + shows "\P\ init_arch_objects tp dev ptr sz us adds \\rv. P\" proof - have pres: "\P\ return () \\rv. P\" 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]: - "\\(s::'state_ext::state_ext state). descendants_range x cref s \ init_arch_objects ty ptr n us y + "\\(s::'state_ext::state_ext state). descendants_range x cref s \ init_arch_objects ty dev ptr n us y \\rv s. descendants_range x cref s\" 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]: "\\(s::'state_ext::state_ext state). caps_overlap_reserved S s\ - init_arch_objects ty ptr n us y + init_arch_objects ty dev ptr n us y \\rv s. caps_overlap_reserved S s\" 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]: "\(\s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \ valid_global_objs s \ valid_arch_state s \ pspace_aligned s) and K (\ref\set refs. is_aligned ref (obj_bits_api tp us))\ - init_arch_objects tp ptr bits us refs + init_arch_objects tp dev ptr bits us refs \\rv s. \ (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\" apply (rule hoare_gen_asm) apply (simp add: init_arch_objects_def split del: if_split) diff --git a/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy index 45185e8a02..41ab59ae25 100644 --- a/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy @@ -528,7 +528,7 @@ lemma init_arch_objects_valid_vspace: "\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)\ - init_arch_objects type ptr n obj_sz orefs + init_arch_objects type dev ptr n obj_sz orefs \\rv. valid_vspace_objs'\" apply (rule hoare_gen_asm)+ apply (simp add: init_arch_objects_def) diff --git a/proof/refine/RISCV64/Retype_R.thy b/proof/refine/RISCV64/Retype_R.thy index f51fdc333a..f8ce48b864 100644 --- a/proof/refine/RISCV64/Retype_R.thy +++ b/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 _ \ return () - | _ \ init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs)" + | _ \ 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: \ valid_pspace' s \ valid_arch_state' s \ range_cover y sz (obj_bits_api (APIType_map2 (Inr ty)) us) n \ n\ 0) (do x \ 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 diff --git a/proof/refine/X64/Retype_R.thy b/proof/refine/X64/Retype_R.thy index eea316507a..7c4fb10a3c 100644 --- a/proof/refine/X64/Retype_R.thy +++ b/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 _ \ return () - | _ \ init_arch_objects (APIType_map2 (Inr ty)) ptr bits sz refs)" + | _ \ 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 \ Inr PML4Object - \ init_arch_objects (APIType_map2 tp) ptr n m addrs + \ 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: \ valid_pspace' s \ valid_arch_state' s \ range_cover y sz (obj_bits_api (APIType_map2 (Inr ty)) us) n \ n\ 0) (do x \ 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