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

aarch64 aspec+ainvs: add valid_asid_map invariant 

Refine needs slightly stricter information about asid maps, in
particular we need to know explicitly that asid 0 never maps to
a VSpace. This is the reverse of valid_vmid_table, but unfortunately
does not fully follow from valid_vmid_table, because there can
be VSpaces mapped without an assigned VMID.

We shift the test for 0 < asid from entry_for_asid to vspace_for_asid
so we can use entry_for_asid in the formulation of the invariant.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-07-04 12:46:41 +10:00
parent 438e27a8f1
commit c6281810d4
No known key found for this signature in database
GPG Key ID: 20A847CE6AB7F5F3
10 changed files with 116 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
proof/invariant-abstract/AARCH64/ArchAcc_AI.thy
View File

@ -1180,13 +1180,9 @@ lemma set_pt_global_objs [wp]:
crunch v_ker_map[wp]: set_pt "valid_kernel_mappings"
(ignore: set_object wp: set_object_v_ker_map crunch_wps)
lemma set_pt_asid_map [wp]:
"\<lbrace>valid_asid_map\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_asid_map\<rbrace>"
apply (simp add: valid_asid_map_def vspace_at_asid_def)
apply (rule hoare_lift_Pf2 [where f="arch_state"])
apply wp+
done
lemma set_pt_asid_map[wp]:
"set_pt p pt \<lbrace>valid_asid_map\<rbrace>"
by (wp valid_asid_map_lift_strong)
crunches store_pte
for pred_tcb[wp]: "\<lambda>s. Q (pred_tcb_at proj P t s)"
@ -1988,6 +1984,16 @@ lemma set_asid_pool_valid_asid_pool_caps[wp]:
unfolding valid_asid_pool_caps_def
by (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift')
lemma set_asid_pool_None_valid_asid_map[wp]:
"\<lbrace> valid_asid_map and (\<lambda>s. asid_pools_of s p = Some ap) \<rbrace>
set_asid_pool p (ap (asid_low := None))
\<lbrace>\<lambda>_. valid_asid_map\<rbrace>"
unfolding valid_asid_map_def entry_for_asid_def
apply (clarsimp simp: obind_None_eq pool_for_asid_def)
apply (wp hoare_vcg_disj_lift hoare_vcg_ex_lift get_object_wp)
apply (fastforce simp: entry_for_pool_def obind_None_eq in_omonad split: if_split_asm)
done
lemma set_asid_pool_invs_unmap:
"\<lbrace>invs and
(\<lambda>s. asid_pools_of s p = Some ap) and
@ -1996,7 +2002,7 @@ lemma set_asid_pool_invs_unmap:
set_asid_pool p (ap (asid_low := None))
\<lbrace>\<lambda>_. invs\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def
valid_arch_caps_def valid_asid_map_def)
valid_arch_caps_def)
apply (wp valid_irq_node_typ set_asid_pool_typ_at
set_asid_pool_vspace_objs_unmap
valid_irq_handlers_lift

6
proof/invariant-abstract/AARCH64/ArchArch_AI.thy
View File

@ -438,7 +438,8 @@ lemma valid_arch_caps:
lemma valid_asid_map':
"valid_asid_map s \<Longrightarrow> valid_asid_map s'"
by (clarsimp simp: valid_asid_map_def)
by (clarsimp simp: valid_asid_map_def entry_for_asid_def obind_None_eq pool_for_asid_def s'_def
entry_for_pool_def ko)
lemma vspace_for_asid[simp]:
"vspace_for_asid asid s' = vspace_for_asid asid s"
@ -624,7 +625,8 @@ lemma valid_asid_map_asid_upd_strg:
asid_pools_of s ap = Some Map.empty \<and>
asid_table s asid = None \<longrightarrow>
valid_asid_map (asid_table_update asid ap s)"
by (simp add: valid_asid_map_def)
by (simp add: valid_asid_map_def entry_for_asid_def obind_None_eq entry_for_pool_def
pool_for_asid_def)
lemma valid_vspace_objs_asid_upd_strg:
"valid_vspace_objs s \<and>

6
proof/invariant-abstract/AARCH64/ArchCNodeInv_AI.thy
View File

@ -410,10 +410,8 @@ lemma cap_swap_asid_map[wp, CNodeInv_AI_assms]:
cte_wp_at (weak_derived c) a and
cte_wp_at (weak_derived c') b\<rbrace>
cap_swap c a c' b \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>"
apply (simp add: cap_swap_def set_cdt_def valid_asid_map_def vspace_at_asid_def)
apply (rule hoare_pre)
apply (wp set_cap.vs_lookup|simp
|rule hoare_lift_Pf [where f=arch_state])+
apply (simp add: cap_swap_def set_cdt_def vspace_at_asid_def)
apply (wp set_cap.vs_lookup|simp|rule hoare_lift_Pf [where f=arch_state])+
done

11
proof/invariant-abstract/AARCH64/ArchDetype_AI.thy
View File

@ -496,8 +496,15 @@ proof -
thus ?thesis by (simp add: valid_kernel_mappings_def detype_def ball_ran_eq)
qed
lemma valid_asid_map_detype[detype_invs_proofs]: "valid_asid_map (detype (untyped_range cap) s)"
by (simp add: valid_asid_map_def)
lemma valid_asid_map_detype[detype_invs_proofs]:
"valid_asid_map (detype (untyped_range cap) s)"
proof -
have "valid_asid_map s"
using invs by (simp add: invs_def valid_state_def)
thus ?thesis
by (clarsimp simp: valid_asid_map_def entry_for_asid_def obind_None_eq pool_for_asid_def
entry_for_pool_def)
qed
lemma equal_kernel_mappings_detype[detype_invs_proofs]:
"equal_kernel_mappings (detype (untyped_range cap) s)"

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

@ -633,7 +633,7 @@ definition valid_vmid_table_2 :: "(vmid \<rightharpoonup> asid) \<Rightarrow> bo
"valid_vmid_table_2 table \<equiv> \<forall>vmid. table vmid \<noteq> Some 0"
locale_abbrev valid_vmid_table :: "'z::state_ext state \<Rightarrow> bool" where
"valid_vmid_table s \<equiv> valid_vmid_table_2 (arm_vmid_table (arch_state s))"
"valid_vmid_table s \<equiv> valid_vmid_table_2 (vmid_table s)"
lemmas valid_vmid_table_def = valid_vmid_table_2_def
@ -710,10 +710,10 @@ definition state_hyp_refs_of :: "'z::state_ext state \<Rightarrow> obj_ref \<Rig
"state_hyp_refs_of \<equiv> \<lambda>s p. case_option {} (hyp_refs_of) (kheap s p)"
(* covered by ASIDPool case of valid_vspace_obj, vmid_inv, and definition of
vspace_for_asid (asid 0 never mapped) *)
(* Mostly covered by ASIDPool case of valid_vspace_obj and vmid_inv, but we still need to make sure
that ASID 0 is never mapped. *)
definition valid_asid_map :: "'z::state_ext state \<Rightarrow> bool" where
"valid_asid_map \<equiv> \<top>"
"valid_asid_map \<equiv> \<lambda>s. entry_for_asid 0 s = None"
definition valid_global_objs :: "'z::state_ext state \<Rightarrow> bool" where
"valid_global_objs \<equiv> \<top>"
@ -2599,7 +2599,7 @@ lemma vspace_for_asid_lift:
apply (simp add: obind_def pool_for_asid_def o_def split del: if_split)
apply (rule hoare_lift_Pf[where f=asid_table])
apply (rule hoare_lift_Pf[where f=asid_pools_of])
apply (wpsimp wp: assms entry_for_asid_lift split: option.splits)+
apply (wpsimp wp: assms entry_for_asid_lift split: option.splits split_del: if_split)+
done
lemma valid_global_arch_objs_lift:
@ -2914,6 +2914,12 @@ lemma hyp_refs_of_rev:
vcpu_tcb_refs_def refs_of_ao_def
split: kernel_object.splits arch_kernel_obj.splits option.split)
lemma valid_asid_map_lift_strong:
assumes "\<And>P. f \<lbrace>\<lambda>s. P (asid_table s)\<rbrace>"
assumes "\<And>P. f \<lbrace>\<lambda>s. P (asid_pools_of s)\<rbrace>"
shows "f \<lbrace>valid_asid_map\<rbrace>"
by (wpsimp simp: valid_asid_map_def wp: entry_for_asid_lift assms)
end
locale Arch_asid_table_update_eq = Arch +

13
proof/invariant-abstract/AARCH64/ArchKHeap_AI.thy
View File

@ -739,6 +739,12 @@ lemma valid_arch_caps_lift:
apply (wpsimp wp: cap archvspace asidtable pts)+
done
lemma valid_asid_map_lift_strong:
assumes "\<And>P. f \<lbrace>\<lambda>s. P (asid_table s)\<rbrace>"
assumes "\<And>P. f \<lbrace>\<lambda>s. P (asid_pools_of s)\<rbrace>"
shows "f \<lbrace>valid_asid_map\<rbrace>"
by (wpsimp simp: valid_asid_map_def wp: entry_for_asid_lift assms)
context
fixes f :: "'a::state_ext state \<Rightarrow> ('b \<times> 'a state) set \<times> bool"
assumes arch: "\<And>P. f \<lbrace>\<lambda>s. P (arch_state s)\<rbrace>"
@ -754,6 +760,9 @@ private lemma pred_vspace_objs_of_lift: "f \<lbrace> \<lambda>s. P (vspace_objs_
private lemma pred_pts_of_lift: "f \<lbrace> \<lambda>s. P (pts_of s) \<rbrace>"
by (intro vspace_objs_of_pts_lift pred_vspace_objs_of_lift)
private lemma pred_asid_pools_of_lift: "f \<lbrace> \<lambda>s. P (asid_pools_of s) \<rbrace>"
by (intro vspace_objs_of_aps_lift pred_vspace_objs_of_lift)
lemma valid_global_vspace_mappings_lift:
"f \<lbrace>valid_global_vspace_mappings\<rbrace>"
unfolding valid_global_vspace_mappings_def
@ -770,8 +779,8 @@ lemma valid_global_objs_lift_weak:
unfolding valid_global_objs_def by wp
lemma valid_asid_map_lift:
"\<lbrace>valid_asid_map\<rbrace> f \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>"
by (wpsimp simp: valid_asid_map_def)
"f \<lbrace>valid_asid_map\<rbrace>"
by (wp valid_asid_map_lift_strong arch pred_asid_pools_of_lift)
lemma valid_kernel_mappings_lift:
"\<lbrace>valid_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>"

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

@ -390,9 +390,12 @@ lemma invs_A:
apply (clarsimp simp: valid_arch_caps_def valid_asid_pool_caps_def unique_table_caps_def
caps_of_state_init_A_st_Null valid_table_caps_def unique_table_refs_def)
apply (clarsimp simp: state_defs)
apply (clarsimp simp: valid_global_objs_def valid_kernel_mappings_def valid_asid_map_def)
apply (clarsimp simp: valid_global_objs_def valid_kernel_mappings_def)
apply (rule conjI)
apply (clarsimp simp: equal_kernel_mappings_def)
apply (rule conjI)
apply (clarsimp simp: valid_asid_map_def entry_for_asid_def init_A_st_def init_arch_state_def
obind_def pool_for_asid_def)
apply (simp add: pspace_in_kernel_window_init_A_st cap_refs_in_kernel_window_def
caps_of_state_init_A_st_Null valid_refs_def[unfolded cte_wp_at_caps_of_state])
done

13
proof/invariant-abstract/AARCH64/ArchRetype_AI.thy
View File

@ -309,6 +309,14 @@ lemma asid_pools:
by (clarsimp simp: in_opt_map_eq s'_def ps_def)
(erule pspace_no_overlapC [OF orth _ _ cover vp])
lemma asid_pools_of':
"asid_pools_of s' p = Some ap \<Longrightarrow>
asid_pools_of s p = Some ap \<or> ap = Map.empty \<and> p \<in> set (retype_addrs ptr ty n us)"
apply (clarsimp simp: in_opt_map_eq s'_def ps_def split: if_split_asm)
apply (auto simp: default_object_def default_arch_object_def empty_pt_def tyunt
split: apiobject_type.splits aobject_type.splits)
done
lemma pts_of:
"pts_of s p = Some pt \<Longrightarrow> pts_of s' p = Some pt"
by (clarsimp simp: in_opt_map_eq s'_def ps_def)
@ -716,7 +724,10 @@ lemma valid_kernel_mappings:
lemma valid_asid_map:
"valid_asid_map s \<Longrightarrow> valid_asid_map s'"
by (clarsimp simp: valid_asid_map_def)
apply (clarsimp simp: valid_asid_map_def entry_for_asid_def obind_None_eq pool_for_asid_def
entry_for_pool_def)
apply (fastforce dest!: asid_pools_of')
done
lemma vspace_for_asid:
"vspace_for_asid asid s' = Some pt \<Longrightarrow> vspace_for_asid asid s = Some pt"

58
proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy
View File

@ -13,6 +13,14 @@ theory ArchVSpace_AI
imports VSpacePre_AI
begin
context Arch_p_asid_table_update_eq begin (* FIXME AARCh64: move to ArchInvariants_AI *)
lemma valid_asid_map_upd[simp]:
"valid_asid_map (f s) = valid_asid_map s"
by (simp add: valid_asid_map_def)
end
context Arch begin global_naming AARCH64
sublocale
@ -182,7 +190,7 @@ lemma asid_high_bits_shl:
lemma valid_asid_map_unmap:
"valid_asid_map s \<and> is_aligned base asid_low_bits \<longrightarrow>
valid_asid_map(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (asid_table s)(asid_high_bits_of base := None)\<rparr>\<rparr>)"
by (clarsimp simp: valid_asid_map_def)
by (clarsimp simp: valid_asid_map_def entry_for_asid_def obind_None_eq pool_for_asid_def)
lemma asid_low_bits_word_bits:
"asid_low_bits < word_bits"
@ -715,7 +723,7 @@ lemma find_free_vmid_valid_arch [wp]:
unfolding valid_arch_state_def by wpsimp
lemma entry_for_asid_Some_vmidD:
"entry_for_asid asid s = Some entry \<Longrightarrow> ap_vmid entry = vmid_for_asid s asid \<and> 0 < asid"
"entry_for_asid asid s = Some entry \<Longrightarrow> ap_vmid entry = vmid_for_asid s asid"
unfolding entry_for_asid_def vmid_for_asid_def entry_for_pool_def pool_for_asid_def
by (auto simp: obind_def opt_map_def if_option split: option.splits)
@ -836,6 +844,22 @@ lemma valid_vmid_table_None_upd:
"valid_vmid_table_2 table \<Longrightarrow> valid_vmid_table_2 (table(vmid := None))"
by (simp add: valid_vmid_table_2_def)
lemma valid_vmid_table_Some_upd:
"\<lbrakk> valid_vmid_table_2 table; asid \<noteq> 0 \<rbrakk> \<Longrightarrow> valid_vmid_table_2 (table (vmid \<mapsto> asid))"
by (simp add: valid_vmid_table_2_def)
crunches update_asid_pool_entry, set_asid_pool
for pool_for_asid[wp]: "\<lambda>s. P (pool_for_asid as s)"
(simp: pool_for_asid_def)
lemma update_asid_pool_entry_valid_asid_map[wp]:
"update_asid_pool_entry f asid \<lbrace>valid_asid_map\<rbrace>"
unfolding valid_asid_map_def entry_for_asid_def
apply (clarsimp simp: obind_None_eq)
apply (wpsimp wp: hoare_vcg_disj_lift hoare_vcg_ex_lift)
apply (clarsimp simp: pool_for_asid_def entry_for_pool_def obind_None_eq split: if_split_asm)
done
lemma invalidate_asid_entry_invs[wp]:
"invalidate_asid_entry asid \<lbrace>invs\<rbrace>"
unfolding invalidate_asid_entry_def invalidate_asid_def invalidate_vmid_entry_def invs_def
@ -843,7 +867,7 @@ lemma invalidate_asid_entry_invs[wp]:
supply fun_upd_apply[simp del]
apply (wpsimp wp: load_vmid_wp valid_irq_handlers_lift valid_irq_node_typ valid_irq_states_triv
valid_arch_caps_lift pspace_in_kernel_window_atyp_lift_strong
simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_asid_map_def
simp: valid_kernel_mappings_def equal_kernel_mappings_def
valid_global_vspace_mappings_def
| wps)+
apply (clarsimp simp: valid_irq_node_def valid_global_refs_def global_refs_def valid_arch_state_def
@ -852,18 +876,17 @@ lemma invalidate_asid_entry_invs[wp]:
valid_vmid_table_None_upd)
done
crunches find_free_vmid, store_vmid
for valid_asid_map[wp]: valid_asid_map
lemma find_free_vmid_invs[wp]:
"find_free_vmid \<lbrace>invs\<rbrace>"
unfolding invs_def valid_state_def valid_pspace_def
by (wpsimp wp: load_vmid_wp valid_irq_handlers_lift valid_irq_node_typ
valid_arch_caps_lift pspace_in_kernel_window_atyp_lift_strong
simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_asid_map_def
simp: valid_kernel_mappings_def equal_kernel_mappings_def
valid_global_vspace_mappings_def)
lemma valid_vmid_table_Some_upd:
"\<lbrakk> valid_vmid_table_2 table; asid \<noteq> 0 \<rbrakk> \<Longrightarrow> valid_vmid_table_2 (table (vmid \<mapsto> asid))"
by (simp add: valid_vmid_table_2_def)
lemma store_hw_asid_valid_arch[wp]:
"\<lbrace>valid_arch_state and (\<lambda>s. asid_map s asid = None \<and> arm_vmid_table (arch_state s) vmid = None \<and> asid \<noteq> 0)\<rbrace>
store_vmid asid vmid
@ -881,7 +904,7 @@ lemma store_vmid_invs[wp]:
unfolding invs_def valid_state_def valid_pspace_def
by (wpsimp wp: valid_irq_node_typ valid_irq_handlers_lift valid_arch_caps_lift
pspace_in_kernel_window_atyp_lift_strong
simp: valid_kernel_mappings_def equal_kernel_mappings_def valid_asid_map_def
simp: valid_kernel_mappings_def equal_kernel_mappings_def
valid_global_vspace_mappings_def)
lemma invalidate_vmid_entry_None[wp]:
@ -2394,6 +2417,20 @@ lemma set_asid_pool_valid_arch_state:
unfolding valid_arch_state_def
by (wpsimp wp: set_asid_pool_vmid_inv|wps)+
lemma set_asid_pool_invs_valid_asid_map[wp]:
"\<lbrace>valid_asid_map and valid_asid_table and
(\<lambda>s. asid_pools_of s ap = Some pool \<and> pool_for_asid asid s = Some ap \<and> asid \<noteq> 0)\<rbrace>
set_asid_pool ap (pool(asid_low_bits_of asid \<mapsto> ape))
\<lbrace>\<lambda>_. valid_asid_map\<rbrace>"
unfolding valid_asid_map_def entry_for_asid_def
apply (clarsimp simp: obind_None_eq)
apply (wp hoare_vcg_disj_lift hoare_vcg_ex_lift)
apply (fastforce simp: asid_high_low_inj pool_for_asid_def valid_asid_table_def entry_for_pool_def
obind_None_eq
dest: inj_on_domD
split: if_split_asm)
done
lemma set_asid_pool_invs_map:
"\<lbrace>invs and
(\<lambda>s. asid_pools_of s ap = Some pool \<and> pool_for_asid asid s = Some ap \<and>
@ -2403,10 +2440,11 @@ lemma set_asid_pool_invs_map:
and K (pool (asid_low_bits_of asid) = None \<and> 0 < asid \<and> ap_vmid ape = None)\<rbrace>
set_asid_pool ap (pool(asid_low_bits_of asid \<mapsto> ape))
\<lbrace>\<lambda>rv. invs\<rbrace>"
apply (simp add: invs_def valid_state_def valid_pspace_def valid_asid_map_def)
apply (simp add: invs_def valid_state_def valid_pspace_def)
apply (wpsimp wp: valid_irq_node_typ set_asid_pool_typ_at set_asid_pool_arch_objs_map
valid_irq_handlers_lift set_asid_pool_valid_arch_caps_map
set_asid_pool_valid_arch_state)
apply (clarsimp simp: valid_arch_state_def)
done
lemma ako_asid_pools_of:

2
spec/abstract/AARCH64/ArchVSpace_A.thy
View File

@ -50,7 +50,6 @@ definition vspace_for_pool :: "obj_ref \<Rightarrow> asid \<Rightarrow> (obj_ref
(* this is what asid_map encodes in ARM/ARM_HYP; getASIDPoolEntry in Haskell *)
definition entry_for_asid :: "asid \<Rightarrow> 'z::state_ext state \<Rightarrow> asid_pool_entry option" where
"entry_for_asid asid = do {
oassert (0 < asid);
pool_ptr \<leftarrow> pool_for_asid asid;
entry_for_pool pool_ptr asid \<circ> asid_pools_of
}"
@ -68,6 +67,7 @@ definition update_asid_pool_entry ::
definition vspace_for_asid :: "asid \<Rightarrow> 'z::state_ext state \<Rightarrow> obj_ref option" where
"vspace_for_asid asid = do {
oassert (0 < asid);
entry \<leftarrow> entry_for_asid asid;
oreturn $ ap_vspace entry
}"