adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

arm+arm-hyp: kernelBase and physMappingOffset renames 

This brings the naming convention closer to the other architectures,
closer to the Haskell, and closer to the constant renames that happened
in C. It is, however, quite an invasive change.

kernelBase_addr -> pptrBase
kernelBase -> pptrBase
physMappingOffset -> ptrBaseOffset

Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
This commit is contained in:
Rafal Kolanski 2020-11-13 22:24:06 +11:00 committed by Rafal Kolanski
parent 6ed9db6e75
commit 9ed45e17bd
30 changed files with 188 additions and 196 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/access-control/ADT_AC.thy
View File

@ -110,7 +110,7 @@ lemma ptable_state_objs_to_policy:
vspace_cap_rights_to_auth b)" in bexI)
apply clarsimp
apply (rule_tac x="(ptrFromPAddr a + (x && mask aa), auth)" in image_eqI)
apply (simp add: ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def)
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def)
apply (simp add: ptr_offset_in_ptr_range)
apply (simp add: kernel_mappings_kernel_mapping_slots')
@ -177,7 +177,7 @@ lemma get_page_info_state_objs_to_policy:
vspace_cap_rights_to_auth r)" in bexI)
apply clarsimp
apply (rule_tac x="(ptrFromPAddr base + (x && mask sz), auth)" in image_eqI)
apply (simp add: ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def)
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def)
apply (simp add: ptr_offset_in_ptr_range)
apply (clarsimp simp: graph_of_def)

34
proof/crefine/ARM/Arch_C.thy
View File

@ -731,7 +731,7 @@ lemma decodeARMPageTableInvocation_ccorres:
apply (simp add: if_to_top_of_bind del: Collect_const)
apply (rule ccorres_if_cond_throws[rotated -1, where Q=\<top> and Q'=\<top>])
apply vcg
apply (simp add: kernelBase_def ARM.kernelBase_def hd_conv_nth length_ineq_not_Nil)
apply (simp add: pptrBase_def ARM.pptrBase_def hd_conv_nth length_ineq_not_Nil)
apply (simp add: throwError_bind invocationCatch_def)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
@ -830,7 +830,7 @@ lemma decodeARMPageTableInvocation_ccorres:
apply (clarsimp | drule length_le_helper)+
apply (clarsimp simp: valid_cap'_def neq_Nil_conv
mask_add_aligned page_directory_at'_def
less_kernelBase_valid_pde_offset''
less_pptrBase_valid_pde_offset''
pageBits_def pteBits_def pdeBits_def ptBits_def
word_le_nat_alt[symmetric])
apply (auto simp: ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def
@ -1189,9 +1189,9 @@ lemma lookupPTSlot_le_0x3C:
apply clarsimp
apply (simp add: word_bits_def)
apply simp
apply (simp add: ARM.ptrFromPAddr_def physMappingOffset_def)
apply (simp add: ARM.ptrFromPAddr_def pptrBaseOffset_def)
apply (erule aligned_add_aligned)
apply (simp add: kernelBase_addr_def ARM.physBase_def
apply (simp add: pptrBase_def ARM.physBase_def
physBase_def is_aligned_def)
apply (simp add: word_bits_def pteBits_def)
done
@ -1438,8 +1438,8 @@ lemma valid_pde_slots_lift2:
lemma addrFromPPtr_mask_5:
"addrFromPPtr ptr && mask (5::nat) = ptr && mask (5::nat)"
apply (simp add:addrFromPPtr_def physMappingOffset_def
kernelBase_addr_def physBase_def ARM.physBase_def)
apply (simp add:addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM.physBase_def)
apply word_bitwise
apply (simp add:mask_def)
done
@ -1683,7 +1683,7 @@ lemma createMappingEntries_valid_pte_slots'2:
(* replay of proof in Arch_R with stronger validity result *)
lemma createMappingEntries_valid_pde_slots'2:
"\<lbrace>page_directory_at' pd and K (vmsz_aligned' vptr sz \<and> vptr < kernelBase)\<rbrace>
"\<lbrace>page_directory_at' pd and K (vmsz_aligned' vptr sz \<and> vptr < pptrBase)\<rbrace>
createMappingEntries base vptr sz vm_rights attrib pd
\<lbrace>\<lambda>rv. valid_pde_slots'2 rv\<rbrace>,-"
apply (simp add: createMappingEntries_def valid_pde_slots'2_def)
@ -1693,7 +1693,7 @@ lemma createMappingEntries_valid_pde_slots'2:
lookup_pd_slot_eq[unfolded pd_bits_def, folded pdBits_def])
apply (clarsimp simp: lookup_pd_slot_def Let_def mask_add_aligned)
apply (rule conjI)
apply (erule less_kernelBase_valid_pde_offset'')
apply (erule less_pptrBase_valid_pde_offset'')
apply (rule conjI)
apply (clarsimp simp: vaddr_segment_nonsense6)
apply (rule_tac x= 0 in exI)
@ -1710,7 +1710,7 @@ lemma createMappingEntries_valid_pde_slots'2:
apply (clarsimp simp: superSectionPDEOffsets_def length_upto_enum_step pdeBits_def)
apply (clarsimp simp: upto_enum_step_def upto_enum_def comp_def)
apply (clarsimp simp: linorder_not_less field_simps mask_add_aligned)
apply (erule less_kernelBase_valid_pde_offset', simp+)
apply (erule less_pptrBase_valid_pde_offset', simp+)
apply (rule word_of_nat_le, simp)
done
apply (rule conjI)
@ -1893,14 +1893,14 @@ lemma vmsz_aligned_addrFromPPtr':
= vmsz_aligned' p sz"
apply (simp add: vmsz_aligned'_def addrFromPPtr_def
ARM.addrFromPPtr_def)
apply (subgoal_tac "is_aligned physMappingOffset (pageBitsForSize sz)")
apply (subgoal_tac "is_aligned pptrBaseOffset (pageBitsForSize sz)")
apply (rule iffI)
apply (drule(1) aligned_add_aligned)
apply (simp add: pageBitsForSize_def word_bits_def split: vmpage_size.split)
apply simp
apply (erule(1) aligned_sub_aligned)
apply (simp add: pageBitsForSize_def word_bits_def split: vmpage_size.split)
apply (simp add: pageBitsForSize_def physMappingOffset_def kernelBase_addr_def
apply (simp add: pageBitsForSize_def pptrBaseOffset_def pptrBase_def
physBase_def ARM.physBase_def is_aligned_def
split: vmpage_size.split)
done
@ -2191,7 +2191,7 @@ lemma decodeARMFrameInvocation_ccorres:
is_aligned_neg_mask_eq[simp del]
is_aligned_neg_mask_weaken[simp del]
defines "does_not_throw args extraCaps pg_sz mapdata \<equiv>
(mapdata = None \<longrightarrow> \<not> (ARM_H.kernelBase \<le> hd args + 2 ^ pageBitsForSize pg_sz - 1)) \<and>
(mapdata = None \<longrightarrow> \<not> (ARM_H.pptrBase \<le> hd args + 2 ^ pageBitsForSize pg_sz - 1)) \<and>
(mapdata \<noteq> None \<longrightarrow> (fst (the mapdata) = (the (capPDMappedASID (capCap (fst (extraCaps ! 0)))))
\<and> snd (the mapdata) = hd args))"
shows
@ -2472,7 +2472,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
(* frame cap not mapped, check mapping *)
(* disallow mappings above kernelBase *)
(* disallow mappings above pptrBase *)
apply clarsimp
apply (prop_tac "mapdata = None")
apply (simp add: ccap_relation_mapped_asid_0)
@ -2484,7 +2484,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply clarsimp
apply ccorres_rewrite
apply csymbr
apply (simp add: ARM_H.kernelBase_def ARM.kernelBase_def hd_conv_nth length_ineq_not_Nil)
apply (simp add: ARM_H.pptrBase_def ARM.pptrBase_def hd_conv_nth length_ineq_not_Nil)
apply ccorres_rewrite
apply (rule syscall_error_throwError_ccorres_n[unfolded id_def dc_def])
apply (simp add: syscall_error_to_H_cases)
@ -2510,7 +2510,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply (rule ccorres_rhs_assoc)+
apply (csymbr, clarsimp, ccorres_rewrite)
apply (csymbr,
simp add: ARM_H.kernelBase_def ARM.kernelBase_def
simp add: ARM_H.pptrBase_def ARM.pptrBase_def
hd_conv_nth length_ineq_not_Nil,
ccorres_rewrite)
apply (fold dc_def)
@ -2678,7 +2678,7 @@ lemma decodeARMFrameInvocation_ccorres:
framesize_from_H_eq_eqs of_bool_nth[simplified of_bool_from_bool]
vm_page_size_defs neq_Nil_conv excaps_in_mem_def hd_conv_nth
length_ineq_not_Nil numeral_2_eq_2 does_not_throw_def
kernelBase_def ARM.kernelBase_def)
pptrBase_def ARM.pptrBase_def)
apply (frule interpret_excaps_eq[rule_format, where n=0], simp)
apply (frule(1) slotcap_in_mem_PageDirectory)
apply (clarsimp simp: mask_def[where n=4] typ_heap_simps' isCap_simps)
@ -2887,7 +2887,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
apply (simp add: syscall_error_to_H_cases)
apply (rule ccorres_if_cond_throws[rotated -1, where Q=\<top> and Q'=\<top>])
apply vcg
apply (clarsimp simp: hd_conv_nth length_ineq_not_Nil kernelBase_def ARM.kernelBase_def)
apply (clarsimp simp: hd_conv_nth length_ineq_not_Nil pptrBase_def ARM.pptrBase_def)
apply (simp add:injection_handler_throwError)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)

8
proof/crefine/ARM/Finalise_C.thy
View File

@ -1363,7 +1363,7 @@ lemma pageTableMapped_pd:
done
lemma unmapPageTable_ccorres:
"ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask asid_bits \<and> vaddr < kernelBase))
"ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask asid_bits \<and> vaddr < pptrBase))
(UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vaddr_' s = vaddr} \<inter> {s. pt_' s = Ptr ptPtr}) []
(unmapPageTable asid vaddr ptPtr) (Call unmapPageTable_'proc)"
apply (rule ccorres_gen_asm)
@ -1393,7 +1393,7 @@ lemma unmapPageTable_ccorres:
apply (rule_tac Q="\<lambda>rv s. (case rv of Some pd \<Rightarrow> page_directory_at' pd s | _ \<Rightarrow> True) \<and> invs' s"
in hoare_post_imp)
apply (clarsimp simp: lookup_pd_slot_def Let_def
mask_add_aligned less_kernelBase_valid_pde_offset''
mask_add_aligned less_pptrBase_valid_pde_offset''
page_directory_at'_def)
apply (wp pageTableMapped_pd)
apply (clarsimp simp: word_sle_def lookup_pd_slot_def
@ -1414,7 +1414,7 @@ lemma capFSize_eq: "\<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capab
apply (frule (1) cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def
case_option_over_if gen_framesize_to_H_def
ARM_H.kernelBase_def
ARM_H.pptrBase_def
framesize_to_H_def valid_cap'_def
elim!: ccap_relationE simp del: Collect_const)
apply (subgoal_tac "capFSize_CL (cap_frame_cap_lift cap) \<noteq> scast Kernel_C.ARMSmallPage")
@ -1726,7 +1726,7 @@ lemma Arch_finaliseCap_ccorres:
apply (subgoal_tac "capVPMappedAddress cp \<noteq> None")
apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def
case_option_over_if gen_framesize_to_H_def
Kernel_C.ARMSmallPage_def ARM_H.kernelBase_def
Kernel_C.ARMSmallPage_def ARM_H.pptrBase_def
if_split
elim!: ccap_relationE simp del: Collect_const)
apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def

2
proof/crefine/ARM/Invoke_C.thy
View File

@ -1519,7 +1519,7 @@ lemma pspace_no_overlap_underlying_zero_update:
lemma addrFromPPtr_mask:
"n \<le> 28
\<Longrightarrow> addrFromPPtr ptr && mask n = ptr && mask n"
apply (simp add: addrFromPPtr_def physMappingOffset_def kernelBase_addr_def
apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def
ARM.physBase_def)
apply word_bitwise
apply simp

2
proof/crefine/ARM/Retype_C.thy
View File

@ -3714,7 +3714,7 @@ lemma copyGlobalMappings_ccorres:
apply (cinit lift: newPD_' simp: ARMSectionBits_def pdeBits_def)
apply (rule ccorres_h_t_valid_armKSGlobalPD)
apply csymbr
apply (simp add: kernelBase_def ARM.kernelBase_def objBits_simps archObjSize_def
apply (simp add: pptrBase_def ARM.pptrBase_def objBits_simps archObjSize_def
whileAnno_def word_sle_def word_sless_def
Collect_True del: Collect_const)
apply (rule ccorres_pre_gets_armKSGlobalPD_ksArchState)

12
proof/crefine/ARM/VSpace_C.thy
View File

@ -709,8 +709,8 @@ lemma ptrFromPAddr_spec:
Call ptrFromPAddr_'proc
\<lbrace> \<acute>ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s) ) \<rbrace>"
apply vcg
apply (simp add: ARM.ptrFromPAddr_def physMappingOffset_def
kernelBase_addr_def physBase_def ARM.physBase_def)
apply (simp add: ARM.ptrFromPAddr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM.physBase_def)
done
lemma addrFromPPtr_spec:
@ -719,8 +719,8 @@ lemma addrFromPPtr_spec:
\<lbrace> \<acute>ret__unsigned_long = (addrFromPPtr (ptr_val (pptr_' s)) ) \<rbrace>"
apply vcg
apply (simp add: addrFromPPtr_def
ARM.addrFromPPtr_def physMappingOffset_def
kernelBase_addr_def physBase_def ARM.physBase_def)
ARM.addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM.physBase_def)
done
@ -2136,7 +2136,7 @@ lemmas ccorres_move_array_assertion_pde_16
lemma unmapPage_ccorres:
"ccorres dc xfdc (invs' and (\<lambda>s. 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s)
and (\<lambda>_. asid \<le> mask asid_bits \<and> vmsz_aligned' vptr sz
\<and> vptr < kernelBase))
\<and> vptr < pptrBase))
(UNIV \<inter> {s. gen_framesize_to_H (page_size_' s) = sz \<and> page_size_' s < 4}
\<inter> {s. asid_' s = asid} \<inter> {s. vptr_' s = vptr} \<inter> {s. pptr_' s = Ptr pptr}) []
(unmapPage sz asid vptr pptr) (Call unmapPage_'proc)"
@ -2366,7 +2366,7 @@ lemma unmapPage_ccorres:
apply (simp add: vmsz_aligned'_def vmsz_aligned_def)
apply (clarsimp simp: lookup_pd_slot_def Let_def
mask_add_aligned field_simps)
apply (erule less_kernelBase_valid_pde_offset')
apply (erule less_pptrBase_valid_pde_offset')
apply (simp add: vmsz_aligned'_def)
apply (simp add: word_le_nat_alt unat_of_nat)
apply (simp add: upto_enum_step_def)

40
proof/crefine/ARM_HYP/Arch_C.thy
View File

@ -768,7 +768,7 @@ lemma decodeARMPageTableInvocation_ccorres:
apply (simp add: if_to_top_of_bind del: Collect_const)
apply (rule ccorres_if_cond_throws[rotated -1, where Q=\<top> and Q'=\<top>])
apply vcg
apply (simp add: kernelBase_def ARM_HYP.kernelBase_def hd_conv_nth length_ineq_not_Nil)
apply (simp add: pptrBase_def ARM_HYP.pptrBase_def hd_conv_nth length_ineq_not_Nil)
apply (simp add: throwError_bind invocationCatch_def)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
@ -864,7 +864,7 @@ lemma decodeARMPageTableInvocation_ccorres:
apply (clarsimp | drule length_le_helper)+
apply (clarsimp simp: valid_cap'_def neq_Nil_conv
mask_add_aligned page_directory_at'_def
less_kernelBase_valid_pde_offset''
less_pptrBase_valid_pde_offset''
word_le_nat_alt[symmetric] table_bits_defs)
apply (auto simp: ct_in_state'_def pred_tcb_at' mask_def valid_tcb_state'_def
elim!: pred_tcb'_weakenE dest!: st_tcb_at_idle_thread')[1]
@ -1210,9 +1210,9 @@ lemma lookupPTSlot_le_0x3C:
apply clarsimp
apply simp
apply simp
apply (simp add: ARM_HYP.ptrFromPAddr_def physMappingOffset_def)
apply (simp add: ARM_HYP.ptrFromPAddr_def pptrBaseOffset_def)
apply (erule aligned_add_aligned)
apply (simp add: kernelBase_addr_def ARM_HYP.physBase_def
apply (simp add: pptrBase_def ARM_HYP.physBase_def
physBase_def is_aligned_def)
apply (simp add: word_bits_def)
done
@ -1473,16 +1473,16 @@ lemma obj_at_pte_aligned:
lemma addrFromPPtr_mask_5:
"addrFromPPtr ptr && mask (5::nat) = ptr && mask (5::nat)"
apply (simp add:addrFromPPtr_def physMappingOffset_def
kernelBase_addr_def physBase_def ARM_HYP.physBase_def)
apply (simp add:addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM_HYP.physBase_def)
apply word_bitwise
apply (simp add:mask_def)
done
lemma addrFromPPtr_mask_6:
"addrFromPPtr ptr && mask (6::nat) = ptr && mask (6::nat)"
apply (simp add:addrFromPPtr_def physMappingOffset_def
kernelBase_addr_def physBase_def ARM_HYP.physBase_def)
apply (simp add:addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM_HYP.physBase_def)
apply word_bitwise
apply (simp add:mask_def)
done
@ -1852,7 +1852,7 @@ lemma createMappingEntries_valid_pte_slots'2:
(* replay of proof in Arch_R with stronger validity result *)
lemma createMappingEntries_valid_pde_slots'2:
"\<lbrace>page_directory_at' pd and K (vmsz_aligned' vptr sz \<and> vptr < kernelBase \<and> vmsz_aligned' base sz)\<rbrace>
"\<lbrace>page_directory_at' pd and K (vmsz_aligned' vptr sz \<and> vptr < pptrBase \<and> vmsz_aligned' base sz)\<rbrace>
createMappingEntries base vptr sz vm_rights attrib pd
\<lbrace>\<lambda>rv. valid_pde_slots'2 rv\<rbrace>,-"
apply (simp add: createMappingEntries_def valid_pde_slots'2_def)
@ -1861,7 +1861,7 @@ lemma createMappingEntries_valid_pde_slots'2:
apply (clarsimp simp: page_directory_at'_def
lookup_pd_slot_eq[simplified pd_bits_def pde_bits_def])
apply (clarsimp simp: lookup_pd_slot_def Let_def mask_add_aligned table_bits_defs)
apply (rule conjI, erule less_kernelBase_valid_pde_offset'')
apply (rule conjI, erule less_pptrBase_valid_pde_offset'')
apply (rule conjI, subst vaddr_segment_nonsense6, assumption, blast)
apply (rule_tac x= 0 in exI)
apply (simp add: isSuperSectionPDE_def)
@ -1878,7 +1878,7 @@ lemma createMappingEntries_valid_pde_slots'2:
apply (clarsimp simp: superSectionPDEOffsets_def length_upto_enum_step table_bits_defs)
apply (clarsimp simp: upto_enum_step_def upto_enum_def comp_def)
apply (clarsimp simp: linorder_not_less field_simps mask_add_aligned)
apply (erule less_kernelBase_valid_pde_offset'[simplified table_bits_defs], simp+)
apply (erule less_pptrBase_valid_pde_offset'[simplified table_bits_defs], simp+)
apply (rule word_of_nat_le, simp)
done
apply (rule conjI)
@ -2176,14 +2176,14 @@ lemma vmsz_aligned_addrFromPPtr':
= vmsz_aligned' p sz"
apply (simp add: vmsz_aligned'_def addrFromPPtr_def
ARM_HYP.addrFromPPtr_def)
apply (subgoal_tac "is_aligned physMappingOffset (pageBitsForSize sz)")
apply (subgoal_tac "is_aligned pptrBaseOffset (pageBitsForSize sz)")
apply (rule iffI)
apply (drule(1) aligned_add_aligned)
apply (simp add: pageBitsForSize_def word_bits_def split: vmpage_size.split)
apply simp
apply (erule(1) aligned_sub_aligned)
apply (simp add: pageBitsForSize_def word_bits_def split: vmpage_size.split)
apply (simp add: pageBitsForSize_def physMappingOffset_def kernelBase_addr_def
apply (simp add: pageBitsForSize_def pptrBaseOffset_def pptrBase_def
physBase_def ARM_HYP.physBase_def is_aligned_def
split: vmpage_size.split)
done
@ -2568,7 +2568,7 @@ lemma throwError_invocationCatch:
lemma decodeARMFrameInvocation_ccorres:
notes if_cong[cong] tl_drop_1[simp]
defines "does_not_throw args extraCaps pg_sz mapdata \<equiv>
(mapdata = None \<longrightarrow> \<not> (ARM_HYP_H.kernelBase \<le> hd args + 2 ^ pageBitsForSize pg_sz - 1)) \<and>
(mapdata = None \<longrightarrow> \<not> (ARM_HYP_H.pptrBase \<le> hd args + 2 ^ pageBitsForSize pg_sz - 1)) \<and>
(mapdata \<noteq> None \<longrightarrow> (fst (the mapdata) = (the (capPDMappedASID (capCap (fst (extraCaps ! 0)))))
\<and> snd (the mapdata) = hd args))"
shows
@ -2694,7 +2694,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply (rule ccorres_if_cond_throws[rotated -1,where Q = \<top> and Q' = \<top>])
apply vcg
apply (clarsimp simp: paddrTop_def ARM_HYP.paddrTop_def pptrTop_def fromPAddr_def
physBase_def ARM_HYP.physBase_def ARM_HYP.kernelBase_def
physBase_def ARM_HYP.physBase_def ARM_HYP.pptrBase_def
hd_drop_conv_nth hd_conv_nth)
apply (clarsimp dest!: ccap_relation_PageCap_generics)
apply (simp add:injection_handler_throwError)
@ -2867,7 +2867,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)
(* frame cap not mapped, check mapping *)
(* disallow mappings above kernelBase *)
(* disallow mappings above pptrBase *)
apply clarsimp
apply (prop_tac "mapdata = None")
apply (simp add: ccap_relation_mapped_asid_0)
@ -2879,7 +2879,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply clarsimp
apply ccorres_rewrite
apply csymbr
apply (simp add: ARM_HYP_H.kernelBase_def ARM_HYP.kernelBase_def hd_conv_nth length_ineq_not_Nil)
apply (simp add: ARM_HYP_H.pptrBase_def ARM_HYP.pptrBase_def hd_conv_nth length_ineq_not_Nil)
apply ccorres_rewrite
apply (rule syscall_error_throwError_ccorres_n[unfolded id_def dc_def])
apply (simp add: syscall_error_to_H_cases)
@ -2904,7 +2904,7 @@ lemma decodeARMFrameInvocation_ccorres:
apply (rule ccorres_rhs_assoc)+
apply (csymbr, clarsimp, ccorres_rewrite)
apply (csymbr,
simp add: ARM_HYP_H.kernelBase_def ARM_HYP.kernelBase_def
simp add: ARM_HYP_H.pptrBase_def ARM_HYP.pptrBase_def
hd_conv_nth length_ineq_not_Nil,
ccorres_rewrite)
apply (fold dc_def)
@ -3073,7 +3073,7 @@ lemma decodeARMFrameInvocation_ccorres:
framesize_from_H_eq_eqs of_bool_nth[simplified of_bool_from_bool]
vm_page_size_defs neq_Nil_conv excaps_in_mem_def hd_conv_nth
length_ineq_not_Nil numeral_2_eq_2 does_not_throw_def
ARM_HYP_H.kernelBase_def ARM_HYP.kernelBase_def)
ARM_HYP_H.pptrBase_def ARM_HYP.pptrBase_def)
apply (frule interpret_excaps_eq[rule_format, where n=0], simp)
apply (frule(1) slotcap_in_mem_PageDirectory)
apply (clarsimp simp: mask_def[where n=4] typ_heap_simps' isCap_simps)
@ -3289,7 +3289,7 @@ lemma decodeARMPageDirectoryInvocation_ccorres:
apply (simp add: syscall_error_to_H_cases)
apply (rule ccorres_if_cond_throws[rotated -1, where Q=\<top> and Q'=\<top>])
apply vcg
apply (clarsimp simp: hd_conv_nth length_ineq_not_Nil kernelBase_def ARM_HYP.kernelBase_def)
apply (clarsimp simp: hd_conv_nth length_ineq_not_Nil pptrBase_def ARM_HYP.pptrBase_def)
apply (simp add:injection_handler_throwError)
apply (rule syscall_error_throwError_ccorres_n)
apply (simp add: syscall_error_to_H_cases)

8
proof/crefine/ARM_HYP/Finalise_C.thy
View File

@ -1434,7 +1434,7 @@ lemma pageTableMapped_pd:
done
lemma unmapPageTable_ccorres:
"ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask asid_bits \<and> vaddr < kernelBase))
"ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask asid_bits \<and> vaddr < pptrBase))
(UNIV \<inter> {s. asid_' s = asid} \<inter> {s. vaddr_' s = vaddr} \<inter> {s. pt_' s = Ptr ptPtr}) []
(unmapPageTable asid vaddr ptPtr) (Call unmapPageTable_'proc)"
apply (rule ccorres_gen_asm)
@ -1464,7 +1464,7 @@ lemma unmapPageTable_ccorres:
apply (rule_tac Q="\<lambda>rv s. (case rv of Some pd \<Rightarrow> page_directory_at' pd s | _ \<Rightarrow> True) \<and> invs' s"
in hoare_post_imp)
apply (clarsimp simp: lookup_pd_slot_def Let_def
mask_add_aligned less_kernelBase_valid_pde_offset''
mask_add_aligned less_pptrBase_valid_pde_offset''
page_directory_at'_def table_bits_defs)
apply (wp pageTableMapped_pd)
apply (clarsimp simp: word_sle_def lookup_pd_slot_def
@ -2258,7 +2258,7 @@ lemma capFSize_eq: "\<lbrakk>ccap_relation (capability.ArchObjectCap (arch_capab
apply (frule (1) cap_get_tag_isCap_unfolded_H_cap)
apply (clarsimp simp: cap_frame_cap_lift cap_to_H_def
case_option_over_if gen_framesize_to_H_def
ARM_HYP_H.kernelBase_def
ARM_HYP_H.pptrBase_def
framesize_to_H_def valid_cap'_def
elim!: ccap_relationE simp del: Collect_const)
apply (subgoal_tac "capFSize_CL (cap_frame_cap_lift cap) \<noteq> scast Kernel_C.ARMSmallPage")
@ -2583,7 +2583,7 @@ lemma Arch_finaliseCap_ccorres:
apply (subgoal_tac "capVPMappedAddress cp \<noteq> None")
apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def
case_option_over_if gen_framesize_to_H_def
Kernel_C.ARMSmallPage_def ARM_HYP_H.kernelBase_def
Kernel_C.ARMSmallPage_def ARM_HYP_H.pptrBase_def
if_split
elim!: ccap_relationE simp del: Collect_const)
apply (clarsimp simp: cap_small_frame_cap_lift cap_to_H_def

2
proof/crefine/ARM_HYP/Invoke_C.thy
View File

@ -1673,7 +1673,7 @@ lemma pspace_no_overlap_underlying_zero_update:
lemma addrFromPPtr_mask:
"n \<le> 28
\<Longrightarrow> addrFromPPtr ptr && mask n = ptr && mask n"
apply (simp add: addrFromPPtr_def physMappingOffset_def kernelBase_addr_def
apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def
ARM_HYP.physBase_def)
apply word_bitwise
apply simp

14
proof/crefine/ARM_HYP/VSpace_C.thy
View File

@ -781,8 +781,8 @@ lemma ptrFromPAddr_spec:
Call ptrFromPAddr_'proc
\<lbrace> \<acute>ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s) ) \<rbrace>"
apply vcg
apply (simp add: ARM_HYP.ptrFromPAddr_def physMappingOffset_def
kernelBase_addr_def physBase_def ARM_HYP.physBase_def)
apply (simp add: ARM_HYP.ptrFromPAddr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM_HYP.physBase_def)
done
lemma addrFromPPtr_spec:
@ -791,8 +791,8 @@ lemma addrFromPPtr_spec:
\<lbrace> \<acute>ret__unsigned_long = (addrFromPPtr (ptr_val (pptr_' s)) ) \<rbrace>"
apply vcg
apply (simp add: addrFromPPtr_def
ARM_HYP.addrFromPPtr_def physMappingOffset_def
kernelBase_addr_def physBase_def ARM_HYP.physBase_def)
ARM_HYP.addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM_HYP.physBase_def)
done
@ -2691,7 +2691,7 @@ lemma ccorres_seq_IF_False:
lemma ptrFromPAddr_mask6_simp[simp]:
"ptrFromPAddr ps && mask 6 = ps && mask 6"
unfolding ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def ARM_HYP.physBase_def
unfolding ptrFromPAddr_def pptrBaseOffset_def pptrBase_def ARM_HYP.physBase_def
by (subst add.commute, subst mask_add_aligned ; simp add: is_aligned_def)
lemma doFlush_ccorres:
@ -3319,7 +3319,7 @@ lemmas ccorres_move_array_assertion_pde_16
lemma unmapPage_ccorres:
"ccorres dc xfdc (invs' and (\<lambda>s. 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s)
and (\<lambda>_. asid \<le> mask asid_bits \<and> vmsz_aligned' vptr sz
\<and> vptr < kernelBase))
\<and> vptr < pptrBase))
(UNIV \<inter> {s. gen_framesize_to_H (page_size_' s) = sz \<and> page_size_' s < 4}
\<inter> {s. asid_' s = asid} \<inter> {s. vptr_' s = vptr} \<inter> {s. pptr_' s = Ptr pptr}) []
(unmapPage sz asid vptr pptr) (Call unmapPage_'proc)"
@ -3554,7 +3554,7 @@ lemma unmapPage_ccorres:
apply (simp add: vmsz_aligned'_def vmsz_aligned_def)
apply (clarsimp simp: lookup_pd_slot_def Let_def table_bits_defs
mask_add_aligned field_simps)
apply (erule less_kernelBase_valid_pde_offset' [simplified table_bits_defs])
apply (erule less_pptrBase_valid_pde_offset' [simplified table_bits_defs])
apply (simp add: vmsz_aligned'_def)
apply (simp add: word_le_nat_alt unat_of_nat)
apply (simp add: length_superSectionPDEOffsets)

16
proof/infoflow/Example_Valid_State.thy
View File

@ -907,8 +907,8 @@ lemma Sys1AgentMap_simps:
\<Longrightarrow> Sys1AgentMap p = partition_label Low"
unfolding Sys1AgentMap_def
apply simp_all
by (auto simp: ptrFromPAddr_def physMappingOffset_def
kernelBase_addr_def physBase_def s0_ptr_defs)
by (auto simp: ptrFromPAddr_def pptrBaseOffset_def
pptrBase_def physBase_def s0_ptr_defs)
definition
Sys1ASIDMap :: "(auth_graph_label subject_label) agent_asid_map"
@ -1034,7 +1034,7 @@ lemma Sys1_pas_refined:
apply (clarsimp simp: irq_map_wellformed_aux_def s0_internal_def Sys1AgentMap_simps Sys1PAS_def)
apply (clarsimp simp: Sys1AgentMap_def)
apply (clarsimp simp: ptrFromPAddr_def s0_ptr_defs cte_level_bits_def
physMappingOffset_def kernelBase_addr_def physBase_def)
pptrBaseOffset_def pptrBase_def physBase_def)
apply (drule le_less_trans[OF irq_node_offs_min[simplified s0_ptr_defs cte_level_bits_def, simplified]])
apply simp
apply (clarsimp simp: tcb_domain_map_wellformed_aux_def
@ -1069,14 +1069,14 @@ lemma Sys1_pas_refined:
apply (rule Sys1AgentMap_simps(13))
apply simp
apply (drule_tac x=ac in plus_one_helper2)
apply (simp add: ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def
shared_page_ptr_def kernel_base_def)
apply (simp add: add.commute)
apply (erule notE)
apply (rule Sys1AgentMap_simps(13)[symmetric])
apply simp
apply (drule_tac x=ac in plus_one_helper2)
apply (simp add: ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def
s0_ptr_defs)
apply (simp add: add.commute)
@ -1610,7 +1610,7 @@ lemma valid_arch_objs_s0[simp]:
apply (clarsimp simp: valid_vspace_objs_def obj_at_def s0_internal_def)
apply (drule kh0_SomeD)
apply (erule disjE | clarsimp simp: pageBits_def addrFromPPtr_def
physMappingOffset_def kernelBase_addr_def physBase_def is_aligned_def
pptrBaseOffset_def pptrBase_def physBase_def is_aligned_def
obj_at_def kh0_def kh0_obj_def kernel_mapping_slots_def
High_pt'_def Low_pt'_def High_pd'_def Low_pd'_def ptrFromPAddr_def
| erule vs_lookupE, force simp: vs_lookup_def arch_state0_def vs_asid_refs_def)+
@ -1637,7 +1637,7 @@ lemma valid_global_objs_s0[simp]:
"valid_global_objs s0_internal"
apply (clarsimp simp: valid_global_objs_def s0_internal_def arch_state0_def)
by (force simp: valid_vso_at_def obj_at_def kh0_def kh0_obj_def s0_ptr_defs
addrFromPPtr_def physMappingOffset_def kernelBase_addr_def
addrFromPPtr_def pptrBaseOffset_def pptrBase_def
physBase_def is_aligned_def pageBits_def
kernel_mapping_slots_def empty_table_def pde_ref_def
valid_pde_mappings_def)+
@ -1659,7 +1659,7 @@ lemma equal_kernel_mappings_s0[simp]:
apply (drule kh0_SomeD)+
by (erule disjE
| force simp: kh0_obj_def High_pd'_def Low_pd'_def s0_ptr_defs kernel_mapping_slots_def
addrFromPPtr_def physMappingOffset_def kernelBase_addr_def physBase_def)+
addrFromPPtr_def pptrBaseOffset_def pptrBase_def physBase_def)+
lemma valid_asid_map_s0[simp]:
"valid_asid_map s0_internal"

2
proof/infoflow/UserOp_IF.thy
View File

@ -429,7 +429,7 @@ lemma ptrFromPAddr_mask_simp:
"(ptrFromPAddr z && ~~ mask (pageBitsForSize l)) =
(ptrFromPAddr (z && ~~ mask (pageBitsForSize l)))"
apply (simp add: ptrFromPAddr_def field_simps)
apply (subst mask_out_add_aligned[OF is_aligned_physMappingOffset])
apply (subst mask_out_add_aligned[OF is_aligned_pptrBaseOffset])
apply simp
done

16
proof/infoflow/refine/Example_Valid_StateH.thy
View File

@ -2210,26 +2210,26 @@ lemma s0H_valid_objs':
split: if_split_asm)
apply (clarsimp simp: valid_obj'_def global_pdH'_def valid_mapping'_def s0_ptr_defs
is_aligned_def ARM.addrFromPPtr_def ARM.ptrFromPAddr_def
physMappingOffset_def ARM.kernelBase_def ARM.physBase_def
kernelBase_addr_def physBase_def
pptrBaseOffset_def ARM.pptrBase_def ARM.physBase_def
pptrBase_def physBase_def
split: if_split_asm)
apply (clarsimp simp: valid_obj'_def High_pdH_def High_pd'H_def valid_pde'_def pteBits_def
valid_mapping'_def s0_ptr_defs is_aligned_def ARM.addrFromPPtr_def
ARM.kernelBase_def ARM.physBase_def ARM.ptrFromPAddr_def ptBits_def
pageBits_def physMappingOffset_def kernelBase_addr_def physBase_def
ARM.pptrBase_def ARM.physBase_def ARM.ptrFromPAddr_def ptBits_def
pageBits_def pptrBaseOffset_def pptrBase_def physBase_def
split: if_split_asm)
apply (clarsimp simp: valid_obj'_def Low_pdH_def Low_pd'H_def valid_pde'_def valid_mapping'_def
s0_ptr_defs is_aligned_def ARM.addrFromPPtr_def pteBits_def
ARM.ptrFromPAddr_def ARM.physBase_def ptBits_def pageBits_def
physMappingOffset_def kernelBase_addr_def physBase_def
pptrBaseOffset_def pptrBase_def physBase_def
split: if_split_asm)
apply (clarsimp simp: valid_obj'_def High_ptH_def High_pt'H_def valid_mapping'_def s0_ptr_defs
is_aligned_def ARM.addrFromPPtr_def ARM.ptrFromPAddr_def ARM.kernelBase_def
ARM.physBase_def physMappingOffset_def kernelBase_addr_def physBase_def
is_aligned_def ARM.addrFromPPtr_def ARM.ptrFromPAddr_def ARM.pptrBase_def
ARM.physBase_def pptrBaseOffset_def pptrBase_def physBase_def
split: if_split_asm)
apply (clarsimp simp: valid_obj'_def Low_ptH_def Low_pt'H_def valid_mapping'_def s0_ptr_defs
is_aligned_def ARM.addrFromPPtr_def ARM.physBase_def ARM.ptrFromPAddr_def
physMappingOffset_def kernelBase_addr_def physBase_def
pptrBaseOffset_def pptrBase_def physBase_def
split: if_split_asm)
done

14
proof/invariant-abstract/ARM/ArchAInvsPre.thy
View File

@ -100,7 +100,7 @@ lemma get_pd_of_thread_reachable:
lemma is_aligned_ptrFromPAddrD:
"\<lbrakk>is_aligned (ptrFromPAddr b) a; a \<le> 24\<rbrakk> \<Longrightarrow> is_aligned b a"
apply (clarsimp simp: ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def)
apply (clarsimp simp: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def)
apply (erule is_aligned_addD2)
apply (rule is_aligned_weaken[where x = 24])
apply (simp add: is_aligned_def)
@ -188,10 +188,10 @@ lemma device_frame_in_device_region:
\<Longrightarrow> device_state (machine_state s) p \<noteq> None"
by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def)
lemma is_aligned_physMappingOffset:
"is_aligned physMappingOffset (pageBitsForSize sz)"
by (case_tac sz, simp_all add: physMappingOffset_def
kernelBase_addr_def physBase_def is_aligned_def)[1]
lemma is_aligned_pptrBaseOffset:
"is_aligned pptrBaseOffset (pageBitsForSize sz)"
by (case_tac sz, simp_all add: pptrBaseOffset_def
pptrBase_def physBase_def is_aligned_def)[1]
global_naming Arch
named_theorems AInvsPre_asms
@ -230,7 +230,7 @@ lemma (* ptable_rights_imp_frame *)[AInvsPre_asms]:
apply (rule_tac x=sz in exI)
apply (drule_tac x = sz in spec)
apply (subst add.assoc[symmetric])
apply (frule is_aligned_add_helper[OF aligned_add_aligned[OF _ is_aligned_physMappingOffset]])
apply (frule is_aligned_add_helper[OF aligned_add_aligned[OF _ is_aligned_pptrBaseOffset]])
apply (rule le_refl)
apply (rule_tac w = x in and_mask_less')
apply (case_tac sz, simp_all add: word_bits_conv)[1]
@ -248,5 +248,5 @@ requalify_facts
ARM.user_mem_dom_cong
ARM.device_mem_dom_cong
ARM.device_frame_in_device_region
ARM.is_aligned_physMappingOffset
ARM.is_aligned_pptrBaseOffset
end

8
proof/invariant-abstract/ARM/ArchAcc_AI.thy
View File

@ -2590,8 +2590,8 @@ lemma is_aligned_addrFromPPtr_n:
"\<lbrakk> is_aligned p n; n \<le> 28 \<rbrakk> \<Longrightarrow> is_aligned (Platform.ARM.addrFromPPtr p) n"
apply (simp add: Platform.ARM.addrFromPPtr_def)
apply (erule aligned_sub_aligned, simp_all)
apply (simp add: physMappingOffset_def physBase_def
kernelBase_addr_def pageBits_def)
apply (simp add: pptrBaseOffset_def physBase_def
pptrBase_def pageBits_def)
apply (erule is_aligned_weaken[rotated])
apply (simp add: is_aligned_def)
done
@ -2603,8 +2603,8 @@ lemma is_aligned_addrFromPPtr:
lemma is_aligned_ptrFromPAddr_n:
"\<lbrakk>is_aligned x sz; sz\<le> 28\<rbrakk>
\<Longrightarrow> is_aligned (ptrFromPAddr x) sz"
apply (simp add:ptrFromPAddr_def physMappingOffset_def
kernelBase_addr_def physBase_def)
apply (simp add:ptrFromPAddr_def pptrBaseOffset_def
pptrBase_def physBase_def)
apply (erule aligned_add_aligned)
apply (erule is_aligned_weaken[rotated])
apply (simp add:is_aligned_def)

4
proof/invariant-abstract/ARM/ArchKernelInit_AI.thy
View File

@ -363,8 +363,8 @@ lemma invs_A:
apply (clarsimp simp: valid_ao_at_def obj_at_def empty_table_def pde_ref_def
valid_pde_mappings_def valid_vso_at_def)
apply (simp add: kernel_base_def kernel_mapping_slots_def
Platform.ARM.addrFromPPtr_def physMappingOffset_def
kernelBase_addr_def physBase_def pageBits_def is_aligned_def)
Platform.ARM.addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def pageBits_def is_aligned_def)
apply (rule conjI)
apply (simp add: valid_kernel_mappings_def state_defs
valid_kernel_mappings_if_pd_def pde_ref_def

14
proof/invariant-abstract/ARM_HYP/ArchAInvsPre.thy
View File

@ -21,7 +21,7 @@ lemma get_pd_of_thread_reachable:
lemma is_aligned_ptrFromPAddrD:
"\<lbrakk>is_aligned (ptrFromPAddr b) a; a \<le> 25\<rbrakk> \<Longrightarrow> is_aligned b a"
apply (clarsimp simp: ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def physBase_def)
apply (clarsimp simp: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def)
apply (erule is_aligned_addD2)
apply (rule is_aligned_weaken[where x = 25])
apply (simp add: is_aligned_def)
@ -108,10 +108,10 @@ lemma device_frame_in_device_region:
\<Longrightarrow> device_state (machine_state s) p \<noteq> None"
by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def)
lemma is_aligned_physMappingOffset:
"is_aligned physMappingOffset (pageBitsForSize sz)"
by (case_tac sz, simp_all add: physMappingOffset_def
kernelBase_addr_def physBase_def is_aligned_def)[1]
lemma is_aligned_pptrBaseOffset:
"is_aligned pptrBaseOffset (pageBitsForSize sz)"
by (case_tac sz, simp_all add: pptrBaseOffset_def
pptrBase_def physBase_def is_aligned_def)[1]
global_naming Arch
named_theorems AInvsPre_asms
@ -143,7 +143,7 @@ lemma (* ptable_rights_imp_frame *)[AInvsPre_asms]:
apply (rule_tac x=sz in exI)
apply (drule_tac x = sz in spec)
apply (subst add.assoc[symmetric])
apply (frule is_aligned_add_helper[OF aligned_add_aligned[OF _ is_aligned_physMappingOffset]])
apply (frule is_aligned_add_helper[OF aligned_add_aligned[OF _ is_aligned_pptrBaseOffset]])
apply (rule le_refl)
apply (rule_tac w = x in and_mask_less')
apply (case_tac sz, simp_all add: word_bits_conv)[1]
@ -161,5 +161,5 @@ requalify_facts
ARM_HYP.user_mem_dom_cong
ARM_HYP.device_mem_dom_cong
ARM_HYP.device_frame_in_device_region
ARM_HYP.is_aligned_physMappingOffset
ARM_HYP.is_aligned_pptrBaseOffset
end

8
proof/invariant-abstract/ARM_HYP/ArchAcc_AI.thy
View File

@ -2561,8 +2561,8 @@ lemma is_aligned_addrFromPPtr_n:
"\<lbrakk> is_aligned p n; n \<le> 28 \<rbrakk> \<Longrightarrow> is_aligned (Platform.ARM_HYP.addrFromPPtr p) n"
apply (simp add: Platform.ARM_HYP.addrFromPPtr_def)
apply (erule aligned_sub_aligned, simp_all)
apply (simp add: physMappingOffset_def physBase_def
kernelBase_addr_def pageBits_def)
apply (simp add: pptrBaseOffset_def physBase_def
pptrBase_def pageBits_def)
apply (erule is_aligned_weaken[rotated])
apply (simp add: is_aligned_def)
done
@ -2574,8 +2574,8 @@ lemma is_aligned_addrFromPPtr:
lemma is_aligned_ptrFromPAddr_n:
"\<lbrakk>is_aligned x sz; sz\<le> 28\<rbrakk>
\<Longrightarrow> is_aligned (ptrFromPAddr x) sz"
apply (simp add:ptrFromPAddr_def physMappingOffset_def
kernelBase_addr_def physBase_def)
apply (simp add:ptrFromPAddr_def pptrBaseOffset_def
pptrBase_def physBase_def)
apply (erule aligned_add_aligned)
apply (erule is_aligned_weaken[rotated])
apply (simp add:is_aligned_def)

4
proof/refine/ARM/ArchAcc_R.thy
View File

@ -946,10 +946,10 @@ lemma page_table_at_state_relation:
apply (drule_tac x = "ucast y" in spec)
apply (drule sym[where s = "pspace_dom (kheap s)"])
apply (clarsimp simp:typ_at'_def ko_wp_at'_def)
apply (subgoal_tac "(ptr + physMappingOffset + (y << 2)) \<in> dom (ksPSpace sa)")
apply (subgoal_tac "(ptr + pptrBaseOffset + (y << 2)) \<in> dom (ksPSpace sa)")
prefer 2
apply (clarsimp simp: pspace_dom_def)
apply (rule_tac x = "ptr + physMappingOffset" in bexI[where A = "dom (kheap s)"])
apply (rule_tac x = "ptr + pptrBaseOffset" in bexI[where A = "dom (kheap s)"])
apply (simp add:image_def)
apply (rule_tac x = "ucast y" in exI)
apply (simp add:ucast_ucast_len)

30
proof/refine/ARM/Arch_R.thy
View File

@ -969,12 +969,12 @@ shows
apply (rule_tac P="map_data = None \<and> kernel_base \<le> vaddr + 2 ^ pageBitsForSize vmpage_size - 1
\<or> (\<exists>asid' vaddr'. map_data = Some (asid', vaddr') \<and> (asid',vaddr') \<noteq> (asid,vaddr))"
in corres_symmetric_bool_cases[where Q=\<top> and Q'=\<top>, OF refl])
apply (erule disjE; clarsimp simp: whenE_def kernel_base_def kernelBase_def ARM.kernelBase_def
apply (erule disjE; clarsimp simp: whenE_def kernel_base_def pptrBase_def ARM.pptrBase_def
split: option.splits)
apply clarsimp
apply (rule corres_splitEE'[where r'=dc and P=\<top> and P'=\<top>])
apply (case_tac map_data
; clarsimp simp: whenE_def kernel_base_def kernelBase_def ARM.kernelBase_def
; clarsimp simp: whenE_def kernel_base_def pptrBase_def ARM.pptrBase_def
corres_returnOkTT)
\<comment> \<open>pd=undefined as vspace_at_asid not used in find_pd_for_asid_corres and avoid unresolved schematics\<close>
apply (rule corres_splitEE'[
@ -1030,7 +1030,7 @@ shows
apply (simp split: cap.split arch_cap.split option.split,
intro conjI allI impI, simp_all)[1]
apply (rule whenE_throwError_corres_initial, simp)
apply (simp add: kernel_base_def ARM.kernelBase_def kernelBase_def)
apply (simp add: kernel_base_def ARM.pptrBase_def pptrBase_def)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
@ -1099,7 +1099,7 @@ shows
apply (rule whenE_throwError_corres, simp)
apply clarsimp
apply (rule whenE_throwError_corres, simp)
apply (clarsimp simp: kernel_base_def ARM.kernelBase_def kernelBase_def)
apply (clarsimp simp: kernel_base_def ARM.pptrBase_def pptrBase_def)
apply (rule case_option_corresE)
apply (rule corres_trivial)
apply clarsimp
@ -1341,10 +1341,10 @@ lemma sts_valid_arch_inv':
apply simp
done
lemma less_kernelBase_valid_pde_offset':
"\<lbrakk> vptr < kernelBase; x = 0 \<or> is_aligned vptr 24; x \<le> 0xF \<rbrakk>
lemma less_pptrBase_valid_pde_offset':
"\<lbrakk> vptr < pptrBase; x = 0 \<or> is_aligned vptr 24; x \<le> 0xF \<rbrakk>
\<Longrightarrow> valid_pde_mapping_offset' (((x * 4) + (vptr >> 20 << 2)) && mask pdBits)"
apply (clarsimp simp: ARM.kernelBase_def kernelBase_def pdBits_def pageBits_def
apply (clarsimp simp: ARM.pptrBase_def pptrBase_def pdBits_def pageBits_def
valid_pde_mapping_offset'_def pd_asid_slot_def)
apply (drule word_le_minus_one_leq, simp add: pdeBits_def)
apply (drule le_shiftr[where u=vptr and n=20])
@ -1362,19 +1362,19 @@ lemma less_kernelBase_valid_pde_offset':
apply (simp add: shiftl_t2n unat_arith_simps iffD1[OF unat_mult_lem])
done
lemmas less_kernelBase_valid_pde_offset''
= less_kernelBase_valid_pde_offset'[where x=0, simplified]
lemmas less_pptrBase_valid_pde_offset''
= less_pptrBase_valid_pde_offset'[where x=0, simplified]
lemma createMappingEntries_valid_pde_slots':
"\<lbrace>K (vmsz_aligned' vptr sz \<and> is_aligned pd pdBits
\<and> vptr < kernelBase)\<rbrace>
\<and> vptr < pptrBase)\<rbrace>
createMappingEntries base vptr sz vm_rights attrib pd
\<lbrace>\<lambda>rv s. valid_pde_slots' rv\<rbrace>,-"
apply (simp add: createMappingEntries_def valid_pde_slots'_def)
apply (cases sz, simp_all)
apply (wp | simp)+
apply (clarsimp simp: lookup_pd_slot_def Let_def mask_add_aligned)
apply (erule less_kernelBase_valid_pde_offset'')
apply (erule less_pptrBase_valid_pde_offset'')
apply (rule hoare_pre, wp)
apply (clarsimp simp: vmsz_aligned'_def superSectionPDEOffsets_def pdeBits_def del: ballI)
apply (subst p_0x3C_shift[symmetric])
@ -1387,7 +1387,7 @@ lemma createMappingEntries_valid_pde_slots':
apply (clarsimp simp: upto_enum_step_def linorder_not_less pd_bits_def
lookup_pd_slot_def Let_def field_simps
mask_add_aligned pdeBits_def)
apply (erule less_kernelBase_valid_pde_offset'
apply (erule less_pptrBase_valid_pde_offset'
[unfolded pdBits_def pageBits_def pdeBits_def, simplified], simp+)
done
@ -1412,12 +1412,12 @@ lemma findPDForASID_aligned[wp]:
done
lemma findPDForASID_valid_offset'[wp]:
"\<lbrace>valid_objs' and K (vptr < kernelBase)\<rbrace> findPDForASID p
"\<lbrace>valid_objs' and K (vptr < pptrBase)\<rbrace> findPDForASID p
\<lbrace>\<lambda>rv s. valid_pde_mapping_offset' (rv + (vptr >> 20 << 2) && mask pdBits)\<rbrace>,-"
apply (rule hoare_gen_asmE)
apply (rule hoare_post_imp_R, rule findPDForASID_aligned)
apply (simp add: mask_add_aligned)
apply (erule less_kernelBase_valid_pde_offset'')
apply (erule less_pptrBase_valid_pde_offset'')
done
lemma eq_arch_update':
@ -1523,7 +1523,7 @@ lemma ensureSafeMapping_valid_slots_duplicated':
lemma is_aligned_ptrFromPAddr_aligned:
"m \<le> 28 \<Longrightarrow> is_aligned (ptrFromPAddr p) m = is_aligned p m"
apply (simp add:ptrFromPAddr_def is_aligned_mask
physMappingOffset_def kernelBase_addr_def ARM.physBase_def physBase_def)
pptrBaseOffset_def pptrBase_def ARM.physBase_def physBase_def)
apply (subst add.commute)
apply (subst mask_add_aligned)
apply (erule is_aligned_weaken[rotated])

4
proof/refine/ARM/Invariants_H.thy
View File

@ -417,11 +417,11 @@ where valid_cap'_def:
(\<forall>p < 2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT)
(ref + p * 2 ^ pageBits) s) \<and>
(case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow>
0 < asid \<and> asid \<le> 2 ^ asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < kernelBase)
0 < asid \<and> asid \<le> 2 ^ asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase)
| PageTableCap ref mapdata \<Rightarrow>
page_table_at' ref s \<and>
(case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow>
0 < asid \<and> asid \<le> 2^asid_bits - 1 \<and> ref < kernelBase)
0 < asid \<and> asid \<le> 2^asid_bits - 1 \<and> ref < pptrBase)
| PageDirectoryCap ref mapdata \<Rightarrow>
page_directory_at' ref s \<and>
case_option True (\<lambda>asid. 0 < asid \<and> asid \<le> 2^asid_bits - 1) mapdata))"

54
proof/refine/ARM/PageTableDuplicates.thy
View File

@ -503,7 +503,7 @@ lemma is_aligned_le_mask:
lemma global_pd_offset:
"\<lbrakk>is_aligned ptr pdBits ; x \<in> {ptr + (kernelBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}\<rbrakk>
"\<lbrakk>is_aligned ptr pdBits ; x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}\<rbrakk>
\<Longrightarrow> ptr + (x && mask pdBits) = x"
apply (rule mask_eqI[where n = pdBits])
apply (simp add:mask_add_aligned mask_twice pdBits_def pageBits_def)
@ -515,17 +515,17 @@ lemma global_pd_offset:
apply (simp add:field_simps)
apply (frule_tac d1 = "0x3FFF" and p1="ptr" in is_aligned_add_helper[THEN conjunct2])
apply simp
apply (frule_tac d1 = "kernelBase >> 20 << 2" and p1 = "ptr"
apply (frule_tac d1 = "pptrBase >> 20 << 2" and p1 = "ptr"
in is_aligned_add_helper[THEN conjunct2])
apply (simp add: ARM.kernelBase_def kernelBase_def)
apply (simp add: ARM.pptrBase_def pptrBase_def)
apply simp
done
lemma globalPDEWindow_neg_mask:
"\<lbrakk>x && ~~ mask (vs_ptr_align a) = y && ~~ mask (vs_ptr_align a);is_aligned ptr pdBits\<rbrakk>
\<Longrightarrow> y \<in> {ptr + (kernelBase >> 20 << 2)..ptr + (2 ^ (pdBits) - 1)}
\<Longrightarrow> x \<in> {ptr + (kernelBase >> 20 << 2)..ptr + (2 ^ (pdBits) - 1)}"
apply (clarsimp simp:kernelBase_def ARM.kernelBase_def)
\<Longrightarrow> y \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ (pdBits) - 1)}
\<Longrightarrow> x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ (pdBits) - 1)}"
apply (clarsimp simp:pptrBase_def ARM.pptrBase_def)
apply (intro conjI)
apply (rule_tac y = "y &&~~ mask (vs_ptr_align a)" in order_trans)
apply (rule is_aligned_le_mask)
@ -569,7 +569,7 @@ lemma copyGlobalMappings_ksPSpace_stable:
"\<lbrace>\<lambda>s. ksPSpace s x = ko \<and> pspace_distinct' s \<and> pspace_aligned' s \<and>
is_aligned (armKSGlobalPD (ksArchState s)) pdBits\<rbrace>
copyGlobalMappings ptr
\<lbrace>\<lambda>_ s. ksPSpace s x = (if x \<in> {ptr + (kernelBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}
\<lbrace>\<lambda>_ s. ksPSpace s x = (if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}
then ksPSpace s ((armKSGlobalPD (ksArchState s)) + (x && mask pdBits))
else ko)\<rbrace>"
proof -
@ -598,8 +598,8 @@ lemma copyGlobalMappings_ksPSpace_stable:
apply simp
done
have postfix_listD:
"\<And>a as. suffix (a # as) [kernelBase >> 20.e.2 ^ (pdBits - 2) - 1]
\<Longrightarrow> a \<in> set [kernelBase >> 20 .e. 2 ^ (pdBits - 2) - 1]"
"\<And>a as. suffix (a # as) [pptrBase >> 20.e.2 ^ (pdBits - 2) - 1]
\<Longrightarrow> a \<in> set [pptrBase >> 20 .e. 2 ^ (pdBits - 2) - 1]"
apply (clarsimp simp:suffix_def)
apply (subgoal_tac "a \<in> set (zs @ a # as)")
apply (drule sym)
@ -607,12 +607,12 @@ lemma copyGlobalMappings_ksPSpace_stable:
apply simp
done
have in_rangeD: "\<And>x.
\<lbrakk>kernelBase >> 20 \<le> x; x \<le> 2 ^ (pdBits - 2) - 1\<rbrakk>
\<Longrightarrow> ptr + (x << 2) \<in> {ptr + (kernelBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}"
\<lbrakk>pptrBase >> 20 \<le> x; x \<le> 2 ^ (pdBits - 2) - 1\<rbrakk>
\<Longrightarrow> ptr + (x << 2) \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}"
apply (clarsimp simp:blah)
apply (intro conjI)
apply (rule word_plus_mono_right)
apply (simp add:ARM.kernelBase_def kernelBase_def pdBits_def pageBits_def pdeBits_def)
apply (simp add:ARM.pptrBase_def pptrBase_def pdBits_def pageBits_def pdeBits_def)
apply (word_bitwise,simp)
apply (rule is_aligned_no_wrap'[OF ptr_al])
apply (simp add:pdBits_def pageBits_def pdeBits_def)
@ -625,9 +625,9 @@ lemma copyGlobalMappings_ksPSpace_stable:
done
have offset_bound:
"\<And>x. \<lbrakk>is_aligned ptr 14;ptr + (kernelBase >> 20 << 2) \<le> x; x \<le> ptr + 0x3FFF\<rbrakk>
"\<And>x. \<lbrakk>is_aligned ptr 14;ptr + (pptrBase >> 20 << 2) \<le> x; x \<le> ptr + 0x3FFF\<rbrakk>
\<Longrightarrow> x - ptr < 0x4000"
apply (clarsimp simp: ARM.kernelBase_def kernelBase_def field_simps)
apply (clarsimp simp: ARM.pptrBase_def pptrBase_def field_simps)
apply unat_arith
done
@ -657,7 +657,7 @@ lemma copyGlobalMappings_ksPSpace_stable:
apply (rule hoare_pre)
apply (rule hoare_vcg_const_imp_lift)
apply wp
apply (rule_tac V="\<lambda>xs s. \<forall>x \<in> (set [kernelBase >> 20.e.2 ^ (pdBits - 2) - 1] - set xs).
apply (rule_tac V="\<lambda>xs s. \<forall>x \<in> (set [pptrBase >> 20.e.2 ^ (pdBits - 2) - 1] - set xs).
ksPSpace s (ptr + (x << 2)) = ksPSpace s (globalPD + (x << 2))"
and I="\<lambda>s'. globalPD = (armKSGlobalPD (ksArchState s'))
\<and> globalPD = (armKSGlobalPD (ksArchState s))"
@ -669,12 +669,12 @@ lemma copyGlobalMappings_ksPSpace_stable:
apply simp+
apply (erule impE)
apply (rule conjI)
apply (rule le_shiftr[where u="kernelBase >> 18" and n=2, simplified shiftr_shiftr, simplified])
apply (rule word_le_minus_mono_left[where x=ptr and y="(kernelBase >> 18) + ptr", simplified])
apply (simp add: ARM.kernelBase_def kernelBase_def field_simps)
apply (rule le_shiftr[where u="pptrBase >> 18" and n=2, simplified shiftr_shiftr, simplified])
apply (rule word_le_minus_mono_left[where x=ptr and y="(pptrBase >> 18) + ptr", simplified])
apply (simp add: ARM.pptrBase_def pptrBase_def field_simps)
apply (simp add:field_simps)
apply (erule is_aligned_no_wrap')
apply (simp add: ARM.kernelBase_def kernelBase_def pdBits_def pageBits_def)
apply (simp add: ARM.pptrBase_def pptrBase_def pdBits_def pageBits_def)
apply (drule le_m1_iff_lt[THEN iffD1,THEN iffD2,rotated])
apply simp
apply (drule le_shiftr[where u = "x - ptr" and n = 2])
@ -781,13 +781,13 @@ lemma copyGlobalMappings_ksPSpace_concrete:
and al: "is_aligned (armKSGlobalPD (ksArchState s)) pdBits"
"is_aligned ptr pdBits"
shows "ksPSpace s' = (\<lambda>x.
(if x \<in> {ptr + (kernelBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}
(if x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + (2 ^ pdBits - 1)}
then ksPSpace s ((x && mask pdBits) + armKSGlobalPD (ksArchState s)) else ksPSpace s x))"
proof -
have pd: "\<And>pd. \<lbrace>\<lambda>s. armKSGlobalPD (ksArchState s) = pd \<rbrace>
copyGlobalMappings ptr \<lbrace>\<lambda>r s. armKSGlobalPD (ksArchState s) = pd \<rbrace>"
by wp
have comp: "\<And>x. x \<in> {ptr + (kernelBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}
have comp: "\<And>x. x \<in> {ptr + (pptrBase >> 20 << 2)..ptr + 2 ^ pdBits - 1}
\<Longrightarrow> ptr + (x && mask pdBits) = x"
using al
apply -
@ -801,9 +801,9 @@ lemma copyGlobalMappings_ksPSpace_concrete:
apply (simp add:field_simps pdeBits_def)
apply (frule_tac d1 = "0x3FFF" and p1="ptr" in is_aligned_add_helper[THEN conjunct2])
apply simp
apply (frule_tac d1 = "kernelBase >> 20 << 2" and p1 = "ptr"
apply (frule_tac d1 = "pptrBase >> 20 << 2" and p1 = "ptr"
in is_aligned_add_helper[THEN conjunct2])
apply (simp add:ARM.kernelBase_def kernelBase_def)
apply (simp add:ARM.pptrBase_def pptrBase_def)
apply simp
done
@ -829,14 +829,14 @@ lemma copyGlobalMappings_ksPSpace_concrete:
apply (simp add:mask_def pdeBits_def)
apply (rule le_less_trans[OF word_and_le1])
apply simp
apply (frule_tac d1 = "kernelBase >> 20 << 2" in is_aligned_add_helper[THEN conjunct2])
apply (simp add:ARM.kernelBase_def kernelBase_def)
apply (frule_tac d1 = "pptrBase >> 20 << 2" in is_aligned_add_helper[THEN conjunct2])
apply (simp add:ARM.pptrBase_def pptrBase_def)
apply (simp add:field_simps pdeBits_def)
apply (frule_tac d1 = "0x3FFF" and p1="ptr" in is_aligned_add_helper[THEN conjunct2])
apply (simp add: pdeBits_def)
apply (frule_tac d1 = "kernelBase >> 20 << 2" and p1 = "ptr"
apply (frule_tac d1 = "pptrBase >> 20 << 2" and p1 = "ptr"
in is_aligned_add_helper[THEN conjunct2])
apply (simp add:ARM.kernelBase_def kernelBase_def pdeBits_def)
apply (simp add:ARM.pptrBase_def pptrBase_def pdeBits_def)
apply (simp add: pdeBits_def)
apply (cut_tac copyGlobalMappings_ksPSpace_sameD)
apply simp

2
proof/refine/ARM/Retype_R.thy
View File

@ -2556,7 +2556,7 @@ lemma copy_global_corres:
apply (drule(1) pde_relation_aligned_eq)
apply fastforce
apply (wp hoare_vcg_const_Ball_lift | simp)+
apply (simp add: kernel_base_def ARM.kernelBase_def kernelBase_def list_all2_refl pageBits_def)
apply (simp add: kernel_base_def ARM.pptrBase_def pptrBase_def list_all2_refl pageBits_def)
apply (rule corres_trivial, clarsimp simp: state_relation_def arch_state_relation_def)
apply wp+
apply (clarsimp simp: valid_arch_state_def)

4
proof/refine/ARM_HYP/ArchAcc_R.thy
View File

@ -1125,10 +1125,10 @@ lemma page_table_at_state_relation:
apply (drule_tac x = "ucast y" in spec)
apply (drule sym[where s = "pspace_dom (kheap s)"])
apply (clarsimp simp:typ_at'_def ko_wp_at'_def)
apply (subgoal_tac "(ptr + physMappingOffset + (y << 3)) \<in> dom (ksPSpace sa)")
apply (subgoal_tac "(ptr + pptrBaseOffset + (y << 3)) \<in> dom (ksPSpace sa)")
prefer 2
apply (clarsimp simp: pspace_dom_def)
apply (rule_tac x = "ptr + physMappingOffset" in bexI[where A = "dom (kheap s)"])
apply (rule_tac x = "ptr + pptrBaseOffset" in bexI[where A = "dom (kheap s)"])
apply (simp add:image_def pte_bits_def)
apply (rule_tac x = "ucast y" in exI)
apply (simp add:ucast_ucast_len)

30
proof/refine/ARM_HYP/Arch_R.thy
View File

@ -1082,12 +1082,12 @@ shows
\<or> (\<exists>asid' vaddr'. map_data = Some (asid', vaddr') \<and> (asid',vaddr') \<noteq> (asid,vaddr))"
in corres_symmetric_bool_cases[where Q=\<top> and Q'=\<top>, OF refl])
apply (erule disjE
; clarsimp simp: whenE_def kernel_base_def kernelBase_def ARM_HYP.kernelBase_def
; clarsimp simp: whenE_def kernel_base_def pptrBase_def ARM_HYP.pptrBase_def
split: option.splits)
apply clarsimp
apply (rule corres_splitEE'[where r'=dc and P=\<top> and P'=\<top>])
apply (case_tac map_data
; clarsimp simp: whenE_def kernel_base_def kernelBase_def ARM_HYP.kernelBase_def
; clarsimp simp: whenE_def kernel_base_def pptrBase_def ARM_HYP.pptrBase_def
corres_returnOkTT)
\<comment> \<open>pd=undefined as vspace_at_asid not used in find_pd_for_asid_corres and avoid unresolved schematics\<close>
apply (rule corres_splitEE'[
@ -1143,7 +1143,7 @@ shows
apply (simp split: cap.split arch_cap.split option.split,
intro conjI allI impI, simp_all)[1]
apply (rule whenE_throwError_corres_initial, simp)
apply (simp add: kernel_base_def ARM_HYP.kernelBase_def kernelBase_def)
apply (simp add: kernel_base_def ARM_HYP.pptrBase_def pptrBase_def)
apply (rule corres_guard_imp)
apply (rule corres_splitEE)
prefer 2
@ -1210,7 +1210,7 @@ shows
apply (rule whenE_throwError_corres, simp)
apply clarsimp
apply (rule whenE_throwError_corres, simp)
apply (clarsimp simp: kernel_base_def ARM_HYP.kernelBase_def kernelBase_def)
apply (clarsimp simp: kernel_base_def ARM_HYP.pptrBase_def pptrBase_def)
apply (rule case_option_corresE)
apply (rule corres_trivial)
apply clarsimp
@ -1559,10 +1559,10 @@ lemma sts_valid_arch_inv':
apply (case_tac vcpui; wpsimp simp: valid_vcpuinv'_def)
done
lemma less_kernelBase_valid_pde_offset':
"\<lbrakk> vptr < kernelBase; x = 0 \<or> is_aligned vptr 25; x \<le> 0x0F \<rbrakk>
lemma less_pptrBase_valid_pde_offset':
"\<lbrakk> vptr < pptrBase; x = 0 \<or> is_aligned vptr 25; x \<le> 0x0F \<rbrakk>
\<Longrightarrow> valid_pde_mapping_offset' (((x * 8) + (vptr >> 21 << 3)) && mask pdBits)"
apply (clarsimp simp: ARM_HYP.kernelBase_def kernelBase_def pdBits_def pageBits_def
apply (clarsimp simp: ARM_HYP.pptrBase_def pptrBase_def pdBits_def pageBits_def
valid_pde_mapping_offset'_def pd_asid_slot_def pt_index_bits_def
vspace_bits_defs)
apply (drule word_le_minus_one_leq, simp)
@ -1581,26 +1581,26 @@ lemma less_kernelBase_valid_pde_offset':
apply (simp add: shiftl_t2n unat_arith_simps iffD1[OF unat_mult_lem])
done
lemmas less_kernelBase_valid_pde_offset''
= less_kernelBase_valid_pde_offset'[where x=0, simplified pd_bits_def pdBits_def pdeBits_def, simplified]
lemmas less_pptrBase_valid_pde_offset''
= less_pptrBase_valid_pde_offset'[where x=0, simplified pd_bits_def pdBits_def pdeBits_def, simplified]
lemma createMappingEntries_valid_pde_slots':
"\<lbrace>K (vmsz_aligned' vptr sz \<and> is_aligned pd pdBits
\<and> vptr < kernelBase)\<rbrace>
\<and> vptr < pptrBase)\<rbrace>
createMappingEntries base vptr sz vm_rights attrib pd
\<lbrace>\<lambda>rv s. valid_pde_slots' rv\<rbrace>,-"
apply (simp add: createMappingEntries_def valid_pde_slots'_def)
apply (cases sz, simp_all)
apply (wp | simp)+
apply (clarsimp simp: lookup_pd_slot_def Let_def mask_add_aligned vspace_bits_defs)
apply (erule less_kernelBase_valid_pde_offset'')
apply (erule less_pptrBase_valid_pde_offset'')
apply (rule hoare_pre, wp)
apply (clarsimp simp: vmsz_aligned'_def superSectionPDEOffsets_def vspace_bits_defs del: ballI)
apply (simp add: lookup_pd_slot_def Let_def vspace_bits_defs)
apply (clarsimp simp: upto_enum_step_def linorder_not_less pd_bits_def
lookup_pd_slot_def Let_def field_simps
mask_add_aligned)
apply (erule less_kernelBase_valid_pde_offset' [simplified pdBits_def pdeBits_def, simplified])
apply (erule less_pptrBase_valid_pde_offset' [simplified pdBits_def pdeBits_def, simplified])
apply simp
apply simp
done
@ -1626,12 +1626,12 @@ lemma findPDForASID_aligned[wp]:
done
lemma findPDForASID_valid_offset'[wp]:
"\<lbrace>valid_objs' and K (vptr < kernelBase)\<rbrace> findPDForASID p
"\<lbrace>valid_objs' and K (vptr < pptrBase)\<rbrace> findPDForASID p
\<lbrace>\<lambda>rv s. valid_pde_mapping_offset' (rv + (vptr >> 21 << 3) && mask pd_bits)\<rbrace>,-"
apply (rule hoare_gen_asmE)
apply (rule hoare_post_imp_R, rule findPDForASID_aligned)
apply (simp add: mask_add_aligned vspace_bits_defs)
apply (erule less_kernelBase_valid_pde_offset'')
apply (erule less_pptrBase_valid_pde_offset'')
done
lemma eq_arch_update':
@ -1735,7 +1735,7 @@ lemma ensureSafeMapping_valid_slots_duplicated':
lemma is_aligned_ptrFromPAddr_aligned:
"m \<le> 28 \<Longrightarrow> is_aligned (ptrFromPAddr p) m = is_aligned p m"
apply (simp add:ptrFromPAddr_def is_aligned_mask
physMappingOffset_def kernelBase_addr_def ARM_HYP.physBase_def physBase_def)
pptrBaseOffset_def pptrBase_def ARM_HYP.physBase_def physBase_def)
apply (subst add.commute)
apply (subst mask_add_aligned)
apply (erule is_aligned_weaken[rotated])

4
proof/refine/ARM_HYP/Invariants_H.thy
View File

@ -509,12 +509,12 @@ where valid_cap'_def:
(\<forall>p < 2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT)
(ref + p * 2 ^ pageBits) s) \<and>
(case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow>
0 < asid \<and> asid \<le> 2 ^ asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < kernelBase) \<and>
0 < asid \<and> asid \<le> 2 ^ asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) \<and>
rghts \<noteq> VMNoAccess
| PageTableCap ref mapdata \<Rightarrow>
page_table_at' ref s \<and>
(case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow>
0 < asid \<and> asid \<le> 2^asid_bits - 1 \<and> ref < kernelBase)
0 < asid \<and> asid \<le> 2^asid_bits - 1 \<and> ref < pptrBase)
| PageDirectoryCap ref mapdata \<Rightarrow>
page_directory_at' ref s \<and>
case_option True (\<lambda>asid. 0 < asid \<and> asid \<le> 2^asid_bits - 1) mapdata

4
proof/refine/ARM_HYP/VSpace_R.thy
View File

@ -5128,7 +5128,7 @@ lemma in_set_zip_singleton[simp]:
lemma valid_pte'_offset:
"\<lbrakk> valid_pte' pte s; x \<le> 15; pte = LargePagePTE p a b c; vmsz_aligned' p ARMLargePage \<rbrakk>
\<Longrightarrow> valid_pte' (addPTEOffset pte x) s"
using is_aligned_mult_triv2[of x 12, simplified] is_aligned_physMappingOffset [of ARMLargePage]
using is_aligned_mult_triv2[of x 12, simplified] is_aligned_pptrBaseOffset [of ARMLargePage]
apply (clarsimp simp: addPTEOffset_def valid_mapping'_def addPAddr_def fromPAddr_def is_aligned_add)
apply (clarsimp simp: ptrFromPAddr_def vmsz_aligned'_def)
apply (drule aligned_offset_non_zero[rotated -1, where n=16 and y="x * 0x1000"])
@ -5159,7 +5159,7 @@ lemma mapM_x_storePTE_invs:
lemma valid_pde'_offset:
"\<lbrakk> valid_pde' pde s; x \<le> 15; pde = SuperSectionPDE p a b c; vmsz_aligned' p ARMSuperSection \<rbrakk>
\<Longrightarrow> valid_pde' (addPDEOffset pde x) s"
using is_aligned_mult_triv2[of x 21, simplified] is_aligned_physMappingOffset [of ARMSuperSection]
using is_aligned_mult_triv2[of x 21, simplified] is_aligned_pptrBaseOffset [of ARMSuperSection]
apply (clarsimp simp: addPDEOffset_def valid_mapping'_def addPAddr_def fromPAddr_def is_aligned_add)
apply (clarsimp simp: ptrFromPAddr_def vmsz_aligned'_def)
apply (drule aligned_offset_non_zero[rotated -1, where n=25 and y="x * 0x200000"])

6
spec/abstract/KernelInit_A.thy
View File

@ -174,7 +174,7 @@ definition "L2CC_PPTR \<equiv> 0xfff02000 :: word32"
definition "UART_PADDR \<equiv> 0x43f90000 :: word32"
definition "UART_PPTR \<equiv> 0xfff03000 :: word32"
definition "BASE_OFFSET = physMappingOffset"
definition "BASE_OFFSET = pptrBaseOffset"
section \<open>Functions cloned and modified for separation logic to work\<close>
@ -984,8 +984,8 @@ definition
definition
paddr_to_pptr_reg :: "(paddr \<times> paddr) \<Rightarrow> (paddr \<times> paddr)" where
"paddr_to_pptr_reg p_reg \<equiv> (fst p_reg + physMappingOffset,
snd p_reg + physMappingOffset)"
"paddr_to_pptr_reg p_reg \<equiv> (fst p_reg + pptrBaseOffset,
snd p_reg + pptrBaseOffset)"
definition
init_kernel :: "paddr \<Rightarrow> paddr \<Rightarrow> word32 \<Rightarrow> vspace_ref \<Rightarrow> (unit,'z::state_ext) ki_monad" where

16
spec/machine/ARM/Platform.thy
View File

@ -41,30 +41,26 @@ definition
cacheLine :: nat where
"cacheLine = 2^cacheLineBits"
definition
kernelBase_addr :: word32 where
"kernelBase_addr \<equiv> 0xe0000000"
(* Arch specific kernel base address used for haskell spec *)
definition
kernelBase :: word32 where
"kernelBase \<equiv> 0xe0000000"
pptrBase :: word32 where
"pptrBase \<equiv> 0xe0000000"
definition
physBase :: word32 where
"physBase \<equiv> 0x10000000"
definition
physMappingOffset :: word32 where
"physMappingOffset \<equiv> kernelBase_addr - physBase"
pptrBaseOffset :: word32 where
"pptrBaseOffset \<equiv> pptrBase - physBase"
definition
ptrFromPAddr :: "paddr \<Rightarrow> word32" where
"ptrFromPAddr paddr \<equiv> paddr + physMappingOffset"
"ptrFromPAddr paddr \<equiv> paddr + pptrBaseOffset"
definition
addrFromPPtr :: "word32 \<Rightarrow> paddr" where
"addrFromPPtr pptr \<equiv> pptr - physMappingOffset"
"addrFromPPtr pptr \<equiv> pptr - pptrBaseOffset"
definition
minIRQ :: "irq" where

18
spec/machine/ARM_HYP/Platform.thy
View File

@ -41,14 +41,10 @@ definition
cacheLine :: nat where
"cacheLine = 2^cacheLineBits"
definition
kernelBase_addr :: word32 where
"kernelBase_addr \<equiv> 0xe0000000"
(* Arch specific kernel base address used for haskell spec *)
definition
kernelBase :: word32 where
"kernelBase \<equiv> 0xe0000000"
pptrBase :: word32 where
"pptrBase \<equiv> 0xe0000000"
definition
physBase :: word32 where
@ -60,19 +56,19 @@ definition
definition
paddrTop :: "32 word" where
"paddrTop \<equiv> pptrTop - (kernelBase - physBase)"
"paddrTop \<equiv> pptrTop - (pptrBase - physBase)"
definition
physMappingOffset :: word32 where
"physMappingOffset \<equiv> kernelBase_addr - physBase"
pptrBaseOffset :: word32 where
"pptrBaseOffset \<equiv> pptrBase - physBase"
definition
ptrFromPAddr :: "paddr \<Rightarrow> word32" where
"ptrFromPAddr paddr \<equiv> paddr + physMappingOffset"
"ptrFromPAddr paddr \<equiv> paddr + pptrBaseOffset"
definition
addrFromPPtr :: "word32 \<Rightarrow> paddr" where
"addrFromPPtr pptr \<equiv> pptr - physMappingOffset"
"addrFromPPtr pptr \<equiv> pptr - pptrBaseOffset"
definition
minIRQ :: "irq" where