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

proof: update (non-x64) for physBase-dependent defs 

Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2023-03-10 12:12:50 +11:00 committed by Rafal Kolanski
parent 317164b3b7
commit d5fa6043cb
25 changed files with 106 additions and 85 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
proof/access-control/ARM/ArchADT_AC.thy
View File

@ -101,7 +101,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 pptrBaseOffset_def pptrBase_def physBase_def)
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def Kernel_Config.physBase_def)
apply (simp add: ptr_offset_in_ptr_range)
apply (simp add: kernel_mappings_kernel_mapping_slots')
apply (clarsimp simp: graph_of_def)
@ -165,7 +165,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 pptrBaseOffset_def pptrBase_def physBase_def)
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def Kernel_Config.physBase_def)
apply (simp add: ptr_offset_in_ptr_range)
apply (clarsimp simp: get_page_info_def get_pd_entry_def get_pt_info_def
get_pt_entry_def get_arch_obj_def pte_ref_def graph_of_def

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

@ -1188,8 +1188,7 @@ lemma lookupPTSlot_le_0x3C:
apply simp
apply (simp add: ARM.ptrFromPAddr_def pptrBaseOffset_def)
apply (erule aligned_add_aligned)
apply (simp add: pptrBase_def ARM.physBase_def
physBase_def is_aligned_def)
apply (simp add: pptrBase_def Kernel_Config.physBase_def is_aligned_def)
apply (simp add: word_bits_def pteBits_def)
done
@ -1435,8 +1434,7 @@ lemma valid_pde_slots_lift2:
lemma addrFromPPtr_mask_5:
"addrFromPPtr ptr && mask (5::nat) = ptr && mask (5::nat)"
apply (simp add:addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM.physBase_def)
apply (simp add:addrFromPPtr_def pptrBaseOffset_def pptrBase_def Kernel_Config.physBase_def)
apply word_bitwise
apply (simp add:mask_def)
done
@ -2020,7 +2018,7 @@ lemma vmsz_aligned_addrFromPPtr':
apply (erule(1) aligned_sub_aligned)
apply (simp add: pageBitsForSize_def word_bits_def split: vmpage_size.split)
apply (simp add: pageBitsForSize_def pptrBaseOffset_def pptrBase_def
physBase_def ARM.physBase_def is_aligned_def
Kernel_Config.physBase_def is_aligned_def
split: vmpage_size.split)
done

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

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

7
proof/crefine/ARM/SR_lemmas_C.thy
View File

@ -2137,5 +2137,12 @@ lemma msgRegisters_size_sanity:
"size_msgRegisters = unat (n_msgRegisters)"
by (simp add: n_msgRegisters_def size_msgRegisters_def)
(* link up Kernel_Config loaded from the seL4 build system with physBase in C code *)
lemma physBase_spec:
"\<forall>s. \<Gamma>\<turnstile> {s} Call physBase_'proc {t. ret__unsigned_long_' t = Kernel_Config.physBase }"
apply (rule allI, rule conseqPre, vcg)
apply (simp add: Kernel_Config.physBase_def)
done
end
end

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

@ -709,7 +709,7 @@ lemma ptrFromPAddr_spec:
Call ptrFromPAddr_'proc
\<lbrace>\<acute>ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s))\<rbrace>"
apply vcg
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def physBase_def)
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def)
done
lemma addrFromPPtr_spec:
@ -717,7 +717,7 @@ lemma addrFromPPtr_spec:
Call addrFromPPtr_'proc
\<lbrace>\<acute>ret__unsigned_long = addrFromPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def physBase_def)
apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def)
done
lemma addrFromKPPtr_spec:
@ -726,7 +726,7 @@ lemma addrFromKPPtr_spec:
\<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def
kernelELFBase_def physBase_def pptrBase_def mask_def)
kernelELFBase_def pptrBase_def mask_def)
done
abbreviation

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

@ -1209,8 +1209,7 @@ lemma lookupPTSlot_le_0x3C:
apply simp
apply (simp add: ARM_HYP.ptrFromPAddr_def pptrBaseOffset_def)
apply (erule aligned_add_aligned)
apply (simp add: pptrBase_def ARM_HYP.physBase_def
physBase_def is_aligned_def)
apply (simp add: pptrBase_def Kernel_Config.physBase_def is_aligned_def)
apply (simp add: word_bits_def)
done
@ -1471,7 +1470,7 @@ lemma obj_at_pte_aligned:
lemma addrFromPPtr_mask_5:
"addrFromPPtr ptr && mask (5::nat) = ptr && mask (5::nat)"
apply (simp add:addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM_HYP.physBase_def)
pptrBase_def Kernel_Config.physBase_def)
apply word_bitwise
apply (simp add:mask_def)
done
@ -1479,7 +1478,7 @@ lemma addrFromPPtr_mask_5:
lemma addrFromPPtr_mask_6:
"addrFromPPtr ptr && mask (6::nat) = ptr && mask (6::nat)"
apply (simp add:addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def ARM_HYP.physBase_def)
pptrBase_def Kernel_Config.physBase_def)
apply word_bitwise
apply (simp add:mask_def)
done
@ -2273,7 +2272,7 @@ lemma vmsz_aligned_addrFromPPtr':
apply (erule(1) aligned_sub_aligned)
apply (simp add: pageBitsForSize_def word_bits_def split: vmpage_size.split)
apply (simp add: pageBitsForSize_def pptrBaseOffset_def pptrBase_def
physBase_def ARM_HYP.physBase_def is_aligned_def
Kernel_Config.physBase_def is_aligned_def
split: vmpage_size.split)
done
@ -2800,9 +2799,9 @@ lemma decodeARMFrameInvocation_ccorres:
in ccorres_symb_exec_r_known_rv)
apply (rule conseqPre, vcg)
(* FIXME: temporary workaround, there should only be one physBase *)
apply (clarsimp simp: unify_physBase dest!: ccap_relation_PageCap_generics)
apply (clarsimp simp: paddrTop_def pptrTop_def fromPAddr_def
ARM_HYP.physBase_def ARM_HYP.pptrBase_def
apply (clarsimp dest!: ccap_relation_PageCap_generics)
apply (clarsimp simp: paddrTop_def pptrTop_def fromPAddr_def pptrBaseOffset_def
Kernel_Config.physBase_def ARM_HYP.pptrBase_def
hd_drop_conv_nth hd_conv_nth false_def true_def
split: if_split)
apply ceqv

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

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

9
proof/crefine/ARM_HYP/SR_lemmas_C.thy
View File

@ -2438,19 +2438,12 @@ lemma unat_scast_numDomains:
"unat (SCAST(32 signed \<rightarrow> machine_word_len) Kernel_C.numDomains) = unat Kernel_C.numDomains"
by (simp add: scast_eq sint_numDomains_to_H unat_numDomains_to_H numDomains_machine_word_safe)
(* FIXME physBase now has two definitions: Kernel_Config.physBase and Platform.ARM_HYP.physBase,
the latter should be removed, but sees plenty of use in ARM_HYP *)
(* doubles as a sanity check of Kernel_Config being correctly loaded from the seL4 build system *)
(* link up Kernel_Config loaded from the seL4 build system with physBase in C code *)
lemma physBase_spec:
"\<forall>s. \<Gamma>\<turnstile> {s} Call physBase_'proc {t. ret__unsigned_long_' t = Kernel_Config.physBase }"
apply (rule allI, rule conseqPre, vcg)
apply (simp add: Kernel_Config.physBase_def)
done
(* FIXME: this is a temporary fix, only Kernel_Config.physBase should remain in the end *)
lemma unify_physBase:
"Kernel_Config.physBase = Platform.ARM_HYP.physBase"
by (simp add: Kernel_Config.physBase_def Platform.ARM_HYP.physBase_def)
end
end

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

@ -781,8 +781,7 @@ lemma ptrFromPAddr_spec:
Call ptrFromPAddr_'proc
\<lbrace>\<acute>ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s))\<rbrace>"
apply vcg
(* FIXME: unify_physBase will be unnecessary once there is only one physBase *)
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def unify_physBase)
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def)
done
lemma addrFromPPtr_spec:
@ -790,8 +789,7 @@ lemma addrFromPPtr_spec:
Call addrFromPPtr_'proc
\<lbrace>\<acute>ret__unsigned_long = addrFromPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
(* FIXME: unify_physBase will be unnecessary once there is only one physBase *)
apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def unify_physBase)
apply (simp add: addrFromPPtr_def pptrBaseOffset_def pptrBase_def)
done
lemma addrFromKPPtr_spec:
@ -799,9 +797,8 @@ lemma addrFromKPPtr_spec:
Call addrFromKPPtr_'proc
\<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
(* FIXME: unify_physBase will be unnecessary once there is only one physBase *)
apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def
kernelELFBase_def unify_physBase pptrBase_def mask_def)
kernelELFBase_def pptrBase_def mask_def)
done
abbreviation
@ -2686,7 +2683,7 @@ lemma ccorres_seq_IF_False:
lemma ptrFromPAddr_mask6_simp[simp]:
"ptrFromPAddr ps && mask 6 = ps && mask 6"
unfolding ptrFromPAddr_def pptrBaseOffset_def pptrBase_def ARM_HYP.physBase_def
unfolding ptrFromPAddr_def pptrBaseOffset_def pptrBase_def Kernel_Config.physBase_def
by (subst add.commute, subst mask_add_aligned ; simp add: is_aligned_def)
lemma doFlush_ccorres:

7
proof/crefine/RISCV64/SR_lemmas_C.thy
View File

@ -2130,5 +2130,12 @@ lemma unat_scast_numDomains:
"unat (SCAST(32 signed \<rightarrow> machine_word_len) Kernel_C.numDomains) = unat Kernel_C.numDomains"
by (simp add: scast_eq sint_numDomains_to_H unat_numDomains_to_H numDomains_machine_word_safe)
(* link up Kernel_Config loaded from the seL4 build system with physBase in C code *)
lemma physBase_spec:
"\<forall>s. \<Gamma>\<turnstile> {s} Call physBase_'proc {t. ret__unsigned_long_' t = Kernel_Config.physBase }"
apply (rule allI, rule conseqPre, vcg)
apply (simp add: Kernel_Config.physBase_def)
done
end
end

2
proof/crefine/RISCV64/VSpace_C.thy
View File

@ -868,7 +868,7 @@ lemma addrFromKPPtr_spec:
\<lbrace>\<acute>ret__unsigned_long = addrFromKPPtr (ptr_val (pptr_' s))\<rbrace>"
apply vcg
apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def
kernelELFBase_def kernelELFPAddrBase_def)
kernelELFBase_def kernelELFPAddrBase_def mask_def)
done
lemma isValidVTableRoot_def2:

14
proof/infoflow/ARM/Example_Valid_State.thy
View File

@ -906,7 +906,7 @@ lemma Sys1AgentMap_simps:
unfolding Sys1AgentMap_def
apply simp_all
by (auto simp: ptrFromPAddr_def pptrBaseOffset_def
pptrBase_def physBase_def s0_ptr_defs)
pptrBase_def Kernel_Config.physBase_def s0_ptr_defs)
definition
Sys1ASIDMap :: "(auth_graph_label subject_label) agent_asid_map"
@ -1032,7 +1032,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
pptrBaseOffset_def pptrBase_def physBase_def)
pptrBaseOffset_def pptrBase_def Kernel_Config.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
@ -1067,14 +1067,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 pptrBaseOffset_def pptrBase_def physBase_def
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def Kernel_Config.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 pptrBaseOffset_def pptrBase_def physBase_def
apply (simp add: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def Kernel_Config.physBase_def
s0_ptr_defs)
apply (simp add: add.commute)
@ -1612,7 +1612,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
pptrBaseOffset_def pptrBase_def physBase_def is_aligned_def
pptrBaseOffset_def pptrBase_def Kernel_Config.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)+
@ -1640,7 +1640,7 @@ lemma valid_global_objs_s0[simp]:
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 pptrBaseOffset_def pptrBase_def
physBase_def is_aligned_def pageBits_def
Kernel_Config.physBase_def is_aligned_def pageBits_def
kernel_mapping_slots_def empty_table_def pde_ref_def
valid_pde_mappings_def)+
@ -1661,7 +1661,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 pptrBaseOffset_def pptrBase_def physBase_def)+
addrFromPPtr_def pptrBaseOffset_def pptrBase_def Kernel_Config.physBase_def)+
lemma valid_asid_map_s0[simp]:
"valid_asid_map s0_internal"

17
proof/infoflow/RISCV64/Example_Valid_State.thy
View File

@ -1497,21 +1497,25 @@ lemma valid_arch_state_s0[simp]:
simp: init_vspace_uses_def split: if_splits)
apply (fastforce elim: dual_order.strict_trans[rotated] split: if_splits
simp: init_vspace_uses_def pptr_base_def pptrBase_def
canonical_bit_def kernel_elf_base_def kernelELFBase_def)
canonical_bit_def kernel_elf_base_def kernelELFBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def mask_def)
apply (fastforce dest: dual_order.strict_trans1[where a=kernel_elf_base, rotated]
dual_order.strict_trans1[OF _ pptr_base_kernel_elf_base]
canonical_user_below_pptr_base
simp: init_vspace_uses_def pptr_base_def pptrBase_def
canonical_bit_def kernel_elf_base_def kernelELFBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def mask_def
split: if_splits)
apply (fastforce dest: dual_order.strict_trans2 canonical_user_below_pptr_base
simp: init_vspace_uses_def pptr_base_def pptrBase_def canonical_bit_def
kdev_base_def kdevBase_def kernel_elf_base_def kernelELFBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def mask_def
split: if_splits)
apply (fastforce dest: dual_order.strict_trans1[where a=kernel_elf_base, rotated]
canonical_user_below_pptr_base
simp: user_window_def user_region_def init_vspace_uses_def pptr_base_def
pptrBase_def canonical_bit_def kernel_elf_base_def kernelELFBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def mask_def
split: if_splits)+
apply (fastforce simp: valid_global_arch_objs_def obj_at_def kh0_def a_type_def
init_global_pt_def max_pt_level_not_asid_pool_level[symmetric])
@ -1814,21 +1818,24 @@ lemma valid_global_pd_mappings_s0_helper':
apply (clarsimp simp: ptes_of_def pts_of_s0 riscv_global_pt_is_aligned global_pte_def
table_index_offset_pt_bits_left is_aligned_pt_slot_offset_pte
split: if_splits)
apply (clarsimp simp: misc kernel_elf_base_def kernelELFBase_def)
apply (clarsimp simp: misc kernel_elf_base_def kernelELFBase_def kernelELFPAddrBase_def
Kernel_Config.physBase_def)
apply (word_bitwise, fastforce)
apply (clarsimp simp: misc s0_ptr_defs kernel_mapping_slots_def
kernel_elf_base_def kernelELFBase_def)
kernel_elf_base_def kernelELFBase_def kernelELFPAddrBase_def
Kernel_Config.physBase_def)
apply (word_bitwise, fastforce)
apply (clarsimp simp: ptes_of_def pts_of_s0 riscv_global_pt_is_aligned
is_aligned_pt_slot_offset_pte global_pte_def
split: if_splits)
apply (clarsimp simp: addr_from_ppn_def bit_simps s0_ptr_defs pt_bits_left_def mask_def
pt_slot_offset_def pt_index_def kernel_elf_base_def kernelELFBase_def)
pt_slot_offset_def pt_index_def kernel_elf_base_def kernelELFBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def)
apply (word_bitwise, fastforce)
apply (clarsimp simp: addr_from_ppn_def ptrFromPAddr_def addrFromKPPtr_def bit_simps
is_aligned_def s0_ptr_defs pt_bits_left_def mask_def pptrBaseOffset_def
paddrBase_def kernel_elf_base_def kernelELFBase_def
kernelELFBaseOffset_def kernelELFPAddrBase_def)
kernelELFBaseOffset_def kernelELFPAddrBase_def Kernel_Config.physBase_def)
apply (word_bitwise, fastforce)
done

18
proof/infoflow/refine/ARM/Example_Valid_StateH.thy
View File

@ -2187,26 +2187,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
pptrBaseOffset_def ARM.pptrBase_def ARM.physBase_def
pptrBase_def physBase_def
pptrBaseOffset_def ARM.pptrBase_def Kernel_Config.physBase_def
pptrBase_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.pptrBase_def ARM.physBase_def ARM.ptrFromPAddr_def ptBits_def
pageBits_def pptrBaseOffset_def pptrBase_def physBase_def
ARM.pptrBase_def ARM.ptrFromPAddr_def ptBits_def
pageBits_def pptrBaseOffset_def pptrBase_def Kernel_Config.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
pptrBaseOffset_def pptrBase_def physBase_def
ARM.ptrFromPAddr_def ptBits_def pageBits_def
pptrBaseOffset_def pptrBase_def Kernel_Config.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.pptrBase_def
ARM.physBase_def pptrBaseOffset_def pptrBase_def physBase_def
pptrBaseOffset_def pptrBase_def Kernel_Config.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
pptrBaseOffset_def pptrBase_def physBase_def
is_aligned_def ARM.addrFromPPtr_def ARM.ptrFromPAddr_def
pptrBaseOffset_def pptrBase_def Kernel_Config.physBase_def
split: if_split_asm)
done

5
proof/invariant-abstract/AARCH64/ArchInvariants_AI.thy
View File

@ -1494,9 +1494,10 @@ lemma canonical_user_ge0[intro!,simp]:
"0 < canonical_user"
by (simp add: canonical_user_def mask_def ipa_size_def)
lemma pptr_base_kernel_elf_base:
lemma pptr_base_kernel_elf_base: (* FIXME MK: candidate for Kernel_Config_Lemmas *)
"pptr_base < kernel_elf_base"
by (simp add: pptr_base_def pptrBase_def kernel_elf_base_def kernelELFBase_def)
by (simp add: pptr_base_def pptrBase_def canonical_bit_def kernel_elf_base_def kernelELFBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def mask_def)
lemma pptrTop_le_ipa_size:
"pptrTop \<le> mask ipa_size"

3
proof/invariant-abstract/AARCH64/ArchKernelInit_AI.thy
View File

@ -252,7 +252,8 @@ lemma irq_node_pptr_base_kernel_elf_base:
"\<lbrakk>x \<le> pptr_base + (m + (mask cte_level_bits + 0x3000)); m \<le> mask (size irq) << cte_level_bits \<rbrakk>
\<Longrightarrow> \<not> kernel_elf_base \<le> x" for irq::irq
apply (simp add: word_size cte_level_bits_def mask_def pptr_base_def pptrBase_def
kernel_elf_base_def kernelELFBase_def canonical_bit_def not_le)
Kernel_Config.physBase_def kernel_elf_base_def kernelELFBase_def canonical_bit_def
not_le)
apply unat_arith
done

4
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 pptrBaseOffset_def pptrBase_def physBase_def)
apply (clarsimp simp: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def Kernel_Config.physBase_def)
apply (erule is_aligned_addD2)
apply (rule is_aligned_weaken[where x = 24])
apply (simp add: is_aligned_def)
@ -188,7 +188,7 @@ lemma device_frame_in_device_region:
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]
pptrBase_def Kernel_Config.physBase_def is_aligned_def)[1]
global_naming Arch
named_theorems AInvsPre_asms

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

@ -2547,7 +2547,7 @@ 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: pptrBaseOffset_def physBase_def
apply (simp add: pptrBaseOffset_def Kernel_Config.physBase_def
pptrBase_def pageBits_def)
apply (erule is_aligned_weaken[rotated])
apply (simp add: is_aligned_def)
@ -2561,7 +2561,7 @@ 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 pptrBaseOffset_def
pptrBase_def physBase_def)
pptrBase_def Kernel_Config.physBase_def)
apply (erule aligned_add_aligned)
apply (erule is_aligned_weaken[rotated])
apply (simp add:is_aligned_def)

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

@ -360,7 +360,7 @@ lemma invs_A:
valid_pde_mappings_def valid_vso_at_def)
apply (simp add: kernel_base_def kernel_mapping_slots_def
Platform.ARM.addrFromPPtr_def pptrBaseOffset_def
pptrBase_def physBase_def pageBits_def is_aligned_def)
pptrBase_def Kernel_Config.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

4
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 pptrBaseOffset_def pptrBase_def physBase_def)
apply (clarsimp simp: ptrFromPAddr_def pptrBaseOffset_def pptrBase_def Kernel_Config.physBase_def)
apply (erule is_aligned_addD2)
apply (rule is_aligned_weaken[where x = 25])
apply (simp add: is_aligned_def)
@ -108,7 +108,7 @@ lemma device_frame_in_device_region:
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]
pptrBase_def Kernel_Config.physBase_def is_aligned_def)[1]
global_naming Arch
named_theorems AInvsPre_asms

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

@ -2552,7 +2552,7 @@ 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: pptrBaseOffset_def physBase_def
apply (simp add: pptrBaseOffset_def Kernel_Config.physBase_def
pptrBase_def pageBits_def)
apply (erule is_aligned_weaken[rotated])
apply (simp add: is_aligned_def)
@ -2566,7 +2566,7 @@ 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 pptrBaseOffset_def
pptrBase_def physBase_def)
pptrBase_def Kernel_Config.physBase_def)
apply (erule aligned_add_aligned)
apply (erule is_aligned_weaken[rotated])
apply (simp add:is_aligned_def)

5
proof/invariant-abstract/RISCV64/ArchInvariants_AI.thy
View File

@ -1280,9 +1280,10 @@ lemma canonical_user_pptr_base:
"canonical_user < pptr_base"
by (simp add: canonical_user_def pptr_base_def pptrBase_def canonical_bit_def mask_def)
lemma pptr_base_kernel_elf_base:
lemma pptr_base_kernel_elf_base: (* FIXME MK: candidate for Kernel_Config_Lemmas *)
"pptr_base < kernel_elf_base"
by (simp add: pptr_base_def pptrBase_def canonical_bit_def kernel_elf_base_def kernelELFBase_def)
by (simp add: pptr_base_def pptrBase_def canonical_bit_def kernel_elf_base_def kernelELFBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def mask_def)
lemma above_pptr_base_canonical:
"pptr_base \<le> p \<Longrightarrow> canonical_address p"

29
proof/invariant-abstract/RISCV64/ArchKernelInit_AI.thy
View File

@ -262,7 +262,8 @@ lemma elf_window_1M:
"\<lbrakk> kernel_elf_base \<le> vref; vref < kernel_elf_base + (1 << 20) \<rbrakk> \<Longrightarrow>
table_index (pt_slot_offset max_pt_level riscv_global_pt_ptr vref) = 0x1FE"
apply (simp add: table_index_riscv_global_pt_ptr)
apply (simp add: bit_simps kernel_elf_base_def kernelELFBase_def)
apply (simp add: bit_simps kernel_elf_base_def kernelELFBase_def kernelELFPAddrBase_def
Kernel_Config.physBase_def)
apply word_bitwise
apply (clarsimp simp: word_size)
done
@ -281,11 +282,12 @@ lemma translate_address_kernel_elf_window:
apply (simp add: elf_window_1M is_aligned_pt_slot_offset_pte)
apply (simp add: bit_simps addr_from_ppn_def shiftl_shiftl)
apply (simp add: ptrFromPAddr_def addrFromPPtr_def)
apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def kernelELFBase_def)
apply (simp add: addrFromKPPtr_def kernelELFBaseOffset_def kernelELFPAddrBase_def kernelELFBase_def
Kernel_Config.physBase_def mask_def)
apply (simp add: pt_bits_left_def bit_simps level_defs)
apply (rule conjI)
apply (simp add: pptrBase_def pptrBaseOffset_def paddrBase_def canonical_bit_def is_aligned_def)
apply (simp add: kernel_elf_base_def kernelELFBase_def)
apply (simp add: kernel_elf_base_def kernelELFBase_def kernelELFPAddrBase_def Kernel_Config.physBase_def)
apply (subst word_plus_and_or_coroll)
apply (simp add: canonical_bit_def word_size mask_def)
apply word_bitwise
@ -301,7 +303,8 @@ lemma kernel_window_init_st:
lemma kernel_elf_window_init_st:
"kernel_elf_window init_A_st = { kernel_elf_base ..< kernel_elf_base + (1 << 20) }"
apply (clarsimp simp: state_defs kernel_elf_window_def kernel_elf_base_def kernelELFBase_def
pptr_base_def pptrBase_def canonical_bit_def)
pptr_base_def pptrBase_def canonical_bit_def kernelELFPAddrBase_def
Kernel_Config.physBase_def)
apply (rule set_eqI, clarsimp)
apply (rule iffI)
apply auto[1]
@ -326,18 +329,22 @@ proof -
(simp add: canonical_user_def mask_def pptr_base_def pptrBase_def)
have [simp]: "p \<le> canonical_user \<Longrightarrow> \<not> kernel_elf_base \<le> p" for p
by (rule notI, drule (1) order_trans)
(simp add: canonical_user_def mask_def kernel_elf_base_def kernelELFBase_def)
(simp add: canonical_user_def mask_def kernel_elf_base_def kernelELFBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def)
have [simp]: "p \<le> canonical_user \<Longrightarrow> \<not> kdev_base \<le> p" for p
by (rule notI, drule (1) order_trans)
(simp add: canonical_user_def mask_def kdev_base_def kdevBase_def)
have [simp]: "kernel_elf_base \<le> p \<Longrightarrow> \<not> p < pptr_base + 0x40000000" for p
by (rule notI, drule (1) order_le_less_trans)
(simp add: kernel_elf_base_def kernelELFBase_def pptr_base_def pptrBase_def)
(simp add: kernel_elf_base_def kernelELFBase_def pptr_base_def pptrBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def mask_def)
have [simp]: "kdev_base \<le> p \<Longrightarrow> \<not> p < kernel_elf_base + 0x100000" for p
by (rule notI, drule (1) order_le_less_trans)
(simp add: kernel_elf_base_def kernelELFBase_def kdev_base_def kdevBase_def)
(simp add: kernel_elf_base_def kernelELFBase_def kdev_base_def kdevBase_def pptrBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def mask_def)
have "pptr_base + 0x40000000 < kernel_elf_base + 0x100000"
by (simp add: kernel_elf_base_def kernelELFBase_def pptr_base_def pptrBase_def)
by (simp add: kernel_elf_base_def kernelELFBase_def pptr_base_def pptrBase_def
kernelELFPAddrBase_def Kernel_Config.physBase_def mask_def)
thus ?thesis
using canonical_user_pptr_base pptr_base_kernel_elf_base
unfolding valid_uses_2_def init_vspace_uses_def window_defs
@ -389,7 +396,8 @@ lemma irq_node_pptr_base_kernel_elf_base:
"\<lbrakk>x \<le> pptr_base + (m + (mask cte_level_bits + 0x3000)); m \<le> mask (size irq) << cte_level_bits \<rbrakk>
\<Longrightarrow> \<not> kernel_elf_base \<le> x" for irq::irq
apply (simp add: word_size cte_level_bits_def mask_def pptr_base_def pptrBase_def
kernel_elf_base_def kernelELFBase_def canonical_bit_def not_le)
kernel_elf_base_def kernelELFBase_def canonical_bit_def not_le
kernelELFPAddrBase_def Kernel_Config.physBase_def)
apply unat_arith
done
@ -411,7 +419,8 @@ lemma irq_node_in_kernel_window_init_arch_state':
apply (simp add: pptr_base_num cte_level_bits_def canonical_bit_def mask_def word_size)
apply unat_arith
apply (simp add: kernel_elf_base_def kernelELFBase_def cte_level_bits_def canonical_bit_def
mask_def init_irq_node_ptr_def pptr_base_num word_size)
mask_def init_irq_node_ptr_def pptr_base_num word_size kernelELFPAddrBase_def
Kernel_Config.physBase_def)
apply unat_arith
apply clarsimp
done

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

@ -1494,7 +1494,8 @@ 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 pptrBaseOffset_def pptrBase_def physBase_def)
apply (simp add: ptrFromPAddr_def is_aligned_mask pptrBaseOffset_def pptrBase_def
Kernel_Config.physBase_def)
apply (subst add.commute)
apply (subst mask_add_aligned)
apply (erule is_aligned_weaken[rotated])

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

@ -576,7 +576,7 @@ lemma decodeARMPageFlush_corres:
page_size \<leftarrow> returnOk $ 1 << pageBitsForSize vmpage_size;
whenE (page_size \<le> start \<or> page_size < end) $
throwError $ ExceptionTypes_A.syscall_error.InvalidArgument 0;
whenE (pstart < ARM_HYP.physBase \<or> ARM_HYP.paddrTop < end - start + pstart) $
whenE (pstart < physBase \<or> ARM_HYP.paddrTop < end - start + pstart) $
throwError ExceptionTypes_A.syscall_error.IllegalOperation;
returnOk $
arch_invocation.InvokePage $
@ -605,7 +605,7 @@ lemma decodeARMPageFlush_corres:
apply (rule whenE_throwError_corres, simp)
apply simp
apply (rule whenE_throwError_corres, simp)
apply (simp add: fromPAddr_def physBase_def paddrTop_def add.commute)
apply (simp add: fromPAddr_def Kernel_Config.physBase_def paddrTop_def add.commute)
apply (rule corres_trivial)
apply (rule corres_returnOk)
apply (clarsimp simp: archinv_relation_def page_invocation_map_def flush_type_map_def)
@ -1726,7 +1726,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
pptrBaseOffset_def pptrBase_def ARM_HYP.physBase_def physBase_def)
pptrBaseOffset_def pptrBase_def Kernel_Config.physBase_def)
apply (subst add.commute)
apply (subst mask_add_aligned)
apply (erule is_aligned_weaken[rotated])